Function --enforce-contract causes global var precondition assertion to fail

[BeamRaceMuppet]

CBMC version: 6.1.1

Instrumenting a function with --enforce-contract that has in its contract a precondition that a global variable be set to a particular value prior to entry causes assertions that the value is correctly set prior to call to fail. Minimal reproducer:

#include <stdbool.h>

bool is_initialized = false;

// Avoid double-initialization by requiring is_initialized==false
void initialize(void)
__CPROVER_requires(is_initialized == false)
__CPROVER_ensures(is_initialized == true)
__CPROVER_assigns(is_initialized)
{
    is_initialized = true;
}

int main(void)
{
    __CPROVER_assert(is_initialized == false, "Precondition for initialize()");
    initialize();
    __CPROVER_assert(is_initialized == true, "Postcondition for initialize()");

    return 0;
}

CBMC is run like this:

goto-cc initialize.c -o initialize.goto && goto-instrument --enforce-contract initialize  initialize.goto initialize.inst.goto && cbmc initialize.inst.goto

Expected output: VERIFICATION SUCCESSFUL.

Observed output:

** Results:
initialize.c function initialize
[initialize.postcondition.1] line 8 Check ensures clause: SUCCESS
[initialize.assigns.1] line 9 Check that is_initialized is valid: SUCCESS
[initialize.assigns.2] line 11 Check that is_initialized is assignable: SUCCESS

initialize.c function main
[main.assertion.1] line 16 assertion is_initialized == false: FAILURE
[main.assertion.2] line 18 Postcondition for initialize(): SUCCESS

** 1 of 5 failed (2 iterations)
VERIFICATION FAILED

Note that simply running

    cbmc initialize.c

Results in success:

** Results:
initialize.c function main
[main.assertion.1] line 16 assertion is_initialized == false: SUCCESS
[main.assertion.2] line 18 Postcondition for initialize(): SUCCESS

Also, using --replace-call-with-contract instead of --enforce-contract like this:

    goto-cc initialize.c -o initialize.goto && goto-instrument --replace-call-with-contract initialize  initialize.goto initialize.inst.goto && cbmc --trace initialize.inst.goto

Also results in success:

initialize.c function main
[main.assertion.1] line 16 assertion is_initialized == false: SUCCESS
[main.assertion.2] line 18 Postcondition for initialize(): SUCCESS

But using both --replace-call-with-contract and --enforce-contract like this:

goto-cc initialize.c -o initialize.goto && goto-instrument --enforce-contract initialize --replace-call-with-contract initialize initialize.goto initialize.inst.goto && cbmc initialize.inst.goto

Still results in failure:

[initialize.precondition.1] line 17 Check requires clause of initialize in main: FAILURE

initialize.c function main
[main.assertion.1] line 16 assertion is_initialized == false: FAILURE
[main.assertion.2] line 18 Postcondition for initialize(): SUCCESS

If we add the line "is_initialized = false" right before the assertion it is false, like this:

