SVM optimizations

VSharp.API/Options.cs

@@ -4,11 +4,18 @@
 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
     }
 
@@ -23,32 +30,24 @@ public enum SearchStrategy
     }
 
     /// <summary>
-    /// 
-    /// </summary>
-    public enum CoverageZone
-    {
-        Method,
-        Class,
-        Module
-    }
-
-    /// <summary>
-    /// 
+    /// Parameters of the test generation run. 
     /// </summary>
-    /// <param name="OutputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+    /// <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="CoverageZone"></param>
-    /// <param name="ExecutionMode"></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).</param>
-    /// <param name="IsConstraintIndependenceEnabled"></param>
-    /// <param name="IsSolverIncrementalityEnabled"></param>
-    /// <param name="Visualize"></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,
-        CoverageZone CoverageZone = CoverageZone.Method,
         ExecutionMode ExecutionMode = ExecutionMode.Symbolic,
         bool GuidedSearch = false,
         uint RecThreshold = 0u,
@@ -58,15 +57,8 @@ public readonly record struct CoverOptions(
         bool Visualize = false
     )
     {
-        internal SiliOptions ToSiliOptions()
+        internal SiliOptions ToSiliOptions(coverageZone coverageZone)
         {
-            var coverageZone = CoverageZone switch
-            {
-                CoverageZone.Method => Interpreter.IL.coverageZone.MethodZone,
-                CoverageZone.Class => Interpreter.IL.coverageZone.ClassZone,
-                CoverageZone.Module => Interpreter.IL.coverageZone.ModuleZone
-            };
-
             var searchMode = SearchStrategy switch
             {
                 SearchStrategy.DFS => Interpreter.IL.searchMode.DFSMode,

VSharp.API/VSharp.cs

@@ -75,7 +75,7 @@ public static class TestGenerator
         {
             // TODO: customize search strategies via console options
             UnitTests unitTests = new UnitTests(options.OutputDirectory.FullName);
-            SILI explorer = new SILI(options.ToSiliOptions());
+            SILI explorer = new SILI(options.ToSiliOptions(coverageZone.MethodZone));
             Core.API.ConfigureSolver(SolverPool.mkSolver(), options.IsSolverIncrementalityEnabled);
             Core.API.SetConstraintIndependenceEnabled(options.IsConstraintIndependenceEnabled);
 

VSharp.SILI.Core/SolverInteraction.fs

@@ -2,6 +2,7 @@ namespace VSharp.Core
 
 open System.Collections.Generic
 open FSharpx.Collections
+open Microsoft.FSharp.Core
 open VSharp
 
 module public SolverInteraction =

VSharp.Solver/Z3.fs

@@ -75,7 +75,7 @@ module internal Z3 =
 
         let getMemoryConstant mkConst (typ : regionSort * fieldId list) =
             let result : ArrayExpr ref = ref null
-            if encodingCache.regionConstants.TryGetValue(typ, result) then !result
+            if encodingCache.regionConstants.TryGetValue(typ, result) then result.Value
             else
                 let regConst = mkConst()
                 encodingCache.regionConstants.Add(typ, regConst)
@@ -84,8 +84,10 @@ module internal Z3 =
         member x.Reset() =
             encodingCache <- freshCache()
 
-        member x.ClearTermToExpressionCache() =
+        member x.ClearQueryScopedCache() =
             encodingCache.termToExpression.Clear()
+            encodingCache.heapAddresses.Clear()
+            encodingCache.regionConstants.Clear()
 
         member private x.ValidateId id =
             assert(not <| String.IsNullOrWhiteSpace id)
@@ -743,9 +745,6 @@ module internal Z3 =
                     targetModel.state.allocatedTypes <- PersistentDict.add addr typ targetModel.state.allocatedTypes)
             targetModel.state.startingTime <- VectorTime.min targetModel.state.startingTime [encodingCache.lastSymbolicAddress - 1]
 
-            encodingCache.heapAddresses.Clear()
-            encodingCache.termToExpression.Clear()
-
     let private ctx = new Context()
     let private builder = Z3Builder(ctx)
 
@@ -773,36 +772,38 @@ module internal Z3 =
                 printLog Trace "SOLVER: trying to solve constraints..."
                 printLogLazy Trace "%s" (lazy(q.ToString()))
                 try
-                    let query = builder.EncodeTerm encCtx q
-                    let assumptions = query.assumptions
-                    let assumptions =
-                        seq {
-                            yield! (Seq.cast<_> assumptions)
-                            yield query.expr
-                        } |> Array.ofSeq
-//                    let pathAtoms = addSoftConstraints q.lvl
-                    let result = optCtx.Check assumptions
-                    match result with
-                    | Status.SATISFIABLE ->
-                        trace "SATISFIABLE"
-                        let z3Model = optCtx.Model
-                        let updatedModel = {currentModel with state = {currentModel.state with model = currentModel.state.model}}
-                        builder.UpdateModel z3Model updatedModel                      
-                        builder.ClearTermToExpressionCache()
-                        SmtSat { mdl = updatedModel }
-                    | Status.UNSATISFIABLE ->
-                        trace "UNSATISFIABLE"
-                        builder.ClearTermToExpressionCache()
-                        SmtUnsat { core = Array.empty (*optCtx.UnsatCore |> Array.map (builder.Decode Bool)*) }
-                    | Status.UNKNOWN ->
-                        trace "UNKNOWN"
-                        builder.ClearTermToExpressionCache()
-                        SmtUnknown optCtx.ReasonUnknown
-                    | _ -> __unreachable__()
-                with
-                | :? EncodingException as e ->
-                    printLog Info "SOLVER: exception was thrown: %s" e.Message
-                    SmtUnknown (sprintf "Z3 has thrown an exception: %s" e.Message)
+                    try
+                        let query = builder.EncodeTerm encCtx q
+                        let assumptions = query.assumptions
+                        let assumptions =
+                            seq {
+                                yield! (Seq.cast<_> assumptions)
+                                yield query.expr
+                            }
+                            |> Seq.distinct |> Array.ofSeq
+//                      let pathAtoms = addSoftConstraints q.lvl
+                        let result = optCtx.Check assumptions
+                        match result with
+                        | Status.SATISFIABLE ->
+                            trace "SATISFIABLE"
+                            let z3Model = optCtx.Model
+                            let updatedModel = {currentModel with state = {currentModel.state with model = currentModel.state.model}}
+                            builder.UpdateModel z3Model updatedModel
+                            SmtSat { mdl = updatedModel }
+                        | Status.UNSATISFIABLE ->
+                            trace "UNSATISFIABLE"
+                            SmtUnsat { core = Array.empty (*optCtx.UnsatCore |> Array.map (builder.Decode Bool)*) }
+                        | Status.UNKNOWN ->
+                            trace "UNKNOWN"
+                            SmtUnknown optCtx.ReasonUnknown
+                        | _ -> __unreachable__()
+                    with
+                    | :? EncodingException as e ->
+                        printLog Info "SOLVER: exception was thrown: %s" e.Message
+                        SmtUnknown (sprintf "Z3 has thrown an exception: %s" e.Message)
+                finally
+                    builder.ClearQueryScopedCache()
+
 
             member x.Assert encCtx (fml : term) =
                 printLogLazy Trace "SOLVER: Asserting: %s" (lazy(fml.ToString()))
@@ -817,43 +818,46 @@ module internal Z3 =
                         yield! Seq.cast<BoolExpr> encoded.assumptions
                         yield encoded.expr :?> BoolExpr
                     }
-                try                    
-                    let exprs = Seq.collect encodeToBoolExprs formulas
-                    let boolConsts = seq {
-                        for expr in exprs do
-                            let mutable name = ""
-                            if assumptions.TryGetValue(expr, &name) then
-                                yield ctx.MkBoolConst name
-                            else
-                                name <- $"p{assumptions.Count}"
-                                printLog Trace $"SOLVER: assert: {name} => {expr}"
-                                assumptions.[expr] <- name
-                                let boolConst = ctx.MkBoolConst name
-                                let implication = ctx.MkImplies(boolConst, expr)
-                                optCtx.Assert implication
-                                yield boolConst
-                    }
-                    let names = boolConsts |> Seq.map (fun c -> c.ToString())
-                    printLog Trace $"""SOLVER: check: {join " & " names}"""
-                    let result = optCtx.Check boolConsts
-                    match result with
-                    | Status.SATISFIABLE ->
-                        let z3Model = optCtx.Model
-                        let updatedModel = {currentModel with state = {currentModel.state with model = currentModel.state.model}}  
-                        builder.UpdateModel z3Model updatedModel
-                        builder.ClearTermToExpressionCache()
-                        SmtSat { mdl = updatedModel }
-                    | Status.UNSATISFIABLE ->
-                        builder.ClearTermToExpressionCache()
-                        SmtUnsat { core = Array.empty }
-                    | Status.UNKNOWN ->
-                        builder.ClearTermToExpressionCache()
-                        SmtUnknown optCtx.ReasonUnknown
-                    | _ -> __unreachable__()
-                with
-                | :? EncodingException as e ->
-                    printLog Info "SOLVER: exception was thrown: %s" e.Message
-                    SmtUnknown (sprintf "Z3 has thrown an exception: %s" e.Message)
+                try
+                    try                    
+                        let exprs = Seq.collect encodeToBoolExprs formulas |> Seq.distinct
+                        let boolConsts = seq {
+                            for expr in exprs do
+                                let mutable name = ""
+                                if assumptions.TryGetValue(expr, &name) then
+                                    yield ctx.MkBoolConst name
+                                else
+                                    name <- $"p{assumptions.Count}"
+                                    printLog Trace $"SOLVER: assert: {name} => {expr}"
+                                    assumptions.[expr] <- name
+                                    let boolConst = ctx.MkBoolConst name
+                                    let implication = ctx.MkImplies(boolConst, expr)
+                                    optCtx.Assert implication
+                                    yield boolConst
+                        }
+                        let names = boolConsts |> Seq.map (fun c -> c.ToString())
+                        printLog Trace $"""SOLVER: check: {join " & " names}"""
+                        let result = optCtx.Check boolConsts
+                        match result with
+                        | Status.SATISFIABLE ->
+                            trace "SATISFIABLE"
+                            let z3Model = optCtx.Model
+                            let updatedModel = {currentModel with state = {currentModel.state with model = currentModel.state.model}}  
+                            builder.UpdateModel z3Model updatedModel
+                            SmtSat { mdl = updatedModel }
+                        | Status.UNSATISFIABLE ->
+                            trace "UNSATISFIABLE"
+                            SmtUnsat { core = Array.empty }
+                        | Status.UNKNOWN ->
+                            trace "UNKNOWN"
+                            SmtUnknown optCtx.ReasonUnknown
+                        | _ -> __unreachable__()
+                    with
+                    | :? EncodingException as e ->
+                        printLog Info "SOLVER: exception was thrown: %s" e.Message
+                        SmtUnknown (sprintf "Z3 has thrown an exception: %s" e.Message)
+                finally
+                    builder.ClearQueryScopedCache()
 
     let reset() =
         builder.Reset()

VSharp.Test/IntegrationTests.cs

@@ -120,7 +120,7 @@ public TestSvmCommand(
             private TestResult Explore(TestExecutionContext context)
             {
                 Core.API.ConfigureSolver(SolverPool.mkSolver(), false);
-                Core.API.SetConstraintIndependenceEnabled(true);
+                Core.API.SetConstraintIndependenceEnabled(false);
 
                 var methodInfo = innerCommand.Test.Method.MethodInfo;
                 try