diff options
91 files changed, 1998 insertions, 381 deletions
@@ -88,6 +88,7 @@ BACKEND=\ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ + Allnontrap.v Allnontrapproof.v \ Allocation.v Allocproof.v \ Tunneling.v Tunnelingproof.v \ Linear.v Lineartyping.v \ diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 1a1e7f2f..016a1c5a 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -689,8 +689,12 @@ Definition transl_memory_access_float None mk_immed addr args k. -Definition transl_load (chunk: memory_chunk) (addr: addressing) - (args: list mreg) (dst: mreg) (k: code) := +Definition transl_load (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (dst: mreg) (k: code) := + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm") + | TRAP => match chunk with | Mint8signed => transl_memory_access_int Pldrsb mk_immed_mem_small dst addr args k @@ -708,6 +712,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k | _ => Error (msg "Asmgen.transl_load") + end end. Definition transl_store (chunk: memory_chunk) (addr: addressing) @@ -747,8 +752,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) else loadind_int IR13 f.(fn_link_ofs) IR12 c) | 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 arg) => diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 25f91d23..92ae524f 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -303,6 +303,7 @@ Proof. eapply tail_nolabel_trans. 2: eapply loadind_label; eauto. unfold loadind_int; TailNoLabel. eapply transl_op_label; eauto. unfold transl_load, transl_memory_access_int, transl_memory_access_float in H. + destruct t; try discriminate. destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. unfold transl_store, transl_memory_access_int, transl_memory_access_float in H. destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. @@ -618,6 +619,12 @@ Opaque loadind. split. eapply agree_set_undef_mreg; eauto. congruence. simpl; congruence. +- (* Mload notrap1 *) + 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/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 807e069d..7ef7b776 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -1540,8 +1540,8 @@ Proof. Qed. Lemma transl_load_correct: - forall chunk addr args dst k c (rs: regset) a m v, - transl_load chunk addr args dst k = OK c -> + forall trap chunk addr args dst k c (rs: regset) a m v, + transl_load trap chunk addr args dst k = OK c -> eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> exists rs', @@ -1549,7 +1549,9 @@ Lemma transl_load_correct: /\ rs'#(preg_of dst) = v /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. Proof. - intros. destruct chunk; simpl in H. + intros. + destruct trap; try (simpl in *; discriminate). + destruct chunk; simpl in H. eapply transl_load_int_correct; eauto. eapply transl_load_int_correct; eauto. eapply transl_load_int_correct; eauto. @@ -975,6 +975,20 @@ Proof. apply Val.offset_ptr_inject; auto. 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. End EVAL_COMPAT. (** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *) @@ -1080,6 +1094,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. rewrite val_inject_list_lessdef in H. + eapply eval_addressing_inj_none with (sp1 := sp). + intros. rewrite <- val_inject_lessdef; auto. + rewrite <- val_inject_lessdef; auto. + eauto. auto. +Qed. + End EVAL_LESSDEF. (** Compatibility of the evaluation functions with memory injections. *) @@ -1132,6 +1159,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/backend/Allnontrap.v b/backend/Allnontrap.v new file mode 100644 index 00000000..acf03eca --- /dev/null +++ b/backend/Allnontrap.v @@ -0,0 +1,26 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. + + +Definition transf_ros (ros: reg + ident) : reg + ident := ros. + +Definition transf_instr (pc: node) (instr: instruction) := + match instr with + | Iload trap chunk addr args dst s => Iload NOTRAP chunk addr args dst s + | _ => 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 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. + diff --git a/backend/Allnontrapproof.v b/backend/Allnontrapproof.v new file mode 100644 index 00000000..92e5a88c --- /dev/null +++ b/backend/Allnontrapproof.v @@ -0,0 +1,215 @@ +Require Import FunInd. +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 Allnontrap. + + +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(transf_instr pc i). +Proof. + intros until i. intro Hcode. + unfold transf_function; simpl. + rewrite PTree.gmap. + unfold option_map. + rewrite Hcode. + reflexivity. +Qed. + +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 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. +- (* op *) + econstructor; split. + eapply exec_Iop with (v := v); eauto. + rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. + constructor; auto. +(* load *) +- 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. + constructor; auto. +- (* load notrap1 *) + 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. + constructor; auto. +- (* load notrap2 *) + 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. + constructor; auto. +- (* 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. + constructor; auto. +(* call *) +- econstructor; split. + eapply exec_Icall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + constructor. constructor; auto. constructor. +(* tailcall *) +- econstructor; split. + eapply exec_Itailcall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + 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. +(* cond *) +- econstructor; split. + eapply exec_Icond; eauto. + constructor; auto. +(* jumptbl *) +- econstructor; split. + eapply exec_Ijumptable; eauto. + constructor; auto. +(* return *) +- econstructor; split. + eapply exec_Ireturn; eauto. + constructor; auto. +(* internal function *) +- simpl. econstructor; split. + eapply exec_function_internal; eauto. + constructor; auto. +(* 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. +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_step. + apply senv_preserved. + eexact transf_initial_states. + eexact transf_final_states. + exact step_simulation. +Qed. + +End PRESERVATION. diff --git a/backend/Allocation.v b/backend/Allocation.v index 13e14530..6e4fcc82 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -58,7 +58,7 @@ Inductive block_shape: Type := (mv2: moves) (s: node) | BSopdead (op: operation) (args: list reg) (res: reg) (mv: moves) (s: node) - | BSload (chunk: memory_chunk) (addr: addressing) (args: list reg) (dst: reg) + | BSload (trap : trapping_mode) (chunk: memory_chunk) (addr: addressing) (args: list reg) (dst: reg) (mv1: moves) (args': list mreg) (dst': mreg) (mv2: moves) (s: node) | BSloaddead (chunk: memory_chunk) (addr: addressing) (args: list reg) (dst: reg) @@ -226,15 +226,19 @@ Definition pair_instr_block | operation_other _ _ => pair_Iop_block op args res s b end - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => let (mv1, b1) := extract_moves nil b in match b1 with - | Lload chunk' addr' args' dst' :: b2 => + | Lload trap' chunk' addr' args' dst' :: b2 => + assertion (trapping_mode_eq trap' trap); if chunk_eq chunk Mint64 && Archi.splitlong then + (* TODO: do not support non trapping split loads *) + assertion (trapping_mode_eq trap TRAP); assertion (chunk_eq chunk' Mint32); let (mv2, b3) := extract_moves nil b2 in match b3 with - | Lload chunk'' addr'' args'' dst'' :: b4 => + | Lload trap'' chunk'' addr'' args'' dst'' :: b4 => + assertion (trapping_mode_eq trap'' TRAP); let (mv3, b5) := extract_moves nil b4 in assertion (chunk_eq chunk'' Mint32); assertion (eq_addressing addr addr'); @@ -254,7 +258,7 @@ Definition pair_instr_block assertion (chunk_eq chunk chunk'); assertion (eq_addressing addr addr'); assertion (check_succ s b3); - Some(BSload chunk addr args dst mv1 args' dst' mv2 s)) + Some(BSload trap chunk addr args dst mv1 args' dst' mv2 s)) | _ => assertion (check_succ s b1); Some(BSloaddead chunk addr args dst mv1 s) @@ -1023,7 +1027,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv) | BSopdead op args res mv s => assertion (reg_unconstrained res e); track_moves env mv e - | BSload chunk addr args dst mv1 args' dst' mv2 s => + | BSload trap chunk addr args dst mv1 args' dst' mv2 s => do e1 <- track_moves env mv2 e; do e2 <- transfer_use_def args dst args' dst' (destroyed_by_load chunk addr) e1; track_moves env mv1 e2 @@ -1263,7 +1267,7 @@ Definition successors_block_shape (bsh: block_shape) : list node := | BShighlong src dst mv s => s :: nil | BSop op args res mv1 args' res' mv2 s => s :: nil | BSopdead op args res mv s => s :: nil - | BSload chunk addr args dst mv1 args' dst' mv2 s => s :: nil + | BSload trap chunk addr args dst mv1 args' dst' mv2 s => s :: nil | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => s :: nil | BSload2_1 addr args dst mv1 args' dst' mv2 s => s :: nil | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s => s :: nil diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 1804f46b..3d8fb451 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -96,44 +96,44 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr expand_block_shape (BSopdead op args res mv s) (Iop op args res s) (expand_moves mv (Lbranch s :: k)) - | ebs_load: forall chunk addr args dst mv1 args' dst' mv2 s k, + | ebs_load: forall trap chunk addr args dst mv1 args' dst' mv2 s k, wf_moves mv1 -> wf_moves mv2 -> - expand_block_shape (BSload chunk addr args dst mv1 args' dst' mv2 s) - (Iload chunk addr args dst s) + expand_block_shape (BSload trap chunk addr args dst mv1 args' dst' mv2 s) + (Iload trap chunk addr args dst s) (expand_moves mv1 - (Lload chunk addr args' dst' :: expand_moves mv2 (Lbranch s :: k))) + (Lload trap chunk addr args' dst' :: expand_moves mv2 (Lbranch s :: k))) | ebs_load2: forall addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s k, wf_moves mv1 -> wf_moves mv2 -> wf_moves mv3 -> Archi.splitlong = true -> offset_addressing addr 4 = Some addr2 -> expand_block_shape (BSload2 addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s) - (Iload Mint64 addr args dst s) + (Iload TRAP Mint64 addr args dst s) (expand_moves mv1 - (Lload Mint32 addr args1' dst1' :: + (Lload TRAP Mint32 addr args1' dst1' :: expand_moves mv2 - (Lload Mint32 addr2 args2' dst2' :: + (Lload TRAP Mint32 addr2 args2' dst2' :: expand_moves mv3 (Lbranch s :: k)))) | ebs_load2_1: forall addr args dst mv1 args' dst' mv2 s k, wf_moves mv1 -> wf_moves mv2 -> Archi.splitlong = true -> expand_block_shape (BSload2_1 addr args dst mv1 args' dst' mv2 s) - (Iload Mint64 addr args dst s) + (Iload TRAP Mint64 addr args dst s) (expand_moves mv1 - (Lload Mint32 addr args' dst' :: + (Lload TRAP Mint32 addr args' dst' :: expand_moves mv2 (Lbranch s :: k))) | ebs_load2_2: forall addr addr2 args dst mv1 args' dst' mv2 s k, wf_moves mv1 -> wf_moves mv2 -> Archi.splitlong = true -> offset_addressing addr 4 = Some addr2 -> expand_block_shape (BSload2_2 addr addr2 args dst mv1 args' dst' mv2 s) - (Iload Mint64 addr args dst s) + (Iload TRAP Mint64 addr args dst s) (expand_moves mv1 - (Lload Mint32 addr2 args' dst' :: + (Lload TRAP Mint32 addr2 args' dst' :: expand_moves mv2 (Lbranch s :: k))) - | ebs_load_dead: forall chunk addr args dst mv s k, + | ebs_load_dead: forall trap chunk addr args dst mv s k, wf_moves mv -> expand_block_shape (BSloaddead chunk addr args dst mv s) - (Iload chunk addr args dst s) + (Iload trap chunk addr args dst s) (expand_moves mv (Lbranch s :: k)) | ebs_store: forall chunk addr args src mv1 args' src' s k, wf_moves mv1 -> @@ -1970,8 +1970,8 @@ Ltac UseShape := end. Remark addressing_not_long: - forall env f addr args dst s r, - wt_instr f env (Iload Mint64 addr args dst s) -> Archi.splitlong = true -> + forall trap env f addr args dst s r, + wt_instr f env (Iload trap Mint64 addr args dst s) -> Archi.splitlong = true -> In r args -> r <> dst. Proof. intros. inv H. @@ -1981,7 +1981,7 @@ Proof. { rewrite <- H5. apply in_map; auto. } assert (C: env r = Tint). { apply A in B. rewrite B. unfold Tptr. rewrite Archi.splitlong_ptr32 by auto. auto. } - red; intros; subst r. rewrite C in H8; discriminate. + red; intros; subst r. rewrite C in H9; discriminate. Qed. (** The proof of semantic preservation is a simulation argument of the @@ -2082,8 +2082,8 @@ Proof. econstructor; eauto. eapply wt_exec_Iop; eauto. -(* load regular *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. +(* load regular TRAP *) +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. exploit transfer_use_def_satisf; eauto. intros [X Y]. exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. @@ -2100,7 +2100,7 @@ Proof. econstructor; eauto. (* load pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. @@ -2155,7 +2155,7 @@ Proof. econstructor; eauto. (* load first word of a pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. @@ -2185,7 +2185,7 @@ Proof. econstructor; eauto. (* load second word of a pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. @@ -2229,6 +2229,79 @@ Proof. econstructor; eauto. eapply wt_exec_Iload; eauto. +- (* load notrap1 *) + generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). + intro WTRS'. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit transfer_use_def_satisf; eauto. intros [X Y]. + exploit eval_addressing_lessdef_none; eauto. intro Haddr. + exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. eapply exec_Lload_notrap1. rewrite <- Haddr. + apply eval_addressing_preserved. exact symbols_preserved. eauto. + + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + +(* load notrap1 dead *) +- exploit exec_moves; eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. + eapply reg_unconstrained_satisf; eauto. + intros [enext [U V]]. + econstructor; eauto. + eapply wt_exec_Iload_notrap; eauto. + +(* load regular notrap2 *) +- generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). + intro WTRS'. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit transfer_use_def_satisf; eauto. intros [X Y]. + exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. + destruct (Mem.loadv chunk m' a') as [v' |] eqn:Hload. + { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F. + apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + } + { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. eapply exec_Lload_notrap2. rewrite <- F. + apply eval_addressing_preserved. exact symbols_preserved. assumption. + eauto. + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + } + +- (* load notrap2 dead *) + exploit exec_moves; eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. + eapply reg_unconstrained_satisf; eauto. + intros [enext [U V]]. + econstructor; eauto. + eapply wt_exec_Iload_notrap; eauto. + (* store *) - exploit exec_moves; eauto. intros [ls1 [X Y]]. exploit add_equations_lessdef; eauto. intros LD. simpl in LD. inv LD. diff --git a/backend/Bounds.v b/backend/Bounds.v index fa695234..b8c12166 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -67,7 +67,7 @@ Definition instr_within_bounds (i: instruction) := | Lgetstack sl ofs ty r => slot_within_bounds sl ofs ty /\ mreg_within_bounds r | Lsetstack r sl ofs ty => slot_within_bounds sl ofs ty | Lop op args res => mreg_within_bounds res - | Lload chunk addr args dst => mreg_within_bounds dst + | Lload trap chunk addr args dst => mreg_within_bounds dst | Lcall sig ros => size_arguments sig <= bound_outgoing b | Lbuiltin ef args res => (forall r, In r (params_of_builtin_res res) \/ In r (destroyed_by_builtin ef) -> mreg_within_bounds r) @@ -104,7 +104,7 @@ Definition record_regs_of_instr (u: RegSet.t) (i: instruction) : RegSet.t := | Lgetstack sl ofs ty r => record_reg u r | Lsetstack r sl ofs ty => record_reg u r | Lop op args res => record_reg u res - | Lload chunk addr args dst => record_reg u dst + | Lload trap chunk addr args dst => record_reg u dst | Lstore chunk addr args src => u | Lcall sig ros => u | Ltailcall sig ros => u @@ -280,7 +280,7 @@ Definition defined_by_instr (r': mreg) (i: instruction) := match i with | Lgetstack sl ofs ty r => r' = r | Lop op args res => r' = res - | Lload chunk addr args dst => r' = dst + | Lload trap chunk addr args dst => r' = dst | Lbuiltin ef args res => In r' (params_of_builtin_res res) \/ In r' (destroyed_by_builtin ef) | _ => False end. diff --git a/backend/CSE.v b/backend/CSE.v index ecfa1f9e..2827161d 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -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 chunk addr args dst s => - add_load before dst 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 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 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 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 9b1243c8..34ec0118 100644 --- a/backend/CSEdomain.v +++ b/backend/CSEdomain.v @@ -43,7 +43,7 @@ Definition eq_list_valnum: forall (x y: list valnum), {x=y}+{x<>y} := list_eq_de Definition eq_rhs (x y: rhs) : {x=y}+{x<>y}. Proof. - generalize chunk_eq eq_operation eq_addressing eq_valnum eq_list_valnum. + generalize trapping_mode_eq chunk_eq eq_operation eq_addressing eq_valnum eq_list_valnum. decide equality. Defined. @@ -109,7 +109,16 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem): | 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 chunk addr vl) v. + 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) + | load_notrap2_eval_to: forall chunk addr vl a, + 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) *). Inductive equation_holds (valu: valuation) (ge: genv) (sp: val) (m: mem): equation -> Prop := diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 03c7ecfc..5bbb7508 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -71,7 +71,11 @@ Lemma rhs_eval_to_exten: Proof. intros. inv H; simpl in *. - constructor. rewrite valnums_val_exten by assumption. auto. -- econstructor; eauto. rewrite valnums_val_exten by assumption. auto. +- eapply load_eval_to; eauto. rewrite valnums_val_exten by assumption. auto. +(* +- apply load_notrap1_eval_to; auto. rewrite valnums_val_exten by assumption. assumption. +- eapply load_notrap2_eval_to; eauto. rewrite valnums_val_exten by assumption. assumption. +*) Qed. Lemma equation_holds_exten: @@ -393,6 +397,39 @@ Proof. + intros. apply Regmap.gso; auto. Qed. +(* +Lemma add_load_holds_none1: + forall valu1 ge sp rs m n addr (args: list reg) chunk dst, + numbering_holds valu1 ge sp rs m n -> + eval_addressing ge sp addr rs##args = None -> + exists valu2, numbering_holds valu2 ge sp (rs#dst <- (default_notrap_load_value chunk)) m (add_load n dst chunk addr args). +Proof. + unfold add_load; intros. + destruct (valnum_regs n args) as [n1 vl] eqn:VN. + exploit valnum_regs_holds; eauto. + intros (valu2 & A & B & C & D & E). + eapply add_rhs_holds; eauto. ++ rewrite Regmap.gss; auto. eapply load_notrap1_eval_to. rewrite <- B; eauto. ++ intros. apply Regmap.gso; auto. +Qed. + +Lemma add_load_holds_none2: + forall valu1 ge sp rs m n addr (args: list reg) a chunk dst, + numbering_holds valu1 ge sp rs m n -> + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = None -> + exists valu2, numbering_holds valu2 ge sp (rs#dst <- (default_notrap_load_value chunk)) m (add_load n dst NOTRAP chunk addr args). +Proof. + unfold add_load; intros. + destruct (valnum_regs n args) as [n1 vl] eqn:VN. + exploit valnum_regs_holds; eauto. + intros (valu2 & A & B & C & D & E). + eapply add_rhs_holds; eauto. ++ rewrite Regmap.gss; auto. eapply load_notrap2_eval_to. rewrite <- B; eauto. assumption. ++ intros. apply Regmap.gso; auto. +Qed. + *) + Lemma set_unknown_holds: forall valu ge sp rs m n r v, numbering_holds valu ge sp rs m n -> @@ -456,8 +493,8 @@ Lemma kill_all_loads_hold: Proof. intros. eapply kill_equations_hold; eauto. unfold filter_loads; intros. inv H1. - constructor. rewrite <- H2. apply op_depends_on_memory_correct; auto. - discriminate. + 1: constructor; rewrite <- H2; apply op_depends_on_memory_correct; auto. + all: discriminate. Qed. Lemma kill_loads_after_store_holds: @@ -486,6 +523,20 @@ Proof. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va. +(* +- eapply load_notrap1_eval_to; assumption. +- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate. + eapply load_notrap2_eval_to; eauto. + rewrite <- H9. + destruct a; simpl in H1; try discriminate. + destruct a0; simpl in H9; try discriminate; simpl; trivial. + rewrite negb_false_iff in H6. unfold aaddressing in H6. + eapply Mem.load_store_other. eauto. + eapply pdisjoint_sound; eauto. + apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. + erewrite <- regs_valnums_sound by eauto. eauto with va. + apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va. +*) Qed. Lemma store_normalized_range_sound: @@ -562,6 +613,19 @@ Proof. unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. auto. +(* +- eapply load_notrap1_eval_to; assumption. +- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate. + eapply load_notrap2_eval_to; eauto. rewrite <- H11. + destruct a; simpl in H10; try discriminate; simpl; trivial. + rewrite negb_false_iff in H8. + eapply Mem.load_storebytes_other. eauto. + rewrite H6. rewrite Z2Nat.id by omega. + eapply pdisjoint_sound. eauto. + unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. + erewrite <- regs_valnums_sound by eauto. eauto with va. + auto. +*) Qed. Lemma load_memcpy: @@ -1034,6 +1098,10 @@ Proof. 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). + destruct trap. + + (* TRAP *) + { destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?. + (* replaced by move *) exploit find_rhs_sound; eauto. intros (v' & EV & LD). @@ -1063,7 +1131,103 @@ Proof. unfold transfer; rewrite H. eapply add_load_holds; eauto. apply set_reg_lessdef; auto. + } + + (* NOTRAP *) + { + 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]]. + + assert ( + exists v' : val, + Mem.loadv chunk m' a' = Some v' /\ Val.lessdef v v') as Hload' by + (apply Mem.loadv_extends with (m1 := m) (addr1 := a); assumption). + destruct Hload' as [v' [Hv'1 Hv'2]]. + + econstructor. split. + eapply exec_Iload; eauto. + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; 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; assumption. + } + +- (* 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. + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; 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. + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; 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]. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index e92be2b4..84ca403e 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -255,6 +255,18 @@ Proof. left; econstructor; split. econstructor; eauto. econstructor; eauto with coqlib. +(* Lload notrap1 *) + assert (eval_addressing tge sp addr (LTL.reglist rs args) = None). + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. + left; econstructor; split. + eapply exec_Lload_notrap1; eauto. + econstructor; eauto with coqlib. +(* Lload notrap2 *) + assert (eval_addressing tge sp addr (LTL.reglist rs args) = Some a). + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. + left; econstructor; split. + eapply exec_Lload_notrap2; eauto. + econstructor; eauto with coqlib. (* Lstore *) assert (eval_addressing tge sp addr (LTL.reglist rs args) = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. diff --git a/backend/Constprop.v b/backend/Constprop.v index 4aab7677..eda41b39 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -181,7 +181,7 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) let (op', args') := op_strength_reduction op args aargs in Iop op' args' res s' end - | Iload chunk addr args dst s => + | Iload TRAP chunk addr args dst s => let aargs := aregs ae args in let a := ValueDomain.loadv chunk rm am (eval_static_addressing addr aargs) in match const_for_result a with @@ -189,7 +189,7 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) Iop cop nil dst s | None => let (addr', args') := addr_strength_reduction addr args aargs in - Iload chunk addr' args' dst s + Iload TRAP chunk addr' args' dst s end | Istore chunk addr args src s => let aargs := aregs ae args in diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index a5d08a0f..63cfee24 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -406,6 +406,8 @@ Proof. assert (VM1: vmatch bc a aa) by (eapply eval_static_addressing_sound; eauto with va). set (av := loadv chunk (romem_for cu) am aa). assert (VM2: vmatch bc v av) by (eapply loadv_sound; eauto). + destruct trap. + { destruct (const_for_result av) as [cop|] eqn:?; intros. + (* constant-propagated *) exploit const_for_result_correct; eauto. intros (v' & A & B). @@ -431,6 +433,59 @@ Proof. left; econstructor; econstructor; split. eapply exec_Iload; eauto. eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + } + { + assert (exists v2 : val, + eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + destruct Hexist2 as [v2 [Heval2 Hlessdef2]]. + destruct (Mem.loadv_extends chunk m m' a v2 v MEM H1 Hlessdef2) as [vX [Hvx1 Hvx2]]. + left; econstructor; econstructor; split. + eapply exec_Iload with (a := v2); eauto. + try (erewrite eval_addressing_preserved with (ge1:=ge); auto; + exact symbols_preserved). + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + + } + +- (* Iload notrap1 *) + rename pc'0 into pc. TransfInstr. + assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = None). + rewrite eval_addressing_preserved with (ge1 := ge); eauto. + apply eval_addressing_lessdef_none with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + exact symbols_preserved. + + left; econstructor; econstructor; split. + eapply exec_Iload_notrap1; eauto. + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + +- (* Iload notrap2 *) + rename pc'0 into pc. TransfInstr. + assert (exists v2 : val, + eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + destruct Hexist2 as [a' [Heval' Hlessdef']]. + destruct (Mem.loadv chunk m' a') eqn:Hload'. + { + left; econstructor; econstructor; split. + eapply exec_Iload; eauto. + + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + } + { + left; econstructor; econstructor; split. + eapply exec_Iload_notrap2; eauto. + + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + } - (* Istore *) rename pc'0 into pc. TransfInstr. diff --git a/backend/Deadcode.v b/backend/Deadcode.v index 2286876e..1f208a91 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -123,7 +123,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) if is_dead nres then after else if is_int_zero nres then (kill res ne, nm) else (add_needs args (needs_of_operation op nres) (kill res ne), nm) - | Some (Iload chunk addr args dst s) => + | Some (Iload trap chunk addr args dst s) => let ndst := nreg ne dst in if is_dead ndst then after else if is_int_zero ndst then (kill dst ne, nm) @@ -175,7 +175,7 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t) end else instr - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => let ndst := nreg (fst an!!pc) dst in if is_dead ndst then Inop s diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 2edc0395..6919fe78 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -829,6 +829,83 @@ Ltac UseTransfer := apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. +- (* load notrap1 *) + TransfInstr; UseTransfer. + destruct (is_dead (nreg ne dst)) eqn:DEAD; + [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO]; + simpl in *. ++ (* dead instruction, turned into a nop *) + econstructor; split. + eapply exec_Inop; eauto. + eapply match_succ_states; eauto. simpl; auto. + apply eagree_update_dead; auto with na. ++ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) + econstructor; split. + eapply exec_Iop with (v := Vint Int.zero); eauto. + eapply match_succ_states; eauto. simpl; auto. + apply eagree_update; auto. + rewrite is_int_zero_sound by auto. + unfold default_notrap_load_value. + constructor. ++ (* preserved *) + exploit eval_addressing_lessdef_none. eapply add_needs_all_lessdef; eauto. eassumption. + intro Hnone'. + assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr te ## args = None) as Hnone2'. + erewrite eval_addressing_preserved with (ge1 := ge). + assumption. + exact symbols_preserved. + + econstructor; split. + eapply exec_Iload_notrap1; eauto. + eapply match_succ_states; eauto. simpl; auto. + apply eagree_update; eauto 2 with na. + eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. + +- (* load notrap2 *) + TransfInstr; UseTransfer. + + destruct (is_dead (nreg ne dst)) eqn:DEAD; + [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO]; + simpl in *. ++ (* dead instruction, turned into a nop *) + econstructor; split. + eapply exec_Inop; eauto. + eapply match_succ_states; eauto. simpl; auto. + apply eagree_update_dead; auto with na. ++ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) + econstructor; split. + eapply exec_Iop with (v := Vint Int.zero); eauto. + eapply match_succ_states; eauto. simpl; auto. + apply eagree_update; auto. + rewrite is_int_zero_sound by auto. + unfold default_notrap_load_value. + constructor. ++ (* preserved *) + exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto. + intros (ta & U & V). + destruct (Mem.loadv chunk tm ta) eqn:Hchunk2. + { + econstructor; split. + eapply exec_Iload. eauto. + erewrite eval_addressing_preserved with (ge1 := ge). + eassumption. + exact symbols_preserved. + eassumption. + eapply match_succ_states; eauto. simpl; auto. + apply eagree_update; eauto 2 with na. + eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. + } + { + econstructor; split. + eapply exec_Iload_notrap2. eauto. + erewrite eval_addressing_preserved with (ge1 := ge). + eassumption. + exact symbols_preserved. + eassumption. + eapply match_succ_states; eauto. simpl; auto. + apply eagree_update; eauto 2 with na. + eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. + } - (* store *) TransfInstr; UseTransfer. destruct (nmem_contains nm (aaddressing (vanalyze cu f) # pc addr args) diff --git a/backend/Debugvar.v b/backend/Debugvar.v index 1f361030..56908855 100644 --- a/backend/Debugvar.v +++ b/backend/Debugvar.v @@ -233,7 +233,7 @@ Definition transfer (lm: labelmap) (before: option avail) (i: instruction): (lm, Some (kill (S sl ofs ty) s)) | Lop op args dst => (lm, Some (kill (R dst) s)) - | Lload chunk addr args dst => + | Lload trap chunk addr args dst => (lm, Some (kill (R dst) s)) | Lstore chunk addr args src => (lm, before) diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v index d31c63ec..95020637 100644 --- a/backend/Debugvarproof.v +++ b/backend/Debugvarproof.v @@ -449,6 +449,22 @@ Proof. eauto. eauto. apply eval_add_delta_ranges. traceEq. constructor; auto. +- (* load notrap1 *) + econstructor; split. + eapply plus_left. + eapply exec_Lload_notrap1. + rewrite <- H; apply eval_addressing_preserved; exact symbols_preserved. + eauto. eauto. + apply eval_add_delta_ranges. traceEq. + constructor; auto. +- (* load notrap2 *) + econstructor; split. + eapply plus_left. + eapply exec_Lload_notrap2. + rewrite <- H; apply eval_addressing_preserved; exact symbols_preserved. + eauto. eauto. + apply eval_add_delta_ranges. traceEq. + constructor; auto. - (* store *) econstructor; split. eapply plus_left. diff --git a/backend/Inlining.v b/backend/Inlining.v index f7ee4166..9cf535b9 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -364,9 +364,9 @@ Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit := | Iop op args res s => set_instr (spc ctx pc) (Iop (sop ctx op) (sregs ctx args) (sreg ctx res) (spc ctx s)) - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => set_instr (spc ctx pc) - (Iload chunk (saddr ctx addr) (sregs ctx args) (sreg ctx dst) (spc ctx s)) + (Iload trap chunk (saddr ctx addr) (sregs ctx args) (sreg ctx dst) (spc ctx s)) | Istore chunk addr args src s => set_instr (spc ctx pc) (Istore chunk (saddr ctx addr) (sregs ctx args) (sreg ctx src) (spc ctx s)) diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index 842e0c93..609b2637 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -57,7 +57,7 @@ let used_in_globvar io gv = let fun_inline_analysis id io fn = let inst io nid = function | Iop (op, args, dest, succ) -> used_id io (globals_operation op) - | Iload (chunk, addr, args, dest, succ) + | Iload (_, chunk, addr, args, dest, succ) | Istore (chunk, addr, args, dest, succ) -> used_id io (globals_addressing addr) | Ibuiltin (ef, args, dest, succ) -> used_id io (globals_of_builtin_args args) | Icall (_, Coq_inr cid, _, _, _) diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 181f40bf..b60c1cb7 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -929,6 +929,15 @@ Proof. intros. inv H. eauto. Qed. +Lemma eval_addressing_none: + forall sp' ctx addr rs, + eval_addressing ge (Vptr sp' (Ptrofs.repr (dstk ctx))) addr rs = None -> + eval_addressing ge (Vptr sp' Ptrofs.zero) (saddr ctx addr) rs = None. +Proof. + intros until rs; intro Heval. + destruct addr; destruct rs as [| r0 rs1]; simpl in *; trivial; discriminate. +Qed. + Theorem step_simulation: forall S1 t S2, step ge S1 t S2 -> @@ -976,6 +985,51 @@ Proof. apply match_stacks_inside_set_reg; auto. apply agree_set_reg; auto. +- (* load notrap1 *) + exploit tr_funbody_inv; eauto. intros TR; inv TR. + left; econstructor; split. + eapply plus_one. eapply exec_Iload_notrap1. eassumption. + rewrite eval_addressing_preserved with (ge1:=ge) (ge2:=tge). + exploit eval_addressing_inj_none. + 4: eassumption. + intros. eapply symbol_address_inject. + eapply match_stacks_inside_globals; eauto. + eauto. + instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. + rewrite Ptrofs.add_zero_l. + apply eval_addressing_none. + exact symbols_preserved. + econstructor; eauto. + apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. + +- (* load notrap2 *) + exploit tr_funbody_inv; eauto. intros TR; inv TR. + + exploit eval_addressing_inject. + eapply match_stacks_inside_globals; eauto. + eexact SP. + instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. + eauto. + fold (saddr ctx addr). intros [a' [P Q]]. + + destruct (Mem.loadv chunk m' a') eqn:Hload'. + + left; econstructor; split. + eapply plus_one. + eapply exec_Iload; eauto. + try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved). + econstructor; eauto. + apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. + + + left; econstructor; split. + eapply plus_one. + eapply exec_Iload_notrap2; eauto. + try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved). + econstructor; eauto. + apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. + - (* store *) exploit tr_funbody_inv; eauto. intros TR; inv TR. exploit eval_addressing_inject. diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index c345c942..e20fb373 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -270,10 +270,10 @@ Inductive tr_instr: context -> node -> instruction -> code -> Prop := Ple res ctx.(mreg) -> c!(spc ctx pc) = Some (Iop (sop ctx op) (sregs ctx args) (sreg ctx res) (spc ctx s)) -> tr_instr ctx pc (Iop op args res s) c - | tr_load: forall ctx pc c chunk addr args res s, + | tr_load: forall ctx pc c trap chunk addr args res s, Ple res ctx.(mreg) -> - c!(spc ctx pc) = Some (Iload chunk (saddr ctx addr) (sregs ctx args) (sreg ctx res) (spc ctx s)) -> - tr_instr ctx pc (Iload chunk addr args res s) c + c!(spc ctx pc) = Some (Iload trap chunk (saddr ctx addr) (sregs ctx args) (sreg ctx res) (spc ctx s)) -> + tr_instr ctx pc (Iload trap chunk addr args res s) c | tr_store: forall ctx pc c chunk addr args src s, c!(spc ctx pc) = Some (Istore chunk (saddr ctx addr) (sregs ctx args) (sreg ctx src) (spc ctx s)) -> tr_instr ctx pc (Istore chunk addr args src s) c diff --git a/backend/LTL.v b/backend/LTL.v index 5e7eec8c..ee8b4826 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -29,7 +29,7 @@ Definition node := positive. Inductive instruction: Type := | Lop (op: operation) (args: list mreg) (res: mreg) - | Lload (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) + | Lload (trap : trapping_mode) (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) | Lgetstack (sl: slot) (ofs: Z) (ty: typ) (dst: mreg) | Lsetstack (src: mreg) (sl: slot) (ofs: Z) (ty: typ) | Lstore (chunk: memory_chunk) (addr: addressing) (args: list mreg) (src: mreg) @@ -209,11 +209,24 @@ Inductive step: state -> trace -> state -> Prop := rs' = Locmap.set (R res) v (undef_regs (destroyed_by_op op) rs) -> step (Block s f sp (Lop op args res :: bb) rs m) E0 (Block s f sp bb rs' m) - | exec_Lload: forall s f sp chunk addr args dst bb rs m a v rs', + | exec_Lload: forall s f sp trap chunk addr args dst bb rs m a v rs', eval_addressing ge sp addr (reglist rs args) = Some a -> Mem.loadv chunk m a = Some v -> rs' = Locmap.set (R dst) v (undef_regs (destroyed_by_load chunk addr) rs) -> - step (Block s f sp (Lload chunk addr args dst :: bb) rs m) + step (Block s f sp (Lload trap chunk addr args dst :: bb) rs m) + E0 (Block s f sp bb rs' m) + | exec_Lload_notrap1: forall s f sp chunk addr args dst bb rs m rs', + eval_addressing ge sp addr (reglist rs args) = None -> + rs' = Locmap.set (R dst) (default_notrap_load_value chunk) + (undef_regs (destroyed_by_load chunk addr) rs) -> + step (Block s f sp (Lload NOTRAP chunk addr args dst :: bb) rs m) + E0 (Block s f sp bb rs' m) + | exec_Lload_notrap2: forall s f sp chunk addr args dst bb rs m a rs', + eval_addressing ge sp addr (reglist rs args) = Some a -> + Mem.loadv chunk m a = None -> + rs' = Locmap.set (R dst) (default_notrap_load_value chunk) + (undef_regs (destroyed_by_load chunk addr) rs) -> + step (Block s f sp (Lload NOTRAP chunk addr args dst :: bb) rs m) E0 (Block s f sp bb rs' m) | exec_Lgetstack: forall s f sp sl ofs ty dst bb rs m rs', rs' = Locmap.set (R dst) (rs (S sl ofs ty)) (undef_regs (destroyed_by_getstack sl) rs) -> diff --git a/backend/Linear.v b/backend/Linear.v index 447c6ba6..1443f795 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -28,7 +28,7 @@ Inductive instruction: Type := | Lgetstack: slot -> Z -> typ -> mreg -> instruction | Lsetstack: mreg -> slot -> Z -> typ -> instruction | Lop: operation -> list mreg -> mreg -> instruction - | Lload: memory_chunk -> addressing -> list mreg -> mreg -> instruction + | Lload: trapping_mode -> memory_chunk -> addressing -> list mreg -> mreg -> instruction | Lstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Lcall: signature -> mreg + ident -> instruction | Ltailcall: signature -> mreg + ident -> instruction @@ -160,11 +160,28 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Lop op args res :: b) rs m) E0 (State s f sp b rs' m) | exec_Lload: - forall s f sp chunk addr args dst b rs m a v rs', + forall s f sp trap chunk addr args dst b rs m a v rs', eval_addressing ge sp addr (reglist rs args) = Some a -> Mem.loadv chunk m a = Some v -> rs' = Locmap.set (R dst) v (undef_regs (destroyed_by_load chunk addr) rs) -> - step (State s f sp (Lload chunk addr args dst :: b) rs m) + step (State s f sp (Lload trap chunk addr args dst :: b) rs m) + E0 (State s f sp b rs' m) + | exec_Lload_notrap1: + forall s f sp chunk addr args dst b rs m rs', + eval_addressing ge sp addr (reglist rs args) = None -> + rs' = Locmap.set (R dst) + (default_notrap_load_value chunk) + (undef_regs (destroyed_by_load chunk addr) rs) -> + step (State s f sp (Lload NOTRAP chunk addr args dst :: b) rs m) + E0 (State s f sp b rs' m) + | exec_Lload_notrap2: + forall s f sp chunk addr args dst b rs m a rs', + eval_addressing ge sp addr (reglist rs args) = Some a -> + Mem.loadv chunk m a = None -> + rs' = Locmap.set (R dst) + (default_notrap_load_value chunk) + (undef_regs (destroyed_by_load chunk addr) rs) -> + step (State s f sp (Lload NOTRAP chunk addr args dst :: b) rs m) E0 (State s f sp b rs' m) | exec_Lstore: forall s f sp chunk addr args src b rs m m' a rs', diff --git a/backend/Linearize.v b/backend/Linearize.v index 2cfa4d3c..4216958c 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -163,8 +163,8 @@ Fixpoint linearize_block (b: LTL.bblock) (k: code) : code := | nil => k | LTL.Lop op args res :: b' => Lop op args res :: linearize_block b' k - | LTL.Lload chunk addr args dst :: b' => - Lload chunk addr args dst :: linearize_block b' k + | LTL.Lload trap chunk addr args dst :: b' => + Lload trap chunk addr args dst :: linearize_block b' k | LTL.Lgetstack sl ofs ty dst :: b' => Lgetstack sl ofs ty dst :: linearize_block b' k | LTL.Lsetstack src sl ofs ty :: b' => diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 10a3d8b2..18dc52a5 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -585,45 +585,61 @@ Proof. intros; eapply reachable_successors; eauto. eapply is_tail_lin_block; eauto. eapply is_tail_find_label; eauto. - (* Lop *) +- (* Lop *) left; econstructor; split. simpl. apply plus_one. econstructor; eauto. instantiate (1 := v); rewrite <- H; apply eval_operation_preserved. exact symbols_preserved. econstructor; eauto. - (* Lload *) +- (* Lload *) left; econstructor; split. simpl. - apply plus_one. econstructor. + apply plus_one. eapply exec_Lload. instantiate (1 := a). rewrite <- H; apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. econstructor; eauto. - (* Lgetstack *) +- (* Lload notrap1 *) + left; econstructor; split. simpl. + apply plus_one. eapply exec_Lload_notrap1. + rewrite <- H. + apply eval_addressing_preserved. + exact symbols_preserved. eauto. + econstructor; eauto. + +- (* Lload notrap2 *) + left; econstructor; split. simpl. + apply plus_one. eapply exec_Lload_notrap2. + rewrite <- H. + apply eval_addressing_preserved. + exact symbols_preserved. eauto. eauto. + econstructor; eauto. + +- (* Lgetstack *) left; econstructor; split. simpl. apply plus_one. econstructor; eauto. econstructor; eauto. - (* Lsetstack *) +- (* Lsetstack *) left; econstructor; split. simpl. apply plus_one. econstructor; eauto. econstructor; eauto. - (* Lstore *) +- (* Lstore *) left; econstructor; split. simpl. apply plus_one. econstructor. instantiate (1 := a). rewrite <- H; apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. econstructor; eauto. - (* Lcall *) +- (* Lcall *) exploit find_function_translated; eauto. intros [tfd [A B]]. left; econstructor; split. simpl. apply plus_one. econstructor; eauto. symmetry; eapply sig_preserved; eauto. econstructor; eauto. constructor; auto. econstructor; eauto. - (* Ltailcall *) +- (* Ltailcall *) exploit find_function_translated; eauto. intros [tfd [A B]]. left; econstructor; split. simpl. apply plus_one. econstructor; eauto. @@ -633,18 +649,18 @@ Proof. rewrite (match_parent_locset _ _ STACKS). econstructor; eauto. - (* Lbuiltin *) +- (* Lbuiltin *) left; econstructor; split. simpl. apply plus_one. eapply exec_Lbuiltin; eauto. eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. - (* Lbranch *) +- (* Lbranch *) assert ((reachable f)!!pc = true). apply REACH; simpl; auto. right; split. simpl; omega. split. auto. simpl. econstructor; eauto. - (* Lcond *) +- (* Lcond *) assert (REACH1: (reachable f)!!pc1 = true) by (apply REACH; simpl; auto). assert (REACH2: (reachable f)!!pc2 = true) by (apply REACH; simpl; auto). simpl linearize_block. @@ -670,18 +686,18 @@ Proof. apply plus_one. eapply exec_Lcond_false. eauto. eauto. econstructor; eauto. - (* Ljumptable *) +- (* Ljumptable *) assert (REACH': (reachable f)!!pc = true). apply REACH. simpl. eapply list_nth_z_in; eauto. right; split. simpl; omega. split. auto. econstructor; eauto. - (* Lreturn *) +- (* Lreturn *) left; econstructor; split. simpl. apply plus_one. econstructor; eauto. rewrite (stacksize_preserved _ _ TRF). eauto. rewrite (match_parent_locset _ _ STACKS). econstructor; eauto. - (* internal functions *) +- (* internal functions *) assert (REACH: (reachable f)!!(LTL.fn_entrypoint f) = true). apply reachable_entrypoint. monadInv H7. @@ -691,13 +707,13 @@ Proof. generalize EQ; intro EQ'; monadInv EQ'. simpl. econstructor; eauto. simpl. eapply is_tail_add_branch. constructor. - (* external function *) +- (* external function *) monadInv H8. left; econstructor; split. apply plus_one. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. - (* return *) +- (* return *) inv H3. inv H1. left; econstructor; split. apply plus_one. econstructor. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 1fe23a9d..da66b6ff 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -76,7 +76,7 @@ Definition wt_instr (i: instruction) : bool := let (targs, tres) := type_of_operation op in subtype tres (mreg_type res) end - | Lload chunk addr args dst => + | Lload trap chunk addr args dst => subtype (type_of_chunk chunk) (mreg_type dst) | Ltailcall sg ros => zeq (size_arguments sg) 0 @@ -332,6 +332,20 @@ Local Opaque mreg_type. apply wt_setreg. eapply Val.has_subtype; eauto. destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto. apply wt_undef_regs; auto. +- (* load notrap1 *) + simpl in *; InvBooleans. + econstructor; eauto. + apply wt_setreg. eapply Val.has_subtype; eauto. + unfold default_notrap_load_value. + constructor. + apply wt_undef_regs; auto. +- (* load notrap2 *) + simpl in *; InvBooleans. + econstructor; eauto. + apply wt_setreg. eapply Val.has_subtype; eauto. + unfold default_notrap_load_value. + constructor. + apply wt_undef_regs; auto. - (* store *) simpl in *; InvBooleans. econstructor. eauto. eauto. eauto. diff --git a/backend/Liveness.v b/backend/Liveness.v index 16533158..afe11ae6 100644 --- a/backend/Liveness.v +++ b/backend/Liveness.v @@ -79,7 +79,7 @@ Definition transfer reg_list_live args (reg_dead res after) else after - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => if Regset.mem dst after then reg_list_live args (reg_dead dst after) else diff --git a/backend/Mach.v b/backend/Mach.v index 9fdee9eb..1c6fdb18 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -56,7 +56,7 @@ Inductive instruction: Type := | Msetstack: mreg -> ptrofs -> typ -> instruction | Mgetparam: ptrofs -> typ -> mreg -> instruction | Mop: operation -> list mreg -> mreg -> instruction - | Mload: memory_chunk -> addressing -> list mreg -> mreg -> instruction + | Mload: trapping_mode -> memory_chunk -> addressing -> list mreg -> mreg -> instruction | Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Mcall: signature -> mreg + ident -> instruction | Mtailcall: signature -> mreg + ident -> instruction @@ -321,11 +321,24 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Mop op args res :: c) rs m) E0 (State s f sp c rs' m) | exec_Mload: - forall s f sp chunk addr args dst c rs m a v rs', + forall s f sp trap chunk addr args dst c rs m a v rs', eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- v) -> - step (State s f sp (Mload chunk addr args dst :: c) rs m) + step (State s f sp (Mload trap chunk addr args dst :: c) rs m) + E0 (State s f sp c rs' m) + | exec_Mload_notrap1: + forall s f sp chunk addr args dst c rs m rs', + eval_addressing ge sp addr rs##args = None -> + rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) -> + step (State s f sp (Mload NOTRAP chunk addr args dst :: c) rs m) + E0 (State s f sp c rs' m) + | exec_Mload_notrap2: + forall s f sp chunk addr args dst c rs m a rs', + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = None -> + rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) -> + step (State s f sp (Mload NOTRAP chunk addr args dst :: c) rs m) E0 (State s f sp c rs' m) | exec_Mstore: forall s f sp chunk addr args src c rs m m' a rs', diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index 1c449e74..b309a9f2 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -61,9 +61,10 @@ let print_succ pp s dfl = let print_instruction pp succ = function | Lop(op, args, res) -> fprintf pp "%a = %a" mreg res (print_operation mreg) (op, args) - | Lload(chunk, addr, args, dst) -> - fprintf pp "%a = %s[%a]" - mreg dst (name_of_chunk chunk) (print_addressing mreg) (addr, args) + | Lload(trap,chunk, addr, args, dst) -> + fprintf pp "%a = %s[%a]%a" + mreg dst (name_of_chunk chunk) (print_addressing mreg) (addr, args) + print_trapping_mode trap | Lgetstack(sl, ofs, ty, dst) -> fprintf pp "%a = %a" mreg dst slot (sl, ofs, ty) | Lsetstack(src, sl, ofs, ty) -> diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index 517f3037..70e65832 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -48,10 +48,11 @@ let print_instruction pp i = | Mop(op, args, res) -> fprintf pp "\t%a = %a\n" reg res (PrintOp.print_operation reg) (op, args) - | Mload(chunk, addr, args, dst) -> - fprintf pp "\t%a = %s[%a]\n" + | Mload(trap, chunk, addr, args, dst) -> + fprintf pp "\t%a = %s[%a]%a\n" reg dst (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) + print_trapping_mode trap | Mstore(chunk, addr, args, src) -> fprintf pp "\t%s[%a] = %a\n" (name_of_chunk chunk) diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 841540b6..c25773e5 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -50,10 +50,11 @@ let print_instruction pp (pc, i) = fprintf pp "%a = %a\n" reg res (PrintOp.print_operation reg) (op, args); print_succ pp s (pc - 1) - | Iload(chunk, addr, args, dst, s) -> - fprintf pp "%a = %s[%a]\n" + | Iload(trap, chunk, addr, args, dst, s) -> + fprintf pp "%a = %s[%a]%a\n" reg dst (name_of_chunk chunk) - (PrintOp.print_addressing reg) (addr, args); + (PrintOp.print_addressing reg) (addr, args) + print_trapping_mode trap; print_succ pp s (pc - 1) | Istore(chunk, addr, args, src, s) -> fprintf pp "%s[%a] = %a\n" diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml index 6432682a..1c7655fb 100644 --- a/backend/PrintXTL.ml +++ b/backend/PrintXTL.ml @@ -86,9 +86,10 @@ let print_instruction pp succ = function fprintf pp "(%a) = (%a) using %a, %a" vars dsts vars srcs var t1 var t2 | Xop(op, args, res) -> fprintf pp "%a = %a" var res (print_operation var) (op, args) - | Xload(chunk, addr, args, dst) -> - fprintf pp "%a = %s[%a]" - var dst (name_of_chunk chunk) (print_addressing var) (addr, args) + | Xload(trap, chunk, addr, args, dst) -> + fprintf pp "%a = %s[%a]%a" + var dst (name_of_chunk chunk) (print_addressing var) (addr, args) + print_trapping_mode trap | Xstore(chunk, addr, args, src) -> fprintf pp "%s[%a] = %a" (name_of_chunk chunk) (print_addressing var) (addr, args) var src diff --git a/backend/RTL.v b/backend/RTL.v index 9599a24a..29a49311 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -43,11 +43,12 @@ Inductive instruction: Type := (** [Iop op args dest succ] performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest], and branches to [succ]. *) - | Iload: memory_chunk -> addressing -> list reg -> reg -> node -> instruction - (** [Iload chunk addr args dest succ] loads a [chunk] quantity from + | Iload: trapping_mode -> memory_chunk -> addressing -> list reg -> reg -> node -> instruction + (** [Iload trap chunk addr args dest succ] loads a [chunk] quantity from the address determined by the addressing mode [addr] and the values of the [args] registers, stores the quantity just read - into [dest], and branches to [succ]. *) + into [dest], and branches to [succ]. + If trap=NOTRAP, then failures lead to a default value written to [dest]. *) | Istore: memory_chunk -> addressing -> list reg -> reg -> node -> instruction (** [Istore chunk addr args src succ] stores the value of register [src] in the [chunk] quantity at the @@ -212,12 +213,25 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp pc rs m) E0 (State s f sp pc' (rs#res <- v) m) | exec_Iload: - forall s f sp pc rs m chunk addr args dst pc' a v, - (fn_code f)!pc = Some(Iload chunk addr args dst pc') -> + forall s f sp pc rs m trap chunk addr args dst pc' a v, + (fn_code f)!pc = Some(Iload trap chunk addr args dst pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> step (State s f sp pc rs m) E0 (State s f sp pc' (rs#dst <- v) m) + | exec_Iload_notrap1: + forall s f sp pc rs m chunk addr args dst pc', + (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') -> + eval_addressing ge sp addr rs##args = None -> + step (State s f sp pc rs m) + E0 (State s f sp pc' (rs#dst <- (default_notrap_load_value chunk)) m) + | exec_Iload_notrap2: + forall s f sp pc rs m chunk addr args dst pc' a, + (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') -> + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = None-> + step (State s f sp pc rs m) + E0 (State s f sp pc' (rs#dst <- (default_notrap_load_value chunk)) m) | exec_Istore: forall s f sp pc rs m chunk addr args src pc' a m', (fn_code f)!pc = Some(Istore chunk addr args src pc') -> @@ -299,8 +313,8 @@ Proof. Qed. Lemma exec_Iload': - forall s f sp pc rs m chunk addr args dst pc' rs' a v, - (fn_code f)!pc = Some(Iload chunk addr args dst pc') -> + forall s f sp pc rs m trap chunk addr args dst pc' rs' a v, + (fn_code f)!pc = Some(Iload trap chunk addr args dst pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> rs' = (rs#dst <- v) -> @@ -384,7 +398,7 @@ Definition successors_instr (i: instruction) : list node := match i with | Inop s => s :: nil | Iop op args res s => s :: nil - | Iload chunk addr args dst s => s :: nil + | Iload trap chunk addr args dst s => s :: nil | Istore chunk addr args src s => s :: nil | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil @@ -403,7 +417,7 @@ Definition instr_uses (i: instruction) : list reg := match i with | Inop s => nil | Iop op args res s => args - | Iload chunk addr args dst s => args + | Iload trap chunk addr args dst s => args | Istore chunk addr args src s => src :: args | Icall sig (inl r) args res s => r :: args | Icall sig (inr id) args res s => args @@ -422,7 +436,7 @@ Definition instr_defs (i: instruction) : option reg := match i with | Inop s => None | Iop op args res s => Some res - | Iload chunk addr args dst s => Some dst + | Iload trap chunk addr args dst s => Some dst | Istore chunk addr args src s => None | Icall sig ros args res s => Some res | Itailcall sig ros args => None @@ -462,7 +476,7 @@ Definition max_reg_instr (m: positive) (pc: node) (i: instruction) := match i with | Inop s => m | Iop op args res s => fold_left Pos.max args (Pos.max res m) - | Iload chunk addr args dst s => fold_left Pos.max args (Pos.max dst m) + | Iload trap chunk addr args dst s => fold_left Pos.max args (Pos.max dst m) | Istore chunk addr args src s => fold_left Pos.max args (Pos.max src m) | Icall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m)) | Icall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m) diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 9d7a8506..a0ca0f17 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -436,7 +436,7 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node) transl_exprlist map al rl no | Eload chunk addr al => do rl <- alloc_regs map al; - do no <- add_instr (Iload chunk addr rl rd nd); + do no <- add_instr (Iload TRAP chunk addr rl rd nd); transl_exprlist map al rl no | Econdition a b c => do nfalse <- transl_expr map c rd nd; diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 17022a7d..aa83da6d 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -707,7 +707,7 @@ Inductive tr_expr (c: code): tr_expr c map pr (Eop op al) ns nd rd dst | tr_Eload: forall map pr chunk addr al ns nd rd n1 rl dst, tr_exprlist c map pr al ns n1 rl -> - c!n1 = Some (Iload chunk addr rl rd nd) -> + c!n1 = Some (Iload TRAP chunk addr rl rd nd) -> reg_map_ok map rd dst -> ~In rd pr -> tr_expr c map pr (Eload chunk addr al) ns nd rd dst | tr_Econdition: forall map pr a ifso ifnot ns nd rd ntrue nfalse dst, diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 8336d1bf..74bfa582 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -104,11 +104,11 @@ Inductive wt_instr : instruction -> Prop := valid_successor s -> wt_instr (Iop op args res s) | wt_Iload: - forall chunk addr args dst s, + forall trap chunk addr args dst s, map env args = type_of_addressing addr -> env dst = type_of_chunk chunk -> valid_successor s -> - wt_instr (Iload chunk addr args dst s) + wt_instr (Iload trap chunk addr args dst s) | wt_Istore: forall chunk addr args src s, map env args = type_of_addressing addr -> @@ -282,7 +282,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := else (let (targs, tres) := type_of_operation op in do e1 <- S.set_list e args targs; S.set e1 res tres) - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => do x <- check_successor s; do e1 <- S.set_list e args (type_of_addressing addr); S.set e1 dst (type_of_chunk chunk) @@ -841,14 +841,24 @@ Proof. Qed. Lemma wt_exec_Iload: - forall env f chunk addr args dst s m a v rs, - wt_instr f env (Iload chunk addr args dst s) -> + forall env f trap chunk addr args dst s m a v rs, + wt_instr f env (Iload trap chunk addr args dst s) -> Mem.loadv chunk m a = Some v -> wt_regset env rs -> wt_regset env (rs#dst <- v). Proof. intros. destruct a; simpl in H0; try discriminate. inv H. - eapply wt_regset_assign; eauto. rewrite H8; eapply Mem.load_type; eauto. + eapply wt_regset_assign; eauto. rewrite H9; eapply Mem.load_type; eauto. +Qed. + +Lemma wt_exec_Iload_notrap: + forall env f chunk addr args dst s rs, + wt_instr f env (Iload NOTRAP chunk addr args dst s) -> + wt_regset env rs -> + wt_regset env (rs#dst <- (default_notrap_load_value chunk)). +Proof. + intros. + eapply wt_regset_assign; eauto. simpl. trivial. Qed. Lemma wt_exec_Ibuiltin: @@ -930,6 +940,10 @@ Proof. econstructor; eauto. eapply wt_exec_Iop; eauto. (* Iload *) econstructor; eauto. eapply wt_exec_Iload; eauto. + (* Iload notrap1*) + econstructor; eauto. eapply wt_exec_Iload_notrap; eauto. + (* Iload notrap2*) + econstructor; eauto. eapply wt_exec_Iload_notrap; eauto. (* Istore *) econstructor; eauto. (* Icall *) diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index 7db8a866..f2658b04 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -249,18 +249,18 @@ let block_of_RTL_instr funsig tyenv = function else let t = new_temp (tyenv res) in (t :: args2', t) in movelist args1 args3 (Xop(op, args3, res3) :: move res3 res1 [Xbranch s]) - | RTL.Iload(chunk, addr, args, dst, s) -> + | RTL.Iload(trap, chunk, addr, args, dst, s) -> if Archi.splitlong && chunk = Mint64 then begin match offset_addressing addr (coqint_of_camlint 4l) with | None -> assert false | Some addr' -> - [Xload(Mint32, addr, vregs tyenv args, + [Xload(trap, Mint32, addr, vregs tyenv args, V((if Archi.big_endian then dst else twin_reg dst), Tint)); - Xload(Mint32, addr', vregs tyenv args, + Xload(trap, Mint32, addr', vregs tyenv args, V((if Archi.big_endian then twin_reg dst else dst), Tint)); Xbranch s] end else - [Xload(chunk, addr, vregs tyenv args, vreg tyenv dst); Xbranch s] + [Xload(trap, chunk, addr, vregs tyenv args, vreg tyenv dst); Xbranch s] | RTL.Istore(chunk, addr, args, src, s) -> if Archi.splitlong && chunk = Mint64 then begin match offset_addressing addr (coqint_of_camlint 4l) with @@ -364,7 +364,7 @@ let live_before instr after = if VSet.mem res after then vset_addlist args (VSet.remove res after) else after - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> if VSet.mem dst after then vset_addlist args (VSet.remove dst after) else after @@ -459,7 +459,7 @@ let dce_instr instr after k = if VSet.mem res after then instr :: k else k - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> if VSet.mem dst after then instr :: k else k @@ -550,7 +550,7 @@ let spill_costs f = (* temps must not be spilled *) | Xop(op, args, res) -> charge_list 10 1 args; charge 10 1 res - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> charge_list 10 1 args; charge 10 1 dst | Xstore(chunk, addr, args, src) -> charge_list 10 1 args; charge 10 1 src @@ -677,7 +677,7 @@ let add_interfs_instr g instr live = (vset_addlist (res :: argl) (VSet.remove res live)) end; add_interfs_destroyed g (VSet.remove res live) (destroyed_by_op op) - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> add_interfs_def g dst live; add_interfs_destroyed g (VSet.remove dst live) (destroyed_by_load chunk addr) @@ -782,7 +782,7 @@ let tospill_instr alloc instr ts = ts | Xop(op, args, res) -> addlist_tospill alloc args (add_tospill alloc res ts) - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> addlist_tospill alloc args (add_tospill alloc dst ts) | Xstore(chunk, addr, args, src) -> addlist_tospill alloc args (add_tospill alloc src ts) @@ -964,10 +964,10 @@ let spill_instr tospill eqs instr = add res tmp (kill tmp (kill res eqs2))) end end - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> let (args', c1, eqs1) = reload_vars tospill eqs args in let (dst', c2, eqs2) = save_var tospill eqs1 dst in - (c1 @ Xload(chunk, addr, args', dst') :: c2, eqs2) + (c1 @ Xload(trap, chunk, addr, args', dst') :: c2, eqs2) | Xstore(chunk, addr, args, src) -> let (args', c1, eqs1) = reload_vars tospill eqs args in let (src', c2, eqs2) = reload_var tospill eqs1 src in @@ -1115,8 +1115,8 @@ let transl_instr alloc instr k = LTL.Lop(Omove, [rarg1], rres) :: LTL.Lop(op, rres :: rargl, rres) :: k end - | Xload(chunk, addr, args, dst) -> - LTL.Lload(chunk, addr, mregs_of alloc args, mreg_of alloc dst) :: k + | Xload(trap, chunk, addr, args, dst) -> + LTL.Lload(trap, chunk, addr, mregs_of alloc args, mreg_of alloc dst) :: k | Xstore(chunk, addr, args, src) -> LTL.Lstore(chunk, addr, mregs_of alloc args, mreg_of alloc src) :: k | Xcall(sg, vos, args, res) -> diff --git a/backend/Renumber.v b/backend/Renumber.v index 10f58251..7ba16658 100644 --- a/backend/Renumber.v +++ b/backend/Renumber.v @@ -43,7 +43,7 @@ Definition renum_instr (i: instruction) : instruction := match i with | Inop s => Inop (renum_pc s) | Iop op args res s => Iop op args res (renum_pc s) - | Iload chunk addr args res s => Iload chunk addr args res (renum_pc s) + | Iload trap chunk addr args res s => Iload trap chunk addr args res (renum_pc s) | Istore chunk addr args src s => Istore chunk addr args src (renum_pc s) | Icall sg ros args res s => Icall sg ros args res (renum_pc s) | Itailcall sg ros args => i diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index 7cda9425..2e161965 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -175,6 +175,18 @@ Proof. rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Iload; eauto. constructor; auto. eapply reach_succ; eauto. simpl; auto. + (* load notrap1 *) + 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. + constructor; auto. eapply reach_succ; eauto. simpl; auto. + (* load notrap2 *) + 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. + constructor; auto. eapply reach_succ; eauto. simpl; auto. (* store *) econstructor; split. assert (eval_addressing tge sp addr rs ## args = Some a). diff --git a/backend/Splitting.ml b/backend/Splitting.ml index 40f09c3d..78eb66a5 100644 --- a/backend/Splitting.ml +++ b/backend/Splitting.ml @@ -151,8 +151,8 @@ let ren_instr f maps pc i = | Inop s -> Inop s | Iop(op, args, res, s) -> Iop(op, ren_regs before args, ren_reg after res, s) - | Iload(chunk, addr, args, dst, s) -> - Iload(chunk, addr, ren_regs before args, ren_reg after dst, s) + | Iload(trap, chunk, addr, args, dst, s) -> + Iload(trap, chunk, addr, ren_regs before args, ren_reg after dst, s) | Istore(chunk, addr, args, src, s) -> Istore(chunk, addr, ren_regs before args, ren_reg before src, s) | Icall(sg, ros, args, res, s) -> diff --git a/backend/Stacking.v b/backend/Stacking.v index 7b382d05..0e3f2832 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -133,8 +133,8 @@ Definition transl_instr end | Lop op args res => Mop (transl_op fe op) args res :: k - | Lload chunk addr args dst => - Mload chunk (transl_addr fe addr) args dst :: k + | Lload trap chunk addr args dst => + Mload trap chunk (transl_addr fe addr) args dst :: k | Lstore chunk addr args src => Mstore chunk (transl_addr fe addr) args src :: k | Lcall sig ros => diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 326fab61..d3fcdb91 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1918,6 +1918,46 @@ Proof. apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. +- (* Lload notrap1*) + assert (eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = None) as Haddress. + eapply eval_addressing_inject_none; eauto. + eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP. + eapply agree_reglist; eauto. + econstructor; split. + apply plus_one. apply exec_Mload_notrap1. + rewrite <- Haddress. apply eval_addressing_preserved. exact symbols_preserved. + eauto. econstructor; eauto with coqlib. + apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. + apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. + +- (* Lload notrap2 *) + assert (exists a', + eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' + /\ Val.inject j a a'). + eapply eval_addressing_inject; eauto. + eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP. + eapply agree_reglist; eauto. + destruct H1 as [a' [A B]]. + + destruct ( Mem.loadv chunk m' a') as [v'|] eqn:Hloadv. + { + econstructor; split. + apply plus_one. apply exec_Mload with (a:=a') (v:=v'); eauto. + try (rewrite <- A; apply eval_addressing_preserved; auto; exact symbols_preserved). + econstructor; eauto with coqlib. + apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. + apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. + } + { + econstructor; split. + apply plus_one. apply exec_Mload_notrap2 with (a:=a'); eauto. + try (rewrite <- A; apply eval_addressing_preserved; auto; exact symbols_preserved). + + econstructor; eauto with coqlib. + apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. + apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. + } + - (* Lstore *) assert (exists a', eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 06e314f3..5cb1b980 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -438,6 +438,43 @@ Proof. apply eval_addressing_preserved. exact symbols_preserved. eauto. econstructor; eauto. apply set_reg_lessdef; auto. +- (* load notrap1 *) + TransfInstr. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. + left. + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- (default_notrap_load_value chunk)) m'); split. + eapply exec_Iload_notrap1. + eassumption. + eapply eval_addressing_lessdef_none. eassumption. + erewrite eval_addressing_preserved. + eassumption. exact symbols_preserved. + + econstructor; eauto. apply set_reg_lessdef; auto. + +- (* load notrap2 *) + TransfInstr. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. + left. + + exploit eval_addressing_lessdef; eauto. + intros [a' [ADDR' ALD]]. + + destruct (Mem.loadv chunk m' a') eqn:Echunk2. + + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v) m'); split. + eapply exec_Iload with (a:=a'). eassumption. + erewrite eval_addressing_preserved. + eassumption. + exact symbols_preserved. + assumption. + econstructor; eauto. apply set_reg_lessdef; auto. + + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- (default_notrap_load_value chunk)) m'); split. + eapply exec_Iload_notrap2. eassumption. + erewrite eval_addressing_preserved. + eassumption. + exact symbols_preserved. + assumption. + econstructor; eauto. apply set_reg_lessdef; auto. + - (* store *) TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 4f95ac9b..d3b8a9f0 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -441,6 +441,31 @@ Proof. rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef. +- (* Lload notrap1 *) + exploit eval_addressing_lessdef_none. apply reglist_lessdef; eauto. eassumption. + left; simpl; econstructor; split. + eapply exec_Lload_notrap1. + rewrite <- H0. + apply eval_addressing_preserved. exact symbols_preserved. eauto. + econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef. +- (* Lload notrap2 *) + exploit eval_addressing_lessdef. apply reglist_lessdef; eauto. eauto. + intros (ta & EV & LD). + destruct (Mem.loadv chunk tm ta) eqn:Htload. + { + left; simpl; econstructor; split. + eapply exec_Lload. + rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved. + exact Htload. eauto. + econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef. + } + { + left; simpl; econstructor; split. + eapply exec_Lload_notrap2. + rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved. + exact Htload. eauto. + econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef. + } - (* Lgetstack *) left; simpl; econstructor; split. econstructor; eauto. diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v index 8ac7c4ce..1b5f2547 100644 --- a/backend/Unusedglob.v +++ b/backend/Unusedglob.v @@ -46,7 +46,7 @@ Definition ref_instruction (i: instruction) : list ident := match i with | Inop _ => nil | Iop op _ _ _ => globals_operation op - | Iload _ addr _ _ _ => globals_addressing addr + | Iload _ _ addr _ _ _ => globals_addressing addr | Istore _ addr _ _ _ => globals_addressing addr | Icall _ (inl r) _ _ _ => nil | Icall _ (inr id) _ _ _ => id :: nil diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 680daba7..fa120b6d 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -915,7 +915,7 @@ Proof. /\ Val.inject j a ta). { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args). intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. - apply KEPT. red. exists pc, (Iload chunk addr args dst pc'); auto. + apply KEPT. red. exists pc, (Iload trap chunk addr args dst pc'); auto. econstructor; eauto. apply regs_inject; auto. assumption. } @@ -924,6 +924,36 @@ Proof. econstructor; split. eapply exec_Iload; eauto. econstructor; eauto. apply set_reg_inject; auto. +- (* load notrap1 *) + assert (eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = None). + { eapply eval_addressing_inj_none. + intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. + apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto. + econstructor; eauto. + rewrite Ptrofs.add_zero; reflexivity. + apply regs_inject; auto. + eassumption. + assumption. } + + econstructor; split. eapply exec_Iload_notrap1; eauto. + econstructor; eauto. apply set_reg_inject; auto. + +- (* load notrap2 *) + assert (A: exists ta, + eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta + /\ Val.inject j a ta). + { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args). + intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. + apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto. + econstructor; eauto. + apply regs_inject; auto. + assumption. } + destruct A as (ta & B & C). + destruct (Mem.loadv chunk tm ta) eqn:Echunk2. + + econstructor; split. eapply exec_Iload; eauto. + econstructor; eauto. apply set_reg_inject; auto. + + econstructor; split. eapply exec_Iload_notrap2; eauto. + econstructor; eauto. apply set_reg_inject; auto. - (* store *) assert (A: exists ta, eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 8dbb67a7..084a4548 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -139,9 +139,14 @@ Definition transfer (f: function) (rm: romem) (pc: node) (ae: aenv) (am: amem) : | Some(Iop op args res s) => let a := eval_static_operation op (aregs ae args) in VA.State (AE.set res a ae) am - | Some(Iload chunk addr args dst s) => + | Some(Iload TRAP chunk addr args dst s) => let a := loadv chunk rm am (eval_static_addressing addr (aregs ae args)) in VA.State (AE.set dst a ae) am + + (* TODO: maybe a case analysis on the results of loadv? *) + + | Some(Iload NOTRAP chunk addr args dst s) => + VA.State (AE.set dst Vtop ae) am | Some(Istore chunk addr args src s) => let am' := storev chunk am (eval_static_addressing addr (aregs ae args)) (areg ae src) in VA.State ae am' @@ -1268,11 +1273,29 @@ Proof. apply ematch_update; auto. eapply eval_static_operation_sound; eauto with va. - (* load *) + destruct trap. + + eapply sound_succ_state; eauto. simpl; auto. + unfold transfer; rewrite H. eauto. + apply ematch_update; auto. eapply loadv_sound; eauto with va. + eapply eval_static_addressing_sound; eauto with va. + + eapply sound_succ_state; eauto. simpl; auto. + unfold transfer; rewrite H. eauto. + apply ematch_update; auto. + eapply vmatch_top. + eapply loadv_sound; try eassumption. + eapply eval_static_addressing_sound; eauto with va. +- (* load notrap1 *) eapply sound_succ_state; eauto. simpl; auto. unfold transfer; rewrite H. eauto. - apply ematch_update; auto. eapply loadv_sound; eauto with va. - eapply eval_static_addressing_sound; eauto with va. - + apply ematch_update; auto. + unfold default_notrap_load_value. + constructor. +- (* load notrap2 *) + eapply sound_succ_state; eauto. simpl; auto. + unfold transfer; rewrite H. eauto. + apply ematch_update; auto. + unfold default_notrap_load_value. + constructor. - (* store *) exploit eval_static_addressing_sound; eauto with va. intros VMADDR. eapply sound_succ_state; eauto. simpl; auto. diff --git a/backend/XTL.ml b/backend/XTL.ml index f10efeed..c496fafb 100644 --- a/backend/XTL.ml +++ b/backend/XTL.ml @@ -30,7 +30,7 @@ type instruction = | Xspill of var * var | Xparmove of var list * var list * var * var | Xop of operation * var list * var - | Xload of memory_chunk * addressing * var list * var + | Xload of trapping_mode * memory_chunk * addressing * var list * var | Xstore of memory_chunk * addressing * var list * var | Xcall of signature * (var, ident) sum * var list * var list | Xtailcall of signature * (var, ident) sum * var list @@ -159,7 +159,7 @@ let type_instr = function let (targs, tres) = type_of_operation op in set_vars_type args targs; set_var_type res tres - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> set_vars_type args (type_of_addressing addr); set_var_type dst (type_of_chunk chunk) | Xstore(chunk, addr, args, src) -> diff --git a/backend/XTL.mli b/backend/XTL.mli index 54988d4b..b4b77fab 100644 --- a/backend/XTL.mli +++ b/backend/XTL.mli @@ -31,7 +31,7 @@ type instruction = | Xspill of var * var | Xparmove of var list * var list * var * var | Xop of operation * var list * var - | Xload of memory_chunk * addressing * var list * var + | Xload of trapping_mode * memory_chunk * addressing * var list * var | Xstore of memory_chunk * addressing * var list * var | Xcall of signature * (var, ident) sum * var list * var list | Xtailcall of signature * (var, ident) sum * var list diff --git a/common/AST.v b/common/AST.v index a91138c9..bb8508b7 100644 --- a/common/AST.v +++ b/common/AST.v @@ -193,6 +193,16 @@ Definition chunk_of_type (ty: typ) := Lemma chunk_of_Tptr: chunk_of_type Tptr = Mptr. Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed. +(** Trapping mode: does undefined behavior result in a trap or an undefined value (e.g. for loads) *) +Inductive trapping_mode : Type := TRAP | NOTRAP. + +Definition trapping_mode_eq : forall x y : trapping_mode, + { x=y } + { x <> y}. +Proof. + decide equality. +Defined. + + (** Initialization data for global variables. *) Inductive init_data: Type := diff --git a/common/Memory.v b/common/Memory.v index b68a5049..cfd13601 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -39,6 +39,9 @@ Require Import Values. Require Export Memdata. Require Export Memtype. +Definition default_notrap_load_value (chunk : memory_chunk) := Vundef. + + (* To avoid useless definitions of inductors in extracted code. *) Local Unset Elimination Schemes. Local Unset Case Analysis Schemes. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index e477957a..baddb722 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -90,3 +90,7 @@ let rec print_builtin_res px oc = function fprintf oc "splitlong(%a, %a)" (print_builtin_res px) hi (print_builtin_res px) lo +let print_trapping_mode oc = function + | TRAP -> () + | NOTRAP -> output_string oc " [notrap]" + diff --git a/driver/Clflags.ml b/driver/Clflags.ml index cf1220d1..fd8227c9 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -75,3 +75,4 @@ let option_fglobaladdroffset = ref false let option_fxsaddr = ref true let option_faddx = ref false let option_fcoalesce_mem = ref true +let option_all_loads_nontrap = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index c683c136..7536e8ff 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -42,6 +42,7 @@ Require Constprop. Require CSE. Require Deadcode. Require Unusedglob. +Require Allnontrap. Require Allocation. Require Tunneling. Require Linearize. @@ -63,6 +64,7 @@ Require Constpropproof. Require CSEproof. Require Deadcodeproof. Require Unusedglobproof. +Require Allnontrapproof. Require Allocproof. Require Tunnelingproof. Require Linearizeproof. @@ -136,6 +138,8 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 7) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 8) + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -243,6 +247,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass Unusedglobproof.match_prog + ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog ::: mkpass Linearizeproof.match_prog @@ -286,7 +291,8 @@ Proof. destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. - destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. + set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. + destruct (Allocation.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. set (p16 := Tunneling.tunnel_program p15) in *. destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate. set (p18 := CleanupLabels.transf_program p17) in *. @@ -307,6 +313,7 @@ Proof. exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14; split. apply Unusedglobproof.transf_program_match; auto. + exists p14bis; split. apply total_if_match. apply Allnontrapproof.transf_program_match. exists p15; split. apply Allocproof.transf_program_match; auto. exists p16; split. apply Tunnelingproof.transf_program_match. exists p17; split. apply Linearizeproof.transf_program_match; auto. @@ -364,7 +371,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 p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -394,6 +401,8 @@ Ltac DestructM := eapply compose_forward_simulations. eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. + eapply compose_forward_simulations. eapply Allocproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Tunnelingproof.transf_program_correct; eassumption. diff --git a/driver/Compopts.v b/driver/Compopts.v index 9c6448b7..26d888ae 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -62,3 +62,6 @@ Parameter thumb: unit -> bool. (** Flag -g. For insertion of debugging information. *) Parameter debug: unit -> bool. + +(** Flag -fall-loads-nontrap. Turn user loads into non trapping. *) +Parameter all_loads_nontrap: unit -> bool.
\ No newline at end of file diff --git a/driver/Driver.ml b/driver/Driver.ml index 288bb436..59b7b222 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -391,6 +391,7 @@ let cmdline_actions = @ f_opt "xsaddr" option_fxsaddr @ f_opt "addx" option_faddx @ f_opt "coalesce-mem" option_fcoalesce_mem + @ f_opt "all-loads-nontrap" option_all_loads_nontrap (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) diff --git a/extraction/extraction.v b/extraction/extraction.v index ee45b756..994d41a4 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -127,6 +127,10 @@ Extract Constant Compopts.optim_addx => "fun _ -> !Clflags.option_faddx". Extract Constant Compopts.optim_coalesce_mem => "fun _ -> !Clflags.option_fcoalesce_mem". +Extract Constant Compopts.va_strict => + "fun _ -> false". +Extract Constant Compopts.all_loads_nontrap => + "fun _ -> !Clflags.option_all_loads_nontrap". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index f09aa99c..e37176ef 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -107,16 +107,16 @@ Inductive instruction : Type := | Pstsud (rd rs1 rs2: ireg)
(** Loads **)
- | Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *)
- | Plbu (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte unsigned *)
- | Plh (rd: ireg) (ra: ireg) (ofs: addressing) (**r load half word *)
- | Plhu (rd: ireg) (ra: ireg) (ofs: addressing) (**r load half word unsigned *)
- | Plw (rd: ireg) (ra: ireg) (ofs: addressing) (**r load int32 *)
- | Plw_a (rd: ireg) (ra: ireg) (ofs: addressing) (**r load any32 *)
- | Pld (rd: ireg) (ra: ireg) (ofs: addressing) (**r load int64 *)
- | Pld_a (rd: ireg) (ra: ireg) (ofs: addressing) (**r load any64 *)
- | Pfls (rd: freg) (ra: ireg) (ofs: addressing) (**r load float *)
- | Pfld (rd: freg) (ra: ireg) (ofs: addressing) (**r load 64-bit float *)
+ | Plb (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *)
+ | Plbu (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte unsigned *)
+ | Plh (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load half word *)
+ | Plhu (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load half word unsigned *)
+ | Plw (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load int32 *)
+ | Plw_a (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load any32 *)
+ | Pld (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load int64 *)
+ | Pld_a (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load any64 *)
+ | Pfls (trap: trapping_mode) (rd: freg) (ra: ireg) (ofs: addressing) (**r load float *)
+ | Pfld (trap: trapping_mode) (rd: freg) (ra: ireg) (ofs: addressing) (**r load 64-bit float *)
| Plq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (**r load 2*64-bit *)
| Plo (rs: gpreg_o) (ra: ireg) (ofs: addressing) (**r load 4*64-bit *)
@@ -481,41 +481,41 @@ Definition basic_to_instruction (b: basic) := | PArithARRI64 (Asmvliw.Pcmoveil cond) rd rs1 imm => Pcmoveil cond rd rs1 imm
| PArithARRI64 (Asmvliw.Pcmoveuil cond) rd rs1 imm => Pcmoveuil cond rd rs1 imm
(** Load *)
- | PLoadRRO Asmvliw.Plb rd ra ofs => Plb rd ra (AOff ofs)
- | PLoadRRO Asmvliw.Plbu rd ra ofs => Plbu rd ra (AOff ofs)
- | PLoadRRO Asmvliw.Plh rd ra ofs => Plh rd ra (AOff ofs)
- | PLoadRRO Asmvliw.Plhu rd ra ofs => Plhu rd ra (AOff ofs)
- | PLoadRRO Asmvliw.Plw rd ra ofs => Plw rd ra (AOff ofs)
- | PLoadRRO Asmvliw.Plw_a rd ra ofs => Plw_a rd ra (AOff ofs)
- | PLoadRRO Asmvliw.Pld rd ra ofs => Pld rd ra (AOff ofs)
- | PLoadRRO Asmvliw.Pld_a rd ra ofs => Pld_a rd ra (AOff ofs)
- | PLoadRRO Asmvliw.Pfls rd ra ofs => Pfls rd ra (AOff ofs)
- | PLoadRRO Asmvliw.Pfld rd ra ofs => Pfld rd ra (AOff ofs)
+ | PLoadRRO trap Asmvliw.Plb rd ra ofs => Plb trap rd ra (AOff ofs)
+ | PLoadRRO trap Asmvliw.Plbu rd ra ofs => Plbu trap rd ra (AOff ofs)
+ | PLoadRRO trap Asmvliw.Plh rd ra ofs => Plh trap rd ra (AOff ofs)
+ | PLoadRRO trap Asmvliw.Plhu rd ra ofs => Plhu trap rd ra (AOff ofs)
+ | PLoadRRO trap Asmvliw.Plw rd ra ofs => Plw trap rd ra (AOff ofs)
+ | PLoadRRO trap Asmvliw.Plw_a rd ra ofs => Plw_a trap rd ra (AOff ofs)
+ | PLoadRRO trap Asmvliw.Pld rd ra ofs => Pld trap rd ra (AOff ofs)
+ | PLoadRRO trap Asmvliw.Pld_a rd ra ofs => Pld_a trap rd ra (AOff ofs)
+ | PLoadRRO trap Asmvliw.Pfls rd ra ofs => Pfls trap rd ra (AOff ofs)
+ | PLoadRRO trap Asmvliw.Pfld rd ra ofs => Pfld trap rd ra (AOff ofs)
| PLoadQRRO qrs ra ofs => Plq qrs ra (AOff ofs)
| PLoadORRO qrs ra ofs => Plo qrs ra (AOff ofs)
- | PLoadRRR Asmvliw.Plb rd ra ro => Plb rd ra (AReg ro)
- | PLoadRRR Asmvliw.Plbu rd ra ro => Plbu rd ra (AReg ro)
- | PLoadRRR Asmvliw.Plh rd ra ro => Plh rd ra (AReg ro)
- | PLoadRRR Asmvliw.Plhu rd ra ro => Plhu rd ra (AReg ro)
- | PLoadRRR Asmvliw.Plw rd ra ro => Plw rd ra (AReg ro)
- | PLoadRRR Asmvliw.Plw_a rd ra ro => Plw_a rd ra (AReg ro)
- | PLoadRRR Asmvliw.Pld rd ra ro => Pld rd ra (AReg ro)
- | PLoadRRR Asmvliw.Pld_a rd ra ro => Pld_a rd ra (AReg ro)
- | PLoadRRR Asmvliw.Pfls rd ra ro => Pfls rd ra (AReg ro)
- | PLoadRRR Asmvliw.Pfld rd ra ro => Pfld rd ra (AReg ro)
-
- | PLoadRRRXS Asmvliw.Plb rd ra ro => Plb rd ra (ARegXS ro)
- | PLoadRRRXS Asmvliw.Plbu rd ra ro => Plbu rd ra (ARegXS ro)
- | PLoadRRRXS Asmvliw.Plh rd ra ro => Plh rd ra (ARegXS ro)
- | PLoadRRRXS Asmvliw.Plhu rd ra ro => Plhu rd ra (ARegXS ro)
- | PLoadRRRXS Asmvliw.Plw rd ra ro => Plw rd ra (ARegXS ro)
- | PLoadRRRXS Asmvliw.Plw_a rd ra ro => Plw_a rd ra (ARegXS ro)
- | PLoadRRRXS Asmvliw.Pld rd ra ro => Pld rd ra (ARegXS ro)
- | PLoadRRRXS Asmvliw.Pld_a rd ra ro => Pld_a rd ra (ARegXS ro)
- | PLoadRRRXS Asmvliw.Pfls rd ra ro => Pfls rd ra (ARegXS ro)
- | PLoadRRRXS Asmvliw.Pfld rd ra ro => Pfld rd ra (ARegXS ro)
+ | PLoadRRR trap Asmvliw.Plb rd ra ro => Plb trap rd ra (AReg ro)
+ | PLoadRRR trap Asmvliw.Plbu rd ra ro => Plbu trap rd ra (AReg ro)
+ | PLoadRRR trap Asmvliw.Plh rd ra ro => Plh trap rd ra (AReg ro)
+ | PLoadRRR trap Asmvliw.Plhu rd ra ro => Plhu trap rd ra (AReg ro)
+ | PLoadRRR trap Asmvliw.Plw rd ra ro => Plw trap rd ra (AReg ro)
+ | PLoadRRR trap Asmvliw.Plw_a rd ra ro => Plw_a trap rd ra (AReg ro)
+ | PLoadRRR trap Asmvliw.Pld rd ra ro => Pld trap rd ra (AReg ro)
+ | PLoadRRR trap Asmvliw.Pld_a rd ra ro => Pld_a trap rd ra (AReg ro)
+ | PLoadRRR trap Asmvliw.Pfls rd ra ro => Pfls trap rd ra (AReg ro)
+ | PLoadRRR trap Asmvliw.Pfld rd ra ro => Pfld trap rd ra (AReg ro)
+
+ | PLoadRRRXS trap Asmvliw.Plb rd ra ro => Plb trap rd ra (ARegXS ro)
+ | PLoadRRRXS trap Asmvliw.Plbu rd ra ro => Plbu trap rd ra (ARegXS ro)
+ | PLoadRRRXS trap Asmvliw.Plh rd ra ro => Plh trap rd ra (ARegXS ro)
+ | PLoadRRRXS trap Asmvliw.Plhu rd ra ro => Plhu trap rd ra (ARegXS ro)
+ | PLoadRRRXS trap Asmvliw.Plw rd ra ro => Plw trap rd ra (ARegXS ro)
+ | PLoadRRRXS trap Asmvliw.Plw_a rd ra ro => Plw_a trap rd ra (ARegXS ro)
+ | PLoadRRRXS trap Asmvliw.Pld rd ra ro => Pld trap rd ra (ARegXS ro)
+ | PLoadRRRXS trap Asmvliw.Pld_a rd ra ro => Pld_a trap rd ra (ARegXS ro)
+ | PLoadRRRXS trap Asmvliw.Pfls rd ra ro => Pfls trap rd ra (ARegXS ro)
+ | PLoadRRRXS trap Asmvliw.Pfld rd ra ro => Pfld trap rd ra (ARegXS ro)
(** Store *)
| PStoreRRO Asmvliw.Psb rd ra ofs => Psb rd ra (AOff ofs)
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 9b4489c5..91e5ac89 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -260,11 +260,11 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := parexec (** Auxiliaries for memory accesses *) -Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := parexec_load_offset chunk rs rs m m d a ofs. +Definition exec_load_offset (trap: trapping_mode) (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := parexec_load_offset trap chunk rs rs m m d a ofs. -Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_reg chunk rs rs m m d a ro. +Definition exec_load_reg (trap: trapping_mode) (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_reg trap chunk rs rs m m d a ro. -Definition exec_load_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_regxs chunk rs rs m m d a ro. +Definition exec_load_regxs (trap: trapping_mode) (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_regxs trap chunk rs rs m m d a ro. Definition exec_load_q_offset (rs: regset) (m: mem) (d : gpreg_q) (a: ireg) (ofs: offset) := parexec_load_q_offset rs rs m m d a ofs. diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index c4c1bbf1..65792d13 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -83,9 +83,9 @@ Coercion OArithRRI32: arith_name_rri32 >-> Funclass. Coercion OArithRRI64: arith_name_rri64 >-> Funclass. Inductive load_op := - | OLoadRRO (n: load_name) (ofs: offset) - | OLoadRRR (n: load_name) - | OLoadRRRXS (n: load_name) + | OLoadRRO (n: load_name) (trap: trapping_mode) (ofs: offset) + | OLoadRRR (n: load_name) (trap: trapping_mode) + | OLoadRRRXS (n: load_name) (trap: trapping_mode) . Coercion OLoadRRO: load_name >-> Funclass. @@ -142,33 +142,39 @@ Definition arith_eval (ao: arith_op) (l: list value) := | _, _ => None end. -Definition exec_load_deps_offset (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) := +Definition exec_incorrect_load trap chunk := + match trap with + | TRAP => None + | NOTRAP => Some (Val (concrete_default_notrap_load_value chunk)) + end. + +Definition exec_load_deps_offset (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) := let (ge, fn) := Ge in match (eval_offset ofs) with | OK ptr => match Mem.loadv chunk m (Val.offset_ptr v ptr) with - | None => None + | None => exec_incorrect_load trap chunk | Some vl => Some (Val vl) end | _ => None end. -Definition exec_load_deps_reg (chunk: memory_chunk) (m: mem) (v vo: val) := +Definition exec_load_deps_reg (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v vo: val) := match Mem.loadv chunk m (Val.addl v vo) with - | None => None + | None => exec_incorrect_load trap chunk | Some vl => Some (Val vl) end. -Definition exec_load_deps_regxs (chunk: memory_chunk) (m: mem) (v vo: val) := +Definition exec_load_deps_regxs (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v vo: val) := match Mem.loadv chunk m (Val.addl v (Val.shll vo (scale_of_chunk chunk))) with - | None => None + | None => exec_incorrect_load trap chunk | Some vl => Some (Val vl) end. Definition load_eval (lo: load_op) (l: list value) := match lo, l with - | OLoadRRO n ofs, [Val v; Memstate m] => exec_load_deps_offset (load_chunk n) m v ofs - | OLoadRRR n, [Val v; Val vo; Memstate m] => exec_load_deps_reg (load_chunk n) m v vo - | OLoadRRRXS n, [Val v; Val vo; Memstate m] => exec_load_deps_regxs (load_chunk n) m v vo + | OLoadRRO n trap ofs, [Val v; Memstate m] => exec_load_deps_offset trap (load_chunk n) m v ofs + | OLoadRRR n trap, [Val v; Val vo; Memstate m] => exec_load_deps_reg trap (load_chunk n) m v vo + | OLoadRRRXS n trap, [Val v; Val vo; Memstate m] => exec_load_deps_regxs trap (load_chunk n) m v vo | _, _ => None end. @@ -364,24 +370,47 @@ Proof. Qed. Hint Resolve offset_eq_correct: wlp. +Definition trapping_mode_eq trap1 trap2 := + RET (match trap1, trap2 with + | TRAP, TRAP | NOTRAP, NOTRAP => true + | TRAP, NOTRAP | NOTRAP, TRAP => false + end). +Lemma trapping_mode_eq_correct t1 t2: + WHEN trapping_mode_eq t1 t2 ~> b THEN b = true -> t1 = t2. +Proof. + wlp_simplify. + destruct t1; destruct t2; trivial; discriminate. +Qed. +Hint Resolve trapping_mode_eq_correct: wlp. + Definition load_op_eq (o1 o2: load_op): ?? bool := match o1 with - | OLoadRRO n1 ofs1 => - match o2 with OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (offset_eq ofs1 ofs2) | _ => RET false end - | OLoadRRR n1 => - match o2 with OLoadRRR n2 => phys_eq n1 n2 | _ => RET false end - | OLoadRRRXS n1 => - match o2 with OLoadRRRXS n2 => phys_eq n1 n2 | _ => RET false end + | OLoadRRO n1 trap ofs1 => + match o2 with + | OLoadRRO n2 trap2 ofs2 => iandb (phys_eq n1 n2) (iandb (offset_eq ofs1 ofs2) (trapping_mode_eq trap trap2)) + | _ => RET false + end + | OLoadRRR n1 trap => + match o2 with + | OLoadRRR n2 trap2 => iandb (phys_eq n1 n2) (trapping_mode_eq trap trap2) + | _ => RET false + end + | OLoadRRRXS n1 trap => + match o2 with + | OLoadRRRXS n2 trap2 => iandb (phys_eq n1 n2) (trapping_mode_eq trap trap2) + | _ => RET false + end end. Lemma load_op_eq_correct o1 o2: WHEN load_op_eq o1 o2 ~> b THEN b = true -> o1 = o2. Proof. destruct o1, o2; wlp_simplify; try discriminate. - - f_equal. pose (Ptrofs.eq_spec ofs ofs0). - rewrite H in *. trivial. - - congruence. - - congruence. + { f_equal. + destruct trap, trap0; simpl in *; trivial; discriminate. + pose (Ptrofs.eq_spec ofs ofs0). + rewrite H in *. trivial. } + all: destruct trap, trap0; simpl in *; trivial; discriminate. Qed. Hint Resolve load_op_eq_correct: wlp. Opaque load_op_eq_correct. @@ -617,21 +646,21 @@ Definition trans_arith (ai: ar_instruction) : inst := Definition trans_basic (b: basic) : inst := match b with | PArith ai => trans_arith ai - | PLoadRRO n d a ofs => [(#d, Op (Load (OLoadRRO n ofs)) (PReg (#a) @ PReg pmem @ Enil))] - | PLoadRRR n d a ro => [(#d, Op (Load (OLoadRRR n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] - | PLoadRRRXS n d a ro => [(#d, Op (Load (OLoadRRRXS n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PLoadRRO trap n d a ofs => [(#d, Op (Load (OLoadRRO n trap ofs)) (PReg (#a) @ PReg pmem @ Enil))] + | PLoadRRR trap n d a ro => [(#d, Op (Load (OLoadRRR n trap)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PLoadRRRXS trap n d a ro => [(#d, Op (Load (OLoadRRRXS n trap)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg (#s) @ PReg (#a) @ PReg pmem @ Enil))] | PLoadQRRO qd a ofs => let (d0, d1) := gpreg_q_expand qd in - [(#d0, Op (Load (OLoadRRO Pld_a ofs)) (PReg (#a) @ PReg pmem @ Enil)); - (#d1, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(PReg (#a)) @ PReg pmem @ Enil))] + [(#d0, Op (Load (OLoadRRO Pld_a TRAP ofs)) (PReg (#a) @ PReg pmem @ Enil)); + (#d1, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(PReg (#a)) @ PReg pmem @ Enil))] | PLoadORRO od a ofs => match gpreg_o_expand od with | (d0, d1, d2, d3) => - [(#d0, Op (Load (OLoadRRO Pld_a ofs)) (PReg (#a) @ PReg pmem @ Enil)); - (#d1, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(PReg (#a)) @ PReg pmem @ Enil)); - (#d2, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 16)))) (Old(PReg (#a)) @ PReg pmem @ Enil)); - (#d3, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 24)))) (Old(PReg (#a)) @ PReg pmem @ Enil))] + [(#d0, Op (Load (OLoadRRO Pld_a TRAP ofs)) (PReg (#a) @ PReg pmem @ Enil)); + (#d1, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(PReg (#a)) @ PReg pmem @ Enil)); + (#d2, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 16)))) (Old(PReg (#a)) @ PReg pmem @ Enil)); + (#d3, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 24)))) (Old(PReg (#a)) @ PReg pmem @ Enil))] end | PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] | PStoreRRRXS n s a ro => [(pmem, Op (Store (OStoreRRRXS n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] @@ -861,21 +890,21 @@ Local Ltac preg_eq_discr r rd := unfold parexec_load_offset; simpl; unfold exec_load_deps_offset; erewrite GENV, H, H0; unfold eval_offset; simpl; auto; - destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; + destruct (Mem.loadv _ _ _) eqn:MEML; destruct trap; simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. (* Load Reg *) + destruct i; simpl load_chunk. all: unfold parexec_load_reg; simpl; unfold exec_load_deps_reg; rewrite H, H0; rewrite (H0 rofs); - destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; + destruct (Mem.loadv _ _ _) eqn:MEML; destruct trap; simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. (* Load Reg XS *) + destruct i; simpl load_chunk. all: unfold parexec_load_regxs; simpl; unfold exec_load_deps_regxs; rewrite H, H0; rewrite (H0 rofs); - destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; + destruct (Mem.loadv _ _ _) eqn:MEML; destruct trap; simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. @@ -1537,9 +1566,9 @@ Definition string_of_load_name (n: load_name) : pstring := Definition string_of_load (op: load_op): pstring := match op with - | OLoadRRO n _ => string_of_load_name n - | OLoadRRR n => string_of_load_name n - | OLoadRRRXS n => string_of_load_name n + | OLoadRRO n _ _ => string_of_load_name n + | OLoadRRR n _ => string_of_load_name n + | OLoadRRRXS n _ => string_of_load_name n end. Definition string_of_store_name (n: store_name) : pstring := diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index ade84e7b..fd50f3b4 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -912,12 +912,12 @@ end. Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) := match ty, preg_of dst with - | Tint, IR rd => OK (indexed_memory_access (PLoadRRO Plw rd) base ofs ::i k) - | Tlong, IR rd => OK (indexed_memory_access (PLoadRRO Pld rd) base ofs ::i k) - | Tsingle, IR rd => OK (indexed_memory_access (PLoadRRO Pfls rd) base ofs ::i k) - | Tfloat, IR rd => OK (indexed_memory_access (PLoadRRO Pfld rd) base ofs ::i k) - | Tany32, IR rd => OK (indexed_memory_access (PLoadRRO Plw_a rd) base ofs ::i k) - | Tany64, IR rd => OK (indexed_memory_access (PLoadRRO Pld_a rd) base ofs ::i k) + | Tint, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Plw rd) base ofs ::i k) + | Tlong, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pld rd) base ofs ::i k) + | Tsingle, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pfls rd) base ofs ::i k) + | Tfloat, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pfld rd) base ofs ::i k) + | Tany32, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Plw_a rd) base ofs ::i k) + | Tany64, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pld_a rd) base ofs ::i k) | _, _ => Error (msg "Asmblockgen.loadind") end. @@ -933,7 +933,7 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: bcode) end. Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) := - indexed_memory_access (PLoadRRO Pld dst) base ofs. + indexed_memory_access (PLoadRRO TRAP Pld dst) base ofs. Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) := indexed_memory_access (PStoreRRO Psd src) base ofs. @@ -993,27 +993,28 @@ Definition chunk2load (chunk: memory_chunk) := | Many64 => Pld_a end. -Definition transl_load_rro (chunk: memory_chunk) (addr: addressing) +Definition transl_load_rro (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access (PLoadRRO (chunk2load chunk) r) addr args k. + transl_memory_access (PLoadRRO trap (chunk2load chunk) r) addr args k. -Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing) +Definition transl_load_rrr (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access2 (PLoadRRR (chunk2load chunk) r) addr args k. + transl_memory_access2 (PLoadRRR trap (chunk2load chunk) r) addr args k. -Definition transl_load_rrrXS (chunk: memory_chunk) (scale : Z) +Definition transl_load_rrrXS (trap: trapping_mode) (chunk: memory_chunk) (scale : Z) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access2XS chunk (PLoadRRRXS (chunk2load chunk) r) scale args k. + transl_memory_access2XS chunk (PLoadRRRXS trap (chunk2load chunk) r) scale args k. -Definition transl_load (chunk: memory_chunk) (addr: addressing) +Definition transl_load (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := match addr with - | Aindexed2XS scale => transl_load_rrrXS chunk scale args dst k - | Aindexed2 => transl_load_rrr chunk addr args dst k - | _ => transl_load_rro chunk addr args dst k + | Aindexed2XS scale => transl_load_rrrXS trap chunk scale args dst k + | Aindexed2 => transl_load_rrr trap chunk addr args dst k + | _ => transl_load_rro trap chunk addr args dst k end. Definition chunk2store (chunk: memory_chunk) := @@ -1073,8 +1074,8 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst) else (loadind_ptr SP f.(fn_link_ofs) FP) ::i c) | MBop op args res => transl_op op args res k - | MBload chunk addr args dst => - transl_load chunk addr args dst k + | MBload trap chunk addr args dst => + transl_load trap chunk addr args dst k | MBstore chunk addr args src => transl_store chunk addr args src k end. diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index c44ef3ff..6baca8c0 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1204,6 +1204,62 @@ Local Transparent destroyed_by_op. eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.
simpl; congruence.
+ - (* notrap1 cannot happen *)
+ simpl in EQ0. unfold transl_load in EQ0.
+ destruct addr; simpl in H.
+ all: unfold transl_load_rrrXS, transl_load_rrr, transl_load_rro in EQ0;
+ monadInv EQ0; unfold transl_memory_access2XS, transl_memory_access2, transl_memory_access in EQ2;
+ destruct args as [|h0 t0]; try discriminate;
+ destruct t0 as [|h1 t1]; try discriminate;
+ destruct t1 as [|h2 t2]; try discriminate.
+
+ - (* MBload notrap2 TODO *)
+ simpl in EQ0. rewrite Hheader in DXP.
+
+ assert (eval_addressing tge sp addr (map ms args) = Some a).
+ rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+ exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
+ intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+
+ destruct (Mem.loadv chunk m1 a') as [v' | ] eqn:Hload.
+ {
+ exploit transl_load_correct; eauto.
+ intros [rs2 [P [Q R]]].
+
+ eapply exec_straight_body in P.
+ 2: eapply code_to_basics_id; eauto.
+ destruct P as (l & ll & TBC & CTB & EXECB).
+ exists rs2, m1, ll.
+ eexists. eexists. split. instantiate (1 := x). eauto.
+ repeat (split; auto).
+ eapply basics_to_code_app; eauto.
+ remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+(* assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
+ rewrite <- Hheadereq. *) subst.
+ eapply match_codestate_intro; eauto. simpl. simpl in EQ.
+
+ eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.
+ simpl; congruence.
+ }
+ {
+ exploit transl_load_correct_notrap2; eauto.
+ intros [rs2 [P [Q R]]].
+
+ eapply exec_straight_body in P.
+ 2: eapply code_to_basics_id; eauto.
+ destruct P as (l & ll & TBC & CTB & EXECB).
+ exists rs2, m1, ll.
+ eexists. eexists. split. instantiate (1 := x). eauto.
+ repeat (split; auto).
+ eapply basics_to_code_app; eauto.
+ remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+(* assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
+ rewrite <- Hheadereq. *) subst.
+ eapply match_codestate_intro; eauto. simpl. simpl in EQ.
+
+ eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.
+ simpl; congruence.
+ }
- (* MBstore *)
simpl in EQ0. rewrite Hheader in DXP.
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v index decc3e2e..07c445e2 100644 --- a/mppa_k1c/Asmblockgenproof0.v +++ b/mppa_k1c/Asmblockgenproof0.v @@ -897,34 +897,36 @@ Lemma exec_basic_instr_pc: Proof. intros. destruct b; try destruct i; try destruct i. all: try (inv H; Simpl). - 1-10: try (unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). - 1-10: try (unfold parexec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). - 1-10: try (unfold parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). - 1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). - 1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. - 1-10: try (unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. - - (* PLoadQRRO *) + 1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. + + 1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. + + { (* PLoadQRRO *) unfold parexec_load_q_offset in H1. destruct (gpreg_q_expand _) as [r0 r1] in H1. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. - - (* PLoadORRO *) + inv H1. Simpl. } + { (* PLoadORRO *) unfold parexec_load_o_offset in H1. destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. - - (* PStoreQRRO *) + inv H1. Simpl. } + 1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail. + 1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail. + 1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail. + + { (* PStoreQRRO *) unfold parexec_store_q_offset in H1. destruct (gpreg_q_expand _) as [r0 r1] in H1. unfold eval_offset in H1; try discriminate. destruct (Mem.storev _ _ _) in H1; try discriminate. destruct (Mem.storev _ _ _) in H1; try discriminate. - inv H1. Simpl. reflexivity. - - (* PStoreORRO *) + inv H1. Simpl. reflexivity. } + { (* PStoreORRO *) unfold parexec_store_o_offset in H1. destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. unfold eval_offset in H1; try discriminate. @@ -932,7 +934,7 @@ Proof. destruct (Mem.storev _ _ _) in H1; try discriminate. destruct (Mem.storev _ _ _) in H1; try discriminate. destruct (Mem.storev _ _ _) in H1; try discriminate. - inv H1. Simpl. reflexivity. + inv H1. Simpl. reflexivity. } - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index e1e2b0b0..c0a05ab3 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1661,9 +1661,9 @@ Qed. Lemma indexed_load_access_correct: - forall chunk (mk_instr: ireg -> offset -> basic) rd m, + forall trap chunk (mk_instr: ireg -> offset -> basic) rd m, (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset trap chunk rs m rd base ofs) -> forall (base: ireg) ofs k (rs: regset) v, Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v -> exists rs', @@ -1716,7 +1716,7 @@ Proof. /\ c = indexed_memory_access mk_instr base ofs :: k /\ forall base' ofs' rs', exec_basic_instr ge (mk_instr base' ofs') rs' m = - exec_load_offset (chunk_of_type ty) rs' m rd base' ofs'). + exec_load_offset TRAP (chunk_of_type ty) rs' m rd base' ofs'). { unfold loadind in TR. destruct ty, (preg_of dst); inv TR; econstructor; esplit; eauto. } destruct A as (mk_instr & rd & rdEq & B & C). subst c. rewrite rdEq. @@ -1784,7 +1784,9 @@ Lemma loadind_ptr_correct: /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r. Proof. intros. eapply indexed_load_access_correct; eauto with asmgen. - intros. unfold Mptr. assert (Archi.ptr64 = true). auto. rewrite H0. auto. + intros. unfold Mptr. assert (Archi.ptr64 = true). auto. rewrite H0. + instantiate (1 := TRAP). + auto. Qed. Lemma storeind_ptr_correct: @@ -1877,11 +1879,11 @@ Proof. Qed. Lemma transl_load_access2_correct: - forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c rd (rs: regset) m v mro mr1 ro v', + forall trap chunk (mk_instr: ireg -> ireg -> basic) addr args k c rd (rs: regset) m v mro mr1 ro v', args = mr1 :: mro :: nil -> ireg_of mro = OK ro -> (forall base rs, - exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg chunk rs m rd base ro) -> + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg trap chunk rs m rd base ro) -> transl_memory_access2 mk_instr addr args k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> Mem.loadv chunk m v = Some v' -> @@ -1899,12 +1901,35 @@ Proof. split; intros; Simpl. auto. Qed. +Lemma transl_load_access2_correct_notrap2: + forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c rd (rs: regset) m v mro mr1 ro, + args = mr1 :: mro :: nil -> + ireg_of mro = OK ro -> + (forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg NOTRAP chunk rs m rd base ro) -> + transl_memory_access2 mk_instr addr args k = OK c -> + eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> + Mem.loadv chunk m v = None -> + exists rs', + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m + /\ rs'#rd = concrete_default_notrap_load_value chunk + /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r. +Proof. + intros until ro; intros ARGS IREGE INSTR TR EV LOAD. + exploit transl_memory_access2_correct; eauto. + intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS. + econstructor; split. + eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2. + rewrite INSTR. unfold exec_load_reg. unfold parexec_load_reg. rewrite B, LOAD. reflexivity. Simpl. + split; intros; Simpl. auto. +Qed. + Lemma transl_load_access2XS_correct: - forall chunk (mk_instr: ireg -> ireg -> basic) (scale : Z) args k c rd (rs: regset) m v mro mr1 ro v', + forall trap chunk (mk_instr: ireg -> ireg -> basic) (scale : Z) args k c rd (rs: regset) m v mro mr1 ro v', args = mr1 :: mro :: nil -> ireg_of mro = OK ro -> (forall base rs, - exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs chunk rs m rd base ro) -> + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs trap chunk rs m rd base ro) -> transl_memory_access2XS chunk mk_instr scale args k = OK c -> eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v -> Mem.loadv chunk m v = Some v' -> @@ -1922,13 +1947,39 @@ Proof. unfold scale_of_chunk. subst scale. rewrite B, LOAD. reflexivity. Simpl. - split; intros; Simpl. auto. + split. trivial. intros. Simpl. +Qed. + +Lemma transl_load_access2XS_correct_notrap2: + forall chunk (mk_instr: ireg -> ireg -> basic) (scale : Z) args k c rd (rs: regset) m v mro mr1 ro, + args = mr1 :: mro :: nil -> + ireg_of mro = OK ro -> + (forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs NOTRAP chunk rs m rd base ro) -> + transl_memory_access2XS chunk mk_instr scale args k = OK c -> + eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v -> + Mem.loadv chunk m v = None -> + exists rs', + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m + /\ rs'#rd = concrete_default_notrap_load_value chunk + /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r. +Proof. + intros until ro; intros ARGS IREGE INSTR TR EV LOAD. + exploit transl_memory_access2XS_correct; eauto. + intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C & D). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS. + econstructor; split. + eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2. + rewrite INSTR. unfold exec_load_regxs. unfold parexec_load_regxs. + unfold scale_of_chunk. + subst scale. + rewrite B, LOAD. reflexivity. Simpl. + split. trivial. intros. Simpl. Qed. Lemma transl_load_access_correct: - forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v', + forall trap chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v', (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset trap chunk rs m rd base ofs) -> transl_memory_access mk_instr addr args k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> Mem.loadv chunk m v = Some v' -> @@ -1946,54 +1997,119 @@ Proof. split; intros; Simpl. auto. Qed. +Lemma transl_load_access_correct_notrap2: + forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v, + (forall base ofs rs, + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset NOTRAP chunk rs m rd base ofs) -> + transl_memory_access mk_instr addr args k = OK c -> + eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> + Mem.loadv chunk m v = None -> + exists rs', + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m + /\ rs'#rd = concrete_default_notrap_load_value chunk + /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r. +Proof. + intros until v; intros INSTR TR EV LOAD. + exploit transl_memory_access_correct; eauto. + intros (base & ofs & rs' & ptr & A & PtrEq & B & C). + econstructor; split. + eapply exec_straight_opt_right. eexact A. apply exec_straight_one. + rewrite INSTR. unfold exec_load_offset. unfold parexec_load_offset. rewrite PtrEq, B, LOAD. reflexivity. Simpl. + split. trivial. intros. Simpl. +Qed. + Lemma transl_load_memory_access_ok: - forall addr chunk args dst k c rs a v m, + forall addr trap chunk args dst k c rs a v m, (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) -> - transl_load chunk addr args dst k = OK c -> + transl_load trap chunk addr args dst k = OK c -> eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> exists mk_instr rd, preg_of dst = IR rd /\ transl_memory_access mk_instr addr args k = OK c /\ forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs. + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset trap chunk rs m rd base ofs. Proof. intros until m. intros ADDR TR ? ?. unfold transl_load in TR. destruct addr; try contradiction. - monadInv TR. destruct chunk; ArgsInv; econstructor; (esplit; eauto). - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split; - [ instantiate (1 := (PLoadRRO _ x)); simpl; reflexivity + [ instantiate (1 := (PLoadRRO _ _ x)); simpl; reflexivity | eauto ]. - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split; - [ instantiate (1 := (PLoadRRO _ x)); simpl; reflexivity + [ instantiate (1 := (PLoadRRO _ _ x)); simpl; reflexivity | eauto ]. Qed. -Lemma transl_load_memory_access2_ok: - forall addr chunk args dst k c rs a v m, - addr = Aindexed2 -> - transl_load chunk addr args dst k = OK c -> +Lemma transl_load_memory_access_ok_notrap2: + forall addr chunk args dst k c rs a m, + (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) -> + transl_load NOTRAP chunk addr args dst k = OK c -> eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a -> + Mem.loadv chunk m a = None -> + exists mk_instr rd, + preg_of dst = IR rd + /\ transl_memory_access mk_instr addr args k = OK c + /\ forall base ofs rs, + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset NOTRAP chunk rs m rd base ofs. +Proof. + intros until m. intros ADDR TR ? ?. + unfold transl_load in TR. destruct addr; try contradiction. + - monadInv TR. destruct chunk; ArgsInv; econstructor; (esplit; eauto). + - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split; + [ instantiate (1 := (PLoadRRO _ _ x)); simpl; reflexivity + | eauto ]. + - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split; + [ instantiate (1 := (PLoadRRO _ _ x)); simpl; reflexivity + | eauto ]. +Qed. + +Lemma transl_load_memory_access2_ok: + forall trap chunk args dst k c rs a v m, + transl_load trap chunk Aindexed2 args dst k = OK c -> + eval_addressing ge (rs (IR SP)) Aindexed2 (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> exists mk_instr mr0 mro rd ro, args = mr0 :: mro :: nil /\ preg_of dst = IR rd /\ preg_of mro = IR ro - /\ transl_memory_access2 mk_instr addr args k = OK c + /\ transl_memory_access2 mk_instr Aindexed2 args k = OK c /\ forall base rs, - exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg chunk rs m rd base ro. + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg trap chunk rs m rd base ro. Proof. - intros until m. intros ? TR ? ?. + intros until m. intros TR ? ?. unfold transl_load in TR. subst. monadInv TR. destruct chunk. all: unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists; [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity - | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRR _ x)); simpl; reflexivity + | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRR _ _ x)); simpl; reflexivity + | eauto]. +Qed. + + +Lemma transl_load_memory_access2_ok_notrap2: + forall chunk args dst k c rs a m, + transl_load NOTRAP chunk Aindexed2 args dst k = OK c -> + eval_addressing ge (rs (IR SP)) Aindexed2 (map rs (map preg_of args)) = Some a -> + Mem.loadv chunk m a = None -> + exists mk_instr mr0 mro rd ro, + args = mr0 :: mro :: nil + /\ preg_of dst = IR rd + /\ preg_of mro = IR ro + /\ transl_memory_access2 mk_instr Aindexed2 args k = OK c + /\ forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg NOTRAP chunk rs m rd base ro. +Proof. + intros until m. intros TR ? ?. + unfold transl_load in TR. subst. monadInv TR. destruct chunk. all: + unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists; + [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity + | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRR _ _ x)); simpl; reflexivity | eauto]. Qed. Lemma transl_load_memory_access2XS_ok: - forall scale chunk args dst k c rs a v m, - transl_load chunk (Aindexed2XS scale) args dst k = OK c -> + forall scale trap chunk args dst k c rs a v m, + transl_load trap chunk (Aindexed2XS scale) args dst k = OK c -> eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> exists mk_instr mr0 mro rd ro, @@ -2002,19 +2118,41 @@ Lemma transl_load_memory_access2XS_ok: /\ preg_of mro = IR ro /\ transl_memory_access2XS chunk mk_instr scale args k = OK c /\ forall base rs, - exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs chunk rs m rd base ro. + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs trap chunk rs m rd base ro. Proof. intros until m. intros TR ? ?. unfold transl_load in TR. subst. monadInv TR. destruct chunk. all: unfold transl_memory_access2XS in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists; [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity - | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRRXS _ x)); simpl; rewrite Heqb; eauto + | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRRXS _ _ x)); simpl; rewrite Heqb; eauto + | eauto]. +Qed. + + +Lemma transl_load_memory_access2XS_ok_notrap2: + forall scale chunk args dst k c rs a m, + transl_load NOTRAP chunk (Aindexed2XS scale) args dst k = OK c -> + eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a -> + Mem.loadv chunk m a = None -> + exists mk_instr mr0 mro rd ro, + args = mr0 :: mro :: nil + /\ preg_of dst = IR rd + /\ preg_of mro = IR ro + /\ transl_memory_access2XS chunk mk_instr scale args k = OK c + /\ forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs NOTRAP chunk rs m rd base ro. +Proof. + intros until m. intros TR ? ?. + unfold transl_load in TR. subst. monadInv TR. destruct chunk. all: + unfold transl_memory_access2XS in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists; + [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity + | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRRXS _ _ x)); simpl; rewrite Heqb; eauto | eauto]. Qed. Lemma transl_load_correct: - forall chunk addr args dst k c (rs: regset) m a v, - transl_load chunk addr args dst k = OK c -> + forall trap chunk addr args dst k c (rs: regset) m a v, + transl_load trap chunk addr args dst k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> exists rs', @@ -2038,6 +2176,32 @@ Proof. eapply transl_load_access_correct; eauto with asmgen. Qed. +Lemma transl_load_correct_notrap2: + forall chunk addr args dst k c (rs: regset) m a, + transl_load NOTRAP chunk addr args dst k = OK c -> + eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a -> + Mem.loadv chunk m a = None -> + exists rs', + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m + /\ rs'#(preg_of dst) = (concrete_default_notrap_load_value chunk) + /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r. +Proof. + intros until a; intros TR EV LOAD. destruct addr. + - exploit transl_load_memory_access2XS_ok_notrap2; eauto. intros (mk_instr & mr0 & mro & rd & ro & argsEq & rdEq & roEq & B & C). + rewrite rdEq. eapply transl_load_access2XS_correct_notrap2; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. + - exploit transl_load_memory_access2_ok_notrap2; eauto. intros (mk_instr & mr0 & mro & rd & ro & argsEq & rdEq & roEq & B & C). + rewrite rdEq. eapply transl_load_access2_correct_notrap2; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. + - exploit transl_load_memory_access_ok_notrap2; eauto; try discriminate; try (simpl; reflexivity). + intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq; + eapply transl_load_access_correct_notrap2; eauto with asmgen. + - exploit transl_load_memory_access_ok_notrap2; eauto; try discriminate; try (simpl; reflexivity). + intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq; + eapply transl_load_access_correct_notrap2; eauto with asmgen. + - exploit transl_load_memory_access_ok_notrap2; eauto; try discriminate; try (simpl; reflexivity). + intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq; + eapply transl_load_access_correct_notrap2; eauto with asmgen. +Qed. + Lemma transl_store_access2_correct: forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c r1 (rs: regset) m v mr1 mro ro m', args = mr1 :: mro :: nil -> diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index 9c256bd0..37bfbed9 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -190,10 +190,10 @@ let expand_builtin_memcpy_big sz al src dst = end); cpy tmpbuf2 16L (fun x y z -> Plq(x, y, z)) (fun x y z -> Psq(x, y, z)); - cpy tmpbuf 8L (fun x y z -> Pld(x, y, z)) (fun x y z -> Psd(x, y, z)); - cpy tmpbuf 4L (fun x y z -> Plw(x, y, z)) (fun x y z -> Psw(x, y, z)); - cpy tmpbuf 2L (fun x y z -> Plh(x, y, z)) (fun x y z -> Psh(x, y, z)); - cpy tmpbuf 1L (fun x y z -> Plb(x, y, z)) (fun x y z -> Psb(x, y, z)); + cpy tmpbuf 8L (fun x y z -> Pld(TRAP, x, y, z)) (fun x y z -> Psd(x, y, z)); + cpy tmpbuf 4L (fun x y z -> Plw(TRAP, x, y, z)) (fun x y z -> Psw(x, y, z)); + cpy tmpbuf 2L (fun x y z -> Plh(TRAP, x, y, z)) (fun x y z -> Psh(x, y, z)); + cpy tmpbuf 1L (fun x y z -> Plb(TRAP, x, y, z)) (fun x y z -> Psb(x, y, z)); assert (!remaining = 0L) end else @@ -203,7 +203,7 @@ let expand_builtin_memcpy_big sz al src dst = let lbl = new_label() in emit (Ploopdo (tmpbuf, lbl)); emit Psemi; - emit (Plb (tmpbuf, srcptr, AOff Z.zero)); + emit (Plb (TRAP, tmpbuf, srcptr, AOff Z.zero)); emit (Paddil (srcptr, srcptr, Z.one)); emit Psemi; emit (Psb (tmpbuf, dstptr, AOff Z.zero)); @@ -223,30 +223,30 @@ let expand_builtin_memcpy sz al args = let expand_builtin_vload_common chunk base ofs res = match chunk, res with | Mint8unsigned, BR(Asmvliw.IR res) -> - emit (Plbu (res, base, AOff ofs)) + emit (Plbu (TRAP, res, base, AOff ofs)) | Mint8signed, BR(Asmvliw.IR res) -> - emit (Plb (res, base, AOff ofs)) + emit (Plb (TRAP, res, base, AOff ofs)) | Mint16unsigned, BR(Asmvliw.IR res) -> - emit (Plhu (res, base, AOff ofs)) + emit (Plhu (TRAP, res, base, AOff ofs)) | Mint16signed, BR(Asmvliw.IR res) -> - emit (Plh (res, base, AOff ofs)) + emit (Plh (TRAP, res, base, AOff ofs)) | Mint32, BR(Asmvliw.IR res) -> - emit (Plw (res, base, AOff ofs)) + emit (Plw (TRAP, res, base, AOff ofs)) | Mint64, BR(Asmvliw.IR res) -> - emit (Pld (res, base, AOff ofs)) + emit (Pld (TRAP, res, base, AOff ofs)) | Mint64, BR_splitlong(BR(Asmvliw.IR res1), BR(Asmvliw.IR res2)) -> let ofs' = Integers.Ptrofs.add ofs _4 in if base <> res2 then begin - emit (Plw (res2, base, AOff ofs)); - emit (Plw (res1, base, AOff ofs')) + emit (Plw (TRAP, res2, base, AOff ofs)); + emit (Plw (TRAP, res1, base, AOff ofs')) end else begin - emit (Plw (res1, base, AOff ofs')); - emit (Plw (res2, base, AOff ofs)) + emit (Plw (TRAP, res1, base, AOff ofs')); + emit (Plw (TRAP, res2, base, AOff ofs)) end | Mfloat32, BR(Asmvliw.IR res) -> - emit (Pfls (res, base, AOff ofs)) + emit (Pfls (TRAP, res, base, AOff ofs)) | Mfloat64, BR(Asmvliw.IR res) -> - emit (Pfld (res, base, AOff ofs)) + emit (Pfld (TRAP, res, base, AOff ofs)) | _ -> assert false diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 54e9c847..e042d95a 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -308,6 +308,16 @@ Inductive cf_instruction : Type := . (** Loads **) +Definition concrete_default_notrap_load_value (chunk : memory_chunk) := + match chunk with + | Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned + | Mint32 => Vint Int.zero + | Mint64 => Vlong Int64.zero + | Many32 | Many64 => Vundef + | Mfloat32 => Vsingle Float32.zero + | Mfloat64 => Vfloat Float.zero + end. + Inductive load_name : Type := | Plb (**r load byte *) | Plbu (**r load byte unsigned *) @@ -322,9 +332,9 @@ Inductive load_name : Type := . Inductive ld_instruction : Type := - | PLoadRRO (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset) - | PLoadRRR (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) - | PLoadRRRXS (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) + | PLoadRRO (trap: trapping_mode) (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset) + | PLoadRRR (trap: trapping_mode) (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) + | PLoadRRRXS (trap: trapping_mode) (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) | PLoadQRRO (rd: gpreg_q) (ra: ireg) (ofs: offset) | PLoadORRO (rd: gpreg_o) (ra: ireg) (ofs: offset) . @@ -1202,10 +1212,16 @@ Definition eval_offset (ofs: offset) : res ptrofs := OK ofs. (** * load/store *) -Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) := +Definition parexec_incorrect_load trap chunk d rsw mw := + match trap with + | TRAP => Stuck + | NOTRAP => Next (rsw#d <- (concrete_default_notrap_load_value chunk)) mw + end. + +Definition parexec_load_offset (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) := match (eval_offset ofs) with | OK ptr => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with - | None => Stuck + | None => parexec_incorrect_load trap chunk d rsw mw | Some v => Next (rsw#d <- v) mw end | _ => Stuck @@ -1250,15 +1266,15 @@ Definition parexec_load_o_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_o) (a end end. -Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) := +Definition parexec_load_reg (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) := match Mem.loadv chunk mr (Val.addl (rsr a) (rsr ro)) with - | None => Stuck + | None => parexec_incorrect_load trap chunk d rsw mw | Some v => Next (rsw#d <- v) mw end. -Definition parexec_load_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) := +Definition parexec_load_regxs (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) := match Mem.loadv chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) with - | None => Stuck + | None => parexec_incorrect_load trap chunk d rsw mw | Some v => Next (rsw#d <- v) mw end. @@ -1271,7 +1287,8 @@ Definition parexec_store_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: | _ => Stuck end. -Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) := +Definition parexec_store_reg + (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) := match Mem.storev chunk mr (Val.addl (rsr a) (rsr ro)) (rsr s) with | None => Stuck | Some m' => Next rsw m' @@ -1329,7 +1346,7 @@ Definition load_chunk n := | Pfls => Mfloat32 | Pfld => Mfloat64 end. - + Definition store_chunk n := match n with | Psb => Mint8unsigned @@ -1348,12 +1365,12 @@ Definition bstep (bi: basic) (rsr rsw: regset) (mr mw: mem) := match bi with | PArith ai => Next (parexec_arith_instr ai rsr rsw) mw - | PLoadRRO n d a ofs => parexec_load_offset (load_chunk n) rsr rsw mr mw d a ofs - | PLoadRRR n d a ro => parexec_load_reg (load_chunk n) rsr rsw mr mw d a ro - | PLoadRRRXS n d a ro => parexec_load_regxs (load_chunk n) rsr rsw mr mw d a ro - | PLoadQRRO d a ofs => + | PLoad (PLoadRRO trap n d a ofs) => parexec_load_offset trap (load_chunk n) rsr rsw mr mw d a ofs + | PLoad (PLoadRRR trap n d a ro) => parexec_load_reg trap (load_chunk n) rsr rsw mr mw d a ro + | PLoad (PLoadRRRXS trap n d a ro) => parexec_load_regxs trap (load_chunk n) rsr rsw mr mw d a ro + | PLoad (PLoadQRRO d a ofs) => parexec_load_q_offset rsr rsw mr mw d a ofs - | PLoadORRO d a ofs => + | PLoad (PLoadORRO d a ofs) => parexec_load_o_offset rsr rsw mr mw d a ofs | PStoreRRO n s a ofs => parexec_store_offset (store_chunk n) rsr rsw mr mw s a ofs diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index f9a774e8..7aea2929 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -1706,6 +1706,27 @@ Proof. - apply Val.offset_ptr_inject; auto. 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 *. + 1,2: inv Hinjvl; trivial; + inv H0; trivial; + inv H2; trivial; + discriminate. + 2,3: inv Hinjvl; trivial; discriminate. + inv Hinjvl; trivial; inv H0; trivial; + inv H; trivial; discriminate. +Qed. + End EVAL_COMPAT. (** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *) @@ -1812,6 +1833,24 @@ 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 *. + 1, 2, 4, 5: inv Hlessdef; trivial; + inv H0; trivial; + inv H2; trivial; + discriminate. + inv Hlessdef; trivial. + inv H0; trivial. + discriminate. +Qed. + End EVAL_LESSDEF. (** Compatibility of the evaluation functions with memory injections. *) @@ -1864,6 +1903,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/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index 7c8f65a8..0611fdda 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -2,6 +2,7 @@ Require Import Coqlib. Require Import Asmvliw. Require Import Values. Require Import Integers. +Require Import AST. Require Compopts. Definition gpreg_q_list : list gpreg_q := @@ -89,8 +90,8 @@ Fixpoint coalesce_mem (insns : list basic) : list basic := | None => h0 :: (coalesce_mem t0) end - | (PLoadRRO Pld_a rd0 ra0 ofs0), - (PLoadRRO Pld_a rd1 ra1 ofs1) => + | (PLoad (PLoadRRO TRAP Pld_a rd0 ra0 ofs0)), + (PLoad (PLoadRRO TRAP Pld_a rd1 ra1 ofs1)) => match gpreg_q_search rd0 rd1 with | Some rd0rd1 => let zofs0 := Ptrofs.signed ofs0 in @@ -100,8 +101,8 @@ Fixpoint coalesce_mem (insns : list basic) : list basic := if coalesce_octuples then match t1 with - | (PLoadRRO Pld_a rd2 ra2 ofs2) :: - (PLoadRRO Pld_a rd3 ra3 ofs3) :: t3 => + | (PLoad (PLoadRRO TRAP Pld_a rd2 ra2 ofs2)) :: + (PLoad (PLoadRRO TRAP Pld_a rd3 ra3 ofs3)) :: t3 => match gpreg_o_search rd0 rd1 rd2 rd3 with | Some octuple => let zofs2 := Ptrofs.signed ofs2 in diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 327901f3..cdda0e6d 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -302,7 +302,7 @@ let arith_rec i = | PArithR (i, rd) -> arith_r_rec i (IR rd) let load_rec i = match i with - | PLoadRRO (i, rs1, rs2, imm) -> + | PLoadRRO (trap, i, rs1, rs2, imm) -> { inst = load_real i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2)]; imm = (Some (Off imm)) ; is_control = false; read_at_id = []; read_at_e1 = [] } | PLoadQRRO(rs, ra, imm) -> @@ -313,7 +313,7 @@ let load_rec i = match i with let (((rs0, rs1), rs2), rs3) = gpreg_o_expand rs in { inst = loadorro_real; write_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; read_locs = [Mem; Reg (IR ra)]; imm = (Some (Off imm)) ; is_control = false; read_at_id = []; read_at_e1 = []} - | PLoadRRR (i, rs1, rs2, rs3) | PLoadRRRXS (i, rs1, rs2, rs3) -> + | PLoadRRR (trap, i, rs1, rs2, rs3) | PLoadRRRXS (trap, i, rs1, rs2, rs3) -> { inst = load_real i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2); Reg (IR rs3)]; imm = None ; is_control = false; read_at_id = []; read_at_e1 = [] } diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 21af276b..867c10c5 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -96,36 +96,42 @@ Proof. Qed. Lemma exec_load_offset_pc_var: - forall t rs m rd ra ofs rs' m' v, - exec_load_offset t rs m rd ra ofs = Next rs' m' -> - exec_load_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. + forall trap t rs m rd ra ofs rs' m' v, + exec_load_offset trap t rs m rd ra ofs = Next rs' m' -> + exec_load_offset trap t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. + - unfold parexec_incorrect_load in *. + destruct trap; try discriminate. + inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. Qed. Lemma exec_load_reg_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_load_reg t rs m rd ra ro = Next rs' m' -> - exec_load_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. + forall trap t rs m rd ra ro rs' m' v, + exec_load_reg trap t rs m rd ra ro = Next rs' m' -> + exec_load_reg trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. Proof. intros. unfold exec_load_reg in *. unfold parexec_load_reg in *. rewrite Pregmap.gso; try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. + - unfold parexec_incorrect_load in *. + destruct trap; try discriminate. + inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. Qed. Lemma exec_load_regxs_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_load_regxs t rs m rd ra ro = Next rs' m' -> - exec_load_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. + forall trap t rs m rd ra ro rs' m' v, + exec_load_regxs trap t rs m rd ra ro = Next rs' m' -> + exec_load_regxs trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. Proof. intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. + - unfold parexec_incorrect_load in *. + destruct trap; try discriminate. + inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. Qed. Lemma exec_load_offset_q_pc_var: diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 0c179a07..930b1c51 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -251,6 +251,10 @@ module Target (*: TARGET*) = | ARegXS _ -> fprintf oc ".xs" | _ -> () + let lsvariant oc = function + | TRAP -> () + | NOTRAP -> output_string oc ".s" + let icond_name = let open Asmvliw in function | ITne | ITneu -> "ne" | ITeq | ITequ -> "eq" @@ -420,18 +424,18 @@ module Target (*: TARGET*) = section oc Section_text (* Load/Store instructions *) - | Plb(rd, ra, adr) -> - fprintf oc " lbs%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra - | Plbu(rd, ra, adr) -> - fprintf oc " lbz%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra - | Plh(rd, ra, adr) -> - fprintf oc " lhs%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra - | Plhu(rd, ra, adr) -> - fprintf oc " lhz%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra - | Plw(rd, ra, adr) | Plw_a(rd, ra, adr) | Pfls(rd, ra, adr) -> - fprintf oc " lws%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra - | Pld(rd, ra, adr) | Pfld(rd, ra, adr) | Pld_a(rd, ra, adr) -> assert Archi.ptr64; - fprintf oc " ld%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra + | Plb(trap, rd, ra, adr) -> + fprintf oc " lbs%a%a %a = %a[%a]\n" lsvariant trap xscale adr ireg rd addressing adr ireg ra + | Plbu(trap, rd, ra, adr) -> + fprintf oc " lbz%a%a %a = %a[%a]\n" lsvariant trap xscale adr ireg rd addressing adr ireg ra + | Plh(trap, rd, ra, adr) -> + fprintf oc " lhs%a%a %a = %a[%a]\n" lsvariant trap xscale adr ireg rd addressing adr ireg ra + | Plhu(trap, rd, ra, adr) -> + fprintf oc " lhz%a%a %a = %a[%a]\n" lsvariant trap xscale adr ireg rd addressing adr ireg ra + | Plw(trap, rd, ra, adr) | Plw_a(trap, rd, ra, adr) | Pfls(trap, rd, ra, adr) -> + fprintf oc " lws%a%a %a = %a[%a]\n" lsvariant trap xscale adr ireg rd addressing adr ireg ra + | Pld(trap, rd, ra, adr) | Pfld(trap, rd, ra, adr) | Pld_a(trap, rd, ra, adr) -> assert Archi.ptr64; + fprintf oc " ld%a%a %a = %a[%a]\n" lsvariant trap xscale adr ireg rd addressing adr ireg ra | Plq(rd, ra, adr) -> fprintf oc " lq%a %a = %a[%a]\n" xscale adr gpreg_q rd addressing adr ireg ra | Plo(rd, ra, adr) -> diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 2c9bdf3e..7d84447e 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -472,6 +472,24 @@ Proof. rewrite Ptrofs.add_zero_l; eauto with va. 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. + inv Hlist. + destruct addr; trivial; discriminate. + inv H0. + destruct addr; trivial; discriminate. + inv H2. + destruct addr; trivial; discriminate. + inv H3; + destruct addr; trivial; discriminate. +Qed. + Theorem eval_static_operation_sound: forall op vargs m vres aargs, eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres -> diff --git a/mppa_k1c/lib/Machblock.v b/mppa_k1c/lib/Machblock.v index 2759c49d..5a7f1782 100644 --- a/mppa_k1c/lib/Machblock.v +++ b/mppa_k1c/lib/Machblock.v @@ -20,7 +20,7 @@ Inductive basic_inst: Type := | MBsetstack: mreg -> ptrofs -> typ -> basic_inst | MBgetparam: ptrofs -> typ -> mreg -> basic_inst | MBop: operation -> list mreg -> mreg -> basic_inst - | MBload: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst + | MBload: trapping_mode -> memory_chunk -> addressing -> list mreg -> mreg -> basic_inst | MBstore: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst . @@ -207,11 +207,22 @@ Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m: rs' = ((undef_regs (destroyed_by_op op) rs)#res <- v) -> basic_step s fb sp rs m (MBop op args res) rs' m | exec_MBload: - forall addr args a v rs' chunk dst, + forall addr args a v rs' trap chunk dst, eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- v) -> - basic_step s fb sp rs m (MBload chunk addr args dst) rs' m + basic_step s fb sp rs m (MBload trap chunk addr args dst) rs' m + | exec_MBload_notrap1: + forall addr args rs' chunk dst, + eval_addressing ge sp addr rs##args = None -> + rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) -> + basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m + | exec_MBload_notrap2: + forall addr args a rs' chunk dst, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = None -> + rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) -> + basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m | exec_MBstore: forall chunk addr args src m' a rs', eval_addressing ge sp addr rs##args = Some a -> diff --git a/mppa_k1c/lib/Machblockgen.v b/mppa_k1c/lib/Machblockgen.v index db48934e..a65b218f 100644 --- a/mppa_k1c/lib/Machblockgen.v +++ b/mppa_k1c/lib/Machblockgen.v @@ -33,7 +33,7 @@ Definition trans_inst (i:Mach.instruction) : Machblock_inst := | Msetstack src ofs ty => MB_basic (MBsetstack src ofs ty) | Mgetparam ofs ty dst => MB_basic (MBgetparam ofs ty dst) | Mop op args res => MB_basic (MBop op args res) - | Mload chunk addr args dst => MB_basic (MBload chunk addr args dst) + | Mload trap chunk addr args dst=> MB_basic (MBload trap chunk addr args dst) | Mstore chunk addr args src => MB_basic (MBstore chunk addr args src) | Mlabel l => MB_label l end. diff --git a/mppa_k1c/lib/Machblockgenproof.v b/mppa_k1c/lib/Machblockgenproof.v index ab7fff74..02d154c7 100644 --- a/mppa_k1c/lib/Machblockgenproof.v +++ b/mppa_k1c/lib/Machblockgenproof.v @@ -483,6 +483,10 @@ Proof. unfold Genv.symbol_address; rewrite symbols_preserved; auto. - eapply exec_MBload; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. + - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + unfold Genv.symbol_address; rewrite symbols_preserved; auto. + - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + unfold Genv.symbol_address; rewrite symbols_preserved; auto. - eapply exec_MBstore; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. Qed. diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index a686414a..29e2c028 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -783,8 +783,13 @@ Definition transl_memory_access Error(msg "Asmgen.transl_memory_access") end. -Definition transl_load (chunk: memory_chunk) (addr: addressing) - (args: list mreg) (dst: mreg) (k: code) := +Definition transl_load + (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (dst: mreg) (k: code) := + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on PPC") + | TRAP => match chunk with | Mint8signed => do r <- ireg_of dst; @@ -812,6 +817,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k | _ => Error (msg "Asmgen.transl_load") + end end. Definition transl_store (chunk: memory_chunk) (addr: addressing) @@ -869,8 +875,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) loadind GPR1 f.(fn_link_ofs) Tint R11 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 r) => diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index d653633c..21d5ce48 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -328,6 +328,7 @@ Proof. eapply loadind_label; eauto. eapply tail_nolabel_trans; eapply loadind_label; eauto. eapply transl_op_label; eauto. + destruct t; try discriminate. destruct m; monadInv H; (eapply tail_nolabel_trans; [eapply transl_memory_access_label; TailNoLabel|TailNoLabel]). destruct m; monadInv H; eapply transl_memory_access_label; TailNoLabel. destruct s0; monadInv H; TailNoLabel. @@ -657,6 +658,13 @@ Opaque loadind. split. simpl; congruence. apply R; auto with asmgen. + +- (* 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/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 884d5366..6ceb7f85 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1677,8 +1677,8 @@ Qed. (** Translation of loads *) Lemma transl_load_correct: - forall chunk addr args dst k c (rs: regset) m a v, - transl_load chunk addr args dst k = OK c -> + forall trap chunk addr args dst k c (rs: regset) m a v, + transl_load trap chunk addr args dst k = OK c -> eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> exists rs', @@ -1687,6 +1687,7 @@ Lemma transl_load_correct: /\ forall r, r <> PC -> r <> GPR12 -> r <> GPR0 -> r <> preg_of dst -> rs' r = rs r. Proof. intros. + destruct trap; try discriminate. assert (LD: forall v, Val.lessdef a v -> v = a). { intros. inv H2; auto. discriminate H1. } assert (BASE: forall mk1 mk2 k' chunk' v', diff --git a/powerpc/Op.v b/powerpc/Op.v index 0f082c1f..cbd0291b 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -1032,6 +1032,21 @@ Proof. apply Val.add_inject; auto. apply H; simpl; auto. 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. End EVAL_COMPAT. (** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *) @@ -1098,6 +1113,20 @@ Proof. rewrite <- val_inject_list_lessdef. eauto. 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. + Lemma eval_operation_lessdef: forall sp op vl1 vl2 v1 m1 m2, Val.lessdef_list vl1 vl2 -> @@ -1189,6 +1218,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/riscV/Asmgen.v b/riscV/Asmgen.v index a704ed74..ecaca7b3 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -770,9 +770,13 @@ Definition transl_memory_access Error(msg "Asmgen.transl_memory_access") end. -Definition transl_load (chunk: memory_chunk) (addr: addressing) +Definition transl_load (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: code) := - match chunk with + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm") + | TRAP => + match chunk with | Mint8signed => do r <- ireg_of dst; transl_memory_access (Plb r) addr args k @@ -799,6 +803,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access (Pfld r) addr args k | _ => Error (msg "Asmgen.transl_load") + end end. Definition transl_store (chunk: memory_chunk) (addr: addressing) @@ -848,8 +853,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) else loadind_ptr SP f.(fn_link_ofs) X30 c) | 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 r) => diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 5ec57886..e2fafb16 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -359,7 +359,7 @@ Proof. - destruct ep. eapply loadind_label; eauto. eapply tail_nolabel_trans. apply loadind_ptr_label. eapply loadind_label; eauto. - eapply transl_op_label; eauto. -- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. +- destruct t; (try discriminate); destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. - destruct s0; monadInv H; TailNoLabel. - destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]). @@ -725,6 +725,12 @@ Local Transparent destroyed_by_op. intros; auto with asmgen. 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 (map rs args) = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 98d5bd33..175e484f 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1318,8 +1318,8 @@ Proof. Qed. Lemma transl_load_correct: - forall chunk addr args dst k c (rs: regset) m a v, - transl_load chunk addr args dst k = OK c -> + forall trap chunk addr args dst k c (rs: regset) m a v, + transl_load trap chunk addr args dst k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> exists rs', @@ -1327,7 +1327,8 @@ Lemma transl_load_correct: /\ rs'#(preg_of dst) = v /\ forall r, r <> PC -> r <> X31 -> r <> preg_of dst -> rs'#r = rs#r. Proof. - intros until v; intros TR EV LOAD. + intros until v; intros TR EV LOAD. + destruct trap; try (simpl in *; discriminate). assert (A: exists mk_instr, transl_memory_access mk_instr addr args k = OK c /\ forall base ofs rs, @@ -1159,6 +1159,20 @@ Proof. apply Val.offset_ptr_inject; auto. 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. End EVAL_COMPAT. (** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *) @@ -1265,6 +1279,18 @@ 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. *) @@ -1317,6 +1343,20 @@ 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/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. |