Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load

53 files changed, 1855 insertions, 601 deletions

diff --git a/.gitignore b/.gitignore
index 9b5167ef..eb11c837 100644
--- a/.gitignore
+++ b/.gitignore
@@ -45,15 +45,12 @@
 /riscV/ConstpropOp.v
 /riscV/SelectOp.v
 /riscV/SelectLong.v
-<<<<<<< HEAD
 /mppa_k1c/ConstpropOp.v
 /mppa_k1c/SelectOp.v
 /mppa_k1c/SelectLong.v
-=======
 /aarch64/ConstpropOp.v
 /aarch64/SelectOp.v
 /aarch64/SelectLong.v
->>>>>>> e1725209b2b4401adc63ce5238fa5db7c134609c
 /backend/SelectDiv.v
 /backend/SplitLong.v
 /cparser/Parser.v
diff --git a/Makefile b/Makefile
index f0a2dedc..6f2a786e 100644
--- a/Makefile
+++ b/Makefile
@@ -80,6 +80,7 @@ BACKEND=\
   Tailcall.v Tailcallproof.v \
   Inlining.v Inliningspec.v Inliningproof.v \
   Renumber.v Renumberproof.v \
+  Duplicate.v Duplicateproof.v \
   RTLtyping.v \
   Kildall.v Liveness.v \
   ValueDomain.v ValueAOp.v ValueAnalysis.v \
