Combining mathsat, tuple-sym-flattener and smt-symex-guard gives false true

[Novak756]

Hi again, this seems to be a rather specific issue:
runnnig esbmc --mathsat --tuple-sym-flattener --smt-during-symex --smt-symex-guard on bug.c esbmc returns VERIFICATION SUCCESFUL .
Correct result should be VERIFICATION FAILED, which is also found when using a different backend solver or when running without --tuple-sym-flattener. It also finds the bug after removing unneccessary array initialisations (see bug_noArray.c in the zip)

Versions:
ESBMC: Built from commit 3462e18
MATHSAT: MathSAT5 version 5.6.10 (9293adc746be) (latest release)
I'll recheck on latest mathsat release once the build has finished.
PS: Sorry for the large WE but it has been difficult to downsize while maintaining the bug (or without running into high runtimes).

[lucasccordeiro]

Hi @Novak756,

The flag --smt-during-symex is exeprimental in ESBMC.

Do you have some specific reason why do you want to use it?

Incremental SMT:
  --smt-during-symex                    enable incremental SMT solving
                                        {experimental},
  --smt-thread-guard                    check the thread guard during thread
                                        exploration {experimental},
  --smt-symex-guard                     check conditional goto statements
                                        during symbolic execution
                                        {experimental},
  --smt-symex-assert                    check assertion statements during
                                        symbolic execution {experimental},

[Novak756]

Not necessarily, it's not urgent, just something I noticed.

[Anthonysdu]

@Novak756
I got

Solving with solver MathSAT5 version 5.5.4 (cb2aadea7102) (Feb 22 2019 08:56:16, gmp 6.1.0, gcc 4.8.5, 64-bit)
Runtime decision procedure: 6.905s
Building error trace

[Counterexample]


State 1 file esbmc_intrinsics.h line 16 column 1 thread 0
----------------------------------------------------
  alloc = ARRAY_OF(0)

with flags esbmc --mathsat --tuple-sym-flattener --smt-during-symex --smt-symex-guard bug.c Can you confrim if the flags / programs are correct?

[Novak756]

Strange... the flags are correct, but my output for bug.c is

ESBMC version 7.5.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Enabling --no-slice due to presence of --smt-during-symex
Parsing /host/bug.c
Converting
Generating GOTO Program
GOTO program creation time: 0.192s
GOTO program processing time: 0.001s
Starting Bounded Model Checking
[...]
Symex completed in: 10.932s (720 assignments)
Slicing time: 0.001s (removed 0 assignments)
Generated 144 VCC(s), 0 remaining after simplification (720 assignments)
BMC program time: 10.933s

VERIFICATION SUCCESSFUL

and for bug_noArray.c it finds the error (similar output when running bug.c with z3 instead of mathsat)

ESBMC version 7.5.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Enabling --no-slice due to presence of --smt-during-symex
Parsing /host/bug_noArray.c
Converting
Generating GOTO Program
GOTO program creation time: 0.197s
GOTO program processing time: 0.001s
Starting Bounded Model Checking
[...]
Symex completed in: 18.284s (374 assignments)
Slicing time: 0.000s (removed 1 assignments)
Generated 73 VCC(s), 1 remaining after simplification (373 assignments)
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.001s
Solving with solver MathSAT5 version 5.5.4 (cb2aadea7102) (Feb 22 2019 08:56:16, gmp 6.1.0, gcc 4.8.5, 64-bit)
Runtime decision procedure: 6.886s
Building error trace

[Counterexample]
State 1 file esbmc_intrinsics.h line 16 column 1 thread 0
----------------------------------------------------
  alloc = ARRAY_OF(0)
[...]
Violated property:
  file bug_noArray.c line 51 column 11 function main
  assertion
  0 == ((signed int)(0 == ((unsigned int)((unsigned char)(tmp___6[3])) << 24 | (16777215 & (unsigned int)((unsigned char)(tmp___6[2]))) << 16 | 16777215 & ((unsigned int)((signed int)((unsigned short int)((unsigned char)(tmp___6[1]))) << 8 | (signed int)((unsigned short int)((unsigned char)(tmp___6[0])))))))) && 0 == ((signed int)(16384 == FV35)) && (_Bool)((signed int)FV36) && ((_Bool)((signed int)FV36) || (_Bool)((signed int)FV37))

VERIFICATION FAILED

[lucasccordeiro]

@Novak756: It would be great to check the git commit you're in.

[Novak756]

I just rebuilt on the latest commit ( 7736aca ) and it's still there for me.
I'm building with cmake .. -GNinja -DDOWNLOAD_DEPENDENCIES=On -DBUILD_STATIC=On -DBoolector_DIR=$PWD/../../boolector-release -DZ3_DIR=$PWD/../../z3 -DENABLE_MATHSAT=ON -DMathsat_DIR=$PWD/../../mathsat -DENABLE_YICES=On -DYices_DIR=$PWD/../../yices -DCVC4_DIR=$PWD/../../cvc4 -DGMP_DIR=$PWD/../../gmp -DCMAKE_INSTALL_PREFIX:PATH=$PWD/../../release and mathsat wget http://mathsat.fbk.eu/download.php?file=mathsat-5.5.4-linux-x86_64.tar.gz -O mathsat.tar.gz && tar xf mathsat.tar.gz && mv mathsat-5.5.4-linux-x86_64 mathsat.
Maybe download-dependencies is fetching something incorrectly?
But if you are unable to recreate it might just be an issue on my end ...

[Anthonysdu]

The current master can output the failure in bug.c.

But the log here is different, You can also check if the uploaded program is the same as your local file.

Symex completed in: 10.932s (720 assignments)
Slicing time: 0.001s (removed 0 assignments)
Generated 144 VCC(s), 0 remaining after simplification (720 assignments)

[Novak756]

Yes that seems to be the same log I'm getting (see above). I checked against fresh downloads of the files I uploaded.

[Novak756]

Hi, in case it helps with finding the issue, I found (somewhat) smaller cases for unsoundness (no error even though the error is reachable):

extern void __VERIFIER_error();

extern char __VERIFIER_nondet_char();
extern int __VERIFIER_nondet_int();
extern unsigned long __VERIFIER_nondet_ulong();

long id(long e) {
  char f = 0;
  return e;
}

int main() 
{
  int b = __VERIFIER_nondet_int();
  long h = 1;
  char d = __VERIFIER_nondet_char();
  if (d == 0)
    b = 1;
  long i[16];
  long *array = i;
  
  for (int e = 0; e < 16; e++) {
    unsigned int g = (unsigned int)__VERIFIER_nondet_ulong();
    array[e] = id(h & g);
  }
  if ((int)i[0] == 0) {
    __VERIFIER_error();
    ;
  }
}

and imprecision (claiming div-by-zero error which is clearly not possible as the helper checks right before)

extern int __VERIFIER_nondet_int();
int div_zero_helper(f) {
    if (f == 0)
        return 0;
    return __VERIFIER_nondet_int() / f;
}

int main() {
    int d = __VERIFIER_nondet_int();
    long h[4];
    long *a = h;
    for (int b = 0; b < 4; b++) {
        d = h[3];
        a[b] = div_zero_helper((short)d);
    }
}

These are triggered when running with --mathsat --smt-during-symex --smt-symex-guard
Unfortunately, I could not get them smaller than this without the error disappearing.
This is still not urgent, but maybe it helps :)
Version: Built from latest main 602c8d6 ; mathsat 5.5.4. (as in BUILDING.md)