diff options
| -rw-r--r-- | mppa_k1c/NeedOp.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 12 | ||||
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 2 |
3 files changed, 18 insertions, 0 deletions
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 5f8648d3..c5d9e58f 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -47,6 +47,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv) | Oand => op2 (bitwise nv) | Oandimm n => op1 (andimm nv n) + | Onand => op2 (bitwise nv) + | Onandimm n => op1 (andimm nv n) | Oor => op2 (bitwise nv) | Oorimm n => op1 (orimm nv n) | Oxor => op2 (bitwise nv) @@ -148,6 +150,8 @@ Proof. - apply mul_sound; auto. - apply and_sound; auto. - apply andimm_sound; auto. +- apply notint_sound; apply and_sound; auto. +- apply notint_sound; apply andimm_sound; auto. - apply or_sound; auto. - apply orimm_sound; auto. - apply xor_sound; auto. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 3a006fb2..8c5f01cd 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -78,6 +78,8 @@ Inductive operation : Type := | Omodu (**r [rd = r1 % r2] (unsigned) *) | Oand (**r [rd = r1 & r2] *) | Oandimm (n: int) (**r [rd = r1 & n] *) + | Onand (**r [rd = ~(r1 & r2)] *) + | Onandimm (n: int) (**r [rd = ~(r1 & n)] *) | Oor (**r [rd = r1 | r2] *) | Oorimm (n: int) (**r [rd = r1 | n] *) | Oxor (**r [rd = r1 ^ r2] *) @@ -248,6 +250,8 @@ Definition eval_operation | Omodu, v1 :: v2 :: nil => Val.modu v1 v2 | Oand, v1 :: v2 :: nil => Some (Val.and v1 v2) | Oandimm n, v1 :: nil => Some (Val.and v1 (Vint n)) + | Onand, v1 :: v2 :: nil => Some (Val.notint (Val.and v1 v2)) + | Onandimm n, v1 :: nil => Some (Val.notint (Val.and v1 (Vint n))) | Oor, v1 :: v2 :: nil => Some (Val.or v1 v2) | Oorimm n, v1 :: nil => Some (Val.or v1 (Vint n)) | Oxor, v1 :: v2 :: nil => Some (Val.xor v1 v2) @@ -405,6 +409,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Omodu => (Tint :: Tint :: nil, Tint) | Oand => (Tint :: Tint :: nil, Tint) | Oandimm _ => (Tint :: nil, Tint) + | Onand => (Tint :: Tint :: nil, Tint) + | Onandimm _ => (Tint :: nil, Tint) | Oor => (Tint :: Tint :: nil, Tint) | Oorimm _ => (Tint :: nil, Tint) | Oxor => (Tint :: Tint :: nil, Tint) @@ -552,6 +558,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* and, andimm *) - destruct v0; destruct v1... - destruct v0... + (* nand, nandimm *) + - destruct v0; destruct v1... + - destruct v0... (* or, orimm *) - destruct v0; destruct v1... - destruct v0... @@ -1016,6 +1025,9 @@ Proof. (* and, andimm *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. + (* nand, nandimm *) + - inv H4; inv H2; simpl; auto. + - inv H4; simpl; auto. (* or, orimm *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 26a49135..a78857b3 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -65,6 +65,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omodu, v1::v2::nil => modu v1 v2 | Oand, v1::v2::nil => and v1 v2 | Oandimm n, v1::nil => and v1 (I n) + | Onand, v1::v2::nil => notint (and v1 v2) + | Onandimm n, v1::nil => notint (and v1 (I n)) | Oor, v1::v2::nil => or v1 v2 | Oorimm n, v1::nil => or v1 (I n) | Oxor, v1::v2::nil => xor v1 v2 |