SVM optimizations

VSharp.API/Options.cs

@@ -0,0 +1,90 @@
+using System.IO;
+using VSharp.Interpreter.IL;
+
+namespace VSharp
+{
+    /// <summary>
+    /// Symbolic virtual machine execution mode.
+    /// </summary>
+    public enum ExecutionMode
+    {
+        /// <summary>
+        /// Pure symbolic execution. Cannot cope with external dependencies in code. 
+        /// </summary>
+        Symbolic,
+        /// <summary>
+        /// (Experimental) Concrete and symbolic execution combination. Allows to explore code with external dependencies by
+        /// instantiating concrete objects.
+        /// </summary>
+        Concolic
+    }
+
+    /// <summary>
+    /// 
+    /// </summary>
+    public enum SearchStrategy
+    {
+        DFS,
+        BFS,
+        ShortestDistance
+    }
+
+    /// <summary>
+    /// Parameters of the test generation run. 
+    /// </summary>
+    /// <param name="OutputDirectory">Directory to place generated <c>*.vst</c> tests. If <c>null</c> or empty, process working directory is used.
+    /// <c>null</c> by default. </param>
+    /// <param name="SearchStrategy"></param>
+    /// <param name="ExecutionMode">Symbolic virtual machine execution mode. <see cref="F:ExecutionMode.Symbolic"/> by default.</param>
+    /// <param name="GuidedSearch"></param>
+    /// <param name="RecThreshold"></param>
+    /// <param name="Timeout">Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interruption).
+    /// -1 by default</param>
+    /// <param name="IsConstraintIndependenceEnabled">If true, constraint independence optimization is enabled: independent constraint sets are maintained
+    /// during symbolic execution. In general, improves execution time. <c>true</c> by default.</param>
+    /// <param name="IsSolverIncrementalityEnabled">If true, SMT solver works in incremental mode during symbolic execution. May improve execution
+    /// time in some cases. <c>false</c> by default.</param>
+    /// <param name="Visualize">If true, symbolic execution process animation is saved in <c>/visualize</c> subdirectory of the <see cref="OutputDirectory"/>.</param>
+    public readonly record struct CoverOptions(
+        DirectoryInfo OutputDirectory = null,
+        SearchStrategy SearchStrategy = SearchStrategy.DFS,
+        ExecutionMode ExecutionMode = ExecutionMode.Symbolic,
+        bool GuidedSearch = false,
+        uint RecThreshold = 0u,
+        int Timeout = -1,
+        bool IsConstraintIndependenceEnabled = true,
+        bool IsSolverIncrementalityEnabled = false,
+        bool Visualize = false
+    )
+    {
+        internal SiliOptions ToSiliOptions(coverageZone coverageZone)
+        {
+            var searchMode = SearchStrategy switch
+            {
+                SearchStrategy.DFS => Interpreter.IL.searchMode.DFSMode,
+                SearchStrategy.BFS => Interpreter.IL.searchMode.BFSMode,
+                SearchStrategy.ShortestDistance => Interpreter.IL.searchMode.ShortestDistanceBasedMode
+            };
+
+            if (GuidedSearch)
+            {
+                searchMode = searchMode.NewGuidedMode(searchMode);
+            }
+
+            var executionMode = ExecutionMode switch
+            {
+                ExecutionMode.Symbolic => Interpreter.IL.executionMode.SymbolicMode,
+                ExecutionMode.Concolic => Interpreter.IL.executionMode.ConcolicMode
+            };
+
+            return new SiliOptions(
+                explorationMode.NewTestCoverageMode(coverageZone, searchMode),
+                executionMode,
+                OutputDirectory,
+                RecThreshold,
+                Timeout,
+                Visualize
+            );
+        }
+    }
+}

VSharp.API/VSharp.cs

