Merge branch 'mppa-refactor' into mppa-work

1 files changed, 1204 insertions, 44 deletions

diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index c15a33af..8620326f 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -15,7 +15,9 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Abstract syntax and semantics for K1c assembly language. *)
+(** Abstract syntax and semantics for VLIW semantics of K1c assembly language. *)
+
+(* FIXME: develop/fix the comments in this file *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -31,24 +33,1012 @@ Require Import Locations.
 Require Stacklayout.
 Require Import Conventions.
 Require Import Errors.
-Require Export Asmblock.
 Require Import Sorting.Permutation.
 
+(** * Abstract syntax *)
+
+(** A K1c program is syntactically given as a list of functions. 
+    Each function is associated to a list of bundles of type [bblock] below.
+    Hence, syntactically, we view each bundle as a basic block:
+    this view induces our sequential semantics of bundles defined in [Asmblock].
+*)
+
+(** General Purpose registers.
+*)
+
+Inductive gpreg: Type :=
+  | GPR0:  gpreg | GPR1:  gpreg | GPR2:  gpreg | GPR3:  gpreg | GPR4:  gpreg
+  | GPR5:  gpreg | GPR6:  gpreg | GPR7:  gpreg | GPR8:  gpreg | GPR9:  gpreg
+  | GPR10: gpreg | GPR11: gpreg | GPR12: gpreg | GPR13: gpreg | GPR14: gpreg
+  | GPR15: gpreg | GPR16: gpreg | GPR17: gpreg | GPR18: gpreg | GPR19: gpreg
+  | GPR20: gpreg | GPR21: gpreg | GPR22: gpreg | GPR23: gpreg | GPR24: gpreg
+  | GPR25: gpreg | GPR26: gpreg | GPR27: gpreg | GPR28: gpreg | GPR29: gpreg
+  | GPR30: gpreg | GPR31: gpreg | GPR32: gpreg | GPR33: gpreg | GPR34: gpreg
+  | GPR35: gpreg | GPR36: gpreg | GPR37: gpreg | GPR38: gpreg | GPR39: gpreg
+  | GPR40: gpreg | GPR41: gpreg | GPR42: gpreg | GPR43: gpreg | GPR44: gpreg
+  | GPR45: gpreg | GPR46: gpreg | GPR47: gpreg | GPR48: gpreg | GPR49: gpreg
+  | GPR50: gpreg | GPR51: gpreg | GPR52: gpreg | GPR53: gpreg | GPR54: gpreg
+  | GPR55: gpreg | GPR56: gpreg | GPR57: gpreg | GPR58: gpreg | GPR59: gpreg
+  | GPR60: gpreg | GPR61: gpreg | GPR62: gpreg | GPR63: gpreg.
+
+Definition ireg := gpreg.
+Definition freg := gpreg.
+
+Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+
+Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+
+(** We model the following registers of the RISC-V architecture. *)
+
+(** basic register *)
+Inductive preg: Type :=
+  | IR: gpreg -> preg                   (**r integer general purpose registers *)
+  | RA: preg
+  | PC: preg
+  .
+
+Coercion IR: gpreg >-> preg.
+
+Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
+Proof. decide equality. apply ireg_eq. Defined.
+
+Module PregEq.
+  Definition t  := preg.
+  Definition eq := preg_eq.
+End PregEq.
+
+Module Pregmap := EMap(PregEq).
+
+(** Conventional names for stack pointer ([SP]) and return address ([RA]). *)
+
+Notation "'SP'" := GPR12 (only parsing) : asm.
+Notation "'FP'" := GPR17 (only parsing) : asm.
+Notation "'MFP'" := R17 (only parsing) : asm.
+Notation "'GPRA'" := GPR16 (only parsing) : asm.
+Notation "'RTMP'" := GPR32 (only parsing) : asm.
+
+Inductive btest: Type :=
+  | BTdnez                              (**r Double Not Equal to Zero *)
+  | BTdeqz                              (**r Double Equal to Zero *)
+  | BTdltz                              (**r Double Less Than Zero *)
+  | BTdgez                              (**r Double Greater Than or Equal to Zero *)
+  | BTdlez                              (**r Double Less Than or Equal to Zero *)
+  | BTdgtz                              (**r Double Greater Than Zero *)
+(*| BTodd                               (**r Odd (LSB Set) *)
+  | BTeven                              (**r Even (LSB Clear) *)
+*)| BTwnez                              (**r Word Not Equal to Zero *)
+  | BTweqz                              (**r Word Equal to Zero *)
+  | BTwltz                              (**r Word Less Than Zero *)
+  | BTwgez                              (**r Word Greater Than or Equal to Zero *)
+  | BTwlez                              (**r Word Less Than or Equal to Zero *)
+  | BTwgtz                              (**r Word Greater Than Zero *)
+  .
+
+Inductive itest: Type :=
+  | ITne                                (**r Not Equal *)
+  | ITeq                                (**r Equal *)
+  | ITlt                                (**r Less Than *)
+  | ITge                                (**r Greater Than or Equal *)
+  | ITle                                (**r Less Than or Equal *)
+  | ITgt                                (**r Greater Than *)
+  | ITneu                               (**r Unsigned Not Equal *)
+  | ITequ                               (**r Unsigned Equal *)
+  | ITltu                               (**r Less Than Unsigned *)
+  | ITgeu                               (**r Greater Than or Equal Unsigned *)
+  | ITleu                               (**r Less Than or Equal Unsigned *)
+  | ITgtu                               (**r Greater Than Unsigned *)
+  (* Not used yet *)
+  | ITall                               (**r All Bits Set in Mask *)
+  | ITnall                              (**r Not All Bits Set in Mask *)
+  | ITany                               (**r Any Bits Set in Mask *)
+  | ITnone                              (**r Not Any Bits Set in Mask *)
+  .
+
+Inductive ftest: Type :=
+  | FTone                               (**r Ordered and Not Equal *)
+  | FTueq                               (**r Unordered or Equal *)
+  | FToeq                               (**r Ordered and Equal *)
+  | FTune                               (**r Unordered or Not Equal *)
+  | FTolt                               (**r Ordered and Less Than *)
+  | FTuge                               (**r Unordered or Greater Than or Equal *)
+  | FToge                               (**r Ordered and Greater Than or Equal *)
+  | 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. *)
+
+Inductive offset : Type :=
+  | Ofsimm (ofs: ptrofs)
+  | Ofslow (id: ident) (ofs: ptrofs).
+
+(** We model a subset of the K1c instruction set. In particular, we do not
+  support floats yet.
+
+  Although it is possible to use the 32-bits mode, for now we don't support it.
+
+  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.
+
+  When mapping to actual instructions, the OCaml code in TargetPrinter.ml
+  throws an error if we are not in 64-bits mode.
+*)
+
+(** * Instructions *)
+
+Definition label := positive.
+
+(* FIXME - rewrite the comment *)
+(** A note on immediates: there are various constraints on immediate
+  operands to K1c instructions.  We do not attempt to capture these
+  restrictions in the abstract syntax nor in the semantics.  The
+  assembler will emit an error if immediate operands exceed the
+  representable range.  Of course, our K1c generator (file
+  [Asmgen]) is careful to respect this range. *)
+
+(** Instructions to be expanded in control-flow 
+*)
+Inductive ex_instruction : Type :=
+  (* Pseudo-instructions *)
+(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *)
+  | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *) *)
+
+  | 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:
+
+- [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.
+
+- [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 *)
+Inductive cf_instruction : Type :=
+  | Pret                                            (**r return *)
+  | Pcall   (l: label)                              (**r function call *)
+  | Picall  (r: ireg)                               (**r function call on register value *)
+  | Pjumptable (r: ireg) (labels: list label) (**r N-way branch through a jump table (pseudo) *)
+
+  (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *)
+  | Pgoto   (l: label)                              (**r goto *)
+  | Pigoto  (r: ireg)                               (**r goto from register *)
+  | Pj_l    (l: label)                              (**r jump to label *)
+
+  (* Conditional branches *)
+  | Pcb     (bt: btest) (r: ireg) (l: label)        (**r branch based on btest *)
+  | Pcbu    (bt: btest) (r: ireg) (l: label)        (**r branch based on btest with unsigned semantics *)
+.
+
+(** Loads **)
+Inductive load_name : Type :=
+  | Plb                                             (**r load byte *)
+  | Plbu                                            (**r load byte unsigned *)
+  | Plh                                             (**r load half word *)
+  | Plhu                                            (**r load half word unsigned *)
+  | Plw                                             (**r load int32 *)
+  | Plw_a                                           (**r load any32 *)
+  | Pld                                             (**r load int64 *)
+  | Pld_a                                           (**r load any64 *)
+  | Pfls                                            (**r load float *)
+  | Pfld                                            (**r load 64-bit float *)
+.
+
+Inductive ld_instruction : Type :=
+  | PLoadRRO   (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset)
+  | PLoadRRR   (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
+.
+
+Coercion PLoadRRO:       load_name        >-> Funclass.
+Coercion PLoadRRR:       load_name        >-> Funclass.
+
+(** Stores **)
+Inductive store_name : Type :=
+  | Psb                                             (**r store byte *)
+  | Psh                                             (**r store half byte *)
+  | Psw                                             (**r store int32 *)
+  | Psw_a                                           (**r store any32 *)
+  | Psd                                             (**r store int64 *)
+  | Psd_a                                           (**r store any64 *)
+  | Pfss                                            (**r store float *)
+  | Pfsd                                            (**r store 64-bit float *)
+.
+
+Inductive st_instruction : Type :=
+  | PStoreRRO  (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset)
+  | PStoreRRR  (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
+.
+
+Coercion PStoreRRO:       store_name        >-> Funclass.
+Coercion PStoreRRR:       store_name        >-> Funclass.
+
+(** Arithmetic instructions **)
+Inductive arith_name_r : Type :=
+  | Ploadsymbol (id: ident) (ofs: ptrofs)           (**r load the address of a symbol *)
+.
+
+Inductive arith_name_rr : Type :=
+  | Pmv                                             (**r register move *)
+  | Pnegw                                           (**r negate word *)
+  | Pnegl                                           (**r negate long *)
+  | Pcvtl2w                                         (**r Convert Long to Word *)
+  | Psxwd                                           (**r Sign Extend Word to Double Word *)
+  | Pzxwd                                           (**r Zero Extend Word to Double Word *)
+
+  | Pfabsd                                          (**r float absolute double *)
+  | Pfabsw                                          (**r float absolute word *)
+  | Pfnegd                                          (**r float negate double *)
+  | Pfnegw                                          (**r float negate word *)
+  | Pfnarrowdw                                      (**r float narrow 64 -> 32 bits *)
+  | Pfwidenlwd                                      (**r Floating Point widen from 32 bits to 64 bits *)
+  | Pfloatwrnsz                                     (**r Floating Point conversion from integer (int -> SINGLE) *)
+  | Pfloatuwrnsz                                    (**r Floating Point conversion from integer (unsigned int -> SINGLE) *)
+  | Pfloatudrnsz                                    (**r Floating Point Conversion from integer (unsigned long -> float) *)
+  | Pfloatudrnsz_i32                                (**r Floating Point Conversion from integer (unsigned int -> float) *)
+  | Pfloatdrnsz                                     (**r Floating Point Conversion from integer (long -> float) *)
+  | Pfloatdrnsz_i32                                 (**r Floating Point Conversion from integer (int -> float) *)
+  | Pfixedwrzz                                      (**r Integer conversion from floating point (single -> int) *)
+  | Pfixeduwrzz                                     (**r Integer conversion from floating point (single -> unsigned int) *)
+  | Pfixeddrzz                                      (**r Integer conversion from floating point (float -> long) *)
+  | Pfixedudrzz                                      (**r Integer conversion from floating point (float -> unsigned long) *)
+  | Pfixeddrzz_i32                                  (**r Integer conversion from floating point (float -> int) *)
+  | Pfixedudrzz_i32                                  (**r Integer conversion from floating point (float -> unsigned int) *)
+.
+
+Inductive arith_name_ri32 : Type :=
+  | Pmake                                           (**r load immediate *)
+.
+
+Inductive arith_name_ri64 : Type :=
+  | Pmakel                                          (**r load immediate long *)
+.
+
+Inductive arith_name_rf32 : Type :=
+  | Pmakefs                                         (**r load immediate single *)
+.
+
+Inductive arith_name_rf64 : Type :=
+  | Pmakef                                          (**r load immediate float *)
+.
+
+Inductive arith_name_rrr : Type :=
+  | Pcompw  (it: itest)                             (**r comparison word *)
+  | Pcompl  (it: itest)                             (**r comparison long *)
+  | Pfcompw (ft: ftest)                             (**r comparison float32 *)
+  | Pfcompl (ft: ftest)                             (**r comparison float64 *)
+
+  | Paddw                                           (**r add word *)
+  | Psubw                                           (**r sub word *)
+  | Pmulw                                           (**r mul word *)
+  | Pandw                                           (**r and word *)
+  | Pnandw                                          (**r nand word *)
+  | Porw                                            (**r or word *)
+  | Pnorw                                           (**r nor word *)
+  | Pxorw                                           (**r xor word *)
+  | Pnxorw                                          (**r nxor word *)
+  | Pandnw                                          (**r andn word *)
+  | Pornw                                           (**r orn word *)
+  | Psraw                                           (**r shift right arithmetic word *)
+  | Psrlw                                           (**r shift right logical word *)
+  | Psllw                                           (**r shift left logical word *)
+
+  | Paddl                                           (**r add long *)
+  | Psubl                                           (**r sub long *)
+  | Pandl                                           (**r and long *)
+  | Pnandl                                          (**r nand long *)
+  | Porl                                            (**r or long *)
+  | Pnorl                                           (**r nor long *)
+  | Pxorl                                           (**r xor long *)
+  | Pnxorl                                          (**r nxor long *)
+  | Pandnl                                          (**r andn long *)
+  | Pornl                                           (**r orn long *)
+  | Pmull                                           (**r mul long (low part) *)
+  | Pslll                                           (**r shift left logical long *)
+  | Psrll                                           (**r shift right logical long *)
+  | Psral                                           (**r shift right arithmetic long *)
+
+  | Pfaddd                                          (**r float add double *)
+  | Pfaddw                                          (**r float add word *)
+  | Pfsbfd                                          (**r float sub double *)
+  | Pfsbfw                                          (**r float sub word *)
+  | Pfmuld                                          (**r float multiply double *)
+  | Pfmulw                                          (**r float multiply word *)
+.
+
+Inductive arith_name_rri32 : Type :=
+  | Pcompiw (it: itest)                             (**r comparison imm word *)
+
+  | Paddiw                                          (**r add imm word *)
+  | Pmuliw                                          (**r add imm word *)
+  | Pandiw                                          (**r and imm word *)
+  | Pnandiw                                         (**r nand imm word *)
+  | Poriw                                           (**r or imm word *)
+  | Pnoriw                                          (**r nor imm word *)
+  | Pxoriw                                          (**r xor imm word *)
+  | Pnxoriw                                         (**r nxor imm word *)
+  | Pandniw                                         (**r andn word *)
+  | Porniw                                          (**r orn word *)
+  | Psraiw                                          (**r shift right arithmetic imm word *)
+  | Psrliw                                          (**r shift right logical imm word *)
+  | Pslliw                                          (**r shift left logical imm word *)
+  | Proriw                                          (**r rotate right imm word *)
+  | Psllil                                          (**r shift left logical immediate long *)
+  | Psrlil                                          (**r shift right logical immediate long *)
+  | Psrail                                          (**r shift right arithmetic immediate long *)
+.
+
+Inductive arith_name_rri64 : Type :=
+  | Pcompil (it: itest)                             (**r comparison imm long *)
+  | Paddil                                          (**r add immediate long *) 
+  | Pmulil                                          (**r mul immediate long *) 
+  | Pandil                                          (**r and immediate long *) 
+  | Pnandil                                         (**r nand immediate long *) 
+  | Poril                                           (**r or immediate long *) 
+  | Pnoril                                          (**r nor immediate long *) 
+  | Pxoril                                          (**r xor immediate long *) 
+  | Pnxoril                                         (**r nxor immediate long *) 
+  | Pandnil                                         (**r andn immediate long *)
+  | Pornil                                          (**r orn immediate long *)
+.
+
+Inductive arith_name_arrr : Type :=
+  | Pmaddw                                           (**r multiply add word *)
+  | Pmaddl                                           (**r multiply add long *)
+  | Pcmove (bt: btest)                               (**r conditional move *)
+  | Pcmoveu (bt: btest)                              (**r conditional move, test on unsigned semantics *)
+.
+
+Inductive arith_name_arri32 : Type :=
+  | Pmaddiw                                           (**r multiply add word *)
+.
+
+Inductive arith_name_arri64 : Type :=
+  | Pmaddil                                           (**r multiply add long *)
+.
+
+Inductive ar_instruction : Type :=
+  | PArithR     (i: arith_name_r)     (rd: ireg)
+  | PArithRR    (i: arith_name_rr)    (rd rs: ireg)
+  | PArithRI32  (i: arith_name_ri32)  (rd: ireg) (imm: int)
+  | PArithRI64  (i: arith_name_ri64)  (rd: ireg) (imm: int64)
+  | PArithRF32  (i: arith_name_rf32)  (rd: ireg) (imm: float32)
+  | PArithRF64  (i: arith_name_rf64)  (rd: ireg) (imm: float)
+  | PArithRRR   (i: arith_name_rrr)   (rd rs1 rs2: ireg)
+  | PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int)
+  | PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64)
+  | PArithARRR   (i: arith_name_arrr)   (rd rs1 rs2: ireg)
+  | PArithARRI32 (i: arith_name_arri32) (rd rs: ireg) (imm: int)
+  | PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64)
+.
+
+Coercion PArithR:       arith_name_r        >-> Funclass.
+Coercion PArithRR:      arith_name_rr       >-> Funclass.
+Coercion PArithRI32:    arith_name_ri32     >-> Funclass.
+Coercion PArithRI64:    arith_name_ri64     >-> Funclass.
+Coercion PArithRF32:    arith_name_rf32     >-> Funclass.
+Coercion PArithRF64:    arith_name_rf64     >-> Funclass.
+Coercion PArithRRR:     arith_name_rrr      >-> Funclass.
+Coercion PArithRRI32:   arith_name_rri32    >-> Funclass.
+Coercion PArithRRI64:   arith_name_rri64    >-> Funclass.
+Coercion PArithARRR:     arith_name_arrr      >-> Funclass.
+Coercion PArithARRI32:   arith_name_arri32    >-> Funclass.
+Coercion PArithARRI64:   arith_name_arri64    >-> Funclass.
+
+Inductive basic : Type :=
+  | PArith          (i: ar_instruction)
+  | PLoad           (i: ld_instruction)
+  | PStore          (i: st_instruction)
+  | Pallocframe (sz: Z) (pos: ptrofs)               (**r allocate new stack frame *)
+  | Pfreeframe  (sz: Z) (pos: ptrofs)               (**r deallocate stack frame and restore previous frame *)
+  | Pget    (rd: ireg) (rs: preg)                   (**r get system register *)
+  | Pset    (rd: preg) (rs: ireg)                   (**r set system register *)
+  | Pnop                                            (**r virtual instruction that does nothing *)
+.
+
+Coercion PLoad:         ld_instruction >-> basic.
+Coercion PStore:        st_instruction >-> basic.
+Coercion PArith:        ar_instruction >-> basic.
+
+
+Inductive control : Type :=
+  | PExpand         (i: ex_instruction)
+  | PCtlFlow        (i: cf_instruction)
+.
+
+Coercion PExpand:   ex_instruction >-> control.
+Coercion PCtlFlow:  cf_instruction >-> control.
+
+
+(** * Definition of a bblock (ie a bundle) *)
+
+Definition non_empty_body (body: list basic): bool :=
+  match body with
+  | nil => false
+  | _ => true
+  end.
+
+Definition non_empty_exit (exit: option control): bool :=
+  match exit with
+  | None => false
+  | _ => true
+  end.
+
+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 ?
+ *)
+Definition builtin_aloneb (body: list basic) (exit: option control) :=
+  match exit with
+  | Some (PExpand (Pbuiltin _ _ _)) =>
+    match body with
+    | nil => true
+    | _ => false
+    end
+  | _ => true
+  end.
+
+Definition wf_bblockb (body: list basic) (exit: option control) :=
+  (non_empty_bblockb body exit) && (builtin_aloneb body exit).
+
+(** A bblock is well-formed if he contains at least one instruction,
+    and if there is a builtin then it must be alone in this bblock. *)
+
+Record bblock := mk_bblock {
+  header: list label;
+  body: list basic;
+  exit: option control;
+  correct: Is_true (wf_bblockb body exit)
+}.
+
+(* FIXME? redundant with definition in Machblock *)
+Definition length_opt {A} (o: option A) : nat :=
+  match o with
+  | Some o => 1
+  | None => 0
+  end.
+
+(* WARNING: the 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)).
+
+Definition bblocks := list bblock.
+
+Fixpoint size_blocks (l: bblocks): Z :=
+  match l with
+  | nil => 0
+  | b :: l =>
+     (size b) + (size_blocks l)
+  end
+  .
+
+Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
+Definition fundef := AST.fundef function.
+Definition program := AST.program fundef unit.
+
+(** * Operational semantics *)
+
+(** The semantics operates over a single mapping from registers
+  (type [preg]) to values.  We maintain
+  the convention that integer registers are mapped to values of
+  type [Tint] or [Tlong] (in 64 bit mode),
+  and float registers to values of type [Tsingle] or [Tfloat]. *)
+
+Definition regset := Pregmap.t val.
+
+Definition genv := Genv.t fundef unit.
+
+Notation "a # b" := (a b) (at level 1, only parsing) : asm.
+Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
+
+Open Scope asm.
+
+(** Undefining some registers *)
+
+Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
+  match l with
+  | nil => rs
+  | r :: l' => undef_regs l' (rs#r <- Vundef)
+  end.
+
+
+(** Assigning a register pair *)
+Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
+  match p with
+  | One r => rs#r <- v
+  | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
+  end.
+
+(* TODO: Is it still useful ?? *)
+
+
+(** Assigning multiple registers *)
+
+(* Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset :=
+  match rl, vl with
+  | r1 :: rl', v1 :: vl' => set_regs rl' vl' (rs#r1 <- v1)
+  | _, _ => rs
+  end.
+ *)
+(** Assigning the result of a builtin *)
+
+Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
+  match res with
+  | BR r => rs#r <- v
+  | BR_none => rs
+  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+  end.
+
 Local Open Scope asm.
 
+(** * Parallel Semantics of bundles *)
+
 Section RELSEM.
 
 (** Execution of arith instructions *)
 
 Variable ge: genv.
 
-(* TODO: on pourrait mettre ça dans Asmblock pour factoriser le code
-   en définissant 
-    exec_arith_instr ai rs := parexec_arith_instr ai rs rs
-*)
+(** The semantics is purely small-step and defined as a function
+  from the current state (a register set + a memory state)
+  to either [Next rs' m'] where [rs'] and [m'] are the updated register
+  set and memory state after execution of the instruction at [rs#PC],
+  or [Stuck] if the processor is stuck. *)
+
+Inductive outcome: Type :=
+  | Next (rs:regset) (m:mem)
+  | Stuck
+.
+
+(** ** Arithmetic Expressions (including comparisons) *)
+
+Inductive signedness: Type := Signed | Unsigned.
+
+Inductive intsize: Type := Int | Long.
+
+Definition itest_for_cmp (c: comparison) (s: signedness) :=
+  match c, s with
+  | Cne, Signed => ITne
+  | Ceq, Signed => ITeq
+  | Clt, Signed => ITlt
+  | Cge, Signed => ITge
+  | Cle, Signed => ITle
+  | Cgt, Signed => ITgt
+  | Cne, Unsigned => ITneu
+  | Ceq, Unsigned => ITequ
+  | Clt, Unsigned => ITltu
+  | Cge, Unsigned => ITgeu
+  | Cle, Unsigned => ITleu
+  | Cgt, Unsigned => ITgtu
+  end.
+
+Inductive oporder_ftest :=
+  | Normal (ft: ftest)
+  | Reversed (ft: ftest)
+.
+
+Definition ftest_for_cmp (c: comparison) :=
+  match c with
+  | Ceq => Normal FToeq
+  | Cne => Normal FTune
+  | Clt => Normal FTolt
+  | Cle => Reversed FToge
+  | Cgt => Reversed FTolt
+  | Cge => Normal FToge
+  end.
+
+Definition notftest_for_cmp (c: comparison) :=
+  match c with
+  | Ceq => Normal FTune
+  | Cne => Normal FToeq
+  | Clt => Normal FTuge
+  | Cle => Reversed FTult
+  | Cgt => Reversed FTuge
+  | Cge => Normal FTult
+  end.
+
+(* CoMPare Signed Words to Zero *)
+Definition btest_for_cmpswz (c: comparison) :=
+  match c with
+  | Cne => BTwnez
+  | Ceq => BTweqz
+  | Clt => BTwltz
+  | Cge => BTwgez
+  | Cle => BTwlez
+  | Cgt => BTwgtz
+  end.
+
+(* CoMPare Signed Doubles to Zero *)
+Definition btest_for_cmpsdz (c: comparison) :=
+  match c with
+  | Cne => BTdnez
+  | Ceq => BTdeqz
+  | Clt => BTdltz
+  | Cge => BTdgez
+  | Cle => BTdlez
+  | Cgt => BTdgtz
+  end.
+
+Definition cmp_for_btest (bt: btest) :=
+  match bt with
+  | BTwnez => (Some Cne, Int)
+  | BTweqz => (Some Ceq, Int)
+  | BTwltz => (Some Clt, Int)
+  | BTwgez => (Some Cge, Int)
+  | BTwlez => (Some Cle, Int)
+  | BTwgtz => (Some Cgt, Int)
+
+  | BTdnez => (Some Cne, Long)
+  | BTdeqz => (Some Ceq, Long)
+  | BTdltz => (Some Clt, Long)
+  | BTdgez => (Some Cge, Long)
+  | BTdlez => (Some Cle, Long)
+  | BTdgtz => (Some Cgt, Long)
+  end.
+
+Definition cmpu_for_btest (bt: btest) :=
+  match bt with
+  | BTwnez => (Some Cne, Int)
+  | BTweqz => (Some Ceq, Int)
+  | BTdnez => (Some Cne, Long)
+  | BTdeqz => (Some Ceq, Long)
+  | _ => (None, Int)
+  end.
+
+
+(* 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.
+
+Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
+   (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
+   -> (Val_cmpu_bool cmp v1 v2) = Some b.
+Proof.
+  intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto).
+Qed.
+
+Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2).
+
+Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val):
+   Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2)
+               (Val_cmpu cmp v1 v2).
+Proof.
+  unfold Val.cmpu, Val_cmpu.
+  remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
+  destruct ob; simpl.
+  - erewrite Val_cmpu_bool_correct; eauto.
+    econstructor.
+  - econstructor.
+Qed.
+
+Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val)
+ := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2).
+
+Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
+   (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
+   -> (Val_cmplu_bool cmp v1 v2) = Some b.
+Proof.
+  intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto).
+Qed.
+
+Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2).
+
+Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val):
+   Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2))
+               (Val_cmplu cmp v1 v2).
+Proof.
+  unfold Val.cmplu, Val_cmplu.
+  remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
+  destruct ob as [b|]; simpl.
+  - erewrite Val_cmplu_bool_correct; eauto.
+    simpl. econstructor.
+  - econstructor.
+Qed.
+
+
+
+(** Comparing integers *)
+Definition compare_int (t: itest) (v1 v2: val): val :=
+  match t with
+  | ITne  => Val.cmp Cne v1 v2
+  | ITeq  => Val.cmp Ceq v1 v2
+  | ITlt  => Val.cmp Clt v1 v2
+  | ITge  => Val.cmp Cge v1 v2
+  | ITle  => Val.cmp Cle v1 v2
+  | ITgt  => Val.cmp Cgt v1 v2
+  | ITneu => Val_cmpu Cne v1 v2
+  | ITequ => Val_cmpu Ceq v1 v2
+  | ITltu => Val_cmpu Clt v1 v2
+  | ITgeu => Val_cmpu Cge v1 v2
+  | ITleu => Val_cmpu Cle v1 v2
+  | ITgtu => Val_cmpu Cgt v1 v2
+  | ITall
+  | ITnall
+  | ITany
+  | ITnone => Vundef
+  end.
+
+Definition compare_long (t: itest) (v1 v2: val): val :=
+  let res := match t with
+  | ITne  => Val.cmpl Cne v1 v2
+  | ITeq  => Val.cmpl Ceq v1 v2
+  | ITlt  => Val.cmpl Clt v1 v2
+  | ITge  => Val.cmpl Cge v1 v2
+  | ITle  => Val.cmpl Cle v1 v2
+  | ITgt  => Val.cmpl Cgt v1 v2
+  | ITneu => Some (Val_cmplu Cne v1 v2)
+  | ITequ => Some (Val_cmplu Ceq v1 v2)
+  | ITltu => Some (Val_cmplu Clt v1 v2)
+  | ITgeu => Some (Val_cmplu Cge v1 v2)
+  | ITleu => Some (Val_cmplu Cle v1 v2)
+  | ITgtu => Some (Val_cmplu Cgt v1 v2)
+  | ITall
+  | ITnall
+  | ITany
+  | ITnone => Some Vundef
+  end in 
+  match res with
+  | Some v => v
+  | None => Vundef
+  end
+  .
+
+Definition compare_single (t: ftest) (v1 v2: val): val :=
+  match t with
+  | FTone | FTueq => Vundef (* unused *)
+  | FToeq => Val.cmpfs Ceq v1 v2
+  | FTune => Val.cmpfs Cne v1 v2
+  | FTolt => Val.cmpfs Clt v1 v2
+  | FTuge => Val.notbool (Val.cmpfs Clt v1 v2)
+  | FToge => Val.cmpfs Cge v1 v2
+  | FTult => Val.notbool (Val.cmpfs Cge v1 v2)
+  end.
+
+Definition compare_float (t: ftest) (v1 v2: val): val :=
+  match t with
+  | FTone | FTueq => Vundef (* unused *)
+  | FToeq => Val.cmpf Ceq v1 v2
+  | FTune => Val.cmpf Cne v1 v2
+  | FTolt => Val.cmpf Clt v1 v2
+  | FTuge => Val.notbool (Val.cmpf Clt v1 v2)
+  | FToge => Val.cmpf Cge v1 v2
+  | FTult => Val.notbool (Val.cmpf Cge v1 v2)
+  end.
+
+Definition arith_eval_r n :=
+  match n with
+  | Ploadsymbol s ofs => Genv.symbol_address ge s ofs
+  end
+.
+
+Definition arith_eval_rr n v :=
+  match n with
+  | Pmv => v
+  | Pnegw => Val.neg v
+  | Pnegl => Val.negl v
+  | Pcvtl2w => Val.loword v
+  | Psxwd => Val.longofint v
+  | Pzxwd => Val.longofintu v
+  | Pfnegd => Val.negf v
+  | Pfnegw => Val.negfs v
+  | Pfabsd => Val.absf v
+  | Pfabsw => Val.absfs v
+  | Pfnarrowdw => Val.singleoffloat v
+  | Pfwidenlwd => Val.floatofsingle v
+  | Pfloatwrnsz => match Val.singleofint v with Some f => f | _ => Vundef end
+  | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end
+  | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end
+  | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end
+  | Pfloatudrnsz_i32 => match Val.floatofintu v with Some f => f | _ => Vundef end
+  | Pfloatdrnsz_i32 => match Val.floatofint v with Some f => f | _ => Vundef end
+  | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end
+  | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end
+  | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end
+  | Pfixedudrzz => match Val.longuoffloat v with Some i => i | _ => Vundef end
+  | Pfixeddrzz_i32 => match Val.intoffloat v with Some i => i | _ => Vundef end
+  | Pfixedudrzz_i32 => match Val.intuoffloat v with Some i => i | _ => Vundef end
+  end.
+
+Definition arith_eval_ri32 n i :=
+  match n with
+  | Pmake => Vint i
+  end.
+
+Definition arith_eval_ri64 n i :=
+  match n with
+  | Pmakel => Vlong i
+  end.
+
+Definition arith_eval_rf32 n i :=
+  match n with
+  | Pmakefs => Vsingle i
+  end.
+
+Definition arith_eval_rf64 n i :=
+  match n with
+  | Pmakef => Vfloat i
+  end.
+
+Definition arith_eval_rrr n v1 v2 :=
+  match n with
+  | Pcompw c => compare_int c v1 v2
+  | Pcompl c => compare_long c v1 v2
+  | Pfcompw c => compare_single c v1 v2
+  | Pfcompl c => compare_float c v1 v2
+
+  | Paddw  => Val.add  v1 v2
+  | Psubw  => Val.sub  v1 v2
+  | Pmulw  => Val.mul  v1 v2
+  | Pandw  => Val.and  v1 v2
+  | Pnandw => Val.notint (Val.and v1 v2)
+  | Porw   => Val.or   v1 v2
+  | Pnorw  => Val.notint (Val.or v1 v2)
+  | Pxorw  => Val.xor  v1 v2
+  | Pnxorw => Val.notint (Val.xor v1 v2)
+  | Pandnw => Val.and (Val.notint v1) v2
+  | Pornw  => Val.or (Val.notint v1) v2
+  | Psrlw  => Val.shru v1 v2
+  | Psraw  => Val.shr  v1 v2
+  | Psllw  => Val.shl  v1 v2
+
+  | Paddl => Val.addl v1 v2
+  | Psubl => Val.subl v1 v2
+  | Pandl => Val.andl v1 v2
+  | Pnandl => Val.notl (Val.andl v1 v2)
+  | Porl  => Val.orl  v1 v2
+  | Pnorl  => Val.notl (Val.orl  v1 v2)
+  | Pxorl  => Val.xorl  v1 v2
+  | Pnxorl  => Val.notl (Val.xorl  v1 v2)
+  | Pandnl => Val.andl (Val.notl v1) v2
+  | Pornl  => Val.orl (Val.notl v1) v2
+  | Pmull => Val.mull v1 v2
+  | Pslll => Val.shll v1 v2
+  | Psrll => Val.shrlu v1 v2
+  | Psral => Val.shrl v1 v2
+
+  | Pfaddd => Val.addf v1 v2
+  | Pfaddw => Val.addfs v1 v2
+  | Pfsbfd => Val.subf v1 v2
+  | Pfsbfw => Val.subfs v1 v2
+  | Pfmuld => Val.mulf v1 v2
+  | Pfmulw => Val.mulfs v1 v2
+  end.
+
+Definition arith_eval_rri32 n v i :=
+  match n with
+  | Pcompiw c => compare_int c v (Vint i)
+  | Paddiw  => Val.add   v (Vint i)
+  | Pmuliw  => Val.mul   v (Vint i)
+  | Pandiw  => Val.and   v (Vint i)
+  | Pnandiw => Val.notint (Val.and  v (Vint i))
+  | Poriw   => Val.or    v (Vint i)
+  | Pnoriw  => Val.notint (Val.or v (Vint i))
+  | Pxoriw  => Val.xor   v (Vint i)
+  | Pnxoriw => Val.notint (Val.xor v (Vint i))
+  | Pandniw => Val.and (Val.notint v) (Vint i)
+  | Porniw  => Val.or (Val.notint v) (Vint i)
+  | Psraiw  => Val.shr   v (Vint i)
+  | Psrliw  => Val.shru  v (Vint i)
+  | Pslliw  => Val.shl   v (Vint i)
+  | Proriw  => Val.ror   v (Vint i)
+  | Psllil  => Val.shll  v (Vint i)
+  | Psrlil  => Val.shrlu v (Vint i)
+  | Psrail  => Val.shrl  v (Vint i)
+  end.
+
+Definition arith_eval_rri64 n v i :=
+  match n with
+  | Pcompil c => compare_long c v (Vlong i)
+  | Paddil  => Val.addl v (Vlong i)
+  | Pmulil  => Val.mull v (Vlong i)
+  | Pandil  => Val.andl v (Vlong i)
+  | Pnandil  => Val.notl (Val.andl v (Vlong i))
+  | Poril   => Val.orl  v (Vlong i)
+  | Pnoril   => Val.notl (Val.orl  v (Vlong i))
+  | Pxoril  => Val.xorl  v (Vlong i)
+  | Pnxoril  => Val.notl (Val.xorl  v (Vlong i))
+  | Pandnil => Val.andl (Val.notl v) (Vlong i)
+  | Pornil  => Val.orl (Val.notl v) (Vlong i)
+  end.
+
+Definition arith_eval_arrr n v1 v2 v3 :=
+  match n with
+  | Pmaddw => Val.add v1 (Val.mul v2 v3)
+  | Pmaddl => Val.addl v1 (Val.mull v2 v3)
+  | Pcmove bt =>
+    match cmp_for_btest bt with
+    | (Some c, Int)  =>
+      match Val.cmp_bool c v2 (Vint Int.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (Some c, Long) =>
+      match Val.cmpl_bool c v2 (Vlong Int64.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (None, _) => Vundef
+    end
+  | Pcmoveu bt =>
+    match cmpu_for_btest bt with
+    | (Some c, Int)  =>
+      match Val_cmpu_bool c v2 (Vint Int.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (Some c, Long) =>
+      match Val_cmplu_bool c v2 (Vlong Int64.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (None, _) => Vundef
+    end
+  end.
+
+Definition arith_eval_arri32 n v1 v2 v3 :=
+  match n with
+  | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3))
+  end.
+
+Definition arith_eval_arri64 n v1 v2 v3 :=
+  match n with
+  | Pmaddil => Val.addl v1 (Val.mull v2 (Vlong v3))
+  end.
+
 Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
   match ai with
-  | PArithR n d => rsw#d <- (arith_eval_r ge n)
+  | PArithR n d => rsw#d <- (arith_eval_r n)
 
   | PArithRR n d s => rsw#d <- (arith_eval_rr n rsr#s)
 
@@ -66,11 +1056,20 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
   | PArithARRI64 n d s i => rsw#d <- (arith_eval_arri64 n rsr#d rsr#s i)
   end.
 
+Definition eval_offset (ofs: offset) : res ptrofs :=
+  match ofs with
+  | Ofsimm n => OK n
+  | Ofslow id delta => 
+      match (Genv.symbol_address ge id delta) with
+      | Vptr b ofs => OK ofs
+      | _ => Error (msg "Asmblock.eval_offset")
+      end
+  end.
+
 (** * load/store *)
 
-(* TODO: factoriser ? *)
 Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) :=
-  match (eval_offset ge ofs) with
+  match (eval_offset ofs) with
   | OK ptr => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with
               | None => Stuck
               | Some v => Next (rsw#d <- v) mw
@@ -85,7 +1084,7 @@ Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem)
   end.
 
 Definition parexec_store_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a: ireg) (ofs: offset) :=
