Huge refactoring of pretrainng data generation.

VSharp.API/VSharp.cs

@@ -190,8 +190,8 @@ private static Statistics StartExploration(
                     oracle: options.Oracle,
                     coverageToSwitchToAI:options.CoverageToSwitchToAI,
                     stepsToPlay:options.StepsToPlay,
-                    serialize:false,
-                    pathToSerialize:"");
+                    serialize:options.Serialize,
+                    mapName:options.MapName);
 
             var fuzzerOptions =
                 new FuzzerOptions(

VSharp.API/VSharpOptions.cs

@@ -114,6 +114,8 @@ public readonly record struct VSharpOptions
     public readonly Oracle? Oracle = null;
     public readonly uint CoverageToSwitchToAI = 0;
     public readonly uint StepsToPlay = 0;
+    public readonly string MapName = "";
+    public readonly bool Serialize = false;
 
     /// <summary>
     /// Symbolic virtual machine options.
@@ -145,7 +147,9 @@ public VSharpOptions(
         uint stepsLimit = DefaultStepsLimit,
         Oracle? oracle = null,
         uint coverageToSwitchToAI = 0,
-        uint stepsToPlay = 0)
+        uint stepsToPlay = 0,
+        string mapName = "",
+        bool serialize = false)
     {
         Timeout = timeout;
         SolverTimeout = solverTimeout;
@@ -162,6 +166,8 @@ public VSharpOptions(
         Oracle = oracle;
         CoverageToSwitchToAI = coverageToSwitchToAI;
         StepsToPlay = stepsToPlay;
+        MapName = mapName;
+        Serialize = serialize;
     }
 
     /// <summary>

VSharp.Explorer/AISearcher.fs

@@ -5,13 +5,7 @@ open VSharp
 open VSharp.IL.Serializer
 open VSharp.ML.GameServer.Messages
 
-type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, serialize:bool, stepsToPlay:uint, pathToSerialize:string) =
-    let folderToStoreSerializationResult = getFolderToStoreSerializationResult pathToSerialize
-    let fileForExpectedResults = getFileForExpectedResults folderToStoreSerializationResult
-    do
-        if serialize
-        then            
-            System.IO.File.AppendAllLines(fileForExpectedResults, ["GraphID ExpectedStateNumber ExpectedRewardForCoveredInStep ExpectedRewardForVisitedInstructionsInStep TotalReachableRewardFromCurrentState"])
+type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, stepsToPlay:uint) =
     let mutable lastCollectedStatistics = Statistics()
     let mutable (gameState:Option<GameState>) = None
     let mutable useDefaultSearcher = coverageToSwitchToAI > 0u
@@ -51,19 +45,16 @@ type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, serialize:bo
 
                     part1.ToArray()                    
                     |> Array.map (fun s -> State(s.Id
-                                                 , s.Position
-                                                 , s.PredictedUsefulness
+                                                 , s.Position                                                 
                                                  , s.PathConditionSize
                                                  , s.VisitedAgainVertices
                                                  , s.VisitedNotCoveredVerticesInZone
                                                  , s.VisitedNotCoveredVerticesOutOfZone
+                                                 , s.StepWhenMovedLastTime
+                                                 , s.InstructionsVisitedInCurrentBlock
                                                  , s.History
                                                  , s.Children |> Array.filter activeStates.Contains)
                     )
-
-
-
-
 
                 gameState <- Some <| GameState (vertices.ToArray(), states, edges.ToArray())
 
@@ -97,7 +88,7 @@ type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, serialize:bo
         then
             if Seq.length availableStates > 0
             then
-                let gameStateDelta,_ = collectGameStateDelta serialize                
+                let gameStateDelta = collectGameStateDelta ()                
                 updateGameState gameStateDelta
                 let statistics = computeStatistics gameState.Value
                 Application.applicationGraphDelta.Clear()
@@ -107,7 +98,7 @@ type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, serialize:bo
         elif Seq.length availableStates = 0
         then None
         else
-            let gameStateDelta,_ = collectGameStateDelta serialize
+            let gameStateDelta = collectGameStateDelta ()
             updateGameState gameStateDelta
             let statistics = computeStatistics gameState.Value
             if isInAIMode()
