Check flags are not respected within quantified expressions

[SaswatPadhi]

CBMC version: 5.34.0
Operating system: Linux

Test case:

#include <assert.h>
#include <stdlib.h>

int main() {
  char *a;

  // lots of errors with `--pointer-check` enabled
  assert(*a == *a);

  // no errors even with `--pointer-check` enabled
  assert(
    __CPROVER_forall {
      int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)
    }
  );
}

Exact command line resulting in the issue:

$ cbmc --pointer-check test.c

What behaviour did you expect:

NULL and invalid pointer issues would be checked within both assertions.

What happened instead:

NULL and invalid pointer issues are checked within first assertion but not the second. Commenting out the first assertion results in VERIFICATION SUCCESSFUL output even with --pointer-check flag.

The bounds for the quantified variable are constants and CBMC does not ignore the quantifier (with the SAT backend).

Even with the SMT backend, with which quantifiers are not unrolled, --pointer-check is not really checked within the quantified expression. Running the following gives VERIFICATION SUCCESSFUL on commenting the first assertion:

$ cbmc --z3 --pointer-check test.c

[SaswatPadhi]

cc: @feliperodri

[martin-cs]

cbmc/src/analyses/goto_check.cpp

Line 1565 in 06c563a

// we don't look into quantifiers

is the problem but the fix is non-trivial because you may need the assert in side the range of the quantifiers which doesn't work because you can't have an instructiont inside an exprt. Of the top of my head I think you might have to create a copy of the quantified expression and replace some terms with the conditions that check the assertion. This feels kind of nasty though.

  assert( __CPROVER_forall { int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)  } );

would become:

  assert( __CPROVER_forall { int i ; (0 <= i && i < 1) ==> POINTER_CHECK(*(a+i))  } );
  assert( __CPROVER_forall { int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)  } );

[martin-cs]

Of course, this is just the tip of the iceberg as what happens if the checks are from the side that is bounding the range, for example 0 <= i && i < *p.

[SaswatPadhi]

Thanks for taking a look, @martin-cs. I thought about this a little bit more along the same lines as you proposed above.

For the unbounded quantification case, which is only handled by the SMT solver, we would have an expression of the form:

assert(__CPROVER_forall { int j ; pred(j) }); // pred is some complex predicate

As you suggested above, could we instrument it to:

assert(__CPROVER_forall { int j ; pred_SAFETY(j) });
assert(__CPROVER_forall { int j ; pred(j) });

where pred_SAFETY is a conjunction of all the additional safety predicates introduced by --*-check flags on the pred expression?

This case is ignored by SAT backend. However, we can extend this idea to the bounded quantification case that is handled by the SAT backend:

assert(__CPROVER_forall { int j ; lb <= j && j <= ub ==> pred(j) }); // pred is some complex predicate

Here, in addition to pred being safe for every j, we also want lb and ub to be safe before asserting the quantified expression. So could we instrument this to:

assert(lb_SAFETY && ub_SAFETY);
assert(__CPROVER_forall { int j ; lb <= j && j <= ub ==> pred_SAFETY(j) });
assert(__CPROVER_forall { int j ; lb <= j && j <= ub ==> pred(j) }); // pred is some complex predicate

where e_SAFETY is a conjunction of all the additional safety predicates introduced by --*-check flags on an expression e?

The quantifiers are still bounded and the SAT backend should still be able to handle this.

[martin-cs]

Sounds reasonable. I wish there were a more straight-forward way of doing this but I am not immediately seeing what it would be. I guess that if the quantifier is inside an expression, so...

assume(p == NULL || __CPROVER_forall { int i ; p->start <= i && i <= p->end ==> p->data[i] == 0} );

then that will have to be copied as well.

Thinking about it, there is s simpler but less desirable approach which is to convert the quantifiers into loops. But I don't think you want to go that route.

Maybe it is worth seeing what Frama-C and VCC do for this kind of thing.

[SaswatPadhi]

Thinking about it, there is s simpler but less desirable approach which is to convert the quantifiers into loops. But I don't think you want to go that route.

Yes, we are writing these quantified predicates within contracts for functions and loops, so loop-ifying them wouldn't be possible there. For generic assertions, we could though.

[TGWDB]

cbmc/src/analyses/goto_check.cpp

Line 1565 in 06c563a

// we don't look into quantifiers

is the problem but the fix is non-trivial because you may need the assert in side the range of the quantifiers which doesn't work because you can't have an instructiont inside an exprt.

