Stabilization: part XXIV

VSharp.API/VSharp.cs

@@ -148,7 +148,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, $"Unknown method: {unknownMethodException.Method.FullName}, {unknownMethodException.Message}");
                     Logger.printLogString(Logger.Error, $"StackTrace: {unknownMethodException.InterpreterStackTrace}");
                     return;
                 }

VSharp.CSharpUtils/CultureInfoUtils.cs

@@ -2,6 +2,6 @@
 
 public static class CultureInfoUtils
 {
-    [Implements("System.Void System.Globalization.CultureInfo..cctor()")]
+    // [Implements("System.Void System.Globalization.CultureInfo..cctor()")]
     public static void CultureInfoStaticConstructor() { }
 }

VSharp.CSharpUtils/GCUtils.cs

@@ -21,5 +21,10 @@ public static object GCHandleInternalGet(IntPtr ptr)
         public static void KeepAlive(object ptr)
         {
         }
+
+        [Implements("System.Void System.GC._SuppressFinalize(System.Object)")]
+        public static void SuppressFinalize(object obj)
+        {
+        }
     }
 }

VSharp.CSharpUtils/StringUtils.cs

@@ -13,6 +13,15 @@ public static int GetHashCode(string str)
         [Implements("System.Boolean System.String.Equals(this, System.String)")]
         public static bool Equals(string str1, string str2)
         {
+            if (string.IsNullOrEmpty(str1) && string.IsNullOrEmpty(str2))
+                return true;
+
+            if (string.IsNullOrEmpty(str1))
+                return false;
+
+            if (string.IsNullOrEmpty(str2))
+                return false;
+
             if (str1.Length != str2.Length)
                 return false;
 
@@ -24,5 +33,29 @@ public static bool Equals(string str1, string str2)
 
             return true;
         }
+
+        [Implements("System.Boolean System.String.Equals(System.String, System.String, System.StringComparison)")]
+        public static bool EqualsWithComparison(string str1, string str2, System.StringComparison comparison)
+        {
+            return Equals(str1, str2);
+        }
+
+        [Implements("System.Boolean System.String.StartsWith(this, System.String, System.StringComparison)")]
+        public static bool StartsWith(string str1, string str2, System.StringComparison comparison)
+        {
+            var len1 = str1.Length;
+            var len2 = str2.Length;
+
+            if (len2 > len1)
+                return false;
+
+            for (var i = 0; i < len2; i++)
+            {
+                if (str1[i] != str2[i])
+                    return false;
+            }
+
+            return true;
+        }
     }
 }

VSharp.IL/Loader.fs

@@ -94,7 +94,13 @@ module Loader =
         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 string = [|"System.Boolean System.String.StartsWith(this, System.String, System.StringComparison)"|]
