diff --git a/VSharp.API/VSharp.cs b/VSharp.API/VSharp.cs index 0b9ebf080..b5de719ae 100644 --- a/VSharp.API/VSharp.cs +++ b/VSharp.API/VSharp.cs @@ -30,6 +30,10 @@ public enum SearchStrategy /// ShortestDistance, /// + /// Picks the state closest to not covered locations (considering function calls). + /// + InterproceduralShortestDistance, + /// /// With a high probability picks the state closest to not covered locations. /// 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 }; } diff --git a/VSharp.SILI/BidirectionalSearcher.fs b/VSharp.SILI/BidirectionalSearcher.fs index 613667ee5..5f1a6516b 100644 --- a/VSharp.SILI/BidirectionalSearcher.fs +++ b/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 diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs index f3075ee8e..6cafeae72 100644 --- a/VSharp.SILI/CILState.fs +++ b/VSharp.SILI/CILState.fs @@ -1,5 +1,6 @@ namespace VSharp.Interpreter.IL +open FSharpx.Collections open VSharp open System.Text open System.Collections.Generic @@ -7,6 +8,10 @@ open VSharp.Core open VSharp.Interpreter.IL open ipOperations +type CallStackEvent = + | Push of callFrom: codeLocation * callTo: codeLocation + | Pop + [] type cilState = { mutable ipStack : ipStack @@ -23,6 +28,7 @@ type cilState = mutable suspended : bool mutable targets : Set option mutable lastPushInfo : term option + mutable lastCallStackEvents : CallStackEvent FSharpx.Collections.Queue /// /// All basic blocks visited by the state. /// @@ -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 | [] -> () diff --git a/VSharp.SILI/CombinedWeighter.fs b/VSharp.SILI/CombinedWeighter.fs index c59d47096..c71c07a1b 100644 --- a/VSharp.SILI/CombinedWeighter.fs +++ b/VSharp.SILI/CombinedWeighter.fs @@ -7,20 +7,18 @@ open VSharp.Interpreter.IL.TypeUtils /// /// Combines two weighters using the given combinator function. /// -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 = diff --git a/VSharp.SILI/ConcolicSearcher.fs b/VSharp.SILI/ConcolicSearcher.fs index c809c74f6..0a85bf044 100644 --- a/VSharp.SILI/ConcolicSearcher.fs +++ b/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 diff --git a/VSharp.SILI/ContributedCoverageSearcher.fs b/VSharp.SILI/ContributedCoverageSearcher.fs index 3b758359d..dff5acda3 100644 --- a/VSharp.SILI/ContributedCoverageSearcher.fs +++ b/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()) diff --git a/VSharp.SILI/DistanceWeighter.fs b/VSharp.SILI/DistanceWeighter.fs index 05978d493..41f683027 100644 --- a/VSharp.SILI/DistanceWeighter.fs +++ b/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 diff --git a/VSharp.SILI/FairSearcher.fs b/VSharp.SILI/FairSearcher.fs index 5b993ba1d..44d66970b 100644 --- a/VSharp.SILI/FairSearcher.fs +++ b/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 diff --git a/VSharp.SILI/InterleavedSearcher.fs b/VSharp.SILI/InterleavedSearcher.fs index c1e805273..168400ebc 100644 --- a/VSharp.SILI/InterleavedSearcher.fs +++ b/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 diff --git a/VSharp.SILI/InterproceduralSearcher.fs b/VSharp.SILI/InterproceduralSearcher.fs new file mode 100644 index 000000000..07fad6a5d --- /dev/null +++ b/VSharp.SILI/InterproceduralSearcher.fs @@ -0,0 +1,332 @@ +namespace VSharp.Interpreter.IL + +open System +open System.Collections.Generic +open Microsoft.FSharp.Core +open VSharp +open VSharp.GraphUtils +open VSharp.Interpreter.IL +open VSharp.Utils +open CilStateOperations + +[] +type InterprocDistance = + | Approximate of uint + | Precise of uint + | Infinity + + member x.IsPrecise_ = + match x with + | Precise _ -> true + | _ -> false + + member x.IsApproximate_ = + match x with + | Approximate _ -> true + | _ -> false + + member x.Unwrap() = + match x with + | Approximate d + | Precise d -> d + | Infinity -> UInt32.MaxValue + + static member (+) (one, another) = + match one, another with + | Infinity, _ | _, Infinity -> Infinity + | Precise d1, Precise d2 -> Precise(d1 + d2) + | Approximate d1, Precise d2 + | Precise d1, Approximate d2 + | Approximate d1, Approximate d2 -> Approximate(d1 + d2) + + interface IComparable with + member this.CompareTo other = + match other with + | :? InterprocDistance as other -> (this :> IComparable<_>).CompareTo other + | _ -> invalidArg (nameof(other)) "(InterprocDistance) Types of compared objects don't match" + + interface IComparable with + member this.CompareTo other = + match this, other with + | Infinity, Infinity -> 0 + | Infinity, _ -> 1 + | _, Infinity -> -1 + | Approximate d1, Precise d2 -> 1 + | Precise d1, Approximate d2 -> -1 + | Approximate d1, Approximate d2 + | Precise d1, Precise d2 -> d1.CompareTo d2 + +type private callTree = { + parent : callTree option + children : HashSet + callLocation : codeLocation option + mutable minDistanceToUncoveredOnReturn : InterprocDistance + } + +type private distanceCache = Dictionary> + +type InterproceduralSearcher(maxBound, statistics : SILIStatistics) = + + let mutable priorityQueue : IPriorityCollection = BidictionaryPriorityQueue() + + let callTreeRoot = { + parent = None + children = HashSet() + callLocation = None + minDistanceToUncoveredOnReturn = Precise 0u + } + + let callTrees = Dictionary() + let callWeights = Dictionary>() + let dijkstraWeightCaches = Dictionary() + let returnsCache = Dictionary>() + + let ignoreState s = violatesLevel s maxBound + + let getReturns method = + Dict.getValueOrUpdate returnsCache method (fun _ -> HashSet method.CFG.Sinks) + + let getCallWeight method = + if callWeights.ContainsKey method then + let weight, _ = callWeights.[method] + weight + else + Approximate 1u + + let getCallInfo codeLocation = + if codeLocation.method.CFG.Calls.ContainsKey codeLocation.offset then + Some codeLocation.method.CFG.Calls.[codeLocation.offset] + else + None + + let stepWeight toLocation = + let callInfo = getCallInfo toLocation + if callInfo.IsSome then (getCallWeight callInfo.Value.Callee) + Precise 1u else Precise 1u + + let dijkstra offsetFrom (edges : graph) (cache : distanceCache) method = + let dist = Dictionary() + dist.Add (offsetFrom, Precise 0u) + let queue = Queue<_>() + queue.Enqueue offsetFrom + while not <| Seq.isEmpty queue do + let parent = queue.Dequeue() + if cache.ContainsKey parent then + for parentWeight in cache.[parent] do + if not <| dist.ContainsKey parentWeight.Key then + dist.Add (parentWeight.Key, dist.[parent] + parentWeight.Value) + else + for child in edges.[parent] do + let codeLocation = { offset = child; method = method } + if dist.ContainsKey child && dist.[parent] + stepWeight codeLocation < dist.[child] then + dist.Remove child |> ignore + if not <| dist.ContainsKey child then + dist.Add (child, dist.[parent] + stepWeight codeLocation) + queue.Enqueue child + dist + + let localDistancesFrom location = + let cfg = location.method.CFG + let basicBlock = cfg.ResolveBasicBlock location.offset + let distanceCache = Dict.getValueOrUpdate dijkstraWeightCaches location.method distanceCache + + Dict.getValueOrUpdate distanceCache basicBlock (fun () -> + dijkstra basicBlock cfg.Edges distanceCache location.method) + + let getMinDistanceToReturn codeLocation = + let localDistances = localDistancesFrom codeLocation + let returns = getReturns codeLocation.method + let distancesToReturn = returns |> Seq.filter localDistances.ContainsKey |> Seq.map (fun o -> localDistances.[o]) + if Seq.isEmpty distancesToReturn then Precise 0u else Seq.min distancesToReturn + + let getMinDistanceToUncoveredAndToReturn codeLocation = + let localDistances = localDistancesFrom codeLocation + let returns = getReturns codeLocation.method + let updateMinDistances (currentMinToUncovered, currentMinToReturn) (kvp : KeyValuePair) = + // TODO: check all instructions of basic block for coverage + let loc = { offset = kvp.Key; method = codeLocation.method } + let distance = kvp.Value + let newMinToUncovered = + if distance < currentMinToUncovered && distance.Unwrap() <> 0u && not <| CodeLocation.isBasicBlockCoveredByTest loc then distance + else currentMinToUncovered + let newMinToReturn = + if distance < currentMinToReturn && (returns.Contains kvp.Key) then distance + else currentMinToReturn + newMinToUncovered, newMinToReturn + let minToUncovered, minToReturn = Seq.fold updateMinDistances (Infinity, Infinity) localDistances + if minToReturn = Infinity then minToUncovered, Precise 0u else minToUncovered, minToReturn + + let weightLocation location minDistanceOnReturn = + if not <| location.method.InCoverageZone then + let minDistanceToReturn = getMinDistanceToReturn location + minDistanceToReturn + minDistanceOnReturn + else + let minDistanceToLocalUncovered, minDistanceToReturn = getMinDistanceToUncoveredAndToReturn location + min minDistanceToLocalUncovered (minDistanceToReturn + minDistanceOnReturn) + + let weight state = + match ipOperations.ip2codeLocation state.ipStack.Head with + | Some location -> + let tree = callTrees.[state] + //assert tree.callLocation.IsSome + weightLocation location tree.minDistanceToUncoveredOnReturn + | None -> Precise 0u + + // TODO: use CPS? + let rec updateCallTree (queue : Queue) = + if queue.Count = 0 then + () + else + let dequeued = queue.Dequeue() + match dequeued.callLocation with + | Some location -> + let newMinDistanceOnReturn = weightLocation location (if dequeued.parent.IsSome then dequeued.parent.Value.minDistanceToUncoveredOnReturn else Precise 0u) + if newMinDistanceOnReturn <> dequeued.minDistanceToUncoveredOnReturn && newMinDistanceOnReturn.IsApproximate_ && dequeued.minDistanceToUncoveredOnReturn.IsPrecise_ then + Logger.info $"Distance is updated: {dequeued.minDistanceToUncoveredOnReturn} -> {newMinDistanceOnReturn}" + dequeued.minDistanceToUncoveredOnReturn <- newMinDistanceOnReturn + | None -> () + dequeued.children |> Seq.iter queue.Enqueue + updateCallTree queue + + let calculateCallWeight (method : Method) = + let startBlock = { method = method; offset = 0 } + getMinDistanceToReturn startBlock + stepWeight startBlock + + let recalculateWeights() = + let queue = Queue() + queue.Enqueue callTreeRoot + updateCallTree queue + + let states = priorityQueue.ToSeq + priorityQueue <- BidictionaryPriorityQueue() + for state in states do + let weight = weight state + priorityQueue.Insert state weight + + // TODO: use CPS? + let rec updateCallWeights (preciseWeightMethods : Queue) = + if preciseWeightMethods.Count = 0 then + () + else + let preciseWeightMethod = preciseWeightMethods.Dequeue() + Logger.info $"Weight for {preciseWeightMethod.Name} is precise, recalculate" + let weightsToRecalculate = + callWeights + |> Seq.map (|KeyValue|) + |> Seq.filter (fun (_, v) -> (snd v).Contains preciseWeightMethod) + + for method, _ in weightsToRecalculate do + if dijkstraWeightCaches.ContainsKey method then + dijkstraWeightCaches.[method].Clear() + + let newWeight = calculateCallWeight method + callWeights.[method] <- (newWeight, snd callWeights.[method]) + + if newWeight.IsPrecise_ then + preciseWeightMethods.Enqueue method + + updateCallWeights preciseWeightMethods + + let addCallWeight method = + let callWeight = calculateCallWeight method + let callees = method.CFG.Calls.Values |> Seq.map (fun ci -> ci.Callee) |> HashSet + callWeights.[method] <- (callWeight, callees) + + if callWeight.IsPrecise_ then + let queue = Queue() + queue.Enqueue(method) + updateCallWeights queue + recalculateWeights() + + let pushToTree state fromLoc = + let callTree = callTrees.[state] + let newCallTreeNode = { + parent = Some callTree + children = HashSet() + callLocation = fromLoc + minDistanceToUncoveredOnReturn = + if fromLoc.IsSome then weightLocation fromLoc.Value callTree.minDistanceToUncoveredOnReturn else Precise 0u + } + callTree.children.Add newCallTreeNode |> ignore + callTrees.[state] <- newCallTreeNode + + let storageDump() = + Logger.info "Storage:" + priorityQueue.ToSeqWithPriority + |> Seq.sortByDescending snd + |> Seq.iter (fun (state, weight) -> + Logger.info $"{weight} {state.currentLoc.method} {state.currentLoc.offset}") + + let init states = + for state in states |> Seq.filter (not << ignoreState) do + callTrees.[state] <- callTreeRoot + pushToTree state None + let weight = weight state + priorityQueue.Insert state weight + + let pick() = + //storageDump() + priorityQueue.Choose() + + let pickWithSelector selector = priorityQueue.Choose selector + + let popFromTree state = + let callTree = callTrees.[state] + assert callTree.parent.IsSome + callTrees.[state] <- callTree.parent.Value + + let update parent newStates = + if priorityQueue.Contains parent then + assert(callTrees.ContainsKey parent) + if ignoreState parent && priorityQueue.Contains parent then + priorityQueue.Remove parent + else + for event in parent.lastCallStackEvents do + match event with + | Push(fromLoc, _) -> pushToTree parent (Some fromLoc) + | Pop -> popFromTree parent + + let newParentWeight = weight parent + priorityQueue.Update parent newParentWeight + + let tryAddCallWeight state = + match ipOperations.ip2codeLocation state.ipStack.Head with + | Some location -> + if not <| callWeights.ContainsKey location.method then + addCallWeight location.method + | None -> () + + tryAddCallWeight parent + + let parentCallTree = callTrees.[parent] + + for state in newStates |> Seq.filter (not << ignoreState) do + assert(not <| priorityQueue.Contains state) + callTrees.[state] <- parentCallTree + let weight = weight state + priorityQueue.Insert state weight + tryAddCallWeight state + + let reset() = + priorityQueue.Clear() + callTrees.Clear() + callWeights.Clear() + dijkstraWeightCaches.Clear() + returnsCache.Clear() + + let remove state = + if priorityQueue.Contains state then + priorityQueue.Remove state + callTrees.Remove state |> ignore + + member x.RecalculateWeights() = recalculateWeights() + + interface IForwardSearcher with + override x.Init states = init states + override x.Pick() = pick() + override x.Pick(selector) = pickWithSelector selector + override x.Update (parent, newStates) = update parent newStates + override x.States() = priorityQueue.ToSeq + override x.Refresh() = x.RecalculateWeights() + override x.Remove(state) = remove state + override x.Reset() = reset() + override x.StatesCount with get() = int priorityQueue.Count diff --git a/VSharp.SILI/Options.fs b/VSharp.SILI/Options.fs index 8fa44e443..9accb9062 100644 --- a/VSharp.SILI/Options.fs +++ b/VSharp.SILI/Options.fs @@ -11,6 +11,7 @@ type searchMode = | ContributedCoverageMode | FairMode of searchMode | InterleavedMode of searchMode * int * searchMode * int + | InterproceduralShortestDistanceMode | ConcolicMode of searchMode | GuidedMode of searchMode diff --git a/VSharp.SILI/SILI.fs b/VSharp.SILI/SILI.fs index 7de6a9778..7bf6e5eaf 100644 --- a/VSharp.SILI/SILI.fs +++ b/VSharp.SILI/SILI.fs @@ -70,6 +70,7 @@ type public SILI(options : SiliOptions) = FairSearcher((fun _ -> mkForwardSearcher baseMode), uint branchReleaseTimeout, statistics) :> IForwardSearcher | InterleavedMode(base1, stepCount1, base2, stepCount2) -> InterleavedSearcher([mkForwardSearcher base1, stepCount1; mkForwardSearcher base2, stepCount2]) :> IForwardSearcher + | InterproceduralShortestDistance -> InterproceduralSearcher(infty, statistics) :> IForwardSearcher | GuidedMode baseMode -> let baseSearcher = mkForwardSearcher baseMode GuidedSearcher(infty, options.recThreshold, baseSearcher, StatisticsTargetCalculator(statistics)) :> IForwardSearcher @@ -116,6 +117,7 @@ type public SILI(options : SiliOptions) = match TestGenerator.state2test isError entryMethod cmdArgs cilState message with | Some test -> statistics.TrackFinished cilState + searcher.Refresh() reporter test | None -> () with :? InsufficientInformationException as e -> @@ -286,6 +288,7 @@ type public SILI(options : SiliOptions) = Application.moveState loc s (Seq.cast<_> newStates) statistics.TrackFork s newStates searcher.UpdateStates s newStates + clearLastCallStackEvents s member private x.Backward p' s' = assert(currentLoc s' = p'.loc) diff --git a/VSharp.SILI/Searcher.fs b/VSharp.SILI/Searcher.fs index 17aa9b4df..65a83b2c1 100644 --- a/VSharp.SILI/Searcher.fs +++ b/VSharp.SILI/Searcher.fs @@ -20,6 +20,7 @@ type IBidirectionalSearcher = abstract member Answer : pob -> pobStatus -> unit abstract member Statuses : unit -> seq abstract member States : unit -> cilState seq + abstract member Refresh : unit -> unit abstract member Reset : unit -> unit abstract member Remove : cilState -> unit abstract member StatesCount : int @@ -30,6 +31,7 @@ type IForwardSearcher = abstract member Pick : unit -> cilState option abstract member Pick : (cilState -> bool) -> cilState option abstract member States : unit -> cilState seq + abstract member Refresh : unit -> unit abstract member Reset : unit -> unit abstract member Remove : cilState -> unit abstract member StatesCount : int @@ -80,6 +82,7 @@ type SimpleForwardSearcher(maxBound) = override x.Update (parent, newStates) = x.Insert forPropagation (parent, newStates) override x.States() = forPropagation + override x.Refresh() = () override x.Reset() = forPropagation.Clear() override x.Remove cilState = forPropagation.Remove cilState |> ignore override x.StatesCount with get() = forPropagation.Count @@ -116,9 +119,8 @@ type DFSSearcher(maxBound) = type IWeighter = abstract member Weight : cilState -> uint option - abstract member Next : unit -> uint -type WeightedSearcher(maxBound, weighter : IWeighter, storage : IPriorityCollection) = +type WeightedSearcher(maxBound, weighter : IWeighter, storage : IPriorityCollection) = let optionWeight s = try option { @@ -160,6 +162,7 @@ type WeightedSearcher(maxBound, weighter : IWeighter, storage : IPriorityCollect override x.Pick selector = x.Pick selector override x.Update (parent, newStates) = x.Update (parent, newStates) override x.States() = storage.ToSeq + override x.Refresh() = () override x.Reset() = storage.Clear() override x.Remove cilState = if storage.Contains cilState then storage.Remove cilState override x.StatesCount with get() = int x.Count diff --git a/VSharp.SILI/TargetedSearcher.fs b/VSharp.SILI/TargetedSearcher.fs index 8f092912f..073ea327a 100644 --- a/VSharp.SILI/TargetedSearcher.fs +++ b/VSharp.SILI/TargetedSearcher.fs @@ -230,6 +230,7 @@ type GuidedSearcher(maxBound, threshold : uint, baseSearcher : IForwardSearcher, override x.Pick selector = pick (Some selector) override x.Update (parent, newStates) = update parent newStates override x.States() = baseSearcher.States() + override x.Refresh() = () override x.Reset() = reset () override x.Remove cilState = remove cilState override x.StatesCount with get() = baseSearcher.StatesCount + (targetedSearchers.Values |> Seq.sumBy (fun s -> int s.Count)) diff --git a/VSharp.SILI/VSharp.SILI.fsproj b/VSharp.SILI/VSharp.SILI.fsproj index 765e67bd4..0ab54028e 100644 --- a/VSharp.SILI/VSharp.SILI.fsproj +++ b/VSharp.SILI/VSharp.SILI.fsproj @@ -47,6 +47,7 @@ + diff --git a/VSharp.Test/IntegrationTests.cs b/VSharp.Test/IntegrationTests.cs index 10dabe12a..92e9a5009 100644 --- a/VSharp.Test/IntegrationTests.cs +++ b/VSharp.Test/IntegrationTests.cs @@ -24,7 +24,8 @@ public enum SearchStrategy ShortestDistance, RandomShortestDistance, ContributedCoverage, - Interleaved + Interleaved, + InterproceduralShortestDistance } public enum CoverageZone @@ -189,6 +190,7 @@ public TestSvmCommand( SearchStrategy.RandomShortestDistance => searchMode.RandomShortestDistanceBasedMode, SearchStrategy.ContributedCoverage => searchMode.ContributedCoverageMode, SearchStrategy.Interleaved => searchMode.NewInterleavedMode(searchMode.ShortestDistanceBasedMode, 1, searchMode.ContributedCoverageMode, 9), + SearchStrategy.InterproceduralShortestDistance => searchMode.InterproceduralShortestDistanceMode, _ => throw new ArgumentOutOfRangeException(nameof(strat), strat, null) }; diff --git a/VSharp.Test/Tests/LoanExam.cs b/VSharp.Test/Tests/LoanExam.cs index 3a044bd51..6c298c7dc 100644 --- a/VSharp.Test/Tests/LoanExam.cs +++ b/VSharp.Test/Tests/LoanExam.cs @@ -194,7 +194,7 @@ private int CalculateByOtherCredits(bool otherCredits, CreditPurpose creditPurpo } } - [TestSvm(95, 0, -1, false, strat: SearchStrategy.Interleaved, coverageZone: CoverageZone.Class)] + [TestSvm(95, 0, 40, false, strat: SearchStrategy.InterproceduralShortestDistance, releaseBranches: true)] public CreditResult Build(Request request) { var SumPoints = 0; diff --git a/VSharp.Utils/DiscretePDF.fs b/VSharp.Utils/DiscretePDF.fs index 6e06f15c8..0b7990c04 100644 --- a/VSharp.Utils/DiscretePDF.fs +++ b/VSharp.Utils/DiscretePDF.fs @@ -235,6 +235,16 @@ type public DiscretePDF<'a when 'a : equality>(comparer : IComparer<'a>) = | None -> () } + let rec enumerateWithPriority optNode = + seq { + match optNode with + | Some node -> + yield node.Key, node.Weight + yield! enumerateWithPriority node.Left + yield! enumerateWithPriority node.Right + | None -> () + } + member x.Empty() = root = None member private x.Lookup(item : 'a) = lookup root item @@ -280,9 +290,11 @@ type public DiscretePDF<'a when 'a : equality>(comparer : IComparer<'a>) = count <- 0u member x.ToSeq = enumerate root + member x.ToSeqWithPriority = enumerateWithPriority root + member x.Count = count - interface IPriorityCollection<'a> with + interface IPriorityCollection<'a, uint> with override x.Insert item priority = x.Insert(item, priority) override x.Remove item = x.Remove(item) override x.Update item priority = x.Update(item, priority) @@ -293,13 +305,14 @@ type public DiscretePDF<'a when 'a : equality>(comparer : IComparer<'a>) = override x.Clear() = x.Clear() override x.Count = x.Count override x.ToSeq = x.ToSeq + override x.ToSeqWithPriority = x.ToSeqWithPriority module public DiscretePDF = let insert (dpdf: DiscretePDF<'a>) item weight = dpdf.Insert(item, weight) let remove (dpdf: DiscretePDF<'a>) item = dpdf.Remove(item) let update (dpdf: DiscretePDF<'a>) item weight = dpdf.Update(item, weight) - let choose (dpdf: DiscretePDF<'a>) = (dpdf :> IPriorityCollection<'a>).Choose() - let chooseWithSelector (dpdf: DiscretePDF<'a>) selector = (dpdf :> IPriorityCollection<'a>).Choose(selector) + let choose (dpdf: DiscretePDF<'a>) = (dpdf :> IPriorityCollection<'a, uint>).Choose() + let chooseWithSelector (dpdf: DiscretePDF<'a>) selector = (dpdf :> IPriorityCollection<'a, uint>).Choose(selector) let contains (dpdf: DiscretePDF<'a>) item = dpdf.Contains(item) let tryGetWeight (dpdf: DiscretePDF<'a>) item = dpdf.TryGetWeight item let toSeq (dpdf: DiscretePDF<'a>) = dpdf.ToSeq diff --git a/VSharp.Utils/PriorityCollection.fs b/VSharp.Utils/PriorityCollection.fs index 5754fd261..826a3d8e1 100644 --- a/VSharp.Utils/PriorityCollection.fs +++ b/VSharp.Utils/PriorityCollection.fs @@ -1,25 +1,28 @@ namespace VSharp.Utils +open System open System.Collections.Generic open System.Linq open VSharp -type IPriorityCollection<'a> = - abstract member Insert : 'a -> uint -> unit +type IPriorityCollection<'a, 'b> = + abstract member Insert : 'a -> 'b -> unit abstract member Remove : 'a -> unit - abstract member Update : 'a -> uint -> unit + abstract member Update : 'a -> 'b -> unit abstract member Choose : unit -> 'a option abstract member Choose : ('a -> bool) -> 'a option abstract member Contains : 'a -> bool - abstract member TryGetPriority : 'a -> uint option + abstract member TryGetPriority : 'a -> 'b option abstract member Clear : unit -> unit abstract member Count : uint abstract member ToSeq : 'a seq + abstract member ToSeqWithPriority : ('a * 'b) seq -type BidictionaryPriorityQueue<'a when 'a : equality>() = - let valuesToPriority = Dictionary<'a, uint>() - let priorityToList = SortedDictionary>() +// Less == better +type BidictionaryPriorityQueue<'a, 'b when 'a : equality and 'b : comparison>() = + let valuesToPriority = Dictionary<'a, 'b>() + let priorityToList = SortedDictionary<'b, LinkedList<'a>>() let isEmpty () = valuesToPriority.Count = 0 let insert item priority = assert(not <| valuesToPriority.ContainsKey item) @@ -53,7 +56,7 @@ type BidictionaryPriorityQueue<'a when 'a : equality>() = valuesToPriority.Clear() priorityToList.Clear() - interface IPriorityCollection<'a> with + interface IPriorityCollection<'a, 'b> with override x.Insert item priority = insert item priority override x.Remove item = remove item override x.Update item priority = @@ -66,3 +69,4 @@ type BidictionaryPriorityQueue<'a when 'a : equality>() = override x.Clear() = clear () override x.Count = uint valuesToPriority.Count override x.ToSeq = valuesToPriority.Keys |> seq + override x.ToSeqWithPriority = valuesToPriority |> Seq.map (|KeyValue|)