Stackoverflow in Cabsvisit for SV-COMP

[michael-schwarz]

On two of the programs from SV-COMP, we get a Stackoverflow in Cabsvisit

• [ ] ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--vfio--pci--vfio-pci.ko-entry_point.cil.out.i (line 140207)
• [ ] ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point.cil.out.i (line 139889)

Called from file "src/frontc/cabsvisit.ml", line 170, characters 22-55
Called from file "src/frontc/cabsvisit.ml", line 353, characters 10-34
Called from file "src/frontc/cabsvisit.ml", line 413, characters 16-23
Called from file "src/frontc/cabsvisit.ml", line 125, characters 15-18
Called from file "src/frontc/cabsvisit.ml", line 170, characters 22-55
Called from file "src/frontc/cabsvisit.ml", line 353, characters 10-34

[michael-schwarz]

The problem seems to be in CIL indeed. During conversion from cabs to cil, a visitor is used to remove superfluous parentheses. We then run into the stack overflow because the two programs each contain a switch statement that has >130k children (the cases):

switch(pos) {
  case 786431LL:
  case 786430LL:
  case 786420LL:
   [...]
  case 655362LL:
  case 655361LL:
  case 655360LL:
}

If I reduce the number of cases to a more reasonable number, it works again.

There might be some way to modify the visitor to use recursion more sparingly, but I don't think it is worth the effort. Programs with tens of thousands of cases for a single switch are not too common in my opinion.