Now a more general way to perform imm operations

riscV/Asmgen.v

@@ -219,6 +219,12 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru
   | Some false => sem r1 X0
   end.
 
+Definition get_opimmR0 (rd: ireg) (opi: opimm) :=
+  match opi with
+  | OPimmADD i => Paddiw rd X0 i
+  | OPimmADDL i => Paddil rd X0 i
+  end.
+
 Definition transl_cbranch
            (cond: condition) (args: list mreg) (lbl: label) (k: code) :=
   match cond, args with
@@ -770,6 +776,9 @@ Definition transl_op
   | Ocmp cmp, _ =>
       do rd <- ireg_of res;
      transl_cond_op cmp rd args k
+  | OEimmR0 opi, nil =>
+      do rd <- ireg_of res;
+      OK (get_opimmR0 rd opi :: k)
   | OEseqw optR0, a1 :: a2 :: nil =>
       do rd <- ireg_of res;
       do rs1 <- ireg_of a1;
@@ -819,9 +828,6 @@ Definition transl_op
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Paddiw rd rs n :: k)
-  | OEaddiwr0 n, nil =>
-      do rd <- ireg_of res;
-      OK (Paddiw rd X0 n :: k)
   | OEandiw n, a1 :: nil =>
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
@@ -879,9 +885,6 @@ Definition transl_op
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Paddil rd rs n :: k)
-  | OEaddilr0 n, nil =>
-      do rd <- ireg_of res;
-      OK (Paddil rd X0 n :: k)
   | OEandil n, a1 :: nil =>
       do rd <- ireg_of res;
       do rs <- ireg_of a1;

riscV/Asmgenproof.v

@@ -308,6 +308,7 @@ Opaque Int.eq.
 - apply opimm64_label; intros; exact I.
 - destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
 - eapply transl_cond_op_label; eauto.
+- destruct opi; simpl; TailNoLabel.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.

riscV/Asmgenproof1.v

@@ -1258,7 +1258,12 @@ 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,8,9,10,17,18,19,20:
+  { unfold get_opimmR0; destruct opi; simpl;
+    econstructor; split; try apply exec_straight_one; simpl; eauto;
+    split; intros; Simpl.
+    try rewrite Int.add_commut; auto.
+    try rewrite Int64.add_commut; auto. }
+  7,8,9,16,17,18:
     econstructor; split; try apply exec_straight_one; simpl; eauto;
     split; intros; Simpl; try destruct (rs x0);
     try rewrite Int64.add_commut;

riscV/ExpansionOracle.ml

@@ -117,7 +117,7 @@ let load_hilo64 dest hi lo succ map_consts not_final =
 let loadimm32 dest n succ map_consts not_final =
   match make_immed32 n with
   | Imm32_single imm ->
-      let op1 = OEaddiwr0 imm in
+      let op1 = OEimmR0 (OPimmADD imm) in
       let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
       build_head_tuple [] sv
   | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts not_final
@@ -125,7 +125,7 @@ let loadimm32 dest n succ map_consts not_final =
 let loadimm64 dest n succ map_consts not_final =
   match make_immed64 n with
   | Imm64_single imm ->
-      let op1 = OEaddilr0 imm in
+      let op1 = OEimmR0 (OPimmADDL imm) in
       let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
       build_head_tuple [] sv
   | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts not_final

riscV/NeedOp.v

@@ -87,6 +87,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv)
   | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv)
   | Ocmp c => needs_of_condition c
+  | OEimmR0 _ => op1 (default nv)
   | OEseqw _ => op2 (default nv)
   | OEsnew _ => op2 (default nv)
   | OEsequw _ => op2 (default nv)
@@ -98,7 +99,6 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | OExoriw _ => op1 (bitwise nv)
   | OEluiw _ => op1 (default nv)
   | OEaddiw _ => op1 (default nv)
-  | OEaddiwr0 _ => op1 (default nv)
   | OEandiw n => op1 (andimm nv n)
   | OEoriw n => op1 (orimm nv n)
   | OEseql _ => op2 (default nv)
@@ -112,7 +112,6 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | OExoril _ => op1 (default nv)
   | OEluil _ => op1 (default nv)
   | OEaddil _ => op1 (default nv)
