diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index 72d36040f..9f18a4f0d 100644 --- a/VSharp.SILI.Core/API.fs +++ b/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, 1, true Copying.fillArray state address arrayType (makeNumber 0) length char diff --git a/VSharp.SILI.Core/API.fsi b/VSharp.SILI.Core/API.fsi index 412633571..ef1ab6831 100644 --- a/VSharp.SILI.Core/API.fsi +++ b/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 diff --git a/VSharp.SILI.Core/ArrayInitialization.fs b/VSharp.SILI.Core/ArrayInitialization.fs index 2fb811cd5..4eb11e3a4 100644 --- a/VSharp.SILI.Core/ArrayInitialization.fs +++ b/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 diff --git a/VSharp.SILI.Core/ConcreteMemory.fs b/VSharp.SILI.Core/ConcreteMemory.fs index 1d4bff0ab..75342a24d 100644 --- a/VSharp.SILI.Core/ConcreteMemory.fs +++ b/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() let virtToPhys = Dictionary() - ConcreteMemory(physToVirt, virtToPhys) + let deps = Dictionary() + ConcreteMemory(physToVirt, virtToPhys, deps) // ----------------------------- Primitives ----------------------------- @@ -97,6 +99,14 @@ 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 @@ -104,14 +114,18 @@ type public ConcreteMemory private (physToVirt, virtToPhys) = override x.Copy() = let physToVirt' = Dictionary() let virtToPhys' = Dictionary() + let deps' = Dictionary() 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 diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index 49d4e860c..105dd7adb 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/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,25 +1014,30 @@ 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 @@ -1008,11 +1045,14 @@ module internal Memory = 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 diff --git a/VSharp.SILI.Core/State.fs b/VSharp.SILI.Core/State.fs index 509519640..8ce9bf670 100644 --- a/VSharp.SILI.Core/State.fs +++ b/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 = diff --git a/VSharp.SILI.Core/TypeSolver.fs b/VSharp.SILI.Core/TypeSolver.fs index f2d759a24..6283cbc68 100644 --- a/VSharp.SILI.Core/TypeSolver.fs +++ b/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 diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index fdf8f9c76..f1d1d713b 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/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) diff --git a/VSharp.SILI/TestGenerator.fs b/VSharp.SILI/TestGenerator.fs index 9ceb0ed59..a8fa3f5a4 100644 --- a/VSharp.SILI/TestGenerator.fs +++ b/VSharp.SILI/TestGenerator.fs @@ -31,20 +31,12 @@ module TestGenerator = | ConcreteType typ -> let cha = ConcreteHeapAddress addr match typ with - | TypeUtils.ArrayType(elemType, dim) -> + | TypeUtils.ArrayType(_, SymbolicDimension _) -> __notImplemented__() + | TypeUtils.ArrayType _ -> let index = test.MemoryGraph.ReserveRepresentation() indices.Add(addr, index) let arrayType, (lengths : int array), (lowerBounds : int array) = - match dim with - | Vector -> - let arrayType = (elemType, 1, true) - arrayType, [| ArrayLength(cha, MakeNumber 0, arrayType) |> eval |> unbox |], null - | ConcreteDimension rank -> - let arrayType = (elemType, rank, false) - arrayType, - Array.init rank (fun i -> ArrayLength(cha, MakeNumber i, arrayType) |> eval |> unbox), - Array.init rank (fun i -> ArrayLowerBound(cha, MakeNumber i, arrayType) |> eval |> unbox) - | SymbolicDimension -> __notImplemented__() + Memory.ReadArrayParams typ cha (eval >> unbox) let length = Array.reduce ( * ) lengths // TODO: normalize model (for example, try to minimize lengths of generated arrays) if maxBufferSize > 0 && length > maxBufferSize then @@ -68,7 +60,7 @@ module TestGenerator = let encodeArrayCompactly (state : state) (model : model) (encode : term -> obj) (test : UnitTest) arrayType cha typ lengths lowerBounds index = if state.concreteMemory.Contains cha then - test.MemoryGraph.AddArray typ (state.concreteMemory.VirtToPhys cha :?> Array |> Array.mapToOneDArray test.MemoryGraph.Encode) lengths lowerBounds index + test.MemoryGraph.AddArray typ (state.concreteMemory.VirtToPhys cha :?> Array |> Array.mapToOneDArray (test.MemoryGraph.Encode >> fst)) lengths lowerBounds index else let arrays = if VectorTime.less cha VectorTime.zero then @@ -101,7 +93,7 @@ module TestGenerator = // TODO: if addr is managed by concrete memory, then just serialize it normally (by test.MemoryGraph.AddArray) test.MemoryGraph.AddCompactArrayRepresentation typ defaultValue indices values lengths lowerBounds index - let rec private term2obj (model : model) state indices mockCache (test : UnitTest) = function + let rec private term2obj (model : model) state (indices : Dictionary) mockCache (test : UnitTest) = function | {term = Concrete(_, TypeUtils.AddressType)} -> __unreachable__() | {term = Concrete(v, t)} when t.IsEnum -> test.MemoryGraph.RepresentEnum v | {term = Concrete(v, _)} -> v @@ -122,11 +114,24 @@ module TestGenerator = | {term = HeapRef({term = ConcreteHeapAddress(addr)}, _)} when VectorTime.less addr VectorTime.zero -> match model with | StateModel(modelState, _) -> - let eval address = - address |> Ref |> Memory.Read modelState |> model.Complete |> term2obj model state indices mockCache test - let arr2Obj = encodeArrayCompactly state model (term2obj model state indices mockCache test) - let typ = modelState.allocatedTypes.[addr] - obj2test eval arr2Obj indices (encodeTypeMock model state indices mockCache test >> test.AllocateMockObject) test addr typ + match modelState.concreteMemory.TryVirtToPhys addr with + | Some o -> + let index = ref 0 + if indices.TryGetValue(addr, index) then + let referenceRepr : referenceRepr = {index = index.Value} + referenceRepr :> obj + else + let orepr, index = test.MemoryGraph.Encode o + match index with + | Some i -> indices.Add(addr, i) + | None -> () + orepr + | None -> // mocks and big arrays are allocated symbolically + let eval address = + address |> Ref |> Memory.Read modelState |> model.Complete |> term2obj model state indices mockCache test + let arr2Obj = encodeArrayCompactly state model (term2obj model state indices mockCache test) + let typ = modelState.allocatedTypes.[addr] + obj2test eval arr2Obj indices (encodeTypeMock model state indices mockCache test >> test.AllocateMockObject) test addr typ | PrimitiveModel _ -> __unreachable__() | {term = HeapRef({term = ConcreteHeapAddress(addr)}, _)} -> let eval address = @@ -223,7 +228,8 @@ module TestGenerator = if not isError && not hasException then let retVal = model.Eval cilState.Result - test.Expected <- term2obj model cilState.state indices mockCache test retVal + let tmp = term2obj model cilState.state indices mockCache test retVal + test.Expected <- tmp Some test | _ -> __unreachable__() diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 04845e5c1..6f9ac43ab 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -10,7 +10,6 @@ open VSharp.Core.SolverInteraction open Logger module internal Z3 = - // ------------------------------- Exceptions ------------------------------- type EncodingException(msg : string) = @@ -69,13 +68,88 @@ module internal Z3 = lastSymbolicAddress = 0 } + // -----------------------Concrete memory ------------------------- + let rec unboxConcrete state defaults term = + match Terms.TryTermToObj state (createObjOfType state defaults) term with + | Some o -> Some (o |> unbox) + | None -> None + + and createObjOfType state (defaults : Dictionary) addr typ = + let cm = state.concreteMemory + try + let unboxConcrete' t = unboxConcrete state defaults t + let cha = addr |> ConcreteHeapAddress + let result = ref (ref Nop) + match typ with + | ArrayType(_, SymbolicDimension _) -> () + | ArrayType(elemType, _) -> + let eval address = + address |> Ref |> Memory.Read state |> unboxConcrete' |> Option.get + let arrayType, (lengths : int array), (lowerBounds : int array) = + Memory.ReadArrayParams typ cha eval + let length = Array.reduce ( * ) lengths + if length > 128 then () // TODO: move magic number + else + let arr = if (lowerBounds = null) then Array.CreateInstance(elemType, lengths) + else Array.CreateInstance(elemType, lengths, lowerBounds) + cm.Allocate addr arr + if defaults.TryGetValue(ArrayIndexSort arrayType, result) then + match result.Value.Value with + | {term = HeapRef({term = ConcreteHeapAddress(a)}, _)} -> + cm.AddDep a addr + | _ -> () + let value = result.Value.Value |> unboxConcrete' |> Option.get + Array.fill arr value + | _ when typ = typeof -> + let arTyp = (typeof, 1, true) + let l : int = ClassField(cha, Reflection.stringLengthField) |> Ref + |> Memory.Read state |> unboxConcrete' |> Option.get + let contents = Array.init l (fun i -> ArrayIndex(cha, [MakeNumber i], arTyp) |> Ref + |> Memory.Read state |> unboxConcrete' |> Option.get) + cm.Allocate addr (String(contents) :> obj) + | _ -> + let o = Reflection.createObject typ + cm.Allocate addr o + Reflection.fieldsOf false typ |> + Seq.iter (fun (fid, _) -> + let region = HeapFieldSort fid + if defaults.TryGetValue(region, result) then + let value = result.Value.Value |> unboxConcrete' |> Option.get + match result.Value.Value with + | {term = HeapRef({term = ConcreteHeapAddress(a)}, _)} -> + cm.AddDep a addr + | _ -> () + cm.WriteClassField addr fid value + ) + with + // when objects are created, the are only filled with defaults + // Careful: the use of unmarshalling here is incorrect + | :? MemberAccessException // Could not create an instance + | :? ArgumentException as e -> // Could not unbox concrete or type is not supported + if cm.Contains addr then cm.Remove addr + raise e + | _ -> internalfail "Unexpected exception in object creation" + + let concreteAllocator state defaultValues typ addr = + let cm = state.concreteMemory + if VectorTime.less addr VectorTime.zero then + state.allocatedTypes <- PersistentDict.add addr (ConcreteType typ) state.allocatedTypes + if cm.Contains addr then () + else + try + createObjOfType state defaultValues addr typ + with // if type cannot be allocated concretely, it will be stored symbolically + | :? MemberAccessException -> () // Could not create an instance + | :? ArgumentException -> () // Could not unbox concrete ot type is not supported + | _ -> internalfail "Unexpected exception in object creation" + // ------------------------------- Encoding: primitives ------------------------------- type private Z3Builder(ctx : Context) = let mutable encodingCache = freshCache() let emptyState = Memory.EmptyState() let mutable maxBufferSize = 128 - + let defaultValues = Dictionary() let getMemoryConstant mkConst (typ : regionSort * fieldId list) = let result : ArrayExpr ref = ref null if encodingCache.regionConstants.TryGetValue(typ, result) then result.Value @@ -563,12 +637,12 @@ module internal Z3 = // ------------------------------- Decoding ------------------------------- - member private x.DecodeExpr op t (expr : Expr) = + member private x.DecodeExpr state op t cmAllocate (expr : Expr) = // TODO: bug -- decoding arguments with type of expression - Expression (Operator op) (expr.Args |> Seq.map (x.Decode t) |> List.ofSeq) t + Expression (Operator op) (expr.Args |> Seq.map (x.Decode state t cmAllocate) |> List.ofSeq) t - member private x.DecodeBoolExpr op (expr : Expr) = - x.DecodeExpr op typeof expr + member private x.DecodeBoolExpr state op cmAllocate (expr : Expr) = + x.DecodeExpr state op typeof cmAllocate expr member private x.GetTypeOfBV (bv : BitVecExpr) = if bv.SortSize = 32u then typeof @@ -577,8 +651,9 @@ module internal Z3 = elif bv.SortSize = 16u then typeof else __unreachable__() - member private x.DecodeConcreteHeapAddress typ (expr : Expr) : vectorTime = + member private x.DecodeConcreteHeapAddress state typ cmAllocate (expr : Expr) : vectorTime = // TODO: maybe throw away typ? + let cm = state.concreteMemory let result = ref vectorTime.Empty let checkAndGet key = encodingCache.heapAddresses.TryGetValue(key, result) let charArray = typeof @@ -588,12 +663,16 @@ module internal Z3 = // NOTE: storing most concrete type for string encodingCache.heapAddresses.Remove((charArray, expr)) |> ignore encodingCache.heapAddresses.Add((typ, expr), result.Value) + // strings are filled symbolically + if cm.Contains result.Value then Memory.Unmarshall state result.Value result.Value elif typ = charArray && checkAndGet (typeof, expr) then result.Value else encodingCache.lastSymbolicAddress <- encodingCache.lastSymbolicAddress - 1 let addr = [encodingCache.lastSymbolicAddress] encodingCache.heapAddresses.Add((typ, expr), addr) + if cmAllocate then + concreteAllocator state defaultValues typ addr addr member private x.DecodeSymbolicTypeAddress (expr : Expr) = @@ -601,14 +680,14 @@ module internal Z3 = if encodingCache.staticKeys.TryGetValue(expr, result) then result.Value else __notImplemented__() - member private x.DecodeMemoryKey (reg : regionSort) (exprs : Expr array) = + member private x.DecodeMemoryKey state (reg : regionSort) cmAllocate (exprs : Expr array) = let toType (elementType : Type, rank, isVector) = if isVector then elementType.MakeArrayType() else elementType.MakeArrayType(rank) match reg with | HeapFieldSort field -> assert(exprs.Length = 1) - let address = exprs.[0] |> x.DecodeConcreteHeapAddress field.declaringType |> ConcreteHeapAddress + let address = exprs.[0] |> x.DecodeConcreteHeapAddress state field.declaringType cmAllocate |> ConcreteHeapAddress ClassField(address, field) | StaticFieldSort field -> assert(exprs.Length = 1) @@ -616,22 +695,22 @@ module internal Z3 = StaticField(typ, field) | ArrayIndexSort typ -> assert(exprs.Length >= 2) - let heapAddress = exprs.[0] |> x.DecodeConcreteHeapAddress (toType typ) |> ConcreteHeapAddress - let indices = exprs |> Seq.tail |> Seq.map (x.Decode Types.IndexType) |> List.ofSeq + let heapAddress = exprs.[0] |> x.DecodeConcreteHeapAddress state (toType typ) cmAllocate |> ConcreteHeapAddress + let indices = exprs |> Seq.tail |> Seq.map (x.Decode state Types.IndexType cmAllocate) |> List.ofSeq ArrayIndex(heapAddress, indices, typ) | ArrayLengthSort typ -> assert(exprs.Length = 2) - let heapAddress = exprs.[0] |> x.DecodeConcreteHeapAddress (toType typ) |> ConcreteHeapAddress - let index = x.Decode Types.IndexType exprs.[1] + let heapAddress = exprs.[0] |> x.DecodeConcreteHeapAddress state (toType typ) cmAllocate |> ConcreteHeapAddress + let index = x.Decode state Types.IndexType cmAllocate exprs.[1] ArrayLength(heapAddress, index, typ) | ArrayLowerBoundSort typ -> assert(exprs.Length = 2) - let heapAddress = exprs.[0] |> x.DecodeConcreteHeapAddress (toType typ) |> ConcreteHeapAddress - let index = x.Decode Types.IndexType exprs.[1] + let heapAddress = exprs.[0] |> x.DecodeConcreteHeapAddress state (toType typ) cmAllocate |> ConcreteHeapAddress + let index = x.Decode state Types.IndexType cmAllocate exprs.[1] ArrayLowerBound(heapAddress, index, typ) | StackBufferSort key -> assert(exprs.Length = 1) - let index = x.Decode typeof exprs.[0] + let index = x.Decode state typeof cmAllocate exprs.[0] StackBufferIndex(key, index) member private x.DecodeBv t (bv : BitVecNum) = @@ -642,11 +721,11 @@ module internal Z3 = | 8u -> Concrete (convert bv.Int t) t | _ -> __notImplemented__() - member public x.Decode t (expr : Expr) = + member public x.Decode state t cmAllocate (expr : Expr) = match expr with | :? BitVecNum as bv when Types.IsNumeric t -> x.DecodeBv t bv | :? BitVecNum as bv when not (Types.IsValueType t) -> - let address = x.DecodeConcreteHeapAddress t bv |> ConcreteHeapAddress + let address = x.DecodeConcreteHeapAddress state t cmAllocate bv |> ConcreteHeapAddress HeapRef address t | :? BitVecExpr as bv when bv.IsConst -> if encodingCache.e2t.ContainsKey(expr) then encodingCache.e2t.[expr] @@ -657,18 +736,18 @@ module internal Z3 = if encodingCache.e2t.ContainsKey(expr) then encodingCache.e2t.[expr] elif expr.IsTrue then True elif expr.IsFalse then False - elif expr.IsNot then x.DecodeBoolExpr OperationType.LogicalNot expr - elif expr.IsAnd then x.DecodeBoolExpr OperationType.LogicalAnd expr - elif expr.IsOr then x.DecodeBoolExpr OperationType.LogicalOr expr - elif expr.IsEq then x.DecodeBoolExpr OperationType.Equal expr - elif expr.IsBVSGT then x.DecodeBoolExpr OperationType.Greater expr - elif expr.IsBVUGT then x.DecodeBoolExpr OperationType.Greater_Un expr - elif expr.IsBVSGE then x.DecodeBoolExpr OperationType.GreaterOrEqual expr - elif expr.IsBVUGE then x.DecodeBoolExpr OperationType.GreaterOrEqual_Un expr - elif expr.IsBVSLT then x.DecodeBoolExpr OperationType.Less expr - elif expr.IsBVULT then x.DecodeBoolExpr OperationType.Less_Un expr - elif expr.IsBVSLE then x.DecodeBoolExpr OperationType.LessOrEqual expr - elif expr.IsBVULE then x.DecodeBoolExpr OperationType.LessOrEqual_Un expr + elif expr.IsNot then x.DecodeBoolExpr state OperationType.LogicalNot cmAllocate expr + elif expr.IsAnd then x.DecodeBoolExpr state OperationType.LogicalAnd cmAllocate expr + elif expr.IsOr then x.DecodeBoolExpr state OperationType.LogicalOr cmAllocate expr + elif expr.IsEq then x.DecodeBoolExpr state OperationType.Equal cmAllocate expr + elif expr.IsBVSGT then x.DecodeBoolExpr state OperationType.Greater cmAllocate expr + elif expr.IsBVUGT then x.DecodeBoolExpr state OperationType.Greater_Un cmAllocate expr + elif expr.IsBVSGE then x.DecodeBoolExpr state OperationType.GreaterOrEqual cmAllocate expr + elif expr.IsBVUGE then x.DecodeBoolExpr state OperationType.GreaterOrEqual_Un cmAllocate expr + elif expr.IsBVSLT then x.DecodeBoolExpr state OperationType.Less cmAllocate expr + elif expr.IsBVULT then x.DecodeBoolExpr state OperationType.Less_Un cmAllocate expr + elif expr.IsBVSLE then x.DecodeBoolExpr state OperationType.LessOrEqual cmAllocate expr + elif expr.IsBVULE then x.DecodeBoolExpr state OperationType.LessOrEqual_Un cmAllocate expr else __notImplemented__() member private x.WriteFields structure value = function @@ -695,11 +774,12 @@ module internal Z3 = let subst = Dictionary() let stackEntries = Dictionary() let state = {Memory.EmptyState() with complete = true} + let cm = state.concreteMemory encodingCache.t2e |> Seq.iter (fun kvp -> match kvp.Key with | {term = Constant(_, StructFieldChain(fields, StackReading(key)), t)} as constant -> let refinedExpr = m.Eval(kvp.Value.expr, false) - let decoded = x.Decode t refinedExpr + let decoded = x.Decode state t false refinedExpr if decoded <> constant then x.WriteDictOfValueTypes stackEntries key fields key.TypeOfLocation decoded | {term = Constant(_, (:? IMemoryAccessConstantSource as ms), _)} as constant -> @@ -707,19 +787,19 @@ module internal Z3 = | HeapAddressSource(StackReading(key)) -> let refinedExpr = m.Eval(kvp.Value.expr, false) let t = key.TypeOfLocation - let addr = refinedExpr |> x.DecodeConcreteHeapAddress t |> ConcreteHeapAddress + let addr = refinedExpr |> x.DecodeConcreteHeapAddress state t false |> ConcreteHeapAddress stackEntries.Add(key, HeapRef addr t |> ref) | HeapAddressSource(:? functionResultConstantSource as frs) -> let refinedExpr = m.Eval(kvp.Value.expr, false) let t = (frs :> ISymbolicConstantSource).TypeOfLocation - let term = x.Decode t refinedExpr + let term = x.Decode state t false refinedExpr assert(not (constant = term) || kvp.Value.expr = refinedExpr) if constant <> term then subst.Add(ms, term) | _ -> () | {term = Constant(_, :? IStatedSymbolicConstantSource, _)} -> () | {term = Constant(_, source, t)} as constant -> let refinedExpr = m.Eval(kvp.Value.expr, false) - let term = x.Decode t refinedExpr + let term = x.Decode state t false refinedExpr assert(not (constant = term) || kvp.Value.expr = refinedExpr) if constant <> term then subst.Add(source, term) | _ -> ()) @@ -731,55 +811,85 @@ module internal Z3 = (key, Some term, typ)) Memory.NewStackFrame state None (List.ofSeq frame) - let defaultValues = Dictionary() - encodingCache.regionConstants |> Seq.iter (fun kvp -> - let region, fields = kvp.Key + let processRegionConstraints isSymbolic (kvp : KeyValuePair<(regionSort * fieldId list), ArrayExpr>) = let constant = kvp.Value let arr = m.Eval(constant, false) + let region, fields = kvp.Key let typeOfLocation = if fields.IsEmpty then region.TypeOfLocation else fields.Head.typ - let rec parseArray (arr : Expr) = - if arr.IsConstantArray then + + let getValueAndWrite (arr : Expr) cmAllocate addr = + let value = + if Types.IsValueType typeOfLocation then + x.Decode state typeOfLocation cmAllocate (Array.last arr.Args) + else + let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress state typeOfLocation cmAllocate + HeapRef (address |> ConcreteHeapAddress) typeOfLocation + match addr with + | ClassField({term = HeapRef({term = ConcreteHeapAddress(base_addr)}, _)}, _) + | ArrayIndex({term = HeapRef({term = ConcreteHeapAddress(base_addr)}, _)}, _, _) -> + match value with + | {term = HeapRef({term = ConcreteHeapAddress(a)}, _)} when not <| cm.Contains a -> + // Concrete memory objects cannot address symbolic objects + if cm.Contains base_addr then Memory.Unmarshall state base_addr + | _ -> () + | _ -> () + let states = Memory.Write state (Ref addr) value + assert(states.Length = 1 && states.[0] = state) + + let writeHelper symbolicProcessor mixedProcessor addr = + // Strings and array metadata are written symbolically + match addr with + | _ when typeOfLocation = typeof -> symbolicProcessor addr + | ArrayLength _ + | ArrayLowerBound _ -> symbolicProcessor addr + | _ -> mixedProcessor addr // may contain symbolic and concrete writes + + let writeSymbolic arr = writeHelper (getValueAndWrite arr false) (fun _ -> ()) + let writeMixed arr = writeHelper (fun _ -> ()) (getValueAndWrite arr true) + + let rec parseArray (arr : Expr) = + if arr.IsConstantArray && isSymbolic then // defaults are written symbolically assert(arr.Args.Length = 1) let constantValue = - if Types.IsValueType typeOfLocation then x.Decode typeOfLocation arr.Args.[0] + if Types.IsValueType typeOfLocation then x.Decode state typeOfLocation false arr.Args.[0] else - let addr = x.DecodeConcreteHeapAddress typeOfLocation arr.Args.[0] |> ConcreteHeapAddress - HeapRef addr typeOfLocation + let addr = x.DecodeConcreteHeapAddress state typeOfLocation false arr.Args.[0] + HeapRef (addr |> ConcreteHeapAddress) typeOfLocation x.WriteDictOfValueTypes defaultValues region fields region.TypeOfLocation constantValue - elif arr.IsDefaultArray then - assert(arr.Args.Length = 1) - elif arr.IsStore then + else if arr.IsStore then assert(arr.Args.Length >= 3) parseArray arr.Args.[0] - let address = x.DecodeMemoryKey region arr.Args.[1..arr.Args.Length - 2] - let value = - if Types.IsValueType typeOfLocation then - x.Decode typeOfLocation (Array.last arr.Args) - else - let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress typeOfLocation |> ConcreteHeapAddress - HeapRef address typeOfLocation - let address = fields |> List.fold (fun address field -> StructField(address, field)) address - let states = Memory.Write state (Ref address) value - assert(states.Length = 1 && states.[0] = state) - elif arr.IsConst then () + let addr = x.DecodeMemoryKey state region (not isSymbolic) arr.Args.[1..arr.Args.Length - 2] + if isSymbolic + then writeSymbolic arr addr + else writeMixed arr addr + elif arr.IsConst || arr.IsConstantArray then () else internalfailf "Unexpected array expression in model: %O" arr - parseArray arr) + parseArray arr + + // Process symbolic writes + encodingCache.regionConstants |> Seq.iter (processRegionConstraints true) defaultValues |> Seq.iter (fun kvp -> let region = kvp.Key let constantValue = kvp.Value.Value Memory.FillRegion state constantValue region) + // Create default concretes encodingCache.heapAddresses |> Seq.iter (fun kvp -> let typ, _ = kvp.Key let addr = kvp.Value - if VectorTime.less addr VectorTime.zero && not <| PersistentDict.contains addr state.allocatedTypes then - state.allocatedTypes <- PersistentDict.add addr (ConcreteType typ) state.allocatedTypes) - state.startingTime <- [encodingCache.lastSymbolicAddress - 1] + concreteAllocator state defaultValues typ addr + ) - encodingCache.heapAddresses.Clear() + // Process stores + encodingCache.regionConstants |> Seq.iter (processRegionConstraints false) + + state.startingTime <- [encodingCache.lastSymbolicAddress - 1] state.model <- PrimitiveModel subst + encodingCache.heapAddresses.Clear() + defaultValues.Clear() StateModel(state, typeModel.CreateEmpty()) diff --git a/VSharp.TestRenderer/CodeRenderer.cs b/VSharp.TestRenderer/CodeRenderer.cs index 45d2f2c6c..41ed1eb21 100644 --- a/VSharp.TestRenderer/CodeRenderer.cs +++ b/VSharp.TestRenderer/CodeRenderer.cs @@ -478,12 +478,7 @@ public static ExpressionSyntax RenderArrayCreation( ); ExpressionSyntax array; - if (allowImplicit && initializer != null) - // TODO: update for multidimensional arrays (use .WithCommas) - array = ImplicitArrayCreationExpression(initializer); - else - array = ArrayCreationExpression(Token(SyntaxKind.NewKeyword), type, initializer); - + array = ArrayCreationExpression(Token(SyntaxKind.NewKeyword), type, initializer); return array; } diff --git a/VSharp.TestRenderer/MethodRenderer.cs b/VSharp.TestRenderer/MethodRenderer.cs index 6bed5172d..ca865f138 100644 --- a/VSharp.TestRenderer/MethodRenderer.cs +++ b/VSharp.TestRenderer/MethodRenderer.cs @@ -354,7 +354,9 @@ private ExpressionSyntax RenderArray(ArrayTypeSyntax type, System.Array obj, str } var allowImplicit = elemType is { IsValueType: true } && rank == 1; - return RenderArrayCreation(type, initializer, allowImplicit); + var arr = RenderArrayCreation(type, initializer, allowImplicit); + var arrayId = AddDecl(preferredName, type, arr); + return arrayId; } private ExpressionSyntax RenderArray(System.Array obj, string? preferredName) diff --git a/VSharp.Utils/MemoryGraph.fs b/VSharp.Utils/MemoryGraph.fs index 691d4e1c8..a2a7051c0 100644 --- a/VSharp.Utils/MemoryGraph.fs +++ b/VSharp.Utils/MemoryGraph.fs @@ -204,13 +204,14 @@ and MemoryGraph(repr : memoryRepr, mocker : ITypeMockSerializer, createCompactRe member private x.IsSerializable (t : Type) = // TODO: find out which types can be serialized by XMLSerializer - (t.IsPrimitive && not t.IsEnum) || t = typeof || (t.IsArray && (x.IsSerializable <| t.GetElementType())) + (t.IsPrimitive && not t.IsEnum) || t = typeof member private x.EncodeArray (arr : Array) = let contents = seq { for elem in arr do - yield x.Encode elem + let res, _ = x.Encode elem + yield res } |> Array.ofSeq let lowerBounds = if arr.Rank = 1 && arr.GetLowerBound 0 = 0 then null @@ -232,7 +233,7 @@ and MemoryGraph(repr : memoryRepr, mocker : ITypeMockSerializer, createCompactRe member private x.EncodeStructure (obj : obj) = let t = obj.GetType() - let fields = t |> Reflection.fieldsOf false |> Seq.map (fun (_, field) -> field.GetValue(obj) |> x.Encode) |> Array.ofSeq + let fields = t |> Reflection.fieldsOf false |> Seq.map (fun (_, field) -> field.GetValue(obj) |> x.Encode |> fst) |> Array.ofSeq let repr : structureRepr = {typ = x.RegisterType t; fields = fields} repr :> obj @@ -241,48 +242,57 @@ and MemoryGraph(repr : memoryRepr, mocker : ITypeMockSerializer, createCompactRe let repr : enumRepr = {typ = x.RegisterType t; underlyingValue = Convert.ChangeType(obj, Enum.GetUnderlyingType t)} repr :> obj - member private x.Bind (obj : obj) (repr : obj) = - sourceObjects.Add obj - objReprs.Add repr - assert(sourceObjects.Count = objReprs.Count) - sourceObjects.Count - 1 + member private x.Bind (obj : obj) (repr : obj) (idx : int option) = + match idx with + | Some i -> + sourceObjects.[i] <- obj + objReprs.[i] <- repr + i + | None -> + sourceObjects.Add obj + objReprs.Add repr + assert(sourceObjects.Count = objReprs.Count) + sourceObjects.Count - 1 - member x.Encode (obj : obj) : obj = + member x.Encode (obj : obj) = match obj with - | null -> null - | :? referenceRepr -> obj - | :? structureRepr -> obj - | :? arrayRepr -> obj - | :? pointerRepr -> obj - | :? enumRepr -> obj - | _ when mocker.IsMockObject obj -> mocker.Serialize obj + | null -> null, None + | :? referenceRepr -> obj, None + | :? structureRepr -> obj, None + | :? arrayRepr -> obj, None + | :? pointerRepr -> obj, None + | :? enumRepr -> obj, None + | _ when mocker.IsMockObject obj -> mocker.Serialize obj, None | _ -> // TODO: delegates? let t = obj.GetType() - if x.IsSerializable t then obj + if x.IsSerializable t then obj, None else match t with | _ when t.IsValueType -> - if t.IsEnum then x.RepresentEnum obj - else x.EncodeStructure obj + if t.IsEnum then x.RepresentEnum obj, None + else x.EncodeStructure obj, None | _ -> let idx = match Seq.tryFindIndex (fun obj' -> Object.ReferenceEquals(obj, obj')) sourceObjects with | Some idx -> idx | None -> + let i = x.ReserveRepresentation() + let r : referenceRepr = {index = i} + x.Bind obj r (Some i) |> ignore let repr = match t with | _ when t.IsArray -> x.EncodeArray (obj :?> Array) | _ -> x.EncodeStructure obj - x.Bind obj repr + x.Bind obj repr (Some i) let reference : referenceRepr = {index = idx} - reference :> obj + reference :> obj, Some idx member x.RepresentStruct (typ : Type) (fields : obj array) = let repr : structureRepr = {typ = x.RegisterType typ; fields = fields} repr :> obj - member x.ReserveRepresentation() = x.Bind null null + member x.ReserveRepresentation() = x.Bind null null None member x.AddClass (typ : Type) (fields : obj array) index = let repr : structureRepr = {typ = x.RegisterType typ; fields = fields} diff --git a/VSharp.Utils/UnitTest.fs b/VSharp.Utils/UnitTest.fs index bb9c7e3b0..48e85abba 100644 --- a/VSharp.Utils/UnitTest.fs +++ b/VSharp.Utils/UnitTest.fs @@ -78,7 +78,7 @@ type UnitTest private (m : MethodBase, info : testInfo, createCompactRepr : bool and set this = let t = typeof let p = t.GetProperty("thisArg") - p.SetValue(info, memoryGraph.Encode this) + p.SetValue(info, memoryGraph.Encode this |> fst) member x.Args with get() = args member x.IsError @@ -128,7 +128,7 @@ type UnitTest private (m : MethodBase, info : testInfo, createCompactRepr : bool let mp = t.GetProperty("mockClassTypeParameters") mp.SetValue(info, mockedParameters |> Array.map (fun m -> match m with - | Some m -> m.Serialize memoryGraph.Encode + | Some m -> m.Serialize (memoryGraph.Encode >> fst) | None -> typeMockRepr.NullRepr)) // @concreteParameters and @mockedParameters should have equal lengths and be complementary: @@ -140,7 +140,7 @@ type UnitTest private (m : MethodBase, info : testInfo, createCompactRepr : bool let mp = t.GetProperty("mockMethodTypeParameters") mp.SetValue(info, mockedParameters |> Array.map (fun m -> match m with - | Some m -> m.Serialize memoryGraph.Encode + | Some m -> m.Serialize (memoryGraph.Encode >> fst) | None -> typeMockRepr.NullRepr)) member x.MemoryGraph with get() = memoryGraph @@ -152,7 +152,7 @@ type UnitTest private (m : MethodBase, info : testInfo, createCompactRepr : bool let t = typeof let p = t.GetProperty("args") p.SetValue(info, Array.zeroCreate <| m.GetParameters().Length) - let value = memoryGraph.Encode value + let value = memoryGraph.Encode value |> fst info.args.[arg.Position] <- value member x.AddExtraAssemblySearchPath path = @@ -165,7 +165,7 @@ type UnitTest private (m : MethodBase, info : testInfo, createCompactRepr : bool let extraAssempliesProperty = t.GetProperty("extraAssemblyLoadDirs") extraAssempliesProperty.SetValue(info, Array.ofList extraAssemblyLoadDirs) let typeMocksProperty = t.GetProperty("typeMocks") - typeMocksProperty.SetValue(info, typeMocks.ToArray() |> Array.map (fun m -> m.Serialize memoryGraph.Encode)) + typeMocksProperty.SetValue(info, typeMocks.ToArray() |> Array.map (fun m -> m.Serialize (memoryGraph.Encode >> fst))) let serializer = XmlSerializer t use stream = File.Create(destination) serializer.Serialize(stream, info)