-  match (eval_offset ge ofs) with
+  match (eval_offset ofs) with
   | OK ptr => match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with
               | None => Stuck
               | Some m' => Next rsw m'
@@ -99,11 +1098,34 @@ Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem
   | Some m' => Next rsw m'
   end.
 
-(* rem: parexec_store = exec_store *)
+Definition load_chunk n :=
+  match n with
+  | Plb => Mint8signed
+  | Plbu => Mint8unsigned
+  | Plh => Mint16signed
+  | Plhu => Mint16unsigned
+  | Plw => Mint32
+  | Plw_a => Many32
+  | Pld => Mint64
+  | Pld_a => Many64
+  | Pfls => Mfloat32
+  | Pfld => Mfloat64
+  end.
+
+Definition store_chunk n :=
+  match n with
+  | Psb => Mint8unsigned
+  | Psh => Mint16unsigned
+  | Psw => Mint32
+  | Psw_a => Many32
+  | Psd => Mint64
+  | Psd_a => Many64
+  | Pfss => Mfloat32
+  | Pfsd => Mfloat64
+  end.
 
 (** * basic instructions *)
 
-(* TODO: factoriser ? *)
 Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
   match bi with
   | PArith ai => Next (parexec_arith_instr ai rsr rsw) mw
@@ -159,14 +1181,40 @@ Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) :=
      end
   end.
 
