Improving the coqdoc

1 files changed, 88 insertions, 130 deletions

diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v
index 301ee69a..296963a7 100644
--- a/kvx/Asmvliw.v
+++ b/kvx/Asmvliw.v
@@ -41,7 +41,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
@@ -165,7 +165,7 @@ End PregEq.
 
 Module Pregmap := EMap(PregEq).
 
-(** Conventional names for stack pointer ([SP]), return address ([RA]), frame pointer ([FP]) and other temporaries used *)
+(** ** 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.
@@ -173,6 +173,8 @@ Notation "'MFP'" := R17 (only parsing) : asm.
 Notation "'GPRA'" := GPR16 (only parsing) : asm.
 Notation "'RTMP'" := GPR32 (only parsing) : asm.
 
+(** ** Names of tests in comparisons *)
+
 Inductive btest: Type :=
   | BTdnez                              (**r Double Not Equal to Zero *)
   | BTdeqz                              (**r Double Equal to Zero *)
@@ -214,55 +216,47 @@ Inductive ftest: Type :=
   | FTult                               (**r Unordered or Less Than *)
   .
 
-(** Offsets for load and store instructions.  An offset is either an
-  immediate integer or the low part of a symbol. *)
+(** *** Offsets for load and store instructions. *)
 
 Definition offset : Type := ptrofs.
 
-(** We model a subset of the KVX instruction set. In particular, we do not
-  support floats yet.
+(** *** Labels for goto (in the current function) *)
 
-  Although it is possible to use the 32-bits mode, for now we don't support it.
+Definition label := positive.
 
-  We follow a design close to the one used for the Risc-V port: one set of
-  pseudo-instructions for 32-bit integer arithmetic, with suffix W, another
-  set for 64-bit integer arithmetic, with suffix L.
+(** ** Instructions *)
+
+(** We model a subset of the KVX instruction set.
 
-  When mapping to actual instructions, the OCaml code in TargetPrinter.ml
+-  Although it is possible to use the 32-bits mode, for now we don't support it. When mapping to actual instructions, the OCaml code in TargetPrinter.ml
   throws an error if we are not in 64-bits mode.
-*)
 
-(** * Instructions *)
+- We follow a design close to the one used for the Risc-V port: one set of
+  pseudo-instructions for 32-bit integer arithmetic, with suffix W, another
+  set for 64-bit integer arithmetic, with suffix L.
 
-Definition label := positive.
+- With respect to other CompCert assemblies, we define a type hierarchy of instructions (instead of a flat type).
+  This helps us to factorize similar cases for the scheduling verifier.
+
+*)
 
-(** 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)
               -> builtin_res preg -> ex_instruction   (**r built-in function (pseudo) *)
 .
 
-(** FIXME: comment not up to date !
-
-
- The pseudo-instructions are the following:
+(** Similarly to other CompCert assembly languages, the pseudo-instructions are the following:
 
 - [Ploadsymbol]: load the address of a symbol in an integer register.
-  Expands to the [la] assembler pseudo-instruction, which does the right
-  thing even if we are in PIC mode.
 
 - [Pallocframe sz pos]: in the formal semantics, this
   pseudo-instruction allocates a memory block with bounds [0] and
   [sz], stores the value of the stack pointer at offset [pos] in this
   block, and sets the stack pointer to the address of the bottom of
   this block.
-  In the printed ASM assembly code, this allocation is:
-<<
-        mv      x30, sp
-        sub     sp,  sp, #sz
-        sw      x30, #pos(sp)
->>
+
   This cannot be expressed in our memory model, which does not reflect
   the fact that stack frames are adjacent and allocated/freed
   following a stack discipline.
@@ -270,25 +264,13 @@ Inductive ex_instruction : Type :=
 - [Pfreeframe sz pos]: in the formal semantics, this pseudo-instruction
   reads the word at [pos] of the block pointed by the stack pointer,
   frees this block, and sets the stack pointer to the value read.
-  In the printed ASM assembly code, this freeing is just an increment of [sp]:
-<<
-        add     sp,  sp, #sz
->>
   Again, our memory model cannot comprehend that this operation
   frees (logically) the current stack frame.
 
 - [Pbtbl reg table]: this is a N-way branch, implemented via a jump table
-  as follows:
-<<
-        la      x31, table
-        add     x31, x31, reg
-        jr      x31
-table:  .long   table[0], table[1], ...
->>
-  Note that [reg] contains 4 times the index of the desired table entry.
 *)
 
-(** Control Flow instructions *)
+(** *** Control Flow instructions *)
 Inductive cf_instruction : Type :=
   | Pret                                            (**r return *)
   | Pcall   (l: label)                              (**r function call *)
@@ -305,7 +287,7 @@ Inductive cf_instruction : Type :=
   | Pcbu    (bt: btest) (r: ireg) (l: label)        (**r branch based on btest with unsigned semantics *)
 .
 
-(** Loads **)
+(** *** Loads *)
 Definition concrete_default_notrap_load_value (chunk : memory_chunk) :=
   match chunk with
   | Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned
@@ -337,7 +319,7 @@ Inductive ld_instruction : Type :=
   | PLoadORRO  (rd: gpreg_o) (ra: ireg) (ofs: offset)
 .
 
-(** Stores **)
+(** *** Stores *)
 Inductive store_name : Type :=
   | Psb                                             (**r store byte *)
   | Psh                                             (**r store half byte *)
@@ -357,7 +339,7 @@ Inductive st_instruction : Type :=
   | PStoreORRO (rs: gpreg_o) (ra: ireg) (ofs: offset)
 .
 
-(** Arithmetic instructions **)
+(** *** Arithmetic instructions *)
 Inductive arith_name_r : Type :=
   | Ploadsymbol (id: ident) (ofs: ptrofs)           (**r load the address of a symbol *)
 .
@@ -571,6 +553,8 @@ Coercion PArithARRI64:   arith_name_arri64    >-> Funclass.
 
 End PArithCoercions.
 
+(** ** Basic instructions *)
+
 Inductive basic : Type :=
   | PArith          (i: ar_instruction)
   | PLoad           (i: ld_instruction)
@@ -586,6 +570,7 @@ Coercion PLoad:         ld_instruction >-> basic.
 Coercion PStore:        st_instruction >-> basic.
 Coercion PArith:        ar_instruction >-> basic.
 
+(** ** Control-flow instructions *)
 
 Inductive control : Type :=
   | PExpand         (i: ex_instruction)
@@ -596,9 +581,9 @@ Coercion PExpand:   ex_instruction >-> control.
 Coercion PCtlFlow:  cf_instruction >-> control.
 
 
-(** * Definition of a bblock (ie a bundle)
+(** * Definition of a bblock (ie a bundle) *)
 
-A bundle/bblock must contain at least one instruction.
+(** A bundle/bblock must contain at least one instruction.
 
 This choice simplifies the definition of [find_bblock] below:
 indeed, each address of a code block identifies at most one bundle
@@ -621,9 +606,8 @@ Definition non_empty_exit (exit: option control): bool :=
 Definition non_empty_bblockb (body: list basic) (exit: option control): bool := non_empty_body body || non_empty_exit exit.
 
 
-(** TODO
- * For now, we consider a builtin is alone in a bundle (and a basic block).
- * Is there a way to avoid that ?
+(** For now, we consider a builtin is alone in a bundle (and a basic block).
+    Is there a way to avoid that ? (TODO)
  *)
 Definition builtin_aloneb (body: list basic) (exit: option control) :=
   match exit with
@@ -655,12 +639,12 @@ Definition length_opt {A} (o: option A) : nat :=
   | None => 0
   end.
 
-(* WARNING: the notion of size is not the same than in Machblock !
-   We ignore labels here...
+(** The notion of size induces the notion of "valid" code address given by [find_bblock]
+    The result is in Z to be compatible with operations on PC. 
 
-   This notion of size induces the notion of "valid" code address given by [find_bblock]
+    WARNING: this notion of size is not the same than in Machblock !
+    We ignore labels here...
 
-   The result is in Z to be compatible with operations on PC.
 *)
 Definition size (b:bblock): Z := Z.of_nat (length (body b) + length_opt (exit b)).
 
@@ -678,7 +662,7 @@ Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
 Definition fundef := AST.fundef function.
 Definition program := AST.program fundef unit.
 
-(** * Operational semantics *)
+(** * Parallel Semantics of bundles *)
 
 (** The semantics operates over a single mapping from registers
   (type [preg]) to values.  We maintain
@@ -695,7 +679,7 @@ Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm
 
 Open Scope asm.
 
-(** Undefining some registers *)
+(** *** Undefining some registers *)
 
 Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
   match l with
@@ -704,7 +688,7 @@ Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
   end.
 
 
-(** Assigning a register pair *)
+(** *** Assigning a register pair *)
 Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
   match p with
   | One r => rs#r <- v
@@ -712,7 +696,7 @@ Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
   end.
 
 
-(** Assigning the result of a builtin *)
+(** *** Assigning the result of a builtin *)
 
 Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   match res with
@@ -723,12 +707,8 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
 
 Local Open Scope asm.
 
-(** * Parallel Semantics of bundles *)
-
 Section RELSEM.
 
-(** Execution of arith instructions *)
-
 Variable ge: genv.
 
 (** The parallel semantics on bundles is purely small-step and defined as a relation
@@ -753,7 +733,7 @@ Inductive outcome: Type :=
   | Stuck
 .
 
-(** ** Arithmetic Expressions (including comparisons) *)
+(** *** Arithmetic Expressions (including comparisons) *)
 
 Inductive signedness: Type := Signed | Unsigned.
 
@@ -800,7 +780,7 @@ Definition notftest_for_cmp (c: comparison) :=
   | Cge => Normal FTult
   end.
 
-(* CoMPare Signed Words to Zero *)
+(* **** CoMPare Signed Words to Zero *)
 Definition btest_for_cmpswz (c: comparison) :=
   match c with
   | Cne => BTwnez
@@ -811,7 +791,7 @@ Definition btest_for_cmpswz (c: comparison) :=
   | Cgt => BTwgtz
   end.
 
-(* CoMPare Signed Doubles to Zero *)
+(* **** CoMPare Signed Doubles to Zero *)
 Definition btest_for_cmpsdz (c: comparison) :=
   match c with
   | Cne => BTdnez
@@ -849,7 +829,7 @@ Definition cmpu_for_btest (bt: btest) :=
   end.
 
 
-(* a few lemma on comparisons of unsigned (e.g. pointers) *)
+(* **** a few lemma on comparisons of unsigned (e.g. pointers) *)
 
 Definition Val_cmpu_bool cmp v1 v2: option bool :=
   Val.cmpu_bool (fun _ _ => true) cmp v1 v2.
@@ -901,7 +881,7 @@ Qed.
 
 
 
-(** Comparing integers *)
+(** **** Comparing integers *)
 Definition compare_int (t: itest) (v1 v2: val): val :=
   match t with
   | ITne  => Val.cmp Cne v1 v2
@@ -961,6 +941,8 @@ Definition compare_float (t: ftest) (v1 v2: val): val :=
   | FTult => Val.notbool (Val.cmpf Cge v1 v2)
   end.
 
+(** **** Arithmetic evaluators *)
+
 Definition arith_eval_r n :=
   match n with
   | Ploadsymbol s ofs => Genv.symbol_address ge s ofs
@@ -1212,7 +1194,7 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
 
 Definition eval_offset (ofs: offset) : res ptrofs := OK ofs.
 
-(** * load/store *)
+(** *** load/store instructions *)
 
 Definition parexec_incorrect_load trap chunk d rsw mw :=
   match trap with
@@ -1361,7 +1343,7 @@ Definition store_chunk n :=
   | Pfsd => Mfloat64
   end.
 
-(** * basic instructions *)
+(** ** Basic (instruction) step *)
 
 Definition bstep (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
   match bi with
@@ -1417,7 +1399,7 @@ Definition bstep (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
   | Pnop => Next rsw mw
 end.
 
-(* parexec with writes-in-order *)
+(** *** parexec with writes-in-order *)
 Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) :=
   match body with
   | nil => Next rsw mw
@@ -1428,7 +1410,7 @@ Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) :=
      end
   end.
 
-(** TODO: redundant w.r.t Machblock ?? *)
+(* TODO: redundant w.r.t Machblock ?? *)
 Lemma in_dec (lbl: label) (l: list label):  { List.In lbl l } + { ~(List.In lbl l) }.
 Proof.
   apply List.in_dec.
@@ -1437,7 +1419,7 @@ Qed.
 
 
 
-(** Note: copy-paste from Machblock *)
+(* Note: copy-paste from Machblock *)
 Definition is_label (lbl: label) (bb: bblock) : bool :=
   if in_dec lbl (header bb) then true else false.
 
@@ -1455,7 +1437,7 @@ Qed.
 
 
 
-(** convert a label into a position in the code *)
+(** **** convert a label into a position in the code *)
 Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z :=
   match lb with
   | nil => None
@@ -1472,11 +1454,9 @@ Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem)
       end
   end.
 
-(** Evaluating a branch 
+(** **** Parallel Evaluation of a branch *)
 
-Warning: in m PC is assumed to be already pointing on the next instruction !
-
-*)
+(** Warning: PC is assumed to be already pointing on the next bundle ! *)
 
 Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem) (res: option bool) :=
   match res with
@@ -1486,72 +1466,54 @@ Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem)
   end.
 
 
-(* FIXME: comment not up-to-date for parallel semantics *)
-
-(** Execution of a single control-flow instruction [i] in initial state [rs] and
-    [m].  Return updated state.
-
-    As above: PC is assumed to be incremented on the next block before the control-flow instruction
-
-    For instructions that correspond tobuiltin
-    actual RISC-V instructions, the cases are straightforward
-    transliterations of the informal descriptions given in the RISC-V
-    user-mode specification.  For pseudo-instructions, refer to the
-    informal descriptions given above.
+(** **** Parallel execution of a control-flow instruction  *)
 
-    Note that we set to [Vundef] the registers used as temporaries by
-    the expansions of the pseudo-instructions, so that the RISC-V code
-    we generate cannot use those registers to hold values that must
-    survive the execution of the pseudo-instruction. *)
+(**  As above: PC is assumed to be incremented on the next block before the control-flow instruction
+*)
 
 Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) (mw: mem) :=
   match oc with
-  | Some ic =>
-(** Get/Set system registers *)
-  match ic with
-
-
-(** Branch Control Unit instructions *)
-  | Pret =>
+  | None => Next (rsw#PC <- (rsr#PC)) mw
+  | Some ic => (**r Branch Control Unit instructions *)
+    match ic with
+    | Pret =>
       Next (rsw#PC <- (rsr#RA)) mw
-  | Pcall s =>
+    | Pcall s =>
       Next (rsw#RA <- (rsr#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw
-  | Picall r =>
+    | Picall r =>
       Next (rsw#RA <- (rsr#PC) #PC <- (rsr#r)) mw
-  | Pjumptable r tbl =>
+    | Pjumptable r tbl =>
       match rsr#r with
       | Vint n =>
-          match list_nth_z tbl (Int.unsigned n) with
-          | None => Stuck
-          | Some lbl => par_goto_label f lbl rsr (rsw #GPR62 <- Vundef #GPR63 <- Vundef) mw
-          end
+        match list_nth_z tbl (Int.unsigned n) with
+        | None => Stuck
+        | Some lbl => par_goto_label f lbl rsr (rsw #GPR62 <- Vundef #GPR63 <- Vundef) mw
+        end
       | _ => Stuck
       end
-  | Pgoto s =>
+    | Pgoto s =>
       Next (rsw#PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw
-  | Pigoto r =>
+    | Pigoto r =>
       Next (rsw#PC <- (rsr#r)) mw
-  | Pj_l l =>
+    | Pj_l l =>
       par_goto_label f l rsr rsw mw
-  | Pcb bt r l =>
+    | Pcb bt r l =>
       match cmp_for_btest bt with
       | (Some c, Int)  => par_eval_branch f l rsr rsw mw (Val.cmp_bool c rsr#r (Vint (Int.repr 0)))
       | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val.cmpl_bool c rsr#r (Vlong (Int64.repr 0)))
       | (None, _) => Stuck
       end
-  | Pcbu bt r l => 
+    | Pcbu bt r l => 
       match cmpu_for_btest bt with
       | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val_cmpu_bool c rsr#r (Vint (Int.repr 0)))
       | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val_cmplu_bool c rsr#r (Vlong (Int64.repr 0)))
       | (None, _) => Stuck
       end
-
-(** Pseudo-instructions *)
-  | Pbuiltin ef args res =>
+    (**r Pseudo-instructions *)
+    | Pbuiltin ef args res =>
       Stuck (**r treated specially below *)
-  end
-  | None => Next (rsw#PC <- (rsr#PC)) mw
-end.
+    end
+  end.
 
 
 Definition incrPC size_b (rs: regset) :=
@@ -1567,7 +1529,7 @@ Definition parexec_wio f bdy ext size_b (rs: regset) (m: mem): outcome :=
   | Stuck => Stuck
   end.
 
-(** non-deterministic (out-of-order writes) parallel execution of bundles *)
+(** *** non-deterministic (out-of-order writes) parallel execution of bundles *)
 Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (o: outcome): Prop :=
    exists bdy1 bdy2, Permutation (bdy1++bdy2) (body bundle) /\ 
       o=match parexec_wio f bdy1 (exit bundle) (Ptrofs.repr (size bundle)) rs m with
@@ -1575,14 +1537,13 @@ Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (
       | Stuck => Stuck
       end.
 
-(** deterministic parallel (out-of-order writes) execution of bundles *)
+(** *** deterministic parallel (out-of-order writes) execution of bundles *)
 Definition det_parexec (f: function) (bundle: bblock) (rs: regset) (m: mem) rs' m': Prop :=
    forall o, parexec_bblock f bundle rs m o -> o = Next rs' m'.
 
 
-(* FIXME: comment not up-to-date *)
-(** Translation of the LTL/Linear/Mach view of machine registers to
-  the RISC-V view.  Note that no LTL register maps to [X31].  This
+(** *** Translation of the LTL/Linear/Mach view of machine registers to
+  the assembly view.  Note that no LTL register maps to [X31].  This
   register is reserved as temporary, to be used by the generated RV32G
   code.  *)
 
@@ -1605,7 +1566,7 @@ Definition preg_of (r: mreg) : preg :=
   | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63
   end.
 
-(** Undefine all registers except SP and callee-save registers *)
+(** **** Undefine all registers except SP and callee-save registers *)
 
 Definition undef_caller_save_regs (rs: regset) : regset :=
   fun r =>
@@ -1614,10 +1575,9 @@ Definition undef_caller_save_regs (rs: regset) : regset :=
     then rs r
     else Vundef.
 
-(* FIXME: comment not up-to-date *)
-(** Extract the values of the arguments of an external call.
+(** **** Extract the values of the arguments of an external call.
     We exploit the calling conventions from module [Conventions], except that
-    we use RISC-V registers instead of locations. *)
+    we use assembly registers instead of locations. *)
 
 Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
   | extcall_arg_reg: forall r,
@@ -1646,12 +1606,12 @@ Definition loc_external_result (sg: signature) : rpair preg :=
   map_rpair preg_of (loc_result sg).
 
 
-(** Looking up bblocks in a code sequence by position. *)
+(** ** Looking up bblocks in a code sequence by position. *)
 Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock :=
   match lb with
   | nil => None
   | b :: il => 
-    if zlt pos 0 then None  (* NOTE: It is impossible to branch inside a block *)
+    if zlt pos 0 then None  (*r NOTE: It is impossible to branch inside a block *)
     else if zeq pos 0 then Some b
     else find_bblock (pos - (size b)) il
   end.
@@ -1721,9 +1681,7 @@ Qed.
 
 End RELSEM.
 
-(** Execution of whole programs. *)
-
-(** Execution of whole programs. *)
+(** ** Execution of whole programs. *)
 
 Inductive initial_state (p: program): state -> Prop :=
   | initial_state_intro: forall m0,