search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
783 stars 253 forks source link

RFC : turn the interpreter into the reference semantics for GOTO programs #8277

Open martin-cs opened 2 months ago

martin-cs commented 2 months ago

Originally a valid GOTO program was one generated by goto_convert from the C front-end. This is not an ideal definition but it did the job for a while. As other language front-ends rise in importance it becomes a less useful definition. As a result there have been a number of questions about what constitute valid GOTO programs ( https://github.com/diffblue/cbmc/issues/7471 https://github.com/diffblue/cbmc/issues/6495 ) and their semantics ( https://github.com/diffblue/cbmc/issues/8258 https://github.com/diffblue/cbmc/issues/8223 https://github.com/diffblue/cbmc/issues/8196 https://github.com/diffblue/cbmc/issues/7072 https://github.com/diffblue/cbmc/issues/4323 https://github.com/diffblue/cbmc/pull/2031 ).

Having a declarative semantics would be mathematically and conceptually appealing but many of the practical benefits would be achieved by having an executable semantics. So, I propose turning the interpreter https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/interpreter_class.h into the "formal semantics" of GOTO programs. This is mostly just documentation, adding checks, invariants and assumptions and possibly some testing.

martin-cs commented 2 months ago

CC @tautschnig w.r.t. our earlier discussion

peterschrammel commented 1 month ago

It might be worth using our test suites to automatically sanity cross-check the various implementations we have (interpretation, BMC, goto-analyzer). It's likely that they disagree in a few cases and we need to make a call which of them is actually right/intended/desired.