implement frame-related asserted exprs and TraitDecreases

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -1182,7 +1182,7 @@ private void AddFunctionOverrideSubsetChk(Function func, BoogieStmtListBuilder b
  Bpl.Expr consequent2 = InRWClause(tok, o, f, traitFrameExps, etran, null, null);
  Bpl.Expr q = new Bpl.ForallExpr(tok, new List<TypeVariable>(), new List<Variable> { oVar, fVar },
  BplImp(BplAnd(ante, oInCallee), consequent2));
- builder.Add(Assert(tok, q, new PODesc.TraitFrame(func.WhatKind, false), kv));
+ builder.Add(Assert(tok, q, new PODesc.TraitFrame(func.WhatKind, false, func.Reads.Expressions, traitFrameExps), kv));
  }
 
  private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builder, ExpressionTranslator etran,
@@ -1517,11 +1517,10 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo
  var caller = new List<Expr>();
  var calleeDafny = new List<Expression>();
  var callerDafny = new List<Expression>();
- FunctionCallSubstituter sub = null;
+ FunctionCallSubstituter sub = new FunctionCallSubstituter(substMap, typeMap, T, I);
 
  for (int i = 0; i < N; i++) {
  Expression e0 = calleeDecreases[i];
- sub ??= new FunctionCallSubstituter(substMap, typeMap, T, I);
  Expression e1 = sub.Substitute(contextDecreases[i]);
  if (!CompatibleDecreasesTypes(e0.Type, e1.Type)) {
  N = i;
@@ -1565,7 +1564,13 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo
  bool allowNoChange = N == decrCountT && decrCountT <= decrCountC;
  var decrChk = DecreasesCheck(toks, null, calleeDafny, callerDafny, callee, caller, null,
  null, allowNoChange, false);
- builder.Add(Assert(original.RangeToken, decrChk, new PODesc.TraitDecreases(original.WhatKind)));
+ var assertedExpr = new DecreasesToExpr(
+ Token.NoToken,
+ contextDecreases.Select(sub.Substitute).ToList(),
+ calleeDecreases,
+ true);
+ var desc = new PODesc.TraitDecreases(original.WhatKind, assertedExpr);
+ builder.Add(Assert(original.RangeToken, decrChk, desc));
  }
 
  private void AddMethodOverrideFrameSubsetChk(Method m, bool isModifies, BoogieStmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables,
@@ -1610,7 +1615,7 @@ private void AddMethodOverrideFrameSubsetChk(Method m, bool isModifies, BoogieSt
  var consequent2 = InRWClause(tok, o, f, traitFrameExps, etran, null, null);
  var q = new Boogie.ForallExpr(tok, new List<TypeVariable>(), new List<Variable> { oVar, fVar },
  BplImp(BplAnd(ante, oInCallee), consequent2));
- builder.Add(Assert(m.RangeToken, q, new PODesc.TraitFrame(m.WhatKind, isModifies), kv));
+ builder.Add(Assert(m.RangeToken, q, new PODesc.TraitFrame(m.WhatKind, isModifies, classFrameExps, traitFrameExps), kv));
  }
 
  // Return a way to know if an assertion should be converted to an assumption

Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs

@@ -351,7 +351,9 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List<Variable
  // check well-formedness of the modifies clauses
  CheckFrameWellFormed(new WFOptions(), s.Mod.Expressions, locals, builder, etran);
  // check that the modifies is a subset
- CheckFrameSubset(s.Tok, s.Mod.Expressions, null, null, etran, etran.ModifiesFrame(s.Tok), builder, new PODesc.ModifyFrameSubset("modify statement"), null);
+ var contextModFrames = (codeContext as IMethodCodeContext)?.Modifies.Expressions ?? new();
+ var desc = new PODesc.ModifyFrameSubset("modify statement", s.Mod.Expressions, contextModFrames);
+ CheckFrameSubset(s.Tok, s.Mod.Expressions, null, null, etran, etran.ModifiesFrame(s.Tok), builder, desc, null);
  // cause the change of the heap according to the given frame
  var suffix = CurrentIdGenerator.FreshId("modify#");
  string modifyFrameName = "$Frame$" + suffix;
@@ -1281,8 +1283,16 @@ void TrForallAssign(ForallStmt s, AssignStmt s0,
  var lhs = Substitute(s0.Lhs.Resolved, null, substMap);
  TrStmt_CheckWellformed(lhs, definedness, locals, etran, false);
  string description = GetObjFieldDetails(lhs, etran, out var obj, out var F);
+ var (lhsObj, lhsField) = lhs switch {
+ MemberSelectExpr e => (e.Obj, e.Member as Field),
+ SeqSelectExpr e => (e.Seq, null),
+ MultiSelectExpr e => (e.Array, null),
+ _ => throw new cce.UnreachableException()
+ };
+ var contextModFrames = (codeContext as IMethodCodeContext)?.Modifies.Expressions ?? new();
+ var desc = new PODesc.Modifiable(description, contextModFrames, lhsObj, lhsField);
  definedness.Add(Assert(lhs.tok, Bpl.Expr.SelectTok(lhs.tok, etran.ModifiesFrame(lhs.tok), obj, F),
- new PODesc.Modifiable(description)));
+ desc));
  if (s0.Rhs is ExprRhs) {
  var r = (ExprRhs)s0.Rhs;
  var rhs = Substitute(r.Expr, null, substMap);
@@ -1300,9 +1310,8 @@ void TrForallAssign(ForallStmt s, AssignStmt s0,
  CheckSubrange(r.Tok, translatedRhs, rhs.Type, lhsType, rhs, definedness);
  if (lhs is MemberSelectExpr) {
  var fse = (MemberSelectExpr)lhs;
- var field = fse.Member as Field;
- Contract.Assert(field != null);
- Check_NewRestrictions(fse.tok, fse.Obj, obj, field, translatedRhs, definedness, etran);
+ Contract.Assert(lhsField != null);
+ Check_NewRestrictions(fse.tok, fse.Obj, obj, lhsField, translatedRhs, definedness, etran);
  }
  }
 
@@ -1325,12 +1334,13 @@ void TrForallAssign(ForallStmt s, AssignStmt s0,
  var Rhs = ((ExprRhs)s0.Rhs).Expr;
  var rhs = etran.TrExpr(Substitute(Rhs, null, substMap));
  var rhsPrime = etran.TrExpr(Substitute(Rhs, null, substMapPrime));
- var lhsComponents = lhs switch {
- SeqSelectExpr seq => new List<Expression> { seq.Seq, seq.E0 },
- MultiSelectExpr multi => (new List<Expression> { multi.Array }).Concat(multi.Indices).ToList(),
- MemberSelectExpr mse => new List<Expression> { mse.Obj },
- _ => throw new cce.UnreachableException()
- };
+ var lhsComponents = new List<Expression> { lhsObj };
+ if (lhs is SeqSelectExpr sse) {
+ lhsComponents.Add(sse.E0);
+ } else if (lhs is MultiSelectExpr multi) {
+ lhsComponents.AddRange(multi.Indices);
+ }
+
  definedness.Add(Assert(s0.Tok,
  BplOr(
  BplOr(Bpl.Expr.Neq(obj, objPrime), Bpl.Expr.Neq(F, FPrime)),
@@ -1461,7 +1471,9 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr,
 
  if (s.Mod.Expressions != null) { // check well-formedness and that the modifies is a subset
  CheckFrameWellFormed(new WFOptions(), s.Mod.Expressions, locals, builder, etran);
- CheckFrameSubset(s.Tok, s.Mod.Expressions, null, null, etran, etran.ModifiesFrame(s.Tok), builder, new PODesc.ModifyFrameSubset("loop modifies clause"), null);
+ var contextModFrames = (codeContext as IMethodCodeContext)?.Modifies.Expressions ?? new();
+ var desc = new PODesc.ModifyFrameSubset("loop modifies clause", s.Mod.Expressions, contextModFrames);
+ CheckFrameSubset(s.Tok, s.Mod.Expressions, null, null, etran, etran.ModifiesFrame(s.Tok), builder, desc, null);
  DefineFrame(s.Tok, etran.ModifiesFrame(s.Tok), s.Mod.Expressions, builder, locals, loopFrameName);
  }
  builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr));
@@ -2039,10 +2051,12 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
  }
  // Check that the modifies clause of a subcall is a subset of the current modifies frame,
  // but only if we're in a context that defines a modifies frame.
- if (codeContext is IMethodCodeContext) {
- var modifiesSubst = new Substituter(null, new Dictionary<IVariable, Expression>(), tySubst);
- CheckFrameSubset(tok, callee.Mod.Expressions.ConvertAll(modifiesSubst.SubstFrameExpr),
- receiver, substMap, etran, etran.ModifiesFrame(tok), builder, new PODesc.ModifyFrameSubset("call"), null);
+ if (codeContext is IMethodCodeContext methodCodeContext) {
+ var modifiesSubst = new Substituter(null, directSubstMap, tySubst);
+ var calleeFrame = callee.Mod.Expressions.ConvertAll(modifiesSubst.SubstFrameExpr);
+ var desc = new PODesc.ModifyFrameSubset("call", calleeFrame, methodCodeContext.Modifies.Expressions);
+ CheckFrameSubset(tok, calleeFrame,
+ receiver, substMap, etran, etran.ModifiesFrame(tok), builder, desc, null);
  }
 
  // Check termination
@@ -2487,6 +2501,8 @@ void ProcessLhss(List<Expression> lhss, bool rhsCanAffectPreviouslyKnownExpressi
 
  var lhsNameSet = new Dictionary<string, object>();
 
+ var contextModFrames = (codeContext as IMethodCodeContext)?.Modifies.Expressions ?? new();
+
  // Note, the resolver does not check for duplicate IdentifierExpr's in LHSs, so do it here.
  foreach (var lhs in lhss) {
  Contract.Assume(!(lhs is ConcreteSyntaxExpression));
@@ -2536,7 +2552,8 @@ void ProcessLhss(List<Expression> lhss, bool rhsCanAffectPreviouslyKnownExpressi
  prevObj[i] = obj;
  if (!useSurrogateLocal) {
  // check that the enclosing modifies clause allows this object to be written: assert $_ModifiesFrame[obj]);
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.ModifiesFrame(tok), obj, GetField(fse)), new PODesc.Modifiable("an object")));
+ var desc = new PODesc.Modifiable("an object", contextModFrames, fse.Obj, field);
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.ModifiesFrame(tok), obj, GetField(fse)), desc));
  }
 
  if (useSurrogateLocal) {
@@ -2585,7 +2602,8 @@ void ProcessLhss(List<Expression> 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.ModifiesFrame(tok), obj, fieldName), new PODesc.Modifiable("an array element")));
+ var desc = new PODesc.Modifiable("an array element", contextModFrames, sel.Seq, null);
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.ModifiesFrame(tok), obj, fieldName), desc));
 
  bLhss.Add(null);
  lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) {
@@ -2609,7 +2627,8 @@ void ProcessLhss(List<Expression> lhss, bool rhsCanAffectPreviouslyKnownExpressi
  "$index" + i, predef.FieldName(mse.tok), builder, locals);
  prevObj[i] = obj;
  prevIndex[i] = fieldName;
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.ModifiesFrame(tok), obj, fieldName), new PODesc.Modifiable("an array element")));
+ var desc = new PODesc.Modifiable("an array element", contextModFrames, mse.Array, null);
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.ModifiesFrame(tok), obj, fieldName), desc));
 
  bLhss.Add(null);
  lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) {

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -747,10 +747,18 @@
 
  private readonly string whatKind;
  private bool isModify;
+ private readonly List<FrameExpression> subsetFrames;
+ private readonly List<FrameExpression> supersetFrames;
 
- public TraitFrame(string whatKind, bool isModify) {
+ public TraitFrame(string whatKind, bool isModify, List<FrameExpression> subsetFrames, List<FrameExpression> supersetFrames) {
  this.whatKind = whatKind;
  this.isModify = isModify;
+ this.subsetFrames = subsetFrames;
+ this.supersetFrames = supersetFrames;
+ }
+
+ public override Expression GetAssertedExpr(DafnyOptions options) {
+ return Utils.MakeDafnyMultiFrameCheck(supersetFrames, subsetFrames);
  }
 }
 
@@ -766,9 +774,15 @@
  public override bool ProvedOutsideUserCode => true;
 
  private readonly string whatKind;
+ private readonly Expression expr;
 
- public TraitDecreases(string whatKind) {
+ public TraitDecreases(string whatKind, Expression expr) {
  this.whatKind = whatKind;
+ this.expr = expr;
+ }
+
+ public override Expression GetAssertedExpr(DafnyOptions options) {
+ return expr;
  }
 }
 
@@ -844,9 +858,18 @@
  public override string ShortDescription => "modify frame subset";
 
  private readonly string whatKind;
+ private readonly Expression expr;
+ private readonly List<FrameExpression> subsetFrames;
+ private readonly List<FrameExpression> supersetFrames;
 
- public ModifyFrameSubset(string whatKind) {
+ public ModifyFrameSubset(string whatKind, List<FrameExpression> subsetFrames, List<FrameExpression> supersetFrames) {
  this.whatKind = whatKind;
+ this.subsetFrames = subsetFrames;
+ this.supersetFrames = supersetFrames;
+ }
+
+ public override Expression GetAssertedExpr(DafnyOptions options) {
+ return Utils.MakeDafnyMultiFrameCheck(supersetFrames, subsetFrames);
  }
 }
 
@@ -988,9 +1011,19 @@
  public override string ShortDescription => "modifiable";
 
  private readonly string description;
+ private readonly List<FrameExpression> frames;
+ private readonly Expression obj;
+ private readonly Field field;
 
- public Modifiable(string description) {
+ public Modifiable(string description, List<FrameExpression> frames, Expression obj, Field field) {
  this.description = description;
+ this.frames = frames;
+ this.obj = obj;
+ this.field = field;
+ }
+
+ public override Expression GetAssertedExpr(DafnyOptions options) {
+ return Utils.MakeDafnyFrameCheck(frames, obj, field);
  }
 }
 
@@ -1832,4 +1865,72 @@
  .Select(ctor => new ExprDotName(Token.NoToken, root, ctor.Name + "?", null) as Expression)
  .Aggregate((e0, e1) => new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Or, e0, e1));
  }
