Merge pull request #295 from oveeernight/splitting

Splitting

Author: MchKosticyn

VSharp.InternalCalls/ByReference.fs

@@ -18,11 +18,12 @@ module ByReference =
         assert(isValueField field)
         Memory.ReferenceField state this field
 
-    let internal ctor (state : state) (args : term list) : (term * state) list =
+    let internal ctor (state : state) (args : term list) : term =
         assert(List.length args = 3)
         let this, ref = List.item 0 args, List.item 2 args
         let fieldRef = referenceValueField state this
-        Memory.Write state fieldRef ref |> List.map (withFst (Nop()))
+        Memory.Write state fieldRef ref
+        Nop()
 
     let internal getValue (state : state) (args : term list) : term =
         assert(List.length args = 2)

VSharp.InternalCalls/ByReference.fsi

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

VSharp.InternalCalls/Enum.fs

@@ -68,12 +68,14 @@ module internal Enum =
                 valuesList.Add(TypeUtils.convert v typeof<UInt64> :?> UInt64)
             let values = Memory.ObjectToTerm state (valuesList.ToArray()) typeof<UInt64[]>
             let valuesCase state k =
-                Memory.Write state valuesPtr values |> k
+                 Memory.Write state valuesPtr values
+                 List.singleton state |> k
             let namesAndValuesCase state k =
                 let names = Memory.ObjectToTerm state names typeof<string[]>
                 let namesPtr = Memory.ReadField state namesRef refField
-                let states = Memory.Write state valuesPtr values
-                List.collect (fun state -> Memory.Write state namesPtr names) states |> k
+                Memory.Write state valuesPtr values
+                Memory.Write state namesPtr names
+                List.singleton state |> k
             let needNames = (Types.Cast getNamesFlag typeof<int>) === (MakeNumber 1)
             StatedConditionalExecutionAppend state
                 (fun state k -> k (needNames, state))

VSharp.InternalCalls/Environment.fs

@@ -36,8 +36,7 @@ module internal Environment =
         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)
+        Memory.WriteClassField state dir nameField name
         dir
 
     let FileExists (_ : state) (args : term list) =

VSharp.InternalCalls/IntPtr.fs

@@ -8,21 +8,23 @@ open VSharp.Core
 
 module IntPtr =
 
-    let private intPtrCtor (state : state) this term : (term * state) list =
+    let private intPtrCtor (state : state) this term : term =
         let ptr = MakeIntPtr term
-        Memory.Write state this ptr |> List.map (withFst (Nop()))
+        Memory.Write state this ptr
+        Nop()
+        
 
-    let internal intPtrCtorFromInt (state : state) (args : term list) : (term * state) list =
+    let internal intPtrCtorFromInt (state : state) (args : term list) : term =
         assert(List.length args = 2)
         let this, intTerm = List.item 0 args, List.item 1 args
         intPtrCtor state this intTerm
 
-    let internal intPtrCtorFromPtr (state : state) (args : term list) : (term * state) list =
+    let internal intPtrCtorFromPtr (state : state) (args : term list) : term =
         assert(List.length args = 2)
         let this, ptrTerm = List.item 0 args, List.item 1 args
         intPtrCtor state this ptrTerm
 
-    let internal intPtrCtorFromLong (state : state) (args : term list) : (term * state) list =
+    let internal intPtrCtorFromLong (state : state) (args : term list) : term =
         assert(List.length args = 2)
         let this, intTerm = List.item 0 args, List.item 1 args
         intPtrCtor state this intTerm
@@ -37,21 +39,22 @@ module IntPtr =
 
 module UIntPtr =
 
-    let private uintPtrCtor (state : state) this term : (term * state) list =
+    let private uintPtrCtor (state : state) this term : term =
         let ptr = MakeUIntPtr term
-        Memory.Write state this ptr |> List.map (withFst (Nop()))
+        Memory.Write state this ptr
+        Nop()
 
-    let internal uintPtrCtorFromUInt (state : state) (args : term list) : (term * state) list =
+    let internal uintPtrCtorFromUInt (state : state) (args : term list) : term =
         assert(List.length args = 2)
         let this, intTerm = List.item 0 args, List.item 1 args
         uintPtrCtor state this intTerm
 
