Simple modular reasoning example with contracts fails

[rod-chapman]

CBMC version: 6.0.0
Operating system: macOS
Exact command line resulting in the issue: make -f make_inc2
What behaviour did you expect: success
What happened instead: verification fails - see below.

See this example: https://github.com/rod-chapman/cbmc-examples/tree/main/modularity

This is an example of modular reasoning using contracts. I have a function called "inc()" increments its parameter by one, so declared in p.h as:

int32_t inc (int32_t x)
__CPROVER_requires(x < 20)
__CPROVER_ensures(__CPROVER_return_value == x + 1);

I then want to verify a function that calls inc() twice. See the files q.h and q.c

BUT...

make -f make_inc2

fails with:

** Results:
./p.h function inc
[inc.assertion.1] line 3 undefined function should be unreachable: FAILURE

./q.h function inc2
[inc2.overflow.1] line 5 arithmetic overflow on signed + in x_wrapper + 2: SUCCESS
[inc2.postcondition.1] line 5 Check ensures clause of contract contract::inc2 for function inc2: SUCCESS

... then...
q.c function inc2
[inc2.no_alloc_dealloc_in_ensures.1] line 4 Check that ensures do not allocate or deallocate memory: SUCCESS
[inc2.no_alloc_dealloc_in_requires.1] line 4 Check that requires do not allocate or deallocate memory: SUCCESS
[inc2.no_recursive_call.1] line 4 No recursive call to function inc2 when checking contract inc2: SUCCESS
[inc2.single_top_level_call.1] line 4 Only a single top-level call to function inc2 when checking contract inc2: SUCCESS
[inc2.assigns.1] line 6 Check that r is assignable: SUCCESS
[inc2.assigns.2] line 7 Check that r is assignable: SUCCESS
[inc2.assigns.3] line 8 Check that r is assignable: SUCCESS

It appears to be unhappy because I have not compiled the body of inc() (in file p.c).

This shouldn't be necessary. Firstly, I haven't written p.c yet, so it can't be supplied. Secondly, the whole point of modular reasoning with contracts is to avoid such need in the first please?

[tautschnig]

You will want --replace-call-with-contract inc to make this work:

--- a/modularity/make_inc2
+++ b/modularity/make_inc2
@@ -17,7 +17,7 @@ results_smt: $(FILE)_contracts.goto
        cbmc $(CHECKS) --verbosity 6 --smt2 $<

 $(FILE)_contracts.goto: $(FILE).goto
-       goto-instrument --dfcc $(HARNESS) --enforce-contract $(TARGET) $< $@
+       goto-instrument --dfcc $(HARNESS) --enforce-contract $(TARGET) --replace-call-with-contract inc $< $@

 $(FILE).goto: $(FILE).c
        goto-cc --function $(HARNESS) -DCBMC -o $@ $^

With that change, verification passes as expected.

[rod-chapman]

Of course! How stupid I am... apologies.

That's likely to be a common mistake, so could we get a better error message than

[inc.assertion.1] line 3 undefined function should be unreachable: FAILURE

such as

[inc.assertion.1] line 3 unable to inline call to undefined function inc. Consider replacing contracts for this call

That would have immediately led me to the correct course of action.

In the long term, I'd still like to see this decision taken automatically - i.e. if a called function has contracts, then replace them automatically without needing the command-line switch at all.

[rod-chapman]

Or... another potential policy:

if we're verifying a function that has --enforce-contracts set for it, then automatically apply --replace-call-with-contract for all called functions that also have contracts. If a called function has no contracts, then inline if its full definition is available. If no contracts and no definition, then error.

Does that make sense?

[tautschnig]

I am concerned that a contract might not be strong enough for a particular calling context. So we'd then have to add an option "do-not-replace-call-with-contract". How about the following variation on your proposal: when a definition is not available, but a contract is available, use the contract. Otherwise, when the definition is available, use the full implementation. Else, error.

[rod-chapman]

Not sure... that would mean my verification time and complexity will unexpectedly change depending on which translation units I just happened to have compiled and linked into a single GOTO binary. Sounds fragile.

[remi-delmas-3000]

We went to some length to decouple functions and contracts, so that different contracts could be used for the same function at different call sites, or the same contract could be reused for several functions.

Right now the function/contract mapping is specified on the command line. Maybe some pragma could be used in the source code itself to tell the tools what contract to use at each call site.

[rod-chapman]

Aren't there horrible soundness issues if you prove a function implementation satisfies contract X, but then a caller says it wants contract Y?

[rod-chapman]

Which customer wants this feature? What do they use it for?

[rod-chapman]

Back to the plot - can we at least improve the error message please?