dafny-lang · fabiomadge · Jan 31, 2023 · Jan 31, 2023
diff --git a/Source/DafnyCore/Compilers/Python/Compiler-python.cs b/Source/DafnyCore/Compilers/Python/Compiler-python.cs
@@ -1740,6 +1740,5 @@ protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageV
       exceptBlock.WriteLine($"{IdProtect(haltMessageVarName)} = e.message");
       TrStmt(recoveryBody, exceptBlock);
     }
-
   }
 }
diff --git a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs
@@ -3,26 +3,26 @@
 namespace Microsoft.Dafny {
   public class FunctionCallSubstituter : Substituter {
     public readonly Function A, B;
-    public FunctionCallSubstituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Dictionary<TypeParameter, Type> typeMap, Function a, Function b)
-      : base(receiverReplacement, substMap, typeMap) {
+    public FunctionCallSubstituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Function a, Function b)
+      : base(receiverReplacement, substMap, new Dictionary<TypeParameter, Type>()) {
       A = a;
       B = b;
     }
     public override Expression Substitute(Expression expr) {
-      if (expr is FunctionCallExpr e) {
-        var receiver = Substitute(e.Receiver);
-        var newArgs = SubstituteExprList(e.Args);
-        var newFce = new FunctionCallExpr(e.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel);
-        if (e.Function == A && e.Receiver is ThisExpr && receiver is ThisExpr) {
+      if (expr is FunctionCallExpr) {
+        FunctionCallExpr e = (FunctionCallExpr)expr;
+        Expression receiver = Substitute(e.Receiver);
+        List<Expression> newArgs = SubstituteExprList(e.Args);
+        FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel);
+        if (e.Function == A) {
           newFce.Function = B;
           newFce.Type = e.Type; // TODO: this may not work with type parameters.
-          receiver.Type = Resolver.GetThisType(B.tok, (TopLevelDeclWithMembers)B.EnclosingClass);
         } else {
           newFce.Function = e.Function;
           newFce.Type = e.Type;
         }
-        newFce.TypeApplication_AtEnclosingClass = SubstituteTypeList(e.TypeApplication_AtEnclosingClass);  // resolve here
-        newFce.TypeApplication_JustFunction = SubstituteTypeList(e.TypeApplication_JustFunction);  // resolve here
+        newFce.TypeApplication_AtEnclosingClass = e.TypeApplication_AtEnclosingClass;  // resolve here
+        newFce.TypeApplication_JustFunction = e.TypeApplication_JustFunction;  // resolve here
         newFce.IsByMethodCall = e.IsByMethodCall;
         return newFce;
       }

diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
@@ -213,8 +213,7 @@ private void AddAllocationAxiom(Boogie.Declaration fieldDeclaration, Field f, To
         AddWellformednessCheck(cf);
         if (InVerificationScope(cf)) {
           var etran = new ExpressionTranslator(this, predef, f.tok);
-          var visibilityLevel = cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf);
-          heightAntecedent = Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
+          heightAntecedent = Bpl.Expr.Lt(Bpl.Expr.Literal(cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf)), etran.FunctionContextHeight());
         }
       }
 
@@ -878,8 +877,8 @@ private void AddFunctionOverrideCheckImpl(Function f) {
       }
       // the procedure itself
       var req = new List<Boogie.Requires>();
-      // free requires fh == FunctionContextHeight;
-      req.Add(Requires(f.tok, true, etran.HeightContext(f, true), null, null));
+      // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
+      req.Add(Requires(f.tok, true, etran.HeightContext(f.OverriddenFunction), null, null));
       if (f is TwoStateFunction) {
         // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
         var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr);
@@ -921,16 +920,18 @@ private void AddFunctionOverrideCheckImpl(Function f) {
       }
 
       var substMap = new Dictionary<IVariable, Expression>();
-      foreach (var (formal, overriddenFormal) in f.Formals.Zip(f.OverriddenFunction.Formals, Tuple.Create)) {
-        // get corresponding formal in the class
-        var ie = new IdentifierExpr(formal.tok, formal.AssignUniqueName(f.IdGenerator)) { Var = formal, Type = formal.Type };
-        substMap.Add(overriddenFormal, ie);
+      for (int i = 0; i < f.Formals.Count; i++) {
+        //get corresponsing formal in the class
+        var ie = new IdentifierExpr(f.Formals[i].tok, f.Formals[i].AssignUniqueName(f.IdGenerator));
+        ie.Var = f.Formals[i]; ie.Type = ie.Var.Type;
+        substMap.Add(f.OverriddenFunction.Formals[i], ie);
       }
 
       if (f.OverriddenFunction.Result != null) {
         Contract.Assert(pOut != null);
-        // get corresponding formal in the class
-        var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator)) { Var = pOut, Type = pOut.Type };
+        //get corresponsing formal in the class
+        var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator));
+        ie.Var = pOut; ie.Type = ie.Var.Type;
         substMap.Add(f.OverriddenFunction.Result, ie);
       }
 
