ValueRelations fails to update constant bound for integers of different bitwidth

[tomsik68]

Running symbiotic on the file https://github.com/sosy-lab/sv-benchmarks/blob/master/c/busybox-1.22.0/tac-1.i crashes during instrumentation in ValueRelations plugin. Unfortunately, I can't provide smaller example right now.

The exact command I used is: ./symbiotic --save-files --sv-comp --32 --prp memsafety ~/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i >log 2>&1, symbiotic version is:

version: 7.9.0-dev
LLVM version: 8.0.1
symbiotic            -> 52661613e3fa7895b6545ae6c2c6865c2714b611 (Release)
dg                   -> d5c35153e589c743c5e1f0ae23962effb2ce12ee (Release)
sbt-slicer           -> 85c8cb482fecdd065329a55551bae93af2408c7b (Release)
sbt-instrumentation  -> 9df4452d3003e17e2e16a0094115ab81598fdcf7 (Release)
klee                 -> acd0e7c0e185418105257217f5863ef025780777 (Release)

The relevant part of crash log is in instrumentation part:

sbt-instr: /var/local/opt/llvm-8/llvm-8.0.1.src/lib/Support/APInt.cpp:195: llvm::APInt &llvm::APInt::operator+=(const llvm::APInt &): Assertion `BitWidth == RHS.BitWidth && "Bit widths must be the same"' failed.

The full log is available on pastebin.

I believe this piece of code is where it crashes, because APInt-s are not used elsewhere: https://github.com/mchalupa/dg/blob/025e9560d62cb6ef9c9a40f3c9ddee2d848262b8/include/dg/llvm/ValueRelations/RelationsAnalyzer.h#L353

[tomsik68]

This happens also on the following benchmarks:

• https://github.com/sosy-lab/sv-benchmarks/blob/master/c/aws-c-common/aws_array_eq_c_str_harness.i
• https://github.com/sosy-lab/sv-benchmarks/blob/master/c/aws-c-common/aws_byte_buf_write_from_whole_buffer_harness-1.i
• https://github.com/sosy-lab/sv-benchmarks/blob/master/c/aws-c-common/aws_priority_queue_init_dynamic_harness-1.i

[mchalupa]

@GiraffeReversed , is this still an issue?

[GiraffeReversed]

No, APInt is no longer used anywhere in the code. I also run symbiotic on the tac-1.i benchmark and no problem appeared.