SVM optimizations

VSharp.API/SvmOptions.cs

@@ -0,0 +1,24 @@
+using VSharp.Core;
+
+namespace VSharp
+{
+    /// <summary>
+    /// Advanced symbolic virtual machine options.
+    /// </summary>
+    /// <param name="IsConstraintIndependenceEnabled">If true, independent constraint sets are maintained (constraint independence optimization).</param>
+    /// <param name="IsConditionEvaluationEnabled">If true, branch condition is evaluated with current model to avoid extra SMT solver queries.</param>
+    /// <param name="IsSolverIncrementalityEnabled">If true, SMT solver works in incremental mode.</param>
+    public readonly record struct SvmOptions(
+        bool IsConstraintIndependenceEnabled = false,
+        bool IsConditionEvaluationEnabled = false,
+        bool IsSolverIncrementalityEnabled = false
+    )
+    {
+        internal featureFlags GetFeatureFlags() =>
+            new featureFlags(
+                isConstraintIndependenceEnabled: IsConstraintIndependenceEnabled,
+                isConditionEvaluationEnabled: IsConditionEvaluationEnabled,
+                isIncrementalityEnabled: IsSolverIncrementalityEnabled
+            );
+    }
+}

VSharp.API/VSharp.cs

@@ -71,7 +71,7 @@ public void GenerateReport(TextWriter writer)
 
     public static class TestGenerator
     {
-        private static Statistics StartExploration(List<MethodBase> methods, string resultsFolder, string[] mainArguments = null)
+        private static Statistics StartExploration(List<MethodBase> methods, string resultsFolder, SvmOptions svmOptions, string[] mainArguments = null)
         {
             var recThreshold = 0u;
             var options =
@@ -80,6 +80,9 @@ private static Statistics StartExploration(List<MethodBase> methods, string resu
             SILI explorer = new SILI(options);
             UnitTests unitTests = new UnitTests(resultsFolder);
             Core.API.ConfigureSolver(SolverPool.mkSolver());
+            Core.API.SetFeatureFlags(svmOptions.GetFeatureFlags());
+
+            // TODO: single solver instance for multiple methods causes problems in incrementality mode
             foreach (var method in methods)
             {
                 if (method == method.Module.Assembly.EntryPoint)
@@ -111,21 +114,23 @@ private static bool Reproduce(DirectoryInfo testDir)
         /// </summary>
         /// <param name="method">Type to be covered with tests.</param>
         /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="svmOptions">Advanced symbolic virtual machine options.</param>
         /// <returns>Summary of tests generation process.</returns>
-        public static Statistics Cover(MethodBase method, string outputDirectory = "")
+        public static Statistics Cover(MethodBase method, string outputDirectory = "", SvmOptions svmOptions = new())
         {
             List<MethodBase> methods = new List<MethodBase> {method};
-            return StartExploration(methods, outputDirectory);
+            return StartExploration(methods, outputDirectory, svmOptions);
         }
 
         /// <summary>
         /// Generates test coverage for all public methods of specified type.
         /// </summary>
         /// <param name="type">Type to be covered with tests.</param>
         /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="svmOptions">Advanced symbolic virtual machine options.</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, string outputDirectory = "")
+        public static Statistics Cover(Type type, string outputDirectory = "", SvmOptions svmOptions = new())
         {
             BindingFlags bindingFlags = BindingFlags.Instance | BindingFlags.Static | BindingFlags.Public |
                                         BindingFlags.DeclaredOnly;
@@ -140,18 +145,19 @@ public static Statistics Cover(Type type, string outputDirectory = "")
                 throw new ArgumentException("I've not found any public method of class " + type.FullName);
             }
 
-            return StartExploration(methods, outputDirectory);
+            return StartExploration(methods, outputDirectory, svmOptions);
         }
 
         /// <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="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="svmOptions">Advanced symbolic virtual machine options.</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, string outputDirectory = "")
+        public static Statistics Cover(Assembly assembly, string outputDirectory = "", SvmOptions svmOptions = new())
         {
             List<MethodBase> methods;
             BindingFlags bindingFlags = BindingFlags.Instance | BindingFlags.Static | BindingFlags.Public |
@@ -173,7 +179,7 @@ public static Statistics Cover(Assembly assembly, string outputDirectory = "")
                 throw new ArgumentException("I've not found any public method in assembly");
             }
 
-            return StartExploration(methods, outputDirectory);
+            return StartExploration(methods, outputDirectory, svmOptions);
         }
 
         /// <summary>
@@ -182,10 +188,11 @@ public static Statistics Cover(Assembly assembly, string outputDirectory = "")
         /// <param name="assembly">Assembly to be covered with tests.</param>
         /// <param name="args">Command line arguments of entry point</param>
         /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="svmOptions">Advanced symbolic virtual machine options.</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, string outputDirectory = "")
