Skip to content

Commit d2b50a7

Browse files
Parzival-05Parzival-05
committed
GPU support
1 parent 410c7f0 commit d2b50a7

File tree

9 files changed

+145
-42
lines changed

9 files changed

+145
-42
lines changed

‎VSharp.API/VSharp.cs‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -111,7 +111,7 @@ public IEnumerable<FileInfo> Results()
111111

112112
public static class TestGenerator
113113
{
114-
private class Reporter: IReporter
114+
private class Reporter : IReporter
115115
{
116116
private readonly UnitTests _unitTests;
117117
private readonly bool _isQuiet;
@@ -124,7 +124,7 @@ public Reporter(UnitTests unitTests, bool isQuiet)
124124

125125
public void ReportFinished(UnitTest unitTest) => _unitTests.GenerateTest(unitTest);
126126
public void ReportException(UnitTest unitTest) => _unitTests.GenerateError(unitTest);
127-
public void ReportIIE(InsufficientInformationException iie) {}
127+
public void ReportIIE(InsufficientInformationException iie) { }
128128

129129
public void ReportInternalFail(Method? method, Exception exn)
130130
{
@@ -179,7 +179,7 @@ private static Statistics StartExploration(
179179
explorationMode: explorationMode.NewTestCoverageMode(
180180
coverageZone,
181181
options.Timeout > 0 ? searchMode.NewFairMode(baseSearchMode) : baseSearchMode
182-
182+
183183
),
184184
recThreshold: options.RecursionThreshold,
185185
solverTimeout: options.SolverTimeout,
@@ -191,8 +191,11 @@ private static Statistics StartExploration(
191191
stopOnCoverageAchieved: 100,
192192
randomSeed: options.RandomSeed,
193193
stepsLimit: options.StepsLimit,
194-
aiAgentTrainingOptions: options.AIAgentTrainingOptions == null ? FSharpOption<AIAgentTrainingOptions>.None :FSharpOption<AIAgentTrainingOptions>.Some(options.AIAgentTrainingOptions),
195-
pathToModel: options.PathToModel == null ? FSharpOption<string>.None : FSharpOption<string>.Some(options.PathToModel));
194+
aiAgentTrainingOptions: options.AIAgentTrainingOptions == null ? FSharpOption<AIAgentTrainingOptions>.None : FSharpOption<AIAgentTrainingOptions>.Some(options.AIAgentTrainingOptions),
195+
pathToModel: options.PathToModel == null ? FSharpOption<string>.None : FSharpOption<string>.Some(options.PathToModel),
196+
useGPU: options.UseGPU == null ? FSharpOption<bool>.None : FSharpOption<bool>.Some(options.UseGPU),
197+
optimize: options.Optimize == null ? FSharpOption<bool>.None : FSharpOption<bool>.Some(options.Optimize)
198+
);
196199

197200
var fuzzerOptions =
198201
new FuzzerOptions(
@@ -326,7 +329,7 @@ private static int CheckCoverage(
326329
public static Statistics Cover(MethodBase method, VSharpOptions options = new())
327330
{
328331
AssemblyManager.LoadCopy(method.Module.Assembly);
329-
var methods = new List<MethodBase> {method};
332+
var methods = new List<MethodBase> { method };
330333
var statistics = StartExploration(methods, coverageZone.MethodZone, options);
331334

332335
if (options.RenderTests)

‎VSharp.API/VSharpOptions.cs‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,8 @@ public readonly record struct VSharpOptions
115115
public readonly uint StepsLimit = DefaultStepsLimit;
116116
public readonly AIAgentTrainingOptions AIAgentTrainingOptions = null;
117117
public readonly string PathToModel = DefaultPathToModel;
118+
public readonly bool UseGPU = false;
119+
public readonly bool Optimize = false;
118120

119121
/// <summary>
120122
/// Symbolic virtual machine options.
@@ -133,6 +135,8 @@ public readonly record struct VSharpOptions
133135
/// <param name="stepsLimit">Number of symbolic machine steps to stop execution after. Zero value means no limit.</param>
134136
/// <param name="aiAgentTrainingOptions">Settings for AI searcher training.</param>
135137
/// <param name="pathToModel">Path to ONNX file with model to use in AI searcher.</param>
138+
/// <param name="useGPU">Enables GPU processing.</param>
139+
/// <param name="optimize">Optimize.</param>
136140
public VSharpOptions(
137141
int timeout = DefaultTimeout,
138142
int solverTimeout = DefaultSolverTimeout,
@@ -147,7 +151,9 @@ public VSharpOptions(
147151
int randomSeed = DefaultRandomSeed,
148152
uint stepsLimit = DefaultStepsLimit,
149153
AIAgentTrainingOptions aiAgentTrainingOptions = null,
150-
string pathToModel = DefaultPathToModel)
154+
string pathToModel = DefaultPathToModel,
155+
bool useGPU = false,
156+
bool optimize = false)
151157
{
152158
Timeout = timeout;
153159
SolverTimeout = solverTimeout;
@@ -163,6 +169,8 @@ public VSharpOptions(
163169
StepsLimit = stepsLimit;
164170
AIAgentTrainingOptions = aiAgentTrainingOptions;
165171
PathToModel = pathToModel;
172+
UseGPU = useGPU;
173+
Optimize = optimize;
166174
}
167175

168176
/// <summary>

‎VSharp.Explorer/AISearcher.fs‎

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -193,15 +193,24 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingOptions: Option<AIAgentT
193193
oracle.Feedback(Feedback.IncorrectPredictedStateId stateId)
194194
None
195195

196-
new(pathToONNX: string) =
196+
new(pathToONNX: string, useGPU: bool, optimize: bool) =
197197
let numOfVertexAttributes = 7
198198
let numOfStateAttributes = 7
199199
let numOfHistoryEdgeAttributes = 2
200200

201201
let createOracle (pathToONNX: string) =
202-
let sessionOptions = new SessionOptions()
203-
sessionOptions.ExecutionMode <- ExecutionMode.ORT_PARALLEL
204-
sessionOptions.GraphOptimizationLevel <- GraphOptimizationLevel.ORT_ENABLE_ALL
202+
let sessionOptions =
203+
if useGPU then
204+
SessionOptions.MakeSessionOptionWithCudaProvider(0)
205+
else
206+
new SessionOptions()
207+
208+
if optimize then
209+
sessionOptions.ExecutionMode <- ExecutionMode.ORT_PARALLEL
210+
sessionOptions.GraphOptimizationLevel <- GraphOptimizationLevel.ORT_ENABLE_ALL
211+
else
212+
sessionOptions.GraphOptimizationLevel <- GraphOptimizationLevel.ORT_ENABLE_BASIC
213+
205214
let session = new InferenceSession(pathToONNX, sessionOptions)
206215
let runOptions = new RunOptions()
207216
let feedback (x: Feedback) = ()

‎VSharp.Explorer/Explorer.fs‎

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,20 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
131131
| None -> failwith "Empty oracle for AI searcher."
132132
| None ->
133133
match options.pathToModel with
134-
| Some s -> AISearcher s
134+
| Some s ->
135+
let useGPU =
136+
if options.useGPU.IsSome then
137+
options.useGPU.Value
138+
else
139+
false
140+
141+
let optimize =
142+
if options.optimize.IsSome then
143+
options.optimize.Value
144+
else
145+
false
146+
147+
AISearcher(s, useGPU, optimize)
135148
| None -> failwith "Empty model for AI searcher."
136149
| BFSMode -> BFSSearcher() :> IForwardSearcher
137150
| DFSMode -> DFSSearcher() :> IForwardSearcher

‎VSharp.Explorer/Options.fs‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,9 @@ type SVMOptions =
6969
randomSeed: int
7070
stepsLimit: uint
7171
aiAgentTrainingOptions: Option<AIAgentTrainingOptions>
72-
pathToModel: Option<string> }
72+
pathToModel: Option<string>
73+
useGPU: Option<bool>
74+
optimize: Option<bool> }
7375

7476
type explorationModeOptions =
7577
| Fuzzing of FuzzerOptions

‎VSharp.ML.GameServer.Runner/Main.fs‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,8 @@ type CliArguments =
4141
| [<Unique; Mandatory>] Mode of Mode
4242
| [<Unique>] OutFolder of string
4343
| [<Unique>] StepsToSerialize of uint
44+
| [<Unique>] UseGPU
45+
| [<Unique>] Optimize
4446
interface IArgParserTemplate with
4547
member s.Usage =
4648
match s with
@@ -52,6 +54,8 @@ type CliArguments =
5254
"Mode to run application. Server --- to train network, Generator --- to generate data for training."
5355
| OutFolder _ -> "Folder to store generated data."
5456
| StepsToSerialize _ -> "Maximal number of steps for each method to serialize."
57+
| UseGPU -> "Enables GPU processing."
58+
| Optimize -> "Optimize."
5559

5660
let mutable inTrainMode = true
5761

@@ -310,6 +314,10 @@ let main args =
310314
| Some steps -> steps
311315
| None -> 500u
312316

317+
let useGPU = (args.TryGetResult <@ UseGPU @>).IsSome
318+
319+
let optimize = (args.TryGetResult <@ Optimize @>).IsSome
320+
313321
let outputDirectory = Path.Combine(Directory.GetCurrentDirectory(), string port)
314322

315323
if Directory.Exists outputDirectory then

‎VSharp.Runner/RunnerProgram.cs‎

Lines changed: 58 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -90,12 +90,12 @@ public static class RunnerProgram
9090
{
9191
var t = methodArgumentValue.Split('.');
9292
var className = t.Length == 1 ? "" : t[t.Length - 2];
93-
var methodName = t.Last();
93+
var methodName = t.Last();
9494
var x = type.GetMethods(Reflection.allBindingFlags);
9595
method ??= x
9696
.Where(m => type.FullName.Split('.').Last().Contains(className) && m.Name.Contains(methodName))
9797
.MinBy(m => m.Name.Length);
98-
if (method != null)
98+
if (method != null)
9999
break;
100100
}
101101
catch (Exception)
@@ -132,7 +132,10 @@ private static void EntryPointHandler(
132132
Verbosity verbosity,
133133
uint recursionThreshold,
134134
ExplorationMode explorationMode,
135-
string pathToModel)
135+
string pathToModel,
136+
bool useGPU,
137+
bool optimize
138+
)
136139
{
137140
var assembly = TryLoadAssembly(assemblyPath);
138141
var options =
@@ -145,7 +148,9 @@ private static void EntryPointHandler(
145148
verbosity: verbosity,
146149
recursionThreshold: recursionThreshold,
147150
explorationMode: explorationMode,
148-
pathToModel: pathToModel);
151+
pathToModel: pathToModel,
152+
useGPU: useGPU,
153+
optimize: optimize);
149154

150155
if (assembly == null) return;
151156

@@ -239,7 +244,9 @@ private static void AllPublicMethodsHandler(
239244
Verbosity verbosity,
240245
uint recursionThreshold,
241246
ExplorationMode explorationMode,
242-
string pathToModel)
247+
string pathToModel,
248+
bool useGPU,
249+
bool optimize)
243250
{
244251
var assembly = TryLoadAssembly(assemblyPath);
245252
var options =
@@ -252,7 +259,9 @@ private static void AllPublicMethodsHandler(
252259
verbosity: verbosity,
253260
recursionThreshold: recursionThreshold,
254261
explorationMode: explorationMode,
255-
pathToModel: pathToModel);
262+
pathToModel: pathToModel,
263+
useGPU: useGPU,
264+
optimize: optimize);
256265

257266
if (assembly == null) return;
258267

@@ -276,7 +285,9 @@ private static void PublicMethodsOfTypeHandler(
276285
Verbosity verbosity,
277286
uint recursionThreshold,
278287
ExplorationMode explorationMode,
279-
string pathToModel)
288+
string pathToModel,
289+
bool useGPU,
290+
bool optimize)
280291
{
281292
var assembly = TryLoadAssembly(assemblyPath);
282293
if (assembly == null) return;
@@ -298,7 +309,9 @@ private static void PublicMethodsOfTypeHandler(
298309
verbosity: verbosity,
299310
recursionThreshold: recursionThreshold,
300311
explorationMode: explorationMode,
301-
pathToModel: pathToModel);
312+
pathToModel: pathToModel,
313+
useGPU: useGPU,
314+
optimize: optimize);
302315

303316
Statistics statistics;
304317
if (runTests)
@@ -321,7 +334,9 @@ private static void SpecificMethodHandler(
321334
Verbosity verbosity,
322335
uint recursionThreshold,
323336
ExplorationMode explorationMode,
324-
string pathToModel)
337+
string pathToModel,
338+
bool useGPU,
339+
bool optimize)
325340
{
326341
var assembly = TryLoadAssembly(assemblyPath);
327342
if (assembly == null) return;
@@ -359,7 +374,9 @@ private static void SpecificMethodHandler(
359374
verbosity: verbosity,
360375
recursionThreshold: recursionThreshold,
361376
explorationMode: explorationMode,
362-
pathToModel: pathToModel);
377+
pathToModel: pathToModel,
378+
useGPU: useGPU,
379+
optimize: optimize);
363380

364381
Statistics statistics;
365382
if (runTests || checkCoverage)
@@ -381,7 +398,9 @@ private static void NamespaceHandler(
381398
Verbosity verbosity,
382399
uint recursionThreshold,
383400
ExplorationMode explorationMode,
384-
string pathToModel)
401+
string pathToModel,
402+
bool useGPU,
403+
bool optimize)
385404
{
386405
var assembly = TryLoadAssembly(assemblyPath);
387406
if (assembly == null) return;
@@ -403,7 +422,9 @@ private static void NamespaceHandler(
403422
verbosity: verbosity,
404423
recursionThreshold: recursionThreshold,
405424
explorationMode: explorationMode,
406-
pathToModel: pathToModel);
425+
pathToModel: pathToModel,
426+
useGPU: useGPU,
427+
optimize: optimize);
407428

