Integer Promotions with --16 --LP32

[melshuber]

Hi,

Are the integer promotions done by CBMC when using the arguments --16 --LP32 weird?

I know this post is quite long, sorry but I tried to put in as many details this issue I found.
I am also not totally sure if this is really an issue, so i mainly want to start a discussion.

Observations

When using CMBC on code for 8bit MCU (sizeof(int)==2), I encountered strange behaviour when in CBMC

unsigned int non_det_unsigned();

void integer_promotion_16(void)
{
        __CPROVER_assert(sizeof(unsigned int) == 2, "[--16] size of int is 16 bit");
        __CPROVER_assert(sizeof(unsigned long) == 4, "[--LP32] size of long is 32 bit");

        unsigned int k = non_det_unsigned();
        __CPROVER_assume(k < 1);
        __CPROVER_assert(k != 0xffff, "false counter example 16Bit?");
}

running cbmc --16 --LP32 --trace --function integer_promotion_16 testfile.c finds a counter example by assigning 0xffff to k (see cbmc output at the end of this posting). I think the counter example should be eliminated in by the assumption that k < 1.

void integer_promotion_32(void)
{
        __CPROVER_assert(sizeof(unsigned int) == 4, "[--32] size of int is 32 bit");
        __CPROVER_assert(sizeof(unsigned long) == 8, "[--LP64] size of long is 64 bit");

        unsigned int k = non_det_unsigned();
        __CPROVER_assume(k < 1);
        __CPROVER_assert(k != 0xffffffff, "using --32 --LP64 is fine");
}

On the other side the same function designed for 32bit works fine as cbmc --32 --LP64 --trace --function integer_promotion_32 testfile.c cannot find a counter example.

I dug a little deeper and added the assertion __CPROVER_assert(k < 1 && 0, "always fail"); to how the condition is evaluated.

Violated property:
  file test-cbmc.c line 10 function integer_promotion_16
  always fail
  (signed int)k < 1 && 0 != 0

This reveals that the unsigned value k is casted to signed int. Depending on the interpretation of the cast I guess it does (((signed int)0xffff) == -1) < 1, this lets CBMC can find this counter example.

Problem

However I think that CBMC is wrong in this case, because according to the usual arithmetic conversions from the C standard the right hand operator has to be converted to unsigned.

[...] if the operand that has unsigned integer type has rank greater or
equal to the rank of the type of the other operand, then the operand with
signed integer type is converted to the type of the operand with unsigned
integer type.
[...]

Further the rules in 6.3.1.1 Par 2 in the standard also do not apply because the type is already int.

When using the 32 bit version the always fail assertion, the right hand operator is casted as expected.

Violated property:
  file test-cbmc.c line 21 function integer_promotion_32
  always fail
  k < (unsigned int)1 && 0 != 0

First steps to a solution?

I think it has something to do with default arithmetic promotions to int (6.3.1.1 in the c-spec).
I did not dig to deeply into to CBMC code, but i think it is implemented in c_typecastt::minimum_promotion.

Changing the Line 418 in https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/c_typecast.cpp

  c_typet max_type = std::max(c_type, INT); break;

to

  c_typet max_type;

  // minimum promotion
  switch(config.ansi_c.int_width) {
  case 16: max_type = std::max(c_type, SHORT); break; // int has 16 Bit
  case 32: max_type = std::max(c_type, INT); break;   // int has 32 Bit
  case 64: max_type = std::max(c_type, LONG); break;  // int has 64 Bit
  default: UNREACHABLE;
  };

seems to fix the problem.

I know very little about CBMC internal, and i suspect that this change has side effects somewhere else. Therefore I did not create a pull request yet.

CBMC output

Note i also tried it with the newest CBMC version 5.8 (eb5ec24) and got the same results.

$ cbmc --16 --LP32 --trace --function integer_promotion_16 test-cbmc.c
CBMC version 5.6 64-bit x86_64 linux
Parsing test-cbmc.c
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Converting
Type-checking test-cbmc
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
**** WARNING: no body for function non_det_unsigned
size of program expression: 35 steps
simple slicing removed 2 assignments
Generated 3 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
57 variables, 77 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
57 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime decision procedure: 0.001s

** Results:
[integer_promotion_16.assertion.1] [--16] size of int is 16 bit: SUCCESS
[integer_promotion_16.assertion.2] [--LP32] size of long is 32 bit: SUCCESS
[integer_promotion_16.assertion.3] false counter example 16Bit?: FAILURE

Trace for integer_promotion_16.assertion.3:

State 18 file test-cbmc.c line 8 function integer_promotion_16 thread 0
----------------------------------------------------
  k=0u (0000000000000000)

State 22 file test-cbmc.c line 8 function integer_promotion_16 thread 0
----------------------------------------------------
  k=65535u (1111111111111111)

Violated property:
  file test-cbmc.c line 10 function integer_promotion_16
  false counter example 16Bit?
  k != 0xFFFFu


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

[martin-cs]

Thanks for the in-depth and informative query. It may take a little while to work through this and get back to you.