diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 16:16:42 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 16:16:42 +0100 |
| commit | 0d66eae95a8905ff985cd4738808fc93215a4904 (patch) | |
| tree | fb3fc30d85ed470e8d6d5a925e3a23016c6e3061 /mppa_k1c/Op.v | |
| parent | 1b1577c372c71a11831feb043e3b050deb60ba99 (diff) | |
| download | compcert-kvx-0d66eae95a8905ff985cd4738808fc93215a4904.tar.gz compcert-kvx-0d66eae95a8905ff985cd4738808fc93215a4904.zip | |
nand debut
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 12 |
1 files changed, 12 insertions, 0 deletions
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. |