Asserting conditions over uninitialized variables

[salvadorer]

Dear all,
looking at the following program, I am asking myself why CBMC does not report the assertion failure:

#include <assert.h>

extern void __VERIFIER_assume(int cond);
extern int __VERIFIER_nondet_int(void);

int main(void) {
  if (__VERIFIER_nondet_int())
    goto switch_2_1;
  int tmp_ndt_4 = __VERIFIER_nondet_int();
  __VERIFIER_assume(__VERIFIER_nondet_int());
  __VERIFIER_assume (tmp_ndt_4 == 1);
  switch_2_1:
    assert(tmp_ndt_4 > 0);
  return 0;
}

I know that jumping over a variable declaration and reading the variable can give any value, so I thought the assertion should fail.
The observed behavior is especially surprising since changing the first assumption to __VERIFIER_assume(0) would give the warning about the assertion as expected.

Calling "cbmc test.c" gives:
** Results:
test.c function main
[main.assertion.1] line 13 assertion tmp_ndt_4 > 0: SUCCESS

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

CBMC version: 5.95.0
Operating system: Ubuntu

[NlightNFotis]

From a cursory reading of your program, your __VERIFIER_assume(tmp_ndt_4 == 1); statement is telling CBMC to explore only the state space where tmp_ndt_4 is equal to 1. In those states, tmp_ndt_4 > 0 is equivalent to 1 > 0 which is trivially true.

Your __VERIFIER_assume(0) is basically cutting off paths from that state space exploration, which is causing a different path to be explored (to my understanding, one in which the first if antecedent is followed, resulting in tmp_ndt_4 being nondeterministic).

[salvadorer]

For the branch in which the condition in the if is evaluated to false it makes sense, but to my understanding CBMC should explore all branches and for the other branch (where the if-condition evaluates to true) the assertion might not hold (for both versions of the first assumption). Therefore I don't understand why the assertion is not reported.

[esteffin]

Hi, I tested your program and I can say that the behaviour you experimented is a current bug of CBMC.

Here's a simplified version of your program:

#include <assert.h>

extern void __VERIFIER_assume(int cond);
extern int __VERIFIER_nondet_int(void);

int main(void) {
  int if_condition = __VERIFIER_nondet_int();
  if (if_condition) {
    goto label;
  }
  int var = __VERIFIER_nondet_int();
  __VERIFIER_assume (var == 1); 
  label:
    assert(var > 0); 
  return 0;
}

Running CBMC should return verification failure and the trace to obtain this is by having condition = 1, then as we skip the initialization of var var has a nondeterministic value, so it is possible to reach assert(var > 0 with var < 0.

For some reason it seems that the simplification step of CBMC adds a non-guarded (by the if condition) assignment var = 1.

For the moment it is possible to get the expected VERIFICATION FAILED result by adding the --no-simplify argument to CBMC.

[esteffin]

Actually it seems to be a problem also when removing the __VERIFIER_assume and initializing var to 1 in the first place as follows:

#include <assert.h>

extern void __VERIFIER_assume(int cond);
extern int __VERIFIER_nondet_int(void);

int main(void) {
  int if_condition = __VERIFIER_nondet_int();
  if (if_condition) {
    goto label;
  }
  int var = 1;
  label:
    assert(var > 0); 
  return 0;
}

Also in this case the variable var should have a nondeterministic value as its initialization is only in the control-flow where condition is false, so when condition is true it should fail violating the assertion.

This happens irregardless of --no-simplify and --no-propagation.

[tautschnig]

We might have to move all declarations (not the initialisations!) to the beginning of a block while producing the GOTO program.

[esteffin]

We might have to move all declarations (not the initialisations!) to the beginning of a block while producing the GOTO program.

I agree as:

• it is the semantics of C89,
• it seems it is the same semantics implicitly used by C99.

Still it has to be investigated why in the original program the simplifier adds an unguarded var = 1 after the __VERIFIER_assume(var == 1);.