+
+ /// <summary>
+ /// Builds an expression that represents whether (the relevant subset of) the given `supersetFrames`
+ /// permit read/modification access to all objects, arrays, and/or sets of objects/arrays in the `subsetFrames`.
+ /// </summary>
+ public static Expression MakeDafnyMultiFrameCheck(List<FrameExpression> supersetFrames, List<FrameExpression> subsetFrames) {
+ return subsetFrames
+ .Select(target => MakeDafnyFrameCheck(supersetFrames, target.E, target.Field))
+ .Aggregate((e0, e1) => new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, e0, e1));
+ }
+
+ /// <summary>
+ /// Builds an expression that represents whether (the relevant subset of) the given frames
+ /// permit read/modification access to an object/array (or set of objects/arrays).
+ /// </summary>
+ public static Expression MakeDafnyFrameCheck(List<FrameExpression> frames, Expression objOrObjSet, Field field) {
+ if (frames.Any(frame => frame.E is WildcardExpr)) {
+ return new LiteralExpr(Token.NoToken, true);
+ }
+
+ Type objType;
+ BoundVar objVar;
+ Expression objOperand;
+ var isSetObj = objOrObjSet.Type is SetType;
+ if (isSetObj) {
+ objType = objOrObjSet.Type.AsSetType.Arg;
+ objVar = new BoundVar(Token.NoToken, "obj", objType);
+ objOperand = new IdentifierExpr(Token.NoToken, objVar);
+ } else {
+ objType = objOrObjSet.Type;
+ objVar = null;
+ objOperand = objOrObjSet;
+ }
+
+ var disjuncts = new List<Expression>();
+ foreach (var frame in frames) {
+ var isSetFrame = frame.E.Type is SetType;
+ var frameObjType = isSetFrame ? frame.E.Type.AsSetType.Arg : frame.E.Type;
+ var isTypeRelated = objType.IsSubtypeOf(frameObjType, false, false);
+ var isFieldRelated = field == null || frame.Field == null || field.Name.Equals(frame.Field.Name);
+ if (!(isTypeRelated && isFieldRelated)) {
+ continue;
+ }
+
+ var relationOp = isSetFrame ? BinaryExpr.Opcode.In : BinaryExpr.Opcode.Eq;
+ disjuncts.Add(new BinaryExpr(Token.NoToken, relationOp, objOperand, frame.E));
+ }
+
+ if (disjuncts.Count == 0) {
+ var emptySet = new SetDisplayExpr(Token.NoToken, true, new());
+ disjuncts.Add(new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.In, objOperand, emptySet));
+ }
+
+ var check = disjuncts.Aggregate((e0, e1) =>
+ new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Or, e0, e1));
+ if (!isSetObj) {
+ return check;
+ }
+
+ return new ForallExpr(
+ Token.NoToken,
+ RangeToken.NoToken,
+ new() { objVar },
+ new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.In, objOperand, objOrObjSet),
+ check,
+ null
+ );
+ }
 }

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/modifiable.dfy

