Insufficient details to construct counterexample path

michael-emmi commented 4 years ago
This probably boils down to an issue with Corral, but I thought I’d post here first in case there’s some issue with the way we’re invoking Corral.
% cat a.c && echo --- && smack a.c
#include <smack.h>
#include <stdio.h>

int main() {
        int x = 0;
        printf("Hello, world!");
        assert(x);
}
---
SMACK program verifier version 2.4.0
Traceback (most recent call last):
  File "/usr/local/bin/smack", line 13, in <module>
    smack.top.main()
  File "/usr/local/bin/../share/smack/top.py", line 685, in main
    verify_bpl(args)
  File "/usr/local/bin/../share/smack/top.py", line 507, in verify_bpl
    verifier_output = try_command(command, timeout=args.time_limit)
  File "/usr/local/bin/../share/smack/utils.py", line 69, in try_command
    raise Exception(output)
Exception: Single threaded program detected
LB: Took 0.00 s
Verifying program while tracking: {assertsPassed}
Program has a potential bug: 
Unhandled Exception:
CoreLib.InsufficientDetailsToConstructCexPath: StratifiedInliningErrorReporter: Must find a successor
  at CoreLib.StratifiedInliningErrorReporter.GetAbsyTraceLabels (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x000ce] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at CoreLib.StratifiedInliningErrorReporter.GetAbsyTrace (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x00027] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at CoreLib.StratifiedInliningErrorReporter.OnModel (System.Collections.Generic.IList`1[T] labels, Microsoft.Boogie.Model model, Microsoft.Boogie.ProverInterface+Outcome proverOutcome) [0x0002e] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.CheckOutcomeCore (Microsoft.Boogie.ProverInterface+ErrorHandler handler, System.Int32 taskID) [0x006d0] in <19ca4884bb9d4ccb8c3a80682b5b183b>:0 
  at CoreLib.StratifiedInlining.CheckVC (Microsoft.Boogie.ProverInterface+ErrorHandler reporter) [0x0003e] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at CoreLib.StratifiedInlining.Fwd (System.Collections.Generic.HashSet`1[T] openCallSites, CoreLib.StratifiedInliningErrorReporter reporter, System.Boolean main, System.Int32 recBound) [0x00110] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at CoreLib.StratifiedInlining.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00645] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at VC.ConditionGeneration.VerifyImplementation (Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1[Microsoft.Boogie.Counterexample]& errors, System.String requestId) [0x00019] in <693f0436fa9c41f6a229442309a8ffe4>:0 
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Boolean needErrorTraces, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Collections.Generic.List`1[System.String]& timedOut, System.Boolean isCBA) [0x003f0] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Boolean isCBA) [0x00007] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at cba.VerificationPass.feedToBoogie (cba.CBAProgram p) [0x00070] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at cba.VerificationPass.runCBAPass (cba.CBAProgram prog) [0x0001f] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at cba.CompilerPass.runPass (Microsoft.Boogie.Program inp) [0x00012] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at ProgTransformation.TransformationPass.run (ProgTransformation.PersistentProgram inp) [0x0009c] in <5fc8c0b22e1047d2a1bef434cbda2c83>:0 
  at cba.CompilerPass.run (cba.PersistentCBAProgram inp) [0x00007] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at cba.CBADriver.VerifyProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x00156] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.CBADriver.checkPath (cba.PersistentCBAProgram prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x0002a] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.CBADriver.checkPath (cba.PersistentCBAProgram pmeta, cba.VarSet trackedVars, cba.ErrorTrace& trace) [0x00001] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.Driver.checkAndRefinePathFewPasses (cba.PersistentCBAProgram counterexample, cba.RefinementState refinementState, cba.ErrorTrace& cexTrace) [0x00013] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.Driver.checkAndRefine (cba.PersistentCBAProgram prog, cba.RefinementState refinementState, System.Action`2[T1,T2] printTrace, cba.ErrorTrace& cexTrace) [0x001d4] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.Driver.run (System.String[] args) [0x00466] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.Driver.Main (System.String[] args) [0x00067] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