-  | OEaddilr0 _ => op1 (default nv)
   | OEandil _ => op1 (default nv)
   | OEoril _ => op1 (default nv)
   | OEloadli _ => op1 (default nv)

riscV/Op.v

@@ -76,6 +76,11 @@ Inductive mayundef: Type :=
   | MUshrx: int -> mayundef
   | MUshrxl: int -> mayundef.
 
+(* This allow to have a single RTL constructor to perform an arith operation between an immediate and X0 *)
+Inductive opimm: Type :=
+  | OPimmADD: int -> opimm
+  | OPimmADDL: int64 -> opimm.
+
 (** Arithmetic and logical operations.  In the descriptions, [rd] is the
   result of the operation and [r1], [r2], etc, are the arguments. *)
 
@@ -179,6 +184,7 @@ Inductive operation : Type :=
 (*c Boolean tests: *)
   | Ocmp (cond: condition)   (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
   (* Expansed conditions *)
+  | OEimmR0 (opi: opimm)
   | 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 *)
@@ -188,7 +194,6 @@ Inductive operation : Type :=
   | OEsltiw (n: int)                             (**r set-less-than immediate *)
   | OEsltiuw (n: int)                            (**r set-less-than unsigned immediate *)
   | OEaddiw (n: int)                             (**r add immediate *)
-  | OEaddiwr0 (n: int)                           (**r add immediate *)
   | OEandiw (n: int)                             (**r and immediate *)
   | OEoriw (n: int)                              (**r or immediate *)
   | OExoriw (n: int)                             (**r xor immediate *)
@@ -202,7 +207,6 @@ Inductive operation : Type :=
   | OEsltil (n: int64)                           (**r set-less-than immediate *)
   | OEsltiul (n: int64)                          (**r set-less-than unsigned immediate *)
   | OEaddil (n: int64)                           (**r add immediate *)
-  | OEaddilr0 (n: int64)                         (**r add immediate *)
   | OEandil (n: int64)                           (**r and immediate *)
   | OEoril (n: int64)                            (**r or immediate *)
   | OExoril (n: int64)                           (**r xor immediate *)
@@ -300,6 +304,12 @@ Definition eval_may_undef (mu: mayundef) (v1 v2: val): val :=
       end
   end.
 
+Definition eval_opimmR0 (opi: opimm): val :=
+  match opi with
+  | OPimmADD i => Val.add (Vint i) zero32
+  | OPimmADDL i => Val.addl (Vlong i) zero64
+  end.
+
 (** * Evaluation functions *)
 
 (** Evaluation of conditions, operators and addressing modes applied
@@ -443,6 +453,7 @@ Definition eval_operation
   | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1)
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
   (* Expansed conditions *)
+  | OEimmR0 opi, nil => Some (eval_opimmR0 opi)
   | 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)
@@ -454,7 +465,6 @@ Definition eval_operation
   | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n))
   | OEluiw n, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12)))
   | OEaddiw n, v1::nil => Some (Val.add (Vint n) v1)
-  | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32)
   | OEandiw n, v1::nil => Some (Val.and (Vint n) v1)
   | OEoriw n, v1::nil => Some (Val.or (Vint n) v1)
   | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64))
@@ -468,7 +478,6 @@ Definition eval_operation
   | 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))))
   | OEaddil n, v1::nil => Some (Val.addl (Vlong n) v1)
-  | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64)
   | OEandil n, v1::nil => Some (Val.andl (Vlong n) v1)
   | OEoril n, v1::nil => Some (Val.orl (Vlong n) v1)
   | OEloadli n, nil => Some (Vlong n)
@@ -557,6 +566,12 @@ Definition type_of_condition (c: condition) : list typ :=
   | CEbgeul _ => Tlong :: Tlong :: nil
   end.
 
+Definition type_of_opimmR0 (opi: opimm) : typ :=
+  match opi with
+  | OPimmADD _ => Tint
+  | OPimmADDL _ => Tlong
+  end.
+
 Definition type_of_operation (op: operation) : list typ * typ :=
   match op with
   | Omove => (nil, Tint)   (* treated specially *)
@@ -652,6 +667,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osingleoflong => (Tlong :: nil, Tsingle)
   | Osingleoflongu => (Tlong :: nil, Tsingle)
   | Ocmp c => (type_of_condition c, Tint)
