From dc43cc3371f7837cff5b8d1fd536aba54e99232f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 23 Apr 2020 09:00:46 +0200 Subject: CSE3analysisaux: pp_rhs --- backend/CSE3analysisaux.ml | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'backend') diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 23e20ea8..0260f3b1 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -37,6 +37,14 @@ let print_set s = List.iter (fun i -> Printf.printf "%d; " (P.to_int i)) (PSet.elements s); Printf.printf "}\n";; +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 preanalysis (tenv : typing_env) (f : RTL.coq_function) = let cur_eq_id = ref 0 and cur_catalog = ref PTree.empty @@ -48,6 +56,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let eq_find_oracle node eq = Hashtbl.find_opt eq_table (flatten_eq eq) and rhs_find_oracle node sop args = + (* Printf.printf "query for %a\n" pp_rhs (sop, args); *) match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with | None -> PSet.empty | Some s -> s in -- cgit From 69447b8515c0bd123c6aa72c5545cf9beda79ec4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 23 Apr 2020 11:43:06 +0200 Subject: fix in CSE3 move propagation --- backend/CSE3analysis.v | 19 ++++++++++++++----- backend/CSE3analysisaux.ml | 39 ++++++++++++++++++++++++++++++--------- backend/CSE3analysisproof.v | 26 ++++++++++++++++++-------- 3 files changed, 62 insertions(+), 22 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index b495371d..91064a5d 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) diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 0260f3b1..e8e608da 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -32,10 +32,10 @@ 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 @@ -45,6 +45,16 @@ let pp_rhs oc (sop, args) = (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 and cur_catalog = ref PTree.empty @@ -54,14 +64,21 @@ 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 + 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 = - (* Printf.printf "query for %a\n" pp_rhs (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 + 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 @@ -88,6 +105,10 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = | _, _ -> ()); Some coq_id end + in + 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..116353fa 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. -- cgit From 2316b5dc954b4047f3f48c61e7f4e34deb729efe Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 23 Apr 2020 12:29:38 +0200 Subject: make tracing output optional --- backend/CSE3analysisaux.ml | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index e8e608da..3f7d5bb9 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -65,16 +65,18 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = and cur_moves = ref (PMap.init PSet.empty) in let eq_find_oracle node eq = let o = Hashtbl.find_opt eq_table (flatten_eq eq) in - Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node) - pp_eq eq (pp_option pp_P) o; + (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 = let o = match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with | None -> PSet.empty | Some s -> s in - Printf.printf "@%d: rhs_find %a = %a\n" (P.to_int node) pp_rhs (sop, args) - pp_set o; + (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 @@ -106,8 +108,9 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = Some coq_id end in - Printf.printf "@%d: mutating_eq_find %a -> %a\n" (P.to_int node) - pp_eq eq (pp_option pp_P) o; + (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 -- cgit