Parsing results in Stack Overflow

[michael-schwarz]

I looked at the tasks that are worth 90x as much as others where Mopsa successfully verifies them.

Turns out that Goblint doesn't even get this far, because there already is a StackOverflow in some CIL visitor:

./goblint ../../sv-comp/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--vfio--pci--vfio-pci.ko-entry_point.cil.out.i
[Debug] Parsing files.
Frontc is parsing ../../sv-comp/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--vfio--pci--vfio-pci.ko-entry_point.cil.out.i
Fatal error: exception Stack overflow
Raised by primitive operation at GoblintCil__Cabsvisit.childrenStatement.vs in file "src/frontc/cabsvisit.ml", line 345, characters 9-136
Called from GoblintCil__Cabsvisit.mapNoCopy in file "src/frontc/cabsvisit.ml", line 122, characters 15-18
Called from GoblintCil__Cabsvisit.doVisitList in file "src/frontc/cabsvisit.ml", line 167, characters 22-55
Called from GoblintCil__Cabsvisit.childrenStatement.vs in file "src/frontc/cabsvisit.ml", line 346, characters 10-34
Called from GoblintCil__Cabsvisit.childrenStatement in file "src/frontc/cabsvisit.ml", line 406, characters 16-23
Called from GoblintCil__Cabsvisit.mapNoCopy in file "src/frontc/cabsvisit.ml", line 122, characters 15-18
[...]

[michael-schwarz]

The problem is that there is a switch over a variable of type long long and 131072 possible values are explicitly listed for one case. The task consists of 10k LoC and + 131k LoC of case statements.

[michael-schwarz]

And we can do at least this task after I have rewritten it to use an if then else for all of those cases!

[michael-schwarz]

The second task in this category that Mopsa succeeds on is of the same nature.

[michael-schwarz]

Looks like we can still parse the program to CABS, but the CABS->CIL step then fails in a visitor attempting to remove spurious parens, before any of the actual work begins.

I won't have the time to work on this, but if someone wants to write a cheap pre-processing script in python that syntactically transforms such ridiculous programs into something more meaningful, this will be very impactful for Goblint points.