diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index 6c1359775..0b24bf1b1 100644 --- a/VSharp.SILI.Core/API.fs +++ b/VSharp.SILI.Core/API.fs @@ -556,8 +556,8 @@ module API = | Ite iteType -> let filtered = iteType.filter (fun r -> Pointers.isBadRef r |> isTrue |> not) filtered.ToDisjunctiveGvs() - |> List.iter (fun (g, r) -> state.memory.GuardedWriteClassField (Some g) (extractAddress r) field value) - | _ -> state.memory.WriteClassField (extractAddress reference) field value + |> List.iter (fun (g, r) -> state.memory.WriteClassField (Some g) (extractAddress r) field value) + | _ -> state.memory.WriteClassField None (extractAddress reference) field value let WriteClassField state reference field value = WriteClassFieldUnsafe emptyReporter state reference field value @@ -733,7 +733,7 @@ module API = let symbolicCase address = let address, arrayType = memory.StringArrayInfo address (Some length) Copying.fillArray state address arrayType (makeNumber 0) length char - memory.WriteClassField address Reflection.stringLengthField length + memory.WriteClassField None address Reflection.stringLengthField length match string.term, concreteChar, concreteLen with | HeapRef({term = ConcreteHeapAddress a} as address, sightType), Some (:? char as c), Some (:? int as len) when cm.Contains a -> diff --git a/VSharp.SILI.Core/Copying.fs b/VSharp.SILI.Core/Copying.fs index 9d070c522..952952036 100644 --- a/VSharp.SILI.Core/Copying.fs +++ b/VSharp.SILI.Core/Copying.fs @@ -75,7 +75,7 @@ module internal Copying = let stringAddress = ConcreteHeapAddress stringConcreteAddress let stringAddress, arrayType = memory.StringArrayInfo stringAddress (Some arrayLength) copyArray state arrayAddress startIndex arrayType stringAddress (makeNumber 0) arrayType arrayLength - memory.WriteClassField stringAddress Reflection.stringLengthField arrayLength + memory.WriteClassField None stringAddress Reflection.stringLengthField arrayLength let copyCharArrayToString (state : state) arrayAddress stringConcreteAddress startIndex length = let memory = state.memory diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index d2a561367..d142dcf71 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -2040,9 +2040,7 @@ module internal Memory = self.CommonWriteArrayIndex None address indices arrayType value member self.WriteArrayRange address fromIndices toIndices arrayType value = self.CommonWriteArrayRange None address fromIndices toIndices arrayType value - member self.WriteClassField address field value = - self.CommonWriteClassField None address field value - member self.GuardedWriteClassField guard address field value = + member self.WriteClassField guard address field value = self.CommonWriteClassField guard address field value member self.WriteStackLocation key value = writeStackLocation key value diff --git a/VSharp.SILI.Core/MemoryRegion.fs b/VSharp.SILI.Core/MemoryRegion.fs index 471aa6144..36f92364f 100644 --- a/VSharp.SILI.Core/MemoryRegion.fs +++ b/VSharp.SILI.Core/MemoryRegion.fs @@ -265,7 +265,6 @@ type heapArrayKey = return (gi &&& gt, i::terms) }) |> List.map (fun (g, address::indices) -> (g, OneArrayIndexKey(address, indices))) - // 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 -> list { @@ -280,7 +279,6 @@ type heapArrayKey = let! gIndices, lbs, ubs = boundsPairs return (gAddr &&& gIndices, RangeArrayIndexKey(addr, lbs, ubs)) } - // TODO: if lbs and ubs are unions of concrete values, then unguard them as well override x.InRegionCondition region = match x with @@ -302,7 +300,8 @@ type heapArrayKey = let addressesAreEqual = address === keyAddress let inBounds acc i (l, u) = acc &&& (simplifyLessOrEqual l i id &&& simplifyLessOrEqual i u id) (addressesAreEqual, keyIndices, List.zip lbs ubs) |||> List.fold2 inBounds - | RangeArrayIndexKey _, RangeArrayIndexKey _ -> internalfail $"MatchCondition for RangeArrayIndexKey is not implemented: {x} {key}" + | RangeArrayIndexKey _, RangeArrayIndexKey _ -> + internalfail $"IntersectionCondition for RangeArrayIndexKey is not implemented: {x} {key}" override x.MatchCondition key keyIndexingRegion = let keysAreEqual = (x :> IHeapArrayKey).IntersectionCondition key match x, key with @@ -484,8 +483,8 @@ type symbolicTypeKey = override x.Unguard = [(True(), x)] override x.InRegionCondition _ = __unreachable__() - override x.IntersectionCondition _ = - __unreachable__() + override x.IntersectionCondition key = + Concrete (x.typ = key.typ) typeof override x.MatchCondition key _ = Concrete (x.typ = key.typ) typeof override x.IsExplicit _ = __unreachable__() @@ -505,7 +504,7 @@ type symbolicTypeKey = and ISymbolicTypeKey = IMemoryKey> type updateTreeKey<'key, 'value when 'key : equality> = - {key : 'key; value : 'value; guard : term option; time : vectorTime} + {key : 'key; value : 'value; guard : term option} interface IRegionTreeKey> with override x.Hides y = x.key = y.key && x.hasTrueGuard member x.termGuard = Option.defaultValue (True()) x.guard @@ -517,7 +516,7 @@ type updateTreeKey<'key, 'value when 'key : equality> = match x.guard with | Some g when isFalse g -> true | _ -> false - override x.ToString() = (x.key, x.value, x.guard, x.time).ToString() + override x.ToString() = (x.key, x.value, x.guard).ToString() type updateTree<'key, 'value, 'reg when 'key :> IMemoryKey<'key, 'reg> and 'reg :> IRegion<'reg> and 'key : equality and 'value : equality and 'reg : equality> = regionTree, 'reg> @@ -528,125 +527,132 @@ module private UpdateTree = let isEmpty tree = RegionTree.isEmpty tree - let private getSplittingAndSymbolicTree readKey tree predicate = - let rec recReading (Node d) keysPath = - let splittingTree, symbolicTree = PersistentDict.partition (fun _ (k, _) -> predicate k) d - let collectSplittingAndSymbolicTree (splitting, symbolic) stReg (stUtKey, st) = - let keysAreMatch = (readKey :> IMemoryKey<_,_>).MatchCondition stUtKey.key stReg - let finalGuard = keysAreMatch &&& stUtKey.termGuard - let stSplitting, stSymbolic = recReading st (stUtKey::keysPath) - let modifiedSymbolic = PersistentDict.append symbolic stSymbolic - if finalGuard = False() then - PersistentDict.append splitting stSplitting, modifiedSymbolic - else - let modifiedSplitting = PersistentDict.add stReg ({stUtKey with guard = if isTrue finalGuard then None else Some finalGuard}, Node stSplitting) splitting - modifiedSplitting, modifiedSymbolic - PersistentDict.fold collectSplittingAndSymbolicTree (PersistentDict.empty, symbolicTree) splittingTree - recReading tree [] + let rec private termIsAddress term = + match term.term with + | HeapRef _ + | Struct _ + | Concrete(:? concreteHeapAddress, _) -> true + | Ite iteType -> iteType.exists termIsAddress + | _ -> false + + let private splitInvariantTree readKey (Node d) predicate specializedReading = + let mutable matchingWrites = List.empty + let mutable symbolicStack = List.empty + let mutable foundExactKey = false + let rec recSplit (Node d) = + // records ordered from newest to oldest + let records = PersistentDict.toSeq d |> Seq.rev // may be inefficient? + let enumerator = records.GetEnumerator() + while not foundExactKey && enumerator.MoveNext() do + let reg, (utKey, subtree) = enumerator.Current + let readCondition = (readKey :> IMemoryKey<_,_>).IntersectionCondition utKey.key + let finalGuard = readCondition &&& utKey.termGuard + // found exactly match with [readKey] + if isTrue finalGuard then + foundExactKey <- true + if predicate utKey then + matchingWrites <- (finalGuard, utKey.value)::matchingWrites + else + symbolicStack <- (reg, (utKey, subtree))::symbolicStack + elif predicate utKey then + if isFalse finalGuard |> not then + let value = + if (utKey.key :> IMemoryKey<_,_>).IsRange then specializedReading readKey utKey else utKey.value + matchingWrites <- (finalGuard, value)::matchingWrites + recSplit subtree + else do + symbolicStack <- (reg, (utKey, subtree))::symbolicStack + recSplit (Node d) + let symbolicTree = List.fold (fun tree (r, (k, t)) -> PersistentDict.add r (k, t) tree) PersistentDict.empty symbolicStack + List.rev matchingWrites, symbolicTree let private splitRead d key explicitAddresses specializedReading predicate isDefault makeSymbolic makeDefault = - let concrete, symbolic = getSplittingAndSymbolicTree key (Node d) predicate - let branches = RegionTree.foldr (fun _ utKey acc -> - if (utKey.key :> IMemoryKey<_,_>).IsRange then - let rangeReading = specializedReading key utKey - (utKey.termGuard, rangeReading)::acc - else - (utKey.termGuard, utKey.value)::acc) [] (Node concrete) - if PersistentDict.isEmpty symbolic && key.IsExplicit explicitAddresses then iteType.FromGvs branches - else if PersistentDict.isEmpty symbolic && isDefault key then + let matchingWrites, symbolicTree = splitInvariantTree key (Node d) predicate specializedReading + if PersistentDict.isEmpty symbolicTree && key.IsExplicit explicitAddresses then + match matchingWrites with + | [(_, v)] -> v + | _ -> iteType.FromGvs matchingWrites |> Merging.merge + elif PersistentDict.isEmpty symbolicTree && isDefault key then assert not (key.IsExplicit explicitAddresses) let defaultCase = makeDefault() - {branches = branches; elseValue = defaultCase} + {branches = matchingWrites; elseValue = defaultCase} |> Merging.merge else - let symbolicCase = makeSymbolic (Node symbolic) - {branches = branches; elseValue = symbolicCase} - |> Merging.merge - - ///Collects nodes that should have been on the top of update tree if we did not use splitting - let rec private collectBranchLatestRecords (Node d) predicate latestRecords = - let collectSubtreeNodes acc r (k, st) = - if predicate k then - collectBranchLatestRecords st predicate acc - else - let currLatestTime = (latestRecords |> List.head |> snd).time - if VectorTime.greater k.time currLatestTime then // found strictly later record, reset acc - [(r, k)] - else if VectorTime.equals k.time currLatestTime then - (r,k)::acc - else acc - PersistentDict.fold collectSubtreeNodes latestRecords d - - let rec private collectLatestRecords (Node tree) predicate = - PersistentDict.toSeq tree |> List.ofSeq |> List.map (fun (r, (k, t)) -> collectBranchLatestRecords t predicate [(r, k)]) |> List.concat + let symbolicCase = makeSymbolic (Node symbolicTree) + {branches = matchingWrites; elseValue = symbolicCase} |> Merging.merge let read (key : 'key) (tree : updateTree<'key, term, 'reg>) explicitAddresses specializedReading predicate isDefault makeSymbolic makeDefault = + assert(not key.IsUnion) let reg = key.Region let d = RegionTree.localize reg tree if PersistentDict.isEmpty d then if isDefault key then makeDefault() else makeSymbolic (Node d) else - let latestRecords = collectLatestRecords (Node d) predicate - let sameKey, otherKeys = latestRecords |> List.partition (fun (_, k) -> k.key = key) - let keyRegion = List.fold (fun acc (r, _) -> (acc :> IRegion<_>).Subtract r) reg otherKeys - if reg = keyRegion && (List.head sameKey |> snd).hasTrueGuard then - let key = List.head sameKey |> snd - key.value - else if key.IsRange then makeSymbolic (Node d) - else splitRead d key explicitAddresses specializedReading predicate isDefault makeSymbolic makeDefault + // do not change the order of pattern matching + match PersistentDict.last d with + | Some(_, ({key = key'; value = value'} as utKey, _)) when utKey.hasTrueGuard && key = key' -> value' // exact match + | _ when key.IsRange -> makeSymbolic (Node d) // range key reading + | Some(_, ({key = key'} as utKey, _)) + when utKey.hasTrueGuard && key.IntersectionCondition key' |> isTrue && key'.IsRange -> // specialized reading + specializedReading key utKey + | _ when makeDefault() |> termIsAddress -> // reading from addresses region + splitRead d key explicitAddresses specializedReading predicate isDefault makeSymbolic makeDefault + | _ -> // reading from non addresses region + makeSymbolic (Node d) let memset (keyAndValues : seq<'key * 'value>) (tree : updateTree<'key, 'value, 'reg>) = - let keyAndRegions = keyAndValues |> Seq.mapi (fun i (key, value) -> key.Region, {key=key; value=value; guard = None; time = [i]}) + let keyAndRegions = keyAndValues |> Seq.map (fun (key, value) -> key.Region, {key=key; value=value; guard = None}) RegionTree.memset keyAndRegions tree - let rec private hangRecordUnderSplittingTree region utKey (Node d) predicate = - let splittingTree, symbolicTree = PersistentDict.partition (fun _ (k, _) -> predicate k) d - let keyGuard treeKey = + let rec private placeRecordUnderInvariantSubtree region utKey (Node d) predicate = + let mutable restRegion = region + let guardFromOverwriting treeKey = !!((utKey.key :> IMemoryKey<_,_>).IntersectionCondition treeKey.key &&& utKey.termGuard) &&& treeKey.termGuard - let hangUnderSplittingSubtree acc stReg (stUtKey, st) = - let modifiedSubtree = hangRecordUnderSplittingTree stReg utKey st predicate - let updatedGuard = keyGuard stUtKey - if isFalse updatedGuard then PersistentDict.append acc modifiedSubtree + let placeRecordUnderBranch acc stReg (stUtKey, st) = + restRegion <- (restRegion :> IRegion<_>).Subtract stReg + if predicate utKey then + let modifiedSubtree = placeRecordUnderInvariantSubtree stReg utKey st predicate + let updatedGuard = guardFromOverwriting stUtKey + if isFalse updatedGuard then PersistentDict.append acc modifiedSubtree + else + let guardedStUtKey = {stUtKey with guard = Some updatedGuard} + PersistentDict.add stReg (guardedStUtKey, Node modifiedSubtree) acc else - let guardedStUtKey = {stUtKey with guard = Some updatedGuard} - PersistentDict.add stReg (guardedStUtKey, Node modifiedSubtree) acc - let splittingTree = PersistentDict.fold hangUnderSplittingSubtree PersistentDict.empty splittingTree - let restRegion = PersistentDict.fold (fun acc r _ -> (acc :> IRegion<_>).Subtract r) region splittingTree - if restRegion.IsEmpty then splittingTree - else PersistentDict.add restRegion (utKey, Node symbolicTree) splittingTree + let subtree = PersistentDict.add stReg (stUtKey, st) PersistentDict.empty + PersistentDict.add stReg (utKey, Node subtree) acc + let modifiedTree = PersistentDict.fold placeRecordUnderBranch PersistentDict.empty d + if restRegion.IsEmpty then + modifiedTree + else + PersistentDict.add restRegion (utKey, Node PersistentDict.empty) modifiedTree let write region (utKey : updateTreeKey<_,_>) tree predicate = - if utKey.hasFalseGuard then tree + assert(not (utKey.key :> IMemoryKey<_,_>).IsUnion) + assert(not utKey.hasFalseGuard) + if termIsAddress utKey.value |> not then + RegionTree.write utKey.key.Region utKey tree + elif predicate utKey then + // invariant will be preserved, do usual write + RegionTree.write utKey.key.Region utKey tree else - let unguardedKey = (utKey.key :> IMemoryKey<_,_>).Unguard - let disjointUnguardedKey = List.mapFold (fun disjGuard (g, k) -> (disjGuard &&& g, k), !!g &&& disjGuard) (True()) unguardedKey |> fst - let writeOneKey (g, k) accTree = - let included, disjoint = RegionTree.localizeFilterHidden region utKey accTree - let refinedKey = - let guard = utKey.termGuard &&& g |> Some - {utKey with guard = guard; key = k} - if predicate refinedKey then - PersistentDict.add region (refinedKey, Node included) disjoint |> Node - else - let modifiedTree = hangRecordUnderSplittingTree region utKey (Node included) predicate - PersistentDict.append modifiedTree disjoint |> Node - List.foldBack writeOneKey disjointUnguardedKey tree - + // need to preserve the invariant that is concrete values are always at the top of the tree + let included, disjoint = RegionTree.localizeFilterHidden region utKey tree + let modifiedTree = placeRecordUnderInvariantSubtree region utKey (Node included) predicate + PersistentDict.append disjoint modifiedTree |> Node - let map (mapKey : 'reg -> 'key -> 'reg * 'key) mapValue (tree : updateTree<'key, 'value, 'reg>) predicate = - let mapper reg {key=k; value=v; guard = g; time = t} = + let map (mapKey : 'reg -> 'key -> 'reg * 'key) mapValue (tree : updateTree<'key, 'value, 'reg>) = + let mapper reg {key = k; value = v; guard = g} = 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}) - let splitWrite reg key tree = write reg key tree predicate - RegionTree.choose mapper tree splitWrite + | Some False -> None + | _ -> Some(reg', k'.Region, {key = k'; value = mapValue v; guard = g'}) + RegionTree.choose mapper tree RegionTree.write - let compose (earlier : updateTree<'key, 'value, 'reg>) (later : updateTree<'key, 'value, 'reg>) predicate nextUpdateTime = - let writeOneKey reg utKey (accTree, time) = + let compose (earlier : updateTree<'key, 'value, 'reg>) (later : updateTree<'key, 'value, 'reg>) = + let writeOneKey reg utKey accTree = assert(not (utKey.key :> IMemoryKey<_,_>).IsUnion) - write reg {utKey with time = time} accTree predicate, VectorTime.next time - RegionTree.foldr writeOneKey (earlier, nextUpdateTime) later + RegionTree.write reg utKey accTree + RegionTree.foldr writeOneKey earlier later let deterministicCompose earlier later = RegionTree.append earlier later @@ -664,7 +670,7 @@ module private UpdateTree = [] type memoryRegion<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> = - {typ : Type; updates : updateTree<'key, term, 'reg>; defaultValue : term option; nextUpdateTime : vectorTime; explicitAddresses : vectorTime pset} + {typ : Type; updates : updateTree<'key, term, 'reg>; defaultValue : term option; explicitAddresses : vectorTime pset} with override x.Equals(other : obj) = match other with @@ -686,24 +692,21 @@ type memoryRegion<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, ' HashCode.Combine(x.typ, x.updates, defaultValue) module MemoryRegion = - - let empty typ = {typ = typ; updates = UpdateTree.empty; defaultValue = None; nextUpdateTime = [1]; explicitAddresses = PersistentSet.empty} - let emptyWithExplicit typ addr = {typ = typ; updates = UpdateTree.empty; defaultValue = None; nextUpdateTime = [1]; explicitAddresses = PersistentSet.add PersistentSet.empty addr} + let empty typ = {typ = typ; updates = UpdateTree.empty; defaultValue = None; explicitAddresses = PersistentSet.empty} + let emptyWithExplicit typ addr = {typ = typ; updates = UpdateTree.empty; defaultValue = None; explicitAddresses = PersistentSet.add PersistentSet.empty addr} let addExplicitAddress addr mr = {mr with explicitAddresses = PersistentSet.add mr.explicitAddresses addr} - let valueIsConcrete key = - match key.value.term with - | Concrete _ -> true - | HeapRef(address, _) -> isConcreteHeapAddress address - | _ -> (key.key :> IMemoryKey<_,_>).IsRange - let rec valueIsConcreteHeapAddress key = - match key.value.term with + let rec private isConcreteHeapAddress term = + match term.term with | Concrete(:? concreteHeapAddress, _) -> true | HeapRef(address, _) when isConcreteHeapAddress address -> true | Struct(s, _) -> - PersistentDict.exists (fun (_, v) -> valueIsConcreteHeapAddress {key with value = v}) s - | _ when (key.key :> IMemoryKey<_,_>).IsRange -> true + PersistentDict.exists (fun (_, v) -> isConcreteHeapAddress v) s + | Ite iteType -> iteType.exists isConcreteHeapAddress | _ -> false + let private valueIsConcreteHeapAddress utKey = + if (utKey.key :> IMemoryKey<_,_>).IsRange then true + else isConcreteHeapAddress utKey.value let fillRegion defaultValue (region : memoryRegion<_,_>) = { region with defaultValue = Some defaultValue } @@ -712,7 +715,7 @@ module MemoryRegion = 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 () = + let makeDefault() = match mr.defaultValue with | Some d -> d | _ -> makeDefaultValue mr.typ @@ -727,30 +730,31 @@ module MemoryRegion = canCastImplicitly typ cellType || isPointer typ && isIntegral cellType let memset mr keysAndValues = - {typ = mr.typ; updates = UpdateTree.memset keysAndValues mr.updates; defaultValue = mr.defaultValue - nextUpdateTime = [1 + Seq.length keysAndValues]; explicitAddresses = mr.explicitAddresses} + {typ = mr.typ; updates = UpdateTree.memset keysAndValues mr.updates; defaultValue = mr.defaultValue; + explicitAddresses = mr.explicitAddresses} let write mr guard key value = assert(validateWrite value mr.typ) - let utKey = {key = key; value = value; guard = guard; time = mr.nextUpdateTime} - let updates = UpdateTree.write (key :> IMemoryKey<_,_>).Region utKey mr.updates valueIsConcreteHeapAddress - {mr with updates = updates; nextUpdateTime = VectorTime.next mr.nextUpdateTime } + assert(not (key :> IMemoryKey<_,_>).IsUnion) + let utKey = {key = key; value = value; guard = guard} + {mr with updates = UpdateTree.write (key :> IMemoryKey<_,_>).Region utKey mr.updates valueIsConcreteHeapAddress} let map (mapTerm : term -> term) (mapType : Type -> Type) (mapTime : vectorTime -> vectorTime) mr = let typ = mapType mr.typ - let updates = UpdateTree.map (fun reg k -> k.Map mapTerm mapType mapTime reg) mapTerm mr.updates valueIsConcreteHeapAddress + let updates = UpdateTree.map (fun reg k -> k.Map mapTerm mapType mapTime reg) mapTerm mr.updates let defaultValue = Option.map mapTerm mr.defaultValue - {typ = typ; updates = updates; defaultValue = defaultValue; nextUpdateTime = mr.nextUpdateTime; explicitAddresses = mr.explicitAddresses } + {typ = typ; updates = updates; defaultValue = defaultValue; explicitAddresses = mr.explicitAddresses } let mapKeys<'reg, 'key when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> (mapKey : 'reg -> 'key -> 'reg * 'key) mr = - {mr with updates = UpdateTree.map mapKey id mr.updates valueIsConcreteHeapAddress } + {mr with updates = UpdateTree.map mapKey id mr.updates } let deterministicCompose earlier later = assert later.defaultValue.IsNone if earlier.typ = later.typ then if UpdateTree.isEmpty earlier.updates then { later with defaultValue = earlier.defaultValue } - else {typ = earlier.typ; updates = UpdateTree.deterministicCompose earlier.updates later.updates; defaultValue = earlier.defaultValue - nextUpdateTime = VectorTime.singletonsSum earlier.nextUpdateTime earlier.nextUpdateTime + else {typ = earlier.typ + updates = UpdateTree.deterministicCompose earlier.updates later.updates + defaultValue = earlier.defaultValue explicitAddresses = PersistentDict.append earlier.explicitAddresses later.explicitAddresses} else internalfail "Composing two incomparable memory objects!" @@ -760,8 +764,8 @@ module MemoryRegion = if later.updates |> UpdateTree.forall (fun k -> not k.key.IsUnion) then deterministicCompose earlier later elif earlier.typ = later.typ then - let composedTree, nextTime = UpdateTree.compose earlier.updates later.updates valueIsConcreteHeapAddress earlier.nextUpdateTime - {earlier with updates = composedTree; nextUpdateTime = nextTime } + let composedTree = UpdateTree.compose earlier.updates later.updates + {earlier with updates = composedTree} else internalfail "Composing two incomparable memory objects!" let toString indent mr = UpdateTree.print indent toString mr.updates diff --git a/VSharp.SILI.Core/State.fs b/VSharp.SILI.Core/State.fs index 6950e4b28..cb1653771 100644 --- a/VSharp.SILI.Core/State.fs +++ b/VSharp.SILI.Core/State.fs @@ -257,9 +257,7 @@ and IMemory = abstract WriteStackLocation : stackKey -> term -> unit - abstract WriteClassField : term -> fieldId -> term -> unit - abstract GuardedWriteClassField : term option -> term -> fieldId -> term -> unit - + abstract WriteClassField : term option -> term -> fieldId -> term -> unit abstract Write : IErrorReporter -> term -> term -> unit abstract AllocateOnStack : stackKey -> term -> unit diff --git a/VSharp.SILI.Core/Terms.fs b/VSharp.SILI.Core/Terms.fs index 756fe8b27..ccb0aaf9a 100644 --- a/VSharp.SILI.Core/Terms.fs +++ b/VSharp.SILI.Core/Terms.fs @@ -220,16 +220,22 @@ and iteType = genericIteType and genericIteType<'a> = {branches: (term * 'a) list; elseValue : 'a} with static member FromGvs gvs = - if List.length gvs < 2 then internalfail "Empty and one-element unions are forbidden!" + if List.length gvs < 2 then internalfail "Empty and one-element ite's are forbidden!" let branches, e = List.splitAt (List.length gvs - 1) gvs {branches = branches; elseValue = e |> List.head |> snd} + member x.mapValues mapper = {branches = List.map (fun (g, v) -> (g, mapper v)) x.branches; elseValue = mapper x.elseValue} + member x.filter predicate = if predicate x.elseValue then {branches = List.filter (snd >> predicate) x.branches; elseValue = x.elseValue} else List.filter (snd >> predicate) x.branches |> genericIteType<'a>.FromGvs + + member x.exists predicate = + predicate x.elseValue || List.exists (fun (g, v) -> predicate v) x.branches + member x.choose mapper = let chooser (g, v) = Option.bind (fun w -> Some(g, w)) (mapper v) match mapper x.elseValue with diff --git a/VSharp.Test/Tests/Lists.cs b/VSharp.Test/Tests/Lists.cs index 78d71aebb..88652071f 100644 --- a/VSharp.Test/Tests/Lists.cs +++ b/VSharp.Test/Tests/Lists.cs @@ -532,59 +532,6 @@ public static int TestOverlappingCopy1(int[] a, int i) return 3; } - [TestSvm(94)] - public static int TestSolvingCopyOverwrittenValueUnreachable1(string[] a, string[] b) - { - if (a != null && b != null && a.Length > b.Length) - { - a[0] = "42"; - b[0] = "4"; - Array.Copy(a, 0, b, 0, b.Length); - if (b[0] != "42") // unreachable - { - return -1; - } - - return 0; - } - - return 3; - } - - [TestSvm(95)] - public static int TestSolvingCopyOverwrittenValueUnreachable2(string[] a, int i, string[] b) - { - if (a != null && b != null && a.Length > b.Length) - { - b[i] = "500"; - Array.Copy(a, 0, b, 0, b.Length); - if (b.Length > 0 && a[i] != "500" && b[i] == "500") // unreachable - { - return -1; - } - - return 0; - } - - return 3; - } - - [TestSvm(94)] - public static int TestSolvingCopy8(object[] a, object[] b, int i) - { - if (a.Length > b.Length && 0 <= i && i < b.Length) - { - Array.Fill(a, "abc"); - Array.Copy(a, b, b.Length); - - if (b[i] == b[i + 1]) - return 42; - return 10; - } - - return 3; - } - [TestSvm(97)] public static int TestSolvingCopy9(object[] a, int i, object[] b) { @@ -785,20 +732,6 @@ public class MyClass public int x; } - [TestSvm(88)] - public static int LastRecordReachability(string[] a, string[] b, int i, string s) - { - a[i] = "1"; - b[1] = s; - if (b[1] != s) - { - // unreachable - return -1; - } - - return 0; - } - [TestSvm(90)] public static int ArrayElementsAreReferences(MyClass[] a, int i, int j) { @@ -924,44 +857,6 @@ public static int ConcreteDictionaryTest(int v) return 0; } - [TestSvm(100)] - public static int ConcreteDictionaryTest1(int a, string b) - { - var d = new Dictionary>(); - d.Add(1, new List { "2", "3" }); - d.Add(4, new List { "5", "6" }); - if (d.TryGetValue(a, out var res)) - { - if (res.Contains(b)) - return 1; - return 0; - } - - return 2; - } - - public class Person - { - public string FirstName { get; set; } - public string LastName { get; init; } - }; - - [TestSvm(95)] - public static int IteKeyWrite(int i) - { - var a = new Person[4]; - a[0] = new Person() {FirstName = "asd", LastName = "qwe"}; - a[3] = new Person() {FirstName = "zxc", LastName = "vbn"}; - var p = a[i]; - p.FirstName = "323"; - if (i == 0 && a[3].FirstName == "323") - { - return -1; - } - - return 1; - } - [TestSvm(100)] public static int ListContains(int a, int b) { @@ -1413,33 +1308,6 @@ public static int ConcurrentDict(int a, int b) return -1; return 0; } - [TestSvm(95)] - public static int TestSplittingWithCopy(int srcI, int dstI, int len) - { - string[] arr = {"a", "b", "c", "d", "e"}; - var a = new string[5]; - Array.Copy(arr, srcI, a, dstI, len); - if (a[2].Length == 3) - return -1; - return 1; - } - [TestSvm(91)] - public static int TestSplittingWithCopyRegionsImportance(string[] a, int i) - { - a[i] = "a"; - a[1] = "b"; - var b = new string[a.Length]; - Array.Copy(a, 0, b, 0, a.Length); - if (i == 1 && b[i] == "a") // unreachable - // record b[i], "a" exists only if i != 1 - return -1; - if (i != 1 && b[i] != "a") // unreachable - { - return -2; - } - - return 1; - } [TestSvm(83)] public static int VolatileWrite() diff --git a/VSharp.Test/Tests/Splitting.cs b/VSharp.Test/Tests/Splitting.cs new file mode 100644 index 000000000..46628b4cc --- /dev/null +++ b/VSharp.Test/Tests/Splitting.cs @@ -0,0 +1,196 @@ +using System; +using System.Collections.Generic; +using NUnit.Framework; +using VSharp.Test; + +namespace IntegrationTests; + +[TestSvmFixture] +class SplittingTest +{ + [TestSvm(94)] + public static int TestSolvingCopyOverwrittenValueUnreachable1(string[] a, string[] b) + { + if (a != null && b != null && a.Length > b.Length) + { + a[0] = "42"; + b[0] = "4"; + Array.Copy(a, 0, b, 0, b.Length); + if (b[0] != "42") // unreachable + { + return -1; + } + + return 0; + } + + return 3; + } + + [TestSvm(95)] + public static int TestSolvingCopyOverwrittenValueUnreachable2(string[] a, int i, string[] b) + { + if (a != null && b != null && a.Length > b.Length) + { + b[i] = "500"; + Array.Copy(a, 0, b, 0, b.Length); + if (b.Length > 0 && a[i] != "500" && b[i] == "500") // unreachable + { + return -1; + } + + return 0; + } + + return 3; + } + + [TestSvm(94)] + public static int TestSolvingCopy8(object[] a, object[] b, int i) + { + if (a.Length > b.Length && 0 <= i && i < b.Length) + { + Array.Fill(a, "abc"); + Array.Copy(a, b, b.Length); + + if (b[i] == b[i + 1]) + return 42; + return 10; + } + + return 3; + } + + [TestSvm(88)] + public static int LastRecordReachability(string[] a, string[] b, int i, string s) + { + a[i] = "1"; + b[1] = s; + if (b[1] != s) + { + // unreachable + return -1; + } + + return 0; + } + + [TestSvm(100)] + public static int ConcreteDictionaryTest1(int a, string b) + { + var d = new Dictionary>(); + d.Add(1, new List { "2", "3" }); + d.Add(4, new List { "5", "6" }); + if (d.TryGetValue(a, out var res)) + { + if (res.Contains(b)) + return 1; + return 0; + } + + return 2; + } + + public static int IrrelevantRecordsAreUnreachable(int i, string s) + { + var a = new string[] { "a", "b", "c", "d" }; + a[2] = "323"; + a[i] = s; + a[1] = "1"; + if (a[i] != "1" && a[i] != s) + { + return -1; + } + + return 1; + } + + public class Person + { + public string FirstName { get; set; } + public string LastName { get; init; } + public override int GetHashCode() + { + return 800; + } + }; + + [TestSvm(95)] + public static int IteKeyWrite(int i) + { + var a = new Person[4]; + a[0] = new Person() {FirstName = "asd", LastName = "qwe"}; + a[3] = new Person() {FirstName = "zxc", LastName = "vbn"}; + var p = a[i]; + p.FirstName = "323"; + if (i == 0 && a[3].FirstName == "323") + { + // unreachable + return -1; + } + + return 1; + } + + [TestSvm(96)] + public static int IteValueWrite(int i, int j) + { + var a = new string[] { "a", "b", "c", "d" }; + a[j] = a[i]; + if (a[j] == "a") return 0; + if (a[j] == "b") return 1; + if (a[j] == "c") return 2; + if (a[j] == "d") return 3; + // unreachable + return -1; + } + + [TestSvm(95)] + public static int TestSplittingWithCopy(int srcI, int dstI, int len, int i) + { + string[] arr = {"a", "b", "c", "d", "e"}; + var a = new string[5]; + Array.Copy(arr, srcI, a, dstI, len); + if (a[i].Length != 1) + return -1; + return 1; + } + [TestSvm(91)] + public static int TestSplittingWithCopyRegionsImportance(string[] a, int i) + { + a[i] = "a"; + a[1] = "b"; + var b = new string[a.Length]; + Array.Copy(a, 0, b, 0, a.Length); + if (i == 1 && b[i] == "a") // unreachable + // record b[i], "a" exists only if i != 1 + return -1; + if (i != 1 && b[i] != "a") // unreachable + { + return -2; + } + + return 1; + } + + [TestSvm(93)] + public static int ExistingKeyReading(string s1, string s2, int i) + { + var a = new string[10]; + a[i] = s1; + a[2] = s2; + if (a[i] == s2) return 1; + if (a[i] == s1) return 0; + return -1; + } + + [Ignore("Implement branching with solver interaction on callVirt")] + public static int CallVirtIte(int i) + { + var a = new object[] { "aasd", 500, new Person() }; + var r = a[i].GetHashCode(); + if (r == 500) return 1; + if (r == 800) return 2; + return 0; + } +} diff --git a/VSharp.Utils/PersistentDictionary.fs b/VSharp.Utils/PersistentDictionary.fs index 8d133cb93..9c0293ebb 100644 --- a/VSharp.Utils/PersistentDictionary.fs +++ b/VSharp.Utils/PersistentDictionary.fs @@ -58,6 +58,7 @@ module public PersistentDict = | None -> add key (mapper defaultValue) d let public size (d : pdict<'a, 'b>) = d.impl.Length + let public last (d : pdict<'a, 'b>) = d.impl.Iterator() |> Seq.tryLast let public map (keyMapper : 'a -> 'a) (valueMapper : 'b -> 'c) (d : pdict<'a, 'b>) : pdict<'a, 'c> = d |> toSeq |> Seq.map (fun (k, v) -> (keyMapper k, valueMapper v)) |> ofSeq @@ -79,7 +80,7 @@ module public PersistentDict = let public partition predicate (d : pdict<'a, 'b>) = let mutable sat = empty let mutable unsat = empty - for (k, v) in toSeq d do + for k, v in toSeq d do if predicate k v then sat <- add k v sat else unsat <- add k v unsat sat, unsat diff --git a/VSharp.Utils/RegionTree.fs b/VSharp.Utils/RegionTree.fs index 7ee8a980c..8d0bdbc00 100644 --- a/VSharp.Utils/RegionTree.fs +++ b/VSharp.Utils/RegionTree.fs @@ -68,11 +68,9 @@ module RegionTree = let memset regionsAndKeys (Node tree) = regionsAndKeys |> Seq.fold (fun acc (reg, k) -> PersistentDict.add reg (k, Node PersistentDict.empty) acc) tree |> Node - let private commonWrite reg key tree filter = - let included, disjoint = splitNode filter reg tree - Node(PersistentDict.add reg (key, Node included) disjoint) let write reg key tree = - commonWrite reg key tree (key :> IRegionTreeKey<_>).Hides + let included, disjoint = splitNode (key :> IRegionTreeKey<_>).Hides reg tree + Node(PersistentDict.add reg (key, Node included) disjoint) let rec foldl folder acc (Node d) = PersistentDict.fold (fun acc reg (k, t) -> let acc = folder acc reg k in foldl folder acc t) acc d diff --git a/VSharp.Utils/VectorTime.fs b/VSharp.Utils/VectorTime.fs index e70360ac6..0d5d54335 100644 --- a/VSharp.Utils/VectorTime.fs +++ b/VSharp.Utils/VectorTime.fs @@ -21,13 +21,6 @@ module VectorTime = let singleton t : vectorTime = List.singleton t - let next t : vectorTime = - let x = extractFromSingleton t - x + 1 |> singleton - - let singletonsSum t1 t2 = - extractFromSingleton t1 + extractFromSingleton t2 |> singleton - let rec compare (t1 : vectorTime) (t2 : vectorTime) = List.compareWith (fun (v1 : int32) (v2 : int32) -> v1.CompareTo(v2)) t1 t2