Skip to content

Commit

Permalink
Option to configure path to model.
Browse files Browse the repository at this point in the history
  • Loading branch information
gsvgit committed Jan 17, 2024
1 parent c05ce47 commit d7c05ab
Show file tree
Hide file tree
Showing 8 changed files with 65 additions and 43 deletions.
6 changes: 2 additions & 4 deletions VSharp.API/VSharp.cs
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,9 @@
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Net.WebSockets;
using System.Reflection;
using System.Text;
using VSharp.CSharpUtils;
using VSharp.IL;
using VSharp.Interpreter.IL;
using VSharp.Explorer;

Expand Down Expand Up @@ -187,8 +185,8 @@ private static Statistics StartExploration(
stopOnCoverageAchieved: 100,
randomSeed: options.RandomSeed,
stepsLimit: options.StepsLimit,
oracle: options.Oracle,
aiAgentTrainingOptions: options.AIAgentTrainingOptions
aiAgentTrainingOptions: options.AIAgentTrainingOptions,
pathToModel: options.PathToModel
);

var fuzzerOptions =
Expand Down
10 changes: 6 additions & 4 deletions VSharp.API/VSharpOptions.cs
Original file line number Diff line number Diff line change
Expand Up @@ -111,8 +111,8 @@ public readonly record struct VSharpOptions
public readonly bool ReleaseBranches = DefaultReleaseBranches;
public readonly int RandomSeed = DefaultRandomSeed;
public readonly uint StepsLimit = DefaultStepsLimit;
public readonly Oracle? Oracle = null;
public readonly AIAgentTrainingOptions AIAgentTrainingOptions = null;
public readonly string PathToModel = null;

