diff options
Diffstat (limited to 'riscV/Op.v')
| -rw-r--r-- | riscV/Op.v | 34 |
1 files changed, 24 insertions, 10 deletions
@@ -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; |