concolic failures

[zapashcanon]

From the report generated:

    run 1151: testcomp/sv-benchmarks/c/seq-pthread/cs_stateful-1.i
    run 1150: testcomp/sv-benchmarks/c/seq-pthread/cs_stack-2.i
    run 1149: testcomp/sv-benchmarks/c/seq-pthread/cs_read_write_lock-2.i
    run 1148: testcomp/sv-benchmarks/c/seq-pthread/cs_queue-2.i
    run 1147: testcomp/sv-benchmarks/c/seq-pthread/cs_fib_longer-2.i
    run 1146: testcomp/sv-benchmarks/c/seq-pthread/cs_fib-2.i
    run 853: testcomp/sv-benchmarks/c/ntdrivers/parport.i.cil-1.c
    run 852: testcomp/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c
    run 851: testcomp/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c
    run 850: testcomp/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c
    run 849: testcomp/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c
    run 116: testcomp/sv-benchmarks/c/eca-rers2012/Problem18_label00.c
    run 115: testcomp/sv-benchmarks/c/eca-rers2012/Problem16_label00.c
    run 114: testcomp/sv-benchmarks/c/eca-rers2012/Problem15_label00.c
    run 113: testcomp/sv-benchmarks/c/eca-rers2012/Problem12_label00.c
    run 112: testcomp/sv-benchmarks/c/eca-rers2012/Problem11_label00.c
    run 111: testcomp/sv-benchmarks/c/eca-rers2012/Problem06_label00.c
    run 110: testcomp/sv-benchmarks/c/eca-rers2012/Problem05_label00.c
    run 107: testcomp/sv-benchmarks/c/busybox-1.22.0/test-1.i
    run 106: testcomp/sv-benchmarks/c/busybox-1.22.0/printf-3.i
    run 105: testcomp/sv-benchmarks/c/busybox-1.22.0/od-4.i
    run 104: testcomp/sv-benchmarks/c/busybox-1.22.0/ls-incomplete-2.i

I had a quick look at the output:

• 104, 849, 850, 851, 852, 853, 1146, 1147, 1148, 1149, 1150, 1151 (error 125) owi: internal error, uncaught exception: Failure("TODO"), I guess something is missing in the concolic monad ;
• 105 (error 26) seems to be the same as #272 ;
• 106, 107 (error 125) owi: internal error, uncaught exception: Failure("alloc: cannot allocate base pointer [...] here we should probably abort as it's done in the symbolic monad instead of failing... ;
• 110, 111, 112, 113, 114, 115, 116 (error 43) unknown import "summaries" "exit" (maybe we should add a an interface of expected imported functions to make sure we have all of them in both symbolic and concolic mode).

FYI the full results are on the server in owi/bench/results-testcomp-owi_w24_O3_concolic-2024-06-14_15h54m53s/.

[zshipko]

owi: internal error, uncaught exception: Failure("TODO")

this is also what's blocking me from experimenting with the concolic backend, i saw there were a few TODOs in https://github.com/OCamlPro/owi/blob/main/src/concolic/concolic.ml but didn't get deep enough into it to figure out which one I'm running into.

[chambart]

I would assume https://github.com/OCamlPro/owi/blob/82c1b6affcd531d06a771b56504109737228b2d7/src/concolic/concolic.ml#L85 This is the most likely one in a program compiled from C like language. This is going to occur on calls to function pointer.

[chambart]

@zshipko Could you try again now that #314 is merged ?

[zshipko]

@chambart yes, this fixes it for me - thank you!

[zapashcanon]

From the latest run:

20..87,93,94,104,106,107, 742: Failure("alloc: cannot allocate base pointer [...] are expected

105: undefined symbol are expected

110, 111, 112, 113, 114, 115, 116 (error 43): unknown import "summaries" "exit" should be fixed

1146, 1147, 1148, 1149, 1150: Failure("TODO equal_func_intf") should be fixed

We still have a lot of nothing, I guess they'll disappear by using bigger numbers of retries for the two concolic loops.

[zapashcanon]

The exit ones should be fixed in #315

[zapashcanon]

I added a commit in #315 that will abort instead of failing for the cannot allocate base pointer cases

[zapashcanon]

351 should fix the Failure("TODO equal_func_intf")