fix: Correct null-related checking of type bounds, and add axioms

Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs

@@ -35,7 +35,7 @@ private NonNullTypeDecl(ClassLikeDecl cl, List<TypeParameter> tps, BoundVar id)
   }
 
   public override List<Type> ParentTypes(List<Type> typeArgs, bool includeTypeBounds) {
-    List<Type> result = new List<Type>(base.ParentTypes(typeArgs, includeTypeBounds));
+    var result = new List<Type>(base.ParentTypes(typeArgs, includeTypeBounds));
 
     foreach (var rhsParentType in Class.ParentTypes(typeArgs, includeTypeBounds)) {
       var rhsParentUdt = (UserDefinedType)rhsParentType; // all parent types of .Class are expected to be possibly-null class types

Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs

@@ -104,15 +104,19 @@ public void SetMembersBeforeResolution() {
     MembersBeforeResolution = Members.ToImmutableList();
   }
 
-  private List<Type> RawTraitsWithArgument(List<Type> typeArgs) {
+  public List<Type> RawTraitsWithArgument(List<Type> typeArgs) {
     Contract.Requires(typeArgs != null);
     Contract.Requires(typeArgs.Count == TypeArgs.Count);
     // Instantiate with the actual type arguments
     var subst = TypeParameter.SubstitutionMap(TypeArgs, typeArgs);
-    return ParentTraits.ConvertAll(traitType => {
+    var isReferenceType = this is ClassLikeDecl { IsReferenceTypeDecl: true };
+    var results = new List<Type>();
+    foreach (var traitType in ParentTraits) {
       var ty = (UserDefinedType)traitType.Subst(subst);
-      return (Type)UserDefinedType.CreateNullableTypeIfReferenceType(ty);
-    });
+      Contract.Assert(isReferenceType || !ty.IsRefType);
+      results.Add(UserDefinedType.CreateNullableTypeIfReferenceType(ty));
+    }
+    return results;
   }
 
   public override List<Type> ParentTypes(List<Type> typeArgs, bool includeTypeBounds) {

Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs

@@ -344,7 +344,7 @@ void CheckTypeInstantiation(IToken tok, string what, string className, List<Type
       VisitType(tok, actual, inGhostContext);
       foreach (var typeBound in formal.TypeBounds) {
         var bound = typeBound.Subst(typeMap);
-        if (!actual.IsSubtypeOf(bound, false, false)) {
+        if (!Type.IsSupertype(bound, actual) || (actual.IsRefType && !actual.IsNonNullRefType && !bound.IsRefType)) {
           var index = actualTypeArgs.Count == 1 ? "" : " " + i;
           reporter.Error(MessageSource.Resolver, tok,
             $"type parameter{index} ('{formal.Name}') passed to {what} '{className}' must meet type bound '{bound}' (got '{actual}')");

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -1414,6 +1414,9 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
           }
         }
 
+        // Check that type arguments satisfy their required
+        //   - type characteristics, and
+        //   - type bounds
         TypeCharacteristicChecker.InferAndCheck(declarations, isAnExport, reporter);
 
         // Check that functions claiming to be abstemious really are, and check that 'older' parameters are used only when allowed

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -1700,7 +1700,7 @@ void AddTypeBoundConstraints(IToken tok, List<TypeParameter> typeParameters, Dic
           var preTypeBoundWithSubst = preTypeBound.Substitute(subst);
           var actualPreType = subst[typeParameter];
           AddSubtypeConstraint(preTypeBoundWithSubst, actualPreType, tok,
-            $"actual type parameter '{{1}}' for formal type parameter '{typeParameter.Name}' must satisfy the type bound '{{0}}'");
+            $"actual type argument '{{1}}' for formal type parameter '{typeParameter.Name}' must satisfy the type bound '{{0}}'");
         }
       }
     }

Source/DafnyCore/Resolver/TailRecursion.cs

@@ -340,7 +340,7 @@ TailRecursionStatus ConfirmTailCall(IToken tok, Method method, List<Type> typeAp
       if (formal != actual) {
         if (reportErrors) {
           reporter.Error(MessageSource.Resolver, tok,
-            "the recursive call to '{0}' is not tail recursive because the actual type parameter{1} is not the formal type parameter '{2}'",
+            "the recursive call to '{0}' is not tail recursive because the actual type argument{1} is not the formal type parameter '{2}'",
             method.Name, method.TypeArgs.Count == 1 ? "" : " " + i, formal.Name);
         }
         return TailRecursionStatus.NotTailRecursive;

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -88,10 +88,10 @@ void AddClassMembers(TopLevelDeclWithMembers c, bool includeAllMethods, bool inc
       Add $Is and $IsAlloc for this class :
          axiom (forall p: ref, G: Ty ::
             { $Is(p, TClassA(G), h) }
-            $Is(p, TClassA(G), h) <=> (p == null || dtype(p) == TClassA(G));
+            $Is(p, TClassA(G), h) <==> (p == null || dtype(p) == TClassA(G));
          axiom (forall p: ref, h: Heap, G: Ty ::
             { $IsAlloc(p, TClassA(G), h) }
-            $IsAlloc(p, TClassA(G), h) => (p == null || h[p, alloc]);
+            $IsAlloc(p, TClassA(G), h) ==> (p == null || h[p, alloc]);
      */
     private void AddIsAndIsAllocForReferenceType(ClassLikeDecl c) {
       Contract.Requires(c.IsReferenceTypeDecl);
@@ -1898,43 +1898,51 @@ private void InsertChecksum(Method m, Boogie.Declaration decl, bool specificatio
 
     internal IEnumerable<Bpl.Expr> TypeBoundAxioms(IToken tok, List<TypeParameter> typeParameters) {
       foreach (var typeParameter in typeParameters.Where(typeParameter => typeParameter.TypeBounds.Any())) {
-        {
-          // (forall bx: Box ::
-          //   { $IsBox(bx, X) }
-          //   $IsBox(bx, X) ==>
-          //     $IsBox(bx, Bound0) && $IsBox(bx, Bound1) && ...);
-          var vars = new List<Bpl.Variable>();
-          var bx = BplBoundVar("bx", predef.BoxType, vars);
-          var isBox = MkIs(bx, new UserDefinedType(typeParameter));
-          Bpl.Expr bounds = Bpl.Expr.True;
-          foreach (var typeBound in typeParameter.TypeBounds) {
-            bounds = BplAnd(bounds, MkIs(bx, TypeToTy(typeBound), true));
-          }
+        TypeBoundAxiomExpressions(tok, new List<Variable>(), new UserDefinedType(typeParameter), typeParameter.TypeBounds,
+          out var isBoxExpr, out var isAllocBoxExpr);
+        yield return isBoxExpr;
+        yield return isAllocBoxExpr;
+      }
+    }
 
-          var body = BplImp(isBox, bounds);
-          var q = new Bpl.ForallExpr(tok, vars, BplTrigger(isBox), body);
-          yield return q;
+    public void TypeBoundAxiomExpressions(IToken tok, List<Bpl.Variable> bvarsTypeParameters, Type type, List<Type> typeBounds,
+      out Bpl.Expr isBoxExpr, out Bpl.Expr isAllocBoxExpr) {
+      {
+        // (forall bvarsTypeParameters, bx: Box ::
+        //   { $IsBox(bx, typeExpression) }
+        //   $IsBox(bx, typeExpression) ==>
+        //     $IsBox(bx, Bound0) && $IsBox(bx, Bound1) && ...);
+        var vars = new List<Bpl.Variable>();
+        vars.AddRange(bvarsTypeParameters);
+        var bx = BplBoundVar("bx", predef.BoxType, vars);
+        var isBox = MkIs(bx, TypeToTy(type), true);
+        Bpl.Expr bounds = Bpl.Expr.True;
+        foreach (var typeBound in typeBounds) {
+          bounds = BplAnd(bounds, MkIs(bx, TypeToTy(typeBound), true));
         }
 
-        {
-          // (forall bx: Box, $Heap: Heap ::
-          //   { $IsAllocBox(bx, X, $h) }
-          //   $IsAllocBox(bx, X, $h) && $IsGoodHeap($h) ==>
-          //     $IsAllocBox(bx, Bound0, $h) && $IsAllocBox(bx, Bound1, $h) && ...);
-          var vars = new List<Bpl.Variable>();
-          var bx = BplBoundVar("bx", predef.BoxType, vars);
-          var heap = BplBoundVar("$h", predef.HeapType, vars);
-          var isGoodHeap = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, heap);
-          var isAllocBox = MkIsAlloc(bx, new UserDefinedType(typeParameter), heap);
-          Bpl.Expr bounds = Bpl.Expr.True;
-          foreach (var typeBound in typeParameter.TypeBounds) {
-            bounds = BplAnd(bounds, MkIsAlloc(bx, TypeToTy(typeBound), heap, true));
-          }
+        var body = BplImp(isBox, bounds);
+        isBoxExpr = new Bpl.ForallExpr(tok, vars, BplTrigger(isBox), body);
+      }
 
-          var body = BplImp(BplAnd(isAllocBox, isGoodHeap), bounds);
-          var q = new Bpl.ForallExpr(tok, vars, BplTrigger(isAllocBox), body);
-          yield return q;
+      {
+        // (forall bx: Box, $Heap: Heap ::
+        //   { $IsAllocBox(bx, X, $h) }
+        //   $IsAllocBox(bx, X, $h) && $IsGoodHeap($h) ==>
+        //     $IsAllocBox(bx, Bound0, $h) && $IsAllocBox(bx, Bound1, $h) && ...);
+        var vars = new List<Bpl.Variable>();
+        vars.AddRange(bvarsTypeParameters);
+        var bx = BplBoundVar("bx", predef.BoxType, vars);
+        var heap = BplBoundVar("$h", predef.HeapType, vars);
+        var isGoodHeap = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, heap);
+        var isAllocBox = MkIsAlloc(bx, TypeToTy(type), heap, true);
+        Bpl.Expr bounds = Bpl.Expr.True;
+        foreach (var typeBound in typeBounds) {
+          bounds = BplAnd(bounds, MkIsAlloc(bx, TypeToTy(typeBound), heap, true));
         }
+
+        var body = BplImp(BplAnd(isAllocBox, isGoodHeap), bounds);
+        isAllocBoxExpr = new Bpl.ForallExpr(tok, vars, BplTrigger(isAllocBox), body);
       }
     }
   }

Source/DafnyCore/Verifier/BoogieGenerator.Types.cs

@@ -983,22 +983,28 @@ void AddRedirectingTypeDeclAxioms<T>(bool is_alloc, T dd, string fullName)
 
     Bpl.Expr body, is_o;
     string comment;
+    Trigger trigger;
 
     if (is_alloc) {
       comment = $"$IsAlloc axiom for {dd.WhatKind} {fullName}";
       var h = BplBoundVar("$h", predef.HeapType, vars);
       // $IsAlloc(o, ..)
       is_o = MkIsAlloc(o, o_ty, h, ModeledAsBoxType(baseType));
+      trigger = BplTrigger(is_o);
       if (baseType.IsNumericBased() || baseType.IsBitVectorType || baseType.IsBoolType || baseType.IsCharType) {
         body = is_o;
       } else {
         Bpl.Expr rhs = MkIsAlloc(o, baseType, h);
+        if (dd is NonNullTypeDecl) {
+          trigger.Next = BplTrigger(rhs);
+        }
         body = BplIff(is_o, rhs);
       }
     } else {
       comment = $"$Is axiom for {dd.WhatKind} {fullName}";
       // $Is(o, ..)
       is_o = MkIs(o, o_ty, ModeledAsBoxType(baseType));
+      trigger = BplTrigger(is_o);
       var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(dd.tok), null);
       Bpl.Expr parentConstraint, constraint;
       if (baseType.IsNumericBased() || baseType.IsBitVectorType || baseType.IsBoolType || baseType.IsCharType) {
@@ -1009,13 +1015,16 @@ void AddRedirectingTypeDeclAxioms<T>(bool is_alloc, T dd, string fullName)
         constraint = etran.TrExpr(ModuleResolver.GetImpliedTypeConstraint(substitutee, udt));
       } else {
         parentConstraint = MkIs(o, baseType);
+        if (dd is NonNullTypeDecl) {
+          trigger.Next = BplTrigger(parentConstraint);
+        }
         // conjoin the constraint
         constraint = etran.TrExpr(dd.Constraint ?? Expression.CreateBoolLiteral(dd.tok, true));
       }
       body = BplIff(is_o, BplAnd(parentConstraint, constraint));
     }
 
-    var axiom = new Bpl.Axiom(dd.tok, BplForall(vars, BplTrigger(is_o), body), comment);
+    var axiom = new Bpl.Axiom(dd.tok, BplForall(vars, trigger, body), comment);
     AddOtherDefinition(GetOrCreateTypeConstructor(dd), axiom);
   }
 

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -1074,50 +1074,58 @@ private void CreateRevealableConstant(Function f) {
     /// </summary>
     private void AddTraitParentAxioms() {
       foreach (ModuleDefinition m in program.RawModules()) {
-        foreach (TopLevelDecl d in m.TopLevelDecls) {
-          var c = d as TopLevelDeclWithMembers;
-          if (c == null || !RevealedInScope(d)) {
-            continue;
-          }
-          foreach (var parentType in c.ParentTraits) {
+        foreach (var c in m.TopLevelDecls.OfType<TopLevelDeclWithMembers>().Where(RevealedInScope)) {
+          foreach (var parentTypeInExtendsClause in c.ParentTraits) {
             var childType = UserDefinedType.FromTopLevelDecl(c.tok, c);
+            var parentType = (UserDefinedType)parentTypeInExtendsClause;
+            if (parentType.IsRefType) {
+              // use the nullable versions of the types
+              Contract.Assert(childType.IsRefType);
+              parentType = UserDefinedType.CreateNullableType(parentType);
+            } else {
+              childType = UserDefinedType.CreateNonNullTypeIfReferenceType(childType);
+            }
 
-            Bpl.Expr heap; var heapVar = BplBoundVar("$heap", predef.HeapType, out heap);
-            Bpl.Expr o; var oVar = BplBoundVar("$o", TrType(childType), out o);
-            Bpl.Expr oNotNull = childType.IsRefType ? Bpl.Expr.Neq(o, predef.Null) : Bpl.Expr.True;
+            var bvarsTypeParameters = MkTyParamBinders(GetTypeParams(c), out _);
 
-            var oj = BoxifyForTraitParent(c.tok, o, ((UserDefinedType)parentType.NormalizeExpand()).ResolvedClass, childType);
+            // axioms with "$IsBox(...) ==> ..." and "$IsAllocBox(...) ==> ..."
+            TypeBoundAxiomExpressions(c.tok, bvarsTypeParameters, childType, new List<Type>() { parentType },
+              out var isBoxExpr, out var isAllocBoxExpr);
+
+            var heapVar = BplBoundVar("$heap", predef.HeapType, out var heap);
+            var oVar = BplBoundVar("$o", TrType(childType), out var o);
 
-            List<Bpl.Expr> tyexprs;
-            var bvarsTypeParameters = MkTyParamBinders(GetTypeParams(c), out tyexprs);
+            var oj = BoxifyForTraitParent(c.tok, o, ((UserDefinedType)parentType.NormalizeExpand()).ResolvedClass, childType);
 
             // axiom (forall T: Ty, $o: ref ::
             //     { $Is($o, C(T)) }
-            //     $o != null && $Is($o, C(T)) ==> $Is($o, J(G(T)));
+            //     $Is($o, C(T)) ==> $Is($o, J(G(T)));
             var isC = MkIs(o, childType);
             var isJ = MkIs(oj, parentType);
             var bvs = new List<Bpl.Variable>();
             bvs.AddRange(bvarsTypeParameters);
             bvs.Add(oVar);
             var tr = BplTrigger(isC);
-            var body = BplImp(BplAnd(oNotNull, isC), isJ);
+            var body = BplImp(isC, isJ);
 
             sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, new Bpl.ForallExpr(c.tok, bvs, tr, body),
-              $"type axiom for trait parent: {d} extends {parentType}"));
+              $"type axiom for trait parent: {childType.Name} extends {parentType}"));
+            sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, isBoxExpr));
 
             // axiom (forall T: Ty, $Heap: Heap, $o: ref ::
             //     { $IsAlloc($o, C(T), $Heap) }
-            //     $o != null && $IsAlloc($o, C(T), $Heap) ==> $IsAlloc($o, J(G(T)), $Heap);
+            //     $IsAlloc($o, C(T), $Heap) ==> $IsAlloc($o, J(G(T)), $Heap);
             var isAllocC = MkIsAlloc(o, childType, heap);
             var isAllocJ = MkIsAlloc(oj, parentType, heap);
             bvs = new List<Bpl.Variable>();
             bvs.AddRange(bvarsTypeParameters);
             bvs.Add(oVar);
             bvs.Add(heapVar);
             tr = BplTrigger(isAllocC);
-            body = BplImp(BplAnd(oNotNull, isAllocC), isAllocJ);
+            body = BplImp(isAllocC, isAllocJ);
             sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, new Bpl.ForallExpr(c.tok, bvs, tr, body),
-              $"allocation axiom for trait parent: {d} extends {parentType}"));
+              $"allocation axiom for trait parent: {childType.Name} extends {parentType}"));
+            sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, isAllocBoxExpr));
           }
         }
       }