Skip to content

Path Condition to ONNX interface #95

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 8, 2025
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
73 changes: 68 additions & 5 deletions VSharp.Explorer/AISearcher.fs
Original file line number Diff line number Diff line change
@@ -213,7 +213,8 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
aiAgentTrainingModelOptions: Option<AIAgentTrainingModelOptions>
) =
let numOfVertexAttributes = 7
let numOfStateAttributes = 7
let numOfStateAttributes = 6
let numOfPathConditionVertexAttributes = 49
let numOfHistoryEdgeAttributes = 2


@@ -248,10 +249,33 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
let gameState = currentGameState.Value
let stateIds = Dictionary<uint<stateId>, int>()
let verticesIds = Dictionary<uint<basicBlockGlobalId>, int>()
let pathConditionVerticesIds = Dictionary<uint<pathConditionVertexId>, 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 |]

@@ -285,8 +309,6 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
stateIds.Add(v.Id, i)
let j = i * numOfStateAttributes
attributes.[j] <- float32 v.Position
// TODO: Support path condition
// attributes.[j + 1] <- float32 v.PathConditionSize
attributes.[j + 2] <- float32 v.VisitedAgainVertices
attributes.[j + 3] <- float32 v.VisitedNotCoveredVerticesInZone
attributes.[j + 4] <- float32 v.VisitedNotCoveredVerticesOutOfZone
@@ -295,6 +317,31 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai

OrtValue.CreateTensorValueFromMemory(attributes, shape), numOfParentOfEdges, 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] <- pathConditionVerticesIds.[v.Id]

index.[firstFreePositionOfIndex + 2 * numOfPcToPcEdges] <-
pathConditionVerticesIds.[child]

firstFreePositionOfIndex <- firstFreePositionOfIndex + 1
// from child to vertex
index.[firstFreePositionOfIndex] <- pathConditionVerticesIds.[child]

index.[firstFreePositionOfIndex + 2 * numOfPcToPcEdges] <-
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 |]
@@ -310,11 +357,13 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
OrtValue.CreateTensorValueFromMemory(index, shapeOfIndex),
OrtValue.CreateTensorValueFromMemory(attributes, shapeOfAttributes)

let historyEdgesIndex_vertexToState, historyEdgesAttributes, parentOfEdges =
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; gameState.States.Length |]
let index_pcToState = Array.zeroCreate (2 * gameState.States.Length)

let shapeOfHistoryAttributes =
[| int64 numOfHistoryEdges; int64 numOfHistoryEdgeAttributes |]
@@ -323,6 +372,7 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
let mutable firstFreePositionInParentsOf = 0
let mutable firstFreePositionInHistoryIndex = 0
let mutable firstFreePositionInHistoryAttributes = 0
let mutable firstFreePositionInPcToState = 0

gameState.States
|> Array.iter (fun state ->
@@ -334,6 +384,14 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai

firstFreePositionInParentsOf <- firstFreePositionInParentsOf + state.Children.Length

index_pcToState.[firstFreePositionInPcToState] <-
int64 pathConditionVerticesIds[state.PathCondition.Id]

index_pcToState.[firstFreePositionInPcToState + gameState.States.Length] <-
int64 stateIds[state.Id]

firstFreePositionInPcToState <- firstFreePositionInPcToState + 1

state.History
|> Array.iteri (fun i historyElem ->
let j = firstFreePositionInHistoryIndex + i
@@ -352,7 +410,8 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai

OrtValue.CreateTensorValueFromMemory(historyIndex_vertexToState, shapeOfHistory),
OrtValue.CreateTensorValueFromMemory(historyAttributes, shapeOfHistoryAttributes),
OrtValue.CreateTensorValueFromMemory(parentOf, shapeOfParentOf)
OrtValue.CreateTensorValueFromMemory(parentOf, shapeOfParentOf),
OrtValue.CreateTensorValueFromMemory(index_pcToState, shapeOfPcToState)

let statePosition_stateToVertex, statePosition_vertexToState =
let data_stateToVertex = Array.zeroCreate (2 * gameState.States.Length)
@@ -380,6 +439,7 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai

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)
@@ -390,6 +450,9 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
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)

Unchanged files with check annotations Beta