+        let span = [|
+            "System.Boolean System.MemoryExtensions.StartsWith(System.ReadOnlySpan`1[T], System.ReadOnlySpan`1[T])"
+            "System.Boolean System.SpanHelpers.SequenceEqual(System.Byte&, System.Byte&, System.UIntPtr)"
+        |]
+        let vector = [|"System.Int32 System.Numerics.Vector`1[T].get_Count()"|]
+        Array.concat [intPtr; volatile; defaultComparer; string; span; vector]
 
     let private concreteInvocations =
         set [
@@ -135,6 +141,10 @@ module Loader =
             "System.Type System.RuntimeType.get_DeclaringType(this)"
             "System.String System.RuntimeType.get_Namespace(this)"
             "System.Boolean System.Type.get_IsAbstract(this)"
+            "System.Object[] System.Reflection.RuntimeAssembly.GetCustomAttributes(this, System.Type, System.Boolean)"
+
+            // Assembly
+            "System.String System.Reflection.RuntimeAssembly.get_Location(this)"
 
             // EqualityComparer
             "System.Object System.Collections.Generic.ComparerHelpers.CreateDefaultEqualityComparer(System.Type)"
@@ -162,6 +172,23 @@ module Loader =
             // Environment
             "System.Int32 System.Environment.get_TickCount()"
             "System.Boolean System.Numerics.Vector.get_IsHardwareAccelerated()"
+            "System.String System.Environment.GetEnvironmentVariable(System.String)"
+
+            // Guid
+            "System.Guid System.Guid.NewGuid()"
+
+            // CultureInfo
+            "System.Globalization.CultureInfo System.Globalization.CultureInfo.get_CurrentCulture()"
+            "System.Globalization.CultureInfo System.Globalization.CultureInfo.get_InvariantCulture()"
+            "System.Globalization.CompareInfo System.Globalization.CultureInfo.get_CompareInfo(this)"
+            "System.Boolean System.Globalization.GlobalizationMode.get_Invariant()"
+            "System.String System.Globalization.CultureInfo.get_Name(this)"
+            "System.Globalization.CultureInfo System.Globalization.CultureInfo.GetCultureInfo(System.String)"
+            "System.Globalization.CultureData System.Globalization.CultureData.GetCultureData(System.String, System.Boolean)"
+
+            // ResourceManager
+            "System.Void System.Resources.ResourceManager..ctor(this, System.String, System.Reflection.Assembly)"
+            "System.String System.Resources.ResourceManager.GetString(this, System.String, System.Globalization.CultureInfo)"
 
             // Buffers
             "System.Buffers.TlsOverPerCoreLockedStacksArrayPool`1+ThreadLocalArray[T][] System.Buffers.TlsOverPerCoreLockedStacksArrayPool`1[T].InitializeTlsBucketsAndTrimming(this)"

VSharp.InternalCalls/Buffer.fs

@@ -10,47 +10,25 @@ open VSharp.Interpreter.IL.CilStateOperations
 
 module internal Buffer =
 
-    let private getArrayInfo cilState ref =
+    let private getAddress cilState ref =
         let state = cilState.state
-        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
-                (Some (address, indices, arrayType), cilState) |> List.singleton
-            elif t = typeof<string> then
-                let address, stringArrayType = Memory.StringArrayInfo state address None
-                (Some (address, [zero], stringArrayType), cilState) |> List.singleton
-            else internalfail $"Memmove: unexpected HeapRef type {t}"
-        | Ref(ArrayIndex(address, indices, arrayType)) ->
-            (Some (address, indices, arrayType), cilState) |> List.singleton
-        | Ref(ClassField(address, field)) when field = Reflection.stringFirstCharField ->
-            let address, stringArrayType = Memory.StringArrayInfo state address None
-            (Some (address, [zero], stringArrayType), cilState) |> List.singleton
-        | Ptr(HeapLocation _ as pointerBase, sightType, offset) ->
-            let cases = PtrToRefFork state pointerBase sightType offset
-            assert(List.isEmpty cases |> not)
-            let createArrayRef (address, state) =
-                let cilState = changeState cilState state
-                match address with
-                | Some(ArrayIndex(address, index, arrayType)) -> Some (address, index, arrayType), cilState
-                | _ ->
-                    let iie = createInsufficientInformation "Memmove: unknown pointer"
-                    cilState.iie <- Some iie
-                    None, cilState
-            List.map createArrayRef cases
+        let cases = Memory.TryAddressFromRefFork state ref
+        assert(List.length cases >= 1)
+        let createArrayRef (address, state) =
+            let cilState = changeState cilState state
+            match address with
+            | Some address -> Some address, cilState
+            | _ ->
+                let iie = createInsufficientInformation "Memmove: unknown pointer"
+                cilState.iie <- Some iie
+                None, cilState
+        List.map createArrayRef cases
 
-        | _ -> internalfail $"Memmove: unexpected reference {ref}"
-
-    let private Copy dstAddr dstIndex dstIndices dstArrayType srcAddr srcIndex srcIndices srcArrayType state elemCount =
+    let private Copy dstAddr dstIndex dstIndices dstArrayType srcAddr srcIndex srcIndices srcArrayType state bytesCount =
+        if Memory.IsSafeContextCopy srcArrayType dstArrayType |> not then
+            internalfail $"Buffer.Copy: unsafe memory copy is not implemented, src type {srcArrayType}, dst type {dstArrayType}"
+        let size = TypeUtils.internalSizeOf (fst3 srcArrayType)
+        let elemCount = Arithmetics.Div bytesCount (MakeNumber size)
         let dstType = Types.ArrayTypeToSymbolicType dstArrayType
         let srcType = Types.ArrayTypeToSymbolicType srcArrayType
         let dstHeapRef = HeapRef dstAddr dstType
@@ -67,46 +45,81 @@ module internal Buffer =
             | None -> srcLinearIndex
         Memory.CopyArray state srcHeapRef srcLinearIndex srcType dstHeapRef dstLinearIndex dstType elemCount
 
-    let CommonMemmove (cilState : cilState) dst dstIndex src srcIndex elemCount =
+    let CommonMemmove (cilState : cilState) dst dstIndex src srcIndex bytesCount =
         let state = cilState.state
-        let elemCount = Types.Cast elemCount typeof<int>
+        let bytesCount = Types.Cast bytesCount typeof<int>
         let checkDst (info, cilState) =
             match info with
-            | Some(dstAddr, dstIndices, dstArrayType) ->
+            | Some (dstAddress : address) ->
                 let checkSrc (info, cilState) =
                     match info with
-                    | Some(srcAddr, srcIndices, srcArrayType) ->
-                        Copy dstAddr dstIndex dstIndices dstArrayType srcAddr srcIndex srcIndices srcArrayType state elemCount
-                        cilState
+                    | Some (srcAddress : address) ->
+                        let dstType = lazy dstAddress.TypeOfLocation
+                        let srcType = lazy srcAddress.TypeOfLocation
+                        let dstSize = lazy(TypeUtils.internalSizeOf dstType.Value)
+                        let srcSize = lazy(TypeUtils.internalSizeOf srcType.Value)
+                        let allSafe() =
+                            let isSafe =
+                                dstType.Value = srcType.Value
+                                || TypeUtils.canCastImplicitly srcType.Value dstType.Value
+                                && dstSize.Value = srcSize.Value
+                            isSafe && MakeNumber srcSize.Value = bytesCount
+                        let dstSafe = lazy(MakeNumber dstSize.Value = bytesCount)
+                        let srcSafe = lazy(MakeNumber srcSize.Value = bytesCount)
+                        match dstAddress, srcAddress with
+                        | _ when allSafe() ->
+                            let value = read cilState (Ref srcAddress)
+                            let cilStates = write cilState (Ref dstAddress) value
+                            assert(List.length cilStates = 1)
+                            List.head cilStates
+                        | _ when dstSafe.Value ->
+                            let ptr = Types.Cast (Ref srcAddress) (dstType.Value.MakePointerType())
+                            let value = read cilState ptr
+                            let cilStates = write cilState (Ref dstAddress) value
+                            assert(List.length cilStates = 1)
+                            List.head cilStates
+                        | _ when srcSafe.Value ->
+                            let value = read cilState (Ref srcAddress)
+                            let ptr = Types.Cast (Ref dstAddress) (srcType.Value.MakePointerType())
+                            let cilStates = write cilState ptr value
+                            assert(List.length cilStates = 1)
+                            List.head cilStates
+                        | ArrayIndex(dstAddress, dstIndices, dstArrayType), ArrayIndex(srcAddress, srcIndices, srcArrayType) ->
+                            Copy dstAddress dstIndex dstIndices dstArrayType srcAddress srcIndex srcIndices srcArrayType state bytesCount
+                            cilState
+                        // TODO: implement unsafe copy
+                        | _ -> internalfail $"CommonMemmove unexpected addresses {srcAddress}, {dstAddress}"
                     | None -> cilState
-                getArrayInfo cilState src |> List.map checkSrc
+                getAddress cilState src |> List.map checkSrc
             | None -> cilState |> List.singleton
-        getArrayInfo cilState dst |> List.collect checkDst
+        getAddress cilState dst |> List.collect checkDst
 
-    let Memmove (cilState : cilState) dst src elemCount =
-        CommonMemmove cilState dst None src None elemCount
+    let Memmove (cilState : cilState) dst src bytesCount =
+        CommonMemmove cilState dst None src None bytesCount
 
     let GenericMemmove (_ : IInterpreter) (cilState : cilState) (args : term list) =
         assert(List.length args = 4)
-        let dst, src, elemCount = args[1], args[2], args[3]
-        Memmove cilState dst src elemCount
+        let elemType, dst, src, elemCount = args[0], args[1], args[2], args[3]
+        let elemSize = Helpers.unwrapType elemType |> TypeUtils.internalSizeOf
+        let bytesCount = Arithmetics.Mul elemCount (MakeNumber elemSize)
+        Memmove cilState dst src bytesCount
 
     let ByteMemmove (_ : IInterpreter) (cilState : cilState) (args : term list) =
         assert(List.length args = 3)
-        let dst, src, elemCount = args[0], args[1], args[2]
-        Memmove cilState dst src elemCount
+        let dst, src, bytesCount = args[0], args[1], args[2]
+        Memmove cilState dst src bytesCount
 
     let MemoryCopy (i : IInterpreter) (cilState : cilState) (args : term list) =
         assert(List.length args = 4)
-        let dst, src, dstSize, count = args[0], args[1], args[2], args[3]
+        let dst, src, dstBytesCount, bytesCount = args[0], args[1], args[2], args[3]
         let memMove cilState k =
-            Memmove cilState dst src count |> k
+            Memmove cilState dst src bytesCount |> k
         let checkDst cilState k =
             i.NpeOrInvoke cilState dst memMove k
         let checkSrc cilState k =
             i.NpeOrInvoke cilState src checkDst k
         StatedConditionalExecutionCIL cilState
-            (fun state k -> k (Arithmetics.LessOrEqual count dstSize, state))
+            (fun state k -> k (Arithmetics.LessOrEqual bytesCount dstBytesCount, state))
             checkSrc
             (i.Raise i.ArgumentOutOfRangeException)
             id

VSharp.InternalCalls/Environment.fs

@@ -1,13 +1,14 @@
 namespace VSharp.System
 
 open global.System
+open VSharp
 open VSharp.Core
 
 // ------------------------------- mscorlib.System.Environment -------------------------------
 
-module Environment =
+module internal Environment =
 
-    let internal GetResourceFromDefault (state : state) (_ : term list) =
+    let GetResourceFromDefault (state : state) (_ : term list) =
         Memory.AllocateString "Getting resource strings currently not supported!" state
 
     let GetCurrentManagedThreadId  (_ : state) (_ : term list) =
@@ -16,14 +17,29 @@ module Environment =
     let GetManagedThreadId  (_ : state) (_ : term list) =
         MakeNumber 0
 
-    let internal WriteLine (_ : state) (args : term list) =
+    let WriteLine (_ : state) (args : term list) =
         assert(List.length args = 1)
         Nop()
 
-    let internal get_IsOutputRedirected (_ : state) (args : term list) =
+    let get_IsOutputRedirected (_ : state) (args : term list) =
         assert(List.length args = 0)
         MakeBool false
 
-    let internal consoleClear (_ : state) (args : term list) =
+    let consoleClear (_ : state) (args : term list) =
         assert(List.length args = 0)
         Nop()
+
+    let CreateDirectory (state : state) (args : term list) =
+        assert(List.length args = 1)
+        let name = args[0]
+        let t = typeof<System.IO.DirectoryInfo>
+        let dir = Memory.AllocateDefaultClass state t
+        let fields = Reflection.fieldsOf false t
+        let nameField = fields |> Array.find (fun (f, _) -> f.name = "_name") |> fst
+        let states = Memory.WriteClassField state dir nameField name
+        assert(List.length states = 1)
+        dir
+
+    let FileExists (_ : state) (args : term list) =
+        assert(List.length args = 1)
+        False()

VSharp.InternalCalls/Environment.fsi

@@ -18,10 +18,17 @@ module internal Environment =
     val GetManagedThreadId : state -> term list -> term
 
     [<Implements("System.Void System.Console.WriteLine(System.String)")>]
+    [<Implements("System.Void System.Console.WriteLine(System.Object)")>]
     val WriteLine : state -> term list -> term
 
     [<Implements("System.Boolean System.Console.get_IsOutputRedirected()")>]
     val get_IsOutputRedirected : state -> term list -> term
 
     [<Implements("System.Void System.Console.Clear()")>]
     val consoleClear : state -> term list -> term
+
+    [<Implements("System.IO.DirectoryInfo System.IO.Directory.CreateDirectory(System.String)")>]
+    val CreateDirectory : state -> term list -> term
+
+    [<Implements("System.Boolean System.IO.File.Exists(System.String)")>]
+    val FileExists : state -> term list -> term

VSharp.InternalCalls/Globalization.fs

@@ -26,3 +26,7 @@ module internal Globalization =
     let get_Invariant (_ : state) (args : term list) : term =
         assert(List.length args = 0)
         True()
+
+    let get_Name (state : state) (args : term list) : term =
+        assert(List.length args = 1)
+        Memory.AllocateString "Culture" state

VSharp.InternalCalls/Globalization.fsi

@@ -6,14 +6,17 @@ open VSharp.Core
 
 module internal Globalization =
 
-    [<Implements("System.Globalization.CultureInfo System.Globalization.CultureInfo.get_CurrentCulture()")>]
+    // [<Implements("System.Globalization.CultureInfo System.Globalization.CultureInfo.get_CurrentCulture()")>]
     val get_CurrentCulture : state -> term list -> term
 
-    [<Implements("System.Globalization.CultureInfo System.Globalization.CultureInfo.get_InvariantCulture()")>]
+    // [<Implements("System.Globalization.CultureInfo System.Globalization.CultureInfo.get_InvariantCulture()")>]
     val get_InvariantCulture : state -> term list -> term
 
     [<Implements("System.Globalization.CompareInfo System.Globalization.CultureInfo.get_CompareInfo(this)")>]
     val get_CompareInfo : state -> term list -> term
 
-    [<Implements("System.Boolean System.Globalization.GlobalizationMode.get_Invariant()")>]
+    // [<Implements("System.Boolean System.Globalization.GlobalizationMode.get_Invariant()")>]
     val get_Invariant : state -> term list -> term
+
+    [<Implements("System.String System.Globalization.CultureInfo.get_Name(this)")>]
+    val get_Name : state -> term list -> term