[Admitted checker] Checker expansion for reg Ocmp (without scratch)

4 files changed, 36 insertions, 36 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 4b27ee81..7f63bfee 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -105,8 +105,8 @@ Definition addimm32 := opimm32 Paddw Paddiw.
 Definition andimm32 := opimm32 Pandw Pandiw.
 Definition orimm32  := opimm32 Porw  Poriw.
 Definition xorimm32 := opimm32 Pxorw Pxoriw.
-(* TODO REMOVE Definition sltimm32 := opimm32 Psltw Psltiw.*)
-(* TODO REMOVE Definition sltuimm32 := opimm32 Psltuw Psltiuw.*)
+Definition sltimm32 := opimm32 Psltw Psltiw.
+Definition sltuimm32 := opimm32 Psltuw Psltiuw.
   
 Definition load_hilo64 (r: ireg) (hi lo: int64) k :=
   if Int64.eq lo Int64.zero then Pluil r hi :: k
@@ -132,8 +132,8 @@ Definition addimm64 := opimm64 Paddl Paddil.
 Definition andimm64 := opimm64 Pandl Pandil.
 Definition orimm64  := opimm64 Porl  Poril.
 Definition xorimm64 := opimm64 Pxorl  Pxoril.
-(* TODO REMOVE Definition sltimm64 := opimm64 Psltl Psltil.*)
-(* TODO REMOVE Definition sltuimm64 := opimm64 Psltul Psltiul.*)
+Definition sltimm64 := opimm64 Psltl Psltil.
+Definition sltuimm64 := opimm64 Psltul Psltiul.
 
 Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   if Ptrofs.eq_dec n Ptrofs.zero then
@@ -145,7 +145,7 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   
 (** Translation of conditional branches. *)
 
-(* TODO REMOVE Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
+Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
   match cmp with
   | Ceq => Pbeqw r1 r2 lbl
   | Cne => Pbnew r1 r2 lbl
@@ -203,7 +203,7 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
   | Cle => (Pfles rd fs1 fs2, true)
   | Cgt => (Pflts rd fs2 fs1, true)
   | Cge => (Pfles rd fs2 fs1, true)
-   end.*)
+   end.
  
 Definition apply_bin_r0_r0r0lbl (optR0: option bool) (sem: ireg0 -> ireg0 -> label -> instruction) (r1 r2: ireg0) (lbl: label) :=
   match optR0 with
@@ -222,7 +222,7 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru
 Definition transl_cbranch
            (cond: condition) (args: list mreg) (lbl: label) (k: code) :=
   match cond, args with
-(* TODO REMOVE | Ccomp c, a1 :: a2 :: nil =>
+| Ccomp c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (transl_cbranch_int32s c r1 r2 lbl :: k)
   | Ccompu c, a1 :: a2 :: nil =>
@@ -273,7 +273,7 @@ Definition transl_cbranch
   | Cnotcompfs c, f1 :: f2 :: nil =>
       do r1 <- freg_of f1; do r2 <- freg_of f2;
       let (insn, normal) := transl_cond_single c X31 r1 r2 in
-   OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)*)
+   OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
 
   | CEbeqw optR0, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
@@ -319,7 +319,7 @@ Definition transl_cbranch
   [rd] target register to 0 or 1 depending on the truth value of the
   condition. *)
 
-(* TODO REMOVE Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
+Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
   match cmp with
   | Ceq => Pseqw rd r1 r2 :: k
   | Cne => Psnew rd r1 r2 :: k
@@ -393,9 +393,9 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
   match cmp with
   | Clt => sltuimm64 rd r1 n k
   | _   => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)
-   end. *)
+   end.
 
-(* TODO REMOVE Definition transl_cond_op
+Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
   match cond, args with
   | Ccomp c, a1 :: a2 :: nil =>
@@ -440,7 +440,7 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
   | _, _ =>
       Error(msg "Asmgen.transl_cond_op")
-   end.*)
+   end.
 
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
@@ -755,9 +755,9 @@ Definition transl_op
   | Osingleoflongu, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfcvtslu rd rs :: k)
-  (* TODO REMOVE | Ocmp cmp, _ =>
+  | Ocmp cmp, _ =>
       do rd <- ireg_of res;
-     transl_cond_op cmp rd args k *)
+     transl_cond_op cmp rd args k
   | OEseqw 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 52a3bf27..47ee39f0 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -161,7 +161,7 @@ Proof.
 Qed.
 Hint Resolve addptrofs_label: labels.
 
-(* TODO REMOVE Remark transl_cond_float_nolabel:
+Remark transl_cond_float_nolabel:
   forall c r1 r2 r3 insn normal,
   transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn.
 Proof.
@@ -173,14 +173,14 @@ Remark transl_cond_single_nolabel:
   transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn.
 Proof.
   unfold transl_cond_single; intros. destruct c; inv H; exact I.
-   Qed.*)
+   Qed.
 
 Remark transl_cbranch_label:
   forall cond args lbl k c,
   transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.
 Proof.
   intros. unfold transl_cbranch in H; destruct cond; TailNoLabel.
-  (* TODO REMOVE - destruct c0; simpl; TailNoLabel.
+- destruct c0; simpl; TailNoLabel.
 - destruct c0; simpl; TailNoLabel.
 - destruct (Int.eq n Int.zero).
   destruct c0; simpl; TailNoLabel.
@@ -211,7 +211,7 @@ Proof.
   destruct normal; TailNoLabel.
 - destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
   apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-     destruct normal; TailNoLabel.*)
+     destruct normal; TailNoLabel.
 - destruct optR0 as [[]|]; TailNoLabel.
 - destruct optR0 as [[]|]; TailNoLabel.
 - destruct optR0 as [[]|]; TailNoLabel.
