Skip to content

Termination: incorrect verdict for some `ldv-linux-3.4-simple` benchmarks

The following 15 tasks are labeled as true for property termination, but I believe that all of them have an infinite execution:

ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--devices--phram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--maps--netsc520.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--maps--ts5500_flash.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--platform--x86--dell-wmi-aio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--pps--clients--pps-ktimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--staging--iio--iio_dummy_evgen.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--devices--phram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--maps--netsc520.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--maps--ts5500_flash.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--pci--pci-stub.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--platform--x86--dell-wmi-aio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--pps--clients--pps-ktimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--staging--iio--iio_dummy_evgen.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i

Existence of an infinite loop

All the ldv-linux-3.4-simple/32* files contain a code snippet in main() similar to this one:

  while (1) {
    while_continue: ;
    {
    tmp___1 = __VERIFIER_nondet_int();
    }
    if (tmp___1) {
    } else {
      goto while_break;
    }
    {
    tmp___0 = __VERIFIER_nondet_int();
    }
    {
    goto switch_default;
    if (0) {
      switch_default:
      goto switch_break;
    } else {
      switch_break: ;
    }
    }
  }

which can loop forever if the execution gets to the first line of the code and the function __VERIFIER_nondet_int() always returns 1.

And all the ldv-linux-3.4-simple/43* benchmarks contain a code snippet in main() similar to this one (a goto variant of the previous loop):

  goto ldv_15355;
  ldv_15354:
  {
  tmp___0 = __VERIFIER_nondet_int();
  }
  {
  goto switch_default;
  if (0) {
    switch_default: ;
    goto ldv_15353;
  } else {
    switch_break: ;
  }
  }
  ldv_15353: ;
  ldv_15355:
  {
  tmp___1 = __VERIFIER_nondet_int();
  }
  if (tmp___1 != 0) {
    goto ldv_15354;
  } else {
    goto ldv_15356;
  }

which can also loop forever if the execution gets to the first line of the code and the function __VERIFIER_nondet_int() always returns 1.

The only question is whether the first lines of the snippets are reachable.

Reachability of the infinite loop

I added asserts before the first line of the snippet, e.g.,

  __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);
  while (1) {

and

  __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);    
  goto ldv_15355;

and prepared input harnesses that lead to this location. When compiled (clang -Wl,--allow-multiple-definition with_assert_before_infinite_loop/$BENCHMARK harness.c) and executed (./a.out), the asserts are indeed reached.

> bash run_all.sh

Benchmark 32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:1275: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462036 Aborted                 (core dumped) ./a.out

Benchmark 32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--devices--phram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:1925: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462051 Aborted                 (core dumped) ./a.out

Benchmark 32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--maps--netsc520.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:1111: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462067 Aborted                 (core dumped) ./a.out

Benchmark 32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--maps--ts5500_flash.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:1096: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462083 Aborted                 (core dumped) ./a.out

Benchmark 32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--pps--clients--pps-ktimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:961: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462098 Aborted                 (core dumped) ./a.out

Benchmark 43_1a_cilled_ok_nondet_linux-43_1a-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:1255: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462113 Aborted                 (core dumped) ./a.out

Benchmark 43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--devices--phram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:1785: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462128 Aborted                 (core dumped) ./a.out

Benchmark 43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--maps--netsc520.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:1133: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462144 Aborted                 (core dumped) ./a.out

Benchmark 43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--maps--ts5500_flash.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:1112: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462161 Aborted                 (core dumped) ./a.out

Benchmark 43_1a_cilled_ok_nondet_linux-43_1a-drivers--pci--pci-stub.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:1455: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462176 Aborted                 (core dumped) ./a.out

Benchmark 43_1a_cilled_ok_nondet_linux-43_1a-drivers--pps--clients--pps-ktimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:950: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462192 Aborted                 (core dumped) ./a.out