var methodName = t.Last();
var x = type.GetMethods(Reflection.allBindingFlags);
method ??= x
.Where(m => type.FullName.Split('.').Last().Contains(className) && m.Name.Contains(methodName))

Check warning on line 96 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Dereference of a possibly null reference.

Check warning on line 96 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Dereference of a possibly null reference.
.MinBy(m => m.Name.Length);
if (method != null)
break;
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
parseResult.GetValueForOption(pathToModelOption),

Check warning on line 533 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.EntryPointHandler(FileInfo assemblyPath, string[]? args, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.

Check warning on line 533 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.EntryPointHandler(FileInfo assemblyPath, string[]? args, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
parseResult.GetValueForOption(pathToModelOption),

Check warning on line 597 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.AllPublicMethodsHandler(FileInfo assemblyPath, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.

Check warning on line 597 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.AllPublicMethodsHandler(FileInfo assemblyPath, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
parseResult.GetValueForOption(pathToModelOption),

Check warning on line 627 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.PublicMethodsOfTypeHandler(FileInfo assemblyPath, string typeName, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.

Check warning on line 627 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.PublicMethodsOfTypeHandler(FileInfo assemblyPath, string typeName, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
pathToModel,

Check warning on line 660 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.SpecificMethodHandler(FileInfo assemblyPath, string methodName, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, bool checkCoverage, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.

Check warning on line 660 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.SpecificMethodHandler(FileInfo assemblyPath, string methodName, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, bool checkCoverage, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
public readonly bool ReleaseBranches = DefaultReleaseBranches;
public readonly int RandomSeed = DefaultRandomSeed;
public readonly uint StepsLimit = DefaultStepsLimit;
public readonly AIOptions? AIOptions = null;

Check warning on line 116 in VSharp.API/VSharpOptions.cs

GitHub Actions / build

The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.

Check warning on line 116 in VSharp.API/VSharpOptions.cs

GitHub Actions / build

The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
public readonly string PathToModel = DefaultPathToModel;
public readonly bool UseGPU = false;
public readonly bool Optimize = false;
bool releaseBranches = DefaultReleaseBranches,
int randomSeed = DefaultRandomSeed,
uint stepsLimit = DefaultStepsLimit,
AIOptions? aiOptions = null,

Check warning on line 153 in VSharp.API/VSharpOptions.cs

GitHub Actions / build

The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.

Check warning on line 153 in VSharp.API/VSharpOptions.cs

GitHub Actions / build

The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
string pathToModel = DefaultPathToModel,
bool useGPU = false,
bool optimize = false)
// TODO: merging!
type memoryRegion<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> with
override x.ToString() = MemoryRegion.toString "" x

Check warning on line 788 in VSharp.SILI.Core/MemoryRegion.fs

GitHub Actions / build

Override implementations in augmentations are now deprecated. Override implementations should be given as part of the initial declaration of a type.

Check warning on line 788 in VSharp.SILI.Core/MemoryRegion.fs

GitHub Actions / build

Override implementations in augmentations are now deprecated. Override implementations should be given as part of the initial declaration of a type.
type setKeyWrapper<'key when 'key : equality> =
{key : 'key}
returnType = types.Last();
}
var declaringType = mi.DeclaringType;
return declaringType.GetProperty(propertyName, Reflection.allBindingFlags, null, returnType, argumentTypes, null) != null;

Check warning on line 152 in VSharp.TestRenderer/CodeRenderer.cs

GitHub Actions / build

Dereference of a possibly null reference.

Check warning on line 152 in VSharp.TestRenderer/CodeRenderer.cs

GitHub Actions / build

Dereference of a possibly null reference.
}
propertyName = string.Empty;
// NOTE: first 16 bytes contain array meta info
public const int ArrayElementsOffset = 16;
public static readonly int StringElementsOffset = RuntimeHelpers.OffsetToStringData;

Check warning on line 56 in VSharp.CSharpUtils/LayoutUtils.cs

GitHub Actions / build

'RuntimeHelpers.OffsetToStringData' is obsolete: 'OffsetToStringData has been deprecated. Use string.GetPinnableReference() instead.'

Check warning on line 56 in VSharp.CSharpUtils/LayoutUtils.cs

GitHub Actions / build

'RuntimeHelpers.OffsetToStringData' is obsolete: 'OffsetToStringData has been deprecated. Use string.GetPinnableReference() instead.'
}
}