[ERROR] FATAL UNHANDLED EXCEPTION: CoreLib.InsufficientDetailsToConstructCexPath: StratifiedInliningErrorReporter: Must find a successor
  at CoreLib.StratifiedInliningErrorReporter.GetAbsyTraceLabels (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x000ce] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at CoreLib.StratifiedInliningErrorReporter.GetAbsyTrace (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x00027] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at CoreLib.StratifiedInliningErrorReporter.OnModel (System.Collections.Generic.IList`1[T] labels, Microsoft.Boogie.Model model, Microsoft.Boogie.ProverInterface+Outcome proverOutcome) [0x0002e] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.CheckOutcomeCore (Microsoft.Boogie.ProverInterface+ErrorHandler handler, System.Int32 taskID) [0x006d0] in <19ca4884bb9d4ccb8c3a80682b5b183b>:0 
  at CoreLib.StratifiedInlining.CheckVC (Microsoft.Boogie.ProverInterface+ErrorHandler reporter) [0x0003e] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at CoreLib.StratifiedInlining.Fwd (System.Collections.Generic.HashSet`1[T] openCallSites, CoreLib.StratifiedInliningErrorReporter reporter, System.Boolean main, System.Int32 recBound) [0x00110] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at CoreLib.StratifiedInlining.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00645] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at VC.ConditionGeneration.VerifyImplementation (Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1[Microsoft.Boogie.Counterexample]& errors, System.String requestId) [0x00019] in <693f0436fa9c41f6a229442309a8ffe4>:0 
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Boolean needErrorTraces, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Collections.Generic.List`1[System.String]& timedOut, System.Boolean isCBA) [0x003f0] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Boolean isCBA) [0x00007] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at cba.VerificationPass.feedToBoogie (cba.CBAProgram p) [0x00070] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at cba.VerificationPass.runCBAPass (cba.CBAProgram prog) [0x0001f] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at cba.CompilerPass.runPass (Microsoft.Boogie.Program inp) [0x00012] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at ProgTransformation.TransformationPass.run (ProgTransformation.PersistentProgram inp) [0x0009c] in <5fc8c0b22e1047d2a1bef434cbda2c83>:0 
  at cba.CompilerPass.run (cba.PersistentCBAProgram inp) [0x00007] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 
  at cba.CBADriver.VerifyProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x00156] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.CBADriver.checkPath (cba.PersistentCBAProgram prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x0002a] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.CBADriver.checkPath (cba.PersistentCBAProgram pmeta, cba.VarSet trackedVars, cba.ErrorTrace& trace) [0x00001] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.Driver.checkAndRefinePathFewPasses (cba.PersistentCBAProgram counterexample, cba.RefinementState refinementState, cba.ErrorTrace& cexTrace) [0x00013] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.Driver.checkAndRefine (cba.PersistentCBAProgram prog, cba.RefinementState refinementState, System.Action`2[T1,T2] printTrace, cba.ErrorTrace& cexTrace) [0x001d4] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.Driver.run (System.String[] args) [0x00466] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 
  at cba.Driver.Main (System.String[] args) [0x00067] in <9c847b8b7e9c451fb8593bfcea859ec4>:0
zvonimir commented 4 years ago
I reported this while back to Corral developers, and here is the discussion: https://github.com/boogie-org/corral/issues/55
michael-emmi commented 4 years ago
What should we do with this?
Get Corral to say that it cannot construct a trace?
Get Corral to report potential incompleteness?
Just handle this exception in Smack and explain that we cannot construct a trace?
michael-emmi commented 4 years ago
I think this issue may be distinct from boogie-org/corral#55 because it only shows up with z3-4.8.6, and not prior versions.
smackers / smack

Insufficient details to construct counterexample path #521
