diff options
Diffstat (limited to 'riscV/Op.v')
| -rw-r--r-- | riscV/Op.v | 109 |
1 files changed, 43 insertions, 66 deletions
@@ -69,6 +69,13 @@ Inductive condition : Type := | CEbgel (optR0: option bool) (**r branch-if-greater-or-equal signed *) | CEbgeul (optR0: option bool). (**r branch-if-greater-or-equal unsigned *) +(* This type will define the eval function of a OEmayundef operation. *) +Inductive mayundef: Type := + | MUint: mayundef + | MUlong: mayundef + | MUshrx: int -> mayundef + | MUshrxl: int -> mayundef. + (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -201,9 +208,7 @@ Inductive operation : Type := | OExoril (n: int64) (**r xor immediate *) | OEluil (n: int64) (**r load upper-immediate *) | OEloadli (n: int64) (**r load an immediate int64 *) - | OEmayundef (is_long: bool) - | OEshrxundef (n: int) - | OEshrxlundef (n: int) + | OEmayundef (mu: mayundef) | OEfeqd (**r compare equal *) | OEfltd (**r compare less-than *) | OEfled (**r compare less-than/equal *) @@ -242,9 +247,9 @@ Defined. Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec; intros. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec Val.eq; intros. decide equality. - all: destruct optR0, optR1; decide equality. + all: try destruct optR0, optR1; try decide equality. Defined. (* Alternate definition: @@ -271,42 +276,28 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 v | Some false => sem v1 vz end. -Definition may_undef_int (is_long: bool) (v1 v2: val): val := - if negb is_long then - match v1 with - | Vint _ => v2 - | _ => Vundef - end - else - match v1 with - | Vlong _ => v2 - | _ => 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 +Definition eval_may_undef (mu: mayundef) (v1 v2: val): val := + match mu with + | MUint => match v1 with + | Vint _ => v2 + | _ => Vundef + end + | MUlong => match v1 with + | Vlong _ => v2 + | _ => Vundef + end + | MUshrx i => + match v1 with + | Vint _ => + if Int.ltu i (Int.repr 31) then v1 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 + | MUshrxl i => + match v1 with + | Vlong _ => + if Int.ltu i (Int.repr 63) then v1 else Vundef | _ => Vundef end - | _ => Vundef end. (** * Evaluation functions *) @@ -481,9 +472,7 @@ Definition eval_operation | 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)) + | OEmayundef mu, v1 :: v2 :: nil => Some (eval_may_undef mu v1 v2) | 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) @@ -693,8 +682,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | 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) @@ -736,6 +723,14 @@ Proof. intros. unfold Val.has_type, Val.addl. destruct Archi.ptr64, v1, v2; auto. Qed. +Remark type_mayundef: + forall mu v1 v2, Val.has_type (eval_may_undef mu v1 v2) Tany64. +Proof. + intros. unfold eval_may_undef. + destruct mu eqn:EQMU, v1, v2; simpl; auto. + all: destruct Int.ltu; simpl; auto. +Qed. + Lemma type_of_operation_sound: forall op vl sp v m, op <> Omove -> @@ -946,8 +941,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OExoriw *) - destruct v0... (* OEluiw *) - - unfold may_undef_int; - destruct (Int.ltu _ _); cbn; trivial. + - destruct (Int.ltu _ _); cbn; trivial. (* OEseql *) - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... @@ -986,16 +980,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* 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. + - apply type_mayundef. (* OEfeqd *) - destruct v0; destruct v1; cbn; auto. destruct Float.cmp; cbn; auto. @@ -1721,7 +1706,7 @@ Proof. (* shru, shruimm *) - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. - (* shrx *) + (* shrx *) - inv H4; cbn; try apply Val.val_inject_undef. destruct (Int.ltu n (Int.repr 63)); cbn. apply Val.inject_long. @@ -1851,17 +1836,9 @@ Proof. (* 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. + - destruct mu; inv H4; inv H2; simpl; auto; + try destruct (Int.ltu _ _); simpl; auto. + all: eapply Val.inject_ptr; eauto. (* OEfeqd *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. |