AI guided searcher

.github/workflows/build_vsharp.yml

@@ -1,31 +1,39 @@
 name: 'Build VSharp'
 
 on:
-  workflow_call
+  [workflow_call, pull_request, push]
 
 jobs:
   build:
     runs-on: ubuntu-22.04
     steps:
+    - uses: actions/setup-dotnet@v4
+      with:
+        dotnet-version: '7.0.x'
+
     - name: Checkout VSharp
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         submodules: false
-    - uses: actions/cache@v3
+
+    - uses: actions/cache@v4
       id: nuget-cache
       with:
         path: ~/.nuget/packages
         key: ${{ runner.os }}-nuget-${{ hashFiles('**/*.csproj', '**/*.fsproj') }}
         restore-keys: |
           ${{ runner.os }}-nuget-
+
     - name: Build VSharp
       run:
-        dotnet build -c DebugTailRec
-    - uses: actions/upload-artifact@v3
+        dotnet build -c Release
+
+    - uses: actions/upload-artifact@v4
       with:
         name: runner
         path: ./VSharp.Runner/bin/DebugTailRec/net7.0
-    - uses: actions/upload-artifact@v3
+
+    - uses: actions/upload-artifact@v4
       with:
         name: test_runner
         path: ./VSharp.TestRunner/bin/DebugTailRec/net7.0

.travis.yml

@@ -1,8 +1,9 @@
 language: csharp
 mono: none
-dotnet: 3.0.100
+dotnet: 6.0
 solution: VSharp.sln
 install:
   - dotnet restore
+  - dotnet tool restore
 script:
   - dotnet test -c Release

VSharp.API/VSharp.cs

@@ -5,6 +5,7 @@
 using System.Linq;
 using System.Reflection;
 using System.Text;
+using Microsoft.FSharp.Core;
 using VSharp.CoverageTool;
 using VSharp.CSharpUtils;
 using VSharp.Interpreter.IL;
@@ -110,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;
@@ -123,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)
             {
@@ -178,6 +179,7 @@ private static Statistics StartExploration(
                     explorationMode: explorationMode.NewTestCoverageMode(
                         coverageZone,
                         options.Timeout > 0 ? searchMode.NewFairMode(baseSearchMode) : baseSearchMode
+
                     ),
                     recThreshold: options.RecursionThreshold,
                     solverTimeout: options.SolverTimeout,
@@ -188,8 +190,12 @@ private static Statistics StartExploration(
                     checkAttributes: true,
                     stopOnCoverageAchieved: 100,
                     randomSeed: options.RandomSeed,
-                    stepsLimit: options.StepsLimit
-                );
+                    stepsLimit: options.StepsLimit,
+                    aiOptions: options.AIOptions == null ? FSharpOption<AIOptions>.None : FSharpOption<AIOptions>.Some(options.AIOptions),
+                    pathToModel: options.PathToModel == null ? FSharpOption<string>.None : FSharpOption<string>.Some(options.PathToModel),
+                    useGPU: options.UseGPU,
+                    optimize: options.Optimize
+                    );
 
             var fuzzerOptions =
                 new FuzzerOptions(
@@ -279,6 +285,7 @@ private static searchMode ToSiliMode(this SearchStrategy searchStrategy)
                 SearchStrategy.ExecutionTree => searchMode.ExecutionTreeMode,
                 SearchStrategy.ExecutionTreeContributedCoverage => searchMode.NewInterleavedMode(searchMode.ExecutionTreeMode, 1, searchMode.ContributedCoverageMode, 1),
                 SearchStrategy.Interleaved => searchMode.NewInterleavedMode(searchMode.ShortestDistanceBasedMode, 1, searchMode.ContributedCoverageMode, 9),
+                SearchStrategy.AI => searchMode.AIMode,
                 _ => throw new UnreachableException("Unknown search strategy")
             };
         }
@@ -322,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)

VSharp.API/VSharpOptions.cs

@@ -1,4 +1,6 @@
 using System.IO;
+using Microsoft.FSharp.Core;
+using VSharp.Explorer;
 
 namespace VSharp;
 
@@ -38,7 +40,8 @@
     /// <summary>
     /// Interleaves <see cref="ShortestDistance"/> and <see cref="ContributedCoverage"/> strategies.
     /// </summary>
-    Interleaved
+    Interleaved,
+    AI
 }
 
 /// <summary>
@@ -96,6 +99,7 @@
     private const bool DefaultReleaseBranches = true;
     private const int DefaultRandomSeed = -1;
     private const uint DefaultStepsLimit = 0;
+    private const string DefaultPathToModel = "models/model.onnx";
 
     public readonly int Timeout = DefaultTimeout;
     public readonly int SolverTimeout = DefaultSolverTimeout;
@@ -109,6 +113,10 @@
     public readonly bool ReleaseBranches = DefaultReleaseBranches;
     public readonly int RandomSeed = DefaultRandomSeed;
     public readonly uint StepsLimit = DefaultStepsLimit;
+    public readonly AIOptions? AIOptions = null;
+    public readonly string PathToModel = DefaultPathToModel;
+    public readonly bool UseGPU = false;
+    public readonly bool Optimize = false;
 
     /// <summary>
     /// Symbolic virtual machine options.
@@ -125,6 +133,10 @@
     /// <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="aiOptions">Settings for AI searcher training.</param>
+    /// <param name="pathToModel">Path to ONNX file with model to use in AI searcher.</param>
+    /// <param name="useGPU">Specifies whether the ONNX execution session should use a CUDA-enabled GPU.</param>
+    /// <param name="optimize">Enabling options like parallel execution and various graph transformations to enhance performance of ONNX.</param>
     public VSharpOptions(
         int timeout = DefaultTimeout,
         int solverTimeout = DefaultSolverTimeout,
@@ -137,7 +149,11 @@
         ExplorationMode explorationMode = DefaultExplorationMode,
         bool releaseBranches = DefaultReleaseBranches,
         int randomSeed = DefaultRandomSeed,
-        uint stepsLimit = DefaultStepsLimit)
+        uint stepsLimit = DefaultStepsLimit,
+        AIOptions? aiOptions = null,
+        string pathToModel = DefaultPathToModel,
+        bool useGPU = false,
+        bool optimize = false)
     {
         Timeout = timeout;
         SolverTimeout = solverTimeout;
@@ -151,11 +167,20 @@
         ReleaseBranches = releaseBranches;
         RandomSeed = randomSeed;
         StepsLimit = stepsLimit;
+        AIOptions = aiOptions;
+        PathToModel = pathToModel;
+        UseGPU = useGPU;
+        Optimize = optimize;
     }
 
     /// <summary>
     /// <seealso cref="RenderedTestsDirectory"/>
     /// </summary>
     public DirectoryInfo RenderedTestsDirectoryInfo =>
         Directory.Exists(RenderedTestsDirectory) ? new DirectoryInfo(RenderedTestsDirectory) : null;
+
+    public string GetDefaultPathToModel()
+    {
+        return DefaultPathToModel;
+    }
 }