@@ -28,7 +28,7 @@ internal Statistics(TimeSpan time, DirectoryInfo outputDir, uint tests, uint err
         public TimeSpan TestGenerationTime { get; }
 
         /// <summary>
-        /// Directory where *.vst tests are placed
+        /// Directory where *.vst tests are placed.
         /// </summary>
         public DirectoryInfo OutputDir { get; }
 
@@ -71,21 +71,16 @@ public void GenerateReport(TextWriter writer)
 
     public static class TestGenerator
     {
-        private static Statistics StartExploration(List<MethodBase> methods, string resultsFolder, string[] mainArguments = null, int timeout = -1)
+        private static Statistics StartExploration(List<MethodBase> methods, CoverOptions options = new(), string[] mainArguments = null)
         {
-            var recThreshold = 0u;
-            UnitTests unitTests = new UnitTests(resultsFolder);
+            var outputDirectory = options.OutputDirectory ?? new DirectoryInfo(Directory.GetCurrentDirectory());
             // TODO: customize search strategies via console options
-            var options =
-                new SiliOptions(
-                    explorationMode.NewTestCoverageMode(coverageZone.MethodZone, searchMode.DFSMode),
-                    executionMode.SymbolicMode,
-                    unitTests.TestDirectory,
-                    recThreshold,
-                    timeout,
-                    false);
-            SILI explorer = new SILI(options);
-            Core.API.ConfigureSolver(SolverPool.mkSolver());
+            UnitTests unitTests = new UnitTests(outputDirectory.FullName);
+            SILI explorer = new SILI(options.ToSiliOptions(coverageZone.MethodZone));
+            // TODO: refresh solver ctx for each method in incremental mode
+            Core.API.ConfigureSolver(SolverPool.mkSolver(), options.IsSolverIncrementalityEnabled);
+            Core.API.SetConstraintIndependenceEnabled(options.IsConstraintIndependenceEnabled);
+
             foreach (var method in methods)
             {
                 if (method == method.Module.Assembly.EntryPoint)
@@ -116,24 +111,22 @@ public static bool Reproduce(DirectoryInfo testDir)
         /// Generates test coverage for specified method.
         /// </summary>
         /// <param name="method">Type to be covered with tests.</param>
-        /// <param name="timeout">Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption).</param>
-        /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="options">Additional parameters of the run.</param>
         /// <returns>Summary of tests generation process.</returns>
-        public static Statistics Cover(MethodBase method, int timeout = -1, string outputDirectory = "")
+        public static Statistics Cover(MethodBase method, CoverOptions options = new())
         {
             List<MethodBase> methods = new List<MethodBase> {method};
-            return StartExploration(methods, outputDirectory, null, timeout);
+            return StartExploration(methods, options);
         }
 
         /// <summary>
         /// Generates test coverage for all public methods of specified type.
         /// </summary>
         /// <param name="type">Type to be covered with tests.</param>
-        /// <param name="timeout">Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption).</param>
-        /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="options">Additional parameters of the run.</param>
         /// <returns>Summary of tests generation process.</returns>
         /// <exception cref="ArgumentException">Thrown if specified class does not contain public methods.</exception>
-        public static Statistics Cover(Type type, int timeout = -1, string outputDirectory = "")
+        public static Statistics Cover(Type type, CoverOptions options = new())
         {
             List<MethodBase> methods = new List<MethodBase>(type.GetConstructors());
 
@@ -146,19 +139,18 @@ public static Statistics Cover(Type type, int timeout = -1, string outputDirecto
                 throw new ArgumentException("I've not found any public method or constructor of class " + type.FullName);
             }
 
-            return StartExploration(methods, outputDirectory, null, timeout);
+            return StartExploration(methods, options);
         }
 
         /// <summary>
         /// Generates test coverage for all public methods of all public classes in the specified assembly.
         /// </summary>
         /// <param name="assembly">Assembly to be covered with tests.</param>
-        /// <param name="timeout">Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption).</param>
-        /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="options">Additional parameters of the run.</param>
         /// <returns>Summary of tests generation process.</returns>
         /// <exception cref="ArgumentException">Thrown if no public methods found in assembly.
         /// </exception>
-        public static Statistics Cover(Assembly assembly, int timeout = -1, string outputDirectory = "")
+        public static Statistics Cover(Assembly assembly, CoverOptions options = new())
         {
             List<MethodBase> methods;
             BindingFlags bindingFlags = BindingFlags.Instance | BindingFlags.Static | BindingFlags.Public |
@@ -180,20 +172,19 @@ public static Statistics Cover(Assembly assembly, int timeout = -1, string outpu
                 throw new ArgumentException("I've not found any public method in assembly");
             }
 
-            return StartExploration(methods, outputDirectory, null, timeout);
+            return StartExploration(methods, options);
         }
 
         /// <summary>
         /// Generates test coverage for the entry point of the specified assembly.
         /// </summary>
         /// <param name="assembly">Assembly to be covered with tests.</param>
-        /// <param name="args">Command line arguments of entry point</param>
-        /// <param name="timeout">Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption).</param>
-        /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="args">Command line arguments of entry point.</param>
+        /// <param name="options">Additional parameters of the run.</param>
         /// <returns>Summary of tests generation process.</returns>
         /// <exception cref="ArgumentException">Thrown if assembly does not contain entry point.
         /// </exception>
-        public static Statistics Cover(Assembly assembly, string[] args, int timeout = -1, string outputDirectory = "")
+        public static Statistics Cover(Assembly assembly, string[] args, CoverOptions options = new())
         {
             List<MethodBase> methods;
             var entryPoint = assembly.EntryPoint;
@@ -203,63 +194,59 @@ public static Statistics Cover(Assembly assembly, string[] args, int timeout = -
             }
             methods = new List<MethodBase> { entryPoint };
 
-            return StartExploration(methods, outputDirectory, args, timeout);
+            return StartExploration(methods, options, args);
         }
 
         /// <summary>
         /// Generates test coverage for the specified method and runs all tests.
         /// </summary>
         /// <param name="method">Type to be covered with tests.</param>
-        /// <param name="timeout">Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption).</param>
-        /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="options">Additional parameters of the run.</param>
         /// <returns>True if all generated tests have passed.</returns>
-        public static bool CoverAndRun(MethodBase method, int timeout = -1, string outputDirectory = "")
+        public static bool CoverAndRun(MethodBase method, CoverOptions options = new())
         {
-            var stats = Cover(method, timeout, outputDirectory);
+            var stats = Cover(method, options);
             return Reproduce(stats.OutputDir);
         }
 
         /// <summary>
         /// Generates test coverage for the specified type and runs all tests.
         /// </summary>
         /// <param name="type">Type to be covered with tests.</param>
-        /// <param name="timeout">Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption).</param>
-        /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="options">Additional parameters of the run.</param>
         /// <returns>True if all generated tests have passed.</returns>
         /// <exception cref="ArgumentException">Thrown if specified class does not contain public methods.</exception>
-        public static bool CoverAndRun(Type type, int timeout = -1, string outputDirectory = "")
+        public static bool CoverAndRun(Type type, CoverOptions options = new())
         {
-            var stats = Cover(type, timeout, outputDirectory);
+            var stats = Cover(type, options);
             return Reproduce(stats.OutputDir);
         }
 
         /// <summary>
         /// Generates test coverage for all public methods of all public classes of the specified assembly and runs all tests.
         /// </summary>
         /// <param name="assembly">Assembly to be covered with tests.</param>
-        /// <param name="timeout">Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption).</param>
-        /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="options">Additional parameters of the run.</param>
         /// <returns>True if all generated tests have passed.</returns>
         /// <exception cref="ArgumentException">Thrown if no public methods found in assembly.
         /// </exception>
-        public static bool CoverAndRun(Assembly assembly, int timeout = -1, string outputDirectory = "")
+        public static bool CoverAndRun(Assembly assembly, CoverOptions options = new())
         {
-            var stats = Cover(assembly, timeout, outputDirectory);
+            var stats = Cover(assembly, options);
             return Reproduce(stats.OutputDir);
         }
 
         /// <summary>
         /// Generates test coverage for entry point of the specified assembly and runs all tests.
         /// </summary>
         /// <param name="assembly">Assembly to be covered with tests.</param>
-        /// <param name="args">Command line arguments of entry point</param>
-        /// <param name="timeout">Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption).</param>
-        /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="args">Command line arguments of entry point.</param>
+        /// <param name="options">Additional parameters of the run.</param>
         /// <returns>True if all generated tests have passed.</returns>
         /// <exception cref="ArgumentException">Thrown if assembly does not contain entry point.</exception>
-        public static bool CoverAndRun(Assembly assembly, string[] args, int timeout = -1, string outputDirectory = "")
+        public static bool CoverAndRun(Assembly assembly, string[] args, CoverOptions options = new())
         {
-            var stats = Cover(assembly, args, timeout, outputDirectory);
+            var stats = Cover(assembly, args, options);
             return Reproduce(stats.OutputDir);
         }