[style] 'cilState.Write' returns 'Unit'

VSharp.InternalCalls/Buffer.fs

@@ -53,7 +53,7 @@ module internal Buffer =
             let checkDst (info, cilState : cilState) =
                 match info with
                 | Some (dstAddress : address) ->
-                    let checkSrc (info, cilState : cilState) =
+                    let checkSrc info (cilState : cilState) =
                         match info with
                         | Some (srcAddress : address) ->
                             let dstType = lazy dstAddress.TypeOfLocation
@@ -71,28 +71,26 @@ module internal Buffer =
                             match dstAddress, srcAddress with
                             | _ when allSafe() ->
                                 let value = cilState.Read (Ref srcAddress)
-                                let cilStates = cilState.Write (Ref dstAddress) value
-                                assert(List.length cilStates = 1)
-                                List.head cilStates
+                                cilState.Write (Ref dstAddress) value
                             | _ when dstSafe.Value ->
                                 let ptr = Types.Cast (Ref srcAddress) (dstType.Value.MakePointerType())
                                 let value = cilState.Read ptr
-                                let cilStates = cilState.Write (Ref dstAddress) value
-                                assert(List.length cilStates = 1)
-                                List.head cilStates
+                                cilState.Write (Ref dstAddress) value
                             | _ when srcSafe.Value ->
                                 let value = cilState.Read (Ref srcAddress)
                                 let ptr = Types.Cast (Ref dstAddress) (srcType.Value.MakePointerType())
-                                let cilStates = cilState.Write ptr value
-                                assert(List.length cilStates = 1)
-                                List.head cilStates
+                                cilState.Write ptr value
                             | 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
-                    getAddress cilState src |> List.map checkSrc
+                        | None -> ()
+                    let addressesWithStates = getAddress cilState src
+                    let mutable resultCilStates = List.empty
+                    for address, cilState in addressesWithStates do
+                        checkSrc address cilState
+                        resultCilStates <- cilState :: resultCilStates
+                    resultCilStates
                 | None -> cilState |> List.singleton
             getAddress cilState dst |> List.collect checkDst
 

VSharp.InternalCalls/Interlocked.fs

@@ -1,7 +1,7 @@
 namespace VSharp.System
 
 open global.System
-open VSharp
+
 open VSharp.Core
 open VSharp.Interpreter.IL
 open VSharp.Interpreter.IL.CilState
@@ -11,10 +11,9 @@ module internal Interlocked =
     let exchange (interpreter : IInterpreter) (cilState : cilState) location value =
         let exchange (cilState : cilState) k =
             let currentValue = cilState.Read location
-            let cilStates = cilState.Write location value
-            for cilState in cilStates do
-                cilState.Push currentValue
-            k cilStates
+            cilState.Write location value
+            cilState.Push currentValue
+            List.singleton cilState |> k
         interpreter.NpeOrInvoke cilState location exchange id
 
     let commonCompareExchange (interpreter : IInterpreter) (cilState : cilState) location value compared =
@@ -23,7 +22,7 @@ module internal Interlocked =
             let cilStates =
                 cilState.StatedConditionalExecutionCIL
                     (fun cilState k -> k (currentValue === compared, cilState))
-                    (fun cilState k -> k (cilState.Write location value))
+                    (fun cilState k -> k (cilState.Write location value; List.singleton cilState))
                     (fun cilState k -> k (List.singleton cilState))
                     id
             for cilState in cilStates do

VSharp.InternalCalls/Object.fs

@@ -41,12 +41,8 @@ module internal Object =
                 else t
             let newObject = Memory.AllocateDefaultClass state t
             let fields = Reflection.fieldsOf false t
-            let copyField cilStates (field, _) =
-                let copyForState (cilState : cilState) =
-                    let v = cilState.ReadField object field
-                    cilState.WriteClassField newObject field v
-                List.collect copyForState cilStates
-            let cilStates = Array.fold copyField (List.singleton cilState) fields
-            for cilState in cilStates do
-                cilState.Push newObject
-            cilStates
+            for field, _ in fields do
+                let v = cilState.ReadField object field
+                cilState.WriteClassField newObject field v
+            cilState.Push newObject
+            List.singleton cilState

VSharp.InternalCalls/Span.fs

@@ -137,6 +137,7 @@ module internal ReadOnlySpan =
         let span = cilState.Read this
         let initializedSpan = InitSpanStruct cilState span refToFirst length
         cilState.Write this initializedSpan
+        List.singleton cilState
 
     let CtorFromPtr (i : IInterpreter) (cilState : cilState) (args : term list) : cilState list =
         assert(List.length args = 4)
@@ -237,8 +238,7 @@ module internal ReadOnlySpan =
             let arrayRef = Memory.AllocateConcreteObject state rawData arrayType
             let refToFirstElement = Memory.ReferenceArrayIndex state arrayRef [MakeNumber 0] None
             let count = MakeNumber rawData.Length