-    let internal uintPtrCtorFromPtr (state : state) (args : term list) : (term * state) list =
+    let internal uintPtrCtorFromPtr (state : state) (args : term list) : term =
         assert(List.length args = 2)
         let this, ptrTerm = List.item 0 args, List.item 1 args
         uintPtrCtor state this ptrTerm
 
-    let internal uintPtrCtorFromULong (state : state) (args : term list) : (term * state) list =
+    let internal uintPtrCtorFromULong (state : state) (args : term list) : term =
         assert(List.length args = 2)
         let this, intTerm = List.item 0 args, List.item 1 args
         uintPtrCtor state this intTerm

VSharp.InternalCalls/IntPtr.fsi

@@ -7,27 +7,27 @@ open VSharp.Core
 module internal IntPtr =
 
     [<Implements("System.Void System.IntPtr..ctor(this, System.Int32)")>]
-    val intPtrCtorFromInt : state -> term list -> (term * state) list
+    val intPtrCtorFromInt : state -> term list -> term
 
     [<Implements("System.Void System.IntPtr..ctor(this, System.Void*)")>]
-    val intPtrCtorFromPtr : state -> term list -> (term * state) list
+    val intPtrCtorFromPtr : state -> term list -> term
 
     [<Implements("System.Void System.IntPtr..ctor(this, System.Int64)")>]
-    val intPtrCtorFromLong : state -> term list -> (term * state) list
+    val intPtrCtorFromLong : state -> term list -> term
 
     [<Implements("System.Void* System.IntPtr.ToPointer(this)")>]
     val intPtrToPointer : state -> term list -> term
 
 module internal UIntPtr =
 
     [<Implements("System.Void System.UIntPtr..ctor(this, System.UInt32)")>]
-    val uintPtrCtorFromUInt : state -> term list -> (term * state) list
+    val uintPtrCtorFromUInt : state -> term list -> term
 
     [<Implements("System.Void System.UIntPtr..ctor(this, System.Void*)")>]
-    val uintPtrCtorFromPtr : state -> term list -> (term * state) list
+    val uintPtrCtorFromPtr : state -> term list -> term
 
     [<Implements("System.Void System.UIntPtr..ctor(this, System.UInt64)")>]
-    val uintPtrCtorFromULong : state -> term list -> (term * state) list
+    val uintPtrCtorFromULong : state -> term list -> term
 
     [<Implements("System.Void* System.UIntPtr.ToPointer(this)")>]
     val uintPtrToPointer : state -> term list -> term

VSharp.InternalCalls/String.fs

@@ -162,8 +162,7 @@ module internal String =
             let char = Memory.ReadStringChar cilState.state this index
             cilState.Push char
             List.singleton cilState |> k
-        let arrayLength = Add length (MakeNumber 1)
-        interpreter.AccessArray getChar cilState arrayLength index id
+        interpreter.AccessArray getChar cilState length index id
 
     let AllCharsInUInt32AreAscii (_ : state) (_ : term list) =
         // TODO: try to not internal call it

VSharp.SILI.Core/API.fs

@@ -80,7 +80,7 @@ module API =
         let Ref address = Ref address
         let Ptr baseAddress typ offset = Ptr baseAddress typ offset
         let HeapRef address baseType = HeapRef address baseType
-        let Union gvs = Union gvs
+        let Ite iteType = Ite iteType
 
         let True() = True()
         let False() = False()
@@ -426,9 +426,9 @@ module API =
                         let index = indices[0]
                         t, mul index (TypeUtils.internalSizeOf t |> makeNumber)
                 Ptr baseAddress sightType (add offset indexOffset)
-            | Union gvs ->
+            | Ite iteType ->
                 let referenceArrayIndex term = ReferenceArrayIndex state term indices valueType
-                Merging.guardedMap referenceArrayIndex gvs
+                Merging.guardedMap referenceArrayIndex iteType
             | _ -> internalfail $"Referencing array index: expected reference, but got {arrayRef}"
 
         let ReferenceField state reference fieldId =
@@ -468,11 +468,6 @@ module API =
         let TryAddressFromRefFork state ref =
             CommonTryAddressFromRef state ref true
 
