Skip to content

CBMC 5.84 unsound in presence of undefined behaviour #7732

Closed
@rod-chapman

Description

@rod-chapman

I find CBMC 5.84 reports an unsound result for the following test case:

#include <stdio.h>

#ifdef CBMC
#else
#define __CPROVER_assert(...)
#endif

int main(void) {
  volatile int x = 0;
  int y;

  // This statement exhibits both unspecified behaviour on evalation order,
  // and also Undefined Behaviour, owing to more than one side-effect to
  // a single object before a single sequence point
  y = (x = 2) + (x = 1);

  __CPROVER_assert(y == 0, "Oops0..."); // FAILURE
  __CPROVER_assert(y == 1, "Oops1..."); // FAILURE
  __CPROVER_assert(y == 2, "Oops2..."); // SUCCESS ?!?!?
  __CPROVER_assert(y == 3, "Oops3..."); // FAILURE
  printf ("y is %d\n", y); // Prints "y is 3" with clang 14.0.3

}

An attempt to verify shows that CBMC thinks that the final value of y is 2:

rodchap@f4d4889dcf6d try % cbmc --version
5.84.0 (cbmc-5.84.0)
rodchap@f4d4889dcf6d try % cbmc -DCBMC rogu.c
CBMC version 5.84.0 (cbmc-5.84.0) 64-bit arm64 macos
Parsing rogu.c
Converting
Type-checking rogu
Generating GOTO Program
Adding CPROVER library (arm64)
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.000527709s
size of program expression: 44 steps
simple slicing removed 21 assignments
Generated 4 VCC(s), 3 remaining after simplification
Runtime Postprocess Equation: 5.792e-06s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 5.75e-05s
Running propositional reduction
Post-processing
Runtime Post-process: 2.5e-06s
Solving with MiniSAT 2.2.1 with simplifier
64 variables, 0 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 1.5708e-05s
Runtime decision procedure: 8.6625e-05s

** Results:
rogu.c function main
[main.assertion.1] line 17 Oops0...: FAILURE
[main.assertion.2] line 18 Oops1...: FAILURE
[main.assertion.3] line 19 Oops2...: SUCCESS
[main.assertion.4] line 20 Oops3...: FAILURE

** 3 of 4 failed (2 iterations)
VERIFICATION FAILED

Compling with clang 14.0.3 (on Apple M1 macOS 13.3.1):

rodchap@f4d4889dcf6d try % gcc --version     
Apple clang version 14.0.3 (clang-1403.0.22.14.1)
Target: arm64-apple-darwin22.4.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin
rodchap@f4d4889dcf6d try % gcc -o rogu rogu.c
rogu.c:15:10: warning: multiple unsequenced modifications to 'x' [-Wunsequenced]
  y = (x = 2) + (x = 1);
         ^         ~
1 warning generated.
rodchap@f4d4889dcf6d try % ./rogu
y is 3

I would hope that CBMC would detect the undefined behaviour (as clang does) and reject the program.

Metadata

Metadata

Assignees

Labels

Version 6Pull requests and issues requiring a major version bumpawsBugs or features of importance to AWS CBMC usersaws-highsoundnessSoundness bug? Review and add "aws" if it is, or remove "soundness" if it isn't.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions