diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-11 11:57:30 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-11 11:57:30 +0100 |
| commit | 2231fe82a807cebab5cae495ed08cda17810efdc (patch) | |
| tree | 76e59dd1e069ffac31f5cf9736e71db34f760a20 /backend/CSE3analysis.v | |
| parent | 4dc9118a4578be8b869a8dd8fa98c15a0b592419 (diff) | |
| download | compcert-kvx-2231fe82a807cebab5cae495ed08cda17810efdc.tar.gz compcert-kvx-2231fe82a807cebab5cae495ed08cda17810efdc.zip | |
CSE3 ready to run?
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 140f2333..18aa33b1 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -303,16 +303,16 @@ Record analysis_hints := hint_eq_find_oracle : node -> equation -> option eq_id; hint_eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t }. -Definition analysis (hints : analysis_hints) := +Definition context_from_hints (hints : analysis_hints) := let eqs := hint_eq_catalog hints in let reg_kills := get_reg_kills eqs in let mem_kills := get_mem_kills eqs in let moves := get_moves eqs in - internal_analysis (ctx := {| - eq_catalog := fun eq_id => PTree.get eq_id eqs; - eq_find_oracle := hint_eq_find_oracle hints ; - eq_rhs_oracle := hint_eq_rhs_oracle hints; - eq_kill_reg := fun reg => PMap.get reg reg_kills; - eq_kill_mem := fun _ => mem_kills; - eq_moves := fun reg => PMap.get reg moves - |}). + {| + eq_catalog := fun eq_id => PTree.get eq_id eqs; + eq_find_oracle := hint_eq_find_oracle hints ; + eq_rhs_oracle := hint_eq_rhs_oracle hints; + eq_kill_reg := fun reg => PMap.get reg reg_kills; + eq_kill_mem := fun _ => mem_kills; + eq_moves := fun reg => PMap.get reg moves + |}. |