diff options
| -rw-r--r-- | riscV/Asmgen.v | 32 | ||||
| -rw-r--r-- | riscV/Asmgenproof.v | 8 | ||||
| -rw-r--r-- | riscV/Asmgenproof1.v | 69 | ||||
| -rw-r--r-- | riscV/ExpansionOracle.ml | 18 | ||||
| -rw-r--r-- | riscV/NeedOp.v | 4 | ||||
| -rw-r--r-- | riscV/Op.v | 124 | ||||
| -rw-r--r-- | riscV/OpWeights.ml | 4 | ||||
| -rw-r--r-- | riscV/ValueAOp.v | 50 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 375 |
9 files changed, 568 insertions, 116 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index d826f139..d0c826a3 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -281,6 +281,12 @@ Definition transl_cbranch | CEbnew optR0, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (apply_bin_r0_r0r0lbl optR0 Pbnew r1 r2 lbl :: k) + | CEbequw optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k) + | CEbneuw optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbnew r1 r2 lbl :: k) | CEbltw optR0, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (apply_bin_r0_r0r0lbl optR0 Pbltw r1 r2 lbl :: k) @@ -299,6 +305,12 @@ Definition transl_cbranch | CEbnel optR0, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (apply_bin_r0_r0r0lbl optR0 Pbnel r1 r2 lbl :: k) + | CEbequl optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbeql r1 r2 lbl :: k) + | CEbneul optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbnel r1 r2 lbl :: k) | CEbltl optR0, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (apply_bin_r0_r0r0lbl optR0 Pbltl r1 r2 lbl :: k) @@ -768,6 +780,16 @@ Definition transl_op do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (apply_bin_r0_r0r0 optR0 (Psnew rd) rs1 rs2 :: k) + | OEsequw optR0, a1 :: a2 :: nil => + do rd <- ireg_of res; + do rs1 <- ireg_of a1; + do rs2 <- ireg_of a2; + OK (apply_bin_r0_r0r0 optR0 (Pseqw rd) rs1 rs2 :: k) + | OEsneuw optR0, a1 :: a2 :: nil => + do rd <- ireg_of res; + do rs1 <- ireg_of a1; + do rs2 <- ireg_of a2; + OK (apply_bin_r0_r0r0 optR0 (Psnew rd) rs1 rs2 :: k) | OEsltw optR0, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; @@ -806,6 +828,16 @@ Definition transl_op do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (apply_bin_r0_r0r0 optR0 (Psnel rd) rs1 rs2 :: k) + | OEsequl optR0, a1 :: a2 :: nil => + do rd <- ireg_of res; + do rs1 <- ireg_of a1; + do rs2 <- ireg_of a2; + OK (apply_bin_r0_r0r0 optR0 (Pseql rd) rs1 rs2 :: k) + | OEsneul optR0, a1 :: a2 :: nil => + do rd <- ireg_of res; + do rs1 <- ireg_of a1; + do rs2 <- ireg_of a2; + OK (apply_bin_r0_r0r0 optR0 (Psnel rd) rs1 rs2 :: k) | OEsltl optR0, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 47ee39f0..82c1917d 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -224,6 +224,10 @@ Proof. - destruct optR0 as [[]|]; TailNoLabel. - destruct optR0 as [[]|]; TailNoLabel. - destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. Qed. Remark transl_cond_op_label: @@ -312,6 +316,10 @@ Opaque Int.eq. - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. +- destruct optR0 as [[]|]; simpl; TailNoLabel. +- destruct optR0 as [[]|]; simpl; TailNoLabel. +- destruct optR0 as [[]|]; simpl; TailNoLabel. +- destruct optR0 as [[]|]; simpl; TailNoLabel. Qed. Remark indexed_memory_access_label: diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 57d281ec..0b1abe2a 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -497,6 +497,36 @@ Proof. - destruct optR0 as [[]|]; unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; auto; + simpl in *. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int.eq Int.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int.eq i Int.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: (Int.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; auto; + simpl in *. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int.eq Int.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int.eq i Int.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: negb (Int.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR0 as [[]|]; @@ -528,6 +558,36 @@ Proof. unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; unfold zero64, Op.zero64 in *; eexists; eexists; eauto; split; constructor; + simpl in *; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int64.eq Int64.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int64.eq i Int64.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: (Int64.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: negb (Int64.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR0 as [[]|]; unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; @@ -1198,13 +1258,15 @@ 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 *) - 5: econstructor; split; try apply exec_straight_one; simpl; eauto; + 7: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; rewrite Int.add_commut; auto. - 9: econstructor; split; try apply exec_straight_one; simpl; eauto; + 13: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; rewrite Int64.add_commut; auto. all: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0; econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl. + all: destruct (rs x0); auto. + all: destruct (rs x1); auto. Qed. (** Memory accesses *) @@ -1512,6 +1574,3 @@ Proof. Qed. End CONSTRUCTORS. - - - diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index dc7f4b82..fa05d318 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -118,8 +118,8 @@ let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k = let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Ceq -> Icond (CEbequw optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbneuw optR0, [ a1; a2 ], succ1, succ2, info) :: k | Clt -> Icond (CEbltuw optR0, [ a1; a2 ], succ1, succ2, info) :: k | Cle -> Icond (CEbgeuw optR0, [ a2; a1 ], succ1, succ2, info) :: k | Cgt -> Icond (CEbltuw optR0, [ a2; a1 ], succ1, succ2, info) :: k @@ -138,8 +138,8 @@ let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k = let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Ceq -> Icond (CEbequl optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbneul optR0, [ a1; a2 ], succ1, succ2, info) :: k | Clt -> Icond (CEbltul optR0, [ a1; a2 ], succ1, succ2, info) :: k | Cle -> Icond (CEbgeul optR0, [ a2; a1 ], succ1, succ2, info) :: k | Cgt -> Icond (CEbltul optR0, [ a2; a1 ], succ1, succ2, info) :: k @@ -164,8 +164,8 @@ let cond_int32s is_x0 cmp a1 a2 dest succ k = let cond_int32u is_x0 cmp a1 a2 dest succ k = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k + | Ceq -> Iop (OEsequw optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) :: k | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k | Cle -> Iop (OEsltuw optR0, [ a2; a1 ], dest, n2pi ()) @@ -196,8 +196,8 @@ let cond_int64s is_x0 cmp a1 a2 dest succ k = let cond_int64u is_x0 cmp a1 a2 dest succ k = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k + | Ceq -> Iop (OEsequl optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsneul optR0, [ a1; a2 ], dest, succ) :: k | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k | Cle -> Iop (OEsltul optR0, [ a2; a1 ], dest, n2pi ()) @@ -327,7 +327,7 @@ let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k = insn :: (if normal' then Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info) - else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) + else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) (* TODO Maybe incorrect *) :: k let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index db8b68ef..a0ec7732 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -89,6 +89,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ocmp c => needs_of_condition c | OEseqw _ => op2 (default nv) | OEsnew _ => op2 (default nv) + | OEsequw _ => op2 (default nv) + | OEsneuw _ => op2 (default nv) | OEsltw _ => op2 (default nv) | OEsltuw _ => op2 (default nv) | OEsltiw n => op1 (default nv) @@ -98,6 +100,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEaddiwr0 n => op1 (modarith nv) | 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) @@ -51,14 +51,18 @@ Inductive condition : Type := | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) | Cnotcompfs (c: comparison) (**r negation of a floating-point comparison *) (* Expansed branches *) - | CEbeqw (optR0: option bool) (**r branch-if-equal *) + | CEbeqw (optR0: option bool) (**r branch-if-equal signed *) | CEbnew (optR0: option bool) (**r branch-if-not-equal signed *) + | CEbequw (optR0: option bool) (**r branch-if-equal unsigned *) + | CEbneuw (optR0: option bool) (**r branch-if-not-equal unsigned *) | CEbltw (optR0: option bool) (**r branch-if-less signed *) | CEbltuw (optR0: option bool) (**r branch-if-less unsigned *) | CEbgew (optR0: option bool) (**r branch-if-greater-or-equal signed *) | CEbgeuw (optR0: option bool) (**r branch-if-greater-or-equal unsigned *) - | CEbeql (optR0: option bool) (**r branch-if-equal *) + | CEbeql (optR0: option bool) (**r branch-if-equal signed *) | CEbnel (optR0: option bool) (**r branch-if-not-equal signed *) + | CEbequl (optR0: option bool) (**r branch-if-equal unsigned *) + | CEbneul (optR0: option bool) (**r branch-if-not-equal unsigned *) | CEbltl (optR0: option bool) (**r branch-if-less signed *) | CEbltul (optR0: option bool) (**r branch-if-less unsigned *) | CEbgel (optR0: option bool) (**r branch-if-greater-or-equal signed *) @@ -167,8 +171,10 @@ Inductive operation : Type := (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) (* Expansed conditions *) - | OEseqw (optR0: option bool) (**r [rd <- rs1 == rs2] (pseudo) *) - | OEsnew (optR0: option bool) (**r [rd <- rs1 != rs2] (pseudo) *) + | 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 *) | 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 *) @@ -176,8 +182,10 @@ Inductive operation : Type := | OExoriw (n: int) (**r xor immediate *) | OEluiw (n: int) (**r load upper-immediate *) | OEaddiwr0 (n: int) (**r add immediate *) - | OEseql (optR0: option bool) (**r [rd <- rs1 == rs2] (pseudo) *) - | OEsnel (optR0: option bool) (**r [rd <- rs1 != rs2] (pseudo) *) + | 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 *) | 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 *) @@ -270,14 +278,18 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) (* Expansed branches *) - | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 - | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 + | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cne) v1 v2 zero32 + | CEbequw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 + | CEbneuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Clt) v1 v2 zero32 | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cge) v1 v2 zero32 | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 - | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 - | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 + | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 + | CEbneul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Clt) v1 v2 zero64 | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cge) v1 v2 zero64 @@ -383,8 +395,10 @@ Definition eval_operation | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1)) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) (* Expansed conditions *) - | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) - | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) + | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Ceq) v1 v2 zero32) + | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Cne) v1 v2 zero32) + | OEsequw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) + | OEsneuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) | OEsltw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Clt) v1 v2 zero32) | OEsltuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32) | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n)) @@ -392,8 +406,10 @@ Definition eval_operation | 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) - | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) - | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64)) + | 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)) + | OEsneul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64)) | OEsltl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Clt) v1 v2 zero64)) | OEsltul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64)) | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n))) @@ -469,12 +485,16 @@ Definition type_of_condition (c: condition) : list typ := | Cnotcompfs _ => Tsingle :: Tsingle :: nil | CEbeqw _ => Tint :: Tint :: nil | CEbnew _ => Tint :: Tint :: nil + | CEbequw _ => Tint :: Tint :: nil + | CEbneuw _ => Tint :: Tint :: nil | CEbltw _ => Tint :: Tint :: nil | CEbltuw _ => Tint :: Tint :: nil | CEbgew _ => Tint :: Tint :: nil | CEbgeuw _ => Tint :: Tint :: nil | CEbeql _ => Tlong :: Tlong :: nil | CEbnel _ => Tlong :: Tlong :: nil + | CEbequl _ => Tlong :: Tlong :: nil + | CEbneul _ => Tlong :: Tlong :: nil | CEbltl _ => Tlong :: Tlong :: nil | CEbltul _ => Tlong :: Tlong :: nil | CEbgel _ => Tlong :: Tlong :: nil @@ -578,6 +598,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ocmp c => (type_of_condition c, Tint) | OEseqw _ => (Tint :: Tint :: nil, Tint) | OEsnew _ => (Tint :: Tint :: nil, Tint) + | OEsequw _ => (Tint :: Tint :: nil, Tint) + | OEsneuw _ => (Tint :: Tint :: nil, Tint) | OEsltw _ => (Tint :: Tint :: nil, Tint) | OEsltuw _ => (Tint :: Tint :: nil, Tint) | OEsltiw _ => (Tint :: nil, Tint) @@ -587,6 +609,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEaddiwr0 _ => (nil, Tint) | OEseql _ => (Tlong :: Tlong :: nil, Tint) | OEsnel _ => (Tlong :: Tlong :: nil, Tint) + | OEsequl _ => (Tlong :: Tlong :: nil, Tint) + | OEsneul _ => (Tlong :: Tlong :: nil, Tint) | OEsltl _ => (Tlong :: Tlong :: nil, Tint) | OEsltul _ => (Tlong :: Tlong :: nil, Tint) | OEsltil _ => (Tlong :: nil, Tint) @@ -808,9 +832,15 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* cmp *) - destruct (eval_condition cond vl m)... destruct b... (* OEseqw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + destruct Val.cmp_bool... all: destruct b... + (* OEsnew *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + destruct Val.cmp_bool... all: destruct b... + (* OEsequw *) - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; destruct Val.cmpu_bool... all: destruct b... - (* OEsnew *) + (* OEsneuw *) - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; destruct Val.cmpu_bool... all: destruct b... (* OEsltw *) @@ -831,9 +861,15 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEaddiwr0 *) - trivial. (* OEseql *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + destruct Val.cmpl_bool... all: destruct b... + (* OEsnel *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + destruct Val.cmpl_bool... all: destruct b... + (* OEsequl *) - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; destruct Val.cmplu_bool... all: destruct b... - (* OEsnel *) + (* OEsneul *) - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; destruct Val.cmplu_bool... all: destruct b... (* OEsltl *) @@ -944,12 +980,16 @@ Definition negate_condition (cond: condition): condition := | Cnotcompfs c => Ccompfs c | CEbeqw optR0 => CEbnew optR0 | CEbnew optR0 => CEbeqw optR0 + | CEbequw optR0 => CEbneuw optR0 + | CEbneuw optR0 => CEbequw optR0 | CEbltw optR0 => CEbgew optR0 | CEbltuw optR0 => CEbgeuw optR0 | CEbgew optR0 => CEbltw optR0 | CEbgeuw optR0 => CEbltuw optR0 | CEbeql optR0 => CEbnel optR0 | CEbnel optR0 => CEbeql optR0 + | CEbequl optR0 => CEbneul optR0 + | CEbneul optR0 => CEbequl optR0 | CEbltl optR0 => CEbgel optR0 | CEbltul optR0 => CEbgeul optR0 | CEbgel optR0 => CEbltl optR0 @@ -975,6 +1015,10 @@ Proof. repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto. repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; apply Val.negate_cmpu_bool. repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; apply Val.negate_cmpu_bool. @@ -987,6 +1031,10 @@ Proof. repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; apply Val.negate_cmpu_bool. repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; apply Val.negate_cmplu_bool. repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; apply Val.negate_cmplu_bool. @@ -1094,12 +1142,12 @@ Definition cond_depends_on_memory (cond : condition) : bool := | Ccompuimm _ _ => negb Archi.ptr64 | Ccomplu _ => Archi.ptr64 | Ccompluimm _ _ => Archi.ptr64 - | CEbeqw _ => negb Archi.ptr64 - | CEbnew _ => negb Archi.ptr64 + | CEbequw _ => negb Archi.ptr64 + | CEbneuw _ => negb Archi.ptr64 | CEbltuw _ => negb Archi.ptr64 | CEbgeuw _ => negb Archi.ptr64 - | CEbeql _ => Archi.ptr64 - | CEbnel _ => Archi.ptr64 + | CEbequl _ => Archi.ptr64 + | CEbneul _ => Archi.ptr64 | CEbltul _ => Archi.ptr64 | CEbgeul _ => Archi.ptr64 | _ => false @@ -1108,12 +1156,12 @@ Definition cond_depends_on_memory (cond : condition) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with | Ocmp cmp => cond_depends_on_memory cmp - | OEseqw _ => negb Archi.ptr64 - | OEsnew _ => negb Archi.ptr64 + | OEsequw _ => negb Archi.ptr64 + | OEsneuw _ => negb Archi.ptr64 | OEsltiuw _ => negb Archi.ptr64 | OEsltuw _ => negb Archi.ptr64 - | OEseql _ => Archi.ptr64 - | OEsnel _ => Archi.ptr64 + | OEsequl _ => Archi.ptr64 + | OEsneul _ => Archi.ptr64 | OEsltul _ => Archi.ptr64 | OEsltiul _ => Archi.ptr64 | _ => false @@ -1380,6 +1428,10 @@ Proof. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. - destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; eapply eval_cmpu_bool_inj'; eauto. - destruct optR0 as [[]|]; unfold apply_bin_r0 in *; eapply eval_cmpu_bool_inj'; eauto. @@ -1392,6 +1444,10 @@ Proof. - destruct optR0 as [[]|]; unfold apply_bin_r0 in *; eapply eval_cmpu_bool_inj'; eauto. - destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; eapply eval_cmplu_bool_inj'; eauto. - destruct optR0 as [[]|]; unfold apply_bin_r0 in *; eapply eval_cmplu_bool_inj'; eauto. @@ -1612,8 +1668,16 @@ Proof. destruct b; simpl; constructor. simpl; constructor. (* OEseqw *) - - apply eval_cmpu_bool_inj_opt; auto. + - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. (* OEsnew *) + - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsequw *) + - apply eval_cmpu_bool_inj_opt; auto. + (* OEsneuw *) - apply eval_cmpu_bool_inj_opt; auto. (* OEsltw *) - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; @@ -1628,8 +1692,16 @@ Proof. (* OExoriw *) - inv H4; simpl; auto. (* OEseql *) - - apply eval_cmplu_bool_inj_opt; auto. + - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. (* OEsnel *) + - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsequl *) + - apply eval_cmplu_bool_inj_opt; auto. + (* OEsneul *) - apply eval_cmplu_bool_inj_opt; auto. (* OEsltl *) - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml index 5ac318c8..35ae81e6 100644 --- a/riscV/OpWeights.ml +++ b/riscV/OpWeights.ml @@ -59,12 +59,16 @@ module Rocket = | Ccompluimm _ | CEbeqw _ | CEbnew _ + | CEbequw _ + | CEbneuw _ | CEbltw _ | CEbltuw _ | CEbgew _ | CEbgeuw _ | CEbeql _ | CEbnel _ + | CEbequl _ + | CEbneul _ | CEbltl _ | CEbltul _ | CEbgel _ diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index ece28eff..581229c6 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -41,14 +41,18 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) - | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32 - | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32 + | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32 + | CEbequw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32 + | CEbneuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32 | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32 | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32 | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cge) v1 v2 zero32 | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cge) v1 v2 zero32 - | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64 - | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64 + | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64 + | CEbneul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64 | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64 | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64 | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cge) v1 v2 zero64 @@ -159,8 +163,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) - | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32) - | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32) + | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32) + | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32) + | OEsequw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32) + | OEsneuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32) | OEsltw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32) | OEsltuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32) | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) @@ -168,8 +174,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | 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 - | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64) - | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64) + | 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) + | OEsneul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64) | OEsltl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64) | OEsltul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) @@ -206,7 +214,7 @@ Proof. destruct cond; simpl; eauto with va. inv H2. destruct cond; simpl; eauto with va. - 13: destruct cond; simpl; eauto with va. + 17: destruct cond; simpl; eauto with va. all: destruct optR0 as [[]|]; unfold apply_bin_r0, Op.apply_bin_r0; unfold zero32, Op.zero32, zero64, Op.zero64; eauto with va. Qed. @@ -291,23 +299,23 @@ Proof. apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va. Qed. -Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0, +Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0 cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_r0 optR0 (Val.cmp Clt) a1 a0 Op.zero32) - (of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) b1 b0 zero32)). + vmatch bc (Op.apply_bin_r0 optR0 (Val.cmp cmp) a1 a0 Op.zero32) + (of_optbool (apply_bin_r0 optR0 (cmp_bool cmp) b1 b0 zero32)). Proof. intros. destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va. Qed. -Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0, +Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0 cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc - (Val.maketotal (Op.apply_bin_r0 optR0 (Val.cmpl Clt) a1 a0 Op.zero64)) - (of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) b1 b0 zero64)). + (Val.maketotal (Op.apply_bin_r0 optR0 (Val.cmpl cmp) a1 a0 Op.zero64)) + (of_optbool (apply_bin_r0 optR0 (cmpl_bool cmp) b1 b0 zero64)). Proof. intros. destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; @@ -327,16 +335,16 @@ Proof. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. - 1,2,4: apply eval_cmpu_sound; auto. - apply eval_cmp_sound; auto. + 3,4,6: apply eval_cmpu_sound; auto. + 1,2,3: apply eval_cmp_sound; auto. 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,4: apply eval_cmplu_sound; auto. - apply eval_cmpl_sound; auto. + unfold zero32; simpl; eauto with va. + 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. unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. - unfold zero64; simpl. eauto with va. + unfold zero64; simpl; eauto with va. all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 509697de..7a90fd3a 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -687,7 +687,7 @@ Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) | Ceq => hSop (OEseqw optR0) lhsv | Cne => hSop (OEsnew optR0) lhsv | Clt | Cgt => hSop (OEsltw optR0) lhsv - | Cle | Cge=> + | Cle | Cge => DO hvs <~ (hSop (OEsltw optR0) lhsv);; DO hl <~ make_lhsv_single hvs;; hSop (OExoriw Int.one) hl @@ -695,10 +695,10 @@ Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := match cmp with - | Ceq => hSop (OEseqw optR0) lhsv - | Cne => hSop (OEsnew optR0) lhsv + | Ceq => hSop (OEsequw optR0) lhsv + | Cne => hSop (OEsneuw optR0) lhsv | Clt | Cgt => hSop (OEsltuw optR0) lhsv - | Cle | Cge=> + | Cle | Cge => DO hvs <~ (hSop (OEsltuw optR0) lhsv);; DO hl <~ make_lhsv_single hvs;; hSop (OExoriw Int.one) hl @@ -717,8 +717,8 @@ Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := match cmp with - | Ceq => hSop (OEseql optR0) lhsv - | Cne => hSop (OEsnel optR0) lhsv + | Ceq => hSop (OEsequl optR0) lhsv + | Cne => hSop (OEsneul optR0) lhsv | Clt | Cgt => hSop (OEsltul optR0) lhsv | Cle | Cge => DO hvs <~ (hSop (OEsltul optR0) lhsv);; @@ -778,78 +778,270 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) := (** simplify a symbolic value before assignment to a register *) Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval := match rsv with - | Rop op => - (*match is_move_operation op lr with*) - (*| Some arg => hsi_sreg_get hst arg [>* optimization of Omove <]*) - (*| None =>*) - (*DO lhsv <~ hlist_args hst lr;;*) - (*hSop op lhsv*) - (*end;;*) - match op, lr with - | Ocmp (Ccomp c), a1 :: a2 :: nil => + | Rop (Omove as op) => + match is_move_operation op lr with + | Some arg => hsi_sreg_get hst arg (* optimization of Omove *) + | None => + DO lhsv <~ hlist_args hst lr;; + hSop op lhsv + end + | Rop ((Ocmp cond) as op) => + match cond, lr with + | (Ccomp c), a1 :: a2 :: nil => DO hv1 <~ hsi_sreg_get hst a1;; DO hv2 <~ hsi_sreg_get hst a2;; let is_inv := is_inv_cmp_int c in let optR0 := make_optR0 false is_inv in DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; cond_int32s c lhsv optR0 - | Ocmp (Ccompu c), a1 :: a2 :: nil => + | (Ccompu c), a1 :: a2 :: nil => DO hv1 <~ hsi_sreg_get hst a1;; DO hv2 <~ hsi_sreg_get hst a2;; let is_inv := is_inv_cmp_int c in let optR0 := make_optR0 false is_inv in DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; cond_int32u c lhsv optR0 - | Ocmp (Ccompl c), a1 :: a2 :: nil => + | (Ccompl c), a1 :: a2 :: nil => DO hv1 <~ hsi_sreg_get hst a1;; DO hv2 <~ hsi_sreg_get hst a2;; let is_inv := is_inv_cmp_int c in let optR0 := make_optR0 false is_inv in DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; cond_int64s c lhsv optR0 - | Ocmp (Ccomplu c), a1 :: a2 :: nil => + | (Ccomplu c), a1 :: a2 :: nil => DO hv1 <~ hsi_sreg_get hst a1;; DO hv2 <~ hsi_sreg_get hst a2;; let is_inv := is_inv_cmp_int c in let optR0 := make_optR0 false is_inv in DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; cond_int64u c lhsv optR0 - | Ocmp (Ccompf c), f1 :: f2 :: nil => + | (Ccompf c), f1 :: f2 :: nil => DO hv1 <~ hsi_sreg_get hst f1;; DO hv2 <~ hsi_sreg_get hst f2;; let is_inv := is_inv_cmp_float c in DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; expanse_cond_fp false cond_float c lhsv - | Ocmp (Cnotcompf c), f1 :: f2 :: nil => + | (Cnotcompf c), f1 :: f2 :: nil => DO hv1 <~ hsi_sreg_get hst f1;; DO hv2 <~ hsi_sreg_get hst f2;; let is_inv := is_inv_cmp_float c in DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; expanse_cond_fp true cond_float c lhsv - | Ocmp (Ccompfs c), f1 :: f2 :: nil => + | (Ccompfs c), f1 :: f2 :: nil => DO hv1 <~ hsi_sreg_get hst f1;; DO hv2 <~ hsi_sreg_get hst f2;; let is_inv := is_inv_cmp_float c in DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; expanse_cond_fp false cond_single c lhsv - | Ocmp (Cnotcompfs c), f1 :: f2 :: nil => + | (Cnotcompfs c), f1 :: f2 :: nil => DO hv1 <~ hsi_sreg_get hst f1;; DO hv2 <~ hsi_sreg_get hst f2;; let is_inv := is_inv_cmp_float c in DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; expanse_cond_fp true cond_single c lhsv - (*| Ocmp (Ccomplimm c imm), a1 :: nil => + (*| (Ccomplimm c imm), a1 :: nil => DO hv1 <~ hsi_sreg_get hst a1;; expanse_condimm_int64s c hv1 imm*) | _, _ => DO lhsv <~ hlist_args hst lr;; hSop op lhsv end + | Rop op => + DO lhsv <~ hlist_args hst lr;; + hSop op lhsv | Rload _ chunk addr => DO lhsv <~ hlist_args hst lr;; 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_neg_ltle_cmp: forall v1 v2, + Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmp_bool Cle v2 v1)). +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. + +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. + +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. + +Lemma xor_neg_ltle_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) Cle v2 v1)). +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. + +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. + +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 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. + simplify_SOME z; intros; apply xor_neg_ltle_cmp. + simplify_SOME z; intros; apply cmp_neg_ltgt_cmp. + simplify_SOME z; intros; apply xor_neg_ltge_cmp. +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. + simplify_SOME z; intros; apply xor_neg_ltle_cmpu. + simplify_SOME z; intros; apply cmp_neg_ltgt_cmpu. + simplify_SOME z; intros; apply xor_neg_ltge_cmpu. +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) @@ -857,26 +1049,26 @@ Lemma simplify_correct rsv lr hst: (OK1: seval_sval ge sp (rsv lr st) rs0 m0 <> None), sval_refines ge sp rs0 m0 hv (rsv lr st). Proof. - (* destruct rsv; simpl; auto. - - destruct op; wlp_simplify. - try (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). (* absurd case *) - - erewrite H0; eauto. simplify_SOME args. - intros. congruence. eauto. - - destruct (is_move_operation _ _) eqn: Hmove; wlp_simplify. - + exploit is_move_operation_correct; eauto. - intros (Hop & Hlsv); subst; simpl in *. - simplify_SOME z. - * erewrite H; eauto. - * try_simplify_someHyps; congruence. - * congruence. - + clear Hmove. - 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. (* absurd case *) + destruct rsv; simpl; auto. + - destruct op eqn:EQOP; try apply simplify_nothing. + { destruct (is_move_operation _ _) eqn: Hmove. + + wlp_simplify. + exploit is_move_operation_correct; eauto. + intros (Hop & Hlsv); subst; simpl in *. + simplify_SOME z. + * erewrite H; eauto. + * try_simplify_someHyps; congruence. + * congruence. + + apply simplify_nothing. } + { destruct cond; repeat (destruct lr; try apply simplify_nothing). + + apply simplify_ccomp_correct. + + apply simplify_ccompu_correct. + + admit. + + admit. + + admit. + + admit. + + admit. + + admit. } - (* Rload *) destruct trap; wlp_simplify. erewrite H0; eauto. @@ -886,7 +1078,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.*) Admitted. Global Opaque simplify. Local Hint Resolve simplify_correct: wlp. @@ -1038,30 +1230,30 @@ Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) := | Cge => CEbgeul optR0 end. -Definition cbranch_expanse (prev: hsistate_local) (i: instruction) : ?? (condition * list_hsval) := - match i with - | Icond (Ccomp c) (a1 :: a2 :: nil) _ _ _ => +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) - | Icond (Ccompu c) (a1 :: a2 :: nil) _ _ _ => + | (Ccompu c), (a1 :: a2 :: nil) => let is_inv := is_inv_cmp_int c in let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in DO hv1 <~ hsi_sreg_get prev a1;; DO hv2 <~ hsi_sreg_get prev a2;; DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; RET (cond, lhsv) - | Icond (Ccompl c) (a1 :: a2 :: nil) _ _ _ => + | (Ccompl c), (a1 :: a2 :: nil) => let is_inv := is_inv_cmp_int c in let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in DO hv1 <~ hsi_sreg_get prev a1;; DO hv2 <~ hsi_sreg_get prev a2;; DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; RET (cond, lhsv) - | Icond (Ccomplu c) (a1 :: a2 :: nil) _ _ _ => + | (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;; @@ -1071,10 +1263,9 @@ Definition cbranch_expanse (prev: hsistate_local) (i: instruction) : ?? (conditi (* | Icond (Ccompimm c n) (a1 :: nil) _ _ _ => let cond := transl_cbranch_int32s c (make_optR0 c) in RET (cond, a1 :: a1 :: nil)*) - | Icond cond args _ _ _ => + | _, _ => DO vargs <~ hlist_args prev args;; RET (cond, vargs) - | _ => FAILWITH "cbranch_expanse: not an Icond" end. (** ** Execution of one instruction *) @@ -1094,7 +1285,7 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) : RET (Some (hsist_set_local hst pc' next)) | Icond cond args ifso ifnot _ => let prev := hst.(hsi_local) in - DO res <~ cbranch_expanse prev i;; + DO res <~ cbranch_expanse prev cond args;; let (cond, vargs) := res in let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |}) @@ -1134,27 +1325,101 @@ 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. (* - destruct i; simpl; wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. +Proof. Admitted. + (* TODO destruct i; simpl; + try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail). - (* refines_dyn Iop *) + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. eapply hsist_set_local_correct_dyn; eauto. generalize (sok_local_set_sreg_simp (Rop o)); simpl; eauto. - (* refines_dyn Iload *) + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. eapply hsist_set_local_correct_dyn; eauto. generalize (sok_local_set_sreg_simp (Rload t0 m a)); simpl; eauto. - (* refines_dyn Istore *) + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. eapply hsist_set_local_correct_dyn; eauto. unfold sok_local; simpl; intuition. - (* refines_stat Icond *) + unfold cbranch_expanse; destruct c eqn:EQC; simpl in *. + destruct l. + 2: { + destruct l. + 2: { + destruct l. + { 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). + (*eapply hsist_set_local_correct_dyn; eauto.*) + split. + + constructor; simpl; auto. + 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 args. + { + intros. destruct args0, args2; auto; + unfold Val.cmpu_bool, Val.cmp_bool; + destruct Archi.ptr64; auto. simpl. + destruct (_ && _). + try destruct (Int.eq _ _); auto. + try destruct (Mem.valid_pointer _ _ _ || Mem.valid_pointer _ _ _); + simpl. congruence. + + + + + + + destruct args, args1; try congruence; auto. + destruct args1; try congruence; auto. + destruct args1; try congruence; auto. + destruct v1. + unfold Val.cmpu_bool, Val.cmp_bool. + erewrite H3. + + destruct c eqn:EQC; simpl; eauto. + 8: { destruct (hlist_args (hsi_local hst) l) in Hexta. + destruct in Hexta. + + + destruct exta; simpl in *. + destruct Hexta. + + split; simpl; auto. + destruct NEST as [|st0 se lse TOP NEST]; + econstructor; simpl; auto; constructor; auto. + + + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; + unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition. constructor; simpl; eauto. constructor. - (* refines_dyn Icond *) destruct REF as (EXREF & LREF & NEST). + destruct exta. simpl. split. + constructor; simpl; auto. constructor; simpl; auto. intros; erewrite seval_condition_refines; eauto. + + destruct c eqn:EQC; simpl; eauto. + 8: { destruct (hlist_args (hsi_local hst) l) in Hexta. + destruct in Hexta. + + + destruct exta; simpl in *. + destruct Hexta. + split; simpl; auto. destruct NEST as [|st0 se lse TOP NEST]; econstructor; simpl; auto; constructor; auto. |