From 95c09eceb7f30f0946a7d1ed660b0993602c4201 Mon Sep 17 00:00:00 2001 From: Gitubrr Date: Fri, 19 Dec 2025 21:49:05 +0300 Subject: [PATCH 1/5] removing pc-root from the states --- VSharp.Explorer/AISearcher.fs | 2 +- VSharp.IL/Serializer.fs | 18 ++++++++++-------- VSharp.ML.GameServer/Messages.fs | 2 +- 3 files changed, 12 insertions(+), 10 deletions(-) diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index 49a450b38..a4db61826 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -384,7 +384,7 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option) filterStates process for term in pathCondition do pathConditionDelta.AddRange(collectPathCondition term termsWithId processedPathConditionVertices) - let pathConditionRoot = - PathConditionVertex( - id = getFirstFreePathConditionVertexId (), - pathConditionVertexType = pathConditionVertexType.PathConditionRoot, - children = [| for p in pathCondition -> termsWithId.[p] |] - ) + // let pathConditionRoot = + // PathConditionVertex( + // id = getFirstFreePathConditionVertexId (), + // pathConditionVertexType = pathConditionVertexType.PathConditionRoot, + // children = [| for p in pathCondition -> termsWithId.[p] |] + // ) - pathConditionDelta.Add pathConditionRoot + // pathConditionDelta.Add pathConditionRoot + + let children = [| for p in pathCondition -> termsWithId.[p] |] State( s.Id, (uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1) * 1u, - pathConditionRoot, + children, s.VisitedAgainVertices, s.VisitedNotCoveredVerticesInZone, s.VisitedNotCoveredVerticesOutOfZone, diff --git a/VSharp.ML.GameServer/Messages.fs b/VSharp.ML.GameServer/Messages.fs index 7f13570f7..e748be497 100644 --- a/VSharp.ML.GameServer/Messages.fs +++ b/VSharp.ML.GameServer/Messages.fs @@ -153,7 +153,7 @@ type StateHistoryElem = type State = val Id: uint val Position: uint // to basic block id - val PathCondition: PathConditionVertex + val PathCondition: uint array val VisitedAgainVertices: uint val VisitedNotCoveredVerticesInZone: uint val VisitedNotCoveredVerticesOutOfZone: uint From c5482cbd0c6259329ec3188fc71be82fbdc5ae11 Mon Sep 17 00:00:00 2001 From: Gitubrr Date: Fri, 19 Dec 2025 21:52:41 +0300 Subject: [PATCH 2/5] deleted commemts --- VSharp.IL/Serializer.fs | 9 --------- 1 file changed, 9 deletions(-) diff --git a/VSharp.IL/Serializer.fs b/VSharp.IL/Serializer.fs index 95b646c8e..6f335d456 100644 --- a/VSharp.IL/Serializer.fs +++ b/VSharp.IL/Serializer.fs @@ -495,15 +495,6 @@ let collectGameState (basicBlocks: ResizeArray) filterStates process for term in pathCondition do pathConditionDelta.AddRange(collectPathCondition term termsWithId processedPathConditionVertices) - // let pathConditionRoot = - // PathConditionVertex( - // id = getFirstFreePathConditionVertexId (), - // pathConditionVertexType = pathConditionVertexType.PathConditionRoot, - // children = [| for p in pathCondition -> termsWithId.[p] |] - // ) - - // pathConditionDelta.Add pathConditionRoot - let children = [| for p in pathCondition -> termsWithId.[p] |] State( From 5d0edb0fe03dd47b40b83e684bd1d4bd52ea06de Mon Sep 17 00:00:00 2001 From: Gitubrr Date: Wed, 24 Dec 2025 01:51:48 +0300 Subject: [PATCH 3/5] made egjes between states and pc --- VSharp.Explorer/AISearcher.fs | 22 +++++++++++----------- VSharp.IL/Serializer.fs | 4 ++-- VSharp.ML.GameServer/Messages.fs | 3 +-- 3 files changed, 14 insertions(+), 15 deletions(-) diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index a4db61826..b27cb5f9f 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -361,8 +361,12 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option Array.sumBy(fun s -> s.PathCondition.Length) + let shapeOfPcToState = [| 2L; pathConditionNum |] + let index_pcToState = Array.zeroCreate (2 * pathConditionNum) let shapeOfHistoryAttributes = [| int64 numOfHistoryEdges; int64 numOfHistoryEdgeAttributes |] @@ -381,15 +385,11 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option Array.iteri (fun i pcId -> + let j = firstFreePositionInPcToState + i + index_pcToState[j] <- int64 pathConditionVerticesIds[pcId] + index_pcToState[numOfParentOfEdges + j] <- int64 stateIds[state.Id]) state.History |> Array.iteri (fun i historyElem -> diff --git a/VSharp.IL/Serializer.fs b/VSharp.IL/Serializer.fs index 6f335d456..9b406a63a 100644 --- a/VSharp.IL/Serializer.fs +++ b/VSharp.IL/Serializer.fs @@ -495,13 +495,13 @@ let collectGameState (basicBlocks: ResizeArray) filterStates process for term in pathCondition do pathConditionDelta.AddRange(collectPathCondition term termsWithId processedPathConditionVertices) - let children = [| for p in pathCondition -> termsWithId.[p] |] + let pathConditionId = [| for p in pathCondition -> termsWithId.[p] |] State( s.Id, (uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1) * 1u, - children, + pathConditionId, s.VisitedAgainVertices, s.VisitedNotCoveredVerticesInZone, s.VisitedNotCoveredVerticesOutOfZone, diff --git a/VSharp.ML.GameServer/Messages.fs b/VSharp.ML.GameServer/Messages.fs index e748be497..d85a49f0c 100644 --- a/VSharp.ML.GameServer/Messages.fs +++ b/VSharp.ML.GameServer/Messages.fs @@ -72,7 +72,6 @@ type pathConditionVertexType = | StandardFunctionApplication = 45 | Cast = 46 | Combine = 47 - | PathConditionRoot = 48 [] @@ -153,7 +152,7 @@ type StateHistoryElem = type State = val Id: uint val Position: uint // to basic block id - val PathCondition: uint array + val PathCondition: array> val VisitedAgainVertices: uint val VisitedNotCoveredVerticesInZone: uint val VisitedNotCoveredVerticesOutOfZone: uint From 31eb222743463f5e2f0487a7460c6dd7bcee2b50 Mon Sep 17 00:00:00 2001 From: Gitubrr Date: Wed, 24 Dec 2025 17:07:46 +0300 Subject: [PATCH 4/5] returned counters --- VSharp.Explorer/AISearcher.fs | 4 ++++ VSharp.IL/Serializer.fs | 4 ++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index b27cb5f9f..7b45fb319 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -385,11 +385,15 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option Array.iteri (fun i pcId -> let j = firstFreePositionInPcToState + i index_pcToState[j] <- int64 pathConditionVerticesIds[pcId] index_pcToState[numOfParentOfEdges + j] <- int64 stateIds[state.Id]) + + firstFreePositionInPcToState <- firstFreePositionInPcToState + 1 state.History |> Array.iteri (fun i historyElem -> diff --git a/VSharp.IL/Serializer.fs b/VSharp.IL/Serializer.fs index 9b406a63a..9a7857b6e 100644 --- a/VSharp.IL/Serializer.fs +++ b/VSharp.IL/Serializer.fs @@ -495,13 +495,13 @@ let collectGameState (basicBlocks: ResizeArray) filterStates process for term in pathCondition do pathConditionDelta.AddRange(collectPathCondition term termsWithId processedPathConditionVertices) - let pathConditionId = [| for p in pathCondition -> termsWithId.[p] |] + let pathCondition = [| for p in pathCondition -> termsWithId.[p] |] State( s.Id, (uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1) * 1u, - pathConditionId, + pathCondition, s.VisitedAgainVertices, s.VisitedNotCoveredVerticesInZone, s.VisitedNotCoveredVerticesOutOfZone, From cbaf95aa283a864a33742f7ac037edaec9c0da66 Mon Sep 17 00:00:00 2001 From: Gitubrr Date: Thu, 25 Dec 2025 07:58:31 +0300 Subject: [PATCH 5/5] fixed indexes --- VSharp.Explorer/AISearcher.fs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index 7b45fb319..3a7d893fb 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -393,7 +393,7 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option Array.iteri (fun i historyElem ->