diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-10 16:21:23 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-10 16:21:23 +0200 |
commit | 2e54a9c599ef13e4fe84ec80fac4c1835a052241 (patch) | |
tree | 83c9c98a5ed41f1447edd4089fb9850281bd139e /kvx | |
parent | 0566b93d9e42ab023eb95a4535af0c3a86b0421c (diff) | |
parent | 8d1c157bf4f262de656abfee51afd2f56f8127db (diff) | |
download | compcert-kvx-2e54a9c599ef13e4fe84ec80fac4c1835a052241.tar.gz compcert-kvx-2e54a9c599ef13e4fe84ec80fac4c1835a052241.zip |
Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif-hash-junk
Diffstat (limited to 'kvx')
-rw-r--r-- | kvx/Asm.v | 10 | ||||
-rw-r--r-- | kvx/Asmblockdeps.v | 23 | ||||
-rw-r--r-- | kvx/Asmgenproof.v | 7 | ||||
-rw-r--r-- | kvx/Asmvliw.v | 218 | ||||
-rw-r--r-- | kvx/PostpassScheduling.v | 19 | ||||
-rw-r--r-- | kvx/PostpassSchedulingOracle.ml | 27 | ||||
-rw-r--r-- | kvx/abstractbb/AbstractBasicBlocksDef.v | 44 | ||||
-rw-r--r-- | kvx/abstractbb/ImpSimuTest.v | 30 | ||||
-rw-r--r-- | kvx/abstractbb/Parallelizability.v | 25 | ||||
-rw-r--r-- | kvx/abstractbb/SeqSimuTheory.v | 21 | ||||
-rw-r--r-- | kvx/lib/Machblock.v | 15 | ||||
-rw-r--r-- | kvx/lib/Machblockgen.v | 13 |
12 files changed, 230 insertions, 222 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. diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v index 1881e7e9..3d981100 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -12,12 +12,14 @@ (* *) (* *************************************************************) -(** * Translation from Asmblock to AbstractBB +(** * Translation from [Asmvliw] to [AbstractBB] *) - We define a specific instance of AbstractBB, named L, translate bblocks from Asmblock into this instance - AbstractBB will then define two semantics for L : a sequential, and a semantic one - We prove a bisimulation between the parallel semantics of L and AsmVLIW - From this, we also deduce a bisimulation between the sequential semantics of L and Asmblock *) +(** We define a specific instance [L] of [AbstractBB] and translate [bblocks] from [Asmvliw] into [L]. + [AbstractBB] will then define two semantics for [L]: a sequential and a parallel one. + We prove a bisimulation between the parallel semantics of [L] and [AsmVLIW]. + We also prove a bisimulation between the sequential semantics of [L] and [Asmblock]. + Then, the checkers on [Asmblock] and [Asmvliw] are deduced from those of [L]. + *) Require Import AST. Require Import Asmblock. @@ -40,7 +42,7 @@ Require Import Lia. Open Scope impure. -(** Definition of L *) +(** Definition of [L] *) Module P<: ImpParam. Module R := Pos. @@ -660,7 +662,7 @@ Module IST := ImpSimu L ImpPosDict. Import L. Import P. -(** Compilation from Asmblock to L *) +(** Compilation from [Asmvliw] to [L] *) Local Open Scope positive_scope. @@ -748,6 +750,8 @@ Definition inv_ppos (p: R.t) : option preg := Notation "a @ b" := (Econs a b) (at level 102, right associativity). +(** Translations of instructions *) + Definition trans_control (ctl: control) : inst := match ctl with | Pret => [(#PC, PReg(#RA))] @@ -859,6 +863,8 @@ Proof. intros. destruct bb as [hdr bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity. Qed. +(** Lemmas on the translation *) + Definition state := L.mem. Definition exec := L.run. @@ -1800,6 +1806,7 @@ Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool := Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp. +(** Main simulation (Impure) theorem *) Theorem bblock_simu_test_correct verb p1 p2 : WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockprops.bblock_simu ge fn p1 p2. Proof. @@ -1807,7 +1814,7 @@ Proof. Qed. Hint Resolve bblock_simu_test_correct: wlp. -(* Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *) +(** ** Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *) Import UnsafeImpure. diff --git a/kvx/Asmgenproof.v b/kvx/Asmgenproof.v index f43acd37..9e35e268 100644 --- a/kvx/Asmgenproof.v +++ b/kvx/Asmgenproof.v @@ -13,7 +13,7 @@ (* *) (* *************************************************************) -(** Correctness proof for Asmgen *) +(** Composing all passes from Mach to KVX Asm *) Require Import Coqlib Errors. Require Import Integers Floats AST Linking. @@ -46,7 +46,7 @@ Proof. exists tp; split. apply Asm.transf_program_match; auto. auto. Qed. -(** Return Address Offset *) +(** Return Address Offset for Mach *) Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop := Mach_return_address_offset Asmblockgenproof.return_address_offset. @@ -59,6 +59,7 @@ Proof. intros; eapply Asmblockgenproof.return_address_exists; eauto. Qed. +(** Main preservation theorem: from Mach to KVX Asm *) Section PRESERVATION. @@ -86,7 +87,7 @@ End PRESERVATION. Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes). (*******************************************) -(* Stub actually needed by driver/Compiler *) +(** Stub actually needed by driver/Compiler *) Module Asmgenproof0. 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, diff --git a/kvx/PostpassScheduling.v b/kvx/PostpassScheduling.v index 7518866d..1f1f238a 100644 --- a/kvx/PostpassScheduling.v +++ b/kvx/PostpassScheduling.v @@ -12,6 +12,8 @@ (* *) (* *************************************************************) +(** Implementation (and basic properties) of the verified postpass scheduler *) + Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops. @@ -19,20 +21,13 @@ Require Peephole. Local Open Scope error_monad_scope. -(** Oracle taking as input a basic block, - returns a schedule expressed as a list of bundles *) +(** * Oracle taking as input a basic block, + returns a scheduled list of bundles *) Axiom schedule: bblock -> (list (list basic)) * option control. Extract Constant schedule => "PostpassSchedulingOracle.schedule". -Definition state' := L.mem. -Definition outcome' := option state'. - -Definition bblock' := L.bblock. - -Definition exec' := L.run. - -Definition exec := exec_bblock. +(** * Concat all bundles into one big basic block *) (* Lemmas necessary for defining concat_all *) Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil. @@ -49,8 +44,6 @@ Proof. - intros. rewrite <- app_comm_cons. discriminate. Qed. - - Definition check_size bb := if zlt Ptrofs.max_unsigned (size bb) then Error (msg "PostpassSchedulingproof.check_size") @@ -213,6 +206,8 @@ Qed. Inductive is_concat : bblock -> list bblock -> Prop := | mk_is_concat: forall tbb lbb, concat_all lbb = OK tbb -> is_concat tbb lbb. +(** * Remainder of the verified scheduler *) + Definition verify_schedule (bb bb' : bblock) : res unit := match bblock_simub bb bb' with | true => OK tt diff --git a/kvx/PostpassSchedulingOracle.ml b/kvx/PostpassSchedulingOracle.ml index 67e3f80f..330675b0 100644 --- a/kvx/PostpassSchedulingOracle.ml +++ b/kvx/PostpassSchedulingOracle.ml @@ -504,8 +504,7 @@ let alu_lite_y : int array = let resmap = fun r -> match r with | Rissue -> 3 | Rtiny -> 1 | Rlite -> 1 | _ -> 0 in Array.of_list (List.map resmap resource_names) -let alu_nop : int array = let resmap = fun r -> match r with - | Rissue -> 1 | Rnop -> 1 | _ -> 0 +let alu_nop : int array = let resmap = fun r -> 0 in Array.of_list (List.map resmap resource_names) let alu_tiny : int array = let resmap = fun r -> match r with @@ -627,16 +626,16 @@ let rec_to_usage r = | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y | _ -> raise InvalidEncoding) - | Maddw -> (match encoding with None -> mau_auxr + | Maddw | Msbfw -> (match encoding with None -> mau_auxr | Some U6 | Some S10 | Some U27L5 -> mau_auxr_x | _ -> raise InvalidEncoding) - | Maddd -> (match encoding with None | Some U6 | Some S10 -> mau_auxr + | Maddd | Msbfd -> (match encoding with None | Some U6 | Some S10 -> mau_auxr | Some U27L5 | Some U27L10 -> mau_auxr_x | Some E27U27L10 -> mau_auxr_y) - | Mulw| Msbfw -> (match encoding with None -> mau + | Mulw -> (match encoding with None -> mau | Some U6 | Some S10 | Some U27L5 -> mau_x | _ -> raise InvalidEncoding) - | Muld | Msbfd -> (match encoding with None | Some U6 | Some S10 -> mau + | Muld -> (match encoding with None | Some U6 | Some S10 -> mau | Some U27L5 | Some U27L10 -> mau_x | Some E27U27L10 -> mau_y) | Nop -> alu_nop @@ -914,12 +913,20 @@ let print_bb oc bb = let asm_instructions = Asm.unfold_bblock bb in List.iter (print_inst oc) asm_instructions +let print_schedule sched = + print_string "[ "; + Array.iter (fun x -> Printf.printf "%d; " x) sched; + print_endline "]";; + let do_schedule bb = - let problem = build_problem bb - in let solution = scheduler_by_name (!Clflags.option_fpostpass_sched) problem + let problem = build_problem bb in + (if debug then print_problem stdout problem); + let solution = scheduler_by_name !Clflags.option_fpostpass_sched problem in match solution with | None -> failwith "Could not find a valid schedule" - | Some sol -> let bundles = bundlize_solution bb sol in + | Some sol -> + ((if debug then print_schedule sol); + let bundles = bundlize_solution bb sol in (if debug then begin Printf.eprintf "Scheduling the following group of instructions:\n"; @@ -928,7 +935,7 @@ let do_schedule bb = List.iter (print_bb stderr) bundles; Printf.eprintf "--------------------------------\n" end; - bundles) + bundles)) (** * Dumb schedule if the above doesn't work diff --git a/kvx/abstractbb/AbstractBasicBlocksDef.v b/kvx/abstractbb/AbstractBasicBlocksDef.v index 0b1c502d..948ed660 100644 --- a/kvx/abstractbb/AbstractBasicBlocksDef.v +++ b/kvx/abstractbb/AbstractBasicBlocksDef.v @@ -45,7 +45,7 @@ End LangParam. -(** * Syntax and (sequential) semantics of "basic blocks" *) +(** * Syntax and (sequential) semantics of "abstract basic blocks" *) Module MkSeqLanguage(P: LangParam). Export P. @@ -62,12 +62,12 @@ Definition assign (m: mem) (x:R.t) (v: value): mem := fun y => if R.eq_dec x y then v else m y. -(** expressions *) +(** Expressions *) Inductive exp := - | PReg (x:R.t) - | Op (o:op) (le: list_exp) - | Old (e: exp) + | PReg (x:R.t) (**r pseudo-register *) + | Op (o:op) (le: list_exp) (**r operation *) + | Old (e: exp) (**r evaluation of [e] in the initial state of the instruction (see [inst] below) *) with list_exp := | Enil | Econs (e:exp) (le:list_exp) @@ -95,7 +95,8 @@ with list_exp_eval (le: list_exp) (m old: mem): option (list value) := | LOld le => list_exp_eval le old old end. -Definition inst := list (R.t * exp). (* = a sequence of assignments *) +(** An instruction represents a sequence of assignments where [Old] refers to the initial state of the sequence. *) +Definition inst := list (R.t * exp). Fixpoint inst_run (i: inst) (m old: mem): option mem := match i with @@ -107,6 +108,7 @@ Fixpoint inst_run (i: inst) (m old: mem): option mem := end end. +(** A basic block is a sequence of instructions. *) Definition bblock := list inst. Fixpoint run (p: bblock) (m: mem): option mem := @@ -250,12 +252,16 @@ Qed. End SEQLANG. -Module Terms. -(** terms in the symbolic evaluation -NB: such a term represents the successive computations in one given pseudo-register +(** * Terms in the symbolic execution *) + +(** Such a term represents the successive computations in one given pseudo-register. +The [hid] has no formal semantics: it is only used by the hash-consing oracle (itself dynamically checked to behave like an identity function). + *) +Module Terms. + Inductive term := | Input (x:R.t) (hid:hashcode) | App (o: op) (l: list_term) (hid:hashcode) @@ -334,11 +340,21 @@ Proof. - rewrite IHl; clear IHl. intuition (congruence || eauto). Qed. +(** * Rewriting rules in the symbolic execution *) + +(** The symbolic execution is parametrized by rewriting rules on pseudo-terms. *) + Record pseudo_term: Type := intro_fail { mayfail: list term; effect: term }. +(** Simulation relation between a term and a pseudo-term *) + +Definition match_pt (t: term) (pt: pseudo_term) := + (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m) + /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1). + Lemma inf_option_equivalence (A:Type) (o1 o2: option A): (o1 <> None -> o1 = o2) <-> (forall m1, o1 = Some m1 -> o2 = Some m1). Proof. @@ -346,10 +362,6 @@ Proof. symmetry; eauto. Qed. -Definition match_pt (t: term) (pt: pseudo_term) := - (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m) - /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1). - Lemma intro_fail_correct (l: list term) (t: term) : (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t). Proof. @@ -357,6 +369,7 @@ Proof. Qed. Hint Resolve intro_fail_correct: wlp. +(** The default reduction of a term to a pseudo-term *) Definition identity_fail (t: term):= intro_fail [t] t. Lemma identity_fail_correct (t: term): match_pt t (identity_fail t). @@ -366,6 +379,7 @@ Qed. Global Opaque identity_fail. Hint Resolve identity_fail_correct: wlp. +(** The reduction for constant term *) Definition nofail (is_constant: op -> bool) (t: term):= match t with | Input x _ => intro_fail ([])%list t @@ -385,6 +399,7 @@ Qed. Global Opaque nofail. Hint Resolve nofail_correct: wlp. +(** Term equivalence preserve the simulation by pseudo-terms *) Definition term_equiv t1 t2:= forall ge m, term_eval ge t1 m = term_eval ge t2 m. Global Instance term_equiv_Equivalence : Equivalence term_equiv. @@ -401,6 +416,7 @@ Proof. Qed. Hint Resolve match_pt_term_equiv: wlp. +(** Other generic reductions *) Definition app_fail (l: list term) (pt: pseudo_term): pseudo_term := {| mayfail := List.rev_append l pt.(mayfail); effect := pt.(effect) |}. @@ -431,6 +447,8 @@ Extraction Inline app_fail. Import ImpCore.Notations. Local Open Scope impure_scope. +(** Specification of rewriting functions in parameter of the symbolic execution: in the impure monad, because the rewriting functions produce hash-consed terms (wrapped in pseudo-terms). +*) Record reduction:= { result:> term -> ?? pseudo_term; result_correct: forall t, WHEN result t ~> pt THEN match_pt t pt; diff --git a/kvx/abstractbb/ImpSimuTest.v b/kvx/abstractbb/ImpSimuTest.v index c914eee1..89260ddb 100644 --- a/kvx/abstractbb/ImpSimuTest.v +++ b/kvx/abstractbb/ImpSimuTest.v @@ -10,13 +10,16 @@ (* *) (* *************************************************************) -(** Implementation of a symbolic execution of sequential semantics of Abstract Basic Blocks +(** Implementation of a simulation test (ie a "scheduling verifier") for the sequential semantics of Abstract Basic Blocks. + +It is based on a symbolic execution procedure of Abstract Basic Blocks with imperative hash-consing and rewriting. + +It also provides debugging information when the test fails. -with imperative hash-consing, and rewriting. *) -Require Export Impure.ImpHCons. +Require Export Impure.ImpHCons. (**r Import the Impure library. See https://github.com/boulme/ImpureDemo *) Export Notations. Import HConsing. @@ -32,6 +35,7 @@ Import ListNotations. Local Open Scope list_scope. +(** * Interface of (impure) equality tests for operators *) Module Type ImpParam. Include LangParam. @@ -54,6 +58,8 @@ Include MkSeqLanguage LP. End ISeqLanguage. +(** * A generic dictinary on PseudoRegisters with an impure equality test *) + Module Type ImpDict. Declare Module R: PseudoRegisters. @@ -91,26 +97,27 @@ Parameter eq_test_correct: forall A (d1 d2: t A), (* NB: we could also take an eq_test on R.t (but not really useful with "pure" dictionaries *) - -(* only for debugging *) +(** only for debugging *) Parameter not_eq_witness: forall {A}, t A -> t A -> ?? option R.t. End ImpDict. +(** * Specification of the provided tests *) Module Type ImpSimuInterface. Declare Module CoreL: ISeqLanguage. Import CoreL. Import Terms. +(** the silent test (without debugging informations) *) Parameter bblock_simu_test: reduction -> bblock -> bblock -> ?? bool. Parameter bblock_simu_test_correct: forall reduce (p1 p2 : bblock), WHEN bblock_simu_test reduce p1 p2 ~> b THEN b = true -> forall ge : genv, bblock_simu ge p1 p2. - +(** the verbose test extended with debugging informations *) Parameter verb_bblock_simu_test : reduction -> (R.t -> ?? pstring) -> @@ -127,6 +134,7 @@ Parameter verb_bblock_simu_test_correct: End ImpSimuInterface. +(** * Implementation of the provided tests *) Module ImpSimu (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R): ImpSimuInterface with Module CoreL := L. @@ -168,7 +176,7 @@ Section SimuWithReduce. Variable reduce: reduction. -Section CanonBuilding. +Section CanonBuilding. (** Implementation of the symbolic execution (ie a "canonical form" representing the semantics of an abstract basic block) *) Variable hC_term: hashinfo term -> ?? term. Hypothesis hC_term_correct: forall t, WHEN hC_term t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m. @@ -1117,9 +1125,9 @@ Extraction Inline lift. End ImpSimu. -Require Import FMapPositive. - +(** * Implementation of the Dictionary (based on PositiveMap) *) +Require Import FMapPositive. Require Import PArith. Require Import FMapPositive. @@ -1206,7 +1214,7 @@ Proof. Qed. Global Opaque eq_test. -(* ONLY FOR DEBUGGING INFO: get some key of a non-empty d *) +(** ONLY FOR DEBUGGING INFO: get some key of a non-empty d *) Fixpoint pick {A} (d: t A): ?? R.t := match d with | Leaf _ => FAILWITH "unexpected empty dictionary" @@ -1219,7 +1227,7 @@ Fixpoint pick {A} (d: t A): ?? R.t := RET (xO p) end. -(* ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *) +(** ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *) Fixpoint not_eq_witness {A} (d1 d2: t A): ?? option R.t := match d1, d2 with | Leaf _, Leaf _ => RET None diff --git a/kvx/abstractbb/Parallelizability.v b/kvx/abstractbb/Parallelizability.v index feebeee5..79ec9038 100644 --- a/kvx/abstractbb/Parallelizability.v +++ b/kvx/abstractbb/Parallelizability.v @@ -26,7 +26,7 @@ Require Import Sorting.Permutation. Require Import Bool. Local Open Scope lazy_bool_scope. - +(** * Definition of the parallel semantics *) Module ParallelSemantics (L: SeqLanguage). Export L. @@ -590,17 +590,17 @@ End PARALLELI. End ParallelizablityChecking. -Module Type PseudoRegSet. - -Declare Module R: PseudoRegisters. - -(** We assume a datatype [t] refining (list R.t) +(** * We assume a datatype [PseudoRegSet.t] refining [list R.t] *) +(** This data-refinement is given by an abstract "invariant" match_frame below, preserved by the following operations. - *) +Module Type PseudoRegSet. + +Declare Module R: PseudoRegisters. + Parameter t: Type. Parameter match_frame: t -> (list R.t) -> Prop. @@ -716,6 +716,11 @@ End ParallelChecks. +(** * Implementing the datatype [PosPseudoRegSet.t] refining [list R.t] *) + +(* This data-refinement is given by an abstract "invariant" match_frame below, +preserved by the following operations. +*) Require Import PArith. Require Import MSets.MSetPositive. @@ -724,12 +729,6 @@ Module PosPseudoRegSet <: PseudoRegSet with Module R:=Pos. Module R:=Pos. -(** We assume a datatype [t] refining (list R.t) - -This data-refinement is given by an abstract "invariant" match_frame below, -preserved by the following operations. - -*) Definition t:=PositiveSet.t. diff --git a/kvx/abstractbb/SeqSimuTheory.v b/kvx/abstractbb/SeqSimuTheory.v index 61f8f2ec..a957c50a 100644 --- a/kvx/abstractbb/SeqSimuTheory.v +++ b/kvx/abstractbb/SeqSimuTheory.v @@ -55,13 +55,14 @@ with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) : end end. -(* the symbolic memory: - - pre: pre-condition expressing that the computation has not yet abort on a None. - - post: the post-condition for each pseudo-register -*) -Record smem:= {pre: genv -> mem -> Prop; post:> R.t -> term}. - -(** initial symbolic memory *) +(** The (abstract) symbolic memory state *) +Record smem := +{ + pre: genv -> mem -> Prop; (**r pre-condition expressing that the computation has not yet abort on a None. *) + post:> R.t -> term (**r the output term computed on each pseudo-register *) +}. + +(** Initial symbolic memory state *) Definition smem_empty := {| pre:=fun _ _ => True; post:=(fun x => Input x) |}. Fixpoint exp_term (e: exp) (d old: smem) : term := @@ -78,11 +79,12 @@ with list_exp_term (le: list_exp) (d old: smem) : list_term := end. -(** assignment of the symbolic memory *) +(** assignment of the symbolic memory state *) Definition smem_set (d:smem) x (t:term) := {| pre:=(fun ge m => (term_eval ge (d x) m) <> None /\ (d.(pre) ge m)); post:=fun y => if R.eq_dec x y then t else d y |}. +(** Simulation theory: the theorem [bblock_smem_simu] ensures that the simulation between two abstract basic blocks is implied by the simulation between their symbolic execution. *) Section SIMU_THEORY. Variable ge: genv. @@ -375,8 +377,7 @@ Qed. End SIMU_THEORY. -(** REMARKS: more abstract formulation of the proof... - but relying on functional_extensionality. +(** REMARK: this theorem reformulates the lemma above in a more abstract way (but relies on functional_extensionality axiom). *) Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:= forall m', om=Some m' <-> (d.(pre) ge m /\ forall x, term_eval ge (d x) m = Some (m' x)). diff --git a/kvx/lib/Machblock.v b/kvx/lib/Machblock.v index 08e0eba2..edae0ed4 100644 --- a/kvx/lib/Machblock.v +++ b/kvx/lib/Machblock.v @@ -12,6 +12,8 @@ (* *) (* *************************************************************) +(** Abstract syntax and semantics of a Mach variant, structured with basic-blocks. *) + Require Import Coqlib. Require Import Maps. Require Import AST. @@ -28,7 +30,9 @@ Require Stacklayout. Require Import Mach. Require Import Linking. -(** basic instructions (ie no control-flow) *) +(** * Abstract Syntax *) + +(** ** basic instructions (ie no control-flow) *) Inductive basic_inst: Type := | MBgetstack: ptrofs -> typ -> mreg -> basic_inst | MBsetstack: mreg -> ptrofs -> typ -> basic_inst @@ -40,7 +44,7 @@ Inductive basic_inst: Type := Definition bblock_body := list basic_inst. -(** control flow instructions *) +(** ** control flow instructions *) Inductive control_flow_inst: Type := | MBcall: signature -> mreg + ident -> control_flow_inst | MBtailcall: signature -> mreg + ident -> control_flow_inst @@ -51,6 +55,7 @@ Inductive control_flow_inst: Type := | MBreturn: control_flow_inst . +(** ** basic block *) Record bblock := mk_bblock { header: list label; body: bblock_body; @@ -91,6 +96,8 @@ Proof. destruct e; try (simpl in He; discriminate); auto. Qed. +(** ** programs *) + Definition code := list bblock. Record function: Type := mkfunction @@ -106,7 +113,7 @@ Definition program := AST.program fundef unit. Definition genv := Genv.t fundef unit. -(*** sémantique ***) +(** * Operational (blockstep) semantics ***) Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. Proof. @@ -155,7 +162,7 @@ Definition find_function_ptr Genv.find_symbol ge symb end. -(** Machblock execution states. *) +(** ** Machblock execution states. *) Inductive stackframe: Type := | Stackframe: diff --git a/kvx/lib/Machblockgen.v b/kvx/lib/Machblockgen.v index 287e4f7b..ab186083 100644 --- a/kvx/lib/Machblockgen.v +++ b/kvx/lib/Machblockgen.v @@ -29,6 +29,8 @@ Require Import Mach. Require Import Linking. Require Import Machblock. +(** * Tail-recursive (greedy) translation from Mach code to Machblock code *) + Inductive Machblock_inst: Type := | MB_label (lbl: label) | MB_basic (bi: basic_inst) @@ -71,9 +73,12 @@ Definition add_to_new_bblock (i:Machblock_inst) : bblock := | MB_cfi i => cfi_bblock i end. -(** Adding an instruction to the beginning of a bblock list - * Either adding the instruction to the head of the list, - * or create a new bblock with the instruction *) +(** Adding an instruction to the beginning of a bblock list by + +- either adding the instruction to the head of the list, + +- or creating a new bblock with the instruction +*) Definition add_to_code (i:Machblock_inst) (bl:code) : code := match bl with | bh::bl0 => match i with @@ -112,7 +117,7 @@ Definition transf_program (src: Mach.program) : program := transform_program transf_fundef src. -(** Abstracting trans_code *) +(** * Abstracting trans_code with a simpler inductive relation *) Inductive is_end_block: Machblock_inst -> code -> Prop := | End_empty mbi: is_end_block mbi nil |