From c3d719b7ecd4bf2e1cfaee6e619f3ec8e3fe7e10 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 10 May 2019 14:22:40 +0200 Subject: Asmblockgen prologue is now 1 basicblock (instead of 3) --- mppa_k1c/Asmblockgen.v | 9 ++--- mppa_k1c/Asmblockgenproof.v | 80 +++++++++++++++++++++++++------------------- mppa_k1c/Asmblockgenproof1.v | 47 ++++++++++++-------------- 3 files changed, 72 insertions(+), 64 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index f2292f9a..a4364051 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -1113,10 +1113,11 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: end . -Definition make_prologue (f: Machblock.function) lb := - (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b - Pget GPRA RA ::b - storeind_ptr GPRA SP f.(fn_retaddr_ofs) ::b lb). +Program Definition make_prologue (f: Machblock.function) lb := + ({| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::i + Pget GPRA RA ::i + storeind_ptr GPRA SP f.(fn_retaddr_ofs) ::i nil; + exit := None |} :: lb). Definition transl_function (f: Machblock.function) := do lb <- transl_blocks f f.(Machblock.fn_code) true; diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 0233a3dc..c44ef3ff 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -17,6 +17,7 @@ Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Machblock Conventions Asmblock. Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1. +Require Import Axioms. Module MB := Machblock. Module AB := Asmvliw. @@ -1100,7 +1101,7 @@ Proof. destruct ep eqn:EPeq. (* RTMP contains parent *) + exploit loadind_correct. eexact EQ1. - instantiate (2 := rs1). rewrite DXP; eauto. congruence. + instantiate (2 := rs1). rewrite DXP; eauto. intros [rs2 [P [Q R]]]. eapply exec_straight_body in P. @@ -1121,8 +1122,8 @@ Proof. (* GPR11 does not contain parent *) + rewrite chunk_of_Tptr in A. - exploit loadind_ptr_correct. eexact A. congruence. intros [rs2 [P [Q R]]]. - exploit loadind_correct. eexact EQ1. instantiate (2 := rs2). rewrite Q. eauto. congruence. + exploit loadind_ptr_correct. eexact A. intros [rs2 [P [Q R]]]. + exploit loadind_correct. eexact EQ1. instantiate (2 := rs2). rewrite Q. eauto. intros [rs3 [S [T U]]]. exploit exec_straight_trans. @@ -1593,6 +1594,12 @@ Proof. congruence. Qed. +Lemma next_sep: + forall rs m rs' m', rs = rs' -> m = m' -> Next rs m = Next rs' m'. +Proof. + congruence. +Qed. + Theorem step_simulation: forall S1 t S2, MB.step return_address_offset ge S1 t S2 -> forall S1' (MS: match_states S1 S1'), @@ -1648,55 +1655,58 @@ Proof. intros [m3' [P Q]]. (* Execution of function prologue *) monadInv EQ0. (* rewrite transl_code'_transl_code in EQ1. *) - set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::b - Pget GPRA RA ::b - storeind_ptr GPRA SP (fn_retaddr_ofs f) ::b x0) in *. + set (tfbody := make_prologue f x0) in *. set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *. - set (rs2 := nextblock (bblock_single_inst (Pallocframe (fn_stacksize f) (fn_link_ofs f))) - (rs0#FP <- (parent_sp s) #SP <- sp #RTMP <- Vundef)). + set (rs2 := rs0#FP <- (parent_sp s) #SP <- sp #RTMP <- Vundef). exploit (Pget_correct tge GPRA RA nil rs2 m2'); auto. intros (rs' & U' & V'). - exploit (exec_straight_through_singleinst); eauto. - intro W'. remember (nextblock _ rs') as rs''. - exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs'' m2'). +(* exploit (exec_straight_through_singleinst); eauto. + intro W'. remember (nextblock _ rs') as rs''. *) + exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs' m2'). rewrite chunk_of_Tptr in P. assert (rs' GPRA = rs0 RA). { apply V'. } - assert (rs'' GPRA = rs' GPRA). { subst. Simpl. } assert (rs' SP = rs2 SP). { apply V'; discriminate. } - assert (rs'' SP = rs' SP). { subst. Simpl. } - rewrite H4. rewrite H3. rewrite H6. rewrite H5. + rewrite H4. rewrite H3. (* change (rs' GPRA) with (rs0 RA). *) rewrite ATLR. change (rs2 SP) with sp. eexact P. - congruence. congruence. intros (rs3 & U & V). - exploit (exec_straight_through_singleinst); eauto. - intro W. - remember (nextblock _ rs3) as rs3'. - assert (EXEC_PROLOGUE: +(* exploit (exec_straight_through_singleinst); eauto. + intro W. *) + assert (EXEC_PROLOGUE: exists rs3', exec_straight_blocks tge tf tf.(fn_blocks) rs0 m' - x0 rs3' m3'). - { change (fn_blocks tf) with tfbody; unfold tfbody. - apply exec_straight_blocks_step with rs2 m2'. - unfold exec_bblock. simpl exec_body. rewrite C. fold sp. simpl exec_control. - rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. rewrite regset_same_assign. reflexivity. - reflexivity. - eapply exec_straight_blocks_trans. - - eexact W'. - - eexact W. } + x0 rs3' m3' + /\ forall r, r <> PC -> rs3' r = rs3 r). + { eexists. split. + - change (fn_blocks tf) with tfbody; unfold tfbody. + econstructor; eauto. unfold exec_bblock. simpl exec_body. + rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. + Simpl. unfold parexec_store_offset. rewrite Ptrofs.of_int64_to_int64. unfold eval_offset. + rewrite chunk_of_Tptr in P. Simpl. rewrite ATLR. unfold Mptr in P. assert (Archi.ptr64 = true) by auto. 2: auto. rewrite H3 in P. rewrite P. + simpl. apply next_sep; eauto. reflexivity. + - intros. destruct V' as (V'' & V'). destruct r. + + Simpl. + destruct (gpreg_eq g0 GPR16). { subst. Simpl. rewrite V; try discriminate. rewrite V''. subst rs2. Simpl. } + destruct (gpreg_eq g0 GPR32). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. } + destruct (gpreg_eq g0 GPR12). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. } + destruct (gpreg_eq g0 GPR17). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. } + Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. { destruct g0; try discriminate. contradiction. } + + Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. + + contradiction. + } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3'). exploit exec_straight_steps_2; eauto using functions_transl. - simpl fn_blocks. unfold make_prologue in g. simpl fn_blocks in g. unfold tfbody. simpl bblock_single_inst. omega. constructor. + simpl fn_blocks. simpl fn_blocks in g. omega. constructor. intros (ofs' & X & Y). left; exists (State rs3' m3'); split. eapply exec_straight_steps_1; eauto. - simpl fn_blocks. unfold make_prologue in g. simpl fn_blocks in g. unfold tfbody. simpl bblock_single_inst. omega. + simpl fn_blocks. simpl fn_blocks in g. omega. constructor. econstructor; eauto. rewrite X; econstructor; eauto. apply agree_exten with rs2; eauto with asmgen. unfold rs2. - apply agree_nextblock. apply agree_set_other; auto with asmgen. + apply agree_set_other; auto with asmgen. apply agree_change_sp with (parent_sp s). apply agree_undef_regs with rs0. auto. Local Transparent destroyed_at_function_entry. @@ -1705,17 +1715,17 @@ Local Transparent destroyed_at_function_entry. intros. assert (r <> RTMP). { contradict H3; rewrite H3; unfold data_preg; auto. } - rewrite Heqrs3'. Simpl. rewrite V. rewrite Heqrs''. Simpl. inversion V'. rewrite H6. auto. + rewrite Heqrs3'. Simpl. rewrite V. inversion V'. rewrite H6. auto. assert (r <> GPRA). { contradict H3; rewrite H3; unfold data_preg; auto. } assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. } (* rewrite H8; auto. *) contradict H3; rewrite H3; unfold data_preg; auto. contradict H3; rewrite H3; unfold data_preg; auto. contradict H3; rewrite H3; unfold data_preg; auto. - auto. intros. rewrite Heqrs3'. Simpl. rewrite V by auto with asmgen. + contradict H3; rewrite H3; unfold data_preg; auto. + intros. rewrite Heqrs3'. rewrite V by auto with asmgen. assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. } - rewrite Heqrs''. Simpl. - rewrite H4 by auto with asmgen. reflexivity. + rewrite H4 by auto with asmgen. reflexivity. discriminate. - (* external function *) inv MS. exploit functions_translated; eauto. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 86a0ff88..3c1162bd 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1969,13 +1969,12 @@ Qed. Lemma indexed_memory_access_correct: forall mk_instr base ofs k rs m, - base <> RTMP -> exists base' ofs' rs' ptr', exec_straight_opt (indexed_memory_access mk_instr base ofs ::g k) rs m (mk_instr base' ofs' ::g k) rs' m /\ eval_offset ofs' = OK ptr' /\ Val.offset_ptr rs'#base' ptr' = Val.offset_ptr rs#base ofs - /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. + /\ forall r, r <> PC -> rs'#r = rs#r. Proof. unfold indexed_memory_access; intros. (* destruct Archi.ptr64 eqn:SF. *) @@ -2021,13 +2020,12 @@ Lemma indexed_load_access_correct: exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset 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 -> - base <> RTMP -> exists rs', exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m /\ rs'#rd = v - /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. - intros until m; intros EXEC; intros until v; intros LOAD NOT31. + intros until m; intros EXEC; intros until v; intros LOAD. exploit indexed_memory_access_correct; eauto. intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C). econstructor; split. @@ -2042,20 +2040,18 @@ Lemma indexed_store_access_correct: exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk rs m r1 base ofs) -> forall (base: ireg) ofs k (rs: regset) m', Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' -> - base <> RTMP -> r1 <> RTMP -> exists rs', exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m' - /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. + /\ forall r, r <> PC -> rs'#r = rs#r. Proof. - intros until m; intros EXEC; intros until m'; intros STORE NOT31 NOT31'. - exploit indexed_memory_access_correct. instantiate (1 := base). eauto. + intros until m; intros EXEC; intros until m'; intros STORE. + exploit indexed_memory_access_correct. (* instantiate (1 := base). eauto. *) intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC. unfold exec_store_offset. unfold parexec_store_offset. rewrite PtrEq. rewrite B, C, STORE. eauto. discriminate. - { intro. inv H. contradiction. } auto. Qed. @@ -2063,13 +2059,12 @@ Lemma loadind_correct: forall (base: ireg) ofs ty dst k c (rs: regset) m v, loadind base ofs ty dst k = OK c -> Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v -> - base <> RTMP -> exists rs', exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m /\ rs'#(preg_of dst) = v - /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> preg_of dst -> rs'#r = rs#r. Proof. - intros until v; intros TR LOAD NOT31. + intros until v; intros TR LOAD. assert (A: exists mk_instr rd, preg_of dst = IR rd /\ c = indexed_memory_access mk_instr base ofs :: k @@ -2086,12 +2081,11 @@ Lemma storeind_correct: forall (base: ireg) ofs ty src k c (rs: regset) m m', storeind src base ofs ty k = OK c -> Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) rs#(preg_of src) = Some m' -> - base <> RTMP -> exists rs', exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m' - /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. + /\ forall r, r <> PC -> rs'#r = rs#r. Proof. - intros until m'; intros TR STORE NOT31. + intros until m'; intros TR STORE. assert (A: exists mk_instr rr, preg_of src = IR rr /\ c = indexed_memory_access mk_instr base ofs :: k @@ -2102,7 +2096,6 @@ Proof. destruct A as (mk_instr & rr & rsEq & B & C). subst c. eapply indexed_store_access_correct; eauto with asmgen. congruence. - destruct rr; try discriminate. destruct src; try discriminate. Qed. Ltac bsimpl := unfold exec_bblock; simpl. @@ -2139,23 +2132,21 @@ Qed. Lemma loadind_ptr_correct: forall (base: ireg) ofs (dst: ireg) k (rs: regset) m v, Mem.loadv Mptr m (Val.offset_ptr rs#base ofs) = Some v -> - base <> RTMP -> exists rs', exec_straight ge (loadind_ptr base ofs dst ::g k) rs m k rs' m /\ rs'#dst = v - /\ forall r, r <> PC -> r <> RTMP -> r <> dst -> rs'#r = rs#r. + /\ 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 H1. auto. + intros. unfold Mptr. assert (Archi.ptr64 = true). auto. rewrite H0. auto. Qed. Lemma storeind_ptr_correct: forall (base: ireg) ofs (src: ireg) k (rs: regset) m m', Mem.storev Mptr m (Val.offset_ptr rs#base ofs) rs#src = Some m' -> - base <> RTMP -> src <> RTMP -> exists rs', exec_straight ge (storeind_ptr src base ofs ::g k) rs m k rs' m' - /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. + /\ forall r, r <> PC -> rs'#r = rs#r. Proof. intros. eapply indexed_store_access_correct with (r1 := src); eauto with asmgen. intros. unfold Mptr. assert (Archi.ptr64 = true); auto. @@ -2174,7 +2165,10 @@ Proof. intros until v; intros TR EV. unfold transl_memory_access in TR; destruct addr; ArgsInv. - (* indexed *) - inv EV. apply indexed_memory_access_correct; eauto with asmgen. + inv EV. exploit indexed_memory_access_correct; eauto. intros (base' & ofs' & rs' & ptr' & EOPT & EVALOFF & VALOFF & RSEQ). + eexists; eexists; eexists; eexists. split; try split; try split. + eapply EOPT. unfold eval_offset in EVALOFF. inv EVALOFF. eauto. + { intros. destruct r; rewrite RSEQ; auto. } - (* global *) simpl in EV. inv EV. inv TR. econstructor; econstructor; econstructor; econstructor; split. constructor. apply exec_straight_one. simpl; eauto. auto. @@ -2193,7 +2187,11 @@ Proof. destruct (Genv.find_symbol ge i); discriminate. + simpl. rewrite Ptrofs.add_zero; auto. - (* stack *) - inv TR. inv EV. apply indexed_memory_access_correct; eauto with asmgen. + inv TR. inv EV. + exploit indexed_memory_access_correct; eauto. intros (base' & ofs' & rs' & ptr' & EOPT & EVALOFF & VALOFF & RSEQ). + eexists; eexists; eexists; eexists. split; try split; try split. + eapply EOPT. unfold eval_offset in EVALOFF. inv EVALOFF. eauto. + { intros. destruct r; rewrite RSEQ; auto. } Qed. Lemma transl_memory_access2_correct: @@ -2658,7 +2656,6 @@ Proof. exploit ((loadind_ptr_correct SP (fn_retaddr_ofs f) GPRA (Pset RA GPRA ::g Pfreeframe (fn_stacksize f) (fn_link_ofs f) ::g k)) rs tm). - rewrite <- (sp_val _ _ rs AG). simpl. eexact LRA'. - - congruence. - intros (rs1 & A1 & B1 & C1). assert (agree ms (Vptr stk soff) rs1) as AG1. + destruct AG. -- cgit From 6e995893ccae975f49c250387182fcd3e3e6395a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 12 May 2019 00:42:04 +0200 Subject: directly branch to certain division functions from gcc --- mppa_k1c/TargetPrinter.ml | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 114297c9..3c46ef16 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -34,9 +34,22 @@ module Target (*: TARGET*) = let comment = "#" - let symbol = elf_symbol - let symbol_offset = elf_symbol_offset - let label = elf_label + let subst_symbol = function + "__compcert_i64_udiv" -> "__udivdi3" + | "__compcert_i64_sdiv" -> "__divdi3" + | "__compcert_i64_umod" -> "__umoddi3" + | "__compcert_i64_smod" -> "__moddi3" + | x -> x;; + + let symbol oc symb = + fprintf oc "%s" (subst_symbol (extern_atom symb)) + + let symbol_offset oc (symb, ofs) = + symbol oc symb; + let ofs = camlint64_of_ptrofs ofs in + if ofs <> 0L then fprintf oc " + %Ld" ofs + + let label = elf_label let print_label oc lbl = label oc (transl_label lbl) -- cgit