diff options
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/Asmgen.v | 12 | ||||
| -rw-r--r-- | x86/Asmgenproof.v | 12 | ||||
| -rw-r--r-- | x86/Asmgenproof1.v | 8 | ||||
| -rw-r--r-- | x86/Op.v | 41 | ||||
| -rw-r--r-- | x86/ValueAOp.v | 21 |
5 files changed, 84 insertions, 10 deletions
diff --git a/x86/Asmgen.v b/x86/Asmgen.v index 73e3263e..99e9fc2b 100644 --- a/x86/Asmgen.v +++ b/x86/Asmgen.v @@ -636,9 +636,14 @@ Definition transl_op (** Translation of memory loads and stores *) -Definition transl_load (chunk: memory_chunk) +Definition transl_load + (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dest: mreg) (k: code) : res code := + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load x86 does not support non trapping loads") + | TRAP => do am <- transl_addressing addr args; match chunk with | Mint8unsigned => @@ -659,6 +664,7 @@ Definition transl_load (chunk: memory_chunk) do r <- freg_of dest; OK(Pmovsd_fm r am :: k) | _ => Error (msg "Asmgen.transl_load") + end end. Definition transl_store (chunk: memory_chunk) @@ -699,8 +705,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) loadind RSP f.(fn_link_ofs) Tptr AX k1) | Mop op args res => transl_op op args res k - | Mload chunk addr args dst => - transl_load chunk addr args dst k + | Mload trap chunk addr args dst => + transl_load trap chunk addr args dst k | Mstore chunk addr args src => transl_store chunk addr args src k | Mcall sig (inl reg) => diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v index f1fd41e3..6886b2fd 100644 --- a/x86/Asmgenproof.v +++ b/x86/Asmgenproof.v @@ -235,11 +235,11 @@ Proof. Qed. Remark transl_load_label: - forall chunk addr args dest k c, - transl_load chunk addr args dest k = OK c -> + forall trap chunk addr args dest k c, + transl_load trap chunk addr args dest k = OK c -> tail_nolabel k c. Proof. - intros. monadInv H. destruct chunk; TailNoLabel. + intros. destruct trap; try discriminate. monadInv H. destruct chunk; TailNoLabel. Qed. Remark transl_store_label: @@ -567,6 +567,12 @@ Opaque loadind. split. eapply agree_set_undef_mreg; eauto. congruence. simpl; congruence. +- (* Mload notrap *) (* isn't there a nicer way? *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + +- (* Mload notrap *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + - (* Mstore *) assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v index fd88954e..7cff1047 100644 --- a/x86/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -1464,8 +1464,8 @@ Qed. (** Translation of memory loads. *) Lemma transl_load_correct: - forall chunk addr args dest k c (rs: regset) m a v, - transl_load chunk addr args dest k = OK c -> + forall trap chunk addr args dest k c (rs: regset) m a v, + transl_load trap chunk addr args dest k = OK c -> eval_addressing ge (rs#RSP) addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> exists rs', @@ -1473,7 +1473,9 @@ Lemma transl_load_correct: /\ rs'#(preg_of dest) = v /\ forall r, data_preg r = true -> r <> preg_of dest -> rs'#r = rs#r. Proof. - unfold transl_load; intros. monadInv H. + unfold transl_load; intros. + destruct trap; simpl; try discriminate. + monadInv H. exploit transl_addressing_mode_correct; eauto. intro EA. assert (EA': eval_addrmode ge x rs = a). destruct a; simpl in H1; try discriminate; inv EA; auto. set (rs2 := nextinstr_nf (rs#(preg_of dest) <- v)). @@ -1199,6 +1199,21 @@ Proof. unfold eval_addressing; intros. destruct Archi.ptr64; eauto using eval_addressing32_inj, eval_addressing64_inj. Qed. +Lemma eval_addressing_inj_none: + forall addr sp1 vl1 sp2 vl2, + (forall id ofs, + In id (globals_addressing addr) -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> + eval_addressing ge1 sp1 addr vl1 = None -> + eval_addressing ge2 sp2 addr vl2 = None. +Proof. + intros until vl2. intros Hglobal Hinjsp Hinjvl. + destruct addr; simpl in *; + inv Hinjvl; trivial; try discriminate; inv H0; trivial; try discriminate; inv H2; trivial; try discriminate. +Qed. + Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, (forall id ofs, @@ -1425,6 +1440,19 @@ Proof. destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. +Lemma eval_addressing_lessdef_none: + forall sp addr vl1 vl2, + Val.lessdef_list vl1 vl2 -> + eval_addressing genv sp addr vl1 = None -> + eval_addressing genv sp addr vl2 = None. +Proof. + intros until vl2. intros Hlessdef Heval1. + destruct addr; simpl in *; + inv Hlessdef; trivial; try discriminate; + inv H0; trivial; try discriminate; + inv H2; trivial; try discriminate. +Qed. + End EVAL_LESSDEF. (** Compatibility of the evaluation functions with memory injections. *) @@ -1477,6 +1505,19 @@ Proof. econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. +Lemma eval_addressing_inject_none: + forall addr vl1 vl2, + Val.inject_list f vl1 vl2 -> + eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = None -> + eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = None. +Proof. + intros. + rewrite eval_shift_stack_addressing. + eapply eval_addressing_inj_none with (sp1 := Vptr sp1 Ptrofs.zero); eauto. + intros. apply symbol_address_inject. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. +Qed. + Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, Val.inject_list f vl1 vl2 -> diff --git a/x86/ValueAOp.v b/x86/ValueAOp.v index d0b8427a..e5584b6a 100644 --- a/x86/ValueAOp.v +++ b/x86/ValueAOp.v @@ -261,6 +261,25 @@ Proof. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. apply select_sound; auto. eapply eval_static_condition_sound; eauto. Qed. - +(* +Theorem eval_static_addressing_sound_none: + forall addr vargs aargs, + eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = None -> + list_forall2 (vmatch bc) vargs aargs -> + (eval_static_addressing addr aargs) = Vbot. +Proof. + unfold eval_addressing, eval_static_addressing. + intros until aargs. intros Heval_none Hlist. + destruct (Archi.ptr64). + inv Hlist. + destruct addr; trivial; discriminate. + inv H0. + destruct addr; trivial; try discriminate. simpl in *. + inv H2. + destruct addr; trivial; discriminate. + inv H3; + destruct addr; trivial; discriminate. +Qed. +*) End SOUNDNESS. |