-        let private transformBoxedRef ref =
-            match ref.term with
-            | HeapRef _ -> HeapReferenceToBoxReference ref
-            | _ -> ref
-
         let ExtractAddress ref = extractAddress ref
         let ExtractPointerOffset ptr = extractPointerOffset ptr
 
@@ -485,16 +480,17 @@ module API =
         let ReadThis state method = state.memory.ReadStackLocation (ThisKey method)
         let ReadArgument state parameterInfo = state.memory.ReadStackLocation (ParameterKey parameterInfo)
 
-        let CommonReadField reporter state term field =
-            let doRead target =
-                match target.term with
-                | HeapRef _
-                | Ptr _
-                | Ref _ -> ReferenceField state target field |> state.memory.Read reporter
-                | Struct _ -> state.memory.ReadStruct reporter target field
-                | Combined _ -> state.memory.ReadFieldUnsafe reporter target field
-                | _ -> internalfail $"Reading field of {term}"
-            Merging.guardedApply doRead term
+        let rec CommonReadField reporter state term field =
+            match term.term with
+            | HeapRef _
+            | Ptr _
+            | Ref _ -> ReferenceField state term field |> state.memory.Read reporter
+            | Struct _ -> state.memory.ReadStruct reporter term field
+            | Combined _ -> state.memory.ReadFieldUnsafe reporter term field
+            | Ite iteType ->
+                iteType.filter (fun v -> True() <> IsBadRef v)
+                |> Merging.guardedMap (fun t -> CommonReadField reporter state t field)
+            | _ -> internalfail $"Reading field of {term}"
 
         let ReadField state term field =
             CommonReadField emptyReporter state term field
@@ -522,9 +518,9 @@ module API =
             | HeapRef(addr, typ) when state.memory.MostConcreteTypeOfHeapRef addr typ = typeof<string> ->
                 let addr, arrayType = state.memory.StringArrayInfo addr None
                 state.memory.ReadArrayIndex addr [index] arrayType
-            | Union gvs ->
+            | Ite iteType ->
                 let readStringChar term = ReadStringChar state term index
-                Merging.guardedMap readStringChar gvs
+                Merging.guardedMap readStringChar iteType
             | _ -> internalfail $"Reading string char: expected reference, but got {reference}"
         let ReadStaticField state typ field = state.memory.ReadStaticField typ field
         let ReadDelegate state reference = state.memory.ReadDelegate reference
@@ -538,16 +534,11 @@ module API =
 
         let WriteStackLocation state location value = state.memory.WriteStackLocation location value
 
-        let Write state reference value =
-            let write state reference =
-                state.memory.Write emptyReporter (transformBoxedRef reference) value
-            Branching.guardedStatedMap write state reference
+        let Write state reference value = state.memory.Write emptyReporter reference value
 
         let WriteUnsafe (reporter : IErrorReporter) state reference value =
-            let write state reference =
-                reporter.ConfigureState state
-                state.memory.Write reporter reference value
-            Branching.guardedStatedMap write state reference
+            reporter.ConfigureState state
+            state.memory.Write reporter reference value
 
         let WriteStructField structure field value = writeStruct structure field value
 
@@ -556,13 +547,17 @@ module API =
             writeStruct structure field value
 
         let WriteClassFieldUnsafe (reporter : IErrorReporter) state reference field value =
-            let write state reference =
-                reporter.ConfigureState state
-                match reference.term with
-                | HeapRef(addr, _) -> state.memory.WriteClassField addr field value
+            let extractAddress ref =
+                match ref.term with
+                | HeapRef(addr, _) -> addr
                 | _ -> internalfail $"Writing field of class: expected reference, but got {reference}"
-                state
-            Branching.guardedStatedMap write state reference
+            reporter.ConfigureState state
+            match reference.term with
+            | Ite iteType ->
+                let filtered = iteType.filter (fun r -> Pointers.isBadRef r |> isTrue |> not)
+                filtered.ToDisjunctiveGvs()
+                |> List.iter (fun (g, r) -> state.memory.GuardedWriteClassField (Some g) (extractAddress r) field value)
+            | _ -> state.memory.WriteClassField (extractAddress reference) field value
 
         let WriteClassField state reference field value =
             WriteClassFieldUnsafe emptyReporter state reference field value
