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,23 @@ type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, serialize:bo
         then
             if Seq.length availableStates > 0
             then
-                let _,statistics,_ = collectGameState (Seq.head availableStates).approximateLoc serialize
+                let gameStateDelta,_ = collectGameStateDelta serialize                
+                updateGameState gameStateDelta
+                let statistics = computeStatistics gameState.Value
+                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).approximateLoc serialize
+            let gameStateDelta,_ = collectGameStateDelta serialize
+            updateGameState gameStateDelta
+            let statistics = computeStatistics gameState.Value
+            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/Explorer.fs

@@ -359,15 +359,17 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
                             | _ -> None                        
                     let statistics1 =
                         if options.serialize
-                        then Some(dumpGameState s.CurrentLoc (System.IO.Path.Combine(folderToStoreSerializationResult , string firstFreeEpisodeNumber)) options.serialize)
+                        then Some(dumpGameState (System.IO.Path.Combine(folderToStoreSerializationResult , string firstFreeEpisodeNumber)) options.serialize)
                         else None
                     x.Forward(s)                                        
                     match searcher with                        
                     | :? BidirectionalSearcher as searcher ->
                         match searcher.ForwardSearcher with
                         | :? AISearcher as searcher ->
-                            let gameState, statisticsAfterStep,_ = collectGameState s.approximateLoc options.serialize
-                            searcher.LastGameState <- gameState
+                            ///TODO !!! Do not use collectFullGameState
+                            let gameState,_ = collectFullGameState options.serialize
+                            let statisticsAfterStep = computeStatistics gameState
+                            //searcher.LastGameState <- gameState
                             searcher.LastCollectedStatistics <- statisticsAfterStep
                             let reward = computeReward statisticsBeforeStep.Value statisticsAfterStep
                             if searcher.InAIMode
@@ -376,7 +378,8 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
                     | _ -> ()
                     if options.serialize
                     then 
-                        let _,statistics2,_ = collectGameState s.approximateLoc options.serialize
+                        let gameState,_ = collectFullGameState options.serialize
+                        let statistics2 = computeStatistics gameState
                         saveExpectedResult fileForExpectedResults s.internalId statistics1.Value statistics2 
                 with
                 | e ->

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 computeStatistics (gameState:GameState) =
     let mutable coveredVerticesInZone = 0u
     let mutable coveredVerticesOutOfZone = 0u
     let mutable visitedVerticesInZone = 0u
@@ -193,15 +193,36 @@ let collectGameState (location:codeLocation) (serialize: bool) =
     let mutable touchedVerticesInZone = 0u
     let mutable touchedVerticesOutOfZone = 0u
     let mutable totalVisibleVerticesInZone = 0u
+    for v in gameState.GraphVertices do
+        if v.CoveredByTest && v.InCoverageZone
+        then coveredVerticesInZone <- coveredVerticesInZone + 1u
+        if v.CoveredByTest && not v.InCoverageZone
+        then coveredVerticesOutOfZone <- coveredVerticesOutOfZone + 1u               
+
+        if v.VisitedByState && v.InCoverageZone
+        then visitedVerticesInZone <- visitedVerticesInZone + 1u
+        if v.VisitedByState && not v.InCoverageZone
+        then visitedVerticesOutOfZone <- visitedVerticesOutOfZone + 1u
+
+        if v.InCoverageZone
+        then
+            totalVisibleVerticesInZone <- totalVisibleVerticesInZone + 1u
+            visitedInstructionsInZone <- visitedInstructionsInZone + v.BasicBlockSize
+
+        if v.TouchedByState && v.InCoverageZone
+        then touchedVerticesInZone <- touchedVerticesInZone + 1u
+        if v.TouchedByState && not v.InCoverageZone
+        then touchedVerticesOutOfZone <- touchedVerticesOutOfZone + 1u
+
+    Statistics(coveredVerticesInZone,coveredVerticesOutOfZone,visitedVerticesInZone,visitedVerticesOutOfZone,visitedInstructionsInZone,touchedVerticesInZone,touchedVerticesOutOfZone, totalVisibleVerticesInZone)
+
+
+
+let collectGameState (basicBlocks:ResizeArray<BasicBlock>) (serialize: bool) =
 
