From 87f69026160faad79e81183f4a3a71e85a189fc6 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Thu, 3 Nov 2022 12:49:58 +0300 Subject: [PATCH 01/25] concrete allocation --- VSharp.SILI.Core/Memory.fs | 1 + VSharp.SILI.Core/TypeSolver.fs | 14 ++++- VSharp.SILI/TestGenerator.fs | 14 +++-- VSharp.Solver/Z3.fs | 100 ++++++++++++++++++++------------- 4 files changed, 83 insertions(+), 46 deletions(-) diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index 49d4e860c..88a7300f0 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 diff --git a/VSharp.SILI.Core/TypeSolver.fs b/VSharp.SILI.Core/TypeSolver.fs index f2d759a24..88964030d 100644 --- a/VSharp.SILI.Core/TypeSolver.fs +++ b/VSharp.SILI.Core/TypeSolver.fs @@ -331,13 +331,21 @@ 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 | _ -> () Seq.iter2 refineTypes addresses refsTypes let classParams, methodParams = Array.splitAt typeGenericArguments.Length typeParams diff --git a/VSharp.SILI/TestGenerator.fs b/VSharp.SILI/TestGenerator.fs index 9ceb0ed59..2f361b0f4 100644 --- a/VSharp.SILI/TestGenerator.fs +++ b/VSharp.SILI/TestGenerator.fs @@ -122,11 +122,15 @@ 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 -> o |> unbox + | None -> // mocks and big arrays are allocated symbolically + __unreachable__() + // 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 = diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 04845e5c1..ee0626644 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -563,12 +563,12 @@ module internal Z3 = // ------------------------------- Decoding ------------------------------- - member private x.DecodeExpr op t (expr : Expr) = + member private x.DecodeExpr (cm : IConcreteMemory) op t (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 cm t) |> List.ofSeq) t - member private x.DecodeBoolExpr op (expr : Expr) = - x.DecodeExpr op typeof expr + member private x.DecodeBoolExpr (cm : IConcreteMemory) op (expr : Expr) = + x.DecodeExpr cm op typeof expr member private x.GetTypeOfBV (bv : BitVecExpr) = if bv.SortSize = 32u then typeof @@ -577,7 +577,7 @@ module internal Z3 = elif bv.SortSize = 16u then typeof else __unreachable__() - member private x.DecodeConcreteHeapAddress typ (expr : Expr) : vectorTime = + member private x.DecodeConcreteHeapAddress (cm : IConcreteMemory) typ (expr : Expr) : vectorTime = // TODO: maybe throw away typ? let result = ref vectorTime.Empty let checkAndGet key = encodingCache.heapAddresses.TryGetValue(key, result) @@ -588,12 +588,20 @@ 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 cm.Remove 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) + try + let o = Reflection.createObject typ + cm.Allocate addr o + with + | _ -> () // if type cannot be allocated concretely, it will be stored symbolically + addr member private x.DecodeSymbolicTypeAddress (expr : Expr) = @@ -601,14 +609,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 (cm : IConcreteMemory) (reg : regionSort) (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 cm field.declaringType |> ConcreteHeapAddress ClassField(address, field) | StaticFieldSort field -> assert(exprs.Length = 1) @@ -616,22 +624,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 cm (toType typ) |> ConcreteHeapAddress + let indices = exprs |> Seq.tail |> Seq.map (x.Decode cm Types.IndexType) |> 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 cm (toType typ) |> ConcreteHeapAddress + let index = x.Decode cm Types.IndexType 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 cm (toType typ) |> ConcreteHeapAddress + let index = x.Decode cm Types.IndexType exprs.[1] ArrayLowerBound(heapAddress, index, typ) | StackBufferSort key -> assert(exprs.Length = 1) - let index = x.Decode typeof exprs.[0] + let index = x.Decode cm typeof exprs.[0] StackBufferIndex(key, index) member private x.DecodeBv t (bv : BitVecNum) = @@ -642,11 +650,11 @@ module internal Z3 = | 8u -> Concrete (convert bv.Int t) t | _ -> __notImplemented__() - member public x.Decode t (expr : Expr) = + member public x.Decode (cm: IConcreteMemory) t (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 cm t bv |> ConcreteHeapAddress HeapRef address t | :? BitVecExpr as bv when bv.IsConst -> if encodingCache.e2t.ContainsKey(expr) then encodingCache.e2t.[expr] @@ -657,18 +665,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 cm OperationType.LogicalNot expr + elif expr.IsAnd then x.DecodeBoolExpr cm OperationType.LogicalAnd expr + elif expr.IsOr then x.DecodeBoolExpr cm OperationType.LogicalOr expr + elif expr.IsEq then x.DecodeBoolExpr cm OperationType.Equal expr + elif expr.IsBVSGT then x.DecodeBoolExpr cm OperationType.Greater expr + elif expr.IsBVUGT then x.DecodeBoolExpr cm OperationType.Greater_Un expr + elif expr.IsBVSGE then x.DecodeBoolExpr cm OperationType.GreaterOrEqual expr + elif expr.IsBVUGE then x.DecodeBoolExpr cm OperationType.GreaterOrEqual_Un expr + elif expr.IsBVSLT then x.DecodeBoolExpr cm OperationType.Less expr + elif expr.IsBVULT then x.DecodeBoolExpr cm OperationType.Less_Un expr + elif expr.IsBVSLE then x.DecodeBoolExpr cm OperationType.LessOrEqual expr + elif expr.IsBVULE then x.DecodeBoolExpr cm OperationType.LessOrEqual_Un expr else __notImplemented__() member private x.WriteFields structure value = function @@ -695,11 +703,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 cm t refinedExpr if decoded <> constant then x.WriteDictOfValueTypes stackEntries key fields key.TypeOfLocation decoded | {term = Constant(_, (:? IMemoryAccessConstantSource as ms), _)} as constant -> @@ -707,19 +716,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 cm t |> 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 cm t 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 cm t refinedExpr assert(not (constant = term) || kvp.Value.expr = refinedExpr) if constant <> term then subst.Add(source, term) | _ -> ()) @@ -743,9 +752,9 @@ module internal Z3 = if arr.IsConstantArray then 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 cm typeOfLocation arr.Args.[0] else - let addr = x.DecodeConcreteHeapAddress typeOfLocation arr.Args.[0] |> ConcreteHeapAddress + let addr = x.DecodeConcreteHeapAddress cm typeOfLocation arr.Args.[0] |> ConcreteHeapAddress HeapRef addr typeOfLocation x.WriteDictOfValueTypes defaultValues region fields region.TypeOfLocation constantValue elif arr.IsDefaultArray then @@ -753,12 +762,12 @@ module internal Z3 = elif 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 address = x.DecodeMemoryKey cm region arr.Args.[1..arr.Args.Length - 2] let value = if Types.IsValueType typeOfLocation then - x.Decode typeOfLocation (Array.last arr.Args) + x.Decode cm typeOfLocation (Array.last arr.Args) else - let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress typeOfLocation |> ConcreteHeapAddress + let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress cm 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 @@ -771,11 +780,26 @@ module internal Z3 = let constantValue = kvp.Value.Value Memory.FillRegion state constantValue region) + state.startingTime <- [encodingCache.lastSymbolicAddress - 1] + state.model <- PrimitiveModel subst + let sm = StateModel state + encodingCache.heapAddresses |> Seq.iter (fun kvp -> + let unboxConcrete term = + match sm.Complete term with + | {term = Concrete(v, _)} -> v |> unbox + | _ -> __unreachable__() let typ, _ = kvp.Key let addr = kvp.Value + let cha = ConcreteHeapAddress addr if VectorTime.less addr VectorTime.zero && not <| PersistentDict.contains addr state.allocatedTypes then - state.allocatedTypes <- PersistentDict.add addr (ConcreteType typ) state.allocatedTypes) + state.allocatedTypes <- PersistentDict.add addr (ConcreteType typ) state.allocatedTypes + if typ = typeof then + let length : int = ClassField(cha, Reflection.stringLengthField) |> Ref |> Memory.Read state |> unboxConcrete + let contents : char array = Array.init length (fun i -> ArrayIndex(cha, [MakeNumber i], (typeof, 1, true)) + |> Ref |> Memory.Read state |> unboxConcrete) + cm.Allocate addr (String(contents) :> obj) + ) state.startingTime <- [encodingCache.lastSymbolicAddress - 1] encodingCache.heapAddresses.Clear() From ac02a15d7c78651bb129cd8d446ecafe0519dec4 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Thu, 3 Nov 2022 15:14:58 +0300 Subject: [PATCH 02/25] array concrete allocation --- VSharp.SILI/TestGenerator.fs | 2 +- VSharp.Solver/Z3.fs | 129 ++++++++++++++++++++++++++++------- 2 files changed, 106 insertions(+), 25 deletions(-) diff --git a/VSharp.SILI/TestGenerator.fs b/VSharp.SILI/TestGenerator.fs index 2f361b0f4..0831b914b 100644 --- a/VSharp.SILI/TestGenerator.fs +++ b/VSharp.SILI/TestGenerator.fs @@ -123,7 +123,7 @@ module TestGenerator = match model with | StateModel(modelState, _) -> match modelState.concreteMemory.TryVirtToPhys addr with - | Some o -> o |> unbox + | Some o -> o | None -> // mocks and big arrays are allocated symbolically __unreachable__() // let eval address = diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index ee0626644..9c09b612f 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -596,12 +596,6 @@ module internal Z3 = encodingCache.lastSymbolicAddress <- encodingCache.lastSymbolicAddress - 1 let addr = [encodingCache.lastSymbolicAddress] encodingCache.heapAddresses.Add((typ, expr), addr) - try - let o = Reflection.createObject typ - cm.Allocate addr o - with - | _ -> () // if type cannot be allocated concretely, it will be stored symbolically - addr member private x.DecodeSymbolicTypeAddress (expr : Expr) = @@ -740,24 +734,123 @@ module internal Z3 = (key, Some term, typ)) Memory.NewStackFrame state None (List.ofSeq frame) + // gather default values and array metadata let defaultValues = Dictionary() encodingCache.regionConstants |> Seq.iter (fun kvp -> - let region, fields = kvp.Key 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) = + let rec parseArray (arr : Expr) = if arr.IsConstantArray then assert(arr.Args.Length = 1) let constantValue = if Types.IsValueType typeOfLocation then x.Decode cm typeOfLocation arr.Args.[0] else - let addr = x.DecodeConcreteHeapAddress cm typeOfLocation arr.Args.[0] |> ConcreteHeapAddress - HeapRef addr typeOfLocation + let addr = x.DecodeConcreteHeapAddress cm typeOfLocation arr.Args.[0] + // TODO: maybe we need to add cm allocate here? + HeapRef (addr |> ConcreteHeapAddress) typeOfLocation x.WriteDictOfValueTypes defaultValues region fields region.TypeOfLocation constantValue - elif arr.IsDefaultArray then + else if arr.IsStore then + assert(arr.Args.Length >= 3) + parseArray arr.Args.[0] + let addr = x.DecodeMemoryKey cm region arr.Args.[1..arr.Args.Length - 2] + match addr with + | ArrayLength _ + | ArrayLowerBound _ -> + let value = + if Types.IsValueType typeOfLocation then + x.Decode cm typeOfLocation (Array.last arr.Args) + else + let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress cm typeOfLocation |> ConcreteHeapAddress + HeapRef address typeOfLocation + let states = Memory.Write state (Ref addr) value + assert(states.Length = 1 && states.[0] = state) + | _ -> () + else + () + parseArray arr + ) + // fill symbolic memory with defaults + defaultValues |> Seq.iter (fun kvp -> + let region = kvp.Key + let constantValue = kvp.Value.Value + Memory.FillRegion state constantValue region) + + state.startingTime <- [encodingCache.lastSymbolicAddress - 1] + state.model <- PrimitiveModel subst + let sm = StateModel state + // TODO : move to utils ? + let unboxConcrete term = + match sm.Complete term with + | {term = Concrete(v, _)} -> v |> unbox + | _ -> __unreachable__() + + // Create default concretes + encodingCache.heapAddresses |> Seq.iter (fun kvp -> + let typ, _ = kvp.Key + let addr = kvp.Value + let cha = addr |> ConcreteHeapAddress + if VectorTime.lessOrEqual VectorTime.zero addr || typ = typeof then () + else + match typ with + | ArrayType(elemType, dim) -> + let eval address = + address |> Ref |> Memory.Read state |> unboxConcrete + 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 -> __notImplemented__() + let length = Array.reduce ( * ) lengths + if length > 128 then () // TODO: move magic number + else + + let arr = + if (lowerBounds <> null) + then Array.CreateInstance(elemType, lengths, lowerBounds) + else Array.CreateInstance(elemType, lengths) + // TODO: fill with defaults + // let defVal = ref (defaultOf elemType) + // defaultValues.TryGetValue(ArrayIndexSort arrayType, defVal) |> ignore + // let defVal = defVal |> unboxConcrete + // Array.Fill(arr, defVal.Value) + cm.Allocate addr arr + | _ -> + if VectorTime.less addr VectorTime.zero && not <| cm.Contains addr && typ <> typeof then + let fields = Reflection.fieldsOf false typ |> Seq.map fst + try + let o = Reflection.createObject typ + cm.Allocate addr o + defaultValues |> Seq.iter (fun kv -> + match kv.Key with + | HeapFieldSort fId when (Seq.contains fId fields) -> + let a = ClassField(cha, fId) + let states = Memory.Write state (Ref a) kv.Value.Value + assert(states.Length = 1 && states.[0] = state) + | _ -> ()) + with + | _ -> () // if type cannot be allocated concretely, it will be stored symbolically + ) + + // Process stores + encodingCache.regionConstants |> Seq.iter (fun kvp -> + let region, fields = kvp.Key + let constant = kvp.Value + let arr = m.Eval(constant, false) + let typeOfLocation = + if fields.IsEmpty then region.TypeOfLocation + else fields.Head.typ + let rec parseArray (arr : Expr) = + if arr.IsDefaultArray then assert(arr.Args.Length = 1) elif arr.IsStore then assert(arr.Args.Length >= 3) @@ -772,23 +865,11 @@ module internal Z3 = 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 () + elif arr.IsConst || arr.IsConstantArray then () else internalfailf "Unexpected array expression in model: %O" arr parseArray arr) - defaultValues |> Seq.iter (fun kvp -> - let region = kvp.Key - let constantValue = kvp.Value.Value - Memory.FillRegion state constantValue region) - - state.startingTime <- [encodingCache.lastSymbolicAddress - 1] - state.model <- PrimitiveModel subst - let sm = StateModel state encodingCache.heapAddresses |> Seq.iter (fun kvp -> - let unboxConcrete term = - match sm.Complete term with - | {term = Concrete(v, _)} -> v |> unbox - | _ -> __unreachable__() let typ, _ = kvp.Key let addr = kvp.Value let cha = ConcreteHeapAddress addr From f7cbb4a35e8faf663fd0f7a2bfa1a8b6f0adee04 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Thu, 3 Nov 2022 18:06:09 +0300 Subject: [PATCH 03/25] some fixes --- VSharp.SILI.Core/Memory.fs | 10 ++++++++++ VSharp.SILI/TestGenerator.fs | 15 ++++++++------- VSharp.Solver/Z3.fs | 3 ++- 3 files changed, 20 insertions(+), 8 deletions(-) diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index 88a7300f0..ff1f9fc5e 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -377,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 diff --git a/VSharp.SILI/TestGenerator.fs b/VSharp.SILI/TestGenerator.fs index 0831b914b..615ef572d 100644 --- a/VSharp.SILI/TestGenerator.fs +++ b/VSharp.SILI/TestGenerator.fs @@ -123,14 +123,15 @@ module TestGenerator = match model with | StateModel(modelState, _) -> match modelState.concreteMemory.TryVirtToPhys addr with - | Some o -> o + | Some o -> + test.MemoryGraph.Encode o | None -> // mocks and big arrays are allocated symbolically - __unreachable__() - // 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 + // __unreachable__() + 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 = diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 9c09b612f..77578b4c5 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -796,6 +796,7 @@ module internal Z3 = if VectorTime.lessOrEqual VectorTime.zero addr || typ = typeof then () else match typ with + | ArrayType(_, SymbolicDimension _) -> () | ArrayType(elemType, dim) -> let eval address = address |> Ref |> Memory.Read state |> unboxConcrete @@ -809,7 +810,7 @@ module internal Z3 = arrayType, Array.init rank (fun i -> ArrayLength(cha, MakeNumber i, arrayType) |> eval), Array.init rank (fun i -> ArrayLowerBound(cha, MakeNumber i, arrayType) |> eval) - | SymbolicDimension -> __notImplemented__() + | SymbolicDimension -> __unreachable__() let length = Array.reduce ( * ) lengths if length > 128 then () // TODO: move magic number else From 37e8c267c354f4a0bad8b9700c4ccec67d9b738e Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Sat, 5 Nov 2022 19:14:17 +0300 Subject: [PATCH 04/25] tmp --- VSharp.Solver/Z3.fs | 59 ++++++++++++++++++++++----------------------- 1 file changed, 29 insertions(+), 30 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 77578b4c5..9b1cb3bea 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -779,12 +779,11 @@ module internal Z3 = let constantValue = kvp.Value.Value Memory.FillRegion state constantValue region) - state.startingTime <- [encodingCache.lastSymbolicAddress - 1] - state.model <- PrimitiveModel subst - let sm = StateModel state + // state.model <- PrimitiveModel subst + // TODO : move to utils ? let unboxConcrete term = - match sm.Complete term with + match term with | {term = Concrete(v, _)} -> v |> unbox | _ -> __unreachable__() @@ -797,34 +796,34 @@ module internal Z3 = else match typ with | ArrayType(_, SymbolicDimension _) -> () - | ArrayType(elemType, dim) -> - let eval address = - address |> Ref |> Memory.Read state |> unboxConcrete - 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__() - let length = Array.reduce ( * ) lengths - if length > 128 then () // TODO: move magic number - else - - let arr = - if (lowerBounds <> null) - then Array.CreateInstance(elemType, lengths, lowerBounds) - else Array.CreateInstance(elemType, lengths) + | ArrayType(elemType, dim) -> () + // let eval address = + // address |> Ref |> Memory.Read state |> unboxConcrete + // 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__() + // let length = Array.reduce ( * ) lengths + // if length > 128 then () // TODO: move magic number + // else + // + // let arr = + // if (lowerBounds <> null) + // then Array.CreateInstance(elemType, lengths, lowerBounds) + // else Array.CreateInstance(elemType, lengths) // TODO: fill with defaults // let defVal = ref (defaultOf elemType) // defaultValues.TryGetValue(ArrayIndexSort arrayType, defVal) |> ignore // let defVal = defVal |> unboxConcrete // Array.Fill(arr, defVal.Value) - cm.Allocate addr arr + // cm.Allocate addr arr | _ -> if VectorTime.less addr VectorTime.zero && not <| cm.Contains addr && typ <> typeof then let fields = Reflection.fieldsOf false typ |> Seq.map fst @@ -877,15 +876,15 @@ module internal Z3 = if VectorTime.less addr VectorTime.zero && not <| PersistentDict.contains addr state.allocatedTypes then state.allocatedTypes <- PersistentDict.add addr (ConcreteType typ) state.allocatedTypes if typ = typeof then - let length : int = ClassField(cha, Reflection.stringLengthField) |> Ref |> Memory.Read state |> unboxConcrete + let length : int = ClassField(cha, Reflection.stringLengthField) |> Ref |> Memory.Read state |> unboxConcrete let contents : char array = Array.init length (fun i -> ArrayIndex(cha, [MakeNumber i], (typeof, 1, true)) |> Ref |> Memory.Read state |> unboxConcrete) cm.Allocate addr (String(contents) :> obj) ) - state.startingTime <- [encodingCache.lastSymbolicAddress - 1] - encodingCache.heapAddresses.Clear() + state.startingTime <- [encodingCache.lastSymbolicAddress - 1] state.model <- PrimitiveModel subst + encodingCache.heapAddresses.Clear() StateModel(state, typeModel.CreateEmpty()) From 6d88174eb36c68237d06182e8bd0da7871506753 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Sun, 6 Nov 2022 01:18:32 +0300 Subject: [PATCH 05/25] stupid array fillment with default values --- VSharp.Solver/Z3.fs | 95 ++++++++++++++++++++++++--------------------- 1 file changed, 51 insertions(+), 44 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 9b1cb3bea..7a2ad7564 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -778,8 +778,6 @@ module internal Z3 = let region = kvp.Key let constantValue = kvp.Value.Value Memory.FillRegion state constantValue region) - - // state.model <- PrimitiveModel subst // TODO : move to utils ? let unboxConcrete term = @@ -796,49 +794,58 @@ module internal Z3 = else match typ with | ArrayType(_, SymbolicDimension _) -> () - | ArrayType(elemType, dim) -> () - // let eval address = - // address |> Ref |> Memory.Read state |> unboxConcrete - // 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__() - // let length = Array.reduce ( * ) lengths - // if length > 128 then () // TODO: move magic number - // else - // - // let arr = - // if (lowerBounds <> null) - // then Array.CreateInstance(elemType, lengths, lowerBounds) - // else Array.CreateInstance(elemType, lengths) + | ArrayType(elemType, dim) -> + let eval address = + address |> Ref |> Memory.Read state |> unboxConcrete + 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__() + let length = Array.reduce ( * ) lengths + if length > 128 then () // TODO: move magic number + else + + let arr = + if (lowerBounds <> null) + then Array.CreateInstance(elemType, lengths, lowerBounds) + else Array.CreateInstance(elemType, lengths) // TODO: fill with defaults - // let defVal = ref (defaultOf elemType) - // defaultValues.TryGetValue(ArrayIndexSort arrayType, defVal) |> ignore - // let defVal = defVal |> unboxConcrete - // Array.Fill(arr, defVal.Value) - // cm.Allocate addr arr - | _ -> - if VectorTime.less addr VectorTime.zero && not <| cm.Contains addr && typ <> typeof then - let fields = Reflection.fieldsOf false typ |> Seq.map fst - try - let o = Reflection.createObject typ - cm.Allocate addr o - defaultValues |> Seq.iter (fun kv -> - match kv.Key with - | HeapFieldSort fId when (Seq.contains fId fields) -> - let a = ClassField(cha, fId) - let states = Memory.Write state (Ref a) kv.Value.Value - assert(states.Length = 1 && states.[0] = state) - | _ -> ()) - with - | _ -> () // if type cannot be allocated concretely, it will be stored symbolically + cm.Allocate addr arr + let result = ref (ref Nop) // TODO: do we need the else branch here? + if defaultValues.TryGetValue(ArrayIndexSort arrayType, result) then + // TODO: rewrite + let product xss = + let rec product xss k = + match xss with + | [] -> k [[]] + | xs::xss -> product xss (fun yss -> List.collect (fun ys -> List.map (fun x -> x :: ys) xs) yss |> k) + product xss id + let indexes = Seq.map (fun l -> List.init l id) lengths |> List.ofSeq + let indexes = product indexes + let value = result.Value.Value |> unboxConcrete + List.iter (fun i -> cm.WriteArrayIndex addr i value) indexes + | _ -> () + // if VectorTime.less addr VectorTime.zero && not <| cm.Contains addr && typ <> typeof then + // let fields = Reflection.fieldsOf false typ |> Seq.map fst + // try + // let o = Reflection.createObject typ + // cm.Allocate addr o + // defaultValues |> Seq.iter (fun kv -> + // match kv.Key with + // | HeapFieldSort fId when (Seq.contains fId fields) -> + // let a = ClassField(cha, fId) + // let states = Memory.Write state (Ref a) kv.Value.Value + // assert(states.Length = 1 && states.[0] = state) + // | _ -> ()) + // with + // | _ -> () // if type cannot be allocated concretely, it will be stored symbolically ) // Process stores From 77e598f9d5365573829e3bf043f39446a53e58f8 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Sun, 6 Nov 2022 15:12:24 +0300 Subject: [PATCH 06/25] defaults for classes --- VSharp.Solver/Z3.fs | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 7a2ad7564..449e3e18d 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -831,21 +831,21 @@ module internal Z3 = let indexes = product indexes let value = result.Value.Value |> unboxConcrete List.iter (fun i -> cm.WriteArrayIndex addr i value) indexes - | _ -> () - // if VectorTime.less addr VectorTime.zero && not <| cm.Contains addr && typ <> typeof then - // let fields = Reflection.fieldsOf false typ |> Seq.map fst - // try - // let o = Reflection.createObject typ - // cm.Allocate addr o - // defaultValues |> Seq.iter (fun kv -> - // match kv.Key with - // | HeapFieldSort fId when (Seq.contains fId fields) -> - // let a = ClassField(cha, fId) - // let states = Memory.Write state (Ref a) kv.Value.Value - // assert(states.Length = 1 && states.[0] = state) - // | _ -> ()) - // with - // | _ -> () // if type cannot be allocated concretely, it will be stored symbolically + | _ -> + if VectorTime.less addr VectorTime.zero && not <| cm.Contains addr && typ <> typeof then + let fields = Reflection.fieldsOf false typ |> Seq.map fst + + try + let o = Reflection.createObject typ + cm.Allocate addr o + fields |> Seq.iter (fun fId -> + let region = HeapFieldSort fId + let result = ref (ref Nop) + if defaultValues.TryGetValue(region, result) then + cm.WriteClassField addr fId result.Value.Value + ) + with + | _ -> () // if type cannot be allocated concretely, it will be stored symbolically ) // Process stores From b68486ca9e17185a5014c3bec50353cd88b64f44 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Tue, 8 Nov 2022 19:55:10 +0300 Subject: [PATCH 07/25] tmp commit for objects creatipn in model --- VSharp.SILI/TestGenerator.fs | 12 ++++- VSharp.Solver/Z3.fs | 91 ++++++++++++++++++------------------ 2 files changed, 56 insertions(+), 47 deletions(-) diff --git a/VSharp.SILI/TestGenerator.fs b/VSharp.SILI/TestGenerator.fs index 615ef572d..7bc11fcb1 100644 --- a/VSharp.SILI/TestGenerator.fs +++ b/VSharp.SILI/TestGenerator.fs @@ -124,7 +124,14 @@ module TestGenerator = | StateModel(modelState, _) -> match modelState.concreteMemory.TryVirtToPhys addr with | Some o -> - test.MemoryGraph.Encode o + // let index = ref 0 + // if indices.TryGetValue(addr, index) then + // let referenceRepr : referenceRepr = {index = index.Value} + // referenceRepr :> obj + // else + // let index = test.MemoryGraph.ReserveRepresentation() + // indices.Add(addr, index) + test.MemoryGraph.Encode o | None -> // mocks and big arrays are allocated symbolically // __unreachable__() let eval address = @@ -228,7 +235,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 449e3e18d..d32719098 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -780,20 +780,16 @@ module internal Z3 = Memory.FillRegion state constantValue region) // TODO : move to utils ? - let unboxConcrete term = + let rec unboxConcrete term = match term with | {term = Concrete(v, _)} -> v |> unbox + | {term = HeapRef({term = ConcreteHeapAddress(addr)}, _)} when VectorTime.less addr VectorTime.zero -> + cm.VirtToPhys addr |> unbox | _ -> __unreachable__() - // Create default concretes - encodingCache.heapAddresses |> Seq.iter (fun kvp -> - let typ, _ = kvp.Key - let addr = kvp.Value - let cha = addr |> ConcreteHeapAddress - if VectorTime.lessOrEqual VectorTime.zero addr || typ = typeof then () - else + let rec createObjOfType cha typ = match typ with - | ArrayType(_, SymbolicDimension _) -> () + | ArrayType(_, SymbolicDimension _) -> None | ArrayType(elemType, dim) -> let eval address = address |> Ref |> Memory.Read state |> unboxConcrete @@ -809,45 +805,50 @@ module internal Z3 = Array.init rank (fun i -> ArrayLowerBound(cha, MakeNumber i, arrayType) |> eval) | SymbolicDimension -> __unreachable__() let length = Array.reduce ( * ) lengths - if length > 128 then () // TODO: move magic number + if length > 128 then None // TODO: move magic number else - - let arr = - if (lowerBounds <> null) - then Array.CreateInstance(elemType, lengths, lowerBounds) - else Array.CreateInstance(elemType, lengths) - // TODO: fill with defaults - cm.Allocate addr arr - let result = ref (ref Nop) // TODO: do we need the else branch here? - if defaultValues.TryGetValue(ArrayIndexSort arrayType, result) then - // TODO: rewrite - let product xss = - let rec product xss k = - match xss with - | [] -> k [[]] - | xs::xss -> product xss (fun yss -> List.collect (fun ys -> List.map (fun x -> x :: ys) xs) yss |> k) - product xss id - let indexes = Seq.map (fun l -> List.init l id) lengths |> List.ofSeq - let indexes = product indexes - let value = result.Value.Value |> unboxConcrete - List.iter (fun i -> cm.WriteArrayIndex addr i value) indexes + let arr = + if (lowerBounds <> null) + then Array.CreateInstance(elemType, lengths, lowerBounds) + else Array.CreateInstance(elemType, lengths) + let result = ref (ref Nop) // TODO: do we need the else branch here? + if defaultValues.TryGetValue(ArrayIndexSort arrayType, result) then + let value = result.Value.Value |> unboxConcrete + Array.fill arr value + Some (arr :> obj) + | _ when typ = typeof -> + let length : int = ClassField(cha, Reflection.stringLengthField) |> Ref |> Memory.Read state |> unboxConcrete + let contents : char array = Array.init length (fun i -> ArrayIndex(cha, [MakeNumber i], (typeof, 1, true)) + |> Ref |> Memory.Read state |> unboxConcrete) + Some (String(contents) :> obj) | _ -> - if VectorTime.less addr VectorTime.zero && not <| cm.Contains addr && typ <> typeof then - let fields = Reflection.fieldsOf false typ |> Seq.map fst - - try - let o = Reflection.createObject typ - cm.Allocate addr o - fields |> Seq.iter (fun fId -> - let region = HeapFieldSort fId - let result = ref (ref Nop) - if defaultValues.TryGetValue(region, result) then - cm.WriteClassField addr fId result.Value.Value - ) - with - | _ -> () // if type cannot be allocated concretely, it will be stored symbolically + let o = Reflection.createObject typ + Reflection.fieldsOf false typ |> + Seq.iter (fun (fid, finfo) -> + let value = createObjOfType StructField(cha, fId) finfo.FieldType + finfo.SetValue(o, value) + ) + Some o + // fields |> Seq.iter (fun fId -> + // let region = HeapFieldSort fId + // let result = ref (ref Nop) + // if defaultValues.TryGetValue(region, result) then + // cm.WriteClassField addr fId result.Value.Value + // ) + + // Create default concretes + encodingCache.heapAddresses |> Seq.iter (fun kvp -> + let typ, _ = kvp.Key + let addr = kvp.Value + let cha = addr |> ConcreteHeapAddress + if VectorTime.lessOrEqual VectorTime.zero addr || typ = typeof then () + else + match createObjOfType cha typ with + | Some o -> + cm.Allocate addr o + | None -> () // if type cannot be allocated concretely, it will be stored symbolically ) - + // Process stores encodingCache.regionConstants |> Seq.iter (fun kvp -> let region, fields = kvp.Key From 093caf1dd3849608e91fe1bd0a7097801a6768b5 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Thu, 10 Nov 2022 18:18:01 +0300 Subject: [PATCH 08/25] fixed some problems with defaults --- VSharp.Solver/Z3.fs | 78 ++++++++++++++++++++++++++++----------------- 1 file changed, 48 insertions(+), 30 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index d32719098..078f305b0 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -10,7 +10,14 @@ open VSharp.Core.SolverInteraction open Logger module internal Z3 = - + [] + type OptionalBuilder = + member __.Bind(opt, binder) = Option.bind binder opt + member __.Return(value) = Some value + member __.ReturnFrom(value) = value + member __.Zero() = None + member __.Using(resource : #System.IDisposable, binder) = let result = binder resource in resource.Dispose(); result + let opt = OptionalBuilder() // ------------------------------- Exceptions ------------------------------- type EncodingException(msg : string) = @@ -780,19 +787,22 @@ module internal Z3 = Memory.FillRegion state constantValue region) // TODO : move to utils ? - let rec unboxConcrete term = + let unboxConcrete term = match term with - | {term = Concrete(v, _)} -> v |> unbox - | {term = HeapRef({term = ConcreteHeapAddress(addr)}, _)} when VectorTime.less addr VectorTime.zero -> - cm.VirtToPhys addr |> unbox - | _ -> __unreachable__() + | {term = Concrete(v, _)} -> v |> unbox |> Some + // TODO: byRef (?) careful about creation order + // | {term = HeapRef({term = ConcreteHeapAddress(addr)}, _)} when VectorTime.less addr VectorTime.zero -> + // cm.VirtToPhys addr |> unbox + | _ -> None - let rec createObjOfType cha typ = + let rec createObjOfType depth cha typ = match typ with + | _ when depth <= 0 -> None |> Option.get // TODO: separate exception + | _ when typ = typeof -> None |> Option.get // TODO: separate exception | ArrayType(_, SymbolicDimension _) -> None | ArrayType(elemType, dim) -> let eval address = - address |> Ref |> Memory.Read state |> unboxConcrete + address |> Ref |> Memory.Read state |> unboxConcrete |> Option.get let arrayType, (lengths : int array), (lowerBounds : int array) = match dim with | Vector -> @@ -813,28 +823,28 @@ module internal Z3 = else Array.CreateInstance(elemType, lengths) let result = ref (ref Nop) // TODO: do we need the else branch here? if defaultValues.TryGetValue(ArrayIndexSort arrayType, result) then - let value = result.Value.Value |> unboxConcrete + let value = result.Value.Value |> unboxConcrete |> Option.get Array.fill arr value Some (arr :> obj) - | _ when typ = typeof -> - let length : int = ClassField(cha, Reflection.stringLengthField) |> Ref |> Memory.Read state |> unboxConcrete - let contents : char array = Array.init length (fun i -> ArrayIndex(cha, [MakeNumber i], (typeof, 1, true)) - |> Ref |> Memory.Read state |> unboxConcrete) - Some (String(contents) :> obj) + | _ when typ.IsValueType -> + None + // | _ when Types.IsNullable typ -> // TODO ? + // None | _ -> let o = Reflection.createObject typ Reflection.fieldsOf false typ |> Seq.iter (fun (fid, finfo) -> - let value = createObjOfType StructField(cha, fId) finfo.FieldType - finfo.SetValue(o, value) + match createObjOfType (depth - 1) cha finfo.FieldType with + | Some o1 -> finfo.SetValue(o, o1) + | None -> + let region = HeapFieldSort fid + let result = ref (ref Nop) + if defaultValues.TryGetValue(region, result) then + let value = result.Value.Value |> unboxConcrete |> Option.get + finfo.SetValue(o, value) ) Some o - // fields |> Seq.iter (fun fId -> - // let region = HeapFieldSort fId - // let result = ref (ref Nop) - // if defaultValues.TryGetValue(region, result) then - // cm.WriteClassField addr fId result.Value.Value - // ) + // Create default concretes encodingCache.heapAddresses |> Seq.iter (fun kvp -> @@ -843,10 +853,15 @@ module internal Z3 = let cha = addr |> ConcreteHeapAddress if VectorTime.lessOrEqual VectorTime.zero addr || typ = typeof then () else - match createObjOfType cha typ with - | Some o -> - cm.Allocate addr o - | None -> () // if type cannot be allocated concretely, it will be stored symbolically + try + match createObjOfType 4 cha typ with + | Some o -> + cm.Allocate addr o + | None -> () // if type cannot be allocated concretely, it will be stored symbolically + with + | :? MemberAccessException -> () // Could not create an instance + | :? ArgumentException -> () // Could not unbox concrete + | _ -> internalfail "Unexpected exception in object creation" ) // Process stores @@ -884,10 +899,13 @@ module internal Z3 = if VectorTime.less addr VectorTime.zero && not <| PersistentDict.contains addr state.allocatedTypes then state.allocatedTypes <- PersistentDict.add addr (ConcreteType typ) state.allocatedTypes if typ = typeof then - let length : int = ClassField(cha, Reflection.stringLengthField) |> Ref |> Memory.Read state |> unboxConcrete - let contents : char array = Array.init length (fun i -> ArrayIndex(cha, [MakeNumber i], (typeof, 1, true)) - |> Ref |> Memory.Read state |> unboxConcrete) - cm.Allocate addr (String(contents) :> obj) + try + let length : int = ClassField(cha, Reflection.stringLengthField) |> Ref |> Memory.Read state |> unboxConcrete |> Option.get + let contents : char array = Array.init length (fun i -> ArrayIndex(cha, [MakeNumber i], (typeof, 1, true)) + |> Ref |> Memory.Read state |> unboxConcrete |> Option.get) + cm.Allocate addr (String(contents) :> obj) + with + | _ -> () ) state.startingTime <- [encodingCache.lastSymbolicAddress - 1] From 494e84e7f58a8d63069d5a540ab5d64ad976a720 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Fri, 11 Nov 2022 14:28:11 +0300 Subject: [PATCH 09/25] tmp serialization fix --- VSharp.SILI/TestGenerator.fs | 23 +++++++++++++---------- VSharp.Utils/MemoryGraph.fs | 31 ++++++++++++++++--------------- VSharp.Utils/UnitTest.fs | 10 +++++----- 3 files changed, 34 insertions(+), 30 deletions(-) diff --git a/VSharp.SILI/TestGenerator.fs b/VSharp.SILI/TestGenerator.fs index 7bc11fcb1..d8c94ece8 100644 --- a/VSharp.SILI/TestGenerator.fs +++ b/VSharp.SILI/TestGenerator.fs @@ -68,7 +68,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 +101,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 @@ -124,14 +124,17 @@ module TestGenerator = | StateModel(modelState, _) -> 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 index = test.MemoryGraph.ReserveRepresentation() - // indices.Add(addr, index) - test.MemoryGraph.Encode 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) + orepr + | None -> orepr | None -> // mocks and big arrays are allocated symbolically // __unreachable__() let eval address = diff --git a/VSharp.Utils/MemoryGraph.fs b/VSharp.Utils/MemoryGraph.fs index 691d4e1c8..cc2e12c55 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 @@ -247,24 +248,24 @@ and MemoryGraph(repr : memoryRepr, mocker : ITypeMockSerializer, createCompactRe 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 @@ -276,7 +277,7 @@ and MemoryGraph(repr : memoryRepr, mocker : ITypeMockSerializer, createCompactRe | _ -> x.EncodeStructure obj x.Bind obj repr 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} 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) From 759341f6af7d6393dbf5f37551095fe83406e9fa Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Fri, 11 Nov 2022 19:08:18 +0300 Subject: [PATCH 10/25] serialization debug commit --- VSharp.Utils/MemoryGraph.fs | 1 + 1 file changed, 1 insertion(+) diff --git a/VSharp.Utils/MemoryGraph.fs b/VSharp.Utils/MemoryGraph.fs index cc2e12c55..02037778b 100644 --- a/VSharp.Utils/MemoryGraph.fs +++ b/VSharp.Utils/MemoryGraph.fs @@ -205,6 +205,7 @@ 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())) member private x.EncodeArray (arr : Array) = let contents = From 8493e815a85d442b3e1a6850d599274b60a79da2 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Mon, 14 Nov 2022 19:46:36 +0300 Subject: [PATCH 11/25] WIP: change initial cm allocation --- VSharp.SILI.Core/API.fs | 6 +- VSharp.SILI.Core/API.fsi | 2 +- VSharp.SILI.Core/ArrayInitialization.fs | 2 +- VSharp.SILI.Core/Memory.fs | 32 +++++----- VSharp.SILI/Interpreter.fs | 5 +- VSharp.SILI/TestGenerator.fs | 12 ++-- VSharp.Solver/Z3.fs | 82 ++++++++++--------------- 7 files changed, 65 insertions(+), 76 deletions(-) diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index 72d36040f..168cc2f4a 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 @@ -464,8 +464,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..0cdd19fd5 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 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/Memory.fs b/VSharp.SILI.Core/Memory.fs index ff1f9fc5e..0955f9448 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -441,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 @@ -454,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 @@ -477,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 @@ -949,7 +953,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 @@ -1008,7 +1012,7 @@ module internal Memory = 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 @@ -1019,7 +1023,7 @@ 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 -> diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index fdf8f9c76..ab6e9399e 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 @@ -1141,6 +1141,7 @@ type internal ILInterpreter(isConcolicMode : bool) as this = | StateModel(s, _) -> s | _ -> __unreachable__() modelState.allocatedTypes <- PersistentDict.add thisInModel (MockType mock) modelState.allocatedTypes + if modelState.concreteMemory.Contains thisInModel then modelState.concreteMemory.Remove thisInModel 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 d8c94ece8..a4a7d510c 100644 --- a/VSharp.SILI/TestGenerator.fs +++ b/VSharp.SILI/TestGenerator.fs @@ -136,12 +136,12 @@ module TestGenerator = orepr | None -> orepr | None -> // mocks and big arrays are allocated symbolically - // __unreachable__() - 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 + __unreachable__() + // 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 = diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 078f305b0..3901aaa21 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -741,7 +741,7 @@ module internal Z3 = (key, Some term, typ)) Memory.NewStackFrame state None (List.ofSeq frame) - // gather default values and array metadata + // gather default values, array metadata and strings let defaultValues = Dictionary() encodingCache.regionConstants |> Seq.iter (fun kvp -> let constant = kvp.Value @@ -757,7 +757,6 @@ module internal Z3 = if Types.IsValueType typeOfLocation then x.Decode cm typeOfLocation arr.Args.[0] else let addr = x.DecodeConcreteHeapAddress cm typeOfLocation arr.Args.[0] - // TODO: maybe we need to add cm allocate here? HeapRef (addr |> ConcreteHeapAddress) typeOfLocation x.WriteDictOfValueTypes defaultValues region fields region.TypeOfLocation constantValue else if arr.IsStore then @@ -766,7 +765,8 @@ module internal Z3 = let addr = x.DecodeMemoryKey cm region arr.Args.[1..arr.Args.Length - 2] match addr with | ArrayLength _ - | ArrayLowerBound _ -> + | ArrayLowerBound _ + | _ when typeOfLocation = typeof -> let value = if Types.IsValueType typeOfLocation then x.Decode cm typeOfLocation (Array.last arr.Args) @@ -785,21 +785,22 @@ module internal Z3 = let region = kvp.Key let constantValue = kvp.Value.Value Memory.FillRegion state constantValue region) - - // TODO : move to utils ? - let unboxConcrete term = - match term with - | {term = Concrete(v, _)} -> v |> unbox |> Some - // TODO: byRef (?) careful about creation order - // | {term = HeapRef({term = ConcreteHeapAddress(addr)}, _)} when VectorTime.less addr VectorTime.zero -> - // cm.VirtToPhys addr |> unbox - | _ -> None - - let rec createObjOfType depth cha typ = + + let rec unboxConcrete term = + match Terms.TryTermToObj state createObjOfType term with + | Some o -> Some (o |> unbox) + | None -> None + + and symbolicStringToObj cha = + let length : int = ClassField(cha, Reflection.stringLengthField) |> Ref |> Memory.Read state |> unboxConcrete |> Option.get + let contents : char array = Array.init length (fun i -> ArrayIndex(cha, [MakeNumber i], (typeof, 1, true)) + |> Ref |> Memory.Read state |> unboxConcrete |> Option.get) + String(contents) :> obj + + and createObjOfType addr typ = + let cha = addr |> ConcreteHeapAddress match typ with - | _ when depth <= 0 -> None |> Option.get // TODO: separate exception - | _ when typ = typeof -> None |> Option.get // TODO: separate exception - | ArrayType(_, SymbolicDimension _) -> None + | ArrayType(_, SymbolicDimension _) -> () | ArrayType(elemType, dim) -> let eval address = address |> Ref |> Memory.Read state |> unboxConcrete |> Option.get @@ -815,7 +816,7 @@ module internal Z3 = Array.init rank (fun i -> ArrayLowerBound(cha, MakeNumber i, arrayType) |> eval) | SymbolicDimension -> __unreachable__() let length = Array.reduce ( * ) lengths - if length > 128 then None // TODO: move magic number + if length > 128 then () // TODO: move magic number else let arr = if (lowerBounds <> null) @@ -825,40 +826,31 @@ module internal Z3 = if defaultValues.TryGetValue(ArrayIndexSort arrayType, result) then let value = result.Value.Value |> unboxConcrete |> Option.get Array.fill arr value - Some (arr :> obj) - | _ when typ.IsValueType -> - None - // | _ when Types.IsNullable typ -> // TODO ? - // None + cm.Allocate addr arr + | _ when typ = typeof -> + cm.Allocate addr (symbolicStringToObj cha) | _ -> let o = Reflection.createObject typ Reflection.fieldsOf false typ |> Seq.iter (fun (fid, finfo) -> - match createObjOfType (depth - 1) cha finfo.FieldType with - | Some o1 -> finfo.SetValue(o, o1) - | None -> - let region = HeapFieldSort fid - let result = ref (ref Nop) - if defaultValues.TryGetValue(region, result) then - let value = result.Value.Value |> unboxConcrete |> Option.get - finfo.SetValue(o, value) + // TODO: do we need a special case for strings here? + let region = HeapFieldSort fid + let result = ref (ref Nop) + if defaultValues.TryGetValue(region, result) then + let value = result.Value.Value |> unboxConcrete |> Option.get + finfo.SetValue(o, value) ) - Some o - + cm.Allocate addr o // Create default concretes encodingCache.heapAddresses |> Seq.iter (fun kvp -> let typ, _ = kvp.Key let addr = kvp.Value - let cha = addr |> ConcreteHeapAddress - if VectorTime.lessOrEqual VectorTime.zero addr || typ = typeof then () + if VectorTime.lessOrEqual VectorTime.zero addr || cm.Contains addr then () else try - match createObjOfType 4 cha typ with - | Some o -> - cm.Allocate addr o - | None -> () // if type cannot be allocated concretely, it will be stored symbolically - with + createObjOfType 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 | _ -> internalfail "Unexpected exception in object creation" @@ -895,17 +887,9 @@ module internal Z3 = encodingCache.heapAddresses |> Seq.iter (fun kvp -> let typ, _ = kvp.Key let addr = kvp.Value - let cha = ConcreteHeapAddress addr if VectorTime.less addr VectorTime.zero && not <| PersistentDict.contains addr state.allocatedTypes then state.allocatedTypes <- PersistentDict.add addr (ConcreteType typ) state.allocatedTypes - if typ = typeof then - try - let length : int = ClassField(cha, Reflection.stringLengthField) |> Ref |> Memory.Read state |> unboxConcrete |> Option.get - let contents : char array = Array.init length (fun i -> ArrayIndex(cha, [MakeNumber i], (typeof, 1, true)) - |> Ref |> Memory.Read state |> unboxConcrete |> Option.get) - cm.Allocate addr (String(contents) :> obj) - with - | _ -> () + ) state.startingTime <- [encodingCache.lastSymbolicAddress - 1] From b5f12e194e64072e5bd78169832f350c8a3cf413 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Tue, 15 Nov 2022 19:25:05 +0300 Subject: [PATCH 12/25] some fixes for recursive cases --- VSharp.SILI.Core/API.fs | 1 + VSharp.SILI.Core/API.fsi | 2 + VSharp.SILI/Interpreter.fs | 2 +- VSharp.Solver/Z3.fs | 91 ++++++++++++++++++++------------------ 4 files changed, 53 insertions(+), 43 deletions(-) diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index 168cc2f4a..5105f1094 100644 --- a/VSharp.SILI.Core/API.fs +++ b/VSharp.SILI.Core/API.fs @@ -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 diff --git a/VSharp.SILI.Core/API.fsi b/VSharp.SILI.Core/API.fsi index 0cdd19fd5..808305449 100644 --- a/VSharp.SILI.Core/API.fsi +++ b/VSharp.SILI.Core/API.fsi @@ -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 diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index ab6e9399e..f1d1d713b 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -1140,8 +1140,8 @@ 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 - if modelState.concreteMemory.Contains thisInModel then modelState.concreteMemory.Remove thisInModel candidateTypes |> Seq.iter (function | ConcreteType t -> AddConstraint cilState.state !!(Types.TypeIsRef cilState.state t this) | _ -> ()) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 3901aaa21..1faae498b 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -798,49 +798,56 @@ module internal Z3 = String(contents) :> obj and createObjOfType addr typ = - let cha = addr |> ConcreteHeapAddress - match typ with - | ArrayType(_, SymbolicDimension _) -> () - | ArrayType(elemType, dim) -> - let eval address = - address |> Ref |> Memory.Read state |> unboxConcrete |> Option.get - 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__() - let length = Array.reduce ( * ) lengths - if length > 128 then () // TODO: move magic number - else - let arr = - if (lowerBounds <> null) - then Array.CreateInstance(elemType, lengths, lowerBounds) - else Array.CreateInstance(elemType, lengths) - let result = ref (ref Nop) // TODO: do we need the else branch here? - if defaultValues.TryGetValue(ArrayIndexSort arrayType, result) then - let value = result.Value.Value |> unboxConcrete |> Option.get - Array.fill arr value - cm.Allocate addr arr - | _ when typ = typeof -> - cm.Allocate addr (symbolicStringToObj cha) - | _ -> - let o = Reflection.createObject typ - Reflection.fieldsOf false typ |> - Seq.iter (fun (fid, finfo) -> - // TODO: do we need a special case for strings here? - let region = HeapFieldSort fid - let result = ref (ref Nop) - if defaultValues.TryGetValue(region, result) then - let value = result.Value.Value |> unboxConcrete |> Option.get - finfo.SetValue(o, value) + try + let cha = addr |> ConcreteHeapAddress + match typ with + | ArrayType(_, SymbolicDimension _) -> () + | ArrayType(elemType, dim) -> + let eval address = + address |> Ref |> Memory.Read state |> unboxConcrete |> Option.get + 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__() + let length = Array.reduce ( * ) lengths + if length > 128 then () // TODO: move magic number + else + let arr = + if (lowerBounds <> null) + then Array.CreateInstance(elemType, lengths, lowerBounds) + else Array.CreateInstance(elemType, lengths) + let result = ref (ref Nop) // TODO: do we need the else branch here? + if defaultValues.TryGetValue(ArrayIndexSort arrayType, result) then + let value = result.Value.Value |> unboxConcrete |> Option.get + Array.fill arr value + cm.Allocate addr arr + // | _ when typ.IsPointer -> + // () + | _ when typ = typeof -> + cm.Allocate addr (symbolicStringToObj cha) + | _ -> + let o = Reflection.createObject typ + cm.Allocate addr o + Reflection.fieldsOf false typ |> + Seq.iter (fun (fid, finfo) -> + // TODO: do we need a special case for strings here? + let region = HeapFieldSort fid + let result = ref (ref Nop) + if defaultValues.TryGetValue(region, result) then + let value = result.Value.Value |> unboxConcrete |> Option.get + cm.WriteClassField addr fid value ) - cm.Allocate addr o + with + | :? MemberAccessException as e -> // Could not create an instance + if cm.Contains addr then cm.Remove addr + raise e // Create default concretes encodingCache.heapAddresses |> Seq.iter (fun kvp -> From c5a5419f13e0be2660b5d341c25bad000bfb88c1 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Fri, 18 Nov 2022 14:26:22 +0300 Subject: [PATCH 13/25] A bit of refactoring --- VSharp.SILI.Core/API.fs | 1 + VSharp.SILI.Core/API.fsi | 1 + VSharp.SILI.Core/Memory.fs | 17 +++++ VSharp.SILI/TestGenerator.fs | 14 +--- VSharp.Solver/Z3.fs | 139 +++++++++++++++-------------------- 5 files changed, 82 insertions(+), 90 deletions(-) diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index 5105f1094..2edc58ecf 100644 --- a/VSharp.SILI.Core/API.fs +++ b/VSharp.SILI.Core/API.fs @@ -358,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 diff --git a/VSharp.SILI.Core/API.fsi b/VSharp.SILI.Core/API.fsi index 808305449..ef1ab6831 100644 --- a/VSharp.SILI.Core/API.fsi +++ b/VSharp.SILI.Core/API.fsi @@ -230,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/Memory.fs b/VSharp.SILI.Core/Memory.fs index 0955f9448..5689fdffe 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -699,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 = diff --git a/VSharp.SILI/TestGenerator.fs b/VSharp.SILI/TestGenerator.fs index a4a7d510c..8d083d684 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 diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 1faae498b..fbb17ad59 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -76,6 +76,56 @@ 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) + if defaults.TryGetValue(ArrayIndexSort arrayType, result) then + let value = result.Value.Value |> unboxConcrete' |> Option.get + Array.fill arr value + cm.Allocate addr arr + | _ 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, finfo) -> + let region = HeapFieldSort fid + if defaults.TryGetValue(region, result) then + let value = result.Value.Value |> unboxConcrete' |> Option.get + cm.WriteClassField addr fid value + ) + with + | :? MemberAccessException as e -> // Could not create an instance + if cm.Contains addr then cm.Remove addr + raise e + // ------------------------------- Encoding: primitives ------------------------------- type private Z3Builder(ctx : Context) = @@ -786,81 +836,20 @@ module internal Z3 = let constantValue = kvp.Value.Value Memory.FillRegion state constantValue region) - let rec unboxConcrete term = - match Terms.TryTermToObj state createObjOfType term with - | Some o -> Some (o |> unbox) - | None -> None - - and symbolicStringToObj cha = - let length : int = ClassField(cha, Reflection.stringLengthField) |> Ref |> Memory.Read state |> unboxConcrete |> Option.get - let contents : char array = Array.init length (fun i -> ArrayIndex(cha, [MakeNumber i], (typeof, 1, true)) - |> Ref |> Memory.Read state |> unboxConcrete |> Option.get) - String(contents) :> obj - - and createObjOfType addr typ = - try - let cha = addr |> ConcreteHeapAddress - match typ with - | ArrayType(_, SymbolicDimension _) -> () - | ArrayType(elemType, dim) -> - let eval address = - address |> Ref |> Memory.Read state |> unboxConcrete |> Option.get - 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__() - let length = Array.reduce ( * ) lengths - if length > 128 then () // TODO: move magic number - else - let arr = - if (lowerBounds <> null) - then Array.CreateInstance(elemType, lengths, lowerBounds) - else Array.CreateInstance(elemType, lengths) - let result = ref (ref Nop) // TODO: do we need the else branch here? - if defaultValues.TryGetValue(ArrayIndexSort arrayType, result) then - let value = result.Value.Value |> unboxConcrete |> Option.get - Array.fill arr value - cm.Allocate addr arr - // | _ when typ.IsPointer -> - // () - | _ when typ = typeof -> - cm.Allocate addr (symbolicStringToObj cha) - | _ -> - let o = Reflection.createObject typ - cm.Allocate addr o - Reflection.fieldsOf false typ |> - Seq.iter (fun (fid, finfo) -> - // TODO: do we need a special case for strings here? - let region = HeapFieldSort fid - let result = ref (ref Nop) - if defaultValues.TryGetValue(region, result) then - let value = result.Value.Value |> unboxConcrete |> Option.get - cm.WriteClassField addr fid value - ) - with - | :? MemberAccessException as e -> // Could not create an instance - if cm.Contains addr then cm.Remove addr - raise e - // Create default concretes encodingCache.heapAddresses |> Seq.iter (fun kvp -> let typ, _ = kvp.Key let addr = kvp.Value - if VectorTime.lessOrEqual VectorTime.zero addr || cm.Contains addr then () - else - try - createObjOfType 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 - | _ -> internalfail "Unexpected exception in object creation" + 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 + | _ -> internalfail "Unexpected exception in object creation" ) // Process stores @@ -891,14 +880,6 @@ module internal Z3 = else internalfailf "Unexpected array expression in model: %O" arr parseArray arr) - 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] state.model <- PrimitiveModel subst encodingCache.heapAddresses.Clear() From 04fa0abcaf1471e246962246e9d23a9128a58e97 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Fri, 18 Nov 2022 19:30:35 +0300 Subject: [PATCH 14/25] Fixed mock objects unmarshalling --- VSharp.InternalCalls/Type.fs | 3 ++- VSharp.SILI.Core/ConcreteMemory.fs | 33 ++++++++++++++++++++++++++---- VSharp.SILI.Core/Memory.fs | 11 ++++++---- VSharp.SILI.Core/State.fs | 2 ++ VSharp.SILI.Core/TypeSolver.fs | 4 ++-- VSharp.SILI/TestGenerator.fs | 12 +++++------ VSharp.Solver/Z3.fs | 10 ++++++++- 7 files changed, 57 insertions(+), 18 deletions(-) diff --git a/VSharp.InternalCalls/Type.fs b/VSharp.InternalCalls/Type.fs index c1caf51c4..61859f6f7 100644 --- a/VSharp.InternalCalls/Type.fs +++ b/VSharp.InternalCalls/Type.fs @@ -43,7 +43,8 @@ module internal Type = List.singleton (typeRef, state) | _ -> __notImplemented__() // TypeOfMethod state (Types.FromDotNetType state t) - // TODO: restore it after rewriting marshaling/unmarshaling + // TODO: restore it after rewriting marshaling/ + // unmarshaling // __notImplemented__() let GetAssembly (state : state) (args : term list) : (term * state) list = diff --git a/VSharp.SILI.Core/ConcreteMemory.fs b/VSharp.SILI.Core/ConcreteMemory.fs index 1d4bff0ab..cd2bf7bc9 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,12 @@ type public ConcreteMemory private (physToVirt, virtToPhys) = let physicalAddress = {object = obj} virtToPhys[address] <- physicalAddress + member private x.getDepsList ds = + let ds' = ds |> Set.ofList |> Set.toList + let ds'' = List.collect (fun a -> if dependencies.ContainsKey(a) then a::dependencies[a] else [a]) ds |> Set.ofList |> Set.toList + if ds' = ds'' then ds' + else x.getDepsList ds'' + // ------------------------------- Copying ------------------------------- interface IConcreteMemory with @@ -104,14 +112,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 ----------------------------- @@ -145,6 +157,7 @@ type public ConcreteMemory private (physToVirt, virtToPhys) = assert(virtToPhys.ContainsKey address |> not) let physicalAddress = {object = obj} virtToPhys.Add(address, physicalAddress) + // dependencies.Add(address, []) if obj = String.Empty then physToVirt[physicalAddress] <- address else physToVirt.Add(physicalAddress, address) @@ -210,8 +223,20 @@ type public ConcreteMemory private (physToVirt, virtToPhys) = let physAddress = {object = string} physToVirt[physAddress] <- stringAddress + // ------------------------------- Add deps ----------------------------- + + 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 + virtToPhys.Remove a) |> List.forall id assert removed diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index 5689fdffe..148014c51 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -1014,15 +1014,18 @@ 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 address = ConcreteHeapAddress concreteAddress + let cm = state.concreteMemory + let deps = cm.GetDeps concreteAddress |> List.map cm.VirtToPhys + deps |> List.iter (unmarshallObj state address) cm.Remove concreteAddress // ------------------------------- Writing ------------------------------- 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 88964030d..6283cbc68 100644 --- a/VSharp.SILI.Core/TypeSolver.fs +++ b/VSharp.SILI.Core/TypeSolver.fs @@ -333,7 +333,6 @@ module TypeSolver = | TypeSat(refsTypes, typeParams) -> let cm = modelState.concreteMemory let refineTypes addr t = - modelState.allocatedTypes <- PersistentDict.add addr t modelState.allocatedTypes match t with | ConcreteType t -> match cm.TryVirtToPhys addr with @@ -346,7 +345,8 @@ module TypeSolver = 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/TestGenerator.fs b/VSharp.SILI/TestGenerator.fs index 8d083d684..e5cdbe2a6 100644 --- a/VSharp.SILI/TestGenerator.fs +++ b/VSharp.SILI/TestGenerator.fs @@ -128,12 +128,12 @@ module TestGenerator = orepr | None -> orepr | None -> // mocks and big arrays are allocated symbolically - __unreachable__() - // 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 + // __unreachable__() + 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 = diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index fbb17ad59..6909245ac 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -101,6 +101,10 @@ module internal Z3 = let arr = if (lowerBounds = null) then Array.CreateInstance(elemType, lengths) else Array.CreateInstance(elemType, lengths, lowerBounds) 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 cm.Allocate addr arr @@ -118,13 +122,17 @@ module internal Z3 = Seq.iter (fun (fid, finfo) -> let region = HeapFieldSort fid if defaults.TryGetValue(region, result) then + match result.Value.Value with + | {term = HeapRef({term = ConcreteHeapAddress(a)}, _)} -> + cm.AddDep a addr + | _ -> () let value = result.Value.Value |> unboxConcrete' |> Option.get cm.WriteClassField addr fid value ) with | :? MemberAccessException as e -> // Could not create an instance if cm.Contains addr then cm.Remove addr - raise e + raise e // ------------------------------- Encoding: primitives ------------------------------- From ed5761cddead1e09881eba6e99a944bb19224294 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Mon, 21 Nov 2022 13:17:14 +0300 Subject: [PATCH 15/25] Fix array bug (requires refactoring) --- VSharp.Solver/Z3.fs | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 6909245ac..a25826d29 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -100,6 +100,7 @@ module internal Z3 = 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)}, _)} -> @@ -107,7 +108,6 @@ module internal Z3 = | _ -> () let value = result.Value.Value |> unboxConcrete' |> Option.get Array.fill arr value - cm.Allocate addr arr | _ when typ = typeof -> let arTyp = (typeof, 1, true) let l : int = ClassField(cha, Reflection.stringLengthField) |> Ref @@ -821,9 +821,8 @@ module internal Z3 = assert(arr.Args.Length >= 3) parseArray arr.Args.[0] let addr = x.DecodeMemoryKey cm region arr.Args.[1..arr.Args.Length - 2] + // TODO : remove copypaste match addr with - | ArrayLength _ - | ArrayLowerBound _ | _ when typeOfLocation = typeof -> let value = if Types.IsValueType typeOfLocation then @@ -833,6 +832,16 @@ module internal Z3 = HeapRef address typeOfLocation let states = Memory.Write state (Ref addr) value assert(states.Length = 1 && states.[0] = state) + | ArrayLength _ + | ArrayLowerBound _ -> + let value = + if Types.IsValueType typeOfLocation then + x.Decode cm typeOfLocation (Array.last arr.Args) + else + let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress cm typeOfLocation |> ConcreteHeapAddress + HeapRef address typeOfLocation + let states = Memory.Write state (Ref addr) value + assert(states.Length = 1 && states.[0] = state) | _ -> () else () @@ -886,7 +895,7 @@ module internal Z3 = assert(states.Length = 1 && states.[0] = state) elif arr.IsConst || arr.IsConstantArray then () else internalfailf "Unexpected array expression in model: %O" arr - parseArray arr) + if typeOfLocation = typeof then () else parseArray arr) state.startingTime <- [encodingCache.lastSymbolicAddress - 1] state.model <- PrimitiveModel subst From 679b6e993edcaf17d09a0b3e20a83d28cfab24cb Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Mon, 21 Nov 2022 17:58:17 +0300 Subject: [PATCH 16/25] refactoring --- VSharp.Solver/Z3.fs | 92 +++++++++++++++++---------------------------- 1 file changed, 35 insertions(+), 57 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index a25826d29..eed8debad 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -119,7 +119,7 @@ module internal Z3 = let o = Reflection.createObject typ cm.Allocate addr o Reflection.fieldsOf false typ |> - Seq.iter (fun (fid, finfo) -> + Seq.iter (fun (fid, _) -> let region = HeapFieldSort fid if defaults.TryGetValue(region, result) then match result.Value.Value with @@ -799,17 +799,38 @@ module internal Z3 = (key, Some term, typ)) Memory.NewStackFrame state None (List.ofSeq frame) - // gather default values, array metadata and strings let defaultValues = Dictionary() - encodingCache.regionConstants |> Seq.iter (fun kvp -> + let processRegionConstraints isSymbolyc (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 getValueAndWrite (arr : Expr) addr = + let value = + if Types.IsValueType typeOfLocation then + x.Decode cm typeOfLocation (Array.last arr.Args) + else + let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress cm typeOfLocation |> ConcreteHeapAddress + HeapRef address typeOfLocation + 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) (fun _ -> ()) + let writeMixed arr = writeHelper (fun _ -> ()) (getValueAndWrite arr) + let rec parseArray (arr : Expr) = - if arr.IsConstantArray then + if arr.IsConstantArray && isSymbolyc then // defaults are written symbolically assert(arr.Args.Length = 1) let constantValue = if Types.IsValueType typeOfLocation then x.Decode cm typeOfLocation arr.Args.[0] @@ -821,33 +842,15 @@ module internal Z3 = assert(arr.Args.Length >= 3) parseArray arr.Args.[0] let addr = x.DecodeMemoryKey cm region arr.Args.[1..arr.Args.Length - 2] - // TODO : remove copypaste - match addr with - | _ when typeOfLocation = typeof -> - let value = - if Types.IsValueType typeOfLocation then - x.Decode cm typeOfLocation (Array.last arr.Args) - else - let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress cm typeOfLocation |> ConcreteHeapAddress - HeapRef address typeOfLocation - let states = Memory.Write state (Ref addr) value - assert(states.Length = 1 && states.[0] = state) - | ArrayLength _ - | ArrayLowerBound _ -> - let value = - if Types.IsValueType typeOfLocation then - x.Decode cm typeOfLocation (Array.last arr.Args) - else - let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress cm typeOfLocation |> ConcreteHeapAddress - HeapRef address typeOfLocation - let states = Memory.Write state (Ref addr) value - assert(states.Length = 1 && states.[0] = state) - | _ -> () - else - () + if isSymbolyc + 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 - ) - // fill symbolic memory with defaults + + // Process symbolic writes + encodingCache.regionConstants |> Seq.iter (processRegionConstraints true) defaultValues |> Seq.iter (fun kvp -> let region = kvp.Key let constantValue = kvp.Value.Value @@ -869,33 +872,8 @@ module internal Z3 = | _ -> internalfail "Unexpected exception in object creation" ) - // Process stores - encodingCache.regionConstants |> Seq.iter (fun kvp -> - let region, fields = kvp.Key - let constant = kvp.Value - let arr = m.Eval(constant, false) - let typeOfLocation = - if fields.IsEmpty then region.TypeOfLocation - else fields.Head.typ - let rec parseArray (arr : Expr) = - if arr.IsDefaultArray then - assert(arr.Args.Length = 1) - elif arr.IsStore then - assert(arr.Args.Length >= 3) - parseArray arr.Args.[0] - let address = x.DecodeMemoryKey cm region arr.Args.[1..arr.Args.Length - 2] - let value = - if Types.IsValueType typeOfLocation then - x.Decode cm typeOfLocation (Array.last arr.Args) - else - let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress cm 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 || arr.IsConstantArray then () - else internalfailf "Unexpected array expression in model: %O" arr - if typeOfLocation = typeof then () else parseArray arr) + // Process stores + encodingCache.regionConstants |> Seq.iter (processRegionConstraints false) state.startingTime <- [encodingCache.lastSymbolicAddress - 1] state.model <- PrimitiveModel subst From 7175423423d52351cb39e60f88248192e30c7e7b Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Tue, 22 Nov 2022 22:48:23 +0300 Subject: [PATCH 17/25] fixed MemoryGraph encode --- VSharp.Utils/MemoryGraph.fs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/VSharp.Utils/MemoryGraph.fs b/VSharp.Utils/MemoryGraph.fs index 02037778b..779409ba8 100644 --- a/VSharp.Utils/MemoryGraph.fs +++ b/VSharp.Utils/MemoryGraph.fs @@ -272,11 +272,16 @@ and MemoryGraph(repr : memoryRepr, mocker : ITypeMockSerializer, createCompactRe match Seq.tryFindIndex (fun obj' -> Object.ReferenceEquals(obj, obj')) sourceObjects with | Some idx -> idx | None -> + let i = x.ReserveRepresentation() + let r : referenceRepr = {index = i} + sourceObjects.[i] <- obj + objReprs.[i] <- r let repr = match t with | _ when t.IsArray -> x.EncodeArray (obj :?> Array) | _ -> x.EncodeStructure obj - x.Bind obj repr + objReprs.[i] <- repr + i let reference : referenceRepr = {index = idx} reference :> obj, Some idx From 243703689ea9f9e723f9914f8dcbda41847f7687 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Wed, 23 Nov 2022 15:48:07 +0300 Subject: [PATCH 18/25] fixed unmarshalling --- VSharp.SILI.Core/Memory.fs | 11 +++++++--- VSharp.SILI/TestGenerator.fs | 8 +++----- VSharp.Solver/Z3.fs | 40 +++++++++++++++++++++--------------- 3 files changed, 34 insertions(+), 25 deletions(-) diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index 148014c51..105dd7adb 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -1022,10 +1022,9 @@ module internal Memory = | _ -> unmarshallClass state address obj let unmarshall (state : state) concreteAddress = - let address = ConcreteHeapAddress concreteAddress let cm = state.concreteMemory - let deps = cm.GetDeps concreteAddress |> List.map cm.VirtToPhys - deps |> List.iter (unmarshallObj state address) + 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 ------------------------------- @@ -1036,6 +1035,9 @@ module internal Memory = 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 @@ -1048,6 +1050,9 @@ module internal Memory = 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/TestGenerator.fs b/VSharp.SILI/TestGenerator.fs index e5cdbe2a6..a8fa3f5a4 100644 --- a/VSharp.SILI/TestGenerator.fs +++ b/VSharp.SILI/TestGenerator.fs @@ -123,12 +123,10 @@ module TestGenerator = else let orepr, index = test.MemoryGraph.Encode o match index with - | Some i -> - indices.Add(addr, i) - orepr - | None -> orepr + | Some i -> indices.Add(addr, i) + | None -> () + orepr | None -> // mocks and big arrays are allocated symbolically - // __unreachable__() 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) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index eed8debad..7510f20a8 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -131,7 +131,7 @@ module internal Z3 = ) with | :? MemberAccessException as e -> // Could not create an instance - if cm.Contains addr then cm.Remove addr + if cm.Contains addr then Memory.Unmarshall state addr raise e // ------------------------------- Encoding: primitives ------------------------------- @@ -798,9 +798,22 @@ module internal Z3 = let typ = TypeOf term (key, Some term, typ)) Memory.NewStackFrame state None (List.ofSeq frame) - + let defaultValues = Dictionary() - let processRegionConstraints isSymbolyc (kvp : KeyValuePair<(regionSort * fieldId list), ArrayExpr>) = + + let concreteAllocator typ addr = + 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 + | _ -> internalfail "Unexpected exception in object creation" + + let processRegionConstraints isSymbolic (kvp : KeyValuePair<(regionSort * fieldId list), ArrayExpr>) = let constant = kvp.Value let arr = m.Eval(constant, false) let region, fields = kvp.Key @@ -813,8 +826,8 @@ module internal Z3 = if Types.IsValueType typeOfLocation then x.Decode cm typeOfLocation (Array.last arr.Args) else - let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress cm typeOfLocation |> ConcreteHeapAddress - HeapRef address typeOfLocation + let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress cm typeOfLocation + HeapRef (address |> ConcreteHeapAddress) typeOfLocation let states = Memory.Write state (Ref addr) value assert(states.Length = 1 && states.[0] = state) @@ -830,19 +843,21 @@ module internal Z3 = let writeMixed arr = writeHelper (fun _ -> ()) (getValueAndWrite arr) let rec parseArray (arr : Expr) = - if arr.IsConstantArray && isSymbolyc then // defaults are written symbolically + if arr.IsConstantArray && isSymbolic then // defaults are written symbolically assert(arr.Args.Length = 1) let constantValue = if Types.IsValueType typeOfLocation then x.Decode cm typeOfLocation arr.Args.[0] else let addr = x.DecodeConcreteHeapAddress cm typeOfLocation arr.Args.[0] + // concreteAllocator typeOfLocation addr HeapRef (addr |> ConcreteHeapAddress) typeOfLocation x.WriteDictOfValueTypes defaultValues region fields region.TypeOfLocation constantValue else if arr.IsStore then assert(arr.Args.Length >= 3) parseArray arr.Args.[0] let addr = x.DecodeMemoryKey cm region arr.Args.[1..arr.Args.Length - 2] - if isSymbolyc + // concreteAllocator typeOfLocation addr + if isSymbolic then writeSymbolic arr addr else writeMixed arr addr elif arr.IsConst || arr.IsConstantArray then () @@ -860,16 +875,7 @@ module internal Z3 = encodingCache.heapAddresses |> Seq.iter (fun kvp -> let typ, _ = kvp.Key let addr = kvp.Value - 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 - | _ -> internalfail "Unexpected exception in object creation" + concreteAllocator typ addr ) // Process stores From 815bcc911ac6dbb8bf2547b3ad1be520c3c38ad4 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Wed, 23 Nov 2022 16:11:12 +0300 Subject: [PATCH 19/25] change decode signature --- VSharp.Solver/Z3.fs | 87 ++++++++++++++++++++++----------------------- 1 file changed, 43 insertions(+), 44 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 7510f20a8..10768c310 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -140,7 +140,7 @@ module internal Z3 = 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 @@ -628,12 +628,12 @@ module internal Z3 = // ------------------------------- Decoding ------------------------------- - member private x.DecodeExpr (cm : IConcreteMemory) 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 cm t) |> List.ofSeq) t + Expression (Operator op) (expr.Args |> Seq.map (x.Decode state t cmAllocate) |> List.ofSeq) t - member private x.DecodeBoolExpr (cm : IConcreteMemory) op (expr : Expr) = - x.DecodeExpr cm 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 @@ -642,8 +642,9 @@ module internal Z3 = elif bv.SortSize = 16u then typeof else __unreachable__() - member private x.DecodeConcreteHeapAddress (cm : IConcreteMemory) 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 @@ -668,14 +669,14 @@ module internal Z3 = if encodingCache.staticKeys.TryGetValue(expr, result) then result.Value else __notImplemented__() - member private x.DecodeMemoryKey (cm : IConcreteMemory) (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 cm field.declaringType |> ConcreteHeapAddress + let address = exprs.[0] |> x.DecodeConcreteHeapAddress state field.declaringType cmAllocate |> ConcreteHeapAddress ClassField(address, field) | StaticFieldSort field -> assert(exprs.Length = 1) @@ -683,22 +684,22 @@ module internal Z3 = StaticField(typ, field) | ArrayIndexSort typ -> assert(exprs.Length >= 2) - let heapAddress = exprs.[0] |> x.DecodeConcreteHeapAddress cm (toType typ) |> ConcreteHeapAddress - let indices = exprs |> Seq.tail |> Seq.map (x.Decode cm 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 cm (toType typ) |> ConcreteHeapAddress - let index = x.Decode cm 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 cm (toType typ) |> ConcreteHeapAddress - let index = x.Decode cm 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 cm typeof exprs.[0] + let index = x.Decode state typeof cmAllocate exprs.[0] StackBufferIndex(key, index) member private x.DecodeBv t (bv : BitVecNum) = @@ -709,11 +710,11 @@ module internal Z3 = | 8u -> Concrete (convert bv.Int t) t | _ -> __notImplemented__() - member public x.Decode (cm: IConcreteMemory) 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 cm 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] @@ -724,18 +725,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 cm OperationType.LogicalNot expr - elif expr.IsAnd then x.DecodeBoolExpr cm OperationType.LogicalAnd expr - elif expr.IsOr then x.DecodeBoolExpr cm OperationType.LogicalOr expr - elif expr.IsEq then x.DecodeBoolExpr cm OperationType.Equal expr - elif expr.IsBVSGT then x.DecodeBoolExpr cm OperationType.Greater expr - elif expr.IsBVUGT then x.DecodeBoolExpr cm OperationType.Greater_Un expr - elif expr.IsBVSGE then x.DecodeBoolExpr cm OperationType.GreaterOrEqual expr - elif expr.IsBVUGE then x.DecodeBoolExpr cm OperationType.GreaterOrEqual_Un expr - elif expr.IsBVSLT then x.DecodeBoolExpr cm OperationType.Less expr - elif expr.IsBVULT then x.DecodeBoolExpr cm OperationType.Less_Un expr - elif expr.IsBVSLE then x.DecodeBoolExpr cm OperationType.LessOrEqual expr - elif expr.IsBVULE then x.DecodeBoolExpr cm 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 @@ -767,7 +768,7 @@ module internal Z3 = 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 cm 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 -> @@ -775,19 +776,19 @@ module internal Z3 = | HeapAddressSource(StackReading(key)) -> let refinedExpr = m.Eval(kvp.Value.expr, false) let t = key.TypeOfLocation - let addr = refinedExpr |> x.DecodeConcreteHeapAddress cm 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 cm 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 cm 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) | _ -> ()) @@ -798,9 +799,7 @@ module internal Z3 = let typ = TypeOf term (key, Some term, typ)) Memory.NewStackFrame state None (List.ofSeq frame) - - let defaultValues = Dictionary() - + let concreteAllocator typ addr = if VectorTime.less addr VectorTime.zero then state.allocatedTypes <- PersistentDict.add addr (ConcreteType typ) state.allocatedTypes @@ -821,12 +820,12 @@ module internal Z3 = if fields.IsEmpty then region.TypeOfLocation else fields.Head.typ - let getValueAndWrite (arr : Expr) addr = + let getValueAndWrite (arr : Expr) cmAllocate addr = let value = if Types.IsValueType typeOfLocation then - x.Decode cm typeOfLocation (Array.last arr.Args) + x.Decode state typeOfLocation cmAllocate (Array.last arr.Args) else - let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress cm typeOfLocation + let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress state typeOfLocation cmAllocate HeapRef (address |> ConcreteHeapAddress) typeOfLocation let states = Memory.Write state (Ref addr) value assert(states.Length = 1 && states.[0] = state) @@ -839,23 +838,23 @@ module internal Z3 = | ArrayLowerBound _ -> symbolicProcessor addr | _ -> mixedProcessor addr // may contain symbolic and concrete writes - let writeSymbolic arr = writeHelper (getValueAndWrite arr) (fun _ -> ()) - let writeMixed arr = writeHelper (fun _ -> ()) (getValueAndWrite arr) + 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 cm typeOfLocation arr.Args.[0] + if Types.IsValueType typeOfLocation then x.Decode state typeOfLocation false arr.Args.[0] else - let addr = x.DecodeConcreteHeapAddress cm typeOfLocation arr.Args.[0] + let addr = x.DecodeConcreteHeapAddress state typeOfLocation false arr.Args.[0] // concreteAllocator typeOfLocation addr HeapRef (addr |> ConcreteHeapAddress) typeOfLocation x.WriteDictOfValueTypes defaultValues region fields region.TypeOfLocation constantValue else if arr.IsStore then assert(arr.Args.Length >= 3) parseArray arr.Args.[0] - let addr = x.DecodeMemoryKey cm region arr.Args.[1..arr.Args.Length - 2] + let addr = x.DecodeMemoryKey state region (not isSymbolic) arr.Args.[1..arr.Args.Length - 2] // concreteAllocator typeOfLocation addr if isSymbolic then writeSymbolic arr addr From a28286f5eeeeb7619a707c37a0fa460d565aee44 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Wed, 23 Nov 2022 17:02:53 +0300 Subject: [PATCH 20/25] Concrete allocation fix --- VSharp.Solver/Z3.fs | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 10768c310..f97bf001a 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -134,6 +134,19 @@ module internal Z3 = if cm.Contains addr then Memory.Unmarshall state addr raise e + 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 + | _ -> internalfail "Unexpected exception in object creation" + // ------------------------------- Encoding: primitives ------------------------------- type private Z3Builder(ctx : Context) = @@ -655,13 +668,15 @@ module internal Z3 = encodingCache.heapAddresses.Remove((charArray, expr)) |> ignore encodingCache.heapAddresses.Add((typ, expr), result.Value) // strings are filled symbolically - if cm.Contains result.Value then cm.Remove result.Value + 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) = @@ -763,7 +778,7 @@ module internal Z3 = let subst = Dictionary() let stackEntries = Dictionary() let state = {Memory.EmptyState() with complete = true} - let cm = state.concreteMemory + defaultValues.Clear() encodingCache.t2e |> Seq.iter (fun kvp -> match kvp.Key with | {term = Constant(_, StructFieldChain(fields, StackReading(key)), t)} as constant -> @@ -800,18 +815,6 @@ module internal Z3 = (key, Some term, typ)) Memory.NewStackFrame state None (List.ofSeq frame) - let concreteAllocator typ addr = - 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 - | _ -> internalfail "Unexpected exception in object creation" - let processRegionConstraints isSymbolic (kvp : KeyValuePair<(regionSort * fieldId list), ArrayExpr>) = let constant = kvp.Value let arr = m.Eval(constant, false) @@ -848,14 +851,12 @@ module internal Z3 = if Types.IsValueType typeOfLocation then x.Decode state typeOfLocation false arr.Args.[0] else let addr = x.DecodeConcreteHeapAddress state typeOfLocation false arr.Args.[0] - // concreteAllocator typeOfLocation addr HeapRef (addr |> ConcreteHeapAddress) typeOfLocation x.WriteDictOfValueTypes defaultValues region fields region.TypeOfLocation constantValue else if arr.IsStore then assert(arr.Args.Length >= 3) parseArray arr.Args.[0] let addr = x.DecodeMemoryKey state region (not isSymbolic) arr.Args.[1..arr.Args.Length - 2] - // concreteAllocator typeOfLocation addr if isSymbolic then writeSymbolic arr addr else writeMixed arr addr @@ -874,7 +875,7 @@ module internal Z3 = encodingCache.heapAddresses |> Seq.iter (fun kvp -> let typ, _ = kvp.Key let addr = kvp.Value - concreteAllocator typ addr + concreteAllocator state defaultValues typ addr ) // Process stores From 2a74a37e288201b48307a454722fd7c7c45a904e Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Thu, 24 Nov 2022 13:37:13 +0300 Subject: [PATCH 21/25] Fix incorrect use of unmarshalling --- VSharp.Solver/Z3.fs | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index f97bf001a..3d71f2f90 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -103,9 +103,9 @@ module internal Z3 = 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 - | _ -> () + | {term = HeapRef({term = ConcreteHeapAddress(a)}, _)} -> + cm.AddDep a addr + | _ -> () let value = result.Value.Value |> unboxConcrete' |> Option.get Array.fill arr value | _ when typ = typeof -> @@ -122,16 +122,18 @@ module internal Z3 = 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 | _ -> () - let value = result.Value.Value |> unboxConcrete' |> Option.get cm.WriteClassField addr fid value ) with | :? MemberAccessException as e -> // Could not create an instance - if cm.Contains addr then Memory.Unmarshall state addr + // when objects are created, the are only filled with defaults + // Careful: the use of unmarshalling here is incorrect + if cm.Contains addr then cm.Remove addr raise e let concreteAllocator state defaultValues typ addr = @@ -778,7 +780,7 @@ module internal Z3 = let subst = Dictionary() let stackEntries = Dictionary() let state = {Memory.EmptyState() with complete = true} - defaultValues.Clear() + let cm = state.concreteMemory encodingCache.t2e |> Seq.iter (fun kvp -> match kvp.Key with | {term = Constant(_, StructFieldChain(fields, StackReading(key)), t)} as constant -> @@ -830,6 +832,14 @@ module internal Z3 = 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) @@ -884,6 +894,7 @@ module internal Z3 = state.startingTime <- [encodingCache.lastSymbolicAddress - 1] state.model <- PrimitiveModel subst encodingCache.heapAddresses.Clear() + defaultValues.Clear() StateModel(state, typeModel.CreateEmpty()) From 3c5d8c70dc86a30da3c33dccbdd7b995b16e75ff Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Thu, 24 Nov 2022 13:58:13 +0300 Subject: [PATCH 22/25] style and typo fixes tmp --- VSharp.InternalCalls/Type.fs | 3 +-- VSharp.SILI.Core/API.fs | 2 +- VSharp.SILI.Core/ConcreteMemory.fs | 10 +++++----- VSharp.Solver/Z3.fs | 9 +-------- VSharp.Utils/MemoryGraph.fs | 25 ++++++++++++++----------- 5 files changed, 22 insertions(+), 27 deletions(-) diff --git a/VSharp.InternalCalls/Type.fs b/VSharp.InternalCalls/Type.fs index 61859f6f7..c1caf51c4 100644 --- a/VSharp.InternalCalls/Type.fs +++ b/VSharp.InternalCalls/Type.fs @@ -43,8 +43,7 @@ module internal Type = List.singleton (typeRef, state) | _ -> __notImplemented__() // TypeOfMethod state (Types.FromDotNetType state t) - // TODO: restore it after rewriting marshaling/ - // unmarshaling + // TODO: restore it after rewriting marshaling/unmarshaling // __notImplemented__() let GetAssembly (state : state) (args : term list) : (term * state) list = diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index 2edc58ecf..9f18a4f0d 100644 --- a/VSharp.SILI.Core/API.fs +++ b/VSharp.SILI.Core/API.fs @@ -467,7 +467,7 @@ module API = let StringFromReplicatedChar state string char length = let cm = state.concreteMemory let concreteChar = Memory.tryTermToObj state (fun _ _ -> ()) char - let concreteLen = Memory.tryTermToObj state (fun _ _ -> ()) length + 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/ConcreteMemory.fs b/VSharp.SILI.Core/ConcreteMemory.fs index cd2bf7bc9..75342a24d 100644 --- a/VSharp.SILI.Core/ConcreteMemory.fs +++ b/VSharp.SILI.Core/ConcreteMemory.fs @@ -100,8 +100,10 @@ type public ConcreteMemory private (physToVirt, virtToPhys, dependencies) = virtToPhys[address] <- physicalAddress member private x.getDepsList ds = + // TODO: rewrite it more effectively let ds' = ds |> Set.ofList |> Set.toList - let ds'' = List.collect (fun a -> if dependencies.ContainsKey(a) then a::dependencies[a] else [a]) 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'' @@ -157,7 +159,6 @@ type public ConcreteMemory private (physToVirt, virtToPhys, dependencies) = assert(virtToPhys.ContainsKey address |> not) let physicalAddress = {object = obj} virtToPhys.Add(address, physicalAddress) - // dependencies.Add(address, []) if obj = String.Empty then physToVirt[physicalAddress] <- address else physToVirt.Add(physicalAddress, address) @@ -223,8 +224,7 @@ type public ConcreteMemory private (physToVirt, virtToPhys, dependencies) = let physAddress = {object = string} physToVirt[physAddress] <- stringAddress - // ------------------------------- Add deps ----------------------------- - + // ------------------------------- Dependencies ------------------------- override x.AddDep virtAddr1 virtAddr2 = let value = if dependencies.ContainsKey virtAddr1 then virtAddr2::dependencies[virtAddr1] else [virtAddr2] dependencies[virtAddr1] <- value @@ -237,6 +237,6 @@ type public ConcreteMemory private (physToVirt, virtToPhys, dependencies) = override x.Remove address = let toRemove = x.getDepsList [address] let removed = toRemove |> List.map (fun a -> - dependencies.Remove a + dependencies.Remove a |> ignore virtToPhys.Remove a) |> List.forall id assert removed diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 3d71f2f90..fcff2f69c 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -10,14 +10,6 @@ open VSharp.Core.SolverInteraction open Logger module internal Z3 = - [] - type OptionalBuilder = - member __.Bind(opt, binder) = Option.bind binder opt - member __.Return(value) = Some value - member __.ReturnFrom(value) = value - member __.Zero() = None - member __.Using(resource : #System.IDisposable, binder) = let result = binder resource in resource.Dispose(); result - let opt = OptionalBuilder() // ------------------------------- Exceptions ------------------------------- type EncodingException(msg : string) = @@ -840,6 +832,7 @@ module internal Z3 = // 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) diff --git a/VSharp.Utils/MemoryGraph.fs b/VSharp.Utils/MemoryGraph.fs index 779409ba8..a2a7051c0 100644 --- a/VSharp.Utils/MemoryGraph.fs +++ b/VSharp.Utils/MemoryGraph.fs @@ -205,7 +205,6 @@ 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())) member private x.EncodeArray (arr : Array) = let contents = @@ -243,11 +242,17 @@ 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) = match obj with @@ -274,14 +279,12 @@ and MemoryGraph(repr : memoryRepr, mocker : ITypeMockSerializer, createCompactRe | None -> let i = x.ReserveRepresentation() let r : referenceRepr = {index = i} - sourceObjects.[i] <- obj - objReprs.[i] <- r + x.Bind obj r (Some i) |> ignore let repr = match t with | _ when t.IsArray -> x.EncodeArray (obj :?> Array) | _ -> x.EncodeStructure obj - objReprs.[i] <- repr - i + x.Bind obj repr (Some i) let reference : referenceRepr = {index = idx} reference :> obj, Some idx @@ -289,7 +292,7 @@ and MemoryGraph(repr : memoryRepr, mocker : ITypeMockSerializer, createCompactRe 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} From 9dd9d08078673af1212f15e2c291855e39d4b69c Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Thu, 24 Nov 2022 16:28:52 +0300 Subject: [PATCH 23/25] fix type is not supported object creation error --- VSharp.Solver/Z3.fs | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index fcff2f69c..6f9ac43ab 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -122,11 +122,13 @@ module internal Z3 = cm.WriteClassField addr fid value ) with - | :? MemberAccessException as e -> // Could not create an instance - // when objects are created, the are only filled with defaults - // Careful: the use of unmarshalling here is incorrect - if cm.Contains addr then cm.Remove addr - raise e + // 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 @@ -138,7 +140,7 @@ module internal Z3 = 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 + | :? ArgumentException -> () // Could not unbox concrete ot type is not supported | _ -> internalfail "Unexpected exception in object creation" // ------------------------------- Encoding: primitives ------------------------------- From 2de9fc5371b3cae688479fd117d633f76251006e Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Thu, 24 Nov 2022 19:36:59 +0300 Subject: [PATCH 24/25] fixed creation of concrete empty arrays --- VSharp.TestRenderer/CodeRenderer.cs | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) 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; } From 682853d784441deddf9b1f6fb17d8adb00c1ff83 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Thu, 24 Nov 2022 21:38:51 +0300 Subject: [PATCH 25/25] fixed RenderArray in TestRenderer --- VSharp.TestRenderer/MethodRenderer.cs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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)