Counterexamples from Command Line (#1511)

* Move position extraction to DafnyModelState

* Move DafnyModel parsing to DafnyModel class

* Add /extractCounterExample option

* Add a lit Test

* Update option description

* Change source location reporting

Co-authored-by: Robin Salkeld <[email protected]>

Author: Dargones

Source/Dafny/DafnyOptions.cs

@@ -102,6 +102,7 @@ public enum IncludesModes { None, Immediate, Transitive }
     public bool ShowSnippets = false;
     public bool WarningsAsErrors = false;
     [CanBeNull] private TestGenerationOptions testGenOptions = null;
+    public bool ExtractCounterExample = false;
 
     public virtual TestGenerationOptions TestGenOptions =>
       testGenOptions ??= new TestGenerationOptions();
@@ -415,6 +416,10 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com
         case "warningsAsErrors":
           WarningsAsErrors = true;
           return true;
+
+        case "extractCounterExample":
+          ExtractCounterExample = true;
+          return true;
       }
 
       // Unless this is an option for test generation, defer to superclass
@@ -867,6 +872,10 @@ or type definitions during translation.
     Read standard input and treat it as an input .dfy file.
 /warningsAsErrors
     Treat warnings as errors.
+/extractCounterExample
+    If verification fails, report a detailed counterexample for the first
+    failing assertion. Requires specifying the /mv option as well as
+    /proverOpt:0:model_compress=false and /proverOpt:0:model.completion=true.
 {TestGenOptions.Help}
 
 Dafny generally accepts Boogie options and passes these on to Boogie. However,

Source/DafnyDriver/DafnyDriver.cs

@@ -11,6 +11,7 @@
 //---------------------------------------------------------------------------------------------
 
 using System.Security;
+using DafnyServer.CounterExampleGeneration;
 using DafnyTestGeneration;
 
 namespace Microsoft.Dafny {
@@ -214,6 +215,12 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(string[] ar
           "*** Error: Only one .dfy file can be specified for testing");
         return CommandLineArgumentsResult.PREPROCESSING_ERROR;
       }
+
+      if (DafnyOptions.O.ExtractCounterExample && DafnyOptions.O.ModelViewFile == null) {
+        ExecutionEngine.printer.ErrorWriteLine(Console.Out,
+          "*** Error: ModelView file must be specified when attempting counterexample extraction");
+        return CommandLineArgumentsResult.PREPROCESSING_ERROR;
+      }
       return CommandLineArgumentsResult.OK;
     }
 
@@ -290,9 +297,32 @@ static ExitValue ProcessFiles(IList<DafnyFile/*!*/>/*!*/ dafnyFiles, ReadOnlyCol
       if (err == null && dafnyProgram != null && DafnyOptions.O.PrintFunctionCallGraph) {
         Util.PrintFunctionCallGraph(dafnyProgram);
       }
+      if (dafnyProgram != null && DafnyOptions.O.ExtractCounterExample && exitValue == ExitValue.VERIFICATION_ERROR) {
+        PrintCounterexample(DafnyOptions.O.ModelViewFile);
+      }
       return exitValue;
     }
 
