diff options
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 14 | ||||
| -rw-r--r-- | Source/Core/AbsyQuant.cs | 39 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 129 | ||||
| -rw-r--r-- | Source/Core/LambdaHelper.cs | 147 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 36 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 19 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 26 | ||||
| -rw-r--r-- | Test/test2/Answer | 6 | ||||
| -rw-r--r-- | Test/test2/Lambda.bpl | 8 | ||||
| -rw-r--r-- | Test/test2/LambdaOldExpressions.bpl | 26 |
10 files changed, 299 insertions, 151 deletions
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;
}
}
+ /// <summary>
+ /// 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).
+ /// </summary>
+ 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<TypeVariable> typeParameters, List<Variable> 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<TypeVariable> 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<Expr>() != null);
return base.VisitOldExpr((OldExpr)node.Clone());
}
- public override Cmd VisitParCallCmd(ParCallCmd node)
- {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Cmd>() != null);
- ParCallCmd clone = (ParCallCmd)node.Clone();
- Contract.Assert(clone != null);
- clone.CallCmds = new List<CallCmd>(node.CallCmds);
- return base.VisitParCallCmd(clone);
+ public override Cmd VisitParCallCmd(ParCallCmd node) {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+ ParCallCmd clone = (ParCallCmd)node.Clone();
+ Contract.Assert(clone != null);
+ clone.CallCmds = new List<CallCmd>(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<Program>() != null);
return base.VisitProgram((Program)node.Clone());
}
+ public override QKeyValue VisitQKeyValue(QKeyValue node) {
+ //Contract.Requires(node != null);
+ var newParams = new List<object>();
+ 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<BinderExpr>() != null);
@@ -411,14 +424,16 @@ namespace Microsoft.Boogie { }
}
+ // ----------------------------- Substitutions for Expr -------------------------------
+
/// <summary>
/// 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.
/// </summary>
public static Expr Apply(Substitution subst, Expr expr) {
- Contract.Requires(expr != null);
Contract.Requires(subst != null);
+ Contract.Requires(expr != null);
Contract.Ensures(Contract.Result<Expr>() != 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.
/// </summary>
- 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<Expr>() != 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<Expr>() != null);
+ return (Expr)new NormalSubstituter(always, forold).Visit(expr);
}
/// <summary>
+ /// 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.
+ /// </summary>
+ 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<Expr>() != null);
+ return (Expr)new ReplacingOldSubstituter(always, forOld).Visit(expr);
+ }
+
+ // ----------------------------- Substitutions for Cmd -------------------------------
+
+ /// <summary>
/// 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.
/// </summary>
public static Cmd Apply(Substitution subst, Cmd cmd) {
- Contract.Requires(cmd != null);
Contract.Requires(subst != null);
+ Contract.Requires(cmd != null);
Contract.Ensures(Contract.Result<Cmd>() != 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.
/// </summary>
- 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<Cmd>() != null);
- return (Cmd)new NormalSubstituter(always, forold).Visit(cmd);
+ return (Cmd)new NormalSubstituter(always, forOld).Visit(cmd);
}
/// <summary>
- /// 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.
/// </summary>
- 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<Expr>() != null);
- return (Expr)new ReplacingOldSubstituter(always, forold).Visit(expr);
+ Contract.Requires(forOld != null);
+ Contract.Requires(cmd != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+ return (Cmd)new ReplacingOldSubstituter(always, forOld).Visit(cmd);
}
+ // ----------------------------- Substitutions for QKeyValue -------------------------------
+
/// <summary>
- /// 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.
+ /// </summary>
+ 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);
+ }
+ }
+
+ /// <summary>
+ /// Apply a substitution to a list of attributes replacing "old" expressions.
+ /// For a further description, see "ApplyReplacingOldExprs" above for Expr.
/// </summary>
- 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<Cmd>() != 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<Program>() != 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<Procedure>() != 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<Variable, Expr>(); // g -> g0
+ var callOldMapping = new Dictionary<Variable, Expr>(); // 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<Variable,Expr>()),
+ Substituter.SubstitutionFromHashtable(oldSubst),
+ lambda.Body);
+ var lambdaAttrs = Substituter.ApplyReplacingOldExprs(
+ Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>()),
+ Substituter.SubstitutionFromHashtable(oldSubst),
+ lambda.Attributes);
- Set freeVars = new Set();
- lambda.ComputeFreeVariables(freeVars);
// this is ugly, the output will depend on hashing order
- Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();
- List<Variable> formals = new List<Variable>();
- List<Expr> callArgs = new List<Expr>();
- List<Expr> axCallArgs = new List<Expr>();
- List<Variable> dummies = new List<Variable>(lambda.Dummies);
- List<TypeVariable> freeTypeVars = new List<TypeVariable>();
- List<Type/*!*/> fnTypeVarActuals = new List<Type/*!*/>();
- List<TypeVariable> freshTypeVars = new List<TypeVariable>(); // these are only used in the lambda@n function's definition
+ var subst = new Dictionary<Variable, Expr>();
+ var substFnAttrs = new Dictionary<Variable, Expr>();
+ var formals = new List<Variable>();
+ var callArgs = new List<Expr>();
+ var axCallArgs = new List<Expr>();
+ var dummies = new List<Variable>(lambda.Dummies);
+ var freeTypeVars = new List<TypeVariable>();
+ var fnTypeVarActuals = new List<Type/*!*/>();
+ var freshTypeVars = new List<TypeVariable>(); // 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<Type/*!*/> selectTypeParamActuals = new List<Type/*!*/>();
List<TypeVariable> forallTypeVariables = new List<TypeVariable>();
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<Expr> { 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<Variable> FreeOldVars = new GSet<Variable>();
+ 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<LambdaExpr>() != null);
+ Contract.Ensures(Contract.Result<Expr>() != 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<QKeyValue>() != 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<BinderExpr>() != null);
@@ -841,10 +855,9 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<ForallExpr>() == node);
return (ForallExpr)this.VisitQuantifierExpr(node);
}
- public override Expr VisitLambdaExpr(LambdaExpr node)
- {
- Contract.Ensures(Contract.Result<LambdaExpr>() == node);
- return this.VisitBinderExpr(node);
+ public override Expr VisitLambdaExpr(LambdaExpr node) {
+ Contract.Ensures(Contract.Result<Expr>() == 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<QKeyValue>() == 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<BinderExpr>() == 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<CancellationTokenSource>();
+ #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<Expr> axioms;
- List<Function> functions;
- lock (program.TopLevelDeclarations)
- {
- LambdaHelper.Desugar(impl, out axioms, out functions);
- program.TopLevelDeclarations.AddRange(functions);
- }
-
- if (axioms.Count > 0) {
- List<Cmd> cmds = new List<Cmd>();
- 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<Variable, Expr> incarnationMap = ComputeIncarnationMap(entryBlock, new Dictionary<Block, Dictionary<Variable, Expr>>());
- TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo,
- ComputeOldExpressionSubstitution(impl.Proc.Modifies));
- }
- }
-
HandleSelectiveChecking(impl);
diff --git a/Test/test2/Answer b/Test/test2/Answer index 609cf1ed..ecec6339 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -369,7 +369,7 @@ Lambda.bpl(38,3): Error BP5001: This assertion might not hold. Execution trace:
Lambda.bpl(36,5): anon0
-Boogie program verifier finished with 5 verified, 2 errors
+Boogie program verifier finished with 6 verified, 2 errors
-------------------- LambdaPoly.bpl --------------------
LambdaPoly.bpl(28,5): Error BP5001: This assertion might not hold.
@@ -393,7 +393,7 @@ LambdaOldExpressions.bpl(21,3): Related location: This is the postcondition that Execution trace:
LambdaOldExpressions.bpl(25,7): anon0
-Boogie program verifier finished with 2 verified, 1 error
+Boogie program verifier finished with 4 verified, 1 error
-------------------- SelectiveChecking.bpl --------------------
SelectiveChecking.bpl(17,3): Error BP5001: This assertion might not hold.
@@ -453,7 +453,7 @@ Lambda.bpl(38,3): Error BP5001: This assertion might not hold. Execution trace:
Lambda.bpl(36,5): anon0
-Boogie program verifier finished with 5 verified, 2 errors
+Boogie program verifier finished with 6 verified, 2 errors
-------------------- TypeEncodingM.bpl /typeEncoding:m --------------------
TypeEncodingM.bpl(24,3): Error BP5001: This assertion might not hold.
diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl index 477d0f36..68c83d43 100644 --- a/Test/test2/Lambda.bpl +++ b/Test/test2/Lambda.bpl @@ -63,3 +63,11 @@ procedure nestedLambda() a := (lambda x: int :: (lambda y: int :: x+y)); } +// The following tests that the lambda in the desugaring of the +// call command gets replaced. +procedure P(); + ensures (lambda y: int :: y == y)[15]; +procedure Q() +{ + call P(); +} diff --git a/Test/test2/LambdaOldExpressions.bpl b/Test/test2/LambdaOldExpressions.bpl index c26b0198..9f17245f 100644 --- a/Test/test2/LambdaOldExpressions.bpl +++ b/Test/test2/LambdaOldExpressions.bpl @@ -4,8 +4,8 @@ var b: bool; procedure p0();
requires b;
modifies b;
- ensures (lambda x: bool :: old(b))[true];
- ensures !(lambda x: bool :: b)[true];
+ ensures (lambda x: bool :: {:MyAttr "put an attr here", !b} old(b))[true];
+ ensures !(lambda x: bool :: {:AnotherAttr "yes, why not", b} {:ABC b, b, old(b)} b)[true];
implementation p0()
{
@@ -37,3 +37,25 @@ implementation p2() b := !b;
assert (lambda x: bool :: old(b) != b)[true];
}
+
+
+procedure p3();
+ requires b;
+ modifies b;
+ ensures (lambda x: int :: old(old(b)) != b)[15];
+
+implementation p3()
+{
+ b := !b;
+ assert (lambda x: int :: old(old(b)) != b)[15];
+}
+
+// Note that variables (inside and outside old expressions) mentioned
+// in attributes (even if they are not mentioned in the body of the
+// lambda) are also picked up by the auto-generated lambda functions,
+// so that the attributes can be copied to the function and axiom.
+var h: int;
+procedure TestAttributeParameters()
+ ensures (lambda x: int :: {:MyAttribute old(h), h} x < 100)[23];
+{
+}
|