From 3b4e6550adff50ecd6b09ee8e6dfbf9c3e638fe6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 2 Oct 2024 13:23:30 +0200 Subject: [PATCH 1/8] Move ICarriedAttributes --- Source/Core/AST/Absy.cs | 65 ------------------------- Source/Core/AST/ICarriesAttributes.cs | 70 +++++++++++++++++++++++++++ 2 files changed, 70 insertions(+), 65 deletions(-) create mode 100644 Source/Core/AST/ICarriesAttributes.cs diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 3b0366d07..d8f53dbca 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -247,71 +247,6 @@ public void SetMetadata(int index, T value) #endregion } - public interface ICarriesAttributes - { - QKeyValue Attributes { get; set; } - - public void ResolveAttributes(ResolutionContext rc) - { - for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) - { - kv.Resolve(rc); - } - } - - public void TypecheckAttributes(TypecheckingContext tc) - { - var oldGlobalAccessOnlyInOld = tc.GlobalAccessOnlyInOld; - tc.GlobalAccessOnlyInOld = false; - for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) - { - kv.Typecheck(tc); - } - tc.GlobalAccessOnlyInOld = oldGlobalAccessOnlyInOld; - } - - public List FindLayers() - { - List layers = new List(); - for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) - { - if (kv.Key == CivlAttributes.LAYER) - { - layers.AddRange(kv.Params.Select(o => ((LiteralExpr)o).asBigNum.ToIntSafe)); - } - } - return layers.Distinct().OrderBy(l => l).ToList(); - } - - // Look for {:name string} in list of attributes. - public string FindStringAttribute(string name) - { - return QKeyValue.FindStringAttribute(Attributes, name); - } - - public void AddStringAttribute(IToken tok, string name, string parameter) - { - Attributes = new QKeyValue(tok, name, new List() {parameter}, Attributes); - } - - public void CopyIdFrom(IToken tok, ICarriesAttributes src) - { - var id = src.FindStringAttribute("id"); - if (id is not null) { - AddStringAttribute(tok, "id", id); - } - } - - public void CopyIdWithModificationsFrom(IToken tok, ICarriesAttributes src, Func modifier) - { - var id = src.FindStringAttribute("id"); - if (id is not null) { - AddStringAttribute(tok, "id", modifier(id).SolverLabel); - } - } - - } - [ContractClassFor(typeof(Absy))] public abstract class AbsyContracts : Absy { diff --git a/Source/Core/AST/ICarriesAttributes.cs b/Source/Core/AST/ICarriesAttributes.cs new file mode 100644 index 000000000..747d56c41 --- /dev/null +++ b/Source/Core/AST/ICarriesAttributes.cs @@ -0,0 +1,70 @@ +using System; +using System.Collections.Generic; +using System.Linq; + +namespace Microsoft.Boogie; + +public interface ICarriesAttributes +{ + QKeyValue Attributes { get; set; } + + public void ResolveAttributes(ResolutionContext rc) + { + for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) + { + kv.Resolve(rc); + } + } + + public void TypecheckAttributes(TypecheckingContext tc) + { + var oldGlobalAccessOnlyInOld = tc.GlobalAccessOnlyInOld; + tc.GlobalAccessOnlyInOld = false; + for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) + { + kv.Typecheck(tc); + } + tc.GlobalAccessOnlyInOld = oldGlobalAccessOnlyInOld; + } + + public List FindLayers() + { + List layers = new List(); + for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) + { + if (kv.Key == CivlAttributes.LAYER) + { + layers.AddRange(kv.Params.Select(o => ((LiteralExpr)o).asBigNum.ToIntSafe)); + } + } + return layers.Distinct().OrderBy(l => l).ToList(); + } + + // Look for {:name string} in list of attributes. + public string FindStringAttribute(string name) + { + return QKeyValue.FindStringAttribute(Attributes, name); + } + + public void AddStringAttribute(IToken tok, string name, string parameter) + { + Attributes = new QKeyValue(tok, name, new List() {parameter}, Attributes); + } + + public void CopyIdFrom(IToken tok, ICarriesAttributes src) + { + var id = src.FindStringAttribute("id"); + if (id is not null) { + AddStringAttribute(tok, "id", id); + } + } + + public void CopyIdWithModificationsFrom(IToken tok, ICarriesAttributes src, Func modifier) + { + var id = src.FindStringAttribute("id"); + if (id is not null) { + AddStringAttribute(tok, "id", modifier(id).SolverLabel); + } + } + +} \ No newline at end of file From 34dc968732f2d64354c971a83fba06f9bbc0bba2 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 1 Oct 2024 09:54:30 +0200 Subject: [PATCH 2/8] Move some code into DesugarReturns --- Source/VCGeneration/ConditionGeneration.cs | 122 ---------------- .../Transformations/DesugarReturns.cs | 131 ++++++++++++++++++ .../VerificationConditionGenerator.cs | 6 +- 3 files changed, 134 insertions(+), 125 deletions(-) create mode 100644 Source/VCGeneration/Transformations/DesugarReturns.cs diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 6846a7707..45ff736f7 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -258,74 +258,6 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu } } - /// - /// Modifies an implementation by inserting all postconditions - /// as assert statements at the end of the implementation - /// Returns the possibly-new unified exit block of the implementation - /// - /// - /// The unified exit block that has - /// already been constructed for the implementation (and so - /// is already an element of impl.Blocks) - /// - protected static void InjectPostConditions(VCGenOptions options, ImplementationRun run, Block unifiedExitBlock, - Dictionary gotoCmdOrigins) - { - var impl = run.Implementation; - Contract.Requires(impl != null); - Contract.Requires(unifiedExitBlock != null); - Contract.Requires(gotoCmdOrigins != null); - Contract.Requires(impl.Proc != null); - Contract.Requires(unifiedExitBlock.TransferCmd is ReturnCmd); - - TokenTextWriter debugWriter = null; - if (options.PrintWithUniqueASTIds) - { - debugWriter = new TokenTextWriter("", run.OutputWriter, /*setTokens=*/ false, /*pretty=*/ false, options); - debugWriter.WriteLine("Effective postcondition:"); - } - - Substitution formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap(options)); - - // (free and checked) ensures clauses - foreach (Ensures ens in impl.Proc.Ensures) - { - Contract.Assert(ens != null); - - if (!ens.Free) - { - Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); - Ensures ensCopy = (Ensures) cce.NonNull(ens.Clone()); - ensCopy.Condition = e; - AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy); - c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; - // Copy any {:id ...} from the postcondition to the assumption, so - // we can track it while analyzing verification coverage. - (c as ICarriesAttributes).CopyIdFrom(ens.tok, ens); - unifiedExitBlock.Cmds.Add(c); - if (debugWriter != null) - { - c.Emit(debugWriter, 1); - } - } - else if (ens.CanAlwaysAssume()) - { - Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); - unifiedExitBlock.Cmds.Add(new AssumeCmd(ens.tok, e)); - } - else - { - // skip free ensures if it doesn't have the :always_assume attr - } - } - - if (debugWriter != null) - { - debugWriter.WriteLine(); - } - } - - /// /// Get the pre-condition of an implementation, including the where clauses from the in-parameters. /// @@ -519,60 +451,6 @@ public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool pr } - protected Block GenerateUnifiedExit(Implementation impl, Dictionary gotoCmdOrigins) - { - Contract.Requires(impl != null); - Contract.Requires(gotoCmdOrigins != null); - Contract.Ensures(Contract.Result() != null); - - Contract.Ensures(Contract.Result().TransferCmd is ReturnCmd); - Block /*?*/ - exitBlock = null; - - #region Create a unified exit block, if there's more than one - - { - int returnBlocks = 0; - foreach (Block b in impl.Blocks) - { - if (b.TransferCmd is ReturnCmd) - { - exitBlock = b; - returnBlocks++; - } - } - - if (returnBlocks > 1) - { - string unifiedExitLabel = "GeneratedUnifiedExit"; - var unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), - new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken)); - Contract.Assert(unifiedExit != null); - foreach (Block b in impl.Blocks) - { - if (b.TransferCmd is ReturnCmd returnCmd) - { - List labels = new List(); - labels.Add(unifiedExitLabel); - List bs = new List(); - bs.Add(unifiedExit); - GotoCmd go = new GotoCmd(returnCmd.tok, labels, bs); - gotoCmdOrigins[go] = returnCmd; - b.TransferCmd = go; - unifiedExit.Predecessors.Add(b); - } - } - - exitBlock = unifiedExit; - impl.Blocks.Add(unifiedExit); - } - - Contract.Assert(exitBlock != null); - } - return exitBlock; - - #endregion - } public static void ResetPredecessors(List blocks) { diff --git a/Source/VCGeneration/Transformations/DesugarReturns.cs b/Source/VCGeneration/Transformations/DesugarReturns.cs new file mode 100644 index 000000000..3ee9ad52c --- /dev/null +++ b/Source/VCGeneration/Transformations/DesugarReturns.cs @@ -0,0 +1,131 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Boogie; +using VC; + +namespace VCGeneration.Transformations; + +public static class DesugarReturns { + public static Block GenerateUnifiedExit(Implementation impl, out Dictionary gotoCmdOrigins) + { + Contract.Requires(impl != null); + Contract.Requires(gotoCmdOrigins != null); + Contract.Ensures(Contract.Result() != null); + + gotoCmdOrigins = new(); + Contract.Ensures(Contract.Result().TransferCmd is ReturnCmd); + Block exitBlock = null; + + #region Create a unified exit block, if there's more than one + + { + int returnBlocks = 0; + foreach (Block b in impl.Blocks) + { + if (b.TransferCmd is ReturnCmd) + { + exitBlock = b; + returnBlocks++; + } + } + + if (returnBlocks > 1) + { + string unifiedExitLabel = "GeneratedUnifiedExit"; + var unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), + new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken)); + Contract.Assert(unifiedExit != null); + foreach (Block b in impl.Blocks) + { + if (b.TransferCmd is ReturnCmd returnCmd) + { + List labels = new List(); + labels.Add(unifiedExitLabel); + List bs = new List(); + bs.Add(unifiedExit); + GotoCmd go = new GotoCmd(returnCmd.tok, labels, bs); + gotoCmdOrigins[go] = returnCmd; + b.TransferCmd = go; + unifiedExit.Predecessors.Add(b); + } + } + + exitBlock = unifiedExit; + impl.Blocks.Add(unifiedExit); + } + + Contract.Assert(exitBlock != null); + } + return exitBlock; + + #endregion + } + + /// + /// Modifies an implementation by inserting all postconditions + /// as assert statements at the end of the implementation + /// Returns the possibly-new unified exit block of the implementation + /// + /// + /// The unified exit block that has + /// already been constructed for the implementation (and so + /// is already an element of impl.Blocks) + /// + public static void InjectPostConditions(VCGenOptions options, ImplementationRun run, Block unifiedExitBlock, + Dictionary gotoCmdOrigins) + { + var impl = run.Implementation; + Contract.Requires(impl != null); + Contract.Requires(unifiedExitBlock != null); + Contract.Requires(gotoCmdOrigins != null); + Contract.Requires(impl.Proc != null); + Contract.Requires(unifiedExitBlock.TransferCmd is ReturnCmd); + + TokenTextWriter debugWriter = null; + if (options.PrintWithUniqueASTIds) + { + debugWriter = new TokenTextWriter("", run.OutputWriter, /*setTokens=*/ false, /*pretty=*/ false, options); + debugWriter.WriteLine("Effective postcondition:"); + } + + Substitution formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap(options)); + + // (free and checked) ensures clauses + foreach (Ensures ens in impl.Proc.Ensures) + { + Contract.Assert(ens != null); + + if (!ens.Free) + { + Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); + Ensures ensCopy = (Ensures) cce.NonNull(ens.Clone()); + ensCopy.Condition = e; + AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy); + c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; + // Copy any {:id ...} from the postcondition to the assumption, so + // we can track it while analyzing verification coverage. + (c as ICarriesAttributes).CopyIdFrom(ens.tok, ens); + unifiedExitBlock.Cmds.Add(c); + if (debugWriter != null) + { + c.Emit(debugWriter, 1); + } + } + else if (ens.CanAlwaysAssume()) + { + Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); + unifiedExitBlock.Cmds.Add(new AssumeCmd(ens.tok, e)); + } + else + { + // skip free ensures if it doesn't have the :always_assume attr + } + } + + if (debugWriter != null) + { + debugWriter.WriteLine(); + } + } +} \ No newline at end of file diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index 995d0e23c..78b75181c 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -11,6 +11,7 @@ using System.Threading; using Microsoft.BaseTypes; using Microsoft.Boogie.VCExprAST; +using VCGeneration.Transformations; namespace VC { @@ -1293,8 +1294,7 @@ public Dictionary PassifyImpl(ImplementationRun run, out Contract.Ensures(Contract.Result>() != null); var impl = run.Implementation; - Dictionary gotoCmdOrigins = new Dictionary(); - Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins); + var exitBlock = DesugarReturns.GenerateUnifiedExit(impl, out var gotoCmdOrigins); #region Debug Tracing @@ -1349,7 +1349,7 @@ public Dictionary PassifyImpl(ImplementationRun run, out InjectPreconditions(Options, run, cc); // append postconditions, starting in exitBlock and continuing into other blocks, if needed - InjectPostConditions(Options, run, exitBlock, gotoCmdOrigins); + DesugarReturns.InjectPostConditions(Options, run, exitBlock, gotoCmdOrigins); } #endregion From 0be33398e1ad240c58d291588bd25d77e650ab16 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 2 Oct 2024 13:26:09 +0200 Subject: [PATCH 3/8] Move some files --- Source/VCGeneration/{ => Counterexamples}/CallCounterexample.cs | 0 .../{ => Counterexamples}/CalleeCounterexampleInfo.cs | 0 Source/VCGeneration/{ => Counterexamples}/Counterexample.cs | 0 .../VCGeneration/{ => Counterexamples}/CounterexampleComparer.cs | 0 Source/VCGeneration/{ => Counterexamples}/TraceLocation.cs | 0 5 files changed, 0 insertions(+), 0 deletions(-) rename Source/VCGeneration/{ => Counterexamples}/CallCounterexample.cs (100%) rename Source/VCGeneration/{ => Counterexamples}/CalleeCounterexampleInfo.cs (100%) rename Source/VCGeneration/{ => Counterexamples}/Counterexample.cs (100%) rename Source/VCGeneration/{ => Counterexamples}/CounterexampleComparer.cs (100%) rename Source/VCGeneration/{ => Counterexamples}/TraceLocation.cs (100%) diff --git a/Source/VCGeneration/CallCounterexample.cs b/Source/VCGeneration/Counterexamples/CallCounterexample.cs similarity index 100% rename from Source/VCGeneration/CallCounterexample.cs rename to Source/VCGeneration/Counterexamples/CallCounterexample.cs diff --git a/Source/VCGeneration/CalleeCounterexampleInfo.cs b/Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs similarity index 100% rename from Source/VCGeneration/CalleeCounterexampleInfo.cs rename to Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs diff --git a/Source/VCGeneration/Counterexample.cs b/Source/VCGeneration/Counterexamples/Counterexample.cs similarity index 100% rename from Source/VCGeneration/Counterexample.cs rename to Source/VCGeneration/Counterexamples/Counterexample.cs diff --git a/Source/VCGeneration/CounterexampleComparer.cs b/Source/VCGeneration/Counterexamples/CounterexampleComparer.cs similarity index 100% rename from Source/VCGeneration/CounterexampleComparer.cs rename to Source/VCGeneration/Counterexamples/CounterexampleComparer.cs diff --git a/Source/VCGeneration/TraceLocation.cs b/Source/VCGeneration/Counterexamples/TraceLocation.cs similarity index 100% rename from Source/VCGeneration/TraceLocation.cs rename to Source/VCGeneration/Counterexamples/TraceLocation.cs From c016d95b430912e82cacb52256018be5e49fbe6b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 3 Oct 2024 11:50:35 +0200 Subject: [PATCH 4/8] Refactoring --- Source/Core/VariableDependenceAnalyser.cs | 49 +++++----- .../Transformations/DesugarReturns.cs | 90 +++++++++---------- 2 files changed, 70 insertions(+), 69 deletions(-) diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index 105b7811a..2e0ae6c67 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -515,40 +515,42 @@ private void MakeIgnoreList() private Dictionary> ComputeGlobalControlDependences() { - Dictionary> GlobalCtrlDep = new Dictionary>(); - Dictionary>> LocalCtrlDeps = + var globalCtrlDep = new Dictionary>(); + var localCtrlDeps = new Dictionary>>(); // Work out and union together local control dependences - foreach (var Impl in prog.NonInlinedImplementations()) + foreach (var impl in prog.NonInlinedImplementations()) { - Graph blockGraph = prog.ProcessLoops(options, Impl); - LocalCtrlDeps[Impl] = blockGraph.ControlDependence(new Block(prog.tok)); - foreach (var KeyValue in LocalCtrlDeps[Impl]) + var blockGraph = prog.ProcessLoops(options, impl); + localCtrlDeps[impl] = blockGraph.ControlDependence(new Block(prog.tok)); + foreach (var keyValue in localCtrlDeps[impl]) { - GlobalCtrlDep.Add(KeyValue.Key, KeyValue.Value); + globalCtrlDep.Add(keyValue.Key, keyValue.Value); } } - Graph callGraph = Program.BuildCallGraph(options, prog); + var callGraph = Program.BuildCallGraph(options, prog); // Add inter-procedural control dependence nodes based on calls - foreach (var Impl in prog.NonInlinedImplementations()) + foreach (var impl in prog.NonInlinedImplementations()) { - foreach (var b in Impl.Blocks) + foreach (var b in impl.Blocks) { foreach (var cmd in b.Cmds.OfType()) { - var DirectCallee = GetImplementation(cmd.callee); - if (DirectCallee != null) + var directCallee = GetImplementation(cmd.callee); + if (directCallee == null) { - HashSet IndirectCallees = ComputeIndirectCallees(callGraph, DirectCallee); - foreach (var control in GetControllingBlocks(b, LocalCtrlDeps[Impl])) + continue; + } + + var indirectCallees = ComputeIndirectCallees(callGraph, directCallee); + foreach (var control in GetControllingBlocks(b, localCtrlDeps[impl])) + { + foreach (var c in indirectCallees.Select(Item => Item.Blocks).SelectMany(Item => Item)) { - foreach (var c in IndirectCallees.Select(Item => Item.Blocks).SelectMany(Item => Item)) - { - GlobalCtrlDep[control].Add(c); - } + globalCtrlDep[control].Add(c); } } } @@ -556,22 +558,21 @@ private Dictionary> ComputeGlobalControlDependences() } // Compute transitive closure - GlobalCtrlDep.TransitiveClosure(); + globalCtrlDep.TransitiveClosure(); // Finally reverse the dependences - Dictionary> result = new Dictionary>(); - - foreach (var KeyValue in GlobalCtrlDep) + var result = new Dictionary>(); + foreach (var keyValue in globalCtrlDep) { - foreach (var v in KeyValue.Value) + foreach (var v in keyValue.Value) { if (!result.ContainsKey(v)) { result[v] = new HashSet(); } - result[v].Add(KeyValue.Key); + result[v].Add(keyValue.Key); } } diff --git a/Source/VCGeneration/Transformations/DesugarReturns.cs b/Source/VCGeneration/Transformations/DesugarReturns.cs index 3ee9ad52c..9fc282582 100644 --- a/Source/VCGeneration/Transformations/DesugarReturns.cs +++ b/Source/VCGeneration/Transformations/DesugarReturns.cs @@ -72,60 +72,60 @@ public static Block GenerateUnifiedExit(Implementation impl, out Dictionary - public static void InjectPostConditions(VCGenOptions options, ImplementationRun run, Block unifiedExitBlock, - Dictionary gotoCmdOrigins) + public static void InjectPostConditions(VCGenOptions options, ImplementationRun run, Block unifiedExitBlock, + Dictionary gotoCmdOrigins) + { + var impl = run.Implementation; + Contract.Requires(impl != null); + Contract.Requires(unifiedExitBlock != null); + Contract.Requires(gotoCmdOrigins != null); + Contract.Requires(impl.Proc != null); + Contract.Requires(unifiedExitBlock.TransferCmd is ReturnCmd); + + TokenTextWriter debugWriter = null; + if (options.PrintWithUniqueASTIds) { - var impl = run.Implementation; - Contract.Requires(impl != null); - Contract.Requires(unifiedExitBlock != null); - Contract.Requires(gotoCmdOrigins != null); - Contract.Requires(impl.Proc != null); - Contract.Requires(unifiedExitBlock.TransferCmd is ReturnCmd); + debugWriter = new TokenTextWriter("", run.OutputWriter, /*setTokens=*/ false, /*pretty=*/ false, options); + debugWriter.WriteLine("Effective postcondition:"); + } - TokenTextWriter debugWriter = null; - if (options.PrintWithUniqueASTIds) - { - debugWriter = new TokenTextWriter("", run.OutputWriter, /*setTokens=*/ false, /*pretty=*/ false, options); - debugWriter.WriteLine("Effective postcondition:"); - } + Substitution formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap(options)); - Substitution formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap(options)); + // (free and checked) ensures clauses + foreach (Ensures ens in impl.Proc.Ensures) + { + Contract.Assert(ens != null); - // (free and checked) ensures clauses - foreach (Ensures ens in impl.Proc.Ensures) + if (!ens.Free) { - Contract.Assert(ens != null); - - if (!ens.Free) - { - Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); - Ensures ensCopy = (Ensures) cce.NonNull(ens.Clone()); - ensCopy.Condition = e; - AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy); - c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; - // Copy any {:id ...} from the postcondition to the assumption, so - // we can track it while analyzing verification coverage. - (c as ICarriesAttributes).CopyIdFrom(ens.tok, ens); - unifiedExitBlock.Cmds.Add(c); - if (debugWriter != null) - { - c.Emit(debugWriter, 1); - } - } - else if (ens.CanAlwaysAssume()) + Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); + Ensures ensCopy = (Ensures) cce.NonNull(ens.Clone()); + ensCopy.Condition = e; + AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy); + c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; + // Copy any {:id ...} from the postcondition to the assumption, so + // we can track it while analyzing verification coverage. + (c as ICarriesAttributes).CopyIdFrom(ens.tok, ens); + unifiedExitBlock.Cmds.Add(c); + if (debugWriter != null) { - Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); - unifiedExitBlock.Cmds.Add(new AssumeCmd(ens.tok, e)); - } - else - { - // skip free ensures if it doesn't have the :always_assume attr + c.Emit(debugWriter, 1); } } - - if (debugWriter != null) + else if (ens.CanAlwaysAssume()) { - debugWriter.WriteLine(); + Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); + unifiedExitBlock.Cmds.Add(new AssumeCmd(ens.tok, e)); } + else + { + // skip free ensures if it doesn't have the :always_assume attr + } + } + + if (debugWriter != null) + { + debugWriter.WriteLine(); } + } } \ No newline at end of file From 5e6c0a9cd02804446def694529107f8c868daadd Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 3 Oct 2024 11:53:08 +0200 Subject: [PATCH 5/8] Refactoring --- Source/Graph/Graph.cs | 14 +++++++------- Source/Houdini/Houdini.cs | 2 +- Source/Houdini/HoudiniSession.cs | 4 ++-- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 3c3b8ab53..2738566dd 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -99,22 +99,22 @@ public bool DominatedBy(Node dominee, Node dominator, List path = null) return true; } - int currentNodeNum = nodeNumberToImmediateDominator[domineeNum]; + int currentDominatorNum = nodeNumberToImmediateDominator[domineeNum]; while (true) { - if (currentNodeNum == dominatorNum) + if (currentDominatorNum == dominatorNum) { return true; } - if (currentNodeNum == sourceNum) + if (currentDominatorNum == sourceNum) { return false; } - path?.Add(postOrderNumberToNode[currentNodeNum]); + path?.Add(postOrderNumberToNode[currentDominatorNum]); - currentNodeNum = nodeNumberToImmediateDominator[currentNodeNum]; + currentDominatorNum = nodeNumberToImmediateDominator[currentDominatorNum]; } } @@ -429,8 +429,8 @@ public class Graph private HashSet splitCandidates; private DomRelation dominatorMap = null; - private Dictionary> predCache = new Dictionary>(); - private Dictionary> succCache = new Dictionary>(); + private Dictionary> predCache = new(); + private Dictionary> succCache = new(); private bool predComputed; [ContractInvariantMethod] diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 7a74a1f5d..4efc13c77 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -491,7 +491,7 @@ protected void Initialize(TextWriter traceWriter, Program program, HoudiniSessio } var session = new HoudiniSession(this, vcgen, proverInterface, program, - new ImplementationRun(impl, traceWriter), stats, taskID: GetTaskID()); + new ImplementationRun(impl, traceWriter), stats, taskId: GetTaskID()); houdiniSessions.Add(impl, session); } catch (VCGenException) diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 35dcfe685..885c4ac98 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -157,7 +157,7 @@ public bool InUnsatCore(Variable constant) } public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, ProverInterface proverInterface, Program program, - ImplementationRun run, HoudiniStatistics stats, int taskID = -1) + ImplementationRun run, HoudiniStatistics stats, int taskId = -1) { var impl = run.Implementation; this.Description = impl.Name; @@ -166,7 +166,7 @@ public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, Pro collector = new VerificationResultCollector(houdini.Options); collector.OnProgress?.Invoke("HdnVCGen", 0, 0, 0.0); - vcgen.ConvertCFG2DAG(run, taskID: taskID); + vcgen.ConvertCFG2DAG(run, taskID: taskId); var gotoCmdOrigins = vcgen.PassifyImpl(run, out var mvInfo); ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl, out var ecollector); From dab644298adbaac1fae32e46be88258e47b28cd2 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 2 Oct 2024 15:39:32 +0200 Subject: [PATCH 6/8] Extract some code into file RemoveBackEdges --- Source/Core/AST/ICarriesAttributes.cs | 15 +- Source/Houdini/HoudiniSession.cs | 3 +- Source/VCGeneration/ConditionGeneration.cs | 18 +- Source/VCGeneration/StratifiedVC.cs | 5 +- .../Transformations/RemoveBackEdges.cs | 607 +++++++++++++++++ .../VerificationConditionGenerator.cs | 632 +----------------- 6 files changed, 634 insertions(+), 646 deletions(-) create mode 100644 Source/VCGeneration/Transformations/RemoveBackEdges.cs diff --git a/Source/Core/AST/ICarriesAttributes.cs b/Source/Core/AST/ICarriesAttributes.cs index 747d56c41..c0e88bf7d 100644 --- a/Source/Core/AST/ICarriesAttributes.cs +++ b/Source/Core/AST/ICarriesAttributes.cs @@ -51,20 +51,25 @@ public void AddStringAttribute(IToken tok, string name, string parameter) Attributes = new QKeyValue(tok, name, new List() {parameter}, Attributes); } - public void CopyIdFrom(IToken tok, ICarriesAttributes src) +} + +public static class CarriesAttributesExtensions +{ + + + public static void CopyIdFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src) { var id = src.FindStringAttribute("id"); if (id is not null) { - AddStringAttribute(tok, "id", id); + dest.AddStringAttribute(tok, "id", id); } } - public void CopyIdWithModificationsFrom(IToken tok, ICarriesAttributes src, Func modifier) + public static void CopyIdWithModificationsFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src, Func modifier) { var id = src.FindStringAttribute("id"); if (id is not null) { - AddStringAttribute(tok, "id", modifier(id).SolverLabel); + dest.AddStringAttribute(tok, "id", modifier(id).SolverLabel); } } - } \ No newline at end of file diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 885c4ac98..ee24e7bfa 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -8,6 +8,7 @@ using System.Linq; using System.Threading; using System.Threading.Tasks; +using VCGeneration.Transformations; namespace Microsoft.Boogie.Houdini { @@ -166,7 +167,7 @@ public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, Pro collector = new VerificationResultCollector(houdini.Options); collector.OnProgress?.Invoke("HdnVCGen", 0, 0, 0.0); - vcgen.ConvertCFG2DAG(run, taskID: taskId); + new RemoveBackEdges(vcgen).ConvertCfg2Dag(run, taskID: taskId); var gotoCmdOrigins = vcgen.PassifyImpl(run, out var mvInfo); ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl, out var ecollector); diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 45ff736f7..e1c9064a5 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -66,7 +66,7 @@ public static VcOutcome ProverInterfaceOutcomeToConditionGenerationOutcome(Solve [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullDictionaryAndValues(incarnationOriginMap)); + Contract.Invariant(cce.NonNullDictionaryAndValues(IncarnationOriginMap)); Contract.Invariant(program != null); } @@ -81,9 +81,9 @@ void ObjectInvariant() public List CurrentLocalVariables { get; set; } = null; // shared across each implementation; created anew for each implementation - protected Dictionary variable2SequenceNumber; + public Dictionary Variable2SequenceNumber; - public Dictionary incarnationOriginMap = new Dictionary(); + public Dictionary IncarnationOriginMap = new(); public Program program; public CheckerPool CheckerPool { get; } @@ -474,7 +474,7 @@ public static void ResetPredecessors(List blocks) protected Variable CreateIncarnation(Variable x, Absy a) { - Contract.Requires(this.variable2SequenceNumber != null); + Contract.Requires(this.Variable2SequenceNumber != null); Contract.Requires(this.CurrentLocalVariables != null); Contract.Requires(a is Block || a is AssignCmd || a is HavocCmd); @@ -482,13 +482,13 @@ protected Variable CreateIncarnation(Variable x, Absy a) Contract.Ensures(Contract.Result() != null); int currentIncarnationNumber = - variable2SequenceNumber.ContainsKey(x) - ? variable2SequenceNumber[x] + Variable2SequenceNumber.ContainsKey(x) + ? Variable2SequenceNumber[x] : -1; Variable v = new Incarnation(x, currentIncarnationNumber + 1); - variable2SequenceNumber[x] = currentIncarnationNumber + 1; + Variable2SequenceNumber[x] = currentIncarnationNumber + 1; CurrentLocalVariables.Add(v); - incarnationOriginMap.Add((Incarnation) v, a); + IncarnationOriginMap.Add((Incarnation) v, a); return v; } @@ -1382,7 +1382,7 @@ NAryExpr TypedExprEq(Expr e0, Expr e1, bool doNotResolveOverloading = false) /// Creates a new block to add to impl.Blocks, where impl is the implementation that contains /// succ. Caller must do the add to impl.Blocks. /// - protected Block CreateBlockBetween(int predIndex, Block succ) + public Block CreateBlockBetween(int predIndex, Block succ) { Contract.Requires(0 <= predIndex && predIndex < succ.Predecessors.Count); diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index aa080b4af..6bfbfd7ca 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -7,6 +7,7 @@ using System.Diagnostics.Contracts; using Microsoft.BaseTypes; using Microsoft.Boogie.VCExprAST; +using VCGeneration.Transformations; namespace VC { @@ -485,7 +486,7 @@ public void GenerateVCBoolControl() // Passify Program program = vcgen.program; ProverInterface proverInterface = vcgen.prover; - vcgen.ConvertCFG2DAG(run); + new RemoveBackEdges(vcgen).ConvertCfg2Dag(run); vcgen.PassifyImpl(run, out mvInfo); VCExpressionGenerator gen = proverInterface.VCExprGen; @@ -633,7 +634,7 @@ public void GenerateVC() Program program = vcgen.program; ProverInterface proverInterface = vcgen.prover; - vcgen.ConvertCFG2DAG(run); + new RemoveBackEdges(vcgen).ConvertCfg2Dag(run); vcgen.PassifyImpl(run, out mvInfo); VCExpressionGenerator gen = proverInterface.VCExprGen; diff --git a/Source/VCGeneration/Transformations/RemoveBackEdges.cs b/Source/VCGeneration/Transformations/RemoveBackEdges.cs new file mode 100644 index 000000000..d8a43e66b --- /dev/null +++ b/Source/VCGeneration/Transformations/RemoveBackEdges.cs @@ -0,0 +1,607 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using System.Diagnostics.Contracts; +using Microsoft.Boogie; +using Microsoft.Boogie.GraphUtil; +using VC; + +namespace VCGeneration.Transformations; + +public class RemoveBackEdges { + private VerificationConditionGenerator generator; + + public RemoveBackEdges(VerificationConditionGenerator generator) { + this.generator = generator; + } + + public void ConvertCfg2Dag(ImplementationRun run, Dictionary> edgesCut = null, int taskID = -1) + { + var impl = run.Implementation; + Contract.Requires(impl != null); + impl.PruneUnreachableBlocks(generator.Options); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization + + generator.CurrentLocalVariables = impl.LocVars; + generator.Variable2SequenceNumber = new Dictionary(); + generator.IncarnationOriginMap = new Dictionary(); + + #region Debug Tracing + + if (generator.Options.TraceVerify) + { + run.OutputWriter.WriteLine("original implementation"); + ConditionGeneration.EmitImpl(generator.Options, run, false); + } + + #endregion + + #region Debug Tracing + + if (generator.Options.TraceVerify) + { + run.OutputWriter.WriteLine("after desugaring sugared commands like procedure calls"); + ConditionGeneration.EmitImpl(generator.Options, run, true); + } + + #endregion + + // Recompute the predecessors, but first insert a dummy start node that is sure not to be the target of any goto (because the cutting of back edges + // below assumes that the start node has no predecessor) + impl.Blocks.Insert(0, + new Block(Token.NoToken, "0", new List(), + new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] }))); + ConditionGeneration.ResetPredecessors(impl.Blocks); + + var k = Math.Max(generator.Options.KInductionDepth, + QKeyValue.FindIntAttribute(impl.Attributes, "kInductionDepth", -1)); + if (k < 0) + { + ConvertCfg2DagStandard(impl, edgesCut, taskID); + } + else + { + ConvertCfg2DagkInduction(impl, edgesCut, taskID, k); + } + + #region Debug Tracing + + if (generator.Options.TraceVerify) + { + run.OutputWriter.WriteLine("after conversion into a DAG"); + ConditionGeneration.EmitImpl(generator.Options, run, true); + } + + #endregion + } + + private void ConvertCfg2DagStandard(Implementation impl, Dictionary> edgesCut, int taskID) + { + #region Convert program CFG into a DAG + + #region Use the graph library to figure out where the (natural) loops are + + #region Create the graph by adding the source node and each edge + + Graph g = Program.GraphFromImpl(impl); + + #endregion + + //Graph g = program.ProcessLoops(impl); + + g.ComputeLoops(); // this is the call that does all of the processing + if (!g.Reducible) + { + throw new VCGenException("Irreducible flow graphs are unsupported."); + } + + #endregion + + #region Cut the backedges, push assert/assume statements from loop header into predecessors, change them all into assume statements at top of loop, introduce havoc statements + + foreach (Block header in cce.NonNull(g.Headers)) + { + Contract.Assert(header != null); + IDictionary backEdgeNodes = new Dictionary(); + foreach (Block b in cce.NonNull(g.BackEdgeNodes(header))) + { + Contract.Assert(b != null); + backEdgeNodes.Add(b, null); + } + + #region Find the (possibly empty) prefix of assert commands in the header, replace each assert with an assume of the same condition + + List prefixOfPredicateCmdsInit = new List(); + List prefixOfPredicateCmdsMaintained = new List(); + for (int i = 0, n = header.Cmds.Count; i < n; i++) { + if (header.Cmds[i] is not PredicateCmd predicateCmd) { + if (header.Cmds[i] is CommentCmd) { + // ignore + continue; + } + + break; // stop when an assignment statement (or any other non-predicate cmd) is encountered + } + + if (predicateCmd is AssertCmd assertCmd) { + AssertCmd initAssertCmd; + + if (generator.Options.ConcurrentHoudini) { + Contract.Assert(taskID >= 0); + initAssertCmd = generator.Options.Cho[taskID].DisableLoopInvEntryAssert + ? new LoopInitAssertCmd(assertCmd.tok, Expr.True, assertCmd) + : new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); + } else { + initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); + } + + initAssertCmd.Attributes = (QKeyValue)assertCmd.Attributes?.Clone(); + // Copy any {:id ...} from the invariant to the assertion that it's established, so + // we can track it while analyzing verification coverage. + initAssertCmd.CopyIdWithModificationsFrom(assertCmd.tok, assertCmd, + id => new TrackedInvariantEstablished(id)); + + prefixOfPredicateCmdsInit.Add(initAssertCmd); + + LoopInvMaintainedAssertCmd maintainedAssertCmd; + if (generator.Options.ConcurrentHoudini) { + Contract.Assert(taskID >= 0); + maintainedAssertCmd = generator.Options.Cho[taskID].DisableLoopInvMaintainedAssert + ? new LoopInvMaintainedAssertCmd(assertCmd.tok, Expr.True, assertCmd) + : new LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); + } else { + maintainedAssertCmd = new LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); + } + + maintainedAssertCmd.Attributes = (QKeyValue)assertCmd.Attributes?.Clone(); + // Copy any {:id ...} from the invariant to the assertion that it's maintained, so + // we can track it while analyzing verification coverage. + (maintainedAssertCmd as ICarriesAttributes).CopyIdWithModificationsFrom(assertCmd.tok, assertCmd, + id => new TrackedInvariantMaintained(id)); + + prefixOfPredicateCmdsMaintained.Add(maintainedAssertCmd); + AssumeCmd assume = new AssumeCmd(assertCmd.tok, assertCmd.Expr); + // Copy any {:id ...} from the invariant to the assumption used within the body, so + // we can track it while analyzing verification coverage. + assume.CopyIdWithModificationsFrom(assertCmd.tok, assertCmd, + id => new TrackedInvariantAssumed(id)); + + header.Cmds[i] = assume; + } else { + Contract.Assert(predicateCmd is AssumeCmd); + if (generator.Options.AlwaysAssumeFreeLoopInvariants) { + // Usually, "free" stuff, like free loop invariants (and the assume statements + // that stand for such loop invariants) are ignored on the checking side. This + // command-line option changes that behavior to always assume the conditions. + prefixOfPredicateCmdsInit.Add(predicateCmd); + prefixOfPredicateCmdsMaintained.Add(predicateCmd); + } + } + } + + #endregion + + #region Copy the prefix of predicate commands into each predecessor. Do this *before* cutting the backedge!! + + for (int predIndex = 0, n = header.Predecessors.Count; predIndex < n; predIndex++) + { + Block pred = cce.NonNull(header.Predecessors[predIndex]); + + // Create a block between header and pred for the predicate commands if pred has more than one successor + GotoCmd gotocmd = cce.NonNull((GotoCmd)pred.TransferCmd); + Contract.Assert(gotocmd.LabelNames != + null); // if "pred" is really a predecessor, it may be a GotoCmd with at least one label + if (gotocmd.LabelNames.Count > 1) + { + Block newBlock = generator.CreateBlockBetween(predIndex, header); + impl.Blocks.Add(newBlock); + + // if pred is a back edge node, then now newBlock is the back edge node + if (backEdgeNodes.ContainsKey(pred)) + { + backEdgeNodes.Remove(pred); + backEdgeNodes.Add(newBlock, null); + } + + pred = newBlock; + } + + // Add the predicate commands + if (backEdgeNodes.ContainsKey(pred)) + { + pred.Cmds.AddRange(prefixOfPredicateCmdsMaintained); + } + else + { + pred.Cmds.AddRange(prefixOfPredicateCmdsInit); + } + } + + #endregion + + #region Cut the back edge + + foreach (Block backEdgeNode in cce.NonNull(backEdgeNodes.Keys)) + { + Contract.Assert(backEdgeNode != null); + Debug.Assert(backEdgeNode.TransferCmd is GotoCmd, + "An node was identified as the source for a backedge, but it does not have a goto command."); + GotoCmd gotoCmd = backEdgeNode.TransferCmd as GotoCmd; + if (gotoCmd is { LabelTargets.Count: > 1 }) + { + // then remove the backedge by removing the target block from the list of gotos + List remainingTargets = new List(); + List remainingLabels = new List(); + Contract.Assume(gotoCmd.LabelNames != null); + for (int i = 0, n = gotoCmd.LabelTargets.Count; i < n; i++) + { + if (gotoCmd.LabelTargets[i] != header) + { + remainingTargets.Add(gotoCmd.LabelTargets[i]); + remainingLabels.Add(gotoCmd.LabelNames[i]); + } + else + { + RecordCutEdge(edgesCut, backEdgeNode, header); + } + } + + gotoCmd.LabelTargets = remainingTargets; + gotoCmd.LabelNames = remainingLabels; + } + else + { + // This backedge is the only out-going edge from this node. + // Add an "assume false" statement to the end of the statements + // inside of the block and change the goto command to a return command. + var ac = new AssumeCmd(Token.NoToken, Expr.False); + backEdgeNode.Cmds.Add(ac); + backEdgeNode.TransferCmd = new ReturnCmd(backEdgeNode.TransferCmd.tok); + if (gotoCmd is { LabelTargets.Count: 1 }) + { + RecordCutEdge(edgesCut, backEdgeNode, gotoCmd.LabelTargets[0]); + } + } + + #region Remove the backedge node from the list of predecessor nodes in the header + + List newPreds = new List(); + foreach (Block p in header.Predecessors) + { + if (p != backEdgeNode) + { + newPreds.Add(p); + } + } + + header.Predecessors = newPreds; + + #endregion + } + + #endregion + + #region Collect all variables that are assigned to in all of the natural loops for which this is the header + + List varsToHavoc = VarsAssignedInLoop(g, header); + 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 + HavocCmd hc = new HavocCmd(header.tok, havocExprs); + List newCmds = new List(); + newCmds.Add(hc); + foreach (Cmd c in header.Cmds) + { + newCmds.Add(c); + } + + header.Cmds = newCmds; + + #endregion + } + + #endregion + + #endregion Convert program CFG into a DAG + } + + private void ConvertCfg2DagkInduction(Implementation impl, Dictionary> edgesCut, int taskID, + int inductionK) + { + // K-induction has not been adapted to be aware of these parameters which standard CFG to DAG transformation uses + Contract.Requires(edgesCut == null); + Contract.Requires(taskID == -1); + Contract.Requires(0 <= inductionK); + + bool contRuleApplication = true; + while (contRuleApplication) + { + contRuleApplication = false; + + #region Use the graph library to figure out where the (natural) loops are + + #region Create the graph by adding the source node and each edge + + Graph g = Program.GraphFromImpl(impl); + + #endregion + + g.ComputeLoops(); // this is the call that does all of the processing + if (!g.Reducible) + { + throw new VCGenException("Irreducible flow graphs are unsupported."); + } + + #endregion + + foreach (Block header in cce.NonNull(g.Headers)) + { + Contract.Assert(header != null); + + #region Debug Tracing + + if (generator.Options.TraceVerify) + { + generator.Options.OutputWriter.WriteLine("Applying k-induction rule with k=" + inductionK); + } + + #endregion + + #region generate the step case + + Block newHeader = DuplicateLoop(impl, g, header, null, + false, false, "_step_assertion"); + for (int i = 0; i < inductionK; ++i) + { + newHeader = DuplicateLoop(impl, g, header, newHeader, + true, true, + "_step_" + (inductionK - i)); + } + + #endregion + + #region havoc variables that can be assigned in the loop + + List varsToHavoc = VarsAssignedInLoop(g, header); + 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 + HavocCmd hc = new HavocCmd(newHeader.tok, havocExprs); + List havocCmds = new List(); + havocCmds.Add(hc); + + var havocBlock = new Block(newHeader.tok, newHeader.Label + "_havoc", havocCmds, + new GotoCmd(newHeader.tok, new List { newHeader })); + + impl.Blocks.Add(havocBlock); + newHeader.Predecessors.Add(havocBlock); + newHeader = havocBlock; + + #endregion + + #region generate the base case loop copies + + for (int i = 0; i < inductionK; ++i) + { + newHeader = DuplicateLoop(impl, g, header, newHeader, + false, false, + "_base_" + (inductionK - i)); + } + + #endregion + + #region redirect into the new loop copies and remove the original loop (but don't redirect back-edges) + + IDictionary backEdgeNodes = new Dictionary(); + foreach (Block b in cce.NonNull(g.BackEdgeNodes(header))) + { + Contract.Assert(b != null); + backEdgeNodes.Add(b, null); + } + + for (int predIndex = 0, n = header.Predecessors.Count; predIndex < n; predIndex++) + { + Block pred = cce.NonNull(header.Predecessors[predIndex]); + if (!backEdgeNodes.ContainsKey(pred)) + { + GotoCmd gc = pred.TransferCmd as GotoCmd; + Contract.Assert(gc != null); + for (int i = 0; i < gc.LabelTargets.Count; ++i) + { + if (gc.LabelTargets[i] == header) + { + gc.LabelTargets[i] = newHeader; + gc.LabelNames[i] = newHeader.Label; + newHeader.Predecessors.Add(pred); + } + } + } + } + + impl.PruneUnreachableBlocks(generator.Options); + + #endregion + + contRuleApplication = true; + break; + } + } + + ConditionGeneration.ResetPredecessors(impl.Blocks); + impl.FreshenCaptureStates(); + } + + private static void RecordCutEdge(Dictionary> edgesCut, Block from, Block to) { + edgesCut?.GetOrCreate(from, () => new List()).Add(to); + } + + private static List VarsAssignedInLoop(Graph g, Block header) + { + List varsToHavoc = new List(); + foreach (var backEdgeNode in cce.NonNull(g.BackEdgeNodes(header))) + { + Contract.Assert(backEdgeNode != null); + foreach (Block b in g.NaturalLoops(header, backEdgeNode)) + { + Contract.Assert(b != null); + foreach (var c in b.Cmds) + { + Contract.Assert(c != null); + varsToHavoc.AddRange(c.GetAssignedVariables()); + } + } + } + + return varsToHavoc; + } + + public static IEnumerable VarsReferencedInLoop(Graph g, Block header) + { + HashSet referencedVars = new HashSet(); + foreach (Block backEdgeNode in cce.NonNull(g.BackEdgeNodes(header))) + { + Contract.Assert(backEdgeNode != null); + foreach (Block b in g.NaturalLoops(header, backEdgeNode)) + { + Contract.Assert(b != null); + foreach (Cmd c in b.Cmds) + { + Contract.Assert(c != null); + var Collector = new VariableCollector(); + Collector.Visit(c); + foreach (var v in Collector.usedVars) + { + referencedVars.Add(v); + } + } + } + } + + return referencedVars; + } + + private Block DuplicateLoop(Implementation impl, Graph g, + Block header, Block nextHeader, bool cutExits, + bool toAssumptions, string suffix) + { + var ori2CopiedBlocks = new Dictionary(); + var duplicator = new Duplicator(); + + #region create copies of all blocks in the loop + + foreach (Block backEdgeNode in cce.NonNull(g.BackEdgeNodes(header))) + { + Contract.Assert(backEdgeNode != null); + foreach (Block b in g.NaturalLoops(header, backEdgeNode)) + { + Contract.Assert(b != null); + if (ori2CopiedBlocks.ContainsKey(b)) { + continue; + } + + Block copy = (Block)duplicator.Visit(b); + copy.Cmds = new List(copy + .Cmds); // Philipp Ruemmer commented that this was necessary due to a bug in the Duplicator. That was a long time; worth checking whether this has been fixed + copy.Predecessors = new List(); + copy.Label += suffix; + + #region turn asserts into assumptions + + if (toAssumptions) + { + for (int i = 0; i < copy.Cmds.Count; ++i) + { + if (copy.Cmds[i] is AssertCmd ac) + { + copy.Cmds[i] = new AssumeCmd(ac.tok, ac.Expr); + } + } + } + + #endregion + + impl.Blocks.Add(copy); + ori2CopiedBlocks.Add(b, copy); + } + } + + #endregion + + #region adjust the transfer commands of the newly created blocks + + foreach (KeyValuePair pair in ori2CopiedBlocks) + { + var copy = pair.Value; + if (copy.TransferCmd is GotoCmd gc) + { + List newTargets = new List(); + List newLabels = new List(); + + for (int i = 0; i < gc.LabelTargets.Count; ++i) + { + if (gc.LabelTargets[i] == header) + { + if (nextHeader != null) + { + newTargets.Add(nextHeader); + newLabels.Add(nextHeader.Label); + nextHeader.Predecessors.Add(copy); + } + } + else if (ori2CopiedBlocks.TryGetValue(gc.LabelTargets[i], out var newTarget)) + { + newTargets.Add(newTarget); + newLabels.Add(newTarget.Label); + newTarget.Predecessors.Add(copy); + } + else if (!cutExits) + { + newTargets.Add(gc.LabelTargets[i]); + newLabels.Add(gc.LabelNames[i]); + gc.LabelTargets[i].Predecessors.Add(copy); + } + } + + if (newTargets.Count == 0) + { + // if no targets are left, we assume false and return + copy.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); + copy.TransferCmd = new ReturnCmd(Token.NoToken); + } + else + { + copy.TransferCmd = new GotoCmd(gc.tok, newLabels, newTargets); + } + } + else if (cutExits && (copy.TransferCmd is ReturnCmd)) + { + // because return is a kind of exit from the loop, we + // assume false to cut this path + copy.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); + } + } + + #endregion + + return ori2CopiedBlocks[header]; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index 78b75181c..507b01733 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -108,8 +108,8 @@ public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List(); - vcgen.incarnationOriginMap = new Dictionary(); + vcgen.Variable2SequenceNumber = new Dictionary(); + vcgen.IncarnationOriginMap = new Dictionary(); vcgen.CurrentLocalVariables = codeExpr.LocVars; ResetPredecessors(codeExpr.Blocks); @@ -434,7 +434,7 @@ public void PrepareImplementation(ImplementationRun run, VerifierCallback callba if (!data.ConvertedToDAG) { data.ConvertedToDAG = true; - ConvertCFG2DAG(run); + new RemoveBackEdges(this).ConvertCfg2Dag(run); } smokeTester = null; @@ -633,632 +633,6 @@ public override void OnProverWarning(string msg) } } - 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(ImplementationRun run, Dictionary> edgesCut = null, int taskID = -1) - { - var impl = run.Implementation; - Contract.Requires(impl != null); - impl.PruneUnreachableBlocks( - Options); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization - - CurrentLocalVariables = impl.LocVars; - variable2SequenceNumber = new Dictionary(); - incarnationOriginMap = new Dictionary(); - - #region Debug Tracing - - if (Options.TraceVerify) - { - run.OutputWriter.WriteLine("original implementation"); - EmitImpl(Options, run, false); - } - - #endregion - - #region Debug Tracing - - if (Options.TraceVerify) - { - run.OutputWriter.WriteLine("after desugaring sugared commands like procedure calls"); - EmitImpl(Options, run, true); - } - - #endregion - - // Recompute the predecessors, but first insert a dummy start node that is sure not to be the target of any goto (because the cutting of back edges - // below assumes that the start node has no predecessor) - impl.Blocks.Insert(0, - new Block(new Token(-17, -4), "0", new List(), - new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] }))); - ResetPredecessors(impl.Blocks); - - var k = Math.Max(Options.KInductionDepth, - QKeyValue.FindIntAttribute(impl.Attributes, "kInductionDepth", -1)); - if (k < 0) - { - ConvertCFG2DAGStandard(impl, edgesCut, taskID); - } - else - { - ConvertCFG2DAGKInduction(impl, edgesCut, taskID, k); - } - - #region Debug Tracing - - if (Options.TraceVerify) - { - run.OutputWriter.WriteLine("after conversion into a DAG"); - EmitImpl(Options, run, true); - } - - #endregion - } - - private void ConvertCFG2DAGStandard(Implementation impl, Dictionary> edgesCut, int taskID) - { - #region Convert program CFG into a DAG - - #region Use the graph library to figure out where the (natural) loops are - - #region Create the graph by adding the source node and each edge - - Graph g = Program.GraphFromImpl(impl); - - #endregion - - //Graph g = program.ProcessLoops(impl); - - g.ComputeLoops(); // this is the call that does all of the processing - if (!g.Reducible) - { - throw new VCGenException("Irreducible flow graphs are unsupported."); - } - - #endregion - - #region Cut the backedges, push assert/assume statements from loop header into predecessors, change them all into assume statements at top of loop, introduce havoc statements - - foreach (Block header in cce.NonNull(g.Headers)) - { - Contract.Assert(header != null); - IDictionary backEdgeNodes = new Dictionary(); - foreach (Block b in cce.NonNull(g.BackEdgeNodes(header))) - { - Contract.Assert(b != null); - backEdgeNodes.Add(b, null); - } - - #region Find the (possibly empty) prefix of assert commands in the header, replace each assert with an assume of the same condition - - List prefixOfPredicateCmdsInit = new List(); - List prefixOfPredicateCmdsMaintained = new List(); - for (int i = 0, n = header.Cmds.Count; i < n; i++) - { - PredicateCmd predicateCmd = header.Cmds[i] as PredicateCmd; - if (predicateCmd != null) - { - if (predicateCmd is AssertCmd) - { - AssertCmd assertCmd = (AssertCmd)predicateCmd; - AssertCmd initAssertCmd = null; - - if (Options.ConcurrentHoudini) - { - Contract.Assert(taskID >= 0); - if (Options.Cho[taskID].DisableLoopInvEntryAssert) - { - initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, Expr.True, assertCmd); - } - else - { - initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); - } - } - else - { - initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); - } - - initAssertCmd.Attributes = (QKeyValue)assertCmd.Attributes?.Clone(); - // Copy any {:id ...} from the invariant to the assertion that it's established, so - // we can track it while analyzing verification coverage. - (initAssertCmd as ICarriesAttributes).CopyIdWithModificationsFrom(assertCmd.tok, assertCmd, - id => new TrackedInvariantEstablished(id)); - - prefixOfPredicateCmdsInit.Add(initAssertCmd); - - LoopInvMaintainedAssertCmd maintainedAssertCmd; - if (Options.ConcurrentHoudini) - { - Contract.Assert(taskID >= 0); - if (Options.Cho[taskID].DisableLoopInvMaintainedAssert) - { - maintainedAssertCmd = new Bpl.LoopInvMaintainedAssertCmd(assertCmd.tok, Expr.True, assertCmd); - } - else - { - maintainedAssertCmd = new Bpl.LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); - } - } - else - { - maintainedAssertCmd = new Bpl.LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); - } - - maintainedAssertCmd.Attributes = (QKeyValue)assertCmd.Attributes?.Clone(); - // Copy any {:id ...} from the invariant to the assertion that it's maintained, so - // we can track it while analyzing verification coverage. - (maintainedAssertCmd as ICarriesAttributes).CopyIdWithModificationsFrom(assertCmd.tok, assertCmd, - id => new TrackedInvariantMaintained(id)); - - prefixOfPredicateCmdsMaintained.Add(maintainedAssertCmd); - AssumeCmd assume = new AssumeCmd(assertCmd.tok, assertCmd.Expr); - // Copy any {:id ...} from the invariant to the assumption used within the body, so - // we can track it while analyzing verification coverage. - (assume as ICarriesAttributes).CopyIdWithModificationsFrom(assertCmd.tok, assertCmd, - id => new TrackedInvariantAssumed(id)); - - header.Cmds[i] = assume; - } - else - { - Contract.Assert(predicateCmd is AssumeCmd); - if (Options.AlwaysAssumeFreeLoopInvariants) - { - // Usually, "free" stuff, like free loop invariants (and the assume statements - // that stand for such loop invariants) are ignored on the checking side. This - // command-line option changes that behavior to always assume the conditions. - prefixOfPredicateCmdsInit.Add(predicateCmd); - prefixOfPredicateCmdsMaintained.Add(predicateCmd); - } - } - } - else if (header.Cmds[i] is CommentCmd) - { - // ignore - } - else - { - break; // stop when an assignment statement (or any other non-predicate cmd) is encountered - } - } - - #endregion - - #region Copy the prefix of predicate commands into each predecessor. Do this *before* cutting the backedge!! - - for (int predIndex = 0, n = header.Predecessors.Count; predIndex < n; predIndex++) - { - Block pred = cce.NonNull(header.Predecessors[predIndex]); - - // Create a block between header and pred for the predicate commands if pred has more than one successor - GotoCmd gotocmd = cce.NonNull((GotoCmd)pred.TransferCmd); - Contract.Assert(gotocmd.LabelNames != - null); // if "pred" is really a predecessor, it may be a GotoCmd with at least one label - if (gotocmd.LabelNames.Count > 1) - { - Block newBlock = CreateBlockBetween(predIndex, header); - impl.Blocks.Add(newBlock); - - // if pred is a back edge node, then now newBlock is the back edge node - if (backEdgeNodes.ContainsKey(pred)) - { - backEdgeNodes.Remove(pred); - backEdgeNodes.Add(newBlock, null); - } - - pred = newBlock; - } - - // Add the predicate commands - if (backEdgeNodes.ContainsKey(pred)) - { - pred.Cmds.AddRange(prefixOfPredicateCmdsMaintained); - } - else - { - pred.Cmds.AddRange(prefixOfPredicateCmdsInit); - } - } - - #endregion - - #region Cut the back edge - - foreach (Block backEdgeNode in cce.NonNull(backEdgeNodes.Keys)) - { - Contract.Assert(backEdgeNode != null); - Debug.Assert(backEdgeNode.TransferCmd is GotoCmd, - "An node was identified as the source for a backedge, but it does not have a goto command."); - GotoCmd gtc = backEdgeNode.TransferCmd as GotoCmd; - if (gtc != null && gtc.LabelTargets != null && gtc.LabelTargets.Count > 1) - { - // then remove the backedge by removing the target block from the list of gotos - List remainingTargets = new List(); - List remainingLabels = new List(); - Contract.Assume(gtc.LabelNames != null); - for (int i = 0, n = gtc.LabelTargets.Count; i < n; i++) - { - if (gtc.LabelTargets[i] != header) - { - remainingTargets.Add(gtc.LabelTargets[i]); - remainingLabels.Add(gtc.LabelNames[i]); - } - else - { - RecordCutEdge(edgesCut, backEdgeNode, header); - } - } - - gtc.LabelTargets = remainingTargets; - gtc.LabelNames = remainingLabels; - } - else - { - // This backedge is the only out-going edge from this node. - // Add an "assume false" statement to the end of the statements - // inside of the block and change the goto command to a return command. - AssumeCmd ac = new AssumeCmd(Token.NoToken, Expr.False); - backEdgeNode.Cmds.Add(ac); - backEdgeNode.TransferCmd = new ReturnCmd(Token.NoToken); - if (gtc != null && gtc.LabelTargets != null && gtc.LabelTargets.Count == 1) - { - RecordCutEdge(edgesCut, backEdgeNode, gtc.LabelTargets[0]); - } - } - - #region Remove the backedge node from the list of predecessor nodes in the header - - List newPreds = new List(); - foreach (Block p in header.Predecessors) - { - if (p != backEdgeNode) - { - newPreds.Add(p); - } - } - - header.Predecessors = newPreds; - - #endregion - } - - #endregion - - #region Collect all variables that are assigned to in all of the natural loops for which this is the header - - List varsToHavoc = VarsAssignedInLoop(g, header); - 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 - HavocCmd hc = new HavocCmd(header.tok, havocExprs); - List newCmds = new List(); - newCmds.Add(hc); - foreach (Cmd c in header.Cmds) - { - newCmds.Add(c); - } - - header.Cmds = newCmds; - - #endregion - } - - #endregion - - #endregion Convert program CFG into a DAG - } - - public static List VarsAssignedInLoop(Graph g, Block header) - { - List varsToHavoc = new List(); - foreach (var backEdgeNode in cce.NonNull(g.BackEdgeNodes(header))) - { - Contract.Assert(backEdgeNode != null); - foreach (Block b in g.NaturalLoops(header, backEdgeNode)) - { - Contract.Assert(b != null); - foreach (var c in b.Cmds) - { - Contract.Assert(c != null); - varsToHavoc.AddRange(c.GetAssignedVariables()); - } - } - } - - return varsToHavoc; - } - - public static IEnumerable VarsReferencedInLoop(Graph g, Block header) - { - HashSet referencedVars = new HashSet(); - foreach (Block backEdgeNode in cce.NonNull(g.BackEdgeNodes(header))) - { - Contract.Assert(backEdgeNode != null); - foreach (Block b in g.NaturalLoops(header, backEdgeNode)) - { - Contract.Assert(b != null); - foreach (Cmd c in b.Cmds) - { - Contract.Assert(c != null); - var Collector = new VariableCollector(); - Collector.Visit(c); - foreach (var v in Collector.usedVars) - { - referencedVars.Add(v); - } - } - } - } - - return referencedVars; - } - - private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary> edgesCut, int taskID, - int inductionK) - { - // K-induction has not been adapted to be aware of these parameters which standard CFG to DAG transformation uses - Contract.Requires(edgesCut == null); - Contract.Requires(taskID == -1); - Contract.Requires(0 <= inductionK); - - bool contRuleApplication = true; - while (contRuleApplication) - { - contRuleApplication = false; - - #region Use the graph library to figure out where the (natural) loops are - - #region Create the graph by adding the source node and each edge - - Graph g = Program.GraphFromImpl(impl); - - #endregion - - g.ComputeLoops(); // this is the call that does all of the processing - if (!g.Reducible) - { - throw new VCGenException("Irreducible flow graphs are unsupported."); - } - - #endregion - - foreach (Block header in cce.NonNull(g.Headers)) - { - Contract.Assert(header != null); - - #region Debug Tracing - - if (Options.TraceVerify) - { - Options.OutputWriter.WriteLine("Applying k-induction rule with k=" + inductionK); - } - - #endregion - - #region generate the step case - - Block newHeader = DuplicateLoop(impl, g, header, null, - false, false, "_step_assertion"); - for (int i = 0; i < inductionK; ++i) - { - newHeader = DuplicateLoop(impl, g, header, newHeader, - true, true, - "_step_" + (inductionK - i)); - } - - #endregion - - #region havoc variables that can be assigned in the loop - - List varsToHavoc = VarsAssignedInLoop(g, header); - 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 - HavocCmd hc = new HavocCmd(newHeader.tok, havocExprs); - List havocCmds = new List(); - havocCmds.Add(hc); - - Block havocBlock = new Block(newHeader.tok, newHeader.Label + "_havoc", havocCmds, - new GotoCmd(newHeader.tok, new List { newHeader })); - - impl.Blocks.Add(havocBlock); - newHeader.Predecessors.Add(havocBlock); - newHeader = havocBlock; - - #endregion - - #region generate the base case loop copies - - for (int i = 0; i < inductionK; ++i) - { - newHeader = DuplicateLoop(impl, g, header, newHeader, - false, false, - "_base_" + (inductionK - i)); - } - - #endregion - - #region redirect into the new loop copies and remove the original loop (but don't redirect back-edges) - - IDictionary backEdgeNodes = new Dictionary(); - foreach (Block b in cce.NonNull(g.BackEdgeNodes(header))) - { - Contract.Assert(b != null); - backEdgeNodes.Add(b, null); - } - - for (int predIndex = 0, n = header.Predecessors.Count(); predIndex < n; predIndex++) - { - Block pred = cce.NonNull(header.Predecessors[predIndex]); - if (!backEdgeNodes.ContainsKey(pred)) - { - GotoCmd gc = pred.TransferCmd as GotoCmd; - Contract.Assert(gc != null); - for (int i = 0; i < gc.LabelTargets.Count(); ++i) - { - if (gc.LabelTargets[i] == header) - { - gc.LabelTargets[i] = newHeader; - gc.LabelNames[i] = newHeader.Label; - newHeader.Predecessors.Add(pred); - } - } - } - } - - impl.PruneUnreachableBlocks(Options); - - #endregion - - contRuleApplication = true; - break; - } - } - - ResetPredecessors(impl.Blocks); - impl.FreshenCaptureStates(); - } - - private Block DuplicateLoop(Implementation impl, Graph g, - Block header, Block nextHeader, bool cutExits, - bool toAssumptions, string suffix) - { - IDictionary ori2CopiedBlocks = new Dictionary(); - Duplicator duplicator = new Duplicator(); - - #region create copies of all blocks in the loop - - foreach (Block backEdgeNode in cce.NonNull(g.BackEdgeNodes(header))) - { - Contract.Assert(backEdgeNode != null); - foreach (Block b in g.NaturalLoops(header, backEdgeNode)) - { - Contract.Assert(b != null); - if (!ori2CopiedBlocks.ContainsKey(b)) - { - Block copy = (Block)duplicator.Visit(b); - copy.Cmds = new List(copy - .Cmds); // Philipp Ruemmer commented that this was necessary due to a bug in the Duplicator. That was a long time; worth checking whether this has been fixed - copy.Predecessors = new List(); - copy.Label = copy.Label + suffix; - - #region turn asserts into assumptions - - if (toAssumptions) - { - for (int i = 0; i < copy.Cmds.Count(); ++i) - { - AssertCmd ac = copy.Cmds[i] as AssertCmd; - if (ac != null) - { - copy.Cmds[i] = new AssumeCmd(ac.tok, ac.Expr); - } - } - } - - #endregion - - impl.Blocks.Add(copy); - ori2CopiedBlocks.Add(b, copy); - } - } - } - - #endregion - - #region adjust the transfer commands of the newly created blocks - - foreach (KeyValuePair pair in ori2CopiedBlocks) - { - Block copy = pair.Value; - GotoCmd gc = copy.TransferCmd as GotoCmd; - if (gc != null) - { - List newTargets = new List(); - List newLabels = new List(); - - for (int i = 0; i < gc.LabelTargets.Count(); ++i) - { - if (gc.LabelTargets[i] == header) - { - if (nextHeader != null) - { - newTargets.Add(nextHeader); - newLabels.Add(nextHeader.Label); - nextHeader.Predecessors.Add(copy); - } - } - else if (ori2CopiedBlocks.TryGetValue(gc.LabelTargets[i], out var newTarget)) - { - newTargets.Add(newTarget); - newLabels.Add(newTarget.Label); - newTarget.Predecessors.Add(copy); - } - else if (!cutExits) - { - newTargets.Add(gc.LabelTargets[i]); - newLabels.Add(gc.LabelNames[i]); - gc.LabelTargets[i].Predecessors.Add(copy); - } - } - - if (newTargets.Count() == 0) - { - // if no targets are left, we assume false and return - copy.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); - copy.TransferCmd = new ReturnCmd(Token.NoToken); - } - else - { - copy.TransferCmd = new GotoCmd(gc.tok, newLabels, newTargets); - } - } - else if (cutExits && (copy.TransferCmd is ReturnCmd)) - { - // because return is a kind of exit from the loop, we - // assume false to cut this path - copy.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); - } - } - - #endregion - - return ori2CopiedBlocks[header]; - } - public void DesugarCalls(Implementation impl) { foreach (Block block in impl.Blocks) From cb17b6f97a741e72c710a42b2bdebcb8f842f3a7 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 3 Oct 2024 12:06:08 +0200 Subject: [PATCH 7/8] Refactoring --- Source/Core/AST/CallCmd.cs | 6 +- Source/Core/AST/ICarriesAttributes.cs | 2 - Source/VCGeneration/AssertCounterexample.cs | 4 +- Source/VCGeneration/ConditionGeneration.cs | 13 +-- .../Counterexamples/CallCounterexample.cs | 14 +-- .../CalleeCounterexampleInfo.cs | 11 +-- .../Counterexamples/Counterexample.cs | 81 +++++++-------- Source/VCGeneration/LoopExtractor.cs | 77 ++++++++------- Source/VCGeneration/ReturnCounterexample.cs | 20 ++-- Source/VCGeneration/Split.cs | 14 ++- Source/VCGeneration/StratifiedVC.cs | 2 +- .../Transformations/DesugarReturns.cs | 2 +- .../VerificationConditionGenerator.cs | 99 ++++++++----------- Source/VCGeneration/VerificationRunResult.cs | 4 +- 14 files changed, 161 insertions(+), 188 deletions(-) diff --git a/Source/Core/AST/CallCmd.cs b/Source/Core/AST/CallCmd.cs index d39768d22..e35541b6d 100644 --- a/Source/Core/AST/CallCmd.cs +++ b/Source/Core/AST/CallCmd.cs @@ -882,7 +882,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) // Do this after copying the attributes so it doesn't get overwritten if (callId is not null) { - (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req, + a.CopyIdWithModificationsFrom(tok, req, id => new TrackedCallRequiresGoal(callId, id)); } @@ -899,7 +899,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) Contract.Assert(a != null); // These probably won't have IDs, but copy if they do. if (callId is not null) { - (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req, + a.CopyIdWithModificationsFrom(tok, req, id => new TrackedCallRequiresAssumed(callId, id)); } @@ -1066,7 +1066,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) #endregion if (callId is not null) { - (assume as ICarriesAttributes).CopyIdWithModificationsFrom(tok, e, + assume.CopyIdWithModificationsFrom(tok, e, id => new TrackedCallEnsures(callId, id)); } diff --git a/Source/Core/AST/ICarriesAttributes.cs b/Source/Core/AST/ICarriesAttributes.cs index c0e88bf7d..a24485f89 100644 --- a/Source/Core/AST/ICarriesAttributes.cs +++ b/Source/Core/AST/ICarriesAttributes.cs @@ -55,8 +55,6 @@ public void AddStringAttribute(IToken tok, string name, string parameter) public static class CarriesAttributesExtensions { - - public static void CopyIdFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src) { var id = src.FindStringAttribute("id"); diff --git a/Source/VCGeneration/AssertCounterexample.cs b/Source/VCGeneration/AssertCounterexample.cs index d4074e463..e43d6fecd 100644 --- a/Source/VCGeneration/AssertCounterexample.cs +++ b/Source/VCGeneration/AssertCounterexample.cs @@ -39,8 +39,8 @@ public override byte[] Checksum public override Counterexample Clone() { - var ret = new AssertCounterexample(options, Trace, AugmentedTrace, FailingAssert, Model, MvInfo, Context, ProofRun); - ret.calleeCounterexamples = calleeCounterexamples; + var ret = new AssertCounterexample(Options, Trace, AugmentedTrace, FailingAssert, Model, MvInfo, Context, ProofRun); + ret.CalleeCounterexamples = CalleeCounterexamples; return ret; } } \ No newline at end of file diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index e1c9064a5..2e7f91060 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -236,7 +236,7 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu AssumeCmd c = new AssumeCmd(req.tok, e, CivlAttributes.ApplySubstitutionToPoolHints(formalProcImplSubst, req.Attributes)); // Copy any {:id ...} from the precondition to the assumption, so // we can track it while analyzing verification coverage. - (c as ICarriesAttributes).CopyIdFrom(req.tok, req); + c.CopyIdFrom(req.tok, req); c.IrrelevantForChecksumComputation = true; insertionPoint.Cmds.Add(c); if (debugWriter != null) @@ -883,14 +883,7 @@ private void AddDebugInfo(Cmd c, Dictionary incarnationMap, List { if (param is IdentifierExpr identifierExpr) { - if (incarnationMap.ContainsKey(identifierExpr.Decl)) - { - debugExprs.Add(incarnationMap[identifierExpr.Decl]); - } - else - { - debugExprs.Add(identifierExpr); - } + debugExprs.Add(incarnationMap.GetValueOrDefault(identifierExpr.Decl, identifierExpr)); } else { @@ -1207,7 +1200,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing var assumeCmd = new AssumeCmd(c.tok, assumption); // Copy any {:id ...} from the assignment to the assumption, so // we can track it while analyzing verification coverage. - (assumeCmd as ICarriesAttributes).CopyIdFrom(assign.tok, assign); + assumeCmd.CopyIdFrom(assign.tok, assign); passiveCmds.Add(assumeCmd); } diff --git a/Source/VCGeneration/Counterexamples/CallCounterexample.cs b/Source/VCGeneration/Counterexamples/CallCounterexample.cs index 065094515..e98ce17b3 100644 --- a/Source/VCGeneration/Counterexamples/CallCounterexample.cs +++ b/Source/VCGeneration/Counterexamples/CallCounterexample.cs @@ -8,7 +8,7 @@ public class CallCounterexample : Counterexample { public CallCmd FailingCall; public Requires FailingRequires; - public AssertRequiresCmd FailingAssert; + public AssertRequiresCmd FailingFailingAssert; [ContractInvariantMethod] void ObjectInvariant() @@ -18,12 +18,12 @@ void ObjectInvariant() } - public CallCounterexample(VCGenOptions options, List trace, List augmentedTrace, AssertRequiresCmd assertRequiresCmd, Model model, + public CallCounterexample(VCGenOptions options, List trace, List augmentedTrace, AssertRequiresCmd failingAssertRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, byte[] checksum = null) : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun) { - var failingRequires = assertRequiresCmd.Requires; - var failingCall = assertRequiresCmd.Call; + var failingRequires = failingAssertRequires.Requires; + var failingCall = failingAssertRequires.Call; Contract.Requires(!failingRequires.Free); Contract.Requires(trace != null); Contract.Requires(context != null); @@ -31,7 +31,7 @@ public CallCounterexample(VCGenOptions options, List trace, List Contract.Requires(failingRequires != null); this.FailingCall = failingCall; this.FailingRequires = failingRequires; - this.FailingAssert = assertRequiresCmd; + this.FailingFailingAssert = failingAssertRequires; this.checksum = checksum; this.SugaredCmdChecksum = failingCall.Checksum; } @@ -52,8 +52,8 @@ public override byte[] Checksum public override Counterexample Clone() { - var ret = new CallCounterexample(options, Trace, AugmentedTrace, FailingAssert, Model, MvInfo, Context, ProofRun, Checksum); - ret.calleeCounterexamples = calleeCounterexamples; + var ret = new CallCounterexample(Options, Trace, AugmentedTrace, FailingFailingAssert, Model, MvInfo, Context, ProofRun, Checksum); + ret.CalleeCounterexamples = CalleeCounterexamples; return ret; } } \ No newline at end of file diff --git a/Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs b/Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs index df8e7ba40..cde621743 100644 --- a/Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs +++ b/Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs @@ -5,21 +5,20 @@ namespace Microsoft.Boogie; public class CalleeCounterexampleInfo { - public Counterexample counterexample; + public readonly Counterexample Counterexample; - public List /*!>!*/ - args; + public readonly List /*!>!*/ Args; [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(args)); + Contract.Invariant(cce.NonNullElements(Args)); } public CalleeCounterexampleInfo(Counterexample cex, List!*/> x) { Contract.Requires(cce.NonNullElements(x)); - counterexample = cex; - args = x; + Counterexample = cex; + Args = x; } } \ No newline at end of file diff --git a/Source/VCGeneration/Counterexamples/Counterexample.cs b/Source/VCGeneration/Counterexamples/Counterexample.cs index cbe482c4d..da9cdca9c 100644 --- a/Source/VCGeneration/Counterexamples/Counterexample.cs +++ b/Source/VCGeneration/Counterexamples/Counterexample.cs @@ -18,34 +18,34 @@ void ObjectInvariant() { Contract.Invariant(Trace != null); Contract.Invariant(Context != null); - Contract.Invariant(cce.NonNullDictionaryAndValues(calleeCounterexamples)); + Contract.Invariant(cce.NonNullDictionaryAndValues(CalleeCounterexamples)); } public ProofRun ProofRun { get; } - protected readonly VCGenOptions options; + protected readonly VCGenOptions Options; [Peer] public List Trace; - public List AugmentedTrace; + public readonly List AugmentedTrace; public Model Model { get; } - public ModelViewInfo MvInfo; - public ProverContext Context; + public readonly ModelViewInfo MvInfo; + public readonly ProverContext Context; public abstract byte[] Checksum { get; } public byte[] SugaredCmdChecksum; public bool IsAuxiliaryCexForDiagnosingTimeouts; - public Dictionary calleeCounterexamples; + public Dictionary CalleeCounterexamples; internal Counterexample(VCGenOptions options, List trace, List augmentedTrace, Model model, VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun) { Contract.Requires(trace != null); Contract.Requires(context != null); - this.options = options; + this.Options = options; this.Trace = trace; this.Model = model; this.MvInfo = mvInfo; this.Context = context; this.ProofRun = proofRun; - this.calleeCounterexamples = new Dictionary(); + this.CalleeCounterexamples = new Dictionary(); // the call to instance method GetModelValue in the following code requires the fields Model and Context to be initialized if (augmentedTrace != null) { @@ -60,13 +60,13 @@ internal Counterexample(VCGenOptions options, List trace, List au public void AddCalleeCounterexample(TraceLocation loc, CalleeCounterexampleInfo cex) { Contract.Requires(cex != null); - calleeCounterexamples[loc] = cex; + CalleeCounterexamples[loc] = cex; } public void AddCalleeCounterexample(int numBlock, int numInstr, CalleeCounterexampleInfo cex) { Contract.Requires(cex != null); - calleeCounterexamples[new TraceLocation(numBlock, numInstr)] = cex; + CalleeCounterexamples[new TraceLocation(numBlock, numInstr)] = cex; } public void AddCalleeCounterexample(Dictionary cs) @@ -112,11 +112,11 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) { int numBlock = -1; string ind = new string(' ', indent); - foreach (Block b in Trace) + foreach (var block in Trace) { - Contract.Assert(b != null); + Contract.Assert(block != null); numBlock++; - if (b.tok == null) + if (block.tok == null) { tw.WriteLine("{0}", ind); } @@ -125,36 +125,37 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) // for ErrorTrace == 1 restrict the output; // do not print tokens with -17:-4 as their location because they have been // introduced in the translation and do not give any useful feedback to the user - if (!(options.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) + if (Options.ErrorTrace == 1 && block.tok.line == -17 && block.tok.col == -4) { - if (blockAction != null) + continue; + } + + blockAction?.Invoke(block); + + tw.WriteLine("{4}{0}({1},{2}): {3}", block.tok.filename, block.tok.line, block.tok.col, block.Label, ind); + + for (int numInstr = 0; numInstr < block.Cmds.Count; numInstr++) + { + var loc = new TraceLocation(numBlock, numInstr); + if (!CalleeCounterexamples.ContainsKey(loc)) { - blockAction(b); + continue; } - tw.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind); - - for (int numInstr = 0; numInstr < b.Cmds.Count; numInstr++) + var cmd = GetTraceCmd(loc); + var calleeName = GetCalledProcName(cmd); + if (calleeName.StartsWith(VC.StratifiedVerificationConditionGeneratorBase.recordProcName) && + Options.StratifiedInlining > 0) { - var loc = new TraceLocation(numBlock, numInstr); - if (calleeCounterexamples.ContainsKey(loc)) - { - var cmd = GetTraceCmd(loc); - var calleeName = GetCalledProcName(cmd); - if (calleeName.StartsWith(VC.StratifiedVerificationConditionGeneratorBase.recordProcName) && - options.StratifiedInlining > 0) - { - Contract.Assert(calleeCounterexamples[loc].args.Count == 1); - var arg = calleeCounterexamples[loc].args[0]; - tw.WriteLine("{0}value = {1}", ind, arg.ToString()); - } - else - { - tw.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind); - calleeCounterexamples[loc].counterexample.Print(indent + 4, tw); - tw.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind); - } - } + Contract.Assert(CalleeCounterexamples[loc].Args.Count == 1); + var arg = CalleeCounterexamples[loc].Args[0]; + tw.WriteLine("{0}value = {1}", ind, arg.ToString()); + } + else + { + tw.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind); + CalleeCounterexamples[loc].Counterexample.Print(indent + 4, tw); + tw.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind); } } } @@ -165,8 +166,8 @@ public void PrintModel(TextWriter tw, Counterexample counterexample) { Contract.Requires(counterexample != null); - var filenameTemplate = options.ModelViewFile; - if (Model == null || filenameTemplate == null || options.StratifiedInlining > 0) + var filenameTemplate = Options.ModelViewFile; + if (Model == null || filenameTemplate == null || Options.StratifiedInlining > 0) { return; } diff --git a/Source/VCGeneration/LoopExtractor.cs b/Source/VCGeneration/LoopExtractor.cs index 0aa72bf9d..a8fa2bc30 100644 --- a/Source/VCGeneration/LoopExtractor.cs +++ b/Source/VCGeneration/LoopExtractor.cs @@ -332,9 +332,8 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G } blockMap[block] = newBlock; - if (newBlocksCreated.ContainsKey(block)) + if (newBlocksCreated.TryGetValue(block, out var original)) { - var original = newBlocksCreated[block]; var newBlock2 = new Block(original.tok) { Label = original.Label, @@ -353,44 +352,46 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G var loopNodes = GetBlocksInAllNaturalLoops(options, header, g); //var loopNodes = g.NaturalLoops(header, source); foreach (var bl in auxGotoCmd.LabelTargets) { - if (g.Nodes.Contains(bl) && //newly created blocks are not present in NaturalLoop(header, xx, g) - !loopNodes.Contains(bl)) + if (!g.Nodes.Contains(bl) || //newly created blocks are not present in NaturalLoop(header, xx, g) + loopNodes.Contains(bl)) { - var auxNewBlock = new Block(bl.tok) - { - Label = bl.Label, - //these blocks may have read/write locals that are not present in naturalLoops - //we need to capture these variables - Cmds = Substituter.Apply(subst, bl.Cmds) - }; - //add restoration code for such blocks - if (loopHeaderToAssignCmd.TryGetValue(header, out var assignCmd)) - { - auxNewBlock.Cmds.Add(assignCmd); - } - - List lhsg = new List(); - List /*!*/ - globalsMods = loopHeaderToLoopProc[header].Modifies; - foreach (IdentifierExpr gl in globalsMods) - { - lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl)); - } - - List rhsg = new List(); - foreach (IdentifierExpr gl in globalsMods) - { - rhsg.Add(new OldExpr(Token.NoToken, gl)); - } - - if (lhsg.Count != 0) - { - AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg); - auxNewBlock.Cmds.Add(globalAssignCmd); - } - - blockMap[(Block) bl] = auxNewBlock; + continue; } + + var auxNewBlock = new Block(bl.tok) + { + Label = bl.Label, + //these blocks may have read/write locals that are not present in naturalLoops + //we need to capture these variables + Cmds = Substituter.Apply(subst, bl.Cmds) + }; + //add restoration code for such blocks + if (loopHeaderToAssignCmd.TryGetValue(header, out var assignCmd)) + { + auxNewBlock.Cmds.Add(assignCmd); + } + + List lhsg = new List(); + List /*!*/ + globalsMods = loopHeaderToLoopProc[header].Modifies; + foreach (IdentifierExpr gl in globalsMods) + { + lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl)); + } + + List rhsg = new List(); + foreach (IdentifierExpr gl in globalsMods) + { + rhsg.Add(new OldExpr(Token.NoToken, gl)); + } + + if (lhsg.Count != 0) + { + AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg); + auxNewBlock.Cmds.Add(globalAssignCmd); + } + + blockMap[bl] = auxNewBlock; } } } diff --git a/Source/VCGeneration/ReturnCounterexample.cs b/Source/VCGeneration/ReturnCounterexample.cs index 837b5864c..526ee4959 100644 --- a/Source/VCGeneration/ReturnCounterexample.cs +++ b/Source/VCGeneration/ReturnCounterexample.cs @@ -8,7 +8,7 @@ public class ReturnCounterexample : Counterexample { public TransferCmd FailingReturn; public Ensures FailingEnsures; - public AssertEnsuresCmd FailingAssert; + public AssertEnsuresCmd FailingFailingAssert; [ContractInvariantMethod] void ObjectInvariant() @@ -18,11 +18,12 @@ void ObjectInvariant() } - public ReturnCounterexample(VCGenOptions options, List trace, List augmentedTrace, AssertEnsuresCmd assertEnsuresCmd, TransferCmd failingReturn, Model model, + public ReturnCounterexample(VCGenOptions options, List trace, List augmentedTrace, + AssertEnsuresCmd failingAssertEnsures, TransferCmd failingReturn, Model model, VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, byte[] checksum) : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun) { - var failingEnsures = assertEnsuresCmd.Ensures; + var failingEnsures = failingAssertEnsures.Ensures; Contract.Requires(trace != null); Contract.Requires(context != null); Contract.Requires(failingReturn != null); @@ -30,7 +31,7 @@ public ReturnCounterexample(VCGenOptions options, List trace, List /// Returns the checksum of the corresponding assertion. /// - public override byte[] Checksum - { - get { return checksum; } - } + public override byte[] Checksum => checksum; public override Counterexample Clone() { - var ret = new ReturnCounterexample(options, Trace, AugmentedTrace, FailingAssert, FailingReturn, Model, MvInfo, Context, ProofRun, checksum); - ret.calleeCounterexamples = calleeCounterexamples; + var ret = new ReturnCounterexample(Options, Trace, AugmentedTrace, FailingFailingAssert, FailingReturn, Model, MvInfo, Context, ProofRun, checksum); + ret.CalleeCounterexamples = CalleeCounterexamples; return ret; } } \ No newline at end of file diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 746c549eb..fc5ff9473 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -443,13 +443,11 @@ void UpdateIncomingPaths(BlockStats s) void ComputeBlockSetsHelper(Block b, bool allowSmall) { Contract.Requires(b != null); - if (keepAtAll.Contains(b)) + if (!keepAtAll.Add(b)) { return; } - keepAtAll.Add(b); - if (allowSmall) { foreach (Block ch in b.Exits()) @@ -478,7 +476,7 @@ void ComputeBlockSetsHelper(Block b, bool allowSmall) } } - void ComputeBlockSets(bool allowSmall) + private void ComputeBlockSets(bool allowSmall) { protectedFromAssertToAssume.Clear(); keepAtAll.Clear(); @@ -488,12 +486,12 @@ void ComputeBlockSets(bool allowSmall) if (assertToAssume) { - foreach (Block b in allowSmall ? Blocks : bigBlocks) + foreach (var block in allowSmall ? Blocks : bigBlocks) { - Contract.Assert(b != null); - if (ComputeReachableNodes(b).Contains(cce.NonNull(splitBlock))) + Contract.Assert(block != null); + if (ComputeReachableNodes(block).Contains(cce.NonNull(splitBlock))) { - keepAtAll.Add(b); + keepAtAll.Add(block); } } diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 6bfbfd7ca..8d33b9848 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -965,7 +965,7 @@ public override Counterexample ExtractLoopTrace(Counterexample cex, string mainP return ExtractLoopTraceRec( new CalleeCounterexampleInfo(cex, new List()), - mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample; + mainProcName, inlinedProcs, extractLoopMappingInfo).Counterexample; } protected override bool ProcIsLoop(string procname) diff --git a/Source/VCGeneration/Transformations/DesugarReturns.cs b/Source/VCGeneration/Transformations/DesugarReturns.cs index 9fc282582..4362273a6 100644 --- a/Source/VCGeneration/Transformations/DesugarReturns.cs +++ b/Source/VCGeneration/Transformations/DesugarReturns.cs @@ -105,7 +105,7 @@ public static void InjectPostConditions(VCGenOptions options, ImplementationRun c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; // Copy any {:id ...} from the postcondition to the assumption, so // we can track it while analyzing verification coverage. - (c as ICarriesAttributes).CopyIdFrom(ens.tok, ens); + c.CopyIdFrom(ens.tok, ens); unifiedExitBlock.Cmds.Add(c); if (debugWriter != null) { diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index 507b01733..6366ae47a 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -77,7 +77,7 @@ public static AssumeCmd AssertTurnedIntoAssume(VCGenOptions options, AssertCmd a // Copy any {:id ...} from the assertion to the assumption, so // we can track it while analyzing verification coverage. But // skip it if it's `true` because that's never useful to track. - (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt); + assume.CopyIdFrom(assrt.tok, assrt); } return assume; @@ -578,14 +578,13 @@ public override void OnModel(IList labels /*!*/ /*!*/, Model model, #region Map passive program errors back to original program errors - ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample; - if (returnExample != null) + if (newCounterexample is ReturnCounterexample returnExample) { - foreach (Block b in returnExample.Trace) + foreach (var block in returnExample.Trace) { - Contract.Assert(b != null); - Contract.Assume(b.TransferCmd != null); - ReturnCmd cmd = gotoCmdOrigins.ContainsKey(b.TransferCmd) ? gotoCmdOrigins[b.TransferCmd] : null; + Contract.Assert(block != null); + Contract.Assume(block.TransferCmd != null); + var cmd = gotoCmdOrigins.GetValueOrDefault(block.TransferCmd); if (cmd != null) { returnExample.FailingReturn = cmd; @@ -798,17 +797,6 @@ public Dictionary PassifyImpl(ImplementationRun run, out HandleSelectiveChecking(impl); - -// #region Constant Folding -// #endregion -// #region Debug Tracing -// if (CommandLineOptions.Clo.TraceVerify) -// { -// Console.WriteLine("after constant folding"); -// EmitImpl(impl, true); -// } -// #endregion - return gotoCmdOrigins; } @@ -1114,7 +1102,7 @@ public virtual Counterexample ExtractLoopTrace(Counterexample cex, string mainPr return ExtractLoopTraceRec( new CalleeCounterexampleInfo(cex, new List()), - mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample; + mainProcName, inlinedProcs, extractLoopMappingInfo).Counterexample; } protected CalleeCounterexampleInfo ExtractLoopTraceRec( @@ -1123,16 +1111,16 @@ protected CalleeCounterexampleInfo ExtractLoopTraceRec( Dictionary> extractLoopMappingInfo) { Contract.Requires(currProc != null); - if (cexInfo.counterexample == null) + if (cexInfo.Counterexample == null) { return cexInfo; } - var cex = cexInfo.counterexample; + var cex = cexInfo.Counterexample; // Go through all blocks in the trace, map them back to blocks in the original program (if there is one) var ret = cex.Clone(); ret.Trace = new List(); - ret.calleeCounterexamples = new Dictionary(); + ret.CalleeCounterexamples = new Dictionary(); for (int numBlock = 0; numBlock < cex.Trace.Count; numBlock++) { @@ -1148,7 +1136,7 @@ protected CalleeCounterexampleInfo ExtractLoopTraceRec( { Cmd cmd = block.Cmds[numInstr]; var loc = new TraceLocation(numBlock, numInstr); - if (!cex.calleeCounterexamples.ContainsKey(loc)) + if (!cex.CalleeCounterexamples.ContainsKey(loc)) { if (GetCallee(cex.GetTraceCmd(loc), inlinedProcs) != null) { @@ -1160,7 +1148,7 @@ protected CalleeCounterexampleInfo ExtractLoopTraceRec( string callee = cex.GetCalledProcName(cex.GetTraceCmd(loc)); Contract.Assert(callee != null); - var calleeTrace = cex.calleeCounterexamples[loc]; + var calleeTrace = cex.CalleeCounterexamples[loc]; Debug.Assert(calleeTrace != null); var origTrace = ExtractLoopTraceRec(calleeTrace, callee, inlinedProcs, extractLoopMappingInfo); @@ -1170,25 +1158,25 @@ protected CalleeCounterexampleInfo ExtractLoopTraceRec( // Absorb the trace into the current trace int currLen = ret.Trace.Count; - ret.Trace.AddRange(origTrace.counterexample.Trace); + ret.Trace.AddRange(origTrace.Counterexample.Trace); - foreach (var kvp in origTrace.counterexample.calleeCounterexamples) + foreach (var kvp in origTrace.Counterexample.CalleeCounterexamples) { var newloc = new TraceLocation(kvp.Key.numBlock + currLen, kvp.Key.numInstr); - ret.calleeCounterexamples.Add(newloc, kvp.Value); + ret.CalleeCounterexamples.Add(newloc, kvp.Value); } } else { var origLoc = new TraceLocation(ret.Trace.Count - 1, GetCallCmdPosition(origBlock, callCnt, inlinedProcs, callee)); - ret.calleeCounterexamples.Add(origLoc, origTrace); + ret.CalleeCounterexamples.Add(origLoc, origTrace); callCnt++; } } } - return new CalleeCounterexampleInfo(ret, cexInfo.args); + return new CalleeCounterexampleInfo(ret, cexInfo.Args); } // return the position of the i^th CallCmd in the block (count only those Calls that call a procedure in inlinedProcs). @@ -1377,34 +1365,31 @@ public static Counterexample AssertCmdToCounterexample(VCGenOptions options, Ass /// /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt". /// - public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assrt, + public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assert, Counterexample cex, Block implEntryBlock, Dictionary gotoCmdOrigins) { - Contract.Requires(assrt != null); + Contract.Requires(assert != null); Contract.Requires(cex != null); Contract.Requires(implEntryBlock != null); Contract.Requires(gotoCmdOrigins != null); Contract.Ensures(Contract.Result() != null); Counterexample cc; - if (assrt is AssertRequiresCmd) + if (assert is AssertRequiresCmd assertRequiresCmd) { - var aa = (AssertRequiresCmd)assrt; - cc = new CallCounterexample(options, cex.Trace, cex.AugmentedTrace, aa, cex.Model, cex.MvInfo, cex.Context, - cex.ProofRun, aa.Checksum); + cc = new CallCounterexample(options, cex.Trace, cex.AugmentedTrace, assertRequiresCmd, cex.Model, cex.MvInfo, cex.Context, + cex.ProofRun, assertRequiresCmd.Checksum); } - else if (assrt is AssertEnsuresCmd && cex is ReturnCounterexample) + else if (assert is AssertEnsuresCmd assertEnsuresCmd && cex is ReturnCounterexample returnCounterexample) { - var aa = (AssertEnsuresCmd)assrt; - var oldCex = (ReturnCounterexample)cex; // The first three parameters of ReturnCounterexample are: List trace, List augmentedTrace, TransferCmd failingReturn, Ensures failingEnsures. // We have the "aa" version of failingEnsures, namely aa.Ensures. The first and third parameters take more work to reconstruct. // (The code here assumes the labels of blocks remain the same. If that's not the case, then it is possible that the trace // computed does not lead to where the error is, but at least the error will not be masked.) List reconstructedTrace = null; Block prevBlock = null; - foreach (var blk in cex.Trace) + foreach (var blk in returnCounterexample.Trace) { if (reconstructedTrace == null) { @@ -1456,11 +1441,11 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options if (reconstructedTrace != null) { // The reconstructed trace ends with a "return;" in the passive command, so we now try to convert it to the original (non-passive) "return;" - foreach (Block b in reconstructedTrace) + foreach (var block in reconstructedTrace) { - Contract.Assert(b != null); - Contract.Assume(b.TransferCmd != null); - returnCmd = gotoCmdOrigins.ContainsKey(b.TransferCmd) ? gotoCmdOrigins[b.TransferCmd] : null; + Contract.Assert(block != null); + Contract.Assume(block.TransferCmd != null); + returnCmd = gotoCmdOrigins.GetValueOrDefault(block.TransferCmd); if (returnCmd != null) { break; @@ -1474,13 +1459,13 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options } } - cc = new ReturnCounterexample(options, reconstructedTrace ?? cex.Trace, cex.AugmentedTrace, aa, - returnCmd ?? oldCex.FailingReturn, - cex.Model, cex.MvInfo, cex.Context, cex.ProofRun, aa.Checksum); + cc = new ReturnCounterexample(options, reconstructedTrace ?? returnCounterexample.Trace, returnCounterexample.AugmentedTrace, assertEnsuresCmd, + returnCmd ?? returnCounterexample.FailingReturn, + returnCounterexample.Model, returnCounterexample.MvInfo, returnCounterexample.Context, returnCounterexample.ProofRun, assertEnsuresCmd.Checksum); } else { - cc = new AssertCounterexample(options, cex.Trace, cex.AugmentedTrace, assrt, cex.Model, cex.MvInfo, cex.Context, + cc = new AssertCounterexample(options, cex.Trace, cex.AugmentedTrace, assert, cex.Model, cex.MvInfo, cex.Context, cex.ProofRun); } @@ -1527,34 +1512,34 @@ VCExpr LetVC(List blocks, IEnumerable sortedNodes = dag.TopologicalSort(); Contract.Assert(sortedNodes != null); - Dictionary blockVariables = new Dictionary(); + var blockVariables = new Dictionary(); List bindings = new List(); VCExpressionGenerator gen = proverCtxt.ExprGen; Contract.Assert(gen != null); foreach (Block block in sortedNodes) { - VCExpr SuccCorrect; - GotoCmd gotocmd = block.TransferCmd as GotoCmd; + VCExpr succCorrect; + var gotocmd = block.TransferCmd as GotoCmd; if (gotocmd == null) { ReturnExprCmd re = block.TransferCmd as ReturnExprCmd; if (re == null) { - SuccCorrect = VCExpressionGenerator.True; + succCorrect = VCExpressionGenerator.True; } else { - SuccCorrect = proverCtxt.BoogieExprTranslator.Translate(re.Expr); + succCorrect = proverCtxt.BoogieExprTranslator.Translate(re.Expr); if (isPositiveContext) { - SuccCorrect = gen.Not(SuccCorrect); + succCorrect = gen.Not(succCorrect); } } } else { Contract.Assert(gotocmd.LabelTargets != null); - List SuccCorrectVars = new List(gotocmd.LabelTargets.Count); + var succCorrectVars = new List(gotocmd.LabelTargets.Count); foreach (Block successor in gotocmd.LabelTargets) { Contract.Assert(successor != null); @@ -1568,14 +1553,14 @@ VCExpr LetVC(List blocks, s = gen.Implies(controlTransferExpr, s); } - SuccCorrectVars.Add(s); + succCorrectVars.Add(s); } - SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars); + succCorrect = gen.NAry(VCExpressionGenerator.AndOp, succCorrectVars); } VCContext context = new VCContext(Options, absyIds, proverCtxt, controlFlowVariableExpr, isPositiveContext); - VCExpr vc = Wlp.Block(block, SuccCorrect, context); + VCExpr vc = Wlp.Block(block, succCorrect, context); assertionCount += context.AssertionCount; VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool); diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs index b2566f93e..9f48dc5a1 100644 --- a/Source/VCGeneration/VerificationRunResult.cs +++ b/Source/VCGeneration/VerificationRunResult.cs @@ -32,9 +32,9 @@ public void ComputePerAssertOutcomes(out Dictionary pe if (counterExample is AssertCounterexample assertCounterexample) { underlyingAssert = assertCounterexample.FailingAssert; } else if (counterExample is CallCounterexample callCounterexample) { - underlyingAssert = callCounterexample.FailingAssert; + underlyingAssert = callCounterexample.FailingFailingAssert; } else if (counterExample is ReturnCounterexample returnCounterexample) { - underlyingAssert = returnCounterexample.FailingAssert; + underlyingAssert = returnCounterexample.FailingFailingAssert; } else { continue; } From 3b0b961fc04cbbb0a5107fabbdbdcb1c87da8b1b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 3 Oct 2024 12:27:11 +0200 Subject: [PATCH 8/8] Fix --- Source/VCGeneration/Transformations/RemoveBackEdges.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/VCGeneration/Transformations/RemoveBackEdges.cs b/Source/VCGeneration/Transformations/RemoveBackEdges.cs index d8a43e66b..731f7a1e5 100644 --- a/Source/VCGeneration/Transformations/RemoveBackEdges.cs +++ b/Source/VCGeneration/Transformations/RemoveBackEdges.cs @@ -48,7 +48,7 @@ public void ConvertCfg2Dag(ImplementationRun run, Dictionary> // Recompute the predecessors, but first insert a dummy start node that is sure not to be the target of any goto (because the cutting of back edges // below assumes that the start node has no predecessor) impl.Blocks.Insert(0, - new Block(Token.NoToken, "0", new List(), + new Block(new Token(-17, -4), "0", new List(), new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] }))); ConditionGeneration.ResetPredecessors(impl.Blocks);