diff options
| -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) |