Benchmark 43_1a_cilled_ok_nondet_linux-43_1a-drivers--staging--iio--iio_dummy_evgen.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:1667: void main(void): Assertion `0' failed.
run_all.sh: line 23: 3462207 Aborted                 (core dumped) ./a.out

Benchmark 32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--platform--x86--dell-wmi-aio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:3390: void main(void): Assertion `0' failed.
run_all.sh: line 32: 3462222 Aborted                 (core dumped) ./a.out

Benchmark 43_1a_cilled_ok_nondet_linux-43_1a-drivers--platform--x86--dell-wmi-aio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:3311: void main(void): Assertion `0' failed.
run_all.sh: line 32: 3462237 Aborted                 (core dumped) ./a.out

Benchmark 32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--staging--iio--iio_dummy_evgen.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
a.out: infinite loop:1754: void main(void): Assertion `0' failed.
run_all.sh: line 41: 3462252 Aborted                 (core dumped) ./a.out

Reproduction

Everything needed to reproduce the reachability test should be in the archive reproduction.zip. It contains:

  1. the original benchmarks in original
  2. the benchmarks with added asserts in with_assert_before_infinite_loop
  3. the test harnesses harness.c, harness1.c, and harness2.c that contain definitions of __VERIFIER_nondet_* functions and initialization of static extern structs (and the necessary definitions of the structs)
  4. the script run_all.sh to compile and run all the files in with_assert_before_infinite_loop together with the corresponding harnesses

The files in with_assert_before_infinite_loop only differ from the ones in original in the added asserts:

> diff -r original/ with_assert_before_infinite_loop/

diff '--color=auto' -r original/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
1274a1275
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);
diff '--color=auto' -r original/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--devices--phram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--devices--phram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
1924a1925
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);      
diff '--color=auto' -r original/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--maps--netsc520.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--maps--netsc520.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
1110a1111
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);      
diff '--color=auto' -r original/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--maps--ts5500_flash.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--mtd--maps--ts5500_flash.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
1095a1096
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);      
diff '--color=auto' -r original/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--platform--x86--dell-wmi-aio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--platform--x86--dell-wmi-aio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
3389a3390
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);      
diff '--color=auto' -r original/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--pps--clients--pps-ktimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--pps--clients--pps-ktimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
960a961
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);      
diff '--color=auto' -r original/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--staging--iio--iio_dummy_evgen.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--staging--iio--iio_dummy_evgen.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
1753a1754
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);      
diff '--color=auto' -r original/43_1a_cilled_ok_nondet_linux-43_1a-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/43_1a_cilled_ok_nondet_linux-43_1a-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
1254a1255
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);    
diff '--color=auto' -r original/43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--devices--phram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--devices--phram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
1784a1785
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);    
diff '--color=auto' -r original/43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--maps--netsc520.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--maps--netsc520.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
1132a1133
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);    
diff '--color=auto' -r original/43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--maps--ts5500_flash.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--maps--ts5500_flash.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
1111a1112
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);    
diff '--color=auto' -r original/43_1a_cilled_ok_nondet_linux-43_1a-drivers--pci--pci-stub.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/43_1a_cilled_ok_nondet_linux-43_1a-drivers--pci--pci-stub.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
1454a1455
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);    
diff '--color=auto' -r original/43_1a_cilled_ok_nondet_linux-43_1a-drivers--platform--x86--dell-wmi-aio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/43_1a_cilled_ok_nondet_linux-43_1a-drivers--platform--x86--dell-wmi-aio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
3310a3311
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);    
diff '--color=auto' -r original/43_1a_cilled_ok_nondet_linux-43_1a-drivers--pps--clients--pps-ktimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/43_1a_cilled_ok_nondet_linux-43_1a-drivers--pps--clients--pps-ktimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
949a950
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);    
diff '--color=auto' -r original/43_1a_cilled_ok_nondet_linux-43_1a-drivers--staging--iio--iio_dummy_evgen.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i with_assert_before_infinite_loop/43_1a_cilled_ok_nondet_linux-43_1a-drivers--staging--iio--iio_dummy_evgen.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
1666a1667
>   __assert_fail ("0", "infinite loop", __LINE__, __extension__ __PRETTY_FUNCTION__);
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information