From 31c3ca256506274e578ccca15b7db37280ea6bd5 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 27 Apr 2019 22:35:51 +0200 Subject: add bitfield insert opcode but not yet used nor translated --- mppa_k1c/ExtValues.v | 14 ++++++++++---- mppa_k1c/Machregs.v | 4 +++- mppa_k1c/NeedOp.v | 1 + mppa_k1c/Op.v | 36 +++++++++++++++++++++++++++++++++++- mppa_k1c/ValueAOp.v | 41 +++++++++++++++++++++++++++++++++++++++++ 5 files changed, 90 insertions(+), 6 deletions(-) diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 1348c0e8..58e8054f 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -41,8 +41,11 @@ Definition bitfield_maskl stop start := Definition insf stop start prev fld := let mask := bitfield_mask stop start in - Val.or (Val.and prev (Val.notint mask)) - (Val.and (Val.shl fld (Vint (Int.repr start))) mask). + if is_bitfield stop start + then + Val.or (Val.and prev (Val.notint mask)) + (Val.and (Val.shl fld (Vint (Int.repr start))) mask) + else Vundef. Definition is_bitfieldl stop start := (Z.leb start stop) @@ -74,5 +77,8 @@ Definition extfsl stop start v := Definition insfl stop start prev fld := let mask := bitfield_maskl stop start in - Val.orl (Val.andl prev (Val.notl mask)) - (Val.andl (Val.shll fld (Vint (Int.repr start))) mask). + if is_bitfieldl stop start + then + Val.orl (Val.andl prev (Val.notl mask)) + (Val.andl (Val.shll fld (Vint (Int.repr start))) mask) + else Vundef. diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 06758756..ee85fb1c 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -210,7 +210,9 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => true + | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ + | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ + | Oinsf _ _ | Oinsfl _ _ => true | _ => false end. diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 53c9c117..abdcd94a 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -119,6 +119,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ocmp c => needs_of_condition c | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => op3 (default nv) | Oextfz _ _ | Oextfs _ _ | Oextfzl _ _ | Oextfsl _ _ => op1 (default nv) + | Oinsf _ _ | Oinsfl _ _ => op2 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 2836f7cf..093c8c17 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -201,7 +201,9 @@ Inductive operation : Type := | Oextfz (stop : Z) (start : Z) | Oextfs (stop : Z) (start : Z) | Oextfzl (stop : Z) (start : Z) - | Oextfsl (stop : Z) (start : Z). + | Oextfsl (stop : Z) (start : Z) + | Oinsf (stop : Z) (start : Z) + | Oinsfl (stop : Z) (start : Z). (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -506,6 +508,8 @@ Definition eval_operation | (Oextfs stop start), v0::nil => Some (extfs stop start v0) | (Oextfzl stop start), v0::nil => Some (extfzl stop start v0) | (Oextfsl stop start), v0::nil => Some (extfsl stop start v0) + | (Oinsf stop start), v0::v1::nil => Some (insf stop start v0 v1) + | (Oinsfl stop start), v0::v1::nil => Some (insfl stop start v0 v1) | _, _ => None end. @@ -701,6 +705,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oselectfs cond => (Tsingle :: Tsingle :: (arg_type_of_condition0 cond) :: nil, Tsingle) | Oextfz _ _ | Oextfs _ _ => (Tint :: nil, Tint) | Oextfzl _ _ | Oextfsl _ _ => (Tlong :: nil, Tlong) + | Oinsf _ _ => (Tint :: Tint :: nil, Tint) + | Oinsfl _ _ => (Tlong :: Tlong :: nil, Tlong) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -993,6 +999,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). destruct (is_bitfieldl _ _). + destruct v0; simpl; trivial. + constructor. + (* insf *) + - unfold insf, bitfield_mask. + destruct (is_bitfield _ _). + + destruct v0; destruct v1; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + + constructor. + (* insf *) + - unfold insfl, bitfield_mask. + destruct (is_bitfieldl _ _). + + destruct v0; destruct v1; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + + constructor. Qed. End SOUNDNESS. @@ -1626,6 +1644,22 @@ Proof. destruct (is_bitfieldl _ _). + inv H4; trivial. + trivial. + + (* insf *) + - unfold insf. + destruct (is_bitfield _ _). + + inv H4; inv H2; trivial. + simpl. destruct (Int.ltu _ _); trivial. + simpl. trivial. + + trivial. + + (* insfl *) + - unfold insfl. + destruct (is_bitfieldl _ _). + + inv H4; inv H2; trivial. + simpl. destruct (Int.ltu _ _); trivial. + simpl. trivial. + + trivial. Qed. Lemma eval_addressing_inj: diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index b7bd6ec9..fe8bddcf 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -119,6 +119,34 @@ Definition eval_static_extfzl (stop : Z) (start : Z) (v : aval) := end else Vtop. +Definition eval_static_insf stop start prev fld := + let mask := Int.repr (zbitfield_mask stop start) in + if is_bitfield stop start + then + match prev, fld with + | (I prevI), (I fldI) => + if Int.ltu (Int.repr start) Int.iwordsize + then I (Int.or (Int.and prevI (Int.not mask)) + (Int.and (Int.shl fldI (Int.repr start)) mask)) + else Vtop + | _, _ => Vtop + end + else Vtop. + +Definition eval_static_insfl stop start prev fld := + let mask := Int64.repr (zbitfield_mask stop start) in + if is_bitfieldl stop start + then + match prev, fld with + | (L prevL), (L fldL) => + if Int.ltu (Int.repr start) Int64.iwordsize' + then L (Int64.or (Int64.and prevL (Int64.not mask)) + (Int64.and (Int64.shl' fldL (Int.repr start)) mask)) + else Vtop + | _,_ => Vtop + end + else Vtop. + Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 @@ -251,6 +279,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | (Oextfs stop start), v0::nil => eval_static_extfs stop start v0 | (Oextfzl stop start), v0::nil => eval_static_extfzl stop start v0 | (Oextfsl stop start), v0::nil => eval_static_extfsl stop start v0 + | (Oinsf stop start), v0::v1::nil => eval_static_insf stop start v0 v1 + | (Oinsfl stop start), v0::v1::nil => eval_static_insfl stop start v0 v1 | _, _ => Vbot end. @@ -400,6 +430,17 @@ Proof. destruct (is_bitfieldl _ _). + inv H1; constructor. + constructor. + + (* insf *) + - unfold insf, eval_static_insf. + destruct (is_bitfield _ _). + + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + constructor. + (* insfl *) + - unfold insfl, eval_static_insfl. + destruct (is_bitfieldl _ _). + + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + constructor. Qed. End SOUNDNESS. -- cgit