@@ -0,0 +1,68 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+class C {
+ var x: int
+ var y: int
+ method ModifyClassField()
+ modifies this`y
+ {
+ x := 0;
+ }
+}
+
+class C2 {
+ var x: int
+ var y: int
+}
+
+method ModifyObject(s: seq<C>, t: seq<C2>)
+ requires |s| > 1
+ requires |t| > 0
+ // singletons
+ modifies s[1] // no field
+ modifies (s[1] as C)`x // right field
+ modifies (s[0] as C)`y // right object, wrong field
+ modifies (t[0] as C2)`x // wrong type, right field name
+ // sets
+ modifies {s[1]} // no field
+ modifies {s[1] as C}`x // right field
+ modifies {s[0] as C}`y // right object, wrong field
+ modifies {t[0] as C2}`x // wrong type, right field name
+{
+ s[0].x := 1;
+}
+
+method ModifyObjects(s: seq<C>)
+ requires |s| > 1
+ modifies s[1]
+ modifies (set c | c in s)`y
+{
+ forall c | c in s {
+ c.x := 1;
+ }
+}
+
+method ModifyArray(a: array<int>, b: array<int>)
+ modifies b
+{
+ if a.Length > 0 {
+ a[0] := 1;
+ }
+}
+
+method ModifyArrays(s: seq<array<int>>)
+ requires |s| > 1
+ modifies s[1]
+{
+ forall a | a in s && a.Length > 0 {
+ a[0] := 1;
+ }
+}
+
+method ModifyMultiDimArray(a: array2<int>)
+{
+ if a.Length0 > 0 && a.Length1 > 0 {
+ a[0, 0] := 1;
+ }
+}