[fix] Fix TestRunner returning on failed test | Reset searcher after exploration

Author: mxprshn

VSharp.CSharpUtils/CompositeCompilationAssemblyResolver.cs

@@ -0,0 +1,33 @@
+using System.Collections.Generic;
+using Microsoft.Extensions.DependencyModel;
+using Microsoft.Extensions.DependencyModel.Resolution;
+
+namespace VSharp.CSharpUtils
+{
+    public class CompositeCompilationAssemblyResolver : ICompilationAssemblyResolver
+    {
+        private readonly ICompilationAssemblyResolver[] _resolvers;
+
+        public CompositeCompilationAssemblyResolver(ICompilationAssemblyResolver[] resolvers)
+        {
+            _resolvers = resolvers;
+        }
+
+        public bool TryResolveAssemblyPaths(CompilationLibrary library, List<string> assemblies)
+        {
+            foreach (ICompilationAssemblyResolver resolver in _resolvers)
+            {
+                try
+                {
+                    if (resolver.TryResolveAssemblyPaths(library, assemblies))
+                    {
+                        return true;
+                    }
+                }
+                catch { }
+            }
+
+            return false;
+        }
+    }
+}

VSharp.CSharpUtils/VSharp.CSharpUtils.csproj

@@ -13,6 +13,7 @@
 
     <ItemGroup>
       <PackageReference Include="Microsoft.Extensions.DependencyInjection" Version="2.0.0" />
+      <PackageReference Include="Microsoft.Extensions.DependencyModel" Version="6.0.0-rc.2.21480.5" />
     </ItemGroup>
 
 </Project>

VSharp.IL/CFG.fs

@@ -258,7 +258,7 @@ and Method internal (m : MethodBase) as this =
             Method.ReportCFGLoaded this
             cfg |> CfgInfo |> Some
         else None)
-    
+
     let blocksCoveredByTests = HashSet<offset>()
 
     member x.CFG with get() =
@@ -291,13 +291,13 @@ and Method internal (m : MethodBase) as this =
     static member val internal CoverageZone : Method -> bool = fun _ -> true with get, set
 
     member x.InCoverageZone with get() = Method.CoverageZone x
-    
+
     member x.BasicBlocksCount with get() =
         if x.HasBody then x.CFG.SortedOffsets |> Seq.length |> uint else 0u
-    
+
     member x.BlocksCoveredByTests with get() = blocksCoveredByTests :> IReadOnlySet<offset>
     member x.SetBlockIsCoveredByTest(offset : offset) = blocksCoveredByTests.Add(offset)
-    
+
     member x.ResetStatistics() = blocksCoveredByTests.Clear()
 
 [<CustomEquality; CustomComparison>]
@@ -319,7 +319,7 @@ type public codeLocation = {offset : offset; method : Method}
 module public CodeLocation =
     let isBasicBlockCoveredByTest (blockStart : codeLocation) =
         blockStart.method.BlocksCoveredByTests.Contains blockStart.offset
-        
+
     let hasSiblings (blockStart : codeLocation) =
         let method = blockStart.method
         method.HasBody && method.CFG.HasSiblings blockStart.offset
@@ -515,7 +515,7 @@ module Application =
     let addGoal = graph.AddGoal
     let addGoals = graph.AddGoals
     let removeGoal = graph.RemoveGoal
