Skip to content

Commit

Permalink
GPU support
Browse files Browse the repository at this point in the history
  • Loading branch information
Parzival-05 committed Dec 24, 2024
1 parent 8e112ff commit fb3674a
Show file tree
Hide file tree
Showing 9 changed files with 149 additions and 44 deletions.
15 changes: 9 additions & 6 deletions VSharp.API/VSharp.cs
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ public IEnumerable<FileInfo> Results()

public static class TestGenerator
{
private class Reporter: IReporter
private class Reporter : IReporter
{
private readonly UnitTests _unitTests;
private readonly bool _isQuiet;
Expand All @@ -124,7 +124,7 @@ public Reporter(UnitTests unitTests, bool isQuiet)

public void ReportFinished(UnitTest unitTest) => _unitTests.GenerateTest(unitTest);
public void ReportException(UnitTest unitTest) => _unitTests.GenerateError(unitTest);
public void ReportIIE(InsufficientInformationException iie) {}
public void ReportIIE(InsufficientInformationException iie) { }

public void ReportInternalFail(Method? method, Exception exn)
{
Expand Down Expand Up @@ -179,7 +179,7 @@ private static Statistics StartExploration(
explorationMode: explorationMode.NewTestCoverageMode(
coverageZone,
options.Timeout > 0 ? searchMode.NewFairMode(baseSearchMode) : baseSearchMode

),
recThreshold: options.RecursionThreshold,
solverTimeout: options.SolverTimeout,
Expand All @@ -191,8 +191,11 @@ private static Statistics StartExploration(
stopOnCoverageAchieved: 100,
randomSeed: options.RandomSeed,
stepsLimit: options.StepsLimit,
aiAgentTrainingOptions: options.AIAgentTrainingOptions == null ? FSharpOption<AIAgentTrainingOptions>.None :FSharpOption<AIAgentTrainingOptions>.Some(options.AIAgentTrainingOptions),
pathToModel: options.PathToModel == null ? FSharpOption<string>.None : FSharpOption<string>.Some(options.PathToModel));
aiAgentTrainingOptions: options.AIAgentTrainingOptions == null ? FSharpOption<AIAgentTrainingOptions>.None : FSharpOption<AIAgentTrainingOptions>.Some(options.AIAgentTrainingOptions),
pathToModel: options.PathToModel == null ? FSharpOption<string>.None : FSharpOption<string>.Some(options.PathToModel),
useGPU: options.UseGPU == null ? FSharpOption<bool>.None : FSharpOption<bool>.Some(options.UseGPU),
optimize: options.Optimize == null ? FSharpOption<bool>.None : FSharpOption<bool>.Some(options.Optimize)
);

var fuzzerOptions =
new FuzzerOptions(
Expand Down Expand Up @@ -326,7 +329,7 @@ private static int CheckCoverage(
public static Statistics Cover(MethodBase method, VSharpOptions options = new())
{
AssemblyManager.LoadCopy(method.Module.Assembly);
var methods = new List<MethodBase> {method};
var methods = new List<MethodBase> { method };
var statistics = StartExploration(methods, coverageZone.MethodZone, options);

if (options.RenderTests)
Expand Down
10 changes: 9 additions & 1 deletion VSharp.API/VSharpOptions.cs
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,8 @@ public readonly record struct VSharpOptions
public readonly uint StepsLimit = DefaultStepsLimit;
public readonly AIAgentTrainingOptions AIAgentTrainingOptions = null;
public readonly string PathToModel = DefaultPathToModel;
public readonly bool UseGPU = false;
public readonly bool Optimize = false;

/// <summary>
/// Symbolic virtual machine options.
Expand All @@ -133,6 +135,8 @@ public readonly record struct VSharpOptions
/// <param name="stepsLimit">Number of symbolic machine steps to stop execution after. Zero value means no limit.</param>
/// <param name="aiAgentTrainingOptions">Settings for AI searcher training.</param>
/// <param name="pathToModel">Path to ONNX file with model to use in AI searcher.</param>
/// <param name="useGPU">Enables GPU processing.</param>
/// <param name="optimize">Optimize.</param>
public VSharpOptions(
int timeout = DefaultTimeout,
int solverTimeout = DefaultSolverTimeout,
Expand All @@ -147,7 +151,9 @@ public VSharpOptions(
int randomSeed = DefaultRandomSeed,
uint stepsLimit = DefaultStepsLimit,
AIAgentTrainingOptions aiAgentTrainingOptions = null,
string pathToModel = DefaultPathToModel)
string pathToModel = DefaultPathToModel,
bool useGPU = false,
bool optimize = false)
{
Timeout = timeout;
SolverTimeout = solverTimeout;
Expand All @@ -163,6 +169,8 @@ public VSharpOptions(
StepsLimit = stepsLimit;
AIAgentTrainingOptions = aiAgentTrainingOptions;
PathToModel = pathToModel;
UseGPU = useGPU;
Optimize = optimize;
}

/// <summary>
Expand Down
21 changes: 17 additions & 4 deletions VSharp.Explorer/AISearcher.fs
Original file line number Diff line number Diff line change
Expand Up @@ -165,23 +165,36 @@ type internal AISearcher(oracle : Oracle, aiAgentTrainingOptions : Option<AIAgen
incorrectPredictedStateId <- true
oracle.Feedback (Feedback.IncorrectPredictedStateId stateId)
None
new(pathToONNX : string) =

new(pathToONNX : string, useGPU : bool, optimize : bool) =
let numOfVertexAttributes = 7
let numOfStateAttributes = 7
let numOfHistoryEdgeAttributes = 2

let createOracle (pathToONNX : string) =
let sessionOptions = new SessionOptions ()
sessionOptions.ExecutionMode <- ExecutionMode.ORT_PARALLEL
sessionOptions.GraphOptimizationLevel <- GraphOptimizationLevel.ORT_ENABLE_ALL
let sessionOptions =
if useGPU then
SessionOptions.MakeSessionOptionWithCudaProvider (0)
else
new SessionOptions ()

if optimize then
sessionOptions.ExecutionMode <- ExecutionMode.ORT_PARALLEL
sessionOptions.GraphOptimizationLevel <- GraphOptimizationLevel.ORT_ENABLE_ALL
else
sessionOptions.GraphOptimizationLevel <- GraphOptimizationLevel.ORT_ENABLE_BASIC

let session =
new InferenceSession (pathToONNX, sessionOptions)
let runOptions = new RunOptions ()
let feedback (x : Feedback) = ()

let predict (gameState : GameState) =
let stateIds =
Dictionary<uint<stateId>, int> ()
let verticesIds =
Dictionary<uint<basicBlockGlobalId>, int> ()

let networkInput =
let res = Dictionary<_, _> ()
let gameVertices =
Expand Down
15 changes: 14 additions & 1 deletion VSharp.Explorer/Explorer.fs
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,20 @@ type private SVMExplorer(explorationOptions : ExplorationOptions, statistics : S
| None -> failwith "Empty oracle for AI searcher."
| None ->
match options.pathToModel with
| Some s -> AISearcher s
| Some s ->
let useGPU =
if options.useGPU.IsSome then
options.useGPU.Value
else
false

let optimize =
if options.optimize.IsSome then
options.optimize.Value
else
false

AISearcher (s, useGPU, optimize)
| None -> failwith "Empty model for AI searcher."
| BFSMode -> BFSSearcher () :> IForwardSearcher
| DFSMode -> DFSSearcher () :> IForwardSearcher
Expand Down
2 changes: 2 additions & 0 deletions VSharp.Explorer/Options.fs
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,8 @@ type SVMOptions =
stepsLimit : uint
aiAgentTrainingOptions : Option<AIAgentTrainingOptions>
pathToModel : Option<string>
useGPU : Option<bool>
optimize : Option<bool>
}

type explorationModeOptions =
Expand Down
12 changes: 9 additions & 3 deletions VSharp.ML.GameServer.Runner/Main.fs
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,8 @@ type CliArguments =
| [<Unique ; Mandatory>] Mode of Mode
| [<Unique>] OutFolder of string
| [<Unique>] StepsToSerialize of uint

| [<Unique>] UseGPU
| [<Unique>] Optimize
interface IArgParserTemplate with
member s.Usage =
match s with
Expand All @@ -53,6 +54,8 @@ type CliArguments =
"Mode to run application. Server --- to train network, Generator --- to generate data for training."
| OutFolder _ -> "Folder to store generated data."
| StepsToSerialize _ -> "Maximal number of steps for each method to serialize."
| UseGPU -> "Enables GPU processing."
| Optimize -> "Optimize."

let mutable inTrainMode = true

Expand Down Expand Up @@ -290,8 +293,11 @@ let main args =
| Some steps -> steps
| None -> 500u

let outputDirectory =
Path.Combine (Directory.GetCurrentDirectory (), string port)
let useGPU = (args.TryGetResult <@ UseGPU @>).IsSome

let optimize = (args.TryGetResult <@ Optimize @>).IsSome

let outputDirectory = Path.Combine(Directory.GetCurrentDirectory(), string port)

if Directory.Exists outputDirectory then
Directory.Delete (outputDirectory, true)
Expand Down
75 changes: 58 additions & 17 deletions VSharp.Runner/RunnerProgram.cs
Original file line number Diff line number Diff line change
Expand Up @@ -90,12 +90,12 @@ public static class RunnerProgram
{
var t = methodArgumentValue.Split('.');
var className = t.Length == 1 ? "" : t[t.Length - 2];
var methodName = t.Last();
var methodName = t.Last();
var x = type.GetMethods(Reflection.allBindingFlags);
method ??= x
.Where(m => type.FullName.Split('.').Last().Contains(className) && m.Name.Contains(methodName))
.MinBy(m => m.Name.Length);
if (method != null)
if (method != null)
break;
}
catch (Exception)
Expand Down Expand Up @@ -132,7 +132,10 @@ private static void EntryPointHandler(
Verbosity verbosity,
uint recursionThreshold,
ExplorationMode explorationMode,
string pathToModel)
string pathToModel,
bool useGPU,
bool optimize
)
{
var assembly = TryLoadAssembly(assemblyPath);
var options =
Expand All @@ -145,7 +148,9 @@ private static void EntryPointHandler(
verbosity: verbosity,
recursionThreshold: recursionThreshold,
explorationMode: explorationMode,
pathToModel: pathToModel);
pathToModel: pathToModel,
useGPU: useGPU,
optimize: optimize);

if (assembly == null) return;

Expand Down Expand Up @@ -239,7 +244,9 @@ private static void AllPublicMethodsHandler(
Verbosity verbosity,
uint recursionThreshold,
ExplorationMode explorationMode,
string pathToModel)
string pathToModel,
bool useGPU,
bool optimize)
{
var assembly = TryLoadAssembly(assemblyPath);
var options =
Expand All @@ -252,7 +259,9 @@ private static void AllPublicMethodsHandler(
verbosity: verbosity,
recursionThreshold: recursionThreshold,
explorationMode: explorationMode,
pathToModel: pathToModel);
pathToModel: pathToModel,
useGPU: useGPU,
optimize: optimize);

if (assembly == null) return;

Expand All @@ -276,7 +285,9 @@ private static void PublicMethodsOfTypeHandler(
Verbosity verbosity,
uint recursionThreshold,
ExplorationMode explorationMode,
string pathToModel)
string pathToModel,
bool useGPU,
bool optimize)
{
var assembly = TryLoadAssembly(assemblyPath);
if (assembly == null) return;
Expand All @@ -298,7 +309,9 @@ private static void PublicMethodsOfTypeHandler(
verbosity: verbosity,
recursionThreshold: recursionThreshold,
explorationMode: explorationMode,
pathToModel: pathToModel);
pathToModel: pathToModel,
useGPU: useGPU,
optimize: optimize);

Statistics statistics;
if (runTests)
Expand All @@ -321,7 +334,9 @@ private static void SpecificMethodHandler(
Verbosity verbosity,
uint recursionThreshold,
ExplorationMode explorationMode,
string pathToModel)
string pathToModel,
bool useGPU,
bool optimize)
{
var assembly = TryLoadAssembly(assemblyPath);
if (assembly == null) return;
Expand Down Expand Up @@ -359,7 +374,9 @@ private static void SpecificMethodHandler(
verbosity: verbosity,
recursionThreshold: recursionThreshold,
explorationMode: explorationMode,
pathToModel: pathToModel);
pathToModel: pathToModel,
useGPU: useGPU,
optimize: optimize);

Statistics statistics;
if (runTests || checkCoverage)
Expand All @@ -381,7 +398,9 @@ private static void NamespaceHandler(
Verbosity verbosity,
uint recursionThreshold,
ExplorationMode explorationMode,
string pathToModel)
string pathToModel,
bool useGPU,
bool optimize)
{
var assembly = TryLoadAssembly(assemblyPath);
if (assembly == null) return;
Expand All @@ -403,7 +422,9 @@ private static void NamespaceHandler(
verbosity: verbosity,
recursionThreshold: recursionThreshold,
explorationMode: explorationMode,
pathToModel: pathToModel);
pathToModel: pathToModel,
useGPU: useGPU,
optimize: optimize);

Statistics statistics;
if (runTests)
Expand All @@ -427,6 +448,14 @@ public static int Main(string[] args)
aliases: new[] { "--model", "-m" },
() => defaultOptions.GetDefaultPathToModel(),
"Path to ONNX file with model for AI searcher.");
var useGPUOption = new Option<bool>(
aliases: new[] { "--gpu" },
() => false,
"Enables GPU processing.");
var optimizeOption = new Option<bool>(
aliases: new[] { "--optimize" },
() => false,
"Optimize option.");
var solverTimeoutOption = new Option<int>(
aliases: new[] { "--solver-timeout", "-st" },
() => -1,
Expand Down Expand Up @@ -473,6 +502,8 @@ public static int Main(string[] args)
rootCommand.AddGlobalOption(recursionThresholdOption);
rootCommand.AddGlobalOption(explorationModeOption);
rootCommand.AddGlobalOption(pathToModelOption);
rootCommand.AddGlobalOption(useGPUOption);
rootCommand.AddGlobalOption(optimizeOption);

var entryPointCommand =
new Command("--entry-point", "Generate test coverage from the entry point of assembly (assembly must contain Main method)");
Expand All @@ -499,7 +530,9 @@ public static int Main(string[] args)
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
parseResult.GetValueForOption(pathToModelOption)
parseResult.GetValueForOption(pathToModelOption),
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
});

Expand Down Expand Up @@ -561,7 +594,9 @@ public static int Main(string[] args)
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
parseResult.GetValueForOption(pathToModelOption)
parseResult.GetValueForOption(pathToModelOption),
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
});

Expand Down Expand Up @@ -589,7 +624,9 @@ public static int Main(string[] args)
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
parseResult.GetValueForOption(pathToModelOption)
parseResult.GetValueForOption(pathToModelOption),
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
});

Expand Down Expand Up @@ -620,7 +657,9 @@ public static int Main(string[] args)
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
pathToModel
pathToModel,
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
});

Expand Down Expand Up @@ -649,7 +688,9 @@ public static int Main(string[] args)
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
pathToModel
pathToModel,
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
});

Expand Down
Loading

0 comments on commit fb3674a

Please sign in to comment.