Skip to content

Commit

Permalink
Couple of TODOs, remove extraneous code from AddMethodOverrideFrameSu…
Browse files Browse the repository at this point in the history 
…bsetChk
  • Loading branch information
@robin-aws
robin-aws committed Aug 30, 2023
1 parent b484dae commit 1f8b12c
Show file tree
Hide file tree
Showing 3 changed files with 26 additions and 42 deletions.
42 changes: 14 additions & 28 deletions Source/DafnyCore/Verifier/Translator.ClassMembers.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1391,7 +1391,7 @@ private void AddMethodOverrideFrameSubsetChk(Method m, bool isModifies, BoogieSt
originalTraitFrameExps = m.OverriddenMethod.Reads;
}

List<FrameExpression> traitFrameExps = new List<FrameExpression>();
var traitFrameExps = new List<FrameExpression>();
if (originalTraitFrameExps != null) {
// Not currently possible for modifies, but is supported for reads
if (originalTraitFrameExps.Any(e => e.E is WildcardExpr)) {
Expand All @@ -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 $<EnclosingClass>_Reads/ModifiesFrame: <alpha>[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<alpha> $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<TypeVariable> { alpha }, new List<Variable> { 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<alpha> 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<TypeVariable> { alpha }, new List<Variable> { 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<TypeVariable> { alpha }, new List<Variable> { oVar, fVar },
Boogie.Expr.Imp(Boogie.Expr.And(ante, oInCallee), consequent2));
builder.Add(Assert(tok, q, new PODesc.TraitFrame(m.WhatKind, isModifies), kv));
}
Expand Down
2 changes: 0 additions & 2 deletions Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Boogie.IdentifierExpr>() != null);
Expand Down
24 changes: 12 additions & 12 deletions Source/DafnyCore/Verifier/Translator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Variable>();
GenerateIteratorImplPrelude(iter, inParams, new List<Variable>(), builder, localVariables, etran);
Expand Down Expand Up @@ -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<Variable>();
GenerateIteratorImplPrelude(iter, inParams, new List<Variable>(), builder, localVariables, etran);
Expand Down Expand Up @@ -3887,7 +3887,7 @@ void GenerateIteratorImplPrelude(IteratorDecl iter, List<Variable> 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");
}
Expand Down Expand Up @@ -3979,16 +3979,16 @@ void CheckFrameEmpty(IToken tok,
Contract.Requires(predef != null);

// emit: assert (forall<alpha> 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<TypeVariable> { alpha }, new List<Variable> { oVar, fVar },
var q = new Bpl.ForallExpr(tok, new List<TypeVariable> { alpha }, new List<Variable> { oVar, fVar },
Bpl.Expr.Imp(ante, notInFrame));
if (IsExprAlways(q, true)) {
return;
Expand Down

0 comments on commit 1f8b12c

Please sign in to comment.