+    /// <summary>
+    /// Extract the counterexample corresponding to the first failing
+    /// assertion and print it to the console
+    /// </summary>
+    /// <param name="modelViewFile"> Name of the file from which to read
+    /// the counterexample </param> 
+    private static void PrintCounterexample(string modelViewFile) {
+      var model = DafnyModel.ExtractModel(File.ReadAllText(modelViewFile));
+      Console.WriteLine("Counterexample for first failing assertion: ");
+      foreach (var state in model.States.Where(state => !state.IsInitialState)) {
+        Console.WriteLine(state.FullStateName + ":");
+        var vars = state.ExpandedVariableSet(-1);
+        foreach (var variable in vars) {
+          Console.WriteLine($"\t{variable.ShortName} : " +
+                            $"{variable.Type.InDafnyFormat()} = " +
+                            $"{variable.Value}");
+        }
+      }
+    }
+
     private static string BoogieProgramSuffix(string printFile, string suffix) {
       var baseName = Path.GetFileNameWithoutExtension(printFile);
       var dirName = Path.GetDirectoryName(printFile);

Source/DafnyDriver/DafnyDriver.csproj

@@ -17,6 +17,7 @@
   <ItemGroup>
     <ProjectReference Include="..\Dafny\DafnyPipeline.csproj" />
     <ProjectReference Include="..\DafnyTestGeneration\DafnyTestGeneration.csproj" />
+    <ProjectReference Include="..\DafnyServer\DafnyServer.csproj" />
   </ItemGroup>
 
   <ItemGroup>

Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs

@@ -4,7 +4,6 @@
 using Microsoft.Dafny.LanguageServer.Workspace;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
-using System;
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
@@ -76,39 +75,19 @@ private IEnumerable<CounterExampleItem> GetCounterExamples(DafnyModel model) {
         return model.States
           .WithCancellation(cancellationToken)
           .OfType<DafnyModelState>()
-          .Where(state => !IsInitialState(state))
+          .Where(state => !state.IsInitialState)
           .Select(GetCounterExample);
       }
 
-      private static bool IsInitialState(DafnyModelState state) {
-        return state.ShortenedStateName.Equals(InitialStateName);
-      }
-
       private CounterExampleItem GetCounterExample(DafnyModelState state) {
+        HashSet<DafnyModelVariable> vars = state.ExpandedVariableSet(counterExampleDepth);
         return new(
-          GetPositionFromInitialState(state),
-          GetVariablesFromState(state, counterExampleDepth)
-        );
-      }
-
-      private static Position GetPositionFromInitialState(DafnyModelState state) {
-        var match = StatePositionRegex.Match(state.ShortenedStateName);
-        if (!match.Success) {
-          throw new ArgumentException($"state does not contain position: {state.ShortenedStateName}");
-        }
-        // Note: lines in a model start with 1, characters/columns with 0.
-        return new Position(
-          int.Parse(match.Groups["line"].Value) - 1,
-          int.Parse(match.Groups["character"].Value)
-        );
-      }
-
-      private IDictionary<string, string> GetVariablesFromState(DafnyModelState state, int maxDepth) {
-        HashSet<DafnyModelVariable> vars = state.ExpandedVariableSet(maxDepth);
-        return vars.WithCancellation(cancellationToken).ToDictionary(
+          new Position(state.GetLineId() - 1, state.GetCharId()),
+          vars.WithCancellation(cancellationToken).ToDictionary(
             variable => variable.ShortName + ":" + variable.Type.InDafnyFormat(),
             variable => variable.Value
-          );
+          )
+        );
       }
     }
   }

Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs

@@ -4,6 +4,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
 using Microsoft.Boogie;
@@ -80,6 +81,19 @@ public DafnyModel(Model model) {
       }
     }
 
+    /// <summary>
+    /// Extract and parse the first Dafny model recorded in the model view file.
+    /// </summary>
+    public static DafnyModel ExtractModel(string mv) {
+      const string begin = "*** MODEL";
+      const string end = "*** END_MODEL";
+      var beginIndex = mv.IndexOf(begin, StringComparison.Ordinal);
+      var endIndex = mv.IndexOf(end, StringComparison.Ordinal);
+      var modelString = mv.Substring(beginIndex, endIndex + end.Length - beginIndex);
+      var model = Model.ParseModels(new StringReader(modelString)).First();
+      return new DafnyModel(model);
+    }
+
     /// <summary>
     /// Collect the array dimensions from the various array.Length functions,
     /// and collect all known datatype values

Source/DafnyServer/CounterExampleGeneration/DafnyModelState.cs

@@ -4,6 +4,7 @@
 using System;
 using System.Collections.Generic;
 using System.Linq;
