diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-07-16 21:11:34 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-07-16 21:13:40 +0200 |
| commit | 7b34d3c03fea76b85ec72d5ee82c53353960e2b2 (patch) | |
| tree | b73f98ebdbc87fbdf22df7a554d116abeb676524 /backend/CSE3.v | |
| parent | e11b548d94b247b5359960b8d31027b53ee0dffc (diff) | |
| download | compcert-kvx-7b34d3c03fea76b85ec72d5ee82c53353960e2b2.tar.gz compcert-kvx-7b34d3c03fea76b85ec72d5ee82c53353960e2b2.zip | |
make CSE3 condition parametric
Diffstat (limited to 'backend/CSE3.v')
| -rw-r--r-- | backend/CSE3.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index 746ba399..5d05821a 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -20,6 +20,14 @@ Local Open Scope error_monad_scope. Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints. +Record cse3params : Type := + mkcse3params + { cse3_conditions : bool; + }. + +Section PARAMS. + Variable params : cse3params. + Section REWRITE. Context {ctx : eq_context}. @@ -54,7 +62,7 @@ Definition subst_args fmap pc xl := forward_move_l_b (PMap.get pc fmap) xl. Definition find_cond_in_fmap fmap pc cond args := - if Compopts.optim_CSE3_conditions tt + if cse3_conditions params then match PMap.get pc fmap with | Some rel => @@ -129,3 +137,5 @@ Definition transf_fundef (fd: fundef) : res fundef := Definition transf_program (p: program) : res program := transform_partial_program transf_fundef p. + +End PARAMS. |