/// <summary>
/// Symbolic virtual machine options.
Expand All @@ -129,6 +129,8 @@ public readonly record struct VSharpOptions
/// <param name="releaseBranches">If true and timeout is specified, a part of allotted time in the end is given to execute remaining states without branching.</param>
/// <param name="randomSeed">Fixed seed for random operations. Used if greater than or equal to zero.</param>
/// <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>
public VSharpOptions(
int timeout = DefaultTimeout,
int solverTimeout = DefaultSolverTimeout,
Expand All @@ -142,8 +144,8 @@ public VSharpOptions(
bool releaseBranches = DefaultReleaseBranches,
int randomSeed = DefaultRandomSeed,
uint stepsLimit = DefaultStepsLimit,
Oracle? oracle = null,
AIAgentTrainingOptions aiAgentTrainingOptions = null)
AIAgentTrainingOptions aiAgentTrainingOptions = null,
string pathToModel = null)
{
Timeout = timeout;
SolverTimeout = solverTimeout;
Expand All @@ -157,8 +159,8 @@ public VSharpOptions(
ReleaseBranches = releaseBranches;
RandomSeed = randomSeed;
StepsLimit = stepsLimit;
Oracle = oracle;
AIAgentTrainingOptions = aiAgentTrainingOptions;
PathToModel = pathToModel;
}

/// <summary>
Expand Down
11 changes: 10 additions & 1 deletion VSharp.Explorer/Explorer.fs
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,16 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
let rec mkForwardSearcher mode =
let getRandomSeedOption() = if options.randomSeed < 0 then None else Some options.randomSeed
match mode with
| AIMode -> AISearcher(options.oracle.Value, options.aiAgentTrainingOptions) :> IForwardSearcher
| AIMode ->
match options.aiAgentTrainingOptions with
| Some aiOptions ->
match aiOptions.oracle with
| Some oracle -> AISearcher(oracle, options.aiAgentTrainingOptions) :> IForwardSearcher
| None -> failwith "Empty oracle for AI searcher."
| None ->
match options.pathToModel with
| Some s -> AISearcher s
| None -> failwith "Empty model for AI searcher."
| BFSMode -> BFSSearcher() :> IForwardSearcher
| DFSMode -> DFSSearcher() :> IForwardSearcher
| ShortestDistanceBasedMode -> ShortestDistanceBasedSearcher statistics :> IForwardSearcher
Expand Down
6 changes: 4 additions & 2 deletions VSharp.Explorer/Options.fs
Original file line number Diff line number Diff line change
Expand Up @@ -46,13 +46,15 @@ type Oracle =
/// <param name="defaultSearchStrategy">Default searcher that will be used to play few initial steps.</param>
/// <param name="serializeSteps">Determine whether steps should be serialized.</param>
/// <param name="mapName">Name of map to play.</param>
/// <param name="mapName">Name of map to play.</param>
type AIAgentTrainingOptions =
{
stepsToSwitchToAI: uint<step>
stepsToPlay: uint<step>
defaultSearchStrategy: searchMode
serializeSteps: bool
mapName: string
mapName: string
oracle: Option<Oracle>
}

type SVMOptions = {
Expand All @@ -67,8 +69,8 @@ type SVMOptions = {
stopOnCoverageAchieved : int
randomSeed : int
stepsLimit : uint
oracle: Option<Oracle>
aiAgentTrainingOptions: Option<AIAgentTrainingOptions>
pathToModel: Option<string>
}

type explorationModeOptions =
Expand Down
4 changes: 3 additions & 1 deletion VSharp.ML.GameServer.Runner/Main.fs
Original file line number Diff line number Diff line change
Expand Up @@ -156,8 +156,9 @@ let ws outputDirectory (webSocket : WebSocket) (context: HttpContext) =
| x -> failwithf $"Unexpected searcher {x}. Use DFS or BFS for now."
serializeSteps = false
mapName = gameMap.MapName
oracle = Some oracle
}
let options = VSharpOptions(timeout = 15 * 60, outputDirectory = outputDirectory, oracle = oracle, searchStrategy = SearchStrategy.AI, aiAgentTrainingOptions = aiTrainingOptions, solverTimeout=2)
let options = VSharpOptions(timeout = 15 * 60, outputDirectory = outputDirectory, searchStrategy = SearchStrategy.AI, aiAgentTrainingOptions = aiTrainingOptions, solverTimeout=2)
let statistics = TestGenerator.Cover(method, options)
let actualCoverage =
try
Expand Down Expand Up @@ -206,6 +207,7 @@ let generateDataForPretraining outputDirectory datasetBasePath (maps:Dictionary<
defaultSearchStrategy = searchMode.BFSMode
serializeSteps = true
mapName = kvp.Value.MapName
oracle = None
}
let options = VSharpOptions(timeout = 5 * 60, outputDirectory = outputDirectory, searchStrategy = SearchStrategy.ExecutionTreeContributedCoverage, stepsLimit = stepsToSerialize, solverTimeout=2, aiAgentTrainingOptions = aiTrainingOptions)
let statistics = TestGenerator.Cover(method, options)
Expand Down
44 changes: 29 additions & 15 deletions VSharp.Runner/RunnerProgram.cs
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,10 @@ public static int Main(string[] args)
aliases: new[] { "--timeout", "-t" },
() => -1,
"Time for test generation in seconds. Negative value means no timeout.");
var pathToModelOption = new Option<string>(
aliases: new[] { "--model", "-m" },
() => null,
"Path to ONNX file with model for AI searcher.");
var solverTimeoutOption = new Option<int>(
aliases: new[] { "--solver-timeout", "-st" },
() => -1,
Expand Down Expand Up @@ -178,6 +182,7 @@ public static int Main(string[] args)
entryPointCommand.AddArgument(assemblyPathArgument);
entryPointCommand.AddArgument(concreteArguments);
entryPointCommand.AddGlobalOption(timeoutOption);
entryPointCommand.AddGlobalOption(pathToModelOption);
entryPointCommand.AddGlobalOption(solverTimeoutOption);
entryPointCommand.AddGlobalOption(outputOption);
entryPointCommand.AddOption(unknownArgsOption);
Expand All @@ -192,6 +197,7 @@ public static int Main(string[] args)
rootCommand.AddCommand(allPublicMethodsCommand);
allPublicMethodsCommand.AddArgument(assemblyPathArgument);
allPublicMethodsCommand.AddGlobalOption(timeoutOption);
allPublicMethodsCommand.AddGlobalOption(pathToModelOption);
allPublicMethodsCommand.AddGlobalOption(solverTimeoutOption);
allPublicMethodsCommand.AddGlobalOption(outputOption);
allPublicMethodsCommand.AddGlobalOption(renderTestsOption);
Expand All @@ -208,6 +214,7 @@ public static int Main(string[] args)
publicMethodsOfClassCommand.AddArgument(classArgument);
publicMethodsOfClassCommand.AddArgument(assemblyPathArgument);
publicMethodsOfClassCommand.AddGlobalOption(timeoutOption);
publicMethodsOfClassCommand.AddGlobalOption(pathToModelOption);
publicMethodsOfClassCommand.AddGlobalOption(solverTimeoutOption);
publicMethodsOfClassCommand.AddGlobalOption(outputOption);
publicMethodsOfClassCommand.AddGlobalOption(renderTestsOption);
Expand All @@ -223,6 +230,7 @@ public static int Main(string[] args)
specificMethodCommand.AddArgument(methodArgument);
specificMethodCommand.AddArgument(assemblyPathArgument);
specificMethodCommand.AddGlobalOption(timeoutOption);
specificMethodCommand.AddGlobalOption(pathToModelOption);
specificMethodCommand.AddGlobalOption(solverTimeoutOption);
specificMethodCommand.AddGlobalOption(outputOption);
specificMethodCommand.AddGlobalOption(renderTestsOption);
Expand All @@ -238,6 +246,7 @@ public static int Main(string[] args)
namespaceCommand.AddArgument(namespaceArgument);
namespaceCommand.AddArgument(assemblyPathArgument);
namespaceCommand.AddGlobalOption(timeoutOption);
namespaceCommand.AddGlobalOption(pathToModelOption);
namespaceCommand.AddGlobalOption(solverTimeoutOption);
namespaceCommand.AddGlobalOption(outputOption);
namespaceCommand.AddGlobalOption(renderTestsOption);
Expand All @@ -249,8 +258,8 @@ public static int Main(string[] args)

rootCommand.Description = "Symbolic execution engine for .NET";

entryPointCommand.Handler = CommandHandler.Create<FileInfo, string[], int, int, DirectoryInfo, bool, bool, bool, SearchStrategy, Verbosity, uint, ExplorationMode>(
(assemblyPath, args, timeout, solverTimeout, output, unknownArgs, renderTests, runTests, strat, verbosity, recursionThreshold, explorationMode) =>
entryPointCommand.Handler = CommandHandler.Create<FileInfo, string[], int, string, int, DirectoryInfo, bool, bool, bool, SearchStrategy, Verbosity, uint, ExplorationMode>(
(assemblyPath, args, timeout, pathToModel, solverTimeout, output, unknownArgs, renderTests, runTests, strat, verbosity, recursionThreshold, explorationMode) =>
{
var assembly = TryLoadAssembly(assemblyPath);
var inputArgs = unknownArgs ? null : args;
Expand All @@ -263,7 +272,8 @@ public static int Main(string[] args)
searchStrategy: strat,
verbosity: verbosity,
recursionThreshold: recursionThreshold,
explorationMode: explorationMode);
explorationMode: explorationMode,
pathToModel: pathToModel);
if (assembly == null) return;
Expand All @@ -275,8 +285,8 @@ public static int Main(string[] args)
else PostProcess(TestGenerator.Cover(assembly, inputArgs, options));
});