+        public static Statistics Cover(Assembly assembly, string[] args, string outputDirectory = "", SvmOptions svmOptions = new())
         {
             List<MethodBase> methods;
             var entryPoint = assembly.EntryPoint;
@@ -195,18 +202,19 @@ public static Statistics Cover(Assembly assembly, string[] args, string outputDi
             }
             methods = new List<MethodBase> { entryPoint };
 
-            return StartExploration(methods, outputDirectory, args);
+            return StartExploration(methods, outputDirectory, svmOptions, 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="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="svmOptions">Advanced symbolic virtual machine options.</param>
         /// <returns>True if all generated tests have passed.</returns>
-        public static bool CoverAndRun(MethodBase method, string outputDirectory = "")
+        public static bool CoverAndRun(MethodBase method, string outputDirectory = "", SvmOptions svmOptions = new())
         {
-            var stats = Cover(method, outputDirectory);
+            var stats = Cover(method, outputDirectory, svmOptions);
             return Reproduce(stats.OutputDir);
         }
 
@@ -215,11 +223,12 @@ public static bool CoverAndRun(MethodBase method, string outputDirectory = "")
         /// </summary>
         /// <param name="type">Type to be covered with tests.</param>
         /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="svmOptions">Advanced symbolic virtual machine options.</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, string outputDirectory = "")
+        public static bool CoverAndRun(Type type, string outputDirectory = "", SvmOptions svmOptions = new())
         {
-            var stats = Cover(type, outputDirectory);
+            var stats = Cover(type, outputDirectory, svmOptions);
             return Reproduce(stats.OutputDir);
         }
 
@@ -228,12 +237,13 @@ public static bool CoverAndRun(Type type, string outputDirectory = "")
         /// </summary>
         /// <param name="assembly">Assembly to be covered with tests.</param>
         /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="svmOptions">Advanced symbolic virtual machine options.</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, string outputDirectory = "")
+        public static bool CoverAndRun(Assembly assembly, string outputDirectory = "", SvmOptions svmOptions = new())
         {
-            var stats = Cover(assembly, outputDirectory);
+            var stats = Cover(assembly, outputDirectory, svmOptions);
             return Reproduce(stats.OutputDir);
         }
 
@@ -243,11 +253,12 @@ public static bool CoverAndRun(Assembly assembly, string outputDirectory = "")
         /// <param name="assembly">Assembly to be covered with tests.</param>
         /// <param name="args">Command line arguments of entry point</param>
         /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+        /// <param name="svmOptions">Advanced symbolic virtual machine options.</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, string outputDirectory = "")
+        public static bool CoverAndRun(Assembly assembly, string[] args, string outputDirectory = "", SvmOptions svmOptions = new())
         {
-            var stats = Cover(assembly, args, outputDirectory);
+            var stats = Cover(assembly, args, outputDirectory, svmOptions);
             return Reproduce(stats.OutputDir);
         }
 

VSharp.Runner/RunnerProgram.cs

@@ -1,5 +1,4 @@
 using System;
-using System.Collections.Generic;
 using System.CommandLine;
 using System.CommandLine.Invocation;
 using System.IO;
@@ -122,6 +121,10 @@ public static int Main(string[] args)
             var unknownArgsOption =
                 new Option("--unknown-args", description: "Force engine to generate various input console arguments");
 
+            var constraintIndependenceOption = new Option<bool>("--c-independence", description: "Advanced: maintain independent constraint sets (constraint independence optimization)");
+            var conditionEvaluationOption = new Option<bool>("--eval-condition", description: "Advanced: evaluate branch condition with current model to avoid extra SMT solver queries");
+            var incrementalityOption = new Option<bool>("--incrementality", description: "Advanced: enable SMT solver incremental mode");
+
             var rootCommand = new RootCommand();
 
             var entryPointCommand =
@@ -131,66 +134,97 @@ public static int Main(string[] args)
             entryPointCommand.AddArgument(concreteArguments);
             entryPointCommand.AddGlobalOption(outputOption);
             entryPointCommand.AddOption(unknownArgsOption);
+            entryPointCommand.AddOption(constraintIndependenceOption);
+            entryPointCommand.AddOption(conditionEvaluationOption);
+            entryPointCommand.AddOption(incrementalityOption);
+
             var allPublicMethodsCommand =
                 new Command("--all-public-methods", "Generate unit tests for all public methods of all public classes of assembly");
             rootCommand.AddCommand(allPublicMethodsCommand);
             allPublicMethodsCommand.AddArgument(assemblyPathArgument);
             allPublicMethodsCommand.AddGlobalOption(outputOption);
+            allPublicMethodsCommand.AddOption(constraintIndependenceOption);
+            allPublicMethodsCommand.AddOption(conditionEvaluationOption);
+            allPublicMethodsCommand.AddOption(incrementalityOption);
+
             var publicMethodsOfClassCommand =
                 new Command("--public-methods-of-class", "Generate unit tests for all public methods of specified class");
             rootCommand.AddCommand(publicMethodsOfClassCommand);
             var classArgument = new Argument<string>("class-name");
             publicMethodsOfClassCommand.AddArgument(classArgument);
             publicMethodsOfClassCommand.AddArgument(assemblyPathArgument);
             publicMethodsOfClassCommand.AddGlobalOption(outputOption);
