diff --git a/VSharp.API/VSharp.cs b/VSharp.API/VSharp.cs index f6b186161..3990084d4 100644 --- a/VSharp.API/VSharp.cs +++ b/VSharp.API/VSharp.cs @@ -191,7 +191,7 @@ private static Statistics StartExploration( stopOnCoverageAchieved: 100, randomSeed: options.RandomSeed, stepsLimit: options.StepsLimit, - aiAgentTrainingOptions: options.AIAgentTrainingOptions == null ? FSharpOption.None : FSharpOption.Some(options.AIAgentTrainingOptions), + aiOptions: options.AIOptions == null ? FSharpOption.None : FSharpOption.Some(options.AIOptions), pathToModel: options.PathToModel == null ? FSharpOption.None : FSharpOption.Some(options.PathToModel), useGPU: options.UseGPU == null ? FSharpOption.None : FSharpOption.Some(options.UseGPU), optimize: options.Optimize == null ? FSharpOption.None : FSharpOption.Some(options.Optimize) diff --git a/VSharp.API/VSharpOptions.cs b/VSharp.API/VSharpOptions.cs index 7d6d7901b..c26eca6ef 100644 --- a/VSharp.API/VSharpOptions.cs +++ b/VSharp.API/VSharpOptions.cs @@ -113,7 +113,7 @@ public readonly record struct VSharpOptions public readonly bool ReleaseBranches = DefaultReleaseBranches; public readonly int RandomSeed = DefaultRandomSeed; public readonly uint StepsLimit = DefaultStepsLimit; - public readonly AIAgentTrainingOptions AIAgentTrainingOptions = null; + public readonly AIOptions? AIOptions = null; public readonly string PathToModel = DefaultPathToModel; public readonly bool UseGPU = false; public readonly bool Optimize = false; @@ -133,7 +133,7 @@ public readonly record struct VSharpOptions /// If true and timeout is specified, a part of allotted time in the end is given to execute remaining states without branching. /// Fixed seed for random operations. Used if greater than or equal to zero. /// Number of symbolic machine steps to stop execution after. Zero value means no limit. - /// Settings for AI searcher training. + /// Settings for AI searcher training. /// Path to ONNX file with model to use in AI searcher. /// Specifies whether the ONNX execution session should use a CUDA-enabled GPU. /// Enabling options like parallel execution and various graph transformations to enhance performance of ONNX. @@ -150,7 +150,7 @@ public VSharpOptions( bool releaseBranches = DefaultReleaseBranches, int randomSeed = DefaultRandomSeed, uint stepsLimit = DefaultStepsLimit, - AIAgentTrainingOptions aiAgentTrainingOptions = null, + AIOptions? aiOptions = null, string pathToModel = DefaultPathToModel, bool useGPU = false, bool optimize = false) @@ -167,7 +167,7 @@ public VSharpOptions( ReleaseBranches = releaseBranches; RandomSeed = randomSeed; StepsLimit = stepsLimit; - AIAgentTrainingOptions = aiAgentTrainingOptions; + AIOptions = aiOptions; PathToModel = pathToModel; UseGPU = useGPU; Optimize = optimize; diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index 80c30d426..6e5739fd4 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -2,64 +2,78 @@ namespace VSharp.Explorer open System.Collections.Generic open Microsoft.ML.OnnxRuntime +open System.Text.Json open VSharp open VSharp.IL.Serializer open VSharp.ML.GameServer.Messages +open System.IO -type internal AISearcher(oracle : Oracle, aiAgentTrainingOptions : Option) = +type AIMode = + | Runner + | TrainingSendModel + | TrainingSendEachStep + +type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option) = let stepsToSwitchToAI = - match aiAgentTrainingOptions with + match aiAgentTrainingMode with | None -> 0u - | Some options -> options.stepsToSwitchToAI + | Some(SendModel options) -> options.aiAgentTrainingOptions.stepsToSwitchToAI + | Some(SendEachStep options) -> options.aiAgentTrainingOptions.stepsToSwitchToAI let stepsToPlay = - match aiAgentTrainingOptions with + match aiAgentTrainingMode with | None -> 0u - | Some options -> options.stepsToPlay + | Some(SendModel options) -> options.aiAgentTrainingOptions.stepsToPlay + | Some(SendEachStep options) -> options.aiAgentTrainingOptions.stepsToPlay - let mutable lastCollectedStatistics = - Statistics () + let mutable lastCollectedStatistics = Statistics() let mutable defaultSearcherSteps = 0u - let mutable (gameState : Option) = - None - let mutable useDefaultSearcher = - stepsToSwitchToAI > 0u + let mutable (gameState: Option) = None + let mutable useDefaultSearcher = stepsToSwitchToAI > 0u let mutable afterFirstAIPeek = false - let mutable incorrectPredictedStateId = - false + let mutable incorrectPredictedStateId = false + let defaultSearcher = - match aiAgentTrainingOptions with - | None -> BFSSearcher () :> IForwardSearcher - | Some options -> - match options.defaultSearchStrategy with - | BFSMode -> BFSSearcher () :> IForwardSearcher - | DFSMode -> DFSSearcher () :> IForwardSearcher + let pickSearcher = + function + | BFSMode -> BFSSearcher() :> IForwardSearcher + | DFSMode -> DFSSearcher() :> IForwardSearcher | x -> failwithf $"Unexpected default searcher {x}. DFS and BFS supported for now." + + match aiAgentTrainingMode with + | None -> BFSSearcher() :> IForwardSearcher + | Some(SendModel options) -> pickSearcher options.aiAgentTrainingOptions.aiBaseOptions.defaultSearchStrategy + | Some(SendEachStep options) -> pickSearcher options.aiAgentTrainingOptions.aiBaseOptions.defaultSearchStrategy + let mutable stepsPlayed = 0u + let isInAIMode () = (not useDefaultSearcher) && afterFirstAIPeek - let q = ResizeArray<_> () - let availableStates = HashSet<_> () - let updateGameState (delta : GameState) = + + 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 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 activeStates = vertices |> Seq.collect (fun v -> v.States) |> HashSet let states = let part1 = @@ -69,9 +83,9 @@ type internal AISearcher(oracle : Oracle, aiAgentTrainingOptions : Option Array.map (fun s -> - State ( + State( s.Id, s.Position, s.PathConditionSize, @@ -82,101 +96,134 @@ type internal AISearcher(oracle : Oracle, aiAgentTrainingOptions : Option Array.filter activeStates.Contains - ) - ) - - gameState <- Some <| GameState (vertices.ToArray (), states, edges.ToArray ()) + )) + gameState <- Some <| GameState(vertices.ToArray(), states, edges.ToArray()) let init states = q.AddRange states defaultSearcher.Init q states |> Seq.iter (availableStates.Add >> ignore) + let reset () = - defaultSearcher.Reset () + defaultSearcher.Reset() defaultSearcherSteps <- 0u - lastCollectedStatistics <- Statistics () + lastCollectedStatistics <- Statistics() gameState <- None afterFirstAIPeek <- false incorrectPredictedStateId <- false useDefaultSearcher <- stepsToSwitchToAI > 0u - q.Clear () - availableStates.Clear () + q.Clear() + availableStates.Clear() + let update (parent, newSates) = if useDefaultSearcher then - defaultSearcher.Update (parent, newSates) + defaultSearcher.Update(parent, newSates) + newSates |> Seq.iter (availableStates.Add >> ignore) + let remove state = if useDefaultSearcher then defaultSearcher.Remove state + let removed = availableStates.Remove state assert removed + for bb in state._history do bb.Key.AssociatedStates.Remove state |> ignore - let inTrainMode = - aiAgentTrainingOptions.IsSome + let aiMode = + match aiAgentTrainingMode with + | Some(SendEachStep _) -> TrainingSendEachStep + | Some(SendModel _) -> TrainingSendModel + | None -> Runner let pick selector = if useDefaultSearcher then defaultSearcherSteps <- defaultSearcherSteps + 1u + if Seq.length availableStates > 0 then - let gameStateDelta = - collectGameStateDelta () + let gameStateDelta = collectGameStateDelta () updateGameState gameStateDelta - let statistics = - computeStatistics gameState.Value - Application.applicationGraphDelta.Clear () + let statistics = computeStatistics gameState.Value + Application.applicationGraphDelta.Clear() lastCollectedStatistics <- statistics useDefaultSearcher <- defaultSearcherSteps < stepsToSwitchToAI - defaultSearcher.Pick () + + defaultSearcher.Pick() elif Seq.length availableStates = 0 then None elif Seq.length availableStates = 1 then - Some (Seq.head availableStates) + Some(Seq.head availableStates) else - let gameStateDelta = - collectGameStateDelta () + let gameStateDelta = collectGameStateDelta () updateGameState gameStateDelta - let statistics = - computeStatistics gameState.Value + let statistics = computeStatistics gameState.Value + if isInAIMode () then - let reward = - computeReward lastCollectedStatistics statistics - oracle.Feedback (Feedback.MoveReward reward) - Application.applicationGraphDelta.Clear () - if inTrainMode && stepsToPlay = stepsPlayed then + let reward = computeReward lastCollectedStatistics statistics + oracle.Feedback(Feedback.MoveReward reward) + + Application.applicationGraphDelta.Clear() + + if stepsToPlay = stepsPlayed then None else let toPredict = - if inTrainMode && stepsPlayed > 0u then - gameStateDelta - else - gameState.Value + match aiMode with + | TrainingSendEachStep -> + if stepsPlayed > 0u then + gameStateDelta + else + gameState.Value + | TrainingSendModel + | Runner -> gameState.Value + let stateId = oracle.Predict toPredict afterFirstAIPeek <- true - let state = - availableStates |> Seq.tryFind (fun s -> s.internalId = stateId) + let state = availableStates |> Seq.tryFind (fun s -> s.internalId = stateId) lastCollectedStatistics <- statistics stepsPlayed <- stepsPlayed + 1u + match state with | Some state -> Some state | None -> incorrectPredictedStateId <- true - oracle.Feedback (Feedback.IncorrectPredictedStateId stateId) + oracle.Feedback(Feedback.IncorrectPredictedStateId stateId) None - new(pathToONNX : string, useGPU : bool, optimize : bool) = + new + ( + pathToONNX: string, + useGPU: bool, + optimize: bool, + aiAgentTrainingModelOptions: Option + ) = let numOfVertexAttributes = 7 let numOfStateAttributes = 7 let numOfHistoryEdgeAttributes = 2 - let createOracle (pathToONNX : string) = + let serializeOutput (output: IDisposableReadOnlyCollection) = + let arrayOutput = + seq { 0 .. output.Count - 1 } + |> Seq.map (fun i -> output[i].GetTensorDataAsSpan().ToArray()) + + let arrayOutputJson = JsonSerializer.Serialize arrayOutput + arrayOutputJson + + let writeStep (gameState: GameState) (output: IDisposableReadOnlyCollection) (filePath: string) = + let gameStateJson = JsonSerializer.Serialize gameState + let stateJson = serializeOutput output + File.WriteAllText(filePath + "_gameState", gameStateJson) + File.WriteAllText(filePath + "_nn_output", stateJson) + + let createOracleRunner (pathToONNX: string, aiAgentTrainingModelOptions: Option) = + let sessionOptions = if useGPU then - SessionOptions.MakeSessionOptionWithCudaProvider (0) + SessionOptions.MakeSessionOptionWithCudaProvider(0) else - new SessionOptions () + new SessionOptions() if optimize then sessionOptions.ExecutionMode <- ExecutionMode.ORT_PARALLEL @@ -184,85 +231,51 @@ type internal AISearcher(oracle : Oracle, aiAgentTrainingOptions : Option, int> () - let verticesIds = - Dictionary, int> () + let predict (gameState: GameState) = + let stateIds = Dictionary, int>() + let verticesIds = Dictionary, int>() let networkInput = - let res = Dictionary<_, _> () + let res = Dictionary<_, _>() + let gameVertices = - let shape = - [| - int64 gameState.GraphVertices.Length - numOfVertexAttributes - |] + let shape = [| int64 gameState.GraphVertices.Length; numOfVertexAttributes |] + let attributes = Array.zeroCreate (gameState.GraphVertices.Length * numOfVertexAttributes) + for i in 0 .. gameState.GraphVertices.Length - 1 do let v = gameState.GraphVertices.[i] - verticesIds.Add (v.Id, i) + verticesIds.Add(v.Id, i) let j = i * numOfVertexAttributes - attributes.[j] <- - float32 - <| if v.InCoverageZone then - 1u - else - 0u + attributes.[j] <- float32 <| if v.InCoverageZone then 1u else 0u attributes.[j + 1] <- float32 <| v.BasicBlockSize - attributes.[j + 2] <- - float32 - <| if v.CoveredByTest then - 1u - else - 0u - attributes.[j + 3] <- - float32 - <| if v.VisitedByState then - 1u - else - 0u - attributes.[j + 4] <- - float32 - <| if v.TouchedByState then - 1u - else - 0u - attributes.[j + 5] <- - float32 - <| if v.ContainsCall then - 1u - else - 0u - attributes.[j + 6] <- - float32 - <| if v.ContainsThrow then - 1u - else - 0u - OrtValue.CreateTensorValueFromMemory (attributes, shape) + attributes.[j + 2] <- float32 <| if v.CoveredByTest then 1u else 0u + attributes.[j + 3] <- float32 <| if v.VisitedByState then 1u else 0u + attributes.[j + 4] <- float32 <| if v.TouchedByState then 1u else 0u + attributes.[j + 5] <- float32 <| if v.ContainsCall then 1u else 0u + attributes.[j + 6] <- float32 <| if v.ContainsThrow then 1u else 0u + + OrtValue.CreateTensorValueFromMemory(attributes, shape) let states, numOfParentOfEdges, numOfHistoryEdges = let mutable numOfParentOfEdges = 0 let mutable numOfHistoryEdges = 0 - let shape = - [| - int64 gameState.States.Length - numOfStateAttributes - |] - let attributes = - Array.zeroCreate (gameState.States.Length * numOfStateAttributes) + let shape = [| int64 gameState.States.Length; numOfStateAttributes |] + let attributes = Array.zeroCreate (gameState.States.Length * numOfStateAttributes) + for i in 0 .. gameState.States.Length - 1 do let v = gameState.States.[i] numOfHistoryEdges <- numOfHistoryEdges + v.History.Length numOfParentOfEdges <- numOfParentOfEdges + v.Children.Length - stateIds.Add (v.Id, i) + stateIds.Add(v.Id, i) let j = i * numOfStateAttributes attributes.[j] <- float32 v.Position attributes.[j + 1] <- float32 v.PathConditionSize @@ -271,86 +284,74 @@ type internal AISearcher(oracle : Oracle, aiAgentTrainingOptions : Option Array.iteri (fun i e -> index[i] <- int64 verticesIds[e.VertexFrom] index[gameState.Map.Length + i] <- int64 verticesIds[e.VertexTo] - attributes[i] <- int64 e.Label.Token - ) + attributes[i] <- int64 e.Label.Token) - OrtValue.CreateTensorValueFromMemory (index, shapeOfIndex), - OrtValue.CreateTensorValueFromMemory (attributes, shapeOfAttributes) + OrtValue.CreateTensorValueFromMemory(index, shapeOfIndex), + OrtValue.CreateTensorValueFromMemory(attributes, shapeOfAttributes) let historyEdgesIndex_vertexToState, historyEdgesAttributes, parentOfEdges = - let shapeOfParentOf = - [| 2L ; numOfParentOfEdges |] - let parentOf = - Array.zeroCreate (2 * numOfParentOfEdges) - let shapeOfHistory = - [| 2L ; numOfHistoryEdges |] - let historyIndex_vertexToState = - Array.zeroCreate (2 * numOfHistoryEdges) + let shapeOfParentOf = [| 2L; numOfParentOfEdges |] + let parentOf = Array.zeroCreate (2 * numOfParentOfEdges) + let shapeOfHistory = [| 2L; numOfHistoryEdges |] + let historyIndex_vertexToState = Array.zeroCreate (2 * numOfHistoryEdges) + let shapeOfHistoryAttributes = - [| - int64 numOfHistoryEdges - int64 numOfHistoryEdgeAttributes - |] - let historyAttributes = - Array.zeroCreate (2 * numOfHistoryEdges) + [| int64 numOfHistoryEdges; int64 numOfHistoryEdgeAttributes |] + + let historyAttributes = Array.zeroCreate (2 * numOfHistoryEdges) let mutable firstFreePositionInParentsOf = 0 - let mutable firstFreePositionInHistoryIndex = - 0 - let mutable firstFreePositionInHistoryAttributes = - 0 + let mutable firstFreePositionInHistoryIndex = 0 + let mutable firstFreePositionInHistoryAttributes = 0 + gameState.States |> Array.iter (fun state -> state.Children |> Array.iteri (fun i children -> let j = firstFreePositionInParentsOf + i parentOf[j] <- int64 stateIds[state.Id] - parentOf[numOfParentOfEdges + j] <- int64 stateIds[children] - ) + parentOf[numOfParentOfEdges + j] <- int64 stateIds[children]) + firstFreePositionInParentsOf <- firstFreePositionInParentsOf + state.Children.Length + state.History |> Array.iteri (fun i historyElem -> let j = firstFreePositionInHistoryIndex + i historyIndex_vertexToState[j] <- int64 verticesIds[historyElem.GraphVertexId] historyIndex_vertexToState[numOfHistoryEdges + j] <- int64 stateIds[state.Id] - let j = - firstFreePositionInHistoryAttributes + numOfHistoryEdgeAttributes * i + let j = firstFreePositionInHistoryAttributes + numOfHistoryEdgeAttributes * i historyAttributes[j] <- int64 historyElem.NumOfVisits - historyAttributes[j + 1] <- int64 historyElem.StepWhenVisitedLastTime - ) + historyAttributes[j + 1] <- int64 historyElem.StepWhenVisitedLastTime) + firstFreePositionInHistoryIndex <- firstFreePositionInHistoryIndex + state.History.Length + firstFreePositionInHistoryAttributes <- firstFreePositionInHistoryAttributes - + numOfHistoryEdgeAttributes * state.History.Length - ) + + numOfHistoryEdgeAttributes * state.History.Length) - OrtValue.CreateTensorValueFromMemory (historyIndex_vertexToState, shapeOfHistory), - OrtValue.CreateTensorValueFromMemory (historyAttributes, shapeOfHistoryAttributes), - OrtValue.CreateTensorValueFromMemory (parentOf, shapeOfParentOf) + OrtValue.CreateTensorValueFromMemory(historyIndex_vertexToState, shapeOfHistory), + OrtValue.CreateTensorValueFromMemory(historyAttributes, shapeOfHistoryAttributes), + OrtValue.CreateTensorValueFromMemory(parentOf, shapeOfParentOf) let statePosition_stateToVertex, statePosition_vertexToState = - let data_stateToVertex = - Array.zeroCreate (2 * gameState.States.Length) - let data_vertexToState = - Array.zeroCreate (2 * gameState.States.Length) - let shape = - [| 2L ; gameState.States.Length |] + let data_stateToVertex = Array.zeroCreate (2 * gameState.States.Length) + let data_vertexToState = Array.zeroCreate (2 * gameState.States.Length) + let shape = [| 2L; gameState.States.Length |] let mutable firstFreePosition = 0 + gameState.GraphVertices |> Array.iter (fun v -> v.States @@ -362,46 +363,56 @@ type internal AISearcher(oracle : Oracle, aiAgentTrainingOptions : Option().ToArray () + let output = session.Run(runOptions, networkInput, session.OutputNames) + + let _ = + match aiAgentTrainingModelOptions with + | Some options -> writeStep gameState output (options.outputDirectory + ($"/{stepsPlayed}")) + | None -> () - let id = - weighedStates |> Array.mapi (fun i v -> i, v) |> Array.maxBy snd |> fst + stepsPlayed <- stepsPlayed + 1 + + let weighedStates = output[0].GetTensorDataAsSpan().ToArray() + + let id = weighedStates |> Array.mapi (fun i v -> i, v) |> Array.maxBy snd |> fst stateIds |> Seq.find (fun kvp -> kvp.Value = id) |> (fun x -> x.Key) - Oracle (predict, feedback) + Oracle(predict, feedback) + + let aiAgentTrainingOptions = + match aiAgentTrainingModelOptions with + | Some aiAgentTrainingModelOptions -> Some(SendModel aiAgentTrainingModelOptions) + | None -> None - AISearcher (createOracle pathToONNX, None) + AISearcher(createOracleRunner (pathToONNX, aiAgentTrainingModelOptions), aiAgentTrainingOptions) interface IForwardSearcher with override x.Init states = init states - override x.Pick () = pick (always true) + override x.Pick() = pick (always true) override x.Pick selector = pick selector - override x.Update (parent, newStates) = update (parent, newStates) - override x.States () = availableStates - override x.Reset () = reset () + override x.Update(parent, newStates) = update (parent, newStates) + override x.States() = availableStates + override x.Reset() = reset () override x.Remove cilState = remove cilState override x.StatesCount = availableStates.Count diff --git a/VSharp.Explorer/Explorer.fs b/VSharp.Explorer/Explorer.fs index 29399ec3d..f116e1645 100644 --- a/VSharp.Explorer/Explorer.fs +++ b/VSharp.Explorer/Explorer.fs @@ -12,30 +12,25 @@ open VSharp.Core open VSharp.Interpreter.IL open CilState open VSharp.Explorer -open VSharp.ML.GameServer.Messages open VSharp.Solver open VSharp.IL.Serializer type IReporter = - abstract member ReportFinished : UnitTest -> unit - abstract member ReportException : UnitTest -> unit - abstract member ReportIIE : InsufficientInformationException -> unit - abstract member ReportInternalFail : Method -> Exception -> unit - abstract member ReportCrash : Exception -> unit + abstract member ReportFinished: UnitTest -> unit + abstract member ReportException: UnitTest -> unit + abstract member ReportIIE: InsufficientInformationException -> unit + abstract member ReportInternalFail: Method -> Exception -> unit + abstract member ReportCrash: Exception -> unit -type EntryPointConfiguration(mainArguments : string[]) = +type EntryPointConfiguration(mainArguments: string[]) = - member x.Args = - if mainArguments = null then - None - else - Some mainArguments + member x.Args = if mainArguments = null then None else Some mainArguments type WebConfiguration - (mainArguments : string[], environmentName : string, contentRootPath : DirectoryInfo, applicationName : string) = + (mainArguments: string[], environmentName: string, contentRootPath: DirectoryInfo, applicationName: string) = inherit EntryPointConfiguration(mainArguments) - member internal x.ToWebConfig () = + member internal x.ToWebConfig() = { environmentName = environmentName contentRootPath = contentRootPath @@ -43,20 +38,27 @@ type WebConfiguration } type private IExplorer = - abstract member Reset : seq -> unit - abstract member StartExploration : (Method * state) list -> (Method * EntryPointConfiguration * state) list -> Task + abstract member Reset: seq -> unit + abstract member StartExploration: (Method * state) list -> (Method * EntryPointConfiguration * state) list -> Task -type private SVMExplorer(explorationOptions : ExplorationOptions, statistics : SVMStatistics, reporter : IReporter) = +type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVMStatistics, reporter: IReporter) = let options = explorationOptions.svmOptions + let folderToStoreSerializationResult = - match options.aiAgentTrainingOptions with - | None -> "" - | Some options -> + match options.aiOptions with + | Some((Training trainingOptions)) -> + let mapName = + match trainingOptions with + | SendModel aiAgentTrainingModelOptions -> + aiAgentTrainingModelOptions.aiAgentTrainingOptions.aiBaseOptions.mapName + | SendEachStep aiOptions -> aiOptions.aiAgentTrainingOptions.aiBaseOptions.mapName + getFolderToStoreSerializationResult (Path.GetDirectoryName explorationOptions.outputDirectory.FullName) - options.mapName - let hasTimeout = - explorationOptions.timeout.TotalMilliseconds > 0 + mapName + | _ -> "" + + let hasTimeout = explorationOptions.timeout.TotalMilliseconds > 0 let solverTimeout = if options.solverTimeout > 0 then @@ -70,41 +72,38 @@ type private SVMExplorer(explorationOptions : ExplorationOptions, statistics : S -1 let branchReleaseTimeout = - let doubleTimeout = - double explorationOptions.timeout.TotalMilliseconds - if not hasTimeout then - Double.PositiveInfinity - elif not options.releaseBranches then - doubleTimeout - else - doubleTimeout * 80.0 / 100.0 + let doubleTimeout = double explorationOptions.timeout.TotalMilliseconds + + if not hasTimeout then Double.PositiveInfinity + elif not options.releaseBranches then doubleTimeout + else doubleTimeout * 80.0 / 100.0 let hasStepsLimit = options.stepsLimit > 0u do - API.ConfigureSolver (SolverPool.mkSolver (solverTimeout)) - VSharp.System.SetUp.ConfigureInternalCalls () - API.ConfigureChars (options.prettyChars) + API.ConfigureSolver(SolverPool.mkSolver (solverTimeout)) + VSharp.System.SetUp.ConfigureInternalCalls() + API.ConfigureChars(options.prettyChars) let mutable branchesReleased = false let mutable isStopped = false - let mutable isCoverageAchieved : unit -> bool = - always false + let mutable isCoverageAchieved: unit -> bool = always false - let emptyState = - Memory.EmptyIsolatedState () - let interpreter = ILInterpreter () + let emptyState = Memory.EmptyIsolatedState() + let interpreter = ILInterpreter() do if options.visualize then DotVisualizer explorationOptions.outputDirectory :> IVisualizer |> Application.setVisualizer + SetMaxBuferSize options.maxBufferSize TestGenerator.setMaxBufferSize options.maxBufferSize let isSat pc = // TODO: consider trivial cases emptyState.pc <- pc + match SolverInteraction.checkSat emptyState with | SolverInteraction.SmtSat _ | SolverInteraction.SmtUnknown _ -> true @@ -116,115 +115,127 @@ type private SVMExplorer(explorationOptions : ExplorationOptions, statistics : S None else Some options.randomSeed + match mode with | AIMode -> - match options.aiAgentTrainingOptions with + let useGPU = + if options.useGPU.IsSome then + options.useGPU.Value + else + false + + let optimize = + if options.optimize.IsSome then + options.optimize.Value + else + false + + match options.aiOptions with | Some aiOptions -> - match aiOptions.oracle with - | Some oracle -> AISearcher (oracle, options.aiAgentTrainingOptions) :> IForwardSearcher - | None -> failwith "Empty oracle for AI searcher." + match aiOptions with + | Training aiAgentTrainingOptions -> + match aiAgentTrainingOptions with + | SendEachStep aiAgentTrainingEachStepOptions -> + match aiAgentTrainingEachStepOptions.aiAgentTrainingOptions.oracle with + | Some oracle -> AISearcher(oracle, Some aiAgentTrainingOptions) :> IForwardSearcher + | None -> failwith "Empty oracle for AI searcher training (send each step mode)." + | SendModel aiAgentTrainingModelOptions -> + match options.pathToModel with + | Some path -> + AISearcher(path, useGPU, optimize, Some aiAgentTrainingModelOptions) :> IForwardSearcher + | None -> failwith "Empty model for AI searcher training (send model mode)." + | DatasetGenerator aiOptions -> mkForwardSearcher aiOptions.defaultSearchStrategy | None -> match options.pathToModel with - | Some s -> - let useGPU = - if options.useGPU.IsSome then - options.useGPU.Value - else - false - - let optimize = - if options.optimize.IsSome then - options.optimize.Value - else - false - - AISearcher (s, useGPU, optimize) + | Some s -> AISearcher(s, useGPU, optimize, None) | None -> failwith "Empty model for AI searcher." - | BFSMode -> BFSSearcher () :> IForwardSearcher - | DFSMode -> DFSSearcher () :> IForwardSearcher + | BFSMode -> BFSSearcher() :> IForwardSearcher + | DFSMode -> DFSSearcher() :> IForwardSearcher | ShortestDistanceBasedMode -> ShortestDistanceBasedSearcher statistics :> IForwardSearcher | RandomShortestDistanceBasedMode -> - RandomShortestDistanceBasedSearcher (statistics, getRandomSeedOption ()) :> IForwardSearcher + RandomShortestDistanceBasedSearcher(statistics, getRandomSeedOption ()) :> IForwardSearcher | ContributedCoverageMode -> DFSSortedByContributedCoverageSearcher statistics :> IForwardSearcher - | ExecutionTreeMode -> ExecutionTreeSearcher (getRandomSeedOption ()) + | ExecutionTreeMode -> ExecutionTreeSearcher(getRandomSeedOption ()) | FairMode baseMode -> - FairSearcher ((fun _ -> mkForwardSearcher baseMode), uint branchReleaseTimeout, statistics) + FairSearcher((fun _ -> mkForwardSearcher baseMode), uint branchReleaseTimeout, statistics) :> IForwardSearcher - | InterleavedMode (base1, stepCount1, base2, stepCount2) -> - InterleavedSearcher ( - [ - mkForwardSearcher base1, stepCount1 - mkForwardSearcher base2, stepCount2 - ] - ) + | InterleavedMode(base1, stepCount1, base2, stepCount2) -> + InterleavedSearcher([ mkForwardSearcher base1, stepCount1; mkForwardSearcher base2, stepCount2 ]) :> IForwardSearcher - let mutable searcher : IBidirectionalSearcher = + let mutable searcher: IBidirectionalSearcher = match options.explorationMode with - | TestCoverageMode (_, searchMode) -> + | TestCoverageMode(_, searchMode) -> let baseSearcher = if options.recThreshold > 0u then - GuidedSearcher ( + GuidedSearcher( mkForwardSearcher searchMode, - RecursionBasedTargetManager (statistics, options.recThreshold) + RecursionBasedTargetManager(statistics, options.recThreshold) ) :> IForwardSearcher else mkForwardSearcher searchMode - BidirectionalSearcher (baseSearcher, BackwardSearcher (), DummyTargetedSearcher.DummyTargetedSearcher ()) + + BidirectionalSearcher(baseSearcher, BackwardSearcher(), DummyTargetedSearcher.DummyTargetedSearcher()) :> IBidirectionalSearcher | StackTraceReproductionMode _ -> __notImplemented__ () let releaseBranches () = if not branchesReleased then branchesReleased <- true - statistics.OnBranchesReleased () - ReleaseBranches () + statistics.OnBranchesReleased() + ReleaseBranches() + let dfsSearcher = DFSSortedByContributedCoverageSearcher statistics :> IForwardSearcher - let bidirectionalSearcher = - OnlyForwardSearcher (dfsSearcher) - dfsSearcher.Init <| searcher.States () + + let bidirectionalSearcher = OnlyForwardSearcher(dfsSearcher) + dfsSearcher.Init <| searcher.States() searcher <- bidirectionalSearcher - let reportStateIncomplete (state : cilState) = + let reportStateIncomplete (state: cilState) = searcher.Remove state - statistics.IncompleteStates.Add (state) + statistics.IncompleteStates.Add(state) Application.terminateState state reporter.ReportIIE state.iie.Value let reportIncomplete = reporter.ReportIIE - let reportState (suite : testSuite) (cilState : cilState) = + let reportState (suite: testSuite) (cilState: cilState) = try let isNewHistory () = - let methodHistory = - Set.filter (fun h -> h.method.InCoverageZone) cilState.history + let methodHistory = Set.filter (fun h -> h.method.InCoverageZone) cilState.history + Set.isEmpty methodHistory || Set.exists (not << statistics.IsBasicBlockCoveredByTest) methodHistory + let isError = suite.IsErrorSuite + let isNewTest = match suite with | Test -> isNewHistory () - | Error (msg, isFatal) -> statistics.IsNewError cilState msg isFatal + | Error(msg, isFatal) -> statistics.IsNewError cilState msg isFatal + if isNewTest then let state = cilState.state - let callStackSize = - Memory.CallStackSize state + let callStackSize = Memory.CallStackSize state let entryMethod = cilState.EntryMethod - let hasException = - cilState.IsUnhandledException + let hasException = cilState.IsUnhandledException + if isError && not hasException then if entryMethod.HasParameterOnStack then Memory.ForcePopFrames (callStackSize - 2) state else Memory.ForcePopFrames (callStackSize - 1) state + match TestGenerator.state2test suite entryMethod state with | Some test -> - statistics.TrackFinished (cilState, isError) + statistics.TrackFinished(cilState, isError) + match suite with | Test -> reporter.ReportFinished test | Error _ -> reporter.ReportException test + if isCoverageAchieved () then isStopped <- true | None -> () @@ -232,37 +243,38 @@ type private SVMExplorer(explorationOptions : ExplorationOptions, statistics : S cilState.SetIIE e reportStateIncomplete cilState - let reportStateInternalFail (state : cilState) (e : Exception) = + let reportStateInternalFail (state: cilState) (e: Exception) = match e with | :? InsufficientInformationException as e -> if not state.IsIIEState then state.SetIIE e + reportStateIncomplete state | _ -> searcher.Remove state - statistics.InternalFails.Add (e) + statistics.InternalFails.Add(e) Application.terminateState state reporter.ReportInternalFail state.EntryMethod e - let reportInternalFail (method : Method) (e : Exception) = + let reportInternalFail (method: Method) (e: Exception) = match e with | :? InsufficientInformationException as e -> reportIncomplete e | _ -> - statistics.InternalFails.Add (e) + statistics.InternalFails.Add(e) reporter.ReportInternalFail method e - let reportFinished (state : cilState) = + let reportFinished (state: cilState) = let result = Memory.StateResult state.state Logger.info $"Result of method {state.EntryMethod.FullName} is {result}" Application.terminateState state reportState Test state - let wrapOnError isFatal (state : cilState) errorMessage = + let wrapOnError isFatal (state: cilState) errorMessage = if not <| String.IsNullOrWhiteSpace errorMessage then Logger.info $"Error in {state.EntryMethod.FullName}: {errorMessage}" + Application.terminateState state - let testSuite = - Error (errorMessage, isFatal) + let testSuite = Error(errorMessage, isFatal) reportState testSuite state let reportError = wrapOnError false @@ -273,55 +285,66 @@ type private SVMExplorer(explorationOptions : ExplorationOptions, statistics : S hasTimeout && statistics.CurrentExplorationTime.TotalMilliseconds >= explorationOptions.timeout.TotalMilliseconds + let shouldReleaseBranches () = options.releaseBranches && statistics.CurrentExplorationTime.TotalMilliseconds >= branchReleaseTimeout + let isStepsLimitReached () = hasStepsLimit && statistics.StepsCount >= options.stepsLimit - static member private AllocateByRefParameters initialState (method : Method) = - let allocateIfByRef (pi : ParameterInfo) = + static member private AllocateByRefParameters initialState (method: Method) = + let allocateIfByRef (pi: ParameterInfo) = let parameterType = pi.ParameterType + if parameterType.IsByRef then if Memory.CallStackSize initialState = 0 then Memory.NewStackFrame initialState None [] - let typ = parameterType.GetElementType () + + let typ = parameterType.GetElementType() let position = pi.Position + 1 + let stackRef = Memory.AllocateTemporaryLocalVariableOfType initialState pi.Name position typ + Some stackRef else None + method.Parameters |> Array.map allocateIfByRef |> Array.toList - member private x.FormIsolatedInitialStates (method : Method, initialState : state) = + member private x.FormIsolatedInitialStates(method: Method, initialState: state) = try initialState.model <- Memory.EmptyModel method let declaringType = method.DeclaringType - let cilState = - cilState.CreateInitial method initialState + let cilState = cilState.CreateInitial method initialState + let this = if method.HasThis then if Types.IsValueType declaringType then Memory.NewStackFrame initialState None [] + Memory.AllocateTemporaryLocalVariableOfType initialState "this" 0 declaringType |> Some else - let this = - Memory.MakeSymbolicThis initialState method + let this = Memory.MakeSymbolicThis initialState method !!(IsNullReference this) |> AddConstraint initialState Some this else None - let parameters = - SVMExplorer.AllocateByRefParameters initialState method + + let parameters = SVMExplorer.AllocateByRefParameters initialState method Memory.InitFunctionFrame initialState method this (Some parameters) + match this with | Some this -> SolveThisType initialState this | _ -> () + let cilStates = ILInterpreter.CheckDisallowNullAttribute method None cilState false id + assert (List.length cilStates = 1) + if not method.IsStaticConstructor then let cilState = List.head cilStates interpreter.InitializeStatics cilState declaringType List.singleton @@ -333,84 +356,92 @@ type private SVMExplorer(explorationOptions : ExplorationOptions, statistics : S [] member private x.FormEntryPointInitialStates - (method : Method, config : EntryPointConfiguration, initialState : state) + (method: Method, config: EntryPointConfiguration, initialState: state) : cilState list = try assert method.IsStatic let optionArgs = config.Args let parameters = method.Parameters - let hasParameters = - Array.length parameters > 0 + let hasParameters = Array.length parameters > 0 + let state = { initialState with complete = not hasParameters || Option.isSome optionArgs } + state.model <- Memory.EmptyModel method + match optionArgs with | Some args -> let stringType = typeof let argsNumber = MakeNumber args.Length - let argsRef = - Memory.AllocateConcreteVectorArray state argsNumber stringType args - let args = - Some (List.singleton (Some argsRef)) + let argsRef = Memory.AllocateConcreteVectorArray state argsNumber stringType args + let args = Some(List.singleton (Some argsRef)) Memory.InitFunctionFrame state method None args | None when hasParameters -> Memory.InitFunctionFrame state method None None // NOTE: if args are symbolic, constraint 'args != null' is added assert (Array.length parameters = 1) let argsParameter = Array.head parameters - let argsParameterTerm = - Memory.ReadArgument state argsParameter + let argsParameterTerm = Memory.ReadArgument state argsParameter AddConstraint state (!!(IsNullReference argsParameterTerm)) // Filling model with default args to match PC let modelState = match state.model with | StateModel modelState -> modelState | _ -> __unreachable__ () + let argsForModel = Memory.AllocateVectorArray modelState (MakeNumber 0) typeof + Memory.WriteStackLocation modelState (ParameterKey argsParameter) argsForModel | None -> let args = Some List.empty Memory.InitFunctionFrame state method None args + Memory.InitializeStaticMembers state method.DeclaringType + let initialState = match config with | :? WebConfiguration as config -> - let webConfig = config.ToWebConfig () + let webConfig = config.ToWebConfig() cilState.CreateWebInitial method state webConfig | _ -> cilState.CreateInitial method state + [ initialState ] with e -> reportInternalFail method e [] - member private x.Forward (s : cilState) = + member private x.Forward(s: cilState) = let loc = s.approximateLoc let ip = s.CurrentIp let stackSize = s.StackSize // TODO: update pobs when visiting new methods; use coverageZone - let goodStates, iieStates, errors = - interpreter.ExecuteOneInstruction s + let goodStates, iieStates, errors = interpreter.ExecuteOneInstruction s + for s in goodStates @ iieStates @ errors do if not s.HasRuntimeExceptionOrError then statistics.TrackStepForward s ip stackSize + let goodStates, toReportFinished = goodStates |> List.partition (fun s -> s.IsExecutable || s.IsIsolated) + toReportFinished |> List.iter reportFinished - let errors, _ = - errors |> List.partition (fun s -> not s.HasReportedError) + let errors, _ = errors |> List.partition (fun s -> not s.HasReportedError) + let errors, toReportExceptions = errors |> List.partition (fun s -> s.IsIsolated || not s.IsStoppedByException) + let runtimeExceptions, userExceptions = toReportExceptions |> List.partition (fun s -> s.HasRuntimeExceptionOrError) + runtimeExceptions |> List.iter (fun state -> reportError state null) userExceptions |> List.iter reportFinished - let iieStates, toReportIIE = - iieStates |> List.partition (fun s -> s.IsIsolated) + let iieStates, toReportIIE = iieStates |> List.partition (fun s -> s.IsIsolated) toReportIIE |> List.iter reportStateIncomplete let mutable sIsStopped = false + let newStates = match goodStates, iieStates, errors with | s' :: goodStates, _, _ when LanguagePrimitives.PhysicalEquality s s' -> goodStates @ iieStates @ errors @@ -424,36 +455,41 @@ type private SVMExplorer(explorationOptions : ExplorationOptions, statistics : S Application.moveState loc s (Seq.cast<_> newStates) statistics.TrackFork s newStates searcher.UpdateStates s newStates + if sIsStopped then searcher.Remove s - member private x.Backward p' (s' : cilState) = + member private x.Backward p' (s': cilState) = assert (s'.CurrentLoc = p'.loc) let sLvl = s'.Level + if p'.lvl >= sLvl then let lvl = p'.lvl - sLvl let pc = Memory.WLP s'.state p'.pc + match isSat pc with | true when not s'.IsIsolated -> searcher.Answer p' (Witnessed s') | true -> statistics.TrackStepBackward p' s' + let p = { loc = s'.StartingLoc lvl = lvl pc = pc } + Logger.trace $"Backward:\nWas: {p'}\nNow: {p}\n\n" Application.addGoal p.loc searcher.UpdatePobs p' p | false -> Logger.trace "UNSAT for pob = %O and s'.PC = %s" p' (API.Print.PrintPC s'.state.pc) - member private x.BidirectionalSymbolicExecution () = + member private x.BidirectionalSymbolicExecution() = let mutable action = Stop let pick () = - match searcher.Pick () with + match searcher.Pick() with | Stop -> false | a -> action <- a @@ -466,21 +502,26 @@ type private SVMExplorer(explorationOptions : ExplorationOptions, statistics : S && pick () do if shouldReleaseBranches () then releaseBranches () + match action with | GoFront s -> try - if - options.aiAgentTrainingOptions.IsSome - && options.aiAgentTrainingOptions.Value.serializeSteps - then + let needToSerialize = + match options.aiOptions with + | Some(DatasetGenerator _) -> true + | _ -> false + + if needToSerialize then dumpGameState - (Path.Combine (folderToStoreSerializationResult, string firstFreeEpisodeNumber)) + (Path.Combine(folderToStoreSerializationResult, string firstFreeEpisodeNumber)) s.internalId + firstFreeEpisodeNumber <- firstFreeEpisodeNumber + 1 - x.Forward (s) + + x.Forward(s) with e -> reportStateInternalFail s e - | GoBack (s, p) -> + | GoBack(s, p) -> try x.Backward p s with e -> @@ -488,43 +529,46 @@ type private SVMExplorer(explorationOptions : ExplorationOptions, statistics : S | Stop -> __unreachable__ () member private x.AnswerPobs initialStates = - statistics.ExplorationStarted () + statistics.ExplorationStarted() // For backward compatibility. TODO: remove main pobs at all let mainPobs = [] Application.spawnStates (Seq.cast<_> initialStates) mainPobs |> Seq.map (fun pob -> pob.loc) |> Seq.toArray |> Application.addGoals searcher.Init initialStates mainPobs + initialStates |> Seq.filter (fun s -> s.IsIIEState) |> Seq.iter reportStateIncomplete - x.BidirectionalSymbolicExecution () - searcher.Statuses () + + x.BidirectionalSymbolicExecution() + + searcher.Statuses() |> Seq.iter (fun (pob, status) -> match status with | pobStatus.Unknown -> Logger.warning $"Unknown status for pob at {pob.loc}" - | _ -> () - ) + | _ -> ()) interface IExplorer with member x.Reset entryMethods = HashMap.clear () - API.Reset () + API.Reset() SolverPool.reset () - searcher.Reset () + searcher.Reset() isStopped <- false branchesReleased <- false SolverInteraction.setOnSolverStarted statistics.SolverStarted SolverInteraction.setOnSolverStopped statistics.SolverStopped - AcquireBranches () + AcquireBranches() isCoverageAchieved <- always false + match options.explorationMode with | TestCoverageMode _ -> if options.stopOnCoverageAchieved > 0 then let checkCoverage () = - let cov = - statistics.GetCurrentCoverage entryMethods + let cov = statistics.GetCurrentCoverage entryMethods cov >= options.stopOnCoverageAchieved + isCoverageAchieved <- checkCoverage | StackTraceReproductionMode _ -> __notImplemented__ () @@ -533,54 +577,54 @@ type private SVMExplorer(explorationOptions : ExplorationOptions, statistics : S try try interpreter.ConfigureErrorReporter reportError reportFatalError - let isolatedInitialStates = - isolated |> List.collect x.FormIsolatedInitialStates + let isolatedInitialStates = isolated |> List.collect x.FormIsolatedInitialStates + let entryPointsInitialStates = entryPoints |> List.collect x.FormEntryPointInitialStates + let iieStates, initialStates = isolatedInitialStates @ entryPointsInitialStates |> List.partition (fun state -> state.IsIIEState) + iieStates |> List.iter reportStateIncomplete - statistics.SetStatesGetter (fun () -> searcher.States ()) - statistics.SetStatesCountGetter (fun () -> searcher.StatesCount) + statistics.SetStatesGetter(fun () -> searcher.States()) + statistics.SetStatesCountGetter(fun () -> searcher.StatesCount) + if not initialStates.IsEmpty then x.AnswerPobs initialStates with e -> reportCrash e finally try - statistics.ExplorationFinished () - API.Restore () - searcher.Reset () + statistics.ExplorationFinished() + API.Restore() + searcher.Reset() with e -> reportCrash e } - member private x.Stop () = isStopped <- true + member private x.Stop() = isStopped <- true -type private FuzzerExplorer(explorationOptions : ExplorationOptions, statistics : SVMStatistics) = +type private FuzzerExplorer(explorationOptions: ExplorationOptions, statistics: SVMStatistics) = interface IExplorer with member x.Reset _ = () member x.StartExploration isolated _ = - let saveStatistic = - statistics.SetBasicBlocksAsCoveredByTest - let outputDir = - explorationOptions.outputDirectory.FullName - let cancellationTokenSource = - new CancellationTokenSource () - cancellationTokenSource.CancelAfter (explorationOptions.timeout) - let methodsBase = - isolated |> List.map (fun (m, _) -> (m :> IMethod).MethodBase) + let saveStatistic = statistics.SetBasicBlocksAsCoveredByTest + let outputDir = explorationOptions.outputDirectory.FullName + let cancellationTokenSource = new CancellationTokenSource() + cancellationTokenSource.CancelAfter(explorationOptions.timeout) + let methodsBase = isolated |> List.map (fun (m, _) -> (m :> IMethod).MethodBase) + task { try - let targetAssemblyPath = - (Seq.head methodsBase).Module.Assembly.Location + let targetAssemblyPath = (Seq.head methodsBase).Module.Assembly.Location let onCancelled () = Logger.warning "Fuzzer canceled" + let interactor = - Fuzzer.Interactor ( + Fuzzer.Interactor( targetAssemblyPath, methodsBase, cancellationTokenSource.Token, @@ -588,30 +632,30 @@ type private FuzzerExplorer(explorationOptions : ExplorationOptions, statistics saveStatistic, onCancelled ) - do! interactor.StartFuzzing () + + do! interactor.StartFuzzing() with e -> Logger.error $"Fuzzer unhandled exception: {e}" raise e } -type public Explorer(options : ExplorationOptions, reporter : IReporter) = +type public Explorer(options: ExplorationOptions, reporter: IReporter) = - let statistics = - new SVMStatistics (Seq.empty, true) + let statistics = new SVMStatistics(Seq.empty, true) let explorers = let createFuzzer () = - FuzzerExplorer (options, statistics) :> IExplorer + FuzzerExplorer(options, statistics) :> IExplorer let createSVM () = - SVMExplorer (options, statistics, reporter) :> IExplorer + SVMExplorer(options, statistics, reporter) :> IExplorer match options.explorationModeOptions with | Fuzzing _ -> createFuzzer () |> Array.singleton | SVM _ -> createSVM () |> Array.singleton - | Combined _ -> [| createFuzzer () ; createSVM () |] + | Combined _ -> [| createFuzzer (); createSVM () |] - let inCoverageZone coverageZone (entryMethods : Method list) = + let inCoverageZone coverageZone (entryMethods: Method list) = match coverageZone with | MethodZone -> fun method -> entryMethods |> List.contains method | ClassZone -> @@ -623,34 +667,38 @@ type public Explorer(options : ExplorationOptions, reporter : IReporter) = entryMethods |> List.exists (fun m -> method.Module.ModuleHandle = m.Module.ModuleHandle) - member private x.TrySubstituteTypeParameters (state : state) (methodBase : MethodBase) = - let method = - Application.getMethod methodBase + member private x.TrySubstituteTypeParameters (state: state) (methodBase: MethodBase) = + let method = Application.getMethod methodBase + let getConcreteType = function | ConcreteType t -> Some t | _ -> None + try if method.ContainsGenericParameters then match SolveGenericMethodParameters state.typeStorage method with - | Some (classParams, methodParams) -> - let classParams = - classParams |> Array.choose getConcreteType - let methodParams = - methodParams |> Array.choose getConcreteType + | Some(classParams, methodParams) -> + let classParams = classParams |> Array.choose getConcreteType + let methodParams = methodParams |> Array.choose getConcreteType let declaringType = methodBase.DeclaringType + let isSuitableType () = not declaringType.IsGenericType || classParams.Length = declaringType.GetGenericArguments().Length + let isSuitableMethod () = methodBase.IsConstructor || not methodBase.IsGenericMethod || methodParams.Length = methodBase.GetGenericArguments().Length + if isSuitableType () && isSuitableMethod () then let reflectedType = Reflection.concretizeTypeParameters methodBase.ReflectedType classParams + let method = Reflection.concretizeMethodParameters reflectedType methodBase methodParams + Some method else None @@ -664,30 +712,31 @@ type public Explorer(options : ExplorationOptions, reporter : IReporter) = member x.Reset entryMethods = statistics.Reset entryMethods Application.setCoverageZone (inCoverageZone options.coverageZone entryMethods) + for explorer in explorers do explorer.Reset entryMethods member x.StartExploration - (isolated : MethodBase seq) - (entryPoints : (MethodBase * EntryPointConfiguration) seq) + (isolated: MethodBase seq) + (entryPoints: (MethodBase * EntryPointConfiguration) seq) : unit = try let trySubstituteTypeParameters method = - let emptyState = - Memory.EmptyIsolatedState () + let emptyState = Memory.EmptyIsolatedState() (Option.defaultValue method (x.TrySubstituteTypeParameters emptyState method), emptyState) + let isolated = isolated |> Seq.map trySubstituteTypeParameters |> Seq.map (fun (m, s) -> Application.getMethod m, s) |> Seq.toList + let entryPoints = entryPoints |> Seq.map (fun (m, a) -> let m, s = trySubstituteTypeParameters m - (Application.getMethod m, a, s) - ) + (Application.getMethod m, a, s)) |> Seq.toList (List.map fst isolated) @ (List.map (fun (x, _, _) -> x) entryPoints) |> x.Reset @@ -695,8 +744,7 @@ type public Explorer(options : ExplorationOptions, reporter : IReporter) = let explorationTasks = explorers |> Array.map (fun e -> e.StartExploration isolated entryPoints) - let finished = - Task.WaitAll (explorationTasks, options.timeout) + let finished = Task.WaitAll(explorationTasks, options.timeout) if not finished then Logger.warning "Exploration cancelled" @@ -713,4 +761,4 @@ type public Explorer(options : ExplorationOptions, reporter : IReporter) = member x.Statistics = statistics interface IDisposable with - member x.Dispose () = (statistics :> IDisposable).Dispose () + member x.Dispose() = (statistics :> IDisposable).Dispose() diff --git a/VSharp.Explorer/Options.fs b/VSharp.Explorer/Options.fs index a5ddca2e5..5aed4a4d3 100644 --- a/VSharp.Explorer/Options.fs +++ b/VSharp.Explorer/Options.fs @@ -28,14 +28,15 @@ type fuzzerIsolation = | Process type FuzzerOptions = { - isolation : fuzzerIsolation - coverageZone : coverageZone + isolation: fuzzerIsolation + coverageZone: coverageZone } [] type Oracle = - val Predict : GameState -> uint - val Feedback : Feedback -> unit + val Predict: GameState -> uint + val Feedback: Feedback -> unit + new(predict, feedback) = { Predict = predict @@ -51,33 +52,60 @@ type Oracle = /// Determine whether steps should be serialized. /// Name of map to play. /// Name of map to play. + + +type AIBaseOptions = + { + defaultSearchStrategy: searchMode + mapName: string + } + type AIAgentTrainingOptions = { - stepsToSwitchToAI : uint - stepsToPlay : uint - defaultSearchStrategy : searchMode - serializeSteps : bool - mapName : string - oracle : Option + aiBaseOptions: AIBaseOptions + stepsToSwitchToAI: uint + stepsToPlay: uint + oracle: option + } + +type AIAgentTrainingEachStepOptions = + { + aiAgentTrainingOptions: AIAgentTrainingOptions + } + + +type AIAgentTrainingModelOptions = + { + aiAgentTrainingOptions: AIAgentTrainingOptions + outputDirectory: string } + +type AIAgentTrainingMode = + | SendEachStep of AIAgentTrainingEachStepOptions + | SendModel of AIAgentTrainingModelOptions + +type AIOptions = + | Training of AIAgentTrainingMode + | DatasetGenerator of AIBaseOptions + type SVMOptions = { - explorationMode : explorationMode - recThreshold : uint - solverTimeout : int - visualize : bool - releaseBranches : bool - maxBufferSize : int - prettyChars : bool // If true, 33 <= char <= 126, otherwise any char - checkAttributes : bool - stopOnCoverageAchieved : int - randomSeed : int - stepsLimit : uint - aiAgentTrainingOptions : Option - pathToModel : Option - useGPU : Option - optimize : Option + explorationMode: explorationMode + recThreshold: uint + solverTimeout: int + visualize: bool + releaseBranches: bool + maxBufferSize: int + prettyChars: bool // If true, 33 <= char <= 126, otherwise any char + checkAttributes: bool + stopOnCoverageAchieved: int + randomSeed: int + stepsLimit: uint + aiOptions: Option + pathToModel: Option + useGPU: Option + optimize: Option } type explorationModeOptions = @@ -87,28 +115,28 @@ type explorationModeOptions = type ExplorationOptions = { - timeout : System.TimeSpan - outputDirectory : DirectoryInfo - explorationModeOptions : explorationModeOptions + timeout: System.TimeSpan + outputDirectory: DirectoryInfo + explorationModeOptions: explorationModeOptions } member this.fuzzerOptions = match this.explorationModeOptions with | Fuzzing x -> x - | Combined (_, x) -> x + | Combined(_, x) -> x | _ -> failwith "" member this.svmOptions = match this.explorationModeOptions with | SVM x -> x - | Combined (x, _) -> x + | Combined(x, _) -> x | _ -> failwith "" member this.coverageZone = match this.explorationModeOptions with | SVM x -> match x.explorationMode with - | TestCoverageMode (coverageZone, _) -> coverageZone + | TestCoverageMode(coverageZone, _) -> coverageZone | StackTraceReproductionMode _ -> failwith "" - | Combined (_, x) -> x.coverageZone + | Combined(_, x) -> x.coverageZone | Fuzzing x -> x.coverageZone diff --git a/VSharp.ML.GameServer.Runner/Main.fs b/VSharp.ML.GameServer.Runner/Main.fs index b8ffdfed6..9daaee2fd 100644 --- a/VSharp.ML.GameServer.Runner/Main.fs +++ b/VSharp.ML.GameServer.Runner/Main.fs @@ -16,13 +16,13 @@ open VSharp.IL open VSharp.ML.GameServer.Messages open VSharp.Runner - [] type ExplorationResult = val ActualCoverage : uint val TestsCount : uint val ErrorsCount : uint val StepsCount : uint + new(actualCoverage, testsCount, errorsCount, stepsCount) = { ActualCoverage = actualCoverage @@ -34,6 +34,8 @@ type ExplorationResult = type Mode = | Server = 0 | Generator = 1 + | SendModel = 2 + type CliArguments = | [] Port of int | [] DatasetBasePath of string @@ -41,6 +43,13 @@ type CliArguments = | [] Mode of Mode | [] OutFolder of string | [] StepsToSerialize of uint + | [] Model of string + | [] StepsToPlay of uint + | [] DefaultSearcher of string + | [] StepsToStart of uint + | [] AssemblyFullName of string + | [] NameOfObjectToCover of string + | [] MapName of string | [] UseGPU | [] Optimize @@ -55,6 +64,13 @@ type CliArguments = "Mode to run application. Server --- to train network, Generator --- to generate data for training." | OutFolder _ -> "Folder to store generated data." | StepsToSerialize _ -> "Maximal number of steps for each method to serialize." + | Model _ -> """Path to ONNX model (use it for training in mode "SendModel")""" + | StepsToPlay _ -> """Steps to start""" + | DefaultSearcher _ -> """Default searcher""" + | StepsToStart _ -> """Steps to start""" + | AssemblyFullName _ -> """Path to dll that contains game map""" + | NameOfObjectToCover _ -> """Name of object to cover""" + | MapName _ -> """Name of map""" | UseGPU -> "Specifies whether the ONNX execution session should use a CUDA-enabled GPU." | Optimize -> "Enabling options like parallel execution and various graph transformations to enhance performance of ONNX." @@ -64,19 +80,24 @@ let mutable inTrainMode = true let explore (gameMap : GameMap) options = let assembly = RunnerProgram.TryLoadAssembly <| FileInfo gameMap.AssemblyFullName + let method = RunnerProgram.ResolveMethod (assembly, gameMap.NameOfObjectToCover) let statistics = TestGenerator.Cover (method, options) + let actualCoverage = try let testsDir = statistics.OutputDir let _expectedCoverage = 100 let exploredMethodInfo = AssemblyManager.NormalizeMethod method + let status, actualCoverage, message = VSharp.Test.TestResultChecker.Check (testsDir, exploredMethodInfo :?> MethodInfo, _expectedCoverage) + printfn $"Actual coverage for {gameMap.MapName}: {actualCoverage}" + if actualCoverage < 0 then 0u else @@ -92,13 +113,28 @@ let explore (gameMap : GameMap) options = statistics.StepsCount * 1u ) +let getGameMap (gameMaps : ResizeArray) (mapName : string) = + let mutable gameMapRes : Option = + None + + for gameMap in gameMaps do + if gameMap.MapName = mapName then + gameMapRes <- Some gameMap + + match gameMapRes with + | Some gameMap -> printfn ($"{gameMap.ToString}") + | None -> printfn "map is not selected" + + gameMapRes let loadGameMaps (datasetDescriptionFilePath : string) = let jsonString = File.ReadAllText datasetDescriptionFilePath let maps = ResizeArray () + for map in System.Text.Json.JsonSerializer.Deserialize jsonString do maps.Add map + maps let ws port outputDirectory (webSocket : WebSocket) (context : HttpContext) = @@ -111,6 +147,7 @@ let ws port outputDirectory (webSocket : WebSocket) (context : HttpContext) = serializeOutgoingMessage message |> System.Text.Encoding.UTF8.GetBytes |> ByteSegment + webSocket.send Text byteResponse true let oracle = @@ -123,14 +160,17 @@ let ws port outputDirectory (webSocket : WebSocket) (context : HttpContext) = | Feedback.ServerError s -> OutgoingMessage.ServerError s | Feedback.MoveReward reward -> OutgoingMessage.MoveReward reward | Feedback.IncorrectPredictedStateId i -> OutgoingMessage.IncorrectPredictedStateId i + do! sendResponse message } + match Async.RunSynchronously res with | Choice1Of2 () -> () | Choice2Of2 error -> failwithf $"Error: %A{error}" let predict = let mutable cnt = 0u + fun (gameState : GameState) -> let toDot drawHistory = let file = Path.Join ("dot", $"{cnt}.dot") @@ -141,16 +181,20 @@ let ws port outputDirectory (webSocket : WebSocket) (context : HttpContext) = socket { do! sendResponse (ReadyForNextStep gameState) let! msg = webSocket.read () + let res = match msg with | (Text, data, true) -> let msg = deserializeInputMessage data + match msg with | Step stepParams -> (stepParams.StateId) | _ -> failwithf $"Unexpected message: %A{msg}" | _ -> failwithf $"Unexpected message: %A{msg}" + return res } + match Async.RunSynchronously res with | Choice1Of2 i -> i | Choice2Of2 error -> failwithf $"Error: %A{error}" @@ -159,40 +203,56 @@ let ws port outputDirectory (webSocket : WebSocket) (context : HttpContext) = while loop do let! msg = webSocket.read () + match msg with | (Text, data, true) -> let message = deserializeInputMessage data + match message with | ServerStop -> loop <- false | Start gameMap -> printfn $"Start map {gameMap.MapName}, port {port}" + let aiTrainingOptions = { + aiBaseOptions = + { + defaultSearchStrategy = + match gameMap.DefaultSearcher with + | searcher.BFS -> BFSMode + | searcher.DFS -> DFSMode + | x -> failwithf $"Unexpected searcher {x}. Use DFS or BFS for now." + mapName = gameMap.MapName + } stepsToSwitchToAI = gameMap.StepsToStart stepsToPlay = gameMap.StepsToPlay - defaultSearchStrategy = - match gameMap.DefaultSearcher with - | searcher.BFS -> BFSMode - | searcher.DFS -> DFSMode - | x -> failwithf $"Unexpected searcher {x}. Use DFS or BFS for now." - serializeSteps = false - mapName = gameMap.MapName oracle = Some oracle } + + let aiOptions : AIOptions = + (Training ( + SendEachStep + { + aiAgentTrainingOptions = aiTrainingOptions + } + )) + let options = VSharpOptions ( timeout = 15 * 60, outputDirectory = outputDirectory, searchStrategy = SearchStrategy.AI, - aiAgentTrainingOptions = aiTrainingOptions, + aiOptions = (Some aiOptions |> Option.defaultValue Unchecked.defaultof<_>), solverTimeout = 2 ) + let explorationResult = explore gameMap options Application.reset () API.Reset () HashMap.hashMap.Clear () + do! sendResponse ( GameOver ( @@ -201,6 +261,7 @@ let ws port outputDirectory (webSocket : WebSocket) (context : HttpContext) = explorationResult.ErrorsCount ) ) + printfn $"Finish map {gameMap.MapName}, port {port}" | x -> failwithf $"Unexpected message: %A{x}" @@ -221,6 +282,7 @@ let generateDataForPretraining outputDirectory datasetBasePath (maps : ResizeArr for map in maps do if map.StepsToStart = 0u then printfn $"Generation for {map.MapName} started." + let map = GameMap ( map.StepsToPlay, @@ -230,14 +292,11 @@ let generateDataForPretraining outputDirectory datasetBasePath (maps : ResizeArr map.NameOfObjectToCover, map.MapName ) - let aiTrainingOptions = + + let aiBaseOptions = { - stepsToSwitchToAI = 0u - stepsToPlay = 0u - defaultSearchStrategy = searchMode.BFSMode - serializeSteps = true + defaultSearchStrategy = BFSMode mapName = map.MapName - oracle = None } let options = @@ -247,32 +306,100 @@ let generateDataForPretraining outputDirectory datasetBasePath (maps : ResizeArr searchStrategy = SearchStrategy.ExecutionTreeContributedCoverage, stepsLimit = stepsToSerialize, solverTimeout = 2, - aiAgentTrainingOptions = aiTrainingOptions + aiOptions = + (Some (DatasetGenerator aiBaseOptions) + |> Option.defaultValue Unchecked.defaultof<_>) ) + let folderForResults = Serializer.getFolderToStoreSerializationResult outputDirectory map.MapName + if Directory.Exists folderForResults then Directory.Delete (folderForResults, true) + let _ = Directory.CreateDirectory folderForResults let explorationResult = explore map options + File.WriteAllText ( Path.Join (folderForResults, "result"), $"{explorationResult.ActualCoverage} {explorationResult.TestsCount} {explorationResult.StepsCount} {explorationResult.ErrorsCount}" ) + printfn $"Generation for {map.MapName} finished with coverage {explorationResult.ActualCoverage}, tests {explorationResult.TestsCount}, steps {explorationResult.StepsCount},errors {explorationResult.ErrorsCount}." + Application.reset () API.Reset () HashMap.hashMap.Clear () +let runTrainingSendModelMode + outputDirectory + (gameMap : GameMap) + (pathToModel : string) + (useGPU : bool) + (optimize : bool) + = + printfn $"Run infer on {gameMap.MapName} have started." + + let aiTrainingOptions = + { + aiBaseOptions = + { + defaultSearchStrategy = + match gameMap.DefaultSearcher with + | searcher.BFS -> BFSMode + | searcher.DFS -> DFSMode + | x -> failwithf $"Unexpected searcher {x}. Use DFS or BFS for now." + + mapName = gameMap.MapName + } + stepsToSwitchToAI = gameMap.StepsToStart + stepsToPlay = gameMap.StepsToPlay + oracle = None + } + + let aiOptions : AIOptions = + Training ( + SendModel + { + aiAgentTrainingOptions = aiTrainingOptions + outputDirectory = outputDirectory + } + ) + + let options = + VSharpOptions ( + timeout = 15 * 60, + outputDirectory = outputDirectory, + searchStrategy = SearchStrategy.AI, + solverTimeout = 2, + aiOptions = (Some aiOptions |> Option.defaultValue Unchecked.defaultof<_>), + pathToModel = pathToModel, + useGPU = useGPU, + optimize = optimize + ) + + let explorationResult = + explore gameMap options + + File.WriteAllText ( + Path.Join (outputDirectory, gameMap.MapName + "result"), + $"{explorationResult.ActualCoverage} {explorationResult.TestsCount} {explorationResult.StepsCount} {explorationResult.ErrorsCount}" + ) + + printfn + $"Running for {gameMap.MapName} finished with coverage {explorationResult.ActualCoverage}, tests {explorationResult.TestsCount}, steps {explorationResult.StepsCount},errors {explorationResult.ErrorsCount}." + + + [] let main args = let parser = ArgumentParser.Create (programName = "VSharp.ML.GameServer.Runner.exe") - let args = parser.Parse args + let args = parser.Parse args let mode = args.GetResult <@ Mode @> let port = @@ -280,38 +407,23 @@ let main args = | Some port -> port | None -> 8100 - let datasetBasePath = - match args.TryGetResult <@ DatasetBasePath @> with - | Some path -> path - | None -> "" - - let datasetDescription = - match args.TryGetResult <@ DatasetDescription @> with + let outputDirectory = + match args.TryGetResult <@ OutFolder @> with | Some path -> path - | None -> "" - - let stepsToSerialize = - match args.TryGetResult <@ StepsToSerialize @> with - | Some steps -> steps - | None -> 500u + | None -> Path.Combine (Directory.GetCurrentDirectory (), string port) - let useGPU = - (args.TryGetResult <@ UseGPU @>).IsSome + let cleanOutputDirectory () = + if Directory.Exists outputDirectory then + Directory.Delete (outputDirectory, true) - let optimize = - (args.TryGetResult <@ Optimize @>).IsSome - - let outputDirectory = - Path.Combine (Directory.GetCurrentDirectory (), string port) - - if Directory.Exists outputDirectory then - Directory.Delete (outputDirectory, true) - let testsDirInfo = Directory.CreateDirectory outputDirectory + printfn $"outputDir: {outputDirectory}" match mode with | Mode.Server -> + let _ = cleanOutputDirectory () + try startWebServer { defaultConfig with @@ -325,7 +437,61 @@ let main args = with e -> printfn $"Failed on port {port}" printfn $"{e.Message}" + | Mode.SendModel -> + let model = + match args.TryGetResult <@ Model @> with + | Some path -> path + | None -> "models/model.onnx" + + let stepsToPlay = + args.GetResult <@ StepsToPlay @> + + let defaultSearcher = + let s = args.GetResult <@ DefaultSearcher @> + let upperedS = + String.map System.Char.ToUpper s + + match upperedS with + | "BFS" -> searcher.BFS + | "DFS" -> searcher.DFS + | _ -> failwith "Use BFS or DFS as a default searcher" + + let stepsToStart = + args.GetResult <@ StepsToStart @> + let assemblyFullName = + args.GetResult <@ AssemblyFullName @> + let nameOfObjectToCover = + args.GetResult <@ NameOfObjectToCover @> + let mapName = args.GetResult <@ MapName @> + + let gameMap = + GameMap ( + stepsToPlay = stepsToPlay, + stepsToStart = stepsToStart, + assemblyFullName = assemblyFullName, + defaultSearcher = defaultSearcher, + nameOfObjectToCover = nameOfObjectToCover, + mapName = mapName + ) + + let useGPU = + (args.TryGetResult <@ UseGPU @>).IsSome + let optimize = + (args.TryGetResult <@ Optimize @>).IsSome + + runTrainingSendModelMode outputDirectory gameMap model useGPU optimize | Mode.Generator -> + let datasetDescription = + args.GetResult <@ DatasetDescription @> + let datasetBasePath = + args.GetResult <@ DatasetBasePath @> + + let stepsToSerialize = + match args.TryGetResult <@ StepsToSerialize @> with + | Some steps -> steps + | None -> 500u + + let _ = cleanOutputDirectory () let maps = loadGameMaps datasetDescription generateDataForPretraining outputDirectory datasetBasePath maps stepsToSerialize | x -> failwithf $"Unexpected mode {x}." diff --git a/VSharp.Test/Benchmarks/Benchmarks.cs b/VSharp.Test/Benchmarks/Benchmarks.cs index 12e022ffd..b00901ad5 100644 --- a/VSharp.Test/Benchmarks/Benchmarks.cs +++ b/VSharp.Test/Benchmarks/Benchmarks.cs @@ -93,7 +93,7 @@ public static BenchmarkResult Run( stopOnCoverageAchieved: -1, randomSeed: randomSeed, stepsLimit: stepsLimit, - aiAgentTrainingOptions: null, + aiOptions: null, pathToModel: null, useGPU: null, optimize: null diff --git a/VSharp.Test/IntegrationTests.cs b/VSharp.Test/IntegrationTests.cs index 00ed34653..c8bbced2d 100644 --- a/VSharp.Test/IntegrationTests.cs +++ b/VSharp.Test/IntegrationTests.cs @@ -132,6 +132,7 @@ static TestSvmAttribute() private readonly ExplorationMode _explorationMode; private readonly int _randomSeed; private readonly uint _stepsLimit; + public readonly AIOptions? _aiOptions; private readonly string _pathToModel; private readonly bool _useGPU; private readonly bool _optimize; @@ -200,6 +201,7 @@ public TestCommand Wrap(TestCommand command) _explorationMode, _randomSeed, _stepsLimit, + _aiOptions, _pathToModel, _useGPU, _optimize, @@ -227,6 +229,7 @@ private class TestSvmCommand : DelegatingTestCommand private readonly ExplorationMode _explorationMode; private readonly int _randomSeed; private readonly uint _stepsLimit; + public readonly AIOptions? _aiOptions; private readonly string _pathToModel; private readonly bool _useGPU; private readonly bool _optimize; @@ -263,6 +266,7 @@ public TestSvmCommand( ExplorationMode explorationMode, int randomSeed, uint stepsLimit, + AIOptions? aiOptions, string pathToModel, bool useGPU, bool optimize, @@ -319,6 +323,7 @@ public TestSvmCommand( _explorationMode = explorationMode; _randomSeed = randomSeed; _stepsLimit = stepsLimit; + _aiOptions = aiOptions; _pathToModel = pathToModel; _useGPU = useGPU; _optimize = optimize; @@ -478,7 +483,7 @@ private TestResult Explore(TestExecutionContext context) stopOnCoverageAchieved: _expectedCoverage ?? -1, randomSeed: _randomSeed, stepsLimit: _stepsLimit, - aiAgentTrainingOptions: null, + aiOptions: _aiOptions, pathToModel: _pathToModel, useGPU: _useGPU, optimize: _optimize