@@ -945,8 +946,8 @@ private void AddFunctionOverrideCheckImpl(Function f) {
       //adding assert W <= Frame’
       AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap);
 
-      //adding assume Q;
-      //assert Post’;
+      //adding assume Q; assert Post’;
+      //adding assume J.F(ins) == C.F(ins);
       AddFunctionOverrideEnsChk(f, builder, etran, substMap, typeMap, implInParams, implOutParams.Count == 0 ? null : implOutParams[0]);
 
       var stmts = builder.Collect(f.tok);
@@ -1133,7 +1134,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
       // The axiom
       Boogie.Expr ax = BplForall(f.tok, new List<Boogie.TypeVariable>(), forallFormals, null, tr,
         Boogie.Expr.Imp(Boogie.Expr.And(ReceiverNotNull(bvThisExpr), isOfSubtype), synonyms));
-      var activate = AxiomActivation(overridingFunction, etran, true);
+      var activate = AxiomActivation(f, etran);
       string comment = "override axiom for " + f.FullSanitizedName + " in class " + overridingFunction.EnclosingClass.FullSanitizedName;
       return new Boogie.Axiom(f.tok, Boogie.Expr.Imp(activate, ax), comment);
     }

diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs
@@ -258,11 +258,12 @@ public Boogie.IdentifierExpr FunctionContextHeight() {
         return new Boogie.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Boogie.Type.Int);
       }
 
-      public Boogie.Expr HeightContext(ICallable m, bool intermediateScope = false) {
+      public Boogie.Expr HeightContext(ICallable m) {
         Contract.Requires(m != null);
         // free requires fh == FunctionContextHeight;
-        var visibilityLevel = m.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(m);
-        Boogie.Expr context = Boogie.Expr.Eq(MkFunctionHeight(visibilityLevel, intermediateScope), FunctionContextHeight());
+        var module = m.EnclosingModule;
+        Boogie.Expr context =
+          Boogie.Expr.Eq(Boogie.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(m)), FunctionContextHeight());
         return context;
       }
 

diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
@@ -2054,7 +2054,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
       //   (mh == ModuleContextHeight && fh <= FunctionContextHeight)
       //
       // USE_VIA_CONTEXT
-      //   fh < FunctionContextHeight &&
+      //   (mh != ModuleContextHeight || fh != FunctionContextHeight) &&
       //   GOOD_PARAMETERS
       // where GOOD_PARAMETERS means:
       //   $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
@@ -2157,9 +2157,10 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
       foreach (AttributedExpression req in f.Req) {
         pre = BplAnd(pre, etran.TrExpr(Substitute(req.E, null, substMap)));
       }
-      // useViaContext: fh < FunctionContextHeight
-      var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f.OverriddenFunction ?? f);
-      Expr useViaContext = Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
+      // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)
+      var mod = f.EnclosingClass.EnclosingModuleDefinition;
+      Bpl.Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True :
+        (Bpl.Expr)Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
       // useViaCanCall: f#canCall(args)
       Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool);
       Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args));
@@ -2254,14 +2255,15 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
       return (olderParameterCount, olderCondition);
     }
 
