(#156) - Un peu de cleaning et de doc

10 files changed, 53 insertions, 497 deletions

diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v
index 113f5d51..96571841 100644
--- a/mppa_k1c/Archi.v
+++ b/mppa_k1c/Archi.v
@@ -14,10 +14,9 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Architecture-dependent parameters for RISC-V *)
+(** Architecture-dependent parameters for MPPA K1c. Mostly copied from the Risc-V backend *)
 
 Require Import ZArith.
-(*From Flocq*)
 Require Import Binary Bits.
 
 Definition ptr64 := true.
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 620aa91e..1964e5f8 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -15,7 +15,13 @@
 (*                                                                     *)

 (* *********************************************************************)

 

-(** Abstract syntax and semantics for K1c assembly language. *)

+(** * Abstract syntax for K1c 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

+    We define [unfold : list bblock -> list instruction]

+    An Asm function is then defined as : [fn_sig], [fn_blocks], [fn_code], and a proof of [unfold fn_blocks = fn_code]

+    [fn_code] has no semantic. Instead, the semantic of Asm is given by using the AsmVLIW semantic on [fn_blocks] *)

 

 Require Import Coqlib.

 Require Import Maps.

@@ -57,10 +63,6 @@ Inductive instruction : Type :=
   | Psemi                                           (**r semi colon separating bundles *)

   | Pnop                                            (**r instruction that does nothing *)

 

-  (** builtins *)

-  | Pclzll (rd rs: ireg)

-  | Pstsud (rd rs1 rs2: ireg)

-

   (** Control flow instructions *)

   | Pget    (rd: ireg) (rs: preg)                   (**r get system register *)

   | Pset    (rd: preg) (rs: ireg)                   (**r set system register *)

@@ -101,6 +103,8 @@ Inductive instruction : Type :=
   | Pafaddw (addr: ireg) (incr_res: ireg)

   | Palclrd (dst: ireg) (addr: ireg)

   | Palclrw (dst: ireg) (addr: ireg)

+  | Pclzll (rd rs: ireg)

+  | Pstsud (rd rs1 rs2: ireg)

             

   (** Loads **)

   | Plb     (rd: ireg) (ra: ireg) (ofs: addressing)     (**r load byte *)

@@ -571,12 +575,6 @@ Definition genv := Genv.t fundef unit.
 

 Definition function_proj (f: function) := Asmvliw.mkfunction (fn_sig f) (fn_blocks f).

 

-(* 

-Definition fundef_proj (fu: fundef) : Asmblock.fundef := transf_fundef function_proj fu.

-

-Definition program_proj (p: program) : Asmblock.program := transform_program fundef_proj p.

- *)

-

 Definition fundef_proj (fu: fundef) : Asmvliw.fundef := 

   match fu with

   | Internal f => Internal (function_proj f)

@@ -650,35 +648,6 @@ Proof.
   rewrite transf_function_proj. auto.

 Qed.

 

-(* Definition transf_globdef (gd: globdef Asmblock.fundef unit) : globdef fundef unit :=

-  match gd with

-  | Gfun f => Gfun (transf_fundef f)

-  | Gvar gu => Gvar gu

-  end.

-

-Lemma transf_globdef_proj: forall gd, globdef_proj (transf_globdef gd) = gd.

-Proof.

-  intros gd. destruct gd as [f|v]; simpl; auto.

-  rewrite transf_fundef_proj; auto.

-Qed.

-

-Fixpoint transf_prog_defs (l: list (ident * globdef Asmblock.fundef unit))

-                            : list (ident * globdef fundef unit) :=

-  match l with

-  | nil => nil

-  | (i, gd) :: l => (i, transf_globdef gd) :: transf_prog_defs l

-  end.

-

-Lemma transf_prog_proj: forall p, prog_defs p = prog_defs_proj (transf_prog_defs (prog_defs p)).

-Proof.

-  intros p. destruct p as [defs pub main]. simpl.

-  induction defs; simpl; auto.

-  destruct a as [i gd]. simpl.

-  rewrite transf_globdef_proj.

-  congruence.

-Qed.

- *)

-

 Definition transf_program : Asmvliw.program -> program := transform_program transf_fundef.

 

 Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B),

@@ -716,7 +685,6 @@ Proof.
   intros. congruence.

 Qed.

 