allPublicMethodsCommand.Handler = CommandHandler.Create<FileInfo, int, int, DirectoryInfo, bool, bool, bool, SearchStrategy, Verbosity, uint, ExplorationMode>(
(assemblyPath, timeout, solverTimeout, output, renderTests, runTests, singleFile, strat, verbosity, recursionThreshold, explorationMode) =>
allPublicMethodsCommand.Handler = CommandHandler.Create<FileInfo, int, string, int, DirectoryInfo, bool, bool, bool, SearchStrategy, Verbosity, uint, ExplorationMode>(
(assemblyPath, timeout, pathToModel, solverTimeout, output, renderTests, runTests, singleFile, strat, verbosity, recursionThreshold, explorationMode) =>
{
var assembly = TryLoadAssembly(assemblyPath);
var options =
Expand All @@ -288,7 +298,8 @@ public static int Main(string[] args)
searchStrategy: strat,
verbosity: verbosity,
recursionThreshold: recursionThreshold,
explorationMode: explorationMode);
explorationMode: explorationMode,
pathToModel: pathToModel);
if (assembly == null) return;
Expand All @@ -300,8 +311,8 @@ public static int Main(string[] args)
else PostProcess(TestGenerator.Cover(assembly, options));
});

publicMethodsOfClassCommand.Handler = CommandHandler.Create<string, FileInfo, int, int, DirectoryInfo, bool, bool, SearchStrategy, Verbosity, uint, ExplorationMode>(
(className, assemblyPath, timeout, solverTimeout, output, renderTests, runTests, strat, verbosity, recursionThreshold, explorationMode) =>
publicMethodsOfClassCommand.Handler = CommandHandler.Create<string, FileInfo, int, string, int, DirectoryInfo, bool, bool, SearchStrategy, Verbosity, uint, ExplorationMode>(
(className, assemblyPath, timeout, pathToModel, solverTimeout, output, renderTests, runTests, strat, verbosity, recursionThreshold, explorationMode) =>
{
var assembly = TryLoadAssembly(assemblyPath);
if (assembly == null) return;
Expand All @@ -322,7 +333,8 @@ public static int Main(string[] args)
searchStrategy: strat,
verbosity: verbosity,
recursionThreshold: recursionThreshold,
explorationMode: explorationMode);
explorationMode: explorationMode,
pathToModel: pathToModel);
if (runTests)
{
Expand All @@ -332,8 +344,8 @@ public static int Main(string[] args)
else PostProcess(TestGenerator.Cover(type, options));
});

