Bug: Taipan-Default does not detect reachable error call

[AlexWatts98]

Basic Info

• Version: 0.3.0-dev-c73552deb7 (d790fec)

• Java Version: 21.0.8

• Operating System: Ubuntu 22.04.5 LTS

• Input file: bug.c

• Settings: svcomp-Reach-64bit-Taipan_Default.epf.txt (Added .txt file extension because upload was blocked for .epf)

• Toolchain: TaipanReach.xml

• Complete Ultimate log files: taipan-default.log, taipan-bitvector.log, automizer-default.log

• Command: UTaipan-linux/Ultimate -tc UTaipan-linux/config/TaipanReach.xml -s UTaipan-linux/config/svcomp-Reach-64bit-Taipan_Default.epf -i bug.c

• Commands for sanity checks with Taipan-Bitvector and Automizer-Default:
  UTaipan-linux/Ultimate -tc UTaipan-linux/config/TaipanReach.xml -s UTaipan-linux/config/svcomp-Reach-64bit-Taipan_Bitvector.epf -i bug.c
UAutomizer-linux/Ultimate -tc UAutomizer-linux/config/AutomizerReach.xml -s UAutomizer-linux/config/svcomp-Reach-64bit-Automizer_Default.epf -i bug.c

Description

The __VERIFIER_error(); in the given bug.c should be reachable (for instance when packet contains only 0, except for packet[34]=3 and packet[240]=53). However, with Taipan-Default Ultimate claims that the program is correct, while it reports it as incorrect for the other toolchains.

I have added the logs for Taipan-Bitvector and Automizer-Default above as examples, but Automizer, GemCutter and Kojak all behave as expected for me and report the error as reachable with both Default and Bitvector settings.

Interestingly, Taipan-Default seems to be able to correctly identify the error when I remove the comment at the counter variable increment in the loop or even just delete some empty lines.

[maul-esel]

Thank you @AlexWatts98 for reporting this bug.

I can reproduce it on the latest dev (35a8436) as well. It seems to be a genuine soundness bug in SIFA (symbolic interpretation with fluid abstractions), the engine behind Taipan. If I run the analysis with Java asserts enabled (-ea), Taipan internally detects the unsoundness and fails with

java.lang.AssertionError: invalid Hoare triple in SifaRunner Trace length 15
	at de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.singletracecheck.TraceCheckUtils.checkInterpolantsInductivityForward(TraceCheckUtils.java:213)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.SifaRunner.<init>(SifaRunner.java:119)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.IpTcStrategyModuleSifa.construct(IpTcStrategyModuleSifa.java:67)

In particular, the invalid Hoare triple is the following:

5: Hoare triple

{464#(and
  (<= 1931 |#StackAllocations|)
  (= |#InitialAllocations| 1)
  (<= |ULTIMATE.start_main_~c~0#1| 127)
  (= |ULTIMATE.start_main_~counter~0#1| 0)
  (<= 2 |#StackHeapBarrier|)
  (<= 0 (+ |ULTIMATE.start_main_~c~0#1| 128))
  (<= 3 |ULTIMATE.start_main_~#packet~0#1.base|)
)}

assume !(0 == main_~state~0#1);

{466#(and
  (= |#InitialAllocations| 1)
  (or
    (and
      (= 2 |ULTIMATE.start_main_~state~0#1|)
      (= (+ |ULTIMATE.start_main_~#packet~0#1.base| 1928) |#StackAllocations|)
      (= (mod (select |#memory_int| (+ |ULTIMATE.start_main_~#packet~0#1.base| 248)) 256) 0)
      (<= (+ |#StackHeapBarrier| 1) |ULTIMATE.start_main_~#packet~0#1.base|)
      (exists ((|v_ULTIMATE.start_main_~c~0#1_60| Int))
        (and
          (<= |v_ULTIMATE.start_main_~c~0#1_60| 127)
          (= 35 (mod |v_ULTIMATE.start_main_~c~0#1_60| 256))
          (<= 0 (+ |v_ULTIMATE.start_main_~c~0#1_60| 128))
        )
      )
    )
    (and
      (= (+ |ULTIMATE.start_main_~#packet~0#1.base| 1928) |#StackAllocations|)
      (= (mod (select |#memory_int| (+ |ULTIMATE.start_main_~#packet~0#1.base| 248)) 256) 0)
      (<= (+ |#StackHeapBarrier| 1) |ULTIMATE.start_main_~#packet~0#1.base|)
      (exists ((|v_ULTIMATE.start_main_~c~0#1_62| Int) (|v_ULTIMATE.start_main_#t~mem11#1_22| Int))
        (and
          (<= |v_ULTIMATE.start_main_~c~0#1_62| 127)
          (or
            (and
              (= 35 (mod |v_ULTIMATE.start_main_~c~0#1_62| 256))
              (or
                (and
                  (= 2 |ULTIMATE.start_main_~state~0#1|)
                  (not (= (mod (select |#memory_int| (+ |ULTIMATE.start_main_~#packet~0#1.base| 264)) 256) 0))
                )
                (and
                  (= (mod (select |#memory_int| (+ |ULTIMATE.start_main_~#packet~0#1.base| 264)) 256) 0)
                  (= |ULTIMATE.start_main_~state~0#1| 4)
                )
              )
            )
            (and
              (= 2 |ULTIMATE.start_main_~state~0#1|)
              (= |ULTIMATE.start_main_#t~mem11#1| |v_ULTIMATE.start_main_#t~mem11#1_22|)
              (not (= 35 (mod |v_ULTIMATE.start_main_~c~0#1_62| 256)))
            )
          )
          (<= 0 (+ |v_ULTIMATE.start_main_~c~0#1_62| 128))
        )
      )
      (exists ((|v_ULTIMATE.start_main_~c~0#1_60| Int))
        (and
          (<= |v_ULTIMATE.start_main_~c~0#1_60| 127)
          (= 35 (mod |v_ULTIMATE.start_main_~c~0#1_60| 256))
          (<= 0 (+ |v_ULTIMATE.start_main_~c~0#1_60| 128))
        )
      )
    )
  )
  (<= |ULTIMATE.start_main_~c~0#1| 127)
  (= |ULTIMATE.start_main_~counter~0#1| 0)
  (<= 2 |#StackHeapBarrier|)
  (<= 0 (+ |ULTIMATE.start_main_~c~0#1| 128))
)} is INVALID

Notably, the precondition doesn't contain any information about the variable |ULTIMATE.start_main_~state~0#1|, the statement only assumes it is non-zero, and the postcondition claims it must be 2 or 4.

@danieldietsch you know most about SIFA. Do you have any idea what could cause this, or where to look for the bug?