Merge pull request #315 from ch3zych3z/mem-refactor

Memory refactoring

VSharp.Explorer/Explorer.fs

@@ -55,7 +55,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
     let mutable isStopped = false
     let mutable isCoverageAchieved : unit -> bool = always false
 
-    let emptyState = Memory.EmptyState()
+    let emptyState = Memory.EmptyIsolatedState()
     let interpreter = ILInterpreter()
 
 
@@ -214,7 +214,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
                         Memory.NewStackFrame initialState None []
                         Memory.AllocateTemporaryLocalVariableOfType initialState "this" 0 declaringType |> Some
                     else
-                        let this = Memory.MakeSymbolicThis method
+                        let this = Memory.MakeSymbolicThis initialState method
                         !!(IsNullReference this) |> AddConstraint initialState
                         Some this
                 else None
@@ -508,7 +508,7 @@ type public Explorer(options : ExplorationOptions, reporter: IReporter) =
 
         try
             let trySubstituteTypeParameters method =
-                let emptyState = Memory.EmptyState()
+                let emptyState = Memory.EmptyIsolatedState()
                 (Option.defaultValue method (x.TrySubstituteTypeParameters emptyState method), emptyState)
             let isolated =
                 isolated

VSharp.Fuzzer/TestGeneration.fs

@@ -17,7 +17,7 @@ module internal TestGeneration =
 
         Logger.traceTestGeneration "Creating state"
         let m = generationData.method
-        let state = Memory.EmptyState()
+        let state = Memory.EmptyIsolatedState()
         state.model <- Memory.EmptyModel m
         state.typeStorage <- generationData.typeStorage
 
@@ -117,7 +117,7 @@ module internal TestGeneration =
             | Returned obj ->
                 Logger.traceTestGeneration "Pushing result onto evaluation stack"
                 let returnedTerm = Memory.ObjectToTerm state obj m.ReturnType
-                state.evaluationStack <- EvaluationStack.Push returnedTerm state.evaluationStack
+                state.memory.EvaluationStack <- EvaluationStack.Push returnedTerm state.memory.EvaluationStack
                 Test
 
         Logger.traceTestGeneration "State to test started"

VSharp.SILI.Core/API.fsi

@@ -255,7 +255,8 @@ module API =
         val EmptyStack : evaluationStack
 
     module public Memory =
-        val EmptyState : unit -> state
+        val EmptyIsolatedState : unit -> state
+        val EmptyCompleteState : unit -> state
         val EmptyModel : IMethod -> model
         val PopFrame : state -> unit
         val ForcePopFrames : int -> state -> unit
@@ -304,7 +305,7 @@ module API =
 
         val DefaultOf : Type -> term
 
-        val MakeSymbolicThis : IMethod -> term
+        val MakeSymbolicThis : state -> IMethod -> term
 
         val CallStackContainsFunction : state -> IMethod -> bool
         val CallStackSize : state -> int
@@ -362,7 +363,6 @@ module API =
         val StringCtorOfCharArrayAndLen : state -> term -> term -> term -> state list
 
         // TODO: get rid of all unnecessary stuff below!
-        val ComposeStates : state -> state -> state list
         val WLP : state -> pathCondition -> pathCondition
 
         val Merge2States : state -> state -> state list

VSharp.SILI.Core/ArrayInitialization.fs

@@ -54,21 +54,23 @@ module internal ArrayInitialization =
         assert (rawData.Length % size = 0)
         let dims = rankOf typeOfArray
         let arrayType = symbolicTypeToArrayType typeOfArray
-        let lbs = List.init dims (fun dim -> Memory.readLowerBound state address (makeNumber dim) arrayType |> extractIntFromTerm)
-        let lens = List.init dims (fun dim -> Memory.readLength state address (makeNumber dim) arrayType |> extractIntFromTerm)
+        let memory = state.memory
+        let lbs = List.init dims (fun dim -> memory.ReadLowerBound address (makeNumber dim) arrayType |> extractIntFromTerm)
+        let lens = List.init dims (fun dim -> memory.ReadLength address (makeNumber dim) arrayType |> extractIntFromTerm)
         let allIndices = Array.allIndicesViaLens lbs lens
         let indicesAndValues =
             Seq.mapi (fun i indices -> List.map makeNumber indices, termCreator rawData (i * size)) allIndices
-        Memory.initializeArray state address indicesAndValues arrayType
+        memory.InitializeArray address indicesAndValues arrayType
 
