> Am I totally on the wrong track here? That depends on what you want your assumptions to do. This definitely doesn't solve the problems I'm having implementing C++ contracts, especially axioms, which can involve declarations of undecidable functions. For example, is_reachable(p, q) for a pair of pointers can't be implemented for normal systems (maybe it could with one sanitizer or another), but it could be used for static analyzers (or optimizers maybe?) that understood the inherent meaning of a "call" to that function.
Our problem is that we need to communicate an assumption syntactically through to GIMPLE, but without the usual ODR requirements of C++. Specifically, we need to allow assumptions on conditions that use functions that are declared but not defined anywhere. Now, I'm not an optimizer expert at all, so I could be way wrong, but my sense is that depending on the constantness of a function will not help you get better assumptions, because you aren't necessarily interested in the value of the expression, only the facts introduced by it (e.g., for some x, x == 5). > Should we have __builtin_assume? I'd like it. The "if (predicate) unreachable" pattern doesn't work for C++ contracts. This works just fine for C++ contracts in LLVM. There's another solution to the problem: define undefinable functions as "= undecidable". > Should we instead fix our code so forgetting a "const" attribute won't > hurt performance if it can be inferred? Probably? If you have an assertion that you want to promote to an assumption vial __builtin_assume (using LLVM), you'll get a warning. Throw in -werror, and your program doesn't compile. That seems unfortunate. This has come up in WG21 discussions around contracts. There's some momentum to relax the requirement that asserted contracts don't have side effects because it's sometimes useful to call predicates that log something, throw, terminate, etc. If we allow "promotion" of assertions to assumptions, then that requirement is simply going to break a lot of code. Also, most functions aren't declared const, and requiring that broadly would be a non-starter for adding contracts to a program.