-(** Manipulations over the [PC] register: continuing with the next
-  instruction ([nextblock]) or branching to a label ([goto_label]). *)
+(** 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.
+  apply Pos.eq_dec.
+Qed.
+
 
-(* TODO: factoriser ? *)
-Definition par_nextblock size_b (rs: regset) :=
-  rs#PC <- (Val.offset_ptr rs#PC size_b).
 
-(* TODO: factoriser ? *)
+(** Note: copy-paste from Machblock *)
+Definition is_label (lbl: label) (bb: bblock) : bool :=
+  if in_dec lbl (header bb) then true else false.
+
+Lemma is_label_correct_true lbl bb:
+  List.In lbl (header bb) <-> is_label lbl bb = true. 
+Proof.
+  unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
+Qed.
+
+Lemma is_label_correct_false lbl bb:
+  ~(List.In lbl (header bb)) <-> is_label lbl bb = false. 
+Proof.
+  unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
+Qed.
+
+
+
+(** 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
+  | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb'
+  end.
+
 Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem) :=
   match label_pos lbl 0 (fn_blocks f) with
   | None => Stuck
@@ -182,7 +1230,7 @@ Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem)
 Warning: in m PC is assumed to be already pointing on the next instruction !
 
 *)
-(* TODO: factoriser ? *)
+
 Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem) (res: option bool) :=
   match res with
     | Some true  => par_goto_label f l rsr rsw mw
