Closed
Conversation
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)} |
Member
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 |
Member
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) |
Member
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 No newline at end of file |
Member
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 |
Member
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} No newline at end of file |
Member
There was a problem hiding this comment.
Нужно добавить пустую строчку в конец файла
mxprshn
commented
Dec 24, 2021
| 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 -> |
Member
Author
There was a problem hiding this comment.
В этом месте не уверен по поводу того, нужно ли вместе с параметрами добавить что-то в allocatedTypes у state
Member
Author
|
Сломалась версия runtime, пофикшу |
mxprshn
commented
Mar 21, 2022
| // |> Seq.filter (fun atom -> z3Model.Eval(atom, false).IsTrue) | ||
| // |> Seq.map (fun atom -> paths.[atom]) | ||
| SmtSat { mdl = model; usedPaths = [](*usedPaths*) } | ||
| builder.ClearT2E() |
Member
Author
There was a problem hiding this comment.
Немного напрягло, что пришлось чистить кэш (иначе в модель попадали лишние константы из кэша)
Member
Author
|
Перенесено в общий пуллреквест с оптимизациями |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.