Merge remote-tracking branch 'origin/mppa-licm' into mppa-features

35 files changed, 2951 insertions, 105 deletions

diff --git a/Makefile b/Makefile
index ee8a11bc..a69f7e2e 100644
--- a/Makefile
+++ b/Makefile
@@ -88,15 +88,17 @@ BACKEND=\
   Kildall.v Liveness.v \
   ValueDomain.v ValueAOp.v ValueAnalysis.v \
   ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
+  Inject.v Injectproof.v \
   CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \
   CSE2deps.v CSE2depsproof.v \
   CSE2.v CSE2proof.v \
   CSE3analysis.v CSE3analysisproof.v CSE3.v CSE3proof.v \
+  LICM.v LICMproof.v \
   NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \
   Unusedglob.v Unusedglobproof.v \
   Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \
   ForwardMoves.v ForwardMovesproof.v \
-  FirstNop.v \
+  FirstNop.v FirstNopproof.v \
   Allnontrap.v Allnontrapproof.v \
   Allocation.v Allocproof.v \
   Tunneling.v Tunnelingproof.v \
diff --git a/aarch64/Archi.v b/aarch64/Archi.v
index aef4ab77..7d7b6887 100644
--- a/aarch64/Archi.v
+++ b/aarch64/Archi.v
@@ -86,3 +86,5 @@ Global Opaque ptr64 big_endian splitlong
 (** Whether to generate position-independent code or not *)
 
 Parameter pic_code: unit -> bool.
+
+Definition has_notrap_loads := false.
diff --git a/aarch64/Op.v b/aarch64/Op.v
index c0b9d435..afc25aa6 100644
--- a/aarch64/Op.v
+++ b/aarch64/Op.v
@@ -938,14 +938,19 @@ Definition is_trapping_op (op : operation) :=
   end.
                 
 
+Definition args_of_operation op :=
+  if eq_operation op Omove
+  then 1%nat
+  else List.length (fst (type_of_operation op)).
+
 Lemma is_trapping_op_sound:
   forall op vl sp m,
-    op <> Omove ->
     is_trapping_op op = false ->
-    (List.length vl) = (List.length (fst (type_of_operation op))) ->
+    (List.length vl) = args_of_operation op ->
     eval_operation genv sp op vl m <> None.
 Proof.
-  destruct op; intros; simpl in *; try congruence.
+  unfold args_of_operation.
+  destruct op; destruct eq_operation; intros; simpl in *; try congruence.
   all: try (destruct vl as [ | vh1 vl1]; try discriminate).
   all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
   all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
diff --git a/arm/Archi.v b/arm/Archi.v
index 16d6c71d..738341cc 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -97,3 +97,5 @@ Parameter abi: abi_kind.
 (** Whether instructions added with Thumb2 are supported. True for ARMv6T2
   and above. *)
 Parameter thumb2_support: bool.
+
+Definition has_notrap_loads := false.
diff --git a/arm/Op.v b/arm/Op.v
index 671bdbe4..25e48ce1 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -531,14 +531,19 @@ Definition is_trapping_op (op : operation) :=
   end.
                 
 
+Definition args_of_operation op :=
+  if eq_operation op Omove
+  then 1%nat
+  else List.length (fst (type_of_operation op)).
+
 Lemma is_trapping_op_sound:
   forall op vl sp m,
-    op <> Omove ->
     is_trapping_op op = false ->
-    (List.length vl) = (List.length (fst (type_of_operation op))) ->
+    (List.length vl) = args_of_operation op ->
     eval_operation genv sp op vl m <> None.
 Proof.
-  destruct op; intros; simpl in *; try congruence.
+  unfold args_of_operation.
+  destruct op; destruct eq_operation; intros; simpl in *; try congruence.
   all: try (destruct vl as [ | vh1 vl1]; try discriminate).
   all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
   all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
diff --git a/backend/CSE2.v b/backend/CSE2.v
index dc206c75..8e2307b0 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -262,33 +262,29 @@ Definition load (chunk: memory_chunk) (addr : addressing)
   | None => load1 chunk addr dst args rel
   end.
 
-(* NO LONGER NEEDED
-Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop :=
-  match l with
-  | nil => True
-  | (r,sv)::tail => (tr ! r) = Some sv /\ list_represents tail tr
+Definition kill_builtin_res res rel :=
+  match res with
+  | BR r => kill_reg r rel
+  | _ => rel
   end.
 
-Lemma elements_represent :
-  forall { X : Type },
-  forall tr : (PTree.t X),
-    (list_represents (PTree.elements tr) tr).
-Proof.
-  intros.
-  generalize (PTree.elements_complete tr).
-  generalize (PTree.elements tr).
-  induction l; simpl; trivial.
-  intro COMPLETE.
-  destruct a as [ r sv ].
-  split.
-  {
-    apply COMPLETE.
-    left; reflexivity.
-  }
-  apply IHl; auto.
-Qed.
-*)
-    
+Definition apply_external_call ef (rel : RELATION.t) : RELATION.t :=
+  match ef with
+  | EF_builtin name sg
+  | EF_runtime name sg =>
+    match Builtins.lookup_builtin_function name sg with
+    | Some bf => rel
+    | None => kill_mem rel
+    end
+  | EF_malloc (* FIXME *)
+  | EF_external _ _
+  | EF_vstore _ 
+  | EF_free (* FIXME *)
+  | EF_memcpy _ _ (* FIXME *)
+  | EF_inline_asm _ _ _ => kill_mem rel
+  | _ => rel
+  end.
+                              
 Definition apply_instr instr (rel : RELATION.t) : RB.t :=
   match instr with
   | Inop _
@@ -298,7 +294,7 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t :=
   | Iop op args dst _ => Some (gen_oper op dst args rel)
   | Iload trap chunk addr args dst _ => Some (load chunk addr dst args rel)
   | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
-  | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *)
+  | Ibuiltin ef _ res _ => Some (kill_builtin_res res (apply_external_call ef rel))
   | Itailcall _ _ _ | Ireturn _ => RB.bot
   end.
 
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 309ccce1..9e0ad909 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -1033,7 +1033,16 @@ Proof.
     assumption.
   }
   intuition congruence.
-Qed. 
+Qed.
+
+Lemma kill_builtin_res_sound:
+  forall res (m : mem) (rs : regset) vres (rel : RELATION.t)
+         (REL : sem_rel m rel rs),
+         (sem_rel m (kill_builtin_res res rel) (regmap_setres res vres rs)).
+Proof.
+  destruct res; simpl; intros; trivial.
+  apply kill_reg_sound; trivial.
+Qed.
 End SOUNDNESS.
 
 Definition match_prog (p tp: RTL.program) :=
@@ -1116,6 +1125,22 @@ Definition is_killed_in_fmap fmap pc res :=
   | Some map => is_killed_in_map map pc res
   end.
 
+Lemma external_call_sound:
+  forall ef (rel : RELATION.t) sp (m m' : mem) (rs : regset) vargs t vres
+         (REL : sem_rel fundef unit ge sp m rel rs)
+         (CALL : external_call ef ge vargs m t vres m'),
+    sem_rel fundef unit ge sp m' (apply_external_call ef rel) rs.
+Proof.
+  destruct ef; intros; simpl in *.
+  all: eauto using kill_mem_sound.
+  all: unfold builtin_or_external_sem in *.
+  1, 2: destruct (Builtins.lookup_builtin_function name sg);
+    eauto using kill_mem_sound;
+    inv CALL; eauto using kill_mem_sound.
+  all: inv CALL.
+  all: eauto using kill_mem_sound.
+Qed.
+  
 Definition sem_rel_b' := sem_rel_b fundef unit ge.
 Definition fmap_sem' := fmap_sem fundef unit ge.
 Definition subst_arg_ok' := subst_arg_ok fundef unit ge.
@@ -1578,9 +1603,9 @@ Proof.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
   
-  apply sem_rel_b_ge with (rb2 := Some RELATION.top).
+  apply sem_rel_b_ge with (rb2 := Some (kill_builtin_res res (apply_external_call ef mpc))).
   {
-    replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)).
+    replace (Some (kill_builtin_res res (apply_external_call ef mpc))) with (apply_instr' (fn_code f) pc (map # pc)).
     {
       eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
       2: apply apply_instr'_bot.
@@ -1591,8 +1616,8 @@ Proof.
     rewrite MPC.
     reflexivity.
   }
-  apply top_ok.
-  
+  apply kill_builtin_res_sound.
+  eapply external_call_sound with (m := m); eassumption.
 
 (* cond *)
 - econstructor; split.
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 90ce4ce7..bc5d3244 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -325,6 +325,29 @@ Section OPERATIONS.
              (rel : RELATION.t) : RELATION.t :=
     store1 chunk addr (forward_move_l rel args) src ty rel.
 
+  Definition kill_builtin_res res rel :=
+    match res with
+    | BR r => kill_reg r rel
+    | _ => rel
+    end.
+
+  Definition apply_external_call ef (rel : RELATION.t) : RELATION.t :=
+    match ef with
+    | EF_builtin name sg
+    | EF_runtime name sg =>
+      match Builtins.lookup_builtin_function name sg with
+      | Some bf => rel
+      | None => kill_mem rel
+      end
+    | EF_malloc (* FIXME *)
+    | EF_external _ _
+    | EF_vstore _ 
+    | EF_free (* FIXME *)
+    | EF_memcpy _ _ (* FIXME *)
+    | EF_inline_asm _ _ _ => kill_mem rel
+    | _ => rel
+    end.
+
   Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t :=
   match instr with
   | Inop _
@@ -335,7 +358,7 @@ Section OPERATIONS.
   | Iop op args dst _ => Some (oper dst (SOp op) args rel)
   | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel)
   | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
-  | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *)
+  | Ibuiltin ef _ res _ => Some (kill_builtin_res res (apply_external_call ef rel))
   | Itailcall _ _ _ | Ireturn _ => RB.bot
   end.
   End PER_NODE.
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index b87ec92c..f4ec7a10 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -869,6 +869,36 @@ Section SOUNDNESS.
 
   Hint Resolve store_sound : cse3.
 
