Merge remote-tracking branch 'VSharpMain/master' into FromMain

PySymGym · Dec 14, 2023 · 44330ed · 44330ed
2 parents 7dab8d4 + 7089616
commit 44330ed
Show file tree

Hide file tree

Showing 693 changed files with 130,043 additions and 33,597 deletions.
diff --git a/.github/workflows/build_vsharp.yml b/.github/workflows/build_vsharp.yml
@@ -20,12 +20,12 @@ jobs:
           ${{ runner.os }}-nuget-
     - name: Build VSharp
       run:
-        dotnet build -c Release
+        dotnet build -c DebugTailRec
     - uses: actions/upload-artifact@v3
       with:
         name: runner
-        path: ./VSharp.Runner/bin/Release/netcoreapp6.0
+        path: ./VSharp.Runner/bin/DebugTailRec/net7.0
     - uses: actions/upload-artifact@v3
       with:
         name: test_runner
-        path: ./VSharp.TestRunner/bin/Release/netcoreapp6.0
+        path: ./VSharp.TestRunner/bin/DebugTailRec/net7.0
diff --git a/.github/workflows/integration_tests.yml b/.github/workflows/integration_tests.yml
@@ -26,8 +26,8 @@ jobs:
     - name: Run tests
       run: |
         dotnet tool restore
-        dotnet test -c Release --logger "trx;LogFileName=tests-results.trx"
-        dotnet test -c Release --filter TestCategory=Generated --logger "trx;LogFileName=generated-tests-results.trx"
+        dotnet test -c DebugTailRec --logger "trx;LogFileName=tests-results.trx"
+        dotnet test -c Release --filter "TestCategory=Generated&TestCategory!=FatalError" --logger "trx;LogFileName=generated-tests-results.trx"
     - name: Upload tests results to GitHub artifacts
       uses: actions/upload-artifact@v3
       if: success() || failure()

diff --git a/VSharp.API/VSharp.API.csproj b/VSharp.API/VSharp.API.csproj
@@ -36,47 +36,46 @@
     </ItemGroup>
 
     <PropertyGroup>
-        <TargetFramework>netcoreapp6.0</TargetFramework>
+        <TargetFramework>net7.0</TargetFramework>
     </PropertyGroup>
 
     <PropertyGroup>
-      <TargetsForTfmSpecificBuildOutput>$(TargetsForTfmSpecificBuildOutput);CopyProjectReferencesToPackage</TargetsForTfmSpecificBuildOutput>
+        <TargetsForTfmSpecificBuildOutput>$(TargetsForTfmSpecificBuildOutput);CopyProjectReferencesToPackage</TargetsForTfmSpecificBuildOutput>
     </PropertyGroup>
 
     <Target Name="CopyProjectReferencesToPackage" DependsOnTargets="BuildOnlySettings;ResolveReferences">
-      <ItemGroup>
-        <_ReferenceCopyLocalPaths Include="@(ReferenceCopyLocalPaths-&gt;WithMetadataValue('ReferenceSourceTarget', 'ProjectReference')-&gt;WithMetadataValue('PrivateAssets', 'All'))" />
-      </ItemGroup>
+        <ItemGroup>
+            <_ReferenceCopyLocalPaths Include="@(ReferenceCopyLocalPaths-&gt;WithMetadataValue('ReferenceSourceTarget', 'ProjectReference')-&gt;WithMetadataValue('PrivateAssets', 'All'))" />
+        </ItemGroup>
 
-      <ItemGroup>
-        <BuildOutputInPackage Include="@(_ReferenceCopyLocalPaths)" TargetPath="%(_ReferenceCopyLocalPaths.DestinationSubDirectory)" />
-      </ItemGroup>
+        <ItemGroup>
+            <BuildOutputInPackage Include="@(_ReferenceCopyLocalPaths)" TargetPath="%(_ReferenceCopyLocalPaths.DestinationSubDirectory)" />
+        </ItemGroup>
     </Target>
 
     <ItemGroup>