@@ -226,7 +226,7 @@ Proof.
 - destruct optR0 as [[]|]; TailNoLabel.
 Qed.
 
-(* TODO REMOVE Remark transl_cond_op_label:
+Remark transl_cond_op_label:
   forall cond args r k c,
   transl_cond_op cond r args k = OK c -> tail_nolabel k c.
 Proof.
@@ -279,7 +279,7 @@ Proof.
 - destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
   apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
   destruct normal; TailNoLabel.
-   Qed.*)
+   Qed.
 
 Remark transl_op_label:
   forall op args r k c,
@@ -303,7 +303,7 @@ Opaque Int.eq.
 - apply opimm64_label; intros; exact I.
 - apply opimm64_label; intros; exact I.
 - destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
-(* TODO REMOVE - eapply transl_cond_op_label; eauto.*)
+- eapply transl_cond_op_label; eauto.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 429c5fec..57d281ec 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -292,7 +292,7 @@ Qed.
 
 (** Translation of conditional branches *)
 
-(* TODO REMOVE Lemma transl_cbranch_int32s_correct:
+Lemma transl_cbranch_int32s_correct:
   forall cmp r1 r2 lbl (rs: regset) m b,
   Val.cmp_bool cmp rs##r1 rs##r2 = Some b ->
   exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m =
@@ -375,7 +375,7 @@ Proof.
   rewrite <- Float32.cmp_swap. auto.
 - simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
   rewrite <- Float32.cmp_swap. auto.
-   Qed.*)
+   Qed.
 
 (* TODO UNUSUED ? Remark branch_on_X31:
   forall normal lbl (rs: regset) m b,
@@ -417,7 +417,7 @@ Proof.
   { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. }
   clear EVAL MEXT AG.
   destruct cond; simpl in TRANSL; ArgsInv.
-  (* TODO REMOVE - exists rs, (transl_cbranch_int32s c0 x x0 lbl).
+  - exists rs, (transl_cbranch_int32s c0 x x0 lbl).
   intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
 - exists rs, (transl_cbranch_int32u c0 x x0 lbl).
   intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
@@ -492,7 +492,7 @@ Proof.
   econstructor; econstructor.
   split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
   split. rewrite V; destruct normal, b; reflexivity.
-     intros; Simpl.*)
+     intros; Simpl.
 
 - destruct optR0 as [[]|];
   unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
@@ -589,7 +589,7 @@ Qed.
 
 (** Translation of condition operators *)
 
-(* TODO REMOVE Lemma transl_cond_int32s_correct:
+Lemma transl_cond_int32s_correct:
   forall cmp rd r1 r2 k rs m,
   exists rs',
      exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m
@@ -984,7 +984,7 @@ Proof.
 * econstructor; split.
   apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
   split; intros; Simpl.
-   Qed.*)
+   Qed.
 
 (** Some arithmetic properties. *)
 
@@ -1195,8 +1195,8 @@ Opaque Int.eq.
       apply exec_straight_one. simpl; reflexivity. auto. 
       split; intros; Simpl. }
   (* cond *)
-  (* TODO REMOVE { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
-     exists rs'; split. eexact A. eauto with asmgen. }*)
+  { 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;
   split; intros; Simpl; rewrite Int.add_commut; auto.
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index e267fd5a..b3a440a4 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -284,7 +284,7 @@ let expanse_condimm_int32u cmp a1 n dest succ k =
           (cond_int32u false cmp a1 (r2p ()) dest succ k)
 
 let expanse_condimm_int64s cmp a1 n dest succ k =
-  if Int.eq n Int.zero then cond_int64s true cmp a1 a1 dest succ k
+  if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k
   else
     match cmp with
     | Ceq | Cne ->
@@ -391,14 +391,14 @@ let expanse (sb : superblock) code pm =
           debug "Iop/Ccompu\n";
           exp := cond_int32u false c a1 a2 dest succ [];
           was_exp := true
-      | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
+      (*| Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccompimm\n";
           exp := expanse_condimm_int32s c a1 imm dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccompuimm\n";
           exp := expanse_condimm_int32u c a1 imm dest succ [];
-          was_exp := true
+          was_exp := true*)
       | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
           debug "Iop/Ccompl\n";
           exp := cond_int64s false c a1 a2 dest succ [];
@@ -407,14 +407,14 @@ let expanse (sb : superblock) code pm =
           debug "Iop/Ccomplu\n";
           exp := cond_int64u false c a1 a2 dest succ [];
           was_exp := true
-      | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
+      (*| Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccomplimm\n";
           exp := expanse_condimm_int64s c a1 imm dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccompluimm\n";
           exp := expanse_condimm_int64u c a1 imm dest succ [];
-          was_exp := true
+          was_exp := true*)
       | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
           debug "Iop/Ccompf\n";
           exp := expanse_cond_fp false cond_float c f1 f2 dest succ [];
@@ -431,7 +431,7 @@ let expanse (sb : superblock) code pm =
           debug "Iop/Cnotcompfs\n";
           exp := expanse_cond_fp true cond_single c f1 f2 dest succ [];
           was_exp := true
-      | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
+      (*| Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
           debug "Icond/Ccomp\n";
           exp := cbranch_int32s false c a1 a2 info succ1 succ2 [];
           was_branch := true;
@@ -491,7 +491,7 @@ let expanse (sb : superblock) code pm =
           debug "Icond/Cnotcompfs\n";
           exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 [];
           was_branch := true;
-          was_exp := true
+          was_exp := true*)
       | _ -> new_order := n :: !new_order);
       if !was_exp then (
         node := !node + 1;