diff --git a/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs index f98620fdddc..0d5466b02fd 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs @@ -15,25 +15,25 @@ public class MemberSelectExpr : Expression, IHasReferences, ICloneable - [FilledInDuringResolution] public List PreTypeApplication_AtEnclosingClass; + [FilledInDuringResolution] public List PreTypeApplicationAtEnclosingClass; /// /// PreTypeApplication_JustMember is the list of type arguments used to instantiate the type parameters /// of Member. /// - [FilledInDuringResolution] public List PreTypeApplication_JustMember; + [FilledInDuringResolution] public List PreTypeApplicationJustMember; /// /// TypeApplication_AtEnclosingClass is the list of type arguments used to instantiate the type that /// declares Member (which is some supertype of the receiver type). /// - [FilledInDuringResolution] public List TypeApplication_AtEnclosingClass; + [FilledInDuringResolution] public List TypeApplicationAtEnclosingClass; /// /// TypeApplication_JustMember is the list of type arguments used to instantiate the type parameters /// of Member. /// - [FilledInDuringResolution] public List TypeApplication_JustMember; + [FilledInDuringResolution] public List TypeApplicationJustMember; /// /// Returns a mapping from formal type parameters to actual type arguments. For example, given @@ -54,21 +54,21 @@ public Dictionary TypeArgumentSubstitutionsAtMemberDeclarat // Add the mappings from the member's own type parameters if (Member is ICallable icallable) { - Contract.Assert(TypeApplication_JustMember.Count == icallable.TypeArgs.Count); + Contract.Assert(TypeApplicationJustMember.Count == icallable.TypeArgs.Count); for (var i = 0; i < icallable.TypeArgs.Count; i++) { - subst.Add(icallable.TypeArgs[i], TypeApplication_JustMember[i]); + subst.Add(icallable.TypeArgs[i], TypeApplicationJustMember[i]); } } else { - Contract.Assert(TypeApplication_JustMember.Count == 0); + Contract.Assert(TypeApplicationJustMember.Count == 0); } // Add the mappings from the enclosing class. TopLevelDecl cl = Member.EnclosingClass; // Expand the type down to its non-null type, if any if (cl != null) { - Contract.Assert(cl.TypeArgs.Count == TypeApplication_AtEnclosingClass.Count); + Contract.Assert(cl.TypeArgs.Count == TypeApplicationAtEnclosingClass.Count); for (var i = 0; i < cl.TypeArgs.Count; i++) { - subst.Add(cl.TypeArgs[i], TypeApplication_AtEnclosingClass[i]); + subst.Add(cl.TypeArgs[i], TypeApplicationAtEnclosingClass[i]); } } @@ -94,21 +94,21 @@ public Dictionary PreTypeArgumentSubstitutionsAtMemberDe // Add the mappings from the member's own type parameters if (Member is ICallable icallable) { - Contract.Assert(PreTypeApplication_JustMember.Count == icallable.TypeArgs.Count); + Contract.Assert(PreTypeApplicationJustMember.Count == icallable.TypeArgs.Count); for (var i = 0; i < icallable.TypeArgs.Count; i++) { - subst.Add(icallable.TypeArgs[i], PreTypeApplication_JustMember[i]); + subst.Add(icallable.TypeArgs[i], PreTypeApplicationJustMember[i]); } } else { - Contract.Assert(PreTypeApplication_JustMember.Count == 0); + Contract.Assert(PreTypeApplicationJustMember.Count == 0); } // Add the mappings from the enclosing class. TopLevelDecl cl = Member.EnclosingClass; // Expand the type down to its non-null type, if any if (cl != null) { - Contract.Assert(cl.TypeArgs.Count == PreTypeApplication_AtEnclosingClass.Count); + Contract.Assert(cl.TypeArgs.Count == PreTypeApplicationAtEnclosingClass.Count); for (var i = 0; i < cl.TypeArgs.Count; i++) { - subst.Add(cl.TypeArgs[i], PreTypeApplication_AtEnclosingClass[i]); + subst.Add(cl.TypeArgs[i], PreTypeApplicationAtEnclosingClass[i]); } } @@ -134,7 +134,7 @@ public Dictionary TypeArgumentSubstitutionsWithParents() { Contract.Requires(WasResolved()); Contract.Ensures(Contract.Result>() != null); - return TypeArgumentSubstitutionsWithParentsAux(Obj.Type, Member, TypeApplication_JustMember); + return TypeArgumentSubstitutionsWithParentsAux(Obj.Type, Member, TypeApplicationJustMember); } public static Dictionary TypeArgumentSubstitutionsWithParentsAux(Type receiverType, MemberDecl member, List typeApplicationMember) { @@ -193,8 +193,8 @@ public static Dictionary TypeArgumentSubstitutionsWithParen void ObjectInvariant() { Contract.Invariant(Obj != null); Contract.Invariant(MemberName != null); - Contract.Invariant((Member != null) == (TypeApplication_AtEnclosingClass != null)); // TypeApplication_* are set whenever Member is set - Contract.Invariant((Member != null) == (TypeApplication_JustMember != null)); // TypeApplication_* are set whenever Member is set + Contract.Invariant((Member != null) == (TypeApplicationAtEnclosingClass != null)); // TypeApplication_* are set whenever Member is set + Contract.Invariant((Member != null) == (TypeApplicationJustMember != null)); // TypeApplication_* are set whenever Member is set } public MemberSelectExpr Clone(Cloner cloner) { @@ -209,8 +209,8 @@ public MemberSelectExpr(Cloner cloner, MemberSelectExpr original) : base(cloner, Member = cloner.CloneMember(original.Member, true); AtLabel = original.AtLabel; InCompiledContext = original.InCompiledContext; - TypeApplication_AtEnclosingClass = original.TypeApplication_AtEnclosingClass; - TypeApplication_JustMember = original.TypeApplication_JustMember; + TypeApplicationAtEnclosingClass = original.TypeApplicationAtEnclosingClass; + TypeApplicationJustMember = original.TypeApplicationJustMember; } } @@ -236,16 +236,16 @@ public MemberSelectExpr(IToken tok, Expression obj, Field field) this.Member = field; // resolve here var receiverType = obj.Type.NormalizeExpand(); - this.TypeApplication_AtEnclosingClass = receiverType.TypeArgs; - this.TypeApplication_JustMember = new List(); + this.TypeApplicationAtEnclosingClass = receiverType.TypeArgs; + this.TypeApplicationJustMember = new List(); var typeMap = new Dictionary(); if (receiverType is UserDefinedType udt) { var cl = udt.ResolvedClass as TopLevelDeclWithMembers; Contract.Assert(cl != null); - Contract.Assert(cl.TypeArgs.Count == TypeApplication_AtEnclosingClass.Count); + Contract.Assert(cl.TypeArgs.Count == TypeApplicationAtEnclosingClass.Count); for (var i = 0; i < cl.TypeArgs.Count; i++) { - typeMap.Add(cl.TypeArgs[i], TypeApplication_AtEnclosingClass[i]); + typeMap.Add(cl.TypeArgs[i], TypeApplicationAtEnclosingClass[i]); } foreach (var entry in cl.ParentFormalTypeParametersToActuals) { var v = entry.Value.Subst(typeMap); @@ -254,9 +254,9 @@ public MemberSelectExpr(IToken tok, Expression obj, Field field) } else if (field.EnclosingClass == null) { // leave typeMap as the empty substitution } else { - Contract.Assert(field.EnclosingClass.TypeArgs.Count == TypeApplication_AtEnclosingClass.Count); + Contract.Assert(field.EnclosingClass.TypeArgs.Count == TypeApplicationAtEnclosingClass.Count); for (var i = 0; i < field.EnclosingClass.TypeArgs.Count; i++) { - typeMap.Add(field.EnclosingClass.TypeArgs[i], TypeApplication_AtEnclosingClass[i]); + typeMap.Add(field.EnclosingClass.TypeArgs[i], TypeApplicationAtEnclosingClass[i]); } } this.Type = field.Type.Subst(typeMap); // resolve here @@ -289,7 +289,7 @@ public override IEnumerable SubExpressions { get { yield return Obj; } } - public override IEnumerable ComponentTypes => Util.Concat(TypeApplication_AtEnclosingClass, TypeApplication_JustMember); + public override IEnumerable ComponentTypes => Util.Concat(TypeApplicationAtEnclosingClass, TypeApplicationJustMember); [FilledInDuringResolution] public List ResolvedOutparameterTypes; diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs index 2b5d5d31bef..7b4f54224e3 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Linq; using System.Numerics; namespace Microsoft.Dafny; @@ -49,7 +50,7 @@ public virtual IEnumerable TerminalExpressions { public Type Type { get { Contract.Ensures(type != null || Contract.Result() == null); // useful in conjunction with postcondition of constructor - return type == null ? null : type.Normalize(); + return type?.Normalize(); } set { Contract.Requires(!WasResolved()); // set it only once @@ -127,6 +128,23 @@ public virtual IEnumerable SubExpressions { get { yield break; } } + public IEnumerable DescendantsAndSelf { + get { + Stack todo = new(); + List result = new(); + todo.Push(this); + while (todo.Any()) { + var current = todo.Pop(); + result.Add(current); + foreach (var child in current.SubExpressions) { + todo.Push(child); + } + } + + return result; + } + } + /// /// Returns the list of types that appear in this expression proper (that is, not including types that /// may appear in subexpressions). Types occurring in substatements of the expression are not included. @@ -136,9 +154,7 @@ public virtual IEnumerable ComponentTypes { get { yield break; } } - public virtual bool IsImplicit { - get { return false; } - } + public virtual bool IsImplicit => false; public static IEnumerable Conjuncts(Expression expr) { Contract.Requires(expr != null); @@ -769,7 +785,7 @@ public static Expression CreateFieldSelect(IToken tok, Expression receiver, Fiel /// Wrap the resolved MemberSelectExpr in the usual unresolved structure, in case the expression is cloned and re-resolved. /// public static Expression WrapResolvedMemberSelect(MemberSelectExpr memberSelectExpr) { - List optTypeArguments = memberSelectExpr.TypeApplication_JustMember.Count == 0 ? null : memberSelectExpr.TypeApplication_JustMember; + List optTypeArguments = memberSelectExpr.TypeApplicationJustMember.Count == 0 ? null : memberSelectExpr.TypeApplicationJustMember; return new ExprDotName(memberSelectExpr.tok, memberSelectExpr.Obj, memberSelectExpr.MemberName, optTypeArguments) { ResolvedExpression = memberSelectExpr, Type = memberSelectExpr.Type @@ -908,4 +924,10 @@ public string AsStringLiteral() { public override IEnumerable Children => SubExpressions; public override IEnumerable PreResolveChildren => Children; + + public static Expression CreateAssigned(IToken tok, IdentifierExpr inner) { + return new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Assigned, inner) { + Type = Type.Bool + }; + } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs b/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs index b81c90e4840..74da619191e 100644 --- a/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs @@ -114,14 +114,14 @@ public enum ResolvedOpcode { } private ResolvedOpcode _theResolvedOp = ResolvedOpcode.YetUndetermined; public ResolvedOpcode ResolvedOp { - set { - Contract.Assume(_theResolvedOp == ResolvedOpcode.YetUndetermined || _theResolvedOp == value); // there's never a reason for resolution to change its mind, is there? - _theResolvedOp = value; - } get { Debug.Assert(_theResolvedOp != ResolvedOpcode.YetUndetermined); // shouldn't read it until it has been properly initialized return _theResolvedOp; } + set { + Contract.Assume(_theResolvedOp == ResolvedOpcode.YetUndetermined || _theResolvedOp == value); // there's never a reason for resolution to change its mind, is there? + _theResolvedOp = value; + } } public ResolvedOpcode ResolvedOp_PossiblyStillUndetermined { // offer a way to return _theResolveOp -- for experts only! get { return _theResolvedOp; } diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs index 6bb7c994880..ab73b05d1a1 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs @@ -9,6 +9,11 @@ public class AssignStmt : Statement, ICloneable { public readonly AssignmentRhs Rhs; public override IEnumerable Children => new List { Lhs, Rhs }.Where(x => x != null); public override IEnumerable PreResolveChildren => Children; + + public override IEnumerable GetAssignedLocals() { + return new[] { Lhs.Resolved }.OfType(); + } + [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Lhs != null); diff --git a/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs b/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs index 159ddb223fa..4288038b6c3 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs @@ -22,6 +22,9 @@ public ConcreteUpdateStatement(RangeToken rangeToken, List lhss, Att public override IEnumerable Children => Lhss; public override IEnumerable PreResolveChildren => Lhss; + public override IEnumerable GetAssignedLocals() { + return Lhss.Select(lhs => lhs.Resolved).OfType(); + } public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { return formatter.SetIndentUpdateStmt(this, indentBefore, false); diff --git a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs index 41348dae006..22b17ce7c8a 100644 --- a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs @@ -19,6 +19,10 @@ void ObjectInvariant() { } public override IEnumerable Children => Lhs.Concat(new Node[] { MethodSelect, Bindings }); + public override IEnumerable GetAssignedLocals() { + return Lhs.Select(lhs => lhs.Resolved).OfType(); + } + public readonly List Lhs; public readonly MemberSelectExpr MethodSelect; private readonly IToken overrideToken; diff --git a/Source/DafnyCore/AST/Statements/OpaqueBlock.cs b/Source/DafnyCore/AST/Statements/OpaqueBlock.cs new file mode 100644 index 00000000000..3611bac7165 --- /dev/null +++ b/Source/DafnyCore/AST/Statements/OpaqueBlock.cs @@ -0,0 +1,53 @@ +using System.Collections.Generic; +using System.Linq; + +namespace Microsoft.Dafny; + +public class OpaqueBlock : BlockStmt, ICanResolveNewAndOld { + public readonly List Ensures; + public readonly Specification Modifies; + + protected OpaqueBlock(Cloner cloner, OpaqueBlock original) : base(cloner, original) { + Ensures = original.Ensures.Select(cloner.CloneAttributedExpr).ToList(); + Modifies = cloner.CloneSpecFrameExpr(original.Modifies); + } + + public override IEnumerable SpecificationSubExpressions { + get { + foreach (var e in Ensures) { + yield return e.E; + } + foreach (var e in Modifies.Expressions) { + yield return e.E; + } + } + } + + public OpaqueBlock(RangeToken rangeToken, List body, + List ensures, + Specification modifies) : base(rangeToken, body) { + Ensures = ensures; + Modifies = modifies; + } + + public override void GenResolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) { + + resolver.Scope.PushMarker(); + foreach (Statement ss in Body) { + resolver.ResolveStatementWithLabels(ss, resolutionContext); + } + resolver.Scope.PopMarker(); + + resolver.ResolveAttributes(Modifies, resolutionContext); + foreach (var fe in Modifies.Expressions) { + resolver.ResolveFrameExpression(fe, FrameExpressionUse.Modifies, resolutionContext); + } + + foreach (var ensure in Ensures) { + resolver.ResolveAttributes(ensure, resolutionContext); + resolver.ResolveExpression(ensure.E, resolutionContext); + resolver.ConstrainTypeExprBool(ensure.E, "Postcondition must be a boolean (got {0})"); + } + base.GenResolve(resolver, resolutionContext); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/Statements/Statement.cs b/Source/DafnyCore/AST/Statements/Statement.cs index a8e2a7302ab..67c8c7fdabd 100644 --- a/Source/DafnyCore/AST/Statements/Statement.cs +++ b/Source/DafnyCore/AST/Statements/Statement.cs @@ -77,6 +77,23 @@ public virtual IEnumerable SubStatements { get { yield break; } } + public IEnumerable DescendantsAndSelf { + get { + Stack todo = new(); + List result = new(); + todo.Push(this); + while (todo.Any()) { + var current = todo.Pop(); + result.Add(current); + foreach (var child in current.SubStatements) { + todo.Push(child); + } + } + + return result; + } + } + /// /// Returns the non-null substatements of the Statements, before resolution occurs /// @@ -175,4 +192,6 @@ public override string ToString() { public override IEnumerable PreResolveChildren => (Attributes != null ? new List { Attributes } : Enumerable.Empty()).Concat( PreResolveSubStatements).Concat(PreResolveSubExpressions); + + public virtual IEnumerable GetAssignedLocals() => Enumerable.Empty(); } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Substituter.cs b/Source/DafnyCore/AST/Substituter.cs index 2cf2d0b05d0..4af3641b4f3 100644 --- a/Source/DafnyCore/AST/Substituter.cs +++ b/Source/DafnyCore/AST/Substituter.cs @@ -118,15 +118,15 @@ public virtual Expression Substitute(Expression expr) { } else if (expr is MemberSelectExpr) { var mse = (MemberSelectExpr)expr; var newObj = Substitute(mse.Obj); - var newTypeApplicationAtEnclosingClass = SubstituteTypeList(mse.TypeApplication_AtEnclosingClass); - var newTypeApplicationJustMember = SubstituteTypeList(mse.TypeApplication_JustMember); + var newTypeApplicationAtEnclosingClass = SubstituteTypeList(mse.TypeApplicationAtEnclosingClass); + var newTypeApplicationJustMember = SubstituteTypeList(mse.TypeApplicationJustMember); if (newObj != mse.Obj || - newTypeApplicationAtEnclosingClass != mse.TypeApplication_AtEnclosingClass || - newTypeApplicationJustMember != mse.TypeApplication_JustMember) { + newTypeApplicationAtEnclosingClass != mse.TypeApplicationAtEnclosingClass || + newTypeApplicationJustMember != mse.TypeApplicationJustMember) { var fseNew = new MemberSelectExpr(mse.tok, newObj, mse.MemberName) { Member = mse.Member, - TypeApplication_AtEnclosingClass = newTypeApplicationAtEnclosingClass, - TypeApplication_JustMember = newTypeApplicationJustMember, + TypeApplicationAtEnclosingClass = newTypeApplicationAtEnclosingClass, + TypeApplicationJustMember = newTypeApplicationJustMember, AtLabel = mse.AtLabel ?? oldHeapLabel }; newExpr = fseNew; diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs index d7d946b7b2d..7b5f3bde91d 100644 --- a/Source/DafnyCore/AST/SystemModuleManager.cs +++ b/Source/DafnyCore/AST/SystemModuleManager.cs @@ -380,8 +380,8 @@ private Expression ArrowSubtypeConstraint(IToken tok, RangeToken rangeToken, Bou } var fn = new MemberSelectExpr(tok, f, member.Name) { Member = member, - TypeApplication_AtEnclosingClass = f.Type.TypeArgs, - TypeApplication_JustMember = new List(), + TypeApplicationAtEnclosingClass = f.Type.TypeArgs, + TypeApplicationJustMember = new List(), Type = GetTypeOfFunction(member, tps.ConvertAll(tp => (Type)new UserDefinedType(tp)), new List()) }; Expression body = new ApplyExpr(tok, fn, args, tok); diff --git a/Source/DafnyCore/Backends/BoogieExtractor.cs b/Source/DafnyCore/Backends/BoogieExtractor.cs index 7d5c7b868e3..dd9a226fdc0 100644 --- a/Source/DafnyCore/Backends/BoogieExtractor.cs +++ b/Source/DafnyCore/Backends/BoogieExtractor.cs @@ -189,25 +189,27 @@ public override void VisitMethod(Method method) { private QKeyValue? GetKeyValues(IToken tok, Attributes attributes) { QKeyValue? kv = null; var extractAttributes = Attributes.FindAllExpressions(attributes, AttributeAttribute); - if (extractAttributes != null) { - if (extractAttributes.Count == 0) { - throw new ExtractorError($"first argument to :{AttributeAttribute} is expected to be a literal string; got no arguments"); - } - for (var i = extractAttributes.Count; 0 <= --i;) { - string? attrName = null; - var parameters = new List(); - foreach (var argument in extractAttributes[i]) { - if (attrName != null) { - parameters.Add(ExtractExpr(argument)); - } else if (argument is StringLiteralExpr { Value: string name }) { - attrName = name; - } else { - throw new ExtractorError($"first argument to :{AttributeAttribute} is expected to be a literal string; got: {argument}"); - } - } + if (extractAttributes == null) { + return kv; + } - kv = new Boogie.QKeyValue(tok, attrName, parameters, kv); + if (extractAttributes.Count == 0) { + throw new ExtractorError($"first argument to :{AttributeAttribute} is expected to be a literal string; got no arguments"); + } + for (var i = extractAttributes.Count; 0 <= --i;) { + string? attrName = null; + var parameters = new List(); + foreach (var argument in extractAttributes[i]) { + if (attrName != null) { + parameters.Add(ExtractExpr(argument)); + } else if (argument is StringLiteralExpr { Value: string name }) { + attrName = name; + } else { + throw new ExtractorError($"first argument to :{AttributeAttribute} is expected to be a literal string; got: {argument}"); + } } + + kv = new QKeyValue(tok, attrName, parameters, kv); } return kv; diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs index c51b107f6d4..9366be441ec 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs @@ -86,7 +86,7 @@ public virtual void EmitExpr(Expression expr, bool inLetExprBody, ConcreteSyntax wr.Write(preStr); if (sf.IsStatic && !SupportsStaticsInGenericClasses && sf.EnclosingClass.TypeArgs.Count != 0) { - var typeArgs = e.TypeApplication_AtEnclosingClass; + var typeArgs = e.TypeApplicationAtEnclosingClass; Contract.Assert(typeArgs.Count == sf.EnclosingClass.TypeArgs.Count); wr.Write("{0}.", TypeName_Companion(e.Obj.Type, wr, e.tok, sf)); EmitNameAndActualTypeArgs(IdName(e.Member), typeArgs, e.tok, null, false, wr); @@ -100,8 +100,8 @@ void writeObj(ConcreteSyntaxTree w) { TrParenExpr(e.Obj, w, inLetExprBody, wStmts); } - var typeArgs = CombineAllTypeArguments(e.Member, e.TypeApplication_AtEnclosingClass, - e.TypeApplication_JustMember); + var typeArgs = CombineAllTypeArguments(e.Member, e.TypeApplicationAtEnclosingClass, + e.TypeApplicationJustMember); EmitMemberSelect(writeObj, e.Obj.Type, e.Member, typeArgs, e.TypeArgumentSubstitutionsWithParents(), selectExpr.Type).EmitRead(wr); } @@ -109,7 +109,7 @@ void writeObj(ConcreteSyntaxTree w) { wr.Write(postStr); } else { var typeArgs = - CombineAllTypeArguments(e.Member, e.TypeApplication_AtEnclosingClass, e.TypeApplication_JustMember); + CombineAllTypeArguments(e.Member, e.TypeApplicationAtEnclosingClass, e.TypeApplicationJustMember); var typeMap = e.TypeArgumentSubstitutionsWithParents(); var customReceiver = NeedsCustomReceiverNotTrait(e.Member); if (!customReceiver && !e.Member.IsStatic) { diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index 98c390f870c..c7993c0365a 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -531,7 +531,7 @@ protected virtual void EmitMultiAssignment(List lhsExprs, List EmitIdentifier(target, w), memberSelectExpr.Obj.Type, memberSelectExpr.Member, typeArgs, memberSelectExpr.TypeArgumentSubstitutionsWithParents(), memberSelectExpr.Type, internalAccess: enclosingMethod is Constructor); lhssn.Add(newLhs); @@ -3295,7 +3295,7 @@ bool IsTailRecursiveByMethodCall(FunctionCallExpr fce) { protected virtual void EmitMemberSelect(AssignStmt s0, List tupleTypeArgsList, ConcreteSyntaxTree wr, string tup) { var lhs = (MemberSelectExpr)s0.Lhs; - var typeArgs = TypeArgumentInstantiation.ListFromMember(lhs.Member, null, lhs.TypeApplication_JustMember); + var typeArgs = TypeArgumentInstantiation.ListFromMember(lhs.Member, null, lhs.TypeApplicationJustMember); var lvalue = EmitMemberSelect(w => { var wObj = EmitCoercionIfNecessary(from: null, to: tupleTypeArgsList[0], s0.Tok, w); EmitTupleSelect(tup, 0, wObj); @@ -3936,7 +3936,7 @@ ILvalue CreateLvalue(Expression lhs, ConcreteSyntaxTree wr, ConcreteSyntaxTree w ll.Obj.Type.IsNonNullRefType || !ll.Obj.Type.IsRefType ? null : UserDefinedType.CreateNonNullType((UserDefinedType)ll.Obj.Type.NormalizeExpand()), "_obj", wr, wStmts ); - var typeArgs = TypeArgumentInstantiation.ListFromMember(ll.Member, null, ll.TypeApplication_JustMember); + var typeArgs = TypeArgumentInstantiation.ListFromMember(ll.Member, null, ll.TypeApplicationJustMember); return EmitMemberSelect(writeStabilized, ll.Obj.Type, ll.Member, typeArgs, ll.TypeArgumentSubstitutionsWithParents(), lhs.Type, internalAccess: enclosingMethod is Constructor); @@ -4474,7 +4474,7 @@ protected virtual void TrCallStmt(CallStmt s, string receiverReplacement, Concre EmitTypeName_Companion(s.Receiver.Type, wr, wr, s.Tok, s.Method); wr.Write(StaticClassAccessor); } - var typeArgs = CombineAllTypeArguments(s.Method, s.MethodSelect.TypeApplication_AtEnclosingClass, s.MethodSelect.TypeApplication_JustMember); + var typeArgs = CombineAllTypeArguments(s.Method, s.MethodSelect.TypeApplicationAtEnclosingClass, s.MethodSelect.TypeApplicationJustMember); var firstReceiverArg = receiverReplacement != null ? new IdentifierExpr(s.Receiver.tok, receiverReplacement) { Type = s.Receiver.Type } : s.Receiver; EmitNameAndActualTypeArgs(protectedName, TypeArgumentInstantiation.ToActuals(ForTypeParameters(typeArgs, s.Method, false)), s.Tok, diff --git a/Source/DafnyCore/CounterExampleGeneration/PartialState.cs b/Source/DafnyCore/CounterExampleGeneration/PartialState.cs index 0704d02578c..29a069ddd4f 100644 --- a/Source/DafnyCore/CounterExampleGeneration/PartialState.cs +++ b/Source/DafnyCore/CounterExampleGeneration/PartialState.cs @@ -165,7 +165,7 @@ private void SetupVars() { } names = names.Concat(State.Variables).Distinct().ToList(); var notDefinitelyAssigned = new HashSet(); - foreach (var name in names.Where(name => name.StartsWith("defass#"))) { + foreach (var name in names.Where(name => name.StartsWith(BoogieGenerator.DefassPrefix))) { var val = State.TryGet(name); if (val == null) { continue; diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 5873add2c99..2ac3fb6598f 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -2142,6 +2142,7 @@ FunctionBody = (. Contract.Ensures(Contract.ValueAtReturn(out block) != null); @@ -2154,6 +2155,27 @@ BlockStmt .) . +OpaqueBlock += (. + List body = new List(); + List ensures = new(); + List modifies = new List(); + Attributes modifiesAttributes = null; + IToken start; + .) + "opaque" (. start = t; .) + { ModifiesClause + | EnsuresClause + } + "{" + { Stmt } + "}" + (. + s = new OpaqueBlock(new RangeToken(start, t), body, ensures, + new Specification(modifies, modifiesAttributes)); + .) + . + /*------------------------------------------------------------------------*/ DividedBlockStmt = (. Contract.Ensures(Contract.ValueAtReturn(out body) != null); @@ -2187,6 +2209,7 @@ OneStmt .) SYNC ( BlockStmt (. s = bs; .) + | OpaqueBlock | IF(IsReveal(scanner.Peek())) RevealStmt | UpdateStmt // includes UpdateFailure | VarDeclStatement diff --git a/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs b/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs index 505b02be47f..2ba91bfa61d 100644 --- a/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs +++ b/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs @@ -102,7 +102,7 @@ protected override bool VisitOneStmt(Statement stmt, ref bool inGhostContext) { return false; } else if (stmt is CallStmt) { var s = (CallStmt)stmt; - CheckTypeInstantiation(s.Tok, s.Method.WhatKind, s.Method.Name, s.Method.TypeArgs, s.MethodSelect.TypeApplication_JustMember, inGhostContext); + CheckTypeInstantiation(s.Tok, s.Method.WhatKind, s.Method.Name, s.Method.TypeArgs, s.MethodSelect.TypeApplicationJustMember, inGhostContext); // recursively visit all subexpressions, noting that some of them may correspond to ghost formal parameters Contract.Assert(s.Lhs.Count == s.Method.Outs.Count); for (var i = 0; i < s.Method.Outs.Count; i++) { @@ -243,7 +243,7 @@ bool VisitPattern(CasePattern pat, bool patternGhostContext) { } else if (expr is MemberSelectExpr) { var e = (MemberSelectExpr)expr; if (e.Member is Function || e.Member is Method) { - CheckTypeInstantiation(e.tok, e.Member.WhatKind, e.Member.Name, ((ICallable)e.Member).TypeArgs, e.TypeApplication_JustMember, inGhostContext); + CheckTypeInstantiation(e.tok, e.Member.WhatKind, e.Member.Name, ((ICallable)e.Member).TypeArgs, e.TypeApplicationJustMember, inGhostContext); } } else if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 68fa345f809..2e1ba07fc05 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -1758,9 +1758,9 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List decl substMap, out var recursiveCallReceiver, out var recursiveCallArgs); var methodSel = new MemberSelectExpr(com.tok, recursiveCallReceiver, prefixLemma.Name); methodSel.Member = prefixLemma; // resolve here - methodSel.TypeApplication_AtEnclosingClass = + methodSel.TypeApplicationAtEnclosingClass = prefixLemma.EnclosingClass.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp.tok, tp)); - methodSel.TypeApplication_JustMember = + methodSel.TypeApplicationJustMember = prefixLemma.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp.tok, tp)); methodSel.Type = new InferredTypeProxy(); var recursiveCall = new CallStmt(com.RangeToken, new List(), methodSel, diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs index ab543dfd24d..910066ad6c8 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs @@ -160,14 +160,14 @@ protected override void PostVisitOneExpression(Expression expr, TypeInferenceChe var e = (MemberSelectExpr)expr; if (e.Member is Function || e.Member is Method) { var i = 0; - foreach (var p in Util.Concat(e.TypeApplication_AtEnclosingClass, e.TypeApplication_JustMember)) { - var tp = i < e.TypeApplication_AtEnclosingClass.Count ? + foreach (var p in Util.Concat(e.TypeApplicationAtEnclosingClass, e.TypeApplicationJustMember)) { + var tp = i < e.TypeApplicationAtEnclosingClass.Count ? (e.Member.EnclosingClass is DefaultClassDecl ? // In a "revealedFunction" attribute, the EnclosingClass is DefaultClassDecl // and does not have type arguments null : e.Member.EnclosingClass.TypeArgs[i]) - : ((ICallable)e.Member).TypeArgs[i - e.TypeApplication_AtEnclosingClass.Count]; + : ((ICallable)e.Member).TypeArgs[i - e.TypeApplicationAtEnclosingClass.Count]; if (tp == null) { continue; } diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 2e7093c9260..d5f65401db7 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -372,8 +372,8 @@ public void ResolveRevealLemmaAttribute(Expression arg) { var rr = new MemberSelectExpr(f.tok, receiver, f.Name); rr.Member = f; - rr.TypeApplication_AtEnclosingClass = typeApplication; - rr.TypeApplication_JustMember = typeApplication_JustForMember; + rr.TypeApplicationAtEnclosingClass = typeApplication; + rr.TypeApplicationJustMember = typeApplication_JustForMember; List args = new List(); for (int i = 0; i < f.Ins.Count; i++) { args.Add(new IntType()); @@ -571,8 +571,8 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont reporter.Error(MessageSource.Resolver, e.tok, "a two-state function can be used only in a two-state context"); } // build the type substitution map - e.TypeApplication_AtEnclosingClass = tentativeReceiverType.TypeArgs; - e.TypeApplication_JustMember = new List(); + e.TypeApplicationAtEnclosingClass = tentativeReceiverType.TypeArgs; + e.TypeApplicationJustMember = new List(); Dictionary subst; var ctype = tentativeReceiverType as UserDefinedType; if (ctype == null) { @@ -583,15 +583,15 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont foreach (var tp in fn.TypeArgs) { Type prox = new InferredTypeProxy(); subst[tp] = prox; - e.TypeApplication_JustMember.Add(prox); + e.TypeApplicationJustMember.Add(prox); } subst = BuildTypeArgumentSubstitute(subst); e.Type = SelectAppropriateArrowTypeForFunction(fn, subst, SystemModuleManager); } else if (member is Field) { var field = (Field)member; e.Member = field; - e.TypeApplication_AtEnclosingClass = tentativeReceiverType.TypeArgs; - e.TypeApplication_JustMember = new List(); + e.TypeApplicationAtEnclosingClass = tentativeReceiverType.TypeArgs; + e.TypeApplicationJustMember = new List(); if (e.Obj is StaticReceiverExpr && !field.IsStatic) { reporter.Error(MessageSource.Resolver, expr, "a field must be selected via an object, not just a class name"); } @@ -5810,8 +5810,8 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, Type receiverType // Now, fill in rr.Type. This requires taking into consideration the type parameters passed to the receiver's type as well as any type // parameters used in this NameSegment/ExprDotName. // Add to "subst" the type parameters given to the member's class/datatype - rr.TypeApplication_AtEnclosingClass = new List(); - rr.TypeApplication_JustMember = new List(); + rr.TypeApplicationAtEnclosingClass = new List(); + rr.TypeApplicationJustMember = new List(); Dictionary subst; var rType = (receiverTypeBound ?? receiver.Type).NormalizeExpand(); if (rType is UserDefinedType udt && udt.ResolvedClass != null) { @@ -5819,14 +5819,14 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, Type receiverType if (member.EnclosingClass == null) { // this can happen for some special members, like real.Floor } else { - rr.TypeApplication_AtEnclosingClass.AddRange(rType.AsParentType(member.EnclosingClass).TypeArgs); + rr.TypeApplicationAtEnclosingClass.AddRange(rType.AsParentType(member.EnclosingClass).TypeArgs); } } else { var vtd = ProgramResolver.SystemModuleManager.AsValuetypeDecl(rType); if (vtd != null) { Contract.Assert(vtd.TypeArgs.Count == rType.TypeArgs.Count); subst = TypeParameter.SubstitutionMap(vtd.TypeArgs, rType.TypeArgs); - rr.TypeApplication_AtEnclosingClass.AddRange(rType.TypeArgs); + rr.TypeApplicationAtEnclosingClass.AddRange(rType.TypeArgs); } else { Contract.Assert(rType.TypeArgs.Count == 0); subst = new Dictionary(); @@ -5852,7 +5852,7 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, Type receiverType } for (int i = 0; i < fn.TypeArgs.Count; i++) { var ta = i < suppliedTypeArguments ? optTypeArguments[i] : new InferredTypeProxy(); - rr.TypeApplication_JustMember.Add(ta); + rr.TypeApplicationJustMember.Add(ta); subst.Add(fn.TypeArgs[i], ta); } subst = BuildTypeArgumentSubstitute(subst, receiverTypeBound ?? receiver.Type); @@ -5871,7 +5871,7 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, Type receiverType } for (int i = 0; i < m.TypeArgs.Count; i++) { var ta = i < suppliedTypeArguments ? optTypeArguments[i] : new InferredTypeProxy(); - rr.TypeApplication_JustMember.Add(ta); + rr.TypeApplicationJustMember.Add(ta); subst.Add(m.TypeArgs[i], ta); } subst = BuildTypeArgumentSubstitute(subst, receiverTypeBound ?? receiver.Type); @@ -5953,8 +5953,8 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext // produce a FunctionCallExpr instead of an ApplyExpr(MemberSelectExpr) var rr = new FunctionCallExpr(e.Lhs.Tok, callee.Name, mse.Obj, e.tok, e.CloseParen, e.Bindings, atLabel) { Function = callee, - TypeApplication_AtEnclosingClass = mse.TypeApplication_AtEnclosingClass, - TypeApplication_JustFunction = mse.TypeApplication_JustMember + TypeApplication_AtEnclosingClass = mse.TypeApplicationAtEnclosingClass, + TypeApplication_JustFunction = mse.TypeApplicationJustMember }; var typeMap = BuildTypeArgumentSubstitute(mse.TypeArgumentSubstitutionsAtMemberDeclaration()); ResolveActualParameters(rr.Bindings, callee.Ins, e.tok, callee, resolutionContext, typeMap, callee.IsStatic ? null : mse.Obj); diff --git a/Source/DafnyCore/Resolver/PreType/INewOrOldResolver.cs b/Source/DafnyCore/Resolver/PreType/INewOrOldResolver.cs index 3e7101822a4..c1c293cc554 100644 --- a/Source/DafnyCore/Resolver/PreType/INewOrOldResolver.cs +++ b/Source/DafnyCore/Resolver/PreType/INewOrOldResolver.cs @@ -27,4 +27,8 @@ public void ScopePushAndReport(Scope scope, IVariable v, string kind) } void ResolveStatementWithLabels(Statement statement, ResolutionContext resolutionContext); + void ResolveFrameExpression( + FrameExpression frameExpression, + FrameExpressionUse frameExpressionUse, + ResolutionContext context); } \ No newline at end of file diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index ef2929eadb7..0c452ce41d3 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -1625,12 +1625,12 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, DPreType receiver // Now, fill in rr.PreType. This requires taking into consideration the type parameters passed to the receiver's type as well as any type // parameters used in this NameSegment/ExprDotName. // Add to "subst" the type parameters given to the member's class/datatype - rr.PreTypeApplication_AtEnclosingClass = new List(); - rr.PreTypeApplication_JustMember = new List(); + rr.PreTypeApplicationAtEnclosingClass = new List(); + rr.PreTypeApplicationJustMember = new List(); var rType = receiverPreTypeBound; var subst = PreType.PreTypeSubstMap(rType.Decl.TypeArgs, rType.Arguments); Contract.Assert(member.EnclosingClass != null); - rr.PreTypeApplication_AtEnclosingClass.AddRange(rType.AsParentType(member.EnclosingClass, this).Arguments); + rr.PreTypeApplicationAtEnclosingClass.AddRange(rType.AsParentType(member.EnclosingClass, this).Arguments); if (member is Field field) { if (optTypeArguments != null) { @@ -1646,7 +1646,7 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, DPreType receiver if (optTypeArguments != null) { if (suppliedTypeArguments == function.TypeArgs.Count) { // preserve the given types in the resolved MemberSelectExpr - rr.TypeApplication_JustMember = optTypeArguments; + rr.TypeApplicationJustMember = optTypeArguments; } else { ReportError(tok, "function '{0}' expects {1} type argument{2} (got {3})", member.Name, function.TypeArgs.Count, Util.Plural(function.TypeArgs.Count), suppliedTypeArguments); @@ -1655,7 +1655,7 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, DPreType receiver for (int i = 0; i < function.TypeArgs.Count; i++) { var ta = i < suppliedTypeArguments ? Type2PreType(optTypeArguments[i]) : CreatePreTypeProxy($"function call to {function.Name}, type argument {i}"); - rr.PreTypeApplication_JustMember.Add(ta); + rr.PreTypeApplicationJustMember.Add(ta); subst.Add(function.TypeArgs[i], ta); } subst = BuildPreTypeArgumentSubstitute(subst, receiverPreTypeBound); @@ -1675,7 +1675,7 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, DPreType receiver if (optTypeArguments != null) { if (suppliedTypeArguments == method.TypeArgs.Count) { // preserve the given types in the resolved MemberSelectExpr - rr.TypeApplication_JustMember = optTypeArguments; + rr.TypeApplicationJustMember = optTypeArguments; } else { ReportError(tok, "method '{0}' expects {1} type argument{2} (got {3})", member.Name, method.TypeArgs.Count, Util.Plural(method.TypeArgs.Count), suppliedTypeArguments); @@ -1684,7 +1684,7 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, DPreType receiver for (int i = 0; i < method.TypeArgs.Count; i++) { var ta = i < suppliedTypeArguments ? Type2PreType(optTypeArguments[i]) : CreatePreTypeProxy($"method call to {method.Name}, type argument {i}"); - rr.PreTypeApplication_JustMember.Add(ta); + rr.PreTypeApplicationJustMember.Add(ta); subst.Add(method.TypeArgs[i], ta); } subst = BuildPreTypeArgumentSubstitute(subst, receiverPreTypeBound); @@ -1753,8 +1753,8 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext // resolve as a FunctionCallExpr instead of as an ApplyExpr(MemberSelectExpr) var rr = new FunctionCallExpr(e.Lhs.tok, callee.Name, mse.Obj, e.tok, e.CloseParen, e.Bindings, atLabel) { Function = callee, - PreTypeApplication_AtEnclosingClass = mse.PreTypeApplication_AtEnclosingClass, - PreTypeApplication_JustFunction = mse.PreTypeApplication_JustMember + PreTypeApplication_AtEnclosingClass = mse.PreTypeApplicationAtEnclosingClass, + PreTypeApplication_JustFunction = mse.PreTypeApplicationJustMember }; var typeMap = mse.PreTypeArgumentSubstitutionsAtMemberDeclaration(); var preTypeMap = BuildPreTypeArgumentSubstitute( diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index caf13af4ff3..8992a33b3d1 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -877,7 +877,7 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r if (callee != null) { // We're looking at a method call if (callee.Outs.Count != 0) { - var typeMap = PreType.PreTypeSubstMap(callee.TypeArgs, methodCallInfo.Callee.PreTypeApplication_JustMember); + var typeMap = PreType.PreTypeSubstMap(callee.TypeArgs, methodCallInfo.Callee.PreTypeApplicationJustMember); firstPreType = callee.Outs[0].PreType.Substitute(typeMap); } else { ReportError(s.Rhs.tok, $"Expected '{callee.Name}' to have a success/failure output value, but the method returns nothing."); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs index 00866bceacf..8f064443a2d 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs @@ -1484,6 +1484,11 @@ void ResolveMethod(Method m) { } } + public void ResolveFrameExpression(FrameExpression frameExpression, FrameExpressionUse frameExpressionUse, + ResolutionContext context) { + ResolveFrameExpression(frameExpression, frameExpressionUse, context.CodeContext); + } + void ResolveFrameExpression(FrameExpression fe, FrameExpressionUse use, ICodeContext codeContext) { Contract.Requires(fe != null); Contract.Requires(codeContext != null); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs b/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs index 00d87118ee3..1d094c78df7 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs @@ -113,9 +113,9 @@ protected override void PostVisitOneExpression(Expression expr, IASTVisitorConte functionCallExpr.TypeApplication_JustFunction = PreType2TypeUtil.Combine(functionCallExpr.TypeApplication_JustFunction, functionCallExpr.PreTypeApplication_JustFunction, true); } else if (expr is MemberSelectExpr memberSelectExpr) { - memberSelectExpr.TypeApplication_AtEnclosingClass = memberSelectExpr.PreTypeApplication_AtEnclosingClass.ConvertAll(PreType2TypeUtil.PreType2FixedType); - memberSelectExpr.TypeApplication_JustMember = - PreType2TypeUtil.Combine(memberSelectExpr.TypeApplication_JustMember, memberSelectExpr.PreTypeApplication_JustMember, true); + memberSelectExpr.TypeApplicationAtEnclosingClass = memberSelectExpr.PreTypeApplicationAtEnclosingClass.ConvertAll(PreType2TypeUtil.PreType2FixedType); + memberSelectExpr.TypeApplicationJustMember = + PreType2TypeUtil.Combine(memberSelectExpr.TypeApplicationJustMember, memberSelectExpr.PreTypeApplicationJustMember, true); } else if (expr is ComprehensionExpr comprehensionExpr) { VisitVariableList(comprehensionExpr.BoundVars, false); } else if (expr is LetExpr letExpr) { diff --git a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs index 27d33b0978b..3d785dd8243 100644 --- a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs +++ b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs @@ -316,11 +316,11 @@ protected override void VisitOneExpr(Expression expr) { var e = (MemberSelectExpr)expr; if (e.Member is Function || e.Member is Method) { var i = 0; - foreach (var p in Util.Concat(e.PreTypeApplication_AtEnclosingClass, e.PreTypeApplication_JustMember)) { + foreach (var p in Util.Concat(e.PreTypeApplicationAtEnclosingClass, e.PreTypeApplicationJustMember)) { var tp = - i < e.PreTypeApplication_AtEnclosingClass.Count + i < e.PreTypeApplicationAtEnclosingClass.Count ? e.Member.EnclosingClass.TypeArgs[i] - : ((ICallable)e.Member).TypeArgs[i - e.PreTypeApplication_AtEnclosingClass.Count]; + : ((ICallable)e.Member).TypeArgs[i - e.PreTypeApplicationAtEnclosingClass.Count]; if (!IsDetermined(p)) { cus.ReportError(e.tok, $"type parameter '{tp.Name}' (inferred to be '{p}') to the {e.Member.WhatKind} '{e.Member.Name}' could not be determined"); } else { diff --git a/Source/DafnyCore/Resolver/TailRecursion.cs b/Source/DafnyCore/Resolver/TailRecursion.cs index d2c7ce0586f..699f1797923 100644 --- a/Source/DafnyCore/Resolver/TailRecursion.cs +++ b/Source/DafnyCore/Resolver/TailRecursion.cs @@ -136,7 +136,7 @@ TailRecursionStatus CheckTailRecursive(Statement stmt, Method enclosingMethod, r var s = (CallStmt)stmt; if (s.Method == enclosingMethod) { DisallowRecursiveCallsInExpressions(s, enclosingMethod, reportErrors); - var status = ConfirmTailCall(s.Tok, s.Method, s.MethodSelect.TypeApplication_JustMember, s.Lhs, reportErrors); + var status = ConfirmTailCall(s.Tok, s.Method, s.MethodSelect.TypeApplicationJustMember, s.Lhs, reportErrors); if (status == TailRecursionStatus.TailCallSpent) { tailCall = s; } diff --git a/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs b/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs index e1b4c96659e..ce32c3a8068 100644 --- a/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs +++ b/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs @@ -329,8 +329,8 @@ public static HideRevealStmt BuildRevealStmt(Function func, IToken tok, ModuleDe var rr = new MemberSelectExpr(func.Tok, receiver, callableName); rr.Type = new InferredTypeProxy(); rr.Member = member; - rr.TypeApplication_JustMember = new List(); - rr.TypeApplication_AtEnclosingClass = args; + rr.TypeApplicationJustMember = new List(); + rr.TypeApplicationAtEnclosingClass = args; var call = new CallStmt(func.RangeToken, new List(), rr, new List(), func.Tok); diff --git a/Source/DafnyCore/Rewriters/ExpectContracts.cs b/Source/DafnyCore/Rewriters/ExpectContracts.cs index d557f62332d..7d66ed412b2 100644 --- a/Source/DafnyCore/Rewriters/ExpectContracts.cs +++ b/Source/DafnyCore/Rewriters/ExpectContracts.cs @@ -170,9 +170,9 @@ private MemberDecl GenerateMethodWrapper(TopLevelDeclWithMembers parent, MemberD var receiver = ModuleResolver.GetReceiver(parent, origMethod, decl.tok); var memberSelectExpr = new MemberSelectExpr(decl.tok, receiver, origMethod.Name); memberSelectExpr.Member = origMethod; - memberSelectExpr.TypeApplication_JustMember = + memberSelectExpr.TypeApplicationJustMember = newMethod.TypeArgs.Select(tp => (Type)new UserDefinedType(tp)).ToList(); - memberSelectExpr.TypeApplication_AtEnclosingClass = + memberSelectExpr.TypeApplicationAtEnclosingClass = parent.TypeArgs.Select(tp => (Type)new UserDefinedType(tp)).ToList(); var callStmt = new CallStmt(decl.RangeToken, outs, memberSelectExpr, args); diff --git a/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs b/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs index 3516f6c4b98..40c9a482885 100644 --- a/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs +++ b/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs @@ -109,8 +109,8 @@ private void VisitAssign(ForallStmt stmt) { Fi = memberSelect.Obj; lhsBuilder = e => new MemberSelectExpr(memberSelect.tok, e, memberSelect.MemberName) { Member = memberSelect.Member, - TypeApplication_AtEnclosingClass = memberSelect.TypeApplication_AtEnclosingClass, - TypeApplication_JustMember = memberSelect.TypeApplication_JustMember, + TypeApplicationAtEnclosingClass = memberSelect.TypeApplicationAtEnclosingClass, + TypeApplicationJustMember = memberSelect.TypeApplicationJustMember, Type = memberSelect.Type }; break; diff --git a/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs b/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs index c16f4b92488..385f703867a 100644 --- a/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs +++ b/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs @@ -60,8 +60,8 @@ protected void AnnotateRevealFunction(Method lemma, Function f) { var nameSegment = new NameSegment(f.tok, f.Name, f.TypeArgs.Count == 0 ? null : typeApplication); var rr = new MemberSelectExpr(f.tok, receiver, f.Name); rr.Member = f; - rr.TypeApplication_AtEnclosingClass = typeApplication; - rr.TypeApplication_JustMember = typeApplication_JustForMember; + rr.TypeApplicationAtEnclosingClass = typeApplication; + rr.TypeApplicationJustMember = typeApplication_JustForMember; List args = new List(); for (int i = 0; i < f.Ins.Count; i++) { args.Add(new IntType()); diff --git a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs b/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs index 549ed8bad9a..d158261d849 100644 --- a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs +++ b/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs @@ -140,8 +140,8 @@ internal override void PostResolve(Program program) { var receiverExpr = new StaticReceiverExpr(tok, (TopLevelDeclWithMembers)method.EnclosingClass, true); var methodSelectExpr = new MemberSelectExpr(tok, receiverExpr, method.Name) { Member = method, - TypeApplication_JustMember = new List(), - TypeApplication_AtEnclosingClass = new List() + TypeApplicationJustMember = new List(), + TypeApplicationAtEnclosingClass = new List() }; if (method.Ins.Count != 0) { diff --git a/Source/DafnyCore/Triggers/TriggerExtensions.cs b/Source/DafnyCore/Triggers/TriggerExtensions.cs index de3eba4153a..e1417a6492a 100644 --- a/Source/DafnyCore/Triggers/TriggerExtensions.cs +++ b/Source/DafnyCore/Triggers/TriggerExtensions.cs @@ -417,8 +417,8 @@ private static bool ShallowEq(MemberSelectExpr expr1, MemberSelectExpr expr2) { Func comparer1 = TypeEq; return expr1.MemberName == expr2.MemberName && expr1.Member == expr2.Member && - expr1.TypeApplication_AtEnclosingClass.SequenceEqual(expr2.TypeApplication_AtEnclosingClass, new PredicateEqualityComparer(comparer)) && - expr1.TypeApplication_JustMember.SequenceEqual(expr2.TypeApplication_JustMember, new PredicateEqualityComparer(comparer1)); + expr1.TypeApplicationAtEnclosingClass.SequenceEqual(expr2.TypeApplicationAtEnclosingClass, new PredicateEqualityComparer(comparer)) && + expr1.TypeApplicationJustMember.SequenceEqual(expr2.TypeApplicationJustMember, new PredicateEqualityComparer(comparer1)); } internal static bool TypeEq(Type type1, Type type2) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs index 622f426aea6..20900f58c02 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs @@ -829,12 +829,12 @@ static Bpl.Axiom BplAxiom(Bpl.Expr e) { return new Bpl.Axiom(e.tok, e); } - static Bpl.Expr BplLocalVar(string name, Bpl.Type ty, List lvars) { + public static Bpl.Expr BplLocalVar(string name, Bpl.Type ty, List lvars) { lvars.Add(BplLocalVar(name, ty, out var v)); return v; } - static Bpl.LocalVariable BplLocalVar(string name, Bpl.Type ty, out Bpl.Expr e) { + public static Bpl.LocalVariable BplLocalVar(string name, Bpl.Type ty, out Bpl.Expr e) { Contract.Requires(ty != null); var v = new Bpl.LocalVariable(ty.tok, new Bpl.TypedIdent(ty.tok, name, ty)); e = new Bpl.IdentifierExpr(ty.tok, name, ty); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs index 3bd716859c5..b595aeec5f7 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs @@ -17,6 +17,7 @@ namespace Microsoft.Dafny { public partial class BoogieGenerator { + public const string DefassPrefix = "defass#"; #region Definite-assignment tracking @@ -48,14 +49,14 @@ bool NeedsDefiniteAssignmentTracker(bool isGhost, Type type, bool isField) { Bpl.Variable tracker; if (isOutParam) { - tracker = new Bpl.Formal(p.Tok, new Bpl.TypedIdent(p.Tok, "defass#" + p.UniqueName, Bpl.Type.Bool), false); + tracker = new Bpl.Formal(p.Tok, new Bpl.TypedIdent(p.Tok, DefassPrefix + p.UniqueName, Bpl.Type.Bool), false); } else { - tracker = new Bpl.LocalVariable(p.Tok, new Bpl.TypedIdent(p.Tok, "defass#" + p.UniqueName, Bpl.Type.Bool)); + tracker = new Bpl.LocalVariable(p.Tok, new Bpl.TypedIdent(p.Tok, DefassPrefix + p.UniqueName, Bpl.Type.Bool)); } localVariables.Add(tracker); var ie = new Bpl.IdentifierExpr(p.Tok, tracker); - definiteAssignmentTrackers.Add(p.UniqueName, ie); + DefiniteAssignmentTrackers.Add(p.UniqueName, ie); return ie; } @@ -63,8 +64,8 @@ void AddExistingDefiniteAssignmentTracker(IVariable p, bool forceGhostVar) { Contract.Requires(p != null); if (NeedsDefiniteAssignmentTracker(p.IsGhost || forceGhostVar, p.Type, false)) { - var ie = new Bpl.IdentifierExpr(p.Tok, "defass#" + p.UniqueName, Bpl.Type.Bool); - definiteAssignmentTrackers.Add(p.UniqueName, ie); + var ie = new Bpl.IdentifierExpr(p.Tok, DefassPrefix + p.UniqueName, Bpl.Type.Bool); + DefiniteAssignmentTrackers.Add(p.UniqueName, ie); } } @@ -79,13 +80,13 @@ void AddDefiniteAssignmentTrackerSurrogate(Field field, TopLevelDeclWithMembers } var nm = SurrogateName(field); - var tracker = new Bpl.LocalVariable(field.tok, new Bpl.TypedIdent(field.tok, "defass#" + nm, Bpl.Type.Bool)); + var tracker = new Bpl.LocalVariable(field.tok, new Bpl.TypedIdent(field.tok, DefassPrefix + nm, Bpl.Type.Bool)); localVariables.Add(tracker); var ie = new Bpl.IdentifierExpr(field.tok, tracker); - definiteAssignmentTrackers.Add(nm, ie); + DefiniteAssignmentTrackers.Add(nm, ie); } - void RemoveDefiniteAssignmentTrackers(List ss, int prevDefAssTrackerCount) { + public void RemoveDefiniteAssignmentTrackers(List ss, int prevDefAssTrackerCount) { Contract.Requires(ss != null); foreach (var s in ss) { if (s is VarDeclStmt vdecl) { @@ -107,17 +108,17 @@ void RemoveDefiniteAssignmentTrackers(List ss, int prevDefAssTrackerC } } - Contract.Assert(prevDefAssTrackerCount == definiteAssignmentTrackers.Count); + Contract.Assert(prevDefAssTrackerCount == DefiniteAssignmentTrackers.Count); } void RemoveDefiniteAssignmentTracker(IVariable p) { Contract.Requires(p != null); - definiteAssignmentTrackers.Remove(p.UniqueName); + DefiniteAssignmentTrackers.Remove(p.UniqueName); } void RemoveDefiniteAssignmentTrackerSurrogate(Field field) { Contract.Requires(field != null); - definiteAssignmentTrackers.Remove(SurrogateName(field)); + DefiniteAssignmentTrackers.Remove(SurrogateName(field)); } void MarkDefiniteAssignmentTracker(IdentifierExpr expr, BoogieStmtListBuilder builder) { @@ -132,7 +133,7 @@ void MarkDefiniteAssignmentTracker(IToken tok, string name, BoogieStmtListBuilde Contract.Requires(builder != null); Bpl.IdentifierExpr ie; - if (definiteAssignmentTrackers.TryGetValue(name, out ie)) { + if (DefiniteAssignmentTrackers.TryGetValue(name, out ie)) { builder.Add(Bpl.Cmd.SimpleAssign(tok, ie, Bpl.Expr.True)); } } @@ -162,7 +163,7 @@ void CheckDefiniteAssignment(IdentifierExpr expr, BoogieStmtListBuilder builder) Contract.Requires(builder != null); Bpl.IdentifierExpr ie; - if (definiteAssignmentTrackers.TryGetValue(expr.Var.UniqueName, out ie)) { + if (DefiniteAssignmentTrackers.TryGetValue(expr.Var.UniqueName, out ie)) { builder.Add(Assert(GetToken(expr), ie, new PODesc.DefiniteAssignment("variable", expr.Var.Name, "here"))); } @@ -173,7 +174,7 @@ void CheckDefiniteAssignment(IdentifierExpr expr, BoogieStmtListBuilder builder) /// Bpl.IdentifierExpr /*?*/ GetDefiniteAssignmentTracker(IVariable var) { Bpl.IdentifierExpr ie; - if (definiteAssignmentTrackers.TryGetValue(var.UniqueName, out ie)) { + if (DefiniteAssignmentTrackers.TryGetValue(var.UniqueName, out ie)) { return ie; } @@ -187,7 +188,7 @@ void CheckDefiniteAssignmentSurrogate(IToken tok, Field field, bool atNew, Boogi var nm = SurrogateName(field); Bpl.IdentifierExpr ie; - if (definiteAssignmentTrackers.TryGetValue(nm, out ie)) { + if (DefiniteAssignmentTrackers.TryGetValue(nm, out ie)) { var desc = new PODesc.DefiniteAssignment( "field", field.Name, atNew ? "at this point in the constructor body" : "here"); builder.Add(Assert(tok, ie, desc)); @@ -230,7 +231,7 @@ void CheckDefiniteAssignmentReturn(IToken tok, Formal p, BoogieStmtListBuilder b Contract.Requires(builder != null); Bpl.IdentifierExpr ie; - if (definiteAssignmentTrackers.TryGetValue(p.UniqueName, out ie)) { + if (DefiniteAssignmentTrackers.TryGetValue(p.UniqueName, out ie)) { var desc = new PODesc.DefiniteAssignment("out-parameter", p.Name, "at this return point"); builder.Add(Assert(tok, ie, desc)); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index 4343488dfa7..663b8ed47f6 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -65,7 +65,7 @@ void ObjectInvariant() { /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in. /// ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, string thisVar, - Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, IFrameScope scope, + Function applyLimitedCurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, IFrameScope scope, string readsFrame, string modifiesFrame, bool stripLits) { Contract.Requires(boogieGenerator != null); @@ -78,7 +78,7 @@ void ObjectInvariant() { this.predef = predef; this._the_heap_expr = heap; this.This = thisVar; - this.applyLimited_CurrentFunction = applyLimited_CurrentFunction; + this.applyLimited_CurrentFunction = applyLimitedCurrentFunction; this.layerInterCluster = layerInterCluster; if (layerIntraCluster == null) { this.layerIntraCluster = layerInterCluster; @@ -649,8 +649,8 @@ public Boogie.Expr TrExpr(Expression expr) { return TrExpr(new FunctionCallExpr(e.tok, fn.Name, mem.Obj, e.tok, e.CloseParen, e.Args) { Function = fn, Type = e.Type, - TypeApplication_AtEnclosingClass = mem.TypeApplication_AtEnclosingClass, - TypeApplication_JustFunction = mem.TypeApplication_JustMember + TypeApplication_AtEnclosingClass = mem.TypeApplicationAtEnclosingClass, + TypeApplication_JustFunction = mem.TypeApplicationJustMember }); } } @@ -833,10 +833,8 @@ public Boogie.Expr TrExpr(Expression expr) { // by $IsAllocBox. return BoogieGenerator.MkIsAllocBox(BoxIfNecessary(e.E.tok, TrExpr(e.E), e.E.Type), e.E.Type, HeapExpr); case UnaryOpExpr.ResolvedOpcode.Assigned: - var ns = e.E as NameSegment; - Contract.Assert(ns != null); string name = null; - switch (ns.Resolved) { + switch (e.E.Resolved) { case IdentifierExpr ie: name = ie.Var.UniqueName; break; @@ -850,7 +848,7 @@ public Boogie.Expr TrExpr(Expression expr) { if (name == null) { return Expr.True; } - BoogieGenerator.definiteAssignmentTrackers.TryGetValue(name, out var defass); + BoogieGenerator.DefiniteAssignmentTrackers.TryGetValue(name, out var defass); return defass; default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 1cc1db20321..1157343bdac 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -18,119 +18,121 @@ using PODesc = Microsoft.Dafny.ProofObligationDescription; namespace Microsoft.Dafny { - public partial class BoogieGenerator { - /// - /// Instances of WFOptions are used as an argument to CheckWellformed, supplying options for the - /// checks to be performed. - /// If "SelfCallsAllowance" is non-null, termination checks will be omitted for calls that look - /// like it. This is useful in function postconditions, where the result of the function is - /// syntactically given as what looks like a recursive call with the same arguments. - /// "DoReadsChecks" indicates whether or not to perform reads checks. If so, the generated code - /// will make references to $_ReadsFrame. If "saveReadsChecks" is true, then the reads checks will - /// be recorded but postponed. In particular, CheckWellformed will append to .Locals a list of - /// fresh local variables and will append to .Assert assertions with appropriate error messages - /// that can be used later. As a convenience, the ProcessSavedReadsChecks will make use of .Locals - /// and .Asserts (and AssignLocals) and update a given StmtListBuilder. - /// "LValueContext" indicates that the expression checked for well-formedness is an L-value of - /// some assignment. - /// - private class WFOptions { - public readonly Function SelfCallsAllowance; - public readonly bool DoReadsChecks; - public readonly bool DoOnlyCoarseGrainedTerminationChecks; // termination checks don't look at decreases clause, but reports errors for any intra-SCC call (this is used in default-value expressions) - public readonly List Locals; - public readonly List> CreateAsserts; - public readonly bool LValueContext; - public readonly Bpl.QKeyValue AssertKv; - - public WFOptions() { - } - public WFOptions(Function selfCallsAllowance, bool doReadsChecks, - bool saveReadsChecks = false, bool doOnlyCoarseGrainedTerminationChecks = false) { - Contract.Requires(!saveReadsChecks || doReadsChecks); // i.e., saveReadsChecks ==> doReadsChecks - SelfCallsAllowance = selfCallsAllowance; - DoReadsChecks = doReadsChecks; - DoOnlyCoarseGrainedTerminationChecks = doOnlyCoarseGrainedTerminationChecks; - if (saveReadsChecks) { - Locals = new List(); - CreateAsserts = new(); - } - } + /// + /// Instances of WFOptions are used as an argument to CheckWellformed, supplying options for the + /// checks to be performed. + /// If "SelfCallsAllowance" is non-null, termination checks will be omitted for calls that look + /// like it. This is useful in function postconditions, where the result of the function is + /// syntactically given as what looks like a recursive call with the same arguments. + /// "DoReadsChecks" indicates whether or not to perform reads checks. If so, the generated code + /// will make references to $_ReadsFrame. If "saveReadsChecks" is true, then the reads checks will + /// be recorded but postponed. In particular, CheckWellformed will append to .Locals a list of + /// fresh local variables and will append to .Assert assertions with appropriate error messages + /// that can be used later. As a convenience, the ProcessSavedReadsChecks will make use of .Locals + /// and .Asserts (and AssignLocals) and update a given StmtListBuilder. + /// "LValueContext" indicates that the expression checked for well-formedness is an L-value of + /// some assignment. + /// + public class WFOptions { + public readonly Function SelfCallsAllowance; + public readonly bool DoReadsChecks; + public readonly bool DoOnlyCoarseGrainedTerminationChecks; // termination checks don't look at decreases clause, but reports errors for any intra-SCC call (this is used in default-value expressions) + public readonly List Locals; + public readonly List> CreateAsserts; + public readonly bool LValueContext; + public readonly Bpl.QKeyValue AssertKv; + + public WFOptions() { + } - private WFOptions(Function selfCallsAllowance, bool doReadsChecks, bool doOnlyCoarseGrainedTerminationChecks, - List locals, List> createAsserts, bool lValueContext, Bpl.QKeyValue assertKv) { - SelfCallsAllowance = selfCallsAllowance; - DoReadsChecks = doReadsChecks; - DoOnlyCoarseGrainedTerminationChecks = doOnlyCoarseGrainedTerminationChecks; - Locals = locals; - CreateAsserts = createAsserts; - LValueContext = lValueContext; - AssertKv = assertKv; + public WFOptions(Function selfCallsAllowance, bool doReadsChecks, + bool saveReadsChecks = false, bool doOnlyCoarseGrainedTerminationChecks = false) { + Contract.Requires(!saveReadsChecks || doReadsChecks); // i.e., saveReadsChecks ==> doReadsChecks + SelfCallsAllowance = selfCallsAllowance; + DoReadsChecks = doReadsChecks; + DoOnlyCoarseGrainedTerminationChecks = doOnlyCoarseGrainedTerminationChecks; + if (saveReadsChecks) { + Locals = new List(); + CreateAsserts = new(); } + } - public WFOptions(Bpl.QKeyValue kv) { - AssertKv = kv; - } + private WFOptions(Function selfCallsAllowance, bool doReadsChecks, bool doOnlyCoarseGrainedTerminationChecks, + List locals, List> createAsserts, bool lValueContext, Bpl.QKeyValue assertKv) { + SelfCallsAllowance = selfCallsAllowance; + DoReadsChecks = doReadsChecks; + DoOnlyCoarseGrainedTerminationChecks = doOnlyCoarseGrainedTerminationChecks; + Locals = locals; + CreateAsserts = createAsserts; + LValueContext = lValueContext; + AssertKv = assertKv; + } - /// - /// Clones the given "options", but turns reads checks on or off. - /// - public WFOptions WithReadsChecks(bool doReadsChecks) { - return new WFOptions(SelfCallsAllowance, doReadsChecks, DoOnlyCoarseGrainedTerminationChecks, - Locals, CreateAsserts, LValueContext, AssertKv); - } + public WFOptions(Bpl.QKeyValue kv) { + AssertKv = kv; + } - /// - /// Clones the given "options", but sets "LValueContext" to "lValueContext". - /// - public WFOptions WithLValueContext(bool lValueContext) { - return new WFOptions(SelfCallsAllowance, DoReadsChecks, DoOnlyCoarseGrainedTerminationChecks, - Locals, CreateAsserts, lValueContext, AssertKv); - } + /// + /// Clones the given "options", but turns reads checks on or off. + /// + public WFOptions WithReadsChecks(bool doReadsChecks) { + return new WFOptions(SelfCallsAllowance, doReadsChecks, DoOnlyCoarseGrainedTerminationChecks, + Locals, CreateAsserts, LValueContext, AssertKv); + } - public Action AssertSink(BoogieGenerator tran, BoogieStmtListBuilder builder) { - return (t, e, d, qk) => { - if (Locals != null) { - var b = BplLocalVar(tran.CurrentIdGenerator.FreshId("b$reqreads#"), Bpl.Type.Bool, Locals); - CreateAsserts.Add(() => tran.Assert(t, b, d, qk)); - builder.Add(Bpl.Cmd.SimpleAssign(e.tok, (Bpl.IdentifierExpr)b, e)); - } else { - builder.Add(tran.Assert(t, e, d, qk)); - } - }; - } + /// + /// Clones the given "options", but sets "LValueContext" to "lValueContext". + /// + public WFOptions WithLValueContext(bool lValueContext) { + return new WFOptions(SelfCallsAllowance, DoReadsChecks, DoOnlyCoarseGrainedTerminationChecks, + Locals, CreateAsserts, lValueContext, AssertKv); + } - public List AssignLocals { - get { - return Map(Locals, l => - Bpl.Cmd.SimpleAssign(l.tok, - new Bpl.IdentifierExpr(Token.NoToken, l), - Bpl.Expr.True) - ); + public Action AssertSink(BoogieGenerator tran, BoogieStmtListBuilder builder) { + return (t, e, d, qk) => { + if (Locals != null) { + var b = BoogieGenerator.BplLocalVar(tran.CurrentIdGenerator.FreshId("b$reqreads#"), Bpl.Type.Bool, Locals); + CreateAsserts.Add(() => tran.Assert(t, b, d, qk)); + builder.Add(Bpl.Cmd.SimpleAssign(e.tok, (Bpl.IdentifierExpr)b, e)); + } else { + builder.Add(tran.Assert(t, e, d, qk)); } + }; + } + + public List AssignLocals { + get { + return Map(Locals, l => + Bpl.Cmd.SimpleAssign(l.tok, + new Bpl.IdentifierExpr(Token.NoToken, l), + Bpl.Expr.True) + ); } + } - public void ProcessSavedReadsChecks(List locals, BoogieStmtListBuilder builderInitializationArea, BoogieStmtListBuilder builder) { - Contract.Requires(locals != null); - Contract.Requires(builderInitializationArea != null); - Contract.Requires(builder != null); - Contract.Requires(Locals != null && CreateAsserts != null); // ProcessSavedReadsChecks should be called only if the constructor was called with saveReadsChecks - - // var b$reads_guards#0 : bool ... - locals.AddRange(Locals); - // b$reads_guards#0 := true ... - foreach (var cmd in AssignLocals) { - builderInitializationArea.Add(cmd); - } - // assert b$reads_guards#0; ... - foreach (var a in CreateAsserts) { - builder.Add(a()); - } + public void ProcessSavedReadsChecks(List locals, BoogieStmtListBuilder builderInitializationArea, BoogieStmtListBuilder builder) { + Contract.Requires(locals != null); + Contract.Requires(builderInitializationArea != null); + Contract.Requires(builder != null); + Contract.Requires(Locals != null && CreateAsserts != null); // ProcessSavedReadsChecks should be called only if the constructor was called with saveReadsChecks + + // var b$reads_guards#0 : bool ... + locals.AddRange(Locals); + // b$reads_guards#0 := true ... + foreach (var cmd in AssignLocals) { + builderInitializationArea.Add(cmd); + } + // assert b$reads_guards#0; ... + foreach (var a in CreateAsserts) { + builder.Add(a()); } } + } + + public partial class BoogieGenerator { - void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, string comment) { + public void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, string comment) { Contract.Requires(expr != null); Contract.Requires(expr.Type != null && expr.Type.IsBoolType); Contract.Requires(wfOptions != null); @@ -246,7 +248,7 @@ public void DoWithDelayedReadsChecks(bool doOnlyCoarseGrainedTerminationChecks, /// /// Check the well-formedness of "expr" (but don't leave hanging around any assumptions that affect control flow) /// - void CheckWellformed(Expression expr, WFOptions wfOptions, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { + public void CheckWellformed(Expression expr, WFOptions wfOptions, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { Contract.Requires(expr != null); Contract.Requires(wfOptions != null); Contract.Requires(locals != null); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index c9c0acc2c7f..d2b73c28414 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -1,6 +1,4 @@ -using System; using System.Collections.Generic; -using System.Collections.Immutable; using System.Diagnostics.Contracts; using System.Linq; using DafnyCore.Verifier; diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index 1eef6d4472e..380f149ef57 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -655,14 +655,10 @@ private StmtList TrMethodContractWellformednessCheck(Method m, ExpressionTransla } if (!(m is TwoStateLemma)) { - // play havoc with the heap according to the modifies clause - builder.Add(new Boogie.HavocCmd(m.tok, new List { etran.HeapCastToIdentifierExpr })); - // assume the usual two-state boilerplate information - foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, m.AllowsAllocation, etran.Old, etran, etran.Old)) { - if (tri.IsFree) { - builder.Add(TrAssumeCmd(m.tok, tri.Expr)); - } - } + var modifies = m.Mod; + var allowsAllocation = m.AllowsAllocation; + + ApplyModifiesEffect(m, etran, builder, modifies, allowsAllocation, m.IsGhost); } // also play havoc with the out parameters @@ -691,6 +687,18 @@ private StmtList TrMethodContractWellformednessCheck(Method m, ExpressionTransla return stmts; } + public void ApplyModifiesEffect(INode node, ExpressionTranslator etran, BoogieStmtListBuilder builder, + Specification modifies, bool allowsAllocation, bool isGhostContext) { + // play havoc with the heap according to the modifies clause + builder.Add(new Boogie.HavocCmd(node.Tok, new List { etran.HeapCastToIdentifierExpr })); + // assume the usual two-state boilerplate information + foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(node.Tok, modifies.Expressions, isGhostContext, allowsAllocation, etran.Old, etran, etran.Old)) { + if (tri.IsFree) { + builder.Add(TrAssumeCmd(node.Tok, tri.Expr)); + } + } + } + private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, List localVariables, ExpressionTranslator etran) { var inductionVars = ApplyInduction(m.Ins, m.Attributes); @@ -743,8 +751,8 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, List (Type)new UserDefinedType(tp.tok, tp)), - TypeApplication_JustMember = m.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp.tok, tp)), + TypeApplicationAtEnclosingClass = m.EnclosingClass.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp.tok, tp)), + TypeApplicationJustMember = m.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp.tok, tp)), Type = new InferredTypeProxy() }; var recursiveCall = new CallStmt(m.tok.ToRange(), new List(), methodSel, recursiveCallArgs) { @@ -793,7 +801,7 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, List AddExistingDefiniteAssignmentTracker(p, m.IsGhost)); // translate the body TrStmt(m.Body, builder, localVariables, etran); @@ -805,7 +813,7 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, List locals, stmtContext = StmtType.NONE; // done with translating expect stmt. } - private void TrAssertStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, List locals, + public void TrAssertStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { var stmtBuilder = new BoogieStmtListBuilder(this, options, builder.Context); var defineFuel = DefineFuelConstant(stmt.Tok, stmt.Attributes, stmtBuilder, etran); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 147e8aeb646..c166e512b95 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -12,6 +12,8 @@ namespace Microsoft.Dafny { public partial class BoogieGenerator { + public const string FrameVariablePrefix = "$Frame$"; + private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { @@ -249,7 +251,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, } else if (stmt is DividedBlockStmt) { var s = (DividedBlockStmt)stmt; AddComment(builder, stmt, "divided block before new;"); - var prevDefiniteAssignmentTrackerCount = definiteAssignmentTrackers.Count; + var prevDefiniteAssignmentTrackerCount = DefiniteAssignmentTrackers.Count; var tok = s.SeparatorTok ?? s.Tok; // a DividedBlockStmt occurs only inside a Constructor body of a class var cl = (ClassDecl)((Constructor)codeContext).EnclosingClass; @@ -286,8 +288,10 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, TrStmtList(s.BodyProper, builder, locals, etran); RemoveDefiniteAssignmentTrackers(s.Body, prevDefiniteAssignmentTrackerCount); + } else if (stmt is OpaqueBlock opaqueBlock) { + OpaqueBlockVerifier.EmitBoogie(this, opaqueBlock, builder, locals, etran, (IMethodCodeContext)codeContext); } else if (stmt is BlockStmt blockStmt) { - var prevDefiniteAssignmentTrackerCount = definiteAssignmentTrackers.Count; + var prevDefiniteAssignmentTrackerCount = DefiniteAssignmentTrackers.Count; TrStmtList(blockStmt.Body, builder, locals, etran, blockStmt.RangeToken); RemoveDefiniteAssignmentTrackers(blockStmt.Body, prevDefiniteAssignmentTrackerCount); } else if (stmt is IfStmt ifStmt) { @@ -334,7 +338,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, 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; + string modifyFrameName = FrameVariablePrefix + suffix; var preModifyHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$PreModifyHeap$" + suffix, predef.HeapType)); locals.Add(preModifyHeapVar); DefineFrame(s.Tok, etran.ModifiesFrame(s.Tok), s.Mod.Expressions, builder, locals, modifyFrameName); @@ -748,7 +752,7 @@ private void TrMatchStmt(MatchStmt stmt, BoogieStmtListBuilder builder, List>(); - foreach (var dat in definiteAssignmentTrackers.Values) { // TODO: the order is non-deterministic and may change between invocations of Dafny + foreach (var dat in DefiniteAssignmentTrackers.Values) { // TODO: the order is non-deterministic and may change between invocations of Dafny var preLoopDat = new Bpl.LocalVariable(dat.tok, new Bpl.TypedIdent(dat.tok, "preLoop$" + suffix + "$" + dat.Name, dat.Type)); locals.Add(preLoopDat); var ie = new Bpl.IdentifierExpr(s.Tok, preLoopDat); @@ -1660,7 +1664,7 @@ void TrAlternatives(List alternatives, IToken elseToken, Act } else { b.Add(TrAssumeCmdWithDependencies(etran, alternative.Guard.tok, alternative.Guard, "alternative guard")); } - var prevDefiniteAssignmentTrackerCount = definiteAssignmentTrackers.Count; + var prevDefiniteAssignmentTrackerCount = DefiniteAssignmentTrackers.Count; TrStmtList(alternative.Body, b, locals, etran, alternative.RangeToken); RemoveDefiniteAssignmentTrackers(alternative.Body, prevDefiniteAssignmentTrackerCount); Bpl.StmtList thn = b.Collect(alternative.Tok); @@ -1949,13 +1953,15 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E CheckFrameSubset(tok, callee.Reads.Expressions.ConvertAll(readsSubst.SubstFrameExpr), receiver, substMap, etran, etran.ReadsFrame(tok), builder, desc, null); } + + // substitute actual args for parameters in description expression frames... + var frameExpressions = callee.Mod.Expressions.ConvertAll(directSub.SubstFrameExpr); // 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 methodCodeContext) { - // substitute actual args for parameters in description expression frames... var desc = new PODesc.ModifyFrameSubset( "call", - callee.Mod.Expressions.ConvertAll(directSub.SubstFrameExpr), + frameExpressions, methodCodeContext.Modifies.Expressions ); // ... but that substitution isn't needed for frames passed to CheckFrameSubset @@ -2837,7 +2843,7 @@ private void IntroduceAndAssignExistentialVars(ExistsExpr exists, BoogieStmtList builder.Add(TrAssumeCmd(exists.tok, etran.TrExpr(exists.Term))); } - void TrStmtList(List stmts, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, + public void TrStmtList(List stmts, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, RangeToken scopeRange = null, bool processLabels = true) { Contract.Requires(stmts != null); Contract.Requires(builder != null); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index ccc218892c0..0652b8baeb0 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -1757,7 +1757,9 @@ Bpl.Expr InSeqRange(IToken tok, Bpl.Expr index, Type indexType, Bpl.Expr seq, bo ICallable codeContext = null; // the method/iterator whose implementation is currently being translated or the function whose specification is being checked for well-formedness Bpl.LocalVariable yieldCountVariable = null; // non-null when an iterator body is being translated bool inBodyInitContext = false; // true during the translation of the .BodyInit portion of a divided constructor body - readonly Dictionary definiteAssignmentTrackers = new Dictionary(); + + public Dictionary DefiniteAssignmentTrackers { get; } = new(); + bool assertAsAssume = false; // generate assume statements instead of assert statements Func assertionOnlyFilter = null; // generate assume statements instead of assert statements if not targeted by {:only} public enum StmtType { NONE, ASSERT, ASSUME }; @@ -2048,7 +2050,7 @@ void GenerateImplPrelude(Method m, bool wellformednessProc, List inPar } } - void DefineFrame(IToken/*!*/ tok, Boogie.IdentifierExpr frameIdentifier, List/*!*/ frameClause, + public void DefineFrame(IToken/*!*/ tok, Boogie.IdentifierExpr frameIdentifier, List/*!*/ frameClause, BoogieStmtListBuilder/*!*/ builder, List/*!*/ localVariables, string name, ExpressionTranslator/*?*/ etran = null) { Contract.Requires(tok != null); Contract.Requires(frameIdentifier != null); @@ -2082,7 +2084,7 @@ void DefineFrame(IToken/*!*/ tok, Boogie.IdentifierExpr frameIdentifier, List calleeFrame, + public void CheckFrameSubset(IToken tok, List calleeFrame, Expression receiverReplacement, Dictionary substMap, ExpressionTranslator /*!*/ etran, Boogie.IdentifierExpr /*!*/ enclosingFrame, BoogieStmtListBuilder /*!*/ builder, @@ -2095,14 +2097,14 @@ void CheckFrameSubset(IToken tok, List calleeFrame, void CheckFrameSubset(IToken tok, List calleeFrame, Expression receiverReplacement, Dictionary substMap, ExpressionTranslator/*!*/ etran, Boogie.IdentifierExpr /*!*/ enclosingFrame, - Action MakeAssert, + Action makeAssert, PODesc.ProofObligationDescription desc, Bpl.QKeyValue kv) { Contract.Requires(tok != null); Contract.Requires(calleeFrame != null); Contract.Requires(receiverReplacement == null || substMap != null); Contract.Requires(etran != null); - Contract.Requires(MakeAssert != null); + Contract.Requires(makeAssert != null); Contract.Requires(predef != null); // emit: assert (forall o: ref, f: Field :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> enclosingFrame[o,f]); @@ -2119,7 +2121,7 @@ void CheckFrameSubset(IToken tok, List calleeFrame, if (IsExprAlways(q, true)) { return; } - MakeAssert(tok, q, desc, kv); + makeAssert(tok, q, desc, kv); } void CheckFrameEmpty(IToken tok, @@ -2775,14 +2777,23 @@ Bpl.Constant GetFieldNameFamily(string n) { /// This method is expected to be called just once for each function in the program. /// Bpl.Function GetOrCreateFunction(Function f) { - if (this.declarationMapping.TryGetValue(f, out var result)) { + if (declarationMapping.TryGetValue(f, out var result)) { return result; } Contract.Requires(f != null); Contract.Requires(predef != null && sink != null); - // declare the function + var func = GetFunctionBoogieDefinition(f); + sink.AddTopLevelDeclaration(func); + + sink.AddTopLevelDeclaration(GetCanCallFunction(f)); + + declarationMapping[f] = func; + return func; + } + + private Bpl.Function GetFunctionBoogieDefinition(Function f) { Bpl.Function func; { var formals = new List(); @@ -2811,10 +2822,12 @@ Bpl.Function GetOrCreateFunction(Function f) { if (InsertChecksums) { InsertChecksum(f, func); } - sink.AddTopLevelDeclaration(func); } + return func; + } - // declare the corresponding canCall function + private Bpl.Function GetCanCallFunction(Function f) { + Bpl.Function canCallF; { var formals = new List(); formals.AddRange(MkTyParamFormals(GetTypeParams(f), false)); @@ -2831,12 +2844,9 @@ Bpl.Function GetOrCreateFunction(Function f) { formals.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(f.IdGenerator), TrType(p.Type)), true)); } var res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false); - var canCallF = new Bpl.Function(f.tok, f.FullSanitizedName + "#canCall", new List(), formals, res); - sink.AddTopLevelDeclaration(canCallF); + canCallF = new Bpl.Function(f.tok, f.FullSanitizedName + "#canCall", new List(), formals, res); } - - declarationMapping[f] = func; - return func; + return canCallF; } /// @@ -2970,7 +2980,7 @@ private void GenerateMethodParametersChoose(IToken tok, IMethodCodeContext m, Me } } if (includeOutParams) { - Contract.Assume(definiteAssignmentTrackers.Count == 0); + Contract.Assume(DefiniteAssignmentTrackers.Count == 0); foreach (Formal p in m.Outs) { Contract.Assert(VisibleInScope(p.Type)); Contract.Assert(!p.IsOld); // out-parameters are never old (perhaps we want to relax this condition in the future) @@ -2988,7 +2998,7 @@ private void GenerateMethodParametersChoose(IToken tok, IMethodCodeContext m, Me } // tear down definite-assignment trackers m.Outs.ForEach(RemoveDefiniteAssignmentTracker); - Contract.Assert(definiteAssignmentTrackers.Count == 0); + Contract.Assert(DefiniteAssignmentTrackers.Count == 0); if (kind == MethodTranslationKind.Implementation) { outParams.Add(new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "$_reverifyPost", Bpl.Type.Bool), false)); @@ -3404,7 +3414,7 @@ public override IToken WithVal(string newVal) { } } - Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription description, Bpl.QKeyValue kv = null) { + public Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription description, Bpl.QKeyValue kv = null) { var cmd = Assert(tok, condition, description, tok, kv); return cmd; } @@ -3516,7 +3526,7 @@ Bpl.StmtList TrStmt2StmtList(BoogieStmtListBuilder builder, /// if (*) { S ; assume false; } /// where "S" is the given "builderToCollect". This method consumes what has been built up in "builderToCollect". /// - void PathAsideBlock(IToken tok, BoogieStmtListBuilder builderToCollect, BoogieStmtListBuilder builder) { + public void PathAsideBlock(IToken tok, BoogieStmtListBuilder builderToCollect, BoogieStmtListBuilder builder) { Contract.Requires(tok != null); Contract.Requires(builderToCollect != null); Contract.Requires(builderToCollect != null); diff --git a/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs b/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs index dc8aeb1a07d..8053210c2e3 100644 --- a/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs +++ b/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs @@ -1,3 +1,4 @@ +using System.Collections.Generic; using System.Linq; using Microsoft.Boogie; @@ -6,16 +7,18 @@ public class BoogieStmtListBuilder { public DafnyOptions Options { get; } public BodyTranslationContext Context { get; set; } public StmtListBuilder builder; + public readonly List Commands; public BoogieGenerator tran; public BoogieStmtListBuilder WithContext(BodyTranslationContext context) { if (context == Context) { return this; } - return new BoogieStmtListBuilder(builder, tran, Options, context); + return new BoogieStmtListBuilder(Commands, builder, tran, Options, context); } - private BoogieStmtListBuilder(StmtListBuilder builder, BoogieGenerator tran, DafnyOptions options, BodyTranslationContext context) { + private BoogieStmtListBuilder(List commands, StmtListBuilder builder, BoogieGenerator tran, DafnyOptions options, BodyTranslationContext context) { + Commands = commands; this.builder = builder; this.tran = tran; Options = options; @@ -23,13 +26,15 @@ private BoogieStmtListBuilder(StmtListBuilder builder, BoogieGenerator tran, Daf } public BoogieStmtListBuilder(BoogieGenerator tran, DafnyOptions options, BodyTranslationContext context) { - builder = new Boogie.StmtListBuilder(); + builder = new StmtListBuilder(); this.tran = tran; - this.Options = options; + Options = options; + Commands = new(); Context = context; } public void Add(Cmd cmd) { + Commands.Add(cmd); builder.Add(cmd); if (cmd is Boogie.AssertCmd) { tran.assertionCount++; @@ -47,14 +52,22 @@ public void Add(Cmd cmd) { } public void Add(StructuredCmd scmd) { + Commands.Add(scmd); builder.Add(scmd); if (scmd is Boogie.WhileCmd whyle && whyle.Invariants.Any(inv => inv is Boogie.AssertCmd)) { tran.assertionCount++; } } - public void Add(TransferCmd tcmd) { builder.Add(tcmd); } - public void AddLabelCmd(string label) { builder.AddLabelCmd(label); } + public void Add(TransferCmd tcmd) { + Commands.Add(tcmd); + builder.Add(tcmd); + } + + public void AddLabelCmd(string label) { + Commands.Add(label); + builder.AddLabelCmd(label); + } public void AddLocalVariable(string name) { builder.AddLocalVariable(name); } public StmtList Collect(Boogie.IToken tok) { diff --git a/Source/DafnyCore/Verifier/OpaqueBlockVerifier.cs b/Source/DafnyCore/Verifier/OpaqueBlockVerifier.cs new file mode 100644 index 00000000000..bc890a890aa --- /dev/null +++ b/Source/DafnyCore/Verifier/OpaqueBlockVerifier.cs @@ -0,0 +1,114 @@ +using System.Collections.Generic; +using System.Linq; +using Microsoft.Boogie; +using Microsoft.Dafny; +using Microsoft.Dafny.ProofObligationDescription; +using Formal = Microsoft.Dafny.Formal; +using DafnyIdentifierExpr = Microsoft.Dafny.IdentifierExpr; +using BoogieIdentifierExpr = Microsoft.Boogie.IdentifierExpr; +using ProofObligationDescription = Microsoft.Dafny.ProofObligationDescription.ProofObligationDescription; +using Token = Microsoft.Dafny.Token; + +namespace DafnyCore.Verifier; + +public static class OpaqueBlockVerifier { + public static void EmitBoogie(BoogieGenerator generator, OpaqueBlock block, BoogieStmtListBuilder builder, + List locals, BoogieGenerator.ExpressionTranslator etran, IMethodCodeContext codeContext) { + + var hasModifiesClause = block.Modifies.Expressions.Any(); + var blockBuilder = new BoogieStmtListBuilder(generator, builder.Options, builder.Context); + + var bodyTranslator = GetBodyTranslator(generator, block, locals, etran, hasModifiesClause, blockBuilder); + var prevDefiniteAssignmentTrackerCount = generator.DefiniteAssignmentTrackers.Count; + generator.TrStmtList(block.Body, blockBuilder, locals, bodyTranslator, block.RangeToken); + generator.RemoveDefiniteAssignmentTrackers(block.Body, prevDefiniteAssignmentTrackerCount); + + var assignedVariables = block.DescendantsAndSelf. + SelectMany(s => s.GetAssignedLocals()).Select(ie => ie.Var) + .ToHashSet(); + List totalEnsures = new(); + + var variablesUsedInEnsures = block.Ensures.SelectMany(ae => ae.E.DescendantsAndSelf). + OfType().DistinctBy(ie => ie.Var); + var implicitAssignedIdentifiers = variablesUsedInEnsures.Where( + v => assignedVariables.Contains(v.Var) && generator.DefiniteAssignmentTrackers.ContainsKey(v.Var.UniqueName)); + foreach (var v in implicitAssignedIdentifiers) { + var expression = new AttributedExpression(Expression.CreateAssigned(v.Tok, v)); + totalEnsures.Add(expression); + blockBuilder.Add(generator.Assert( + v.Tok, etran.TrExpr(expression.E), + new DefiniteAssignment("variable", v.Var.Name, "here"))); + } + + foreach (var ensure in block.Ensures) { + totalEnsures.Add(ensure); + blockBuilder.Add(generator.Assert( + ensure.Tok, etran.TrExpr(ensure.E), + new OpaqueEnsuresDescription(), + etran.TrAttributes(ensure.Attributes, null))); + } + + if (hasModifiesClause) { + var context = new OpaqueBlockContext(codeContext, block); + if (context is IMethodCodeContext methodCodeContext) { + generator.CheckFrameSubset( + block.Tok, block.Modifies.Expressions, + null, null, etran, etran.ModifiesFrame(block.Tok), blockBuilder, new ModifyFrameSubset( + "opaque block", + block.Modifies.Expressions, + methodCodeContext.Modifies.Expressions + ), null); + } + } + + generator.PathAsideBlock(block.Tok, blockBuilder, builder); + builder.Add(new HavocCmd(Token.NoToken, assignedVariables.Select(v => new BoogieIdentifierExpr(v.Tok, v.UniqueName)).ToList())); + + if (hasModifiesClause) { + generator.ApplyModifiesEffect(block, etran, builder, block.Modifies, true, block.IsGhost); + } + + foreach (var ensure in totalEnsures) { + generator.CheckWellformedAndAssume(ensure.E, new WFOptions(null, false), + locals, builder, etran, null); + } + } + + private static BoogieGenerator.ExpressionTranslator GetBodyTranslator(BoogieGenerator generator, OpaqueBlock block, List locals, + BoogieGenerator.ExpressionTranslator etran, bool hasModifiesClause, BoogieStmtListBuilder blockBuilder) { + BoogieGenerator.ExpressionTranslator bodyTranslator; + if (hasModifiesClause) { + string modifyFrameName = BoogieGenerator.FrameVariablePrefix + generator.CurrentIdGenerator.FreshId("opaque#"); + generator.DefineFrame(block.Tok, etran.ModifiesFrame(block.Tok), block.Modifies.Expressions, blockBuilder, locals, modifyFrameName); + bodyTranslator = etran.WithModifiesFrame(modifyFrameName); + } else { + bodyTranslator = etran; + } + + return bodyTranslator; + } + + class OpaqueEnsuresDescription : ProofObligationDescription { + public override string SuccessDescription => "ensures always holds"; + + public override string FailureDescription => "ensures might not hold"; + + public override string ShortDescription => "opaque block ensure clause"; + public override bool IsImplicit => false; + } + + class OpaqueBlockContext : CallableWrapper, IMethodCodeContext { + private readonly IMethodCodeContext callable; + private readonly OpaqueBlock opaqueBlock; + + public OpaqueBlockContext(IMethodCodeContext callable, OpaqueBlock opaqueBlock) + : base(callable, callable.IsGhost) { + this.callable = callable; + this.opaqueBlock = opaqueBlock; + } + + public List Outs => callable.Outs; + + public Specification Modifies => opaqueBlock.Modifies; + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs index 4591969b753..a83a9be9c58 100644 --- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs +++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs @@ -12,6 +12,7 @@ namespace Microsoft.Dafny.ProofObligationDescription; public abstract class ProofObligationDescription : Boogie.ProofObligationDescription { public virtual bool IsImplicit => true; + // An expression that, if verified, would trigger a success for this ProofObligationDescription // It is only printed for the user, so it does not need to be resolved. public virtual Expression GetAssertedExpr(DafnyOptions options) { diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index 5bd4344ac6d..d11ea371ff7 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/Source/DafnyDriver/Commands/VerifyCommand.cs @@ -93,14 +93,13 @@ public static async Task HandleVerification(DafnyOptions options) { await proofDependenciesReported; if (!resolution.HasErrors && options.BoogieExtractionTargetFile != null) { - using (var engine = ExecutionEngine.CreateWithoutSharedCache(options)) { - try { - var extractedProgram = BoogieExtractor.Extract(resolution.ResolvedProgram); - engine.PrintBplFile(options.BoogieExtractionTargetFile, extractedProgram, true, pretty: true); - } catch (ExtractorError extractorError) { - await options.OutputWriter.WriteLineAsync($"Boogie axiom extraction error: {extractorError.Message}"); - return 1; - } + using var engine = ExecutionEngine.CreateWithoutSharedCache(options); + try { + var extractedProgram = BoogieExtractor.Extract(resolution.ResolvedProgram); + engine.PrintBplFile(options.BoogieExtractionTargetFile, extractedProgram, true, pretty: true); + } catch (ExtractorError extractorError) { + await options.OutputWriter.WriteLineAsync($"Boogie axiom extraction error: {extractorError.Message}"); + return 1; } } } diff --git a/Source/DafnyTestGeneration/Inlining/FunctionCallToMethodCallRewriter.cs b/Source/DafnyTestGeneration/Inlining/FunctionCallToMethodCallRewriter.cs index fe5c3484bb0..2fdfe1c8c68 100644 --- a/Source/DafnyTestGeneration/Inlining/FunctionCallToMethodCallRewriter.cs +++ b/Source/DafnyTestGeneration/Inlining/FunctionCallToMethodCallRewriter.cs @@ -70,7 +70,7 @@ public override Statement CloneStmt(Statement stmt, bool isReference) { CloneExpr(funcCallExpr.Receiver.Resolved), funcCallExpr.Function.ByMethodDecl.Name); memberSelectExpr.Member = funcCallExpr.Function.ByMethodDecl; - memberSelectExpr.TypeApplication_JustMember = funcCallExpr.TypeApplication_JustFunction; + memberSelectExpr.TypeApplicationJustMember = funcCallExpr.TypeApplication_JustFunction; newResolvedStmts.Add(new CallStmt(stmt.RangeToken, updateStmt.Lhss.Select(lhs => CloneExpr(lhs.Resolved)).ToList(), memberSelectExpr, funcCallExpr.Args.ConvertAll(e => CloneExpr(e.Resolved)))); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy new file mode 100644 index 00000000000..1347dc780c6 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy @@ -0,0 +1,183 @@ +// RUN: ! %verify --standard-libraries=true %s &> "%t" +// RUN: %diff "%s.expect" "%t" + +method Foo() returns (x: int) + ensures x > 4 +{ + x := 1; + var y := 1; + opaque + ensures x > 3 + { + x := x + y; + x := x + 2; + } + assert x == 4; // error + x := x + 1; +} + +method StructuredCommandsIf(t: bool) +{ + var x := 1; + opaque + { + if (t) { + x := x + 2; + } + } + assert x >= 1; // error +} + +method StructuredCommandsWhile() +{ + var x := 1; + opaque + { + while (x > 0) + decreases x + { + x := x - 1; + } + } + assert x >= 1; // error +} + +method BadlyFormedSpec() +{ + var x := 1; + opaque + ensures 3 / x == 1 // error: possible division by zero + { + x := 3; + } + var y; + opaque ensures y == y { } // error: y is not assigned + y := 1; +} + +class Wrapper { + var x: int +} + +method ContainingMethodModifies(wrapper: Wrapper, unchangedWrapper: Wrapper) returns (x: int) + modifies wrapper + ensures x > 4 +{ + wrapper.x := 2; + opaque + ensures wrapper.x > 3 + { + wrapper.x := wrapper.x + 2; + unchangedWrapper.x := 10; // error + } + x := wrapper.x + 1; +} + +method ExplicitModifies(wrapper: Wrapper) returns (x: int) + modifies wrapper + ensures x > 4 +{ + wrapper.x := 2; + opaque + ensures wrapper.x > 3 + modifies {} + { + wrapper.x := wrapper.x + 2; // error + } + x := wrapper.x + 1; +} + +method ModifiesTooMuch(wrapper: Wrapper, unchangedWrapper: Wrapper) + modifies wrapper +{ + opaque + modifies wrapper, unchangedWrapper // error + { + unchangedWrapper.x := 10; + } +} + +method Nested(w1: Wrapper, w2: Wrapper) + modifies w1, w2 +{ + opaque + modifies w1 + { + opaque modifies w2 // error + { + w2.x := 10; + } + } +} + +method DefiniteAssignment() +{ + var x: int; + opaque + ensures x == 3 + { + x := 3; + } + var target := x; + var y: int; + opaque + { + y := 4; + } + target := y; // error: !assigned(y) + var z: int; + opaque + ensures z == z // error !assigned(z) + { + if (*) { + z := 5; + } + } + target := z; +} + +method EnsuresDoesNotHold() { + var x: int; + opaque + ensures false + { + x := 3; + } +} + +import opened Std.Wrappers +method Returns(input: Option) returns (r: Option) + requires input.Some? ==> input == Some(3) +{ + var x: int; + opaque + ensures x == 3 + { + x :- input; + } + var y: int; + opaque + { + y := 4; + return Some(y); + } + var z: int; + opaque + ensures z > 5 + { + z :| z > 10; + } + r := Some(z); +} + +method MultipleAssignment() returns (r: int) { + var tuple := (3,2); + var x: int; + var y: int; + opaque + ensures x == 3 + { + x, y := tuple.0, tuple.1; + } + r := x; +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect new file mode 100644 index 00000000000..a063323faee --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect @@ -0,0 +1,14 @@ +opaqueBlock.dfy(15,11): Error: assertion might not hold +opaqueBlock.dfy(28,11): Error: assertion might not hold +opaqueBlock.dfy(42,11): Error: assertion might not hold +opaqueBlock.dfy(49,14): Error: possible division by zero +opaqueBlock.dfy(54,17): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here +opaqueBlock.dfy(71,21): Error: assignment might update an object not in the enclosing context's modifies clause +opaqueBlock.dfy(85,12): Error: assignment might update an object not in the enclosing context's modifies clause +opaqueBlock.dfy(93,2): Error: opaque block might violate context's modifies clause +opaqueBlock.dfy(106,4): Error: opaque block might violate context's modifies clause +opaqueBlock.dfy(127,12): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here +opaqueBlock.dfy(130,17): Error: variable 'z', which is subject to definite-assignment rules, might be uninitialized here +opaqueBlock.dfy(142,12): Error: ensures might not hold + +Dafny program verifier finished with 2 verified, 12 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3461.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3461.dfy.expect index 72379bc71f5..a0eb81388b9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3461.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3461.dfy.expect @@ -3,7 +3,6 @@ git-issue-3461.dfy(11,0): Error: a class cannot be declared 'opaque' git-issue-3461.dfy(12,0): Error: a datatype or codatatype cannot be declared 'opaque' git-issue-3461.dfy(13,0): Error: a newtype cannot be declared 'opaque' git-issue-3461.dfy(14,0): Error: a subset type cannot be declared 'opaque' -git-issue-3461.dfy(17,2): Warning: opaque is deprecated as an identifier. It will soon become a reserved word. Use a different name. -git-issue-3461.dfy(17,2): Error: missing semicolon at end of statement +git-issue-3461.dfy(17,9): Error: lbrace expected git-issue-3461.dfy(18,0): Error: this symbol not expected in VarDeclStatement 7 parse errors detected in git-issue-3461.dfy diff --git a/docs/DafnyRef/GrammarDetails.md b/docs/DafnyRef/GrammarDetails.md index 79d8be47d26..af6ed32b078 100644 --- a/docs/DafnyRef/GrammarDetails.md +++ b/docs/DafnyRef/GrammarDetails.md @@ -1142,6 +1142,19 @@ CalcOp = ) ```` +#### 17.2.6.24. Opaque block {#g-opaque-block} + +([discussion](#sec-opaque-block)) + +````grammar +OpaqueBlock = "opaque" OpaqueSpec BlockStmt + +OpaqueSpec = { + | ModifiesClause(allowLambda: false) + | EnsuresClause(allowLambda: false) +} +```` + ### 17.2.7. Expressions #### 17.2.7.1. Top-level expression {#g-top-level-expression} diff --git a/docs/DafnyRef/Statements.md b/docs/DafnyRef/Statements.md index f85787e2e22..a47fc45aa9e 100644 --- a/docs/DafnyRef/Statements.md +++ b/docs/DafnyRef/Statements.md @@ -2476,4 +2476,27 @@ the expressions is to provide hints to aid Dafny in proving that step. As shown in the example, comments can also be used to aid the human reader in cases where Dafny can prove the step automatically. +## 8.24. Opaque Block ([grammar](#g-opaque-block)) {#sec-opaque-block} +As a Dafny sequence of statements grows in length, it can become harder to verify later statements in the block. With each statement, new information can become available, and with each modification of the heap, it becomes more expensive to access information from an older heap version. To reduce the verification complexity of long lists of statements, Dafny users can extract part of this block into a separate method or lemma. However, doing so introduces some boilerplate, which is where opaque blocks come in. They achieve a similar effect on verification performance as extracting code, but without the boilerplate. +An opaque block is similar to a block statement: it contains a sequence of zero or more statements, enclosed by curly braces. However, an opaque block is preceded by the keyword 'opaque', and may define ensures and modifies clauses before the curly braces. Anything that happens inside the block is invisible to the statements that come after it, unless it is specified by the ensures clause. Here is an example: + + +```dafny +method OpaqueBlockUser() returns (x: int) + ensures x > 4 +{ + x := 1; + var y := 1; + opaque + ensures x > 3 + { + x := x + y; + x := x + 2; + } + assert x == 4; // error + x := x + 1; +} +``` + +By default, the modifies clause of an opaque block is the same as that of the enclosing context. Opaque blocks may be nested. diff --git a/docs/DafnyRef/Statements.opaqueBlock.expect b/docs/DafnyRef/Statements.opaqueBlock.expect new file mode 100644 index 00000000000..dd8065e0784 --- /dev/null +++ b/docs/DafnyRef/Statements.opaqueBlock.expect @@ -0,0 +1,3 @@ +text.dfy(12,11): Error: assertion might not hold + +Dafny program verifier finished with 0 verified, 1 error