diff options
-rw-r--r-- | riscV/Asmgen.v | 8 | ||||
-rw-r--r-- | riscV/Asmgenproof1.v | 9 | ||||
-rw-r--r-- | riscV/ExpansionOracle.ml | 69 | ||||
-rw-r--r-- | riscV/NeedOp.v | 24 | ||||
-rw-r--r-- | riscV/Op.v | 70 | ||||
-rw-r--r-- | riscV/PrintOp.ml | 4 | ||||
-rw-r--r-- | riscV/RTLpathSE_simplify.v | 480 | ||||
-rw-r--r-- | riscV/ValueAOp.v | 33 | ||||
-rw-r--r-- | scheduling/RTLpathSE_impl.v | 986 |
9 files changed, 545 insertions, 1138 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index d0c826a3..4876f7ec 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -812,10 +812,10 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pxoriw rd rs n :: k) - | OEluiw n, nil => + | OEluiw n _, a1 :: nil => do rd <- ireg_of res; OK (Pluiw rd n :: k) - | OEaddiwr0 n, nil => + | OEaddiwr0 n _, a1 :: nil => do rd <- ireg_of res; OK (Paddiw rd X0 n :: k) | OEseql optR0, a1 :: a2 :: nil => @@ -860,10 +860,10 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pxoril rd rs n :: k) - | OEluil n, nil => + | OEluil n, a1 :: nil => do rd <- ireg_of res; OK (Pluil rd n :: k) - | OEaddilr0 n, nil => + | OEaddilr0 n, a1 :: nil => do rd <- ireg_of res; OK (Paddil rd X0 n :: k) | OEloadli n, nil => diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 35c5b9d6..a826455e 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1258,10 +1258,11 @@ Opaque Int.eq. { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) - 7: econstructor; split; try apply exec_straight_one; simpl; eauto; - split; intros; Simpl; rewrite Int.add_commut; auto. - 13: econstructor; split; try apply exec_straight_one; simpl; eauto; - split; intros; Simpl; rewrite Int64.add_commut; auto. + 7,8,15,16: + econstructor; split; try apply exec_straight_one; simpl; eauto; + split; intros; Simpl; unfold may_undef_int; try destruct is_long; simpl; + try rewrite Int.add_commut; try rewrite Int64.add_commut; + destruct (rs (preg_of m0)); try discriminate; eauto. all: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0; econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl. diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 11a66322..103285b4 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -35,29 +35,29 @@ let n2pi () = type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul -let load_hilo32 dest hi lo succ k = - if Int.eq lo Int.zero then Iop (OEluiw hi, [], dest, succ) :: k +let load_hilo32 a1 dest hi lo succ is_long k = + if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [a1], dest, succ) :: k else - Iop (OEluiw hi, [], dest, n2pi ()) + Iop (OEluiw (hi, is_long), [a1], dest, n2pi ()) :: Iop (Oaddimm lo, [ dest ], dest, succ) :: k -let load_hilo64 dest hi lo succ k = - if Int64.eq lo Int64.zero then Iop (OEluil hi, [], dest, succ) :: k +let load_hilo64 a1 dest hi lo succ k = + if Int64.eq lo Int64.zero then Iop (OEluil hi, [a1], dest, succ) :: k else - Iop (OEluil hi, [], dest, n2pi ()) + Iop (OEluil hi, [a1], dest, n2pi ()) :: Iop (Oaddlimm lo, [ dest ], dest, succ) :: k -let loadimm32 dest n succ k = +let loadimm32 a1 dest n succ is_long k = match make_immed32 n with - | Imm32_single imm -> Iop (OEaddiwr0 imm, [], dest, succ) :: k - | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ k + | Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [a1], dest, succ) :: k + | Imm32_pair (hi, lo) -> load_hilo32 a1 dest hi lo succ is_long k -let loadimm64 dest n succ k = +let loadimm64 a1 dest n succ k = match make_immed64 n with - | Imm64_single imm -> Iop (OEaddilr0 imm, [], dest, succ) :: k - | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ k + | Imm64_single imm -> Iop (OEaddilr0 imm, [a1], dest, succ) :: k + | Imm64_pair (hi, lo) -> load_hilo64 a1 dest hi lo succ k | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k let get_opimm imm = function @@ -68,12 +68,12 @@ let get_opimm imm = function | Sltil -> OEsltil imm | Sltiul -> OEsltiul imm -let opimm32 a1 dest n succ k op opimm = +let opimm32 a1 dest n succ is_long k op opimm = match make_immed32 n with | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k | Imm32_pair (hi, lo) -> reg := !reg + 1; - load_hilo32 (r2p ()) hi lo (n2pi ()) + load_hilo32 a1 (r2p ()) hi lo (n2pi ()) is_long (Iop (op, [ a1; r2p () ], dest, succ) :: k) let opimm64 a1 dest n succ k op opimm = @@ -81,7 +81,7 @@ let opimm64 a1 dest n succ k op opimm = | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k | Imm64_pair (hi, lo) -> reg := !reg + 1; - load_hilo64 (r2p ()) hi lo (n2pi ()) + load_hilo64 a1 (r2p ()) hi lo (n2pi ()) (Iop (op, [ a1; r2p () ], dest, succ) :: k) | Imm64_large imm -> reg := !reg + 1; @@ -89,11 +89,11 @@ let opimm64 a1 dest n succ k op opimm = :: Iop (op, [ a1; r2p () ], dest, succ) :: k -let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xoriw +let xorimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k Oxor Xoriw -let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Sltiw +let sltimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw -let sltuimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltuw None) Sltiuw +let sltuimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril @@ -233,28 +233,28 @@ let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k = if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k else ( reg := !reg + 1; - loadimm32 (r2p ()) n (n2pi ()) + loadimm32 a1 (r2p ()) n (n2pi ()) false (cbranch_int32s false cmp a1 (r2p ()) info succ1 succ2 k)) let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k = if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k else ( reg := !reg + 1; - loadimm32 (r2p ()) n (n2pi ()) + loadimm32 a1 (r2p ()) n (n2pi ()) false (cbranch_int32u false cmp a1 (r2p ()) info succ1 succ2 k)) let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k = if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k else ( reg := !reg + 1; - loadimm64 (r2p ()) n (n2pi ()) + loadimm64 a1 (r2p ()) n (n2pi ()) (cbranch_int64s false cmp a1 (r2p ()) info succ1 succ2 k)) let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k = if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k else ( reg := !reg + 1; - loadimm64 (r2p ()) n (n2pi ()) + loadimm64 a1 (r2p ()) n (n2pi ()) (cbranch_int64u false cmp a1 (r2p ()) info succ1 succ2 k)) let expanse_condimm_int32s cmp a1 n dest succ k = @@ -262,25 +262,25 @@ let expanse_condimm_int32s cmp a1 n dest succ k = else match cmp with | Ceq | Cne -> - xorimm32 a1 dest n (n2pi ()) + xorimm32 a1 dest n (n2pi ()) false (cond_int32s true cmp dest dest dest succ k) - | Clt -> sltimm32 a1 dest n succ k + | Clt -> sltimm32 a1 dest n succ false k | Cle -> - if Int.eq n (Int.repr Int.max_signed) then loadimm32 dest Int.one succ k - else sltimm32 a1 dest (Int.add n Int.one) succ k + if Int.eq n (Int.repr Int.max_signed) then loadimm32 a1 dest Int.one succ false k + else sltimm32 a1 dest (Int.add n Int.one) succ false k | _ -> reg := !reg + 1; - loadimm32 (r2p ()) n (n2pi ()) + loadimm32 a1 (r2p ()) n (n2pi ()) false (cond_int32s false cmp a1 (r2p ()) dest succ k) let expanse_condimm_int32u cmp a1 n dest succ k = if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k else match cmp with - | Clt -> sltuimm32 a1 dest n succ k + | Clt -> sltuimm32 a1 dest n succ false k | _ -> reg := !reg + 1; - loadimm32 (r2p ()) n (n2pi ()) + loadimm32 a1 (r2p ()) n (n2pi ()) false (cond_int32u false cmp a1 (r2p ()) dest succ k) let expanse_condimm_int64s cmp a1 n dest succ k = @@ -294,11 +294,11 @@ let expanse_condimm_int64s cmp a1 n dest succ k = | Clt -> sltimm64 a1 dest n succ k | Cle -> if Int64.eq n (Int64.repr Int64.max_signed) then - loadimm32 dest Int.one succ k + loadimm32 a1 dest Int.one succ true k else sltimm64 a1 dest (Int64.add n Int64.one) succ k | _ -> reg := !reg + 1; - loadimm64 (r2p ()) n (n2pi ()) + loadimm64 a1 (r2p ()) n (n2pi ()) (cond_int64s false cmp a1 (r2p ()) dest succ k) let expanse_condimm_int64u cmp a1 n dest succ k = @@ -308,7 +308,7 @@ let expanse_condimm_int64u cmp a1 n dest succ k = | Clt -> sltuimm64 a1 dest n succ k | _ -> reg := !reg + 1; - loadimm64 (r2p ()) n (n2pi ()) + loadimm64 a1 (r2p ()) n (n2pi ()) (cond_int64u false cmp a1 (r2p ()) dest succ k) let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k = @@ -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 @@ -510,7 +510,8 @@ let expanse (sb : superblock) code pm = sb.instructions; sb.instructions <- Array.of_list (List.rev !new_order); sb.liveins <- !liveins; - debug_flag := false; + print_ptree_regset !liveins; + (*debug_flag := false;*) (!code', !pm') let rec find_last_node_reg = function diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index a0ec7732..d90c1b66 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -93,23 +93,23 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEsneuw _ => op2 (default nv) | OEsltw _ => op2 (default nv) | OEsltuw _ => op2 (default nv) - | OEsltiw n => op1 (default nv) - | OEsltiuw n => op1 (default nv) - | OExoriw n => op1 (bitwise nv) - | OEluiw n => op1 (default nv) - | OEaddiwr0 n => op1 (modarith nv) + | OEsltiw _ => op1 (default nv) + | OEsltiuw _ => op1 (default nv) + | OExoriw _ => op1 (bitwise nv) + | OEluiw _ _ => op1 (default nv) + | OEaddiwr0 _ _ => op1 (default nv) (* TODO gourdinl modarith impossible? *) | OEseql _ => op2 (default nv) | OEsnel _ => op2 (default nv) | OEsequl _ => op2 (default nv) | OEsneul _ => op2 (default nv) | OEsltl _ => op2 (default nv) | OEsltul _ => op2 (default nv) - | OEsltil n => op1 (default nv) - | OEsltiul n => op1 (default nv) - | OExoril n => op1 (default nv) - | OEluil n => op1 (default nv) - | OEaddilr0 n => op1 (modarith nv) - | OEloadli n => op1 (default nv) + | OEsltil _ => op1 (default nv) + | OEsltiul _ => op1 (default nv) + | OExoril _ => op1 (default nv) + | OEluil _ => op1 (default nv) + | OEaddilr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *) + | OEloadli _ => op1 (default nv) | OEfeqd => op2 (default nv) | OEfltd => op2 (default nv) | OEfled => op2 (default nv) @@ -184,8 +184,6 @@ Proof. - apply shrimm_sound; auto. - apply shruimm_sound; auto. - apply xor_sound; auto with na. -- auto with na. -- auto with na. Qed. Lemma operation_is_redundant_sound: @@ -173,19 +173,19 @@ Inductive operation : Type := (* Expansed conditions *) | OEseqw (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) | OEsnew (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) - | OEsequw (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) - | OEsneuw (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) + | OEsequw (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) + | OEsneuw (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) | OEsltw (optR0: option bool) (**r set-less-than *) | OEsltuw (optR0: option bool) (**r set-less-than unsigned *) | OEsltiw (n: int) (**r set-less-than immediate *) | OEsltiuw (n: int) (**r set-less-than unsigned immediate *) | OExoriw (n: int) (**r xor immediate *) - | OEluiw (n: int) (**r load upper-immediate *) - | OEaddiwr0 (n: int) (**r add immediate *) + | OEluiw (n: int) (is_long: bool) (**r load upper-immediate *) + | OEaddiwr0 (n: int) (is_long: bool) (**r add immediate *) | OEseql (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) | OEsnel (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) - | OEsequl (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) - | OEsneul (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) + | OEsequl (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) + | OEsneul (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) | OEsltl (optR0: option bool) (**r set-less-than *) | OEsltul (optR0: option bool) (**r set-less-than unsigned *) | OEsltil (n: int64) (**r set-less-than immediate *) @@ -263,6 +263,24 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 v | Some false => sem v1 vz end. +Definition may_undef_int (is_long: bool) (sem: val -> val -> val) (v1 vimm vz: val): val := + if negb is_long then + match v1 with + | Vint _ => sem vimm vz + | _ => Vundef + end + else + match v1 with + | Vlong _ => sem vimm vz + | _ => Vundef + end. + +Definition may_undef_luil (v1: val) (n: int64): val := + match v1 with + | Vlong _ => Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))) + | _ => Vundef + end. + Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2 @@ -404,8 +422,8 @@ Definition eval_operation | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n)) | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n)) | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n)) - | OEluiw n, nil => Some(Vint (Int.shl n (Int.repr 12))) - | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32) + | OEluiw n is_long, v1::nil => Some (may_undef_int is_long Val.shl v1 (Vint n) (Vint (Int.repr 12))) + | OEaddiwr0 n is_long, v1::nil => Some (may_undef_int is_long Val.add v1 (Vint n) zero32) | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64)) | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64)) | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) @@ -415,8 +433,8 @@ Definition eval_operation | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n))) | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n))) | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n)) - | OEluil n, nil => Some(Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))) - | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64) + | OEluil n, v1::nil => Some (may_undef_luil v1 n) + | OEaddilr0 n, v1::nil => Some (may_undef_int true Val.addl v1 (Vlong n) zero64) | OEloadli n, nil => Some (Vlong n) | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2) | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2) @@ -605,8 +623,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltiw _ => (Tint :: nil, Tint) | OEsltiuw _ => (Tint :: nil, Tint) | OExoriw _ => (Tint :: nil, Tint) - | OEluiw _ => (nil, Tint) - | OEaddiwr0 _ => (nil, Tint) + | OEluiw _ _ => (Tint :: nil, Tint) + | OEaddiwr0 _ _ => (Tint :: nil, Tint) | OEseql _ => (Tlong :: Tlong :: nil, Tint) | OEsnel _ => (Tlong :: Tlong :: nil, Tint) | OEsequl _ => (Tlong :: Tlong :: nil, Tint) @@ -616,8 +634,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltil _ => (Tlong :: nil, Tint) | OEsltiul _ => (Tlong :: nil, Tint) | OExoril _ => (Tlong :: nil, Tlong) - | OEluil _ => (nil, Tlong) - | OEaddilr0 _ => (nil, Tlong) + | OEluil _ => (Tlong :: nil, Tlong) + | OEaddilr0 _ => (Tlong :: nil, Tlong) | OEloadli _ => (nil, Tlong) | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) | OEfltd => (Tfloat :: Tfloat :: nil, Tint) @@ -857,9 +875,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OExoriw *) - destruct v0... (* OEluiw *) - - trivial. + - unfold may_undef_int; + destruct v0, is_long; simpl; trivial; + destruct (Int.ltu _ _); cbn; trivial. (* OEaddiwr0 *) - - trivial. + - destruct v0, is_long; simpl; trivial. (* OEseql *) - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... @@ -886,9 +906,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OExoril *) - destruct v0... (* OEluil *) - - trivial. + - destruct v0; simpl; trivial. (* OEaddilr0 *) - - trivial. + - destruct v0; simpl; trivial. (* OEloadli *) - trivial. (* OEfeqd *) @@ -1691,6 +1711,15 @@ Proof. - apply eval_cmpu_bool_inj; auto. (* OExoriw *) - inv H4; simpl; auto. + (* OEluiw *) + - unfold may_undef_int; + destruct is_long; + inv H4; simpl; auto; + destruct (Int.ltu _ _); auto. + (* OEaddiwr0 *) + - unfold may_undef_int; + destruct is_long; + inv H4; simpl; auto. (* OEseql *) - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; @@ -1715,6 +1744,11 @@ Proof. - apply eval_cmplu_bool_inj; auto. (* OExoril *) - inv H4; simpl; auto. + (* OEluil *) + - inv H4; simpl; auto. + (* OEaddilr0 *) + - unfold may_undef_int; + inv H4; simpl; auto. (* OEfeqd *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index 2b5ae1f5..2738e16d 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -192,8 +192,8 @@ let print_operation reg pp = function | OEsltiw n, [r1] -> fprintf pp "OEsltiw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n) | OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n) - | OEluiw n, [] -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n) - | OEaddiwr0 n, [] -> fprintf pp "OEaddiwr0(%ld,X0)" (camlint_of_coqint n) + | OEluiw (n, _), [] -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n) + | OEaddiwr0 (n, _), [] -> fprintf pp "OEaddiwr0(%ld,X0)" (camlint_of_coqint n) | OEseql optR0, [r1;r2] -> fprintf pp "OEseql"; (get_optR0_s Ceq reg pp r1 r2 optR0) | OEsnel optR0, [r1;r2] -> fprintf pp "OEsnel"; (get_optR0_s Cne reg pp r1 r2 optR0) | OEsltl optR0, [r1;r2] -> fprintf pp "OEsltl"; (get_optR0_s Clt reg pp r1 r2 optR0) diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 311f2828..f17dfe7d 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -4,6 +4,7 @@ Require Import Op Registers. Require Import RTLpathSE_theory. Require Import RTLpathSE_simu_specs. Require Import Asmgen Asmgenproof1. +Require Import Lia. (** Useful functions for conditions/branches expansion *) @@ -30,44 +31,48 @@ Definition make_lhsv_single (hvs: hsval) : list_hsval := (* Immediate loads *) -Definition load_hilo32 (hi lo: int) := +Definition load_hilo32 (hv1: hsval) (hi lo: int) (is_long: bool) := + let hl := make_lhsv_single hv1 in if Int.eq lo Int.zero then - fSop (OEluiw hi) fSnil + fSop (OEluiw hi is_long) hl else - let hvs := fSop (OEluiw hi) fSnil in - let hl := make_lhsv_single hvs in - fSop (Oaddimm lo) hl. + let hvs := fSop (OEluiw hi is_long) hl in + let hl' := make_lhsv_single hvs in + fSop (Oaddimm lo) hl'. -Definition load_hilo64 (hi lo: int64) := +Definition load_hilo64 (hv1: hsval) (hi lo: int64) := + let hl := make_lhsv_single hv1 in if Int64.eq lo Int64.zero then - fSop (OEluil hi) fSnil + fSop (OEluil hi) hl else - let hvs := fSop (OEluil hi) fSnil in + let hvs := fSop (OEluil hi) hl in let hl := make_lhsv_single hvs in fSop (Oaddlimm lo) hl. -Definition loadimm32 (n: int) := +Definition loadimm32 (hv1: hsval) (n: int) (is_long: bool) := match make_immed32 n with | Imm32_single imm => - fSop (OEaddiwr0 imm) fSnil - | Imm32_pair hi lo => load_hilo32 hi lo + let hl := make_lhsv_single hv1 in + fSop (OEaddiwr0 imm is_long) hl + | Imm32_pair hi lo => load_hilo32 hv1 hi lo is_long end. -Definition loadimm64 (n: int64) := +Definition loadimm64 (hv1: hsval) (n: int64) := match make_immed64 n with | Imm64_single imm => - fSop (OEaddilr0 imm) fSnil - | Imm64_pair hi lo => load_hilo64 hi lo + let hl := make_lhsv_single hv1 in + fSop (OEaddilr0 imm) hl + | Imm64_pair hi lo => load_hilo64 hv1 hi lo | Imm64_large imm => fSop (OEloadli imm) fSnil end. -Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) := +Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) (is_long: bool) := match make_immed32 n with | Imm32_single imm => let hl := make_lhsv_single hv1 in fSop (opimm imm) hl | Imm32_pair hi lo => - let hvs := load_hilo32 hi lo in + let hvs := load_hilo32 hv1 hi lo is_long in let hl := make_lhsv_cmp false hv1 hvs in fSop op hl end. @@ -78,7 +83,7 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper let hl := make_lhsv_single hv1 in fSop (opimm imm) hl | Imm64_pair hi lo => - let hvs := load_hilo64 hi lo in + let hvs := load_hilo64 hv1 hi lo in let hl := make_lhsv_cmp false hv1 hvs in fSop op hl | Imm64_large imm => @@ -87,9 +92,9 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper fSop op hl end. -Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw. -Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw. -Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw. +Definition xorimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n Oxor OExoriw is_long. +Definition sltimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltw None) OEsltiw is_long. +Definition sltuimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltuw None) OEsltiuw is_long. Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril. Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil. Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul. @@ -150,17 +155,17 @@ Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) := match cmp with | Ceq | Cne => let optR0 := make_optR0 true is_inv in - let hvs := xorimm32 hv1 n in + let hvs := xorimm32 hv1 n false in let hl := make_lhsv_cmp false hvs hvs in cond_int32s cmp hl optR0 - | Clt => sltimm32 hv1 n + | Clt => sltimm32 hv1 n false | Cle => if Int.eq n (Int.repr Int.max_signed) then - loadimm32 Int.one - else sltimm32 hv1 (Int.add n Int.one) + loadimm32 hv1 Int.one false + else sltimm32 hv1 (Int.add n Int.one) false | _ => let optR0 := make_optR0 false is_inv in - let hvs := loadimm32 n in + let hvs := loadimm32 hv1 n false in let hl := make_lhsv_cmp is_inv hv1 hvs in cond_int32s cmp hl optR0 end. @@ -173,10 +178,10 @@ Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) := cond_int32u cmp hl optR0 else match cmp with - | Clt => sltuimm32 hv1 n + | Clt => sltuimm32 hv1 n false | _ => let optR0 := make_optR0 false is_inv in - let hvs := loadimm32 n in + let hvs := loadimm32 hv1 n false in let hl := make_lhsv_cmp is_inv hv1 hvs in cond_int32u cmp hl optR0 end. @@ -197,11 +202,11 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) := | Clt => sltimm64 hv1 n | Cle => if Int64.eq n (Int64.repr Int64.max_signed) then - loadimm32 Int.one + loadimm32 hv1 Int.one true else sltimm64 hv1 (Int64.add n Int64.one) | _ => let optR0 := make_optR0 false is_inv in - let hvs := loadimm64 n in + let hvs := loadimm64 hv1 n in let hl := make_lhsv_cmp is_inv hv1 hvs in cond_int64s cmp hl optR0 end. @@ -217,7 +222,7 @@ Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) := | Clt => sltuimm64 hv1 n | _ => let optR0 := make_optR0 false is_inv in - let hvs := loadimm64 n in + let hvs := loadimm64 hv1 n in let hl := make_lhsv_cmp is_inv hv1 hvs in cond_int64u cmp hl optR0 end. @@ -246,6 +251,48 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) := let hl := make_lhsv_single hvs in if normal' then hvs else fSop (OExoriw Int.one) hl. +(* Branches instructions *) + +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 => CEbequw optR0 + | Cne => CEbneuw 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 => CEbequl optR0 + | Cne => CEbneul optR0 + | Clt => CEbltul optR0 + | Cle => CEbgeul optR0 + | Cgt => CEbltul optR0 + | Cge => CEbgeul optR0 + end. + (** Target op simplifications using "fake" values *) Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := @@ -317,6 +364,111 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca | _, _ => None end. +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) => + 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)*) + (*| (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 + 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) + | (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 + let lhsv := make_lhsv_cmp is_inv hv1 hv1 in + let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in + Some (cond, lhsv) + else + let hvs := loadimm32 n in + let lhsv := make_lhsv_cmp is_inv hv1 hvs in + let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in + Some (cond, lhsv)) + | (Ccompuimm 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 + let lhsv := make_lhsv_cmp is_inv hv1 hv1 in + let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in + Some (cond, lhsv) + else + let hvs := loadimm32 n in + let lhsv := make_lhsv_cmp is_inv hv1 hvs in + let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in + Some (cond, lhsv)) + | (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 + 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) + | (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 + 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) + | (Ccomplimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + let hv1 := fsi_sreg_get prev a1 in + (if Int64.eq n Int64.zero then + let lhsv := make_lhsv_cmp is_inv hv1 hv1 in + let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in + Some (cond, lhsv) + else + let hvs := loadimm64 n in + let lhsv := make_lhsv_cmp is_inv hv1 hvs in + let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in + Some (cond, lhsv)) + | (Ccompluimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + let hv1 := fsi_sreg_get prev a1 in + (if Int64.eq n Int64.zero then + let lhsv := make_lhsv_cmp is_inv hv1 hv1 in + let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in + Some (cond, lhsv) + else + let hvs := loadimm64 n in + let lhsv := make_lhsv_cmp is_inv hv1 hvs in + let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in + Some (cond, lhsv)) + | (Ccompf 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_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 + | (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 + | (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*) + | _, _ => None + end. + (** Auxiliary lemmas on comparisons *) (* Signed ints *) @@ -360,6 +512,14 @@ Proof. repeat destruct (_ && _); simpl; auto. Qed. +Remark ltu_12_wordsize: + Int.ltu (Int.repr 12) Int.iwordsize = true. +Proof. + unfold Int.iwordsize, Int.zwordsize. simpl. + unfold Int.ltu. apply zlt_true. + rewrite !Int.unsigned_repr; try cbn; try omega. +Qed. + (* Signed longs *) Lemma xor_neg_ltle_cmpl: forall v1 v2, @@ -400,6 +560,24 @@ Proof. rewrite Int64.xor_is_zero in EQ1; congruence. Qed. +Lemma cmp_ltle_add_one: forall v n, + Int.eq n (Int.repr Int.max_signed) = false -> + Some (Val.of_optbool (Val.cmp_bool Clt v (Vint (Int.add n Int.one)))) = + Some (Val.of_optbool (Val.cmp_bool Cle v (Vint n))). +Proof. + intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto. + unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). + destruct (zlt (Int.signed n) (Int.signed i)). + rewrite zlt_false by omega. auto. + rewrite zlt_true by omega. auto. + rewrite Int.add_signed. symmetry; apply Int.signed_repr. + specialize (Int.eq_spec n (Int.repr Int.max_signed)). + rewrite EQMAX; simpl; intros. + assert (Int.signed n <> Int.max_signed). + { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. } + generalize (Int.signed_range n); omega. +Qed. + Lemma cmpl_ltle_add_one: forall v n, Int64.eq n (Int64.repr Int64.max_signed) = false -> Some (Val.of_optbool (Val.cmpl_bool Clt v (Vlong (Int64.add n Int64.one)))) = @@ -418,6 +596,26 @@ Proof. generalize (Int64.signed_range n); omega. Qed. +Remark lt_maxsgn_false_int: forall i, + Int.lt (Int.repr Int.max_signed) i = false. +Proof. + intros; unfold Int.lt. + specialize Int.signed_range with i; intros. + rewrite zlt_false; auto. destruct H. + rewrite Int.signed_repr; try (cbn; lia). + apply Z.le_ge. trivial. +Qed. + +Remark lt_maxsgn_false_long: forall i, + Int64.lt (Int64.repr Int64.max_signed) i = false. +Proof. + intros; unfold Int64.lt. + specialize Int64.signed_range with i; intros. + rewrite zlt_false; auto. destruct H. + rewrite Int64.signed_repr; try (cbn; lia). + apply Z.le_ge. trivial. +Qed. + (* Unsigned longs *) Lemma xor_neg_ltle_cmplu: forall mptr v1 v2, @@ -593,6 +791,66 @@ Proof. rewrite xor_neg_optb; trivial. Qed. +Lemma simplify_ccompimm_correct ge sp hst st c r n rs0 m m0 v: forall + (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), + seval_smem ge sp (si_smem st) rs0 m0 = Some m -> + Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp + (hsval_proj (expanse_condimm_int32s c (fsi_sreg_get hst r) n)) rs0 m0 = + Some (Val.of_optbool (Val.cmp_bool c v (Vint n))). +Proof. + intros. + unfold expanse_condimm_int32s, cond_int32s in *; destruct c; + intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl; + try apply Int.same_if_eq in EQIMM; subst; + unfold loadimm32, sltimm32, xorimm32, opimm32, load_hilo32; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + unfold Val.cmp, zero32. + all: + try apply xor_neg_ltle_cmp; + try apply xor_neg_ltge_cmp; trivial. + 4: + try destruct (Int.eq n (Int.repr Int.max_signed)) eqn:EQMAX; subst; + try apply Int.same_if_eq in EQMAX; subst; simpl. + 4: + intros; try (specialize make_immed32_sound with (Int.one); + destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl. + 6: + intros; try (specialize make_immed32_sound with (Int.add n Int.one); + destruct (make_immed32 (Int.add n Int.one)) eqn:EQMKI_A2); intros; simpl. + 1,2,3,8,9: + intros; try (specialize make_immed32_sound with (n); + destruct (make_immed32 n) eqn:EQMKI); intros; simpl. + all: + try destruct (Int.eq lo Int.zero) eqn:EQLO32; + try apply Int.same_if_eq in EQLO32; subst; + try erewrite fSop_correct; eauto; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + try rewrite OK2; + try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst; + try rewrite xor_neg_ltle_cmp; trivial; + unfold Val.cmp, may_undef_int, zero32, Val.add; simpl; + destruct v; auto. + all: + try rewrite ltu_12_wordsize; + try rewrite <- H; + try (apply cmp_ltle_add_one; auto); + try rewrite Int.add_commut, Int.add_zero_l in *; + try ( + simpl; trivial; + try rewrite Int.xor_is_zero; + try destruct (Int.lt _ _) eqn:EQLT; trivial; + try rewrite lt_maxsgn_false_int in EQLT; + simpl; trivial; try discriminate; fail). +Qed. + Lemma simplify_ccompuimm_correct ge sp hst st c r n rs0 m m0 v: forall (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), seval_smem ge sp (si_smem st) rs0 m0 = Some m -> @@ -612,36 +870,31 @@ Proof. erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto. unfold expanse_condimm_int32u, cond_int32u in *; destruct c; intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl; + try apply Int.same_if_eq in EQIMM; subst; unfold loadimm32, sltuimm32, opimm32, load_hilo32; try erewrite !fsi_sreg_get_correct; eauto; try rewrite OKv1; trivial; + try rewrite xor_neg_ltle_cmpu; unfold Val.cmpu, zero32. - (* Simplify make immediate and decompose subcases *) all: try (specialize make_immed32_sound with n; destruct (make_immed32 n) eqn:EQMKI); try destruct (Int.eq lo Int.zero) eqn:EQLO; + try apply Int.same_if_eq in EQLO; subst; + intros; subst; try erewrite fSop_correct; eauto; simpl; try erewrite !fsi_sreg_get_correct; eauto; try rewrite OKv1; try rewrite OK2; - rewrite HMEM. - (* Ceq, Cne, Clt = itself *) - all: intros; try apply Int.same_if_eq in EQIMM; subst; trivial. - (* Cle = xor (Clt) *) - all: try apply xor_neg_ltle_cmpu; trivial. - (* Others subcases with swap/negation *) - all: - unfold Val.cmpu; - try apply Int.same_if_eq in EQLO; subst; - try rewrite Int.add_commut, Int.add_zero_l in *; trivial; - try (rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu; - trivial; fail); - try (replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmpu_bool; trivial; fail); - try (replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb; trivial; fail). - all: rewrite HMEM; trivial. + rewrite HMEM; + unfold may_undef_int, Val.cmpu; + destruct v; simpl; auto; + try rewrite EQIMM; try destruct (Archi.ptr64); simpl; + try rewrite ltu_12_wordsize; trivial; + try rewrite Int.add_commut, Int.add_zero_l; + try destruct (Int.ltu _ _) eqn:EQLTU; simpl; + try rewrite EQLTU; simpl; + trivial. Qed. Lemma simplify_ccompl_correct ge sp hst st c r r0 rs0 m0 v v0: forall @@ -718,53 +971,64 @@ Proof. intros. unfold expanse_condimm_int64s, cond_int64s in *; destruct c; intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl; + try apply Int64.same_if_eq in EQIMM; subst; unfold loadimm32, loadimm64, sltimm64, xorimm64, opimm64, load_hilo32, load_hilo64; try erewrite !fsi_sreg_get_correct; eauto; try rewrite OKv1; unfold Val.cmpl, zero64. - (* Simplify make immediate and decompose subcases *) - 2,4,6,10,12: - try (specialize make_immed64_sound with n; - destruct (make_immed64 n) eqn:EQMKI_A0). - 20: - try (specialize make_immed32_sound with (Int.one); - destruct (make_immed32 Int.one) eqn:EQMKI_A1). - 20,21: - try (specialize make_immed64_sound with (Int64.add n Int64.one); - destruct (make_immed64 (Int64.add n Int64.one)) eqn:EQMKI_A2). all: + try apply xor_neg_ltle_cmpl; + try apply xor_neg_ltge_cmpl; + try rewrite optbool_mktotal; trivial. + 4: + try destruct (Int64.eq n (Int64.repr Int64.max_signed)) eqn:EQMAX; subst; + try apply Int64.same_if_eq in EQMAX; subst; simpl. + 4: + intros; try (specialize make_immed32_sound with (Int.one); + destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl. + 6: + intros; try (specialize make_immed64_sound with (Int64.add n Int64.one); + destruct (make_immed64 (Int64.add n Int64.one)) eqn:EQMKI_A2); intros; simpl. + 1,2,3,9,10: + intros; try (specialize make_immed64_sound with (n); + destruct (make_immed64 n) eqn:EQMKI); intros; simpl. + all: try destruct (Int.eq lo Int.zero) eqn:EQLO32; + try apply Int.same_if_eq in EQLO32; subst; try destruct (Int64.eq lo Int64.zero) eqn:EQLO64; - try destruct (Int64.eq lo0 Int64.zero) eqn:EQLO064; - try destruct (Int64.eq n (Int64.repr Int64.max_signed)) eqn:EQMAX; + try apply Int64.same_if_eq in EQLO64; subst; try erewrite fSop_correct; eauto; simpl; try erewrite !fsi_sreg_get_correct; eauto; try rewrite OKv1; - try rewrite OK2. - (* Ceq, Cne, Clt = itself *) - all: intros; try apply Int64.same_if_eq in EQIMM; subst; - try (rewrite optbool_mktotal; trivial; fail). - (* Others simple subcases *) - all: - unfold Val.cmpl; - try apply Int64.same_if_eq in EQLO64; subst; - try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial; - try (rewrite <- xor_neg_ltle_cmpl; unfold Val.cmpl; - trivial; fail); - try erewrite xorl_zero_eq_cmpl; eauto; - try apply xor_neg_ltle_cmpl; - try apply xor_neg_ltge_cmpl; - trivial; - try rewrite optbool_mktotal; trivial. - + try rewrite OK2; + unfold may_undef_luil; + try rewrite (Int64.add_commut _ Int64.zero), Int64.add_zero_l in H; subst; + try fold (Val.cmpl Clt v (Vlong imm)); + try rewrite xor_neg_ltge_cmpl; trivial; + try rewrite xor_neg_ltle_cmpl; trivial; + unfold Val.cmpl, may_undef_luil, Val.addl; + try rewrite xorl_zero_eq_cmpl; trivial; + try rewrite optbool_mktotal; trivial; + unfold may_undef_int, zero32, Val.add; simpl; + destruct v; auto. + 6,7,8: + try rewrite <- optbool_mktotal; trivial; + try rewrite Int64.add_commut, Int64.add_zero_l in *; + try fold (Val.cmpl Clt (Vlong i) (Vlong imm)); + try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))))); + try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo))); + try rewrite xor_neg_ltge_cmpl; trivial; + try rewrite xor_neg_ltle_cmpl; trivial. all: - try apply Int64.same_if_eq in EQLO064; subst; - try rewrite (Int64.add_commut (Int64.sign_ext 32 (Int64.shl hi0 (Int64.repr 12))) Int64.zero) in H; - try rewrite (Int64.add_commut (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) Int64.zero) in H; - try rewrite Int64.add_zero_l in H; try rewrite <- H; - try apply cmpl_ltle_add_one; auto. -all: admit. -Admitted. + try rewrite <- H; + try apply cmpl_ltle_add_one; auto; + try rewrite ltu_12_wordsize; + try rewrite Int.add_commut, Int.add_zero_l in *; + try rewrite Int64.add_commut, Int64.add_zero_l in *; + simpl; try rewrite lt_maxsgn_false_long; + try (rewrite <- H; trivial; fail); + simpl; trivial. +Qed. Lemma simplify_ccompluimm_correct ge sp hst st c r n rs0 m m0 v: forall (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), @@ -805,7 +1069,7 @@ Proof. all: try apply xor_neg_ltle_cmplu; trivial. (* Others subcases with swap/negation *) all: - unfold Val.cmplu; + unfold Val.cmplu, may_undef_int, zero64, Val.addl; try apply Int64.same_if_eq in EQLO; subst; try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial; try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu; @@ -814,10 +1078,15 @@ Proof. rewrite Val.swap_cmplu_bool; trivial; fail); try (replace (Clt) with (negate_comparison Cge) by auto; rewrite Val.negate_cmplu_bool; rewrite xor_neg_optb; trivial; fail); - rewrite optbool_mktotal; trivial. + try rewrite optbool_mktotal; trivial. all: + try destruct v; simpl; auto; + try destruct (Archi.ptr64); simpl; + try rewrite EQIMM; try rewrite HMEM; trivial; - rewrite <- xor_neg_ltge_cmplu; unfold Val.cmplu; rewrite <- optbool_mktotal; trivial. + try destruct (Int64.ltu _ _); + try rewrite <- xor_neg_ltge_cmplu; unfold Val.cmplu; + try rewrite <- optbool_mktotal; trivial. Qed. Lemma simplify_ccompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall @@ -945,7 +1214,7 @@ Proof. (* Ccompu *) - eapply simplify_ccompu_correct; eauto. (* Ccompimm *) - - (* TODO gourdinl *) admit. + - eapply simplify_ccompimm_correct; eauto. (* Ccompuimm *) - eapply simplify_ccompuimm_correct; eauto. (* Ccompl *) @@ -953,7 +1222,7 @@ Proof. (* Ccomplu *) - eapply simplify_ccomplu_correct; eauto. (* Ccomplimm *) - - admit. + - eapply simplify_ccomplimm_correct; eauto. (* Ccompluimm *) - eapply simplify_ccompluimm_correct; eauto. (* Ccompf *) @@ -964,7 +1233,36 @@ Proof. - eapply simplify_ccompfs_correct; eauto. (* Cnotcompfs *) - eapply simplify_cnotcompfs_correct; eauto. - Admitted. +Qed. + +Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall + (TARGET: target_cbranch_expanse hst c l = Some (c', l')) + (LREF : hsilocal_refines ge sp rs0 m0 hst st) + (OK: hsok_local ge sp rs0 m0 hst), + 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. +Proof. + (*unfold target_cbranch_expanse, seval_condition; simpl. + intros H (LREF & SREF & SREG & SMEM) ?. + destruct c; try congruence. + + all: + repeat (destruct l; simpl in H; try congruence); + destruct c; inv H; simpl; + erewrite !fsi_sreg_get_correct; eauto; + try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); + try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence). + + all: + 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.*) + all:admit. +Admitted. (*Qed.*) Global Opaque target_op_simplify. - +Global Opaque target_cbranch_expanse. diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 581229c6..00b49bc1 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -27,6 +27,24 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 | Some false => sem v1 vz end. +Definition may_undef_int (is_long: bool) (sem: aval -> aval -> aval) (v1 vimm vz: aval): aval := + if negb is_long then + match v1 with + | I _ => sem vimm vz + | _ => Ifptr Ptop + end + else + match v1 with + | L _ => sem vimm vz + | _ => Ifptr Ptop + end. + +Definition may_undef_luil (v1: aval) (n: int64): aval := + match v1 with + | L _ => sign_ext 32 (shll (L n) (L (Int64.repr 12))) + | _ => Ifptr Ptop + end. + Definition eval_static_condition (cond: condition) (vl: list aval): abool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 @@ -172,8 +190,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) - | OEluiw n, nil => I (Int.shl n (Int.repr 12)) - | OEaddiwr0 n, nil => add (I n) zero32 + | OEluiw n is_long, v1::nil => may_undef_int is_long shl v1 (I n) (I (Int.repr 12)) + | OEaddiwr0 n is_long, v1::nil => may_undef_int is_long add v1 (I n) zero32 | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64) | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64) | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64) @@ -183,8 +201,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) | OExoril n, v1::nil => xorl v1 (L n) - | OEluil n, nil => L (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))) - | OEaddilr0 n, nil => addl (L n) zero64 + | OEluil n, v1::nil => may_undef_luil v1 n + | OEaddilr0 n, v1::nil => may_undef_int true addl v1 (L n) zero64 | OEloadli n, nil => L (n) | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2) @@ -340,6 +358,13 @@ Proof. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. unfold zero32; simpl; eauto with va. + + 1,2,11,12: + try unfold Op.may_undef_int, may_undef_int, Op.zero32, zero32, Op.zero64, zero64; + try unfold Op.may_undef_luil, may_undef_luil; simpl; unfold ntop1; + inv H1; try destruct is_long; simpl; try destruct (Int.ltu _ _); eauto with va; + try apply vmatch_ifptr_i; try apply vmatch_ifptr_l. + 3,4,6: apply eval_cmplu_sound; auto. 1,2,3: apply eval_cmpl_sound; auto. unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 4a1a5f5b..06fdaab4 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -647,27 +647,6 @@ Proof. explore; try congruence. Qed. -(* TODO gourdinl MOVE EXPANSIONS BELOW ELSEWHERE *) - -(* TODO gourdinl IF NEEDED LATER Fixpoint hlist_sval (l: list hsval): ?? list_hsval := - match l with - | nil => hSnil() - | r::l => - DO lhsv <~ hlist_sval l;; - hScons r lhsv - end.*) - -(* - - - - - - - - - *) - (** simplify a symbolic value before assignment to a register *) Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval := match rsv with @@ -687,729 +666,6 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs hSload hst NOTRAP chunk addr lhsv end. -(* -Lemma simplify_nothing lr (hst: hsistate_local) op: - WHEN DO lhsv <~ hlist_args hst lr;; hSop op lhsv ~> hv - THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) - (m0 : mem) (st : sistate_local), - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp op args m) <> None -> - seval_sval ge sp (hsval_proj hv) rs0 m0 = - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp op args m)). -Proof. - wlp_simplify. - generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0. - destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto. - intro H0; clear H0; simplify_SOME z; congruence. -Qed. - - -Lemma xor_ceq_zero: forall v n cmp, - cmp = Ceq \/ cmp = Cne -> - Some - (Val.of_optbool (Val.cmp_bool cmp (Val.xor v (Vint n)) (Vint Int.zero))) = - Some (Val.of_optbool (Val.cmp_bool cmp v (Vint n))). -Proof. - intros; destruct v; unfold Val.xor; simpl; auto. - destruct cmp, H; try discriminate; simpl; - destruct (Int.eq (Int.xor i n) Int.zero) eqn:EQ; - rewrite Int.xor_is_zero in EQ; rewrite EQ; trivial. -Qed. - -(* TODO gourdinl Lemma xor_neg_ltge_cmp: forall v1 v2, - Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmp_bool Cge v1 v2)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - unfold Val.cmp; simpl; - try rewrite Int.eq_sym; - try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl; - try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one; - auto. - Qed.*) - -(* TODO gourdinl useless? Lemma cmp_neg_ltgt_cmp: forall v1 v2, - Some (Val.cmp Clt v1 v2) = Some (Val.of_optbool (Val.cmp_bool Cgt v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence; - unfold Val.cmp; simpl; auto. - Qed.*) - - -(* TODO gourdinl Lemma xor_neg_ltge_cmpu: forall mptr v1 v2, - Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cge v1 v2)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - unfold Val.cmpu; simpl; - try rewrite Int.eq_sym; - try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl; - try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one; - auto. - 1,2: - unfold Val.cmpu, Val.cmpu_bool; - destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _); - try destruct (eq_block _ _); auto. - unfold Val.cmpu, Val.cmpu_bool; simpl; - destruct Archi.ptr64; try destruct (_ || _); simpl; auto; - destruct (eq_block b b0); destruct (eq_block b0 b); - try congruence; - try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); - simpl; auto; - repeat destruct (_ && _); simpl; auto. - Qed.*) - -(* TODO gourdinl Lemma cmp_neg_ltgt_cmpu: forall mptr v1 v2, - Some (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) = - Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cgt v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence; - unfold Val.cmpu; simpl; auto. - destruct (Archi.ptr64); - destruct (eq_block b b0); destruct (eq_block b0 b); - try congruence. - - repeat destruct (_ || _); simpl; auto. - - repeat destruct (_ && _); simpl; auto. - Qed.*) - -Lemma optbool_mktotal: forall v, - Some (Val.maketotal (option_map Val.of_bool v)) = - Some (Val.of_optbool v). -Proof. - intros. eapply f_equal. - destruct v; simpl; auto. -Qed. - -Lemma cmplu_optbool_mktotal: forall mptr cmp v1 v2, - Some (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) cmp v1 v2)) = - Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) cmp v1 v2)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence; - unfold Val.cmplu; simpl; auto; - destruct (Archi.ptr64); simpl; - try destruct (eq_block _ _); simpl; - try destruct (_ && _); simpl; - try destruct (Ptrofs.cmpu _ _); - try destruct cmp; simpl; auto. -Qed. - -Lemma xor_neg_ltle_cmpl: forall v1 v2, - Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmpl_bool Cle v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - destruct (Int64.lt _ _); auto. -Qed. - -Lemma cmp_neg_ltgt_cmpl: forall v1 v2, - Some (Val.maketotal (Val.cmpl Clt v1 v2)) = - Some (Val.of_optbool (Val.cmpl_bool Cgt v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - destruct (Int64.lt _ _); auto. -Qed. - -Lemma xor_neg_ltge_cmpl: forall v1 v2, - Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmpl_bool Cge v1 v2)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - destruct (Int64.lt _ _); auto. -Qed. - -Lemma xor_neg_ltle_cmplu: forall mptr v1 v2, - Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cle v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - destruct (Int64.ltu _ _); auto. - 1,2: unfold Val.cmplu; simpl; auto; - destruct (Archi.ptr64); simpl; - try destruct (eq_block _ _); simpl; - try destruct (_ && _); simpl; - try destruct (Ptrofs.cmpu _ _); - try destruct cmp; simpl; auto. - unfold Val.cmplu; simpl; - destruct Archi.ptr64; try destruct (_ || _); simpl; auto; - destruct (eq_block b b0); destruct (eq_block b0 b); - try congruence; - try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); - simpl; auto; - repeat destruct (_ && _); simpl; auto. -Qed. - -Lemma cmp_neg_ltgt_cmplu: forall mptr v1 v2, - Some (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) = - Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cgt v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - destruct (Int64.ltu _ _); auto. - 1,2: unfold Val.cmplu; simpl; auto; - destruct (Archi.ptr64); simpl; - try destruct (eq_block _ _); simpl; - try destruct (_ && _); simpl; - try destruct (Ptrofs.cmpu _ _); - try destruct cmp; simpl; auto. - unfold Val.cmplu; simpl; - destruct Archi.ptr64; try destruct (_ || _); simpl; auto; - destruct (eq_block b b0); destruct (eq_block b0 b); - try congruence; - try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); - simpl; auto; - repeat destruct (_ && _); simpl; auto. -Qed. - -Lemma xor_neg_ltge_cmplu: forall mptr v1 v2, - Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cge v1 v2)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - destruct (Int64.ltu _ _); auto. - 1,2: unfold Val.cmplu; simpl; auto; - destruct (Archi.ptr64); simpl; - try destruct (eq_block _ _); simpl; - try destruct (_ && _); simpl; - try destruct (Ptrofs.cmpu _ _); - try destruct cmp; simpl; auto. - unfold Val.cmplu; simpl; - destruct Archi.ptr64; try destruct (_ || _); simpl; auto; - destruct (eq_block b b0); destruct (eq_block b0 b); - try congruence; - try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); - simpl; auto; - repeat destruct (_ && _); simpl; auto. -Qed. - - - -Lemma xor_neg_eqne_cmpfs: forall v1 v2, - Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmpfs_bool Cne v1 v2)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence; - unfold Val.cmpfs; simpl. - rewrite Float32.cmp_ne_eq. - destruct (Float32.cmp _ _ _); simpl; auto. -Qed. - -Lemma cmp_neg_ltgt_cmpf: forall v1 v2, - Some (Val.cmpf Clt v1 v2) = Some (Val.of_optbool (Val.cmpf_bool Cgt v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence; - unfold Val.cmpf; simpl; auto. - replace Cgt with (swap_comparison Clt) by auto. - rewrite Float.cmp_swap. - destruct (Float.cmp _ _ _); simpl; auto. -Qed. - -Lemma cmp_neg_lege_cmpf: forall v1 v2, - Some (Val.cmpf Cle v1 v2) = Some (Val.of_optbool (Val.cmpf_bool Cge v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence; - unfold Val.cmpf; simpl; auto. - replace Cle with (swap_comparison Cge) by auto. - rewrite Float.cmp_swap. - destruct (Float.cmp _ _ _); simpl; auto. -Qed. - - - -(* TODO gourdinl Lemma cmp_le_max: forall v*) - (*(CONTRA: Some*) - (*(Val.of_optbool (Val.cmp_bool Cle v (Vint (Int.repr Int.max_signed)))) =*) - (*None -> False),*) - (*Some (Vint Int.one) =*) - (*Some (Val.of_optbool (Val.cmp_bool Cle v (Vint (Int.repr Int.max_signed)))).*) -(*Proof.*) - (*intros; destruct v. simpl in *; try discriminate CONTRA; auto.*) - -Lemma simplify_ccomp_correct: forall c r r0 (hst: hsistate_local), - WHEN DO hv1 <~ hsi_sreg_get hst r;; - DO hv2 <~ hsi_sreg_get hst r0;; - DO lhsv <~ make_lhsv_cmp (is_inv_cmp_int c) hv1 hv2;; - cond_int32s c lhsv None ~> hv - THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) - (m0 : mem) (st : sistate_local), - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccomp c)) args m) <> None -> - seval_sval ge sp (hsval_proj hv) rs0 m0 = - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccomp c)) args m)). -Proof. - unfold cond_int32s in *; destruct c; - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail). - all: - try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto); - erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; - erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; - simplify_SOME z; unfold Val.cmp. - - intros; apply xor_neg_ltle_cmp. - - intros; replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmp_bool; trivial. - - intros; replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmp_bool. - rewrite xor_neg_optb; trivial. -Qed. - -Lemma simplify_ccompu_correct: forall c r r0 (hst: hsistate_local), - WHEN DO hv1 <~ hsi_sreg_get hst r;; - DO hv2 <~ hsi_sreg_get hst r0;; - DO lhsv <~ make_lhsv_cmp (is_inv_cmp_int c) hv1 hv2;; - cond_int32u c lhsv None ~> hv - THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) - (m0 : mem) (st : sistate_local), - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompu c)) args m) <> None -> - seval_sval ge sp (hsval_proj hv) rs0 m0 = - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompu c)) args m)). -Proof. - unfold cond_int32u in *; destruct c; - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail). - all: - try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto); - erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; - erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; - simplify_SOME z; unfold Val.cmpu. - - intros; apply xor_neg_ltle_cmpu. - - intros; replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmpu_bool; trivial. - - intros; replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmpu_bool. - rewrite xor_neg_optb; trivial. -Qed. - -Lemma mkimm_single_equal: forall n imm, - make_immed32 n = Imm32_single imm -> - n = imm. -Proof. - intros. unfold make_immed32 in H. - destruct (Int.eq _ _); inv H; auto. -Qed. - -Lemma mkimm_pair_equal: forall n hi lo, - make_immed32 n = Imm32_pair hi lo -> - hi = (Int.shru (Int.sub n (Int.sign_ext 12 n)) (Int.repr 12)) /\ - lo = (Int.sign_ext 12 n). -Proof. - intros. unfold make_immed32 in H. - destruct (Int.eq _ _) in H; try congruence. - inv H. auto. -Qed. - -(* TODO gourdinl Lemma mkimm_pair_lo_zero_equal: forall n hi lo, - make_immed32 n = Imm32_pair hi lo -> - Int.eq n Int.zero = false -> - Int.eq lo Int.zero = true -> - n = Int.shl hi (Int.repr 12). -Proof. - intros. unfold make_immed32 in H. - destruct (Int.eq _ _) in H; try discriminate. - inv H. apply Int.same_if_eq in H1. rewrite H1. - rewrite Int.sub_zero_l. unfold Int.shru, Int.shl. - *) - -Lemma simplify_ccompimm_correct: forall c n r (hst: hsistate_local), - WHEN DO hv1 <~ hsi_sreg_get hst r;; expanse_condimm_int32s c hv1 n ~> hv - THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) - (m0 : mem) (st : sistate_local), - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompimm c n)) args m) <> None -> - seval_sval ge sp (hsval_proj hv) rs0 m0 = - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompimm c n)) args m)). -Proof. - unfold expanse_condimm_int32s, cond_int32s in *; destruct c; - intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl; - unfold loadimm32, sltimm32, xorimm32, opimm32, load_hilo32. - 1,3,5,7,9,11: - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence; - try (simplify_SOME z; contradiction; fail); - try erewrite H9; eauto; try erewrite H8; eauto; - try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto; - try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto; - try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto; - simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction. - 4: rewrite <- xor_neg_ltle_cmp; unfold Val.cmp. - 5: intros; replace (Clt) with (swap_comparison Cgt) by auto; - unfold Val.cmp; rewrite Val.swap_cmp_bool; trivial. - 6: intros; replace (Clt) with (negate_comparison Cge) by auto; - unfold Val.cmp; rewrite Val.negate_cmp_bool; rewrite xor_neg_optb. - 1,2,3,4,5,6: apply Int.same_if_eq in EQIMM; subst; trivial. - all: - specialize make_immed32_sound with n; - destruct (make_immed32 n) eqn:EQMKI; - try destruct (Int.eq n (Int.repr Int.max_signed)) eqn:EQMAX; - try destruct (Int.eq lo Int.zero) eqn:EQLO. - 19,21,22: - specialize make_immed32_sound with (Int.one); - destruct (make_immed32 Int.one) eqn:EQMKI_A1. - 25,26,27: - specialize make_immed32_sound with (Int.add n Int.one); - destruct (make_immed32 (Int.add n Int.one)) eqn:EQMKI_A2. - all: - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail). - all: - try erewrite H12; eauto; try erewrite H11; eauto; - try erewrite H10; eauto; try erewrite H9; eauto; try erewrite H8; eauto; - try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto; - try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto; - try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto; - simplify_SOME z; unfold Val.cmp, zero32; intros; try contradiction. - all: try apply Int.same_if_eq in H1; subst. - all: try apply Int.same_if_eq in EQLO; subst. - all: try apply Int.same_if_eq in EQMAX; subst. - all: try rewrite Int.add_commut, Int.add_zero_l; trivial. - all: try apply xor_ceq_zero; auto. - (* Problème d'implémentation lié au addiwr0 ? - --> On dirait que comme l'instruction n'a pas d'argument une fois expansée, - un cas spécial se produit si l'argument de départ n'est pas un entier : - L'instruction addiwr0 est configurée pour toujours renvoyer Int.one, - mais si le premier argument de la comparaison originelle n'est pas un - Vint, alors on se retrouve avec : - Some (Vint Int.one) = Some (Val.of_optbool None) - <-> Some (Vint Int.zero) = Some (Vundef) - Il faudrait peut-être modifier la sémantique dans Op pour éliminer ce cas. *) - admit. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - { apply cmp_ltle_add_one; auto. } - { apply Int.same_if_eq in H2; subst. - rewrite (Int.add_commut (Int.shl hi (Int.repr 12)) Int.zero) in H. - rewrite Int.add_zero_l in H. rewrite <- H. - apply cmp_ltle_add_one; auto. } - { rewrite <- H. apply cmp_ltle_add_one; auto. } - { rewrite (Int.add_commut (Int.shl hi (Int.repr 12))). rewrite Int.add_zero_l. - apply cmp_ltle_add_one. rewrite Int.add_commut, Int.add_zero_l in EQMAX. - auto. } - { apply Int.same_if_eq in H2; subst. - rewrite (Int.add_commut (Int.shl hi0 (Int.repr 12)) Int.zero) in H. - rewrite Int.add_zero_l in H. rewrite <- H. - rewrite (Int.add_commut (Int.shl hi (Int.repr 12)) Int.zero) in *. - rewrite Int.add_zero_l in *. apply cmp_ltle_add_one; auto. } - { rewrite <- H. - rewrite (Int.add_commut (Int.shl hi (Int.repr 12)) Int.zero) in *. - rewrite Int.add_zero_l in *. apply cmp_ltle_add_one; auto. } - { apply cmp_ltle_add_one; auto. } - { apply Int.same_if_eq in H2; subst. - rewrite (Int.add_commut (Int.shl hi0 (Int.repr 12)) Int.zero) in H. - rewrite Int.add_zero_l in H. rewrite <- H. - apply cmp_ltle_add_one; auto. } - { rewrite <- H. apply cmp_ltle_add_one; auto. } - { intros; replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmp_bool. - rewrite xor_neg_optb; trivial. } - { intros; replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmp_bool. - rewrite xor_neg_optb; trivial. } - { intros; replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmp_bool. - rewrite xor_neg_optb; trivial. } - { intros; replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmp_bool. - rewrite xor_neg_optb; trivial. } - { intros; replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmp_bool. - rewrite xor_neg_optb; trivial. } - { intros; replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmp_bool. - rewrite xor_neg_optb; trivial. } -Admitted. -(*Qed.*) - - -Lemma simplify_ccompl_correct: forall c r r0 (hst: hsistate_local), - WHEN DO hv1 <~ hsi_sreg_get hst r;; - DO hv2 <~ hsi_sreg_get hst r0;; - DO lhsv <~ make_lhsv_cmp (is_inv_cmp_int c) hv1 hv2;; - cond_int64s c lhsv None ~> hv - THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) - (m0 : mem) (st : sistate_local), - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompl c)) args m) <> None -> - seval_sval ge sp (hsval_proj hv) rs0 m0 = - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompl c)) args m)). -Proof. - unfold cond_int64s in *; destruct c; - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail). - all: - try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto); - erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; - erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; - simplify_SOME z; unfold Val.cmpl. - 1,2,3: intros; apply optbool_mktotal. - - intros; apply xor_neg_ltle_cmpl. - - intros; replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmpl_bool; trivial. - apply optbool_mktotal. - - intros; apply xor_neg_ltge_cmpl. -Qed. - -Lemma simplify_ccomplu_correct: forall c r r0 (hst: hsistate_local), - WHEN DO hv1 <~ hsi_sreg_get hst r;; - DO hv2 <~ hsi_sreg_get hst r0;; - DO lhsv <~ make_lhsv_cmp (is_inv_cmp_int c) hv1 hv2;; - cond_int64u c lhsv None ~> hv - THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) - (m0 : mem) (st : sistate_local), - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccomplu c)) args m) <> None -> - seval_sval ge sp (hsval_proj hv) rs0 m0 = - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccomplu c)) args m)). -Proof. - unfold cond_int64u in *; destruct c; - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail). - all: - try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto); - erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; - erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; - simplify_SOME z; unfold Val.cmplu. - 1,2,3: intros; apply optbool_mktotal. - - intros; apply xor_neg_ltle_cmplu. - - intros; replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmplu_bool; trivial. - apply optbool_mktotal. - - intros; apply xor_neg_ltge_cmplu. -Qed. - - - -Lemma simplify_ccompf_correct: forall c r r0 (hst: hsistate_local), - WHEN DO hv1 <~ hsi_sreg_get hst r;; - DO hv2 <~ hsi_sreg_get hst r0;; - DO lhsv <~ make_lhsv_cmp (is_inv_cmp_float c) hv1 hv2;; - expanse_cond_fp false cond_float c lhsv ~> hv - THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) - (m0 : mem) (st : sistate_local), - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompf c)) args m) <> None -> - seval_sval ge sp (hsval_proj hv) rs0 m0 = - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompf c)) args m)). -Proof. - unfold expanse_cond_fp in *; destruct c; - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail). - all: - try (erewrite H9; eauto; erewrite H8; eauto); - try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto); - erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; - erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; - simplify_SOME z; unfold Val.cmpf. - - intros; apply xor_neg_eqne_cmpf. - - intros; replace (Clt) with (swap_comparison Cgt) by auto; - rewrite swap_cmpf_bool; trivial. - - intros; replace (Cle) with (swap_comparison Cge) by auto; - rewrite swap_cmpf_bool; trivial. -Qed. - -Lemma simplify_cnotcompf_correct: forall c r r0 (hst: hsistate_local), - WHEN DO hv1 <~ hsi_sreg_get hst r;; - DO hv2 <~ hsi_sreg_get hst r0;; - DO lhsv <~ make_lhsv_cmp (is_inv_cmp_float c) hv1 hv2;; - expanse_cond_fp true cond_float c lhsv ~> hv - THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) - (m0 : mem) (st : sistate_local), - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Cnotcompf c)) args m) <> None -> - seval_sval ge sp (hsval_proj hv) rs0 m0 = - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Cnotcompf c)) args m)). -Proof. - unfold expanse_cond_fp in *; destruct c; - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail). - all: - try (erewrite H9; eauto; erewrite H8; eauto); - try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto); - erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; - erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; - simplify_SOME z; unfold Val.cmpf. - all: intros; apply f_equal; - try destruct z0, z2; try destruct z2, z4; - try destruct z8, z10; - simpl; trivial. - 2: rewrite Float.cmp_ne_eq; rewrite negb_involutive; trivial. - 4: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float.cmp_swap; simpl. - 5: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float.cmp_swap; simpl. - all: destruct (Float.cmp _ _ _); trivial. -Qed. - -Lemma simplify_ccompfs_correct: forall c r r0 (hst: hsistate_local), - WHEN DO hv1 <~ hsi_sreg_get hst r;; - DO hv2 <~ hsi_sreg_get hst r0;; - DO lhsv <~ make_lhsv_cmp (is_inv_cmp_float c) hv1 hv2;; - expanse_cond_fp false cond_single c lhsv ~> hv - THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) - (m0 : mem) (st : sistate_local), - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompfs c)) args m) <> None -> - seval_sval ge sp (hsval_proj hv) rs0 m0 = - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompfs c)) args m)). -Proof. - unfold expanse_cond_fp in *; destruct c; - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail). - all: - try (erewrite H9; eauto; erewrite H8; eauto); - try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto); - erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; - erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; - simplify_SOME z; unfold Val.cmpfs. - - intros; apply xor_neg_eqne_cmpfs. - - intros; replace (Clt) with (swap_comparison Cgt) by auto; - rewrite swap_cmpfs_bool; trivial. - - intros; replace (Cle) with (swap_comparison Cge) by auto; - rewrite swap_cmpfs_bool; trivial. -Qed. - -Lemma simplify_cnotcompfs_correct: forall c r r0 (hst: hsistate_local), - WHEN DO hv1 <~ hsi_sreg_get hst r;; - DO hv2 <~ hsi_sreg_get hst r0;; - DO lhsv <~ make_lhsv_cmp (is_inv_cmp_float c) hv1 hv2;; - expanse_cond_fp true cond_single c lhsv ~> hv - THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) - (m0 : mem) (st : sistate_local), - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Cnotcompfs c)) args m) <> None -> - seval_sval ge sp (hsval_proj hv) rs0 m0 = - (SOME args <- - seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 - m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Cnotcompfs c)) args m)). -Proof. - unfold expanse_cond_fp in *; destruct c; - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail). - all: - try (erewrite H9; eauto; erewrite H8; eauto); - try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto); - erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; - erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; - simplify_SOME z; unfold Val.cmpfs. - all: intros; apply f_equal; - try destruct z0, z2; try destruct z2, z4; - try destruct z8, z10; - simpl; trivial. - 2: rewrite Float32.cmp_ne_eq; rewrite negb_involutive; trivial. - 4: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl. - 5: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl. - all: destruct (Float32.cmp _ _ _); trivial. - Qed.*) - Lemma simplify_correct rsv lr hst: WHEN simplify rsv lr hst ~> hv THEN forall ge sp rs0 m0 st (REF: hsilocal_refines ge sp rs0 m0 hst st) @@ -1443,8 +699,7 @@ Proof. destruct (eval_addressing _ _ _ _) as [a|] eqn: Ha; try congruence. destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. destruct (Mem.loadv _ _ _); try congruence. -(*Qed.*) -Admitted. +Qed. Global Opaque simplify. Local Hint Resolve simplify_correct: wlp. @@ -1544,7 +799,7 @@ Proof. rewrite <- X, sok_local_set_sreg. intuition eauto. - destruct REF; intuition eauto. - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto. - Qed. + Qed. Global Opaque hslocal_set_sreg. Local Hint Resolve hslocal_set_sreg_correct: wlp. @@ -1557,45 +812,7 @@ Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) : 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 => CEbequw optR0 - | Cne => CEbneuw 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 => CEbequl optR0 - | Cne => CEbneul optR0 - | Clt => CEbltul optR0 - | Cle => CEbgeul optR0 - | Cgt => CEbltul optR0 - | 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 @@ -1605,132 +822,12 @@ Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : ?? ( 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) := - 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_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) - | (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) - | (Ccompimm c n), (a1 :: nil) => - let is_inv := is_inv_cmp_int c in - DO hv1 <~ hsi_sreg_get prev a1;; - (if Int.eq n Int.zero then - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;; - let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in - RET (cond, lhsv) - else - DO hvs <~ loadimm32 n;; - DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;; - let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in - RET (cond, lhsv)) - | (Ccompuimm c n), (a1 :: nil) => - let is_inv := is_inv_cmp_int c in - DO hv1 <~ hsi_sreg_get prev a1;; - (if Int.eq n Int.zero then - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;; - let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in - RET (cond, lhsv) - else - DO hvs <~ loadimm32 n;; - DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;; - let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in - RET (cond, lhsv)) - | (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) - | (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) - | (Ccomplimm c n), (a1 :: nil) => - let is_inv := is_inv_cmp_int c in - DO hv1 <~ hsi_sreg_get prev a1;; - (if Int64.eq n Int64.zero then - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;; - let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in - RET (cond, lhsv) - else - DO hvs <~ loadimm64 n;; - DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;; - let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in - RET (cond, lhsv)) - | (Ccompluimm c n), (a1 :: nil) => - let is_inv := is_inv_cmp_int c in - DO hv1 <~ hsi_sreg_get prev a1;; - (if Int64.eq n Int64.zero then - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;; - let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in - RET (cond, lhsv) - else - DO hvs <~ loadimm64 n;; - DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;; - let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in - RET (cond, lhsv)) - | (Ccompf c), (f1 :: f2 :: nil) => - DO hv1 <~ hsi_sreg_get prev f1;; - DO hv2 <~ hsi_sreg_get prev f2;; - let is_inv := is_inv_cmp_float c in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - expanse_cbranch_fp false cond_float c lhsv - | (Cnotcompf c), (f1 :: f2 :: nil) => - DO hv1 <~ hsi_sreg_get prev f1;; - DO hv2 <~ hsi_sreg_get prev f2;; - let is_inv := is_inv_cmp_float c in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - expanse_cbranch_fp true cond_float c lhsv - | (Ccompfs c), (f1 :: f2 :: nil) => - DO hv1 <~ hsi_sreg_get prev f1;; - DO hv2 <~ hsi_sreg_get prev f2;; - let is_inv := is_inv_cmp_float c in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - expanse_cbranch_fp false cond_single c lhsv - | (Cnotcompfs c), (f1 :: f2 :: nil) => - DO hv1 <~ hsi_sreg_get prev f1;; - DO hv2 <~ hsi_sreg_get prev f2;; - let is_inv := is_inv_cmp_float c in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - expanse_cbranch_fp true cond_single c lhsv - | _, _ => - DO vargs <~ hlist_args prev args;; - RET (cond, vargs) - end.*) + *) (** ** Execution of one instruction *) - -(* TODO: This function could be defined in a specific file for each target *) -Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) := - None. - -Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall - (TARGET: target_cbranch_expanse hst c l = Some (c', l')) - (LREF : hsilocal_refines ge sp rs0 m0 hst st) - (OK: hsok_local ge sp rs0 m0 hst), - 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. -Proof. - unfold target_cbranch_expanse; simpl; intros; try congruence. -Qed. -Global Opaque target_cbranch_expanse. - Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg): ?? (condition * list_hsval) := - match target_cbranch_expanse prev cond args with + match target_cbranch_expanse prev cond args with | Some (cond', vargs) => DO vargs' <~ fsval_list_proj vargs;; RET (cond', vargs) @@ -1855,7 +952,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. Admitted. (* +Proof. destruct i; simpl; try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail). - (* refines_dyn Iop *) @@ -1871,66 +968,19 @@ Proof. Admitted. (* eapply hsist_set_local_correct_dyn; eauto. unfold sok_local; simpl; intuition. - (* refines_stat Icond *) - unfold cbranch_expanse; destruct c eqn:EQC; - try apply hsiexec_cond_noexp. - + repeat (destruct l; try apply hsiexec_cond_noexp). - wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. - * unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition. - constructor; simpl; eauto. - constructor. - * destruct REF as (EXREF & LREF & NEST). - split. - -- do 2 (constructor; simpl; auto). - intros; erewrite seval_condition_refines; eauto. - destruct c0; simpl; unfold seval_condition; - erewrite H3; eauto; erewrite H2; eauto; - erewrite H1; eauto; erewrite H0; eauto; - erewrite H; eauto; simplify_SOME z. - all: intros; destruct z0, z2; auto. - -- split; simpl; auto. - destruct NEST as [|st0 se lse TOP NEST]; - econstructor; simpl; auto; constructor; auto. - + admit. - + repeat (destruct l; try apply hsiexec_cond_noexp). - destruct (Int.eq _ _) eqn:EQIMM; simpl. - 1: admit. - - unfold loadimm32; destruct make_immed32 eqn:EQMKI. - { - wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. - * unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition. - constructor; simpl; eauto. - constructor. - * destruct REF as (EXREF & LREF & NEST). - split. - -- do 2 (constructor; simpl; auto). - intros; erewrite seval_condition_refines; eauto. - destruct c0; simpl; unfold seval_condition. - - { simpl in *. apply mkimm_single_equal in EQMKI; subst. - destruct (seval_smem _ _ _ _ _) eqn:EQSM; try congruence. - - erewrite H4; eauto; erewrite H3; eauto; - erewrite H2; eauto; erewrite H1; eauto; - try erewrite H0; eauto; try erewrite H; eauto; - simplify_SOME z. rewrite Int.add_zero. trivial. - - simplify_SOME x. - } - 2: { - generalize (sok_local_set_sreg_simp (Rop (OEaddiwr0 imm))); simpl; eauto. - intros.j - apply hsilocal_refines_smem_refines in LREF; auto. - - rewrite <- LREF. auto. - 2: { eauto. - all: intros; destruct z0, z2; auto. - -- split; simpl; auto. - destruct NEST as [|st0 se lse TOP NEST]; - econstructor; simpl; auto; constructor; auto. - - + admit. - + admit. - *) -(*Qed.*) + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. + + unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition. + constructor; simpl; eauto. + constructor. + + destruct REF as (EXREF & LREF & NEST). + split. + * constructor; simpl; auto. + constructor; simpl; auto. + intros; erewrite seval_condition_refines; eauto. + * split; simpl; auto. + destruct NEST as [|st0 se lse TOP NEST]; + econstructor; simpl; auto; constructor; auto. +Qed. Global Opaque hsiexec_inst. Local Hint Resolve hsiexec_inst_correct: wlp. |