diff --git a/backend/Duplicate.v b/backend/Duplicate.v
new file mode 100644
index 00000000..3ad37c83
--- /dev/null
+++ b/backend/Duplicate.v
@@ -0,0 +1,198 @@
+(** RTL node duplication using external oracle. Used to form superblock
+  structures *)
+
+Require Import AST RTL Maps Globalenvs.
+Require Import Coqlib Errors Op.
+
+Local Open Scope error_monad_scope.
+Local Open Scope positive_scope.
+
+(** External oracle returning the new RTL code (entry point unchanged),
+    along with the new entrypoint, and a mapping of new nodes to old nodes *)
+Axiom duplicate_aux: function -> code * node * (PTree.t node).
+
+Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux".
+
+(** * Verification of node duplications *)
+
+Definition verify_is_copy dupmap n n' :=
+  match dupmap!n' with
+  | None => Error(msg "verify_is_copy None")
+  | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end
+  end.
+
+Fixpoint verify_is_copy_list dupmap ln ln' :=
+  match ln with
+  | n::ln => match ln' with
+             | n'::ln' => do u <- verify_is_copy dupmap n n';
+                          verify_is_copy_list dupmap ln ln'
+             | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end
+  | nil => match ln' with
+          | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'")
+          | nil => OK tt end
+  end.
+
+Definition verify_mapping_entrypoint dupmap (f f': function): res unit :=
+  verify_is_copy dupmap (fn_entrypoint f) (fn_entrypoint f').
+
+Lemma product_eq {A B: Type} :
+  (forall (a b: A), {a=b} + {a<>b}) ->
+  (forall (c d: B), {c=d} + {c<>d}) ->
+  forall (x y: A+B), {x=y} + {x<>y}.
+Proof.
+  intros H H'. intros. decide equality.
+Qed.
+
+(** FIXME Ideally i would like to put this in AST.v but i get an "illegal application"
+ * error when doing so *)
+Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}.
+Proof.
+  intros.
+  apply (builtin_arg_eq Pos.eq_dec).
+Defined.
+Global Opaque builtin_arg_eq_pos.
+
+Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}.
+Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed.
+Global Opaque builtin_res_eq_pos.
+
+Definition verify_match_inst dupmap inst tinst :=
+  match inst with
+  | Inop n => match tinst with Inop n' => do u <- verify_is_copy dupmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end
+
+  | Iop op lr r n => match tinst with
+      Iop op' lr' r' n' =>
+          do u <- verify_is_copy dupmap n n';
+          if (eq_operation op op') then
+            if (list_eq_dec Pos.eq_dec lr lr') then
+              if (Pos.eq_dec r r') then
+                OK tt
+              else Error (msg "Different r in Iop")
+            else Error (msg "Different lr in Iop")
+          else Error(msg "Different operations in Iop")
+      | _ => Error(msg "verify_match_inst Inop") end
+
+  | Iload m a lr r n => match tinst with
+      | Iload m' a' lr' r' n' =>
+          do u <- verify_is_copy dupmap n n';
+          if (chunk_eq m m') then
+            if (eq_addressing a a') then
+              if (list_eq_dec Pos.eq_dec lr lr') then
+                if (Pos.eq_dec r r') then OK tt
+                else Error (msg "Different r in Iload")
+              else Error (msg "Different lr in Iload")
+            else Error (msg "Different addressing in Iload")
+          else Error (msg "Different mchunk in Iload")
+      | _ => Error (msg "verify_match_inst Iload") end
+
+  | Istore m a lr r n => match tinst with
+      | Istore m' a' lr' r' n' =>
+          do u <- verify_is_copy dupmap n n';
+          if (chunk_eq m m') then
+            if (eq_addressing a a') then
+              if (list_eq_dec Pos.eq_dec lr lr') then
+                if (Pos.eq_dec r r') then OK tt
+                else Error (msg "Different r in Istore")
+              else Error (msg "Different lr in Istore")
+            else Error (msg "Different addressing in Istore")
+          else Error (msg "Different mchunk in Istore")
+      | _ => Error (msg "verify_match_inst Istore") end
+
+  | Icall s ri lr r n => match tinst with
+      | Icall s' ri' lr' r' n' =>
+          do u <- verify_is_copy dupmap n n';
+          if (signature_eq s s') then
+            if (product_eq Pos.eq_dec ident_eq ri ri') then
+              if (list_eq_dec Pos.eq_dec lr lr') then
+                if (Pos.eq_dec r r') then OK tt
+                else Error (msg "Different r r' in Icall")
+              else Error (msg "Different lr in Icall")
+            else Error (msg "Different ri in Icall")
+          else Error (msg "Different signatures in Icall")
+      | _ => Error (msg "verify_match_inst Icall") end
+
+  | Itailcall s ri lr => match tinst with
+      | Itailcall s' ri' lr' =>
+          if (signature_eq s s') then
+            if (product_eq Pos.eq_dec ident_eq ri ri') then
+              if (list_eq_dec Pos.eq_dec lr lr') then OK tt
+              else Error (msg "Different lr in Itailcall")
+            else Error (msg "Different ri in Itailcall")
+          else Error (msg "Different signatures in Itailcall")
+      | _ => Error (msg "verify_match_inst Itailcall") end
+
+  | Ibuiltin ef lbar brr n => match tinst with
+      | Ibuiltin ef' lbar' brr' n' =>
+          do u <- verify_is_copy dupmap n n';
+          if (external_function_eq ef ef') then
+            if (list_eq_dec builtin_arg_eq_pos lbar lbar') then
+              if (builtin_res_eq_pos brr brr') then OK tt
+              else Error (msg "Different brr in Ibuiltin")
+            else Error (msg "Different lbar in Ibuiltin")
+          else Error (msg "Different ef in Ibuiltin")
+      | _ => Error (msg "verify_match_inst Ibuiltin") end
+
+  | Icond cond lr n1 n2 => match tinst with
+      | Icond cond' lr' n1' n2' =>
+          do u1 <- verify_is_copy dupmap n1 n1';
+          do u2 <- verify_is_copy dupmap n2 n2';
+          if (eq_condition cond cond') then
+            if (list_eq_dec Pos.eq_dec lr lr') then OK tt
+            else Error (msg "Different lr in Icond")
+          else Error (msg "Different cond in Icond")
+      | _ => Error (msg "verify_match_inst Icond") end
+
+  | Ijumptable r ln => match tinst with
+      | Ijumptable r' ln' =>
+          do u <- verify_is_copy_list dupmap ln ln';
+          if (Pos.eq_dec r r') then OK tt
+          else Error (msg "Different r in Ijumptable")
+      | _ => Error (msg "verify_match_inst Ijumptable") end
+
+  | Ireturn or => match tinst with
+      | Ireturn or' =>
+          if (option_eq Pos.eq_dec or or') then OK tt
+          else Error (msg "Different or in Ireturn")
+      | _ => Error (msg "verify_match_inst Ireturn") end
+  end.
+
+Definition verify_mapping_mn dupmap f f' (m: positive*positive) :=
+  let (tn, n) := m in
+  match (fn_code f)!n with
+  | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code f)!n")
+  | Some inst => match (fn_code f')!tn with
+                 | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code xf)!tn")
+                 | Some tinst => verify_match_inst dupmap inst tinst
+                 end
+  end.
+
+Fixpoint verify_mapping_mn_rec dupmap f f' lm :=
+  match lm with
+  | nil => OK tt
+  | m :: lm => do u <- verify_mapping_mn dupmap f f' m;
+               do u2 <- verify_mapping_mn_rec dupmap f f' lm;
+               OK tt
+  end.
+
+Definition verify_mapping_match_nodes dupmap (f f': function): res unit :=
+  verify_mapping_mn_rec dupmap f f' (PTree.elements dupmap).
+
+(** Verifies that the [dupmap] of the translated function [f'] is giving correct information in regards to [f] *)
+Definition verify_mapping dupmap (f f': function) : res unit :=
+  do u <- verify_mapping_entrypoint dupmap f f';
+  do v <- verify_mapping_match_nodes dupmap f f'; OK tt.
+
+(** * Entry points *)
+
+Definition transf_function (f: function) : res function :=
+  let (tcte, dupmap) := duplicate_aux f in
+  let (tc, te) := tcte in
+  let f' := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in
+  do u <- verify_mapping dupmap f f';
+  OK f'.
+
+Definition transf_fundef (f: fundef) : res fundef :=
+  transf_partial_fundef transf_function f.
+
+Definition transf_program (p: program) : res program :=
+  transform_partial_program transf_fundef p.
\ No newline at end of file
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
new file mode 100644
index 00000000..9ff2ae55
--- /dev/null
+++ b/backend/Duplicateaux.ml
@@ -0,0 +1,13 @@
+open RTL
+open Maps
+
+let rec make_identity_ptree_rec = function
+| [] -> PTree.empty
+| m::lm -> let (n, _) = m in PTree.set n n (make_identity_ptree_rec lm)
+
+let make_identity_ptree f = make_identity_ptree_rec (PTree.elements (fn_code f))
+
+(* For now, identity function *)
+let duplicate_aux f =
+  let pTreeId = make_identity_ptree f
+  in (((fn_code f), (fn_entrypoint f)), pTreeId)
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
new file mode 100644
index 00000000..39b7a353
--- /dev/null
+++ b/backend/Duplicateproof.v
@@ -0,0 +1,494 @@
+(** Correctness proof for code duplication *)
+Require Import AST Linking Errors Globalenvs Smallstep.
+Require Import Coqlib Maps Events Values.
+Require Import Op RTL Duplicate.
+
+Local Open Scope positive_scope.
+
+(** * Definition of [match_states] (independently of the translation) *)
+
+(* est-ce plus simple de prendre dupmap: node -> node, avec un noeud hors CFG à la place de None ? *)
+Inductive match_inst (dupmap: PTree.t node): instruction -> instruction -> Prop :=
+  | match_inst_nop: forall n n',
+      dupmap!n' = (Some n) -> match_inst dupmap (Inop n) (Inop n')
+  | match_inst_op: forall n n' op lr r,
+      dupmap!n' = (Some n) -> match_inst dupmap (Iop op lr r n) (Iop op lr r n')
+  | match_inst_load: forall n n' m a lr r,
+      dupmap!n' = (Some n) -> match_inst dupmap (Iload m a lr r n) (Iload m a lr r n')
+  | match_inst_store: forall n n' m a lr r,
+      dupmap!n' = (Some n) -> match_inst dupmap (Istore m a lr r n) (Istore m a lr r n')
+  | match_inst_call: forall n n' s ri lr r,
+      dupmap!n' = (Some n) -> match_inst dupmap (Icall s ri lr r n) (Icall s ri lr r n')
+  | match_inst_tailcall: forall s ri lr,
+      match_inst dupmap (Itailcall s ri lr) (Itailcall s ri lr)
+  | match_inst_builtin: forall n n' ef la br,
+      dupmap!n' = (Some n) -> match_inst dupmap (Ibuiltin ef la br n) (Ibuiltin ef la br n')
+  | match_inst_cond: forall ifso ifso' ifnot ifnot' c lr,
+      dupmap!ifso' = (Some ifso) -> dupmap!ifnot' = (Some ifnot) ->
+      match_inst dupmap (Icond c lr ifso ifnot) (Icond c lr ifso' ifnot')
+  | match_inst_jumptable: forall ln ln' r,
+      list_forall2 (fun n n' => (dupmap!n' = (Some n))) ln ln' ->
+      match_inst dupmap (Ijumptable r ln) (Ijumptable r ln')
+  | match_inst_return: forall or, match_inst dupmap (Ireturn or) (Ireturn or).
+
+Record match_function dupmap f f': Prop := {
+  dupmap_correct: forall n n', dupmap!n' = Some n ->
+    (forall i, (fn_code f)!n = Some i -> exists i', (fn_code f')!n' = Some i' /\ match_inst dupmap i i');
+  dupmap_entrypoint: dupmap!(fn_entrypoint f') = Some (fn_entrypoint f);
+  preserv_fnsig: fn_sig f = fn_sig f';
+  preserv_fnparams: fn_params f = fn_params f';
+  preserv_fnstacksize: fn_stacksize f = fn_stacksize f'
+}.
+
+Inductive match_fundef: RTL.fundef -> RTL.fundef -> Prop :=
+  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
+  | match_External ef: match_fundef (External ef) (External ef).
+
+Inductive match_stackframes: stackframe -> stackframe -> Prop :=
+  | match_stackframe_intro 
+      dupmap res f sp pc rs f' pc'
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc' = Some pc):
+      match_stackframes (Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs).
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_intro 
+      dupmap st f sp pc rs m st' f' pc'
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc' = Some pc):
+      match_states (State st f sp pc rs m) (State st' f' sp pc' rs m)
+  | match_states_call:
+    forall st st' f f' args m
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_fundef f f'),
+      match_states (Callstate st f args m) (Callstate st' f' args m)
+  | match_states_return:
+    forall st st' v m
+      (STACKS: list_forall2 match_stackframes st st'),
+      match_states (Returnstate st v m) (Returnstate st' v m).
+
+(** * Auxiliary properties *)
+
+
+Theorem transf_function_preserves:
+  forall f f',
+  transf_function f = OK f' ->
+     fn_sig f = fn_sig f' /\ fn_params f = fn_params f' /\ fn_stacksize f = fn_stacksize f'.
+Proof.
+  intros. unfold transf_function in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H.
+  repeat (split; try reflexivity).
+Qed.
+
+
+Lemma verify_mapping_mn_rec_step:
+  forall dupmap lb b f f',
+  In b lb ->
+  verify_mapping_mn_rec dupmap f f' lb = OK tt ->
+  verify_mapping_mn dupmap f f' b = OK tt.
+Proof.
+  induction lb; intros.
+  - monadInv H0. inversion H.
+  - inversion H.
+    + subst. monadInv H0. destruct x. assumption.
+    + monadInv H0. destruct x0. eapply IHlb; assumption.
+Qed.
+
+Lemma verify_is_copy_correct:
+  forall dupmap n n',
+  verify_is_copy dupmap n n' = OK tt ->
+  dupmap ! n' = Some n.
+Proof.
+  intros. unfold verify_is_copy in H. destruct (_ ! n') eqn:REVM; [|inversion H].
+  destruct (n ?= p) eqn:NP; try (inversion H; fail).
+  eapply Pos.compare_eq in NP. subst.
+  reflexivity.
+Qed.
+
+Lemma verify_is_copy_list_correct:
+  forall dupmap ln ln',
+  verify_is_copy_list dupmap ln ln' = OK tt ->
+  list_forall2 (fun n n' => dupmap ! n' = Some n) ln ln'.
+Proof.
+  induction ln.
+  - intros. destruct ln'; monadInv H. constructor.
+  - intros. destruct ln'; monadInv H. destruct x. apply verify_is_copy_correct in EQ.
+    eapply IHln in EQ0. constructor; assumption.
+Qed.
+
+Lemma verify_match_inst_correct:
+  forall dupmap i i',
+  verify_match_inst dupmap i i' = OK tt ->
+  match_inst dupmap i i'.
+Proof.
+  intros. unfold verify_match_inst in H.
+  destruct i; try (inversion H; fail).
+(* Inop *)
+  - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
+    constructor; eauto.
+(* Iop *)
+  - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
+    destruct (eq_operation _ _); try discriminate.
+    destruct (list_eq_dec _ _ _); try discriminate.
+    destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst.
+    constructor. assumption.
+(* Iload *)
+  - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
+    destruct (chunk_eq _ _); try discriminate.
+    destruct (eq_addressing _ _); try discriminate.
+    destruct (list_eq_dec _ _ _); try discriminate.
+    destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst.
+    constructor. assumption.
+(* Istore *)
+  - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
+    destruct (chunk_eq _ _); try discriminate.
+    destruct (eq_addressing _ _); try discriminate.
+    destruct (list_eq_dec _ _ _); try discriminate.
+    destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst.
+    constructor. assumption.
+(* Icall *)
+  - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
+    destruct (signature_eq _ _); try discriminate.
+    destruct (product_eq _ _ _ _); try discriminate.
+    destruct (list_eq_dec _ _ _); try discriminate.
+    destruct (Pos.eq_dec _ _); try discriminate. subst.
+    constructor. assumption.
+(* Itailcall *)
+  - destruct i'; try (inversion H; fail).
+    destruct (signature_eq _ _); try discriminate.
+    destruct (product_eq _ _ _ _); try discriminate.
+    destruct (list_eq_dec _ _ _); try discriminate. subst. clear H.
+    constructor.
+(* Ibuiltin *)
+  - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
+    destruct (external_function_eq _ _); try discriminate.
+    destruct (list_eq_dec _ _ _); try discriminate.
+    destruct (builtin_res_eq_pos _ _); try discriminate. subst.
+    constructor. assumption.
+(* Icond *)
+  - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
+    destruct x0. eapply verify_is_copy_correct in EQ1.
+    destruct (eq_condition _ _); try discriminate.
+    destruct (list_eq_dec _ _ _); try discriminate. subst.
+    constructor; assumption.
+(* Ijumptable *)
+  - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_list_correct in EQ.
+    destruct (Pos.eq_dec _ _); try discriminate. subst.
+    constructor. assumption.
+(* Ireturn *)
+  - destruct i'; try (inversion H; fail).
+    destruct (option_eq _ _ _); try discriminate. subst. clear H.
+    constructor.
+Qed.
+
+
+Lemma verify_mapping_mn_correct mp n n' i f f' tc:
+  mp ! n' = Some n ->
+  (fn_code f) ! n = Some i ->
+  (fn_code f') = tc ->
+  verify_mapping_mn mp f f' (n', n) = OK tt ->
+  exists i',
+     tc ! n' = Some i'
+  /\ match_inst mp i i'.
+Proof.
+  unfold verify_mapping_mn; intros H H0 H1 H2. rewrite H0 in H2. clear H0. rewrite H1 in H2. clear H1.
+  destruct (tc ! n') eqn:TCN; [| inversion H2].
+  exists i0. split; auto.
+  eapply verify_match_inst_correct. assumption.
+Qed.
+
+
+Lemma verify_mapping_mn_rec_correct:
+  forall mp n n' i f f' tc,
+  mp ! n' = Some n ->
+  (fn_code f) ! n = Some i ->
+  (fn_code f') = tc ->
+  verify_mapping_mn_rec mp f f' (PTree.elements mp) = OK tt ->
+  exists i',
+     tc ! n' = Some i'
+  /\ match_inst mp i i'.
+Proof.
+  intros. exploit PTree.elements_correct. eapply H. intros IN.
+  eapply verify_mapping_mn_rec_step in H2; eauto.
+  eapply verify_mapping_mn_correct; eauto.
+Qed.
+
+Theorem transf_function_correct f f':
+    transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
+Proof.
+  unfold transf_function.
+  intros TRANSF.
+  destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te).
+  monadInv TRANSF.
+  unfold verify_mapping in EQ. monadInv EQ.
+  exists mp; constructor 1; simpl; auto.
+  + (* correct *) 
+  intros until n'. intros REVM i FNC.
+  unfold verify_mapping_match_nodes in EQ. simpl in EQ. destruct x1.
+  eapply verify_mapping_mn_rec_correct; eauto.
+  simpl; eauto.
+  + (* entrypoint *)
+  intros. unfold verify_mapping_entrypoint in EQ0. simpl in EQ0.
+  eapply verify_is_copy_correct; eauto.
+  destruct x0; auto.
+Qed.
+
+Lemma transf_fundef_correct f f':
+  transf_fundef f = OK f' -> match_fundef f f'.
+Proof.
+  intros TRANSF; destruct f; simpl; monadInv TRANSF.
+  + exploit transf_function_correct; eauto.
+    intros (dupmap & MATCH_F).
+    eapply match_Internal; eauto.
+  + eapply match_External.
+Qed.
+
+(** * Preservation proof *)
+
+Definition match_prog (p tp: program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
+Proof.
+  intros. eapply match_transform_partial_program_contextual; eauto.
+Qed.
+
+Section PRESERVATION.
+
+Variable prog: program.
+Variable tprog: program.
+
+Hypothesis TRANSL: match_prog prog tprog.
+
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof.
+  rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
+Qed.
+
+(* UNUSED LEMMA ?
+Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z.
+Proof.
+  unfold Senv.equiv. intuition congruence.
+Qed.
+*)
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof.
+  eapply (Genv.senv_match TRANSL).
+Qed.
+
+Lemma functions_translated:
+  forall (v: val) (f: fundef),
+  Genv.find_funct ge v = Some f ->
+  exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge v = Some tf /\ linkorder cunit prog.
+Proof.
+  intros. exploit (Genv.find_funct_match TRANSL); eauto.
+  intros (cu & tf & A & B & C).
+  repeat eexists; intuition eauto.
+  + unfold incl; auto.
+  + eapply linkorder_refl.
+Qed.
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
+Proof.
+  intros.
+  exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
+Qed.
+
+Lemma function_sig_translated:
+  forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f.
+Proof.
+  intros. destruct f.
+  - simpl in H. monadInv H. simpl. symmetry. apply transf_function_preserves. assumption.
+  - simpl in H. monadInv H. reflexivity.
+Qed.
+
+Lemma list_nth_z_dupmap:
+  forall dupmap ln ln' (pc pc': node) val,
+  list_nth_z ln val = Some pc ->
+  list_forall2 (fun n n' => dupmap!n' = Some n) ln ln' ->
+  exists pc',
+     list_nth_z ln' val = Some pc'
+  /\ dupmap!pc' = Some pc.
+Proof.
+  induction ln; intros until val; intros LNZ LFA.
+  - inv LNZ.
+  - inv LNZ. destruct (zeq val 0) eqn:ZEQ.
+    + inv H0. destruct ln'; inv LFA.
+      simpl. exists p. split; auto.
+    + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto.
+      intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence.
+Qed.
+
+Theorem transf_initial_states:
+  forall s1, initial_state prog s1 ->
+  exists s2, initial_state tprog s2 /\ match_states s1 s2.
+Proof.
+  intros. inv H.
+  exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
+  eexists. split.
+  - econstructor; eauto.
+    + eapply (Genv.init_mem_transf_partial TRANSL); eauto.
+    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
+      symmetry. eapply match_program_main. eauto.
+    + destruct f.
+      * monadInv TRANSF. rewrite <- H3. symmetry; eapply transf_function_preserves. assumption.
+      * monadInv TRANSF. assumption.
+  - constructor; eauto.
+    + constructor. 
+    + apply transf_fundef_correct; auto.
+Qed.
+
+Theorem transf_final_states:
+  forall s1 s2 r,
+  match_states s1 s2 -> final_state s1 r -> final_state s2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
+
+Theorem step_simulation:
+  forall s1 t s1', step ge s1 t s1' ->
+  forall s2 (MS: match_states s1 s2),
+  exists s2',
+     step tge s2 t s2'
+  /\ match_states s1' s2'.
+Proof.
+  Local Hint Resolve transf_fundef_correct.
+  induction 1; intros; inv MS.
+(* Inop *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H2 & H3).
+    inv H3.
+    eexists. split.
+    + eapply exec_Inop; eauto.
+    + econstructor; eauto.
+(* Iop *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H2 & H3). inv H3.
+    pose symbols_preserved as SYMPRES.
+    eexists. split.
+    + eapply exec_Iop; eauto. erewrite eval_operation_preserved; eauto.
+    + econstructor; eauto.
+(* Iload *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H2 & H3). inv H3.
+    pose symbols_preserved as SYMPRES.
+    eexists. split.
+    + eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto.
+    + econstructor; eauto.
+(* Istore *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H2 & H3). inv H3.
+    pose symbols_preserved as SYMPRES.
+    eexists. split.
+    + eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto.
+    + econstructor; eauto.
+(* Icall *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H2 & H3). inv H3.
+    pose symbols_preserved as SYMPRES.
+    destruct ros.
+    * simpl in H0. apply functions_translated in H0.
+      destruct H0 as (tf & cunit & TFUN & GFIND & LO).
+      eexists. split.
+      + eapply exec_Icall. eassumption. simpl. eassumption.
+        apply function_sig_translated. assumption.
+      + repeat (econstructor; eauto).
+    * simpl in H0. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate.
+      apply function_ptr_translated in H0. destruct H0 as (tf & GFF & TF).
+      eexists. split.
+      + eapply exec_Icall. eassumption. simpl. rewrite symbols_preserved. rewrite GFS.
+        eassumption. apply function_sig_translated. assumption.
+      + repeat (econstructor; eauto).
+(* Itailcall *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H10 & H11). inv H11.
+    pose symbols_preserved as SYMPRES.
+    destruct ros.
+    * simpl in H0. apply functions_translated in H0.
+      destruct H0 as (tf & cunit & TFUN & GFIND & LO).
+      eexists. split.
+      + eapply exec_Itailcall. eassumption. simpl. eassumption.
+        apply function_sig_translated. assumption.
+        erewrite <- preserv_fnstacksize; eauto.
+      + repeat (constructor; auto).
+    * simpl in H0. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate.
+      apply function_ptr_translated in H0. destruct H0 as (tf & GFF & TF).
+      eexists. split.
+      + eapply exec_Itailcall. eassumption. simpl. rewrite symbols_preserved. rewrite GFS.
+        eassumption. apply function_sig_translated. assumption.
+        erewrite <- preserv_fnstacksize; eauto.
+      + repeat (constructor; auto).
+(* Ibuiltin *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H2 & H3). inv H3.
+    pose symbols_preserved as SYMPRES.
+    eexists. split.
+    + eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_preserved; eauto.
+      eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
+    + econstructor; eauto.
+(* Icond *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H2 & H3). inv H3.
+    pose symbols_preserved as SYMPRES.
+    eexists. split.
+    + eapply exec_Icond; eauto.
+    + econstructor; eauto. destruct b; auto.
+(* Ijumptable *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H2 & H3). inv H3.
+    pose symbols_preserved as SYMPRES.
+    exploit list_nth_z_dupmap; eauto. intros (pc'1 & LNZ & REVM).
+    eexists. split.
+    + eapply exec_Ijumptable; eauto.
+    + econstructor; eauto.
+(* Ireturn *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H2 & H3). inv H3.
+    pose symbols_preserved as SYMPRES.
+    eexists. split.
+    + eapply exec_Ireturn; eauto. erewrite <- preserv_fnstacksize; eauto.
+    + econstructor; eauto.
+(* exec_function_internal *)
+  - inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split.
+    + eapply exec_function_internal. erewrite <- preserv_fnstacksize; eauto.
+    + erewrite preserv_fnparams; eauto.
+      econstructor; eauto. apply dupmap_entrypoint. assumption.
+(* exec_function_external *)
+  - inversion TRANSF as [|]; subst. eexists. split.
+    + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+    + constructor. assumption.
+(* exec_return *)
+  - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split.
+    + constructor.
+    + inv H1. econstructor; eauto.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (semantics prog) (semantics tprog).
+Proof.
+  eapply forward_simulation_step with match_states.
+  - eapply senv_preserved.
+  - eapply transf_initial_states.
+  - eapply transf_final_states.
+  - eapply step_simulation.
+Qed.
+
+End PRESERVATION.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 92c18415..994d2652 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -321,7 +321,10 @@ Local Opaque mreg_type.
   + (* other ops *)
     destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans.
     econstructor; eauto.
-    apply wt_setreg. eapply Val.has_subtype; eauto.
+ 
+    apply wt_setreg; auto; try (apply wt_undef_regs; auto).
+    eapply Val.has_subtype; eauto.
+    
     change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto.
     red; intros; subst op. simpl in ISMOVE.
     destruct args; try discriminate. destruct args; discriminate.
diff --git a/common/AST.v b/common/AST.v
index bb8508b7..86cab287 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -17,7 +17,7 @@
   the abstract syntax trees of many of the intermediate languages. *)
 
 Require Import String.
-Require Import Coqlib Maps Errors Integers Floats.
+Require Import Coqlib Maps Errors Integers Floats BinPos.
 Require Archi.
 
 Set Implicit Arguments.
@@ -640,11 +640,28 @@ Inductive builtin_arg (A: Type) : Type :=
   | BA_splitlong (hi lo: builtin_arg A)
   | BA_addptr (a1 a2: builtin_arg A).
 
+Definition builtin_arg_eq {A: Type}:
+  (forall x y : A, {x = y} + {x <> y}) ->
+  forall (ba1 ba2: (builtin_arg A)), {ba1=ba2} + {ba1<>ba2}.
+Proof.
+  intro. generalize Integers.int_eq int64_eq float_eq float32_eq chunk_eq ptrofs_eq ident_eq.
+  decide equality.
+Defined.
+Global Opaque builtin_arg_eq.
+
 Inductive builtin_res (A: Type) : Type :=
   | BR (x: A)
   | BR_none
   | BR_splitlong (hi lo: builtin_res A).
 
+Definition builtin_res_eq {A: Type}:
+  (forall x y : A, {x = y} + {x <> y}) ->
+  forall (a b: builtin_res A), {a=b} + {a<>b}.
+Proof.
+  intro. decide equality.
+Defined.
+Global Opaque builtin_res_eq.
+
 Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident :=
   match a with
   | BA_loadglobal chunk id ofs => id :: nil
diff --git a/configure b/configure
index c4fcf511..9b5109b1 100755
--- a/configure
+++ b/configure
@@ -470,6 +470,7 @@ if test "$arch" = "mppa_k1c"; then
   system="linux"
 fi
 
+#
 # AArch64 (ARMv8 64 bits) Target Configuration
 #
 if test "$arch" = "aarch64"; then
@@ -567,14 +568,14 @@ missingtools=false
 echo "Testing Coq... " | tr -d '\n'
 coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
 case "$coq_ver" in
-  8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10)
+  8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
         if $ignore_coq_version; then
             echo "Warning: this version of Coq is unsupported, proceed at your own risks."
         else
-            echo "Error: CompCert requires one of the following Coq versions: 8.10, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0"
+            echo "Error: CompCert requires one of the following Coq versions: 8.10, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0"
             missingtools=true
         fi;;
   "")
@@ -910,6 +911,4 @@ cat <<EOF
     Coq development will not be installed
 EOF
 fi
-
 fi
-
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 0112a5ec..193d83c4 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -18,6 +18,7 @@
 type struct_passing_style =
   | SP_ref_callee                       (* by reference, callee takes copy *)
   | SP_ref_caller                       (* by reference, caller takes copy *)
+  | SP_value32_ref_callee               (* by value if <= 32 bits, by ref_callee otherwise *)
   | SP_split_args                       (* by value, as a sequence of ints *)
 
 type struct_return_style =
@@ -268,8 +269,9 @@ let mppa_k1c =
     bigendian = false;
     bitfields_msb_first = false; (* TO CHECK *)
     supports_unaligned_accesses = true;
-    struct_passing_style = SP_split_args;
-    struct_return_style = SR_int1248 }
+    struct_passing_style = SP_value32_ref_callee;
+    struct_return_style = SR_int1to4 }
+
 let aarch64 =
   { i32lpll64 with name = "aarch64";
                    struct_passing_style = SP_ref_callee; (* Wrong *)
diff --git a/cparser/Machine.mli b/cparser/Machine.mli
index 31726d7f..ea25c4f6 100644
--- a/cparser/Machine.mli
+++ b/cparser/Machine.mli
@@ -17,6 +17,7 @@
 type struct_passing_style =
   | SP_ref_callee                       (* by reference, callee takes copy *)
   | SP_ref_caller                       (* by reference, caller takes copy *)
+  | SP_value32_ref_callee               (* by value if <= 32 bits, by ref_callee otherwise *)
   | SP_split_args                       (* by value, as a sequence of ints *)
 
 type struct_return_style =
diff --git a/cparser/StructPassing.ml b/cparser/StructPassing.ml
index 5c6454f0..3aff090e 100644
--- a/cparser/StructPassing.ml
+++ b/cparser/StructPassing.ml
@@ -68,7 +68,16 @@ let classify_param env ty =
     match !struct_passing_style with
     | SP_ref_callee -> Param_unchanged
     | SP_ref_caller -> Param_ref_caller
-    | _ ->
+    | SP_value32_ref_callee ->
+      (match sizeof env ty, alignof env ty with
+      | Some sz, Some al ->
+          if (sz <= 4) then
+            Param_flattened ((sz+3)/4, sz, al) (* FIXME - why (sz+3)/4 ? *)
+          else
+            Param_unchanged
+      | _, _ -> Param_unchanged (* when parsing prototype with incomplete structure definition *)
+      )
+    | SP_split_args ->
       match sizeof env ty, alignof env ty with
       | Some sz, Some al ->
           Param_flattened ((sz + 3) / 4, sz, al)
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 7536e8ff..f948d595 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -38,6 +38,7 @@ Require RTLgen.
 Require Tailcall.
 Require Inlining.
 Require Renumber.
+Require Duplicate.
 Require Constprop.
 Require CSE.
 Require Deadcode.
@@ -60,6 +61,7 @@ Require RTLgenproof.
 Require Tailcallproof.
 Require Inliningproof.
 Require Renumberproof.
+Require Duplicateproof.
 Require Constpropproof.
 Require CSEproof.
 Require Deadcodeproof.
@@ -128,17 +130,18 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    @@ print (print_RTL 2)
    @@ time "Renumbering" Renumber.transf_program
    @@ print (print_RTL 3)
-   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
+  @@@ time "Duplicating" Duplicate.transf_program
    @@ print (print_RTL 4)
-   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
+   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
    @@ print (print_RTL 5)
-  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
+   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
    @@ print (print_RTL 6)
-  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
    @@ print (print_RTL 7)
-  @@@ time "Unused globals" Unusedglob.transform_program
+  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
    @@ print (print_RTL 8)
    @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
+  @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 9)
   @@@ time "Register allocation" Allocation.transf_program
    @@ print print_LTL
@@ -242,6 +245,7 @@ Definition CompCert's_passes :=
   ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog)
   ::: mkpass Inliningproof.match_prog
   ::: mkpass Renumberproof.match_prog
+  ::: mkpass Duplicateproof.match_prog
   ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog)
   ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog)
   ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog)
@@ -308,6 +312,7 @@ Proof.
   exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match.
   exists p8; split. apply Inliningproof.transf_program_match; auto.
   exists p9; split. apply Renumberproof.transf_program_match; auto.
+<<<<<<< HEAD
   exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match.
   exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match.
   exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match.
@@ -320,6 +325,20 @@ Proof.
   exists p18; split. apply CleanupLabelsproof.transf_program_match; auto.
   exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match.
   exists p20; split. apply Stackingproof.transf_program_match; auto.
+=======
+  exists p10; split. apply Duplicateproof.transf_program_match; auto.
+  exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match.
+  exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match.
+  exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match.
+  exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match.
+  exists p15; split. apply Unusedglobproof.transf_program_match; auto.
+  exists p16; split. apply Allocproof.transf_program_match; auto.
+  exists p17; split. apply Tunnelingproof.transf_program_match.
+  exists p18; split. apply Linearizeproof.transf_program_match; auto.
+  exists p19; split. apply CleanupLabelsproof.transf_program_match; auto.
+  exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match.
+  exists p21; split. apply Stackingproof.transf_program_match; auto.
+>>>>>>> origin/mppa-work
   exists tp; split. apply Asmgenproof.transf_program_match; auto.
   reflexivity.
 Qed.
@@ -390,6 +409,7 @@ Ltac DestructM :=
   eapply compose_forward_simulations.
     eapply Inliningproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations. eapply Duplicateproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct.
   eapply compose_forward_simulations.
diff --git a/lib/Floats.v b/lib/Floats.v
index 13350dd0..272efa52 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -16,7 +16,7 @@
 
 (** Formalization of floating-point numbers, using the Flocq library. *)
 
-Require Import Coqlib Zbits Integers.
+Require Import Coqlib Zbits Integers Axioms.
 (*From Flocq*)
 Require Import Binary Bits Core.
 Require Import IEEE754_extra.
@@ -27,8 +27,69 @@ Close Scope R_scope.
 Open Scope Z_scope.
 
 Definition float := binary64. (**r the type of IEE754 double-precision FP numbers *)
+
+Definition float_eq: forall (i1 i2: float), {i1=i2} + {i1<>i2}.
+Proof.
+  intros. destruct i1.
+(* B754_zero *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + apply eqb_prop in BEQ. subst. left. reflexivity.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_infinity *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + apply eqb_prop in BEQ. subst. left. reflexivity.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_nan *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + generalize (Pos.eq_dec pl pl0). intro. inv H.
+      ++ left. apply eqb_prop in BEQ. subst.
+         assert (e = e0) by (apply proof_irr). congruence.
+      ++ right. intro. inv H. contradiction.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_finite *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ; [apply eqb_prop in BEQ | apply eqb_false_iff in BEQ].
+    generalize (Pos.eq_dec m m0). intro. inv H.
+    generalize (Z.eq_dec e e1). intro. inv H.
+    1: { left. assert (e0 = e2) by (apply proof_irr). congruence. }
+    all: right; intro; inv H; contradiction.
+Qed.
+
 Definition float32 := binary32. (**r the type of IEE754 single-precision FP numbers *)
 
+Definition float32_eq: forall (i1 i2: float32), {i1=i2} + {i1<>i2}.
+Proof.
+  intros. destruct i1.
+(* B754_zero *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + apply eqb_prop in BEQ. subst. left. reflexivity.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_infinity *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + apply eqb_prop in BEQ. subst. left. reflexivity.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_nan *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + generalize (Pos.eq_dec pl pl0). intro. inv H.
+      ++ left. apply eqb_prop in BEQ. subst.
+         assert (e = e0) by (apply proof_irr). congruence.
+      ++ right. intro. inv H. contradiction.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_finite *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ; [apply eqb_prop in BEQ | apply eqb_false_iff in BEQ].
+    generalize (Pos.eq_dec m m0). intro. inv H.
+    generalize (Z.eq_dec e e1). intro. inv H.
+    1: { left. assert (e0 = e2) by (apply proof_irr). congruence. }
+    all: right; intro; inv H; contradiction.
+Qed.
+
 (** Boolean-valued comparisons *)
 
 Definition cmp_of_comparison (c: comparison) (x: option Datatypes.comparison) : bool :=
diff --git a/lib/Integers.v b/lib/Integers.v
index 3b6c35eb..3e78ee60 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -16,7 +16,7 @@
 (** Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *)
 
 Require Import Eqdep_dec Zquot Zwf.
-Require Import Coqlib Zbits.
+Require Import Coqlib Zbits Axioms.
 Require Archi.
 
 (** * Comparisons *)
@@ -29,6 +29,11 @@ Inductive comparison : Type :=
   | Cgt : comparison               (**r greater than *)
   | Cge : comparison.              (**r greater than or equal *)
 
+Definition comparison_eq: forall (x y: comparison), {x = y} + {x <> y}.
+Proof.
+  decide equality.
+Defined.
+
 Definition negate_comparison (c: comparison): comparison :=
   match c with
   | Ceq => Cne
@@ -4535,8 +4540,26 @@ End Int64.
 
 Strategy 0 [Wordsize_64.wordsize].
 
+Definition int_eq: forall (i1 i2: int), {i1=i2} + {i1<>i2}.
+Proof.
+  generalize Z.eq_dec. intros.
+  destruct i1. destruct i2. generalize (H intval intval0). intro.
+  inversion H0.
+  - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence.
+  - right. intro. inversion H2. contradiction.
+Qed.
+
 Notation int64 := Int64.int.
 
+Definition int64_eq: forall (i1 i2: int64), {i1=i2} + {i1<>i2}.
+Proof.
+  generalize Z.eq_dec. intros.
+  destruct i1. destruct i2. generalize (H intval intval0). intro.
+  inversion H0.
+  - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence.
+  - right. intro. inversion H2. contradiction.
+Qed.
+
 Global Opaque Int.repr Int64.repr Byte.repr.
 
 (** * Specialization to offsets in pointer values *)
@@ -4813,6 +4836,15 @@ Strategy 0 [Wordsize_Ptrofs.wordsize].
 
 Notation ptrofs := Ptrofs.int.
 
+Definition ptrofs_eq: forall (i1 i2: ptrofs), {i1=i2} + {i1<>i2}.
+Proof.
+  generalize Z.eq_dec. intros.
+  destruct i1. destruct i2. generalize (H intval intval0). intro.
+  inversion H0.
+  - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence.
+  - right. intro. inversion H2. contradiction.
+Qed.
+
 Global Opaque Ptrofs.repr.
 
 Hint Resolve Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans
diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v
index cdcf58c3..69b32c7c 100644
--- a/mppa_k1c/Archi.v
+++ b/mppa_k1c/Archi.v
@@ -17,7 +17,6 @@
 (** Architecture-dependent parameters for MPPA K1c. Mostly copied from the Risc-V backend *)
 
 Require Import ZArith List.
-(*From Flocq*)
 Require Import Binary Bits.
 
 Definition ptr64 := true.
diff --git a/mppa_k1c/Asmaux.v b/mppa_k1c/Asmaux.v
index 94b39f4e..891d1068 100644
--- a/mppa_k1c/Asmaux.v
+++ b/mppa_k1c/Asmaux.v
@@ -2,4 +2,4 @@ Require Import Asm.
 Require Import AST.
 
 (** Constant only needed by Asmexpandaux.ml *)
-Program Definition dummy_function := {| fn_code := nil; fn_sig := signature_main; fn_blocks := nil |}.

+Program Definition dummy_function := {| fn_code := nil; fn_sig := signature_main; fn_blocks := nil |}.
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 65792d13..c7cfe43c 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1665,11 +1665,17 @@ Hint Resolve bblock_simu_test_correct: wlp.
 
 Import UnsafeImpure.
 
-Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := unsafe_coerce (bblock_simu_test verb p1 p2).
+Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := 
+  match unsafe_coerce (bblock_simu_test verb p1 p2) with
+  | Some b => b
+  | None => false
+  end.
 
 Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
 Proof.
-   intros; unfold pure_bblock_simu_test. intros; eapply bblock_simu_test_correct; eauto.
+   unfold pure_bblock_simu_test. 
+   destruct (unsafe_coerce (bblock_simu_test verb p1 p2)) eqn: UNSAFE; try discriminate.
+   intros; subst. eapply bblock_simu_test_correct; eauto.
    apply unsafe_coerce_not_really_correct; eauto.
 Qed.
 
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index fd50f3b4..5825fd04 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -1112,10 +1112,12 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co
 
 Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
   match i with
+  | MBgetstack ofs ty dst => before && negb (mreg_eq dst MFP)
   | MBsetstack src ofs ty => before
   | MBgetparam ofs ty dst => negb (mreg_eq dst MFP)
   | MBop op args res => before && negb (mreg_eq res MFP)
-  | _ => false
+  | MBload chunk addr args dst => before && negb (mreg_eq dst MFP)
+  | MBstore chunk addr args res => before
   end.
 
 (** This is the naive definition, which is not tail-recursive unlike the other backends *)
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 6baca8c0..cdbaf16a 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -47,7 +47,6 @@ Lemma senv_preserved:
   Senv.equiv ge tge.

 Proof (Genv.senv_match TRANSF).

 

-

 Lemma functions_translated:

   forall b f,

   Genv.find_funct_ptr ge b = Some f ->

@@ -65,8 +64,6 @@ Proof.
   monadInv B. rewrite H0 in EQ; inv EQ; auto.

 Qed.

 

-(** * Properties of control flow *)

-

 Lemma transf_function_no_overflow:

   forall f tf,

   transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.

@@ -75,23 +72,7 @@ Proof.
   omega.

 Qed.

 

-(** The following lemmas show that the translation from Mach to Asm

-  preserves labels, in the sense that the following diagram commutes:

-<<

-                          translation

-        Mach code ------------------------ Asm instr sequence

-            |                                          |

-            | Mach.find_label lbl       find_label lbl |

-            |                                          |

-            v                                          v

-        Mach code tail ------------------- Asm instr seq tail

-                          translation

->>

-  The proof demands many boring lemmas showing that Asm constructor

-  functions do not introduce new labels.

-*)

-

-Section TRANSL_LABEL.

+Section TRANSL_LABEL. (* Lemmas on translation of MB.is_label into AB.is_label *)
 

 Lemma gen_bblocks_label:

   forall hd bdy ex tbb tc,

@@ -113,7 +94,7 @@ Proof.
   all: inv GENB; simpl; auto.

 Qed.

 

-Lemma in_dec_transl:

+Remark in_dec_transl:
   forall lbl hd,

   (if in_dec lbl hd then true else false) = (if MB.in_dec lbl hd then true else false).

 Proof.

@@ -226,7 +207,7 @@ Proof.
   rewrite H. auto.

 Qed.

 

-Lemma transl_find_label:

+Theorem transl_find_label:
   forall lbl f tf,

   transf_function f = OK tf ->

   match MB.find_label lbl f.(MB.fn_code) with

@@ -241,8 +222,8 @@ Qed.
 

 End TRANSL_LABEL.

 

-(** A valid branch in a piece of Mach code translates to a valid ``go to''

-  transition in the generated Asm code. *)

+(** A valid branch in a piece of Machblock code translates to a valid ``go to''
+  transition in the generated Asmblock code. *)
 

 Lemma find_label_goto_label:

   forall f tf lbl rs m c' b ofs,

@@ -270,48 +251,47 @@ Qed.
 

 (** Existence of return addresses *)

 

-(* 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. eapply Asmblockgenproof0.return_address_exists; eauto.

 

 - intros. monadInv H0.

   destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. monadInv EQ. simpl.

-(*   rewrite transl_code'_transl_code in EQ0. *)

-  exists x; exists true; split; auto. (*  unfold fn_code. *)

+  exists x; exists true; split; auto.
   repeat constructor.

-  - exact transf_function_no_overflow.

+- exact transf_function_no_overflow.
 Qed.

 

 (** * Proof of semantic preservation *)

 

-(** Semantic preservation is proved using simulation diagrams

+(** Semantic preservation is proved using a complex simulation diagram
   of the following form.

 <<

-           st1 --------------- st2

-            |                   |

-           t|                  *|t

-            |                   |

-            v                   v

-           st1'--------------- st2'

+                                     MB.step
+                      ---------------------------------------->
+                      header      body          exit
+                  st1 -----> st2 -----> st3 ------------------> st4
+                   |          |          |                       |
+                   |   (A)    |   (B)    |         (C)           |
+   match_codestate |          |          |                       |
+                   |  header  |   body1  |  body2                |  match_states
+                  cs1 -----> cs2 -----> cs3 ------> cs4          |
+                   |                  /                \  exit   |
+   match_asmstate  |   ---------------                  --->---  |
+                   |  /   match_asmstate                       \ |
+                  st'1 ---------------------------------------> st'2
+                                     AB.step                  *
 >>

-  The invariant is the [match_states] predicate below, which includes:

-- The Asm code pointed by the PC register is the translation of

-  the current Mach code sequence.

-- Mach register values and Asm register values agree.

-*)

-

-(** We need to show that, in the simulation diagram, we cannot

-  take infinitely many Mach transitions that correspond to zero

-  transitions on the Asm side.  Actually, all Mach transitions

-  correspond to at least one Asm transition, except the

-  transition from [Machsem.Returnstate] to [Machsem.State].

-  So, the following integer measure will suffice to rule out

-  the unwanted behaviour. *)

+  The invariant between each MB.step/AB.step is the [match_states] predicate below.
+  However, we also need to introduce an intermediary state [Codestate] which allows
+  us to reason on a finer grain, executing header, body and exit separately.
 

+  This [Codestate] consists in a state like [Asmblock.State], except that the
+  code is directly stored in the state, much like [Machblock.State]. It also features
+  additional useful elements to keep track of while executing a bblock.
+*)
 

 Remark preg_of_not_FP: forall r, negb (mreg_eq r MFP) = true -> IR FP <> preg_of r.

 Proof.

@@ -349,17 +329,18 @@ Inductive match_states: Machblock.state -> Asmvliw.state -> Prop :=
                    (Asmvliw.State rs m').

 

 Record codestate :=

-  Codestate {     pstate: state;

+  Codestate {     pstate: state;        (**r projection to Asmblock.state *)
                   pheader: list label;

-                  pbody1: list basic;

-                  pbody2: list basic;

-                  pctl: option control;

-                  fpok: bool;

-                  rem: list AB.bblock;

-                  cur: option bblock }.

-

-(*   | Codestate: state -> list AB.bblock -> option bblock -> codestate. *)

-

+                  pbody1: list basic;   (**r list of basic instructions coming from the translation of the Machblock body *)
+                  pbody2: list basic;   (**r list of basic instructions coming from the translation of the Machblock exit *)
+                  pctl: option control; (**r exit instruction, coming from the translation of the Machblock exit *)
+                  ep: bool;             (**r reflects the [ep] variable used in the translation *)
+                  rem: list AB.bblock;  (**r remaining bblocks to execute *)
+                  cur: bblock           (**r current bblock to execute - to keep track of its size when incrementing PC *)
+            }.
+
+(* The part that deals with Machblock <-> Codestate agreement
+ * Note about DXP: the property of [ep] only matters if the current block doesn't have a header, hence the condition *)
 Inductive match_codestate fb: Machblock.state -> codestate -> Prop :=

   | match_codestate_intro:

       forall s sp ms m rs0 m0 f tc ep c bb tbb tbc tbi

@@ -369,7 +350,6 @@ Inductive match_codestate fb: Machblock.state -> codestate -> Prop :=
         (TBC: transl_basic_code f (MB.body bb) (if MB.header bb then ep else false) = OK tbc)

         (TIC: transl_instr_control f (MB.exit bb) = OK tbi)

         (TBLS: transl_blocks f c false = OK tc)

-(*         (TRANS: transl_blocks f (bb::c) ep = OK (tbb::tc)) *)

         (AG: agree ms sp rs0)

         (DXP: (if MB.header bb then ep else false) = true -> rs0#FP = parent_sp s)

         ,

@@ -377,14 +357,15 @@ Inductive match_codestate fb: Machblock.state -> codestate -> Prop :=
         {|  pstate := (Asmvliw.State rs0 m0);

             pheader := (MB.header bb);

             pbody1 := tbc;

-            pbody2 := (extract_basic tbi);

+            pbody2 := extract_basic tbi;
             pctl := extract_ctl tbi;

-            fpok := ep;

+            ep := ep;
             rem := tc;

-            cur := Some tbb

+            cur := tbb
         |}

 .

 

+(* The part ensuring that the code in Codestate actually resides at [rs PC] *)
 Inductive match_asmstate fb: codestate -> Asmvliw.state -> Prop :=

   | match_asmstate_some:

       forall rs f tf tc m tbb ofs ep tbdy tex lhd

@@ -392,7 +373,6 @@ Inductive match_asmstate fb: codestate -> Asmvliw.state -> Prop :=
         (TRANSF: transf_function f = OK tf)

         (PCeq: rs PC = Vptr fb ofs)

         (TAIL: code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (tbb::tc))

-(*         (HDROK: header tbb = lhd) *)

         ,

       match_asmstate fb 

         {|  pstate := (Asmvliw.State rs m);

@@ -400,12 +380,13 @@ Inductive match_asmstate fb: codestate -> Asmvliw.state -> Prop :=
             pbody1 := tbdy;

             pbody2 := extract_basic tex;

             pctl := extract_ctl tex;

-            fpok := ep;

+            ep := ep;
             rem := tc;

-            cur := Some tbb |}

+            cur := tbb |}
         (Asmvliw.State rs m)

 .

 

+(* Useful for dealing with the many cases in some proofs *)
 Ltac exploreInst :=

   repeat match goal with

   | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var

@@ -417,12 +398,14 @@ Ltac exploreInst :=
   | [ H : Error _ = OK _ |- _ ] => inversion H

   end.

 

+(** Some translation properties *)
+
 Lemma transl_blocks_nonil:

   forall f bb c tc ep,

   transl_blocks f (bb::c) ep = OK tc ->

   exists tbb tc', tc = tbb :: tc'.

 Proof.

-  intros until ep. intros TLBS. monadInv TLBS. monadInv EQ. unfold gen_bblocks.

+  intros until ep0. intros TLBS. monadInv TLBS. monadInv EQ. unfold gen_bblocks.
   destruct (extract_ctl x2).

   - destruct c0; destruct i; simpl; eauto. destruct x1; simpl; eauto.

   - destruct x1; simpl; eauto.

@@ -469,7 +452,7 @@ Lemma transl_blocks_distrib:
   -> transl_block f bb (if MB.header bb then ep else false) = OK (tbb :: nil)

   /\ transl_blocks f c false = OK tc.

 Proof.

-  intros until ep. intros TLBS Hbuiltin.

+  intros until ep0. intros TLBS Hbuiltin.
   destruct bb as [hd bdy ex].

   monadInv TLBS. monadInv EQ.

   exploit no_builtin_preserved; eauto. intros Hectl. destruct Hectl.

@@ -584,6 +567,9 @@ Proof.
     * unfold transl_comp_notfloat32. exploreInst; try discriminate.

 Qed.

 

+(* Proving that one can decompose a [match_state] relation into a [match_codestate]
+   and a [match_asmstate], along with some helpful properties tying both relations together *)
+
 Theorem match_state_codestate:

   forall mbs abs s fb sp bb c ms m,

   (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->

@@ -596,7 +582,7 @@ Theorem match_state_codestate:
     /\ transl_blocks f (bb::c) ep = OK (tbb::tc)

     /\ body tbb = pbody1 cs ++ pbody2 cs

     /\ exit tbb = pctl cs

-    /\ cur cs = Some tbb /\ rem cs = tc

+    /\ cur cs = tbb /\ rem cs = tc
     /\ pstate cs = abs.

 Proof.

   intros until m. intros Hnobuiltin Hnotempty Hmbs MS. subst. inv MS.

@@ -611,7 +597,7 @@ Proof.
     eapply transl_instr_control_nobuiltin; eauto.

   intros (Hth & Htbdy & Htexit).

   exists {| pstate := (State rs m'); pheader := (Machblock.header bb); pbody1 := x; pbody2 := extract_basic x0;

-            pctl := extract_ctl x0; fpok := ep; rem := tc'; cur := Some tbb |}, fb, f, tbb, tc', ep.

+            pctl := extract_ctl x0; ep := ep0; rem := tc'; cur := tbb |}, fb, f, tbb, tc', ep0.
   repeat split. 1-2: econstructor; eauto.

   { destruct (MB.header bb). eauto. discriminate. } eauto.

   unfold transl_blocks. fold transl_blocks. unfold transl_block. rewrite EQ. simpl. rewrite EQ1; simpl.

@@ -624,7 +610,7 @@ Definition mb_remove_body (bb: MB.bblock) :=
 

 Lemma exec_straight_pnil:

   forall c rs1 m1 rs2 m2,

-  exec_straight tge c rs1 m1 (Pnop::gnil) rs2 m2 ->

+  exec_straight tge c rs1 m1 (Pnop ::g nil) rs2 m2 ->
   exec_straight tge c rs1 m1 nil rs2 m2.

 Proof.

   intros. eapply exec_straight_trans. eapply H. econstructor; eauto.

@@ -656,10 +642,9 @@ Lemma nextblock_preserves:
 Proof.

   intros. destruct r; try discriminate.

   subst. Simpl.

-(*   - subst. Simpl. *)

 Qed.

 

-Lemma cons3_app {A: Type}:

+Remark cons3_app {A: Type}:
   forall a b c (l: list A),

   a :: b :: c :: l = (a :: b :: c :: nil) ++ l.

 Proof.

@@ -693,36 +678,20 @@ Proof.
   induction lb; intros; simpl; congruence.

 Qed.

 

-(* Lemma goto_label_inv:

-  forall fn tbb l rs m b ofs,

-  rs PC = Vptr b ofs ->

-  goto_label fn l rs m = goto_label fn l (nextblock tbb rs) m.

-Proof.

-  intros.

-  unfold goto_label. rewrite nextblock_pc. unfold Val.offset_ptr. rewrite H.

-  exploreInst; auto.

-  unfold nextblock. rewrite Pregmap.gss.

-  

-Qed.

-

-

-Lemma exec_control_goto_label_inv:

-  exec_control tge fn (Some ctl) rs m = goto_label fn l rs m ->

-  exec_control tge fn (Some ctl) (nextblock tbb rs) m = goto_label fn l (nextblock tbb rs) m.

-Proof.

-Qed. *)

-

+(* See (C) in the diagram. The proofs are mostly adapted from the previous Mach->Asm proofs, but are
+   unfortunately quite cumbersome. To reproduce them, it's best to have a Coq IDE with you and see by
+   yourself the steps *)
 Theorem step_simu_control:

-  forall bb' fb fn s sp c ms' m' rs2 m2 E0 S'' rs1 m1 tbb tbdy2 tex cs2,

+  forall bb' fb fn s sp c ms' m' rs2 m2 t S'' rs1 m1 tbb tbdy2 tex cs2,
   MB.body bb' = nil ->

   (forall ef args res, MB.exit bb' <> Some (MBbuiltin ef args res)) ->

   Genv.find_funct_ptr tge fb = Some (Internal fn) ->

   pstate cs2 = (Asmvliw.State rs2 m2) ->

   pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex ->

-  cur cs2 = Some tbb ->

+  cur cs2 = tbb ->
   match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2 ->

   match_asmstate fb cs2 (Asmvliw.State rs1 m1) ->

-  exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') E0 S'' ->

+  exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') t S'' ->
   (exists rs3 m3 rs4 m4,

       exec_body tge tbdy2 rs2 m2 = Next rs3 m3

   /\  exec_control_rel tge fn tex tbb rs3 m3 rs4 m4

@@ -731,7 +700,7 @@ Proof.
   intros until cs2. intros Hbody Hbuiltin FIND Hpstate Hpbody1 Hpbody2 Hpctl Hcur MCS MAS ESTEP.

   inv ESTEP.

   - inv MCS. inv MAS. simpl in *.

-    inv Hcur. inv Hpstate.

+    inv Hpstate.
     destruct ctl.

     + (* MBcall *)

       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.

@@ -834,7 +803,6 @@ Proof.
 

       assert (f0 = f) by congruence. subst f0. assert (f1 = f) by congruence. subst f1. clear H11.

       remember (nextblock tbb rs2) as rs2'.

-      (* inv AT. monadInv H4. *)

       exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND'.

       assert (tf = fn) by congruence. subst tf.

       exploit find_label_goto_label.

@@ -853,7 +821,6 @@ Proof.
         assert (forall r : preg, r <> PC -> rs' r = rs2 r).

         { intros. destruct r.

           - destruct g. all: rewrite INV; Simpl; auto.

-(*           - destruct g. all: rewrite INV; Simpl; auto. *)

           - rewrite INV; Simpl; auto.

           - contradiction. }

         eauto with asmgen.

@@ -962,11 +929,8 @@ Proof.
       econstructor; eauto.

         unfold nextblock, incrPC. repeat apply agree_set_other; auto with asmgen.

 

-  - inv MCS. inv MAS. simpl in *. subst. inv Hpstate. inv Hcur.

-(*     exploit transl_blocks_distrib; eauto. (* rewrite <- H2. discriminate. *)

-    intros (TLB & TLBS).

- *) destruct bb' as [hd' bdy' ex']; simpl in *. subst.

-(*     unfold transl_block in TLB. simpl in TLB. unfold gen_bblocks in TLB; simpl in TLB. inv TLB. *)

+  - inv MCS. inv MAS. simpl in *. subst. inv Hpstate.
+    destruct bb' as [hd' bdy' ex']; simpl in *. subst.
     monadInv TBC. monadInv TIC. simpl in *. rewrite H5. rewrite H6.

     simpl. repeat eexists.

     econstructor. 4: instantiate (3 := false). all:eauto.

@@ -1023,7 +987,8 @@ Proof.
   all: eauto.

 Qed.

 

-Lemma step_simu_basic:

+(* Handling the individual instructions of theorem (B) in the above diagram. A bit less cumbersome, but still tough *)
+Theorem step_simu_basic:
   forall bb bb' s fb sp c ms m rs1 m1 ms' m' bi cs1 tbdy bdy,

   MB.header bb = nil -> MB.body bb = bi::(bdy) -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->

   bb' = {| MB.header := nil; MB.body := bdy; MB.exit := MB.exit bb |} ->

@@ -1032,7 +997,7 @@ Lemma step_simu_basic:
   match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->

   (exists rs2 m2 l cs2 tbdy',

        cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := tbdy'; pbody2 := pbody2 cs1;

-                pctl := pctl cs1; fpok := fp_is_parent (fpok cs1) bi; rem := rem cs1; cur := cur cs1 |}

+                pctl := pctl cs1; ep := fp_is_parent (ep cs1) bi; rem := rem cs1; cur := cur cs1 |}
     /\ tbdy = l ++ tbdy'

     /\ exec_body tge l rs1 m1 = Next rs2 m2

     /\ match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2).

@@ -1041,6 +1006,7 @@ Proof.
   simpl in *. inv Hpstate.

   rewrite Hbody in TBC. monadInv TBC.

   inv BSTEP.

+
   - (* MBgetstack *)

     simpl in EQ0.

     unfold Mach.load_stack in H.

@@ -1056,12 +1022,17 @@ Proof.
     repeat (split; auto).

       eapply basics_to_code_app; eauto.

     remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.

-(*     assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. }

-    rewrite <- Hheadereq. *) subst.

+    assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. }
+    subst. simpl in Hheadereq.
 

-    eapply match_codestate_intro; eauto. simpl. simpl in EQ. (*  { destruct (MB.header bb); auto. } *)

+    eapply match_codestate_intro; eauto.
+      { simpl. simpl in EQ. rewrite <- Hheadereq in EQ. assumption. }
     eapply agree_set_mreg; eauto with asmgen.

-    intro Hep. simpl in Hep. inv Hep.

+    intro Hep. simpl in Hep. 
+    destruct (andb_prop _ _ Hep). clear Hep.
+    rewrite <- Hheadereq in DXP. subst. rewrite <- DXP. rewrite Hrs'2. reflexivity.
+    discriminate. apply preg_of_not_FP; assumption. reflexivity.
+
   - (* MBsetstack *)

     simpl in EQ0.

     unfold Mach.store_stack in H.

@@ -1078,8 +1049,7 @@ Proof.
     repeat (split; auto).

       eapply basics_to_code_app; eauto.

     remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.

-(*     assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }

-    rewrite <- Hheadereq. *) subst.

+    subst.
     eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto.

 

     eapply agree_undef_regs; eauto with asmgen.

@@ -1095,10 +1065,9 @@ Proof.
     exploit Mem.loadv_extends. eauto. eexact H1. auto.

     intros [v' [C D]].

 

-  (* Opaque loadind. *)

-(*     left; eapply exec_straight_steps; eauto; intros. monadInv TR. *)

     monadInv EQ0. rewrite Hheader. rewrite Hheader in DXP.

-    destruct ep eqn:EPeq.

+    destruct ep0 eqn:EPeq.
+
   (* RTMP contains parent *)

     + exploit loadind_correct. eexact EQ1.

       instantiate (2 := rs1). rewrite DXP; eauto.

@@ -1113,14 +1082,14 @@ Proof.
       { eapply basics_to_code_app; eauto. }

       remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.

       assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. }

-      (* rewrite <- Hheadereq.  *)subst.

+      subst.
       eapply match_codestate_intro; eauto.

 

       eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.

       simpl; intros. rewrite R; auto with asmgen.

       apply preg_of_not_FP; auto.

 

-  (* GPR11 does not contain parent *)

+  (* RTMP does not contain parent *)
     + rewrite chunk_of_Tptr in A. 

       exploit loadind_ptr_correct. eexact A. intros [rs2 [P [Q R]]].

       exploit loadind_correct. eexact EQ1. instantiate (2 := rs2). rewrite Q. eauto.

@@ -1169,8 +1138,7 @@ Proof.
     repeat (split; auto).

       eapply basics_to_code_app; eauto.

     remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.

-(*     assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }

-    rewrite <- Hheadereq. *) subst.

+    subst.
     eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto.

     apply agree_set_undef_mreg with rs1; auto. 

     apply Val.lessdef_trans with v'; auto.

@@ -1197,12 +1165,15 @@ Local Transparent destroyed_by_op.
     repeat (split; auto).

       eapply basics_to_code_app; eauto.

     remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.

-(*     assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }

-    rewrite <- Hheadereq. *) subst.

+    assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
+    subst.
     eapply match_codestate_intro; eauto. simpl. simpl in EQ.

-

-    eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.

-    simpl; congruence.

+    rewrite <- Hheadereq in EQ. assumption.
+    eapply agree_set_mreg; eauto with asmgen.
+    intro Hep. simpl in Hep. 
+    destruct (andb_prop _ _ Hep). clear Hep.
+    subst. rewrite <- DXP. rewrite R; try discriminate. reflexivity.
+    apply preg_of_not_FP; assumption. reflexivity.
 

   - (* notrap1 cannot happen *)

     simpl in EQ0. unfold transl_load in EQ0.

@@ -1279,11 +1250,13 @@ Local Transparent destroyed_by_op.
     repeat (split; auto).

       eapply basics_to_code_app; eauto.

     remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.

+    assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
     subst.

     eapply match_codestate_intro; eauto. simpl. simpl in EQ.

-

+    rewrite <- Hheadereq in EQ. assumption.
     eapply agree_undef_regs; eauto with asmgen.

-    simpl; congruence.

+    intro Hep. simpl in Hep.
+    subst. rewrite <- DXP. rewrite Q; try discriminate. reflexivity. reflexivity.
 Qed.

 

 Lemma exec_body_trans:

@@ -1309,13 +1282,12 @@ Qed.
 Inductive exec_header: codestate -> codestate -> Prop :=

   | exec_header_cons: forall cs1,

       exec_header cs1 {| pstate := pstate cs1; pheader := nil; pbody1 := pbody1 cs1; pbody2 := pbody2 cs1;

-                          pctl := pctl cs1; fpok := (if pheader cs1 then fpok cs1 else false); rem := rem cs1;

-                          (* cur := match cur cs1 with None => None | Some bcur => Some (remove_header bcur) end *)

+                          pctl := pctl cs1; ep := (if pheader cs1 then ep cs1 else false); rem := rem cs1;
                           cur := cur cs1 |}.

 

-Lemma step_simu_header:

+(* Theorem (A) in the diagram, the easiest of all *)
+Theorem step_simu_header:
   forall bb s fb sp c ms m rs1 m1 cs1,

-(*   (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> *)

   pstate cs1 = (State rs1 m1) ->

   match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->

   (exists cs1',

@@ -1340,7 +1312,8 @@ Proof.
   simpl. econstructor; eauto.

 Qed.

 

-Lemma step_simu_body:

+(* Theorem (B) in the diagram, using step_simu_basic + induction on the Machblock body *)
+Theorem step_simu_body:
   forall bb s fb sp c ms m rs1 m1 ms' cs1 m',

   MB.header bb = nil ->

   (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->

@@ -1349,14 +1322,14 @@ Lemma step_simu_body:
   match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->

   (exists rs2 m2 cs2 ep,

        cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := nil; pbody2 := pbody2 cs1;

-                pctl := pctl cs1; fpok := ep; rem := rem cs1; cur := cur cs1 |}

+                pctl := pctl cs1; ep := ep; rem := rem cs1; cur := cur cs1 |}
     /\ exec_body tge (pbody1 cs1) rs1 m1 = Next rs2 m2

     /\ match_codestate fb (MB.State s fb sp ({| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |}::c) ms' m') cs2).

 Proof.

   intros bb. destruct bb as [hd bdy ex]; simpl; auto. induction bdy as [|bi bdy].

   - intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS.

     inv BSTEP.

-    exists rs1, m1, cs1, (fpok cs1).

+    exists rs1, m1, cs1, (ep cs1).
     inv MCS. inv Hpstate. simpl in *. monadInv TBC. repeat (split; simpl; auto).

     econstructor; eauto.

   - intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS. inv BSTEP.

@@ -1371,23 +1344,6 @@ Proof.
     rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto.

 Qed.

 

-(* Lemma exec_body_straight:

-  forall l rs0 m0 rs1 m1,

-  l <> nil ->

-  exec_body tge l rs0 m0 = Next rs1 m1 ->

-  exec_straight tge l rs0 m0 nil rs1 m1.

-Proof.

-  induction l as [|i1 l].

-    intros. contradict H; auto.

-  destruct l as [|i2 l].

-  - intros until m1. intros _ EXEB. simpl in EXEB.

-    destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.

-    inv EXEB. econstructor; eauto.

-  - intros until m1. intros _ EXEB. simpl in EXEB. simpl in IHl.

-    destruct (exec_basic_instr tge i1 rs0 m0) eqn:EBI; try discriminate.

-    econstructor; eauto. eapply IHl; eauto. discriminate.

-Qed. *)

-

 Lemma exec_body_pc:

   forall l rs1 m1 rs2 m2,

   exec_body tge l rs1 m1 = Next rs2 m2 ->

@@ -1432,7 +1388,8 @@ Proof.
   contradict H. unfold mbsize. simpl. auto.

 Qed.

 

-(* Alternative form of step_simulation_bblock, easier to prove *)

+(* Bringing theorems (A), (B) and (C) together, for the case of the absence of builtin instruction *)
+(* This more general form is easier to prove, but the actual theorem is step_simulation_bblock further below *)
 Lemma step_simulation_bblock':

   forall sf f sp bb bb' bb'' rs m rs' m' s'' c S1,

   bb' = mb_remove_header bb ->

@@ -1481,8 +1438,6 @@ Proof.
     intros (cs1' & EXEH & MCS2).

 

     (* step_simu_body part *)

-(*     assert (MB.body bb = MB.body (mb_remove_header bb)). { destruct bb; simpl; auto. }

-    rewrite H in BSTEP. clear H. *)

     assert (Hpstate': pstate cs1' = pstate cs1). { inv EXEH; auto. }

     exploit step_simu_body.

       3: eapply BSTEP.

@@ -1502,8 +1457,8 @@ Proof.
       9: eapply MCS'. all: simpl.

       10: eapply ESTEP.

       all: simpl; eauto.

-      rewrite Hpbody2. rewrite Hpctl. rewrite Hcur.

-      { inv MAS; simpl in *. inv Hcur. inv Hpstate2. eapply match_asmstate_some; eauto.

+      rewrite Hpbody2. rewrite Hpctl.
+      { inv MAS; simpl in *. inv Hpstate2. eapply match_asmstate_some; eauto.
         erewrite exec_body_pc; eauto. }

     intros (rs3 & m3 & rs4 & m4 & EXEB' & EXECTL' & MS').

 

@@ -1528,11 +1483,11 @@ Proof.
     assert (f1 = f0) by congruence. subst f0.

     rewrite PCeq in Hrs1pc. inv Hrs1pc.

     exploit functions_translated; eauto. intros (tf1 & FIND'' & TRANS''). rewrite FIND' in FIND''.

-    inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ. inv Hcur.

+    inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ.
     eapply find_bblock_tail; eauto.

 Qed.

 

-Lemma step_simulation_bblock:

+Theorem step_simulation_bblock:
   forall sf f sp bb ms m ms' m' S2 c,

   body_step ge sf f sp (Machblock.body bb) ms m ms' m' ->

   (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->

@@ -1548,12 +1503,7 @@ Proof.
   - econstructor.

 Qed.

 

-Definition measure (s: MB.state) : nat :=

-  match s with

-  | MB.State _ _ _ _ _ _ => 0%nat

-  | MB.Callstate _ _ _ _ => 0%nat

-  | MB.Returnstate _ _ _ => 1%nat

-  end.

+(** Dealing now with the builtin case *)
 

 Definition split (c: MB.code) :=

   match c with

@@ -1609,7 +1559,7 @@ Proof.
   eapply transl_code_at_pc_split_builtin; eauto.

 Qed.

 

-Lemma step_simulation_builtin:

+Theorem step_simulation_builtin:
   forall ef args res bb sf f sp c ms m t S2,

   MB.body bb = nil -> MB.exit bb = Some (MBbuiltin ef args res) ->

   exit_step return_address_offset ge (MB.exit bb) (Machblock.State sf f sp (bb :: c) ms m) t S2 ->

@@ -1656,6 +1606,16 @@ Proof.
   congruence.

 Qed.

 

+(* Measure to prove finite stuttering, see the other backends *)
+Definition measure (s: MB.state) : nat :=
+  match s with
+  | MB.State _ _ _ _ _ _ => 0%nat
+  | MB.Callstate _ _ _ _ => 0%nat
+  | MB.Returnstate _ _ _ => 1%nat
+  end.
+
+(* The actual MB.step/AB.step simulation, using the above theorems, plus extra proofs
+   for the internal and external function cases *)
 Theorem step_simulation:

   forall S1 t S2, MB.step return_address_offset ge S1 t S2 ->

   forall S1' (MS: match_states S1 S1'),

@@ -1710,25 +1670,20 @@ Proof.
   exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto.

   intros [m3' [P Q]].

   (* Execution of function prologue *)

-  monadInv EQ0. (* rewrite transl_code'_transl_code in EQ1. *)

+  monadInv EQ0.
   set (tfbody := make_prologue f x0) in *.

   set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *.

   set (rs2 := rs0#FP <- (parent_sp s) #SP <- sp #RTMP <- Vundef).

   exploit (Pget_correct tge GPRA RA nil rs2 m2'); auto.

   intros (rs' & U' & V').

-(*   exploit (exec_straight_through_singleinst); eauto.

-  intro W'. remember (nextblock _ rs') as rs''. *)

   exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs' m2').

-    rewrite chunk_of_Tptr in P.

+  { rewrite chunk_of_Tptr in P.
     assert (rs' GPRA = rs0 RA). { apply V'. }

     assert (rs' SP = rs2 SP). { apply V'; discriminate. }

     rewrite H4. rewrite H3.

-    (* change (rs' GPRA) with (rs0 RA). *)

     rewrite ATLR.

-    change (rs2 SP) with sp. eexact P.

+    change (rs2 SP) with sp. eexact P. }
   intros (rs3 & U & V).

-(*   exploit (exec_straight_through_singleinst); eauto.

-  intro W. *)

   assert (EXEC_PROLOGUE: exists rs3',

             exec_straight_blocks tge tf

               tf.(fn_blocks) rs0 m'

@@ -1774,7 +1729,6 @@ Local Transparent destroyed_at_function_entry.
   rewrite Heqrs3'. Simpl. rewrite V. inversion V'. rewrite H6. auto.

   assert (r <> GPRA). { contradict H3; rewrite H3; unfold data_preg; auto. }

   assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }

-  (* rewrite H8; auto. *)

   contradict H3; rewrite H3; unfold data_preg; auto.

   contradict H3; rewrite H3; unfold data_preg; auto.

   contradict H3; rewrite H3; unfold data_preg; auto.

@@ -1782,6 +1736,7 @@ Local Transparent destroyed_at_function_entry.
   intros. rewrite Heqrs3'. rewrite V by auto with asmgen.

   assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }

   rewrite H4 by auto with asmgen. reflexivity. discriminate.

+
 - (* external function *)

   inv MS.

   exploit functions_translated; eauto.

diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index a360aa7c..d3eb1dde 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -1204,7 +1204,8 @@ Qed.
 Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
 Proof.
   red; intros until x. unfold cast8unsigned.
-  rewrite Val.zero_ext_and. apply eval_andimm. compute. discriminate.
+
+  rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. discriminate.
 Qed.
 
 Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
@@ -1217,7 +1218,7 @@ Qed.
 Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
 Proof.
   red; intros until x. unfold cast8unsigned.
-  rewrite Val.zero_ext_and. apply eval_andimm. compute. discriminate.
+  rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. discriminate.
 Qed.
 
 Theorem eval_intoffloat:
diff --git a/mppa_k1c/abstractbb/Impure/ImpConfig.v b/mppa_k1c/abstractbb/Impure/ImpConfig.v
index 1bd93d4c..e49a4611 100644
--- a/mppa_k1c/abstractbb/Impure/ImpConfig.v
+++ b/mppa_k1c/abstractbb/Impure/ImpConfig.v
@@ -22,9 +22,9 @@ Module Type ImpureView.
 (* START COMMENT *)
  Module UnsafeImpure.
 
- Parameter unsafe_coerce: forall {A}, t A -> A.
+ Parameter unsafe_coerce: forall {A}, t A -> option A.
 
- Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=x -> mayRet k x. 
+ Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=Some x -> mayRet k x.
 
  Extraction Inline unsafe_coerce.
 
@@ -41,11 +41,11 @@ Module Impure: ImpureView.
 
   Module UnsafeImpure.
 
-  Definition unsafe_coerce {A} (x:t A) := x.
+  Definition unsafe_coerce {A} (x:t A) := Some x.
 
-  Lemma unsafe_coerce_not_really_correct: forall A (k: t A) x, (unsafe_coerce k)=x -> mayRet k x.
+  Lemma unsafe_coerce_not_really_correct: forall A (k: t A) x, (unsafe_coerce k)=Some x -> mayRet k x.
   Proof.
-    unfold unsafe_coerce, mayRet; auto.
+    unfold unsafe_coerce, mayRet; congruence.
   Qed.
 
   End UnsafeImpure.
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index ecaca7b3..0fa47fca 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -25,6 +25,8 @@ Require Import Op Locations Mach Asm.
 Local Open Scope string_scope.
 Local Open Scope error_monad_scope.
 
+Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
+
 (** The code generation functions take advantage of several
   characteristics of the [Mach] code generated by earlier passes of the
   compiler, mostly that argument and result registers are of the correct
diff --git a/test/c/Makefile b/test/c/Makefile
index 72814390..a2a80e06 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -8,7 +8,9 @@ EXECUTE:=timeout --signal=SIGTERM 20s $(EXECUTE)
 
 LIBS=$(LIBMATH)
 
-TIME=ocaml unix.cma ../../tools/xtime.ml -o /dev/null -mintime 2.0 -minruns 4
+TIME=time >/dev/null
+# FIXME - maybe this is better? From v3.6
+# TIME=ocaml unix.cma ../../tools/xtime.ml -o /dev/null -mintime 2.0 -minruns 4
 
 PROGS?=fib integr qsort fft fftsp fftw sha1 sha3 aes almabench \
   lists binarytrees fannkuch mandelbrot nbody \
diff --git a/test/c/Results/mandelbrot-mppa_k1c b/test/c/Results/mandelbrot-mppa_k1c
index 246f7ce1..f50961fe 100644
--- a/test/c/Results/mandelbrot-mppa_k1c
+++ b/test/c/Results/mandelbrot-mppa_k1c
diff --git a/test/c/aes.c b/test/c/aes.c
index 16f02e47..0a64fe60 100644
--- a/test/c/aes.c
+++ b/test/c/aes.c
@@ -1441,6 +1441,10 @@ int main(int argc, char ** argv)
           (u8 *)"\x00\x11\x22\x33\x44\x55\x66\x77\x88\x99\xAA\xBB\xCC\xDD\xEE\xFF",
           (u8 *)"\x8E\xA2\xB7\xCA\x51\x67\x45\xBF\xEA\xFC\x49\x90\x4B\x49\x60\x89",
           5, 6);
+#ifdef __K1C__
+  do_bench(2000);
+#else
   do_bench(1000000);
+#endif
   return 0;
 }
diff --git a/test/c/almabench.c b/test/c/almabench.c
index 5487b062..4417200c 100644
--- a/test/c/almabench.c
+++ b/test/c/almabench.c
@@ -42,10 +42,15 @@
 #define R2D (180.0 / PI)
 #define GAUSSK 0.01720209895
 #define TEST_LOOPS 20
-#define TEST_LENGTH 36525
 #define sineps 0.3977771559319137
 #define coseps 0.9174820620691818
 
+#ifdef __K1C__
+#define TEST_LENGTH 12
+#else
+#define TEST_LENGTH 36525
+#endif
+
 const double amas [8] = { 6023600.0, 408523.5, 328900.5, 3098710.0, 1047.355, 3498.5, 22869.0, 19314.0 };
 
 const double a [8][3] =
diff --git a/test/c/mandelbrot.c b/test/c/mandelbrot.c
index 133d55c5..fb8b929c 100644
--- a/test/c/mandelbrot.c
+++ b/test/c/mandelbrot.c
@@ -27,7 +27,7 @@ int main (int argc, char **argv)
 
     if (argc < 2) {
 #ifdef __K1C__
-      w = h = 50;
+      w = h = 40;
 #else
       w = h = 1000;
 #endif
diff --git a/test/c/sha1.c b/test/c/sha1.c
index 0a6ac8fe..624030cc 100644
--- a/test/c/sha1.c
+++ b/test/c/sha1.c
@@ -231,6 +231,10 @@ int main(int argc, char ** argv)
   }
   do_test(test_input_1, test_output_1);
   do_test(test_input_2, test_output_2);
+#ifdef __K1C__
+  do_bench(500);
+#else
   do_bench(200000);
+#endif
   return 0;
 }
diff --git a/test/c/sha3.c b/test/c/sha3.c
index a0905817..164e3086 100644
--- a/test/c/sha3.c
+++ b/test/c/sha3.c
@@ -190,8 +190,13 @@ test_triplet_t testvec[4] = {
   }
 };
 
+#ifdef __K1C__
+#define DATALEN 1000
+#define NITER 7
+#else
 #define DATALEN 100000
 #define NITER 25
+#endif
 
 int main()
 {
diff --git a/test/c/siphash24.c b/test/c/siphash24.c
index 4a42e013..ce0df78c 100644
--- a/test/c/siphash24.c
+++ b/test/c/siphash24.c
@@ -235,13 +235,19 @@ int test_vectors()
 
 u8 testdata[100] = { 1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 12, 34, 56, 78, 90 };
 
+#ifdef __K1C__
+#define NITER 1000
+#else
+#define NITER 1000000
+#endif
+
 int speed_test(void)
 {
   u8 out[8], k[16];
   int i;
 
   for(i = 0; i < 16; ++i ) k[i] = i;
-  for(i = 0; i < 1000000; i++) {
+  for(i = 0; i < NITER; i++) {
     testdata[99] = (u8) i;
     crypto_auth(out, testdata, 100, k);
   }
diff --git a/test/endian.h b/test/endian.h
index 8be2850c..d6e121f4 100644
--- a/test/endian.h
+++ b/test/endian.h
@@ -1,7 +1,7 @@
 #if defined(__ppc__) || defined(__PPC__) || defined(__ARMEB__)
 #define ARCH_BIG_ENDIAN
 #elif defined(__i386__) || defined(__x86_64__) || defined(__ARMEL__) \
-   || defined(__riscv) || defined(__aarch64__)
+   || defined(__riscv) || defined(__aarch64__) || defined(__K1C__)
 #undef ARCH_BIG_ENDIAN
 #else
 #error "unknown endianness"
diff --git a/test/monniaux/Makefile b/test/monniaux/Makefile
index a6b19891..d7437eea 100644
--- a/test/monniaux/Makefile
+++ b/test/monniaux/Makefile
@@ -20,9 +20,12 @@ oracle_times.txt: PostpassSchedulingOracle.patch
 	bash build_benches.sh $@
 
 measures.csv:
-	(cd ../../ && make -j20 && make install)
-	bash build_benches.sh
-	bash run_benches.sh $@
+	@echo "Building compcert.."
+	@(cd ../../ && make -s -j20 && make -s install)
+	@echo "Building benches..."
+	@bash build_benches.sh
+	@echo "Benches built. Running benches..."
+	@bash run_benches.sh $@
 
 #compile_times.pdf: gencompile.py verifier_times.txt oracle_times.txt
 #	python3.5 $^ $@
@@ -32,4 +35,5 @@ measures.csv:
 
 .PHONY:
 clean:
+	@bash clean_benches.sh
 	rm -f verifier_times.txt oracle_times.txt compile_times.pdf measure_times.k1c.pdf measures.csv
diff --git a/test/monniaux/README.md b/test/monniaux/README.md
index dbb3f337..14b062da 100644
--- a/test/monniaux/README.md
+++ b/test/monniaux/README.md
@@ -1,13 +1,18 @@
-# Benchmarking CompCert and GCC
+# Benchmarking `CompCert` and GCC
 
-rules.mk contains generic rules to compile with gcc and ccomp, with different
-optimizations, and producing different binaries. It also produces a
-measures.csv file containing the different timings given by the bench.
+## Compiling `CompCert`
 
-Up to 5 different optimizations can be used.
+The first step to benchmark `CompCert` is to compile it - the `INSTALL.md` instructions of the project root folder should guide you on installing it.
 
-To use this rule.mk, create a folder, put inside all the .c/.h source files,
-and write a Makefile ressembling:
+For the benchmarks to work, the compiler `ccomp` should be on your `$PATH`, with the runtime libraries installed correctly (with a successful `make install` on the project root directory).
+
+## Using the harness
+
+`rules.mk` contains generic rules to compile with `gcc` and `ccomp`, with different optimizations, and producing different binaries. It also produces a `measures.csv` file containing the different timings given by the bench.
+
+Up to 5 different sets of optimizations per compiler can be used.
+
+To use this `rules.mk`, create a folder, put inside all the .c/.h source files, and write a Makefile resembling:
 ```make
 TARGET=float_mat
 MEASURES="c1 c2 c3 c4 c5 c6 c7 c8"
@@ -15,57 +20,88 @@ MEASURES="c1 c2 c3 c4 c5 c6 c7 c8"
 include ../rules.mk
 ```
 
-This is all that is required to write, the rules.mk handles everything.
+This is all that is required to write, the `rules.mk` handles everything.
 
-There is the possibility to define some variables to finetune what you want.
-For instance, `ALL_CFILES` describes the .c source files whose objects are
-to be linked.
+There is the possibility to define some variables to fine tune what you want. For instance, `ALL_CFILES` describes the .c source files whose objects are to be linked.
 
 Here is an exhaustive list of the variables:
 - `TARGET`: name of the binary to produce
 - `MEASURES`: list of the different timings. This supposes that the program
-prints something of the form "c3 cycles: 44131" for instance. In the above
-example, the Makefile would generate such a line:
-```
-float_mat c3,  1504675,  751514,  553235, 1929369,  1372441 
-```
+prints something of the form `c3 cycles: 44131`.
 - `ALL_CFILES`: list of .c files to compile. By default, `$(wildcard *.c)`
-- `CLOCK`: basename of the clock file to compile. Default `../clock`
-- `ALL_CFLAGS`: cflags that are to be included for all compilers
+- `CLOCK`: `basename` of the clock file to compile. Default `../clock`
+- `ALL_CFLAGS`: `cflags` that are to be included for all compilers
 - `ALL_GCCFLAGS`: same, but GCC specific
-- `ALL_CCOMPFLAGS`: same, but ccomp specific
-- `K1C_CC`: GCC compiler (default k1-cos-gcc)
-- `K1C_CCOMP`: compcert compiler (default ccomp)
-- `EXECUTE_CYCLES`: running command (default `k1-cluster` with some options)
-- `GCCiFLAGS` with i from 0 to 4: the wanted optimizations. If one of these flags is empty, nothing is done. Same for `CCOMPiFLAGS`. For now, the default values:
-```
-# You can define up to GCC4FLAGS and CCOMP4FLAGS
-GCC0FLAGS?=
-GCC1FLAGS?=$(ALL_GCCFLAGS) -O1
-GCC2FLAGS?=$(ALL_GCCFLAGS) -O2
-GCC3FLAGS?=$(ALL_GCCFLAGS) -O3
-GCC4FLAGS?=
-CCOMP0FLAGS?=
-CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -fno-postpass
-CCOMP2FLAGS?=$(ALL_CCOMPFLAGS)
-CCOMP3FLAGS?=
-CCOMP4FLAGS?=
-
-# Prefix names
-GCC0PREFIX?=
-GCC1PREFIX?=.gcc.o1
-GCC2PREFIX?=.gcc.o2
-GCC3PREFIX?=.gcc.o3
-GCC4PREFIX?=
-CCOMP0PREFIX?=
-CCOMP1PREFIX?=.ccomp.o1
-CCOMP2PREFIX?=.ccomp.o2
-CCOMP3PREFIX?=
-CCOMP4PREFIX?= 
-```
+- `ALL_CCOMPFLAGS`: same, but `ccomp` specific
+- `K1C_CC`: GCC compiler (default `k1-cos-gcc`)
+- `K1C_CCOMP`: `CompCert` compiler (default `ccomp`)
+- `EXECUTE_CYCLES`: running command (default is `k1-cluster --syscall=libstd_scalls.so --cycle-based --`)
+- `EXECUTE_ARGS`: execution arguments. You can use a macro `__BASE__` which expands to the name of the binary being executed.
+- `GCCiFLAGS` with `i` from 0 to 4: the wanted optimizations. If one of these flags is empty, nothing is done. Same for `CCOMPiFLAGS`. Look at `rules.mk` to see the default values. You might find something like this:
+
+    # You can define up to GCC4FLAGS and CCOMP4FLAGS
+    GCC0FLAGS?=
+    GCC1FLAGS?=$(ALL_GCCFLAGS) -O1
+    GCC2FLAGS?=$(ALL_GCCFLAGS) -O2
+    GCC3FLAGS?=$(ALL_GCCFLAGS) -O3
+    GCC4FLAGS?=
+    CCOMP0FLAGS?=
+    CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -fno-postpass
+    CCOMP2FLAGS?=$(ALL_CCOMPFLAGS)
+    CCOMP3FLAGS?=
+    CCOMP4FLAGS?=
+
+    # Prefix names
+    GCC0PREFIX?=
+    GCC1PREFIX?=.gcc.o1
+    GCC2PREFIX?=.gcc.o2
+    GCC3PREFIX?=.gcc.o3
+    GCC4PREFIX?=
+    CCOMP0PREFIX?=
+    CCOMP1PREFIX?=.ccomp.o1
+    CCOMP2PREFIX?=.ccomp.o2
+    CCOMP3PREFIX?=
+    CCOMP4PREFIX?=
+
+The `PREFIX` are the prefixes to add to the secondary produced files (assembly, object, executable, ..). You should be careful that if a `FLAGS` is set, then the according `PREFIX` should be set as well.
+
+Assembly files are generated in `asm/`, objects in `obj/`, binaries in `bin/` and outputs in `out/`.
+
+To compile and execute all the benches : `make` while in the `monniaux` directory (without any `-j` flag). Doing so will compile CompCert, install it, and then proceed to execute each bench.
+
+To compile and/or execute a single bench, `cd` to the bench directory, then:
+- `make` for compiling the bench
+- `make run` for running it
+
+You can use `-j` flag when in a single bench directory.
+
+## Individual scripts
+
+If you want to run the building and running scripts individually without having to use the `Makefile` from `test/monniaux`, you can run the `build_benches.sh` script which builds each bench using all the available cores on your machine.
+
+Once the benches are built, you can then run `run_benches.sh file.csv` where `file.csv` is where you want to store the timings of the benchmarks. `run_benches.sh` also uses all the available cores of your machine.
+
+## Adding timings to a benchmark
+
+If you just add a benchmark without any timing function, the resulting `measures.csv` file will be empty for lack of timing output.
+
+To add a timing, you must use the functions whose prototypes are in `clock.h`
+
+    #include "../clock.h"
+    /* ... */
+    clock_prepare();
+    /* ... */
+    clock_start();
+    /* .. computations .. */
+    clock_stop();
+    /* ... */
+    print_total_clock(); // print to stdout
+    printerr_total_clock(); // print to stderr
+
+If the benchmark doesn't use `stdout` in a binary way you can use `print_total_clock()`. However, some benchmarks like `jpeg-6b` print their binary content to `stdout`, which then messes up the `grep` command when attempting to use it to extract the cycles from `stdout`.
 
-The `PREFIX` are the prefixes to add to the .s, .o, etc.. You should be careful that if a FLAGS is set, then the according PREFIX should be set as well.
+The solution is then to use `printerr_total_clock()` which will print the cycles to `stderr`, and use `EXECUTE_ARGS` ressembling this:
 
-Assembly files will be generated in `asm/`, objects in `obj/`, binaries in `bin/` and outputs in `out/`.
+    EXECUTE_ARGS=-dct int -outfile __BASE__.jpg testimg.ppm 2> __BASE__.out
 
-To compile and execute all the benches : `make`
+`__BASE__` is a macro that gets expanded to the base name - that is, the `TARGET` concatenated with one of the `GCCiPREFIX` or `CCOMPiPREFIX`. For instance, in `jpeg-6b`, `__BASE__` could be `jpeg-6b.ccomp.o2`.
diff --git a/test/monniaux/benches.sh b/test/monniaux/benches.sh
index 2365063a..434e1b15 100644
--- a/test/monniaux/benches.sh
+++ b/test/monniaux/benches.sh
@@ -1,3 +1,3 @@
-benches="binary_search bitsliced-aes bitsliced-tea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha-2 tacle-bench-lift tacle-bench-powerwindow too_slow heptagon_radio_transmitter lustrev4_lustrec_heater_control lustrev4_lv4_heater_control lustrev4_lv6-en-2cgc_heater_control lustrev6-convertible-en-2cgc xor_and_mat"
+benches="binary_search bitsliced-aes bitsliced-tea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha-2 tacle-bench-lift tacle-bench-powerwindow too_slow heptagon_radio_transmitter lustrev4_lustrec_heater_control lustrev4_lv4_heater_control lustrev4_lv6-en-2cgc_heater_control lustrev6-convertible-en-2cgc xor_and_mat glpk-4.65 picosat-965 genann jpeg-6b zlib-1.2.11 ocaml tiff-4.0.10 ncompress"
 
 # Removed for now : ternary
diff --git a/test/monniaux/build_benches.sh b/test/monniaux/build_benches.sh
index 931cebac..01abf55d 100755
--- a/test/monniaux/build_benches.sh
+++ b/test/monniaux/build_benches.sh
@@ -2,15 +2,21 @@
 
 TMPFILE=/tmp/1513times.txt
 
+cores=$(grep -c ^processor /proc/cpuinfo)
 source benches.sh
 
+default="\e[39m"
+magenta="\e[35m"
+red="\e[31m"
+
 rm -f commands.txt
 rm -f $TMPFILE
 for bench in $benches; do
+  echo -e "${magenta}Building $bench..${default}"
   if [ "$1" == "" ]; then 
-    (cd $bench && make -j20)
+    (cd $bench && make -s -j$cores > /dev/null &> /dev/null) || { echo -e "${red}Build failed" && break; }
   else
-    (cd $bench && make -j20) | grep -P "\d+: \d+\.\d+" >> $TMPFILE
+    (cd $bench && make -j$cores) | grep -P "\d+: \d+\.\d+" >> $TMPFILE
   fi
 done
 
diff --git a/test/monniaux/clean_benches.sh b/test/monniaux/clean_benches.sh
index c0a87ff9..dff15fd4 100755
--- a/test/monniaux/clean_benches.sh
+++ b/test/monniaux/clean_benches.sh
@@ -1,8 +1,12 @@
 
 source benches.sh
 
+blue="\e[34m"
+default="\e[39m"
+
 rm -f commands.txt
 for bench in $benches; do
-  (cd $bench && make clean)
+  echo -e "${blue}Cleaning $bench..${default}"
+  (cd $bench && make -s clean)
 done
 rm -f *.o
diff --git a/test/monniaux/genann/Makefile b/test/monniaux/genann/Makefile
new file mode 100644
index 00000000..2e76ec63
--- /dev/null
+++ b/test/monniaux/genann/Makefile
@@ -0,0 +1,4 @@
+ALL_CFILES= example4shorter.c genann.c
+TARGET=genann4
+
+include ../rules.mk
diff --git a/test/monniaux/genann/make.proto b/test/monniaux/genann/make.proto
deleted file mode 100644
index 7c4248bf..00000000
--- a/test/monniaux/genann/make.proto
+++ /dev/null
@@ -1,2 +0,0 @@
-sources: example4shorter.c genann.c
-target: genann4
\ No newline at end of file
diff --git a/test/monniaux/glpk-4.65/Makefile b/test/monniaux/glpk-4.65/Makefile
index a0ab40dc..eaa3f4b0 100644
--- a/test/monniaux/glpk-4.65/Makefile
+++ b/test/monniaux/glpk-4.65/Makefile
@@ -1,39 +1,6 @@
 ALL_CFLAGS += -I src/amd -I src/colamd -I src/mpl -I src/simplex -I src/api -I src/intopt -I src/minisat -I src/npp -I src/zlib -I src/bflib -I src/env -I src/misc -I src/draft -I src
-
-include ../rules.mk
-
-LIBS = -lm
-
-src=examples/glpsol.c $(wildcard src/*/*.c)
-
-PRODUCTS?=glpsol.gcc.host glpsol.ccomp.host glpsol.gcc.k1c glpsol.gcc.o1.k1c glpsol.ccomp.k1c
-PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS))
-
-all: $(PRODUCTS)
-
-.PHONY:
-run: measures.csv
-
-
-glpsol.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o 
-	$(CC) $(CFLAGS) $+ $(LIBS) -o $@
-glpsol.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o 
-	$(CCOMP) $(CCOMPFLAGS) $+ $(LIBS) -o $@
-glpsol.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CC) $(K1C_CFLAGS) $+  $(LIBS) -o $@
-glpsol.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+  $(LIBS) -o $@
-glpsol.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+  $(LIBS) -o $@
-
+ALL_CFILES=examples/glpsol.c $(wildcard src/*/*.c)
+TARGET=glpk
 EXECUTE_ARGS=--math examples/prod.mod
 
-measures.csv: $(PRODUCTS_OUT)
-	echo "benches, gcc host,ccomp host,gcc k1c,gcc o1 k1c,ccomp k1c" > $@
-
-.SECONDARY:
-
-.PHONY:
-clean:
-	rm -f *.o *.s *.k1c *.csv
-
+include ../rules.mk
diff --git a/test/monniaux/jpeg-6b/Makefile b/test/monniaux/jpeg-6b/Makefile
index 5a45b729..2bec9bb7 100644
--- a/test/monniaux/jpeg-6b/Makefile
+++ b/test/monniaux/jpeg-6b/Makefile
@@ -1,6 +1,6 @@
-all: cjpeg.gcc.k1c.out djpeg.gcc.k1c.out cjpeg.gcc.o1.k1c.out djpeg.gcc.o1.k1c.out cjpeg.ccomp.k1c.out djpeg.ccomp.k1c.out
+TARGET=jpeg-6b
 
-LIBSOURCES= jcapimin.c jcapistd.c jccoefct.c jccolor.c jcdctmgr.c jchuff.c \
+ALL_CFILES= jcapimin.c jcapistd.c jccoefct.c jccolor.c jcdctmgr.c jchuff.c \
         jcinit.c jcmainct.c jcmarker.c jcmaster.c jcomapi.c jcparam.c \
         jcphuff.c jcprepct.c jcsample.c jctrans.c jdapimin.c jdapistd.c \
         jdatadst.c jdatasrc.c jdcoefct.c jdcolor.c jddctmgr.c jdhuff.c \
@@ -8,36 +8,53 @@ LIBSOURCES= jcapimin.c jcapistd.c jccoefct.c jccolor.c jcdctmgr.c jchuff.c \
         jdpostct.c jdsample.c jdtrans.c jerror.c jfdctflt.c jfdctfst.c \
         jfdctint.c jidctflt.c jidctfst.c jidctint.c jidctred.c jquant1.c \
         jquant2.c jutils.c jmemmgr.c jmemansi.c
-CSOURCES=$(LIBSOURCES) rdppm.c rdgif.c rdtarga.c rdrle.c rdbmp.c rdswitch.c cdjpeg.c wrppm.c wrgif.c wrtarga.c wrrle.c wrbmp.c rdcolmap.c
+ALL_CFILES+=rdppm.c rdgif.c rdtarga.c rdrle.c rdbmp.c rdswitch.c cdjpeg.c wrppm.c wrgif.c wrtarga.c wrrle.c wrbmp.c rdcolmap.c
+ALL_CFILES+=cjpeg.c
 
-LIB_K1C_GCC_OFILES=$(CSOURCES:.c=.gcc.k1c.o)
-LIB_K1C_GCC_O1_OFILES=$(CSOURCES:.c=.gcc.o1.k1c.o)
-LIB_K1C_CCOMP_OFILES=$(CSOURCES:.c=.ccomp.k1c.o)
+EXECUTE_ARGS=-dct int -outfile __BASE__.jpg testimg.ppm 2> __BASE__.out
 
 include ../rules.mk
 
-cjpeg.gcc.k1c: $(LIB_K1C_GCC_OFILES) cjpeg.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o
-djpeg.gcc.k1c: $(LIB_K1C_GCC_OFILES) djpeg.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o
-
-cjpeg.gcc.o1.k1c: $(LIB_K1C_GCC_O1_OFILES) cjpeg.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o
-djpeg.gcc.o1.k1c: $(LIB_K1C_GCC_O1_OFILES) djpeg.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o
-
-cjpeg.ccomp.k1c: $(LIB_K1C_CCOMP_OFILES) cjpeg.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o
-djpeg.ccomp.k1c: $(LIB_K1C_CCOMP_OFILES) djpeg.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o
-
-
-djpeg.%.out: djpeg.%
-	$(EXECUTE_CYCLES) $< -dct int -ppm -outfile $@.ppm testorig.jpg 2> $@
-	cmp $@.ppm testimg.ppm 2>> $@
-
-cjpeg.%.out: cjpeg.%
-	$(EXECUTE_CYCLES) $< -dct int -outfile $@.jpg testimg.ppm 2> $@
-	cmp $@.jpg testimg.jpg 2>> $@
-
-.SECONDARY:
+#all: cjpeg.gcc.k1c.out djpeg.gcc.k1c.out cjpeg.gcc.o1.k1c.out djpeg.gcc.o1.k1c.out cjpeg.ccomp.k1c.out djpeg.ccomp.k1c.out
+#
+#LIBSOURCES= jcapimin.c jcapistd.c jccoefct.c jccolor.c jcdctmgr.c jchuff.c \
+#        jcinit.c jcmainct.c jcmarker.c jcmaster.c jcomapi.c jcparam.c \
+#        jcphuff.c jcprepct.c jcsample.c jctrans.c jdapimin.c jdapistd.c \
+#        jdatadst.c jdatasrc.c jdcoefct.c jdcolor.c jddctmgr.c jdhuff.c \
+#        jdinput.c jdmainct.c jdmarker.c jdmaster.c jdmerge.c jdphuff.c \
+#        jdpostct.c jdsample.c jdtrans.c jerror.c jfdctflt.c jfdctfst.c \
+#        jfdctint.c jidctflt.c jidctfst.c jidctint.c jidctred.c jquant1.c \
+#        jquant2.c jutils.c jmemmgr.c jmemansi.c
+#CSOURCES=$(LIBSOURCES) rdppm.c rdgif.c rdtarga.c rdrle.c rdbmp.c rdswitch.c cdjpeg.c wrppm.c wrgif.c wrtarga.c wrrle.c wrbmp.c rdcolmap.c
+#
+#LIB_K1C_GCC_OFILES=$(CSOURCES:.c=.gcc.k1c.o)
+#LIB_K1C_GCC_O1_OFILES=$(CSOURCES:.c=.gcc.o1.k1c.o)
+#LIB_K1C_CCOMP_OFILES=$(CSOURCES:.c=.ccomp.k1c.o)
+#
+#include ../rules.mk
+#
+#cjpeg.gcc.k1c: $(LIB_K1C_GCC_OFILES) cjpeg.gcc.k1c.o
+#	$(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o
+#djpeg.gcc.k1c: $(LIB_K1C_GCC_OFILES) djpeg.gcc.k1c.o
+#	$(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o
+#
+#cjpeg.gcc.o1.k1c: $(LIB_K1C_GCC_O1_OFILES) cjpeg.gcc.k1c.o
+#	$(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o
+#djpeg.gcc.o1.k1c: $(LIB_K1C_GCC_O1_OFILES) djpeg.gcc.k1c.o
+#	$(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o
+#
+#cjpeg.ccomp.k1c: $(LIB_K1C_CCOMP_OFILES) cjpeg.gcc.k1c.o
+#	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o
+#djpeg.ccomp.k1c: $(LIB_K1C_CCOMP_OFILES) djpeg.gcc.k1c.o
+#	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o
+#
+#
+#djpeg.%.out: djpeg.%
+#	$(EXECUTE_CYCLES) $< -dct int -ppm -outfile $@.ppm testorig.jpg 2> $@
+#	cmp $@.ppm testimg.ppm 2>> $@
+#
+#cjpeg.%.out: cjpeg.%
+#	$(EXECUTE_CYCLES) $< -dct int -outfile $@.jpg testimg.ppm 2> $@
+#	cmp $@.jpg testimg.jpg 2>> $@
+#
+#.SECONDARY:
diff --git a/test/monniaux/ncompress/Makefile b/test/monniaux/ncompress/Makefile
index cf543976..14a99d0b 100644
--- a/test/monniaux/ncompress/Makefile
+++ b/test/monniaux/ncompress/Makefile
@@ -1,52 +1,4 @@
-include ../rules.mk
-
-all: check
-
-
-all: compress.gcc.host compress.ccomp.host compress.gcc.k1c compress.ccomp.k1c
-
-compress.gcc.host : compress42.c ../clock.gcc.host.o
-	$(CC) $(CFLAGS) $+ -o $@
-
-compress.ccomp.host : compress42.c ../clock.gcc.host.o
-	$(CCOMP) $(CCOMPFLAGS) $+ -o $@
-
-compress.gcc.k1c : compress42.gcc.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-compress.ccomp.k1c : compress42.ccomp.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-INFILE=Makefile
-COMPRESSED=foo.gcc.host.Z
-
-foo.gcc.host.Z: compress.gcc.host $(INFILE)
-	./compress.gcc.host <$(INFILE) >foo.gcc.host.Z 2> foo.gcc.host.Z.out
+TARGET=compress
+EXECUTE_ARGS= < Makefile > __BASE__.Z 2> __BASE__.out
 
-foo.ccomp.k1c.Z: compress.ccomp.k1c $(INFILE)
-	$(EXECUTE) ./compress.ccomp.k1c <$(INFILE) >foo.ccomp.k1c.Z 2> foo.ccomp.k1c.Z.out
-
-foo.gcc.k1c.Z: compress.gcc.k1c $(INFILE)
-	$(EXECUTE) ./compress.gcc.k1c <$(INFILE) >foo.gcc.k1c.Z 2> foo.gcc.k1c.Z.out
-
-foo.gcc.host.txt: compress.gcc.host $(COMPRESSED)
-	./compress.gcc.host -d <$(COMPRESSED) >foo.gcc.host.txt 2> foo.gcc.host.txt.out
-
-foo.ccomp.k1c.txt: compress.gcc.host $(COMPRESSED)
-	$(EXECUTE) ./compress.ccomp.k1c -d <$(COMPRESSED) >foo.ccomp.k1c.txt 2> foo.ccomp.k1c.txt.out
-
-foo.gcc.k1c.txt: compress.gcc.host $(COMPRESSED)
-	$(EXECUTE) ./compress.gcc.k1c -d <$(COMPRESSED) >foo.gcc.k1c.txt 2> foo.gcc.k1c.txt.out
-
-check: foo.gcc.host.Z foo.gcc.host.txt foo.ccomp.k1c.Z foo.ccomp.k1c.txt foo.gcc.k1c.Z foo.gcc.k1c.txt
-	cmp foo.gcc.host.Z foo.ccomp.k1c.Z
-	cmp foo.gcc.host.Z foo.gcc.k1c.Z
-	cmp foo.gcc.host.txt foo.ccomp.k1c.txt
-	cmp foo.gcc.host.txt foo.gcc.k1c.txt
-
-clean:
-	rm -f *.Z *.txt *.out *.o *.s *.host *.k1c
-
-.PHONY: clean
-
-.SECONDARY: %.s
+include ../rules.mk
diff --git a/test/monniaux/ocaml/Makefile b/test/monniaux/ocaml/Makefile
index b63c8864..20f32b65 100644
--- a/test/monniaux/ocaml/Makefile
+++ b/test/monniaux/ocaml/Makefile
@@ -1,33 +1,6 @@
-ALL_CFLAGS=-Ibyterun
+TARGET=ocaml
+ALL_CFLAGS=-Ibyterun -lm
+ALL_CFILES=$(wildcard byterun/*.c)
 EXECUTE_ARGS=examples/quicksort
 
 include ../rules.mk
-
-ALL_CCOMPFLAGS=
-LDLIBS=-lm
-
-CFILES=$(wildcard byterun/*.c)
-
-CCOMP_K1C_S=$(patsubst %.c,%.ccomp.k1c.s,$(CFILES))
-CCOMP_HOST_S=$(patsubst %.c,%.ccomp.host.s,$(CFILES))
-
-GCC_K1C_S=$(patsubst %.c,%.gcc.k1c.s,$(CFILES))
-GCC_O1_K1C_S=$(patsubst %.c,%.gcc.o1.k1c.s,$(CFILES))
-GCC_HOST_S=$(patsubst %.c,%.gcc.host.s,$(CFILES))
-
-all: $(CCOMP_K1C_S) $(GCC_K1C_S) ocamlrun.ccomp.k1c.out ocamlrun.gcc.k1c.out ocamlrun.gcc.o1.k1c.out
-
-ocamlrun.ccomp.k1c : $(CCOMP_K1C_S) ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ $(LDLIBS)
-
-ocamlrun.ccomp.host : $(CCOMP_HOST_S) ../clock.gcc.host.o
-	$(CCOMP) $(CCOMPFLAGS) $+ -o $@ $(LDLIBS)
-
-ocamlrun.gcc.k1c : $(GCC_K1C_S) ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@ $(LDLIBS)
-
-ocamlrun.gcc.o1.k1c : $(GCC_O1_K1C_S) ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ $(LDLIBS)
-
-ocamlrun.gcc.host : $(GCC_HOST_S) ../clock.gcc.host.o
-	$(CC) $(CFLAGS) $+ -o $@ $(LDLIBS)
diff --git a/test/monniaux/pcre2-10.32/Makefile b/test/monniaux/pcre2-10.32/Makefile
index 98c2c8c2..b6b66c37 100644
--- a/test/monniaux/pcre2-10.32/Makefile
+++ b/test/monniaux/pcre2-10.32/Makefile
@@ -1,4 +1,7 @@
-CFILES = \
+TARGET=pcre2
+ALL_CFLAGS = -DHAVE_CONFIG_H -DPCRE2_CODE_UNIT_WIDTH=8 
+EXECUTE_ARGS=testdata/testinput6 > /dev/null 2> __BASE__.out
+ALL_CFILES = \
        pcre2_auto_possess.c \
        pcre2_chartables.c \
        pcre2_compile.c \
@@ -28,39 +31,5 @@ CFILES = \
        pcre2posix.c \
        pcre2test.c
 
-HFILES = config.h  pcre2_internal.h    pcre2posix.h \
-pcre2.h   pcre2_intmodedep.h  pcre2_ucp.h
-
-K1C_GCC_OFILES=$(CFILES:.c=.gcc.k1c.o)
-K1C_GCC_OFILES_O1=$(CFILES:.c=.gcc.o1.k1c.o)
-K1C_CCOMP_OFILES=$(CFILES:.c=.ccomp.k1c.o)
-K1C_GCC_SFILES=$(CFILES:.c=.gcc.k1c.s)
-K1C_CCOMP_SFILES=$(CFILES:.c=.ccomp.k1c.s)
-HOST_GCC_OFILES=$(CFILES:.c=.gcc.host.o)
-
-all:	pcre2test.gcc.o1.k1c.out pcre2test.gcc.k1c.out pcre2test.ccomp.k1c.out $(K1C_GCC_SFILES) $(K1C_CCOMP_SFILES)
-
-ALL_CFLAGS = -DHAVE_CONFIG_H -DPCRE2_CODE_UNIT_WIDTH=8 
-EXECUTE_ARGS = testdata/testinput6
-
 include ../rules.mk
 
-
-$(K1C_GCC_SFILES) $(K1C_GCC_OFILES_O1) $(K1C_CCOMP_SFILES) $(HOST_GCC_OFILES): $(HFILES)
-
-pcre2test.gcc.host: $(HOST_GCC_OFILES)
-	$(CC) $(CFLAGS) -o $@ $+ ../clock.gcc.host.o
-
-pcre2test.gcc.k1c: $(K1C_GCC_OFILES) ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) -o $@ $+
-
-pcre2test.gcc.o1.k1c: $(K1C_GCC_OFILES_O1) ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+
-
-pcre2test.ccomp.k1c: $(K1C_CCOMP_OFILES) ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+
-
-.PHONY: clean
-
-clean:
-	rm -f *.s *.o *.k1c
diff --git a/test/monniaux/pcre2-10.32/pcre2test.c b/test/monniaux/pcre2-10.32/pcre2test.c
index 25a7c4a1..a1fb64cb 100644
--- a/test/monniaux/pcre2-10.32/pcre2test.c
+++ b/test/monniaux/pcre2-10.32/pcre2test.c
@@ -8792,7 +8792,7 @@ FREECONTEXTS;
 #endif
 
   clock_stop();
-  print_total_clock();
+  printerr_total_clock();
   
 return yield;
 }
diff --git a/test/monniaux/picosat-965/Makefile b/test/monniaux/picosat-965/Makefile
index 991278ff..a887c0de 100644
--- a/test/monniaux/picosat-965/Makefile
+++ b/test/monniaux/picosat-965/Makefile
@@ -1,37 +1,11 @@
 EXECUTE_ARGS=sudoku.sat
-
-include ../rules.mk
-
-#ALL_CFLAGS = -DNDEBUG
 ALL_CFLAGS = -DNALARM -DNZIP -DNGETRUSAGE -DNDEBUG
-K1C_CFLAGS += $(EMBEDDED_CFLAGS)
-K1C_CCOMPFLAGS += $(EMBEDDED_CFLAGS)
-CCOMPFLAGS += -fbitfields
-K1C_CCOMPFLAGS += -fbitfields # -fno-if-conversion
-
-K1C_CFLAGS += $(ALL_CFLAGS)
-K1C_CCOMPFLAGS += $(ALL_CFLAGS)
-CCOMPFLAGS += $(ALL_CFLAGS)
-CFLAGS += $(ALL_CFLAGS)
-
-all: picosat.ccomp.k1c.s version.ccomp.k1c.s app.ccomp.k1c.s main.ccomp.k1c.s picosat.gcc.k1c.s version.gcc.k1c.s app.gcc.k1c.s main.gcc.k1c.s picosat.ccomp.k1c.out picosat.gcc.o1.k1c.out picosat.gcc.k1c.out picosat picosat.ccomp.host.out picosat.gcc.host.out
-
-picosat.ccomp.k1c : picosat.ccomp.k1c.s version.ccomp.k1c.s app.ccomp.k1c.s main.ccomp.k1c.s ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
+ALL_CCOMPFLAGS += -fbitfields # -fno-if-conversion
+TARGET=picosat
+ALL_CFILES=picosat.c version.c app.c main.c
 
-picosat.gcc.k1c : picosat.gcc.k1c.s version.gcc.k1c.s app.gcc.k1c.s main.gcc.k1c.s ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-picosat.gcc.o1.k1c : picosat.gcc.o1.k1c.s version.gcc.o1.k1c.s app.gcc.o1.k1c.s main.gcc.o1.k1c.s ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-picosat.ccomp.host : picosat.ccomp.host.s version.ccomp.host.s app.ccomp.host.s main.ccomp.host.s ../clock.gcc.host.o
-	$(CCOMP) $(CCOMPFLAGS) $+ -o $@
-
-picosat.gcc.host : picosat.gcc.host.s version.gcc.host.s app.gcc.host.s main.gcc.host.s ../clock.gcc.host.o
-	$(CC) $(FLAGS) $+ -o $@
-
-clean:
-	-rm -f *.s *.k1c *.out
+include ../rules.mk
 
-.PHONY: clean
+# FIXME - what were these for?
+#K1C_CFLAGS += $(EMBEDDED_CFLAGS)
+#K1C_CCOMPFLAGS += $(EMBEDDED_CFLAGS)
diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk
index 9d05b4d6..2de2c466 100644
--- a/test/monniaux/rules.mk
+++ b/test/monniaux/rules.mk
@@ -7,6 +7,9 @@ ALL_CFILES?=$(wildcard *.c)
 # Name of the target
 TARGET?=toto
 
+# Arguments of execution
+EXECUTE_ARGS?=
+
 # Name of the clock object
 CLOCK=../clock
 
@@ -25,30 +28,31 @@ K1C_CC?=k1-cos-gcc
 K1C_CCOMP?=ccomp
 
 # Command to execute
+#EXECUTE_CYCLES?=timeout --signal=SIGTERM 3m k1-cluster --syscall=libstd_scalls.so --cycle-based --
 EXECUTE_CYCLES?=k1-cluster --syscall=libstd_scalls.so --cycle-based --
 
 # You can define up to GCC4FLAGS and CCOMP4FLAGS
-GCC0FLAGS?=
-GCC1FLAGS?=$(ALL_GCCFLAGS) -O1 -g
+GCC0FLAGS?=$(ALL_GCCFLAGS) -O0
+GCC1FLAGS?=$(ALL_GCCFLAGS) -O1
 GCC2FLAGS?=$(ALL_GCCFLAGS) -O2
 GCC3FLAGS?=$(ALL_GCCFLAGS) -O3
 GCC4FLAGS?=
-CCOMP0FLAGS?=
-CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -O1 -g
-CCOMP2FLAGS?=$(ALL_CCOMPFLAGS)
-CCOMP3FLAGS?=
+CCOMP0FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fno-postpass
+CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fpostpass= greedy
+CCOMP2FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fno-if-conversion
+CCOMP3FLAGS?=$(ALL_CCOMPFLAGS) -O2
 CCOMP4FLAGS?=
 
 # Prefix names
-GCC0PREFIX?=
+GCC0PREFIX?=.gcc.o0
 GCC1PREFIX?=.gcc.o1
 GCC2PREFIX?=.gcc.o2
 GCC3PREFIX?=.gcc.o3
 GCC4PREFIX?=
-CCOMP0PREFIX?=
-CCOMP1PREFIX?=.ccomp.o1
-CCOMP2PREFIX?=.ccomp.o2
-CCOMP3PREFIX?=
+CCOMP0PREFIX?=.ccomp.nobundle
+CCOMP1PREFIX?=.ccomp.greedy
+CCOMP2PREFIX?=.ccomp.noif
+CCOMP3PREFIX?=.ccomp
 CCOMP4PREFIX?=
 
 # List of outfiles, updated by gen_rules
@@ -92,7 +96,8 @@ obj/%.o: asm/%.s
 
 out/%.out: bin/%.bin
 	@mkdir -p $(@D)
-	$(EXECUTE_CYCLES) $< | tee $@
+	@rm -f $@
+	$(EXECUTE_CYCLES) $< $(subst __BASE__,$(patsubst %.out,%,$@),$(EXECUTE_ARGS)) | tee -a $@
 
 ##
 # Generating the rules for all the compiler/flags..
@@ -132,7 +137,7 @@ endif
 
 measures.csv: $(OUTFILES)
 	@echo $(FIRSTLINE) > $@
-	@for i in $(MEASURES); do\
+	@for i in "$(MEASURES)"; do\
 		first=$$(grep "$$i cycles" $(firstword $(OUTFILES)));\
 		if test ! -z "$$first"; then\
 			if [ "$$i" != "time" ]; then\
@@ -153,5 +158,5 @@ run: measures.csv
 
 clean:
 	rm -f *.o *.s *.bin *.out
-	rm -f asm/*.s bin/*.bin obj/*.o out/*.out
+	rm -rf asm/ bin/ obj/ out/
 
diff --git a/test/monniaux/run_benches.sh b/test/monniaux/run_benches.sh
index 5f9f22cb..2b2e28d6 100755
--- a/test/monniaux/run_benches.sh
+++ b/test/monniaux/run_benches.sh
@@ -1,12 +1,16 @@
 
 source benches.sh
 
+cores=$(grep -c ^processor /proc/cpuinfo)
+processes=$((cores/4))
+
 rm -f commands.txt
 for bench in $benches; do
-  echo "(cd $bench && make -j5 run)" >> commands.txt
+  echo "(cd $bench && echo \"Running $bench..\" &&\
+    make -j4 run > /dev/null && echo \"$bench DONE\")" >> commands.txt
 done
 
-cat commands.txt | xargs -n1 -I{} -P4 bash -c '{}'
+cat commands.txt | xargs -n1 -I{} -P$processes bash -c '{}'
 
 ##
 # Gather all the CSV files
diff --git a/test/monniaux/tiff-4.0.10/Makefile b/test/monniaux/tiff-4.0.10/Makefile
index db3428fa..ac1aa276 100644
--- a/test/monniaux/tiff-4.0.10/Makefile
+++ b/test/monniaux/tiff-4.0.10/Makefile
@@ -1,52 +1,7 @@
+TARGET=ppm2tiff
+ALL_CFLAGS=-lm
 ALL_CCOMPFLAGS = -flongdouble
+EXECUTE_ARGS= -c g3 __BASE__.g3.tif < example_bw.pbm
 
 include ../rules.mk
 
-LIBS=-lm
-
-src=$(wildcard *.c)
-
-PRODUCTS?=ppm2tiff.gcc.host ppm2tiff.ccomp.host ppm2tiff.gcc.k1c ppm2tiff.gcc.o1.k1c ppm2tiff.ccomp.k1c
-PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS))
-
-all: $(PRODUCTS)
-
-.PHONY:
-run: measures.csv
-
-ppm2tiff.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o 
-	$(CC) $(CFLAGS) $+ $(LIBS) -o $@
-ppm2tiff.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o 
-	$(CCOMP) $(CCOMPFLAGS) $+ $(LIBS) -o $@
-ppm2tiff.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CC) $(K1C_CFLAGS) $+ $(LIBS) -o $@
-ppm2tiff.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ $(LIBS) -o $@
-ppm2tiff.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ $(LIBS) -o $@
-
-ppm2tiff.gcc.host.out: ppm2tiff.gcc.host
-	bunzip2 < example_bw.pbm.bz2 | ./$< -c g3 $<.g3.tif | tee $@
-
-ppm2tiff.ccomp.host.out: ppm2tiff.ccomp.host
-	bunzip2 < example_bw.pbm.bz2 | ./$< -c g3 $<.g3.tif | tee $@
-
-ppm2tiff.gcc.k1c.out: ppm2tiff.gcc.k1c
-	bunzip2 < example_bw.pbm.bz2 | $(EXECUTE_CYCLES) ./$< -c g3 $<.g3.tif | tee $@
-
-ppm2tiff.gcc.o1.k1c.out: ppm2tiff.gcc.o1.k1c
-	bunzip2 < example_bw.pbm.bz2 | $(EXECUTE_CYCLES) ./$< -c g3 $<.g3.tif | tee $@
-
-ppm2tiff.ccomp.k1c.out: ppm2tiff.ccomp.k1c
-	bunzip2 < example_bw.pbm.bz2 | $(EXECUTE_CYCLES) ./$< -c g3 $<.g3.tif | tee $@
-
-measures.csv: $(PRODUCTS_OUT)
-	echo "benches, gcc host,ccomp host,gcc k1c,gcc o1 k1c,ccomp k1c" > $@
-	echo "ppm2tiff ", $$(grep 'cycles' ppm2tiff.gcc.host.out | cut -d':' -f2), $$(grep 'cycles' ppm2tiff.ccomp.host.out | cut -d':' -f2), $$(grep 'cycles' ppm2tiff.gcc.k1c.out | cut -d':' -f2), $$(grep 'cycles' ppm2tiff.gcc.o1.k1c.out | cut -d':' -f2), $$(grep 'cycles' ppm2tiff.ccomp.k1c.out | cut -d':' -f2)>> $@
-
-.SECONDARY:
-
-.PHONY:
-clean:
-	rm -f *.o *.s *.k1c *.csv
-
diff --git a/test/monniaux/tiff-4.0.10/example_bw.pbm b/test/monniaux/tiff-4.0.10/example_bw.pbm
new file mode 100644
index 00000000..971a82bb
--- /dev/null
+++ b/test/monniaux/tiff-4.0.10/example_bw.pbm
diff --git a/test/monniaux/zlib-1.2.11/Makefile b/test/monniaux/zlib-1.2.11/Makefile
index 202f2ea4..9e6920f5 100644
--- a/test/monniaux/zlib-1.2.11/Makefile
+++ b/test/monniaux/zlib-1.2.11/Makefile
@@ -1,53 +1,62 @@
-ALL_CCOMPFLAGS = -faddx
-ALL_CFLAGS = -D_POSIX_C_SOURCE=2 -D_LARGEFILE64_SOURCE=1 -U__STRICT_ANSI__
+TARGET=zlib
 
-include ../rules.mk
-
-src=$(wildcard *.c)
-
-PRODUCTS?=minigzip.gcc.host minigzip.ccomp.host minigzip.gcc.k1c minigzip.gcc.o1.k1c minigzip.ccomp.k1c
-PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS))
-
-all: $(PRODUCTS)
-
-.PHONY:
-run: measures.csv
-
-
-minigzip.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o 
-	$(CC) $(CFLAGS) $+ -lm -o $@
-minigzip.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o 
-	$(CCOMP) $(CCOMPFLAGS) $+ -lm -o $@
-minigzip.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CC) $(K1C_CFLAGS) $+ -lm -o $@
-minigzip.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -lm -o $@
-minigzip.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -lm -o $@
-measures.csv: $(PRODUCTS_OUT)
-	echo "benches, gcc host,ccomp host,gcc k1c,gcc o1 k1c,ccomp k1c" > $@
-	echo "zlib ", $$(grep 'cycles' minigzip.gcc.host.out | cut -d':' -f2), $$(grep 'cycles' minigzip.ccomp.host.out | cut -d':' -f2), $$(grep 'cycles' minigzip.gcc.k1c.out | cut -d':' -f2), $$(grep 'cycles' minigzip.gcc.o1.k1c.out | cut -d':' -f2), $$(grep 'cycles' minigzip.ccomp.k1c.out | cut -d':' -f2)>> $@
+ALL_CCOMPFLAGS=-faddx
+ALL_CFLAGS=  -D_POSIX_C_SOURCE=2 -D_LARGEFILE64_SOURCE=1 -U__STRICT_ANSI__
+EXECUTE_ARGS=< zlib_small.txt > /dev/null 2> __BASE__.out
 
-SAMPLE_FILE=zlib.h
-
-minigzip.gcc.host.out minigzip.gcc.host.output: minigzip.gcc.host
-	./$< < $(SAMPLE_FILE) > $<.output 2> $@
-
-minigzip.ccomp.host.out minigzip.ccomp.host.output: minigzip.ccomp.host
-	./$< < $(SAMPLE_FILE) > $<.output 2> $@
-
-minigzip.gcc.k1c.out minigzip.gcc.k1c.output: minigzip.gcc.k1c
-	$(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@
-
-minigzip.gcc.o1.k1c.out minigzip.gcc.o1.k1c.output: minigzip.gcc.o1.k1c
-	$(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@
-
-minigzip.ccomp.k1c.out minigzip.ccomp.k1c.output: minigzip.ccomp.k1c
-	$(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@
-
-.SECONDARY:
+include ../rules.mk
 
-.PHONY:
-clean:
-	rm -f *.o *.s *.k1c *.csv
 
+#ALL_CCOMPFLAGS = -faddx
+#ALL_CFLAGS = -D_POSIX_C_SOURCE=2 -D_LARGEFILE64_SOURCE=1 -U__STRICT_ANSI__
+#
+#include ../rules.mk
+#
+#src=$(wildcard *.c)
+#
+#PRODUCTS?=minigzip.gcc.host minigzip.ccomp.host minigzip.gcc.k1c minigzip.gcc.o1.k1c minigzip.ccomp.k1c
+#PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS))
+#
+#all: $(PRODUCTS)
+#
+#.PHONY:
+#run: measures.csv
+#
+#
+#minigzip.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o 
+#	$(CC) $(CFLAGS) $+ -lm -o $@
+#minigzip.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o 
+#	$(CCOMP) $(CCOMPFLAGS) $+ -lm -o $@
+#minigzip.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o 
+#	$(K1C_CC) $(K1C_CFLAGS) $+ -lm -o $@
+#minigzip.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o 
+#	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -lm -o $@
+#minigzip.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o 
+#	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -lm -o $@
+#measures.csv: $(PRODUCTS_OUT)
+#	echo "benches, gcc host,ccomp host,gcc k1c,gcc o1 k1c,ccomp k1c" > $@
+#	echo "zlib ", $$(grep 'cycles' minigzip.gcc.host.out | cut -d':' -f2), $$(grep 'cycles' minigzip.ccomp.host.out | cut -d':' -f2), $$(grep 'cycles' minigzip.gcc.k1c.out | cut -d':' -f2), $$(grep 'cycles' minigzip.gcc.o1.k1c.out | cut -d':' -f2), $$(grep 'cycles' minigzip.ccomp.k1c.out | cut -d':' -f2)>> $@
+#
+#SAMPLE_FILE=zlib.h
+#
+#minigzip.gcc.host.out minigzip.gcc.host.output: minigzip.gcc.host
+#	./$< < $(SAMPLE_FILE) > $<.output 2> $@
+#
+#minigzip.ccomp.host.out minigzip.ccomp.host.output: minigzip.ccomp.host
+#	./$< < $(SAMPLE_FILE) > $<.output 2> $@
+#
+#minigzip.gcc.k1c.out minigzip.gcc.k1c.output: minigzip.gcc.k1c
+#	$(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@
+#
+#minigzip.gcc.o1.k1c.out minigzip.gcc.o1.k1c.output: minigzip.gcc.o1.k1c
+#	$(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@
+#
+#minigzip.ccomp.k1c.out minigzip.ccomp.k1c.output: minigzip.ccomp.k1c
+#	$(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@
+#
+#.SECONDARY:
+#
+#.PHONY:
+#clean:
+#	rm -f *.o *.s *.k1c *.csv
+#
diff --git a/test/monniaux/zlib-1.2.11/zlib_small.txt b/test/monniaux/zlib-1.2.11/zlib_small.txt
new file mode 100644
index 00000000..2c494200
--- /dev/null
+++ b/test/monniaux/zlib-1.2.11/zlib_small.txt
@@ -0,0 +1,539 @@
+
+
+
+#ifndef ZLIB_H
+#define ZLIB_H
+
+#include "zconf.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#define ZLIB_VERSION "1.2.11"
+#define ZLIB_VERNUM 0x12b0
+#define ZLIB_VER_MAJOR 1
+#define ZLIB_VER_MINOR 2
+#define ZLIB_VER_REVISION 11
+#define ZLIB_VER_SUBREVISION 0
+
+
+
+
+typedef voidpf (*alloc_func) OF((voidpf opaque, uInt items, uInt size));
+typedef void   (*free_func)  OF((voidpf opaque, voidpf address));
+
+struct internal_state;
+
+typedef struct z_stream_s {
+    z_const Bytef *next_in;     
+
+    uLong    total_in;  
+
+    uInt     avail_out; 
+
+
+    z_const char *msg;  
+
+
+    alloc_func zalloc;  
+
+    voidpf     opaque;  
+
+    uLong   adler;      
+
+} z_stream;
+
+typedef z_stream FAR *z_streamp;
+
+
+
+typedef struct gz_header_s {
+    int     text;       
+
+    int     xflags;     
+
+    Bytef   *extra;     
+
+    uInt    extra_max;  
+
+    uInt    name_max;   
+
+    uInt    comm_max;   
+
+    int     done;       
+
+} gz_header;
+
+typedef gz_header FAR *gz_headerp;
+
+
+
+
+                        
+
+
+#define Z_OK            0
+#define Z_STREAM_END    1
+#define Z_NEED_DICT     2
+#define Z_ERRNO        (-1)
+#define Z_STREAM_ERROR (-2)
+#define Z_DATA_ERROR   (-3)
+#define Z_MEM_ERROR    (-4)
+#define Z_BUF_ERROR    (-5)
+#define Z_VERSION_ERROR (-6)
+
+
+
+#define Z_NO_COMPRESSION         0
+#define Z_BEST_SPEED             1
+#define Z_BEST_COMPRESSION       9
+#define Z_DEFAULT_COMPRESSION  (-1)
+
+
+
+#define Z_BINARY   0
+#define Z_TEXT     1
+#define Z_ASCII    Z_TEXT   
+
+
+#define Z_DEFLATED   8
+
+
+
+#define zlib_version zlibVersion()
+
+
+
+ZEXTERN const char * ZEXPORT zlibVersion OF((void));
+
+
+
+
+
+
+
+ZEXTERN int ZEXPORT deflate OF((z_streamp strm, int flush));
+
+
+
+
+ZEXTERN int ZEXPORT deflateEnd OF((z_streamp strm));
+
+
+
+
+
+
+
+
+ZEXTERN int ZEXPORT inflate OF((z_streamp strm, int flush));
+
+
+
+
+ZEXTERN int ZEXPORT inflateEnd OF((z_streamp strm));
+
+
+
+
+                        
+
+
+
+
+
+ZEXTERN int ZEXPORT deflateSetDictionary OF((z_streamp strm,
+                                             const Bytef *dictionary,
+                                             uInt  dictLength));
+
+
+
+ZEXTERN int ZEXPORT deflateGetDictionary OF((z_streamp strm,
+                                             Bytef *dictionary,
+                                             uInt  *dictLength));
+
+
+
+ZEXTERN int ZEXPORT deflateCopy OF((z_streamp dest,
+                                    z_streamp source));
+
+
+
+ZEXTERN int ZEXPORT deflateReset OF((z_streamp strm));
+
+
+
+ZEXTERN int ZEXPORT deflateParams OF((z_streamp strm,
+                                      int level,
+                                      int strategy));
+
+
+
+ZEXTERN int ZEXPORT deflateTune OF((z_streamp strm,
+                                    int good_length,
+                                    int max_lazy,
+                                    int nice_length,
+                                    int max_chain));
+
+
+
+ZEXTERN uLong ZEXPORT deflateBound OF((z_streamp strm,
+                                       uLong sourceLen));
+
+
+
+ZEXTERN int ZEXPORT deflatePending OF((z_streamp strm,
+                                       unsigned *pending,
+                                       int *bits));
+
+
+
+ZEXTERN int ZEXPORT deflatePrime OF((z_streamp strm,
+                                     int bits,
+                                     int value));
+
+
+
+ZEXTERN int ZEXPORT deflateSetHeader OF((z_streamp strm,
+                                         gz_headerp head));
+
+
+
+
+
+
+ZEXTERN int ZEXPORT inflateSetDictionary OF((z_streamp strm,
+                                             const Bytef *dictionary,
+                                             uInt  dictLength));
+
+
+
+ZEXTERN int ZEXPORT inflateGetDictionary OF((z_streamp strm,
+                                             Bytef *dictionary,
+                                             uInt  *dictLength));
+
+
+
+ZEXTERN int ZEXPORT inflateSync OF((z_streamp strm));
+
+
+
+ZEXTERN int ZEXPORT inflateCopy OF((z_streamp dest,
+                                    z_streamp source));
+
+
+
+ZEXTERN int ZEXPORT inflateReset OF((z_streamp strm));
+
+
+
+ZEXTERN int ZEXPORT inflateReset2 OF((z_streamp strm,
+                                      int windowBits));
+
+
+
+ZEXTERN int ZEXPORT inflatePrime OF((z_streamp strm,
+                                     int bits,
+                                     int value));
+
+
+
+ZEXTERN long ZEXPORT inflateMark OF((z_streamp strm));
+
+
+
+ZEXTERN int ZEXPORT inflateGetHeader OF((z_streamp strm,
+                                         gz_headerp head));
+
+
+
+
+
+
+typedef unsigned (*in_func) OF((void FAR *,
+                                z_const unsigned char FAR * FAR *));
+typedef int (*out_func) OF((void FAR *, unsigned char FAR *, unsigned));
+
+ZEXTERN int ZEXPORT inflateBack OF((z_streamp strm,
+                                    in_func in, void FAR *in_desc,
+                                    out_func out, void FAR *out_desc));
+
+
+
+ZEXTERN int ZEXPORT inflateBackEnd OF((z_streamp strm));
+
+
+
+ZEXTERN uLong ZEXPORT zlibCompileFlags OF((void));
+
+
+
+#ifndef Z_SOLO
+
+                        
+
+
+ZEXTERN int ZEXPORT compress OF((Bytef *dest,   uLongf *destLen,
+                                 const Bytef *source, uLong sourceLen));
+
+
+
+ZEXTERN int ZEXPORT compress2 OF((Bytef *dest,   uLongf *destLen,
+                                  const Bytef *source, uLong sourceLen,
+                                  int level));
+
+
+
+ZEXTERN uLong ZEXPORT compressBound OF((uLong sourceLen));
+
+
+
+ZEXTERN int ZEXPORT uncompress OF((Bytef *dest,   uLongf *destLen,
+                                   const Bytef *source, uLong sourceLen));
+
+
+
+ZEXTERN int ZEXPORT uncompress2 OF((Bytef *dest,   uLongf *destLen,
+                                    const Bytef *source, uLong *sourceLen));
+
+
+
+                        
+
+
+typedef struct gzFile_s *gzFile;    
+
+
+ZEXTERN gzFile ZEXPORT gzdopen OF((int fd, const char *mode));
+
+
+
+ZEXTERN int ZEXPORT gzbuffer OF((gzFile file, unsigned size));
+
+
+
+ZEXTERN int ZEXPORT gzsetparams OF((gzFile file, int level, int strategy));
+
+
+
+ZEXTERN int ZEXPORT gzread OF((gzFile file, voidp buf, unsigned len));
+
+
+
+ZEXTERN z_size_t ZEXPORT gzfread OF((voidp buf, z_size_t size, z_size_t nitems,
+                                     gzFile file));
+
+
+
+ZEXTERN int ZEXPORT gzwrite OF((gzFile file,
+                                voidpc buf, unsigned len));
+
+
+
+ZEXTERN z_size_t ZEXPORT gzfwrite OF((voidpc buf, z_size_t size,
+                                      z_size_t nitems, gzFile file));
+
+
+
+ZEXTERN int ZEXPORTVA gzprintf Z_ARG((gzFile file, const char *format, ...));
+
+
+
+ZEXTERN int ZEXPORT gzputs OF((gzFile file, const char *s));
+
+
+
+ZEXTERN char * ZEXPORT gzgets OF((gzFile file, char *buf, int len));
+
+
+
+ZEXTERN int ZEXPORT gzputc OF((gzFile file, int c));
+
+
+
+ZEXTERN int ZEXPORT gzgetc OF((gzFile file));
+
+
+
+ZEXTERN int ZEXPORT gzungetc OF((int c, gzFile file));
+
+
+
+ZEXTERN int ZEXPORT gzflush OF((gzFile file, int flush));
+
+
+
+
+
+
+ZEXTERN int ZEXPORT    gzrewind OF((gzFile file));
+
+
+
+
+
+
+
+
+
+ZEXTERN int ZEXPORT gzeof OF((gzFile file));
+
+
+
+ZEXTERN int ZEXPORT gzdirect OF((gzFile file));
+
+
+
+ZEXTERN int ZEXPORT    gzclose OF((gzFile file));
+
+
+
+ZEXTERN int ZEXPORT gzclose_r OF((gzFile file));
+ZEXTERN int ZEXPORT gzclose_w OF((gzFile file));
+
+
+
+ZEXTERN const char * ZEXPORT gzerror OF((gzFile file, int *errnum));
+
+
+
+ZEXTERN void ZEXPORT gzclearerr OF((gzFile file));
+
+
+
+#endif 
+
+
+
+
+
+ZEXTERN uLong ZEXPORT adler32 OF((uLong adler, const Bytef *buf, uInt len));
+
+
+
+ZEXTERN uLong ZEXPORT adler32_z OF((uLong adler, const Bytef *buf,
+                                    z_size_t len));
+
+
+
+
+
+
+ZEXTERN uLong ZEXPORT crc32   OF((uLong crc, const Bytef *buf, uInt len));
+
+
+
+ZEXTERN uLong ZEXPORT crc32_z OF((uLong adler, const Bytef *buf,
+                                  z_size_t len));
+
+
+
+
+
+
+
+                        
+
+ZEXTERN int ZEXPORT deflateInit_ OF((z_streamp strm, int level,
+                                     const char *version, int stream_size));
+ZEXTERN int ZEXPORT inflateInit_ OF((z_streamp strm,
+                                     const char *version, int stream_size));
+ZEXTERN int ZEXPORT deflateInit2_ OF((z_streamp strm, int  level, int  method,
+                                      int windowBits, int memLevel,
+                                      int strategy, const char *version,
+                                      int stream_size));
+ZEXTERN int ZEXPORT inflateInit2_ OF((z_streamp strm, int  windowBits,
+                                      const char *version, int stream_size));
+ZEXTERN int ZEXPORT inflateBackInit_ OF((z_streamp strm, int windowBits,
+                                         unsigned char FAR *window,
+                                         const char *version,
+                                         int stream_size));
+#ifdef Z_PREFIX_SET
+#  define z_deflateInit(strm, level) \
+          deflateInit_((strm), (level), ZLIB_VERSION, (int)sizeof(z_stream))
+#  define z_inflateInit(strm) \
+          inflateInit_((strm), ZLIB_VERSION, (int)sizeof(z_stream))
+#  define z_deflateInit2(strm, level, method, windowBits, memLevel, strategy) \
+          deflateInit2_((strm),(level),(method),(windowBits),(memLevel),\
+                        (strategy), ZLIB_VERSION, (int)sizeof(z_stream))
+#  define z_inflateInit2(strm, windowBits) \
+          inflateInit2_((strm), (windowBits), ZLIB_VERSION, \
+                        (int)sizeof(z_stream))
+#  define z_inflateBackInit(strm, windowBits, window) \
+          inflateBackInit_((strm), (windowBits), (window), \
+                           ZLIB_VERSION, (int)sizeof(z_stream))
+#else
+#  define deflateInit(strm, level) \
+          deflateInit_((strm), (level), ZLIB_VERSION, (int)sizeof(z_stream))
+#  define inflateInit(strm) \
+          inflateInit_((strm), ZLIB_VERSION, (int)sizeof(z_stream))
+#  define deflateInit2(strm, level, method, windowBits, memLevel, strategy) \
+          deflateInit2_((strm),(level),(method),(windowBits),(memLevel),\
+                        (strategy), ZLIB_VERSION, (int)sizeof(z_stream))
+#  define inflateInit2(strm, windowBits) \
+          inflateInit2_((strm), (windowBits), ZLIB_VERSION, \
+                        (int)sizeof(z_stream))
+#  define inflateBackInit(strm, windowBits, window) \
+          inflateBackInit_((strm), (windowBits), (window), \
+                           ZLIB_VERSION, (int)sizeof(z_stream))
+#endif
+
+#ifndef Z_SOLO
+
+
+
+struct gzFile_s {
+    unsigned have;
+    unsigned char *next;
+    z_off64_t pos;
+};
+ZEXTERN int ZEXPORT gzgetc_ OF((gzFile file));  
+
+#ifdef Z_LARGE64
+   ZEXTERN gzFile ZEXPORT gzopen64 OF((const char *, const char *));
+   ZEXTERN z_off64_t ZEXPORT gzseek64 OF((gzFile, z_off64_t, int));
+   ZEXTERN z_off64_t ZEXPORT gztell64 OF((gzFile));
+   ZEXTERN z_off64_t ZEXPORT gzoffset64 OF((gzFile));
+   ZEXTERN uLong ZEXPORT adler32_combine64 OF((uLong, uLong, z_off64_t));
+   ZEXTERN uLong ZEXPORT crc32_combine64 OF((uLong, uLong, z_off64_t));
+#endif
+
+#if !defined(ZLIB_INTERNAL) && defined(Z_WANT64)
+#  ifdef Z_PREFIX_SET
+#    define z_gzopen z_gzopen64
+#    define z_gzseek z_gzseek64
+#    define z_gztell z_gztell64
+#    define z_gzoffset z_gzoffset64
+#    define z_adler32_combine z_adler32_combine64
+#    define z_crc32_combine z_crc32_combine64
+#  else
+#    define gzopen gzopen64
+#    define gzseek gzseek64
+#    define gztell gztell64
+#    define gzoffset gzoffset64
+#    define adler32_combine adler32_combine64
+#    define crc32_combine crc32_combine64
+#  endif
+#  ifndef Z_LARGE64
+     ZEXTERN gzFile ZEXPORT gzopen64 OF((const char *, const char *));
+     ZEXTERN z_off_t ZEXPORT gzseek64 OF((gzFile, z_off_t, int));
+     ZEXTERN z_off_t ZEXPORT gztell64 OF((gzFile));
+     ZEXTERN z_off_t ZEXPORT gzoffset64 OF((gzFile));
+     ZEXTERN uLong ZEXPORT adler32_combine64 OF((uLong, uLong, z_off_t));
+     ZEXTERN uLong ZEXPORT crc32_combine64 OF((uLong, uLong, z_off_t));
+#  endif
+#else
+   ZEXTERN gzFile ZEXPORT gzopen OF((const char *, const char *));
+   ZEXTERN z_off_t ZEXPORT gzseek OF((gzFile, z_off_t, int));
+   ZEXTERN z_off_t ZEXPORT gztell OF((gzFile));
+   ZEXTERN z_off_t ZEXPORT gzoffset OF((gzFile));
+   ZEXTERN uLong ZEXPORT adler32_combine OF((uLong, uLong, z_off_t));
+   ZEXTERN uLong ZEXPORT crc32_combine OF((uLong, uLong, z_off_t));
+#endif
+
+#else 
+
+
+
+
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 585ffb1c..3447d6a5 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -10,7 +10,7 @@ LIBS=$(LIBMATH)
 # Can run, both in compiled mode and in interpreter mode,
 # and have reference output in Results
 
-TESTS=int32 int64 floats floats-basics floats-lit \
+TESTS?=int32 int64 floats floats-basics floats-lit \
   expr1 expr6 funptr2 initializers initializers2 initializers3 \
   volatile1 volatile2 volatile3 volatile4 \
   funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \
diff --git a/test/regression/extasm.c b/test/regression/extasm.c
index 8abeb98f..352b930b 100644
--- a/test/regression/extasm.c
+++ b/test/regression/extasm.c
@@ -24,7 +24,7 @@ int clobbers(int x, int z)
  || (defined(ARCH_riscV) && defined(MODEL_64)) \
  || (defined(ARCH_powerpc) && defined(MODEL_ppc64)) \
  || (defined(ARCH_powerpc) && defined(MODEL_e5500)) \
- || (defined(ARCH_mppa_k1c) && defined(MODEL_64))
+ || (defined(ARCH_mppa_k1c) && defined(MODEL_64)) \
  || defined(ARCH_aarch64)
 #define SIXTYFOUR
 #else