diff options
-rw-r--r-- | backend/CSE.v | 26 | ||||
-rw-r--r-- | backend/CSEdomain.v | 12 | ||||
-rw-r--r-- | backend/CSEproof.v | 70 |
3 files changed, 89 insertions, 19 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index 1c884cf0..2827161d 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -202,10 +202,10 @@ Definition add_op (n: numbering) (rd: reg) (op: operation) (rs: list reg) := and added to [n] as described in [add_rhs]. *) Definition add_load (n: numbering) (rd: reg) - (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) + (chunk: memory_chunk) (addr: addressing) (rs: list reg) := let (n1, vs) := valnum_regs n rs in - add_rhs n1 rd (Load trap chunk addr vs). + add_rhs n1 rd (Load chunk addr vs). (** [set_unknown n rd] returns a numbering where [rd] is mapped to no value number, and no equations are added. This is useful @@ -246,7 +246,7 @@ Definition kill_equations (pred: rhs -> bool) (n: numbering) : numbering := Definition filter_loads (r: rhs) : bool := match r with | Op op _ => op_depends_on_memory op - | Load _ _ _ _ => true + | Load _ _ _ => true end. Definition kill_all_loads (n: numbering) : numbering := @@ -262,7 +262,7 @@ Definition filter_after_store (app: VA.t) (n: numbering) (p: aptr) (sz: Z) (r: r match r with | Op op vl => op_depends_on_memory op - | Load trap chunk addr vl => + | Load chunk addr vl => match regs_valnums n vl with | None => true | Some rl => @@ -297,7 +297,7 @@ Definition add_store_result (app: VA.t) (n: numbering) (chunk: memory_chunk) (ad let (n1, vsrc) := valnum_reg n rsrc in let (n2, vargs) := valnum_regs n1 rargs in {| num_next := n2.(num_next); - num_eqs := Eq vsrc false (Load TRAP chunk addr vargs) :: n2.(num_eqs); + num_eqs := Eq vsrc false (Load chunk addr vargs) :: n2.(num_eqs); num_reg := n2.(num_reg); num_val := n2.(num_val) |} else n. @@ -326,7 +326,7 @@ Definition kill_loads_after_storebytes Definition shift_memcpy_eq (src sz delta: Z) (e: equation) := match e with - | Eq l strict (Load trap chunk (Ainstack i) _) => + | Eq l strict (Load chunk (Ainstack i) _) => let i := Ptrofs.unsigned i in let j := i + delta in if zle src i @@ -334,7 +334,7 @@ Definition shift_memcpy_eq (src sz delta: Z) (e: equation) := && zeq (Z.modulo delta (align_chunk chunk)) 0 && zle 0 j && zle j Ptrofs.max_unsigned - then Some(Eq l strict (Load trap chunk (Ainstack (Ptrofs.repr j)) nil)) + then Some(Eq l strict (Load chunk (Ainstack (Ptrofs.repr j)) nil)) else None | _ => None end. @@ -459,8 +459,10 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb before | Iop op args res s => add_op before res op args - | Iload trap chunk addr args dst s => - add_load before dst trap chunk addr args + | Iload TRAP chunk addr args dst s => + add_load before dst chunk addr args + | Iload NOTRAP _ _ _ dst _ => + set_unknown before dst | Istore chunk addr args src s => let app := approx!!pc in let n := kill_loads_after_store app before chunk addr args in @@ -534,14 +536,14 @@ Definition transf_instr (n: numbering) (instr: instruction) := let (op', args') := reduce _ combine_op n1 op args vl in Iop op' args' res s end - | Iload trap chunk addr args dst s => + | Iload TRAP chunk addr args dst s => let (n1, vl) := valnum_regs n args in - match find_rhs n1 (Load trap chunk addr vl) with + match find_rhs n1 (Load chunk addr vl) with | Some r => Iop Omove (r :: nil) dst s | None => let (addr', args') := reduce _ combine_addr n1 addr args vl in - Iload trap chunk addr' args' dst s + Iload TRAP chunk addr' args' dst s end | Istore chunk addr args src s => let (n1, vl) := valnum_regs n args in diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v index 26d9c481..34ec0118 100644 --- a/backend/CSEdomain.v +++ b/backend/CSEdomain.v @@ -32,7 +32,7 @@ Definition valnum := positive. Inductive rhs : Type := | Op: operation -> list valnum -> rhs - | Load: trapping_mode -> memory_chunk -> addressing -> list valnum -> rhs. + | Load: memory_chunk -> addressing -> list valnum -> rhs. Inductive equation : Type := | Eq (v: valnum) (strict: bool) (r: rhs). @@ -74,7 +74,7 @@ Definition empty_numbering := Definition valnums_rhs (r: rhs): list valnum := match r with | Op op vl => vl - | Load trap chunk addr vl => vl + | Load chunk addr vl => vl end. Definition wf_rhs (next: valnum) (r: rhs) : Prop := @@ -106,11 +106,11 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem): | op_eval_to: forall op vl v, eval_operation ge sp op (map valu vl) m = Some v -> rhs_eval_to valu ge sp m (Op op vl) v - | load_eval_to: forall trap chunk addr vl a v, + | load_eval_to: forall chunk addr vl a v, eval_addressing ge sp addr (map valu vl) = Some a -> Mem.loadv chunk m a = Some v -> - rhs_eval_to valu ge sp m (Load trap chunk addr vl) v - | load_notrap1_eval_to: forall chunk addr vl, + rhs_eval_to valu ge sp m (Load chunk addr vl) v +(* | load_notrap1_eval_to: forall chunk addr vl, eval_addressing ge sp addr (map valu vl) = None -> rhs_eval_to valu ge sp m (Load NOTRAP chunk addr vl) (default_notrap_load_value chunk) @@ -118,7 +118,7 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem): eval_addressing ge sp addr (map valu vl) = Some a -> Mem.loadv chunk m a = None -> rhs_eval_to valu ge sp m (Load NOTRAP chunk addr vl) - (default_notrap_load_value chunk). + (default_notrap_load_value chunk) *). Inductive equation_holds (valu: valuation) (ge: genv) (sp: val) (m: mem): equation -> Prop := diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 50eb4637..684729d4 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1164,8 +1164,76 @@ Proof. apply set_reg_lessdef; assumption. } -(* TODO *) +- (* Iload notrap 1*) + destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. + destruct SAT as [valu1 NH1]. + exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). + + econstructor. split. + eapply exec_Iload_notrap1; eauto. + rewrite eval_addressing_preserved with (ge1 := ge). + apply eval_addressing_lessdef_none with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + exact symbols_preserved. + + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef. + constructor. assumption. +- (* Iload notrap 2*) + destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. + destruct SAT as [valu1 NH1]. + exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). + + assert (exists a' : val, + eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a') + as Haa'. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + destruct Haa' as [a' [Ha'1 Ha'2]]. + + destruct (Mem.loadv chunk m' a') eqn:Hload'. + + { + econstructor. split. + eapply exec_Iload; eauto. + rewrite eval_addressing_preserved with (ge1 := ge). + exact Ha'1. + exact symbols_preserved. + + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + unfold default_notrap_load_value. + apply set_reg_lessdef; eauto. + } + { + econstructor. split. + eapply exec_Iload_notrap2; eauto. + rewrite eval_addressing_preserved with (ge1 := ge). + exact Ha'1. + exact symbols_preserved. + + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef. + constructor. assumption. + } + - (* Istore *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. destruct SAT as [valu1 NH1]. |