__CPROVER_assume behaviour different --float-overflow-check in CBMC 5.48 and CBMC 6.4

[sree314]

Apologies for not testing on 6.6 but I'm running Ubuntu 20.04.

For this file, I get verification successful (no overflow, correct) on 5.48 and verification failure on 6.3.1 and 6.4 :

#include <assert.h>


union IntFloat {
  float f;
  unsigned int i;
};

int main(void) {
  union IntFloat a, b;
  float c;
  
  __CPROVER_assume((a.i == 0x3f800000) || (a.i == 0));
  __CPROVER_assume(b.i == 0);

  c = a.f + b.f;
}

Here's the trace from 6.4:

CBMC version 6.4.0 (cbmc-6.4.0) 64-bit x86_64 linux
Type-checking test2
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Building error trace

** Results:
/tmp/test2.c function main
[main.overflow.1] line 16 arithmetic overflow on floating-point addition in byte_extract_little_endian(a, 0l, float) + byte_extract_little_endian(b, 0l, float): FAILURE

Trace for main.overflow.1:

State 11 file /tmp/test2.c function main line 10 thread 0
----------------------------------------------------
  a={ .f=0.0f } (00000000 00000000 00000000 00000000)

State 12 file /tmp/test2.c function main line 10 thread 0
----------------------------------------------------
  b={ .f=0.0f } (00000000 00000000 00000000 00000000)

State 13 file /tmp/test2.c function main line 11 thread 0
----------------------------------------------------
  c=0.0f (00000000 00000000 00000000 00000000)

Assumption:
  file /tmp/test2.c line 13 function main
  a.i == (unsigned int)0x3F800000 || a.i == (unsigned int)0

Assumption:
  file /tmp/test2.c line 14 function main
  b.i == (unsigned int)0

Violated property:
  file /tmp/test2.c function main line 16 thread 0
  arithmetic overflow on floating-point addition in byte_extract_little_endian(a, 0l, float) + byte_extract_little_endian(b, 0l, float)
  isinf(a.f) || isinf(b.f) || !isinf(FLOAT+(a.f, b.f, __CPROVER_rounding_mode))



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

and the trace from 5.48

CBMC version 5.48.0 (cbmc-5.48.0) 64-bit x86_64 linux
Parsing /tmp/test2.c
Converting
Type-checking test2
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00147907s
size of program expression: 46 steps
simple slicing removed 6 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.7519e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00261172s
Running propositional reduction
Post-processing
Runtime Post-process: 4.6756e-05s
Solving with MiniSAT 2.2.1 with simplifier
1333 variables, 4834 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.00724309s
Runtime decision procedure: 0.00992374s

** Results:
/tmp/test2.c function main
[main.overflow.1] line 16 arithmetic overflow on floating-point addition in byte_extract_little_endian(a, 0l, float) + byte_extract_little_endian(b, 0l, float): SUCCESS

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

[tautschnig]

Confirming that there is something weird going on, consider this modified version of your example (and now using the latest CBMC release):

union IntFloat {
  float f;
  unsigned int i;
};

int main(void) {
  union IntFloat a;

  __CPROVER_assume((a.i == 0x3f800000u) || (a.i == 0));
  unsigned ai = a.i;
  float af = a.f;
  __CPROVER_assert(!__CPROVER_isinff(a.f), "");
}

which yields the following trace:

$ cbmc 8633.c --trace
CBMC version 6.6.0 (cbmc-6.6.0) 64-bit x86_64 linux
Type-checking 8633
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Building error trace

** Results:
8633.c function main
[main.assertion.1] line 12 assertion: FAILURE

Trace for main.assertion.1:

State 11 file 8633.c function main line 7 thread 0
----------------------------------------------------
  a={ .f=0.0f } (00000000 00000000 00000000 00000000)

Assumption:
  file 8633.c line 9 function main
  a.i == 0x3F800000u || a.i == (unsigned int)0

State 14 file 8633.c function main line 10 thread 0
----------------------------------------------------
  ai=0x3F800000u (00111111 10000000 00000000 00000000)

State 16 file 8633.c function main line 11 thread 0
----------------------------------------------------
  af=+INFINITY (01111111 10000000 00000000 00000000)

Violated property:
  file 8633.c function main line 12 thread 0
  assertion
  !isinf(a.f)



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

Note that ai and af ought to be the same bit pattern, but for some reason aren't.

[tautschnig]

Turns out this is a bug in union field sensitivity when using uninitialised variables (which is undefined behavior in C anyway, but we've obviously tolerated this for a long time). You can avoid this problem by doing:

union IntFloat __VERIFIER_nondet_(void);

int main(void) {
  union IntFloat a = __VERIFIER_nondet_();
  union IntFloat b = __VERIFIER_nondet_();
  float c;

  __CPROVER_assume((a.i == 0x3f800000) || (a.i == 0));
  __CPROVER_assume(b.i == 0);

  c = a.f + b.f;
}

which will then successfully verify using all known versions of CBMC.

[sree314]

Ah, that makes sense. I chose a slightly roundabout workaround, and this is a better solution. Thanks!

In general, would assume'ing the value of undefined variables (other than unions) also cause this issue? If so, some of the examples in the manual here (http://www.cprover.org/cprover-manual/modeling/assumptions/) also have assume's on undefined variables and might need to be updated.

[tautschnig]

In general, would assume'ing the value of undefined variables (other than unions) also cause this issue? If so, some of the examples in the manual here (http://www.cprover.org/cprover-manual/modeling/assumptions/) also have assume's on undefined variables and might need to be updated.

No, this problem is very specific to unions as for those we (also) have one symbol for each member, yet still need to keep the values in sync across them.