diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 13:15:53 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 13:15:53 +0100 |
| commit | 0a13bf127bb385df424bd9e392742d4fc5bef86a (patch) | |
| tree | e01a0c87bc5225934604cb1d3a786b7c02b6243f /backend | |
| parent | f01d490fad2fbf7fb7a2e0861075ca6c09976ec4 (diff) | |
| download | compcert-kvx-0a13bf127bb385df424bd9e392742d4fc5bef86a.tar.gz compcert-kvx-0a13bf127bb385df424bd9e392742d4fc5bef86a.zip | |
begin implementing -fcse3-conditions
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CSE3analysis.v | 11 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 12 |
2 files changed, 15 insertions, 8 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 383147bb..75e00f67 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -477,10 +477,13 @@ Section OPERATIONS. end. Definition apply_cond cond args (rel : RELATION.t) : RB.t := - match apply_cond1 cond args rel with - | Some rel => Some (apply_cond0 cond args rel) - | None => RB.bot - end. + if Compopts.optim_CSE3_conditions tt + then + match apply_cond1 cond args rel with + | Some rel => Some (apply_cond0 cond args rel) + | None => RB.bot + end + else Some rel. Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) := match instr with diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 29d171eb..d53cf604 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1350,10 +1350,14 @@ Section SOUNDNESS. Proof. unfold apply_cond. intros. - pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1. - destruct apply_cond1 eqn:COND1. - { apply apply_cond0_sound; auto. } - exact SOUND1. + destruct (Compopts.optim_CSE3_conditions tt). + { + pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1. + destruct apply_cond1 eqn:COND1. + { apply apply_cond0_sound; auto. } + exact SOUND1. + } + exact REL. Qed. (* |