Discrepancy between CBMC versions

[zhassan-aws]

CBMC version: 5.70.0, 5.71.0
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out

The results differs between CBMC 5.70 and CBMC 5.71 on the attached goto binary.

CBMC 5.70.0:

CBMC version 5.70.0 (cbmc-5.70.0) 64-bit x86_64 linux
Reading GOTO program from file s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out
Generating GOTO Program
...
/home/ubuntu/git/iss2051/s2n-quic/quic/s2n-quic-core/src/packet/number/mod.rs function packet::number::dpn
[packet::number::dpn.unreachable.1] line 280 unreachable code: SUCCESS
[packet::number::dpn.assertion.1] line 289 assertion failed: x == y: SUCCESS
...
** 0 of 142 failed (1 iterations)
VERIFICATION SUCCESSFUL

CBMC 5.71.0:

CBMC version 5.71.0 (cbmc-5.71.0) 64-bit x86_64 linux
Reading GOTO program from file s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out
Generating GOTO Program
...
/home/ubuntu/git/iss2051/s2n-quic/quic/s2n-quic-core/src/packet/number/mod.rs function packet::number::dpn
[packet::number::dpn.unreachable.1] line 280 unreachable code: SUCCESS
[packet::number::dpn.assertion.1] line 289 assertion failed: x == y: FAILURE
...
** 1 of 142 failed (2 iterations)
VERIFICATION FAILED

The result of CBMC 5.72.0 is identical to that of 5.71.0.

s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out.tar.gz

[martin-cs]

I wouldn't expect a GOTO file to be portable between versions. They are pretty much a dump of the internal data structure so if anything changes between versions they will be incorrectly formed. Treat them like .o files; I would regenerate it with each version.

Would you mind running the whole tool chain for each version and see if the results differ?

[zhassan-aws]

Makes sense. I'm still seeing the discrepancy though when starting from the symbol table file generated by Kani (attached) using the following command sequence:

symtab2gb s2n_quic_core-8f24532ce3fa20f6.symtab.json --out s2n_quic_core-8f24532ce3fa20f6.symtab.out
goto-cc s2n_quic_core-8f24532ce3fa20f6.symtab.out /home/ubuntu/git/kani/library/kani/kani_lib.c -o s2n_quic_core-8f24532ce3fa20f6.out
goto-cc s2n_quic_core-8f24532ce3fa20f6.out --function s2n_quic_core::packet::number::kani_round_trip -o s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out
goto-instrument --add-library s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out
goto-instrument --generate-function-body-options assert-false-assume-false --generate-function-body ".*" --drop-unused-functions s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out
goto-instrument --ensure-one-backedge-per-target s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out
cbmc s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out

where kani_lib.c can be found here.

s2n_quic_core-8f24532ce3fa20f6.symtab.json.tar.gz

[martin-cs]

Thanks for doing this; it rules out a few issues. This will need a closer look.

[tautschnig]

Bisecting showed that union field sensitivity (50dbf7e) introduced this spurious result. I will debug to figure out what might be going on here.