From 2e39ecb491bbd001ecdfba73115bc76e3f53f517 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 29 Jul 2020 09:17:26 +0200 Subject: Improving the coqdoc --- kvx/Asm.v | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'kvx/Asm.v') diff --git a/kvx/Asm.v b/kvx/Asm.v index 69d0ecf6..30aafc55 100644 --- a/kvx/Asm.v +++ b/kvx/Asm.v @@ -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. -- cgit