408429
Statistics statistics;
409430
if (runTests)
@@ -427,6 +448,14 @@ public static int Main(string[] args)
427448
aliases: new[] { "--model", "-m" },
428449
() => defaultOptions.GetDefaultPathToModel(),
429450
"Path to ONNX file with model for AI searcher.");
451+
var useGPUOption = new Option<bool>(
452+
aliases: new[] { "--gpu" },
453+
() => false,
454+
"Enables GPU processing.");
455+
var optimizeOption = new Option<bool>(
456+
aliases: new[] { "--optimize" },
457+
() => false,
458+
"Optimize option.");
430459
var solverTimeoutOption = new Option<int>(
431460
aliases: new[] { "--solver-timeout", "-st" },
432461
() => -1,
@@ -473,6 +502,8 @@ public static int Main(string[] args)
473502
rootCommand.AddGlobalOption(recursionThresholdOption);
474503
rootCommand.AddGlobalOption(explorationModeOption);
475504
rootCommand.AddGlobalOption(pathToModelOption);
505+
rootCommand.AddGlobalOption(useGPUOption);
506+
rootCommand.AddGlobalOption(optimizeOption);
476507

477508
var entryPointCommand =
478509
new Command("--entry-point", "Generate test coverage from the entry point of assembly (assembly must contain Main method)");
@@ -499,7 +530,9 @@ public static int Main(string[] args)
499530
parseResult.GetValueForOption(verbosityOption),
500531
parseResult.GetValueForOption(recursionThresholdOption),
501532
parseResult.GetValueForOption(explorationModeOption),
502-
parseResult.GetValueForOption(pathToModelOption)
533+
parseResult.GetValueForOption(pathToModelOption),
534+
parseResult.GetValueForOption(useGPUOption),
535+
parseResult.GetValueForOption(optimizeOption)
503536
);
504537
});
505538