So I played around a little and tried allowing the insertion inside quantifiers to see what would come out. (That is, use the default check insertion code in goto_check.cpp for the check_rec_address and check_rec functions.) Perhaps surprisingly, this appears to work without any obvious issues.

Here is the test.c file above:

tgw@DB0907:~/github/testing/Issue6231$ cat test.c
#include <assert.h>
#include <stdlib.h>

int main() {
  char *a;

  // lots of errors with `--pointer-check` enabled
  assert(*a == *a);

  // no errors even with `--pointer-check` enabled
  assert(
    __CPROVER_forall {
      int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)
    }
  );
}

Now running it with current release version of cbmc yields the following (trimmed) output:

tgw@DB0907:~/github/testing/Issue6231$ /home/tgw/github/master-cbmc-build/bin/cbmc --pointer-check test.c
CBMC version 5.36.0 (cbmc-5.36.0) 64-bit x86_64 linux
...
[main.pointer_dereference.6] line 8 dereference failure: invalid integer address in *a: FAILURE
[main.assertion.2] line 11 assertion __CPROVER_forall { int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i) }: SUCCESS

** 6 of 8 failed (3 iterations)
VERIFICATION FAILED

Running the same code with the modifications to allow checks to be added inside forall and exist operations yields the following (trimmed) output:

tgw@DB0907:~/github/testing/Issue6231$ cbmc --pointer-check test.c
CBMC version 5.36.0 (cbmc-5.36.0-34-ga508bca27-dirty) 64-bit x86_64 linux
[main.pointer_dereference.6] line 8 dereference failure: invalid integer address in *a: FAILURE
[main.assertion.2] line 11 assertion __CPROVER_forall { int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i) }: SUCCESS
[main.pointer_dereference.7] line 11 dereference failure: pointer NULL in a[(signed long int)i]: FAILURE
[main.pointer_dereference.8] line 11 dereference failure: pointer invalid in a[(signed long int)i]: FAILURE
[main.pointer_dereference.9] line 11 dereference failure: deallocated dynamic object in a[(signed long int)i]: FAILURE
[main.pointer_dereference.10] line 11 dereference failure: dead object in a[(signed long int)i]: FAILURE
[main.pointer_dereference.11] line 11 dereference failure: pointer outside object bounds in a[(signed long int)i]: FAILURE
[main.pointer_dereference.12] line 11 dereference failure: invalid integer address in a[(signed long int)i]: FAILURE

** 12 of 14 failed (5 iterations)
VERIFICATION FAILED

This apparently seems to work.

I also experimented with some of the comments above regarding putting part of the bound check inside as in the following code:

tgw@DB0907:~/github/testing/Issue6231$ cat -n inside.c
     1  #include <assert.h>
     2  #include <stdlib.h>
     3
     4  int main() {
     5    char *a;
     6    int *p;
     7    int q = 2;
     8    p = &q;
     9
    10    // lots of errors with `--pointer-check` enabled
    11    assert(*a == *a);
    12
    13    // no errors even with `--pointer-check` enabled
    14    assert(
    15      __CPROVER_forall {
    16        int i ; (0 <= i && i < *p) ==> *(a+i) == *(a+i)
    17      }
    18    );
    19  }

and also with line 7 changed to int q; (i.e. non-deterministic initialisation) and these all yielded the same verification results (summary below):

** Results:
nondet.c function main
[main.assertion.1] line 11 assertion *a == *a: SUCCESS
[main.pointer_dereference.1] line 11 dereference failure: pointer NULL in *a: FAILURE
[main.pointer_dereference.2] line 11 dereference failure: pointer invalid in *a: FAILURE
[main.pointer_dereference.3] line 11 dereference failure: deallocated dynamic object in *a: FAILURE
[main.pointer_dereference.4] line 11 dereference failure: dead object in *a: FAILURE
[main.pointer_dereference.5] line 11 dereference failure: pointer outside object bounds in *a: FAILURE
[main.pointer_dereference.6] line 11 dereference failure: invalid integer address in *a: FAILURE
[main.assertion.2] line 14 assertion __CPROVER_forall { int i ; (0 <= i && i < *p) ==> *(a+i) == *(a+i) }: SUCCESS
[main.pointer_dereference.7] line 14 dereference failure: dead object in *p: SUCCESS
[main.pointer_dereference.8] line 14 dereference failure: pointer outside object bounds in *p: SUCCESS
[main.pointer_dereference.9] line 14 dereference failure: pointer NULL in a[(signed long int)i]: FAILURE
[main.pointer_dereference.10] line 14 dereference failure: pointer invalid in a[(signed long int)i]: FAILURE
[main.pointer_dereference.11] line 14 dereference failure: deallocated dynamic object in a[(signed long int)i]: FAILURE
[main.pointer_dereference.12] line 14 dereference failure: dead object in a[(signed long int)i]: FAILURE
[main.pointer_dereference.13] line 14 dereference failure: pointer outside object bounds in a[(signed long int)i]: FAILURE
[main.pointer_dereference.14] line 14 dereference failure: invalid integer address in a[(signed long int)i]: FAILURE

