Aliasing pre-condition not processed correctly if `is_fresh` clause it not standalone

[hanno-becker]

CBMC Version: 6.3.1

The following proves successfully:

void dummy0(int *r, int *a)
__CPROVER_requires(__CPROVER_is_fresh(r, sizeof(*r)))
__CPROVER_requires(r == a)
__CPROVER_assigns(*r)
__CPROVER_ensures(*a==42) {
  *r = 42;
}

/*
goto-cc harness.c --function harness -o a.out
goto-instrument --dfcc harness --enforce-contract dummy0 a.out b.out
cbmc b.out
*/
void harness(void) {
  int *r;
  int *a;
  dummy0(r, a);
}

The following does not:

void dummy0(int *r, int *a)
__CPROVER_requires(r != NULL && __CPROVER_is_fresh(r, sizeof(*r)))
__CPROVER_requires(r == a)
__CPROVER_assigns(*r)
__CPROVER_ensures(*a==42) {
  *r = 42;
}

/*
goto-cc harness.c --function harness -o a.out
goto-instrument --dfcc harness --enforce-contract dummy0 a.out b.out
cbmc b.out
*/
void harness(void) {
  int *r;
  int *a;
  dummy0(r, a);
}

Even if the r != NULL clause is redundant, this is surprising -- is there dedicated logic for detecting is_fresh clauses which only works when is_fresh is used at the top-level in a requires clause?

[remi-delmas-3000]

This harness gets into a state where r == a and *r != *a:

void dummy0(int *r, int *a)
__CPROVER_requires(r != NULL && __CPROVER_is_fresh(r, sizeof(int)) && r == a)
__CPROVER_assigns(*r)
__CPROVER_ensures(*a == 42) {
  int *dummy_r_before = r;
  int *dummy_a_before = a;
  int dummy_star_r_before = *r;
  int dummy_star_a_before = *a;
  __CPROVER_assert(r == a, " r == a before");
  __CPROVER_assert(*r == *a, "*r == *a before");
  *r = 42;
  int *dummy_r_after = r;
  int *dummy_a_after = a;
  int dummy_star_r_after = *r;
  int dummy_start_a_after = *a;
  __CPROVER_assert(r == a, " r == a after");
  __CPROVER_assert(*r == *a, "*r == *a after");
}

[dummy0.assertion.1] line 15  r == a before: SUCCESS
[dummy0.assertion.2] line 16 *r == *a before: FAILURE
[dummy0.assigns.1] line 17 Check that *r is assignable: SUCCESS

[dummy0.assertion.3] line 22  r == a after: SUCCESS
[dummy0.assertion.4] line 23 *r == *a after: FAILURE

with trace for dummy0.assertion.2

  dummy_r_before=&dynamic_object$10 (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 475 file cases.c function dummy0 line 12 thread 0
  dummy_a_before=&dynamic_object$10 (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 483 file cases.c function dummy0 line 13 thread 0
  dummy_star_r_before=268435502 (00010000 00000000 00000000 00101110)
State 491 file cases.c function dummy0 line 14 thread 0
  dummy_star_a_before=268435498 (00010000 00000000 00000000 00101010)

and trace for dummy0.assertion.4

State 473 file cases.c function dummy0 line 11 thread 0
  dummy_r_before=&dynamic_object$10 (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 475 file cases.c function dummy0 line 12 thread 0
  dummy_a_before=&dynamic_object$10 (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 483 file cases.c function dummy0 line 13 thread 0
  dummy_star_r_before=268435498 (00010000 00000000 00000000 00101010)
State 491 file cases.c function dummy0 line 14 thread 0
  dummy_star_a_before=268435498 (00010000 00000000 00000000 00101010)
State 498 file cases.c function dummy0 line 17 thread 0
State 499 file cases.c function dummy0 line 17 thread 0
State 500 file cases.c function dummy0 line 17 thread 0
State 523 file cases.c function dummy0 line 17 thread 0
State 531 file cases.c function dummy0 line 17 thread 0
State 533 file cases.c function dummy0 line 18 thread 0
  dummy_r_after=&dynamic_object$10 (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 535 file cases.c function dummy0 line 19 thread 0
  dummy_a_after=&dynamic_object$10 (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 543 file cases.c function dummy0 line 20 thread 0
  dummy_star_r_after=42 (00000000 00000000 00000000 00101010)
State 551 file cases.c function dummy0 line 21 thread 0
  dummy_start_a_after=268435498 (00010000 00000000 00000000 00101010)
  file cases.c function dummy0 line 23 thread 0

Interestingly, the counter examples disappear if i break down the conjunction into separate clauses:

void dummy0(int *r, int *a)
__CPROVER_requires(r != NULL)
__CPROVER_requires(__CPROVER_is_fresh(r, sizeof(int)))
__CPROVER_requires(r == a)
__CPROVER_assigns(*r)
__CPROVER_ensures(*a == 42) {
  int *dummy_r_before = r;
  int *dummy_a_before = a;
  int dummy_star_r_before = *r;
  int dummy_start_a_before = *a;
  __CPROVER_assert(r == a, " r == a before");
  __CPROVER_assert(*r == *a, "*r == *a before");
  *r = 42;
  int *dummy_r_after = r;
  int *dummy_a_after = a;
  int dummy_star_r_after = *r;
  int dummy_start_a_after = *a;
  __CPROVER_assert(r == a, " r == a after");
  __CPROVER_assert(*r == *a, "*r == *a after");
}

[dummy0.postcondition.1] line 10 Check ensures clause of contract contract::dummy0 for function dummy0: SUCCESS
...
[dummy0.assertion.1] line 15  r == a before: SUCCESS
[dummy0.assertion.2] line 16 *r == *a before: SUCCESS
...
[dummy0.assertion.3] line 22  r == a after: SUCCESS
[dummy0.assertion.4] line 23 *r == *a after: SUCCESS

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

[remi-delmas-3000]

Minimum reproducer

/* cbmc main.c */
void main(void) {
  int *r;
  int *a;
  bool tmp_if_expr;
  if(r==NULL) {
    goto L1;
  }
  r = malloc(4);
  __CPROVER_assume(r);
  tmp_if_expr = true;
  goto L2;
L1:
  tmp_if_expr = false;
L2:
  __CPROVER_assume(tmp_if_expr); 

  // if `r == NULL` held in the initial state, `malloc` was skipped, `tmp_if_expr` set to `false` and `__CPROVER_assume(false)` was executed. Since progress stops on an assume false, none of the downstream assertions will be reached with `r == NULL`.

  // if `r != NULL` held in the initial state,  `malloc` was executed, `r` was updated to a point to a fresh object, and `tmp_if_expr` set to `true` and `__CPROVER_assume(true)` was executed. Execution continue with `r` pointing to a fresh object.

  __CPROVER_assume(r == a);
  __CPROVER_assert(a == r, "a == r before");
  __CPROVER_assert(*a == *r, "*a == *r before");
  *r = 42;
  __CPROVER_assert(a == r, "a == r after");
  __CPROVER_assert(*a == *r, "*a == *r after");
}

[tautschnig]

The problem is that the value set that we use for dereferencing during symbolic execution does not have any value for a (as only assignments, but not assumptions, trigger updates to the value set).