[feat] Allocate concrete objects in MkModel

VSharp.SILI.Core/API.fs

@@ -114,7 +114,7 @@ module API =
 
         let ReinterpretConcretes terms t = reinterpretConcretes terms t
 
-        let TryTermToObj state term = Memory.tryTermToObj state term
+        let TryTermToObj state objCreate term = Memory.tryTermToObj state objCreate term
 
         let (|ConcreteHeapAddress|_|) t = (|ConcreteHeapAddress|_|) t
 
@@ -273,6 +273,7 @@ module API =
             Memory.fillModelWithParametersAndThis modelState method
             StateModel(modelState, typeModel)
 
+        let Unmarshall state a = Memory.unmarshall state a
         let PopFrame state = Memory.popFrame state
         let ForcePopFrames count state = Memory.forcePopFrames count state
         let PopTypeVariables state = Memory.popTypeVariablesSubstitution state
@@ -357,6 +358,7 @@ module API =
         let ReadStaticField state typ field = Memory.readStaticField state typ field
         let ReadDelegate state reference = Memory.readDelegate state reference
 
+        let ReadArrayParams typ cha eval = Memory.readArrayParams typ cha eval 
         let InitializeArray state arrayRef handleTerm = ArrayInitialization.initializeArray state arrayRef handleTerm
 
         let WriteLocalVariable state location value = Memory.writeStackLocation state location value
@@ -464,8 +466,8 @@ module API =
 
         let StringFromReplicatedChar state string char length =
             let cm = state.concreteMemory
-            let concreteChar = Memory.tryTermToObj state char
-            let concreteLen = Memory.tryTermToObj state length
+            let concreteChar = Memory.tryTermToObj state (fun _ _ -> ()) char
+            let concreteLen = Memory.tryTermToObj state (fun _ _ -> ()) length
             let symbolicCase address =
                 let arrayType = typeof<char>, 1, true
                 Copying.fillArray state address arrayType (makeNumber 0) length char

VSharp.SILI.Core/API.fsi

@@ -71,7 +71,7 @@ module API =
 
         val ReinterpretConcretes : term list -> Type -> obj
 
-        val TryTermToObj : state -> term -> obj option
+        val TryTermToObj : state -> (concreteHeapAddress -> Type -> unit) -> term -> obj option
 
         val IsStruct : term -> bool
         val IsReference : term -> bool
@@ -209,6 +209,8 @@ module API =
     module public Memory =
         val EmptyState : unit -> state
         val EmptyModel : IMethod -> typeModel -> model
+
+        val Unmarshall : state -> concreteHeapAddress -> unit
         val PopFrame : state -> unit
         val ForcePopFrames : int -> state -> unit
         val PopTypeVariables : state -> unit
@@ -228,6 +230,7 @@ module API =
         val ReadStaticField : state -> Type -> fieldId -> term
         val ReadDelegate : state -> term -> term option
 
+        val ReadArrayParams : Type -> term -> (address -> int) -> arrayType * int array * int array
         val InitializeArray : state -> term -> term -> unit
 
         val Write : state -> term -> term -> state list

VSharp.SILI.Core/ArrayInitialization.fs

@@ -77,7 +77,7 @@ module internal ArrayInitialization =
     let initializeArray state arrayRef handleTerm =
         let cm = state.concreteMemory
         assert(Terms.isStruct handleTerm)
-        match arrayRef.term, Memory.tryTermToObj state handleTerm with
+        match arrayRef.term, Memory.tryTermToObj state (fun _ _ -> ()) handleTerm with
         | HeapRef({term = ConcreteHeapAddress address}, _), Some(:? RuntimeFieldHandle as rfh)
             when cm.Contains address ->
                 cm.InitializeArray address rfh

VSharp.SILI.Core/ConcreteMemory.fs

@@ -7,10 +7,11 @@ open System.Runtime.CompilerServices
 open System.Threading
 open VSharp
 
