diff options
| -rw-r--r-- | backend/CSE3analysis.v | 24 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 18 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Compopts.v | 3 | ||||
| -rw-r--r-- | driver/Driver.ml | 2 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 |
6 files changed, 36 insertions, 14 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index bd507dec..ade79c28 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -78,7 +78,10 @@ Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. Definition lub x y := if Compopts.optim_CSE3_across_merges tt then PSet.inter x y - else PSet.empty. + else + if PSet.eq x y + then x + else PSet.empty. Definition glb := PSet.union. @@ -94,8 +97,10 @@ Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. intuition. - apply PSet.is_subset_spec. intro. - rewrite PSet.gempty. - discriminate. + destruct (PSet.eq x y). + + auto. + + rewrite PSet.gempty. + discriminate. Qed. Lemma ge_lub_right: forall x y, ge (lub x y) y. @@ -110,8 +115,10 @@ Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. intuition. - apply PSet.is_subset_spec. intro. - rewrite PSet.gempty. - discriminate. + destruct (PSet.eq x y). + + subst. auto. + + rewrite PSet.gempty. + discriminate. Qed. Definition top := PSet.empty. @@ -310,8 +317,11 @@ Section OPERATIONS. else let args' := forward_move_l rel args in match rhs_find op args' rel with - | Some r => (* FIXME RELATION.glb ( *) move r dst rel (* ) - (oper1 dst op args' rel) *) + | Some r => + if Compopts.optim_CSE3_glb tt + then RELATION.glb (move r dst rel) + (oper1 dst op args' rel) + else oper1 dst op args' rel | None => oper1 dst op args' rel end. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 0c2aeb8e..f4e3672d 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -799,13 +799,17 @@ Section SOUNDNESS. rewrite <- (forward_move_sound rel rs m r) by auto. apply move_sound; auto. - destruct rhs_find as [src |] eqn:RHS_FIND. - + (* FIXME apply sem_rel_glb; split. *) - * pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND. - eapply forward_move_rhs_sound in RHS. - 2: eassumption. - rewrite <- (sem_rhs_det SOUND RHS). - apply move_sound; auto. - (* FIXME * apply oper1_sound; auto. *) + + destruct (Compopts.optim_CSE3_glb tt). + * apply sem_rel_glb; split. + ** pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND. + eapply forward_move_rhs_sound in RHS. + 2: eassumption. + rewrite <- (sem_rhs_det SOUND RHS). + apply move_sound; auto. + ** apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + * ** apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + apply oper1_sound; auto. apply forward_move_rhs_sound; auto. Qed. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index d84a546d..b0d3740e 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -31,6 +31,7 @@ let option_fcse3 = ref true let option_fcse3_alias_analysis = ref true let option_fcse3_across_calls = ref false let option_fcse3_across_merges = ref true +let option_fcse3_glb = ref true let option_fredundancy = ref true let option_fduplicate = ref (-1) let option_finvertcond = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index 445f5793..d576ede6 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -54,6 +54,9 @@ Parameter optim_CSE3_across_calls: unit -> bool. (** Flag -fcse3-across-calls. For DMonniaux's common subexpression elimination. Propagate information across control-flow merges (may increase register pressure). *) Parameter optim_CSE3_across_merges: unit -> bool. +(** Flag -fcse3-glb *) +Parameter optim_CSE3_glb: unit -> bool. + (** Flag -fmove-loop-invariants. *) Parameter optim_move_loop_invariants: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 9d1caa9e..90afb812 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -201,6 +201,7 @@ Processing options: -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on] -fcse3-across-calls Propagate CSE3 information across function calls [off] -fcse3-across-merges Propagate CSE3 information across control-flow merges [on] + -fcse3-glb Refine CSE3 information using greatest lower bounds [on] -fmove-loop-invariants Perform loop-invariant code motion [off] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] @@ -415,6 +416,7 @@ let cmdline_actions = @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis @ f_opt "cse3-across-calls" option_fcse3_across_calls @ f_opt "cse3-across-merges" option_fcse3_across_merges + @ f_opt "cse3-glb" option_fcse3_glb @ f_opt "move-loop-invariants" option_fmove_loop_invariants @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass diff --git a/extraction/extraction.v b/extraction/extraction.v index a7772224..e43594fc 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -127,6 +127,8 @@ Extract Constant Compopts.optim_CSE3_across_calls => "fun _ -> !Clflags.option_fcse3_across_calls". Extract Constant Compopts.optim_CSE3_across_merges => "fun _ -> !Clflags.option_fcse3_across_merges". +Extract Constant Compopts.optim_CSE3_glb => + "fun _ -> !Clflags.option_fcse3_glb". Extract Constant Compopts.optim_move_loop_invariants => "fun _ -> !Clflags.option_fmove_loop_invariants". |