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

8 files changed, 1164 insertions, 2 deletions

diff --git a/backend/CSE.v b/backend/CSE.v
index 1936d4e4..838d96a6 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -493,7 +493,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
               | _ =>
                   empty_numbering
               end
-          | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ =>
+          | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ | EF_profiling _ _ =>
               set_res_unknown before res
           end
       | Icond cond args ifso ifnot _ =>
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 5bbb7508..a7465cee 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -1318,6 +1318,7 @@ Proof.
   + apply CASE2; inv H1; auto.
   + apply CASE1.
   + apply CASE2; inv H1; auto.
+  + apply CASE2; inv H1; auto.
 * apply set_res_lessdef; auto.
 
 - (* Icond *)
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index e14da87e..7fa10aee 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -111,6 +111,10 @@ let elf_symbol_offset oc (symb, ofs) =
   if ofs <> 0L then fprintf oc " + %Ld" ofs
 
 (* Functions for fun and var info *)
+let elf_text_print_fun_info oc name =
+  fprintf oc "	.type	%s, @function\n" name;
+  fprintf oc "	.size	%s, . - %s\n" name name
+
 let elf_print_fun_info oc name =
   fprintf oc "	.type	%a, @function\n" elf_symbol name;
   fprintf oc "	.size	%a, . - %a\n" elf_symbol name elf_symbol name
@@ -311,4 +315,84 @@ let common_section ?(sec = ".bss") () =
   if !Clflags.option_fcommon then
     "COMM"
   else