-type public ConcreteMemory private (physToVirt, virtToPhys) =
+type public ConcreteMemory private (physToVirt, virtToPhys, dependencies) =
 
     let mutable physToVirt = physToVirt
     let mutable virtToPhys = virtToPhys
+    let mutable dependencies = dependencies
 
 // ----------------------------- Helpers -----------------------------
 
@@ -84,7 +85,8 @@ type public ConcreteMemory private (physToVirt, virtToPhys) =
     new () =
         let physToVirt = Dictionary<physicalAddress, concreteHeapAddress>()
         let virtToPhys = Dictionary<concreteHeapAddress, physicalAddress>()
-        ConcreteMemory(physToVirt, virtToPhys)
+        let deps =  Dictionary<concreteHeapAddress, concreteHeapAddress list>()
+        ConcreteMemory(physToVirt, virtToPhys, deps)
 
 // ----------------------------- Primitives -----------------------------
 
@@ -97,21 +99,33 @@ type public ConcreteMemory private (physToVirt, virtToPhys) =
         let physicalAddress = {object = obj}
         virtToPhys[address] <- physicalAddress
 
+    member private x.getDepsList ds =
+        // TODO: rewrite it more effectively
+        let ds' = ds |> Set.ofList |> Set.toList
+        let ds'' = ds |> List.collect (fun a -> if dependencies.ContainsKey(a) then a::dependencies[a] else [a])  
+                      |> Set.ofList |> Set.toList
+        if ds' = ds'' then ds'
+        else x.getDepsList ds''
+
 // ------------------------------- Copying -------------------------------
 
     interface IConcreteMemory with
 
         override x.Copy() =
             let physToVirt' = Dictionary<physicalAddress, concreteHeapAddress>()
             let virtToPhys' = Dictionary<concreteHeapAddress, physicalAddress>()
+            let deps' =  Dictionary<concreteHeapAddress, concreteHeapAddress list>()
             copiedObjects.Clear()
             for kvp in physToVirt do
                 let phys, virt = kvp.Key, kvp.Value
                 let phys' = deepCopyObject phys
                 if virtToPhys.ContainsKey virt then
                     virtToPhys'.Add(virt, phys')
+                    if dependencies.ContainsKey virt then
+                        let d' = dependencies[virt] // TODO: deepcopy
+                        deps'.Add(virt, d')
                 physToVirt'.Add(phys', virt)
