From 281ed82f24bcb0ba5f132a95d5691155d5c6d3be Mon Sep 17 00:00:00 2001 From: Aleksandr Fedchin Date: Tue, 9 Apr 2024 13:09:16 -0500 Subject: [PATCH] Counterexamples As Assumptions (#5013) ### Problem Right now Dafny reports counterexamples using special syntax that may be difficult to understand. For example, consider the following Dafny program that defines a standard `List` datatype with a function `View` that maps the list to a sequence of integers: ```Dafny datatype Node = Cons(next:Node, value:int) | Nil { function View():seq ensures Cons? ==> |View()| > 0 && View()[0] == value && View()[1..] == next.View() { if Nil? then [] else [value] + next.View() } } ``` Suppose we were to (incorrectly) assert that the list cannot correspond to the sequence of integers `[1, 2, 3]`, like so: ```Dafny method m(list:Node) { assert list.View() != [1, 2, 3]; } ``` Currently, Dafny would return the following counterexample: ``` At "method m(list:Node) {" (file.dfy:20): list:Problem.Node = Cons(next := @0, value := 1) @0:Problem.Node = Cons(next := @2, value := 2) @2:Problem.Node = Cons(next := @4, value := 3) @4:Problem.Node = Nil ``` This counterexample is confusing because it does not explain what the meaning of `@0`, `@1`, etc. is. The notation is different from the Dafny syntax, and it also does not capture some of the information that is actually contained within the counterexample because there is no way to express this information using this custom syntax. In particular, the counterexample constrains the value returned by calling `View()` on the `list` variable. This constrain might be redundant in this particular example but in general, we would want to capture all the information contained in the counterexample. ### Solution This PR redesigns the counterexample generation functionality so that counterexamples are represented internally and can be printed as Dafny assumptions. For example, for the program above, the counterexample will now look like this: ```Dafny assume Node.Cons(Node.Cons(Node.Cons(Node.Nil, 3), 2), 1) == list && Node.Cons(Node.Cons(Node.Cons(Node.Nil, 3), 2), 1).View.requires() && [1, 2, 3] == Node.Cons(Node.Cons(Node.Cons(Node.Nil, 3), 2), 1).View() && Node.Cons(Node.Cons(Node.Nil, 3), 2).View.requires() && [2, 3] == Node.Cons(Node.Cons(Node.Nil, 3), 2).View() && Node.Cons(Node.Nil, 3).View.requires() && [3] == Node.Cons(Node.Nil, 3).View() && Node.Nil.View.requires() && [] == Node.Nil.View(); ``` While admittedly more verbose because it explores the return values of functions, this counterexample precisely constrains the argument that leads to the assertion violation. In particular, if you were to insert this assumption into the code and revert the assertion, Dafny would verify that this counterexample is correct. At a high level, this makes the following changes: 1) Represent counterexamples as Dafny statements that the user can insert directly into their code to debug the failing assertion. 2) Make sure the counterexamples are wellformed, i.e. the constraints are ordered in such a way that the resulting assumption verifies. 3) Support counterexample constraints over function return values (as an example of something that can really only be done using native Dafny syntax) 4) Automatically fix counterexamples that are internally inconsistent, when such an inconsistency can be easily detected. For instance, a counterexample will never describe negative indices of an array or sequence, call a set empty if it contains elements, etc. All of these are possible in the counterexample model returned by Boogie but we prune such inconsistencies before reporting the counterexample, when possible. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin Co-authored-by: Aaron Tomb --- .../CounterExampleGeneration/Constraint.cs | 595 +++++++++ .../CounterExampleGeneration/DafnyModel.cs | 1064 +++++++++-------- .../DafnyModelState.cs | 236 ---- .../DafnyModelTypeUtils.cs | 43 +- .../DafnyModelVariable.cs | 299 ----- .../ModelFuncWrapper.cs | 34 +- .../CounterExampleGeneration/PartialState.cs | 324 +++++ .../CounterExampleGeneration/PartialValue.cs | 180 +++ .../CounterExampleGeneration/README.md | 15 - .../Verifier/BoogieGenerator.TrStatement.cs | 2 +- .../Verifier/CaptureStateExtensions.cs | 8 +- .../Various/CounterExampleTest.cs | 640 +++++----- .../Handlers/Custom/CounterExampleItem.cs | 11 +- .../Custom/DafnyCounterExampleHandler.cs | 14 +- Source/DafnyServer/CounterExampleProvider.cs | 11 +- Source/DafnyTestGeneration.Test/BasicTypes.cs | 2 +- .../DafnyTestGeneration.Test/Collections.cs | 1 + Source/DafnyTestGeneration/TestMethod.cs | 88 +- .../git-issues/git-issue-2026.dfy.expect | 29 +- .../LitTest/server/counterexample.transcript | 6 - .../server/counterexample.transcript.expect | 9 - .../server/counterexample_commandline.dfy | 3 +- .../counterexample_commandline.dfy.expect | 29 +- .../LitTest/server/git-issue223.transcript | 9 - .../server/git-issue223.transcript.expect | 17 - docs/DafnyRef/UserGuide.md | 20 +- 26 files changed, 2133 insertions(+), 1556 deletions(-) create mode 100644 Source/DafnyCore/CounterExampleGeneration/Constraint.cs delete mode 100644 Source/DafnyCore/CounterExampleGeneration/DafnyModelState.cs delete mode 100644 Source/DafnyCore/CounterExampleGeneration/DafnyModelVariable.cs create mode 100644 Source/DafnyCore/CounterExampleGeneration/PartialState.cs create mode 100644 Source/DafnyCore/CounterExampleGeneration/PartialValue.cs delete mode 100644 Source/DafnyCore/CounterExampleGeneration/README.md delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample.transcript delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample.transcript.expect delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/server/git-issue223.transcript delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/server/git-issue223.transcript.expect diff --git a/Source/DafnyCore/CounterExampleGeneration/Constraint.cs b/Source/DafnyCore/CounterExampleGeneration/Constraint.cs new file mode 100644 index 00000000000..190b21089cc --- /dev/null +++ b/Source/DafnyCore/CounterExampleGeneration/Constraint.cs @@ -0,0 +1,595 @@ +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +#nullable enable + +using System.Collections.Generic; +using System.Linq; +using Microsoft.Boogie; + +namespace Microsoft.Dafny; + +/// +/// This class represents constraints over partial values in the counterexample model. +/// A constraint is a Boolean expression over partial values. +/// +public abstract class Constraint { + + // We cannot add a constraint to the counterexample assumption until we know how to refer to each of the + // partial values referenced by the constraint: + private readonly List referencedValues; + public IEnumerable ReferencedValues => referencedValues.AsEnumerable(); + + protected Constraint(IEnumerable referencedValues, bool isWellFormedNessConstraint = false) { + this.referencedValues = referencedValues.ToList(); + if (isWellFormedNessConstraint) { + return; + } + foreach (var partialValue in this.referencedValues) { + partialValue.Constraints.Add(this); + } + } + + /// Return the Dafny expression corresponding to the constraint. + /// Maps a partial value to a Dafny expression by which we can refer to this value. + /// + public Expression? AsExpression(Dictionary definitions) { + if (referencedValues.Any(value => !definitions.ContainsKey(value))) { + return null; + } + var expression = AsExpressionHelper(definitions); + expression.Type = Type.Bool; + return expression; + } + + /// This is intended for debugging as we don't know apriori how to refer to partial values + public override string ToString() { + var temporaryIds = new Dictionary(); + foreach (var partialValue in referencedValues) { + temporaryIds[partialValue] = new IdentifierExpr(Token.NoToken, "E#" + partialValue.Element.Id); + } + if (this is DefinitionConstraint definitionConstraint) { + return definitionConstraint.RightHandSide(temporaryIds).ToString() ?? ""; + } + return AsExpression(temporaryIds)?.ToString() ?? ""; + } + + protected abstract Expression AsExpressionHelper(Dictionary definitions); + + + /// + /// Take a list of constraints and a dictionary of known ways to refer to partial values. + /// Update the dictionary according to the constraints in the list and return an ordered list of constraints that + /// can form a counterexample assumption. + /// + /// + /// + /// If false, do not allow new referring to partial values by identifiers + /// if True, remove constraints over literal values, since those should be self-evident + /// that are not already in knownDefinitions map + public static List ResolveAndOrder( + Dictionary knownDefinitions, + List constraints, + bool allowNewIdentifiers, + bool prune) { + Constraint? newConstraint = null; + var oldConstraints = new List(); + oldConstraints.AddRange(constraints.Where(constraint => + allowNewIdentifiers || constraint is not IdentifierExprConstraint)); + var newConstraints = new List(); + var knownAsLiteral = new HashSet(); + do { + if (newConstraint != null) { + oldConstraints.Remove(newConstraint); + } + + // Prioritize literals and display expressions + var displayConstraint = oldConstraints + .OfType() + .Where(constraint => constraint is LiteralExprConstraint || + constraint is SeqDisplayConstraint || + constraint is DatatypeValueConstraint) + .FirstOrDefault(constraint => !knownDefinitions.ContainsKey(constraint.DefinedValue) + && constraint.ReferencedValues.All(knownDefinitions.ContainsKey)); + if (displayConstraint != null) { + knownAsLiteral.Add(displayConstraint.DefinedValue); + knownDefinitions[displayConstraint.DefinedValue] = displayConstraint.RightHandSide(knownDefinitions); + knownDefinitions[displayConstraint.DefinedValue].Type = displayConstraint.DefinedValue.Type; + newConstraint = displayConstraint; + continue; + } + + // Add all constrains where we know how to refer to each referenced value + newConstraint = oldConstraints.Where(constraint => + constraint is not DefinitionConstraint && + constraint.ReferencedValues.All(knownDefinitions.ContainsKey)) + .FirstOrDefault(constraint => !prune || constraint is IdentifierExprConstraint || constraint.ReferencedValues.Any(value => !knownAsLiteral.Contains(value))); + if (newConstraint != null) { + newConstraints.Add(newConstraint); + continue; + } + + // update knownDefinitions map with new definitions + var definition = oldConstraints.OfType().FirstOrDefault(definition => + !knownDefinitions.ContainsKey(definition.DefinedValue) && + definition.ReferencedValues.All(knownDefinitions.ContainsKey)); + if (definition != null) { + if (!prune || definition is FunctionCallConstraint || + definition.referencedValues.Any(value => !knownAsLiteral.Contains(value))) { + newConstraints.AddRange(definition.WellFormed); + } + knownDefinitions[definition.DefinedValue] = definition.RightHandSide(knownDefinitions); + knownDefinitions[definition.DefinedValue].Type = definition.DefinedValue.Type; + newConstraint = definition; + continue; + } + + // append all other constraints to the end + newConstraint = oldConstraints.FirstOrDefault(constraint => !prune || constraint is FunctionCallConstraint || constraint is IdentifierExprConstraint || constraint.referencedValues.Any(value => !knownAsLiteral.Contains(value))); + if (newConstraint != null) { + if (newConstraint is DefinitionConstraint definitionConstraint) { + newConstraints.AddRange(definitionConstraint.WellFormed); + } + + newConstraints.Add(newConstraint); + } + } while (newConstraint != null); + + return newConstraints; + } + +} + +/// +/// Definition Constraint is a constraint that identifies a partial value with an expression over other partial values +/// +public abstract class DefinitionConstraint : Constraint { + + public readonly PartialValue DefinedValue; + public readonly List WellFormed; + + protected DefinitionConstraint( + IEnumerable referencedValues, + PartialValue definedValue, + List wellFormed) : base(referencedValues) { + DefinedValue = definedValue; + DefinedValue.Constraints.Add(this); + WellFormed = wellFormed; + } + + public abstract Expression RightHandSide(Dictionary definitions); + + protected override Expression AsExpressionHelper(Dictionary definitions) { + var expression = RightHandSide(definitions); + expression.Type = DefinedValue.Type; + var binaryExpr = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Eq, definitions[DefinedValue], expression) { + Type = Type.Bool + }; + return binaryExpr; + } +} + +public class IdentifierExprConstraint : DefinitionConstraint { + private readonly string name; + + public IdentifierExprConstraint(PartialValue definedValue, string name) + : base(new List(), definedValue, new List()) { + this.name = name; + } + + public override Expression RightHandSide(Dictionary definitions) { + return new IdentifierExpr(Token.NoToken, name); + } +} + +public class ArraySelectionConstraint : DefinitionConstraint { + public PartialValue Array; + public List indices; + + public ArraySelectionConstraint(PartialValue definedValue, PartialValue array, List indices) + : base(new List() { array }, definedValue, + new List() { new ArrayLengthConstraint(array, indices) }) { + Array = array; + this.indices = indices; + } + + public override Expression RightHandSide(Dictionary definitions) { + if (indices.Count == 1) { + return new SeqSelectExpr(Token.NoToken, true, definitions[Array], indices.First(), null, Token.NoToken); + } + return new MultiSelectExpr(Token.NoToken, definitions[Array], indices.OfType().ToList()); + } +} + +public class LiteralExprConstraint : DefinitionConstraint { + + public readonly Expression LiteralExpr; + public LiteralExprConstraint(PartialValue definedValue, Expression literalExpr) + : base(new List(), definedValue, new List()) { + LiteralExpr = literalExpr; + } + + public override Expression RightHandSide(Dictionary definitions) { + return LiteralExpr; + } +} + +public abstract class MemberSelectExprConstraint : DefinitionConstraint { + + public readonly PartialValue Obj; + public readonly string MemberName; + + protected MemberSelectExprConstraint( + PartialValue definedValue, + PartialValue obj, + string memberName, + List constraint) : base(new List { obj }, definedValue, constraint) { + Obj = obj; + MemberName = memberName; + } + + public override Expression RightHandSide(Dictionary definitions) { + return new MemberSelectExpr(Token.NoToken, definitions[Obj], MemberName); + } +} + +public class MemberSelectExprDatatypeConstraint : MemberSelectExprConstraint { + public MemberSelectExprDatatypeConstraint(PartialValue definedValue, PartialValue obj, string memberName) + : base(definedValue, obj, memberName, new List()) { } +} + +public class MemberSelectExprClassConstraint : MemberSelectExprConstraint { + public MemberSelectExprClassConstraint(PartialValue definedValue, PartialValue obj, string memberName) + : base(definedValue, obj, memberName, new List { new NotNullConstraint(obj) }) { + } +} + +public class DatatypeValueConstraint : DefinitionConstraint { + + public readonly IEnumerable UnnamedDestructors; + private readonly string constructorName; + private readonly string datatypeName; + + public DatatypeValueConstraint( + PartialValue definedValue, + string datatypeName, + string constructorName, + IReadOnlyCollection unnamedDestructors) + : base(unnamedDestructors, definedValue, new List()) { + UnnamedDestructors = unnamedDestructors; + this.constructorName = constructorName; + this.datatypeName = datatypeName; + } + + public override Expression RightHandSide(Dictionary definitions) { + return new DatatypeValue(Token.NoToken, datatypeName, + constructorName, + UnnamedDestructors.Select(destructor => definitions[destructor]).ToList()); + } +} + +public class SeqSelectExprConstraint : DefinitionConstraint { + + public readonly PartialValue Seq; + public readonly PartialValue Index; + + + public SeqSelectExprConstraint(PartialValue definedValue, PartialValue seq, PartialValue index) : base( + new List { seq, index }, definedValue, + new List { new CardinalityGtThanConstraint(seq, index) }) { + Seq = seq; + Index = index; + } + + public override Expression RightHandSide(Dictionary definitions) { + return new SeqSelectExpr( + Token.NoToken, + true, + definitions[Seq], + definitions[Index], + null, + Token.NoToken); + } +} + +public class MapSelectExprConstraint : DefinitionConstraint { + + public readonly PartialValue Map; + public readonly PartialValue Key; + + + public MapSelectExprConstraint(PartialValue definedValue, PartialValue map, PartialValue key) : base( + new List { map, key }, definedValue, new List { + new ContainmentConstraint(key, map, true) + }) { + Map = map; + Key = key; + } + + public override Expression RightHandSide(Dictionary definitions) { + return new SeqSelectExpr(Token.NoToken, true, definitions[Map], definitions[Key], null, Token.NoToken); + } +} + +public class SeqSelectExprWithLiteralConstraint : DefinitionConstraint { + + public readonly PartialValue Seq; + public readonly LiteralExpr Index; + + + public SeqSelectExprWithLiteralConstraint(PartialValue definedValue, PartialValue seq, LiteralExpr index) : base( + new List { seq }, definedValue, + new List { new CardinalityGtThanLiteralConstraint(seq, index) }) { + Seq = seq; + Index = index; + } + + public override Expression RightHandSide(Dictionary definitions) { + return new SeqSelectExpr(Token.NoToken, true, definitions[Seq], Index, null, Token.NoToken); + } +} + +public class CardinalityConstraint : DefinitionConstraint { + + public readonly PartialValue Collection; + + + public CardinalityConstraint(PartialValue definedValue, PartialValue collection) : base( + new List { collection }, definedValue, new List()) { + Collection = collection; + } + + public override Expression RightHandSide(Dictionary definitions) { + return new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Cardinality, definitions[Collection]); + } +} + +public class SeqDisplayConstraint : DefinitionConstraint { + private readonly List elements; + + + public SeqDisplayConstraint(PartialValue definedValue, List elements) : base(elements, definedValue, + new List()) { + this.elements = elements; + } + + public override Expression RightHandSide(Dictionary definitions) { + return new SeqDisplayExpr(Token.NoToken, elements.ConvertAll(element => definitions[element])); + } +} + +public class SetDisplayConstraint : Constraint { + private readonly List elements; + private readonly PartialValue set; + + + public SetDisplayConstraint(PartialValue set, List elements) : base(elements.Append(set)) { + this.elements = elements; + this.set = set; + } + + protected override Expression AsExpressionHelper(Dictionary definitions) { + var setDisplayExpr = new SetDisplayExpr(Token.NoToken, true, elements.ConvertAll(element => definitions[element])); + setDisplayExpr.Type = set.Type; + return new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Eq, definitions[set], setDisplayExpr); + } +} + +public class MapKeysDisplayConstraint : Constraint { + private readonly List elements; + private readonly PartialValue map; + + + public MapKeysDisplayConstraint(PartialValue map, List elements) : base(elements.Append(map)) { + this.elements = elements; + this.map = map; + } + + protected override Expression AsExpressionHelper(Dictionary definitions) { + var setDisplayExpr = new SetDisplayExpr(Token.NoToken, true, elements.ConvertAll(element => definitions[element])); + setDisplayExpr.Type = new SetType(true, map.Type.TypeArgs[0]); + var memberSelectExpr = new MemberSelectExpr(Token.NoToken, definitions[map], "Keys"); + memberSelectExpr.Type = new SetType(true, map.Type.TypeArgs[0]); + return new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Eq, memberSelectExpr, setDisplayExpr); + } +} + +public class FunctionCallConstraint : DefinitionConstraint { + private readonly List args; + private readonly PartialValue receiver; + private readonly string functionName; + + + public FunctionCallConstraint( + PartialValue definedValue, + PartialValue receiver, + List args, + string functionName, + bool receiverIsReferenceType) : base(args.Append(receiver), definedValue, + receiverIsReferenceType + ? new List + { new NotNullConstraint(receiver), new FunctionCallRequiresConstraint(receiver, args, functionName) } + : new List { new FunctionCallRequiresConstraint(receiver, args, functionName) }) { + this.args = args; + this.receiver = receiver; + this.functionName = functionName; + } + + public override Expression RightHandSide(Dictionary definitions) { + return new ApplySuffix( + Token.NoToken, + null, + new ExprDotName(Token.NoToken, definitions[receiver], functionName, null), + args.Select(formal => + new ActualBinding(null, definitions[formal])).ToList(), + Token.NoToken); + } +} + +public class FunctionCallRequiresConstraint : Constraint { + private readonly List args; + private readonly PartialValue receiver; + private readonly string functionName; + + + public FunctionCallRequiresConstraint(PartialValue receiver, List args, string functionName) + : base(args.Append(receiver), true) { + this.args = args; + this.receiver = receiver; + this.functionName = functionName; + } + + protected override Expression AsExpressionHelper(Dictionary definitions) { + return new ApplySuffix( + Token.NoToken, + null, + new ExprDotName(Token.NoToken, definitions[receiver], functionName + ".requires", null), + args.Select(formal => + new ActualBinding(null, definitions[formal])).ToList(), + Token.NoToken); + } +} + +public class ContainmentConstraint : Constraint { + + public readonly PartialValue Element, Set; + public readonly bool IsIn; + public ContainmentConstraint(PartialValue element, PartialValue set, bool isIn) + : base(new List { element, set }) { + Element = element; + Set = set; + this.IsIn = isIn; + } + + protected override Expression AsExpressionHelper(Dictionary definitions) { + return new BinaryExpr( + Token.NoToken, + IsIn ? BinaryExpr.Opcode.In : BinaryExpr.Opcode.NotIn, + definitions[Element], + definitions[Set]); + } +} + +public class ArrayLengthConstraint : Constraint { + + public PartialValue Array; + public List indices; + + public ArrayLengthConstraint(PartialValue array, List indices) + : base(new List { array }) { + Array = array; + this.indices = indices; + } + + protected override Expression AsExpressionHelper(Dictionary definitions) { + var length0 = new MemberSelectExpr(Token.NoToken, definitions[Array], indices.Count == 1 ? "Length" : "Length0"); + length0.Type = Type.Int; + var constraint = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Gt, length0, indices.First()); + constraint.Type = Type.Bool; + for (int i = 1; i < indices.Count; i++) { + var length = new MemberSelectExpr(Token.NoToken, definitions[Array], $"Length{i}"); + length.Type = Type.Int; + var newConstraint = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Gt, length, indices[i]); + newConstraint.Type = Type.Bool; + constraint = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, constraint, newConstraint); + constraint.Type = Type.Bool; + } + return constraint; + } +} + +public class NeqConstraint : Constraint { + private readonly PartialValue value; + private readonly PartialValue neq; + public NeqConstraint(PartialValue value, PartialValue neq) : base(new List { value, neq }) { + this.value = value; + this.neq = neq; + } + + protected override Expression AsExpressionHelper(Dictionary definitions) { + return new BinaryExpr( + Token.NoToken, + BinaryExpr.Opcode.Neq, + definitions[value], + definitions[neq]); + } +} + + +public class DatatypeConstructorCheckConstraint : Constraint { + private readonly PartialValue obj; + public readonly string ConstructorName; + + public DatatypeConstructorCheckConstraint(PartialValue obj, string constructorName) + : base(new List { obj }) { + this.obj = obj; + ConstructorName = constructorName; + } + + protected override Expression AsExpressionHelper(Dictionary definitions) { + return new MemberSelectExpr(Token.NoToken, definitions[obj], ConstructorName + "?"); + } +} + +public class CardinalityGtThanConstraint : Constraint { + private readonly PartialValue collection; + private readonly PartialValue bound; + + public CardinalityGtThanConstraint(PartialValue collection, PartialValue bound) + : base(new List { collection, bound }) { + this.collection = collection; + this.bound = bound; + } + + protected override Expression AsExpressionHelper(Dictionary definitions) { + var cardinalityExpr = new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Cardinality, definitions[collection]) { + Type = Type.Int + }; + return new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Gt, cardinalityExpr, definitions[bound]); + } +} + +public class CardinalityGtThanLiteralConstraint : Constraint { + private readonly PartialValue collection; + private readonly LiteralExpr bound; + + public CardinalityGtThanLiteralConstraint(PartialValue collection, LiteralExpr bound) + : base(new List { collection }) { + this.collection = collection; + this.bound = bound; + } + + protected override Expression AsExpressionHelper(Dictionary definitions) { + var cardinalityExpr = new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Cardinality, definitions[collection]) { + Type = Type.Int + }; + return new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Gt, cardinalityExpr, bound); + } +} + +public class TypeTestConstraint : Constraint { + public readonly Type Type; + private readonly PartialValue value; + public TypeTestConstraint(PartialValue value, Type type) : base(new List { value }) { + Type = type; + this.value = value; + } + + protected override Expression AsExpressionHelper(Dictionary definitions) { + return new TypeTestExpr(Token.NoToken, definitions[value], Type); + } +} + +public class NotNullConstraint : Constraint { + private readonly PartialValue value; + + public NotNullConstraint(PartialValue value) : base(new List { value }) { + this.value = value; + } + + protected override Expression AsExpressionHelper(Dictionary definitions) { + var nullValue = new LiteralExpr(Token.NoToken) { + Type = new InferredTypeProxy() + }; + return new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Neq, definitions[value], nullValue); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs index 9333dafe9ec..1ab7cfebe77 100644 --- a/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs +++ b/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs @@ -1,5 +1,6 @@ -// Copyright by the contributors to the Dafny Project +// Copyright by the contributors to the Dafny Project // SPDX-License-Identifier: MIT +#nullable enable using System; using System.Collections.Generic; @@ -8,6 +9,7 @@ using System.Numerics; using System.Text; using System.Text.RegularExpressions; +using Microsoft.BaseTypes; using Microsoft.Boogie; namespace Microsoft.Dafny { @@ -15,12 +17,13 @@ namespace Microsoft.Dafny { /// /// A wrapper around Boogie's Model class that allows extracting /// types and values of Elements representing Dafny variables. The three core - /// methods are: GetDafnyType, CanonicalName, and GetExpansion + /// methods are: GetDafnyType, DatatypeConstructorName, and GetExpansion /// public class DafnyModel { + public readonly List LoopGuards; private readonly DafnyOptions options; public readonly Model Model; - public readonly List States = new(); + public readonly List States = new(); public static readonly UserDefinedType UnknownType = new(new Token(), "?", null); private readonly ModelFuncWrapper fSetSelect, fSeqLength, fSeqIndex, fBox, @@ -28,24 +31,18 @@ public class DafnyModel { fNull, fSetUnion, fSetIntersection, fSetDifference, fSetUnionOne, fSetEmpty, fSeqEmpty, fSeqBuild, fSeqAppend, fSeqDrop, fSeqTake, fSeqUpdate, fSeqCreate, fU2Real, fU2Bool, fU2Int, - fMapDomain, fMapElements, fMapBuild, fIs, fIsBox, fUnbox; + fMapDomain, fMapElements, fMapValues, fMapBuild, fMapEmpty, fIs, fIsBox, fUnbox, fLs, fLz; private readonly Dictionary datatypeValues = new(); - - // maps a numeric type (int, real, bv4, etc.) to the set of integer - // values of that type that appear in the model. - private readonly Dictionary> reservedNumerals = new(); - // set of all UTF values for characters that appear in the model - private readonly HashSet reservedChars = new(); - private bool isTrueReserved; // True if "true" appears anywhere in the model - // maps an element representing a primitive to its string representation - private readonly Dictionary reservedValuesMap = new(); - // maps width to a unique object representing bitvector type of such width - private readonly Dictionary bitvectorTypes = new(); + private readonly List bitvectorFunctions = new(); // the model will begin assigning characters starting from this utf value - private const int FirstCharacterUtfValue = 65; // 'A' private static readonly Regex UnderscoreRemovalRegex = new("__"); + // This set is used by GetDafnyType to prevent infinite recursion + private HashSet exploredElements = new(); + + private readonly Dictionary concretizedValues = new(); + public DafnyModel(Model model, DafnyOptions options) { Model = model; this.options = options; @@ -70,7 +67,9 @@ public DafnyModel(Model model, DafnyOptions options) { fSetDifference = new ModelFuncWrapper(this, "Set#Difference", 2, 0); fMapDomain = new ModelFuncWrapper(this, "Map#Domain", 1, 0); fMapElements = new ModelFuncWrapper(this, "Map#Elements", 1, 0); + fMapValues = new ModelFuncWrapper(this, "Map#Values", 1, 0); fMapBuild = new ModelFuncWrapper(this, "Map#Build", 3, 0); + fMapEmpty = new ModelFuncWrapper(this, "Map#Empty", 0, 0); fIs = new ModelFuncWrapper(this, "$Is", 2, tyArgMultiplier); fIsBox = new ModelFuncWrapper(this, "$IsBox", 2, 0); fBox = new ModelFuncWrapper(this, "$Box", 1, tyArgMultiplier); @@ -86,15 +85,88 @@ public DafnyModel(Model model, DafnyOptions options) { fTag = new ModelFuncWrapper(this, "Tag", 1, 0); fBv = new ModelFuncWrapper(this, "TBitvector", 1, 0); fUnbox = new ModelFuncWrapper(this, "$Unbox", 2, 0); + fLs = new ModelFuncWrapper(this, "$LS", 1, 0); + fLz = new ModelFuncWrapper(this, "$LZ", 0, 0); InitDataTypes(); - RegisterReservedChars(); - RegisterReservedInts(); - RegisterReservedBools(); - RegisterReservedReals(); RegisterReservedBitVectors(); + LoopGuards = new List(); foreach (var s in model.States) { - var sn = new DafnyModelState(this, s); + var sn = new PartialState(this, s); States.Add(sn); + if (sn.IsLoopEntryState) { + LoopGuards.Add("counterexampleLoopGuard" + LoopGuards.Count); + } + sn.LoopGuards = LoopGuards.ToList(); + } + } + + public void AssignConcretePrimitiveValues() { + bool isTrueReserved = false; + foreach (var app in fU2Bool.Apps) { + isTrueReserved |= ((Model.Boolean)app.Result).Value; + } + foreach (var element in Model.Elements) { + var type = GetFormattedDafnyType(element); + if (type is BoolType && GetLiteralExpression(element, type) == null) { + if (isTrueReserved) { + concretizedValues[element] = new LiteralExpr(Token.NoToken, false); + } else { + concretizedValues[element] = new LiteralExpr(Token.NoToken, true); + } + continue; + } + if (GetLiteralExpression(element, type) != null) { + continue; + } + ModelFuncWrapper? otherValuesFunction = null; + switch (type) { + case BitvectorType bitvectorType: { + var funcName = "U_2_bv" + bitvectorType.Width; + if (Model.HasFunc(funcName)) { + otherValuesFunction = new ModelFuncWrapper(Model.GetFunc(funcName), 0); + } + break; + } + case CharType: + otherValuesFunction = fCharToInt; + break; + case RealType: + otherValuesFunction = fU2Real; + break; + case IntType: + otherValuesFunction = fU2Int; + break; + default: + continue; + } + var reservedValues = otherValuesFunction!.Apps + .Select(app => GetLiteralExpression(app.Result, type)) + .OfType() + .Select(literal => literal.ToString()).ToHashSet(); + reservedValues.UnionWith(concretizedValues.Values.Select(literal => literal.ToString())); + int numericalValue = -1; + LiteralExpr? literal = null; + bool literalIsReserved = true; + while (literalIsReserved) { + numericalValue++; + switch (type) { + case BitvectorType: + case IntType: { + literal = new LiteralExpr(Token.NoToken, BigInteger.Parse(numericalValue.ToString())); + break; + } + case CharType: + literal = new CharLiteralExpr(Token.NoToken, PrettyPrintChar(numericalValue)); + break; + case RealType: + literal = new LiteralExpr(Token.NoToken, BigDec.FromString(numericalValue.ToString())); + break; + } + if (!reservedValues.Contains(literal!.ToString())) { + literalIsReserved = false; + } + } + concretizedValues[element] = literal!; } } @@ -113,14 +185,17 @@ public static DafnyModel ExtractModel(DafnyOptions options, string mv) { public override string ToString() { var result = new StringBuilder(); + AssignConcretePrimitiveValues(); + result.AppendLine("WARNING: the following counterexample may be inconsistent or invalid. See dafny.org/dafny/DafnyRef/DafnyRef#sec-counterexamples"); + if (LoopGuards.Count > 0) { + result.AppendLine("Temporary variables to describe counterexamples: "); + foreach (var loopGuard in LoopGuards) { + result.AppendLine($"ghost var {loopGuard} : bool := false;"); + } + } foreach (var state in States.Where(state => state.StateContainsPosition())) { result.AppendLine(state.FullStateName + ":"); - var vars = state.ExpandedVariableSet(-1); - foreach (var variable in vars) { - result.AppendLine($"\t{variable.ShortName} : " + - $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " + - $"{variable.Value}"); - } + result.AppendLine(state.AsAssumption().ToString()); } return result.ToString(); } @@ -145,71 +220,33 @@ private void InitDataTypes() { } } - /// Register all char values specified by the model - private void RegisterReservedChars() { - foreach (var app in fCharToInt.Apps) { - if (int.TryParse(((Model.Integer)app.Result).Numeral, - out var UTFCode) && UTFCode is <= char.MaxValue and >= 0) { - reservedChars.Add(UTFCode); - } - } - } - /// /// Return the character representation of a UTF code understood by Dafny /// This is either the character itself, if it is a parsable ASCII, /// Escaped character, for the cases specified in Dafny manual, /// Or escaped UTF code otherwise /// - private string PrettyPrintChar(int UTFCode) { - switch (UTFCode) { + private static string PrettyPrintChar(int utfCode) { + switch (utfCode) { case 0: - return "'\\0'"; + return "\\0"; case 9: - return "'\\t'"; + return "\\t"; case 10: - return "'\\n'"; + return "\\n"; case 13: - return "'\\r'"; + return "\\r"; case 34: - return "'\\\"'"; + return "\\\""; case 39: - return "'\\\''"; + return "\\\'"; case 92: - return "'\\\\'"; + return "\\\\"; default: - if ((UTFCode >= 32) && (UTFCode <= 126)) { - return $"'{Convert.ToChar(UTFCode)}'"; + if (utfCode is >= 32 and <= 126) { + return $"{Convert.ToChar(utfCode)}"; } - return $"'\\u{UTFCode:X4}'"; - } - } - - /// Registered all int values specified by the model - private void RegisterReservedInts() { - reservedNumerals[Type.Int] = new(); - foreach (var app in fU2Int.Apps) { - if (app.Result is Model.Integer integer && int.TryParse(integer.Numeral, out int value)) { - reservedNumerals[Type.Int].Add(value); - } - } - } - - /// Registered all bool values specified by the model - private void RegisterReservedBools() { - foreach (var app in fU2Bool.Apps) { - isTrueReserved |= ((Model.Boolean)app.Result).Value; - } - } - - /// Registered all real values specified by the model - private void RegisterReservedReals() { - reservedNumerals[Type.Real] = new(); - foreach (var app in fU2Real.Apps) { - var valueAsString = app.Result.ToString()?.Split(".")[0] ?? ""; - if ((app.Result is Model.Real) && int.TryParse(valueAsString, out int value)) { - reservedNumerals[Type.Real].Add(value); - } + return $"\\U{{{utfCode:X4}}}"; } } @@ -220,46 +257,39 @@ private void RegisterReservedBitVectors() { if (!bvFuncName.IsMatch(func.Name)) { continue; } - - int width = int.Parse(func.Name[6..]); - if (!bitvectorTypes.ContainsKey(width)) { - bitvectorTypes[width] = new BitvectorType(options, width); - } - - var type = bitvectorTypes[width]; - - if (!reservedNumerals.ContainsKey(type)) { - reservedNumerals[type] = new(); - } - - foreach (var app in func.Apps) { - if (int.TryParse((app.Result as Model.BitVector).Numeral, - out var value)) { - reservedNumerals[type].Add(value); - } - } + bitvectorFunctions.Add(func); } } - /// - /// Return True iff the variable name is referring to a variable that has - /// a direct analog in Dafny source (i.e. not $Heap, $_Frame, $nw, etc.) - /// - public static bool IsUserVariableName(string name) => - !name.Contains("$") && name.Count(c => c == '#') <= 1; - - public bool ElementIsNull(Model.Element element) => element == fNull.GetConstant(); - /// /// Return the name of a 0-arity type function that maps to the element if such /// a function exists and is unique. Return null otherwise. /// - private static string GetTrueTypeName(Model.Element element) { - return element?.Names.FirstOrDefault(funcTuple => funcTuple.Func.Arity == 0)?.Func.Name; + private static string? GetTrueTypeName(Model.Element element) { + return element.Names.FirstOrDefault(funcTuple => funcTuple.Func.Arity == 0)?.Func.Name; } /// Get the Dafny type of an element - internal Type GetDafnyType(Model.Element element) { + internal Type GetFormattedDafnyType(Model.Element element) { + exploredElements = new HashSet(); + return DafnyModelTypeUtils.GetInDafnyFormat(GetDafnyType(element)); + } + + internal void AddTypeConstraints(PartialValue partialValue) { + foreach (var typeElement in GetIsResults(partialValue.Element)) { + var reconstructedType = DafnyModelTypeUtils.GetInDafnyFormat(ReconstructType(typeElement)); + if (reconstructedType.ToString() != partialValue.Type.ToString()) { + var _ = new TypeTestConstraint(partialValue, reconstructedType); + } + } + } + + /// Get the Dafny type of an element + private Type GetDafnyType(Model.Element element) { + if (exploredElements.Contains(element)) { + return UnknownType; + } + exploredElements.Add(element); switch (element.Kind) { case Model.ElementKind.Boolean: return Type.Bool; @@ -270,7 +300,7 @@ internal Type GetDafnyType(Model.Element element) { case Model.ElementKind.BitVector: return new BitvectorType(options, ((Model.BitVector)element).Size); case Model.ElementKind.Uninterpreted: - return GetDafnyType(element as Model.Uninterpreted); + return GetDafnyType((element as Model.Uninterpreted)!); case Model.ElementKind.DataValue: if (((Model.DatatypeValue)element).ConstructorName is "-" or "/") { return GetDafnyType( @@ -295,10 +325,351 @@ internal Type GetDafnyType(Model.Element element) { return result; } + private Expression? GetLiteralExpression(Model.Element element, Type type) { + var result = GetLiteralExpressionHelper(element, type); + if (concretizedValues.ContainsKey(element) && result == null) { + result = concretizedValues[element]; + } + if (result != null) { + result.Type = type; + } + return result; + } + + /// + /// If the provided represents a literal in Dafny, return that literal. + /// Otherwise, return null. + /// + private Expression? GetLiteralExpressionHelper(Model.Element element, Type type) { + if (Equals(element, fNull.GetConstant())) { + return new LiteralExpr(Token.NoToken); + } + + if (element is not Model.Real && element is Model.Number number) { + return new LiteralExpr(Token.NoToken, BigInteger.Parse(number.Numeral)); + } + + if (element is Model.Real real) { + return new LiteralExpr(Token.NoToken, BigDec.FromString(real.ToString())); + } + + if (element is Model.Boolean boolean) { + return new LiteralExpr(Token.NoToken, boolean.Value); + } + + if (element.Kind == Model.ElementKind.DataValue) { + var datatypeValue = (Model.DatatypeValue)element; + switch (datatypeValue.ConstructorName) { + case "-": + return new NegationExpression(Token.NoToken, + GetLiteralExpression(datatypeValue.Arguments.First(), type)); + case "/": + return new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Div, + GetLiteralExpression(datatypeValue.Arguments[0], type), + GetLiteralExpression(datatypeValue.Arguments[1], type)); + } + } + + var unboxedValue = fU2Int.OptEval(element); + unboxedValue ??= fU2Bool.OptEval(element); + unboxedValue ??= fU2Real.OptEval(element); + if (unboxedValue != null) { + return GetLiteralExpression(unboxedValue, type); + } + + if (fCharToInt.OptEval(element) is Model.Integer literalCharValue) { + if (int.TryParse(literalCharValue.Numeral, + out var utfCode) && utfCode is <= char.MaxValue and >= 0) { + return new CharLiteralExpr(Token.NoToken, PrettyPrintChar(utfCode)); + } + } + + foreach (var bitvectorFunction in bitvectorFunctions) { + if (bitvectorFunction.OptEval(element) is Model.Number literalBitVectorValur) { + return new LiteralExpr(Token.NoToken, + BigInteger.Parse(literalBitVectorValur.Numeral)); + } + } + + return null; + } + + public void GetExpansion(PartialState state, PartialValue value) { + var literalExpr = GetLiteralExpression(value.Element, value.Type); + if (literalExpr != null) { + var _ = new LiteralExprConstraint(value, literalExpr); + return; + } + + if (value.Nullable) { + var _ = new NotNullConstraint(value); + } + + if (value.Type is BitvectorType || value.Type is CharType || value.Type is RealType || value.Type is BoolType || value.Type is IntType) { + foreach (var element in Model.Elements.Where(element => !Equals(element, value.Element))) { + var elementType = GetFormattedDafnyType(element); + if (elementType.ToString() == value.Type.ToString()) { + var partialValue = PartialValue.Get(element, state); + var _ = new NeqConstraint(value, partialValue); + } + } + return; + } + + var valueIsDatatype = datatypeValues.TryGetValue(value.Element, out var fnTuple); + + var layerValue = fLz.GetConstant(); + while (layerValue != null && fLs.AppWithArg(0, layerValue) != null && !Equals(fLs.AppWithArg(0, layerValue)!.Result, fLz.GetConstant())) { + layerValue = fLs.AppWithArg(0, layerValue)!.Result; + } + var functionApplications = GetFunctionConstants(value.Element, layerValue); + foreach (var functionApplication in functionApplications) { + var result = PartialValue.Get(functionApplication.Result, state); + var args = functionApplication.Args.Select(arg => PartialValue.Get(arg, state)).ToList(); + args = Equals(functionApplication.Args[0], layerValue) ? args.Skip(2).ToList() : args.Skip(1).ToList(); + var _ = new FunctionCallConstraint(result, value, args, functionApplication.Func.Name.Split(".").Last(), !valueIsDatatype); + } + + if (valueIsDatatype) { + var __ = new DatatypeConstructorCheckConstraint(value, fnTuple!.Func.Name.Split(".").Last()); + // Elt is a datatype value + var destructors = GetDestructorFunctions(value.Element).OrderBy(f => f.Name).ToList(); + if (destructors.Count > fnTuple.Args.Length) { + // Try to filter out predicate functions + // (that follow a format very similar to that of destructor names) + destructors = destructors.Where(destructor => + fnTuple.Args.Any(arg => Equals(destructor.OptEval(value.Element), arg))) + .ToList(); + } + + var elements = new List(); + if (destructors.Count == fnTuple.Args.Length) { + // we know all destructor names + foreach (var func in destructors) { + if (func.OptEval(value.Element) is not { } modelElement) { + continue; + } + var element = PartialValue.Get(UnboxNotNull(modelElement), state); + elements.Add(element); + var elementName = UnderscoreRemovalRegex.Replace(func.Name.Split(".").Last(), "_"); + var _ = new MemberSelectExprDatatypeConstraint(element, value, elementName); + } + } else { + // we don't know destructor names, so we use indices instead + for (int i = 0; i < fnTuple.Args.Length; i++) { + var element = PartialValue.Get(UnboxNotNull(fnTuple.Args[i]), state); + elements.Add(element); + } + } + var ___ = new DatatypeValueConstraint(value, value.Type.ToString(), fnTuple.Func.Name.Split(".").Last(), elements); + return; + } + + switch (value.Type) { + case SeqType: { + if (fSeqEmpty.AppWithResult(value.Element) != null) { + var _ = new LiteralExprConstraint(value, new SeqDisplayExpr(Token.NoToken, new List())); + return; + } + var lenghtTuple = fSeqLength.AppWithArg(0, value.Element); + BigNum seqLength = BigNum.MINUS_ONE; + if (lenghtTuple != null) { + var lengthValue = PartialValue.Get(lenghtTuple.Result, state); + var lengthValueLiteral = GetLiteralExpression(lengthValue.Element, lengthValue.Type); + if (lengthValueLiteral != null) { + BigNum.TryParse(lengthValueLiteral.ToString(), out seqLength); + } + var _ = new CardinalityConstraint(lengthValue, value); + } + + // Sequences can be constructed with the build operator: + List elements = new(); + + Model.Element substring = value.Element; + while (fSeqBuild.AppWithResult(substring) != null) { + elements.Insert(0, PartialValue.Get(UnboxNotNull(fSeqBuild.AppWithResult(substring)!.Args[1]), state)); + substring = fSeqBuild.AppWithResult(substring)!.Args[0]; + } + + for (int i = 0; i < elements.Count; i++) { + var index = new LiteralExpr(Token.NoToken, i) { + Type = Type.Int + }; + var _ = new SeqSelectExprWithLiteralConstraint(elements[i], value, index); + } + + if (elements.Count == 0) { + foreach (var funcTuple in fSeqIndex.AppsWithArg(0, value.Element)) { + var elementId = PartialValue.Get(funcTuple.Args[1], state); + var elementIdTry = GetLiteralExpression(funcTuple.Args[1], Type.Int); + if (elementIdTry != null && elementIdTry.ToString().Contains("-")) { + continue; + } + if (elementIdTry != null && BigNum.TryParse(elementIdTry.ToString(), out var elementIdTryBigNum)) { + if (!seqLength.Equals(BigNum.MINUS_ONE) && !(elementIdTryBigNum - seqLength).IsNegative) { + continue; // element out of bounds for sequence + } + } + var element = PartialValue.Get(UnboxNotNull(funcTuple.Result), state); + var _ = new SeqSelectExprConstraint(element, value, elementId); + } + } else { + var _ = new SeqDisplayConstraint(value, elements); + } + + return; + } + case SetType: { + if (fMapDomain.AppsWithResult(value.Element).Any()) { + foreach (var map in fMapDomain.AppsWithResult(value.Element)) { + var mapValue = PartialValue.Get(map.Args[0], state); + var _ = new MemberSelectExprDatatypeConstraint(value, mapValue, "Keys"); + } + return; + } + if (fMapValues.AppsWithResult(value.Element).Any()) { + foreach (var map in fMapValues.AppsWithResult(value.Element)) { + var mapValue = PartialValue.Get(map.Args[0], state); + var _ = new MemberSelectExprDatatypeConstraint(value, mapValue, "Values"); + } + } + if (fSetEmpty.AppWithResult(value.Element) != null) { + var _ = new LiteralExprConstraint(value, new SetDisplayExpr(Token.NoToken, true, new List())); + return; + } + + foreach (var tpl in fSetSelect.AppsWithArg(0, value.Element)) { + var setElement = PartialValue.Get(UnboxNotNull(tpl.Args[1]), state); + var containment = tpl.Result; + if (containment is Model.Boolean boolean) { + var _ = new ContainmentConstraint(setElement, value, boolean.Value); + } + } + + return; + } + case MapType: { + var mapKeysAdded = new HashSet(); // prevents mapping a key to multiple values + var mapsElementsVisited = new HashSet(); // prevents infinite recursion + var current = value.Element; + var mapBuilds = fMapBuild.AppsWithResult(current).ToList(); + var result = new List(); + while (mapBuilds.Count != 0) { + foreach (var mapBuild in mapBuilds.Where(m => Equals(m.Args[0], current))) { + result.AddRange(AddMappingHelper( + state, + value, + Unbox(mapBuild.Args[1]), + Unbox(mapBuild.Args[2]), + mapKeysAdded)); + } + + mapsElementsVisited.Add(current); + var nextMapBuild = mapBuilds.FirstOrDefault(m => !mapsElementsVisited.Contains(m.Args[0])); + if (nextMapBuild == null) { + return; + } + + current = nextMapBuild.Args[0]; + mapBuilds = fMapBuild.AppsWithResult(nextMapBuild.Args[0]) + .Where(m => !mapsElementsVisited.Contains(m.Args[0])).ToList(); + result.AddRange(AddMappingHelper( + state, + value, + Unbox(nextMapBuild.Args[1]), + Unbox(nextMapBuild.Args[2]), + mapKeysAdded)); + } + + var mapDomain = fMapDomain.OptEval(current); + var mapElements = fMapElements.OptEval(current); + if (mapDomain != null && mapElements != null) { + foreach (var app in fSetSelect.AppsWithArg(0, mapDomain)) { + var valueElement = fSetSelect.OptEval(mapElements, app.Args[1]); + if (valueElement != null) { + valueElement = Unbox(valueElement); + } + result.AddRange(AddMappingHelper( + state, + value, + Unbox(app.Args[1]), + valueElement, + mapKeysAdded, !((Model.Boolean)app.Result).Value)); + } + } + + + if (!result.Any() && fMapEmpty.AppWithResult(value.Element) != null) { + var _ = new LiteralExprConstraint(value, new MapDisplayExpr(Token.NoToken, true, new List())); + } + + return; + + } + default: { + + var heap = state.State.TryGet("$Heap"); + // Elt is an array or an object: + if (heap == null) { + return; + } + + var constantFields = GetDestructorFunctions(value.Element).OrderBy(f => f.Name).ToList(); + var fields = fSetSelect.AppsWithArgs(0, heap, 1, value.Element).ToList(); + + foreach (var fieldFunc in constantFields) { + if (fieldFunc.OptEval(value.Element) is not { } modelElement) { + continue; + } + var field = PartialValue.Get(UnboxNotNull(modelElement), state); + var fieldName = UnderscoreRemovalRegex.Replace(fieldFunc.Name.Split(".").Last(), "_"); + if (fieldName.Contains("#")) { + continue; + } + var _ = new MemberSelectExprClassConstraint(field, value, fieldName); + } + + if (!fields.Any()) { + return; + } + + foreach (var tpl in fSetSelect.AppsWithArg(0, fields.ToList()[0].Result)) { + foreach (var fieldName in GetFieldNames(tpl.Args[1])) { + if (fieldName != "alloc") { + var field = PartialValue.Get(UnboxNotNull(tpl.Result), state); + // make sure the field in quetion is not an array index + if (fieldName.Contains("#")) { + continue; + } + if (fieldName.StartsWith('[') && fieldName.EndsWith(']')) { + var indexStrings = fieldName.TrimStart('[').TrimEnd(']').Split(","); + var indices = new List(); + foreach (var indexString in indexStrings) { + if (BigInteger.TryParse(indexString, out var index)) { + var indexLiteral = new LiteralExpr(Token.NoToken, index); + indexLiteral.Type = Type.Int; + indices.Add(indexLiteral); + } + } + if (indices.Count != indexStrings.Length) { + continue; + } + var _ = new ArraySelectionConstraint(field, value, indices); + } else { + var _ = new MemberSelectExprClassConstraint(field, value, fieldName); + } + } + } + } + return; + } + } + } + /// /// Get the Dafny type of the value indicated by /// This is in contrast to ReconstructType, which returns the type indicated by the element itself. - /// This method tries to extract the base type (so seq instead of string) + /// This method tries to extract the base type (so sequence of characters instead of string) /// private Type GetDafnyType(Model.Uninterpreted element) { var finalResult = UnknownType; @@ -312,43 +683,30 @@ private Type GetDafnyType(Model.Uninterpreted element) { } } var seqOperation = fSeqAppend.AppWithResult(element); - seqOperation ??= fSeqDrop.AppWithResult(element); - seqOperation ??= fSeqTake.AppWithResult(element); - seqOperation ??= fSeqUpdate.AppWithResult(element); - if (seqOperation != null) { - return GetDafnyType(seqOperation.Args[0]); - } + if (seqOperation != null && !exploredElements.Contains(seqOperation.Args[0])) { return GetDafnyType(seqOperation.Args[0]); } + seqOperation = fSeqDrop.AppWithResult(element); + if (seqOperation != null && !exploredElements.Contains(seqOperation.Args[0])) { return GetDafnyType(seqOperation.Args[0]); } + seqOperation = fSeqTake.AppWithResult(element); + if (seqOperation != null && !exploredElements.Contains(seqOperation.Args[0])) { return GetDafnyType(seqOperation.Args[0]); } + seqOperation = fSeqUpdate.AppWithResult(element); + if (seqOperation != null && !exploredElements.Contains(seqOperation.Args[0])) { return GetDafnyType(seqOperation.Args[0]); } seqOperation = fSeqBuild.AppWithResult(element); - if (seqOperation != null) { - return new SeqType(GetDafnyType(Unbox(seqOperation.Args[1]))); - } + if (seqOperation != null && !exploredElements.Contains(UnboxNotNull(seqOperation.Args[1]))) { return new SeqType(GetDafnyType(UnboxNotNull(seqOperation.Args[1]))); } seqOperation = fSeqCreate.AppWithResult(element); - seqOperation ??= fSeqEmpty.AppWithResult(element); - if (seqOperation != null) { - return new SeqType(ReconstructType(seqOperation.Args.First())); - } + if (seqOperation != null && !exploredElements.Contains(UnboxNotNull(seqOperation.Args.First()))) { return new SeqType(ReconstructType(seqOperation.Args.First())); } + if (fSeqEmpty.AppWithResult(element) != null) { return new SeqType(null); } var setOperation = fSetUnion.AppWithResult(element); - setOperation ??= fSetIntersection.AppWithResult(element); - setOperation ??= fSetDifference.AppWithResult(element); - if (setOperation != null) { - return GetDafnyType(setOperation.Args[0]); - } + if (setOperation != null && !exploredElements.Contains(setOperation.Args[0])) { return GetDafnyType(setOperation.Args[0]); } + setOperation = fSetIntersection.AppWithResult(element); + if (setOperation != null && !exploredElements.Contains(setOperation.Args[0])) { return GetDafnyType(setOperation.Args[0]); } + setOperation = fSetDifference.AppWithResult(element); + if (setOperation != null && !exploredElements.Contains(setOperation.Args[0])) { return GetDafnyType(setOperation.Args[0]); } setOperation = fSetUnionOne.AppWithResult(element); - if (setOperation != null) { - return new SetType(true, GetDafnyType(Unbox(setOperation.Args[1]))); - } - setOperation = fSetEmpty.AppWithResult(element); - if (setOperation != null) { - var setElement = fSetSelect.AppWithArg(0, element); - if (setElement != null) { - return new SetType(true, GetDafnyType(setElement.Args[1])); - } - // not possible to infer the type argument in this case if type encoding is Arguments - return new SetType(true, UnknownType); - } + if (setOperation != null && !exploredElements.Contains(setOperation.Args[1])) { return new SetType(true, GetDafnyType(UnboxNotNull(setOperation.Args[1]))); } + if (fSetEmpty.AppWithResult(element) != null) { return new SetType(true, null); } var mapOperation = fMapBuild.AppWithResult(element); if (mapOperation != null) { - return new MapType(true, GetDafnyType(Unbox(mapOperation.Args[1])), GetDafnyType(Unbox(mapOperation.Args[2]))); + return new MapType(true, GetDafnyType(UnboxNotNull(mapOperation.Args[1])), GetDafnyType(UnboxNotNull(mapOperation.Args[2]))); } var unboxedTypes = fIsBox.AppsWithArg(0, element) .Where(tuple => ((Model.Boolean)tuple.Result).Value) @@ -363,18 +721,25 @@ private Type GetDafnyType(Model.Uninterpreted element) { return finalResult; } var dtypeElement = fDtype.OptEval(element); - return dtypeElement != null ? ReconstructType(dtypeElement) : finalResult; + if (dtypeElement != null) { + ReconstructType(dtypeElement); + } + if (datatypeValues.TryGetValue(element, out var fnTuple)) { + var fullyQualifiedPath = fnTuple.Func.Name[1..].Split("."); + return new UserDefinedType(Token.NoToken, string.Join(".", fullyQualifiedPath.Take(fullyQualifiedPath.Count() - 1)), null); + } + return finalResult; } /// /// Reconstruct Dafny type from an element that represents a type in Z3 /// - private Type ReconstructType(Model.Element typeElement) { + private Type ReconstructType(Model.Element? typeElement) { if (typeElement == null) { return UnknownType; } var fullName = GetTrueTypeName(typeElement); - if (fullName != null && fullName.Length > 7 && fullName[..7].Equals("Tclass.")) { + if (fullName is { Length: > 7 } && fullName[..7].Equals("Tclass.")) { return new UserDefinedType(new Token(), fullName[7..], null); } switch (fullName) { @@ -387,8 +752,8 @@ private Type ReconstructType(Model.Element typeElement) { case "TChar": return Type.Char; } - if (fBv.AppWithResult(typeElement) != null) { - return new BitvectorType(options, ((Model.Integer)fBv.AppWithResult(typeElement).Args[0]).AsInt()); + if (fBv.AppWithResult(typeElement) is { } tupleWrapper) { + return new BitvectorType(options, ((Model.Integer)tupleWrapper.Args[0]).AsInt()); } Type fallBackType = UnknownType; // to be returned in the event all else fails @@ -432,369 +797,106 @@ private Type ReconstructType(Model.Element typeElement) { } } - /// - /// Extract the string representation of the element. - /// Return "" if !IsPrimitive(elt, state) unless elt is a datatype, - /// in which case return the corresponding constructor name. - /// - public string CanonicalName(Model.Element elt, Type type) { - if (elt == null || (type is UserDefinedType userDefinedType && userDefinedType.Name == UnknownType.Name)) { - return "?"; - } - if (elt == fNull.GetConstant()) { - return "null"; - } - if (elt is Model.Integer or Model.Boolean or Model.Real) { - return elt.ToString(); - } - if (elt is Model.BitVector vector) { - return vector.Numeral; - } - if (elt.Kind == Model.ElementKind.DataValue) { - if (((Model.DatatypeValue)elt).ConstructorName == "-") { - return "-" + CanonicalName(((Model.DatatypeValue)elt).Arguments.First(), type); - } - if (((Model.DatatypeValue)elt).ConstructorName == "/") { - return CanonicalName(((Model.DatatypeValue)elt).Arguments.First(), type) + - "/" + CanonicalName(((Model.DatatypeValue)elt).Arguments[1], type); - } - } - if (datatypeValues.TryGetValue(elt, out var fnTuple)) { - return fnTuple.Func.Name.Split(".").Last(); - } - switch (type) { - case BitvectorType bitvectorType: { - int width = bitvectorType.Width; - var funcName = "U_2_bv" + width; - if (!bitvectorTypes.ContainsKey(width)) { - bitvectorTypes[width] = new BitvectorType(options, width); - reservedNumerals[bitvectorTypes[width]] = new HashSet(); - } - if (!Model.HasFunc(funcName)) { - return GetUnreservedNumericValue(elt, bitvectorTypes[width]); - } - if (Model.GetFunc(funcName).OptEval(elt) != null) { - return (Model.GetFunc(funcName).OptEval(elt) as Model.Number)?.Numeral; - } - return GetUnreservedNumericValue(elt, bitvectorTypes[width]); - } - case CharType: { - if (fCharToInt.OptEval(elt) != null) { - if (int.TryParse(((Model.Integer)fCharToInt.OptEval(elt)).Numeral, - out var UTFCode) && UTFCode is <= char.MaxValue and >= 0) { - return PrettyPrintChar(UTFCode); - } - } - return GetUnreservedCharValue(elt); - } - case RealType when fU2Real.OptEval(elt) != null: - return CanonicalName(fU2Real.OptEval(elt), type); - case RealType: - return GetUnreservedNumericValue(elt, Type.Real); - case BoolType when fU2Bool.OptEval(elt) != null: - return CanonicalName(fU2Bool.OptEval(elt), type); - case BoolType: - return GetUnreservedBoolValue(elt); - case IntType when fU2Int.OptEval(elt) != null: - return CanonicalName(fU2Int.OptEval(elt), type); - case IntType: - return GetUnreservedNumericValue(elt, Type.Int); - default: - return ""; - } - } - - /// - /// Find a char value that is different from any other value - /// of that type in the entire model. Reserve that value for given element - /// - private string GetUnreservedCharValue(Model.Element element) { - if (reservedValuesMap.TryGetValue(element, out var reservedValue)) { - return reservedValue; - } - int i = FirstCharacterUtfValue; - while (reservedChars.Contains(i)) { - i++; - } - reservedValuesMap[element] = PrettyPrintChar(i); - reservedChars.Add(i); - return reservedValuesMap[element]; - } - - /// - /// Find a bool value that is different from any other value - /// of that type in the entire model (if possible). - /// Reserve that value for given element - /// - private string GetUnreservedBoolValue(Model.Element element) { - if (reservedValuesMap.TryGetValue(element, out var reservedValue)) { - return reservedValue; - } - if (!isTrueReserved) { - isTrueReserved = true; - reservedValuesMap[element] = true.ToString().ToLower(); - } else { - reservedValuesMap[element] = false.ToString().ToLower(); - } - return reservedValuesMap[element]; - } - - /// - /// Find a value of the given numericType that is different from - /// any other value of that type in the entire model. - /// Reserve that value for given element - /// - public string GetUnreservedNumericValue(Model.Element element, Type numericType) { - if (reservedValuesMap.TryGetValue(element, out var reservedValue)) { - return reservedValue; - } - int i = 0; - while (reservedNumerals[numericType].Contains(i)) { - i++; - } - if (numericType == Type.Real) { - reservedValuesMap[element] = i + ".0"; - } else { - reservedValuesMap[element] = i.ToString(); - } - reservedNumerals[numericType].Add(i); - return reservedValuesMap[element]; - } - /// /// Perform operations necessary to add a mapping to a map variable, - /// return newly created DafnyModelVariable objects + /// return newly created PartialValue objects /// - private IEnumerable AddMappingHelper(DafnyModelState state, MapVariable mapVariable, Model.Element keyElement, Model.Element valueElement, HashSet keySet) { - if (mapVariable == null) { + private IEnumerable AddMappingHelper(PartialState state, PartialValue? mapVariable, Model.Element? keyElement, Model.Element? valueElement, HashSet keySet, bool keyNotPresent = false) { + if (mapVariable == null || keyElement == null || keySet.Contains(keyElement)) { yield break; } - var pairId = mapVariable.Children.Count.ToString(); - var key = DafnyModelVariableFactory.Get(state, keyElement, pairId, mapVariable); - if (valueElement != null) { - var value = DafnyModelVariableFactory.Get(state, valueElement, pairId, mapVariable); - mapVariable.AddMapping(key, value); + var key = PartialValue.Get(keyElement, state); + var opcode = keyNotPresent ? BinaryExpr.Opcode.NotIn : BinaryExpr.Opcode.In; + var _ = new ContainmentConstraint(key, mapVariable, opcode == BinaryExpr.Opcode.In); + // Note that it is possible for valueElement to not be null while the element is not present in the set! + if (valueElement != null && !keyNotPresent) { + var value = PartialValue.Get(valueElement, state); + var __ = new MapSelectExprConstraint(value, mapVariable, key); yield return value; - } else { - mapVariable.AddMapping(key, null); } keySet.Add(keyElement); yield return key; } /// - /// Return a set of variables associated with an element. These could be - /// values of fields for objects, values at certain positions for - /// sequences, etc. + /// Return all functions application relevant to an element. These can be: + /// 1) destructor values of a datatype + /// 2) constant fields of an object + /// 3) function applications /// - public IEnumerable GetExpansion(DafnyModelState state, DafnyModelVariable var) { - HashSet result = new(); - if (var.Element.Kind != Model.ElementKind.Uninterpreted) { - return result; // primitive types can't have fields + private List GetDestructorFunctions(Model.Element element) { + var possibleTypeIdentifiers = GetIsResults(element); + if (fDtype.OptEval(element) != null) { + possibleTypeIdentifiers.Add(fDtype.OptEval(element)!); } - - if (datatypeValues.TryGetValue(var.Element, out var fnTuple)) { - // Elt is a datatype value - var destructors = GetDestructorFunctions(var.Element).OrderBy(f => f.Name).ToList(); - if (destructors.Count > fnTuple.Args.Length) { - // Try to filter out predicate functions - // (that follow a format very similar to that of destructor names) - destructors = destructors.Where(destructor => - fnTuple.Args.Any(arg => destructor.OptEval(var.Element) == arg)) - .ToList(); - } - if (destructors.Count == fnTuple.Args.Length) { - // we know all destructor names - foreach (var func in destructors) { - result.Add(DafnyModelVariableFactory.Get(state, Unbox(func.OptEval(var.Element)), - UnderscoreRemovalRegex.Replace(func.Name.Split(".").Last(), "_"), var)); - } - } else { - // we don't know destructor names, so we use indices instead - for (int i = 0; i < fnTuple.Args.Length; i++) { - result.Add(DafnyModelVariableFactory.Get(state, Unbox(fnTuple.Args[i]), - "[" + i + "]", var)); - } + var possiblyNullableTypes = possibleTypeIdentifiers + .Select(ReconstructType).OfType() + .Where(type => type.Name != UnknownType.Name); + var types = possiblyNullableTypes.Select(DafnyModelTypeUtils.GetNonNullable).OfType().ToList(); + List result = new(); + var builtInDatatypeDestructor = new Regex("^.*[^_](__)*_q$"); + var canCallFunctions = new HashSet(); + foreach (var app in element.References) { + if (app.Func.Arity != 1 || !Equals(app.Args[0], element) || + !types.Any(type => app.Func.Name.StartsWith(type.Name + ".")) || + builtInDatatypeDestructor.IsMatch(app.Func.Name.Split(".").Last()) || + app.Func.Name.Split(".").Last().StartsWith("_")) { + continue; } - return result; - } - switch (var.Type) { - case SeqType: { - var seqLen = fSeqLength.OptEval(var.Element); - if (seqLen != null) { - var length = DafnyModelVariableFactory.Get(state, seqLen, "Length", var); - result.Add(length); - (var as SeqVariable)?.SetLength(length); - } - - // Sequences can be constructed with the build operator: - List elements = new(); - - var substring = var.Element; - while (fSeqBuild.AppWithResult(substring) != null) { - elements.Insert(0, Unbox(fSeqBuild.AppWithResult(substring).Args[1])); - substring = fSeqBuild.AppWithResult(substring).Args[0]; - } - for (int i = 0; i < elements.Count; i++) { - var e = DafnyModelVariableFactory.Get(state, Unbox(elements[i]), "[" + i + "]", var); - result.Add(e); - (var as SeqVariable)?.AddAtIndex(e, i.ToString()); - } - if (elements.Count > 0) { - return result; - } - - // Otherwise, sequences can be reconstructed index by index, ensuring indices are in ascending order. - // NB: per https://github.com/dafny-lang/dafny/issues/3048 , not all indices may be parsed as a BigInteger, - // so ensure we do not try to sort those numerically. - var intIndices = new List<(Model.Element, BigInteger)>(); - var otherIndices = new List<(Model.Element, String)>(); - foreach (var tpl in fSeqIndex.AppsWithArg(0, var.Element)) { - var asString = tpl.Args[1].ToString(); - if (BigInteger.TryParse(asString, out var bi)) { - intIndices.Add((Unbox(tpl.Result), bi)); - } else { - otherIndices.Add((Unbox(tpl.Result), asString)); - } - } - - var sortedIndices = intIndices - .OrderBy(p => p.Item2) - .Select(p => (p.Item1, p.Item2.ToString())) - .Concat(otherIndices); - - foreach (var (res, idx) in sortedIndices) { - var e = DafnyModelVariableFactory.Get(state, res, "[" + idx + "]", var); - result.Add(e); - (var as SeqVariable)?.AddAtIndex(e, idx); - } - - return result; - } - case SetType: { - foreach (var tpl in fSetSelect.AppsWithArg(0, var.Element)) { - var setElement = tpl.Args[1]; - var containment = tpl.Result; - if (containment.Kind != Model.ElementKind.Boolean) { - continue; - } - - result.Add(DafnyModelVariableFactory.Get(state, Unbox(setElement), - ((Model.Boolean)containment).ToString(), var)); - } - return result; - } - case MapType: { - var mapKeysAdded = new HashSet(); // prevents mapping a key to multiple values - var mapsElementsVisited = new HashSet(); // prevents infinite recursion - var current = var.Element; - var mapBuilds = fMapBuild.AppsWithResult(var.Element).ToList(); - while (mapBuilds.Count != 0) { - foreach (var mapBuild in mapBuilds.Where(m => m.Args[0] == current && !mapKeysAdded.Contains(m.Args[1]))) { - result.UnionWith(AddMappingHelper( - state, - var as MapVariable, - Unbox(mapBuild.Args[1]), - Unbox(mapBuild.Args[2]), - mapKeysAdded)); - } - mapsElementsVisited.Add(current); - var nextMapBuild = mapBuilds.FirstOrDefault(m => !mapsElementsVisited.Contains(m.Args[0])); - if (nextMapBuild == null) { - break; - } - current = nextMapBuild.Args[0]; - mapBuilds = fMapBuild.AppsWithResult(nextMapBuild.Args[0]).Where(m => !mapsElementsVisited.Contains(m.Args[0])).ToList(); - if (mapKeysAdded.Contains(nextMapBuild.Args[1])) { - continue; - } - result.UnionWith(AddMappingHelper( - state, - var as MapVariable, - Unbox(nextMapBuild.Args[1]), - Unbox(nextMapBuild.Args[2]), - mapKeysAdded)); - } - var mapDomain = fMapDomain.OptEval(current); - var mapElements = fMapElements.OptEval(current); - if (mapDomain == null || mapElements == null) { - return result; - } - foreach (var app in fSetSelect.AppsWithArg(0, mapDomain)) { - if (!((Model.Boolean)app.Result).Value) { - continue; - } - result.UnionWith(AddMappingHelper( - state, - var as MapVariable, - Unbox(app.Args[1]), - Unbox(fSetSelect.OptEval(mapElements, app.Args[1])), - mapKeysAdded)); - } - return result; - } - } - - // Elt is an array or an object: - var heap = state.State.TryGet("$Heap"); - if (heap == null) { - return result; - } - var constantFields = GetDestructorFunctions(var.Element).OrderBy(f => f.Name).ToList(); - foreach (var field in constantFields) { - result.Add(DafnyModelVariableFactory.Get(state, Unbox(field.OptEval(var.Element)), - UnderscoreRemovalRegex.Replace(field.Name.Split(".").Last(), "_"), var)); - } - var fields = fSetSelect.AppsWithArgs(0, heap, 1, var.Element); - if (fields == null || !fields.Any()) { - return result; - } - foreach (var tpl in fSetSelect.AppsWithArg(0, fields.ToList()[0].Result)) { - foreach (var fieldName in GetFieldNames(tpl.Args[1])) { - if (fieldName != "alloc") { - result.Add(DafnyModelVariableFactory.Get(state, Unbox(tpl.Result), fieldName, var)); - } + if (app.Func.Name.EndsWith("#canCall")) { + canCallFunctions.Add(app.Func.Name); + } else { + result.Add(app.Func); } } - return result; + return result.Where(func => canCallFunctions.All(canCall => !canCall.StartsWith(func.Name))).ToList(); } /// - /// Return all functions mapping an object to a destructor value. + /// Return all function applications relevant to an element. /// - private List GetDestructorFunctions(Model.Element element) { + private List GetFunctionConstants(Model.Element element, Model.Element? heap) { var possibleTypeIdentifiers = GetIsResults(element); if (fDtype.OptEval(element) != null) { - possibleTypeIdentifiers.Add(fDtype.OptEval(element)); + possibleTypeIdentifiers.Add(fDtype.OptEval(element)!); } var possiblyNullableTypes = possibleTypeIdentifiers - .Select(isResult => ReconstructType(isResult) as UserDefinedType) - .Where(type => type != null && type.Name != UnknownType.Name); - var types = possiblyNullableTypes.Select(type => DafnyModelTypeUtils.GetNonNullable(type) as UserDefinedType); - List result = new(); - var builtInDatatypeDestructor = new Regex("^.*[^_](__)*_q$"); + .Select(ReconstructType).OfType() + .Where(type => type.Name != UnknownType.Name); + var types = possiblyNullableTypes.Select(DafnyModelTypeUtils.GetNonNullable).OfType().ToList(); + List applications = new(); + List wellFormed = new(); foreach (var app in element.References) { - if (app.Func.Arity != 1 || app.Args[0] != element || + if (app.Args.Length == 0 || (!Equals(app.Args[0], element) && (heap == null || !Equals(app.Args[0], heap) || app.Args.Length == 1 || !Equals(app.Args[1], element))) || !types.Any(type => app.Func.Name.StartsWith(type.Name + ".")) || - builtInDatatypeDestructor.IsMatch(app.Func.Name.Split(".").Last())) { + app.Func.Name.Split(".").Last().StartsWith("_")) { continue; } - result.Add(app.Func); + + if (app.Func.Name.EndsWith("#canCall")) { + if (app.Result is Model.Boolean { Value: true }) { + wellFormed.Add(app); + } + } else { + applications.Add(app); + } } - return result; - } - private const string PleaseEnableModelCompressFalse = - "Please enable /proverOpt:O:model_compress=false (for z3 version < 4.8.7)" + - " or /proverOpt:O:model.compact=false (for z3 version >= 4.8.7)," + - " otherwise you'll get unexpected values."; + return applications.Where(application => + wellFormed.Any(wellFormedTuple => wellFormedTuple.Func.Name == application.Func.Name + "#canCall" && + ((wellFormedTuple.Args.Length == application.Args.Length && + wellFormedTuple.Args.SequenceEqual(application.Args)) || + (wellFormedTuple.Args.Length == application.Args.Length - 1 && + wellFormedTuple.Args.SequenceEqual(application.Args[1..])))) + ).ToList(); + } /// /// Return the name of the field represented by the given element. /// Special care is required if the element represents an array index /// - private List GetFieldNames(Model.Element elt) { + private List GetFieldNames(Model.Element? elt) { if (elt == null) { return new List(); } @@ -807,20 +909,18 @@ private List GetFieldNames(Model.Element elt) { .ToList(); } // Reaching this code means elt is an index into an array - var indices = new Model.Element[(int)dims]; + var indices = new Model.Element?[(int)dims]; for (int i = (int)dims; 0 <= --i;) { - ModelFuncWrapper.ModelFuncTupleWrapper dimTuple; + ModelFuncWrapper.ModelFuncTupleWrapper? dimTuple; if (i == 0) { dimTuple = fIndexField.AppWithResult(elt); if (dimTuple == null) { - options.OutputWriter.WriteLine(PleaseEnableModelCompressFalse); continue; } indices[i] = dimTuple.Args[0]; } else { dimTuple = fMultiIndexField.AppWithResult(elt); if (dimTuple == null) { - options.OutputWriter.WriteLine(PleaseEnableModelCompressFalse); continue; } indices[i] = dimTuple.Args[1]; @@ -834,16 +934,18 @@ private List GetFieldNames(Model.Element elt) { } /// Unboxes an element, if possible - private Model.Element Unbox(Model.Element elt) { - if (elt == null) { - return null; - } + private Model.Element? Unbox(Model.Element? elt) { + return elt == null ? null : UnboxNotNull(elt); + } + + /// Unboxes an element, if possible + private Model.Element UnboxNotNull(Model.Element elt) { var unboxed = fBox.AppWithResult(elt); if (unboxed != null) { - return Unbox(unboxed.Args[0]); + return UnboxNotNull(unboxed.Args[0]); } unboxed = fUnbox.AppWithArg(1, elt); - return unboxed != null ? Unbox(unboxed.Result) : elt; + return unboxed != null ? UnboxNotNull(unboxed.Result) : elt; } } } diff --git a/Source/DafnyCore/CounterExampleGeneration/DafnyModelState.cs b/Source/DafnyCore/CounterExampleGeneration/DafnyModelState.cs deleted file mode 100644 index 6d2a6cb3fd4..00000000000 --- a/Source/DafnyCore/CounterExampleGeneration/DafnyModelState.cs +++ /dev/null @@ -1,236 +0,0 @@ -// Copyright by the contributors to the Dafny Project -// SPDX-License-Identifier: MIT - - -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text.RegularExpressions; -using Microsoft.Boogie; - -namespace Microsoft.Dafny { - - /// - /// Represents a program state in a DafnyModel - /// - public class DafnyModelState { - - internal readonly DafnyModel Model; - internal readonly Model.CapturedState State; - internal int VarIndex; // used to assign unique indices to variables - private readonly List vars; - private readonly List boundVars; - // varMap prevents the creation of multiple variables for the same element. - private readonly Dictionary varMap; - // varNameCount keeps track of the number of variables with the same name. - // Name collision can happen in the presence of an old expression, - // for instance, in which case the it is important to distinguish between - // two variables that have the same name using an index provided by Boogie - private readonly Dictionary varNameCount; - - private const string InitialStateName = ""; - private static readonly Regex StatePositionRegex = new( - @".*\((?\d+),(?\d+)\)", - RegexOptions.IgnoreCase | RegexOptions.Singleline - ); - - internal DafnyModelState(DafnyModel model, Model.CapturedState state) { - Model = model; - State = state; - VarIndex = 0; - vars = new(); - varMap = new(); - varNameCount = new(); - boundVars = new(BoundVars()); - SetupVars(); - } - - /// - /// Start with the union of vars and boundVars and expand the set by adding - /// variables that represent fields of any object in the original set or - /// elements of any sequence in the original set, etc. This is done - /// recursively in breadth-first order and only up to a certain maximum - /// depth. - /// - /// The maximum depth up to which to expand the - /// variable set. - /// Set of variables - public List ExpandedVariableSet(int maxDepth) { - List expandedSet = new(); - // The following is the queue for elements to be added to the set. The 2nd - // element of a tuple is the depth of the variable w.r.t. the original set - List> varsToAdd = new(); - vars.ForEach(variable => varsToAdd.Add(new(variable, 0))); - boundVars.ForEach(variable => varsToAdd.Add(new(variable, 0))); - while (varsToAdd.Count != 0) { - var (next, depth) = varsToAdd[0]; - varsToAdd.RemoveAt(0); - if (expandedSet.Contains(next)) { - continue; - } - if (depth == maxDepth) { - break; - } - expandedSet.Add(next); - // fields of primitive types are skipped: - foreach (var v in next.GetExpansion(). - Where(variable => !expandedSet.Contains(variable) && !variable.IsPrimitive)) { - varsToAdd.Add(new(v, depth + 1)); - } - } - return expandedSet; - } - - internal bool ExistsVar(Model.Element element) { - return varMap.ContainsKey(element); - } - - internal void AddVar(Model.Element element, DafnyModelVariable var) { - if (!ExistsVar(element)) { - varMap[element] = var; - } - } - - internal DafnyModelVariable GetVar(Model.Element element) { - return varMap[element]; - } - - internal void AddVarName(string name) { - varNameCount[name] = varNameCount.GetValueOrDefault(name, 0) + 1; - } - - internal bool VarNameIsShared(string name) { - return varNameCount.GetValueOrDefault(name, 0) > 1; - } - - public string FullStateName => State.Name; - - private string ShortenedStateName => ShortenName(State.Name, 20); - - public bool IsInitialState => FullStateName.Equals(InitialStateName); - - public bool StateContainsPosition() { - return StatePositionRegex.Match(ShortenedStateName).Success; - } - - public int GetLineId() { - var match = StatePositionRegex.Match(ShortenedStateName); - if (!match.Success) { - throw new ArgumentException( - $"state does not contain position: {ShortenedStateName}"); - } - return int.Parse(match.Groups["line"].Value); - } - - public int GetCharId() { - var match = StatePositionRegex.Match(ShortenedStateName); - if (!match.Success) { - throw new ArgumentException( - $"state does not contain position: {ShortenedStateName}"); - } - return int.Parse(match.Groups["character"].Value); - } - - /// - /// Initialize the vars list, which stores all variables relevant to - /// the counterexample except for the bound variables - /// - private void SetupVars() { - var names = Enumerable.Empty(); - if (Model.States.Count > 0) { - var prev = Model.States.Last(); - names = prev.vars.ConvertAll(variable => variable.Name); - } - names = names.Concat(State.Variables).Distinct(); - foreach (var v in names) { - if (!DafnyModel.IsUserVariableName(v)) { - continue; - } - var val = State.TryGet(v); - if (val == null) { - continue; // This variable has no value in the model, so ignore it. - } - - var vn = DafnyModelVariableFactory.Get(this, val, v, duplicate: true); - vars.Add(vn); - } - } - - /// - /// Return list of bound variables - /// - private IEnumerable BoundVars() { - foreach (var f in Model.Model.Functions) { - if (f.Arity != 0) { - continue; - } - int n = f.Name.IndexOf('!'); - if (n == -1) { - continue; - } - var name = f.Name.Substring(0, n); - if (!name.Contains('#') || name.Contains("$")) { - continue; - } - - yield return DafnyModelVariableFactory.Get(this, f.GetConstant(), name, - null, true); - } - } - - private static string ShortenName(string name, int fnLimit) { - var loc = TryParseSourceLocation(name); - if (loc != null) { - var fn = loc.Filename; - int idx = fn.LastIndexOfAny(new[] { '\\', '/' }); - if (idx > 0) { - fn = fn.Substring(idx + 1); - } - if (fn.Length > fnLimit) { - fn = fn.Substring(0, fnLimit) + ".."; - } - var addInfo = loc.AddInfo; - if (addInfo != "") { - addInfo = ":" + addInfo; - } - return $"{fn}({loc.Line},{loc.Column}){addInfo}"; - } - return name; - } - - /// - /// Parse a string (typically the name of the captured state in Boogie) to - /// extract a SourceLocation from it. An example of a string to be parsed: - /// @"c:\users\foo\bar.c(12,10) : random string" - /// The ": random string" part is optional. - /// - private static SourceLocation TryParseSourceLocation(string name) { - int par = name.LastIndexOf('('); - if (par <= 0) { - return null; - } - var res = new SourceLocation() { Filename = name.Substring(0, par) }; - var words = name.Substring(par + 1) - .Split(',', ')', ':') - .Where(x => x != "") - .ToArray(); - if (words.Length < 2) { - return null; - } - if (!int.TryParse(words[0], out res.Line) || - !int.TryParse(words[1], out res.Column)) { - return null; - } - int colon = name.IndexOf(':', par); - res.AddInfo = colon > 0 ? name.Substring(colon + 1).Trim() : ""; - return res; - } - - private class SourceLocation { - public string Filename; - public string AddInfo; - public int Line; - public int Column; - } - } -} \ No newline at end of file diff --git a/Source/DafnyCore/CounterExampleGeneration/DafnyModelTypeUtils.cs b/Source/DafnyCore/CounterExampleGeneration/DafnyModelTypeUtils.cs index 7e17ad24ef1..b6ff5486a6b 100644 --- a/Source/DafnyCore/CounterExampleGeneration/DafnyModelTypeUtils.cs +++ b/Source/DafnyCore/CounterExampleGeneration/DafnyModelTypeUtils.cs @@ -1,5 +1,6 @@ // Copyright by the contributors to the Dafny Project // SPDX-License-Identifier: MIT +#nullable enable using System; using System.Linq; @@ -28,7 +29,9 @@ public static Type GetNonNullable(Type type) { } public static Type ReplaceTypeVariables(Type type, Type with) { - return ReplaceType(type, t => t.Name.Contains('$'), _ => with); + var result = ReplaceType(type, t => t.Name.Contains('$'), _ => with); + FillInTypeArgs(result, with); + return result; } /// @@ -61,6 +64,8 @@ public static Type GetInDafnyFormat(Type type) { // The code below converts every "__" to "_": newName = UnderscoreRemovalRegex.Replace(newName, "_"); newName = ConvertTupleName(newName); + newName = string.Join(".", newName.Split(".") + .Where(part => part != "_module" && part != "_default" && part != "_System")); return new UserDefinedType(new Token(), newName, type.TypeArgs.ConvertAll(t => TransformType(t, GetInDafnyFormat))); } @@ -82,15 +87,15 @@ private static Type TransformType(Type type, Func transfo switch (type) { case BasicType: return type; - case MapType mapType: + case MapType mapType when mapType.HasTypeArg(): return new MapType(mapType.Finite, TransformType(mapType.Domain, transform), TransformType(mapType.Range, transform)); - case SeqType seqType: + case SeqType seqType when seqType.HasTypeArg(): return new SeqType(TransformType(seqType.Arg, transform)); - case SetType setType: + case SetType setType when setType.HasTypeArg(): return new SetType(setType.Finite, TransformType(setType.Arg, transform)); - case MultiSetType multiSetType: + case MultiSetType multiSetType when multiSetType.HasTypeArg(): return new MultiSetType(TransformType(multiSetType, transform)); case UserDefinedType userDefinedType: return transform(userDefinedType); @@ -101,5 +106,33 @@ private static Type TransformType(Type type, Func transfo } return type; } + + /// + /// Whenever a collection type does not have an argument, fill it in with the provided arg type + /// + private static void FillInTypeArgs(Type type, Type arg) { + switch (type) { + case BasicType: + return; + case MapType mapType when !mapType.HasTypeArg(): + mapType.SetTypeArgs(arg, arg); + return; + case SeqType seqType when !seqType.HasTypeArg(): + seqType.SetTypeArg(arg); + return; + case SetType setType when !setType.HasTypeArg(): + setType.SetTypeArg(arg); + return; + case MultiSetType multiSetType when !multiSetType.HasTypeArg(): + multiSetType.SetTypeArg(arg); + return; + case UserDefinedType userDefinedType: + userDefinedType.TypeArgs.ForEach(typ => FillInTypeArgs(typ, arg)); + return; + case InferredTypeProxy inferredTypeProxy: + FillInTypeArgs(inferredTypeProxy.T, arg); + return; + } + } } } \ No newline at end of file diff --git a/Source/DafnyCore/CounterExampleGeneration/DafnyModelVariable.cs b/Source/DafnyCore/CounterExampleGeneration/DafnyModelVariable.cs deleted file mode 100644 index 855b59e5ab1..00000000000 --- a/Source/DafnyCore/CounterExampleGeneration/DafnyModelVariable.cs +++ /dev/null @@ -1,299 +0,0 @@ -// Copyright by the contributors to the Dafny Project -// SPDX-License-Identifier: MIT - -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text.RegularExpressions; -using Microsoft.Boogie; - -namespace Microsoft.Dafny { - - /// - /// A static class for generating instance of DafnyModelvariable and its - /// subclasses. The factory chooses which subclass of DafnyModelVariable to - /// employ depending on the DafnyModelType` of the `Element` for which the - /// variable is generated. - /// - public static class DafnyModelVariableFactory { - - /// - /// Create a new variable to be associated with the given model element in - /// a given counterexample state or return such a variable if one already - /// exists. - /// - /// - /// - /// the name to be assigned to the variable OR, - /// if parent != null, the name of the field associated with it. In the later - /// case, Name is set to some unique id. - /// if not null, this variable represents the field of - /// some parent object - /// forces the creation of a new variable even if - /// one already exists - /// - public static DafnyModelVariable Get(DafnyModelState state, - Model.Element element, string name, DafnyModelVariable parent = null, - bool duplicate = false) { - if (state.ExistsVar(element)) { - parent?.AddChild(name, state.GetVar(element)); - if (!duplicate) { - return state.GetVar(element); - } - return new DuplicateVariable(state, state.GetVar(element), name, parent); - } - - return state.Model.GetDafnyType(element) switch { - SeqType _ => new SeqVariable(state, element, name, parent), - MapType _ => new MapVariable(state, element, name, parent), - _ => new DafnyModelVariable(state, element, name, parent) - }; - } - } - - /// - /// Represents a variable at a particular state. Note that a variable in Dafny - /// source can be represented by multiple DafnyModelVariables, one for each - /// DafnyModelState in DafnyModel. - /// - public class DafnyModelVariable { - - public readonly string Name; // name given to the variable at creation - public readonly Microsoft.Dafny.Type Type; // Dafny type of the variable - public readonly Model.Element Element; - // Maps a field name, sequence index, or some other identifier to - // a list of DafnyModelVariables that represent the corresponding value - private readonly Dictionary> children; - private readonly DafnyModelState state; // the associated captured state - public virtual Dictionary> Children => children; - - internal DafnyModelVariable(DafnyModelState state, Model.Element element, - string name, DafnyModelVariable parent) { - this.state = state; - Element = element; - Type = state.Model.GetDafnyType(element); - children = new Dictionary>(); - state.AddVar(element, this); - if (parent == null) { - Name = name; - } else { - Name = "@" + state.VarIndex++; - parent.AddChild(name, this); - } - state.AddVarName(ShortName); - } - - public virtual IEnumerable GetExpansion() { - return state.Model.GetExpansion(state, this); - } - - public string CanonicalName() { - return state.Model.CanonicalName(Element, Type); - } - - public virtual string Value { - get { - var result = state.Model.CanonicalName(Element, Type); - if (children.Count == 0) { - if (result != "") { - return result; - } - return Type is SetType ? "{}" : "()"; - } - - List<(string ChildName, string ChildValue)> childList = new(); - foreach (var childName in children.Keys) { - foreach (var child in children[childName]) { - if (child.IsPrimitive) { - childList.Add(new ValueTuple(childName, child.Value)); - } else { - childList.Add(new ValueTuple(childName, child.ShortName)); - } - } - } - string childValues; - if (Type is SetType) { - childValues = string.Join(", ", - childList.ConvertAll(tpl => tpl.Item2 + " := " + tpl.Item1)); - return result + "{" + childValues + "}"; - } - childValues = string.Join(", ", - childList.ConvertAll(tpl => tpl.Item1 + " := " + tpl.Item2)); - return result + "(" + childValues + ")"; - } - } - public bool IsPrimitive => Type is BasicType || state.Model.ElementIsNull(Element); - - public string ShortName { - get { - var shortName = Regex.Replace(Name, @"#.*$", ""); - return state.VarNameIsShared(shortName) ? Name : shortName; - } - } - - internal void AddChild(string name, DafnyModelVariable child) { - name = Regex.Replace(name, "^_h", "#"); - if (!children.ContainsKey(name)) { - children[name] = new(); - } - children[name].Add(child); - } - - public override int GetHashCode() { - return Element.Id.GetHashCode(); - } - - public override bool Equals(object obj) { - if (obj is not DafnyModelVariable other) { - return false; - } - - return other.Element == Element && - other.state == state && - other.Name == Name; - } - } - - /// - /// a variable that has a different name but represents the same Element in - /// the same DafnyModelState as some other variable. - /// - public class DuplicateVariable : DafnyModelVariable { - - public readonly DafnyModelVariable Original; - - internal DuplicateVariable(DafnyModelState state, - DafnyModelVariable original, string newName, DafnyModelVariable parent) - : base(state, original.Element, newName, parent) { - Original = original; - } - - public override string Value => Original.ShortName; - - public override Dictionary> Children => Original.Children; - - public override IEnumerable GetExpansion() { - return Original.GetExpansion(); - } - } - - /// - /// A variable that represents a sequence. - /// - public class SeqVariable : DafnyModelVariable { - - private DafnyModelVariable seqLength; - // Dafny integers are unbounded, hence using strings for seq indices: - private readonly Dictionary seqElements; - - internal SeqVariable(DafnyModelState state, Model.Element element, - string name, DafnyModelVariable parent) - : base(state, element, name, parent) { - seqLength = null; - seqElements = new Dictionary(); - } - - public override string Value { - get { - var length = GetLength(); - if (length == -1 || seqElements.Count != length) { - return base.Value; - } - List result = new(); - for (int i = 0; i < length; i++) { - var id = i.ToString(); - if (!seqElements.ContainsKey(id)) { - return base.Value; - } - result.Add(seqElements[id].IsPrimitive ? - seqElements[id].Value : - seqElements[id].ShortName); - } - return "[" + string.Join(", ", result) + "]"; - } - } - - public int GetLength() { - if (int.TryParse((seqLength?.Element as Model.Integer)?.Numeral, - out var value)) { - return value; - } - // Since the length is not explicitly specified, the index of the last known element should suffice - int lastId = 0; - foreach (var id in seqElements.Keys) { - if (int.TryParse(id, out var idAsInt)) { - if (lastId < idAsInt + 1) { - lastId = idAsInt + 1; - } - } else { - return -1; // Failed to parse the index, so just say that the length is unknown - } - } - return lastId; - } - - public DafnyModelVariable this[int index] => seqElements.GetValueOrDefault(index.ToString(), null); - - public void SetLength(DafnyModelVariable seqLength) { - this.seqLength = seqLength; - } - - public void AddAtIndex(DafnyModelVariable e, string index) { - if (index == null) { - return; - } - seqElements[index] = e; - } - } - - /// - /// A variable that represents a map. - /// - public class MapVariable : DafnyModelVariable { - - public readonly Dictionary - Mappings = new(); - - internal MapVariable(DafnyModelState state, Model.Element element, - string name, DafnyModelVariable parent) - : base(state, element, name, parent) { } - - public override string Value { - get { - if (Mappings.Count == 0) { - return "map[]"; - } - // maps a key-value pair to how many times it appears in the map - // a key value pair can appear many times in a map due to "?:int" etc. - Dictionary mapStrings = new(); - foreach (var key in Mappings.Keys) { - var keyString = key.IsPrimitive ? key.Value : key.Name; - var valueString = "?"; - if (Mappings[key] != null) { - valueString = Mappings[key].IsPrimitive - ? Mappings[key].Value - : Mappings[key].Name; - } - var mapString = keyString + " := " + valueString; - mapStrings[mapString] = - mapStrings.GetValueOrDefault(mapString, 0) + 1; - } - - return "map[" + string.Join(", ", mapStrings.Keys.ToList() - .ConvertAll(keyValuePair => - mapStrings[keyValuePair] == 1 - ? keyValuePair - : keyValuePair + " [+" + (mapStrings[keyValuePair] - 1) + - "]")) + - "]"; - } - } - - public void AddMapping(DafnyModelVariable from, DafnyModelVariable to) { - if (Mappings.ContainsKey(from)) { - return; - } - Mappings[from] = to; - } - } -} \ No newline at end of file diff --git a/Source/DafnyCore/CounterExampleGeneration/ModelFuncWrapper.cs b/Source/DafnyCore/CounterExampleGeneration/ModelFuncWrapper.cs index 96334b6bc83..5970115bc65 100644 --- a/Source/DafnyCore/CounterExampleGeneration/ModelFuncWrapper.cs +++ b/Source/DafnyCore/CounterExampleGeneration/ModelFuncWrapper.cs @@ -1,5 +1,6 @@ // Copyright by the contributors to the Dafny Project // SPDX-License-Identifier: MIT +#nullable enable using System; using System.Collections.Generic; @@ -28,25 +29,30 @@ public ModelFuncWrapper(DafnyModel model, string name, int arity, int argsToSkip func = model.Model.MkFunc(name, arity + this.argsToSkip); } - private ModelFuncTupleWrapper ConvertFuncTuple(Model.FuncTuple tuple) { - return tuple == null ? null : new ModelFuncTupleWrapper(func, tuple.Result, tuple.Args[argsToSkip..]); + public ModelFuncWrapper(Model.Func func, int argsToSkip) { + this.func = func; + this.argsToSkip = argsToSkip; + } + + private ModelFuncTupleWrapper? ConvertFuncTuple(Model.FuncTuple? tuple) { + return tuple == null ? null : new ModelFuncTupleWrapper(tuple.Result, tuple.Args[argsToSkip..]); } - public ModelFuncTupleWrapper AppWithResult(Model.Element element) { + public ModelFuncTupleWrapper? AppWithResult(Model.Element element) { return ConvertFuncTuple(func.AppWithResult(element)); } public IEnumerable AppsWithResult(Model.Element element) { - return func.AppsWithResult(element).Select(ConvertFuncTuple); + return func.AppsWithResult(element).Select(ConvertFuncTuple).OfType(); } - public IEnumerable Apps => func.Apps.Select(ConvertFuncTuple); + public IEnumerable Apps => func.Apps.Select(ConvertFuncTuple).OfType(); - public Model.Element GetConstant() { + public Model.Element? GetConstant() { return func.GetConstant(); } - public Model.Element OptEval(Model.Element element) { + public Model.Element? OptEval(Model.Element? element) { if (element == null) { return null; } @@ -54,11 +60,11 @@ public Model.Element OptEval(Model.Element element) { return app?.Result; } - public ModelFuncTupleWrapper AppWithArg(int index, Model.Element element) { + public ModelFuncTupleWrapper? AppWithArg(int index, Model.Element element) { return ConvertFuncTuple(func.AppWithArg(argsToSkip + index, element)); } - public Model.Element OptEval(Model.Element first, Model.Element second) { + public Model.Element? OptEval(Model.Element? first, Model.Element? second) { if (first == null || second == null) { return null; } @@ -67,11 +73,11 @@ public Model.Element OptEval(Model.Element first, Model.Element second) { } public IEnumerable AppsWithArg(int i, Model.Element element) { - return func.AppsWithArg(i + argsToSkip, element).Select(ConvertFuncTuple); + return func.AppsWithArg(i + argsToSkip, element).Select(ConvertFuncTuple).OfType(); } public IEnumerable AppsWithArgs(int i0, Model.Element element0, int i1, Model.Element element1) { - return func.AppsWithArgs(i0 + argsToSkip, element0, i1 + argsToSkip, element1).Select(ConvertFuncTuple); + return func.AppsWithArgs(i0 + argsToSkip, element0, i1 + argsToSkip, element1).Select(ConvertFuncTuple).OfType(); } /// @@ -107,13 +113,11 @@ public class ModelFuncTupleWrapper { static readonly Model.Element[] EmptyArgs = Array.Empty(); - public readonly Model.Func Func; - public Model.Element Result; + public readonly Model.Element Result; public readonly Model.Element[] Args; - public ModelFuncTupleWrapper(Model.Func func, Model.Element res, Model.Element[] args) { + public ModelFuncTupleWrapper(Model.Element res, Model.Element[] args) { Args = args ?? EmptyArgs; - Func = func; Result = res; } } diff --git a/Source/DafnyCore/CounterExampleGeneration/PartialState.cs b/Source/DafnyCore/CounterExampleGeneration/PartialState.cs new file mode 100644 index 00000000000..0704d02578c --- /dev/null +++ b/Source/DafnyCore/CounterExampleGeneration/PartialState.cs @@ -0,0 +1,324 @@ +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +#nullable enable + +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text.RegularExpressions; +using Microsoft.Boogie; + +namespace Microsoft.Dafny; + +public class PartialState { + + public bool IsLoopEntryState => FullStateName.Contains(CaptureStateExtensions.AfterLoopIterationsStateMarker); + // ghost variables introduced by the counterexample whose values must be true for the counterexample to hold: + public List LoopGuards = new(); + public readonly Dictionary> KnownVariableNames = new(); + private readonly List initialPartialValues; + internal readonly DafnyModel Model; + internal readonly Model.CapturedState State; + private const string InitialStateName = ""; + private static readonly Regex StatePositionRegex = new( + @".*\((?\d+),(?\d+)\)", + RegexOptions.IgnoreCase | RegexOptions.Singleline + ); + internal readonly Dictionary AllPartialValues = new(); + + private const string BoundVarPrefix = "boundVar"; + + internal PartialState(DafnyModel model, Model.CapturedState state) { + Model = model; + State = state; + initialPartialValues = new List(); + SetupBoundVars(); + SetupVars(); + } + + /// + /// Start with the union of vars and boundVars and expand the set by adding + /// all partial values that are necessary to fully constrain the counterexample. + /// + /// Set of partial values + public HashSet ExpandedVariableSet() { + HashSet expandedSet = new(); + // The following is the queue for elements to be added to the set. The 2nd + // element of a tuple is the depth of the variable w.r.t. the original set + List> varsToAdd = new(); + initialPartialValues.ForEach(variable => varsToAdd.Add(new(variable, 0))); + while (varsToAdd.Count != 0) { + var (next, depth) = varsToAdd[0]; + varsToAdd.RemoveAt(0); + if (expandedSet.Contains(next)) { + continue; + } + expandedSet.Add(next); + // fields of primitive types are skipped: + foreach (var v in next.GetRelatedValues(). + Where(variable => !expandedSet.Contains(variable))) { + varsToAdd.Add(new(v, depth + 1)); + } + } + return expandedSet; + } + + /// + /// Return a conjunction of expression that is represented by a balanced AST. This is intended to prevent + /// stackoverflow errors that occur if multiple conjuncts are joined in a linked list fashion. + /// + /// + private Expression GetCompactConjunction(List conjuncts) { + if (!conjuncts.Any()) { + return new LiteralExpr(Token.NoToken, true); + } + + if (conjuncts.Count() == 1) { + return conjuncts.First(); + } + + var middle = conjuncts.Count() / 2; + var left = GetCompactConjunction(conjuncts.Take(middle).ToList()); + var right = GetCompactConjunction(conjuncts.Skip(middle).ToList()); + return new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, left, right); + } + + /// + /// Convert this counterexample state into an assumption that could be inserted in Dafny source code + /// + public Statement AsAssumption() { + var allVariableNames = new Dictionary(); + var variables = ExpandedVariableSet().ToArray(); + var constraintSet = new HashSet(); + + // Collect all constraints into one list: + foreach (var variable in variables) { + foreach (var constraint in variable.Constraints) { + constraintSet.Add(constraint); + } + } + + // Ignore TypeTest constraints because they make the counterexample too verbose + var constraints = constraintSet.Where(constraint => constraint is not TypeTestConstraint).ToList(); + constraints = Constraint.ResolveAndOrder(allVariableNames, constraints, true, true); + + // Create a bound variable for every partial value that we cannot otherwise refer to using variables in scope + var boundVars = new List(); + for (int i = 0; i < variables.Length; i++) { + if (!allVariableNames.ContainsKey(variables[i])) { + boundVars.Add(new BoundVar(Token.NoToken, BoundVarPrefix + boundVars.Count, variables[i].Type)); + allVariableNames[variables[i]] = new IdentifierExpr(Token.NoToken, boundVars.Last()); + } + } + + // Translate all constraints to Dafny expressions, removing any duplicates: + var constraintsAsExpressions = new List(); + var constraintsAsStrings = new HashSet(); + foreach (var constraint in constraints) { + var constraintAsExpression = constraint.AsExpression(allVariableNames); + if (constraintAsExpression == null) { + continue; + } + var constraintAsString = constraintAsExpression.ToString(); + if (constraintsAsStrings.Contains(constraintAsString)) { + continue; + } + + constraintsAsStrings.Add(constraintAsString); + constraintsAsExpressions.Add(constraintAsExpression); + } + + // Convert the constraints into one conjunction + Expression expression = GetCompactConjunction(constraintsAsExpressions); + + if (constraintsAsExpressions.Count > 0 && boundVars.Count > 0) { + expression = new ExistsExpr(Token.NoToken, RangeToken.NoToken, boundVars, null, expression, null); + } + + if ((LoopGuards.Count != 0 && !IsLoopEntryState) || LoopGuards.Count > 1) { + Expression loopGuard = new IdentifierExpr(Token.NoToken, LoopGuards[0]); + for (int i = 1; i < LoopGuards.Count; i++) { + if (i == LoopGuards.Count - 1 && IsLoopEntryState) { + continue; + } + loopGuard = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, loopGuard, + new IdentifierExpr(Token.NoToken, LoopGuards[i])); + } + expression = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Imp, loopGuard, expression); + } + + if (!IsLoopEntryState) { + return new AssumeStmt(RangeToken.NoToken, expression, null); + } + return new UpdateStmt(RangeToken.NoToken, new List() { new IdentifierExpr(Token.NoToken, LoopGuards.Last()) }, + new List() { new ExprRhs(expression) }); + } + + /// + /// Initialize the vars list, which stores all variables relevant to + /// the counterexample except for the bound variables + /// + private void SetupVars() { + var names = Enumerable.Empty(); + foreach (var partialState in Model.States) { + names = names.Concat(partialState.State.Variables); + } + names = names.Concat(State.Variables).Distinct().ToList(); + var notDefinitelyAssigned = new HashSet(); + foreach (var name in names.Where(name => name.StartsWith("defass#"))) { + var val = State.TryGet(name); + if (val == null) { + continue; + } + if (val is Model.Boolean { Value: false }) { + notDefinitelyAssigned.Add(name[7..]); + } + } + foreach (var v in names) { + if (!IsUserVariableName(v) || notDefinitelyAssigned.Contains(v)) { + continue; + } + var val = State.TryGet(v); + if (val == null) { + continue; // This variable has no value in the model, so ignore it. + } + + var value = PartialValue.Get(val, this); + initialPartialValues.Add(value); + var _ = new IdentifierExprConstraint(value, v.Split("#").First()); + if (!KnownVariableNames.ContainsKey(value)) { + KnownVariableNames[value] = new List(); + } + KnownVariableNames[value].Add(v.Split("#").First()); + } + } + + /// + /// Return True iff the variable name is referring to a variable that has + /// a direct analog in Dafny source (i.e. not $Heap, $_Frame, $nw, etc.) + /// + private static bool IsUserVariableName(string name) => + !name.Contains("$") && name.Count(c => c == '#') <= 1; + + /// + /// Instantiate BoundVariables + /// + private void SetupBoundVars() { + foreach (var f in Model.Model.Functions) { + if (f.Arity != 0) { + continue; + } + int n = f.Name.IndexOf('!'); + if (n == -1) { + continue; + } + var name = f.Name[..n]; + if (!name.Contains('#') || name.Contains('$')) { + continue; + } + + var value = PartialValue.Get(f.GetConstant(), this); + initialPartialValues.Add(value); + var _ = new IdentifierExprConstraint(value, name); + if (!KnownVariableNames.ContainsKey(value)) { + KnownVariableNames[value] = new(); + } + KnownVariableNames[value].Add(name); + } + } + + public string FullStateName => State.Name; + + private string ShortenedStateName => ShortenName(State.Name, 20); + + public bool IsInitialState => FullStateName.Equals(InitialStateName); + + public bool StateContainsPosition() { + return StatePositionRegex.Match(ShortenedStateName).Success; + } + + public int GetLineId() { + var match = StatePositionRegex.Match(ShortenedStateName); + if (!match.Success) { + throw new ArgumentException( + $"state does not contain position: {ShortenedStateName}"); + } + return int.Parse(match.Groups["line"].Value); + } + + public int GetCharId() { + var match = StatePositionRegex.Match(ShortenedStateName); + if (!match.Success) { + throw new ArgumentException( + $"state does not contain position: {ShortenedStateName}"); + } + return int.Parse(match.Groups["character"].Value); + } + + private static string ShortenName(string name, int fnLimit) { + var loc = TryParseSourceLocation(name); + if (loc != null) { + var fn = loc.Filename; + int idx = fn.LastIndexOfAny(new[] { '\\', '/' }); + if (idx > 0) { + fn = fn[(idx + 1)..]; + } + if (fn.Length > fnLimit) { + fn = fn[..fnLimit] + ".."; + } + var addInfo = loc.AddInfo; + if (addInfo != "") { + addInfo = ":" + addInfo; + } + return $"{fn}({loc.Line},{loc.Column}){addInfo}"; + } + return name; + } + + /// + /// Parse a string (typically the name of the captured state in Boogie) to + /// extract a SourceLocation from it. An example of a string to be parsed: + /// @"c:\users\foo\bar.c(12,10) : random string" + /// The ": random string" part is optional. + /// + private static SourceLocation? TryParseSourceLocation(string name) { + int par = name.LastIndexOf('('); + if (par <= 0) { + return null; + } + // var res = new SourceLocation { Filename = name[..par] }; + var words = name[(par + 1)..] + .Split(',', ')', ':') + .Where(x => x != "") + .ToArray(); + if (words.Length < 2) { + return null; + } + if (!int.TryParse(words[0], out var line) || + !int.TryParse(words[1], out var column)) { + return null; + } + int colon = name.IndexOf(':', par); + var res = new SourceLocation( + name[..par], + colon > 0 ? name[(colon + 1)..].Trim() : "", + line, + column); + return res; + } + + private class SourceLocation { + public readonly string Filename; + public readonly string AddInfo; + public readonly int Line; + public readonly int Column; + + public SourceLocation(string filename, string addInfo, int line, int column) { + Filename = filename; + AddInfo = addInfo; + Line = line; + Column = column; + } + } + +} \ No newline at end of file diff --git a/Source/DafnyCore/CounterExampleGeneration/PartialValue.cs b/Source/DafnyCore/CounterExampleGeneration/PartialValue.cs new file mode 100644 index 00000000000..c8125fbd65b --- /dev/null +++ b/Source/DafnyCore/CounterExampleGeneration/PartialValue.cs @@ -0,0 +1,180 @@ +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +#nullable enable + +using System.Collections.Generic; +using System.Linq; +using System.Numerics; +using Microsoft.Boogie; + +namespace Microsoft.Dafny; + +/// +/// Each PartialValue corresponds to an Element in the counterexample model returned by Boogie and represents a +/// Dafny value about which we might have limited information (e.g. a sequence of which we only know one element) +/// +public class PartialValue { + + public readonly Model.Element Element; // the element in the counterexample model associated with the value + public readonly List Constraints; // constraints describing this value + public readonly PartialState state; // corresponding state in the counterexample model + private readonly Type type; // Dafny type associated with the value + private bool haveExpanded; + + /// + /// This factory method ensures we don't create duplicate partial value objects for the same element and state in the + /// counterexample model + /// + public static PartialValue Get(Model.Element element, PartialState state) { + if (state.AllPartialValues.TryGetValue(element, out var value)) { + return value; + } + + return new PartialValue(element, state); + } + + private PartialValue(Model.Element element, PartialState state) { + Element = element; + this.state = state; + Constraints = new(); + haveExpanded = false; + state.AllPartialValues[element] = this; + type = state.Model.GetFormattedDafnyType(element); + var _ = new TypeTestConstraint(this, type); + state.Model.AddTypeConstraints(this); + } + + /// + /// Return all partial values that appear in any of the constraints describing this element + /// + public IEnumerable GetRelatedValues() { + var relatedValues = new HashSet() { this }; + if (!haveExpanded) { + state.Model.GetExpansion(state, this); + haveExpanded = true; + } + + foreach (var constraint in Constraints) { + foreach (var value in constraint.ReferencedValues) { + if (!relatedValues.Contains(value)) { + relatedValues.Add(value); + yield return value; + } + } + + if (constraint is DefinitionConstraint definitionConstraint && + !relatedValues.Contains(definitionConstraint.DefinedValue)) { + relatedValues.Add(definitionConstraint.DefinedValue); + yield return definitionConstraint.DefinedValue; + } + } + } + + public bool Nullable => Constraints.OfType() + .Any(test => test.Type is UserDefinedType userDefinedType && userDefinedType.Name.EndsWith("?")); + + public Type Type => type; + + public string PrimitiveLiteral { + get { + return Constraints.OfType() + .Select(literal => literal.LiteralExpr.ToString()).FirstOrDefault() ?? ""; + } + } + + public Dictionary Fields() { + var fields = new Dictionary(); + foreach (var memberSelectExpr in Constraints.OfType() + .Where(constraint => Equals(constraint.Obj, this))) { + fields[memberSelectExpr.MemberName] = memberSelectExpr.DefinedValue; + } + + return fields; + } + + public IEnumerable UnnamedDestructors() { + var datatypeValue = Constraints.OfType() + .FirstOrDefault(constraint => Equals(constraint.DefinedValue, this)); + if (datatypeValue != null) { + foreach (var destructor in datatypeValue.UnnamedDestructors) { + yield return destructor; + } + } + } + + public IEnumerable SetElements() { + return Constraints.OfType() + .Where(containment => Equals(containment.Set, this)) + .Select(containment => containment.Element); + } + + public string DatatypeConstructorName() { + return Constraints.OfType() + .Select(constructorCheck => constructorCheck.ConstructorName).FirstOrDefault() ?? ""; + } + + public IEnumerable<(PartialValue Key, PartialValue Value)> Mappings() { + foreach (var mapping in Constraints.OfType().Where(constraint => Equals(constraint.Map, this))) { + yield return new(mapping.Key, mapping.DefinedValue); + } + } + + public int? Cardinality() { + if (Constraints.OfType().Any(constraint => + (constraint.LiteralExpr is DisplayExpression displayExpression && !displayExpression.SubExpressions.Any()) || + (constraint.LiteralExpr is MapDisplayExpr mapDisplayExpr && !mapDisplayExpr.Elements.Any()))) { + return 0; + } + + var cardinality = Constraints.OfType() + .FirstOrDefault(constraint => Equals(constraint.Collection, this))?.DefinedValue; + if (cardinality == null) { + return -1; + } + + var cardinalityLiteral = + cardinality.Constraints.OfType().FirstOrDefault()?.LiteralExpr as LiteralExpr; + if (cardinalityLiteral == null) { + return -1; + } + + if (cardinalityLiteral.Value is not BigInteger bigInteger || + !bigInteger.LessThanOrEquals(new BigInteger(int.MaxValue))) { + return -1; + } + + return (int)bigInteger; + } + + + public PartialValue? this[int i] { + get { + foreach (var seqSelectConstraint in Constraints.OfType() + .Where(constraint => Equals(constraint.Seq, this))) { + if (seqSelectConstraint.Index.ToString() == i.ToString()) { + return seqSelectConstraint.DefinedValue; + } + } + + foreach (var seqSelectConstraint in Constraints.OfType() + .Where(constraint => Equals(constraint.Seq, this))) { + var indexLiteral = seqSelectConstraint.Index.Constraints.OfType().FirstOrDefault() + ?.LiteralExpr; + if (indexLiteral != null && indexLiteral.ToString() == i.ToString()) { + return seqSelectConstraint.DefinedValue; + } + } + + return null; + } + } + + public override bool Equals(object? obj) { + return obj is PartialValue other && other.Element == Element && other.state == state; + } + + public override int GetHashCode() { + return Element.GetHashCode(); + } + +} \ No newline at end of file diff --git a/Source/DafnyCore/CounterExampleGeneration/README.md b/Source/DafnyCore/CounterExampleGeneration/README.md deleted file mode 100644 index 42d4b3d2b86..00000000000 --- a/Source/DafnyCore/CounterExampleGeneration/README.md +++ /dev/null @@ -1,15 +0,0 @@ -# Counterexample Generation - -The following is a class-by-class description of the files in this directory intended to help with maintaining and improving the counterexample generation feature of Dafny: - -- [DafnyModel](DafnyModel.cs) - a wrapper around Boogie's `Model` class that defines Dafny specific functions and provides functionality for extracting types and values of `Elements` representing Dafny variables. The three core methods are: - - `GetDafnyType`, which returns a `DafnyModelType` instance for an arbitrary `Element` in the underlying model - - `CanonicalName`, which returns the value of any Element representing a variable of the basic type in Dafny - - `GetExpansion`, which computes all the "children" of a particular variable, that is fields for objects, destructor values for datatypes, elements for sequences, etc. -- [DafnyModelState](DafnyModelState.cs) - Represents a state in a `DafnyModel` and captures the values of all variables at a particular point in the code. -- [DafnyModelVariable](DafnyModelVariable.cs) - Represents a variable at a particular state. Note that a variable in Dafny source can be represented by multiple `DafnyModelVariables`, one for each `DafnyModelState` in `DafnyModel`. The subclasses of `DafnyModelVariable` are: - - `DuplicateVariable` - a variable that has a different name but represents the same `Element` in the same `DafnyModelState` as some other variable. - - `MapVariable` - a variable that represents a map. Allows adding mappings to the map and displaying the map using Dafny syntax. - - `SeqVariable` - a variable that represents a sequence. Allows displaying the sequence using Dafny syntax. -- [DafnyModelVariableFactory](DafnyModelVariable.cs) - A static class for generating instance of `DafnyModelvariable` and its subclasses. The factory chooses which subclass of `DafnyModelVariable` to employ depending on the `Microsoft.Dafny.Type` of the `Element` for which the variable is generated. -- [DafnyModelType](DafnyModelTypeUtils.cs) - Contains a set of utils for manipulating type objects (e.g. reconstructing the original Dafny type name from its Boogie translation: `Mo_dule_.Module2_.Cla__ss` from `Mo__dule___mModule2__.Cla____ss`). diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index c27b90f21bc..23025289acf 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -1510,7 +1510,7 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, } var loopBodyBuilder = new BoogieStmtListBuilder(this, options); - loopBodyBuilder.AddCaptureState(s.Tok, true, "after some loop iterations"); + loopBodyBuilder.AddCaptureState(s.Tok, true, CaptureStateExtensions.AfterLoopIterationsStateMarker); // As the first thing inside the loop, generate: if (!w) { CheckWellformed(inv); assume false; } invDefinednessBuilder.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False)); diff --git a/Source/DafnyCore/Verifier/CaptureStateExtensions.cs b/Source/DafnyCore/Verifier/CaptureStateExtensions.cs index b406b4aa7a0..acb4a5a3f7d 100644 --- a/Source/DafnyCore/Verifier/CaptureStateExtensions.cs +++ b/Source/DafnyCore/Verifier/CaptureStateExtensions.cs @@ -3,9 +3,11 @@ using Bpl = Microsoft.Boogie; namespace Microsoft.Dafny { - static class CaptureStateExtensions { + public static class CaptureStateExtensions { - public static void AddCaptureState(this BoogieStmtListBuilder builder, Statement statement) { + public const string AfterLoopIterationsStateMarker = "after some loop iterations"; + + internal static void AddCaptureState(this BoogieStmtListBuilder builder, Statement statement) { if (builder.Options.ExpectingModel || builder.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) { builder.Add(CaptureState(builder.Options, statement)); } @@ -17,7 +19,7 @@ private static Bpl.Cmd CaptureState(DafnyOptions options, Statement stmt) { return CaptureState(options, stmt.RangeToken.EndToken, true, null); } - public static void AddCaptureState(this BoogieStmtListBuilder builder, IToken tok, bool isEndToken, string /*?*/ additionalInfo) { + internal static void AddCaptureState(this BoogieStmtListBuilder builder, IToken tok, bool isEndToken, string /*?*/ additionalInfo) { if (builder.Options.ExpectingModel || builder.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) { builder.Add(CaptureState(builder.Options, tok, isEndToken, additionalInfo)); } diff --git a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs index 660d1a95ea2..d57d6dc0f18 100644 --- a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs @@ -5,21 +5,16 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using OmniSharp.Extensions.LanguageServer.Protocol; using System.Linq; +using System.Numerics; using System.Text.RegularExpressions; using System.Threading.Tasks; using Microsoft.Boogie; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Microsoft.Dafny.LanguageServer.Workspace; -using Microsoft.Extensions.Logging; using Xunit; using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { - static class StringAssert { - public static void Matches(string value, Regex regex) { - Assert.True(regex.Matches(value).Any()); - } - } public class CounterExampleTest : ClientBasedLanguageServerTest { @@ -50,7 +45,7 @@ public async Task CounterexamplesStillWorksIfNothingHasBeenVerified(Action options.Set(ProjectManager.Verification, VerifyOnMode.Never)); var source = @" method Abs(x: int) returns (y: int) - ensures y > 0 + ensures y >= 0 { } ".TrimStart(); @@ -61,7 +56,7 @@ ensures y > 0 OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); Assert.Equal((2, 6), counterExamples[0].Position); - Assert.True(counterExamples[0].Variables.ContainsKey("y:int")); + Assert.Matches("-[0-9]+ == y", counterExamples[0].Assumption); } [Theory] @@ -70,7 +65,7 @@ public async Task FileWithBodyLessMethodReturnsSingleCounterExampleForPostcondit await SetUpOptions(optionSettings); var source = @" method Abs(x: int) returns (y: int) - ensures y > 0 + ensures y >= 0 { } ".TrimStart(); @@ -81,7 +76,7 @@ ensures y > 0 OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); Assert.Equal((2, 6), counterExamples[0].Position); - Assert.True(counterExamples[0].Variables.ContainsKey("y:int")); + Assert.Matches("-[0-9]+ == y", counterExamples[0].Assumption); } [Theory] @@ -104,9 +99,7 @@ method Abs(x: int) returns (y: int) Assert.Equal((2, 6), counterExamples[0].Position); Assert.Equal((3, 18), counterExamples[1].Position); Assert.Equal((4, 14), counterExamples[2].Position); - Assert.True(counterExamples[2].Variables.ContainsKey("x:int")); - Assert.True(counterExamples[2].Variables.ContainsKey("y:int")); - Assert.True(counterExamples[2].Variables.ContainsKey("z:int")); + Assert.Matches("-[0-9]+ == [xyz]", counterExamples[2].Assumption); } [Theory] @@ -136,7 +129,7 @@ public async Task GetCounterExampleWithMultipleMethodsWithErrorsReturnsCounterEx await SetUpOptions(optionSettings); var source = @" method Abs(x: int) returns (y: int) - ensures y > 0 + ensures y >= 0 { } @@ -154,10 +147,15 @@ method Negate(a: int) returns (b: int) .OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); Assert.Equal((2, 6), counterExamples[0].Position); - Assert.True(counterExamples[0].Variables.ContainsKey("y:int")); + Assert.Matches(new Regex("-[0-9]+ == y"), counterExamples[0].Assumption); Assert.Equal((7, 6), counterExamples[1].Position); - Assert.True(counterExamples[1].Variables.ContainsKey("a:int")); - Assert.True(counterExamples[1].Variables.ContainsKey("b:int")); + var aRegex = new Regex("(-?[0-9]+) == a"); + var bRegex = new Regex("(-?[0-9]+) == b"); + Assert.Matches(aRegex, counterExamples[1].Assumption); + Assert.Matches(bRegex, counterExamples[1].Assumption); + Assert.NotEqual( + aRegex.Match(counterExamples[1].Assumption).Groups[1].Value, + bRegex.Match(counterExamples[1].Assumption).Groups[1].Value); } [Theory] @@ -174,9 +172,24 @@ method a(r:real) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("r:real")); - Assert.Equal("1.0", counterExamples[0].Variables["r:real"]); + Assert.Contains("1.0 == r", counterExamples[0].Assumption); + } + + [Theory] + [MemberData(nameof(OptionSettings))] + public async Task SpecificInteger(Action optionSettings) { + await SetUpOptions(optionSettings); + var source = @" + method a(i:int) { + assert i != 25; + } + ".TrimStart(); + var documentItem = CreateTestDocument(source, "integer.dfy"); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var counterExamples = (await RequestCounterExamples(documentItem.Uri)). + OrderBy(counterexample => counterexample.Position).ToArray(); + Assert.Single(counterExamples); + Assert.Contains("25 == i", counterExamples[0].Assumption); } [Theory] @@ -193,9 +206,7 @@ method a(r:real) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("r:real")); - StringAssert.Matches(counterExamples[0].Variables["r:real"], new Regex("[0-9]+\\.[0-9]+/[0-9]+\\.[0-9]+")); + Assert.Matches("[0-9]+\\.[0-9]+ / [0-9]+\\.[0-9]+ == r;", counterExamples[0].Assumption); } [Theory] @@ -215,9 +226,7 @@ method a(v:Value) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("v:_module.Value")); - Assert.Equal("(v := 0.0)", counterExamples[0].Variables["v:_module.Value"]); + Assert.Contains("0.0 == v.v", counterExamples[0].Assumption); } [Theory] @@ -237,9 +246,7 @@ method a(v:Value) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("v:_module.Value")); - Assert.Equal("(with_underscore_ := 42)", counterExamples[0].Variables["v:_module.Value"]); + Assert.Contains("42 == v.with_underscore_", counterExamples[0].Assumption); } [Theory] @@ -259,9 +266,7 @@ method a(v:Value) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("v:_module.Value")); - StringAssert.Matches(counterExamples[0].Variables["v:_module.Value"], new Regex("\\(v := [0-9]+\\.[0-9]+/[0-9]+\\.[0-9]+\\)")); + Assert.Matches($"\\(?[0-9]+\\.[0-9]+ / [0-9]+\\.[0-9]+\\)? == v.v", counterExamples[0].Assumption); } [Theory] @@ -281,12 +286,10 @@ method IsSelfReferring(n:Node) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("n:_module.Node")); - Assert.Equal("(next := n)", counterExamples[0].Variables["n:_module.Node"]); + Assert.Matches("n == n.next", counterExamples[0].Assumption); } - [Theory] + [Theory(Skip = "This test should be re-enabled once we can assert inequality between objects")] [MemberData(nameof(OptionSettings))] public async Task ObjectWithANonNullField(Action optionSettings) { await SetUpOptions(optionSettings); @@ -303,9 +306,8 @@ method IsSelfRecursive(n:Node) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(2, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("n:_module.Node")); - StringAssert.Matches(counterExamples[0].Variables["n:_module.Node"], new Regex("\\(next := @[0-9]+\\)")); + Assert.Contains("n != null", counterExamples[0].Assumption); + Assert.Contains("n.next != n", counterExamples[0].Assumption); } [Theory] @@ -325,9 +327,7 @@ method IsSelfRecursive(n:Node) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("n:_module.Node")); - Assert.Equal("(next := null)", counterExamples[0].Variables["n:_module.Node"]); + Assert.Contains("null == n.next", counterExamples[0].Assumption); } [Theory] @@ -353,15 +353,8 @@ modifies this await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); - Assert.Equal(2, counterExamples.Length); - Assert.Equal(2, counterExamples[0].Variables.Count); - Assert.Equal(2, counterExamples[1].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("amount:int")); - Assert.True(counterExamples[1].Variables.ContainsKey("amount:int")); - Assert.True(counterExamples[0].Variables.ContainsKey("this:_module.BankAccountUnsafe")); - Assert.True(counterExamples[1].Variables.ContainsKey("this:_module.BankAccountUnsafe")); - StringAssert.Matches(counterExamples[0].Variables["this:_module.BankAccountUnsafe"], new Regex("\\(balance := [0-9]+\\)")); - StringAssert.Matches(counterExamples[1].Variables["this:_module.BankAccountUnsafe"], new Regex("\\(balance := \\-[0-9]+\\)")); + Assert.Matches("[0-9]+ == this.balance", counterExamples[0].Assumption); + Assert.Matches("-[0-9]+ == this.balance", counterExamples[1].Assumption); } [Theory] @@ -378,9 +371,29 @@ method a(c:char) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("c:char")); - Assert.Equal("'0'", counterExamples[0].Variables["c:char"]); + Assert.Contains("'0' == c", counterExamples[0].Assumption); + } + + [Theory] + [MemberData(nameof(OptionSettings))] + public async Task TwoCharacters(Action optionSettings) { + await SetUpOptions(optionSettings); + var source = @" + method a(c1:char, c2:char) { + assert c1 == c2; + } + ".TrimStart(); + var documentItem = CreateTestDocument(source, "TwoCharacters.dfy"); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var counterExamples = (await RequestCounterExamples(documentItem.Uri)). + OrderBy(counterexample => counterexample.Position).ToArray(); + Assert.Single(counterExamples); + var charRegex = "(\'[^']+\')"; + Assert.Matches(charRegex + " == c1", counterExamples[0].Assumption); + Assert.Matches(charRegex + " == c2", counterExamples[0].Assumption); + var c1 = Regex.Match(counterExamples[0].Assumption, charRegex + " == c1").Groups[1]; + var c2 = Regex.Match(counterExamples[0].Assumption, charRegex + " == c2").Groups[1]; + Assert.NotEqual(c1, c2); } [Theory] @@ -397,10 +410,7 @@ method a(c:char) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("c:char")); - StringAssert.Matches(counterExamples[0].Variables["c:char"], new Regex("('.'|\\?#[0-9]+)")); - Assert.NotEqual("'0'", counterExamples[0].Variables["c:char"]); + Assert.Matches("'.+' == c", counterExamples[0].Assumption); } [Theory] @@ -418,15 +428,31 @@ method a(b:B) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("b:_module.B")); - // Unnamed destructors are implicitly assigned names starting with "#" during resolution: - Assert.Equal("A(#0 := 5)", counterExamples[0].Variables["b:_module.B"]); + Assert.Contains("B.A(5) == b", counterExamples[0].Assumption); } [Theory] [MemberData(nameof(OptionSettings))] - public async Task DatatypeWithDestructorThanIsADataValue(Action optionSettings) { + public async Task DatatypeWithUnnamedDestructor2(Action optionSettings) { + await SetUpOptions(optionSettings); + var source = @" + datatype A = A(i:int) + datatype B = B(A) + method a(b:B) { + assert b != B(A(5)); + } + ".TrimStart(); + var documentItem = CreateTestDocument(source, "DatatypeWithUnnamedDestructor.dfy"); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var counterExamples = (await RequestCounterExamples(documentItem.Uri)). + OrderBy(counterexample => counterexample.Position).ToArray(); + Assert.Single(counterExamples); + Assert.Contains("B.B(A.A(5)) == b", counterExamples[0].Assumption); + } + + [Theory] + [MemberData(nameof(OptionSettings))] + public async Task DatatypeWithDestructorThatIsADataValue(Action optionSettings) { await SetUpOptions(optionSettings); var source = @" datatype A = B(x:real) @@ -439,9 +465,8 @@ method destructorNameTest(a:A) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("a:_module.A")); - StringAssert.Matches(counterExamples[0].Variables["a:_module.A"], new Regex("B\\(x := -[0-9]+\\.[0-9]+/[0-9]+\\.[0-9]+\\)")); + var realRegex = "-\\(?[0-9]+\\.[0-9]+ / [0-9]+\\.[0-9]+\\)"; + Assert.Matches($"A.B\\({realRegex}\\) == a", counterExamples[0].Assumption); } [Theory] @@ -460,11 +485,8 @@ requires h0.Right? && h1.Left? { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(2, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("h0:_module.Hand")); - Assert.True(counterExamples[0].Variables.ContainsKey("h1:_module.Hand")); - StringAssert.Matches(counterExamples[0].Variables["h0:_module.Hand"], new Regex("Right\\([a|b] := -?[0-9]+, [b|a] := -?[0-9]+\\)")); - StringAssert.Matches(counterExamples[0].Variables["h1:_module.Hand"], new Regex("Left\\([x|y] := -?[0-9]+, [x|y] := -?[0-9]+\\)")); + Assert.Matches("Hand\\.Right\\([0-9]+, [0-9]+\\) == h0", counterExamples[0].Assumption); + Assert.Matches("Hand\\.Left\\([0-9]+, [0-9]+\\) == h1", counterExamples[0].Assumption); } [Theory] @@ -482,9 +504,7 @@ method T_datatype0_1(h:Hand) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("h:_module.Hand")); - StringAssert.Matches(counterExamples[0].Variables["h:_module.Hand"], new Regex("Left\\([a|b] := 3, [a|b] := 3\\)")); + Assert.Contains("Hand.Left(3, 3) == h", counterExamples[0].Assumption); } [Theory] @@ -502,9 +522,7 @@ method m (a:A) requires !a.B_?{ var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("a:_module.A")); - StringAssert.Matches(counterExamples[0].Variables["a:_module.A"], new Regex("C\\((B_q|C_q|D_q) := false, (B_q|C_q|D_q) := false, (B_q|C_q|D_q) := false\\)")); + Assert.Contains("A.C(false, false, false) == a", counterExamples[0].Assumption); } @@ -523,36 +541,12 @@ method m(a:A) requires a == One(false) || a == One(true) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("a:_module.A")); - Assert.Equal("One(b := false)", counterExamples[0].Variables["a:_module.A"]); + Assert.Contains("A.One(false) == a", counterExamples[0].Assumption); } [Theory] [MemberData(nameof(OptionSettings))] - public async Task ArbitraryBool(Action optionSettings) { - await SetUpOptions(optionSettings); - var source = @" - datatype List = Nil | Cons(head: T, tail: List) - method listHasSingleElement(list:List) - requires list != Nil - { - assert list.tail != Nil; - } - ".TrimStart(); - var documentItem = CreateTestDocument(source, "ArbitraryBool.dfy"); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var counterExamples = (await RequestCounterExamples(documentItem.Uri)). - OrderBy(counterexample => counterexample.Position).ToArray(); - Assert.Single(counterExamples); - Assert.Equal(2, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("list:_module.List")); - StringAssert.Matches(counterExamples[0].Variables["list:_module.List"], new Regex("Cons\\(head := (true|false), tail := @[0-9]+\\)")); - } - - [Theory] - [MemberData(nameof(OptionSettings))] - public async Task ArbitraryInt(Action optionSettings) { + public async Task DestructorDoesNotMatter(Action optionSettings) { await SetUpOptions(optionSettings); var source = @" datatype List = Nil | Cons(head: T, tail: List) @@ -567,31 +561,7 @@ method listHasSingleElement(list:List) var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(2, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("list:_module.List")); - StringAssert.Matches(counterExamples[0].Variables["list:_module.List"], new Regex("Cons\\(head := -?[0-9]+, tail := @[0-9]+\\)")); - } - - [Theory] - [MemberData(nameof(OptionSettings))] - public async Task ArbitraryReal(Action optionSettings) { - await SetUpOptions(optionSettings); - var source = @" - datatype List = Nil | Cons(head: T, tail: List) - method listHasSingleElement(list:List) - requires list != Nil - { - assert list.tail != Nil; - } - ".TrimStart(); - var documentItem = CreateTestDocument(source, "ArbitraryReal.dfy"); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var counterExamples = (await RequestCounterExamples(documentItem.Uri)). - OrderBy(counterexample => counterexample.Position).ToArray(); - Assert.Single(counterExamples); - Assert.Equal(2, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("list:_module.List")); - StringAssert.Matches(counterExamples[0].Variables["list:_module.List"], new Regex("Cons\\(head := -?[0-9]+\\.[0-9], tail := @[0-9]+\\)")); + Assert.Matches("List\\.Cons\\([0-9]+, List\\.Nil\\) == list", counterExamples[0].Assumption); } [Theory] @@ -608,9 +578,9 @@ method a(arr:array) requires arr.Length == 2 { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("arr:_System.array"), string.Join(", ", counterExamples[0].Variables)); - Assert.Equal("(Length := 2, [0] := 4, [1] := 5)", counterExamples[0].Variables["arr:_System.array"]); + Assert.Contains("2 == arr.Length", counterExamples[0].Assumption); + Assert.Contains("4 == arr[0]", counterExamples[0].Assumption); + Assert.Contains("5 == arr[1]", counterExamples[0].Assumption); } [Theory] @@ -627,9 +597,8 @@ method a(s:seq) requires |s| == 1 { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("s:seq")); - Assert.Equal("[4]", counterExamples[0].Variables["s:seq"]); + Assert.Contains("1 == |s|", counterExamples[0].Assumption); + Assert.Contains("4 == s[0]", counterExamples[0].Assumption); } [Theory] @@ -646,9 +615,8 @@ method a(s:seq) requires |s| == 2 { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("s:seq")); - Assert.Equal("(Length := 2, [1] := 2)", counterExamples[0].Variables["s:seq"]); + Assert.Contains("2 == |s|", counterExamples[0].Assumption); + Assert.Contains("2 == s[1]", counterExamples[0].Assumption); } [Theory] @@ -665,9 +633,7 @@ method a(bv:bv7) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("bv:bv7")); - Assert.Equal("2", counterExamples[0].Variables["bv:bv7"]); + Assert.Contains("2 == bv", counterExamples[0].Assumption); } [Theory] @@ -684,9 +650,7 @@ method a(b:bv2) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("b:bv2")); - StringAssert.Matches(counterExamples[0].Variables["b:bv2"], new Regex("[023]")); + Assert.Matches("[023] == b", counterExamples[0].Assumption); } [Theory] @@ -703,11 +667,8 @@ method m(a:bv1, b:bv1) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(2, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("a:bv1")); - Assert.True(counterExamples[0].Variables.ContainsKey("b:bv1")); - StringAssert.Matches(counterExamples[0].Variables["a:bv1"], new Regex("(1|b)")); - StringAssert.Matches(counterExamples[0].Variables["b:bv1"], new Regex("(1|a)")); + Assert.Contains("1 == a", counterExamples[0].Assumption); + Assert.Contains("1 == b", counterExamples[0].Assumption); } [Theory] @@ -727,9 +688,7 @@ method a(v:Value) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("v:_module.Value")); - Assert.Equal("(b := 2)", counterExamples[0].Variables["v:_module.Value"]); + Assert.Matches("2 == v.b", counterExamples[0].Assumption); } [Theory] @@ -746,8 +705,8 @@ method a(s:set>>>) requires |s| <= 1{ var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.True(counterExamples[0].Variables.ContainsKey("s:set>>>")); - StringAssert.Matches(counterExamples[0].Variables["s:set>>>"], new Regex("\\{@[0-9]+ := true\\}")); + Assert.Contains("exists boundVar0: seq>>", counterExamples[0].Assumption); + Assert.Contains("boundVar0 in s", counterExamples[0].Assumption); } [Theory] @@ -764,9 +723,10 @@ method m(a:array3) requires a.Length0 == 4 requires a.Length1 == 5 requires var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("a:_System.array3"), string.Join(", ", counterExamples[0].Variables)); - Assert.Equal("(Length0 := 4, Length1 := 5, Length2 := 6, [2,3,1] := 7)", counterExamples[0].Variables["a:_System.array3"]); + Assert.Matches("(a.Length0 == 4|4 == a.Length0)", counterExamples[0].Assumption); + Assert.Matches("(a.Length1 == 5|5 == a.Length1)", counterExamples[0].Assumption); + Assert.Matches("(a.Length2 == 6|6 == a.Length2)", counterExamples[0].Assumption); + Assert.Contains("7 == a[2, 3, 1]", counterExamples[0].Assumption); } [Theory] @@ -783,10 +743,7 @@ method test(x:array, y:array) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(2, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("x:_System.array")); - Assert.True(counterExamples[0].Variables.ContainsKey("y:_System.array")); - Assert.True(counterExamples[0].Variables["y:_System.array"] == "x" || counterExamples[0].Variables["x:_System.array"] == "y"); + Assert.Matches("(x == y|y == x)", counterExamples[0].Assumption); } [Theory] @@ -806,27 +763,16 @@ method a(s1:set, s2:set) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(4, counterExamples.Length); - Assert.Equal(5, counterExamples[2].Variables.Count); - Assert.True(counterExamples[3].Variables.ContainsKey("s1:set")); - Assert.True(counterExamples[3].Variables.ContainsKey("s2:set")); - Assert.True(counterExamples[3].Variables.ContainsKey("sUnion:set")); - Assert.True(counterExamples[3].Variables.ContainsKey("sInter:set")); - Assert.True(counterExamples[3].Variables.ContainsKey("sDiff:set")); - var s1 = counterExamples[3].Variables["s1:set"][1..^1].Split(", "); - var s2 = counterExamples[3].Variables["s2:set"][1..^1].Split(", "); - var sUnion = counterExamples[3].Variables["sUnion:set"][1..^1].Split(", "); - var sInter = counterExamples[3].Variables["sInter:set"][1..^1].Split(", "); - var sDiff = counterExamples[3].Variables["sDiff:set"][1..^1].Split(", "); - Assert.Contains("'a' := true", s1); - Assert.Contains("'a' := false", s2); - Assert.Contains("'a' := true", sDiff); - Assert.Contains("'a' := true", sUnion); - Assert.Contains("'a' := false", sInter); - Assert.Contains("'b' := true", s1); - Assert.Contains("'b' := true", s2); - Assert.Contains("'b' := false", sDiff); - Assert.Contains("'b' := true", sUnion); - Assert.Contains("'b' := true", sInter); + Assert.Contains("'a' in s1", counterExamples[3].Assumption); + Assert.Contains("'a' !in s2", counterExamples[3].Assumption); + Assert.Contains("'a' in sDiff", counterExamples[3].Assumption); + Assert.Contains("'a' in sUnion", counterExamples[3].Assumption); + Assert.Contains("'a' !in sInter", counterExamples[3].Assumption); + Assert.Contains("'b' in s1", counterExamples[3].Assumption); + Assert.Contains("'b' in s2", counterExamples[3].Assumption); + Assert.Contains("'b' !in sDiff", counterExamples[3].Assumption); + Assert.Contains("'b' in sUnion", counterExamples[3].Assumption); + Assert.Contains("'b' in sInter", counterExamples[3].Assumption); } [Theory] @@ -843,9 +789,7 @@ method test() { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(1, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("s:set")); - StringAssert.Matches(counterExamples[1].Variables["s:set"], new Regex("\\{.*6 := true.*\\}")); + Assert.Contains("6 in s", counterExamples[1].Assumption); } [Theory] @@ -861,9 +805,7 @@ public async Task StringBuilding(Action optionSettings) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("s:seq")); - Assert.Equal("['a', 'b', 'c']", counterExamples[0].Variables["s:seq"]); + Assert.Contains("['a', 'b', 'c'] == s", counterExamples[0].Assumption); } [Theory] @@ -879,13 +821,10 @@ public async Task SequenceEdit(Action optionSettings) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(3, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("s1:seq")); - Assert.True(counterExamples[1].Variables.ContainsKey("s2:seq")); - Assert.True(counterExamples[1].Variables.ContainsKey("c:char")); - Assert.Equal("['a', 'b', 'c']", counterExamples[1].Variables["s1:seq"]); - Assert.Equal("['a', 'd', 'c']", counterExamples[1].Variables["s2:seq"]); - Assert.Equal("'d'", counterExamples[1].Variables["c:char"]); + Assert.Contains("3 == |s2|", counterExamples[1].Assumption); + Assert.Contains("'a' == s2[0]", counterExamples[1].Assumption); + Assert.Contains("'d' == s2[1]", counterExamples[1].Assumption); + Assert.Contains("'c' == s2[2]", counterExamples[1].Assumption); } [Theory] @@ -902,9 +841,7 @@ method test() { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(1, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("s:seq")); - StringAssert.Matches(counterExamples[1].Variables["s:seq"], new Regex("\\[6\\]")); + Assert.Contains("[6] == s", counterExamples[1].Assumption); } [Theory] @@ -913,7 +850,7 @@ public async Task SequenceConcat(Action optionSettings) { await SetUpOptions(optionSettings); var source = @" method a(s1:string, s2:string) requires |s1| == 1 && |s2| == 1 { - var sCat:string := s2 + s1; + var sCat:string := s1 + s2; assert sCat[0] != 'a' || sCat[1] != 'b'; }".TrimStart(); var documentItem = CreateTestDocument(source, "SequenceConcat.dfy"); @@ -921,16 +858,15 @@ method a(s1:string, s2:string) requires |s1| == 1 && |s2| == 1 { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(3, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("s1:seq")); - Assert.True(counterExamples[1].Variables.ContainsKey("s2:seq")); - Assert.True(counterExamples[1].Variables.ContainsKey("sCat:seq")); - Assert.Equal("['b']", counterExamples[1].Variables["s1:seq"]); - Assert.Equal("['a']", counterExamples[1].Variables["s2:seq"]); - Assert.Equal("['a', 'b']", counterExamples[1].Variables["sCat:seq"]); + Assert.Contains("1 == |s1|", counterExamples[1].Assumption); + Assert.Contains("1 == |s2|", counterExamples[1].Assumption); + Assert.Contains("'a' == sCat[0]", counterExamples[1].Assumption); + Assert.Contains("'a' == s1[0]", counterExamples[1].Assumption); + Assert.Contains("'b' == sCat[1]", counterExamples[1].Assumption); + Assert.Contains("'b' == s2[0]", counterExamples[1].Assumption); } - [Theory] + [Theory(Skip = "This test should be re-enabled once counterexamples support lambda expressions")] [MemberData(nameof(OptionSettings))] public async Task SequenceGenerate(Action optionSettings) { await SetUpOptions(optionSettings); @@ -943,11 +879,7 @@ method a(multiplier:int) { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); - Assert.Equal(2, counterExamples.Length); - Assert.True(counterExamples[1].Variables.ContainsKey("multiplier:int")); - Assert.True(counterExamples[1].Variables.ContainsKey("s:seq")); - StringAssert.Matches(counterExamples[1].Variables["s:seq"], new Regex("\\(Length := 3, .*\\[2\\] := 6.*\\)")); - Assert.Equal("3", counterExamples[1].Variables["multiplier:int"]); + Assert.Fail("This test needs to be updated in a way that deals with the variables introduced as part of the lambda expression."); } [Theory] @@ -955,8 +887,8 @@ method a(multiplier:int) { public async Task SequenceSub(Action optionSettings) { await SetUpOptions(optionSettings); var source = @" - method a(s:seq) requires |s| == 5 { - var sSub:seq := s[2..4]; + method a(s:seq) requires |s| == 7 { + var sSub:seq := s[2..6]; assert sSub[0] != 'a' || sSub[1] != 'b'; }".TrimStart(); var documentItem = CreateTestDocument(source, "SequenceSub.dfy"); @@ -964,11 +896,12 @@ method a(s:seq) requires |s| == 5 { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(2, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("sSub:seq")); - Assert.True(counterExamples[1].Variables.ContainsKey("s:seq")); - Assert.Equal("['a', 'b']", counterExamples[1].Variables["sSub:seq"]); - StringAssert.Matches(counterExamples[0].Variables["s:seq"], new Regex("\\(Length := 5,.*\\[2\\] := 'a', \\[3\\] := 'b'.*")); + Assert.Contains("4 == |sSub|", counterExamples[1].Assumption); + Assert.Contains("7 == |s|", counterExamples[1].Assumption); + Assert.Contains("'a' == s[2]", counterExamples[1].Assumption); + Assert.Contains("'b' == s[3]", counterExamples[1].Assumption); + Assert.Contains("'a' == sSub[0]", counterExamples[1].Assumption); + Assert.Contains("'b' == sSub[1]", counterExamples[1].Assumption); } [Theory] @@ -976,20 +909,16 @@ method a(s:seq) requires |s| == 5 { public async Task SequenceDrop(Action optionSettings) { await SetUpOptions(optionSettings); var source = @" - method a(s:seq) requires |s| == 5 { + method a(s:seq) requires s == ['a', 'b', 'c', 'd', 'e'] { var sSub:seq := s[2..]; - assert sSub[0] != 'a' || sSub[1] != 'b' || sSub[2] != 'c'; + assert false; }".TrimStart(); var documentItem = CreateTestDocument(source, "SequenceDrop.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(2, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("sSub:seq")); - Assert.True(counterExamples[1].Variables.ContainsKey("s:seq")); - Assert.Equal("['a', 'b', 'c']", counterExamples[1].Variables["sSub:seq"]); - StringAssert.Matches(counterExamples[0].Variables["s:seq"], new Regex("\\(Length := 5,.*\\[2\\] := 'a', \\[3\\] := 'b', \\[4\\] := 'c'.*")); + Assert.Contains("['c', 'd', 'e'] == sSub", counterExamples[1].Assumption); } [Theory] @@ -1006,11 +935,9 @@ method a(s:seq) requires |s| == 5 { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(2, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("sSub:seq")); - Assert.True(counterExamples[1].Variables.ContainsKey("s:seq")); - Assert.Equal("['a', 'b', 'c']", counterExamples[1].Variables["sSub:seq"]); - StringAssert.Matches(counterExamples[0].Variables["s:seq"], new Regex("\\(Length := 5,.*\\[0\\] := 'a', \\[1\\] := 'b', \\[2\\] := 'c'.*")); + Assert.Contains("'a' == s[0]", counterExamples[0].Assumption); + Assert.Contains("'b' == s[1]", counterExamples[0].Assumption); + Assert.Contains("'c' == s[2]", counterExamples[0].Assumption); } [Theory] @@ -1043,9 +970,8 @@ method test() { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(1, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("m:map")); - StringAssert.Matches(counterExamples[1].Variables["m:map"], new Regex("map\\[.*3 := false.*")); + Assert.Contains("3 in m", counterExamples[1].Assumption); + Assert.Contains("false == m[3]", counterExamples[1].Assumption); } [Theory] @@ -1055,29 +981,56 @@ public async Task MapsEmpty(Action optionSettings) { var source = @" method test() { var m : map := map[]; - assert 3 in m; + assert false; }".TrimStart(); var documentItem = CreateTestDocument(source, "MapsEmpty.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(1, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("m:map")); - Assert.Equal("map[]", counterExamples[1].Variables["m:map"]); + Assert.Matches("(map\\[\\] == m|0 == \\|m\\|)", counterExamples[1].Assumption); } - [Theory] + [Theory(Skip = "This test should be re-enabled once we support traits")] [MemberData(nameof(OptionSettings))] public async Task TraitType(Action optionSettings) { await SetUpOptions(optionSettings); var source = @" module M { - trait C { - predicate Valid() {false} + trait T { + function Value():int reads this + } + class C extends T { + var value:int + function Value():int + reads this + { value } + } + method test(t1:T, t2:T) { + assert t1.Value() == t2.Value(); + } + }".TrimStart(); + var documentItem = CreateTestDocument(source, "TraitType.dfy"); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var counterExamples = (await RequestCounterExamples(documentItem.Uri)). + OrderBy(counterexample => counterexample.Position).ToArray(); + Assert.Single(counterExamples); + Assert.Fail("This test needs to be updated once we support traits"); + } + + [Theory] + [MemberData(nameof(OptionSettings))] + public async Task ClassTypeWithPredicate(Action optionSettings) { + await SetUpOptions(optionSettings); + var source = @" + module M { + class C { + predicate Valid() + function Identity(i:int):int + function Sum(a:int, b:int):int } method test(c:C) { - assert c.Valid(); + assert !c.Valid() || c.Identity(1) != 1 || c.Sum(1, 2) != 3; } }".TrimStart(); var documentItem = CreateTestDocument(source, "TraitType.dfy"); @@ -1085,8 +1038,9 @@ method test(c:C) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Single(counterExamples[0].Variables); - Assert.True(counterExamples[0].Variables.ContainsKey("c:M.C")); + Assert.Contains("1 == c.Identity(1)", counterExamples[0].Assumption); + Assert.Contains("3 == c.Sum(1, 2)", counterExamples[0].Assumption); + Assert.Contains("true == c.Valid()", counterExamples[0].Assumption); } [Theory] @@ -1105,7 +1059,7 @@ method test() { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); - Assert.True(counterExamples[^1].Variables.ContainsKey("c:(int, bool) ~> real")); + Assert.Equal(4, counterExamples.Count()); } [Theory] @@ -1122,8 +1076,9 @@ method test() { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(2, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("s:set>")); + Assert.Matches("boundVar[0-9]+: map", counterExamples[1].Assumption); + Assert.Matches("boundVar[0-9]+ in s", counterExamples[1].Assumption); + Assert.Matches("5 == boundVar[0-9]+\\[3\\]", counterExamples[1].Assumption); } [Theory] @@ -1133,8 +1088,7 @@ public async Task DatatypeTypeAsTypeArgument(Action optionSettings var source = @" module M { datatype C = A | B - method test() { - var s : set := {A}; + method test(s:set) { assert |s| == 0; } }".TrimStart(); @@ -1142,10 +1096,9 @@ method test() { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); - Assert.Equal(2, counterExamples.Length); - Assert.Equal(2, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("s:set")); - Assert.Contains(counterExamples[1].Variables.Keys, key => key.EndsWith("M.C")); + Assert.Single(counterExamples); + Assert.Contains("exists boundVar0: M.C ::", counterExamples[0].Assumption); + Assert.Contains("boundVar0 in s", counterExamples[0].Assumption); } [Theory] @@ -1162,10 +1115,9 @@ method test() { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(1, counterExamples[1].Variables.Count); - // Cannot infer the type when Arguments polymorphic encoding is used - Assert.True(counterExamples[1].Variables.ContainsKey("s:set")); - Assert.Equal("{}", counterExamples[1].Variables["s:set"]); + // the assertion below ensures Dafny does not emit a type constraint if it cannot figure out the variable's type + Assert.DoesNotContain("?", counterExamples[1].Assumption); + Assert.Matches("({} == s|0 == \\|s\\|)", counterExamples[1].Assumption); } [Theory] @@ -1173,27 +1125,21 @@ method test() { public async Task MapsUpdate(Action optionSettings) { await SetUpOptions(optionSettings); var source = @" - method test(value:int) { + method test(value:int) requires value != 3 { var m := map[3 := -1]; - var b := m[3] == -1; m := m[3 := value]; - assert b && m[3] <= 0; + assert m[3] <= 0; }".TrimStart(); var documentItem = CreateTestDocument(source, "MapsUpdate.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); - Assert.Equal(4, counterExamples.Length); - Assert.Equal(2, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("m:map")); - StringAssert.Matches(counterExamples[1].Variables["m:map"], new Regex("map\\[.*3 := -1.*")); - Assert.Equal(3, counterExamples[3].Variables.Count); - Assert.True(counterExamples[3].Variables.ContainsKey("m:map")); - Assert.True(counterExamples[3].Variables.ContainsKey("value:int")); - Assert.True(counterExamples[3].Variables.ContainsKey("b:bool")); - Assert.Equal("true", counterExamples[3].Variables["b:bool"]); - StringAssert.Matches(counterExamples[3].Variables["value:int"], new Regex("[1-9][0-9]*")); - StringAssert.Matches(counterExamples[3].Variables["m:map"], new Regex("map\\[.*3 := [1-9].*")); + Assert.Equal(3, counterExamples.Length); + Assert.Contains("-1 == m[3]", counterExamples[1].Assumption); + Assert.Matches("[1-9][0-9]* == m\\[3\\]", counterExamples[2].Assumption); + Assert.Matches("[1-9][0-9]* == value", counterExamples[2].Assumption); + Assert.DoesNotContain("m[3] == -1", counterExamples[2].Assumption); + Assert.DoesNotContain("-1 == m[3]", counterExamples[2].Assumption); } [Theory] @@ -1201,38 +1147,30 @@ method test(value:int) { public async Task MapsUpdateStoredInANewVariable(Action optionSettings) { await SetUpOptions(optionSettings); var source = @" - method T_map1(m:map, key:int, val:int) - requires key in m.Keys + method T_map1(m:map) { - var m' := m[key := val - 1]; - m' := m'[key := val]; - assert m'.Values == m.Values - {m[key]} + {val}; + var m' := m[4 := 5]; + m' := m'[4 := 6]; + assert m'.Values == m.Values - {m[4]} + {6}; }".TrimStart(); var documentItem = CreateTestDocument(source, "MapsUpdateStoredInANewVariable.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); - Assert.Equal(3, counterExamples.Length); - Assert.Equal(4, counterExamples[2].Variables.Count); - Assert.True(counterExamples[2].Variables.ContainsKey("m:map")); - Assert.True(counterExamples[2].Variables.ContainsKey("m':map")); - Assert.True(counterExamples[2].Variables.ContainsKey("val:int")); - Assert.True(counterExamples[2].Variables.ContainsKey("key:int")); - var key = counterExamples[2].Variables["key:int"]; - var val = counterExamples[2].Variables["val:int"]; - StringAssert.Matches(counterExamples[2].Variables["m':map"], new Regex("map\\[.*" + key + " := " + val + ".*")); + Assert.Contains("6 == m'[4]", counterExamples.Last().Assumption); + Assert.DoesNotContain("5 == m'[4]", counterExamples.Last().Assumption); } [Theory] [MemberData(nameof(OptionSettings))] - public async Task MapsBuildRecursive(Action optionSettings) { + public async Task MapsBuildRecursiveSameValue(Action optionSettings) { await SetUpOptions(optionSettings); var source = @" method T_map2() { - var m := map[5 := 39]; - m := m[5 := 38]; - m := m[5 := 37]; + var m := map[5 := 9]; + m := m[5 := 99]; + m := m[5 := 999]; m := m[5 := 36]; assert 5 !in m; }".TrimStart(); @@ -1241,9 +1179,34 @@ method T_map2() var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(5, counterExamples.Length); - Assert.Equal(1, counterExamples[4].Variables.Count); - Assert.True(counterExamples[4].Variables.ContainsKey("m:map")); - StringAssert.Matches(counterExamples[4].Variables["m:map"], new Regex("map\\[.*5 := 36.*")); + Assert.Contains("5 in m", counterExamples[4].Assumption); + Assert.Contains("36 == m[5]", counterExamples[4].Assumption); + Assert.DoesNotContain("9", counterExamples[4].Assumption); + } + + [Theory] + [MemberData(nameof(OptionSettings))] + public async Task MapsBuildRecursive(Action optionSettings) { + await SetUpOptions(optionSettings); + var source = @" + method T_map2() + { + var m := map[1 := 9]; + m := m[2 := 99]; + m := m[3 := 999]; + assert false; + }".TrimStart(); + var documentItem = CreateTestDocument(source, "MapsBuildRecursive.dfy"); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var counterExamples = (await RequestCounterExamples(documentItem.Uri)). + OrderBy(counterexample => counterexample.Position).ToArray(); + Assert.Equal(4, counterExamples.Length); + Assert.Contains("1 in m", counterExamples[3].Assumption); + Assert.Contains("2 in m", counterExamples[3].Assumption); + Assert.Contains("3 in m", counterExamples[3].Assumption); + Assert.Contains("9 == m[1]", counterExamples[3].Assumption); + Assert.Contains("99 == m[2]", counterExamples[3].Assumption); + Assert.Contains("999 == m[3]", counterExamples[3].Assumption); } [Theory] @@ -1262,17 +1225,8 @@ method T_map0(m:map, key:int, val:int) var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(4, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("m:map")); - Assert.True(counterExamples[1].Variables.ContainsKey("m':map")); - Assert.True(counterExamples[1].Variables.ContainsKey("val:int")); - Assert.True(counterExamples[1].Variables.ContainsKey("key:int")); - var key = counterExamples[1].Variables["key:int"]; - var val = counterExamples[1].Variables["val:int"]; - var mapRegex = new Regex("map\\[.*" + key + " := " + val + ".*"); - Assert.True(mapRegex.IsMatch(counterExamples[1].Variables["m':map"]) || - mapRegex.IsMatch(counterExamples[1].Variables["m:map"])); - + // The precise counterexample that Dafny returns in this case is ambiguous, so there are no further assertions. + // Keeping this test case because it used to trigger an infinite loop. } [Theory] @@ -1289,11 +1243,8 @@ method test(m:map) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(2, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("m:map")); - Assert.True(counterExamples[1].Variables.ContainsKey("keys:set")); - StringAssert.Matches(counterExamples[1].Variables["m:map"], new Regex("map\\[.*25 := .*")); - StringAssert.Matches(counterExamples[1].Variables["keys:set"], new Regex("\\{.*25 := true.*")); + Assert.Contains("25 in m", counterExamples[1].Assumption); + Assert.Matches("(keys == m.Keys|m.Keys == keys)", counterExamples[1].Assumption); } [Theory] @@ -1310,11 +1261,9 @@ method test(m:map) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Equal(2, counterExamples.Length); - Assert.Equal(2, counterExamples[1].Variables.Count); - Assert.True(counterExamples[1].Variables.ContainsKey("m:map")); - Assert.True(counterExamples[1].Variables.ContainsKey("values:set")); - StringAssert.Matches(counterExamples[1].Variables["m:map"], new Regex("map\\[.* := 'c'.*")); - StringAssert.Matches(counterExamples[1].Variables["values:set"], new Regex("\\{.*'c' := true.*")); + Assert.Equal(2, counterExamples.Length); + Assert.Matches("('c' in values|'c' in m.Values)", counterExamples[1].Assumption); + Assert.Matches("(values == m.Values|m.Values == values)", counterExamples[1].Assumption); } [Theory] @@ -1333,9 +1282,7 @@ method test(m:map) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("m:map")); - StringAssert.Matches(counterExamples[0].Variables["m:map"], new Regex("map\\[.*[0-9]+ := [0-9]+.*")); + Assert.Matches("[0-9]+ in m", counterExamples[0].Assumption); } [Theory] @@ -1358,9 +1305,7 @@ method test() { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(1, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("this:Mo_dule_.Module2_.Cla__ss")); - Assert.Equal("(i := 5)", counterExamples[0].Variables["this:Mo_dule_.Module2_.Cla__ss"]); + Assert.Matches("5 == this.i", counterExamples[0].Assumption); } [Theory] @@ -1380,10 +1325,12 @@ function plus(a: nat64, b: nat64): nat64 { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.True(counterExamples[0].Variables.ContainsKey("a:int")); - Assert.True(counterExamples[0].Variables.ContainsKey("b:int")); - var a = long.Parse(counterExamples[0].Variables["a:int"]); - var b = long.Parse(counterExamples[0].Variables["b:int"]); + var aRegex = new Regex("([0-9]+) == a"); + var bRegex = new Regex("([0-9]+) == b"); + Assert.Matches(aRegex, counterExamples[0].Assumption); + Assert.Matches(bRegex, counterExamples[0].Assumption); + var a = long.Parse(aRegex.Match(counterExamples[0].Assumption).Groups[1].Value); + var b = long.Parse(bRegex.Match(counterExamples[0].Assumption).Groups[1].Value); Assert.True(a + b < a || a + b < b); } @@ -1396,20 +1343,20 @@ module M { datatype D = C(i:int) { predicate p() {true} } - - method test(d: D) { + } + method test(d: M.D) { if (d.p()) { - assert d.i != 123; + assert d.i != 123; } - } }".TrimStart(); var documentItem = CreateTestDocument(source, "DatatypeWithPredicate.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.True(counterExamples[0].Variables.ContainsKey("d:M.D")); - Assert.Equal("C(i := 123)", counterExamples[0].Variables["d:M.D"]); + Assert.Contains("M.D.C(123) == d", counterExamples.First().Assumption); + Assert.Contains("M.D.C(123).p.requires()", counterExamples.First().Assumption); + Assert.Contains("true == M.D.C(123).p()", counterExamples.First().Assumption); } /** Makes sure the counterexample lists the base type of a variable */ @@ -1427,8 +1374,6 @@ public async Task SubsetType(Action optionSettings) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.True(counterExamples[0].Variables.ContainsKey("s:seq")); - Assert.Equal("['a', 'w', 's']", counterExamples[0].Variables["s:seq"]); } /// @@ -1455,10 +1400,9 @@ method test(c: C?) { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.True(counterExamples[0].Variables.ContainsKey("c:M.C?")); - Assert.True(counterExamples[0].Variables["c:M.C?"] is - "(c1 := '\\u1023', c2 := '\\u1023')" or - "(c2 := '\\u1023', c1 := '\\u1023')"); + Assert.Contains("c != null", counterExamples[0].Assumption); + Assert.Contains("'\\U{1023}' == c.c1", counterExamples[0].Assumption); + Assert.Contains("'\\U{1023}' == c.c2", counterExamples[0].Assumption); } /// @@ -1475,11 +1419,10 @@ public async Task NonIntegerSeqIndices(Action optionSettings) { var documentItem = CreateTestDocument(source, "NonIntegerSeqIndices.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - /* First, ensure we can correctly extract counterexamples without crashing... */ var nonIntegralIndexedSeqs = (await RequestCounterExamples(documentItem.Uri)) - .SelectMany(cet => cet.Variables.ToList()) - /* Then, extract the number of non-integral indexed sequences from the repro case... */ + .Select(cet => cet.Assumption) + // Then, extract the number of non-integral indexed sequences from the repro case... .Count(IsNegativeIndexedSeq); // With more recent Z3 versions (at least 4.11+, but maybe going back farther), this situation doesn't seem @@ -1493,24 +1436,12 @@ public async Task NonIntegerSeqIndices(Action optionSettings) { } /* Helper for the NonIntegerSeqIndices test. */ - private static bool IsNegativeIndexedSeq(KeyValuePair kvp) { + private static bool IsNegativeIndexedSeq(string assumption) { var r = new Regex(@"\[\(- \d+\)\]"); - return kvp.Key.Contains("seq<_module.uint8>") && r.IsMatch(kvp.Value); - } - - [Fact] - public void TestIsNegativeIndexedSeq() { - Assert.False( - IsNegativeIndexedSeq(new KeyValuePair("uint8", "42"))); - Assert.False( - IsNegativeIndexedSeq(new KeyValuePair("seq<_module.uint8>", "(Length := 42, [0] := 42)"))); - Assert.True( - IsNegativeIndexedSeq(new KeyValuePair("seq<_module.uint8>", "(Length := 9899, [(- 1)] := 42)"))); - Assert.True( - IsNegativeIndexedSeq(new KeyValuePair("seq>", "(Length := 1123, [(- 12345)] := @12)"))); + return r.IsMatch(assumption); } - [Theory] + [Theory(Skip = "This test should be re-enabled once it is OK to use fully-qualified names everywhere")] [MemberData(nameof(OptionSettings))] public async Task TypePolymorphism(Action optionSettings) { await SetUpOptions(optionSettings); @@ -1525,10 +1456,7 @@ class C { var counterExamples = (await RequestCounterExamples(documentItem.Uri)). OrderBy(counterexample => counterexample.Position).ToArray(); Assert.Single(counterExamples); - Assert.Equal(3, counterExamples[0].Variables.Count); - Assert.True(counterExamples[0].Variables.ContainsKey("a:M.C.Equal$T")); - Assert.True(counterExamples[0].Variables.ContainsKey("b:M.C.Equal$T")); - Assert.True(counterExamples[0].Variables.ContainsKey("this:M.C")); + Assert.Fail("This test needs to be updated so that types in the counterexample can be properly resolved."); } /// diff --git a/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs b/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs index 0ccca4b0bfc..d1aadd9f3bd 100644 --- a/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs +++ b/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs @@ -2,5 +2,14 @@ using System.Collections.Generic; namespace Microsoft.Dafny.LanguageServer.Handlers.Custom { - public record CounterExampleItem(Position Position, IDictionary Variables); + public class CounterExampleItem { + public Position Position { get; } + + public string Assumption { get; } + + public CounterExampleItem(Position position, string assumption) { + Position = position; + Assumption = assumption; + } + } } diff --git a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs index 47e882942c1..20d70713a81 100644 --- a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs @@ -95,7 +95,9 @@ private IEnumerable GetLanguageSpecificModels(IReadOnlyList GetCounterExamples(DafnyModel model) { @@ -104,15 +106,11 @@ private IEnumerable GetCounterExamples(DafnyModel model) { .Select(GetCounterExample); } - private CounterExampleItem GetCounterExample(DafnyModelState state) { - List vars = state.ExpandedVariableSet(counterExampleDepth); + private CounterExampleItem GetCounterExample(PartialState state) { return new( new Position(state.GetLineId() - 1, state.GetCharId()), - vars.WithCancellation(cancellationToken).ToDictionary( - variable => variable.ShortName + ":" + DafnyModelTypeUtils.GetInDafnyFormat(variable.Type), - variable => variable.Value - ) - ); + state.AsAssumption().ToString() + ); } } } diff --git a/Source/DafnyServer/CounterExampleProvider.cs b/Source/DafnyServer/CounterExampleProvider.cs index 6c997c18531..9857cf7d4f0 100644 --- a/Source/DafnyServer/CounterExampleProvider.cs +++ b/Source/DafnyServer/CounterExampleProvider.cs @@ -12,7 +12,6 @@ namespace DafnyServer { public sealed class CounterExampleProvider { - private const int maximumCounterexampleDepth = 5; public readonly string ModelBvd; public CounterExampleProvider() { @@ -68,14 +67,14 @@ private CounterExample ConvertModels(List specificModels) { }; AddLineInformation(counterExampleState, state.FullStateName); - var vars = state.ExpandedVariableSet(maximumCounterexampleDepth); + var vars = state.ExpandedVariableSet(); foreach (var variableNode in vars) { counterExampleState.Variables.Add(new CounterExampleVariable { - Name = variableNode.ShortName, - Value = variableNode.Value, - // CanonicalName is same as Value now but keeping this for legacy - CanonicalName = variableNode.Value + Name = "", + Value = variableNode.ToString(), + // DatatypeConstructorName is same as Value now but keeping this for legacy + CanonicalName = variableNode.ToString() }); } var index = counterExample.States.FindIndex(c => c.Column == counterExampleState.Column && c.Line == counterExampleState.Line); diff --git a/Source/DafnyTestGeneration.Test/BasicTypes.cs b/Source/DafnyTestGeneration.Test/BasicTypes.cs index 19ff2fd62be..11d80d063eb 100644 --- a/Source/DafnyTestGeneration.Test/BasicTypes.cs +++ b/Source/DafnyTestGeneration.Test/BasicTypes.cs @@ -214,7 +214,7 @@ module SimpleTest { Assert.True(methods.All(m => m.ValueCreation.Count == 0)); Assert.True(methods.Exists(m => m.ArgValues[0] == "'B'")); Assert.True(methods.Exists(m => - Regex.IsMatch(m.ArgValues[0], "'[^B]'"))); + Regex.IsMatch(m.ArgValues[0], "'[^B]+'"))); } } diff --git a/Source/DafnyTestGeneration.Test/Collections.cs b/Source/DafnyTestGeneration.Test/Collections.cs index 16e86dec823..740010a0b07 100644 --- a/Source/DafnyTestGeneration.Test/Collections.cs +++ b/Source/DafnyTestGeneration.Test/Collections.cs @@ -35,6 +35,7 @@ module SimpleTest { } else if (|tseq| > 0 && tseq[0].1.1 == 'R') { return 2; } + return 3; } } ".TrimStart(); diff --git a/Source/DafnyTestGeneration/TestMethod.cs b/Source/DafnyTestGeneration/TestMethod.cs index 3dce9938cba..65fedd9fb87 100644 --- a/Source/DafnyTestGeneration/TestMethod.cs +++ b/Source/DafnyTestGeneration/TestMethod.cs @@ -9,6 +9,7 @@ using Microsoft.Boogie; using Microsoft.Dafny; using MapType = Microsoft.Dafny.MapType; +using Token = Microsoft.Dafny.Token; using Type = Microsoft.Dafny.Type; namespace DafnyTestGeneration { @@ -20,7 +21,7 @@ public class TestMethod { // list of values to mock together with their types // maps a variable that is mocked to its unique id - private readonly Dictionary mockedVarId = new(); + private readonly Dictionary mockedVarId = new(); public readonly List<(string parentId, string fieldName, string childId)> Assignments = new(); public readonly List<(string id, Type type, string value)> ValueCreation = new(); // next id to assign to a variable with given name: @@ -44,18 +45,25 @@ public class TestMethod { private List getDefaultValueParams = new(); // similar to above but for objects private readonly HashSet getClassTypeInstanceParams = new(); - private Dictionary defaultValueForType = new(); private readonly Modifications cache; + private readonly Dictionary constraintContext; + public TestMethod(DafnyInfo dafnyInfo, string log, Modifications cache) { DafnyInfo = dafnyInfo; this.cache = cache; var typeNames = ExtractPrintedInfo(log, "Types | "); var argumentNames = ExtractPrintedInfo(log, "Impl | "); dafnyModel = DafnyModel.ExtractModel(dafnyInfo.Options, log); + dafnyModel.AssignConcretePrimitiveValues(); MethodName = argumentNames.First(); argumentNames.RemoveAt(0); NOfTypeArgs = dafnyInfo.GetTypeArgs(MethodName).Count; + constraintContext = new Dictionary(); + foreach (var partialValue in dafnyModel.States.First().KnownVariableNames.Keys) { + constraintContext[partialValue] = new Microsoft.Dafny.IdentifierExpr(Token.NoToken, dafnyModel.States.First().KnownVariableNames[partialValue].First()); + constraintContext[partialValue].Type = partialValue.Type; + } ArgValues = ExtractInputs(dafnyModel.States.First(), argumentNames, typeNames); } @@ -136,9 +144,17 @@ public static string EmitSynthesizeMethods(DafnyInfo dafnyInfo, Modifications ca /// type alone /// the types of the elements /// - private List ExtractInputs(DafnyModelState state, IReadOnlyList printOutput, IReadOnlyList types) { + private List ExtractInputs(PartialState state, IReadOnlyList printOutput, IReadOnlyList types) { var result = new List(); - var vars = state.ExpandedVariableSet(-1); + var vars = state.ExpandedVariableSet(); + var constraintSet = new List(); + foreach (var variable in vars) { + foreach (var constraint in variable.Constraints) { + constraintSet.Add(constraint); + } + } + var constraints = constraintSet.ToList(); + constraints = Constraint.ResolveAndOrder(constraintContext, constraints, false, false); var parameterIndex = DafnyInfo.IsStatic(MethodName) ? -1 : -2; for (var i = 0; i < printOutput.Count; i++) { if (types[i] == "Ty") { @@ -188,8 +204,8 @@ private List ExtractInputs(DafnyModelState state, IReadOnlyList } // Returns a new value of the defaultType type (set to int by default) - private string GetADefaultTypeValue(DafnyModelVariable variable) { - return dafnyModel.GetUnreservedNumericValue(variable.Element, Type.Int); + private string GetADefaultTypeValue(PartialValue variable) { + return "0"; } private string GetFunctionOfType(ArrowType type) { @@ -219,7 +235,7 @@ private Type GetBasicType(Type start, Func stopCondition) { /// Extract the value of a variable. This can have side-effects on /// assignments, reservedValues, reservedValuesMap, and objectsToMock. /// - private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { + private string ExtractVariable(PartialValue variable, Type/*?*/ asType) { if (variable == null) { if (asType != null) { return GetDefaultValue(asType); @@ -238,10 +254,6 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { return mockedVarId[variable]; } - if (variable is DuplicateVariable duplicateVariable) { - return ExtractVariable(duplicateVariable.Original, asType); - } - List elements = new(); var variableType = DafnyModelTypeUtils.GetInDafnyFormat( DafnyModelTypeUtils.ReplaceTypeVariables(variable.Type, defaultType)); @@ -259,18 +271,17 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { case BoolType: case CharType: case BitvectorType: - return GetPrimitiveAsType(variable.Value, asType); + return GetPrimitiveAsType(variable.PrimitiveLiteral, asType); case SeqType seqType: var asBasicSeqType = GetBasicType(asType, type => type is SeqType) as SeqType; - var seqVar = variable as SeqVariable; - if (seqVar?.GetLength() == -1) { + if (variable?.Cardinality() == -1) { if (seqType.Arg is CharType) { return "\"\""; } return AddValue(asType ?? variableType, "[]"); } - for (var i = 0; i < seqVar?.GetLength(); i++) { - var element = seqVar?[i]; + for (var i = 0; i < variable?.Cardinality(); i++) { + var element = variable?[i]; if (element == null) { getDefaultValueParams = new(); elements.Add(GetDefaultValue(seqType.Arg, asBasicSeqType?.TypeArgs?.FirstOrDefault((Type/*?*/)null))); @@ -302,18 +313,14 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { return AddValue(asType ?? variableType, $"[{string.Join(", ", elements)}]"); case SetType: var asBasicSetType = GetBasicType(asType, type => type is SetType) as SetType; - if (!variable.Children.ContainsKey("true")) { - return AddValue(asType ?? variableType, "{}"); - } - foreach (var element in variable.Children["true"]) { + foreach (var element in variable.SetElements()) { elements.Add(ExtractVariable(element, asBasicSetType?.TypeArgs?.FirstOrDefault((Type/*?*/)null))); } return AddValue(asType ?? variableType, $"{{{string.Join(", ", elements)}}}"); case MapType: var asBasicMapType = GetBasicType(asType, type => type is MapType) as MapType; - var mapVar = variable as MapVariable; List mappingStrings = new(); - foreach (var mapping in mapVar?.Mappings ?? new()) { + foreach (var mapping in variable?.Mappings()) { var asTypeTypeArgs = asBasicMapType?.TypeArgs?.Count == 2 ? asBasicMapType.TypeArgs : null; mappingStrings.Add($"{ExtractVariable(mapping.Key, asTypeTypeArgs?[0])} := {ExtractVariable(mapping.Value, asTypeTypeArgs?[1])}"); @@ -321,8 +328,8 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { return AddValue(asType ?? variableType, $"map[{string.Join(", ", mappingStrings)}]"); case UserDefinedType tupleType when tupleType.Name.StartsWith("_tuple#"): return AddValue(asType ?? variableType, "(" + - string.Join(",", variable.Children.Values - .Select(v => ExtractVariable(v.First(), null))) + ")"); + string.Join(",", variable.UnnamedDestructors() + .Select(v => ExtractVariable(v, null))) + ")"); case ArrowType arrowType: var asBasicArrowType = GetBasicType(asType, type => type is ArrowType) as ArrowType; return GetFunctionOfType(asBasicArrowType ?? arrowType); @@ -335,7 +342,7 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { case UserDefinedType arrType when new Regex("^_System.array[0-9]*\\?$").IsMatch(arrType.Name): errorMessages.Add($"// Failed because arrays are not yet supported (type {arrType} element {variable.Element})"); break; - case UserDefinedType _ when variable.CanonicalName() == "null": + case UserDefinedType _ when variable.PrimitiveLiteral != "": return "null"; case UserDefinedType userDefinedType: var basicType = GetBasicType(asType ?? userDefinedType, @@ -346,28 +353,28 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { return GetClassTypeInstance(userDefinedType, asType, variable); } - if (variable.CanonicalName() == "") { + if (variable.DatatypeConstructorName() == "") { getDefaultValueParams = new(); return GetDefaultValue(userDefinedType, asType); } - var ctor = DafnyInfo.Datatypes[basicType.Name].Ctors.FirstOrDefault(ctor => ctor.Name == variable.CanonicalName(), null); + var ctor = DafnyInfo.Datatypes[basicType.Name].Ctors.FirstOrDefault(ctor => ctor.Name == variable.DatatypeConstructorName(), null); if (ctor == null) { - errorMessages.Add($"// Failed: Cannot find constructor {variable.CanonicalName()} for datatype {basicType}"); + errorMessages.Add($"// Failed: Cannot find constructor {variable.DatatypeConstructorName()} for datatype {basicType}"); return basicType.ToString(); } List fields = new(); for (int i = 0; i < ctor.Destructors.Count; i++) { var fieldName = ctor.Destructors[i].Name; - if (!variable.Children.ContainsKey(fieldName)) { + if (!variable.Fields().ContainsKey(fieldName)) { fieldName = $"[{i}]"; } - if (!variable.Children.ContainsKey(fieldName)) { + if (!variable.Fields().ContainsKey(fieldName)) { errorMessages.Add($"// Failed: Cannot find destructor " + $"{ctor.Destructors[i].Name} of constructor " + - $"{variable.CanonicalName()} for datatype " + + $"{variable.DatatypeConstructorName()} for datatype " + $"{basicType}. Available destructors are: " + - string.Join(",", variable.Children.Keys.ToList())); + string.Join(",", variable.Fields().Keys.ToList())); return basicType.ToString(); } @@ -375,18 +382,18 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { Utils.UseFullName(ctor.Destructors[i].Type), ctor.EnclosingDatatype.TypeArgs.ConvertAll(arg => arg.Name), basicType.TypeArgs); if (ctor.Destructors[i].Name.StartsWith("#")) { - fields.Add(ExtractVariable(variable.Children[fieldName].First(), destructorType)); + fields.Add(ExtractVariable(variable.Fields()[fieldName], destructorType)); } else { fields.Add(ctor.Destructors[i].Name + ":=" + - ExtractVariable(variable.Children[fieldName].First(), destructorType)); + ExtractVariable(variable.Fields()[fieldName], destructorType)); } } var value = basicType.ToString(); if (fields.Count == 0) { - value += "." + variable.CanonicalName(); + value += "." + variable.DatatypeConstructorName(); } else { - value += "." + variable.CanonicalName() + "(" + + value += "." + variable.DatatypeConstructorName() + "(" + string.Join(",", fields) + ")"; } return AddValue(asType ?? userDefinedType, value); @@ -395,7 +402,7 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { return "null"; } - private string GetClassTypeInstance(UserDefinedType type, Type/*?*/ asType, DafnyModelVariable/*?*/ variable) { + private string GetClassTypeInstance(UserDefinedType type, Type/*?*/ asType, PartialValue/*?*/ variable) { var asBasicType = GetBasicType(asType, _ => false); if ((asBasicType != null) && (asBasicType is not UserDefinedType)) { return GetDefaultValue(asType, asType); @@ -454,13 +461,12 @@ private string GetClassTypeInstance(UserDefinedType type, Type/*?*/ asType, Dafn return varId; } - private string GetFieldValue((string name, Type type, bool mutable, string/*?*/ defValue) field, DafnyModelVariable/*?*/ variable) { + private string GetFieldValue((string name, Type type, bool mutable, string/*?*/ defValue) field, PartialValue/*?*/ variable) { if (field.defValue != null) { return field.defValue; } - if (variable != null && variable.Children.ContainsKey(field.name) && - variable.Children[field.name].Count == 1) { - return ExtractVariable(variable.Children[field.name].First(), field.type); + if (variable != null && variable.Fields().ContainsKey(field.name)) { + return ExtractVariable(variable.Fields()[field.name], field.type); } var previouslyCreated = ValueCreation.FirstOrDefault(obj => diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect index 6e0c90512a3..cad8bc15090 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect @@ -1,32 +1,21 @@ git-issue-2026.dfy(18,18): Error: this invariant could not be proved to be maintained by the loop Related message: loop invariant violation Related counterexample: + WARNING: the following counterexample may be inconsistent or invalid. See dafny.org/dafny/DafnyRef/DafnyRef#sec-counterexamples + Temporary variables to describe counterexamples: + ghost var counterexampleLoopGuard0 : bool := false; git-issue-2026.dfy(12,0): initial state: - n : int = 2 - ret : ? = ? + assume 2 == n; git-issue-2026.dfy(13,24): - n : int = 2 - ret : _System.array?> = (Length := 2, [0] := @0) - @0 : seq = ['o', 'd', 'd'] + assume ret != null && ret.Length > 0 && 2 == n && 2 == ret.Length && ['o', 'd', 'd'] == ret[0]; git-issue-2026.dfy(15,14): - n : int = 2 - ret : _System.array?> = (Length := 2, [0] := @0) - i : int = 0 - @0 : seq = ['o', 'd', 'd'] + assume ret != null && ret.Length > 0 && 2 == n && 2 == ret.Length && ['o', 'd', 'd'] == ret[0] && 0 == i; git-issue-2026.dfy(16,4): after some loop iterations: - n : int = 2 - ret : _System.array?> = (Length := 2) - i : int = 0 + counterexampleLoopGuard0 := ret != null && 2 == n && 2 == ret.Length && 0 == i; git-issue-2026.dfy(22,27): - n : int = 2 - ret : _System.array?> = (Length := 2, [0] := @0) - i : int = 0 - @0 : seq = ['o', 'd', 'd'] + assume counterexampleLoopGuard0 ==> ret != null && ret.Length > 0 && 2 == n && 2 == ret.Length && ['o', 'd', 'd'] == ret[0] && 0 == i; git-issue-2026.dfy(26,18): - n : int = 2 - ret : _System.array?> = (Length := 2, [0] := @0) - i : int = 1 - @0 : seq = ['o', 'd', 'd'] + assume counterexampleLoopGuard0 ==> ret != null && ret.Length > 0 && 2 == n && 2 == ret.Length && ['o', 'd', 'd'] == ret[0] && 1 == i; Dafny program verifier finished with 0 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample.transcript b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample.transcript deleted file mode 100644 index d6fea106fd2..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample.transcript +++ /dev/null @@ -1,6 +0,0 @@ -# RUN: %server "%s" > "%t" -# RUN: %diff "%s.expect" "%t" - -counterexample -eyJhcmdzIjpbXSwiZmlsZW5hbWUiOiJhYnMuZGZ5Iiwic291cmNlIjoibWV0aG9kIEFicyh4OiBpbnQpIFxyXG4gICAgcmV0dXJucyAoeTogaW50KVxyXG5lbnN1cmVzIHkgPj0gMCB7XHJcbiAgICByZXR1cm4geDtcclxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 -[[DAFNY-CLIENT: EOM]] diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample.transcript.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample.transcript.expect deleted file mode 100644 index 9f68c5dfd27..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample.transcript.expect +++ /dev/null @@ -1,9 +0,0 @@ -# Reading from counterexample.transcript - -Verifying Abs (correctness) ... - [1 proof obligation] error -abs.dfy(4,4): Error: a postcondition could not be proved on this return path -abs.dfy(3,10): Related location: this is the postcondition that could not be proved -COUNTEREXAMPLE_START {"States":[{"Column":0,"Line":0,"Name":"","Variables":[{"CanonicalName":"-1","Name":"x","RealName":null,"Value":"-1"}]},{"Column":15,"Line":3,"Name":"abs.dfy(3,15): initial state","Variables":[{"CanonicalName":"-1","Name":"x","RealName":null,"Value":"-1"}]},{"Column":12,"Line":4,"Name":"abs.dfy(4,12)","Variables":[{"CanonicalName":"-1","Name":"x","RealName":null,"Value":"-1"},{"CanonicalName":"-1","Name":"y","RealName":null,"Value":"-1"}]}]} COUNTEREXAMPLE_END -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy index 71c45e8bb77..d23397890f2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy @@ -19,6 +19,7 @@ module Patterns { s[n] == p[n] || p[n] == '?' { + b := false; var i := 0; while (i < |s|) invariant i <= |s| @@ -27,7 +28,7 @@ module Patterns { p[n] == '?' { if (s[i] != p[i]) { // must add && (p[i] != '?') to verify - return false; + return; } i := i + 1; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect index eb9c2fad072..1a0deba5dfa 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect @@ -1,25 +1,16 @@ -counterexample_commandline.dfy(30,20): Error: a postcondition could not be proved on this return path +counterexample_commandline.dfy(31,20): Error: a postcondition could not be proved on this return path Related counterexample: + WARNING: the following counterexample may be inconsistent or invalid. See dafny.org/dafny/DafnyRef/DafnyRef#sec-counterexamples + Temporary variables to describe counterexamples: + ghost var counterexampleLoopGuard0 : bool := false; counterexample_commandline.dfy(21,8): initial state: - this : Patterns.Simple = (p := @0) - s : seq = ['A'] - @0 : seq = ['?'] + assume this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\U{0002}' == s[0] && 1 == |this.p| && '?' == this.p[0]; counterexample_commandline.dfy(22,22): - this : Patterns.Simple = (p := @0) - s : seq = ['A'] - i : int = 0 - @0 : seq = ['?'] - counterexample_commandline.dfy(23,12): after some loop iterations: - this : Patterns.Simple = (p := @0) - s : seq = ['A'] - i : int = 0 - @0 : seq = ['?'] - counterexample_commandline.dfy(30,32): - this : Patterns.Simple = (p := @0) - s : seq = ['A'] - i : int = 0 - b : bool = false - @0 : seq = ['?'] + assume this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\U{0002}' == s[0] && false == b && 1 == |this.p| && '?' == this.p[0]; + counterexample_commandline.dfy(23,22): + assume this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\U{0002}' == s[0] && false == b && 0 == i && '?' == this.p[0] && 1 == |this.p|; + counterexample_commandline.dfy(24,12): after some loop iterations: + counterexampleLoopGuard0 := this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\U{0002}' == s[0] && false == b && 0 == i && '?' == this.p[0] && 1 == |this.p|; counterexample_commandline.dfy(18,22): Related location: this is the postcondition that could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/git-issue223.transcript b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/git-issue223.transcript deleted file mode 100644 index 7bec0961f2a..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/git-issue223.transcript +++ /dev/null @@ -1,9 +0,0 @@ -# RUN: %server "%s" > "%t" -# RUN: %diff "%s.expect" "%t" - -counterexample -eyJhcmdzIjpbXSwiZmlsZW5hbWUiOiJhYnMuZGZ5Iiwic291cmNlIjoibWV0aG9kIEFicyh4OiBpbnQpIFxyXG4gICAgcmV0dXJucyAoeTogaW50KVxyXG5lbnN1cmVzIHkgPj0gMCB7XHJcbiAgICByZXR1cm4geDtcclxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 -[[DAFNY-CLIENT: EOM]] -counterexample -eyJhcmdzIjpbXSwiZmlsZW5hbWUiOiJhYnMuZGZ5Iiwic291cmNlIjoibWV0aG9kIEFicyh4OiBpbnQpIFxyXG4gICAgcmV0dXJucyAoeTogaW50KVxyXG5lbnN1cmVzIHkgPj0gMCB7XHJcbiAgICByZXR1cm4geDtcclxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 -[[DAFNY-CLIENT: EOM]] diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/git-issue223.transcript.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/git-issue223.transcript.expect deleted file mode 100644 index ceb6bdf0793..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/git-issue223.transcript.expect +++ /dev/null @@ -1,17 +0,0 @@ -# Reading from git-issue223.transcript - -Verifying Abs (correctness) ... - [1 proof obligation] error -abs.dfy(4,4): Error: a postcondition could not be proved on this return path -abs.dfy(3,10): Related location: this is the postcondition that could not be proved -COUNTEREXAMPLE_START {"States":[{"Column":0,"Line":0,"Name":"","Variables":[{"CanonicalName":"-1","Name":"x","RealName":null,"Value":"-1"}]},{"Column":15,"Line":3,"Name":"abs.dfy(3,15): initial state","Variables":[{"CanonicalName":"-1","Name":"x","RealName":null,"Value":"-1"}]},{"Column":12,"Line":4,"Name":"abs.dfy(4,12)","Variables":[{"CanonicalName":"-1","Name":"x","RealName":null,"Value":"-1"},{"CanonicalName":"-1","Name":"y","RealName":null,"Value":"-1"}]}]} COUNTEREXAMPLE_END -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] - -Verifying Abs (correctness) ... - [0 proof obligations] error -abs.dfy(4,4): Error: a postcondition could not be proved on this return path -abs.dfy(3,10): Related location: this is the postcondition that could not be proved -COUNTEREXAMPLE_START {"States":[{"Column":0,"Line":0,"Name":"","Variables":[{"CanonicalName":"-1","Name":"x","RealName":null,"Value":"-1"}]},{"Column":15,"Line":3,"Name":"abs.dfy(3,15): initial state","Variables":[{"CanonicalName":"-1","Name":"x","RealName":null,"Value":"-1"}]},{"Column":12,"Line":4,"Name":"abs.dfy(4,12)","Variables":[{"CanonicalName":"-1","Name":"x","RealName":null,"Value":"-1"},{"CanonicalName":"-1","Name":"y","RealName":null,"Value":"-1"}]}]} COUNTEREXAMPLE_END -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 6e779312294..6ad372623c0 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -1013,6 +1013,13 @@ This list is not exhaustive but can definitely be useful to provide the next ste `method m_mod(i) returns (j: T)`
  ` requires A(i)`
  ` modifies this, i`
  ` ensures B(i, j)`
`{`
  ` ...`
`}`

`method n_mod() {`
  ` ...`




  ` var x := m_mod(a);`
  ` assert P(x);` | `method m_mod(i) returns (j: T)`
  ` requires A(i)`
  ` modifies this, i`
  ` ensures B(i, j)`
`{`
  ` ...`
`}`

`method n_mod() {`
  ` ...`
  ` assert A(k);`
  ` modify this, i; // Temporarily`
  ` var x: T; // Temporarily`
  ` assume B(k, x);`
  `// var x := m_mod(k);`
  ` assert P(x);`
`modify x, y;`
`assert P(x, y, z);` | `assert x != z && y != z;`
`modify x, y;`
`assert P(x, y, z);` +#### 13.7.1.4. Counterexamples {#sec-counterexamples} + +When verification fails, we can rerun Dafny with `--extract-counterexample` flag to get a counterexample that can potentially explain the proof failure. +Note that Danfy cannot guarantee that the counterexample it reports provably violates the assertion it was generated for (see [^smt-encoding]) +The counterexample takes the form of assumptions that can be inserted into the code to describe the potential conditions under which the given assertion is violated. +This output should be inspected manually and treated as a hint. + ### 13.7.2. Verification debugging when verification is slow {#sec-verification-debugging-slow} In this section, we describe techniques to apply in the case when verification is slower than expected, does not terminate, or times out. @@ -2316,6 +2323,12 @@ and what information it produces about the verification process. * `--isolate-assertions` - verify assertions individually +* `--extract-counterexample` - if verification fails, report a potential + counterexample as a set of assumptions that can be inserted into the code. + Note that Danfy cannot guarantee that the counterexample + it reports provably violates the assertion or that the assumptions are not + mutually inconsistent (see [^smt-encoding]), so this output should be inspected manually and treated as a hint. + Controlling the proof engine: * `--cores:` - sets the number or percent of the available cores to be used for verification @@ -2469,13 +2482,6 @@ Legacy options: * `1` (default) - in the body of prefix lemmas, rewrite any use of a focal predicate `P` to `P#[_k-1]`. -* `-extractCounterexample` - control generation of counterexamples. If - verification fails, report a detailed counterexample for the first - failing assertion. Requires specifying the `-mv` option, to specify - where to write the counterexample, as well as the - `-proverOpt:O:model_compress=false` and - `-proverOpt:O:model.completion=true` options. - ### 13.9.8. Controlling compilation {#sec-controlling-compilation} These options control what code gets compiled, what target language is