diff --git a/.DS_Store b/.DS_Store deleted file mode 100644 index e330b3264..000000000 Binary files a/.DS_Store and /dev/null differ diff --git a/.github/workflows/build_vsharp.yml b/.github/workflows/build_vsharp.yml index 3ad121329..edc53591f 100644 --- a/.github/workflows/build_vsharp.yml +++ b/.github/workflows/build_vsharp.yml @@ -1,31 +1,39 @@ name: 'Build VSharp' on: - workflow_call + [workflow_call, pull_request, push] jobs: build: runs-on: ubuntu-22.04 steps: + - uses: actions/setup-dotnet@v4 + with: + dotnet-version: '7.0.x' + - name: Checkout VSharp - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: submodules: false - - uses: actions/cache@v3 + + - uses: actions/cache@v4 id: nuget-cache with: path: ~/.nuget/packages key: ${{ runner.os }}-nuget-${{ hashFiles('**/*.csproj', '**/*.fsproj') }} restore-keys: | ${{ runner.os }}-nuget- + - name: Build VSharp run: - dotnet build -c DebugTailRec - - uses: actions/upload-artifact@v3 + dotnet build -c Release + + - uses: actions/upload-artifact@v4 with: name: runner path: ./VSharp.Runner/bin/DebugTailRec/net7.0 - - uses: actions/upload-artifact@v3 + + - uses: actions/upload-artifact@v4 with: name: test_runner path: ./VSharp.TestRunner/bin/DebugTailRec/net7.0 diff --git a/.travis.yml b/.travis.yml index 072ac0b86..ba4bb3ae0 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,8 +1,9 @@ language: csharp mono: none -dotnet: 3.0.100 +dotnet: 6.0 solution: VSharp.sln install: - dotnet restore + - dotnet tool restore script: - dotnet test -c Release diff --git a/VSharp.API/VSharp.API.csproj b/VSharp.API/VSharp.API.csproj index 395ab0041..9613591e3 100644 --- a/VSharp.API/VSharp.API.csproj +++ b/VSharp.API/VSharp.API.csproj @@ -36,7 +36,7 @@ - net7.0 + net8.0 @@ -69,7 +69,7 @@ - + diff --git a/VSharp.API/VSharp.cs b/VSharp.API/VSharp.cs index 07743fd0a..20ea57652 100644 --- a/VSharp.API/VSharp.cs +++ b/VSharp.API/VSharp.cs @@ -5,6 +5,7 @@ using System.Linq; using System.Reflection; using System.Text; +using Microsoft.FSharp.Core; using VSharp.CoverageTool; using VSharp.CSharpUtils; using VSharp.Interpreter.IL; @@ -110,7 +111,7 @@ public IEnumerable Results() public static class TestGenerator { - private class Reporter: IReporter + private class Reporter : IReporter { private readonly UnitTests _unitTests; private readonly bool _isQuiet; @@ -123,7 +124,7 @@ public Reporter(UnitTests unitTests, bool isQuiet) public void ReportFinished(UnitTest unitTest) => _unitTests.GenerateTest(unitTest); public void ReportException(UnitTest unitTest) => _unitTests.GenerateError(unitTest); - public void ReportIIE(InsufficientInformationException iie) {} + public void ReportIIE(InsufficientInformationException iie) { } public void ReportInternalFail(Method? method, Exception exn) { @@ -178,6 +179,7 @@ private static Statistics StartExploration( explorationMode: explorationMode.NewTestCoverageMode( coverageZone, options.Timeout > 0 ? searchMode.NewFairMode(baseSearchMode) : baseSearchMode + ), recThreshold: options.RecursionThreshold, solverTimeout: options.SolverTimeout, @@ -188,8 +190,12 @@ private static Statistics StartExploration( checkAttributes: true, stopOnCoverageAchieved: 100, randomSeed: options.RandomSeed, - stepsLimit: options.StepsLimit - ); + stepsLimit: options.StepsLimit, + aiOptions: options.AIOptions == null ? FSharpOption.None : FSharpOption.Some(options.AIOptions), + pathToModel: options.PathToModel == null ? FSharpOption.None : FSharpOption.Some(options.PathToModel), + useGPU: options.UseGPU, + optimize: options.Optimize + ); var fuzzerOptions = new FuzzerOptions( @@ -279,6 +285,7 @@ private static searchMode ToSiliMode(this SearchStrategy searchStrategy) SearchStrategy.ExecutionTree => searchMode.ExecutionTreeMode, SearchStrategy.ExecutionTreeContributedCoverage => searchMode.NewInterleavedMode(searchMode.ExecutionTreeMode, 1, searchMode.ContributedCoverageMode, 1), SearchStrategy.Interleaved => searchMode.NewInterleavedMode(searchMode.ShortestDistanceBasedMode, 1, searchMode.ContributedCoverageMode, 9), + SearchStrategy.AI => searchMode.AIMode, _ => throw new UnreachableException("Unknown search strategy") }; } @@ -322,7 +329,7 @@ private static int CheckCoverage( public static Statistics Cover(MethodBase method, VSharpOptions options = new()) { AssemblyManager.LoadCopy(method.Module.Assembly); - var methods = new List {method}; + var methods = new List { method }; var statistics = StartExploration(methods, coverageZone.MethodZone, options); if (options.RenderTests) diff --git a/VSharp.API/VSharpOptions.cs b/VSharp.API/VSharpOptions.cs index 91541e2e9..c26eca6ef 100644 --- a/VSharp.API/VSharpOptions.cs +++ b/VSharp.API/VSharpOptions.cs @@ -1,4 +1,6 @@ using System.IO; +using Microsoft.FSharp.Core; +using VSharp.Explorer; namespace VSharp; @@ -38,7 +40,8 @@ public enum SearchStrategy /// /// Interleaves and strategies. /// - Interleaved + Interleaved, + AI } /// @@ -96,6 +99,7 @@ public readonly record struct VSharpOptions private const bool DefaultReleaseBranches = true; private const int DefaultRandomSeed = -1; private const uint DefaultStepsLimit = 0; + private const string DefaultPathToModel = "models/model.onnx"; public readonly int Timeout = DefaultTimeout; public readonly int SolverTimeout = DefaultSolverTimeout; @@ -109,6 +113,10 @@ public readonly record struct VSharpOptions public readonly bool ReleaseBranches = DefaultReleaseBranches; public readonly int RandomSeed = DefaultRandomSeed; public readonly uint StepsLimit = DefaultStepsLimit; + public readonly AIOptions? AIOptions = null; + public readonly string PathToModel = DefaultPathToModel; + public readonly bool UseGPU = false; + public readonly bool Optimize = false; /// /// Symbolic virtual machine options. @@ -125,6 +133,10 @@ 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. + /// 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. public VSharpOptions( int timeout = DefaultTimeout, int solverTimeout = DefaultSolverTimeout, @@ -137,7 +149,11 @@ public VSharpOptions( ExplorationMode explorationMode = DefaultExplorationMode, bool releaseBranches = DefaultReleaseBranches, int randomSeed = DefaultRandomSeed, - uint stepsLimit = DefaultStepsLimit) + uint stepsLimit = DefaultStepsLimit, + AIOptions? aiOptions = null, + string pathToModel = DefaultPathToModel, + bool useGPU = false, + bool optimize = false) { Timeout = timeout; SolverTimeout = solverTimeout; @@ -151,6 +167,10 @@ public VSharpOptions( ReleaseBranches = releaseBranches; RandomSeed = randomSeed; StepsLimit = stepsLimit; + AIOptions = aiOptions; + PathToModel = pathToModel; + UseGPU = useGPU; + Optimize = optimize; } /// @@ -158,4 +178,9 @@ public VSharpOptions( /// public DirectoryInfo RenderedTestsDirectoryInfo => Directory.Exists(RenderedTestsDirectory) ? new DirectoryInfo(RenderedTestsDirectory) : null; + + public string GetDefaultPathToModel() + { + return DefaultPathToModel; + } } diff --git a/VSharp.CSharpUtils/VSharp.CSharpUtils.csproj b/VSharp.CSharpUtils/VSharp.CSharpUtils.csproj index 362dcd884..8f2fceaa2 100644 --- a/VSharp.CSharpUtils/VSharp.CSharpUtils.csproj +++ b/VSharp.CSharpUtils/VSharp.CSharpUtils.csproj @@ -1,7 +1,7 @@ - net7.0 + net8.0 true Debug;Release;DebugTailRec AnyCPU diff --git a/VSharp.CoverageTool/VSharp.CoverageTool.fsproj b/VSharp.CoverageTool/VSharp.CoverageTool.fsproj index e753e049a..32b985fad 100644 --- a/VSharp.CoverageTool/VSharp.CoverageTool.fsproj +++ b/VSharp.CoverageTool/VSharp.CoverageTool.fsproj @@ -1,7 +1,7 @@  - net7.0 + net8.0 true Debug;Release;DebugTailRec AnyCPU @@ -61,7 +61,7 @@ - + diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs new file mode 100644 index 000000000..458b6b2c3 --- /dev/null +++ b/VSharp.Explorer/AISearcher.fs @@ -0,0 +1,493 @@ +namespace VSharp.Explorer + +open System.Collections.Generic +open Microsoft.ML.OnnxRuntime +open System +open System.Text +open System.Text.Json +open VSharp +open VSharp.IL.Serializer +open VSharp.ML.GameServer.Messages + +type AIMode = + | Runner + | TrainingSendModel + | TrainingSendEachStep + + +type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: 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 + lastCollectedStatistics <- Statistics() + gameState <- None + afterFirstAIPeek <- false + incorrectPredictedStateId <- false + useDefaultSearcher <- stepsToSwitchToAI > 0u + q.Clear() + availableStates.Clear() + + let update (parent, newStates) = + if useDefaultSearcher then + defaultSearcher.Update(parent, newStates) + + newStates |> 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 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 () + gameState <- AISearcher.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 + elif Seq.length availableStates = 1 then + Some(Seq.head availableStates) + else + let gameStateDelta = collectGameStateDelta () + gameState <- AISearcher.updateGameState gameStateDelta gameState + let statistics = computeStatistics gameState.Value + + if isInAIMode () then + let reward = computeReward lastCollectedStatistics statistics + oracle.Feedback(Feedback.MoveReward reward) + + Application.applicationGraphDelta.Clear() + + let toPredict = + 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 -> + incorrectPredictedStateId <- true + oracle.Feedback(Feedback.IncorrectPredictedStateId stateId) + None + + static member updateGameState (delta: GameState) (gameState: Option) = + match gameState with + | 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 + + let states = + let part1 = + s.States + |> Array.filter (fun s -> activeStates.Contains s.Id && (not <| updatedStates.Contains s.Id)) + |> ResizeArray<_> + + part1.AddRange delta.States + + part1.ToArray() + |> Array.map (fun s -> + State( + s.Id, + s.Position, + s.PathCondition, + s.VisitedAgainVertices, + s.VisitedNotCoveredVerticesInZone, + s.VisitedNotCoveredVerticesOutOfZone, + s.StepWhenMovedLastTime, + s.InstructionsVisitedInCurrentBlock, + s.History, + s.Children |> Array.filter activeStates.Contains + )) + + let pathConditionVertices = ResizeArray s.PathConditionVertices + + pathConditionVertices.AddRange delta.PathConditionVertices + + Some + <| GameState(vertices.ToArray(), states, pathConditionVertices.ToArray(), edges.ToArray()) + + static member convertOutputToJson(output: IDisposableReadOnlyCollection) = + seq { 0 .. output.Count - 1 } + |> Seq.map (fun i -> output[i].GetTensorDataAsSpan().ToArray()) + + + + new + ( + pathToONNX: string, + useGPU: bool, + optimize: bool, + aiAgentTrainingModelOptions: Option + ) = + let numOfVertexAttributes = 7 + let numOfStateAttributes = 6 + let numOfPathConditionVertexAttributes = 49 + let numOfHistoryEdgeAttributes = 2 + + + let createOracleRunner (pathToONNX: string, aiAgentTrainingModelOptions: Option) = + let sessionOptions = + if useGPU then + SessionOptions.MakeSessionOptionWithCudaProvider(0) + else + new SessionOptions() + + if optimize then + sessionOptions.ExecutionMode <- ExecutionMode.ORT_PARALLEL + sessionOptions.GraphOptimizationLevel <- GraphOptimizationLevel.ORT_ENABLE_ALL + else + sessionOptions.GraphOptimizationLevel <- GraphOptimizationLevel.ORT_ENABLE_BASIC + + let session = new InferenceSession(pathToONNX, sessionOptions) + + let runOptions = new RunOptions() + let feedback (x: Feedback) = () + + let mutable stepsPlayed = 0 + let mutable currentGameState = None + + let predict (gameStateOrDelta: GameState) = + let _ = + match aiAgentTrainingModelOptions with + | Some _ when not (stepsPlayed = 0) -> + currentGameState <- AISearcher.updateGameState gameStateOrDelta currentGameState + | _ -> currentGameState <- Some gameStateOrDelta + + let gameState = currentGameState.Value + let stateIds = Dictionary, int>() + let verticesIds = Dictionary, int>() + let pathConditionVerticesIds = Dictionary, int>() + + let networkInput = + let res = Dictionary<_, _>() + + let pathConditionVertices, numOfPcToPcEdges = + let mutable numOfPcToPcEdges = 0 + + let shape = + [| int64 gameState.PathConditionVertices.Length + numOfPathConditionVertexAttributes |] + + let attributes = + Array.zeroCreate ( + gameState.PathConditionVertices.Length * numOfPathConditionVertexAttributes + ) + + for i in 0 .. gameState.PathConditionVertices.Length - 1 do + let v = gameState.PathConditionVertices.[i] + numOfPcToPcEdges <- numOfPcToPcEdges + v.Children.Length * 2 + pathConditionVerticesIds.Add(v.Id, i) + let j = i * numOfPathConditionVertexAttributes + attributes.[j + int v.Type] <- float32 1u + + OrtValue.CreateTensorValueFromMemory(attributes, shape), numOfPcToPcEdges + + + 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) + let j = i * numOfVertexAttributes + 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) + + let states, numOfParentOfEdges, numOfPathConditionEdges, numOfHistoryEdges = + let mutable numOfParentOfEdges = 0 + let mutable numOfPathConditionEdges = 0 + let mutable numOfHistoryEdges = 0 + 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] + numOfParentOfEdges <- numOfParentOfEdges + v.Children.Length + numOfPathConditionEdges <- numOfPathConditionEdges + v.PathCondition.Length + numOfHistoryEdges <- numOfHistoryEdges + v.History.Length + stateIds.Add(v.Id, i) + let j = i * numOfStateAttributes + attributes.[j] <- float32 v.Position + attributes.[j + 1] <- float32 v.VisitedAgainVertices + attributes.[j + 2] <- float32 v.VisitedNotCoveredVerticesInZone + attributes.[j + 3] <- float32 v.VisitedNotCoveredVerticesOutOfZone + attributes.[j + 4] <- float32 v.StepWhenMovedLastTime + attributes.[j + 5] <- float32 v.InstructionsVisitedInCurrentBlock + + OrtValue.CreateTensorValueFromMemory(attributes, shape), numOfParentOfEdges, numOfPathConditionEdges, numOfHistoryEdges + + let pcToPcEdgeIndex = + let shapeOfIndex = [| 2L; numOfPcToPcEdges |] + let index = Array.zeroCreate (2 * numOfPcToPcEdges) + let mutable firstFreePositionOfIndex = 0 + + for v in gameState.PathConditionVertices do + for child in v.Children do + // from vertex to child + index.[firstFreePositionOfIndex] <- int64 pathConditionVerticesIds.[v.Id] + + index.[firstFreePositionOfIndex + numOfPcToPcEdges] <- + int64 pathConditionVerticesIds.[child] + + firstFreePositionOfIndex <- firstFreePositionOfIndex + 1 + // from child to vertex + index.[firstFreePositionOfIndex] <- int64 pathConditionVerticesIds.[child] + + index.[firstFreePositionOfIndex + numOfPcToPcEdges] <- + int64 pathConditionVerticesIds.[v.Id] + + firstFreePositionOfIndex <- firstFreePositionOfIndex + 1 + + OrtValue.CreateTensorValueFromMemory(index, shapeOfIndex) + + + let vertexToVertexEdgesIndex, vertexToVertexEdgesAttributes = + let shapeOfIndex = [| 2L; gameState.Map.Length |] + let shapeOfAttributes = [| int64 gameState.Map.Length |] + let index = Array.zeroCreate (2 * gameState.Map.Length) + let attributes = Array.zeroCreate gameState.Map.Length + + gameState.Map + |> 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) + + OrtValue.CreateTensorValueFromMemory(index, shapeOfIndex), + OrtValue.CreateTensorValueFromMemory(attributes, shapeOfAttributes) + + let historyEdgesIndex_vertexToState, historyEdgesAttributes, parentOfEdges, edgeIndex_pcToState = + let shapeOfParentOf = [| 2L; numOfParentOfEdges |] + let parentOf = Array.zeroCreate (2 * numOfParentOfEdges) + let shapeOfHistory = [| 2L; numOfHistoryEdges |] + let historyIndex_vertexToState = Array.zeroCreate (2 * numOfHistoryEdges) + let shapeOfPcToState = [| 2L; numOfPathConditionEdges |] + let index_pcToState = Array.zeroCreate (2 * numOfPathConditionEdges) + + let shapeOfHistoryAttributes = + [| int64 numOfHistoryEdges; int64 numOfHistoryEdgeAttributes |] + + let historyAttributes = Array.zeroCreate (2 * numOfHistoryEdges) + let mutable firstFreePositionInParentsOf = 0 + let mutable firstFreePositionInHistoryIndex = 0 + let mutable firstFreePositionInHistoryAttributes = 0 + let mutable firstFreePositionInPcToState = 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]) + + firstFreePositionInParentsOf <- firstFreePositionInParentsOf + state.Children.Length + + state.PathCondition + |> Array.iteri (fun i pcId -> + let j = firstFreePositionInPcToState + i + index_pcToState[j] <- int64 pathConditionVerticesIds[pcId] + index_pcToState[numOfPathConditionEdges + j] <- int64 stateIds[state.Id]) + + firstFreePositionInPcToState <- firstFreePositionInPcToState + state.PathCondition.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 + historyAttributes[j] <- int64 historyElem.NumOfVisits + historyAttributes[j + 1] <- int64 historyElem.StepWhenVisitedLastTime) + + firstFreePositionInHistoryIndex <- firstFreePositionInHistoryIndex + state.History.Length + + firstFreePositionInHistoryAttributes <- + firstFreePositionInHistoryAttributes + + numOfHistoryEdgeAttributes * state.History.Length) + + OrtValue.CreateTensorValueFromMemory(historyIndex_vertexToState, shapeOfHistory), + OrtValue.CreateTensorValueFromMemory(historyAttributes, shapeOfHistoryAttributes), + OrtValue.CreateTensorValueFromMemory(parentOf, shapeOfParentOf), + OrtValue.CreateTensorValueFromMemory(index_pcToState, shapeOfPcToState) + + 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 mutable firstFreePosition = 0 + + gameState.GraphVertices + |> Array.iter (fun v -> + v.States + |> Array.iteri (fun i stateId -> + let j = firstFreePosition + i + let stateIndex = int64 stateIds[stateId] + let vertexIndex = int64 verticesIds[v.Id] + data_stateToVertex[j] <- stateIndex + data_stateToVertex[stateIds.Count + j] <- vertexIndex + + data_vertexToState[j] <- vertexIndex + data_vertexToState[stateIds.Count + j] <- stateIndex) + + firstFreePosition <- firstFreePosition + v.States.Length) + + OrtValue.CreateTensorValueFromMemory(data_stateToVertex, shape), + OrtValue.CreateTensorValueFromMemory(data_vertexToState, shape) + + res.Add("game_vertex", gameVertices) + res.Add("state_vertex", states) + res.Add("path_condition_vertex", pathConditionVertices) + + res.Add("gamevertex_to_gamevertex_index", vertexToVertexEdgesIndex) + res.Add("gamevertex_to_gamevertex_type", vertexToVertexEdgesAttributes) + + res.Add("gamevertex_history_statevertex_index", historyEdgesIndex_vertexToState) + res.Add("gamevertex_history_statevertex_attrs", historyEdgesAttributes) + + res.Add("gamevertex_in_statevertex", statePosition_vertexToState) + res.Add("statevertex_parentof_statevertex", parentOfEdges) + + res.Add("pathconditionvertex_to_pathconditionvertex", pcToPcEdgeIndex) + res.Add("pathconditionvertex_to_statevertex", edgeIndex_pcToState) + + res + + let output = session.Run(runOptions, networkInput, session.OutputNames) + + let _ = + match aiAgentTrainingModelOptions with + | Some aiAgentOptions -> + aiAgentOptions.stepSaver ( + AIGameStep(gameState = gameStateOrDelta, output = AISearcher.convertOutputToJson output) + ) + | None -> () + + 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) + + let aiAgentTrainingOptions = + match aiAgentTrainingModelOptions with + | Some aiAgentTrainingModelOptions -> Some(SendModel aiAgentTrainingModelOptions) + | None -> None + + AISearcher(createOracleRunner (pathToONNX, aiAgentTrainingModelOptions), aiAgentTrainingOptions) + + interface IForwardSearcher with + override x.Init states = init states + 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.Remove cilState = remove cilState + override x.StatesCount = availableStates.Count diff --git a/VSharp.Explorer/Explorer.fs b/VSharp.Explorer/Explorer.fs index 847c78dfc..94eb5afef 100644 --- a/VSharp.Explorer/Explorer.fs +++ b/VSharp.Explorer/Explorer.fs @@ -13,50 +13,61 @@ open VSharp.Interpreter.IL open CilState open VSharp.Explorer 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 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 with get() = - 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) = +type WebConfiguration + (mainArguments: string[], environmentName: string, contentRootPath: DirectoryInfo, applicationName: string) = inherit EntryPointConfiguration(mainArguments) member internal x.ToWebConfig() = - { - environmentName = environmentName - contentRootPath = contentRootPath - applicationName = applicationName - } + { environmentName = environmentName + contentRootPath = contentRootPath + applicationName = applicationName } type private IExplorer = 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) = - let options = explorationOptions.svmOptions + let folderToStoreSerializationResult = + match options.aiOptions with + | Some(DatasetGenerator aiOptions) -> + let mapName = aiOptions.mapName + + getFolderToStoreSerializationResult + (Path.GetDirectoryName explorationOptions.outputDirectory.FullName) + mapName + | _ -> "" + let hasTimeout = explorationOptions.timeout.TotalMilliseconds > 0 let solverTimeout = - if options.solverTimeout > 0 then options.solverTimeout * 1000 + if options.solverTimeout > 0 then + options.solverTimeout * 1000 // Setting timeout / 2 as solver's timeout doesn't guarantee that SILI // stops exactly in timeout. To guarantee that we need to pass timeout // based on remaining time to solver dynamically. - elif hasTimeout then int explorationOptions.timeout.TotalMilliseconds / 2 - else -1 + elif hasTimeout then + int explorationOptions.timeout.TotalMilliseconds / 2 + else + -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 @@ -64,67 +75,110 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let hasStepsLimit = options.stepsLimit > 0u do - API.ConfigureSolver(SolverPool.mkSolver(solverTimeout)) + 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() do if options.visualize then - DotVisualizer explorationOptions.outputDirectory :> IVisualizer |> Application.setVisualizer + 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 | _ -> false let rec mkForwardSearcher mode = - let getRandomSeedOption() = if options.randomSeed < 0 then None else Some options.randomSeed + let getRandomSeedOption () = + if options.randomSeed < 0 then + None + else + Some options.randomSeed + match mode with + | AIMode -> + let useGPU = options.useGPU + let optimize = options.optimize + + match options.aiOptions with + | Some aiOptions -> + 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 -> AISearcher(s, useGPU, optimize, None) + | None -> failwith "Empty model for AI searcher." | BFSMode -> BFSSearcher() :> IForwardSearcher | DFSMode -> DFSSearcher() :> IForwardSearcher | ShortestDistanceBasedMode -> ShortestDistanceBasedSearcher statistics :> IForwardSearcher - | RandomShortestDistanceBasedMode -> RandomShortestDistanceBasedSearcher(statistics, getRandomSeedOption()) :> IForwardSearcher + | RandomShortestDistanceBasedMode -> + RandomShortestDistanceBasedSearcher(statistics, getRandomSeedOption ()) :> IForwardSearcher | ContributedCoverageMode -> DFSSortedByContributedCoverageSearcher statistics :> IForwardSearcher - | ExecutionTreeMode -> ExecutionTreeSearcher(getRandomSeedOption()) + | ExecutionTreeMode -> ExecutionTreeSearcher(getRandomSeedOption ()) | FairMode baseMode -> - FairSearcher((fun _ -> mkForwardSearcher baseMode), uint branchReleaseTimeout, statistics) :> IForwardSearcher + FairSearcher((fun _ -> mkForwardSearcher baseMode), uint branchReleaseTimeout, statistics) + :> IForwardSearcher | InterleavedMode(base1, stepCount1, base2, stepCount2) -> - InterleavedSearcher([mkForwardSearcher base1, stepCount1; mkForwardSearcher base2, stepCount2]) :> IForwardSearcher + InterleavedSearcher([ mkForwardSearcher base1, stepCount1; mkForwardSearcher base2, stepCount2 ]) + :> IForwardSearcher - let mutable searcher : IBidirectionalSearcher = + let mutable searcher: IBidirectionalSearcher = match options.explorationMode with | TestCoverageMode(_, searchMode) -> let baseSearcher = if options.recThreshold > 0u then - GuidedSearcher(mkForwardSearcher searchMode, RecursionBasedTargetManager(statistics, options.recThreshold)) :> IForwardSearcher + GuidedSearcher( + mkForwardSearcher searchMode, + RecursionBasedTargetManager(statistics, options.recThreshold) + ) + :> IForwardSearcher else mkForwardSearcher searchMode - BidirectionalSearcher(baseSearcher, BackwardSearcher(), DummyTargetedSearcher.DummyTargetedSearcher()) :> IBidirectionalSearcher - | StackTraceReproductionMode _ -> __notImplemented__() - let releaseBranches() = + BidirectionalSearcher(baseSearcher, BackwardSearcher(), DummyTargetedSearcher.DummyTargetedSearcher()) + :> IBidirectionalSearcher + | StackTraceReproductionMode _ -> __notImplemented__ () + + let releaseBranches () = if not branchesReleased then branchesReleased <- true statistics.OnBranchesReleased() ReleaseBranches() - let dfsSearcher = DFSSortedByContributedCoverageSearcher statistics :> IForwardSearcher + + let dfsSearcher = + DFSSortedByContributedCoverageSearcher statistics :> IForwardSearcher + 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) Application.terminateState state @@ -132,44 +186,54 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let reportIncomplete = reporter.ReportIIE - let reportState (suite : testSuite) (cilState : cilState) = + let reportState (suite: testSuite) (cilState: cilState) = try - let isNewHistory() = + 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() + | Test -> isNewHistory () | Error(msg, isFatal) -> statistics.IsNewError cilState msg isFatal + if isNewTest then let state = cilState.state let callStackSize = Memory.CallStackSize state 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 + 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 + + if isCoverageAchieved () then isStopped <- true | None -> () with :? InsufficientInformationException as e -> 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 @@ -177,23 +241,23 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM 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 + | :? InsufficientInformationException as e -> reportIncomplete 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) reportState testSuite state @@ -202,76 +266,106 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let reportFatalError = wrapOnError true let reportCrash = reporter.ReportCrash - let isTimeoutReached() = hasTimeout && statistics.CurrentExplorationTime.TotalMilliseconds >= explorationOptions.timeout.TotalMilliseconds - let shouldReleaseBranches() = options.releaseBranches && statistics.CurrentExplorationTime.TotalMilliseconds >= branchReleaseTimeout - let isStepsLimitReached() = hasStepsLimit && statistics.StepsCount >= options.stepsLimit + let isTimeoutReached () = + hasTimeout + && statistics.CurrentExplorationTime.TotalMilliseconds + >= explorationOptions.timeout.TotalMilliseconds - static member private AllocateByRefParameters initialState (method : Method) = - let allocateIfByRef (pi : ParameterInfo) = + 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 + + 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 this = if method.HasThis then if Types.IsValueType declaringType then Memory.NewStackFrame initialState None [] - Memory.AllocateTemporaryLocalVariableOfType initialState "this" 0 declaringType |> Some + + Memory.AllocateTemporaryLocalVariableOfType initialState "this" 0 declaringType + |> Some else let this = Memory.MakeSymbolicThis initialState method !!(IsNullReference this) |> AddConstraint initialState Some this - else None + 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) + + 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 else Memory.MarkTypeInitialized initialState declaringType cilStates - with - | e -> + with e -> reportInternalFail method e [] - member private x.FormEntryPointInitialStates (method : Method, config : EntryPointConfiguration, initialState : state) : cilState list = + member private x.FormEntryPointInitialStates + (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 state = { initialState with complete = not hasParameters || Option.isSome optionArgs } + + 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 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) + assert (Array.length parameters = 1) let argsParameter = Array.head parameters let argsParameterTerm = Memory.ReadArgument state argsParameter AddConstraint state (!!(IsNullReference argsParameterTerm)) @@ -279,101 +373,144 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let modelState = match state.model with | StateModel modelState -> modelState - | _ -> __unreachable__() - let argsForModel = Memory.AllocateVectorArray modelState (MakeNumber 0) typeof + | _ -> __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 -> + + [ 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 + 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) + + 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) + + 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 - | _, s'::iieStates, _ when LanguagePrimitives.PhysicalEquality s s' -> - goodStates @ iieStates @ errors - | _, _, s'::errors when LanguagePrimitives.PhysicalEquality s s' -> - goodStates @ iieStates @ errors + | s' :: goodStates, _, _ when LanguagePrimitives.PhysicalEquality s s' -> goodStates @ iieStates @ errors + | _, s' :: iieStates, _ when LanguagePrimitives.PhysicalEquality s s' -> goodStates @ iieStates @ errors + | _, _, s' :: errors when LanguagePrimitives.PhysicalEquality s s' -> goodStates @ iieStates @ errors | _ -> sIsStopped <- true goodStates @ iieStates @ errors + + s.children <- s.children @ newStates 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) + 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} + + 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) + | false -> Logger.trace "UNSAT for pob = %O and s'.PC = %s" p' (API.Print.PrintPC s'.state.pc) member private x.BidirectionalSymbolicExecution() = + let mutable action = Stop - let pick() = + + let pick () = match searcher.Pick() with | Stop -> false - | a -> action <- a; true + | a -> + action <- a + true (* TODO: checking for timeout here is not fine-grained enough (that is, we can work significantly beyond the timeout, but we'll live with it for now. *) - while not isStopped && not <| isStepsLimitReached() && not <| isTimeoutReached() && pick() do - if shouldReleaseBranches() then - releaseBranches() + while not isStopped + && not <| isStepsLimitReached () + && not <| isTimeoutReached () + && pick () do + if shouldReleaseBranches () then + releaseBranches () + match action with | GoFront s -> try + let needToSerialize = + match options.aiOptions with + | Some(DatasetGenerator _) -> true + | _ -> false + + if needToSerialize then + dumpGameState + (Path.Combine(folderToStoreSerializationResult, string firstFreeEpisodeNumber)) + s.internalId + + pathConditionVertices.Clear() + resetPathConditionVertexIdCounter () + firstFreeEpisodeNumber <- firstFreeEpisodeNumber + 1 + x.Forward(s) - with - | e -> reportStateInternalFail s e + with e -> + reportStateInternalFail s e | GoBack(s, p) -> try x.Backward p s - with - | e -> reportStateInternalFail s e - | Stop -> __unreachable__() + with e -> + reportStateInternalFail s e + | Stop -> __unreachable__ () member private x.AnswerPobs initialStates = statistics.ExplorationStarted() @@ -383,19 +520,24 @@ 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 + + initialStates + |> Seq.filter (fun s -> s.IsIIEState) + |> Seq.iter reportStateIncomplete + x.BidirectionalSymbolicExecution() - searcher.Statuses() |> Seq.iter (fun (pob, status) -> + + searcher.Statuses() + |> Seq.iter (fun (pob, status) -> match status with - | pobStatus.Unknown -> - Logger.warning $"Unknown status for pob at {pob.loc}" + | pobStatus.Unknown -> Logger.warning $"Unknown status for pob at {pob.loc}" | _ -> ()) interface IExplorer with member x.Reset entryMethods = - HashMap.clear() + HashMap.clear () API.Reset() - SolverPool.reset() + SolverPool.reset () searcher.Reset() isStopped <- false branchesReleased <- false @@ -403,14 +545,16 @@ 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 - let checkCoverage() = + let checkCoverage () = let cov = statistics.GetCurrentCoverage entryMethods cov >= options.stopOnCoverageAchieved + isCoverageAchieved <- checkCoverage - | StackTraceReproductionMode _ -> __notImplemented__() + | StackTraceReproductionMode _ -> __notImplemented__ () member x.StartExploration isolated entryPoints = task { @@ -418,22 +562,29 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM try interpreter.ConfigureErrorReporter reportError reportFatalError let isolatedInitialStates = isolated |> List.collect x.FormIsolatedInitialStates - let entryPointsInitialStates = entryPoints |> List.collect x.FormEntryPointInitialStates + + 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 -> reportCrash e + with e -> + reportCrash e finally try statistics.ExplorationFinished() API.Restore() searcher.Reset() - with e -> reportCrash e + with e -> + reportCrash e } member private x.Stop() = isStopped <- true @@ -450,25 +601,29 @@ type private FuzzerExplorer(explorationOptions: ExplorationOptions, statistics: 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 onCancelled () = Logger.warning "Fuzzer canceled" - let interactor = Fuzzer.Interactor( - targetAssemblyPath, - methodsBase, - cancellationTokenSource.Token, - outputDir, - saveStatistic, - onCancelled - ) - do! interactor.StartFuzzing () + + let interactor = + Fuzzer.Interactor( + targetAssemblyPath, + methodsBase, + cancellationTokenSource.Token, + outputDir, + saveStatistic, + onCancelled + ) + + 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) @@ -480,25 +635,30 @@ type public Explorer(options : ExplorationOptions, reporter: IReporter) = SVMExplorer(options, statistics, reporter) :> IExplorer match options.explorationModeOptions with - | Fuzzing _ -> createFuzzer() |> Array.singleton - | SVM _ -> createSVM() |> Array.singleton - | Combined _ -> - [| - createFuzzer() - createSVM() - |] - - let inCoverageZone coverageZone (entryMethods : Method list) = + | Fuzzing _ -> createFuzzer () |> Array.singleton + | SVM _ -> createSVM () |> Array.singleton + | Combined _ -> [| createFuzzer (); createSVM () |] + + let inCoverageZone coverageZone (entryMethods: Method list) = match coverageZone with | MethodZone -> fun method -> entryMethods |> List.contains method - | ClassZone -> fun method -> entryMethods |> List.exists (fun m -> method.DeclaringType.TypeHandle = m.DeclaringType.TypeHandle) - | ModuleZone -> fun method -> entryMethods |> List.exists (fun m -> method.Module.ModuleHandle = m.Module.ModuleHandle) - - member private x.TrySubstituteTypeParameters (state : state) (methodBase : MethodBase) = + | ClassZone -> + fun method -> + entryMethods + |> List.exists (fun m -> method.DeclaringType.TypeHandle = m.DeclaringType.TypeHandle) + | ModuleZone -> + fun method -> + entryMethods + |> List.exists (fun m -> method.Module.ModuleHandle = m.Module.ModuleHandle) + + member private x.TrySubstituteTypeParameters (state: state) (methodBase: MethodBase) = let method = Application.getMethod methodBase - let getConcreteType = function - | ConcreteType t -> Some t - | _ -> None + + let getConcreteType = + function + | ConcreteType t -> Some t + | _ -> None + try if method.ContainsGenericParameters then match SolveGenericMethodParameters state.typeStorage method with @@ -506,42 +666,56 @@ type public Explorer(options : ExplorationOptions, reporter: IReporter) = let classParams = classParams |> Array.choose getConcreteType let methodParams = methodParams |> Array.choose getConcreteType let declaringType = methodBase.DeclaringType - let isSuitableType() = + + let isSuitableType () = not declaringType.IsGenericType || classParams.Length = declaringType.GetGenericArguments().Length - let isSuitableMethod() = + + 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 + + if isSuitableType () && isSuitableMethod () then + let reflectedType = + Reflection.concretizeTypeParameters methodBase.ReflectedType classParams + + let method = + Reflection.concretizeMethodParameters reflectedType methodBase methodParams + Some method else None | _ -> None - else Some methodBase - with - | e -> + else + Some methodBase + with e -> reporter.ReportInternalFail method e None 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) : unit = + member x.StartExploration + (isolated: MethodBase seq) + (entryPoints: (MethodBase * EntryPointConfiguration) seq) + : unit = try let trySubstituteTypeParameters method = 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 + |> Seq.map (fun (m, s) -> Application.getMethod m, s) + |> Seq.toList + let entryPoints = entryPoints |> Seq.map (fun (m, a) -> @@ -549,28 +723,26 @@ type public Explorer(options : ExplorationOptions, reporter: IReporter) = (Application.getMethod m, a, s)) |> Seq.toList - (List.map fst isolated) - @ (List.map (fun (x, _, _) -> x) entryPoints) - |> x.Reset + (List.map fst isolated) @ (List.map (fun (x, _, _) -> x) entryPoints) |> x.Reset let explorationTasks = - explorers - |> Array.map (fun e -> e.StartExploration isolated entryPoints) + explorers |> Array.map (fun e -> e.StartExploration isolated entryPoints) let finished = Task.WaitAll(explorationTasks, options.timeout) - if not finished then Logger.warning "Exploration cancelled" + if not finished then + Logger.warning "Exploration cancelled" for explorationTask in explorationTasks do if explorationTask.IsFaulted then for ex in explorationTask.Exception.InnerExceptions do - reporter.ReportCrash ex + reporter.ReportCrash ex with | :? AggregateException as e -> reporter.ReportCrash e.InnerException | e -> reporter.ReportCrash e - member x.Statistics with get() = statistics + member x.Statistics = statistics interface IDisposable with member x.Dispose() = (statistics :> IDisposable).Dispose() diff --git a/VSharp.Explorer/Options.fs b/VSharp.Explorer/Options.fs index 8a138d72c..1d94d900b 100644 --- a/VSharp.Explorer/Options.fs +++ b/VSharp.Explorer/Options.fs @@ -2,6 +2,9 @@ namespace VSharp.Explorer open System.Diagnostics open System.IO +open VSharp.ML.GameServer.Messages +open System.Net.Sockets +open Microsoft.ML.OnnxRuntime type searchMode = | DFSMode @@ -12,6 +15,7 @@ type searchMode = | ExecutionTreeMode | FairMode of searchMode | InterleavedMode of searchMode * int * searchMode * int + | AIMode type coverageZone = | MethodZone @@ -22,56 +26,114 @@ type explorationMode = | TestCoverageMode of coverageZone * searchMode | StackTraceReproductionMode of StackTrace -type fuzzerIsolation = - | Process - -type FuzzerOptions = { - isolation: fuzzerIsolation - coverageZone: coverageZone -} - -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 -} +type fuzzerIsolation = | Process + +type FuzzerOptions = + { isolation: fuzzerIsolation + coverageZone: coverageZone } + +[] +type Oracle = + val Predict: GameState -> uint + val Feedback: Feedback -> unit + + new(predict, feedback) = + { Predict = predict + Feedback = feedback } + +/// +/// Options used in AI agent training. +/// +/// Number of steps of default searcher prior to switch to AI mode. +/// Number of steps to play in AI mode. +/// Default searcher that will be used to play few initial steps. +/// Determine whether steps should be serialized. +/// Name of map to play. +/// Name of map to play. + +[] +type AIGameStep = + interface IRawOutgoingMessageBody + val GameState: GameState + val Output: seq> + + new(gameState, output) = + { GameState = gameState + Output = output } + + +type AIBaseOptions = + { defaultSearchStrategy: searchMode + mapName: string } + +type AIAgentTrainingOptions = + { aiBaseOptions: AIBaseOptions + stepsToSwitchToAI: uint + stepsToPlay: uint + oracle: option } + +type AIAgentTrainingEachStepOptions = + { aiAgentTrainingOptions: AIAgentTrainingOptions } + + +type AIAgentTrainingModelOptions = + { aiAgentTrainingOptions: AIAgentTrainingOptions + outputDirectory: string + stepSaver: AIGameStep -> Unit } + + +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 + aiOptions: Option + pathToModel: Option + useGPU: bool + optimize: bool } type explorationModeOptions = | Fuzzing of FuzzerOptions | SVM of SVMOptions | Combined of SVMOptions * FuzzerOptions -type ExplorationOptions = { - timeout : System.TimeSpan - outputDirectory : DirectoryInfo - explorationModeOptions : explorationModeOptions -} -with +type ExplorationOptions = + { 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.Explorer/Statistics.fs b/VSharp.Explorer/Statistics.fs index f3a1c1037..1e21b3b43 100644 --- a/VSharp.Explorer/Statistics.fs +++ b/VSharp.Explorer/Statistics.fs @@ -13,6 +13,7 @@ open FSharpx.Collections open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.ML.GameServer.Messages open VSharp.Utils open CilState @@ -159,6 +160,7 @@ type public SVMStatistics(entryMethods : Method seq, generalizeGenericsCoverage member x.TrackStepForward (s : cilState) (ip : instructionPointer) (stackSize : int) = stepsCount <- stepsCount + 1u + s.stepWhenMovedLastTime <- stepsCount * 1u Logger.traceWithTag Logger.stateTraceTag $"{stepsCount} FORWARD: {s.internalId}" let setCoveredIfNeeded (loc : codeLocation) = @@ -227,6 +229,8 @@ type public SVMStatistics(entryMethods : Method seq, generalizeGenericsCoverage let mutable hasNewCoverage = false let blocks = Seq.distinct blocks for block in blocks do + block.BasicBlock.IsCovered <- true + let added = Application.applicationGraphDelta.TouchedBasicBlocks.Add block.BasicBlock let generalizedMethod = generalizeIfNeeded block.method let method = block.method let mutable isNewBlock = false diff --git a/VSharp.Explorer/VSharp.Explorer.fsproj b/VSharp.Explorer/VSharp.Explorer.fsproj index 23cc6c3f3..f10d1162b 100644 --- a/VSharp.Explorer/VSharp.Explorer.fsproj +++ b/VSharp.Explorer/VSharp.Explorer.fsproj @@ -1,7 +1,7 @@  - net7.0 + net8.0 Debug;Release;DebugTailRec AnyCPU true @@ -32,7 +32,11 @@ + + + PreserveNewest + @@ -44,6 +48,8 @@ - + + + diff --git a/VSharp.Explorer/models/model.onnx b/VSharp.Explorer/models/model.onnx new file mode 100644 index 000000000..238d24e77 Binary files /dev/null and b/VSharp.Explorer/models/model.onnx differ diff --git a/VSharp.Fuzzer/VSharp.Fuzzer.fsproj b/VSharp.Fuzzer/VSharp.Fuzzer.fsproj index 5ca5c3305..47bb867f3 100644 --- a/VSharp.Fuzzer/VSharp.Fuzzer.fsproj +++ b/VSharp.Fuzzer/VSharp.Fuzzer.fsproj @@ -2,7 +2,7 @@ Exe - net7.0 + net8.0 Debug;Release;DebugTailRec AnyCPU $(DefineConstants);TRACEX @@ -41,7 +41,7 @@ - + diff --git a/VSharp.IL/CFG.fs b/VSharp.IL/CFG.fs index 6bafd5834..6de1eb186 100644 --- a/VSharp.IL/CFG.fs +++ b/VSharp.IL/CFG.fs @@ -2,11 +2,13 @@ namespace VSharp open System.Collections.Concurrent open VSharp.GraphUtils +open VSharp.ML.GameServer.Messages open global.System open System.Reflection open System.Collections.Generic open Microsoft.FSharp.Collections open VSharp +open VSharp.Core type ICallGraphNode = inherit IGraphNode @@ -14,29 +16,63 @@ type ICallGraphNode = type IReversedCallGraphNode = inherit IGraphNode -module CallGraph = - let callGraphDistanceFrom = Dictionary>() - let callGraphDistanceTo = Dictionary>() +type coverageType = + | ByTest + | ByEntryPointTest type [] terminalSymbol -type ICfgNode = - inherit IGraphNode - abstract Offset : offset +module CallGraph = + let callGraphDistanceFrom = Dictionary>() + let callGraphDistanceTo = Dictionary>() + let dummyTerminalForCallShortcut = 3 + +type ICfgNode = + inherit IGraphNode + abstract Offset : offset + +type IInterproceduralCfgNode = + inherit IGraphNode + abstract IsCovered : bool with get + abstract IsVisited : bool with get + abstract IsTouched : bool with get + abstract IsGoal : bool with get + abstract IsSink : bool with get + + +[] +type EdgeType = + | CFG + | ShortcutForCall + | Call of int + | Return of int + +[] +type EdgeLabel = + val EdgeType: EdgeType + val IsCovered: bool + val IsVisited: bool + [] type internal temporaryCallInfo = {callee: MethodWithBody; callFrom: offset; returnTo: offset} -type BasicBlock (method: MethodWithBody, startOffset: offset) = +type BasicBlock (method: MethodWithBody, startOffset: offset, id:uint) = let mutable finalOffset = startOffset + let mutable containsCall = false + let mutable containsThrow = false let mutable startOffset = startOffset let mutable isGoal = false let mutable isCovered = false + let mutable isVisited = false + let mutable isSink = false + let mutable visitedInstructions = 0u let associatedStates = HashSet() let incomingCFGEdges = HashSet() let incomingCallEdges = HashSet() let outgoingEdges = Dictionary, HashSet>() + member this.Id = id member this.StartOffset with get () = startOffset and internal set v = startOffset <- v @@ -45,12 +81,23 @@ type BasicBlock (method: MethodWithBody, startOffset: offset) = member this.IncomingCFGEdges = incomingCFGEdges member this.IncomingCallEdges = incomingCallEdges member this.AssociatedStates = associatedStates + member this.VisitedInstructions + with get () = visitedInstructions + and set v = visitedInstructions <- v member this.IsCovered with get () = isCovered and set v = isCovered <- v + member this.IsVisited + with get () = isVisited + and set v = isVisited <- v member this.IsGoal with get () = isGoal and set v = isGoal <- v + member this.IsTouched + with get () = visitedInstructions > 0u + member this.IsSink + with get () = isSink + and set v = isSink <- v member this.HasSiblings with get () = let siblings = HashSet() @@ -60,10 +107,18 @@ type BasicBlock (method: MethodWithBody, startOffset: offset) = siblings.Count > 1 member this.FinalOffset - with get () = finalOffset - and internal set (v : offset) = finalOffset <- v - - member private this.GetInstructions() = + with get () = finalOffset + and set (v: offset) = finalOffset <- v + + member this.ContainsCall + with get () = containsCall + and set (v: bool) = containsCall <- v + + member this.ContainsThrow + with get () = containsThrow + and set (v: bool) = containsThrow <- v + + member this.GetInstructions() = let parsedInstructions = method.ParsedInstructions let mutable instr = parsedInstructions[this.StartOffset] assert(Offset.from (int instr.offset) = this.StartOffset) @@ -83,16 +138,34 @@ type BasicBlock (method: MethodWithBody, startOffset: offset) = member this.BlockSize with get() = this.GetInstructions() |> Seq.length - + interface ICfgNode with member this.OutgoingEdges with get () = - let exists, cfgEdges = outgoingEdges.TryGetValue CfgInfo.TerminalForCFGEdge - if exists - then cfgEdges |> Seq.cast - else Seq.empty + let exists1,cfgEdges = outgoingEdges.TryGetValue CfgInfo.TerminalForCFGEdge + let exists2,cfgSpecialEdges = outgoingEdges.TryGetValue CallGraph.dummyTerminalForCallShortcut + seq{ + if exists1 + then yield! cfgEdges |> Seq.cast + if exists2 + then yield! cfgSpecialEdges |> Seq.cast + } member this.Offset = startOffset - + + interface IInterproceduralCfgNode with + member this.OutgoingEdges + with get () = + seq{ + for kvp in outgoingEdges do + if kvp.Key <> CallGraph.dummyTerminalForCallShortcut + then yield! kvp.Value |> Seq.cast + } + member this.IsCovered with get() = this.IsCovered + member this.IsVisited with get() = this.IsVisited + member this.IsTouched with get() = this.IsTouched + member this.IsGoal with get() = this.IsGoal + member this.IsSink with get() = this.IsSink + and [] CallInfo = val Callee: Method val CallFrom: offset @@ -102,10 +175,10 @@ and [] CallInfo = Callee = callee CallFrom = callFrom ReturnTo = returnTo - } + } -and CfgInfo internal (method : MethodWithBody) = - let () = assert method.HasBody +and CfgInfo internal (method : MethodWithBody, getNextBasicBlockGlobalId: unit -> uint) = + let () = assert method.HasBody let ilBytes = method.ILBytes let exceptionHandlers = method.ExceptionHandlers let sortedBasicBlocks = ResizeArray() @@ -142,7 +215,7 @@ and CfgInfo internal (method : MethodWithBody) = let splitBasicBlock (block : BasicBlock) intermediatePoint = - let newBlock = BasicBlock(method, block.StartOffset) + let newBlock = BasicBlock(method, block.StartOffset, getNextBasicBlockGlobalId()) addBasicBlock newBlock block.StartOffset <- intermediatePoint @@ -170,7 +243,7 @@ and CfgInfo internal (method : MethodWithBody) = let makeNewBasicBlock startVertex = match vertexToBasicBlock[int startVertex] with | None -> - let newBasicBlock = BasicBlock(method, startVertex) + let newBasicBlock = BasicBlock(method, startVertex, getNextBasicBlockGlobalId()) vertexToBasicBlock[int startVertex] <- Some newBasicBlock addBasicBlock newBasicBlock newBasicBlock @@ -213,6 +286,7 @@ and CfgInfo internal (method : MethodWithBody) = let processCall (callee : MethodWithBody) callFrom returnTo k = calls.Add(currentBasicBlock, CallInfo(callee :?> Method, callFrom, returnTo)) currentBasicBlock.FinalOffset <- callFrom + currentBasicBlock.ContainsThrow <- true let newBasicBlock = makeNewBasicBlock returnTo addEdge currentBasicBlock newBasicBlock dfs' newBasicBlock returnTo k @@ -273,7 +347,7 @@ and CfgInfo internal (method : MethodWithBody) = if i.Value <> infinity then distFromNode.Add(i.Key, i.Value) distFromNode) - + let resolveBasicBlockIndex offset = let rec binSearch (sortedOffsets : ResizeArray) offset l r = if l >= r then l @@ -290,11 +364,11 @@ and CfgInfo internal (method : MethodWithBody) = binSearch sortedBasicBlocks offset 0 (sortedBasicBlocks.Count - 1) let resolveBasicBlock offset = sortedBasicBlocks[resolveBasicBlockIndex offset] - + do let startVertices = [| - yield 0 + yield 0 for handler in exceptionHandlers do yield handler.handlerOffset match handler.ehcType with @@ -322,12 +396,12 @@ and CfgInfo internal (method : MethodWithBody) = let basicBlock = resolveBasicBlock offset basicBlock.HasSiblings -and Method internal (m : MethodBase) as this = +and Method internal (m : MethodBase,getNextBasicBlockGlobalId) as this = inherit MethodWithBody(m) let cfg = lazy( if this.HasBody then Logger.trace $"Add CFG for {this}." - let cfg = CfgInfo this + let cfg = CfgInfo(this, getNextBasicBlockGlobalId) Method.ReportCFGLoaded this cfg else internalfailf $"Getting CFG of method {this} without body (extern or abstract)") @@ -445,14 +519,38 @@ and and IGraphTrackableState = abstract member CodeLocation: codeLocation abstract member CallStack: list + abstract member Id: uint + abstract member PathCondition: pathCondition + abstract member VisitedNotCoveredVerticesInZone: uint with get + abstract member VisitedNotCoveredVerticesOutOfZone: uint with get + abstract member VisitedAgainVertices: uint with get + abstract member InstructionsVisitedInCurrentBlock : uint with get, set + abstract member History: Dictionary + abstract member Children: array + abstract member StepWhenMovedLastTime: uint with get module public CodeLocation = let hasSiblings (blockStart : codeLocation) = blockStart.method.CFG.HasSiblings blockStart.offset -type ApplicationGraph() = - +type ApplicationGraphDelta() = + let loadedMethods = ResizeArray() + let touchedBasicBlocks = HashSet() + let touchedStates = HashSet() + let removedStates = HashSet() + member this.LoadedMethods = loadedMethods + member this.TouchedBasicBlocks = touchedBasicBlocks + member this.TouchedStates = touchedStates + member this.RemovedStates = removedStates + member this.Clear() = + loadedMethods.Clear() + touchedBasicBlocks.Clear() + touchedStates.Clear() + removedStates.Clear() + +type ApplicationGraph(getNextBasicBlockGlobalId,applicationGraphDelta:ApplicationGraphDelta) = + let dummyTerminalForCallEdge = 1 let dummyTerminalForReturnEdge = 2 @@ -462,43 +560,90 @@ type ApplicationGraph() = let callFrom = callSource.BasicBlock let callTo = calledMethodCfgInfo.EntryPoint let exists, location = callerMethodCfgInfo.Calls.TryGetValue callSource.BasicBlock + if not <| callTo.IncomingCallEdges.Contains callFrom then let mutable returnTo = callFrom // if not exists then it should be from exception mechanism - if not callTarget.method.IsStaticConstructor && exists then + if (not callTarget.method.IsStaticConstructor) && exists then returnTo <- callerMethodCfgInfo.ResolveBasicBlock location.ReturnTo - let exists, callEdges = callFrom.OutgoingEdges.TryGetValue dummyTerminalForCallEdge - if exists then - let added = callEdges.Add callTo - assert added - else callFrom.OutgoingEdges.Add(dummyTerminalForCallEdge, Seq.singleton callTo |> HashSet) - - for returnFrom in calledMethodCfgInfo.Sinks do - let outgoingEdges = returnFrom.OutgoingEdges - let exists, returnEdges = outgoingEdges.TryGetValue dummyTerminalForReturnEdge - if exists then + + let exists, callEdges = callFrom.OutgoingEdges.TryGetValue dummyTerminalForCallEdge + if exists then + let added = callEdges.Add callTo + assert added + else + callFrom.OutgoingEdges.Add(dummyTerminalForCallEdge, HashSet [|callTo|]) + + for returnFrom in calledMethodCfgInfo.Sinks do + let exists,returnEdges = returnFrom.OutgoingEdges.TryGetValue dummyTerminalForReturnEdge + if exists + then let added = returnEdges.Add returnTo assert added - else outgoingEdges.Add(dummyTerminalForReturnEdge, Seq.singleton returnTo |> HashSet) + else + returnFrom.OutgoingEdges.Add(dummyTerminalForReturnEdge, HashSet [|returnTo|]) let added = returnTo.IncomingCallEdges.Add returnFrom assert added - - // 'returnFrom' may be equal to 'callFrom' - callTo.IncomingCallEdges.Add callFrom |> ignore - - let moveState (initialPosition : codeLocation) (stateWithNewPosition : IGraphTrackableState) = - // Not implemented yet - () - - let addStates (parentState : Option) (states : array) = - // Not implemented yet - () + let added = applicationGraphDelta.TouchedBasicBlocks.Add returnFrom + () + + let added = callTo.IncomingCallEdges.Add callFrom + assert added + else () + + let moveState (initialPosition: codeLocation) (stateWithNewPosition: IGraphTrackableState) = + let added = applicationGraphDelta.TouchedBasicBlocks.Add initialPosition.BasicBlock + let added = applicationGraphDelta.TouchedBasicBlocks.Add stateWithNewPosition.CodeLocation.BasicBlock + let removed = initialPosition.BasicBlock.AssociatedStates.Remove stateWithNewPosition + if removed + then + let added = stateWithNewPosition.CodeLocation.BasicBlock.AssociatedStates.Add stateWithNewPosition + assert added + if stateWithNewPosition.History.ContainsKey stateWithNewPosition.CodeLocation.BasicBlock + then + if initialPosition.BasicBlock <> stateWithNewPosition.CodeLocation.BasicBlock + then + let history = stateWithNewPosition.History[stateWithNewPosition.CodeLocation.BasicBlock] + stateWithNewPosition.History[stateWithNewPosition.CodeLocation.BasicBlock] + <- StateHistoryElem(stateWithNewPosition.CodeLocation.BasicBlock.Id, history.NumOfVisits + 1u, stateWithNewPosition.StepWhenMovedLastTime) + else stateWithNewPosition.InstructionsVisitedInCurrentBlock <- stateWithNewPosition.InstructionsVisitedInCurrentBlock + 1u + else stateWithNewPosition.History.Add(stateWithNewPosition.CodeLocation.BasicBlock, StateHistoryElem(stateWithNewPosition.CodeLocation.BasicBlock.Id, 1u, stateWithNewPosition.StepWhenMovedLastTime)) + stateWithNewPosition.CodeLocation.BasicBlock.VisitedInstructions <- + max + stateWithNewPosition.CodeLocation.BasicBlock.VisitedInstructions + (uint ((stateWithNewPosition.CodeLocation.BasicBlock.GetInstructions() + |> Seq.findIndex (fun instr -> Offset.from (int instr.offset) = stateWithNewPosition.CodeLocation.offset)) + 1)) + stateWithNewPosition.CodeLocation.BasicBlock.IsVisited <- + stateWithNewPosition.CodeLocation.BasicBlock.IsVisited + || stateWithNewPosition.CodeLocation.offset = stateWithNewPosition.CodeLocation.BasicBlock.FinalOffset + + let addStates (parentState:Option) (states:array) = + //Option.iter (applicationGraphDelta.TouchedStates.Add >> ignore) parentState + parentState |> Option.iter (fun v -> applicationGraphDelta.TouchedBasicBlocks.Add v.CodeLocation.BasicBlock |> ignore) + for newState in states do + //let added = applicationGraphDelta.TouchedStates.Add newState + let added = applicationGraphDelta.TouchedBasicBlocks.Add newState.CodeLocation.BasicBlock + let added = newState.CodeLocation.BasicBlock.AssociatedStates.Add newState + if newState.History.ContainsKey newState.CodeLocation.BasicBlock + then + let history = newState.History[newState.CodeLocation.BasicBlock] + newState.History[newState.CodeLocation.BasicBlock] <- StateHistoryElem(newState.CodeLocation.BasicBlock.Id, history.NumOfVisits + 1u, newState.StepWhenMovedLastTime) + else newState.History.Add(newState.CodeLocation.BasicBlock, StateHistoryElem(newState.CodeLocation.BasicBlock.Id, 1u, newState.StepWhenMovedLastTime)) + newState.CodeLocation.BasicBlock.VisitedInstructions <- + max + newState.CodeLocation.BasicBlock.VisitedInstructions + (uint ((newState.CodeLocation.BasicBlock.GetInstructions() + |> Seq.findIndex (fun instr -> Offset.from (int instr.offset) = newState.CodeLocation.offset)) + 1)) + newState.CodeLocation.BasicBlock.IsVisited <- + newState.CodeLocation.BasicBlock.IsVisited + || newState.CodeLocation.offset = newState.CodeLocation.BasicBlock.FinalOffset let getShortestDistancesToGoals (states : array) = __notImplemented__() member this.RegisterMethod (method : Method) = assert method.HasBody + applicationGraphDelta.LoadedMethods.Add method member this.AddCallEdge (sourceLocation : codeLocation) (targetLocation : codeLocation) = addCallEdge sourceLocation targetLocation @@ -540,16 +685,27 @@ type NullVisualizer() = override x.VisualizeStep _ _ _ = () module Application = + let applicationGraphDelta = ApplicationGraphDelta() + let mutable basicBlockGlobalCount = 0u + let getNextBasicBlockGlobalId () = + let r = basicBlockGlobalCount + basicBlockGlobalCount <- basicBlockGlobalCount + 1u + r let private methods = ConcurrentDictionary() let private _loadedMethods = ConcurrentDictionary() let loadedMethods = _loadedMethods :> seq<_> - let graph = ApplicationGraph() - // TODO: if visualizer is not set, decline all 'ApplicationGraph' calls + let mutable graph = ApplicationGraph(getNextBasicBlockGlobalId, applicationGraphDelta) let mutable visualizer : IVisualizer = NullVisualizer() + let reset () = + applicationGraphDelta.Clear() + basicBlockGlobalCount <- 0u + graph <- ApplicationGraph(getNextBasicBlockGlobalId, applicationGraphDelta) + methods.Clear() + _loadedMethods.Clear() let getMethod (m : MethodBase) : Method = let desc = Reflection.getMethodDescriptor m - Dict.getValueOrUpdate methods desc (fun () -> Method(m)) + Dict.getValueOrUpdate methods desc (fun () -> Method(m,getNextBasicBlockGlobalId)) let setCoverageZone (zone : Method -> bool) = Method.CoverageZone <- zone @@ -570,8 +726,12 @@ module Application = graph.AddForkedStates toState forked visualizer.VisualizeStep fromLoc toState forked - let terminateState state = + let terminateState (state: IGraphTrackableState) = // TODO: gsv: propagate this into application graph + let removed = state.CodeLocation.BasicBlock.AssociatedStates.Remove state + let added = applicationGraphDelta.TouchedBasicBlocks.Add state.CodeLocation.BasicBlock + //let added = applicationGraphDelta.TouchedStates.Add state + //let added = applicationGraphDelta.RemovedStates state visualizer.TerminateState state let addCallEdge = graph.AddCallEdge @@ -584,4 +744,4 @@ module Application = Method.ReportCFGLoaded <- fun m -> graph.RegisterMethod m let added = _loadedMethods.TryAdd(m, ()) - assert added + assert added \ No newline at end of file diff --git a/VSharp.IL/CallGraph.fs b/VSharp.IL/CallGraph.fs deleted file mode 100644 index e69de29bb..000000000 diff --git a/VSharp.IL/ILRewriter.fs b/VSharp.IL/ILRewriter.fs index e177d7e34..3acc43ca6 100644 --- a/VSharp.IL/ILRewriter.fs +++ b/VSharp.IL/ILRewriter.fs @@ -817,7 +817,7 @@ module internal ILRewriter = offsetToInstr[codeSize] <- il let mutable branch = false - let mutable offset = 0 + let mutable offset = 0 let codeSize : offset = Offset.from codeSize while offset < codeSize do let startOffset = offset @@ -827,11 +827,11 @@ module internal ILRewriter = let size = match op.OperandType with | OperandType.InlineNone - | OperandType.InlineSwitch -> 0 + | OperandType.InlineSwitch -> 0 | OperandType.ShortInlineVar | OperandType.ShortInlineI - | OperandType.ShortInlineBrTarget -> 1 - | OperandType.InlineVar -> 2 + | OperandType.ShortInlineBrTarget -> 1 + | OperandType.InlineVar -> 2 | OperandType.InlineI | OperandType.InlineMethod | OperandType.InlineType @@ -840,9 +840,9 @@ module internal ILRewriter = | OperandType.InlineTok | OperandType.ShortInlineR | OperandType.InlineField - | OperandType.InlineBrTarget -> 4 + | OperandType.InlineBrTarget -> 4 | OperandType.InlineI8 - | OperandType.InlineR -> 8 + | OperandType.InlineR -> 8 | _ -> __unreachable__() if offset + size > codeSize then invalidProgram "IL stream unexpectedly ended!" diff --git a/VSharp.IL/MethodBody.fs b/VSharp.IL/MethodBody.fs index 692f23fe7..25d0bd1ac 100644 --- a/VSharp.IL/MethodBody.fs +++ b/VSharp.IL/MethodBody.fs @@ -389,10 +389,10 @@ module MethodBody = let private operandType2operandSize = [| - 4; 4; 4; 8; 4 - 0; -1; 8; 4; 4 - 4; 4; 4; 4; 2 - 1; 1; 4; 1 + 4; 4; 4; 8; 4 + 0; -1; 8; 4; 4 + 4; 4; 4; 4; 2 + 1; 1; 4; 1 |] let private jumpTargetsForNext (opCode : OpCode) _ (pos : offset) = @@ -420,9 +420,9 @@ module MethodBody = let private inlineSwitch (opCode : OpCode) ilBytes (pos : offset) = let opcodeSize = Offset.from opCode.Size let n = NumberCreator.extractUnsignedInt32 ilBytes (pos + opcodeSize) |> int - let nextInstruction = pos + opcodeSize + 4 * n + 4 + let nextInstruction = pos + opcodeSize + 4 * n + 4 let nextOffsets = - List.init n (fun x -> nextInstruction + Offset.from (NumberCreator.extractInt32 ilBytes (pos + opcodeSize + 4 * (x + 1)))) + List.init n (fun x -> nextInstruction + Offset.from (NumberCreator.extractInt32 ilBytes (pos + opcodeSize + 4 * (x + 1)))) ConditionalBranch(nextInstruction, nextOffsets) let private jumpTargetsForReturn _ _ _ = Return diff --git a/VSharp.IL/OpCodes.fs b/VSharp.IL/OpCodes.fs index e36b14874..4bfc1fce9 100644 --- a/VSharp.IL/OpCodes.fs +++ b/VSharp.IL/OpCodes.fs @@ -233,9 +233,7 @@ type OpCodeValues = | Refanytype = 0xFE1Ds | Readonly_ = 0xFE1Es -[] -type offsets -type offset = int +type offset = int module Offset = let from (x : int) : offset = LanguagePrimitives.Int32WithMeasure x diff --git a/VSharp.IL/Serializer.fs b/VSharp.IL/Serializer.fs new file mode 100644 index 000000000..9a7857b6e --- /dev/null +++ b/VSharp.IL/Serializer.fs @@ -0,0 +1,595 @@ +module VSharp.IL.Serializer + +open System +open System.Collections.Generic +open System.IO +open System.Reflection +open System.Text.Json +open Microsoft.FSharp.Collections +open VSharp +open VSharp.GraphUtils +open VSharp.ML.GameServer.Messages +open FSharpx.Collections +open type VSharp.Core.termNode +open VSharp.Core + + + +[] +type Statistics = + val CoveredVerticesInZone: uint + val CoveredVerticesOutOfZone: uint + val VisitedVerticesInZone: uint + val VisitedVerticesOutOfZone: uint + val VisitedInstructionsInZone: uint + val TouchedVerticesInZone: uint + val TouchedVerticesOutOfZone: uint + val TotalVisibleVerticesInZone: uint + + new + ( + coveredVerticesInZone, + coveredVerticesOutOfZone, + visitedVerticesInZone, + visitedVerticesOutOfZone, + visitedInstructionsInZone, + touchedVerticesInZone, + touchedVerticesOutOfZone, + totalVisibleVerticesInZone + ) = + { CoveredVerticesInZone = coveredVerticesInZone + CoveredVerticesOutOfZone = coveredVerticesOutOfZone + VisitedVerticesInZone = visitedVerticesInZone + VisitedVerticesOutOfZone = visitedVerticesOutOfZone + VisitedInstructionsInZone = visitedInstructionsInZone + TouchedVerticesInZone = touchedVerticesInZone + TouchedVerticesOutOfZone = touchedVerticesOutOfZone + TotalVisibleVerticesInZone = totalVisibleVerticesInZone } + +[] +type StateMetrics = + val StateId: uint + val NextInstructionIsUncoveredInZone: float + val ChildNumber: uint + val VisitedVerticesInZone: uint + val HistoryLength: uint + val DistanceToNearestUncovered: uint + val DistanceToNearestNotVisited: uint + val DistanceToNearestReturn: uint + + new + ( + stateId, + nextInstructionIsUncoveredInZone, + childNumber, + visitedVerticesInZone, + historyLength, + distanceToNearestUncovered, + distanceToNearestNotVisited, + distanceTuNearestReturn + ) = + { StateId = stateId + NextInstructionIsUncoveredInZone = nextInstructionIsUncoveredInZone + ChildNumber = childNumber + VisitedVerticesInZone = visitedVerticesInZone + HistoryLength = historyLength + DistanceToNearestUncovered = distanceToNearestUncovered + DistanceToNearestNotVisited = distanceToNearestNotVisited + DistanceToNearestReturn = distanceTuNearestReturn } + +[] +type StateInfoToDump = + val StateId: uint + val NextInstructionIsUncoveredInZone: float + val ChildNumberNormalized: float + val VisitedVerticesInZoneNormalized: float + val Productivity: float + val DistanceToReturnNormalized: float + val DistanceToUncoveredNormalized: float + val DistanceToNotVisitedNormalized: float + val ExpectedWeight: float + + new + ( + stateId, + nextInstructionIsUncoveredInZone, + childNumber, + visitedVerticesInZone, + productivity, + distanceToReturn, + distanceToUncovered, + distanceToNotVisited + ) = + { StateId = stateId + NextInstructionIsUncoveredInZone = nextInstructionIsUncoveredInZone + ChildNumberNormalized = childNumber + VisitedVerticesInZoneNormalized = visitedVerticesInZone + Productivity = productivity + DistanceToReturnNormalized = distanceToReturn + DistanceToUncoveredNormalized = distanceToUncovered + DistanceToNotVisitedNormalized = distanceToNotVisited + ExpectedWeight = + nextInstructionIsUncoveredInZone + + childNumber + + visitedVerticesInZone + + distanceToReturn + + distanceToUncovered + + distanceToNotVisited + + productivity } + +let mutable firstFreeEpisodeNumber = 0 + +let calculateStateMetrics interproceduralGraphDistanceFrom (state: IGraphTrackableState) = + let currentBasicBlock = state.CodeLocation.BasicBlock + + let distances = + let assembly = currentBasicBlock.Method.Module.Assembly + + let callGraphDist = + Dict.getValueOrUpdate interproceduralGraphDistanceFrom assembly (fun () -> Dictionary<_, _>()) + + Dict.getValueOrUpdate callGraphDist (currentBasicBlock :> IInterproceduralCfgNode) (fun () -> + let dist = + incrementalSourcedShortestDistanceBfs (currentBasicBlock :> IInterproceduralCfgNode) callGraphDist + + let distFromNode = Dictionary() + + for i in dist do + if i.Value <> infinity then + distFromNode.Add(i.Key, i.Value) + + distFromNode) + + let childCountStore = Dictionary<_, HashSet<_>>() + + let rec childCount (state: IGraphTrackableState) = + if childCountStore.ContainsKey state then + childCountStore[state] + else + let cnt = + Array.fold + (fun (cnt: HashSet<_>) n -> + cnt.UnionWith(childCount n) + cnt) + (HashSet<_>(state.Children)) + state.Children + + childCountStore.Add(state, cnt) + cnt + + let childNumber = uint (childCount state).Count + + let visitedVerticesInZone = + state.History + |> Seq.fold + (fun cnt kvp -> + if kvp.Key.IsGoal && not kvp.Key.IsCovered then + cnt + 1u + else + cnt) + 0u + + let nextInstructionIsUncoveredInZone = + let notTouchedFollowingBlocs, notVisitedFollowingBlocs, notCoveredFollowingBlocs = + let mutable notCoveredBasicBlocksInZone = 0 + let mutable notVisitedBasicBlocksInZone = 0 + let mutable notTouchedBasicBlocksInZone = 0 + let basicBlocks = HashSet<_>() + + currentBasicBlock.OutgoingEdges.Values |> Seq.iter basicBlocks.UnionWith + + basicBlocks + |> Seq.iter (fun basicBlock -> + if basicBlock.IsGoal then + if not basicBlock.IsTouched then + notTouchedBasicBlocksInZone <- notTouchedBasicBlocksInZone + 1 + elif not basicBlock.IsVisited then + notVisitedBasicBlocksInZone <- notVisitedBasicBlocksInZone + 1 + elif not basicBlock.IsCovered then + notCoveredBasicBlocksInZone <- notCoveredBasicBlocksInZone + 1) + + notTouchedBasicBlocksInZone, notVisitedBasicBlocksInZone, notCoveredBasicBlocksInZone + + if + state.CodeLocation.offset <> currentBasicBlock.FinalOffset + && currentBasicBlock.IsGoal + then + if not currentBasicBlock.IsVisited then 1.0 + elif not currentBasicBlock.IsCovered then 0.5 + else 0.0 + elif state.CodeLocation.offset = currentBasicBlock.FinalOffset then + if notTouchedFollowingBlocs > 0 then 1.0 + elif notVisitedFollowingBlocs > 0 then 0.5 + elif notCoveredFollowingBlocs > 0 then 0.3 + else 0.0 + else + 0.0 + + let historyLength = + state.History |> Seq.fold (fun cnt kvp -> cnt + kvp.Value.NumOfVisits) 0u + + let getMinBy cond = + let s = distances |> Seq.filter cond + + if Seq.isEmpty s then + UInt32.MaxValue + else + s |> Seq.minBy (fun x -> x.Value) |> (fun x -> x.Value) + + let distanceToNearestUncovered = + getMinBy (fun kvp -> kvp.Key.IsGoal && not kvp.Key.IsCovered) + + let distanceToNearestNotVisited = + getMinBy (fun kvp -> kvp.Key.IsGoal && not kvp.Key.IsVisited) + + let distanceToNearestReturn = getMinBy (fun kvp -> kvp.Key.IsGoal && kvp.Key.IsSink) + + StateMetrics( + state.Id, + nextInstructionIsUncoveredInZone, + childNumber, + visitedVerticesInZone, + historyLength, + distanceToNearestUncovered, + distanceToNearestNotVisited, + distanceToNearestReturn + ) + +let getFolderToStoreSerializationResult (prefix: string) suffix = + let folderName = Path.Combine(Path.Combine(prefix, "SerializedEpisodes"), suffix) + folderName + +let computeStatistics (gameState: GameState) = + let mutable coveredVerticesInZone = 0u + let mutable coveredVerticesOutOfZone = 0u + let mutable visitedVerticesInZone = 0u + let mutable visitedVerticesOutOfZone = 0u + let mutable visitedInstructionsInZone = 0u + let mutable touchedVerticesInZone = 0u + let mutable touchedVerticesOutOfZone = 0u + let mutable totalVisibleVerticesInZone = 0u + + for v in gameState.GraphVertices do + if v.CoveredByTest && v.InCoverageZone then + coveredVerticesInZone <- coveredVerticesInZone + 1u + + if v.CoveredByTest && not v.InCoverageZone then + coveredVerticesOutOfZone <- coveredVerticesOutOfZone + 1u + + if v.VisitedByState && v.InCoverageZone then + visitedVerticesInZone <- visitedVerticesInZone + 1u + + if v.VisitedByState && not v.InCoverageZone then + visitedVerticesOutOfZone <- visitedVerticesOutOfZone + 1u + + if v.InCoverageZone then + totalVisibleVerticesInZone <- totalVisibleVerticesInZone + 1u + visitedInstructionsInZone <- visitedInstructionsInZone + v.BasicBlockSize + + if v.TouchedByState && v.InCoverageZone then + touchedVerticesInZone <- touchedVerticesInZone + 1u + + if v.TouchedByState && not v.InCoverageZone then + touchedVerticesOutOfZone <- touchedVerticesOutOfZone + 1u + + Statistics( + coveredVerticesInZone, + coveredVerticesOutOfZone, + visitedVerticesInZone, + visitedVerticesOutOfZone, + visitedInstructionsInZone, + touchedVerticesInZone, + touchedVerticesOutOfZone, + totalVisibleVerticesInZone + ) + +let collectStatesInfoToDump (basicBlocks: ResizeArray) = + let statesMetrics = ResizeArray<_>() + + for currentBasicBlock in basicBlocks do + let interproceduralGraphDistanceFrom = + Dictionary>() + + currentBasicBlock.AssociatedStates + |> Seq.iter (fun s -> statesMetrics.Add(calculateStateMetrics interproceduralGraphDistanceFrom s)) + + let statesInfoToDump = + let mutable maxVisitedVertices = UInt32.MinValue + let mutable maxChildNumber = UInt32.MinValue + let mutable minDistToUncovered = UInt32.MaxValue + let mutable minDistToNotVisited = UInt32.MaxValue + let mutable minDistToReturn = UInt32.MaxValue + + statesMetrics + |> ResizeArray.iter (fun s -> + if s.VisitedVerticesInZone > maxVisitedVertices then + maxVisitedVertices <- s.VisitedVerticesInZone + + if s.ChildNumber > maxChildNumber then + maxChildNumber <- s.ChildNumber + + if s.DistanceToNearestUncovered < minDistToUncovered then + minDistToUncovered <- s.DistanceToNearestUncovered + + if s.DistanceToNearestNotVisited < minDistToNotVisited then + minDistToNotVisited <- s.DistanceToNearestNotVisited + + if s.DistanceToNearestReturn < minDistToReturn then + minDistToReturn <- s.DistanceToNearestReturn) + + let normalize minV v (sm: StateMetrics) = + if + v = minV + || (v = UInt32.MaxValue && sm.DistanceToNearestReturn = UInt32.MaxValue) + then + 1.0 + elif v = UInt32.MaxValue then + 0.0 + else + float (1u + minV) / float (1u + v) + + statesMetrics + |> ResizeArray.map (fun m -> + StateInfoToDump( + m.StateId, + m.NextInstructionIsUncoveredInZone, + (if maxChildNumber = 0u then + 0.0 + else + float m.ChildNumber / float maxChildNumber), + (if maxVisitedVertices = 0u then + 0.0 + else + float m.VisitedVerticesInZone / float maxVisitedVertices), + float m.VisitedVerticesInZone / float m.HistoryLength, + normalize minDistToReturn m.DistanceToNearestReturn m, + normalize minDistToUncovered m.DistanceToNearestUncovered m, + normalize minDistToUncovered m.DistanceToNearestNotVisited m + )) + + statesInfoToDump + +let getFirstFreePathConditionVertexId, resetPathConditionVertexIdCounter = + let mutable count = 0u + + fun () -> + let res = count + count <- count + 1u + res + , fun () -> count <- 0u + +let pathConditionVertices = HashSet() +let termsWithId = Dictionary>() + +let collectPathCondition + term + (termsWithId: Dictionary>) + (processedPathConditionVertices: HashSet) + = // TODO: Support other operations + let termsToVisit = Stack [| term |] + let pathConditionDelta = ResizeArray() + + let getIdForTerm term = + if termsWithId.ContainsKey term then + termsWithId.[term] + else + let newId = getFirstFreePathConditionVertexId () + termsWithId.Add(term, newId) + newId + + let handleChild term (children: ResizeArray<_>) = + children.Add(getIdForTerm term) + termsToVisit.Push term + + while termsToVisit.Count > 0 do + let currentTerm = termsToVisit.Pop() + + let markAsVisited (vertexType: pathConditionVertexType) children = + let newVertex = PathConditionVertex(getIdForTerm currentTerm, vertexType, children) + processedPathConditionVertices.Add currentTerm |> ignore + pathConditionDelta.Add newVertex + + if not <| processedPathConditionVertices.Contains currentTerm then + match currentTerm.term with + | Nop -> markAsVisited pathConditionVertexType.Nop [||] + | Concrete(_, _) -> markAsVisited pathConditionVertexType.Constant [||] + | Constant(_, _, _) -> markAsVisited pathConditionVertexType.Constant [||] + | Expression(operation, termList, _) -> + let children = ResizeArray>() + + for t in termList do + handleChild t children + + let children = children.ToArray() + + match operation with + | Operator operator -> + match operator with + | OperationType.UnaryMinus -> pathConditionVertexType.UnaryMinus + | OperationType.BitwiseNot -> pathConditionVertexType.BitwiseNot + | OperationType.BitwiseAnd -> pathConditionVertexType.BitwiseAnd + | OperationType.BitwiseOr -> pathConditionVertexType.BitwiseOr + | OperationType.BitwiseXor -> pathConditionVertexType.BitwiseXor + | OperationType.LogicalNot -> pathConditionVertexType.LogicalNot + | OperationType.LogicalAnd -> pathConditionVertexType.LogicalAnd + | OperationType.LogicalOr -> pathConditionVertexType.LogicalOr + | OperationType.LogicalXor -> pathConditionVertexType.LogicalXor + | OperationType.Equal -> pathConditionVertexType.Equal + | OperationType.NotEqual -> pathConditionVertexType.NotEqual + | OperationType.Greater -> pathConditionVertexType.Greater + | OperationType.Greater_Un -> pathConditionVertexType.Greater_Un + | OperationType.Less -> pathConditionVertexType.Less + | OperationType.Less_Un -> pathConditionVertexType.Less_Un + | OperationType.GreaterOrEqual -> pathConditionVertexType.GreaterOrEqual + | OperationType.GreaterOrEqual_Un -> pathConditionVertexType.GreaterOrEqual_Un + | OperationType.LessOrEqual -> pathConditionVertexType.LessOrEqual + | OperationType.LessOrEqual_Un -> pathConditionVertexType.LessOrEqual_Un + | OperationType.Add -> pathConditionVertexType.Add + | OperationType.AddNoOvf -> pathConditionVertexType.AddNoOvf + | OperationType.AddNoOvf_Un -> pathConditionVertexType.AddNoOvf_Un + | OperationType.Subtract -> pathConditionVertexType.Subtract + | OperationType.SubNoOvf -> pathConditionVertexType.SubNoOvf + | OperationType.SubNoOvf_Un -> pathConditionVertexType.SubNoOvf_Un + | OperationType.Divide -> pathConditionVertexType.Divide + | OperationType.Divide_Un -> pathConditionVertexType.Divide_Un + | OperationType.Multiply -> pathConditionVertexType.Multiply + | OperationType.MultiplyNoOvf -> pathConditionVertexType.MultiplyNoOvf + | OperationType.MultiplyNoOvf_Un -> pathConditionVertexType.MultiplyNoOvf_Un + | OperationType.Remainder -> pathConditionVertexType.Remainder + | OperationType.Remainder_Un -> pathConditionVertexType.Remainder_Un + | OperationType.ShiftLeft -> pathConditionVertexType.ShiftLeft + | OperationType.ShiftRight -> pathConditionVertexType.ShiftRight + | OperationType.ShiftRight_Un -> pathConditionVertexType.ShiftRight_Un + | unexpectedOperation -> failwith $"Add {unexpectedOperation} support." + |> fun vertexType -> markAsVisited vertexType children + + | Application(_) -> markAsVisited pathConditionVertexType.StandardFunctionApplication children + | Cast(_, _) -> markAsVisited pathConditionVertexType.Cast children + | Combine -> markAsVisited pathConditionVertexType.Combine children + | Struct(fields, _) -> + let children = ResizeArray>() + + for _, t in PersistentDict.toSeq fields do + handleChild t children + + markAsVisited pathConditionVertexType.Struct (children.ToArray()) + | HeapRef(_, _) -> markAsVisited pathConditionVertexType.HeapRef [||] + | Ref(_) -> markAsVisited pathConditionVertexType.Ref [||] + | Ptr(_, _, t) -> + let children = ResizeArray> [||] + handleChild t children + markAsVisited pathConditionVertexType.Ptr (children.ToArray()) + | Slice(t, listOfTuples) -> + let children = ResizeArray> [||] + handleChild t children + + for t1, t2, t3, _ in listOfTuples do + handleChild t1 children + handleChild t2 children + handleChild t3 children + + markAsVisited pathConditionVertexType.Slice (children.ToArray()) + | Ite(_) -> markAsVisited pathConditionVertexType.Ite [||] + + pathConditionDelta + +let collectGameState (basicBlocks: ResizeArray) filterStates processedPathConditionVertices termsWithId = + + let vertices = ResizeArray<_>() + let allStates = HashSet<_>() + + let activeStates = + basicBlocks + |> Seq.collect (fun basicBlock -> basicBlock.AssociatedStates) + |> Seq.map (fun s -> s.Id) + |> fun x -> HashSet x + + let pathConditionDelta = ResizeArray() + + for currentBasicBlock in basicBlocks do + let states = + currentBasicBlock.AssociatedStates + |> Seq.map (fun (s: IGraphTrackableState) -> + let pathCondition = s.PathCondition |> PC.toSeq + + for term in pathCondition do + pathConditionDelta.AddRange(collectPathCondition term termsWithId processedPathConditionVertices) + + let pathCondition = [| for p in pathCondition -> termsWithId.[p] |] + + State( + s.Id, + (uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1) + * 1u, + pathCondition, + s.VisitedAgainVertices, + s.VisitedNotCoveredVerticesInZone, + s.VisitedNotCoveredVerticesOutOfZone, + s.StepWhenMovedLastTime, + s.InstructionsVisitedInCurrentBlock, + s.History |> Seq.map (fun kvp -> kvp.Value) |> Array.ofSeq, + s.Children + |> Array.map (fun s -> s.Id) + |> (fun x -> + if filterStates then + Array.filter activeStates.Contains x + else + x) + ) + |> allStates.Add + |> ignore + + s.Id) + |> Array.ofSeq + + + GameMapVertex( + currentBasicBlock.Id, + currentBasicBlock.IsGoal, + uint + <| currentBasicBlock.FinalOffset - currentBasicBlock.StartOffset + 1, + currentBasicBlock.IsCovered, + currentBasicBlock.IsVisited, + currentBasicBlock.IsTouched, + currentBasicBlock.ContainsCall, + currentBasicBlock.ContainsThrow, + states + ) + |> vertices.Add + + let edges = ResizeArray<_>() + + for basicBlock in basicBlocks do + for outgoingEdges in basicBlock.OutgoingEdges do + for targetBasicBlock in outgoingEdges.Value do + GameMapEdge(basicBlock.Id, targetBasicBlock.Id, GameEdgeLabel(int outgoingEdges.Key)) + |> edges.Add + + GameState(vertices.ToArray(), allStates |> Array.ofSeq, pathConditionDelta.ToArray(), edges.ToArray()) + +let collectGameStateDelta () = + let basicBlocks = HashSet<_>(Application.applicationGraphDelta.TouchedBasicBlocks) + + for method in Application.applicationGraphDelta.LoadedMethods do + for basicBlock in method.BasicBlocks do + basicBlock.IsGoal <- method.InCoverageZone + let added = basicBlocks.Add(basicBlock) + () + + collectGameState (ResizeArray basicBlocks) false pathConditionVertices termsWithId + +let dumpGameState fileForResultWithoutExtension (movedStateId: uint) = + let basicBlocks = ResizeArray<_>() + + for method in Application.loadedMethods do + for basicBlock in method.Key.BasicBlocks do + basicBlock.IsGoal <- method.Key.InCoverageZone + basicBlocks.Add(basicBlock) + + let gameState = + collectGameState basicBlocks true (HashSet()) (Dictionary>()) + + let statesInfoToDump = collectStatesInfoToDump basicBlocks + let gameStateJson = JsonSerializer.Serialize gameState + let statesInfoJson = JsonSerializer.Serialize statesInfoToDump + File.WriteAllText(fileForResultWithoutExtension + "_gameState", gameStateJson) + File.WriteAllText(fileForResultWithoutExtension + "_statesInfo", statesInfoJson) + File.WriteAllText(fileForResultWithoutExtension + "_movedState", string movedStateId) + +let computeReward (statisticsBeforeStep: Statistics) (statisticsAfterStep: Statistics) = + let rewardForCoverage = + (statisticsAfterStep.CoveredVerticesInZone + - statisticsBeforeStep.CoveredVerticesInZone) + * 1u + + let rewardForVisitedInstructions = + (statisticsAfterStep.VisitedInstructionsInZone + - statisticsBeforeStep.VisitedInstructionsInZone) + * 1u + + let maxPossibleReward = + (statisticsBeforeStep.TotalVisibleVerticesInZone + - statisticsBeforeStep.CoveredVerticesInZone) + * 1u + + Reward(rewardForCoverage, rewardForVisitedInstructions, maxPossibleReward) diff --git a/VSharp.IL/VSharp.IL.fsproj b/VSharp.IL/VSharp.IL.fsproj index 1648a2174..42c6329d1 100644 --- a/VSharp.IL/VSharp.IL.fsproj +++ b/VSharp.IL/VSharp.IL.fsproj @@ -1,7 +1,7 @@ - + - net7.0 + net8.0 true Debug;Release;DebugTailRec AnyCPU @@ -20,15 +20,18 @@ + + - + + diff --git a/VSharp.InternalCalls/VSharp.InternalCalls.fsproj b/VSharp.InternalCalls/VSharp.InternalCalls.fsproj index 6f91b03b4..706b68b13 100644 --- a/VSharp.InternalCalls/VSharp.InternalCalls.fsproj +++ b/VSharp.InternalCalls/VSharp.InternalCalls.fsproj @@ -1,7 +1,7 @@  - net7.0 + net8.0 Debug;Release;DebugTailRec AnyCPU @@ -84,7 +84,7 @@ - + diff --git a/VSharp.ML.GameServer.Runner/Main.fs b/VSharp.ML.GameServer.Runner/Main.fs new file mode 100644 index 000000000..9f409b36f --- /dev/null +++ b/VSharp.ML.GameServer.Runner/Main.fs @@ -0,0 +1,468 @@ +open System +open System.IO +open System.Text.Json +open System.Net.Sockets +open System.Reflection +open Argu +open Microsoft.FSharp.Core +open Suave +open Suave.Operators +open Suave.Filters +open Suave.Logging +open Suave.Sockets +open Suave.Sockets.Control +open Suave.WebSocket +open VSharp +open VSharp.Core +open VSharp.Explorer +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 + TestsCount = testsCount + ErrorsCount = errorsCount + StepsCount = stepsCount } + +type Mode = + | Server = 0 + | Generator = 1 + | SendModel = 2 + +let TIMEOUT_FOR_TRAINING = 15 * 60 +let SOLVER_TIMEOUT_FOR_TRAINING = 2 + +type CliArguments = + | [] Port of int + | [] DatasetBasePath of string + | [] DatasetDescription of string + | [] 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 of bool + | [] Optimize of bool + + interface IArgParserTemplate with + member s.Usage = + match s with + | Port _ -> "Port to communicate with game client." + | DatasetBasePath _ -> + "Full path to dataset root directory. Dll location is /" + | DatasetDescription _ -> "Full paths to JSON-file with dataset description." + | Mode _ -> + "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 required to play (after `StepsToStart` steps)""" + | DefaultSearcher _ -> """Defines the default searcher algorithm (BFS | DFS)""" + | StepsToStart _ -> """Steps required to start the game""" + | AssemblyFullName _ -> """Path to the DLL that contains the game map implementation""" + | NameOfObjectToCover _ -> """The name of the object that needs to be covered""" + | MapName _ -> """The name of the map used in the game""" + | 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." + +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 + uint actualCoverage * 1u + with e -> + printfn $"Coverage checking problem:{e.Message} \n {e.StackTrace}" + 0u + + ExplorationResult( + actualCoverage, + statistics.TestsCount * 1u, + statistics.ErrorsCount * 1u, + statistics.StepsCount * 1u + ) + +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) = + let mutable loop = true + + socket { + + let sendResponse (message: OutgoingMessage) = + let byteResponse = + serializeOutgoingMessage message + |> System.Text.Encoding.UTF8.GetBytes + |> ByteSegment + + webSocket.send Text byteResponse true + + let oracle = + let feedback = + fun (feedback: Feedback) -> + let res = + socket { + let message = + match feedback with + | 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") + gameState.ToDot file drawHistory + cnt <- cnt + 1u + //toDot false + let res = + 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}" + + Oracle(predict, feedback) + + 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 stepsToStart = gameMap.StepsToStart + let stepsToPlay = gameMap.StepsToPlay + + 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 = stepsToStart + stepsToPlay = stepsToPlay + oracle = Some oracle } + + let aiOptions: AIOptions = + (Training(SendEachStep { aiAgentTrainingOptions = aiTrainingOptions })) + + let options = + VSharpOptions( + timeout = TIMEOUT_FOR_TRAINING, + outputDirectory = outputDirectory, + searchStrategy = SearchStrategy.AI, + aiOptions = aiOptions, + stepsLimit = uint (stepsToPlay + stepsToStart), + solverTimeout = SOLVER_TIMEOUT_FOR_TRAINING + ) + + let explorationResult = explore gameMap options + + Application.reset () + API.Reset() + HashMap.hashMap.Clear() + Serializer.pathConditionVertices.Clear() + Serializer.resetPathConditionVertexIdCounter () + Serializer.termsWithId.Clear() + + do! + sendResponse ( + GameOver( + explorationResult.ActualCoverage, + explorationResult.TestsCount, + explorationResult.StepsCount, + explorationResult.ErrorsCount + ) + ) + + printfn $"Finish map {gameMap.MapName}, port {port}" + | x -> failwithf $"Unexpected message: %A{x}" + + | (Close, _, _) -> + let emptyResponse = [||] |> ByteSegment + do! webSocket.send Close emptyResponse true + loop <- false + | _ -> () + } + +let app port outputDirectory : WebPart = + choose [ path "/gameServer" >=> handShake (ws port outputDirectory) ] + +let serializeExplorationResult (explorationResult: ExplorationResult) = + $"{explorationResult.ActualCoverage} {explorationResult.TestsCount} {explorationResult.StepsCount} {explorationResult.ErrorsCount}" + +let generateDataForPretraining outputDirectory datasetBasePath (maps: ResizeArray) stepsToSerialize = + for map in maps do + if map.StepsToStart = 0u then + printfn $"Generation for {map.MapName} started." + + let map = + GameMap( + map.StepsToPlay, + map.StepsToStart, + Path.Combine(datasetBasePath, map.AssemblyFullName), + map.DefaultSearcher, + map.NameOfObjectToCover, + map.MapName + ) + + let aiBaseOptions = + { defaultSearchStrategy = BFSMode + mapName = map.MapName } + + let options = + VSharpOptions( + timeout = 5 * 60, + outputDirectory = outputDirectory, + searchStrategy = SearchStrategy.ExecutionTreeContributedCoverage, + stepsLimit = stepsToSerialize, + solverTimeout = 2, + aiOptions = DatasetGenerator aiBaseOptions + ) + + 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"), serializeExplorationResult explorationResult) + + 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 stepsToStart = gameMap.StepsToStart + let stepsToPlay = gameMap.StepsToPlay + + 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 = stepsToStart + stepsToPlay = stepsToPlay + oracle = None } + + let steps = ResizeArray() + let stepSaver (aiGameStep: AIGameStep) = steps.Add aiGameStep + + let aiOptions: AIOptions = + Training( + SendModel + { aiAgentTrainingOptions = aiTrainingOptions + outputDirectory = outputDirectory + stepSaver = stepSaver } + ) + + let options = + VSharpOptions( + timeout = TIMEOUT_FOR_TRAINING, + outputDirectory = outputDirectory, + searchStrategy = SearchStrategy.AI, + solverTimeout = SOLVER_TIMEOUT_FOR_TRAINING, + stepsLimit = uint (stepsToPlay + stepsToStart), + aiOptions = aiOptions, + pathToModel = pathToModel, + useGPU = useGPU, + optimize = optimize + ) + + let explorationResult = explore gameMap options + + File.WriteAllText( + Path.Join(outputDirectory, gameMap.MapName + "result"), + serializeExplorationResult explorationResult + ) + + printfn + $"Running for {gameMap.MapName} finished with coverage {explorationResult.ActualCoverage}, tests {explorationResult.TestsCount}, steps {explorationResult.StepsCount},errors {explorationResult.ErrorsCount}." + + let stream = + let host = "localhost" // TODO: working within a local network + let client = new TcpClient() + client.Connect(host, port) + client.SendBufferSize <- 4096 + client.GetStream() + + let needToSendSteps = + let buffer = Array.zeroCreate 1 + let bytesRead = stream.Read(buffer, 0, 1) + + if bytesRead = 0 then + failwith "Connection is closed?!" + + stream.Close() + buffer.[0] <> byte 0 + + if needToSendSteps then + File.WriteAllText(Path.Join(outputDirectory, gameMap.MapName + "_steps"), JsonSerializer.Serialize steps) + +[] +let main args = + let parser = + ArgumentParser.Create(programName = "VSharp.ML.GameServer.Runner.exe") + + let args = parser.Parse args + let mode = args.GetResult <@ Mode @> + + let port = args.GetResult(Port, defaultValue = 8100) + + let outputDirectory = + args.GetResult(OutFolder, defaultValue = Path.Combine(Directory.GetCurrentDirectory(), string port)) + + let cleanOutputDirectory () = + if Directory.Exists outputDirectory then + Directory.Delete(outputDirectory, true) + + Directory.CreateDirectory outputDirectory + + printfn $"outputDir: {outputDirectory}" + + match mode with + | Mode.Server -> + let _ = cleanOutputDirectory () + + try + startWebServer + { defaultConfig with + logger = Targets.create Verbose [||] + bindings = [ HttpBinding.createSimple HTTP "127.0.0.1" port ] } + (app port outputDirectory) + with e -> + printfn $"Failed on port {port}" + printfn $"{e.Message}" + | Mode.SendModel -> + let model = args.GetResult(Model, defaultValue = "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.GetResult(UseGPU, defaultValue = false) + let optimize = args.GetResult(Optimize, defaultValue = false) + + runTrainingSendModelMode outputDirectory gameMap model useGPU optimize port + | Mode.Generator -> + let datasetDescription = args.GetResult <@ DatasetDescription @> + let datasetBasePath = args.GetResult <@ DatasetBasePath @> + let stepsToSerialize = args.GetResult(StepsToSerialize, defaultValue = 500u) + + + let _ = cleanOutputDirectory () + let maps = loadGameMaps datasetDescription + generateDataForPretraining outputDirectory datasetBasePath maps stepsToSerialize + | x -> failwithf $"Unexpected mode {x}." + + 0 diff --git a/VSharp.ML.GameServer.Runner/VSharp.ML.GameServer.Runner.fsproj b/VSharp.ML.GameServer.Runner/VSharp.ML.GameServer.Runner.fsproj new file mode 100644 index 000000000..3930f5611 --- /dev/null +++ b/VSharp.ML.GameServer.Runner/VSharp.ML.GameServer.Runner.fsproj @@ -0,0 +1,29 @@ + + + + Exe + net8.0 + VSharp.ML.GameServer + + + + + + + + + + + + + + + + + + + + + + + diff --git a/VSharp.ML.GameServer/Messages.fs b/VSharp.ML.GameServer/Messages.fs new file mode 100644 index 000000000..d85a49f0c --- /dev/null +++ b/VSharp.ML.GameServer/Messages.fs @@ -0,0 +1,408 @@ +module VSharp.ML.GameServer.Messages + +open System.Text +open System.Text.Json +open System.Text.Json.Serialization +open VSharp + +type searcher = + | BFS = 0 + | DFS = 1 + +[] +type RawInputMessage = + val MessageType: string + val MessageBody: string + + [] + new(messageType, messageBody) = + { MessageBody = messageBody + MessageType = messageType } + +type IRawOutgoingMessageBody = interface end + +[] +type pathConditionVertexId + +type pathConditionVertexType = + | UnaryMinus = 0 + | BitwiseNot = 1 + | BitwiseAnd = 2 + | BitwiseOr = 3 + | BitwiseXor = 4 + | LogicalNot = 5 + | LogicalAnd = 6 + | LogicalOr = 7 + | LogicalXor = 8 + | Equal = 9 + | NotEqual = 10 + | Greater = 11 + | Greater_Un = 12 + | Less = 13 + | Less_Un = 14 + | GreaterOrEqual = 15 + | GreaterOrEqual_Un = 16 + | LessOrEqual = 17 + | LessOrEqual_Un = 18 + | Add = 19 + | AddNoOvf = 20 + | AddNoOvf_Un = 21 + | Subtract = 22 + | SubNoOvf = 23 + | SubNoOvf_Un = 24 + | Divide = 25 + | Divide_Un = 26 + | Multiply = 27 + | MultiplyNoOvf = 28 + | MultiplyNoOvf_Un = 29 + | Remainder = 30 + | Remainder_Un = 31 + | ShiftLeft = 32 + | ShiftRight = 33 + | ShiftRight_Un = 34 + | Nop = 35 + | Concrete = 36 + | Constant = 37 + | Struct = 39 + | HeapRef = 40 + | Ref = 41 + | Ptr = 42 + | Slice = 43 + | Ite = 44 + | StandardFunctionApplication = 45 + | Cast = 46 + | Combine = 47 + + +[] +type PathConditionVertex = + val Id: uint + val Type: pathConditionVertexType + val Children: array> + + new(id, pathConditionVertexType, children) = + { Id = id + Type = pathConditionVertexType + Children = children } + +[] +type test + +[] +type error + +[] +type step + +[] +type percent + +[] +type basicBlockGlobalId + +[] +type instruction + +[] +type GameOverMessageBody = + interface IRawOutgoingMessageBody + val ActualCoverage: uint + val TestsCount: uint32 + val StepsCount: uint32 + val ErrorsCount: uint32 + + new(actualCoverage, testsCount, stepsCount, errorsCount) = + { ActualCoverage = actualCoverage + TestsCount = testsCount + StepsCount = stepsCount + ErrorsCount = errorsCount } + +[] +type RawOutgoingMessage = + val MessageType: string + val MessageBody: obj + + new(messageType, messageBody) = + { MessageBody = messageBody + MessageType = messageType } + +[] +type stateId + +[] +type GameStep = + val StateId: uint + + [] + new(stateId) = { StateId = stateId } + + +[] +type StateHistoryElem = + val GraphVertexId: uint + val NumOfVisits: uint + val StepWhenVisitedLastTime: uint + + new(graphVertexId, numOfVisits, stepWhenVisitedLastTime) = + { GraphVertexId = graphVertexId + NumOfVisits = numOfVisits + StepWhenVisitedLastTime = stepWhenVisitedLastTime } + +[] +type State = + val Id: uint + val Position: uint // to basic block id + val PathCondition: array> + val VisitedAgainVertices: uint + val VisitedNotCoveredVerticesInZone: uint + val VisitedNotCoveredVerticesOutOfZone: uint + val StepWhenMovedLastTime: uint + val InstructionsVisitedInCurrentBlock: uint + val History: array + val Children: array> + + new + ( + id, + position, + pathCondition, + visitedAgainVertices, + visitedNotCoveredVerticesInZone, + visitedNotCoveredVerticesOutOfZone, + stepWhenMovedLastTime, + instructionsVisitedInCurrentBlock, + history, + children + ) = + { Id = id + Position = position + PathCondition = pathCondition + VisitedAgainVertices = visitedAgainVertices + VisitedNotCoveredVerticesInZone = visitedNotCoveredVerticesInZone + VisitedNotCoveredVerticesOutOfZone = visitedNotCoveredVerticesOutOfZone + StepWhenMovedLastTime = stepWhenMovedLastTime + InstructionsVisitedInCurrentBlock = instructionsVisitedInCurrentBlock + History = history + Children = children } + +[] +type GameMapVertex = + val Id: uint + val InCoverageZone: bool + val BasicBlockSize: uint // instructions + val CoveredByTest: bool + val VisitedByState: bool + val TouchedByState: bool + val ContainsCall: bool + val ContainsThrow: bool + val States: uint[] + + new + ( + id, + inCoverageZone, + basicBlockSize, + containsCall, + containsThrow, + coveredByTest, + visitedByState, + touchedByState, + states + ) = + { Id = id + InCoverageZone = inCoverageZone + BasicBlockSize = basicBlockSize + CoveredByTest = coveredByTest + VisitedByState = visitedByState + TouchedByState = touchedByState + ContainsCall = containsCall + ContainsThrow = containsThrow + States = states } + +[] +type GameEdgeLabel = + val Token: int + new(token) = { Token = token } + +[] +type GameMapEdge = + val VertexFrom: uint + val VertexTo: uint + val Label: GameEdgeLabel + + new(vFrom, vTo, label) = + { VertexFrom = vFrom + VertexTo = vTo + Label = label } + +[] +type GameState = + interface IRawOutgoingMessageBody + val GraphVertices: GameMapVertex[] + val States: State[] + val PathConditionVertices: PathConditionVertex[] + val Map: GameMapEdge[] + + new(graphVertices, states, pathConditionVertices, map) = + { GraphVertices = graphVertices + States = states + PathConditionVertices = pathConditionVertices + Map = map } + + member this.ToDot file drawHistoryEdges = + let vertices = ResizeArray<_>() + let edges = ResizeArray<_>() + + for v in this.GraphVertices do + let color = + if v.CoveredByTest then "green" + elif v.VisitedByState then "red" + elif v.TouchedByState then "yellow" + else "white" + + vertices.Add($"{v.Id} [label={v.Id}, shape=box, style=filled, fillcolor={color}]") + + for s in v.States do + edges.Add($"99{s}00 -> {v.Id} [label=L]") + + for s in this.States do + vertices.Add($"99{s.Id}00 [label={s.Id}, shape=circle]") + + for v in s.Children do + edges.Add($"99{s.Id}00 -> 99{v}00 [label=ch]") + + if drawHistoryEdges then + for v in s.History do + edges.Add($"99{s.Id}00 -> {v.GraphVertexId} [label={v.NumOfVisits}]") + + for e in this.Map do + edges.Add($"{e.VertexFrom}->{e.VertexTo}[label={e.Label.Token}]") + + let dot = + seq { + "digraph g{" + yield! vertices + yield! edges + "}" + } + + System.IO.File.WriteAllLines(file, dot) + +[] +type coverageReward + +[] +type visitedInstructionsReward + +[] +type maxPossibleReward + +[] +type MoveReward = + val ForCoverage: uint + val ForVisitedInstructions: uint + + new(forCoverage, forVisitedInstructions) = + { ForCoverage = forCoverage + ForVisitedInstructions = forVisitedInstructions } + +[] +type Reward = + interface IRawOutgoingMessageBody + val ForMove: MoveReward + val MaxPossibleReward: uint + + new(forMove, maxPossibleReward) = + { ForMove = forMove + MaxPossibleReward = maxPossibleReward } + + new(forCoverage, forVisitedInstructions, maxPossibleReward) = + { ForMove = MoveReward(forCoverage, forVisitedInstructions) + MaxPossibleReward = maxPossibleReward } + +type Feedback = + | MoveReward of Reward + | IncorrectPredictedStateId of uint + | ServerError of string + +[] +type GameMap = + val StepsToPlay: uint + val StepsToStart: uint + + [)>] + val DefaultSearcher: searcher + + val AssemblyFullName: string + val NameOfObjectToCover: string + val MapName: string + + new(stepsToPlay, stepsToStart, assembly, defaultSearcher, objectToCover) = + { StepsToPlay = stepsToPlay + StepsToStart = stepsToStart + AssemblyFullName = assembly + NameOfObjectToCover = objectToCover + DefaultSearcher = defaultSearcher + MapName = $"{objectToCover}_{defaultSearcher}_{stepsToStart}" } + + [] + new(stepsToPlay, stepsToStart, assemblyFullName, defaultSearcher, nameOfObjectToCover, mapName) = + { StepsToPlay = stepsToPlay + StepsToStart = stepsToStart + AssemblyFullName = assemblyFullName + DefaultSearcher = defaultSearcher + NameOfObjectToCover = nameOfObjectToCover + MapName = mapName } + +type InputMessage = + | ServerStop + | Start of GameMap + | Step of GameStep + +[] +type ServerErrorMessageBody = + interface IRawOutgoingMessageBody + val ErrorMessage: string + new(errorMessage) = { ErrorMessage = errorMessage } + +[] +type IncorrectPredictedStateIdMessageBody = + interface IRawOutgoingMessageBody + val StateId: uint + new(stateId) = { StateId = stateId } + +type OutgoingMessage = + | GameOver of uint * uint32 * uint32 * uint32 + | MoveReward of Reward + | IncorrectPredictedStateId of uint + | ReadyForNextStep of GameState + | ServerError of string + +let (|MsgTypeStart|MsgTypeStep|MsgStop|) (str: string) = + let normalized = str.ToLowerInvariant().Trim() + + if normalized = "start" then MsgTypeStart + elif normalized = "step" then MsgTypeStep + elif normalized = "stop" then MsgStop + else failwithf $"Unexpected message type %s{str}" + +let deserializeInputMessage (messageData: byte[]) = + let rawInputMessage = + let str = Encoding.UTF8.GetString messageData + str |> JsonSerializer.Deserialize + + match rawInputMessage.MessageType with + | MsgStop -> ServerStop + | MsgTypeStart -> Start(JsonSerializer.Deserialize rawInputMessage.MessageBody) + | MsgTypeStep -> Step(JsonSerializer.Deserialize(rawInputMessage.MessageBody)) + +let serializeOutgoingMessage (message: OutgoingMessage) = + match message with + | GameOver(actualCoverage, testsCount, stepsCount, errorsCount) -> + RawOutgoingMessage("GameOver", box (GameOverMessageBody(actualCoverage, testsCount, stepsCount, errorsCount))) + | MoveReward reward -> RawOutgoingMessage("MoveReward", reward) + | IncorrectPredictedStateId stateId -> + RawOutgoingMessage("IncorrectPredictedStateId", IncorrectPredictedStateIdMessageBody stateId) + | ReadyForNextStep state -> RawOutgoingMessage("ReadyForNextStep", state) + | ServerError errorMessage -> RawOutgoingMessage("ServerError", ServerErrorMessageBody errorMessage) + |> JsonSerializer.Serialize diff --git a/VSharp.ML.GameServer/VSharp.ML.GameServer.fsproj b/VSharp.ML.GameServer/VSharp.ML.GameServer.fsproj new file mode 100644 index 000000000..be51761c3 --- /dev/null +++ b/VSharp.ML.GameServer/VSharp.ML.GameServer.fsproj @@ -0,0 +1,19 @@ + + + + net8.0 + + + + + + + + + + + + + + + diff --git a/VSharp.Runner/RunnerProgram.cs b/VSharp.Runner/RunnerProgram.cs index f41e3515b..096c04d18 100644 --- a/VSharp.Runner/RunnerProgram.cs +++ b/VSharp.Runner/RunnerProgram.cs @@ -14,7 +14,7 @@ namespace VSharp.Runner public static class RunnerProgram { - private static Assembly? TryLoadAssembly(FileInfo assemblyPath) + public static Assembly? TryLoadAssembly(FileInfo assemblyPath) { try { @@ -28,6 +28,93 @@ public static class RunnerProgram } } + public static Type? ResolveType(Assembly assembly, string? classArgumentValue) + { + if (classArgumentValue == null) + { + Console.Error.WriteLine("Specified class can not be null"); + return null; + } + + var specificClass = + assembly.GetType(classArgumentValue) ?? + assembly.GetTypes() + .Where(t => (t.FullName ?? t.Name).Contains(classArgumentValue)) + .MinBy(t => t.FullName?.Length ?? t.Name.Length); + if (specificClass == null) + { + Console.Error.WriteLine("I did not found type you specified {0} in assembly {1}", classArgumentValue, + assembly.Location); + return null; + } + + return specificClass; + } + + public static MethodBase? ResolveMethod(Assembly assembly, string? methodArgumentValue) + { + if (methodArgumentValue == null) + { + Console.Error.WriteLine("Specified method can not be null"); + return null; + } + + MethodBase? method = null; + if (Int32.TryParse(methodArgumentValue, out var metadataToken)) + { + foreach (var module in assembly.GetModules()) + { + try + { + method = module.ResolveMethod(metadataToken); + if (method != null) break; + } + catch + { + // ignored + } + } + + if (method == null) + { + Console.Error.WriteLine("I did not found method you specified by token {0} in assembly {1}", + metadataToken, assembly.Location); + return null; + } + } + else + { + foreach (var type in assembly.GetTypes()) + { + try + { + var t = methodArgumentValue.Split('.'); + var className = t.Length == 1 ? "" : t[t.Length - 2]; + var methodName = t.Last(); + var x = type.GetMethods(Reflection.allBindingFlags); + method ??= x + .Where(m => type.FullName.Split('.').Last().Contains(className) && m.Name.Contains(methodName)) + .MinBy(m => m.Name.Length); + if (method != null) + break; + } + catch (Exception) + { + // ignored + } + } + + if (method == null) + { + Console.Error.WriteLine("I did not found method you specified by name {0} in assembly {1}", + methodArgumentValue, assembly.Location); + return null; + } + } + + return method; + } + private static void PostProcess(Statistics statistics) { statistics.GenerateReport(Console.Out); @@ -44,7 +131,11 @@ private static void EntryPointHandler( SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, - ExplorationMode explorationMode) + ExplorationMode explorationMode, + string pathToModel, + bool useGPU, + bool optimize + ) { var assembly = TryLoadAssembly(assemblyPath); var options = @@ -56,7 +147,10 @@ private static void EntryPointHandler( searchStrategy: strat, verbosity: verbosity, recursionThreshold: recursionThreshold, - explorationMode: explorationMode); + explorationMode: explorationMode, + pathToModel: pathToModel, + useGPU: useGPU, + optimize: optimize); if (assembly == null) return; @@ -149,7 +243,10 @@ private static void AllPublicMethodsHandler( SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, - ExplorationMode explorationMode) + ExplorationMode explorationMode, + string pathToModel, + bool useGPU, + bool optimize) { var assembly = TryLoadAssembly(assemblyPath); var options = @@ -161,7 +258,10 @@ private static void AllPublicMethodsHandler( searchStrategy: strat, verbosity: verbosity, recursionThreshold: recursionThreshold, - explorationMode: explorationMode); + explorationMode: explorationMode, + pathToModel: pathToModel, + useGPU: useGPU, + optimize: optimize); if (assembly == null) return; @@ -184,7 +284,10 @@ private static void PublicMethodsOfTypeHandler( SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, - ExplorationMode explorationMode) + ExplorationMode explorationMode, + string pathToModel, + bool useGPU, + bool optimize) { var assembly = TryLoadAssembly(assemblyPath); if (assembly == null) return; @@ -205,7 +308,10 @@ private static void PublicMethodsOfTypeHandler( searchStrategy: strat, verbosity: verbosity, recursionThreshold: recursionThreshold, - explorationMode: explorationMode); + explorationMode: explorationMode, + pathToModel: pathToModel, + useGPU: useGPU, + optimize: optimize); Statistics statistics; if (runTests) @@ -227,7 +333,10 @@ private static void SpecificMethodHandler( SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, - ExplorationMode explorationMode) + ExplorationMode explorationMode, + string pathToModel, + bool useGPU, + bool optimize) { var assembly = TryLoadAssembly(assemblyPath); if (assembly == null) return; @@ -264,7 +373,10 @@ private static void SpecificMethodHandler( searchStrategy: strat, verbosity: verbosity, recursionThreshold: recursionThreshold, - explorationMode: explorationMode); + explorationMode: explorationMode, + pathToModel: pathToModel, + useGPU: useGPU, + optimize: optimize); Statistics statistics; if (runTests || checkCoverage) @@ -285,7 +397,10 @@ private static void NamespaceHandler( SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, - ExplorationMode explorationMode) + ExplorationMode explorationMode, + string pathToModel, + bool useGPU, + bool optimize) { var assembly = TryLoadAssembly(assemblyPath); if (assembly == null) return; @@ -306,7 +421,10 @@ private static void NamespaceHandler( searchStrategy: strat, verbosity: verbosity, recursionThreshold: recursionThreshold, - explorationMode: explorationMode); + explorationMode: explorationMode, + pathToModel: pathToModel, + useGPU: useGPU, + optimize: optimize); Statistics statistics; if (runTests) @@ -326,6 +444,18 @@ public static int Main(string[] args) aliases: new[] { "--timeout", "-t" }, () => -1, "Time for test generation in seconds. Negative value means no timeout."); + var pathToModelOption = new Option( + aliases: new[] { "--model", "-m" }, + () => defaultOptions.GetDefaultPathToModel(), + "Path to ONNX file with model for AI searcher."); + var useGPUOption = new Option( + aliases: new[] { "--gpu" }, + () => false, + "Enables GPU processing."); + var optimizeOption = new Option( + aliases: new[] { "--optimize" }, + () => false, + "Optimize option."); var solverTimeoutOption = new Option( aliases: new[] { "--solver-timeout", "-st" }, () => -1, @@ -371,6 +501,9 @@ public static int Main(string[] args) rootCommand.AddGlobalOption(verbosityOption); rootCommand.AddGlobalOption(recursionThresholdOption); rootCommand.AddGlobalOption(explorationModeOption); + rootCommand.AddGlobalOption(pathToModelOption); + rootCommand.AddGlobalOption(useGPUOption); + rootCommand.AddGlobalOption(optimizeOption); var entryPointCommand = new Command("--entry-point", "Generate test coverage from the entry point of assembly (assembly must contain Main method)"); @@ -396,7 +529,10 @@ public static int Main(string[] args) parseResult.GetValueForOption(searchStrategyOption), parseResult.GetValueForOption(verbosityOption), parseResult.GetValueForOption(recursionThresholdOption), - parseResult.GetValueForOption(explorationModeOption) + parseResult.GetValueForOption(explorationModeOption), + parseResult.GetValueForOption(pathToModelOption), + parseResult.GetValueForOption(useGPUOption), + parseResult.GetValueForOption(optimizeOption) ); }); @@ -457,7 +593,10 @@ public static int Main(string[] args) parseResult.GetValueForOption(searchStrategyOption), parseResult.GetValueForOption(verbosityOption), parseResult.GetValueForOption(recursionThresholdOption), - parseResult.GetValueForOption(explorationModeOption) + parseResult.GetValueForOption(explorationModeOption), + parseResult.GetValueForOption(pathToModelOption), + parseResult.GetValueForOption(useGPUOption), + parseResult.GetValueForOption(optimizeOption) ); }); @@ -484,7 +623,10 @@ public static int Main(string[] args) parseResult.GetValueForOption(searchStrategyOption), parseResult.GetValueForOption(verbosityOption), parseResult.GetValueForOption(recursionThresholdOption), - parseResult.GetValueForOption(explorationModeOption) + parseResult.GetValueForOption(explorationModeOption), + parseResult.GetValueForOption(pathToModelOption), + parseResult.GetValueForOption(useGPUOption), + parseResult.GetValueForOption(optimizeOption) ); }); @@ -499,6 +641,7 @@ public static int Main(string[] args) specificMethodCommand.SetHandler(context => { var parseResult = context.ParseResult; + var pathToModel = parseResult.GetValueForOption(pathToModelOption); var output = parseResult.GetValueForOption(outputOption); Debug.Assert(output is not null); SpecificMethodHandler( @@ -513,7 +656,10 @@ public static int Main(string[] args) parseResult.GetValueForOption(searchStrategyOption), parseResult.GetValueForOption(verbosityOption), parseResult.GetValueForOption(recursionThresholdOption), - parseResult.GetValueForOption(explorationModeOption) + parseResult.GetValueForOption(explorationModeOption), + pathToModel, + parseResult.GetValueForOption(useGPUOption), + parseResult.GetValueForOption(optimizeOption) ); }); @@ -528,6 +674,7 @@ public static int Main(string[] args) { var parseResult = context.ParseResult; var output = parseResult.GetValueForOption(outputOption); + var pathToModel = parseResult.GetValueForOption(pathToModelOption); Debug.Assert(output is not null); NamespaceHandler( parseResult.GetValueForArgument(assemblyPathArgument), @@ -540,7 +687,10 @@ public static int Main(string[] args) parseResult.GetValueForOption(searchStrategyOption), parseResult.GetValueForOption(verbosityOption), parseResult.GetValueForOption(recursionThresholdOption), - parseResult.GetValueForOption(explorationModeOption) + parseResult.GetValueForOption(explorationModeOption), + pathToModel, + parseResult.GetValueForOption(useGPUOption), + parseResult.GetValueForOption(optimizeOption) ); }); diff --git a/VSharp.Runner/VSharp.Runner.csproj b/VSharp.Runner/VSharp.Runner.csproj index cbb961513..f5c8d3eeb 100644 --- a/VSharp.Runner/VSharp.Runner.csproj +++ b/VSharp.Runner/VSharp.Runner.csproj @@ -1,7 +1,7 @@ - net7.0 + net8.0 Exe VSharp.Runner Debug;Release;DebugTailRec @@ -21,6 +21,7 @@ + diff --git a/VSharp.SILI.Core/PathCondition.fs b/VSharp.SILI.Core/PathCondition.fs index f30f80b5c..cd17e694a 100644 --- a/VSharp.SILI.Core/PathCondition.fs +++ b/VSharp.SILI.Core/PathCondition.fs @@ -7,7 +7,7 @@ type pathCondition = pset // - PC does not contain True // - if PC contains False then False is the only element in PC -module internal PC = +module PC = let public empty : pathCondition = PersistentSet.empty let public isEmpty pc = PersistentSet.isEmpty pc diff --git a/VSharp.SILI.Core/VSharp.SILI.Core.fsproj b/VSharp.SILI.Core/VSharp.SILI.Core.fsproj index b87de58a3..d366086f4 100644 --- a/VSharp.SILI.Core/VSharp.SILI.Core.fsproj +++ b/VSharp.SILI.Core/VSharp.SILI.Core.fsproj @@ -1,7 +1,7 @@  - net7.0 + net8.0 Debug;Release;DebugTailRec AnyCPU @@ -53,7 +53,7 @@ - + diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs index d7fc576cf..a8ef1cdeb 100644 --- a/VSharp.SILI/CILState.fs +++ b/VSharp.SILI/CILState.fs @@ -7,16 +7,17 @@ open System.Collections.Generic open VSharp.Core open VSharp.Interpreter.IL open IpOperations +open VSharp.ML.GameServer.Messages module CilState = type prefix = | Constrained of System.Type - let mutable currentStateId = 0u + let mutable currentStateId = 0u let getNextStateId() = let nextId = currentStateId - currentStateId <- currentStateId + 1u + currentStateId <- currentStateId + 1u nextId type public ErrorReporter internal (cilState : cilState) = @@ -112,12 +113,19 @@ module CilState = /// /// Deterministic state id. /// - internalId : uint + mutable internalId : uint + mutable visitedAgainVertices: uint + mutable visitedNotCoveredVerticesInZone: uint + mutable visitedNotCoveredVerticesOutOfZone: uint + mutable stepWhenMovedLastTime: uint + mutable instructionsVisitedInCurrentBlock: uint + mutable _history: Dictionary + mutable children: list webConfiguration : webConfiguration option } static member private CommonCreateInitial (m : Method) (state : state) webConfiguration = - let ip = Instruction(0, m) + let ip = Instruction(0, m) let approximateLoc = ip.ToCodeLocation() |> Option.get { ipStack = List.singleton ip @@ -137,6 +145,13 @@ module CilState = history = Set.empty entryMethod = Some m internalId = getNextStateId() + visitedAgainVertices = 0u + visitedNotCoveredVerticesInZone = 0u + visitedNotCoveredVerticesOutOfZone = 0u + stepWhenMovedLastTime = 0u + instructionsVisitedInCurrentBlock = 0u + _history = Dictionary() + children = [] webConfiguration = webConfiguration } @@ -158,7 +173,7 @@ module CilState = member x.StartsFromMethodBeginning with get() = match x.startingIP with - | Instruction (0, _) -> true + | Instruction (0, _) -> true | _ -> false member x.SetCurrentTime time = x.state.currentTime <- time @@ -466,6 +481,7 @@ module CilState = let mkCilState state' = if LanguagePrimitives.PhysicalEquality state' x.state then x else clone.Copy(state') + StatedConditionalExecution x.state conditionInvocation (fun state k -> thenBranch (mkCilState state) k) (fun state k -> elseBranch (mkCilState state) k) @@ -501,7 +517,14 @@ module CilState = // -------------------- Changing inner state -------------------- member x.Copy(state : state) = - { x with state = state; internalId = getNextStateId() } + let historyCopy = Dictionary<_,_>() + for kvp in x._history do historyCopy.Add(kvp.Key, kvp.Value) + { x with state = state + internalId = getNextStateId() + children = [] + _history = historyCopy + stepWhenMovedLastTime = x.stepWhenMovedLastTime + } // This function copies cilState, instead of mutation member x.ChangeState state' : cilState = @@ -520,6 +543,17 @@ module CilState = interface IGraphTrackableState with override this.CodeLocation = this.approximateLoc override this.CallStack = Memory.StackTrace this.state.memory.Stack |> List.map (fun m -> m :?> Method) + override this.Id = this.internalId + override this.PathCondition with get () = this.state.pc + override this.VisitedAgainVertices with get () = this.visitedAgainVertices + override this.VisitedNotCoveredVerticesInZone with get () = this.visitedNotCoveredVerticesInZone + override this.VisitedNotCoveredVerticesOutOfZone with get () = this.visitedNotCoveredVerticesOutOfZone + override this.StepWhenMovedLastTime with get () = this.stepWhenMovedLastTime + override this.InstructionsVisitedInCurrentBlock + with get() = this.instructionsVisitedInCurrentBlock + and set v = this.instructionsVisitedInCurrentBlock <- v + override this.History with get () = this._history + override this.Children with get () = this.children |> Seq.cast<_> |> Array.ofSeq module CilStateOperations = open CilState diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index 32d540ce0..b46d93ba7 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -661,7 +661,7 @@ type ILInterpreter() as this = static member InitFunctionFrameCIL (cilState : cilState) (method : Method) this paramValues = Memory.InitFunctionFrame cilState.state method this (paramValues |> Option.bind (List.map Some >> Some)) - Instruction(0, method) |> cilState.PushToIp + Instruction(0, method) |> cilState.PushToIp static member CheckDisallowNullAttribute (method : Method) (argumentsOpt : term list option) (cilState : cilState) shouldReportError k = if not <| method.CheckAttributes then @@ -869,7 +869,7 @@ type ILInterpreter() as this = | _ -> __unreachable__() let bodyForModel = Memory.AllocateString " " modelState let modelStates = Memory.Write modelState bodyArgRef bodyForModel - Instruction(0, method) |> cilState.PushToIp + Instruction(0, method) |> cilState.PushToIp List.singleton cilState member private x.ConfigureAspNet (cilState : cilState) thisOption = @@ -884,7 +884,7 @@ type ILInterpreter() as this = let contentRootPath = Memory.AllocateString webConfig.contentRootPath.FullName cilState.state let parameters = Some [Some webAppOptions; Some environmentName; Some applicationName; Some contentRootPath] Memory.InitFunctionFrame cilState.state method None parameters - Instruction(0, method) |> cilState.PushToIp + Instruction(0, method) |> cilState.PushToIp List.singleton cilState member private x.ExecutorExecute (cilState : cilState) thisOption args = @@ -904,7 +904,7 @@ type ILInterpreter() as this = |> Application.getMethod let args = Some (List.map Some args) Memory.InitFunctionFrame cilState.state invokeMethod None args - Instruction(0, invokeMethod) |> cilState.PushToIp + Instruction(0, invokeMethod) |> cilState.PushToIp List.singleton cilState | _ -> internalfail $"ExecutorExecute: unexpected 'this' {thisOption}" @@ -1944,11 +1944,11 @@ type ILInterpreter() as this = executeAllInstructions ([],[],[]) cilState id member private x.IncrementLevelIfNeeded (m : Method) (offset : offset) (cilState : cilState) = - if offset = 0 || m.CFG.IsLoopEntry offset then + if offset = 0 || m.CFG.IsLoopEntry offset then cilState.IncrementLevel {offset = offset; method = m} member private x.DecrementMethodLevel (cilState : cilState) method = - let key = {offset = 0; method = method} + let key = {offset = 0; method = method} cilState.DecrementLevel key member private x.InTryBlock offset (clause : exceptionHandlingClause) = @@ -2001,7 +2001,7 @@ type ILInterpreter() as this = // Normal execution // Also on entering try block we push new exception register | Instruction(offset, m) -> - if offset = 0 then Logger.info $"Starting to explore method {m}" + if offset = 0 then Logger.info $"Starting to explore method {m}" x.PushExceptionRegisterIfNeeded cilState m offset x.ExecuteInstruction m offset cilState |> k // Exiting method diff --git a/VSharp.SILI/VSharp.SILI.fsproj b/VSharp.SILI/VSharp.SILI.fsproj index 5cf1a1e6e..c99128d9c 100644 --- a/VSharp.SILI/VSharp.SILI.fsproj +++ b/VSharp.SILI/VSharp.SILI.fsproj @@ -1,7 +1,7 @@ - + - net7.0 + net8.0 Debug;Release;DebugTailRec AnyCPU @@ -29,7 +29,7 @@ - + diff --git a/VSharp.Solver/VSharp.Solver.fsproj b/VSharp.Solver/VSharp.Solver.fsproj index 0dff8a882..fb4a8aa5a 100644 --- a/VSharp.Solver/VSharp.Solver.fsproj +++ b/VSharp.Solver/VSharp.Solver.fsproj @@ -1,7 +1,7 @@  - net7.0 + net8.0 Debug;Release;DebugTailRec AnyCPU @@ -27,7 +27,7 @@ - + diff --git a/VSharp.Test/Benchmarks/Benchmarks.cs b/VSharp.Test/Benchmarks/Benchmarks.cs index b1ebd7d67..8e0f49aaa 100644 --- a/VSharp.Test/Benchmarks/Benchmarks.cs +++ b/VSharp.Test/Benchmarks/Benchmarks.cs @@ -35,7 +35,7 @@ private static bool TryBuildGeneratedTests() return process.IsSuccess(); } - private class Reporter: IReporter + private class Reporter : IReporter { private readonly UnitTests _unitTests; @@ -92,7 +92,11 @@ public static BenchmarkResult Run( checkAttributes: false, stopOnCoverageAchieved: -1, randomSeed: randomSeed, - stepsLimit: stepsLimit + stepsLimit: stepsLimit, + aiOptions: null, + pathToModel: null, + useGPU: false, + optimize: false ); var fuzzerOptions = new FuzzerOptions( @@ -111,7 +115,7 @@ public static BenchmarkResult Run( using var explorer = new Explorer.Explorer(explorationOptions, new Reporter(unitTests)); explorer.StartExploration( - new[] {exploredMethodInfo}, + new[] { exploredMethodInfo }, global::System.Array.Empty>() ); diff --git a/VSharp.Test/IntegrationTests.cs b/VSharp.Test/IntegrationTests.cs index 955b71205..6346f9a57 100644 --- a/VSharp.Test/IntegrationTests.cs +++ b/VSharp.Test/IntegrationTests.cs @@ -7,6 +7,7 @@ using System.Reflection; using System.Runtime.ExceptionServices; using System.Threading; +using Microsoft.FSharp.Collections; using NUnit.Framework; using NUnit.Framework.Interfaces; using NUnit.Framework.Internal; @@ -28,7 +29,8 @@ public enum SearchStrategy ContributedCoverage, ExecutionTree, ExecutionTreeContributedCoverage, - Interleaved + Interleaved, + AI } public enum CoverageZone @@ -73,7 +75,7 @@ public IEnumerable BuildFrom(ITypeInfo typeInfo) } [AttributeUsage(AttributeTargets.Class | AttributeTargets.Struct | AttributeTargets.Method, AllowMultiple = true)] - public class IgnoreFuzzerAttribute: Attribute + public class IgnoreFuzzerAttribute : Attribute { public string Reason { get; init; } @@ -130,6 +132,9 @@ static TestSvmAttribute() private readonly ExplorationMode _explorationMode; private readonly int _randomSeed; private readonly uint _stepsLimit; + private readonly string _pathToModel; + private readonly bool _useGPU; + private readonly bool _optimize; public TestSvmAttribute( int expectedCoverage = -1, @@ -140,13 +145,16 @@ public TestSvmAttribute( SearchStrategy strat = SearchStrategy.BFS, CoverageZone coverageZone = CoverageZone.Class, TestsCheckerMode testsCheckerMode = TestsCheckerMode.RenderAndRun, - bool checkAttributes = true, bool hasExternMocking = false, + bool checkAttributes = true, OsType supportedOs = OsType.All, FuzzerIsolation fuzzerIsolation = FuzzerIsolation.Process, ExplorationMode explorationMode = ExplorationMode.Sili, int randomSeed = 0, - uint stepsLimit = 0) + uint stepsLimit = 0, + string pathToModel = "models/model.onnx", + bool useGPU = false, + bool optimize = false) { if (expectedCoverage < 0) _expectedCoverage = null; @@ -160,6 +168,7 @@ public TestSvmAttribute( _strat = strat; _coverageZone = coverageZone; _testsCheckerMode = testsCheckerMode; + _hasExternMocking = hasExternMocking; _checkAttributes = checkAttributes; _hasExternMocking = hasExternMocking; _supportedOs = supportedOs; @@ -167,6 +176,9 @@ public TestSvmAttribute( _explorationMode = explorationMode; _randomSeed = randomSeed; _stepsLimit = stepsLimit; + _pathToModel = pathToModel; + _useGPU = useGPU; + _optimize = optimize; } public TestCommand Wrap(TestCommand command) @@ -182,12 +194,15 @@ public TestCommand Wrap(TestCommand command) _coverageZone, _testsCheckerMode, _checkAttributes, - _hasExternMocking, _supportedOs, _fuzzerIsolation, _explorationMode, _randomSeed, - _stepsLimit + _stepsLimit, + _hasExternMocking, + _pathToModel, + _useGPU, + _optimize ); } @@ -211,8 +226,11 @@ private class TestSvmCommand : DelegatingTestCommand private readonly ExplorationMode _explorationMode; private readonly int _randomSeed; private readonly uint _stepsLimit; + private readonly string _pathToModel; + private readonly bool _useGPU; + private readonly bool _optimize; - private class Reporter: IReporter + private class Reporter : IReporter { private readonly UnitTests _unitTests; @@ -223,7 +241,7 @@ public Reporter(UnitTests unitTests) public void ReportFinished(UnitTest unitTest) => _unitTests.GenerateTest(unitTest); public void ReportException(UnitTest unitTest) => _unitTests.GenerateError(unitTest); - public void ReportIIE(InsufficientInformationException iie) {} + public void ReportIIE(InsufficientInformationException iie) { } public void ReportInternalFail(Method method, Exception exn) => ExceptionDispatchInfo.Capture(exn).Throw(); public void ReportCrash(Exception exn) => ExceptionDispatchInfo.Capture(exn).Throw(); } @@ -239,12 +257,15 @@ public TestSvmCommand( CoverageZone coverageZone, TestsCheckerMode testsCheckerMode, bool checkAttributes, - bool hasExternMocking, OsType supportedOs, FuzzerIsolation fuzzerIsolation, ExplorationMode explorationMode, int randomSeed, - uint stepsLimit) : base(innerCommand) + uint stepsLimit, + bool hasExternMocking, + string pathToModel, + bool useGPU, + bool optimize) : base(innerCommand) { _baseCoverageZone = coverageZone; _baseSearchStrat = TestContext.Parameters[SearchStrategyParameterName] == null ? @@ -274,6 +295,7 @@ public TestSvmCommand( SearchStrategy.ExecutionTree => searchMode.ExecutionTreeMode, SearchStrategy.ExecutionTreeContributedCoverage => searchMode.NewInterleavedMode(searchMode.ExecutionTreeMode, 1, searchMode.ContributedCoverageMode, 1), SearchStrategy.Interleaved => searchMode.NewInterleavedMode(searchMode.ShortestDistanceBasedMode, 1, searchMode.ContributedCoverageMode, 9), + SearchStrategy.AI => searchMode.AIMode, _ => throw new ArgumentOutOfRangeException(nameof(strat), strat, null) }; @@ -296,6 +318,9 @@ public TestSvmCommand( _explorationMode = explorationMode; _randomSeed = randomSeed; _stepsLimit = stepsLimit; + _pathToModel = pathToModel; + _useGPU = useGPU; + _optimize = optimize; } private TestResult IgnoreTest(TestExecutionContext context) @@ -355,7 +380,7 @@ DirectoryInfo testsDir bool success; var resultMessage = string.Empty; uint? actualCoverage; - if (_expectedCoverage is {} expectedCoverage) + if (_expectedCoverage is { } expectedCoverage) { TestContext.Out.WriteLine("Starting coverage tool..."); success = @@ -427,7 +452,7 @@ private TestResult Explore(TestExecutionContext context) }; var originMethodInfo = innerCommand.Test.Method.MethodInfo; - var exploredMethodInfo = (MethodInfo) AssemblyManager.NormalizeMethod(originMethodInfo); + var exploredMethodInfo = (MethodInfo)AssemblyManager.NormalizeMethod(originMethodInfo); var stats = new TestStatistics( exploredMethodInfo, _releaseBranches, @@ -451,7 +476,11 @@ private TestResult Explore(TestExecutionContext context) checkAttributes: _checkAttributes, stopOnCoverageAchieved: _expectedCoverage ?? -1, randomSeed: _randomSeed, - stepsLimit: _stepsLimit + stepsLimit: _stepsLimit, + aiOptions: null, + pathToModel: _pathToModel, + useGPU: _useGPU, + optimize: _optimize ); var fuzzerOptions = new FuzzerOptions( @@ -474,8 +503,9 @@ private TestResult Explore(TestExecutionContext context) ); using var explorer = new Explorer.Explorer(explorationOptions, new Reporter(unitTests)); + Application.reset(); explorer.StartExploration( - new [] { exploredMethodInfo }, + new[] { exploredMethodInfo }, global::System.Array.Empty>() ); diff --git a/VSharp.Test/Tests/ControlFlow.cs b/VSharp.Test/Tests/ControlFlow.cs index 54234e21d..22b49fbda 100644 --- a/VSharp.Test/Tests/ControlFlow.cs +++ b/VSharp.Test/Tests/ControlFlow.cs @@ -1,4 +1,4 @@ -using System; +using System; using NUnit.Framework; using VSharp.Test; @@ -375,6 +375,21 @@ public static int NestedForsSimple(int x) return res; } + + [TestSvm(100, strat: SearchStrategy.AI)] + public static int NestedForsSimple_AI(int x) + { + int res = 0; + for (int i = 0; i < x; i++) + { + for (int j = 0; j < x; j++) + { + res++; + } + } + + return res; + } [Ignore("Looping due to non-terminating paths")] public static int NestedForsHard(int x) diff --git a/VSharp.Test/Tests/LoanExam.cs b/VSharp.Test/Tests/LoanExam.cs index f2ecd760b..dfece59f1 100644 --- a/VSharp.Test/Tests/LoanExam.cs +++ b/VSharp.Test/Tests/LoanExam.cs @@ -1,4 +1,4 @@ -using System; +using System; using VSharp.Test; namespace IntegrationTests; diff --git a/VSharp.Test/Tests/Mocking.cs b/VSharp.Test/Tests/Mocking.cs index 2ba995330..bf3441d8e 100644 --- a/VSharp.Test/Tests/Mocking.cs +++ b/VSharp.Test/Tests/Mocking.cs @@ -1,6 +1,5 @@ using System; using System.Collections.Generic; -using System.Diagnostics; using System.Diagnostics.CodeAnalysis; using NUnit.Framework; using VSharp.Test; diff --git a/VSharp.Test/VSharp.Test.csproj b/VSharp.Test/VSharp.Test.csproj index e9ded0459..571f25464 100644 --- a/VSharp.Test/VSharp.Test.csproj +++ b/VSharp.Test/VSharp.Test.csproj @@ -1,7 +1,7 @@  - net7.0 + net8.0 false Release AnyCPU diff --git a/VSharp.TestExtensions/VSharp.TestExtensions.csproj b/VSharp.TestExtensions/VSharp.TestExtensions.csproj index 31765b139..66ea2d619 100644 --- a/VSharp.TestExtensions/VSharp.TestExtensions.csproj +++ b/VSharp.TestExtensions/VSharp.TestExtensions.csproj @@ -1,7 +1,7 @@ - net7.0 + net8.0 enable enable VSharp.TestExtensions diff --git a/VSharp.TestGenerator/VSharp.TestGenerator.fsproj b/VSharp.TestGenerator/VSharp.TestGenerator.fsproj index 245b2ab64..337b856c2 100644 --- a/VSharp.TestGenerator/VSharp.TestGenerator.fsproj +++ b/VSharp.TestGenerator/VSharp.TestGenerator.fsproj @@ -1,7 +1,7 @@  - net7.0 + net8.0 true Debug;Release;DebugTailRec AnyCPU @@ -27,7 +27,7 @@ - + diff --git a/VSharp.TestRenderer/VSharp.TestRenderer.csproj b/VSharp.TestRenderer/VSharp.TestRenderer.csproj index d517d3d98..9680ee2ed 100644 --- a/VSharp.TestRenderer/VSharp.TestRenderer.csproj +++ b/VSharp.TestRenderer/VSharp.TestRenderer.csproj @@ -1,7 +1,7 @@ - net7.0 + net8.0 enable enable Exe diff --git a/VSharp.TestRunner/VSharp.TestRunner.csproj b/VSharp.TestRunner/VSharp.TestRunner.csproj index ced2b512e..b5b331622 100644 --- a/VSharp.TestRunner/VSharp.TestRunner.csproj +++ b/VSharp.TestRunner/VSharp.TestRunner.csproj @@ -1,7 +1,7 @@ - net7.0 + net8.0 Exe true Debug;Release;DebugTailRec diff --git a/VSharp.Utils/GraphUtils.fs b/VSharp.Utils/GraphUtils.fs index 9ec54799b..6978a65a6 100644 --- a/VSharp.Utils/GraphUtils.fs +++ b/VSharp.Utils/GraphUtils.fs @@ -5,6 +5,12 @@ open System.Collections.Generic module GraphUtils = type graph<'a> = Dictionary<'a, HashSet<'a>> type distanceCache<'a> = Dictionary<'a, Dictionary<'a, uint>> + + type ICallGraphNode = + abstract OutgoingEdges : seq with get + + type IReversedCallGraphNode = + abstract OutgoingEdges : seq with get type IGraphNode<'t> = abstract OutgoingEdges : seq<'t> with get diff --git a/VSharp.Utils/Prelude.fs b/VSharp.Utils/Prelude.fs index 24415e6e7..0aa28e977 100644 --- a/VSharp.Utils/Prelude.fs +++ b/VSharp.Utils/Prelude.fs @@ -13,7 +13,9 @@ type InsufficientInformationException(msg : string) = [] module public Prelude = - + + type [] byte_offset + let public internalfail message = raise (InternalException message) let public internalfailf format = Printf.ksprintf internalfail format let undefinedBehaviour reason = internalfail $"Undefined behaviour: %s{reason}" diff --git a/VSharp.Utils/UnitTests.fs b/VSharp.Utils/UnitTests.fs index 5f7848453..2d6ec572c 100644 --- a/VSharp.Utils/UnitTests.fs +++ b/VSharp.Utils/UnitTests.fs @@ -32,11 +32,11 @@ type UnitTests(outputDir : string) = member x.GenerateTest (test : UnitTest) = testNumber <- testNumber + 1u - generateTest test ("test" + testNumber.ToString()) + generateTest test (test.Method.Name + ".test" + testNumber.ToString()) member x.GenerateError (test : UnitTest) = errorNumber <- errorNumber + 1u - generateTest test ("error" + errorNumber.ToString()) + generateTest test (test.Method.Name + ".error" + errorNumber.ToString()) member x.WriteReport (reporter : Action) = let reportFileName = $"%s{currentDir.FullName}%c{Path.DirectorySeparatorChar}report.txt" diff --git a/VSharp.Utils/VSharp.Utils.fsproj b/VSharp.Utils/VSharp.Utils.fsproj index 3bb1a19d6..21b098816 100644 --- a/VSharp.Utils/VSharp.Utils.fsproj +++ b/VSharp.Utils/VSharp.Utils.fsproj @@ -1,7 +1,7 @@  - net7.0 + net8.0 Debug;Release;DebugTailRec AnyCPU @@ -53,7 +53,7 @@ - + diff --git a/VSharp.sln b/VSharp.sln index b98c7da26..b097d73b8 100644 --- a/VSharp.sln +++ b/VSharp.sln @@ -1,4 +1,4 @@ - + Microsoft Visual Studio Solution File, Format Version 12.00 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VSharp.CSharpUtils", "VSharp.CSharpUtils\VSharp.CSharpUtils.csproj", "{C3AC6243-43EB-4312-AF41-03D36CED52DE}" EndProject @@ -28,6 +28,10 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VSharp.TestExtensions", "VS EndProject Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "VSharp.TestGenerator", "VSharp.TestGenerator\VSharp.TestGenerator.fsproj", "{8FC15B9A-7563-4480-9E3A-30DE29CD9C5F}" EndProject +Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "VSharp.ML.GameServer.Runner", "VSharp.ML.GameServer.Runner\VSharp.ML.GameServer.Runner.fsproj", "{68921FA7-1FBD-43E5-9459-EA01303A4DC8}" +EndProject +Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "VSharp.ML.GameServer", "VSharp.ML.GameServer\VSharp.ML.GameServer.fsproj", "{44586A7C-12E4-4765-ADF0-20DE2ED2EEC7}" +EndProject Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "VSharp.Fuzzer", "VSharp.Fuzzer\VSharp.Fuzzer.fsproj", "{70A99736-8F51-40EA-9AB3-37E64697D3B8}" EndProject Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "VSharp.Explorer", "VSharp.Explorer\VSharp.Explorer.fsproj", "{9455C456-51A6-4CA3-B33A-4F168CBADADA}" @@ -125,6 +129,36 @@ Global {8FC15B9A-7563-4480-9E3A-30DE29CD9C5F}.Release|Any CPU.Build.0 = Release|Any CPU {8FC15B9A-7563-4480-9E3A-30DE29CD9C5F}.DebugTailRec|Any CPU.ActiveCfg = DebugTailRec|Any CPU {8FC15B9A-7563-4480-9E3A-30DE29CD9C5F}.DebugTailRec|Any CPU.Build.0 = DebugTailRec|Any CPU + {8FC15B9A-7563-4480-9E3A-30DE29CD9C5F}.DebugTailRec|Any CPU.ActiveCfg = Debug|Any CPU + {8FC15B9A-7563-4480-9E3A-30DE29CD9C5F}.DebugTailRec|Any CPU.Build.0 = Debug|Any CPU + {4C5B924D-8934-44F2-847A-BE91416DB557}.ReleaseConcolic|Any CPU.ActiveCfg = Release|Any CPU + {4C5B924D-8934-44F2-847A-BE91416DB557}.DebugConcolic|Any CPU.ActiveCfg = Debug|Any CPU + {4C5B924D-8934-44F2-847A-BE91416DB557}.DebugConcolic|Any CPU.Build.0 = Debug|Any CPU + {4C5B924D-8934-44F2-847A-BE91416DB557}.ReleaseConcolic|Any CPU.Build.0 = Release|Any CPU + {68921FA7-1FBD-43E5-9459-EA01303A4DC8}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {68921FA7-1FBD-43E5-9459-EA01303A4DC8}.Debug|Any CPU.Build.0 = Debug|Any CPU + {68921FA7-1FBD-43E5-9459-EA01303A4DC8}.Release|Any CPU.ActiveCfg = Release|Any CPU + {68921FA7-1FBD-43E5-9459-EA01303A4DC8}.Release|Any CPU.Build.0 = Release|Any CPU + {68921FA7-1FBD-43E5-9459-EA01303A4DC8}.DebugTailRec|Any CPU.ActiveCfg = Debug|Any CPU + {68921FA7-1FBD-43E5-9459-EA01303A4DC8}.DebugTailRec|Any CPU.Build.0 = Debug|Any CPU + {68921FA7-1FBD-43E5-9459-EA01303A4DC8}.ReleaseConcolic|Any CPU.ActiveCfg = Debug|Any CPU + {68921FA7-1FBD-43E5-9459-EA01303A4DC8}.ReleaseConcolic|Any CPU.Build.0 = Debug|Any CPU + {68921FA7-1FBD-43E5-9459-EA01303A4DC8}.DebugConcolic|Any CPU.ActiveCfg = Debug|Any CPU + {68921FA7-1FBD-43E5-9459-EA01303A4DC8}.DebugConcolic|Any CPU.Build.0 = Debug|Any CPU + {44586A7C-12E4-4765-ADF0-20DE2ED2EEC7}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {44586A7C-12E4-4765-ADF0-20DE2ED2EEC7}.Debug|Any CPU.Build.0 = Debug|Any CPU + {44586A7C-12E4-4765-ADF0-20DE2ED2EEC7}.Release|Any CPU.ActiveCfg = Release|Any CPU + {44586A7C-12E4-4765-ADF0-20DE2ED2EEC7}.Release|Any CPU.Build.0 = Release|Any CPU + {44586A7C-12E4-4765-ADF0-20DE2ED2EEC7}.DebugTailRec|Any CPU.ActiveCfg = Debug|Any CPU + {44586A7C-12E4-4765-ADF0-20DE2ED2EEC7}.DebugTailRec|Any CPU.Build.0 = Debug|Any CPU + {44586A7C-12E4-4765-ADF0-20DE2ED2EEC7}.ReleaseConcolic|Any CPU.ActiveCfg = Debug|Any CPU + {44586A7C-12E4-4765-ADF0-20DE2ED2EEC7}.ReleaseConcolic|Any CPU.Build.0 = Debug|Any CPU + {44586A7C-12E4-4765-ADF0-20DE2ED2EEC7}.DebugConcolic|Any CPU.ActiveCfg = Debug|Any CPU + {44586A7C-12E4-4765-ADF0-20DE2ED2EEC7}.DebugConcolic|Any CPU.Build.0 = Debug|Any CPU + {AEB2ABD0-5045-4A28-BBEB-2F353BD543FE}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {AEB2ABD0-5045-4A28-BBEB-2F353BD543FE}.Debug|Any CPU.Build.0 = Debug|Any CPU + {AEB2ABD0-5045-4A28-BBEB-2F353BD543FE}.Release|Any CPU.ActiveCfg = Release|Any CPU + {AEB2ABD0-5045-4A28-BBEB-2F353BD543FE}.Release|Any CPU.Build.0 = Release|Any CPU {70A99736-8F51-40EA-9AB3-37E64697D3B8}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {70A99736-8F51-40EA-9AB3-37E64697D3B8}.Debug|Any CPU.Build.0 = Debug|Any CPU {70A99736-8F51-40EA-9AB3-37E64697D3B8}.Release|Any CPU.ActiveCfg = Release|Any CPU @@ -143,5 +177,9 @@ Global {CA15A9BA-17DC-4D0C-853E-11E1A4B8D29F}.Release|Any CPU.Build.0 = Release|Any CPU {CA15A9BA-17DC-4D0C-853E-11E1A4B8D29F}.DebugTailRec|Any CPU.ActiveCfg = Debug|Any CPU {CA15A9BA-17DC-4D0C-853E-11E1A4B8D29F}.DebugTailRec|Any CPU.Build.0 = Debug|Any CPU + {AEB2ABD0-5045-4A28-BBEB-2F353BD543FE}.DebugTailRec|Any CPU.ActiveCfg = Debug|Any CPU + {AEB2ABD0-5045-4A28-BBEB-2F353BD543FE}.DebugTailRec|Any CPU.Build.0 = Debug|Any CPU + EndGlobalSection + GlobalSection(NestedProjects) = preSolution EndGlobalSection EndGlobal diff --git a/global.json b/global.json index 3cb4f9622..18b689d10 100644 --- a/global.json +++ b/global.json @@ -1,6 +1,6 @@ { "sdk": { - "version": "7.0.0", + "version": "8.0.0", "rollForward": "latestMinor", "allowPrerelease": false }