-(* I think it is a special case of Asmblock -> Asm. Very handy to have *)

 Lemma match_program_transf:

   forall p tp, match_prog p tp -> transf_program p = tp.

 Proof.

diff --git a/mppa_k1c/Asmaux.v b/mppa_k1c/Asmaux.v
index 85359658..94b39f4e 100644
--- a/mppa_k1c/Asmaux.v
+++ b/mppa_k1c/Asmaux.v
@@ -1,5 +1,5 @@
 Require Import Asm.
 Require Import AST.
 
-(* Constant only needed by Asmexpandaux.ml *)
+(** Constant only needed by Asmexpandaux.ml *)
 Program Definition dummy_function := {| fn_code := nil; fn_sig := signature_main; fn_blocks := nil |}.

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 0a25e81a..9b4489c5 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -15,7 +15,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Abstract syntax and semantics for K1c assembly language. *)
+(** Sequential block semantics for K1c assembly. The syntax is given in AsmVLIW *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -172,7 +172,6 @@ Proof.
 Qed.
 
 Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try (left; discriminate); try (right; discriminate)).
-(* Local Obligation Tactic := bblock_auto_correct. *)
 
 Lemma Istrue_proof_irrelevant (b: bool): forall (p1 p2:Is_true b), p1=p2.
 Proof.
@@ -250,9 +249,6 @@ Proof.
   intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity.
 Qed.
 
-
-
-
 (** * Sequential Semantics of basic blocks *)
 Section RELSEM.
 
@@ -302,29 +298,8 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
 
 Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome := par_goto_label f lbl rs rs m.
 
-(** Evaluating a branch 
-
-Warning: in m PC is assumed to be already pointing on the next instruction !
-
-*)
 Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome := par_eval_branch f l rs rs m res.
 
-(** 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.
-
-    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. *)
-
 Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome := parexec_control ge f oc rs rs m.
 
 Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome :=
@@ -368,16 +343,11 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State rs m) t (State rs' m')
   .
 
-
-
 End RELSEM.
 
-
-
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
-
 Definition data_preg (r: preg) : bool :=
   match r with
   | RA  => false
@@ -386,4 +356,3 @@ Definition data_preg (r: preg) : bool :=
   | IR _   => true
   | PC     => false
   end.
-
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index a7fa5cff..2d144bb6 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1,3 +1,10 @@
+(** * Translation from Asmblock 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 *)
+
 Require Import AST.
 Require Import Asmblock.
 Require Import Asmblockgenproof0.
@@ -17,6 +24,8 @@ Require Import Chunks.
 
 Open Scope impure.
 
+(** Definition of L *)
+
 Module P<: ImpParam.
 Module R := Pos.
 
@@ -459,18 +468,6 @@ Qed.
 Hint Resolve op_eq_correct: wlp.
 Global Opaque op_eq_correct.
 
-
-(* QUICK FIX WITH struct_eq *)
-
-(* Definition op_eq (o1 o2: op): ?? bool := struct_eq o1 o2. 
-
-Theorem op_eq_correct o1 o2: 
- WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2.
-Proof.
-  wlp_simplify.
-Qed.
-*)
-
 End IMPPARAM.
 
 End P.
@@ -550,7 +547,7 @@ Proof.
   - unfold ppos. unfold pmem. discriminate.
 Qed.
 
-(** Inversion functions, used for debugging *)
+(** Inversion functions, used for debug traces *)
 
 Definition pos_to_ireg (p: R.t) : option gpreg :=
   match p with
@@ -574,9 +571,6 @@ Definition inv_ppos (p: R.t) : option preg :=
        end
   end.
 
-
-(** Traduction Asmblock -> Asmblockdeps *)
-
 Notation "a @ b" := (Econs a b) (at level 102, right associativity).
 
 Definition trans_control (ctl: control) : inst :=
@@ -720,7 +714,7 @@ Proof.
   intros. congruence.
 Qed.
 
-(** Parallelizability of a bblock (bundle) *)
+(** Parallelizability test of a bblock (bundle), and bisimulation of the Asmblock and L parallel semantics *)
 
 Module PChk := ParallelChecks L PosPseudoRegSet.
 
@@ -1162,7 +1156,7 @@ Proof.
   destruct (prun_iw _ _ _ _); simpl; eauto.
 Qed.
 
-(* sequential execution *)
+(** sequential execution *)
 Theorem bisimu_basic ge fn bi rs m s:
   Ge = Genv ge fn ->
   match_states (State rs m) s ->
