First version of incremental game state update.

VSharp.Explorer/AISearcher.fs

@@ -1,19 +1,55 @@
 namespace VSharp.Explorer
 
 open System.Collections.Generic
+open VSharp
 open VSharp.IL.Serializer
 open VSharp.ML.GameServer.Messages
-open VSharp.Prelude
 
 type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, serialize:bool) =
     let mutable lastCollectedStatistics = Statistics()
-    let mutable gameState = None
+    let mutable (gameState:Option<GameState>) = None
     let mutable useDefaultSearcher = coverageToSwitchToAI > 0u
     let mutable afterFirstAIPeek = false
     let mutable incorrectPredictedStateId = false
     let defaultSearcher = BFSSearcher() :> IForwardSearcher
     let q = ResizeArray<_>()
     let availableStates = HashSet<_>()
+    let updateGameState (delta:GameState) =
+            match gameState with
+            | None ->
+                gameState <- Some delta
+            | Some s ->
+                let updatedBasicBlocks = delta.GraphVertices |> Array.map (fun b -> b.Id) |> HashSet
+                let updatedStates = delta.States |> Array.map (fun s -> s.Id) |> HashSet
+                let vertices =
+                    s.GraphVertices
+                    |> Array.filter (fun v -> updatedBasicBlocks.Contains v.Id |> not)
+                    |> ResizeArray<_>
+                vertices.AddRange delta.GraphVertices
+                let edges =
+                    s.Map
+                    |> Array.filter (fun e -> updatedBasicBlocks.Contains e.VertexFrom |> not)
+                    |> ResizeArray<_>
+                edges.AddRange delta.Map
+                let activeStates = vertices |> Seq.collect (fun v -> v.States) |> HashSet
+                let states =
+                    s.States |> Array.filter (fun s -> activeStates.Contains s.Id && (not <| updatedStates.Contains s.Id))
+                    |> Array.map (fun s -> State(s.Id
+                                                 , s.Position
+                                                 , s.PredictedUsefulness
+                                                 , s.PathConditionSize
+                                                 , s.VisitedAgainVertices
+                                                 , s.VisitedNotCoveredVerticesInZone
+                                                 , s.VisitedNotCoveredVerticesOutOfZone
+                                                 , s.History
+                                                 , s.Children |> Array.filter activeStates.Contains )
+                    )
+                    |> ResizeArray<_>
+                states.AddRange delta.States
+
+                gameState <- Some <| GameState (vertices.ToArray(), states.ToArray(), edges.ToArray())
+
+
     let init states =
         q.AddRange states
         defaultSearcher.Init q  
@@ -43,17 +79,21 @@ type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, serialize:bo
         then
             if Seq.length availableStates > 0
             then
-                let _,statistics,_ = collectGameState (Seq.head availableStates).CurrentLoc serialize
+                let gameStateDelta,statistics,_ = collectGameStateDelta serialize
+                updateGameState gameStateDelta
+                Application.applicationGraphDelta.Clear()
                 lastCollectedStatistics <- statistics
                 useDefaultSearcher <- (statistics.CoveredVerticesInZone * 100u) / statistics.TotalVisibleVerticesInZone  < coverageToSwitchToAI
             defaultSearcher.Pick()
         elif Seq.length availableStates = 0
         then None
         else            
-            let gameState,statistics,_ = collectGameState (Seq.head availableStates).CurrentLoc serialize
+            let gameStateDelta,statistics,_ = collectGameStateDelta serialize
+            updateGameState gameStateDelta
+            Application.applicationGraphDelta.Clear()
             lastCollectedStatistics <- statistics
-            let stateId, predictedUsefulness =
-                let x,y = oracle.Predict gameState
+            let stateId, _ =
+                let x,y = oracle.Predict gameState.Value
                 x * 1u<stateId>, y
             afterFirstAIPeek <- true
             let state = availableStates |> Seq.tryFind (fun s -> s.internalId = stateId)

VSharp.Explorer/Statistics.fs

