Interprocedural searcher

VSharp.API/VSharp.cs

@@ -30,6 +30,10 @@ public enum SearchStrategy
         /// </summary>
         ShortestDistance,
         /// <summary>
+        /// Picks the state closest to not covered locations (considering function calls).
+        /// </summary>
+        InterproceduralShortestDistance,
+        /// <summary>
         /// With a high probability picks the state closest to not covered locations.
         /// </summary>
         RandomShortestDistance,
@@ -238,7 +242,8 @@ private static searchMode ToSiliMode(this SearchStrategy searchStrategy)
                 SearchStrategy.ShortestDistance => searchMode.ShortestDistanceBasedMode,
                 SearchStrategy.RandomShortestDistance => searchMode.RandomShortestDistanceBasedMode,
                 SearchStrategy.ContributedCoverage => searchMode.ContributedCoverageMode,
-                SearchStrategy.Interleaved => searchMode.NewInterleavedMode(searchMode.ShortestDistanceBasedMode, 1, searchMode.ContributedCoverageMode, 9)
+                SearchStrategy.Interleaved => searchMode.NewInterleavedMode(searchMode.ShortestDistanceBasedMode, 1, searchMode.ContributedCoverageMode, 9),
+                SearchStrategy.InterproceduralShortestDistance => searchMode.InterproceduralShortestDistanceMode
             };
         }
 

VSharp.SILI/BidirectionalSearcher.fs

