diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-01 09:27:39 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-01 09:27:39 +0100 |
commit | 80db8e4b9a2321f0b102e97b70181fe368a077b4 (patch) | |
tree | f3b7482705c5c0ad1225459938b8589dd408e11f /riscV | |
parent | 8fb2a5a165ecd48b2df76b9beff7a83cc14b5e6c (diff) | |
download | compcert-kvx-80db8e4b9a2321f0b102e97b70181fe368a077b4.tar.gz compcert-kvx-80db8e4b9a2321f0b102e97b70181fe368a077b4.zip |
Proof of fsval condition cmp ok
Diffstat (limited to 'riscV')
-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 |
8 files changed, 527 insertions, 170 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. |