specificMethodCommand.Handler = CommandHandler.Create<string, FileInfo, int, int, DirectoryInfo, bool, bool, SearchStrategy, Verbosity, uint, ExplorationMode>(
(methodName, assemblyPath, timeout, solverTimeout, output, renderTests, runTests, strat, verbosity, recursionThreshold, explorationMode) =>
specificMethodCommand.Handler = CommandHandler.Create<string, FileInfo, int, string, int, DirectoryInfo, bool, bool, SearchStrategy, Verbosity, uint, ExplorationMode>(
(methodName, assemblyPath, timeout, pathToModel, solverTimeout, output, renderTests, runTests, strat, verbosity, recursionThreshold, explorationMode) =>
{
var assembly = TryLoadAssembly(assemblyPath);
if (assembly == null) return;
Expand Down Expand Up @@ -370,7 +382,8 @@ public static int Main(string[] args)
searchStrategy: strat,
verbosity: verbosity,
recursionThreshold: recursionThreshold,
explorationMode: explorationMode);
explorationMode: explorationMode,
pathToModel: pathToModel);
if (runTests)
{
Expand All @@ -380,8 +393,8 @@ public static int Main(string[] args)
else PostProcess(TestGenerator.Cover(method, options));
});

namespaceCommand.Handler = CommandHandler.Create<string, FileInfo, int, int, DirectoryInfo, bool, bool, SearchStrategy, Verbosity, uint, ExplorationMode>(
(namespaceName, assemblyPath, timeout, solverTimeout, output, renderTests, runTests, strat, verbosity, recursionThreshold, explorationMode) =>
namespaceCommand.Handler = CommandHandler.Create<string, FileInfo, int, string, int, DirectoryInfo, bool, bool, SearchStrategy, Verbosity, uint, ExplorationMode>(
(namespaceName, assemblyPath, timeout, pathToModel, solverTimeout, output, renderTests, runTests, strat, verbosity, recursionThreshold, explorationMode) =>
{
var assembly = TryLoadAssembly(assemblyPath);
if (assembly == null) return;
Expand All @@ -402,7 +415,8 @@ public static int Main(string[] args)
searchStrategy: strat,
verbosity: verbosity,
recursionThreshold: recursionThreshold,
explorationMode: explorationMode);
explorationMode: explorationMode,
pathToModel: pathToModel);
if (runTests)
{
TestGenerator.CoverAndRun(namespaceTypes, out var statistics, options);
Expand Down
4 changes: 2 additions & 2 deletions VSharp.Test/Benchmarks/Benchmarks.cs
Original file line number Diff line number Diff line change
Expand Up @@ -91,8 +91,8 @@ public static BenchmarkResult Run(
stopOnCoverageAchieved: -1,
randomSeed: randomSeed,
stepsLimit: stepsLimit,
oracle:null,
aiAgentTrainingOptions: null
aiAgentTrainingOptions: null,
pathToModel: null
);

var fuzzerOptions = new FuzzerOptions(
Expand Down
Loading

0 comments on commit d7c05ab

Please sign in to comment.