diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-05-31 02:07:54 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-31 02:07:54 +0100 |
commit | 68ab5fb3aa207fa4907fd67ba2751c59fb5e1ce2 (patch) | |
tree | 0d8579d46a6312df9895fd56e5894b73da82caf4 /src | |
parent | a8aef8ab043500f10cfb82ee5d86efedba50cae4 (diff) | |
download | vericert-68ab5fb3aa207fa4907fd67ba2751c59fb5e1ce2.tar.gz vericert-68ab5fb3aa207fa4907fd67ba2751c59fb5e1ce2.zip |
Do not remove dependencies from control-flow
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/Schedule.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 9ba2b51..829ded1 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -559,12 +559,17 @@ let assigned_vars vars = function | RBsetpred (_, _, _, _) -> vars | RBexit (_, _) -> vars +(** To be able to properly eliminate dependencies on control-flow, one needs to be able to handle + comparisons of a register that has a value in one version, and no value in the other, which the + checker currently does not. *) + let get_pred = function | RBnop -> None | RBop (op, _, _, _) -> op | RBload (op, _, _, _, _) -> op | RBstore (op, _, _, _, _) -> op - | RBexit (op, _) -> op + (* | RBexit (op, _) -> op *) + | RBexit (op, _) -> None | RBsetpred (_, _, _, _) -> None let independant_pred p p' = |