+using System.Text.RegularExpressions;
 using Microsoft.Boogie;
 
 namespace DafnyServer.CounterExampleGeneration {
@@ -24,6 +25,12 @@ public class DafnyModelState {
     private readonly Dictionary<Model.Element, DafnyModelVariable> varMap;
     private readonly Dictionary<string, int> varNamesMap;
 
+    private const string InitialStateName = "<initial>";
+    private static Regex statePositionRegex = new(
+      @".*\((?<line>\d+),(?<character>\d+)\)",
+      RegexOptions.IgnoreCase | RegexOptions.Singleline
+    );
+
     public DafnyModelState(DafnyModel model, Model.CapturedState state) {
       Model = model;
       State = state;
@@ -97,6 +104,24 @@ public bool VarNameIsShared(string name) {
 
     public 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);
+    }
+
     /// <summary>
     /// Initialize the vars list, which stores all variables relevant to
     /// the counterexample except for Skolem constants

Source/DafnyTestGeneration/TestMethod.cs

@@ -35,7 +35,7 @@ public TestMethod(DafnyInfo dafnyInfo, string log) {
       DafnyInfo = dafnyInfo;
       var typeNames = ExtractPrintedInfo(log, "Types | ");
       var argumentNames = ExtractPrintedInfo(log, "Impl | ");
-      var dafnyModel = ExtractModel(log);
+      var dafnyModel = DafnyModel.ExtractModel(log);
       MethodName = Utils.GetDafnyMethodName(argumentNames.First());
       argumentNames.RemoveAt(0);
       RegisterReservedValues(dafnyModel.Model);
@@ -314,19 +314,6 @@ private static List<string> ExtractPrintedInfo(string log, string prefix) {
       return new List<string>();
     }
 
-    /// <summary>
-    /// Extract and parse the first Dafny model recorded in the log file.
-    /// </summary>
-    private static DafnyModel ExtractModel(string log) {
-      const string begin = "*** MODEL";
-      const string end = "*** END_MODEL";
-      var beginIndex = log.IndexOf(begin, StringComparison.Ordinal);
-      var endIndex = log.IndexOf(end, StringComparison.Ordinal);
-      var modelString = log.Substring(beginIndex, endIndex + end.Length - beginIndex);
-      var model = Model.ParseModels(new StringReader(modelString)).First();
-      return new DafnyModel(model);
-    }
-
     /// <summary>  Return the test method as a list of lines of code </summary>
     private List<string> TestMethodLines() {
 

Test/server/counterexample_commandline.dfy

@@ -0,0 +1,37 @@
+// RUN: %dafny /compile:0 /proverOpt:O:model_compress=false /proverOpt:O:model.completion=true /warnShadowing /extractCounterExample /errorTrace:0 /mv:%t.model "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// The following method performs string equality comparison whereas its 
+// specification states that it must perform pattern matching (the difference
+// being that the '?' metacharacter in the pattern is supposed to match
+// any character in the string). 
+module Patterns {
+
+    class Simple {
+
+        var p:string;
+
+        method Match(s: string) returns (b: bool) 
+            requires |p| == 1 // this is to make counterexample deterministic
+            requires |p| == |s|
+            ensures b <==> forall n :: 0 <= n < |s| ==> 
+                    s[n] == p[n] || 
+                    p[n] == '?'
+        { 
+            var i := 0;
+            while (i < |s|) 
+                invariant i <= |s|
+                invariant forall n :: 0 <= n < i ==> 
+                    s[n] == p[n] || 
+                    p[n] == '?'
+            {
+                if (s[i] != p[i]) { // must add && (p[i] != '?') to verify
+                    return false;
+                } 
+                i := i + 1;
+            }
+            return true;
+        }
+    }
+
+}

Test/server/counterexample_commandline.dfy.expect

@@ -0,0 +1,25 @@
+counterexample_commandline.dfy(29,20): Error: A postcondition might not hold on this return path.
+counterexample_commandline.dfy(17,22): Related location: This is the postcondition that might not hold.
+
+Dafny program verifier finished with 1 verified, 1 error
+Counterexample for first failing assertion: 
+counterexample_commandline.dfy(20,8): initial state:
+	s : seq<char> = [?#0]
+	this : Patterns.Simple? = (p := @2)
+	@2 : seq<char> = ['?']
+counterexample_commandline.dfy(21,22):
+	s : seq<char> = [?#0]
+	this : Patterns.Simple? = (p := @2)
+	i : int = 0
+	@2 : seq<char> = ['?']
+counterexample_commandline.dfy(22,12): after some loop iterations:
+	s : seq<char> = [?#0]
+	this : Patterns.Simple? = (p := @2)
+	i : int = 0
+	@2 : seq<char> = ['?']
+counterexample_commandline.dfy(29,32):
+	s : seq<char> = [?#0]
+	this : Patterns.Simple? = (p := @2)
+	i : int = 0
+	b : bool = false
+	@2 : seq<char> = ['?']