diff options
| -rw-r--r-- | backend/CSE3analysis.v | 41 | ||||
| -rw-r--r-- | backend/CSE3analysisaux.ml | 49 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 47 | ||||
| -rw-r--r-- | driver/Clflags.ml | 5 | ||||
| -rw-r--r-- | driver/Compopts.v | 5 | ||||
| -rw-r--r-- | driver/Driver.ml | 5 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 |
7 files changed, 119 insertions, 35 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index b495371d..ef487c86 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -274,11 +274,20 @@ Section OPERATIONS. Definition oper (dst : reg) (op: sym_op) (args : list reg) (rel : RELATION.t) : RELATION.t := - match rhs_find op (forward_move_l rel args) rel with - | Some r => RELATION.glb (move r dst rel) - (oper1 dst op args rel) - | None => oper1 dst op args rel - end. + if is_smove op + then + match args with + | src::nil => + move (forward_move rel src) dst rel + | _ => kill_reg dst rel + end + 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) *) + | None => oper1 dst op args' rel + end. Definition clever_kill_store (chunk : memory_chunk) (addr: addressing) (args : list reg) @@ -335,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/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 23e20ea8..3f7d5bb9 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -32,10 +32,28 @@ let print_eq channel (lhs, sop, args) = Printf.printf "%a = %s @ %a\n" print_reg lhs (string_of_chunk chunk) (PrintOp.print_addressing print_reg) (addr, args);; -let print_set s = - Printf.printf "{ "; - List.iter (fun i -> Printf.printf "%d; " (P.to_int i)) (PSet.elements s); - Printf.printf "}\n";; +let pp_set oc s = + Printf.fprintf oc "{ "; + List.iter (fun i -> Printf.fprintf oc "%d; " (P.to_int i)) (PSet.elements s); + Printf.fprintf oc "}";; + +let pp_rhs oc (sop, args) = + match sop with + | SOp op -> PrintOp.print_operation PrintRTL.reg oc (op, args) + | SLoad(chunk, addr) -> + Printf.fprintf oc "%s[%a]" + (PrintAST.name_of_chunk chunk) + (PrintOp.print_addressing PrintRTL.reg) (addr, args);; + +let pp_eq oc eq = + Printf.fprintf oc "x%d = %a" (P.to_int eq.eq_lhs) + pp_rhs (eq.eq_op, eq.eq_args);; + +let pp_P oc x = Printf.fprintf oc "%d" (P.to_int x) + +let pp_option pp oc = function + | None -> output_string oc "none" + | Some x -> pp oc x;; let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let cur_eq_id = ref 0 @@ -46,13 +64,23 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = and cur_kill_mem = ref PSet.empty and cur_moves = ref (PMap.init PSet.empty) in let eq_find_oracle node eq = - Hashtbl.find_opt eq_table (flatten_eq eq) + let o = Hashtbl.find_opt eq_table (flatten_eq eq) in + (if !Clflags.option_debug_compcert > 1 + then Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node) + pp_eq eq (pp_option pp_P) o); + o and rhs_find_oracle node sop args = - match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with - | None -> PSet.empty - | Some s -> s in + let o = + match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with + | None -> PSet.empty + | Some s -> s in + (if !Clflags.option_debug_compcert > 1 + then Printf.printf "@%d: rhs_find %a = %a\n" + (P.to_int node) pp_rhs (sop, args) pp_set o); + o in let mutating_eq_find_oracle node eq : P.t option = let (flat_eq_lhs, flat_eq_op, flat_eq_args) as flat_eq = flatten_eq eq in + let o = match Hashtbl.find_opt eq_table flat_eq with | Some x -> Some x @@ -79,6 +107,11 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = | _, _ -> ()); Some coq_id end + in + (if !Clflags.option_debug_compcert > 1 + then Printf.printf "@%d: mutating_eq_find %a -> %a\n" (P.to_int node) + pp_eq eq (pp_option pp_P) o); + o in match internal_analysis diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 3ea5e078..c65a6d9e 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -778,15 +778,25 @@ Section SOUNDNESS. intros until v. intros REL RHS. unfold oper. - destruct rhs_find as [src |] eqn:RHS_FIND. - - 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. + destruct (is_smove sop). + - subst. + simpl in RHS. + destruct args. contradiction. + destruct args. 2: contradiction. + cbn in *. + subst. + 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. *) + apply oper1_sound; auto. - - apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. Qed. Hint Resolve oper_sound : cse3. @@ -907,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) @@ -916,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 bb40844e..8f3b6605 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 @@ -89,6 +90,6 @@ let option_fmove_loop_invariants = ref true let option_fnontrap_loads = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 - let option_profile_arcs = ref false let option_fbranch_probabilities = ref true +let option_debug_compcert = ref 0 diff --git a/driver/Compopts.v b/driver/Compopts.v index 58ac62b7..3c5ccf36 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 20c10ace..b9060ca7 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] @@ -339,6 +340,7 @@ let cmdline_actions = Exact "-Obranchless", Set option_Obranchless; Exact "-fprofile-use=", String (fun s -> Profilingaux.load_profiling_info s); Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n); + Exact "-debug-compcert", Integer (fun n -> option_debug_compcert := n); Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); @@ -410,6 +412,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 9070e26d..b40d444a 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". |