-            let cilStates = cilState.Write countRef count
-            assert(List.length cilStates = 1 && cilStates[0] = cilState)
+            cilState.Write countRef count
             cilState.Push refToFirstElement
             List.singleton cilState
         | _ -> internalfail $"GetSpanDataFrom: unexpected field handle {fieldHandleTerm} or type handle {typeHandleTerm}"

VSharp.InternalCalls/String.fs

@@ -47,19 +47,18 @@ module internal String =
             (length >>= zero)
             &&& (startIndex >>= zero)
         let copy (cilState : cilState) k =
-            let cilStates = cilState.WriteClassField this Reflection.stringLengthField length
+            cilState.WriteClassField this Reflection.stringLengthField length
             let bytesCount = Mul length (MakeNumber sizeof<char>)
-            let memMove cilState =
-                Buffer.CommonMemmove cilState this None ptr (Some startIndex) bytesCount
-            List.collect memMove cilStates |> k
+            Buffer.CommonMemmove cilState this None ptr (Some startIndex) bytesCount |> k
         let checkPtr (cilState : cilState) k =
             cilState.StatedConditionalExecutionCIL
                 (fun state k -> k (!!(IsBadRef ptr), state))
                 copy
                 (i.Raise i.ArgumentOutOfRangeException)
                 k
         let emptyStringCase (cilState : cilState) k =
-            cilState.WriteClassField this Reflection.stringLengthField zero |> k
+            cilState.WriteClassField this Reflection.stringLengthField zero
+            List.singleton cilState |> k
         let checkLength (cilState : cilState) k =
             cilState.StatedConditionalExecutionCIL
                 (fun state k -> k (length === zero, state))

VSharp.InternalCalls/Thread.fs

@@ -33,7 +33,8 @@ module Thread =
         assert(List.length args = 2)
         let obj, resultRef = args[0], args[1]
         let success (cilState : cilState) k =
-            cilState.Write resultRef (True()) |> k
+            cilState.Write resultRef (True())
+            List.singleton cilState |> k
         cilState.BranchOnNullCIL obj
             (interpreter.Raise interpreter.ArgumentNullException)
             success

VSharp.InternalCalls/Unsafe.fs

@@ -92,14 +92,16 @@ module internal Unsafe =
         let typ = Helpers.unwrapType typ
         let castedPtr = Types.Cast ref (typ.MakePointerType())
         let writeByPtr (cilState : cilState) k =
-            cilState.Write castedPtr value |> k
+            cilState.Write castedPtr value
+            List.singleton cilState |> k
         i.NpeOrInvoke cilState castedPtr writeByPtr id
 
     let WriteUnaligned (i : IInterpreter) (cilState : cilState) (args : term list) =
         assert(List.length args = 2)
         let ref, value = args[0], args[1]
         let writeByPtr (cilState : cilState) k =
-            cilState.Write ref value |> k
+            cilState.Write ref value
+            List.singleton cilState |> k
         i.NpeOrInvoke cilState ref writeByPtr id
 
     let SizeOf (_ : state) (args : term list) : term =

VSharp.InternalCalls/Volatile.fs

@@ -21,3 +21,4 @@ module Volatile =
         assert(List.length args = 3)
         let ref, value = args[1], args[2]
         cilState.Write ref value
+        List.singleton cilState

VSharp.SILI/CILState.fs

@@ -444,18 +444,15 @@ module CilState =
 
         member x.Write ref value =
             Memory.WriteUnsafe x.ErrorReporter.Value x.state ref value
-            List.singleton x
 
         member x.WriteClassField ref field value =
             Memory.WriteClassFieldUnsafe x.ErrorReporter.Value x.state ref field value
-            List.singleton x
 
         member x.WriteStructField term field value =
             Memory.WriteStructFieldUnsafe x.ErrorReporter.Value x.state term field value
 
         member x.WriteIndex term index value valueType =
             Memory.WriteArrayIndexUnsafe x.ErrorReporter.Value x.state term index value valueType
-            List.singleton x
 
         // -------------------------- Branching --------------------------
 

VSharp.SILI/Interpreter.fs

@@ -1309,7 +1309,8 @@ type ILInterpreter() as this =
         let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Stobj.Size)
         let store (cilState : cilState) k =
             let value = Types.Cast value typ
-            cilState.Write ref value |> k
+            cilState.Write ref value
+            List.singleton cilState |> k
         x.NpeOrInvokeStatementCIL cilState ref store id
 
     member x.LdFldWithFieldInfo (fieldInfo : FieldInfo) addressNeeded (cilState : cilState) =
