diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index fd844a775..7e0afdc3d 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -6,7 +6,6 @@ using System.Diagnostics.Contracts; using System.Security.Cryptography; using Microsoft.BaseTypes; -using Microsoft.Boogie.GraphUtil; namespace Microsoft.Boogie { @@ -3507,1080 +3506,6 @@ public Block getBlock(string label) } } - public class Implementation : DeclWithFormals { - public List LocVars; - - [Rep] public StmtList StructuredStmts; - - [field: Rep] - public List Blocks { - get; - set; - } - public Procedure Proc; - - // Blocks before applying passification etc. - // Both are used only when /inline is set. - public List OriginalBlocks; - public List OriginalLocVars; - - // Map filled in during passification to allow augmented error trace reporting - public Dictionary> debugInfos = new(); - - public readonly ISet AssertionChecksums = new HashSet(ChecksumComparer.Default); - - public sealed class ChecksumComparer : IEqualityComparer - { - static IEqualityComparer defaultComparer; - - public static IEqualityComparer Default - { - get - { - if (defaultComparer == null) - { - defaultComparer = new ChecksumComparer(); - } - - return defaultComparer; - } - } - - public bool Equals(byte[] x, byte[] y) - { - if (x == null || y == null) - { - return x == y; - } - else - { - return x.SequenceEqual(y); - } - } - - public int GetHashCode(byte[] checksum) - { - if (checksum == null) - { - throw new ArgumentNullException("checksum"); - } - else - { - var result = 17; - for (int i = 0; i < checksum.Length; i++) - { - result = result * 23 + checksum[i]; - } - - return result; - } - } - } - - public void AddAssertionChecksum(byte[] checksum) - { - Contract.Requires(checksum != null); - - if (AssertionChecksums != null) - { - AssertionChecksums.Add(checksum); - } - } - - public ISet AssertionChecksumsInCachedSnapshot { get; set; } - - public bool IsAssertionChecksumInCachedSnapshot(byte[] checksum) - { - Contract.Requires(AssertionChecksumsInCachedSnapshot != null); - - return AssertionChecksumsInCachedSnapshot.Contains(checksum); - } - - public IList RecycledFailingAssertions { get; protected set; } - - public void AddRecycledFailingAssertion(AssertCmd assertion) - { - if (RecycledFailingAssertions == null) - { - RecycledFailingAssertions = new List(); - } - - RecycledFailingAssertions.Add(assertion); - } - - public Cmd ExplicitAssumptionAboutCachedPrecondition { get; set; } - - // Strongly connected components - private StronglyConnectedComponents scc; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(LocVars != null); - Contract.Invariant(cce.NonNullElements(Blocks)); - Contract.Invariant(cce.NonNullElements(OriginalBlocks, true)); - Contract.Invariant(cce.NonNullElements(scc, true)); - } - - private bool BlockPredecessorsComputed; - - public bool StronglyConnectedComponentsComputed - { - get { return this.scc != null; } - } - - public bool IsSkipVerification(CoreOptions options) - { - bool verify = true; - cce.NonNull(this.Proc).CheckBooleanAttribute("verify", ref verify); - this.CheckBooleanAttribute("verify", ref verify); - if (!verify) { - return true; - } - - if (options.ProcedureInlining == CoreOptions.Inlining.Assert || - options.ProcedureInlining == CoreOptions.Inlining.Assume) { - Expr inl = this.FindExprAttribute("inline"); - if (inl == null) { - inl = this.Proc.FindExprAttribute("inline"); - } - - if (inl != null) { - return true; - } - } - - if (options.StratifiedInlining > 0) { - return !QKeyValue.FindBoolAttribute(Attributes, "entrypoint"); - } - - return false; - } - - public string Id - { - get - { - var id = (this as ICarriesAttributes).FindStringAttribute("id"); - if (id == null) - { - id = Name + GetHashCode().ToString() + ":0"; - } - - return id; - } - } - - public int Priority - { - get - { - int priority = 0; - CheckIntAttribute("priority", ref priority); - if (priority <= 0) - { - priority = 1; - } - - return priority; - } - } - - public Dictionary GetExtraSMTOptions() - { - Dictionary extraSMTOpts = new(); - for (var a = Attributes; a != null; a = a.Next) { - var n = a.Params.Count; - var k = a.Key; - if (k.Equals("smt_option")) { - if (n == 2 && a.Params[0] is string s) { - extraSMTOpts.Add(s, a.Params[1].ToString()); - } - } - } - - return extraSMTOpts; - } - - public IDictionary ErrorChecksumToCachedError { get; private set; } - - public bool IsErrorChecksumInCachedSnapshot(byte[] checksum) - { - Contract.Requires(ErrorChecksumToCachedError != null); - - return ErrorChecksumToCachedError.ContainsKey(checksum); - } - - public void SetErrorChecksumToCachedError(IEnumerable> errors) - { - Contract.Requires(errors != null); - - ErrorChecksumToCachedError = new Dictionary(ChecksumComparer.Default); - foreach (var kv in errors) - { - ErrorChecksumToCachedError[kv.Item1] = kv.Item3; - if (kv.Item2 != null) - { - ErrorChecksumToCachedError[kv.Item2] = null; - } - } - } - - public bool HasCachedSnapshot - { - get { return ErrorChecksumToCachedError != null && AssertionChecksumsInCachedSnapshot != null; } - } - - public bool AnyErrorsInCachedSnapshot - { - get - { - Contract.Requires(ErrorChecksumToCachedError != null); - - return ErrorChecksumToCachedError.Any(); - } - } - - IList injectedAssumptionVariables; - - public IList InjectedAssumptionVariables - { - get { return injectedAssumptionVariables != null ? injectedAssumptionVariables : new List(); } - } - - IList doomedInjectedAssumptionVariables; - - public IList DoomedInjectedAssumptionVariables - { - get - { - return doomedInjectedAssumptionVariables != null - ? doomedInjectedAssumptionVariables - : new List(); - } - } - - public List RelevantInjectedAssumptionVariables(Dictionary incarnationMap) - { - return InjectedAssumptionVariables.Where(v => - { - if (incarnationMap.TryGetValue(v, out var e)) - { - var le = e as LiteralExpr; - return le == null || !le.IsTrue; - } - else - { - return false; - } - }).ToList(); - } - - public List RelevantDoomedInjectedAssumptionVariables(Dictionary incarnationMap) - { - return DoomedInjectedAssumptionVariables.Where(v => - { - if (incarnationMap.TryGetValue(v, out var e)) - { - var le = e as LiteralExpr; - return le == null || !le.IsTrue; - } - else - { - return false; - } - }).ToList(); - } - - public Expr ConjunctionOfInjectedAssumptionVariables(Dictionary incarnationMap, out bool isTrue) - { - Contract.Requires(incarnationMap != null); - - var vars = RelevantInjectedAssumptionVariables(incarnationMap).Select(v => incarnationMap[v]).ToList(); - isTrue = vars.Count == 0; - return LiteralExpr.BinaryTreeAnd(vars); - } - - public void InjectAssumptionVariable(LocalVariable variable, bool isDoomed = false) - { - LocVars.Add(variable); - if (isDoomed) - { - if (doomedInjectedAssumptionVariables == null) - { - doomedInjectedAssumptionVariables = new List(); - } - - doomedInjectedAssumptionVariables.Add(variable); - } - else - { - if (injectedAssumptionVariables == null) - { - injectedAssumptionVariables = new List(); - } - - injectedAssumptionVariables.Add(variable); - } - } - - public Implementation(IToken tok, string name, List typeParams, List inParams, - List outParams, List localVariables, [Captured] StmtList structuredStmts, QKeyValue kv) - : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) - { - Contract.Requires(structuredStmts != null); - Contract.Requires(localVariables != null); - Contract.Requires(outParams != null); - Contract.Requires(inParams != null); - Contract.Requires(typeParams != null); - Contract.Requires(name != null); - Contract.Requires(tok != null); - //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()); - } - - public Implementation(IToken tok, string name, List typeParams, List inParams, - List outParams, List localVariables, [Captured] StmtList structuredStmts) - : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()) - { - Contract.Requires(structuredStmts != null); - Contract.Requires(localVariables != null); - Contract.Requires(outParams != null); - Contract.Requires(inParams != null); - Contract.Requires(typeParams != null); - Contract.Requires(name != null); - Contract.Requires(tok != null); - //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()); - } - - public Implementation(IToken tok, string name, List typeParams, List inParams, - List outParams, List localVariables, [Captured] StmtList structuredStmts, Errors errorHandler) - : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler) - { - Contract.Requires(errorHandler != null); - Contract.Requires(structuredStmts != null); - Contract.Requires(localVariables != null); - Contract.Requires(outParams != null); - Contract.Requires(inParams != null); - Contract.Requires(typeParams != null); - Contract.Requires(name != null); - Contract.Requires(tok != null); - //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler); - } - - public Implementation(IToken /*!*/ tok, - string /*!*/ name, - List /*!*/ typeParams, - List /*!*/ inParams, - List /*!*/ outParams, - List /*!*/ localVariables, - [Captured] StmtList /*!*/ structuredStmts, - QKeyValue kv, - Errors /*!*/ errorHandler) - : base(tok, name, typeParams, inParams, outParams) - { - Contract.Requires(tok != null); - Contract.Requires(name != null); - Contract.Requires(typeParams != null); - Contract.Requires(inParams != null); - Contract.Requires(outParams != null); - Contract.Requires(localVariables != null); - Contract.Requires(structuredStmts != null); - Contract.Requires(errorHandler != null); - LocVars = localVariables; - StructuredStmts = structuredStmts; - BigBlocksResolutionContext ctx = new BigBlocksResolutionContext(structuredStmts, errorHandler); - Blocks = ctx.Blocks; - BlockPredecessorsComputed = false; - scc = null; - Attributes = kv; - } - - public Implementation(IToken tok, string name, List typeParams, List inParams, - List outParams, List localVariables, [Captured] List block) - : this(tok, name, typeParams, inParams, outParams, localVariables, block, null) - { - Contract.Requires(cce.NonNullElements(block)); - Contract.Requires(localVariables != null); - Contract.Requires(outParams != null); - Contract.Requires(inParams != null); - Contract.Requires(typeParams != null); - Contract.Requires(name != null); - Contract.Requires(tok != null); - //:this(tok, name, typeParams, inParams, outParams, localVariables, block, null); - } - - public Implementation(IToken /*!*/ tok, - string /*!*/ name, - List /*!*/ typeParams, - List /*!*/ inParams, - List /*!*/ outParams, - List /*!*/ localVariables, - [Captured] List /*!*/ blocks, - QKeyValue kv) - : base(tok, name, typeParams, inParams, outParams) - { - Contract.Requires(name != null); - Contract.Requires(inParams != null); - Contract.Requires(outParams != null); - Contract.Requires(localVariables != null); - Contract.Requires(cce.NonNullElements(blocks)); - LocVars = localVariables; - Blocks = blocks; - BlockPredecessorsComputed = false; - scc = null; - Attributes = kv; - } - - public override void Emit(TokenTextWriter stream, int level) - { - stream.Write(this, level, "implementation "); - EmitAttributes(stream); - stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); - EmitSignature(stream, false); - stream.WriteLine(); - - stream.WriteLine(level, "{0}", '{'); - - foreach (Variable /*!*/ v in this.LocVars) - { - Contract.Assert(v != null); - v.Emit(stream, level + 1); - } - - if (this.StructuredStmts != null && !stream.Options.PrintInstrumented && - !stream.Options.PrintInlined) - { - if (this.LocVars.Count > 0) - { - stream.WriteLine(); - } - - if (stream.Options.PrintUnstructured < 2) - { - if (stream.Options.PrintUnstructured == 1) - { - stream.WriteLine(this, level + 1, "/*** structured program:"); - } - - this.StructuredStmts.Emit(stream, level + 1); - if (stream.Options.PrintUnstructured == 1) - { - stream.WriteLine(level + 1, "**** end structured program */"); - } - } - } - - if (this.StructuredStmts == null || 1 <= stream.Options.PrintUnstructured || - stream.Options.PrintInstrumented || stream.Options.PrintInlined) - { - foreach (Block b in this.Blocks) - { - b.Emit(stream, level + 1); - } - } - - stream.WriteLine(level, "{0}", '}'); - - stream.WriteLine(); - stream.WriteLine(); - } - - public override void Register(ResolutionContext rc) - { - // nothing to register - } - - public override void Resolve(ResolutionContext rc) - { - if (Proc != null) - { - // already resolved - return; - } - - Proc = rc.LookUpProcedure(cce.NonNull(this.Name)); - if (Proc == null) - { - rc.Error(this, "implementation given for undeclared procedure: {0}", this.Name); - } - else if (Proc is ActionDecl actionDecl) - { - actionDecl.Impl = this; - } - - int previousTypeBinderState = rc.TypeBinderState; - try - { - RegisterTypeParameters(rc); - - rc.PushVarContext(); - rc.Proc = Proc; - RegisterFormals(InParams, rc); - RegisterFormals(OutParams, rc); - foreach (Variable v in LocVars) - { - Contract.Assert(v != null); - v.Register(rc); - v.Resolve(rc); - } - rc.Proc = null; - - foreach (Variable v in LocVars) - { - Contract.Assert(v != null); - v.ResolveWhere(rc); - } - - rc.PushProcedureContext(); - foreach (Block b in Blocks) - { - b.Register(rc); - } - - (this as ICarriesAttributes).ResolveAttributes(rc); - - rc.Proc = Proc; - rc.StateMode = Proc.IsPure ? ResolutionContext.State.StateLess : ResolutionContext.State.Two; - foreach (Block b in Blocks) - { - b.Resolve(rc); - } - rc.Proc = null; - rc.StateMode = ResolutionContext.State.Single; - - rc.PopProcedureContext(); - rc.PopVarContext(); - - Type.CheckBoundVariableOccurrences(TypeParameters, - InParams.Select(Item => Item.TypedIdent.Type).ToList(), - OutParams.Select(Item => Item.TypedIdent.Type).ToList(), - this.tok, "implementation arguments", - rc); - } - finally - { - rc.TypeBinderState = previousTypeBinderState; - } - - SortTypeParams(); - } - - public override void Typecheck(TypecheckingContext tc) - { - //Contract.Requires(tc != null); - base.Typecheck(tc); - - Contract.Assume(this.Proc != null); - - if (this.TypeParameters.Count != Proc.TypeParameters.Count) - { - tc.Error(this, "mismatched number of type parameters in procedure implementation: {0}", - this.Name); - } - else - { - // if the numbers of type parameters are different, it is - // difficult to compare the argument types - MatchFormals(this.InParams, Proc.InParams, "in", tc); - MatchFormals(this.OutParams, Proc.OutParams, "out", tc); - } - - var oldProc = tc.Proc; - tc.Proc = Proc; - tc.Impl = this; - foreach (Variable /*!*/ v in LocVars) - { - Contract.Assert(v != null); - v.Typecheck(tc); - } - foreach (Block b in Blocks) - { - b.Typecheck(tc); - } - Contract.Assert(tc.Proc == Proc); - tc.Impl = null; - tc.Proc = oldProc; - - if (Proc is ActionDecl || Proc is YieldProcedureDecl) - { - var graph = Program.GraphFromImpl(this); - if (!Graph.Acyclic(graph)) - { - if (Proc is ActionDecl) - { - tc.Error(this, "action implementation may not have loops"); - } - else // Proc is YieldProcedureDecl - { - graph.ComputeLoops(); - if (!graph.Reducible) - { - tc.Error(this, "irreducible control flow graph not allowed"); - } - else - { - TypecheckLoopAnnotations(tc, graph); - } - } - } - } - } - - private void TypecheckLoopAnnotations(TypecheckingContext tc, Graph graph) - { - var yieldingProc = (YieldProcedureDecl)Proc; - foreach (var header in graph.Headers) - { - var yieldingLayer = yieldingProc.Layer; - var yieldCmd = (PredicateCmd)header.Cmds.FirstOrDefault(cmd => - cmd is PredicateCmd predCmd && predCmd.HasAttribute(CivlAttributes.YIELDS)); - if (yieldCmd == null) - { - yieldingLayer = int.MinValue; - } - else - { - var layers = yieldCmd.Layers; - header.Cmds.Remove(yieldCmd); - if (layers.Any()) - { - if (layers.Count > 1) - { - tc.Error(header, "expected layer attribute to indicate the highest yielding layer of this loop"); - continue; - } - if (layers[0] > yieldingLayer) - { - tc.Error(header, - "yielding layer of loop must not be more than the layer of enclosing procedure"); - continue; - } - yieldingLayer = layers[0]; - } - } - - var yieldInvariants = header.Cmds - .TakeWhile(cmd => cmd is CallCmd { Proc: YieldInvariantDecl }).OfType() - .ToList(); - header.Cmds.RemoveRange(0, yieldInvariants.Count); - if (yieldInvariants.Any() && yieldCmd == null) - { - tc.Error(header, "expected :yields attribute on this loop"); - } - foreach (var callCmd in yieldInvariants) - { - var yieldInvariant = (YieldInvariantDecl)callCmd.Proc; - var calleeLayerNum = yieldInvariant.Layer; - if (calleeLayerNum > yieldingLayer) - { - tc.Error(callCmd, $"loop must yield at layer {calleeLayerNum} of the called yield invariant"); - } - } - foreach (var predCmd in header.Cmds.TakeWhile(cmd => cmd is PredicateCmd).OfType()) - { - if (predCmd.Layers.Min() <= yieldingLayer && - VariableCollector.Collect(predCmd, true).OfType().Any()) - { - tc.Error(predCmd, - "invariant may not access a global variable since one of its layers is a yielding layer of its loop"); - } - } - - yieldingProc.YieldingLoops[header] = new YieldingLoop(yieldingLayer, yieldInvariants); - } - } - - void MatchFormals(List /*!*/ implFormals, List /*!*/ procFormals, string /*!*/ inout, - TypecheckingContext /*!*/ tc) - { - Contract.Requires(implFormals != null); - Contract.Requires(procFormals != null); - Contract.Requires(inout != null); - Contract.Requires(tc != null); - if (implFormals.Count != procFormals.Count) - { - tc.Error(this, "mismatched number of {0}-parameters in procedure implementation: {1}", - inout, this.Name); - } - else - { - // unify the type parameters so that types can be compared - Contract.Assert(Proc != null); - Contract.Assert(this.TypeParameters.Count == Proc.TypeParameters.Count); - - IDictionary /*!*/ - subst1 = - new Dictionary(); - IDictionary /*!*/ - subst2 = - new Dictionary(); - - for (int i = 0; i < this.TypeParameters.Count; ++i) - { - TypeVariable /*!*/ - newVar = - new TypeVariable(Token.NoToken, Proc.TypeParameters[i].Name); - Contract.Assert(newVar != null); - subst1.Add(Proc.TypeParameters[i], newVar); - subst2.Add(this.TypeParameters[i], newVar); - } - - for (int i = 0; i < implFormals.Count; i++) - { - // the names of the formals are allowed to change from the proc to the impl - - // but types must be identical - Type t = cce.NonNull((Variable) implFormals[i]).TypedIdent.Type.Substitute(subst2); - Type u = cce.NonNull((Variable) procFormals[i]).TypedIdent.Type.Substitute(subst1); - if (!t.Equals(u)) - { - string /*!*/ - a = cce.NonNull((Variable) implFormals[i]).Name; - Contract.Assert(a != null); - string /*!*/ - b = cce.NonNull((Variable) procFormals[i]).Name; - Contract.Assert(b != null); - string /*!*/ - c; - if (a == b) - { - c = a; - } - else - { - c = String.Format("{0} (named {1} in implementation)", b, a); - } - - tc.Error(this, "mismatched type of {0}-parameter in implementation {1}: {2}", inout, this.Name, c); - } - } - } - } - - private Dictionary /*?*/ - formalMap = null; - - public void ResetImplFormalMap() - { - this.formalMap = null; - } - - public Dictionary /*!*/ GetImplFormalMap(CoreOptions options) - { - Contract.Ensures(Contract.Result>() != null); - - if (this.formalMap != null) - { - return this.formalMap; - } - else - { - Dictionary /*!*/ - map = new Dictionary(InParams.Count + OutParams.Count); - - Contract.Assume(this.Proc != null); - Contract.Assume(InParams.Count == Proc.InParams.Count); - for (int i = 0; i < InParams.Count; i++) - { - Variable /*!*/ - v = InParams[i]; - Contract.Assert(v != null); - IdentifierExpr ie = new IdentifierExpr(v.tok, v); - Variable /*!*/ - pv = Proc.InParams[i]; - Contract.Assert(pv != null); - map.Add(pv, ie); - } - - System.Diagnostics.Debug.Assert(OutParams.Count == Proc.OutParams.Count); - for (int i = 0; i < OutParams.Count; i++) - { - Variable /*!*/ - v = cce.NonNull(OutParams[i]); - IdentifierExpr ie = new IdentifierExpr(v.tok, v); - Variable pv = cce.NonNull(Proc.OutParams[i]); - map.Add(pv, ie); - } - - this.formalMap = map; - - if (options.PrintWithUniqueASTIds) - { - options.OutputWriter.WriteLine("Implementation.GetImplFormalMap on {0}:", this.Name); - using TokenTextWriter stream = - new TokenTextWriter("", options.OutputWriter, /*setTokens=*/false, /*pretty=*/ false, options); - foreach (var e in map) - { - options.OutputWriter.Write(" "); - cce.NonNull((Variable /*!*/) e.Key).Emit(stream, 0); - options.OutputWriter.Write(" --> "); - cce.NonNull((Expr) e.Value).Emit(stream); - options.OutputWriter.WriteLine(); - } - } - - return map; - } - } - - /// - /// Return a collection of blocks that are reachable from the block passed as a parameter. - /// The block must be defined in the current implementation - /// - public ICollection GetConnectedComponents(Block startingBlock) - { - Contract.Requires(startingBlock != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>(), true)); - Contract.Assert(this.Blocks.Contains(startingBlock)); - - if (!this.BlockPredecessorsComputed) - { - ComputeStronglyConnectedComponents(); - } - -#if DEBUG_PRINT - System.Console.WriteLine("* Strongly connected components * \n{0} \n ** ", scc); -#endif - - foreach (ICollection component in cce.NonNull(this.scc)) - { - foreach (Block /*!*/ b in component) - { - Contract.Assert(b != null); - if (b == startingBlock) // We found the compontent that owns the startingblock - { - return component; - } - } - } - - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // if we are here, it means that the block is not in one of the components. This is an error. - } - - /// - /// Compute the strongly connected compontents of the blocks in the implementation. - /// As a side effect, it also computes the "predecessor" relation for the block in the implementation - /// - override public void ComputeStronglyConnectedComponents() - { - if (!this.BlockPredecessorsComputed) - { - ComputePredecessorsForBlocks(); - } - - Adjacency next = new Adjacency(Successors); - Adjacency prev = new Adjacency(Predecessors); - - this.scc = new StronglyConnectedComponents(this.Blocks, next, prev); - scc.Compute(); - - - foreach (Block /*!*/ block in this.Blocks) - { - Contract.Assert(block != null); - block.Predecessors = new List(); - } - } - - /// - /// Reset the abstract stated computed before - /// - override public void ResetAbstractInterpretationState() - { - foreach (Block /*!*/ b in this.Blocks) - { - Contract.Assert(b != null); - b.ResetAbstractInterpretationState(); - } - } - - /// - /// A private method used as delegate for the strongly connected components. - /// It return, given a node, the set of its successors - /// - private IEnumerable /**/ /*!*/ Successors(Block node) - { - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - - GotoCmd gotoCmd = node.TransferCmd as GotoCmd; - - if (gotoCmd != null) - { - // If it is a gotoCmd - Contract.Assert(gotoCmd.labelTargets != null); - - return gotoCmd.labelTargets; - } - else - { - // otherwise must be a ReturnCmd - Contract.Assert(node.TransferCmd is ReturnCmd); - - return new List(); - } - } - - /// - /// A private method used as delegate for the strongly connected components. - /// It return, given a node, the set of its predecessors - /// - private IEnumerable /**/ /*!*/ Predecessors(Block node) - { - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - - Contract.Assert(this.BlockPredecessorsComputed); - - return node.Predecessors; - } - - /// - /// Compute the predecessor informations for the blocks - /// - public void ComputePredecessorsForBlocks() - { - var blocks = this.Blocks; - foreach (Block b in blocks) - { - b.Predecessors = new List(); - } - - ComputePredecessorsForBlocks(blocks); - - this.BlockPredecessorsComputed = true; - } - - public static void ComputePredecessorsForBlocks(List blocks) - { - foreach (var block in blocks) { - if (block.TransferCmd is not GotoCmd gtc) { - continue; - } - - Contract.Assert(gtc.labelTargets != null); - foreach (var /*!*/ dest in gtc.labelTargets) - { - Contract.Assert(dest != null); - dest.Predecessors.Add(block); - } - } - } - - public void PruneUnreachableBlocks(CoreOptions options) - { - var toVisit = new Stack(); - var reachableBlocks = new List(); - var reachable = new HashSet(); // the set of elements in "reachableBlocks" - - toVisit.Push(Blocks[0]); - while (toVisit.Count != 0) - { - var block = toVisit.Pop(); - if (!reachable.Add(block)) { - continue; - } - - reachableBlocks.Add(block); - if (block.TransferCmd is GotoCmd gotoCmd) { - if (options.PruneInfeasibleEdges) { - foreach (var command in block.Cmds) { - Contract.Assert(command != null); - if (command is PredicateCmd { Expr: LiteralExpr { IsFalse: true } }) { - // This statement sequence will never reach the end, because of this "assume false" or "assert false". - // Hence, it does not reach its successors. - block.TransferCmd = new ReturnCmd(block.TransferCmd.tok); - goto NEXT_BLOCK; - } - } - } - - // it seems that the goto statement at the end may be reached - foreach (var next in gotoCmd.labelTargets) { - Contract.Assume(next != null); - toVisit.Push(next); - } - } - - NEXT_BLOCK: - { - } - } - - this.Blocks = reachableBlocks; - } - - public override Absy StdDispatch(StandardVisitor visitor) - { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitImplementation(this); - } - - public void FreshenCaptureStates() - { - // Assume commands with the "captureState" attribute allow model states to be - // captured for error reporting. - // Some program transformations, such as loop unrolling, duplicate parts of the - // program, leading to "capture-state-assumes" being duplicated. This leads - // to ambiguity when getting a state from the model. - // This method replaces the key of every "captureState" attribute with something - // unique - - int FreshCounter = 0; - foreach (var b in Blocks) - { - List newCmds = new List(); - for (int i = 0; i < b.Cmds.Count(); i++) - { - var a = b.Cmds[i] as AssumeCmd; - if (a != null && (QKeyValue.FindStringAttribute(a.Attributes, "captureState") != null)) - { - string StateName = QKeyValue.FindStringAttribute(a.Attributes, "captureState"); - newCmds.Add(new AssumeCmd(Token.NoToken, a.Expr, FreshenCaptureState(a.Attributes, FreshCounter))); - FreshCounter++; - } - else - { - newCmds.Add(b.Cmds[i]); - } - } - - b.Cmds = newCmds; - } - } - - private QKeyValue FreshenCaptureState(QKeyValue Attributes, int FreshCounter) - { - // Returns attributes identical to Attributes, but: - // - reversed (for ease of implementation; should not matter) - // - with the value for "captureState" replaced by a fresh value - Contract.Requires(QKeyValue.FindStringAttribute(Attributes, "captureState") != null); - string FreshValue = QKeyValue.FindStringAttribute(Attributes, "captureState") + "$renamed$" + Name + "$" + - FreshCounter; - - QKeyValue result = null; - while (Attributes != null) - { - if (Attributes.Key.Equals("captureState")) - { - result = new QKeyValue(Token.NoToken, Attributes.Key, new List() {FreshValue}, result); - } - else - { - result = new QKeyValue(Token.NoToken, Attributes.Key, Attributes.Params, result); - } - - Attributes = Attributes.Next; - } - - return result; - } - } - public class TypedIdent : Absy { diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index 76123cb38..3a0bc2f09 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -1189,225 +1189,6 @@ public override void Emit(TokenTextWriter stream, int level) //--------------------------------------------------------------------- // Block - public sealed class Block : Absy - { - private string /*!*/ label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal - - public string /*!*/ Label - { - get - { - Contract.Ensures(Contract.Result() != null); - return this.label; - } - set - { - Contract.Requires(value != null); - this.label = value; - } - } - - [Rep] [ElementsPeer] public List /*!*/ cmds; - - public List /*!*/ Cmds - { - get - { - Contract.Ensures(Contract.Result>() != null); - return this.cmds; - } - set - { - Contract.Requires(value != null); - this.cmds = value; - } - } - - public IEnumerable Exits() - { - if (TransferCmd is GotoCmd g) - { - return cce.NonNull(g.labelTargets); - } - return new List(); - } - - [Rep] //PM: needed to verify Traverse.Visit - public TransferCmd - TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures) - - public byte[] Checksum; - - // Abstract interpretation - - // public bool currentlyTraversed; - - public enum VisitState - { - ToVisit, - BeingVisited, - AlreadyVisited - } // used by WidenPoints.Compute - - public VisitState TraversingStatus; - - public int aiId; // block ID used by the abstract interpreter, which may change these numbers with each AI run - public bool widenBlock; - - public int - iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not - - // VC generation and SCC computation - public List /*!*/ Predecessors; - - // This field is used during passification to null-out entries in block2Incarnation dictionary early - public int succCount; - - private HashSet _liveVarsBefore; - - public IEnumerable liveVarsBefore - { - get - { - Contract.Ensures(cce.NonNullElements(Contract.Result>(), true)); - if (this._liveVarsBefore == null) - { - return null; - } - else - { - return this._liveVarsBefore.AsEnumerable(); - } - } - set - { - Contract.Requires(cce.NonNullElements(value, true)); - if (value == null) - { - this._liveVarsBefore = null; - } - else - { - this._liveVarsBefore = new HashSet(value); - } - } - } - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(this.label != null); - Contract.Invariant(this.cmds != null); - Contract.Invariant(cce.NonNullElements(this._liveVarsBefore, true)); - } - - public bool IsLive(Variable v) - { - Contract.Requires(v != null); - if (liveVarsBefore == null) - { - return true; - } - - return liveVarsBefore.Contains(v); - } - - public Block() - : this(Token.NoToken, "", new List(), new ReturnCmd(Token.NoToken)) - { - } - - public Block(IToken tok, string /*!*/ label, List /*!*/ cmds, TransferCmd transferCmd) - : base(tok) - { - Contract.Requires(label != null); - Contract.Requires(cmds != null); - Contract.Requires(tok != null); - this.label = label; - this.cmds = cmds; - this.TransferCmd = transferCmd; - this.Predecessors = new List(); - this._liveVarsBefore = null; - this.TraversingStatus = VisitState.ToVisit; - this.iterations = 0; - } - - public void Emit(TokenTextWriter stream, int level) - { - Contract.Requires(stream != null); - stream.WriteLine(); - stream.WriteLine( - this, - level, - "{0}:{1}", - stream.Options.PrintWithUniqueASTIds - ? String.Format("h{0}^^{1}", this.GetHashCode(), this.Label) - : this.Label, - this.widenBlock ? " // cut point" : ""); - - foreach (Cmd /*!*/ c in this.Cmds) - { - Contract.Assert(c != null); - c.Emit(stream, level + 1); - } - - Contract.Assume(this.TransferCmd != null); - this.TransferCmd.Emit(stream, level + 1); - } - - public void Register(ResolutionContext rc) - { - Contract.Requires(rc != null); - rc.AddBlock(this); - } - - public override void Resolve(ResolutionContext rc) - { - foreach (Cmd /*!*/ c in Cmds) - { - Contract.Assert(c != null); - c.Resolve(rc); - } - - Contract.Assume(this.TransferCmd != null); - TransferCmd.Resolve(rc); - } - - public override void Typecheck(TypecheckingContext tc) - { - foreach (Cmd /*!*/ c in Cmds) - { - Contract.Assert(c != null); - c.Typecheck(tc); - } - - Contract.Assume(this.TransferCmd != null); - TransferCmd.Typecheck(tc); - } - - /// - /// Reset the abstract intepretation state of this block. It does this by putting the iterations to 0 and the pre and post states to null - /// - public void ResetAbstractInterpretationState() - { - // this.currentlyTraversed = false; - this.TraversingStatus = VisitState.ToVisit; - this.iterations = 0; - } - - [Pure] - public override string ToString() - { - Contract.Ensures(Contract.Result() != null); - return this.Label + (this.widenBlock ? "[w]" : ""); - } - - public override Absy StdDispatch(StandardVisitor visitor) - { - Contract.Ensures(Contract.Result() != null); - return visitor.VisitBlock(this); - } - } //--------------------------------------------------------------------- // Commands @@ -3716,7 +3497,7 @@ void ObjectInvariant() { Contract.Invariant(labelNames == null || labelTargets == null || labelNames.Count == labelTargets.Count); } - + [NotDelayed] public GotoCmd(IToken /*!*/ tok, List /*!*/ labelSeq) : base(tok) @@ -3758,6 +3539,11 @@ public GotoCmd(IToken /*!*/ tok, List /*!*/ blockSeq) this.labelTargets = blockSeq; } + public void RemoveTarget(Block b) { + labelNames.Remove(b.Label); + labelTargets.Remove(b); + } + public void AddTarget(Block b) { Contract.Requires(b != null); diff --git a/Source/Core/AST/Block.cs b/Source/Core/AST/Block.cs new file mode 100644 index 000000000..3e4aa3277 --- /dev/null +++ b/Source/Core/AST/Block.cs @@ -0,0 +1,226 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace Microsoft.Boogie; + +public sealed class Block : Absy +{ + private string /*!*/ label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal + + public string /*!*/ Label + { + get + { + Contract.Ensures(Contract.Result() != null); + return this.label; + } + set + { + Contract.Requires(value != null); + this.label = value; + } + } + + [Rep] [ElementsPeer] public List /*!*/ cmds; + + public List /*!*/ Cmds + { + get + { + Contract.Ensures(Contract.Result>() != null); + return this.cmds; + } + set + { + Contract.Requires(value != null); + this.cmds = value; + } + } + + public IEnumerable Exits() + { + if (TransferCmd is GotoCmd g) + { + return cce.NonNull(g.labelTargets); + } + return new List(); + } + + [Rep] //PM: needed to verify Traverse.Visit + public TransferCmd + TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures) + + public byte[] Checksum; + + // Abstract interpretation + + // public bool currentlyTraversed; + + public enum VisitState + { + ToVisit, + BeingVisited, + AlreadyVisited + } // used by WidenPoints.Compute + + public VisitState TraversingStatus; + + public int aiId; // block ID used by the abstract interpreter, which may change these numbers with each AI run + public bool widenBlock; + + public int + iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not + + // VC generation and SCC computation + public List /*!*/ Predecessors; + + // This field is used during passification to null-out entries in block2Incarnation dictionary early + public int succCount; + + private HashSet _liveVarsBefore; + + public IEnumerable liveVarsBefore + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result>(), true)); + if (this._liveVarsBefore == null) + { + return null; + } + else + { + return this._liveVarsBefore.AsEnumerable(); + } + } + set + { + Contract.Requires(cce.NonNullElements(value, true)); + if (value == null) + { + this._liveVarsBefore = null; + } + else + { + this._liveVarsBefore = new HashSet(value); + } + } + } + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(this.label != null); + Contract.Invariant(this.cmds != null); + Contract.Invariant(cce.NonNullElements(this._liveVarsBefore, true)); + } + + public bool IsLive(Variable v) + { + Contract.Requires(v != null); + if (liveVarsBefore == null) + { + return true; + } + + return liveVarsBefore.Contains(v); + } + + public Block() + : this(Token.NoToken, "", new List(), new ReturnCmd(Token.NoToken)) + { + } + + public Block(IToken tok, string /*!*/ label, List /*!*/ cmds, TransferCmd transferCmd) + : base(tok) + { + Contract.Requires(label != null); + Contract.Requires(cmds != null); + Contract.Requires(tok != null); + this.label = label; + this.cmds = cmds; + this.TransferCmd = transferCmd; + this.Predecessors = new List(); + this._liveVarsBefore = null; + this.TraversingStatus = VisitState.ToVisit; + this.iterations = 0; + } + + public void Emit(TokenTextWriter stream, int level) + { + Contract.Requires(stream != null); + stream.WriteLine(); + stream.WriteLine( + this, + level, + "{0}:{1}", + stream.Options.PrintWithUniqueASTIds + ? String.Format("h{0}^^{1}", this.GetHashCode(), this.Label) + : this.Label, + this.widenBlock ? " // cut point" : ""); + + foreach (Cmd /*!*/ c in this.Cmds) + { + Contract.Assert(c != null); + c.Emit(stream, level + 1); + } + + Contract.Assume(this.TransferCmd != null); + this.TransferCmd.Emit(stream, level + 1); + } + + public void Register(ResolutionContext rc) + { + Contract.Requires(rc != null); + rc.AddBlock(this); + } + + public override void Resolve(ResolutionContext rc) + { + foreach (Cmd /*!*/ c in Cmds) + { + Contract.Assert(c != null); + c.Resolve(rc); + } + + Contract.Assume(this.TransferCmd != null); + TransferCmd.Resolve(rc); + } + + public override void Typecheck(TypecheckingContext tc) + { + foreach (Cmd /*!*/ c in Cmds) + { + Contract.Assert(c != null); + c.Typecheck(tc); + } + + Contract.Assume(this.TransferCmd != null); + TransferCmd.Typecheck(tc); + } + + /// + /// Reset the abstract intepretation state of this block. It does this by putting the iterations to 0 and the pre and post states to null + /// + public void ResetAbstractInterpretationState() + { + // this.currentlyTraversed = false; + this.TraversingStatus = VisitState.ToVisit; + this.iterations = 0; + } + + [Pure] + public override string ToString() + { + Contract.Ensures(Contract.Result() != null); + return this.Label + (this.widenBlock ? "[w]" : ""); + } + + public override Absy StdDispatch(StandardVisitor visitor) + { + Contract.Ensures(Contract.Result() != null); + return visitor.VisitBlock(this); + } +} \ No newline at end of file diff --git a/Source/Core/AST/Implementation.cs b/Source/Core/AST/Implementation.cs new file mode 100644 index 000000000..9169f014b --- /dev/null +++ b/Source/Core/AST/Implementation.cs @@ -0,0 +1,1093 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie.GraphUtil; + +namespace Microsoft.Boogie; + +public class Implementation : DeclWithFormals { + public List LocVars; + + [Rep] public StmtList StructuredStmts; + + [field: Rep] + public List Blocks { + get; + set; + } + public Procedure Proc; + + // Blocks before applying passification etc. + // Both are used only when /inline is set. + public List OriginalBlocks; + public List OriginalLocVars; + + // Map filled in during passification to allow augmented error trace reporting + public Dictionary> debugInfos = new(); + + public readonly ISet AssertionChecksums = new HashSet(ChecksumComparer.Default); + + public sealed class ChecksumComparer : IEqualityComparer + { + static IEqualityComparer defaultComparer; + + public static IEqualityComparer Default + { + get + { + if (defaultComparer == null) + { + defaultComparer = new ChecksumComparer(); + } + + return defaultComparer; + } + } + + public bool Equals(byte[] x, byte[] y) + { + if (x == null || y == null) + { + return x == y; + } + else + { + return x.SequenceEqual(y); + } + } + + public int GetHashCode(byte[] checksum) + { + if (checksum == null) + { + throw new ArgumentNullException("checksum"); + } + else + { + var result = 17; + for (int i = 0; i < checksum.Length; i++) + { + result = result * 23 + checksum[i]; + } + + return result; + } + } + } + + public void AddAssertionChecksum(byte[] checksum) + { + Contract.Requires(checksum != null); + + if (AssertionChecksums != null) + { + AssertionChecksums.Add(checksum); + } + } + + public ISet AssertionChecksumsInCachedSnapshot { get; set; } + + public bool IsAssertionChecksumInCachedSnapshot(byte[] checksum) + { + Contract.Requires(AssertionChecksumsInCachedSnapshot != null); + + return AssertionChecksumsInCachedSnapshot.Contains(checksum); + } + + public IList RecycledFailingAssertions { get; protected set; } + + public void AddRecycledFailingAssertion(AssertCmd assertion) + { + if (RecycledFailingAssertions == null) + { + RecycledFailingAssertions = new List(); + } + + RecycledFailingAssertions.Add(assertion); + } + + public Cmd ExplicitAssumptionAboutCachedPrecondition { get; set; } + + // Strongly connected components + private StronglyConnectedComponents scc; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(LocVars != null); + Contract.Invariant(cce.NonNullElements(Blocks)); + Contract.Invariant(cce.NonNullElements(OriginalBlocks, true)); + Contract.Invariant(cce.NonNullElements(scc, true)); + } + + private bool BlockPredecessorsComputed; + + public bool StronglyConnectedComponentsComputed + { + get { return this.scc != null; } + } + + public bool IsSkipVerification(CoreOptions options) + { + bool verify = true; + cce.NonNull(this.Proc).CheckBooleanAttribute("verify", ref verify); + this.CheckBooleanAttribute("verify", ref verify); + if (!verify) { + return true; + } + + if (options.ProcedureInlining == CoreOptions.Inlining.Assert || + options.ProcedureInlining == CoreOptions.Inlining.Assume) { + Expr inl = this.FindExprAttribute("inline"); + if (inl == null) { + inl = this.Proc.FindExprAttribute("inline"); + } + + if (inl != null) { + return true; + } + } + + if (options.StratifiedInlining > 0) { + return !QKeyValue.FindBoolAttribute(Attributes, "entrypoint"); + } + + return false; + } + + public string Id + { + get + { + var id = (this as ICarriesAttributes).FindStringAttribute("id"); + if (id == null) + { + id = Name + GetHashCode().ToString() + ":0"; + } + + return id; + } + } + + public int Priority + { + get + { + int priority = 0; + CheckIntAttribute("priority", ref priority); + if (priority <= 0) + { + priority = 1; + } + + return priority; + } + } + + public Dictionary GetExtraSMTOptions() + { + Dictionary extraSMTOpts = new(); + for (var a = Attributes; a != null; a = a.Next) { + var n = a.Params.Count; + var k = a.Key; + if (k.Equals("smt_option")) { + if (n == 2 && a.Params[0] is string s) { + extraSMTOpts.Add(s, a.Params[1].ToString()); + } + } + } + + return extraSMTOpts; + } + + public IDictionary ErrorChecksumToCachedError { get; private set; } + + public bool IsErrorChecksumInCachedSnapshot(byte[] checksum) + { + Contract.Requires(ErrorChecksumToCachedError != null); + + return ErrorChecksumToCachedError.ContainsKey(checksum); + } + + public void SetErrorChecksumToCachedError(IEnumerable> errors) + { + Contract.Requires(errors != null); + + ErrorChecksumToCachedError = new Dictionary(ChecksumComparer.Default); + foreach (var kv in errors) + { + ErrorChecksumToCachedError[kv.Item1] = kv.Item3; + if (kv.Item2 != null) + { + ErrorChecksumToCachedError[kv.Item2] = null; + } + } + } + + public bool HasCachedSnapshot + { + get { return ErrorChecksumToCachedError != null && AssertionChecksumsInCachedSnapshot != null; } + } + + public bool AnyErrorsInCachedSnapshot + { + get + { + Contract.Requires(ErrorChecksumToCachedError != null); + + return ErrorChecksumToCachedError.Any(); + } + } + + IList injectedAssumptionVariables; + + public IList InjectedAssumptionVariables + { + get { return injectedAssumptionVariables != null ? injectedAssumptionVariables : new List(); } + } + + IList doomedInjectedAssumptionVariables; + + public IList DoomedInjectedAssumptionVariables + { + get + { + return doomedInjectedAssumptionVariables != null + ? doomedInjectedAssumptionVariables + : new List(); + } + } + + public List RelevantInjectedAssumptionVariables(Dictionary incarnationMap) + { + return InjectedAssumptionVariables.Where(v => + { + if (incarnationMap.TryGetValue(v, out var e)) + { + var le = e as LiteralExpr; + return le == null || !le.IsTrue; + } + else + { + return false; + } + }).ToList(); + } + + public List RelevantDoomedInjectedAssumptionVariables(Dictionary incarnationMap) + { + return DoomedInjectedAssumptionVariables.Where(v => + { + if (incarnationMap.TryGetValue(v, out var e)) + { + var le = e as LiteralExpr; + return le == null || !le.IsTrue; + } + else + { + return false; + } + }).ToList(); + } + + public Expr ConjunctionOfInjectedAssumptionVariables(Dictionary incarnationMap, out bool isTrue) + { + Contract.Requires(incarnationMap != null); + + var vars = RelevantInjectedAssumptionVariables(incarnationMap).Select(v => incarnationMap[v]).ToList(); + isTrue = vars.Count == 0; + return LiteralExpr.BinaryTreeAnd(vars); + } + + public void InjectAssumptionVariable(LocalVariable variable, bool isDoomed = false) + { + LocVars.Add(variable); + if (isDoomed) + { + if (doomedInjectedAssumptionVariables == null) + { + doomedInjectedAssumptionVariables = new List(); + } + + doomedInjectedAssumptionVariables.Add(variable); + } + else + { + if (injectedAssumptionVariables == null) + { + injectedAssumptionVariables = new List(); + } + + injectedAssumptionVariables.Add(variable); + } + } + + public Implementation(IToken tok, string name, List typeParams, List inParams, + List outParams, List localVariables, [Captured] StmtList structuredStmts, QKeyValue kv) + : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) + { + Contract.Requires(structuredStmts != null); + Contract.Requires(localVariables != null); + Contract.Requires(outParams != null); + Contract.Requires(inParams != null); + Contract.Requires(typeParams != null); + Contract.Requires(name != null); + Contract.Requires(tok != null); + //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()); + } + + public Implementation(IToken tok, string name, List typeParams, List inParams, + List outParams, List localVariables, [Captured] StmtList structuredStmts) + : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()) + { + Contract.Requires(structuredStmts != null); + Contract.Requires(localVariables != null); + Contract.Requires(outParams != null); + Contract.Requires(inParams != null); + Contract.Requires(typeParams != null); + Contract.Requires(name != null); + Contract.Requires(tok != null); + //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()); + } + + public Implementation(IToken tok, string name, List typeParams, List inParams, + List outParams, List localVariables, [Captured] StmtList structuredStmts, Errors errorHandler) + : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler) + { + Contract.Requires(errorHandler != null); + Contract.Requires(structuredStmts != null); + Contract.Requires(localVariables != null); + Contract.Requires(outParams != null); + Contract.Requires(inParams != null); + Contract.Requires(typeParams != null); + Contract.Requires(name != null); + Contract.Requires(tok != null); + //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler); + } + + public Implementation(IToken /*!*/ tok, + string /*!*/ name, + List /*!*/ typeParams, + List /*!*/ inParams, + List /*!*/ outParams, + List /*!*/ localVariables, + [Captured] StmtList /*!*/ structuredStmts, + QKeyValue kv, + Errors /*!*/ errorHandler) + : base(tok, name, typeParams, inParams, outParams) + { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(typeParams != null); + Contract.Requires(inParams != null); + Contract.Requires(outParams != null); + Contract.Requires(localVariables != null); + Contract.Requires(structuredStmts != null); + Contract.Requires(errorHandler != null); + LocVars = localVariables; + StructuredStmts = structuredStmts; + BigBlocksResolutionContext ctx = new BigBlocksResolutionContext(structuredStmts, errorHandler); + Blocks = ctx.Blocks; + BlockPredecessorsComputed = false; + scc = null; + Attributes = kv; + } + + public Implementation(IToken tok, string name, List typeParams, List inParams, + List outParams, List localVariables, [Captured] List block) + : this(tok, name, typeParams, inParams, outParams, localVariables, block, null) + { + Contract.Requires(cce.NonNullElements(block)); + Contract.Requires(localVariables != null); + Contract.Requires(outParams != null); + Contract.Requires(inParams != null); + Contract.Requires(typeParams != null); + Contract.Requires(name != null); + Contract.Requires(tok != null); + //:this(tok, name, typeParams, inParams, outParams, localVariables, block, null); + } + + public Implementation(IToken /*!*/ tok, + string /*!*/ name, + List /*!*/ typeParams, + List /*!*/ inParams, + List /*!*/ outParams, + List /*!*/ localVariables, + [Captured] List /*!*/ blocks, + QKeyValue kv) + : base(tok, name, typeParams, inParams, outParams) + { + Contract.Requires(name != null); + Contract.Requires(inParams != null); + Contract.Requires(outParams != null); + Contract.Requires(localVariables != null); + Contract.Requires(cce.NonNullElements(blocks)); + LocVars = localVariables; + Blocks = blocks; + BlockPredecessorsComputed = false; + scc = null; + Attributes = kv; + } + + public override void Emit(TokenTextWriter stream, int level) { + void BlocksWriters(TokenTextWriter stream) { + if (this.StructuredStmts != null && !stream.Options.PrintInstrumented && !stream.Options.PrintInlined) { + if (this.LocVars.Count > 0) { + stream.WriteLine(); + } + + if (stream.Options.PrintUnstructured < 2) { + if (stream.Options.PrintUnstructured == 1) { + stream.WriteLine(this, level + 1, "/*** structured program:"); + } + + this.StructuredStmts.Emit(stream, level + 1); + if (stream.Options.PrintUnstructured == 1) { + stream.WriteLine(level + 1, "**** end structured program */"); + } + } + } + + if (StructuredStmts == null || 1 <= stream.Options.PrintUnstructured || + stream.Options.PrintInstrumented || stream.Options.PrintInlined) { + foreach (Block b in Blocks) { + b.Emit(stream, level + 1); + } + } + } + + EmitImplementation(stream, level, BlocksWriters, showLocals: true); + } + + public void EmitImplementation(TokenTextWriter stream, int level, IEnumerable blocks, + bool showLocals) { + EmitImplementation(stream, level, writer => { + foreach (var block in blocks) { + block.Emit(writer, level + 1); + } + }, showLocals); + } + + public void EmitImplementation(TokenTextWriter stream, int level, Action printBlocks, bool showLocals) + { + stream.Write(this, level, "implementation "); + EmitAttributes(stream); + stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); + EmitSignature(stream, false); + stream.WriteLine(); + + stream.WriteLine(level, "{0}", '{'); + + if (showLocals) { + foreach (Variable /*!*/ v in this.LocVars) + { + Contract.Assert(v != null); + v.Emit(stream, level + 1); + } + } + + printBlocks(stream); + + stream.WriteLine(level, "{0}", '}'); + + stream.WriteLine(); + stream.WriteLine(); + } + + public override void Register(ResolutionContext rc) + { + // nothing to register + } + + public override void Resolve(ResolutionContext rc) + { + if (Proc != null) + { + // already resolved + return; + } + + Proc = rc.LookUpProcedure(cce.NonNull(this.Name)); + if (Proc == null) + { + rc.Error(this, "implementation given for undeclared procedure: {0}", this.Name); + } + else if (Proc is ActionDecl actionDecl) + { + actionDecl.Impl = this; + } + + int previousTypeBinderState = rc.TypeBinderState; + try + { + RegisterTypeParameters(rc); + + rc.PushVarContext(); + rc.Proc = Proc; + RegisterFormals(InParams, rc); + RegisterFormals(OutParams, rc); + foreach (Variable v in LocVars) + { + Contract.Assert(v != null); + v.Register(rc); + v.Resolve(rc); + } + rc.Proc = null; + + foreach (Variable v in LocVars) + { + Contract.Assert(v != null); + v.ResolveWhere(rc); + } + + rc.PushProcedureContext(); + foreach (Block b in Blocks) + { + b.Register(rc); + } + + (this as ICarriesAttributes).ResolveAttributes(rc); + + rc.Proc = Proc; + rc.StateMode = Proc.IsPure ? ResolutionContext.State.StateLess : ResolutionContext.State.Two; + foreach (Block b in Blocks) + { + b.Resolve(rc); + } + rc.Proc = null; + rc.StateMode = ResolutionContext.State.Single; + + rc.PopProcedureContext(); + rc.PopVarContext(); + + Type.CheckBoundVariableOccurrences(TypeParameters, + InParams.Select(Item => Item.TypedIdent.Type).ToList(), + OutParams.Select(Item => Item.TypedIdent.Type).ToList(), + this.tok, "implementation arguments", + rc); + } + finally + { + rc.TypeBinderState = previousTypeBinderState; + } + + SortTypeParams(); + } + + public override void Typecheck(TypecheckingContext tc) + { + //Contract.Requires(tc != null); + base.Typecheck(tc); + + Contract.Assume(this.Proc != null); + + if (this.TypeParameters.Count != Proc.TypeParameters.Count) + { + tc.Error(this, "mismatched number of type parameters in procedure implementation: {0}", + this.Name); + } + else + { + // if the numbers of type parameters are different, it is + // difficult to compare the argument types + MatchFormals(this.InParams, Proc.InParams, "in", tc); + MatchFormals(this.OutParams, Proc.OutParams, "out", tc); + } + + var oldProc = tc.Proc; + tc.Proc = Proc; + tc.Impl = this; + foreach (Variable /*!*/ v in LocVars) + { + Contract.Assert(v != null); + v.Typecheck(tc); + } + foreach (Block b in Blocks) + { + b.Typecheck(tc); + } + Contract.Assert(tc.Proc == Proc); + tc.Impl = null; + tc.Proc = oldProc; + + if (Proc is ActionDecl || Proc is YieldProcedureDecl) + { + var graph = Program.GraphFromImpl(this); + if (!Graph.Acyclic(graph)) + { + if (Proc is ActionDecl) + { + tc.Error(this, "action implementation may not have loops"); + } + else // Proc is YieldProcedureDecl + { + graph.ComputeLoops(); + if (!graph.Reducible) + { + tc.Error(this, "irreducible control flow graph not allowed"); + } + else + { + TypecheckLoopAnnotations(tc, graph); + } + } + } + } + } + + private void TypecheckLoopAnnotations(TypecheckingContext tc, Graph graph) + { + var yieldingProc = (YieldProcedureDecl)Proc; + foreach (var header in graph.Headers) + { + var yieldingLayer = yieldingProc.Layer; + var yieldCmd = (PredicateCmd)header.Cmds.FirstOrDefault(cmd => + cmd is PredicateCmd predCmd && predCmd.HasAttribute(CivlAttributes.YIELDS)); + if (yieldCmd == null) + { + yieldingLayer = int.MinValue; + } + else + { + var layers = yieldCmd.Layers; + header.Cmds.Remove(yieldCmd); + if (layers.Any()) + { + if (layers.Count > 1) + { + tc.Error(header, "expected layer attribute to indicate the highest yielding layer of this loop"); + continue; + } + if (layers[0] > yieldingLayer) + { + tc.Error(header, + "yielding layer of loop must not be more than the layer of enclosing procedure"); + continue; + } + yieldingLayer = layers[0]; + } + } + + var yieldInvariants = header.Cmds + .TakeWhile(cmd => cmd is CallCmd { Proc: YieldInvariantDecl }).OfType() + .ToList(); + header.Cmds.RemoveRange(0, yieldInvariants.Count); + if (yieldInvariants.Any() && yieldCmd == null) + { + tc.Error(header, "expected :yields attribute on this loop"); + } + foreach (var callCmd in yieldInvariants) + { + var yieldInvariant = (YieldInvariantDecl)callCmd.Proc; + var calleeLayerNum = yieldInvariant.Layer; + if (calleeLayerNum > yieldingLayer) + { + tc.Error(callCmd, $"loop must yield at layer {calleeLayerNum} of the called yield invariant"); + } + } + foreach (var predCmd in header.Cmds.TakeWhile(cmd => cmd is PredicateCmd).OfType()) + { + if (predCmd.Layers.Min() <= yieldingLayer && + VariableCollector.Collect(predCmd, true).OfType().Any()) + { + tc.Error(predCmd, + "invariant may not access a global variable since one of its layers is a yielding layer of its loop"); + } + } + + yieldingProc.YieldingLoops[header] = new YieldingLoop(yieldingLayer, yieldInvariants); + } + } + + void MatchFormals(List /*!*/ implFormals, List /*!*/ procFormals, string /*!*/ inout, + TypecheckingContext /*!*/ tc) + { + Contract.Requires(implFormals != null); + Contract.Requires(procFormals != null); + Contract.Requires(inout != null); + Contract.Requires(tc != null); + if (implFormals.Count != procFormals.Count) + { + tc.Error(this, "mismatched number of {0}-parameters in procedure implementation: {1}", + inout, this.Name); + } + else + { + // unify the type parameters so that types can be compared + Contract.Assert(Proc != null); + Contract.Assert(this.TypeParameters.Count == Proc.TypeParameters.Count); + + IDictionary /*!*/ + subst1 = + new Dictionary(); + IDictionary /*!*/ + subst2 = + new Dictionary(); + + for (int i = 0; i < this.TypeParameters.Count; ++i) + { + TypeVariable /*!*/ + newVar = + new TypeVariable(Token.NoToken, Proc.TypeParameters[i].Name); + Contract.Assert(newVar != null); + subst1.Add(Proc.TypeParameters[i], newVar); + subst2.Add(this.TypeParameters[i], newVar); + } + + for (int i = 0; i < implFormals.Count; i++) + { + // the names of the formals are allowed to change from the proc to the impl + + // but types must be identical + Type t = cce.NonNull((Variable) implFormals[i]).TypedIdent.Type.Substitute(subst2); + Type u = cce.NonNull((Variable) procFormals[i]).TypedIdent.Type.Substitute(subst1); + if (!t.Equals(u)) + { + string /*!*/ + a = cce.NonNull((Variable) implFormals[i]).Name; + Contract.Assert(a != null); + string /*!*/ + b = cce.NonNull((Variable) procFormals[i]).Name; + Contract.Assert(b != null); + string /*!*/ + c; + if (a == b) + { + c = a; + } + else + { + c = String.Format("{0} (named {1} in implementation)", b, a); + } + + tc.Error(this, "mismatched type of {0}-parameter in implementation {1}: {2}", inout, this.Name, c); + } + } + } + } + + private Dictionary /*?*/ + formalMap = null; + + public void ResetImplFormalMap() + { + this.formalMap = null; + } + + public Dictionary /*!*/ GetImplFormalMap(CoreOptions options) + { + Contract.Ensures(Contract.Result>() != null); + + if (this.formalMap != null) + { + return this.formalMap; + } + else + { + Dictionary /*!*/ + map = new Dictionary(InParams.Count + OutParams.Count); + + Contract.Assume(this.Proc != null); + Contract.Assume(InParams.Count == Proc.InParams.Count); + for (int i = 0; i < InParams.Count; i++) + { + Variable /*!*/ + v = InParams[i]; + Contract.Assert(v != null); + IdentifierExpr ie = new IdentifierExpr(v.tok, v); + Variable /*!*/ + pv = Proc.InParams[i]; + Contract.Assert(pv != null); + map.Add(pv, ie); + } + + System.Diagnostics.Debug.Assert(OutParams.Count == Proc.OutParams.Count); + for (int i = 0; i < OutParams.Count; i++) + { + Variable /*!*/ + v = cce.NonNull(OutParams[i]); + IdentifierExpr ie = new IdentifierExpr(v.tok, v); + Variable pv = cce.NonNull(Proc.OutParams[i]); + map.Add(pv, ie); + } + + this.formalMap = map; + + if (options.PrintWithUniqueASTIds) + { + options.OutputWriter.WriteLine("Implementation.GetImplFormalMap on {0}:", this.Name); + using TokenTextWriter stream = + new TokenTextWriter("", options.OutputWriter, /*setTokens=*/false, /*pretty=*/ false, options); + foreach (var e in map) + { + options.OutputWriter.Write(" "); + cce.NonNull((Variable /*!*/) e.Key).Emit(stream, 0); + options.OutputWriter.Write(" --> "); + cce.NonNull((Expr) e.Value).Emit(stream); + options.OutputWriter.WriteLine(); + } + } + + return map; + } + } + + /// + /// Return a collection of blocks that are reachable from the block passed as a parameter. + /// The block must be defined in the current implementation + /// + public ICollection GetConnectedComponents(Block startingBlock) + { + Contract.Requires(startingBlock != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>(), true)); + Contract.Assert(this.Blocks.Contains(startingBlock)); + + if (!this.BlockPredecessorsComputed) + { + ComputeStronglyConnectedComponents(); + } + +#if DEBUG_PRINT + System.Console.WriteLine("* Strongly connected components * \n{0} \n ** ", scc); +#endif + + foreach (ICollection component in cce.NonNull(this.scc)) + { + foreach (Block /*!*/ b in component) + { + Contract.Assert(b != null); + if (b == startingBlock) // We found the compontent that owns the startingblock + { + return component; + } + } + } + + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // if we are here, it means that the block is not in one of the components. This is an error. + } + + /// + /// Compute the strongly connected compontents of the blocks in the implementation. + /// As a side effect, it also computes the "predecessor" relation for the block in the implementation + /// + public override void ComputeStronglyConnectedComponents() + { + if (!this.BlockPredecessorsComputed) + { + ComputePredecessorsForBlocks(); + } + + Adjacency next = new Adjacency(Successors); + Adjacency prev = new Adjacency(Predecessors); + + this.scc = new StronglyConnectedComponents(this.Blocks, next, prev); + scc.Compute(); + + + foreach (Block /*!*/ block in this.Blocks) + { + Contract.Assert(block != null); + block.Predecessors = new List(); + } + } + + /// + /// Reset the abstract stated computed before + /// + override public void ResetAbstractInterpretationState() + { + foreach (Block /*!*/ b in this.Blocks) + { + Contract.Assert(b != null); + b.ResetAbstractInterpretationState(); + } + } + + /// + /// A private method used as delegate for the strongly connected components. + /// It return, given a node, the set of its successors + /// + private IEnumerable /**/ /*!*/ Successors(Block node) + { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + + GotoCmd gotoCmd = node.TransferCmd as GotoCmd; + + if (gotoCmd != null) + { + // If it is a gotoCmd + Contract.Assert(gotoCmd.labelTargets != null); + + return gotoCmd.labelTargets; + } + else + { + // otherwise must be a ReturnCmd + Contract.Assert(node.TransferCmd is ReturnCmd); + + return new List(); + } + } + + /// + /// A private method used as delegate for the strongly connected components. + /// It return, given a node, the set of its predecessors + /// + private IEnumerable /**/ /*!*/ Predecessors(Block node) + { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + + Contract.Assert(this.BlockPredecessorsComputed); + + return node.Predecessors; + } + + /// + /// Compute the predecessor informations for the blocks + /// + public void ComputePredecessorsForBlocks() + { + var blocks = this.Blocks; + foreach (Block b in blocks) + { + b.Predecessors = new List(); + } + + ComputePredecessorsForBlocks(blocks); + + this.BlockPredecessorsComputed = true; + } + + public static void ComputePredecessorsForBlocks(List blocks) + { + foreach (var block in blocks) { + if (block.TransferCmd is not GotoCmd gtc) { + continue; + } + + Contract.Assert(gtc.labelTargets != null); + foreach (var /*!*/ dest in gtc.labelTargets) + { + Contract.Assert(dest != null); + dest.Predecessors.Add(block); + } + } + } + + public void PruneUnreachableBlocks(CoreOptions options) + { + var toVisit = new Stack(); + var reachableBlocks = new List(); + var reachable = new HashSet(); // the set of elements in "reachableBlocks" + + toVisit.Push(Blocks[0]); + while (toVisit.Count != 0) + { + var block = toVisit.Pop(); + if (!reachable.Add(block)) { + continue; + } + + reachableBlocks.Add(block); + if (block.TransferCmd is GotoCmd gotoCmd) { + if (options.PruneInfeasibleEdges) { + foreach (var command in block.Cmds) { + Contract.Assert(command != null); + if (command is PredicateCmd { Expr: LiteralExpr { IsFalse: true } }) { + // This statement sequence will never reach the end, because of this "assume false" or "assert false". + // Hence, it does not reach its successors. + block.TransferCmd = new ReturnCmd(block.TransferCmd.tok); + goto NEXT_BLOCK; + } + } + } + + // it seems that the goto statement at the end may be reached + foreach (var next in gotoCmd.labelTargets) { + Contract.Assume(next != null); + toVisit.Push(next); + } + } + + NEXT_BLOCK: + { + } + } + + this.Blocks = reachableBlocks; + } + + public override Absy StdDispatch(StandardVisitor visitor) + { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitImplementation(this); + } + + public void FreshenCaptureStates() + { + // Assume commands with the "captureState" attribute allow model states to be + // captured for error reporting. + // Some program transformations, such as loop unrolling, duplicate parts of the + // program, leading to "capture-state-assumes" being duplicated. This leads + // to ambiguity when getting a state from the model. + // This method replaces the key of every "captureState" attribute with something + // unique + + int FreshCounter = 0; + foreach (var b in Blocks) + { + List newCmds = new List(); + for (int i = 0; i < b.Cmds.Count(); i++) + { + var a = b.Cmds[i] as AssumeCmd; + if (a != null && (QKeyValue.FindStringAttribute(a.Attributes, "captureState") != null)) + { + string StateName = QKeyValue.FindStringAttribute(a.Attributes, "captureState"); + newCmds.Add(new AssumeCmd(Token.NoToken, a.Expr, FreshenCaptureState(a.Attributes, FreshCounter))); + FreshCounter++; + } + else + { + newCmds.Add(b.Cmds[i]); + } + } + + b.Cmds = newCmds; + } + } + + private QKeyValue FreshenCaptureState(QKeyValue Attributes, int FreshCounter) + { + // Returns attributes identical to Attributes, but: + // - reversed (for ease of implementation; should not matter) + // - with the value for "captureState" replaced by a fresh value + Contract.Requires(QKeyValue.FindStringAttribute(Attributes, "captureState") != null); + string FreshValue = QKeyValue.FindStringAttribute(Attributes, "captureState") + "$renamed$" + Name + "$" + + FreshCounter; + + QKeyValue result = null; + while (Attributes != null) + { + if (Attributes.Key.Equals("captureState")) + { + result = new QKeyValue(Token.NoToken, Attributes.Key, new List() {FreshValue}, result); + } + else + { + result = new QKeyValue(Token.NoToken, Attributes.Key, Attributes.Params, result); + } + + Attributes = Attributes.Next; + } + + return result; + } +} \ No newline at end of file diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs index a171b549d..5684c315f 100644 --- a/Source/Core/AST/Program.cs +++ b/Source/Core/AST/Program.cs @@ -3,6 +3,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using System.Text; using Microsoft.Boogie.GraphUtil; namespace Microsoft.Boogie; diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs index 81d3ec591..5e2a19351 100644 --- a/Source/Core/CoreOptions.cs +++ b/Source/Core/CoreOptions.cs @@ -82,7 +82,8 @@ public enum VerbosityLevel int VcsMaxKeepGoingSplits { get; } double VcsMaxCost { get; } bool VcsSplitOnEveryAssert { get; } - string PrintPrunedFile { get; } + string PrintSplitFile { get; } + bool PrintSplitDeclarations { get; } bool PrettyPrint { get; } bool NormalizeDeclarationOrder { get; } XmlSink XmlSink { get; } diff --git a/Source/Core/PrintOptions.cs b/Source/Core/PrintOptions.cs index fc7663b44..80b4b8fc8 100644 --- a/Source/Core/PrintOptions.cs +++ b/Source/Core/PrintOptions.cs @@ -13,13 +13,13 @@ public interface PrintOptions { bool PrintInlined { get; } int StratifiedInlining { get; } bool PrintDesugarings { get; set; } - bool PrintPassive { get; set; } + string PrintPassiveFile { get; set; } int PrintUnstructured { get; set; } bool ReflectAdd { get; } } record PrintOptionsRec(bool PrintWithUniqueASTIds, bool PrintInstrumented, bool PrintInlined, int StratifiedInlining, bool ReflectAdd) : PrintOptions { public bool PrintDesugarings { get; set; } - public bool PrintPassive { get; set; } + public string PrintPassiveFile { get; set; } public int PrintUnstructured { get; set; } } \ No newline at end of file diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 5c1966e04..426c46e0b 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -65,7 +65,8 @@ void ObjectInvariant2() public int VerifySnapshots { get; set; } = -1; public bool VerifySeparately { get; set; } public string PrintFile { get; set; } - public string PrintPrunedFile { get; set; } + public string PrintSplitFile { get; set; } + public bool PrintSplitDeclarations { get; set; } /** * Whether to emit {:qid}, {:skolemid} and set-info :boogie-vc-id @@ -88,9 +89,9 @@ public bool PrintDesugarings { set => printDesugarings = value; } - public bool PrintPassive { - get => printPassive; - set => printPassive = value; + public string PrintPassiveFile { + get => printPassiveFile; + set => printPassiveFile = value; } public List> UseResolvedProgram { get; } = new(); @@ -600,7 +601,7 @@ void ObjectInvariant5() private bool printWithUniqueAstIds = false; private int printUnstructured = 0; private bool printDesugarings = false; - private bool printPassive = false; + private string printPassiveFile; private bool emitDebugInformation = true; private bool normalizeNames; private bool normalizeDeclarationOrder = true; @@ -698,9 +699,25 @@ protected override bool ParseOption(string name, CommandLineParseState ps) return true; case "printPruned": + case "printSplit": if (ps.ConfirmArgumentCount(1)) { - PrintPrunedFile = args[ps.i]; + PrintSplitFile = args[ps.i]; + } + + return true; + case "printSplitDeclarations": + if (ps.ConfirmArgumentCount(0)) + { + PrintSplitDeclarations = true; + } + + return true; + + case "printPassive": + if (ps.ConfirmArgumentCount(1)) + { + PrintPassiveFile = args[ps.i]; } return true; diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 6fe111559..338982a0c 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -135,11 +135,6 @@ public async Task ProcessProgram(TextWriter output, Program program, strin { programId = "main_program_id"; } - - if (Options.PrintFile != null && !Options.PrintPassive) { - // Printing passive programs happens later - PrintBplFile(Options.PrintFile, program, false, true, Options.PrettyPrint); - } PipelineOutcome outcome = ResolveAndTypecheck(program, bplFileName, out var civlTypeChecker); if (outcome != PipelineOutcome.ResolvedAndTypeChecked) { @@ -240,15 +235,15 @@ public void EliminateDeadVariables(Program program) { Microsoft.Boogie.UnusedVarEliminator.Eliminate(program); } - - - public void PrintBplFile(string filename, Program program, bool allowPrintDesugaring, bool setTokens = true, - bool pretty = false) - { + + public void PrintBplFile(string filename, Program program, + bool allowPrintDesugaring, bool setTokens = true, + bool pretty = false) { PrintBplFile(Options, filename, program, allowPrintDesugaring, setTokens, pretty); } - public static void PrintBplFile(ExecutionEngineOptions options, string filename, Program program, bool allowPrintDesugaring, bool setTokens = true, + public static void PrintBplFile(ExecutionEngineOptions options, string filename, Program program, + bool allowPrintDesugaring, bool setTokens = true, bool pretty = false) { @@ -612,7 +607,7 @@ private ProcessedProgram PreProcessProgramVerification(Program program) program.Emit(new TokenTextWriter(Options.OutputWriter, Options.PrettyPrint, Options)); } - program.DeclarationDependencies = Prune.ComputeDeclarationDependencies(Options, program); + program.DeclarationDependencies = Pruner.ComputeDeclarationDependencies(Options, program); return processedProgram; }).Result; } @@ -733,11 +728,13 @@ public IReadOnlyList GetVerificationTasks(Program program) Inline(program); var processedProgram = PreProcessProgramVerification(program); + return GetPrioritizedImplementations(program).SelectMany(implementation => { var writer = TextWriter.Null; var vcGenerator = new VerificationConditionGenerator(processedProgram.Program, CheckerPool); + var run = new ImplementationRun(implementation, writer); var collector = new VerificationResultCollector(Options); vcGenerator.PrepareImplementation(run, collector, out _, @@ -745,7 +742,7 @@ public IReadOnlyList GetVerificationTasks(Program program) out var modelViewInfo); ConditionGeneration.ResetPredecessors(run.Implementation.Blocks); - var splits = ManualSplitFinder.FocusAndSplit(Options, run, gotoCmdOrigins, vcGenerator).ToList(); + var splits = ManualSplitFinder.FocusAndSplit(program, Options, run, gotoCmdOrigins, vcGenerator).ToList(); for (var index = 0; index < splits.Count; index++) { var split = splits[index]; split.SplitIndex = index; diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs index 297d7619d..d61e7cd18 100644 --- a/Source/ExecutionEngine/VerificationTask.cs +++ b/Source/ExecutionEngine/VerificationTask.cs @@ -44,7 +44,7 @@ public VerificationTask(ExecutionEngine engine, ProcessedProgram processedProgra public IVerificationTask FromSeed(int newSeed) { - var split = new ManualSplit(Split.Options, Split.Blocks, Split.GotoCmdOrigins, + var split = new ManualSplit(Split.Options, () => Split.Blocks, Split.GotoCmdOrigins, Split.parent, Split.Run, Split.Token, newSeed); split.SplitIndex = Split.SplitIndex; return new VerificationTask(engine, ProcessedProgram, split, modelViewInfo); diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index ebb80e3e4..d3be8bfe6 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -1145,15 +1145,18 @@ public ICollection ComputeReachability(Node start, bool forward = true) todo.Push(start); while (todo.Any()) { - var b = todo.Pop(); - if (visited.Contains(b)) + var current = todo.Pop(); + if (!visited.Add(current)) { continue; } - visited.Add(b); - var related = forward ? this.Successors(b) : this.Predecessors(b); - related.Where(blk => !visited.Contains(blk)).ToList().ForEach(blk => todo.Push(blk)); + var targets = forward ? this.Successors(current) : this.Predecessors(current); + foreach (var target in targets) { + if (!visited.Contains(target)) { + todo.Push(target); + } + } } return visited; } diff --git a/Source/Provers/LeanAuto/LeanAutoGenerator.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs index 511a099fa..e3a5310b4 100644 --- a/Source/Provers/LeanAuto/LeanAutoGenerator.cs +++ b/Source/Provers/LeanAuto/LeanAutoGenerator.cs @@ -50,7 +50,7 @@ public static void EmitPassiveProgramAsLean(VCGenOptions options, Program p, Tex var liveDeclarations = !options.Prune ? p.TopLevelDeclarations - : Prune.GetLiveDeclarations(options, p, allBlocks.ToList()).ToList(); + : Pruner.GetLiveDeclarations(options, p, allBlocks.ToList()).ToList(); generator.WriteLine("-- Type constructors"); // Always include all type constructors diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs index 9e9606ecf..75dba5998 100644 --- a/Source/VCGeneration/BlockTransformations.cs +++ b/Source/VCGeneration/BlockTransformations.cs @@ -1,73 +1,210 @@ +using System; +using System.Collections; using System.Collections.Generic; -using System.Diagnostics.Contracts; +using System.Collections.Immutable; using System.Linq; +using System.Reactive; using Microsoft.Boogie; +using Microsoft.Boogie.GraphUtil; +using VCGeneration.Prune; namespace VCGeneration; -public static class BlockTransformations -{ - public static List DeleteNoAssertionBlocks(List blocks) - { - - blocks.ForEach(StopControlFlowAtAssumeFalse); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously - var todo = new Stack(); - var peeked = new HashSet(); - var interestingBlocks = new HashSet(); - todo.Push(blocks[0]); - while(todo.Any()) - { - /* - * DFS traversal where each node is handled before and after its children were visited. - * Pop == true means it's after the children. - */ - var currentBlock = todo.Peek(); - var pop = peeked.Contains(currentBlock); - peeked.Add(currentBlock); - var interesting = false; - if (currentBlock.TransferCmd is GotoCmd exit) { - if (pop) - { - Contract.Assert(pop); - var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList()); - currentBlock.TransferCmd = gtc; - interesting = interesting || gtc.labelTargets.Count != 0; +public static class BlockTransformations { + public static void Optimize(List blocks, Program program) { + foreach (var block in blocks) { + // TODO somehow this had 0 effect on my customer codebase + OldBlockTransformations.StopControlFlowAtAssumeFalse(block); + } + PruneAssumptions(program, blocks); + OptimizeBlocks(blocks); + } + + public static void OptimizeBlocks(List blocks) { + DeleteUselessBlocks(blocks); + MergeOneToOneBlocks(blocks); + } + + private static void DeleteUselessBlocks(List blocks) { + var toVisit = new HashSet(); + var removed = new HashSet(); + foreach (var block in blocks) { + toVisit.Add(block); + } + while(toVisit.Count > 0) { + var block = toVisit.First(); + toVisit.Remove(block); + if (removed.Contains(block)) { + continue; + } + if (block.Cmds.Any()) { + continue; + } + + var isBranchingBlock = block.TransferCmd is GotoCmd gotoCmd1 && gotoCmd1.labelTargets.Count > 1 && + block.Predecessors.Count != 1; + if (isBranchingBlock) { + continue; + } + + removed.Add(block); + blocks.Remove(block); + + var noPredecessors = !block.Predecessors.Any(); + var noSuccessors = block.TransferCmd is not GotoCmd outGoto2 || !outGoto2.labelTargets.Any(); + foreach (var predecessor in block.Predecessors) { + var intoCmd = (GotoCmd)predecessor.TransferCmd; + intoCmd.RemoveTarget(block); + if (noSuccessors) { + toVisit.Add(predecessor); } - else - { - exit.labelTargets.ForEach(b => todo.Push(b)); + } + + if (block.TransferCmd is not GotoCmd outGoto) { + continue; + } + + foreach (var outBlock in outGoto.labelTargets) { + outBlock.Predecessors.Remove(block); + if (noPredecessors) { + toVisit.Add(outBlock); } } - if (pop) - { - interesting = interesting || ContainsAssert(currentBlock); - if (interesting) { - interestingBlocks.Add(currentBlock); + + foreach (var predecessor in block.Predecessors) { + var intoCmd = (GotoCmd)predecessor.TransferCmd; + foreach (var outBlock in outGoto.labelTargets) { + if (!intoCmd.labelTargets.Contains(outBlock)) { + intoCmd.AddTarget(outBlock); + outBlock.Predecessors.Add(predecessor); + } } - todo.Pop(); } } - interestingBlocks.Add(blocks[0]); // must not be empty - return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders. } - private static bool ContainsAssert(Block b) - { - bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); } - return b.Cmds.Exists(IsNonTrivialAssert); + private static void MergeOneToOneBlocks(List blocks) { + var stack = new Stack(); + foreach (var block in blocks) { + if (!block.Predecessors.Any()) { + stack.Push(block); + } + } + while (stack.Any()) { + var current = stack.Pop(); + if (current.TransferCmd is not GotoCmd gotoCmd) { + continue; + } + + if (gotoCmd.labelTargets.Count != 1) { + foreach (var aNext in gotoCmd.labelTargets) { + stack.Push(aNext); + } + continue; + } + + var next = gotoCmd.labelTargets.Single(); + if (next.Predecessors.Count != 1) { + stack.Push(next); + continue; + } + + blocks.Remove(next); + current.Cmds.AddRange(next.Cmds); + current.TransferCmd = next.TransferCmd; + foreach (var nextTarget in current.Exits()) { + nextTarget.Predecessors.Remove(next); + nextTarget.Predecessors.Add(current); + } + stack.Push(current); + } } - private static void StopControlFlowAtAssumeFalse(Block b) - { - var firstFalseIdx = b.Cmds.FindIndex(IsAssumeFalse); - if (firstFalseIdx == -1) - { - return; + public static void PruneAssumptions(Program program, List blocks) { + Dictionary> commandVariables = new(); + + var gatekeepers = program.Variables. + Where(g => g.Name.Contains("Height") || g.Name.StartsWith("reveal__")).ToList(); + + var controlFlowGraph = Pruner.GetControlFlowGraph(blocks); + var asserts = controlFlowGraph.Nodes.OfType().ToList(); + var assumesToKeep = new HashSet(); + foreach (var assert in asserts) { + var proofByContradiction = assert.Expr.Equals(Expr.False) + || assert.Expr.ToString() == "Lit(false)"; // TODO use annotation placed by Dafny + var reachableAssumes = controlFlowGraph.ComputeReachability(assert, false).OfType().ToHashSet(); + if (proofByContradiction) { + foreach (var assume in reachableAssumes) { + assumesToKeep.Add(assume); + } + + continue; + } + + var dependencyGraph = new Graph(); + foreach (var cmd in reachableAssumes.Append(assert)) { + var variables = GetVariables(cmd); + var groups = variables.GroupBy(v => v is Constant + || v is GlobalVariable + || v is Incarnation { OriginalVariable: Constant or GlobalVariable }).ToList(); + + var locals = groups.FirstOrDefault(g => !g.Key) ?? Enumerable.Empty(); + var globalsForCommand = groups.FirstOrDefault(g => g.Key); + var localsKnot = new object(); + foreach (var local in locals) { + dependencyGraph.AddEdge(local, localsKnot); + dependencyGraph.AddEdge(localsKnot, local); + } + + if (globalsForCommand != null) { + var globalsKnot = new object(); + foreach (var global in globalsForCommand) { + dependencyGraph.AddEdge(global, globalsKnot); + dependencyGraph.AddEdge(globalsKnot, global); + } + dependencyGraph.AddEdge(localsKnot, globalsKnot); + } + } + + var controlFlowAssumes = new List(); + // var controlFlowAssumes = + // reachableAssumes.Where(cmd => QKeyValue.FindBoolAttribute(cmd.Attributes, "partition")). + // SelectMany(GetVariables).ToList(); + HashSet dependentVariables = new(); + + foreach (var root in controlFlowAssumes.Concat(gatekeepers).Concat(GetVariables(assert))) { + if (!dependencyGraph.Nodes.Contains(root)) { + continue; + } + foreach (var reachable in dependencyGraph.ComputeReachability(root)) { + if (reachable is Variable variable) { + dependentVariables.Add(variable); + } + } + } + + foreach(var assumeCmd in reachableAssumes) { + if (assumeCmd.Expr.Equals(Expr.False) // TODO take into account Lit, use annotation placed by Dafny + || GetVariables(assumeCmd).Overlaps(dependentVariables)) { + assumesToKeep.Add(assumeCmd); // Explicit assume false should be kept. // TODO take into account Lit ?? + } else { + var c = 3; + } + } + } + + foreach (var block in blocks) { + block.Cmds = block.Cmds.Where(cmd => cmd is not AssumeCmd assumeCmd || assumesToKeep.Contains(assumeCmd)).ToList(); } - b.Cmds = b.Cmds.Take(firstFalseIdx + 1).ToList(); - b.TransferCmd = b.TransferCmd is GotoCmd ? new ReturnCmd(b.tok) : b.TransferCmd; + return; + + ISet GetVariables(PredicateCmd cmd) { + return commandVariables.GetOrCreate(cmd, () => { + var set = new GSet(); + cmd.Expr.ComputeFreeVariables(set); + return set.OfType().ToHashSet(); + }); + } } - - private static bool IsAssumeFalse (Cmd c) { return c is AssumeCmd { Expr: LiteralExpr { asBool: false } }; } } \ No newline at end of file diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs index 8c993f068..49f23b1df 100644 --- a/Source/VCGeneration/Checker.cs +++ b/Source/VCGeneration/Checker.cs @@ -163,7 +163,7 @@ private void Setup(Program program, ProverContext ctx, Split split) // TODO(wuestholz): Is this lock necessary? lock (Program.TopLevelDeclarations) { - var declarations = split.TopLevelDeclarations; + var declarations = split.PrunedDeclarations; var reorderedDeclarations = GetReorderedDeclarations(declarations, SolverOptions.RandomSeed); foreach (var declaration in reorderedDeclarations) { Contract.Assert(declaration != null); diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index d1528d907..f0f481b8e 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -223,10 +223,9 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu Block origStartBlock = impl.Blocks[0]; Block insertionPoint = new Block( new Token(-17, -4), blockLabel, startCmds, - new GotoCmd(Token.NoToken, new List {origStartBlock.Label}, new List {origStartBlock})); + new GotoCmd(impl.tok, new List {origStartBlock.Label}, new List {origStartBlock})); - impl.Blocks[0] = insertionPoint; // make insertionPoint the start block - impl.Blocks.Add(origStartBlock); // and put the previous start block at the end of the list + impl.Blocks.Insert(0, insertionPoint); // make insertionPoint the start block // (free and checked) requires clauses foreach (Requires req in impl.Proc.Requires) @@ -506,17 +505,17 @@ public virtual void Close() } - public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool printDesugarings) + public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool printDesugarings, IEnumerable overrideBlocks = null) { var impl = run.Implementation; + overrideBlocks ??= impl.Blocks; + Contract.Requires(impl != null); - int oldPrintUnstructured = options.PrintUnstructured; - options.PrintUnstructured = 2; // print only the unstructured program bool oldPrintDesugaringSetting = options.PrintDesugarings; options.PrintDesugarings = printDesugarings; - impl.Emit(new TokenTextWriter("", run.OutputWriter, /*setTokens=*/ false, /*pretty=*/ false, options), 0); + var writer = new TokenTextWriter("", run.OutputWriter, /*setTokens=*/ false, /*pretty=*/ false, options); + impl.EmitImplementation(writer, 0, overrideBlocks, true); options.PrintDesugarings = oldPrintDesugaringSetting; - options.PrintUnstructured = oldPrintUnstructured; } @@ -546,20 +545,19 @@ protected Block GenerateUnifiedExit(Implementation impl, Dictionary 1) { string unifiedExitLabel = "GeneratedUnifiedExit"; - Block unifiedExit; - unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), + 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) + if (b.TransferCmd is ReturnCmd returnCmd) { List labels = new List(); labels.Add(unifiedExitLabel); List bs = new List(); bs.Add(unifiedExit); - GotoCmd go = new GotoCmd(Token.NoToken, labels, bs); - gotoCmdOrigins[go] = (ReturnCmd) b.TransferCmd; + GotoCmd go = new GotoCmd(returnCmd.tok, labels, bs); + gotoCmdOrigins[go] = returnCmd; b.TransferCmd = go; unifiedExit.Predecessors.Add(b); } diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs index ebaeedf60..6aa00a93a 100644 --- a/Source/VCGeneration/FocusAttribute.cs +++ b/Source/VCGeneration/FocusAttribute.cs @@ -28,7 +28,7 @@ public static List FocusImpl(VCGenOptions options, ImplementationRu focusBlocks.Reverse(); } if (!focusBlocks.Any()) { - return new List { new(options, impl.Blocks, gotoCmdOrigins, par, run, run.Implementation.tok) }; + return new List { new(options, () => impl.Blocks, gotoCmdOrigins, par, run, run.Implementation.tok) }; } var ancestorsPerBlock = new Dictionary>(); @@ -71,7 +71,7 @@ void FocusRec(IToken focusToken, int focusIndex, IReadOnlyList blocksToIn } newBlocks.Reverse(); Contract.Assert(newBlocks[0] == oldToNewBlockMap[impl.Blocks[0]]); - result.Add(new ManualSplit(options, BlockTransformations.DeleteNoAssertionBlocks(newBlocks), gotoCmdOrigins, par, run, focusToken)); + result.Add(new ManualSplit(options, () => OldBlockTransformations.DeleteNoAssertionBlocks(newBlocks), gotoCmdOrigins, par, run, focusToken)); } else if (!blocksToInclude.Contains(focusBlocks[focusIndex].Block) || freeAssumeBlocks.Contains(focusBlocks[focusIndex].Block)) { diff --git a/Source/VCGeneration/ManualSplit.cs b/Source/VCGeneration/ManualSplit.cs index e46d722f8..867594717 100644 --- a/Source/VCGeneration/ManualSplit.cs +++ b/Source/VCGeneration/ManualSplit.cs @@ -1,3 +1,4 @@ +using System; using System.Collections.Generic; using Microsoft.Boogie; @@ -10,7 +11,7 @@ public class ManualSplit : Split public ManualSplit(VCGenOptions options, - List blocks, + Func> blocks, Dictionary gotoCmdOrigins, VerificationConditionGenerator par, ImplementationRun run, diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs index 9d1804742..6a5261458 100644 --- a/Source/VCGeneration/ManualSplitFinder.cs +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -1,23 +1,28 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using System.Threading.Tasks.Dataflow; using Microsoft.Boogie; using VC; namespace VCGeneration; public static class ManualSplitFinder { - public static IEnumerable FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par) { + public static IEnumerable FocusAndSplit(Program program, VCGenOptions options, ImplementationRun run, + Dictionary gotoCmdOrigins, VerificationConditionGenerator par) { var focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par); - return focussedImpl.SelectMany(FindManualSplits); + return focussedImpl.SelectMany(s => FindManualSplits(program, s)); } - private static List FindManualSplits(ManualSplit initialSplit) { + private static List FindManualSplits(Program program, ManualSplit initialSplit) { Contract.Requires(initialSplit.Implementation != null); Contract.Ensures(Contract.Result>() == null || cce.NonNullElements(Contract.Result>())); var splitOnEveryAssert = initialSplit.Options.VcsSplitOnEveryAssert; initialSplit.Run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); + if (splitOnEveryAssert) { + return SplitEachAssert(program, initialSplit); + } var splitPoints = new Dictionary>(); foreach (var block in initialSplit.Blocks) { @@ -34,10 +39,12 @@ public static IEnumerable FocusAndSplit(VCGenOptions options, Imple Block entryPoint = initialSplit.Blocks[0]; var blockAssignments = PickBlocksToVerify(initialSplit.Blocks, splitPoints); var entryBlockHasSplit = splitPoints.ContainsKey(entryPoint); - var baseSplitBlocks = BlockTransformations.DeleteNoAssertionBlocks( - DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, - -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert)); - splits.Add(new ManualSplit(initialSplit.Options, baseSplitBlocks, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, initialSplit.Token)); + var firstSplitBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, + -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert); + splits.Add(new ManualSplit(initialSplit.Options, () => { + BlockTransformations.Optimize(firstSplitBlocks, program); + return firstSplitBlocks; + }, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, initialSplit.Token)); foreach (var block in initialSplit.Blocks) { var tokens = splitPoints.GetValueOrDefault(block); if (tokens == null) { @@ -49,13 +56,35 @@ public static IEnumerable FocusAndSplit(VCGenOptions options, Imple bool lastSplitInBlock = i == tokens.Count - 1; var newBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, i, block, lastSplitInBlock, splitOnEveryAssert); splits.Add(new ManualSplit(initialSplit.Options, - BlockTransformations.DeleteNoAssertionBlocks(newBlocks), initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, token)); + () => { + BlockTransformations.Optimize(newBlocks, program); + return newBlocks; + }, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, token)); } } } return splits; } + private static List SplitEachAssert(Program program, ManualSplit initialSplit) + { + var result = new List(); + foreach (var block in initialSplit.Blocks) { + foreach (Cmd command in block.Cmds) { + if (command is AssertCmd assertCmd) { + var newBlocks = SplitOnAssert(initialSplit.Options, initialSplit.Blocks, assertCmd); + result.Add(new ManualSplit(initialSplit.Options, + () => { + BlockTransformations.Optimize(newBlocks, program); + return newBlocks; + }, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, assertCmd.tok)); + } + } + } + + return result; + } + private static bool ShouldSplitHere(Cmd c, bool splitOnEveryAssert) { return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "split_here") || c is AssertCmd && splitOnEveryAssert; @@ -90,7 +119,26 @@ private static Dictionary PickBlocksToVerify(List blocks, D return blockAssignments; } - private static List DoPreAssignedManualSplit(VCGenOptions options, List blocks, Dictionary blockAssignments, int splitNumberWithinBlock, + private static List SplitOnAssert(VCGenOptions options, List oldBlocks, AssertCmd assertToKeep) { + var oldToNewBlockMap = new Dictionary(oldBlocks.Count); + + var newBlocks = new List(oldBlocks.Count); + foreach (var oldBlock in oldBlocks) { + var newBlock = new Block { + Label = oldBlock.Label, + tok = oldBlock.tok, + Cmds = oldBlock.Cmds.Select(cmd => + cmd != assertToKeep ? CommandTransformations.AssertIntoAssume(options, cmd) : cmd).ToList() + }; + oldToNewBlockMap[oldBlock] = newBlock; + newBlocks.Add(newBlock); + } + + AddBlockJumps(oldBlocks, oldToNewBlockMap); + return newBlocks; + } + private static List DoPreAssignedManualSplit(VCGenOptions options, List blocks, + Dictionary blockAssignments, int splitNumberWithinBlock, Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert) { var newBlocks = new List(blocks.Count); // Copies of the original blocks //var duplicator = new Duplicator(); @@ -127,8 +175,16 @@ private static List DoPreAssignedManualSplit(VCGenOptions options, List oldBlocks, Dictionary oldToNewBlockMap) + { + foreach (var oldBlock in oldBlocks) { + var newBlock = oldToNewBlockMap[oldBlock]; + if (oldBlock.TransferCmd is ReturnCmd returnCmd) { + ((ReturnCmd)newBlock.TransferCmd).tok = returnCmd.tok; continue; } @@ -142,6 +198,5 @@ private static List DoPreAssignedManualSplit(VCGenOptions options, List DeleteNoAssertionBlocks(List blocks) + { + blocks.ForEach(StopControlFlowAtAssumeFalse); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously + var todo = new Stack(); + var peeked = new HashSet(); + var interestingBlocks = new HashSet(); + todo.Push(blocks[0]); + while(todo.Any()) + { + /* + * DFS traversal where each node is handled before and after its children were visited. + * Pop == true means it's after the children. + */ + var currentBlock = todo.Peek(); + var pop = peeked.Contains(currentBlock); + peeked.Add(currentBlock); + var interesting = false; + if (currentBlock.TransferCmd is GotoCmd exit) { + if (pop) + { + Contract.Assert(pop); + var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList()); + currentBlock.TransferCmd = gtc; + interesting = interesting || gtc.labelTargets.Count != 0; + } + else + { + exit.labelTargets.ForEach(b => todo.Push(b)); + } + } + if (pop) + { + interesting = interesting || ContainsAssert(currentBlock); + if (interesting) { + interestingBlocks.Add(currentBlock); + } + todo.Pop(); + } + } + interestingBlocks.Add(blocks[0]); // must not be empty + return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders. + } + + private static bool ContainsAssert(Block b) + { + bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); } + return b.Cmds.Exists(IsNonTrivialAssert); + } + + public static void StopControlFlowAtAssumeFalse(Block block) + { + var firstFalseIdx = block.Cmds.FindIndex(IsAssumeFalse); + if (firstFalseIdx == -1) + { + return; + } + + block.Cmds = block.Cmds.Take(firstFalseIdx + 1).ToList(); + if (block.TransferCmd is GotoCmd gotoCmd) { + block.TransferCmd = new ReturnCmd(block.tok); + foreach (var target in gotoCmd.labelTargets) { + target.Predecessors.Remove(block); + } + } + } + + private static bool IsAssumeFalse (Cmd c) { return c is AssumeCmd { Expr: LiteralExpr { asBool: false } }; } +} \ No newline at end of file diff --git a/Source/VCGeneration/Prune/DataflowAnalysis.cs b/Source/VCGeneration/Prune/DataflowAnalysis.cs index 071d0ffec..3a1896f1a 100644 --- a/Source/VCGeneration/Prune/DataflowAnalysis.cs +++ b/Source/VCGeneration/Prune/DataflowAnalysis.cs @@ -42,8 +42,7 @@ public void Run() { var previous = getPrevious(node); var previousStates = previous.Select(p => outStates.GetValueOrDefault(p)).Where(x => x != null).ToList(); var inState = previousStates.Any() ? previousStates.Aggregate(Merge) : Empty; - var previousInState = inStates.GetValueOrDefault(node); - if (previousInState != null && StateEquals(inState, previousInState)) { + if (inStates.ContainsKey(node) && StateEquals(inState, inStates[node])) { continue; } diff --git a/Source/VCGeneration/Prune/Prune.cs b/Source/VCGeneration/Prune/Pruner.cs similarity index 88% rename from Source/VCGeneration/Prune/Prune.cs rename to Source/VCGeneration/Prune/Pruner.cs index 455d2878a..969054063 100644 --- a/Source/VCGeneration/Prune/Prune.cs +++ b/Source/VCGeneration/Prune/Pruner.cs @@ -8,7 +8,7 @@ namespace Microsoft.Boogie { - public class Prune { + public class Pruner { public static Dictionary>? ComputeDeclarationDependencies(VCGenOptions options, Program program) { @@ -98,7 +98,7 @@ private static RevealedState GetRevealedState(List blocks) Aggregate(RevealedState.AllHidden, RevealedAnalysis.MergeStates); } - private static Graph GetControlFlowGraph(List blocks) + public static Graph GetControlFlowGraph(List blocks) { /* * Generally the blocks created by splitting have unset block.Predecessors fields @@ -110,22 +110,17 @@ private static Graph GetControlFlowGraph(List blocks) block.Predecessors.Clear(); } Implementation.ComputePredecessorsForBlocks(blocks); - var graph = new Graph(); + var graph = new Graph(); foreach (var block in blocks) { + var commands = block.Cmds.Append(block.TransferCmd).ToList(); foreach (var predecessor in block.Predecessors) { - var last = predecessor.Cmds.LastOrDefault(); - if (last != null) { - graph.AddEdge(last, block.Cmds[0]); - } else { - if (predecessor.Predecessors.Any()) { - throw new Exception(); - } - } + var previous = predecessor.TransferCmd; + graph.AddEdge(previous, commands.First()); } - for (var index = 0; index < block.Cmds.Count - 1; index++) { - var command = block.Cmds[index]; - var nextCommand = block.Cmds[index + 1]; + for (var index = 0; index < commands.Count - 1; index++) { + var command = commands[index]; + var nextCommand = commands[index + 1]; graph.AddEdge(command, nextCommand); } } diff --git a/Source/VCGeneration/Prune/RevealedAnalysis.cs b/Source/VCGeneration/Prune/RevealedAnalysis.cs index b146ce22b..59adfe6a0 100644 --- a/Source/VCGeneration/Prune/RevealedAnalysis.cs +++ b/Source/VCGeneration/Prune/RevealedAnalysis.cs @@ -16,11 +16,11 @@ public bool IsRevealed(Function function) { public static readonly RevealedState AllHidden = new(HideRevealCmd.Modes.Hide, ImmutableHashSet.Empty); } -class RevealedAnalysis : DataflowAnalysis> { +class RevealedAnalysis : DataflowAnalysis> { - public RevealedAnalysis(IReadOnlyList roots, - Func> getNext, - Func> getPrevious) : base(roots, getNext, getPrevious) + public RevealedAnalysis(IReadOnlyList roots, + Func> getNext, + Func> getPrevious) : base(roots, getNext, getPrevious) { } @@ -80,7 +80,7 @@ static RevealedState GetUpdatedState(HideRevealCmd hideRevealCmd, RevealedState return state with { Offset = newOffset }; } - protected override ImmutableStack Update(Cmd node, ImmutableStack state) { + protected override ImmutableStack Update(Absy node, ImmutableStack state) { if (state.IsEmpty) { throw new Exception("Unbalanced use of push and pop commands"); } diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 4cd19abc5..50f6242cc 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1,5 +1,6 @@ using System; using System.Collections.Generic; +using System.ComponentModel; using System.Diagnostics; using System.Linq; using System.Threading; @@ -10,6 +11,7 @@ using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.SMTLib; using System.Threading.Tasks; +using VCGeneration; namespace VC { @@ -19,12 +21,33 @@ public class Split : ProofRun private readonly Random randomGen; public ImplementationRun Run { get; } - public int RandomSeed { get; private set; } + public int RandomSeed { get; } - public List Blocks { get; } + private List blocks; + public List Blocks { + get + { + lock (this) { + blocks ??= getBlocks(); + } + + return blocks; + } + } readonly List bigBlocks = new(); public List Asserts => Blocks.SelectMany(block => block.cmds.OfType()).ToList(); public readonly IReadOnlyList TopLevelDeclarations; + public IReadOnlyList prunedDeclarations; + + public IReadOnlyList PrunedDeclarations { + get { + if (prunedDeclarations == null) { + prunedDeclarations = Pruner.GetLiveDeclarations(parent.Options, parent.program, Blocks).ToList(); + } + + return prunedDeclarations; + } + } readonly Dictionary /*!*/ stats = new Dictionary(); @@ -50,31 +73,26 @@ public readonly VerificationConditionGenerator /*!*/ public Implementation /*!*/ Implementation => Run.Implementation; - Dictionary /*!*/ - copies = new Dictionary(); + Dictionary /*!*/ copies = new(); bool doingSlice; double sliceInitialLimit; double sliceLimit; bool slicePos; - - HashSet /*!*/ protectedFromAssertToAssume = new HashSet(); - - HashSet /*!*/ keepAtAll = new HashSet(); + HashSet /*!*/ protectedFromAssertToAssume = new(); + HashSet /*!*/ keepAtAll = new(); // async interface public int SplitIndex { get; set; } public VerificationConditionGenerator.ErrorReporter reporter; - private static int debugCounter; - public Split(VCGenOptions options, List /*!*/ blocks, + public Split(VCGenOptions options, Func> /*!*/ getBlocks, Dictionary /*!*/ gotoCmdOrigins, VerificationConditionGenerator /*!*/ par, ImplementationRun run, int? randomSeed = null) { - Contract.Requires(cce.NonNullElements(blocks)); Contract.Requires(gotoCmdOrigins != null); Contract.Requires(par != null); - this.Blocks = blocks; + this.getBlocks = getBlocks; this.GotoCmdOrigins = gotoCmdOrigins; parent = par; this.Run = run; @@ -82,32 +100,38 @@ public Split(VCGenOptions options, List /*!*/ blocks, Interlocked.Increment(ref currentId); TopLevelDeclarations = par.program.TopLevelDeclarations; - var counter = debugCounter++; - PrintTopLevelDeclarationsForPruning(par.program, Implementation, "before#" + counter); - TopLevelDeclarations = Prune.GetLiveDeclarations(options, par.program, blocks).ToList(); - PrintTopLevelDeclarationsForPruning(par.program, Implementation, "after#" + counter); RandomSeed = randomSeed ?? Implementation.RandomSeed ?? Options.RandomSeed ?? 0; randomGen = new Random(RandomSeed); } + + - private void PrintTopLevelDeclarationsForPruning(Program program, Implementation implementation, string suffix) - { - if (!Options.Prune || Options.PrintPrunedFile == null) - { + public void PrintSplit() { + if (Options.PrintSplitFile == null) { return; } using var writer = new TokenTextWriter( - $"{Options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}.bpl", false, + $"{Options.PrintSplitFile}-{Util.EscapeFilename(Implementation.Name)}-{SplitIndex}.spl", false, Options.PrettyPrint, Options); + Implementation.EmitImplementation(writer, 0, Blocks, false); + PrintSplitDeclarations(writer); + } + + private void PrintSplitDeclarations(TokenTextWriter writer) + { + if (!Options.Prune || !Options.PrintSplitDeclarations) + { + return; + } + var functionAxioms = - program.Functions.Where(f => f.DefinitionAxioms.Any()).SelectMany(f => f.DefinitionAxioms); + PrunedDeclarations.OfType().Where(f => f.DefinitionAxioms.Any()).SelectMany(f => f.DefinitionAxioms); var constantAxioms = - program.Constants.Where(f => f.DefinitionAxioms.Any()).SelectMany(c => c.DefinitionAxioms); + PrunedDeclarations.OfType().Where(f => f.DefinitionAxioms.Any()).SelectMany(c => c.DefinitionAxioms); - foreach (var declaration in (TopLevelDeclarations ?? program.TopLevelDeclarations) - .Except(functionAxioms.Concat(constantAxioms)).ToList()) + foreach (var declaration in PrunedDeclarations.Except(functionAxioms.Concat(constantAxioms)).ToList()) { declaration.Emit(writer, 0); } @@ -178,21 +202,13 @@ public void DumpDot(int splitNum) string filename = string.Format("{0}.split.{1}.bpl", Implementation.Name, splitNum); using (StreamWriter sw = File.CreateText(filename)) { - int oldPrintUnstructured = Options.PrintUnstructured; - Options.PrintUnstructured = 2; // print only the unstructured program - bool oldPrintDesugaringSetting = Options.PrintDesugarings; - Options.PrintDesugarings = false; - List backup = Implementation.Blocks; - Contract.Assert(backup != null); - Implementation.Blocks = Blocks; - Implementation.Emit(new TokenTextWriter(filename, sw, /*setTokens=*/ false, /*pretty=*/ false, Options), 0); - Implementation.Blocks = backup; - Options.PrintDesugarings = oldPrintDesugaringSetting; - Options.PrintUnstructured = oldPrintUnstructured; + var writer = new TokenTextWriter(filename, sw, /*setTokens=*/ false, /*pretty=*/ false, Options); + Implementation.EmitImplementation(writer, 0, Blocks, false); } } int bsid; + private readonly Func> getBlocks; BlockStats GetBlockStats(Block b) { @@ -679,7 +695,7 @@ private Split DoSplit() } } - return new Split(Options, newBlocks, newGotoCmdOrigins, parent, Run); + return new Split(Options, () => newBlocks, newGotoCmdOrigins, parent, Run); } private Split SplitAt(int idx) @@ -715,11 +731,7 @@ private Split SliceAsserts(double limit, bool pos) void Print() { - List tmp = Implementation.Blocks; - Contract.Assert(tmp != null); - Implementation.Blocks = Blocks; - ConditionGeneration.EmitImpl(Options, Run, false); - Implementation.Blocks = tmp; + ConditionGeneration.EmitImpl(Options, Run, false, Blocks); } public Counterexample ToCounterexample(ProverContext context) @@ -923,6 +935,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa ModelViewInfo mvInfo, uint timeout, uint rlimit, CancellationToken cancellationToken) { + PrintSplit(); Contract.Requires(checker != null); Contract.Requires(callback != null); diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index 63b763de0..7926edaa0 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -35,6 +35,7 @@ public class SplitAndVerifyWorker private int totalResourceCount; public SplitAndVerifyWorker( + Program program, VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, ImplementationRun run, @@ -64,7 +65,7 @@ public SplitAndVerifyWorker( ResetPredecessors(Implementation.Blocks); - ManualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator).ToList(); + ManualSplits = ManualSplitFinder.FocusAndSplit(program, options, run, gotoCmdOrigins, verificationConditionGenerator).ToList(); if (ManualSplits.Count == 1 && maxSplits > 1) { diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index f2e57c3b8..d9f14c4c7 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -407,7 +407,7 @@ public override async Task VerifyImplementation(ImplementationRun run } } - var worker = new SplitAndVerifyWorker(Options, this, run, dataGotoCmdOrigins, callback, + var worker = new SplitAndVerifyWorker(program, Options, this, run, dataGotoCmdOrigins, callback, dataModelViewInfo, vcOutcome); vcOutcome = await worker.WorkUntilDone(cancellationToken); @@ -450,6 +450,17 @@ public void PrepareImplementation(ImplementationRun run, VerifierCallback callba data.ModelViewInfo = modelViewInfo; ExpandAsserts(run.Implementation); + + if (Options.PrintPassiveFile != null) { + lock (Options) { + var prev = Options.PrintUnstructured; + Options.PrintUnstructured = 2; + using var writer = new TokenTextWriter(Options.PrintPassiveFile, false, false, Options); + writer.WriteLine(); + program.Emit(writer); + Options.PrintUnstructured = prev; + } + } } else { diff --git a/Test/pruning/MonomorphicSplit.bpl b/Test/pruning/MonomorphicSplit.bpl index 6ce0fc954..a1f247dc5 100644 --- a/Test/pruning/MonomorphicSplit.bpl +++ b/Test/pruning/MonomorphicSplit.bpl @@ -1,5 +1,5 @@ -// RUN: %parallel-boogie /prune:1 /errorTrace:0 /printPruned:"%t" "%s" > "%t" -// RUN: %OutputCheck "%s" --file-to-check="%t-after#0-monomorphicSplit.bpl" +// RUN: %parallel-boogie /prune:1 /errorTrace:0 /printSplitDeclarations /printSplit:"%t" "%s" > "%t" +// RUN: %OutputCheck "%s" --file-to-check="%t-monomorphicSplit--1.spl" // The following checks are a bit simplistic, but this is // on purpose to reduce brittleness. We assume there would now be two uses clauses