@@ -191,6 +1239,8 @@ 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.
 
@@ -257,18 +1307,19 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset)
 end.
 
 
-Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rsr rsw: regset) (mr mw: mem): outcome :=
+Definition incrPC size_b (rs: regset) :=
+  rs#PC <- (Val.offset_ptr rs#PC size_b).
+
+(** parallel execution of the exit instruction of a bundle *)
+Definition parexec_exit (f: function) ext size_b (rsr rsw: regset) (mw: mem) 
+  := parexec_control f ext (incrPC size_b rsr) rsw mw.
+
+Definition parexec_wio_bblock_aux f bdy ext size_b (rsr rsw: regset) (mr mw: mem): outcome :=
   match parexec_wio_body bdy rsr rsw mr mw with
-  | Next rsw mw =>
-    let rsr := par_nextblock size_b rsr in 
-    parexec_control f ext rsr rsw mw
+  | Next rsw mw => parexec_exit f ext size_b rsr rsw mw
   | Stuck => Stuck
   end.
 
-(** parallel in-order writes execution of bundles *)
-Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome :=
-  parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs rs m m.
-
 (** 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) /\ 
@@ -277,28 +1328,93 @@ Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (
       | Stuck => Stuck
       end.
 
-Lemma parexec_bblock_write_in_order f b rs m:
-   parexec_bblock f b rs m (parexec_wio_bblock f b rs m).
-Proof.
-   exists (body b). exists nil.
-   constructor 1.
-   - rewrite app_nil_r; auto.
-   - unfold parexec_wio_bblock.
-     destruct (parexec_wio_bblock_aux f _ _ _ _ _); simpl; auto.
-Qed.
-
 (** 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'.
 
 
-Local Hint Resolve parexec_bblock_write_in_order.
+(* 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
+  register is reserved as temporary, to be used by the generated RV32G
+  code.  *)
+
+
+(* FIXME - R16 and R32 are excluded *)
+Definition preg_of (r: mreg) : preg :=
+  match r with
+  | R0  => GPR0  | R1  => GPR1  | R2  => GPR2  | R3  => GPR3  | R4  => GPR4
+  | R5  => GPR5  | R6  => GPR6  | R7  => GPR7  | R8  => GPR8  | R9  => GPR9
+  | R10 => GPR10 | R11 => GPR11 (* | R12 => GPR12 | R13 => GPR13 | R14  => GPR14 *)
+  | R15 => GPR15 (* | R16 => GPR16 *) | R17 => GPR17 | R18 => GPR18 | R19  => GPR19
+  | R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24  => GPR24
+  | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29  => GPR29
+  | R30 => GPR30 | R31 => GPR31 (* | R32 => GPR32 *) | R33 => GPR33 | R34  => GPR34
+  | R35 => GPR35 | R36 => GPR36 | R37 => GPR37 | R38 => GPR38 | R39  => GPR39
+  | R40 => GPR40 | R41 => GPR41 | R42 => GPR42 | R43 => GPR43 | R44  => GPR44
+  | R45 => GPR45 | R46 => GPR46 | R47 => GPR47 | R48 => GPR48 | R49  => GPR49
+  | R50 => GPR50 | R51 => GPR51 | R52 => GPR52 | R53 => GPR53 | R54  => GPR54
+  | R55 => GPR55 | R56 => GPR56 | R57 => GPR57 | R58 => GPR58 | R59  => GPR59
+  | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63
+  end.
+
+(** Undefine all registers except SP and callee-save registers *)
+
+Definition undef_caller_save_regs (rs: regset) : regset :=
+  fun r =>
+    if preg_eq r SP
+    || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs))
+    then rs r
+    else Vundef.
+
+(* FIXME: comment not up-to-date *)
+(** 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. *)
+
+Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
+  | extcall_arg_reg: forall r,
+      extcall_arg rs m (R r) (rs (preg_of r))
+  | extcall_arg_stack: forall ofs ty bofs v,
+      bofs = Stacklayout.fe_ofs_arg + 4 * ofs ->
+      Mem.loadv (chunk_of_type ty) m
+                (Val.offset_ptr rs#SP (Ptrofs.repr bofs)) = Some v ->
+      extcall_arg rs m (S Outgoing ofs ty) v.
+
+Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop :=
+  | extcall_arg_one: forall l v,
+      extcall_arg rs m l v ->
+      extcall_arg_pair rs m (One l) v
+  | extcall_arg_twolong: forall hi lo vhi vlo,
+      extcall_arg rs m hi vhi ->
+      extcall_arg rs m lo vlo ->
+      extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo).
+
+Definition extcall_arguments
+    (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
+  list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args.
 
-Lemma det_parexec_write_in_order f b rs m rs' m':
-   det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'.
-Proof.
-   unfold det_parexec; auto.
-Qed.
+
+Definition loc_external_result (sg: signature) : rpair preg :=
+  map_rpair preg_of (loc_result sg).
+
+
+(** 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 *)
+    else if zeq pos 0 then Some b
+    else find_bblock (pos - (size b)) il
+  end.
+
+
+Inductive state: Type :=
+  | State: regset -> mem -> state.
+
+Definition nextblock (b:bblock) (rs: regset) :=
+  incrPC (Ptrofs.repr (size b)) rs.
 
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
@@ -331,10 +1447,54 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State rs m) t (State rs' m')
   .
 