@@ -1342,7 +1343,8 @@ type ILInterpreter() as this =
             let reference =
                 if TypeUtils.isPointer fieldInfo.DeclaringType then targetRef
                 else Reflection.wrapField fieldInfo |> Memory.ReferenceField cilState.state targetRef
-            cilState.Write reference value |> k
+            cilState.Write reference value
+            List.singleton cilState |> k
         x.NpeOrInvokeStatementCIL cilState targetRef storeWhenTargetIsNotNull id
 
     member private x.LdElemCommon (typ : Type option) (cilState : cilState) arrayRef indices =
@@ -1395,7 +1397,8 @@ type ILInterpreter() as this =
         let checkedStElem (cilState : cilState) (k : cilState list -> 'a) =
             let typeOfValue = TypeOf value
             let uncheckedStElem (cilState : cilState) (k : cilState list -> 'a) =
-                cilState.WriteIndex arrayRef indices value typ |> k
+                cilState.WriteIndex arrayRef indices value typ
+                List.singleton cilState |> k
             let checkTypeMismatch (cilState : cilState) (k : cilState list -> 'a) =
                 let condition =
                     if Types.IsValueType typeOfValue then True()
@@ -1467,7 +1470,8 @@ type ILInterpreter() as this =
         let value, address = cilState.Pop2()
         let store (cilState : cilState) k =
             let value = valueCast value
-            cilState.Write address value |> k
+            cilState.Write address value
+            List.singleton cilState |> k
         x.NpeOrInvokeStatementCIL cilState address store id
 
     member x.BoxNullable (t : Type) (v : term) (cilState : cilState) : cilState list =
@@ -2165,12 +2169,12 @@ type ILInterpreter() as this =
             | OpCodeValues.Xor -> (fun _ _ -> bitwiseOrBoolOperation OperationType.BitwiseXor OperationType.LogicalXor) |> fallThrough m offset cilState
             | OpCodeValues.Neg -> (fun _ _ -> performCILUnaryOperation OperationType.UnaryMinus) |> fallThrough m offset cilState
             | OpCodeValues.Not -> (fun _ _ -> bitwiseOrBoolNot) |> fallThrough m offset cilState
-            | OpCodeValues.Stloc -> stloc (fun ilBytes offset -> NumberCreator.extractUnsignedInt16 ilBytes (offset + Offset.from OpCodes.Stloc.Size) |> int) |> forkThrough m offset cilState
-            | OpCodeValues.Stloc_0 -> stloc (fun _ _ -> 0) |> forkThrough m offset cilState
-            | OpCodeValues.Stloc_1 -> stloc (fun _ _ -> 1) |> forkThrough m offset cilState
-            | OpCodeValues.Stloc_2 -> stloc (fun _ _ -> 2) |> forkThrough m offset cilState
-            | OpCodeValues.Stloc_3 -> stloc (fun _ _ -> 3) |> forkThrough m offset cilState
-            | OpCodeValues.Stloc_S -> stloc (fun ilBytes offset -> NumberCreator.extractUnsignedInt8 ilBytes (offset + Offset.from OpCodes.Stloc_S.Size) |> int) |> forkThrough m offset cilState
+            | OpCodeValues.Stloc -> stloc (fun ilBytes offset -> NumberCreator.extractUnsignedInt16 ilBytes (offset + Offset.from OpCodes.Stloc.Size) |> int) |> fallThrough m offset cilState
+            | OpCodeValues.Stloc_0 -> stloc (fun _ _ -> 0) |> fallThrough m offset cilState
+            | OpCodeValues.Stloc_1 -> stloc (fun _ _ -> 1) |> fallThrough m offset cilState
+            | OpCodeValues.Stloc_2 -> stloc (fun _ _ -> 2) |> fallThrough m offset cilState
+            | OpCodeValues.Stloc_3 -> stloc (fun _ _ -> 3) |> fallThrough m offset cilState
+            | OpCodeValues.Stloc_S -> stloc (fun ilBytes offset -> NumberCreator.extractUnsignedInt8 ilBytes (offset + Offset.from OpCodes.Stloc_S.Size) |> int) |> fallThrough m offset cilState
             | OpCodeValues.Starg -> starg (fun ilBytes offset -> NumberCreator.extractUnsignedInt16 ilBytes (offset + Offset.from OpCodes.Starg.Size) |> int) |> forkThrough m offset cilState
             | OpCodeValues.Starg_S -> starg (fun ilBytes offset -> NumberCreator.extractUnsignedInt8 ilBytes (offset + Offset.from OpCodes.Starg_S.Size) |> int) |> forkThrough m offset cilState
             | OpCodeValues.Ldc_I4 -> ldc (fun ilBytes offset -> NumberCreator.extractInt32 ilBytes (offset + Offset.from OpCodes.Ldc_I4.Size)) typedefof<int32> |> fallThrough m offset cilState