-      <ProjectReference Include="..\VSharp.CSharpUtils\VSharp.CSharpUtils.csproj" PrivateAssets="all" />
-      <ProjectReference Include="..\VSharp.IL\VSharp.IL.fsproj" PrivateAssets="all" />
-      <ProjectReference Include="..\VSharp.InternalCalls\VSharp.InternalCalls.fsproj" PrivateAssets="all" />
-      <ProjectReference Include="..\VSharp.SILI\VSharp.SILI.fsproj" PrivateAssets="all" />
-      <ProjectReference Include="..\VSharp.SILI.Core\VSharp.SILI.Core.fsproj" PrivateAssets="all" />
-      <ProjectReference Include="..\VSharp.Solver\VSharp.Solver.fsproj" PrivateAssets="all" />
-      <ProjectReference Include="..\VSharp.TestExtensions\VSharp.TestExtensions.csproj" PrivateAssets="all" />
-      <ProjectReference Include="..\VSharp.TestRenderer\VSharp.TestRenderer.csproj" PrivateAssets="all" />
-      <ProjectReference Include="..\VSharp.TestRunner\VSharp.TestRunner.csproj" PrivateAssets="all" />
-      <ProjectReference Include="..\VSharp.Utils\VSharp.Utils.fsproj" PrivateAssets="all" />
+        <ProjectReference Include="..\VSharp.CSharpUtils\VSharp.CSharpUtils.csproj" PrivateAssets="all" />
+        <ProjectReference Include="..\VSharp.IL\VSharp.IL.fsproj" PrivateAssets="all" />
+        <ProjectReference Include="..\VSharp.InternalCalls\VSharp.InternalCalls.fsproj" PrivateAssets="all" />
+        <ProjectReference Include="..\VSharp.SILI\VSharp.SILI.fsproj" PrivateAssets="all" />
+        <ProjectReference Include="..\VSharp.SILI.Core\VSharp.SILI.Core.fsproj" PrivateAssets="all" />
+        <ProjectReference Include="..\VSharp.Solver\VSharp.Solver.fsproj" PrivateAssets="all" />
+        <ProjectReference Include="..\VSharp.Explorer\VSharp.Explorer.fsproj" />
+        <ProjectReference Include="..\VSharp.TestExtensions\VSharp.TestExtensions.csproj" PrivateAssets="all" />
+        <ProjectReference Include="..\VSharp.TestRenderer\VSharp.TestRenderer.csproj" PrivateAssets="all" />
+        <ProjectReference Include="..\VSharp.TestRunner\VSharp.TestRunner.csproj" PrivateAssets="all" />
+        <ProjectReference Include="..\VSharp.Utils\VSharp.Utils.fsproj" PrivateAssets="all" />
     </ItemGroup>
 
     <ItemGroup>
-      <PackageReference Include="CsvHelper" Version="30.0.1" />
-      <PackageReference Include="FSharp.Core" Version="7.0.300" />
-      <PackageReference Include="FSharpx.Collections" Version="3.1.0" />
-      <PackageReference Include="Microsoft.Extensions.DependencyInjection" Version="2.0.0" />
-      <PackageReference Include="Microsoft.Extensions.DependencyModel" Version="3.0.0" />
-      <PackageReference Include="System.CommandLine" Version="2.0.0-beta1.21308.1" />
-      <PackageReference Include="JetBrains.Roslyn.References.Repack" Version="42.42.20220228.125130" />
-      <PackageReference Include="Microsoft.Z3.x64" Version="4.8.6" />
-      <PackageReference Include="vsteam.Z3.M1" Version="4.8.11-alpha.2" />
-      <PackageReference Include="System.CommandLine" Version="2.0.0-beta1.21308.1" />
+        <PackageReference Include="CsvHelper" Version="30.0.1" />
+        <PackageReference Include="FSharp.Core" Version="7.0.*" />
+        <PackageReference Include="FSharpx.Collections" Version="3.1.0" />
+        <PackageReference Include="Microsoft.Extensions.DependencyInjection" Version="2.0.0" />
+        <PackageReference Include="Microsoft.Extensions.DependencyModel" Version="3.0.0" />
+        <PackageReference Include="System.CommandLine" Version="2.0.0-beta1.21308.1" />
+        <PackageReference Include="JetBrains.Roslyn.References.Repack" Version="42.42.20220228.125130" />
+        <PackageReference Include="System.CommandLine" Version="2.0.0-beta1.21308.1" />
+        <PackageReference Include="VSTeam.Z3" Version="4.11.2-alpha" />
     </ItemGroup>
-
 </Project>
diff --git a/VSharp.API/VSharp.cs b/VSharp.API/VSharp.cs
@@ -1,7 +1,6 @@
 #nullable enable
 using System;
 using System.Collections.Generic;