-    let vertices = Dictionary<_,_>()
+    let vertices = ResizeArray<_>()
     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<_>()
 
@@ -212,31 +233,6 @@ let collectGameState (location:codeLocation) (serialize: bool) =
         |> fun x -> HashSet x
 
     for currentBasicBlock in basicBlocks do        
-        let isCovered = if currentBasicBlock.IsCovered then 1u else 0u
-        if currentBasicBlock.IsGoal
-        then coveredVerticesInZone <- coveredVerticesInZone + isCovered
-        else coveredVerticesOutOfZone <- coveredVerticesOutOfZone + isCovered
-
-        let isVisited = if currentBasicBlock.IsVisited then 1u else 0u
-        if currentBasicBlock.IsGoal
-        then visitedVerticesInZone <- visitedVerticesInZone + isVisited
-        else visitedVerticesOutOfZone <- visitedVerticesOutOfZone + isVisited
-
-        let isTouched = if currentBasicBlock.IsTouched then 1u else 0u
-        if currentBasicBlock.IsGoal
-        then touchedVerticesInZone <- touchedVerticesInZone + isTouched
-        else touchedVerticesOutOfZone <- touchedVerticesOutOfZone + isTouched        
-
-        if currentBasicBlock.IsGoal
-        then totalVisibleVerticesInZone <- totalVisibleVerticesInZone + 1u
-
-        if currentBasicBlock.IsVisited
-        then
-            visitedInstructionsInZone <- visitedInstructionsInZone + uint (currentBasicBlock.BlockSize)
-        elif currentBasicBlock.IsTouched
-        then
-            visitedInstructionsInZone <- visitedInstructionsInZone + currentBasicBlock.VisitedInstructions
-
         let interproceduralGraphDistanceFrom = Dictionary<Assembly, GraphUtils.distanceCache<IInterproceduralCfgNode>>()
 
         let states =
@@ -270,7 +266,7 @@ let collectGameState (location:codeLocation) (serialize: bool) =
             currentBasicBlock.IsVisited,
             currentBasicBlock.IsTouched,
             states)
-        |> (fun x -> vertices.Add(x.Id,x))
+        |> vertices.Add
 
     let statesInfoToDump =
         if serialize
@@ -317,24 +313,41 @@ let collectGameState (location:codeLocation) (serialize: bool) =
     for basicBlock in basicBlocks do
         for outgoingEdges in basicBlock.OutgoingEdges do
             for targetBasicBlock in outgoingEdges.Value do
-                GameMapEdge (vertices.[basicBlock.Id].Id,
-                             vertices[targetBasicBlock.Id].Id,
+                GameMapEdge (basicBlock.Id,
+                             targetBasicBlock.Id,
                              GameEdgeLabel (int outgoingEdges.Key))
                 |> edges.Add
 
-    GameState (vertices.Values |> Array.ofSeq, allStates |> Array.ofSeq, edges.ToArray())
-    , Statistics(coveredVerticesInZone,coveredVerticesOutOfZone,visitedVerticesInZone,visitedVerticesOutOfZone,visitedInstructionsInZone,touchedVerticesInZone,touchedVerticesOutOfZone, totalVisibleVerticesInZone)
+    GameState (vertices.ToArray(), allStates |> Array.ofSeq, edges.ToArray())    
     , statesInfoToDump
 
-let dumpGameState (location:codeLocation) fileForResultWithoutExtension serialize =
-    let gameState, statistics, statesInfoToDump = collectGameState location serialize
+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 fileForResultWithoutExtension serialize =
+    let gameState, statesInfoToDump = collectFullGameState serialize
     if serialize
     then
         let gameStateJson = JsonSerializer.Serialize gameState        
         let statesInfoJson = JsonSerializer.Serialize statesInfoToDump.Value
         System.IO.File.WriteAllText(fileForResultWithoutExtension + "_gameState",gameStateJson)
         System.IO.File.WriteAllText(fileForResultWithoutExtension + "_statesInfo",statesInfoJson)
-    statistics
+    computeStatistics gameState
 
 let computeReward (statisticsBeforeStep:Statistics) (statisticsAfterStep:Statistics) =
     let rewardForCoverage =