@@ -233,6 +233,7 @@ type public SVMStatistics(entryMethods : Method seq, generalizeGenericsCoverage
         let blocks = Seq.distinct blocks
         for block in blocks do
             block.BasicBlock.IsCovered <- true
+            let added = Application.applicationGraphDelta.TouchedBasicBlocks.Add block.BasicBlock 
             let generalizedMethod = generalizeIfNeeded block.method
             let method = block.method
             let mutable isNewBlock = false

VSharp.IL/CFG.fs

@@ -521,7 +521,19 @@ module public CodeLocation =
     let hasSiblings (blockStart : codeLocation) =
         blockStart.method.CFG.HasSiblings blockStart.offset
 
-type ApplicationGraph(getNextBasicBlockGlobalId) =
+type ApplicationGraphDelta() =
+    let loadedMethods = ResizeArray<Method>()
+    let touchedBasicBlocks = HashSet<BasicBlock>()
+    let touchedStates = HashSet<IGraphTrackableState>()
+    member this.LoadedMethods = loadedMethods
+    member this.TouchedBasicBlocks = touchedBasicBlocks
+    member this.TouchedStates = touchedStates
+    member this.Clear() =
+        loadedMethods.Clear()
+        touchedBasicBlocks.Clear()
+        touchedStates.Clear()
+
+type ApplicationGraph(getNextBasicBlockGlobalId,applicationGraphDelta:ApplicationGraphDelta) =
 
     let dummyTerminalForCallEdge = 1<terminalSymbol>
     let dummyTerminalForReturnEdge = 2<terminalSymbol>
@@ -564,6 +576,8 @@ type ApplicationGraph(getNextBasicBlockGlobalId) =
         else ()
 
     let moveState (initialPosition: codeLocation) (stateWithNewPosition: IGraphTrackableState) =
+        let added = applicationGraphDelta.TouchedBasicBlocks.Add initialPosition.BasicBlock
+        let added = applicationGraphDelta.TouchedBasicBlocks.Add stateWithNewPosition.CodeLocation.BasicBlock
         let removed = initialPosition.BasicBlock.AssociatedStates.Remove stateWithNewPosition
         if removed        
         then
@@ -584,9 +598,13 @@ type ApplicationGraph(getNextBasicBlockGlobalId) =
             stateWithNewPosition.CodeLocation.BasicBlock.IsVisited
             || stateWithNewPosition.CodeLocation.offset = stateWithNewPosition.CodeLocation.BasicBlock.FinalOffset
 
-    let addStates (parentState:Option<IGraphTrackableState>) (states:array<IGraphTrackableState>) =
+    let addStates (parentState:Option<IGraphTrackableState>) (states:array<IGraphTrackableState>) = 
+        //Option.iter (applicationGraphDelta.TouchedStates.Add >> ignore) parentState
+        parentState |> Option.iter (fun v -> applicationGraphDelta.TouchedBasicBlocks.Add v.CodeLocation.BasicBlock |> ignore) 
         for newState in states do
-            newState.CodeLocation.BasicBlock.AssociatedStates.Add newState
+            //let added = applicationGraphDelta.TouchedStates.Add newState
+            let added = applicationGraphDelta.TouchedBasicBlocks.Add newState.CodeLocation.BasicBlock
+            let added = newState.CodeLocation.BasicBlock.AssociatedStates.Add newState
             if newState.History.ContainsKey newState.CodeLocation.BasicBlock
             then newState.History[newState.CodeLocation.BasicBlock] <- newState.History[newState.CodeLocation.BasicBlock] + 1u
             else newState.History.Add(newState.CodeLocation.BasicBlock, 1u)
@@ -604,6 +622,7 @@ type ApplicationGraph(getNextBasicBlockGlobalId) =
 
     member this.RegisterMethod (method: Method) =
         assert method.HasBody
+        applicationGraphDelta.LoadedMethods.Add method
 
     member this.AddCallEdge (sourceLocation : codeLocation) (targetLocation : codeLocation) =
         addCallEdge sourceLocation targetLocation
@@ -645,6 +664,7 @@ type NullVisualizer() =
         override x.VisualizeStep _ _ _ = ()
 
 module Application =
+    let applicationGraphDelta = ApplicationGraphDelta()
     let mutable basicBlockGlobalCount = 0u<basicBlockGlobalId>
     let getNextBasicBlockGlobalId () =
         let r = basicBlockGlobalCount
@@ -653,12 +673,13 @@ module Application =
     let private methods = ConcurrentDictionary<methodDescriptor, Method>()
     let private _loadedMethods = ConcurrentDictionary<Method, unit>()
     let loadedMethods = _loadedMethods :> seq<_>
-    let mutable graph = ApplicationGraph(getNextBasicBlockGlobalId)
+    let mutable graph = ApplicationGraph(getNextBasicBlockGlobalId, applicationGraphDelta)
     let mutable visualizer : IVisualizer = NullVisualizer()
 
     let reset () =
+        applicationGraphDelta.Clear()
         basicBlockGlobalCount <- 0u<basicBlockGlobalId>
-        graph <- ApplicationGraph(getNextBasicBlockGlobalId)
+        graph <- ApplicationGraph(getNextBasicBlockGlobalId, applicationGraphDelta)
         methods.Clear()
         _loadedMethods.Clear()
     let getMethod (m : MethodBase) : Method =
@@ -684,8 +705,9 @@ module Application =
         graph.AddForkedStates toState forked
         visualizer.VisualizeStep fromLoc toState forked
 
-    let terminateState state =
+    let terminateState (state: IGraphTrackableState) =
         // TODO: gsv: propagate this into application graph
+        let removed = state.CodeLocation.BasicBlock.AssociatedStates.Remove state
         visualizer.TerminateState state
 
     let addCallEdge = graph.AddCallEdge

VSharp.IL/Serializer.fs

@@ -181,10 +181,10 @@ let getFolderToStoreSerializationResult suffix =
     folderName
 
 let getFileForExpectedResults folderToStoreSerializationResult =
-    let path = System.IO.Path.Combine(folderToStoreSerializationResult,"expectedResults.txt")    
+    let path = System.IO.Path.Combine(folderToStoreSerializationResult, "expectedResults.txt")    
     path
 
-let collectGameState (location:codeLocation) (serialize: bool) =
+let collectGameState (basicBlocks:ResizeArray<BasicBlock>) (serialize: bool) =
     let mutable coveredVerticesInZone = 0u
     let mutable coveredVerticesOutOfZone = 0u
     let mutable visitedVerticesInZone = 0u
@@ -197,11 +197,6 @@ let collectGameState (location:codeLocation) (serialize: bool) =
     let vertices = Dictionary<_,_>()
     let allStates = HashSet<_>()
 
-    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<_>()
 
@@ -326,8 +321,26 @@ let collectGameState (location:codeLocation) (serialize: bool) =
     , Statistics(coveredVerticesInZone,coveredVerticesOutOfZone,visitedVerticesInZone,visitedVerticesOutOfZone,visitedInstructionsInZone,touchedVerticesInZone,touchedVerticesOutOfZone, totalVisibleVerticesInZone)
     , statesInfoToDump
 
+let collectFullGameState serialize =
+    let basicBlocks = ResizeArray<_>()
+    for method in Application.loadedMethods do
+        for basicBlock in method.Key.BasicBlocks do
+            basicBlock.IsGoal <- method.Key.InCoverageZone
+            basicBlocks.Add(basicBlock)
+    collectGameState basicBlocks serialize
+
+let collectGameStateDelta serialize =
+    let basicBlocks = HashSet<_>(Application.applicationGraphDelta.TouchedBasicBlocks)
+    for method in Application.applicationGraphDelta.LoadedMethods do
+        for basicBlock in method.BasicBlocks do
+            basicBlock.IsGoal <- method.InCoverageZone
+            let added = basicBlocks.Add(basicBlock)
+            ()
+    collectGameState (ResizeArray basicBlocks) serialize
+
+
 let dumpGameState (location:codeLocation) fileForResultWithoutExtension serialize =
-    let gameState, statistics, statesInfoToDump = collectGameState location serialize
+    let gameState, statistics, statesInfoToDump = collectFullGameState serialize
     if serialize
     then
         let gameStateJson = JsonSerializer.Serialize gameState