diff options
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 33 |
1 files changed, 8 insertions, 25 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index c5b7db45..72584d2a 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -17,8 +17,6 @@ (** Abstract syntax and semantics for VLIW semantics of K1c assembly language. *) -(* FIXME: develop/fix the comments in this file *) - Require Import Coqlib. Require Import Maps. Require Import AST. @@ -45,8 +43,7 @@ Require Import Chunks. this view induces our sequential semantics of bundles defined in [Asmblock]. *) -(** General Purpose registers. -*) +(** General Purpose registers. *) Inductive gpreg: Type := | GPR0: gpreg | GPR1: gpreg | GPR2: gpreg | GPR3: gpreg | GPR4: gpreg @@ -152,9 +149,6 @@ Definition gpreg_o_expand (x : gpreg_o) : gpreg * gpreg * gpreg * gpreg := Lemma gpreg_o_eq : forall (x y : gpreg_o), {x=y} + {x<>y}. Proof. decide equality. Defined. -(** We model the following registers of the RISC-V architecture. *) - -(** basic register *) Inductive preg: Type := | IR: gpreg -> preg (**r integer general purpose registers *) | RA: preg @@ -173,7 +167,7 @@ End PregEq. Module Pregmap := EMap(PregEq). -(** Conventional names for stack pointer ([SP]) and return address ([RA]). *) +(** Conventional names for stack pointer ([SP]), return address ([RA]), frame pointer ([FP]) and other temporaries used *) Notation "'SP'" := GPR12 (only parsing) : asm. Notation "'FP'" := GPR17 (only parsing) : asm. @@ -188,9 +182,7 @@ Inductive btest: Type := | BTdgez (**r Double Greater Than or Equal to Zero *) | BTdlez (**r Double Less Than or Equal to Zero *) | BTdgtz (**r Double Greater Than Zero *) -(*| BTodd (**r Odd (LSB Set) *) - | BTeven (**r Even (LSB Clear) *) -*)| BTwnez (**r Word Not Equal to Zero *) + | BTwnez (**r Word Not Equal to Zero *) | BTweqz (**r Word Equal to Zero *) | BTwltz (**r Word Less Than Zero *) | BTwgez (**r Word Greater Than or Equal to Zero *) @@ -251,16 +243,7 @@ Definition offset : Type := ptrofs. Definition label := positive. -(* FIXME - rewrite the comment *) -(** A note on immediates: there are various constraints on immediate - operands to K1c instructions. We do not attempt to capture these - restrictions in the abstract syntax nor in the semantics. The - assembler will emit an error if immediate operands exceed the - representable range. Of course, our K1c generator (file - [Asmgen]) is careful to respect this range. *) - -(** Instructions to be expanded in control-flow -*) +(** Instructions to be expanded in control-flow *) Inductive ex_instruction : Type := (* Pseudo-instructions *) | Pbuiltin: external_function -> list (builtin_arg preg) @@ -1355,7 +1338,7 @@ Definition store_chunk n := (** * basic instructions *) -Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) := +Definition bstep (bi: basic) (rsr rsw: regset) (mr mw: mem) := match bi with | PArith ai => Next (parexec_arith_instr ai rsr rsw) mw @@ -1414,7 +1397,7 @@ Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) := match body with | nil => Next rsw mw | bi::body' => - match parexec_basic_instr bi rsr rsw mr mw with + match bstep bi rsr rsw mr mw with | Next rsw mw => parexec_wio_body body' rsr rsw mr mw | Stuck => Stuck end @@ -1550,12 +1533,12 @@ Definition incrPC size_b (rs: regset) := rs#PC <- (Val.offset_ptr rs#PC size_b). (** parallel execution of the exit instruction of a bundle *) -Definition parexec_exit (f: function) ext size_b (rsr rsw: regset) (mw: mem) +Definition estep (f: function) ext size_b (rsr rsw: regset) (mw: mem) := parexec_control f ext (incrPC size_b rsr) rsw mw. Definition parexec_wio f bdy ext size_b (rs: regset) (m: mem): outcome := match parexec_wio_body bdy rs rs m m with - | Next rsw mw => parexec_exit f ext size_b rs rsw mw + | Next rsw mw => estep f ext size_b rs rsw mw | Stuck => Stuck end. |