Constraint independence #124
Closed
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
MchKosticyn
reviewed
Dec 2, 2021
VSharp.SILI.Core/PathCondition.fs
Outdated
Comment on lines
45
to
78
| let condConsts = discoverConstants [cond] |> PersistentSet.ofSeq | ||
| let pufWithNewConsts = | ||
| condConsts | ||
| |> PersistentSet.filter (fun t -> None = PersistentUnionFind.tryFind t pc.constants) | ||
| |> PersistentSet.fold PersistentUnionFind.add pc.constants | ||
| let constsWithSources = | ||
| Seq.map | ||
| (function | ||
| | ConstantT(_, src, _) as constant -> constant, src | ||
| | _ -> __unreachable__() | ||
| ) | ||
| // Merge sets of constants dependent in terms of ISymbolicConstantSource | ||
| let pufMergedByConstantSource = | ||
| Seq.allPairs | ||
| (condConsts |> PersistentSet.toSeq |> constsWithSources) | ||
| (pc.constants |> PersistentUnionFind.toSeq |> constsWithSources) | ||
| |> Seq.filter (fun ((_, src1), (_, src2)) -> not <| src1.IndependentWith src2) | ||
| |> Seq.fold (fun puf ((const1, _), (const2, _)) -> PersistentUnionFind.union const1 const2 puf) pufWithNewConsts | ||
| (* | ||
| Merge sets of constants dependent in terms of reachability in graph where | ||
| edge between constants means that they are contained in the same condition | ||
| *) | ||
| let pufMergedByDependentCondition = | ||
| condConsts | ||
| |> someSetElement | ||
| |> function | ||
| | Some(parent) -> | ||
| PersistentSet.fold (fun puf t -> PersistentUnionFind.union t parent puf) pufMergedByConstantSource condConsts | ||
| | None -> pufMergedByConstantSource | ||
| {constants = pufMergedByDependentCondition | ||
| conditionsWithConstants = | ||
| condConsts | ||
| |> someSetElement | ||
| |> (fun head -> PersistentDict.add cond head pc.conditionsWithConstants)} |
There was a problem hiding this comment.
Лучше это выделить в отдельную функцию
VSharp.SILI.Core/Memory.fs
Outdated
Comment on lines
669
to
671
| |> function | ||
| | Some(fragment) -> fragment | ||
| | None -> pc |
There was a problem hiding this comment.
Вероятно, Option.defaultValue здесь будет лучше смотреться
VSharp.SILI.Core/PathCondition.fs
Outdated
Comment on lines
50
to
61
| let constsWithSources = | ||
| Seq.map | ||
| (function | ||
| | ConstantT(_, src, _) as constant -> constant, src | ||
| | _ -> __unreachable__() | ||
| ) | ||
| // Merge sets of constants dependent in terms of ISymbolicConstantSource | ||
| let pufMergedByConstantSource = | ||
| Seq.allPairs | ||
| (condConsts |> PersistentSet.toSeq |> constsWithSources) | ||
| (pc.constants |> PersistentUnionFind.toSeq |> constsWithSources) | ||
| |> Seq.filter (fun ((_, src1), (_, src2)) -> not <| src1.IndependentWith src2) |
There was a problem hiding this comment.
Source из константы не нужен в последствии, поэтому вместо создания последовательности из пар (константа, source), стоит объявить функцию, которая будет принимать пару конастант и сравнивать их source
VSharp.SILI.Core/PathCondition.fs
Outdated
| pc.conditionsWithConstants | ||
| |> PersistentDict.fold groupConditionsByUnionFindParent PersistentDict.empty | ||
| |> PersistentDict.toSeq | ||
| |> Seq.map conditionsGroupToPathCondition |
There was a problem hiding this comment.
Стоит добавить пустую строчку, чтобы гит не ругался
VSharp.SILI.Core/PathCondition.fs
Outdated
Comment on lines
99
to
101
| |> function | ||
| | Some(someConst) -> PersistentUnionFind.tryFind someConst pc.constants | ||
| | None -> None |
There was a problem hiding this comment.
Тут можно использовать Option.bind
VSharp.Utils/PersistentUnionFind.fs
Outdated
| traverse unwrappedNext updatedDict | ||
| else updatedDict | ||
| let subsetElements = traverse a PersistentDict.empty | ||
| {elements = subsetElements} |
There was a problem hiding this comment.
Нужно добавить пустую строчку в конец файла
mxprshn
commented
Dec 24, 2021
| @@ -333,6 +349,20 @@ module internal Memory = | |||
| let declaringType = fromDotNetType m.DeclaringType | |||
| if isValueType declaringType then __insufficientInformation__ "Can't execute in isolation methods of value types, because we can't be sure where exactly \"this\" is allocated!" | |||
| else HeapRef (Constant "this" {baseSource = {key = ThisKey m; time = Some VectorTime.zero}} AddressType) declaringType | |||
|
|
|||
| let fillWithParametersAndThis state (method : System.Reflection.MethodBase) = | |||
| let parameters = method.GetParameters() |> Seq.map (fun param -> | |||
There was a problem hiding this comment.
В этом месте не уверен по поводу того, нужно ли вместе с параметрами добавить что-то в allocatedTypes у state
|
Сломалась версия runtime, пофикшу |
mxprshn
commented
Mar 21, 2022
| // let usedPaths = | ||
| // pathAtoms | ||
| // |> Seq.filter (fun atom -> z3Model.Eval(atom, false).IsTrue) | ||
| // |> Seq.map (fun atom -> paths.[atom]) | ||
| SmtSat { mdl = model; usedPaths = [](*usedPaths*) } | ||
| builder.ClearT2E() |
There was a problem hiding this comment.
Немного напрягло, что пришлось чистить кэш (иначе в модель попадали лишние константы из кэша)
|
Перенесено в общий пуллреквест с оптимизациями |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.