From 00b747721c20d48f4dd32f2546c28f733da5edb7 Mon Sep 17 00:00:00 2001 From: Aleksandr Fedchin Date: Mon, 4 Sep 2023 08:59:26 -0700 Subject: [PATCH 01/70] Store Progress --- .../CounterExampleGeneration/DafnyModel.cs | 52 +-- .../DafnyModelState.cs | 233 -------------- .../DafnyModelVariable.cs | 300 ------------------ .../CounterExampleGeneration/PartialState.cs | 197 ++++++++++++ .../CounterExampleGeneration/PartialValue.cs | 84 +++++ .../Custom/DafnyCounterExampleHandler.cs | 4 +- Source/DafnyTestGeneration/TestMethod.cs | 26 +- 7 files changed, 321 insertions(+), 575 deletions(-) delete mode 100644 Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs delete mode 100644 Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelVariable.cs create mode 100644 Source/DafnyLanguageServer/CounterExampleGeneration/PartialState.cs create mode 100644 Source/DafnyLanguageServer/CounterExampleGeneration/PartialValue.cs diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs index 0cb7a6cb420..5be675a9e2f 100644 --- a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs +++ b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs @@ -20,7 +20,7 @@ namespace Microsoft.Dafny.LanguageServer.CounterExampleGeneration { public class DafnyModel { 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, @@ -93,7 +93,7 @@ public DafnyModel(Model model, DafnyOptions options) { RegisterReservedReals(); RegisterReservedBitVectors(); foreach (var s in model.States) { - var sn = new DafnyModelState(this, s); + var sn = new PartialState(this, s); States.Add(sn); } } @@ -565,16 +565,16 @@ public string GetUnreservedNumericValue(Model.Element element, Type numericType) /// /// 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) { + private IEnumerable AddMappingHelper(PartialState state, PartialValue mapVariable, Model.Element keyElement, Model.Element valueElement, HashSet keySet) { if (mapVariable == null) { yield break; } var pairId = mapVariable.Children.Count.ToString(); - var key = DafnyModelVariableFactory.Get(state, keyElement, pairId, mapVariable); + var key = state.GetPartialValue(keyElement, new IdentifierExpr(Token.NoToken, pairId + mapVariable)); if (valueElement != null) { - var value = DafnyModelVariableFactory.Get(state, valueElement, pairId, mapVariable); + var value = state.GetPartialValue(valueElement, new IdentifierExpr(Token.NoToken, pairId + mapVariable)); mapVariable.AddMapping(key, value); yield return value; } else { @@ -589,8 +589,8 @@ private IEnumerable AddMappingHelper(DafnyModelState state, /// values of fields for objects, values at certain positions for /// sequences, etc. /// - public IEnumerable GetExpansion(DafnyModelState state, DafnyModelVariable var) { - HashSet result = new(); + public IEnumerable GetExpansion(PartialState state, PartialValue var) { + HashSet result = new(); if (var.Element.Kind != Model.ElementKind.Uninterpreted) { return result; // primitive types can't have fields } @@ -608,14 +608,14 @@ public IEnumerable GetExpansion(DafnyModelState state, Dafny 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)); + result.Add(state.GetPartialValue(Unbox(func.OptEval(var.Element)), + new IdentifierExpr(Token.NoToken, 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)); + result.Add(state.GetPartialValue(Unbox(fnTuple.Args[i]), + new IdentifierExpr(Token.NoToken, "[" + i + "]" + var))); } } return result; @@ -625,9 +625,9 @@ public IEnumerable GetExpansion(DafnyModelState state, Dafny case SeqType: { var seqLen = fSeqLength.OptEval(var.Element); if (seqLen != null) { - var length = DafnyModelVariableFactory.Get(state, seqLen, "Length", var); + var length = state.GetPartialValue(seqLen, new IdentifierExpr(Token.NoToken, "Length" + var)); result.Add(length); - (var as SeqVariable)?.SetLength(length); + var.SetLength(length); } // Sequences can be constructed with the build operator: @@ -639,9 +639,9 @@ public IEnumerable GetExpansion(DafnyModelState state, Dafny substring = fSeqBuild.AppWithResult(substring).Args[0]; } for (int i = 0; i < elements.Count; i++) { - var e = DafnyModelVariableFactory.Get(state, Unbox(elements[i]), "[" + i + "]", var); + var e = state.GetPartialValue(Unbox(elements[i]), new IdentifierExpr(Token.NoToken, "[" + i + "]" + var)); result.Add(e); - (var as SeqVariable)?.AddAtIndex(e, i.ToString()); + var.AddAtIndex(e, i.ToString()); } if (elements.Count > 0) { return result; @@ -667,9 +667,9 @@ public IEnumerable GetExpansion(DafnyModelState state, Dafny .Concat(otherIndices); foreach (var (res, idx) in sortedIndices) { - var e = DafnyModelVariableFactory.Get(state, res, "[" + idx + "]", var); + var e = state.GetPartialValue(res, new IdentifierExpr(Token.NoToken, "[" + idx + "]"+ var)); result.Add(e); - (var as SeqVariable)?.AddAtIndex(e, idx); + var.AddAtIndex(e, idx); } return result; @@ -682,8 +682,8 @@ public IEnumerable GetExpansion(DafnyModelState state, Dafny continue; } - result.Add(DafnyModelVariableFactory.Get(state, Unbox(setElement), - ((Model.Boolean)containment).ToString(), var)); + result.Add(state.GetPartialValue(Unbox(setElement), + new IdentifierExpr(Token.NoToken, ((Model.Boolean)containment).ToString() + var))); } return result; } @@ -696,7 +696,7 @@ public IEnumerable GetExpansion(DafnyModelState state, Dafny foreach (var mapBuild in mapBuilds.Where(m => m.Args[0] == current && !mapKeysAdded.Contains(m.Args[1]))) { result.UnionWith(AddMappingHelper( state, - var as MapVariable, + var, Unbox(mapBuild.Args[1]), Unbox(mapBuild.Args[2]), mapKeysAdded)); @@ -713,7 +713,7 @@ public IEnumerable GetExpansion(DafnyModelState state, Dafny } result.UnionWith(AddMappingHelper( state, - var as MapVariable, + var, Unbox(nextMapBuild.Args[1]), Unbox(nextMapBuild.Args[2]), mapKeysAdded)); @@ -729,7 +729,7 @@ public IEnumerable GetExpansion(DafnyModelState state, Dafny } result.UnionWith(AddMappingHelper( state, - var as MapVariable, + var, Unbox(app.Args[1]), Unbox(fSetSelect.OptEval(mapElements, app.Args[1])), mapKeysAdded)); @@ -745,8 +745,8 @@ public IEnumerable GetExpansion(DafnyModelState state, Dafny } 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)); + result.Add(state.GetPartialValue(Unbox(field.OptEval(var.Element)), + new IdentifierExpr(Token.NoToken, UnderscoreRemovalRegex.Replace(field.Name.Split(".").Last(), "_") + var))); } var fields = fSetSelect.AppsWithArgs(0, heap, 1, var.Element); if (fields == null || !fields.Any()) { @@ -755,7 +755,7 @@ public IEnumerable GetExpansion(DafnyModelState state, Dafny 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)); + result.Add(state.GetPartialValue(Unbox(tpl.Result), new IdentifierExpr(Token.NoToken, fieldName + var))); } } } diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs deleted file mode 100644 index f7632fb2e2c..00000000000 --- a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs +++ /dev/null @@ -1,233 +0,0 @@ -// Copyright by the contributors to the Dafny Project -// SPDX-License-Identifier: MIT - -#nullable disable - -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text.RegularExpressions; -using Microsoft.Boogie; - -namespace Microsoft.Dafny.LanguageServer.CounterExampleGeneration { - - /// - /// 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 HashSet ExpandedVariableSet(int maxDepth) { - 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(); - 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 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/DafnyLanguageServer/CounterExampleGeneration/DafnyModelVariable.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelVariable.cs deleted file mode 100644 index 8a3073a79ca..00000000000 --- a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelVariable.cs +++ /dev/null @@ -1,300 +0,0 @@ -// Copyright by the contributors to the Dafny Project -// SPDX-License-Identifier: MIT -#nullable disable - -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text.RegularExpressions; -using Microsoft.Boogie; - -namespace Microsoft.Dafny.LanguageServer.CounterExampleGeneration { - - /// - /// 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/DafnyLanguageServer/CounterExampleGeneration/PartialState.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/PartialState.cs new file mode 100644 index 00000000000..aef78a4e838 --- /dev/null +++ b/Source/DafnyLanguageServer/CounterExampleGeneration/PartialState.cs @@ -0,0 +1,197 @@ +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT + +#nullable disable +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text.RegularExpressions; +using Microsoft.Boogie; + +namespace Microsoft.Dafny.LanguageServer.CounterExampleGeneration; + +public class PartialState { + + internal readonly DafnyModel Model; + internal readonly Model.CapturedState State; + private readonly Dictionary values; + private const string InitialStateName = ""; + private static readonly Regex StatePositionRegex = new( + @".*\((?\d+),(?\d+)\)", + RegexOptions.IgnoreCase | RegexOptions.Singleline + ); + + internal PartialValue GetPartialValue(Model.Element element, Expression definition, bool addAsSynonym=false) { + if (!values.ContainsKey(element)) { + values[element] = new PartialValue(element, this, definition); + } else { + values[element].AddDefinition(definition, addAsSynonym); + } + return values[element]; + } + + internal PartialState(DafnyModel model, Model.CapturedState state) { + Model = model; + State = state; + values = new(); + SetupBoundVars(); + 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 HashSet ExpandedVariableSet(int maxDepth) { + 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(); + values.Values.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.GetRelatedValues(). + Where(variable => !expandedSet.Contains(variable) && !variable.IsPrimitive)) { + varsToAdd.Add(new(v, depth + 1)); + } + } + return expandedSet; + } + + /// + /// 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(); + 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. + } + values[val] = GetPartialValue(val, new IdentifierExpr(Token.NoToken, v), true); + } + } + + /// + /// 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; + } + values[f.GetConstant()] = GetPartialValue(f.GetConstant(), new IdentifierExpr(Token.NoToken, name), true); + } + } + + public string FullStateName => State.Name; + + private string ShortenedStateName => ShortenName(State.Name, 20); + + public bool IsInitialState => FullStateName.Equals(InitialStateName); + + 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 res.Line) || + !int.TryParse(words[1], out res.Column)) { + return null; + } + int colon = name.IndexOf(':', par); + res.AddInfo = colon > 0 ? name[(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/DafnyLanguageServer/CounterExampleGeneration/PartialValue.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/PartialValue.cs new file mode 100644 index 00000000000..d48ac0811bf --- /dev/null +++ b/Source/DafnyLanguageServer/CounterExampleGeneration/PartialValue.cs @@ -0,0 +1,84 @@ +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT + +#nullable disable +using System.Collections.Generic; +using Dafny; +using Microsoft.Boogie; + +namespace Microsoft.Dafny.LanguageServer.CounterExampleGeneration; + +public class PartialValue { + + public readonly Model.Element Element; // the element in the counterexample model associated with the value + private HashSet constraints; // constraints imposed on this value + private Expression definition; // a deterministic expression that can be used to name this value + private HashSet synonyms; + private readonly PartialState state; // corresponding state in the counterexample model + private bool constraintsGathered; + + public bool HasDefinition => definition != null; + + internal PartialValue(Model.Element element, PartialState state, Expression definition=null) { + Element = element; + this.state = state; + this.definition = definition; // TODO: what to do when definition is replaced? + constraints = new(); + synonyms = new(); + constraintsGathered = false; + } + + public IEnumerable GetRelatedValues() { + GatherConstraints(); + return Sequence.Empty; // TODO + } + + public void GatherConstraints() { + if (constraintsGathered) { + return; + } + // TODO + } + + internal void AddDefinition(Expression definition, bool addAsSynonym=false) { + if (!HasDefinition) { + this.definition = definition; + } else if (addAsSynonym) { + synonyms.Add(definition); + } + constraints.Add(definition); + } + + public bool IsPrimitive => false; // TODO + + public string ShortName => ""; // TODO + + public Type Type => Type.Int; // TODO + + public string Value => ""; // TODO + + public Dictionary> Children => new(); // TODO + + public string CanonicalName() => ""; // TODO + + public Dictionary Mappings = new(); // TODO + + public int GetLength() => 0; // TODO + + + public PartialValue this[int i] { + get { throw new System.NotImplementedException(); } // TODO + } + + public void AddAtIndex(object p0, string idx) { + throw new System.NotImplementedException(); + } + + public void SetLength(object length) { + throw new System.NotImplementedException(); + } + + public void AddMapping(object key, object p1) { + throw new System.NotImplementedException(); + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs index ac55cdfadd9..2593bbcad11 100644 --- a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs @@ -92,8 +92,8 @@ private IEnumerable GetCounterExamples(DafnyModel model) { .Select(GetCounterExample); } - private CounterExampleItem GetCounterExample(DafnyModelState state) { - HashSet vars = state.ExpandedVariableSet(counterExampleDepth); + private CounterExampleItem GetCounterExample(PartialState state) { + HashSet vars = state.ExpandedVariableSet(counterExampleDepth); return new( new Position(state.GetLineId() - 1, state.GetCharId()), vars.WithCancellation(cancellationToken).ToDictionary( diff --git a/Source/DafnyTestGeneration/TestMethod.cs b/Source/DafnyTestGeneration/TestMethod.cs index 9250c8eacc7..03b4ad0cf12 100644 --- a/Source/DafnyTestGeneration/TestMethod.cs +++ b/Source/DafnyTestGeneration/TestMethod.cs @@ -21,7 +21,7 @@ public class TestMethod { // list of values to mock together with their types // maps a variable that is mocked to its unique id - private readonly Dictionary mockedVarId = new(); + private readonly Dictionary mockedVarId = new(); public readonly List<(string parentId, string fieldName, string childId)> Assignments = new(); public readonly List<(string id, Type type, string value)> ValueCreation = new(); // next id to assign to a variable with given name: @@ -142,7 +142,7 @@ public static string EmitSynthesizeMethods(DafnyInfo dafnyInfo) { /// type alone /// the types of the elements /// - private List ExtractInputs(DafnyModelState state, IReadOnlyList printOutput, IReadOnlyList types) { + private List ExtractInputs(PartialState state, IReadOnlyList printOutput, IReadOnlyList types) { var result = new List(); var vars = state.ExpandedVariableSet(-1); var parameterIndex = DafnyInfo.IsStatic(MethodName) ? -1 : -2; @@ -194,7 +194,7 @@ private List ExtractInputs(DafnyModelState state, IReadOnlyList } // Returns a new value of the defaultType type (set to int by default) - private string GetADefaultTypeValue(DafnyModelVariable variable) { + private string GetADefaultTypeValue(PartialValue variable) { return dafnyModel.GetUnreservedNumericValue(variable.Element, Type.Int); } @@ -225,7 +225,7 @@ private Type GetBasicType(Type start, Func stopCondition) { /// Extract the value of a variable. This can have side-effects on /// assignments, reservedValues, reservedValuesMap, and objectsToMock. /// - private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { + private string ExtractVariable(PartialValue variable, Type/*?*/ asType) { if (variable == null) { if (asType != null) { return GetDefaultValue(asType); @@ -244,9 +244,9 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { return mockedVarId[variable]; } - if (variable is DuplicateVariable duplicateVariable) { + /*if (variable is DuplicateVariable duplicateVariable) { return ExtractVariable(duplicateVariable.Original, asType); - } + }*/ // TODO: Is there any new form of duplication? List elements = new(); var variableType = DafnyModelTypeUtils.GetInDafnyFormat( @@ -268,15 +268,14 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { return GetPrimitiveAsType(variable.Value, asType); case SeqType seqType: var asBasicSeqType = GetBasicType(asType, type => type is SeqType) as SeqType; - var seqVar = variable as SeqVariable; - if (seqVar?.GetLength() == -1) { + if (variable?.GetLength() == -1) { if (seqType.Arg is CharType) { return "\"\""; } return AddValue(asType ?? variableType, "[]"); } - for (var i = 0; i < seqVar?.GetLength(); i++) { - var element = seqVar?[i]; + for (var i = 0; i < variable?.GetLength(); i++) { + var element = variable?[i]; if (element == null) { getDefaultValueParams = new(); elements.Add(GetDefaultValue(seqType.Arg, asBasicSeqType?.TypeArgs?.FirstOrDefault((Type/*?*/)null))); @@ -317,9 +316,8 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { return AddValue(asType ?? variableType, $"{{{string.Join(", ", elements)}}}"); case MapType: var asBasicMapType = GetBasicType(asType, type => type is MapType) as MapType; - var mapVar = variable as MapVariable; List mappingStrings = new(); - foreach (var mapping in mapVar?.Mappings ?? new()) { + foreach (var mapping in variable?.Mappings ?? new()) { var asTypeTypeArgs = asBasicMapType?.TypeArgs?.Count == 2 ? asBasicMapType.TypeArgs : null; mappingStrings.Add($"{ExtractVariable(mapping.Key, asTypeTypeArgs?[0])} := {ExtractVariable(mapping.Value, asTypeTypeArgs?[1])}"); @@ -401,7 +399,7 @@ private string ExtractVariable(DafnyModelVariable variable, Type/*?*/ asType) { return "null"; } - private string GetClassTypeInstance(UserDefinedType type, Type/*?*/ asType, DafnyModelVariable/*?*/ variable) { + private string GetClassTypeInstance(UserDefinedType type, Type/*?*/ asType, PartialValue/*?*/ variable) { var asBasicType = GetBasicType(asType, _ => false); if ((asBasicType != null) && (asBasicType is not UserDefinedType)) { return GetDefaultValue(asType, asType); @@ -460,7 +458,7 @@ private string GetClassTypeInstance(UserDefinedType type, Type/*?*/ asType, Dafn return varId; } - private string GetFieldValue((string name, Type type, bool mutable, string/*?*/ defValue) field, DafnyModelVariable/*?*/ variable) { + private string GetFieldValue((string name, Type type, bool mutable, string/*?*/ defValue) field, PartialValue/*?*/ variable) { if (field.defValue != null) { return field.defValue; } From cc874dc02779bf783d3db43ff972aa9f7b74c45e Mon Sep 17 00:00:00 2001 From: Aleksandr Fedchin Date: Wed, 25 Oct 2023 10:35:28 -0700 Subject: [PATCH 02/70] minor changes --- .../CounterExampleGeneration/DafnyModel.cs | 22 ++++++++++++++----- .../ModelFuncWrapper.cs | 2 +- .../CounterExampleGeneration/PartialValue.cs | 2 ++ 3 files changed, 19 insertions(+), 7 deletions(-) diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs index 5be675a9e2f..2e1c852dff1 100644 --- a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs +++ b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs @@ -297,12 +297,22 @@ internal Type GetDafnyType(Model.Element element) { return result; } + public void GetExpansion(PartialState state, PartialValue value) { + foreach (var funcTuple in value.Element.References) { + if (funcTuple.Func == fSeqLength.func) { + + } else if (funcTuple.Func == fIs.func) { + + } // etc. + } + } + /// /// 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) /// - private Type GetDafnyType(Model.Uninterpreted element) { + /*private Type GetDafnyType(Model.Uninterpreted element) { var finalResult = UnknownType; foreach (var typeElement in GetIsResults(element)) { var reconstructedType = ReconstructType(typeElement); @@ -366,7 +376,7 @@ private Type GetDafnyType(Model.Uninterpreted element) { } var dtypeElement = fDtype.OptEval(element); return dtypeElement != null ? ReconstructType(dtypeElement) : finalResult; - } + }*/ /// /// Reconstruct Dafny type from an element that represents a type in Z3 @@ -439,7 +449,7 @@ private Type ReconstructType(Model.Element typeElement) { /// 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) { + /*public string CanonicalName(Model.Element elt, Type type) { if (elt == null || (type is UserDefinedType userDefinedType && userDefinedType.Name == UnknownType.Name)) { return "?"; } @@ -504,7 +514,7 @@ public string CanonicalName(Model.Element elt, Type type) { default: return ""; } - } + }*/ /// /// Find a char value that is different from any other value @@ -589,7 +599,7 @@ private IEnumerable AddMappingHelper(PartialState state, PartialVa /// values of fields for objects, values at certain positions for /// sequences, etc. /// - public IEnumerable GetExpansion(PartialState state, PartialValue var) { + /*public IEnumerable GetExpansion(PartialState state, PartialValue var) { HashSet result = new(); if (var.Element.Kind != Model.ElementKind.Uninterpreted) { return result; // primitive types can't have fields @@ -760,7 +770,7 @@ public IEnumerable GetExpansion(PartialState state, PartialValue v } } return result; - } + }*/ /// /// Return all functions mapping an object to a destructor value. diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/ModelFuncWrapper.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/ModelFuncWrapper.cs index a6747f8b92e..1b9cfa37153 100644 --- a/Source/DafnyLanguageServer/CounterExampleGeneration/ModelFuncWrapper.cs +++ b/Source/DafnyLanguageServer/CounterExampleGeneration/ModelFuncWrapper.cs @@ -21,7 +21,7 @@ namespace Microsoft.Dafny.LanguageServer.CounterExampleGeneration; /// class ModelFuncWrapper { - private readonly Model.Func func; + public readonly Model.Func func; private readonly int argsToSkip; public ModelFuncWrapper(DafnyModel model, string name, int arity, int argsToSkip) { diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/PartialValue.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/PartialValue.cs index d48ac0811bf..286fc9a17c3 100644 --- a/Source/DafnyLanguageServer/CounterExampleGeneration/PartialValue.cs +++ b/Source/DafnyLanguageServer/CounterExampleGeneration/PartialValue.cs @@ -37,6 +37,8 @@ public void GatherConstraints() { if (constraintsGathered) { return; } + state.Model.GetExpansion(state, this); + constraintsGathered = true; // TODO } From 1be23887353ae0771bd0bb287097b5a78e655952 Mon Sep 17 00:00:00 2001 From: Aleksandr Fedchin Date: Thu, 16 Nov 2023 04:30:18 -0800 Subject: [PATCH 03/70] Counterexample parity for extension vs command line --- Source/DafnyCore/DafnyConsolePrinter.cs | 5 ++- Source/DafnyCore/DafnyOptions.cs | 13 ++++-- Source/DafnyCore/Options/CommonOptionBag.cs | 15 ++++++- Source/DafnyCore/Options/DafnyCommands.cs | 3 +- Source/DafnyDriver/CompilerDriver.cs | 40 +++++++++++-------- Source/DafnyLanguageServer/LanguageServer.cs | 7 ---- .../ProgramModification.cs | 19 --------- .../server/counterexample_commandline.dfy | 2 +- .../counterexample_commandline.dfy.expect | 21 +--------- 9 files changed, 53 insertions(+), 72 deletions(-) diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index 87744bb3028..64da91b90a6 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/Source/DafnyCore/DafnyConsolePrinter.cs @@ -35,13 +35,14 @@ public record VerificationResultLogEntry( ConditionGeneration.Outcome Outcome, TimeSpan RunTime, int ResourceCount, - List VCResults); + List VCResults, + List Counterexamples); public record ConsoleLogEntry(ImplementationLogEntry Implementation, VerificationResultLogEntry Result); public static VerificationResultLogEntry DistillVerificationResult(VerificationResult verificationResult) { return new VerificationResultLogEntry( verificationResult.Outcome, verificationResult.End - verificationResult.Start, - verificationResult.ResourceCount, verificationResult.VCResults.Select(DistillVCResult).ToList()); + verificationResult.ResourceCount, verificationResult.VCResults.Select(DistillVCResult).ToList(), verificationResult.Errors); } private static VCResultLogEntry DistillVCResult(VCResult r) { diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 9e273019b37..49d0d04205b 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -729,6 +729,7 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p case "extractCounterexample": ExtractCounterexample = true; + EnhancedErrorMessages = 1; return true; case "verificationLogger": @@ -1148,6 +1149,13 @@ public void SetZ3Options(Version z3Version) { SetZ3Option("type_check", "true"); SetZ3Option("smt.qi.eager_threshold", "100"); // TODO: try lowering SetZ3Option("smt.delay_units", "true"); + SetZ3Option("model_evaluator.completion", "true"); + SetZ3Option("model.completion", "true"); + if (z3Version is null || z3Version < new Version(4, 8, 6)) { + SetZ3Option("model_compress", "false"); + } else { + SetZ3Option("model.compact", "false"); + } // This option helps avoid "time travelling triggers". // See: https://github.com/dafny-lang/dafny/discussions/3362 @@ -1419,10 +1427,7 @@ focal predicate P to P#[_k-1]. /extractCounterexample If verification fails, report a detailed counterexample for the - first failing assertion. Requires specifying the /mv: option as well - as /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or - /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and - /proverOpt:O:model.completion=true. + first failing assertion (experimental). ---- Compilation options --------------------------------------------------- diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 3f23b1a1dc5..2428d5dbe3e 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -291,6 +291,11 @@ Allow Dafny code to depend on the standard libraries included with the Dafny dis Not compatible with the --unicode-char:false option. "); + public static readonly Option ExtractCounterexample = new("--extract-counterexample", () => false, + @" +If verification fails, report a detailed counterexample for the first failing assertion (experimental).".TrimStart()) { + }; + static CommonOptionBag() { DafnyOptions.RegisterLegacyUi(Target, DafnyOptions.ParseString, "Compilation options", "compileTarget", @" cs (default) - Compile to .NET via C#. @@ -475,6 +480,11 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, } }); + DafnyOptions.RegisterLegacyBinding(ExtractCounterexample, (options, value) => { + options.ExtractCounterexample = value; + options.EnhancedErrorMessages = 1; + }); + DooFile.RegisterLibraryChecks( new Dictionary() { { UnicodeCharacters, DooFile.CheckOptionMatches }, @@ -522,8 +532,9 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, OptimizeErasableDatatypeWrapper, AddCompileSuffix, SystemModule, - ExecutionCoverageReport - ); + ExecutionCoverageReport, + ExtractCounterexample + ); } public static readonly Option FormatPrint = new("--print", diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index 28edb04304f..865537e26e2 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -43,7 +43,8 @@ static DafnyCommands() { CommonOptionBag.WarnContradictoryAssumptions, CommonOptionBag.WarnRedundantAssumptions, CommonOptionBag.NoTimeStampForCoverageReport, - CommonOptionBag.VerificationCoverageReport + CommonOptionBag.VerificationCoverageReport, + CommonOptionBag.ExtractCounterexample }.ToList(); public static IReadOnlyList