Incorrect handling of constant variables
This witness (witness.graphml
) contains a safe and inductive invariant for the program (sw_sym_ex.c
).
However, LIV (at commit cf736e45) computes a wrong answer when checking the inductivity of the invariant.
liv$ bin/liv --no-cache-update --cache-dir lib/cvt_cache/ \
--verifier actors/cbmc.yml --verifierversion default \
--allow-missing-invariant --all-possible-invariant-locations --fuzzy-invariant-locations 1 \
--witness witness.graphml --property path/to/unreach-call.prp --data-model LP64 sw_sym_ex.c
Generated 3 programs
Using verifier "cbmc-default" from actors/cbmc.yml which claims to be tool version "CBMC 5.43.0 (cbmc-5.43.0-18-gb83f0e1cc3)"
Verification result of output/program_1.c: true
Verification result of output/program_2.c: false(unreach-call)
Verification result of output/program_3.c: true
Overall result: false
Some constant variables are declared at the beginning of main
of sw_sym_ex.c
:
// snippet of sw_sym_ex.c
typedef unsigned char SORT_1; // BV with 8 bits
const SORT_1 mask_SORT_1 = (SORT_1)-1 >> (sizeof(SORT_1) * 8 - 8);
const SORT_1 msb_SORT_1 = (SORT_1)1 << (8 - 1);
typedef unsigned char SORT_5; // BV with 1 bits
const SORT_5 mask_SORT_5 = (SORT_5)-1 >> (sizeof(SORT_5) * 8 - 1);
const SORT_5 msb_SORT_5 = (SORT_5)1 << (1 - 1);
const SORT_5 var_7 = 0;
const SORT_5 var_13 = 1;
const SORT_1 var_33 = 0;
const SORT_1 var_42 = 4;
const SORT_1 var_54 = 5;
const SORT_1 var_193 = 3;
const SORT_1 var_199 = 2;
When generating program_2.c
, LIV incorrectly havocked these constant variables:
// snippet of program_2.c
typedef unsigned char SORT_1;
const SORT_1 mask_SORT_1 = __VERIFIER_nondet_char();
const SORT_1 msb_SORT_1 = __VERIFIER_nondet_char();
typedef unsigned char SORT_5;
const SORT_5 mask_SORT_5 = __VERIFIER_nondet_char();
const SORT_5 msb_SORT_5 = __VERIFIER_nondet_char();
const SORT_5 var_7 = __VERIFIER_nondet_char();
const SORT_5 var_13 = __VERIFIER_nondet_char();
const SORT_1 var_33 = __VERIFIER_nondet_char();
const SORT_1 var_42 = __VERIFIER_nondet_char();
const SORT_1 var_54 = __VERIFIER_nondet_char();
const SORT_1 var_193 = __VERIFIER_nondet_char();
const SORT_1 var_199 = __VERIFIER_nondet_char();
As some constraints in the invariant depend on the constant variables,
such havocking alters the satisfiability of the query.
(The correct answer should be true
, but now it becomes false
.)
In fact, if program_2.c
is modified to preserve these constant values program_2_mod.c
),
then the inductivity check succeeds (confirmed by CBMC)