From b2b8676197264accc883adbcbf5115ddbffabd85 Mon Sep 17 00:00:00 2001 From: Anya497 Date: Thu, 20 Mar 2025 10:19:44 +0300 Subject: [PATCH 1/8] Run VSharp building on pull request and push. --- .github/workflows/build_vsharp.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build_vsharp.yml b/.github/workflows/build_vsharp.yml index 3ad121329..da9bca66d 100644 --- a/.github/workflows/build_vsharp.yml +++ b/.github/workflows/build_vsharp.yml @@ -1,7 +1,7 @@ name: 'Build VSharp' on: - workflow_call + [workflow_call, pull_request, push] jobs: build: From d6c320a4bec464847bdbec7cf15d928cd8fc4820 Mon Sep 17 00:00:00 2001 From: Anya497 Date: Thu, 20 Mar 2025 10:23:03 +0300 Subject: [PATCH 2/8] Refresh versions. --- .github/workflows/build_vsharp.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/build_vsharp.yml b/.github/workflows/build_vsharp.yml index da9bca66d..0f7ade532 100644 --- a/.github/workflows/build_vsharp.yml +++ b/.github/workflows/build_vsharp.yml @@ -8,10 +8,10 @@ jobs: runs-on: ubuntu-22.04 steps: - 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 @@ -21,11 +21,11 @@ jobs: - name: Build VSharp run: dotnet build -c DebugTailRec - - uses: actions/upload-artifact@v3 + - 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 From b428cf6b238d01c47ed556e0eeff28275c24a26e Mon Sep 17 00:00:00 2001 From: Anya497 Date: Thu, 20 Mar 2025 10:26:34 +0300 Subject: [PATCH 3/8] Setup dotnet7. --- .github/workflows/build_vsharp.yml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/.github/workflows/build_vsharp.yml b/.github/workflows/build_vsharp.yml index 0f7ade532..c1b017169 100644 --- a/.github/workflows/build_vsharp.yml +++ b/.github/workflows/build_vsharp.yml @@ -7,10 +7,15 @@ 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@v4 with: submodules: false + - uses: actions/cache@v4 id: nuget-cache with: @@ -18,13 +23,16 @@ jobs: key: ${{ runner.os }}-nuget-${{ hashFiles('**/*.csproj', '**/*.fsproj') }} restore-keys: | ${{ runner.os }}-nuget- + - name: Build VSharp run: dotnet build -c DebugTailRec + - uses: actions/upload-artifact@v4 with: name: runner path: ./VSharp.Runner/bin/DebugTailRec/net7.0 + - uses: actions/upload-artifact@v4 with: name: test_runner From 3f9d71072c86cc206b1955b12395c17e18a97f58 Mon Sep 17 00:00:00 2001 From: Anya497 Date: Thu, 20 Mar 2025 13:01:08 +0300 Subject: [PATCH 4/8] Build in Release mode. --- .github/workflows/build_vsharp.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build_vsharp.yml b/.github/workflows/build_vsharp.yml index c1b017169..edc53591f 100644 --- a/.github/workflows/build_vsharp.yml +++ b/.github/workflows/build_vsharp.yml @@ -26,7 +26,7 @@ jobs: - name: Build VSharp run: - dotnet build -c DebugTailRec + dotnet build -c Release - uses: actions/upload-artifact@v4 with: From 1dd6401358aca164dd776f170777c74e30bb6ac5 Mon Sep 17 00:00:00 2001 From: Anya497 Date: Sat, 15 Mar 2025 10:36:43 +0300 Subject: [PATCH 5/8] Add path condition vertex type. Support path condition processing. Refactor. --- VSharp.IL/Serializer.fs | 630 +++++++++++++++++++++---------- VSharp.ML.GameServer/Messages.fs | 422 +++++++++++++-------- 2 files changed, 703 insertions(+), 349 deletions(-) diff --git a/VSharp.IL/Serializer.fs b/VSharp.IL/Serializer.fs index dc25cfd75..f42e9d46f 100644 --- a/VSharp.IL/Serializer.fs +++ b/VSharp.IL/Serializer.fs @@ -10,6 +10,9 @@ open VSharp open VSharp.GraphUtils open VSharp.ML.GameServer.Messages open FSharpx.Collections +open type VSharp.Core.termNode +open VSharp.Core + [] @@ -21,20 +24,28 @@ type Statistics = 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 - } - + 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 @@ -45,6 +56,7 @@ type StateMetrics = val DistanceToNearestUncovered: uint val DistanceToNearestNotVisited: uint val DistanceToNearestReturn: uint + new ( stateId, @@ -56,16 +68,14 @@ type StateMetrics = distanceToNearestNotVisited, distanceTuNearestReturn ) = - { - StateId = stateId - NextInstructionIsUncoveredInZone = nextInstructionIsUncoveredInZone - ChildNumber = childNumber - VisitedVerticesInZone = visitedVerticesInZone - HistoryLength = historyLength - DistanceToNearestUncovered = distanceToNearestUncovered - DistanceToNearestNotVisited = distanceToNearestNotVisited - DistanceToNearestReturn = distanceTuNearestReturn - } + { StateId = stateId + NextInstructionIsUncoveredInZone = nextInstructionIsUncoveredInZone + ChildNumber = childNumber + VisitedVerticesInZone = visitedVerticesInZone + HistoryLength = historyLength + DistanceToNearestUncovered = distanceToNearestUncovered + DistanceToNearestNotVisited = distanceToNearestNotVisited + DistanceToNearestReturn = distanceTuNearestReturn } [] type StateInfoToDump = @@ -78,6 +88,7 @@ type StateInfoToDump = val DistanceToUncoveredNormalized: float val DistanceToNotVisitedNormalized: float val ExpectedWeight: float + new ( stateId, @@ -87,98 +98,147 @@ type StateInfoToDump = productivity, distanceToReturn, distanceToUncovered, - distanceToNotVisited + 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 - } + { 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 calculateStateMetrics interproceduralGraphDistanceFrom (state: IGraphTrackableState) = let currentBasicBlock = state.CodeLocation.BasicBlock - let distances = + + 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 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 + 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) + |> 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 - + + 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) + + 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 = + + 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 computeStatistics (gameState: GameState) = let mutable coveredVerticesInZone = 0u let mutable coveredVerticesOutOfZone = 0u let mutable visitedVerticesInZone = 0u @@ -187,164 +247,342 @@ let computeStatistics (gameState:GameState) = 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 + 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) = + + 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>() + let interproceduralGraphDistanceFrom = + Dictionary>() + currentBasicBlock.AssociatedStates - |> Seq.iter (fun s -> statesMetrics.Add (calculateStateMetrics interproceduralGraphDistanceFrom s)) - - let statesInfoToDump = + |> 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) - + 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)) + |> 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 collectGameState (basicBlocks:ResizeArray) filterStates = - + +let getFirstFreePathConditionVertexId = + let mutable count = 0u + + fun () -> + let res = count + count <- count + 1u + res + +let pathConditionVertices = Dictionary() + +let collectPathCondition term = // TODO: Support other operations + let termsToVisit = + Stack> [| (term, getFirstFreePathConditionVertexId ()) |] + + let pathConditionDelta = ResizeArray() + + while termsToVisit.Count > 0 do + let currentTerm, currentTermId = termsToVisit.Pop() + + let markAsVisited (vertexType: pathConditionVertexType) children = + let newVertex = PathConditionVertex(currentTermId, vertexType, children) + pathConditionVertices.Add(currentTerm, newVertex) + pathConditionDelta.Add newVertex + + let handleTerm term (children: ResizeArray<_>) = + let termId = + if not <| pathConditionVertices.ContainsKey term then + getFirstFreePathConditionVertexId () + else + pathConditionVertices.[term].Id + + children.Add termId + termsToVisit.Push((term, termId)) + + if not <| pathConditionVertices.ContainsKey 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 + handleTerm 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 + handleTerm t children + + markAsVisited pathConditionVertexType.Struct (children.ToArray()) + | HeapRef(_, _) -> markAsVisited pathConditionVertexType.HeapRef [||] + | Ref(_) -> markAsVisited pathConditionVertexType.Ref [||] + | Ptr(_, _, t) -> + let children = ResizeArray> [||] + handleTerm t children + markAsVisited pathConditionVertexType.Ptr (children.ToArray()) + | Slice(t, listOfTuples) -> + let children = ResizeArray> [||] + handleTerm t children + + for t1, t2, t3, _ in listOfTuples do + handleTerm t1 children + handleTerm t2 children + handleTerm t3 children + + markAsVisited pathConditionVertexType.Slice (children.ToArray()) + | Ite(_) -> markAsVisited pathConditionVertexType.Ite [||] + + pathConditionDelta + +let collectGameState (basicBlocks: ResizeArray) filterStates = + 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 - - for currentBasicBlock in basicBlocks do + + let pathConditionDelta = ResizeArray() + + for currentBasicBlock in basicBlocks do let states = currentBasicBlock.AssociatedStates - |> Seq.map (fun s -> - State(s.Id, - (uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1) * 1u, - s.PathConditionSize, - 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) - ) + |> Seq.map (fun (s: IGraphTrackableState) -> + let pathCondition = s.PathCondition |> PC.toSeq + + for term in pathCondition do + pathConditionDelta.AddRange(collectPathCondition term) + + State( + s.Id, + (uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1) + * 1u, + PathConditionVertex( + id = getFirstFreePathConditionVertexId (), + pathConditionVertexType = pathConditionVertexType.PathConditionRoot, + children = [| for p in pathCondition -> pathConditionVertices.[p].Id |] + ), + 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 - ) + + s.Id) |> Array.ofSeq - + GameMapVertex( currentBasicBlock.Id, currentBasicBlock.IsGoal, - uint <| currentBasicBlock.FinalOffset - currentBasicBlock.StartOffset + 1, + uint + <| currentBasicBlock.FinalOffset - currentBasicBlock.StartOffset + 1, currentBasicBlock.IsCovered, currentBasicBlock.IsVisited, currentBasicBlock.IsTouched, currentBasicBlock.ContainsCall, currentBasicBlock.ContainsThrow, - states) + 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)) + GameMapEdge(basicBlock.Id, targetBasicBlock.Id, GameEdgeLabel(int outgoingEdges.Key)) |> edges.Add - - GameState (vertices.ToArray(), allStates |> Array.ofSeq, edges.ToArray()) - + + 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 -let dumpGameState fileForResultWithoutExtension (movedStateId:uint) = + collectGameState (ResizeArray basicBlocks) false + +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 let statesInfoToDump = collectStatesInfoToDump basicBlocks - let gameStateJson = JsonSerializer.Serialize gameState + 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 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) - \ No newline at end of file + (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.ML.GameServer/Messages.fs b/VSharp.ML.GameServer/Messages.fs index aa5fdedf4..43c60c51b 100644 --- a/VSharp.ML.GameServer/Messages.fs +++ b/VSharp.ML.GameServer/Messages.fs @@ -4,99 +4,187 @@ 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} + new(messageType, messageBody) = + { MessageBody = messageBody + MessageType = messageType } type IRawOutgoingMessageBody = interface end -type [] test -type [] error -type [] step -type [] percent -type [] basicBlockGlobalId -type [] instruction +[] +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 + | PathConditionRoot = 48 + [] -type GameOverMessageBody = - interface IRawOutgoingMessageBody - val ActualCoverage: uint - val TestsCount: uint32 - val ErrorsCount: uint32 - new (actualCoverage, testsCount, errorsCount) = {ActualCoverage = actualCoverage; TestsCount = testsCount; ErrorsCount = errorsCount} - +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 ErrorsCount: uint32 + + new(actualCoverage, testsCount, errorsCount) = + { ActualCoverage = actualCoverage + TestsCount = testsCount + ErrorsCount = errorsCount } + [] type RawOutgoingMessage = val MessageType: string val MessageBody: obj - new (messageType, messageBody) = {MessageBody = messageBody; MessageType = messageType} - -type [] stateId + + new(messageType, messageBody) = + { MessageBody = messageBody + MessageType = messageType } + +[] +type stateId [] type GameStep = - val StateId: uint - + val StateId: uint + [] - new (stateId) = {StateId = stateId} - + 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 - } + + new(graphVertexId, numOfVisits, stepWhenVisitedLastTime) = + { GraphVertexId = graphVertexId + NumOfVisits = numOfVisits + StepWhenVisitedLastTime = stepWhenVisitedLastTime } [] type State = val Id: uint val Position: uint // to basic block id - val PathConditionSize: uint + val PathCondition: PathConditionVertex val VisitedAgainVertices: uint val VisitedNotCoveredVerticesInZone: uint val VisitedNotCoveredVerticesOutOfZone: uint val StepWhenMovedLastTime: uint val InstructionsVisitedInCurrentBlock: uint val History: array - val Children: array> - new(id, - position, - pathConditionSize, - visitedAgainVertices, - visitedNotCoveredVerticesInZone, - visitedNotCoveredVerticesOutOfZone, - stepWhenMovedLastTime, - instructionsVisitedInCurrentBlock, - history, - children) = - { - Id = id - Position = position - PathConditionSize = pathConditionSize - VisitedAgainVertices = visitedAgainVertices - VisitedNotCoveredVerticesInZone = visitedNotCoveredVerticesInZone - VisitedNotCoveredVerticesOutOfZone = visitedNotCoveredVerticesOutOfZone - StepWhenMovedLastTime = stepWhenMovedLastTime - InstructionsVisitedInCurrentBlock = instructionsVisitedInCurrentBlock - History = history - Children = children - } - -[] + 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 @@ -107,98 +195,129 @@ type GameMapVertex = 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 - } + + 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} + 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} - + + 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, map) = {GraphVertices = graphVertices; States = states; Map = map} - + + 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" + 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 + + 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 - "}" - } + seq { + "digraph g{" + yield! vertices + yield! edges + "}" + } + System.IO.File.WriteAllLines(file, dot) - -type [] coverageReward -type [] visitedInstructionsReward -type [] maxPossibleReward - + +[] +type coverageReward + +[] +type visitedInstructionsReward + +[] +type maxPossibleReward + [] type MoveReward = val ForCoverage: uint val ForVisitedInstructions: uint - new (forCoverage, forVisitedInstructions) = {ForCoverage = forCoverage; ForVisitedInstructions = forVisitedInstructions} + + 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} + + new(forMove, maxPossibleReward) = + { ForMove = forMove + MaxPossibleReward = maxPossibleReward } + + new(forCoverage, forVisitedInstructions, maxPossibleReward) = + { ForMove = MoveReward(forCoverage, forVisitedInstructions) + MaxPossibleReward = maxPossibleReward } type Feedback = | MoveReward of Reward @@ -209,83 +328,80 @@ type Feedback = type GameMap = val StepsToPlay: uint val StepsToStart: uint + [)>] - val DefaultSearcher: searcher + 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, 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 - } + 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 ServerErrorMessageBody = + interface IRawOutgoingMessageBody + val ErrorMessage: string + new(errorMessage) = { ErrorMessage = errorMessage } [] - type IncorrectPredictedStateIdMessageBody = - interface IRawOutgoingMessageBody - val StateId: uint - new (stateId) = {StateId = stateId} - +type IncorrectPredictedStateIdMessageBody = + interface IRawOutgoingMessageBody + val StateId: uint + new(stateId) = { StateId = stateId } + type OutgoingMessage = - | GameOver of uint*uint32*uint32 + | GameOver of uint * uint32 * uint32 | MoveReward of Reward | IncorrectPredictedStateId of uint | ReadyForNextStep of GameState | ServerError of string - -let (|MsgTypeStart|MsgTypeStep|MsgStop|) (str: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 + + 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 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)) + | MsgTypeStart -> Start(JsonSerializer.Deserialize rawInputMessage.MessageBody) + | MsgTypeStep -> Step(JsonSerializer.Deserialize(rawInputMessage.MessageBody)) -let serializeOutgoingMessage (message:OutgoingMessage) = +let serializeOutgoingMessage (message: OutgoingMessage) = match message with - | GameOver (actualCoverage,testsCount, errorsCount) -> RawOutgoingMessage("GameOver", box (GameOverMessageBody (actualCoverage, testsCount, errorsCount))) + | GameOver(actualCoverage, testsCount, errorsCount) -> + RawOutgoingMessage("GameOver", box (GameOverMessageBody(actualCoverage, testsCount, errorsCount))) | MoveReward reward -> RawOutgoingMessage("MoveReward", reward) - | IncorrectPredictedStateId stateId -> RawOutgoingMessage("IncorrectPredictedStateId", IncorrectPredictedStateIdMessageBody stateId) + | IncorrectPredictedStateId stateId -> + RawOutgoingMessage("IncorrectPredictedStateId", IncorrectPredictedStateIdMessageBody stateId) | ReadyForNextStep state -> RawOutgoingMessage("ReadyForNextStep", state) | ServerError errorMessage -> RawOutgoingMessage("ServerError", ServerErrorMessageBody errorMessage) |> JsonSerializer.Serialize - - - \ No newline at end of file From 64b5bf5eebf8d29571d7d4942f987c2f077a6024 Mon Sep 17 00:00:00 2001 From: Anya497 Date: Wed, 19 Mar 2025 14:16:00 +0300 Subject: [PATCH 6/8] Reset dictionary with path condition vertices. Refactor. --- VSharp.ML.GameServer.Runner/Main.fs | 166 +++++++++++++++------------- 1 file changed, 88 insertions(+), 78 deletions(-) diff --git a/VSharp.ML.GameServer.Runner/Main.fs b/VSharp.ML.GameServer.Runner/Main.fs index 1ae0927da..17ba5e6b7 100644 --- a/VSharp.ML.GameServer.Runner/Main.fs +++ b/VSharp.ML.GameServer.Runner/Main.fs @@ -23,22 +23,22 @@ type ExplorationResult = val TestsCount: uint val ErrorsCount: uint val StepsCount: uint + new(actualCoverage, testsCount, errorsCount, stepsCount) = - { - ActualCoverage = actualCoverage - TestsCount = testsCount - ErrorsCount = errorsCount - StepsCount = stepsCount - } + { ActualCoverage = actualCoverage + TestsCount = testsCount + ErrorsCount = errorsCount + StepsCount = stepsCount } type Mode = | Server = 0 | Generator = 1 + type CliArguments = | [] Port of int | [] DatasetBasePath of string | [] DatasetDescription of string - | [] Mode of Mode + | [] Mode of Mode | [] OutFolder of string | [] StepsToSerialize of uint | [] UseGPU @@ -62,21 +62,21 @@ type CliArguments = 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 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 exploredMethodInfo = AssemblyManager.NormalizeMethod method + let status, actualCoverage, message = - VSharp.Test.TestResultChecker.Check (testsDir, exploredMethodInfo :?> MethodInfo, _expectedCoverage) + VSharp.Test.TestResultChecker.Check(testsDir, exploredMethodInfo :?> MethodInfo, _expectedCoverage) + printfn $"Actual coverage for {gameMap.MapName}: {actualCoverage}" + if actualCoverage < 0 then 0u else @@ -85,7 +85,7 @@ let explore (gameMap: GameMap) options = printfn $"Coverage checking problem:{e.Message} \n {e.StackTrace}" 0u - ExplorationResult ( + ExplorationResult( actualCoverage, statistics.TestsCount * 1u, statistics.ErrorsCount * 1u, @@ -94,11 +94,12 @@ let explore (gameMap: GameMap) options = let loadGameMaps (datasetDescriptionFilePath: string) = - let jsonString = - File.ReadAllText datasetDescriptionFilePath - let maps = ResizeArray () + let jsonString = File.ReadAllText datasetDescriptionFilePath + let maps = ResizeArray() + for map in System.Text.Json.JsonSerializer.Deserialize jsonString do maps.Add map + maps let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) = @@ -111,6 +112,7 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) = serializeOutgoingMessage message |> System.Text.Encoding.UTF8.GetBytes |> ByteSegment + webSocket.send Text byteResponse true let oracle = @@ -123,17 +125,20 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) = | Feedback.ServerError s -> OutgoingMessage.ServerError s | Feedback.MoveReward reward -> OutgoingMessage.MoveReward reward | Feedback.IncorrectPredictedStateId i -> OutgoingMessage.IncorrectPredictedStateId i + do! sendResponse message } + match Async.RunSynchronously res with - | Choice1Of2 () -> () + | 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") + let file = Path.Join("dot", $"{cnt}.dot") gameState.ToDot file drawHistory cnt <- cnt + 1u //toDot false @@ -141,48 +146,54 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) = socket { do! sendResponse (ReadyForNextStep gameState) let! msg = webSocket.read () + let res = match msg with | (Text, data, true) -> let msg = deserializeInputMessage data + match msg with | Step stepParams -> (stepParams.StateId) | _ -> failwithf $"Unexpected message: %A{msg}" | _ -> failwithf $"Unexpected message: %A{msg}" + return res } + match Async.RunSynchronously res with | Choice1Of2 i -> i | Choice2Of2 error -> failwithf $"Error: %A{error}" - Oracle (predict, feedback) + 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 = - { - stepsToSwitchToAI = stepsToStart - stepsToPlay = stepsToPlay - defaultSearchStrategy = - match gameMap.DefaultSearcher with - | searcher.BFS -> BFSMode - | searcher.DFS -> DFSMode - | x -> failwithf $"Unexpected searcher {x}. Use DFS or BFS for now." - serializeSteps = false - mapName = gameMap.MapName - oracle = Some oracle - } + { stepsToSwitchToAI = stepsToStart + stepsToPlay = stepsToPlay + defaultSearchStrategy = + match gameMap.DefaultSearcher with + | searcher.BFS -> BFSMode + | searcher.DFS -> DFSMode + | x -> failwithf $"Unexpected searcher {x}. Use DFS or BFS for now." + serializeSteps = false + mapName = gameMap.MapName + oracle = Some oracle } + let options = - VSharpOptions ( + VSharpOptions( timeout = 15 * 60, outputDirectory = outputDirectory, searchStrategy = SearchStrategy.AI, @@ -190,20 +201,23 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) = stepsLimit = uint (stepsToPlay + stepsToStart), solverTimeout = 2 ) - let explorationResult = - explore gameMap options + + let explorationResult = explore gameMap options Application.reset () - API.Reset () - HashMap.hashMap.Clear () + API.Reset() + HashMap.hashMap.Clear() + Serializer.pathConditionVertices.Clear() + do! sendResponse ( - GameOver ( + GameOver( explorationResult.ActualCoverage, explorationResult.TestsCount, explorationResult.ErrorsCount ) ) + printfn $"Finish map {gameMap.MapName}, port {port}" | x -> failwithf $"Unexpected message: %A{x}" @@ -215,36 +229,33 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) = } let app port outputDirectory : WebPart = - choose - [ - path "/gameServer" >=> handShake (ws port outputDirectory) - ] + choose [ path "/gameServer" >=> handShake (ws port outputDirectory) ] 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 ( + GameMap( map.StepsToPlay, map.StepsToStart, - Path.Combine (datasetBasePath, map.AssemblyFullName), + Path.Combine(datasetBasePath, map.AssemblyFullName), map.DefaultSearcher, map.NameOfObjectToCover, map.MapName ) + let aiTrainingOptions = - { - stepsToSwitchToAI = 0u - stepsToPlay = 0u - defaultSearchStrategy = searchMode.BFSMode - serializeSteps = true - mapName = map.MapName - oracle = None - } + { stepsToSwitchToAI = 0u + stepsToPlay = 0u + defaultSearchStrategy = searchMode.BFSMode + serializeSteps = true + mapName = map.MapName + oracle = None } let options = - VSharpOptions ( + VSharpOptions( timeout = 5 * 60, outputDirectory = outputDirectory, searchStrategy = SearchStrategy.ExecutionTreeContributedCoverage, @@ -252,28 +263,34 @@ let generateDataForPretraining outputDirectory datasetBasePath (maps: ResizeArra solverTimeout = 2, aiAgentTrainingOptions = aiTrainingOptions ) + let folderForResults = Serializer.getFolderToStoreSerializationResult outputDirectory map.MapName + if Directory.Exists folderForResults then - Directory.Delete (folderForResults, true) - let _ = - Directory.CreateDirectory folderForResults + Directory.Delete(folderForResults, true) + + let _ = Directory.CreateDirectory folderForResults let explorationResult = explore map options - File.WriteAllText ( - Path.Join (folderForResults, "result"), + + File.WriteAllText( + Path.Join(folderForResults, "result"), $"{explorationResult.ActualCoverage} {explorationResult.TestsCount} {explorationResult.StepsCount} {explorationResult.ErrorsCount}" ) + printfn $"Generation for {map.MapName} finished with coverage {explorationResult.ActualCoverage}, tests {explorationResult.TestsCount}, steps {explorationResult.StepsCount},errors {explorationResult.ErrorsCount}." + Application.reset () - API.Reset () - HashMap.hashMap.Clear () + API.Reset() + HashMap.hashMap.Clear() [] let main args = let parser = - ArgumentParser.Create (programName = "VSharp.ML.GameServer.Runner.exe") + ArgumentParser.Create(programName = "VSharp.ML.GameServer.Runner.exe") + let args = parser.Parse args let mode = args.GetResult <@ Mode @> @@ -298,19 +315,16 @@ let main args = | Some steps -> steps | None -> 500u - let useGPU = - (args.TryGetResult <@ UseGPU @>).IsSome + let useGPU = (args.TryGetResult <@ UseGPU @>).IsSome - let optimize = - (args.TryGetResult <@ Optimize @>).IsSome + let optimize = (args.TryGetResult <@ Optimize @>).IsSome - let outputDirectory = - Path.Combine (Directory.GetCurrentDirectory (), string port) + let outputDirectory = Path.Combine(Directory.GetCurrentDirectory(), string port) if Directory.Exists outputDirectory then - Directory.Delete (outputDirectory, true) - let testsDirInfo = - Directory.CreateDirectory outputDirectory + Directory.Delete(outputDirectory, true) + + let testsDirInfo = Directory.CreateDirectory outputDirectory printfn $"outputDir: {outputDirectory}" match mode with @@ -319,11 +333,7 @@ let main args = startWebServer { defaultConfig with logger = Targets.create Verbose [||] - bindings = - [ - HttpBinding.createSimple HTTP "127.0.0.1" port - ] - } + bindings = [ HttpBinding.createSimple HTTP "127.0.0.1" port ] } (app port outputDirectory) with e -> printfn $"Failed on port {port}" From b3621060175b51040b28d029b7a5072232176f0a Mon Sep 17 00:00:00 2001 From: Anya497 Date: Wed, 19 Mar 2025 14:38:42 +0300 Subject: [PATCH 7/8] Update path condition. Refactor. --- VSharp.Explorer/AISearcher.fs | 297 +++++++++++++++++----------------- 1 file changed, 145 insertions(+), 152 deletions(-) diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index e1a31ab0e..b02f9a423 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -17,49 +17,51 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option 0u | Some options -> options.stepsToPlay - let mutable lastCollectedStatistics = - Statistics () + let mutable lastCollectedStatistics = Statistics() let mutable defaultSearcherSteps = 0u - let mutable (gameState: Option) = - None - let mutable useDefaultSearcher = - stepsToSwitchToAI > 0u + let mutable (gameState: Option) = None + let mutable useDefaultSearcher = stepsToSwitchToAI > 0u let mutable afterFirstAIPeek = false - let mutable incorrectPredictedStateId = - false + let mutable incorrectPredictedStateId = false + let defaultSearcher = match aiAgentTrainingOptions with - | None -> BFSSearcher () :> IForwardSearcher + | None -> BFSSearcher() :> IForwardSearcher | Some options -> match options.defaultSearchStrategy with - | BFSMode -> BFSSearcher () :> IForwardSearcher - | DFSMode -> DFSSearcher () :> IForwardSearcher + | BFSMode -> BFSSearcher() :> IForwardSearcher + | DFSMode -> DFSSearcher() :> IForwardSearcher | x -> failwithf $"Unexpected default searcher {x}. DFS and BFS supported for now." + let mutable stepsPlayed = 0u + let isInAIMode () = (not useDefaultSearcher) && afterFirstAIPeek - let q = ResizeArray<_> () - let availableStates = HashSet<_> () + + let q = ResizeArray<_>() + let availableStates = HashSet<_>() + let updateGameState (delta: GameState) = match gameState with | None -> gameState <- Some delta | Some s -> - let updatedBasicBlocks = - delta.GraphVertices |> Array.map (fun b -> b.Id) |> HashSet - let updatedStates = - delta.States |> Array.map (fun s -> s.Id) |> HashSet + let updatedBasicBlocks = delta.GraphVertices |> Array.map (fun b -> b.Id) |> HashSet + let updatedStates = delta.States |> Array.map (fun s -> s.Id) |> HashSet + let vertices = s.GraphVertices |> Array.filter (fun v -> updatedBasicBlocks.Contains v.Id |> not) |> ResizeArray<_> + vertices.AddRange delta.GraphVertices + let edges = s.Map |> Array.filter (fun e -> updatedBasicBlocks.Contains e.VertexFrom |> not) |> ResizeArray<_> + edges.AddRange delta.Map - let activeStates = - vertices |> Seq.collect (fun v -> v.States) |> HashSet + let activeStates = vertices |> Seq.collect (fun v -> v.States) |> HashSet let states = let part1 = @@ -69,12 +71,12 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option Array.map (fun s -> - State ( + State( s.Id, s.Position, - s.PathConditionSize, + s.PathCondition, s.VisitedAgainVertices, s.VisitedNotCoveredVerticesInZone, s.VisitedNotCoveredVerticesOutOfZone, @@ -82,69 +84,80 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option Array.filter activeStates.Contains - ) - ) + )) + + let pathConditionVertices = + ResizeArray s.PathConditionVertices + + pathConditionVertices.AddRange delta.PathConditionVertices - gameState <- Some <| GameState (vertices.ToArray (), states, edges.ToArray ()) + gameState <- + Some + <| GameState(vertices.ToArray(), states, pathConditionVertices.ToArray(), edges.ToArray()) let init states = q.AddRange states defaultSearcher.Init q states |> Seq.iter (availableStates.Add >> ignore) + let reset () = - defaultSearcher.Reset () + defaultSearcher.Reset() defaultSearcherSteps <- 0u - lastCollectedStatistics <- Statistics () + lastCollectedStatistics <- Statistics() gameState <- None afterFirstAIPeek <- false incorrectPredictedStateId <- false useDefaultSearcher <- stepsToSwitchToAI > 0u - q.Clear () - availableStates.Clear () - let update (parent, newSates) = + q.Clear() + availableStates.Clear() + + let update (parent, newStates) = if useDefaultSearcher then - defaultSearcher.Update (parent, newSates) - newSates |> Seq.iter (availableStates.Add >> ignore) + 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 inTrainMode = - aiAgentTrainingOptions.IsSome + let inTrainMode = aiAgentTrainingOptions.IsSome let pick selector = if useDefaultSearcher then defaultSearcherSteps <- defaultSearcherSteps + 1u + if Seq.length availableStates > 0 then - let gameStateDelta = - collectGameStateDelta () + let gameStateDelta = collectGameStateDelta () updateGameState gameStateDelta - let statistics = - computeStatistics gameState.Value - Application.applicationGraphDelta.Clear () + let statistics = computeStatistics gameState.Value + Application.applicationGraphDelta.Clear() lastCollectedStatistics <- statistics useDefaultSearcher <- defaultSearcherSteps < stepsToSwitchToAI - defaultSearcher.Pick () + + defaultSearcher.Pick() elif Seq.length availableStates = 0 then None elif Seq.length availableStates = 1 then - Some (Seq.head availableStates) + Some(Seq.head availableStates) else - let gameStateDelta = - collectGameStateDelta () + let gameStateDelta = collectGameStateDelta () updateGameState gameStateDelta - let statistics = - computeStatistics gameState.Value + let statistics = computeStatistics gameState.Value + if isInAIMode () then - let reward = - computeReward lastCollectedStatistics statistics - oracle.Feedback (Feedback.MoveReward reward) - Application.applicationGraphDelta.Clear () + let reward = computeReward lastCollectedStatistics statistics + oracle.Feedback(Feedback.MoveReward reward) + + Application.applicationGraphDelta.Clear() + if inTrainMode && stepsToPlay = stepsPlayed then None else @@ -153,17 +166,18 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option Seq.tryFind (fun s -> s.internalId = stateId) + let state = availableStates |> Seq.tryFind (fun s -> s.internalId = stateId) lastCollectedStatistics <- statistics stepsPlayed <- stepsPlayed + 1u + match state with | Some state -> Some state | None -> incorrectPredictedStateId <- true - oracle.Feedback (Feedback.IncorrectPredictedStateId stateId) + oracle.Feedback(Feedback.IncorrectPredictedStateId stateId) None new(pathToONNX: string, useGPU: bool, optimize: bool) = @@ -174,9 +188,9 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option, int> () - let verticesIds = - Dictionary, int> () + let stateIds = Dictionary, int>() + let verticesIds = Dictionary, int>() let networkInput = - let res = Dictionary<_, _> () + let res = Dictionary<_, _>() + let gameVertices = - let shape = - [| - int64 gameState.GraphVertices.Length - numOfVertexAttributes - |] + let shape = [| int64 gameState.GraphVertices.Length; numOfVertexAttributes |] + let attributes = Array.zeroCreate (gameState.GraphVertices.Length * numOfVertexAttributes) + for i in 0 .. gameState.GraphVertices.Length - 1 do let v = gameState.GraphVertices.[i] - verticesIds.Add (v.Id, i) + verticesIds.Add(v.Id, i) let j = i * numOfVertexAttributes attributes.[j] <- float32 <| if v.InCoverageZone then 1u else 0u attributes.[j + 1] <- float32 <| v.BasicBlockSize @@ -216,111 +226,97 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option Array.iteri (fun i e -> index[i] <- int64 verticesIds[e.VertexFrom] index[gameState.Map.Length + i] <- int64 verticesIds[e.VertexTo] - attributes[i] <- int64 e.Label.Token - ) + attributes[i] <- int64 e.Label.Token) - OrtValue.CreateTensorValueFromMemory (index, shapeOfIndex), - OrtValue.CreateTensorValueFromMemory (attributes, shapeOfAttributes) + OrtValue.CreateTensorValueFromMemory(index, shapeOfIndex), + OrtValue.CreateTensorValueFromMemory(attributes, shapeOfAttributes) let historyEdgesIndex_vertexToState, historyEdgesAttributes, parentOfEdges = - let shapeOfParentOf = - [| 2L ; numOfParentOfEdges |] - let parentOf = - Array.zeroCreate (2 * numOfParentOfEdges) - let shapeOfHistory = - [| 2L ; numOfHistoryEdges |] - let historyIndex_vertexToState = - Array.zeroCreate (2 * numOfHistoryEdges) + let shapeOfParentOf = [| 2L; numOfParentOfEdges |] + let parentOf = Array.zeroCreate (2 * numOfParentOfEdges) + let shapeOfHistory = [| 2L; numOfHistoryEdges |] + let historyIndex_vertexToState = Array.zeroCreate (2 * numOfHistoryEdges) + let shapeOfHistoryAttributes = - [| - int64 numOfHistoryEdges - int64 numOfHistoryEdgeAttributes - |] - let historyAttributes = - Array.zeroCreate (2 * numOfHistoryEdges) + [| int64 numOfHistoryEdges; int64 numOfHistoryEdgeAttributes |] + + let historyAttributes = Array.zeroCreate (2 * numOfHistoryEdges) let mutable firstFreePositionInParentsOf = 0 - let mutable firstFreePositionInHistoryIndex = - 0 - let mutable firstFreePositionInHistoryAttributes = - 0 + let mutable firstFreePositionInHistoryIndex = 0 + let mutable firstFreePositionInHistoryAttributes = 0 + gameState.States |> Array.iter (fun state -> state.Children |> Array.iteri (fun i children -> let j = firstFreePositionInParentsOf + i parentOf[j] <- int64 stateIds[state.Id] - parentOf[numOfParentOfEdges + j] <- int64 stateIds[children] - ) + parentOf[numOfParentOfEdges + j] <- int64 stateIds[children]) + firstFreePositionInParentsOf <- firstFreePositionInParentsOf + state.Children.Length + state.History |> Array.iteri (fun i historyElem -> let j = firstFreePositionInHistoryIndex + i historyIndex_vertexToState[j] <- int64 verticesIds[historyElem.GraphVertexId] historyIndex_vertexToState[numOfHistoryEdges + j] <- int64 stateIds[state.Id] - let j = - firstFreePositionInHistoryAttributes + numOfHistoryEdgeAttributes * i + let j = firstFreePositionInHistoryAttributes + numOfHistoryEdgeAttributes * i historyAttributes[j] <- int64 historyElem.NumOfVisits - historyAttributes[j + 1] <- int64 historyElem.StepWhenVisitedLastTime - ) + historyAttributes[j + 1] <- int64 historyElem.StepWhenVisitedLastTime) + firstFreePositionInHistoryIndex <- firstFreePositionInHistoryIndex + state.History.Length + firstFreePositionInHistoryAttributes <- firstFreePositionInHistoryAttributes - + numOfHistoryEdgeAttributes * state.History.Length - ) + + numOfHistoryEdgeAttributes * state.History.Length) - OrtValue.CreateTensorValueFromMemory (historyIndex_vertexToState, shapeOfHistory), - OrtValue.CreateTensorValueFromMemory (historyAttributes, shapeOfHistoryAttributes), - OrtValue.CreateTensorValueFromMemory (parentOf, shapeOfParentOf) + OrtValue.CreateTensorValueFromMemory(historyIndex_vertexToState, shapeOfHistory), + OrtValue.CreateTensorValueFromMemory(historyAttributes, shapeOfHistoryAttributes), + OrtValue.CreateTensorValueFromMemory(parentOf, shapeOfParentOf) let statePosition_stateToVertex, statePosition_vertexToState = - let data_stateToVertex = - Array.zeroCreate (2 * gameState.States.Length) - let data_vertexToState = - Array.zeroCreate (2 * gameState.States.Length) - let shape = - [| 2L ; gameState.States.Length |] + let data_stateToVertex = Array.zeroCreate (2 * gameState.States.Length) + let data_vertexToState = Array.zeroCreate (2 * gameState.States.Length) + let shape = [| 2L; gameState.States.Length |] let mutable firstFreePosition = 0 + gameState.GraphVertices |> Array.iter (fun v -> v.States @@ -332,46 +328,43 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option().ToArray () + let output = session.Run(runOptions, networkInput, session.OutputNames) + let weighedStates = output[0].GetTensorDataAsSpan().ToArray() - let id = - weighedStates |> Array.mapi (fun i v -> i, v) |> Array.maxBy snd |> fst + let id = weighedStates |> Array.mapi (fun i v -> i, v) |> Array.maxBy snd |> fst stateIds |> Seq.find (fun kvp -> kvp.Value = id) |> (fun x -> x.Key) - Oracle (predict, feedback) + Oracle(predict, feedback) - AISearcher (createOracle pathToONNX, None) + AISearcher(createOracle pathToONNX, None) interface IForwardSearcher with override x.Init states = init states - override x.Pick () = pick (always true) + override x.Pick() = pick (always true) override x.Pick selector = pick selector - override x.Update (parent, newStates) = update (parent, newStates) - override x.States () = availableStates - override x.Reset () = reset () + override x.Update(parent, newStates) = update (parent, newStates) + override x.States() = availableStates + override x.Reset() = reset () override x.Remove cilState = remove cilState override x.StatesCount = availableStates.Count From 1f6e3f0545cf8933f86d65028e7e23b3768c49fe Mon Sep 17 00:00:00 2001 From: Anya497 Date: Wed, 19 Mar 2025 14:41:05 +0300 Subject: [PATCH 8/8] Pass path condition instead its size. Make PC not internal to use its methods. --- VSharp.IL/CFG.fs | 3 ++- VSharp.SILI.Core/PathCondition.fs | 2 +- VSharp.SILI/CILState.fs | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/VSharp.IL/CFG.fs b/VSharp.IL/CFG.fs index b5b465670..6de1eb186 100644 --- a/VSharp.IL/CFG.fs +++ b/VSharp.IL/CFG.fs @@ -8,6 +8,7 @@ open System.Reflection open System.Collections.Generic open Microsoft.FSharp.Collections open VSharp +open VSharp.Core type ICallGraphNode = inherit IGraphNode @@ -519,7 +520,7 @@ and IGraphTrackableState = abstract member CodeLocation: codeLocation abstract member CallStack: list abstract member Id: uint - abstract member PathConditionSize: uint + abstract member PathCondition: pathCondition abstract member VisitedNotCoveredVerticesInZone: uint with get abstract member VisitedNotCoveredVerticesOutOfZone: uint with get abstract member VisitedAgainVertices: uint with get 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/CILState.fs b/VSharp.SILI/CILState.fs index 44a90cb96..a8ef1cdeb 100644 --- a/VSharp.SILI/CILState.fs +++ b/VSharp.SILI/CILState.fs @@ -544,7 +544,7 @@ module CilState = 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.PathConditionSize with get () = PersistentSet.cardinality this.state.pc |> uint32 + 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