@@ -78,6 +78,8 @@ type BidirectionalSearcher(forward : IForwardSearcher, backward : IBackwardSearc
             backward.Reset()
             targeted.Reset()
 
+        override x.Refresh() = forward.Refresh()
+
         override x.Remove cilState =
             forward.Remove cilState
             backward.Remove cilState
@@ -98,6 +100,7 @@ type OnlyForwardSearcher(searcher : IForwardSearcher) =
             | Some s -> GoFront s
             | None -> Stop
         override x.States() = searcher.States()
+        override x.Refresh() = searcher.Refresh()
         override x.Reset() = searcher.Reset()
         override x.Remove cilState = searcher.Remove cilState
         override x.StatesCount with get() = searcher.StatesCount

VSharp.SILI/CILState.fs

@@ -1,12 +1,17 @@
 namespace VSharp.Interpreter.IL
 
+open FSharpx.Collections
 open VSharp
 open System.Text
 open System.Collections.Generic
 open VSharp.Core
 open VSharp.Interpreter.IL
 open ipOperations
 
+type CallStackEvent =
+    | Push of callFrom: codeLocation * callTo: codeLocation
+    | Pop
+
 [<ReferenceEquality>]
 type cilState =
     { mutable ipStack : ipStack
@@ -23,6 +28,7 @@ type cilState =
       mutable suspended : bool
       mutable targets : Set<codeLocation> option
       mutable lastPushInfo : term option
+      mutable lastCallStackEvents : CallStackEvent FSharpx.Collections.Queue
       /// <summary>
       /// All basic blocks visited by the state.
       /// </summary>
@@ -80,6 +86,7 @@ module internal CilStateOperations =
           suspended = false
           targets = None
           lastPushInfo = None
+          lastCallStackEvents = Queue.empty
           history = Set.empty
           entryMethod = Some entryMethod
           id = getNextStateId()
@@ -176,6 +183,7 @@ module internal CilStateOperations =
         | Some loc' when loc'.method.HasBody ->
             cilState.currentLoc <- loc'
             Application.addCallEdge loc loc'
+            cilState.lastCallStackEvents <- Queue.conj (Push(loc, loc')) cilState.lastCallStackEvents
         | _ -> ()
         cilState.ipStack <- ip :: cilState.ipStack
 
@@ -223,6 +231,9 @@ module internal CilStateOperations =
         | Some value when value > 0u -> cilState.level <- PersistentDict.add k (value - 1u) lvl
         | _ -> ()
 
+    let clearLastCallStackEvents (cilState : cilState) =
+        cilState.lastCallStackEvents <- Queue.empty
+
     let setBasicBlockIsVisited (cilState : cilState) (loc : codeLocation) =
         cilState.history <- Set.add loc cilState.history
 
@@ -233,6 +244,7 @@ module internal CilStateOperations =
         Memory.PopFrame cilState.state
         let ip = List.tail cilState.ipStack
         cilState.ipStack <- ip
+        cilState.lastCallStackEvents <- Queue.conj Pop cilState.lastCallStackEvents
         match ip with
         | ip::_ -> moveCodeLoc cilState ip
         | [] -> ()

VSharp.SILI/CombinedWeighter.fs

@@ -7,20 +7,18 @@ open VSharp.Interpreter.IL.TypeUtils
 /// <summary>
 /// Combines two weighters using the given combinator function.
 /// </summary>
-type internal CombinedWeighter(one : IWeighter, another : IWeighter, maxPriority : uint, combinator : uint option -> uint option -> uint option) =
+type internal CombinedWeighter(one : IWeighter, another : IWeighter, combinator : uint option -> uint option -> uint option) =
 
     interface IWeighter with
         override x.Weight(state) =
             let oneWeight = one.Weight state
             let anotherWeight = another.Weight state
             combinator oneWeight anotherWeight
-        override x.Next() = maxPriority
 
 type internal AugmentedWeighter(baseWeighter : IWeighter, mapping : uint option -> uint option) =
 
         interface IWeighter with
             override x.Weight(state) = baseWeighter.Weight state |> mapping
-            override x.Next() = baseWeighter.Next()
 
 module internal WeightOperations =
 

VSharp.SILI/ConcolicSearcher.fs

@@ -9,5 +9,6 @@ type internal ConcolicSearcher(baseSearcher : IForwardSearcher) =
         override x.Update(parent, newStates) = baseSearcher.Update(parent, newStates)
         override x.States() = baseSearcher.States()
         override x.Reset() = baseSearcher.Reset()
+        override x.Refresh() = baseSearcher.Refresh()
         override x.Remove cilState = baseSearcher.Remove cilState
         override x.StatesCount with get() = baseSearcher.StatesCount

VSharp.SILI/ContributedCoverageSearcher.fs

@@ -12,7 +12,6 @@ type internal ContributedCoverageWeighter(statistics : SILIStatistics) =
 
     interface IWeighter with
         override x.Weight(state) = weight state
-        override x.Next() = UInt32.MaxValue
 
 type internal ContributedCoverageSearcher(maxBound, statistics) =
     inherit WeightedSearcher(maxBound, ContributedCoverageWeighter(statistics), BidictionaryPriorityQueue())
@@ -21,8 +20,6 @@ type internal ContributedCoverageWithDistanceAsFallbackWeighter(statistics) =
     inherit CombinedWeighter(
         ContributedCoverageWeighter(statistics),
         IntraproceduralShortestDistanceToUncoveredWeighter(statistics),
-        UInt32.MaxValue,
         WeightOperations.withInverseLinearFallback 100u)
-
 type internal ContributedCoverageWithDistanceAsFallbackSearcher(maxBound, statistics) =
     inherit WeightedSearcher(maxBound, ContributedCoverageWithDistanceAsFallbackWeighter(statistics), BidictionaryPriorityQueue())

VSharp.SILI/DistanceWeighter.fs

@@ -93,7 +93,6 @@ type ShortestDistanceWeighter(target : codeLocation) =
                     return weight * logarithmicScale state.stepsNumber
                 | None -> return 1u
             }
-        override x.Next() = 0u
 
 type IntraproceduralShortestDistanceToUncoveredWeighter(statistics : SILIStatistics) =
 
@@ -107,6 +106,7 @@ type IntraproceduralShortestDistanceToUncoveredWeighter(statistics : SILIStatist
                 |> Seq.fold (fun min kvp ->
                     let loc = { offset = kvp.Key; method = method }
                     let distance = kvp.Value
+                    // TODO: check all instructions of basic block for coverage
                     if distance < min && distance <> 0u && not <| statistics.IsCovered loc then distance
                     else min) infinity
             Some minDistance
@@ -118,5 +118,3 @@ type IntraproceduralShortestDistanceToUncoveredWeighter(statistics : SILIStatist
                 | Some loc when loc.method.InCoverageZone -> minDistance loc.method loc.offset
                 | Some _ -> None
                 | None -> Some 1u)
-
-        override x.Next() = 0u

VSharp.SILI/FairSearcher.fs

@@ -131,6 +131,8 @@ type internal FairSearcher(baseSearcherFactory : unit -> IForwardSearcher, timeo
 
     let remove cilState = baseSearcher.Remove cilState
 
+    let refresh() = baseSearcher.Refresh()
+
     member x.BaseSearcher with get() = baseSearcher
 
     interface IForwardSearcher with
@@ -141,4 +143,5 @@ type internal FairSearcher(baseSearcherFactory : unit -> IForwardSearcher, timeo
         override x.States() = states()
         override x.Reset() = reset()
         override x.Remove cilState = remove cilState
+        override x.Refresh() = refresh()
         override x.StatesCount with get() = baseSearcher.StatesCount

VSharp.SILI/InterleavedSearcher.fs

@@ -32,6 +32,8 @@ type InterleavedSearcher(searchersWithStepCount: (IForwardSearcher * int) list)
 
     let states() = searchersWithStepCount |> Seq.collect (fun (s, _) -> s.States()) |> Seq.distinct
 
+    let refresh() = for searcher, _ in searchersWithStepCount do searcher.Refresh()
+
     let reset() = for searcher, _ in searchersWithStepCount do searcher.Reset()
 
     let remove cilState = for searcher, _ in searchersWithStepCount do searcher.Remove cilState
@@ -42,6 +44,7 @@ type InterleavedSearcher(searchersWithStepCount: (IForwardSearcher * int) list)
         override x.Pick selector = pick (Some selector)
         override x.Update (parent, newStates) = update (parent, newStates)
         override x.States() = states()
+        override x.Refresh() = refresh()
         override x.Reset() = reset()
         override x.Remove cilState = remove cilState
         override x.StatesCount with get() = searchersEnumerator.Current.StatesCount