Stabilization: part XXII

VSharp.API/VSharp.API.csproj

@@ -60,6 +60,7 @@
       <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.SVM\VSharp.SVM.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" />

VSharp.API/VSharp.cs

@@ -8,6 +8,7 @@
 using System.Text;
 using VSharp.CSharpUtils;
 using VSharp.Interpreter.IL;
+using VSharp.SVM;
 
 namespace VSharp
 {
@@ -117,7 +118,7 @@ private static Statistics StartExploration(
             var baseSearchMode = options.SearchStrategy.ToSiliMode();
             // TODO: customize search strategies via console options
             var siliOptions =
-                new SiliOptions(
+                new SVMOptions(
                     explorationMode: explorationMode.NewTestCoverageMode(
                         coverageZone,
                         options.Timeout > 0 ? searchMode.NewFairMode(baseSearchMode) : baseSearchMode
@@ -135,7 +136,7 @@ private static Statistics StartExploration(
                     stepsLimit: options.StepsLimit
                 );
 
-            using var explorer = new SILI(siliOptions);
+            using var explorer = new SVM.SVM(siliOptions);
             var statistics = explorer.Statistics;
 
             void HandleInternalFail(Method? method, Exception exception)
@@ -148,6 +149,7 @@ void HandleInternalFail(Method? method, Exception exception)
                 if (exception is UnknownMethodException unknownMethodException)
                 {
                     Logger.printLogString(Logger.Error, $"Unknown method: {unknownMethodException.Method.FullName}");
+                    Logger.printLogString(Logger.Error, $"StackTrace: {unknownMethodException.InterpreterStackTrace}");
                     return;
                 }
 

VSharp.CSharpUtils/ReflectionUtils.cs

@@ -48,7 +48,9 @@ public static IEnumerable<Type> EnumerateExplorableTypes(this Assembly assembly)
         private static bool IsPublic(Type t)
         {
             Debug.Assert(t != null && t != t.DeclaringType);
-            return t.IsPublic || t.IsNestedPublic && IsPublic(t.DeclaringType);
+            return
+                t.IsPublic
+                || t is { IsNestedPublic: true, DeclaringType: not null } && IsPublic(t.DeclaringType);
         }
 
         public static IEnumerable<Type> GetExportedTypesChecked(this Assembly assembly)

VSharp.InternalCalls/Loader.fs → VSharp.IL/Loader.fs

@@ -28,7 +28,7 @@ module Loader =
     let private CSharpUtilsAssembly =
         AssemblyName("VSharp.CSharpUtils").FullName |> AssemblyManager.LoadFromAssemblyName
 
-    let public CSharpImplementations =
+    let internal CSharpImplementations =
         // Loading assembly and collecting methods via VSharp assembly load context,
         // because C# internal calls will be explored by VSharp
         seq [
@@ -51,15 +51,19 @@ module Loader =
         ]
         |> collectImplementations
 
-    let public FSharpImplementations =
-        // Loading assembly and collecting methods via default assembly load context,
-        // because all VSharp types, like VSharp.Core.state are loaded via default load context,
-        // so F# internal calls (which use state) must be loaded via default load context
-        Assembly.GetExecutingAssembly().GetTypes()
-        |> Array.filter Microsoft.FSharp.Reflection.FSharpType.IsModule
-        |> collectImplementations
+    // Loading assembly and collecting methods via default assembly load context,
+    // because all VSharp types, like VSharp.Core.state are loaded via default load context,
+    // so F# internal calls (which use state) must be loaded via default load context
+    let mutable internal FSharpImplementations : Map<string, MethodInfo> = Map.empty
+
+    let public SetInternalCallsAssembly (asm : Assembly) =
+        let implementations =
+            asm.GetTypes()
+            |> Array.filter Microsoft.FSharp.Reflection.FSharpType.IsModule
+            |> collectImplementations
+        FSharpImplementations <- implementations
 
-    let private runtimeExceptionsConstructors =
+    let internal runtimeExceptionsConstructors =
         // Loading assembly and collecting methods via VSharp assembly load context,
         // because exceptions constructors will be explored by VSharp
         CSharpUtilsAssembly.GetType("VSharp.CSharpUtils.Exceptions")
@@ -69,18 +73,9 @@ module Loader =
     let private runtimeExceptionsImplementations =
         runtimeExceptionsConstructors.Values |> Seq.map Reflection.getFullMethodName |> set
 
-    let mutable public CilStateImplementations : string seq =
-        Seq.empty
-
-    let public hasRuntimeExceptionsImplementation (fullMethodName : string) =
-        Map.containsKey fullMethodName runtimeExceptionsConstructors
-
-    let public isRuntimeExceptionsImplementation (fullMethodName : string) =
+    let internal isRuntimeExceptionsImplementation (fullMethodName : string) =
         Set.contains fullMethodName runtimeExceptionsImplementations
 
-    let public getRuntimeExceptionsImplementation (fullMethodName : string) =
-        runtimeExceptionsConstructors.[fullMethodName]
-
     let private shimImplementations =
         set [
             "System.DateTime System.DateTime.get_Now()"
@@ -92,9 +87,15 @@ module Loader =
             // Socket.Read  TODO: writing to the out parameters
         ]
 
-    let public isShimmed (fullMethodName : string) =
+    let internal isShimmed (fullMethodName : string) =
         Set.contains fullMethodName shimImplementations
 
+    let internal trustedIntrinsics =
+        let intPtr = Reflection.getAllMethods typeof<IntPtr> |> Array.map Reflection.getFullMethodName
+        let volatile = Reflection.getAllMethods typeof<System.Threading.Volatile> |> Array.map Reflection.getFullMethodName
+        let defaultComparer = [|"System.Collections.Generic.Comparer`1[T] System.Collections.Generic.Comparer`1[T].get_Default()"|]
+        Array.concat [intPtr; volatile; defaultComparer]
+
     let private concreteInvocations =
         set [
             // Types
@@ -133,6 +134,7 @@ module Loader =
             "System.RuntimeType System.ModuleHandle.GetModuleType(System.Reflection.RuntimeModule)"
             "System.Type System.RuntimeType.get_DeclaringType(this)"
             "System.String System.RuntimeType.get_Namespace(this)"
+            "System.Boolean System.Type.get_IsAbstract(this)"
 
             // EqualityComparer
             "System.Object System.Collections.Generic.ComparerHelpers.CreateDefaultEqualityComparer(System.Type)"
@@ -179,5 +181,5 @@ module Loader =
             "System.Void VSharp.CSharpUtils.Exceptions.CreateOutOfMemoryException()"
         ]
 
-    let isInvokeInternalCall (fullMethodName : string) =
+    let internal isInvokeInternalCall (fullMethodName : string) =
         concreteInvocations.Contains fullMethodName

VSharp.IL/MethodBody.fs

@@ -30,6 +30,7 @@ type MethodWithBody internal (m : MethodBase) =
     let returnType = Reflection.getMethodReturnType m
     let parameters = m.GetParameters()
     let hasThis = Reflection.hasThis m
+    let hasNonVoidResult = lazy(Reflection.hasNonVoidResult m)
     let isDynamic = m :? DynamicMethod
     let metadataToken = if isDynamic then m.GetHashCode() else m.MetadataToken
     let isStatic = m.IsStatic
@@ -45,11 +46,22 @@ type MethodWithBody internal (m : MethodBase) =
     let methodImplementationFlags = lazy m.GetMethodImplementationFlags()
     let isDelegateConstructor = lazy(Reflection.isDelegateConstructor m)
     let isDelegate = lazy(Reflection.isDelegate m)
-    let isFSharpInternalCall = lazy(Map.containsKey fullGenericMethodName.Value Loader.FSharpImplementations)
+    let tryFSharpInternalCall = lazy(Map.tryFind fullGenericMethodName.Value Loader.FSharpImplementations)
+    let isFSharpInternalCall = lazy(Option.isSome tryFSharpInternalCall.Value)
     let isCSharpInternalCall = lazy(Map.containsKey fullGenericMethodName.Value Loader.CSharpImplementations)
-    let isCilStateInternalCall = lazy(Seq.contains fullGenericMethodName.Value Loader.CilStateImplementations)
+    let isShimmed = lazy(Loader.isShimmed fullGenericMethodName.Value)
+    let isConcreteCall = lazy(Loader.isInvokeInternalCall fullGenericMethodName.Value)
+    let isRuntimeException = lazy(Loader.isRuntimeExceptionsImplementation fullGenericMethodName.Value)
+    let runtimeExceptionImpl = lazy(Map.tryFind fullGenericMethodName.Value Loader.runtimeExceptionsConstructors)
+    let isNotImplementedIntrinsic =
+        lazy(
+            let isIntrinsic =
+                let intrinsicAttr = "System.Runtime.CompilerServices.IntrinsicAttribute"
+                customAttributes |> Seq.exists (fun m -> m.AttributeType.ToString() = intrinsicAttr)
+            isIntrinsic && (Array.contains fullGenericMethodName.Value Loader.trustedIntrinsics |> not)
+        )
     let isImplementedInternalCall =
-        lazy(isFSharpInternalCall.Value || isCSharpInternalCall.Value || isCilStateInternalCall.Value)
+        lazy(isFSharpInternalCall.Value || isCSharpInternalCall.Value)
     let isInternalCall =
         lazy (
             int (m.GetMethodImplementationFlags() &&& MethodImplAttributes.InternalCall) <> 0
@@ -60,7 +72,7 @@ type MethodWithBody internal (m : MethodBase) =
         if not isCSharpInternalCall.Value then m
         else Loader.CSharpImplementations[fullGenericMethodName.Value]
     let methodBodyBytes =
-        if isFSharpInternalCall.Value || isCilStateInternalCall.Value then null
+        if isFSharpInternalCall.Value then null
         else actualMethod.GetMethodBody()
     let localVariables = if methodBodyBytes = null then null else methodBodyBytes.LocalVariables
     let methodBody = lazy(
@@ -107,6 +119,9 @@ type MethodWithBody internal (m : MethodBase) =
     member x.DeclaringType = declaringType
     member x.ReflectedType = m.ReflectedType
     member x.Parameters = parameters
+    member x.HasParameterOnStack =
+        x.DeclaringType.IsValueType && not x.IsStatic
+        || x.Parameters |> Array.exists (fun p -> p.ParameterType.IsByRef)
     member x.LocalVariables = localVariables
     member x.HasThis = hasThis
     member x.MetadataToken = metadataToken
@@ -199,6 +214,8 @@ type MethodWithBody internal (m : MethodBase) =
     member x.IsExternalMethod with get() = Reflection.isExternalMethod m
     member x.IsQCall with get() = DllManager.isQCall m
 
+    member x.HasNonVoidResult = hasNonVoidResult.Value
+
     interface VSharp.Core.IMethod with
         override x.Name = name
         override x.FullName = fullName
@@ -235,6 +252,27 @@ type MethodWithBody internal (m : MethodBase) =
     member x.IsInternalCall with get() = isInternalCall.Value
     member x.IsImplementedInternalCall with get () = isImplementedInternalCall.Value
 
+    member x.IsShimmed with get() = isShimmed.Value
+
+    member x.CanCallConcrete with get() = x.IsConcretelyInvokable && isConcreteCall.Value
+
+    member x.IsFSharpInternalCall with get() = isFSharpInternalCall.Value
+    member x.IsCSharpInternalCall with get() = isCSharpInternalCall.Value
+
+    member x.GetInternalCall with get() =
+        match tryFSharpInternalCall.Value with
+        | Some method -> method
+        | None -> internalfail $"GetInternalCall: no internal call for method {fullGenericMethodName.Value}"
+
+    member x.IsRuntimeException with get() = isRuntimeException.Value
+    member x.HasRuntimeExceptionImpl with get() = Option.isSome runtimeExceptionImpl.Value
+    member x.RuntimeExceptionImpl with get() =
+        match runtimeExceptionImpl.Value with
+        | Some ctor -> ctor
+        | None -> internalfail $"RuntimeExceptionImpl: no runtime exception implementation for method {fullGenericMethodName.Value}"
+
+    member x.IsNotImplementedIntrinsic with get() = isNotImplementedIntrinsic.Value
+
     member x.CanBeOverriden targetType =
         match m with
         | :? ConstructorInfo -> false

VSharp.IL/VSharp.IL.fsproj

@@ -14,6 +14,7 @@
     </PropertyGroup>
 
     <ItemGroup>
+      <Compile Include="Loader.fs" />
       <Compile Include="OpCodes.fs" />
       <Compile Include="ILRewriter.fs" />
       <Compile Include="MethodBody.fs" />
@@ -22,7 +23,6 @@
     </ItemGroup>
 
     <ItemGroup>
-      <ProjectReference Include="..\VSharp.InternalCalls\VSharp.InternalCalls.fsproj" />
       <ProjectReference Include="..\VSharp.SILI.Core\VSharp.SILI.Core.fsproj" />
       <ProjectReference Include="..\VSharp.Utils\VSharp.Utils.fsproj" />
     </ItemGroup>

VSharp.InternalCalls/Activator.fs

@@ -5,7 +5,7 @@ open VSharp.Core
 
 module internal Activator =
 
-    let internal CreateInstance (state : state) (args : term list) : term =
+    let internal CreateInstance (_ : state) (args : term list) : term =
         assert(List.length args = 1)
         let t = args[0] |> Helpers.unwrapType
         Memory.DefaultOf t

VSharp.InternalCalls/Activator.fsi

@@ -5,5 +5,5 @@ open VSharp.Core
 
 module internal Activator =
 
-    [<Implements("System.Object System.Activator.CreateInstance()")>]
-    val internal CreateInstance : state -> term list -> term
+    [<Implements("T System.Activator.CreateInstance()")>]
+    val CreateInstance : state -> term list -> term

VSharp.InternalCalls/Buffer.fs

@@ -6,48 +6,73 @@ open VSharp.Core
 
 // ------------------------------ System.Buffer --------------------------------
 
-module Buffer =
+module internal Buffer =
 
-    let private Memmove (state : state) dst src elemCount =
-        let elemCount = Types.Cast elemCount typeof<int>
-        let getArrayInfo ref =
-            match ref.term with
-            | Ref(ArrayIndex(address, indices, arrayType)) -> address, indices, arrayType
-            | Ref(ClassField(address, field)) when field = Reflection.stringFirstCharField ->
+    let private getArrayInfo state ref =
+        let zero = MakeNumber 0
+        match ref.term with
+        | HeapRef(address, _) ->
+            let t = MostConcreteTypeOfRef state ref
+            if TypeUtils.isArrayType t then
+                let elemType = t.GetElementType()
+                let indices, arrayType =
+                    if t.IsSZArray then [zero], (elemType, 1, true)
+                    else
+                        let rank = t.GetArrayRank()
+                        let indices = List.init rank (fun _ -> zero)
+                        let arrayType = (elemType, rank, false)
+                        indices, arrayType
+                address, indices, arrayType
+            elif t = typeof<string> then
                 let address, stringArrayType = Memory.StringArrayInfo state address None
-                address, [MakeNumber 0], stringArrayType
-            | Ptr(HeapLocation(address, t), sightType, offset) ->
-                match TryPtrToArrayInfo t sightType offset with
-                | Some(index, arrayType) ->
-                    let address =
-                        if t = typeof<string> then Memory.StringArrayInfo state address None |> fst
-                        else address
-                    address, index, arrayType
-                | None -> internalfail $"Memmove: unexpected pointer {ref}"
-            | _ -> internalfail $"Memmove: unexpected reference {ref}"
-        let dstAddr, dstIndices, dstArrayType = getArrayInfo dst
-        let srcAddr, srcIndices, srcArrayType = getArrayInfo src
+                address, [zero], stringArrayType
+            else internalfail $"Memmove: unexpected HeapRef type {t}"
+        | Ref(ArrayIndex(address, indices, arrayType)) -> address, indices, arrayType
+        | Ref(ClassField(address, field)) when field = Reflection.stringFirstCharField ->
+            let address, stringArrayType = Memory.StringArrayInfo state address None
+            address, [zero], stringArrayType
+        | Ptr(HeapLocation _ as pointerBase, sightType, offset) ->
+            match TryPtrToRef state pointerBase sightType offset with
+            | Some(ArrayIndex(address, index, arrayType)) -> address, index, arrayType
+            | _ -> internalfail $"Memmove: unexpected pointer {ref}"
+        | _ -> internalfail $"Memmove: unexpected reference {ref}"
+
+    let CommonMemmove (state : state) dst dstIndex src srcIndex elemCount =
+        let elemCount = Types.Cast elemCount typeof<int>
+        let dstAddr, dstIndices, dstArrayType = getArrayInfo state dst
+        let srcAddr, srcIndices, srcArrayType = getArrayInfo state src
         let dstType = Types.ArrayTypeToSymbolicType dstArrayType
         let srcType = Types.ArrayTypeToSymbolicType srcArrayType
         let dstHeapRef = HeapRef dstAddr dstType
         let srcHeapRef = HeapRef srcAddr srcType
         let dstLinearIndex = Memory.LinearizeArrayIndex state dstAddr dstIndices dstArrayType
+        let dstLinearIndex =
+            match dstIndex with
+            | Some dstIndex -> API.Arithmetics.Add dstLinearIndex dstIndex
+            | None -> dstLinearIndex
         let srcLinearIndex = Memory.LinearizeArrayIndex state srcAddr srcIndices srcArrayType
+        let srcLinearIndex =
+            match srcIndex with
+            | Some srcIndex -> API.Arithmetics.Add srcLinearIndex srcIndex
+            | None -> srcLinearIndex
         Memory.CopyArray state srcHeapRef srcLinearIndex srcType dstHeapRef dstLinearIndex dstType elemCount
 
-    let internal GenericMemmove (state : state) (args : term list) : term =
+    let Memmove (state : state) dst src elemCount =
+        CommonMemmove state dst None src None elemCount
+
+    let GenericMemmove (state : state) (args : term list) : term =
         assert(List.length args = 4)
         let dst, src, elemCount = args[1], args[2], args[3]
         Memmove state dst src elemCount
         Nop()
 
-    let internal ByteMemmove (state : state) (args : term list) : term =
+    let ByteMemmove (state : state) (args : term list) : term =
         assert(List.length args = 3)
         let dst, src, elemCount = args[0], args[1], args[2]
         Memmove state dst src elemCount
         Nop()
 
-    let internal MemoryCopy (state : state) (args : term list) : term =
+    let MemoryCopy (state : state) (args : term list) : term =
         assert(List.length args = 4)
         let dst, src, dstSize, count = args[0], args[1], args[2], args[3]
         // TODO: use 'dstSize' to check for exception

VSharp.InternalCalls/Buffer.fsi

@@ -6,11 +6,13 @@ open VSharp.Core
 
 module internal Buffer =
 
+    val CommonMemmove : state -> term -> term option -> term -> term option -> term -> unit
+
     [<Implements("System.Void System.Buffer.Memmove(T&, T&, System.UIntPtr)")>]
-    val internal GenericMemmove : state -> term list -> term
+    val GenericMemmove : state -> term list -> term
 
     [<Implements("System.Void System.Buffer.Memmove(System.Byte&, System.Byte&, System.UIntPtr)")>]
-    val internal ByteMemmove : state -> term list -> term
+    val ByteMemmove : state -> term list -> term
 
     [<Implements("System.Void System.Buffer.MemoryCopy(System.Void*, System.Void*, System.Int64, System.Int64)")>]
-    val internal MemoryCopy : state -> term list -> term
+    val MemoryCopy : state -> term list -> term

VSharp.InternalCalls/ByReference.fsi

@@ -6,10 +6,10 @@ open VSharp.Core
 
 module internal ByReference =
 
-    val internal isValueField : fieldId -> bool
+    val isValueField : fieldId -> bool
 
     [<Implements("System.Void System.ByReference`1[T]..ctor(this, T&)")>]
-    val internal ctor : state -> term list -> (term * state) list
+    val ctor : state -> term list -> (term * state) list
 
     [<Implements("T& System.ByReference`1[T].get_Value(this)")>]
-    val internal getValue : state -> term list -> term
+    val getValue : state -> term list -> term