Skip to content

Commit

Permalink
Avoid extra graph traversals in game state collection.
Browse files Browse the repository at this point in the history
  • Loading branch information
@gsvgit
gsvgit committed Aug 1, 2023
1 parent 0b982e8 commit 621bfa9
Show file tree
Hide file tree
Showing 3 changed files with 39 additions and 68 deletions.
28 changes: 18 additions & 10 deletions VSharp.IL/CFG.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -56,7 +57,7 @@ type EdgeLabel =
[<Struct>]
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<basicBlockGlobalId>) =
let mutable finalOffset = startOffset
let mutable startOffset = startOffset
let mutable isGoal = false
Expand All @@ -69,6 +70,7 @@ type BasicBlock (method: MethodWithBody, startOffset: offset) as this =
let incomingCallEdges = HashSet<BasicBlock>()
let outgoingEdges = Dictionary<int<terminalSymbol>, HashSet<BasicBlock>>()

member this.Id = id
member this.StartOffset
with get () = startOffset
and internal set v = startOffset <- v
Expand Down Expand Up @@ -165,7 +167,7 @@ and [<Struct>] CallInfo =
ReturnTo = returnTo
}

and CfgInfo internal (method : MethodWithBody) =
and CfgInfo internal (method : MethodWithBody, getNextBasicBlockGlobalId: unit -> uint<basicBlockGlobalId>) =
let () = assert method.HasBody
let ilBytes = method.ILBytes
let exceptionHandlers = method.ExceptionHandlers
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -526,7 +528,7 @@ module public CodeLocation =
| Some cfg -> cfg.HasSiblings blockStart.offset
| None -> false

type ApplicationGraph() =
type ApplicationGraph(getNextBasicBlockGlobalId) =

let dummyTerminalForCallEdge = 1<terminalSymbol>
let dummyTerminalForReturnEdge = 2<terminalSymbol>
Expand Down Expand Up @@ -664,19 +666,25 @@ type NullVisualizer() =
override x.VisualizeStep _ _ _ = ()

module Application =
let mutable basicBlockGlobalCount = 0u<basicBlockGlobalId>
let getNextBasicBlockGlobalId () =
let r = basicBlockGlobalCount
basicBlockGlobalCount <- basicBlockGlobalCount + 1u<basicBlockGlobalId>
r
let private methods = ConcurrentDictionary<methodDescriptor, Method>()
let private _loadedMethods = ConcurrentDictionary<Method, unit>()
let loadedMethods = _loadedMethods :> seq<_>
let mutable graph = ApplicationGraph()
let mutable graph = ApplicationGraph(getNextBasicBlockGlobalId)
let mutable visualizer : IVisualizer = NullVisualizer()

let reset () =
graph <- ApplicationGraph()
basicBlockGlobalCount <- 0u<basicBlockGlobalId>
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
Expand Down
68 changes: 15 additions & 53 deletions VSharp.IL/Serializer.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<graphVertexId>
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<graphVertexId>
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<graphVertexId>
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
Expand Down Expand Up @@ -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
Expand All @@ -300,7 +262,7 @@ let collectGameState (location:codeLocation) =

GameMapVertex(
0u,
kvp.Key,
currentBasicBlock.Id,
currentBasicBlock.IsGoal,
uint <| currentBasicBlock.FinalOffset - currentBasicBlock.StartOffset + 1<offsets>,
currentBasicBlock.IsCovered,
Expand Down Expand Up @@ -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

Expand Down
11 changes: 6 additions & 5 deletions VSharp.ML.GameServer/Messages.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ type IRawOutgoingMessageBody = interface end
type [<Measure>] test
type [<Measure>] error

type [<Measure>] basicBlockGlobalId

[<Struct>]
type GameOverMessageBody =
interface IRawOutgoingMessageBody
Expand Down Expand Up @@ -57,7 +59,7 @@ type InputMessage =

[<Struct>]
type StateHistoryElem =
val GraphVertexId: uint
val GraphVertexId: uint<basicBlockGlobalId>
val NumOfVisits: uint
new (graphVertexId, numOfVisits) =
{
Expand All @@ -66,7 +68,6 @@ type StateHistoryElem =
}

type [<Measure>] stateId
type [<Measure>] graphVertexId

[<Struct>]
type State =
Expand Down Expand Up @@ -103,7 +104,7 @@ type State =
[<Struct>]
type GameMapVertex =
val Uid: uint
val Id: uint<graphVertexId>
val Id: uint<basicBlockGlobalId>
val InCoverageZone: bool
val BasicBlockSize: uint
val CoveredByTest: bool
Expand Down Expand Up @@ -136,8 +137,8 @@ type GameEdgeLabel =

[<Struct>]
type GameMapEdge =
val VertexFrom: uint<graphVertexId>
val VertexTo: uint<graphVertexId>
val VertexFrom: uint<basicBlockGlobalId>
val VertexTo: uint<basicBlockGlobalId>
val Label: GameEdgeLabel
new (vFrom, vTo, label) = {VertexFrom = vFrom; VertexTo = vTo; Label = label}

Expand Down

0 comments on commit 621bfa9

Please sign in to comment.