diff --git a/Source/DafnyCore/TestGenerationOptions.cs b/Source/DafnyCore/TestGenerationOptions.cs index 02a40421821..a44d7f03e43 100644 --- a/Source/DafnyCore/TestGenerationOptions.cs +++ b/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; diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs index b932046bb11..8d6237b43f9 100644 --- a/Source/DafnyTestGeneration.Test/Various.cs +++ b/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> optionSettings) { + public async Task BranchBasedTests(List> 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> 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> 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> 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 } diff --git a/Source/DafnyTestGeneration/BlockBasedModifier.cs b/Source/DafnyTestGeneration/BlockBasedModifier.cs index 1f44b212c6e..0e388ee8a16 100644 --- a/Source/DafnyTestGeneration/BlockBasedModifier.cs +++ b/Source/DafnyTestGeneration/BlockBasedModifier.cs @@ -32,8 +32,7 @@ protected override IEnumerable 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; } diff --git a/Source/DafnyTestGeneration/GenerateTestsCommand.cs b/Source/DafnyTestGeneration/GenerateTestsCommand.cs index fd20c745353..4343e945a41 100644 --- a/Source/DafnyTestGeneration/GenerateTestsCommand.cs +++ b/Source/DafnyTestGeneration/GenerateTestsCommand.cs @@ -31,7 +31,8 @@ public class GenerateTestsCommand : ICommandSpec { private enum Mode { Path, - Block + Block, + CallGraph } /// @@ -48,8 +49,9 @@ internal static DafnyOptions CopyForProcedure(DafnyOptions options, HashSet 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); diff --git a/Source/DafnyTestGeneration/Main.cs b/Source/DafnyTestGeneration/Main.cs index 12468c93144..1885fd6347e 100644 --- a/Source/DafnyTestGeneration/Main.cs +++ b/Source/DafnyTestGeneration/Main.cs @@ -23,22 +23,21 @@ public static class Main { /// loop unrolling may cause false negatives. /// /// - public static async IAsyncEnumerable GetDeadCodeStatistics(Program program) { + public static async IAsyncEnumerable 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 allStates = new(); HashSet 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(); - 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 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 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 GetModifications(Modifications cache, Program program) { + private static IEnumerable 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(); } - 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 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 GetTestMethodsForProgram(Progra } yield return testMethod; } - SetNonZeroExitCode = dafnyInfo.SetNonZeroExitCode || SetNonZeroExitCode; } /// @@ -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 " + diff --git a/Source/DafnyTestGeneration/PathBasedModifier.cs b/Source/DafnyTestGeneration/PathBasedModifier.cs index 7d9fca8d690..7c177e54a97 100644 --- a/Source/DafnyTestGeneration/PathBasedModifier.cs +++ b/Source/DafnyTestGeneration/PathBasedModifier.cs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: MIT #nullable disable +using System; using System.Collections.Generic; using System.Linq; using Microsoft.Boogie; @@ -23,54 +24,61 @@ public class PathBasedModifier : ProgramModifier { // prefix given to variables indicating whether or not a block was visited private const string BlockVarNamePrefix = "block"; - private List paths = new(); + // Dafny will try to generate tests for paths through the program of increasingly greater length, + // PathLengthStep determines the increments by which Dafny should increase maximum path length in-between attempts + private const int PathLengthStep = 5; public PathBasedModifier(Modifications modifications) { this.modifications = modifications; } protected override IEnumerable GetModifications(Program p) { - paths = new List(); - VisitProgram(p); // populates paths - foreach (var path in paths) { - path.AssertPath(); - var testEntryNames = Utils.DeclarationHasAttribute(path.Impl, TestGenerationOptions.TestInlineAttribute) - ? TestEntries - : new() { path.Impl.VerboseName }; - yield return modifications.GetProgramModification(p, path.Impl, new HashSet(), testEntryNames, - $"{path.Impl.VerboseName.Split(" ")[0]}" + path.name); - path.NoAssertPath(); - } - } - - private void VisitProgram(Program node) { - foreach (var implementation in node.Implementations) { - VisitImplementation(implementation); - } - } + foreach (var implementation in p.Implementations) { + if (!ImplementationIsToBeTested(implementation) || + !DafnyInfo.IsAccessible(implementation.VerboseName.Split(" ")[0])) { + continue; + } - /// - /// Insert variables to register which blocks are visited - /// and then populate the paths field. - /// - private void VisitImplementation(Implementation node) { - if (!ImplementationIsToBeTested(node) || - !DafnyInfo.IsAccessible(node.VerboseName.Split(" ")[0])) { - return; + int pathLength = PathLengthStep; + bool newPathsFound = true; + // Consider paths of increasing length, pruning out infeasible sub-paths in the process: + while (newPathsFound) { + List pathsToConsider = new(); // paths without known unfeasible subpaths + var totalPaths = 0; + foreach (var path in GeneratePaths(implementation, pathLength - PathLengthStep, pathLength)) { + totalPaths++; + var pathId = path.ToString(DafnyInfo.Options); + if (pathLength <= PathLengthStep || !modifications.Values.Any(modification => + pathId.StartsWith(modification.uniqueId) && + modification.CounterexampleStatus == ProgramModification.Status.Failure)) { + pathsToConsider.Add(path); + } + } + newPathsFound = pathsToConsider.Count() != 0; + if (DafnyInfo.Options.Verbose) { + Console.Out.WriteLine( + $"// Now considering paths of length {pathLength - PathLengthStep} to {pathLength} for {implementation.VerboseName}"); + Console.Out.WriteLine($"// Maximum number of feasible paths of this length is {pathsToConsider.Count} out of {totalPaths} total"); + } + foreach (var path in pathsToConsider) { + path.AssertPath(); + var testEntryNames = Utils.DeclarationHasAttribute(path.Impl, TestGenerationOptions.TestInlineAttribute) + ? TestEntries + : new() { path.Impl.VerboseName }; + yield return modifications.GetProgramModification(p, path.Impl, new HashSet(), testEntryNames, + path.ToString(DafnyInfo.Options)); + path.NoAssertPath(); + } + pathLength += PathLengthStep; + } } - var blockToVariable = InitBlockVars(node); - GeneratePaths(node, - blockToVariable, - node.Blocks[0], - new HashSet(), - new List()); } /// /// Modify implementation by adding variables indicating whether or not /// certain blocks were visited. /// - internal static Dictionary InitBlockVars(Implementation node) { + private static Dictionary InitBlockVars(Implementation node) { var blockToVariable = new Dictionary(); foreach (var block in node.Blocks) { var varName = BlockVarNamePrefix + block.UniqueId; @@ -90,55 +98,92 @@ internal static Dictionary InitBlockVars(Implementation node) { } /// - /// Populate paths field with paths generated for the given implementation + /// Iterate over paths through an implementation in a depth-first search fashion /// - /// implementation to generate paths for - /// maps block to flag variables - /// block with which to start AST traversal - /// set of block already inside the path - /// the blocks forming the path - private void GeneratePaths(Implementation impl, - Dictionary blockToVariable, Block block, - HashSet currSet, List currList) { - if (currSet.Contains(blockToVariable[block])) { - return; - } - - // if the block contains a return command, it is the last one in the path: - if (block.TransferCmd is ReturnCmd) { - paths.Add(new Path(impl, currSet.ToList(), block, - $"(path through {string.Join(",", currList.ConvertAll(Utils.GetBlockId).Where(id => id != null))},{Utils.GetBlockId(block) ?? ""})")); - return; - } - - // otherwise, each goto statement presents a new path to take: - currSet.Add(blockToVariable[block]); - currList.Add(block); - var gotoCmd = block.TransferCmd as GotoCmd; - foreach (var b in gotoCmd?.labelTargets ?? new List()) { - GeneratePaths(impl, blockToVariable, b, currSet, currList); + private IEnumerable GeneratePaths(Implementation impl, int minPathLength, int maxPathLength) { + List currPath = new(); // list of basic blocks along the current path + // remember alternative paths that could have been taken at every goto: + List> otherGotos = new() { new() }; + // set of boolean variables indicating that blocks in currPath list have been visited: + HashSet currPathVariables = new(); + var blockToVariable = InitBlockVars(impl); + var block = impl.Blocks[0]; + while (block != null) { + if ((block.TransferCmd is ReturnCmd && currPath.Count >= minPathLength) || currPath.Count == maxPathLength - 1) { + yield return new Path(impl, currPathVariables.ToList(), new() { block }, + currPath.Append(block).ToList()); + } else { + if (currPath.Count != 0 && ((GotoCmd)currPath.Last().TransferCmd).labelTargets.Count != 1) { + currPathVariables.Add(blockToVariable[block]); // only constrain the path if there is more than one goto + } + currPath.Add(block); + otherGotos.Add(new List()); + var gotoCmd = block.TransferCmd as GotoCmd; + foreach (var nextBlock in gotoCmd?.labelTargets ?? new List()) { + if (currPathVariables.Contains(blockToVariable[nextBlock])) { // this prevents cycles + continue; + } + otherGotos.Last().Add(nextBlock); + } + if (otherGotos.Last().Count > 0) { + block = otherGotos.Last().First(); + continue; + } + } + var options = otherGotos.Last(); + while (otherGotos.Count > 1 && options.Count <= 1) { + currPathVariables.Remove(blockToVariable[currPath.Last()]); + currPath.RemoveAt(currPath.Count - 1); + otherGotos.RemoveAt(otherGotos.Count - 1); + options = otherGotos.Last(); + } + if (options.Count <= 1) { + block = null; + continue; + } + options.RemoveAt(0); + block = options.First(); } - currList.RemoveAt(currList.Count - 1); - currSet.Remove(blockToVariable[block]); } - internal class Path { + private class Path { - internal string name; public readonly Implementation Impl; - public readonly List path; // flags for the blocks along the path + private readonly List path; // flags for the blocks along the path private readonly List returnBlocks; // block(s) where the path ends + private readonly List pathBlocks; - internal Path(Implementation impl, IEnumerable path, Block returnBlock, string name) - : this(impl, path, new List() { returnBlock }, name) { - } - - internal Path(Implementation impl, IEnumerable path, List returnBlocks, string name) { + internal Path(Implementation impl, IEnumerable path, List returnBlocks, List pathBlocks) { Impl = impl; this.path = new(); this.path.AddRange(path); // deepcopy is necessary here this.returnBlocks = returnBlocks; - this.name = name; + this.pathBlocks = pathBlocks; + } + + public string ToString(DafnyOptions options) { + return $"{Impl.VerboseName.Split(" ")[0]} path through " + + $"{string.Join(",", pathBlocks.ConvertAll(block => Utils.GetBlockId(block, options) ?? block.UniqueId.ToString()))}"; + } + + /// + /// Constructs a binary tree of disjunctions made up of + /// This limits the depth of the resulting AST and prevents stack overflow during verification for large trees + /// + private Expr ConstructDisjunction(List clauses) { + if (clauses.Count >= 2) { + int mid = clauses.Count / 2; + return new NAryExpr(new Token(), + new BinaryOperator(new Token(), BinaryOperator.Opcode.Or), + new List() { + ConstructDisjunction(clauses.GetRange(0, mid)), + ConstructDisjunction(clauses.GetRange(mid, clauses.Count - mid)) + }); + } + if (clauses.Count == 1) { + return clauses[0]; + } + return new LiteralExpr(new Token(), true); } internal void AssertPath() { @@ -149,13 +194,8 @@ internal void AssertPath() { } } - Expr condition = new IdentifierExpr(new Token(), path[0]); - for (int i = 1; i < path.Count(); i++) { - condition = new NAryExpr(new Token(), - new BinaryOperator(new Token(), BinaryOperator.Opcode.Or), - new List() - { condition, new IdentifierExpr(new Token(), path[i]) }); - } + var condition = + ConstructDisjunction(path.Select(variable => new IdentifierExpr(new Token(), variable) as Expr).ToList()); foreach (var returnBlock in returnBlocks) { returnBlock.cmds.Add(new AssertCmd(new Token(), condition)); diff --git a/Source/DafnyTestGeneration/ProgramModification.cs b/Source/DafnyTestGeneration/ProgramModification.cs index 1d5376b5a55..ce26f60f5ea 100644 --- a/Source/DafnyTestGeneration/ProgramModification.cs +++ b/Source/DafnyTestGeneration/ProgramModification.cs @@ -31,12 +31,19 @@ public ProgramModification GetProgramModification(Program program, return idToModification[uniqueId]; } + public ProgramModification GetProgramModification(string uniqueId) { + if (!idToModification.ContainsKey(uniqueId)) { + return null; + } + return idToModification[uniqueId]; + } + public IEnumerable Values => idToModification.Values; public int NumberOfBlocksCovered(Implementation implementation, bool onlyIfTestsExists = false) { return NumberOfBlocksCovered(implementation.Blocks - .Where(block => Utils.GetBlockId(block) != null) - .Select(Utils.GetBlockId).ToHashSet(), onlyIfTestsExists); + .Where(block => Utils.GetBlockId(block, options) != null) + .Select(block => Utils.GetBlockId(block, options)).ToHashSet(), onlyIfTestsExists); } public int NumberOfBlocksCovered(HashSet blockIds, bool onlyIfTestsExists = false) { @@ -65,7 +72,7 @@ internal enum Status { Success, Failure, Untested } internal Status CounterexampleStatus; public readonly Implementation Implementation; // implementation under test - private readonly string uniqueId; + internal readonly string uniqueId; public readonly HashSet CapturedStates; private readonly HashSet testEntryNames; @@ -135,12 +142,6 @@ private static void SetupForCounterexamples(DafnyOptions options) { var guid = Guid.NewGuid().ToString(); program.Resolve(options); program.Typecheck(options); - engine.EliminateDeadVariables(program); - engine.CollectModSets(program); - engine.Inline(program); - program.RemoveTopLevelDeclarations(declaration => - declaration is Microsoft.Boogie.Implementation or Procedure && - Utils.DeclarationHasAttribute(declaration, "inline")); var result = await Task.WhenAny(engine.InferAndVerify(writer, program, new PipelineStatistics(), null, _ => { }, guid), diff --git a/Source/DafnyTestGeneration/ProgramModifier.cs b/Source/DafnyTestGeneration/ProgramModifier.cs index 95523ebe4d9..e430bc89586 100644 --- a/Source/DafnyTestGeneration/ProgramModifier.cs +++ b/Source/DafnyTestGeneration/ProgramModifier.cs @@ -37,11 +37,29 @@ public IEnumerable GetModifications( DafnyInfo = dafnyInfo; var options = dafnyInfo.Options; BlockCoalescer.CoalesceBlocks(program); - program = new AnnotationVisitor().VisitProgram(program); + foreach (var implementation in program.Implementations.Where(i => Utils.DeclarationHasAttribute(i, TestGenerationOptions.TestInlineAttribute))) { + var depthExpression = Utils.GetAttributeValue(implementation, TestGenerationOptions.TestInlineAttribute).First(); + var attribute = new QKeyValue(new Token(), "inline", + new List() { depthExpression }, null); + attribute.Next = implementation.Attributes; + implementation.Attributes = attribute; + } + if (options.TestGenOptions.Mode is TestGenerationOptions.Modes.Block or TestGenerationOptions.Modes.Path) { + program = new AnnotationVisitor(options).VisitProgram(program); + } AddAxioms(options, program); program.Resolve(options); program.Typecheck(options); + using (var engine = ExecutionEngine.CreateWithoutSharedCache(options)) { + engine.EliminateDeadVariables(program); + engine.CollectModSets(program); + engine.Inline(program); + } + program.RemoveTopLevelDeclarations(declaration => declaration is Implementation or Procedure && Utils.DeclarationHasAttribute(declaration, "inline")); program = new RemoveChecks(options).VisitProgram(program); + if (options.TestGenOptions.Mode is TestGenerationOptions.Modes.CallGraph) { + program = new AnnotationVisitor(options).VisitProgram(program); + } TestEntries = program.Implementations .Where(implementation => Utils.DeclarationHasAttribute(implementation, TestGenerationOptions.TestEntryAttribute) && @@ -56,9 +74,8 @@ public IEnumerable GetModifications( protected abstract IEnumerable GetModifications(Program p); protected bool ImplementationIsToBeTested(Implementation impl) => - (Utils.DeclarationHasAttribute(impl, TestGenerationOptions.TestEntryAttribute) || - Utils.DeclarationHasAttribute(impl, TestGenerationOptions.TestInlineAttribute)) && - impl.Name.StartsWith(ImplPrefix) && !impl.Name.EndsWith(CtorPostfix); + Utils.DeclarationHasAttribute(impl, TestGenerationOptions.TestEntryAttribute) && + impl.Name.StartsWith(ImplPrefix) && !impl.Name.EndsWith(CtorPostfix); /// /// Add axioms necessary for counterexample generation to work efficiently @@ -123,9 +140,14 @@ protected static LocalVariable GetNewLocalVariable( /// private class AnnotationVisitor : StandardVisitor { private Implementation/*?*/ implementation; + private DafnyOptions options; + + public AnnotationVisitor(DafnyOptions options) { + this.options = options; + } public override Block VisitBlock(Block node) { - var state = Utils.GetBlockId(node); + var state = Utils.GetBlockId(node, options); if (state == null) { // cannot map back to Dafny source location return base.VisitBlock(node); } @@ -150,15 +172,7 @@ public override Implementation VisitImplementation(Implementation node) { data = new List { "Impl", node.VerboseName.Split(" ")[0] }; data.AddRange(node.InParams.Select(var => new IdentifierExpr(new Token(), var))); node.Blocks[0].cmds.Insert(0, GetAssumePrintCmd(data)); - if (Utils.DeclarationHasAttribute(node, TestGenerationOptions.TestInlineAttribute)) { - // This method is inlined (and hence tested) - var depthExpression = Utils.GetAttributeValue(node, TestGenerationOptions.TestInlineAttribute).First(); - var attribute = new QKeyValue(new Token(), "inline", - new List() { depthExpression }, null); - attribute.Next = node.Attributes; - node.Attributes = attribute; - VisitBlockList(node.Blocks); - } else if (Utils.DeclarationHasAttribute(node, TestGenerationOptions.TestEntryAttribute)) { + if (Utils.DeclarationHasAttribute(node, TestGenerationOptions.TestEntryAttribute) || Utils.DeclarationHasAttribute(node, TestGenerationOptions.TestInlineAttribute)) { VisitBlockList(node.Blocks); } return node; diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index f72f3032e22..2f6978bd899 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -130,14 +130,15 @@ public static string GetStringRepresentation(DafnyOptions options, Microsoft.Boo /// /// Extract string mapping this basic block to a location in Dafny code. /// - public static string GetBlockId(Block block) { + public static string GetBlockId(Block block, DafnyOptions options) { var state = block.cmds.OfType().FirstOrDefault( cmd => cmd.Attributes != null && cmd.Attributes.Key == "captureState" && cmd.Attributes.Params != null && cmd.Attributes.Params.Count() == 1) ?.Attributes.Params[0].ToString(); - return state == null ? null : Regex.Replace(state, @"\s+", ""); + string uniqueId = options.TestGenOptions.Mode != TestGenerationOptions.Modes.Block ? "#" + block.UniqueId : ""; + return state == null ? null : Regex.Replace(state, @"\s+", "") + uniqueId; } public static IList GetAttributeValue(Implementation implementation, string attribute) { diff --git a/docs/dev/news/4326.feat b/docs/dev/news/4326.feat new file mode 100644 index 00000000000..fb7b7d19b4d --- /dev/null +++ b/docs/dev/news/4326.feat @@ -0,0 +1 @@ +Support generating of tests targeting path-coverage of the entire program and tests targeting call-graph-sensitive block coverage (referred to as Branch coverage) \ No newline at end of file