-    let commonInitializeArray state address typ (handle : RuntimeFieldHandle) =
-        let cm = state.concreteMemory
+    let commonInitializeArray (state : state) address typ (handle : RuntimeFieldHandle) =
+        let memory = state.memory
+        let cm = memory.ConcreteMemory
         match address.term with
         | ConcreteHeapAddress a when cm.Contains a ->
             cm.InitializeArray a handle
         | _ ->
             let fieldInfo = FieldInfo.GetFieldFromHandle handle
-            let arrayType = Memory.mostConcreteTypeOfHeapRef state address typ
+            let arrayType = memory.MostConcreteTypeOfHeapRef address typ
             let t = arrayType.GetElementType()
             assert t.IsValueType // TODO: be careful about type variables
             let rawData = Reflection.byteArrayFromField fieldInfo
@@ -88,17 +90,17 @@ module internal ArrayInitialization =
             | _ when t = typedefof<char> -> fillArray charTermCreator sizeof<char>
             | _ -> __notImplemented__()
 
-    let initializeArray state arrayRef handleTerm =
+    let initializeArray (state : state) arrayRef handleTerm =
         assert(Terms.isStruct handleTerm)
-        match arrayRef.term, Memory.tryTermToObj state handleTerm with
+        match arrayRef.term, state.memory.TryTermToObj handleTerm with
         | HeapRef(address, typ), Some(:? RuntimeFieldHandle as rfh) ->
             commonInitializeArray state address typ rfh
         | _ -> internalfailf $"initializeArray: case for (arrayRef = {arrayRef}), (handleTerm = {handleTerm}) is not implemented"
 
-    let allocateOptimizedArray state (fieldInfo : FieldInfo) =
+    let allocateOptimizedArray (state : state) (fieldInfo : FieldInfo) =
         let arrayType = typeof<byte>.MakeArrayType()
         let lb = makeNumber 0
         let length = internalSizeOf fieldInfo.FieldType |> makeNumber
-        let array = Memory.allocateArray state arrayType [lb] [length]
+        let array = state.memory.AllocateArray arrayType [lb] [length]
         commonInitializeArray state array arrayType fieldInfo.FieldHandle
         HeapRef array arrayType

VSharp.SILI.Core/Branching.fs

@@ -1,6 +1,7 @@
 namespace VSharp.Core
 
 open VSharp
+open Memory
 
 module internal Branching =
 
@@ -17,13 +18,13 @@ module internal Branching =
             match pcs with
             | [] -> k []
             | (pc, v)::pcs ->
-                let copyState (pc, v) k = f (Memory.copy state pc) v k
+                let copyState (pc, v) k = f (state.Copy pc) v k
                 Cps.List.mapk copyState pcs (fun results ->
                     state.pc <- pc
                     f state v (fun r ->
                     r::results |> mergeResults |> k)))
         | _ -> f state term (List.singleton >> k)
-    let guardedStatedApplyk f state term k = commonGuardedStatedApplyk f state term Memory.mergeResults k
+    let guardedStatedApplyk f state term k = commonGuardedStatedApplyk f state term State.mergeResults k
     let guardedStatedApply f state term = guardedStatedApplyk (Cps.ret2 f) state term id
 
     let guardedStatedMap mapper state term =
@@ -67,7 +68,7 @@ module internal Branching =
                     thenBranch conditionState (List.singleton >> k)
                 | SolverInteraction.SmtSat model ->
                     let thenState = conditionState
-                    let elseState = Memory.copy conditionState elsePc
+                    let elseState = conditionState.Copy elsePc
                     elseState.model <- model.mdl
                     assert(PC.toSeq elsePc |> conjunction |> elseState.model.Eval |> isTrue)
                     thenState.pc <- PC.add pc condition
@@ -103,7 +104,7 @@ module internal Branching =
                     elseBranch conditionState (List.singleton >> k)
                 | SolverInteraction.SmtSat model ->
                     let thenState = conditionState
-                    let elseState = Memory.copy conditionState (PC.add pc notCondition)
+                    let elseState = conditionState.Copy (PC.add pc notCondition)
                     thenState.model <- model.mdl
                     assert(PC.toSeq thenPc |> conjunction |> thenState.model.Eval |> isTrue)
                     TypeStorage.addTypeConstraint typeStorageCopy.Constraints notCondition
@@ -117,6 +118,6 @@ module internal Branching =
         else __unreachable__())
 
     let statedConditionalExecutionWithMergek state conditionInvocation thenBranch elseBranch k =