@@ -766,26 +761,26 @@ module API =
         let rec ArrayRank state arrayRef =
             match arrayRef.term with
             | HeapRef(addr, typ) -> state.memory.MostConcreteTypeOfHeapRef addr typ |> TypeUtils.rankOf |> makeNumber
-            | Union gvs -> Merging.guardedMap (ArrayRank state) gvs
+            | Ite iteType -> Merging.guardedMap (ArrayRank state) iteType
             | _ -> internalfail $"Getting rank of array: expected ref, but got {arrayRef}"
 
         let rec ArrayLengthByDimension state arrayRef index =
             match arrayRef.term with
             | HeapRef(addr, typ) ->
                 let memory = state.memory
                 memory.MostConcreteTypeOfHeapRef addr typ |> symbolicTypeToArrayType |> memory.ReadLength addr index
-            | Union gvs ->
+            | Ite iteType ->
                 let arrayLengthByDimension term = ArrayLengthByDimension state term index
-                Merging.guardedMap arrayLengthByDimension gvs
+                Merging.guardedMap arrayLengthByDimension iteType
             | _ -> internalfail $"reading array length: expected heap reference, but got {arrayRef}"
         let rec ArrayLowerBoundByDimension state arrayRef index =
             match arrayRef.term with
             | HeapRef(addr, typ) ->
                 let memory = state.memory
                 memory.MostConcreteTypeOfHeapRef addr typ |> symbolicTypeToArrayType |> memory.ReadLowerBound addr index
-            | Union gvs ->
+            | Ite iteType ->
                 let arrayLowerBoundByDimension term = ArrayLowerBoundByDimension state term index
-                Merging.guardedMap arrayLowerBoundByDimension gvs
+                Merging.guardedMap arrayLowerBoundByDimension iteType
             | _ -> internalfail $"reading array lower bound: expected heap reference, but got {arrayRef}"
 
         let rec CountOfArrayElements state arrayRef =
@@ -795,7 +790,7 @@ module API =
                 let arrayType = memory.MostConcreteTypeOfHeapRef address typ |> symbolicTypeToArrayType
                 let lens = List.init arrayType.dimension (fun dim -> memory.ReadLength address (makeNumber dim) arrayType)
                 List.fold mul (makeNumber 1) lens
-            | Union gvs -> Merging.guardedMap (CountOfArrayElements state) gvs
+            | Ite iteType -> Merging.guardedMap (CountOfArrayElements state) iteType
             | _ -> internalfail $"counting array elements: expected heap reference, but got {arrayRef}"
 
         let StringLength state strRef = state.memory.LengthOfString strRef

VSharp.SILI.Core/API.fsi

@@ -51,8 +51,7 @@ module API =
         val Ref : address -> term
         val Ptr : pointerBase -> Type -> term -> term
         val HeapRef : heapAddress -> Type -> term
-        val Union : (term * term) list -> term
-
+        val Ite : iteType -> term
         val True : unit -> term
         val False : unit -> term
         val NullRef : Type -> term
@@ -295,14 +294,14 @@ module API =
 
         val InitializeArray : state -> term -> term -> unit
 
-        val Write : state -> term -> term -> state list
-        val WriteUnsafe : IErrorReporter -> state -> term -> term -> state list
+        val Write : state -> term -> term -> unit
+        val WriteUnsafe : IErrorReporter -> state -> term -> term -> unit
         val WriteStackLocation : state -> stackKey -> term -> unit
         val WriteStructField : term -> fieldId -> term -> term
         val WriteStructFieldUnsafe : IErrorReporter -> state -> term -> fieldId -> term -> term
-        val WriteClassFieldUnsafe : IErrorReporter -> state -> term -> fieldId -> term -> state list
-        val WriteClassField : state -> term -> fieldId -> term -> state list
-        val WriteArrayIndexUnsafe : IErrorReporter -> state -> term -> term list -> term -> Type option -> state list
+        val WriteClassFieldUnsafe : IErrorReporter -> state -> term -> fieldId -> term -> unit
+        val WriteClassField : state -> term -> fieldId -> term -> unit
+        val WriteArrayIndexUnsafe : IErrorReporter -> state -> term -> term list -> term -> Type option -> unit
         val WriteStaticField : state -> Type -> fieldId -> term -> unit
 
         val DefaultOf : Type -> term