SVCOMP-benchmark incorrect (reachability false alarm)

[xbauch]

The benchmark https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loop-floats-scientific-comp/loop4_true-unreach-call.c.i

is incorrectly marked as violating assertion (should be "no property violated").

CBMC version: 5.10
Operating system: 64-bit linux
Exact command line resulting in the issue: ./cbmc-wrapper --graphml-witness witness.graphml --32 --propertyfile ../sv-benchmarks/c/ReachSafety.prp ../sv-benchmarks/c/loop-floats-scientific-comp/loop4_true-unreach-call.c.i
What behaviour did you expect: VERIFICATION SUCCESSFUL
What happened instead:

Violated property:
file ../sv-benchmarks/c/loop-floats-scientific-comp/loop4_true-unreach-call.c.i function __VERIFIER_assert line 974 thread 0
assertion
FALSE

VERIFICATION FAILED
EC=10
FALSE

[xbauch]

The benchmark https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

results in:

Violated property:
file ../sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c function acpi_container_add line 3277 thread 0
strcpy src/dst overlap
POINTER_OBJECT(__cil_tmp11) != POINTER_OBJECT("ACPI container device")

VERIFICATION FAILED
EC=10
FALSE

(should've also been successful).

[xbauch]

The benchmark https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

results in:

Violated property:
file ../../sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c function acpi_fan_add line 3256 thread 0
strcpy src/dst overlap
POINTER_OBJECT(__cil_tmp13) != POINTER_OBJECT("Fan")

VERIFICATION FAILED
EC=10
FALSE

(should've also been successful).

[xbauch]

The benchmark https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--topstar-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

results in:

Violated property:
file ../../sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--topstar-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c function acpi_topstar_add line 3502 thread 0
strcpy src/dst overlap
POINTER_OBJECT(__cil_tmp11) != POINTER_OBJECT("Topstar TPSACPI")

VERIFICATION FAILED
EC=10
FALSE

(I'm not sure what the correct result should be).

[xbauch]

The benchmark https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_true-termination.4-32_1-drivers--firmware--google--gsmi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

results in:

Violated property:
file ../../sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_true-termination.4-32_1-drivers--firmware--google--gsmi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c function gsmi_get_next_variable line 4615 thread 0
memcpy src/dst overlap
POINTER_OBJECT(__cil_tmp135) != POINTER_OBJECT(__cil_tmp139)

VERIFICATION FAILED
EC=10
FALSE

(should've also been successful).

[xbauch]

The benchmark https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--video--aty--radeonfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

results in:

Violated property:
file ../../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--video--aty--radeonfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c function radeon_match_mode line 11526 thread 0
memcpy src/dst overlap
POINTER_OBJECT((void *)dest) != POINTER_OBJECT((const void *)src)

VERIFICATION FAILED
EC=10
FALSE

(should've also been successful).

[xbauch]

The benchmark https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--video--udlfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

results in:

Violated property:
file ../../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--video--udlfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c function dlfb_setup_modes line 5814 thread 0
memcpy src/dst overlap
POINTER_OBJECT((void *)&info->fix) != POINTER_OBJECT((const void *)&dlfb_fix)

VERIFICATION FAILED
EC=10
FALSE

(I'm not sure what the correct result should be).

[xbauch]

So basically for line

strcpy(__cil_tmp11, "Topstar TPSACPI");

we create a VCC stating that the source and destination pointers cannot point to the same address. I guess we can't really follow the pointer arithmetic needed for the exact value of __cil_tmp11 (so it gets abstracted to TOP). But is it really sensible to have this VCC in the case source is a constant string?

[karkhaz]

Thanks @xbauch. I might pick up some more src/dst overlaps over the next few days (these may be the same as yours, or different ones). When I do so, I'll open a PR against the sv-benchmarks repository like the others I opened, changing the memcpy calls to memmove.

I'm not sure what to do about strcpy src/dst overlap. There isn't an equivalent of memove for strings.

[peterschrammel]

The problem is that __cil_tmp11 can point anywhere because it has been computed from a nondeterministic pointer (the device passed from the main function, for which memory has never been allocated...).

Last year we did some fixes by adding preconditions to the benchmarks before calling library functions (e.g. sosy-lab/sv-benchmarks@786a943) which was not so much appreciated. Ideally, the benchmark should be fixed by allocating memory for device, which can be tricky in some cases...

[xbauch]

Or something like PR #3251, given that we know that device should point to a particular structure.

[peterschrammel]

Yes, but this must be the same for all participating verification tools. Such a harness must be part of the benchmark.

[TGWDB]

Closing as the benchmarks are no longer available and it is unclear if this can be reproduced. Please reopen if you believe this is erroneous/if you can show a current example.

[martin-cs]

Is
https://github.com/sosy-lab/sv-benchmarks/blob/99d37c5b4072891803b9e5c154127c912477f705/c/loop-floats-scientific-comp/loop4.i
the first of the benchmarks? SVCOMP has been reorganised a bit but the same benchmarks are likely still available. ( See also #3436 and #3427 )