@@ -122,11 +113,7 @@ type internal AISearcher(coverageToSwitchToAI: uint, oracle:Oracle, serialize:bo
                     let x,y = oracle.Predict gameState.Value
                     x * 1u<stateId>, y
                 afterFirstAIPeek <- true
-                let state = availableStates |> Seq.tryFind (fun s -> s.internalId = stateId)
-                if serialize
-                then
-                    dumpGameState (System.IO.Path.Combine(folderToStoreSerializationResult , string firstFreeEpisodeNumber)) serialize
-                    saveExpectedResult fileForExpectedResults stateId lastCollectedStatistics statistics
+                let state = availableStates |> Seq.tryFind (fun s -> s.internalId = stateId)                
                 lastCollectedStatistics <- statistics
                 stepsPlayed <- stepsPlayed + 1u
                 match state with

VSharp.Explorer/Explorer.fs

@@ -27,10 +27,9 @@ type private IExplorer =
     abstract member StartExploration: (Method * state) list -> (Method * string[] * state) list -> Task
 
 type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVMStatistics, reporter: IReporter) =
-
-    let mutable stepsCount = 0
-    let options = explorationOptions.svmOptions
-
+    let options = explorationOptions.svmOptions 
+    let folderToStoreSerializationResult =
+        getFolderToStoreSerializationResult explorationOptions.outputDirectory.FullName options.mapName    
     let hasTimeout = explorationOptions.timeout.TotalMilliseconds > 0
 
     let solverTimeout =
@@ -79,7 +78,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
     let rec mkForwardSearcher mode =
         let getRandomSeedOption() = if options.randomSeed < 0 then None else Some options.randomSeed
         match mode with
-        | AIMode -> AISearcher(options.coverageToSwitchToAI, options.oracle.Value, options.serialize, options.stepsToPlay, options.pathToSerialize) :> IForwardSearcher
+        | AIMode -> AISearcher(options.coverageToSwitchToAI, options.oracle.Value, options.stepsToPlay) :> IForwardSearcher
         | BFSMode -> BFSSearcher() :> IForwardSearcher
         | DFSMode -> DFSSearcher() :> IForwardSearcher
         | ShortestDistanceBasedMode -> ShortestDistanceBasedSearcher statistics :> IForwardSearcher
