From cfbb83ff12549044fa0ed9e143ee0a54fcef24d5 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sun, 1 Apr 2012 21:39:57 -0700 Subject: partial work on non-uniform loop unrolling --- Source/Provers/SMTLib/ProverInterface.cs | 66 ++++++++++++++++++++++++++++++++ Source/VCGeneration/Check.cs | 4 ++ Source/VCGeneration/StratifiedVC.cs | 33 +++++++++++++--- 3 files changed, 98 insertions(+), 5 deletions(-) diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 6ef3778d..dd742544 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -846,6 +846,72 @@ namespace Microsoft.Boogie.SMTLib DeclCollector.Push(); } + public override Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions) { + unsatisfiedSoftAssumptions = new List(); + + Push(); + foreach (var a in hardAssumptions) { + SendThisVC("(assert " + VCExpr2String(a, 1) + ")"); + } + Check(); + Outcome outcome = GetResponse(); + if (outcome != Outcome.Invalid) { + Pop(); + return outcome; + } + + List currAssumptions = new List(); + foreach (var a in softAssumptions) { + currAssumptions.Add(VCExpr2String(a, 1)); + } + + int k = 0; + List relaxVars = new List(); + while (true) { + Push(); + AssertAxioms(); + foreach (var a in currAssumptions) { + SendThisVC("(assert " + a + ")"); + } + Check(); + outcome = GetResponse(); + Pop(); + if (outcome != Outcome.Valid) + break; + string relaxVar = "relax_" + k; + relaxVars.Add(relaxVar); + SendThisVC("(declare-fun " + relaxVar + " () Int)"); + List nextAssumptions = new List(); + for (int i = 0; i < currAssumptions.Count; i++) { + string constraint = "(= " + relaxVar + " " + i + ")"; + nextAssumptions.Add("(or " + currAssumptions[i] + " " + constraint + ")"); + } + currAssumptions = nextAssumptions; + k++; + } + + if (outcome == Outcome.Invalid) { + foreach (var relaxVar in relaxVars) { + SendThisVC("(get-value (" + relaxVar + "))"); + var resp = Process.GetProverResponse(); + if (resp == null) break; + if (!(resp.Name == "" && resp.ArgCount == 1)) break; + resp = resp.Arguments[0]; + if (!(resp.Name == "" && resp.ArgCount == 2)) break; + resp = resp.Arguments[1]; + if (resp.ArgCount != 0) + break; + int v; + if (int.TryParse(resp.Name, out v)) + unsatisfiedSoftAssumptions.Add(v); + else + break; + } + } + + Pop(); + return outcome; + } } public class SMTLibProverContext : DeclFreeProverContext diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index d74497c0..5702111d 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -829,6 +829,10 @@ namespace Microsoft.Boogie { throw new NotImplementedException(); } + public virtual Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions) { + throw new NotImplementedException(); + } + public virtual Outcome CheckOutcomeCore(ErrorHandler handler) { throw new NotImplementedException(); diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index b9b0928c..fd153e11 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1108,6 +1108,25 @@ namespace VC checker.TheoremProver.LogComment(str); } + public Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions) { + ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions); + switch (outcome) { + case ProverInterface.Outcome.Valid: + return Outcome.Correct; + case ProverInterface.Outcome.Invalid: + return Outcome.Errors; + case ProverInterface.Outcome.OutOfMemory: + return Outcome.OutOfMemory; + case ProverInterface.Outcome.TimeOut: + return Outcome.TimedOut; + case ProverInterface.Outcome.Undetermined: + return Outcome.Inconclusive; + default: + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + public Outcome CheckAssumptions(List assumptions, out List unsatCore) { if (!UseCheckAssumptions) { Outcome ret; @@ -1612,7 +1631,7 @@ namespace VC int iters = 0; - // for blocking candidates (and focussing on a counterexample) + // for blocking candidates (and focusing on a counterexample) var block = new HashSet(); // Process tasks while not done. We're done when: @@ -1717,8 +1736,7 @@ namespace VC foreach (var id in calls.currCandidates) { var rb = calls.getRecursionBound(id); - if (rb <= bound) continue; - if (rb < minRecReached) minRecReached = rb; + if (bound < rb && rb < minRecReached) minRecReached = rb; } bound = minRecReached; if (useSummary) summaryComputation.boundChanged(); @@ -2238,14 +2256,19 @@ namespace VC bool allTrue = true; bool allFalse = true; + List softAssumptions = new List(); + List unsatisfiedSoftAssumptions; assumptions = new List(); procsThatReachedRecBound.Clear(); foreach (int id in calls.currCandidates) { - if (calls.getRecursionBound(id) <= bound) + int idBound = calls.getRecursionBound(id); + if (idBound <= bound) { + if (idBound > 0) + softAssumptions.Add(calls.getFalseExpr(id)); if (block.Contains(id)) { Contract.Assert(useSummary); @@ -2276,7 +2299,7 @@ namespace VC } else { - ret = checker.CheckAssumptions(assumptions, out unsatCore); + ret = checker.CheckAssumptions(assumptions, softAssumptions, out unsatisfiedSoftAssumptions); } if (ret != Outcome.Correct && ret != Outcome.Errors) -- cgit v1.2.3 From 3968dee28a8ee0c7164fb98208a796657c3b8479 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sun, 1 Apr 2012 22:21:17 -0700 Subject: commented out SuperAwesomeMethod --- Source/VCGeneration/StratifiedVC.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 013d7900..965939fc 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1929,6 +1929,7 @@ namespace VC calleeToCallSites[callee].Remove(cs); } +#if SuperAwesomeMethod private Outcome FindUnsatCoreInMainCallees(Implementation impl, ApiChecker checker, VCExpressionGenerator Gen, PCBErrorReporter reporter, List assumptions, out HashSet unsatCore) { Debug.Assert(checker is ApiChecker); @@ -1950,7 +1951,7 @@ namespace VC } return Outcome.Correct; } - + private Outcome FindUnsatCore(Implementation impl, ApiChecker checker, VCExpressionGenerator Gen, PCBErrorReporter reporter, List assumptions, out HashSet unsatCore) { Helpers.ExtraTraceInformation("Number of assumptions = " + assumptions.Count); @@ -2174,8 +2175,7 @@ namespace VC InlineIntoMain(checker, impl, unsatCore); } } - - +#endif // A step of the stratified inlining algorithm: both under-approx and over-approx queries private Outcome stratifiedStep(int bound, VerificationState vState, HashSet block) -- cgit v1.2.3 From 7119f6238657fe4c419c6366e801ff067ffb8506 Mon Sep 17 00:00:00 2001 From: qadeer Date: Mon, 2 Apr 2012 17:21:49 -0700 Subject: deleted the option UseUnsatCoreForInlining Split ApiChecker.CheckAssumptions into two different methods, one which computes the unsatCore and one which does not Further edits to the MaxSat code --- Source/Core/CommandLineOptions.cs | 5 -- Source/Provers/SMTLib/ProverInterface.cs | 6 +- Source/VCGeneration/Check.cs | 2 +- Source/VCGeneration/StratifiedVC.cs | 97 ++++++++------------------------ 4 files changed, 28 insertions(+), 82 deletions(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 1a2d7fda..5e5a896a 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -564,7 +564,6 @@ namespace Microsoft.Boogie { public int StratifiedInliningOption = 0; public bool StratifiedInliningWithoutModels = false; // disable model generation for SI public int StratifiedInliningVerbose = 0; // verbosity level - public bool UseUnsatCoreForInlining = false; public int RecursionBound = 500; public string inferLeastForUnsat = null; public string CoverageReporterPath = null; @@ -1027,10 +1026,6 @@ namespace Microsoft.Boogie { } return true; - case "useUnsatCoreForInlining": - UseUnsatCoreForInlining = true; - return true; - case "inferLeastForUnsat": if (ps.ConfirmArgumentCount(1)) { inferLeastForUnsat = args[ps.i]; diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 5e262f87..9987e6f4 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -85,7 +85,7 @@ namespace Microsoft.Boogie.SMTLib { currentLogFile = OpenOutputFile(""); } - if (CommandLineOptions.Clo.ProcedureCopyBound > 0 || CommandLineOptions.Clo.UseUnsatCoreForInlining) + if (CommandLineOptions.Clo.ProcedureCopyBound > 0) { SendThisVC("(set-option :produce-unsat-cores true)"); this.usingUnsatCore = true; @@ -835,7 +835,7 @@ namespace Microsoft.Boogie.SMTLib DeclCollector.Push(); } - public override Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions) { + public override Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions, ErrorHandler handler) { unsatisfiedSoftAssumptions = new List(); Push(); @@ -863,7 +863,7 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(assert " + a + ")"); } Check(); - outcome = GetResponse(); + outcome = CheckOutcomeCore(handler); Pop(); if (outcome != Outcome.Valid) break; diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 1a6732c2..f9999a74 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -829,7 +829,7 @@ namespace Microsoft.Boogie { throw new NotImplementedException(); } - public virtual Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions) { + public virtual Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions, ErrorHandler handler) { throw new NotImplementedException(); } diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index b9ab40b2..12be00b2 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1039,8 +1039,6 @@ namespace VC private List numAxiomsPushed; // Api-based theorem prover private ProverInterface TheoremProver; - // Use checkAssumptions? - public static bool UseCheckAssumptions = true; private FCallHandler calls; // Underlying checker public Checker underlyingChecker; @@ -1109,7 +1107,7 @@ namespace VC } public Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions) { - ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions); + ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, reporter); switch (outcome) { case ProverInterface.Outcome.Valid: return Outcome.Correct; @@ -1127,33 +1125,24 @@ namespace VC } } - public Outcome CheckAssumptions(List assumptions, out List unsatCore) { - if (!UseCheckAssumptions) { - Outcome ret; - - unsatCore = new List(); - for (int i = 0; i < assumptions.Count; i++) - unsatCore.Add(i); - - if (assumptions.Count == 0) - { - return CheckVC(); - } + public Outcome CheckAssumptions(List assumptions) { + if (assumptions.Count == 0) { + return CheckVC(); + } - Push(); + Push(); - foreach (var a in assumptions) - { - AddAxiom(a); - } - ret = CheckVC(); + foreach (var a in assumptions) { + AddAxiom(a); + } + Outcome ret = CheckVC(); - Pop(); + Pop(); - return ret; + return ret; + } - } - + public Outcome CheckAssumptions(List assumptions, out List unsatCore) { if (assumptions.Count == 0) { unsatCore = new List(); return CheckVC(); @@ -2180,68 +2169,33 @@ namespace VC // A step of the stratified inlining algorithm: both under-approx and over-approx queries private Outcome stratifiedStep(int bound, VerificationState vState, HashSet block) { - Outcome ret; - List unsatCore; - - // No need of computing Unsat cores for stratified inlining - if (!CommandLineOptions.Clo.UseUnsatCoreForInlining && CommandLineOptions.Clo.ProverName == "SMTLIB") - ApiChecker.UseCheckAssumptions = false; - var reporter = vState.reporter as StratifiedInliningErrorReporter; var calls = vState.calls; var checker = vState.checker; reporter.underapproximationMode = true; checker.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;"); - List assumptions; - List ids; - - while (true) + List assumptions = new List(); + List ids = new List(); + foreach (int id in calls.currCandidates) { - assumptions = new List(); - ids = new List(); - foreach (int id in calls.currCandidates) - { - assumptions.Add(calls.getFalseExpr(id)); - ids.Add(id); - } - ret = checker.CheckAssumptions(assumptions, out unsatCore); - if (!CommandLineOptions.Clo.UseUnsatCoreForInlining) break; - if (ret != Outcome.Correct) break; - Debug.Assert(unsatCore.Count <= assumptions.Count); - if (unsatCore.Count == assumptions.Count) - break; - - var unsatCoreIds = new List(); - foreach (int i in unsatCore) - unsatCoreIds.Add(ids[i]); - vState.checker.LogComment(";;;;;;;;;;;; Expansion begin ;;;;;;;;;;"); - bool incrementalSearch = - CommandLineOptions.Clo.StratifiedInliningOption == 0 || - CommandLineOptions.Clo.StratifiedInliningOption == 2; - DoExpansion(incrementalSearch, unsatCoreIds, vState); - vState.calls.forcedCandidates.UnionWith(unsatCoreIds); - vState.checker.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;"); + assumptions.Add(calls.getFalseExpr(id)); + ids.Add(id); } - + Outcome ret = checker.CheckAssumptions(assumptions); checker.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;"); - if (ret == Outcome.Errors) - { - return ret; - } - if (ret != Outcome.Correct) { - // The query ran out of memory or time, that's it, - // we cannot do better. Give up! + // Either the query returned an error or it ran out of memory or time. + // In all cases, we are done. return ret; } - // If we didn't underapproximate, then we're done if (calls.currCandidates.Count == 0) { - return ret; + // If we didn't underapproximate, then we're done + return ret; } checker.LogComment(";;;;;;;;;;;; Overapprox mode begin ;;;;;;;;;;"); @@ -2271,20 +2225,17 @@ namespace VC if (block.Contains(id)) { Contract.Assert(useSummary); - //checker.AddAxiom(calls.getFalseExpr(id)); assumptions.Add(calls.getFalseExpr(id)); allTrue = false; } else { - //checker.TheoremProver.PushVCExpression(calls.getTrueExpr(id)); allFalse = false; } } else { procsThatReachedRecBound.Add(calls.getProc(id)); - //checker.AddAxiom(calls.getFalseExpr(id)); assumptions.Add(calls.getFalseExpr(id)); allTrue = false; } -- cgit v1.2.3 From 36c96118667c326eb687bb05bc1be42ce8f78509 Mon Sep 17 00:00:00 2001 From: qadeer Date: Tue, 3 Apr 2012 09:22:05 -0700 Subject: added nonUniformUnfolding option --- Source/Core/CommandLineOptions.cs | 4 +++- Source/Provers/SMTLib/ProverInterface.cs | 4 +++- Source/VCGeneration/StratifiedVC.cs | 20 ++++++++------------ 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 5e5a896a..ed80f6ac 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -565,6 +565,7 @@ namespace Microsoft.Boogie { public bool StratifiedInliningWithoutModels = false; // disable model generation for SI public int StratifiedInliningVerbose = 0; // verbosity level public int RecursionBound = 500; + public bool NonUniformUnfolding = false; public string inferLeastForUnsat = null; public string CoverageReporterPath = null; public Process coverageReporter = null; // used internally for debugging @@ -1223,7 +1224,8 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) || ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) || ps.CheckBooleanFlag("contractInfer", ref ContractInfer) || - ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) + ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) || + ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ) { // one of the boolean flags matched return true; diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 9987e6f4..5667429a 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -864,9 +864,9 @@ namespace Microsoft.Boogie.SMTLib } Check(); outcome = CheckOutcomeCore(handler); - Pop(); if (outcome != Outcome.Valid) break; + Pop(); string relaxVar = "relax_" + k; relaxVars.Add(relaxVar); SendThisVC("(declare-fun " + relaxVar + " () Int)"); @@ -882,6 +882,7 @@ namespace Microsoft.Boogie.SMTLib if (outcome == Outcome.Invalid) { foreach (var relaxVar in relaxVars) { SendThisVC("(get-value (" + relaxVar + "))"); + FlushLogFile(); var resp = Process.GetProverResponse(); if (resp == null) break; if (!(resp.Name == "" && resp.ArgCount == 1)) break; @@ -896,6 +897,7 @@ namespace Microsoft.Boogie.SMTLib else break; } + Pop(); } Pop(); diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 12be00b2..98f20d21 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1106,7 +1106,8 @@ namespace VC checker.TheoremProver.LogComment(str); } - public Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions) { + public Outcome CheckAssumptions(List hardAssumptions, List softAssumptions) { + List unsatisfiedSoftAssumptions; ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, reporter); switch (outcome) { case ProverInterface.Outcome.Valid: @@ -1613,7 +1614,7 @@ namespace VC // bool underApproxNeeded = true; // The recursion bound for stratified search - int bound = 1; + int bound = CommandLineOptions.Clo.NonUniformUnfolding ? CommandLineOptions.Clo.RecursionBound : 1; int done = 0; @@ -1720,13 +1721,7 @@ namespace VC if (block.Count == 0) { // Increment bound - var minRecReached = CommandLineOptions.Clo.RecursionBound + 1; - foreach (var id in calls.currCandidates) - { - var rb = calls.getRecursionBound(id); - if (bound < rb && rb < minRecReached) minRecReached = rb; - } - bound = minRecReached; + bound++; if (useSummary) summaryComputation.boundChanged(); if (bound > CommandLineOptions.Clo.RecursionBound) @@ -2210,7 +2205,6 @@ namespace VC bool allTrue = true; bool allFalse = true; List softAssumptions = new List(); - List unsatisfiedSoftAssumptions; assumptions = new List(); procsThatReachedRecBound.Clear(); @@ -2220,7 +2214,7 @@ namespace VC int idBound = calls.getRecursionBound(id); if (idBound <= bound) { - if (idBound > 0) + if (idBound > 1) softAssumptions.Add(calls.getFalseExpr(id)); if (block.Contains(id)) { @@ -2249,7 +2243,9 @@ namespace VC } else { - ret = checker.CheckAssumptions(assumptions, softAssumptions, out unsatisfiedSoftAssumptions); + ret = CommandLineOptions.Clo.NonUniformUnfolding + ? checker.CheckAssumptions(assumptions, softAssumptions) + : checker.CheckAssumptions(assumptions); } if (ret != Outcome.Correct && ret != Outcome.Errors) -- cgit v1.2.3 From 3ff2e42970584ad66f8b8e353ddce86dbea92baf Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 4 Apr 2012 09:34:14 -0700 Subject: small fix added regressions --- Source/Provers/SMTLib/ProverInterface.cs | 31 ++- Test/stratifiedinline/Answer | 422 +++++++++++++++++++++++++++++++ Test/stratifiedinline/bar10.bpl | 41 +++ Test/stratifiedinline/bar7.bpl | 2 +- Test/stratifiedinline/bar8.bpl | 2 +- Test/stratifiedinline/bar9.bpl | 45 ++++ Test/stratifiedinline/runtest.bat | 12 + 7 files changed, 540 insertions(+), 15 deletions(-) create mode 100644 Test/stratifiedinline/bar10.bpl create mode 100644 Test/stratifiedinline/bar9.bpl diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 5667429a..08322ebb 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -838,9 +838,20 @@ namespace Microsoft.Boogie.SMTLib public override Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions, ErrorHandler handler) { unsatisfiedSoftAssumptions = new List(); - Push(); + // First, convert both hard and soft assumptions to SMTLIB strings + List hardAssumptionStrings = new List(); foreach (var a in hardAssumptions) { - SendThisVC("(assert " + VCExpr2String(a, 1) + ")"); + hardAssumptionStrings.Add(VCExpr2String(a, 1)); + } + List currAssumptionStrings = new List(); + foreach (var a in softAssumptions) { + currAssumptionStrings.Add(VCExpr2String(a, 1)); + } + + Push(); + AssertAxioms(); + foreach (var a in hardAssumptionStrings) { + SendThisVC("(assert " + a + ")"); } Check(); Outcome outcome = GetResponse(); @@ -849,17 +860,11 @@ namespace Microsoft.Boogie.SMTLib return outcome; } - List currAssumptions = new List(); - foreach (var a in softAssumptions) { - currAssumptions.Add(VCExpr2String(a, 1)); - } - int k = 0; List relaxVars = new List(); while (true) { Push(); - AssertAxioms(); - foreach (var a in currAssumptions) { + foreach (var a in currAssumptionStrings) { SendThisVC("(assert " + a + ")"); } Check(); @@ -870,12 +875,12 @@ namespace Microsoft.Boogie.SMTLib string relaxVar = "relax_" + k; relaxVars.Add(relaxVar); SendThisVC("(declare-fun " + relaxVar + " () Int)"); - List nextAssumptions = new List(); - for (int i = 0; i < currAssumptions.Count; i++) { + List nextAssumptionStrings = new List(); + for (int i = 0; i < currAssumptionStrings.Count; i++) { string constraint = "(= " + relaxVar + " " + i + ")"; - nextAssumptions.Add("(or " + currAssumptions[i] + " " + constraint + ")"); + nextAssumptionStrings.Add("(or " + currAssumptionStrings[i] + " " + constraint + ")"); } - currAssumptions = nextAssumptions; + currAssumptionStrings = nextAssumptionStrings; k++; } diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index aee2722e..6e23c098 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -62,3 +62,425 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors ----- +----- Running regression test bar7.bpl +bar7.bpl(42,3): Error BP5001: This assertion might not hold. +Execution trace: + bar7.bpl(35,5): anon0 + bar7.bpl(37,5): anon4_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(7,3): anon2_Else + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + bar7.bpl(42,3): anon3 + +Boogie program verifier finished with 0 verified, 1 error +----- +----- Running regression test bar8.bpl +bar8.bpl(41,3): Error BP5001: This assertion might not hold. +Execution trace: + bar8.bpl(34,5): anon0 + bar8.bpl(36,5): anon4_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(7,3): anon2_Else + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + bar8.bpl(41,3): anon3 + +Boogie program verifier finished with 0 verified, 1 error +----- +----- Running regression test bar9.bpl +bar9.bpl(44,3): Error BP5001: This assertion might not hold. +Execution trace: + bar9.bpl(35,5): anon0 + bar9.bpl(41,5): anon4_Else + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(16,3): anon2_Else + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(26,3): anon2_Else + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + bar9.bpl(44,3): anon3 + +Boogie program verifier finished with 0 verified, 1 error +----- +----- Running regression test bar10.bpl +bar10.bpl(40,3): Error BP5001: This assertion might not hold. +Execution trace: + bar10.bpl(35,5): anon0 + Inlined call to procedure bar1 begins + bar10.bpl(16,3): anon0 + bar10.bpl(16,3): anon2_Else + Inlined call to procedure bar1 ends + Inlined call to procedure bar2 begins + bar10.bpl(26,3): anon0 + bar10.bpl(26,3): anon2_Else + Inlined call to procedure bar2 ends + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(7,3): anon2_Else + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + +Boogie program verifier finished with 0 verified, 1 error +----- diff --git a/Test/stratifiedinline/bar10.bpl b/Test/stratifiedinline/bar10.bpl new file mode 100644 index 00000000..8cfcfc13 --- /dev/null +++ b/Test/stratifiedinline/bar10.bpl @@ -0,0 +1,41 @@ +var i: int; +var m: int; + +procedure {:inline 1} foo() +modifies i; +{ + if (i < 20) { + i := i + 1; + call foo(); + } +} + +procedure {:inline 1} bar1(j: int) +modifies i; +{ + if (j < 2*m) + { + i := i + 1; + call bar1(j+1); + } +} + +procedure {:inline 1} bar2(j: int) +modifies i; +{ + if (j < m) { + i := i - 1; + call bar2(j+1); + } +} + +procedure main() +modifies i; +{ + i := 0; + call bar1(0); + call bar2(0); + i := 0; + call foo(); + assert i < 10; +} \ No newline at end of file diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl index 747510de..b28777bd 100644 --- a/Test/stratifiedinline/bar7.bpl +++ b/Test/stratifiedinline/bar7.bpl @@ -4,7 +4,7 @@ var m: int; procedure {:inline 1} foo() modifies i; { - if (i < 80) { + if (i < 20) { i := i + 1; call foo(); } diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl index d447e3a7..e96655f3 100644 --- a/Test/stratifiedinline/bar8.bpl +++ b/Test/stratifiedinline/bar8.bpl @@ -4,7 +4,7 @@ var m: int; procedure {:inline 1} foo() modifies i; { - if (i < 80) { + if (i < 20) { i := i + 1; call foo(); } diff --git a/Test/stratifiedinline/bar9.bpl b/Test/stratifiedinline/bar9.bpl new file mode 100644 index 00000000..12de78ad --- /dev/null +++ b/Test/stratifiedinline/bar9.bpl @@ -0,0 +1,45 @@ +var i: int; +var m: int; + +procedure {:inline 1} foo(x: int) +modifies i; +{ + if (i < x) { + i := i + 1; + call foo(x); + } +} + +procedure {:inline 1} bar1(j: int) +modifies i; +{ + if (j < 2*m) + { + i := i + 1; + call bar1(j+1); + } +} + +procedure {:inline 1} bar2(j: int) +modifies i; +{ + if (j < m) { + i := i - 1; + call bar2(j+1); + } +} + +procedure main() +modifies i; +{ + i := 0; + if (*) { + call foo(20); + i := 0; + call foo(4); + } else { + call bar1(0); + call bar2(0); + } + assert i < 10; +} \ No newline at end of file diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat index 194570d0..d731d605 100644 --- a/Test/stratifiedinline/runtest.bat +++ b/Test/stratifiedinline/runtest.bat @@ -19,4 +19,16 @@ echo ----- echo ----- Running regression test bar6.bpl %BGEXE% %* /noinfer /stratifiedInline:1 bar6.bpl echo ----- +echo ----- Running regression test bar7.bpl +%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar7.bpl +echo ----- +echo ----- Running regression test bar8.bpl +%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar8.bpl +echo ----- +echo ----- Running regression test bar9.bpl +%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar9.bpl +echo ----- +echo ----- Running regression test bar10.bpl +%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar10.bpl +echo ----- -- cgit v1.2.3 From 659491fddae2ee457100b6fa4c27afef3340621e Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 4 Apr 2012 18:40:59 -0700 Subject: Fixed bug with triply nested maps and polymorphism (reported as Item # 10218). --- Source/Core/AbsyCmd.cs | 2 +- Test/aitest9/TestIntervals.bpl | 16 ++++++++++++++++ Test/aitest9/answer | 2 +- 3 files changed, 18 insertions(+), 2 deletions(-) diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 62ebc77f..1367a08d 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1472,7 +1472,7 @@ namespace Microsoft.Boogie { NAryExpr/*!*/ res = Expr.Select(Map.AsExpr, Indexes); Contract.Assert(res != null); res.TypeParameters = this.TypeParameters; - res.Type = Map.AsExpr.Type.AsMap.Result; + res.Type = this.Type; return res; } } diff --git a/Test/aitest9/TestIntervals.bpl b/Test/aitest9/TestIntervals.bpl index b989e16c..bee73a57 100644 --- a/Test/aitest9/TestIntervals.bpl +++ b/Test/aitest9/TestIntervals.bpl @@ -22,3 +22,19 @@ procedure P() assert -3 <= c; assert c <= 0; // error (there was once an error in the Intervals which thought this assertion to be true) } + +// The following tests a triply nested array, where the innermost array is a polymorphic map. +// There was once an error in Boogie's handling of such things in the AI code. + +type ref; +type teflon; + +type Field a; +type HeapType = [Field a]a; +var Heap: HeapType; + +procedure Q(myField: Field [ref][teflon]bool, r: ref, t: teflon) + modifies Heap; +{ + Heap[myField][r][t] := true; +} diff --git a/Test/aitest9/answer b/Test/aitest9/answer index 27e18ca4..d68508af 100644 --- a/Test/aitest9/answer +++ b/Test/aitest9/answer @@ -18,4 +18,4 @@ Execution trace: TestIntervals.bpl(14,14): anon12_Then TestIntervals.bpl(17,5): anon8 -Boogie program verifier finished with 0 verified, 1 error +Boogie program verifier finished with 1 verified, 1 error -- cgit v1.2.3