Merge pull request #310 from MchKosticyn/master

Stabilization: part XXXIII

VSharp.API/VSharp.cs

@@ -242,7 +242,7 @@ private static Statistics StartExploration(
                 unitTests.UnitTestsCount,
                 unitTests.ErrorsCount,
                 statistics.StepsCount,
-                statistics.IncompleteStates.Select(e => e.iie.Value.Message).Distinct(),
+                statistics.IncompleteStates.Select(s => s.iie.Value.Message).Distinct(),
                 generatedTestInfos);
             unitTests.WriteReport(statistics.PrintStatistics);
 

VSharp.API/VSharpOptions.cs

@@ -82,34 +82,77 @@ public enum ExplorationMode
     Interleaving
 }
 
-/// <summary>
-/// Symbolic virtual machine options.
-/// </summary>
-/// <param name="Timeout">Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interruption).</param>
-/// <param name="SolverTimeout">Timeout for SMT solver in seconds. Negative value means no timeout.</param>
-/// <param name="OutputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
-/// <param name="RenderedTestsDirectory">Directory to place the project with rendered NUnit tests (if <see cref="RenderTests"/> is enabled). If null or empty, parent of process working directory is used.</param>
-/// <param name="RenderTests">If true, NUnit tests are rendered.</param>
-/// <param name="SearchStrategy">Strategy which symbolic virtual machine uses for branch selection.</param>
-/// <param name="Verbosity">Determines which messages are displayed in output.</param>
-/// <param name="RecursionThreshold">If greater than zero, terminate exploration of states which have visited the same loop entry or method more times than the value.</param>
-/// <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>
-public readonly record struct VSharpOptions(
-    int Timeout = -1,
-    int SolverTimeout = -1,
-    string OutputDirectory = "",
-    string RenderedTestsDirectory = "",
-    bool RenderTests = false,
-    SearchStrategy SearchStrategy = SearchStrategy.BFS,
-    Verbosity Verbosity = Verbosity.Quiet,
-    uint RecursionThreshold = 0u,
-    ExplorationMode ExplorationMode = ExplorationMode.Sili,
-    bool ReleaseBranches = true,
-    int RandomSeed = -1,
-    uint StepsLimit = 0)
+public readonly record struct VSharpOptions
 {
+    private const int DefaultTimeout = -1;
+    private const int DefaultSolverTimeout = -1;
+    private const string DefaultOutputDirectory = "";
+    private const string DefaultRenderedTestsDirectory = "";
+    private const bool DefaultRenderTests = false;
+    private const SearchStrategy DefaultSearchStrategy = SearchStrategy.BFS;
+    private const Verbosity DefaultVerbosity = Verbosity.Quiet;
+    private const uint DefaultRecursionThreshold = 0u;
+    private const ExplorationMode DefaultExplorationMode = ExplorationMode.Sili;
+    private const bool DefaultReleaseBranches = true;
+    private const int DefaultRandomSeed = -1;
+    private const uint DefaultStepsLimit = 0;
+
+    public readonly int Timeout = DefaultTimeout;
+    public readonly int SolverTimeout = DefaultSolverTimeout;
+    public readonly string OutputDirectory = DefaultOutputDirectory;
+    public readonly string RenderedTestsDirectory = DefaultRenderedTestsDirectory;
+    public readonly bool RenderTests = DefaultRenderTests;
+    public readonly SearchStrategy SearchStrategy = DefaultSearchStrategy;
+    public readonly Verbosity Verbosity = DefaultVerbosity;
+    public readonly uint RecursionThreshold = DefaultRecursionThreshold;
+    public readonly ExplorationMode ExplorationMode = DefaultExplorationMode;
+    public readonly bool ReleaseBranches = DefaultReleaseBranches;
+    public readonly int RandomSeed = DefaultRandomSeed;
+    public readonly uint StepsLimit = DefaultStepsLimit;
+
+    /// <summary>
+    /// Symbolic virtual machine options.
+    /// </summary>
+    /// <param name="timeout">Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interruption).</param>
+    /// <param name="solverTimeout">Timeout for SMT solver in seconds. Negative value means no timeout.</param>
+    /// <param name="outputDirectory">Directory to place generated *.vst tests. If null or empty, process working directory is used.</param>
+    /// <param name="renderedTestsDirectory">Directory to place the project with rendered NUnit tests (if <see cref="renderTests"/> is enabled). If null or empty, parent of process working directory is used.</param>
+    /// <param name="renderTests">If true, NUnit tests are rendered.</param>
+    /// <param name="searchStrategy">Strategy which symbolic virtual machine uses for branch selection.</param>
+    /// <param name="verbosity">Determines which messages are displayed in output.</param>
+    /// <param name="recursionThreshold">If greater than zero, terminate exploration of states which have visited the same loop entry or method more times than the value.</param>
+    /// <param name="explorationMode">Determines which mode is used for exploration.</param>
+    /// <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>
+    public VSharpOptions(
+        int timeout = DefaultTimeout,
+        int solverTimeout = DefaultSolverTimeout,
+        string outputDirectory = DefaultOutputDirectory,
+        string renderedTestsDirectory = DefaultRenderedTestsDirectory,
+        bool renderTests = DefaultRenderTests,
+        SearchStrategy searchStrategy = DefaultSearchStrategy,
+        Verbosity verbosity = DefaultVerbosity,
+        uint recursionThreshold = DefaultRecursionThreshold,
+        ExplorationMode explorationMode = DefaultExplorationMode,
+        bool releaseBranches = DefaultReleaseBranches,
+        int randomSeed = DefaultRandomSeed,
+        uint stepsLimit = DefaultStepsLimit)
+    {
+        Timeout = timeout;
+        SolverTimeout = solverTimeout;
+        OutputDirectory = outputDirectory;
+        RenderedTestsDirectory = renderedTestsDirectory;
+        RenderTests = renderTests;
+        SearchStrategy = searchStrategy;
+        Verbosity = verbosity;
+        RecursionThreshold = recursionThreshold;
+        ExplorationMode = explorationMode;
+        ReleaseBranches = releaseBranches;
+        RandomSeed = randomSeed;
+        StepsLimit = stepsLimit;
+    }
+
     /// <summary>
     /// <seealso cref="RenderedTestsDirectory"/>
     /// </summary>

VSharp.CSharpUtils/VSharpAssemblyLoadContext.cs

@@ -11,6 +11,11 @@ namespace VSharp.CSharpUtils
 {
     public class VSharpAssemblyLoadContext : AssemblyLoadContext, IDisposable
     {
+        private static string GetTypeName(Type t)
+        {
+            return t.AssemblyQualifiedName ?? t.FullName ?? t.Name;
+        }
+
         private readonly Dictionary<string, AssemblyDependencyResolver> _resolvers = new();
 
         private readonly Dictionary<string, Assembly> _assemblies = new();
@@ -106,7 +111,7 @@ protected override IntPtr LoadUnmanagedDll(string unmanagedDllName)
                     continue;
                 }
 
-                _types[type.FullName] = type;
+                _types[GetTypeName(type)] = type;
             }
             return asm;
         }
