diff --git a/VSharp.API/VSharp.cs b/VSharp.API/VSharp.cs index 434b3a874..f6b186161 100644 --- a/VSharp.API/VSharp.cs +++ b/VSharp.API/VSharp.cs @@ -111,7 +111,7 @@ public IEnumerable Results() public static class TestGenerator { - private class Reporter: IReporter + private class Reporter : IReporter { private readonly UnitTests _unitTests; private readonly bool _isQuiet; @@ -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) { @@ -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, @@ -191,8 +191,11 @@ private static Statistics StartExploration( stopOnCoverageAchieved: 100, randomSeed: options.RandomSeed, stepsLimit: options.StepsLimit, - aiAgentTrainingOptions: options.AIAgentTrainingOptions == null ? FSharpOption.None :FSharpOption.Some(options.AIAgentTrainingOptions), - pathToModel: options.PathToModel == null ? FSharpOption.None : FSharpOption.Some(options.PathToModel)); + aiAgentTrainingOptions: options.AIAgentTrainingOptions == null ? FSharpOption.None : FSharpOption.Some(options.AIAgentTrainingOptions), + pathToModel: options.PathToModel == null ? FSharpOption.None : FSharpOption.Some(options.PathToModel), + useGPU: options.UseGPU == null ? FSharpOption.None : FSharpOption.Some(options.UseGPU), + optimize: options.Optimize == null ? FSharpOption.None : FSharpOption.Some(options.Optimize) + ); var fuzzerOptions = new FuzzerOptions( @@ -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 {method}; + var methods = new List { method }; var statistics = StartExploration(methods, coverageZone.MethodZone, options); if (options.RenderTests) diff --git a/VSharp.API/VSharpOptions.cs b/VSharp.API/VSharpOptions.cs index 9132eaf6f..ffcb0330b 100644 --- a/VSharp.API/VSharpOptions.cs +++ b/VSharp.API/VSharpOptions.cs @@ -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; /// /// Symbolic virtual machine options. @@ -133,6 +135,8 @@ public readonly record struct VSharpOptions /// Number of symbolic machine steps to stop execution after. Zero value means no limit. /// Settings for AI searcher training. /// Path to ONNX file with model to use in AI searcher. + /// Enables GPU processing. + /// Optimize. public VSharpOptions( int timeout = DefaultTimeout, int solverTimeout = DefaultSolverTimeout, @@ -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; @@ -163,6 +169,8 @@ public VSharpOptions( StepsLimit = stepsLimit; AIAgentTrainingOptions = aiAgentTrainingOptions; PathToModel = pathToModel; + UseGPU = useGPU; + Optimize = optimize; } /// diff --git a/VSharp.Explorer/AISearcher.fs b/VSharp.Explorer/AISearcher.fs index 629a8c4b1..80c30d426 100644 --- a/VSharp.Explorer/AISearcher.fs +++ b/VSharp.Explorer/AISearcher.fs @@ -165,23 +165,36 @@ type internal AISearcher(oracle : Oracle, aiAgentTrainingOptions : Option, int> () let verticesIds = Dictionary, int> () + let networkInput = let res = Dictionary<_, _> () let gameVertices = diff --git a/VSharp.Explorer/Explorer.fs b/VSharp.Explorer/Explorer.fs index bff57569f..29399ec3d 100644 --- a/VSharp.Explorer/Explorer.fs +++ b/VSharp.Explorer/Explorer.fs @@ -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 diff --git a/VSharp.Explorer/Options.fs b/VSharp.Explorer/Options.fs index a573129d0..a5ddca2e5 100644 --- a/VSharp.Explorer/Options.fs +++ b/VSharp.Explorer/Options.fs @@ -76,6 +76,8 @@ type SVMOptions = stepsLimit : uint aiAgentTrainingOptions : Option pathToModel : Option + useGPU : Option + optimize : Option } type explorationModeOptions = diff --git a/VSharp.ML.GameServer.Runner/Main.fs b/VSharp.ML.GameServer.Runner/Main.fs index 3684ab0be..f34563e9b 100644 --- a/VSharp.ML.GameServer.Runner/Main.fs +++ b/VSharp.ML.GameServer.Runner/Main.fs @@ -41,7 +41,8 @@ type CliArguments = | [] Mode of Mode | [] OutFolder of string | [] StepsToSerialize of uint - + | [] UseGPU + | [] Optimize interface IArgParserTemplate with member s.Usage = match s with @@ -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 @@ -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) diff --git a/VSharp.Runner/RunnerProgram.cs b/VSharp.Runner/RunnerProgram.cs index a3b841c3c..096c04d18 100644 --- a/VSharp.Runner/RunnerProgram.cs +++ b/VSharp.Runner/RunnerProgram.cs @@ -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) @@ -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 = @@ -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; @@ -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 = @@ -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; @@ -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; @@ -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) @@ -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; @@ -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) @@ -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; @@ -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) @@ -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( + aliases: new[] { "--gpu" }, + () => false, + "Enables GPU processing."); + var optimizeOption = new Option( + aliases: new[] { "--optimize" }, + () => false, + "Optimize option."); var solverTimeoutOption = new Option( aliases: new[] { "--solver-timeout", "-st" }, () => -1, @@ -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)"); @@ -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) ); }); @@ -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) ); }); @@ -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) ); }); @@ -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) ); }); @@ -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) ); }); diff --git a/VSharp.Test/Benchmarks/Benchmarks.cs b/VSharp.Test/Benchmarks/Benchmarks.cs index 677e8ed8e..12e022ffd 100644 --- a/VSharp.Test/Benchmarks/Benchmarks.cs +++ b/VSharp.Test/Benchmarks/Benchmarks.cs @@ -35,7 +35,7 @@ private static bool TryBuildGeneratedTests() return process.IsSuccess(); } - private class Reporter: IReporter + private class Reporter : IReporter { private readonly UnitTests _unitTests; @@ -94,7 +94,9 @@ public static BenchmarkResult Run( randomSeed: randomSeed, stepsLimit: stepsLimit, aiAgentTrainingOptions: null, - pathToModel: null + pathToModel: null, + useGPU: null, + optimize: null ); var fuzzerOptions = new FuzzerOptions( @@ -113,7 +115,7 @@ public static BenchmarkResult Run( using var explorer = new Explorer.Explorer(explorationOptions, new Reporter(unitTests)); explorer.StartExploration( - new[] {exploredMethodInfo}, + new[] { exploredMethodInfo }, global::System.Array.Empty>() ); diff --git a/VSharp.Test/IntegrationTests.cs b/VSharp.Test/IntegrationTests.cs index 13ce410fc..00ed34653 100644 --- a/VSharp.Test/IntegrationTests.cs +++ b/VSharp.Test/IntegrationTests.cs @@ -75,7 +75,7 @@ public IEnumerable BuildFrom(ITypeInfo typeInfo) } [AttributeUsage(AttributeTargets.Class | AttributeTargets.Struct | AttributeTargets.Method, AllowMultiple = true)] - public class IgnoreFuzzerAttribute: Attribute + public class IgnoreFuzzerAttribute : Attribute { public string Reason { get; init; } @@ -133,6 +133,9 @@ static TestSvmAttribute() private readonly int _randomSeed; private readonly uint _stepsLimit; private readonly string _pathToModel; + private readonly bool _useGPU; + private readonly bool _optimize; + public TestSvmAttribute( int expectedCoverage = -1, @@ -150,7 +153,9 @@ public TestSvmAttribute( ExplorationMode explorationMode = ExplorationMode.Sili, int randomSeed = 0, uint stepsLimit = 0, - string pathToModel = "models/model.onnx") + string pathToModel = "models/model.onnx", + bool useGPU = false, + bool optimize = false) { if (expectedCoverage < 0) _expectedCoverage = null; @@ -172,6 +177,8 @@ public TestSvmAttribute( _explorationMode = explorationMode; _randomSeed = randomSeed; _pathToModel = pathToModel; + _useGPU = useGPU; + _optimize = optimize; _stepsLimit = stepsLimit; } @@ -194,6 +201,8 @@ public TestCommand Wrap(TestCommand command) _randomSeed, _stepsLimit, _pathToModel, + _useGPU, + _optimize, _hasExternMocking ); } @@ -219,8 +228,10 @@ private class TestSvmCommand : DelegatingTestCommand private readonly int _randomSeed; private readonly uint _stepsLimit; private readonly string _pathToModel; + private readonly bool _useGPU; + private readonly bool _optimize; - private class Reporter: IReporter + private class Reporter : IReporter { private readonly UnitTests _unitTests; @@ -231,7 +242,7 @@ public Reporter(UnitTests unitTests) 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) => ExceptionDispatchInfo.Capture(exn).Throw(); public void ReportCrash(Exception exn) => ExceptionDispatchInfo.Capture(exn).Throw(); } @@ -253,6 +264,8 @@ public TestSvmCommand( int randomSeed, uint stepsLimit, string pathToModel, + bool useGPU, + bool optimize, bool hasExternMocking) : base(innerCommand) { _baseCoverageZone = coverageZone; @@ -307,6 +320,8 @@ public TestSvmCommand( _randomSeed = randomSeed; _stepsLimit = stepsLimit; _pathToModel = pathToModel; + _useGPU = useGPU; + _optimize = optimize; } private TestResult IgnoreTest(TestExecutionContext context) @@ -366,7 +381,7 @@ DirectoryInfo testsDir bool success; var resultMessage = string.Empty; uint? actualCoverage; - if (_expectedCoverage is {} expectedCoverage) + if (_expectedCoverage is { } expectedCoverage) { TestContext.Out.WriteLine("Starting coverage tool..."); success = @@ -438,7 +453,7 @@ private TestResult Explore(TestExecutionContext context) }; var originMethodInfo = innerCommand.Test.Method.MethodInfo; - var exploredMethodInfo = (MethodInfo) AssemblyManager.NormalizeMethod(originMethodInfo); + var exploredMethodInfo = (MethodInfo)AssemblyManager.NormalizeMethod(originMethodInfo); var stats = new TestStatistics( exploredMethodInfo, _releaseBranches, @@ -463,8 +478,10 @@ private TestResult Explore(TestExecutionContext context) stopOnCoverageAchieved: _expectedCoverage ?? -1, randomSeed: _randomSeed, stepsLimit: _stepsLimit, - aiAgentTrainingOptions:null, - pathToModel: _pathToModel + aiAgentTrainingOptions: null, + pathToModel: _pathToModel, + useGPU: _useGPU, + optimize: _optimize ); var fuzzerOptions = new FuzzerOptions( @@ -489,7 +506,7 @@ private TestResult Explore(TestExecutionContext context) using var explorer = new Explorer.Explorer(explorationOptions, new Reporter(unitTests)); Application.reset(); explorer.StartExploration( - new [] { exploredMethodInfo }, + new[] { exploredMethodInfo }, global::System.Array.Empty>() );