From cef9160ad0965c9c2015ca85bce5df90833990ab Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Mon, 27 May 2024 23:59:59 +0300 Subject: [PATCH] [style] 'cilState.Write' returns 'Unit' --- VSharp.InternalCalls/Buffer.fs | 24 +++++++++++------------- VSharp.InternalCalls/Interlocked.fs | 11 +++++------ VSharp.InternalCalls/Object.fs | 14 +++++--------- VSharp.InternalCalls/Span.fs | 4 ++-- VSharp.InternalCalls/String.fs | 9 ++++----- VSharp.InternalCalls/Thread.fs | 3 ++- VSharp.InternalCalls/Unsafe.fs | 6 ++++-- VSharp.InternalCalls/Volatile.fs | 1 + VSharp.SILI/CILState.fs | 3 --- VSharp.SILI/Interpreter.fs | 24 ++++++++++++++---------- 10 files changed, 48 insertions(+), 51 deletions(-) diff --git a/VSharp.InternalCalls/Buffer.fs b/VSharp.InternalCalls/Buffer.fs index 7a91c07d1..704666eed 100644 --- a/VSharp.InternalCalls/Buffer.fs +++ b/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 diff --git a/VSharp.InternalCalls/Interlocked.fs b/VSharp.InternalCalls/Interlocked.fs index fd76c946e..ef94766dc 100644 --- a/VSharp.InternalCalls/Interlocked.fs +++ b/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 diff --git a/VSharp.InternalCalls/Object.fs b/VSharp.InternalCalls/Object.fs index bb7de1a0b..3e4ae82f5 100644 --- a/VSharp.InternalCalls/Object.fs +++ b/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 diff --git a/VSharp.InternalCalls/Span.fs b/VSharp.InternalCalls/Span.fs index 6c4450ca6..de12e7991 100644 --- a/VSharp.InternalCalls/Span.fs +++ b/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}" diff --git a/VSharp.InternalCalls/String.fs b/VSharp.InternalCalls/String.fs index 96302afb4..6b79eeb86 100644 --- a/VSharp.InternalCalls/String.fs +++ b/VSharp.InternalCalls/String.fs @@ -47,11 +47,9 @@ 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) - 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)) @@ -59,7 +57,8 @@ module internal String = (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)) diff --git a/VSharp.InternalCalls/Thread.fs b/VSharp.InternalCalls/Thread.fs index 0b12ca87e..ef7a1f805 100644 --- a/VSharp.InternalCalls/Thread.fs +++ b/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 diff --git a/VSharp.InternalCalls/Unsafe.fs b/VSharp.InternalCalls/Unsafe.fs index ffca3f0bd..265fd97cc 100644 --- a/VSharp.InternalCalls/Unsafe.fs +++ b/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 = diff --git a/VSharp.InternalCalls/Volatile.fs b/VSharp.InternalCalls/Volatile.fs index 6b09b02de..062c41c61 100644 --- a/VSharp.InternalCalls/Volatile.fs +++ b/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 diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs index da23dec7b..d7fc576cf 100644 --- a/VSharp.SILI/CILState.fs +++ b/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 -------------------------- diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index cc781868d..32d540ce0 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/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 |> fallThrough m offset cilState