diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CSE2.v | 115 | ||||
| -rw-r--r-- | backend/CSE3.v | 93 | ||||
| -rw-r--r-- | backend/CSE3analysis.v | 403 | ||||
| -rw-r--r-- | backend/CSE3analysisaux.ml | 97 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 926 | ||||
| -rw-r--r-- | backend/CSE3proof.v | 875 | ||||
| -rw-r--r-- | backend/FirstNop.v | 18 | ||||
| -rw-r--r-- | backend/FirstNopproof.v | 274 |
8 files changed, 2687 insertions, 114 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index d5444e3b..efa70b40 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -29,7 +29,7 @@ Proof. decide equality. Defined. -Module RELATION. +Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. Definition t := (PTree.t sym_val). Definition eq (r1 r2 : t) := @@ -138,119 +138,6 @@ Qed. End RELATION. -Module Type SEMILATTICE_WITHOUT_BOTTOM. - - Parameter t: Type. - Parameter eq: t -> t -> Prop. - Axiom eq_refl: forall x, eq x x. - Axiom eq_sym: forall x y, eq x y -> eq y x. - Axiom eq_trans: forall x y z, eq x y -> eq y z -> eq x z. - Parameter beq: t -> t -> bool. - Axiom beq_correct: forall x y, beq x y = true -> eq x y. - Parameter ge: t -> t -> Prop. - Axiom ge_refl: forall x y, eq x y -> ge x y. - Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Parameter lub: t -> t -> t. - Axiom ge_lub_left: forall x y, ge (lub x y) x. - Axiom ge_lub_right: forall x y, ge (lub x y) y. - -End SEMILATTICE_WITHOUT_BOTTOM. - -Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM). - Definition t := option L.t. - Definition eq (a b : t) := - match a, b with - | None, None => True - | Some x, Some y => L.eq x y - | Some _, None | None, Some _ => False - end. - - Lemma eq_refl: forall x, eq x x. - Proof. - unfold eq; destruct x; trivial. - apply L.eq_refl. - Qed. - - Lemma eq_sym: forall x y, eq x y -> eq y x. - Proof. - unfold eq; destruct x; destruct y; trivial. - apply L.eq_sym. - Qed. - - Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. - Proof. - unfold eq; destruct x; destruct y; destruct z; trivial. - - apply L.eq_trans. - - contradiction. - Qed. - - Definition beq (x y : t) := - match x, y with - | None, None => true - | Some x, Some y => L.beq x y - | Some _, None | None, Some _ => false - end. - - Lemma beq_correct: forall x y, beq x y = true -> eq x y. - Proof. - unfold beq, eq. - destruct x; destruct y; trivial; try congruence. - apply L.beq_correct. - Qed. - - Definition ge (x y : t) := - match x, y with - | None, Some _ => False - | _, None => True - | Some a, Some b => L.ge a b - end. - - Lemma ge_refl: forall x y, eq x y -> ge x y. - Proof. - unfold eq, ge. - destruct x; destruct y; trivial. - apply L.ge_refl. - Qed. - - Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Proof. - unfold ge. - destruct x; destruct y; destruct z; trivial; try contradiction. - apply L.ge_trans. - Qed. - - Definition bot: t := None. - Lemma ge_bot: forall x, ge x bot. - Proof. - unfold ge, bot. - destruct x; trivial. - Qed. - - Definition lub (a b : t) := - match a, b with - | None, _ => b - | _, None => a - | (Some x), (Some y) => Some (L.lub x y) - end. - - Lemma ge_lub_left: forall x y, ge (lub x y) x. - Proof. - unfold ge, lub. - destruct x; destruct y; trivial. - - apply L.ge_lub_left. - - apply L.ge_refl. - apply L.eq_refl. - Qed. - - Lemma ge_lub_right: forall x y, ge (lub x y) y. - Proof. - unfold ge, lub. - destruct x; destruct y; trivial. - - apply L.ge_lub_right. - - apply L.ge_refl. - apply L.eq_refl. - Qed. -End ADD_BOTTOM. Module RB := ADD_BOTTOM(RELATION). Module DS := Dataflow_Solver(RB)(NodeSetForward). diff --git a/backend/CSE3.v b/backend/CSE3.v new file mode 100644 index 00000000..d0dc3aef --- /dev/null +++ b/backend/CSE3.v @@ -0,0 +1,93 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps CSE2deps. +Require Import CSE3analysis HashedSet. +Require Import RTLtyping. + +Local Open Scope error_monad_scope. + +Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints. + +Section REWRITE. + Context {ctx : eq_context}. + +Definition find_op_in_fmap fmap pc op args := + match PMap.get pc fmap with + | Some rel => rhs_find (ctx:=ctx) pc (SOp op) args rel + | None => None + end. + +Definition find_load_in_fmap fmap pc chunk addr args := + match PMap.get pc fmap with + | Some rel => rhs_find (ctx:=ctx) pc (SLoad chunk addr) args rel + | None => None + end. + +Definition forward_move_b (rb : RB.t) (x : reg) := + match rb with + | None => x + | Some rel => forward_move (ctx := ctx) rel x + end. + +Definition subst_arg (fmap : PMap.t RB.t) (pc : node) (x : reg) : reg := + forward_move_b (PMap.get pc fmap) x. + +Definition forward_move_l_b (rb : RB.t) (xl : list reg) := + match rb with + | None => xl + | Some rel => forward_move_l (ctx := ctx) rel xl + end. + +Definition subst_args fmap pc xl := + forward_move_l_b (PMap.get pc fmap) xl. + +Definition transf_instr (fmap : PMap.t RB.t) + (pc: node) (instr: instruction) := + match instr with + | Iop op args dst s => + let args' := subst_args fmap pc args in + match (if is_trivial_op op then None else find_op_in_fmap fmap pc op args') with + | None => Iop op args' dst s + | Some src => Iop Omove (src::nil) dst s + end + | Iload trap chunk addr args dst s => + let args' := subst_args fmap pc args in + match find_load_in_fmap fmap pc chunk addr args' with + | None => Iload trap chunk addr args' dst s + | Some src => Iop Omove (src::nil) dst s + end + | Istore chunk addr args src s => + Istore chunk addr (subst_args fmap pc args) src s + | Icall sig ros args dst s => + Icall sig ros (subst_args fmap pc args) dst s + | Itailcall sig ros args => + Itailcall sig ros (subst_args fmap pc args) + | Icond cond args s1 s2 => + Icond cond (subst_args fmap pc args) s1 s2 + | Ijumptable arg tbl => + Ijumptable (subst_arg fmap pc arg) tbl + | Ireturn (Some arg) => + Ireturn (Some (subst_arg fmap pc arg)) + | _ => instr + end. +End REWRITE. + +Definition transf_function (f: function) : res function := + do tenv <- type_function f; + let (invariants, hints) := preanalysis tenv f in + let ctx := context_from_hints hints in + if check_inductiveness (ctx:=ctx) f tenv invariants + then + OK {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := PTree.map (transf_instr (ctx := ctx) invariants) + f.(fn_code); + fn_entrypoint := f.(fn_entrypoint) |} + else Error (msg "cse3: not inductive"). + +Definition transf_fundef (fd: fundef) : res fundef := + AST.transf_partial_fundef transf_function fd. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v new file mode 100644 index 00000000..12fb2d1f --- /dev/null +++ b/backend/CSE3analysis.v @@ -0,0 +1,403 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps CSE2deps. +Require Import HashedSet. +Require List Compopts. + +Definition typing_env := reg -> typ. + +Definition loadv_storev_compatible_type + (chunk : memory_chunk) (ty : typ) : bool := + match chunk, ty with + | Mint32, Tint + | Mint64, Tlong + | Mfloat32, Tsingle + | Mfloat64, Tfloat => true + | _, _ => false + end. + +Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. + Definition t := PSet.t. + Definition eq (x : t) (y : t) := x = y. + + Lemma eq_refl: forall x, eq x x. + Proof. + unfold eq. trivial. + Qed. + + Lemma eq_sym: forall x y, eq x y -> eq y x. + Proof. + unfold eq. congruence. + Qed. + + Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Proof. + unfold eq. congruence. + Qed. + + Definition beq (x y : t) := if PSet.eq x y then true else false. + + Lemma beq_correct: forall x y, beq x y = true -> eq x y. + Proof. + unfold beq. + intros. + destruct PSet.eq; congruence. + Qed. + + Definition ge (x y : t) := (PSet.is_subset x y) = true. + + Lemma ge_refl: forall x y, eq x y -> ge x y. + Proof. + unfold eq, ge. + intros. + subst y. + apply PSet.is_subset_spec. + trivial. + Qed. + + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge. + intros. + rewrite PSet.is_subset_spec in *. + intuition. + Qed. + + Definition lub := PSet.inter. + + Lemma ge_lub_left: forall x y, ge (lub x y) x. + Proof. + unfold ge, lub. + intros. + apply PSet.is_subset_spec. + intro. + rewrite PSet.ginter. + rewrite andb_true_iff. + intuition. + Qed. + + Lemma ge_lub_right: forall x y, ge (lub x y) y. + Proof. + unfold ge, lub. + intros. + apply PSet.is_subset_spec. + intro. + rewrite PSet.ginter. + rewrite andb_true_iff. + intuition. + Qed. + + Definition top := PSet.empty. +End RELATION. + +Module RB := ADD_BOTTOM(RELATION). +Module DS := Dataflow_Solver(RB)(NodeSetForward). + +Inductive sym_op : Type := +| SOp : operation -> sym_op +| SLoad : memory_chunk -> addressing -> sym_op. + +Definition eq_dec_sym_op : forall s s' : sym_op, {s = s'} + {s <> s'}. +Proof. + generalize eq_operation. + generalize eq_addressing. + generalize chunk_eq. + decide equality. +Defined. + +Definition eq_dec_args : forall l l' : list reg, { l = l' } + { l <> l' }. +Proof. + apply List.list_eq_dec. + exact peq. +Defined. + +Record equation := + mkequation + { eq_lhs : reg; + eq_op : sym_op; + eq_args : list reg }. + +Definition eq_dec_equation : + forall eq eq' : equation, {eq = eq'} + {eq <> eq'}. +Proof. + generalize peq. + generalize eq_dec_sym_op. + 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) := + Regmap.set i (PSet.add j (Regmap.get i m)) m. + +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) : + 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 + (PMap.init PSet.empty). + +Definition eq_depends_on_mem eq := + match eq_op eq with + | SLoad _ _ => true + | SOp op => op_depends_on_memory op + 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 + then PSet.add eqno already + else already) eqs PSet.empty. + +Definition is_move (op : operation) : + { op = Omove } + { op <> Omove }. +Proof. + destruct op; try (right ; congruence). + left; trivial. +Qed. + +Definition is_smove (sop : sym_op) : + { sop = SOp Omove } + { sop <> SOp Omove }. +Proof. + destruct sop; try (right ; congruence). + destruct (is_move o). + - left; congruence. + - right; congruence. +Qed. + +Definition get_moves (eqs : PTree.t equation) : + 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). + +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_moves : reg -> PSet.t }. + +Section OPERATIONS. + Context {ctx : eq_context}. + + Definition kill_reg (r : reg) (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_reg ctx r). + + Definition kill_mem (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_mem ctx tt). + + Definition pick_source (l : list reg) := (* todo: take min? *) + match l with + | h::t => Some h + | nil => None + end. + + Definition forward_move (rel : RELATION.t) (x : reg) : reg := + match pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x))) with + | None => x + | Some eqno => + match eq_catalog ctx eqno with + | Some eq => + if is_smove (eq_op eq) && peq x (eq_lhs eq) + then + match eq_args eq with + | src::nil => src + | _ => x + end + else x + | _ => x + end + end. + + Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := + List.map (forward_move rel). + + Section PER_NODE. + Variable no : node. + + Definition eq_find (eq : equation) := + match eq_find_oracle ctx no eq with + | Some id => + match eq_catalog ctx id with + | Some eq' => if eq_dec_equation eq eq' then Some id else None + | None => None + end + | None => None + 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 + | None => None + | 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) + else None + end + end. + + Definition oper2 (dst : reg) (op: sym_op)(args : list reg) + (rel : RELATION.t) : RELATION.t := + let rel' := kill_reg dst rel in + match eq_find {| eq_lhs := dst; + eq_op := op; + eq_args:= args |} with + | Some id => PSet.add id rel' + | None => rel' + end. + + Definition oper1 (dst : reg) (op: sym_op) (args : list reg) + (rel : RELATION.t) : RELATION.t := + if List.in_dec peq dst args + then kill_reg dst rel + else oper2 dst op args rel. + + + Definition move (src dst : reg) (rel : RELATION.t) : RELATION.t := + match eq_find {| eq_lhs := dst; + eq_op := SOp Omove; + eq_args:= src::nil |} with + | Some eq_id => PSet.add eq_id (kill_reg dst rel) + | None => kill_reg dst rel + end. + + Definition oper (dst : reg) (op: sym_op) (args : list reg) + (rel : RELATION.t) : RELATION.t := + match rhs_find op (forward_move_l rel args) rel with + | Some r => move r dst rel + | None => oper1 dst op args rel + end. + + Definition clever_kill_store + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) + (rel : RELATION.t) : RELATION.t := + PSet.subtract rel + (PSet.filter + (fun eqno => + match eq_catalog ctx eqno with + | None => false + | Some eq => + match eq_op eq with + | SOp op => true + | SLoad chunk' addr' => + may_overlap chunk addr args chunk' addr' (eq_args eq) + end + end) + (PSet.inter rel (eq_kill_mem ctx tt))). + + Definition store2 + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) + (rel : RELATION.t) : RELATION.t := + if Compopts.optim_CSE3_alias_analysis tt + then clever_kill_store chunk addr args src rel + else kill_mem rel. + + Definition store1 + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) (ty: typ) + (rel : RELATION.t) : RELATION.t := + 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 + | Some id => PSet.add id rel' + | None => rel' + end + else rel'. + + Definition store + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) (ty: typ) + (rel : RELATION.t) : RELATION.t := + store1 chunk addr (forward_move_l rel args) src ty rel. + + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t := + match instr with + | Inop _ + | Icond _ _ _ _ + | Ijumptable _ _ => Some rel + | Istore chunk addr args src _ => + Some (store chunk addr args src (tenv 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 _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *) + | Itailcall _ _ _ | Ireturn _ => RB.bot + end. + End PER_NODE. + +Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t := + match ro with + | None => None + | Some x => + match code ! pc with + | None => RB.bot + | Some instr => apply_instr pc tenv instr x + end + end. + +Definition invariants := PMap.t RB.t. + +Definition rel_leb (x y : RELATION.t) : bool := (PSet.is_subset y x). + +Definition relb_leb (x y : RB.t) : bool := + match x, y with + | None, _ => true + | (Some _), None => false + | (Some x), (Some y) => rel_leb x y + end. + +Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: invariants) := + (RB.beq (Some RELATION.top) (PMap.get (fn_entrypoint fn) inv)) && + PTree_Properties.for_all (fn_code fn) + (fun pc instr => + 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) + end). + +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 := + mkanalysis_hints + { hint_eq_catalog : PTree.t equation; + hint_eq_find_oracle : node -> equation -> option eq_id; + hint_eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t }. + +Definition context_from_hints (hints : analysis_hints) := + let eqs := hint_eq_catalog hints in + let reg_kills := get_reg_kills eqs in + let mem_kills := get_mem_kills eqs in + let moves := get_moves eqs in + {| + eq_catalog := fun eq_id => PTree.get eq_id eqs; + eq_find_oracle := hint_eq_find_oracle hints ; + eq_rhs_oracle := hint_eq_rhs_oracle hints; + eq_kill_reg := fun reg => PMap.get reg reg_kills; + eq_kill_mem := fun _ => mem_kills; + eq_moves := fun reg => PMap.get reg moves + |}. diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml new file mode 100644 index 00000000..23e20ea8 --- /dev/null +++ b/backend/CSE3analysisaux.ml @@ -0,0 +1,97 @@ +open CSE3analysis +open Maps +open HashedSet +open Camlcoq + +let flatten_eq eq = + ((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);; + +let imp_add_i_j s i j = + s := PMap.set i (PSet.add j (PMap.get i !s)) !s;; + +let string_of_chunk = function + | AST.Mint8signed -> "int8signed" + | AST.Mint8unsigned -> "int8unsigned" + | AST.Mint16signed -> "int16signed" + | AST.Mint16unsigned -> "int16unsigned" + | AST.Mint32 -> "int32" + | AST.Mint64 -> "int64" + | AST.Mfloat32 -> "float32" + | AST.Mfloat64 -> "float64" + | AST.Many32 -> "any32" + | AST.Many64 -> "any64";; + +let print_reg channel i = + Printf.fprintf channel "r%d" i;; + +let print_eq channel (lhs, sop, args) = + match sop with + | SOp op -> + Printf.printf "%a = %a\n" print_reg lhs (PrintOp.print_operation print_reg) (op, args) + | SLoad(chunk, addr) -> + Printf.printf "%a = %s @ %a\n" print_reg lhs (string_of_chunk chunk) + (PrintOp.print_addressing print_reg) (addr, args);; + +let print_set s = + Printf.printf "{ "; + List.iter (fun i -> Printf.printf "%d; " (P.to_int i)) (PSet.elements s); + Printf.printf "}\n";; + +let 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 cur_kill_reg = ref (PMap.init PSet.empty) + and cur_kill_mem = ref PSet.empty + and cur_moves = ref (PMap.init PSet.empty) in + let eq_find_oracle node eq = + Hashtbl.find_opt eq_table (flatten_eq eq) + and rhs_find_oracle node sop args = + match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with + | None -> PSet.empty + | Some s -> s in + let 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 + 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); + 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 + then cur_kill_mem := PSet.add coq_id !cur_kill_mem); + (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 + match + internal_analysis + { 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_moves = (fun reg -> PMap.get reg !cur_moves) + } tenv f + with None -> failwith "CSE3analysisaux analysis failed, try re-running with -fno-cse3" + | Some invariants -> + invariants, + { hint_eq_catalog = !cur_catalog; + hint_eq_find_oracle= eq_find_oracle; + hint_eq_rhs_oracle = rhs_find_oracle };; diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v new file mode 100644 index 00000000..b87ec92c --- /dev/null +++ b/backend/CSE3analysisproof.v @@ -0,0 +1,926 @@ + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE3analysis CSE2deps CSE2depsproof HashedSet. +Require Import RTLtyping. +Require Import Lia. + +Lemma rel_leb_correct: + forall x x', + rel_leb x x' = true <-> RELATION.ge x' x. +Proof. + unfold rel_leb, RELATION.ge. + split; auto. +Qed. + +Hint Resolve rel_leb_correct : cse3. + +Lemma relb_leb_correct: + forall x x', + relb_leb x x' = true <-> RB.ge x' x. +Proof. + unfold relb_leb, RB.ge. + destruct x; destruct x'; split; trivial; try contradiction; discriminate. +Qed. + +Hint Resolve relb_leb_correct : cse3. + +Theorem loadv_storev_really_same: + forall chunk: memory_chunk, + forall m1: mem, + forall addr v: val, + forall m2: mem, + forall ty : typ, + forall TYPE: Val.has_type v ty, + forall STORE: Mem.storev chunk m1 addr v = Some m2, + forall COMPATIBLE: loadv_storev_compatible_type chunk ty = true, + Mem.loadv chunk m2 addr = Some v. +Proof. + intros. + rewrite Mem.loadv_storev_same with (m1:=m1) (v:=v) by assumption. + f_equal. + destruct chunk; destruct ty; try discriminate. + all: destruct v; trivial; try contradiction. + all: unfold Val.load_result, Val.has_type in *. + all: destruct Archi.ptr64; trivial; discriminate. +Qed. + +Lemma subst_args_notin : + forall (rs : regset) dst v args, + ~ In dst args -> + (rs # dst <- v) ## args = rs ## args. +Proof. + induction args; simpl; trivial. + intro NOTIN. + destruct (peq a dst). + { + subst a. + intuition congruence. + } + rewrite Regmap.gso by congruence. + f_equal. + apply IHargs. + intuition congruence. +Qed. + +Lemma add_i_j_adds : forall i j m, + PSet.contains (Regmap.get i (add_i_j i j m)) j = true. +Proof. + intros. + unfold add_i_j. + rewrite Regmap.gss. + auto with pset. +Qed. +Hint Resolve add_i_j_adds: cse3. + +Lemma add_i_j_monotone : forall i j i' j' m, + PSet.contains (Regmap.get i' m) j' = true -> + PSet.contains (Regmap.get i' (add_i_j i j m)) j' = true. +Proof. + intros. + unfold add_i_j. + destruct (peq i i'). + - subst i'. + rewrite Regmap.gss. + destruct (peq j j'). + + subst j'. + apply PSet.gadds. + + eauto with pset. + - rewrite Regmap.gso. + assumption. + congruence. +Qed. + +Hint Resolve add_i_j_monotone: cse3. + +Lemma add_ilist_j_monotone : forall ilist j i' j' m, + PSet.contains (Regmap.get i' m) j' = true -> + PSet.contains (Regmap.get i' (add_ilist_j ilist j m)) j' = true. +Proof. + induction ilist; simpl; intros until m; intro CONTAINS; auto with cse3. +Qed. +Hint Resolve add_ilist_j_monotone: cse3. + +Lemma add_ilist_j_adds : forall ilist j m, + forall i, In i ilist -> + PSet.contains (Regmap.get i (add_ilist_j ilist j m)) j = true. +Proof. + induction ilist; simpl; intros until i; intro IN. + contradiction. + destruct IN as [HEAD | TAIL]; subst; auto with cse3. +Qed. +Hint Resolve add_ilist_j_adds: cse3. + +Definition xlget_kills (eqs : list (eq_id * equation)) (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 := +(fold_left + (fun (a : PSet.t) (p : positive * equation) => + if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a) + eqs m). + +Lemma xlget_kills_monotone : + forall eqs m i j, + PSet.contains (Regmap.get i m) j = true -> + PSet.contains (Regmap.get i (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl; trivial. + intros. + auto with cse3. +Qed. + +Hint Resolve xlget_kills_monotone : cse3. + +Lemma xlget_mem_kills_monotone : + forall eqs m j, + PSet.contains m j = true -> + PSet.contains (xlget_mem_kills eqs m) j = true. +Proof. + induction eqs; simpl; trivial. + intros. + destruct eq_depends_on_mem. + - apply IHeqs. + destruct (peq (fst a) j). + + subst j. apply PSet.gadds. + + rewrite PSet.gaddo by congruence. + trivial. + - auto. +Qed. + +Hint Resolve xlget_mem_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 -> + PSet.contains (Regmap.get lhs (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros until j. + intro HEAD_TAIL. + destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl. + - auto with cse3. + - eapply IHeqs. eassumption. +Qed. +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 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_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 |} -> + 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. + eapply xlget_kills_has_lhs. + apply PTree.elements_correct. + eassumption. +Qed. + +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 |} -> + PSet.contains (eq_kill_reg (context_from_hints hints) lhs) j = true. +Proof. + intros; simpl. + eapply get_kills_has_lhs. + eassumption. +Qed. + +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 |} -> + 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) => + add_i_j (eq_lhs (snd p)) (fst p) + (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills. + eapply xlget_kills_has_arg. + - apply PTree.elements_correct. + eassumption. + - assumption. +Qed. + +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 |} -> + In arg args -> + PSet.contains (eq_kill_reg (context_from_hints hints) arg) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_arg; eassumption. +Qed. + +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 -> + PSet.contains (xlget_mem_kills eqs m) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros. + destruct H. + { subst a. + simpl. + rewrite H0. + apply xlget_mem_kills_monotone. + apply PSet.gadds. + } + eauto. +Qed. + +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 -> + 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). + eapply xlget_kills_has_eq_depends_on_mem. + apply PTree.elements_correct. + eassumption. + trivial. +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 -> + PSet.contains (eq_kill_mem (context_from_hints hints) tt) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_eq_depends_on_mem; eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_eq_depends_on_mem : cse3. + +Definition eq_involves (eq : equation) (i : reg) := + i = (eq_lhs eq) \/ In i (eq_args eq). + +Section SOUNDNESS. + Context {F V : Type}. + Context {genv: Genv.t F V}. + Context {sp : val}. + + Context {ctx : eq_context}. + + Definition sem_rhs (sop : sym_op) (args : list reg) + (rs : regset) (m : mem) (v' : val) := + match sop with + | SOp op => + match eval_operation genv sp op (rs ## args) m with + | Some v => v' = v + | None => False + end + | SLoad chunk addr => + match + match eval_addressing genv sp addr (rs ## args) with + | Some a => Mem.loadv chunk m a + | None => None + end + with + | Some dat => v' = dat + | None => v' = default_notrap_load_value chunk + 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_rel (rel : RELATION.t) (rs : regset) (m : mem) := + forall i eq, + PSet.contains rel i = true -> + eq_catalog ctx i = Some eq -> + sem_eq eq rs m. + + 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 |} -> + 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 |} -> + 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 -> + eq_depends_on_mem eq = true -> + PSet.contains (eq_kill_mem ctx tt) j = true. + + Theorem kill_reg_sound : + forall rel rs m dst v, + (sem_rel rel rs m) -> + (sem_rel (kill_reg (ctx:=ctx) dst rel) (rs#dst <- v) m). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_reg. + 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). + 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. + 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. + } + destruct (peq dst lhs). + { + congruence. + } + rewrite subst_args_notin by assumption. + destruct sop. + - destruct (eval_operation genv sp o rs ## args m) as [ev | ]; trivial. + rewrite Regmap.gso by congruence. + assumption. + - rewrite Regmap.gso by congruence. + assumption. + Qed. + + Hint Resolve kill_reg_sound : cse3. + + Theorem kill_reg_sound2 : + forall rel rs m dst, + (sem_rel rel rs m) -> + (sem_rel (kill_reg (ctx:=ctx) dst rel) rs m). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_reg. + 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). + 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. + Qed. + + Lemma pick_source_sound : + forall (l : list reg), + match pick_source l with + | Some x => In x l + | None => True + end. + Proof. + unfold pick_source. + destruct l; simpl; trivial. + left; trivial. + Qed. + + Hint Resolve pick_source_sound : cse3. + + Theorem forward_move_sound : + forall rel rs m x, + (sem_rel rel rs m) -> + rs # (forward_move (ctx := ctx) rel x) = rs # x. + Proof. + unfold sem_rel, forward_move. + intros until x. + intro REL. + pose proof (pick_source_sound (PSet.elements (PSet.inter rel (eq_moves ctx x)))) as ELEMENT. + destruct (pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x)))). + 2: reflexivity. + 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 | ]. + 2: reflexivity. + destruct (peq x (eq_lhs eq)). + 2: reflexivity. + simpl. + subst x. + rewrite PSet.elements_spec in ELEMENT. + 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]. + reflexivity. + destruct t. + 2: reflexivity. + simpl in REL. + intuition congruence. + Qed. + + Hint Resolve forward_move_sound : cse3. + + Theorem forward_move_l_sound : + forall rel rs m l, + (sem_rel rel rs m) -> + rs ## (forward_move_l (ctx := ctx) rel l) = rs ## l. + Proof. + induction l; simpl; intros; trivial. + erewrite forward_move_sound by eassumption. + intuition congruence. + Qed. + + Hint Resolve forward_move_l_sound : cse3. + + Theorem kill_mem_sound : + forall rel rs m m', + (sem_rel rel rs m) -> + (sem_rel (kill_mem (ctx:=ctx) rel) rs m'). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_mem. + intros until m'. + intros REL i eq. + specialize REL with (i := i) (eq0 := eq). + intros SUBTRACT CATALOG. + rewrite PSet.gsubtract in SUBTRACT. + rewrite andb_true_iff in SUBTRACT. + intuition. + destruct (eq_op eq) 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 (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 negb_true_iff in H0. + rewrite OP in CATALOG. + intuition. + congruence. + Qed. + + Hint Resolve kill_mem_sound : cse3. + + Theorem eq_find_sound: + forall no eq id, + eq_find (ctx := ctx) no eq = Some id -> + eq_catalog ctx id = Some eq. + Proof. + unfold eq_find. + intros. + destruct (eq_find_oracle ctx no eq) as [ id' | ]. + 2: discriminate. + destruct (eq_catalog ctx id') as [eq' |] eqn:CATALOG. + 2: discriminate. + destruct (eq_dec_equation eq eq'). + 2: discriminate. + congruence. + Qed. + + Hint Resolve eq_find_sound : cse3. + + Theorem rhs_find_sound: + forall no sop args rel src rs m, + sem_rel rel rs m -> + rhs_find (ctx := ctx) no sop args rel = Some src -> + sem_rhs sop args rs m (rs # src). + Proof. + unfold rhs_find, sem_rel, sem_eq. + intros until m. + intros REL FIND. + pose proof (pick_source_sound (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel))) as SOURCE. + destruct (pick_source (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel))) as [ src' | ]. + 2: discriminate. + rewrite PSet.elements_spec in SOURCE. + rewrite PSet.ginter in SOURCE. + rewrite andb_true_iff in SOURCE. + 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)). + 2: discriminate. + destruct (eq_dec_args args (eq_args eq)). + 2: discriminate. + simpl in FIND. + intuition congruence. + Qed. + + Hint Resolve rhs_find_sound : cse3. + + Theorem forward_move_rhs_sound : + forall sop args rel rs m v, + (sem_rel rel rs m) -> + (sem_rhs sop args rs m v) -> + (sem_rhs sop (forward_move_l (ctx := ctx) rel args) rs m v). + Proof. + intros until v. + intros REL RHS. + destruct sop; simpl in *. + all: erewrite forward_move_l_sound by eassumption; assumption. + Qed. + + Hint Resolve forward_move_rhs_sound : cse3. + + Lemma arg_not_replaced: + forall (rs : regset) dst v args, + ~ In dst args -> + (rs # dst <- v) ## args = rs ## args. + Proof. + induction args; simpl; trivial. + intuition. + f_equal; trivial. + apply Regmap.gso; congruence. + Qed. + + Lemma sem_rhs_depends_on_args_only: + forall sop args rs dst m v, + sem_rhs sop args rs m v -> + ~ In dst args -> + sem_rhs sop args (rs # dst <- v) m v. + Proof. + unfold sem_rhs. + intros. + rewrite arg_not_replaced by assumption. + assumption. + Qed. + + Lemma replace_sound: + forall no eqno dst sop args rel rs m v, + 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 -> + 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. + clear FIND. + inv CATALOG. + unfold sem_eq. + simpl in *. + rewrite Regmap.gss. + apply sem_rhs_depends_on_args_only; auto. + - rewrite PSet.gaddo in CONTAINS by congruence. + eapply kill_reg_sound; eauto. + Qed. + + Lemma sem_rhs_det: + forall {sop} {args} {rs} {m} {v} {v'}, + sem_rhs sop args rs m v -> + sem_rhs sop args rs m v' -> + v = v'. + Proof. + intros until v'. intro SEMv. + destruct sop; simpl in *. + - destruct eval_operation. + congruence. + contradiction. + - destruct eval_addressing. + + destruct Mem.loadv; congruence. + + congruence. + Qed. + + Theorem oper2_sound: + forall no dst sop args rel rs m v, + sem_rel rel rs m -> + not (In dst args) -> + sem_rhs sop args rs m v -> + sem_rel (oper2 (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. + Proof. + 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. + destruct eq_find. + 2: auto with cse3; fail. + specialize EQ_FIND_SOUND with (id := e). + intuition. + intros i eq CONTAINS. + destruct (peq i e). + { subst i. + rewrite H. + clear H. + intro Z. + inv Z. + unfold sem_eq. + simpl. + rewrite Regmap.gss. + apply sem_rhs_depends_on_args_only; auto. + } + rewrite PSet.gaddo in CONTAINS by congruence. + apply (kill_reg_sound rel rs m dst v REL i eq); auto. + Qed. + + Hint Resolve oper2_sound : cse3. + + Theorem oper1_sound: + forall no dst sop args rel rs m v, + sem_rel rel rs m -> + sem_rhs sop args rs m v -> + sem_rel (oper1 (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. + Proof. + intros. + unfold oper1. + destruct in_dec; auto with cse3. + Qed. + + Hint Resolve oper1_sound : cse3. + + Lemma move_sound : + forall no : node, + forall rel : RELATION.t, + forall src dst : reg, + forall rs m, + sem_rel rel rs m -> + sem_rel (move (ctx:=ctx) no src dst rel) (rs # dst <- (rs # src)) m. + Proof. + unfold move. + intros until m. + intro REL. + pose proof (eq_find_sound no {| eq_lhs := dst; eq_op := SOp Omove; eq_args := src :: nil |}) as EQ_FIND_SOUND. + destruct eq_find. + - intros i eq CONTAINS. + destruct (peq i e). + + subst i. + rewrite (EQ_FIND_SOUND e) by trivial. + intro Z. + inv Z. + unfold sem_eq. + simpl. + destruct (peq src dst). + * subst dst. + reflexivity. + * rewrite Regmap.gss. + rewrite Regmap.gso by congruence. + reflexivity. + + intros. + rewrite PSet.gaddo in CONTAINS by congruence. + apply (kill_reg_sound rel rs m dst (rs # src) REL i); auto. + - apply kill_reg_sound; auto. + Qed. + + Hint Resolve move_sound : cse3. + + Theorem oper_sound: + forall no dst sop args rel rs m v, + sem_rel rel rs m -> + sem_rhs sop args rs m v -> + sem_rel (oper (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. + Proof. + intros until v. + intros REL RHS. + unfold oper. + destruct rhs_find as [src |] eqn:RHS_FIND. + - pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND. + eapply forward_move_rhs_sound in RHS. + 2: eassumption. + rewrite <- (sem_rhs_det SOUND RHS). + apply move_sound; auto. + - apply oper1_sound; auto. + Qed. + + Hint Resolve oper_sound : cse3. + + + Theorem clever_kill_store_sound: + forall chunk addr args a src rel rs m m', + sem_rel rel rs m -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs # src) = Some m' -> + sem_rel (clever_kill_store (ctx:=ctx) chunk addr args src rel) rs m'. + Proof. + unfold clever_kill_store. + intros until m'. intros REL ADDR STORE i eq CONTAINS CATALOG. + autorewrite with pset in CONTAINS. + destruct (PSet.contains rel i) eqn:RELi; simpl in CONTAINS. + 2: discriminate. + rewrite CATALOG in CONTAINS. + unfold sem_rel in REL. + specialize REL with (i := i) (eq0 := eq). + destruct eq; simpl in *. + unfold sem_eq in *. + simpl in *. + destruct eq_op as [op' | chunk' addr']; simpl. + - destruct (op_depends_on_memory op') eqn:DEPENDS. + + erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. + discriminate. + + rewrite op_depends_on_memory_correct with (m2:=m); trivial. + apply REL; auto. + - simpl in REL. + erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. + simpl in CONTAINS. + rewrite negb_true_iff in CONTAINS. + destruct (eval_addressing genv sp addr' rs ## eq_args) as [a'|] eqn:ADDR'. + + 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. + Qed. + + Hint Resolve clever_kill_store_sound : cse3. + + Theorem store2_sound: + forall chunk addr args a src rel rs m m', + sem_rel rel rs m -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs # src) = Some m' -> + sem_rel (store2 (ctx:=ctx) chunk addr args src rel) rs m'. + Proof. + unfold store2. + intros. + destruct (Compopts.optim_CSE3_alias_analysis tt); eauto with cse3. + Qed. + + Hint Resolve store2_sound : cse3. + + Theorem store1_sound: + forall no chunk addr args a src rel tenv rs m m', + sem_rel rel rs m -> + wt_regset tenv rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs#src) = Some m' -> + sem_rel (store1 (ctx:=ctx) no chunk addr args src (tenv src) rel) rs m'. + Proof. + unfold store1. + intros until m'. + intros REL WT ADDR STORE. + assert (sem_rel (store2 (ctx:=ctx) chunk addr args src rel) rs m') as REL' by eauto with cse3. + destruct loadv_storev_compatible_type eqn:COMPATIBLE. + 2: auto; fail. + destruct eq_find as [eq_id | ] eqn:FIND. + 2: auto; fail. + 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. + inv CATALOG. + unfold sem_eq. + simpl. + rewrite ADDR. + rewrite loadv_storev_really_same with (m1:=m) (v:=rs#src) (ty:=(tenv src)); trivial. + } + unfold sem_rel in REL'. + rewrite PSet.gaddo in CONTAINS by congruence. + eauto. + Qed. + + Hint Resolve store1_sound : cse3. + + Theorem store_sound: + forall no chunk addr args a src rel tenv rs m m', + sem_rel rel rs m -> + wt_regset tenv rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs#src) = Some m' -> + sem_rel (store (ctx:=ctx) no chunk addr args src (tenv src) rel) rs m'. + Proof. + unfold store. + intros until m'. + intros REL WT ADDR STORE. + rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial. + rewrite <- forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. + apply store1_sound with (a := a) (m := m); trivial. + rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. + assumption. + Qed. + + Hint Resolve store_sound : cse3. + + Section INDUCTIVENESS. + Variable fn : RTL.function. + Variable tenv : typing_env. + Variable inv: invariants. + + Definition is_inductive_step (pc pc' : node) := + forall instr, + 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)). + + Definition is_inductive_allstep := + forall pc pc', is_inductive_step pc pc'. + + Lemma checked_is_inductive_allstep: + (check_inductiveness (ctx:=ctx) fn tenv inv) = true -> + is_inductive_allstep. + Proof. + unfold check_inductiveness, is_inductive_allstep, is_inductive_step. + rewrite andb_true_iff. + rewrite PTree_Properties.for_all_correct. + intros (ENTRYPOINT & ALL). + intros until instr. + intros INSTR IN_SUCC. + specialize ALL with (x := pc) (a := instr). + 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. + Qed. + + Lemma checked_is_inductive_entry: + (check_inductiveness (ctx:=ctx) fn tenv inv) = true -> + inv # (fn_entrypoint fn) = Some RELATION.top. + Proof. + unfold check_inductiveness, is_inductive_allstep, is_inductive_step. + rewrite andb_true_iff. + intros (ENTRYPOINT & ALL). + apply RB.beq_correct in ENTRYPOINT. + unfold RB.eq, RELATION.eq in ENTRYPOINT. + destruct (inv # (fn_entrypoint fn)) as [rel | ]. + 2: contradiction. + f_equal. + symmetry. + assumption. + Qed. + 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 new file mode 100644 index 00000000..19fb20be --- /dev/null +++ b/backend/CSE3proof.v @@ -0,0 +1,875 @@ +(* +Replace available expressions by the register containing their value. + +Proofs. + +David Monniaux, CNRS, VERIMAG + *) + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE3 CSE3analysis CSE3analysisproof. +Require Import RTLtyping. + + +Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transf_program p = OK tp -> match_prog p tp. +Proof. + intros. eapply match_transform_partial_program; eauto. +Qed. + +Section PRESERVATION. + +Variables prog tprog: program. +Hypothesis TRANSF: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Section SOUNDNESS. +Variable sp : val. +Variable ctx : eq_context. + +Definition sem_rel_b (rel : RB.t) (rs : regset) (m : mem) := + match rel with + | None => False + | Some rel => sem_rel (ctx:=ctx) (genv:=ge) (sp:=sp) rel rs m + end. + +Lemma forward_move_b_sound : + forall rel rs m x, + (sem_rel_b rel rs m) -> + rs # (forward_move_b (ctx := ctx) rel x) = rs # x. +Proof. + destruct rel as [rel | ]; simpl; intros. + 2: contradiction. + eapply forward_move_sound; eauto. + Qed. + + Lemma forward_move_l_b_sound : + forall rel rs m x, + (sem_rel_b rel rs m) -> + rs ## (forward_move_l_b (ctx := ctx) rel x) = rs ## x. + Proof. + destruct rel as [rel | ]; simpl; intros. + 2: contradiction. + eapply forward_move_l_sound; eauto. + Qed. + + Definition fmap_sem (fmap : PMap.t RB.t) (pc : node) (rs : regset) (m : mem) := + sem_rel_b (PMap.get pc fmap) rs m. + + Lemma subst_arg_ok: + forall invariants, + forall pc, + forall rs, + forall m, + forall arg, + forall (SEM : fmap_sem invariants pc rs m), + rs # (subst_arg (ctx:=ctx) invariants pc arg) = rs # arg. + Proof. + intros. + apply forward_move_b_sound with (m:=m). + assumption. + Qed. + + Lemma subst_args_ok: + forall invariants, + forall pc, + forall rs, + forall m, + forall args, + forall (SEM : fmap_sem invariants pc rs m), + rs ## (subst_args (ctx:=ctx) invariants pc args) = rs ## args. + Proof. + intros. + apply forward_move_l_b_sound with (m:=m). + assumption. + Qed. +End SOUNDNESS. + +Lemma functions_translated: + forall (v: val) (f: RTL.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. +Proof. + apply (Genv.find_funct_transf_partial TRANSF). +Qed. + +Lemma function_ptr_translated: + forall (b: block) (f: RTL.fundef), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. +Proof. + apply (Genv.find_funct_ptr_transf_partial TRANSF). +Qed. + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof. + apply (Genv.find_symbol_match TRANSF). +Qed. + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof. + apply (Genv.senv_match TRANSF). +Qed. + +Lemma sig_preserved: + forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f. +Proof. + destruct f; simpl; intros. + - monadInv H. + monadInv EQ. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ1. + reflexivity. + - monadInv H. + reflexivity. +Qed. + +Lemma stacksize_preserved: + forall f tf, transf_function f = OK tf -> fn_stacksize tf = fn_stacksize f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma params_preserved: + forall f tf, transf_function f = OK tf -> fn_params tf = fn_params f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma entrypoint_preserved: + forall f tf, transf_function f = OK tf -> fn_entrypoint tf = fn_entrypoint f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma sig_preserved2: + forall f tf, transf_function f = OK tf -> fn_sig tf = fn_sig f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma transf_function_is_typable: + forall f tf, transf_function f = OK tf -> + exists tenv, type_function f = OK tenv. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + exists x. + assumption. +Qed. +Lemma transf_function_invariants_inductive: + forall f tf tenv, transf_function f = OK tf -> + type_function f = OK tenv -> + check_inductiveness (ctx:=(context_from_hints (snd (preanalysis tenv f)))) + f tenv (fst (preanalysis tenv f)) = true. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + replace x with tenv in * by congruence. + clear x. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness; trivial; discriminate. +Qed. + +Lemma find_function_translated: + forall ros rs fd, + find_function ge ros rs = Some fd -> + exists tfd, + find_function tge ros rs = Some tfd /\ transf_fundef fd = OK tfd. +Proof. + unfold find_function; intros. destruct ros as [r|id]. + eapply functions_translated; eauto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence. + eapply function_ptr_translated; eauto. +Qed. + +Check sem_rel_b. +Inductive match_stackframes: list stackframe -> list stackframe -> signature -> Prop := + | match_stackframes_nil: forall sg, + sg.(sig_res) = Tint -> + match_stackframes nil nil sg + | match_stackframes_cons: + forall res f sp pc rs s tf ts sg tenv + (STACKS: match_stackframes s ts (fn_sig tf)) + (FUN: transf_function f = OK tf) + (WTF: type_function f = OK tenv) + (WTRS: wt_regset tenv rs) + (WTRES: tenv res = proj_sig_res sg) + (REL: forall m vres, + sem_rel_b sp (context_from_hints (snd (preanalysis tenv f))) + ((fst (preanalysis tenv f))#pc) (rs#res <- vres) m), + + match_stackframes + (Stackframe res f sp pc rs :: s) + (Stackframe res tf sp pc rs :: ts) + sg. + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall s f sp pc rs m ts tf tenv + (STACKS: match_stackframes s ts (fn_sig tf)) + (FUN: transf_function f = OK tf) + (WTF: type_function f = OK tenv) + (WTRS: wt_regset tenv rs) + (REL: sem_rel_b sp (context_from_hints (snd (preanalysis tenv f))) ((fst (preanalysis tenv f))#pc) rs m), + match_states (State s f sp pc rs m) + (State ts tf sp pc rs m) + | match_states_call: + forall s f args m ts tf + (STACKS: match_stackframes s ts (funsig tf)) + (FUN: transf_fundef f = OK tf) + (WTARGS: Val.has_type_list args (sig_args (funsig tf))), + match_states (Callstate s f args m) + (Callstate ts tf args m) + | match_states_return: + forall s res m ts sg + (STACKS: match_stackframes s ts sg) + (WTRES: Val.has_type res (proj_sig_res sg)), + match_states (Returnstate s res m) + (Returnstate ts res m). + +Lemma match_stackframes_change_sig: + forall s ts sg sg', + match_stackframes s ts sg -> + sg'.(sig_res) = sg.(sig_res) -> + match_stackframes s ts sg'. +Proof. + intros. inv H. + constructor. congruence. + econstructor; eauto. + unfold proj_sig_res in *. rewrite H0; auto. +Qed. + +Lemma transf_function_at: + forall f tf pc tenv instr + (TF : transf_function f = OK tf) + (TYPE : type_function f = OK tenv) + (PC : (fn_code f) ! pc = Some instr), + (fn_code tf) ! pc = Some (transf_instr + (ctx := (context_from_hints (snd (preanalysis tenv f)))) + (fst (preanalysis tenv f)) + pc instr). +Proof. + intros. + unfold transf_function in TF. + monadInv TF. + replace x with tenv in * by congruence. + clear EQ. + destruct (preanalysis tenv f) as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + simpl. + rewrite PTree.gmap. + rewrite PC. + reflexivity. +Qed. + +Ltac TR_AT := erewrite transf_function_at by eauto. + +Hint Resolve wt_instrs type_function_correct : wt. + +Lemma wt_undef : + forall tenv rs dst, + wt_regset tenv rs -> + wt_regset tenv rs # dst <- Vundef. +Proof. + unfold wt_regset. + intros. + destruct (peq r dst). + { subst dst. + rewrite Regmap.gss. + constructor. + } + rewrite Regmap.gso by congruence. + auto. +Qed. + +Lemma rel_ge: + forall inv inv' + (GE : RELATION.ge inv' inv) + ctx sp rs m + (REL: sem_rel (genv:=ge) (sp:=sp) (ctx:=ctx) inv rs m), + sem_rel (genv:=ge) (sp:=sp) (ctx:=ctx) inv' rs m. +Proof. + unfold sem_rel, RELATION.ge. + intros. + apply (REL i); trivial. + eapply HashedSet.PSet.is_subset_spec1; eassumption. +Qed. + +Hint Resolve rel_ge : cse3. + +Lemma sem_rhs_sop : + forall sp op rs args m v, + eval_operation ge sp op rs ## args m = Some v -> + sem_rhs (genv:=ge) (sp:=sp) (SOp op) args rs m v. +Proof. + intros. simpl. + rewrite H. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sop : cse3. + +Lemma sem_rhs_sload : + forall sp chunk addr rs args m a v, + eval_addressing ge sp addr rs ## args = Some a -> + Mem.loadv chunk m a = Some v -> + sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m v. +Proof. + intros. simpl. + rewrite H. rewrite H0. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sload : cse3. + +Lemma sem_rhs_sload_notrap1 : + forall sp chunk addr rs args m, + eval_addressing ge sp addr rs ## args = None -> + sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m Vundef. +Proof. + intros. simpl. + rewrite H. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sload_notrap1 : cse3. + +Lemma sem_rhs_sload_notrap2 : + forall sp chunk addr rs args m a, + eval_addressing ge sp addr rs ## args = Some a -> + Mem.loadv chunk m a = None -> + sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m Vundef. +Proof. + intros. simpl. + rewrite H. rewrite H0. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sload_notrap2 : cse3. + +Lemma sem_rel_top: + forall ctx sp rs m, sem_rel (genv:=ge) (sp:=sp) (ctx:=ctx) RELATION.top rs m. +Proof. + unfold sem_rel, RELATION.top. + intros. + rewrite HashedSet.PSet.gempty in *. + discriminate. +Qed. + +Hint Resolve sem_rel_top : cse3. + +Lemma sem_rel_b_top: + forall ctx sp rs m, sem_rel_b sp ctx (Some RELATION.top) rs m. +Proof. + intros. simpl. + apply sem_rel_top. +Qed. + +Hint Resolve sem_rel_b_top : cse3. + +Ltac IND_STEP := + match goal with + REW: (fn_code ?fn) ! ?mpc = Some ?minstr + |- + sem_rel_b ?sp (context_from_hints (snd (preanalysis ?tenv ?fn))) ((fst (preanalysis ?tenv ?fn)) # ?mpc') ?rs ?m => + assert (is_inductive_allstep (ctx:= (context_from_hints (snd (preanalysis tenv fn)))) fn tenv (fst (preanalysis tenv fn))) 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:=mpc) (pc':=mpc') (instr:=minstr); + simpl in IND; + rewrite REW in IND; + simpl in IND; + destruct ((fst (preanalysis tenv fn)) # mpc') as [zinv' | ]; + destruct ((fst (preanalysis tenv fn)) # mpc) as [zinv | ]; + simpl in *; + intuition; + eapply rel_ge; eauto with cse3; + idtac mpc mpc' fn minstr + end. + +Lemma if_same : forall {T : Type} (b : bool) (x : T), + (if b then x else x) = x. +Proof. + destruct b; trivial. +Qed. + +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. + - (* Inop *) + exists (State ts tf sp pc' rs m). split. + + apply exec_Inop; auto. + TR_AT. reflexivity. + + econstructor; eauto. + IND_STEP. + - (* 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'. + assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iop op args res pc'))) by reflexivity. + unfold transf_instr, find_op_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct (if is_trivial_op op + then None + else + rhs_find pc (SOp op) + (subst_args (fst (preanalysis tenv f)) pc args) t) eqn:FIND. + ** destruct (is_trivial_op op). discriminate. + apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iop with (op := op) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)). + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_operation_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iop with (op := op) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)). + TR_AT. + { subst instr'. + rewrite if_same in H1. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_operation_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * eapply wt_exec_Iop with (f:=f); try eassumption. + eauto with wt. + * IND_STEP. + apply oper_sound; eauto with cse3. + + - (* 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'. + assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity. + unfold transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. (* ADDR *) + rewrite H1 in FIND_SOUND. (* LOAD *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload with (trap := trap) (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iload with (chunk := chunk) (trap := trap) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * eapply wt_exec_Iload with (f:=f); try eassumption. + eauto with wt. + * IND_STEP. + apply oper_sound; eauto with cse3. + + - (* Iload notrap1 *) + exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. (* ADDR *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * apply wt_undef; assumption. + * IND_STEP. + apply oper_sound; eauto with cse3. + + - (* Iload notrap2 *) + exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. (* ADDR *) + rewrite H1 in FIND_SOUND. (* LOAD *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload_notrap2 with (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * apply wt_undef; assumption. + * IND_STEP. + apply oper_sound; eauto with cse3. + + - (* Istore *) + exists (State ts tf sp pc' rs m'). split. + + eapply exec_Istore 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. + rewrite eval_addressing_preserved with (ge1 := ge) by exact symbols_preserved. + assumption. + + econstructor; eauto. + IND_STEP. + apply store_sound with (a0:=a) (m0:=m); eauto with cse3. + + - (* Icall *) + destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. + econstructor. split. + + eapply exec_Icall; try eassumption. + * TR_AT. reflexivity. + * apply sig_preserved; auto. + + rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + assert (wt_instr f tenv (Icall (funsig fd) ros args res pc')) as WTcall by eauto with wt. + inv WTcall. + constructor; trivial. + * 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. + * rewrite sig_preserved with (f:=fd) by trivial. + rewrite <- H7. + apply wt_regset_list; auto. + - (* Itailcall *) + destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. + econstructor. split. + + eapply exec_Itailcall; try eassumption. + * TR_AT. reflexivity. + * apply sig_preserved; auto. + * rewrite stacksize_preserved with (f:=f); eauto. + + rewrite subst_args_ok with (m:=m) (sp := (Vptr stk Ptrofs.zero)) by trivial. + assert (wt_instr f tenv (Itailcall (funsig fd) ros args)) as WTcall by eauto with wt. + inv WTcall. + constructor; trivial. + * rewrite sig_preserved with (f:=fd) by trivial. + inv STACKS. + ** econstructor; eauto. + rewrite H7. + rewrite <- sig_preserved2 with (tf:=tf) by trivial. + assumption. + ** econstructor; eauto. + unfold proj_sig_res in *. + rewrite H7. + rewrite WTRES. + rewrite sig_preserved2 with (f:=f) by trivial. + reflexivity. + * rewrite sig_preserved with (f:=fd) by trivial. + rewrite <- H6. + apply wt_regset_list; auto. + - (* Ibuiltin *) + econstructor. split. + + eapply exec_Ibuiltin; try eassumption. + * TR_AT. reflexivity. + * eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + * eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + econstructor; eauto. + * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt. + * IND_STEP. + - (* 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. + + - (* Ijumptable *) + econstructor. split. + + eapply exec_Ijumptable with (arg := (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc arg)); try eassumption. + * TR_AT. reflexivity. + * 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. + + - (* Ireturn *) + destruct or as [arg | ]. + -- econstructor. split. + + eapply exec_Ireturn with (or := Some (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc arg)). + * TR_AT. reflexivity. + * rewrite stacksize_preserved with (f:=f); eauto. + + simpl. + rewrite subst_arg_ok with (sp:=(Vptr stk Ptrofs.zero)) (m:=m) by trivial. + econstructor; eauto. + apply type_function_correct in WTF. + apply wt_instrs with (pc:=pc) (instr:=(Ireturn (Some arg))) in WTF. + 2: assumption. + inv WTF. + rewrite sig_preserved2 with (f:=f) by assumption. + rewrite <- H3. + unfold wt_regset in WTRS. + apply WTRS. + -- econstructor. split. + + eapply exec_Ireturn; try eassumption. + * TR_AT; reflexivity. + * rewrite stacksize_preserved with (f:=f); eauto. + + econstructor; eauto. + simpl. trivial. + - (* Callstate internal *) + monadInv FUN. + rename x into tf. + destruct (transf_function_is_typable f tf EQ) as [tenv TENV]. + econstructor; split. + + apply exec_function_internal. + rewrite stacksize_preserved with (f:=f); eauto. + + rewrite params_preserved with (tf:=tf) (f:=f) by assumption. + rewrite entrypoint_preserved with (tf:=tf) (f:=f) by assumption. + econstructor; eauto. + * apply type_function_correct in TENV. + inv TENV. + simpl in WTARGS. + rewrite sig_preserved2 with (f:=f) in WTARGS by assumption. + 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. + + - (* external *) + simpl in FUN. + inv FUN. + econstructor. split. + + eapply exec_function_external. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + econstructor; eauto. + eapply external_call_well_typed; eauto. + - (* return *) + inv STACKS. + econstructor. split. + + eapply exec_return. + + econstructor; eauto. + apply wt_regset_assign; trivial. + rewrite WTRES0. + exact WTRES. +Qed. + +Lemma transf_initial_states: + forall S1, RTL.initial_state prog S1 -> + exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. +Proof. + intros. inversion H. + exploit function_ptr_translated; eauto. + intros (tf & A & B). + exists (Callstate nil tf nil m0); split. + - econstructor; eauto. + + eapply (Genv.init_mem_match TRANSF); eauto. + + replace (prog_main tprog) with (prog_main prog). + rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main; eauto. + + rewrite <- H3. eapply sig_preserved; eauto. + - constructor; trivial. + + constructor. rewrite sig_preserved with (f:=f) by assumption. + rewrite H3. reflexivity. + + rewrite sig_preserved with (f:=f) by assumption. + rewrite H3. reflexivity. +Qed. + +Lemma transf_final_states: + forall S1 S2 r, match_states S1 S2 -> final_state S1 r -> final_state S2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). +Proof. + eapply forward_simulation_step. + - apply senv_preserved. + - eexact transf_initial_states. + - eexact transf_final_states. + - intros. eapply step_simulation; eauto. +Qed. + +End PRESERVATION. diff --git a/backend/FirstNop.v b/backend/FirstNop.v new file mode 100644 index 00000000..f7e5261e --- /dev/null +++ b/backend/FirstNop.v @@ -0,0 +1,18 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. + +Definition transf_function (f: function) : function := + let start_pc := Pos.succ (max_pc_function f) in + {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := PTree.set start_pc (Inop f.(fn_entrypoint)) f.(fn_code); + fn_entrypoint := start_pc |}. + +Definition transf_fundef (fd: fundef) : fundef := + AST.transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. + diff --git a/backend/FirstNopproof.v b/backend/FirstNopproof.v new file mode 100644 index 00000000..5d9a7d6a --- /dev/null +++ b/backend/FirstNopproof.v @@ -0,0 +1,274 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import FirstNop. +Require Import Lia. + +Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. eapply match_transform_program; eauto. +Qed. + +Section PRESERVATION. + +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transf_fundef f). +Proof (Genv.find_funct_transf TRANSL). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + Genv.find_funct_ptr tge v = Some (transf_fundef f). +Proof (Genv.find_funct_ptr_transf TRANSL). + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof (Genv.find_symbol_transf TRANSL). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf TRANSL). + +Lemma sig_preserved: + forall f, funsig (transf_fundef f) = funsig f. +Proof. + destruct f; reflexivity. +Qed. + +Lemma find_function_translated: + forall ros rs fd, + find_function ge ros rs = Some fd -> + find_function tge ros rs = Some (transf_fundef fd). +Proof. + unfold find_function; intros. destruct ros as [r|id]. + eapply functions_translated; eauto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence. + eapply function_ptr_translated; eauto. +Qed. + +Lemma transf_function_at: + forall f pc i, + f.(fn_code)!pc = Some i -> + (transf_function f).(fn_code)!pc = Some i. +Proof. + intros until i. intro Hcode. + unfold transf_function; simpl. + destruct (peq pc (Pos.succ (max_pc_function f))) as [EQ | NEQ]. + { assert (pc <= (max_pc_function f))%positive as LE by (eapply max_pc_function_sound; eassumption). + subst pc. + lia. + } + rewrite PTree.gso by congruence. + assumption. +Qed. + +Hint Resolve transf_function_at : firstnop. + +Ltac TR_AT := + match goal with + | [ A: (fn_code _)!_ = Some _ |- _ ] => + generalize (transf_function_at _ _ _ A); intros + end. + + +Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := +| match_frames_intro: forall res f sp pc rs, + match_frames (Stackframe res f sp pc rs) + (Stackframe res (transf_function f) sp pc rs). + +Inductive match_states: RTL.state -> RTL.state -> Prop := + | match_regular_states: forall stk f sp pc rs m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (State stk f sp pc rs m) + (State stk' (transf_function f) sp pc rs m) + | match_callstates: forall stk f args m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Callstate stk f args m) + (Callstate stk' (transf_fundef f) args m) + | match_returnstates: forall stk v m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Returnstate stk v m) + (Returnstate stk' v m). + +(* +Lemma match_pc_refl : forall f pc, match_pc f pc pc. +Proof. + unfold match_pc. + left. + trivial. +Qed. + +Hint Resolve match_pc_refl : firstnop. + +Lemma initial_jump: + forall f, + (fn_code (transf_function f)) ! (Pos.succ (max_pc_function f)) = + Some (Inop (fn_entrypoint f)). +Proof. + intros. unfold transf_function. simpl. + apply PTree.gss. +Qed. + +Hint Resolve initial_jump : firstnop. + *) + +Lemma match_pc_same : + forall f pc i, + PTree.get pc (fn_code f) = Some i -> + PTree.get pc (fn_code (transf_function f)) = Some i. +Proof. + intros. + unfold transf_function. simpl. + rewrite <- H. + apply PTree.gso. + pose proof (max_pc_function_sound f pc i H) as LE. + unfold Ple in LE. + lia. +Qed. + +Hint Resolve match_pc_same : firstnop. + + +Definition measure (S: RTL.state) : nat := + match S with + | State _ _ _ _ _ _ => 0%nat + | Callstate _ _ _ _ => 1%nat + | Returnstate _ _ _ => 0%nat + end. + +Lemma step_simulation: + forall S1 t S2, + step ge S1 t S2 -> + forall S1' (MS: match_states S1 S1'), + (exists S2', plus step tge S1' t S2' /\ match_states S2 S2') + \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. +Proof. + induction 1; intros; inv MS. + - left. econstructor. split. + + eapply plus_one. eapply exec_Inop; eauto with firstnop. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iop with (v:=v); eauto with firstnop. + rewrite <- H0. + apply eval_operation_preserved. + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop. + rewrite <- H0. + apply eval_addressing_preserved. + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iload_notrap1; eauto with firstnop. + rewrite <- H0. + apply eval_addressing_preserved. + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iload_notrap2; eauto with firstnop. + rewrite <- H0. + apply eval_addressing_preserved. + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Istore; eauto with firstnop. + rewrite <- H0. + apply eval_addressing_preserved. + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Icall. + apply match_pc_same. exact H. + apply find_function_translated. + exact H0. + apply sig_preserved. + + constructor. + constructor; auto. + constructor. + - left. econstructor. split. + + eapply plus_one. eapply exec_Itailcall. + apply match_pc_same. exact H. + apply find_function_translated. + exact H0. + apply sig_preserved. + unfold transf_function; simpl. + eassumption. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Ibuiltin; eauto with firstnop. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Icond; eauto with firstnop. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Ijumptable; eauto with firstnop. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Ireturn; eauto with firstnop. + + constructor; auto. + - left. econstructor. split. + + eapply plus_two. + * eapply exec_function_internal; eauto with firstnop. + * eapply exec_Inop. + unfold transf_function; simpl. + rewrite PTree.gss. + reflexivity. + * auto. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_function_external; eauto with firstnop. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor; auto. + - left. + inv STACKS. inv H1. + econstructor; split. + + eapply plus_one. eapply exec_return; eauto. + + constructor; auto. +Qed. + +Lemma transf_initial_states: + forall S1, RTL.initial_state prog S1 -> + exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. +Proof. + intros. inv H. econstructor; split. + econstructor. + eapply (Genv.init_mem_transf TRANSL); eauto. + rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto. + eapply function_ptr_translated; eauto. + rewrite <- H3; apply sig_preserved. + constructor. constructor. +Qed. + +Lemma transf_final_states: + forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). +Proof. + eapply forward_simulation_star. + apply senv_preserved. + eexact transf_initial_states. + eexact transf_final_states. + exact step_simulation. +Qed. + +End PRESERVATION. |