+            publicMethodsOfClassCommand.AddOption(constraintIndependenceOption);
+            publicMethodsOfClassCommand.AddOption(conditionEvaluationOption);
+            publicMethodsOfClassCommand.AddOption(incrementalityOption);
+
             var specificMethodCommand =
                 new Command("--method", "Try to resolve and generate unit test coverage for the specified method");
             rootCommand.AddCommand(specificMethodCommand);
             var methodArgument = new Argument<string>("method-name");
             specificMethodCommand.AddArgument(methodArgument);
             specificMethodCommand.AddArgument(assemblyPathArgument);
             specificMethodCommand.AddGlobalOption(outputOption);
+            specificMethodCommand.AddOption(constraintIndependenceOption);
+            specificMethodCommand.AddOption(conditionEvaluationOption);
+            specificMethodCommand.AddOption(incrementalityOption);
 
             rootCommand.Description = "Symbolic execution engine for .NET";
 
-            entryPointCommand.Handler = CommandHandler.Create<FileInfo, string[], DirectoryInfo, bool>((assemblyPath, args, output, unknownArgs) =>
-            {
-                var assembly = ResolveAssembly(assemblyPath);
-                if (unknownArgs)
-                    args = null;
-                if (assembly != null)
-                    PostProcess(TestGenerator.Cover(assembly, args, output.FullName));
-            });
-            allPublicMethodsCommand.Handler = CommandHandler.Create<FileInfo, DirectoryInfo>((assemblyPath, output) =>
-            {
-                var assembly = ResolveAssembly(assemblyPath);
-                if (assembly != null)
-                    PostProcess(TestGenerator.Cover(assembly, output.FullName));
-            });
-            publicMethodsOfClassCommand.Handler = CommandHandler.Create<string, FileInfo, DirectoryInfo>((className, assemblyPath, output) =>
-            {
-                var assembly = ResolveAssembly(assemblyPath);
-                if (assembly != null)
+            entryPointCommand.Handler = CommandHandler.Create<FileInfo, string[], DirectoryInfo, bool, bool, bool, bool>
+            (
+                (assemblyPath, args, output, unknownArgs, cIndependence, evalCondition, incrementality) =>
                 {
-                    var type = ResolveType(assembly, className);
-                    if (type != null)
+                    var options = new SvmOptions(cIndependence, evalCondition, incrementality);
+                    var assembly = ResolveAssembly(assemblyPath);
+                    if (unknownArgs)
+                        args = null;
+                    if (assembly != null)
+                        PostProcess(TestGenerator.Cover(assembly, args, output.FullName, options));
+                }
+            );
+            allPublicMethodsCommand.Handler = CommandHandler.Create<FileInfo, DirectoryInfo, bool, bool, bool>
+            (
+                (assemblyPath, output, cIndependence, evalCondition, incrementality) =>
+                {
+                    var options = new SvmOptions(cIndependence, evalCondition, incrementality);
+                    var assembly = ResolveAssembly(assemblyPath);
+                    if (assembly != null)
+                        PostProcess(TestGenerator.Cover(assembly, output.FullName, options));
+                }
+            );
+            publicMethodsOfClassCommand.Handler = CommandHandler.Create<string, FileInfo, DirectoryInfo, bool, bool, bool>
+            (
+                (className, assemblyPath, output, cIndependence, evalCondition, incrementality) =>
+                {
+                    var options = new SvmOptions(cIndependence, evalCondition, incrementality);
+                    var assembly = ResolveAssembly(assemblyPath);
+                    if (assembly != null)
                     {
-                        PostProcess(TestGenerator.Cover(type, output.FullName));
+                        var type = ResolveType(assembly, className);
+                        if (type != null)
+                        {
+                            PostProcess(TestGenerator.Cover(type, output.FullName, options));
+                        }
                     }
                 }
-            });
-            specificMethodCommand.Handler = CommandHandler.Create<string, FileInfo, DirectoryInfo>((methodName, assemblyPath, output) =>
-            {
-                var assembly = ResolveAssembly(assemblyPath);
-                if (assembly != null)
+            );
+            specificMethodCommand.Handler = CommandHandler.Create<string, FileInfo, DirectoryInfo, bool, bool, bool>
+            (
+                (methodName, assemblyPath, output, cIndependence, evalCondition, incrementality) =>
                 {
-                    var method = ResolveMethod(assembly, methodName);
-                    if (method != null)
+                    var options = new SvmOptions(cIndependence, evalCondition, incrementality);
+                    var assembly = ResolveAssembly(assemblyPath);
+                    if (assembly != null)
                     {
-                        PostProcess(TestGenerator.Cover(method, output.FullName));
+                        var method = ResolveMethod(assembly, methodName);
+                        if (method != null)
+                        {
+                            PostProcess(TestGenerator.Cover(method, output.FullName, options));
+                        }
                     }
                 }
-            });
+            );
 
             return rootCommand.InvokeAsync(args).Result;
         }