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 e1a31ab0e..15962de84 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -2,61 +2,43 @@ namespace VSharp.Explorer open System.Collections.Generic open Microsoft.ML.OnnxRuntime +open System.IO +open System +open System.Net +open System.Net.Sockets +open System.Text +open System.Text.Json open VSharp open VSharp.IL.Serializer open VSharp.ML.GameServer.Messages -type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option) = - let stepsToSwitchToAI = - match aiAgentTrainingOptions with - | None -> 0u - | Some options -> options.stepsToSwitchToAI +type AIMode = + | Runner + | TrainingSendModel + | TrainingSendEachStep - let stepsToPlay = - match aiAgentTrainingOptions with - | None -> 0u - | Some options -> options.stepsToPlay - - let mutable lastCollectedStatistics = - Statistics () - let mutable defaultSearcherSteps = 0u - let mutable (gameState: Option) = - None - let mutable useDefaultSearcher = - stepsToSwitchToAI > 0u - let mutable afterFirstAIPeek = 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 - | x -> failwithf $"Unexpected default searcher {x}. DFS and BFS supported for now." - let mutable stepsPlayed = 0u - let isInAIMode () = - (not useDefaultSearcher) && afterFirstAIPeek - let q = ResizeArray<_> () - let availableStates = HashSet<_> () - let updateGameState (delta: GameState) = +module GameUtils = + let updateGameState (delta: GameState) (gameState: Option) = match gameState with - | None -> gameState <- Some delta + | None -> 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 @@ -85,13 +67,58 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option) = + let stepsToSwitchToAI = + match aiAgentTrainingMode with + | None -> 0u + | Some (SendModel options) -> options.aiAgentTrainingOptions.stepsToSwitchToAI + | Some (SendEachStep options) -> options.aiAgentTrainingOptions.stepsToSwitchToAI + + let stepsToPlay = + match aiAgentTrainingMode with + | None -> 0u + | Some (SendModel options) -> options.aiAgentTrainingOptions.stepsToPlay + | Some (SendEachStep options) -> options.aiAgentTrainingOptions.stepsToPlay + + let mutable lastCollectedStatistics = + Statistics () + let mutable defaultSearcherSteps = 0u + let mutable (gameState: Option) = + None + let mutable useDefaultSearcher = + stepsToSwitchToAI > 0u + let mutable afterFirstAIPeek = false + let mutable incorrectPredictedStateId = + false + + let defaultSearcher = + 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 init states = q.AddRange states defaultSearcher.Init q states |> Seq.iter (availableStates.Add >> ignore) + let reset () = defaultSearcher.Reset () defaultSearcherSteps <- 0u @@ -102,33 +129,43 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option 0u q.Clear () availableStates.Clear () + let update (parent, newSates) = if useDefaultSearcher then 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 () - updateGameState gameStateDelta + gameState <- GameUtils.updateGameState gameStateDelta gameState let statistics = computeStatistics gameState.Value Application.applicationGraphDelta.Clear () lastCollectedStatistics <- statistics useDefaultSearcher <- defaultSearcherSteps < stepsToSwitchToAI + defaultSearcher.Pick () elif Seq.length availableStates = 0 then None @@ -137,28 +174,37 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option 0u then - gameStateDelta - else - gameState.Value + match aiMode with + | TrainingSendEachStep + | TrainingSendModel -> + if stepsPlayed > 0u then + gameStateDelta + else + gameState.Value + | Runner -> gameState.Value + let stateId = oracle.Predict toPredict afterFirstAIPeek <- true let state = availableStates |> Seq.tryFind (fun s -> s.internalId = stateId) lastCollectedStatistics <- statistics stepsPlayed <- stepsPlayed + 1u + match state with | Some state -> Some state | None -> @@ -166,12 +212,57 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: 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 stepToString (gameState: GameState) (output: IDisposableReadOnlyCollection) = + let gameStateJson = + JsonSerializer.Serialize gameState + let outputJson = serializeOutput output + let DELIM = Environment.NewLine + let strToSaveAsList = + [ + gameStateJson + DELIM + outputJson + DELIM + ] + String.concat " " strToSaveAsList + + let createOracleRunner (pathToONNX: string, aiAgentTrainingModelOptions: Option) = + let host = "localhost" + let port = + match aiAgentTrainingModelOptions with + | Some options -> options.port + | None -> 0 + + let client = new TcpClient () + client.Connect (host, port) + client.SendBufferSize <- 2048 + let stream = client.GetStream () + + let saveStep (gameState: GameState) (output: IDisposableReadOnlyCollection) = + let bytes = + Encoding.UTF8.GetBytes (stepToString gameState output) + stream.Write (bytes, 0, bytes.Length) + stream.Flush () + let sessionOptions = if useGPU then SessionOptions.MakeSessionOptionWithCudaProvider (0) @@ -186,10 +277,20 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option + currentGameState <- GameUtils.updateGameState gameStateOrDelta currentGameState + | _ -> currentGameState <- Some gameStateOrDelta + let gameState = currentGameState.Value let stateIds = Dictionary, int> () let verticesIds = @@ -197,14 +298,17 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option () + let gameVertices = 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) @@ -216,6 +320,7 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option Array.iteri (fun i e -> index[i] <- int64 verticesIds[e.VertexFrom] @@ -271,11 +379,13 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option Array.iter (fun state -> state.Children @@ -291,7 +402,9 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option Array.iteri (fun i historyElem -> let j = firstFreePositionInHistoryIndex + i @@ -303,7 +416,9 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option Array.iter (fun v -> v.States @@ -334,8 +450,10 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option saveStep gameStateOrDelta output + | None -> () + + stepsPlayed <- stepsPlayed + 1 + let weighedStates = output[0].GetTensorDataAsSpan().ToArray () @@ -364,7 +490,12 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option Some (SendModel aiAgentTrainingModelOptions) + | None -> None + + AISearcher (createOracleRunner (pathToONNX, aiAgentTrainingModelOptions), aiAgentTrainingOptions) interface IForwardSearcher with override x.Init states = init states diff --git a/VSharp.Explorer/Explorer.fs b/VSharp.Explorer/Explorer.fs index ec79cca9f..c0d2e86f8 100644 --- a/VSharp.Explorer/Explorer.fs +++ b/VSharp.Explorer/Explorer.fs @@ -12,7 +12,6 @@ open VSharp.Core open VSharp.Interpreter.IL open CilState open VSharp.Explorer -open VSharp.ML.GameServer.Messages open VSharp.Solver open VSharp.IL.Serializer @@ -45,13 +44,16 @@ type private IExplorer = 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 (DatasetGenerator aiOptions) -> + let mapName = aiOptions.mapName getFolderToStoreSerializationResult (Path.GetDirectoryName explorationOptions.outputDirectory.FullName) - options.mapName + mapName + | _ -> "" + let hasTimeout = explorationOptions.timeout.TotalMilliseconds > 0 @@ -69,6 +71,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM 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 @@ -93,12 +96,14 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM 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 @@ -110,21 +115,32 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM None else Some options.randomSeed + match mode with | AIMode -> - match options.aiAgentTrainingOptions with + let useGPU = + options.useGPU.IsSome && options.useGPU.Value + let optimize = + options.optimize.IsSome && options.optimize.Value + + 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 = - options.useGPU.IsSome && options.useGPU.Value - let optimize = - options.optimize.IsSome && options.optimize.Value - AISearcher (s, useGPU, optimize) + | Some s -> AISearcher (s, useGPU, optimize, None) | None -> failwith "Empty model for AI searcher." | BFSMode -> BFSSearcher () :> IForwardSearcher | DFSMode -> DFSSearcher () :> IForwardSearcher @@ -157,6 +173,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM :> IForwardSearcher else mkForwardSearcher searchMode + BidirectionalSearcher (baseSearcher, BackwardSearcher (), DummyTargetedSearcher.DummyTargetedSearcher ()) :> IBidirectionalSearcher | StackTraceReproductionMode _ -> __notImplemented__ () @@ -166,8 +183,10 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM branchesReleased <- true statistics.OnBranchesReleased () ReleaseBranches () + let dfsSearcher = DFSSortedByContributedCoverageSearcher statistics :> IForwardSearcher + let bidirectionalSearcher = OnlyForwardSearcher (dfsSearcher) dfsSearcher.Init <| searcher.States () @@ -186,13 +205,17 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let isNewHistory () = 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 + if isNewTest then let state = cilState.state let callStackSize = @@ -200,17 +223,21 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let entryMethod = cilState.EntryMethod 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) + match suite with | Test -> reporter.ReportFinished test | Error _ -> reporter.ReportException test + if isCoverageAchieved () then isStopped <- true | None -> () @@ -223,6 +250,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM | :? InsufficientInformationException as e -> if not state.IsIIEState then state.SetIIE e + reportStateIncomplete state | _ -> searcher.Remove state @@ -246,6 +274,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM 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) @@ -259,25 +288,32 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM 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) = let parameterType = pi.ParameterType + if parameterType.IsByRef then if Memory.CallStackSize initialState = 0 then Memory.NewStackFrame initialState None [] + 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) = @@ -286,10 +322,12 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let declaringType = method.DeclaringType 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 @@ -299,15 +337,20 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM Some this else None + 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 @@ -327,11 +370,14 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let parameters = method.Parameters 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 @@ -354,19 +400,24 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM 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 () cilState.CreateWebInitial method state webConfig | _ -> cilState.CreateInitial method state + [ initialState ] with e -> reportInternalFail method e @@ -379,24 +430,31 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM // TODO: update pobs when visiting new methods; use coverageZone 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, 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) 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 @@ -410,25 +468,30 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM 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) = 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 @@ -452,17 +515,22 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM && 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)) s.internalId + firstFreeEpisodeNumber <- firstFreeEpisodeNumber + 1 + x.Forward (s) with e -> reportStateInternalFail s e @@ -481,10 +549,13 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM 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 () |> Seq.iter (fun (pob, status) -> match status with @@ -504,6 +575,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM SolverInteraction.setOnSolverStopped statistics.SolverStopped AcquireBranches () isCoverageAchieved <- always false + match options.explorationMode with | TestCoverageMode _ -> if options.stopOnCoverageAchieved > 0 then @@ -511,6 +583,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let cov = statistics.GetCurrentCoverage entryMethods cov >= options.stopOnCoverageAchieved + isCoverageAchieved <- checkCoverage | StackTraceReproductionMode _ -> __notImplemented__ () @@ -521,14 +594,18 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM interpreter.ConfigureErrorReporter reportError reportFatalError 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) + if not initialStates.IsEmpty then x.AnswerPobs initialStates with e -> @@ -560,11 +637,13 @@ type private FuzzerExplorer(explorationOptions: ExplorationOptions, statistics: 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 onCancelled () = Logger.warning "Fuzzer canceled" + let interactor = Fuzzer.Interactor ( targetAssemblyPath, @@ -574,6 +653,7 @@ type private FuzzerExplorer(explorationOptions: ExplorationOptions, statistics: saveStatistic, onCancelled ) + do! interactor.StartFuzzing () with e -> Logger.error $"Fuzzer unhandled exception: {e}" @@ -612,10 +692,12 @@ type public Explorer(options: ExplorationOptions, reporter: IReporter) = 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 @@ -625,18 +707,23 @@ type public Explorer(options: ExplorationOptions, reporter: IReporter) = 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 @@ -650,6 +737,7 @@ 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 @@ -663,11 +751,13 @@ type public Explorer(options: ExplorationOptions, reporter: IReporter) = 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) -> diff --git a/VSharp.Explorer/Options.fs b/VSharp.Explorer/Options.fs index 4b29327d8..62a509884 100644 --- a/VSharp.Explorer/Options.fs +++ b/VSharp.Explorer/Options.fs @@ -36,6 +36,7 @@ type FuzzerOptions = type Oracle = val Predict: GameState -> uint val Feedback: Feedback -> unit + new(predict, feedback) = { Predict = predict @@ -51,16 +52,44 @@ 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 = { + aiBaseOptions: AIBaseOptions stepsToSwitchToAI: uint stepsToPlay: uint - defaultSearchStrategy: searchMode - serializeSteps: bool - mapName: string - oracle: Option + oracle: option } +type AIAgentTrainingEachStepOptions = + { + aiAgentTrainingOptions: AIAgentTrainingOptions + } + + +type AIAgentTrainingModelOptions = + { + aiAgentTrainingOptions: AIAgentTrainingOptions + outputDirectory: string + port: int + } + + +type AIAgentTrainingMode = + | SendEachStep of AIAgentTrainingEachStepOptions + | SendModel of AIAgentTrainingModelOptions + +type AIOptions = + | Training of AIAgentTrainingMode + | DatasetGenerator of AIBaseOptions + type SVMOptions = { explorationMode: explorationMode @@ -74,7 +103,7 @@ type SVMOptions = stopOnCoverageAchieved: int randomSeed: int stepsLimit: uint - aiAgentTrainingOptions: Option + aiOptions: Option pathToModel: Option useGPU: Option optimize: Option diff --git a/VSharp.ML.GameServer.Runner/Main.fs b/VSharp.ML.GameServer.Runner/Main.fs index 3e26ddb99..f3946d486 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: ResizeArra 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: ResizeArra 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,95 @@ let generateDataForPretraining outputDirectory datasetBasePath (maps: ResizeArra 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) (port: int) = + 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 + port = port + } + ) + + 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 +402,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 +432,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 port | 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