-    Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran, bool requiresFullScope = false) {
+    Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran) {
       Contract.Requires(f != null);
       Contract.Requires(etran != null);
       Contract.Requires(VisibleInScope(f));
+      var module = f.EnclosingClass.EnclosingModuleDefinition;
 
       if (InVerificationScope(f)) {
-        var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f);
-        return Expr.Le(MkFunctionHeight(visibilityLevel, !requiresFullScope), etran.FunctionContextHeight());
+        return
+          Bpl.Expr.Le(Bpl.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
       } else {
         return Bpl.Expr.True;
       }
@@ -2301,7 +2303,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
       // for visibility==ForeignModuleOnly, means:
       //   GOOD_PARAMETERS
       // for visibility==IntraModuleOnly, means:
-      //   fh < FunctionContextHeight &&
+      //   fh != FunctionContextHeight &&
       //   GOOD_PARAMETERS
       // where GOOD_PARAMETERS means:
       //   $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
@@ -2506,11 +2508,12 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
         return null;
       }
 
-      // useViaContext: fh < FunctionContextHeight
-      var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f);
+      // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)
+      ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition;
       Bpl.Expr useViaContext = !InVerificationScope(f)
-        ? Bpl.Expr.True
-        : Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
+        ? (Bpl.Expr)Bpl.Expr.True
+        : Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)),
+          etran.FunctionContextHeight());
       // ante := (useViaContext && typeAnte && pre)
       ante = BplAnd(useViaContext, BplAnd(ante, pre));
 
@@ -3480,42 +3483,65 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder
         builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(en.E)));
       }
 
-      //generating assume C.F(ins) == out, if a result variable was given
-      if (resultVariable != null) {
-        var funcIdC = new FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
-        var argsC = new List<Bpl.Expr>();
-
-        // add type arguments
-        argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy));
-
-        // add fuel arguments
-        if (f.IsFuelAware()) {
-          argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));
-        }
-
-        // add heap arguments
-        if (f is TwoStateFunction) {
-          argsC.Add(etran.Old.HeapExpr);
-        }
-        if (AlwaysUseHeap || f.ReadsHeap) {
-          argsC.Add(etran.HeapExpr);
+      //generating assume J.F(ins) == C.F(ins)
+      Bpl.FunctionCall funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
+      Bpl.FunctionCall funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType)));
+      List<Bpl.Expr> argsC = new List<Bpl.Expr>();
+      List<Bpl.Expr> argsT = new List<Bpl.Expr>();
+      // add type arguments
+      argsT.AddRange(GetTypeArguments(f.OverriddenFunction, f).ConvertAll(TypeToTy));
+      argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy));
+      // add fuel arguments
+      if (f.IsFuelAware()) {
+        argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));
+      }
+      if (f.OverriddenFunction.IsFuelAware()) {
+        argsT.Add(etran.layerInterCluster.GetFunctionFuel(f));
+      }
+      // add heap arguments
+      if (f is TwoStateFunction) {
+        argsC.Add(etran.Old.HeapExpr);
+        argsT.Add(etran.Old.HeapExpr);
+      }
+      if (AlwaysUseHeap || f.ReadsHeap) {
+        argsC.Add(etran.HeapExpr);
+      }
+      if (AlwaysUseHeap || f.OverriddenFunction.ReadsHeap) {
+        argsT.Add(etran.HeapExpr);
+      }
+      // add "ordinary" parameters (including "this", if any)
+      var prefixCount = implInParams.Count - f.Formals.Count;
+      for (var i = 0; i < implInParams.Count; i++) {
+        Bpl.Expr cParam = new Bpl.IdentifierExpr(f.tok, implInParams[i]);
+        Bpl.Expr tParam = new Bpl.IdentifierExpr(f.OverriddenFunction.tok, implInParams[i]);
+        if (prefixCount <= i && ModeledAsBoxType(f.OverriddenFunction.Formals[i - prefixCount].Type)) {
+          tParam = BoxIfNecessary(f.tok, tParam, f.Formals[i - prefixCount].Type);
         }
+        argsC.Add(cParam);
+        argsT.Add(tParam);
+      }
+      Bpl.Expr funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
+      Bpl.Expr funcExpT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT);
+      var funcExpCPossiblyBoxed = funcExpC;
+      if (ModeledAsBoxType(f.OverriddenFunction.ResultType)) {
+        funcExpCPossiblyBoxed = BoxIfUnboxed(funcExpCPossiblyBoxed, f.ResultType);
+      }
+      builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpCPossiblyBoxed, funcExpT)));
 
