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/Asmvliw.v | 218 ++++++++++++++++++++++++---------------------------------- 1 file changed, 88 insertions(+), 130 deletions(-) (limited to 'kvx/Asmvliw.v') 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, -- cgit