int main(void)
{
    is_initialized = false;
    __CPROVER_assert(is_initialized == false, "Precondition for initialize()");
    [...]

Then using --enforce-contract will finally prove the precondition assertion:

initialize.c function main
[main.assertion.1] line 17 Precondition for initialize(): SUCCESS

[lks9]

Just an observation, the example can be much simplified, you don't need a precondition for initilialize:

#include <stdbool.h>

void initialize(void)
__CPROVER_ensures(true)
{
    // nothing here
}

bool var = false;

void main(void)
{
    assert(var == false);
}

My suspicion is that --enforce-contract implies --nondet-static to use symbolic/non-deterministic values for global variables. So initializations like var = false are ignored and then assertion FAILURE is expected. I could imagine that the only problem here would be missing documentation for that.

The option --nondet-static makes sense especially in modular contract-based verification, where we do not assume that variable values are still as initilized before the execution of a function. But for your example, since the main function is executed first, one would normally assume they are still as initialized.

[BeamRaceMuppet]

Thanks for your explanation @lks9, which makes sense.

Having used two other industrialized verifiers with modular verification, Frama-C with WP and Ada/SPARK, I would suggest CBMC could improve its behavior in a way that makes users happier (and by extension the developers happier, by way of reduced issue reports) by doing the following: Have --enforce-contract do the implied --nondet-static only from the "perspective" of the function being enforced. So in your minimal example which has two functions, main and initialize, var would be --nondet-static only from the "perspective" of initialize and not from the "perspective" of main.

Frama-C/WP and Ada/SPARK already behave roughly like this. (There are technicalities, but my original example directly translated to either system would more or less work.)

As a workaround for now I can use a C preprocessor define to simulate what I am proposing, by hiding from an --enforce-contract run the code that will break because of its implied --nondet-static. For example, my original reproducer can be modified as follows:

#include <stdbool.h>

bool is_initialized = false;

// Avoid double-initialization by requiring is_initialized==false
void initialize(void)
__CPROVER_requires(is_initialized == false)
__CPROVER_ensures(is_initialized == true)
__CPROVER_assigns(is_initialized)
{
    is_initialized = true;
}

#ifndef ENFORCE_CONTRACT
int main(void)
{
    __CPROVER_assert(is_initialized == false, "Precondition for initialize()");
    initialize();
    __CPROVER_assert(is_initialized == true, "Postcondition for initialize()");

    return 0;
}
#endif //ENFORCE_CONTRACT

Then we can --enforce-contract this way:

goto-cc -DENFORCE_CONTRACT initialize.c -o initialize.goto && goto-instrument --enforce-contract initialize  initialize.goto initialize.inst.goto && cbmc --function initialize initialize.inst.goto

Which gives us success:

** Results:
initialize.c function initialize
[initialize.postcondition.1] line 8 Check ensures clause: SUCCESS
[initialize.assigns.1] line 9 Check that is_initialized is valid: SUCCESS
[initialize.assigns.2] line 11 Check that is_initialized is assignable: SUCCESS

** 0 of 3 failed (1 iterations)
VERIFICATION SUCCESSFUL

And then to verify the larger program main we do this:

goto-cc initialize.c -o initialize.goto && goto-instrument --replace-call-with-contract initialize  initialize.goto initialize.inst.goto && cbmc initialize.inst.goto

Resulting in:

** Results:
initialize.c function initialize
[initialize.assigns.1] line 9 Check that is_initialized is valid: SUCCESS
[initialize.pointer_dereference.1] line 9 dereference failure: pointer outside object bounds in *((_Bool *)__car_lb): SUCCESS
[initialize.precondition.1] line 18 Check requires clause of initialize in main: SUCCESS

initialize.c function main
[main.assertion.1] line 17 Precondition for initialize(): SUCCESS
[main.assertion.2] line 19 Postcondition for initialize(): SUCCESS

** 0 of 5 failed (1 iterations)
VERIFICATION SUCCESSFUL

I suppose the CBMC developers currently envision users separating out functions into separate files for modular verification with --enforce-contract, but for many larger projects that would like to incrementally adopt CBMC this is going to create friction and require too much rework of build systems, etc.

Finally, if nothing else, certainly documentation needs to be improved, as you mentioned, and it would be good if CBMC issued a warning when --enforce-contract is used that it is changing initialized globals to be nondet. The warning could look something like:

Warning: initialize.c line 3: Ignoring initialization of is_initialized. Will be treated as non-deterministic (because --enforce-contract).

[lks9]

Thank you for the context!

Then we can --enforce-contract this way:

goto-cc -DENFORCE_CONTRACT initialize.c -o initialize.goto && goto-instrument --enforce-contract initialize initialize.goto initialize.inst.goto && cbmc --function initialize initialize.inst.goto

It tried it out, with the option --function you don't need the #ifndef workaround, it also works fine with the original version of your program. For the main function, --function main is implicit.

I suppose the CBMC developers currently envision users separating out functions into separate files for modular verification with --enforce-contract, but for many larger projects that would like to incrementally adopt CBMC this is going to create friction and require too much rework of build systems, etc.

I guess so, since even the never-reached assertions inside a different function still appear in the ** Results, even when the function itself is never reached.

Finally, if nothing else, certainly documentation needs to be improved, as you mentioned, and it would be good if CBMC issued a warning when --enforce-contract is used that it is changing initialized globals to be nondet. The warning could look something like:

Personally, I doubt that such a specific warning would be helpful in other situations. I think it would be much more helpful to have a bit more insight in the settings cbmc is using, not only the command line arguments but a way to export (and import) the exact settings cbmc is using internally. Then one could just look in this file and directly tell "ah, yes, this behavior comes from the option nondet_static = true". I am still only guessing that it came from that option.

This could give more insight, as it seems that there are some undocumented default values when command line flags are missing or when other options are given (perhaps with a --show-settings FILE). Importing the settings could be a bit more convenient than having all options in the command line (perhaps with a --use-settings FILE). That would make the options (and their implicit defaults) more transparent.