summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/DafnyAst.cs2
-rw-r--r--Source/Dafny/RefinementTransformer.cs10
-rw-r--r--Source/Dafny/Resolver.cs9
-rw-r--r--Source/Dafny/Rewriter.cs118
4 files changed, 76 insertions, 63 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 3cc2e420..5382047e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1236,6 +1236,7 @@ namespace Microsoft.Dafny {
public readonly bool IsStatic;
public readonly bool IsGhost;
public TopLevelDecl EnclosingClass; // filled in during resolution
+ public MemberDecl RefinementBase; // filled in during the pre-resolution refinement transformation; null if the member is new here
public MemberDecl(IToken tok, string name, bool isStatic, bool isGhost, Attributes attributes)
: base(tok, name, attributes) {
@@ -3262,7 +3263,6 @@ namespace Microsoft.Dafny {
: base(tok) {
Contract.Requires(tok != null);
this.Value = b;
-
}
}
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index d045426d..91f79a23 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -629,6 +629,8 @@ namespace Microsoft.Dafny
} else {
reporter.Error(nwMember, "a field declaration ({0}) in a refining class ({1}) must replace a field in the refinement base", nwMember.Name, nw.Name);
}
+ nwMember.RefinementBase = member;
+
} else if (nwMember is Function) {
var f = (Function)nwMember;
bool isPredicate = f is Predicate;
@@ -676,7 +678,9 @@ namespace Microsoft.Dafny
} else if (f.Body != null) {
reporter.Error(nwMember, "a refining function is not allowed to extend/change the body");
}
- nw.Members[index] = CloneFunction(f.tok, prevFunction, f.IsGhost, f.Ens, moreBody, replacementBody, prevFunction.Body == null, f.Attributes);
+ var newFn = CloneFunction(f.tok, prevFunction, f.IsGhost, f.Ens, moreBody, replacementBody, prevFunction.Body == null, f.Attributes);
+ newFn.RefinementBase = member;
+ nw.Members[index] = newFn;
}
} else {
@@ -726,7 +730,9 @@ namespace Microsoft.Dafny
replacementBody = MergeBlockStmt(replacementBody, prevMethod.Body);
}
}
- nw.Members[index] = CloneMethod(prevMethod, m.Ens, decreases, replacementBody, prevMethod.Body == null, m.Attributes);
+ var newM = CloneMethod(prevMethod, m.Ens, decreases, replacementBody, prevMethod.Body == null, m.Attributes);
+ newM.RefinementBase = member;
+ nw.Members[index] = newM;
}
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index ef1f3e33..5883f4b5 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -185,10 +185,9 @@ namespace Microsoft.Dafny
// global variable moduleInfo. Then the signatures of the module members are resolved, followed
// by the bodies.
var literalDecl = (LiteralModuleDecl)decl;
- var m = (literalDecl).ModuleDef;
+ var m = literalDecl.ModuleDef;
var errorCount = ErrorCount;
- rewriter.PreResolve(m);
ModuleSignature refinedSig = null;
if (m.RefinementBaseRoot != null) {
if (ResolvePath(m.RefinementBaseRoot, m.RefinementBaseName, out refinedSig)) {
@@ -202,6 +201,9 @@ namespace Microsoft.Dafny
Error(m.RefinementBaseName[0], "module ({0}) named as refinement base does not exist", Util.Comma(".", m.RefinementBaseName, x => x.val));
}
}
+ if (errorCount == ErrorCount) {
+ rewriter.PreResolve(m);
+ }
literalDecl.Signature = RegisterTopLevelDecls(m, true);
literalDecl.Signature.Refines = refinedSig;
var sig = literalDecl.Signature;
@@ -4451,10 +4453,9 @@ namespace Microsoft.Dafny
Contract.Requires(obj != null);
Contract.Requires(field != null);
Contract.Requires(obj.Type != null); // "obj" is required to be resolved
- Contract.Requires(typeSubstMap != null);
var e = new FieldSelectExpr(tok, obj, field.Name);
e.Field = field; // resolve here
- e.Type = SubstType(field.Type, typeSubstMap); // resolve here
+ e.Type = typeSubstMap == null ? field.Type : SubstType(field.Type, typeSubstMap); // resolve here
return e;
}
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index c95be2f4..f248fae2 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -90,6 +90,11 @@ namespace Microsoft.Dafny
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);
@@ -188,17 +193,24 @@ namespace Microsoft.Dafny
if (member is Function && member.Name == "Valid" && !member.IsStatic) {
var valid = (Function)member;
if (valid.IsGhost && valid.ResultType is BoolType) {
- var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, self, Repr); // this in Repr
- var c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NotInSet, cNull, Repr); // null !in Repr
- var c = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c0, c1);
+ 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) {
- var F = new FieldSelectExpr(tok, implicitSelf, ff.Item1.Name);
- F.Field = ff.Item1;
- F.Type = ff.Item1.Type;
-
- c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NeqCommon, F, cNull);
- c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, F, Repr);
+ if (ff.Item1.RefinementBase != null) {
+ // the field has been inherited from a refined module, so don't include it here
+ continue;
+ }
+ var F = Resolver.NewFieldSelectExpr(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 {
@@ -222,46 +234,44 @@ namespace Microsoft.Dafny
} else if (member is Constructor) {
var ctor = (Constructor)member;
- if (ctor.Body == null) {
- ctor.Body = new BlockStmt(tok, new List<Statement>());
- }
- // TODO: these assignments should be included on every return path
- var bodyStatements = ((BlockStmt)ctor.Body).Body;
- // Repr := {this};
- var e = new SetDisplayExpr(tok, new List<Expression>() { self });
- e.Type = new SetType(new ObjectType());
- Statement s = new AssignStmt(tok, Repr, new ExprRhs(e));
- s.IsGhost = true;
- bodyStatements.Add(s);
+ if (ctor.Body != null) {
+ var bodyStatements = ((BlockStmt)ctor.Body).Body;
+ // Repr := {this};
+ var e = new SetDisplayExpr(tok, new List<Expression>() { self });
+ e.Type = new SetType(new ObjectType());
+ Statement s = new AssignStmt(tok, Repr, new ExprRhs(e));
+ s.IsGhost = true;
+ bodyStatements.Add(s);
- AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);
+ AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);
+ }
} else if (member is Method && !member.IsStatic) {
var m = (Method)member;
if (Valid != null && !IsSimpleQueryMethod(m)) {
- // modifies Repr;
- m.Mod.Expressions.Add(new FrameExpression(Repr.tok, Repr, null));
- // ensures Valid();
- var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List<Expression>());
- valid.Function = Valid;
- valid.Type = Type.Bool;
- 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 FreshExpr(tok, e1);
- freshness.Type = Type.Bool;
- m.Ens.Insert(1, new MaybeFreeExpression(freshness));
+ 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<Expression>());
+ valid.Function = Valid;
+ valid.Type = Type.Bool;
+ 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 FreshExpr(tok, e1);
+ freshness.Type = Type.Bool;
+ m.Ens.Insert(1, new MaybeFreeExpression(freshness));
+ }
- if (m.Body == null) {
- m.Body = new BlockStmt(tok, new List<Statement>());
+ if (m.Body != null) {
+ var bodyStatements = ((BlockStmt)m.Body).Body;
+ AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);
}
- // TODO: these assignments should be included on every return path
- var bodyStatements = ((BlockStmt)m.Body).Body;
- AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);
}
}
}
@@ -269,27 +279,23 @@ namespace Microsoft.Dafny
void AddSubobjectReprs(Boogie.IToken tok, List<Tuple<Field, Field>> subobjects, List<Statement> 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 = new FieldSelectExpr(tok, implicitSelf, ff.Item1.Name);
- F.Field = ff.Item1;
- F.Type = ff.Item1.Type;
-
+ var F = Resolver.NewFieldSelectExpr(tok, implicitSelf, ff.Item1, null); // create a resolved FieldSelectExpr
Expression e = new SetDisplayExpr(tok, new List<Expression>() { F });
- e.Type = new SetType(new ObjectType());
+ e.Type = new SetType(new ObjectType()); // resolve here
var rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, Repr, e);
- rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;
- rhs.Type = Repr.Type;
+ 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 = new FieldSelectExpr(tok, F, ff.Item2.Name);
- FRepr.Field = ff.Item2;
- FRepr.Type = ff.Item2.Type;
+ var FRepr = Resolver.NewFieldSelectExpr(tok, F, ff.Item2, null); // create resolved FieldSelectExpr
rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, rhs, FRepr);
- rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;
- rhs.Type = Repr.Type;
+ rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union; // resolve here
+ rhs.Type = Repr.Type; // resolve here
}
// Repr := Repr + ...;
Statement s = new AssignStmt(tok, Repr, new ExprRhs(rhs));
@@ -334,8 +340,8 @@ namespace Microsoft.Dafny
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;
- p.Type = Type.Bool;
+ p.ResolvedOp = rop; // resolve here
+ p.Type = Type.Bool; // resolve here
return p;
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 18:03:35 +0000