From 1f8b12c2903dfad04e921962db8d234b52025c8b Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 29 Aug 2023 17:09:11 -0700 Subject: [PATCH] Couple of TODOs, remove extraneous code from AddMethodOverrideFrameSubsetChk --- .../Verifier/Translator.ClassMembers.cs | 42 +++++++------------ .../Translator.ExpressionTranslator.cs | 2 - Source/DafnyCore/Verifier/Translator.cs | 24 +++++------ 3 files changed, 26 insertions(+), 42 deletions(-) diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 3cae206a520..e3f8fc90d64 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -1391,7 +1391,7 @@ private void AddMethodOverrideFrameSubsetChk(Method m, bool isModifies, BoogieSt originalTraitFrameExps = m.OverriddenMethod.Reads; } - List traitFrameExps = new List(); + var traitFrameExps = new List(); if (originalTraitFrameExps != null) { // Not currently possible for modifies, but is supported for reads if (originalTraitFrameExps.Any(e => e.E is WildcardExpr)) { @@ -1400,39 +1400,25 @@ private void AddMethodOverrideFrameSubsetChk(Method m, bool isModifies, BoogieSt } foreach (var e in originalTraitFrameExps) { var newE = Substitute(e.E, null, substMap, typeMap); - FrameExpression fe = new FrameExpression(e.tok, newE, e.FieldName); + var fe = new FrameExpression(e.tok, newE, e.FieldName); traitFrameExps.Add(fe); } } - QKeyValue kv = etran.TrAttributes(m.Attributes, null); - - IToken tok = m.tok; - // Declare a local variable $_Reads/ModifiesFrame: [ref, Field alpha]bool - // The next line is a throw-away expression, used only to extract the type and name of the $_Reads/ModifiesFrame variable - Boogie.IdentifierExpr traitFrame = isModifies ? etran.ModifiesFrame(m.OverriddenMethod.tok) : etran.ReadsFrame(m.OverriddenMethod.tok); - traitFrame.Name = m.EnclosingClass.Name + "_" + traitFrame.Name; - Contract.Assert(traitFrame.Type != null); // follows from the postcondition of ModifiesFrame/ReadsFrame - Boogie.LocalVariable frame = new Boogie.LocalVariable(tok, new Boogie.TypedIdent(tok, null ?? traitFrame.Name, traitFrame.Type)); - localVariables.Add(frame); - // $_Frame := (lambda $o: ref, $f: Field alpha :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause); - Boogie.TypeVariable alpha = new Boogie.TypeVariable(tok, "alpha"); - Boogie.BoundVariable oVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$o", predef.RefType)); - Boogie.IdentifierExpr o = new Boogie.IdentifierExpr(tok, oVar); - Boogie.BoundVariable fVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$f", predef.FieldName(tok, alpha))); - Boogie.IdentifierExpr f = new Boogie.IdentifierExpr(tok, fVar); - Boogie.Expr ante = Boogie.Expr.And(Boogie.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o)); - Boogie.Expr consequent = InRWClause(tok, o, f, traitFrameExps, etran, null, null); - Boogie.Expr lambda = new Boogie.LambdaExpr(tok, new List { alpha }, new List { oVar, fVar }, null, - Boogie.Expr.Imp(ante, consequent)); - - //to initialize $_Frame variable to Frame' - builder.Add(Boogie.Cmd.SimpleAssign(tok, new Boogie.IdentifierExpr(tok, frame), lambda)); + var kv = etran.TrAttributes(m.Attributes, null); + + var tok = m.tok; + var alpha = new Boogie.TypeVariable(tok, "alpha"); + var oVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$o", predef.RefType)); + var o = new Boogie.IdentifierExpr(tok, oVar); + var fVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$f", predef.FieldName(tok, alpha))); + var f = new Boogie.IdentifierExpr(tok, fVar); + var ante = Boogie.Expr.And(Boogie.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o)); // emit: assert (forall o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> $_Frame[o,f]); - Boogie.Expr oInCallee = InRWClause(tok, o, f, classFrameExps, etran, null, null); - Boogie.Expr consequent2 = InRWClause(tok, o, f, traitFrameExps, etran, null, null); - Boogie.Expr q = new Boogie.ForallExpr(tok, new List { alpha }, new List { oVar, fVar }, + var oInCallee = InRWClause(tok, o, f, classFrameExps, etran, null, null); + var consequent2 = InRWClause(tok, o, f, traitFrameExps, etran, null, null); + var q = new Boogie.ForallExpr(tok, new List { alpha }, new List { oVar, fVar }, Boogie.Expr.Imp(Boogie.Expr.And(ante, oInCallee), consequent2)); builder.Add(Assert(tok, q, new PODesc.TraitFrame(m.WhatKind, isModifies), kv)); } diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs index 1589db9d6b3..d076b3c8968 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs @@ -231,8 +231,6 @@ private static ExpressionTranslator CloneExpressionTranslator(ExpressionTranslat return et; } - - public Boogie.IdentifierExpr ReadsFrame(IToken tok) { Contract.Requires(tok != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 1984ee8a951..bcbb7b8d57b 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -1703,7 +1703,7 @@ void AddWellformednessCheck(IteratorDecl iter, Procedure proc) { var builder = new BoogieStmtListBuilder(this, options); var etran = new ExpressionTranslator(this, predef, iter.tok); // Don't do reads checks since iterator reads clauses mean something else. - // TODO: expand explanation + // See comment inside GenerateIteratorImplPrelude(). etran = etran.WithReadsFrame(null); var localVariables = new List(); GenerateIteratorImplPrelude(iter, inParams, new List(), builder, localVariables, etran); @@ -1853,7 +1853,7 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { var builder = new BoogieStmtListBuilder(this, options); var etran = new ExpressionTranslator(this, predef, iter.tok); // Don't do reads checks since iterator reads clauses mean something else. - // TODO: expand explanation + // See comment inside GenerateIteratorImplPrelude(). etran = etran.WithReadsFrame(null); var localVariables = new List(); GenerateIteratorImplPrelude(iter, inParams, new List(), builder, localVariables, etran); @@ -3887,7 +3887,7 @@ void GenerateIteratorImplPrelude(IteratorDecl iter, List inParams, Lis // mean something different from reads clauses on functions or methods: // the memory locations that are not havoced by a yield statement. // Look for the references to the YieldHavoc, IterHavoc0 and IterHavoc1 DafnyPrelude.bpl functions for details. - // TODO: assert etran.readsFrame == null (since there's no way to specify THIS kind of reads frame on iterators) + Contract.Assert(etran.readsFrame == null); DefineFrame(iter.tok, etran.ModifiesFrame(iter.tok), iteratorFrame, builder, localVariables, null); builder.AddCaptureState(iter.tok, false, "initial state"); } @@ -3979,16 +3979,16 @@ void CheckFrameEmpty(IToken tok, Contract.Requires(predef != null); // emit: assert (forall o: ref, f: Field alpha :: o != null && $Heap[o,alloc] ==> !frame[o,f]); - Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha"); - Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType)); - Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar); - Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha))); - 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 inFrame = Bpl.Expr.Select(frame, o, f); - Bpl.Expr notInFrame = Bpl.Expr.Not(inFrame); + var alpha = new Bpl.TypeVariable(tok, "alpha"); + var oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType)); + var o = new Bpl.IdentifierExpr(tok, oVar); + var fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha))); + var f = new Bpl.IdentifierExpr(tok, fVar); + var ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o)); + var inFrame = Bpl.Expr.Select(frame, o, f); + var notInFrame = Bpl.Expr.Not(inFrame); - Bpl.Expr q = new Bpl.ForallExpr(tok, new List { alpha }, new List { oVar, fVar }, + var q = new Bpl.ForallExpr(tok, new List { alpha }, new List { oVar, fVar }, Bpl.Expr.Imp(ante, notInFrame)); if (IsExprAlways(q, true)) { return;