[Test Generation] Change the set of coverage criteria that can be targeted

Source/DafnyCore/TestGenerationOptions.cs

@@ -8,7 +8,7 @@ public class TestGenerationOptions {
     public const string TestInlineAttribute = "testInline";
     public const string TestEntryAttribute = "testEntry";
     public bool WarnDeadCode = false;
-    public enum Modes { None, Block, Path };
+    public enum Modes { None, Block, CallGraph, Path };
     public Modes Mode = Modes.None;
     public uint SeqLengthLimit = 0;
     [CanBeNull] public string PrintBpl = null;

Source/DafnyTestGeneration.Test/Various.cs

@@ -223,21 +223,12 @@ module Paths {
   method {:testEntry} eightPaths (i:int)
     returns (divBy2:bool, divBy3:bool, divBy5:bool)
   {
-    if (i % 2 == 0) {
-      divBy2 := true;
-    } else {
-      divBy2 := false;
-    }
-    if (i % 3 == 0) {
-      divBy3 := true;
-    } else {
-      divBy3 := false;
-    }
-    if (i % 5 == 0) {
-      divBy5 := true;
-    } else {
-      divBy5 := false;
-    }
+    divBy2 := ifThenElse(i % 2 == 0, true, false);
+    divBy3 := ifThenElse(i % 3 == 0, true, false);
+    divBy5 := ifThenElse(i % 5 == 0, true, false);
+  }
+  predicate {:testInline 1} ifThenElse(condition:bool, thenBranch:bool, elseBranch:bool) {
+    if condition then thenBranch else elseBranch
   }
 }
 ".TrimStart();
@@ -267,30 +258,25 @@ module Paths {
 
     [Theory]
     [MemberData(nameof(OptionSettings))]
-    public async Task BlockBasedTests(List<Action<DafnyOptions>> optionSettings) {
+    public async Task BranchBasedTests(List<Action<DafnyOptions>> optionSettings) {
       var source = @"
 module Paths {
-  method {:testEntry} eightPaths (i:int) returns (divBy2:bool, divBy3:bool, divBy5:bool) {
-    if (i % 2 == 0) {
-      divBy2 := true;
-    } else {
-      divBy2 := false;
-    }
-    if (i % 3 == 0) {
-      divBy3 := true;
-    } else {
-      divBy3 := false;
-    }
-    if (i % 5 == 0) {
-      divBy5 := true;
-    } else {
-      divBy5 := false;
-    }
+  method {:testEntry} eightPaths (i:int)
+    returns (divBy2:bool, divBy3:bool, divBy5:bool)
+  {
+    divBy2 := ifThenElse(i % 2 == 0, true, false);
+    divBy3 := ifThenElse(i % 3 == 0, true, false);
+    divBy5 := ifThenElse(i % 5 == 0, true, false);
+  }
+  predicate {:testInline 1} ifThenElse(condition:bool, thenBranch:bool, elseBranch:bool) {
+    if condition then thenBranch else elseBranch
   }
 }
 ".TrimStart();
       var options = GetDafnyOptions(optionSettings, output);
       var program = Utils.Parse(options, source, false);
+      options.TestGenOptions.Mode =
+        TestGenerationOptions.Modes.CallGraph;
       var methods = await Main.GetTestMethodsForProgram(program).ToListAsync();
       Assert.True(methods.Count is >= 2 and <= 6);
       Assert.True(methods.All(m => m.MethodName == "Paths.eightPaths"));
@@ -309,6 +295,39 @@ module Paths {
       Assert.True(values.Exists(i => i % 5 != 0));
     }
 
+    [Theory]
+    [MemberData(nameof(OptionSettings))]
+    public async Task BlockBasedTests(List<Action<DafnyOptions>> optionSettings) {
+      var source = @"
+module Paths {
+  method {:testEntry} eightPaths (i:int)
+    returns (divBy2:bool, divBy3:bool, divBy5:bool)
+  {
+    divBy2 := ifThenElse(i % 2 == 0, true, false);
+    divBy3 := ifThenElse(i % 3 == 0, true, false);
+    divBy5 := ifThenElse(i % 5 == 0, true, false);
+  }
+  predicate {:testInline 1} ifThenElse(condition:bool, thenBranch:bool, elseBranch:bool) {
+    if condition then thenBranch else elseBranch
+  }
+}
+".TrimStart();
+      var options = GetDafnyOptions(optionSettings, output);
+      var program = Utils.Parse(options, source, false);
+      var methods = await Main.GetTestMethodsForProgram(program).ToListAsync();
+      Assert.True(methods.Count is >= 1 and <= 2);
+      Assert.True(methods.All(m => m.MethodName == "Paths.eightPaths"));
+      Assert.True(methods.All(m => m.DafnyInfo.IsStatic("Paths.eightPaths")));
+      Assert.True(methods.All(m => m.ArgValues.Count == 1));
+      Assert.True(methods.All(m => m.ValueCreation.Count == 0));
+      var values = methods.Select(m =>
+          int.TryParse(m.ArgValues[0], out var result) ? (int?)result : null)
+        .ToList();
+      Assert.True(values.All(i => i != null));
+      Assert.True(values.Exists(i => i % 2 == 0 || i % 3 == 0 || i % 5 == 0));
+      Assert.True(values.Exists(i => i % 2 != 0 || i % 3 != 0 || i % 5 != 0));
+    }
+
     [Theory]
     [MemberData(nameof(OptionSettings))]
     public async Task RecursivelyExtractObjectFields(List<Action<DafnyOptions>> optionSettings) {
@@ -493,9 +512,9 @@ requires a > 0
       var options = GetDafnyOptions(optionSettings, output);
       var program = Utils.Parse(options, source, false);
       options.TestGenOptions.WarnDeadCode = true;
-      var stats = await Main.GetDeadCodeStatistics(program).ToListAsync();
+      var stats = await Main.GetDeadCodeStatistics(program, new Modifications(options)).ToListAsync();
       Assert.Contains(stats, s => s.Contains("(6,14) is potentially unreachable."));
-      Assert.Equal(2, stats.Count); // second is line with stats
+      Assert.Equal(1, stats.Count(line => line.Contains("unreachable"))); // second is line with stats
     }
 
     [Theory]
@@ -513,7 +532,7 @@ public async Task NoDeadCode(List<Action<DafnyOptions>> optionSettings) {
       var options = GetDafnyOptions(optionSettings, output);
       var program = Utils.Parse(options, source, false);
       options.TestGenOptions.WarnDeadCode = true;
-      var stats = await Main.GetDeadCodeStatistics(program).ToListAsync();
+      var stats = await Main.GetDeadCodeStatistics(program, new Modifications(options)).ToListAsync();
       Assert.Single(stats); // the only line with stats
     }
 

Source/DafnyTestGeneration/BlockBasedModifier.cs

@@ -32,8 +32,7 @@ protected override IEnumerable<ProgramModification> GetModifications(Program p)
       if (program == null || implementation == null) {
         return null;
       }
-
-      var state = Utils.GetBlockId(node);
+      var state = Utils.GetBlockId(node, DafnyInfo.Options);
       if (state == null) {
         return null;
       }

Source/DafnyTestGeneration/GenerateTestsCommand.cs

@@ -31,7 +31,8 @@ public class GenerateTestsCommand : ICommandSpec {
 
   private enum Mode {
     Path,
-    Block
+    Block,
+    CallGraph
   }
 
   /// <summary>
@@ -48,8 +49,9 @@ internal static DafnyOptions CopyForProcedure(DafnyOptions options, HashSet<stri
   }
 
   private readonly Argument<Mode> modeArgument = new("mode", @"
-block - Prints block-coverage tests for the given program.
-path - Prints path-coverage tests for the given program.");
+Block - Prints block-coverage tests for the given program.
+CallGraph - Prints call-graph-coverage tests for the given program.
+Path - Prints path-coverage tests for the given program.");
 
   public Command Create() {
     var result = new Command("generate-tests", "(Experimental) Generate Dafny tests that ensure block or path coverage of a particular Dafny program.");
@@ -62,6 +64,7 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo
     var mode = context.ParseResult.GetValueForArgument(modeArgument) switch {
       Mode.Path => TestGenerationOptions.Modes.Path,
       Mode.Block => TestGenerationOptions.Modes.Block,
+      Mode.CallGraph => TestGenerationOptions.Modes.CallGraph,
       _ => throw new ArgumentOutOfRangeException()
     };
     PostProcess(dafnyOptions, options, context, mode);

Source/DafnyTestGeneration/Main.cs

@@ -23,22 +23,21 @@ public static class Main {
     /// loop unrolling may cause false negatives.
     /// </summary>
     /// <returns></returns>
-    public static async IAsyncEnumerable<string> GetDeadCodeStatistics(Program program) {
+    public static async IAsyncEnumerable<string> GetDeadCodeStatistics(Program program, Modifications cache) {
 
       program.Reporter.Options.PrintMode = PrintModes.Everything;
 
-      var cache = new Modifications(program.Options);
-      var modifications = GetModifications(cache, program).ToList();
-      var blocksReached = modifications.Count;
+      var blocksReached = 0;
       HashSet<string> allStates = new();
       HashSet<string> allDeadStates = new();
 
       // Generate tests based on counterexamples produced from modifications
-      for (var i = modifications.Count - 1; i >= 0; i--) {
-        await modifications[i].GetCounterExampleLog(cache);
+      foreach (var modification in GetModifications(cache, program, out _)) {
+        blocksReached++;
+        await modification.GetCounterExampleLog(cache);
         var deadStates = new HashSet<string>();
-        if (!modifications[i].IsCovered(cache)) {
-          deadStates = modifications[i].CapturedStates;
+        if (!modification.IsCovered(cache)) {
+          deadStates = modification.CapturedStates;
         }
 
         if (deadStates.Count != 0) {
@@ -48,10 +47,16 @@ public static async IAsyncEnumerable<string> GetDeadCodeStatistics(Program progr
           blocksReached--;
           allDeadStates.UnionWith(deadStates);
         }
-        allStates.UnionWith(modifications[i].CapturedStates);
+
+        foreach (var state in modification.CapturedStates) {
+          if (!allStates.Contains(state)) {
+            yield return $"Code at {state} is reachable.";
+            allStates.Add(state);
+          }
+        }
       }
 
-      yield return $"Out of {modifications.Count} basic blocks " +
+      yield return $"Out of {blocksReached} basic blocks " +
                    $"({allStates.Count} capturedStates), {blocksReached} " +
                    $"({allStates.Count - allDeadStates.Count}) are reachable. " +
                    "There might be false negatives if you are not unrolling " +
@@ -66,21 +71,27 @@ public static async IAsyncEnumerable<string> GetDeadCodeStatistics(string source
         yield return "Cannot parse program";
         yield break;
       }
-      await foreach (var line in GetDeadCodeStatistics(program)) {
+      if (Utils.ProgramHasAttribute(program,
+            TestGenerationOptions.TestInlineAttribute)) {
+        options.VerifyAllModules = true;
+      }
+      var cache = new Modifications(program.Options);
+      await foreach (var line in GetDeadCodeStatistics(program, cache)) {
         yield return line;
       }
     }
 
-    private static IEnumerable<ProgramModification> GetModifications(Modifications cache, Program program) {
+    private static IEnumerable<ProgramModification> GetModifications(Modifications cache, Program program, out DafnyInfo dafnyInfo) {
       var options = program.Options;
       var success = Inlining.InliningTranslator.TranslateForFutureInlining(program, options, out var boogieProgram);
+      dafnyInfo = null;
       if (!success) {
         options.Printer.ErrorWriteLine(options.ErrorWriter,
           $"Error: Failed at resolving or translating the inlined Dafny code.");
         SetNonZeroExitCode = true;
         return new List<ProgramModification>();
       }
-      var dafnyInfo = new DafnyInfo(program);
+      dafnyInfo = new DafnyInfo(program);
       SetNonZeroExitCode = dafnyInfo.SetNonZeroExitCode || SetNonZeroExitCode;
       if (!Utils.ProgramHasAttribute(program,
             TestGenerationOptions.TestEntryAttribute)) {
@@ -109,11 +120,7 @@ public static async IAsyncEnumerable<TestMethod> GetTestMethodsForProgram(Progra
       // Generate tests based on counterexamples produced from modifications
 
       cache ??= new Modifications(options);
-      var programModifications = GetModifications(cache, program).ToList();
-      // Suppressing error messages which will be printed when dafnyInfo is initialized again in GetModifications
-      var dafnyInfo = new DafnyInfo(program, true);
-      SetNonZeroExitCode = dafnyInfo.SetNonZeroExitCode || SetNonZeroExitCode;
-      foreach (var modification in programModifications) {
+      foreach (var modification in GetModifications(cache, program, out var dafnyInfo)) {
 
         var log = await modification.GetCounterExampleLog(cache);
         if (log == null) {
@@ -125,7 +132,6 @@ public static async IAsyncEnumerable<TestMethod> GetTestMethodsForProgram(Progra
         }
         yield return testMethod;
       }
-      SetNonZeroExitCode = dafnyInfo.SetNonZeroExitCode || SetNonZeroExitCode;
     }
 
     /// <summary>
@@ -177,7 +183,7 @@ string EscapeDafnyStringLiteral(string str) {
           ProgramModification.Status.Failure);
         int queries = failedQueries + cache.ModificationsWithStatus(implementation,
           ProgramModification.Status.Success);
-        int blocks = implementation.Blocks.Where(block => Utils.GetBlockId(block) != block.Label).ToHashSet().Count;
+        int blocks = implementation.Blocks.Where(block => Utils.GetBlockId(block, options) != block.Label).ToHashSet().Count;
         int coveredByCounterexamples = cache.NumberOfBlocksCovered(implementation);
         int coveredByTests = cache.NumberOfBlocksCovered(implementation, onlyIfTestsExists: true);
         yield return $"// Out of {blocks} locations in the " +