New string representation and string equality

VSharp.SILI.Core/API.fs

@@ -169,7 +169,7 @@ module API =
         let AllocateInHeap state term = Memory.allocateInHeap m.Value state term
         let AllocateDefaultStatic state termType qualifiedTypeName = Memory.mkDefaultStruct m.Value true termType |> Memory.allocateInStaticMemory m.Value state qualifiedTypeName
         let MakeDefaultStruct termType = Memory.mkDefaultStruct m.Value false termType
-        let AllocateString length str state = Strings.makeString length str (Memory.tick()) |> Memory.allocateInHeap m.Value state
+        let AllocateString str state = Strings.makeString m.Value (Memory.tick()) str |> Memory.allocateInHeap m.Value state
 
         let IsTypeNameInitialized qualifiedTypeName state = Memory.typeNameInitialized m.Value qualifiedTypeName state
         let Dump state = State.dumpMemory state
@@ -183,8 +183,7 @@ module API =
             let term, state = Memory.npe m.Value state
             thrower term, state
         let InvalidCastException state thrower =
-            let messageString = "Specified cast is not valid."
-            let message, state = Memory.AllocateString messageString.Length messageString state
+            let message, state = Memory.AllocateString "Specified cast is not valid." state
             let term, state = State.createInstance m.Value typeof<System.InvalidCastException> [message] state
             thrower term, state
         let TypeInitializerException qualifiedTypeName innerException state thrower =

VSharp.SILI.Core/API.fsi

@@ -145,7 +145,7 @@ module API =
         val AllocateInHeap : state -> term -> term * state
         val AllocateDefaultStatic : state -> termType -> string -> state
         val MakeDefaultStruct : termType -> term
-        val AllocateString : int -> 'a -> state -> term * state
+        val AllocateString : string -> state -> term * state
 
         val IsTypeNameInitialized : string -> state -> term
         val Dump : state -> string

VSharp.SILI.Core/Strings.fs

@@ -1,19 +1,32 @@
 namespace VSharp.Core
 
 open VSharp
+open Arrays
 open Types
 
 module internal Strings =
 
-    let makeString (length : int) str timestamp =
-        let fields : symbolicHeap =
-            Heap.ofSeq (seq [ makeStringKey "System.String.m_StringLength", { value = Concrete Metadata.empty length (Numeric typedefof<int>); created = timestamp; modified = timestamp };
-            makeStringKey "System.String.m_FirstChar", { value = Concrete Metadata.empty str String; created = timestamp; modified = timestamp }])
-        Struct Metadata.empty fields String
+    let makeString metadata time (str : string) =
+        let fields =
+            let stringTermLength = Concrete metadata str.Length lengthTermType
+            let arraySource = (str + "\000").ToCharArray()
+            let valMaker i = makeNumber arraySource.[i] metadata
+            let keyMaker i mtd = makeIntegerArray metadata (fun _ -> makeNumber i mtd) 1
+            let array = makeLinearConcreteArray metadata keyMaker valMaker (str.Length + 1) (Numeric typedefof<char>)
+            Heap.ofSeq (seq [ makeStringKey "System.String.m_StringLength", { value = stringTermLength; created = time; modified = time };
+                              makeStringKey "System.String.m_FirstChar", { value = array; created = time; modified = time } ])
+        Struct metadata fields String
 
     let simplifyEquality mtd x y =
         match x.term, y.term with
         | Concrete(x, StringType), Concrete(y, StringType) -> makeBool ((x :?> string) = (y :?> string)) mtd
+        | Struct(fieldsOfX, StringType), Struct(fieldsOfY, StringType) ->
+            let str1Len = fieldsOfX.[makeStringKey "System.String.m_StringLength"].value
+            let str2Len = fieldsOfY.[makeStringKey "System.String.m_StringLength"].value
+            let str1Arr = fieldsOfX.[makeStringKey "System.String.m_FirstChar"].value
+            let str2Arr = fieldsOfY.[makeStringKey "System.String.m_FirstChar"].value
+            simplifyEqual mtd str1Len str2Len (fun lengthEq ->
+            simplifyAnd mtd lengthEq (Arrays.equalsArrayIndices mtd str1Arr str2Arr) id)
         | _ -> __notImplemented__()
 
     let simplifyConcatenation mtd x y =

VSharp.SILI.Core/Terms.fs

@@ -109,6 +109,8 @@ type termNode =
             | Constant(name, _, _) -> name.v
             | Concrete(_, t) when Types.isFunction t -> sprintf "<Lambda Expression %O>" t
             | Concrete(_, Null) -> "null"
+            | Concrete(c, Numeric t) when t = typedefof<char> && c :?> char = '\000' -> "'\\000'"
+            | Concrete(c, Numeric t) when t = typedefof<char> -> sprintf "'%O'" c
             | Concrete(:? concreteHeapAddress as k, _) -> k |> List.map toString |> join "."
             | Concrete(value, _) -> value.ToString()
             | Expression(operation, operands, _) ->

VSharp.SILI.Core/VSharp.SILI.Core.fsproj

@@ -63,8 +63,8 @@
     <Compile Include="Merging.fs" />
     <Compile Include="Common.fs" />
     <Compile Include="Arithmetics.fs" />
-    <Compile Include="Strings.fs" />
     <Compile Include="Arrays.fs" />
+    <Compile Include="Strings.fs" />
     <Compile Include="Pointers.fs" />
     <Compile Include="Operators.fs" />
     <Compile Include="Substitution.fs" />

VSharp.SILI/Extern/System/Environment.fs

@@ -9,6 +9,5 @@ open VSharp.Core
 module Environment =
 
     let internal GetResourceFromDefault (state : state) (args : term list) =
-        let result = "Getting resource strings currently not supported!"
-        let reference, state = Memory.AllocateString result.Length result state
+        let reference, state = Memory.AllocateString "Getting resource strings currently not supported!" state
         Return reference, state

VSharp.SILI/Interpreter.fs

@@ -113,7 +113,7 @@ module internal Interpreter =
         Reset()
         let k = Enter null state k
         let stringTypeName = typeof<string>.AssemblyQualifiedName
-        let emptyString, state = Memory.AllocateString 0 String.Empty state
+        let emptyString, state = Memory.AllocateString String.Empty state
         initializeStaticMembersIfNeed null state stringTypeName (fun (result, state) ->
         let emptyFieldRef, state = Memory.ReferenceStaticField state false "System.String.Empty" Types.String stringTypeName
         Memory.Mutate state emptyFieldRef emptyString |> snd |> restoreAfter k)
@@ -818,8 +818,7 @@ module internal Interpreter =
         let obj = ast.Value.Value
         match mType with
         | Types.StringType ->
-            let stringLength = String.length (obj.ToString())
-            Memory.AllocateString stringLength obj state |> k
+            Memory.AllocateString (obj :?> string) state |> k
         | Core.Null -> k (Terms.MakeNullRef Null, state)
         | _ -> k (Concrete obj mType, state)