diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 11:00:56 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 11:00:56 +0100 |
| commit | 456787ab7f394e15b3b0481f4d4178ebf04259c7 (patch) | |
| tree | bb60e8ec5ff950a49a4cafa9264000be1c0747e3 /mppa_k1c | |
| parent | fbe5ac2c9619441ad84dedf3c0cdabb315f9f974 (diff) | |
| download | compcert-kvx-456787ab7f394e15b3b0481f4d4178ebf04259c7.tar.gz compcert-kvx-456787ab7f394e15b3b0481f4d4178ebf04259c7.zip | |
instruction rotate
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/NeedOp.v | 1 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 2 |
2 files changed, 3 insertions, 0 deletions
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 117bbcb4..28d60fa5 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -54,6 +54,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshl | Oshr | Oshru => op2 (default nv) | Oshlimm n => op1 (shlimm nv n) | Oshrimm n => op1 (shrimm nv n) + | Ororimm n => op1 (ror nv n) | Oshruimm n => op1 (shruimm nv n) | Oshrximm n => op1 (default nv) | Omakelong => op2 (default nv) diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 74101f53..e91c6ae1 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -89,6 +89,7 @@ Inductive operation : Type := | Oshru (**r [rd = r1 >> r2] (unsigned) *) | Oshruimm (n: int) (**r [rd = r1 >> n] (unsigned) *) | Oshrximm (n: int) (**r [rd = r1 / 2^n] (signed) *) + | Ororimm (n: int) (**r rotate right immediate *) (*c 64-bit integer arithmetic: *) | Omakelong (**r [rd = r1 << 32 | r2] *) | Olowlong (**r [rd = low-word(r1)] *) @@ -414,6 +415,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshru => (Tint :: Tint :: nil, Tint) | Oshruimm _ => (Tint :: nil, Tint) | Oshrximm _ => (Tint :: nil, Tint) + | Ororimm _ => (Tint :: nil, Tint) | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) | Ohighlong => (Tlong :: nil, Tint) |