From 621bfa9f5071ca6872d6c25ac6314459f2dc2d53 Mon Sep 17 00:00:00 2001 From: gsv Date: Tue, 1 Aug 2023 12:40:32 +0300 Subject: [PATCH] Avoid extra graph traversals in game state collection. --- VSharp.IL/CFG.fs | 28 ++++++++----- VSharp.IL/Serializer.fs | 68 +++++++------------------------- VSharp.ML.GameServer/Messages.fs | 11 +++--- 3 files changed, 39 insertions(+), 68 deletions(-) diff --git a/VSharp.IL/CFG.fs b/VSharp.IL/CFG.fs index 196a04307..5e8fe6cea 100644 --- a/VSharp.IL/CFG.fs +++ b/VSharp.IL/CFG.fs @@ -2,6 +2,7 @@ namespace VSharp open System.Collections.Concurrent open VSharp.GraphUtils +open VSharp.ML.GameServer.Messages open global.System open System.Reflection open System.Collections.Generic @@ -56,7 +57,7 @@ type EdgeLabel = [] type internal temporaryCallInfo = {callee: MethodWithBody; callFrom: offset; returnTo: offset} -type BasicBlock (method: MethodWithBody, startOffset: offset) as this = +type BasicBlock (method: MethodWithBody, startOffset: offset, id:uint) = let mutable finalOffset = startOffset let mutable startOffset = startOffset let mutable isGoal = false @@ -69,6 +70,7 @@ type BasicBlock (method: MethodWithBody, startOffset: offset) as this = let incomingCallEdges = HashSet() let outgoingEdges = Dictionary, HashSet>() + member this.Id = id member this.StartOffset with get () = startOffset and internal set v = startOffset <- v @@ -165,7 +167,7 @@ and [] CallInfo = ReturnTo = returnTo } -and CfgInfo internal (method : MethodWithBody) = +and CfgInfo internal (method : MethodWithBody, getNextBasicBlockGlobalId: unit -> uint) = let () = assert method.HasBody let ilBytes = method.ILBytes let exceptionHandlers = method.ExceptionHandlers @@ -202,7 +204,7 @@ and CfgInfo internal (method : MethodWithBody) = let splitBasicBlock (block : BasicBlock) intermediatePoint = - let newBlock = BasicBlock(method, block.StartOffset) + let newBlock = BasicBlock(method, block.StartOffset, getNextBasicBlockGlobalId()) addBasicBlock newBlock block.StartOffset <- intermediatePoint @@ -230,7 +232,7 @@ and CfgInfo internal (method : MethodWithBody) = let makeNewBasicBlock startVertex = match vertexToBasicBlock[int startVertex] with | None -> - let newBasicBlock = BasicBlock(method, startVertex) + let newBasicBlock = BasicBlock(method, startVertex, getNextBasicBlockGlobalId()) vertexToBasicBlock[int startVertex] <- Some newBasicBlock addBasicBlock newBasicBlock newBasicBlock @@ -382,12 +384,12 @@ and CfgInfo internal (method : MethodWithBody) = let basicBlock = resolveBasicBlock offset basicBlock.HasSiblings -and Method internal (m : MethodBase) as this = +and Method internal (m : MethodBase,getNextBasicBlockGlobalId) as this = inherit MethodWithBody(m) let cfg = lazy( if this.HasBody then Logger.trace $"Add CFG for {this}." - let cfg = this |> CfgInfo |> Some + let cfg = CfgInfo(this, getNextBasicBlockGlobalId) |> Some Method.ReportCFGLoaded this cfg else None) @@ -526,7 +528,7 @@ module public CodeLocation = | Some cfg -> cfg.HasSiblings blockStart.offset | None -> false -type ApplicationGraph() = +type ApplicationGraph(getNextBasicBlockGlobalId) = let dummyTerminalForCallEdge = 1 let dummyTerminalForReturnEdge = 2 @@ -664,19 +666,25 @@ type NullVisualizer() = override x.VisualizeStep _ _ _ = () module Application = + let mutable basicBlockGlobalCount = 0u + let getNextBasicBlockGlobalId () = + let r = basicBlockGlobalCount + basicBlockGlobalCount <- basicBlockGlobalCount + 1u + r let private methods = ConcurrentDictionary() let private _loadedMethods = ConcurrentDictionary() let loadedMethods = _loadedMethods :> seq<_> - let mutable graph = ApplicationGraph() + let mutable graph = ApplicationGraph(getNextBasicBlockGlobalId) let mutable visualizer : IVisualizer = NullVisualizer() let reset () = - graph <- ApplicationGraph() + basicBlockGlobalCount <- 0u + graph <- ApplicationGraph(getNextBasicBlockGlobalId) methods.Clear() _loadedMethods.Clear() let getMethod (m : MethodBase) : Method = let desc = Reflection.getMethodDescriptor m - Dict.getValueOrUpdate methods desc (fun () -> Method(m)) + Dict.getValueOrUpdate methods desc (fun () -> Method(m,getNextBasicBlockGlobalId)) let setCoverageZone (zone : Method -> bool) = Method.CoverageZone <- zone diff --git a/VSharp.IL/Serializer.fs b/VSharp.IL/Serializer.fs index 01e502831..c6c381e42 100644 --- a/VSharp.IL/Serializer.fs +++ b/VSharp.IL/Serializer.fs @@ -192,64 +192,26 @@ let collectGameState (location:codeLocation) = let mutable visitedInstructionsInZone = 0u let mutable touchedVerticesInZone = 0u let mutable touchedVerticesOutOfZone = 0u - let mutable totalVisibleVerticesInZone = 0u - let mutable firstFreeBasicBlockID = 0u + let mutable totalVisibleVerticesInZone = 0u let vertices = Dictionary<_,_>() let allStates = HashSet<_>() - let basicBlocks = Dictionary<_,_>() - let basicBlocksIds = Dictionary<_,_>() - let visitedMethods = HashSet<_>() - let rec collectFullGraph (method:Method) = - if not <| visitedMethods.Contains method - then - let added = visitedMethods.Add method - assert added - for basicBlock in method.ForceCFG.SortedBasicBlocks do - basicBlock.IsGoal <- method.InCoverageZone - basicBlocks.Add(firstFreeBasicBlockID, basicBlock) - basicBlocksIds.Add(basicBlock, firstFreeBasicBlockID) - firstFreeBasicBlockID <- firstFreeBasicBlockID + + 1u - for state in basicBlock.AssociatedStates do - state.History - |> Seq.iter (fun kvp -> collectFullGraph (kvp.Key.Method :?> Method)) - basicBlock.IncomingCallEdges - |> Seq.iter (fun x -> collectFullGraph (x.Method :?> Method)) - for edge in basicBlock.OutgoingEdges do - for bb in edge.Value do - if bb.Method <> basicBlock.Method - then collectFullGraph (bb.Method :?> Method) - - //(method :> VSharp.ICallGraphNode).OutgoingEdges - //|> Seq.iter (fun x -> collectFullGraph (x:?> Method)) - (method :> VSharp.IReversedCallGraphNode).OutgoingEdges - |> Seq.iter (fun x -> collectFullGraph (x:?> Method)) - collectFullGraph location.method - - let getBasicBlockId = - let basicBlockToIdMap = Dictionary<_,_>() - for kvp in basicBlocks do basicBlockToIdMap.Add(kvp.Value, uint kvp.Key) - fun basicBlock -> - let exists,id = basicBlockToIdMap.TryGetValue basicBlock - if exists - then id - else - let id = uint firstFreeBasicBlockID - firstFreeBasicBlockID <- firstFreeBasicBlockID + 1u - basicBlockToIdMap.Add(basicBlock, id) - id - + let basicBlocks = ResizeArray<_>() + for method in Application.loadedMethods do + for basicBlock in method.Key.BasicBlocks do + basicBlock.IsGoal <- method.Key.InCoverageZone + basicBlocks.Add(basicBlock) + //let statesMetrics = ResizeArray<_>() let activeStates = basicBlocks - |> Seq.collect (fun kvp -> kvp.Value.AssociatedStates) + |> Seq.collect (fun basicBlock -> basicBlock.AssociatedStates) |> Seq.map (fun s -> s.Id) |> fun x -> HashSet x - for kvp in basicBlocks do - let currentBasicBlock = kvp.Value + for currentBasicBlock in basicBlocks do let isCovered = if currentBasicBlock.IsCovered then 1u else 0u if currentBasicBlock.IsGoal then coveredVerticesInZone <- coveredVerticesInZone + isCovered @@ -288,7 +250,7 @@ let collectGameState (location:codeLocation) = s.VisitedAgainVertices, s.VisitedNotCoveredVerticesInZone, s.VisitedNotCoveredVerticesOutOfZone, - s.History |> Seq.map (fun kvp -> StateHistoryElem(getBasicBlockId kvp.Key, kvp.Value)) |> Array.ofSeq, + s.History |> Seq.map (fun kvp -> StateHistoryElem(kvp.Key.Id, kvp.Value)) |> Array.ofSeq, s.Children |> Array.map (fun s -> s.Id) |> Array.filter activeStates.Contains ) |> allStates.Add @@ -300,7 +262,7 @@ let collectGameState (location:codeLocation) = GameMapVertex( 0u, - kvp.Key, + currentBasicBlock.Id, currentBasicBlock.IsGoal, uint <| currentBasicBlock.FinalOffset - currentBasicBlock.StartOffset + 1, currentBasicBlock.IsCovered, @@ -349,11 +311,11 @@ let collectGameState (location:codeLocation) = *) let edges = ResizeArray<_>() - for kvp in basicBlocks do - for outgoingEdges in kvp.Value.OutgoingEdges do + for basicBlock in basicBlocks do + for outgoingEdges in basicBlock.OutgoingEdges do for targetBasicBlock in outgoingEdges.Value do - GameMapEdge (vertices.[kvp.Key].Id, - vertices[basicBlocksIds[targetBasicBlock]].Id, + GameMapEdge (vertices.[basicBlock.Id].Id, + vertices[targetBasicBlock.Id].Id, GameEdgeLabel (int outgoingEdges.Key)) |> edges.Add diff --git a/VSharp.ML.GameServer/Messages.fs b/VSharp.ML.GameServer/Messages.fs index e7bd181a2..583879f78 100644 --- a/VSharp.ML.GameServer/Messages.fs +++ b/VSharp.ML.GameServer/Messages.fs @@ -16,6 +16,8 @@ type IRawOutgoingMessageBody = interface end type [] test type [] error +type [] basicBlockGlobalId + [] type GameOverMessageBody = interface IRawOutgoingMessageBody @@ -57,7 +59,7 @@ type InputMessage = [] type StateHistoryElem = - val GraphVertexId: uint + val GraphVertexId: uint val NumOfVisits: uint new (graphVertexId, numOfVisits) = { @@ -66,7 +68,6 @@ type StateHistoryElem = } type [] stateId -type [] graphVertexId [] type State = @@ -103,7 +104,7 @@ type State = [] type GameMapVertex = val Uid: uint - val Id: uint + val Id: uint val InCoverageZone: bool val BasicBlockSize: uint val CoveredByTest: bool @@ -136,8 +137,8 @@ type GameEdgeLabel = [] type GameMapEdge = - val VertexFrom: uint - val VertexTo: uint + val VertexFrom: uint + val VertexTo: uint val Label: GameEdgeLabel new (vFrom, vTo, label) = {VertexFrom = vFrom; VertexTo = vTo; Label = label}