diffblue/cbmc

Negative Boolean variables in CNF's comments

Closed this issue · 2 comments

olegzaikin commented

CBMC version: 5.95.1
Operating system: Ubuntu 22.04 LTS
Exact command line resulting in the issue: for cbmc_test.c containing the following source code:

char Func(char aa, char bb, char cc, char dd, char M)
{
  return (aa + ((bb & cc) | dd) )+ M;
}

int main() {
  char input[2];
  char output[2];
  char a = 0;
  char b = 1;
  char c = 2;
  char d = 3;
  a = Func(a, b, c, d, input[0]);
  d = Func(d, a, b, c, input[1]);
  output[0] = a;
  output[1] = d;
  __CPROVER_assume( output[0] == 0 );
  __CPROVER_assume( output[1] == 0 );
  __CPROVER_assert(0,"test");
  return 0;
}

CNF is generated via the command

cbmc ./cbmc_test.c --dimacs --outfile cbmc_test.cnf

What behaviour did you expect: cbmc_test.cnf is a CNF in DIMACS form, where in comments for each array from cbmc_test.c the corresponding Boolean variables in the CNF are specified.
What happened instead: In the comments, variables for the array output are:
output!0@1#2[[0]] -1 -10 12 14 16 18 20 22
output!0@1#2[[1]] 32 34 -36 38 40 42 44 46
However, some of these integers are negative, e.g. -1.
Could you please explain why?

tautschnig commented

We do not necessarily introduce fresh Boolean variables for all bits of a symbol, see https://github.com/diffblue/cbmc/blob/develop/src/solvers/flattening/boolbv.cpp#L475. Instead, we try to propagate bits where possible. In your case, the values of output!0@1#2[[0]] and output!0@1#2[[1]] will really only depend on input!0@1#1[[0]] and input!0@1#1[[1]] with some bit-operations applied to them: you are adding a constant to M in Func, which we have a more efficient encoding of than the general case of adding two fully symbolic values.

Hope this helps!

  • 👍1
tautschnig commented

Closing as I believe to have answered the question. Please feel free to re-open with follow-up comments!

  • 👍1