+
+(** parallel in-order writes execution of bundles *)
+Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome :=
+  parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs rs m m.
+
+
+Lemma parexec_bblock_write_in_order f b rs m:
+   parexec_bblock f b rs m (parexec_wio_bblock f b rs m).
+Proof.
+   exists (body b). exists nil.
+   constructor 1.
+   - rewrite app_nil_r; auto.
+   - unfold parexec_wio_bblock.
+     destruct (parexec_wio_bblock_aux f _ _ _ _ _); simpl; auto.
+Qed.
+
+
+Local Hint Resolve parexec_bblock_write_in_order.
+
+Lemma det_parexec_write_in_order f b rs m rs' m':
+   det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'.
+Proof.
+   unfold det_parexec; auto.
+Qed.
+
 End RELSEM.
 
 (** Execution of whole programs. *)
 
+(** Execution of whole programs. *)
+
+Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall m0,
+      let ge := Genv.globalenv p in
+      let rs0 :=
+        (Pregmap.init Vundef)
+        # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero)
+        # SP <- Vnullptr
+        # RA <- Vnullptr in
+      Genv.init_mem p = Some m0 ->
+      initial_state p (State rs0 m0).
+
+Inductive final_state: state -> int -> Prop :=
+  | final_state_intro: forall rs m r,
+      rs PC = Vnullptr ->
+      rs GPR0 = Vint r ->
+      final_state (State rs m) r.
+
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
@@ -402,4 +1562,4 @@ Ltac Det_WIO X :=
   inv H; rewrite H0 in *; eelim NOTNULL; eauto.
 - (* final states *)
   intros s r1 r2 H H0; inv H; inv H0. congruence.
-Qed.
\ No newline at end of file
+Qed.