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