From 636dbaae33fa4cc16434a6e6f8315391b81043c7 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Wed, 10 Apr 2024 16:41:50 +0300 Subject: [PATCH 1/8] [fix] fixed concrete memory --- VSharp.SILI.Core/ConcreteMemory.fs | 34 ++++++++++++------------------ 1 file changed, 13 insertions(+), 21 deletions(-) diff --git a/VSharp.SILI.Core/ConcreteMemory.fs b/VSharp.SILI.Core/ConcreteMemory.fs index 74ed514a7..b66efc1d6 100644 --- a/VSharp.SILI.Core/ConcreteMemory.fs +++ b/VSharp.SILI.Core/ConcreteMemory.fs @@ -30,18 +30,6 @@ type private ChildLocation = assert x.Type.IsValueType { x with structFields = fieldId :: x.structFields } - member x.Includes(childKind : ChildKind) = x.childKind = childKind - - member x.Includes(childLoc : ChildLocation) = - x.childKind = childLoc.childKind - && - let structFields = x.structFields - let otherStructFields = childLoc.structFields - let length = List.length structFields - let otherLength = List.length otherStructFields - length = otherLength && otherStructFields = structFields - || length > otherLength && otherStructFields = List.skip (length - otherLength) structFields - type private Cell = | Concrete of physicalAddress | Symbolic @@ -122,17 +110,15 @@ type public ConcreteMemory private (physToVirt, virtToPhys, children, parents, c assert(parent.object <> null) let childObj = child.object let childIsNull = childObj = null + let childType = childLoc.Type if childIsNull && update then + assert(not childType.IsValueType || TypeUtils.isNullable childType) let exists, childDict = children.TryGetValue parent - if exists then - for KeyValue(childLoc, _) in childDict do - if childLoc.Includes childLoc then - childDict.Remove childLoc |> ignore + if exists then childDict.Remove childLoc |> ignore elif not childIsNull then - let t = childLoc.Type - if t.IsValueType then + if childType.IsValueType then assert(childObj :? ValueType) - let fields = Reflection.fieldsOf false t + let fields = Reflection.fieldsOf false childType for fieldId, fieldInfo in fields do if Reflection.isReferenceOrContainsReferences fieldId.typ then let child = { object = fieldInfo.GetValue childObj } @@ -531,6 +517,13 @@ type public ConcreteMemory private (physToVirt, virtToPhys, children, parents, c let removed = virtToPhys.Remove address assert removed x.RemoveFromFullyConcretesRec phys + x.MarkSymbolic phys + + member private x.MarkSymbolic phys = + let exists, parentDict = parents.TryGetValue phys + if exists then + for KeyValue(parent, childKind) in parentDict do + children[parent][childKind] <- Symbolic member private x.RemoveFromFullyConcretesRec phys = let removed = HashSet() @@ -543,6 +536,5 @@ type public ConcreteMemory private (physToVirt, virtToPhys, children, parents, c fullyConcretes.Remove child |> ignore let exists, parentDict = parents.TryGetValue child if exists then - for KeyValue(parent, childKind) in parentDict do - children[parent][childKind] <- Symbolic + for KeyValue(parent, _) in parentDict do queue.Enqueue parent From a44e93bcffefca46089dad04741561c0ef878ea2 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 2 May 2024 15:37:18 +0300 Subject: [PATCH 2/8] [fix] fixed unsafe operations - fixed unsafe operations - added style fixes --- VSharp.SILI.Core/Memory.fs | 38 +++++++------------ VSharp.SILI.Core/MemoryRegion.fs | 30 +++++++++------ VSharp.SILI.Core/Substitution.fs | 4 +- VSharp.SILI.Core/Terms.fs | 46 ++++++++++++----------- VSharp.Solver/Z3.fs | 38 +++++++++---------- VSharp.Test/Tests/Lists.cs | 2 +- VSharp.Test/Tests/Unsafe.cs | 53 +++++++++++++++++++++++++++ VSharp.TestGenerator/TestGenerator.fs | 2 +- VSharp.Utils/Prelude.fs | 5 +++ 9 files changed, 136 insertions(+), 82 deletions(-) diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index d2a561367..26b967f11 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -325,7 +325,7 @@ module internal Memory = let writeStruct structTerm field value = commonWriteStruct None structTerm field value let guardedWriteStruct guard structTerm field value = commonWriteStruct guard structTerm field value - + let isSafeContextWrite actualType neededType = assert(neededType <> typeof) neededType = actualType @@ -972,44 +972,32 @@ module internal Memory = if isAlive then List.singleton address else List.empty - member private self.SliceTerm term startByte endByte pos stablePos = - match term.term with - | Slice(term, cuts) when stablePos -> - assert(List.isEmpty cuts |> not) - let _, _, p = List.head cuts - createSlice term ((startByte, endByte, p) :: cuts) - | Slice(term, cuts) -> - assert(List.isEmpty cuts |> not) - let _, _, p = List.head cuts - createSlice term ((startByte, endByte, add pos p) :: cuts) - | _ -> createSlice term (List.singleton (startByte, endByte, pos)) - // NOTE: returns list of slices // TODO: return empty if every slice is invalid - member private self.CommonReadTermUnsafe (reporter : IErrorReporter) term startByte endByte pos stablePos sightType = + member private self.CommonReadTermUnsafe (reporter : IErrorReporter) term startByte endByte pos isWrite sightType = match term.term, sightType with - | Slice _, _ -> - self.SliceTerm term startByte endByte pos stablePos |> List.singleton + | Slice(term, cuts), _ -> + createSlice term ((startByte, endByte, pos, isWrite) :: cuts) |> List.singleton | _, Some sightType when startByte = makeNumber 0 && let typ = typeOf term let size = internalSizeOf typ endByte = makeNumber size && typ = sightType -> List.singleton term - | Struct(fields, t), _ -> self.CommonReadStructUnsafe reporter fields t startByte endByte pos stablePos sightType + | Struct(fields, t), _ -> self.CommonReadStructUnsafe reporter fields t startByte endByte pos isWrite sightType | HeapRef _, _ | Ref _, _ | Ptr _, _ -> self.ReadAddressUnsafe reporter term startByte endByte - | Combined([t], _), _ -> self.CommonReadTermUnsafe reporter t startByte endByte pos stablePos sightType + | Combined([t], _), _ -> self.CommonReadTermUnsafe reporter t startByte endByte pos isWrite sightType | Combined(slices, _), _ -> - let readSlice part = self.CommonReadTermUnsafe reporter part startByte endByte pos stablePos sightType + let readSlice part = self.CommonReadTermUnsafe reporter part startByte endByte pos isWrite sightType List.collect readSlice slices | Concrete _, _ | Constant _, _ | Expression _, _ -> - self.SliceTerm term startByte endByte pos stablePos |> List.singleton + createSlice term (List.singleton (startByte, endByte, pos, isWrite)) |> List.singleton | Ite iteType, _ -> - let mapper term = self.CommonReadTermUnsafe reporter term startByte endByte pos stablePos sightType + let mapper term = self.CommonReadTermUnsafe reporter term startByte endByte pos isWrite sightType let mappedIte = iteType.mapValues mapper assert(List.forall (fun (_, list) -> List.length list = 1) mappedIte.branches && List.length mappedIte.elseValue = 1) mappedIte.mapValues List.head |> Merging.merge |> List.singleton @@ -1021,9 +1009,9 @@ module internal Memory = member private self.ReadTermPartUnsafe reporter term startByte endByte sightType = self.CommonReadTermUnsafe reporter term startByte endByte startByte true sightType - member private self.CommonReadStructUnsafe reporter fields structType startByte endByte pos stablePos sightType = + member private self.CommonReadStructUnsafe reporter fields structType startByte endByte pos isWrite sightType = let readField fieldId = fields[fieldId] - self.CommonReadFieldsUnsafe reporter readField false structType startByte endByte pos stablePos sightType + self.CommonReadFieldsUnsafe reporter readField false structType startByte endByte pos isWrite sightType member private self.ReadStructUnsafe reporter fields structType startByte endByte sightType = self.CommonReadStructUnsafe reporter fields structType startByte endByte (neg startByte) false sightType @@ -1069,10 +1057,10 @@ module internal Memory = | _ -> List.map getField allFields else List.empty - member private self.CommonReadFieldsUnsafe reporter readField isStatic (blockType : Type) startByte endByte pos stablePos sightType = + member private self.CommonReadFieldsUnsafe reporter readField isStatic (blockType : Type) startByte endByte pos isWrite sightType = let affectedFields = self.GetAffectedFields reporter readField isStatic blockType startByte endByte let readField (_, o, v, s, e) = - self.CommonReadTermUnsafe reporter v s e (add pos o) stablePos sightType + self.CommonReadTermUnsafe reporter v s e (add pos o) isWrite sightType List.collect readField affectedFields member private self.ReadFieldsUnsafe reporter readField isStatic (blockType : Type) startByte endByte sightType = diff --git a/VSharp.SILI.Core/MemoryRegion.fs b/VSharp.SILI.Core/MemoryRegion.fs index 471aa6144..bf8db5b3a 100644 --- a/VSharp.SILI.Core/MemoryRegion.fs +++ b/VSharp.SILI.Core/MemoryRegion.fs @@ -251,29 +251,36 @@ type heapArrayKey = let address' = mapTerm address let lowerBounds' = List.map mapTerm lowerBounds let upperBounds' = List.map mapTerm upperBounds - let y = if lowerBounds' = upperBounds' then OneArrayIndexKey(address', lowerBounds') - else RangeArrayIndexKey(address', lowerBounds', upperBounds') - reg', y + let key = + if lowerBounds' = upperBounds' then OneArrayIndexKey(address', lowerBounds') + else RangeArrayIndexKey(address', lowerBounds', upperBounds') + reg', key override x.IsUnion = isUnion x.Address override x.Unguard = match x with | OneArrayIndexKey(address, indices) -> - (address::indices, [True(), []]) ||> List.foldBack (fun index accTerms -> + let unGuard index accTerms = list { let! gt, terms = accTerms let! gi, i = Merging.unguardGvs index return (gi &&& gt, i::terms) - }) - |> List.map (fun (g, address::indices) -> (g, OneArrayIndexKey(address, indices))) + } + let createKey (g, addressWithIndices) = + match addressWithIndices with + | address::indices -> g, OneArrayIndexKey(address, indices) + | _ -> __unreachable__() + List.foldBack unGuard (address::indices) [True(), List.empty] + |> List.map createKey // TODO: if indices are unions of concrete values, then unguard them as well | RangeArrayIndexKey(address, lowerBounds, upperBounds) -> - let boundsPairs = (lowerBounds, upperBounds, [True(), [], []]) |||> List.foldBack2 (fun lb ub acc -> + let unGuard lb ub acc = list { let! g, accLbs, accUbs = acc let! gl, l = Merging.unguardGvs lb let! gu, u = Merging.unguardGvs ub return (g &&& gl &&& gu, l::accLbs, u::accUbs) - }) + } + let boundsPairs = List.foldBack2 unGuard lowerBounds upperBounds [True(), [], []] let addresses = Merging.unguardGvs address list { let! gAddr, addr = addresses @@ -420,7 +427,7 @@ type stackBufferIndexKey = override x.Map mapTerm _ _ reg = reg, {index = mapTerm x.index} override x.IsUnion = - match x.index.term with + match x.index.term with // TODO: #Roma | Ite {branches = branches; elseValue = e} -> List.forall (fst >> isConcrete) branches | _ -> false override x.Unguard = @@ -631,14 +638,13 @@ module private UpdateTree = PersistentDict.append modifiedTree disjoint |> Node List.foldBack writeOneKey disjointUnguardedKey tree - - let map (mapKey : 'reg -> 'key -> 'reg * 'key) mapValue (tree : updateTree<'key, 'value, 'reg>) predicate = + let map (mapKey : 'reg -> 'key -> 'reg * 'key) mapValue (tree : updateTree<'key, term, 'reg>) predicate = let mapper reg {key=k; value=v; guard = g; time = t} = let reg', k' = mapKey reg k let g' = Option.map mapValue g match g' with | Some g when g = False() -> None - | _ -> Some(reg', k'.Region, {key=k'; value=mapValue v; guard=g'; time=t}) + | _ -> Some(reg', k'.Region, {key = k'; value = mapValue v; guard = g'; time = t}) let splitWrite reg key tree = write reg key tree predicate RegionTree.choose mapper tree splitWrite diff --git a/VSharp.SILI.Core/Substitution.fs b/VSharp.SILI.Core/Substitution.fs index 892857407..7bea3e535 100644 --- a/VSharp.SILI.Core/Substitution.fs +++ b/VSharp.SILI.Core/Substitution.fs @@ -102,11 +102,11 @@ module Substitution = recur shift (fun shift' -> Ptr address' (typeSubst typ) shift' |> k)) | Slice(part, slices) -> - let substSlices (s, e, pos) k = + let substSlices (s, e, pos, isWrite) k = recur s (fun s' -> recur e (fun e' -> recur pos (fun pos' -> - k (s', e', pos')))) + k (s', e', pos', isWrite)))) Cps.List.mapk substSlices slices (fun slices' -> recur part (fun part' -> createSlice part' slices' |> k)) diff --git a/VSharp.SILI.Core/Terms.fs b/VSharp.SILI.Core/Terms.fs index 756fe8b27..acd2084e2 100644 --- a/VSharp.SILI.Core/Terms.fs +++ b/VSharp.SILI.Core/Terms.fs @@ -16,8 +16,8 @@ type IMethod = abstract ReturnType : Type abstract DeclaringType : Type abstract ReflectedType : Type - abstract Parameters : Reflection.ParameterInfo[] - abstract LocalVariables : IList + abstract Parameters : ParameterInfo[] + abstract LocalVariables : IList abstract HasThis : bool abstract HasParameterOnStack : bool abstract IsConstructor : bool @@ -29,13 +29,13 @@ type IMethod = abstract ResolveOverrideInType : Type -> IMethod abstract CanBeOverriddenInType : Type -> bool abstract IsImplementedInType : Type -> bool - abstract MethodBase : System.Reflection.MethodBase + abstract MethodBase : MethodBase [] type stackKey = | ThisKey of IMethod - | ParameterKey of Reflection.ParameterInfo - | LocalVariableKey of Reflection.LocalVariableInfo * IMethod + | ParameterKey of ParameterInfo + | LocalVariableKey of LocalVariableInfo * IMethod | TemporaryLocalVariableKey of Type * int override x.ToString() = match x with @@ -125,7 +125,7 @@ type termNode = | Ref of address // NOTE: use ptr only in case of reinterpretation: changed sight type or address arithmetic, otherwise use ref instead | Ptr of pointerBase * Type * term // base address * sight type * offset (in bytes) - | Slice of term * list // what term to slice * list of slices (start byte * end byte * position inside combine) + | Slice of term * list // what term to slice * list of slices (start byte * end byte * position inside combine * is write) | Ite of iteType override x.ToString() = @@ -204,7 +204,7 @@ type termNode = | Ptr(StaticLocation t, typ, shift) -> $"(StaticsPtr {t} as {typ}, offset = {shift})" |> k | Slice(term, slices) -> - let slices = List.map (fun (s, e, _) -> $"[{s} .. {e}]") slices |> join ", " + let slices = List.map (fun (s, e, _, _) -> $"[{s} .. {e}]") slices |> join ", " $"Slice({term}, {slices})" |> k and fieldsToString indent fields = @@ -310,7 +310,7 @@ and and delegateInfo = { - methodInfo : System.Reflection.MethodInfo + methodInfo : MethodInfo target : term delegateType : Type } @@ -371,7 +371,7 @@ module internal Terms = let makeNullPtr typ = Ptr (HeapLocation(zeroAddress(), typ)) typ (makeNumber 0) - + let True() = Concrete (box true) typeof let IteAsGvs iteType = iteType.branches @ [(True(), iteType.elseValue)] @@ -434,8 +434,8 @@ module internal Terms = | Struct(fields, _) -> fields | term -> internalfail $"struct or class expected, {term} received" - let private typeOfIte (getType : 'a -> Type) (iteType : iteType) = - let types = iteType.mapValues getType + let private typeOfIte (getType : term -> Type) (iteType : iteType) = + let types = iteType.mapValues getType match types with | {branches = []; elseValue = _} -> __unreachable__() | {branches = branches; elseValue = elset} -> @@ -443,7 +443,7 @@ module internal Terms = List.forall (snd >> (=) elset) branches if allSame then elset else - branches |> List.fold (fun acc (g, t) -> if t.IsAssignableTo acc then acc else t) elset + branches |> List.fold (fun acc (_, t) -> if t.IsAssignableTo acc then acc else t) elset let commonTypeOf getType term = match term.term with @@ -536,7 +536,7 @@ module internal Terms = let castConcrete (concrete : obj) (t : Type) = let actualType = getTypeOfConcrete concrete let functionIsCastedToMethodPointer () = - typedefof.IsAssignableFrom(actualType) && typedefof.IsAssignableFrom(t) + typedefof.IsAssignableFrom(actualType) && typedefof.IsAssignableFrom(t) if actualType = t then Concrete concrete t elif actualType = typeof && t = typeof then @@ -910,7 +910,7 @@ module internal Terms = let mutable solidPartSize = 0 for slice in sliceTerms do match slice.term with - | Slice(term, [{term = Concrete(s, _)}, {term = Concrete(e, _)}, {term = Concrete(pos, _)}]) -> + | Slice(term, [{term = Concrete(s, _)}, {term = Concrete(e, _)}, {term = Concrete(pos, _)}, _]) -> let o = slicingTerm term let sliceBytes = concreteToBytes o let sliceLength = Array.length sliceBytes @@ -945,7 +945,7 @@ module internal Terms = and private allSlicesAreConcrete slices = let rec sliceIsConcrete t = match t.term with - | Slice({term = Concrete _}, [({term = Concrete _}, {term = Concrete _}, {term = Concrete _})]) + | Slice({term = Concrete _}, [{term = Concrete _}, {term = Concrete _}, {term = Concrete _}, _]) | Concrete _ -> true | Combined(slices, _) -> allSlicesAreConcrete slices | _ -> false @@ -963,10 +963,11 @@ module internal Terms = let mutable left = 0 let mutable right = termSize let mutable position = 0 + let mutable resultIsWrite = false let mutable isValid = true let narrowed () = left > 0 || right < termSize || position <> 0 - let narrow (l, r, p as current) _ = + let narrow (l, r, p, isWrite as current) _ = let wereConcrete = List.isEmpty cuts match l.term, r.term, p.term with // TODO: need to simplify after symbolic elements? @@ -980,7 +981,8 @@ module internal Terms = let sliceRight = min (r - position) right let sliceSize = sliceRight - sliceLeft right <- min (left + sliceSize) right - position <- max p 0 + position <- if isWrite then max p position else max (position + p) 0 + resultIsWrite <- isWrite if right - left > 0 then assert(left >= 0 && left < termSize) assert(right > 0 && right <= termSize) @@ -989,7 +991,7 @@ module internal Terms = isValid <- false // Case, when concrete cut is not whole term | _ when wereConcrete && narrowed() -> - let cut = (makeNumber left, makeNumber right, makeNumber position) + let cut = (makeNumber left, makeNumber right, makeNumber position, resultIsWrite) cuts <- current :: List.singleton cut | _ -> cuts <- current :: cuts @@ -997,7 +999,7 @@ module internal Terms = match cuts with | _ when not isValid -> Slice term List.empty | [] when narrowed() -> - let cut = (makeNumber left, makeNumber right, makeNumber position) + let cut = (makeNumber left, makeNumber right, makeNumber position, resultIsWrite) Slice term (List.singleton cut) | [] -> assert(left = 0 && right = termSize && position = 0) @@ -1030,7 +1032,7 @@ module internal Terms = valueTypeToTerm obj t | [{term = Slice(p, cuts)}] -> match cuts with - | [({term = Concrete(s, _)}, {term = Concrete(e, _)}, {term = Concrete(pos, _)})] -> + | [{term = Concrete(s, _)}, {term = Concrete(e, _)}, {term = Concrete(pos, _)}, _] -> let s = convert s typeof :?> int let e = convert e typeof :?> int let pos = convert pos typeof :?> int @@ -1075,7 +1077,7 @@ module internal Terms = foldList folder gs state (fun state -> foldList folder vs state k) | Slice(t, slices) -> - let foldSlice state (s, e, pos) k = + let foldSlice state (s, e, pos, _) k = doFold folder state s (fun state -> doFold folder state e (fun state -> doFold folder state pos k)) @@ -1132,7 +1134,7 @@ module internal Terms = and private foldFields isStatic folder acc typ = let fields = Reflection.fieldsOf isStatic typ - let addField heap (fieldId, fieldInfo : Reflection.FieldInfo) = + let addField heap (fieldId, fieldInfo : FieldInfo) = folder heap fieldInfo fieldId fieldInfo.FieldType FSharp.Collections.Array.fold addField acc fields diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 35a4385ee..eab420702 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -149,7 +149,7 @@ module internal Z3 = type private Z3Builder(ctx : Context) = let mutable encodingCache = freshCache() - let emptyState = Memory.EmptyIsolatedState() + let emptyState = EmptyIsolatedState() let mutable maxBufferSize = 128 let typeOfLocation (regionSort : regionSort) (path : path) = @@ -732,7 +732,7 @@ module internal Z3 = assert(termSortSize % 8u = 0u && termSortSize > 0u) let zero = ctx.MkBV(0, termSortSize) let sizeExpr = ctx.MkBV(termSortSize / 8u, termSortSize) - let addBounds (startByte, endByte, pos) (assumptions, startExpr, sizeExpr, position) = + let addBounds (startByte, endByte, pos, isWrite) (assumptions, startExpr, sizeExpr, position) = let assumptions = assumptions @ startByte.assumptions @ endByte.assumptions @ pos.assumptions let startByte = x.ExtractOrExtend (startByte.expr :?> BitVecExpr) termSortSize let endByte = x.ExtractOrExtend (endByte.expr :?> BitVecExpr) termSortSize @@ -744,7 +744,7 @@ module internal Z3 = let sliceSize = x.MkBVSub(right, left) let newLeft = x.MkBVAdd(startExpr, left) let newRight = x.Min (x.MkBVAdd(newLeft, sliceSize)) sizeExpr - let newPos = x.Max pos zero + let newPos = if isWrite then x.Max pos position else x.Max (x.MkBVAdd(position, pos)) zero assumptions, newLeft, newRight, newPos List.foldBack addBounds cuts (assumptions, zero, sizeExpr, zero) @@ -772,18 +772,17 @@ module internal Z3 = member private x.EncodeSlice slice = match slice.term with | Slice(term, cuts) -> - let slices = List.map (fun (s, e, pos) -> x.EncodeTerm s, x.EncodeTerm e, x.EncodeTerm pos) cuts + let slices = List.map (fun (s, e, pos, isWrite) -> x.EncodeTerm s, x.EncodeTerm e, x.EncodeTerm pos, isWrite) cuts x.EncodeTerm term, slices | Ite {branches = ite; elseValue = e} -> let extractTerm slice = match slice.term with | Slice(t, _) -> t | _ -> slice - let encodedTerm = {branches = List.map (fun (g, s) -> (g, extractTerm s)) ite; elseValue = extractTerm e} |> x.EncodeIte - + let encodedTerm = x.EncodeIte {branches = List.map (fun (g, s) -> (g, extractTerm s)) ite; elseValue = extractTerm e} let extractCuts slice = match slice.term with - | Slice(t, cuts) -> cuts + | Slice(_, cuts) -> cuts | _ -> List.empty let iteCuts = List.map (fun (_, s) -> extractCuts s) ite let elseCuts = extractCuts e @@ -796,11 +795,12 @@ module internal Z3 = let branches = itePart |> List.map (fun (g, p) -> (g, proj p)) let elseChar = proj elsePart {branches = branches; elseValue = elseChar} |> x.EncodeIte - let encodeSlicePart itePart elsePart = - let encodedStarts = encodeCutChar fst3 itePart elsePart - let encodedEnds = encodeCutChar snd3 itePart elsePart - let encodedPoss = encodeCutChar thd3 itePart elsePart - (encodedStarts, encodedEnds, encodedPoss) + let encodeSlicePart itePart (_, _, _, isWrite as elsePart) = + let encodedStarts = encodeCutChar fst4 itePart elsePart + let encodedEnds = encodeCutChar snd4 itePart elsePart + let encodedPoss = encodeCutChar thd4 itePart elsePart + assert(List.forall (fun (_, (_, _, _, isWrite')) -> isWrite = isWrite') itePart) + (encodedStarts, encodedEnds, encodedPoss, isWrite) let encodedSliceParts = List.map2 encodeSlicePart iteSliceParts elseCuts encodedTerm, encodedSliceParts | _ -> x.EncodeTerm slice, List.empty @@ -869,7 +869,7 @@ module internal Z3 = (x.MkITE(guard :?> BoolExpr, value, prevIte), assumptions) |> k Cps.List.foldrk constructUnion (elseValue, []) iteType.branches (fun (ite, assumptions) -> {expr = ite; assumptions = assumptions}) - + member private x.EncodeExpression term op args typ = encodingCache.Get(term, fun () -> match op with @@ -987,13 +987,13 @@ module internal Z3 = match path with | StructFieldPart field -> assert(IsStruct term) - Memory.ReadField emptyState term field + ReadField emptyState term field | PointerAddress -> assert(IsPtr term) - Memory.ExtractAddress term + ExtractAddress term | PointerOffset -> assert(IsPtr term) - Memory.ExtractPointerOffset term + ExtractPointerOffset term let value = path.Fold readFieldIfNeed record.value let valueExpr = specializeWithKey value readKey record.key |> x.EncodeTerm let assumptions = List.append assumptions valueExpr.assumptions @@ -1319,10 +1319,10 @@ module internal Z3 = | [PointerOffset], Ptr(HeapLocation(address, t), sightType, _) -> Ptr (HeapLocation(address, t)) sightType value | [StructFieldPart field], Struct _ -> - Memory.WriteStructField term field value + WriteStructField term field value | StructFieldPart field :: parts, Struct(contents, _) -> let recurred = x.WriteByPath contents[field] value parts - Memory.WriteStructField term field recurred + WriteStructField term field recurred | StructFieldPart _ :: _, _ -> internalfail $"WriteByPath: expected structure, but got {term}" | PointerOffset :: parts, _ | PointerAddress :: parts, _ when List.isEmpty parts |> not -> @@ -1338,7 +1338,7 @@ module internal Z3 = let term = if exists then res else - let res = Memory.DefaultOf t |> ref + let res = DefaultOf t |> ref dict.Add(key, res) res term.Value <- x.WriteByPath term.Value value path.parts diff --git a/VSharp.Test/Tests/Lists.cs b/VSharp.Test/Tests/Lists.cs index 78d71aebb..7086d08bb 100644 --- a/VSharp.Test/Tests/Lists.cs +++ b/VSharp.Test/Tests/Lists.cs @@ -644,7 +644,7 @@ public static int TestSolvingCopy11(string[] a, int i, string[] b) return 3; } - [TestSvm(90)] + [Ignore("fix array memory region")] public static int ArrayAliasWrite(object[] o, string[] s, string str1, string str2) { if (o[42] == str1) diff --git a/VSharp.Test/Tests/Unsafe.cs b/VSharp.Test/Tests/Unsafe.cs index 2a2f40878..43eb61ab5 100644 --- a/VSharp.Test/Tests/Unsafe.cs +++ b/VSharp.Test/Tests/Unsafe.cs @@ -1008,5 +1008,58 @@ public static bool CheckUnsafeArrayCopy(int offset1, int offset2, int value) return true; } + + [TestSvm(100)] + public static bool CheckSpecificUnsafeArrayCopy(int offset1, int offset2, int value) + { + if (value == -1) + return CheckUnsafeArrayCopy(offset1, offset2, value); + if (value == Int32.MinValue) + return CheckUnsafeArrayCopy(offset1, offset2, value); + if (value == Int32.MinValue + 1) + return CheckUnsafeArrayCopy(offset1, offset2, value); + if (value == Int32.MaxValue) + return CheckUnsafeArrayCopy(offset1, offset2, value); + if (value == Int32.MaxValue - 1) + return CheckUnsafeArrayCopy(offset1, offset2, value); + + return false; + } + + [TestSvm(94)] + public static bool CheckUnsafeIntCopy(int value) + { + var copied = 0; + var pV = (byte*) &value; + var pC = (byte*) &copied; + for (var i = 0; i < sizeof(int); i++) + { + *pC = *pV; + pC++; + pV++; + } + + if (copied != value) + return false; + + return true; + } + + [TestSvm(100)] + public static bool CheckSpecificUnsafeIntCopy(int value) + { + if (value == -1) + return CheckUnsafeIntCopy(value); + if (value == Int32.MinValue) + return CheckUnsafeIntCopy(value); + if (value == Int32.MaxValue) + return CheckUnsafeIntCopy(value); + if (value == Int32.MinValue + 1) + return CheckUnsafeIntCopy(value); + if (value == Int32.MaxValue - 1) + return CheckUnsafeIntCopy(value); + + return false; + } } } diff --git a/VSharp.TestGenerator/TestGenerator.fs b/VSharp.TestGenerator/TestGenerator.fs index e77b20fd6..c1e8f49c1 100644 --- a/VSharp.TestGenerator/TestGenerator.fs +++ b/VSharp.TestGenerator/TestGenerator.fs @@ -335,7 +335,7 @@ module TestGenerator = for pi in parametersInfo do let arg = Memory.ReadArgument state pi let concreteArg = term2obj model state indices mockCache implementations test arg - test.AddArg (Array.head parametersInfo) concreteArg + test.AddArg pi concreteArg else for pi in parametersInfo do let value = diff --git a/VSharp.Utils/Prelude.fs b/VSharp.Utils/Prelude.fs index b4c0b2d2f..24415e6e7 100644 --- a/VSharp.Utils/Prelude.fs +++ b/VSharp.Utils/Prelude.fs @@ -50,6 +50,11 @@ module public Prelude = let inline public snd3 (_, y, _) = y let inline public thd3 (_, _, z) = z + let inline public fst4 (x, _, _, _) = x + let inline public snd4 (_, y, _, _) = y + let inline public thd4 (_, _, z, _) = z + let inline public fth4 (_, _, _, a) = a + let inline public appIfNotNull f lhs rhs = if lhs = null then rhs else f lhs From 1b557da2cd8e56ed62789dd319e601dc5e1cd501 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 9 May 2024 14:37:42 +0300 Subject: [PATCH 3/8] [style] fixed style --- VSharp.API/VSharpOptions.cs | 2 +- VSharp.Explorer/Explorer.fs | 1 - VSharp.Runner/RunnerProgram.cs | 1 - 3 files changed, 1 insertion(+), 3 deletions(-) diff --git a/VSharp.API/VSharpOptions.cs b/VSharp.API/VSharpOptions.cs index 60e9af2a2..91541e2e9 100644 --- a/VSharp.API/VSharpOptions.cs +++ b/VSharp.API/VSharpOptions.cs @@ -89,7 +89,7 @@ public readonly record struct VSharpOptions private const string DefaultOutputDirectory = ""; private const string DefaultRenderedTestsDirectory = ""; private const bool DefaultRenderTests = false; - private const SearchStrategy DefaultSearchStrategy = SearchStrategy.BFS; + private const SearchStrategy DefaultSearchStrategy = SearchStrategy.ExecutionTreeContributedCoverage; private const Verbosity DefaultVerbosity = Verbosity.Quiet; private const uint DefaultRecursionThreshold = 0u; private const ExplorationMode DefaultExplorationMode = ExplorationMode.Sili; diff --git a/VSharp.Explorer/Explorer.fs b/VSharp.Explorer/Explorer.fs index 8b166db8a..847c78dfc 100644 --- a/VSharp.Explorer/Explorer.fs +++ b/VSharp.Explorer/Explorer.fs @@ -75,7 +75,6 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let emptyState = Memory.EmptyIsolatedState() let interpreter = ILInterpreter() - do if options.visualize then DotVisualizer explorationOptions.outputDirectory :> IVisualizer |> Application.setVisualizer diff --git a/VSharp.Runner/RunnerProgram.cs b/VSharp.Runner/RunnerProgram.cs index 2fa6aaf31..f41e3515b 100644 --- a/VSharp.Runner/RunnerProgram.cs +++ b/VSharp.Runner/RunnerProgram.cs @@ -2,7 +2,6 @@ using System; using System.Collections.Generic; using System.CommandLine; -using System.CommandLine.Invocation; using System.Diagnostics; using System.IO; using System.Linq; From 9f0af4150925af49b26f71028846a014c2a1eda2 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Mon, 27 May 2024 23:59:59 +0300 Subject: [PATCH 4/8] [style] 'cilState.Write' returns 'Unit' --- VSharp.InternalCalls/Buffer.fs | 24 +++++++++++------------- VSharp.InternalCalls/Interlocked.fs | 11 +++++------ VSharp.InternalCalls/Object.fs | 14 +++++--------- VSharp.InternalCalls/Span.fs | 4 ++-- VSharp.InternalCalls/String.fs | 9 ++++----- VSharp.InternalCalls/Thread.fs | 3 ++- VSharp.InternalCalls/Unsafe.fs | 6 ++++-- VSharp.InternalCalls/Volatile.fs | 1 + VSharp.SILI/CILState.fs | 3 --- VSharp.SILI/Interpreter.fs | 24 ++++++++++++++---------- 10 files changed, 48 insertions(+), 51 deletions(-) diff --git a/VSharp.InternalCalls/Buffer.fs b/VSharp.InternalCalls/Buffer.fs index 7a91c07d1..704666eed 100644 --- a/VSharp.InternalCalls/Buffer.fs +++ b/VSharp.InternalCalls/Buffer.fs @@ -53,7 +53,7 @@ module internal Buffer = let checkDst (info, cilState : cilState) = match info with | Some (dstAddress : address) -> - let checkSrc (info, cilState : cilState) = + let checkSrc info (cilState : cilState) = match info with | Some (srcAddress : address) -> let dstType = lazy dstAddress.TypeOfLocation @@ -71,28 +71,26 @@ module internal Buffer = match dstAddress, srcAddress with | _ when allSafe() -> let value = cilState.Read (Ref srcAddress) - let cilStates = cilState.Write (Ref dstAddress) value - assert(List.length cilStates = 1) - List.head cilStates + cilState.Write (Ref dstAddress) value | _ when dstSafe.Value -> let ptr = Types.Cast (Ref srcAddress) (dstType.Value.MakePointerType()) let value = cilState.Read ptr - let cilStates = cilState.Write (Ref dstAddress) value - assert(List.length cilStates = 1) - List.head cilStates + cilState.Write (Ref dstAddress) value | _ when srcSafe.Value -> let value = cilState.Read (Ref srcAddress) let ptr = Types.Cast (Ref dstAddress) (srcType.Value.MakePointerType()) - let cilStates = cilState.Write ptr value - assert(List.length cilStates = 1) - List.head cilStates + cilState.Write ptr value | ArrayIndex(dstAddress, dstIndices, dstArrayType), ArrayIndex(srcAddress, srcIndices, srcArrayType) -> Copy dstAddress dstIndex dstIndices dstArrayType srcAddress srcIndex srcIndices srcArrayType state bytesCount - cilState // TODO: implement unsafe copy | _ -> internalfail $"CommonMemmove unexpected addresses {srcAddress}, {dstAddress}" - | None -> cilState - getAddress cilState src |> List.map checkSrc + | None -> () + let addressesWithStates = getAddress cilState src + let mutable resultCilStates = List.empty + for address, cilState in addressesWithStates do + checkSrc address cilState + resultCilStates <- cilState :: resultCilStates + resultCilStates | None -> cilState |> List.singleton getAddress cilState dst |> List.collect checkDst diff --git a/VSharp.InternalCalls/Interlocked.fs b/VSharp.InternalCalls/Interlocked.fs index fd76c946e..ef94766dc 100644 --- a/VSharp.InternalCalls/Interlocked.fs +++ b/VSharp.InternalCalls/Interlocked.fs @@ -1,7 +1,7 @@ namespace VSharp.System open global.System -open VSharp + open VSharp.Core open VSharp.Interpreter.IL open VSharp.Interpreter.IL.CilState @@ -11,10 +11,9 @@ module internal Interlocked = let exchange (interpreter : IInterpreter) (cilState : cilState) location value = let exchange (cilState : cilState) k = let currentValue = cilState.Read location - let cilStates = cilState.Write location value - for cilState in cilStates do - cilState.Push currentValue - k cilStates + cilState.Write location value + cilState.Push currentValue + List.singleton cilState |> k interpreter.NpeOrInvoke cilState location exchange id let commonCompareExchange (interpreter : IInterpreter) (cilState : cilState) location value compared = @@ -23,7 +22,7 @@ module internal Interlocked = let cilStates = cilState.StatedConditionalExecutionCIL (fun cilState k -> k (currentValue === compared, cilState)) - (fun cilState k -> k (cilState.Write location value)) + (fun cilState k -> k (cilState.Write location value; List.singleton cilState)) (fun cilState k -> k (List.singleton cilState)) id for cilState in cilStates do diff --git a/VSharp.InternalCalls/Object.fs b/VSharp.InternalCalls/Object.fs index bb7de1a0b..3e4ae82f5 100644 --- a/VSharp.InternalCalls/Object.fs +++ b/VSharp.InternalCalls/Object.fs @@ -41,12 +41,8 @@ module internal Object = else t let newObject = Memory.AllocateDefaultClass state t let fields = Reflection.fieldsOf false t - let copyField cilStates (field, _) = - let copyForState (cilState : cilState) = - let v = cilState.ReadField object field - cilState.WriteClassField newObject field v - List.collect copyForState cilStates - let cilStates = Array.fold copyField (List.singleton cilState) fields - for cilState in cilStates do - cilState.Push newObject - cilStates + for field, _ in fields do + let v = cilState.ReadField object field + cilState.WriteClassField newObject field v + cilState.Push newObject + List.singleton cilState diff --git a/VSharp.InternalCalls/Span.fs b/VSharp.InternalCalls/Span.fs index 6c4450ca6..de12e7991 100644 --- a/VSharp.InternalCalls/Span.fs +++ b/VSharp.InternalCalls/Span.fs @@ -137,6 +137,7 @@ module internal ReadOnlySpan = let span = cilState.Read this let initializedSpan = InitSpanStruct cilState span refToFirst length cilState.Write this initializedSpan + List.singleton cilState let CtorFromPtr (i : IInterpreter) (cilState : cilState) (args : term list) : cilState list = assert(List.length args = 4) @@ -237,8 +238,7 @@ module internal ReadOnlySpan = let arrayRef = Memory.AllocateConcreteObject state rawData arrayType let refToFirstElement = Memory.ReferenceArrayIndex state arrayRef [MakeNumber 0] None let count = MakeNumber rawData.Length - let cilStates = cilState.Write countRef count - assert(List.length cilStates = 1 && cilStates[0] = cilState) + cilState.Write countRef count cilState.Push refToFirstElement List.singleton cilState | _ -> internalfail $"GetSpanDataFrom: unexpected field handle {fieldHandleTerm} or type handle {typeHandleTerm}" diff --git a/VSharp.InternalCalls/String.fs b/VSharp.InternalCalls/String.fs index 96302afb4..6b79eeb86 100644 --- a/VSharp.InternalCalls/String.fs +++ b/VSharp.InternalCalls/String.fs @@ -47,11 +47,9 @@ module internal String = (length >>= zero) &&& (startIndex >>= zero) let copy (cilState : cilState) k = - let cilStates = cilState.WriteClassField this Reflection.stringLengthField length + cilState.WriteClassField this Reflection.stringLengthField length let bytesCount = Mul length (MakeNumber sizeof) - let memMove cilState = - Buffer.CommonMemmove cilState this None ptr (Some startIndex) bytesCount - List.collect memMove cilStates |> k + Buffer.CommonMemmove cilState this None ptr (Some startIndex) bytesCount |> k let checkPtr (cilState : cilState) k = cilState.StatedConditionalExecutionCIL (fun state k -> k (!!(IsBadRef ptr), state)) @@ -59,7 +57,8 @@ module internal String = (i.Raise i.ArgumentOutOfRangeException) k let emptyStringCase (cilState : cilState) k = - cilState.WriteClassField this Reflection.stringLengthField zero |> k + cilState.WriteClassField this Reflection.stringLengthField zero + List.singleton cilState |> k let checkLength (cilState : cilState) k = cilState.StatedConditionalExecutionCIL (fun state k -> k (length === zero, state)) diff --git a/VSharp.InternalCalls/Thread.fs b/VSharp.InternalCalls/Thread.fs index 0b12ca87e..ef7a1f805 100644 --- a/VSharp.InternalCalls/Thread.fs +++ b/VSharp.InternalCalls/Thread.fs @@ -33,7 +33,8 @@ module Thread = assert(List.length args = 2) let obj, resultRef = args[0], args[1] let success (cilState : cilState) k = - cilState.Write resultRef (True()) |> k + cilState.Write resultRef (True()) + List.singleton cilState |> k cilState.BranchOnNullCIL obj (interpreter.Raise interpreter.ArgumentNullException) success diff --git a/VSharp.InternalCalls/Unsafe.fs b/VSharp.InternalCalls/Unsafe.fs index ffca3f0bd..265fd97cc 100644 --- a/VSharp.InternalCalls/Unsafe.fs +++ b/VSharp.InternalCalls/Unsafe.fs @@ -92,14 +92,16 @@ module internal Unsafe = let typ = Helpers.unwrapType typ let castedPtr = Types.Cast ref (typ.MakePointerType()) let writeByPtr (cilState : cilState) k = - cilState.Write castedPtr value |> k + cilState.Write castedPtr value + List.singleton cilState |> k i.NpeOrInvoke cilState castedPtr writeByPtr id let WriteUnaligned (i : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 2) let ref, value = args[0], args[1] let writeByPtr (cilState : cilState) k = - cilState.Write ref value |> k + cilState.Write ref value + List.singleton cilState |> k i.NpeOrInvoke cilState ref writeByPtr id let SizeOf (_ : state) (args : term list) : term = diff --git a/VSharp.InternalCalls/Volatile.fs b/VSharp.InternalCalls/Volatile.fs index 6b09b02de..062c41c61 100644 --- a/VSharp.InternalCalls/Volatile.fs +++ b/VSharp.InternalCalls/Volatile.fs @@ -21,3 +21,4 @@ module Volatile = assert(List.length args = 3) let ref, value = args[1], args[2] cilState.Write ref value + List.singleton cilState diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs index da23dec7b..d7fc576cf 100644 --- a/VSharp.SILI/CILState.fs +++ b/VSharp.SILI/CILState.fs @@ -444,18 +444,15 @@ module CilState = member x.Write ref value = Memory.WriteUnsafe x.ErrorReporter.Value x.state ref value - List.singleton x member x.WriteClassField ref field value = Memory.WriteClassFieldUnsafe x.ErrorReporter.Value x.state ref field value - List.singleton x member x.WriteStructField term field value = Memory.WriteStructFieldUnsafe x.ErrorReporter.Value x.state term field value member x.WriteIndex term index value valueType = Memory.WriteArrayIndexUnsafe x.ErrorReporter.Value x.state term index value valueType - List.singleton x // -------------------------- Branching -------------------------- diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index cc781868d..32d540ce0 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -1309,7 +1309,8 @@ type ILInterpreter() as this = let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Stobj.Size) let store (cilState : cilState) k = let value = Types.Cast value typ - cilState.Write ref value |> k + cilState.Write ref value + List.singleton cilState |> k x.NpeOrInvokeStatementCIL cilState ref store id member x.LdFldWithFieldInfo (fieldInfo : FieldInfo) addressNeeded (cilState : cilState) = @@ -1342,7 +1343,8 @@ type ILInterpreter() as this = let reference = if TypeUtils.isPointer fieldInfo.DeclaringType then targetRef else Reflection.wrapField fieldInfo |> Memory.ReferenceField cilState.state targetRef - cilState.Write reference value |> k + cilState.Write reference value + List.singleton cilState |> k x.NpeOrInvokeStatementCIL cilState targetRef storeWhenTargetIsNotNull id member private x.LdElemCommon (typ : Type option) (cilState : cilState) arrayRef indices = @@ -1395,7 +1397,8 @@ type ILInterpreter() as this = let checkedStElem (cilState : cilState) (k : cilState list -> 'a) = let typeOfValue = TypeOf value let uncheckedStElem (cilState : cilState) (k : cilState list -> 'a) = - cilState.WriteIndex arrayRef indices value typ |> k + cilState.WriteIndex arrayRef indices value typ + List.singleton cilState |> k let checkTypeMismatch (cilState : cilState) (k : cilState list -> 'a) = let condition = if Types.IsValueType typeOfValue then True() @@ -1467,7 +1470,8 @@ type ILInterpreter() as this = let value, address = cilState.Pop2() let store (cilState : cilState) k = let value = valueCast value - cilState.Write address value |> k + cilState.Write address value + List.singleton cilState |> k x.NpeOrInvokeStatementCIL cilState address store id member x.BoxNullable (t : Type) (v : term) (cilState : cilState) : cilState list = @@ -2165,12 +2169,12 @@ type ILInterpreter() as this = | OpCodeValues.Xor -> (fun _ _ -> bitwiseOrBoolOperation OperationType.BitwiseXor OperationType.LogicalXor) |> fallThrough m offset cilState | OpCodeValues.Neg -> (fun _ _ -> performCILUnaryOperation OperationType.UnaryMinus) |> fallThrough m offset cilState | OpCodeValues.Not -> (fun _ _ -> bitwiseOrBoolNot) |> fallThrough m offset cilState - | OpCodeValues.Stloc -> stloc (fun ilBytes offset -> NumberCreator.extractUnsignedInt16 ilBytes (offset + Offset.from OpCodes.Stloc.Size) |> int) |> forkThrough m offset cilState - | OpCodeValues.Stloc_0 -> stloc (fun _ _ -> 0) |> forkThrough m offset cilState - | OpCodeValues.Stloc_1 -> stloc (fun _ _ -> 1) |> forkThrough m offset cilState - | OpCodeValues.Stloc_2 -> stloc (fun _ _ -> 2) |> forkThrough m offset cilState - | OpCodeValues.Stloc_3 -> stloc (fun _ _ -> 3) |> forkThrough m offset cilState - | OpCodeValues.Stloc_S -> stloc (fun ilBytes offset -> NumberCreator.extractUnsignedInt8 ilBytes (offset + Offset.from OpCodes.Stloc_S.Size) |> int) |> forkThrough m offset cilState + | OpCodeValues.Stloc -> stloc (fun ilBytes offset -> NumberCreator.extractUnsignedInt16 ilBytes (offset + Offset.from OpCodes.Stloc.Size) |> int) |> fallThrough m offset cilState + | OpCodeValues.Stloc_0 -> stloc (fun _ _ -> 0) |> fallThrough m offset cilState + | OpCodeValues.Stloc_1 -> stloc (fun _ _ -> 1) |> fallThrough m offset cilState + | OpCodeValues.Stloc_2 -> stloc (fun _ _ -> 2) |> fallThrough m offset cilState + | OpCodeValues.Stloc_3 -> stloc (fun _ _ -> 3) |> fallThrough m offset cilState + | OpCodeValues.Stloc_S -> stloc (fun ilBytes offset -> NumberCreator.extractUnsignedInt8 ilBytes (offset + Offset.from OpCodes.Stloc_S.Size) |> int) |> fallThrough m offset cilState | OpCodeValues.Starg -> starg (fun ilBytes offset -> NumberCreator.extractUnsignedInt16 ilBytes (offset + Offset.from OpCodes.Starg.Size) |> int) |> forkThrough m offset cilState | OpCodeValues.Starg_S -> starg (fun ilBytes offset -> NumberCreator.extractUnsignedInt8 ilBytes (offset + Offset.from OpCodes.Starg_S.Size) |> int) |> forkThrough m offset cilState | OpCodeValues.Ldc_I4 -> ldc (fun ilBytes offset -> NumberCreator.extractInt32 ilBytes (offset + Offset.from OpCodes.Ldc_I4.Size)) typedefof |> fallThrough m offset cilState From f6afecaac657b513ff7b43b8341d440919575433 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Sun, 27 Oct 2024 14:45:10 +0300 Subject: [PATCH 5/8] [fix] fixed generic method approximation --- VSharp.IL/MethodBody.fs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/VSharp.IL/MethodBody.fs b/VSharp.IL/MethodBody.fs index 5f80a459c..692f23fe7 100644 --- a/VSharp.IL/MethodBody.fs +++ b/VSharp.IL/MethodBody.fs @@ -84,7 +84,13 @@ type MethodWithBody internal (m : MethodBase) = let actualMethod = if not isCSharpInternalCall.Value then m - else Loader.CSharpImplementations[fullGenericMethodName.Value] + else + let method = Loader.CSharpImplementations[fullGenericMethodName.Value] + if method.IsGenericMethod && (m.DeclaringType.IsGenericType || m.IsGenericMethod) then + let _, genericArgs, _ = Reflection.generalizeMethodBase m + method.MakeGenericMethod(genericArgs) + else method + let methodBodyBytes = if isFSharpInternalCall.Value then null else actualMethod.GetMethodBody() From 9b21dd3909e79595cee527c31ddc1275c52677d1 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Sun, 27 Oct 2024 14:46:25 +0300 Subject: [PATCH 6/8] [style] fixed style --- VSharp.Explorer/Statistics.fs | 1 - VSharp.InternalCalls/IntPtr.fs | 1 - VSharp.SILI.Core/MemoryRegion.fs | 4 +++- VSharp.Solver/Z3.fs | 1 - 4 files changed, 3 insertions(+), 4 deletions(-) diff --git a/VSharp.Explorer/Statistics.fs b/VSharp.Explorer/Statistics.fs index f1921429e..f3a1c1037 100644 --- a/VSharp.Explorer/Statistics.fs +++ b/VSharp.Explorer/Statistics.fs @@ -16,7 +16,6 @@ open VSharp.Interpreter.IL open VSharp.Utils open CilState -open IpOperations open CodeLocation type pob = {loc : codeLocation; lvl : uint; pc : pathCondition} diff --git a/VSharp.InternalCalls/IntPtr.fs b/VSharp.InternalCalls/IntPtr.fs index 0e974becf..5d21301de 100644 --- a/VSharp.InternalCalls/IntPtr.fs +++ b/VSharp.InternalCalls/IntPtr.fs @@ -12,7 +12,6 @@ module IntPtr = let ptr = MakeIntPtr term Memory.Write state this ptr Nop() - let internal intPtrCtorFromInt (state : state) (args : term list) : term = assert(List.length args = 2) diff --git a/VSharp.SILI.Core/MemoryRegion.fs b/VSharp.SILI.Core/MemoryRegion.fs index bf8db5b3a..9af8f0f14 100644 --- a/VSharp.SILI.Core/MemoryRegion.fs +++ b/VSharp.SILI.Core/MemoryRegion.fs @@ -280,7 +280,8 @@ type heapArrayKey = let! gu, u = Merging.unguardGvs ub return (g &&& gl &&& gu, l::accLbs, u::accUbs) } - let boundsPairs = List.foldBack2 unGuard lowerBounds upperBounds [True(), [], []] + let initialState = List.singleton (True(), List.empty, List.empty) + let boundsPairs = List.foldBack2 unGuard lowerBounds upperBounds initialState let addresses = Merging.unguardGvs address list { let! gAddr, addr = addresses @@ -716,6 +717,7 @@ module MemoryRegion = let maxTime (tree : updateTree<'a, heapAddress, 'b>) startingTime = RegionTree.foldl (fun m _ {key=_; value=v} -> VectorTime.max m (timeOf v)) startingTime tree + let read mr key isDefault instantiate specializedReading = let makeSymbolic tree = instantiate mr.typ {mr with updates = tree} let makeDefault () = diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index eab420702..1749d9225 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -1491,7 +1491,6 @@ module internal Z3 = StateModel state with e -> internalfail $"MkModel: caught exception {e}" - let private ctx = new Context() let private builder = Z3Builder(ctx) From 6efe77541119aaebd138b114bfd80098cc113066 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Sun, 27 Oct 2024 14:46:51 +0300 Subject: [PATCH 7/8] [test] added tests --- VSharp.Test/Tests/BoxUnbox.cs | 10 +++++----- VSharp.Test/Tests/Unsafe.cs | 26 ++++++++++++++++++++++++++ 2 files changed, 31 insertions(+), 5 deletions(-) diff --git a/VSharp.Test/Tests/BoxUnbox.cs b/VSharp.Test/Tests/BoxUnbox.cs index b60190d7a..24766805e 100644 --- a/VSharp.Test/Tests/BoxUnbox.cs +++ b/VSharp.Test/Tests/BoxUnbox.cs @@ -17,11 +17,11 @@ public A() } } - public struct B + public struct B { - private double x; + private T x; - public B(double z) + public B(T z) { x = z; } @@ -45,14 +45,14 @@ private static T Cast (object o) [TestSvm] public static B UnboxAny1() { - var b = new B(5); + var b = new B(5); return Cast(b); } [TestSvm] public static object UnboxAny2() { - var b = new B(5); + var b = new B(5); return Cast(b); } diff --git a/VSharp.Test/Tests/Unsafe.cs b/VSharp.Test/Tests/Unsafe.cs index 43eb61ab5..f250b7edd 100644 --- a/VSharp.Test/Tests/Unsafe.cs +++ b/VSharp.Test/Tests/Unsafe.cs @@ -822,6 +822,32 @@ public static int DoubleReinterpretation1(int[] arr, int i, int j) } } + [TestSvm(100)] + public static int DoubleReinterpretation2(long a, int i) + { + var p = &a; + var ptr = (int*)((byte*)p + i); + var v = *ptr; + var ptr2 = (byte*)&v + 1; + return *ptr2; + } + + [TestSvm(94)] + public static bool DoubleReinterpretation3(long a, int i, int j) + { + var b = a; + var p = &a; + var ptr = (int*)((byte*)p + i); + var v = *ptr; + ptr = (int*)((byte *)p + i); + *ptr = v; + var p2 = &b; + var ptr2 = (int*)((byte *)p2 + i); + if (*(int*)((byte *)ptr + j) == *(int*)((byte *)ptr2 + j)) + return true; + return false; + } + [TestSvm(100)] public static int DoubleWrite(long[] arr, int i, int v, byte v2) { From 3e06213286d76d9a70ce96c5e61b00b79667b3f7 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Sun, 27 Oct 2024 14:53:36 +0300 Subject: [PATCH 8/8] [fix] fixed CI ubuntu version --- .github/workflows/build_vsharp.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build_vsharp.yml b/.github/workflows/build_vsharp.yml index 13602f8fb..3ad121329 100644 --- a/.github/workflows/build_vsharp.yml +++ b/.github/workflows/build_vsharp.yml @@ -5,7 +5,7 @@ on: jobs: build: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - name: Checkout VSharp uses: actions/checkout@v3