| commit | ef9d5270bdd6e33fea3992018671c4ea13e160e6 | |
| author | Mistral Orhan Jean-Pierre Contrastin <mojpc2@fb.com> | |
| Tue, 16 Aug 2022 12:25:33 +0000 (16 05:25 -0700) | ||
| committer | Facebook GitHub Bot <facebook-github-bot@users.noreply.github.com> | |
| Tue, 16 Aug 2022 12:25:33 +0000 (16 05:25 -0700) | ||
| tree | 57e1359012575de8b9aa743e4d009972f499d2ad | treesnapshot (tar.gz zip) |
| parent | 5fdd52e82b61199118d529f00391a6534c0c2758 | commitdiff |
Rewrite dynamic access solving
Summary:
Switches to a set representation for dynamic accesses within the solver.
The diff also moves away from using the transitive closure of the subset relation to propagate the constraint and does so in a semi-naïve manner by only considering each new generation at each iteration.
This diff is behaviour changing, we previously propagated the constraint backwards in the subset relation or forwards, but didn't allow for a combination of both. For example, if we had a dynamic access to a CoW array, we'd propagate to the other arrays based off of it, but not to any birfurcations from the previous array. See the test case.
Differential Revision: D38501367
fbshipit-source-id: 0797f6ab96d78190969ca64d472277d89ff38e45
Summary:
Switches to a set representation for dynamic accesses within the solver.
The diff also moves away from using the transitive closure of the subset relation to propagate the constraint and does so in a semi-naïve manner by only considering each new generation at each iteration.
This diff is behaviour changing, we previously propagated the constraint backwards in the subset relation or forwards, but didn't allow for a combination of both. For example, if we had a dynamic access to a CoW array, we'd propagate to the other arrays based off of it, but not to any birfurcations from the previous array. See the test case.
Differential Revision: D38501367
fbshipit-source-id: 0797f6ab96d78190969ca64d472277d89ff38e45