@@ -561,7 +594,9 @@ public static int Main(string[] args)
561594
parseResult.GetValueForOption(verbosityOption),
562595
parseResult.GetValueForOption(recursionThresholdOption),
563596
parseResult.GetValueForOption(explorationModeOption),
564-
parseResult.GetValueForOption(pathToModelOption)
597+
parseResult.GetValueForOption(pathToModelOption),
598+
parseResult.GetValueForOption(useGPUOption),
599+
parseResult.GetValueForOption(optimizeOption)
565600
);
566601
});
567602

@@ -589,7 +624,9 @@ public static int Main(string[] args)
589624
parseResult.GetValueForOption(verbosityOption),
590625
parseResult.GetValueForOption(recursionThresholdOption),
591626
parseResult.GetValueForOption(explorationModeOption),
592-
parseResult.GetValueForOption(pathToModelOption)
627+
parseResult.GetValueForOption(pathToModelOption),
628+
parseResult.GetValueForOption(useGPUOption),
629+
parseResult.GetValueForOption(optimizeOption)
593630
);
594631
});
595632

@@ -620,7 +657,9 @@ public static int Main(string[] args)
620657
parseResult.GetValueForOption(verbosityOption),
621658
parseResult.GetValueForOption(recursionThresholdOption),
622659
parseResult.GetValueForOption(explorationModeOption),
623-
pathToModel
660+
pathToModel,
661+
parseResult.GetValueForOption(useGPUOption),
662+
parseResult.GetValueForOption(optimizeOption)
624663
);
625664
});
626665

@@ -649,7 +688,9 @@ public static int Main(string[] args)
649688
parseResult.GetValueForOption(verbosityOption),
650689
parseResult.GetValueForOption(recursionThresholdOption),
651690
parseResult.GetValueForOption(explorationModeOption),
652-
pathToModel
691+
pathToModel,
692+
parseResult.GetValueForOption(useGPUOption),
693+
parseResult.GetValueForOption(optimizeOption)
653694
);
654695
});
655696

0 commit comments

Comments
 (0)