-    
+
     let resetMethodStatistics() =
         lock methods (fun () ->
             for method in methods.Values do

VSharp.SILI/BidirectionalSearcher.fs

@@ -1,6 +1,5 @@
 namespace VSharp.Interpreter.IL
 
-open System.Reflection
 open System.Collections.Generic
 open FSharpx.Collections
 open VSharp
@@ -78,6 +77,11 @@ type BidirectionalSearcher(forward : IForwardSearcher, backward : IBackwardSearc
 //                        GoFront s
 //                    | None -> Stop
 
+        override x.Reset () =
+            forward.Reset()
+            backward.Reset()
+            targeted.Reset()
+
 type OnlyForwardSearcher(searcher : IForwardSearcher) =
     interface IBidirectionalSearcher with
         override x.Init _ cilStates _ = searcher.Init cilStates
@@ -90,6 +94,7 @@ type OnlyForwardSearcher(searcher : IForwardSearcher) =
             | Some s -> GoFront s
             | None -> Stop
         override x.States() = searcher.States()
+        override x.Reset() = searcher.Reset()
 
 // TODO: check pob duplicates
 type BackwardSearcher() =
@@ -191,6 +196,8 @@ type BackwardSearcher() =
                 // TODO: need this?
                 internalfail "olololo!"
 
+        override x.Reset() = clear()
+
 module DummyTargetedSearcher =
     open CilStateOperations
 
@@ -232,3 +239,9 @@ module DummyTargetedSearcher =
 
             override x.Pick () =
                 targets.Keys |> Seq.tryPick (fun ip -> forPropagation.[ip] |> Seq.tryHead)
+
+            override x.Reset () =
+                forPropagation.Clear()
+                finished.Clear()
+                reached.Clear()
+                targets.Clear()

VSharp.SILI/InterleavedSearcher.fs

@@ -3,27 +3,30 @@
 open System.Linq
 
 type InterleavedSearcher(searchersWithStepCount: (IForwardSearcher * int) list) =
-    
-    let searchers = seq { while true do yield! searchersWithStepCount |> Seq.collect Enumerable.Repeat }    
+
+    let searchers = seq { while true do yield! searchersWithStepCount |> Seq.collect Enumerable.Repeat }
     let searchersEnumerator = searchers.GetEnumerator()
-    
+
     let getCurrentSearcher() =
         searchersEnumerator.MoveNext() |> ignore
         searchersEnumerator.Current
 
-    let init states = for searcher, _ in searchersWithStepCount do searcher.Init states          
-    
+    let init states = for searcher, _ in searchersWithStepCount do searcher.Init states
+
     // TODO: handle None
     let pick() = getCurrentSearcher().Pick()
-    
+
     let update (parent, newStates) =
         for searcher, _ in searchersWithStepCount do
             searcher.Update(parent, newStates)
-    
-    let states() = searchersWithStepCount |> Seq.collect (fun (s, _) -> s.States()) |> Seq.distinct 
-    
+
+    let states() = searchersWithStepCount |> Seq.collect (fun (s, _) -> s.States()) |> Seq.distinct
+
+    let reset() = for searcher, _ in searchersWithStepCount do searcher.Reset()
+
     interface IForwardSearcher with
         override x.Init states = init states
         override x.Pick() = pick()
         override x.Update (parent, newStates) = update (parent, newStates)
         override x.States() = states()
+        override x.Reset() = reset()

VSharp.SILI/SILI.fs

@@ -16,7 +16,6 @@ open VSharp.Solver
 type public SILI(options : SiliOptions) =
 
     let stopwatch = Stopwatch()
-    let () = stopwatch.Start()
     let timeout = if options.timeout <= 0 then Int64.MaxValue else int64 options.timeout * 1000L
     let branchReleaseTimeout = if options.timeout <= 0 || not options.releaseBranches then Int64.MaxValue else timeout * 80L / 100L
     let mutable branchesReleased = false
@@ -214,6 +213,7 @@ type public SILI(options : SiliOptions) =
         isStopped <- false
         branchesReleased <- false
         AcquireBranches()
+        searcher.Reset()
         let mainPobs = coveragePobsForMethod entryPoint |> Seq.filter (fun pob -> pob.loc.offset <> 0<offsets>)
         Application.spawnStates (Seq.cast<_> initialStates)
         mainPobs |> Seq.map (fun pob -> pob.loc) |> Seq.toArray |> Application.addGoals
@@ -245,58 +245,66 @@ type public SILI(options : SiliOptions) =
     member x.InterpretEntryPoint (method : MethodBase) (mainArguments : string[]) (onFinished : Action<UnitTest>)
                                  (onException : Action<UnitTest>) (onIIE : Action<InsufficientInformationException>)
                                  (onInternalFail : Action<Exception>) : unit =
+        stopwatch.Restart()
         reportInternalFail <- wrapOnInternalFail onInternalFail
         try
-            assert method.IsStatic
-            let optionArgs = if mainArguments = null then None else Some mainArguments
-            let method = Application.getMethod method
-            reportFinished <- wrapOnTest onFinished method optionArgs
-            reportError <- wrapOnError onException method optionArgs
-            reportIncomplete <- wrapOnIIE onIIE
-            interpreter.ConfigureErrorReporter reportError
-            let state = Memory.EmptyState()
-            state.model <- Memory.EmptyModel method
-            let argsToState args =
-                let argTerms = Seq.map (fun str -> Memory.AllocateString str state) args
-                let stringType = typeof<string>
-                let argsNumber = MakeNumber mainArguments.Length
-                Memory.AllocateConcreteVectorArray state argsNumber stringType argTerms
-            let arguments = Option.map (argsToState >> List.singleton) optionArgs
-            ILInterpreter.InitFunctionFrame state method None arguments
-            if Option.isNone optionArgs then
-                // NOTE: if args are symbolic, constraint 'args != null' is added
-                let parameters = method.Parameters
-                assert(Array.length parameters = 1)
-                let argsParameter = Array.head parameters
-                let argsParameterTerm = Memory.ReadArgument state argsParameter
-                AddConstraint state (!!(IsNullReference argsParameterTerm))
-            Memory.InitializeStaticMembers state method.DeclaringType
-            let initialState = makeInitialState method state
-            x.AnswerPobs method [initialState]
-        with
-        | e -> reportInternalFail e
+            try
+                assert method.IsStatic
+                let optionArgs = if mainArguments = null then None else Some mainArguments
+                let method = Application.getMethod method
+                reportFinished <- wrapOnTest onFinished method optionArgs
+                reportError <- wrapOnError onException method optionArgs
+                reportIncomplete <- wrapOnIIE onIIE
+                interpreter.ConfigureErrorReporter reportError
+                let state = Memory.EmptyState()
+                state.model <- Memory.EmptyModel method
+                let argsToState args =
+                    let argTerms = Seq.map (fun str -> Memory.AllocateString str state) args
+                    let stringType = typeof<string>
+                    let argsNumber = MakeNumber mainArguments.Length
+                    Memory.AllocateConcreteVectorArray state argsNumber stringType argTerms
+                let arguments = Option.map (argsToState >> List.singleton) optionArgs
+                ILInterpreter.InitFunctionFrame state method None arguments
+                if Option.isNone optionArgs then
+                    // NOTE: if args are symbolic, constraint 'args != null' is added
+                    let parameters = method.Parameters
+                    assert(Array.length parameters = 1)
+                    let argsParameter = Array.head parameters
+                    let argsParameterTerm = Memory.ReadArgument state argsParameter
+                    AddConstraint state (!!(IsNullReference argsParameterTerm))
+                Memory.InitializeStaticMembers state method.DeclaringType
+                let initialState = makeInitialState method state
+                x.AnswerPobs method [initialState]
+            with
+            | e -> reportInternalFail e
+        finally
+            searcher.Reset()
 
     member x.InterpretIsolated (method : MethodBase) (onFinished : Action<UnitTest>)
                                (onException : Action<UnitTest>) (onIIE : Action<InsufficientInformationException>)
                                (onInternalFail : Action<Exception>) : unit =
+        stopwatch.Restart()
         reportInternalFail <- wrapOnInternalFail onInternalFail
         try
-            Reset()
-            SolverPool.reset()
-            let method = Application.getMethod method
-            reportFinished <- wrapOnTest onFinished method None
-            reportError <- wrapOnError onException method None
-            reportIncomplete <- wrapOnIIE onIIE
-            interpreter.ConfigureErrorReporter reportError
-            let initialStates = x.FormInitialStates method
-            let iieStates, initialStates = initialStates |> List.partition (fun state -> state.iie.IsSome)
-            iieStates |> List.iter reportIncomplete
-            if not initialStates.IsEmpty then
-                x.AnswerPobs method initialStates
-            Restore()
-        with
-        | e -> reportInternalFail e
-        
+            try
+                Reset()
+                SolverPool.reset()
+                let method = Application.getMethod method
+                reportFinished <- wrapOnTest onFinished method None
+                reportError <- wrapOnError onException method None
+                reportIncomplete <- wrapOnIIE onIIE
+                interpreter.ConfigureErrorReporter reportError
+                let initialStates = x.FormInitialStates method
+                let iieStates, initialStates = initialStates |> List.partition (fun state -> state.iie.IsSome)
+                iieStates |> List.iter reportIncomplete
+                if not initialStates.IsEmpty then
+                    x.AnswerPobs method initialStates
+                Restore()
+            with
+            | e -> reportInternalFail e
+        finally
+            searcher.Reset()
+
     member x.Stop() = isStopped <- true
 
     member x.Statistics with get() = statistics

VSharp.SILI/Searcher.fs

@@ -20,17 +20,20 @@ type IBidirectionalSearcher =
     abstract member Answer : pob -> pobStatus -> unit
     abstract member Statuses : unit -> seq<pob * pobStatus>
     abstract member States : unit -> cilState seq
+    abstract member Reset : unit -> unit
 
 type IForwardSearcher =
     abstract member Init : cilState seq -> unit
     abstract member Update : cilState * cilState seq -> unit
     abstract member Pick : unit -> cilState option
     abstract member States : unit -> cilState seq
+    abstract member Reset : unit -> unit
 
 type ITargetedSearcher =
     abstract member SetTargets : ip -> ip seq -> unit
     abstract member Update : cilState -> cilState seq -> cilState seq // returns states that reached its target
     abstract member Pick : unit -> cilState option
+    abstract member Reset : unit -> unit
 
 type backwardAction = Propagate of cilState * pob | InitTarget of ip * pob seq | NoAction
 
@@ -41,6 +44,7 @@ type IBackwardSearcher =
     abstract member Statuses : unit -> seq<pob * pobStatus>
     abstract member Pick : unit -> backwardAction
     abstract member AddBranch : cilState -> pob list
+    abstract member Reset : unit -> unit
 
     // TODO: get rid of this!
     abstract member RemoveBranch : cilState -> unit
@@ -70,16 +74,17 @@ type SimpleForwardSearcher(maxBound) =
         override x.Update (parent, newStates) =
             x.Insert forPropagation (parent, newStates)
         override x.States() = forPropagation
+        override x.Reset() = forPropagation.Clear()
 
     abstract member Choose : seq<cilState> -> cilState option
     default x.Choose states = Seq.tryLast states
-    
+
     abstract member Insert : List<cilState> -> cilState * seq<cilState> -> unit
     default x.Insert states (parent, newStates) =
         if isStopped parent then
             states.Remove(parent) |> ignore
         Seq.iter (add states) newStates
-        
+
     abstract member Init : List<cilState> -> seq<cilState> -> unit
     default x.Init states initStates = states.AddRange(initStates)
 
@@ -151,6 +156,7 @@ type WeightedSearcher(maxBound, weighter : IWeighter, storage : IPriorityCollect
         override x.Pick() = x.Pick()
         override x.Update (parent, newStates) = x.Update (parent, newStates)
         override x.States() = storage.ToSeq
+        override x.Reset() = storage.Clear()
 
     member x.Weighter = weighter
     member x.TryGetWeight state = storage.TryGetPriority state

VSharp.SILI/TargetedSearcher.fs

@@ -213,13 +213,18 @@ type GuidedSearcher(maxBound, threshold : uint, baseSearcher : IForwardSearcher,
 
     let pick () = pick' id
 
+    let reset () =
+        baseSearcher.Reset()
+        for searcher in targetedSearchers.Values do (searcher :> IForwardSearcher).Reset()
+
     interface IForwardSearcher with
         override x.Init states =
             baseSearcher.Init states
             insertInTargetedSearchers states
         override x.Pick() = pick ()
         override x.Update (parent, newStates) = update parent newStates
         override x.States() = baseSearcher.States()
+        override x.Reset() = reset ()
 
 type ShortestDistanceBasedSearcher(maxBound, statistics : SILIStatistics) =
     inherit WeightedSearcher(maxBound, IntraproceduralShortestDistanceToUncoveredWeighter(statistics), BidictionaryPriorityQueue())