-using System.Diagnostics;
 using System.IO;
 using System.Linq;
 using System.Net.WebSockets;
@@ -10,6 +9,7 @@
 using VSharp.CSharpUtils;
 using VSharp.IL;
 using VSharp.Interpreter.IL;
+using VSharp.Explorer;
 
 namespace VSharp
 {
@@ -80,6 +80,7 @@ public void GenerateReport(TextWriter writer)
         {
             writer.WriteLine("Total time: {0:00}:{1:00}:{2:00}.{3}.", TestGenerationTime.Hours,
                 TestGenerationTime.Minutes, TestGenerationTime.Seconds, TestGenerationTime.Milliseconds);
+            writer.WriteLine("Total coverage: {0}", GeneratedTestInfos.LastOrDefault().Coverage);
             var count = IncompleteBranches.Count();
             if (count > 0)
             {
@@ -106,31 +107,82 @@ public IEnumerable<FileInfo> Results()
 
     public static class TestGenerator
     {
+        private class Reporter: IReporter
+        {
+            private readonly UnitTests _unitTests;
+            private readonly bool _isQuiet;
+
+            public Reporter(UnitTests unitTests, bool isQuiet)
+            {
+                _unitTests = unitTests;
+                _isQuiet = isQuiet;
+            }
+
+            public void ReportFinished(UnitTest unitTest) => _unitTests.GenerateTest(unitTest);
+            public void ReportException(UnitTest unitTest) => _unitTests.GenerateError(unitTest);
+            public void ReportIIE(InsufficientInformationException iie) {}
+
+            public void ReportInternalFail(Method? method, Exception exn)
+            {
+                if (_isQuiet) return;
+
+                if (exn is UnknownMethodException unknownMethodException)
+                {
+                    Logger.printLogString(Logger.Error, $"Unknown method: {unknownMethodException.Method.FullName}, {unknownMethodException.Message}");
+                    Logger.printLogString(Logger.Error, $"StackTrace: {unknownMethodException.InterpreterStackTrace}");
+                    return;
+                }
+
+                var messageBuilder = new StringBuilder();
+
+                if (method is not null)
+                {
+                    messageBuilder.AppendLine($"Explored method: {method.DeclaringType}.{method.Name}");
+                }
+
+                messageBuilder.AppendLine($"Exception: {exn.GetType()} {exn.Message}");
+
+                var trace = exn.StackTrace;
+                if (trace is not null)
+                {
+                    messageBuilder.AppendLine(trace);
+                }
+
+                Logger.printLogString(Logger.Error, messageBuilder.ToString());
+            }
+
+            public void ReportCrash(Exception exn)
+            {
+                if (_isQuiet) return;
+                Logger.printLogString(Logger.Critical, $"{exn}");
+            }
+        }
+
         private static Statistics StartExploration(
             IEnumerable<MethodBase> methods,
             coverageZone coverageZone,
             VSharpOptions options,
             string[]? mainArguments = null)
         {
-            Logger.currentLogLevel = options.Verbosity.ToLoggerLevel();
+            Logger.changeVerbosityTuple(Logger.defaultTag, options.Verbosity.ToLoggerLevel());
 
             var unitTests = new UnitTests(options.OutputDirectory);
             var baseSearchMode = options.SearchStrategy.ToSiliMode();
             // TODO: customize search strategies via console options
+
             var siliOptions =
-                new SiliOptions(
+                new SVMOptions(
                     explorationMode: explorationMode.NewTestCoverageMode(
                         coverageZone,
                         //timeout > 0 ? searchMode.NewFairMode(baseSearchMode) : baseSearchMode
                         baseSearchMode
                     ),
-                    outputDirectory: unitTests.TestDirectory,
                     recThreshold: options.RecursionThreshold,
-                    timeout: options.Timeout,
                     solverTimeout: options.SolverTimeout,
                     visualize: false,
                     releaseBranches: options.ReleaseBranches,
                     maxBufferSize: 128,
+                    prettyChars: true,
                     checkAttributes: true,
                     stopOnCoverageAchieved: 100,
                     randomSeed: options.RandomSeed,
@@ -141,53 +193,29 @@ private static Statistics StartExploration(
                     serialize:false,
                     pathToSerialize:"");
 
-            using var explorer = new SILI(siliOptions);
-            var statistics = explorer.Statistics;
+            var fuzzerOptions =
+                new FuzzerOptions(
+                    isolation: fuzzerIsolation.Process,
+                    coverageZone: coverageZone
+                );
 
-            void HandleInternalFail(Method? method, Exception exception)
+            var explorationModeOptions = options.ExplorationMode switch
             {
-                if (options.Verbosity == Verbosity.Quiet)
-                {
-                    return;
-                }
-
-                if (exception is UnknownMethodException unknownMethodException)
-                {
-                    Logger.printLogString(Logger.Error, $"Unknown method: {unknownMethodException.Method.FullName}");
-                    return;
-                }
-
-                var messageBuilder = new StringBuilder();
-
-                if (method is not null)
-                {
-                    messageBuilder.AppendLine($"Explored method: {method.DeclaringType}.{method.Name}");
-                }
-
-                messageBuilder.Append($"Exception: {exception.GetType()} {exception.Message}");
-
-                var trace = new StackTrace(exception, true);
-                var frame = trace.GetFrame(0);
-
-                if (frame is not null)
-                {
-                    messageBuilder.AppendLine();
-                    messageBuilder.Append($"At: {frame.GetFileName()}, {frame.GetFileLineNumber()}");
-                }
-
-                Logger.printLogString(Logger.Error, messageBuilder.ToString());
-            }
+                ExplorationMode.Fuzzing => Explorer.explorationModeOptions.NewFuzzing(fuzzerOptions),
+                ExplorationMode.Sili => Explorer.explorationModeOptions.NewSVM(siliOptions),
+                ExplorationMode.Interleaving => Explorer.explorationModeOptions.NewCombined(siliOptions, fuzzerOptions),
+                _ => throw new ArgumentOutOfRangeException($"StartExploration: unexpected exploration mode {options.ExplorationMode}")
+            };
 
-            void HandleCrash(Exception exception)
-            {
-                if (options.Verbosity == Verbosity.Quiet)
-                {
-                    return;
-                }
+            var explorationOptions = new ExplorationOptions(
+                timeout: options.Timeout == -1 ? TimeSpanBuilders.Infinite : TimeSpanBuilders.FromSeconds(options.Timeout),
+                outputDirectory: unitTests.TestDirectory,
+                explorationModeOptions: explorationModeOptions
+            );
 
-                Logger.printLogString(Logger.Critical, $"{exception}");
-            }
+            using var explorer = new Explorer.Explorer(explorationOptions, new Reporter(unitTests, options.Verbosity == Verbosity.Quiet));
 
+            var statistics = explorer.Statistics;
             var isolated = new List<MethodBase>();
             var entryPoints = new List<Tuple<MethodBase, string[]?>>();
 
@@ -204,33 +232,25 @@ void HandleCrash(Exception exception)
                 }
             }
 
-            var testInfos = new List<GeneratedTestInfo>();
-
-            void OnTest(UnitTest test)
-            {
-                var coverage = statistics.GetCurrentCoverage();
-                testInfos.Add(new GeneratedTestInfo(false, statistics.CurrentExplorationTime, statistics.StepsCount, coverage));
-                unitTests.GenerateTest(test);
-            }
-
-            void OnError(UnitTest test)
-            {
-                var coverage = statistics.GetCurrentCoverage();
-                testInfos.Add(new GeneratedTestInfo(true, statistics.CurrentExplorationTime, statistics.StepsCount, coverage));
-                unitTests.GenerateError(test);
-            }
+            explorer.StartExploration(isolated, entryPoints);
 
-            explorer.Interpret(isolated, entryPoints, OnTest, OnError, _ => { },
-                HandleInternalFail, HandleCrash);
+            var generatedTestInfos = statistics.GeneratedTestInfos.Select(i =>
+                new GeneratedTestInfo(
+                    IsError: i.isError,
+                    ExecutionTime: i.executionTime,
+                    StepsCount: i.stepsCount,
+                    Coverage: i.coverage
+                )
+            );
 
             var result = new Statistics(
                 statistics.CurrentExplorationTime,
                 unitTests.TestDirectory,
                 unitTests.UnitTestsCount,
                 unitTests.ErrorsCount,
                 statistics.StepsCount,
-                statistics.IncompleteStates.Select(e => e.iie.Value.Message).Distinct(),
-                testInfos);
+                statistics.IncompleteStates.Select(s => s.iie.Value.Message).Distinct(),
+                generatedTestInfos);
             unitTests.WriteReport(statistics.PrintStatistics);
 
             return result;