-            ConcreteMemory(physToVirt', virtToPhys')
+            ConcreteMemory(physToVirt', virtToPhys', deps')
 
 // ----------------------------- Primitives -----------------------------
 
@@ -210,8 +224,19 @@ type public ConcreteMemory private (physToVirt, virtToPhys) =
             let physAddress = {object = string}
             physToVirt[physAddress] <- stringAddress
 
+    // ------------------------------- Dependencies -------------------------    
+        override x.AddDep virtAddr1 virtAddr2 =
+            let value = if dependencies.ContainsKey virtAddr1 then virtAddr2::dependencies[virtAddr1] else [virtAddr2]
+            dependencies[virtAddr1] <- value
+
+        override x.GetDeps addr =
+            x.getDepsList [addr]
+
     // ------------------------------- Remove -------------------------------
 
         override x.Remove address =
-            let removed = virtToPhys.Remove address
+            let toRemove = x.getDepsList [address]
+            let removed = toRemove |> List.map (fun a ->
+                dependencies.Remove a |> ignore
+                virtToPhys.Remove a) |> List.forall id
             assert removed

VSharp.SILI.Core/Memory.fs

@@ -360,6 +360,7 @@ module internal Memory =
                 let t = method.DeclaringType
                 let addr = [-1]
                 let thisRef = HeapRef (ConcreteHeapAddress addr) t
+                state.concreteMemory.Allocate addr (Reflection.createObject t) // TODO: do we need here protection from abstract types?
                 state.allocatedTypes <- PersistentDict.add addr (ConcreteType t) state.allocatedTypes
                 state.startingTime <- [-2]
                 (ThisKey method, Some thisRef, t) :: parameters // TODO: incorrect type when ``this'' is Ref to stack
@@ -376,6 +377,16 @@ module internal Memory =
         assert(not typ.IsAbstract)
         let concreteAddress = freshAddress state
         assert(not <| PersistentDict.contains concreteAddress state.allocatedTypes)
+        match state.model with
+        | PrimitiveModel _ ->
+            // try concrete allocation
+            let cm = state.concreteMemory
+            assert(not <| cm.Contains concreteAddress)
+            try
+                cm.Allocate concreteAddress (Reflection.createObject typ)
+            with
+            | _ -> ()
+        | _ -> ()
         state.allocatedTypes <- PersistentDict.add concreteAddress (ConcreteType typ) state.allocatedTypes
         concreteAddress
 
@@ -430,10 +441,14 @@ module internal Memory =
 
     // ---------------- Try term to object ----------------
 
-    let tryAddressToObj (state : state) address =
+    let tryAddressToObj (state : state) objCreate address (typ : Type) =
         if address = VectorTime.zero then Some null
-        else state.concreteMemory.TryVirtToPhys address
-
+        else
+            match state.concreteMemory.TryVirtToPhys address with
+            | Some o -> Some o
+            | None ->
+                objCreate address typ
+                state.concreteMemory.TryVirtToPhys address
     let tryPointerToObj state address (offset : int) =
         let cm = state.concreteMemory
         match cm.TryVirtToPhys address with
@@ -443,21 +458,21 @@ module internal Memory =
             Some (pObj :> obj)
         | None -> None
 
-    let rec tryTermToObj (state : state) term =
+    let rec tryTermToObj (state : state) objCreate term =
         match term.term with
         | Concrete(obj, _) -> Some obj
-        | Struct(fields, typ) when isNullable typ -> tryNullableTermToObj state fields typ
-        | Struct(fields, typ) when not typ.IsByRefLike -> tryStructTermToObj state fields typ
-        | HeapRef({term = ConcreteHeapAddress a}, _) -> tryAddressToObj state a
+        | Struct(fields, typ) when isNullable typ -> tryNullableTermToObj state objCreate fields typ
+        | Struct(fields, typ) when not typ.IsByRefLike -> tryStructTermToObj state objCreate fields typ
+        | HeapRef({term = ConcreteHeapAddress a}, typ) -> tryAddressToObj state objCreate a typ
         | Ptr(HeapLocation({term = ConcreteHeapAddress a}, _), _, ConcreteT (:? int as offset, _)) ->
             tryPointerToObj state a offset
         | _ -> None
 
-    and tryStructTermToObj (state : state) fields typ =
+    and tryStructTermToObj (state : state) objCreate fields typ =
         let structObj = Reflection.createObject typ
         let addField _ (fieldId, value) k =
             let fieldInfo = Reflection.getFieldInfo fieldId
-            match tryTermToObj state value with
+            match tryTermToObj state objCreate value with
             // field was not found in the structure, skipping it
             | _ when fieldInfo = null -> k ()
             // field can be converted to obj, so continue
@@ -466,11 +481,11 @@ module internal Memory =
             | None -> None
         Cps.Seq.foldlk addField () (PersistentDict.toSeq fields) (fun _ -> Some structObj)
 
-    and tryNullableTermToObj (state : state) fields typ =
+    and tryNullableTermToObj (state : state) objCreate fields typ =
         let valueField, hasValueField = Reflection.fieldsOfNullable typ
         let value = PersistentDict.find fields valueField
         let hasValue = PersistentDict.find fields hasValueField
-        match tryTermToObj state value with
+        match tryTermToObj state objCreate value with
         | Some obj when hasValue = True -> Some obj
         | _ when hasValue = False -> Some null
         | _ -> None
@@ -684,6 +699,23 @@ module internal Memory =
         | StackBufferIndex(key, index) -> readStackBuffer state key index
         | ArrayLowerBound(address, dimension, typ) -> readLowerBound state address dimension typ
 
+    let readArrayParams typ cha eval =
+        match typ with
+        | ArrayType(elemType, dim) ->   
+            let arrayType, (lengths : int array), (lowerBounds : int array) =
+                match dim with
+                | Vector ->
+                    let arrayType = (elemType, 1, true)
+                    arrayType, [| ArrayLength(cha, makeNumber 0, arrayType) |> eval |], null
+                | ConcreteDimension rank ->
+                    let arrayType = (elemType, rank, false)
+                    arrayType,
+                    Array.init rank (fun i -> ArrayLength(cha, makeNumber i, arrayType) |> eval),
+                    Array.init rank (fun i -> ArrayLowerBound(cha, makeNumber i, arrayType) |> eval)
+                | SymbolicDimension -> __unreachable__()
+            arrayType, lengths, lowerBounds
+        | _ -> internalfail "reading array parameters for invalid type"
+
 // ------------------------------- Unsafe reading -------------------------------
 
     let private checkBlockBounds state reportError blockSize startByte endByte =
@@ -938,7 +970,7 @@ module internal Memory =
 
     let writeBoxedLocation state (address : concreteHeapAddress) value =
         let cm = state.concreteMemory
-        match tryTermToObj state value with
+        match tryTermToObj state (fun _ _ -> ()) value with
         | Some value when cm.Contains(address) ->
             cm.Remove address
             cm.Allocate address value
@@ -982,37 +1014,45 @@ module internal Memory =
         writeArrayIndexSymbolic state address [stringLength] (tChar, 1, true) (Concrete '\000' tChar)
         writeClassFieldSymbolic state address Reflection.stringLengthField stringLength
 
-    let unmarshall (state : state) concreteAddress =
-        let address = ConcreteHeapAddress concreteAddress
-        let cm = state.concreteMemory
-        let obj = cm.VirtToPhys concreteAddress
+    let unmarshallObj state address (obj : obj) =
         assert(box obj <> null)
         match obj with
         | :? Array as array -> unmarshallArray state address array
         | :? String as string -> unmarshallString state address string
         | _ -> unmarshallClass state address obj
+
+    let unmarshall (state : state) concreteAddress =
+        let cm = state.concreteMemory
+        let deps = cm.GetDeps concreteAddress |> List.map (fun a -> cm.VirtToPhys a, ConcreteHeapAddress a)
+        deps |> List.iter (fun (d, a) -> unmarshallObj state a d)
         cm.Remove concreteAddress
 
 // ------------------------------- Writing -------------------------------
 
     let writeClassField state address (field : fieldId) value =
         let cm = state.concreteMemory
-        let concreteValue = tryTermToObj state value
+        let concreteValue = tryTermToObj state (fun _ _ -> ()) value
         match address.term, concreteValue with
         | ConcreteHeapAddress concreteAddress, Some obj when cm.Contains concreteAddress ->
             cm.WriteClassField concreteAddress field obj
+            match value with
+            | {term = HeapRef({term = ConcreteHeapAddress(a)}, _)} -> cm.AddDep a concreteAddress
+            | _ -> ()
         | ConcreteHeapAddress concreteAddress, None when cm.Contains concreteAddress ->
             unmarshall state concreteAddress
             writeClassFieldSymbolic state address field value
         | _ -> writeClassFieldSymbolic state address field value
 
     let writeArrayIndex state address indices arrayType value =
         let cm = state.concreteMemory
-        let concreteValue = tryTermToObj state value
+        let concreteValue = tryTermToObj state (fun _ _ -> ()) value
         let concreteIndices = tryIntListFromTermList indices
         match address.term, concreteValue, concreteIndices with
         | ConcreteHeapAddress a, Some obj, Some concreteIndices when cm.Contains a ->
             cm.WriteArrayIndex a concreteIndices obj
+            match value with
+            | {term = HeapRef({term = ConcreteHeapAddress(addr)}, _)} -> cm.AddDep addr a
+            | _ -> ()
         | ConcreteHeapAddress a, _, None
         | ConcreteHeapAddress a, None, _ when cm.Contains a ->
             unmarshall state a

VSharp.SILI.Core/State.fs

@@ -28,6 +28,8 @@ type IConcreteMemory =
     abstract WriteArrayIndex : concreteHeapAddress -> int list -> obj -> unit
     abstract InitializeArray : concreteHeapAddress -> RuntimeFieldHandle -> unit
     abstract CopyCharArrayToString : concreteHeapAddress -> concreteHeapAddress -> unit
+    abstract GetDeps : concreteHeapAddress -> concreteHeapAddress list
+    abstract AddDep : concreteHeapAddress -> concreteHeapAddress -> unit
     abstract Remove : concreteHeapAddress -> unit
 
 type IMethodMock =

VSharp.SILI.Core/TypeSolver.fs

@@ -331,14 +331,22 @@ module TypeSolver =
         | StateModel(modelState, typeModel) ->
             match solverResult with
             | TypeSat(refsTypes, typeParams) ->
+                let cm = modelState.concreteMemory
                 let refineTypes addr t =
-                    modelState.allocatedTypes <- PersistentDict.add addr t modelState.allocatedTypes
                     match t with
                     | ConcreteType t ->
-                        if t.IsValueType then
-                            let value = makeDefaultValue t
-                            modelState.boxedLocations <- PersistentDict.add addr value modelState.boxedLocations
-                    | _ -> ()
+                        match cm.TryVirtToPhys addr with
+                        | Some o ->
+                            let t1 = TypeUtils.getTypeOfConcrete o
+                            if t <> t1 then
+                                cm.Remove addr
+                                cm.Allocate addr (Reflection.createObject t)
+                        | None ->
+                            if t.IsValueType then
+                                let value = makeDefaultValue t
+                                modelState.boxedLocations <- PersistentDict.add addr value modelState.boxedLocations
+                    | MockType _ -> if cm.Contains addr then Memory.unmarshall modelState addr
+                    modelState.allocatedTypes <- PersistentDict.add addr t modelState.allocatedTypes
                 Seq.iter2 refineTypes addresses refsTypes
                 let classParams, methodParams = Array.splitAt typeGenericArguments.Length typeParams
                 typeModel.classesParams <- classParams

VSharp.SILI/Interpreter.fs

@@ -1012,9 +1012,9 @@ type internal ILInterpreter(isConcolicMode : bool) as this =
         if method.IsConcretelyInvokable && Loader.isInvokeInternalCall fullMethodName then
             // Before term args, type args are located
             let termArgs = List.skip (List.length args - method.Parameters.Length) args
-            let objArgs = List.choose (TryTermToObj state) termArgs
+            let objArgs = List.choose (TryTermToObj state (fun _ _ -> ())) termArgs
             let hasThis = Option.isSome thisOption
-            let thisObj = Option.bind (TryTermToObj state) thisOption
+            let thisObj = Option.bind (TryTermToObj state (fun _ _ -> ())) thisOption
             match thisObj with
             | _ when List.length objArgs <> List.length termArgs -> false
             | None when hasThis -> false
@@ -1140,6 +1140,7 @@ type internal ILInterpreter(isConcolicMode : bool) as this =
                     match model with
                     | StateModel(s, _) -> s
                     | _ -> __unreachable__()
+                if modelState.concreteMemory.Contains thisInModel then Memory.Unmarshall modelState thisInModel 
                 modelState.allocatedTypes <- PersistentDict.add thisInModel (MockType mock) modelState.allocatedTypes
                 candidateTypes |> Seq.iter (function
                     | ConcreteType t -> AddConstraint cilState.state !!(Types.TypeIsRef cilState.state t this)