From b2171eb8e6af1d0a19bd42fb455fccc7e9f34fe9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 25 Nov 2020 15:03:55 +0100 Subject: cond_valid_pointer_eq --- backend/CSE3analysis.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'backend') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 8b7f1190..84f4a426 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -160,6 +160,20 @@ 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) := -- cgit From d30d56425a8cf73852f7acafe21458be6c787ebc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 13:54:36 +0100 Subject: passage à Equ MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- backend/CSE3analysis.v | 133 ++++++++++++++---------------- backend/CSE3analysisaux.ml | 57 ++++++++----- backend/CSE3analysisproof.v | 195 +++++++++++++++++++++++--------------------- 3 files changed, 196 insertions(+), 189 deletions(-) (limited to 'backend') 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. -- cgit From d09c509f8d1bd8335ebedbe260320bb43c5a2723 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 15:11:15 +0100 Subject: ajouté Cond, tout passe MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- backend/CSE3analysis.v | 16 +++-- backend/CSE3analysisaux.ml | 34 +++++++--- backend/CSE3analysisproof.v | 158 +++++++++++++++++++++++++++++++++++++------- 3 files changed, 168 insertions(+), 40 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 137282a4..4b616568 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -146,7 +146,8 @@ Proof. Defined. Inductive equation_or_condition := - | Equ : reg -> sym_op -> list reg -> equation_or_condition. +| Equ : reg -> sym_op -> list reg -> equation_or_condition +| Cond : condition -> list reg -> equation_or_condition. Definition eq_dec_equation : forall eq eq' : equation_or_condition, {eq = eq'} + {eq <> eq'}. @@ -154,6 +155,7 @@ Proof. generalize peq. generalize eq_dec_sym_op. generalize eq_dec_args. + generalize eq_condition. decide equality. Defined. @@ -172,6 +174,7 @@ Definition get_reg_kills (eqs : PTree.t equation_or_condition) : | Equ lhs sop args => add_i_j lhs eqno (add_ilist_j args eqno already) + | Cond cond args => add_ilist_j args eqno already end) eqs (PMap.init PSet.empty). @@ -182,15 +185,13 @@ Definition eq_cond_depends_on_mem eq_cond := | SLoad _ _ => true | SOp op => op_depends_on_memory op end + | Cond cond args => cond_depends_on_memory cond end. 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 + | Equ _ (SLoad _ _) _ => true + | _ => false end. Definition get_mem_kills (eqs : PTree.t equation_or_condition) : PSet.t := @@ -229,6 +230,7 @@ Definition get_moves (eqs : PTree.t equation_or_condition) : if is_smove sop then add_i_j lhs eqno already else already + | _ => already end) eqs (PMap.init PSet.empty). Record eq_context := mkeqcontext @@ -294,11 +296,11 @@ Section OPERATIONS. | None => None | Some src => match eq_catalog ctx src with - | None => None | 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 + | _ => None end end. diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index f50f4a46..731212eb 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -17,11 +17,14 @@ open Camlcoq open Coqlib type flattened_equation_or_condition = - | Flat_equ of int * sym_op * int list;; + | Flat_equ of int * sym_op * int list + | Flat_cond of Op.condition * int list;; let flatten_eq = function | Equ(lhs, sop, args) -> - Flat_equ((P.to_int lhs), sop, (List.map P.to_int args));; + Flat_equ((P.to_int lhs), sop, (List.map P.to_int args)) + | Cond(cond, args) -> + Flat_cond(cond, (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;; @@ -49,6 +52,9 @@ let print_eq channel (lhs, sop, args) = Printf.printf "%a = %s @ %a" print_reg lhs (string_of_chunk chunk) (PrintOp.print_addressing print_reg) (addr, args);; +let print_cond channel (cond, args) = + Printf.printf "cond %a" (PrintOp.print_condition print_reg) (cond, args);; + let pp_intset oc s = Printf.fprintf oc "{ "; List.iter (fun i -> Printf.fprintf oc "%d; " (P.to_int i)) (PSet.elements s); @@ -66,7 +72,10 @@ 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);; + pp_rhs (sop, args) + | Cond(cond, args) -> + Printf.fprintf oc "cond %a" + (PrintOp.print_condition PrintRTL.reg) (cond, args);; let pp_P oc x = Printf.fprintf oc "%d" (P.to_int x) @@ -94,8 +103,10 @@ let pp_equation hints chan x = | None -> output_string chan "???" | Some eq -> match eq with - Equ(lhs, sop, args) -> - print_eq chan (P.to_int lhs, sop, List.map P.to_int args);; + | Equ(lhs, sop, args) -> + print_eq chan (P.to_int lhs, sop, List.map P.to_int args) + | Cond(cond, args) -> + print_cond chan (cond, List.map P.to_int args);; let pp_relation hints chan rel = pp_set "; " (pp_equation hints) chan rel;; @@ -222,15 +233,20 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = (PSet.add coq_id (match Hashtbl.find_opt rhs_table (flat_eq_op, flat_eq_args) with | None -> PSet.empty - | Some s -> s))); + | Some s -> s)) + | Flat_cond _ -> ()); (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 - | _, _ -> ()); + (match sop, args with + | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves lhs coq_id + | _, _ -> ()) + | Cond(cond, args) -> + List.iter + (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) args + ); (if eq_cond_depends_on_mem eq then cur_kill_mem := PSet.add coq_id !cur_kill_mem); (if eq_cond_depends_on_store eq diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 5fcaa048..228fec93 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -135,6 +135,7 @@ Definition xlget_kills (eqs : list (eq_id * equation_or_condition)) | Equ lhs sop args => add_i_j lhs (fst item) (add_ilist_j args (fst item) already) + | Cond cond args => add_ilist_j args (fst item) already end) eqs m. Definition xlget_mem_kills (eqs : list (positive * equation_or_condition)) @@ -165,8 +166,7 @@ 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. + destruct eq_cond as [eq_lhs eq_sop eq_args | eq_cond eq_args]; auto with cse3. Qed. Hint Resolve xlget_kills_monotone : cse3. @@ -241,6 +241,23 @@ Qed. Hint Resolve xlget_kills_has_arg : cse3. +Lemma xlget_cond_kills_has_arg : + forall eqs m cond arg args j, + In (j, (Cond cond args)) eqs -> + In arg args -> + PSet.contains (Regmap.get arg (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros until j. + intros HEAD_TAIL ARG. + destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl. + - auto with cse3. + - eapply IHeqs; eassumption. +Qed. + +Hint Resolve xlget_cond_kills_has_arg : cse3. + Lemma get_kills_has_lhs : forall eqs lhs sop args j, PTree.get j eqs = Some (Equ lhs sop args) -> @@ -253,7 +270,8 @@ Proof. (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) + add_i_j lhs0 (fst p) (add_ilist_j args0 (fst p) a) + | Cond _ args0 => add_ilist_j args0 (fst p) a end)) with xlget_kills. eapply xlget_kills_has_lhs. apply PTree.elements_correct. @@ -287,7 +305,8 @@ Proof. (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) + add_i_j lhs0 (fst p) (add_ilist_j args0 (fst p) a) + | Cond _ args0 => add_ilist_j args0 (fst p) a end)) with xlget_kills. eapply xlget_kills_has_arg. - apply PTree.elements_correct. @@ -310,6 +329,43 @@ Qed. Hint Resolve context_from_hints_get_kills_has_arg : cse3. +Lemma get_cond_kills_has_arg : + forall eqs cond arg args j, + PTree.get j eqs = Some (Cond cond args) -> + In arg args -> + PSet.contains (Regmap.get arg (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_or_condition) => + match snd p with + | Equ lhs0 _ args0 => + add_i_j lhs0 (fst p) (add_ilist_j args0 (fst p) a) + | Cond _ args0 => add_ilist_j args0 (fst p) a + end)) with xlget_kills. + eapply xlget_cond_kills_has_arg. + - apply PTree.elements_correct. + eassumption. + - assumption. +Qed. + +Hint Resolve get_cond_kills_has_arg : cse3. + +Lemma context_from_hints_get_cond_kills_has_arg : + forall hints cond arg args j, + PTree.get j (hint_eq_catalog hints) = Some (Cond cond args) -> + In arg args -> + PSet.contains (eq_kill_reg (context_from_hints hints) arg) j = true. +Proof. + intros. + simpl. + eapply get_cond_kills_has_arg; eassumption. +Qed. + +Hint Resolve context_from_hints_get_cond_kills_has_arg : cse3. + Lemma xlget_kills_has_eq_depends_on_mem : forall eqs eq j m, In (j, eq) eqs -> @@ -420,6 +476,7 @@ Definition eq_involves (eq : equation_or_condition) (i : reg) := match eq with | Equ lhs sop args => i = lhs \/ In i args + | Cond cond args => In i args end. Section SOUNDNESS. @@ -452,6 +509,7 @@ Section SOUNDNESS. 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) + | Cond cond args => eval_condition cond (rs ## args) m = Some true end. Definition sem_rel (rel : RELATION.t) (rs : regset) (m : mem) := @@ -496,6 +554,13 @@ Section SOUNDNESS. In arg args -> PSet.contains (eq_kill_reg ctx arg) j = true. + Hypothesis ctx_cond_kill_reg_has_arg : + forall cond args j, + eq_catalog ctx j = Some (Cond cond args) -> + forall arg, + In arg args -> + PSet.contains (eq_kill_reg ctx arg) j = true. + Hypothesis ctx_kill_mem_has_depends_on_mem : forall eq j, eq_catalog ctx j = Some eq -> @@ -517,8 +582,8 @@ Section SOUNDNESS. intros until v. intros REL i eq. specialize REL with (i := i) (eq0 := eq). - destruct eq as [lhs sop args]; simpl. - specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i). + destruct eq as [lhs sop args | cond args]; simpl. + * specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i). specialize ctx_kill_reg_has_arg with (lhs := lhs) (sop := sop) (args := args) (j := i) (arg := dst). intuition. rewrite PSet.gsubtract in H. @@ -546,6 +611,24 @@ Section SOUNDNESS. assumption. - rewrite Regmap.gso by congruence. assumption. + * specialize ctx_cond_kill_reg_has_arg with (cond := cond) (args := args) (j := i) (arg := dst). + intuition. + rewrite PSet.gsubtract in H. + rewrite andb_true_iff in H. + rewrite negb_true_iff in H. + intuition. + simpl in *. + assert ({In dst args} + {~In dst args}) as IN_ARGS. + { + apply List.in_dec. + apply peq. + } + destruct IN_ARGS as [IN_ARGS | NOTIN_ARGS]. + { intuition. + congruence. + } + rewrite subst_args_notin by assumption. + assumption. Qed. Hint Resolve kill_reg_sound : cse3. @@ -559,14 +642,20 @@ Section SOUNDNESS. intros until dst. intros REL i eq. specialize REL with (i := i) (eq0 := eq). - destruct eq as [lhs sop args]; simpl. - specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i). + destruct eq as [lhs sop args | cond args]; simpl. + * specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i). specialize ctx_kill_reg_has_arg with (lhs := lhs) (sop := sop) (args := args) (j := i) (arg := dst). intuition. rewrite PSet.gsubtract in H. rewrite andb_true_iff in H. rewrite negb_true_iff in H. intuition. + * specialize ctx_cond_kill_reg_has_arg with (cond := cond) (args := args) (j := i) (arg := dst). + intuition. + rewrite PSet.gsubtract in H. + rewrite andb_true_iff in H. + rewrite negb_true_iff in H. + intuition. Qed. Lemma pick_source_sound : @@ -597,7 +686,7 @@ Section SOUNDNESS. destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG. 2: reflexivity. specialize REL with (i := r) (eq0 := eq). - destruct eq as [lhs sop args]; cbn in *. (* TODO *) + destruct eq as [lhs sop args | cond args]; cbn in *; trivial. destruct (is_smove sop) as [MOVE | ]. 2: reflexivity. rewrite MOVE in *; cbn in *. @@ -645,8 +734,8 @@ Section SOUNDNESS. rewrite PSet.gsubtract in SUBTRACT. rewrite andb_true_iff in SUBTRACT. intuition. - destruct eq as [lhs sop args] eqn:EQ. - destruct sop as [op | chunk addr] eqn:OP. + destruct eq as [lhs sop args | cond args] eqn:EQ. + * destruct sop as [op | chunk addr] eqn:OP. - specialize ctx_kill_mem_has_depends_on_mem with (eq0 := eq) (j := i). rewrite EQ in ctx_kill_mem_has_depends_on_mem. unfold eq_cond_depends_on_mem in ctx_kill_mem_has_depends_on_mem. @@ -660,6 +749,15 @@ Section SOUNDNESS. rewrite negb_true_iff in H0. intuition. congruence. + * specialize ctx_kill_mem_has_depends_on_mem with (eq0 := eq) (j := i). + 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 (cond_depends_on_memory_correct cond) with (m2 := m). + assumption. + destruct (cond_depends_on_memory cond) in *; trivial. + rewrite negb_true_iff in H0. + intuition. + congruence. Qed. Hint Resolve kill_mem_sound : cse3. @@ -698,8 +796,8 @@ Section SOUNDNESS. rewrite PSet.gsubtract in SUBTRACT. rewrite andb_true_iff in SUBTRACT. intuition. - destruct eq as [lhs sop args] eqn:EQ. - destruct sop as [op | chunk addr] eqn:OP. + destruct eq as [lhs sop args | cond 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. @@ -708,6 +806,9 @@ Section SOUNDNESS. rewrite negb_true_iff in H0. intuition. congruence. + * rewrite cond_valid_pointer_eq with (m2 := m). + assumption. + eapply store_preserves_validity; eauto. Qed. Hint Resolve kill_store_sound : cse3. @@ -748,7 +849,8 @@ Section SOUNDNESS. destruct (eq_catalog ctx src') as [eq | ] eqn:CATALOG. 2: discriminate. specialize REL with (i := src') (eq0 := eq). - destruct eq as [eq_lhs eq_sop eq_args] eqn:EQ. + destruct eq as [eq_lhs eq_sop eq_args | eq_cond eq_args] eqn:EQ. + 2: discriminate. destruct (eq_dec_sym_op sop eq_sop). 2: discriminate. destruct (eq_dec_args args eq_args). @@ -887,12 +989,14 @@ Section SOUNDNESS. destruct (PSet.contains rel e) eqn:CONTAINSe. { 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 *. - replace v with (rs # dst) by (eapply sem_rhs_det; eassumption). - rewrite Regmap.gsident. - apply sem_rhs_idem_write. - assumption. + destruct eq as [eq_lhs eq_sop eq_args | eq_cond eq_args]; cbn in *. + - replace v with (rs # dst) by (eapply sem_rhs_det; eassumption). + rewrite Regmap.gsident. + apply sem_rhs_idem_write. + assumption. + - replace v with (rs # dst) by (eapply sem_rhs_det; eassumption). + rewrite arglist_idem_write. + assumption. } rewrite PSet.gaddo in CONTAINS by congruence. apply (kill_reg_sound rel rs m dst v REL i eq); auto. @@ -923,14 +1027,17 @@ 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. + destruct eq as [lhs sop args | cond args] eqn:EQ. + * rewrite Regmap.gsident. replace ((rs # r <- (rs # r)) ## args) with (rs ## args). { apply REL; auto. } apply list_map_exten. intros. apply Regmap.gsident. + (* TODO simplify? *) + * rewrite arglist_idem_write. + auto. Qed. Lemma move_sound : @@ -1028,8 +1135,8 @@ Section SOUNDNESS. rewrite CATALOG in CONTAINS. unfold sem_rel in REL. specialize REL with (i := i) (eq0 := eq). - destruct eq as [eq_lhs eq_sop eq_args]; simpl in *. - unfold sem_eq in *. + destruct eq as [eq_lhs eq_sop eq_args | eq_cond eq_args]; simpl in *. + * unfold sem_eq in *. simpl in *. destruct eq_sop as [op' | chunk' addr']; simpl. - rewrite op_valid_pointer_eq with (m2 := m). @@ -1044,6 +1151,9 @@ Section SOUNDNESS. + erewrite may_overlap_sound with (chunk:=chunk) (addr:=addr) (args:=args) (chunk':=chunk') (addr':=addr') (args':=eq_args); try eassumption. apply REL; auto. + apply REL; auto. + * rewrite cond_valid_pointer_eq with (m2 := m). + auto. + eapply store_preserves_validity; eauto. Qed. Hint Resolve clever_kill_store_sound : cse3. -- cgit From 01f0108df437df0792ac560f630e7969be76b60b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 15:25:21 +0100 Subject: begin implementing cond table --- backend/CSE3analysisaux.ml | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 731212eb..e8964090 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -186,12 +186,20 @@ let refine_analysis ctx tenv refine_invariants (List.map fst (PTree.elements f.RTL.fn_code)) f.RTL.fn_entrypoint succ_f pred_f tfr invariants0;; + +let add_to_set_in_table table key item = + Hashtbl.add table key + (PSet.add item + (match Hashtbl.find_opt table key with + | None -> PSet.empty + | Some s -> s));; let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let cur_eq_id = ref 0 and cur_catalog = ref PTree.empty and eq_table = Hashtbl.create 100 and rhs_table = Hashtbl.create 100 + and cond_table = Hashtbl.create 100 and cur_kill_reg = ref (PMap.init PSet.empty) and cur_kill_mem = ref PSet.empty and cur_kill_store = ref PSet.empty @@ -229,12 +237,11 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = (cur_catalog := PTree.set coq_id eq !cur_catalog); (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)) - | Flat_cond _ -> ()); + add_to_set_in_table rhs_table + (flat_eq_op, flat_eq_args) coq_id + | Flat_cond(flat_eq_cond, flat_eq_args) -> + add_to_set_in_table cond_table + (flat_eq_cond, flat_eq_args) coq_id); (match eq with | Equ(lhs, sop, args) -> List.iter -- cgit From 3c670f954dc470333e94932279e02e6940ff9f15 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 16:24:01 +0100 Subject: is_condition_present_sound --- backend/CSE3analysis.v | 7 ++++++- backend/CSE3analysisaux.ml | 5 +---- backend/CSE3analysisproof.v | 16 ++++++++++++++++ 3 files changed, 23 insertions(+), 5 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 4b616568..390f6d26 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -290,6 +290,12 @@ Section OPERATIONS. | None => None end. + Definition is_condition_present + (rel : RELATION.t) (cond : condition) (args : list reg) := + match eq_find (Cond cond args) with + | Some id => PSet.contains rel id + | None => false + end. Definition rhs_find (sop : sym_op) (args : list reg) (rel : RELATION.t) : option reg := match pick_source (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel)) with @@ -509,7 +515,6 @@ Definition internal_analysis (f : RTL.function) : option invariants := DS.fixpoint (RTL.fn_code f) RTL.successors_instr (apply_instr' tenv (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). - End OPERATIONS. Record analysis_hints := diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index e8964090..1642a269 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -199,7 +199,6 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = and cur_catalog = ref PTree.empty and eq_table = Hashtbl.create 100 and rhs_table = Hashtbl.create 100 - and cond_table = Hashtbl.create 100 and cur_kill_reg = ref (PMap.init PSet.empty) and cur_kill_mem = ref PSet.empty and cur_kill_store = ref PSet.empty @@ -239,9 +238,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = | Flat_equ(flat_eq_lhs, flat_eq_op, flat_eq_args) -> add_to_set_in_table rhs_table (flat_eq_op, flat_eq_args) coq_id - | Flat_cond(flat_eq_cond, flat_eq_args) -> - add_to_set_in_table cond_table - (flat_eq_cond, flat_eq_args) coq_id); + | Flat_cond(flat_eq_cond, flat_eq_args) -> ()); (match eq with | Equ(lhs, sop, args) -> List.iter diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 228fec93..7e456748 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -831,6 +831,22 @@ Section SOUNDNESS. Hint Resolve eq_find_sound : cse3. + Theorem is_condition_present_sound : + forall node rel cond args rs m + (REL : sem_rel rel rs m) + (COND : (is_condition_present (ctx := ctx) node rel cond args) = true), + (eval_condition cond (rs ## args) m) = Some true. + Proof. + unfold sem_rel, is_condition_present. + intros. + destruct eq_find as [i |] eqn:FIND. + 2: discriminate. + pose proof (eq_find_sound node (Cond cond args) i FIND) as CATALOG. + exact (REL i (Cond cond args) COND CATALOG). + Qed. + + Hint Resolve is_condition_present_sound : cse3. + Theorem rhs_find_sound: forall no sop args rel src rs m, sem_rel rel rs m -> -- cgit From 61b433cd903fa4182ae255f0f61f692eb163d677 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 19:57:56 +0100 Subject: remains one admit --- backend/CSE3proof.v | 54 +++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 46 insertions(+), 8 deletions(-) (limited to 'backend') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 3fbc9912..215f5c41 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -765,14 +765,52 @@ Proof. eapply external_call_sound; eauto with cse3. - (* Icond *) - econstructor. split. - + eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. - * TR_AT. reflexivity. - * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. - eassumption. - * reflexivity. - + econstructor; eauto. - destruct b; IND_STEP. + destruct (find_cond_in_fmap (ctx := (context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc cond args) as [bfound | ] eqn:FIND_COND. + + econstructor; split. + * eapply exec_Inop; try eassumption. + TR_AT. unfold transf_instr. rewrite FIND_COND. reflexivity. + * replace bfound with b. + { econstructor; eauto. + admit. + } + unfold find_cond_in_fmap in FIND_COND. + change RB.t with (option RELATION.t) in REL. + change Regmap.get with PMap.get in REL. + destruct (@PMap.get (option RELATION.t) pc + (@fst invariants analysis_hints (preanalysis tenv f))) as [rel | ] eqn:FIND_REL. + 2: discriminate. + pose proof (is_condition_present_sound pc rel cond args rs m REL) as COND_PRESENT_TRUE. + pose proof (is_condition_present_sound pc rel (negate_condition cond) args rs m REL) as COND_PRESENT_FALSE. + rewrite eval_negate_condition in COND_PRESENT_FALSE. + destruct (is_condition_present pc rel cond args). + { rewrite COND_PRESENT_TRUE in H0 by trivial. + congruence. + } + destruct (is_condition_present pc rel (negate_condition cond) args). + { destruct (eval_condition cond rs ## args m) as [b0 | ]. + 2: discriminate. + inv H0. + cbn in COND_PRESENT_FALSE. + intuition. + inv H0. + inv FIND_COND. + destruct b; trivial; cbn in H2; discriminate. + } + rewrite <- subst_args_ok with (invariants := (fst (preanalysis tenv f))) (ctx := (context_from_hints (snd (preanalysis tenv f)))) (pc := pc) (sp:=sp) (m:=m) in COND_PRESENT_TRUE. + admit. + unfold fmap_sem. + change RB.t with (option RELATION.t). + rewrite FIND_REL. + exact REL. + + econstructor; split. + * eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. + ** TR_AT. unfold transf_instr. rewrite FIND_COND. + reflexivity. + ** rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + eassumption. + ** reflexivity. + * econstructor; eauto. + destruct b; IND_STEP. - (* Ijumptable *) econstructor. split. -- cgit From 3570ba2827908b280315c922ba7e43289f6d802a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 22:12:38 +0100 Subject: not yet the transfer functions that record predicates --- backend/CSE3.v | 24 +++++++++++++++++- backend/CSE3analysisaux.ml | 2 +- backend/CSE3proof.v | 61 ++++++++++++++++++++++++++++++++++++++++------ 3 files changed, 78 insertions(+), 9 deletions(-) (limited to 'backend') diff --git a/backend/CSE3.v b/backend/CSE3.v index df1c2bfc..482069d7 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -53,6 +53,24 @@ Definition forward_move_l_b (rb : RB.t) (xl : list reg) := Definition subst_args fmap pc xl := forward_move_l_b (PMap.get pc fmap) xl. +Definition find_cond_in_fmap fmap pc cond args := + match PMap.get pc fmap with + | Some rel => + if is_condition_present (ctx:=ctx) pc rel cond args + then Some true + else + let ncond := negate_condition cond in + if is_condition_present (ctx:=ctx) pc rel ncond args + then Some false + else let args' := subst_args fmap pc args in + if is_condition_present (ctx:=ctx) pc rel cond args' + then Some true + else if is_condition_present (ctx:=ctx) pc rel ncond args' + then Some false + else None + | None => None + end. + Definition transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) := match instr with @@ -75,7 +93,11 @@ Definition transf_instr (fmap : PMap.t RB.t) | Itailcall sig ros args => Itailcall sig ros (subst_args fmap pc args) | Icond cond args s1 s2 expected => - Icond cond (subst_args fmap pc args) s1 s2 expected + let args' := subst_args fmap pc args in + match find_cond_in_fmap fmap pc cond args with + | None => Icond cond args' s1 s2 expected + | Some b => Inop (if b then s1 else s2) + end | Ijumptable arg tbl => Ijumptable (subst_arg fmap pc arg) tbl | Ireturn (Some arg) => diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 1642a269..ab8cbeed 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -206,7 +206,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 o = None then failwith "eq_find_oracle"); + (* FIXME (if o = None then failwith "eq_find_oracle"); *) (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); diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 215f5c41..7af62b95 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -771,7 +771,28 @@ Proof. TR_AT. unfold transf_instr. rewrite FIND_COND. reflexivity. * replace bfound with b. { econstructor; eauto. - admit. + assert (is_inductive_allstep (ctx:= (context_from_hints (snd (preanalysis tenv f)))) f tenv (fst (preanalysis tenv f))) as IND by + (apply checked_is_inductive_allstep; + eapply transf_function_invariants_inductive; eassumption). + unfold is_inductive_allstep, is_inductive_step, apply_instr' in IND. + specialize IND with (pc:=pc) (pc':= if b then ifso else ifnot) (instr:= (Icond cond args ifso ifnot predb)). + cbn in IND. + rewrite H in IND. + assert (RB.ge (fst (preanalysis tenv f)) # (if b then ifso else ifnot) + match (fst (preanalysis tenv f)) # pc with + | Some x => apply_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc tenv (Icond cond args ifso ifnot predb) x + | None => None + end) as INDUCTIVE by (destruct b; intuition). + clear IND. + + change node with positive. + + destruct ((fst (preanalysis tenv f)) # pc). + 2: exfalso; exact REL. + + destruct ((fst (preanalysis tenv f)) # (if b then ifso else ifnot)). + - eapply rel_ge. exact INDUCTIVE. exact REL. + - cbn in INDUCTIVE. exfalso. exact INDUCTIVE. } unfold find_cond_in_fmap in FIND_COND. change RB.t with (option RELATION.t) in REL. @@ -796,12 +817,38 @@ Proof. inv FIND_COND. destruct b; trivial; cbn in H2; discriminate. } - rewrite <- subst_args_ok with (invariants := (fst (preanalysis tenv f))) (ctx := (context_from_hints (snd (preanalysis tenv f)))) (pc := pc) (sp:=sp) (m:=m) in COND_PRESENT_TRUE. - admit. - unfold fmap_sem. - change RB.t with (option RELATION.t). - rewrite FIND_REL. - exact REL. + clear COND_PRESENT_TRUE COND_PRESENT_FALSE. + pose proof (is_condition_present_sound pc rel cond (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_TRUE. + pose proof (is_condition_present_sound pc rel (negate_condition cond) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_FALSE. + rewrite eval_negate_condition in COND_PRESENT_FALSE. + + destruct is_condition_present. + { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_TRUE. + { rewrite COND_PRESENT_TRUE in H0 by trivial. + congruence. + } + unfold fmap_sem. + change RB.t with (option RELATION.t). + rewrite FIND_REL. + exact REL. + } + destruct is_condition_present. + { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_FALSE. + { destruct (eval_condition cond rs ## args m) as [b0 | ]. + 2: discriminate. + inv H0. + cbn in COND_PRESENT_FALSE. + intuition. + inv H0. + inv FIND_COND. + destruct b; trivial; cbn in H2; discriminate. + } + unfold fmap_sem. + change RB.t with (option RELATION.t). + rewrite FIND_REL. + exact REL. + } + discriminate. + econstructor; split. * eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. ** TR_AT. unfold transf_instr. rewrite FIND_COND. -- cgit From 120857f71e64c7627d2921d00b804cbc49864042 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 2 Dec 2020 17:27:09 +0100 Subject: attempt at initial analysis --- backend/CSE3analysisaux.ml | 36 +++++++++++++++++++++++++++++++++++- 1 file changed, 35 insertions(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index ab8cbeed..39490d79 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -134,6 +134,32 @@ let rb_glb (x : RB.t) (y : RB.t) : RB.t = | None, _ | _, None -> None | (Some x'), (Some y') -> Some (RELATION.glb x' y');; +let compute_invariants + (nodes : RTL.node list) + (entrypoint : RTL.node) + (successors : RTL.node -> RTL.node list) + (tfr : RTL.node -> RB.t -> RB.t) = + let todo = ref IntSet.empty + and invariants = ref (PMap.set entrypoint (Some RELATION.top) (PMap.init RB.bot)) in + let add_todo (pc : RTL.node) = + todo := IntSet.add (P.to_int pc) !todo in + let update_node (pc : RTL.node) = + (if !Clflags.option_debug_compcert > 9 + then Printf.printf "UP updating node %d\n" (P.to_int pc)); + let cur = PMap.get pc !invariants in + List.iter (fun next_pc -> + let previous = PMap.get next_pc !invariants in + let next = RB.lub previous (tfr pc cur) in + if not (RB.beq previous next) + then add_todo next_pc) (successors pc) in + add_todo entrypoint; + while not (IntSet.is_empty !todo) do + let nxt = IntSet.max_elt !todo in + todo := IntSet.remove nxt !todo; + update_node (P.of_int nxt) + done; + !invariants;; + let refine_invariants (nodes : RTL.node list) (entrypoint : RTL.node) @@ -146,7 +172,7 @@ let refine_invariants todo := IntSet.add (P.to_int pc) !todo in let update_node (pc : RTL.node) = (if !Clflags.option_debug_compcert > 9 - then Printf.printf "updating node %d\n" (P.to_int pc)); + then Printf.printf "DOWN updating node %d\n" (P.to_int pc)); if not (peq pc entrypoint) then let cur = PMap.get pc !invariants in @@ -176,6 +202,14 @@ let get_default default x ptree = | None -> default | Some y -> y;; +let initial_analysis ctx tenv (f : RTL.coq_function) = + let succ_map = RTL.successors_map f in + let succ_f x = get_default [] x succ_map in + let tfr = apply_instr' ctx tenv f.RTL.fn_code in + compute_invariants + (List.map fst (PTree.elements f.RTL.fn_code)) + f.RTL.fn_entrypoint succ_f tfr;; + let refine_analysis ctx tenv (f : RTL.coq_function) (invariants0 : RB.t PMap.t) = let succ_map = RTL.successors_map f in -- cgit From a100edde18de43cf933c0d53467e196541436e13 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 2 Dec 2020 19:00:21 +0100 Subject: start checking for bugs --- backend/CSE3analysisaux.ml | 117 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 115 insertions(+), 2 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 39490d79..5ffa9222 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -151,7 +151,9 @@ let compute_invariants let previous = PMap.get next_pc !invariants in let next = RB.lub previous (tfr pc cur) in if not (RB.beq previous next) - then add_todo next_pc) (successors pc) in + then ( + invariants := PMap.set next_pc next !invariants; + add_todo next_pc)) (successors pc) in add_todo entrypoint; while not (IntSet.is_empty !todo) do let nxt = IntSet.max_elt !todo in @@ -228,7 +230,7 @@ let add_to_set_in_table table key item = | None -> PSet.empty | Some s -> s));; -let preanalysis (tenv : typing_env) (f : RTL.coq_function) = +let preanalysis0 (tenv : typing_env) (f : RTL.coq_function) = let cur_eq_id = ref 0 and cur_catalog = ref PTree.empty and eq_table = Hashtbl.create 100 @@ -319,3 +321,114 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = then pp_results f invariants' hints stdout); invariants', hints ;; + +let preanalysis1 (tenv : typing_env) (f : RTL.coq_function) = + let cur_eq_id = ref 0 + and cur_catalog = ref PTree.empty + and eq_table = Hashtbl.create 100 + and rhs_table = Hashtbl.create 100 + and cur_kill_reg = ref (PMap.init PSet.empty) + and cur_kill_mem = ref PSet.empty + and cur_kill_store = ref PSet.empty + and cur_moves = ref (PMap.init PSet.empty) in + let eq_find_oracle node eq = + assert (not (is_trivial eq)); + let o = Hashtbl.find_opt eq_table (flatten_eq eq) in + (* FIXME (if o = None then failwith "eq_find_oracle"); *) + (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 + 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 + (if !Clflags.option_debug_compcert > 5 + then Printf.printf "@%d: rhs_find %a = %a\n" + (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 = flatten_eq eq in + let o = + match Hashtbl.find_opt eq_table flat_eq with + | Some x -> + Some x + | None -> + (* TODO print_eq stderr flat_eq; *) + incr cur_eq_id; + let id = !cur_eq_id in + let coq_id = P.of_int id in + begin + Hashtbl.add eq_table flat_eq coq_id; + (cur_catalog := PTree.set coq_id eq !cur_catalog); + (match flat_eq with + | Flat_equ(flat_eq_lhs, flat_eq_op, flat_eq_args) -> + add_to_set_in_table rhs_table + (flat_eq_op, flat_eq_args) coq_id + | Flat_cond(flat_eq_cond, flat_eq_args) -> ()); + (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 + | _, _ -> ()) + | Cond(cond, args) -> + List.iter + (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) args + ); + (if eq_cond_depends_on_mem eq + then cur_kill_mem := PSet.add coq_id !cur_kill_mem); + (if eq_cond_depends_on_store eq + then cur_kill_store := PSet.add coq_id !cur_kill_store); + Some coq_id + end + in + (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 + in + let ctx = { eq_catalog = (fun eq_id -> PTree.get eq_id !cur_catalog); + eq_find_oracle = mutating_eq_find_oracle; + eq_rhs_oracle = rhs_find_oracle ; + eq_kill_reg = (fun reg -> PMap.get reg !cur_kill_reg); + eq_kill_mem = (fun () -> !cur_kill_mem); + eq_kill_store = (fun () -> !cur_kill_store); + eq_moves = (fun reg -> PMap.get reg !cur_moves) + } in + let invariants = initial_analysis ctx tenv f in + let invariants' = + if ! Clflags.option_fcse3_refine + then refine_analysis ctx tenv f invariants + else invariants + and 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 +;; + +let check_same_invariants max_pc invariants0 invariants1 = + for pc=1 to max_pc + do + let p_pc = P.of_int pc in + if not (RB.beq (PMap.get p_pc invariants0) + (PMap.get p_pc invariants1)) + then failwith (Printf.sprintf "check_same_invariants at %d" pc) + done;; + +let check_same_catalog catalog0 catalog1 = + if not (PTree.beq eq_dec_equation catalog0 catalog1) + then failwith "catalogs not equal";; + +let preanalysis (tenv : typing_env) (f : RTL.coq_function) = + let invariants0, hints0 = preanalysis0 tenv f + and invariants1, hints1 = preanalysis1 tenv f in + check_same_invariants (P.to_int (RTL.max_pc_function f)) + invariants0 invariants1; + check_same_catalog hints0.hint_eq_catalog hints1.hint_eq_catalog; + invariants1, hints1;; -- cgit From 0f9018baabe8feeed19d8f7e14f8480e898b5a84 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 8 Dec 2020 19:56:28 +0100 Subject: CSE3 now runs on its own fixpoint iterator not based on Kildall.v --- backend/CSE3analysis.v | 2 + backend/CSE3analysisaux.ml | 115 +-------------------------------------------- 2 files changed, 3 insertions(+), 114 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 390f6d26..bcdebca7 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -509,12 +509,14 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva (fun pc' => relb_leb rel' (PMap.get pc' inv)) (RTL.successors_instr instr) end). +(* No longer used. Incompatible with transfer functions that yield a different result depending on the successor. Definition internal_analysis (tenv : typing_env) (f : RTL.function) : option invariants := DS.fixpoint (RTL.fn_code f) RTL.successors_instr (apply_instr' tenv (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). +*) End OPERATIONS. Record analysis_hints := diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 5ffa9222..b8f98b0d 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -230,99 +230,7 @@ let add_to_set_in_table table key item = | None -> PSet.empty | Some s -> s));; -let preanalysis0 (tenv : typing_env) (f : RTL.coq_function) = - let cur_eq_id = ref 0 - and cur_catalog = ref PTree.empty - and eq_table = Hashtbl.create 100 - and rhs_table = Hashtbl.create 100 - and cur_kill_reg = ref (PMap.init PSet.empty) - and cur_kill_mem = ref PSet.empty - and cur_kill_store = ref PSet.empty - and cur_moves = ref (PMap.init PSet.empty) in - let eq_find_oracle node eq = - assert (not (is_trivial eq)); - let o = Hashtbl.find_opt eq_table (flatten_eq eq) in - (* FIXME (if o = None then failwith "eq_find_oracle"); *) - (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 - 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 - (if !Clflags.option_debug_compcert > 5 - then Printf.printf "@%d: rhs_find %a = %a\n" - (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 = flatten_eq eq in - let o = - match Hashtbl.find_opt eq_table flat_eq with - | Some x -> - Some x - | None -> - (* TODO print_eq stderr flat_eq; *) - incr cur_eq_id; - let id = !cur_eq_id in - let coq_id = P.of_int id in - begin - Hashtbl.add eq_table flat_eq coq_id; - (cur_catalog := PTree.set coq_id eq !cur_catalog); - (match flat_eq with - | Flat_equ(flat_eq_lhs, flat_eq_op, flat_eq_args) -> - add_to_set_in_table rhs_table - (flat_eq_op, flat_eq_args) coq_id - | Flat_cond(flat_eq_cond, flat_eq_args) -> ()); - (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 - | _, _ -> ()) - | Cond(cond, args) -> - List.iter - (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) args - ); - (if eq_cond_depends_on_mem eq - then cur_kill_mem := PSet.add coq_id !cur_kill_mem); - (if eq_cond_depends_on_store eq - then cur_kill_store := PSet.add coq_id !cur_kill_store); - Some coq_id - end - in - (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 - in - let ctx = { eq_catalog = (fun eq_id -> PTree.get eq_id !cur_catalog); - eq_find_oracle = mutating_eq_find_oracle; - eq_rhs_oracle = rhs_find_oracle ; - eq_kill_reg = (fun reg -> PMap.get reg !cur_kill_reg); - eq_kill_mem = (fun () -> !cur_kill_mem); - eq_kill_store = (fun () -> !cur_kill_store); - eq_moves = (fun reg -> PMap.get reg !cur_moves) - } in - match internal_analysis ctx tenv f - with None -> failwith "CSE3analysisaux analysis failed, try re-running with -fno-cse3" - | Some invariants -> - let invariants' = - if ! Clflags.option_fcse3_refine - then refine_analysis ctx tenv f invariants - else invariants - and 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 -;; - -let preanalysis1 (tenv : typing_env) (f : RTL.coq_function) = +let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let cur_eq_id = ref 0 and cur_catalog = ref PTree.empty and eq_table = Hashtbl.create 100 @@ -411,24 +319,3 @@ let preanalysis1 (tenv : typing_env) (f : RTL.coq_function) = then pp_results f invariants' hints stdout); invariants', hints ;; - -let check_same_invariants max_pc invariants0 invariants1 = - for pc=1 to max_pc - do - let p_pc = P.of_int pc in - if not (RB.beq (PMap.get p_pc invariants0) - (PMap.get p_pc invariants1)) - then failwith (Printf.sprintf "check_same_invariants at %d" pc) - done;; - -let check_same_catalog catalog0 catalog1 = - if not (PTree.beq eq_dec_equation catalog0 catalog1) - then failwith "catalogs not equal";; - -let preanalysis (tenv : typing_env) (f : RTL.coq_function) = - let invariants0, hints0 = preanalysis0 tenv f - and invariants1, hints1 = preanalysis1 tenv f in - check_same_invariants (P.to_int (RTL.max_pc_function f)) - invariants0 invariants1; - check_same_catalog hints0.hint_eq_catalog hints1.hint_eq_catalog; - invariants1, hints1;; -- cgit From d7213cfdef90fc3ebc5f57ae18277d7b4c9dd126 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 8 Dec 2020 20:16:47 +0100 Subject: analysis with Abst_same --- backend/CSE3analysis.v | 35 ++++++++++++++++++++--------------- backend/CSE3analysisproof.v | 14 ++++++++++---- backend/CSE3proof.v | 12 +++++++++--- 3 files changed, 39 insertions(+), 22 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index bcdebca7..8cfbaaa1 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -127,6 +127,9 @@ End RELATION. Module RB := ADD_BOTTOM(RELATION). Module DS := Dataflow_Solver(RB)(NodeSetForward). +Inductive abst_insn_out := +| Abst_same : RB.t -> abst_insn_out. + Inductive sym_op : Type := | SOp : operation -> sym_op | SLoad : memory_chunk -> addressing -> sym_op. @@ -461,27 +464,27 @@ Section OPERATIONS. | _ => rel end. - Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t := + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : abst_insn_out := match instr with | Inop _ | Icond _ _ _ _ _ - | Ijumptable _ _ => Some rel + | Ijumptable _ _ => Abst_same (Some rel) | Istore chunk addr args src _ => - Some (store tenv chunk addr args src rel) - | Iop op args dst _ => Some (oper dst (SOp op) args rel) - | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel) - | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) - | Ibuiltin ef _ res _ => Some (kill_builtin_res res (apply_external_call ef rel)) - | Itailcall _ _ _ | Ireturn _ => RB.bot + Abst_same (Some (store tenv chunk addr args src rel)) + | Iop op args dst _ => Abst_same (Some (oper dst (SOp op) args rel)) + | Iload trap chunk addr args dst _ => Abst_same (Some (oper dst (SLoad chunk addr) args rel)) + | Icall _ _ _ dst _ => Abst_same (Some (kill_reg dst (kill_mem rel))) + | Ibuiltin ef _ res _ => Abst_same (Some (kill_builtin_res res (apply_external_call ef rel))) + | Itailcall _ _ _ | Ireturn _ => Abst_same RB.bot end. End PER_NODE. -Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t := +Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : abst_insn_out := match ro with - | None => None + | None => Abst_same RB.bot | Some x => match code ! pc with - | None => RB.bot + | None => Abst_same RB.bot | Some instr => apply_instr pc tenv instr x end end. @@ -504,10 +507,12 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva match PMap.get pc inv with | None => true | Some rel => - let rel' := apply_instr pc tenv instr rel in - List.forallb - (fun pc' => relb_leb rel' (PMap.get pc' inv)) - (RTL.successors_instr instr) + match apply_instr pc tenv instr rel with + | Abst_same rel' => + List.forallb + (fun pc' => relb_leb rel' (PMap.get pc' inv)) + (RTL.successors_instr instr) + end end). (* No longer used. Incompatible with transfer functions that yield a different result depending on the successor. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 7e456748..10ffe760 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1298,7 +1298,10 @@ Section SOUNDNESS. PTree.get pc (fn_code fn) = Some instr -> In pc' (successors_instr instr) -> RB.ge (PMap.get pc' inv) - (apply_instr' (ctx:=ctx) tenv (fn_code fn) pc (PMap.get pc inv)). + (match apply_instr' (ctx:=ctx) tenv (fn_code fn) pc + (PMap.get pc inv) with + | Abst_same rel' => rel' + end). Definition is_inductive_allstep := forall pc pc', is_inductive_step pc pc'. @@ -1317,11 +1320,14 @@ Section SOUNDNESS. pose proof (ALL INSTR) as AT_PC. destruct (inv # pc). 2: apply RB.ge_bot. - rewrite List.forallb_forall in AT_PC. unfold apply_instr'. rewrite INSTR. - apply relb_leb_correct. - auto. + destruct apply_instr. + { (* same *) + rewrite List.forallb_forall in AT_PC. + apply relb_leb_correct. + auto. + } Qed. Lemma checked_is_inductive_entry: diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 7af62b95..9a55f529 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -449,6 +449,7 @@ Lemma step_simulation: exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. Proof. induction 1; intros S1' MS; inv MS. + all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))). - (* Inop *) exists (State ts tf sp pc' rs m). split. + apply exec_Inop; auto. @@ -779,9 +780,14 @@ Proof. cbn in IND. rewrite H in IND. assert (RB.ge (fst (preanalysis tenv f)) # (if b then ifso else ifnot) - match (fst (preanalysis tenv f)) # pc with - | Some x => apply_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc tenv (Icond cond args ifso ifnot predb) x - | None => None + match + match (fst (preanalysis tenv f)) # pc with + | Some x => + apply_instr (ctx:=ctx) pc tenv (Icond cond args ifso ifnot predb) x + | None => Abst_same RB.bot + end + with + | Abst_same rel' => rel' end) as INDUCTIVE by (destruct b; intuition). clear IND. -- cgit From 816ff701ed0e448fccf0b19cfc08a91ace49123d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 00:12:18 +0100 Subject: progress moving to list of items --- backend/CSE3analysis.v | 50 ++++---- backend/CSE3analysisproof.v | 2 + backend/CSE3proof.v | 273 +++++++++++++++++++++++++++++++++----------- 3 files changed, 233 insertions(+), 92 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 8cfbaaa1..46ae4aea 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -127,9 +127,6 @@ End RELATION. Module RB := ADD_BOTTOM(RELATION). Module DS := Dataflow_Solver(RB)(NodeSetForward). -Inductive abst_insn_out := -| Abst_same : RB.t -> abst_insn_out. - Inductive sym_op : Type := | SOp : operation -> sym_op | SLoad : memory_chunk -> addressing -> sym_op. @@ -464,28 +461,29 @@ Section OPERATIONS. | _ => rel end. - Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : abst_insn_out := + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) := match instr with - | Inop _ - | Icond _ _ _ _ _ - | Ijumptable _ _ => Abst_same (Some rel) - | Istore chunk addr args src _ => - Abst_same (Some (store tenv chunk addr args src rel)) - | Iop op args dst _ => Abst_same (Some (oper dst (SOp op) args rel)) - | Iload trap chunk addr args dst _ => Abst_same (Some (oper dst (SLoad chunk addr) args rel)) - | Icall _ _ _ dst _ => Abst_same (Some (kill_reg dst (kill_mem rel))) - | Ibuiltin ef _ res _ => Abst_same (Some (kill_builtin_res res (apply_external_call ef rel))) - | Itailcall _ _ _ | Ireturn _ => Abst_same RB.bot + | Inop pc' => (pc', (Some rel))::nil + | Icond _ _ ifso ifnot _ => (ifso, (Some rel))::(ifnot, (Some rel))::nil + | Ijumptable _ targets => List.map (fun pc' => (pc', (Some rel))) targets + | Istore chunk addr args src pc' => + (pc', (Some (store tenv chunk addr args src rel)))::nil + | Iop op args dst pc' => (pc', (Some (oper dst (SOp op) args rel)))::nil + | Iload trap chunk addr args dst pc' => (pc', (Some (oper dst (SLoad chunk addr) args rel)))::nil + | Icall _ _ _ dst pc' => (pc', (Some (kill_reg dst (kill_mem rel))))::nil + | Ibuiltin ef _ res pc' => (pc', (Some (kill_builtin_res res (apply_external_call ef rel))))::nil + | Itailcall _ _ _ | Ireturn _ => nil end. End PER_NODE. -Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : abst_insn_out := - match ro with - | None => Abst_same RB.bot - | Some x => - match code ! pc with - | None => Abst_same RB.bot - | Some instr => apply_instr pc tenv instr x +Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : + list (node * RB.t) := + match code ! pc with + | None => nil + | Some instr => + match ro with + | None => List.map (fun pc' => (pc', RB.bot)) (successors_instr instr) + | Some x => apply_instr pc tenv instr x end end. @@ -507,12 +505,10 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva match PMap.get pc inv with | None => true | Some rel => - match apply_instr pc tenv instr rel with - | Abst_same rel' => - List.forallb - (fun pc' => relb_leb rel' (PMap.get pc' inv)) - (RTL.successors_instr instr) - end + List.forallb + (fun szz => + relb_leb (snd szz) (PMap.get (fst szz) inv)) + (apply_instr pc tenv instr rel) end). (* No longer used. Incompatible with transfer functions that yield a different result depending on the successor. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 10ffe760..8cc009cc 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1288,6 +1288,7 @@ Section SOUNDNESS. Hint Resolve external_call_sound : cse3. + (* Section INDUCTIVENESS. Variable fn : RTL.function. Variable tenv : typing_env. @@ -1348,4 +1349,5 @@ Section SOUNDNESS. End INDUCTIVENESS. Hint Resolve checked_is_inductive_allstep checked_is_inductive_entry : cse3. + *) End SOUNDNESS. diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 9a55f529..972cae5f 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -422,6 +422,7 @@ Qed. Hint Resolve sem_rel_b_top : cse3. +(* Ltac IND_STEP := match goal with REW: (fn_code ?fn) ! ?mpc = Some ?minstr @@ -442,20 +443,42 @@ Ltac IND_STEP := eapply rel_ge; eauto with cse3 (* ; for printing idtac mpc mpc' fn minstr *) end. - + *) + Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. Proof. induction 1; intros S1' MS; inv MS. - all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))). + all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))) in *. + all: try set (invs := (fst (preanalysis tenv f))) in *. - (* Inop *) exists (State ts tf sp pc' rs m). split. + apply exec_Inop; auto. TR_AT. reflexivity. + econstructor; eauto. - IND_STEP. + + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + unfold sem_rel_b. + apply (rel_ge inv_pc inv_pc'); auto. + (* END INVARIANT *) + - (* Iop *) exists (State ts tf sp pc' (rs # res <- v) m). split. + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'. @@ -517,9 +540,28 @@ Proof. + econstructor; eauto. * eapply wt_exec_Iop with (f:=f); try eassumption. eauto with wt. - * IND_STEP. - apply oper_sound; eauto with cse3. - + * + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Iload *) exists (State ts tf sp pc' (rs # dst <- v) m). split. + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'. @@ -576,8 +618,27 @@ Proof. + econstructor; eauto. * eapply wt_exec_Iload with (f:=f); try eassumption. eauto with wt. - * IND_STEP. - apply oper_sound; eauto with cse3. + * (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Iload notrap1 *) exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. @@ -633,8 +694,27 @@ Proof. assumption. + econstructor; eauto. * apply wt_undef; assumption. - * IND_STEP. - apply oper_sound; eauto with cse3. + * (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Iload notrap2 *) exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. @@ -691,8 +771,27 @@ Proof. assumption. + econstructor; eauto. * apply wt_undef; assumption. - * IND_STEP. - apply oper_sound; eauto with cse3. + * (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Istore *) exists (State ts tf sp pc' rs m'). split. @@ -705,8 +804,27 @@ Proof. * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. assumption. + econstructor; eauto. - IND_STEP. - apply store_sound with (a0:=a) (m0:=m); eauto with cse3. + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply store_sound with (a0:=a) (m0:=m); unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Icall *) destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. @@ -721,9 +839,29 @@ Proof. * econstructor; eauto. ** rewrite sig_preserved with (f:=fd); assumption. ** intros. - IND_STEP. - apply kill_reg_sound; eauto with cse3. - eapply kill_mem_sound; eauto with cse3. + + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + (* END INVARIANT *) + { apply kill_reg_sound; unfold ctx; eauto with cse3. + eapply kill_mem_sound; unfold ctx; eauto with cse3. } * rewrite sig_preserved with (f:=fd) by trivial. rewrite <- H7. apply wt_regset_list; auto. @@ -761,54 +899,48 @@ Proof. * eapply external_call_symbols_preserved; eauto. apply senv_preserved. + econstructor; eauto. * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt. - * IND_STEP. - apply kill_builtin_res_sound; eauto with cse3. - eapply external_call_sound; eauto with cse3. + * (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + (* END INVARIANT *) + + apply kill_builtin_res_sound; unfold ctx; eauto with cse3. + eapply external_call_sound; unfold ctx; eauto with cse3. - (* Icond *) - destruct (find_cond_in_fmap (ctx := (context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc cond args) as [bfound | ] eqn:FIND_COND. + destruct (find_cond_in_fmap (ctx := ctx) invs pc cond args) as [bfound | ] eqn:FIND_COND. + econstructor; split. * eapply exec_Inop; try eassumption. - TR_AT. unfold transf_instr. rewrite FIND_COND. reflexivity. + TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity. * replace bfound with b. { econstructor; eauto. - assert (is_inductive_allstep (ctx:= (context_from_hints (snd (preanalysis tenv f)))) f tenv (fst (preanalysis tenv f))) as IND by - (apply checked_is_inductive_allstep; - eapply transf_function_invariants_inductive; eassumption). - unfold is_inductive_allstep, is_inductive_step, apply_instr' in IND. - specialize IND with (pc:=pc) (pc':= if b then ifso else ifnot) (instr:= (Icond cond args ifso ifnot predb)). - cbn in IND. - rewrite H in IND. - assert (RB.ge (fst (preanalysis tenv f)) # (if b then ifso else ifnot) - match - match (fst (preanalysis tenv f)) # pc with - | Some x => - apply_instr (ctx:=ctx) pc tenv (Icond cond args ifso ifnot predb) x - | None => Abst_same RB.bot - end - with - | Abst_same rel' => rel' - end) as INDUCTIVE by (destruct b; intuition). - clear IND. - - change node with positive. - - destruct ((fst (preanalysis tenv f)) # pc). - 2: exfalso; exact REL. - - destruct ((fst (preanalysis tenv f)) # (if b then ifso else ifnot)). - - eapply rel_ge. exact INDUCTIVE. exact REL. - - cbn in INDUCTIVE. exfalso. exact INDUCTIVE. + admit. } - unfold find_cond_in_fmap in FIND_COND. - change RB.t with (option RELATION.t) in REL. - change Regmap.get with PMap.get in REL. - destruct (@PMap.get (option RELATION.t) pc - (@fst invariants analysis_hints (preanalysis tenv f))) as [rel | ] eqn:FIND_REL. - 2: discriminate. + unfold sem_rel_b in REL. + destruct (invs # pc) as [rel | ] eqn:FIND_REL. + 2: contradiction. pose proof (is_condition_present_sound pc rel cond args rs m REL) as COND_PRESENT_TRUE. pose proof (is_condition_present_sound pc rel (negate_condition cond) args rs m REL) as COND_PRESENT_FALSE. rewrite eval_negate_condition in COND_PRESENT_FALSE. + unfold find_cond_in_fmap in FIND_COND. + change (@PMap.get (option RELATION.t)) with (@Regmap.get RB.t) in FIND_COND. + rewrite FIND_REL in FIND_COND. destruct (is_condition_present pc rel cond args). { rewrite COND_PRESENT_TRUE in H0 by trivial. congruence. @@ -834,7 +966,8 @@ Proof. congruence. } unfold fmap_sem. - change RB.t with (option RELATION.t). + unfold sem_rel_b. + fold invs. rewrite FIND_REL. exact REL. } @@ -850,20 +983,22 @@ Proof. destruct b; trivial; cbn in H2; discriminate. } unfold fmap_sem. - change RB.t with (option RELATION.t). + unfold sem_rel_b. + fold invs. rewrite FIND_REL. exact REL. } discriminate. + econstructor; split. * eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. - ** TR_AT. unfold transf_instr. rewrite FIND_COND. + ** TR_AT. unfold transf_instr. fold invs. fold ctx. + rewrite FIND_COND. reflexivity. ** rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. eassumption. ** reflexivity. * econstructor; eauto. - destruct b; IND_STEP. + admit. - (* Ijumptable *) econstructor. split. @@ -872,8 +1007,7 @@ Proof. * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. assumption. + econstructor; eauto. - assert (In pc' tbl) as IN_LIST by (eapply list_nth_z_in; eassumption). - IND_STEP. + admit. - (* Ireturn *) destruct or as [arg | ]. @@ -915,9 +1049,18 @@ Proof. apply wt_init_regs. rewrite <- wt_params in WTARGS. assumption. - * rewrite @checked_is_inductive_entry with (tenv:=tenv) (ctx:=(context_from_hints (snd (preanalysis tenv f)))). - ** apply sem_rel_b_top. - ** apply transf_function_invariants_inductive with (tf:=tf); auto. + * assert ((check_inductiveness f tenv (fst (preanalysis tenv f)))=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + clear IND_step. + apply RB.beq_correct in IND_entry. + unfold RB.eq in *. + destruct ((fst (preanalysis tenv f)) # (fn_entrypoint f)). + 2: contradiction. + cbn. + rewrite <- IND_entry. + apply sem_rel_top. - (* external *) simpl in FUN. @@ -935,7 +1078,7 @@ Proof. apply wt_regset_assign; trivial. rewrite WTRES0. exact WTRES. -Qed. +Admitted. Lemma transf_initial_states: forall S1, RTL.initial_state prog S1 -> -- cgit From cf8ff0b0407cd0b4981f363418fde7f96e95d6a5 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 08:46:25 +0100 Subject: CSE3 compiles again, but some admitted lemmas --- backend/CSE3analysisaux.ml | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index b8f98b0d..efe6b600 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -137,8 +137,7 @@ let rb_glb (x : RB.t) (y : RB.t) : RB.t = let compute_invariants (nodes : RTL.node list) (entrypoint : RTL.node) - (successors : RTL.node -> RTL.node list) - (tfr : RTL.node -> RB.t -> RB.t) = + (tfr : RTL.node -> RB.t -> (RTL.node * RB.t) list) = let todo = ref IntSet.empty and invariants = ref (PMap.set entrypoint (Some RELATION.top) (PMap.init RB.bot)) in let add_todo (pc : RTL.node) = @@ -147,13 +146,13 @@ let compute_invariants (if !Clflags.option_debug_compcert > 9 then Printf.printf "UP updating node %d\n" (P.to_int pc)); let cur = PMap.get pc !invariants in - List.iter (fun next_pc -> + List.iter (fun (next_pc, next_contrib) -> let previous = PMap.get next_pc !invariants in - let next = RB.lub previous (tfr pc cur) in + let next = RB.lub previous next_contrib in if not (RB.beq previous next) then ( invariants := PMap.set next_pc next !invariants; - add_todo next_pc)) (successors pc) in + add_todo next_pc)) (tfr pc cur) in add_todo entrypoint; while not (IntSet.is_empty !todo) do let nxt = IntSet.max_elt !todo in @@ -167,7 +166,8 @@ let refine_invariants (entrypoint : RTL.node) (successors : RTL.node -> RTL.node list) (predecessors : RTL.node -> RTL.node list) - (tfr : RTL.node -> RB.t -> RB.t) (invariants0 : RB.t PMap.t) = + (tfr : RTL.node -> RB.t -> (RTL.node * RB.t) list) + (invariants0 : RB.t PMap.t) = let todo = ref IntSet.empty and invariants = ref invariants0 in let add_todo (pc : RTL.node) = @@ -182,7 +182,7 @@ let refine_invariants (List.map (fun pred_pc-> rb_glb cur - (tfr pred_pc (PMap.get pred_pc !invariants))) + (List.assoc pc (tfr pred_pc (PMap.get pred_pc !invariants)))) (predecessors pc)) in if not (RB.beq cur nxt) then @@ -205,12 +205,10 @@ let get_default default x ptree = | Some y -> y;; let initial_analysis ctx tenv (f : RTL.coq_function) = - let succ_map = RTL.successors_map f in - let succ_f x = get_default [] x succ_map in let tfr = apply_instr' ctx tenv f.RTL.fn_code in compute_invariants (List.map fst (PTree.elements f.RTL.fn_code)) - f.RTL.fn_entrypoint succ_f tfr;; + f.RTL.fn_entrypoint tfr;; let refine_analysis ctx tenv (f : RTL.coq_function) (invariants0 : RB.t PMap.t) = -- cgit From b4af6cbe24b1108b4e49d3c17fecc37255bd6151 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 09:07:32 +0100 Subject: avancement dans les preuves --- backend/CSE3proof.v | 35 ++++++++++++++++++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 972cae5f..69e779cd 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -930,7 +930,40 @@ Proof. TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity. * replace bfound with b. { econstructor; eauto. - admit. + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + rewrite andb_true_iff in IND_step_me. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me as [IND_so [IND_not ZOT]]. + clear ZOT. + destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *. + 2: discriminate. + destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *. + 2: discriminate. + rewrite rel_leb_correct in IND_so. + rewrite rel_leb_correct in IND_not. + destruct b. + { + rewrite INV_so. + cbn. + eapply rel_ge; eauto. + } + { + rewrite INV_not. + cbn. + eapply rel_ge; eauto. + } + (* END INVARIANT *) } unfold sem_rel_b in REL. destruct (invs # pc) as [rel | ] eqn:FIND_REL. -- cgit From 8f2cf0b53b3a7fd4bc339fddf89197601eb549c2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 09:13:40 +0100 Subject: one 'admit' less --- backend/CSE3proof.v | 38 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 36 insertions(+), 2 deletions(-) (limited to 'backend') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 69e779cd..661329e8 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -930,7 +930,7 @@ Proof. TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity. * replace bfound with b. { econstructor; eauto. - (* BEGIN INVARIANT *) + (* BEGIN INVARIANT *) fold ctx. fold invs. assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). unfold check_inductiveness in IND. @@ -1031,7 +1031,41 @@ Proof. eassumption. ** reflexivity. * econstructor; eauto. - admit. + + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + rewrite andb_true_iff in IND_step_me. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me as [IND_so [IND_not ZOT]]. + clear ZOT. + destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *. + 2: discriminate. + destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *. + 2: discriminate. + rewrite rel_leb_correct in IND_so. + rewrite rel_leb_correct in IND_not. + destruct b. + { + rewrite INV_so. + cbn. + eapply rel_ge; eauto. + } + { + rewrite INV_not. + cbn. + eapply rel_ge; eauto. + } + (* END INVARIANT *) - (* Ijumptable *) econstructor. split. -- cgit From 04667b444164f8a54c1aab0a8e2422e1951bf9bc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 09:47:24 +0100 Subject: proof for jumptable --- backend/CSE3proof.v | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 661329e8..cc4ab686 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -1074,7 +1074,33 @@ Proof. * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. assumption. + econstructor; eauto. - admit. + + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + rewrite forallb_forall in IND_step_me. + assert (RB.ge (invs # pc') (Some inv_pc)) as GE. + { + apply relb_leb_correct. + specialize IND_step_me with (pc', Some inv_pc). + apply IND_step_me. + apply (in_map (fun pc'0 : node => (pc'0, Some inv_pc))). + eapply list_nth_z_in. + eassumption. + } + destruct (invs # pc'); cbn in *. + 2: contradiction. + eapply rel_ge; eauto. + (* END INVARIANT *) - (* Ireturn *) destruct or as [arg | ]. -- cgit From 414c9f51fc8dcafe5a1deb873c682105ba554bb8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 10:30:41 +0100 Subject: apply_cond1_sound --- backend/CSE3analysisproof.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) (limited to 'backend') diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 8cc009cc..75dae91a 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1288,6 +1288,36 @@ Section SOUNDNESS. Hint Resolve external_call_sound : cse3. + + Definition sem_rel_b (rel : RB.t) (rs : regset) (m : mem) := + match rel with + | None => False + | Some rel => sem_rel rel rs m + end. + + Lemma apply_cond1_sound : + forall pc cond args rel rs m + (COND : (eval_condition cond (rs ## args) m) = Some true) + (REL : (sem_rel rel rs m)), + (sem_rel_b (apply_cond1 (ctx:=ctx) pc cond args rel) rs m). + Proof. + intros. + unfold apply_cond1. + destruct eq_find as [eq_id | ] eqn:FIND; cbn. + 2: assumption. + destruct PSet.contains eqn:CONTAINS. + { + pose proof (eq_find_sound pc (Cond (negate_condition cond) args) eq_id FIND) as FIND_SOUND. + unfold sem_rel in REL. + pose proof (REL eq_id (Cond (negate_condition cond) args) CONTAINS FIND_SOUND) as REL_id. + cbn in REL_id. + rewrite eval_negate_condition in REL_id. + rewrite COND in REL_id. + discriminate. + } + exact REL. + Qed. + (* Section INDUCTIVENESS. Variable fn : RTL.function. -- cgit From a54ea2bfba2ca35b968bbad36bd7e24e5da124c0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 10:49:55 +0100 Subject: apply_cond0_sound --- backend/CSE3analysisproof.v | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 75dae91a..a012771c 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1317,7 +1317,31 @@ Section SOUNDNESS. } exact REL. Qed. - + + Lemma apply_cond0_sound : + forall pc cond args rel rs m + (COND : (eval_condition cond (rs ## args) m) = Some true) + (REL : (sem_rel rel rs m)), + (sem_rel (apply_cond0 (ctx:=ctx) pc cond args rel) rs m). + Proof. + intros. + unfold apply_cond0. + destruct eq_find as [eq_id | ] eqn:FIND; cbn. + 2: assumption. + pose proof (eq_find_sound pc (Cond cond args) eq_id FIND) as FIND_SOUND. + intros eq_id' eq' CONTAINS CATALOG. + destruct (peq eq_id eq_id'). + { subst eq_id'. + unfold sem_eq. + rewrite FIND_SOUND in CATALOG. + inv CATALOG. + assumption. + } + rewrite PSet.gaddo in CONTAINS by assumption. + unfold sem_rel in REL. + eapply REL; eassumption. + Qed. + (* Section INDUCTIVENESS. Variable fn : RTL.function. -- cgit From a0529ae7a4eb991c39f258a8dbc003dd83ad3d36 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 11:02:56 +0100 Subject: apply_cond_sound --- backend/CSE3analysisproof.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'backend') diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index a012771c..29d171eb 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1341,6 +1341,20 @@ Section SOUNDNESS. unfold sem_rel in REL. eapply REL; eassumption. Qed. + + Lemma apply_cond_sound : + forall pc cond args rel rs m + (COND : (eval_condition cond (rs ## args) m) = Some true) + (REL : (sem_rel rel rs m)), + (sem_rel_b (apply_cond (ctx:=ctx) pc cond args rel) rs m). + Proof. + unfold apply_cond. + intros. + pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1. + destruct apply_cond1 eqn:COND1. + { apply apply_cond0_sound; auto. } + exact SOUND1. + Qed. (* Section INDUCTIVENESS. -- cgit From 79c039d7b33878d00f22ad8542dc30a78aa8b70a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 11:34:35 +0100 Subject: CSE3 + conditions proof --- backend/CSE3analysis.v | 25 ++++++++++++++++++- backend/CSE3proof.v | 67 +++++++++++++++++++++++++------------------------- 2 files changed, 58 insertions(+), 34 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 46ae4aea..383147bb 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -461,10 +461,33 @@ Section OPERATIONS. | _ => rel end. + Definition apply_cond1 cond args (rel : RELATION.t) : RB.t := + match eq_find (Cond (negate_condition cond) args) with + | Some eq_id => + if PSet.contains rel eq_id + then RB.bot + else Some rel + | None => Some rel + end. + + Definition apply_cond0 cond args (rel : RELATION.t) : RELATION.t := + match eq_find (Cond cond args) with + | Some eq_id => PSet.add eq_id rel + | None => rel + end. + + Definition apply_cond cond args (rel : RELATION.t) : RB.t := + match apply_cond1 cond args rel with + | Some rel => Some (apply_cond0 cond args rel) + | None => RB.bot + end. + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) := match instr with | Inop pc' => (pc', (Some rel))::nil - | Icond _ _ ifso ifnot _ => (ifso, (Some rel))::(ifnot, (Some rel))::nil + | Icond cond args ifso ifnot _ => + (ifso, (apply_cond cond args rel)):: + (ifnot, (apply_cond (negate_condition cond) args rel))::nil | Ijumptable _ targets => List.map (fun pc' => (pc', (Some rel))) targets | Istore chunk addr args src pc' => (pc', (Some (store tenv chunk addr args src rel)))::nil diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index cc4ab686..50a32d56 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -352,6 +352,23 @@ Qed. Hint Resolve rel_ge : cse3. +Lemma relb_ge: + forall inv inv' + (GE : RB.ge inv' inv) + ctx sp rs m + (REL: sem_rel_b sp ctx inv rs m), + sem_rel_b sp ctx inv' rs m. +Proof. + intros. + destruct inv; cbn in *. + 2: contradiction. + destruct inv'; cbn in *. + 2: assumption. + eapply rel_ge; eassumption. +Qed. + +Hint Resolve relb_ge : cse3. + Lemma sem_rhs_sop : forall sp op rs args m v, eval_operation ge sp op rs ## args m = Some v -> @@ -946,23 +963,15 @@ Proof. rewrite andb_true_iff in IND_step_me. destruct IND_step_me as [IND_so [IND_not ZOT]]. clear ZOT. - destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *. - 2: discriminate. - destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *. - 2: discriminate. - rewrite rel_leb_correct in IND_so. - rewrite rel_leb_correct in IND_not. + rewrite relb_leb_correct in IND_so. + rewrite relb_leb_correct in IND_not. + destruct b. - { - rewrite INV_so. - cbn. - eapply rel_ge; eauto. - } - { - rewrite INV_not. - cbn. - eapply rel_ge; eauto. - } + { eapply relb_ge. eassumption. apply apply_cond_sound; auto. } + eapply relb_ge. eassumption. apply apply_cond_sound; trivial. + rewrite eval_negate_condition. + rewrite H0. + reflexivity. (* END INVARIANT *) } unfold sem_rel_b in REL. @@ -1048,23 +1057,15 @@ Proof. rewrite andb_true_iff in IND_step_me. destruct IND_step_me as [IND_so [IND_not ZOT]]. clear ZOT. - destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *. - 2: discriminate. - destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *. - 2: discriminate. - rewrite rel_leb_correct in IND_so. - rewrite rel_leb_correct in IND_not. + rewrite relb_leb_correct in IND_so. + rewrite relb_leb_correct in IND_not. + destruct b. - { - rewrite INV_so. - cbn. - eapply rel_ge; eauto. - } - { - rewrite INV_not. - cbn. - eapply rel_ge; eauto. - } + { eapply relb_ge. eassumption. apply apply_cond_sound; auto. } + eapply relb_ge. eassumption. apply apply_cond_sound; trivial. + rewrite eval_negate_condition. + rewrite H0. + reflexivity. (* END INVARIANT *) - (* Ijumptable *) @@ -1171,7 +1172,7 @@ Proof. apply wt_regset_assign; trivial. rewrite WTRES0. exact WTRES. -Admitted. +Qed. Lemma transf_initial_states: forall S1, RTL.initial_state prog S1 -> -- cgit From 0a13bf127bb385df424bd9e392742d4fc5bef86a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 13:15:53 +0100 Subject: begin implementing -fcse3-conditions --- backend/CSE3analysis.v | 11 +++++++---- backend/CSE3analysisproof.v | 12 ++++++++---- 2 files changed, 15 insertions(+), 8 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 383147bb..75e00f67 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -477,10 +477,13 @@ Section OPERATIONS. end. Definition apply_cond cond args (rel : RELATION.t) : RB.t := - match apply_cond1 cond args rel with - | Some rel => Some (apply_cond0 cond args rel) - | None => RB.bot - end. + if Compopts.optim_CSE3_conditions tt + then + match apply_cond1 cond args rel with + | Some rel => Some (apply_cond0 cond args rel) + | None => RB.bot + end + else Some rel. Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) := match instr with diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 29d171eb..d53cf604 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1350,10 +1350,14 @@ Section SOUNDNESS. Proof. unfold apply_cond. intros. - pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1. - destruct apply_cond1 eqn:COND1. - { apply apply_cond0_sound; auto. } - exact SOUND1. + destruct (Compopts.optim_CSE3_conditions tt). + { + pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1. + destruct apply_cond1 eqn:COND1. + { apply apply_cond0_sound; auto. } + exact SOUND1. + } + exact REL. Qed. (* -- cgit From eb1121d703835e76babc15b057276d2852ade4ab Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 16:25:46 +0100 Subject: totally switch off conditions in cse3 --- backend/CSE3.v | 35 +++++++++++++++++++---------------- backend/CSE3proof.v | 2 ++ 2 files changed, 21 insertions(+), 16 deletions(-) (limited to 'backend') diff --git a/backend/CSE3.v b/backend/CSE3.v index 482069d7..3a680cf7 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -54,22 +54,25 @@ Definition subst_args fmap pc xl := forward_move_l_b (PMap.get pc fmap) xl. Definition find_cond_in_fmap fmap pc cond args := - match PMap.get pc fmap with - | Some rel => - if is_condition_present (ctx:=ctx) pc rel cond args - then Some true - else - let ncond := negate_condition cond in - if is_condition_present (ctx:=ctx) pc rel ncond args - then Some false - else let args' := subst_args fmap pc args in - if is_condition_present (ctx:=ctx) pc rel cond args' - then Some true - else if is_condition_present (ctx:=ctx) pc rel ncond args' - then Some false - else None - | None => None - end. + if Compopts.optim_CSE3_conditions tt + then + match PMap.get pc fmap with + | Some rel => + if is_condition_present (ctx:=ctx) pc rel cond args + then Some true + else + let ncond := negate_condition cond in + if is_condition_present (ctx:=ctx) pc rel ncond args + then Some false + else let args' := subst_args fmap pc args in + if is_condition_present (ctx:=ctx) pc rel cond args' + then Some true + else if is_condition_present (ctx:=ctx) pc rel ncond args' + then Some false + else None + | None => None + end + else None. Definition transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) := diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 50a32d56..ca43d0bd 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -983,6 +983,8 @@ Proof. unfold find_cond_in_fmap in FIND_COND. change (@PMap.get (option RELATION.t)) with (@Regmap.get RB.t) in FIND_COND. rewrite FIND_REL in FIND_COND. + destruct (Compopts.optim_CSE3_conditions tt). + 2: discriminate. destruct (is_condition_present pc rel cond args). { rewrite COND_PRESENT_TRUE in H0 by trivial. congruence. -- cgit