@@ -1264,7 +1258,6 @@ Qed.
 
 End SECT_PAR.
 
-
 Section SECT_BBLOCK_EQUIV.
 
 Variable Ge: genv.
@@ -1294,6 +1287,8 @@ Proof.
   * discriminate.
 Qed.
 
+(** Used for debug traces *)
+
 Definition gpreg_name (gpr: gpreg) :=
   match gpr with
   | GPR0 => Str ("GPR0") | GPR1 => Str ("GPR1") | GPR2 => Str ("GPR2") | GPR3 => Str ("GPR3") | GPR4 => Str ("GPR4")
@@ -1645,4 +1640,4 @@ Definition bblock_simub: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock
 Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
 Proof.
  eapply (pure_bblock_simu_test_correct true).
-Qed.
\ No newline at end of file
+Qed.
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index e5b9b35a..7e415c2a 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -15,7 +15,8 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Translation from Machblock to K1c assembly language (Asmblock) *)
+(** * Translation from Machblock to K1c assembly language (Asmblock) 
+    Inspired from the Mach->Asm pass of other backends, but adapted to the block structure *)
 
 Require Archi.
 Require Import Coqlib Errors.
@@ -41,23 +42,15 @@ Definition ireg_of (r: mreg) : res ireg :=
 Definition freg_of (r: mreg) : res freg :=
   match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end.
 
-(*
-(** Decomposition of 32-bit integer constants.  They are split into either
-  small signed immediates that fit in 12-bits, or, if they do not fit,
-  into a (20-bit hi, 12-bit lo) pair where lo is sign-extended. *)
-
-*)
 Inductive immed32 : Type :=
   | Imm32_single (imm: int).
 
 Definition make_immed32 (val: int) := Imm32_single val.
 
-(** Likewise, for 64-bit integer constants. *)
 Inductive immed64 : Type :=
   | Imm64_single (imm: int64)
 .
 
-(* For now, let's suppose all instructions of K1c can handle 64-bits immediate *)
 Definition make_immed64 (val: int64) := Imm64_single val.
 
 Notation "a ::g b" := (cons (A:=instruction) a b) (at level 49, right associativity).
@@ -66,12 +59,6 @@ Notation "a ::b lb" := ((bblock_single_inst a) :: lb) (at level 49, right associ
 Notation "a ++g b" := (app (A:=instruction) a b) (at level 49, right associativity).
 Notation "a @@ b" := (app a b) (at level 49, right associativity).
 
-(** Smart constructors for arithmetic operations involving
-  a 32-bit or 64-bit integer constant.  Depending on whether the
-  constant fits in 12 bits or not, one or several instructions
-  are generated as required to perform the operation
-  and prepended to the given instruction sequence [k]. *)
-
 Definition loadimm32 (r: ireg) (n: int) :=
   match make_immed32 n with
   | Imm32_single imm => Pmake r imm
@@ -92,10 +79,6 @@ Definition orimm32  := opimm32 Porw Poriw.
 Definition norimm32 := opimm32 Pnorw Pnoriw.
 Definition xorimm32 := opimm32 Pxorw Pxoriw.
 Definition nxorimm32 := opimm32 Pnxorw Pnxoriw.
-(*
-Definition sltimm32 := opimm32 Psltw Psltiw.
-Definition sltuimm32 := opimm32 Psltuw Psltiuw.
-*)
 
 Definition loadimm64 (r: ireg) (n: int64) :=
   match make_immed64 n with
@@ -118,11 +101,6 @@ Definition norimm64  := opimm64 Pnorl  Pnoril.
 Definition nandimm64 := opimm64 Pnandl Pnandil.
 Definition nxorimm64 := opimm64 Pnxorl  Pnxoril.
 
-(*
-Definition sltimm64 := opimm64 Psltl Psltil.
-Definition sltuimm64 := opimm64 Psltul Psltiul.
-*)
-
 Definition addptrofs (rd rs: ireg) (n: ptrofs) :=
   if Ptrofs.eq_dec n Ptrofs.zero then
     Pmv rd rs
@@ -170,19 +148,6 @@ Definition transl_opt_compuimm
     transl_compi c Unsigned r1 n lbl k
   .
 
-(* Definition transl_opt_compuimm
-    (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction :=
-  loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k). *)
-
-(*   match select_comp n c with
-  | Some Ceq => Pcbu BTweqz r1 lbl ::g k
-  | Some Cne => Pcbu BTwnez r1 lbl ::g k
-  | Some _   => nil (* Never happens *)
-  | None     => loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k)
-  end
-  .
- *)
-
 Definition select_compl (n: int64) (c: comparison) : option comparison :=
   if Int64.eq n Int64.zero then
     match c with
@@ -1052,7 +1017,7 @@ Definition make_epilogue (f: Machblock.function) (k: code) :=
   (loadind_ptr SP f.(fn_retaddr_ofs) GPRA) 
   ::g Pset RA GPRA ::g Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::g k.
 
-(** Translation of a Mach instruction. *)
+(** Translation of a Machblock instruction. *)
 
 Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
                               (ep: bool) (k: bcode) :=
@@ -1096,20 +1061,12 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co
         transl_cbranch cond args lbl nil
     | MBreturn =>
         OK (make_epilogue f (Pret ::g nil))
-      (*OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))*) 
     | MBjumptable arg tbl =>
       do r <- ireg_of arg;
       OK (Pjumptable r tbl ::g nil)
     end
   end.
 