@@ -140,7 +145,7 @@ public Type NormalizeType(Type t)
                 return normalized.MakeGenericType(fixedGenericTypes);
             }
 
-            var name = t.FullName ?? t.Name;
+            var name = GetTypeName(t);
             if (_types.TryGetValue(name, out var normalizedType))
             {
                 return normalizedType;

VSharp.Explorer/BidirectionalSearcher.fs

@@ -5,6 +5,7 @@ open FSharpx.Collections
 
 open VSharp
 open VSharp.Interpreter.IL
+open CilState
 
 type BidirectionalSearcher(forward : IForwardSearcher, backward : IBackwardSearcher, targeted : ITargetedSearcher) =
 
@@ -44,7 +45,7 @@ type BidirectionalSearcher(forward : IForwardSearcher, backward : IBackwardSearc
         override x.UpdatePobs parent child =
             backward.Update parent child
         override x.UpdateStates parent children =
-            if not <| CilStateOperations.isIsolated parent then
+            if not parent.IsIsolated then
                 forward.Update (parent, children)
                 backward.AddBranch parent |> ignore
                 Seq.iter (backward.AddBranch >> ignore) children
@@ -128,8 +129,8 @@ type BackwardSearcher() =
         ancestorOf[child].Add(parent)
         doAddPob child
 
-    let updateQBack s : pob list =
-        match IpOperations.ip2codeLocation (CilStateOperations.currentIp s) with
+    let updateQBack (s : cilState) : pob list =
+        match s.CurrentIp.ToCodeLocation() with
         | None -> []
         | Some loc ->
             let pobsList = ref null
@@ -208,13 +209,12 @@ type BackwardSearcher() =
         override x.StatesCount with get() = qBack.Count
 
 module DummyTargetedSearcher =
-    open CilStateOperations
 
     type DummyTargetedSearcher() =
-        let forPropagation = Dictionary<ip, List<cilState>>()
-        let finished = Dictionary<ip, List<cilState>>()
-        let reached = Dictionary<ip, List<cilState>>()
-        let targets = Dictionary<ip, List<ip>>()
+        let forPropagation = Dictionary<instructionPointer, List<cilState>>()
+        let finished = Dictionary<instructionPointer, List<cilState>>()
+        let reached = Dictionary<instructionPointer, List<cilState>>()
+        let targets = Dictionary<instructionPointer, List<instructionPointer>>()
 
         let addReached from s =
             let mutable l = ref null
@@ -226,9 +226,9 @@ module DummyTargetedSearcher =
         let add (s : cilState) : cilState seq =
             let from = s.startingIP
             assert(targets.ContainsKey from)
-            let current = currentIp s
+            let current = s.CurrentIp
 
-            if isIIEState s || isUnhandledExceptionOrError s || not(isExecutable(s)) then
+            if s.IsIIEState || s.IsUnhandledExceptionOrError || not s.IsExecutable then
                 finished[from].Add(s); Seq.empty
             elif targets[from].Contains(current) then addReached from s
             else
@@ -238,7 +238,7 @@ module DummyTargetedSearcher =
 
         interface ITargetedSearcher with
             override x.SetTargets from tos =
-                if not (targets.ContainsKey from) then targets.Add(from, List<ip>())
+                if not (targets.ContainsKey from) then targets.Add(from, List<instructionPointer>())
                 targets[from].AddRange(tos)
 
             override x.Update parent children =

VSharp.Explorer/DFSSortedByContributedCoverageSearcher.fs

@@ -3,7 +3,7 @@ namespace VSharp.Explorer
 open System.Collections.Generic
 open Microsoft.FSharp.Core
 open VSharp
-open VSharp.Interpreter.IL
+open VSharp.Interpreter.IL.CilState
 open System.Linq
 
 /// <summary>

VSharp.Explorer/DistanceWeighter.fs

@@ -4,8 +4,7 @@ open System
 
 open VSharp
 open VSharp.Interpreter.IL
-open VSharp.Interpreter.IL.CilStateOperations
-open VSharp.Interpreter.IL.IpOperations
+open VSharp.Interpreter.IL.CilState
 
 type ShortestDistanceWeighter(target : codeLocation) =
     let infinity = UInt32.MaxValue
@@ -38,9 +37,9 @@ type ShortestDistanceWeighter(target : codeLocation) =
          |> Seq.min
 
     let calculateCallWeight (state : cilState) =
-        let suitable ip =
-            match offsetOf ip with
-            | Some offset -> Some (forceMethodOf ip, offset)
+        let suitable (ip : instructionPointer) =
+            match ip.Offset with
+            | Some offset -> Some (ip.ForceMethod(), offset)
             | None -> None
         let calculateWeight frameNumber (method, offset) =
             // TODO: do not execute this for frames with frameNumber > current minimum
@@ -90,7 +89,7 @@ type ShortestDistanceWeighter(target : codeLocation) =
     interface IWeighter with
         override x.Weight(state) =
             option {
-                match tryCurrentLoc state with
+                match state.TryCurrentLoc with
                 | Some currLoc ->
                     let! callWeight = calculateCallWeight state
                     let! weight =
@@ -115,8 +114,8 @@ type IntraproceduralShortestDistanceToUncoveredWeighter(statistics : SVMStatisti
 
     interface IWeighter with
         override x.Weight(state) =
-            let calculateWeight ip =
-                match ip2codeLocation ip, ip with
+            let calculateWeight (ip : instructionPointer) =
+                match ip.ToCodeLocation(), ip with
                 | Some loc, _ when loc.method.InCoverageZone -> minDistance loc.method loc.offset |> Some
                 | Some _, _-> None
                 | None, SearchingForHandler(_, _, toObserve, _) ->

VSharp.Explorer/ExecutionTreeSearcher.fs

@@ -5,6 +5,7 @@ open System.Collections.Generic
 
 open VSharp
 open VSharp.Interpreter.IL
+open CilState
 
 type internal ExecutionTreeSearcher(randomSeed : int option) =
 
@@ -20,10 +21,10 @@ type internal ExecutionTreeSearcher(randomSeed : int option) =
 
     let rec getAllStates() = Seq.collect (fun (t : ExecutionTree<cilState>) -> t.States) trees.Values
 
-    let init initialStates =
+    let init (initialStates : cilState seq) =
         if trees.Count > 0 then
             invalidOp "Trying to init non-empty execution tree searcher"
-        for method, methodStates in initialStates |> Seq.groupBy CilStateOperations.entryMethodOf do
+        for method, methodStates in initialStates |> Seq.groupBy (fun s -> s.EntryMethod) do
             methods.Add method
             if Seq.length methodStates > 1 then
                 invalidOp "Cannot init execution tree searcher with more than 1 initial state for method"
@@ -50,8 +51,8 @@ type internal ExecutionTreeSearcher(randomSeed : int option) =
             // Fallback (inefficient, in case of plain fair searcher should not happen)
             getAllStates() |> Seq.tryFind selector
 
-    let remove state =
-        let entryMethod = CilStateOperations.entryMethodOf state
+    let remove (state : cilState) =
+        let entryMethod = state.EntryMethod
         let tree = ref null
         let treeFound = trees.TryGetValue(entryMethod, tree)
         if treeFound then
@@ -67,8 +68,8 @@ type internal ExecutionTreeSearcher(randomSeed : int option) =
         trees.Clear()
         methods.Clear()
 
-    let update parent newStates =
-        let entryMethod = CilStateOperations.entryMethodOf parent
+    let update (parent : cilState) newStates =
+        let entryMethod = parent.EntryMethod
         let tree = ref null
         let treeFound = trees.TryGetValue(entryMethod, tree)
         if treeFound then