diff options
| -rw-r--r-- | riscV/Asmgen.v | 2 | ||||
| -rw-r--r-- | riscV/ExpansionOracle.ml | 10 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 96 |
3 files changed, 100 insertions, 8 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 7f63bfee..d826f139 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -222,7 +222,7 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) := match cond, args with -| Ccomp c, a1 :: a2 :: nil => + | Ccomp c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (transl_cbranch_int32s c r1 r2 lbl :: k) | Ccompu c, a1 :: a2 :: nil => diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index b3a440a4..dc7f4b82 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -370,6 +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;*) let new_order = ref [] in let liveins = ref sb.liveins in let exp = ref [] in @@ -431,7 +432,7 @@ 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; @@ -441,7 +442,7 @@ let expanse (sb : superblock) code pm = exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true - | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> + (*| Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> debug "Icond/Ccompimm\n"; exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 []; was_branch := true; @@ -450,7 +451,7 @@ let expanse (sb : superblock) code pm = debug "Icond/Ccompuimm\n"; exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 []; was_branch := true; - was_exp := true + was_exp := true*) | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) -> debug "Icond/Ccompl\n"; exp := cbranch_int64s false c a1 a2 info succ1 succ2 []; @@ -461,7 +462,7 @@ let expanse (sb : superblock) code pm = exp := cbranch_int64u false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true - | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> + (*| Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> debug "Icond/Ccomplimm\n"; exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 []; was_branch := true; @@ -508,6 +509,7 @@ let expanse (sb : superblock) code pm = sb.instructions; sb.instructions <- Array.of_list (List.rev !new_order); sb.liveins <- !liveins; + (*debug_flag := false;*) (!code', !pm') let rec find_last_node_reg = function diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 710b8d76..509697de 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -597,6 +597,8 @@ Proof. explore; try congruence. Qed. +(* TODO MOVE EXPANSIONS BELOW ELSEWHERE *) + Definition is_inv_cmp_int (cmp: comparison) : bool := match cmp with | Cle | Cgt => true | _ => false end. @@ -988,6 +990,93 @@ Proof. (* TODO Global Opaque hslocal_set_sreg. Local Hint Resolve hslocal_set_sreg_correct: wlp. +(* TODO MOVE ELSEWHERE Branch expansion *) + +(* XXX NOT SURE IF THIS DEF IS NEEDED + * SHOULD WE TAKE THE PREV STATE INTO ACCOUNT HERE? +Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) : ?? list_hsval := + if is_inv then + hlist_args prev*) + +Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbeqw optR0 + | Cne => CEbnew optR0 + | Clt => CEbltw optR0 + | Cle => CEbgew optR0 + | Cgt => CEbltw optR0 + | Cge => CEbgew optR0 + end. + +Definition transl_cbranch_int32u (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbeqw optR0 + | Cne => CEbnew optR0 + | Clt => CEbltuw optR0 + | Cle => CEbgeuw optR0 + | Cgt => CEbltuw optR0 + | Cge => CEbgeuw optR0 + end. + +Definition transl_cbranch_int64s (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbeql optR0 + | Cne => CEbnel optR0 + | Clt => CEbltl optR0 + | Cle => CEbgel optR0 + | Cgt => CEbltl optR0 + | Cge => CEbgel optR0 + end. + +Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbeql optR0 + | Cne => CEbnel optR0 + | Clt => CEbltul optR0 + | Cle => CEbgeul optR0 + | Cgt => CEbltul optR0 + | Cge => CEbgeul optR0 + end. + +Definition cbranch_expanse (prev: hsistate_local) (i: instruction) : ?? (condition * list_hsval) := + match i with + | Icond (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 + DO hv1 <~ hsi_sreg_get prev a1;; + DO hv2 <~ hsi_sreg_get prev a2;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + RET (cond, lhsv) + | Icond (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 + DO hv1 <~ hsi_sreg_get prev a1;; + DO hv2 <~ hsi_sreg_get prev a2;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + RET (cond, lhsv) + | Icond (Ccompl c) (a1 :: a2 :: nil) _ _ _ => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in + DO hv1 <~ hsi_sreg_get prev a1;; + DO hv2 <~ hsi_sreg_get prev a2;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + RET (cond, lhsv) + | Icond (Ccomplu c) (a1 :: a2 :: nil) _ _ _ => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in + DO hv1 <~ hsi_sreg_get prev a1;; + DO hv2 <~ hsi_sreg_get prev a2;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + RET (cond, lhsv) + (* | Icond (Ccompimm c n) (a1 :: nil) _ _ _ => + let cond := transl_cbranch_int32s c (make_optR0 c) in + RET (cond, a1 :: a1 :: nil)*) + | Icond cond args _ _ _ => + DO vargs <~ hlist_args prev args;; + RET (cond, vargs) + | _ => FAILWITH "cbranch_expanse: not an Icond" + end. + (** ** Execution of one instruction *) Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) := @@ -1005,7 +1094,8 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) : RET (Some (hsist_set_local hst pc' next)) | Icond cond args ifso ifnot _ => let prev := hst.(hsi_local) in - DO vargs <~ hlist_args prev args ;; + DO res <~ cbranch_expanse prev i;; + let (cond, vargs) := res in let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |}) | _ => RET None (* TODO jumptable ? *) @@ -1044,7 +1134,7 @@ Lemma hsiexec_inst_correct i hst: exists st', siexec_inst i st = Some st' /\ (forall (REF:hsistate_refines_stat hst st), hsistate_refines_stat hst' st') /\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st'). -Proof. +Proof. Admitted. (* destruct i; simpl; wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. - (* refines_dyn Iop *) eapply hsist_set_local_correct_dyn; eauto. @@ -1068,7 +1158,7 @@ Proof. + split; simpl; auto. destruct NEST as [|st0 se lse TOP NEST]; econstructor; simpl; auto; constructor; auto. -Qed. + Qed.*) Global Opaque hsiexec_inst. Local Hint Resolve hsiexec_inst_correct: wlp. |