diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-29 09:17:26 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-29 09:17:26 +0200 |
| commit | 2e39ecb491bbd001ecdfba73115bc76e3f53f517 (patch) | |
| tree | 7925ef9241e8b6d2a42dafe979010230ad36a84f /kvx/Asm.v | |
| parent | 1bb219c2df5f7b06227a2bddfc24721a372847ab (diff) | |
| download | compcert-kvx-2e39ecb491bbd001ecdfba73115bc76e3f53f517.tar.gz compcert-kvx-2e39ecb491bbd001ecdfba73115bc76e3f53f517.zip | |
Improving the coqdoc
Diffstat (limited to 'kvx/Asm.v')
| -rw-r--r-- | kvx/Asm.v | 10 |
1 files changed, 6 insertions, 4 deletions
@@ -13,7 +13,7 @@ (* *) (* *************************************************************) -(** * Abstract syntax for KVX textual assembly language. +(** Abstract syntax for KVX textual assembly language. Each emittable instruction is defined here. ';;' is also defined as an instruction. The goal of this representation is to stay compatible with the rest of the generic backend of CompCert @@ -49,7 +49,7 @@ Inductive addressing : Type := | ARegXS (ro: ireg) . -(** Syntax *) +(** * Syntax *) Inductive instruction : Type := (** pseudo instructions *) | Pallocframe (sz: Z) (pos: ptrofs) (**r allocate new stack frame *) @@ -104,7 +104,7 @@ Inductive instruction : Type := | Pclzll (rd rs: ireg) | Pstsud (rd rs1 rs2: ireg) - (** Loads **) + (** Loads *) | Plb (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *) | Plbu (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte unsigned *) | Plh (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load half word *) @@ -118,7 +118,7 @@ Inductive instruction : Type := | Plq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (**r load 2*64-bit *) | Plo (rs: gpreg_o) (ra: ireg) (ofs: addressing) (**r load 4*64-bit *) - (** Stores **) + (** Stores *) | Psb (rs: ireg) (ra: ireg) (ofs: addressing) (**r store byte *) | Psh (rs: ireg) (ra: ireg) (ofs: addressing) (**r store half byte *) | Psw (rs: ireg) (ra: ireg) (ofs: addressing) (**r store int32 *) @@ -547,6 +547,8 @@ Definition basic_to_instruction (b: basic) := | PStoreORRO qrs ra ofs => Pso qrs ra (AOff ofs) end. +(** * Semantics (given through the existence of well-formed VLIW program) *) + Section RELSEM. Definition code := list instruction. |