+  | OEimmR0 opi => (nil, type_of_opimmR0 opi)
   | OEseqw _ => (Tint :: Tint :: nil, Tint)
   | OEsnew _ => (Tint :: Tint :: nil, Tint)
   | OEsequw _ => (Tint :: Tint :: nil, Tint)
@@ -663,7 +679,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OExoriw _ => (Tint :: nil, Tint)
   | OEluiw _ => (nil, Tint)
   | OEaddiw _ => (Tint :: nil, Tint)
-  | OEaddiwr0 _ => (nil, Tint)
   | OEandiw _ => (Tint :: nil, Tint)
   | OEoriw _ => (Tint :: nil, Tint)
   | OEseql _ => (Tlong :: Tlong :: nil, Tint)
@@ -679,7 +694,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OExoril _ => (Tlong :: nil, Tlong)
   | OEluil _ => (nil, Tlong)
   | OEaddil _ => (Tlong :: nil, Tlong)
-  | OEaddilr0 _ => (nil, Tlong)
   | OEloadli _ => (nil, Tlong)
   | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64)
   | OEfeqd => (Tfloat :: Tfloat :: nil, Tint)
@@ -907,6 +921,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; cbn; trivial.
   (* cmp *)
   - destruct (eval_condition cond vl m)... destruct b...
+  (* OEimmR0 *)
+  - destruct opi; unfold eval_opimmR0; simpl; auto.
   (* OEseqw *)
   - destruct optR0 as [[]|]; simpl; unfold Val.cmp;
     destruct Val.cmp_bool... all: destruct b...
@@ -932,8 +948,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b...
   (* OEaddiw *)
   - fold (Val.add (Vint n) v0); apply type_add.
-  (* OEaddiwr0 *)
-  - trivial.
   (* OEandiw *)
   - destruct v0...
   (* OEoriw *)
@@ -967,8 +981,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b...
   (* OEaddil *)
   - fold (Val.addl (Vlong n) v0); apply type_addl.
-  (* OEaddilr0 *)
-  - trivial.
   (* OEandil *)
   - destruct v0...
   (* OEoril *)
@@ -1769,6 +1781,8 @@ Proof.
     exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
     destruct b; simpl; constructor.
     simpl; constructor.
+  (* OEimmR0 *)
+  - destruct opi; unfold eval_opimmR0; simpl; auto.
   (* OEseqw *)
   - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp;
     inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto;

riscV/PrintOp.ml

@@ -36,6 +36,10 @@ let mu_name pp = function
   | MUshrx i -> fprintf pp "MUshrx(%ld)" (camlint_of_coqint i)
   | MUshrxl i -> fprintf pp "MUshrxl(%ld)" (camlint_of_coqint i)
 
+let get_immR0 pp = function
+  | OPimmADD i -> fprintf pp "OPimmADD(%ld)" (camlint_of_coqint i)
+  | OPimmADDL i -> fprintf pp "OPimmADDL(%ld)" (camlint_of_coqint i)
+
 let get_optR0_s c reg pp r1 r2 = function
   | None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2
   | Some true -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1
@@ -203,6 +207,7 @@ let print_operation reg pp = function
   | Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1
   | Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1
   | Ocmp c, args -> print_condition reg pp (c, args)
+  | OEimmR0 opi, [] -> fprintf pp "OEimmR0(%a)" get_immR0 opi
   | OEseqw optR0, [r1;r2] -> fprintf pp "OEseqw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
   | OEsnew optR0, [r1;r2] -> fprintf pp "OEsnew"; (get_optR0_s Cne reg pp r1 r2 optR0)
   | OEsequw optR0, [r1;r2] -> fprintf pp "OEsequw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
@@ -214,7 +219,6 @@ let print_operation reg pp = function
   | OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
   | OEaddiw n, [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n)
-  | OEaddiwr0 n, [] -> fprintf pp "OEaddiwr0(X0,%ld)" (camlint_of_coqint n)
   | OEandiw n, [r1] -> fprintf pp "OEandiw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEoriw n, [r1] -> fprintf pp "OEoriw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEseql optR0, [r1;r2] -> fprintf pp "OEseql"; (get_optR0_s Ceq reg pp r1 r2 optR0)
