add bitfield insert opcode but not yet used nor translated

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.