@@ -340,7 +339,11 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
         (* TODO: checking for timeout here is not fine-grained enough (that is, we can work significantly beyond the
                  timeout, but we'll live with it for now. *)
         while not isStopped && not <| isStepsLimitReached() && not <| isTimeoutReached() && pick() do
-            stepsCount <- stepsCount + 1
+            if options.serialize
+            then
+                dumpGameState (System.IO.Path.Combine(folderToStoreSerializationResult, string firstFreeEpisodeNumber))
+                firstFreeEpisodeNumber <- firstFreeEpisodeNumber + 1
+
             if shouldReleaseBranches() then
                 releaseBranches()
             match action with

VSharp.Explorer/Options.fs

@@ -54,7 +54,7 @@ type SVMOptions = {
     coverageToSwitchToAI: uint
     stepsToPlay: uint
     serialize: bool
-    pathToSerialize: string
+    mapName: string
 }
 
 type explorationModeOptions =

VSharp.Explorer/Statistics.fs

@@ -13,6 +13,7 @@ open FSharpx.Collections
 open VSharp
 open VSharp.Core
 open VSharp.Interpreter.IL
+open VSharp.ML.GameServer.Messages
 open VSharp.Utils
 
 open CilState
@@ -160,6 +161,7 @@ type public SVMStatistics(entryMethods : Method seq, generalizeGenericsCoverage
 
     member x.TrackStepForward (s : cilState) (ip : instructionPointer) =
         stepsCount <- stepsCount + 1u
+        s.stepWhenMovedLastTime <- stepsCount * 1u<step>
         Logger.traceWithTag Logger.stateTraceTag $"{stepsCount} FORWARD: {s.internalId}"
 
         let setCoveredIfNeeded (loc : codeLocation) =

VSharp.IL/CFG.fs

@@ -59,6 +59,8 @@ type internal temporaryCallInfo = {callee: MethodWithBody; callFrom: offset; ret
 
 type BasicBlock (method: MethodWithBody, startOffset: offset, id:uint<basicBlockGlobalId>) =
     let mutable finalOffset = startOffset
+    let mutable containsCall = false
+    let mutable containsThrow = false
     let mutable startOffset = startOffset
     let mutable isGoal = false
     let mutable isCovered = false
@@ -108,6 +110,14 @@ type BasicBlock (method: MethodWithBody, startOffset: offset, id:uint<basicBlock
         with get () = finalOffset 
         and set (v: offset) = finalOffset <- v
 
+    member this.ContainsCall
+        with get () = containsCall 
+        and set (v: bool) = containsCall <- v    
+
+    member this.ContainsThrow
+        with get () = containsThrow 
+        and set (v: bool) = containsThrow <- v
+
     member this.GetInstructions() =
         let parsedInstructions = method.ParsedInstructions
         let mutable instr = parsedInstructions[this.StartOffset]
@@ -276,6 +286,7 @@ and CfgInfo internal (method : MethodWithBody, getNextBasicBlockGlobalId: unit -
                 let processCall (callee: MethodWithBody) callFrom returnTo k =
                     calls.Add(currentBasicBlock, CallInfo(callee :?> Method, callFrom, returnTo))
                     currentBasicBlock.FinalOffset <- callFrom
+                    currentBasicBlock.ContainsThrow <- true
                     let newBasicBlock = makeNewBasicBlock returnTo
                     addEdge currentBasicBlock newBasicBlock
                     dfs' newBasicBlock returnTo k
@@ -513,8 +524,10 @@ and IGraphTrackableState =
     abstract member VisitedNotCoveredVerticesInZone: uint with get
     abstract member VisitedNotCoveredVerticesOutOfZone: uint with get
     abstract member VisitedAgainVertices: uint with get
-    abstract member History:  Dictionary<BasicBlock,uint>
-    abstract member Children: array<IGraphTrackableState>  
+    abstract member InstructionsVisitedInCurrentBlock : uint<instruction>  with get, set
+    abstract member History:  Dictionary<BasicBlock,StateHistoryElem>
+    abstract member Children: array<IGraphTrackableState>
+    abstract member StepWhenMovedLastTime: uint<step> with get
 
 module public CodeLocation =
 
@@ -594,9 +607,12 @@ type ApplicationGraph(getNextBasicBlockGlobalId,applicationGraphDelta:Applicatio
         if stateWithNewPosition.History.ContainsKey stateWithNewPosition.CodeLocation.BasicBlock
         then
              if initialPosition.BasicBlock <> stateWithNewPosition.CodeLocation.BasicBlock
-             then stateWithNewPosition.History[stateWithNewPosition.CodeLocation.BasicBlock]
-                    <- stateWithNewPosition.History[stateWithNewPosition.CodeLocation.BasicBlock] + 1u
-        else stateWithNewPosition.History.Add(stateWithNewPosition.CodeLocation.BasicBlock, 1u)
+             then
+                let history = stateWithNewPosition.History[stateWithNewPosition.CodeLocation.BasicBlock]     
+                stateWithNewPosition.History[stateWithNewPosition.CodeLocation.BasicBlock]
+                    <- StateHistoryElem(stateWithNewPosition.CodeLocation.BasicBlock.Id, history.NumOfVisits + 1u, stateWithNewPosition.StepWhenMovedLastTime)
+             else stateWithNewPosition.InstructionsVisitedInCurrentBlock <- stateWithNewPosition.InstructionsVisitedInCurrentBlock + 1u<instruction> 
+        else stateWithNewPosition.History.Add(stateWithNewPosition.CodeLocation.BasicBlock, StateHistoryElem(stateWithNewPosition.CodeLocation.BasicBlock.Id, 1u, stateWithNewPosition.StepWhenMovedLastTime))
         stateWithNewPosition.CodeLocation.BasicBlock.VisitedInstructions <-
             max
                 stateWithNewPosition.CodeLocation.BasicBlock.VisitedInstructions
@@ -613,9 +629,11 @@ type ApplicationGraph(getNextBasicBlockGlobalId,applicationGraphDelta:Applicatio
             //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)
+            if newState.History.ContainsKey newState.CodeLocation.BasicBlock             
+            then
+                let history = newState.History[newState.CodeLocation.BasicBlock]
+                newState.History[newState.CodeLocation.BasicBlock] <- StateHistoryElem(newState.CodeLocation.BasicBlock.Id, history.NumOfVisits + 1u, newState.StepWhenMovedLastTime)
+            else newState.History.Add(newState.CodeLocation.BasicBlock, StateHistoryElem(newState.CodeLocation.BasicBlock.Id, 1u, newState.StepWhenMovedLastTime))
             newState.CodeLocation.BasicBlock.VisitedInstructions <-
                 max
                     newState.CodeLocation.BasicBlock.VisitedInstructions