-        commonStatedConditionalExecutionk state conditionInvocation thenBranch elseBranch Memory.merge2Results k
+        commonStatedConditionalExecutionk state conditionInvocation thenBranch elseBranch State.merge2Results k
     let statedConditionalExecutionWithMerge state conditionInvocation thenBranch elseBranch =
         statedConditionalExecutionWithMergek state conditionInvocation thenBranch elseBranch id

VSharp.SILI.Core/Copying.fs

@@ -12,7 +12,7 @@ module internal Copying =
         let copyOneElem offset =
             let srcIndex = add srcIndex (makeNumber offset)
             let srcIndices = delinearizeArrayIndex srcIndex srcLens srcLBs
-            let srcElem = readArrayIndex state srcAddress srcIndices srcType
+            let srcElem = state.memory.ReadArrayIndex srcAddress srcIndices srcType
             let casted = TypeCasting.cast srcElem dstElemType
             let dstIndex = add dstIndex (makeNumber offset)
             let dstIndices = delinearizeArrayIndex dstIndex dstLens dstLBs
@@ -21,27 +21,29 @@ module internal Copying =
         let toWrite = List.map copyOneElem offsets
         let writeCopied (dstIndices, casted) =
             // Writing saved source elements
-            writeArrayIndex state dstAddress dstIndices dstType casted
+            state.memory.WriteArrayIndex dstAddress dstIndices dstType casted
         List.iter writeCopied toWrite
 
     let private copyArraySymbolic state srcAddress srcIndex srcType srcLens srcLBs dstAddress dstIndex dstType dstLens dstLBs length =
+        let memory = state.memory
         let dstElemType = dstType.elemType
         let srcFromIndices = delinearizeArrayIndex srcIndex srcLens srcLBs
         let lenMinOne = sub length (makeNumber 1)
         let srcToIndices = delinearizeArrayIndex (add srcIndex lenMinOne) srcLens srcLBs
-        let srcMemory = readArrayRange state srcAddress srcFromIndices srcToIndices srcType
+        let srcMemory = memory.ReadArrayRange srcAddress srcFromIndices srcToIndices srcType
         let casted = TypeCasting.cast srcMemory dstElemType
         let dstFromIndices = delinearizeArrayIndex dstIndex dstLens dstLBs
         let dstToIndices = delinearizeArrayIndex (add dstIndex lenMinOne) dstLens dstLBs
-        writeArrayRange state dstAddress dstFromIndices dstToIndices dstType casted
+        memory.WriteArrayRange dstAddress dstFromIndices dstToIndices dstType casted
 
     let private copyArrayCommon state srcAddress srcIndex srcType dstAddress dstIndex dstType length =
+        let memory = state.memory
         let srcDim = srcType.dimension
         let dstDim = dstType.dimension
-        let srcLBs = List.init srcDim (fun dim -> readLowerBound state srcAddress (makeNumber dim) srcType)
-        let srcLens = List.init srcDim (fun dim -> readLength state srcAddress (makeNumber dim) srcType)
-        let dstLBs = List.init dstDim (fun dim -> readLowerBound state dstAddress (makeNumber dim) dstType)
-        let dstLens = List.init dstDim (fun dim -> readLength state dstAddress (makeNumber dim) dstType)
+        let srcLBs = List.init srcDim (fun dim -> memory.ReadLowerBound srcAddress (makeNumber dim) srcType)
+        let srcLens = List.init srcDim (fun dim -> memory.ReadLength srcAddress (makeNumber dim) srcType)
+        let dstLBs = List.init dstDim (fun dim -> memory.ReadLowerBound dstAddress (makeNumber dim) dstType)
+        let dstLens = List.init dstDim (fun dim -> memory.ReadLength dstAddress (makeNumber dim) dstType)
         match length.term with
         | Concrete(l, _) ->
             let length = NumericUtils.ObjToInt l
@@ -54,10 +56,11 @@ module internal Copying =
 
     let copyArray state srcAddress srcIndex srcType dstAddress dstIndex dstType length =
         assert(isSafeContextCopy srcType dstType)
-        let cm = state.concreteMemory
-        let concreteSrcIndex = tryTermToObj state srcIndex
-        let concreteDstIndex = tryTermToObj state dstIndex
-        let concreteLength = tryTermToObj state length
+        let memory = state.memory
+        let cm = memory.ConcreteMemory
+        let concreteSrcIndex = memory.TryTermToObj srcIndex
+        let concreteDstIndex = memory.TryTermToObj dstIndex
+        let concreteLength = memory.TryTermToObj length
         match srcAddress.term, dstAddress.term, concreteSrcIndex, concreteDstIndex, concreteLength with
         | ConcreteHeapAddress src, ConcreteHeapAddress dst, Some srcI, Some dstI, Some l when cm.Contains src && cm.Contains dst ->
             let srcI = NumericUtils.ObjToLong srcI