-    sec
+    sec;;
+
+(* Profiling *)
+let profiling_table : (Digest.t, int) Hashtbl.t = Hashtbl.create 1000;;
+let next_profiling_position = ref 0;;
+let profiling_position (x : Digest.t) : int =
+  match Hashtbl.find_opt profiling_table x with
+  | None -> let y = !next_profiling_position in
+            next_profiling_position := succ y;
+            Hashtbl.replace profiling_table x y;
+            y
+  | Some y -> y;;
+
+let profiling_ids () =
+  let nr_items = !next_profiling_position in
+  let ar = Array.make nr_items "" in
+  Hashtbl.iter
+    (fun x y -> ar.(y) <- x)
+    profiling_table;
+  ar;;
+
+let print_profiling_id oc id =
+  assert (String.length id = 16);
+  output_string oc "	.byte";
+  for i=0 to 15 do
+    fprintf oc " 0x%02x" (Char.code (String.get id i));
+    if i < 15 then output_char oc ','
+  done;
+  output_char oc '\n';;
+
+let profiling_counter_table_name = ".compcert_profiling_counters"
+and profiling_id_table_name = ".compcert_profiling_ids"
+and profiling_write_table = ".compcert_profiling_save_for_this_object"
+and profiling_init = ".compcert_profiling_init"
+and profiling_write_table_helper = "_compcert_write_profiling_table"
+and dtor_section = ".dtors.65435,\"aw\",@progbits"
+(* and fini_section = ".fini_array_00100,\"aw\"" *)
+and init_section = ".init_array,\"aw\"";;
+
+type finalizer_call_method =
+  | Dtors
+  | Init_atexit of (out_channel -> string -> unit);;
+
+let write_symbol_pointer oc sym =
+  if Archi.ptr64
+  then fprintf oc "	.8byte	%s\n" sym
+  else fprintf oc "	.4byte	%s\n" sym;;
+
+let print_profiling_epilogue declare_function finalizer_call_method print_profiling_stub oc =
+  if !Clflags.option_profile_arcs
+  then
+    let nr_items = !next_profiling_position in
+    if nr_items > 0
+    then
+      begin
+        fprintf oc "	.lcomm	%s, %d\n"
+          profiling_counter_table_name (nr_items * 16);
+        fprintf oc "	.section	.rodata\n";
+        fprintf oc "%s:\n" profiling_id_table_name;
+        Array.iter (print_profiling_id oc) (profiling_ids ());
+        fprintf oc "	.text\n";
+        fprintf oc "%s:\n" profiling_write_table;
+        print_profiling_stub oc nr_items
+          profiling_id_table_name
+          profiling_counter_table_name;
+        declare_function oc profiling_write_table;
+        match finalizer_call_method with
+        | Dtors ->
+           fprintf oc "	.section	%s\n" dtor_section;
+           write_symbol_pointer oc profiling_write_table
+        | Init_atexit(atexit_call) ->
+           fprintf oc "	.section	%s\n" init_section;
+           write_symbol_pointer oc profiling_init;
+           fprintf oc "	.text\n";
+           fprintf oc "%s:\n" profiling_init;
+           atexit_call oc profiling_write_table;
+           declare_function oc profiling_init
+      end;;
+
+let profiling_offset id kind =
+  ((profiling_position id)*2 + kind)*8;;
diff --git a/backend/Profiling.v b/backend/Profiling.v
new file mode 100644
index 00000000..4cba49ee
--- /dev/null
+++ b/backend/Profiling.v
@@ -0,0 +1,65 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL.
+
+Local Open Scope positive.
+
+Parameter function_id : function -> AST.profiling_id.
+Parameter branch_id : AST.profiling_id -> node -> AST.profiling_id.
+
+Section PER_FUNCTION_ID.
+  Variable f_id : AST.profiling_id.
+  
+  Definition inject_profiling_call (prog : code)
+             (pc extra_pc ifso ifnot : node) : node * code :=
+    let id := branch_id f_id pc in
+    let extra_pc' := Pos.succ extra_pc in
+    let prog' := PTree.set extra_pc
+                           (Ibuiltin (EF_profiling id 0%Z) nil BR_none ifnot) prog in
+    let prog'':= PTree.set extra_pc'
+                           (Ibuiltin (EF_profiling id 1%Z) nil BR_none ifso) prog' in
+    (Pos.succ extra_pc', prog'').
+  
+  Definition inject_at (prog : code) (pc extra_pc : node) : node * code :=
+    match PTree.get pc prog with
+    | Some (Icond cond args ifso ifnot expected) =>
+      inject_profiling_call
+        (PTree.set pc
+                   (Icond cond args (Pos.succ extra_pc) extra_pc expected) prog)
+        pc extra_pc ifso ifnot
+    | _ => inject_profiling_call prog pc extra_pc 1 1 (* does not happen *)
+    end.
+
+  Definition inject_at' (already : node * code) pc :=
+    let (extra_pc, prog) := already in
+    inject_at prog pc extra_pc.
+
+  Definition inject_l (prog : code) extra_pc injections :=
+    List.fold_left (fun already (inject_pc : node) =>
+                      inject_at' already inject_pc)
+                   injections
+                   (extra_pc, prog).
+
+  Definition gen_conditions (prog : code) :=
+    List.map fst (PTree.elements (PTree.filter1
+                                    (fun instr =>
+                                       match instr with
+                                       | Icond cond args ifso ifnot expected => true
+                                       | _ => false
+                                       end) prog)).
+End PER_FUNCTION_ID.
+
+Definition transf_function (f : function) : function :=
+  let max_pc := max_pc_function f in
+  let conditions := gen_conditions (fn_code f) in
+  {| fn_sig := f.(fn_sig);
+     fn_params := f.(fn_params);
+     fn_stacksize := f.(fn_stacksize);
+     fn_code := snd (inject_l (function_id f) (fn_code f) (Pos.succ max_pc) conditions);
+     fn_entrypoint := f.(fn_entrypoint) |}.
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
diff --git a/backend/ProfilingExploit.v b/backend/ProfilingExploit.v
new file mode 100644
index 00000000..cfca1a12
--- /dev/null
+++ b/backend/ProfilingExploit.v
@@ -0,0 +1,30 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL.
+
+Local Open Scope positive.
+
+Parameter function_id : function -> AST.profiling_id.
+Parameter branch_id : AST.profiling_id -> node -> AST.profiling_id.
+Parameter condition_oracle : AST.profiling_id -> option bool.
+
+Definition transf_instr (f_id : AST.profiling_id)
+           (pc : node) (i : instruction) : instruction :=
+  match i with
+  | Icond cond args ifso ifnot None =>
+    Icond cond args ifso ifnot (condition_oracle (branch_id f_id pc))
+  | _ => i
+  end.
+
+Definition transf_function (f : function) : function :=
+  {| fn_sig := f.(fn_sig);
+     fn_params := f.(fn_params);
+     fn_stacksize := f.(fn_stacksize);
+     fn_code := PTree.map (transf_instr (function_id f)) f.(fn_code);
+     fn_entrypoint := f.(fn_entrypoint) |}.
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
diff --git a/backend/ProfilingExploitproof.v b/backend/ProfilingExploitproof.v
new file mode 100644
index 00000000..bc68c38e
--- /dev/null
+++ b/backend/ProfilingExploitproof.v
@@ -0,0 +1,224 @@
+Require Import FunInd.
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import ProfilingExploit.
+
+
+Definition match_prog (p tp: RTL.program) :=
+  match_program (fun ctx f tf => tf = transf_fundef f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_prog p (transf_program p).
+Proof.
+  intros. eapply match_transform_program; eauto.
+Qed.
+
+Section PRESERVATION.
+
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_transf TRANSL).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  Genv.find_funct_ptr tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_ptr_transf TRANSL).
+
+Lemma symbols_preserved:
+  forall id,
+  Genv.find_symbol tge id = Genv.find_symbol ge id.
+Proof (Genv.find_symbol_transf TRANSL).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_transf TRANSL).
+
+Lemma sig_preserved:
+  forall f, funsig (transf_fundef f) = funsig f.
+Proof.
+  destruct f; reflexivity.
+Qed.
+
+Lemma find_function_translated:
+  forall ros rs fd,
+  find_function ge ros rs = Some fd ->
+  find_function tge ros rs = Some (transf_fundef fd).
+Proof.
+  unfold find_function; intros. destruct ros as [r|id].
+  eapply functions_translated; eauto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
+  eapply function_ptr_translated; eauto.
+Qed.
+
+Lemma transf_function_at:
+  forall f pc i,
+  f.(fn_code)!pc = Some i ->
+  (transf_function f).(fn_code)!pc = Some(transf_instr (function_id f) pc i).
+Proof.
+  intros until i. intro Hcode.
+  unfold transf_function; simpl.
+  rewrite PTree.gmap.
+  unfold option_map.
+  rewrite Hcode.
+  reflexivity.
+Qed.
+
+Ltac TR_AT :=
+  match goal with
+  | [ A: (fn_code _)!_ = Some _ |- _ ] =>
+        generalize (transf_function_at _ _ _ A); intros
+  end.
+
+
+Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
+  | match_frames_intro: forall res f sp pc rs,
+      match_frames (Stackframe res f sp pc rs)
+                   (Stackframe res (transf_function f) sp pc rs).
+
+Inductive match_states: RTL.state -> RTL.state -> Prop :=
+  | match_regular_states: forall stk f sp pc rs m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (State stk f sp pc rs m)
+                   (State stk' (transf_function f) sp pc rs m)
+  | match_callstates: forall stk f args m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Callstate stk f args m)
+                   (Callstate stk' (transf_fundef f) args m)
+  | match_returnstates: forall stk v m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Returnstate stk v m)
+                   (Returnstate stk' v m).
+
+Lemma step_simulation:
+  forall S1 t S2, RTL.step ge S1 t S2 ->
+  forall S1', match_states S1 S1' ->
+  exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
+Proof.
+  induction 1; intros S1' MS; inv MS; try TR_AT.
+- (* nop *)
+  econstructor; split. eapply exec_Inop; eauto.
+  constructor; auto.
+- (* op *)
+  econstructor; split.
+  eapply exec_Iop with (v := v); eauto.
+  rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
+  constructor; auto.
+(* load *)
+- econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload; eauto.
+  constructor; auto.
+- (* load notrap1 *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = None).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload_notrap1; eauto.
+  constructor; auto.
+- (* load notrap2 *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload_notrap2; eauto.
+  constructor; auto. 
+- (* store *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Istore; eauto.
+  constructor; auto. 
+(* call *)
+- econstructor; split.
+  eapply exec_Icall with (fd := transf_fundef fd); eauto.
+    eapply find_function_translated; eauto.
+    apply sig_preserved.
+  constructor. constructor; auto. constructor.
+(* tailcall *)
+- econstructor; split.
+  eapply exec_Itailcall with (fd := transf_fundef fd); eauto.
+    eapply find_function_translated; eauto.
+    apply sig_preserved.
+  constructor. auto.
+(* builtin *)
+- econstructor; split.
+  eapply exec_Ibuiltin; eauto.
+    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  constructor; auto.
+(* cond *)
+- destruct predb.
+  + econstructor; split.
+    eapply exec_Icond; eauto.
+    constructor; auto.
+  + simpl transf_instr in H1.
+    destruct condition_oracle in H1.
+    * econstructor; split.
+      eapply exec_Icond; eauto.
+      constructor; auto.
+    * econstructor; split.
+      eapply exec_Icond; eauto.
+      constructor; auto.
+(* jumptbl *)
+- econstructor; split.
+  eapply exec_Ijumptable; eauto.
+  constructor; auto.
+(* return *)
+- econstructor; split.
+  eapply exec_Ireturn; eauto.
+  constructor; auto.
+(* internal function *)
+-  simpl. econstructor; split.
+  eapply exec_function_internal; eauto.
+  constructor; auto.
+(* external function *)
+- econstructor; split.
+  eapply exec_function_external; eauto.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  constructor; auto.
+(* return *)
+- inv STACKS. inv H1.
+  econstructor; split.
+  eapply exec_return; eauto.
+  constructor; auto.
+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. inv H. econstructor; split.
+  econstructor.
+    eapply (Genv.init_mem_transf TRANSL); eauto.
+    rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto.
+    eapply function_ptr_translated; eauto.
+    rewrite <- H3; apply sig_preserved.
+  constructor. constructor.
+Qed.
+
+Lemma transf_final_states:
+  forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
+Proof.
+  eapply forward_simulation_step.
+  apply senv_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact step_simulation.
+Qed.
+
+End PRESERVATION.
diff --git a/backend/Profilingaux.ml b/backend/Profilingaux.ml
new file mode 100644
index 00000000..f8fc5d6b
--- /dev/null
+++ b/backend/Profilingaux.ml
@@ -0,0 +1,71 @@
+open Camlcoq
+open RTL
+open Maps
+   
+type identifier = Digest.t
+
+let pp_id channel (x : identifier) =
+  assert(String.length x = 16);
+  for i=0 to 15 do
+    Printf.fprintf channel "%02x" (Char.code (String.get x i))
+  done
+
+let print_anonymous_function pp f =
+  let instrs =
+    List.sort
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+      (List.rev_map
+        (fun (pc, i) -> (P.to_int pc, i))
+        (PTree.elements f.fn_code)) in
+  PrintRTL.print_succ pp f.fn_entrypoint
+    (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1);
+  List.iter (PrintRTL.print_instruction pp) instrs;
+  Printf.fprintf pp "}\n\n"
+  
+let function_id (f : coq_function) : identifier =
+  let digest = Digest.string (Marshal.to_string f []) in
+  Printf.fprintf stderr "FUNCTION hash = %a\n" pp_id digest;
+  print_anonymous_function stderr f;
+  digest
+
+let branch_id (f_id : identifier) (node : P.t) : identifier =
+  Digest.string (f_id ^ (Int64.to_string (P.to_int64 node)));;
+
+let profiling_counts : (identifier, (Int64.t*Int64.t)) Hashtbl.t = Hashtbl.create 1000;;
+
+let get_counts id =
+  match Hashtbl.find_opt profiling_counts id with
+  | Some x -> x
+  | None -> (0L, 0L);;
+  
+let add_profiling_counts id counter0 counter1 =
+  let (old0, old1) = get_counts id in
+    Hashtbl.replace profiling_counts id (Int64.add old0 counter0,
+                                         Int64.add old1 counter1);;
+
+let input_counter (ic : in_channel) : Int64.t =
+  let r = ref Int64.zero in
+  for i=0 to 7
+  do
+    r := Int64.add !r (Int64.shift_left (Int64.of_int (input_byte ic)) (8*i))
+  done;
+  !r;;
+  
+let load_profiling_info (filename : string) : unit =
+  let ic = open_in filename in
+  try
+    while true do
+      let id : identifier = really_input_string ic 16 in
+      let counter0 = input_counter ic in
+      let counter1 = input_counter ic in
+      (* Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id counter0 counter1 *)
+      add_profiling_counts id counter0 counter1
+    done
+  with End_of_file -> close_in ic;;
+
+let condition_oracle (id : identifier) : bool option =
+  let (count0, count1) = get_counts id in
+  ( (* if count0 <> 0L || count1 <> 0L then *)
+  Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id count0 count1);
+  if count0 = count1 then None
+  else Some(count1 > count0);;
diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v
new file mode 100644
index 00000000..fc04c77e
--- /dev/null
+++ b/backend/Profilingproof.v
@@ -0,0 +1,687 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import Profiling.
+Require Import Lia.
+
+Local Open Scope positive.
+
+Definition match_prog (p tp: RTL.program) :=
+  match_program (fun ctx f tf => tf = transf_fundef f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_prog p (transf_program p).
+Proof.
+  intros. eapply match_transform_program; eauto.
+Qed.
+
+Section PRESERVATION.
+
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_transf TRANSL).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  Genv.find_funct_ptr tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_ptr_transf TRANSL).
+
+Lemma symbols_preserved:
+  forall id,
+  Genv.find_symbol tge id = Genv.find_symbol ge id.
+Proof (Genv.find_symbol_transf TRANSL).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_transf TRANSL).
+
+Lemma sig_preserved:
+  forall f, funsig (transf_fundef f) = funsig f.
+Proof.
+  destruct f; reflexivity.
+Qed.
+
+Lemma find_function_translated:
+  forall ros rs fd,
+  find_function ge ros rs = Some fd ->
+  find_function tge ros rs = Some (transf_fundef fd).
+Proof.
+  unfold find_function; intros. destruct ros as [r|id].
+  eapply functions_translated; eauto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
+  eapply function_ptr_translated; eauto.
+Qed.
+
+Lemma pair_expand:
+  forall { A B : Type } (p : A*B),
+    p = ((fst p), (snd p)).
+Proof.
+  destruct p; simpl; trivial.
+Qed.
+
+Lemma inject_profiling_call_preserves:
+  forall id body pc extra_pc ifso ifnot pc0,
+    pc0 < extra_pc ->
+    PTree.get pc0 (snd (inject_profiling_call id body pc extra_pc ifso ifnot)) = PTree.get pc0 body.
+Proof.
+  intros. simpl.
+  rewrite PTree.gso by lia.
+  apply PTree.gso.
+  lia.
+Qed.
+    
+Lemma inject_at_preserves :
+  forall id body pc extra_pc pc0,
+    pc0 < extra_pc ->
+    pc0 <> pc ->
+    PTree.get pc0 (snd (inject_at id body pc extra_pc)) = PTree.get pc0 body.
+Proof.
+  intros. unfold inject_at.
+  destruct (PTree.get pc body) eqn:GET.
+  - destruct i.
+    all: try (rewrite inject_profiling_call_preserves; trivial; fail).
+    rewrite inject_profiling_call_preserves by trivial.
+    apply PTree.gso; lia.
+  - apply inject_profiling_call_preserves; trivial.
+Qed.
+
+Lemma inject_profiling_call_increases:
+  forall id body pc extra_pc ifso ifnot,
+    fst (inject_profiling_call id body pc extra_pc ifso ifnot) = extra_pc + 2.
+Proof.
+  intros.
+  simpl.
+  lia.
+Qed.
+
+Lemma inject_at_increases:
+  forall id body pc extra_pc,
+    (fst (inject_at id body pc extra_pc)) = extra_pc + 2.
+Proof.
+  intros. unfold inject_at.
+  destruct (PTree.get pc body).
+  - destruct i; apply inject_profiling_call_increases.
+  - apply inject_profiling_call_increases.
+Qed.
+
+Lemma inject_l_preserves :
+  forall id injections body extra_pc pc0,
+    pc0 < extra_pc ->
+    List.forallb (fun injection => if peq injection pc0 then false else true) injections = true ->
+    PTree.get pc0 (snd (inject_l id body extra_pc injections)) = PTree.get pc0 body.
+Proof.
+  induction injections;
+    intros until pc0; intros BEFORE ALL; simpl; trivial.
+  unfold inject_l.
+  simpl in ALL.
+  rewrite andb_true_iff in ALL.
+  destruct ALL as [NEQ ALL].
+  simpl.
+  rewrite pair_expand with (p := inject_at id body a extra_pc).
+  progress fold (inject_l id (snd (inject_at id body a extra_pc))
+              (fst (inject_at id body a extra_pc))
+              injections).
+  rewrite IHinjections; trivial.
+  - apply inject_at_preserves; trivial.
+    destruct (peq a pc0); congruence.
+  - rewrite inject_at_increases.
+    lia.
+Qed.
+
+Fixpoint inject_l_position extra_pc
+         (injections : list node)
+         (k : nat) {struct injections} : node :=
+  match injections with
+  | nil => extra_pc
+  | pc::l' =>
+    match k with
+    | O => extra_pc
+    | S k' => inject_l_position (extra_pc + 2) 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 k.
+  lia.
+  specialize IHinjections with (pc := pc + 2) (k := k).
+  lia.
+Qed.
+
+Lemma inject_l_injected_pc:
+  forall f_id injections cond args ifso ifnot expected body injnum pc extra_pc
+         (INSTR : body ! pc = Some  (Icond cond args ifso ifnot expected))
+         (BELOW : forallb (fun pc => pc <? extra_pc) injections = true)
+         (NOREPET : list_norepet injections)
+         (NUMBER : nth_error injections injnum = Some pc),
+    PTree.get pc (snd (inject_l f_id body extra_pc injections)) =
+    Some (Icond cond args
+                (Pos.succ (inject_l_position extra_pc injections injnum))
+                (inject_l_position extra_pc injections injnum) expected).
+Proof.
+  induction injections; simpl; intros.
+  { rewrite nth_error_nil in NUMBER.
+    discriminate NUMBER. }
+  simpl in BELOW.
+  rewrite andb_true_iff in BELOW.
+  destruct BELOW as [BELOW1 BELOW2].
+  rewrite Pos.ltb_lt in BELOW1.
+  unfold inject_l.
+  simpl fold_left.
+  rewrite pair_expand with (p := inject_at f_id body a extra_pc).
+  progress fold (inject_l f_id (snd (inject_at f_id body a extra_pc))
+              (fst (inject_at f_id body a extra_pc))
+              injections).
+  destruct injnum as [ | injnum']; simpl in NUMBER.
+  { inv NUMBER.
+    rewrite inject_l_preserves; simpl.
+    - unfold inject_at.
+      rewrite INSTR.
+      unfold inject_profiling_call. simpl.
+      rewrite PTree.gso by lia.
+      rewrite PTree.gso by lia.
+      apply PTree.gss.
+    - rewrite inject_at_increases.
+      lia.
+    - inv NOREPET.
+      rewrite forallb_forall.
+      intros x IN.
+      destruct peq as [EQ | ]; trivial.
+      subst x.
+      contradiction.
+  }
+  simpl.
+  rewrite inject_at_increases.
+  apply IHinjections with (ifso := ifso) (ifnot := ifnot).
+  - rewrite inject_at_preserves; trivial.
+    + rewrite forallb_forall in BELOW2.
+      rewrite <- Pos.ltb_lt.
+      apply nth_error_In in NUMBER.
+      auto.
+    + inv NOREPET.
+      intro ZZZ.
+      subst a.
+      apply nth_error_In in NUMBER.
+      auto.
+
+  - rewrite forallb_forall in BELOW2.
+    rewrite forallb_forall.
+    intros.
+    specialize BELOW2 with x.
+    rewrite Pos.ltb_lt in *.
+    intuition lia.
+  - inv NOREPET. trivial.
+  - trivial.
+Qed.
+ 
+Lemma inject_l_injected0:
+  forall f_id  cond args ifso ifnot expected injections body injnum pc extra_pc
+         (INSTR : body ! pc = Some  (Icond cond args ifso ifnot expected))
+         (BELOW : forallb (fun pc => pc <? extra_pc) injections = true)
+         (NOREPET : list_norepet injections)
+         (NUMBER : nth_error injections injnum = Some pc),
+    PTree.get (inject_l_position extra_pc injections injnum)
+              (snd (inject_l f_id body extra_pc injections)) =
+    Some (Ibuiltin (EF_profiling (branch_id f_id pc) 0%Z) nil BR_none ifnot).
+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.
+  simpl fold_left.
+  rewrite pair_expand with (p := inject_at f_id body a extra_pc).
+  progress fold (inject_l f_id (snd (inject_at f_id body a extra_pc))
+              (fst (inject_at f_id body a extra_pc))
+              injections).
+  destruct injnum as [ | injnum']; simpl in NUMBER.
+  { inv NUMBER.
+    rewrite inject_l_preserves; simpl.
+    - unfold inject_at.
+      rewrite INSTR.
+      unfold inject_profiling_call. simpl.
+      rewrite PTree.gso by lia.
+      apply PTree.gss.
+    - rewrite inject_at_increases.
+      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.
+      lia.
+  }
+  simpl.
+  rewrite inject_at_increases.
+  
+  apply IHinjections.
+  - rewrite inject_at_preserves; trivial.
+    + rewrite forallb_forall in BELOW2.
+      rewrite <- Pos.ltb_lt.
+      apply nth_error_In in NUMBER.
+      auto.
+    + inv NOREPET.
+      intro ZZZ.
+      subst a.
+      apply nth_error_In in NUMBER.
+      auto.
+
+  - rewrite forallb_forall in BELOW2.
+    rewrite forallb_forall.
+    intros.
+    specialize BELOW2 with x.
+    rewrite Pos.ltb_lt in *.
+    intuition lia.
+  - inv NOREPET. trivial.
+  - trivial.
+Qed.
+
+Lemma inject_l_injected1:
+  forall f_id  cond args ifso ifnot expected injections body injnum pc extra_pc
+         (INSTR : body ! pc = Some  (Icond cond args ifso ifnot expected))
+         (BELOW : forallb (fun pc => pc <? extra_pc) injections = true)
+         (NOREPET : list_norepet injections)
+         (NUMBER : nth_error injections injnum = Some pc),
+    PTree.get (Pos.succ (inject_l_position extra_pc injections injnum))
+              (snd (inject_l f_id body extra_pc injections)) =
+    Some (Ibuiltin (EF_profiling (branch_id f_id pc) 1%Z) nil BR_none ifso).
+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.
+  simpl fold_left.
+  rewrite pair_expand with (p := inject_at f_id body a extra_pc).
+  progress fold (inject_l f_id (snd (inject_at f_id body a extra_pc))
+              (fst (inject_at f_id body a extra_pc))
+              injections).
+  destruct injnum as [ | injnum']; simpl in NUMBER.
+  { inv NUMBER.
+    rewrite inject_l_preserves; simpl.
+    - unfold inject_at.
+      rewrite INSTR.
+      unfold inject_profiling_call. simpl.
+      apply PTree.gss.
+    - rewrite inject_at_increases.
+      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.
+      lia.
+  }
+  simpl.
+  rewrite inject_at_increases.
+  
+  apply IHinjections.
+  - rewrite inject_at_preserves; trivial.
+    + rewrite forallb_forall in BELOW2.
+      rewrite <- Pos.ltb_lt.
+      apply nth_error_In in NUMBER.
+      auto.
+    + inv NOREPET.
+      intro ZZZ.
+      subst a.
+      apply nth_error_In in NUMBER.
+      auto.
+
+  - rewrite forallb_forall in BELOW2.
+    rewrite forallb_forall.
+    intros.
+    specialize BELOW2 with x.
+    rewrite Pos.ltb_lt in *.
+    intuition lia.
+  - inv NOREPET. trivial.
+  - trivial.
+Qed.
+  
+Lemma transf_function_at:
+  forall f pc i
+    (CODE : f.(fn_code)!pc = Some i)
+    (INSTR : match i with
+             | Icond _ _ _ _ _ => False
+             | _ => True
+             end),
+    (transf_function f).(fn_code)!pc = Some i.
+Proof.
+  intros.
+  unfold transf_function; simpl.
+  rewrite inject_l_preserves.
+  assumption.
+  - pose proof (max_pc_function_sound f pc i CODE) as LE.
+    unfold Ple in LE.
+    lia.
+  - rewrite forallb_forall.
+    intros x IN.
+    destruct peq; trivial.
+    subst x.
+    unfold gen_conditions in IN.
+    rewrite in_map_iff in IN.
+    destruct IN as [[pc' i'] [EQ IN]].
+    simpl in EQ.
+    subst pc'.
+    apply PTree.elements_complete in IN.
+    rewrite PTree.gfilter1 in IN.
+    rewrite CODE in IN.
+    destruct i; try discriminate; contradiction.
+Qed.
+
+Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
+| match_frames_intro: forall res f sp pc rs,
+      match_frames (Stackframe res f sp pc rs)
+                   (Stackframe res (transf_function f) sp pc rs).
+
+Inductive match_states: RTL.state -> RTL.state -> Prop :=
+  | match_regular_states: forall stk f sp pc rs m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (State stk f sp pc rs m)
+                   (State stk' (transf_function f) sp pc rs m)
+  | match_callstates: forall stk f args m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Callstate stk f args m)
+                   (Callstate stk' (transf_fundef f) args m)
+  | match_returnstates: forall stk v m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Returnstate stk v m)
+                   (Returnstate stk' v m).
+
+Lemma funsig_preserved:
+  forall fd,
+    funsig (transf_fundef fd) = funsig fd.
+Proof.
+  destruct fd; simpl; trivial.
+Qed.
+
+Lemma stacksize_preserved:
+  forall f,
+    fn_stacksize (transf_function f) = fn_stacksize f.
+Proof.
+  destruct f; simpl; trivial.
+Qed.
+
+Hint Resolve symbols_preserved funsig_preserved external_call_symbols_preserved senv_preserved stacksize_preserved : profiling.
+
+Lemma step_simulation:
+  forall s1 t s2 (STEP : step ge s1 t s2)
+  s1' (MS: match_states s1 s1'),
+  exists s2', plus step tge s1' t s2' /\ match_states s2 s2'.
+Proof.
+  induction 1; intros; inv MS.
+  - econstructor; split.
+    + apply plus_one. apply exec_Inop.
+      erewrite transf_function_at; eauto. apply I.
+    + constructor; auto.
+  - econstructor; split.
+    + apply plus_one. apply exec_Iop with (op:=op) (args:=args).
+      * erewrite transf_function_at; eauto. apply I.
+      * rewrite eval_operation_preserved with (ge1:=ge);
+          eauto with profiling.
+    + constructor; auto.
+  - econstructor; split.
+    + apply plus_one. apply exec_Iload with (trap:=trap) (chunk:=chunk)
+                                            (addr:=addr) (args:=args) (a:=a).
+      erewrite transf_function_at; eauto. apply I.
+      rewrite eval_addressing_preserved with (ge1:=ge).
+      all: eauto with profiling.
+    + constructor; auto.
+  - econstructor; split.
+    + apply plus_one. apply exec_Iload_notrap1 with (chunk:=chunk)
+                                            (addr:=addr) (args:=args).
+      erewrite transf_function_at; eauto. apply I.
+      rewrite eval_addressing_preserved with (ge1:=ge).
+      all: eauto with profiling.
+    + constructor; auto.
+  -  econstructor; split.
+    + apply plus_one. apply exec_Iload_notrap2 with (chunk:=chunk)
+                                            (addr:=addr) (args:=args) (a:=a).
+      erewrite transf_function_at; eauto. apply I.
+      rewrite eval_addressing_preserved with (ge1:=ge).
+      all: eauto with profiling.
+    + constructor; auto.
+  -  econstructor; split.
+    + apply plus_one. apply exec_Istore with (chunk:=chunk) (src := src)
+                                            (addr:=addr) (args:=args) (a:=a).
+      erewrite transf_function_at; eauto. apply I.
+      rewrite eval_addressing_preserved with (ge1:=ge).
+      all: eauto with profiling.
+    + constructor; auto.
+  - econstructor; split.
+    + apply plus_one. apply exec_Icall with (sig:=(funsig fd)) (ros:=ros).
+      erewrite transf_function_at; eauto. apply I.
+      apply find_function_translated with (fd := fd).
+      all: eauto with profiling.
+    + constructor; auto.
+      constructor; auto.
+      constructor.
+  - econstructor; split.
+    + apply plus_one. apply exec_Itailcall with (sig:=(funsig fd)) (ros:=ros).
+      erewrite transf_function_at; eauto. apply I.
+      apply find_function_translated with (fd := fd).
+      all: eauto with profiling.
+    + constructor; auto.
+  - econstructor; split.
+    + apply plus_one.
+      apply exec_Ibuiltin with (ef:=ef) (args:=args) (vargs:=vargs).
+      erewrite transf_function_at; eauto. apply I.
+      apply eval_builtin_args_preserved with (ge1:=ge).
+      all: eauto with profiling.
+    + constructor; auto.
+  - destruct b.
+    + assert (In pc (gen_conditions (fn_code f))) as IN.
+              { unfold gen_conditions.
+                rewrite in_map_iff.
+                exists (pc,  (Icond cond args ifso ifnot predb)).
+                split; simpl; trivial.
+                apply PTree.elements_correct.
+                rewrite PTree.gfilter1.
+                rewrite H.
+                reflexivity.
+              }
+      apply In_nth_error in IN.
+      destruct IN as [n IN].
+      econstructor; split.
+      * eapply plus_two.
+        ++ eapply exec_Icond with (cond := cond) (args := args) (predb := predb) (b := true).
+           unfold transf_function. simpl.
+           erewrite inject_l_injected_pc with (cond := cond) (args := args).
+           ** reflexivity.
+           ** eassumption.
+           ** unfold gen_conditions.
+              rewrite forallb_forall.
+              intros x INx.
+              rewrite in_map_iff in INx.
+              destruct INx as [[x' i'] [EQ INx]].
+              simpl in EQ.
+              subst x'.
+              apply PTree.elements_complete in INx.
+              rewrite PTree.gfilter1 in INx.
+              assert (x <= max_pc_function f) as MAX.
+              { destruct ((fn_code f) ! x) eqn:CODEx.
+                2: discriminate.
+                apply max_pc_function_sound with (i:=i).
+                assumption.
+              }
+              rewrite Pos.ltb_lt.
+              lia.
+           ** unfold gen_conditions.
+              apply PTree.elements_keys_norepet.
+           ** exact IN.
+           ** assumption.
+           ** reflexivity.
+        ++ apply exec_Ibuiltin with (ef :=  (EF_profiling (branch_id (function_id f) pc) 1%Z)) (args := nil) (vargs := nil).
+           apply inject_l_injected1 with (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot) (expected := predb).
+           ** exact H.
+           ** unfold gen_conditions.
+              rewrite forallb_forall.
+              intros x INx.
+              rewrite in_map_iff in INx.
+              destruct INx as [[x' i'] [EQ INx]].
+              simpl in EQ.
+              subst x'.
+              apply PTree.elements_complete in INx.
+              rewrite PTree.gfilter1 in INx.
+              assert (x <= max_pc_function f) as MAX.
+              { destruct ((fn_code f) ! x) eqn:CODEx.
+                2: discriminate.
+                apply max_pc_function_sound with (i:=i).
+                assumption.
+              }
+              rewrite Pos.ltb_lt.
+              lia.
+           ** unfold gen_conditions.
+              apply PTree.elements_keys_norepet.
+           ** exact IN.
+           ** constructor.
+           ** constructor.
+        ++ reflexivity.
+      * simpl. constructor; auto.
+        
+    + assert (In pc (gen_conditions (fn_code f))) as IN.
+              { unfold gen_conditions.
+                rewrite in_map_iff.
+                exists (pc,  (Icond cond args ifso ifnot predb)).
+                split; simpl; trivial.
+                apply PTree.elements_correct.
+                rewrite PTree.gfilter1.
+                rewrite H.
+                reflexivity.
+              }
+      apply In_nth_error in IN.
+      destruct IN as [n IN].
+      econstructor; split.
+      * eapply plus_two.
+        ++ eapply exec_Icond with (cond := cond) (args := args) (predb := predb) (b := false).
+           unfold transf_function. simpl.
+           erewrite inject_l_injected_pc with (cond := cond) (args := args).
+           ** reflexivity.
+           ** eassumption.
+           ** unfold gen_conditions.
+              rewrite forallb_forall.
+              intros x INx.
+              rewrite in_map_iff in INx.
+              destruct INx as [[x' i'] [EQ INx]].
+              simpl in EQ.
+              subst x'.
+              apply PTree.elements_complete in INx.
+              rewrite PTree.gfilter1 in INx.
+              assert (x <= max_pc_function f) as MAX.
+              { destruct ((fn_code f) ! x) eqn:CODEx.
+                2: discriminate.
+                apply max_pc_function_sound with (i:=i).
+                assumption.
+              }
+              rewrite Pos.ltb_lt.
+              lia.
+           ** unfold gen_conditions.
+              apply PTree.elements_keys_norepet.
+           ** exact IN.
+           ** assumption.
+           ** reflexivity.
+        ++ apply exec_Ibuiltin with (ef :=  (EF_profiling (branch_id (function_id f) pc) 0%Z)) (args := nil) (vargs := nil).
+           apply inject_l_injected0 with (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot) (expected := predb).
+           ** exact H.
+           ** unfold gen_conditions.
+              rewrite forallb_forall.
+              intros x INx.
+              rewrite in_map_iff in INx.
+              destruct INx as [[x' i'] [EQ INx]].
+              simpl in EQ.
+              subst x'.
+              apply PTree.elements_complete in INx.
+              rewrite PTree.gfilter1 in INx.
+              assert (x <= max_pc_function f) as MAX.
+              { destruct ((fn_code f) ! x) eqn:CODEx.
+                2: discriminate.
+                apply max_pc_function_sound with (i:=i).
+                assumption.
+              }
+              rewrite Pos.ltb_lt.
+              lia.
+           ** unfold gen_conditions.
+              apply PTree.elements_keys_norepet.
+           ** exact IN.
+           ** constructor.
+           ** constructor.
+        ++ reflexivity.
+      * simpl. constructor; auto.
+        
+  - econstructor; split.
+    + apply plus_one.
+      apply exec_Ijumptable with (arg:=arg) (tbl:=tbl) (n:=n).
+      erewrite transf_function_at; eauto. apply I.
+      all: eauto with profiling.
+    + constructor; auto.
+  - econstructor; split.
+    + apply plus_one.
+      apply exec_Ireturn.
+      erewrite transf_function_at; eauto. apply I.
+      rewrite stacksize_preserved. eassumption.
+    + constructor; auto.
+  - econstructor; split.
+    + apply plus_one. apply exec_function_internal.
+      rewrite stacksize_preserved. eassumption.
+    + constructor; auto.
+  - econstructor; split.
+    + apply plus_one. apply exec_function_external.
+      eauto with profiling.
+    + constructor; auto.
+  - inv STACKS. inv H1.
+    econstructor; split.
+    + apply plus_one. apply exec_return.
+    + constructor; auto.
+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. inv H. econstructor; split.
+  econstructor.
+    eapply (Genv.init_mem_transf TRANSL); eauto.
+    rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto.
+    eapply function_ptr_translated; eauto.
+    rewrite <- H3; apply sig_preserved.
+  constructor. constructor.
+Qed.
+
+Lemma transf_final_states:
+  forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
+Proof.
+  eapply forward_simulation_plus.
+  apply senv_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact step_simulation.
+Qed.
+
+End PRESERVATION.