diff options
Diffstat (limited to 'riscV/Op.v')
| -rw-r--r-- | riscV/Op.v | 120 |
1 files changed, 107 insertions, 13 deletions
@@ -180,9 +180,12 @@ Inductive operation : Type := | 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 *) + | 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 *) | OEluiw (n: int) (**r load upper-immediate *) - | OEaddiwr0 (n: int) (**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 *) @@ -191,11 +194,16 @@ Inductive operation : Type := | OEsltul (optR0: option bool) (**r set-less-than unsigned *) | 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 *) | OEluil (n: int64) (**r load upper-immediate *) - | OEaddilr0 (n: int64) (**r add immediate *) | OEloadli (n: int64) (**r load an immediate int64 *) | OEmayundef (is_long: bool) + | OEshrxundef (n: int) + | OEshrxlundef (n: int) | OEfeqd (**r compare equal *) | OEfltd (**r compare less-than *) | OEfled (**r compare less-than/equal *) @@ -252,13 +260,6 @@ Defined. *) Global Opaque eq_condition eq_addressing eq_operation. - -(** * Evaluation functions *) - -(** Evaluation of conditions, operators and addressing modes applied - to lists of values. Return [None] when the computation can trigger an - error, e.g. integer division by zero. [eval_condition] returns a boolean, - [eval_operation] and [eval_addressing] return a value. *) Definition zero32 := (Vint Int.zero). Definition zero64 := (Vlong Int64.zero). @@ -282,6 +283,39 @@ Definition may_undef_int (is_long: bool) (v1 v2: val): val := | _ => Vundef end. +Definition shrx_imm_undef (v1 v2: val): val := + match v1 with + | Vint n1 => + match v2 with + | Vint n2 => + if Int.ltu n2 (Int.repr 31) + then Vint n1 + else Vundef + | _ => Vundef + end + | _ => Vundef + end. + +Definition shrxl_imm_undef (v1 v2: val): val := + match v1 with + | Vlong n1 => + match v2 with + | Vint n2 => + if Int.ltu n2 (Int.repr 63) + then Vlong n1 + else Vundef + | _ => Vundef + end + | _ => Vundef + end. + +(** * Evaluation functions *) + +(** Evaluation of conditions, operators and addressing modes applied + to lists of values. Return [None] when the computation can trigger an + error, e.g. integer division by zero. [eval_condition] returns a boolean, + [eval_operation] and [eval_addressing] return a value. *) + 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 @@ -428,7 +462,10 @@ Definition eval_operation | 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 (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)) | 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)) @@ -439,9 +476,14 @@ Definition eval_operation | 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)))) + | 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) | OEmayundef is_long, v1::v2::nil => Some (may_undef_int is_long v1 v2) + | OEshrxundef n, v1::nil => Some (shrx_imm_undef v1 (Vint n)) + | OEshrxlundef n, v1::nil => Some (shrxl_imm_undef v1 (Vint n)) | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2) | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2) | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2) @@ -631,7 +673,10 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltiuw _ => (Tint :: nil, Tint) | 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) | OEsnel _ => (Tlong :: Tlong :: nil, Tint) | OEsequl _ => (Tlong :: Tlong :: nil, Tint) @@ -640,11 +685,16 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltul _ => (Tlong :: Tlong :: nil, Tint) | OEsltil _ => (Tlong :: nil, Tint) | OEsltiul _ => (Tlong :: nil, Tint) + | OEandil _ => (Tlong :: nil, Tlong) + | OEoril _ => (Tlong :: nil, Tlong) | OExoril _ => (Tlong :: nil, Tlong) | OEluil _ => (nil, Tlong) + | OEaddil _ => (Tlong :: nil, Tlong) | OEaddilr0 _ => (nil, Tlong) | OEloadli _ => (nil, Tlong) | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64) + | OEshrxundef _ => (Tint :: nil, Tint) + | OEshrxlundef _ => (Tlong :: nil, Tlong) | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) | OEfltd => (Tfloat :: Tfloat :: nil, Tint) | OEfled => (Tfloat :: Tfloat :: nil, Tint) @@ -885,13 +935,19 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). all: destruct b... (* OEsltiuw *) - 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 *) + - destruct v0... (* OExoriw *) - destruct v0... (* OEluiw *) - unfold may_undef_int; destruct (Int.ltu _ _); cbn; trivial. - (* OEaddiwr0 *) - - simpl; trivial. (* OEseql *) - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... @@ -915,17 +971,31 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). all: destruct b... (* OEsltiul *) - 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 *) + - destruct v0... (* OExoril *) - destruct v0... (* OEluil *) - simpl; trivial. - (* OEaddilr0 *) - - simpl; trivial. (* OEloadli *) - trivial. (* OEmayundef *) - unfold may_undef_int; destruct is_long, v0, v1; simpl; trivial. + (* OEshrxundef *) + - unfold shrx_imm_undef; + destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + (* OEshrxlundef *) + - unfold shrxl_imm_undef; + destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. (* OEfeqd *) - destruct v0; destruct v1; cbn; auto. destruct Float.cmp; cbn; auto. @@ -1736,6 +1806,14 @@ Proof. - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int. (* OEsltiuw *) - apply eval_cmpu_bool_inj; auto. + (* OEaddiw *) + - fold (Val.add (Vint n) v); + fold (Val.add (Vint n) v'); + apply Val.add_inject; auto. + (* OEandiw *) + - inv H4; cbn; auto. + (* OEoriw *) + - inv H4; cbn; auto. (* OExoriw *) - inv H4; simpl; auto. (* OEluiw *) @@ -1762,12 +1840,28 @@ Proof. - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int. (* OEsltiul *) - apply eval_cmplu_bool_inj; auto. + (* OEaddil *) + - fold (Val.addl (Vlong n) v); + fold (Val.addl (Vlong n) v'); + apply Val.addl_inject; auto. + (* OEandil *) + - inv H4; cbn; auto. + (* OEoril *) + - inv H4; cbn; auto. (* OExoril *) - inv H4; simpl; auto. (* OEmayundef *) - destruct is_long; inv H4; inv H2; unfold may_undef_int; simpl; auto; eapply Val.inject_ptr; eauto. + (* OEshrxundef *) + - inv H4; + unfold shrx_imm_undef; simpl; auto. + destruct (Int.ltu _ _); auto. + (* OEshrxlundef *) + - inv H4; + unfold shrxl_imm_undef; simpl; auto. + destruct (Int.ltu _ _); auto. (* OEfeqd *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. |