@@ -68,13 +71,15 @@ module internal Copying =
         | _ -> copyArrayCommon state srcAddress srcIndex srcType dstAddress dstIndex dstType length
 
     let copyCharArrayToStringSymbolic (state : state) arrayAddress stringConcreteAddress startIndex arrayLength =
+        let memory = state.memory
         let stringAddress = ConcreteHeapAddress stringConcreteAddress
-        let stringAddress, arrayType = stringArrayInfo state stringAddress (Some arrayLength)
+        let stringAddress, arrayType = memory.StringArrayInfo stringAddress (Some arrayLength)
         copyArray state arrayAddress startIndex arrayType stringAddress (makeNumber 0) arrayType arrayLength
-        writeClassField state stringAddress Reflection.stringLengthField arrayLength
+        memory.WriteClassField stringAddress Reflection.stringLengthField arrayLength
 
     let copyCharArrayToString (state : state) arrayAddress stringConcreteAddress startIndex length =
-        let cm = state.concreteMemory
+        let memory = state.memory
+        let cm = memory.ConcreteMemory
         match arrayAddress.term, startIndex.term, length with
         | ConcreteHeapAddress concreteAddress, _, _ when concreteAddress = VectorTime.zero ->
             if cm.Contains stringConcreteAddress then
@@ -103,40 +108,42 @@ module internal Copying =
             if cm.Contains stringConcreteAddress then
                 cm.Remove stringConcreteAddress
             let arrayType = arrayType.CharVector
-            let length = readLength state arrayAddress (makeNumber 0) arrayType
+            let length = memory.ReadLength arrayAddress (makeNumber 0) arrayType
             copyCharArrayToStringSymbolic state arrayAddress stringConcreteAddress startIndex length
 
     let private fillArrayConcrete state arrayAddress arrayType startIndex length lbs lens castedValue =
         let offsets = List.init length id
         let copyOneElem offset =
             let linearIndex = add startIndex (makeNumber offset)
             let indices = delinearizeArrayIndex linearIndex lens lbs
-            writeArrayIndex state arrayAddress indices arrayType castedValue
+            state.memory.WriteArrayIndex arrayAddress indices arrayType castedValue
         List.iter copyOneElem offsets
 
     let private fillArraySymbolic state arrayAddress arrayType startIndex length lbs lens castedValue =
         let lastIndex = sub length (makeNumber 1)
         let lowerBounds = delinearizeArrayIndex startIndex lens lbs
         let upperBounds = delinearizeArrayIndex lastIndex lens lbs
-        writeArrayRange state arrayAddress lowerBounds upperBounds arrayType castedValue
+        state.memory.WriteArrayRange arrayAddress lowerBounds upperBounds arrayType castedValue
 
     let private fillArrayCommon state arrayAddress arrayType index length value =
+        let memory = state.memory
         let dim = arrayType.dimension
         let castedValue = TypeCasting.cast value arrayType.elemType
-        let lbs = List.init dim (fun dim -> readLowerBound state arrayAddress (makeNumber dim) arrayType)
-        let lens = List.init dim (fun dim -> readLength state arrayAddress (makeNumber dim) arrayType)
+        let lbs = List.init dim (fun dim -> memory.ReadLowerBound arrayAddress (makeNumber dim) arrayType)
+        let lens = List.init dim (fun dim -> memory.ReadLength arrayAddress (makeNumber dim) arrayType)
         match length.term with
         | Concrete(l, _) ->
             let length = NumericUtils.ObjToInt l
             fillArrayConcrete state arrayAddress arrayType index length lbs lens castedValue
         | _ -> fillArraySymbolic state arrayAddress arrayType index length lbs lens castedValue
 
     let fillArray state arrayAddress arrayType index length value =
-        let cm = state.concreteMemory
-        let concreteIndex = tryTermToObj state index
-        let concreteLength = tryTermToObj state length
+        let memory = state.memory
+        let cm = memory.ConcreteMemory
+        let concreteIndex = memory.TryTermToObj index
+        let concreteLength = memory.TryTermToObj length
         let castedValue = TypeCasting.cast value arrayType.elemType
-        let concreteValue = tryTermToObj state castedValue
+        let concreteValue = memory.TryTermToObj castedValue
         match arrayAddress.term, concreteIndex, concreteLength, concreteValue with
         | ConcreteHeapAddress address, Some i, Some l, Some v when cm.Contains address ->
             let i = NumericUtils.ObjToInt i