-(* TODO - dans l'idée, transl_instr_control renvoie une liste d'instructions sous la forme :
-  * transl_instr_control _ _ _ = lb ++ (ctl :: nil), où lb est une liste de basics, ctl est un control_inst
-
-  Il faut arriver à exprimer cet aspect là ; extraire le lb, le rajouter dans le body ; et extraire le ctl
-  qu'on met dans le exit
-*)
-
 (** Translation of a code sequence *)
 
 Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
@@ -1120,8 +1077,7 @@ Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
   | _ => false
   end.
 
-(** This is the naive definition that we no longer use because it
-  is not tail-recursive.  It is kept as specification. *)
+(** This is the naive definition, which is not tail-recursive unlike the other backends *)
 
 Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) :=
   match il with
@@ -1147,20 +1103,11 @@ Definition transl_basic_code' (f: Machblock.function) (il: list Machblock.basic_
   transl_basic_rec f il it1p (fun c => OK c). *)
 
 (** Translation of a whole function.  Note that we must check
-  that the generated code contains less than [2^32] instructions,
+  that the generated code contains less than [2^64] instructions,
   otherwise the offset part of the [PC] code pointer could wrap
   around, leading to incorrect executions. *)
 
-(* Local Obligation Tactic := bblock_auto_correct. *)
-
-(* Program Definition gen_bblock_noctl (hd: list label) (c: list basic) :=
-  match c with
-  | nil => {| header := hd; body := Pnop::nil; exit := None |}
-  | i::c => {| header := hd; body := i::c; exit := None |}
-  end.
- *)
-
-(** Can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *)
+(* gen_bblocks can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *)
 Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instruction) :=
   match (extract_ctl ctl) with
   | None => 
@@ -1168,7 +1115,6 @@ Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instr
       | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil
       | i::c => {| header := hd; body := ((i::c) ++ extract_basic ctl); exit := None |} :: nil
       end
