diff options
| -rw-r--r-- | backend/CSE3analysis.v | 133 | ||||
| -rw-r--r-- | backend/CSE3analysisaux.ml | 57 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 195 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 |
4 files changed, 197 insertions, 190 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 84f4a426..137282a4 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -145,14 +145,11 @@ Proof. exact peq. Defined. -Record equation := - mkequation - { eq_lhs : reg; - eq_op : sym_op; - eq_args : list reg }. +Inductive equation_or_condition := + | Equ : reg -> sym_op -> list reg -> equation_or_condition. Definition eq_dec_equation : - forall eq eq' : equation, {eq = eq'} + {eq <> eq'}. + forall eq eq' : equation_or_condition, {eq = eq'} + {eq <> eq'}. Proof. generalize peq. generalize eq_dec_sym_op. @@ -160,20 +157,6 @@ Proof. decide equality. Defined. -Record condition_fact := - mkcondition_fact - { cond_op : condition ; - cond_args : list reg }. - -Definition eq_dec_condition_fact : - forall cf cf' : condition_fact, {cf = cf'} + {cf <> cf'}. -Proof. - generalize peq. - generalize eq_condition. - generalize eq_dec_args. - decide equality. -Defined. - Definition eq_id := node. Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := @@ -182,34 +165,43 @@ Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := Definition add_ilist_j (ilist : list reg) (j : eq_id) (m : Regmap.t PSet.t) := List.fold_left (fun already i => add_i_j i j already) ilist m. -Definition get_reg_kills (eqs : PTree.t equation) : +Definition get_reg_kills (eqs : PTree.t equation_or_condition) : Regmap.t PSet.t := - PTree.fold (fun already (eqno : eq_id) (eq : equation) => - add_i_j (eq_lhs eq) eqno - (add_ilist_j (eq_args eq) eqno already)) eqs + PTree.fold (fun already (eqno : eq_id) (eq_cond : equation_or_condition) => + match eq_cond with + | Equ lhs sop args => + add_i_j lhs eqno + (add_ilist_j args eqno already) + end) eqs (PMap.init PSet.empty). -Definition eq_depends_on_mem eq := - match eq_op eq with - | SLoad _ _ => true - | SOp op => op_depends_on_memory op +Definition eq_cond_depends_on_mem eq_cond := + match eq_cond with + | Equ lhs sop args => + match sop with + | SLoad _ _ => true + | SOp op => op_depends_on_memory op + end end. -Definition eq_depends_on_store eq := - match eq_op eq with - | SLoad _ _ => true - | SOp op => false +Definition eq_cond_depends_on_store eq_cond := + match eq_cond with + | Equ lhs sop args => + match sop with + | SLoad _ _ => true + | SOp op => false + end end. -Definition get_mem_kills (eqs : PTree.t equation) : PSet.t := - PTree.fold (fun already (eqno : eq_id) (eq : equation) => - if eq_depends_on_mem eq +Definition get_mem_kills (eqs : PTree.t equation_or_condition) : PSet.t := + PTree.fold (fun already (eqno : eq_id) (eq : equation_or_condition) => + if eq_cond_depends_on_mem eq then PSet.add eqno already else already) eqs PSet.empty. -Definition get_store_kills (eqs : PTree.t equation) : PSet.t := - PTree.fold (fun already (eqno : eq_id) (eq : equation) => - if eq_depends_on_store eq +Definition get_store_kills (eqs : PTree.t equation_or_condition) : PSet.t := + PTree.fold (fun already (eqno : eq_id) (eq : equation_or_condition) => + if eq_cond_depends_on_store eq then PSet.add eqno already else already) eqs PSet.empty. @@ -229,21 +221,24 @@ Proof. - right; congruence. Qed. -Definition get_moves (eqs : PTree.t equation) : +Definition get_moves (eqs : PTree.t equation_or_condition) : Regmap.t PSet.t := - PTree.fold (fun already (eqno : eq_id) (eq : equation) => - if is_smove (eq_op eq) - then add_i_j (eq_lhs eq) eqno already - else already) eqs (PMap.init PSet.empty). + PTree.fold (fun already (eqno : eq_id) (eq : equation_or_condition) => + match eq with + | Equ lhs sop args => + if is_smove sop + then add_i_j lhs eqno already + else already + end) eqs (PMap.init PSet.empty). Record eq_context := mkeqcontext - { eq_catalog : eq_id -> option equation; - eq_find_oracle : node -> equation -> option eq_id; - eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t; - eq_kill_reg : reg -> PSet.t; - eq_kill_mem : unit -> PSet.t; - eq_kill_store : unit -> PSet.t; - eq_moves : reg -> PSet.t }. + { eq_catalog : eq_id -> option equation_or_condition; + eq_find_oracle : node -> equation_or_condition -> option eq_id; + eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t; + eq_kill_reg : reg -> PSet.t; + eq_kill_mem : unit -> PSet.t; + eq_kill_store : unit -> PSet.t; + eq_moves : reg -> PSet.t }. Section OPERATIONS. Context {ctx : eq_context}. @@ -265,10 +260,10 @@ Section OPERATIONS. | None => x | Some eqno => match eq_catalog ctx eqno with - | Some eq => - if is_smove (eq_op eq) && peq x (eq_lhs eq) + | Some (Equ lhs sop args) => + if is_smove sop && peq x lhs then - match eq_args eq with + match args with | src::nil => src | _ => x end @@ -283,7 +278,7 @@ Section OPERATIONS. Section PER_NODE. Variable no : node. - Definition eq_find (eq : equation) := + Definition eq_find (eq : equation_or_condition) := match eq_find_oracle ctx no eq with | Some id => match eq_catalog ctx id with @@ -300,18 +295,16 @@ Section OPERATIONS. | Some src => match eq_catalog ctx src with | None => None - | Some eq => - if eq_dec_sym_op sop (eq_op eq) && eq_dec_args args (eq_args eq) - then Some (eq_lhs eq) + | Some (Equ eq_lhs eq_sop eq_args) => + if eq_dec_sym_op sop eq_sop && eq_dec_args args eq_args + then Some eq_lhs else None end end. Definition oper2 (dst : reg) (op: sym_op)(args : list reg) (rel : RELATION.t) : RELATION.t := - match eq_find {| eq_lhs := dst; - eq_op := op; - eq_args:= args |} with + match eq_find (Equ dst op args) with | Some id => if PSet.contains rel id then rel @@ -330,9 +323,7 @@ Section OPERATIONS. if peq src dst then rel else - match eq_find {| eq_lhs := dst; - eq_op := SOp Omove; - eq_args:= src::nil |} with + match eq_find (Equ dst (SOp Omove) (src::nil)) with | Some eq_id => PSet.add eq_id (kill_reg dst rel) | None => kill_reg dst rel end. @@ -380,13 +371,13 @@ Section OPERATIONS. (PSet.filter (fun eqno => match eq_catalog ctx eqno with - | None => false - | Some eq => - match eq_op eq with + | Some (Equ eq_lhs eq_sop eq_args) => + match eq_sop with | SOp op => true | SLoad chunk' addr' => - may_overlap chunk addr args chunk' addr' (eq_args eq) + may_overlap chunk addr args chunk' addr' eq_args end + | _ => false end) (PSet.inter rel (eq_kill_store ctx tt))). @@ -405,9 +396,7 @@ Section OPERATIONS. let rel' := store2 chunk addr args src rel in if loadv_storev_compatible_type chunk ty then - match eq_find {| eq_lhs := src; - eq_op := SLoad chunk addr; - eq_args:= args |} with + match eq_find (Equ src (SLoad chunk addr) args) with | Some id => PSet.add id rel' | None => rel' end @@ -523,8 +512,8 @@ End OPERATIONS. Record analysis_hints := mkanalysis_hints - { hint_eq_catalog : PTree.t equation; - hint_eq_find_oracle : node -> equation -> option eq_id; + { hint_eq_catalog : PTree.t equation_or_condition; + hint_eq_find_oracle : node -> equation_or_condition -> option eq_id; hint_eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t }. Definition context_from_hints (hints : analysis_hints) := diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index e038331c..f50f4a46 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -16,8 +16,12 @@ open HashedSet open Camlcoq open Coqlib -let flatten_eq eq = - ((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);; +type flattened_equation_or_condition = + | Flat_equ of int * sym_op * int list;; + +let flatten_eq = function + | Equ(lhs, sop, args) -> + Flat_equ((P.to_int lhs), sop, (List.map P.to_int args));; let imp_add_i_j s i j = s := PMap.set i (PSet.add j (PMap.get i !s)) !s;; @@ -58,9 +62,11 @@ 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_eq oc eq_cond = + match eq_cond with + | Equ(lhs, sop, args) -> + Printf.fprintf oc "x%d = %a" (P.to_int lhs) + pp_rhs (sop, args);; let pp_P oc x = Printf.fprintf oc "%d" (P.to_int x) @@ -68,8 +74,9 @@ let pp_option pp oc = function | None -> output_string oc "none" | Some x -> pp oc x;; -let is_trivial eq = - (eq.eq_op = SOp Op.Omove) && (eq.eq_args = [eq.eq_lhs]);; +let is_trivial = function + | Equ(lhs, (SOp Op.Omove), [lhs']) -> lhs=lhs' + | _ -> false;; let rec pp_list separator pp_item chan = function | [] -> () @@ -86,7 +93,9 @@ 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);; + match eq with + Equ(lhs, sop, args) -> + print_eq chan (P.to_int lhs, sop, List.map P.to_int args);; let pp_relation hints chan rel = pp_set "; " (pp_equation hints) chan rel;; @@ -194,7 +203,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = (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 + let flat_eq = flatten_eq eq in let o = match Hashtbl.find_opt eq_table flat_eq with | Some x -> @@ -207,21 +216,25 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = begin Hashtbl.add eq_table flat_eq coq_id; (cur_catalog := PTree.set coq_id eq !cur_catalog); - Hashtbl.add rhs_table (flat_eq_op, flat_eq_args) - (PSet.add coq_id - (match Hashtbl.find_opt rhs_table (flat_eq_op, flat_eq_args) with - | None -> PSet.empty - | Some s -> s)); - List.iter - (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) - (eq.eq_lhs :: eq.eq_args); - (if eq_depends_on_mem eq + (match flat_eq with + | Flat_equ(flat_eq_lhs, flat_eq_op, flat_eq_args) -> + Hashtbl.add rhs_table (flat_eq_op, flat_eq_args) + (PSet.add coq_id + (match Hashtbl.find_opt rhs_table (flat_eq_op, flat_eq_args) with + | None -> PSet.empty + | Some s -> s))); + (match eq with + | Equ(lhs, sop, args) -> + List.iter + (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) + (lhs :: args); + match sop, args with + | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves lhs coq_id + | _, _ -> ()); + (if eq_cond_depends_on_mem eq then cur_kill_mem := PSet.add coq_id !cur_kill_mem); - (if eq_depends_on_store eq + (if eq_cond_depends_on_store eq then cur_kill_store := PSet.add coq_id !cur_kill_store); - (match eq.eq_op, eq.eq_args with - | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves eq.eq_lhs coq_id - | _, _ -> ()); Some coq_id end in diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index b298ea65..5fcaa048 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -127,22 +127,34 @@ Proof. Qed. Hint Resolve add_ilist_j_adds: cse3. -Definition xlget_kills (eqs : list (eq_id * equation)) (m : Regmap.t PSet.t) : +Definition xlget_kills (eqs : list (eq_id * equation_or_condition)) + (m : Regmap.t PSet.t) : Regmap.t PSet.t := - List.fold_left (fun already (item : eq_id * equation) => - add_i_j (eq_lhs (snd item)) (fst item) - (add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m. - -Definition xlget_mem_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t := + List.fold_left (fun already (item : eq_id * equation_or_condition) => + match snd item with + | Equ lhs sop args => + add_i_j lhs (fst item) + (add_ilist_j args (fst item) already) + end) eqs m. + +Definition xlget_mem_kills (eqs : list (positive * equation_or_condition)) + (m : PSet.t) : PSet.t := (fold_left - (fun (a : PSet.t) (p : positive * equation) => - if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a) + (fun (a : PSet.t) (item : positive * equation_or_condition) => + if eq_cond_depends_on_mem (snd item) + then PSet.add (fst item) a + else a + ) eqs m). -Definition xlget_store_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t := +Definition xlget_store_kills (eqs : list (positive * equation_or_condition)) + (m : PSet.t) : PSet.t := (fold_left - (fun (a : PSet.t) (p : positive * equation) => - if eq_depends_on_store (snd p) then PSet.add (fst p) a else a) + (fun (a : PSet.t) (item : positive * equation_or_condition) => + if eq_cond_depends_on_store (snd item) + then PSet.add (fst item) a + else a + ) eqs m). Lemma xlget_kills_monotone : @@ -152,6 +164,8 @@ Lemma xlget_kills_monotone : Proof. induction eqs; simpl; trivial. intros. + destruct a as [id eq_cond]; cbn. + destruct eq_cond as [eq_lhs eq_sop eq_args]. auto with cse3. Qed. @@ -164,9 +178,10 @@ Lemma xlget_mem_kills_monotone : Proof. induction eqs; simpl; trivial. intros. - destruct eq_depends_on_mem. + destruct a as [id eq_cond]; cbn. + destruct eq_cond_depends_on_mem. - apply IHeqs. - destruct (peq (fst a) j). + destruct (peq id j). + subst j. apply PSet.gadds. + rewrite PSet.gaddo by congruence. trivial. @@ -182,9 +197,10 @@ Lemma xlget_store_kills_monotone : Proof. induction eqs; simpl; trivial. intros. - destruct eq_depends_on_store. + destruct a as [id eq_cond]; cbn. + destruct eq_cond_depends_on_store. - apply IHeqs. - destruct (peq (fst a) j). + destruct (peq id j). + subst j. apply PSet.gadds. + rewrite PSet.gaddo by congruence. trivial. @@ -195,9 +211,7 @@ Hint Resolve xlget_store_kills_monotone : cse3. Lemma xlget_kills_has_lhs : forall eqs m lhs sop args j, - In (j, {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |}) eqs -> + In (j, (Equ lhs sop args)) eqs -> PSet.contains (Regmap.get lhs (xlget_kills eqs m)) j = true. Proof. induction eqs; simpl. @@ -212,9 +226,7 @@ Hint Resolve xlget_kills_has_lhs : cse3. Lemma xlget_kills_has_arg : forall eqs m lhs sop arg args j, - In (j, {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |}) eqs -> + In (j, (Equ lhs sop args)) eqs -> In arg args -> PSet.contains (Regmap.get arg (xlget_kills eqs m)) j = true. Proof. @@ -231,18 +243,18 @@ Hint Resolve xlget_kills_has_arg : cse3. Lemma get_kills_has_lhs : forall eqs lhs sop args j, - PTree.get j eqs = Some {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + PTree.get j eqs = Some (Equ lhs sop args) -> PSet.contains (Regmap.get lhs (get_reg_kills eqs)) j = true. Proof. unfold get_reg_kills. intros. rewrite PTree.fold_spec. change (fold_left - (fun (a : Regmap.t PSet.t) (p : positive * equation) => - add_i_j (eq_lhs (snd p)) (fst p) - (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills. + (fun (a : Regmap.t PSet.t) (p : positive * equation_or_condition) => + match snd p with + | Equ lhs0 _ args0 => + add_i_j lhs0 (fst p) (add_ilist_j args0 (fst p) a) + end)) with xlget_kills. eapply xlget_kills_has_lhs. apply PTree.elements_correct. eassumption. @@ -252,9 +264,7 @@ Hint Resolve get_kills_has_lhs : cse3. Lemma context_from_hints_get_kills_has_lhs : forall hints lhs sop args j, - PTree.get j (hint_eq_catalog hints) = Some {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + PTree.get j (hint_eq_catalog hints) = Some (Equ lhs sop args) -> PSet.contains (eq_kill_reg (context_from_hints hints) lhs) j = true. Proof. intros; simpl. @@ -266,9 +276,7 @@ Hint Resolve context_from_hints_get_kills_has_lhs : cse3. Lemma get_kills_has_arg : forall eqs lhs sop arg args j, - PTree.get j eqs = Some {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + PTree.get j eqs = Some (Equ lhs sop args) -> In arg args -> PSet.contains (Regmap.get arg (get_reg_kills eqs)) j = true. Proof. @@ -276,9 +284,11 @@ Proof. intros. rewrite PTree.fold_spec. change (fold_left - (fun (a : Regmap.t PSet.t) (p : positive * equation) => - add_i_j (eq_lhs (snd p)) (fst p) - (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills. + (fun (a : Regmap.t PSet.t) (p : positive * equation_or_condition) => + match snd p with + | Equ lhs0 _ args0 => + add_i_j lhs0 (fst p) (add_ilist_j args0 (fst p) a) + end)) with xlget_kills. eapply xlget_kills_has_arg. - apply PTree.elements_correct. eassumption. @@ -289,9 +299,7 @@ Hint Resolve get_kills_has_arg : cse3. Lemma context_from_hints_get_kills_has_arg : forall hints lhs sop arg args j, - PTree.get j (hint_eq_catalog hints) = Some {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + PTree.get j (hint_eq_catalog hints) = Some (Equ lhs sop args) -> In arg args -> PSet.contains (eq_kill_reg (context_from_hints hints) arg) j = true. Proof. @@ -305,7 +313,7 @@ Hint Resolve context_from_hints_get_kills_has_arg : cse3. Lemma xlget_kills_has_eq_depends_on_mem : forall eqs eq j m, In (j, eq) eqs -> - eq_depends_on_mem eq = true -> + eq_cond_depends_on_mem eq = true -> PSet.contains (xlget_mem_kills eqs m) j = true. Proof. induction eqs; simpl. @@ -326,17 +334,16 @@ Hint Resolve xlget_kills_has_eq_depends_on_mem : cse3. Lemma get_kills_has_eq_depends_on_mem : forall eqs eq j, PTree.get j eqs = Some eq -> - eq_depends_on_mem eq = true -> + eq_cond_depends_on_mem eq = true -> PSet.contains (get_mem_kills eqs) j = true. Proof. intros. unfold get_mem_kills. rewrite PTree.fold_spec. change (fold_left - (fun (a : PSet.t) (p : positive * equation) => - if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a) - (PTree.elements eqs) PSet.empty) - with (xlget_mem_kills (PTree.elements eqs) PSet.empty). + (fun (a : PSet.t) (p : positive * equation_or_condition) => + if eq_cond_depends_on_mem (snd p) then PSet.add (fst p) a else a)) + with xlget_mem_kills. eapply xlget_kills_has_eq_depends_on_mem. apply PTree.elements_correct. eassumption. @@ -346,7 +353,7 @@ Qed. Lemma context_from_hints_get_kills_has_eq_depends_on_mem : forall hints eq j, PTree.get j (hint_eq_catalog hints) = Some eq -> - eq_depends_on_mem eq = true -> + eq_cond_depends_on_mem eq = true -> PSet.contains (eq_kill_mem (context_from_hints hints) tt) j = true. Proof. intros. @@ -359,7 +366,7 @@ Hint Resolve context_from_hints_get_kills_has_eq_depends_on_mem : cse3. Lemma xlget_kills_has_eq_depends_on_store : forall eqs eq j m, In (j, eq) eqs -> - eq_depends_on_store eq = true -> + eq_cond_depends_on_store eq = true -> PSet.contains (xlget_store_kills eqs m) j = true. Proof. induction eqs; simpl. @@ -380,17 +387,16 @@ Hint Resolve xlget_kills_has_eq_depends_on_store : cse3. Lemma get_kills_has_eq_depends_on_store : forall eqs eq j, PTree.get j eqs = Some eq -> - eq_depends_on_store eq = true -> + eq_cond_depends_on_store eq = true -> PSet.contains (get_store_kills eqs) j = true. Proof. intros. unfold get_store_kills. rewrite PTree.fold_spec. change (fold_left - (fun (a : PSet.t) (p : positive * equation) => - if eq_depends_on_store (snd p) then PSet.add (fst p) a else a) - (PTree.elements eqs) PSet.empty) - with (xlget_store_kills (PTree.elements eqs) PSet.empty). + (fun (a : PSet.t) (p : positive * equation_or_condition) => + if eq_cond_depends_on_store (snd p) then PSet.add (fst p) a else a)) + with xlget_store_kills. eapply xlget_kills_has_eq_depends_on_store. apply PTree.elements_correct. eassumption. @@ -400,7 +406,7 @@ Qed. Lemma context_from_hints_get_kills_has_eq_depends_on_store : forall hints eq j, PTree.get j (hint_eq_catalog hints) = Some eq -> - eq_depends_on_store eq = true -> + eq_cond_depends_on_store eq = true -> PSet.contains (eq_kill_store (context_from_hints hints) tt) j = true. Proof. intros. @@ -410,8 +416,11 @@ Qed. Hint Resolve context_from_hints_get_kills_has_eq_depends_on_store : cse3. -Definition eq_involves (eq : equation) (i : reg) := - i = (eq_lhs eq) \/ In i (eq_args eq). +Definition eq_involves (eq : equation_or_condition) (i : reg) := + match eq with + | Equ lhs sop args => + i = lhs \/ In i args + end. Section SOUNDNESS. Context {F V : Type}. @@ -440,8 +449,10 @@ Section SOUNDNESS. end end. - Definition sem_eq (eq : equation) (rs : regset) (m : mem) := - sem_rhs (eq_op eq) (eq_args eq) rs m (rs # (eq_lhs eq)). + Definition sem_eq (eq : equation_or_condition) (rs : regset) (m : mem) := + match eq with + | Equ lhs sop args => sem_rhs sop args rs m (rs # lhs) + end. Definition sem_rel (rel : RELATION.t) (rs : regset) (m : mem) := forall i eq, @@ -475,16 +486,12 @@ Section SOUNDNESS. Hypothesis ctx_kill_reg_has_lhs : forall lhs sop args j, - eq_catalog ctx j = Some {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + eq_catalog ctx j = Some (Equ lhs sop args) -> PSet.contains (eq_kill_reg ctx lhs) j = true. Hypothesis ctx_kill_reg_has_arg : forall lhs sop args j, - eq_catalog ctx j = Some {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> + eq_catalog ctx j = Some (Equ lhs sop args) -> forall arg, In arg args -> PSet.contains (eq_kill_reg ctx arg) j = true. @@ -492,13 +499,13 @@ Section SOUNDNESS. Hypothesis ctx_kill_mem_has_depends_on_mem : forall eq j, eq_catalog ctx j = Some eq -> - eq_depends_on_mem eq = true -> + eq_cond_depends_on_mem eq = true -> PSet.contains (eq_kill_mem ctx tt) j = true. Hypothesis ctx_kill_store_has_depends_on_store : forall eq j, eq_catalog ctx j = Some eq -> - eq_depends_on_store eq = true -> + eq_cond_depends_on_store eq = true -> PSet.contains (eq_kill_store ctx tt) j = true. Theorem kill_reg_sound : @@ -590,9 +597,11 @@ Section SOUNDNESS. destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG. 2: reflexivity. specialize REL with (i := r) (eq0 := eq). - destruct (is_smove (eq_op eq)) as [MOVE | ]. + destruct eq as [lhs sop args]; cbn in *. (* TODO *) + destruct (is_smove sop) as [MOVE | ]. 2: reflexivity. - destruct (peq x (eq_lhs eq)). + rewrite MOVE in *; cbn in *. + destruct (peq x lhs). 2: reflexivity. simpl. subst x. @@ -600,9 +609,8 @@ Section SOUNDNESS. rewrite PSet.ginter in ELEMENT. rewrite andb_true_iff in ELEMENT. unfold sem_eq in REL. - rewrite MOVE in REL. simpl in REL. - destruct (eq_args eq) as [ | h t]. + destruct args as [ | h t]. reflexivity. destruct t. 2: reflexivity. @@ -637,20 +645,19 @@ Section SOUNDNESS. rewrite PSet.gsubtract in SUBTRACT. rewrite andb_true_iff in SUBTRACT. intuition. - destruct (eq_op eq) as [op | chunk addr] eqn:OP. + destruct eq as [lhs sop args] eqn:EQ. + destruct sop as [op | chunk addr] eqn:OP. - specialize ctx_kill_mem_has_depends_on_mem with (eq0 := eq) (j := i). - unfold eq_depends_on_mem in ctx_kill_mem_has_depends_on_mem. - rewrite OP in ctx_kill_mem_has_depends_on_mem. + rewrite EQ in ctx_kill_mem_has_depends_on_mem. + unfold eq_cond_depends_on_mem in ctx_kill_mem_has_depends_on_mem. rewrite (op_depends_on_memory_correct genv sp op) with (m2 := m). assumption. destruct (op_depends_on_memory op) in *; trivial. rewrite ctx_kill_mem_has_depends_on_mem in H0; trivial. discriminate H0. - specialize ctx_kill_mem_has_depends_on_mem with (eq0 := eq) (j := i). - destruct eq as [lhs op args]; simpl in *. - rewrite OP in ctx_kill_mem_has_depends_on_mem. + rewrite EQ in ctx_kill_mem_has_depends_on_mem. rewrite negb_true_iff in H0. - rewrite OP in CATALOG. intuition. congruence. Qed. @@ -691,15 +698,14 @@ Section SOUNDNESS. rewrite PSet.gsubtract in SUBTRACT. rewrite andb_true_iff in SUBTRACT. intuition. - destruct (eq_op eq) as [op | chunk addr] eqn:OP. + destruct eq as [lhs sop args] eqn:EQ. + destruct sop as [op | chunk addr] eqn:OP. - rewrite op_valid_pointer_eq with (m2 := m). assumption. eapply store_preserves_validity; eauto. - specialize ctx_kill_store_has_depends_on_store with (eq0 := eq) (j := i). - destruct eq as [lhs op args]; simpl in *. - rewrite OP in ctx_kill_store_has_depends_on_store. + rewrite EQ in ctx_kill_store_has_depends_on_store. rewrite negb_true_iff in H0. - rewrite OP in CATALOG. intuition. congruence. Qed. @@ -742,9 +748,10 @@ Section SOUNDNESS. destruct (eq_catalog ctx src') as [eq | ] eqn:CATALOG. 2: discriminate. specialize REL with (i := src') (eq0 := eq). - destruct (eq_dec_sym_op sop (eq_op eq)). + destruct eq as [eq_lhs eq_sop eq_args] eqn:EQ. + destruct (eq_dec_sym_op sop eq_sop). 2: discriminate. - destruct (eq_dec_args args (eq_args eq)). + destruct (eq_dec_args args eq_args). 2: discriminate. simpl in FIND. intuition congruence. @@ -794,17 +801,14 @@ Section SOUNDNESS. sem_rel rel rs m -> sem_rhs sop args rs m v -> ~ In dst args -> - eq_find (ctx := ctx) no - {| eq_lhs := dst; - eq_op := sop; - eq_args:= args |} = Some eqno -> + eq_find (ctx := ctx) no (Equ dst sop args) = Some eqno -> sem_rel (PSet.add eqno (kill_reg (ctx := ctx) dst rel)) (rs # dst <- v) m. Proof. intros until v. intros REL RHS NOTIN FIND i eq CONTAINS CATALOG. destruct (peq i eqno). - subst i. - rewrite eq_find_sound with (no := no) (eq0 := {| eq_lhs := dst; eq_op := sop; eq_args := args |}) in CATALOG by exact FIND. + rewrite eq_find_sound with (no := no) (eq0 := Equ dst sop args) in CATALOG by exact FIND. clear FIND. inv CATALOG. unfold sem_eq. @@ -862,7 +866,7 @@ Section SOUNDNESS. unfold oper2. intros until v. intros REL NOTIN RHS. - pose proof (eq_find_sound no {| eq_lhs := dst; eq_op := sop; eq_args := args |}) as EQ_FIND_SOUND. + pose proof (eq_find_sound no (Equ dst sop args)) as EQ_FIND_SOUND. destruct eq_find. 2: auto with cse3; fail. specialize EQ_FIND_SOUND with (id := e). @@ -881,10 +885,10 @@ Section SOUNDNESS. } 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 e (Equ dst sop args) CONTAINSe H) as RELe. pose proof (REL i eq CONTAINS INi) as RELi. + destruct eq as [eq_lhs eq_sop eq_args]; cbn in *. 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. @@ -919,9 +923,10 @@ Section SOUNDNESS. unfold sem_rel, sem_eq, sem_rhs in *. intros. specialize REL with (i:=i) (eq0:=eq). + destruct eq as [lhs sop args] eqn:EQ. rewrite Regmap.gsident. - replace ((rs # r <- (rs # r)) ## (eq_args eq)) with - (rs ## (eq_args eq)). + replace ((rs # r <- (rs # r)) ## args) with + (rs ## args). { apply REL; auto. } apply list_map_exten. intros. @@ -943,7 +948,7 @@ Section SOUNDNESS. { subst dst. apply rel_idem_replace; auto. } - pose proof (eq_find_sound no {| eq_lhs := dst; eq_op := SOp Omove; eq_args := src :: nil |}) as EQ_FIND_SOUND. + pose proof (eq_find_sound no (Equ dst (SOp Omove) (src::nil))) as EQ_FIND_SOUND. destruct eq_find. - intros i eq CONTAINS. destruct (peq i e). @@ -1023,10 +1028,10 @@ Section SOUNDNESS. rewrite CATALOG in CONTAINS. unfold sem_rel in REL. specialize REL with (i := i) (eq0 := eq). - destruct eq; simpl in *. + destruct eq as [eq_lhs eq_sop eq_args]; simpl in *. unfold sem_eq in *. simpl in *. - destruct eq_op as [op' | chunk' addr']; simpl. + destruct eq_sop as [op' | chunk' addr']; simpl. - rewrite op_valid_pointer_eq with (m2 := m). + cbn in *. apply REL; auto. @@ -1076,7 +1081,7 @@ Section SOUNDNESS. intros i eq CONTAINS CATALOG. destruct (peq i eq_id). { subst i. - rewrite eq_find_sound with (no:=no) (eq0:={| eq_lhs := src; eq_op := SLoad chunk addr; eq_args := args |}) in CATALOG; trivial. + rewrite eq_find_sound with (no:=no) (eq0:=Equ src (SLoad chunk addr) args) in CATALOG; trivial. inv CATALOG. unfold sem_eq. simpl. diff --git a/extraction/extraction.v b/extraction/extraction.v index c5fa7a62..2f6f9599 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -221,7 +221,7 @@ Set Extraction AccessOpaque. Cd "extraction". Separate Extraction - CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem + CSE3analysis.internal_analysis CSE3analysis.eq_cond_depends_on_mem Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env |