Hacker News
points by rramadass 4 days ago | 0 comments
> Why would anyone that already ditched C asserts use C++ contracts when it can’t express what the alternatives already can?

You have not understood the C++26 contracts proposal.

It introduces three new syntax viz. "Pre" and "Post" in function signature declaration and a separate "contract_assert" which you can use anywhere in the code path.

It is the "Pre"/"Post" that is useful here. Since it is part of function signature declaration, a static analyzer can easily make sure that all function calls satisfy the contract else you get warning/error. The compiler on its part can inject appropriate code at the function boundary points to do runtime checking etc.

You cannot do this with assert macros. If you wanted something like this earlier, you would have had to change the compiler to emit modified function prologue/epilogue and build your own contract framework which few people had the capability to do.

You can now see the immediate benefits particularly for standard library (and other) code hardening needs. Many UB circumstances can be easily flagged at compile time without too much complexity.

Finally, note that if you use compile-time switch "ignore" to turn-off everything, only the runtime checks are elided (so you do not lose any performance) but the static analyzer can still catch all possible inconsistencies at compile-time thus giving you the best of both worlds.

[–] William_BB 4 days ago
> a static analyzer can easily make sure that all function calls satisfy the contract

How realistic is the "all function calls" part? Maybe I just don't see the bigger picture, but I would expect most function calls arguments to only be known at runtime, which of course makes static analysis not possible?

[–] rramadass 3 days ago
No, that's not how to look at it.

Obviously "all function calls" phrase cannot be absolute, but most can be caught with the analyzer giving one of proved/disproved/unknown result. The reason all cannot be caught is because pre/post are logical predicates on sets of values and are not part of the typing system.

To understand that, you have to know how a static analyzer works and specifically two of its functions, "Data Flow Analysis" and "Symbolic Execution".

It is Symbolic Execution that does static checking without the need for the actual runtime values to be known. It basically "executes" the code mathematically, building logical predicates over "sets of values" (indicated by the type of the variable) and thence trying to prove/disprove the formula using a solver. Note that the program is being "run" abstractly in the mathematical world using quantifiers just like you do in a mathematical proof.

If you know Hoare triples, and Dijkstra's WP-Calculus you know how to do this mechanically.

So the analyzer does two things; a) in the function itself it assumes pre is true and tries to prove post and b) at the call site it makes sure the paths leading up to the invocation satisfy the pre/post args/result needs thus chaining everything through the codebase. Both are done using symbolic execution. If it cannot prove/disprove the assertions, it remains silent (i.e. "unknown" result above) and leaves it to runtime checks to catch the violations.

Some resources:

1) How Static Analysis works - https://pvs-studio.com/en/blog/posts/1048/

2) A Gentle Introduction to Symbolic Execution for Software Security - https://can-ozkan.medium.com/a-gentle-introduction-to-symbol...

3) Scaling Symbolic Execution to Large Software Systems - https://arxiv.org/abs/2408.01909

[–] William_BB 3 days ago
Thanks for a detailed response, this is very educational
[–] rramadass 3 days ago
Glad you found it useful.

See also: Catching Bugs Early: Validating C++ Contracts with Static Analysis - https://news.ycombinator.com/item?id=50379283