-(* gen_bblock_noctl hd (c ++ (extract_basic ctl)) :: nil *)
   | Some (PExpand (Pbuiltin ef args res)) =>
       match c with
       | nil => {| header := hd; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v
index 89d41017..decc3e2e 100644
--- a/mppa_k1c/Asmblockgenproof0.v
+++ b/mppa_k1c/Asmblockgenproof0.v
@@ -1,3 +1,9 @@
+(** * "block" version of Asmgenproof0
+
+    This module is largely adapted from Asmgenproof0.v of the other backends
+    It needs to stand apart because of the block structure, and the distinction control/basic that there isn't in the other backends
+    It has similar definitions than Asmgenproof0, but adapted to this new structure *)
+
 Require Import Coqlib.
 Require Intv.
 Require Import AST.
@@ -31,19 +37,13 @@ Lemma ireg_of_eq:
   forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
 Proof.
   unfold ireg_of; intros. destruct (preg_of r); inv H; auto.
-(*   destruct b. all: try discriminate.
-  inv H1. auto.
- *)Qed.
+Qed.
 
-(* FIXME - Replaced FR by IR for MPPA *)
 Lemma freg_of_eq:
   forall r r', freg_of r = OK r' -> preg_of r = IR r'.
 Proof.
   unfold freg_of; intros. destruct (preg_of r); inv H; auto.
-(*   destruct b. all: try discriminate.
-  inv H1. auto.
- *)Qed.
-
+Qed.
 
 Lemma preg_of_injective:
   forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2.
@@ -277,24 +277,6 @@ Proof.
   exploit preg_of_injective; eauto. congruence.
 Qed.
 
-(* Lemma agree_undef_regs2:
-  forall ms sp rl rs rs',
-  agree (Mach.undef_regs rl ms) sp rs ->
-  (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') ->
-  agree (Mach.undef_regs rl ms) sp rs'.
-Proof.
-  intros. destruct H. split; auto.
-  rewrite <- agree_sp0. apply H0; auto.
-  rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP.
-  intros. destruct (In_dec mreg_eq r rl).
-  rewrite Mach.undef_regs_same; auto.
-  rewrite H0; auto.
-  apply preg_of_data.
-  rewrite preg_notin_charact. intros; red; intros. elim n.
-  exploit preg_of_injective; eauto. congruence.
-Qed.
- *)
-
 Lemma agree_set_undef_mreg:
   forall ms sp rs r v rl rs',
   agree ms sp rs ->
@@ -607,15 +589,13 @@ Hypothesis transf_function_len:
   forall f tf, transf_function f = OK tf -> size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned.
 
 
-(* NB: the hypothesis in comment on [b] is not needed in the proof ! *)
 Lemma return_address_exists:
-  forall b f (* sg ros *) c, (* b.(MB.exit) = Some (MBcall sg ros) -> *) is_tail (b :: c) f.(MB.fn_code) ->
+  forall b f c, is_tail (b :: c) f.(MB.fn_code) ->
   exists ra, return_address_offset f c ra.
 Proof.
   intros. destruct (transf_function f) as [tf|] eqn:TF.
   + exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1).
     exploit transl_blocks_tail; eauto. intros (tc2 & ep2 & TR2 & TL2).
-(*     unfold return_address_offset. *)
     monadInv TR2.
     assert (TL3: is_tail x0 (fn_blocks tf)).
     { apply is_tail_trans with tc1; auto. 
@@ -632,7 +612,7 @@ Qed.
 End RETADDR_EXISTS.
 
 (** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points
-  within the Asm code generated by translating Mach function [f],
+  within the Asmblock code generated by translating Machblock function [f],
   and [tc] is the tail of the generated code at the position corresponding
   to the code pointer [pc]. *)
 
@@ -850,18 +830,6 @@ Proof.
   apply exec_straight_step with rs2 m2; auto.
 Qed.
 
-(* Theorem exec_straight_bblock:
-  forall rs1 m1 rs2 m2 rs3 m3 b,
-  exec_straight (body b) rs1 m1 nil rs2 m2 ->
-  exec_control_rel (exit b) b rs2 m2 rs3 m3 ->
-  exec_bblock_rel b rs1 m1 rs3 m3.
-Proof.
-  intros.
-  econstructor; eauto. unfold exec_bblock. erewrite exec_straight_body; eauto.
-  inv H0. auto.
-Qed. *)
-
-
 Lemma exec_straight_two:
   forall i1 i2 c rs1 m1 rs2 m2 rs3 m3,
   exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 ->
@@ -973,18 +941,6 @@ Proof.
   - reflexivity.
 Qed.
 
-(* Lemma exec_straight_pc':
-  forall c rs1 m1 rs2 m2,
-  exec_straight c rs1 m1 nil rs2 m2 ->
-  rs2 PC = rs1 PC.
-Proof.
-  induction c; intros; try (inv H; fail).
-  inv H.
-  - erewrite exec_basic_instr_pc; eauto.
-  - rewrite (IHc rs3 m3 rs2 m2); auto.
-    erewrite exec_basic_instr_pc; eauto.
-Qed. *)
-
 Lemma exec_straight_pc:
   forall c c' rs1 m1 rs2 m2,
   exec_straight c rs1 m1 c' rs2 m2 ->
@@ -997,25 +953,6 @@ Proof.
     erewrite exec_basic_instr_pc; eauto.
 Qed.
 
-(* Lemma exec_straight_through:
-  forall c i b lb rs1 m1 rs2 m2 rs2' m2',
-  bblock_basic_ctl c i = b ->
-  exec_straight c rs1 m1 nil rs2 m2 ->
-  nextblock b rs2 = rs2' -> m2 = m2' ->
-  exec_control ge fn i rs2' m2' = Next rs2' m2' -> (* if the control does not jump *)
-  exec_straight_blocks (b::lb) rs1 m1 lb rs2' m2'.
-Proof.
-  intros. subst. destruct i.
-  - constructor 1. 
-      + unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto.
-      + rewrite <- (exec_straight_pc c nil rs1 m1 rs2 m2'); auto.
-  - destruct c as [|i c]; try (inv H0; fail).
-    constructor 1.
-    + unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto.
-    + rewrite <- (exec_straight_pc (i ::i c) nil rs1 m1 rs2 m2'); auto.
-Qed.
- *)
-
 Lemma regset_same_assign (rs: regset) r:
   rs # r <- (rs r) = rs.
 Proof.
@@ -1034,8 +971,6 @@ Proof.
   simpl; auto. unfold nextblock, incrPC; simpl. Simpl. erewrite exec_straight_pc; eauto.
 Qed.
 
-
-
 (** The following lemmas show that straight-line executions
   (predicate [exec_straight_blocks]) correspond to correct Asm executions. *)
 
@@ -1086,7 +1021,6 @@ Qed.
 
 End STRAIGHTLINE.
 
-
 (** * Properties of the Machblock call stack *)
 
 Section MATCH_STACK.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index bc549b4a..e1e2b0b0 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -15,6 +15,8 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+(** * Proof of correctness for individual instructions *)
+
 Require Import Coqlib Errors Maps.
 Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op Locations Machblock Conventions.
@@ -86,31 +88,6 @@ Section CONSTRUCTORS.
 Variable ge: genv.
 Variable fn: function.
 
-(*
-(** 32-bit integer constants and arithmetic *)
-(*
-Lemma load_hilo32_correct:
-  forall rd hi lo k rs m,
-  exists rs',
-     exec_straight ge fn (load_hilo32 rd hi lo k) rs m k rs' m
-  /\ rs'#rd = Vint (Int.add (Int.shl hi (Int.repr 12)) lo)
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
-Proof.
-  unfold load_hilo32; intros. 
-  predSpec Int.eq Int.eq_spec lo Int.zero.
-- subst lo. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split. rewrite Int.add_zero. Simpl.
-  intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split. Simpl. 
-  intros; Simpl.
-Qed.
-*)
-
-*)
-
 Lemma loadimm32_correct:
   forall rd n k rs m,
   exists rs',
@@ -141,60 +118,6 @@ Proof.
   intros; Simpl.
 Qed.
 
-(*
-(*
-Lemma opimm32_correct:
-  forall (op: ireg -> ireg0 -> ireg0 -> instruction)
-         (opi: ireg -> ireg0 -> int -> instruction)
-         (sem: val -> val -> val) m,
-  (forall d s1 s2 rs,
-   exec_instr ge fn (op d s1 s2) rs m = Next (nextinstr (rs#d <- (sem rs##s1 rs##s2))) m) ->
-  (forall d s n rs,
-   exec_instr ge fn (opi d s n) rs m = Next (nextinstr (rs#d <- (sem rs##s (Vint n)))) m) ->
-  forall rd r1 n k rs,
-  r1 <> RTMP ->
-  exists rs',
-     exec_straight ge fn (opimm32 op opi rd r1 n k) rs m k rs' m
-  /\ rs'#rd = sem rs##r1 (Vint n)
-  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
-Proof.
-  intros. unfold opimm32. generalize (make_immed32_sound n); intros E.
-  destruct (make_immed32 n). 
-- subst imm. econstructor; split. 
-  apply exec_straight_one. rewrite H0. simpl; eauto. auto.
-  split. Simpl. intros; Simpl.
-- destruct (load_hilo32_correct RTMP hi lo (op rd r1 RTMP :: k) rs m)
-  as (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one. 
-  rewrite H; eauto. auto.
-  split. Simpl. simpl. rewrite B, C, E. auto. congruence. congruence.
-  intros; Simpl. 
-Qed.
-
-(** 64-bit integer constants and arithmetic *)
-
-Lemma load_hilo64_correct:
-  forall rd hi lo k rs m,
-  exists rs',
-     exec_straight ge fn (load_hilo64 rd hi lo k) rs m k rs' m
-  /\ rs'#rd = Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo)
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
-Proof.
-  unfold load_hilo64; intros. 
-  predSpec Int64.eq Int64.eq_spec lo Int64.zero.
-- subst lo. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split. rewrite Int64.add_zero. Simpl.
-  intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split. Simpl. 
-  intros; Simpl.
-Qed.
-*)
-*)
-
 Lemma opimm64_correct:
   forall (op: arith_name_rrr)
          (opi: arith_name_rri64)
@@ -215,18 +138,6 @@ Proof.
 - subst imm. econstructor; split. 
   apply exec_straight_one. rewrite H0. simpl; eauto. auto.
   split. Simpl. intros; Simpl.
-(*
-- destruct (load_hilo64_correct RTMP hi lo (op rd r1 RTMP :: k) rs m)
-  as (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one. 
-  rewrite H; eauto. auto.
-  split. Simpl. simpl. rewrite B, C, E. auto. congruence. congruence.
-  intros; Simpl. 
-- subst imm. econstructor; split. 
-  eapply exec_straight_two. simpl; eauto. rewrite H. simpl; eauto. auto. auto.
-  split. Simpl. intros; Simpl.
-*)
 Qed.
 
 (** Add offset to pointer *)
@@ -252,35 +163,6 @@ Proof.
   rewrite Ptrofs.of_int64_to_int64 by auto. auto.
 Qed.
 
-(*
-(*
-Lemma addptrofs_correct_2:
-  forall rd r1 n k (rs: regset) m b ofs,
-  r1 <> RTMP -> rs#r1 = Vptr b of
-s ->
-  exists rs',
-     exec_straight ge fn (addptrofs rd r1 n k) rs m k rs' m
-  /\ rs'#rd = Vptr b (Ptrofs.add ofs n)
-  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
-Proof.
-  intros. exploit (addptrofs_correct rd r1 n); eauto. intros (rs' & A & B & C).
-  exists rs'; intuition eauto. 
-  rewrite H0 in B. inv B. auto.
-Qed.
-
-(** Translation of conditional branches *)
-
-Remark branch_on_RTMP:
-  forall normal lbl (rs: regset) m b,
-  rs#RTMP = Val.of_bool (eqb normal b) ->
-  exec_instr ge fn (if normal then Pbnew RTMP X0 lbl else Pbeqw RTMP X0 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. 
-Qed.
-*)
-*)
-
 Ltac ArgsInv :=
   repeat (match goal with
   | [ H: Error _ = OK _ |- _ ] => discriminate
@@ -1522,99 +1404,6 @@ Proof.
   exploit transl_cond_nofloat32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
 Qed.
 
-(*
-(*
-+ (* cmpf *)
-  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
-  fold (Val.cmpf c0 (rs x) (rs x0)).
-  set (v := Val.cmpf c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
-  split; intros; Simpl.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_float_correct with (v := Val.notbool v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-+ (* notcmpf *)
-  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
-  rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)).
-  set (v := Val.cmpf c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_float_correct with (v := v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto.
-  split; intros; Simpl.
-+ (* cmpfs *)
-  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
-  fold (Val.cmpfs c0 (rs x) (rs x0)).
-  set (v := Val.cmpfs c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
-  split; intros; Simpl.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_single_correct with (v := Val.notbool v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-+ (* notcmpfs *)
-  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
-  rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)).
-  set (v := Val.cmpfs c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_single_correct with (v := v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
-  split; intros; Simpl.
-*)
-*)
-
-(** Some arithmetic properties. *)
-
-(* Remark cast32unsigned_from_cast32signed:
-  forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)).
-Proof.
-  intros. apply Int64.same_bits_eq; intros. 
-  rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto.
-  rewrite Int.bits_signed by tauto. fold (Int.testbit i i0).
-  change Int.zwordsize with 32.
-  destruct (zlt i0 32). auto. apply Int.bits_above. auto.
-Qed.
-
-Lemma cast32signed_correct:
-  forall (d s: ireg) (k: code) (rs: regset) (m: mem),
-  exists rs': regset,
-    exec_straight ge (cast32signed d s ::g k) rs m k rs' m
- /\ Val.lessdef (Val.longofint (rs s)) (rs' d)
- /\ (forall r: preg, r <> PC -> r <> d -> rs' r = rs r).
-Proof.
-  intros. unfold cast32signed. destruct (ireg_eq d s).
-- econstructor; split.
-  + apply exec_straight_one. simpl. eauto with asmgen.
-  + split.
-    * rewrite e. Simpl.
-    * intros. destruct r; Simpl.
-- econstructor; split.
-  + apply exec_straight_one. simpl. eauto with asmgen.
-  + split.
-    * Simpl.
-    * intros. destruct r; Simpl.
-Qed. *)
-
 (* Translation of arithmetic operations *)
 
 Ltac SimplEval H :=
@@ -1868,33 +1657,6 @@ Proof.
 + econstructor; econstructor; econstructor; econstructor; split.
   apply exec_straight_opt_refl. 
   split; auto. simpl. subst imm. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
-(*
-+ econstructor; econstructor; econstructor; split. 
-  constructor. eapply exec_straight_two. 
-  simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. destruct (rs base); auto; simpl. rewrite SF. simpl.
-  rewrite Ptrofs.add_assoc. f_equal. f_equal. 
-  rewrite <- (Ptrofs.of_int64_to_int64 SF ofs). rewrite EQ. 
-  symmetry; auto with ptrofs.
-+ econstructor; econstructor; econstructor; split. 
-  constructor. eapply exec_straight_two. 
-  simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold eval_offset. destruct (rs base); auto; simpl. rewrite SF. simpl.
-  rewrite Ptrofs.add_zero. subst imm. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
-(* 32 bits part, irrelevant for us
-- generalize (make_immed32_sound (Ptrofs.to_int ofs)); intros EQ.
-  destruct (make_immed32 (Ptrofs.to_int ofs)).
-+ econstructor; econstructor; econstructor; split.
-  apply exec_straight_opt_refl. 
-  split; auto. simpl. subst imm. rewrite Ptrofs.of_int_to_int by auto. auto.
-+ econstructor; econstructor; econstructor; split. 
-  constructor. eapply exec_straight_two. 
-  simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. destruct (rs base); auto; simpl. rewrite SF. simpl.
-  rewrite Ptrofs.add_assoc. f_equal. f_equal. 
-  rewrite <- (Ptrofs.of_int_to_int SF ofs). rewrite EQ. 
-  symmetry; auto with ptrofs.
-*)*)
 Qed.
 
 
@@ -2555,8 +2317,8 @@ Proof.
           { eapply A2. }
           { apply exec_straight_one. simpl.
             rewrite (C2 SP) by auto with asmgen. rewrite <- (sp_val _ _ rs1 AG1). simpl; rewrite LP'.
-            rewrite FREE'. eauto. (* auto. *) } }
-      * split. (* apply agree_nextinstr.  *)apply agree_set_other; auto with asmgen. 
+            rewrite FREE'. eauto. } }
+      * split. apply agree_set_other; auto with asmgen. 
     apply agree_change_sp with (Vptr stk soff).
     apply agree_exten with rs; auto. intros; rewrite C2; auto with asmgen.
     eapply parent_sp_def; eauto.
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index e7e21a18..e0878c7d 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Correctness proof for RISC-V generation: main proof. *)
+(** Correctness proof for Asmgen *)
 
 Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
@@ -89,4 +89,4 @@ Module Asmgenproof0.
 
 Definition return_address_offset := return_address_offset.
 
-End Asmgenproof0.
\ No newline at end of file
+End Asmgenproof0.
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index c6dd85f4..72584d2a 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -17,8 +17,6 @@
 
 (** 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.
 Require Import AST.
@@ -45,8 +43,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
@@ -152,9 +149,6 @@ Definition gpreg_o_expand (x : gpreg_o) : gpreg * gpreg * gpreg * gpreg :=
 Lemma gpreg_o_eq : forall (x y : gpreg_o), {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
@@ -173,7 +167,7 @@ End PregEq.
 
 Module Pregmap := EMap(PregEq).
 
-(** Conventional names for stack pointer ([SP]) and return address ([RA]). *)
+(** 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.
@@ -188,9 +182,7 @@ Inductive btest: Type :=
   | 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 *)
+  | 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 *)
@@ -251,16 +243,7 @@ Definition offset : Type := ptrofs.
 
 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 
-*)
+(** Instructions to be expanded in control-flow *)
 Inductive ex_instruction : Type :=
   (* Pseudo-instructions *)
   | Pbuiltin: external_function -> list (builtin_arg preg)