-        argsC.AddRange(implInParams.Select(var => new Bpl.IdentifierExpr(f.tok, var)));
-
-        var funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
+      //generating assume C.F(ins) == out, if a result variable was given
+      if (resultVariable != null) {
         var resultVar = new Bpl.IdentifierExpr(resultVariable.tok, resultVariable);
         builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, resultVar)));
       }
 
       //generating trait post-conditions with class variables
       foreach (var en in f.OverriddenFunction.Ens) {
-        // We replace all occurrences of the trait version of the function with the class version. This is only allowed
-        // if the receiver is `this`. We underapproximate this by looking for a `ThisExpr`, which misses more complex
-        // expressions that evaluate to one.
-        var sub = new FunctionCallSubstituter(null, substMap, typeMap, f.OverriddenFunction, f);
-        foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) {
-          builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true)));
+        Expression postcond = Substitute(en.E, null, substMap, typeMap);
+        bool splitHappened;  // we don't actually care
+        foreach (var s in TrSplitExpr(postcond, etran, false, out splitHappened)) {
+          if (s.IsChecked) {
+            builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true)));
+          }
         }
       }
     }
@@ -4739,7 +4765,7 @@ Bpl.Expr CanCallAssumption(Expression expr, ExpressionTranslator etran) {
       Contract.Requires(predef != null);
       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
 
-      if (expr is LiteralExpr or ThisExpr or IdentifierExpr or WildcardExpr or BoogieWrapper) {
+      if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {
         return Bpl.Expr.True;
       } else if (expr is DisplayExpression) {
         DisplayExpression e = (DisplayExpression)expr;
@@ -10726,14 +10752,6 @@ List<Variable> MkTyParamFormals(List<TypeParameter> args, bool includeWhereClaus
       return null;
     }
 
-    // We use the $FunctionContextHeight to restrict the applicability of certain axioms. The entity at the end of a
-    // dependency chain has the highest number. To get more granular control over the visibility, we extend every
-    // visibility level by a precursory intermediate level. This additional level is helpful for proofs that would be
-    // disturbed by axioms that are visible the the final level.
-    static Bpl.Expr MkFunctionHeight(int visibilityLevel, bool intermediateScope = false) {
-      return Expr.Literal(visibilityLevel * 2 + (intermediateScope ? 0 : 1));
-    }
-
     public static void MapM<A>(IEnumerable<A> xs, Action<A> K) {
       Contract.Requires(xs != null);
       Contract.Requires(K != null);

diff --git a/Test/concurrency/10-SequenceInvariant.dfy b/Test/concurrency/10-SequenceInvariant.dfy
@@ -256,7 +256,7 @@ class Thread extends Object {
   }
   twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}
 
-  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
+  predicate localInv() reads * {
     && objectGlobalBaseInv()
   }
   predicate inv() reads * ensures inv() ==> localInv() {
@@ -322,7 +322,7 @@ trait OwnedObject extends Object {
     assert owner in universe.content;
   }
 
-  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
+  predicate localInv() reads * {
     && objectGlobalBaseInv()
     && localUserInv()
   }

diff --git a/Test/concurrency/11-MutexGuard2.dfy b/Test/concurrency/11-MutexGuard2.dfy
@@ -261,7 +261,7 @@ class Thread extends Object {
   }
   twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}
 
-  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
+  predicate localInv() reads * {
     && objectGlobalBaseInv()
   }
   predicate inv() reads * ensures inv() ==> localInv() {
@@ -332,7 +332,7 @@ trait OwnedObject extends Object {
     && unchangedNonvolatileUserFields()
   }
 
-  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
+  predicate localInv() reads * {
     && objectGlobalBaseInv()
     && localUserInv()
   }

diff --git a/Test/concurrency/12-MutexLifetime-short.dfy b/Test/concurrency/12-MutexLifetime-short.dfy
@@ -365,7 +365,7 @@ class Thread extends Object {
   }
   twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}
 
-  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
+  predicate localInv() reads * {
     && objectGlobalBaseInv()
   }
   predicate inv() reads * ensures inv() ==> localInv() {
@@ -439,7 +439,7 @@ trait OwnedObject extends Object {
     && unchangedNonvolatileUserFields()
   }
 
-  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
+  predicate localInv() reads * {
     && objectGlobalBaseInv()
     && this in lifetime.elements
     && (lifetime.alive() ==> owner != null)