From 1bf46169e86ae8e97ac32831092bb705afc91124 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 16 Sep 2021 14:54:34 -0700 Subject: [PATCH 01/55] First step, adding to parser and Method model --- Source/Dafny/AST/DafnyAst.cs | 45 ++++++++++++++++++--------- Source/Dafny/Cloner.cs | 13 ++++---- Source/Dafny/Dafny.atg | 21 +++++++------ Source/Dafny/RefinementTransformer.cs | 13 ++++---- Source/Dafny/Resolver.cs | 6 ++-- Source/Dafny/Rewriter.cs | 4 +-- 6 files changed, 63 insertions(+), 39 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index b27330080aa..2d9738bb99e 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -6446,6 +6446,7 @@ public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext { public readonly List Ins; public readonly List Outs; public readonly List Req; + public readonly List Reads; public readonly Specification Mod; public readonly List Ens; public readonly Specification Decreases; @@ -6493,7 +6494,9 @@ public Method(IToken tok, string name, bool hasStaticKeyword, bool isGhost, [Captured] List typeArgs, [Captured] List ins, [Captured] List outs, - [Captured] List req, [Captured] Specification mod, + [Captured] List req, + [Captured] List reads, + [Captured] Specification mod, [Captured] List ens, [Captured] Specification decreases, [Captured] BlockStmt body, @@ -6505,12 +6508,14 @@ public Method(IToken tok, string name, Contract.Requires(cce.NonNullElements(ins)); Contract.Requires(cce.NonNullElements(outs)); Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(reads != null); Contract.Requires(mod != null); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(decreases != null); this.TypeArgs = typeArgs; this.Ins = ins; this.Outs = outs; + this.Reads = reads; this.Req = req; this.Mod = mod; this.Ens = ens; @@ -6599,12 +6604,14 @@ public Lemma(IToken tok, string name, bool hasStaticKeyword, [Captured] List typeArgs, [Captured] List ins, [Captured] List outs, - [Captured] List req, [Captured] Specification mod, + [Captured] List req, + [Captured] List reads, + [Captured] Specification mod, [Captured] List ens, [Captured] Specification decreases, [Captured] BlockStmt body, Attributes attributes, IToken signatureEllipsis) - : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { + : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { } } @@ -6615,12 +6622,13 @@ public TwoStateLemma(IToken tok, string name, [Captured] List typeArgs, [Captured] List ins, [Captured] List outs, [Captured] List req, + [Captured] List reads, [Captured] Specification mod, [Captured] List ens, [Captured] Specification decreases, [Captured] BlockStmt body, Attributes attributes, IToken signatureEllipsis) - : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { + : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(typeArgs != null); @@ -6660,12 +6668,14 @@ public List BodyProper { // second part of Body's statements public Constructor(IToken tok, string name, List typeArgs, List ins, - List req, [Captured] Specification mod, + List req, + List reads, + [Captured] Specification mod, List ens, Specification decreases, DividedBlockStmt body, Attributes attributes, IToken signatureEllipsis) - : base(tok, name, false, false, typeArgs, ins, new List(), req, mod, ens, decreases, body, attributes, signatureEllipsis) { + : base(tok, name, false, false, typeArgs, ins, new List(), req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); @@ -6692,9 +6702,10 @@ public class PrefixLemma : Method { public readonly ExtremeLemma ExtremeLemma; public PrefixLemma(IToken tok, string name, bool hasStaticKeyword, List typeArgs, Formal k, List ins, List outs, - List req, Specification mod, List ens, Specification decreases, + List req, List reads, Specification mod, + List ens, Specification decreases, BlockStmt body, Attributes attributes, ExtremeLemma extremeLemma) - : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, null) { + : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, null) { Contract.Requires(k != null); Contract.Requires(ins != null && 1 <= ins.Count && ins[0] == k); Contract.Requires(extremeLemma != null); @@ -6716,12 +6727,14 @@ public ExtremeLemma(IToken tok, string name, bool hasStaticKeyword, ExtremePredicate.KType typeOfK, List typeArgs, List ins, [Captured] List outs, - List req, [Captured] Specification mod, + List req, + List reads, + [Captured] Specification mod, List ens, Specification decreases, BlockStmt body, Attributes attributes, IToken signatureEllipsis) - : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { + : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); @@ -6742,12 +6755,14 @@ public LeastLemma(IToken tok, string name, bool hasStaticKeyword, ExtremePredicate.KType typeOfK, List typeArgs, List ins, [Captured] List outs, - List req, [Captured] Specification mod, + List req, + List reads, + [Captured] Specification mod, List ens, Specification decreases, BlockStmt body, Attributes attributes, IToken signatureEllipsis) - : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { + : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); @@ -6767,12 +6782,14 @@ public GreatestLemma(IToken tok, string name, bool hasStaticKeyword, ExtremePredicate.KType typeOfK, List typeArgs, List ins, [Captured] List outs, - List req, [Captured] Specification mod, + List req, + List reads, + [Captured] Specification mod, List ens, Specification decreases, BlockStmt body, Attributes attributes, IToken signatureEllipsis) - : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { + : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 2adeaa603e7..a4f30416227 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -790,6 +790,7 @@ public virtual Method CloneMethod(Method m) { var tps = m.TypeArgs.ConvertAll(CloneTypeParam); var ins = m.Ins.ConvertAll(CloneFormal); var req = m.Req.ConvertAll(CloneAttributedExpr); + var reads = m.Reads.ConvertAll(CloneFrameExpr); var mod = CloneSpecFrameExpr(m.Mod); var decreases = CloneSpecExpr(m.Decreases); @@ -799,23 +800,23 @@ public virtual Method CloneMethod(Method m) { if (m is Constructor) { return new Constructor(Tok(m.tok), m.Name, tps, ins, - req, mod, ens, decreases, (DividedBlockStmt)body, CloneAttributes(m.Attributes), null); + req, reads, mod, ens, decreases, (DividedBlockStmt)body, CloneAttributes(m.Attributes), null); } else if (m is LeastLemma) { return new LeastLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, ((LeastLemma)m).TypeOfK, tps, ins, m.Outs.ConvertAll(CloneFormal), - req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null); + req, reads, mod, ens, decreases, body, CloneAttributes(m.Attributes), null); } else if (m is GreatestLemma) { return new GreatestLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, ((GreatestLemma)m).TypeOfK, tps, ins, m.Outs.ConvertAll(CloneFormal), - req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null); + req, reads, mod, ens, decreases, body, CloneAttributes(m.Attributes), null); } else if (m is Lemma) { return new Lemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal), - req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null); + req, reads, mod, ens, decreases, body, CloneAttributes(m.Attributes), null); } else if (m is TwoStateLemma) { var two = (TwoStateLemma)m; return new TwoStateLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal), - req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null); + req, reads, mod, ens, decreases, body, CloneAttributes(m.Attributes), null); } else { return new Method(Tok(m.tok), m.Name, m.HasStaticKeyword, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal), - req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m.IsByMethod); + req, reads, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m.IsByMethod); } } diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index bb98e0c54c8..f4df8e5fef8 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1667,6 +1667,7 @@ MethodDecl List ins = new List(); List outs = new List(); List req = new List(); + List reads = new List(); List mod = new List(); List ens = new List(); List dec = new List(); @@ -1736,7 +1737,7 @@ MethodDecl | ellipsis (. signatureEllipsis = t; .) ) MethodSpec + req, reads, mod, ens, dec, ref decAttrs, ref modAttrs, caption, isConstructor> [ IF(isConstructor) (. DividedBlockStmt dividedBody; .) DividedBlockStmt @@ -1746,23 +1747,23 @@ MethodDecl (. IToken tok = id; if (isConstructor) { m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins, - req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), (DividedBlockStmt)body, attrs, signatureEllipsis); + req, reads, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), (DividedBlockStmt)body, attrs, signatureEllipsis); } else if (isLeastLemma) { m = new LeastLemma(tok, id.val, dmod.IsStatic, kType, typeArgs, ins, outs, - req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); + req, reads, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else if (isGreatestLemma) { m = new GreatestLemma(tok, id.val, dmod.IsStatic, kType, typeArgs, ins, outs, - req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); + req, reads, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else if (isLemma) { m = new Lemma(tok, id.val, dmod.IsStatic, typeArgs, ins, outs, - req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); + req, reads, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else if (isTwoStateLemma) { m = new TwoStateLemma(tok, id.val, dmod.IsStatic, typeArgs, ins, outs, - req, new Specification(mod, modAttrs), + req, reads, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else { m = new Method(tok, id.val, dmod.IsStatic, dmod.IsGhost, typeArgs, ins, outs, - req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); + req, reads, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } m.BodyStartTok = bodyStart; m.BodyEndTok = bodyEnd; @@ -1852,15 +1853,17 @@ InvariantClause<. List invariants.> = . /*------------------------------------------------------------------------*/ -MethodSpec<.bool isGhost, List req, List mod, List ens, +MethodSpec<.bool isGhost, List req, List reads, List mod, List ens, List decreases, ref Attributes decAttrs, ref Attributes modAttrs, string caption, bool performThisDeprecatedCheck.> = (. Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases)); .) SYNC - { ModifiesClause + { ReadsClause + | ModifiesClause | RequiresClause | EnsuresClause | DecreasesClause diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 6797a39fb85..d8e0760843f 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -479,6 +479,7 @@ Method CloneMethod(Method m, List moreEnsures, Specificati var tps = m.TypeArgs.ConvertAll(refinementCloner.CloneTypeParam); var ins = m.Ins.ConvertAll(refinementCloner.CloneFormal); var req = m.Req.ConvertAll(refinementCloner.CloneAttributedExpr); + var reads = m.Reads.ConvertAll(refinementCloner.CloneFrameExpr); var mod = refinementCloner.CloneSpecFrameExpr(m.Mod); List ens; @@ -493,25 +494,25 @@ Method CloneMethod(Method m, List moreEnsures, Specificati if (m is Constructor) { var dividedBody = (DividedBlockStmt)newBody ?? refinementCloner.CloneDividedBlockStmt((DividedBlockStmt)m.BodyForRefinement); return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, tps, ins, - req, mod, ens, decreases, dividedBody, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); + req, reads, mod, ens, decreases, dividedBody, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); } var body = newBody ?? refinementCloner.CloneBlockStmt(m.BodyForRefinement); if (m is LeastLemma) { return new LeastLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, ((LeastLemma)m).TypeOfK, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal), - req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); + req, reads, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); } else if (m is GreatestLemma) { return new GreatestLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, ((GreatestLemma)m).TypeOfK, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal), - req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); + req, reads, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); } else if (m is Lemma) { return new Lemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal), - req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); + req, reads, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); } else if (m is TwoStateLemma) { var two = (TwoStateLemma)m; return new TwoStateLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal), - req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); + req, reads, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); } else { return new Method(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, m.IsGhost, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal), - req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m.IsByMethod); + req, reads, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m.IsByMethod); } } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a0df51fe8a3..a1d29441c59 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2001,6 +2001,7 @@ ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImport // --- here comes the constructor var init = new Constructor(iter.tok, "_ctor", new List(), iter.Ins, new List(), + new List(), new Specification(new List(), null), new List(), new Specification(new List(), null), @@ -2017,6 +2018,7 @@ ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImport var moveNext = new Method(iter.tok, "MoveNext", false, false, new List(), new List(), new List() { new Formal(iter.tok, "more", Type.Bool, false, false, null) }, new List(), + new List(), new Specification(new List(), null), new List(), new Specification(new List(), null), @@ -2268,7 +2270,7 @@ void RegisterMembers(ModuleDefinition moduleDef, TopLevelDeclWithMembers cl, : com.Ens.ConvertAll(cloner.CloneAttributedExpr); com.PrefixLemma = new PrefixLemma(com.tok, extraName, com.HasStaticKeyword, com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal), - req, cloner.CloneSpecFrameExpr(com.Mod), ens, + req, com.Reads.ConvertAll(cloner.CloneFrameExpr), cloner.CloneSpecFrameExpr(com.Mod), ens, new Specification(decr, null), null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the greatest lemma is known cloner.CloneAttributes(com.Attributes), com); @@ -2302,7 +2304,7 @@ void RegisterByMethod(Function f) { var post = new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq, r, fn)); var method = new Method(tok, f.Name, f.HasStaticKeyword, false, f.TypeArgs, f.Formals, new List() { resultVar }, - f.Req, new Specification(new List(), null), new List() { post }, f.Decreases, + f.Req, f.Reads, new Specification(new List(), null), new List() { post }, f.Decreases, f.ByMethodBody, f.Attributes, null, true); Contract.Assert(f.ByMethodDecl == null); method.InheritVisibility(f); diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 1d62f7b3170..9a6a1a5a3d6 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -1020,11 +1020,11 @@ private void RewriteOpaqueFunctionUseFuel(Function f, List newDecls) Method reveal; if (f is TwoStateFunction) { reveal = new TwoStateLemma(f.tok, "reveal_" + f.Name, f.HasStaticKeyword, new List(), new List(), new List(), new List(), - new Specification(new List(), null), /* newEnsuresList*/new List(), + new List(), new Specification(new List(), null), /* newEnsuresList*/new List(), new Specification(new List(), null), null, lemma_attrs, null); } else { 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 List(), + new List(), new Specification(new List(), null), /* newEnsuresList*/new List(), new Specification(new List(), null), null, lemma_attrs, null); } newDecls.Add(reveal); From 6cf7685ec1002c56c0eabc7c3a4d552f218acc84 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 17 Sep 2021 11:40:03 -0700 Subject: [PATCH 02/55] Split TheFrame into ReadsFrame and ModifiesFrame --- .../Translator.ExpressionTranslator.cs | 58 ++++++++++----- .../Dafny/Verifier/Translator.TrStatement.cs | 18 ++--- Source/Dafny/Verifier/Translator.cs | 74 ++++++++++--------- 3 files changed, 85 insertions(+), 65 deletions(-) diff --git a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs index 8b6a3dc69e3..7093f79a2a4 100644 --- a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs @@ -20,7 +20,8 @@ public Boogie.Expr HeapExpr { public readonly PredefinedDecls predef; public readonly Translator translator; public readonly string This; - public readonly string modifiesFrame; // the name of the context's frame variable. + public readonly string readsFrame; // the name of the context's frame variable for reading state. + public readonly string modifiesFrame; // the name of the context's frame variable for writing state. readonly Function applyLimited_CurrentFunction; public readonly FuelSetting layerInterCluster; public readonly FuelSetting layerIntraCluster = null; // a value of null says to do the same as for inter-cluster calls @@ -46,7 +47,7 @@ void ObjectInvariant() { /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in. /// ExpressionTranslator(Translator translator, PredefinedDecls predef, Boogie.Expr heap, string thisVar, - Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, string modifiesFrame, bool stripLits) { + Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, string readsFrame, string modifiesFrame, bool stripLits) { Contract.Requires(translator != null); Contract.Requires(predef != null); @@ -64,6 +65,7 @@ void ObjectInvariant() { } else { this.layerIntraCluster = layerIntraCluster; } + this.readsFrame = readsFrame; this.modifiesFrame = modifiesFrame; this.stripLits = stripLits; } @@ -93,19 +95,19 @@ public ExpressionTranslator(Translator translator, PredefinedDecls predef, Boogi } public ExpressionTranslator(Translator translator, PredefinedDecls predef, Boogie.Expr heap, string thisVar) - : this(translator, predef, heap, thisVar, null, new FuelSetting(translator, 1), null, "$_Frame", false) { + : this(translator, predef, heap, thisVar, null, new FuelSetting(translator, 1), null, "$_ReadsFrame", "$_ModifiesFrame", false) { Contract.Requires(translator != null); Contract.Requires(predef != null); Contract.Requires(thisVar != null); } public ExpressionTranslator(ExpressionTranslator etran, Boogie.Expr heap) - : this(etran.translator, etran.predef, heap, etran.This, etran.applyLimited_CurrentFunction, etran.layerInterCluster, etran.layerIntraCluster, etran.modifiesFrame, etran.stripLits) { + : this(etran.translator, etran.predef, heap, etran.This, etran.applyLimited_CurrentFunction, etran.layerInterCluster, etran.layerIntraCluster, etran.readsFrame, etran.modifiesFrame, etran.stripLits) { Contract.Requires(etran != null); } - public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame) - : this(etran.translator, etran.predef, etran.HeapExpr, etran.This, etran.applyLimited_CurrentFunction, etran.layerInterCluster, etran.layerIntraCluster, modifiesFrame, etran.stripLits) { + public ExpressionTranslator(ExpressionTranslator etran, string readsFrame, string modifiesFrame) + : this(etran.translator, etran.predef, etran.HeapExpr, etran.This, etran.applyLimited_CurrentFunction, etran.layerInterCluster, etran.layerIntraCluster, readsFrame, modifiesFrame, etran.stripLits) { Contract.Requires(etran != null); Contract.Requires(modifiesFrame != null); } @@ -116,7 +118,7 @@ public ExpressionTranslator Old { Contract.Ensures(Contract.Result() != null); if (oldEtran == null) { - oldEtran = new ExpressionTranslator(translator, predef, new Boogie.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, modifiesFrame, stripLits); + oldEtran = new ExpressionTranslator(translator, predef, new Boogie.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits); oldEtran.oldEtran = oldEtran; } return oldEtran; @@ -129,7 +131,7 @@ public ExpressionTranslator OldAt(Label/*?*/ label) { return Old; } var heapAt = new Boogie.IdentifierExpr(Token.NoToken, "$Heap_at_" + label.AssignUniqueId(translator.CurrentIdGenerator), predef.HeapType); - return new ExpressionTranslator(translator, predef, heapAt, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, modifiesFrame, stripLits); + return new ExpressionTranslator(translator, predef, heapAt, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits); } public bool UsesOldHeap { @@ -143,7 +145,7 @@ public ExpressionTranslator WithLayer(Boogie.Expr layerArgument) { Contract.Requires(layerArgument != null); Contract.Ensures(Contract.Result() != null); - return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, null, new FuelSetting(translator, 0, layerArgument), new FuelSetting(translator, 0, layerArgument), modifiesFrame, stripLits); + return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, null, new FuelSetting(translator, 0, layerArgument), new FuelSetting(translator, 0, layerArgument), readsFrame, modifiesFrame, stripLits); } public ExpressionTranslator WithCustomFuelSetting(CustomFuelSettings customSettings) { @@ -151,7 +153,7 @@ public ExpressionTranslator WithCustomFuelSetting(CustomFuelSettings customSetti Contract.Requires(customSettings != null); Contract.Ensures(Contract.Result() != null); - return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, null, layerInterCluster.WithContext(customSettings), layerIntraCluster.WithContext(customSettings), modifiesFrame, stripLits); + return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, null, layerInterCluster.WithContext(customSettings), layerIntraCluster.WithContext(customSettings), readsFrame, modifiesFrame, stripLits); } public ExpressionTranslator ReplaceLayer(Boogie.Expr layerArgument) { @@ -159,12 +161,12 @@ public ExpressionTranslator ReplaceLayer(Boogie.Expr layerArgument) { Contract.Requires(layerArgument != null); Contract.Ensures(Contract.Result() != null); - return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster.WithLayer(layerArgument), layerIntraCluster.WithLayer(layerArgument), modifiesFrame, stripLits); + return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster.WithLayer(layerArgument), layerIntraCluster.WithLayer(layerArgument), readsFrame, modifiesFrame, stripLits); } public ExpressionTranslator WithNoLits() { Contract.Ensures(Contract.Result() != null); - return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, modifiesFrame, true); + return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, true); } public ExpressionTranslator LimitedFunctions(Function applyLimited_CurrentFunction, Boogie.Expr layerArgument) { @@ -172,36 +174,52 @@ public ExpressionTranslator LimitedFunctions(Function applyLimited_CurrentFuncti Contract.Requires(layerArgument != null); Contract.Ensures(Contract.Result() != null); - return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, applyLimited_CurrentFunction, /* layerArgument */ layerInterCluster, new FuelSetting(translator, 0, layerArgument), modifiesFrame, stripLits); + return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, applyLimited_CurrentFunction, /* layerArgument */ layerInterCluster, new FuelSetting(translator, 0, layerArgument), readsFrame, modifiesFrame, stripLits); } public ExpressionTranslator LayerOffset(int offset) { Contract.Requires(0 <= offset); Contract.Ensures(Contract.Result() != null); - return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster.Offset(offset), layerIntraCluster, modifiesFrame, stripLits); + return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster.Offset(offset), layerIntraCluster, readsFrame, modifiesFrame, stripLits); } public ExpressionTranslator DecreaseFuel(int offset) { Contract.Requires(0 <= offset); Contract.Ensures(Contract.Result() != null); - return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster.Decrease(offset), layerIntraCluster, modifiesFrame, stripLits); + return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster.Decrease(offset), layerIntraCluster, readsFrame, modifiesFrame, stripLits); } private static ExpressionTranslator CloneExpressionTranslator(ExpressionTranslator orig, Translator translator, PredefinedDecls predef, Boogie.Expr heap, string thisVar, - Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, string modifiesFrame, bool stripLits) { - var et = new ExpressionTranslator(translator, predef, heap, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, modifiesFrame, stripLits); + Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, string readsFrame, string modifiesFrame, bool stripLits) { + var et = new ExpressionTranslator(translator, predef, heap, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits); if (orig.oldEtran != null) { - var etOld = new ExpressionTranslator(translator, predef, orig.Old.HeapExpr, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, modifiesFrame, stripLits); + var etOld = new ExpressionTranslator(translator, predef, orig.Old.HeapExpr, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits); etOld.oldEtran = etOld; et.oldEtran = etOld; } return et; } - public Boogie.IdentifierExpr TheFrame(IToken tok) { + public Boogie.IdentifierExpr ReadsFrame(IToken tok) { + Contract.Requires(tok != null); + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result().Type != null); + + return Frame(tok, this.readsFrame); + } + + public Boogie.IdentifierExpr ModifiesFrame(IToken tok) { + Contract.Requires(tok != null); + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result().Type != null); + + return Frame(tok, this.modifiesFrame); + } + + private Boogie.IdentifierExpr Frame(IToken tok, string frameName) { Contract.Requires(tok != null); Contract.Ensures(Contract.Result() != null); Contract.Ensures(Contract.Result().Type != null); @@ -209,7 +227,7 @@ public Boogie.IdentifierExpr TheFrame(IToken tok) { Boogie.TypeVariable alpha = new Boogie.TypeVariable(tok, "beta"); Boogie.Type fieldAlpha = predef.FieldName(tok, alpha); Boogie.Type ty = new Boogie.MapType(tok, new List { alpha }, new List { predef.RefType, fieldAlpha }, Boogie.Type.Bool); - return new Boogie.IdentifierExpr(tok, this.modifiesFrame, ty); + return new Boogie.IdentifierExpr(tok, frameName, ty); } public Boogie.IdentifierExpr Tick() { diff --git a/Source/Dafny/Verifier/Translator.TrStatement.cs b/Source/Dafny/Verifier/Translator.TrStatement.cs index e3afd6252fb..46fffa2d214 100644 --- a/Source/Dafny/Verifier/Translator.TrStatement.cs +++ b/Source/Dafny/Verifier/Translator.TrStatement.cs @@ -584,13 +584,13 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List(), tySubst); CheckFrameSubset(tok, callee.Mod.Expressions.ConvertAll(s.SubstFrameExpr), - receiver, substMap, etran, builder, "call may violate context's modifies clause", null); + receiver, substMap, etran, etran.ModifiesFrame(tok), builder, "call may violate context's modifies clause", null); } // Check termination diff --git a/Source/Dafny/Verifier/Translator.cs b/Source/Dafny/Verifier/Translator.cs index 2fc56129629..8738f4f58bd 100644 --- a/Source/Dafny/Verifier/Translator.cs +++ b/Source/Dafny/Verifier/Translator.cs @@ -2479,7 +2479,7 @@ void AddIteratorWellformed(IteratorDecl iter, Procedure proc) { var builder = new BoogieStmtListBuilder(this); var etran = new ExpressionTranslator(this, predef, iter.tok); var localVariables = new List(); - GenerateIteratorImplPrelude(iter, inParams, new List(), builder, localVariables); + GenerateIteratorImplPrelude(iter, inParams, new List(), builder, localVariables, etran); // check well-formedness of any default-value expressions (before assuming preconditions) foreach (var formal in iter.Ins.Where(formal => formal.DefaultValue != null)) { @@ -2618,7 +2618,7 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { var builder = new BoogieStmtListBuilder(this); var etran = new ExpressionTranslator(this, predef, iter.tok); var localVariables = new List(); - GenerateIteratorImplPrelude(iter, inParams, new List(), builder, localVariables); + GenerateIteratorImplPrelude(iter, inParams, new List(), builder, localVariables, etran); // add locals for the yield-history variables and the extra variables // Assume the precondition and postconditions of the iterator constructor method @@ -4338,7 +4338,7 @@ void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc) { var etran = new ExpressionTranslator(this, predef, m.tok); InitializeFuelConstant(m.tok, builder, etran); var localVariables = new List(); - GenerateImplPrelude(m, wellformednessProc, inParams, outParams, builder, localVariables); + GenerateImplPrelude(m, wellformednessProc, inParams, outParams, builder, localVariables, etran); if (UseOptimizationInZ3) { // We ask Z3 to minimize all parameters of type 'nat'. @@ -5103,7 +5103,7 @@ private void AddFunctionOverrideSubsetChk(Function func, BoogieStmtListBuilder b IToken tok = func.tok; // Declare a local variable $_Frame: [ref, Field alpha]bool - Bpl.IdentifierExpr traitFrame = etran.TheFrame(func.OverriddenFunction.tok); // this is a throw-away expression, used only to extract the type and name of the $_Frame variable + Bpl.IdentifierExpr traitFrame = etran.ReadsFrame(func.OverriddenFunction.tok); // this is a throw-away expression, used only to extract the type and name of the $_Frame variable traitFrame.Name = func.EnclosingClass.Name + "_" + traitFrame.Name; Contract.Assert(traitFrame.Type != null); // follows from the postcondition of TheFrame Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, null ?? traitFrame.Name, traitFrame.Type)); @@ -5369,7 +5369,8 @@ private void AddMethodOverrideSubsetChk(Method m, BoogieStmtListBuilder builder, IToken tok = m.tok; // Declare a local variable $_Frame: [ref, Field alpha]bool - Bpl.IdentifierExpr traitFrame = etran.TheFrame(m.OverriddenMethod.tok); // this is a throw-away expression, used only to extract the type and name of the $_Frame variable + // TODO: need to check reads clauses as well + Bpl.IdentifierExpr traitFrame = etran.ModifiesFrame(m.OverriddenMethod.tok); // this is a throw-away expression, used only to extract the type and name of the $_Frame variable traitFrame.Name = m.EnclosingClass.Name + "_" + traitFrame.Name; Contract.Assert(traitFrame.Type != null); // follows from the postcondition of TheFrame Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, null ?? traitFrame.Name, traitFrame.Type)); @@ -5504,7 +5505,7 @@ void CheckFrameWellFormed(WFOptions wfo, List fes, List inParams, List outParams, - BoogieStmtListBuilder builder, List localVariables) { + BoogieStmtListBuilder builder, List localVariables, ExpressionTranslator etran) { Contract.Requires(m != null); Contract.Requires(inParams != null); Contract.Requires(outParams != null); @@ -5520,7 +5521,7 @@ void GenerateImplPrelude(Method m, bool wellformednessProc, List inPar } // set up the information used to verify the method's modifies clause - DefineFrame(m.tok, m.Mod.Expressions, builder, localVariables, null); + DefineFrame(m.tok, etran.ModifiesFrame(m.tok), m.Mod.Expressions, builder, localVariables, null); if (wellformednessProc) { builder.Add(CaptureState(m.tok, false, "initial state")); } else { @@ -5531,7 +5532,7 @@ void GenerateImplPrelude(Method m, bool wellformednessProc, List inPar } void GenerateIteratorImplPrelude(IteratorDecl iter, List inParams, List outParams, - BoogieStmtListBuilder builder, List localVariables) { + BoogieStmtListBuilder builder, List localVariables, ExpressionTranslator etran) { Contract.Requires(iter != null); Contract.Requires(inParams != null); Contract.Requires(outParams != null); @@ -5544,7 +5545,7 @@ void GenerateIteratorImplPrelude(IteratorDecl iter, List inParams, Lis var th = new ThisExpr(iter); iteratorFrame.Add(new FrameExpression(iter.tok, th, null)); iteratorFrame.AddRange(iter.Modifies.Expressions); - DefineFrame(iter.tok, iteratorFrame, builder, localVariables, null); + DefineFrame(iter.tok, etran.ModifiesFrame(iter.tok), iteratorFrame, builder, localVariables, null); builder.Add(CaptureState(iter.tok, false, "initial state")); } @@ -5562,9 +5563,11 @@ Bpl.Cmd CaptureState(Statement stmt) { return CaptureState(stmt.EndTok, true, null); } - void DefineFrame(IToken/*!*/ tok, List/*!*/ frameClause, + void DefineFrame(IToken/*!*/ tok, Boogie.IdentifierExpr frameIdentifier, List/*!*/ frameClause, BoogieStmtListBuilder/*!*/ builder, List/*!*/ localVariables, string name, ExpressionTranslator/*?*/ etran = null) { Contract.Requires(tok != null); + Contract.Requires(frameIdentifier != null); + Contract.Requires(frameIdentifier.Type != null); Contract.Requires(cce.NonNullElements(frameClause)); Contract.Requires(builder != null); Contract.Requires(cce.NonNullElements(localVariables)); @@ -5577,9 +5580,7 @@ void DefineFrame(IToken/*!*/ tok, List/*!*/ frameClause, etran = new ExpressionTranslator(this, predef, tok); } // Declare a local variable $_Frame: [ref, Field alpha]bool - Bpl.IdentifierExpr theFrame = etran.TheFrame(tok); // this is a throw-away expression, used only to extract the type and name of the $_Frame variable - Contract.Assert(theFrame.Type != null); // follows from the postcondition of TheFrame - Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name ?? theFrame.Name, theFrame.Type)); + Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name ?? frameIdentifier.Name, frameIdentifier.Type)); localVariables.Add(frame); // $_Frame := (lambda $o: ref, $f: Field alpha :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause); // $_Frame := (lambda $o: ref, $f: Field alpha :: $o != null ==> ($o,$f) in Modifies/Reads-Clause); @@ -5599,17 +5600,17 @@ void DefineFrame(IToken/*!*/ tok, List/*!*/ frameClause, void CheckFrameSubset(IToken tok, List calleeFrame, Expression receiverReplacement, Dictionary substMap, - ExpressionTranslator /*!*/ etran, + ExpressionTranslator /*!*/ etran, Boogie.IdentifierExpr /*!*/ enclosingFrame, BoogieStmtListBuilder /*!*/ builder, string errorMessage, Bpl.QKeyValue kv) { - CheckFrameSubset(tok, calleeFrame, receiverReplacement, substMap, etran, + CheckFrameSubset(tok, calleeFrame, receiverReplacement, substMap, etran, enclosingFrame, (t, e, s, q) => builder.Add(Assert(t, e, s, q)), errorMessage, kv); } void CheckFrameSubset(IToken tok, List calleeFrame, Expression receiverReplacement, Dictionary substMap, - ExpressionTranslator/*!*/ etran, + ExpressionTranslator/*!*/ etran, Boogie.IdentifierExpr enclosingFrame, Action MakeAssert, string errorMessage, Bpl.QKeyValue kv) { @@ -5629,7 +5630,7 @@ void CheckFrameSubset(IToken tok, List calleeFrame, Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar); Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o)); Bpl.Expr oInCallee = InRWClause(tok, o, f, calleeFrame, etran, receiverReplacement, substMap); - Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(etran.TheFrame(tok), o, f); + Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(enclosingFrame, o, f); Bpl.Expr q = new Bpl.ForallExpr(tok, new List { alpha }, new List { oVar, fVar }, Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), inEnclosingFrame)); MakeAssert(tok, q, errorMessage, kv); @@ -5972,7 +5973,7 @@ private void AddWellformednessCheck(Function f) { } builder.Add(CaptureState(f.tok, false, "initial state")); - DefineFrame(f.tok, f.Reads, builder, locals, null); + DefineFrame(f.tok, etran.ReadsFrame(f.tok), f.Reads, builder, locals, null); InitializeFuelConstant(f.tok, builder, etran); // Check well-formedness of any default-value expressions (before assuming preconditions). @@ -6082,7 +6083,7 @@ private void AddWellformednessCheck(Function f) { } Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args); - DefineFrame(f.tok, f.Reads, bodyCheckBuilder + DefineFrame(f.tok, etran.ReadsFrame(f.tok), f.Reads, bodyCheckBuilder , new List() /* dummy local variable list, since frame axiom variable (and its definition) * is already added. The only reason why we add the frame axiom definition * again is to make boogie gives the same trace as before the change that @@ -6177,7 +6178,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { builder.Add(CaptureState(decl.tok, false, "initial state")); isAllocContext = new IsAllocContext(true); - DefineFrame(decl.tok, new List(), builder, locals, null); + DefineFrame(decl.tok, etran.ReadsFrame(decl.tok), new List(), builder, locals, null); // some initialization stuff; // This is collected in builderInitializationArea // define frame; @@ -6329,7 +6330,7 @@ void AddWellformednessCheck(ConstantField decl) { builder.Add(CaptureState(decl.tok, false, "initial state")); isAllocContext = new IsAllocContext(true); - DefineFrame(decl.tok, new List(), builder, locals, null); + DefineFrame(decl.tok, etran.ReadsFrame(decl.tok), new List(), builder, locals, null); // check well-formedness of the RHS expression CheckWellformed(decl.Rhs, new WFOptions(null, true), locals, builder, etran); @@ -6400,7 +6401,7 @@ void AddWellformednessCheck(DatatypeCtor ctor) { builder.Add(CaptureState(ctor.tok, false, "initial state")); isAllocContext = new IsAllocContext(true); - DefineFrame(ctor.tok, new List(), builder, locals, null); + DefineFrame(ctor.tok, etran.ReadsFrame(ctor.tok), new List(), builder, locals, null); // check well-formedness of each default-value expression foreach (var formal in ctor.Formals.Where(formal => formal.DefaultValue != null)) { @@ -7307,7 +7308,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu } } if (options.DoReadsChecks && e.Member is Field && ((Field)e.Member).IsMutable) { - options.AssertSink(this, builder)(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field", options.AssertKv); + options.AssertSink(this, builder)(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.ReadsFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field", options.AssertKv); } } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; @@ -7356,7 +7357,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu var i = etran.TrExpr(e.E0); i = ConvertExpression(expr.tok, i, e.E0.Type, Type.Int); Bpl.Expr fieldName = FunctionCall(expr.tok, BuiltinFunction.IndexField, null, i); - options.AssertSink(this, builder)(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element", options.AssertKv); + options.AssertSink(this, builder)(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.ReadsFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element", options.AssertKv); } else { Bpl.Expr lowerBound = e.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(e.E0); Contract.Assert(eSeqType.AsArrayType.Dims == 1); @@ -7366,7 +7367,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(e.tok, iVar); var range = BplAnd(Bpl.Expr.Le(lowerBound, i), Bpl.Expr.Lt(i, upperBound)); var fieldName = FunctionCall(e.tok, BuiltinFunction.IndexField, null, i); - var allowedToRead = Bpl.Expr.SelectTok(e.tok, etran.TheFrame(e.tok), seq, fieldName); + var allowedToRead = Bpl.Expr.SelectTok(e.tok, etran.ReadsFrame(e.tok), seq, fieldName); var trigger = BplTrigger(allowedToRead); // Note, the assertion we're about to produce only seems useful in the check-only mode (that is, with subsumption 0), but if it were to be assumed, we'll use this entire RHS as the trigger var qq = new Bpl.ForallExpr(e.tok, new List { iVar }, trigger, BplImp(range, allowedToRead)); options.AssertSink(this, builder)(expr.tok, qq, "insufficient reads clause to read the indicated range of array elements", options.AssertKv); @@ -7395,7 +7396,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu } if (options.DoReadsChecks) { Bpl.Expr fieldName = etran.GetArrayIndexFieldName(e.tok, e.Indices); - options.AssertSink(this, builder)(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), array, fieldName), "insufficient reads clause to read array element", options.AssertKv); + options.AssertSink(this, builder)(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.ReadsFrame(expr.tok), array, fieldName), "insufficient reads clause to read array element", options.AssertKv); } } else if (expr is SeqUpdateExpr) { var e = (SeqUpdateExpr)expr; @@ -7510,7 +7511,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu objset); var reads = new FrameExpression(e.tok, wrap, null); CheckFrameSubset(expr.tok, new List { reads }, null, null, - etran, options.AssertSink(this, builder), "insufficient reads clause to invoke function", options.AssertKv); + etran, etran.ReadsFrame(expr.tok), options.AssertSink(this, builder), "insufficient reads clause to invoke function", options.AssertKv); } } else if (expr is FunctionCallExpr) { @@ -7628,7 +7629,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu var s = new Substituter(null, new Dictionary(), e.GetTypeArgumentSubstitutions()); CheckFrameSubset(expr.tok, e.Function.Reads.ConvertAll(s.SubstFrameExpr), - e.Receiver, substMap, etran, options.AssertSink(this, builder), "insufficient reads clause to invoke function", options.AssertKv); + e.Receiver, substMap, etran, etran.ReadsFrame(expr.tok), options.AssertSink(this, builder), "insufficient reads clause to invoke function", options.AssertKv); } Bpl.Expr allowance = null; @@ -7920,9 +7921,9 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu // Set up a new frame var frameName = CurrentIdGenerator.FreshId("$_Frame#l"); reads = lam.Reads.ConvertAll(s.SubstFrameExpr); - DefineFrame(e.tok, reads, newBuilder, locals, frameName, comprehensionEtran); - comprehensionEtran = new ExpressionTranslator(comprehensionEtran, frameName); - + comprehensionEtran = new ExpressionTranslator(comprehensionEtran, frameName, comprehensionEtran.modifiesFrame); + DefineFrame(e.tok, comprehensionEtran.ReadsFrame(e.tok), reads, newBuilder, locals, frameName, comprehensionEtran); + // Check frame WF and that it read covers itself newOptions = new WFOptions(options.SelfCallsAllowance, true /* check reads clauses */, true /* delay reads checks */); CheckFrameWellFormed(newOptions, reads, locals, newBuilder, comprehensionEtran); @@ -10062,7 +10063,8 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranPre.IsAlloced(tok, o)); Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF); - consequent = Bpl.Expr.Or(consequent, Bpl.Expr.SelectTok(tok, etranMod.TheFrame(tok), o, f)); + // TODO: double check this is modifies and not reads + consequent = Bpl.Expr.Or(consequent, Bpl.Expr.SelectTok(tok, etranMod.ModifiesFrame(tok), o, f)); Bpl.Trigger tr = new Bpl.Trigger(tok, true, new List { heapOF }); return new Bpl.ForallExpr(tok, new List { alpha }, new List { oVar, fVar }, null, tr, Bpl.Expr.Imp(ante, consequent)); @@ -11651,7 +11653,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi prevObj[i] = obj; if (!useSurrogateLocal) { // check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj]); - builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing context's modifies clause")); + builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.ModifiesFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing context's modifies clause")); } if (useSurrogateLocal) { @@ -11696,7 +11698,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi prevObj[i] = obj; prevIndex[i] = fieldName; // check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj,index]); - builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause")); + builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.ModifiesFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause")); bLhss.Add(null); lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) { @@ -11719,7 +11721,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi "$index" + i, predef.FieldName(mse.tok, predef.BoxType), builder, locals); prevObj[i] = obj; prevIndex[i] = fieldName; - builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause")); + builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.ModifiesFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause")); bLhss.Add(null); lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) { @@ -11947,7 +11949,7 @@ private void CheckElementInit(IToken tok, bool forArray, List dims, options.AssertSink(this, builder)(t, qe, s, qk); }; CheckFrameSubset(tok, new List { reads }, null, null, - etran, maker, + etran, etran.ReadsFrame(tok), maker, "insufficient reads clause to invoke the function passed as an argument to the sequence constructor", options.AssertKv); } From e29db85d035188baf7b99d8d28b9567fa33b92fc Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 17 Sep 2021 13:18:56 -0700 Subject: [PATCH 03/55] Just enough to support the first test case --- Source/Dafny/Resolver.cs | 4 + Source/Dafny/Verifier/Translator.cs | 371 +++++++++--------- .../github-issue-reads-on-methods.dfy | 31 ++ .../github-issue-reads-on-methods.dfy.expect | 3 + 4 files changed, 228 insertions(+), 181 deletions(-) create mode 100644 Test/git-issues/github-issue-reads-on-methods.dfy create mode 100644 Test/git-issues/github-issue-reads-on-methods.dfy.expect diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a1d29441c59..d2bb58bce41 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -10127,6 +10127,10 @@ void ResolveMethod(Method m) { ConstrainTypeExprBool(e.E, "Precondition must be a boolean (got {0})"); } + foreach (FrameExpression fe in m.Reads) { + ResolveFrameExpression(fe, FrameExpressionUse.Reads, m); + } + ResolveAttributes(m.Mod.Attributes, null, new ResolveOpts(m, false)); foreach (FrameExpression fe in m.Mod.Expressions) { ResolveFrameExpression(fe, FrameExpressionUse.Modifies, m); diff --git a/Source/Dafny/Verifier/Translator.cs b/Source/Dafny/Verifier/Translator.cs index 8738f4f58bd..17c8f6cb72f 100644 --- a/Source/Dafny/Verifier/Translator.cs +++ b/Source/Dafny/Verifier/Translator.cs @@ -4829,9 +4829,9 @@ private void AddFunctionOverrideCheckImpl(Function f) { } // modifies $Heap, $Tick var mod = new List { - (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)ordinaryEtran.HeapExpr, - etran.Tick() - }; + (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)ordinaryEtran.HeapExpr, + etran.Tick() + }; var ens = new List(); var proc = new Bpl.Procedure(f.tok, "OverrideCheck$$" + f.FullSanitizedName, new List(), @@ -5117,7 +5117,7 @@ private void AddFunctionOverrideSubsetChk(Function func, BoogieStmtListBuilder b Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o)); Bpl.Expr consequent = InRWClause(tok, o, f, traitFrameExps, etran, null, null); Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new List { alpha }, new List { oVar, fVar }, null, - Bpl.Expr.Imp(ante, consequent)); + Bpl.Expr.Imp(ante, consequent)); //to initialize $_Frame variable to Frame' builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda)); @@ -5126,7 +5126,7 @@ private void AddFunctionOverrideSubsetChk(Function func, BoogieStmtListBuilder b Bpl.Expr oInCallee = InRWClause(tok, o, f, func.Reads, etran, null, null); Bpl.Expr consequent2 = InRWClause(tok, o, f, traitFrameExps, etran, null, null); Bpl.Expr q = new Bpl.ForallExpr(tok, new List { alpha }, new List { oVar, fVar }, - Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), consequent2)); + Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), consequent2)); builder.Add(Assert(tok, q, "expression may read an object not in the parent trait context's reads clause", kv)); } @@ -5384,7 +5384,7 @@ private void AddMethodOverrideSubsetChk(Method m, BoogieStmtListBuilder builder, Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o)); Bpl.Expr consequent = InRWClause(tok, o, f, traitFrameExps, etran, null, null); Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new List { alpha }, new List { oVar, fVar }, null, - Bpl.Expr.Imp(ante, consequent)); + Bpl.Expr.Imp(ante, consequent)); //to initialize $_Frame variable to Frame' builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda)); @@ -5393,7 +5393,7 @@ private void AddMethodOverrideSubsetChk(Method m, BoogieStmtListBuilder builder, Bpl.Expr oInCallee = InRWClause(tok, o, f, classFrameExps, etran, null, null); Bpl.Expr consequent2 = InRWClause(tok, o, f, traitFrameExps, etran, null, null); Bpl.Expr q = new Bpl.ForallExpr(tok, new List { alpha }, new List { oVar, fVar }, - Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), consequent2)); + Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), consequent2)); builder.Add(Assert(tok, q, "expression may modify an object not in the parent trait context's modifies clause", kv)); } @@ -5505,7 +5505,7 @@ void CheckFrameWellFormed(WFOptions wfo, List fes, List inParams, List outParams, - BoogieStmtListBuilder builder, List localVariables, ExpressionTranslator etran) { + BoogieStmtListBuilder builder, List localVariables, ExpressionTranslator etran) { Contract.Requires(m != null); Contract.Requires(inParams != null); Contract.Requires(outParams != null); @@ -5520,7 +5520,8 @@ void GenerateImplPrelude(Method m, bool wellformednessProc, List inPar builder.Add(Bpl.Cmd.SimpleAssign(m.tok, heap, new Bpl.IdentifierExpr(m.tok, "current$Heap", predef.HeapType))); } - // set up the information used to verify the method's modifies clause + // set up the information used to verify the method's reads and modifies clauses + DefineFrame(m.tok, etran.ReadsFrame(m.tok), m.Reads, builder, localVariables, null); DefineFrame(m.tok, etran.ModifiesFrame(m.tok), m.Mod.Expressions, builder, localVariables, null); if (wellformednessProc) { builder.Add(CaptureState(m.tok, false, "initial state")); @@ -5532,7 +5533,7 @@ void GenerateImplPrelude(Method m, bool wellformednessProc, List inPar } void GenerateIteratorImplPrelude(IteratorDecl iter, List inParams, List outParams, - BoogieStmtListBuilder builder, List localVariables, ExpressionTranslator etran) { + BoogieStmtListBuilder builder, List localVariables, ExpressionTranslator etran) { Contract.Requires(iter != null); Contract.Requires(inParams != null); Contract.Requires(outParams != null); @@ -5593,27 +5594,27 @@ void DefineFrame(IToken/*!*/ tok, Boogie.IdentifierExpr frameIdentifier, List { alpha }, new List { oVar, fVar }, null, - Bpl.Expr.Imp(ante, consequent)); + Bpl.Expr.Imp(ante, consequent)); builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda)); } void CheckFrameSubset(IToken tok, List calleeFrame, - Expression receiverReplacement, Dictionary substMap, - ExpressionTranslator /*!*/ etran, Boogie.IdentifierExpr /*!*/ enclosingFrame, - BoogieStmtListBuilder /*!*/ builder, - string errorMessage, - Bpl.QKeyValue kv) { + Expression receiverReplacement, Dictionary substMap, + ExpressionTranslator /*!*/ etran, Boogie.IdentifierExpr /*!*/ enclosingFrame, + BoogieStmtListBuilder /*!*/ builder, + string errorMessage, + Bpl.QKeyValue kv) { CheckFrameSubset(tok, calleeFrame, receiverReplacement, substMap, etran, enclosingFrame, (t, e, s, q) => builder.Add(Assert(t, e, s, q)), errorMessage, kv); } void CheckFrameSubset(IToken tok, List calleeFrame, - Expression receiverReplacement, Dictionary substMap, - ExpressionTranslator/*!*/ etran, Boogie.IdentifierExpr enclosingFrame, - Action MakeAssert, - string errorMessage, - Bpl.QKeyValue kv) { + Expression receiverReplacement, Dictionary substMap, + ExpressionTranslator/*!*/ etran, Boogie.IdentifierExpr enclosingFrame, + Action MakeAssert, + string errorMessage, + Bpl.QKeyValue kv) { Contract.Requires(tok != null); Contract.Requires(calleeFrame != null); Contract.Requires(receiverReplacement == null || substMap != null); @@ -5632,7 +5633,7 @@ void CheckFrameSubset(IToken tok, List calleeFrame, Bpl.Expr oInCallee = InRWClause(tok, o, f, calleeFrame, etran, receiverReplacement, substMap); Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(enclosingFrame, o, f); Bpl.Expr q = new Bpl.ForallExpr(tok, new List { alpha }, new List { oVar, fVar }, - Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), inEnclosingFrame)); + Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), inEnclosingFrame)); MakeAssert(tok, q, errorMessage, kv); } @@ -5756,12 +5757,12 @@ void AddFrameAxiom(Function f) { var ax = new Bpl.ForallExpr(f.tok, new List(), bvars, null, tr, Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, Bpl.Expr.And(h0IsHeapAnchor, heapSucc)), - Bpl.Expr.Imp(q0, eq))); + Bpl.Expr.Imp(q0, eq))); sink.AddTopLevelDeclaration(new Bpl.Axiom(f.tok, ax, comment)); } Bpl.Expr InRWClause(IToken tok, Bpl.Expr o, Bpl.Expr f, List rw, ExpressionTranslator etran, - Expression receiverReplacement, Dictionary substMap) { + Expression receiverReplacement, Dictionary substMap) { Contract.Requires(tok != null); Contract.Requires(o != null); // Contract.Requires(f != null); // f == null means approximate @@ -5774,8 +5775,8 @@ Bpl.Expr InRWClause(IToken tok, Bpl.Expr o, Bpl.Expr f, List rw return InRWClause(tok, o, f, rw, false, etran, receiverReplacement, substMap); } Bpl.Expr InRWClause(IToken tok, Bpl.Expr o, Bpl.Expr f, List rw, bool useInUnchanged, - ExpressionTranslator etran, - Expression receiverReplacement, Dictionary substMap) { + ExpressionTranslator etran, + Expression receiverReplacement, Dictionary substMap) { Contract.Requires(tok != null); Contract.Requires(o != null); // Contract.Requires(f != null); // f == null means approximate @@ -5794,8 +5795,8 @@ Bpl.Expr InRWClause(IToken tok, Bpl.Expr o, Bpl.Expr f, List rw /// "o, Box(o)" for some "o" or "Unbox(bx), bx" for some "bx". /// Bpl.Expr InRWClause_Aux(IToken tok, Bpl.Expr o, Bpl.Expr boxO, Bpl.Expr f, List rw, bool usedInUnchanged, - ExpressionTranslator etran, - Expression receiverReplacement, Dictionary substMap) { + ExpressionTranslator etran, + Expression receiverReplacement, Dictionary substMap) { Contract.Requires(tok != null); Contract.Requires(o != null); Contract.Requires(boxO != null); @@ -6084,11 +6085,11 @@ private void AddWellformednessCheck(Function f) { Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args); DefineFrame(f.tok, etran.ReadsFrame(f.tok), f.Reads, bodyCheckBuilder - , new List() /* dummy local variable list, since frame axiom variable (and its definition) + , new List() /* dummy local variable list, since frame axiom variable (and its definition) * is already added. The only reason why we add the frame axiom definition * again is to make boogie gives the same trace as before the change that * makes reads clauses also guard the requires */ - , null); + , null); wfo = new WFOptions(null, true, true /* do delayed reads checks */); CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran); @@ -6557,7 +6558,7 @@ Bpl.Expr CanCallAssumption(Expression expr, ExpressionTranslator etran) { ApplyExpr e = (ApplyExpr)expr; return BplAnd( Cons(CanCallAssumption(e.Function, etran), - e.Args.ConvertAll(ee => CanCallAssumption(ee, etran)))); + e.Args.ConvertAll(ee => CanCallAssumption(ee, etran)))); } else if (expr is FunctionCallExpr) { FunctionCallExpr e = (FunctionCallExpr)expr; Bpl.Expr r = CanCallAssumption(e.Receiver, etran); @@ -6613,19 +6614,19 @@ Bpl.Expr CanCallAssumption(Expression expr, ExpressionTranslator etran) { break; case BinaryExpr.ResolvedOpcode.EqCommon: case BinaryExpr.ResolvedOpcode.NeqCommon: { - Bpl.Expr r = Bpl.Expr.True; - var dt = e.E0.Type.AsDatatype; - if (dt != null) { - var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(expr.tok, "$IsA#" + dt.FullSanitizedName, Bpl.Type.Bool)); - if (!(e.E0.Resolved is DatatypeValue)) { - r = BplAnd(r, new Bpl.NAryExpr(expr.tok, funcID, new List { etran.TrExpr(e.E0) })); - } - if (!(e.E1.Resolved is DatatypeValue)) { - r = BplAnd(r, new Bpl.NAryExpr(expr.tok, funcID, new List { etran.TrExpr(e.E1) })); - } + Bpl.Expr r = Bpl.Expr.True; + var dt = e.E0.Type.AsDatatype; + if (dt != null) { + var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(expr.tok, "$IsA#" + dt.FullSanitizedName, Bpl.Type.Bool)); + if (!(e.E0.Resolved is DatatypeValue)) { + r = BplAnd(r, new Bpl.NAryExpr(expr.tok, funcID, new List { etran.TrExpr(e.E0) })); + } + if (!(e.E1.Resolved is DatatypeValue)) { + r = BplAnd(r, new Bpl.NAryExpr(expr.tok, funcID, new List { etran.TrExpr(e.E1) })); } - return BplAnd(r, BplAnd(t0, t1)); } + return BplAnd(r, BplAnd(t0, t1)); + } case BinaryExpr.ResolvedOpcode.Mul: if (7 <= DafnyOptions.O.ArithMode) { if (e.E0.Type.IsNumericBased(Type.NumericPersuasion.Int) && !DafnyOptions.O.DisableNLarith) { @@ -7000,37 +7001,45 @@ public WFOptions(Function selfCallsAllowance, bool doReadsChecks, bool saveReads Asserts = new List(); } } + + private WFOptions(Function selfCallsAllowance, bool doReadsChecks, bool doOnlyCoarseGrainedTerminationChecks, + List locals, List asserts, bool lValueContext, Bpl.QKeyValue assertKv) + { + SelfCallsAllowance = selfCallsAllowance; + DoReadsChecks = doReadsChecks; + DoOnlyCoarseGrainedTerminationChecks = doOnlyCoarseGrainedTerminationChecks; + Locals = locals; + Asserts = asserts; + LValueContext = lValueContext; + AssertKv = assertKv; + } public WFOptions(Bpl.QKeyValue kv) { AssertKv = kv; } /// - /// This constructor clones the given "options", but turns off reads checks. (I wish C# allowed - /// me to name the constructor something to indicate this semantics in its name. Sigh.) + /// Clones the given "options", but turns on reads checks. /// - public WFOptions(WFOptions options) { - Contract.Requires(options != null); - SelfCallsAllowance = options.SelfCallsAllowance; - DoReadsChecks = false; // so just leave .Locals and .Asserts as null - DoOnlyCoarseGrainedTerminationChecks = options.DoOnlyCoarseGrainedTerminationChecks; - LValueContext = options.LValueContext; - AssertKv = options.AssertKv; + public WFOptions WithReadsChecks() { + return new WFOptions(SelfCallsAllowance, true, DoOnlyCoarseGrainedTerminationChecks, + Locals, Asserts, LValueContext, AssertKv); + } + + /// + /// Clones the given "options", but turns off reads checks. + /// + public WFOptions WithoutReadsChecks() { + return new WFOptions(SelfCallsAllowance, false, DoOnlyCoarseGrainedTerminationChecks, + Locals, Asserts, LValueContext, AssertKv); } /// - /// This constructor clones the given "options", but sets "LValueContext" to "lValueContext". - /// (I wish C# allowed me to name the constructor something to indicate this semantics in its name. Sigh.) + /// Clones the given "options", but sets "LValueContext" to "lValueContext". /// - public WFOptions(bool lValueContext, WFOptions options) { - Contract.Requires(options != null); - SelfCallsAllowance = options.SelfCallsAllowance; - DoReadsChecks = options.DoReadsChecks; - DoOnlyCoarseGrainedTerminationChecks = options.DoOnlyCoarseGrainedTerminationChecks; - Locals = options.Locals; - Asserts = options.Asserts; - LValueContext = lValueContext; - AssertKv = options.AssertKv; + public WFOptions WithLValueContext(bool lValueContext) { + return new WFOptions(SelfCallsAllowance, false, DoOnlyCoarseGrainedTerminationChecks, + Locals, Asserts, lValueContext, AssertKv); } public Action AssertSink(Translator tran, BoogieStmtListBuilder builder) { @@ -7051,7 +7060,7 @@ public List AssignLocals { Bpl.Cmd.SimpleAssign(l.tok, new Bpl.IdentifierExpr(Token.NoToken, l), Bpl.Expr.True) - ); + ); } } @@ -7090,9 +7099,9 @@ void TrStmt_CheckWellformed(Expression expr, BoogieStmtListBuilder builder, List args.Add(Bpl.Expr.Literal(0)); kv = new Bpl.QKeyValue(expr.tok, "subsumption", args, null); } - var options = new WFOptions(kv); + var options = new WFOptions(kv).WithReadsChecks(); if (lValueContext) { - options = new WFOptions(true, options); + options = options.WithLValueContext(false); } CheckWellformed(expr, options, locals, builder, etran); builder.Add(TrAssumeCmd(expr.tok, CanCallAssumption(expr, etran))); @@ -7115,33 +7124,33 @@ void CheckWellformedAndAssume(Expression expr, WFOptions options, List CheckWellformedAndAssume(e.E1, options, locals, builder, etran); return; case BinaryExpr.ResolvedOpcode.Imp: { - // if (*) { - // WF[e0]; assume e0; WF[e1]; assume e1; - // } else { - // assume e0 ==> e1; - // } - var bAnd = new BoogieStmtListBuilder(this); - CheckWellformedAndAssume(e.E0, options, locals, bAnd, etran); - CheckWellformedAndAssume(e.E1, options, locals, bAnd, etran); - var bImp = new BoogieStmtListBuilder(this); - bImp.Add(TrAssumeCmd(expr.tok, etran.TrExpr(expr))); - builder.Add(new Bpl.IfCmd(expr.tok, null, bAnd.Collect(expr.tok), null, bImp.Collect(expr.tok))); - } + // if (*) { + // WF[e0]; assume e0; WF[e1]; assume e1; + // } else { + // assume e0 ==> e1; + // } + var bAnd = new BoogieStmtListBuilder(this); + CheckWellformedAndAssume(e.E0, options, locals, bAnd, etran); + CheckWellformedAndAssume(e.E1, options, locals, bAnd, etran); + var bImp = new BoogieStmtListBuilder(this); + bImp.Add(TrAssumeCmd(expr.tok, etran.TrExpr(expr))); + builder.Add(new Bpl.IfCmd(expr.tok, null, bAnd.Collect(expr.tok), null, bImp.Collect(expr.tok))); + } return; case BinaryExpr.ResolvedOpcode.Or: { - // if (*) { - // WF[e0]; assume e0; - // } else { - // assume !e0; - // WF[e1]; assume e1; - // } - var b0 = new BoogieStmtListBuilder(this); - CheckWellformedAndAssume(e.E0, options, locals, b0, etran); - var b1 = new BoogieStmtListBuilder(this); - b1.Add(TrAssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)))); - CheckWellformedAndAssume(e.E1, options, locals, b1, etran); - builder.Add(new Bpl.IfCmd(expr.tok, null, b0.Collect(expr.tok), null, b1.Collect(expr.tok))); - } + // if (*) { + // WF[e0]; assume e0; + // } else { + // assume !e0; + // WF[e1]; assume e1; + // } + var b0 = new BoogieStmtListBuilder(this); + CheckWellformedAndAssume(e.E0, options, locals, b0, etran); + var b1 = new BoogieStmtListBuilder(this); + b1.Add(TrAssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)))); + CheckWellformedAndAssume(e.E1, options, locals, b1, etran); + builder.Add(new Bpl.IfCmd(expr.tok, null, b0.Collect(expr.tok), null, b1.Collect(expr.tok))); + } return; default: break; @@ -7221,7 +7230,7 @@ void CheckWellformed(Expression expr, WFOptions options, List locals, /// See class WFOptions for descriptions of the specified options. /// void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr result, Type resultType, - List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { + List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { Contract.Requires(expr != null); Contract.Requires(options != null); Contract.Requires((result == null) == (resultType == null)); @@ -7233,7 +7242,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu var origOptions = options; if (options.LValueContext) { // Turn off LValueContext for any recursive call - options = new WFOptions(false, options); + options = options.WithLValueContext(false); } if (expr is StaticReceiverExpr stexpr) { @@ -7473,8 +7482,8 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu var args = Concat( Map(tt.TypeArgs, TypeToTy), Cons(etran.HeapExpr, - Cons(etran.TrExpr(e.Function), - e.Args.ConvertAll(arg => TrArg(arg))))); + Cons(etran.TrExpr(e.Function), + e.Args.ConvertAll(arg => TrArg(arg))))); // Because type inference often gravitates towards inferring non-constrained types, we'll // do some digging on our own to see if we can discover a more precise type. @@ -7734,7 +7743,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu // Anything read inside the 'old' expressions depends only on the old heap, which isn't included in the // frame axiom. In other words, 'old' expressions have no dependencies on the current heap. Therefore, // we turn off any reads checks for "e.E". - CheckWellformed(e.E, new WFOptions(options), locals, builder, etran.OldAt(e.AtLabel)); + CheckWellformed(e.E, options.WithoutReadsChecks(), locals, builder, etran.OldAt(e.AtLabel)); } else if (expr is UnchangedExpr) { var e = (UnchangedExpr)expr; foreach (var fe in e.Frame) { @@ -7769,16 +7778,16 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu switch (e.ResolvedOp) { case BinaryExpr.ResolvedOpcode.And: case BinaryExpr.ResolvedOpcode.Imp: { - BoogieStmtListBuilder b = new BoogieStmtListBuilder(this); - CheckWellformed(e.E1, options, locals, b, etran); - builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.E0), b.Collect(expr.tok), null, null)); - } + BoogieStmtListBuilder b = new BoogieStmtListBuilder(this); + CheckWellformed(e.E1, options, locals, b, etran); + builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.E0), b.Collect(expr.tok), null, null)); + } break; case BinaryExpr.ResolvedOpcode.Or: { - BoogieStmtListBuilder b = new BoogieStmtListBuilder(this); - CheckWellformed(e.E1, options, locals, b, etran); - builder.Add(new Bpl.IfCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)), b.Collect(expr.tok), null, null)); - } + BoogieStmtListBuilder b = new BoogieStmtListBuilder(this); + CheckWellformed(e.E1, options, locals, b, etran); + builder.Add(new Bpl.IfCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)), b.Collect(expr.tok), null, null)); + } break; case BinaryExpr.ResolvedOpcode.Add: case BinaryExpr.ResolvedOpcode.Sub: @@ -7804,49 +7813,49 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu break; case BinaryExpr.ResolvedOpcode.Div: case BinaryExpr.ResolvedOpcode.Mod: { - Bpl.Expr zero; - if (e.E1.Type.IsBitVectorType) { - zero = BplBvLiteralExpr(e.tok, BaseTypes.BigNum.ZERO, e.E1.Type.AsBitVectorType); - } else if (e.E1.Type.IsNumericBased(Type.NumericPersuasion.Real)) { - zero = Bpl.Expr.Literal(BaseTypes.BigDec.ZERO); - } else { - zero = Bpl.Expr.Literal(0); - } - CheckWellformed(e.E1, options, locals, builder, etran); - builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), zero), "possible division by zero", options.AssertKv)); - CheckResultToBeInType(expr.tok, expr, expr.Type, locals, builder, etran); + Bpl.Expr zero; + if (e.E1.Type.IsBitVectorType) { + zero = BplBvLiteralExpr(e.tok, BaseTypes.BigNum.ZERO, e.E1.Type.AsBitVectorType); + } else if (e.E1.Type.IsNumericBased(Type.NumericPersuasion.Real)) { + zero = Bpl.Expr.Literal(BaseTypes.BigDec.ZERO); + } else { + zero = Bpl.Expr.Literal(0); } + CheckWellformed(e.E1, options, locals, builder, etran); + builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), zero), "possible division by zero", options.AssertKv)); + CheckResultToBeInType(expr.tok, expr, expr.Type, locals, builder, etran); + } break; case BinaryExpr.ResolvedOpcode.LeftShift: case BinaryExpr.ResolvedOpcode.RightShift: { - CheckWellformed(e.E1, options, locals, builder, etran); - var w = e.Type.AsBitVectorType.Width; - var upperMsg = string.Format("shift amount must not exceed the width of the result ({0})", w); - if (e.E1.Type.IsBitVectorType) { - // Known to be non-negative, so we don't need to check lower bound. - // Check upper bound, that is, check "E1 <= w" - var e1Width = e.E1.Type.AsBitVectorType.Width; - if (w < (BigInteger.One << e1Width)) { - // w is a number that can be represented in the e.E1.Type, so do the comparison in that bitvector type. - var bound = BplBvLiteralExpr(e.tok, BaseTypes.BigNum.FromInt(w), e1Width); - var cmp = etran.TrToFunctionCall(expr.tok, "le_bv" + e1Width, Bpl.Type.Bool, etran.TrExpr(e.E1), bound, false); - builder.Add(Assert(expr.tok, cmp, upperMsg, options.AssertKv)); - } else { - // In the previous branch, we had: - // w < 2^e1Width (*) - // From the type of E1, we have: - // E1 < 2^e1Width - // In this branch, (*) does not hold, so we therefore have the following: - // E1 < 2^e1Width <= w - // In other words, the condition - // E1 <= w - // already holds, so there is no reason to check it. - } + CheckWellformed(e.E1, options, locals, builder, etran); + var w = e.Type.AsBitVectorType.Width; + var upperMsg = string.Format("shift amount must not exceed the width of the result ({0})", w); + if (e.E1.Type.IsBitVectorType) { + // Known to be non-negative, so we don't need to check lower bound. + // Check upper bound, that is, check "E1 <= w" + var e1Width = e.E1.Type.AsBitVectorType.Width; + if (w < (BigInteger.One << e1Width)) { + // w is a number that can be represented in the e.E1.Type, so do the comparison in that bitvector type. + var bound = BplBvLiteralExpr(e.tok, BaseTypes.BigNum.FromInt(w), e1Width); + var cmp = etran.TrToFunctionCall(expr.tok, "le_bv" + e1Width, Bpl.Type.Bool, etran.TrExpr(e.E1), bound, false); + builder.Add(Assert(expr.tok, cmp, upperMsg, options.AssertKv)); } else { - builder.Add(Assert(expr.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(e.E1)), "shift amount must be non-negative", options.AssertKv)); - builder.Add(Assert(expr.tok, Bpl.Expr.Le(etran.TrExpr(e.E1), Bpl.Expr.Literal(w)), upperMsg, options.AssertKv)); + // In the previous branch, we had: + // w < 2^e1Width (*) + // From the type of E1, we have: + // E1 < 2^e1Width + // In this branch, (*) does not hold, so we therefore have the following: + // E1 < 2^e1Width <= w + // In other words, the condition + // E1 <= w + // already holds, so there is no reason to check it. } + } else { + builder.Add(Assert(expr.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(e.E1)), "shift amount must be non-negative", options.AssertKv)); + builder.Add(Assert(expr.tok, Bpl.Expr.Le(etran.TrExpr(e.E1), Bpl.Expr.Literal(w)), upperMsg, options.AssertKv)); } + } break; default: CheckWellformed(e.E1, options, locals, builder, etran); @@ -8097,7 +8106,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu } void CheckWellformedSpecialFunction(FunctionCallExpr expr, WFOptions options, Bpl.Expr result, Type resultType, List locals, - BoogieStmtListBuilder builder, ExpressionTranslator etran) { + BoogieStmtListBuilder builder, ExpressionTranslator etran) { Contract.Requires(expr.Function is SpecialFunction); string name = expr.Function.Name; @@ -8112,7 +8121,7 @@ void CheckWellformedSpecialFunction(FunctionCallExpr expr, WFOptions options, Bp } Bpl.Expr CheckWellformedLetExprWithResult(LetExpr e, WFOptions options, Bpl.Expr result, Type resultType, List locals, - BoogieStmtListBuilder builder, ExpressionTranslator etran, bool checkRhs) { + BoogieStmtListBuilder builder, ExpressionTranslator etran, bool checkRhs) { if (e.Exact) { var uniqueSuffix = "#Z" + defaultIdGenerator.FreshNumericId("#Z"); var substMap = SetupBoundVarsAsLocals(e.BoundVars.ToList(), builder, locals, etran, null, "#Z"); @@ -8967,10 +8976,10 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 var isness = BplAnd( Snoc(Map(Enumerable.Range(0, arity), i => - BplAnd(MkIs(boxes[i], types[i], true), - CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(boxes[i], types[i], h0, true) : Bpl.Expr.True)), - BplAnd(MkIs(f, ClassTyCon(ad, types)), - CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(f, ClassTyCon(ad, types), h0) : Bpl.Expr.True))); + BplAnd(MkIs(boxes[i], types[i], true), + CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(boxes[i], types[i], h0, true) : Bpl.Expr.True)), + BplAnd(MkIs(f, ClassTyCon(ad, types)), + CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(f, ClassTyCon(ad, types), h0) : Bpl.Expr.True))); Action AddFrameForFunction = (hN, fname) => { @@ -9027,10 +9036,10 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 var isness = BplAnd( Snoc(Map(Enumerable.Range(0, arity), i => - BplAnd(MkIs(boxes[i], types[i], true), - CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(boxes[i], types[i], h, true) : Bpl.Expr.True)), - BplAnd(MkIs(f, ClassTyCon(ad, types)), - CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(f, ClassTyCon(ad, types), h) : Bpl.Expr.True))); + BplAnd(MkIs(boxes[i], types[i], true), + CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(boxes[i], types[i], h, true) : Bpl.Expr.True)), + BplAnd(MkIs(f, ClassTyCon(ad, types)), + CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(f, ClassTyCon(ad, types), h) : Bpl.Expr.True))); var readsOne = FunctionCall(tok, Reads(arity), objset_ty, Concat(types, Cons(oneheap, Cons(f, boxes)))); var readsH = FunctionCall(tok, Reads(arity), objset_ty, Concat(types, Cons(h, Cons(f, boxes)))); @@ -9039,11 +9048,11 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 var readsNothingH = FunctionCall(tok, BuiltinFunction.SetEqual, null, readsH, empty); sink.AddTopLevelDeclaration(new Axiom(tok, BplForall(bvars, - new Bpl.Trigger(tok, true, new List { readsOne, goodHeap }, - new Bpl.Trigger(tok, true, new List { readsH })), - BplImp( - BplAnd(goodHeap, isness), - BplIff(readsNothingOne, readsNothingH))), + new Bpl.Trigger(tok, true, new List { readsOne, goodHeap }, + new Bpl.Trigger(tok, true, new List { readsH })), + BplImp( + BplAnd(goodHeap, isness), + BplIff(readsNothingOne, readsNothingH))), string.Format("empty-reads property for {0} ", Reads(arity)))); } @@ -9067,10 +9076,10 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 var isness = BplAnd( Snoc(Map(Enumerable.Range(0, arity), i => - BplAnd(MkIs(boxes[i], types[i], true), - CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(boxes[i], types[i], h, true) : Bpl.Expr.True)), - BplAnd(MkIs(f, ClassTyCon(ad, types)), - CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(f, ClassTyCon(ad, types), h) : Bpl.Expr.True))); + BplAnd(MkIs(boxes[i], types[i], true), + CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(boxes[i], types[i], h, true) : Bpl.Expr.True)), + BplAnd(MkIs(f, ClassTyCon(ad, types)), + CommonHeapUse && !FrugalHeapUse ? MkIsAlloc(f, ClassTyCon(ad, types), h) : Bpl.Expr.True))); var readsOne = FunctionCall(tok, Reads(arity), objset_ty, Concat(types, Cons(oneheap, Cons(f, boxes)))); var empty = FunctionCall(tok, BuiltinFunction.SetEmpty, predef.BoxType); @@ -9080,11 +9089,11 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 var requiresH = FunctionCall(tok, Requires(arity), Bpl.Type.Bool, Concat(types, Cons(h, Cons(f, boxes)))); sink.AddTopLevelDeclaration(new Axiom(tok, BplForall(bvars, - new Bpl.Trigger(tok, true, new List { requiresOne, goodHeap }, - new Bpl.Trigger(tok, true, new List { requiresH })), - BplImp( - BplAnd(BplAnd(goodHeap, isness), readsNothingOne), - Bpl.Expr.Eq(requiresOne, requiresH))), + new Bpl.Trigger(tok, true, new List { requiresOne, goodHeap }, + new Bpl.Trigger(tok, true, new List { requiresH })), + BplImp( + BplAnd(BplAnd(goodHeap, isness), readsNothingOne), + Bpl.Expr.Eq(requiresOne, requiresH))), string.Format("empty-reads property for {0}", Requires(arity)))); } @@ -9677,7 +9686,7 @@ Bpl.Procedure AddMethod(Method m, MethodTranslationKind kind) { var dafnyFormalIdExpr = new IdentifierExpr(formal.tok, formal); req.Add(Requires(formal.tok, false, MkIsAlloc(etran.TrExpr(dafnyFormalIdExpr), formal.Type, prevHeap), string.Format("parameter{0} ('{1}') must be allocated in the two-state lemma's previous state", - m.Ins.Count == 1 ? "" : " " + index, formal.Name), null)); + m.Ins.Count == 1 ? "" : " " + index, formal.Name), null)); } index++; } @@ -10843,10 +10852,10 @@ Bpl.Expr SetupVariableAsLocal(IVariable v, Dictionary sub /// allowance || (calleeDecreases LESS contextDecreases). /// void CheckCallTermination(IToken tok, List contextDecreases, List calleeDecreases, - Bpl.Expr allowance, - Expression receiverReplacement, Dictionary substMap, - Dictionary typeMap, - ExpressionTranslator etranCurrent, ExpressionTranslator etranInitial, BoogieStmtListBuilder builder, bool inferredDecreases, string hint) { + Bpl.Expr allowance, + Expression receiverReplacement, Dictionary substMap, + Dictionary typeMap, + ExpressionTranslator etranCurrent, ExpressionTranslator etranInitial, BoogieStmtListBuilder builder, bool inferredDecreases, string hint) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(contextDecreases)); Contract.Requires(cce.NonNullElements(calleeDecreases)); @@ -10909,7 +10918,7 @@ void CheckCallTermination(IToken tok, List contextDecreases, List Bpl.Expr DecreasesCheck(List toks, List types0, List types1, List ee0, List ee1, - BoogieStmtListBuilder builder, string suffixMsg, bool allowNoChange, bool includeLowerBound) { + BoogieStmtListBuilder builder, string suffixMsg, bool allowNoChange, bool includeLowerBound) { Contract.Requires(cce.NonNullElements(toks)); Contract.Requires(cce.NonNullElements(types0)); Contract.Requires(cce.NonNullElements(types1)); @@ -11368,7 +11377,7 @@ Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator return Bpl.Expr.Eq(BplBvLiteralExpr(tok, BaseTypes.BigNum.ZERO, t), x); } } else if ((normType.AsTypeSynonym != null || normType.AsNewtype != null) && - (normType.IsNumericBased() || normType.IsBitVectorType || normType.IsBoolType)) { + (normType.IsNumericBased() || normType.IsBitVectorType || normType.IsBoolType)) { var constraint = Resolver.GetImpliedTypeConstraint(new BoogieWrapper(x, normType), normType); isPred = etran.TrExpr(constraint); } else { @@ -11752,7 +11761,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi /// scope; this is okay, since the purpose of "lhsType" is just to say whether or not the result should be boxed. /// Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, Type lhsType, AssignmentRhs rhs, Type rhsTypeConstraint, - BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { + BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { Contract.Requires(tok != null); Contract.Requires(rhs != null); Contract.Requires(rhsTypeConstraint != null); @@ -12274,8 +12283,8 @@ class LetSuchThatExprInfo { public readonly List