diff options
| -rw-r--r-- | backend/Duplicate.v | 24 | ||||
| -rw-r--r-- | backend/Duplicateproof.v | 20 | ||||
| -rw-r--r-- | backend/Lineartyping.v | 2 | ||||
| -rw-r--r-- | driver/Compiler.v | 50 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 29 |
6 files changed, 71 insertions, 56 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 3ad37c83..46f0855d 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -72,17 +72,19 @@ Definition verify_match_inst dupmap inst tinst := else Error(msg "Different operations in Iop") | _ => Error(msg "verify_match_inst Inop") end - | Iload m a lr r n => match tinst with - | Iload m' a' lr' r' n' => + | Iload tm m a lr r n => match tinst with + | Iload tm' m' a' lr' r' n' => do u <- verify_is_copy dupmap n n'; - if (chunk_eq m m') then - if (eq_addressing a a') then - if (list_eq_dec Pos.eq_dec lr lr') then - if (Pos.eq_dec r r') then OK tt - else Error (msg "Different r in Iload") - else Error (msg "Different lr in Iload") - else Error (msg "Different addressing in Iload") - else Error (msg "Different mchunk in Iload") + if (trapping_mode_eq tm tm') then + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r in Iload") + else Error (msg "Different lr in Iload") + else Error (msg "Different addressing in Iload") + else Error (msg "Different mchunk in Iload") + else Error (msg "Different trapping_mode in Iload") | _ => Error (msg "verify_match_inst Iload") end | Istore m a lr r n => match tinst with @@ -195,4 +197,4 @@ Definition transf_fundef (f: fundef) : res fundef := transf_partial_fundef transf_function f. Definition transf_program (p: program) : res program := - transform_partial_program transf_fundef p.
\ No newline at end of file + transform_partial_program transf_fundef p. diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 39b7a353..e66a1068 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -13,8 +13,8 @@ Inductive match_inst (dupmap: PTree.t node): instruction -> instruction -> Prop dupmap!n' = (Some n) -> match_inst dupmap (Inop n) (Inop n') | match_inst_op: forall n n' op lr r, dupmap!n' = (Some n) -> match_inst dupmap (Iop op lr r n) (Iop op lr r n') - | match_inst_load: forall n n' m a lr r, - dupmap!n' = (Some n) -> match_inst dupmap (Iload m a lr r n) (Iload m a lr r n') + | match_inst_load: forall n n' tm m a lr r, + dupmap!n' = (Some n) -> match_inst dupmap (Iload tm m a lr r n) (Iload tm m a lr r n') | match_inst_store: forall n n' m a lr r, dupmap!n' = (Some n) -> match_inst dupmap (Istore m a lr r n) (Istore m a lr r n') | match_inst_call: forall n n' s ri lr r, @@ -137,6 +137,7 @@ Proof. (* Iload *) - destruct i'; try (inversion H; fail). monadInv H. destruct x. eapply verify_is_copy_correct in EQ. + destruct (trapping_mode_eq _ _); try discriminate. destruct (chunk_eq _ _); try discriminate. destruct (eq_addressing _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. @@ -393,6 +394,21 @@ Proof. eexists. split. + eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto. + econstructor; eauto. +(* Iload notrap1 *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Iload_notrap1; eauto. erewrite eval_addressing_preserved; eauto. + + econstructor; eauto. +(* Iload notrap2 *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Iload_notrap2; eauto. erewrite eval_addressing_preserved; eauto. + + econstructor; eauto. + (* Istore *) - eapply dupmap_correct in DUPLIC; eauto. destruct DUPLIC as (i' & H2 & H3). inv H3. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 994d2652..3fe61470 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -328,7 +328,7 @@ Local Opaque mreg_type. change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. red; intros; subst op. simpl in ISMOVE. destruct args; try discriminate. destruct args; discriminate. - apply wt_undef_regs; auto. + (* no longer needed apply wt_undef_regs; auto. *) - (* load *) simpl in *; InvBooleans. econstructor; eauto. diff --git a/driver/Compiler.v b/driver/Compiler.v index f948d595..72db86e9 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -141,8 +141,9 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 8) @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program - @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 9) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 10) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -250,8 +251,8 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: 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 Unusedglobproof.match_prog ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog ::: mkpass Linearizeproof.match_prog @@ -290,18 +291,19 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. - set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. - 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 (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. + set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. + destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + destruct (partial_if optim_redundancy Deadcode.transf_program p13) as [p14|e] eqn:P14; 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 *. - destruct (partial_if debug Debugvar.transf_program p18) as [p19|e] eqn:P19; simpl in T; try discriminate. - destruct (Stacking.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + set (p17 := Tunneling.tunnel_program p16) in *. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + set (p19 := CleanupLabels.transf_program p18) in *. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -312,25 +314,12 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. -<<<<<<< HEAD - exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match. - 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. - exists p18; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p20; split. apply Stackingproof.transf_program_match; auto. -======= exists p10; split. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. exists p15; split. apply Unusedglobproof.transf_program_match; auto. exists p16; split. apply Allocproof.transf_program_match; auto. exists p17; split. apply Tunnelingproof.transf_program_match. @@ -338,7 +327,6 @@ Proof. exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. exists p21; split. apply Stackingproof.transf_program_match; auto. ->>>>>>> origin/mppa-work exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -390,7 +378,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 p22)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p23)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -419,10 +407,10 @@ Ltac DestructM := eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. 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 Unusedglobproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. eapply Allocproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Tunnelingproof.transf_program_correct; eassumption. diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 5825fd04..50637723 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -1116,7 +1116,7 @@ Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool := | MBsetstack src ofs ty => before | MBgetparam ofs ty dst => negb (mreg_eq dst MFP) | MBop op args res => before && negb (mreg_eq res MFP) - | MBload chunk addr args dst => before && negb (mreg_eq dst MFP) + | MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst MFP) | MBstore chunk addr args res => before end. diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index cdbaf16a..b3e0ee23 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1203,14 +1203,18 @@ Local Transparent destroyed_by_op. 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.
+ eapply basics_to_code_app; eauto.
+ eapply match_codestate_intro; eauto. simpl. rewrite Hheader in *. + simpl in EQ. assumption. + + eapply agree_set_undef_mreg; eauto. intros; auto with asmgen. + + simpl. intro. + rewrite R; try congruence. + apply DXP. + destruct ep0; simpl in *; congruence. + apply preg_of_not_FP. + destruct ep0; simpl in *; congruence. }
{
exploit transl_load_correct_notrap2; eauto.
@@ -1226,10 +1230,15 @@ Local Transparent destroyed_by_op. 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 match_codestate_intro; eauto. simpl. rewrite Hheader in *. simpl in EQ. assumption. eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.
- simpl; congruence.
+ simpl. intro. + rewrite R; try congruence. + apply DXP. + destruct ep0; simpl in *; congruence. + apply preg_of_not_FP. + destruct ep0; simpl in *; congruence. }
- (* MBstore *)
simpl in EQ0. rewrite Hheader in DXP.
|