Loop Unrolling Fails for do { } while(0) Loop contained in a switch

[michael-schwarz]

Minimal example:

// PARAM: --set exp.unrolling-factor 1
int main()
{
  int m;
  int i =0;

  switch (m)
  {
    default:
      do { } while (0);
  }
  return 0;
}

fails with

Fatal error: exception Not_found
Raised at Stdlib__Hashtbl.MakeSeeded.find in file "hashtbl.ml", line 393, characters 21-36
Called from BatOption.map in file "src/batOption.ml", line 37, characters 19-24
Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 710, characters 17-53
Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28
Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 740, characters 27-47
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 876, characters 4-105

This causes issues where some 33 tasks go from correct to Exception(Not_found) in SV-Comp 23 when enabling the auto-tuner for loop unrolling.

[sim642]

Based on the stacktrace, it seems like Cilfacade.stmt_fundecs does is missing information for the newly generated copies of statements. I guess it's constructed before unrolling.
One possibility would be to do another Cilfacade.reset_lazy at some point.

[michael-schwarz]

The problem is deeper than that, the resulting CIL program is wrong:

int main(void) 
{ 
  int m ;

  {
  {
  goto __invalid_label;
  {
  {
  {
#line 9
  if (! 0) {
#line 9
    goto loop_end;
  }
  }
  loop_continue_0: ;
  }
  switch_default: /* CIL Label */ 
  {
#line 9
  while (1) {
    while_continue: /* CIL Label */ ;
#line 9
    if (! 0) {
#line 9
      goto while_break;
    }
  }
  while_break: /* CIL Label */ ;
  }
  loop_end: ;
  }
  switch_break: /* CIL Label */ ;
  }
#line 12
  return (0);
}
}