diff options
| -rw-r--r-- | riscV/ExpansionOracle.ml | 13 | ||||
| -rw-r--r-- | riscV/RTLpathSE_simplify.v | 21 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 29 |
3 files changed, 39 insertions, 24 deletions
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 07999b05..39b8f367 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -370,7 +370,7 @@ let rec write_tree exp current code' new_order = | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction." let expanse (sb : superblock) code pm = - debug_flag := true; + (*debug_flag := true;*) let new_order = ref [] in let liveins = ref sb.liveins in let exp = ref [] in @@ -432,16 +432,16 @@ let expanse (sb : superblock) code pm = debug "Iop/Cnotcompfs\n"; exp := expanse_cond_fp true cond_single c f1 f2 dest succ []; was_exp := true - (*| Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> + | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> debug "Icond/Ccomp\n"; exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; was_branch := true; - was_exp := true*) + was_exp := true | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) -> debug "Icond/Ccompu\n"; exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; was_branch := true; - was_exp := true(* + was_exp := true | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> debug "Icond/Ccompimm\n"; exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 []; @@ -492,7 +492,7 @@ let expanse (sb : superblock) code pm = debug "Icond/Cnotcompfs\n"; exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 []; was_branch := true; - was_exp := true*) + was_exp := true | _ -> new_order := n :: !new_order); if !was_exp then ( node := !node + 1; @@ -510,8 +510,7 @@ let expanse (sb : superblock) code pm = sb.instructions; sb.instructions <- Array.of_list (List.rev !new_order); sb.liveins <- !liveins; - print_ptree_regset !liveins; - debug_flag := false; + (*debug_flag := false;*) (!code', !pm') let rec find_last_node_reg = function diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index f1f44331..f6d96d06 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -293,6 +293,13 @@ Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) := | Cge => CEbgeul optR0 end. +Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (condition * list_hsval) := + let normal := is_normal_cmp cmp in + let normal' := if cnot then negb normal else normal in + let hvs := fn_cond cmp lhsv in + let hl := make_lhsv_cmp false hvs hvs in + if normal' then ((CEbnew (Some false)), hl) else ((CEbeqw (Some false)), hl). + (** Target op simplifications using "fake" values *) Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := @@ -366,13 +373,13 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) := match cond, args with - (*| (Ccomp c), (a1 :: a2 :: nil) => + | (Ccomp c), (a1 :: a2 :: nil) => let is_inv := is_inv_cmp_int c in let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in let hv1 := fsi_sreg_get prev a1 in let hv2 := fsi_sreg_get prev a2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - Some (cond, lhsv)*) + Some (cond, lhsv) | (Ccompu c), (a1 :: a2 :: nil) => let is_inv := is_inv_cmp_int c in let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in @@ -380,7 +387,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args let hv2 := fsi_sreg_get prev a2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in Some (cond, lhsv) - (*| (Ccompimm c n), (a1 :: nil) => + | (Ccompimm c n), (a1 :: nil) => let is_inv := is_inv_cmp_int c in let hv1 := fsi_sreg_get prev a1 in (if Int.eq n Int.zero then @@ -447,25 +454,25 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args let hv2 := fsi_sreg_get prev f2 in let is_inv := is_inv_cmp_float c in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - expanse_cbranch_fp false cond_float c lhsv + Some (expanse_cbranch_fp false cond_float c lhsv) | (Cnotcompf c), (f1 :: f2 :: nil) => let hv1 := fsi_sreg_get prev f1 in let hv2 := fsi_sreg_get prev f2 in let is_inv := is_inv_cmp_float c in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - expanse_cbranch_fp true cond_float c lhsv + Some (expanse_cbranch_fp true cond_float c lhsv) | (Ccompfs c), (f1 :: f2 :: nil) => let hv1 := fsi_sreg_get prev f1 in let hv2 := fsi_sreg_get prev f2 in let is_inv := is_inv_cmp_float c in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - expanse_cbranch_fp false cond_single c lhsv + Some (expanse_cbranch_fp false cond_single c lhsv) | (Cnotcompfs c), (f1 :: f2 :: nil) => let hv1 := fsi_sreg_get prev f1 in let hv2 := fsi_sreg_get prev f2 in let is_inv := is_inv_cmp_float c in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - expanse_cbranch_fp true cond_single c lhsv*) + Some (expanse_cbranch_fp true cond_single c lhsv) | _, _ => None end. diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 76d046fd..7b1df1ab 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -453,7 +453,7 @@ Fixpoint fsval_proj hsv: ?? hsval := if b then (* was not yet really hash-consed *) DO hl' <~ fsval_list_proj hl;; - hSop op hl' + hSop op hl' else RET hsv (* already hash-consed *) | HSload hm t chk addr hl _ => RET hsv (* FIXME ? *) end @@ -834,23 +834,32 @@ Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) : (* -Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : ?? (condition * list_hsval) := - let normal := is_normal_cmp cmp in - let normal' := if cnot then negb normal else normal in - DO hvs <~ fn_cond cmp lhsv;; - DO hl <~ make_lhsv_cmp false hvs hvs;; - if normal' then RET ((CEbnew (Some false)), hl) else RET ((CEbeqw (Some false)), hl). + Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : ?? (condition * list_hsval) := *) (** ** Execution of one instruction *) +(* TODO gourdinl + * This is just useful for debugging fake values hashcode projection *) +Fixpoint check_no_uhid lhsv := + match lhsv with + | HSnil hc => + DO b <~ phys_eq hc unknown_hid;; + assert_b (negb b) "fail no uhid";; + RET tt + | HScons hsv lhsv' hc => + DO b <~ phys_eq hc unknown_hid;; + assert_b (negb b) "fail no uhid";; + check_no_uhid lhsv' + end. + Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg): ?? (condition * list_hsval) := match target_cbranch_expanse prev cond args with | Some (cond', vargs) => DO vargs' <~ fsval_list_proj vargs;; - RET (cond', vargs) + RET (cond', vargs') | None => DO vargs <~ hlist_args prev args ;; RET (cond, vargs) @@ -862,13 +871,13 @@ Lemma cbranch_expanse_correct hst c l: (OK: hsok_local ge sp rs0 m0 hst), seval_condition ge sp (fst r) (hsval_list_proj (snd r)) (si_smem st) rs0 m0 = seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0. -Proof. +Proof. Admitted. (* unfold cbranch_expanse. destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify. + destruct p as [c' l']; simpl. exploit target_cbranch_expanse_correct; eauto. + unfold seval_condition; erewrite H; eauto. -Qed. + Qed.*) Local Hint Resolve cbranch_expanse_correct: wlp. Global Opaque cbranch_expanse. |