diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 18:24:03 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 18:24:03 +0100 |
| commit | 4e3b46ca2a30abf520672f4b1a28f91f171f6e7e (patch) | |
| tree | 044fd5393f5fa563cfc85e7e60a00621d18044da /mppa_k1c/Op.v | |
| parent | fb02f9116621a0bcb9bb2c334ad782fee5887d0e (diff) | |
| download | compcert-kvx-4e3b46ca2a30abf520672f4b1a28f91f171f6e7e.tar.gz compcert-kvx-4e3b46ca2a30abf520672f4b1a28f91f171f6e7e.zip | |
nor implemente
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 8c5f01cd..275613bb 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -82,6 +82,8 @@ Inductive operation : Type := | Onandimm (n: int) (**r [rd = ~(r1 & n)] *) | Oor (**r [rd = r1 | r2] *) | Oorimm (n: int) (**r [rd = r1 | n] *) + | Onor (**r [rd = r1 | r2] *) + | Onorimm (n: int) (**r [rd = r1 | n] *) | Oxor (**r [rd = r1 ^ r2] *) | Oxorimm (n: int) (**r [rd = r1 ^ n] *) | Oshl (**r [rd = r1 << r2] *) @@ -254,6 +256,8 @@ Definition eval_operation | 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)) + | Onor, v1 :: v2 :: nil => Some (Val.notint (Val.or v1 v2)) + | Onorimm n, v1 :: nil => Some (Val.notint (Val.or v1 (Vint n))) | Oxor, v1 :: v2 :: nil => Some (Val.xor v1 v2) | Oxorimm n, v1 :: nil => Some (Val.xor v1 (Vint n)) | Oshl, v1 :: v2 :: nil => Some (Val.shl v1 v2) @@ -413,6 +417,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Onandimm _ => (Tint :: nil, Tint) | Oor => (Tint :: Tint :: nil, Tint) | Oorimm _ => (Tint :: nil, Tint) + | Onor => (Tint :: Tint :: nil, Tint) + | Onorimm _ => (Tint :: nil, Tint) | Oxor => (Tint :: Tint :: nil, Tint) | Oxorimm _ => (Tint :: nil, Tint) | Oshl => (Tint :: Tint :: nil, Tint) @@ -564,6 +570,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* or, orimm *) - destruct v0; destruct v1... - destruct v0... + (* nor, norimm *) + - destruct v0; destruct v1... + - destruct v0... (* xor, xorimm *) - destruct v0; destruct v1... - destruct v0... @@ -1031,6 +1040,9 @@ Proof. (* or, orimm *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. + (* nor, norimm *) + - inv H4; inv H2; simpl; auto. + - inv H4; simpl; auto. (* xor, xorimm *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. |