Fix states attributes calculation (history and children)

PySymGym · Dec 22, 2023 · 5e7da8a · 5e7da8a
1 parent a5efef2
commit 5e7da8a
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 9 deletions.
diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs
@@ -41,7 +41,8 @@ type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, serialize:bo
                 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))
+                    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

diff --git a/VSharp.Explorer/Explorer.fs b/VSharp.Explorer/Explorer.fs
@@ -303,13 +303,13 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
                 goodStates @ iieStates @ errors
             | _ ->
                 sIsStopped <- true
-                goodStates @ iieStates @ errors
-        Application.moveState loc s (Seq.cast<_> newStates)
+                goodStates @ iieStates @ errors        
         for newState in newStates do
             let historyCopy = System.Collections.Generic.Dictionary<_,_>()
             for kvp in s._history do historyCopy.Add(kvp.Key, kvp.Value)
             newState._history <- historyCopy
         s.children <- s.children @ newStates
+        Application.moveState loc s (Seq.cast<_> newStates)
         statistics.TrackFork s newStates
         searcher.UpdateStates s newStates
         if sIsStopped then

diff --git a/VSharp.IL/CFG.fs b/VSharp.IL/CFG.fs
@@ -708,6 +708,8 @@ module Application =
     let terminateState (state: IGraphTrackableState) =
         // TODO: gsv: propagate this into application graph
         let removed = state.CodeLocation.BasicBlock.AssociatedStates.Remove state
+        let added = applicationGraphDelta.TouchedBasicBlocks.Add state.CodeLocation.BasicBlock
+        let added = applicationGraphDelta.TouchedStates.Add state
         visualizer.TerminateState state
 
     let addCallEdge = graph.AddCallEdge

diff --git a/VSharp.IL/Serializer.fs b/VSharp.IL/Serializer.fs
@@ -246,7 +246,7 @@ let collectGameState (basicBlocks:ResizeArray<BasicBlock>) (serialize: bool) =
                       s.VisitedNotCoveredVerticesInZone,
                       s.VisitedNotCoveredVerticesOutOfZone,
                       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
+                      s.Children |> Array.map (fun s -> s.Id) // |> Array.filter activeStates.Contains
                       )
                 |> allStates.Add
                 |> ignore

diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs
@@ -447,10 +447,8 @@ module CilState =
             let clone = { x with state = x.state }
             let mkCilState state' =
                 if LanguagePrimitives.PhysicalEquality state' x.state then x
-                else
-                    let s = clone.Copy(state')
-                    s.internalId <- getNextStateId()
-                    s
+                else clone.Copy(state')
+
             StatedConditionalExecution x.state conditionInvocation
                 (fun state k -> thenBranch (mkCilState state) k)
                 (fun state k -> elseBranch (mkCilState state) k)
@@ -486,7 +484,7 @@ module CilState =
         // -------------------- Changing inner state --------------------
 
         member x.Copy(state : state) =
-            { x with state = state }
+            { x with state = state ;internalId = getNextStateId(); children = [] }
 
         // This function copies cilState, instead of mutation
         member x.ChangeState state' : cilState =