diff options
| -rw-r--r-- | backend/LICMaux.ml | 3 | ||||
| -rw-r--r-- | driver/Clflags.ml | 4 | ||||
| -rw-r--r-- | driver/Compopts.v | 3 | ||||
| -rw-r--r-- | driver/Driver.ml | 2 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 22 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 27 |
7 files changed, 46 insertions, 17 deletions
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 32044cc9..4ebc7844 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -141,7 +141,8 @@ let rewrite_loop_body (last_alloc : reg ref) new_res)); PTree.set res new_res mapper | Iload(trap, chunk, addr, args, res, pc') - when Archi.has_notrap_loads -> + when Archi.has_notrap_loads && + !Clflags.option_fnontrap_loads -> let new_res = P.succ !last_alloc in last_alloc := new_res; add_inj (INJload(chunk, addr, diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 8deb5224..8e3305ef 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -79,9 +79,11 @@ let use_standard_headers = ref Configuration.has_standard_headers let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true -let option_faddx = ref false +let option_faddx = ref false +let option_fmadd = ref true let option_fcoalesce_mem = ref true let option_fforward_moves = ref true let option_fmove_loop_invariants = ref true +let option_fnontrap_loads = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 diff --git a/driver/Compopts.v b/driver/Compopts.v index e4dae87d..5acd2640 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -69,6 +69,9 @@ Parameter optim_xsaddr: unit -> bool. (** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *) Parameter optim_coalesce_mem: unit -> bool. +(* FIXME TEMPORARY Flag -faddx. Fuse (default true) *) +Parameter optim_madd: unit -> bool. + (** FIXME TEMPORARY Flag -faddx. Fuse (default false) *) Parameter optim_addx: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 0f9e637c..6a9e9b92 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -415,6 +415,8 @@ let cmdline_actions = @ f_opt "globaladdroffset" option_fglobaladdroffset @ f_opt "xsaddr" option_fxsaddr @ f_opt "addx" option_faddx + @ f_opt "madd" option_fmadd + @ f_opt "nontrap-loads" option_fnontrap_loads @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "all-loads-nontrap" option_all_loads_nontrap @ f_opt "forward-moves" option_fforward_moves diff --git a/extraction/extraction.v b/extraction/extraction.v index 18637336..b6aa3409 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -142,6 +142,8 @@ Extract Constant Compopts.optim_xsaddr => "fun _ -> !Clflags.option_fxsaddr". Extract Constant Compopts.optim_addx => "fun _ -> !Clflags.option_faddx". +Extract Constant Compopts.optim_madd => + "fun _ -> !Clflags.option_fmadd". Extract Constant Compopts.optim_coalesce_mem => "fun _ -> !Clflags.option_fcoalesce_mem". Extract Constant Compopts.optim_forward_moves => diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index ec3985c5..0974f872 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -168,13 +168,21 @@ Nondetfunction add (e1: expr) (e2: expr) := | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) | t1, (Eop Omul (t2:::t3:::Enil)) => - Eop Omadd (t1:::t2:::t3:::Enil) + if Compopts.optim_madd tt + then Eop Omadd (t1:::t2:::t3:::Enil) + else Eop Oadd (e1:::e2:::Enil) | (Eop Omul (t2:::t3:::Enil)), t1 => - Eop Omadd (t1:::t2:::t3:::Enil) + if Compopts.optim_madd tt + then Eop Omadd (t1:::t2:::t3:::Enil) + else Eop Oadd (e1:::e2:::Enil) | t1, (Eop (Omulimm n) (t2:::Enil)) => - Eop (Omaddimm n) (t1:::t2:::Enil) + if Compopts.optim_madd tt + then Eop (Omaddimm n) (t1:::t2:::Enil) + else Eop Oadd (e1:::e2:::Enil) | (Eop (Omulimm n) (t2:::Enil)), t1 => - Eop (Omaddimm n) (t1:::t2:::Enil) + if Compopts.optim_madd tt + then Eop (Omaddimm n) (t1:::t2:::Enil) + else Eop Oadd (e1:::e2:::Enil) | (Eop (Oshlimm n) (t1:::Enil)), t2 => add_shlimm n t1 t2 | t2, (Eop (Oshlimm n) (t1:::Enil)) => @@ -197,7 +205,9 @@ Nondetfunction sub (e1: expr) (e2: expr) := | t1, (Eop Omul (t2:::t3:::Enil)) => Eop Omsub (t1:::t2:::t3:::Enil) | t1, (Eop (Omulimm n) (t2:::Enil)) => - Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil) + if Compopts.optim_madd tt + then Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil) + else Eop Osub (e1:::e2:::Enil) | _, _ => Eop Osub (e1:::e2:::Enil) end. @@ -712,4 +722,4 @@ End SELECT. (* Local Variables: *) (* mode: coq *) -(* End: *)
\ No newline at end of file +(* End: *) diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index d3eb1dde..368f78f4 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -350,13 +350,19 @@ Proof. apply eval_addimm. EvalOp. repeat rewrite Val.add_assoc. reflexivity. - (* Omadd *) - subst. TrivialExists. + subst. destruct (Compopts.optim_madd tt); TrivialExists; + repeat (eauto; econstructor; simpl). - (* Omadd rev *) - subst. rewrite Val.add_commut. TrivialExists. + subst. destruct (Compopts.optim_madd tt); TrivialExists; + repeat (eauto; econstructor; simpl). + simpl. rewrite Val.add_commut. reflexivity. - (* Omaddimm *) - subst. TrivialExists. + subst. destruct (Compopts.optim_madd tt); TrivialExists; + repeat (eauto; econstructor; simpl). - (* Omaddimm rev *) - subst. rewrite Val.add_commut. TrivialExists. + subst. destruct (Compopts.optim_madd tt); TrivialExists; + repeat (eauto; econstructor; simpl). + simpl. rewrite Val.add_commut. reflexivity. (* Oaddx *) - subst. pose proof eval_addx as ADDX. unfold binary_constructor_sound in ADDX. @@ -380,11 +386,14 @@ Proof. - subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp. - subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp. - TrivialExists. simpl. subst. reflexivity. - - TrivialExists. simpl. subst. - rewrite sub_add_neg. - rewrite neg_mul_distr_r. - unfold Val.neg. - reflexivity. + - destruct (Compopts.optim_madd tt). + + TrivialExists. simpl. subst. + rewrite sub_add_neg. + rewrite neg_mul_distr_r. + unfold Val.neg. + reflexivity. + + TrivialExists. repeat (eauto; econstructor). + simpl. subst. reflexivity. - TrivialExists. Qed. |