From 9c8243d39c4fc029d830dbdc4e7d6c4d7f08e3f5 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 28 Feb 2014 18:35:56 -0800 Subject: Changed all lambda-expression rewriting to be done as a pre-processing step before real verification. Fixed treatment of lambda-expression attributes. --- Source/Core/AbsyCmd.cs | 14 +++ Source/Core/AbsyQuant.cs | 39 +++++--- Source/Core/Duplicator.cs | 129 ++++++++++++++++++-------- Source/Core/LambdaHelper.cs | 147 +++++++++++++++++++----------- Source/Core/StandardVisitor.cs | 36 +++++++- Source/ExecutionEngine/ExecutionEngine.cs | 19 ++-- Source/VCGeneration/VC.cs | 26 ------ 7 files changed, 264 insertions(+), 146 deletions(-) (limited to 'Source') diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index b84770e3..c7a813d3 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1631,6 +1631,20 @@ namespace Microsoft.Boogie { return desugaring; } } + /// + /// This method invokes "visitor.Visit" on the desugaring, and then updates the + /// desugaring to the result thereof. The method's intended use is for subclasses + /// of StandardVisitor that need to also visit the desugaring. Note, since the + /// "desugaring" field is updated, this is not an appropriate method to be called + /// be a ReadOnlyVisitor; such visitors should instead just call + /// visitor.Visit(sugaredCmd.Desugaring). + /// + public void VisitDesugaring(StandardVisitor visitor) { + Contract.Requires(visitor != null && !(visitor is ReadOnlyVisitor)); + if (desugaring != null) { + desugaring = (Cmd)visitor.Visit(desugaring); + } + } protected abstract Cmd/*!*/ ComputeDesugaring(); public override void Emit(TokenTextWriter stream, int level) { diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 45e69eed..63474c69 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -167,28 +167,33 @@ namespace Microsoft.Boogie { } } - public override void ComputeFreeVariables(Set /*Variable*/ freeVars) { + public override void ComputeFreeVariables(Set freeVars) { //Contract.Requires(freeVars != null); - foreach (Variable/*!*/ v in Dummies) { + ComputeBinderFreeVariables(TypeParameters, Dummies, Body, Attributes, freeVars); + } + + public static void ComputeBinderFreeVariables(List typeParameters, List dummies, Expr body, QKeyValue attributes, Set freeVars) { + Contract.Requires(dummies != null); + Contract.Requires(body != null); + + foreach (var v in dummies) { Contract.Assert(v != null); Contract.Assert(!freeVars[v]); } - Body.ComputeFreeVariables(freeVars); - foreach (Variable/*!*/ v in Dummies) { - Contract.Assert(v != null); - foreach (TypeVariable/*!*/ w in v.TypedIdent.Type.FreeVariables) { - Contract.Assert(w != null); - freeVars.Add(w); + body.ComputeFreeVariables(freeVars); + for (var a = attributes; a != null; a = a.Next) { + foreach (var o in a.Params) { + var e = o as Expr; + if (e != null) { + e.ComputeFreeVariables(freeVars); + } } } - foreach (Variable/*!*/ v in Dummies) { - Contract.Assert(v != null); - freeVars.Remove(v); - } - foreach (TypeVariable/*!*/ v in TypeParameters) { - Contract.Assert(v != null); - freeVars.Remove(v); + foreach (var v in dummies) { + freeVars.AddRange(v.TypedIdent.Type.FreeVariables); } + freeVars.RemoveRange(dummies); + freeVars.RemoveRange(typeParameters); } protected List GetUnmentionedTypeParameters() { @@ -353,6 +358,10 @@ namespace Microsoft.Boogie { newParams.Add(o); return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue)Next.Clone()); } + + public override Absy StdDispatch(StandardVisitor visitor) { + return visitor.VisitQKeyValue(this); + } } public class Trigger : Absy { diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 650bb146..cd084e14 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -266,14 +266,13 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return base.VisitOldExpr((OldExpr)node.Clone()); } - public override Cmd VisitParCallCmd(ParCallCmd node) - { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - ParCallCmd clone = (ParCallCmd)node.Clone(); - Contract.Assert(clone != null); - clone.CallCmds = new List(node.CallCmds); - return base.VisitParCallCmd(clone); + public override Cmd VisitParCallCmd(ParCallCmd node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + ParCallCmd clone = (ParCallCmd)node.Clone(); + Contract.Assert(clone != null); + clone.CallCmds = new List(node.CallCmds); + return base.VisitParCallCmd(clone); } public override Procedure VisitProcedure(Procedure node) { //Contract.Requires(node != null); @@ -285,6 +284,20 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return base.VisitProgram((Program)node.Clone()); } + public override QKeyValue VisitQKeyValue(QKeyValue node) { + //Contract.Requires(node != null); + var newParams = new List(); + foreach (var o in node.Params) { + var e = o as Expr; + if (e == null) { + newParams.Add(o); + } else { + newParams.Add((Expr)this.Visit(e)); + } + } + QKeyValue next = node.Next == null ? null : (QKeyValue)this.Visit(node.Next); + return new QKeyValue(node.tok, node.Key, newParams, next); + } public override BinderExpr VisitBinderExpr(BinderExpr node) { //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); @@ -411,14 +424,16 @@ namespace Microsoft.Boogie { } } + // ----------------------------- Substitutions for Expr ------------------------------- + /// /// Apply a substitution to an expression. Any variables not in domain(subst) - /// is not changed. The substitutions applies within the "old", but the "old" + /// is not changed. The substitutions apply within the "old", but the "old" /// expression remains. /// public static Expr Apply(Substitution subst, Expr expr) { - Contract.Requires(expr != null); Contract.Requires(subst != null); + Contract.Requires(expr != null); Contract.Ensures(Contract.Result() != null); return (Expr)new NormalSubstituter(subst).Visit(expr); } @@ -430,23 +445,39 @@ namespace Microsoft.Boogie { /// variables in domain(forOld), apply map "always" to variables in /// domain(always)-domain(forOld), and leave variable unchanged otherwise. /// - public static Expr Apply(Substitution always, Substitution forold, Expr expr) - { - Contract.Requires(expr != null); - Contract.Requires(always != null); - Contract.Requires(forold != null); - Contract.Ensures(Contract.Result() != null); - return (Expr)new NormalSubstituter(always, forold).Visit(expr); + public static Expr Apply(Substitution always, Substitution forold, Expr expr) { + Contract.Requires(always != null); + Contract.Requires(forold != null); + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result() != null); + return (Expr)new NormalSubstituter(always, forold).Visit(expr); } + /// + /// Apply a substitution to an expression replacing "old" expressions. + /// Outside "old" expressions, the substitution "always" is applied; any variable not in + /// domain(always) is not changed. Inside "old" expressions, apply map "forOld" to + /// variables in domain(forOld), apply map "always" to variables in + /// domain(always)-domain(forOld), and leave variable unchanged otherwise. + /// + public static Expr ApplyReplacingOldExprs(Substitution always, Substitution forOld, Expr expr) { + Contract.Requires(always != null); + Contract.Requires(forOld != null); + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result() != null); + return (Expr)new ReplacingOldSubstituter(always, forOld).Visit(expr); + } + + // ----------------------------- Substitutions for Cmd ------------------------------- + /// /// Apply a substitution to a command. Any variables not in domain(subst) - /// is not changed. The substitutions applies within the "old", but the "old" + /// is not changed. The substitutions apply within the "old", but the "old" /// expression remains. /// public static Cmd Apply(Substitution subst, Cmd cmd) { - Contract.Requires(cmd != null); Contract.Requires(subst != null); + Contract.Requires(cmd != null); Contract.Ensures(Contract.Result() != null); return (Cmd)new NormalSubstituter(subst).Visit(cmd); } @@ -458,46 +489,64 @@ namespace Microsoft.Boogie { /// variables in domain(forOld), apply map "always" to variables in /// domain(always)-domain(forOld), and leave variable unchanged otherwise. /// - public static Cmd Apply(Substitution always, Substitution forold, Cmd cmd) + public static Cmd Apply(Substitution always, Substitution forOld, Cmd cmd) { - Contract.Requires(cmd != null); Contract.Requires(always != null); - Contract.Requires(forold != null); + Contract.Requires(forOld != null); + Contract.Requires(cmd != null); Contract.Ensures(Contract.Result() != null); - return (Cmd)new NormalSubstituter(always, forold).Visit(cmd); + return (Cmd)new NormalSubstituter(always, forOld).Visit(cmd); } /// - /// Apply a substitution to an expression replacing "old" expressions. + /// Apply a substitution to a command replacing "old" expressions. /// Outside "old" expressions, the substitution "always" is applied; any variable not in /// domain(always) is not changed. Inside "old" expressions, apply map "forOld" to /// variables in domain(forOld), apply map "always" to variables in /// domain(always)-domain(forOld), and leave variable unchanged otherwise. /// - public static Expr ApplyReplacingOldExprs(Substitution always, Substitution forold, Expr expr) { - Contract.Requires(expr != null); - Contract.Requires(forold != null); + public static Cmd ApplyReplacingOldExprs(Substitution always, Substitution forOld, Cmd cmd) { Contract.Requires(always != null); - Contract.Ensures(Contract.Result() != null); - return (Expr)new ReplacingOldSubstituter(always, forold).Visit(expr); + Contract.Requires(forOld != null); + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + return (Cmd)new ReplacingOldSubstituter(always, forOld).Visit(cmd); } + // ----------------------------- Substitutions for QKeyValue ------------------------------- + /// - /// Apply a substitution to a command replacing "old" expressions. - /// Outside "old" expressions, the substitution "always" is applied; any variable not in - /// domain(always) is not changed. Inside "old" expressions, apply map "oldExpr" to - /// variables in domain(oldExpr), apply map "always" to variables in - /// domain(always)-domain(oldExpr), and leave variable unchanged otherwise. + /// Apply a substitution to a list of attributes. Any variables not in domain(subst) + /// is not changed. The substitutions apply within the "old", but the "old" + /// expression remains. + /// + public static QKeyValue Apply(Substitution subst, QKeyValue kv) { + Contract.Requires(subst != null); + if (kv == null) { + return null; + } else { + return (QKeyValue)new NormalSubstituter(subst).Visit(kv); + } + } + + /// + /// Apply a substitution to a list of attributes replacing "old" expressions. + /// For a further description, see "ApplyReplacingOldExprs" above for Expr. /// - public static Cmd ApplyReplacingOldExprs(Substitution always, Substitution forold, Cmd cmd) { - Contract.Requires(cmd != null); - Contract.Requires(forold != null); + public static QKeyValue ApplyReplacingOldExprs(Substitution always, Substitution forOld, QKeyValue kv) { Contract.Requires(always != null); - Contract.Ensures(Contract.Result() != null); - return (Cmd)new ReplacingOldSubstituter(always, forold).Visit(cmd); + Contract.Requires(forOld != null); + if (kv == null) { + return null; + } else { + return (QKeyValue)new ReplacingOldSubstituter(always, forOld).Visit(kv); + } } - private sealed class NormalSubstituter : Duplicator { + // ------------------------------------------------------------ + + private sealed class NormalSubstituter : Duplicator + { private readonly Substitution/*!*/ always; private readonly Substitution/*!*/ forold; [ContractInvariantMethod] diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index a61c6f33..a727dc95 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -62,75 +62,82 @@ namespace Microsoft.Boogie { static int lambdaid = 0; - public override Program VisitProgram(Program prog) { - //Contract.Requires(prog != null); - Contract.Ensures(Contract.Result() != null); - foreach (Declaration/*!*/ decl in prog.TopLevelDeclarations) { - Contract.Assert(decl != null); - if (decl is Axiom || decl is Function) { - this.Visit(decl); - } - } - - return prog; - } - - public override Procedure VisitProcedure(Procedure node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - // do not visit requires/ensures when calling this on Implementation - return node; - } - public override Expr VisitLambdaExpr(LambdaExpr lambda) { var baseResult = base.VisitLambdaExpr(lambda); lambda = baseResult as LambdaExpr; if (lambda == null) { - return baseResult; + return baseResult; // apparently, the base visitor already turned the lambda into something else } - IToken/*!*/ tok = lambda.tok; - Contract.Assert(tok != null); + // We start by getting rid of any use of "old" inside the lambda. This is done as follows. + // For each variable "g" occurring inside lambda as "old(... g ...)", create a new name "og". + // Replace each old occurrence of "g" with "og", removing the enclosing "old" wrappers. + var oldFinder = new OldFinder(); + oldFinder.Visit(lambda); + var oldSubst = new Dictionary(); // g -> g0 + var callOldMapping = new Dictionary(); // g0 -> old(g) + foreach (var v in oldFinder.FreeOldVars) { + var g = v as GlobalVariable; + if (g != null) { + var g0 = new GlobalVariable(g.tok, new TypedIdent(g.tok, g.TypedIdent.Name + "@old", g.TypedIdent.Type)); + oldSubst.Add(g, new IdentifierExpr(g0.tok, g0)); + callOldMapping.Add(g0, new OldExpr(g0.tok, new IdentifierExpr(g.tok, g))); + } + } + var lambdaBody = Substituter.ApplyReplacingOldExprs( + Substituter.SubstitutionFromHashtable(new Dictionary()), + Substituter.SubstitutionFromHashtable(oldSubst), + lambda.Body); + var lambdaAttrs = Substituter.ApplyReplacingOldExprs( + Substituter.SubstitutionFromHashtable(new Dictionary()), + Substituter.SubstitutionFromHashtable(oldSubst), + lambda.Attributes); - Set freeVars = new Set(); - lambda.ComputeFreeVariables(freeVars); // this is ugly, the output will depend on hashing order - Dictionary subst = new Dictionary(); - List formals = new List(); - List callArgs = new List(); - List axCallArgs = new List(); - List dummies = new List(lambda.Dummies); - List freeTypeVars = new List(); - List fnTypeVarActuals = new List(); - List freshTypeVars = new List(); // these are only used in the lambda@n function's definition + var subst = new Dictionary(); + var substFnAttrs = new Dictionary(); + var formals = new List(); + var callArgs = new List(); + var axCallArgs = new List(); + var dummies = new List(lambda.Dummies); + var freeTypeVars = new List(); + var fnTypeVarActuals = new List(); + var freshTypeVars = new List(); // these are only used in the lambda@n function's definition + + // compute the free variables of the lambda expression, but with lambdaBody instead of lambda.Body + Set freeVars = new Set(); + BinderExpr.ComputeBinderFreeVariables(lambda.TypeParameters, lambda.Dummies, lambdaBody, lambdaAttrs, freeVars); + foreach (object o in freeVars) { - // 'o' is either a Variable or a TypeVariable. Since the lambda desugaring happens only - // at the outermost level of a program (where there are no mutable variables) and, for - // procedure bodies, after the statements have been passified (when mutable variables have - // been replaced by immutable incarnations), we are interested only in BoundVar's and - // TypeVariable's. - BoundVariable v = o as BoundVariable; - if (v != null) { - TypedIdent ti = new TypedIdent(v.TypedIdent.tok, v.TypedIdent.Name, v.TypedIdent.Type); - Formal f = new Formal(v.tok, ti, true); + // 'o' is either a Variable or a TypeVariable. + if (o is Variable) { + var v = o as Variable; + var ti = new TypedIdent(v.TypedIdent.tok, v.TypedIdent.Name, v.TypedIdent.Type); + var f = new Formal(v.tok, ti, true); formals.Add(f); - BoundVariable b = new BoundVariable(v.tok, ti); + substFnAttrs.Add(v, new IdentifierExpr(f.tok, f)); + var b = new BoundVariable(v.tok, ti); dummies.Add(b); - callArgs.Add(new IdentifierExpr(v.tok, v)); - Expr/*!*/ id = new IdentifierExpr(f.tok, b); - Contract.Assert(id != null); + if (callOldMapping.ContainsKey(v)) { + callArgs.Add(callOldMapping[v]); + } else { + callArgs.Add(new IdentifierExpr(v.tok, v)); + } + Expr id = new IdentifierExpr(b.tok, b); subst.Add(v, id); axCallArgs.Add(id); - } else if (o is TypeVariable) { - TypeVariable tv = (TypeVariable)o; + } else { + var tv = (TypeVariable)o; freeTypeVars.Add(tv); fnTypeVarActuals.Add(tv); freshTypeVars.Add(new TypeVariable(tv.tok, tv.Name)); } } + IToken tok = lambda.tok; Formal res = new Formal(tok, new TypedIdent(tok, TypedIdent.NoName, cce.NonNull(lambda.Type)), false); - Function fn = new Function(tok, "lambda@" + lambdaid++, freshTypeVars, formals, res, "auto-generated lambda function", lambda.Attributes); + Function fn = new Function(tok, "lambda@" + lambdaid++, freshTypeVars, formals, res, "auto-generated lambda function", + Substituter.Apply(Substituter.SubstitutionFromHashtable(substFnAttrs), lambdaAttrs)); lambdaFunctions.Add(fn); FunctionCall fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name)); @@ -145,7 +152,7 @@ namespace Microsoft.Boogie { axcall.Type = res.TypedIdent.Type; axcall.TypeParameters = SimpleTypeParamInstantiation.From(freeTypeVars, fnTypeVarActuals); NAryExpr select = Expr.Select(axcall, selectArgs); - select.Type = lambda.Body.Type; + select.Type = lambdaBody.Type; List selectTypeParamActuals = new List(); List forallTypeVariables = new List(); foreach (TypeVariable/*!*/ tp in lambda.TypeParameters) { @@ -156,12 +163,14 @@ namespace Microsoft.Boogie { forallTypeVariables.AddRange(freeTypeVars); select.TypeParameters = SimpleTypeParamInstantiation.From(lambda.TypeParameters, selectTypeParamActuals); - Expr bb = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambda.Body); + Expr bb = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaBody); NAryExpr body = Expr.Eq(select, bb); body.Type = Type.Bool; body.TypeParameters = SimpleTypeParamInstantiation.EMPTY; Trigger trig = new Trigger(select.tok, true, new List { select }); - lambdaAxioms.Add(new ForallExpr(tok, forallTypeVariables, dummies, lambda.Attributes, trig, body)); + lambdaAxioms.Add(new ForallExpr(tok, forallTypeVariables, dummies, + Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaAttrs), + trig, body)); NAryExpr call = new NAryExpr(tok, fcall, callArgs); call.Type = res.TypedIdent.Type; @@ -169,6 +178,40 @@ namespace Microsoft.Boogie { return call; } + public override Cmd VisitCallCmd(CallCmd node) { + var baseResult = base.VisitCallCmd(node); + node = baseResult as CallCmd; + if (node == null) { + return baseResult; // apparently, the base visitor already turned the lambda into something else + } + // also visit the desugaring (which the StandardVisitor does not do) + node.VisitDesugaring(this); + return node; + } + } + } + + class OldFinder : ReadOnlyVisitor + { + public readonly GSet FreeOldVars = new GSet(); + public override Expr VisitOldExpr(OldExpr node) { + Set freeVars = new Set(); + node.Expr.ComputeFreeVariables(freeVars); + foreach (var v in freeVars) { + // Note, "v" is either a Variable or a TypeVariable + if (v is Variable) { + FreeOldVars.Add((Variable)v); + } + } + return node; // don't visit subexpressions, since ComputeFreeVariables has already gone through those + } + public override BinderExpr VisitBinderExpr(BinderExpr node) { + base.VisitBinderExpr(node); + // visit attributes, even though StandardVisitor does not do that (but maybe it should?) + if (node.Attributes != null) { + this.Visit(node.Attributes); + } + return node; } } diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 98987c3f..d4be8ed4 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -297,7 +297,7 @@ namespace Microsoft.Boogie { } public virtual Expr VisitLambdaExpr(LambdaExpr node) { Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); node = (LambdaExpr)this.VisitBinderExpr(node); return node; } @@ -432,6 +432,20 @@ namespace Microsoft.Boogie { node.TopLevelDeclarations = this.VisitDeclarationList(node.TopLevelDeclarations); return node; } + public virtual QKeyValue VisitQKeyValue(QKeyValue node) { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + for (int i = 0, n = node.Params.Count; i < n; i++) { + var e = node.Params[i] as Expr; + if (e != null) { + node.Params[i] = (Expr)this.Visit(e); + } + } + if (node.Next != null) { + node.Next = (QKeyValue)this.Visit(node.Next); + } + return node; + } public virtual BinderExpr VisitBinderExpr(BinderExpr node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); @@ -841,10 +855,9 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() == node); return (ForallExpr)this.VisitQuantifierExpr(node); } - public override Expr VisitLambdaExpr(LambdaExpr node) - { - Contract.Ensures(Contract.Result() == node); - return this.VisitBinderExpr(node); + public override Expr VisitLambdaExpr(LambdaExpr node) { + Contract.Ensures(Contract.Result() == node); + return this.VisitBinderExpr(node); } public override Formal VisitFormal(Formal node) { @@ -969,6 +982,19 @@ namespace Microsoft.Boogie { this.VisitDeclarationList(node.TopLevelDeclarations); return node; } + public override QKeyValue VisitQKeyValue(QKeyValue node) { + Contract.Ensures(Contract.Result() == node); + for (int i = 0, n = node.Params.Count; i < n; i++) { + var e = node.Params[i] as Expr; + if (e != null) { + this.Visit(e); + } + } + if (node.Next != null) { + this.Visit(node.Next); + } + return node; + } public override BinderExpr VisitBinderExpr(BinderExpr node) { Contract.Ensures(Contract.Result() == node); diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 2ccbf4f1..f2b77d0e 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -774,6 +774,16 @@ namespace Microsoft.Boogie } RequestIdToCancellationTokenSources[requestId] = new List(); + #region Do some pre-abstract-interpretation preprocessing on the program + // Doing lambda expansion before abstract interpretation means that the abstract interpreter + // never needs to see any lambda expressions. (On the other hand, if it were useful for it + // to see lambdas, then it would be better to more lambda expansion until after infererence.) + if (CommandLineOptions.Clo.ExpandLambdas) { + LambdaHelper.ExpandLambdas(program); + //PrintBplFile ("-", program, true); + } + #endregion + #region Infer invariants using Abstract Interpretation // Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch) @@ -789,7 +799,7 @@ namespace Microsoft.Boogie #endregion - #region Do some preprocessing on the program (e.g., loop unrolling, lambda expansion) + #region Do some post-abstract-interpretation preprocessing on the program (e.g., loop unrolling) if (CommandLineOptions.Clo.LoopUnrollCount != -1) { @@ -806,13 +816,6 @@ namespace Microsoft.Boogie { program.Emit(new TokenTextWriter(Console.Out)); } - - if (CommandLineOptions.Clo.ExpandLambdas) - { - LambdaHelper.ExpandLambdas(program); - //PrintBplFile ("-", program, true); - } - #endregion if (!CommandLineOptions.Clo.Verify) diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 49ae68e3..d2ab910b 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2638,32 +2638,6 @@ namespace VC { } #endregion Peep-hole optimizations - if (CommandLineOptions.Clo.ExpandLambdas) - { - List axioms; - List functions; - lock (program.TopLevelDeclarations) - { - LambdaHelper.Desugar(impl, out axioms, out functions); - program.TopLevelDeclarations.AddRange(functions); - } - - if (axioms.Count > 0) { - List cmds = new List(); - foreach (Expr ax in axioms) { - Contract.Assert(ax != null); - cmds.Add(new AssumeCmd(ax.tok, ax)); - } - Block entryBlock = cce.NonNull( impl.Blocks[0]); - cmds.AddRange(entryBlock.Cmds); - entryBlock.Cmds = cmds; - // Make sure that all added commands are passive commands. - Dictionary incarnationMap = ComputeIncarnationMap(entryBlock, new Dictionary>()); - TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo, - ComputeOldExpressionSubstitution(impl.Proc.Modifies)); - } - } - HandleSelectiveChecking(impl); -- cgit v1.2.3