How does this differ from existing LLVM interprocedural optimizations? Particularly value propagation sounds like it would handle a lot of these cases.

> You might have heard of dead-code elimination, an LLVM optimization pass that removes code proven as unreachable. I was actually interested in less-obvious situations. In particular blocks that are reachable on the control flow graph, but not when consider wider execution invariants.

I've got a trivial example here: https://gcc.godbolt.org/z/7EnPG5WM6 noinline is added to foo to demonstrate Clang is actually changing the number of arguments foo takes, and its inlined the arguments from bar and baz.

> Can we use information on the call-sites and the corresponding format strings to prove that some code paths, for example formatting for floating point numbers, are actually never taken?

Seems to already have that effect in Clang. Using Emscripten 3.1.3, compiling 2 different main's with just

    printf("Hello world %d\n", argc);

And

    printf("Hello world %d %f\n", argc, volatileFloatArg);

For the single int arg, the top 3 symbols by size are

    47.7%  2.65Ki -NAN(IND)%       0    printf_core
     7.4%     421 -NAN(IND)%       0    [section Data]
     6.6%     375 -NAN(IND)%       0    main

And for the one that added a float arg,

    34.5%  3.04Ki -NAN(IND)%       0    fmt_fp
    28.8%  2.54Ki -NAN(IND)%       0    printf_core
     5.1%     464 -NAN(IND)%       0    [section Data]

So when a float argument wasn't passed into printf, it did not include fmt_fp, a delegate that handles floating point for printf

One issue that can complicate this analysis is linking multiple libraries that reference standard library (or functions in other libraries). If you're linking together object code, without more IR context, LLVM is going to have to be more conservative. So I think if you link in a WASM object code file that references printf, it won't be able to perform all the IPO that will allow it to trim the CFG.