** 12 of 16 failed (5 iterations)
VERIFICATION FAILED

I also created one where the pointer checks should all be safe:

tgw@DB0907:~/github/testing/Issue6231$ cat -n safe.c
     1  #include <assert.h>
     2  #include <stdlib.h>
     3
     4  int main() {
     5    char *a = malloc(4);
     6
     7    // should be safe with `--pointer-check` enabled
     8    assert(*a == *a);
     9
    10    // should be safe with `--pointer-check` enabled
    11    assert(
    12      __CPROVER_forall {
    13        int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)
    14      }
    15    );
    16  }

And tried to see what happens with the checks here (trimmed output):

tgw@DB0907:~/github/testing/Issue6231$ cbmc --pointer-check safe.c
CBMC version 5.36.0 (cbmc-5.36.0-34-ga508bca27-dirty) 64-bit x86_64 linux
** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 26 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 31 max allocation may fail: SUCCESS

safe.c function main
[main.assertion.1] line 8 assertion *a == *a: SUCCESS
[main.pointer_dereference.1] line 8 dereference failure: pointer NULL in *a: SUCCESS
[main.pointer_dereference.2] line 8 dereference failure: pointer invalid in *a: SUCCESS
[main.pointer_dereference.3] line 8 dereference failure: deallocated dynamic object in *a: SUCCESS
[main.pointer_dereference.4] line 8 dereference failure: dead object in *a: SUCCESS
[main.pointer_dereference.5] line 8 dereference failure: pointer outside object bounds in *a: SUCCESS
[main.pointer_dereference.6] line 8 dereference failure: invalid integer address in *a: SUCCESS
[main.assertion.2] line 11 assertion __CPROVER_forall { int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i) }: SUCCESS
[main.pointer_dereference.7] line 11 dereference failure: pointer NULL in a[(signed long int)i]: SUCCESS
[main.pointer_dereference.8] line 11 dereference failure: pointer invalid in a[(signed long int)i]: SUCCESS
[main.pointer_dereference.9] line 11 dereference failure: deallocated dynamic object in a[(signed long int)i]: SUCCESS
[main.pointer_dereference.10] line 11 dereference failure: dead object in a[(signed long int)i]: SUCCESS
[main.pointer_dereference.11] line 11 dereference failure: pointer outside object bounds in a[(signed long int)i]: FAILURE
[main.pointer_dereference.12] line 11 dereference failure: invalid integer address in a[(signed long int)i]: SUCCESS

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

Which seems pretty good (i.e. not too much went wrong), although there is a failure related to checking *(a+i) is within bounds.

Based on this I'd be curious to find further examples of where it should go wrong (and will look at this myself) as well as considering how to implement a proper solution.

I'll update in future, just adding some data here.

[SaswatPadhi]

Thanks a lot for looking into this, @TGWDB! This is great :D

although there is a failure related to checking *(a+i) is within bounds.

Do we know why this is happening?

Based on this I'd be curious to find further examples of where it should go wrong

We have a few examples from the s2n project, where we need quantified loop / function contracts, and we were concerned that we may not catch some memory errors there. (cc: @feliperodri @jimgrundy) But those are pretty large test cases, and they wouldn't still be exhaustive (over all supported checks).

May be we could write small regression tests (one per supported safety check) to catch violations within quantified assertions and assumptions?

[TGWDB]

Thanks a lot for looking into this, @TGWDB! This is great :D

although there is a failure related to checking *(a+i) is within bounds.

Do we know why this is happening?

Not yet. I'm looking into this (and keeping things noted here).

Based on this I'd be curious to find further examples of where it should go wrong

We have a few examples from the s2n project, where we need quantified loop / function contracts, and we were concerned that we may not catch some memory errors there. (cc: @feliperodri @jimgrundy) But those are pretty large test cases, and they wouldn't still be exhaustive (over all supported checks).

May be we could write small regression tests (one per supported safety check) to catch violations within quantified assertions and assumptions?

Small examples are great, but even large ones that can be run independently are not too bad for me to play with. I'm curious to try and find where things go wrong and how they might be able to be fixed early on.