diff options
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 27 |
1 files changed, 6 insertions, 21 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 008e6c67..df394ecf 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -166,6 +166,9 @@ Inductive ex_instruction : Type := | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) *) | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *) + (* Instructions not generated by Asmgen (most likely result of AsmExpand) *) + | Pclzll (rd rs: ireg) + | Pstsud (rd rs1 rs2: ireg) . (** The pseudo-instructions are the following: @@ -1053,28 +1056,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) -(*| Pfence - - | Pfmvxs _ _ - | Pfmvxd _ _ - - | Pfmins _ _ _ - | Pfmaxs _ _ _ - | Pfsqrts _ _ - | Pfmadds _ _ _ _ - | Pfmsubs _ _ _ _ - | Pfnmadds _ _ _ _ - | Pfnmsubs _ _ _ _ - - | Pfmind _ _ _ - | Pfmaxd _ _ _ - | Pfsqrtd _ _ - | Pfmaddd _ _ _ _ - | Pfmsubd _ _ _ _ - | Pfnmaddd _ _ _ _ - | Pfnmsubd _ _ _ _ + | Pclzll _ _ + | Pstsud _ _ _ => Stuck -*)end. + end. (** Translation of the LTL/Linear/Mach view of machine registers to the RISC-V view. Note that no LTL register maps to [X31]. This |