diff options
| -rw-r--r-- | backend/CSE3analysis.v | 22 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 21 | ||||
| -rw-r--r-- | driver/Clflags.ml | 3 | ||||
| -rw-r--r-- | driver/Compopts.v | 5 | ||||
| -rw-r--r-- | driver/Driver.ml | 4 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 |
6 files changed, 44 insertions, 13 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 91064a5d..ef487c86 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -344,16 +344,28 @@ Section OPERATIONS. Definition apply_external_call ef (rel : RELATION.t) : RELATION.t := match ef with - | EF_builtin name sg - | EF_runtime name sg => + | EF_builtin name sg => match Builtins.lookup_builtin_function name sg with | Some bf => rel - | None => kill_mem rel + | None => if Compopts.optim_CSE3_across_calls tt + then kill_mem rel + else RELATION.top end - | EF_malloc (* FIXME *) + | EF_runtime name sg => + if Compopts.optim_CSE3_across_calls tt + then + match Builtins.lookup_builtin_function name sg with + | Some bf => rel + | None => kill_mem rel + end + else RELATION.top + | EF_malloc | EF_external _ _ + | EF_free => + if Compopts.optim_CSE3_across_calls tt + then kill_mem rel + else RELATION.top | EF_vstore _ - | EF_free (* FIXME *) | EF_memcpy _ _ (* FIXME *) | EF_inline_asm _ _ _ => kill_mem rel | _ => rel diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 116353fa..c65a6d9e 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -917,6 +917,17 @@ Section SOUNDNESS. Hint Resolve kill_builtin_res_sound : cse3. + Lemma top_sound: + forall rs m, (sem_rel RELATION.top rs m). + Proof. + unfold RELATION.top, sem_rel. + intros. + rewrite PSet.gempty in H. + discriminate. + Qed. + + Hint Resolve top_sound : cse3. + Lemma external_call_sound: forall ge ef (rel : RELATION.t) (m m' : mem) (rs : regset) vargs t vres (REL : sem_rel rel rs m) @@ -926,11 +937,11 @@ Section SOUNDNESS. destruct ef; intros; simpl in *. all: eauto using kill_mem_sound. all: unfold builtin_or_external_sem in *. - 1, 2: destruct (Builtins.lookup_builtin_function name sg); - eauto using kill_mem_sound; - inv CALL; eauto using kill_mem_sound. - all: inv CALL. - all: eauto using kill_mem_sound. + 1, 2, 3, 5, 6: destruct (Compopts.optim_CSE3_across_calls tt). + all: eauto using kill_mem_sound, top_sound. + 1, 2, 3: destruct (Builtins.lookup_builtin_function name sg). + all: eauto using kill_mem_sound, top_sound. + all: inv CALL; eauto using kill_mem_sound. Qed. Hint Resolve external_call_sound : cse3. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b9828f15..9d868de3 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -25,10 +25,11 @@ let option_ffpu = ref true let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true let option_fconstprop = ref true -let option_fcse = ref false +let option_fcse = ref true let option_fcse2 = ref false let option_fcse3 = ref true let option_fcse3_alias_analysis = ref true +let option_fcse3_across_calls = ref false 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 5acd2640..fb3481e2 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -45,9 +45,12 @@ Parameter optim_CSE2: unit -> bool. (** Flag -fcse3. For DMonniaux's common subexpression elimination. *) Parameter optim_CSE3: unit -> bool. -(** Flag -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. *) +(** Flag -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. Perform a simple alias analysis. *) Parameter optim_CSE3_alias_analysis: unit -> bool. +(** Flag -fcse3-across-calls. For DMonniaux's common subexpression elimination. Propagate information across function calls (may increase register pressure). *) +Parameter optim_CSE3_across_calls: unit -> bool. + (** Flag -fmove-loop-invariants. *) Parameter optim_move_loop_invariants: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 4e4bab16..ea9af62e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -195,10 +195,11 @@ Processing options: -fconst-prop Perform global constant propagation [on] -ffloat-const-prop <n> Control constant propagation of floats (<n>=0: none, <n>=1: limited, <n>=2: full; default is full) - -fcse Perform common subexpression elimination [off] + -fcse Perform common subexpression elimination [on] -fcse2 Perform inter-loop common subexpression elimination [off] -fcse3 Perform inter-loop common subexpression elimination [on] -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on] + -fcse3-across-calls Propagate CSE3 information across function calls [off] -fmove-loop-invariants Perform loop-invariant code motion [off] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] @@ -403,6 +404,7 @@ let cmdline_actions = @ f_opt "cse2" option_fcse2 @ f_opt "cse3" option_fcse3 @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis + @ f_opt "cse3-across-calls" option_fcse3_across_calls @ 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 b6aa3409..fc906631 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -123,6 +123,8 @@ Extract Constant Compopts.optim_CSE3 => "fun _ -> !Clflags.option_fcse3". Extract Constant Compopts.optim_CSE3_alias_analysis => "fun _ -> !Clflags.option_fcse3_alias_analysis". +Extract Constant Compopts.optim_CSE3_across_calls => + "fun _ -> !Clflags.option_fcse3_across_calls". Extract Constant Compopts.optim_move_loop_invariants => "fun _ -> !Clflags.option_fmove_loop_invariants". |