diff --git a/Source/Boogie-NetCore.sln b/Source/Boogie-NetCore.sln index f40ada657..c51fd2333 100644 --- a/Source/Boogie-NetCore.sln +++ b/Source/Boogie-NetCore.sln @@ -31,8 +31,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini-NetCore", "Houdini\ EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Predication-NetCore", "Predication\Predication-NetCore.csproj", "{7A4B3721-D902-4265-94DB-CA8B0BB295B7}" EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Doomed-NetCore", "Doomed\Doomed-NetCore.csproj", "{CE190976-D727-4038-8D8A-8C5579E48CCF}" -EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine-NetCore", "ExecutionEngine\ExecutionEngine-NetCore.csproj", "{51768B2E-FFF9-49F0-96D7-022250A4BEB4}" EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency-NetCore", "Concurrency\Concurrency-NetCore.csproj", "{4AC86856-E985-4DBC-B089-20D5B9317A99}" diff --git a/Source/Boogie.sln b/Source/Boogie.sln index 85a084c22..0ba695c5b 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -36,8 +36,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "Houdini\Houdini. EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Predication", "Predication\Predication.csproj", "{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}" EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Doomed", "Doomed\Doomed.csproj", "{884386A3-58E9-40BB-A273-B24976775553}" -EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "ExecutionEngine\ExecutionEngine.csproj", "{EAA5EB79-D475-4601-A59B-825C191CD25F}" EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BVD", "BVD\BVD.csproj", "{8A05D14E-F2BF-4890-BBE0-D76B18A50797}" diff --git a/Source/BoogieDriver/BoogieDriver-NetCore.csproj b/Source/BoogieDriver/BoogieDriver-NetCore.csproj index 9414572dd..8a121f235 100644 --- a/Source/BoogieDriver/BoogieDriver-NetCore.csproj +++ b/Source/BoogieDriver/BoogieDriver-NetCore.csproj @@ -22,7 +22,6 @@ - diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index 52a3bd0d4..ef32db776 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -214,10 +214,6 @@ {B230A69C-C466-4065-B9C1-84D80E76D802} Core - - {884386A3-58E9-40BB-A273-B24976775553} - Doomed - {EAA5EB79-D475-4601-A59B-825C191CD25F} ExecutionEngine diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 4ed6044b7..6775d20ce 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -305,7 +305,7 @@ public virtual void AttributeUsage() { /// public virtual void ApplyDefaultOptions() { } - + /// /// Parses the command-line arguments "args" into the global flag variables. Returns true /// if there were no errors. @@ -413,14 +413,12 @@ void ObjectInvariant2() { public string PrintFile = null; public int PrintUnstructured = 0; public bool UseBaseNameForFileName = false; - public int DoomStrategy = -1; - public bool DoomRestartTP = false; public bool PrintDesugarings = false; public bool PrintLambdaLifting = false; public bool FreeVarLambdaLifting = false; public string ProverLogFilePath = null; public bool ProverLogFileAppend = false; - + public bool PrintInstrumented = false; public bool InstrumentWithAsserts = false; public string ProverPreamble = null; @@ -564,7 +562,6 @@ public enum OwnershipModelOption { public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present public bool UseArrayTheory = false; public bool WeakArrayTheory = false; - public bool UseLabels = true; public bool RunDiagnosticsOnTimeout = false; public bool TraceDiagnosticsOnTimeout = false; public int TimeLimitPerAssertionInPercent = 10; @@ -599,20 +596,6 @@ public int StepsBeforeWidening public int TrustLayersUpto = -1; public int TrustLayersDownto = int.MaxValue; - public enum VCVariety { - Structured, - Block, - Local, - BlockNested, - BlockReach, - BlockNestedReach, - Dag, - DagIterative, - Doomed, - Unspecified - } - public VCVariety vcVariety = VCVariety.Unspecified; // will not be Unspecified after command line has been parsed - public bool RemoveEmptyBlocks = true; public bool CoalesceBlocks = true; public bool PruneInfeasibleEdges = true; @@ -737,7 +720,7 @@ public enum Inlining { public int StratifiedInliningVerbose = 0; // verbosity level public int RecursionBound = 500; public bool NonUniformUnfolding = false; - public int StackDepthBound = 0; + public int StackDepthBound = 0; public string inferLeastForUnsat = null; // Inference mode for fixed point engine @@ -749,11 +732,11 @@ public enum FixedPointInferenceMode { Call }; public FixedPointInferenceMode FixedPointMode = FixedPointInferenceMode.Procedure; - + public string PrintFixedPoint = null; public string PrintConjectures = null; - + public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically) public enum TypeEncoding { @@ -789,7 +772,7 @@ public IEnumerable ProcsToCheck { } private List procsToCheck = null; // null means "no restriction" - + [ContractInvariantMethod] void ObjectInvariant5() { Contract.Invariant(cce.NonNullElements(this.procsToCheck, true)); @@ -890,7 +873,7 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command int val = 1; if (ps.GetNumericArgument(ref val, 2)) { PrettyPrint = val == 1; - } + } return true; case "CivlDesugaredFile": @@ -919,13 +902,13 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command } return true; - case "proverPreamble": + case "proverPreamble": if (ps.ConfirmArgumentCount(1)) { ProverPreamble = args[ps.i]; } return true; - + case "logPrefix": if (ps.ConfirmArgumentCount(1)) { string s = cce.NonNull(args[ps.i]); @@ -1152,47 +1135,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command } return true; } - case "vc": - if (ps.ConfirmArgumentCount(1)) { - switch (args[ps.i]) { - case "s": - case "structured": - vcVariety = VCVariety.Structured; - break; - case "b": - case "block": - vcVariety = VCVariety.Block; - break; - case "l": - case "local": - vcVariety = VCVariety.Local; - break; - case "n": - case "nested": - vcVariety = VCVariety.BlockNested; - break; - case "m": - vcVariety = VCVariety.BlockNestedReach; - break; - case "r": - vcVariety = VCVariety.BlockReach; - break; - case "d": - case "dag": - vcVariety = VCVariety.Dag; - break; - case "i": - vcVariety = VCVariety.DagIterative; - break; - case "doomed": - vcVariety = VCVariety.Doomed; - break; - default: - ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); - break; - } - } - return true; case "proverDll": if (ps.ConfirmArgumentCount(1)) { @@ -1207,28 +1149,18 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command ProverOptions = ProverOptions.Concat1(cce.NonNull(args[ps.i])); } return true; - + case "proverHelp": if (ps.ConfirmArgumentCount(0)) { ProverHelpRequested = true; } return true; - case "DoomStrategy": - ps.GetNumericArgument(ref DoomStrategy); - return true; - - case "DoomRestartTP": - if (ps.ConfirmArgumentCount(0)) { - DoomRestartTP = true; - } - return true; - case "extractLoops": if (ps.ConfirmArgumentCount(0)) { ExtractLoops = true; } - return true; + return true; case "deterministicExtractLoops": if (ps.ConfirmArgumentCount(0)) { @@ -1502,7 +1434,7 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command case "traceCaching": ps.GetNumericArgument(ref TraceCaching, 4); return true; - + case "platform": if (ps.ConfirmArgumentCount(1)) { StringCollection platformOptions = this.ParseNamedArgumentList(args[ps.i]); @@ -1563,9 +1495,8 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) || ps.CheckBooleanFlag("monomorphize", ref Monomorphize) || ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) || - ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) || + ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) || ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) || - ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) || ps.CheckBooleanFlag("runDiagnosticsOnTimeout", ref RunDiagnosticsOnTimeout) || ps.CheckBooleanFlag("traceDiagnosticsOnTimeout", ref TraceDiagnosticsOnTimeout) || ps.CheckBooleanFlag("boolControlVC", ref SIBoolControlVC, true) || @@ -1597,7 +1528,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command public override void ApplyDefaultOptions() { Contract.Ensures(TheProverFactory != null); - Contract.Ensures(vcVariety != VCVariety.Unspecified); base.ApplyDefaultOptions(); @@ -1617,17 +1547,8 @@ public override void ApplyDefaultOptions() { TheProverFactory = ProverFactory.Load(ProverDllName); } - var proverOpts = TheProverFactory.BlankProverOptions(); - proverOpts.Parse(ProverOptions); if (ProverHelpRequested) { - Console.WriteLine(proverOpts.Help); - } - if (!TheProverFactory.SupportsLabels(proverOpts)) { - UseLabels = false; - } - - if (vcVariety == VCVariety.Unspecified) { - vcVariety = TheProverFactory.DefaultVCVariety; + Console.WriteLine(TheProverFactory.BlankProverOptions().Help); } if (UseArrayTheory) { @@ -1853,7 +1774,7 @@ identifies variables expressions into templates with holes. By default, holes are maximally large subexpressions that do not contain bound variables. This option performs a form of lambda - lifting in which holes are the lambda's free variables. + lifting in which holes are the lambda's free variables. /overlookTypeErrors : skip any implementation with resolution or type checking errors @@ -1961,7 +1882,7 @@ verify several program snapshots (named .v0.bpl 3 - use the more advanced caching and report errors according to the new source locations for errors and their related locations (but not /errorTrace and CaptureState - locations) + locations) /traceCaching: 0 (default) - none 1 - for testing @@ -1975,12 +1896,6 @@ verify each input program separately /coalesceBlocks: 0 = do not coalesce blocks 1 = coalesce blocks (default) - /vc: n = nested block, - m = nested block reach, - b = flat block, r = flat block reach, - s = structured, l = local, - d = dag (default) - doomed = doomed /traceverify print debug output during verification condition generation /subsumption: apply subsumption to asserted conditions: @@ -2025,7 +1940,7 @@ how to encode types when sending VC to theorem prover p = predicates (default) a = arguments m = monomorphic - /monomorphize + /monomorphize Do not abstract map types in the encoding (this is an experimental feature that will not do the right thing if the program uses polymorphism) @@ -2065,7 +1980,7 @@ assertion in the keep going mode. Defaults to 30s. /vcsPathCostMult: /vcsAssumeMult: The cost of a block is - ( + *) * + ( + *) * (1.0 + *) defaults to 1.0, defaults to 0.01. The cost of a single assertion or assumption is diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs index 210fb24e7..1a74ef04c 100644 --- a/Source/Core/VCExp.cs +++ b/Source/Core/VCExp.cs @@ -254,17 +254,6 @@ public virtual bool SupportsDags { } } - public virtual CommandLineOptions.VCVariety DefaultVCVariety { - get { - Contract.Ensures(Contract.Result() != CommandLineOptions.VCVariety.Unspecified); - return CommandLineOptions.VCVariety.DagIterative; - } - } - - public virtual bool SupportsLabels(ProverOptions options) { - return true; - } - public virtual void Close() { } diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs deleted file mode 100644 index c1d6736fd..000000000 --- a/Source/Doomed/DoomCheck.cs +++ /dev/null @@ -1,407 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- - -using System; -using System.Collections; -using System.Collections.Generic; -using System.Diagnostics; -using System.Threading; -using System.IO; -using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; -using Microsoft.Boogie.VCExprAST; - -namespace VC -{ - internal class Evc { - - public DoomErrorHandler ErrorHandler { - set { - m_ErrorHandler = value; - } - } - - [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(m_Checker!=null); -} - - private Checker m_Checker; - private DoomErrorHandler m_ErrorHandler; - - [NotDelayed] - public Evc(Checker check) { - Contract.Requires(check != null); - m_Checker = check; - - } - - public void Initialize(VCExpr evc) { - Contract.Requires(evc != null); - m_Checker.PushVCExpr(evc); - } - - - public bool CheckReachvar(List lv,Dictionary finalreachvars, - int k, int l, bool usenew , out ProverInterface.Outcome outcome) { - Contract.Requires(lv != null); - - VCExpr vc = VCExpressionGenerator.False; - if (usenew ) - { - foreach (Variable v in lv) - { - - vc = m_Checker.VCExprGen.Or( - m_Checker.VCExprGen.Neq( - m_Checker.VCExprGen.Integer(BigNum.ZERO), - m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v)), - vc); - } - //Console.WriteLine("TPQuery k={0}, l={1}, |Sp|={2}", k, l, finalreachvars.Count); - - VCExpr vc21 = m_Checker.VCExprGen.Integer(BigNum.ZERO); // Ask: is the necessary or can we use the same instance term in two inequalities? - VCExpr vc22 = m_Checker.VCExprGen.Integer(BigNum.ZERO); - - foreach (KeyValuePair kvp in finalreachvars) - { - - vc21 = m_Checker.VCExprGen.Add(vc21, m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key)); - vc22 = m_Checker.VCExprGen.Add(vc22, m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key)); - } - - VCExpr post = m_Checker.VCExprGen.Gt(m_Checker.VCExprGen.Integer(BigNum.FromInt(l)), vc21); - - if (k != -1) - { - post = m_Checker.VCExprGen.Or( - post, m_Checker.VCExprGen.Gt(vc22, m_Checker.VCExprGen.Integer(BigNum.FromInt(k))) - ); - } - vc = (m_Checker.VCExprGen.Or(vc, (post) )); - - } - else - { - - foreach (Variable v in lv) - { - - vc = m_Checker.VCExprGen.Or( - m_Checker.VCExprGen.Eq( - m_Checker.VCExprGen.Integer(BigNum.ONE), - m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v)), - vc); - } - Contract.Assert(vc != null); - - // Add the desired outcome of the reachability variables - foreach (KeyValuePair kvp in finalreachvars) - { - vc = m_Checker.VCExprGen.Or( - m_Checker.VCExprGen.Neq( - m_Checker.VCExprGen.Integer(BigNum.FromInt(kvp.Value)), - m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key)), - vc); - } - - } - - // Todo: Check if vc is trivial true or false - outcome = ProverInterface.Outcome.Undetermined; - Contract.Assert(m_ErrorHandler != null); - try - { - m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler); - m_Checker.ProverTask.Wait(); - outcome = m_Checker.ReadOutcome(); - } - catch (UnexpectedProverOutputException e) - { - if (CommandLineOptions.Clo.TraceVerify) - { - Console.WriteLine("Prover is unable to check {0}! Reason:", lv[0].Name); - Console.WriteLine(e.ToString()); - } - return false; - } - finally - { - m_Checker.GoBackToIdle(); - } - return true; - } - } - - internal class DoomCheck { - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(Label2Absy!=null); - Contract.Invariant(m_Check != null); - Contract.Invariant(m_Evc != null); - Contract.Invariant(m_Order != null); - } - - #region Attributes - public Dictionary Label2Absy; - public DoomErrorHandler ErrorHandler { - set { - m_ErrHandler = value; - m_Evc.ErrorHandler = value; - } - - get { - return m_ErrHandler; - } - } - - private DoomErrorHandler m_ErrHandler; - private Checker m_Check; - private DoomDetectionStrategy m_Order; - private Evc m_Evc; - #endregion - - public void __DEBUG_PrintStatistics() - { - Console.WriteLine("Checked/Total: Bl {0} / {1} EQ {2} / {3} {4} Tr {5} {6} / {7}", m_Order.__DEBUG_BlocksChecked, m_Order.__DEBUG_BlocksTotal, m_Order.__DEBUG_EQCChecked, m_Order.__DEBUG_EQCTotal, m_Order.__DEBUG_EQCLeaf, m_Order.__DEBUG_TracesChecked, m_Order.__DEBUG_InfeasibleTraces, m_Order.__DEBUG_TracesTotal); - } - - [NotDelayed] - public DoomCheck (Implementation passive_impl, Block unifiedExit, Checker check, List uncheckable, out int assertionCount) { - Contract.Requires(passive_impl != null); - Contract.Requires(check != null); - Contract.Requires(uncheckable != null); - m_Check = check; - - int replaceThisByCmdLineOption = CommandLineOptions.Clo.DoomStrategy ; - if (CommandLineOptions.Clo.DoomStrategy!=-1) Console.Write("Running experiments using {0} /", replaceThisByCmdLineOption); - switch (replaceThisByCmdLineOption) - { - default: - { - if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("Path Cover specialK Strategy"); - m_Order = new PathCoverStrategyK(passive_impl, unifiedExit, uncheckable); - break; - } - case 1: - { - if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("Path Cover L Strategy"); - m_Order = new PathCoverStrategy(passive_impl, unifiedExit, uncheckable); - break; - } - case 2: - { - if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("hasse strategy"); - m_Order = new HierachyStrategy(passive_impl, unifiedExit, uncheckable); - - break; - } - case 3: - { - if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("hasse+ce strategy"); - m_Order = new HierachyCEStrategy(passive_impl, unifiedExit, uncheckable); - break; - } - case 4: - { - if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("no strategy"); - m_Order = new NoStrategy(passive_impl, unifiedExit, uncheckable); - break; - } - - } - - Label2Absy = new Dictionary(); // This is only a dummy - m_Evc = new Evc(check); - Dictionary l2a = null; - VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount); - Contract.Assert(vce != null); - Contract.Assert( l2a!=null); - Label2Absy = l2a; - - m_Evc.Initialize(vce); - } - - - public void RespawnChecker(Implementation passive_impl, Checker check) - { - Contract.Requires(check != null); - m_Check = check; - Label2Absy = new Dictionary(); // This is only a dummy - m_Evc = new Evc(check); - Dictionary l2a = null; - int assertionCount; // compute and then ignore - VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount); - Contract.Assert(vce != null); - Contract.Assert(l2a != null); - Label2Absy = l2a; - - m_Evc.Initialize(vce); - } - - /* - Set b to the next block that needs to be checked. - - Returns false and set b to null if all blocks are checked. - - Has to be alternated with CheckLabel; might crash otherwise - */ - public bool GetNextBlock(out List lb) - { - return m_Order.GetNextBlock(out lb); - } - - public Stopwatch DEBUG_ProverTime = new Stopwatch(); - - /* - Checking a label means to ask the prover if |= ( rvar=false -> vc ) holds. - - outcome is set to Outcome.Invalid if the Block denoted by reachvar is doomed. - - returns false if the theorem prover throws an exception, otherwise true. - */ - public bool CheckLabel(List lv,Dictionary finalreachvars, out ProverInterface.Outcome outcome) { - Contract.Requires(lv != null); - outcome = ProverInterface.Outcome.Undetermined; - DEBUG_ProverTime.Reset(); - DEBUG_ProverTime.Start(); - if (m_Evc.CheckReachvar(lv,finalreachvars,m_Order.MaxBlocks,m_Order.MinBlocks,m_Order.HACK_NewCheck, out outcome) ) { - DEBUG_ProverTime.Stop(); - if (!m_Order.SetCurrentResult(lv, outcome, m_ErrHandler)) { - outcome = ProverInterface.Outcome.Undetermined; - } - return true; - } else { - DEBUG_ProverTime.Stop(); - Console.WriteLine(outcome); - m_Order.SetCurrentResult(lv, ProverInterface.Outcome.Undetermined, m_ErrHandler); - return false; - } - } - - public List!>!*/>> DoomedSequences { - get { - Contract.Ensures(Contract.ForAll(Contract.Result>>(), i=> cce.NonNullElements(i))); - - return m_Order.DetectedBlock; - } - } - - - #region Error Verification Condition Generation - /* - #region _TESTING_NEW_STUFF_ - CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Block; - //VCExpr wp = Wlp.Block(block, SuccCorrect, context); // Computes wp.S.true - - CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Doomed; - #endregion - - */ - - VCExpr GenerateEVC(Implementation impl, out Dictionary label2absy, Checker ch, out int assertionCount) { - Contract.Requires(impl != null); - Contract.Requires(ch != null); - Contract.Ensures(Contract.Result() != null); - - TypecheckingContext tc = new TypecheckingContext(null); - impl.Typecheck(tc); - label2absy = new Dictionary(); - VCExpr vc; - switch (CommandLineOptions.Clo.vcVariety) { - case CommandLineOptions.VCVariety.Doomed: - vc = LetVC(cce.NonNull(impl.Blocks[0]), label2absy, ch.TheoremProver.Context, out assertionCount); - break; - - default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected enumeration value - } - return vc; - } - - public VCExpr LetVC(Block startBlock, - Dictionary label2absy, - ProverContext proverCtxt, - out int assertionCount) - { - Contract.Requires(startBlock != null); - Contract.Requires(label2absy != null); - Contract.Requires(proverCtxt != null); - Contract.Ensures(Contract.Result() != null); - - Hashtable/**/ blockVariables = new Hashtable/**/(); - List bindings = new List(); - VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt, out assertionCount); - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { - return proverCtxt.ExprGen.Let(bindings, proverCtxt.ExprGen.Not(startCorrect) ); - } else { - return proverCtxt.ExprGen.Let(bindings, startCorrect ); - } - } - - VCExpr LetVC(Block block, - Dictionary label2absy, - Hashtable/**/ blockVariables, - List bindings, - ProverContext proverCtxt, - out int assertionCount) - { - Contract.Requires(label2absy != null); - Contract.Requires(blockVariables != null); - Contract.Requires(proverCtxt != null); - Contract.Requires(cce.NonNullElements(bindings)); - Contract.Ensures(Contract.Result() != null); - - assertionCount = 0; - VCExpressionGenerator gen = proverCtxt.ExprGen; - Contract.Assert(gen != null); - VCExprVar v = (VCExprVar)blockVariables[block]; - if (v == null) { - /* - * For block A (= block), generate: - * LET_binding A_correct = wp(A_body, (/\ S \in Successors(A) :: S_correct)) - * with the side effect of adding the let bindings to "bindings" for any - * successor not yet visited. - */ - VCExpr SuccCorrect; - GotoCmd gotocmd = block.TransferCmd as GotoCmd; - if (gotocmd == null) { - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { - SuccCorrect = VCExpressionGenerator.False; - } else { - SuccCorrect = VCExpressionGenerator.True; - } - } else { - Contract.Assert( gotocmd.labelTargets != null); - List SuccCorrectVars = new List(gotocmd.labelTargets.Count); - foreach (Block successor in gotocmd.labelTargets) { - Contract.Assert(successor != null); - int ac; - VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt, out ac); - assertionCount += ac; - SuccCorrectVars.Add(s); - } - SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars); - } - - VCContext context = new VCContext(label2absy, proverCtxt); - // m_Context = context; - - VCExpr vc = Wlp.Block(block, SuccCorrect, context); - assertionCount += context.AssertionCount; - v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool); - - bindings.Add(gen.LetBinding(v, vc)); - blockVariables.Add(block, v); - } - return v; - } - - - #endregion - - } - -} diff --git a/Source/Doomed/DoomErrorHandler.cs b/Source/Doomed/DoomErrorHandler.cs deleted file mode 100644 index ce14ff73f..000000000 --- a/Source/Doomed/DoomErrorHandler.cs +++ /dev/null @@ -1,86 +0,0 @@ -using System; -using System.Collections; -using System.Collections.Generic; -using System.Diagnostics; -using System.Threading; -using System.IO; -using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; -using Microsoft.Boogie.VCExprAST; - -namespace VC -{ - internal class DoomErrorHandler : ProverInterface.ErrorHandler - { - - protected Dictionary label2Absy; - protected VerifierCallback callback; - private List m_CurrentTrace = new List(); - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(label2Absy != null); - Contract.Invariant(callback != null); - Contract.Invariant(cce.NonNullElements(m_CurrentTrace)); - } - - - public DoomErrorHandler(Dictionary label2Absy, VerifierCallback callback) - { - Contract.Requires(label2Absy != null); - Contract.Requires(callback != null); - this.label2Absy = label2Absy; - this.callback = callback; - } - - public override Absy Label2Absy(string label) - { - //Contract.Requires(label != null); - Contract.Ensures(Contract.Result() != null); - - int id = int.Parse(label); - return cce.NonNull((Absy)label2Absy[id]); - } - - public override void OnProverWarning(string msg) - { - //Contract.Requires(msg != null); - this.callback.OnWarning(msg); - } - - - public List/*!>!*/ TraceNodes - { - get - { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - - return m_CurrentTrace; - } - } - - public override void OnModel(IList/*!>!*/ labels, Model model, ProverInterface.Outcome proverOutcome) - { - // TODO: it would be better to check which reachability variables are actually set to one! - List traceNodes = new List(); - List assertNodes = new List(); - foreach (string s in labels) - { - Contract.Assert(s != null); - Absy node = Label2Absy(s); - if (node is Block) - { - Block b = (Block)node; - traceNodes.Add(b); - //Console.Write("{0}, ", b.Label); - } - } - m_CurrentTrace.AddRange(traceNodes); - } - - } - -} \ No newline at end of file diff --git a/Source/Doomed/Doomed-NetCore.csproj b/Source/Doomed/Doomed-NetCore.csproj deleted file mode 100644 index b1366ab7f..000000000 --- a/Source/Doomed/Doomed-NetCore.csproj +++ /dev/null @@ -1,27 +0,0 @@ - - - - Library - BoogieDoomed - netcoreapp3.1 - - - - - - - - - - - - - - - - runtime; build; native; contentfiles; analyzers - all - - - - diff --git a/Source/Doomed/Doomed.csproj b/Source/Doomed/Doomed.csproj deleted file mode 100644 index eefe8e069..000000000 --- a/Source/Doomed/Doomed.csproj +++ /dev/null @@ -1,186 +0,0 @@ - - - - - Debug - AnyCPU - {884386A3-58E9-40BB-A273-B24976775553} - Library - Properties - Doomed - BoogieDoomed - v4.5 - 512 - - 12.0.0 - 2.0 - 0 - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - False - False - True - False - False - False - True - True - True - True - True - True - True - True - False - True - False - True - False - False - False - False - True - False - True - True - True - False - False - - - - - - - - True - False - False - True - Full - DoNotBuild - 0 - false - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - False - False - True - False - False - False - True - True - False - False - False - True - True - False - False - False - True - False - True - True - False - False - - - - - - - - True - False - Full - DoNotBuild - 0 - false - - - true - - - ..\InterimKey.snk - - - - - - - - - - - - - - - - - - - version.cs - - - - - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} - Basetypes - - - {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} - CodeContractsExtender - - - {B230A69C-C466-4065-B9C1-84D80E76D802} - Core - - - {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} - Graph - - - {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} - Model - - - {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} - ParserHelper - - - {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} - VCExpr - - - {E1F10180-C7B9-4147-B51F-FA1B701966DC} - VCGeneration - - - - - - - - diff --git a/Source/Doomed/DoomedLoopUnrolling.cs b/Source/Doomed/DoomedLoopUnrolling.cs deleted file mode 100644 index 0905deedc..000000000 --- a/Source/Doomed/DoomedLoopUnrolling.cs +++ /dev/null @@ -1,650 +0,0 @@ -using System; -using System.Collections; -using System.Collections.Generic; -using System.Diagnostics; -using System.Threading; -using System.IO; -using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; -using Microsoft.Boogie.VCExprAST; - -namespace VC -{ - #region Loop handeling for doomed code detection - - #region Loop Remover - internal class LoopRemover - { - GraphAnalyzer m_GraphAnalyzer; - - public LoopRemover(GraphAnalyzer ga) - { - m_GraphAnalyzer = ga; - } - - private void m_RemoveBackEdge(Loop l) - { - // first remove the backedges of the nested loops - foreach (Loop c in l.NestedLoops) m_RemoveBackEdge(c); - //Debugger.Break(); - GraphNode loopSkip = null; - foreach (GraphNode gn in l.Cutpoint.Suc) - { - if (l.LoopExitNodes.Contains(gn)) - { - loopSkip = gn; break; - } - } - if (loopSkip == null) - { // We didn't find a loop exit node. There must be a bug - Debugger.Break(); - } - foreach (GraphNode gn in l.Cutpoint.LoopingPred) - { - List newsuc = new List(); - foreach (GraphNode s in gn.Suc) - { - if (s == l.Cutpoint) newsuc.Add(loopSkip); - else newsuc.Add(s); - } - gn.Suc = newsuc; - } - } - - private void m_AbstractLoop(Loop l) - { - foreach (Loop c in l.NestedLoops) m_AbstractLoop(c); - m_HavocLoopBody(l); - m_RemoveBackEdge(l); - } - - public void AbstractLoopUnrolling() - { - foreach (Loop l in m_GraphAnalyzer.Graphloops) - { - m_MarkLoopExitUncheckable(l); - m_AbstractLoopUnrolling(l,null, "",true); - } - } - - private void m_HavocLoopBody(Loop l) - { - List loopblocks = new List(); - foreach (GraphNode g in l.LoopNodes) loopblocks.Add(g.Label); - HavocCmd hcmd = m_ComputHavocCmd(loopblocks, l.Cutpoint.Label.tok); - - //Add Havoc before and after the loop body - foreach (GraphNode g in l.Cutpoint.Suc) // before - { - if (l.LoopNodes.Contains(g)) m_AddHavocCmdToFront(g.Label, hcmd); - } - foreach (GraphNode g in l.Cutpoint.Pre) // and after - { - if (l.LoopNodes.Contains(g)) m_AddHavocCmdToFront(g.Label, hcmd); - } - } - - private void m_AddHavocCmdToFront(Block b, HavocCmd hcmd) - { - List cs = new List(); - cs.Add(hcmd); cs.AddRange(b.Cmds); - b.Cmds = cs; - } - - private HavocCmd m_ComputHavocCmd(List bl, IToken tok) - { - Contract.Requires(bl != null); - Contract.Requires(tok != null); - Contract.Ensures(Contract.Result() != null); - - List varsToHavoc = new List(); - foreach (Block b in bl) - { - Contract.Assert(b != null); - foreach (Cmd c in b.Cmds) - { - Contract.Assert(c != null); - c.AddAssignedVariables(varsToHavoc); - } - } - List havocExprs = new List(); - foreach (Variable v in varsToHavoc) - { - Contract.Assert(v != null); - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - if (!havocExprs.Contains(ie)) - havocExprs.Add(ie); - } - // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct - // the source location for this later on - return new HavocCmd(tok, havocExprs); - } - - private void m_AbstractLoopUnrolling(Loop l, Loop parent, string prefix, bool unfold) - { - //Debugger.Break(); - if (unfold) - { - - Loop first = new Loop(l, m_GraphAnalyzer,prefix+"FI_"); - Loop last = new Loop(l, m_GraphAnalyzer,prefix+"LA_"); - Loop abs = new Loop(l, m_GraphAnalyzer, prefix + "AB_"); - foreach (Loop c in first.NestedLoops) m_AbstractLoopUnrolling(c, first, prefix + "FI_", false); - foreach (Loop c in last.NestedLoops) m_AbstractLoopUnrolling(c, last, prefix + "LA_", false); - foreach (Loop c in abs.NestedLoops) m_AbstractLoopUnrolling(c, abs, prefix + "AB_", true); - - //Debugger.Break(); - - if (parent != null) - { - foreach (GraphNode gn in l.LoopNodes) - { - if (parent.LoopNodes.Contains(gn)) parent.LoopNodes.Remove(gn); - } - foreach (GraphNode gn in abs.LoopNodes) - { - if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn); - } - foreach (GraphNode gn in first.LoopNodes) - { - if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn); - } - foreach (GraphNode gn in last.LoopNodes) - { - if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn); - } - } - - m_HavocLoopBody(abs); - List backupPre = new List(); - backupPre.AddRange(l.Cutpoint.Pre); - foreach (GraphNode pre in backupPre) - { - if (!l.Cutpoint.LoopingPred.Contains(pre)) - { - pre.RemoveEdgeTo(l.Cutpoint); - pre.RemoveEdgeTo(abs.Cutpoint); - pre.AddEdgeTo(first.Cutpoint); - } - } - - m_RemoveRegularLoopExit(last); - m_RemoveRegularLoopExit(abs); - - m_ReplaceBackEdge(first, abs.Cutpoint); - m_ReplaceBackEdge(abs, last.Cutpoint); - foreach (GraphNode gn in first.Cutpoint.Suc) - { - if (!first.LoopNodes.Contains(gn)) - { - m_ReplaceBackEdge(last, gn); - break; - } - } - - // Remove all remaining connections to the original loop - foreach (GraphNode gn in l.LoopExitNodes) - { - List tmp = new List(); - tmp.AddRange(gn.Pre); - foreach (GraphNode g in tmp) - { - if (l.LoopNodes.Contains(g)) - { - //Debugger.Break(); - g.RemoveEdgeTo(gn); - } - } - } - foreach (GraphNode gn in l.LoopNodes) - { - m_GraphAnalyzer.DeleteGraphNode(gn); - } - foreach (GraphNode gn in first.LoopNodes) - { - if (gn != first.Cutpoint && !m_GraphAnalyzer.UncheckableNodes.Contains(gn) ) - m_GraphAnalyzer.UncheckableNodes.Add(gn); - } - foreach (GraphNode gn in last.LoopNodes) - { - if (gn != last.Cutpoint && !m_GraphAnalyzer.UncheckableNodes.Contains(gn)) - m_GraphAnalyzer.UncheckableNodes.Add(gn); - } - MakeLoopExitUncheckable(last.LoopExitNodes); - } - else - { - foreach (Loop c in l.NestedLoops) m_AbstractLoopUnrolling(c, l, prefix, false); - m_AbstractLoop(l); - //MakeLoopExitUncheckable(l.LoopExitNodes); - } - } - - // the loop exit has to be marked uncheckable because otherwise - // while(true) would report unreachable code. - private void m_MarkLoopExitUncheckable(Loop l) - { - - foreach (GraphNode g in l.Cutpoint.Suc) - { - if (!l.LoopNodes.Contains(g)) - { - foreach (GraphNode g_ in m_MarkLoopExitUncheckable(g, l)) - { - if (!m_GraphAnalyzer.UncheckableNodes.Contains(g_)) - m_GraphAnalyzer.UncheckableNodes.Add(g_); - } - } - } - } - - private List m_MarkLoopExitUncheckable(GraphNode g, Loop l) - { - List ret = new List(); - - if (g.Pre.Count > 1) return ret; - ret.Add(g); - foreach (GraphNode gn in g.Suc) - { - ret.AddRange(m_MarkLoopExitUncheckable(gn, l)); - } - - return ret; - } - - // to avoid problems with unreachable code after while(true) {}, try to make the loopexit nodes uncheckable. - private void MakeLoopExitUncheckable(List le) - { - foreach (GraphNode gn in le) - { - if (gn.Suc.Count==1) m_GraphAnalyzer.UncheckableNodes.Add(gn); - } - } - - private void m_RemoveRegularLoopExit(Loop l) - { - List lg = new List(); - lg.AddRange( l.Cutpoint.Suc ); - foreach (GraphNode gn in lg) - { - if (l.LoopExitNodes.Contains(gn)) - { - l.Cutpoint.RemoveEdgeTo(gn); - l.LoopExitNodes.Remove(gn); - } - } - } - - private void m_ReplaceBackEdge(Loop l, GraphNode loopSkip) - { - - foreach (GraphNode gn in l.Cutpoint.LoopingPred) - { - List newsuc = new List(); - foreach (GraphNode s in gn.Suc) - { - if (s == l.Cutpoint) newsuc.Add(loopSkip); - else newsuc.Add(s); - } - gn.Suc = newsuc; - } - } - - - } - #endregion - - #region Graph Analyzer - internal class GraphAnalyzer - { - public List UncheckableNodes = new List(); - - public Dictionary GraphMap = new Dictionary(); - - public List Graphloops = null; - - public GraphAnalyzer(List blocks) - { - //ExitBlock = dedicatedExitBlock; - if (blocks.Count < 1) return; - foreach (Block b in blocks) GraphMap[b] = new GraphNode(b); - foreach (Block b in blocks) - { - foreach (Block pre in b.Predecessors) GraphMap[b].Pre.Add(GraphMap[pre]); - GotoCmd gc = b.TransferCmd as GotoCmd; - if (gc != null) - { - foreach (Block suc in gc.labelTargets) GraphMap[b].Suc.Add(GraphMap[suc]); - } - } - - - m_DetectCutPoints(GraphMap[blocks[0]]); - - //m_DetectCutPoints(GraphMap[blocks[0]], null, new List()); - Graphloops = m_CollectLoops(GraphMap[blocks[0]], null); - - } - - public List ToImplementation(out List uncheckables) - { - List blocks = new List(); - uncheckables = new List(); - - foreach (KeyValuePair kvp in GraphMap) - { - Block b = kvp.Key; - if (UncheckableNodes.Contains(GraphMap[b])) uncheckables.Add(b); - blocks.Add(b); - b.Predecessors = new List(); - foreach (GraphNode p in kvp.Value.Pre) b.Predecessors.Add(p.Label); - if (kvp.Value.Suc.Count > 0) - { - List bs = new List(); - foreach (GraphNode s in kvp.Value.Suc) bs.Add(s.Label); - b.TransferCmd = new GotoCmd(b.tok, bs); - } - else - { - b.TransferCmd = new ReturnCmd(b.tok); - } - } - - return blocks; - } - - public GraphNode CloneGraphNode(GraphNode gn, string prefix) - { - List cmds = new List(gn.Label.Cmds); - - Block b = new Block(gn.Label.tok, prefix+gn.Label.Label, cmds, gn.Label.TransferCmd); - GraphNode clone = new GraphNode(b); - clone.IsCutpoint = gn.IsCutpoint; - clone.Suc.AddRange(gn.Suc); - clone.Pre.AddRange(gn.Pre); - clone.LoopingPred.AddRange(gn.LoopingPred); - GraphMap[b] = clone; - //if (gn.Label == ExitBlock) ExitBlock = b; - return clone; - } - - public void DeleteGraphNode(GraphNode gn) - { - List affected = new List(); - - foreach (KeyValuePair kvp in GraphMap) - { - if (kvp.Value == gn && !affected.Contains(kvp.Key)) affected.Add(kvp.Key); - } - foreach (Block b in affected) - { - GraphMap.Remove(b); - } - } -/* - private void m_DetectCutPoints(GraphNode gn, GraphNode pred, List visited ) - { - if (visited.Contains(gn) ) - { - if (pred != null && !gn.LoopingPred.Contains(pred)) gn.LoopingPred.Add(pred); - gn.IsCutpoint = true; - Console.WriteLine("Normal RootNode {0}", gn.Label.Label); - return; - } - else - { - List visited_ = new List(); - visited_.AddRange(visited); - visited_.Add(gn); - foreach (GraphNode next in gn.Suc) - { - m_DetectCutPoints(next,gn,visited_); - } - } - - } -*/ - - - private void m_DetectCutPoints(GraphNode gn) - { - List todo = new List(); - List done = new List(); - todo.Add(gn); - - GraphNode current = null; - todo[0].Index = 0; - - while (todo.Count > 0) - { - current = todo[0]; - todo.Remove(current); - - bool ready = true; - foreach (GraphNode p in current.Pre) - { - if (!done.Contains(p) ) - { - _loopbacktracking.Clear(); - if (!m_isLoop(current, p, todo, done)) - { - todo.Add(current); - ready = false; - break; - } - else - { - if (!current.LoopingPred.Contains(p)) current.LoopingPred.Add(p); - current.IsCutpoint = true; - } - } - } - if (!ready) continue; - done.Add(current); - foreach (GraphNode s in current.Suc) - { - if (!todo.Contains(s) && !done.Contains(s)) todo.Add(s); - } - } - - } - - List _loopbacktracking = new List(); - private bool m_isLoop(GraphNode loophead, GraphNode gn, List l1, List l2) - { - if (loophead == gn) return true; - if (l1.Contains(gn) || l2.Contains(gn) || _loopbacktracking.Contains(gn)) return false; - _loopbacktracking.Add(gn); - foreach (GraphNode p in gn.Pre) - { - if (m_isLoop(loophead, p, l1, l2)) return true; - } - return false; - } - - private List m_CollectLoops(GraphNode gn, Loop lastLoop) - { - List ret = new List(); - if (gn.Visited) return ret; - gn.Visited = true; - List loopingSucs = new List(); - if (gn.IsCutpoint) - { - Loop l = new Loop(gn); - if (lastLoop != null) - { - lastLoop.SucLoops.Add(l); - l.PreLoops.Add(lastLoop); - } - loopingSucs = l.LoopNodes; - lastLoop = l; - ret.Add(lastLoop); - } - foreach (GraphNode suc in gn.Suc) - { - if (!loopingSucs.Contains(suc)) ret.AddRange(m_CollectLoops(suc, lastLoop)); - } - //Debugger.Break(); - return ret; - } - } - #endregion - - #region GraphNodeStructure - internal class GraphNode - { - public int Index = -1; // Used for scc detection - public int LowLink = -1; // Used for scc detection - - public GraphNode(Block b) - { - Label = b; IsCutpoint = false; - } - public Block Label; - public List Pre = new List(); - public List Suc = new List(); - public bool IsCutpoint; - public bool Visited = false; - public List LoopingPred = new List(); - - public void AddEdgeTo(GraphNode other) - { - if (!this.Suc.Contains(other)) this.Suc.Add(other); - if (!other.Pre.Contains(this)) other.Pre.Add(this); - } - - public void RemoveEdgeTo(GraphNode other) - { - if (this.Suc.Contains(other)) this.Suc.Remove(other); - if (other.Pre.Contains(this)) other.Pre.Remove(this); - } - - } - #endregion - - #region LoopStructure - internal class Loop - { - public Loop(GraphNode cutpoint) - { - if (!cutpoint.IsCutpoint) - { - Debugger.Break(); - } - Cutpoint = cutpoint; - LoopNodes.Add(Cutpoint); - foreach (GraphNode gn in Cutpoint.LoopingPred) - { - CollectLoopBody(gn); - } - CollectLoopExitNodes(); - } - - // Copy Constructor - public Loop(Loop l, GraphAnalyzer ga, string prefix) - { - - Dictionary clonemap = new Dictionary(); - GraphNode clonecutpoint = null; - foreach (GraphNode gn in l.LoopNodes) - { - clonemap[gn] = ga.CloneGraphNode(gn, prefix); - if (gn == l.Cutpoint) clonecutpoint = clonemap[gn]; - } - - if (clonecutpoint == null) - { - Debugger.Break(); - return; - } - // Replace the pre and post nodes by the corresponding clone - foreach (GraphNode gn in l.LoopNodes) - { - List newl = new List(); - foreach (GraphNode g in clonemap[gn].Pre) - { - if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]); - else newl.Add(g); - } - clonemap[gn].Pre = newl; - newl = new List(); - foreach (GraphNode g in clonemap[gn].Suc) - { - if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]); - else newl.Add(g); - } - clonemap[gn].Suc = newl; - newl = new List(); - foreach (GraphNode g in clonemap[gn].LoopingPred) - { - if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]); - else newl.Add(g); - } - clonemap[gn].LoopingPred = newl; - } - - foreach (GraphNode gn in l.Cutpoint.LoopingPred) - { - clonecutpoint.LoopingPred.Remove(gn); - clonecutpoint.LoopingPred.Add(clonemap[gn]); - } - - - - SucLoops.AddRange(l.SucLoops); - PreLoops.AddRange(l.PreLoops); - Cutpoint = clonecutpoint; - LoopNodes.Add(Cutpoint); - foreach (GraphNode gn in Cutpoint.LoopingPred) - { - CollectLoopBody(gn); - } - CollectLoopExitNodes(); - } - - private void CollectLoopBody(GraphNode gn) - { - if (gn == Cutpoint) return; - if (!LoopNodes.Contains(gn)) - { - if (gn.IsCutpoint) // nested loop found - { - Loop lo = new Loop(gn); - foreach (GraphNode lgn in lo.LoopNodes) - { - if (!LoopNodes.Contains(lgn)) LoopNodes.Add(lgn); - } - NestedLoops.Add(lo); - } - else - { - LoopNodes.Add(gn); - } - foreach (GraphNode pre in gn.Pre) if (!gn.LoopingPred.Contains(pre)) CollectLoopBody(pre); - } - } - - private void CollectLoopExitNodes() - { - foreach (GraphNode gn in LoopNodes) - { - foreach (GraphNode gn_ in gn.Suc) - { - if (!LoopNodes.Contains(gn_) && !LoopExitNodes.Contains(gn_)) LoopExitNodes.Add(gn_); - } - } - } - - public GraphNode Cutpoint; - public List LoopExitNodes = new List(); - public List NestedLoops = new List(); - public List SucLoops = new List(); - public List PreLoops = new List(); - public List LoopNodes = new List(); - } - #endregion - - #endregion -} \ No newline at end of file diff --git a/Source/Doomed/DoomedStrategy.cs b/Source/Doomed/DoomedStrategy.cs deleted file mode 100644 index 76261827d..000000000 --- a/Source/Doomed/DoomedStrategy.cs +++ /dev/null @@ -1,528 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Collections; -using System.Collections.Generic; -using System.Diagnostics; -using System.Threading; -using System.IO; -using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; -using Microsoft.Boogie.VCExprAST; - -namespace VC -{ - #region SuperClass for different doomed code detection strategies - abstract internal class DoomDetectionStrategy - { - public int __DEBUG_BlocksChecked = 0; - public int __DEBUG_BlocksTotal = 0; - public int __DEBUG_InfeasibleTraces = 0; - public int __DEBUG_TracesChecked = 0; - public int __DEBUG_TracesTotal = 0; - public int __DEBUG_EQCTotal = 0; - public int __DEBUG_EQCLeaf = 0; - public int __DEBUG_EQCChecked = 0; - - //Please use this one to toggle your Debug output - protected bool __DEBUGOUT = CommandLineOptions.Clo.DoomStrategy != -1; - - protected Implementation impl; - protected BlockHierachy m_BlockH = null; - - protected int m_MaxBranchingDepth = 0; - protected int m_MaxK = 0; - - protected Stopwatch sw = new Stopwatch(); - - - // This is the List with all detected doomed program points. This List is used by VCDoomed.cs to - // create an error message - public List/*!*/>/*!*/ DetectedBlock = new List/*!*/>(); - - private List __DEBUG_minelements = new List(); - - // There is no default constructor, because these parameters are needed for most subclasses - public DoomDetectionStrategy(Implementation imp, Block unifiedexit, List unreach) - { - m_BlockH = new BlockHierachy(imp, unifiedexit); - __DEBUG_EQCLeaf = m_BlockH.Leaves.Count; - - //foreach (BlockHierachyNode bhn in m_BlockH.Leaves) - //{ - // if (bhn.Content.Count > 0) __DEBUG_minelements.Add(bhn.Content[0]); - //} - //if (imp.Blocks.Count>0) m_GatherInfo(imp.Blocks[0], 0, 0,0); - - - if (__DEBUGOUT) - { - Console.WriteLine("MaBranchingDepth {0} MaxMinPP {1} ", m_MaxBranchingDepth, m_MaxK); - - Console.WriteLine("AvgLeaverPerPath {0} AvgPLen {1}", 0, 0); - } - - MaxBlocks = imp.Blocks.Count; - MinBlocks = imp.Blocks.Count; - HACK_NewCheck = false; - __DEBUG_BlocksTotal = imp.Blocks.Count; - } - - public int MaxBlocks, MinBlocks; - public bool HACK_NewCheck; - - // This method is called by the prover while it returns true. The prover checks for each - // List lb if - // |= !lb_1 /\ ... /\ !lb_n => wlp(Program, false) - // and passes the result to SetCurrentResult - abstract public bool GetNextBlock(out List passBlock); - - // This method is called to inform about the prover outcome for the previous GetNextBlock call. - abstract public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb); - - protected List m_GetErrorTraceFromCE(DoomErrorHandler cb) - { - BlockHierachyNode tn=null; - List errortrace = new List(); - foreach (Block b in cb.TraceNodes) - { - if (errortrace.Contains(b)) continue; - if (m_BlockH.BlockToHierachyMap.TryGetValue(b, out tn)) - { - foreach (Block b_ in tn.Unavoidable) - { - if (!errortrace.Contains(b_)) errortrace.Add(b_); - } - foreach (Block b_ in tn.Content) - { - if (!errortrace.Contains(b_)) errortrace.Add(b_); - } - } - } - return errortrace; - } - - private List __pathLength = new List(); - private List __leavespp = new List(); - protected void m_GatherInfo(Block b, int branchingdepth, int leavespp, int plen) - { - if (b.Predecessors.Count > 1) branchingdepth--; - - GotoCmd gc = b.TransferCmd as GotoCmd; - if (__DEBUG_minelements.Contains(b)) leavespp++; - plen++; - if (gc != null && gc.labelTargets.Count>0) - { - if (gc.labelTargets.Count > 1) branchingdepth++; - m_MaxBranchingDepth = (branchingdepth > m_MaxBranchingDepth) ? branchingdepth : m_MaxBranchingDepth; - foreach (Block s in gc.labelTargets) - { - m_GatherInfo(s, branchingdepth, leavespp,plen); - } - } - else - { - __pathLength.Add(plen); - __leavespp.Add(leavespp); - m_MaxK = (m_MaxK > leavespp) ? m_MaxK : leavespp; - } - } - - - - } - #endregion - - #region BruteForce Strategy - internal class NoStrategy : DoomDetectionStrategy - { - private List m_Blocks = new List(); - private int m_Current = 0; - - public NoStrategy(Implementation imp, Block unifiedexit, List unreach) - : base(imp, unifiedexit, unreach) - { - m_Blocks = imp.Blocks; - } - - override public bool GetNextBlock(out List lb) - { - if (m_Current < m_Blocks.Count) - { - lb = new List(); - lb.Add(m_Blocks[m_Current]); - m_Current++; - return true; - } - lb = null; - return false; - } - - // This method is called to inform about the prover outcome for the previous GetNextBlock call. - override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) - { - this.__DEBUG_BlocksChecked++; - // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed) - if (outcome == ProverInterface.Outcome.Valid && m_Current <= m_Blocks.Count) - { - List lb = new List(); - lb.Add(m_Blocks[m_Current - 1]); - DetectedBlock.Add(lb); - } - return true; - } - } - #endregion - - #region Only check the minimal elements of the Hasse diagram - internal class HierachyStrategy : DoomDetectionStrategy - { - private List m_Blocks = new List(); - private List m_doomedBlocks = new List(); - private int m_Current = 0; - - public HierachyStrategy(Implementation imp, Block unifiedexit, List unreach) - : base(imp, unifiedexit, unreach) - { - foreach (BlockHierachyNode bhn in m_BlockH.Leaves) - { - if (bhn.Content.Count > 0) - { - m_Blocks.Add(bhn.Content[0]); - } - } - } - - override public bool GetNextBlock(out List lb) - { - sw.Start(); - if (m_Current < m_Blocks.Count) - { - lb = new List(); - lb.Add(m_Blocks[m_Current]); - m_Current++; - return true; - } - else - { - DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_doomedBlocks)); - } - lb = null; - return false; - } - - // This method is called to inform about the prover outcome for the previous GetNextBlock call. - override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) - { - this.__DEBUG_BlocksChecked++; - // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed) - if (outcome == ProverInterface.Outcome.Valid && m_Current <= m_Blocks.Count) - { - m_doomedBlocks.Add(m_Blocks[m_Current - 1]); - } - if (__DEBUGOUT) Console.WriteLine("K := {0,3} , out {1,8}, time {2,12}", MaxBlocks, outcome, sw.ElapsedTicks); - sw.Stop(); - sw.Reset(); - - return true; - } - } - #endregion - - #region Only check the minimal elements of the Hasse diagram and use CEs - internal class HierachyCEStrategy : DoomDetectionStrategy - { - private List m_Blocks = new List(); - private List m_doomedBlocks = new List(); - private Block m_Current = null; - - public HierachyCEStrategy(Implementation imp, Block unifiedexit, List unreach) - : base(imp, unifiedexit, unreach) - { - foreach (BlockHierachyNode bhn in m_BlockH.Leaves) - { - if (bhn.Content.Count > 0) - { - m_Blocks.Add(bhn.Content[0]); - } - } - } - - override public bool GetNextBlock(out List lb) - { - m_Current = null; - if (m_Blocks.Count > 0) - { - m_Current = m_Blocks[0]; - m_Blocks.Remove(m_Current); - lb = new List(); - lb.Add(m_Current); - return true; - } - else - { - DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_doomedBlocks)); - } - lb = null; - return false; - } - - // This method is called to inform about the prover outcome for the previous GetNextBlock call. - override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) - { - this.__DEBUG_BlocksChecked++; - // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed) - if (outcome == ProverInterface.Outcome.Valid && m_Current != null) - { - m_doomedBlocks.Add(m_Current); - } - else if (outcome == ProverInterface.Outcome.Invalid) - { - List errortrace = m_GetErrorTraceFromCE(cb); - foreach (Block b in errortrace) - { - if (m_Blocks.Contains(b)) - { - m_Blocks.Remove(b); - } - } - cb.TraceNodes.Clear(); - } - return true; - } - } - #endregion - - #region Path Cover Optimization with L - internal class PathCoverStrategy : DoomDetectionStrategy - { - List m_Uncheckedlocks = new List(); - List m_Ignore = new List(); - - Random m_Random = new Random(); - bool m_NoMoreMoves = false; - - private List m_foundBlock = new List(); - - public PathCoverStrategy(Implementation imp, Block unifiedexit, List unreach) - : base(imp, unifiedexit, unreach) - { - m_Ignore = unreach; - HACK_NewCheck = true; - impl = imp; - foreach (BlockHierachyNode bhn in m_BlockH.Leaves) - { - if (bhn.Content.Count > 0) - { - m_Uncheckedlocks.Add(bhn.Content[0]); - } - - } - m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks); - MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0); - MaxBlocks = -1; - } - - override public bool GetNextBlock(out List lb) - { - sw.Start(); - - lb = new List(); - - if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves) - { - if (m_Uncheckedlocks.Count > 0) - { - DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_Uncheckedlocks)); - } - - return false; - } - - lb.AddRange(m_Uncheckedlocks); - - return true; - } - - override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) - { - this.__DEBUG_BlocksChecked++; - // Valid means infeasible... - int oldl = MinBlocks; - int oldsize = m_Uncheckedlocks.Count; - - - if (outcome == ProverInterface.Outcome.Valid) - { - this.__DEBUG_InfeasibleTraces++; - if (MinBlocks == 1) - { - m_NoMoreMoves = true; - } - else - { - MinBlocks = 1; - } - } - else if (outcome == ProverInterface.Outcome.Invalid) - { - this.__DEBUG_TracesChecked++; - - List errortrace = m_GetErrorTraceFromCE(cb); - foreach (Block b in errortrace) - { - if (m_Uncheckedlocks.Contains(b)) - { - m_Uncheckedlocks.Remove(b); - } - } - cb.TraceNodes.Clear(); - m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks); - if (m_MaxK < 1) - { - m_NoMoreMoves = true; m_Uncheckedlocks.Clear(); - } - MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0); - //if (MinBlocks > m_MaxK) MinBlocks = m_MaxK; - - } - else - { - m_NoMoreMoves = true; m_Uncheckedlocks.Clear(); - } - if (__DEBUGOUT) - Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", MaxBlocks, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks); - sw.Stop(); - sw.Reset(); - return true; - } - - - } - #endregion - - #region Path Cover Optimization with K - internal class PathCoverStrategyK : DoomDetectionStrategy - { - List m_Uncheckedlocks = new List(); - List m_Ignore = new List(); - - Random m_Random = new Random(); - bool m_NoMoreMoves = false; - - private List m_foundBlock = new List(); - - public PathCoverStrategyK(Implementation imp, Block unifiedexit, List unreach) - : base(imp, unifiedexit, unreach) - { - m_Ignore = unreach; - HACK_NewCheck = true; - impl = imp; - foreach (BlockHierachyNode bhn in m_BlockH.Leaves) - { - if (bhn.Content.Count > 0) - { - m_Uncheckedlocks.Add(bhn.Content[0]); - } - - } - - m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks); - - MaxBlocks = m_Uncheckedlocks.Count; - if (m_MaxK < m_Uncheckedlocks.Count && m_MaxK > 0) - { - MaxBlocks = m_MaxK; - } - else if (m_MaxK >= m_Uncheckedlocks.Count) - { - MaxBlocks = m_Uncheckedlocks.Count; - } - else - { - MaxBlocks = 1; - } - //Console.WriteLine("InitK {0}, Max {1}", m_MaxK, MaxBlocks); - } - - override public bool GetNextBlock(out List lb) - { - sw.Start(); - - lb = new List(); - - if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves) - { - if (m_Uncheckedlocks.Count > 0) - { - DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_Uncheckedlocks)); - } - - return false; - } - - lb.AddRange(m_Uncheckedlocks); - - MaxBlocks = MaxBlocks > m_Uncheckedlocks.Count ? m_Uncheckedlocks.Count : MaxBlocks; - MinBlocks = MaxBlocks / 2 + (MaxBlocks % 2 > 0 ? 1 : 0); - return true; - } - - override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) - { - this.__DEBUG_BlocksChecked++; - // Valid means infeasible... - int oldk = MaxBlocks; - int oldl = MinBlocks; - int oldsize = m_Uncheckedlocks.Count; - - if (outcome == ProverInterface.Outcome.Valid) - { - this.__DEBUG_InfeasibleTraces++; - if (MaxBlocks == 1) - { - m_NoMoreMoves = true; - } - else - { - MaxBlocks /= 2; - } - } - else if (outcome == ProverInterface.Outcome.Invalid) - { - this.__DEBUG_TracesChecked++; - - List errortrace = m_GetErrorTraceFromCE(cb); - foreach (Block b in errortrace) - { - if (m_Uncheckedlocks.Contains(b)) - { - m_Uncheckedlocks.Remove(b); - } - } - cb.TraceNodes.Clear(); - - int k = m_BlockH.GetMaxK(m_Uncheckedlocks); - MaxBlocks = (k > MaxBlocks) ? MaxBlocks : k; - } - else - { - m_NoMoreMoves = true; m_Uncheckedlocks.Clear(); - } - if (__DEBUGOUT) - Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", oldk, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks); - sw.Stop(); - sw.Reset(); - return true; - } - - - } - #endregion - -} \ No newline at end of file diff --git a/Source/Doomed/HasseDiagram.cs b/Source/Doomed/HasseDiagram.cs deleted file mode 100644 index c866662e4..000000000 --- a/Source/Doomed/HasseDiagram.cs +++ /dev/null @@ -1,424 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Collections; -using System.Collections.Generic; -using System.Diagnostics; -using System.Threading; -using System.IO; -using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; -using Microsoft.Boogie.VCExprAST; - -namespace VC -{ - internal class BlockHierachyNode - { - public List Unavoidable; - public List Content = new List(); - public List Parents = new List(); - public List Children = new List(); - - public bool Checked, Doomed, DoubleChecked; - - public BlockHierachyNode(Block current, List unavoidable) - { - Checked = false; Doomed = false; DoubleChecked = false; - Unavoidable = unavoidable; - Content.Add(current); - } - - public static bool operator <(BlockHierachyNode left, BlockHierachyNode right) - { - return Compare(left,right)>0; - } - - public static bool operator >(BlockHierachyNode left, BlockHierachyNode right) - { - return Compare(left, right) < 0; - } - - // Compare the unavoidable blocks of two BlockHierachyNodes. - // returns 0 if sets have the same size, -1 if l2 has an element - // that is not in l1, otherwise the size of the intersection. - public static int Compare(BlockHierachyNode l1, BlockHierachyNode l2) - { - List tmp = new List(); - tmp.AddRange(l2.Unavoidable); - foreach (Block b in l1.Unavoidable) - { - if (tmp.Contains(b)) tmp.Remove(b); - else return -1; - } - return tmp.Count; - } - } - - internal class HasseDiagram - { - public readonly List Leaves = new List(); - public readonly List Roots = new List(); - - public HasseDiagram(List nodes) - { - Dictionary> largerElements = new Dictionary>(); - foreach (BlockHierachyNode left in nodes) - { - largerElements[left] = new List(); - foreach (BlockHierachyNode right in nodes) - { - if (left != right) - { - if (left < right) - { - largerElements[left].Add(right); - } - } - } - if (largerElements[left].Count == 0) Leaves.Add(left); - } - - List done = new List(); - List lastround = null; - - //Debugger.Break(); - - // Now that we have the leaves, build the Hasse diagram - while (done.Count < nodes.Count) - { - List maxelements = new List(); - maxelements.AddRange(nodes); - foreach (BlockHierachyNode bhn in nodes) - { - if (!done.Contains(bhn)) - { - foreach (BlockHierachyNode tmp in largerElements[bhn]) - { - if (maxelements.Contains(tmp)) maxelements.Remove(tmp); - } - } - else - { - maxelements.Remove(bhn); - } - } - - done.AddRange(maxelements); - - if (lastround != null) - { - foreach (BlockHierachyNode tmp in lastround) - { - foreach (BlockHierachyNode tmp2 in maxelements) - { - if (largerElements[tmp].Contains(tmp2)) - { - if (!tmp.Children.Contains(tmp2)) tmp.Children.Add(tmp2); - if (!tmp2.Parents.Contains(tmp)) tmp2.Parents.Add(tmp); - } - } - } - } - else - { - Roots.AddRange(maxelements); - } - lastround = maxelements; - } - } - - - } - - internal class BlockHierachy - { - public BlockHierachyNode RootNode = null; - readonly public Dictionary BlockToHierachyMap = new Dictionary(); - readonly public Dictionary> Dominators = new Dictionary>(); - readonly public Dictionary> PostDominators = new Dictionary>(); - readonly public List Leaves = new List(); - - private Implementation m_Impl; - - public BlockHierachy(Implementation impl, Block unifiedExit) - { - m_Impl = impl; - List blocks = impl.Blocks; - List tmp_hnodes = new List(); - Dictionary> unavoidable = new Dictionary>(); - - BfsTraverser(blocks[0], true, Dominators); - BfsTraverser(unifiedExit, false, PostDominators); - - foreach (Block b in blocks) - { - List l1 = Dominators[b]; - List l2 = PostDominators[b]; - unavoidable[b] = m_MergeLists(l1, l2); - - BlockHierachyNode bhn = new BlockHierachyNode(b, unavoidable[b]); - bool found = false; - foreach (KeyValuePair kvp in BlockToHierachyMap) - { - if (BlockHierachyNode.Compare(kvp.Value, bhn) == 0) // using the overloaded compare operator - { - kvp.Value.Content.AddRange(bhn.Content); - BlockToHierachyMap[b] = kvp.Value; - found = true; - break; - } - } - if (!found) - { - BlockToHierachyMap[b] = bhn; - tmp_hnodes.Add(bhn); - } - } - - HasseDiagram hd = new HasseDiagram(tmp_hnodes); - Leaves = hd.Leaves; - } - - public int GetMaxK(List blocks) - { - m_GetMaxK(blocks); - return (m_MaxK>0) ? m_MaxK : 1; - } - - private int m_MaxK = 0; - private void m_GetMaxK(List blocks) - { - m_MaxK = 0; - Dictionary kstore = new Dictionary(); - List todo = new List(); - List done = new List(); - todo.Add(m_Impl.Blocks[0]); - kstore[m_Impl.Blocks[0]] = 0; - int localmax; - Block current = null; - while (todo.Count > 0) - { - current = todo[0]; - todo.Remove(current); - bool ready = true; - localmax = 0; - if (current.Predecessors!=null) { - foreach (Block p in current.Predecessors) - { - if (!done.Contains(p)) - { - ready = false; break; - } - else localmax = (localmax > kstore[p]) ? localmax : kstore[p]; - } - } - if (!ready) - { - todo.Add(current); continue; - } - done.Add(current); - kstore[current] = (blocks.Contains(current)) ? localmax +1 : localmax; - - m_MaxK = (kstore[current] > m_MaxK) ? kstore[current] : m_MaxK; - - GotoCmd gc = current.TransferCmd as GotoCmd; - if (gc != null) - { - foreach (Block s in gc.labelTargets) - { - if (!todo.Contains(s)) todo.Add(s); - } - } - } - - } - - public List GetOtherDoomedBlocks(List doomedblocks) - { - List alsoDoomed = new List(); - List todo = new List(); - foreach (Block b in doomedblocks) - { - BlockToHierachyMap[b].Doomed = true; - todo.Add(BlockToHierachyMap[b]); - } - - while (todo.Count > 0) - { - BlockHierachyNode current = todo[0]; - todo.Remove(current); - if (!current.Doomed && current.Children.Count > 0) - { - bool childrenDoomed = true; - foreach (BlockHierachyNode c in current.Children) - { - if (!c.Doomed) { childrenDoomed = false; break; } - } - if (childrenDoomed) current.Doomed = true; - } - - if (current.Doomed) - { - foreach (BlockHierachyNode p in current.Parents) - { - if (!todo.Contains(p)) todo.Add(p); - } - foreach (Block b in current.Content) - { - if (!alsoDoomed.Contains(b)) alsoDoomed.Add(b); - } - } - } - - return alsoDoomed; - } - - public void Impl2Dot(string filename) - { - - Contract.Requires(filename != null); - List nodes = new List(); - List edges = new List(); - - string nodestyle = "[shape=box];"; - - List nl = new List(); - foreach (BlockHierachyNode h in BlockToHierachyMap.Values) if (!nl.Contains(h)) nl.Add(h); - - - foreach (BlockHierachyNode b in nl) - { - String l1 = ""; - foreach (Block bl in b.Content) l1 = String.Format("{0}_{1}", l1, bl.Label); - - Contract.Assert(b != null); - nodes.Add(string.Format("\"{0}\" {1}", l1, nodestyle)); - foreach (BlockHierachyNode b_ in b.Children) - { - - String l2 = ""; - foreach (Block bl in b_.Content) l2 = String.Format("{0}_{1}", l2, bl.Label); - edges.Add(String.Format("\"{0}\" -> \"{1}\";", l1, l2)); - } - - } - - using (StreamWriter sw = new StreamWriter(filename)) - { - sw.WriteLine(String.Format("digraph {0} {{", "DISCO")); - // foreach (string! s in nodes) { - // sw.WriteLine(s); - // } - foreach (string s in edges) - { - Contract.Assert(s != null); - sw.WriteLine(s); - } - sw.WriteLine("}}"); - sw.Close(); - } - } - - private void BfsTraverser(Block current, bool forward, Dictionary> unavoidableBlocks) - { - List todo = new List(); - List done = new List(); - unavoidableBlocks[current] = new List(); - //Debugger.Break(); - todo.Add(current); - while (todo.Count > 0) - { - current = todo[0]; - todo.Remove(current); - List pre = m_Predecessors(current, forward); - bool ready = true; - if (pre != null) - { - foreach (Block bpre in pre) - { - if (!done.Contains(bpre)) - { - ready = false; - break; - } - } - } - if (!ready) - { - todo.Add(current); - continue; - } - done.Add(current); - unavoidableBlocks[current].Add(current); - - List suc = m_Succecessors(current, forward); - if (suc == null) continue; - foreach (Block bsuc in suc) - { - if (unavoidableBlocks.ContainsKey(bsuc)) - { - unavoidableBlocks[bsuc] = m_IntersectLists(unavoidableBlocks[bsuc], unavoidableBlocks[current]); - } - else - { - todo.Add(bsuc); - unavoidableBlocks[bsuc] = new List(); - unavoidableBlocks[bsuc].AddRange(unavoidableBlocks[current]); - } - - } - } - - } - - private List m_MergeLists(List lb1, List lb2) - { - List ret = new List(); - ret.AddRange(lb1); - foreach (Block b in lb2) - { - if (!ret.Contains(b)) ret.Add(b); - } - return ret; - } - - private List m_IntersectLists(List lb1, List lb2) - { - List ret = new List(); - ret.AddRange(lb1); - foreach (Block b in lb2) - { - if (!lb1.Contains(b)) ret.Remove(b); - } - foreach (Block b in lb1) - { - if (ret.Contains(b) && !lb2.Contains(b)) ret.Remove(b); - } - return ret; - } - - private List m_Predecessors(Block b, bool forward) - { - if (forward) return b.Predecessors; - GotoCmd gc = b.TransferCmd as GotoCmd; - if (gc != null) - { - return gc.labelTargets; - } - return null; - } - - private List m_Succecessors(Block b, bool forward) - { - return m_Predecessors(b, !forward); - } - - - } - -} \ No newline at end of file diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs deleted file mode 100644 index 822fb9c04..000000000 --- a/Source/Doomed/VCDoomed.cs +++ /dev/null @@ -1,826 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Collections; -using System.Collections.Generic; -using System.Diagnostics; -using System.Threading; -using System.IO; -using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; -using Microsoft.Boogie.VCExprAST; - -namespace VC { - public partial class DCGen : ConditionGeneration { - private bool _print_time = CommandLineOptions.Clo.DoomStrategy!=-1; - #region Attributes - static private Dictionary/*!*/ m_BlockReachabilityMap; - Dictionary/*!*/ m_copiedBlocks = new Dictionary(); - const string reachvarsuffix = "__ivebeenthere"; - List/*!*/ m_doomedCmds = new List(); - [ContractInvariantMethod] - void ObjectInvariant() { - - } - - #endregion - - - /// - /// Constructor. Initializes the theorem prover. - /// - public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List checkers) - : base(program, checkers) { - Contract.Requires(program != null); - - this.appendLogFile = appendLogFile; - this.logFilePath = logFilePath; - m_BlockReachabilityMap = new Dictionary(); - } - - /// - /// Debug method that prints a dot file of the - /// current set of blocks in impl to filename. - /// - private void Impl2Dot(Implementation impl, string filename) { - Contract.Requires(impl != null); - Contract.Requires(filename != null); - List nodes = new List(); - List edges = new List(); - - string nodestyle = "[shape=box];"; - - foreach (Block b in impl.Blocks) { - Contract.Assert(b != null); - nodes.Add(string.Format("\"{0}\" {1}", b.Label, nodestyle)); - GotoCmd gc = b.TransferCmd as GotoCmd; - if (gc != null) - { - Contract.Assert(gc.labelTargets != null); - foreach (Block b_ in gc.labelTargets) - { - Contract.Assert(b_ != null); - edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label)); - } - } - - //foreach (Block b_ in b.Predecessors) - //{ - // edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label)); - //} - } - - using (StreamWriter sw = new StreamWriter(filename)) { - sw.WriteLine(String.Format("digraph {0} {{", impl.Name)); - // foreach (string! s in nodes) { - // sw.WriteLine(s); - // } - foreach (string s in edges) { - Contract.Assert(s != null); - sw.WriteLine(s); - } - sw.WriteLine("}}"); - sw.Close(); - } - } - private const string _copyPrefix = "CPY__"; - - private List m_UncheckableBlocks = null; - - /// - /// MSchaef: - /// - remove loops and add reach variables - /// - make it a passive program - /// - compute the wlp for each block - /// - check if |= (reach=false) => wlp.S.false holds for each reach - /// - /// - public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) { - Contract.EnsuresOnThrow(true); - - Console.WriteLine(); - Console.WriteLine("Checking function {0}", impl.Name); - callback.OnProgress("doomdetector", 0, 0, 0); - - bool restartTP = CommandLineOptions.Clo.DoomRestartTP ; - - //Impl2Dot(impl, String.Format("c:/dot/{0}_orig.dot", impl.Name)); - - Transform4DoomedCheck(impl); - - //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name)); - - Checker checker = FindCheckerFor(1000); - Contract.Assert(checker != null); - int assertionCount; - DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount); - CumulativeAssertionCount += assertionCount; - - //EmitImpl(impl, false); - - int _totalchecks = 0; - - ProverInterface.Outcome outcome; - dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); - - System.TimeSpan ts = new TimeSpan(); - - if (_print_time) Console.WriteLine("Total number of blocks {0}", impl.Blocks.Count); - - List lb; - List lv = new List(); - - while (dc.GetNextBlock(out lb)) - { - Contract.Assert(lb != null); - outcome = ProverInterface.Outcome.Undetermined; - - Variable v = null; - lv.Clear(); - - foreach (Block b_ in lb) - { - if (!m_BlockReachabilityMap.TryGetValue(b_, out v)) - { - // This should cause an error - continue; - } - //Console.Write("{0}, ",b_.Label); - lv.Add(v); - } - //Console.WriteLine(); - Dictionary finalreachvars = m_GetPostconditionVariables(impl.Blocks,lb); - if (lv.Count < 1) - { - - continue; - } - - Contract.Assert(lv != null); - _totalchecks++; - - - if (!dc.CheckLabel(lv,finalreachvars, out outcome)) { - return Outcome.Inconclusive; - } - ts += dc.DEBUG_ProverTime.Elapsed; - - if (restartTP) - { - checker.Close(); - checker = FindCheckerFor(1000); - dc.RespawnChecker(impl, checker); - dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); - } - - } - checker.Close(); - - if (_print_time) - { - Console.WriteLine("Number of Checkes / #Blocks: {0} of {1}", _totalchecks, impl.Blocks.Count); - dc.__DEBUG_PrintStatistics(); - Console.WriteLine("Total time for this method: {0}", ts.ToString()); - } - #region Try to produce a counter example (brute force) - if (dc.DoomedSequences.Count > 0) { - int counter = 0; - List _all = new List(); - foreach (List lb_ in dc.DoomedSequences) - { - foreach (Block b_ in lb_) - { - if (!_all.Contains(b_) && !m_UncheckableBlocks.Contains(b_)) - { - _all.Add(b_); counter++; - if (!_print_time) Console.WriteLine(b_.Label); - } - } - } - if (_all.Count > 0) - { - Console.WriteLine("#Dead Blocks found: {0}: ", counter); - return Outcome.Errors; - } - } - #endregion - - - return Outcome.Correct; - } - - private Dictionary m_GetPostconditionVariables(List allblock, List passBlock) - { - Dictionary r = new Dictionary(); - foreach (Block b in allblock) - { - Variable v; - if (m_BlockReachabilityMap.TryGetValue(b, out v)) - { - if (passBlock.Contains(b)) r[m_LastReachVarIncarnation[v]] = 1; - } - else - { - Console.WriteLine("there is no reachability variable for {0}", b.Label); - } - } - return r; - } - -#if false - #region Error message construction - private void SearchCounterexample(Implementation impl, DoomErrorHandler errh, VerifierCallback callback) { - Contract.Requires(impl != null); - Contract.Requires(errh != null); - Contract.Requires(callback != null); - Contract.Requires(errh.m_Reachvar != null); - //if (errh.m_Reachvar==null) { - // Contract.Assert(false);throw new cce.UnreachableException(); - //} - m_doomedCmds.Clear(); - - Dictionary> cmdbackup = new Dictionary>(); - - BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, 0, impl.Blocks.Count / 2 - 1); - BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, impl.Blocks.Count / 2, impl.Blocks.Count - 1); - - List causals = CollectCausalStatements(impl.Blocks[0]); - foreach (Cmd c in causals) { - Contract.Assert(c != null); - GenerateErrorMessage(c, causals); - } - - #region Undo all modifications - foreach (KeyValuePair> kvp in cmdbackup) { - Contract.Assert(kvp.Key != null); - Contract.Assert(kvp.Value != null); - kvp.Key.Cmds = kvp.Value; - } - #endregion - } - - #region Causal Statement Tree - - private void GenerateErrorMessage(Cmd causalStatement, List causals) { - Contract.Requires(causalStatement != null); - Contract.Requires(cce.NonNullElements(causals)); - AssumeCmd uc = causalStatement as AssumeCmd; - AssertCmd ac = causalStatement as AssertCmd; - ConsoleColor col = Console.ForegroundColor; - - // Trivial case. Must be either assume or assert false - if (m_doomedCmds.Count == 1) { - Console.WriteLine("Found a trivial error:"); - if (uc != null) { - Console.Write("Trivial false assumption: "); - Console.Write("({0};{1}):", uc.tok.line, uc.tok.col); - } - if (ac != null) { - Console.Write("Trivial false assertion: "); - Console.Write("({0};{1}):", ac.tok.line, ac.tok.col); - } - causalStatement.Emit(new TokenTextWriter("", Console.Out, false), 0); - } else { - // Safety error - if (ac != null) { - Console.ForegroundColor = ConsoleColor.Red; - Console.WriteLine("Safety error:"); - Console.ForegroundColor = col; - Console.Write("This assertion is violated: "); - Console.Write("({0};{1}):", ac.tok.line, ac.tok.col); - ac.Emit(new TokenTextWriter("", Console.Out, false), 0); - } - if (uc != null) { - bool containsAssert = false; - foreach (Cmd c in m_doomedCmds) { - Contract.Assert(c != null); - if (causals.Contains(c)) { - continue; - } - AssertCmd asrt = c as AssertCmd; - if (asrt != null) { - containsAssert = true; - break; - } - } - // Plausibility error - if (containsAssert) { - Console.ForegroundColor = ConsoleColor.Yellow; - Console.WriteLine("Plausibility error:"); - Console.ForegroundColor = col; - Console.Write("There is no legal exeuction passing: "); - Console.Write("({0};{1})", uc.tok.line, uc.tok.col); - uc.Emit(new TokenTextWriter("", Console.Out, false), 0); - } else { // Reachability error - Console.ForegroundColor = ConsoleColor.DarkRed; - Console.WriteLine("Reachability error:"); - Console.ForegroundColor = col; - Console.Write("No execution can reach: "); - Console.Write("({0};{1})", uc.tok.line, uc.tok.col); - uc.Emit(new TokenTextWriter("", Console.Out, false), 0); - } - - } - - Console.ForegroundColor = ConsoleColor.White; - Console.WriteLine("...on any execution passing through:"); - foreach (Cmd c in m_doomedCmds) { - Contract.Assert(c != null); - if (causals.Contains(c)) { - continue; - } - Console.ForegroundColor = col; - Console.Write("In ({0};{1}): ", c.tok.line, c.tok.col); - Console.ForegroundColor = ConsoleColor.DarkYellow; - c.Emit(new TokenTextWriter("", Console.Out, false), 0); - } - Console.ForegroundColor = col; - Console.WriteLine("--"); - - } - } - - private List CollectCausalStatements(Block b) { - Contract.Requires(b != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - - Cmd lastCausal = null; - foreach (Cmd c in b.Cmds) { - Contract.Assert(c != null); - AssertCmd ac = c as AssertCmd; - AssumeCmd uc = c as AssumeCmd; - if (ac != null && !ContainsReachVariable(ac)) { - if (ac.Expr != Expr.True) { - lastCausal = c; - } - } else if (uc != null && !ContainsReachVariable(uc)) { - lastCausal = c; - } - } - - List causals = new List(); - GotoCmd gc = b.TransferCmd as GotoCmd; - if (gc != null && gc.labelTargets != null) { - List tmp; - //bool allcausal = true; - foreach (Block b_ in gc.labelTargets) { - Contract.Assert(b_ != null); - tmp = CollectCausalStatements(b_); - - foreach (Cmd cau in tmp) { - if (!causals.Contains(cau)) - causals.Add(cau); - } - } - //if (allcausal) - if (causals.Count > 0) - return causals; - } - if (lastCausal != null) - causals.Add(lastCausal); - return causals; - } - - #endregion - - bool BruteForceCESearch(Variable reachvar, Implementation impl, VerifierCallback callback, - Dictionary> cmdbackup, int startidx, int endidx) { - Contract.Requires(reachvar != null); - Contract.Requires(impl != null); - Contract.Requires(callback != null); - Contract.Requires(cce.NonNullElements(cmdbackup)); - #region Modify implementation - for (int i = startidx; i <= endidx; i++) { - if (_copiedBlock.Contains(impl.Blocks[i])) - continue; - List cs = new List(); - cmdbackup.Add(impl.Blocks[i], impl.Blocks[i].Cmds); - foreach (Cmd c in impl.Blocks[i].Cmds) { - Contract.Assert(c != null); - if (ContainsReachVariable(c)) { - cs.Add(c); - continue; - } - AssertCmd ac = c as AssertCmd; - AssumeCmd uc = c as AssumeCmd; - if (ac != null) { - cs.Add(new AssertCmd(ac.tok, Expr.True)); - } else if (uc != null) { - cs.Add(new AssertCmd(uc.tok, Expr.True)); - } else { - cs.Add(c); - } - } - impl.Blocks[i].Cmds = cs; - } - #endregion - - ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined; - if (!ReCheckImpl(reachvar, impl, callback, out outcome)) { - UndoBlockModifications(impl, cmdbackup, startidx, endidx); - return false; - } - if (outcome == ProverInterface.Outcome.Valid) { - return true; - } else if (outcome == ProverInterface.Outcome.Invalid) { - UndoBlockModifications(impl, cmdbackup, startidx, endidx); - int mid = startidx + (endidx - startidx) / 2; - if (startidx >= endidx) { - // Now we found an interesting Block and we have to - // search for the interesting statements. - int cmdcount = impl.Blocks[endidx].Cmds.Length; - BruteForceCmd(impl.Blocks[endidx], 0, cmdcount / 2 - 1, reachvar, impl, callback); - BruteForceCmd(impl.Blocks[endidx], cmdcount / 2, cmdcount - 1, reachvar, impl, callback); - return true; - } else { - BruteForceCESearch(reachvar, impl, callback, cmdbackup, startidx, mid); - BruteForceCESearch(reachvar, impl, callback, cmdbackup, mid + 1, endidx); - return true; - } - } else { - UndoBlockModifications(impl, cmdbackup, startidx, endidx); - return false; - } - } - - bool BruteForceCmd(Block b, int startidx, int endidx, Variable reachvar, - Implementation impl, VerifierCallback callback) { - Contract.Requires(b != null); - Contract.Requires(reachvar != null); - Contract.Requires(impl != null); - Contract.Requires(callback != null); - #region Modify Cmds - List backup = b.Cmds; - Contract.Assert(backup != null); - List cs = new List(); - for (int i = 0; i < startidx; i++) { - cs.Add(b.Cmds[i]); - } - for (int i = startidx; i <= endidx; i++) { - Cmd c = b.Cmds[i]; - if (ContainsReachVariable(c)) { - cs.Add(c); - continue; - } - cs.Add(new AssertCmd(c.tok, Expr.True)); - } - for (int i = endidx + 1; i < b.Cmds.Length; i++) { - cs.Add(b.Cmds[i]); - } - - b.Cmds = cs; - #endregion - - #region Recheck - ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined; - if (!ReCheckImpl(reachvar, impl, callback, out outcome)) { - b.Cmds = backup; - return false; - } - #endregion - - if (outcome == ProverInterface.Outcome.Valid) { - return true; - } else if (outcome == ProverInterface.Outcome.Invalid) { - b.Cmds = backup; - if (startidx >= endidx) { - if (!ContainsReachVariable(b.Cmds[endidx])) { - // Console.Write(" Witness ("); - // - // ConsoleColor col = Console.ForegroundColor; - // Console.ForegroundColor = ConsoleColor.White; - // Console.Write("{0};{1}", b.Cmds[endidx].tok.line, b.Cmds[endidx].tok.col ); - // Console.ForegroundColor = col; - // Console.Write("): "); - // Console.ForegroundColor = ConsoleColor.Yellow; - // b.Cmds[endidx].Emit(new TokenTextWriter("", Console.Out, false), 0); - // Console.ForegroundColor = col; - - m_doomedCmds.Add(b.Cmds[endidx]); - return true; - } else { - return false; - } - } else { - int mid = startidx + (endidx - startidx) / 2; - BruteForceCmd(b, startidx, mid, reachvar, impl, callback); - BruteForceCmd(b, mid + 1, endidx, reachvar, impl, callback); - return false; // This is pure random - } - } else { - b.Cmds = backup; - return false; - } - } - - void UndoBlockModifications(Implementation impl, Dictionary/*!*/>/*!*/ cmdbackup, - int startidx, int endidx) { - Contract.Requires(cce.NonNullElements(cmdbackup)); - Contract.Requires(impl != null); - for (int i = startidx; i <= endidx; i++) { - List cs = null; - if (cmdbackup.TryGetValue(impl.Blocks[i], out cs)) { - Contract.Assert(cs != null); - impl.Blocks[i].Cmds = cs; - cmdbackup.Remove(impl.Blocks[i]); - } - } - } - - bool ReCheckImpl(Variable reachvar, Implementation impl, VerifierCallback callback, - out ProverInterface.Outcome outcome) { - Contract.Requires(reachvar != null); - Contract.Requires(impl != null); - Contract.Requires(callback != null); - Checker checker = FindCheckerFor(impl, 1000); - Contract.Assert(checker != null); - DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks); - dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); - outcome = ProverInterface.Outcome.Undetermined; - List rv = new List(); - rv.Add(reachvar); - if (!dc.CheckLabel(rv,null, out outcome)) { - checker.Close(); - return false; - } - checker.Close(); - return true; - } - - - - bool ContainsReachVariable(Cmd c) { - Contract.Requires(c != null); - AssertCmd artc = c as AssertCmd; - AssumeCmd amec = c as AssumeCmd; - Expr e; - if (artc != null) { - e = artc.Expr; - } else if (amec != null) { - e = amec.Expr; - } else { - return false; - } - Set freevars = new Set(); - e.ComputeFreeVariables(freevars); - foreach (Variable v in freevars) { - Contract.Assert(v != null); - if (v.Name.Contains(reachvarsuffix)) - return true; - } - return false; - } -#endregion -#endif - - - Block exitBlock; - - #region Program Passification - private void GenerateHelperBlocks(Implementation impl) { - Contract.Requires(impl != null); - Dictionary gotoCmdOrigins = new Dictionary(); - exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins); - Contract.Assert(exitBlock != null); - - AddBlocksBetween(impl.Blocks); - - #region Insert pre- and post-conditions and where clauses as assume and assert statements - { - List cc = new List(); - // where clauses of global variables - foreach (var gvar in program.GlobalVariables) { - if (gvar.TypedIdent.WhereExpr != null) { - Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr); - cc.Add(c); - } - } - // where clauses of in- and out-parameters - cc.AddRange(GetParamWhereClauses(impl)); - // where clauses of local variables - foreach (Variable lvar in impl.LocVars) { - Contract.Assert(lvar != null); - if (lvar.TypedIdent.WhereExpr != null) { - Cmd c = new AssumeCmd(lvar.tok, lvar.TypedIdent.WhereExpr); - cc.Add(c); - } - } - - // add cc and the preconditions to new blocks preceding impl.Blocks[0] - InjectPreconditions(impl, cc); - - // append postconditions, starting in exitBlock and continuing into other blocks, if needed - InjectPostConditions(impl, exitBlock, gotoCmdOrigins); - } - #endregion - } - - - private Dictionary PassifyProgram(Implementation impl, ModelViewInfo mvInfo) { - Contract.Requires(impl != null); - Contract.Requires(mvInfo != null); - Contract.Requires(this.exitBlock != null); - Contract.Ensures(Contract.Result() != null); - - CurrentLocalVariables = impl.LocVars; - return Convert2PassiveCmd(impl, mvInfo); - //return new Hashtable(); - } - - /// - /// Add additional variable to allow checking as described in the paper - /// "It's doomed; we can prove it" - /// - private List GenerateReachabilityPredicates(Implementation impl) - { - Contract.Requires(impl != null); - - foreach (Block b in impl.Blocks) - { - Contract.Assert(b != null); - //if (b.Predecessors.Length==0) continue; - //if (b.Cmds.Length == 0 ) continue; - - Variable v_ = new LocalVariable(Token.NoToken, - new TypedIdent(b.tok, b.Label + reachvarsuffix, new BasicType(SimpleType.Int ))); - - impl.LocVars.Add(v_); - - m_BlockReachabilityMap[b] = v_; - - IdentifierExpr lhs = new IdentifierExpr(b.tok, v_); - Contract.Assert(lhs != null); - - impl.Proc.Modifies.Add(lhs); - - List lhsl = new List(); - lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs)); - List rhsl = new List(); - rhsl.Add(Expr.Literal(1) ); - - - List cs = new List { new AssignCmd(Token.NoToken, lhsl, rhsl) }; - cs.AddRange(b.Cmds); - b.Cmds = cs; - - //checkBlocks.Add(new CheckableBlock(v_,b)); - } - - List incReachVars = new List(); - foreach (KeyValuePair kvp in m_BlockReachabilityMap) - { - IdentifierExpr lhs = new IdentifierExpr(Token.NoToken, kvp.Value); - impl.Proc.Modifies.Add(lhs); - incReachVars.Add(new AssumeCmd(Token.NoToken, Expr.Le(lhs, Expr.Literal(1)))); - } - - return incReachVars; - } - - #endregion - - #region Compute loop-free approximation - - // this might be redundant, but I didn't find a better place to get this information. - private Dictionary m_LastReachVarIncarnation = new Dictionary(); - - private void Transform4DoomedCheck(Implementation impl) - { - variable2SequenceNumber = new Dictionary(); - incarnationOriginMap = new Dictionary(); - if (impl.Blocks.Count < 1) return; - - impl.PruneUnreachableBlocks(); - AddBlocksBetween(impl.Blocks); - ResetPredecessors(impl.Blocks); - - GraphAnalyzer ga = new GraphAnalyzer(impl.Blocks); - LoopRemover lr = new LoopRemover(ga); - lr.AbstractLoopUnrolling(); - - impl.Blocks = ga.ToImplementation(out m_UncheckableBlocks); - ResetPredecessors(impl.Blocks); - - // Check for the "BlocksBetween" if all their successors are in m_UncheckableBlocks - List oldblocks = new List(); - oldblocks.AddRange(impl.Blocks); - GenerateHelperBlocks(impl); - #region Check for the "BlocksBetween" if all their successors are in m_UncheckableBlocks - foreach (Block b in impl.Blocks) - { - if (oldblocks.Contains(b)) continue; - GotoCmd gc = b.TransferCmd as GotoCmd; - if (gc != null) - { - bool allsuccUncheckable = true; - foreach (Block _b in gc.labelTargets) - { - if (!m_UncheckableBlocks.Contains(_b)) - { - allsuccUncheckable = false; break; - } - } - if (allsuccUncheckable && !m_UncheckableBlocks.Contains(b)) m_UncheckableBlocks.Add(b); - } - } - #endregion - - impl.Blocks = DeepCopyBlocks(impl.Blocks, m_UncheckableBlocks); - - m_BlockReachabilityMap = new Dictionary(); - List cs = GenerateReachabilityPredicates(impl); - - //foreach (Block test in getTheFFinalBlock(impl.Blocks[0])) - //{ - // test.Cmds.AddRange(cs); - //} - - ResetPredecessors(impl.Blocks); - //EmitImpl(impl,false); - - Dictionary var2Expr = PassifyProgram(impl, new ModelViewInfo(program, impl)); - - // Collect the last incarnation of each reachability variable in the passive program - foreach (KeyValuePair kvp in m_BlockReachabilityMap) - { - if (var2Expr.ContainsKey(kvp.Value)) - { - m_LastReachVarIncarnation[kvp.Value] = (Expr)var2Expr[kvp.Value]; - } - } - } - - - List getTheFFinalBlock(Block b) - { - List lb = new List(); - GotoCmd gc = b.TransferCmd as GotoCmd; - if (gc == null) lb.Add(b); - else - { - foreach (Block s in gc.labelTargets) - { - foreach (Block r in getTheFFinalBlock(s)) if (!lb.Contains(r)) lb.Add(r); - } - } - return lb; - } - - - private List DeepCopyBlocks(List lb, List uncheckables) - { - List clones = new List(); - List uncheck_ = new List(); - Dictionary clonemap = new Dictionary(); - - foreach (Block b in lb) - { - Block clone = CloneBlock(b); - clones.Add(clone); - clonemap[b] = clone; - if (uncheckables.Contains(b)) uncheck_.Add(clone); - } - uncheckables.Clear(); - uncheckables.AddRange(uncheck_); - // update the successors and predecessors - foreach (Block b in lb) - { - List newpreds = new List(); - foreach (Block b_ in b.Predecessors) - { - newpreds.Add(clonemap[b_]); - } - clonemap[b].Predecessors = newpreds; - GotoCmd gc = b.TransferCmd as GotoCmd; - ReturnCmd rc = b.TransferCmd as ReturnCmd; - if (gc != null) - { - List lseq = new List(); - List bseq = new List(); - foreach (string s in gc.labelNames) lseq.Add(s); - foreach (Block b_ in gc.labelTargets) bseq.Add(clonemap[b_]); - GotoCmd tcmd = new GotoCmd(gc.tok, lseq, bseq); - clonemap[b].TransferCmd = tcmd; - } - else if (rc != null) - { - clonemap[b].TransferCmd = new ReturnCmd(rc.tok); - } - } - return clones; - } - - private Block CloneBlock(Block b) - { - Block clone = new Block(b.tok, b.Label, b.Cmds, b.TransferCmd); - if (this.exitBlock == b) this.exitBlock = clone; - return clone; - } - #endregion - } -} diff --git a/Source/ExecutionEngine/ExecutionEngine-NetCore.csproj b/Source/ExecutionEngine/ExecutionEngine-NetCore.csproj index 5c618eac1..a7541a6a9 100644 --- a/Source/ExecutionEngine/ExecutionEngine-NetCore.csproj +++ b/Source/ExecutionEngine/ExecutionEngine-NetCore.csproj @@ -16,7 +16,6 @@ - diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 41ebab9f3..706f811bd 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -102,15 +102,11 @@ public void WriteTrailer(PipelineStatistics stats) Contract.Requires(0 <= stats.VerifiedCount && 0 <= stats.ErrorCount && 0 <= stats.InconclusiveCount && 0 <= stats.TimeoutCount && 0 <= stats.OutOfMemoryCount); Console.WriteLine(); - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) - { - Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.DescriptiveToolName, stats.VerifiedCount, stats.ErrorCount, stats.ErrorCount == 1 ? "" : "s"); - } - else if (CommandLineOptions.Clo.ShowVerifiedProcedureCount) + if (CommandLineOptions.Clo.ShowVerifiedProcedureCount) { Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, stats.VerifiedCount, stats.ErrorCount, stats.ErrorCount == 1 ? "" : "s"); } - else + else { Console.Write("{0} finished with {1} error{2}", CommandLineOptions.Clo.DescriptiveToolName, stats.ErrorCount, stats.ErrorCount == 1 ? "" : "s"); } @@ -370,7 +366,7 @@ public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) isMonomorphic = false; return base.VisitDeclWithFormals(node); } - + public override BinderExpr VisitBinderExpr(BinderExpr node) { if (node.TypeParameters.Count > 0) @@ -440,7 +436,7 @@ public static Program CachedProgram(string programId) var result = programCache.Get(programId) as Program; return result; } - + static List Checkers = new List(); static DateTime FirstRequestStart; @@ -788,7 +784,7 @@ public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFil public static void Inline(Program program) { Contract.Requires(program != null); - + if (CommandLineOptions.Clo.Trace) Console.WriteLine("Inlining..."); @@ -996,7 +992,7 @@ public static PipelineOutcome InferAndVerify(Program program, semaphore.Wait(cts.Token); } catch (OperationCanceledException) - { + { break; } tasks[j].Start(Scheduler); @@ -1301,11 +1297,7 @@ public void Add(int index, StringWriter output) private static ConditionGeneration CreateVCGen(Program program, List checkers) { ConditionGeneration vcgen = null; - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) - { - vcgen = new DCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers); - } - else if (CommandLineOptions.Clo.FixedPointEngine != null) + if (CommandLineOptions.Clo.FixedPointEngine != null) { vcgen = new FixedpointVC(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers); } @@ -1315,11 +1307,11 @@ private static ConditionGeneration CreateVCGen(Program program, List ch } else if (CommandLineOptions.Clo.SecureVcGen != null) { - vcgen = new SecureVCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers); + vcgen = new SecureVCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers); } else { - vcgen = new VCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers); + vcgen = new VCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers); } return vcgen; } @@ -1613,7 +1605,7 @@ private static string OutcomeIndication(VC.VCGen.Outcome outcome, List !e.IsAuxiliaryCexForDiagnosingTimeouts).Count(); - Interlocked.Add(ref stats.ErrorCount, cnt); - if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, cnt); } - } + int cnt = errors.Where(e => !e.IsAuxiliaryCexForDiagnosingTimeouts).Count(); + Interlocked.Add(ref stats.ErrorCount, cnt); + if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, cnt); } break; } } diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj index 6cb7b5238..eced1005a 100644 --- a/Source/ExecutionEngine/ExecutionEngine.csproj +++ b/Source/ExecutionEngine/ExecutionEngine.csproj @@ -150,10 +150,6 @@ {B230A69C-C466-4065-B9C1-84D80E76D802} Core - - {884386A3-58E9-40BB-A273-B24976775553} - Doomed - {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} Graph diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 6680b5e36..295d89113 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -629,21 +629,14 @@ private void GenVC(Implementation impl) fv.functionsUsed.Iter(tup => constant2FuncCall.Add(tup.Item2.Name, tup.Item3)); var gen = prover.VCExprGen; - VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : gen.Integer(Microsoft.Basetypes.BigNum.ZERO); + VCExpr controlFlowVariableExpr = gen.Integer(Microsoft.Basetypes.BigNum.ZERO); var vcexpr = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, prover.Context); - if (!CommandLineOptions.Clo.UseLabels) - { - VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(Microsoft.Basetypes.BigNum.ZERO), gen.Integer(Microsoft.Basetypes.BigNum.ZERO)); - VCExpr eqExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(Microsoft.Basetypes.BigNum.FromInt(impl.Blocks[0].UniqueId))); - vcexpr = gen.Implies(eqExpr, vcexpr); - } + VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(Microsoft.Basetypes.BigNum.ZERO), gen.Integer(Microsoft.Basetypes.BigNum.ZERO)); + VCExpr eqExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(Microsoft.Basetypes.BigNum.FromInt(impl.Blocks[0].UniqueId))); + vcexpr = gen.Implies(eqExpr, vcexpr); - ProverInterface.ErrorHandler handler = null; - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) - handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, prover.Context, program); - else - handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, prover.Context, program); + ProverInterface.ErrorHandler handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, prover.Context, program); impl2ErrorHandler.Add(impl.Name, Tuple.Create(handler, collector)); @@ -664,7 +657,7 @@ private void GenVC(Implementation impl) // the right thing. foreach (var tup in fv.functionsUsed) { - // Ignore ones with bound varibles + // Ignore ones with bound variables if (tup.Item2.InParams.Count > 0) continue; var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3); tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt); @@ -3735,8 +3728,7 @@ private static bool CheckIfUnsat(Expr a, VCExpressionGenerator gen, ProverInterf counter++; } - var vc1 = ToVcExpr(a, incarnations, gen); - var vc = gen.LabelPos("Temp", vc1); + var vc = ToVcExpr(a, incarnations, gen); // check prover.AssertAxioms(); @@ -4576,25 +4568,6 @@ public FindSummaryPred(VCExpressionGenerator gen, int assertId) if (op == null) { - var lop = retnary.Op as VCExprLabelOp; - if (lop == null) return ret; - if (lop.pos) return ret; - if (!lop.label.Equals("@" + assertId.ToString())) return ret; - - //var subexpr = retnary[0] as VCExprNAry; - //if (subexpr == null) return ret; - //op = subexpr.Op as VCExprBoogieFunctionOp; - //if (op == null) return ret; - - var subexpr = retnary[0] as VCExprVar; - if (subexpr == null) return ret; - if (!subexpr.Name.StartsWith("AbstractHoudiniControl")) return ret; - - for (int i = 0; i < summaryPreds.Count; i++) - { - if (summaryPreds[i].Item3 == subexpr) - summaryPreds[i] = Tuple.Create(summaryPreds[i].Item1, true, summaryPreds[i].Item3, summaryPreds[i].Item4); - } return ret; } diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 18064bd0e..76b6c84b3 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -153,27 +153,19 @@ public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterf houdiniConstants.UnionWith(houdiniAssumeConstants); var exprGen = proverInterface.Context.ExprGen; - VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); + VCExpr controlFlowVariableExpr = exprGen.Integer(BigNum.ZERO); Dictionary label2absy; conjecture = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context); - if (!CommandLineOptions.Clo.UseLabels) { - VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); - VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))); - conjecture = exprGen.Implies(eqExpr, conjecture); - } + + VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); + VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))); + conjecture = exprGen.Implies(eqExpr, conjecture); Macro macro = new Macro(Token.NoToken, descriptiveName, new List(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false)); proverInterface.DefineMacro(macro, conjecture); conjecture = exprGen.Function(macro); - - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) { - handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, proverInterface.Context, program); - } - else { - handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, proverInterface.Context, program); - } - + handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, proverInterface.Context, program); } private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary currentAssignment) { diff --git a/Source/Provers/SMTLib/Inspector.cs b/Source/Provers/SMTLib/Inspector.cs index 13a2076ef..a395ba6a1 100644 --- a/Source/Provers/SMTLib/Inspector.cs +++ b/Source/Provers/SMTLib/Inspector.cs @@ -16,36 +16,6 @@ namespace Microsoft.Boogie.SMTLib { - internal class FindLabelsVisitor : TraversingVCExprVisitor { - public HashSet/*!*/ Labels = new HashSet(); - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNull(Labels)); - } - - - public static HashSet/*!*/ FindLabels(VCExpr/*!*/ expr) { - Contract.Requires(expr != null); - Contract.Ensures(cce.NonNull(Contract.Result/*!*/>())); - - FindLabelsVisitor visitor = new FindLabelsVisitor(); - visitor.Traverse(expr, true); - return visitor.Labels; - } - - protected override bool StandardResult(VCExpr node, bool arg) { - //Contract.Requires(node!=null); - VCExprNAry nary = node as VCExprNAry; - if (nary != null) { - VCExprLabelOp lab = nary.Op as VCExprLabelOp; - if (lab != null) { - Labels.Add(lab.label); - } - } - return true; - } - } - internal class Inspector { [Rep] protected readonly Process inspector; [Rep] readonly TextReader fromInspector; @@ -83,68 +53,10 @@ public Inspector(SMTLibProverOptions opts) } } - public void NewProblem(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) + public void NewProblem(string descriptiveName) { Contract.Requires(descriptiveName != null); - Contract.Requires(vc != null); - Contract.Requires(handler != null); - HashSet/*!*/ labels = FindLabelsVisitor.FindLabels(vc); - Contract.Assert(labels!=null); toInspector.WriteLine("PROBLEM " + descriptiveName); - toInspector.WriteLine("TOKEN BEGIN"); - foreach (string lab in labels) { - Contract.Assert(lab!=null); - string no = lab.Substring(1); - Absy absy = handler.Label2Absy(no); - - IToken tok = absy.tok; - AssertCmd assrt = absy as AssertCmd; - Block blk = absy as Block; - string val = tok.val; // might require computation, so cache it - if (val == "foo" || tok.filename == null) continue; // no token - - toInspector.Write("TOKEN "); - toInspector.Write(lab); - toInspector.Write(" "); - - if (assrt != null) { - toInspector.Write("ASSERT"); - string errData = assrt.ErrorData as string; - if (errData != null) { - val = errData; - } else if (assrt.ErrorMessage != null) { - val = assrt.ErrorMessage; - } - } else if (blk != null) { - toInspector.Write("BLOCK "); - toInspector.Write(blk.Label); - } else { - Contract.Assume( false); - } - if (val == null || val == "assert" || val == "ensures") { val = ""; } - - if (absy is LoopInitAssertCmd) { - val += " (loop entry)"; - } else if (absy is LoopInvMaintainedAssertCmd) { - val += " (loop body)"; - } else if (val.IndexOf("#VCCERR") >= 0) { - // skip further transformations - } else if (absy is AssertRequiresCmd) { - AssertRequiresCmd req = (AssertRequiresCmd)absy; - IToken t2 = req.Requires.tok; - string tval = t2.val; - if (tval == "requires") - tval = string.Format("{0}({1},{2}))", t2.filename, t2.line, t2.col); - string call = ""; - if (val != "call") call = " in call to " + val; - val = string.Format("precondition {0}{1}", tval, call); - } - - val = val.Replace("\r", "").Replace("\n", " "); - - toInspector.WriteLine(string.Format(" {0} {1} :@:{2}:@:{3}", tok.line, tok.col, tok.filename, val)); - } - toInspector.WriteLine("TOKEN END"); } public void StatsLine(string line) diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index b93414b1c..73861804b 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -435,7 +435,7 @@ public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler Process.PingPong(); // flush any errors if (Process.Inspector != null) - Process.Inspector.NewProblem(descriptiveName, vc, handler); + Process.Inspector.NewProblem(descriptiveName); } if (HasReset) { @@ -1283,7 +1283,7 @@ public override Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1) var result = Outcome.Undetermined; - if (Process == null) + if (Process == null || proverErrors.Count > 0) return result; try { @@ -1459,55 +1459,26 @@ public override Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1) if (globalResult == Outcome.Undetermined) globalResult = result; - if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory || result == Outcome.OutOfResource) { - IList xlabels; - if (CommandLineOptions.Clo.UseLabels) { - labels = GetLabelsInfo(); - if (labels == null) - { - xlabels = new string[] { }; - } - else - { - xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList(); - } - } - else if(CommandLineOptions.Clo.SIBoolControlVC) { - labels = new string[0]; - xlabels = labels; + if (result == Outcome.Invalid) { + Model model = GetErrorModel(); + if (CommandLineOptions.Clo.SIBoolControlVC) { + labels = new string[0]; } else { labels = CalculatePath(handler.StartingProcId()); - xlabels = labels; } - Model model = (result == Outcome.TimeOut || result == Outcome.OutOfMemory || result == Outcome.OutOfResource) ? null : - GetErrorModel(); - handler.OnModel(xlabels, model, result); + handler.OnModel(labels, model, result); } if (labels == null || !labels.Any() || errorsLeft == 0) break; - } finally { + } + finally { if (popLater) { SendThisVC("(pop 1)"); } } - if (CommandLineOptions.Clo.UseLabels) { - var negLabels = labels.Where(l => l.StartsWith("@")).ToArray(); - var posLabels = labels.Where(l => !l.StartsWith("@")); - Func lbl = (s) => SMTLibNamer.QuoteId(Namer.LabelVar(s)); - if (!options.MultiTraces) - posLabels = Enumerable.Empty(); - var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray(); - string expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")"); ; - if (!conjuncts.Any()) - { - expr = "false"; - } - SendThisVC("(assert " + expr + ")"); - SendCheckSat(); - } - else { + { string source = labels[labels.Length - 2]; string target = labels[labels.Length - 1]; SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + "))))"); @@ -2859,10 +2830,5 @@ protected virtual SMTLibProcessTheoremProver SpawnProver(ProverOptions options, return new SMTLibProcessTheoremProver(options, gen, ctx); } - - public override bool SupportsLabels(ProverOptions options) - { - return ((SMTLibProverOptions)options).SupportsLabels; - } } } diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 00ac175a0..7a657e433 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -602,37 +602,6 @@ public bool VisitDistinctOp(VCExprNAry node, LineariserOptions options) return true; } - public bool VisitLabelOp(VCExprNAry node, LineariserOptions options) - { - if (ExprLineariser.UnderQuantifier > 0 && !options.LabelsBelowQuantifiers) { - ExprLineariser.Linearise(node[0], options); - return true; - } - - var op = (VCExprLabelOp)node.Op; - - if (CommandLineOptions.Clo.UseLabels) - { - // Z3 extension - //wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label)); - wr.Write("(! "); - } - - if(!options.LabelsBelowQuantifiers) - wr.Write("({0} {1} ", op.pos ? "and" : "or", SMTLibNamer.QuoteId(ExprLineariser.Namer.LabelVar(op.label))); - - ExprLineariser.Linearise(node[0], options); - - - if (!options.LabelsBelowQuantifiers) - wr.Write(")"); - - if (CommandLineOptions.Clo.UseLabels) - wr.Write(" :{0} {1})", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(ExprLineariser.Namer.LabelName(op.label))); - - return true; - } - public bool VisitSelectOp(VCExprNAry node, LineariserOptions options) { var name = SimplifyLikeExprLineariser.SelectOpName(node); diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index de5ad1099..68305f30e 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -37,15 +37,13 @@ public class SMTLibProverOptions : ProverOptions public SolverKind Solver = SolverKind.Z3; public List SmtOptions = new List(); public List SolverArguments = new List(); - public bool MultiTraces = false; public string Logic = null; // Z3 specific (at the moment; some of them make sense also for other provers) public string Inspector = null; public bool ProduceModel() { - return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini || CommandLineOptions.Clo.UseProverEvaluate || - ExpectingModel(); + return CommandLineOptions.Clo.ExplainHoudini || CommandLineOptions.Clo.UseProverEvaluate || ExpectingModel(); } public bool ExpectingModel() @@ -91,7 +89,7 @@ protected override bool Parse(string opt) AddSolverArgument(opt.Substring(2)); return true; } - + string SolverStr = null; if (ParseString(opt, "SOLVER", ref SolverStr)) { switch (SolverStr.ToLower()) { @@ -109,7 +107,6 @@ protected override bool Parse(string opt) } return - ParseBool(opt, "MULTI_TRACES", ref MultiTraces) || ParseBool(opt, "USE_WEIGHTS", ref UseWeights) || ParseString(opt, "INSPECTOR", ref Inspector) || ParseString(opt, "LOGIC", ref Logic) || @@ -153,11 +150,10 @@ public override string Help USE_WEIGHTS= Pass :weight annotations on quantified formulas (default: true) VERBOSITY= 1 - print prover output (default: 0) O:= Pass (set-option : ) to the SMT solver. -C: Pass to the SMT on the command line. +C: Pass to the SMT solver on the command line. Z3-specific options: ~~~~~~~~~~~~~~~~~~~~ -MULTI_TRACES= Report errors with multiple paths leading to the same assertion. INSPECTOR= Use the specified Z3Inspector binary. "; } diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 96dd9e99c..2f44b8daf 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -77,11 +77,6 @@ private HashSet/*!*/ KnownSelectFunctions get { return _KnownSelectFunctions.Peek(); } } - private HashSet KnownLBL - { - get { return _KnownLBL.Peek(); } - } - // ------ private readonly Stack/*!*/> _KnownFunctions = new Stack>(); private readonly Stack/*!*/> _KnownVariables = new Stack>(); @@ -89,9 +84,8 @@ private HashSet KnownLBL private readonly Stack/*!*/> _KnownTypes = new Stack>(); private readonly Stack/*!*/> _KnownStoreFunctions = new Stack>(); private readonly Stack/*!*/> _KnownSelectFunctions = new Stack>(); - private readonly Stack> _KnownLBL = new Stack>(); - - // lets RPFP checker capture decls + + // lets RPFP checker capture decls public abstract class DeclHandler { public abstract void VarDecl(VCExprVar v); public abstract void FuncDecl(Function f); @@ -110,7 +104,6 @@ private void InitializeKnownDecls() _KnownTypes.Push(new HashSet()); _KnownStoreFunctions.Push(new HashSet()); _KnownSelectFunctions.Push(new HashSet()); - _KnownLBL.Push(new HashSet()); } public void Reset() @@ -120,7 +113,6 @@ public void Reset() _KnownTypes.Clear(); _KnownStoreFunctions.Clear(); _KnownSelectFunctions.Clear(); - _KnownLBL.Clear(); AllDecls.Clear(); IncDecls.Clear(); InitializeKnownDecls(); @@ -134,7 +126,6 @@ public void Push() _KnownTypes.Push(new HashSet(_KnownTypes.Peek())); _KnownStoreFunctions.Push(new HashSet(_KnownStoreFunctions.Peek())); _KnownSelectFunctions.Push(new HashSet(_KnownSelectFunctions.Peek())); - _KnownLBL.Push(new HashSet(_KnownLBL.Peek())); } public void Pop() @@ -145,7 +136,6 @@ public void Pop() _KnownTypes.Pop(); _KnownStoreFunctions.Pop(); _KnownSelectFunctions.Pop(); - _KnownLBL.Pop(); } public void SetNamer(UniqueNamer namer) @@ -250,13 +240,6 @@ public override bool Visit(VCExprNAry node, bool arg) { if (declHandler != null) declHandler.FuncDecl(f); } KnownFunctions.Add(f); - } else { - var lab = node.Op as VCExprLabelOp; - if (lab != null && !KnownLBL.Contains(lab.label)) { - KnownLBL.Add(lab.label); - var name = SMTLibNamer.QuoteId(Namer.LabelVar(lab.label)); - AddDeclaration("(declare-fun " + name + " () Bool)"); - } } } diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index 5139bec0e..975a8d609 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -857,17 +857,6 @@ public bool VisitDistinctOp(VCExprNAry node, LineariserOptions options) { return true; } - public bool VisitLabelOp(VCExprNAry node, LineariserOptions options) { - //Contract.Requires(options != null); - //Contract.Requires(node != null); - VCExprLabelOp op = (VCExprLabelOp)node.Op; - Contract.Assert(op != null); - wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label)); - ExprLineariser.Linearise(node[0], options); - wr.Write(")"); - return true; - } - public bool VisitSelectOp(VCExprNAry node, LineariserOptions options) { //Contract.Requires(options != null); //Contract.Requires(node != null); diff --git a/Source/VCExpr/TermFormulaFlattening.cs b/Source/VCExpr/TermFormulaFlattening.cs index c41500242..c0be7bc42 100644 --- a/Source/VCExpr/TermFormulaFlattening.cs +++ b/Source/VCExpr/TermFormulaFlattening.cs @@ -180,8 +180,7 @@ public override VCExpr Visit(VCExprNAry node, FlattenerState state){ state = state.EnterTerm; if (!node.Op.Equals(VCExpressionGenerator.AndOp) && - !node.Op.Equals(VCExpressionGenerator.OrOp) && - !(node.Op is VCExprLabelOp)) + !node.Op.Equals(VCExpressionGenerator.OrOp)) // standard is to set the polarity to 0 (fits most operators) return base.Visit(node, state.ZeroPolarity); diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 74d16f7c9..c667903b9 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -1359,14 +1359,7 @@ public override VCExpr VisitDistinctOp(VCExprNAry node, VariableBindings binding Contract.Ensures(Contract.Result() != null); return CastArgumentsToOldType(node, bindings, 0); } - public override VCExpr VisitLabelOp(VCExprNAry node, VariableBindings bindings) { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - // argument of the label operator should always be a formula - // (at least for Simplify ... should this be ensured at a later point?) - return CastArguments(node, Type.Bool, bindings, Eraser.Polarity); - } + public override VCExpr VisitIfThenElseOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index a39375b0a..3a63d06ae 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -605,31 +605,6 @@ public VCExpr Store(List allArgs, List/*!*/ typeArgs) { allArgs, typeArgs); } - - // Labels - - public VCExprLabelOp LabelOp(bool pos, string l) { - Contract.Requires(l != null); - Contract.Ensures(Contract.Result() != null); - return new VCExprLabelOp(pos, l); - } - - public VCExpr LabelNeg(string label, VCExpr e) { - Contract.Requires(e != null); - Contract.Requires(label != null); - Contract.Ensures(Contract.Result() != null); - if (e.Equals(True)) { - return e; // don't bother putting negative labels around True (which will expose the True to further peephole optimizations) - } - return Function(LabelOp(false, label), e); - } - public VCExpr LabelPos(string label, VCExpr e) { - Contract.Requires(e != null); - Contract.Requires(label != null); - Contract.Ensures(Contract.Result() != null); - return Function(LabelOp(true, label), e); - } - // Quantifiers public VCExpr Quantify(Quantifier quan, List/*!*/ typeParams, List/*!*/ vars, List/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) { @@ -1476,60 +1451,6 @@ public override Result Accept } } - public class VCExprLabelOp : VCExprOp { - public override int Arity { - get { - return 1; - } - } - public override int TypeParamArity { - get { - return 0; - } - } - public override Type InferType(List args, List/*!*/ typeArgs) { - //Contract.Requires(cce.NonNullElements(typeArgs)); - //Contract.Requires(cce.NonNullElements(args)); - Contract.Ensures(Contract.Result() != null); - return args[0].Type; - } - - public readonly bool pos; - public readonly string label; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(label != null); - } - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object that) { - if (Object.ReferenceEquals(this, that)) - return true; - if (that is VCExprLabelOp) { - VCExprLabelOp/*!*/ thatOp = (VCExprLabelOp)that; - return this.pos == thatOp.pos && this.label.Equals(thatOp.label); - } - return false; - } - [Pure] - public override int GetHashCode() { - return (pos ? 9817231 : 7198639) + label.GetHashCode(); - } - - internal VCExprLabelOp(bool pos, string l) { - Contract.Requires(l != null); - this.pos = pos; - this.label = pos ? "+" + l : "@" + l; - } - public override Result Accept - (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { - //Contract.Requires(visitor != null); - //Contract.Requires(expr != null); - return visitor.VisitLabelOp(expr, arg); - } - } - public class VCExprSelectOp : VCExprOp { private readonly int MapArity; private readonly int MapTypeParamArity; diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs index 8e590a458..8f8e5065a 100644 --- a/Source/VCExpr/VCExprASTPrinter.cs +++ b/Source/VCExpr/VCExprASTPrinter.cs @@ -225,13 +225,6 @@ public bool VisitDistinctOp(VCExprNAry node, TextWriter wr) { //Contract.Requires(node != null); return PrintNAry("Distinct", node, wr); } - public bool VisitLabelOp(VCExprNAry node, TextWriter wr) { - //Contract.Requires(wr != null); - //Contract.Requires(node != null); - VCExprLabelOp/*!*/ op = (VCExprLabelOp)node.Op; - Contract.Assert(op != null); - return PrintNAry("Label " + op.label, node, wr); - } public bool VisitSelectOp(VCExprNAry node, TextWriter wr) { //Contract.Requires(wr != null); //Contract.Requires(node != null); diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 846e43308..b563831bf 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -65,7 +65,6 @@ public interface IVCExprOpVisitor { Result VisitOrOp(VCExprNAry node, Arg arg); Result VisitImpliesOp(VCExprNAry node, Arg arg); Result VisitDistinctOp(VCExprNAry node, Arg arg); - Result VisitLabelOp(VCExprNAry node, Arg arg); Result VisitSelectOp(VCExprNAry node, Arg arg); Result VisitStoreOp(VCExprNAry node, Arg arg); Result VisitFloatAddOp(VCExprNAry node, Arg arg); @@ -139,11 +138,6 @@ public Result VisitDistinctOp(VCExprNAry node, Arg arg) { throw new NotImplementedException(); } - public Result VisitLabelOp(VCExprNAry node, Arg arg) { - Contract.Requires(node != null); - throw new NotImplementedException(); - } - public Result VisitSelectOp(VCExprNAry node, Arg arg) { Contract.Requires(node != null); throw new NotImplementedException(); @@ -1501,10 +1495,6 @@ public virtual Result VisitDistinctOp(VCExprNAry node, Arg arg) { //Contract.Requires(node != null); return StandardResult(node, arg); } - public virtual Result VisitLabelOp(VCExprNAry node, Arg arg) { - //Contract.Requires(node != null); - return StandardResult(node, arg); - } public virtual Result VisitSelectOp(VCExprNAry node, Arg arg) { //Contract.Requires(node != null); return StandardResult(node, arg); diff --git a/Source/VCGeneration/ExprExtensions.cs b/Source/VCGeneration/ExprExtensions.cs index 5e0dcf8e7..653d6c655 100644 --- a/Source/VCGeneration/ExprExtensions.cs +++ b/Source/VCGeneration/ExprExtensions.cs @@ -82,21 +82,9 @@ public static DeclKind GetKind(this FuncDecl f) return DeclKind.And; if (f == VCExpressionGenerator.ImpliesOp) return DeclKind.Implies; - if (f is VCExprLabelOp) - return DeclKind.Label; return DeclKind.Other; } - public static bool IsLabel(this Term t) - { - return (t is VCExprNAry) && (GetAppDecl(t) is VCExprLabelOp); - } - - public static string LabelName(this Term t) - { - return (GetAppDecl(t) as VCExprLabelOp).label; - } - public static Sort GetSort(this Term t) { return t.Type; diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 6499da263..89185d5ce 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -870,10 +870,7 @@ private Term ExtractSmallerVCsRec(TermDict< Term> memo, Term t, List small } } normal: - Term newlbl = null; - if (lhs.IsLabel() && lhs.GetAppArgs()[0] == ctx.MkTrue()) - newlbl = lhs; - res = ctx.MkImplies(lhs,ExtractSmallerVCsRec(memo,t.GetAppArgs()[1],small,newlbl)); + res = ctx.MkImplies(lhs,ExtractSmallerVCsRec(memo,t.GetAppArgs()[1],small,null)); } else if (f.GetKind() == DeclKind.And) { @@ -1356,10 +1353,6 @@ public class CyclicLiveVariableAnalysis : Microsoft.Boogie.LiveVariableAnalysis public void Generate() { - - var oldDagOption = CommandLineOptions.Clo.vcVariety; - CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Dag; - // MarkAllFunctionImplementationsInline(); // This is for SMACK, which goes crazy with functions // Run live variable analysis (TODO: should this be here?) @@ -1499,8 +1492,6 @@ public void Generate() // save some information for debugging purposes // TODO rpfp.ls.SetAnnotationInfo(annotationInfo); - - CommandLineOptions.Clo.vcVariety = oldDagOption; } @@ -1641,12 +1632,6 @@ public void FindLabelsRec(HashSet memo, Term t, Dictionary r { if (memo.Contains(t)) return; - if (t.IsLabel()) - { - string l = t.LabelName(); - if (!res.ContainsKey(l)) - res.Add(l, t.GetAppArgs()[0]); - } if (t.GetKind() == TermKind.App) { var args = t.GetAppArgs(); diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 2228f26e2..d10ef84c8 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -22,8 +22,6 @@ public class StratifiedVC { // boolControlVC (block -> its bool variable) public Dictionary blockToControlVar; - // While using labels (block -> its label) - public Dictionary block2label; public Dictionary> callSites; public Dictionary> recordProcCallSites; @@ -67,13 +65,6 @@ public StratifiedVC(StratifiedInliningInfo siInfo, HashSet procCalls) { blockToControlVar.Add(tup.Key, substDict[tup.Value]); } - // labels - if (info.label2absy != null) - { - block2label = new Dictionary(); - vcexpr = RenameVCExprLabels.Apply(vcexpr, info.vcgen.prover.VCExprGen, info.label2absy, block2label); - } - if(procCalls != null) vcexpr = RemoveProcedureCalls.Apply(vcexpr, info.vcgen.prover.VCExprGen, procCalls); @@ -96,9 +87,7 @@ public StratifiedVC(StratifiedInliningInfo siInfo, HashSet procCalls) { public VCExpr MustReach(Block block) { - Contract.Assert(!CommandLineOptions.Clo.UseLabels); - - // This information is computed lazily + // This information is computed lazily if (mustReachBindings == null) { var vcgen = info.vcgen; @@ -173,69 +162,6 @@ public override string ToString() } } - // Rename all labels in a VC to (globally) fresh labels - class RenameVCExprLabels : MutatingVCExprVisitor - { - Dictionary label2absy; - Dictionary absy2newlabel; - static int counter = 11; - - RenameVCExprLabels(VCExpressionGenerator gen, Dictionary label2absy, Dictionary absy2newlabel) - : base(gen) - { - this.label2absy = label2absy; - this.absy2newlabel = absy2newlabel; - } - - public static VCExpr Apply(VCExpr expr, VCExpressionGenerator gen, Dictionary label2absy, Dictionary absy2newlabel) - { - return (new RenameVCExprLabels(gen, label2absy, absy2newlabel)).Mutate(expr, true); - } - - // Finds labels and changes them to a globally unique label: - protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, - List/*!*/ newSubExprs, - bool changed, - bool arg) - { - Contract.Ensures(Contract.Result() != null); - - VCExpr ret; - if (changed) - ret = Gen.Function(originalNode.Op, - newSubExprs, originalNode.TypeArguments); - else - ret = originalNode; - - VCExprLabelOp lop = originalNode.Op as VCExprLabelOp; - if (lop == null) return ret; - if (!(ret is VCExprNAry)) return ret; - VCExprNAry retnary = (VCExprNAry)ret; - - // remove the sign - var nosign = 0; - if (!Int32.TryParse(lop.label.Substring(1), out nosign)) - return ret; - - if (!label2absy.ContainsKey(nosign)) - return ret; - - string newLabel = "SI" + counter.ToString(); - counter++; - absy2newlabel[label2absy[nosign]] = newLabel; - - if (lop.pos) - { - return Gen.LabelPos(newLabel, retnary[0]); - } - else - { - return Gen.LabelNeg(newLabel, retnary[0]); - } - - } - } - // Remove the uninterpreted function calls that substitute procedure calls class RemoveProcedureCalls : MutatingVCExprVisitor { @@ -490,15 +416,6 @@ public void GenerateVCBoolControl() continue; } var expr = translator.Translate(acmd.Expr); - // Label the assume if it is a procedure call - NAryExpr naryExpr = acmd.Expr as NAryExpr; - if (naryExpr != null && naryExpr.Fun is FunctionCall) - { - var id = acmd.UniqueId; - label2absy[id] = acmd; - expr = gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), expr); - } - c = gen.AndSimp(c, expr); } @@ -588,11 +505,8 @@ public void GenerateVC() { var exprGen = proverInterface.Context.ExprGen; var translator = proverInterface.Context.BoogieExprTranslator; - VCExpr controlFlowVariableExpr = null; - if (!CommandLineOptions.Clo.UseLabels) { - controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int)); - controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable); - } + controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int)); + VCExpr controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable); vcgen.InstrumentCallSites(impl); @@ -1907,75 +1821,12 @@ public Dictionary getLabel2absy() { //Contract.Requires(originalNode != null); //Contract.Requires(cce.NonNullElements(newSubExprs)); Contract.Ensures(Contract.Result() != null); - - VCExpr ret; + if (changed) - ret = Gen.Function(originalNode.Op, + return Gen.Function(originalNode.Op, newSubExprs, originalNode.TypeArguments); else - ret = originalNode; - - VCExprLabelOp lop = originalNode.Op as VCExprLabelOp; - if (lop == null) return ret; - if (!(ret is VCExprNAry)) return ret; - - VCExprNAry retnary = (VCExprNAry)ret; - Contract.Assert(retnary != null); - string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...) - if (lop.label.Substring(1).StartsWith(prefix)) { - int id = Int32.Parse(lop.label.Substring(prefix.Length + 1)); - Dictionary label2absy = getLabel2absy(); - Absy cmd = label2absy[id] as Absy; - //label2absy.Remove(id); - - Contract.Assert(cmd != null); - AssumeCmd acmd = cmd as AssumeCmd; - Contract.Assert(acmd != null); - NAryExpr naryExpr = acmd.Expr as NAryExpr; - Contract.Assert(naryExpr != null); - - string calleeName = naryExpr.Fun.FunctionName; - - VCExprNAry callExpr = retnary[0] as VCExprNAry; - - if (implName2StratifiedInliningInfo.ContainsKey(calleeName)) { - Contract.Assert(callExpr != null); - int candidateId = GetNewId(callExpr); - boogieExpr2Id[new BoogieCallExpr(naryExpr, currInlineCount)] = candidateId; - candidateParent[candidateId] = currInlineCount; - candiate2block2controlVar[candidateId] = new Dictionary(); - - string label = GetLabel(candidateId); - var unique_call_id = QKeyValue.FindIntAttribute(acmd.Attributes, "si_unique_call", -1); - if (unique_call_id != -1) - candidate2callId[candidateId] = unique_call_id; - - //return Gen.LabelPos(label, callExpr); - return Gen.LabelPos(label, id2ControlVar[candidateId]); - } - else if (calleeName.StartsWith(recordProcName)) { - Contract.Assert(callExpr != null); - Debug.Assert(callExpr.Length == 1); - Debug.Assert(callExpr[0] != null); - recordExpr2Var[new BoogieCallExpr(naryExpr, currInlineCount)] = callExpr[0]; - return callExpr; - } - else { - // callExpr can be null; this happens when the FunctionCall was on a - // pure function (not procedure) and the function got inlined - return retnary[0]; - } - } - - // Else, rename label - string newLabel = RenameAbsyLabel(lop.label); - if (lop.pos) { - return Gen.LabelPos(newLabel, retnary[0]); - } - else { - return Gen.LabelNeg(newLabel, retnary[0]); - } - + return originalNode; } // Upgrades summaryTemp to summaryCandidates by matching ensure clauses with @@ -2059,25 +1910,11 @@ public void Clear() { bool arg) { //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null); Contract.Ensures(Contract.Result() != null); - - VCExpr ret; + if (changed) - ret = Gen.Function(originalNode.Op, newSubExprs, originalNode.TypeArguments); + return Gen.Function(originalNode.Op, newSubExprs, originalNode.TypeArguments); else - ret = originalNode; - - VCExprLabelOp lop = originalNode.Op as VCExprLabelOp; - if (lop == null) return ret; - if (!(ret is VCExprNAry)) return ret; - - string prefix = "si_fcall_"; // from FCallHandler::GetLabel - if (lop.label.Substring(1).StartsWith(prefix)) { - int id = Int32.Parse(lop.label.Substring(prefix.Length + 1)); - if (subst.ContainsKey(id)) { - return subst[id]; - } - } - return ret; + return originalNode; } } // end FCallInliner diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index beca32a00..d50843bfd 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -299,18 +299,15 @@ bool CheckUnreachable(Block cur, List seq) lock (ch) { var exprGen = ch.TheoremProver.Context.ExprGen; - VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); + VCExpr controlFlowVariableExpr = exprGen.Integer(BigNum.ZERO); VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch.TheoremProver.Context); Contract.Assert(vc != null); - - if (!CommandLineOptions.Clo.UseLabels) - { - VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); - VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))); - vc = exprGen.Implies(eqExpr, vc); - } - + + VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); + VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))); + vc = exprGen.Implies(eqExpr, vc); + impl.Blocks = backup; if (CommandLineOptions.Clo.TraceVerify) @@ -1388,26 +1385,15 @@ public void BeginCheck(Checker checker, VerifierCallback callback, ModelViewInfo bet.SetCodeExprConverter(cc.CodeExprToVerificationCondition); var exprGen = ctx.ExprGen; - VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); + VCExpr controlFlowVariableExpr = exprGen.Integer(BigNum.ZERO); VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context); Contract.Assert(vc != null); - - if (!CommandLineOptions.Clo.UseLabels) - { - VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); - VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))); - vc = exprGen.Implies(eqExpr, vc); - } - - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) - { - reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program); - } - else - { - reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, this.Checker.TheoremProver.Context, parent.program); - } + + VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); + VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))); + vc = exprGen.Implies(eqExpr, vc); + reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, this.Checker.TheoremProver.Context, parent.program); if (CommandLineOptions.Clo.TraceVerify && no >= 0) { @@ -1495,7 +1481,7 @@ public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, Hashtable block vcgen.AddBlocksBetween(codeExpr.Blocks); Dictionary gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new List(), new ModelViewInfo(codeExpr)); int ac; // computed, but then ignored for this CodeExpr - VCExpr startCorrect = VCGen.LetVCIterative(codeExpr.Blocks, null, label2absy, ctx, out ac, isPositiveContext); + VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks, null, label2absy, ctx, out ac, isPositiveContext); VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect); if (vcgen.CurrentLocalVariables.Count != 0) { @@ -1544,41 +1530,10 @@ public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariable VCExpr vc; int assertionCount; - switch (CommandLineOptions.Clo.vcVariety) { - case CommandLineOptions.VCVariety.Structured: - vc = VCViaStructuredProgram(impl, label2absy, proverContext, out assertionCount); - break; - case CommandLineOptions.VCVariety.Block: - vc = FlatBlockVC(impl, label2absy, false, false, false, proverContext, out assertionCount); - break; - case CommandLineOptions.VCVariety.BlockReach: - vc = FlatBlockVC(impl, label2absy, false, true, false, proverContext, out assertionCount); - break; - case CommandLineOptions.VCVariety.Local: - vc = FlatBlockVC(impl, label2absy, true, false, false, proverContext, out assertionCount); - break; - case CommandLineOptions.VCVariety.BlockNested: - vc = NestedBlockVC(impl, label2absy, false, proverContext, out assertionCount); - break; - case CommandLineOptions.VCVariety.BlockNestedReach: - vc = NestedBlockVC(impl, label2absy, true, proverContext, out assertionCount); - break; - case CommandLineOptions.VCVariety.Dag: - if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags || CommandLineOptions.Clo.FixedPointEngine != null) { - vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/**/(), proverContext, out assertionCount); - } else { - vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, proverContext, out assertionCount); - } - break; - case CommandLineOptions.VCVariety.DagIterative: - vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount); - break; - case CommandLineOptions.VCVariety.Doomed: - vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount); - break; - default: - Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected enumeration value + if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags || CommandLineOptions.Clo.FixedPointEngine != null) { + vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/**/(), proverContext, out assertionCount); + } else { + vc = LetVC(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount); } CumulativeAssertionCount += assertionCount; return vc; @@ -2148,80 +2103,16 @@ public override void OnProverWarning(string msg) { } } - public class ErrorReporterLocal : ErrorReporter { - public ErrorReporterLocal(Dictionary/*!*/ gotoCmdOrigins, - Dictionary/*!*/ label2absy, - List/*!*/ blocks, - Dictionary/*!*/ incarnationOriginMap, - VerifierCallback/*!*/ callback, - ModelViewInfo mvInfo, - ProverContext/*!*/ context, - Program/*!*/ program) - : base(gotoCmdOrigins, label2absy, blocks, incarnationOriginMap, callback, mvInfo, context, program) // here for aesthetic purposes //TODO: Maybe nix? + private void RecordCutEdge(Dictionary> edgesCut, Block from, Block to) + { + if (edgesCut != null) { - Contract.Requires(gotoCmdOrigins != null); - Contract.Requires(label2absy != null); - Contract.Requires(cce.NonNullElements(blocks)); - Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap)); - Contract.Requires(callback != null); - Contract.Requires(context != null); - Contract.Requires(program != null); - } - - public override void OnModel(IList/*!*/ labels, Model model, ProverInterface.Outcome proverOutcome) { - //Contract.Requires(cce.NonNullElements(labels)); - // We ignore the error model here for enhanced error message purposes. - // It is only printed to the command line. - if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) { - if (CommandLineOptions.Clo.PrintErrorModelFile != null) { - model.Write(ErrorReporter.ModelWriter); - ErrorReporter.ModelWriter.Flush(); - } - } - List traceNodes = new List(); - List assertNodes = new List(); - foreach (string s in labels) { - Contract.Assert(s != null); - Absy node = Label2Absy(s); - if (node is Block) { - Block b = (Block)node; - traceNodes.Add(b); - } else { - AssertCmd a = (AssertCmd)node; - assertNodes.Add(a); - } - } - Contract.Assert(assertNodes.Count > 0); - Contract.Assert(traceNodes.Count == assertNodes.Count); - - foreach (AssertCmd a in assertNodes) { - // find the corresponding Block (assertNodes.Count is likely to be 1, or small in any case, so just do a linear search here) - foreach (Block b in traceNodes) { - if (b.Cmds.Contains(a)) { - List trace = new List(); - trace.Add(b); - Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, model, MvInfo, context); - callback.OnCounterexample(newCounterexample, null); - goto NEXT_ASSERT; - } - } - Contract.Assert(false); - throw new cce.UnreachableException(); // there was no block that contains the assert - NEXT_ASSERT: { - } - } + if (!edgesCut.ContainsKey(from)) + edgesCut.Add(from, new List()); + edgesCut[from].Add(to); } } - private void RecordCutEdge(Dictionary> edgesCut, Block from, Block to){ - if (edgesCut != null) - { - if (!edgesCut.ContainsKey(from)) - edgesCut.Add(from, new List()); - edgesCut[from].Add(to); - } - } - public void ConvertCFG2DAG(Implementation impl, Dictionary> edgesCut = null, int taskID = -1) { Contract.Requires(impl != null); @@ -2850,7 +2741,7 @@ public Dictionary PassifyImpl(Implementation impl, out M if (CommandLineOptions.Clo.RemoveEmptyBlocks){ #region Get rid of empty blocks { - RemoveEmptyBlocksIterative(impl.Blocks); + RemoveEmptyBlocks(impl.Blocks); impl.PruneUnreachableBlocks(); } #endregion Get rid of empty blocks @@ -3167,7 +3058,7 @@ protected CalleeCounterexampleInfo extractLoopTraceRec( var loc = new TraceLocation(numBlock, numInstr); if (!cex.calleeCounterexamples.ContainsKey(loc)) { - if (getCallee(cex.getTraceCmd(loc), inlinedProcs) != null) callCnt++; + if (GetCallee(cex.getTraceCmd(loc), inlinedProcs) != null) callCnt++; continue; } string callee = cex.getCalledProcName(cex.getTraceCmd(loc)); @@ -3193,7 +3084,7 @@ protected CalleeCounterexampleInfo extractLoopTraceRec( } else { - var origLoc = new TraceLocation(ret.Trace.Count - 1, getCallCmdPosition(origBlock, callCnt, inlinedProcs, callee)); + var origLoc = new TraceLocation(ret.Trace.Count - 1, GetCallCmdPosition(origBlock, callCnt, inlinedProcs, callee)); ret.calleeCounterexamples.Add(origLoc, origTrace); callCnt++; } @@ -3205,13 +3096,13 @@ protected CalleeCounterexampleInfo extractLoopTraceRec( // return the position of the i^th CallCmd in the block (count only those Calls that call a procedure in inlinedProcs). // Assert failure if there isn't any. // Assert that the CallCmd found calls "callee" - private int getCallCmdPosition(Block block, int i, HashSet inlinedProcs, string callee) + private int GetCallCmdPosition(Block block, int i, HashSet inlinedProcs, string callee) { Debug.Assert(i >= 1); for (int pos = 0; pos < block.Cmds.Count; pos++) { Cmd cmd = block.Cmds[pos]; - string procCalled = getCallee(cmd, inlinedProcs); + string procCalled = GetCallee(cmd, inlinedProcs); if (procCalled != null) { @@ -3228,7 +3119,7 @@ private int getCallCmdPosition(Block block, int i, HashSet inlinedProcs, return -1; } - private string getCallee(Cmd cmd, HashSet inlinedProcs) + private string GetCallee(Cmd cmd, HashSet inlinedProcs) { string procCalled = null; if (cmd is CallCmd) @@ -3439,23 +3330,7 @@ public static Counterexample AssertCmdToCloneCounterexample(AssertCmd assrt, Cou return cc; } - static VCExpr LetVC(Block startBlock, - VCExpr controlFlowVariableExpr, - Dictionary label2absy, - ProverContext proverCtxt, - out int assertionCount) { - Contract.Requires(startBlock != null); - Contract.Requires(proverCtxt != null); - - Contract.Ensures(Contract.Result() != null); - - Hashtable/**/ blockVariables = new Hashtable/**/(); - List bindings = new List(); - VCExpr startCorrect = LetVC(startBlock, controlFlowVariableExpr, label2absy, blockVariables, bindings, proverCtxt, out assertionCount); - return proverCtxt.ExprGen.Let(bindings, startCorrect); - } - - static VCExpr LetVCIterative(List blocks, + static VCExpr LetVC(List blocks, VCExpr controlFlowVariableExpr, Dictionary label2absy, ProverContext proverCtxt, @@ -3531,73 +3406,6 @@ static VCExpr LetVCIterative(List blocks, return proverCtxt.ExprGen.Let(bindings, blockVariables[blocks[0]]); } - static VCExpr LetVC(Block block, - VCExpr controlFlowVariableExpr, - Dictionary label2absy, - Hashtable/**/ blockVariables, - List/*!*/ bindings, - ProverContext proverCtxt, - out int assertionCount) - { - Contract.Requires(block != null); - Contract.Requires(blockVariables!= null); - Contract.Requires(cce.NonNullElements(bindings)); - Contract.Requires(proverCtxt != null); - - Contract.Ensures(Contract.Result() != null); - - assertionCount = 0; - - VCExpressionGenerator gen = proverCtxt.ExprGen; - Contract.Assert(gen != null); - VCExprVar v = (VCExprVar)blockVariables[block]; - if (v == null) { - /* - * For block A (= block), generate: - * LET_binding A_correct = wp(A_body, (/\ S \in Successors(A) :: S_correct)) - * with the side effect of adding the let bindings to "bindings" for any - * successor not yet visited. - */ - VCExpr SuccCorrect; - GotoCmd gotocmd = block.TransferCmd as GotoCmd; - if (gotocmd == null) { - ReturnExprCmd re = block.TransferCmd as ReturnExprCmd; - if (re == null) { - SuccCorrect = VCExpressionGenerator.True; - } else { - SuccCorrect = proverCtxt.BoogieExprTranslator.Translate(re.Expr); - } - } else { - Contract.Assert( gotocmd.labelTargets != null); - List SuccCorrectVars = new List(gotocmd.labelTargets.Count); - foreach (Block successor in gotocmd.labelTargets) { - Contract.Assert(successor != null); - int ac; - VCExpr s = LetVC(successor, controlFlowVariableExpr, label2absy, blockVariables, bindings, proverCtxt, out ac); - assertionCount += ac; - if (controlFlowVariableExpr != null) - { - VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(block.UniqueId))); - VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successor.UniqueId))); - s = gen.Implies(controlTransferExpr, s); - } - SuccCorrectVars.Add(s); - } - SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars); - } - - - VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr); - VCExpr vc = Wlp.Block(block, SuccCorrect, context); - assertionCount += context.AssertionCount; - - v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool); - bindings.Add(gen.LetBinding(v, vc)); - blockVariables.Add(block, v); - } - return v; - } - static VCExpr DagVC(Block block, VCExpr controlFlowVariableExpr, Dictionary label2absy, @@ -3654,293 +3462,10 @@ static VCExpr DagVC(Block block, return vc; } - static VCExpr FlatBlockVC(Implementation impl, - Dictionary label2absy, - bool local, bool reach, bool doomed, - ProverContext proverCtxt, - out int assertionCount) - { - Contract.Requires(impl != null); - Contract.Requires(label2absy != null); - Contract.Requires(proverCtxt != null); - Contract.Requires( !local || !reach); // "reach" must be false for local - - VCExpressionGenerator gen = proverCtxt.ExprGen; - Contract.Assert(gen != null); - Hashtable/* Block --> VCExprVar */ BlkCorrect = BlockVariableMap(impl.Blocks, "_correct", gen); - Hashtable/* Block --> VCExprVar */ BlkReached = reach ? BlockVariableMap(impl.Blocks, "_reached", gen) : null; - - List blocks = impl.Blocks; - Contract.Assert(blocks != null); - // block sorting is now done on the VCExpr - // if (!local && (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).NeedsBlockSorting) { - // blocks = SortBlocks(blocks); - // } - - VCExpr proofObligation; - if (!local) { - proofObligation = cce.NonNull((VCExprVar)BlkCorrect[impl.Blocks[0]]); - } else { - List conjuncts = new List(blocks.Count); - foreach (Block b in blocks) {Contract.Assert(b != null); - VCExpr v = cce.NonNull((VCExprVar)BlkCorrect[b]); - conjuncts.Add(v); - } - proofObligation = gen.NAry(VCExpressionGenerator.AndOp, conjuncts); - } - - VCContext context = new VCContext(label2absy, proverCtxt); - Contract.Assert(context != null); - - List programSemantics = new List(blocks.Count); - foreach (Block b in blocks) {Contract.Assert(b != null); - /* - * In block mode, - * For a return block A, generate: - * A_correct <== wp(A_body, true) [post-condition has been translated into an assert] - * For all other blocks, generate: - * A_correct <== wp(A_body, (/\ S \in Successors(A) :: S_correct)) - * - * In doomed mode, proceed as in block mode, except for a return block A, generate: - * A_correct <== wp(A_body, false) [post-condition has been translated into an assert] - * - * In block reach mode, the wp(A_body,...) in the equations above change to: - * A_reached ==> wp(A_body,...) - * and the conjunction above changes to: - * (/\ S \in Successors(A) :: S_correct \/ (\/ T \in Successors(A) && T != S :: T_reached)) - * - * In local mode, generate: - * A_correct <== wp(A_body, true) - */ - VCExpr SuccCorrect; - if (local) { - SuccCorrect = VCExpressionGenerator.True; - } else { - SuccCorrect = SuccessorsCorrect(b, BlkCorrect, BlkReached, doomed, gen); - } - - VCExpr wlp = Wlp.Block(b, SuccCorrect, context); - if (BlkReached != null) { - wlp = gen.Implies(cce.NonNull((VCExprVar)BlkReached[b]), wlp); - } - - VCExprVar okVar = cce.NonNull((VCExprVar)BlkCorrect[b]); - VCExprLetBinding binding = gen.LetBinding(okVar, wlp); - programSemantics.Add(binding); - } - - assertionCount = context.AssertionCount; - return gen.Let(programSemantics, proofObligation); - } - - private static Hashtable/* Block --> VCExprVar */ BlockVariableMap(List/*!*/ blocks, string suffix, - Microsoft.Boogie.VCExpressionGenerator gen) { - Contract.Requires(cce.NonNullElements(blocks)); - Contract.Requires(suffix != null); - Contract.Requires(gen != null); - Contract.Ensures(Contract.Result() != null); - - Hashtable/* Block --> VCExprVar */ map = new Hashtable/* Block --> (Let)Variable */(); - foreach (Block b in blocks) { - Contract.Assert(b != null); - VCExprVar v = gen.Variable(b.Label + suffix, Bpl.Type.Bool); - Contract.Assert(v != null); - map.Add(b, v); - } - return map; - } - - private static VCExpr SuccessorsCorrect( - Block b, - Hashtable/* Block --> VCExprVar */ BlkCorrect, - Hashtable/* Block --> VCExprVar */ BlkReached, - bool doomed, - Microsoft.Boogie.VCExpressionGenerator gen) { - Contract.Requires(b != null); - Contract.Requires(BlkCorrect != null); - Contract.Requires(gen != null); - Contract.Ensures(Contract.Result() != null); - - VCExpr SuccCorrect = null; - GotoCmd gotocmd = b.TransferCmd as GotoCmd; - if (gotocmd != null) { - foreach (Block successor in cce.NonNull(gotocmd.labelTargets)) { - Contract.Assert(successor != null); - // c := S_correct - VCExpr c = (VCExprVar)BlkCorrect[successor]; - Contract.Assert(c != null); - if (BlkReached != null) { - // c := S_correct \/ Sibling0_reached \/ Sibling1_reached \/ ...; - foreach (Block successorSibling in gotocmd.labelTargets) { - Contract.Assert(successorSibling != null); - if (successorSibling != successor) { - c = gen.Or(c, cce.NonNull((VCExprVar)BlkReached[successorSibling])); - } - } - } - SuccCorrect = SuccCorrect == null ? c : gen.And(SuccCorrect, c); - } - } - if (SuccCorrect == null) { - return VCExpressionGenerator.True; - } else if (doomed) { - return VCExpressionGenerator.False; - } else { - return SuccCorrect; - } - } - - static VCExpr NestedBlockVC(Implementation impl, - Dictionary label2absy, - bool reach, - ProverContext proverCtxt, - out int assertionCount){ - Contract.Requires(impl != null); - Contract.Requires(label2absy != null); - Contract.Requires(proverCtxt != null); - Contract.Requires( impl.Blocks.Count != 0); - Contract.Ensures(Contract.Result() != null); - - VCExpressionGenerator gen = proverCtxt.ExprGen; - Contract.Assert(gen != null); - Graph g = Program.GraphFromImpl(impl); - - Hashtable/* Block --> VCExprVar */ BlkCorrect = BlockVariableMap(impl.Blocks, "_correct", gen); - Hashtable/* Block --> VCExprVar */ BlkReached = reach ? BlockVariableMap(impl.Blocks, "_reached", gen) : null; - - Block startBlock = cce.NonNull( impl.Blocks[0]); - VCExpr proofObligation = (VCExprVar)BlkCorrect[startBlock]; - Contract.Assert(proofObligation != null); - VCContext context = new VCContext(label2absy, proverCtxt); - - Hashtable/*Block->int*/ totalOrder = new Hashtable/*Block->int*/(); - { - List blocks = impl.Blocks; - - // block sorting is now done on the VCExpr - // if (((!)CommandLineOptions.Clo.TheProverFactory).NeedsBlockSorting) { - // blocks = SortBlocks(blocks); - // } - int i = 0; - foreach (Block b in blocks) { - Contract.Assert(b != null); - totalOrder[b] = i; - i++; - } - } - - VCExprLetBinding programSemantics = NestedBlockEquation(cce.NonNull(impl.Blocks[0]), BlkCorrect, BlkReached, totalOrder, context, g, gen); - List ps = new List(1); - ps.Add(programSemantics); - - assertionCount = context.AssertionCount; - return gen.Let(ps, proofObligation); - } - - private static VCExprLetBinding NestedBlockEquation(Block b, - Hashtable/*Block-->VCExprVar*/ BlkCorrect, - Hashtable/*Block-->VCExprVar*/ BlkReached, - Hashtable/*Block->int*/ totalOrder, - VCContext context, - Graph g, - Microsoft.Boogie.VCExpressionGenerator gen) { - Contract.Requires(b != null); - Contract.Requires(BlkCorrect != null); - Contract.Requires(totalOrder != null); - Contract.Requires(g != null); - Contract.Requires(context != null); - - Contract.Ensures(Contract.Result() != null); - - /* - * For a block b, return: - * LET_BINDING b_correct = wp(b_body, X) - * where X is: - * LET (THOSE d \in DirectDominates(b) :: BlockEquation(d)) - * IN (/\ s \in Successors(b) :: s_correct) - * - * When the VC-expression generator does not support LET expresions, this - * will eventually turn into: - * b_correct <== wp(b_body, X) - * where X is: - * (/\ s \in Successors(b) :: s_correct) - * <== - * (/\ d \in DirectDominatees(b) :: BlockEquation(d)) - * - * In both cases above, if BlkReached is non-null, then the wp expression - * is instead: - * b_reached ==> wp(b_body, X) - */ - - VCExpr SuccCorrect = SuccessorsCorrect(b, BlkCorrect, null, false, gen); - Contract.Assert(SuccCorrect != null); - - List bindings = new List(); - foreach (Block dominee in GetSortedBlocksImmediatelyDominatedBy(g, b, totalOrder)) { - Contract.Assert(dominee != null); - VCExprLetBinding c = NestedBlockEquation(dominee, BlkCorrect, BlkReached, totalOrder, context, g, gen); - bindings.Add(c); - } - - VCExpr X = gen.Let(bindings, SuccCorrect); - VCExpr wlp = Wlp.Block(b, X, context); - if (BlkReached != null) { - wlp = gen.Implies((VCExprVar)BlkReached[b], wlp); - Contract.Assert(wlp != null); - } - VCExprVar okVar = cce.NonNull((VCExprVar)BlkCorrect[b]); - return gen.LetBinding(okVar, wlp); - } - - /// - /// Returns a list of g.ImmediatelyDominatedBy(b), but in a sorted order, hoping to steer around - /// the nondeterminism problems we've been seeing by using just this call. - /// - static List/*!*/ GetSortedBlocksImmediatelyDominatedBy(Graph/*!*/ g, Block/*!*/ b, Hashtable/*Block->int*//*!*/ totalOrder) { - Contract.Requires(g != null); - Contract.Requires(b != null); - Contract.Requires(totalOrder != null); - Contract.Ensures(Contract.Result>() != null); - - List list = new List(); - foreach (Block dominee in g.ImmediatelyDominatedBy(b)) { - Contract.Assert(dominee != null); - list.Add(dominee); - } - list.Sort(new Comparison(delegate(Block x, Block y) { - return (int)cce.NonNull(totalOrder[x]) - (int)cce.NonNull(totalOrder[y]); - })); - return list; - } - - static VCExpr VCViaStructuredProgram - (Implementation impl, Dictionary label2absy, - ProverContext proverCtxt, - out int assertionCount) - { - Contract.Requires(impl != null); - Contract.Requires(label2absy != null); - Contract.Requires(proverCtxt != null); - Contract.Ensures(Contract.Result() != null); - - #region Convert block structure back to a "regular expression" - RE r = DAG2RE.Transform(cce.NonNull(impl.Blocks[0])); - Contract.Assert(r != null); - #endregion - - VCContext ctxt = new VCContext(label2absy, proverCtxt); - Contract.Assert(ctxt != null); - #region Send wlp(program,true) to Simplify - var vcexp = Wlp.RegExpr(r, VCExpressionGenerator.True, ctxt); - assertionCount = ctxt.AssertionCount; - return vcexp; - #endregion - } - /// /// Remove empty blocks reachable from the startBlock of the CFG /// - static void RemoveEmptyBlocksIterative(List blocks) { + static void RemoveEmptyBlocks(List blocks) { // postorder traversal of cfg // noting loop heads in [keep] and // generating token information in [renameInfo] @@ -4060,131 +3585,6 @@ static void RemoveEmptyBlocksIterative(List blocks) { } - /// - /// Remove the empty blocks reachable from the block. - /// It changes the visiting state of the blocks, so that if you want to visit again the blocks, you have to reset them... - /// - static List RemoveEmptyBlocks(Block b) { - Contract.Requires(b != null); - Contract.Ensures(Contract.Result>() != null); - - Contract.Assert(b.TraversingStatus == Block.VisitState.ToVisit); - Block renameInfo; - List retVal = removeEmptyBlocksWorker(b, true, out renameInfo); - if (renameInfo != null && !b.tok.IsValid) { - bool onlyAssumes = true; - foreach (Cmd c in b.Cmds) { - if (!(c is AssumeCmd)) { - onlyAssumes = false; - break; - } - } - if (onlyAssumes) { - b.tok = renameInfo.tok; - b.Label = renameInfo.Label; - } - } - return retVal; - } - - /// - /// For every not-yet-visited block n reachable from b, change n's successors to skip empty nodes. - /// Return the *set* of blocks reachable from b without passing through a nonempty block. - /// The target of any backedge is counted as a nonempty block. - /// If renameInfoForStartBlock is non-null, it denotes an empty block with location information, and that - /// information would be appropriate to display - /// - private static List removeEmptyBlocksWorker(Block b, bool startNode, out Block renameInfoForStartBlock) - { - Contract.Requires(b != null); - Contract.Ensures(Contract.ValueAtReturn(out renameInfoForStartBlock) == null || Contract.ValueAtReturn(out renameInfoForStartBlock).tok.IsValid); - // ensures: b in result ==> renameInfoForStartBlock == null; - - renameInfoForStartBlock = null; - List bs = new List(); - GotoCmd gtc = b.TransferCmd as GotoCmd; - - // b has no successors - if (gtc == null || gtc.labelTargets == null || gtc.labelTargets.Count == 0) - { - if (b.Cmds.Count != 0){ // only empty blocks are removed... - bs.Add(b); - } else if (b.tok.IsValid) { - renameInfoForStartBlock = b; - } - return bs; - } - else if (b.TraversingStatus == Block.VisitState.ToVisit) // if b has some successors and we have not seen it so far... - { - b.TraversingStatus = Block.VisitState.BeingVisited; - - // Before recursing down to successors, make a sobering observation: - // If b has no commands and is not the start node, then it will see - // extinction (because it will not be included in the "return setOfSuccessors" - // statement below). In that case, if b has a location, then the location - // information would be lost. Hence, make an attempt to save the location - // by pushing the location onto b's successor. This can be done if (0) b has - // exactly one successor, (1) that successor has no location of its own, and - // (2) that successor has no other predecessors. - if (b.Cmds.Count == 0 && !startNode) { - // b is about to become extinct; try to save its name and location, if possible - if (b.tok.IsValid && gtc.labelTargets.Count == 1) { - Block succ = cce.NonNull(gtc.labelTargets[0]); - if (!succ.tok.IsValid && succ.Predecessors.Count == 1) { - succ.tok = b.tok; - succ.Label = b.Label; - } - } - } - - // recursively call this method on each successor - // merge result into a *set* of blocks - HashSet mergedSuccessors = new HashSet(); - int m = 0; // in the following loop, set renameInfoForStartBlock to the value that all recursive calls agree on, if possible; otherwise, null - foreach (Block dest in gtc.labelTargets){Contract.Assert(dest != null); - Block renameInfo; - List ys = removeEmptyBlocksWorker(dest, false, out renameInfo); - Contract.Assert(ys != null); - if (m == 0) { - renameInfoForStartBlock = renameInfo; - } else if (renameInfoForStartBlock != renameInfo) { - renameInfoForStartBlock = null; - } - foreach (Block successor in ys){ - if (!mergedSuccessors.Contains(successor)) - mergedSuccessors.Add(successor); - } - m++; - } - b.TraversingStatus = Block.VisitState.AlreadyVisited; - - List setOfSuccessors = new List(); - foreach (Block d in mergedSuccessors) - setOfSuccessors.Add(d); - if (b.Cmds.Count == 0 && !startNode) { - // b is about to become extinct - if (b.tok.IsValid) { - renameInfoForStartBlock = b; - } - return setOfSuccessors; - } - // otherwise, update the list of successors of b to be the blocks in setOfSuccessors - gtc.labelTargets = setOfSuccessors; - gtc.labelNames = new List(); - foreach (Block d in setOfSuccessors){ - Contract.Assert(d != null); - gtc.labelNames.Add(d.Label);} - if (!startNode) { - renameInfoForStartBlock = null; - } - return new List { b }; - } - else // b has some successors, but we are already visiting it, or we have already visited it... - { - return new List { b }; - } - } - static void DumpMap(Hashtable /*Variable->Expr*/ map) { Contract.Requires(map != null); foreach (DictionaryEntry de in map) { diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index cad5914b8..32ec5750e 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -73,12 +73,7 @@ public static VCExpr Block(Block b, VCExpr N, VCContext ctxt) try { cce.BeginExpose(ctxt); - if (ctxt.Label2absy == null) { - return res; - } - else { - return gen.Implies(gen.LabelPos(cce.NonNull(id.ToString()), VCExpressionGenerator.True), res); - } + return res; } finally { cce.EndExpose(); } @@ -132,11 +127,8 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) { } ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext; } - - VCExpr R = null; - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { - R = gen.Implies(C, N); - } else { + + { var subsumption = Subsumption(ac); if (subsumption == CommandLineOptions.SubsumptionOption.Always || (subsumption == CommandLineOptions.SubsumptionOption.NotForQuantifiers && !(C is VCExprQuantifier))) @@ -163,19 +155,14 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) { if (ctxt.ControlFlowVariableExpr == null) { Contract.Assert(ctxt.Label2absy != null); - R = gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), C), N); + return gen.AndSimp(C, N); } else { VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(ctxt.ControlFlowVariableExpr, gen.Integer(BigNum.FromInt(b.UniqueId))); Contract.Assert(controlFlowFunctionAppl != null); VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(-ac.UniqueId))); - if (ctxt.Label2absy == null) { - R = gen.AndSimp(gen.Implies(assertFailure, C), N); - } else { - R = gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), gen.Implies(assertFailure, C)), N); - } + return gen.AndSimp(gen.Implies(assertFailure, C), N); } } - return R; } else if (cmd is AssumeCmd) { AssumeCmd ac = (AssumeCmd)cmd; @@ -186,7 +173,7 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) { if (naryExpr.Fun is FunctionCall) { int id = ac.UniqueId; ctxt.Label2absy[id] = ac; - return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N)); + return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes,gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N)); } } } diff --git a/Test/aitest9/TestIntervals.bpl.expect b/Test/aitest9/TestIntervals.bpl.expect index b5ca02eb3..9172122e9 100644 --- a/Test/aitest9/TestIntervals.bpl.expect +++ b/Test/aitest9/TestIntervals.bpl.expect @@ -4,7 +4,7 @@ Execution trace: TestIntervals.bpl(8,3): anon9_LoopHead TestIntervals.bpl(14,3): anon10_Else TestIntervals.bpl(15,3): anon11_Else - TestIntervals.bpl(16,14): anon12_Then + TestIntervals.bpl(16,3): anon12_Else TestIntervals.bpl(19,5): anon8 TestIntervals.bpl(70,3): Error BP5001: This assertion might not hold. Execution trace: diff --git a/Test/doomed/doomdebug.bpl b/Test/doomed/doomdebug.bpl deleted file mode 100644 index ef89e9dc7..000000000 --- a/Test/doomed/doomdebug.bpl +++ /dev/null @@ -1,44 +0,0 @@ -procedure badtrace(x:int, y:int, z:int) -{ - var xin : int; - xin := x+z; - - - if (y>5) { - xin:=5; - } else { - assert xin != x; - } -} - -procedure baddiamond(x:int, y:int, z:int) -{ - var xin : int; - var yin : int; - var zin : int; - xin := x; - yin := y; - zin := z; - - if (y<5) { - xin := xin -3; - } else { - zin := zin +10; - xin := 0; - } - - if (x<100) { - yin := 3; - } else { - zin := 5; - } - - if (z>5) { - yin := yin - 2; - xin := xin + 3; - } - - zin:=zin+yin; - - assert xin!=x; -} diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl deleted file mode 100644 index b211a4811..000000000 --- a/Test/doomed/doomed.bpl +++ /dev/null @@ -1,87 +0,0 @@ -// RUN: %boogie -vc:doomed %s -procedure evilrequires(x:int) - requires x>0; -{ - var y : int; - - if(x<0) { - y := 1; - } else { - y := 2; - } -} - - -procedure evilbranch(x:int) -{ - var y : int; - - if(x<0) { - y := 1; - } else { - y := 2; - } - assume y!=2; - - assert x<0; -} - - -procedure evilloop(x:int) -{ - var y : int; - y:=x; - while (y<100) { - y := y -1; - } -} - -procedure evilnested(x:int) -{ - var i : int; - var j : int; - i:=x-1; - j:=1; - while (i>=0) { - while (j<=i) { - assert j10) { - y:=3; - } else { - assert y!=0; - } -} - -procedure evilcondition(x:int) -{ - var y : int; - y:=0; - if (x!=0) { - y:=3; - } else { - assert x!=0; - } -} - -procedure evilensures(x:int) returns ($result: int) - ensures $result>0; -{ - var y : int; - - if(x<0) { - y := 1; - } else { - $result:=-1; - } -} diff --git a/Test/doomed/lit.local.cfg b/Test/doomed/lit.local.cfg deleted file mode 100644 index 462e3dc5d..000000000 --- a/Test/doomed/lit.local.cfg +++ /dev/null @@ -1 +0,0 @@ -config.unsupported = True diff --git a/Test/doomed/notdoomed.bpl b/Test/doomed/notdoomed.bpl deleted file mode 100644 index 321cf1eb1..000000000 --- a/Test/doomed/notdoomed.bpl +++ /dev/null @@ -1,58 +0,0 @@ -// RUN: %boogie -vc:doomed %s -procedure a(x:int) -{ - var y : int; - - if(x<0) { - y := 1; - } else { - y := 2; - } -} - - -procedure b(x:int) -{ - var y : int; - - if(x<0) { - y := 1; - } else { - y := 2; - assert false; - } -} - - -procedure c(x:int) -{ - var y : int; - - if(x<0) { - y := 1; - } else { - y := 2; - assert {:PossiblyUnreachable} false; - } -} - -procedure useCE(x:int) -{ - var y : int; - - if(x<0) { - y := 1; - } else { - y := 2; - } - if(x<7) { - y := 5; - } else { - y := 6; - } - -} - - - - diff --git a/Test/doomed/runtest.bat b/Test/doomed/runtest.bat deleted file mode 100644 index 8c9364fb4..000000000 --- a/Test/doomed/runtest.bat +++ /dev/null @@ -1,16 +0,0 @@ -@echo off -setlocal - -set BOOGIEDIR=..\..\Binaries -set BGEXE=%BOOGIEDIR%\Boogie.exe - -for %%f in (doomed.bpl) do ( - echo -------------------- %%f -------------------- - %BGEXE% /vc:doomed %* %%f -) - -for %%f in (notdoomed.bpl) do ( - echo -------------------- %%f -------------------- - %BGEXE% /vc:doomed %* %%f -) - diff --git a/Test/doomed/smoke0.bpl b/Test/doomed/smoke0.bpl deleted file mode 100644 index 159244ab6..000000000 --- a/Test/doomed/smoke0.bpl +++ /dev/null @@ -1,79 +0,0 @@ -procedure a(x:int) -{ - var y : int; - - if(x<0) { - y := 1; - } else { - y := 2; - } -} - - -procedure b(x:int) - requires x>0; -{ - var y : int; - - if(x<0) { - y := 1; - } else { - y := 2; - } -} - - - -procedure c(x:int) - requires x>0; -{ - var y : int; - - if(x<0) { - y := 1; - assert false; - } else { - y := 2; - } -} - -procedure d(x:int) - requires x>0; -{ - var y : int; - - if(x<0) { - assert false; - y := 1; - } else { - y := 2; - } -} - - -procedure doomed1(x:int) -{ - var y : int; - y := 0; - if(x<0) { - y := 1; - } else { - assert y!=0; - } -} - - -procedure doomed2(x:int) -{ - var y : int; - y := 0; - if(x!=0) { - y := 1; - } else { - assert x!=0; - } -} - - - - diff --git a/Test/extractloops/lit.local.cfg b/Test/extractloops/lit.local.cfg new file mode 100644 index 000000000..94140b6ba --- /dev/null +++ b/Test/extractloops/lit.local.cfg @@ -0,0 +1,2 @@ +# Do not run tests in this directory and below +config.unsupported = True diff --git a/Test/livevars/bla1.bpl.expect b/Test/livevars/bla1.bpl.expect index 287733890..9fdade6d3 100644 --- a/Test/livevars/bla1.bpl.expect +++ b/Test/livevars/bla1.bpl.expect @@ -40,7 +40,7 @@ Execution trace: bla1.bpl(1526,3): inline$I8xKeyboardGetSysButtonEvent$0$anon6_Else#1 bla1.bpl(1534,3): inline$I8xKeyboardGetSysButtonEvent$0$anon7_Then#1 bla1.bpl(1544,3): inline$I8xKeyboardGetSysButtonEvent$0$anon2#1 - bla1.bpl(1556,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23_false#1 + bla1.bpl(1568,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23_true#1 bla1.bpl(1588,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13_true#1 bla1.bpl(1621,3): inline$storm_IoCompleteRequest$0$label_6_false#1 bla1.bpl(1656,3): inline$storm_IoCompleteRequest$0$anon4_Else#1 @@ -51,14 +51,17 @@ Execution trace: bla1.bpl(1741,3): anon7#1 bla1.bpl(1798,3): inline$storm_IoCancelIrp$0$anon12_Then#1 bla1.bpl(1803,3): inline$storm_IoCancelIrp$0$anon2#1 - bla1.bpl(1827,3): inline$storm_IoCancelIrp$0$anon14_Then#1 + bla1.bpl(1814,3): inline$storm_IoCancelIrp$0$anon14_Else#1 + bla1.bpl(1822,3): inline$storm_IoCancelIrp$0$anon15_Then#1 bla1.bpl(1832,3): inline$storm_IoCancelIrp$0$anon5#1 - bla1.bpl(1853,3): inline$storm_IoCancelIrp$0$anon16_Then#1 + bla1.bpl(1840,3): inline$storm_IoCancelIrp$0$anon16_Else#1 + bla1.bpl(1848,3): inline$storm_IoCancelIrp$0$anon17_Then#1 bla1.bpl(1858,3): inline$storm_IoCancelIrp$0$anon8#1 bla1.bpl(1869,3): inline$storm_IoCancelIrp$0$anon18_Then#1 bla1.bpl(1874,3): inline$storm_IoCancelIrp$0$anon10#1 bla1.bpl(1934,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#1 - bla1.bpl(1962,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Then#1 + bla1.bpl(1949,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Else#1 + bla1.bpl(1957,3): inline$storm_IoAcquireCancelSpinLock$0$anon7_Then#1 bla1.bpl(1967,3): inline$storm_IoAcquireCancelSpinLock$0$anon3#1 bla1.bpl(1978,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Then#1 bla1.bpl(1983,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#1 diff --git a/Test/livevars/stack_overflow.bpl.expect b/Test/livevars/stack_overflow.bpl.expect index f8d88c7d8..0d0e1726c 100644 --- a/Test/livevars/stack_overflow.bpl.expect +++ b/Test/livevars/stack_overflow.bpl.expect @@ -23,82 +23,69 @@ Execution trace: stack_overflow.bpl(1756,3): inline$IoGetCurrentIrpStackLocation$1$label_3_false#1 stack_overflow.bpl(1796,3): inline$storm_thread_dispatch$0$anon4_Else#1 stack_overflow.bpl(1879,3): inline$BDLPnP$0$anon54_Else#1 - stack_overflow.bpl(1889,3): inline$BDLPnP$0$label_16_false#1 + stack_overflow.bpl(1893,3): inline$BDLPnP$0$label_16_true#1 stack_overflow.bpl(1937,3): inline$BDLPnP$0$anon55_Else#1 - stack_overflow.bpl(1951,3): inline$BDLPnP$0$label_26_true#1 + stack_overflow.bpl(1947,3): inline$BDLPnP$0$label_26_false#1 stack_overflow.bpl(1995,3): inline$BDLPnP$0$anon56_Else#1 - stack_overflow.bpl(2009,3): inline$BDLPnP$0$label_36_true#1 + stack_overflow.bpl(2005,3): inline$BDLPnP$0$label_36_false#1 stack_overflow.bpl(2035,3): inline$IoGetCurrentIrpStackLocation$2$label_3_false#1 stack_overflow.bpl(2075,3): inline$BDLPnP$0$anon57_Else#1 stack_overflow.bpl(2102,3): inline$BDLPnP$0$label_44_true#1 stack_overflow.bpl(2111,3): inline$BDLPnP$0$label_47#1 stack_overflow.bpl(2115,3): inline$BDLPnP$0$anon58_Else#1 stack_overflow.bpl(2129,3): inline$BDLPnP$0$label_51_false#1 - stack_overflow.bpl(22560,3): inline$BDLPnP$0$label_52_case_6#1 - stack_overflow.bpl(22613,3): inline$BDLPnPQueryStop$0$anon22_Else#1 - stack_overflow.bpl(22627,3): inline$BDLPnPQueryStop$0$label_9_true#1 - stack_overflow.bpl(22671,3): inline$BDLPnPQueryStop$0$anon23_Else#1 - stack_overflow.bpl(22685,3): inline$BDLPnPQueryStop$0$label_19_true#1 - stack_overflow.bpl(22729,3): inline$BDLPnPQueryStop$0$anon24_Else#1 - stack_overflow.bpl(22743,3): inline$BDLPnPQueryStop$0$label_29_true#1 - stack_overflow.bpl(22750,3): inline$BDLPnPQueryStop$0$label_30#1 - stack_overflow.bpl(22799,3): inline$storm_KeAcquireSpinLock$2$anon7_Else#1 - stack_overflow.bpl(22822,3): inline$storm_KeAcquireSpinLock$2$label_13_true#1 - stack_overflow.bpl(22830,3): inline$storm_KeAcquireSpinLock$2$anon8_Else#1 - stack_overflow.bpl(22850,3): inline$storm_KeAcquireSpinLock$2$anon9_Then#1 - stack_overflow.bpl(22855,3): inline$storm_KeAcquireSpinLock$2$anon6#1 - stack_overflow.bpl(22859,3): inline$storm_KeAcquireSpinLock$2$label_1#1 - stack_overflow.bpl(22876,3): inline$BDLPnPQueryStop$0$anon25_Else#1 - stack_overflow.bpl(22887,3): inline$BDLPnPQueryStop$0$label_34_false#1 - stack_overflow.bpl(22917,3): inline$BDLPnPQueryStop$0$anon26_Else#1 - stack_overflow.bpl(22950,3): inline$storm_KeReleaseSpinLock$4$anon5_Else#1 - stack_overflow.bpl(22990,3): inline$storm_KeReleaseSpinLock$4$label_11_true#1 - stack_overflow.bpl(23006,3): inline$storm_KeReleaseSpinLock$4$anon6_Then#1 - stack_overflow.bpl(23011,3): inline$storm_KeReleaseSpinLock$4$anon4#1 - stack_overflow.bpl(23015,3): inline$storm_KeReleaseSpinLock$4$label_1#1 - stack_overflow.bpl(23028,3): inline$BDLPnPQueryStop$0$anon31_Else#1 - stack_overflow.bpl(23089,3): inline$IoGetCurrentIrpStackLocation$92$label_3_false#1 - stack_overflow.bpl(23129,3): inline$IoCopyCurrentIrpStackLocationToNext$4$anon4_Else#1 - stack_overflow.bpl(23170,3): inline$IoGetNextIrpStackLocation$9$label_3_true#1 - stack_overflow.bpl(23189,3): inline$IoCopyCurrentIrpStackLocationToNext$4$anon5_Else#1 - stack_overflow.bpl(23223,3): inline$BDLCallLowerLevelDriverAndWait$4$anon16_Else#1 - stack_overflow.bpl(23257,3): inline$BDLCallLowerLevelDriverAndWait$4$anon17_Else#1 - stack_overflow.bpl(23285,3): inline$storm_IoSetCompletionRoutine$4$label_7_false#1 - stack_overflow.bpl(23355,3): inline$IoGetNextIrpStackLocation$10$label_3_true#1 - stack_overflow.bpl(23374,3): inline$storm_IoSetCompletionRoutine$4$anon5_Else#1 - stack_overflow.bpl(23390,3): inline$storm_IoSetCompletionRoutine$4$label_1#1 - stack_overflow.bpl(23407,3): inline$BDLCallLowerLevelDriverAndWait$4$anon18_Else#1 - stack_overflow.bpl(23428,3): inline$IoGetCurrentIrpStackLocation$93$label_3_false#1 - stack_overflow.bpl(23468,3): inline$BDLCallLowerLevelDriverAndWait$4$anon19_Else#1 - stack_overflow.bpl(23478,3): inline$BDLCallLowerLevelDriverAndWait$4$label_18_false#1 - stack_overflow.bpl(23510,3): inline$storm_IoCallDriver$9$label_9_false#1 - stack_overflow.bpl(23580,3): inline$IoSetNextIrpStackLocation$10$label_3_true#1 - stack_overflow.bpl(23586,3): inline$IoSetNextIrpStackLocation$10$label_5#1 - stack_overflow.bpl(23608,3): inline$storm_IoCallDriver$9$anon11_Else#1 - stack_overflow.bpl(23648,3): inline$IoGetCurrentIrpStackLocation$94$label_3_true#1 - stack_overflow.bpl(23669,3): inline$storm_IoCallDriver$9$anon13_Else#1 - stack_overflow.bpl(23694,3): inline$storm_IoCallDriver$9$label_27_case_2#1 - stack_overflow.bpl(23764,3): inline$IoGetCurrentIrpStackLocation$95$label_3_true#1 - stack_overflow.bpl(23785,3): inline$CallCompletionRoutine$18$anon10_Else#1 - stack_overflow.bpl(23842,3): inline$IoGetCurrentIrpStackLocation$96$label_3_true#1 - stack_overflow.bpl(23863,3): inline$CallCompletionRoutine$18$anon11_Else#1 - stack_overflow.bpl(23876,3): inline$CallCompletionRoutine$18$label_18_false#1 - stack_overflow.bpl(26004,3): inline$CallCompletionRoutine$18$label_1#1 - stack_overflow.bpl(26025,3): inline$storm_IoCallDriver$9$anon14_Else#1 - stack_overflow.bpl(28395,3): inline$storm_IoCallDriver$9$label_36#1 - stack_overflow.bpl(28399,3): inline$storm_IoCallDriver$9$label_1#1 - stack_overflow.bpl(28421,3): inline$BDLCallLowerLevelDriverAndWait$4$anon20_Else#1 - stack_overflow.bpl(33440,3): inline$BDLCallLowerLevelDriverAndWait$4$label_29_false#1 - stack_overflow.bpl(33598,3): inline$BDLCallLowerLevelDriverAndWait$4$label_30#1 - stack_overflow.bpl(33641,3): inline$BDLPnPQueryStop$0$anon32_Else#1 - stack_overflow.bpl(33809,3): inline$BDLPnPQueryStop$0$anon28_Else#1 - stack_overflow.bpl(33819,3): inline$BDLPnPQueryStop$0$label_45_false#1 - stack_overflow.bpl(33867,3): inline$BDLPnPQueryStop$0$anon29_Else#1 - stack_overflow.bpl(33881,3): inline$BDLPnPQueryStop$0$label_55_true#1 - stack_overflow.bpl(33925,3): inline$BDLPnPQueryStop$0$anon30_Else#1 - stack_overflow.bpl(33935,3): inline$BDLPnPQueryStop$0$label_65_false#1 - stack_overflow.bpl(33946,3): inline$BDLPnPQueryStop$0$label_66#1 - stack_overflow.bpl(33993,3): inline$BDLPnP$0$anon72_Else#1 + stack_overflow.bpl(11320,3): inline$BDLPnP$0$label_52_case_7#1 + stack_overflow.bpl(11369,3): inline$BDLPnPCancelStop$0$anon22_Else#1 + stack_overflow.bpl(11379,3): inline$BDLPnPCancelStop$0$label_8_false#1 + stack_overflow.bpl(11427,3): inline$BDLPnPCancelStop$0$anon23_Else#1 + stack_overflow.bpl(11441,3): inline$BDLPnPCancelStop$0$label_18_true#1 + stack_overflow.bpl(11485,3): inline$BDLPnPCancelStop$0$anon24_Else#1 + stack_overflow.bpl(11495,3): inline$BDLPnPCancelStop$0$label_28_false#1 + stack_overflow.bpl(11506,3): inline$BDLPnPCancelStop$0$label_29#1 + stack_overflow.bpl(11559,3): inline$IoGetCurrentIrpStackLocation$112$label_3_false#1 + stack_overflow.bpl(11599,3): inline$IoCopyCurrentIrpStackLocationToNext$5$anon4_Else#1 + stack_overflow.bpl(11623,3): inline$IoGetNextIrpStackLocation$11$label_3_false#1 + stack_overflow.bpl(11659,3): inline$IoCopyCurrentIrpStackLocationToNext$5$anon5_Else#1 + stack_overflow.bpl(11693,3): inline$BDLCallLowerLevelDriverAndWait$5$anon16_Else#1 + stack_overflow.bpl(11727,3): inline$BDLCallLowerLevelDriverAndWait$5$anon17_Else#1 + stack_overflow.bpl(11755,3): inline$storm_IoSetCompletionRoutine$5$label_7_false#1 + stack_overflow.bpl(11808,3): inline$IoGetNextIrpStackLocation$12$label_3_false#1 + stack_overflow.bpl(11844,3): inline$storm_IoSetCompletionRoutine$5$anon5_Else#1 + stack_overflow.bpl(11860,3): inline$storm_IoSetCompletionRoutine$5$label_1#1 + stack_overflow.bpl(11877,3): inline$BDLCallLowerLevelDriverAndWait$5$anon18_Else#1 + stack_overflow.bpl(11898,3): inline$IoGetCurrentIrpStackLocation$113$label_3_false#1 + stack_overflow.bpl(11938,3): inline$BDLCallLowerLevelDriverAndWait$5$anon19_Else#1 + stack_overflow.bpl(11948,3): inline$BDLCallLowerLevelDriverAndWait$5$label_18_false#1 + stack_overflow.bpl(11980,3): inline$storm_IoCallDriver$11$label_9_false#1 + stack_overflow.bpl(12033,3): inline$IoSetNextIrpStackLocation$12$label_3_false#1 + stack_overflow.bpl(12056,3): inline$IoSetNextIrpStackLocation$12$label_5#1 + stack_overflow.bpl(12078,3): inline$storm_IoCallDriver$11$anon11_Else#1 + stack_overflow.bpl(12118,3): inline$IoGetCurrentIrpStackLocation$114$label_3_true#1 + stack_overflow.bpl(12139,3): inline$storm_IoCallDriver$11$anon13_Else#1 + stack_overflow.bpl(14506,3): inline$storm_IoCallDriver$11$label_27_case_1#1 + stack_overflow.bpl(14576,3): inline$IoGetCurrentIrpStackLocation$119$label_3_true#1 + stack_overflow.bpl(14597,3): inline$CallCompletionRoutine$23$anon10_Else#1 + stack_overflow.bpl(14654,3): inline$IoGetCurrentIrpStackLocation$120$label_3_true#1 + stack_overflow.bpl(14675,3): inline$CallCompletionRoutine$23$anon11_Else#1 + stack_overflow.bpl(14688,3): inline$CallCompletionRoutine$23$label_18_false#1 + stack_overflow.bpl(16816,3): inline$CallCompletionRoutine$23$label_1#1 + stack_overflow.bpl(16837,3): inline$storm_IoCallDriver$11$anon15_Else#1 + stack_overflow.bpl(16865,3): inline$storm_IoCallDriver$11$label_36#1 + stack_overflow.bpl(16869,3): inline$storm_IoCallDriver$11$label_1#1 + stack_overflow.bpl(16891,3): inline$BDLCallLowerLevelDriverAndWait$5$anon20_Else#1 + stack_overflow.bpl(21910,3): inline$BDLCallLowerLevelDriverAndWait$5$label_29_false#1 + stack_overflow.bpl(22068,3): inline$BDLCallLowerLevelDriverAndWait$5$label_30#1 + stack_overflow.bpl(22111,3): inline$BDLPnPCancelStop$0$anon25_Else#1 + stack_overflow.bpl(22125,3): inline$BDLPnPCancelStop$0$label_34_false#1 + stack_overflow.bpl(22154,3): inline$BDLPnPCancelStop$0$anon26_Else#1 + stack_overflow.bpl(22354,3): inline$BDLPnPCancelStop$0$anon30_Else#1 + stack_overflow.bpl(22364,3): inline$BDLPnPCancelStop$0$label_66_false#1 + stack_overflow.bpl(22412,3): inline$BDLPnPCancelStop$0$anon31_Else#1 + stack_overflow.bpl(22426,3): inline$BDLPnPCancelStop$0$label_76_true#1 + stack_overflow.bpl(22470,3): inline$BDLPnPCancelStop$0$anon32_Else#1 + stack_overflow.bpl(22480,3): inline$BDLPnPCancelStop$0$label_86_false#1 + stack_overflow.bpl(22491,3): inline$BDLPnPCancelStop$0$label_87#1 + stack_overflow.bpl(22545,3): inline$BDLPnP$0$anon73_Else#1 stack_overflow.bpl(94595,3): inline$BDLPnP$0$label_139_true#1 stack_overflow.bpl(94624,3): inline$storm_IoCompleteRequest$57$label_6_true#1 stack_overflow.bpl(94632,3): inline$storm_IoCompleteRequest$57$anon3_Else#1 @@ -109,9 +96,13 @@ Execution trace: stack_overflow.bpl(95236,3): inline$storm_thread_dispatch$0$Return#1 stack_overflow.bpl(95296,3): inline$storm_IoCancelIrp$0$anon9_Then#1 stack_overflow.bpl(95301,3): inline$storm_IoCancelIrp$0$anon1#1 - stack_overflow.bpl(95358,3): inline$storm_IoAcquireCancelSpinLock$0$anon4_Then#1 - stack_overflow.bpl(95520,3): inline$storm_IoCancelIrp$0$anon10_Then#1 - stack_overflow.bpl(95541,3): inline$storm_thread_cancel$0$anon2_Then#1 + stack_overflow.bpl(95325,3): inline$storm_IoAcquireCancelSpinLock$0$anon4_Else#1 + stack_overflow.bpl(95346,3): inline$storm_IoAcquireCancelSpinLock$0$anon5_Then#1 + stack_overflow.bpl(95351,3): inline$storm_IoAcquireCancelSpinLock$0$anon3#1 + stack_overflow.bpl(95368,3): inline$storm_IoCancelIrp$0$anon10_Else#1 + stack_overflow.bpl(95379,3): inline$storm_IoCancelIrp$0$label_16_false#1 + stack_overflow.bpl(95509,3): inline$storm_IoCancelIrp$0$label_1#1 + stack_overflow.bpl(95530,3): inline$storm_thread_cancel$0$anon2_Else#1 stack_overflow.bpl(95545,3): inline$storm_thread_cancel$0$Return#1 stack_overflow.bpl(97933,3): inline$storm_thread_completion$0$anon4_Then#1 stack_overflow.bpl(97937,3): inline$storm_thread_completion$0$Return#1 diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl index 4608a7ad8..fe1238ecb 100644 --- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl +++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl @@ -1,4 +1,4 @@ -// RUN: %boogie -typeEncoding:m -proverOpt:MULTI_TRACES "%s" > "%t" +// RUN: %boogie -typeEncoding:m "%s" > "%t" // RUN: %diff "%s.expect" "%t" var v4.Mem: [name][int]int; diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect index 628a1fe45..ac55f4ebb 100644 --- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect +++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect @@ -7,15 +7,6 @@ Execution trace: EQ_v2.Eval__v4.Eval_out.bpl(1991,3): inline$v4.Eval$0$label_11_case_2#2 EQ_v2.Eval__v4.Eval_out.bpl(2013,3): inline$v4.Eval$0$label_14_true#2 EQ_v2.Eval__v4.Eval_out.bpl(2083,3): inline$v4.Eval$0$label_12#2 -EQ_v2.Eval__v4.Eval_out.bpl(2103,5): Error BP5003: A postcondition might not hold on this return path. -EQ_v2.Eval__v4.Eval_out.bpl(1717,3): Related location: This is the postcondition that might not hold. -Execution trace: - EQ_v2.Eval__v4.Eval_out.bpl(1788,3): AA_INSTR_EQ_BODY - EQ_v2.Eval__v4.Eval_out.bpl(1877,3): inline$v2.Eval$0$label_11_case_1#2 - EQ_v2.Eval__v4.Eval_out.bpl(1896,3): inline$v2.Eval$0$label_12#2 - EQ_v2.Eval__v4.Eval_out.bpl(2034,3): inline$v4.Eval$0$label_11_case_1#2 - EQ_v2.Eval__v4.Eval_out.bpl(2056,3): inline$v4.Eval$0$label_13_true#2 - EQ_v2.Eval__v4.Eval_out.bpl(2083,3): inline$v4.Eval$0$label_12#2 EQ_v2.Eval__v4.Eval_out.bpl(2154,5): Error BP5003: A postcondition might not hold on this return path. EQ_v2.Eval__v4.Eval_out.bpl(2122,3): Related location: This is the postcondition that might not hold. Execution trace: @@ -25,4 +16,4 @@ EQ_v2.Eval__v4.Eval_out.bpl(2169,3): Related location: This is the postcondition Execution trace: EQ_v2.Eval__v4.Eval_out.bpl(2180,3): AA_INSTR_EQ_BODY -Boogie program verifier finished with 6 verified, 4 errors +Boogie program verifier finished with 6 verified, 3 errors diff --git a/Test/prover/z3mutl.bpl b/Test/prover/z3mutl.bpl index 6ed56ec86..c013ac095 100644 --- a/Test/prover/z3mutl.bpl +++ b/Test/prover/z3mutl.bpl @@ -1,4 +1,4 @@ -// RUN: %boogie -typeEncoding:m -proverOpt:MULTI_TRACES "%s" > "%t" +// RUN: %boogie -typeEncoding:m "%s" > "%t" // RUN: %diff "%s.expect" "%t" var x:int; diff --git a/Test/prover/z3mutl.bpl.expect b/Test/prover/z3mutl.bpl.expect index a4e7fea79..0459759b9 100644 --- a/Test/prover/z3mutl.bpl.expect +++ b/Test/prover/z3mutl.bpl.expect @@ -1,17 +1,7 @@ z3mutl.bpl(22,5): Error BP5001: This assertion might not hold. -Execution trace: - z3mutl.bpl(7,1): start - z3mutl.bpl(10,1): L1 - z3mutl.bpl(22,1): L5 -z3mutl.bpl(22,5): Error BP5001: This assertion might not hold. Execution trace: z3mutl.bpl(7,1): start z3mutl.bpl(13,1): L2 z3mutl.bpl(22,1): L5 -z3mutl.bpl(22,5): Error BP5001: This assertion might not hold. -Execution trace: - z3mutl.bpl(7,1): start - z3mutl.bpl(16,1): L3 - z3mutl.bpl(22,1): L5 -Boogie program verifier finished with 0 verified, 3 errors +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/stratifiedinline/lit.local.cfg b/Test/stratifiedinline/lit.local.cfg new file mode 100644 index 000000000..94140b6ba --- /dev/null +++ b/Test/stratifiedinline/lit.local.cfg @@ -0,0 +1,2 @@ +# Do not run tests in this directory and below +config.unsupported = True diff --git a/Test/symdiff/foo.bpl b/Test/symdiff/foo.bpl index dce395d86..b796ab3ee 100644 --- a/Test/symdiff/foo.bpl +++ b/Test/symdiff/foo.bpl @@ -1,10 +1,10 @@ -// RUN: %boogie -proverOpt:MULTI_TRACES -errorTrace:0 "%s" > "%t" +// RUN: %boogie -errorTrace:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -procedure Foo(x:int) +procedure Foo(x:int) { var ok:bool; - - ok := true; + + ok := true; if (x == 1) { ok := false; @@ -13,7 +13,7 @@ procedure Foo(x:int) } else if (x == 3) { ok := false; } - + assert ok; } diff --git a/Test/symdiff/foo.bpl.expect b/Test/symdiff/foo.bpl.expect index eec83421d..3d8f12b40 100644 --- a/Test/symdiff/foo.bpl.expect +++ b/Test/symdiff/foo.bpl.expect @@ -1,5 +1,3 @@ foo.bpl(17,3): Error BP5001: This assertion might not hold. -foo.bpl(17,3): Error BP5001: This assertion might not hold. -foo.bpl(17,3): Error BP5001: This assertion might not hold. -Boogie program verifier finished with 0 verified, 3 errors +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect index 7ba7640c8..8f03fc8e5 100644 --- a/Test/test15/CaptureState.bpl.expect +++ b/Test/test15/CaptureState.bpl.expect @@ -5,13 +5,7 @@ Execution trace: CaptureState.bpl(19,5): anon4_Then CaptureState.bpl(27,5): anon3 *** MODEL -%lbl%@1 -> false -%lbl%+0 -> true -%lbl%+2 -> false -%lbl%+3 -> true -%lbl%+4 -> true -%lbl%+5 -> true -$mv_state_const -> 4 +$mv_state_const -> 3 F -> T@FieldName!val!0 Heap -> |T@[Ref,FieldName]Int!val!0| m -> **m @@ -25,12 +19,20 @@ this -> T@Ref!val!0 x -> 40 y -> 0 $mv_state -> { - 4 0 -> true - 4 1 -> true - 4 2 -> true - 4 5 -> true + 3 0 -> true + 3 1 -> true + 3 2 -> true + 3 5 -> true else -> true } +ControlFlow -> { + 0 0 -> 212 + 0 137 -> 139 + 0 139 -> 143 + 0 143 -> (- 437) + 0 212 -> 137 + else -> (- 437) +} Select_[Ref,FieldName]$int -> { |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 8) else -> (- 8) diff --git a/Test/test15/IntInModel.bpl.expect b/Test/test15/IntInModel.bpl.expect index de74ad74a..e4cdbb480 100644 --- a/Test/test15/IntInModel.bpl.expect +++ b/Test/test15/IntInModel.bpl.expect @@ -1,8 +1,11 @@ *** MODEL -%lbl%@1 -> false -%lbl%+0 -> true -%lbl%+2 -> true i -> 0 +ControlFlow -> { + 0 0 -> 30 + 0 24 -> (- 31) + 0 30 -> 24 + else -> (- 31) +} tickleBool -> { false -> true true -> true diff --git a/Test/test15/ModelTest.bpl.expect b/Test/test15/ModelTest.bpl.expect index 992159933..0b297e7c8 100644 --- a/Test/test15/ModelTest.bpl.expect +++ b/Test/test15/ModelTest.bpl.expect @@ -1,14 +1,16 @@ *** MODEL -%lbl%@1 -> false -%lbl%@2 -> false -%lbl%+0 -> true -%lbl%+3 -> true i@0 -> 1 j@0 -> 2 j@1 -> 3 j@2 -> 4 r -> T@ref!val!0 s -> T@ref!val!0 +ControlFlow -> { + 0 0 -> 85 + 0 65 -> (- 139) + 0 85 -> 65 + else -> (- 139) +} tickleBool -> { false -> true true -> true diff --git a/Test/test15/NullInModel.bpl.expect b/Test/test15/NullInModel.bpl.expect index bc003b1f3..4fae67b36 100644 --- a/Test/test15/NullInModel.bpl.expect +++ b/Test/test15/NullInModel.bpl.expect @@ -1,9 +1,12 @@ *** MODEL -%lbl%@1 -> false -%lbl%+0 -> true -%lbl%+2 -> true null -> T@ref!val!0 s -> T@ref!val!0 +ControlFlow -> { + 0 0 -> 38 + 0 25 -> (- 39) + 0 38 -> 25 + else -> (- 39) +} tickleBool -> { false -> true true -> true diff --git a/Test/test7/MultipleErrors.bpl.e1.block.expect b/Test/test7/MultipleErrors.bpl.e1.block.expect deleted file mode 100644 index 73db2a211..000000000 --- a/Test/test7/MultipleErrors.bpl.e1.block.expect +++ /dev/null @@ -1,6 +0,0 @@ -MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. -Execution trace: - MultipleErrors.bpl(24,1): start - MultipleErrors.bpl(27,1): A - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test7/MultipleErrors.bpl.e1.dag.expect b/Test/test7/MultipleErrors.bpl.e1.dag.expect deleted file mode 100644 index 00037e68c..000000000 --- a/Test/test7/MultipleErrors.bpl.e1.dag.expect +++ /dev/null @@ -1,6 +0,0 @@ -MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold. -Execution trace: - MultipleErrors.bpl(24,1): start - MultipleErrors.bpl(31,1): B - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test7/MultipleErrors.bpl.e1.local.expect b/Test/test7/MultipleErrors.bpl.e1.local.expect deleted file mode 100644 index 617c87593..000000000 --- a/Test/test7/MultipleErrors.bpl.e1.local.expect +++ /dev/null @@ -1,5 +0,0 @@ -MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. -Execution trace: - MultipleErrors.bpl(27,1): A - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test7/MultipleErrors.bpl.e10.dag.expect b/Test/test7/MultipleErrors.bpl.e10.dag.expect deleted file mode 100644 index 493a0e3f1..000000000 --- a/Test/test7/MultipleErrors.bpl.e10.dag.expect +++ /dev/null @@ -1,15 +0,0 @@ -MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. -Execution trace: - MultipleErrors.bpl(24,1): start - MultipleErrors.bpl(27,1): A -MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold. -Execution trace: - MultipleErrors.bpl(24,1): start - MultipleErrors.bpl(31,1): B -MultipleErrors.bpl(36,3): Error BP5001: This assertion might not hold. -Execution trace: - MultipleErrors.bpl(24,1): start - MultipleErrors.bpl(31,1): B - MultipleErrors.bpl(35,1): C - -Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test7/MultipleErrors.bpl.e10.local.expect b/Test/test7/MultipleErrors.bpl.e10.local.expect deleted file mode 100644 index 9b685ee3c..000000000 --- a/Test/test7/MultipleErrors.bpl.e10.local.expect +++ /dev/null @@ -1,11 +0,0 @@ -MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. -Execution trace: - MultipleErrors.bpl(27,1): A -MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold. -Execution trace: - MultipleErrors.bpl(31,1): B -MultipleErrors.bpl(36,3): Error BP5001: This assertion might not hold. -Execution trace: - MultipleErrors.bpl(35,1): C - -Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test7/NestedVC.bpl b/Test/test7/NestedVC.bpl deleted file mode 100644 index 4fd22d226..000000000 --- a/Test/test7/NestedVC.bpl +++ /dev/null @@ -1,23 +0,0 @@ -// RUN: %boogie -vc:nested "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure P() -{ -A: goto B, C; -B: goto G; -C: goto D, E; -D: goto F; -E: goto F; -F: goto G; -G: return; -} - -procedure Q(x: bool) -{ -A: goto B, C; -B: assert x; goto G; -C: goto D, E; -D: goto F; -E: goto F; -F: goto G; -G: return; -} diff --git a/Test/test7/NestedVC.bpl.expect b/Test/test7/NestedVC.bpl.expect deleted file mode 100644 index cf9443b6d..000000000 --- a/Test/test7/NestedVC.bpl.expect +++ /dev/null @@ -1,6 +0,0 @@ -NestedVC.bpl(17,4): Error BP5001: This assertion might not hold. -Execution trace: - NestedVC.bpl(16,1): A - NestedVC.bpl(17,1): B - -Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test7/UnreachableBlocks.bpl b/Test/test7/UnreachableBlocks.bpl deleted file mode 100644 index 90f0b0cb3..000000000 --- a/Test/test7/UnreachableBlocks.bpl +++ /dev/null @@ -1,42 +0,0 @@ -// RUN: %boogie -vc:nested "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// In the following program, block "A" has no dominator, which would cause Boogie -// to crash if Boogie didn't first remove unreachable blocks. That is essentially -// what this test tests -procedure P() -{ -entry: - goto A; -A: - return; -B: - goto A; -} - -procedure Q() -{ -entry: - goto entry, A; -A: - return; -} - -procedure R() -{ -entry: - return; -A: - goto A; -} - -procedure S() -{ -entry: - return; -A: - goto C; -B: - goto C; -C: // C has no dominator - return; -} diff --git a/Test/test7/UnreachableBlocks.bpl.expect b/Test/test7/UnreachableBlocks.bpl.expect deleted file mode 100644 index 00ddb38b4..000000000 --- a/Test/test7/UnreachableBlocks.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 4 verified, 0 errors