+  Lemma kill_builtin_res_sound:
+    forall res (m : mem) (rs : regset) vres (rel : RELATION.t)
+           (REL : sem_rel rel rs m),
+      (sem_rel (kill_builtin_res (ctx:=ctx) res rel)
+               (regmap_setres res vres rs) m).
+  Proof.
+    destruct res; simpl; intros; trivial.
+    apply kill_reg_sound; trivial.
+  Qed.
+
+  Hint Resolve kill_builtin_res_sound : cse3.
+
+  Lemma external_call_sound:
+    forall ge ef (rel : RELATION.t) (m m' : mem) (rs : regset) vargs t vres
+           (REL : sem_rel rel rs m)
+           (CALL : external_call ef ge vargs m t vres m'),
+      sem_rel (apply_external_call (ctx:=ctx) ef rel) rs m'.
+  Proof.
+    destruct ef; intros; simpl in *.
+    all: eauto using kill_mem_sound.
+    all: unfold builtin_or_external_sem in *.
+    1, 2: destruct (Builtins.lookup_builtin_function name sg);
+      eauto using kill_mem_sound;
+      inv CALL; eauto using kill_mem_sound.
+    all: inv CALL.
+    all: eauto using kill_mem_sound.
+  Qed.
+
+  Hint Resolve external_call_sound : cse3.
+
   Section INDUCTIVENESS.
     Variable fn : RTL.function.
     Variable tenv : typing_env.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 19fb20be..53872e62 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -224,7 +224,6 @@ Proof.
   eapply function_ptr_translated; eauto.
 Qed.
 
-Check sem_rel_b.
 Inductive match_stackframes: list stackframe -> list stackframe -> signature -> Prop :=
   | match_stackframes_nil: forall sg,
       sg.(sig_res) = Tint ->
@@ -428,8 +427,8 @@ Ltac IND_STEP :=
         destruct ((fst (preanalysis tenv fn)) # mpc) as [zinv | ];
         simpl in *;
         intuition;
-        eapply rel_ge; eauto with cse3;
-        idtac mpc mpc' fn minstr
+        eapply rel_ge; eauto with cse3 (* ; for printing
+        idtac mpc mpc' fn minstr *)
       end.
 
 Lemma if_same : forall {T : Type} (b : bool) (x : T),
@@ -753,6 +752,9 @@ Proof.
     + econstructor; eauto.
       * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt.
       * IND_STEP.
+        apply kill_builtin_res_sound; eauto with cse3.
+        eapply external_call_sound; eauto with cse3.
+        
   - (* Icond *)
     econstructor. split.
     + eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.
diff --git a/backend/FirstNopproof.v b/backend/FirstNopproof.v
index 5d9a7d6a..a5d63c25 100644
--- a/backend/FirstNopproof.v
+++ b/backend/FirstNopproof.v
@@ -168,26 +168,25 @@ Proof.
     + constructor; auto with firstnop.
   - left. econstructor. split.
     + eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop.
-      rewrite <- H0.
-      apply eval_addressing_preserved.
-      apply symbols_preserved.
+      all: rewrite <- H0.
+      all: auto using eval_addressing_preserved, symbols_preserved.
     + constructor; auto with firstnop.
   - left. econstructor. split.
     + eapply plus_one. eapply exec_Iload_notrap1; eauto with firstnop.
-      rewrite <- H0.
-      apply eval_addressing_preserved.
+      all: rewrite <- H0;
+      apply eval_addressing_preserved;
       apply symbols_preserved.
     + constructor; auto with firstnop.
   - left. econstructor. split.
     + eapply plus_one. eapply exec_Iload_notrap2; eauto with firstnop.
-      rewrite <- H0.
-      apply eval_addressing_preserved.
+      all: rewrite <- H0;
+      apply eval_addressing_preserved;
       apply symbols_preserved.
     + constructor; auto with firstnop.
   - left. econstructor. split.
     + eapply plus_one. eapply exec_Istore; eauto with firstnop.
-      rewrite <- H0.
-      apply eval_addressing_preserved.
+      all: rewrite <- H0;
+      apply eval_addressing_preserved;
       apply symbols_preserved.
     + constructor; auto with firstnop.
   - left. econstructor. split.
diff --git a/backend/Inject.v b/backend/Inject.v
new file mode 100644
index 00000000..971a5423
--- /dev/null
+++ b/backend/Inject.v
@@ -0,0 +1,122 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL.
+
+Local Open Scope positive.
+
+Inductive inj_instr : Type :=
+  | INJnop
+  | INJop: operation -> list reg -> reg -> inj_instr
+  | INJload: memory_chunk -> addressing -> list reg -> reg -> inj_instr.
+
+Definition inject_instr (i : inj_instr) (pc' : node) : instruction :=
+  match i with
+  | INJnop => Inop pc'
+  | INJop op args dst => Iop op args dst pc'
+  | INJload chunk addr args dst => Iload NOTRAP chunk addr args dst pc'
+  end.
+
+Fixpoint inject_list (prog : code) (pc : node) (dst : node)
+         (l : list inj_instr) : node * code :=
+  let pc' := Pos.succ pc in
+  match l with
+  | nil => (pc', PTree.set pc (Inop dst) prog)
+  | h::t =>
+    inject_list (PTree.set pc (inject_instr h pc') prog)
+                pc' dst t
+  end.
+
+Definition successor (i : instruction) : node :=
+  match i with
+  | Inop pc' => pc'
+  | Iop _ _ _ pc' => pc'
+  | Iload _ _ _ _ _ pc' => pc'
+  | Istore _ _ _ _ pc' => pc'
+  | Icall _ _ _ _ pc' => pc'
+  | Ibuiltin _ _ _ pc' => pc'
+  | Icond _ _ pc' _ _ => pc'
+  | Itailcall _ _ _
+  | Ijumptable _ _
+  | Ireturn _ => 1
+  end.
+
+Definition alter_successor (i : instruction) (pc' : node) : instruction :=
+  match i with
+  | Inop _ => Inop pc'
+  | Iop op args dst _ => Iop op args dst pc'
+  | Iload trap chunk addr args dst _ => Iload trap chunk addr args dst pc'
+  | Istore chunk addr args src _ => Istore chunk addr args src pc'
+  | Ibuiltin ef args res _ => Ibuiltin ef args res pc'
+  | Icond cond args _ pc2 expected => Icond cond args pc' pc2 expected
+  | Icall sig ros args res _ => Icall sig ros args res pc'
+  | Itailcall _ _ _
+  | Ijumptable _ _
+  | Ireturn _ => i
+  end.
+
+Definition inject_at (prog : code) (pc extra_pc : node)
+           (l : list inj_instr) : node * code :=
+  match PTree.get pc prog with
+  | Some i =>
+    inject_list (PTree.set pc (alter_successor i extra_pc) prog)
+                extra_pc (successor i) l
+  | None => inject_list prog extra_pc 1 l (* does not happen *)
+  end.
+
+Definition inject_at' (already : node * code) pc l :=
+  let (extra_pc, prog) := already in
+  inject_at prog pc extra_pc l.
+
+Definition inject_l (prog : code) extra_pc injections :=
+  List.fold_left (fun already (injection : node * (list inj_instr)) =>
+                    inject_at' already (fst injection) (snd injection))
+    injections
+    (extra_pc, prog).
+(*
+Definition inject' (prog : code) (extra_pc : node) (injections : PTree.t (list inj_instr)) :=
+  PTree.fold inject_at' injections (extra_pc, prog).
+
+Definition inject prog extra_pc injections : code :=
+  snd (inject' prog extra_pc injections).
+*)
+
+Section INJECTOR.
+  Variable gen_injections : function -> node -> reg -> PTree.t (list inj_instr).
+
+  Definition valid_injection_instr (max_reg : reg) (i : inj_instr) :=
+    match i with
+    | INJnop => true
+    | INJop op args res => (max_reg <? res) && (negb (is_trapping_op op)
+       && (Datatypes.length args =? args_of_operation op)%nat) 
+    | INJload _ _ _ res => max_reg <? res
+    end.
+  
+  Definition valid_injections1 max_pc max_reg :=
+    List.forallb
+         (fun injection =>
+            ((fst injection) <=? max_pc) &&
+            (List.forallb (valid_injection_instr max_reg) (snd injection))
+         ).
+
+  Definition valid_injections f :=
+    valid_injections1 (max_pc_function f) (max_reg_function f).
+  
+  Definition transf_function (f : function) : res function :=
+    let max_pc := max_pc_function f in
+    let max_reg := max_reg_function f in
+    let injections := PTree.elements (gen_injections f max_pc max_reg) in
+    if valid_injections1 max_pc max_reg injections
+    then
+      OK {| fn_sig := f.(fn_sig);
+            fn_params := f.(fn_params);
+            fn_stacksize := f.(fn_stacksize);
+            fn_code := snd (inject_l (fn_code f) (Pos.succ max_pc) injections);
+            fn_entrypoint := f.(fn_entrypoint) |}
+    else Error (msg "Inject.transf_function: injections at bad locations").
+
+Definition transf_fundef (fd: fundef) : res fundef :=
+  AST.transf_partial_fundef transf_function fd.
+
+Definition transf_program (p: program) : res program :=
+  transform_partial_program transf_fundef p.
+End INJECTOR.
diff --git a/backend/Injectproof.v b/backend/Injectproof.v
new file mode 100644
index 00000000..75fed25f
--- /dev/null
+++ b/backend/Injectproof.v
@@ -0,0 +1,1794 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Globalenvs Values Events.
+Require Import Inject.
+Require Import Lia.
+
+Local Open Scope positive.
+
+Lemma inject_list_preserves:
+  forall l prog pc dst pc0,
+    pc0 < pc ->
+    PTree.get pc0 (snd (inject_list prog pc dst l)) = PTree.get pc0 prog.
+Proof.
+  induction l; intros; simpl.
+  - apply PTree.gso. lia.
+  - rewrite IHl by lia.
+    apply PTree.gso. lia.
+Qed.
+
+Fixpoint pos_add_nat x n :=
+  match n with
+  | O => x
+  | S n' => Pos.succ (pos_add_nat x n')
+  end.
+
+Lemma pos_add_nat_increases : forall x n, x <= (pos_add_nat x n).
+Proof.
+  induction n; simpl; lia.
+Qed.
+
+Lemma pos_add_nat_succ : forall n x,
+    Pos.succ (pos_add_nat x n) = pos_add_nat (Pos.succ x) n.
+Proof.
+  induction n; simpl; intros; trivial.
+  rewrite IHn.
+  reflexivity.
+Qed.
+
+Lemma pos_add_nat_monotone : forall x n1 n2,
+    (n1 < n2) % nat ->
+    (pos_add_nat x n1) < (pos_add_nat x n2).
+Proof.
+  induction n1; destruct n2; intros.
+  - lia.
+  - simpl.
+    pose proof (pos_add_nat_increases x n2).
+    lia.
+  - lia.
+  - simpl.
+    specialize IHn1 with n2.
+    lia.
+Qed.
+
+Lemma inject_list_increases:
+  forall l prog pc dst,
+    (fst (inject_list prog pc dst l)) = pos_add_nat pc (S (List.length l)).
+Proof.
+  induction l; simpl; intros; trivial.
+  rewrite IHl.
+  simpl.
+  rewrite <- pos_add_nat_succ.
+  reflexivity.
+Qed.
+
+Program Fixpoint bounded_nth
+  {T : Type} (k : nat) (l : list T) (BOUND : (k < List.length l)%nat) : T :=
+  match k, l with
+  | O, h::_ => h
+  | (S k'), _::l' => bounded_nth k' l' _
+  | _, nil => _
+  end.
+Obligation 1.
+Proof.
+  simpl in BOUND.
+  lia.
+Qed.
+Obligation 2.
+Proof.
+  simpl in BOUND.
+  lia.
+Qed.
+
+Program Definition bounded_nth_S_statement : Prop :=
+  forall (T : Type) (k : nat) (h : T) (l : list T) (BOUND : (k < List.length l)%nat),
+    bounded_nth (S k) (h::l) _ = bounded_nth k l BOUND.
+Obligation 1.
+lia.
+Qed.
+
+Lemma bounded_nth_proof_irr :
+  forall {T : Type} (k : nat) (l : list T)
+         (BOUND1 BOUND2 : (k < List.length l)%nat),
+    (bounded_nth k l BOUND1) = (bounded_nth k l BOUND2).
+Proof.
+  induction k; destruct l; simpl; intros; trivial; lia.
+Qed.
+
+Lemma bounded_nth_S : bounded_nth_S_statement.
+Proof.
+  unfold bounded_nth_S_statement.
+  induction k; destruct l; simpl; intros; trivial.
+  1, 2: lia.
+  apply bounded_nth_proof_irr.
+Qed.
+
+Lemma inject_list_injected:
+  forall l prog pc dst k (BOUND : (k < (List.length l))%nat),
+    PTree.get (pos_add_nat pc k) (snd (inject_list prog pc dst l)) =
+    Some (inject_instr (bounded_nth k l BOUND) (Pos.succ (pos_add_nat pc k))).
+Proof.
+  induction l; simpl; intros.
+  - lia.
+  - simpl.
+    destruct k as [ | k]; simpl pos_add_nat.
+    + simpl bounded_nth.
+      rewrite inject_list_preserves by lia.
+      apply PTree.gss.
+    + rewrite pos_add_nat_succ.
+      erewrite IHl.
+      f_equal. f_equal.
+      simpl.
+      apply bounded_nth_proof_irr.
+      Unshelve.
+      lia.
+Qed.
+
+Lemma inject_list_injected_end:
+  forall l prog pc dst,
+    PTree.get (pos_add_nat pc (List.length l))
+              (snd (inject_list prog pc dst l)) =
+    Some (Inop dst).
+Proof.
+  induction l; simpl; intros.
+  - apply PTree.gss.
+  - rewrite pos_add_nat_succ.
+    apply IHl.
+Qed.
+    
+Lemma inject_at_preserves :
+  forall prog pc extra_pc l pc0,
+    pc0 < extra_pc ->
+    pc0 <> pc ->
+    PTree.get pc0 (snd (inject_at prog pc extra_pc l)) = PTree.get pc0 prog.
+Proof.
+  intros. unfold inject_at.
+  destruct (PTree.get pc prog) eqn:GET.
+  - rewrite inject_list_preserves; trivial.
+    apply PTree.gso; lia.
+  - apply inject_list_preserves; trivial.
+Qed.
+
+Lemma inject_at_redirects:
+  forall prog pc extra_pc l i,
+    pc < extra_pc ->
+    PTree.get pc prog = Some i ->
+    PTree.get pc (snd (inject_at prog pc extra_pc l)) =
+    Some (alter_successor i extra_pc).
+Proof.
+  intros until i. intros BEFORE GET. unfold inject_at.
+  rewrite GET.
+  rewrite inject_list_preserves by trivial.
+  apply PTree.gss.
+Qed.
+
+Lemma inject_at_redirects_none:
+  forall prog pc extra_pc l,
+    pc < extra_pc ->
+    PTree.get pc prog = None ->
+    PTree.get pc (snd (inject_at prog pc extra_pc l)) = None.
+Proof.
+  intros until l. intros BEFORE GET. unfold inject_at.
+  rewrite GET.
+  rewrite inject_list_preserves by trivial.
+  assumption.
+Qed.
+
+Lemma inject_at_increases:
+  forall prog pc extra_pc l,
+    (fst (inject_at prog pc extra_pc l)) = pos_add_nat extra_pc (S (List.length l)).  
+Proof.
+  intros. unfold inject_at.
+  destruct (PTree.get pc prog).
+  all: apply inject_list_increases.
+Qed.
+
+Lemma inject_at_injected:
+  forall l prog pc extra_pc k (BOUND : (k < (List.length l))%nat),
+    PTree.get (pos_add_nat extra_pc k) (snd (inject_at prog pc extra_pc l)) =
+    Some (inject_instr (bounded_nth k l BOUND) (Pos.succ (pos_add_nat extra_pc k))).
+Proof.
+  intros. unfold inject_at.
+  destruct (prog ! pc); apply inject_list_injected.
+Qed.
+
+Lemma inject_at_injected_end:
+  forall l prog pc extra_pc i,
+    PTree.get pc prog = Some i ->
+    PTree.get (pos_add_nat extra_pc (List.length l))
+              (snd (inject_at prog pc extra_pc l)) =
+    Some (Inop (successor i)).
+Proof.
+  intros until i. intro REW. unfold inject_at.
+  rewrite REW.
+  apply inject_list_injected_end.
+Qed.
+
+Lemma pair_expand:
+  forall { A B : Type } (p : A*B),
+    p = ((fst p), (snd p)).
+Proof.
+  destruct p; simpl; trivial.
+Qed.
+
+Fixpoint inject_l_position extra_pc
+         (injections : list (node * (list inj_instr)))
+         (k : nat) {struct injections} : node :=
+  match injections with
+  | nil => extra_pc
+  | (pc,l)::l' =>
+    match k with
+    | O => extra_pc
+    | S k' =>
+      inject_l_position
+        (Pos.succ (pos_add_nat extra_pc (List.length l))) l' k'
+    end
+  end.
+
+Lemma inject_l_position_increases : forall injections pc k,
+    pc <= inject_l_position pc injections k.
+Proof.
+  induction injections; simpl; intros.
+  lia.
+  destruct a as [_ l].
+  destruct k.
+  lia.
+  specialize IHinjections with (pc := (Pos.succ (pos_add_nat pc (Datatypes.length l)))) (k := k).
+  assert (pc <= (pos_add_nat pc (Datatypes.length l))) by apply pos_add_nat_increases.
+  lia.
+Qed.
+                    
+Definition inject_l (prog : code) extra_pc injections :=
+  List.fold_left (fun already (injection : node * (list inj_instr)) =>
+                    inject_at' already (fst injection) (snd injection))
+    injections
+    (extra_pc, prog).
+
+Lemma inject_l_preserves :
+  forall injections prog extra_pc pc0,
+    pc0 < extra_pc ->
+    List.forallb (fun injection => if peq (fst injection) pc0 then false else true) injections = true ->
+    PTree.get pc0 (snd (inject_l prog extra_pc injections)) = PTree.get pc0 prog.
+Proof.
+  induction injections;
+    intros until pc0; intros BEFORE ALL; simpl; trivial.
+  unfold inject_l.
+  destruct a as [pc l]. simpl.
+  simpl in ALL.
+  rewrite andb_true_iff in ALL.
+  destruct ALL as [NEQ ALL].
+  rewrite pair_expand with (p := inject_at prog pc extra_pc l).
+  fold (inject_l (snd (inject_at prog pc extra_pc l))
+              (fst (inject_at prog pc extra_pc l))
+              injections).
+  rewrite IHinjections; trivial.
+  - apply inject_at_preserves; trivial.
+    destruct (peq pc pc0); congruence.
+  - rewrite inject_at_increases.
+    pose proof (pos_add_nat_increases extra_pc (S (Datatypes.length l))).
+    lia.
+Qed.
+
+Lemma nth_error_nil : forall { T : Type} k,
+    nth_error (@nil T) k = None.
+Proof.
+  destruct k; simpl; trivial.
+Qed.
+
+Lemma inject_l_injected:
+  forall injections prog injnum pc l extra_pc k
+         (BELOW : forallb (fun injection => (fst injection) <? extra_pc) injections = true)
+         (NUMBER : nth_error injections injnum = Some (pc, l))
+         (BOUND : (k < (List.length l))%nat),
+    PTree.get (pos_add_nat (inject_l_position extra_pc injections injnum) k)
+              (snd (inject_l prog extra_pc injections)) =
+    Some (inject_instr (bounded_nth k l BOUND)
+       (Pos.succ (pos_add_nat (inject_l_position extra_pc injections injnum) k))).
+Proof.
+  induction injections; intros.
+  { rewrite nth_error_nil in NUMBER.
+    discriminate NUMBER.
+  }
+  simpl in BELOW.
+  rewrite andb_true_iff in BELOW.
+  destruct BELOW as [BELOW1 BELOW2].
+  unfold inject_l.
+  destruct a as [pc' l'].
+  simpl fold_left.
+  rewrite pair_expand with (p := inject_at prog pc' extra_pc l').
+  progress fold (inject_l (snd (inject_at prog pc' extra_pc l'))
+              (fst (inject_at prog pc' extra_pc l'))
+              injections).
+  destruct injnum as [ | injnum']; simpl in NUMBER.
+  { inv NUMBER.
+    rewrite inject_l_preserves; simpl.
+    - apply inject_at_injected.
+    - rewrite inject_at_increases.
+      apply pos_add_nat_monotone.
+      lia.
+    - rewrite forallb_forall.
+      rewrite forallb_forall in BELOW2.
+      intros loc IN.
+      specialize BELOW2 with loc.
+      apply BELOW2 in IN.
+      destruct peq as [EQ | ]; trivial.
+      rewrite EQ in IN.
+      rewrite Pos.ltb_lt in IN.
+      pose proof (pos_add_nat_increases extra_pc k).
+      lia.
+  }
+  simpl.
+  rewrite inject_at_increases.
+  apply IHinjections with (pc := pc); trivial.
+  rewrite forallb_forall.
+  rewrite forallb_forall in BELOW2.
+  intros loc IN.
+  specialize BELOW2 with loc.
+  apply BELOW2 in IN.
+  pose proof (pos_add_nat_increases extra_pc (Datatypes.length l')).
+  rewrite Pos.ltb_lt.
+  rewrite Pos.ltb_lt in IN.
+  lia.
+Qed.
+
+Lemma inject_l_injected_end:
+  forall injections prog injnum pc i l extra_pc
+         (BEFORE : PTree.get pc prog = Some i)
+         (DISTINCT : list_norepet (map fst injections))
+         (BELOW : forallb (fun injection => (fst injection) <? extra_pc) injections = true)
+         (NUMBER : nth_error injections injnum = Some (pc, l)),
+    PTree.get (pos_add_nat (inject_l_position extra_pc injections injnum)
+                           (List.length l))
+              (snd (inject_l prog extra_pc injections)) =
+    Some (Inop (successor i)).
+Proof.
+  induction injections; intros.
+  { rewrite nth_error_nil in NUMBER.
+    discriminate NUMBER.
+  }
+  simpl in BELOW.
+  rewrite andb_true_iff in BELOW.
+  destruct BELOW as [BELOW1 BELOW2].
+  unfold inject_l.
+  destruct a as [pc' l'].
+  simpl fold_left.
+  rewrite pair_expand with (p := inject_at prog pc' extra_pc l').
+  progress fold (inject_l (snd (inject_at prog pc' extra_pc l'))
+              (fst (inject_at prog pc' extra_pc l'))
+              injections).
+  destruct injnum as [ | injnum']; simpl in NUMBER.
+  { inv NUMBER.
+    rewrite inject_l_preserves; simpl.
+    - apply inject_at_injected_end; trivial.
+    - rewrite inject_at_increases.
+      apply pos_add_nat_monotone.
+      lia.
+    - rewrite forallb_forall.
+      rewrite forallb_forall in BELOW2.
+      intros loc IN.
+      specialize BELOW2 with loc.
+      apply BELOW2 in IN.
+      destruct peq as [EQ | ]; trivial.
+      rewrite EQ in IN.
+      rewrite Pos.ltb_lt in IN.
+      pose proof (pos_add_nat_increases extra_pc (Datatypes.length l)).
+      lia.
+  }
+  simpl.
+  rewrite inject_at_increases.
+  apply IHinjections with (pc := pc); trivial.
+  {
+    rewrite <- BEFORE.
+    apply inject_at_preserves.
+    {
+      apply nth_error_In in NUMBER.
+      rewrite forallb_forall in BELOW2.
+      specialize BELOW2 with (pc, l).
+      apply BELOW2 in NUMBER.
+      apply Pos.ltb_lt in NUMBER.
+      simpl in NUMBER.
+      assumption.
+    }
+    simpl in DISTINCT.
+    inv DISTINCT.
+    intro SAME.
+    subst pc'.
+    apply nth_error_in in NUMBER.
+    assert (In (fst (pc, l)) (map fst injections)) as Z.
+    { apply in_map. assumption.
+    }
+    simpl in Z.
+    auto.
+  }
+  { inv DISTINCT.
+    assumption.
+  }
+  {
+    rewrite forallb_forall.
+    rewrite forallb_forall in BELOW2.
+    intros loc IN.
+    specialize BELOW2 with loc.
+    apply BELOW2 in IN.
+    pose proof (pos_add_nat_increases extra_pc (Datatypes.length l')).
+    rewrite Pos.ltb_lt.
+    rewrite Pos.ltb_lt in IN.
+    assert (pos_add_nat extra_pc (Datatypes.length l') <
+            pos_add_nat extra_pc (S (Datatypes.length l'))).
+    { apply pos_add_nat_monotone.
+      lia.
+    }
+    lia.
+  }
+Qed.
+
+
+Lemma inject_l_redirects:
+  forall injections prog injnum pc i l extra_pc
+         (BEFORE : PTree.get pc prog = Some i)
+         (DISTINCT : list_norepet (map fst injections))
+         (BELOW : forallb (fun injection => (fst injection) <? extra_pc) injections = true)
+         (NUMBER : nth_error injections injnum = Some (pc, l)),
+    PTree.get pc (snd (inject_l prog extra_pc injections)) =
+    Some (alter_successor i (inject_l_position extra_pc injections injnum)).
+Proof.
+  induction injections; intros.
+  { rewrite nth_error_nil in NUMBER.
+    discriminate NUMBER.
+  }
+  simpl in BELOW.
+  rewrite andb_true_iff in BELOW.
+  destruct BELOW as [BELOW1 BELOW2].
+  unfold inject_l.
+  destruct a as [pc' l'].
+  simpl fold_left.
+  rewrite pair_expand with (p := inject_at prog pc' extra_pc l').
+  progress fold (inject_l (snd (inject_at prog pc' extra_pc l'))
+              (fst (inject_at prog pc' extra_pc l'))
+              injections).
+  simpl in BELOW1.
+  apply Pos.ltb_lt in BELOW1.
+  inv DISTINCT.
+  destruct injnum as [ | injnum']; simpl in NUMBER.
+  { inv NUMBER.
+    rewrite inject_l_preserves; simpl.
+    - apply inject_at_redirects; trivial.
+    - rewrite inject_at_increases.
+      pose proof (pos_add_nat_increases extra_pc (S (Datatypes.length l))).
+      lia.
+    - rewrite forallb_forall.
+      intros loc IN.
+      destruct loc as [pc' l'].
+      simpl in *.
+      destruct peq; trivial.
+      subst pc'.
+      apply in_map with (f := fst) in IN.
+      simpl in IN.
+      exfalso.
+      auto.
+  }
+  simpl.
+  rewrite inject_at_increases.
+  apply IHinjections with (pc := pc) (l := l); trivial.
+  {
+    rewrite <- BEFORE.
+    apply nth_error_In in NUMBER.
+    rewrite forallb_forall in BELOW2.
+    specialize BELOW2 with (pc, l).
+    simpl in BELOW2.
+    rewrite Pos.ltb_lt in BELOW2.
+    apply inject_at_preserves; auto.
+    assert (In (fst (pc, l)) (map fst injections)) as Z.
+    { apply in_map. assumption.
+    }
+    simpl in Z.
+    intro EQ.
+    subst pc'.
+    auto.
+  }
+  {
+    rewrite forallb_forall.
+    rewrite forallb_forall in BELOW2.
+    intros loc IN.
+    specialize BELOW2 with loc.
+    apply BELOW2 in IN.
+    pose proof (pos_add_nat_increases extra_pc (Datatypes.length l')).
+    rewrite Pos.ltb_lt.
+    rewrite Pos.ltb_lt in IN.
+    assert (pos_add_nat extra_pc (Datatypes.length l') <
+            pos_add_nat extra_pc (S (Datatypes.length l'))).
+    { apply pos_add_nat_monotone.
+      lia.
+    }
+    lia.
+  }
+Qed.
+
+(*
+Lemma inject'_preserves :
+  forall injections prog extra_pc pc0,
+    pc0 < extra_pc ->
+    PTree.get pc0 injections = None ->
+    PTree.get pc0 (snd (inject' prog extra_pc injections)) = PTree.get pc0 prog.
+Proof.
+  intros. unfold inject'.
+  rewrite PTree.fold_spec.
+  change (fold_left
+        (fun (a : node * code) (p : positive * list inj_instr) =>
+         inject_at' a (fst p) (snd p)) (PTree.elements injections)
+        (extra_pc, prog)) with (inject_l prog extra_pc (PTree.elements injections)).
+  apply inject_l_preserves; trivial.
+  rewrite List.forallb_forall.
+  intros injection IN.
+  destruct injection as [pc l].
+  simpl.
+  apply PTree.elements_complete in IN.
+  destruct (peq pc pc0); trivial.
+  congruence.
+Qed.
+
+Lemma inject_preserves :
+  forall injections prog extra_pc pc0,
+    pc0 < extra_pc ->
+    PTree.get pc0 injections = None ->
+    PTree.get pc0 (inject prog extra_pc injections) = PTree.get pc0 prog.
+Proof.
+  unfold inject'.
+  apply inject'_preserves.
+Qed.
+*)
+
+Section INJECTOR.
+  Variable gen_injections : function -> node -> reg -> PTree.t (list inj_instr).
+
+  Definition match_prog (p tp: RTL.program) :=
+    match_program (fun ctx f tf => transf_fundef gen_injections f = OK tf) eq p tp.
+
+  Lemma transf_program_match:
+    forall p tp, transf_program gen_injections p = OK tp -> match_prog p tp.
+  Proof.
+    intros. eapply match_transform_partial_program; eauto.
+  Qed.
+
+  Section PRESERVATION.
+
+    Variables prog tprog: program.
+    Hypothesis TRANSF: match_prog prog tprog.
+    Let ge := Genv.globalenv prog.
+    Let tge := Genv.globalenv tprog.
+
+    Definition match_regs (f : function) (rs rs' : regset) :=
+      forall r, r <= max_reg_function f -> (rs'#r = rs#r).
+
+    Lemma match_regs_refl : forall f rs, match_regs f rs rs.
+    Proof.
+      unfold match_regs. intros. trivial.
+    Qed.
+
+    Lemma match_regs_trans : forall f rs1 rs2 rs3,
+        match_regs f rs1 rs2 -> match_regs f rs2 rs3 -> match_regs f rs1 rs3.
+    Proof.
+      unfold match_regs. intros until rs3. intros M12 M23 r.
+      specialize M12 with r.
+      specialize M23 with r.
+      intuition congruence.
+    Qed.
+
+    Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
+    | match_frames_intro: forall res f tf sp pc pc' rs trs
+        (FUN : transf_function gen_injections f = OK tf)
+        (REGS : match_regs f rs trs)
+        (STAR:
+           forall ts m trs1,
+           exists trs2,
+             (match_regs f trs1 trs2) /\
+             Smallstep.star RTL.step tge
+                                      (State ts tf sp pc' trs1 m) E0
+                                      (State ts tf sp pc trs2 m)),
+        match_frames (Stackframe res f sp pc rs)
+                     (Stackframe res tf sp pc' trs).
+
+    Inductive match_states: state -> state -> Prop :=
+    | match_states_intro:
+      forall s f tf sp pc rs trs m ts
+        (FUN : transf_function gen_injections f = OK tf)
+        (STACKS: list_forall2 match_frames s ts)
+        (REGS: match_regs f rs trs),
+      match_states (State s f sp pc rs m) (State ts tf sp pc trs m)
+    | match_states_call:
+        forall s fd tfd args m ts
+        (FUN : transf_fundef gen_injections fd = OK tfd)
+        (STACKS: list_forall2 match_frames s ts),
+          match_states (Callstate s fd args m) (Callstate ts tfd args m)
+    | match_states_return:
+        forall s res m ts
+               (STACKS: list_forall2 match_frames s ts),
+          match_states (Returnstate s res m)
+                       (Returnstate ts res m).
+
+    Lemma functions_translated:
+      forall (v: val) (f: RTL.fundef),
+        Genv.find_funct ge v = Some f ->
+        exists tf,
+          Genv.find_funct tge v = Some tf /\
+          transf_fundef gen_injections f = OK tf.
+    Proof.
+      apply (Genv.find_funct_transf_partial TRANSF).
+    Qed.
+
+    Lemma function_ptr_translated:
+      forall (b: block) (f: RTL.fundef),
+        Genv.find_funct_ptr ge b = Some f ->
+        exists tf,
+          Genv.find_funct_ptr tge b = Some tf /\
+          transf_fundef gen_injections f = OK tf.
+    Proof.
+      apply (Genv.find_funct_ptr_transf_partial TRANSF).
+    Qed.
+
+    Lemma symbols_preserved:
+      forall id,
+        Genv.find_symbol tge id = Genv.find_symbol ge id.
+    Proof.
+      apply (Genv.find_symbol_match TRANSF).
+    Qed.
+
+    Lemma senv_preserved:
+      Senv.equiv ge tge.
+    Proof.
+      apply (Genv.senv_match TRANSF).
+    Qed.
+
+    Lemma sig_preserved:
+      forall f tf, transf_fundef gen_injections f = OK tf
+                   -> funsig tf = funsig f.
+    Proof.
+      destruct f; simpl; intros; monadInv H; trivial.
+      unfold transf_function in *.
+      destruct valid_injections1 in EQ.
+      2: discriminate.
+      inv EQ.
+      reflexivity.
+    Qed.
+
+    Lemma stacksize_preserved:
+      forall f tf, transf_function gen_injections f = OK tf ->
+                   fn_stacksize tf = fn_stacksize f.
+    Proof.
+      destruct f.
+      unfold transf_function.
+      intros.
+      destruct valid_injections1 in H.
+      2: discriminate.
+      inv H.
+      reflexivity.
+    Qed.
+
+    Lemma params_preserved:
+      forall f tf, transf_function gen_injections f = OK tf ->
+                   fn_params tf = fn_params f.
+    Proof.
+      destruct f.
+      unfold transf_function.
+      intros.
+      destruct valid_injections1 in H.
+      2: discriminate.
+      inv H.
+      reflexivity.
+    Qed.
+
+    Lemma entrypoint_preserved:
+      forall f tf, transf_function gen_injections f = OK tf ->
+                   fn_entrypoint tf = fn_entrypoint f.
+    Proof.
+      destruct f.
+      unfold transf_function.
+      intros.
+      destruct valid_injections1 in H.
+      2: discriminate.
+      inv H.
+      reflexivity.
+    Qed.
+
+    Lemma sig_preserved2:
+      forall f tf, transf_function gen_injections f = OK tf ->
+                   fn_sig tf = fn_sig f.
+    Proof.
+      destruct f.
+      unfold transf_function.
+      intros.
+      destruct valid_injections1 in H.
+      2: discriminate.
+      inv H.
+      reflexivity.
+    Qed.
+
+    Lemma transf_initial_states:
+      forall S1, RTL.initial_state prog S1 ->
+                 exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2.
+    Proof.
+      intros. inversion H.
+      exploit function_ptr_translated; eauto.
+      intros (tf & A & B).
+      exists (Callstate nil tf nil m0); split.
+      - econstructor; eauto.
+        + eapply (Genv.init_mem_match TRANSF); eauto.
+        + replace (prog_main tprog) with (prog_main prog).
+          rewrite symbols_preserved. eauto.
+          symmetry. eapply match_program_main; eauto.
+        + rewrite <- H3. eapply sig_preserved; eauto.
+      - constructor; trivial.
+        constructor.
+    Qed.
+
+    Lemma 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.
+
+    Lemma assign_above:
+      forall f trs res v,
+        (max_reg_function f) < res ->
+        match_regs f trs trs # res <- v.
+    Proof.
+      unfold match_regs.
+      intros.
+      apply Regmap.gso.
+      lia.
+    Qed.
+    
+    Lemma transf_function_inj_step:
+      forall ts f tf sp pc trs m ii
+        (FUN : transf_function gen_injections f = OK tf)
+        (GET : (fn_code tf) ! pc = Some (inject_instr ii (Pos.succ pc)))
+        (VALID : valid_injection_instr (max_reg_function f) ii = true),
+      exists trs',
+        RTL.step tge
+              (State ts tf sp pc trs m) E0
+              (State ts tf sp (Pos.succ pc) trs' m) /\
+        match_regs (f : function) trs trs'.
+    Proof.
+      destruct ii as [ |op args res | chunk addr args res]; simpl; intros.
+      - exists trs.
+        split.
+        * apply exec_Inop; assumption.
+        * apply match_regs_refl.
+      - repeat rewrite andb_true_iff in VALID.
+        rewrite negb_true_iff in VALID.
+        destruct VALID as (MAX_REG & NOTRAP & LENGTH).
+        rewrite Pos.ltb_lt in MAX_REG.
+        rewrite Nat.eqb_eq in LENGTH.
+        destruct (eval_operation ge sp op trs ## args m) as [v | ] eqn:EVAL.
+        + exists (trs # res <- v).
+          split.
+          * apply exec_Iop with (op := op) (args := args) (res := res); trivial.
+            rewrite eval_operation_preserved with (ge1 := ge).
+            assumption.
+            exact symbols_preserved.
+          * apply assign_above; auto.
+        + exfalso.
+          generalize EVAL.
+          apply is_trapping_op_sound; trivial.
+          rewrite map_length.
+          assumption.
+      - rewrite Pos.ltb_lt in VALID.
+        destruct (eval_addressing ge sp addr trs ## args) as [a | ] eqn:ADDR.
+        + destruct (Mem.loadv chunk m a) as [v | ] eqn:LOAD.
+          * exists (trs # res <- v).
+            split.
+            ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial.
+               all: try rewrite eval_addressing_preserved with (ge1 := ge).
+               all: auto using symbols_preserved.
+            ** apply assign_above; auto.
+          * exists (trs # res <- Vundef).
+            split.
+            ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial.
+               all: rewrite eval_addressing_preserved with (ge1 := ge).
+               all: auto using symbols_preserved.
+            ** apply assign_above; auto.
+        + exists (trs # res <- Vundef).
+          split.
+          * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial.
+            all: rewrite eval_addressing_preserved with (ge1 := ge).
+            all: auto using symbols_preserved.
+          * apply assign_above; auto.
+    Qed.
+
+    Lemma bounded_nth_In: forall {T : Type} (l : list T) k LESS,
+        In (bounded_nth k l LESS) l.
+    Proof.
+      induction l; simpl; intros.
+      lia.
+      destruct k; simpl.
+      - left; trivial.
+      - right. apply IHl.
+    Qed.
+
+    Lemma transf_function_inj_starstep_rec :
+      forall ts f tf sp m inj_n src_pc inj_pc inj_code
+        (FUN : transf_function gen_injections f = OK tf)
+        (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n =
+               Some (src_pc, inj_code))
+        (POSITION : inject_l_position (Pos.succ (max_pc_function f))
+                                      (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc)
+        (k : nat)
+        (CUR : (k <= (List.length inj_code))%nat)
+        (trs : regset),
+      exists trs',
+        match_regs (f : function) trs trs' /\
+        Smallstep.star RTL.step tge
+              (State ts tf sp (pos_add_nat inj_pc
+                                    ((List.length inj_code) - k)%nat) trs m) E0
+              (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs' m).
+    Proof.
+      induction k; simpl; intros.
+      { rewrite Nat.sub_0_r.
+        exists trs.
+        split.
+        - apply match_regs_refl.
+        - constructor.
+      }
+      assert (k <= Datatypes.length inj_code)%nat as KK by lia.
+      pose proof (IHk KK) as IH.
+      clear IHk KK.
+      pose proof FUN as VALIDATE.
+      unfold transf_function, valid_injections1 in VALIDATE.
+      destruct forallb eqn:FORALL in VALIDATE.
+      2: discriminate.
+      injection VALIDATE.
+      intro TF.
+      symmetry in TF.
+      pose proof (inject_l_injected (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) (fn_code f) inj_n src_pc inj_code (Pos.succ (max_pc_function f)) ((List.length inj_code) - (S k))%nat) as INJECTED.
+      lapply INJECTED.
+      { clear INJECTED.
+        intro INJECTED.
+        assert ((Datatypes.length inj_code - S k <
+                 Datatypes.length inj_code)%nat) as LESS by lia.
+        pose proof (INJECTED INJ LESS) as INJ'.
+        replace (snd
+            (inject_l (fn_code f) (Pos.succ (max_pc_function f))
+                      (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))))) with (fn_code tf) in INJ'.
+        2: rewrite TF; simpl; reflexivity.                                              apply transf_function_inj_step with (f:=f) (ts:=ts) (sp:=sp) (trs:=trs) (m := m) in INJ'.
+        2: assumption.
+        {
+          destruct INJ' as [trs'' [STEP STEPMATCH]].
+          destruct (IH trs'') as [trs' [STARSTEPMATCH STARSTEP]].
+          exists trs'.
+          split.
+          { apply match_regs_trans with (rs2 := trs''); assumption. }
+          eapply Smallstep.star_step with (t1:=E0) (t2:=E0).
+          {
+            rewrite POSITION in STEP.
+            exact STEP.
+          }
+          {
+            replace (Datatypes.length inj_code - k)%nat
+              with (S (Datatypes.length inj_code - (S k)))%nat in STARSTEP by lia.
+            simpl pos_add_nat in STARSTEP.
+            exact STARSTEP.
+          }
+          constructor.
+        }
+        rewrite forallb_forall in FORALL.
+        specialize FORALL with  (src_pc, inj_code).
+        lapply FORALL.
+        {
+          simpl.
+          rewrite andb_true_iff.
+          intros (SRC & ALL_VALID).
+          rewrite forallb_forall in ALL_VALID.
+          apply ALL_VALID.
+          apply bounded_nth_In.
+        }
+        apply nth_error_In with (n := inj_n).
+        assumption.
+      }
+      rewrite forallb_forall in FORALL.
+      rewrite forallb_forall.
+      intros x INx.
+      rewrite Pos.ltb_lt.
+      pose proof (FORALL x INx) as ALLx.
+      rewrite andb_true_iff in ALLx.
+      destruct ALLx as [ALLx1 ALLx2].
+      rewrite Pos.leb_le in ALLx1.
+      lia.
+    Qed.
+    
+    Lemma transf_function_inj_starstep :
+      forall ts f tf sp m inj_n src_pc inj_pc inj_code
+        (FUN : transf_function gen_injections f = OK tf)
+        (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n =
+               Some (src_pc, inj_code))
+        (POSITION : inject_l_position (Pos.succ (max_pc_function f))
+                                      (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc)
+        (trs : regset),
+      exists trs',
+        match_regs (f : function) trs trs' /\
+        Smallstep.star RTL.step tge
+              (State ts tf sp inj_pc trs m) E0
+              (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs' m).
+    Proof.
+      intros.
+      replace (State ts tf sp inj_pc trs m) with (State ts tf sp (pos_add_nat inj_pc ((List.length inj_code) - (List.length inj_code))%nat) trs m).
+      eapply transf_function_inj_starstep_rec; eauto.
+      f_equal.
+      rewrite <- minus_n_n.
+      reflexivity.
+    Qed.
+
+    Lemma transf_function_inj_end :
+      forall ts f tf sp m inj_n src_pc inj_pc inj_code i
+        (FUN : transf_function gen_injections f = OK tf)
+        (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n =
+               Some (src_pc, inj_code))
+        (SRC: (fn_code f) ! src_pc = Some i)
+        (POSITION : inject_l_position (Pos.succ (max_pc_function f))
+                                      (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc)
+        (trs : regset),
+        RTL.step tge
+          (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs m) E0
+          (State ts tf sp (successor i) trs m).
+    Proof.
+      intros.
+      pose proof FUN as VALIDATE.
+      unfold transf_function, valid_injections1 in VALIDATE.
+      destruct forallb eqn:FORALL in VALIDATE.
+      2: discriminate.
+      injection VALIDATE.
+      intro TF.
+      symmetry in TF.
+      pose proof (inject_l_injected_end (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) (fn_code f) inj_n src_pc i inj_code (Pos.succ (max_pc_function f))) as INJECTED.
+      lapply INJECTED.
+      2: assumption.
+      clear INJECTED.
+      intro INJECTED.
+      lapply INJECTED.
+      2: apply (PTree.elements_keys_norepet (gen_injections f (max_pc_function f) (max_reg_function f))); fail.
+      clear INJECTED.
+      intro INJECTED.
+      lapply INJECTED.
+      { clear INJECTED.
+        intro INJECTED.
+        pose proof (INJECTED INJ) as INJ'.
+        clear INJECTED.
+        replace (snd
+                   (inject_l (fn_code f) (Pos.succ (max_pc_function f))
+                             (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))))) with (fn_code tf) in INJ'.
+        2: rewrite TF; simpl; reflexivity.
+        rewrite POSITION in INJ'.
+        apply exec_Inop.
+        assumption.
+      }
+      clear INJECTED.
+      rewrite forallb_forall in FORALL.
+      rewrite forallb_forall.
+      intros x INx.
+      rewrite Pos.ltb_lt.
+      pose proof (FORALL x INx) as ALLx.
+      rewrite andb_true_iff in ALLx.
+      destruct ALLx as [ALLx1 ALLx2].
+      rewrite Pos.leb_le in ALLx1.
+      lia.
+    Qed.
+
+    Lemma transf_function_inj_plusstep :
+      forall ts f tf sp m inj_n src_pc inj_pc inj_code i
+        (FUN : transf_function gen_injections f = OK tf)
+        (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n =
+               Some (src_pc, inj_code))
+        (SRC: (fn_code f) ! src_pc = Some i)
+        (POSITION : inject_l_position (Pos.succ (max_pc_function f))
+                                      (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc)
+        (trs : regset),
+      exists trs',
+        match_regs (f : function) trs trs' /\
+        Smallstep.plus RTL.step tge
+              (State ts tf sp inj_pc trs m) E0
+              (State ts tf sp (successor i) trs' m).
+    Proof.
+      intros.
+      destruct (transf_function_inj_starstep ts f tf sp m inj_n src_pc inj_pc inj_code FUN INJ POSITION trs) as [trs' [MATCH PLUS]].
+      exists trs'.
+      split. assumption.
+      eapply Smallstep.plus_right.
+      exact PLUS.
+      eapply transf_function_inj_end; eassumption.
+      reflexivity.
+    Qed.
+    
+    Lemma transf_function_preserves:
+      forall f tf pc 
+        (FUN : transf_function gen_injections f = OK tf)
+        (LESS : pc <= max_pc_function f)
+        (NOCHANGE : (gen_injections f (max_pc_function f) (max_reg_function f)) ! pc = None),
+        (fn_code tf) ! pc = (fn_code f) ! pc.
+    Proof.
+      intros.
+      unfold transf_function in FUN.
+      destruct valid_injections1 in FUN.
+      2: discriminate.
+      inv FUN.
+      simpl.
+      apply inject_l_preserves.
+      lia.
+      rewrite forallb_forall.
+      intros x INx.
+      destruct peq; trivial.
+      subst pc.
+      exfalso.
+      destruct x as [pc ii].
+      simpl in *.
+      apply PTree.elements_complete in INx.
+      congruence.
+    Qed.
+    
+    Lemma transf_function_redirects:
+      forall f tf pc injl ii
+        (FUN : transf_function gen_injections f = OK tf)
+        (LESS : pc <= max_pc_function f)
+        (INJECTION : (gen_injections f (max_pc_function f) (max_reg_function f)) ! pc = Some injl)
+        (INSTR: (fn_code f) ! pc = Some ii),
+      exists pc' : node,
+        (fn_code tf) ! pc = Some (alter_successor ii pc') /\
+        (forall ts sp m trs,
+            exists trs',
+            match_regs f trs trs' /\
+            Smallstep.plus RTL.step tge
+              (State ts tf sp pc' trs m) E0
+              (State ts tf sp (successor ii) trs' m)).        
+    Proof.
+      intros.
+      apply PTree.elements_correct in INJECTION.
+      apply In_nth_error in INJECTION.
+      destruct INJECTION as [injn INJECTION].
+      exists (inject_l_position (Pos.succ (max_pc_function f))
+                                (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) injn).
+      split.
+      { unfold transf_function in FUN.
+        destruct (valid_injections1) eqn:VALID in FUN.
+        2: discriminate.
+        inv FUN.
+        simpl.
+        apply inject_l_redirects with (l := injl); auto.
+        apply PTree.elements_keys_norepet.
+        unfold valid_injections1 in VALID.
+        rewrite forallb_forall in VALID.
+        rewrite forallb_forall.
+        intros x INx.
+        pose proof (VALID x INx) as VALIDx.
+        clear VALID.
+        rewrite andb_true_iff in VALIDx.
+        rewrite Pos.leb_le in VALIDx.
+        destruct VALIDx as [VALIDx1 VALIDx2].
+        rewrite Pos.ltb_lt.
+        lia.
+      }
+      intros.
+      pose proof (transf_function_inj_plusstep ts f tf sp m injn pc
+                 (inject_l_position (Pos.succ (max_pc_function f))
+                                    (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) injn)
+                 injl ii FUN INJECTION INSTR) as TRANS.
+      lapply TRANS.
+      2: reflexivity.
+      clear TRANS.
+      intro TRANS.
+      exact (TRANS trs).
+    Qed.
+
+    Lemma transf_function_preserves_uses:
+      forall f tf pc rs trs ii
+        (FUN : transf_function gen_injections f = OK tf)
+        (MATCH : match_regs f rs trs)
+        (INSTR : (fn_code f) ! pc = Some ii),
+        trs ## (instr_uses ii) = rs ## (instr_uses ii).
+    Proof.
+      intros.
+      assert (forall r, In r (instr_uses ii) ->
+                        trs # r = rs # r) as SAME.
+      {
+        intros r INr.
+        apply MATCH.
+        apply (max_reg_function_use f pc ii); auto.
+      }
+      induction (instr_uses ii); simpl; trivial.
+      f_equal.
+      - apply SAME. constructor; trivial.
+      - apply IHl. intros.
+        apply SAME. right. assumption.
+    Qed.
+
+    (*
+    Lemma transf_function_preserves_builtin_arg:
+      forall rs trs ef res sp m pc'
+        (arg : builtin_arg reg)
+        (SAME : (forall r,
+                    In r (instr_uses (Ibuiltin ef args res pc')) ->
+                    trs # r = rs # r) )
+        varg
+        (EVAL : eval_builtin_arg ge (fun r => rs#r) sp m arg varg),
+        eval_builtin_arg ge (fun r => trs#r) sp m arg varg.
+    Proof.
+     *)
+    
+    Lemma transf_function_preserves_builtin_args_rec:
+      forall rs trs ef res sp m pc'
+        (args : list (builtin_arg reg))
+        (SAME : (forall r,
+                    In r (instr_uses (Ibuiltin ef args res pc')) ->
+                       trs # r = rs # r) )
+        (vargs : list val)
+        (EVAL : eval_builtin_args ge (fun r => rs#r) sp m args vargs),
+        eval_builtin_args ge (fun r => trs#r) sp m args vargs.
+    Proof.
+      unfold eval_builtin_args.
+      induction args; intros; inv EVAL.
+      - constructor.
+      - constructor.
+        + induction H1.
+          all: try (constructor; auto; fail).
+          * rewrite <- SAME.
+            apply eval_BA.
+            simpl.
+            left. reflexivity.
+          * constructor.
+            ** apply IHeval_builtin_arg1.
+               intros r INr.
+               apply SAME.
+               simpl.
+               simpl in INr.
+               rewrite in_app in INr.
+               rewrite in_app.
+               rewrite in_app.
+               tauto.
+            ** apply IHeval_builtin_arg2.
+               intros r INr.
+               apply SAME.
+               simpl.
+               simpl in INr.
+               rewrite in_app in INr.
+               rewrite in_app.
+               rewrite in_app.
+               tauto.
+          * constructor.
+            ** apply IHeval_builtin_arg1.
+               intros r INr.
+               apply SAME.
+               simpl.
+               simpl in INr.
+               rewrite in_app in INr.
+               rewrite in_app.
+               rewrite in_app.
+               tauto.
+            ** apply IHeval_builtin_arg2.
+               intros r INr.
+               apply SAME.
+               simpl.
+               simpl in INr.
+               rewrite in_app in INr.
+               rewrite in_app.
+               rewrite in_app.
+               tauto.
+        + apply IHargs.
+          2: assumption.
+          intros r INr.
+          apply SAME.
+          simpl.
+          apply in_or_app.
+          right.
+          exact INr.
+    Qed.
+    
+    Lemma transf_function_preserves_builtin_args:
+      forall f tf pc rs trs ef res sp m pc'
+        (args : list (builtin_arg reg))
+        (FUN : transf_function gen_injections f = OK tf)
+        (MATCH : match_regs f rs trs)
+        (INSTR : (fn_code f) ! pc = Some (Ibuiltin ef args res pc'))
+        (vargs : list val)
+        (EVAL : eval_builtin_args ge (fun r => rs#r) sp m args vargs),
+        eval_builtin_args ge (fun r => trs#r) sp m args vargs.
+    Proof.
+      intros.
+      apply transf_function_preserves_builtin_args_rec with (rs := rs) (ef := ef) (res := res) (pc' := pc').
+      intros r INr.
+      apply MATCH.
+      apply (max_reg_function_use f pc (Ibuiltin ef args res pc')).
+      all: auto.
+    Qed.
+    
+    Lemma match_regs_write:
+      forall f rs trs res v
+             (MATCH : match_regs f rs trs),
+        match_regs f (rs # res <- v) (trs # res <- v).
+    Proof.
+      intros.
+      intros r LESS.
+      destruct (peq r res).
+      {
+        subst r.
+        rewrite Regmap.gss.
+        symmetry.
+        apply Regmap.gss.
+      }
+      rewrite Regmap.gso.
+      rewrite Regmap.gso.
+      all: trivial.
+      apply MATCH.
+      trivial.
+    Qed.
+
+    Lemma match_regs_setres:
+      forall f res rs trs vres
+             (MATCH : match_regs f rs trs),
+        match_regs f (regmap_setres res vres rs) (regmap_setres res vres trs).
+    Proof.
+      induction res; simpl; intros; trivial.
+      apply match_regs_write; auto.
+    Qed.
+    
+    Lemma transf_function_preserves_ros:
+      forall f tf pc rs trs ros args res fd pc' sig
+        (FUN : transf_function gen_injections f = OK tf)
+        (MATCH : match_regs f rs trs)
+        (INSTR : (fn_code f) ! pc = Some (Icall sig ros args res pc'))
+        (FIND : find_function ge ros rs = Some fd),
+      exists tfd, find_function tge ros trs = Some tfd
+                  /\ transf_fundef gen_injections fd = OK tfd.
+    Proof.
+      intros; destruct ros as  [r|id].
+      - apply functions_translated; auto.
+        replace (trs # r) with (hd Vundef (trs ## (instr_uses (Icall sig (inl r) args res pc')))) by reflexivity.
+        rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+      - simpl. rewrite symbols_preserved.
+        simpl in FIND.
+        destruct (Genv.find_symbol ge id); try congruence.
+        eapply function_ptr_translated; eauto.
+    Qed.
+
+    Lemma transf_function_preserves_ros_tail:
+      forall f tf pc rs trs ros args fd sig
+        (FUN : transf_function gen_injections f = OK tf)
+        (MATCH : match_regs f rs trs)
+        (INSTR : (fn_code f) ! pc = Some (Itailcall sig ros args))
+        (FIND : find_function ge ros rs = Some fd),
+      exists tfd, find_function tge ros trs = Some tfd
+                  /\ transf_fundef gen_injections fd = OK tfd.
+    Proof.
+      intros; destruct ros as  [r|id].
+      - apply functions_translated; auto.
+        replace (trs # r) with (hd Vundef (trs ## (instr_uses (Itailcall sig (inl r) args)))) by reflexivity.
+        rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+      - simpl. rewrite symbols_preserved.
+        simpl in FIND.
+        destruct (Genv.find_symbol ge id); try congruence.
+        eapply function_ptr_translated; eauto.
+    Qed.
+      
+    Theorem transf_step_correct:
+      forall s1 t s2, step ge s1 t s2 ->
+         forall ts1 (MS: match_states s1 ts1),
+         exists ts2, Smallstep.plus step tge ts1 t ts2 /\ match_states s2 ts2.
+    Proof.
+      induction 1; intros ts1 MS; inv MS; try (inv TRC).
+      - (* nop *)
+        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + exploit transf_function_redirects; eauto.
+          { eapply max_pc_function_sound; eauto. }
+          intros [pc_inj [ALTER SKIP]].
+          specialize SKIP with (ts := ts) (sp := sp) (m := m) (trs := trs).
+          destruct SKIP as [trs' [MATCH PLUS]].
+          econstructor; split.
+          * eapply Smallstep.plus_left.
+            ** apply exec_Inop.
+               exact ALTER.
+            ** apply Smallstep.plus_star.
+               exact PLUS.
+            ** reflexivity.
+          * constructor; trivial.
+            apply match_regs_trans with (rs2 := trs); assumption.
+        + econstructor; split.
+          * apply Smallstep.plus_one.
+            apply exec_Inop.
+            rewrite transf_function_preserves with (f:=f); eauto.
+            eapply max_pc_function_sound; eauto.
+          * constructor; trivial.
+            
+      - (* op *)
+        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + exploit transf_function_redirects; eauto.
+          { eapply max_pc_function_sound; eauto. }
+          intros [pc_inj [ALTER SKIP]].
+          specialize SKIP with (ts := ts) (sp := sp) (m := m)
+             (trs := trs # res <- v).
+          destruct SKIP as [trs' [MATCH PLUS]].
+          econstructor; split.
+          * eapply Smallstep.plus_left.
+            ** apply exec_Iop with (op := op) (args := args).
+               exact ALTER.
+               rewrite eval_operation_preserved with (ge1 := ge).
+               {
+                 replace args with (instr_uses (Iop op args res pc')) by reflexivity.
+                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+                 simpl.
+                 eassumption.
+               }
+               exact symbols_preserved.
+            ** apply Smallstep.plus_star.
+               exact PLUS.
+            ** reflexivity.
+          * constructor; trivial.
+            apply match_regs_trans with (rs2 := trs # res <- v); trivial.
+            apply match_regs_write.
+            assumption.
+        + econstructor; split.
+          * apply Smallstep.plus_one.
+            apply exec_Iop with (op := op) (args := args).
+            ** rewrite transf_function_preserves with (f:=f); eauto.
+               eapply max_pc_function_sound; eauto.
+            ** rewrite eval_operation_preserved with (ge1 := ge).
+               {
+                 replace args with (instr_uses (Iop op args res pc')) by reflexivity.
+                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+                 simpl.
+                 eassumption.
+               }
+               exact symbols_preserved.
+          * constructor; trivial.
+            apply match_regs_write.
+            assumption.
+
+      - (* load *)
+        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + exploit transf_function_redirects; eauto.
+          { eapply max_pc_function_sound; eauto. }
+          intros [pc_inj [ALTER SKIP]].
+          specialize SKIP with (ts := ts) (sp := sp) (m := m)
+             (trs := trs # dst <- v).
+          destruct SKIP as [trs' [MATCH PLUS]].
+          econstructor; split.
+          * eapply Smallstep.plus_left.
+            ** apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args) (a := a).
+               exact ALTER.
+               rewrite eval_addressing_preserved with (ge1 := ge).
+               {
+                 replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity.
+                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               }
+               exact symbols_preserved.
+               eassumption.
+            ** apply Smallstep.plus_star.
+               exact PLUS.
+            ** reflexivity.
+          * constructor; trivial.
+            apply match_regs_trans with (rs2 := trs # dst <- v); trivial.
+            apply match_regs_write.
+            assumption.
+        + econstructor; split.
+          * apply Smallstep.plus_one.
+            apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args) (a := a).
+            ** rewrite transf_function_preserves with (f:=f); eauto.
+               eapply max_pc_function_sound; eauto.
+            ** rewrite eval_addressing_preserved with (ge1 := ge).
+               {
+                 replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity.
+                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               }
+               exact symbols_preserved.
+            ** eassumption.
+          * constructor; trivial.
+            apply match_regs_write.
+            assumption.
+        
+      - (* load notrap1 *)
+        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + exploit transf_function_redirects; eauto.
+          { eapply max_pc_function_sound; eauto. }
+          intros [pc_inj [ALTER SKIP]].
+          specialize SKIP with (ts := ts) (sp := sp) (m := m)
+             (trs := trs # dst <- Vundef).
+          destruct SKIP as [trs' [MATCH PLUS]].
+          econstructor; split.
+          * eapply Smallstep.plus_left.
+            ** apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args).
+               exact ALTER.
+               rewrite eval_addressing_preserved with (ge1 := ge).
+               {
+                 replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
+                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               }
+               exact symbols_preserved.
+            ** apply Smallstep.plus_star.
+               exact PLUS.
+            ** reflexivity.
+          * constructor; trivial.
+            apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial.
+            apply match_regs_write.
+            assumption.
+        + econstructor; split.
+          * apply Smallstep.plus_one.
+            apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args).
+            ** rewrite transf_function_preserves with (f:=f); eauto.
+               eapply max_pc_function_sound; eauto.
+            ** rewrite eval_addressing_preserved with (ge1 := ge).
+               {
+                 replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
+                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               }
+               exact symbols_preserved.
+          * constructor; trivial.
+            apply match_regs_write.
+            assumption.
+
+      - (* load notrap2 *)
+        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + exploit transf_function_redirects; eauto.
+          { eapply max_pc_function_sound; eauto. }
+          intros [pc_inj [ALTER SKIP]].
+          specialize SKIP with (ts := ts) (sp := sp) (m := m)
+             (trs := trs # dst <- Vundef).
+          destruct SKIP as [trs' [MATCH PLUS]].
+          econstructor; split.
+          * eapply Smallstep.plus_left.
+            ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (a := a).
+               exact ALTER.
+               rewrite eval_addressing_preserved with (ge1 := ge).
+               {
+                 replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
+                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               }
+               exact symbols_preserved.
+               eassumption.
+            ** apply Smallstep.plus_star.
+               exact PLUS.
+            ** reflexivity.
+          * constructor; trivial.
+            apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial.
+            apply match_regs_write.
+            assumption.
+        + econstructor; split.
+          * apply Smallstep.plus_one.
+            apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (a := a).
+            ** rewrite transf_function_preserves with (f:=f); eauto.
+               eapply max_pc_function_sound; eauto.
+            ** rewrite eval_addressing_preserved with (ge1 := ge).
+               {
+                 replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
+                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               }
+               exact symbols_preserved.
+            ** eassumption.
+          * constructor; trivial.
+            apply match_regs_write.
+            assumption.
+        
+      - (* store *)
+        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + exploit transf_function_redirects; eauto.
+          { eapply max_pc_function_sound; eauto. }
+          intros [pc_inj [ALTER SKIP]].
+          specialize SKIP with (ts := ts) (sp := sp) (m := m') (trs := trs).
+          destruct SKIP as [trs' [MATCH PLUS]].
+          econstructor; split.
+          * eapply Smallstep.plus_left.
+            ** apply exec_Istore with (chunk := chunk) (addr := addr) (args := args) (a := a) (src := src).
+               exact ALTER.
+               rewrite eval_addressing_preserved with (ge1 := ge).
+               {
+                 replace (trs ## args) with (tl (trs ## (instr_uses (Istore chunk addr args src pc')))) by reflexivity.
+                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               }
+               exact symbols_preserved.
+               replace (trs # src) with (hd Vundef (trs ## (instr_uses (Istore chunk addr args src pc')))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               simpl.
+               eassumption.
+            ** apply Smallstep.plus_star.
+               exact PLUS.
+            ** reflexivity.
+          * constructor; trivial.
+            apply match_regs_trans with (rs2 := trs); trivial.
+        + econstructor; split.
+          * apply Smallstep.plus_one.
+            apply exec_Istore with (chunk := chunk) (addr := addr) (args := args) (a := a) (src := src).
+            ** rewrite transf_function_preserves with (f:=f); eauto.
+               eapply max_pc_function_sound; eauto.
+            ** rewrite eval_addressing_preserved with (ge1 := ge).
+               {
+                 replace (trs ## args) with (tl (trs ## (instr_uses (Istore chunk addr args src pc')))) by reflexivity.
+                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               }
+               exact symbols_preserved.
+            ** replace (trs # src) with (hd Vundef (trs ## (instr_uses (Istore chunk addr args src pc')))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               simpl.
+               eassumption.
+          * constructor; trivial.
+      - (* call *)
+        destruct (transf_function_preserves_ros f tf pc rs trs ros args res fd pc' (funsig fd) FUN REGS H H0) as [tfd [TFD1 TFD2]].
+        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + exploit transf_function_redirects; eauto.
+          { eapply max_pc_function_sound; eauto. }
+          intros [pc_inj [ALTER SKIP]].
+          simpl in ALTER.
+          econstructor; split.
+          * eapply Smallstep.plus_one.
+            apply exec_Icall with (args := args) (sig := (funsig fd)) (ros := ros).
+            exact ALTER.
+            exact TFD1.
+            apply sig_preserved; auto.
+          * destruct ros as [r | id].
+            ** replace (trs ## args) with (tl (trs ## (instr_uses (Icall (funsig fd) (inl r) args res pc')))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               apply match_states_call; auto.
+               constructor; auto.
+               constructor; auto.
+
+               intros.
+               destruct (SKIP ts0 sp m0 trs1) as [trs2 [MATCH PLUS]].
+               exists trs2. split. assumption.
+               apply Smallstep.plus_star. exact PLUS.
+               
+            ** replace (trs ## args) with (trs ## (instr_uses (Icall (funsig fd) (inr id) args res pc'))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               apply match_states_call; auto.
+               constructor; auto.
+               constructor; auto.
+
+               intros.
+               destruct (SKIP ts0 sp m0 trs1) as [trs2 [MATCH PLUS]].
+               exists trs2. split. assumption.
+               apply Smallstep.plus_star. exact PLUS.
+               
+        + econstructor; split.
+          * eapply Smallstep.plus_one.
+            apply exec_Icall with (args := args) (sig := (funsig fd)) (ros := ros).
+            ** rewrite transf_function_preserves with (f:=f); eauto.
+               eapply max_pc_function_sound; eauto.
+            ** exact TFD1.
+            ** apply sig_preserved; auto.
+          * destruct ros as [r | id].
+            ** replace (trs ## args) with (tl (trs ## (instr_uses (Icall (funsig fd) (inl r) args res pc')))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               apply match_states_call; auto.
+               constructor; auto.
+               constructor; auto.
+
+               intros. exists trs1. split.
+               apply match_regs_refl. constructor.
+               
+            ** replace (trs ## args) with (trs ## (instr_uses (Icall (funsig fd) (inr id) args res pc'))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               apply match_states_call; auto.
+               constructor; auto.
+               constructor; auto.
+
+               intros. exists trs1. split.
+               apply match_regs_refl. constructor.
+        
+      -  (* tailcall *)
+        destruct (transf_function_preserves_ros_tail f tf pc rs trs ros args fd (funsig fd) FUN REGS H H0) as [tfd [TFD1 TFD2]].
+        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + exploit transf_function_redirects; eauto.
+          { eapply max_pc_function_sound; eauto. }
+          intros [pc_inj [ALTER SKIP]].
+          simpl in ALTER.
+          econstructor; split.
+          * eapply Smallstep.plus_one.
+            apply exec_Itailcall with (args := args) (sig := (funsig fd)) (ros := ros).
+            exact ALTER.
+            exact TFD1.
+            apply sig_preserved; auto.
+            rewrite stacksize_preserved with (f:=f) by trivial.
+            eassumption.
+          * destruct ros as [r | id].
+            ** replace (trs ## args) with (tl (trs ## (instr_uses (Itailcall (funsig fd) (inl r) args)))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               apply match_states_call; auto.
+            ** replace (trs ## args) with (trs ## (instr_uses (Itailcall (funsig fd) (inr id) args))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               apply match_states_call; auto.
+        + econstructor; split.
+          * eapply Smallstep.plus_one.
+            apply exec_Itailcall with (args := args) (sig := (funsig fd)) (ros := ros).
+            ** rewrite transf_function_preserves with (f:=f); eauto.
+               eapply max_pc_function_sound; eauto.
+            ** exact TFD1.
+            ** apply sig_preserved; auto.
+            ** rewrite stacksize_preserved with (f:=f) by trivial.
+               eassumption.
+          * destruct ros as [r | id].
+            ** replace (trs ## args) with (tl (trs ## (instr_uses (Itailcall (funsig fd) (inl r) args)))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               apply match_states_call; auto.
+            ** replace (trs ## args) with (trs ## (instr_uses (Itailcall (funsig fd) (inr id) args))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               apply match_states_call; auto.
+
+      - (* builtin *)
+        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + exploit transf_function_redirects; eauto.
+          { eapply max_pc_function_sound; eauto. }
+          intros [pc_inj [ALTER SKIP]].
+          specialize SKIP with (ts := ts) (sp := sp) (m := m')
+             (trs := (regmap_setres res vres trs)).
+          destruct SKIP as [trs' [MATCH PLUS]].
+          econstructor; split.
+          * eapply Smallstep.plus_left.
+            ** apply exec_Ibuiltin with (ef := ef) (args := args) (res := res) (vargs := vargs).
+               *** exact ALTER.
+               *** apply eval_builtin_args_preserved with (ge1 := ge); eauto.
+                   exact symbols_preserved.
+                   apply transf_function_preserves_builtin_args with (f:=f) (tf:=tf) (pc:=pc) (rs:=rs) (ef:=ef) (res0:=res) (pc':=pc'); auto.
+               *** eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+            ** apply Smallstep.plus_star.
+               exact PLUS.
+            ** symmetry. apply E0_right.
+          * constructor; trivial.
+            apply match_regs_trans with (rs2 := (regmap_setres res vres trs)); trivial.
+            apply match_regs_setres.
+            assumption.
+        + econstructor; split.
+          * eapply Smallstep.plus_one.
+            apply exec_Ibuiltin with (ef := ef) (args := args) (res := res) (vargs := vargs).
+            ** rewrite transf_function_preserves with (f:=f); eauto.
+               eapply max_pc_function_sound; eauto.
+            ** apply eval_builtin_args_preserved with (ge1 := ge); eauto.
+               exact symbols_preserved.
+               apply transf_function_preserves_builtin_args with (f:=f) (tf:=tf) (pc:=pc) (rs:=rs) (ef:=ef) (res0:=res) (pc':=pc'); auto.
+            ** eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+          * constructor; auto.
+            apply match_regs_setres.
+            assumption.
+            
+      - (* cond *)
+        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + destruct b eqn:B.
+          ++ exploit transf_function_redirects; eauto.
+             { eapply max_pc_function_sound; eauto. }
+             intros [pc_inj [ALTER SKIP]].
+             specialize SKIP with (ts := ts) (sp := sp) (m := m) (trs := trs).
+             destruct SKIP as [trs' [MATCH PLUS]].
+             econstructor; split.
+             * eapply Smallstep.plus_left.
+               ** apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot) (predb := predb).
+                   exact ALTER.
+                   replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity.
+                   rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+                   simpl. reflexivity.
+               ** apply Smallstep.plus_star.
+                  exact PLUS.
+               ** reflexivity.
+             * simpl. constructor; auto.
+               apply match_regs_trans with (rs2:=trs); auto.
+
+          ++ exploit transf_function_redirects; eauto.
+             { eapply max_pc_function_sound; eauto. }
+             intros [pc_inj [ALTER SKIP]].
+             specialize SKIP with (ts := ts) (sp := sp) (m := m) (trs := trs).
+             destruct SKIP as [trs' [MATCH PLUS]].
+             econstructor; split.
+             * eapply Smallstep.plus_one.
+               apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot) (predb := predb).
+               exact ALTER.
+               replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               simpl. reflexivity.
+             * simpl. constructor; auto.
+        + destruct b eqn:B.
+          * econstructor; split.
+            ** eapply Smallstep.plus_one.
+               apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot) (predb := predb).
+               *** rewrite transf_function_preserves with (f:=f); eauto.
+                   eapply max_pc_function_sound; eauto.
+               *** replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity.
+                   rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               *** reflexivity.
+            ** constructor; auto.
+          *  econstructor; split.
+            ** eapply Smallstep.plus_one.
+               apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot) (predb := predb).
+               *** rewrite transf_function_preserves with (f:=f); eauto.
+                   eapply max_pc_function_sound; eauto.
+               *** replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity.
+                   rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               *** reflexivity.
+            ** constructor; auto.
+                       
+      - destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + exploit transf_function_redirects; eauto.
+          { eapply max_pc_function_sound; eauto. }
+          intros [pc_inj [ALTER SKIP]].
+          specialize SKIP with (ts := ts) (sp := sp) (m := m) (trs := trs).
+          destruct SKIP as [trs' [MATCH PLUS]].
+          econstructor; split.
+          * apply Smallstep.plus_one.
+            apply exec_Ijumptable with (arg := arg) (tbl := tbl) (n := n); trivial.
+            replace (trs # arg) with (hd Vundef (trs ## (instr_uses (Ijumptable arg tbl)))) by reflexivity.
+            rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+            eassumption.
+          * constructor; trivial.
+        + econstructor; split.
+          * apply Smallstep.plus_one.
+            apply exec_Ijumptable with (arg := arg) (tbl := tbl) (n := n); trivial.
+            rewrite transf_function_preserves with (f:=f); eauto.
+            eapply max_pc_function_sound; eauto.
+            replace (trs # arg) with (hd Vundef (trs ## (instr_uses (Ijumptable arg tbl)))) by reflexivity.
+            rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+            eassumption.
+          * constructor; trivial.
+      - (* return *)
+         destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+        + exploit transf_function_redirects; eauto.
+          { eapply max_pc_function_sound; eauto. }
+          intros [pc_inj [ALTER SKIP]].
+          specialize SKIP with (ts := ts) (sp := (Vptr stk Ptrofs.zero)) (m := m) (trs := trs).
+          destruct SKIP as [trs' [MATCH PLUS]].
+          econstructor; split.
+          * apply Smallstep.plus_one.
+            apply exec_Ireturn.
+            exact ALTER.
+            rewrite stacksize_preserved with (f:=f); eassumption.
+          * destruct or as [r | ]; simpl.
+            ** replace (trs # r) with (hd Vundef (trs ## (instr_uses (Ireturn (Some r))))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               constructor; auto.
+            ** constructor; auto.
+        + econstructor; split.
+          * apply Smallstep.plus_one.
+            apply exec_Ireturn.
+            rewrite transf_function_preserves with (f:=f); eauto.
+            eapply max_pc_function_sound; eauto.
+            rewrite stacksize_preserved with (f:=f); eassumption.
+          * destruct or as [r | ]; simpl.
+            ** replace (trs # r) with (hd Vundef (trs ## (instr_uses (Ireturn (Some r))))) by reflexivity.
+               rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+               constructor; auto.
+            ** constructor; auto.
+
+      - (* internal call *)
+        monadInv FUN.
+        econstructor; split.
+        + apply Smallstep.plus_one.
+          apply exec_function_internal.
+          rewrite stacksize_preserved with (f:=f) by assumption.
+          eassumption.
+        + rewrite entrypoint_preserved with (f:=f)(tf:=x) by assumption.
+          constructor; auto.
+          rewrite params_preserved with (f:=f)(tf:=x) by assumption.
+          apply match_regs_refl.
+      - (* external call *)
+        monadInv FUN.
+        econstructor; split.
+        + apply Smallstep.plus_one.
+          apply exec_function_external.
+          eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+        + constructor; auto.
+        
+      - (* return *)
+        inv STACKS. inv H1.
+        destruct (STAR bl m (trs # res <- vres)) as [trs2 [MATCH' STAR']].
+        econstructor; split.
+        + eapply Smallstep.plus_left.
+          * apply exec_return.
+          * exact STAR'.
+          * reflexivity.
+        + constructor; trivial.
+          apply match_regs_trans with (rs2 := (trs # res <- vres)).
+          apply match_regs_write.
+          assumption.
+          assumption.
+    Qed.
+
+    Theorem transf_program_correct:
+      Smallstep.forward_simulation (semantics prog) (semantics tprog).
+    Proof.
+      eapply Smallstep.forward_simulation_plus.
+      apply senv_preserved.
+      eexact transf_initial_states.
+      eexact transf_final_states.
+      eexact transf_step_correct.
+    Qed.
+    
+End PRESERVATION.
+End INJECTOR.
diff --git a/backend/LICM.v b/backend/LICM.v
new file mode 100644
index 00000000..0a0a1c7d
--- /dev/null
+++ b/backend/LICM.v
@@ -0,0 +1,9 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL.
+Require Inject.
+
+Axiom gen_injections : function -> node -> reg -> PTree.t (list Inject.inj_instr).
+
+Definition transf_program : program -> res program :=
+  Inject.transf_program gen_injections.
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml
new file mode 100644
index 00000000..4ebc7844
--- /dev/null
+++ b/backend/LICMaux.ml
@@ -0,0 +1,252 @@
+open RTL;;
+open Camlcoq;;
+open Maps;;
+open Kildall;;
+open HashedSet;;
+open Inject;;
+
+type reg = P.t;;
+
+module Dominator =
+  struct
+    type t = Unreachable | Dominated of int | Multiple
+    let bot = Unreachable and top = Multiple
+    let beq a b =
+      match a, b with
+      | Unreachable, Unreachable
+      | Multiple, Multiple -> true
+      | (Dominated x), (Dominated y) -> x = y
+      | _ -> false
+    let lub a b =
+      match a, b with
+      | Multiple, _
+      | _, Multiple -> Multiple
+      | Unreachable, x
+      | x, Unreachable -> x
+      | (Dominated x), (Dominated y) when x=y -> a
+      | (Dominated _), (Dominated _) -> Multiple
+
+    let pp oc = function
+      | Unreachable -> output_string oc "unreachable"
+      | Multiple -> output_string oc "multiple"
+      | Dominated x -> Printf.fprintf oc "%d" x;;
+  end
+
+module Dominator_Solver = Dataflow_Solver(Dominator)(NodeSetForward)
+
+let apply_dominator (is_marked : node -> bool) (pc : node)
+      (before : Dominator.t) : Dominator.t =
+  match before with
+  | Dominator.Unreachable -> before
+  | _ ->
+     if is_marked pc
+     then Dominator.Dominated (P.to_int pc)
+     else before;;
+
+let dominated_parts1 (f : coq_function) :
+      (bool PTree.t) * (Dominator.t PMap.t option) =
+  let headers = Duplicateaux.get_loop_headers f.fn_code f.fn_entrypoint in
+  let dominated = Dominator_Solver.fixpoint f.fn_code RTL.successors_instr
+    (apply_dominator (fun pc -> match PTree.get pc headers with
+                                | Some x -> x
+                                | None -> false)) f.fn_entrypoint
+    Dominator.top in
+  (headers, dominated);;
+
+let dominated_parts (f : coq_function) : Dominator.t PMap.t * PSet.t PTree.t =
+  let (headers, dominated) = dominated_parts1 f in
+  match dominated with
+  | None -> failwith "dominated_parts 1"
+  | Some dominated ->
+     let singletons =
+       PTree.fold (fun before pc flag ->
+         if flag
+         then PTree.set pc (PSet.add pc PSet.empty) before
+         else before) headers PTree.empty in
+     (dominated,
+     PTree.fold (fun before pc ii ->
+         match PMap.get pc dominated with
+         | Dominator.Dominated x ->
+            let px = P.of_int x in
+            (match PTree.get px before with
+             | None -> failwith "dominated_parts 2"
+             | Some old ->
+                PTree.set px (PSet.add pc old) before)
+         | _ -> before) f.fn_code singletons);;
+
+let graph_traversal (initial_node : P.t)
+  (successor_iterator : P.t -> (P.t -> unit) -> unit) : PSet.t =
+  let seen = ref PSet.empty
+  and stack = Stack.create () in
+  Stack.push initial_node stack;
+  while not (Stack.is_empty stack)
+  do
+    let vertex = Stack.pop stack in
+    if not (PSet.contains !seen vertex)
+    then
+      begin
+        seen := PSet.add vertex !seen;
+        successor_iterator vertex (fun x -> Stack.push x stack) 
+      end
+  done;
+  !seen;;
+
+let filter_dominated_part (predecessors : P.t list PTree.t)
+      (header : P.t) (dominated_part : PSet.t) =
+  graph_traversal header
+    (fun (vertex : P.t) (f : P.t -> unit) ->
+      match PTree.get vertex predecessors with
+      | None -> ()
+      | Some l ->
+         List.iter
+           (fun x ->
+             if PSet.contains dominated_part x
+             then f x) l
+    );;
+
+let inner_loops (f : coq_function) =
+  let (dominated, parts) = dominated_parts f
+  and predecessors = Kildall.make_predecessors f.fn_code RTL.successors_instr in
+  (dominated, predecessors, PTree.map (filter_dominated_part predecessors) parts);;
+
+let map_reg mapper r =
+  match PTree.get r mapper with
+  | None -> r
+  | Some x -> x;;
+
+let rewrite_loop_body (last_alloc : reg ref)
+      (insns : RTL.code) (header : P.t) (loop_body : PSet.t) =
+  let seen = ref PSet.empty
+  and stack = Stack.create ()
+  and rewritten = ref [] in
+  let add_inj ii = rewritten := ii::!rewritten in
+  Stack.push (header, PTree.empty) stack;
+  while not (Stack.is_empty stack)
+  do
+    let (pc, mapper) = Stack.pop stack in
+    if not (PSet.contains !seen pc)
+    then
+      begin
+        seen := PSet.add pc !seen;
+        match PTree.get pc insns with
+        | None -> ()
+        | Some ii ->
+           let mapper' =
+             match ii with
+             | Iop(op, args, res, pc') when not (Op.is_trapping_op op) ->
+                let new_res = P.succ !last_alloc in
+                last_alloc := new_res;
+                add_inj (INJop(op,
+                               (List.map (map_reg mapper) args),
+                               new_res));
+                PTree.set res new_res mapper
+             | Iload(trap, chunk, addr, args, res, pc')
+                  when Archi.has_notrap_loads &&
+                       !Clflags.option_fnontrap_loads ->
+                let new_res = P.succ !last_alloc in
+                last_alloc := new_res;
+                add_inj (INJload(chunk, addr,
+                                 (List.map (map_reg mapper) args),
+                                 new_res));
+                PTree.set res new_res mapper
+             | _ -> mapper in
+           List.iter (fun x ->
+               if PSet.contains loop_body x
+               then Stack.push (x, mapper') stack)
+             (successors_instr ii)
+      end
+  done;
+  List.rev !rewritten;;
+
+let pp_inj_instr (oc : out_channel) (ii : inj_instr) =
+  match ii with
+  | INJnop -> output_string oc "nop"
+  | INJop(op, args, res) ->
+     Printf.fprintf oc "%a = %a"
+       PrintRTL.reg res (PrintOp.print_operation PrintRTL.reg) (op, args)
+  | INJload(chunk, addr, args, dst) ->
+     Printf.fprintf oc "%a = %s[%a]"
+       PrintRTL.reg dst (PrintAST.name_of_chunk chunk)
+         (PrintOp.print_addressing PrintRTL.reg) (addr, args);;
+
+let pp_inj_list (oc : out_channel) (l : inj_instr list) =
+  List.iter (Printf.fprintf oc "%a; " pp_inj_instr) l;;
+
+let pp_injections (oc : out_channel) (injections : inj_instr list PTree.t) =
+  List.iter
+    (fun (pc, injl) ->
+      Printf.fprintf oc "%d : %a\n" (P.to_int pc) pp_inj_list injl)
+    (PTree.elements injections);;
+
+let compute_injections1 (f : coq_function) =
+  let (dominated, predecessors, loop_bodies) = inner_loops f
+  and last_alloc = ref (max_reg_function f) in
+  (dominated, predecessors,
+   PTree.map (fun header body ->
+    (body, rewrite_loop_body last_alloc f.fn_code header body)) loop_bodies);;
+
+let compute_injections (f : coq_function) : inj_instr list PTree.t =
+  let (dominated, predecessors, injections) = compute_injections1 f in
+  let output_map = ref PTree.empty in
+  List.iter
+    (fun (header, (body, inj)) ->
+      match PTree.get header predecessors with
+      | None -> failwith "compute_injections"
+      | Some l ->
+         List.iter (fun predecessor ->
+             if (PMap.get predecessor dominated)<>Dominator.Unreachable &&
+                  not (PSet.contains body predecessor)
+             then output_map := PTree.set predecessor inj !output_map) l)
+    (PTree.elements injections);
+  !output_map;;
+  
+let pp_list pp_item oc l =
+  output_string oc "{ ";
+  let first = ref true in
+  List.iter (fun x ->
+      (if !first
+       then first := false
+       else output_string oc ", ");
+      pp_item oc x) l;
+  output_string oc " }";;
+
+let pp_pset oc s =
+  pp_list (fun oc -> Printf.fprintf oc "%d") oc
+    (List.sort (fun x y -> y - x) (List.map P.to_int (PSet.elements s)));;
+
+let print_dominated_parts oc f =
+  List.iter (fun (header, nodes) ->
+      Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes)
+    (PTree.elements (snd (dominated_parts f)));;
+
+let print_inner_loops oc f =
+  List.iter (fun (header, nodes) ->
+      Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes)
+    (PTree.elements (let (_,_,l) = (inner_loops f) in l));;
+
+let print_dominated_parts1 oc f =
+  match snd (dominated_parts1 f) with
+  | None -> output_string oc "error\n"
+  | Some parts ->
+     List.iter
+       (fun (pc, instr) ->
+         Printf.fprintf oc "%d : %a\n" (P.to_int pc) Dominator.pp
+           (PMap.get pc parts)
+       )
+       (PTree.elements f.fn_code);;
+  
+let loop_headers (f : coq_function) : RTL.node list =
+  List.map fst (List.filter snd (PTree.elements (Duplicateaux.get_loop_headers f.fn_code f.fn_entrypoint)));;
+
+let print_loop_headers f =
+  print_endline "Loop headers";
+  List.iter
+    (fun i -> Printf.printf "%d " (P.to_int i))
+    (loop_headers f);
+  print_newline ();;
+
+let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg):
+      (Inject.inj_instr list) PTree.t =
+  let injections = compute_injections f in
+  (* let () = pp_injections stdout injections in *)
+  injections;;
diff --git a/backend/LICMproof.v b/backend/LICMproof.v
new file mode 100644
index 00000000..2b76b668
--- /dev/null
+++ b/backend/LICMproof.v
@@ -0,0 +1,27 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL.
+Require Import LICM.
+Require Injectproof.
+
+Definition match_prog : program -> program -> Prop :=
+  Injectproof.match_prog gen_injections.
+
+Section PRESERVATION.
+
+  Variables prog tprog: program.
+  Hypothesis TRANSF: match_prog prog tprog.
+
+  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.
+  
+  Theorem transf_program_correct :
+    Smallstep.forward_simulation (semantics prog) (semantics tprog).
+  Proof.
+    apply Injectproof.transf_program_correct with (gen_injections := gen_injections).
+    exact TRANSF.
+  Qed.
+End PRESERVATION.
diff --git a/configure b/configure
index cb2f52ba..366ab847 100755
--- a/configure
+++ b/configure
@@ -575,7 +575,7 @@ case "$coq_ver" in
         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.11.0, 8.10.2, 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0"
+            echo "Error: CompCert requires one of the following Coq versions: 8.11.1, 8.11.0, 8.10.2, 8.10.1, 8.10.0, 8.9.1, 8.9.0"
             missingtools=true
         fi;;
   "")
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 558e1d09..fd9603ee 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -79,9 +79,12 @@ let use_standard_headers =  ref Configuration.has_standard_headers
 let option_fglobaladdrtmp = ref false
 let option_fglobaladdroffset = ref false
 let option_fxsaddr = ref true  
-let option_faddx = ref false  
+let option_faddx = ref false
+let option_fmadd = ref true
 let option_fcoalesce_mem = ref true
 let option_fforward_moves = ref true
+let option_fmove_loop_invariants = ref true
+let option_fnontrap_loads = ref true
 let option_all_loads_nontrap = ref false
 let option_inline_auto_threshold = ref 0
 
diff --git a/driver/Compiler.v b/driver/Compiler.v
index ee091c37..69041ab0 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -39,9 +39,11 @@ Require Tailcall.
 Require Inlining.
 Require Profiling.
 Require ProfilingExploit.
+Require FirstNop.
 Require Renumber.
 Require Duplicate.
 Require Constprop.
+Require LICM.
 Require CSE.
 Require ForwardMoves.
 Require CSE2.
@@ -67,9 +69,11 @@ Require Tailcallproof.
 Require Inliningproof.
 Require Profilingproof.
 Require ProfilingExploitproof.
+Require FirstNopproof.
 Require Renumberproof.
 Require Duplicateproof.
 Require Constpropproof.
+Require LICMproof.
 Require CSEproof.
 Require ForwardMovesproof.
 Require CSE2proof.
@@ -142,28 +146,34 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    @@ print (print_RTL 3)
    @@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program)
    @@ print (print_RTL 4)
-   @@ time "Renumbering" Renumber.transf_program
+   @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program)
    @@ print (print_RTL 5)
-  @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program)
+   @@ time "Renumbering" Renumber.transf_program
    @@ print (print_RTL 6)
-   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
+  @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program)
    @@ print (print_RTL 7)
-   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
+   @@ time "Renumbering pre constprop" Renumber.transf_program
    @@ print (print_RTL 8)
-  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
+   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
    @@ print (print_RTL 9)
-   @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program)
+  @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program)
    @@ print (print_RTL 10)
-  @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program)
+   @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program)
    @@ print (print_RTL 11)
-   @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
+  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
    @@ print (print_RTL 12)
-  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+   @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program)
    @@ print (print_RTL 13)
-   @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
+  @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program)
    @@ print (print_RTL 14)
-  @@@ time "Unused globals" Unusedglob.transform_program
+   @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
    @@ print (print_RTL 15)
+  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+   @@ print (print_RTL 16)
+   @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
+   @@ print (print_RTL 17)
+  @@@ time "Unused globals" Unusedglob.transform_program
+   @@ print (print_RTL 18)
   @@@ time "Register allocation" Allocation.transf_program
    @@ print print_LTL
    @@ time "Branch tunneling" Tunneling.tunnel_program
@@ -267,10 +277,13 @@ Definition CompCert's_passes :=
   ::: mkpass Inliningproof.match_prog
   ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog)
   ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog)
+  ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog)
   ::: mkpass Renumberproof.match_prog
   ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog)
+  ::: mkpass Renumberproof.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_move_loop_invariants LICMproof.match_prog)
+  ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog)
   ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog)
   ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog)
   ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog)
@@ -317,11 +330,14 @@ Proof.
   destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate.
   set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *.
   set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *.
-  set (p9 := Renumber.transf_program p8ter) in *.
-  destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate.
-  set (p11 := total_if optim_constprop Constprop.transf_program p10) in *.
-  set (p12 := total_if optim_constprop Renumber.transf_program p11) in *.
-  destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
+  set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *.
+  set (p9bis := Renumber.transf_program p9) in *.
+  destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate.
+  set (p11 := Renumber.transf_program p10) in *.
+  set (p12 := total_if optim_constprop Constprop.transf_program p11) in *.
+  destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate.
+  set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *.
+  destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate.
   set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *.
   destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate.
   set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *.
@@ -345,10 +361,13 @@ Proof.
   exists p8; split. apply Inliningproof.transf_program_match; auto.
   exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto.
   exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto.
-  exists p9; split. apply Renumberproof.transf_program_match; auto.
+  exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match.
+  exists p9bis; split. apply Renumberproof.transf_program_match.
   exists p10; split. eapply partial_if_match; eauto. 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 p11; split. apply Renumberproof.transf_program_match.
+  exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match.
+  exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match.
+  exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match.
   exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match.
   exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match.
   exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match.
@@ -413,7 +432,7 @@ Ltac DestructM :=
       destruct H as (p & M & MM); clear H
   end.
   repeat DestructM. subst tp.
-  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p28)).
+  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p31)).
   {
   eapply compose_forward_simulations.
     eapply SimplExprproof.transl_program_correct; eassumption.
@@ -435,11 +454,16 @@ Ltac DestructM :=
     eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct.
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct.
+  eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct.
   eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct.
   eapply compose_forward_simulations.
-    eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct.
+  eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption.
+  eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct.
+  eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct.
   eapply compose_forward_simulations.
diff --git a/driver/Compopts.v b/driver/Compopts.v
index 1e10009d..58ac62b7 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -48,6 +48,9 @@ Parameter optim_CSE3: unit -> bool.
 (** Flag -fcse3-alias-analysis.  For DMonniaux's common subexpression elimination. *)
 Parameter optim_CSE3_alias_analysis: unit -> bool.
 
+(** Flag -fmove-loop-invariants. *)
+Parameter optim_move_loop_invariants: unit -> bool.
+
 (** Flag -fredundancy.  For dead code elimination. *)
 Parameter optim_redundancy: unit -> bool.
 
@@ -66,6 +69,9 @@ Parameter optim_xsaddr: unit -> bool.
 (** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *)
 Parameter optim_coalesce_mem: unit -> bool.
 
+(* FIXME TEMPORARY Flag -faddx. Fuse (default true) *)
+Parameter optim_madd: unit -> bool.
+
 (** FIXME TEMPORARY Flag -faddx. Fuse (default false) *)
 Parameter optim_addx: unit -> bool.
 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 72715e65..3fae2a7d 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -199,6 +199,7 @@ Processing options:
   -fcse2         Perform inter-loop common subexpression elimination [off]
   -fcse3         Perform inter-loop common subexpression elimination [on]
   -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on]
+  -fmove-loop-invariants Perform loop-invariant code motion [off]
   -fredundancy   Perform redundancy elimination [on]
   -fpostpass     Perform postpass scheduling (only for K1 architecture) [on]
   -fpostpass= <optim> Perform postpass scheduling with the specified optimization [list]
@@ -405,6 +406,7 @@ let cmdline_actions =
   @ f_opt "cse2" option_fcse2
   @ f_opt "cse3" option_fcse3
   @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis
+  @ f_opt "move-loop-invariants" option_fmove_loop_invariants
   @ f_opt "redundancy" option_fredundancy
   @ f_opt "postpass" option_fpostpass
   @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ]
@@ -417,6 +419,8 @@ let cmdline_actions =
   @ f_opt "globaladdroffset" option_fglobaladdroffset
   @ f_opt "xsaddr" option_fxsaddr
   @ f_opt "addx" option_faddx
+  @ f_opt "madd" option_fmadd
+  @ f_opt "nontrap-loads" option_fnontrap_loads
   @ f_opt "coalesce-mem" option_fcoalesce_mem
   @ f_opt "all-loads-nontrap" option_all_loads_nontrap
   @ f_opt "forward-moves" option_fforward_moves
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 98eecc76..9070e26d 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -87,6 +87,9 @@ Extract Inlined Constant Inlining.inlining_info => "Inliningaux.inlining_info".
 Extract Inlined Constant Inlining.inlining_analysis => "Inliningaux.inlining_analysis".
 Extraction Inline Inlining.ret Inlining.bind.
 
+(* Loop invariant code motion *)
+Extract Inlined Constant LICM.gen_injections => "LICMaux.gen_injections".
+
 (* Allocation *)
 Extract Constant Allocation.regalloc => "Regalloc.regalloc".
 
@@ -120,6 +123,9 @@ Extract Constant Compopts.optim_CSE3 =>
   "fun _ -> !Clflags.option_fcse3".
 Extract Constant Compopts.optim_CSE3_alias_analysis =>
   "fun _ -> !Clflags.option_fcse3_alias_analysis".
+Extract Constant Compopts.optim_move_loop_invariants =>
+  "fun _ -> !Clflags.option_fmove_loop_invariants".
+
 Extract Constant Compopts.optim_redundancy =>
   "fun _ -> !Clflags.option_fredundancy".
 Extract Constant Compopts.optim_postpass =>
@@ -136,6 +142,8 @@ Extract Constant Compopts.optim_xsaddr =>
   "fun _ -> !Clflags.option_fxsaddr".
 Extract Constant Compopts.optim_addx =>
   "fun _ -> !Clflags.option_faddx".
+Extract Constant Compopts.optim_madd =>
+  "fun _ -> !Clflags.option_fmadd".
 Extract Constant Compopts.optim_coalesce_mem =>
   "fun _ -> !Clflags.option_fcoalesce_mem".
 Extract Constant Compopts.optim_forward_moves =>
@@ -230,4 +238,5 @@ Separate Extraction
    Floats.Float32.from_parsed Floats.Float.from_parsed
    Globalenvs.Senv.invert_symbol
    Parser.translation_unit_file
-   Compopts.optim_postpass.
+   Compopts.optim_postpass
+   Archi.has_notrap_loads.
diff --git a/lib/extra/HashedMap.v b/lib/extra/HashedMap.v
new file mode 100644
index 00000000..df724867
--- /dev/null
+++ b/lib/extra/HashedMap.v
@@ -0,0 +1,448 @@
+Require Import ZArith.
+Require Import Bool.
+Require Import List.
+Require Coq.Logic.Eqdep_dec.
+
+(* begin from Maps *)
+Fixpoint prev_append (i j: positive) {struct i} : positive :=
+  match i with
+  | xH => j
+  | xI i' => prev_append i' (xI j)
+  | xO i' => prev_append i' (xO j)
+  end.
+
+Definition prev (i: positive) : positive :=
+  prev_append i xH.
+
+Lemma prev_append_prev i j:
+  prev (prev_append i j) = prev_append j i.
+Proof.
+  revert j. unfold prev.
+  induction i as [i IH|i IH|]. 3: reflexivity.
+  intros j. simpl. rewrite IH. reflexivity.
+  intros j. simpl. rewrite IH. reflexivity.
+Qed.
+
+Lemma prev_involutive i :
+  prev (prev i) = i.
+Proof (prev_append_prev i xH).
+
+Lemma prev_append_inj i j j' :
+  prev_append i j = prev_append i j' -> j = j'.
+Proof.
+  revert j j'.
+  induction i as [i Hi|i Hi|]; intros j j' H; auto;
+    specialize (Hi _ _ H); congruence.
+Qed.
+
+(* end from Maps *)
+
+Lemma orb_idem: forall b, orb b b = b.
+Proof.
+  destruct b; reflexivity.
+Qed.
+
+Lemma andb_idem: forall b, andb b b = b.
+Proof.
+  destruct b; reflexivity.
+Qed.
+
+Lemma andb_negb_false: forall b, andb b (negb b) = false.
+Proof.
+  destruct b; reflexivity.
+Qed.
+
+Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem  andb_negb_false : pmap.
+
+Parameter T : Type.
+Parameter T_eq_dec : forall (x y : T), {x = y} + {x <> y}.
+
+Inductive pmap : Type :=
+| Empty : pmap
+| Node : pmap -> option T -> pmap -> pmap.
+Definition empty := Empty.
+
+Definition is_empty x :=
+  match x with
+  | Empty => true
+  | Node _ _ _ => false
+  end.
+
+Definition is_some (x : option T) :=
+  match x with
+  | Some _ => true
+  | None => false
+  end.
+
+Fixpoint wf x :=
+  match x with
+  | Empty => true
+  | Node b0 f b1 =>
+    (wf b0) && (wf b1) &&
+    ((negb (is_empty b0)) || (is_some f) || (negb (is_empty b1)))
+  end.
+
+Definition iswf x := (wf x)=true.
+  
+Lemma empty_wf : iswf empty.
+Proof.
+  reflexivity.
+Qed.
+
+Definition pmap_eq :
+  forall s s': pmap, { s=s' } + { s <> s' }.
+Proof.
+  generalize T_eq_dec.
+  induction s; destruct s'; repeat decide equality.
+Qed.
+
+Fixpoint get (i : positive) (s : pmap) {struct i} : option T :=
+  match s with
+  | Empty => None
+  | Node b0 f b1 =>
+    match i with
+    | xH => f
+    | xO ii => get ii b0
+    | xI ii => get ii b1
+    end
+  end.
+
+Lemma gempty :
+  forall i : positive,
+    get i Empty = None.
+Proof.
+  destruct i; simpl; reflexivity.
+Qed.
+
+Hint Resolve gempty : pmap.
+Hint Rewrite gempty : pmap.
+
+Definition node (b0 : pmap) (f : option T) (b1 : pmap) : pmap :=
+  match b0, f, b1 with
+  | Empty, None, Empty => Empty
+  | _, _, _ => Node b0 f b1
+  end.
+
+Lemma wf_node :
+  forall b0 f b1,
+    iswf b0 -> iswf b1 -> iswf (node b0 f b1).
+Proof.
+  destruct b0; destruct f; destruct b1; simpl.
+  all: unfold iswf; simpl; intros; trivial.
+  all: autorewrite with pmap; trivial.
+  all: rewrite H.
+  all: rewrite H0.
+  all: reflexivity.
+Qed.
+
+Hint Resolve wf_node: pmap.
+
+Lemma gnode :
+  forall b0 f b1 i,
+    get i (node b0 f b1) =
+    get i (Node b0 f b1).
+Proof.
+  destruct b0; simpl; trivial.
+  destruct f; simpl; trivial.
+  destruct b1; simpl; trivial.
+  intro.
+  rewrite gempty.
+  destruct i; simpl; trivial.
+  all: symmetry; apply gempty.
+Qed.
+
+Hint Rewrite gnode : pmap.
+
+Fixpoint set (i : positive) (j : T) (s : pmap) {struct i} : pmap :=
+  match s with
+  | Empty =>
+    match i with
+    | xH => Node Empty (Some j) Empty
+    | xO ii => Node (set ii j Empty) None Empty
+    | xI ii => Node Empty None (set ii j Empty)
+    end
+  | Node b0 f b1 =>
+    match i with
+    | xH => Node b0 (Some j) b1
+    | xO ii => Node (set ii j b0) f b1
+    | xI ii => Node b0 f (set ii j b1)
+    end
+  end.
+
+Lemma set_nonempty:
+  forall i j s, is_empty (set i j s) = false.
+Proof.
+  induction i; destruct s; simpl; trivial.
+Qed.
+
+Hint Rewrite set_nonempty : pmap.
+Hint Resolve set_nonempty : pmap.
+
+Lemma wf_set:
+  forall i j s, (iswf s) -> (iswf (set i j s)).
+Proof.
+  induction i; destruct s; simpl; trivial.
+  all: unfold iswf in *; simpl.
+  all: autorewrite with pmap; simpl; trivial.
+  1,3: auto with pmap.
+  all: intro Z.
+  all: repeat rewrite andb_true_iff in Z.
+  all: intuition.
+Qed.
+
+Hint Resolve wf_set : pset.
+
+Theorem gss :
+  forall (i : positive) (j : T) (s : pmap),
+    get i (set i j s) = Some j.
+Proof.
+  induction i; destruct s; simpl; auto.
+Qed.
+
+Hint Resolve gss : pmap.
+Hint Rewrite gss : pmap.
+
+Theorem gso :
+  forall (i j : positive) (k : T) (s : pmap),
+    i <> j ->
+    get j (set i k s) = get j s.
+Proof.
+  induction i; destruct j; destruct s; simpl; intro; auto with pmap.
+  5, 6: congruence.
+  all: rewrite IHi by congruence.
+  all: trivial.
+  all: apply gempty.
+Qed.
+
+Hint Resolve gso : pmap.
+
+Fixpoint remove (i : positive) (s : pmap) { struct i } : pmap :=
+  match i with
+  | xH =>
+    match s with
+    | Empty => Empty
+    | Node b0 f b1 => node b0 None b1
+    end
+  | xO ii =>
+    match s with
+    | Empty => Empty
+    | Node b0 f b1 => node (remove ii b0) f b1
+    end
+  | xI ii =>
+    match s with
+    | Empty => Empty
+    | Node b0 f b1 => node b0 f (remove ii b1)
+    end
+  end.
+
+Lemma wf_remove :
+  forall i s, (iswf s) -> (iswf (remove i s)).
+Proof.
+  induction i; destruct s; simpl; trivial.
+  all: unfold iswf in *; simpl.
+  all: intro Z.
+  all: repeat rewrite andb_true_iff in Z.
+  all: apply wf_node.
+  all: intuition.
+  all: apply IHi.
+  all: assumption.
+Qed.
+
+Fixpoint remove_noncanon (i : positive) (s : pmap) { struct i } : pmap :=
+  match i with
+  | xH =>
+    match s with
+    | Empty => Empty
+    | Node b0 f b1 => Node b0 None b1
+    end
+  | xO ii =>
+    match s with
+    | Empty => Empty
+    | Node b0 f b1 => Node (remove_noncanon ii b0) f b1
+    end
+  | xI ii =>
+    match s with
+    | Empty => Empty
+    | Node b0 f b1 => Node b0 f (remove_noncanon ii b1)
+    end
+  end.
+
+Lemma remove_noncanon_same:
+  forall i j s, (get j (remove i s)) = (get j (remove_noncanon i s)).
+Proof.
+  induction i; destruct s; simpl; trivial.
+  all: rewrite gnode.
+  3: reflexivity.
+  all: destruct j; simpl; trivial.
+Qed.
+
+Lemma remove_empty :
+  forall i, remove i Empty = Empty.
+Proof.
+  induction i; simpl; trivial.
+Qed.
+
+Hint Rewrite remove_empty : pmap.
+Hint Resolve remove_empty : pmap.
+
+Lemma gremove_noncanon_s :
+  forall i : positive,
+  forall s : pmap,
+    get i (remove_noncanon i s) = None.
+Proof.
+  induction i; destruct s; simpl; trivial.
+Qed.
+
+Theorem grs :
+  forall i : positive,
+  forall s : pmap,
+    get i (remove i s) = None.
+Proof.
+  intros.
+  rewrite remove_noncanon_same.
+  apply gremove_noncanon_s.
+Qed.
+
+Hint Resolve grs : pmap.
+Hint Rewrite grs : pmap.
+
+Lemma gremove_noncanon_o :
+  forall i j : positive,
+  forall s : pmap,
+    i<>j ->
+    get j (remove_noncanon i s) = get j s.
+Proof.
+  induction i; destruct j; destruct s; simpl; intro; trivial.
+  1, 2: rewrite IHi by congruence.
+  1, 2: reflexivity.
+  congruence.
+Qed.
+
+Theorem gro :
+  forall (i j : positive) (s : pmap),
+    i<>j ->
+    get j (remove i s) = get j s.
+Proof.
+  intros.
+  rewrite remove_noncanon_same.
+  apply gremove_noncanon_o.
+  assumption.
+Qed.
+
+Hint Resolve gro : pmap.
+
+Section MAP2.
+  
+  Variable f : option T -> option T -> option T.
+
+  Section NONE_NONE.
+    Hypothesis f_none_none : f None None = None.
+
+    Fixpoint map2_Empty (b : pmap) :=
+      match b with
+      | Empty => Empty
+      | Node b0 bf b1 =>
+        node (map2_Empty b0) (f None bf) (map2_Empty b1)
+      end.
+
+    Lemma gmap2_Empty: forall i b,
+        get i (map2_Empty b) = f None (get i b).
+    Proof.
+      induction i; destruct b as [ | b0 bf b1]; intros; simpl in *.
+      all: try congruence.
+      - replace
+          (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with
+           | Empty => None
+           | Node _ _ c1 => get i c1
+           end)
+          with (get (xI i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))).
+        + rewrite gnode.
+          simpl. apply IHi.
+        + destruct node; auto with pmap.
+      - replace
+          (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with
+           | Empty => None
+           | Node c0 _ _ => get i c0
+           end)
+          with (get (xO i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))).
+        + rewrite gnode.
+          simpl. apply IHi.
+        + destruct node; auto with pmap.
+      - change (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with
+                | Empty => None
+                | Node _ cf _ => cf
+                end) with (get xH (node (map2_Empty b0) (f None bf) (map2_Empty b1))).
+        rewrite gnode. reflexivity.
+    Qed.
+    
+    Fixpoint map2 (a b : pmap) :=
+      match a with
+      | Empty => map2_Empty b
+      | (Node a0 af a1) =>
+        match b with
+        | (Node b0 bf b1) =>
+          node (map2 a0 b0) (f af bf) (map2 a1 b1)
+        | Empty =>
+          node (map2 a0 Empty) (f af None) (map2 a1 Empty)
+        end
+      end.
+  
+    Lemma gmap2: forall a b i,
+        get i (map2 a b) = f (get i a) (get i b).
+    Proof.
+      induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl.
+      { rewrite gmap2_Empty.
+        rewrite gempty.
+        reflexivity. }
+      destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode.
+      - destruct i; simpl.
+        + rewrite IHa1. rewrite gempty.
+          reflexivity.
+        + rewrite IHa0. rewrite gempty.
+          reflexivity.
+        + reflexivity.
+      - destruct i; simpl; congruence.
+    Qed.
+  End NONE_NONE.
+
+  Section IDEM.
+    Hypothesis f_idem : forall x, f x x = x.
+    
+    Fixpoint map2_idem (a b : pmap) :=
+      if pmap_eq a b then a else
+      match a with
+      | Empty => map2_Empty b
+      | (Node a0 af a1) =>
+        match b with
+        | (Node b0 bf b1) =>
+          node (map2_idem a0 b0) (f af bf) (map2_idem a1 b1)
+        | Empty =>
+          node (map2_idem a0 Empty) (f af None) (map2_idem a1 Empty)
+        end
+      end.
+ 
+    Lemma gmap2_idem: forall a b i,
+        get i (map2_idem a b) = f (get i a) (get i b).
+    Proof.
+      induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl.
+      { destruct pmap_eq.
+        - subst b. rewrite gempty. congruence.
+        - rewrite gempty.
+          rewrite gmap2_Empty by congruence.
+          reflexivity.
+      }
+      destruct pmap_eq.
+      { subst b.
+        congruence.
+      }
+      destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode.
+      - destruct i; simpl.
+        + rewrite IHa1. rewrite gempty.
+          reflexivity.
+        + rewrite IHa0. rewrite gempty.
+          reflexivity.
+        + reflexivity.
+      - destruct i; simpl; congruence.
+    Qed.
+  End IDEM.
+End MAP2.
diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v
index 69b32c7c..587f768e 100644
--- a/mppa_k1c/Archi.v
+++ b/mppa_k1c/Archi.v
@@ -26,11 +26,11 @@ Definition big_endian := false.
 Definition align_int64 := 8%Z.
 Definition align_float64 := 8%Z.
 
-Definition splitlong := negb ptr64.
+Definition splitlong := false.
 
 Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.
 Proof.
-  unfold splitlong. destruct ptr64; simpl; congruence. 
+  unfold splitlong. congruence. 
 Qed.
 
 (** THIS IS NOT CHECKED ! NONE OF THIS ! *)
@@ -77,3 +77,5 @@ Global Opaque ptr64 big_endian splitlong
 (** Whether to generate position-independent code or not *)
 
 Parameter pic_code: unit -> bool.
+
+Definition has_notrap_loads := true.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 92061d04..4caac9e1 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -1045,14 +1045,19 @@ Definition is_trapping_op (op : operation) :=
   | _ => false
   end.
 
+Definition args_of_operation op :=
+  if eq_operation op Omove
+  then 1%nat
+  else List.length (fst (type_of_operation op)).
+
 Lemma is_trapping_op_sound:
   forall op vl sp m,
-    op <> Omove ->
     is_trapping_op op = false ->
-    (List.length vl) = (List.length (fst (type_of_operation op))) ->
+    (List.length vl) = args_of_operation op ->
     eval_operation genv sp op vl m <> None.
 Proof.
-  destruct op; intros; simpl in *; try congruence.
+  unfold args_of_operation.
+  destruct op; destruct eq_operation; intros; simpl in *; try congruence.
   all: try (destruct vl as [ | vh1 vl1]; try discriminate).
   all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
   all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index ec3985c5..0974f872 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -168,13 +168,21 @@ Nondetfunction add (e1: expr) (e2: expr) :=
   | t1, Eop (Oaddimm n2) (t2:::Enil) =>
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
   | t1, (Eop Omul (t2:::t3:::Enil)) =>
-      Eop Omadd (t1:::t2:::t3:::Enil)
+    if Compopts.optim_madd tt
+    then Eop Omadd (t1:::t2:::t3:::Enil)
+    else Eop Oadd (e1:::e2:::Enil)
   | (Eop Omul (t2:::t3:::Enil)), t1 =>
-      Eop Omadd (t1:::t2:::t3:::Enil)
+    if Compopts.optim_madd tt
+    then Eop Omadd (t1:::t2:::t3:::Enil)
+    else Eop Oadd (e1:::e2:::Enil)
   | t1, (Eop (Omulimm n) (t2:::Enil)) =>
-      Eop (Omaddimm n) (t1:::t2:::Enil)
+    if Compopts.optim_madd tt
+    then Eop (Omaddimm n) (t1:::t2:::Enil)
+    else Eop Oadd (e1:::e2:::Enil)
   | (Eop (Omulimm n) (t2:::Enil)), t1 =>
-    Eop (Omaddimm n) (t1:::t2:::Enil)
+    if Compopts.optim_madd tt
+    then Eop (Omaddimm n) (t1:::t2:::Enil)
+    else Eop Oadd (e1:::e2:::Enil)
   | (Eop (Oshlimm n) (t1:::Enil)), t2 =>
     add_shlimm n t1 t2
   | t2, (Eop (Oshlimm n) (t1:::Enil)) =>
@@ -197,7 +205,9 @@ Nondetfunction sub (e1: expr) (e2: expr) :=
   | t1, (Eop Omul (t2:::t3:::Enil)) =>
       Eop Omsub (t1:::t2:::t3:::Enil)
   | t1, (Eop (Omulimm n) (t2:::Enil)) =>
-      Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil)
+    if Compopts.optim_madd tt
+    then Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil)
+    else Eop Osub (e1:::e2:::Enil)
   | _, _ => Eop Osub (e1:::e2:::Enil)
   end.
 
@@ -712,4 +722,4 @@ End SELECT.
 
 (* Local Variables: *)
 (* mode: coq *)
-(* End: *)
\ No newline at end of file
+(* End: *)
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index d3eb1dde..368f78f4 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -350,13 +350,19 @@ Proof.
     apply eval_addimm. EvalOp.
     repeat rewrite Val.add_assoc. reflexivity.
   - (* Omadd *)
-    subst. TrivialExists.
+    subst. destruct (Compopts.optim_madd tt); TrivialExists;
+    repeat (eauto; econstructor; simpl).
   - (* Omadd rev *)
-    subst. rewrite Val.add_commut. TrivialExists.
+    subst. destruct (Compopts.optim_madd tt); TrivialExists;
+    repeat (eauto; econstructor; simpl).
+    simpl. rewrite Val.add_commut. reflexivity.
   - (* Omaddimm *)
-    subst. TrivialExists.
+    subst. destruct (Compopts.optim_madd tt); TrivialExists;
+    repeat (eauto; econstructor; simpl).
   - (* Omaddimm rev *)
-    subst. rewrite Val.add_commut. TrivialExists.
+    subst. destruct (Compopts.optim_madd tt); TrivialExists;
+    repeat (eauto; econstructor; simpl).
+    simpl. rewrite Val.add_commut. reflexivity.
     (* Oaddx *)
   - subst. pose proof eval_addx as ADDX.
     unfold binary_constructor_sound in ADDX.
@@ -380,11 +386,14 @@ Proof.
   - subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp.
   - subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp.
   - TrivialExists. simpl. subst. reflexivity.
-  - TrivialExists. simpl. subst.
-    rewrite sub_add_neg.
-    rewrite neg_mul_distr_r.
-    unfold Val.neg.
-    reflexivity.
+  - destruct (Compopts.optim_madd tt).
+    + TrivialExists. simpl. subst.
+      rewrite sub_add_neg.
+      rewrite neg_mul_distr_r.
+      unfold Val.neg.
+      reflexivity.
+    + TrivialExists. repeat (eauto; econstructor).
+      simpl. subst. reflexivity.
   - TrivialExists.
 Qed.
 
diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 10f38391..8f96dafc 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -71,3 +71,5 @@ Global Opaque ptr64 big_endian splitlong
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
               float_of_single_preserves_sNaN.
+
+Definition has_notrap_loads := false.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index b73cb14b..a0ee5bb8 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -592,14 +592,20 @@ Definition is_trapping_op (op : operation) :=
   | _ => false
   end.
 
+Definition args_of_operation op :=
+  if eq_operation op Omove
+  then 1%nat
+  else List.length (fst (type_of_operation op)).
+
+
 Lemma is_trapping_op_sound:
   forall op vl sp m,
-    op <> Omove ->
     is_trapping_op op = false ->
-    (List.length vl) = (List.length (fst (type_of_operation op))) ->
+    (List.length vl) = args_of_operation op ->
     eval_operation genv sp op vl m <> None.
 Proof.
-  destruct op; intros; simpl in *; try congruence.
+  unfold args_of_operation.
+  destruct op; destruct eq_operation; intros; simpl in *; try congruence.
   all: try (destruct vl as [ | vh1 vl1]; try discriminate).
   all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
   all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
diff --git a/riscV/Archi.v b/riscV/Archi.v
index 61d129d0..9bdaad99 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -72,3 +72,5 @@ Global Opaque ptr64 big_endian splitlong
 (** Whether to generate position-independent code or not *)
 
 Parameter pic_code: unit -> bool.
+
+Definition has_notrap_loads := false.
diff --git a/riscV/Op.v b/riscV/Op.v
index a71696c7..14d07e0b 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -682,15 +682,21 @@ Definition is_trapping_op (op : operation) :=
   | Ofloatoflong | Ofloatoflongu => true
   | _ => false
   end.
+                
+
+Definition args_of_operation op :=
+  if eq_operation op Omove
+  then 1%nat
+  else List.length (fst (type_of_operation op)).
 
 Lemma is_trapping_op_sound:
   forall op vl sp m,
-    op <> Omove ->
     is_trapping_op op = false ->
-    (List.length vl) = (List.length (fst (type_of_operation op))) ->
+    (List.length vl) = args_of_operation op ->
     eval_operation genv sp op vl m <> None.
 Proof.
-  destruct op; intros; simpl in *; try congruence.
+  unfold args_of_operation.
+  destruct op; destruct eq_operation; intros; simpl in *; try congruence.
   all: try (destruct vl as [ | vh1 vl1]; try discriminate).
   all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
   all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
diff --git a/test/monniaux/cse2/noloopinvariant.c b/test/monniaux/cse2/noloopinvariant.c
new file mode 100644
index 00000000..5c7789bf
--- /dev/null
+++ b/test/monniaux/cse2/noloopinvariant.c
@@ -0,0 +1,6 @@
+int toto(int *t, int n) {
+  for(int i=1; i<n; i++) {
+    if (t[i] > t[0]) return i;
+  }
+  return 0;
+}
diff --git a/x86/Op.v b/x86/Op.v
index 15672bbe..28e6dbd8 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -760,14 +760,19 @@ Definition is_trapping_op (op : operation) :=
   | _ => false
   end.
 
+Definition args_of_operation op :=
+  if eq_operation op Omove
+  then 1%nat
+  else List.length (fst (type_of_operation op)).
+
 Lemma is_trapping_op_sound:
   forall op vl sp m,
-    op <> Omove ->
     is_trapping_op op = false ->
-    (List.length vl) = (List.length (fst (type_of_operation op))) ->
+    (List.length vl) = args_of_operation op ->
     eval_operation genv sp op vl m <> None.
 Proof.
-  destruct op; intros; simpl in *; try congruence.
+  unfold args_of_operation.
+  destruct op; destruct eq_operation; intros; simpl in *; try congruence.
   all: try (destruct vl as [ | vh1 vl1]; try discriminate).
   all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
   all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
diff --git a/x86_32/Archi.v b/x86_32/Archi.v
index e9d05c14..4681784d 100644
--- a/x86_32/Archi.v
+++ b/x86_32/Archi.v
@@ -64,3 +64,5 @@ Global Opaque ptr64 big_endian splitlong
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
               float_of_single_preserves_sNaN.
+
+Definition has_notrap_loads := false.
diff --git a/x86_64/Archi.v b/x86_64/Archi.v
index 959d8dc1..0e3c55f8 100644
--- a/x86_64/Archi.v
+++ b/x86_64/Archi.v
@@ -64,3 +64,5 @@ Global Opaque ptr64 big_endian splitlong
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
               float_of_single_preserves_sNaN.
+
+Definition has_notrap_loads := false.