using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using Bpl = Microsoft.Boogie;
namespace Microsoft.Dafny
{
[ContractClass(typeof(IRewriterContracts))]
public interface IRewriter
{
void PreResolve(ModuleDefinition m);
void PostResolve(ModuleDefinition m);
// After SCC/Cyclicity/Recursivity analysis:
void PostCyclicityResolve(ModuleDefinition m);
}
[ContractClassFor(typeof(IRewriter))]
abstract class IRewriterContracts : IRewriter
{
public void PreResolve(ModuleDefinition m) {
Contract.Requires(m != null);
}
public void PostResolve(ModuleDefinition m) {
Contract.Requires(m != null);
}
public void PostCyclicityResolve(ModuleDefinition m) {
Contract.Requires(m != null);
}
}
public class AutoGeneratedToken : TokenWrapper
{
public AutoGeneratedToken(Boogie.IToken wrappedToken)
: base(wrappedToken)
{
Contract.Requires(wrappedToken != null);
}
}
///
/// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate
/// into a class. From the user's perspective, what needs to be done is simply:
/// - mark the class with {:autocontracts}
/// - declare a function (or predicate) called Valid()
///
/// AutoContracts will then:
///
/// Declare:
/// ghost var Repr: set(object);
///
/// For function/predicate Valid(), insert:
/// reads this, Repr;
/// Into body of Valid(), insert (at the beginning of the body):
/// this in Repr && null !in Repr
/// and also insert, for every array-valued field A declared in the class:
/// (A != null ==> A in Repr) &&
/// and for every field F of a class type T where T has a field called Repr, also insert:
/// (F != null ==> F in Repr && F.Repr SUBSET Repr && this !in Repr)
/// Except, if A or F is declared with {:autocontracts false}, then the implication will not
/// be added.
///
/// For every constructor, add:
/// modifies this;
/// ensures Valid() && fresh(Repr - {this});
/// At the end of the body of the constructor, add:
/// Repr := {this};
/// if (A != null) { Repr := Repr + {A}; }
/// if (F != null) { Repr := Repr + {F} + F.Repr; }
///
/// For every method, add:
/// requires Valid();
/// modifies Repr;
/// ensures Valid() && fresh(Repr - old(Repr));
/// At the end of the body of the method, add:
/// if (A != null) { Repr := Repr + {A}; }
/// if (F != null) { Repr := Repr + {F} + F.Repr; }
///
public class AutoContractsRewriter : IRewriter
{
public void PreResolve(ModuleDefinition m) {
foreach (var d in m.TopLevelDecls) {
bool sayYes = true;
if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) {
ProcessClassPreResolve((ClassDecl)d);
}
}
}
void ProcessClassPreResolve(ClassDecl cl) {
// Add: ghost var Repr: set;
// ...unless a field with that name is already present
if (!cl.Members.Exists(member => member is Field && member.Name == "Repr")) {
Type ty = new SetType(new ObjectType());
cl.Members.Add(new Field(new AutoGeneratedToken(cl.tok), "Repr", true, ty, null));
}
foreach (var member in cl.Members) {
bool sayYes = true;
if (Attributes.ContainsBool(member.Attributes, "autocontracts", ref sayYes) && !sayYes) {
// the user has excluded this member
continue;
}
if (member.RefinementBase != null) {
// member is inherited from a module where it was already processed
continue;
}
Boogie.IToken tok = new AutoGeneratedToken(member.tok);
if (member is Function && member.Name == "Valid" && !member.IsStatic) {
var valid = (Function)member;
// reads this;
valid.Reads.Add(new FrameExpression(tok, new ThisExpr(tok), null));
// reads Repr;
valid.Reads.Add(new FrameExpression(tok, new MemberSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"), null));
} else if (member is Constructor) {
var ctor = (Constructor)member;
// modifies this;
ctor.Mod.Expressions.Add(new FrameExpression(tok, new ImplicitThisExpr(tok), null));
// ensures Valid();
ctor.Ens.Insert(0, new MaybeFreeExpression(new FunctionCallExpr(tok, "Valid", new ImplicitThisExpr(tok), tok, new List())));
// ensures fresh(Repr - {this});
var freshness = new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Fresh, new BinaryExpr(tok, BinaryExpr.Opcode.Sub,
new MemberSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"),
new SetDisplayExpr(tok, new List() { new ThisExpr(tok) })));
ctor.Ens.Insert(1, new MaybeFreeExpression(freshness));
} else if (member is Method && !member.IsStatic) {
var m = (Method)member;
// requires Valid();
m.Req.Insert(0, new MaybeFreeExpression(new FunctionCallExpr(tok, "Valid", new ImplicitThisExpr(tok), tok, new List())));
// If this is a mutating method, we should also add a modifies clause and a postcondition, but we don't do that if it's
// a simple query method. However, we won't know if it's a simple query method until after resolution, so we'll add the
// rest of the spec then.
}
}
}
public void PostResolve(ModuleDefinition m) {
foreach (var d in m.TopLevelDecls) {
bool sayYes = true;
if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) {
ProcessClassPostResolve((ClassDecl)d);
}
}
}
public void PostCyclicityResolve(ModuleDefinition m) {
}
void ProcessClassPostResolve(ClassDecl cl) {
// Find all fields of a reference type, and make a note of whether or not the reference type has a Repr field.
// Also, find the Repr field and the function Valid in class "cl"
Field ReprField = null;
Function Valid = null;
var subobjects = new List>();
foreach (var member in cl.Members) {
var field = member as Field;
if (field != null) {
bool sayYes = true;
if (field.Name == "Repr") {
ReprField = field;
} else if (Attributes.ContainsBool(field.Attributes, "autocontracts", ref sayYes) && !sayYes) {
// ignore this field
} else if (field.Type is ObjectType) {
subobjects.Add(new Tuple(field, null));
} else if (field.Type.IsRefType) {
var rcl = (ClassDecl)((UserDefinedType)field.Type).ResolvedClass;
Field rRepr = null;
foreach (var memb in rcl.Members) {
var f = memb as Field;
if (f != null && f.Name == "Repr") {
rRepr = f;
break;
}
}
subobjects.Add(new Tuple(field, rRepr));
}
} else if (member is Function && member.Name == "Valid" && !member.IsStatic) {
var fn = (Function)member;
if (fn.Formals.Count == 0 && fn.ResultType.IsBoolType) {
Valid = fn;
}
}
}
Contract.Assert(ReprField != null); // we expect there to be a "Repr" field, since we added one in PreResolve
Boogie.IToken clTok = new AutoGeneratedToken(cl.tok);
Type ty = UserDefinedType.FromTopLevelDecl(clTok, cl);
var self = new ThisExpr(clTok);
self.Type = ty;
var implicitSelf = new ImplicitThisExpr(clTok);
implicitSelf.Type = ty;
var Repr = new MemberSelectExpr(clTok, implicitSelf, "Repr");
Repr.Member = ReprField;
Repr.Type = ReprField.Type;
var cNull = new LiteralExpr(clTok);
cNull.Type = new ObjectType();
foreach (var member in cl.Members) {
bool sayYes = true;
if (Attributes.ContainsBool(member.Attributes, "autocontracts", ref sayYes) && !sayYes) {
continue;
}
Boogie.IToken tok = new AutoGeneratedToken(member.tok);
if (member is Function && member.Name == "Valid" && !member.IsStatic) {
var valid = (Function)member;
if (valid.IsGhost && valid.ResultType.IsBoolType) {
Expression c;
if (valid.RefinementBase == null) {
var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, self, Repr); // this in Repr
var c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NotInSet, cNull, Repr); // null !in Repr
c = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c0, c1);
} else {
c = new LiteralExpr(tok, true);
c.Type = Type.Bool;
}
foreach (var ff in subobjects) {
if (ff.Item1.RefinementBase != null) {
// the field has been inherited from a refined module, so don't include it here
continue;
}
var F = Resolver.NewMemberSelectExpr(tok, implicitSelf, ff.Item1, null);
var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NeqCommon, F, cNull);
var c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, F, Repr);
if (ff.Item2 == null) {
// F != null ==> F in Repr (so, nothing else to do)
} else {
// F != null ==> F in Repr && F.Repr <= Repr && this !in F.Repr
var FRepr = new MemberSelectExpr(tok, F, ff.Item2.Name);
FRepr.Member = ff.Item2;
FRepr.Type = ff.Item2.Type;
var c2 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.Subset, FRepr, Repr);
var c3 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NotInSet, self, FRepr);
c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c1, BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c2, c3));
}
c = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c, BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.Imp, c0, c1));
}
if (valid.Body == null) {
valid.Body = c;
} else {
valid.Body = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c, valid.Body);
}
}
} else if (member is Constructor) {
var ctor = (Constructor)member;
if (ctor.Body != null) {
var bodyStatements = ((BlockStmt)ctor.Body).Body;
// Repr := {this};
var e = new SetDisplayExpr(tok, new List() { self });
e.Type = new SetType(new ObjectType());
Statement s = new AssignStmt(tok, tok, Repr, new ExprRhs(e));
s.IsGhost = true;
bodyStatements.Add(s);
AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);
}
} else if (member is Method && !member.IsStatic) {
var m = (Method)member;
if (Valid != null && !IsSimpleQueryMethod(m)) {
if (member.RefinementBase == null) {
// modifies Repr;
m.Mod.Expressions.Add(new FrameExpression(Repr.tok, Repr, null));
// ensures Valid();
var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List());
valid.Function = Valid;
valid.Type = Type.Bool;
// Add the identity substitution to this call
valid.TypeArgumentSubstitutions = new Dictionary();
foreach (var p in cl.TypeArgs) {
valid.TypeArgumentSubstitutions.Add(p, new UserDefinedType(p));
}
m.Ens.Insert(0, new MaybeFreeExpression(valid));
// ensures fresh(Repr - old(Repr));
var e0 = new OldExpr(tok, Repr);
e0.Type = Repr.Type;
var e1 = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, Repr, e0);
e1.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference;
e1.Type = Repr.Type;
var freshness = new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Fresh, e1);
freshness.Type = Type.Bool;
m.Ens.Insert(1, new MaybeFreeExpression(freshness));
}
if (m.Body != null) {
var bodyStatements = ((BlockStmt)m.Body).Body;
AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);
}
}
}
}
}
void AddSubobjectReprs(Boogie.IToken tok, List> subobjects, List bodyStatements,
Expression self, Expression implicitSelf, Expression cNull, Expression Repr) {
// TODO: these assignments should be included on every return path
foreach (var ff in subobjects) {
var F = Resolver.NewMemberSelectExpr(tok, implicitSelf, ff.Item1, null); // create a resolved MemberSelectExpr
Expression e = new SetDisplayExpr(tok, new List() { F });
e.Type = new SetType(new ObjectType()); // resolve here
var rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, Repr, e);
rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union; // resolve here
rhs.Type = Repr.Type; // resolve here
if (ff.Item2 == null) {
// Repr := Repr + {F} (so, nothing else to do)
} else {
// Repr := Repr + {F} + F.Repr
var FRepr = Resolver.NewMemberSelectExpr(tok, F, ff.Item2, null); // create resolved MemberSelectExpr
rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, rhs, FRepr);
rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union; // resolve here
rhs.Type = Repr.Type; // resolve here
}
// Repr := Repr + ...;
Statement s = new AssignStmt(tok, tok, Repr, new ExprRhs(rhs));
s.IsGhost = true;
// wrap if statement around s
e = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NeqCommon, F, cNull);
var thn = new BlockStmt(tok, tok, new List() { s });
thn.IsGhost = true;
s = new IfStmt(tok, tok, e, thn, null);
s.IsGhost = true;
// finally, add s to the body
bodyStatements.Add(s);
}
}
bool IsSimpleQueryMethod(Method m) {
// A simple query method has out parameters, its body has no effect other than to assign to them,
// and the postcondition does not explicitly mention the pre-state.
return m.Outs.Count != 0 && m.Body != null && LocalAssignsOnly(m.Body) &&
m.Ens.TrueForAll(mfe => !MentionsOldState(mfe.E));
}
bool LocalAssignsOnly(Statement s) {
Contract.Requires(s != null);
if (s is AssignStmt) {
var ss = (AssignStmt)s;
return ss.Lhs.Resolved is IdentifierExpr;
} else if (s is ConcreteUpdateStatement) {
var ss = (ConcreteUpdateStatement)s;
return ss.Lhss.TrueForAll(e => e.Resolved is IdentifierExpr);
} else if (s is CallStmt) {
return false;
} else {
foreach (var ss in s.SubStatements) {
if (!LocalAssignsOnly(ss)) {
return false;
}
}
}
return true;
}
///
/// Returns true iff 'expr' is a two-state expression, that is, if it mentions "old(...)" or "fresh(...)".
///
static bool MentionsOldState(Expression expr) {
Contract.Requires(expr != null);
if (expr is OldExpr) {
return true;
} else if (expr is UnaryOpExpr && ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh) {
return true;
}
foreach (var ee in expr.SubExpressions) {
if (MentionsOldState(ee)) {
return true;
}
}
return false;
}
public static BinaryExpr BinBoolExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1) {
var p = new BinaryExpr(tok, BinaryExpr.ResolvedOp2SyntacticOp(rop), e0, e1);
p.ResolvedOp = rop; // resolve here
p.Type = Type.Bool; // resolve here
return p;
}
}
///
/// For any function foo() with the :opaque attribute,
/// hide the body, so that it can only be seen within its
/// recursive clique (if any), or if the programmer
/// specifically asks to see it via the reveal_foo() lemma
///
public class OpaqueFunctionRewriter : IRewriter {
readonly ResolutionErrorReporter reporter;
protected Dictionary fullVersion; // Given an opaque function, retrieve the full
protected Dictionary original; // Given a full version of an opaque function, find the original opaque version
protected Dictionary revealOriginal; // Map reveal_* lemmas back to their original functions
public OpaqueFunctionRewriter(ResolutionErrorReporter reporter)
: base() {
this.reporter = reporter;
fullVersion = new Dictionary();
original = new Dictionary();
revealOriginal = new Dictionary();
}
public void PreResolve(ModuleDefinition m) {
foreach (var d in m.TopLevelDecls) {
if (d is ClassDecl) {
DuplicateOpaqueClassFunctions((ClassDecl)d);
}
}
}
public void PostResolve(ModuleDefinition m) {
// Fix up the ensures clause of the full version of the function,
// since it may refer to the original opaque function
foreach (var fn in ModuleDefinition.AllFunctions(m.TopLevelDecls)) {
if (isFullVersion(fn)) { // Is this a function we created to supplement an opaque function?
OpaqueFunctionVisitor visitor = new OpaqueFunctionVisitor();
var context = new OpaqueFunctionContext(original[fn], fn);
foreach (Expression ens in fn.Ens) {
visitor.Visit(ens, context);
}
}
}
foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
if (decl is Lemma) {
var lem = (Lemma)decl;
if (revealOriginal.ContainsKey(lem)) {
fixupRevealLemma(lem, revealOriginal[lem]);
fixupTypeArguments(lem, revealOriginal[lem]);
}
}
}
}
public void PostCyclicityResolve(ModuleDefinition m) {
// Add layer quantifier if the function is recursive
foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
if (decl is Lemma) {
var lem = (Lemma)decl;
if (revealOriginal.ContainsKey(lem)) {
needsLayerQuantifier(lem, revealOriginal[lem]);
}
}
}
}
// Is f the full version of an opaque function?
public bool isFullVersion(Function f) {
return original.ContainsKey(f);
}
// In case we change how opacity is denoted
public bool isOpaque(Function f) {
return fullVersion.ContainsKey(f);
}
public Function OpaqueVersion(Function f) {
Function ret;
original.TryGetValue(f, out ret);
return ret;
}
public Function FullVersion(Function f) {
Function ret;
fullVersion.TryGetValue(f, out ret);
return ret;
}
// Trims the body from the original function and then adds an internal,
// full version, along with a lemma connecting the two
protected void DuplicateOpaqueClassFunctions(ClassDecl c) {
List newDecls = new List();
foreach (MemberDecl member in c.Members) {
if (member is Function) {
var f = (Function)member;
if (!Attributes.Contains(f.Attributes, "opaque")) {
// Nothing to do
} else if (f.IsProtected) {
reporter.Error(f.tok, ":opaque is not allowed to be applied to protected functions (this will be allowed when the language introduces 'opaque'/'reveal' as keywords)");
} else if (!RefinementToken.IsInherited(f.tok, c.Module)) {
// Create a copy, which will be the internal version with a full body
// which will allow us to verify that the ensures are true
var cloner = new Cloner();
var fWithBody = cloner.CloneFunction(f, "#" + f.Name + "_FULL");
newDecls.Add(fWithBody);
fullVersion.Add(f, fWithBody);
original.Add(fWithBody, f);
var newToken = new Boogie.Token(f.tok.line, f.tok.col);
newToken.filename = f.tok.filename;
newToken._val = fWithBody.Name;
newToken._kind = f.tok.kind;
newToken._pos = f.tok.pos;
fWithBody.tok = newToken;
// Annotate the new function so we remember that we introduced it
fWithBody.Attributes = new Attributes("opaque_full", new List(), fWithBody.Attributes);
// Create a lemma to allow the user to selectively reveal the function's body
// That is, given:
// function {:opaque} foo(x:int, y:int) : int
// requires 0 <= x < 5;
// requires 0 <= y < 5;
// ensures foo(x, y) < 10;
// { x + y }
// We produce:
// lemma {:axiom} reveal_foo()
// ensures forall x:int, y:int {:trigger foo(x,y)} :: 0 <= x < 5 && 0 <= y < 5 ==> foo(x,y) == foo_FULL(x,y);
Expression reqExpr = new LiteralExpr(f.tok, true);
foreach (Expression req in f.Req) {
Expression newReq = cloner.CloneExpr(req);
reqExpr = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, reqExpr, newReq);
}
List typeVars = new List();
foreach (TypeParameter tp in f.TypeArgs) {
typeVars.Add(cloner.CloneTypeParam(tp));
}
List boundVars = new List();
foreach (Formal formal in f.Formals) {
boundVars.Add(new BoundVar(f.tok, formal.Name, cloner.CloneType(formal.Type)));
}
// Build the implication connecting the function's requires to the connection with the revealed-body version
Func func_builder = func =>
new ApplySuffix(func.tok,
new NameSegment(func.tok, func.Name, null),
func.Formals.ConvertAll(x => (Expression)new IdentifierExpr(func.tok, x.Name)));
var oldEqualsNew = new BinaryExpr(f.tok, BinaryExpr.Opcode.Eq, func_builder(f), func_builder(fWithBody));
var requiresImpliesOldEqualsNew = new BinaryExpr(f.tok, BinaryExpr.Opcode.Imp, reqExpr, oldEqualsNew);
MaybeFreeExpression newEnsures;
if (f.Formals.Count > 0) {
// Build an explicit trigger for the forall, so Z3 doesn't get confused
Expression trigger = func_builder(f);
List args = new List();
args.Add(trigger);
Attributes attrs = new Attributes("trigger", args, null);
// Also specify that this is a type quantifier
attrs = new Attributes("typeQuantifier", new List(), attrs);
newEnsures = new MaybeFreeExpression(new ForallExpr(f.tok, typeVars, boundVars, null, requiresImpliesOldEqualsNew, attrs));
} else {
// No need for a forall
newEnsures = new MaybeFreeExpression(oldEqualsNew);
}
var newEnsuresList = new List();
newEnsuresList.Add(newEnsures);
// Add an axiom attribute so that the compiler won't complain about the lemma's lack of a body
Attributes lemma_attrs = new Attributes("axiom", new List(), null);
var reveal = new Lemma(f.tok, "reveal_" + f.Name, f.HasStaticKeyword, new List(), new List(), new List(), new List(),
new Specification(new List(), null), newEnsuresList,
new Specification(new List(), null), null, lemma_attrs, null);
newDecls.Add(reveal);
revealOriginal[reveal] = f;
// Update f's body to simply call the full version, so we preserve recursion checks, decreases clauses, etc.
f.Body = func_builder(fWithBody);
}
}
}
c.Members.AddRange(newDecls);
}
protected class OpaqueFunctionContext {
public Function original; // The original declaration of the opaque function
public Function full; // The version we added that has a body
public OpaqueFunctionContext(Function Orig, Function Full) {
original = Orig;
full = Full;
}
}
class OpaqueFunctionVisitor : TopDownVisitor {
protected override bool VisitOneExpr(Expression expr, ref OpaqueFunctionContext context) {
if (expr is FunctionCallExpr) {
var e = (FunctionCallExpr)expr;
if (e.Function == context.original) { // Attempting to call the original opaque function
// Redirect the call to the full version and its type-argument substitution map
// First, do some sanity checks:
Contract.Assert(e.TypeArgumentSubstitutions.Count == context.original.EnclosingClass.TypeArgs.Count + context.original.TypeArgs.Count);
Contract.Assert(context.original.EnclosingClass == context.full.EnclosingClass);
Contract.Assert(context.original.TypeArgs.Count == context.full.TypeArgs.Count);
if (context.full.TypeArgs.Count != 0) {
var newTypeArgsSubst = new Dictionary();
context.original.EnclosingClass.TypeArgs.ForEach(tp => newTypeArgsSubst.Add(tp, e.TypeArgumentSubstitutions[tp]));
for (int i = 0; i < context.original.TypeArgs.Count; i++) {
var tpOrig = context.original.TypeArgs[i];
var tpFull = context.full.TypeArgs[i];
newTypeArgsSubst.Add(tpFull, e.TypeArgumentSubstitutions[tpOrig]);
}
e.TypeArgumentSubstitutions = newTypeArgsSubst;
}
e.Function = context.full;
}
}
return true;
}
}
// If the function is recursive, make the reveal lemma quantifier a layerQuantifier
protected void needsLayerQuantifier(Lemma lem, Function fn) {
var origForall = lem.Ens[0].E as ForallExpr;
if (origForall != null && fn.IsRecursive) {
var newAttrib = new Attributes("layerQuantifier", new List(), origForall.Attributes);
var newForall = new ForallExpr(origForall.tok, origForall.TypeArgs, origForall.BoundVars, origForall.Range, origForall.Term, newAttrib);
newForall.Type = Type.Bool;
lem.Ens[0] = new MaybeFreeExpression(newForall);
}
}
// This is for the reveal_F function. The ensures clause looks like this:
//
// ensures forall x : T :: F(x) == F_FULL(x)
//
// But the type argument substitutions for F and F_FULL are way off, so
// we use this function to make a substitution to the type variables the
// forall quantifier binds.
protected void fixupTypeArguments(Lemma lem, Function fn) {
var origForall = lem.Ens[0].E as ForallExpr;
if (origForall != null) {
Contract.Assert(origForall.TypeArgs.Count == fn.TypeArgs.Count);
fixupTypeArguments(lem.Ens[0].E, origForall.TypeArgs);
}
}
protected void fixupTypeArguments(Expression expr, List qparams) {
FunctionCallExpr e;
if ((e = expr as FunctionCallExpr) != null) {
e.TypeArgumentSubstitutions = new Dictionary();
for (int i = 0; i < e.Function.TypeArgs.Count; i++) {
e.TypeArgumentSubstitutions[e.Function.TypeArgs[i]] = new UserDefinedType(qparams[i]);
}
}
foreach (var ee in expr.SubExpressions) {
fixupTypeArguments(ee, qparams);
}
}
protected void fixupRevealLemma(Lemma lem, Function fn) {
if (fn.Req.Count == 0) {
return;
}
// DR: Note: I don't know of any example that actually gets to these lines below:
// Consolidate the requirements
Expression reqs = Expression.CreateBoolLiteral(fn.tok, true);
foreach (var expr in fn.Req) {
reqs = Expression.CreateAnd(reqs, expr);
}
if (fn.Formals.Count == 0)
{
lem.Ens[0] = new MaybeFreeExpression(Expression.CreateImplies(reqs, lem.Ens[0].E));
return;
}
var origForall = (ForallExpr)lem.Ens[0].E;
var origImpl = (BinaryExpr)origForall.Term;
// Substitute the forall's variables for those of the fn
var formals = fn.Formals.ConvertAll(x => (NonglobalVariable)x);
reqs = Expression.VarSubstituter(formals, origForall.BoundVars, reqs);
var newImpl = Expression.CreateImplies(reqs, origImpl.E1);
//var newForall = Expression.CreateQuantifier(origForall, true, newImpl);
var newForall = new ForallExpr(origForall.tok, origForall.TypeArgs, origForall.BoundVars, origForall.Range, newImpl, origForall.Attributes);
newForall.Type = Type.Bool;
lem.Ens[0] = new MaybeFreeExpression(newForall);
}
}
///
/// Automatically accumulate requires for function calls within a function body,
/// if requested via {:autoreq}
///
public class AutoReqFunctionRewriter : IRewriter {
Function parentFunction;
Resolver resolver;
OpaqueFunctionRewriter opaqueInfo;
bool containsMatch; // TODO: Track this per-requirement, rather than per-function
public AutoReqFunctionRewriter(Resolver r, OpaqueFunctionRewriter o) {
this.resolver = r;
this.opaqueInfo = o;
}
public void PreResolve(ModuleDefinition m) {
}
public void PostResolve(ModuleDefinition m) {
var components = m.CallGraph.TopologicallySortedComponents();
foreach (var scComponent in components) { // Visit the call graph bottom up, so anything we call already has its prequisites calculated
if (scComponent is Function) {
Function fn = (Function)scComponent;
if (Attributes.ContainsBoolAtAnyLevel(fn, "autoReq")) {
parentFunction = fn; // Remember where the recursion started
containsMatch = false; // Assume no match statements are involved
if (!opaqueInfo.isOpaque(fn)) { // It's a normal function
List auto_reqs = new List();
// First handle all of the requirements' preconditions
foreach (Expression req in fn.Req) {
auto_reqs.AddRange(generateAutoReqs(req));
}
fn.Req.InsertRange(0, auto_reqs); // Need to come before the actual requires
addAutoReqToolTipInfoToFunction("pre", fn, auto_reqs);
// Then the body itself, if any
if (fn.Body != null) {
auto_reqs = generateAutoReqs(fn.Body);
fn.Req.AddRange(auto_reqs);
addAutoReqToolTipInfoToFunction("post", fn, auto_reqs);
}
} else { // Opaque functions need special handling
// The opaque function's requirements are the same as for the _FULL version,
// so we don't need to generate them again. We do, however, need to swap
// the function's variables for those of the FULL version
List fnVars = new List();
foreach (var formal in fn.Formals) {
var id = new IdentifierExpr(formal.tok, formal.Name);
id.Var = formal; // resolve here
id.Type = formal.Type; // resolve here
fnVars.Add(id);
}
var new_reqs = new List();
foreach (var req in opaqueInfo.FullVersion(fn).Req) {
new_reqs.Add(subVars(opaqueInfo.FullVersion(fn).Formals, fnVars, req, null));
}
fn.Req.Clear();
fn.Req.AddRange(new_reqs);
}
}
}
else if (scComponent is Method)
{
Method method = (Method)scComponent;
if (Attributes.ContainsBoolAtAnyLevel(method, "autoReq"))
{
parentFunction = null;
containsMatch = false; // Assume no match statements are involved
List auto_reqs = new List();
foreach (MaybeFreeExpression req in method.Req)
{
List local_auto_reqs = generateAutoReqs(req.E);
foreach (Expression local_auto_req in local_auto_reqs)
{
auto_reqs.Add(new MaybeFreeExpression(local_auto_req, !req.IsFree));
}
}
method.Req.InsertRange(0, auto_reqs); // Need to come before the actual requires
addAutoReqToolTipInfoToMethod("pre", method, auto_reqs);
}
}
}
}
public void PostCyclicityResolve(ModuleDefinition m) {
}
Expression subVars(List formals, List values, Expression e, Expression f_this) {
Contract.Assert(formals != null);
Contract.Assert(values != null);
Contract.Assert(formals.Count == values.Count);
Dictionary substMap = new Dictionary();
Dictionary typeMap = new Dictionary();
for (int i = 0; i < formals.Count; i++) {
substMap.Add(formals[i], values[i]);
}
Translator.Substituter sub = new Translator.Substituter(f_this, substMap, typeMap, null);
return sub.Substitute(e);
}
public void addAutoReqToolTipInfoToFunction(string label, Function f, List reqs) {
string prefix = "auto requires " + label + " ";
string tip = "";
string sep = "";
foreach (var req in reqs) {
if (containsMatch) { // Pretty print the requirements
tip += sep + prefix + Printer.ExtendedExprToString(req) + ";";
} else {
tip += sep + prefix + Printer.ExprToString(req) + ";";
}
sep = "\n";
}
if (!tip.Equals("")) {
resolver.ReportAdditionalInformation(f.tok, tip, f.tok.val.Length);
if (DafnyOptions.O.AutoReqPrintFile != null) {
using (System.IO.TextWriter writer = new System.IO.StreamWriter(DafnyOptions.O.AutoReqPrintFile, true)) {
writer.WriteLine(f.Name);
writer.WriteLine("\t" + tip);
}
}
}
}
public void addAutoReqToolTipInfoToMethod(string label, Method method, List reqs) {
string tip = "";
foreach (var req in reqs) {
string prefix = "auto ";
if (req.IsFree) {
prefix += "free ";
}
prefix += " requires " + label + " ";
if (containsMatch) { // Pretty print the requirements
tip += prefix + Printer.ExtendedExprToString(req.E) + ";\n";
} else {
tip += prefix + Printer.ExprToString(req.E) + ";\n";
}
}
if (!tip.Equals("")) {
resolver.ReportAdditionalInformation(method.tok, tip, method.tok.val.Length);
if (DafnyOptions.O.AutoReqPrintFile != null) {
using (System.IO.TextWriter writer = new System.IO.StreamWriter(DafnyOptions.O.AutoReqPrintFile, true)) {
writer.WriteLine(method.Name);
writer.WriteLine("\t" + tip);
}
}
}
}
// Stitch a list of expressions together with logical ands
Expression andify(Bpl.IToken tok, List exprs) {
Expression ret = Expression.CreateBoolLiteral(tok, true);
foreach (var expr in exprs) {
ret = Expression.CreateAnd(ret, expr);
}
return ret;
}
List gatherReqs(Function f, List args, Expression f_this) {
List translated_f_reqs = new List();
if (f.Req.Count > 0) {
Dictionary substMap = new Dictionary();
Dictionary typeMap = new Dictionary();
for (int i = 0; i < f.Formals.Count; i++) {
substMap.Add(f.Formals[i], args[i]);
}
foreach (var req in f.Req) {
Translator.Substituter sub = new Translator.Substituter(f_this, substMap, typeMap, null);
translated_f_reqs.Add(sub.Substitute(req));
}
}
return translated_f_reqs;
}
List generateAutoReqs(Expression expr) {
List reqs = new List();
if (expr is LiteralExpr) {
} else if (expr is ThisExpr) {
} else if (expr is IdentifierExpr) {
} else if (expr is SetDisplayExpr) {
SetDisplayExpr e = (SetDisplayExpr)expr;
foreach (var elt in e.Elements) {
reqs.AddRange(generateAutoReqs(elt));
}
} else if (expr is MultiSetDisplayExpr) {
MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;
foreach (var elt in e.Elements) {
reqs.AddRange(generateAutoReqs(elt));
}
} else if (expr is SeqDisplayExpr) {
SeqDisplayExpr e = (SeqDisplayExpr)expr;
foreach (var elt in e.Elements) {
reqs.AddRange(generateAutoReqs(elt));
}
} else if (expr is MapDisplayExpr) {
MapDisplayExpr e = (MapDisplayExpr)expr;
foreach (ExpressionPair p in e.Elements) {
reqs.AddRange(generateAutoReqs(p.A));
reqs.AddRange(generateAutoReqs(p.B));
}
} else if (expr is MemberSelectExpr) {
MemberSelectExpr e = (MemberSelectExpr)expr;
Contract.Assert(e.Member != null && e.Member is Field);
reqs.AddRange(generateAutoReqs(e.Obj));
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
reqs.AddRange(generateAutoReqs(e.Seq));
if (e.E0 != null) {
reqs.AddRange(generateAutoReqs(e.E0));
}
if (e.E1 != null) {
reqs.AddRange(generateAutoReqs(e.E1));
}
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
reqs.AddRange(generateAutoReqs(e.Seq));
reqs.AddRange(generateAutoReqs(e.Index));
reqs.AddRange(generateAutoReqs(e.Value));
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
// All of the arguments need to be satisfied
foreach (var arg in e.Args) {
reqs.AddRange(generateAutoReqs(arg));
}
if (parentFunction != null && ModuleDefinition.InSameSCC(e.Function, parentFunction)) {
// We're making a call within the same SCC, so don't descend into this function
} else {
reqs.AddRange(gatherReqs(e.Function, e.Args, e.Receiver));
}
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved
for (int i = 0; i < dtv.Arguments.Count; i++) {
Expression arg = dtv.Arguments[i];
reqs.AddRange(generateAutoReqs(arg));
}
} else if (expr is OldExpr) {
} else if (expr is MatchExpr) {
MatchExpr e = (MatchExpr)expr;
containsMatch = true;
reqs.AddRange(generateAutoReqs(e.Source));
List newMatches = new List();
foreach (MatchCaseExpr caseExpr in e.Cases) {
//MatchCaseExpr c = new MatchCaseExpr(caseExpr.tok, caseExpr.Id, caseExpr.Arguments, andify(caseExpr.tok, generateAutoReqs(caseExpr.Body)));
//c.Ctor = caseExpr.Ctor; // resolve here
MatchCaseExpr c = Expression.CreateMatchCase(caseExpr, andify(caseExpr.tok, generateAutoReqs(caseExpr.Body)));
newMatches.Add(c);
}
reqs.Add(Expression.CreateMatch(e.tok, e.Source, newMatches, e.Type));
} else if (expr is MultiSetFormingExpr) {
MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
reqs.AddRange(generateAutoReqs(e.E));
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
Expression arg = e.E;
reqs.AddRange(generateAutoReqs(arg));
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
switch (e.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.Imp:
case BinaryExpr.ResolvedOpcode.And:
reqs.AddRange(generateAutoReqs(e.E0));
foreach (var req in generateAutoReqs(e.E1)) {
// We only care about this req if E0 is true, since And short-circuits
reqs.Add(Expression.CreateImplies(e.E0, req));
}
break;
case BinaryExpr.ResolvedOpcode.Or:
reqs.AddRange(generateAutoReqs(e.E0));
foreach (var req in generateAutoReqs(e.E1)) {
// We only care about this req if E0 is false, since Or short-circuits
reqs.Add(Expression.CreateImplies(Expression.CreateNot(e.E1.tok, e.E0), req));
}
break;
default:
reqs.AddRange(generateAutoReqs(e.E0));
reqs.AddRange(generateAutoReqs(e.E1));
break;
}
} else if (expr is TernaryExpr) {
var e = (TernaryExpr)expr;
reqs.AddRange(generateAutoReqs(e.E0));
reqs.AddRange(generateAutoReqs(e.E1));
reqs.AddRange(generateAutoReqs(e.E2));
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
if (e.Exact) {
foreach (var rhs in e.RHSs) {
reqs.AddRange(generateAutoReqs(rhs));
}
var new_reqs = generateAutoReqs(e.Body);
if (new_reqs.Count > 0) {
reqs.Add(Expression.CreateLet(e.tok, e.LHSs, e.RHSs, andify(e.tok, new_reqs), e.Exact));
}
} else {
// TODO: Still need to figure out what the right choice is here:
// Given: var x :| g(x); f(x, y) do we:
// 1) Update the original statement to be: var x :| g(x) && WP(f(x,y)); f(x, y)
// 2) Add forall x :: g(x) ==> WP(f(x, y)) to the function's requirements
// 3) Current option -- do nothing. Up to the spec writer to fix
}
} else if (expr is NamedExpr) {
reqs.AddRange(generateAutoReqs(((NamedExpr)expr).Body));
} else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
// See LetExpr for issues with the e.Range
var auto_reqs = generateAutoReqs(e.Term);
if (auto_reqs.Count > 0) {
Expression allReqsSatisfied = andify(e.Term.tok, auto_reqs);
Expression allReqsSatisfiedAndTerm = Expression.CreateAnd(allReqsSatisfied, e.Term);
e.UpdateTerm(allReqsSatisfiedAndTerm);
resolver.ReportAdditionalInformation(e.tok, "autoreq added (" + Printer.ExtendedExprToString(allReqsSatisfied) + ") &&", e.tok.val.Length);
}
} else if (expr is SetComprehension) {
var e = (SetComprehension)expr;
// Translate "set xs | R :: T"
// See LetExpr for issues with the e.Range
//reqs.AddRange(generateAutoReqs(e.Range));
var auto_reqs = generateAutoReqs(e.Term);
if (auto_reqs.Count > 0) {
reqs.Add(Expression.CreateQuantifier(new ForallExpr(e.tok, new List(), e.BoundVars, e.Range, andify(e.Term.tok, auto_reqs), e.Attributes), true));
}
} else if (expr is MapComprehension) {
var e = (MapComprehension)expr;
// Translate "map x | R :: T" into
// See LetExpr for issues with the e.Range
//reqs.AddRange(generateAutoReqs(e.Range));
var auto_reqs = generateAutoReqs(e.Term);
if (auto_reqs.Count > 0) {
reqs.Add(Expression.CreateQuantifier(new ForallExpr(e.tok, new List(), e.BoundVars, e.Range, andify(e.Term.tok, auto_reqs), e.Attributes), true));
}
} else if (expr is StmtExpr) {
var e = (StmtExpr)expr;
reqs.AddRange(generateAutoReqs(e.E));
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
reqs.AddRange(generateAutoReqs(e.Test));
reqs.Add(Expression.CreateITE(e.Test, andify(e.Thn.tok, generateAutoReqs(e.Thn)), andify(e.Els.tok, generateAutoReqs(e.Els))));
} else if (expr is ConcreteSyntaxExpression) {
var e = (ConcreteSyntaxExpression)expr;
reqs.AddRange(generateAutoReqs(e.ResolvedExpression));
} else {
//Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
return reqs;
}
}
///
/// Replace all occurrences of attribute {:timeLimitMultiplier X} with {:timeLimit Y}
/// where Y = X*default-time-limit or Y = X*command-line-time-limit
///
public class TimeLimitRewriter : IRewriter
{
public void PreResolve(ModuleDefinition m) {
foreach (var d in m.TopLevelDecls) {
if (d is ClassDecl) {
var c = (ClassDecl)d;
foreach (MemberDecl member in c.Members) {
if (member is Function || member is Method) {
// Check for the timeLimitMultiplier attribute
if (Attributes.Contains(member.Attributes, "timeLimitMultiplier")) {
Attributes attrs = member.Attributes;
for (; attrs != null; attrs = attrs.Prev) {
if (attrs.Name == "timeLimitMultiplier") {
if (attrs.Args.Count == 1 && attrs.Args[0] is LiteralExpr) {
var arg = attrs.Args[0] as LiteralExpr;
System.Numerics.BigInteger value = (System.Numerics.BigInteger)arg.Value;
if (value.Sign > 0) {
int current_limit = DafnyOptions.O.ProverKillTime > 0 ? DafnyOptions.O.ProverKillTime : 10; // Default to 10 seconds
attrs.Args[0] = new LiteralExpr(attrs.Args[0].tok, value * current_limit);
attrs.Name = "timeLimit";
}
}
}
}
}
}
}
}
}
}
public void PostResolve(ModuleDefinition m)
{
// Nothing to do here
}
public void PostCyclicityResolve(ModuleDefinition m) {
// Nothing to do here
}
}
}