@@ -228,7 +232,6 @@ let print_operation reg pp = function
   | OExoril n, [r1] -> fprintf pp "OExoril(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n)
   | OEaddil n, [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n)
-  | OEaddilr0 n, [] -> fprintf pp "OEaddilr0(X0,%ld)" (camlint_of_coqint n)
   | OEandil n, [r1] -> fprintf pp "OEandil(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEoril n, [r1] -> fprintf pp "OEoril(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n)

riscV/RTLpathSE_simplify.v

@@ -50,14 +50,14 @@ Definition load_hilo64 (hi lo: int64) :=
 Definition loadimm32 (n: int) :=
   match make_immed32 n with
   | Imm32_single imm =>
-      fSop (OEaddiwr0 imm) fSnil
+      fSop (OEimmR0 (OPimmADD imm)) fSnil
   | Imm32_pair hi lo => load_hilo32 hi lo
   end.
 
 Definition loadimm64 (n: int64) :=
   match make_immed64 n with
   | Imm64_single imm =>
-      fSop (OEaddilr0 imm) fSnil
+      fSop (OEimmR0 (OPimmADDL imm)) fSnil
   | Imm64_pair hi lo => load_hilo64 hi lo
   | Imm64_large imm => fSop (OEloadli imm) fSnil
   end.

riscV/ValueAOp.v

@@ -51,6 +51,12 @@ Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval :=
       end
   end.
 
+Definition eval_opimmR0 (opi: opimm): aval :=
+  match opi with
+  | OPimmADD i => add (I i) zero32
+  | OPimmADDL i => addl (L i) zero64
+  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
@@ -220,6 +226,7 @@ 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)
+  | OEimmR0 opi, nil => eval_opimmR0 opi
   | 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)
@@ -231,7 +238,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OExoriw n, v1::nil => xor v1 (I n)
   | OEluiw n, nil => shl (I n) (I (Int.repr 12))
   | OEaddiw n, v1::nil => add (I n) v1
-  | OEaddiwr0 n, nil => add (I n) zero32
   | OEandiw n, v1::nil => and (I n) v1
   | OEoriw n, v1::nil => or (I n) v1
   | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64)
@@ -247,7 +253,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OExoril n, v1::nil => xorl v1 (L n)
   | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12)))
   | OEaddil n, v1::nil => addl (L n) v1
-  | OEaddilr0 n, nil => addl (L n) zero64
   | OEloadli n, nil => L (n)
   | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2
   | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2)
@@ -472,36 +477,36 @@ Proof.
   destruct (propagate_float_constants tt); constructor.
   rewrite Ptrofs.add_zero_l; eauto with va.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
-  
+
+  unfold Op.eval_opimmR0, eval_opimmR0, Op.zero32, zero32, Op.zero64, zero64;
+  destruct opi; eauto with va.
   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.
   
   { fold (Val.add (Vint n) a1); eauto with va. }
-  { unfold zero32; simpl; eauto with va. }
   { fold (Val.and (Vint n) a1); eauto with va. }
   { fold (Val.or (Vint n) a1); eauto with va. }
   { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1;
   try apply vmatch_ifptr_undef. }
   9: { fold (Val.addl (Vlong n) a1); eauto with va. }
-  10: { fold (Val.andl (Vlong n) a1); eauto with va. }
-  10: { fold (Val.orl (Vlong n) a1); eauto with va. }
-  10: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl;
+  9: { fold (Val.andl (Vlong n) a1); eauto with va. }
+  9: { fold (Val.orl (Vlong n) a1); eauto with va. }
+  9: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl;
   apply vmatch_ifptr_l. }
   
   1,10: simpl; eauto with va.
-  2:
+  10:
     unfold Op.eval_may_undef, eval_may_undef; destruct mu;
     inv H1; inv H0; eauto with va;
     try destruct (Int.ltu _ _); simpl;
     try eapply vmatch_ifptr_p, pmatch_top'; 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. }
+  4,5,7: apply eval_cmplu_sound; auto.
+  1,3,4: apply eval_cmpl_sound; auto.
+  2: { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. }
+  2: { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. }
   all: unfold Val.cmpf; apply of_optbool_sound; eauto with va.
 Qed.