Boogie Stackoverflow when running SMACK

[blizzard4591]

./smack.sh --svcomp-property sv-benchmarks/c/PropertyUnreachCall.prp --bit-precise --bit-precise-pointers --float --verifier svcomp masterPreprocessed.c
Stack overflow: IP: 0x4207f17f, fault addr: 0x7ffe563b9ff0
Stacktrace:
at Microsoft.Boogie.LoopUnroll.Visit (Microsoft.Boogie.LoopUnroll/GraphNode) [0x00138] in <732084b45df14f7aa78ec6e371b86b56>:0
<...>
at Microsoft.Boogie.LoopUnroll.UnrollLoops (Microsoft.Boogie.Block,int,bool) [0x000f1] in <732084b45df14f7aa78ec6e371b86b56>:0
at Microsoft.Boogie.Program.UnrollLoops (int,bool) [0x00047] in <732084b45df14f7aa78ec6e371b86b56>:0
at Microsoft.Boogie.ExecutionEngine.InferAndVerify (Microsoft.Boogie.Program,Microsoft.Boogie.PipelineStatistics,string,Microsoft.Boogie.ErrorReporterDelegate,string) [0x000d7] in :0
at Microsoft.Boogie.ExecutionEngine.ProcessFiles (System.Collections.Generic.List`1,bool,string) [0x00299] in :0
at Microsoft.Boogie.OnlyBoogie.Main (string[]) [0x0025b] in <52112a9183e54afd83466c8eb44e5e45>:0
at (wrapper runtime-invoke) .runtime_invoke_int_object (object,intptr,intptr,intptr) [0x00054] in <52112a9183e54afd83466c8eb44e5e45>:0

Error invoking command:
boogie smack-1.7.1-64/a-clv8e5.bpl /nologo /noinfer /doModSetAnalysis /timeLimit:890 /errorLimit:1 /loopUnroll:100 /proverOpt:OPTIMIZE_FOR_BV=true /z3opt:smt.relevancy=0 /z3opt:smt.bv.enable_int2bv=true /boolControlVC
boogie returned non-zero.

Sadly, I am unable to provide the used source code (NDAs), but I am willing to debug and triage the issue under guidance if requested.

[michael-emmi]

Hi @blizzard4591,
This problem occurs in Boogie which is a tool developed by Microsoft, presumably due to a recursive implementation of loop unrolling, and a high /loopUnroll count, possibly worsened by procedure inlining.

My suggestion — besides opening an issue with Boogie — would be to use Smack with the Corral verifier instead of Boogie. We now use Corral by default, but you can choose explicitly which verifier you want to use with Smack by passing the flag --verifier=boogie or --verifier=corral.

Given that you seem to be using an old version of Smack that didn't enable Corral by default, it would probably be a good idea to upgrade to the latest version as well.

[zvonimir]

Corral currently does not work with the --float option since as of now it still does not support floating-points. Does your example require precise reasoning about floating-points?

I suggest your try invoking SMACK without turning on various SV-COMP heuristics by using this command:

smack float_ops.c --float --bit-precise --verifier=boogie -x=svcomp

[blizzard4591]

Sorry for taking so long, I was working on generating a small example showing the problem.
Yes, reasoning about floating-point values is key for me.

I used CReduce to generate this (somewhat nonsensical) short example:

float x0 = 0.0F, x1;
int x2() {
  __VERIFIER_nondet_uchar();
  __VERIFIER_assume(1);
  __VERIFIER_assume(0);
  __VERIFIER_nondet_uchar();
  __VERIFIER_nondet_uchar();
  __VERIFIER_assume(1);
  __VERIFIER_assume(0);
  __VERIFIER_nondet_uchar();
  __VERIFIER_assume(1);
  __VERIFIER_assume(0);
  __VERIFIER_nondet_uchar();
  __VERIFIER_assume(5);
  __VERIFIER_assume(0);
  __VERIFIER_nondet_uchar();
  __VERIFIER_assume(5);
  __VERIFIER_assume(0);
  __VERIFIER_nondet_uchar();
  __VERIFIER_assume(5);
  __VERIFIER_assume(5);
  __VERIFIER_assume(0);
  __VERIFIER_nondet_uchar();
  __VERIFIER_assume(5);
  __VERIFIER_assume(0);
  __VERIFIER_nondet_uchar();
  __VERIFIER_assume(5);
  __VERIFIER_assume(0);
  __VERIFIER_nondet_uchar();
  __VERIFIER_assume(1);
  __VERIFIER_assume(0);
  __VERIFIER_nondet_uchar();
  __VERIFIER_nondet_uchar();
  __VERIFIER_assume(1);
  __VERIFIER_assume(0);

  return 0;
}

int main() {
  while (1) {
    x2() && 1;
    if (x1)
      ;
  }
}

which, when verified using the command ./smack example.c --float --bit-precise --verifier=boogie -x=svcomp crashes Boogie with a Stack Overflow.

How can I preserve the Boogie Input file for sending this to the Boogie team?

SMACK program verifier version 1.7.2
Error invoking command:
boogie /tmp/creduce/smack-1.7.2/smack/bin/a-5jL4jF.bpl /nologo /noinfer /doModSetAnalysis /timeLimit:890 /errorLimit:1 /loopUnroll:100 /proverOpt:OPTIMIZE_FOR_BV=true /z3opt:smt.relevancy=0 /z3opt:smt.bv.enable_int2bv=true /boolControlVC
boogie returned non-zero.

I can see the path, but the file gets deleted.

[zvonimir]

I investigated this issue. In short, when -x=svcomp is enabled, then SMACK automatically selects 100 loop unrolls as the default for your benchmark. Subsequently, you get the exception in Boogie, which should be investigated further.
In the meantime, I suggest you try the following:

• Add #include "smack.h" to the top of your benchmark
• Invoke SMACK using the command smack example.c --float --bit-precise --verifier=boogie --unroll=5
  This works on my machine. Clearly, you should adjust the unroll factor that suits your expectations. You will not be able to go all the way to 100, but maybe something smaller would be fine too. Please let me know if this helps.
  In the meantime, I will report the Boogie exception.

[zvonimir]

As of half a year ago or so, we added support for floating-points to Corral. This issue probably disappears once Corral is used instead of Boogie. I am closing this, unless someone comments on it providing more feedback.