From f59c540aa7cf85c89ee0cb07c20374c8ad76a46c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 27 Oct 2020 15:21:11 +0100 Subject: new CSE3 --- backend/CSE3analysis.v | 38 ++++++++++++++---------------- backend/CSE3analysisaux.ml | 57 ++++++++++++++++++++++++++++++++++++--------- backend/CSE3analysisproof.v | 53 ++++++++++++++++++++++++++++++++++------- 3 files changed, 107 insertions(+), 41 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 7316c9a9..cd7e3d84 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -282,12 +282,14 @@ Section OPERATIONS. Definition oper2 (dst : reg) (op: sym_op)(args : list reg) (rel : RELATION.t) : RELATION.t := - let rel' := kill_reg dst rel in match eq_find {| eq_lhs := dst; eq_op := op; eq_args:= args |} with - | Some id => PSet.add id rel' - | None => rel' + | Some id => + if PSet.contains rel id + then rel + else PSet.add id (kill_reg dst rel) + | None => kill_reg dst rel end. Definition oper1 (dst : reg) (op: sym_op) (args : list reg) @@ -307,12 +309,6 @@ Section OPERATIONS. | Some eq_id => PSet.add eq_id (kill_reg dst rel) | None => kill_reg dst rel end. - - Definition is_trivial_sym_op sop := - match sop with - | SOp op => is_trivial_op op - | SLoad _ _ => false - end. Definition oper (dst : reg) (op: sym_op) (args : list reg) (rel : RELATION.t) : RELATION.t := @@ -324,18 +320,18 @@ Section OPERATIONS. | _ => kill_reg dst rel end else - if is_trivial_sym_op op - then kill_reg dst rel - else - let args' := forward_move_l rel args in - match rhs_find op args' rel with - | 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. + let args' := forward_move_l rel args in + match rhs_find op args' rel with + | Some r => + if Compopts.optim_CSE3_glb tt + then RELATION.glb (move r dst rel) + (RELATION.glb (oper1 dst op args' rel) + (oper1 dst op args rel)) + else RELATION.glb (oper1 dst op args' rel) + (oper1 dst op args rel) + | None => RELATION.glb (oper1 dst op args' rel) + (oper1 dst op args rel) + end. Definition clever_kill_store (chunk : memory_chunk) (addr: addressing) (args : list reg) diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 3990b765..8c83dc2e 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -39,12 +39,12 @@ let print_reg channel i = let print_eq channel (lhs, sop, args) = match sop with | SOp op -> - Printf.printf "%a = %a\n" print_reg lhs (PrintOp.print_operation print_reg) (op, args) + Printf.printf "%a = %a" print_reg lhs (PrintOp.print_operation print_reg) (op, args) | SLoad(chunk, addr) -> - Printf.printf "%a = %s @ %a\n" print_reg lhs (string_of_chunk chunk) + Printf.printf "%a = %s @ %a" print_reg lhs (string_of_chunk chunk) (PrintOp.print_addressing print_reg) (addr, args);; -let pp_set oc s = +let pp_intset oc s = Printf.fprintf oc "{ "; List.iter (fun i -> Printf.fprintf oc "%d; " (P.to_int i)) (PSet.elements s); Printf.fprintf oc "}";; @@ -70,6 +70,38 @@ let pp_option pp oc = function let is_trivial eq = (eq.eq_op = SOp Op.Omove) && (eq.eq_args = [eq.eq_lhs]);; +let rec pp_list separator pp_item chan = function + | [] -> () + | [h] -> pp_item chan h + | h::t -> + pp_item chan h; + output_string chan separator; + pp_list separator pp_item chan t;; + +let pp_set separator pp_item chan s = + pp_list separator pp_item chan (PSet.elements s);; + +let pp_equation hints chan x = + match PTree.get x hints.hint_eq_catalog with + | None -> output_string chan "???" + | Some eq -> + print_eq chan (P.to_int eq.eq_lhs, eq.eq_op, List.map P.to_int eq.eq_args);; + +let pp_relation hints chan rel = + pp_set "; " (pp_equation hints) chan rel;; + +let pp_relation_b hints chan = function + | None -> output_string chan "bot" + | Some rel -> pp_relation hints chan rel;; + +let pp_results f (invariants : RB.t PMap.t) hints chan = + let max_pc = P.to_int (RTL.max_pc_function f) in + for pc=max_pc downto 1 + do + Printf.fprintf chan "%d: %a\n" pc + (pp_relation_b hints) (PMap.get (P.of_int pc) invariants) + done + let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let cur_eq_id = ref 0 and cur_catalog = ref PTree.empty @@ -81,7 +113,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let eq_find_oracle node eq = assert (not (is_trivial eq)); let o = Hashtbl.find_opt eq_table (flatten_eq eq) in - (if !Clflags.option_debug_compcert > 1 + (if !Clflags.option_debug_compcert > 5 then Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node) pp_eq eq (pp_option pp_P) o); o @@ -90,9 +122,9 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = 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 + (if !Clflags.option_debug_compcert > 5 then Printf.printf "@%d: rhs_find %a = %a\n" - (P.to_int node) pp_rhs (sop, args) pp_set o); + (P.to_int node) pp_rhs (sop, args) pp_intset 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 @@ -124,7 +156,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = Some coq_id end in - (if !Clflags.option_debug_compcert > 1 + (if !Clflags.option_debug_compcert > 5 then Printf.printf "@%d: mutating_eq_find %a -> %a\n" (P.to_int node) pp_eq eq (pp_option pp_P) o); o @@ -140,7 +172,10 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = } tenv f with None -> failwith "CSE3analysisaux analysis failed, try re-running with -fno-cse3" | Some invariants -> - invariants, - { hint_eq_catalog = !cur_catalog; - hint_eq_find_oracle= eq_find_oracle; - hint_eq_rhs_oracle = rhs_find_oracle };; + let hints = { hint_eq_catalog = !cur_catalog; + hint_eq_find_oracle= eq_find_oracle; + hint_eq_rhs_oracle = rhs_find_oracle } in + (if !Clflags.option_debug_compcert > 1 + then pp_results f invariants hints stdout); + invariants, hints +;; diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 66b199cc..ea4d37ca 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -699,6 +699,28 @@ Section SOUNDNESS. + congruence. Qed. + + Lemma arglist_idem_write: + forall { A : Type} args (rs : Regmap.t A) dst, + (rs # dst <- (rs # dst)) ## args = rs ## args. + Proof. + induction args; trivial. + intros. cbn. + f_equal; trivial. + apply Regmap.gsident. + Qed. + + Lemma sem_rhs_idem_write: + forall sop args rs dst m v, + sem_rhs sop args rs m v -> + sem_rhs sop args (rs # dst <- (rs # dst)) m v. + Proof. + intros. + unfold sem_rhs in *. + rewrite arglist_idem_write. + assumption. + Qed. + Theorem oper2_sound: forall no dst sop args rel rs m v, sem_rel rel rs m -> @@ -726,6 +748,17 @@ Section SOUNDNESS. rewrite Regmap.gss. apply sem_rhs_depends_on_args_only; auto. } + intros INi. + destruct (PSet.contains rel e) eqn:CONTAINSe. + { pose proof (REL e {| eq_lhs := dst; eq_op := sop; eq_args := args |} CONTAINSe H) as RELe. + pose proof (REL i eq CONTAINS INi) as RELi. + unfold sem_eq in *. + cbn in RELe. + replace v with (rs # dst) by (eapply sem_rhs_det; eassumption). + rewrite Regmap.gsident. + apply sem_rhs_idem_write. + assumption. + } rewrite PSet.gaddo in CONTAINS by congruence. apply (kill_reg_sound rel rs m dst v REL i eq); auto. Qed. @@ -821,11 +854,7 @@ Section SOUNDNESS. subst. rewrite <- (forward_move_sound rel rs m r) by auto. apply move_sound; auto. - - destruct (is_trivial_sym_op sop). - { - apply kill_reg_sound; auto. - } - destruct rhs_find as [src |] eqn:RHS_FIND. + - destruct rhs_find as [src |] eqn:RHS_FIND. + 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. @@ -833,12 +862,18 @@ Section SOUNDNESS. 2: eassumption. rewrite <- (sem_rhs_det SOUND RHS). apply move_sound; auto. + ** apply sem_rel_glb; split. + *** apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + *** apply oper1_sound; auto. + * apply sem_rel_glb; split. ** 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. + ** apply oper1_sound; auto. + + apply sem_rel_glb; split. + * apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + * apply oper1_sound; auto. Qed. Hint Resolve oper_sound : cse3. -- cgit