diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 08:19:34 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 08:19:34 +0100 |
commit | 47090bb8ddd6edfeef8552259dc738f47545299b (patch) | |
tree | 2fcb80fb438949c4babf4b7622462bdcd442441a | |
parent | 0d471625d7613a72c0bb8519e0427f971b53b35f (diff) | |
parent | e08273dcd62dca09c401fb80517652a657028ef9 (diff) | |
download | compcert-kvx-47090bb8ddd6edfeef8552259dc738f47545299b.tar.gz compcert-kvx-47090bb8ddd6edfeef8552259dc738f47545299b.zip |
Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge
-rw-r--r-- | Makefile | 1 | ||||
-rw-r--r-- | backend/CSE2.v | 506 | ||||
-rw-r--r-- | backend/CSE2proof.v | 1660 | ||||
-rwxr-xr-x | config_rv32.sh | 1 | ||||
-rwxr-xr-x | config_simple.sh | 6 | ||||
-rw-r--r-- | driver/Clflags.ml | 1 | ||||
-rw-r--r-- | driver/Compiler.v | 27 | ||||
-rw-r--r-- | driver/Compopts.v | 3 | ||||
-rw-r--r-- | driver/Driver.ml | 8 | ||||
-rw-r--r-- | extraction/extraction.v | 2 | ||||
-rw-r--r-- | test/monniaux/cse2/loopaccess.c | 7 | ||||
-rw-r--r-- | test/monniaux/cse2/loopinvariant.c | 7 | ||||
-rw-r--r-- | test/monniaux/cse2/loopload.c | 5 |
13 files changed, 2223 insertions, 11 deletions
@@ -86,6 +86,7 @@ BACKEND=\ ValueDomain.v ValueAOp.v ValueAnalysis.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ + CSE2.v CSE2proof.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ diff --git a/backend/CSE2.v b/backend/CSE2.v new file mode 100644 index 00000000..38a46c1b --- /dev/null +++ b/backend/CSE2.v @@ -0,0 +1,506 @@ +(* +Replace available expressions by the register containing their value. + +David Monniaux, CNRS, VERIMAG + *) + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +(* Static analysis *) + +Inductive sym_val : Type := +| SMove (src : reg) +| SOp (op : operation) (args : list reg) +| SLoad (chunk : memory_chunk) (addr : addressing) (args : list reg). + +Definition eq_args (x y : list reg) : { x = y } + { x <> y } := + list_eq_dec peq x y. + +Definition eq_sym_val : forall x y : sym_val, + {x = y} + { x <> y }. +Proof. + generalize eq_operation. + generalize eq_args. + generalize peq. + generalize eq_addressing. + generalize chunk_eq. + decide equality. +Defined. + +Module RELATION. + +Definition t := (PTree.t sym_val). +Definition eq (r1 r2 : t) := + forall x, (PTree.get x r1) = (PTree.get x r2). + +Definition top : t := PTree.empty sym_val. + +Lemma eq_refl: forall x, eq x x. +Proof. + unfold eq. + intros; reflexivity. +Qed. + +Lemma eq_sym: forall x y, eq x y -> eq y x. +Proof. + unfold eq. + intros; eauto. +Qed. + +Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. +Proof. + unfold eq. + intros; congruence. +Qed. + +Definition sym_val_beq (x y : sym_val) := + if eq_sym_val x y then true else false. + +Definition beq (r1 r2 : t) := PTree.beq sym_val_beq r1 r2. + +Lemma beq_correct: forall r1 r2, beq r1 r2 = true -> eq r1 r2. +Proof. + unfold beq, eq. intros r1 r2 EQ x. + pose proof (PTree.beq_correct sym_val_beq r1 r2) as CORRECT. + destruct CORRECT as [CORRECTF CORRECTB]. + pose proof (CORRECTF EQ x) as EQx. + clear CORRECTF CORRECTB EQ. + unfold sym_val_beq in *. + destruct (r1 ! x) as [R1x | ] in *; + destruct (r2 ! x) as [R2x | ] in *; + trivial; try contradiction. + destruct (eq_sym_val R1x R2x) in *; congruence. +Qed. + +Definition ge (r1 r2 : t) := + forall x, + match PTree.get x r1 with + | None => True + | Some v => (PTree.get x r2) = Some v + end. + +Lemma ge_refl: forall r1 r2, eq r1 r2 -> ge r1 r2. +Proof. + unfold eq, ge. + intros r1 r2 EQ x. + pose proof (EQ x) as EQx. + clear EQ. + destruct (r1 ! x). + - congruence. + - trivial. +Qed. + +Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. +Proof. + unfold ge. + intros r1 r2 r3 GE12 GE23 x. + pose proof (GE12 x) as GE12x; clear GE12. + pose proof (GE23 x) as GE23x; clear GE23. + destruct (r1 ! x); trivial. + destruct (r2 ! x); congruence. +Qed. + +Definition lub (r1 r2 : t) := + PTree.combine + (fun ov1 ov2 => + match ov1, ov2 with + | (Some v1), (Some v2) => + if eq_sym_val v1 v2 + then ov1 + else None + | None, _ + | _, None => None + end) + r1 r2. + +Lemma ge_lub_left: forall x y, ge (lub x y) x. +Proof. + unfold ge, lub. + intros r1 r2 x. + rewrite PTree.gcombine by reflexivity. + destruct (_ ! _); trivial. + destruct (_ ! _); trivial. + destruct (eq_sym_val _ _); trivial. +Qed. + +Lemma ge_lub_right: forall x y, ge (lub x y) y. +Proof. + unfold ge, lub. + intros r1 r2 x. + rewrite PTree.gcombine by reflexivity. + destruct (_ ! _); trivial. + destruct (_ ! _); trivial. + destruct (eq_sym_val _ _); trivial. + congruence. +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). + +Definition kill_sym_val (dst : reg) (sv : sym_val) := + match sv with + | SMove src => if peq dst src then true else false + | SOp op args => List.existsb (peq dst) args + | SLoad chunk addr args => List.existsb (peq dst) args + end. + +Definition kill_reg (dst : reg) (rel : RELATION.t) := + PTree.filter1 (fun x => negb (kill_sym_val dst x)) + (PTree.remove dst rel). + +Definition kill_sym_val_mem (sv: sym_val) := + match sv with + | SMove _ => false + | SOp op _ => op_depends_on_memory op + | SLoad _ _ _ => true + end. + +Definition kill_mem (rel : RELATION.t) := + PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel. + + +Definition forward_move (rel : RELATION.t) (x : reg) : reg := + match rel ! x with + | Some (SMove org) => org + | _ => x + end. + +Definition move (src dst : reg) (rel : RELATION.t) := + PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel). + +Definition find_op_fold op args (already : option reg) x sv := + match already with + | Some found => already + | None => + match sv with + | (SOp op' args') => + if (eq_operation op op') && (eq_args args args') + then Some x + else None + | _ => None + end + end. + +Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) := + PTree.fold (find_op_fold op args) rel None. + +Definition find_load_fold chunk addr args (already : option reg) x sv := + match already with + | Some found => already + | None => + match sv with + | (SLoad chunk' addr' args') => + if (chunk_eq chunk chunk') && + (eq_addressing addr addr') && + (eq_args args args') + then Some x + else None + | _ => None + end + end. + +Definition find_load (rel : RELATION.t) (chunk : memory_chunk) (addr : addressing) (args : list reg) := + PTree.fold (find_load_fold chunk addr args) rel None. + +Definition oper2 (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + let rel' := kill_reg dst rel in + PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'. + +Definition oper1 (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + if List.in_dec peq dst args + then kill_reg dst rel + else oper2 op dst args rel. + +Definition oper (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + match find_op rel op (List.map (forward_move rel) args) with + | Some r => move r dst rel + | None => oper1 op dst args rel + end. + +Definition gen_oper (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + match op, args with + | Omove, src::nil => move src dst rel + | _, _ => oper op dst args rel + end. + +Definition load2 (chunk: memory_chunk) (addr : addressing) + (dst : reg) (args : list reg) (rel : RELATION.t) := + let rel' := kill_reg dst rel in + PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) rel'. + +Definition load1 (chunk: memory_chunk) (addr : addressing) + (dst : reg) (args : list reg) (rel : RELATION.t) := + if List.in_dec peq dst args + then kill_reg dst rel + else load2 chunk addr dst args rel. + +Definition load (chunk: memory_chunk) (addr : addressing) + (dst : reg) (args : list reg) (rel : RELATION.t) := + match find_load rel chunk addr (List.map (forward_move rel) args) with + | Some r => move r dst rel + | None => load1 chunk addr dst args rel + end. + +(* NO LONGER NEEDED +Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop := + match l with + | nil => True + | (r,sv)::tail => (tr ! r) = Some sv /\ list_represents tail tr + end. + +Lemma elements_represent : + forall { X : Type }, + forall tr : (PTree.t X), + (list_represents (PTree.elements tr) tr). +Proof. + intros. + generalize (PTree.elements_complete tr). + generalize (PTree.elements tr). + induction l; simpl; trivial. + intro COMPLETE. + destruct a as [ r sv ]. + split. + { + apply COMPLETE. + left; reflexivity. + } + apply IHl; auto. +Qed. +*) + +Definition apply_instr instr (rel : RELATION.t) : RB.t := + match instr with + | Inop _ + | Icond _ _ _ _ + | Ijumptable _ _ => Some rel + | Istore _ _ _ _ _ => Some (kill_mem rel) + | Iop op args dst _ => Some (gen_oper op dst args rel) + | Iload trap chunk addr args dst _ => Some (load chunk addr dst 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. + +Definition apply_instr' 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 instr x + end + end. + +Definition forward_map (f : RTL.function) := DS.fixpoint + (RTL.fn_code f) RTL.successors_instr + (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). + +Definition forward_move_b (rb : RB.t) (x : reg) := + match rb with + | None => x + | Some rel => forward_move rel x + end. + +Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg := + match fmap with + | None => x + | Some inv => forward_move_b (PMap.get pc inv) x + end. + +Definition subst_args fmap pc := List.map (subst_arg fmap pc). + +(* Transform *) +Definition find_op_in_fmap fmap pc op args := + match fmap with + | None => None + | Some map => + match PMap.get pc map with + | Some rel => find_op rel op args + | None => None + end + end. + +Definition find_load_in_fmap fmap pc chunk addr args := + match fmap with + | None => None + | Some map => + match PMap.get pc map with + | Some rel => find_load rel chunk addr args + | None => None + end + end. + +Definition transf_instr (fmap : option (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 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. + +Definition transf_function (f: function) : function := + {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := PTree.map (transf_instr (forward_map f)) f.(fn_code); + fn_entrypoint := f.(fn_entrypoint) |}. + + +Definition transf_fundef (fd: fundef) : fundef := + AST.transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. + +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. diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v new file mode 100644 index 00000000..254cc4ce --- /dev/null +++ b/backend/CSE2proof.v @@ -0,0 +1,1660 @@ +(* +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 CSE2. + +Lemma args_unaffected: + forall rs : regset, + forall dst : reg, + forall v, + forall args : list reg, + existsb (fun y : reg => peq dst y) args = false -> + (rs # dst <- v ## args) = (rs ## args). +Proof. + induction args; simpl; trivial. + destruct (peq dst a) as [EQ | NEQ]; simpl. + { discriminate. + } + intro EXIST. + f_equal. + { + apply Regmap.gso. + congruence. + } + apply IHargs. + assumption. +Qed. + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Section SAME_MEMORY. + Variable m : mem. + +Definition sem_sym_val sym rs (v : option val) : Prop := + match sym with + | SMove src => v = Some (rs # src) + | SOp op args => + v = (eval_operation genv sp op (rs ## args) m) + | SLoad chunk addr args => + match eval_addressing genv sp addr rs##args with + | Some a => match Mem.loadv chunk m a with + | Some dat => v = Some dat + | None => v = None \/ v = Some (default_notrap_load_value chunk) + end + | None => v = None \/ v = Some (default_notrap_load_value chunk) + end + end. + +Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) (v : val) : Prop := + match rel ! x with + | None => True + | Some sym => sem_sym_val sym rs (Some (rs # x)) + end. + +Definition sem_rel (rel : RELATION.t) (rs : regset) := + forall x : reg, (sem_reg rel x rs (rs # x)). + +Definition sem_rel_b (relb : RB.t) (rs : regset) := + match relb with + | Some rel => sem_rel rel rs + | None => False + end. + +Definition fmap_sem (fmap : option (PMap.t RB.t)) + (pc : node) (rs : regset) := + match fmap with + | None => True + | Some m => sem_rel_b (PMap.get pc m) rs + end. + +Lemma subst_arg_ok: + forall f, + forall pc, + forall rs, + forall arg, + fmap_sem (forward_map f) pc rs -> + rs # (subst_arg (forward_map f) pc arg) = rs # arg. +Proof. + intros until arg. + intro SEM. + unfold fmap_sem in SEM. + destruct (forward_map f) as [map |]in *; trivial. + simpl. + unfold sem_rel_b, sem_rel, sem_reg in *. + destruct (map # pc). + 2: contradiction. + pose proof (SEM arg) as SEMarg. + simpl. unfold forward_move. + unfold sem_sym_val in *. + destruct (t ! arg); trivial. + destruct s; congruence. +Qed. + +Lemma subst_args_ok: + forall f, + forall pc, + forall rs, + fmap_sem (forward_map f) pc rs -> + forall args, + rs ## (subst_args (forward_map f) pc args) = rs ## args. +Proof. + induction args; trivial. + simpl. + f_equal. + apply subst_arg_ok; assumption. + assumption. +Qed. + +Lemma kill_reg_sound : + forall rel : RELATION.t, + forall dst : reg, + forall rs, + forall v, + sem_rel rel rs -> + sem_rel (kill_reg dst rel) (rs # dst <- v). +Proof. + unfold sem_rel, kill_reg, sem_reg, sem_sym_val. + intros until v. + intros REL x. + rewrite PTree.gfilter1. + destruct (Pos.eq_dec dst x). + { + subst x. + rewrite PTree.grs. + trivial. + } + rewrite PTree.gro by congruence. + rewrite Regmap.gso by congruence. + destruct (rel ! x) as [relx | ] eqn:RELx; trivial. + unfold kill_sym_val. + pose proof (REL x) as RELinstx. + rewrite RELx in RELinstx. + destruct relx eqn:SYMVAL. + { + destruct (peq dst src); simpl. + { reflexivity. } + rewrite Regmap.gso by congruence. + assumption. + } + { destruct existsb eqn:EXISTS; simpl. + { reflexivity. } + rewrite args_unaffected by exact EXISTS. + assumption. + } + { destruct existsb eqn:EXISTS; simpl. + { reflexivity. } + rewrite args_unaffected by exact EXISTS. + assumption. + } +Qed. + +Lemma write_same: + forall rs : regset, + forall src dst : reg, + (rs # dst <- (rs # src)) # src = rs # src. +Proof. + intros. + destruct (peq src dst). + { + subst dst. + apply Regmap.gss. + } + rewrite Regmap.gso by congruence. + reflexivity. +Qed. + +Lemma move_sound : + forall rel : RELATION.t, + forall src dst : reg, + forall rs, + sem_rel rel rs -> + sem_rel (move src dst rel) (rs # dst <- (rs # src)). +Proof. + intros until rs. intros REL x. + pose proof (kill_reg_sound rel dst rs (rs # src) REL x) as KILL. + pose proof (REL src) as RELsrc. + unfold move. + destruct (peq x dst). + { + subst x. + unfold sem_reg. + rewrite PTree.gss. + rewrite Regmap.gss. + unfold sem_reg in *. + simpl. + unfold forward_move. + destruct (rel ! src) as [ sv |]; simpl. + destruct sv eqn:SV; simpl in *. + { + destruct (peq dst src0). + { + subst src0. + rewrite Regmap.gss. + reflexivity. + } + rewrite Regmap.gso by congruence. + assumption. + } + all: f_equal; symmetry; apply write_same. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + +Lemma move_cases_neq: + forall dst rel a, + a <> dst -> + (forward_move (kill_reg dst rel) a) <> dst. +Proof. + intros until a. intro NEQ. + unfold kill_reg, forward_move. + rewrite PTree.gfilter1. + rewrite PTree.gro by congruence. + destruct (rel ! a); simpl. + 2: congruence. + destruct s. + { + unfold kill_sym_val. + destruct peq; simpl; congruence. + } + all: simpl; + destruct negb; simpl; congruence. +Qed. + +Lemma args_replace_dst : + forall rel, + forall args : list reg, + forall dst : reg, + forall rs : regset, + forall v, + (sem_rel rel rs) -> + not (In dst args) -> + (rs # dst <- v) + ## (map + (forward_move (kill_reg dst rel)) args) = rs ## args. +Proof. + induction args; simpl. + 1: reflexivity. + intros until v. + intros REL NOT_IN. + rewrite IHargs by auto. + f_equal. + pose proof (REL a) as RELa. + rewrite Regmap.gso by (apply move_cases_neq; auto). + unfold kill_reg. + unfold sem_reg in RELa. + unfold forward_move. + rewrite PTree.gfilter1. + rewrite PTree.gro by auto. + destruct (rel ! a); simpl; trivial. + destruct s; simpl in *; destruct negb; simpl; congruence. +Qed. + +Lemma oper2_sound : + forall rel : RELATION.t, + forall op : operation, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall v, + sem_rel rel rs -> + not (In dst args) -> + eval_operation genv sp op (rs ## args) m = Some v -> + sem_rel (oper2 op dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL NOT_IN EVAL x. + pose proof (kill_reg_sound rel dst rs v REL x) as KILL. + unfold oper2. + destruct (peq x dst). + { + subst x. + unfold sem_reg. + rewrite PTree.gss. + rewrite Regmap.gss. + simpl. + rewrite args_replace_dst by auto. + symmetry. + assumption. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + +Lemma oper1_sound : + forall rel : RELATION.t, + forall op : operation, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall v, + sem_rel rel rs -> + eval_operation genv sp op (rs ## args) m = Some v -> + sem_rel (oper1 op dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL EVAL. + unfold oper1. + destruct in_dec. + { + apply kill_reg_sound; auto. + } + apply oper2_sound; auto. +Qed. + +Lemma find_op_sound : + forall rel : RELATION.t, + forall op : operation, + forall src : reg, + forall args: list reg, + forall rs : regset, + sem_rel rel rs -> + find_op rel op args = Some src -> + (eval_operation genv sp op (rs ## args) m) = Some (rs # src). +Proof. + intros until rs. + unfold find_op. + rewrite PTree.fold_spec. + intro REL. + assert ( + forall start, + match start with + | None => True + | Some src => eval_operation genv sp op rs ## args m = Some rs # src + end -> fold_left + (fun (a : option reg) (p : positive * sym_val) => + find_op_fold op args a (fst p) (snd p)) (PTree.elements rel) start = + Some src -> + eval_operation genv sp op rs ## args m = Some rs # src) as REC. + { + unfold sem_rel, sem_reg in REL. + generalize (PTree.elements_complete rel). + generalize (PTree.elements rel). + induction l; simpl. + { + intros. + subst start. + assumption. + } + destruct a as [r sv]; simpl. + intros COMPLETE start GEN. + apply IHl. + { + intros. + apply COMPLETE. + right. + assumption. + } + unfold find_op_fold. + destruct start. + assumption. + destruct sv; trivial. + destruct eq_operation; trivial. + subst op0. + destruct eq_args; trivial. + subst args0. + simpl. + assert ((rel ! r) = Some (SOp op args)) as RELatr. + { + apply COMPLETE. + left. + reflexivity. + } + pose proof (REL r) as RELr. + rewrite RELatr in RELr. + simpl in RELr. + symmetry. + assumption. + } + apply REC; auto. +Qed. + +Lemma find_load_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall src : reg, + forall args: list reg, + forall rs : regset, + sem_rel rel rs -> + find_load rel chunk addr args = Some src -> + match eval_addressing genv sp addr rs##args with + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk + end. +Proof. + intros until rs. + unfold find_load. + rewrite PTree.fold_spec. + intro REL. + assert ( + forall start, + match start with + | None => True + | Some src => + match eval_addressing genv sp addr rs##args with + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk + end + end -> + fold_left + (fun (a : option reg) (p : positive * sym_val) => + find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements rel) start = + Some src -> + match eval_addressing genv sp addr rs##args with + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk + end) as REC. + + { + unfold sem_rel, sem_reg in REL. + generalize (PTree.elements_complete rel). + generalize (PTree.elements rel). + induction l; simpl. + { + intros. + subst start. + assumption. + } + destruct a as [r sv]; simpl. + intros COMPLETE start GEN. + apply IHl. + { + intros. + apply COMPLETE. + right. + assumption. + } + unfold find_load_fold. + destruct start. + assumption. + destruct sv; trivial. + destruct chunk_eq; trivial. + subst chunk0. + destruct eq_addressing; trivial. + subst addr0. + destruct eq_args; trivial. + subst args0. + simpl. + assert ((rel ! r) = Some (SLoad chunk addr args)) as RELatr. + { + apply COMPLETE. + left. + reflexivity. + } + pose proof (REL r) as RELr. + rewrite RELatr in RELr. + simpl in RELr. + destruct eval_addressing. + { destruct Mem.loadv. + congruence. + destruct RELr; congruence. + } + destruct RELr; congruence. + } + apply REC; auto. +Qed. + + +Lemma find_load_sound' : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall src : reg, + forall args: list reg, + forall rs : regset, + forall a, + forall v, + sem_rel rel rs -> + find_load rel chunk addr args = Some src -> + eval_addressing genv sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + v = rs # src. +Proof. + intros until v. intros REL FINDLOAD ADDR LOAD. + pose proof (find_load_sound rel chunk addr src args rs REL FINDLOAD) as Z. + destruct eval_addressing in *. + { + replace a with v0 in * by congruence. + destruct Mem.loadv in * ; congruence. + } + discriminate. +Qed. + +Lemma find_load_notrap1_sound' : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall src : reg, + forall args: list reg, + forall rs : regset, + sem_rel rel rs -> + find_load rel chunk addr args = Some src -> + eval_addressing genv sp addr rs##args = None -> + rs # src = (default_notrap_load_value chunk). +Proof. + intros until rs. intros REL FINDLOAD ADDR. + pose proof (find_load_sound rel chunk addr src args rs REL FINDLOAD) as Z. + rewrite ADDR in Z. + assumption. +Qed. + +Lemma find_load_notrap2_sound' : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall src : reg, + forall args: list reg, + forall rs : regset, + forall a, + sem_rel rel rs -> + find_load rel chunk addr args = Some src -> + eval_addressing genv sp addr rs##args = Some a -> + Mem.loadv chunk m a = None -> + rs # src = (default_notrap_load_value chunk). +Proof. + intros until a. intros REL FINDLOAD ADDR LOAD. + pose proof (find_load_sound rel chunk addr src args rs REL FINDLOAD) as Z. + rewrite ADDR in Z. + destruct Mem.loadv. + discriminate. + assumption. +Qed. + +Lemma forward_move_map: + forall rel args rs, + sem_rel rel rs -> + rs ## (map (forward_move rel) args) = rs ## args. +Proof. + induction args; simpl; trivial. + intros rs REL. + f_equal. + 2: (apply IHargs; assumption). + unfold forward_move, sem_rel, sem_reg, sem_sym_val in *. + pose proof (REL a) as RELa. + destruct (rel ! a); trivial. + destruct s; congruence. +Qed. + +Lemma oper_sound : + forall rel : RELATION.t, + forall op : operation, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall v, + sem_rel rel rs -> + eval_operation genv sp op (rs ## args) m = Some v -> + sem_rel (oper op dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL EVAL. + unfold oper. + destruct find_op eqn:FIND. + { + assert (eval_operation genv sp op rs ## (map (forward_move rel) args) m = Some rs # r) as FIND_OP. + { + apply (find_op_sound rel); trivial. + } + rewrite forward_move_map in FIND_OP by assumption. + replace v with (rs # r) by congruence. + apply move_sound; auto. + } + apply oper1_sound; trivial. +Qed. + +Lemma gen_oper_sound : + forall rel : RELATION.t, + forall op : operation, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall v, + sem_rel rel rs -> + eval_operation genv sp op (rs ## args) m = Some v -> + sem_rel (gen_oper op dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL EVAL. + unfold gen_oper. + destruct op. + { destruct args as [ | h0 t0]. + apply oper_sound; auto. + destruct t0. + { + simpl in *. + replace v with (rs # h0) by congruence. + apply move_sound; auto. + } + apply oper_sound; auto. + } + all: apply oper_sound; auto. +Qed. + + +Lemma load2_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + forall v, + sem_rel rel rs -> + not (In dst args) -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = Some v -> + sem_rel (load2 chunk addr dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL NOT_IN ADDR LOAD x. + pose proof (kill_reg_sound rel dst rs v REL x) as KILL. + unfold load2. + destruct (peq x dst). + { + subst x. + unfold sem_reg. + rewrite PTree.gss. + rewrite Regmap.gss. + simpl. + rewrite args_replace_dst by auto. + destruct eval_addressing. + { + replace a with v0 in * by congruence. + destruct Mem.loadv; congruence. + } + discriminate. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + +Lemma load2_notrap1_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + sem_rel rel rs -> + not (In dst args) -> + eval_addressing genv sp addr (rs ## args) = None -> + sem_rel (load2 chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until rs. + intros REL NOT_IN ADDR x. + pose proof (kill_reg_sound rel dst rs (default_notrap_load_value chunk) REL x) as KILL. + unfold load2. + destruct (peq x dst). + { + subst x. + unfold sem_reg. + rewrite PTree.gss. + rewrite Regmap.gss. + simpl. + rewrite args_replace_dst by auto. + rewrite ADDR. + right. + trivial. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + +Lemma load2_notrap2_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + sem_rel rel rs -> + not (In dst args) -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = None -> + sem_rel (load2 chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until a. + intros REL NOT_IN ADDR LOAD x. + pose proof (kill_reg_sound rel dst rs (default_notrap_load_value chunk) REL x) as KILL. + unfold load2. + destruct (peq x dst). + { + subst x. + unfold sem_reg. + rewrite PTree.gss. + rewrite Regmap.gss. + simpl. + rewrite args_replace_dst by auto. + rewrite ADDR. + rewrite LOAD. + right; trivial. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + +Lemma load1_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + forall v, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = Some v -> + sem_rel (load1 chunk addr dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL ADDR LOAD. + unfold load1. + destruct in_dec. + { + apply kill_reg_sound; auto. + } + apply load2_sound with (a := a); auto. +Qed. + +Lemma load1_notrap1_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = None -> + sem_rel (load1 chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until rs. + intros REL ADDR LOAD. + unfold load1. + destruct in_dec. + { + apply kill_reg_sound; auto. + } + apply load2_notrap1_sound; auto. +Qed. + +Lemma load1_notrap2_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = None -> + sem_rel (load1 chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until a. + intros REL ADDR LOAD. + unfold load1. + destruct in_dec. + { + apply kill_reg_sound; auto. + } + apply load2_notrap2_sound with (a := a); auto. +Qed. + +Lemma load_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + forall v, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = Some v -> + sem_rel (load chunk addr dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL ADDR LOAD. + unfold load. + destruct find_load as [src | ] eqn:FIND. + { + assert (match eval_addressing genv sp addr rs## (map (forward_move rel) args) with + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk + end) as FIND_LOAD. + { + apply (find_load_sound rel); trivial. + } + rewrite forward_move_map in FIND_LOAD by assumption. + destruct eval_addressing in *. + 2: discriminate. + replace v0 with a in * by congruence. + destruct Mem.loadv in *. + 2: discriminate. + replace v with (rs # src) by congruence. + apply move_sound; auto. + } + apply load1_sound with (a := a); trivial. +Qed. + +Lemma load_notrap1_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = None -> + sem_rel (load chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until rs. + intros REL ADDR. + unfold load. + destruct find_load as [src | ] eqn:FIND. + { + assert (match eval_addressing genv sp addr rs## (map (forward_move rel) args) with + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk + end) as FIND_LOAD. + { + apply (find_load_sound rel); trivial. + } + rewrite forward_move_map in FIND_LOAD by assumption. + destruct eval_addressing in *. + discriminate. + rewrite <- FIND_LOAD. + apply move_sound; auto. + } + apply load1_notrap1_sound; trivial. +Qed. + +Lemma load_notrap2_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = None -> + sem_rel (load chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until a. + intros REL ADDR. + unfold load. + destruct find_load as [src | ] eqn:FIND. + { + assert (match eval_addressing genv sp addr rs## (map (forward_move rel) args) with + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk + end) as FIND_LOAD. + { + apply (find_load_sound rel); trivial. + } + rewrite forward_move_map in FIND_LOAD by assumption. + rewrite ADDR in FIND_LOAD. + destruct Mem.loadv; intro. + discriminate. + rewrite <- FIND_LOAD. + apply move_sound; auto. + } + apply load1_notrap2_sound; trivial. +Qed. + +Lemma kill_reg_weaken: + forall res mpc rs, + sem_rel mpc rs -> + sem_rel (kill_reg res mpc) rs. +Proof. + intros until rs. + intros REL x. + pose proof (REL x) as RELx. + unfold kill_reg, sem_reg in *. + rewrite PTree.gfilter1. + destruct (peq res x). + { subst x. + rewrite PTree.grs. + reflexivity. + } + rewrite PTree.gro by congruence. + destruct (mpc ! x) as [sv | ]; trivial. + destruct negb; trivial. +Qed. + +Lemma top_ok: + forall rs, sem_rel RELATION.top rs. +Proof. + unfold sem_rel, sem_reg, RELATION.top. + intros. + rewrite PTree.gempty. + reflexivity. +Qed. + +Lemma sem_rel_ge: + forall r1 r2 : RELATION.t, + (RELATION.ge r1 r2) -> + forall rs : regset, + (sem_rel r2 rs) -> (sem_rel r1 rs). +Proof. + intros r1 r2 GE rs RE x. + pose proof (RE x) as REx. + pose proof (GE x) as GEx. + unfold sem_reg in *. + destruct (r1 ! x) as [r1x | ] in *; + destruct (r2 ! x) as [r2x | ] in *; + congruence. +Qed. +End SAME_MEMORY. + +Lemma kill_mem_sound : + forall m m' : mem, + forall rel : RELATION.t, + forall rs, + sem_rel m rel rs -> sem_rel m' (kill_mem rel) rs. +Proof. + unfold sem_rel, sem_reg. + intros until rs. + intros SEM x. + pose proof (SEM x) as SEMx. + unfold kill_mem. + rewrite PTree.gfilter1. + unfold kill_sym_val_mem. + destruct (rel ! x) as [ sv | ]. + 2: reflexivity. + destruct sv; simpl in *; trivial. + { + destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial. + rewrite SEMx. + apply op_depends_on_memory_correct; auto. + } +Qed. + +End SOUNDNESS. + +Definition match_prog (p tp: RTL.program) := + match_program (fun cu f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. apply match_transform_program; auto. +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; trivial. +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 : function) (pc : node) (i : instruction), + (fn_code f)!pc = Some i -> + (fn_code (transf_function f))!pc = + Some(transf_instr (forward_map f) pc i). +Proof. + intros until i. intro CODE. + unfold transf_function; simpl. + rewrite PTree.gmap. + unfold option_map. + rewrite CODE. + reflexivity. +Qed. + +Definition is_killed_in_map (map : PMap.t RB.t) pc res := + match PMap.get pc map with + | None => True + | Some rel => exists rel', RELATION.ge rel (kill_reg res rel') + end. + +Definition is_killed_in_fmap fmap pc res := + match fmap with + | None => True + | Some map => is_killed_in_map map pc res + end. + +Definition sem_rel_b' := sem_rel_b fundef unit ge. +Definition fmap_sem' := fmap_sem fundef unit ge. +Definition subst_arg_ok' := subst_arg_ok fundef unit ge. +Definition subst_args_ok' := subst_args_ok fundef unit ge. +Definition kill_mem_sound' := kill_mem_sound fundef unit ge. + +Lemma sem_rel_b_ge: + forall rb1 rb2 : RB.t, + (RB.ge rb1 rb2) -> + forall sp m, + forall rs : regset, + (sem_rel_b' sp m rb2 rs) -> (sem_rel_b' sp m rb1 rs). +Proof. + unfold sem_rel_b', sem_rel_b. + destruct rb1 as [r1 | ]; + destruct rb2 as [r2 | ]; simpl; + intros GE sp m rs RE; try contradiction. + apply sem_rel_ge with (r2 := r2); assumption. +Qed. + +Lemma apply_instr'_bot : + forall code, + forall pc, + RB.eq (apply_instr' code pc RB.bot) RB.bot. +Proof. + reflexivity. +Qed. + +Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := +| match_frames_intro: forall res f sp pc rs, + (forall m : mem, + forall vres, (fmap_sem' sp m (forward_map f) pc rs # res <- vres)) -> + 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'), + (fmap_sem' sp m (forward_map f) pc rs) -> + 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). + +Ltac TR_AT := + match goal with + | [ A: (fn_code _)!_ = Some _ |- _ ] => + generalize (transf_function_at _ _ _ A); intros + 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; try TR_AT. +- (* nop *) + econstructor; split. eapply exec_Inop; eauto. + constructor; auto. + + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply sem_rel_b_ge with (rb2 := map # pc); trivial. + replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + unfold sem_rel_b in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. +- (* op *) + unfold transf_instr in *. + destruct find_op_in_fmap eqn:FIND_OP. + { + unfold find_op_in_fmap, fmap_sem', fmap_sem in *. + destruct (forward_map f) as [map |] eqn:MAP. + 2: discriminate. + change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. + destruct (map # pc) as [mpc | ] eqn:MPC. + 2: discriminate. + econstructor; split. + { + eapply exec_Iop with (v := v); eauto. + simpl. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. + { + rewrite MAP in H0. + rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption. + assumption. + } + unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. + } + constructor; eauto. + unfold fmap_sem', fmap_sem in *. + rewrite MAP. + apply sem_rel_b_ge with (rb2 := Some (gen_oper op res args mpc)). + { + replace (Some (gen_oper op res args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + unfold sem_rel_b', sem_rel_b. + apply gen_oper_sound; auto. + } + { + econstructor; split. + { + eapply exec_Iop with (v := v); eauto. + rewrite (subst_args_ok' sp m) by assumption. + rewrite <- H0. + apply eval_operation_preserved. exact symbols_preserved. + } + constructor; eauto. + unfold fmap_sem', fmap_sem in *. + unfold find_op_in_fmap, fmap_sem', fmap_sem in *. + destruct (forward_map f) as [map |] eqn:MAP. + 2: constructor. + change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. + destruct (map # pc) as [mpc | ] eqn:MPC. + 2: contradiction. + + apply sem_rel_b_ge with (rb2 := Some (gen_oper op res args mpc)). + { + replace (Some (gen_oper op res args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + unfold sem_rel_b', sem_rel_b. + apply gen_oper_sound; auto. + } + +(* load *) +- unfold transf_instr in *. + destruct find_load_in_fmap eqn:FIND_LOAD. + { + unfold find_load_in_fmap, fmap_sem', fmap_sem in *. + destruct (forward_map f) as [map |] eqn:MAP. + 2: discriminate. + change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. + destruct (map # pc) as [mpc | ] eqn:MPC. + 2: discriminate. + econstructor; split. + { + eapply exec_Iop with (v := v); eauto. + simpl. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. + { + f_equal. + symmetry. + apply find_load_sound' with (chunk := chunk) (m := m) (a := a) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial. + rewrite MAP in H0. + assumption. + } + unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. + } + constructor; eauto. + unfold fmap_sem', fmap_sem in *. + rewrite MAP. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + unfold sem_rel_b', sem_rel_b. + apply load_sound with (a := a); auto. + } + { + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. + apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. + rewrite (subst_args_ok' sp m); assumption. + constructor; auto. + + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + apply load_sound with (a := a); assumption. + } + +- unfold transf_instr in *. + destruct find_load_in_fmap eqn:FIND_LOAD. + { + unfold find_load_in_fmap, fmap_sem', fmap_sem in *. + destruct (forward_map f) as [map |] eqn:MAP. + 2: discriminate. + change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. + destruct (map # pc) as [mpc | ] eqn:MPC. + 2: discriminate. + + econstructor; split. + { + eapply exec_Iop with (v := (default_notrap_load_value chunk)); eauto. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. + { simpl. + f_equal. + apply find_load_notrap1_sound' with (chunk := chunk) (m := m) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial. + rewrite MAP in H0. + assumption. + } + unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. + } + constructor; eauto. + unfold fmap_sem', fmap_sem in *. + rewrite MAP. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + unfold sem_rel_b', sem_rel_b. + apply load_notrap1_sound; auto. + } + { + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = None). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload_notrap1; eauto. + rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m) ; assumption. + constructor; auto. + + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + apply load_notrap1_sound; trivial. + } + +- (* load notrap2 *) + unfold transf_instr in *. + destruct find_load_in_fmap eqn:FIND_LOAD. + { + unfold find_load_in_fmap, fmap_sem', fmap_sem in *. + destruct (forward_map f) as [map |] eqn:MAP. + 2: discriminate. + change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. + destruct (map # pc) as [mpc | ] eqn:MPC. + 2: discriminate. + econstructor; split. + { + eapply exec_Iop with (v := (default_notrap_load_value chunk)); eauto. + simpl. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. + { + f_equal. + apply find_load_notrap2_sound' with (chunk := chunk) (m := m) (a := a) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial. + rewrite MAP in H0. + assumption. + } + unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. + } + constructor; eauto. + unfold fmap_sem', fmap_sem in *. + rewrite MAP. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + unfold sem_rel_b', sem_rel_b. + apply load_notrap2_sound with (a := a); auto. + } + { + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload_notrap2; eauto. + rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m); assumption. + constructor; auto. + + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + apply load_notrap2_sound with (a := a); assumption. + } + +- (* store *) + econstructor. split. + { + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Istore; eauto. + rewrite (subst_args_ok' sp m); assumption. + } + + constructor; auto. + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply sem_rel_b_ge with (rb2 := Some (kill_mem mpc)); trivial. + { + replace (Some (kill_mem mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + unfold sem_rel_b in *. + rewrite MPC. + rewrite H. + reflexivity. + } + apply (kill_mem_sound' sp m). + assumption. + +(* call *) +- econstructor; split. + eapply exec_Icall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + rewrite (subst_args_ok' sp m) by assumption. + constructor. constructor; auto. + + constructor. + { + intros m' vres. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply sem_rel_b_ge with (rb2 := Some (kill_reg res (kill_mem mpc))). + { + replace (Some (kill_reg res (kill_mem mpc))) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + apply kill_reg_sound. + apply (kill_mem_sound' sp m). + assumption. + } + +(* tailcall *) +- econstructor; split. + eapply exec_Itailcall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + rewrite (subst_args_ok' (Vptr stk Ptrofs.zero) m) by assumption. + constructor. auto. + +(* builtin *) +- econstructor; split. + eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor; auto. + + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + + apply sem_rel_b_ge with (rb2 := Some RELATION.top). + { + replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + apply top_ok. + + +(* cond *) +- econstructor; split. + eapply exec_Icond; eauto. + rewrite (subst_args_ok' sp m); eassumption. + constructor; auto. + + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply sem_rel_b_ge with (rb2 := map # pc); trivial. + replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. + destruct b; tauto. + } + unfold apply_instr'. + unfold sem_rel_b in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. + +(* jumptbl *) +- econstructor; split. + eapply exec_Ijumptable; eauto. + rewrite (subst_arg_ok' sp m); eassumption. + constructor; auto. + + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply sem_rel_b_ge with (rb2 := map # pc); trivial. + replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. + apply list_nth_z_in with (n := Int.unsigned n). + assumption. + } + unfold apply_instr'. + unfold sem_rel_b in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. + +(* return *) +- destruct or as [arg | ]. + { + econstructor; split. + eapply exec_Ireturn; eauto. + unfold regmap_optget. + rewrite (subst_arg_ok' (Vptr stk Ptrofs.zero) m) by eassumption. + constructor; auto. + } + econstructor; split. + eapply exec_Ireturn; eauto. + constructor; auto. + + +(* internal function *) +- simpl. econstructor; split. + eapply exec_function_internal; eauto. + constructor; auto. + + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply sem_rel_b_ge with (rb2 := Some RELATION.top). + { + eapply DS.fixpoint_entry with (code := fn_code f) (successors := successors_instr); try eassumption. + } + apply top_ok. + +(* external function *) +- econstructor; split. + eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor; auto. + +(* return *) +- inv STACKS. inv H1. + econstructor; split. + eapply exec_return; eauto. + constructor; auto. +Admitted. + + +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_step. + apply senv_preserved. + eexact transf_initial_states. + eexact transf_final_states. + exact step_simulation. +Qed. + +End PRESERVATION.
\ No newline at end of file diff --git a/config_rv32.sh b/config_rv32.sh new file mode 100755 index 00000000..a5a5cf1c --- /dev/null +++ b/config_rv32.sh @@ -0,0 +1 @@ +exec ./config_simple.sh rv32-linux --toolprefix riscv64-linux-gnu- "$@" diff --git a/config_simple.sh b/config_simple.sh new file mode 100755 index 00000000..f02680c4 --- /dev/null +++ b/config_simple.sh @@ -0,0 +1,6 @@ +arch=$1 +shift +version=`git rev-parse --short HEAD` +branch=`git rev-parse --abbrev-ref HEAD` +date=`date -I` +./configure --prefix /opt/CompCert/${branch}/${date}_${version}/$arch "$@" $arch diff --git a/driver/Clflags.ml b/driver/Clflags.ml index a4ebee9c..6d6f1df4 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -26,6 +26,7 @@ let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true let option_fconstprop = ref true let option_fcse = ref true +let option_fcse2 = ref true let option_fredundancy = ref true let option_fduplicate = ref false let option_finvertcond = ref true (* only active if option_fduplicate is also true *) diff --git a/driver/Compiler.v b/driver/Compiler.v index 9f53a4fc..499feff2 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -42,6 +42,7 @@ Require Duplicate. Require Constprop. Require CSE. Require ForwardMoves. +Require CSE2. Require Deadcode. Require Unusedglob. Require Allnontrap. @@ -66,6 +67,7 @@ Require Duplicateproof. Require Constpropproof. Require CSEproof. Require ForwardMovesproof. +Require CSE2proof. Require Deadcodeproof. Require Unusedglobproof. Require Allnontrapproof. @@ -140,14 +142,16 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 6) @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 7) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 8) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 9) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 10) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 11) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 12) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -254,6 +258,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) @@ -300,8 +305,9 @@ Proof. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. - set (p13bis := total_if optim_forward_moves ForwardMoves.transf_program p13) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13bis) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. + set (p13ter := total_if optim_forward_moves ForwardMoves.transf_program p13bis) in *. + destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. @@ -324,7 +330,8 @@ Proof. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13bis; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. + exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. + exists p13ter; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. exists p15; split. apply Unusedglobproof.transf_program_match; auto. @@ -385,7 +392,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p24)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p25)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -413,7 +420,9 @@ Ltac DestructM := eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. + eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index a979c69b..b4b9f30d 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -40,6 +40,9 @@ Parameter optim_constprop: unit -> bool. (** Flag -fcse. For common subexpression elimination. *) Parameter optim_CSE: unit -> bool. +(** Flag -fcse2. For DMonniaux's common subexpression elimination. *) +Parameter optim_CSE2: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 70a3739b..db71aef9 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -195,6 +195,7 @@ Processing options: -ffloat-const-prop <n> Control constant propagation of floats (<n>=0: none, <n>=1: limited, <n>=2: full; default is full) -fcse Perform common subexpression elimination [on] + -fcse2 Perform inter-loop common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= <optim> Perform postpass scheduling with the specified optimization [list] @@ -263,8 +264,10 @@ let dump_mnemonics destfile = exit 0 let optimization_options = [ - option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; - option_fpostpass; option_fredundancy; option_finline_functions_called_once; + option_ftailcalls; option_fifconversion; option_fconstprop; + option_fcse; option_fcse2; + option_fpostpass; + option_fredundancy; option_finline; option_finline_functions_called_once; ] let set_all opts () = List.iter (fun r -> r := true) opts @@ -387,6 +390,7 @@ let cmdline_actions = @ f_opt "if-conversion" option_fifconversion @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse + @ f_opt "cse2" option_fcse2 @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass @ f_opt "duplicate" option_fduplicate diff --git a/extraction/extraction.v b/extraction/extraction.v index c2f97778..929c21e0 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -111,6 +111,8 @@ Extract Constant Compopts.optim_constprop => "fun _ -> !Clflags.option_fconstprop". Extract Constant Compopts.optim_CSE => "fun _ -> !Clflags.option_fcse". +Extract Constant Compopts.optim_CSE2 => + "fun _ -> !Clflags.option_fcse2". Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.optim_postpass => diff --git a/test/monniaux/cse2/loopaccess.c b/test/monniaux/cse2/loopaccess.c new file mode 100644 index 00000000..5ddaeb66 --- /dev/null +++ b/test/monniaux/cse2/loopaccess.c @@ -0,0 +1,7 @@ +double toto(double x, int count) { + double r = 5*x + 3; + while (count > r) { + count --; + } + return 5*x + 3; +} diff --git a/test/monniaux/cse2/loopinvariant.c b/test/monniaux/cse2/loopinvariant.c new file mode 100644 index 00000000..64caf80b --- /dev/null +++ b/test/monniaux/cse2/loopinvariant.c @@ -0,0 +1,7 @@ +int toto(int *t, int n) { + int x = t[0]; + for(int i=1; i<n; i++) { + if (t[i] > t[0]) return i; + } + return 0; +} diff --git a/test/monniaux/cse2/loopload.c b/test/monniaux/cse2/loopload.c new file mode 100644 index 00000000..6e0925f7 --- /dev/null +++ b/test/monniaux/cse2/loopload.c @@ -0,0 +1,5 @@ +int find_index(int *t, int n) { + if (t[0] > 0) return 3; + while (n > 0) n--; + return t[0]; +} |