search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
827 stars 260 forks source link

CSmith test with random seed 1684847330 has dump-c checksum mismatch #7729

Open tautschnig opened 1 year ago

tautschnig commented 1 year ago

https://github.com/diffblue/cbmc/actions/runs/5057664809/jobs/9076711993?pr=6785 reported:

Checksum mismatch: GCC: 0xE09F7B20 dump-c: 0x16014CDF

It seems that the semantics of the original C source as generated by CSmith and the one produced by dump-c differ for the program generated with random seed 1684847330. Needs investigation to figure out whether the bug is in dump-c or goto-program conversion. We need to enable debug output in the test example to see where checksums start diverging.

tautschnig commented 1 year ago

The same issue arises with random seed 1684854437 (https://github.com/diffblue/cbmc/actions/runs/5058960713/jobs/9079812267?pr=7728).

tautschnig commented 11 months ago

The issue once again came up, now with random seed 1697191533 (https://github.com/diffblue/cbmc/actions/runs/6506767120/job/17672954027?pr=7933).

tautschnig commented 7 months ago

Another example is random seed 1707092271.

tautschnig commented 5 months ago

Another example is random seed 1714474363.

tautschnig commented 3 months ago

Another example is random seed 1718809244.

tautschnig commented 1 week ago

Here is a reduce example of the problem:

#include <assert.h>
#include <stdint.h>
struct S0 {
  int32_t f4 : 18;
};
int32_t g_93 = -2;
struct S0 g_164 ;
int32_t g_176 ;
int main () {
  g_176 = (g_164.f4 = g_93);
  assert(g_176 == -2);
}

The code introduced in dbe6455944ec fails to accurately represent the semantics of the above assignment through a bitfield in the output of dump-c (the GOTO program, however, is correct). Instead, we will need to create local declarations of structs-with-bitfield (or perhaps see whether we have an existing, matching type) to precisely model this.