generate assert(false) when calling undefined function

[kroening]

This changes the symbolic execution engine to emit an assert(false) when processing a call to a function without body, instead of merely emitting a warning.

The key benefit is that undefined function bodies are a threat to soundness, especially when CBMC is run without a human operator (say in CI) who might spot the warning. A common scenario is a call to a function that was renamed, or whose signature has changed. This scenario now triggers a verification failure.

Users who prefer the previous, or other alternative behaviors, can achieve this via program instrumentation, say using goto-instrument.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: Patch coverage is 81.81818% with 2 lines in your changes missing coverage. Please review.

Project coverage is 78.38%. Comparing base (c3e5ba8) to head (6c99724).

Files	Patch %	Lines
src/goto-symex/symex_function_call.cpp	81.81%	2 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8292      +/-   ##
===========================================
- Coverage    78.40%   78.38%   -0.02%     
===========================================
  Files         1722     1722              
  Lines       188252   188267      +15     
  Branches     18497    18487      -10     
===========================================
- Hits        147593   147572      -21     
- Misses       40659    40695      +36     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[martin-cs]

The idea of getting rid of quiet-ish potential unsoundness is good but for a long time we have been telling people that type nondet_type(); is a good way to model non-determinism. What is the new recommended way?

Also should this change other tools? Could we make the semantics consistent across tools and analyses by simply adding a pass that calls generate_function_bodies with assert-false and nondet-return (or whatever the appropriate level of over-approximation we decide on).

[kroening]

The idea of getting rid of quiet-ish potential unsoundness is good but for a long time we have been telling people that type nondet_type(); is a good way to model non-determinism. What is the new recommended way?

That keeps working (and hasn't emitted a warning before, the prefix nondet_ makes the difference).

[kroening]

Also should this change other tools? Could we make the semantics consistent across tools and analyses by simply adding a pass that calls generate_function_bodies with assert-false and nondet-return (or whatever the appropriate level of over-approximation we decide on).

Worth considering! This may be somewhat specific to the tool, depending on how function pointers are handled.

[karkhaz]

Users who prefer the previous, or other alternative behaviors, can achieve this via program instrumentation, say using goto-instrument.

Can I suggest documenting how to do this, say in cprover-manual/modeling-nondeterminism.md? Something like:

 Note that the body of the function is not defined. The name of the function itself is irrelevant (save for the prefix), but must be unique. Also note that a nondeterministic choice is not to be confused with a probabilistic (or random) choice.

+ You can also cause existing function calls in your program to return a nondeterministic value by using `goto-instrument --generate-havocing-body`.
+ This is particularly useful for functions that do not have an implementation available.
+ By default, such functions are modelled as having a body of `assert(false)`, and CBMC prints a "`no body for callee`" warning.
+ This means that verification will fail on code that calls these functions.
+ Generating a havocing body for functions whose body has not been linked in ensures that you can verify code that calls these functions.
 

[kroening]

Can I suggest documenting how to do this, say in cprover-manual/modeling-nondeterminism.md? Something like:

I think it belongs into a section about modular reasoning.

[tautschnig]

Also needs to be removed from the man page.