diff options
-rw-r--r-- | riscV/BTL_SEsimplify.v | 240 | ||||
-rw-r--r-- | riscV/ExpansionOracle.ml | 160 | ||||
-rw-r--r-- | scheduling/BTL_SEimpl.v | 23 | ||||
-rw-r--r-- | scheduling/BTL_SEsimuref.v | 10 |
4 files changed, 404 insertions, 29 deletions
diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v index 0cdea5fe..baa4edeb 100644 --- a/riscV/BTL_SEsimplify.v +++ b/riscV/BTL_SEsimplify.v @@ -258,6 +258,55 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lsv: list_sval) := let lfsv := make_lfsv_single fsv in if normal' then fsv else fSop (OExoriw Int.one) lfsv. +(** ** Branches instructions *) + +Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) := + match cmp with + | Ceq => CEbeqw optR + | Cne => CEbnew optR + | Clt => CEbltw optR + | Cle => CEbgew optR + | Cgt => CEbltw optR + | Cge => CEbgew optR + end. + +Definition transl_cbranch_int32u (cmp: comparison) (optR: option oreg) := + match cmp with + | Ceq => CEbequw optR + | Cne => CEbneuw optR + | Clt => CEbltuw optR + | Cle => CEbgeuw optR + | Cgt => CEbltuw optR + | Cge => CEbgeuw optR + end. + +Definition transl_cbranch_int64s (cmp: comparison) (optR: option oreg) := + match cmp with + | Ceq => CEbeql optR + | Cne => CEbnel optR + | Clt => CEbltl optR + | Cle => CEbgel optR + | Cgt => CEbltl optR + | Cge => CEbgel optR + end. + +Definition transl_cbranch_int64u (cmp: comparison) (optR: option oreg) := + match cmp with + | Ceq => CEbequl optR + | Cne => CEbneul optR + | Clt => CEbltul optR + | Cle => CEbgeul optR + | Cgt => CEbltul optR + | Cge => CEbgeul optR + end. + +Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lfsv: list_sval) : (condition * list_sval) := + let normal := is_normal_cmp cmp in + let normal' := if cnot then negb normal else normal in + let fsv := fn_cond cmp lfsv in + let lfsv' := make_lfsv_cmp false fsv fsv in + if normal' then ((CEbnew (Some X0_R)), lfsv') else ((CEbeqw (Some X0_R)), lfsv'). + (** Target op simplifications using "fake" values *) Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): option sval := @@ -437,7 +486,109 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt end. Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) := - None. + match cond, args with + | (Ccomp c), (a1 :: a2 :: nil) => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int32s c (make_optR false is_inv) in + let fsv1 := ris_sreg_get prev a1 in + let fsv2 := ris_sreg_get prev a2 in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond, lfsv) + | (Ccompu c), (a1 :: a2 :: nil) => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int32u c (make_optR false is_inv) in + let fsv1 := ris_sreg_get prev a1 in + let fsv2 := ris_sreg_get prev a2 in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond, lfsv) + | (Ccompimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + let fsv1 := ris_sreg_get prev a1 in + (if Int.eq n Int.zero then + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + let cond := transl_cbranch_int32s c (make_optR true is_inv) in + Some (cond, lfsv) + else + let fsv := loadimm32 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + let cond := transl_cbranch_int32s c (make_optR false is_inv) in + Some (cond, lfsv)) + | (Ccompuimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + let fsv1 := ris_sreg_get prev a1 in + (if Int.eq n Int.zero then + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + let cond := transl_cbranch_int32u c (make_optR true is_inv) in + Some (cond, lfsv) + else + let fsv := loadimm32 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + let cond := transl_cbranch_int32u c (make_optR false is_inv) in + Some (cond, lfsv)) + | (Ccompl c), (a1 :: a2 :: nil) => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int64s c (make_optR false is_inv) in + let fsv1 := ris_sreg_get prev a1 in + let fsv2 := ris_sreg_get prev a2 in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond, lfsv) + | (Ccomplu c), (a1 :: a2 :: nil) => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int64u c (make_optR false is_inv) in + let fsv1 := ris_sreg_get prev a1 in + let fsv2 := ris_sreg_get prev a2 in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond, lfsv) + | (Ccomplimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + let fsv1 := ris_sreg_get prev a1 in + (if Int64.eq n Int64.zero then + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + let cond := transl_cbranch_int64s c (make_optR true is_inv) in + Some (cond, lfsv) + else + let fsv := loadimm64 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + let cond := transl_cbranch_int64s c (make_optR false is_inv) in + Some (cond, lfsv)) + | (Ccompluimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + let fsv1 := ris_sreg_get prev a1 in + (if Int64.eq n Int64.zero then + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + let cond := transl_cbranch_int64u c (make_optR true is_inv) in + Some (cond, lfsv) + else + let fsv := loadimm64 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + let cond := transl_cbranch_int64u c (make_optR false is_inv) in + Some (cond, lfsv)) + | (Ccompf c), (f1 :: f2 :: nil) => + let fsv1 := ris_sreg_get prev f1 in + let fsv2 := ris_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cbranch_fp false cond_float c lfsv) + | (Cnotcompf c), (f1 :: f2 :: nil) => + let fsv1 := ris_sreg_get prev f1 in + let fsv2 := ris_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cbranch_fp true cond_float c lfsv) + | (Ccompfs c), (f1 :: f2 :: nil) => + let fsv1 := ris_sreg_get prev f1 in + let fsv2 := ris_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cbranch_fp false cond_single c lfsv) + | (Cnotcompfs c), (f1 :: f2 :: nil) => + let fsv1 := ris_sreg_get prev f1 in + let fsv2 := ris_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cbranch_fp true cond_single c lfsv) + | _, _ => None + end. (** * Auxiliary lemmas on comparisons *) @@ -1706,17 +1857,84 @@ Proof. - eapply simplify_cnotcompfs_correct; eauto. Qed. -(* -Lemma target_cbranch_expanse_correct hrs c l ge sp rs0 m0 st c' l': forall +Lemma target_cbranch_expanse_correct hrs c l ctx st c' l': forall (TARGET: target_cbranch_expanse hrs c l = Some (c', l')) - (LREF : hsilocal_refines ge sp rs0 m0 hrs st) - (OK: hsok_local ge sp rs0 m0 hrs), - seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 = - seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0. + (REF: ris_refines ctx hrs st) + (OK: ris_ok ctx hrs), + eval_scondition ctx c' l' = + eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)). Proof. - unfold target_cbranch_expanse, seval_condition; simpl. - intros H (LREF & SREF & SREG & SMEM) ?. - congruence. + unfold target_cbranch_expanse, eval_scondition; simpl. + intros H ? ?. inversion REF. + destruct c; try congruence; + repeat (destruct l; simpl in H; try congruence). + 1,2,5,6: + destruct c; inv H; simpl; + rewrite !REG_EQ; + try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence); + try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence); + try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence); + try replace (Cle) with (swap_comparison Cge) by auto; + try replace (Clt) with (swap_comparison Cgt) by auto; + try rewrite Val.swap_cmp_bool; trivial; + try rewrite Val.swap_cmpu_bool; trivial; + try rewrite Val.swap_cmpl_bool; trivial; + try rewrite Val.swap_cmplu_bool; trivial. + 1,2,3,4: + try destruct (Int.eq n Int.zero) eqn: EQIMM; + try apply Int.same_if_eq in EQIMM; + try destruct (Int64.eq n Int64.zero) eqn: EQIMM; + try apply Int64.same_if_eq in EQIMM; + destruct c; inv H; simpl; + rewrite !REG_EQ; + try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence); + try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence); + try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence); + unfold loadimm32, load_hilo32, Val.cmp, Val.cmpu, zero32; + unfold loadimm64, load_hilo64, Val.cmpl, Val.cmplu, zero64; + intros; try (specialize make_immed32_sound with (n); + destruct (make_immed32 n) eqn:EQMKI); intros; simpl; + intros; try (specialize make_immed64_sound with (n); + destruct (make_immed64 n) eqn:EQMKI); intros; simpl; + try rewrite EQLO; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; + try apply Int.same_if_eq in EQLO; simpl; trivial; + try apply Int64.same_if_eq in EQLO; simpl; trivial; + unfold eval_may_undef; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; simpl; trivial; + try destruct v; try rewrite H; + try rewrite ltu_12_wordsize; try rewrite EQLO; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite Int.add_zero_l; try rewrite Int64.add_zero_l; + auto; simpl; + try rewrite H in EQIMM; + try rewrite EQLO in EQIMM; + try rewrite Int.add_commut, Int.add_zero_l in EQIMM; + try rewrite Int64.add_commut, Int64.add_zero_l in EQIMM; + try rewrite EQIMM; simpl; + try destruct (Archi.ptr64); trivial. + + 1,2,3,4: + destruct c; inv H; simpl; + rewrite !REG_EQ; + try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence); + try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence); + try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence); + unfold zero32, zero64, Val.cmpf, Val.cmpfs; + destruct v, v0; simpl; trivial; + try rewrite Float.cmp_ne_eq; + try rewrite Float32.cmp_ne_eq; + try rewrite <- Float.cmp_swap; simpl; + try rewrite <- Float32.cmp_swap; simpl; + try destruct (Float.cmp _ _); simpl; + try destruct (Float32.cmp _ _); simpl; + try rewrite Int.eq_true; simpl; + try rewrite Int.eq_false; try apply Int.one_not_zero; + simpl; trivial. Qed. Global Opaque target_op_simplify. - Global Opaque target_cbranch_expanse.*) +Global Opaque target_cbranch_expanse. diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 2a21b7a4..7295ae0d 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -339,6 +339,46 @@ let is_inv_cmp = function Cle | Cgt -> true | _ -> false let make_optR is_x0 is_inv = if is_x0 then if is_inv then Some X0_L else Some X0_R else None +let cbranch_int32s is_x0 cmp a1 a2 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbeqw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbnew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgew optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + +let cbranch_int32u is_x0 cmp a1 a2 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbequw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbneuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltuw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + +let cbranch_int64s is_x0 cmp a1 a2 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbeql optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbnel optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltl optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgel optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltl optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgel optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + +let cbranch_int64u is_x0 cmp a1 a2 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbequl optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbneul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgeul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgeul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + let cond_int32s vn is_x0 cmp a1 a2 dest = let optR = make_optR is_x0 (is_inv_cmp cmp) in match cmp with @@ -439,6 +479,40 @@ let cond_single vn cmp f1 f2 dest = | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ] | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ] +let expanse_cbranchimm_int32s vn cmp a1 n iinfo succ1 succ2 = + if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 iinfo succ1 succ2 [] + else + let r = r2pi () in + let l = loadimm32 vn r n in + let r', l' = extract_arg l in + cbranch_int32s false cmp a1 r' iinfo succ1 succ2 l' + +let expanse_cbranchimm_int32u vn cmp a1 n iinfo succ1 succ2 = + if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 iinfo succ1 succ2 [] + else + let r = r2pi () in + let l = loadimm32 vn r n in + let r', l' = extract_arg l in + cbranch_int32u false cmp a1 r' iinfo succ1 succ2 l' + +let expanse_cbranchimm_int64s vn cmp a1 n iinfo succ1 succ2 = + if Int64.eq n Int64.zero then + cbranch_int64s true cmp a1 a1 iinfo succ1 succ2 [] + else + let r = r2pi () in + let l = loadimm64 vn r n in + let r', l' = extract_arg l in + cbranch_int64s false cmp a1 r' iinfo succ1 succ2 l' + +let expanse_cbranchimm_int64u vn cmp a1 n iinfo succ1 succ2 = + if Int64.eq n Int64.zero then + cbranch_int64u true cmp a1 a1 iinfo succ1 succ2 [] + else + let r = r2pi () in + let l = loadimm64 vn r n in + let r', l' = extract_arg l in + cbranch_int64u false cmp a1 r' iinfo succ1 succ2 l' + let expanse_condimm_int32s vn cmp a1 n dest = if Int.eq n Int.zero then cond_int32s vn true cmp a1 a1 dest else @@ -514,6 +588,16 @@ let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest = let r', l = extract_arg insn in addinst vn (OExoriw Int.one) [ r' ] dest :: l +let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 iinfo succ1 succ2 = + let r = r2pi () in + let normal = is_normal_cmp cmp in + let normal' = if cnot then not normal else normal in + let insn = fn_cond vn cmp f1 f2 r in + let r', l = extract_arg insn in + if normal' then + Scond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, iinfo) :: l + else Scond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, iinfo) :: l + (** Return olds args if the CSE numbering is empty *) let get_arguments vn vals args = @@ -529,22 +613,26 @@ let rec gen_btl_list vn exp = inst :: gen_btl_list vn k | [ Sexp (rd, Smove, args, iinfo) ] -> [ Bop (Omove, args, rd, iinfo) ] | [ Scond (cond, args, succ1, succ2, iinfo) ] -> - [ Bcond (cond, args, succ1, succ2, iinfo) ] + let ib = Bcond (cond, args, succ1, succ2, iinfo) in + [ ib ] | [] -> [] | _ -> failwith "write_tree: invalid list" let expanse_list li = debug "#### New block for expansion oracle\n"; let exp = ref [] in + let was_branch = ref false in let was_exp = ref false in let vn = ref (empty_numbering ()) in let rec expanse_list_rec li = match li with | [] -> li | i :: li' -> + was_branch := false; was_exp := false; (if !Clflags.option_fexpanse_rtlcond then match i with + (* Expansion of conditions - Ocmp *) | Bop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, iinfo) -> debug "Bop/Ccomp\n"; exp := cond_int32s vn false c a1 a2 dest; @@ -605,9 +693,75 @@ let expanse_list li = exp := expanse_cond_fp vn true cond_single c f1 f2 dest; exp := extract_final vn !exp dest; was_exp := true + (* Expansion of branches - Ccomp *) + | Bcond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccomp\n"; + exp := cbranch_int32s false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompu\n"; + exp := cbranch_int32u false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompimm\n"; + exp := expanse_cbranchimm_int32s vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompuimm\n"; + exp := expanse_cbranchimm_int32u vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompl\n"; + exp := cbranch_int64s false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccomplu\n"; + exp := cbranch_int64u false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccomplimm\n"; + exp := expanse_cbranchimm_int64s vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompluimm\n"; + exp := expanse_cbranchimm_int64u vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompf\n"; + exp := + expanse_cbranch_fp vn false cond_float c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Cnotcompf\n"; + exp := + expanse_cbranch_fp vn true cond_float c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompfs\n"; + exp := + expanse_cbranch_fp vn false cond_single c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Cnotcompfs\n"; + exp := + expanse_cbranch_fp vn true cond_single c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true | _ -> ()); (if !Clflags.option_fexpanse_others && not !was_exp then match i with + (* Others expansions *) | Bop (Ofloatconst f, nil, dest, iinfo) -> ( match make_immed64 (Floats.Float.to_bits f) with | Imm64_single _ | Imm64_large _ -> () @@ -814,7 +968,9 @@ let expanse_list li = (* TODO gourdinl empty numb BF? vn := empty_numbering ()*) | _ -> ()); i :: expanse_list_rec li') - else gen_btl_list vn (List.rev !exp) @ expanse_list_rec li' + else + let hd = gen_btl_list vn (List.rev !exp) in + hd @ expanse_list_rec li' in expanse_list_rec li diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 7711c72d..305c3cfa 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -682,12 +682,13 @@ Lemma cbranch_expanse_correct hrs c l: (REF : ris_refines ctx hrs sis) (OK: ris_ok ctx hrs), eval_scondition ctx (fst r) (snd r) = - eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)) - /\ (fst r) = c. + eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)). Proof. unfold cbranch_expanse. - wlp_simplify; inv REF. - unfold eval_scondition; erewrite <- H; eauto. + destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify; + unfold eval_scondition; try erewrite <- H; inversion REF; eauto. + destruct p as [c' l']; simpl. + exploit target_cbranch_expanse_correct; eauto. Qed. Local Hint Resolve cbranch_expanse_correct: wlp. Global Opaque cbranch_expanse. @@ -1133,9 +1134,9 @@ Proof. erewrite <- OK_EQUIV. 2: eauto. eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. } - exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 + exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k)); - exploit H; eauto; intros (SEVAL & EQC); subst; auto. + exploit H; eauto; intros SEVAL; auto. all: simpl in SOUT; generalize SOUT; clear SOUT; inversion_SOME b0; try_simplify_someHyps. @@ -1217,9 +1218,9 @@ Proof. assert (rOK: ris_ok ctx hrs). { simpl in H2; generalize H2; inversion_SOME b0; destruct b0; try_simplify_someHyps. } - exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 + exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k)); - exploit H; eauto; intros (SEVAL & EQC); subst; auto. + exploit H; eauto; intros SEVAL; auto. all: simpl in H2; generalize H2; clear H2; inversion_SOME b0; try_simplify_someHyps. @@ -1444,11 +1445,11 @@ Fixpoint rst_simu_check (rst1 rst2: rstate) {struct rst1} := hrs_simu_check hrs1 hrs2;; sfval_simu_check sfv1 sfv2 | Rcond cond1 lsv1 rsL1 rsR1, Rcond cond2 lsv2 rsL2 rsR2 => - struct_check cond1 cond2 "hsstate_simu_check: conditions do not match";; - phys_check lsv1 lsv2 "hsstate_simu_check: args do not match";; + struct_check cond1 cond2 "rst_simu_check: conditions do not match";; + phys_check lsv1 lsv2 "rst_simu_check: args do not match";; rst_simu_check rsL1 rsL2;; rst_simu_check rsR1 rsR2 - | _, _ => FAILWITH "hsstate_simu_check: simu_check failed" + | _, _ => FAILWITH "rst_simu_check: simu_check failed" end. Lemma rst_simu_check_correct rst1: forall rst2, diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index c812c607..7af1af62 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -260,11 +260,11 @@ Inductive rst_refines ctx: rstate -> sstate -> Prop := (RIS: ris_refines ctx ris sis) (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv) : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv) - | Refcond cond rargs args rifso rifnot ifso ifnot - (RCOND: eval_scondition ctx cond rargs = eval_scondition ctx cond args) - (REFso: eval_scondition ctx cond rargs = Some true -> rst_refines ctx rifso ifso) - (REFnot: eval_scondition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot) - : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args ifso ifnot) + | Refcond rcond cond rargs args rifso rifnot ifso ifnot + (RCOND: eval_scondition ctx rcond rargs = eval_scondition ctx cond args) + (REFso: eval_scondition ctx rcond rargs = Some true -> rst_refines ctx rifso ifso) + (REFnot: eval_scondition ctx rcond rargs = Some false -> rst_refines ctx rifnot ifnot) + : rst_refines ctx (Rcond rcond rargs rifso rifnot) (Scond cond args ifso ifnot) | Refabort : rst_refines ctx Rabort Sabort . |