fix: Make verifier understand (!new) (#1935)

Make the verifier understand that a type marked with `(!new)` is considered allocated in any state. Also, this PR fixes a bug in the compilation of iterators to C#, JavaScript, and Go. The bug had caused malformed code for in-parameters of an iterator, in the case when the type of such an in-parameter was not an auto-init type.
dafny-lang · Apr 13, 2022 · 81cf582 · 81cf582
1 parent 811c966
commit 81cf582
Show file tree

Hide file tree

Showing 13 changed files with 150 additions and 51 deletions.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -13,7 +13,8 @@
 - feat: The dafny language server now returns expressions ranges instead of token ranges to better report errors (https://github.com/dafny-lang/dafny/pull/1985)
 - fix: Comprehensions with nested subset types fully supported, subtype is correctly checked (https://github.com/dafny-lang/dafny/pull/1997)
 - fix: Fix induction hypothesis generated for lemmas with a receiver parameter (https://github.com/dafny-lang/dafny/pull/2002)
-
+- fix: Make verifier understand `(!new)` (https://github.com/dafny-lang/dafny/pull/1935)
+- fix: Fix initialization of non-auto-init in-parameters in C#/JavaScript/Go compilers (https://github.com/dafny-lang/dafny/pull/1935)
 
 # 3.5.0
 

diff --git a/Source/Dafny/Compilers/Compiler-Csharp.cs b/Source/Dafny/Compilers/Compiler-Csharp.cs
@@ -373,7 +373,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete
 
  foreach (var member in iter.Members) {
  if (member is Field f && !f.IsGhost) {
- cw.DeclareField(IdName(f), iter, false, false, f.Type, f.tok, DefaultValue(f.Type, w, f.tok, true), f);
+ cw.DeclareField(IdName(f), iter, false, false, f.Type, f.tok, PlaceboValue(f.Type, w, f.tok, true), f);
  }
  }
 

diff --git a/Source/Dafny/Compilers/Compiler-go.cs b/Source/Dafny/Compilers/Compiler-go.cs
@@ -425,7 +425,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete
  Constructor ct = null;
  foreach (var member in iter.Members) {
  if (member is Field f && !f.IsGhost) {
- cw.DeclareField(IdName(f), iter, false, false, f.Type, f.tok, DefaultValue(f.Type, wr, f.tok, true), f);
+ cw.DeclareField(IdName(f), iter, false, false, f.Type, f.tok, PlaceboValue(f.Type, wr, f.tok, true), f);
  } else if (member is Constructor c) {
  Contract.Assert(ct == null);
  ct = c;

diff --git a/Source/Dafny/Compilers/Compiler-js.cs b/Source/Dafny/Compilers/Compiler-js.cs
@@ -154,7 +154,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete
  foreach (var member in iter.Members) {
  var f = member as Field;
  if (f != null && !f.IsGhost) {
- DeclareField(IdName(f), false, false, f.Type, f.tok, DefaultValue(f.Type, instanceFieldsWriter, f.tok, true), instanceFieldsWriter);
+ DeclareField(IdName(f), false, false, f.Type, f.tok, PlaceboValue(f.Type, instanceFieldsWriter, f.tok, true), instanceFieldsWriter);
  } else if (member is Constructor) {
  Contract.Assert(ct == null); // we're expecting just one constructor
  ct = (Constructor)member;

diff --git a/Source/Dafny/DafnyPrelude.bpl b/Source/Dafny/DafnyPrelude.bpl
@@ -277,7 +277,7 @@ function $Is<T>(T,Ty): bool uses { // no heap for now
  $Is(IMap#Values(v), TISet(t1)) &&
  $Is(IMap#Items(v), TISet(Tclass._System.Tuple2(t0, t1))));
 }
-function  $IsAlloc<T>(T,Ty,Heap): bool uses {
+function $IsAlloc<T>(T,Ty,Heap): bool uses {
  axiom(forall h : Heap, v : int :: { $IsAlloc(v,TInt,h) } $IsAlloc(v,TInt,h));
  axiom(forall h : Heap, v : real :: { $IsAlloc(v,TReal,h) } $IsAlloc(v,TReal,h));
  axiom(forall h : Heap, v : bool :: { $IsAlloc(v,TBool,h) } $IsAlloc(v,TBool,h));
@@ -323,6 +323,12 @@ function $IsAlloc<T>(T,Ty,Heap): bool uses {
  $IsAllocBox(bx, t0, h)));
 }
 
+function $AlwaysAllocated(Ty): bool uses {
+ axiom (forall ty: Ty :: { $AlwaysAllocated(ty) }
+ $AlwaysAllocated(ty) ==>
+ (forall h: Heap, v: Box :: { $IsAllocBox(v, ty, h) } $IsBox(v, ty) ==> $IsAllocBox(v, ty, h)));
+}
+
 // ---------------------------------------------------------------
 // -- Encoding of type names -------------------------------------
 // ---------------------------------------------------------------

diff --git a/Source/Dafny/Verifier/Translator.BoogieFactory.cs b/Source/Dafny/Verifier/Translator.BoogieFactory.cs
@@ -817,8 +817,7 @@ static Bpl.Axiom BplAxiom(Bpl.Expr e) {
  }
 
  static Bpl.Expr BplLocalVar(string name, Bpl.Type ty, List<Bpl.Variable> lvars) {
- Bpl.Expr v;
- lvars.Add(BplLocalVar(name, ty, out v));
+ lvars.Add(BplLocalVar(name, ty, out var v));
  return v;
  }
 
@@ -846,30 +845,26 @@ static Bpl.BoundVariable BplBoundVar(string name, Bpl.Type ty, out Bpl.Expr e) {
  }
 
  static Bpl.Expr BplBoundVar(string name, Bpl.Type ty, List<Bpl.Variable> bvars) {
- Bpl.Expr e;
- bvars.Add(BplBoundVar(name, ty, out e));
+ bvars.Add(BplBoundVar(name, ty, out var e));
  return e;
  }
 
  // Makes a formal variable
  static Bpl.Formal BplFormalVar(string/*?*/ name, Bpl.Type ty, bool incoming) {
- Bpl.Expr _scratch;
- return BplFormalVar(name, ty, incoming, out _scratch);
+ return BplFormalVar(name, ty, incoming, out _);
  }
 
- static Bpl.Formal BplFormalVar(string/*?*/ name, Bpl.Type ty, bool incoming, out Bpl.Expr e) {
- Bpl.Formal res;
+ static Bpl.Formal BplFormalVar(string/*?*/ name, Bpl.Type ty, bool incoming, out Bpl.Expr e, Bpl.Expr whereClause = null) {
  if (name == null) {
  name = Bpl.TypedIdent.NoName;
  }
- res = new Bpl.Formal(ty.tok, new Bpl.TypedIdent(ty.tok, name, ty), incoming);
+ var res = new Bpl.Formal(ty.tok, new Bpl.TypedIdent(ty.tok, name, ty, whereClause), incoming);
  e = new Bpl.IdentifierExpr(ty.tok, res);
  return res;
  }
 
  static Bpl.Expr BplFormalVar(string name, Bpl.Type ty, bool incoming, List<Bpl.Variable> fvars) {
- Bpl.Expr e;
- fvars.Add(BplFormalVar(name, ty, incoming, out e));
+ fvars.Add(BplFormalVar(name, ty, incoming, out var e));
  return e;
  }
  }

diff --git a/Source/Dafny/Verifier/Translator.ClassMembers.cs b/Source/Dafny/Verifier/Translator.ClassMembers.cs
@@ -28,7 +28,7 @@ void AddClassMembers(TopLevelDeclWithMembers c, bool includeAllMethods) {
  //this adds: function implements$J(Ty, typeArgs): bool;
  var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, "ty", predef.Ty), true);
  var vars = new List<Bpl.Variable> { arg_ref };
- vars.AddRange(MkTyParamFormals(GetTypeParams(c)));
+ vars.AddRange(MkTyParamFormals(GetTypeParams(c), false));
  var res = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
  var implement_intr = new Bpl.Function(c.tok, "implements$" + c.FullSanitizedName, vars, res);
  sink.AddTopLevelDeclaration(implement_intr);
@@ -842,7 +842,7 @@ private void AddFunctionOverrideCheckImpl(Function f) {
  }
 
  // parameters of the procedure
- var typeInParams = MkTyParamFormals(GetTypeParams(f));
+ var typeInParams = MkTyParamFormals(GetTypeParams(f), true);
  var inParams = new List<Variable>();
  var outParams = new List<Boogie.Variable>();
  if (!f.IsStatic) {

diff --git a/Source/Dafny/Verifier/Translator.DataTypes.cs b/Source/Dafny/Verifier/Translator.DataTypes.cs
@@ -212,7 +212,7 @@ private void AddCoDatatypeDeclAxioms(CoDatatypeDecl codecl) {
  Action<Bpl.Type> AddAxioms = typeOfK => {
  {
  // Add two copies of the type parameter lists!
- var args = MkTyParamFormals(Concat(GetTypeParams(codecl), GetTypeParams(codecl)), false);
+ var args = MkTyParamFormals(Concat(GetTypeParams(codecl), GetTypeParams(codecl)), false, false);
  if (typeOfK != null) {
  args.Add(BplFormalVar(null, typeOfK, true));
  }

diff --git a/Source/Dafny/Verifier/Translator.cs b/Source/Dafny/Verifier/Translator.cs
@@ -1132,7 +1132,7 @@ public Expr TypeSpecificEqual(IToken tok, Dafny.Type type, Expr e0, Expr e1) {
  }
  }
 
- void AddTypeDecl_Aux(IToken tok, string nm, List<TypeParameter> typeArgs) {
+ void AddTypeDecl_Aux(IToken tok, string nm, List<TypeParameter> typeArgs, TypeParameter.TypeParameterCharacteristics characteristics) {
  Contract.Requires(tok != null);
  Contract.Requires(nm != null);
  Contract.Requires(typeArgs != null);
@@ -1142,29 +1142,43 @@ void AddTypeDecl_Aux(IToken tok, string nm, List<TypeParameter> typeArgs) {
  return;
  }
  if (typeArgs.Count == 0) {
- sink.AddTopLevelDeclaration(
- new Bpl.Constant(tok,
- new TypedIdent(tok, nm, predef.Ty), false /* not unique */));
+ var c = new Bpl.Constant(tok, new TypedIdent(tok, nm, predef.Ty), false /* not unique */);
+ sink.AddTopLevelDeclaration(c);
+ var whereClause = GetTyWhereClause(new Bpl.IdentifierExpr(tok, nm, predef.Ty), characteristics);
+ if (whereClause != null) {
+ AddOtherDefinition(c, BplAxiom(whereClause));
+ }
+
  } else {
  // Note, the function produced is NOT necessarily injective, because the type may be replaced
  // in a refinement module in such a way that the type arguments do not matter.
  var args = new List<Bpl.Variable>(typeArgs.ConvertAll(a => (Bpl.Variable)BplFormalVar(null, predef.Ty, true)));
  var func = new Bpl.Function(tok, nm, args, BplFormalVar(null, predef.Ty, false));
  sink.AddTopLevelDeclaration(func);
+ // axiom (forall T0, T1, ... { T(T0, T1, T2) } :: WhereClause( T(T0, T1, T2) ));
+ var argBoundVars = new List<Bpl.Variable>();
+ var argExprs = typeArgs.ConvertAll(ta => BplBoundVar(ta.Name, predef.Ty, argBoundVars));
+ var funcAppl = FunctionCall(tok, nm, predef.Ty, argExprs);
+ var whereClause = GetTyWhereClause(funcAppl, characteristics);
+ if (whereClause != null) {
+ var tr = new Bpl.Trigger(tok, true, new List<Bpl.Expr> { funcAppl });
+ var axiom = BplAxiom(new Bpl.ForallExpr(tok, new List<Bpl.TypeVariable>(), argBoundVars, null, tr, whereClause));
+ AddOtherDefinition(func, axiom);
+ }
  }
  abstractTypes.Add(nm);
  }
 
  void AddTypeDecl(OpaqueTypeDecl td) {
  Contract.Requires(td != null);
- AddTypeDecl_Aux(td.tok, nameTypeParam(td), td.TypeArgs);
+ AddTypeDecl_Aux(td.tok, nameTypeParam(td), td.TypeArgs, td.Characteristics);
  }
 
 
  void AddTypeDecl(InternalTypeSynonymDecl td) {
  Contract.Requires(td != null);
  Contract.Requires(!RevealedInScope(td));
- AddTypeDecl_Aux(td.tok, "#$" + td.Name, td.TypeArgs);
+ AddTypeDecl_Aux(td.tok, "#$" + td.Name, td.TypeArgs, td.Characteristics);
  }
 
  void AddTypeDecl(RevealableTypeDecl d) {
@@ -4013,7 +4027,7 @@ private void AddWellformednessCheck(Function f) {
  }
 
  // parameters of the procedure
- var typeInParams = MkTyParamFormals(GetTypeParams(f));
+ var typeInParams = MkTyParamFormals(GetTypeParams(f), true);
  var inParams = new List<Bpl.Variable>();
  var outParams = new List<Bpl.Variable>();
  if (!f.IsStatic) {
@@ -4185,8 +4199,8 @@ private void AddWellformednessCheck(Function f) {
  // don't fall through to postcondition checks
  bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Bpl.Expr.False));
  } else {
- Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
- List<Bpl.Expr> args = new List<Bpl.Expr>();
+ var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
+ var args = new List<Bpl.Expr>();
  foreach (var p in GetTypeParams(f)) {
  args.Add(trTypeParamOrOpaqueType(p));
  }
@@ -4230,7 +4244,9 @@ private void AddWellformednessCheck(Function f) {
  // emit the impl only when there are proof obligations.
  QKeyValue kv = etran.TrAttributes(f.Attributes, null);
  var impl = new Bpl.Implementation(f.tok, proc.Name,
- new List<Bpl.TypeVariable>(), Concat(Concat(typeInParams, inParams_Heap), implInParams), implOutParams,
+ new List<Bpl.TypeVariable>(),
+ Concat(Concat(Bpl.Formal.StripWhereClauses(typeInParams), inParams_Heap), implInParams),
+ implOutParams,
  locals, implBody, kv);
  sink.AddTopLevelDeclaration(impl);
  if (InsertChecksums) {
@@ -4268,7 +4284,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) {
  var etran = new ExpressionTranslator(this, predef, decl.tok);
 
  // parameters of the procedure
- var inParams = MkTyParamFormals(decl.TypeArgs);
+ var inParams = MkTyParamFormals(decl.TypeArgs, true);
  Bpl.Type varType = TrType(decl.Var.Type);
  Bpl.Expr wh = GetWhereClause(decl.Var.tok, new Bpl.IdentifierExpr(decl.Var.tok, decl.Var.AssignUniqueName(decl.IdGenerator), varType), decl.Var.Type, etran, NOALLOC);
  inParams.Add(new Bpl.Formal(decl.Var.tok, new Bpl.TypedIdent(decl.Var.tok, decl.Var.AssignUniqueName(decl.IdGenerator), varType, wh), true));
@@ -4416,7 +4432,7 @@ void AddWellformednessCheck(ConstantField decl) {
  var etran = new ExpressionTranslator(this, predef, decl.tok);
 
  // parameters of the procedure
- List<Variable> inParams = MkTyParamFormals(GetTypeParams(decl.EnclosingClass));
+ List<Variable> inParams = MkTyParamFormals(GetTypeParams(decl.EnclosingClass), true);
  if (!decl.IsStatic) {
  var receiverType = Resolver.GetThisType(decl.tok, (TopLevelDeclWithMembers)decl.EnclosingClass);
  Contract.Assert(VisibleInScope(receiverType));
@@ -4494,7 +4510,7 @@ void AddWellformednessCheck(DatatypeCtor ctor) {
  var etran = new ExpressionTranslator(this, predef, ctor.tok);
 
  // parameters of the procedure
- List<Variable> inParams = MkTyParamFormals(GetTypeParams(ctor.EnclosingDatatype));
+ List<Variable> inParams = MkTyParamFormals(GetTypeParams(ctor.EnclosingDatatype), true);
  foreach (var p in ctor.Formals) {
  Bpl.Type varType = TrType(p.Type);
  Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(ctor.IdGenerator), varType), p.Type, etran, NOALLOC);
@@ -7637,7 +7653,7 @@ Bpl.Function GetReadonlyField(Field f) {
  // function f(Ref): ty;
  List<Variable> formals = new List<Variable>();
  if (f is ConstantField) {
- formals.AddRange(MkTyParamFormals(GetTypeParams(f.EnclosingClass)));
+ formals.AddRange(MkTyParamFormals(GetTypeParams(f.EnclosingClass), false));
  }
  if (!f.IsStatic) {
  var udt = UserDefinedType.FromTopLevelDecl(f.tok, f.EnclosingClass);
@@ -7707,7 +7723,7 @@ Bpl.Function GetOrCreateFunction(Function f) {
  Bpl.Function func;
  {
  var formals = new List<Variable>();
- formals.AddRange(MkTyParamFormals(GetTypeParams(f)));
+ formals.AddRange(MkTyParamFormals(GetTypeParams(f), false));
  if (f.IsFuelAware()) {
  formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType), true));
  }
@@ -7734,7 +7750,7 @@ Bpl.Function GetOrCreateFunction(Function f) {
  // declare the corresponding canCall function
  {
  var formals = new List<Variable>();
- formals.AddRange(MkTyParamFormals(GetTypeParams(f)));
+ formals.AddRange(MkTyParamFormals(GetTypeParams(f), false));
  if (f is TwoStateFunction) {
  formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", predef.HeapType), true));
  }
@@ -7825,7 +7841,7 @@ private void GenerateMethodParametersChoose(IToken tok, IMethodCodeContext m, Me
  ExpressionTranslator etran, List<Variable> inParams, out List<Variable> outParams) {
  outParams = new List<Variable>();
  // Add type parameters first, always!
- inParams.AddRange(MkTyParamFormals(GetTypeParams(m)));
+ inParams.AddRange(MkTyParamFormals(GetTypeParams(m), true));
  if (includeReceiver) {
  var receiverType = m is MemberDecl ? Resolver.GetReceiverType(tok, (MemberDecl)m) : Resolver.GetThisType(tok, (IteratorDecl)m);
  Contract.Assert(VisibleInScope(receiverType));
@@ -11775,39 +11791,44 @@ public override BinderExpr VisitBinderExpr(BinderExpr node) {
  }
 
  List<Bpl.Variable> MkTyParamBinders(List<TypeParameter> args) {
- List<Bpl.Expr> _scratch;
- return MkTyParamBinders(args, out _scratch);
+ return MkTyParamBinders(args, out _);
  }
 
  List<Bpl.Variable> MkTyParamBinders(List<TypeParameter> args, out List<Bpl.Expr> exprs) {
- List<Bpl.Variable> vars = new List<Bpl.Variable>();
+ var vars = new List<Bpl.Variable>();
  exprs = new List<Bpl.Expr>();
  foreach (TypeParameter v in args) {
- Bpl.Expr e;
- vars.Add(BplBoundVar(nameTypeParam(v), predef.Ty, out e));
+ vars.Add(BplBoundVar(nameTypeParam(v), predef.Ty, out var e));
  exprs.Add(e);
  }
  return vars;
  }
 
  // For incoming formals
- List<Bpl.Variable> MkTyParamFormals(List<TypeParameter> args, bool named = true) {
- List<Bpl.Expr> _scratch;
- return MkTyParamFormals(args, out _scratch, named);
+ List<Variable> MkTyParamFormals(List<TypeParameter> args, bool includeWhereClause, bool named = true) {
+ return MkTyParamFormals(args, out _, includeWhereClause, named);
  }
 
  // For incoming formals
- List<Bpl.Variable> MkTyParamFormals(List<TypeParameter> args, out List<Bpl.Expr> exprs, bool named = true) {
- List<Bpl.Variable> vars = new List<Bpl.Variable>();
+ List<Bpl.Variable> MkTyParamFormals(List<TypeParameter> args, out List<Bpl.Expr> exprs, bool includeWhereClause, bool named) {
+ var vars = new List<Bpl.Variable>();
  exprs = new List<Bpl.Expr>();
  foreach (TypeParameter v in args) {
- Bpl.Expr e;
- vars.Add(BplFormalVar(named ? nameTypeParam(v) : null, predef.Ty, true, out e));
+ var whereClause = includeWhereClause ? GetTyWhereClause(new Bpl.IdentifierExpr(v.tok, nameTypeParam(v), predef.Ty), v.Characteristics) : null;
+ vars.Add(BplFormalVar(named ? nameTypeParam(v) : null, predef.Ty, true, out var e, whereClause));
  exprs.Add(e);
  }
  return vars;
  }
 
+ public Bpl.Expr/*?*/ GetTyWhereClause(Bpl.Expr expr, TypeParameter.TypeParameterCharacteristics characteristics) {
+ Contract.Requires(expr != null);
+ if (characteristics.ContainsNoReferenceTypes) {
+ return FunctionCall(expr.tok, "$AlwaysAllocated", Bpl.Type.Bool, expr);
+ }
+ return null;
+ }
+
  public static void MapM<A>(IEnumerable<A> xs, Action<A> K) {
  Contract.Requires(xs != null);
  Contract.Requires(K != null);

diff --git a/Test/comp/Iterators.dfy b/Test/comp/Iterators.dfy
@@ -10,6 +10,7 @@ class C {
  print "hello, instance\n";
  print "x is ", x, "\n";
  Client();
+ RegressionClient();
  }
 }
 
@@ -61,3 +62,19 @@ method Client()
  }
  print "\n";
 }
+
+method RegressionClient() {
+ var c := new C;
+ var d := new C;
+ var iter := new RegressionDefaultVsPlaceboInitialization(c, d);
+ var more := iter.MoveNext();
+ if more {
+ print iter.eq, "\n"; // false
+ }
+}
+
+// The following iterator needs to initialize its .x and .y fields with placebos, not default values.
+// In the past, default values had been used, which causes malformed code that refers to a non-existing type descriptor.
+iterator RegressionDefaultVsPlaceboInitialization<X(==)>(x: X, y: X) yields (eq: bool) {
+ yield x == y;
+}
diff --git a/Test/comp/Iterators.dfy.expect b/Test/comp/Iterators.dfy.expect
@@ -1,18 +1,21 @@
 
-Dafny program verifier finished with 5 verified, 0 errors
+Dafny program verifier finished with 8 verified, 0 errors
 hello, instance
 x is 0
 0.0 1.0 2.0 3.0 4.0 5.0 
 0.0 1.0 2.0 
+false
 
-Dafny program verifier finished with 5 verified, 0 errors
+Dafny program verifier finished with 8 verified, 0 errors
 hello, instance
 x is 0
 0.0 1.0 2.0 3.0 4.0 5.0 
 0.0 1.0 2.0 
+false
 
-Dafny program verifier finished with 5 verified, 0 errors
+Dafny program verifier finished with 8 verified, 0 errors
 hello, instance
 x is 0
 0.0 1.0 2.0 3.0 4.0 5.0 
 0.0 1.0 2.0 
+false