From d85a8eb3d89ecb0ff5d7894b26a3497cd9fd7155 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 26 Jan 2021 14:46:37 +0100
Subject: Code simplification of get_path_map (no functionality change)

---
 scheduling/RTLpathLivegenaux.ml | 30 ++++++++++++++++--------------
 1 file changed, 16 insertions(+), 14 deletions(-)

diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml
index ab921954..d415c115 100644
--- a/scheduling/RTLpathLivegenaux.ml
+++ b/scheduling/RTLpathLivegenaux.ml
@@ -82,13 +82,15 @@ let get_path_map code entry join_points =
   let visited = ref (PTree.map (fun n i -> false) code) in
   let path_map = ref PTree.empty in
   let rec dig_path e =
-    let psize = ref (-1) in
-    let path_successors = ref [] in
-    let rec dig_path_rec n : (path_info * node list) option =
-      if not (get_some @@ PTree.get n !visited) then 
+    if (get_some @@ PTree.get e !visited) then
+      ()
+    else begin
+      visited := PTree.set e true !visited;
+      let psize = ref (-1) in
+      let path_successors = ref [] in
+      let rec dig_path_rec n : (path_info * node list) option =
         let inst = get_some @@ PTree.get n code in
         begin
-          visited := PTree.set n true !visited;
           psize := !psize + 1;
           let successor = match predicted_successor inst with
           | None -> None
@@ -102,15 +104,15 @@ let get_path_map code entry join_points =
                             input_regs = Regset.empty; output_regs = Regset.empty },
                         !path_successors @ successors_inst inst)
         end
-      else None
-    in match dig_path_rec e with
-    | None -> ()
-    | Some ret ->
-        let (path_info, succs) = ret in
-        begin
-          path_map := PTree.set e path_info !path_map;
-          List.iter dig_path succs
-        end
+      in match dig_path_rec e with
+      | None -> ()
+      | Some ret ->
+          let (path_info, succs) = ret in
+          begin
+            path_map := PTree.set e path_info !path_map;
+            List.iter dig_path succs
+          end
+    end
   in begin
     dig_path entry;
     !path_map
-- 
cgit 


From 67cfb5b65007aedbcadbdc92d1bc6507c7187858 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Mon, 29 Mar 2021 16:17:31 +0200
Subject: Simplifications on Linearize - details below

While I was developing the new trace linearize, I started off with
implementing a big algorithm reasoning on dependencies etc.., but I
realized later that it was giving a too different performance (sometimes
better, sometimes worst) than the original CompCert. So I
stripped it off gradually until its performance (on regular code with
just branch prediction) was on par with the base Linearize of CompCert.

I was aiming here for something that is either equal, or better, in
terms of performance.

My (then and current) theory is that I have stripped it out so much that
now it's just like the algorithm of CompCert, but with a modification
for Lcond instructions (see the new linearize_aux_cb). However, I never
tested that theory: the code worked, so I left it as is, without any
simplification. But now that I need to get a clear version for my
manuscript, I'm digging into it.

It turns out my theory is not really exact.
A difference is that instead of taking the minpc across the chain, I take
the pc of the very first block of the chain I create. This was (I think)
out of laziness in the middle of two iterations, except that I forgot
about it.

I tested my new theory by deleting all the stuff about dependencies
calculation (commited), and also computing a minpc just like original
compcert (not commited): I get the same exact Mach code than
linearize_aux_cb.

So right now, the only difference between linearize_aux_cb and
linearize_aux_trace is that slightly different minpc computation.

I think transitionning to linearize_aux_cb will be 1) much clearer than
this Frankenstein monster of linearize_aux_trace that I made, and 2)
might be better performing too.

I don't have access to Kalray machines today so i'm leaving this on hold
for now, but tomorrow I will test performance wise to see if there is a
regression. If there isn't, I will commit this (and it will be the
version narrated by my manuscript).

If there is a regression, it would mean selecting the pc of the first
node (in opposition to the minpc) is more performant, so i'd backtrack
the change to linearize_aux_cb anyway and there should then be 0
difference in the generated code.
---
 backend/Linearizeaux.ml | 284 ++++++++++++++----------------------------------
 1 file changed, 79 insertions(+), 205 deletions(-)

diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 3f1a8b6e..402e376d 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -128,6 +128,68 @@ let enumerate_aux_flat f reach =
  * heuristic
  *)
 
+let super_blocks f joins =
+  let blocks = ref [] in
+  let visited = ref IntSet.empty in
+  (* start_block:
+       pc is the function entry point
+          or a join point
+          or the successor of a conditional test *)
+  let rec start_block pc =
+    let npc = P.to_int pc in
+    if not (IntSet.mem npc !visited) then begin
+      visited := IntSet.add npc !visited;
+      in_block [] max_int pc
+    end
+  (* in_block: add pc to block and check successors *)
+  and in_block blk minpc pc =
+    let npc = P.to_int pc in
+    let blk = pc :: blk in
+    let minpc = min npc minpc in
+    match PTree.get pc f.fn_code with
+    | None -> assert false
+    | Some b ->
+       let rec do_instr_list = function
+       | [] -> assert false
+       | Lbranch s :: _ -> next_in_block blk minpc s
+       | Ltailcall (sig0, ros) :: _ -> end_block blk minpc
+       | Lcond (cond, args, ifso, ifnot, pred) :: _ -> begin
+            match pred with
+            | None -> (end_block blk minpc; start_block ifso; start_block ifnot)
+            | Some true -> (next_in_block blk minpc ifso; start_block ifnot)
+            | Some false -> (next_in_block blk minpc ifnot; start_block ifso)
+          end
+       | Ljumptable(arg, tbl) :: _ ->
+             end_block blk minpc; List.iter start_block tbl
+       | Lreturn :: _ -> end_block blk minpc
+       | instr :: b' -> do_instr_list b' in
+       do_instr_list b
+  (* next_in_block: check if join point and either extend block
+     or start block *)
+  and next_in_block blk minpc pc =
+    let npc = P.to_int pc in
+    if IntSet.mem npc joins
+    then (end_block blk minpc; start_block pc)
+    else in_block blk minpc pc
+  (* end_block: record block that we just discovered *)
+  and end_block blk minpc =
+    blocks := (minpc, List.rev blk) :: !blocks
+  in
+    start_block f.fn_entrypoint; !blocks
+
+(* Build the enumeration *)
+
+let enumerate_aux_sb f reach =
+  flatten_blocks (super_blocks f (join_points f))
+
+(**
+ * Alternate enumeration based on traces as identified by Duplicate.v 
+ *
+ * This is a slight alteration to the above heuristic, ensuring that any
+ * superblock will be contiguous in memory, while still following the original
+ * heuristic
+ *)
+
 let get_some = function
 | None -> failwith "Did not get some"
 | Some thing -> thing
@@ -207,98 +269,6 @@ let forward_sequences code entry =
       in [fs] @ ((f code rem_from_node) @ (f code ln))
   in (f code [entry])
 
-(** Unused code
-module PInt = struct
-  type t = P.t
-  let compare x y = compare (P.to_int x) (P.to_int y)
-end
-
-module PSet = Set.Make(PInt)
-
-module LPInt = struct
-  type t = P.t list
-  let rec compare x y =
-    match x with
-    | [] -> ( match y with
-      | [] -> 0
-      | _ -> 1 )
-    | e :: l -> match y with
-      | [] -> -1
-      | e' :: l' ->
-          let e_cmp = PInt.compare e e' in
-          if e_cmp == 0 then compare l l' else e_cmp
-end
-
-module LPSet = Set.Make(LPInt)
-
-let iter_lpset f s = Seq.iter f (LPSet.to_seq s)
-
-let first_of = function
-  | [] -> None
-  | e :: l -> Some e
-
-let rec last_of = function
-  | [] -> None
-  | e :: l -> (match l with [] -> Some e | e :: l -> last_of l)
-
-let can_be_merged code s s' =
-  let last_s = get_some @@ last_of s in
-  let first_s' = get_some @@ first_of s' in
-  match get_some @@ PTree.get last_s code with
-  | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
-  | Lbuiltin _ | Ltailcall _ | Lreturn -> false
-  | Lbranch n -> n == first_s'
-  | Lcond (_, _, ifso, ifnot, info) -> (match info with
-    | None -> false
-    | Some false -> ifnot == first_s'
-    | Some true -> failwith "Inconsistency detected - ifnot is not the preferred branch")
-  | Ljumptable (_, ln) ->
-      match ln with
-      | [] -> false
-      | n :: ln -> n == first_s'
-
-let merge s s' = Some s
-
-let try_merge code (fs: (BinNums.positive list) list) =
-  let seqs = ref (LPSet.of_list fs) in
-  let oldLength = ref (LPSet.cardinal !seqs) in
-  let continue = ref true in
-  let found = ref false in
-  while !continue do
-    begin
-      found := false;
-      iter_lpset (fun s ->
-        if !found then ()
-        else iter_lpset (fun s' ->
-          if (!found || s == s') then ()
-          else if (can_be_merged code s s') then
-            begin
-              seqs := LPSet.remove s !seqs;
-              seqs := LPSet.remove s' !seqs;
-              seqs := LPSet.add (get_some (merge s s')) !seqs;
-              found := true;
-            end
-          else ()
-        ) !seqs
-      ) !seqs;
-      if !oldLength == LPSet.cardinal !seqs then
-        continue := false
-      else
-        oldLength := LPSet.cardinal !seqs
-    end
-  done;
-  !seqs
-*)
-
-(** Code adapted from Duplicateaux.get_loop_headers
-  *
-  * Getting loop branches with a DFS visit :
-  * Each node is either Unvisited, Visited, or Processed
-  * pre-order: node becomes Processed
-  * post-order: node becomes Visited
-  *
-  * If we come accross an edge to a Processed node, it's a loop!
-  *)
 type pos = BinNums.positive
 
 module PP = struct
@@ -315,38 +285,6 @@ module PPMap = Map.Make(PP)
 
 type vstate = Unvisited | Processed | Visited
 
-let get_loop_edges code entry =
-  let visited = ref (PTree.map (fun n i -> Unvisited) code) in
-  let is_loop_edge = ref PPMap.empty
-  in let rec dfs_visit code from = function
-  | [] -> ()
-  | node :: ln ->
-      match (get_some @@ PTree.get node !visited) with
-      | Visited -> ()
-      | Processed -> begin
-          let from_node = get_some from in
-          is_loop_edge := PPMap.add (from_node, node) true !is_loop_edge;
-          visited := PTree.set node Visited !visited
-        end
-      | Unvisited -> begin
-          visited := PTree.set node Processed !visited;
-          let bb = get_some @@ PTree.get node code in
-          let next_visits = (match (last_element bb) with
-          | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
-          | Lbuiltin _ -> assert false
-          | Ltailcall _ | Lreturn -> []
-          | Lbranch n -> [n]
-          | Lcond (_, _, ifso, ifnot, _) -> [ifso; ifnot]
-          | Ljumptable(_, ln) -> ln
-          ) in dfs_visit code (Some node) next_visits;
-          visited := PTree.set node Visited !visited;
-          dfs_visit code from ln
-        end
-  in begin
-    dfs_visit code None [entry];
-    !is_loop_edge
-  end
-
 let ppmap_is_true pp ppmap = PPMap.mem pp ppmap && PPMap.find pp ppmap
 
 module Int = struct
@@ -364,70 +302,6 @@ let print_iset s = begin
   end
 end
 
-let print_depmap dm = begin
-  if !debug_flag then begin
-    Printf.printf "[|";
-    Array.iter (fun s -> print_iset s; Printf.printf ", ") dm;
-    Printf.printf "|]\n"
-  end
-end
-
-let construct_depmap code entry fs =
-  let is_loop_edge = get_loop_edges code entry in
-  let visited = ref (PTree.map (fun n i -> false) code) in
-  let depmap = Array.map (fun e -> ISet.empty) fs in
-  let find_index_of_node n =
-    let index = ref 0 in
-    begin
-      Array.iteri (fun i s ->
-        match List.find_opt (fun e -> e == n) s with
-        | Some _ -> index := i
-        | None -> ()
-      ) fs;
-      !index
-    end
-  in let check_and_update_depmap from target =
-    (* debug "From %d to %d\n" (P.to_int from) (P.to_int target); *)
-    if not (ppmap_is_true (from, target) is_loop_edge) then
-      let in_index_fs = find_index_of_node from in
-      let out_index_fs = find_index_of_node target in
-      if out_index_fs != in_index_fs then
-        depmap.(out_index_fs) <- ISet.add in_index_fs depmap.(out_index_fs)
-      else ()
-    else ()
-  in let rec dfs_visit code = function
-  | [] -> ()
-  | node :: ln ->
-      begin
-        match (get_some @@ PTree.get node !visited) with
-        | true -> ()
-        | false -> begin
-            visited := PTree.set node true !visited;
-            let bb = get_some @@ PTree.get node code in
-            let next_visits =
-              match (last_element bb) with
-              | Ltailcall _ | Lreturn -> []
-              | Lbranch n -> (check_and_update_depmap node n; [n])
-              | Lcond (_, _, ifso, ifnot, _) -> begin
-                  check_and_update_depmap node ifso;
-                  check_and_update_depmap node ifnot;
-                  [ifso; ifnot]
-                end
-              | Ljumptable(_, ln) -> begin
-                  List.iter (fun n -> check_and_update_depmap node n) ln;
-                  ln
-                end
-              (* end of bblocks should not be another value than one of the above *)
-              | _ -> failwith "last_element gave an invalid output"
-            in dfs_visit code next_visits
-          end;
-        dfs_visit code ln
-      end
-  in begin
-    dfs_visit code [entry];
-    depmap
-  end
-
 let print_sequence s =
   if !debug_flag then begin
     Printf.printf "[";
@@ -442,23 +316,26 @@ let print_ssequence ofs =
     Printf.printf "]\n"
   end
 
+let rec minpc_of l =
+  match l with
+  | [] -> None
+  | e::l -> begin
+        let e_score = P.to_int e in
+        let mpc = minpc_of l in 
+        match mpc with
+        | None -> Some e_score
+        | Some e_score' -> if e_score < e_score' then Some e_score else Some e_score'
+      end
+
 let order_sequences code entry fs =
   let fs_a = Array.of_list fs in
-  let depmap = construct_depmap code entry fs_a in
   let fs_evaluated = Array.map (fun e -> false) fs_a in
   let ordered_fs = ref [] in
   let evaluate s_id =
     begin
       assert (not fs_evaluated.(s_id));
       ordered_fs := fs_a.(s_id) :: !ordered_fs;
-      fs_evaluated.(s_id) <- true;
-      (* debug "++++++\n";
-      debug "Scheduling %d\n" s_id;
-      debug "Initial depmap: "; print_depmap depmap; *)
-      Array.iteri (fun i deps ->
-        depmap.(i) <- ISet.remove s_id deps
-      ) depmap;
-      (* debug "Final depmap: "; print_depmap depmap; *)
+      fs_evaluated.(s_id) <- true
     end
   in let choose_best_of candidates =
     let current_best_id = ref None in
@@ -486,24 +363,21 @@ let order_sequences code entry fs =
   in let select_next () =
     let candidates = ref [] in
     begin
-      Array.iteri (fun i deps ->
+      Array.iteri (fun i _ ->
         begin
-          (* debug "Deps of %d: " i; print_iset deps; debug "\n"; *)
-          (* FIXME - if we keep it that way (no dependency check), remove all the unneeded stuff *)
-          if ((* deps == ISet.empty && *) not fs_evaluated.(i)) then
+          if (not fs_evaluated.(i)) then
             candidates := i :: !candidates
         end
-      ) depmap;
+      ) fs_a;
       if not (List.length !candidates > 0) then begin
-        Array.iteri (fun i deps ->
+        Array.iteri (fun i _ ->
           if (not fs_evaluated.(i)) then candidates := i :: !candidates
-        ) depmap;
+        ) fs_a;
       end;
       get_some (choose_best_of !candidates)
     end
   in begin
     debug "-------------------------------\n";
-    debug "depmap: "; print_depmap depmap;
     debug "forward sequences identified: "; print_ssequence fs;
     while List.length !ordered_fs != List.length fs do
       let next_id = select_next () in
-- 
cgit 


From f7365bc7d9b0eabc8fa06cafddad1b17ed01584a Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 30 Mar 2021 15:14:06 +0200
Subject: Simplification of the Linearize heuristic (same result functionally)

---
 backend/Linearizeaux.ml | 222 ++----------------------------------------------
 1 file changed, 6 insertions(+), 216 deletions(-)

diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 402e376d..5914f6a3 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -126,6 +126,10 @@ let enumerate_aux_flat f reach =
  * This is a slight alteration to the above heuristic, ensuring that any
  * superblock will be contiguous in memory, while still following the original
  * heuristic
+ *
+ * Slight change: instead of taking the minimum pc of the superblock, we just take
+ * the pc of the first block.
+ * (experimentally this leads to slightly better performance..)
  *)
 
 let super_blocks f joins =
@@ -139,13 +143,11 @@ let super_blocks f joins =
     let npc = P.to_int pc in
     if not (IntSet.mem npc !visited) then begin
       visited := IntSet.add npc !visited;
-      in_block [] max_int pc
+      in_block [] npc pc
     end
   (* in_block: add pc to block and check successors *)
   and in_block blk minpc pc =
-    let npc = P.to_int pc in
     let blk = pc :: blk in
-    let minpc = min npc minpc in
     match PTree.get pc f.fn_code with
     | None -> assert false
     | Some b ->
@@ -182,218 +184,6 @@ let super_blocks f joins =
 let enumerate_aux_sb f reach =
   flatten_blocks (super_blocks f (join_points f))
 
-(**
- * Alternate enumeration based on traces as identified by Duplicate.v 
- *
- * This is a slight alteration to the above heuristic, ensuring that any
- * superblock will be contiguous in memory, while still following the original
- * heuristic
- *)
-
-let get_some = function
-| None -> failwith "Did not get some"
-| Some thing -> thing
-
-exception EmptyList
-
-let rec last_element = function
-  | [] -> raise EmptyList
-  | e :: [] -> e
-  | e' :: e :: l -> last_element (e::l)
-
-let print_plist l =
-  let rec f = function
-  | [] -> ()
-  | n :: l -> Printf.printf "%d, " (P.to_int n); f l
-  in begin
-    if !debug_flag then begin
-      Printf.printf "[";
-      f l;
-      Printf.printf "]"
-    end
-  end
-
-(* adapted from the above join_points function, but with PTree *)
-let get_join_points code entry =
-  let reached = ref (PTree.map (fun n i -> false) code) in
-  let reached_twice = ref (PTree.map (fun n i -> false) code) in
-  let rec traverse pc =
-    if get_some @@ PTree.get pc !reached then begin
-      if not (get_some @@ PTree.get pc !reached_twice) then
-        reached_twice := PTree.set pc true !reached_twice
-    end else begin
-      reached := PTree.set pc true !reached;
-      traverse_succs (successors_block @@ get_some @@ PTree.get pc code)
-    end
-  and traverse_succs = function
-    | [] -> ()
-    | [pc] -> traverse pc
-    | pc :: l -> traverse pc; traverse_succs l
-  in traverse entry; !reached_twice
-
-let forward_sequences code entry =
-  let visited = ref (PTree.map (fun n i -> false) code) in
-  let join_points = get_join_points code entry in
-  (* returns the list of traversed nodes, and a list of nodes to start traversing next *)
-  let rec traverse_fallthrough code node =
-    (* debug "Traversing %d..\n" (P.to_int node); *)
-    if not (get_some @@ PTree.get node !visited) then begin
-      visited := PTree.set node true !visited;
-      match PTree.get node code with
-      | None -> failwith "No such node"
-      | Some bb ->
-          let ln, rem = match (last_element bb) with
-          | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
-          | Lbuiltin _ -> assert false
-          | Ltailcall _ | Lreturn -> begin (* debug "STOP tailcall/return\n"; *) ([], []) end
-          | Lbranch n ->
-              if get_some @@ PTree.get n join_points then ([], [n])
-              else let ln, rem = traverse_fallthrough code n in (ln, rem)
-          | Lcond (_, _, ifso, ifnot, info) -> (match info with
-            | None -> begin (* debug "STOP Lcond None\n"; *) ([], [ifso; ifnot]) end
-            | Some false ->
-                if get_some @@ PTree.get ifnot join_points then ([], [ifso; ifnot])
-                else let ln, rem = traverse_fallthrough code ifnot in (ln, [ifso] @ rem)
-            | Some true ->
-                if get_some @@ PTree.get ifso join_points then ([], [ifso; ifnot])
-                else let ln, rem = traverse_fallthrough code ifso in (ln, [ifnot] @ rem)
-            )
-          | Ljumptable(_, ln) -> begin (* debug "STOP Ljumptable\n"; *) ([], ln) end
-          in ([node] @ ln, rem)
-      end
-    else ([], [])
-  in let rec f code = function
-  | [] -> []
-  | node :: ln ->
-      let fs, rem_from_node = traverse_fallthrough code node
-      in [fs] @ ((f code rem_from_node) @ (f code ln))
-  in (f code [entry])
-
-type pos = BinNums.positive
-
-module PP = struct
-  type t = pos * pos
-  let compare a b =
-    let ax, ay = a in
-    let bx, by = b in
-    let dx = compare ax bx in
-    if (dx == 0) then compare ay by
-    else dx
-end
-
-module PPMap = Map.Make(PP)
-
-type vstate = Unvisited | Processed | Visited
-
-let ppmap_is_true pp ppmap = PPMap.mem pp ppmap && PPMap.find pp ppmap
-
-module Int = struct
-  type t = int
-  let compare x y = compare x y
-end
-
-module ISet = Set.Make(Int)
-
-let print_iset s = begin
-  if !debug_flag then begin
-    Printf.printf "{";
-    ISet.iter (fun e -> Printf.printf "%d, " e) s;
-    Printf.printf "}"
-  end
-end
-
-let print_sequence s =
-  if !debug_flag then begin
-    Printf.printf "[";
-    List.iter (fun n -> Printf.printf "%d, " (P.to_int n)) s;
-    Printf.printf "]\n"
-  end
-
-let print_ssequence ofs =
-  if !debug_flag then begin
-    Printf.printf "[";
-    List.iter (fun s -> print_sequence s) ofs;
-    Printf.printf "]\n"
-  end
-
-let rec minpc_of l =
-  match l with
-  | [] -> None
-  | e::l -> begin
-        let e_score = P.to_int e in
-        let mpc = minpc_of l in 
-        match mpc with
-        | None -> Some e_score
-        | Some e_score' -> if e_score < e_score' then Some e_score else Some e_score'
-      end
-
-let order_sequences code entry fs =
-  let fs_a = Array.of_list fs in
-  let fs_evaluated = Array.map (fun e -> false) fs_a in
-  let ordered_fs = ref [] in
-  let evaluate s_id =
-    begin
-      assert (not fs_evaluated.(s_id));
-      ordered_fs := fs_a.(s_id) :: !ordered_fs;
-      fs_evaluated.(s_id) <- true
-    end
-  in let choose_best_of candidates =
-    let current_best_id = ref None in
-    let current_best_score = ref None in
-    begin
-      List.iter (fun id ->
-        match !current_best_id with
-        | None -> begin
-            current_best_id := Some id;
-            match fs_a.(id) with
-            | [] -> current_best_score := None
-            | n::l -> current_best_score := Some (P.to_int n)
-          end
-        | Some b -> begin
-            match fs_a.(id) with
-            | [] -> ()
-            | n::l -> let nscore = P.to_int n in
-              match !current_best_score with
-              | None -> (current_best_id := Some id; current_best_score := Some nscore)
-              | Some bs -> if nscore > bs then (current_best_id := Some id; current_best_score := Some nscore)
-          end
-      ) candidates;
-      !current_best_id
-    end
-  in let select_next () =
-    let candidates = ref [] in
-    begin
-      Array.iteri (fun i _ ->
-        begin
-          if (not fs_evaluated.(i)) then
-            candidates := i :: !candidates
-        end
-      ) fs_a;
-      if not (List.length !candidates > 0) then begin
-        Array.iteri (fun i _ ->
-          if (not fs_evaluated.(i)) then candidates := i :: !candidates
-        ) fs_a;
-      end;
-      get_some (choose_best_of !candidates)
-    end
-  in begin
-    debug "-------------------------------\n";
-    debug "forward sequences identified: "; print_ssequence fs;
-    while List.length !ordered_fs != List.length fs do
-      let next_id = select_next () in
-      evaluate next_id
-    done;
-    debug "forward sequences ordered: "; print_ssequence (List.rev (!ordered_fs));
-    List.rev (!ordered_fs)
-  end
-
-let enumerate_aux_trace f reach =
-  let code = f.fn_code in
-  let entry = f.fn_entrypoint in
-  let fs = forward_sequences code entry in
-  let ofs = order_sequences code entry fs in
-  List.flatten ofs
-
 let enumerate_aux f reach =
-  if !Clflags.option_ftracelinearize then enumerate_aux_trace f reach
+  if !Clflags.option_ftracelinearize then enumerate_aux_sb f reach
   else enumerate_aux_flat f reach
-- 
cgit 


From fe7a71c232068bc57e7e14935ff443a4a6315dac Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Wed, 31 Mar 2021 11:34:55 +0200
Subject: Big simplification of get_loop_info

Another remnant of trying to devise a complicated algorithm for a
problem that was, in fact, very simple: I just had to check whether the
branch was within the loop body.

I tested it functionally on the benchmarks: only heapsort is changed, in
slightly worst (4-5%), because the old get_loop_info had done a buggy
guess that proved to be lucky for that particular case.

The other benchmarks are unchanged: the predictions stay the exact same.

The get_loop_info could potentially be improved by having a natural loop
detection that extends to outer loops (not just inner loops), though I
expect the performance improvements would be very small.
---
 backend/Duplicateaux.ml | 127 ++++++------------------------------------------
 1 file changed, 16 insertions(+), 111 deletions(-)

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index b3635527..7504f724 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -270,120 +270,25 @@ let get_inner_loops f code is_loop_header =
     ) (PTree.elements loopmap)
   end
 
-
-(* Returns a PTree of either None or Some b where b determines the node following the loop, for a cb instruction *)
-(* It uses the fact that loops in CompCert are done by a branch (backedge) instruction followed by a cb *)
+(* Returns a PTree of either None or Some b where b determines the node in the loop body, for a cb instruction *)
 let get_loop_info f is_loop_header bfs_order code =
-  debug "GET LOOP INFO\n";
-  debug "==================================\n";
   let loop_info = ref (PTree.map (fun n i -> None) code) in
-  let mark_path n lbody =
-    let cb_info = ref PTree.empty in
-    let visited = ref (PTree.map (fun n i -> false) code) in
-    (* Returns true if there is a path from src to dest (not involving jumptables) *)
-    (* Mark nodes as visited along the way *)
-    let explore src dest =
-      debug "Trying to dive a path from %d to %d\n" (P.to_int src) (P.to_int dest);
-      (* Memoizing the results to avoid exponential blow-up *)
-      let memory = ref PTree.empty in
-      let rec explore_rec src =
-        debug "explore_rec %d vs %d... " (P.to_int src) (P.to_int dest);
-        if (P.to_int src) == (P.to_int dest) then (debug "FOUND\n"; true)
-        else if (get_some @@ PTree.get src !visited) then (debug "VISITED... :( \n"; false)
-        (* if we went out of the innermost loop *)
-        else if (not @@ List.mem src lbody) then (debug "Out of innermost...\n"; false)
-        else begin
-          let inst = get_some @@ PTree.get src code in
-          visited := PTree.set src true !visited;
-          match rtl_successors inst with
-          | [] -> false
-          | [s] -> explore_wrap s
-          | [s1; s2] -> let snapshot_visited = ref !visited in begin
-              debug "\t\tSplit at %d: either %d or %d\n" (P.to_int src) (P.to_int s1) (P.to_int s2);
-              (* Remembering that we tried the ifso node *)
-              cb_info := PTree.set src true !cb_info;
-              match explore_wrap s1 with
-              | true -> (
-                  visited := !snapshot_visited;
-                  match explore_wrap s2 with
-                  | true -> begin
-                      (* Both paths lead to a loop: we cannot predict the CB
-                       * (but the explore still succeeds) *)
-                      cb_info := PTree.remove src !cb_info;
-                      true
-                    end
-                  | false -> true (* nothing to do, the explore succeeded *)
-                )
-              | false -> begin
-                  cb_info := PTree.set src false !cb_info;
-                  match explore_wrap s2 with
-                  | true -> true
-                  | false -> (cb_info := PTree.remove src !cb_info; false)
-                end
-            end
-          | _ -> false
-        end
-      and explore_wrap src = begin
-        match PTree.get src !memory with
-        | Some b -> b
-        | None ->
-            let result = explore_rec src in
-            (memory := PTree.set src result !memory; result)
-      end in explore_wrap src
-    (* Goes forward until a CB is encountered
-     * Returns None if no CB was found, or Some the_cb_node
-     * Marks nodes as visited along the way *)
-    in let rec advance_to_cb src =
-      if (get_some @@ PTree.get src !visited) then None
-      else begin
-        visited := PTree.set src true !visited;
-        match get_some @@ PTree.get src code with
-        | Inop s | Iop (_, _, _, s) | Iload (_,_,_,_,_,s) | Istore (_,_,_,_,s) | Icall (_,_,_,_,s)
-        | Ibuiltin (_,_,_,s) -> advance_to_cb s
-        | Icond _ -> Some src
-        | Ijumptable _ | Itailcall _ | Ireturn _ -> None
-      end
-    in begin
-      debug "Attempting to find natural loop from HEAD %d..\n" (P.to_int n);
-      match advance_to_cb n with
-      | None -> (debug "\tNo CB found\n")
-      | Some s -> ( debug "\tFound a CB! %d\n" (P.to_int s);
-          match get_some @@ PTree.get s !loop_info with
-          | None | Some _ -> begin
-              match get_some @@ PTree.get s code with
-              | Icond (_, _, n1, n2, _) -> (
-                  let b1 = explore n1 n in
-                  let b2 = explore n2 n in
-                  if (b1 && b2) then 
-                    debug "\tBoth paths lead back to the head: NONE\n"
-                  else if (b1 || b2) then begin
-                    if b1 then begin 
-                      debug "\tTrue path leads to the head: TRUE\n"; 
-                      loop_info := PTree.set s (Some true) !loop_info;
-                    end else if b2 then begin
-                      debug "\tFalse path leads to the head: FALSE\n";
-                      loop_info := PTree.set s (Some false) !loop_info
-                    end;
-                    debug "\tSetting other CBs encountered..\n";
-                    List.iter (fun (cb, dir) ->
-                      debug "\t\t%d is %B\n" (P.to_int cb) dir;
-                      loop_info := PTree.set cb (Some dir) !loop_info
-                    ) (PTree.elements !cb_info)
-                  end else
-                    debug "\tNo path leads back to the head: NONE\n"
-                )
-              | _ -> failwith "\tNot an Icond\n"
-            end
-          (* | Some _ -> ( debug "already loop info there\n" ) FIXME - we don't know yet whether a branch to a loop head is a backedge or not *)
-        )
-    end
+  let mark_iloop iloop =
+    List.iter (fun n ->
+      match get_some @@ PTree.get n code with
+      | Icond (_, _, ifso, ifnot, _) ->
+          let b1 = List.mem ifso iloop.body in
+          let b2 = List.mem ifnot iloop.body in
+          if (b1 && b2) then ()
+          else if (b1 || b2) then begin
+            if b1 then loop_info := PTree.set n (Some true) !loop_info
+            else if b2 then loop_info := PTree.set n (Some false) !loop_info
+          end
+      | _ -> ()
+    ) iloop.body
   in let iloops = get_inner_loops f code is_loop_header in
-  begin
-    List.iter (fun il -> mark_path il.head il.body) iloops;
-    (* List.iter mark_path @@ List.filter (fun n -> get_some @@ PTree.get n is_loop_header) bfs_order; *)
-    debug "==================================\n";
-    !loop_info
-  end
+  List.iter mark_iloop iloops;
+  !loop_info
 
 (* Remark - compared to the original Branch Prediction for Free paper, we don't use the store heuristic *)
 let get_directions f code entrypoint = begin
-- 
cgit 


From 6ee3ecb0edc17d61a515054952827c495cc03979 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Fri, 2 Apr 2021 11:41:41 +0200
Subject: Simple backedge detection (modified code from get_loop_headers)

---
 backend/Duplicateaux.ml |  3 +++
 backend/LICMaux.ml      | 40 ++++++++++++++++++++++++++++++++++++++++
 common/DebugPrint.ml    | 14 ++++++++++++++
 3 files changed, 57 insertions(+)

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 7504f724..625cbdd9 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -928,6 +928,9 @@ let loop_rotate f =
   ((code, entrypoint), revmap)
 
 let static_predict f =
+  debug_flag := true;
+  let _ = LICMaux.get_loop_backedges f.fn_code f.fn_entrypoint in
+  debug_flag := false;
   let entrypoint = f.fn_entrypoint in
   let code = f.fn_code in
   let revmap = make_identity_ptree code in
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml
index 1f6b8817..96e8e8ae 100644
--- a/backend/LICMaux.ml
+++ b/backend/LICMaux.ml
@@ -80,6 +80,46 @@ let get_loop_headers code entrypoint = begin
   end
 end
 
+let get_loop_backedges code entrypoint = begin
+  debug "get_loop_backedges\n";
+  let visited = ref (PTree.map (fun n i -> Unvisited) code)
+  and loop_backedge = ref (PTree.map (fun n i -> None) code)
+  in let rec dfs_visit code origin = function
+  | [] -> ()
+  | node :: ln ->
+      debug "ENTERING node %d, REM are %a\n" (P.to_int node) print_intlist ln;
+      match (get_some @@ PTree.get node !visited) with
+      | Visited -> begin
+          debug "\tNode %d is already Visited, skipping\n" (P.to_int node);
+          dfs_visit code origin ln
+        end
+      | Processed -> begin
+          debug "Node %d is a loop header\n" (P.to_int node);
+          debug "The backedge is from %d\n" (P.to_int @@ get_some origin);
+          loop_backedge := PTree.set node origin !loop_backedge;
+          visited := PTree.set node Visited !visited;
+          dfs_visit code origin ln
+        end
+      | Unvisited -> begin
+          visited := PTree.set node Processed !visited;
+          debug "Node %d is Processed\n" (P.to_int node);
+          (match PTree.get node code with
+          | None -> failwith "No such node"
+          | Some i -> let next_visits = rtl_successors i in begin
+              debug "About to visit: %a\n" print_intlist next_visits;
+              dfs_visit code (Some node) next_visits
+            end);
+          debug "Node %d is Visited!\n" (P.to_int node);
+          visited := PTree.set node Visited !visited;
+          dfs_visit code origin ln
+        end
+  in begin
+    dfs_visit code None [entrypoint];
+    debug "LOOP BACKEDGES: %a\n" print_ptree_opint !loop_backedge;
+    !loop_backedge
+  end
+end
+
 
 module Dominator =
   struct
diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml
index 64efe727..931dfdf4 100644
--- a/common/DebugPrint.ml
+++ b/common/DebugPrint.ml
@@ -20,6 +20,20 @@ let print_ptree_bool oc pt =
     end
   else ()
 
+let print_ptree_opint oc pt =
+  if !debug_flag then
+    let elements = PTree.elements pt in
+    begin
+      Printf.fprintf oc "[";
+      List.iter (fun (n, op) ->
+        match op with
+        | None -> ()
+        | Some p -> Printf.fprintf oc "%d -> %d, " (P.to_int n) (P.to_int p)
+      ) elements;
+      Printf.fprintf oc "]\n"
+    end
+  else ()
+
 let print_intlist oc l =
   let rec f oc = function
   | [] -> ()
-- 
cgit 


From b042bca17696a9cb6e2be7bbdac9f08953fff527 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Fri, 2 Apr 2021 11:44:42 +0200
Subject: get_loop_headers simplification (using the new get_loop_backedges)

---
 backend/LICMaux.ml | 46 +++++++---------------------------------------
 1 file changed, 7 insertions(+), 39 deletions(-)

diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml
index 96e8e8ae..b88dbc2d 100644
--- a/backend/LICMaux.ml
+++ b/backend/LICMaux.ml
@@ -41,45 +41,6 @@ let rtl_successors = function
   *
   * If we come accross an edge to a Processed node, it's a loop!
   *)
-let get_loop_headers code entrypoint = begin
-  debug "get_loop_headers\n";
-  let visited = ref (PTree.map (fun n i -> Unvisited) code)
-  and is_loop_header = ref (PTree.map (fun n i -> false) code)
-  in let rec dfs_visit code = function
-  | [] -> ()
-  | node :: ln ->
-      debug "ENTERING node %d, REM are %a\n" (P.to_int node) print_intlist ln;
-      match (get_some @@ PTree.get node !visited) with
-      | Visited -> begin
-          debug "\tNode %d is already Visited, skipping\n" (P.to_int node);
-          dfs_visit code ln
-        end
-      | Processed -> begin
-          debug "Node %d is a loop header\n" (P.to_int node);
-          is_loop_header := PTree.set node true !is_loop_header;
-          visited := PTree.set node Visited !visited;
-          dfs_visit code ln
-        end
-      | Unvisited -> begin
-          visited := PTree.set node Processed !visited;
-          debug "Node %d is Processed\n" (P.to_int node);
-          (match PTree.get node code with
-          | None -> failwith "No such node"
-          | Some i -> let next_visits = rtl_successors i in begin
-              debug "About to visit: %a\n" print_intlist next_visits;
-              dfs_visit code next_visits
-            end);
-          debug "Node %d is Visited!\n" (P.to_int node);
-          visited := PTree.set node Visited !visited;
-          dfs_visit code ln
-        end
-  in begin
-    dfs_visit code [entrypoint];
-    debug "LOOP HEADERS: %a\n" print_ptree_bool !is_loop_header;
-    !is_loop_header
-  end
-end
-
 let get_loop_backedges code entrypoint = begin
   debug "get_loop_backedges\n";
   let visited = ref (PTree.map (fun n i -> Unvisited) code)
@@ -120,6 +81,13 @@ let get_loop_backedges code entrypoint = begin
   end
 end
 
+let get_loop_headers code entrypoint =
+  let backedges = get_loop_backedges code entrypoint in
+  PTree.map (fun _ ob ->
+    match ob with
+    | None -> false
+    | Some _ -> true
+  ) backedges
 
 module Dominator =
   struct
-- 
cgit 


From a4720c58a97c08b1f8852376c39f15dd44cd0f34 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Fri, 2 Apr 2021 13:06:02 +0200
Subject: Getting all loop bodies

---
 backend/Duplicateaux.ml | 38 ++++++++++++++++++++++++++++++++++++--
 common/DebugPrint.ml    | 14 ++++++++++++++
 2 files changed, 50 insertions(+), 2 deletions(-)

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 625cbdd9..17beb4d0 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -270,6 +270,39 @@ let get_inner_loops f code is_loop_header =
     ) (PTree.elements loopmap)
   end
 
+let get_loop_bodies code entrypoint =
+  let predecessors = get_predecessors_rtl code in
+  (* Algorithm from Muchnik, Compiler Design & Implementation, Figure 7.21 page 192 *)
+  let natural_loop n m =
+    debug "Natural Loop from %d to %d\n" (P.to_int n) (P.to_int m);
+    let in_body = ref (PTree.map (fun n b -> false) code) in
+    let body = ref [] in
+    let add_to_body n = begin
+      in_body := PTree.set n true !in_body;
+      body := n :: !body
+    end
+    in let rec process_node p =
+      debug "    Processing node %d\n" (P.to_int p);
+      List.iter (fun pred ->
+        debug "        Looking at predecessor of %d: %d\n" (P.to_int p) (P.to_int pred);
+        let is_in_body = get_some @@ PTree.get pred !in_body in
+        if (not @@ is_in_body) then begin
+          debug "        --> adding to body\n";
+          add_to_body pred;
+          process_node pred
+        end
+      ) (get_some @@ PTree.get p predecessors)
+    in begin
+      add_to_body m;
+      add_to_body n;
+      (if (m != n) then process_node m);
+      !body
+    end
+  in let option_natural_loop n = function
+    | None -> None
+    | Some m -> Some (natural_loop n m)
+  in PTree.map option_natural_loop (LICMaux.get_loop_backedges code entrypoint)
+
 (* Returns a PTree of either None or Some b where b determines the node in the loop body, for a cb instruction *)
 let get_loop_info f is_loop_header bfs_order code =
   let loop_info = ref (PTree.map (fun n i -> None) code) in
@@ -298,6 +331,7 @@ let get_directions f code entrypoint = begin
   let loop_info = get_loop_info f is_loop_header bfs_order code in
   let directions = ref (PTree.map (fun n i -> None) code) in (* None <=> no predicted direction *)
   begin
+    debug_flag := true;
     (* ptree_printbool is_loop_header; *)
     (* debug "\n"; *)
     List.iter (fun n ->
@@ -325,7 +359,7 @@ let get_directions f code entrypoint = begin
           end
           )
       | _ -> ()
-    ) bfs_order;
+    ) bfs_order; debug_flag := false;
     !directions
   end
 end
@@ -929,7 +963,7 @@ let loop_rotate f =
 
 let static_predict f =
   debug_flag := true;
-  let _ = LICMaux.get_loop_backedges f.fn_code f.fn_entrypoint in
+  Printf.printf "Loop bodies: %a" print_ptree_oplist (get_loop_bodies f.fn_code f.fn_entrypoint);
   debug_flag := false;
   let entrypoint = f.fn_entrypoint in
   let code = f.fn_code in
diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml
index 931dfdf4..f68432d9 100644
--- a/common/DebugPrint.ml
+++ b/common/DebugPrint.ml
@@ -44,6 +44,20 @@ let print_intlist oc l =
     end
   end
 
+let print_ptree_oplist oc pt =
+  if !debug_flag then
+    let elements = PTree.elements pt in
+    begin
+      Printf.fprintf oc "[";
+      List.iter (fun (n, ol) ->
+        match ol with
+        | None -> ()
+        | Some l -> Printf.fprintf oc "%d -> %a,\n" (P.to_int n) print_intlist l
+      ) elements;
+      Printf.fprintf oc "]\n"
+    end
+  else ()
+
 (* Adapted from backend/PrintRTL.ml: print_function *)
 let print_code code = let open PrintRTL in let open Printf in
   if (!debug_flag) then begin
-- 
cgit 


From 6d4dc7ae91e4452332e6f513733135fefd6f7f26 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Fri, 2 Apr 2021 13:14:36 +0200
Subject: Outermost loop detection works

---
 backend/Duplicateaux.ml | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 17beb4d0..e864a370 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -306,21 +306,25 @@ let get_loop_bodies code entrypoint =
 (* Returns a PTree of either None or Some b where b determines the node in the loop body, for a cb instruction *)
 let get_loop_info f is_loop_header bfs_order code =
   let loop_info = ref (PTree.map (fun n i -> None) code) in
-  let mark_iloop iloop =
+  let mark_body body =
     List.iter (fun n ->
       match get_some @@ PTree.get n code with
       | Icond (_, _, ifso, ifnot, _) ->
-          let b1 = List.mem ifso iloop.body in
-          let b2 = List.mem ifnot iloop.body in
+          let b1 = List.mem ifso body in
+          let b2 = List.mem ifnot body in
           if (b1 && b2) then ()
           else if (b1 || b2) then begin
             if b1 then loop_info := PTree.set n (Some true) !loop_info
             else if b2 then loop_info := PTree.set n (Some false) !loop_info
           end
       | _ -> ()
-    ) iloop.body
-  in let iloops = get_inner_loops f code is_loop_header in
-  List.iter mark_iloop iloops;
+    ) body
+  in let bodymap = get_loop_bodies code f.fn_entrypoint in
+  List.iter (fun (_,obody) ->
+    match obody with
+    | None -> ()
+    | Some body -> mark_body body
+    ) (PTree.elements bodymap);
   !loop_info
 
 (* Remark - compared to the original Branch Prediction for Free paper, we don't use the store heuristic *)
@@ -962,9 +966,6 @@ let loop_rotate f =
   ((code, entrypoint), revmap)
 
 let static_predict f =
-  debug_flag := true;
-  Printf.printf "Loop bodies: %a" print_ptree_oplist (get_loop_bodies f.fn_code f.fn_entrypoint);
-  debug_flag := false;
   let entrypoint = f.fn_entrypoint in
   let code = f.fn_code in
   let revmap = make_identity_ptree code in
-- 
cgit 


From b6b7b6a525e4b0b9fd727ef9d52c1901c3308cf0 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Fri, 2 Apr 2021 13:16:12 +0200
Subject: More efficient

---
 backend/Duplicateaux.ml | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index e864a370..4d6e7f3a 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -309,14 +309,18 @@ let get_loop_info f is_loop_header bfs_order code =
   let mark_body body =
     List.iter (fun n ->
       match get_some @@ PTree.get n code with
-      | Icond (_, _, ifso, ifnot, _) ->
-          let b1 = List.mem ifso body in
-          let b2 = List.mem ifnot body in
-          if (b1 && b2) then ()
-          else if (b1 || b2) then begin
-            if b1 then loop_info := PTree.set n (Some true) !loop_info
-            else if b2 then loop_info := PTree.set n (Some false) !loop_info
-          end
+      | Icond (_, _, ifso, ifnot, _) -> begin
+          match PTree.get n !loop_info with
+          | None -> ()
+          | Some _ ->
+              let b1 = List.mem ifso body in
+              let b2 = List.mem ifnot body in
+              if (b1 && b2) then ()
+              else if (b1 || b2) then begin
+                if b1 then loop_info := PTree.set n (Some true) !loop_info
+                else if b2 then loop_info := PTree.set n (Some false) !loop_info
+              end
+        end
       | _ -> ()
     ) body
   in let bodymap = get_loop_bodies code f.fn_entrypoint in
-- 
cgit 


From 294df98be0c67f858355ff1ba08e9ac7a03c4ee2 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Fri, 2 Apr 2021 13:42:46 +0200
Subject: Cleaning

---
 backend/Duplicateaux.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 4d6e7f3a..db150521 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -339,7 +339,6 @@ let get_directions f code entrypoint = begin
   let loop_info = get_loop_info f is_loop_header bfs_order code in
   let directions = ref (PTree.map (fun n i -> None) code) in (* None <=> no predicted direction *)
   begin
-    debug_flag := true;
     (* ptree_printbool is_loop_header; *)
     (* debug "\n"; *)
     List.iter (fun n ->
@@ -367,7 +366,7 @@ let get_directions f code entrypoint = begin
           end
           )
       | _ -> ()
-    ) bfs_order; debug_flag := false;
+    ) bfs_order;
     !directions
   end
 end
-- 
cgit 


From 1ea73601db2afc4ea4f5442ac3dbcdd8e1749c17 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 12 Apr 2021 18:23:13 +0200
Subject: collision of registers

---
 aarch64/Machregs.v       | 2 +-
 aarch64/TargetPrinter.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v
index 3d27f48f..bfe23e83 100644
--- a/aarch64/Machregs.v
+++ b/aarch64/Machregs.v
@@ -158,7 +158,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_memcpy sz al => R15 :: R17 :: R29 :: nil
   | EF_inline_asm txt sg clob => destroyed_by_clobber clob
-  | EF_profiling _ _ => R15 :: R17 :: nil
+  | EF_profiling _ _ => R15 :: R17 :: R29 :: nil
   | _ => nil
   end.
 
diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index 9ec1d563..53959152 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -231,8 +231,8 @@ module Target (*: TARGET*) =
       fprintf oc "%s:\n" lbl;
       fprintf oc "	ldaxr	x17, [x15]\n";
       fprintf oc "	add	x17, x17, 1\n";
-      fprintf oc "	stlxr	w17, x17, [x15]\n";
-      fprintf oc "	cbnz	w17, %s\n" lbl;
+      fprintf oc "	stlxr	w29, x17, [x15]\n";
+      fprintf oc "	cbnz	w29, %s\n" lbl;
       fprintf oc "%s end profiling %a %d\n" comment
         Profilingaux.pp_id id kind;;
 
-- 
cgit 


From 76844ba0af1ed68cc542d08bfa335deb59545267 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 12 Apr 2021 18:37:08 +0200
Subject: test profiling

---
 test/monniaux/profiling/compcert_profiling.dat    | Bin 0 -> 96 bytes
 test/monniaux/profiling/test_profiling            | Bin 0 -> 14144 bytes
 test/monniaux/profiling/test_profiling.alloctrace |  83 +++
 test/monniaux/profiling/test_profiling.c          |  15 +
 test/monniaux/profiling/test_profiling.cm         | 112 ++++
 test/monniaux/profiling/test_profiling.i          | 747 ++++++++++++++++++++++
 test/monniaux/profiling/test_profiling.ltl.1      |  19 +
 test/monniaux/profiling/test_profiling.ltl.2      |  19 +
 test/monniaux/profiling/test_profiling.mach       |  20 +
 test/monniaux/profiling/test_profiling.rtl.0      |  23 +
 test/monniaux/profiling/test_profiling.rtl.1      |  23 +
 test/monniaux/profiling/test_profiling.rtl.10     |  21 +
 test/monniaux/profiling/test_profiling.rtl.11     |  21 +
 test/monniaux/profiling/test_profiling.rtl.12     |  21 +
 test/monniaux/profiling/test_profiling.rtl.13     |  21 +
 test/monniaux/profiling/test_profiling.rtl.14     |  21 +
 test/monniaux/profiling/test_profiling.rtl.15     |  21 +
 test/monniaux/profiling/test_profiling.rtl.16     |  21 +
 test/monniaux/profiling/test_profiling.rtl.17     |  21 +
 test/monniaux/profiling/test_profiling.rtl.18     |  21 +
 test/monniaux/profiling/test_profiling.rtl.19     |  21 +
 test/monniaux/profiling/test_profiling.rtl.2      |  23 +
 test/monniaux/profiling/test_profiling.rtl.20     |  21 +
 test/monniaux/profiling/test_profiling.rtl.21     |  21 +
 test/monniaux/profiling/test_profiling.rtl.22     |  21 +
 test/monniaux/profiling/test_profiling.rtl.23     |  21 +
 test/monniaux/profiling/test_profiling.rtl.24     |  21 +
 test/monniaux/profiling/test_profiling.rtl.25     |  21 +
 test/monniaux/profiling/test_profiling.rtl.26     |  21 +
 test/monniaux/profiling/test_profiling.rtl.27     |  21 +
 test/monniaux/profiling/test_profiling.rtl.28     |  21 +
 test/monniaux/profiling/test_profiling.rtl.29     |  21 +
 test/monniaux/profiling/test_profiling.rtl.3      |  23 +
 test/monniaux/profiling/test_profiling.rtl.30     |  21 +
 test/monniaux/profiling/test_profiling.rtl.31     |  21 +
 test/monniaux/profiling/test_profiling.rtl.32     |  21 +
 test/monniaux/profiling/test_profiling.rtl.4      |  23 +
 test/monniaux/profiling/test_profiling.rtl.5      |  23 +
 test/monniaux/profiling/test_profiling.rtl.6      |  21 +
 test/monniaux/profiling/test_profiling.rtl.7      |  21 +
 test/monniaux/profiling/test_profiling.rtl.8      |  21 +
 test/monniaux/profiling/test_profiling.rtl.9      |  21 +
 42 files changed, 1720 insertions(+)
 create mode 100644 test/monniaux/profiling/compcert_profiling.dat
 create mode 100755 test/monniaux/profiling/test_profiling
 create mode 100644 test/monniaux/profiling/test_profiling.alloctrace
 create mode 100644 test/monniaux/profiling/test_profiling.c
 create mode 100644 test/monniaux/profiling/test_profiling.cm
 create mode 100644 test/monniaux/profiling/test_profiling.i
 create mode 100644 test/monniaux/profiling/test_profiling.ltl.1
 create mode 100644 test/monniaux/profiling/test_profiling.ltl.2
 create mode 100644 test/monniaux/profiling/test_profiling.mach
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.0
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.1
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.10
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.11
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.12
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.13
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.14
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.15
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.16
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.17
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.18
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.19
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.2
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.20
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.21
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.22
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.23
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.24
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.25
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.26
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.27
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.28
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.29
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.3
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.30
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.31
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.32
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.4
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.5
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.6
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.7
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.8
 create mode 100644 test/monniaux/profiling/test_profiling.rtl.9

diff --git a/test/monniaux/profiling/compcert_profiling.dat b/test/monniaux/profiling/compcert_profiling.dat
new file mode 100644
index 00000000..fa57a995
Binary files /dev/null and b/test/monniaux/profiling/compcert_profiling.dat differ
diff --git a/test/monniaux/profiling/test_profiling b/test/monniaux/profiling/test_profiling
new file mode 100755
index 00000000..b530aae2
Binary files /dev/null and b/test/monniaux/profiling/test_profiling differ
diff --git a/test/monniaux/profiling/test_profiling.alloctrace b/test/monniaux/profiling/test_profiling.alloctrace
new file mode 100644
index 00000000..b61f6fc2
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.alloctrace
@@ -0,0 +1,83 @@
+-------------- Initial XTL
+
+f() {
+   16:	(x7, x1) = (X1, X0) using x13, x12; 
+   15:	if (x1 <s 2) goto 14 else goto 13
+   14:	x11 = 1; goto 1
+   13:	x6 = int64[x7 + 8]; 
+   12:	X0 = x6; X0 = call "atoi"(X0); x10 = X0; 
+   11:	
+   10:	if (x10 <=s 0) goto 9 else goto 4
+    9:	if (x10 ==s 0) goto 6 else goto 8
+    8:	x3 = "__stringlit_1" + 0; 
+    7:	X0 = x3; X0 = call "printf"(X0); goto 2
+    6:	x9 = "__stringlit_2" + 0; 
+    5:	X0 = x9; X0 = call "printf"(X0); goto 2
+    4:	x5 = "__stringlit_3" + 0; 
+    3:	X0 = x5; X0 = call "printf"(X0); 
+    2:	x11 = 0; 
+    1:	X0 = x11; return X0
+}
+
+------------------ Unspillable variables --------------
+
+x12 x13 
+
+-------------- After initial register allocation
+
+f() {
+   16:	(x7{X1}, x1{X0}) = (X1, X0) using x13{X2}, x12{D0}; 
+{ x1 x7 }
+   15:	if (x1{X0} <s 2) goto 14 else goto 13
+{ x7 }
+   14:	x11{X0} = 1; goto 1
+{ x11 }
+   13:	x6{X0} = int64[x7{X1} + 8]; 
+{ x6 }
+   12:	X0 = x6{X0}; X0 = call "atoi"(X0); x10{X0} = X0; 
+{ x10 }
+   11:	
+{ x10 }
+   10:	if (x10{X0} <=s 0) goto 9 else goto 4
+{ x10 }
+    9:	if (x10{X0} ==s 0) goto 6 else goto 8
+{ }
+    8:	x3{X0} = "__stringlit_1" + 0; 
+{ x3 }
+    7:	X0 = x3{X0}; X0 = call "printf"(X0); goto 2
+{ }
+    6:	x9{X0} = "__stringlit_2" + 0; 
+{ x9 }
+    5:	X0 = x9{X0}; X0 = call "printf"(X0); goto 2
+{ }
+    4:	x5{X0} = "__stringlit_3" + 0; 
+{ x5 }
+    3:	X0 = x5{X0}; X0 = call "printf"(X0); 
+{ }
+    2:	x11{X0} = 0; 
+{ x11 }
+    1:	X0 = x11{X0}; return X0
+{ }
+}
+
+-------------- Candidate allocation
+
+f() {
+   16:	
+   15:	if (X0 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	X0 = 1; goto 1
+   13:	X0 = int64[X1 + 8]; 
+   12:	call "atoi"; 
+   11:	
+   10:	if (X0 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (X0 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	X0 = "__stringlit_1" + 0; 
+    7:	call "printf"; goto 2
+    6:	X0 = "__stringlit_2" + 0; 
+    5:	call "printf"; goto 2
+    4:	X0 = "__stringlit_3" + 0; 
+    3:	call "printf"; 
+    2:	X0 = 0; 
+    1:	return
+}
+
diff --git a/test/monniaux/profiling/test_profiling.c b/test/monniaux/profiling/test_profiling.c
new file mode 100644
index 00000000..013b1d68
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.c
@@ -0,0 +1,15 @@
+#include <stdlib.h>
+#include <stdio.h>
+
+int main(int argc, char **argv) {
+  if (argc < 2) return 1;
+  int i = atoi(argv[1]);
+  if (i > 0) {
+    printf("positive\n");
+  } else if (i==0) {
+    printf("zero\n");
+  } else {
+    printf("negative\n");
+  }
+  return 0;
+}
diff --git a/test/monniaux/profiling/test_profiling.cm b/test/monniaux/profiling/test_profiling.cm
new file mode 100644
index 00000000..2a352510
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.cm
@@ -0,0 +1,112 @@
+var "__stringlit_2" readonly {int8 122,int8 101,int8 114,int8 111,int8 10,int8 0}
+var "__stringlit_1" readonly {int8 110,int8 101,int8 103,int8 97,int8 116,int8 105,int8 118,int8 101,int8 10,int8 0}
+var "__stringlit_3" readonly {int8 112,int8 111,int8 115,int8 105,int8 116,int8 105,int8 118,int8 101,int8 10,int8 0}
+
+extern "__builtin_ais_annot" = builtin "__builtin_ais_annot" : long -> void
+extern "__builtin_expect" = builtin "__builtin_expect" : long -> long -> long
+extern "__builtin_bswap64" = builtin "__builtin_bswap64" : long -> long
+extern "__builtin_bswap" = builtin "__builtin_bswap" : int -> int
+extern "__builtin_bswap32" = builtin "__builtin_bswap32" : int -> int
+extern "__builtin_bswap16" = builtin "__builtin_bswap16" : int -> int16u
+extern "__builtin_clz" = builtin "__builtin_clz" : int -> int
+extern "__builtin_clzl" = builtin "__builtin_clzl" : long -> int
+extern "__builtin_clzll" = builtin "__builtin_clzll" : long -> int
+extern "__builtin_ctz" = builtin "__builtin_ctz" : int -> int
+extern "__builtin_ctzl" = builtin "__builtin_ctzl" : long -> int
+extern "__builtin_ctzll" = builtin "__builtin_ctzll" : long -> int
+extern "__builtin_fabs" = builtin "__builtin_fabs" : float -> float
+extern "__builtin_fabsf" = builtin "__builtin_fabsf" : single -> single
+extern "__builtin_fsqrt" = builtin "__builtin_fsqrt" : float -> float
+extern "__builtin_sqrt" = builtin "__builtin_sqrt" : float -> float
+extern "__builtin_memcpy_aligned" = builtin "__builtin_memcpy_aligned" :
+         long -> long -> long -> long -> void
+extern "__builtin_sel" = builtin "__builtin_sel" : int -> void
+extern "__builtin_annot" = builtin "__builtin_annot" : long -> void
+extern "__builtin_annot_intval" = builtin "__builtin_annot_intval" : long ->
+         int -> int
+extern "__builtin_membar" = builtin "__builtin_membar" : void
+extern "__builtin_va_start" = builtin "__builtin_va_start" : long -> void
+extern "__builtin_va_arg" = builtin "__builtin_va_arg" : long -> int -> void
+extern "__builtin_va_copy" = builtin "__builtin_va_copy" : long -> long ->
+         void
+extern "__builtin_va_end" = builtin "__builtin_va_end" : long -> void
+extern "__compcert_va_int32" = extern "__compcert_va_int32" : long -> int
+extern "__compcert_va_int64" = extern "__compcert_va_int64" : long -> long
+extern "__compcert_va_float64" = extern "__compcert_va_float64" : long ->
+         float
+extern "__compcert_va_composite" = extern "__compcert_va_composite" : long ->
+         long -> long
+extern "__compcert_i64_dtos" = runtime "__compcert_i64_dtos" : float -> long
+extern "__compcert_i64_dtou" = runtime "__compcert_i64_dtou" : float -> long
+extern "__compcert_i64_stod" = runtime "__compcert_i64_stod" : long -> float
+extern "__compcert_i64_utod" = runtime "__compcert_i64_utod" : long -> float
+extern "__compcert_i64_stof" = runtime "__compcert_i64_stof" : long -> single
+extern "__compcert_i64_utof" = runtime "__compcert_i64_utof" : long -> single
+extern "__compcert_i64_sdiv" = runtime "__compcert_i64_sdiv" : long ->
+         long -> long
+extern "__compcert_i64_udiv" = runtime "__compcert_i64_udiv" : long ->
+         long -> long
+extern "__compcert_i64_smod" = runtime "__compcert_i64_smod" : long ->
+         long -> long
+extern "__compcert_i64_umod" = runtime "__compcert_i64_umod" : long ->
+         long -> long
+extern "__compcert_i64_shl" = runtime "__compcert_i64_shl" : long -> int ->
+         long
+extern "__compcert_i64_shr" = runtime "__compcert_i64_shr" : long -> int ->
+         long
+extern "__compcert_i64_sar" = runtime "__compcert_i64_sar" : long -> int ->
+         long
+extern "__compcert_i64_smulh" = runtime "__compcert_i64_smulh" : long ->
+         long -> long
+extern "__compcert_i64_umulh" = runtime "__compcert_i64_umulh" : long ->
+         long -> long
+extern "__compcert_i32_sdiv" = runtime "__compcert_i32_sdiv" : int -> int ->
+         int
+extern "__compcert_i32_udiv" = runtime "__compcert_i32_udiv" : int -> int ->
+         int
+extern "__compcert_i32_smod" = runtime "__compcert_i32_smod" : int -> int ->
+         int
+extern "__compcert_i32_umod" = runtime "__compcert_i32_umod" : int -> int ->
+         int
+extern "__compcert_f32_div" = runtime "__compcert_f32_div" : single ->
+         single -> single
+extern "__compcert_f64_div" = runtime "__compcert_f64_div" : float ->
+         float -> float
+extern "__builtin_fence" = builtin "__builtin_fence" : void
+extern "__builtin_cls" = builtin "__builtin_cls" : int -> int
+extern "__builtin_clsl" = builtin "__builtin_clsl" : long -> int
+extern "__builtin_clsll" = builtin "__builtin_clsll" : long -> int
+extern "__builtin_fmadd" = builtin "__builtin_fmadd" : float -> float ->
+         float -> float
+extern "__builtin_fmsub" = builtin "__builtin_fmsub" : float -> float ->
+         float -> float
+extern "__builtin_fnmadd" = builtin "__builtin_fnmadd" : float -> float ->
+         float -> float
+extern "__builtin_fnmsub" = builtin "__builtin_fnmsub" : float -> float ->
+         float -> float
+extern "__builtin_fmax" = builtin "__builtin_fmax" : float -> float -> float
+extern "__builtin_fmin" = builtin "__builtin_fmin" : float -> float -> float
+extern "__builtin_debug" = extern "__builtin_debug" : int -> void
+extern "atoi" = extern "atoi" : long -> int
+extern "printf" = extern "printf" : long -> int
+"main"('argc', 'argv') : int -> long -> int
+{
+  var 'i', '$71';
+  if ('argc' < 2) {
+    return 1;
+  }
+  '$71' = "atoi"(int64['argv' +l 8LL *l longofint 1]) : long -> int;
+  'i' = '$71';
+  if ('i' > 0) {
+    "printf"("__stringlit_3") : long -> int;
+  } else {
+    if ('i' == 0) {
+      "printf"("__stringlit_2") : long -> int;
+    } else {
+      "printf"("__stringlit_1") : long -> int;
+    }
+  }
+  return 0;
+  return 0;
+}
+
diff --git a/test/monniaux/profiling/test_profiling.i b/test/monniaux/profiling/test_profiling.i
new file mode 100644
index 00000000..35c67916
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.i
@@ -0,0 +1,747 @@
+# 1 "test_profiling.c"
+# 1 "<built-in>"
+# 1 "<command-line>"
+# 1 "/usr/aarch64-linux-gnu/include/stdc-predef.h" 1 3
+# 1 "<command-line>" 2
+# 1 "test_profiling.c"
+# 1 "/usr/aarch64-linux-gnu/include/stdlib.h" 1 3
+# 25 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/libc-header-start.h" 1 3
+# 33 "/usr/aarch64-linux-gnu/include/bits/libc-header-start.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/features.h" 1 3
+# 461 "/usr/aarch64-linux-gnu/include/features.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/sys/cdefs.h" 1 3
+# 452 "/usr/aarch64-linux-gnu/include/sys/cdefs.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/wordsize.h" 1 3
+# 453 "/usr/aarch64-linux-gnu/include/sys/cdefs.h" 2 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/long-double.h" 1 3
+# 454 "/usr/aarch64-linux-gnu/include/sys/cdefs.h" 2 3
+# 462 "/usr/aarch64-linux-gnu/include/features.h" 2 3
+# 485 "/usr/aarch64-linux-gnu/include/features.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/gnu/stubs.h" 1 3
+
+
+
+
+# 1 "/usr/aarch64-linux-gnu/include/bits/wordsize.h" 1 3
+# 6 "/usr/aarch64-linux-gnu/include/gnu/stubs.h" 2 3
+
+
+# 1 "/usr/aarch64-linux-gnu/include/gnu/stubs-lp64.h" 1 3
+# 9 "/usr/aarch64-linux-gnu/include/gnu/stubs.h" 2 3
+# 486 "/usr/aarch64-linux-gnu/include/features.h" 2 3
+# 34 "/usr/aarch64-linux-gnu/include/bits/libc-header-start.h" 2 3
+# 26 "/usr/aarch64-linux-gnu/include/stdlib.h" 2 3
+
+
+
+
+
+# 1 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stddef.h" 1 3
+# 67 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stddef.h" 3
+
+# 67 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stddef.h" 3
+typedef unsigned long size_t;
+# 101 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stddef.h" 3
+typedef signed int wchar_t;
+# 32 "/usr/aarch64-linux-gnu/include/stdlib.h" 2 3
+
+
+# 55 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 1 3
+# 23 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/long-double.h" 1 3
+# 24 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 2 3
+# 80 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 3
+typedef long double _Float128;
+# 95 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 1 3
+# 24 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/long-double.h" 1 3
+# 25 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 2 3
+# 214 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 3
+typedef float _Float32;
+# 251 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 3
+typedef double _Float64;
+# 268 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 3
+typedef double _Float32x;
+# 285 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 3
+typedef long double _Float64x;
+# 96 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 2 3
+# 56 "/usr/aarch64-linux-gnu/include/stdlib.h" 2 3
+
+
+typedef struct
+  {
+    int quot;
+    int rem;
+  } div_t;
+
+
+
+typedef struct
+  {
+    long int quot;
+    long int rem;
+  } ldiv_t;
+
+
+
+
+
+ typedef struct
+  {
+    long long int quot;
+    long long int rem;
+  } lldiv_t;
+# 97 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern size_t __ctype_get_mb_cur_max (void) ;
+
+
+
+extern double atof (const char *__nptr)
+     ;
+
+extern int atoi (const char *__nptr)
+     ;
+
+extern long int atol (const char *__nptr)
+     ;
+
+
+
+ extern long long int atoll (const char *__nptr)
+     ;
+
+
+
+extern double strtod (const char *restrict __nptr,
+        char **restrict __endptr)
+     ;
+
+
+
+extern float strtof (const char *restrict __nptr,
+       char **restrict __endptr) ;
+
+extern long double strtold (const char *restrict __nptr,
+       char **restrict __endptr)
+     ;
+# 176 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern long int strtol (const char *restrict __nptr,
+   char **restrict __endptr, int __base)
+     ;
+
+extern unsigned long int strtoul (const char *restrict __nptr,
+      char **restrict __endptr, int __base)
+     ;
+# 199 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+
+extern long long int strtoll (const char *restrict __nptr,
+         char **restrict __endptr, int __base)
+     ;
+
+
+extern unsigned long long int strtoull (const char *restrict __nptr,
+     char **restrict __endptr, int __base)
+     ;
+# 453 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern int rand (void) ;
+
+extern void srand (unsigned int __seed) ;
+# 539 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern void *malloc (size_t __size)
+     ;
+
+extern void *calloc (size_t __nmemb, size_t __size)
+     ;
+
+
+
+
+
+
+extern void *realloc (void *__ptr, size_t __size)
+     ;
+# 565 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern void free (void *__ptr) ;
+# 591 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern void abort (void) ;
+
+
+
+extern int atexit (void (*__func) (void)) ;
+# 617 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern void exit (int __status) ;
+# 629 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern void _Exit (int __status) ;
+
+
+
+
+extern char *getenv (const char *__name) ;
+# 784 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern int system (const char *__command) ;
+# 808 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+typedef int (*__compar_fn_t) (const void *, const void *);
+# 820 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern void *bsearch (const void *__key, const void *__base,
+        size_t __nmemb, size_t __size, __compar_fn_t __compar)
+     ;
+
+
+
+
+
+
+
+extern void qsort (void *__base, size_t __nmemb, size_t __size,
+     __compar_fn_t __compar) ;
+# 840 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern int abs (int __x) ;
+extern long int labs (long int __x) ;
+
+
+ extern long long int llabs (long long int __x)
+     ;
+
+
+
+
+
+
+extern div_t div (int __numer, int __denom)
+     ;
+extern ldiv_t ldiv (long int __numer, long int __denom)
+     ;
+
+
+ extern lldiv_t lldiv (long long int __numer,
+        long long int __denom)
+     ;
+# 922 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+extern int mblen (const char *__s, size_t __n) ;
+
+
+extern int mbtowc (wchar_t *restrict __pwc,
+     const char *restrict __s, size_t __n) ;
+
+
+extern int wctomb (char *__s, wchar_t __wchar) ;
+
+
+
+extern size_t mbstowcs (wchar_t *restrict __pwcs,
+   const char *restrict __s, size_t __n) ;
+
+extern size_t wcstombs (char *restrict __s,
+   const wchar_t *restrict __pwcs, size_t __n)
+     ;
+# 1013 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/stdlib-float.h" 1 3
+# 1014 "/usr/aarch64-linux-gnu/include/stdlib.h" 2 3
+# 1023 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
+
+# 2 "test_profiling.c" 2
+# 1 "/usr/aarch64-linux-gnu/include/stdio.h" 1 3
+# 27 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/libc-header-start.h" 1 3
+# 28 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
+
+
+
+
+
+# 1 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stddef.h" 1 3
+# 34 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
+
+
+# 1 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stdarg.h" 1 3
+# 43 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stdarg.h" 3
+typedef __builtin_va_list __gnuc_va_list;
+# 37 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
+
+# 1 "/usr/aarch64-linux-gnu/include/bits/types.h" 1 3
+# 27 "/usr/aarch64-linux-gnu/include/bits/types.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/wordsize.h" 1 3
+# 28 "/usr/aarch64-linux-gnu/include/bits/types.h" 2 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/timesize.h" 1 3
+# 19 "/usr/aarch64-linux-gnu/include/bits/timesize.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/wordsize.h" 1 3
+# 20 "/usr/aarch64-linux-gnu/include/bits/timesize.h" 2 3
+# 29 "/usr/aarch64-linux-gnu/include/bits/types.h" 2 3
+
+
+typedef unsigned char __u_char;
+typedef unsigned short int __u_short;
+typedef unsigned int __u_int;
+typedef unsigned long int __u_long;
+
+
+typedef signed char __int8_t;
+typedef unsigned char __uint8_t;
+typedef signed short int __int16_t;
+typedef unsigned short int __uint16_t;
+typedef signed int __int32_t;
+typedef unsigned int __uint32_t;
+
+typedef signed long int __int64_t;
+typedef unsigned long int __uint64_t;
+
+
+
+
+
+
+typedef __int8_t __int_least8_t;
+typedef __uint8_t __uint_least8_t;
+typedef __int16_t __int_least16_t;
+typedef __uint16_t __uint_least16_t;
+typedef __int32_t __int_least32_t;
+typedef __uint32_t __uint_least32_t;
+typedef __int64_t __int_least64_t;
+typedef __uint64_t __uint_least64_t;
+
+
+
+typedef long int __quad_t;
+typedef unsigned long int __u_quad_t;
+
+
+
+
+
+
+
+typedef long int __intmax_t;
+typedef unsigned long int __uintmax_t;
+# 141 "/usr/aarch64-linux-gnu/include/bits/types.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/typesizes.h" 1 3
+# 142 "/usr/aarch64-linux-gnu/include/bits/types.h" 2 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/time64.h" 1 3
+# 143 "/usr/aarch64-linux-gnu/include/bits/types.h" 2 3
+
+
+typedef unsigned long int __dev_t;
+typedef unsigned int __uid_t;
+typedef unsigned int __gid_t;
+typedef unsigned long int __ino_t;
+typedef unsigned long int __ino64_t;
+typedef unsigned int __mode_t;
+typedef unsigned int __nlink_t;
+typedef long int __off_t;
+typedef long int __off64_t;
+typedef int __pid_t;
+typedef struct { int __val[2]; } __fsid_t;
+typedef long int __clock_t;
+typedef unsigned long int __rlim_t;
+typedef unsigned long int __rlim64_t;
+typedef unsigned int __id_t;
+typedef long int __time_t;
+typedef unsigned int __useconds_t;
+typedef long int __suseconds_t;
+
+typedef int __daddr_t;
+typedef int __key_t;
+
+
+typedef int __clockid_t;
+
+
+typedef void * __timer_t;
+
+
+typedef int __blksize_t;
+
+
+
+
+typedef long int __blkcnt_t;
+typedef long int __blkcnt64_t;
+
+
+typedef unsigned long int __fsblkcnt_t;
+typedef unsigned long int __fsblkcnt64_t;
+
+
+typedef unsigned long int __fsfilcnt_t;
+typedef unsigned long int __fsfilcnt64_t;
+
+
+typedef long int __fsword_t;
+
+typedef long int __ssize_t;
+
+
+typedef long int __syscall_slong_t;
+
+typedef unsigned long int __syscall_ulong_t;
+
+
+
+typedef __off64_t __loff_t;
+typedef char *__caddr_t;
+
+
+typedef long int __intptr_t;
+
+
+typedef unsigned int __socklen_t;
+
+
+
+
+typedef int __sig_atomic_t;
+# 39 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/types/__fpos_t.h" 1 3
+
+
+
+
+# 1 "/usr/aarch64-linux-gnu/include/bits/types/__mbstate_t.h" 1 3
+# 13 "/usr/aarch64-linux-gnu/include/bits/types/__mbstate_t.h" 3
+typedef struct
+{
+  int __count;
+  union
+  {
+    unsigned int __wch;
+    char __wchb[4];
+  } __value;
+} __mbstate_t;
+# 6 "/usr/aarch64-linux-gnu/include/bits/types/__fpos_t.h" 2 3
+
+
+
+
+typedef struct _G_fpos_t
+{
+  __off_t __pos;
+  __mbstate_t __state;
+} __fpos_t;
+# 40 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/types/__fpos64_t.h" 1 3
+# 10 "/usr/aarch64-linux-gnu/include/bits/types/__fpos64_t.h" 3
+typedef struct _G_fpos64_t
+{
+  __off64_t __pos;
+  __mbstate_t __state;
+} __fpos64_t;
+# 41 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/types/__FILE.h" 1 3
+
+
+
+struct _IO_FILE;
+typedef struct _IO_FILE __FILE;
+# 42 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/types/FILE.h" 1 3
+
+
+
+struct _IO_FILE;
+
+
+typedef struct _IO_FILE FILE;
+# 43 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/types/struct_FILE.h" 1 3
+# 35 "/usr/aarch64-linux-gnu/include/bits/types/struct_FILE.h" 3
+struct _IO_FILE;
+struct _IO_marker;
+struct _IO_codecvt;
+struct _IO_wide_data;
+
+
+
+
+typedef void _IO_lock_t;
+
+
+
+
+
+struct _IO_FILE
+{
+  int _flags;
+
+
+  char *_IO_read_ptr;
+  char *_IO_read_end;
+  char *_IO_read_base;
+  char *_IO_write_base;
+  char *_IO_write_ptr;
+  char *_IO_write_end;
+  char *_IO_buf_base;
+  char *_IO_buf_end;
+
+
+  char *_IO_save_base;
+  char *_IO_backup_base;
+  char *_IO_save_end;
+
+  struct _IO_marker *_markers;
+
+  struct _IO_FILE *_chain;
+
+  int _fileno;
+  int _flags2;
+  __off_t _old_offset;
+
+
+  unsigned short _cur_column;
+  signed char _vtable_offset;
+  char _shortbuf[1];
+
+  _IO_lock_t *_lock;
+
+
+
+
+
+
+
+  __off64_t _offset;
+
+  struct _IO_codecvt *_codecvt;
+  struct _IO_wide_data *_wide_data;
+  struct _IO_FILE *_freeres_list;
+  void *_freeres_buf;
+  size_t __pad5;
+  int _mode;
+
+  char _unused2[15 * sizeof (int) - 4 * sizeof (void *) - sizeof (size_t)];
+};
+# 44 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
+# 84 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+typedef __fpos_t fpos_t;
+# 133 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+# 1 "/usr/aarch64-linux-gnu/include/bits/stdio_lim.h" 1 3
+# 134 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
+
+
+
+extern FILE *stdin;
+extern FILE *stdout;
+extern FILE *stderr;
+
+
+
+
+
+
+extern int remove (const char *__filename) ;
+
+extern int rename (const char *__old, const char *__new) ;
+# 173 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern FILE *tmpfile (void) ;
+# 187 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern char *tmpnam (char *__s) ;
+# 213 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int fclose (FILE *__stream);
+
+
+
+
+extern int fflush (FILE *__stream);
+# 246 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern FILE *fopen (const char *restrict __filename,
+      const char *restrict __modes) ;
+
+
+
+
+extern FILE *freopen (const char *restrict __filename,
+        const char *restrict __modes,
+        FILE *restrict __stream) ;
+# 304 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern void setbuf (FILE *restrict __stream, char *restrict __buf) ;
+
+
+
+extern int setvbuf (FILE *restrict __stream, char *restrict __buf,
+      int __modes, size_t __n) ;
+# 326 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int fprintf (FILE *restrict __stream,
+      const char *restrict __format, ...);
+
+
+
+
+extern int printf (const char *restrict __format, ...);
+
+extern int sprintf (char *restrict __s,
+      const char *restrict __format, ...) ;
+
+
+
+
+
+extern int vfprintf (FILE *restrict __s, const char *restrict __format,
+       __gnuc_va_list __arg);
+
+
+
+
+extern int vprintf (const char *restrict __format, __gnuc_va_list __arg);
+
+extern int vsprintf (char *restrict __s, const char *restrict __format,
+       __gnuc_va_list __arg) ;
+
+
+
+extern int snprintf (char *restrict __s, size_t __maxlen,
+       const char *restrict __format, ...)
+     ;
+
+extern int vsnprintf (char *restrict __s, size_t __maxlen,
+        const char *restrict __format, __gnuc_va_list __arg)
+     ;
+# 391 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int fscanf (FILE *restrict __stream,
+     const char *restrict __format, ...) ;
+
+
+
+
+extern int scanf (const char *restrict __format, ...) ;
+
+extern int sscanf (const char *restrict __s,
+     const char *restrict __format, ...) ;
+# 416 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int __isoc99_fscanf (FILE *restrict __stream,
+       const char *restrict __format, ...) ;
+extern int __isoc99_scanf (const char *restrict __format, ...) ;
+extern int __isoc99_sscanf (const char *restrict __s,
+       const char *restrict __format, ...) ;
+# 432 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int vfscanf (FILE *restrict __s, const char *restrict __format,
+      __gnuc_va_list __arg)
+     ;
+
+
+
+
+
+extern int vscanf (const char *restrict __format, __gnuc_va_list __arg)
+     ;
+
+
+extern int vsscanf (const char *restrict __s,
+      const char *restrict __format, __gnuc_va_list __arg)
+     ;
+# 465 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int __isoc99_vfscanf (FILE *restrict __s,
+        const char *restrict __format,
+        __gnuc_va_list __arg) ;
+extern int __isoc99_vscanf (const char *restrict __format,
+       __gnuc_va_list __arg) ;
+extern int __isoc99_vsscanf (const char *restrict __s,
+        const char *restrict __format,
+        __gnuc_va_list __arg) ;
+# 485 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int fgetc (FILE *__stream);
+extern int getc (FILE *__stream);
+
+
+
+
+
+extern int getchar (void);
+# 521 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int fputc (int __c, FILE *__stream);
+extern int putc (int __c, FILE *__stream);
+
+
+
+
+
+extern int putchar (int __c);
+# 564 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern char *fgets (char *restrict __s, int __n, FILE *restrict __stream)
+     ;
+# 577 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern char *gets (char *__s) ;
+# 626 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int fputs (const char *restrict __s, FILE *restrict __stream);
+
+
+
+
+
+extern int puts (const char *__s);
+
+
+
+
+
+
+extern int ungetc (int __c, FILE *__stream);
+
+
+
+
+
+
+extern size_t fread (void *restrict __ptr, size_t __size,
+       size_t __n, FILE *restrict __stream) ;
+
+
+
+
+extern size_t fwrite (const void *restrict __ptr, size_t __size,
+        size_t __n, FILE *restrict __s);
+# 684 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int fseek (FILE *__stream, long int __off, int __whence);
+
+
+
+
+extern long int ftell (FILE *__stream) ;
+
+
+
+
+extern void rewind (FILE *__stream);
+# 731 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int fgetpos (FILE *restrict __stream, fpos_t *restrict __pos);
+
+
+
+
+extern int fsetpos (FILE *__stream, const fpos_t *__pos);
+# 757 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern void clearerr (FILE *__stream) ;
+
+extern int feof (FILE *__stream) ;
+
+extern int ferror (FILE *__stream) ;
+# 775 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern void perror (const char *__s);
+
+
+
+
+
+# 1 "/usr/aarch64-linux-gnu/include/bits/sys_errlist.h" 1 3
+# 782 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
+# 858 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+extern int __uflow (FILE *);
+extern int __overflow (FILE *, int);
+# 873 "/usr/aarch64-linux-gnu/include/stdio.h" 3
+
+# 3 "test_profiling.c" 2
+
+
+# 4 "test_profiling.c"
+int main(int argc, char **argv) {
+  if (argc < 2) return 1;
+  int i = atoi(argv[1]);
+  if (i > 0) {
+    printf("positive\n");
+  } else if (i==0) {
+    printf("zero\n");
+  } else {
+    printf("negative\n");
+  }
+  return 0;
+}
diff --git a/test/monniaux/profiling/test_profiling.ltl.1 b/test/monniaux/profiling/test_profiling.ltl.1
new file mode 100644
index 00000000..fdfb7fe0
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.ltl.1
@@ -0,0 +1,19 @@
+main() {
+   16:	
+   15:	if (X0 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	X0 = 1; goto 1
+   13:	X0 = int64[X1 + 8]; 
+   12:	call "atoi"; 
+   11:	
+   10:	if (X0 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (X0 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	X0 = "__stringlit_1" + 0; 
+    7:	call "printf"; goto 2
+    6:	X0 = "__stringlit_2" + 0; 
+    5:	call "printf"; goto 2
+    4:	X0 = "__stringlit_3" + 0; 
+    3:	call "printf"; 
+    2:	X0 = 0; 
+    1:	return
+}
+
diff --git a/test/monniaux/profiling/test_profiling.ltl.2 b/test/monniaux/profiling/test_profiling.ltl.2
new file mode 100644
index 00000000..f9be9feb
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.ltl.2
@@ -0,0 +1,19 @@
+main() {
+goto 15   16:	
+   15:	if (X0 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	X0 = 1; goto 1
+   13:	X0 = int64[X1 + 8]; 
+   12:	call "atoi"; goto 10
+   11:	
+   10:	if (X0 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (X0 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	X0 = "__stringlit_1" + 0; 
+    7:	call "printf"; goto 2
+    6:	X0 = "__stringlit_2" + 0; 
+    5:	call "printf"; goto 2
+    4:	X0 = "__stringlit_3" + 0; 
+    3:	call "printf"; 
+    2:	X0 = 0; 
+    1:	return
+}
+
diff --git a/test/monniaux/profiling/test_profiling.mach b/test/monniaux/profiling/test_profiling.mach
new file mode 100644
index 00000000..31124d94
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.mach
@@ -0,0 +1,20 @@
+main() {
+	if (X0 <s 2) goto 14
+	X0 = int64[X1 + 8]
+	call "atoi"
+	if (X0 <=s 0) goto 9
+	X0 = "__stringlit_3" + 0
+	call "printf"
+	goto 2
+   14:	X0 = 1
+	goto 1
+    9:	if (X0 ==s 0) goto 6
+	X0 = "__stringlit_1" + 0
+	call "printf"
+	goto 2
+    6:	X0 = "__stringlit_2" + 0
+	call "printf"
+    2:	X0 = 0
+    1:	return
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.0 b/test/monniaux/profiling/test_profiling.rtl.0
new file mode 100644
index 00000000..d5ce096d
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.0
@@ -0,0 +1,23 @@
+main(x2, x1) {
+   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
+   15:	x5 = 1
+	goto 1
+   14:	x12 = int64[x1 + 8]
+   13:	x3 = "atoi"(x12)
+   12:	x4 = x3
+   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
+   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
+    9:	x10 = "__stringlit_1" + 0
+    8:	x11 = "printf"(x10)
+	goto 3
+    7:	x8 = "__stringlit_2" + 0
+    6:	x9 = "printf"(x8)
+	goto 3
+    5:	x6 = "__stringlit_3" + 0
+    4:	x7 = "printf"(x6)
+    3:	x5 = 0
+	goto 1
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.1 b/test/monniaux/profiling/test_profiling.rtl.1
new file mode 100644
index 00000000..d5ce096d
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.1
@@ -0,0 +1,23 @@
+main(x2, x1) {
+   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
+   15:	x5 = 1
+	goto 1
+   14:	x12 = int64[x1 + 8]
+   13:	x3 = "atoi"(x12)
+   12:	x4 = x3
+   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
+   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
+    9:	x10 = "__stringlit_1" + 0
+    8:	x11 = "printf"(x10)
+	goto 3
+    7:	x8 = "__stringlit_2" + 0
+    6:	x9 = "printf"(x8)
+	goto 3
+    5:	x6 = "__stringlit_3" + 0
+    4:	x7 = "printf"(x6)
+    3:	x5 = 0
+	goto 1
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.10 b/test/monniaux/profiling/test_profiling.rtl.10
new file mode 100644
index 00000000..8b268c84
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.10
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.11 b/test/monniaux/profiling/test_profiling.rtl.11
new file mode 100644
index 00000000..8b268c84
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.11
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.12 b/test/monniaux/profiling/test_profiling.rtl.12
new file mode 100644
index 00000000..8b268c84
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.12
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.13 b/test/monniaux/profiling/test_profiling.rtl.13
new file mode 100644
index 00000000..8b268c84
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.13
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.14 b/test/monniaux/profiling/test_profiling.rtl.14
new file mode 100644
index 00000000..8b268c84
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.14
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.15 b/test/monniaux/profiling/test_profiling.rtl.15
new file mode 100644
index 00000000..8b268c84
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.15
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.16 b/test/monniaux/profiling/test_profiling.rtl.16
new file mode 100644
index 00000000..8b268c84
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.16
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.17 b/test/monniaux/profiling/test_profiling.rtl.17
new file mode 100644
index 00000000..8b268c84
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.17
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.18 b/test/monniaux/profiling/test_profiling.rtl.18
new file mode 100644
index 00000000..8b268c84
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.18
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.19 b/test/monniaux/profiling/test_profiling.rtl.19
new file mode 100644
index 00000000..091878ec
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.19
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.2 b/test/monniaux/profiling/test_profiling.rtl.2
new file mode 100644
index 00000000..d5ce096d
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.2
@@ -0,0 +1,23 @@
+main(x2, x1) {
+   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
+   15:	x5 = 1
+	goto 1
+   14:	x12 = int64[x1 + 8]
+   13:	x3 = "atoi"(x12)
+   12:	x4 = x3
+   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
+   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
+    9:	x10 = "__stringlit_1" + 0
+    8:	x11 = "printf"(x10)
+	goto 3
+    7:	x8 = "__stringlit_2" + 0
+    6:	x9 = "printf"(x8)
+	goto 3
+    5:	x6 = "__stringlit_3" + 0
+    4:	x7 = "printf"(x6)
+    3:	x5 = 0
+	goto 1
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.20 b/test/monniaux/profiling/test_profiling.rtl.20
new file mode 100644
index 00000000..091878ec
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.20
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.21 b/test/monniaux/profiling/test_profiling.rtl.21
new file mode 100644
index 00000000..091878ec
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.21
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.22 b/test/monniaux/profiling/test_profiling.rtl.22
new file mode 100644
index 00000000..9102f74f
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.22
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	nop
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.23 b/test/monniaux/profiling/test_profiling.rtl.23
new file mode 100644
index 00000000..9102f74f
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.23
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	nop
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.24 b/test/monniaux/profiling/test_profiling.rtl.24
new file mode 100644
index 00000000..9102f74f
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.24
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	nop
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.25 b/test/monniaux/profiling/test_profiling.rtl.25
new file mode 100644
index 00000000..9102f74f
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.25
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	nop
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.26 b/test/monniaux/profiling/test_profiling.rtl.26
new file mode 100644
index 00000000..9102f74f
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.26
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	nop
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.27 b/test/monniaux/profiling/test_profiling.rtl.27
new file mode 100644
index 00000000..9102f74f
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.27
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	nop
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.28 b/test/monniaux/profiling/test_profiling.rtl.28
new file mode 100644
index 00000000..9102f74f
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.28
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	nop
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.29 b/test/monniaux/profiling/test_profiling.rtl.29
new file mode 100644
index 00000000..9102f74f
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.29
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	nop
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.3 b/test/monniaux/profiling/test_profiling.rtl.3
new file mode 100644
index 00000000..d5ce096d
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.3
@@ -0,0 +1,23 @@
+main(x2, x1) {
+   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
+   15:	x5 = 1
+	goto 1
+   14:	x12 = int64[x1 + 8]
+   13:	x3 = "atoi"(x12)
+   12:	x4 = x3
+   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
+   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
+    9:	x10 = "__stringlit_1" + 0
+    8:	x11 = "printf"(x10)
+	goto 3
+    7:	x8 = "__stringlit_2" + 0
+    6:	x9 = "printf"(x8)
+	goto 3
+    5:	x6 = "__stringlit_3" + 0
+    4:	x7 = "printf"(x6)
+    3:	x5 = 0
+	goto 1
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.30 b/test/monniaux/profiling/test_profiling.rtl.30
new file mode 100644
index 00000000..9102f74f
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.30
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	nop
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.31 b/test/monniaux/profiling/test_profiling.rtl.31
new file mode 100644
index 00000000..9102f74f
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.31
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	nop
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.32 b/test/monniaux/profiling/test_profiling.rtl.32
new file mode 100644
index 00000000..9102f74f
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.32
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	nop
+   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.4 b/test/monniaux/profiling/test_profiling.rtl.4
new file mode 100644
index 00000000..d5ce096d
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.4
@@ -0,0 +1,23 @@
+main(x2, x1) {
+   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
+   15:	x5 = 1
+	goto 1
+   14:	x12 = int64[x1 + 8]
+   13:	x3 = "atoi"(x12)
+   12:	x4 = x3
+   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
+   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
+    9:	x10 = "__stringlit_1" + 0
+    8:	x11 = "printf"(x10)
+	goto 3
+    7:	x8 = "__stringlit_2" + 0
+    6:	x9 = "printf"(x8)
+	goto 3
+    5:	x6 = "__stringlit_3" + 0
+    4:	x7 = "printf"(x6)
+    3:	x5 = 0
+	goto 1
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.5 b/test/monniaux/profiling/test_profiling.rtl.5
new file mode 100644
index 00000000..d5ce096d
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.5
@@ -0,0 +1,23 @@
+main(x2, x1) {
+   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
+   15:	x5 = 1
+	goto 1
+   14:	x12 = int64[x1 + 8]
+   13:	x3 = "atoi"(x12)
+   12:	x4 = x3
+   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
+   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
+    9:	x10 = "__stringlit_1" + 0
+    8:	x11 = "printf"(x10)
+	goto 3
+    7:	x8 = "__stringlit_2" + 0
+    6:	x9 = "printf"(x8)
+	goto 3
+    5:	x6 = "__stringlit_3" + 0
+    4:	x7 = "printf"(x6)
+    3:	x5 = 0
+	goto 1
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.6 b/test/monniaux/profiling/test_profiling.rtl.6
new file mode 100644
index 00000000..2f75aa61
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.6
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: none)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 >s 0) goto 4 else goto 9 (prediction: none)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.7 b/test/monniaux/profiling/test_profiling.rtl.7
new file mode 100644
index 00000000..2f75aa61
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.7
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: none)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 >s 0) goto 4 else goto 9 (prediction: none)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.8 b/test/monniaux/profiling/test_profiling.rtl.8
new file mode 100644
index 00000000..8b268c84
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.8
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
diff --git a/test/monniaux/profiling/test_profiling.rtl.9 b/test/monniaux/profiling/test_profiling.rtl.9
new file mode 100644
index 00000000..8b268c84
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.rtl.9
@@ -0,0 +1,21 @@
+main(x2, x1) {
+   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
+   14:	x5 = 1
+	goto 1
+   13:	x12 = int64[x1 + 8]
+   12:	x3 = "atoi"(x12)
+   11:	x4 = x3
+   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
+    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
+    8:	x10 = "__stringlit_1" + 0
+    7:	x11 = "printf"(x10)
+	goto 2
+    6:	x8 = "__stringlit_2" + 0
+    5:	x9 = "printf"(x8)
+	goto 2
+    4:	x6 = "__stringlit_3" + 0
+    3:	x7 = "printf"(x6)
+    2:	x5 = 0
+    1:	return x5
+}
+
-- 
cgit 


From 5a846f2aeb5eb659c1b510e3fb27e49677cb8680 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 12 Apr 2021 18:38:39 +0200
Subject: rm spurious files

---
 test/monniaux/profiling/test_profiling.alloctrace |  83 ---
 test/monniaux/profiling/test_profiling.cm         | 112 ----
 test/monniaux/profiling/test_profiling.i          | 747 ----------------------
 test/monniaux/profiling/test_profiling.ltl.1      |  19 -
 test/monniaux/profiling/test_profiling.ltl.2      |  19 -
 test/monniaux/profiling/test_profiling.mach       |  20 -
 test/monniaux/profiling/test_profiling.rtl.0      |  23 -
 test/monniaux/profiling/test_profiling.rtl.1      |  23 -
 test/monniaux/profiling/test_profiling.rtl.10     |  21 -
 test/monniaux/profiling/test_profiling.rtl.11     |  21 -
 test/monniaux/profiling/test_profiling.rtl.12     |  21 -
 test/monniaux/profiling/test_profiling.rtl.13     |  21 -
 test/monniaux/profiling/test_profiling.rtl.14     |  21 -
 test/monniaux/profiling/test_profiling.rtl.15     |  21 -
 test/monniaux/profiling/test_profiling.rtl.16     |  21 -
 test/monniaux/profiling/test_profiling.rtl.17     |  21 -
 test/monniaux/profiling/test_profiling.rtl.18     |  21 -
 test/monniaux/profiling/test_profiling.rtl.19     |  21 -
 test/monniaux/profiling/test_profiling.rtl.2      |  23 -
 test/monniaux/profiling/test_profiling.rtl.20     |  21 -
 test/monniaux/profiling/test_profiling.rtl.21     |  21 -
 test/monniaux/profiling/test_profiling.rtl.22     |  21 -
 test/monniaux/profiling/test_profiling.rtl.23     |  21 -
 test/monniaux/profiling/test_profiling.rtl.24     |  21 -
 test/monniaux/profiling/test_profiling.rtl.25     |  21 -
 test/monniaux/profiling/test_profiling.rtl.26     |  21 -
 test/monniaux/profiling/test_profiling.rtl.27     |  21 -
 test/monniaux/profiling/test_profiling.rtl.28     |  21 -
 test/monniaux/profiling/test_profiling.rtl.29     |  21 -
 test/monniaux/profiling/test_profiling.rtl.3      |  23 -
 test/monniaux/profiling/test_profiling.rtl.30     |  21 -
 test/monniaux/profiling/test_profiling.rtl.31     |  21 -
 test/monniaux/profiling/test_profiling.rtl.32     |  21 -
 test/monniaux/profiling/test_profiling.rtl.4      |  23 -
 test/monniaux/profiling/test_profiling.rtl.5      |  23 -
 test/monniaux/profiling/test_profiling.rtl.6      |  21 -
 test/monniaux/profiling/test_profiling.rtl.7      |  21 -
 test/monniaux/profiling/test_profiling.rtl.8      |  21 -
 test/monniaux/profiling/test_profiling.rtl.9      |  21 -
 39 files changed, 1705 deletions(-)
 delete mode 100644 test/monniaux/profiling/test_profiling.alloctrace
 delete mode 100644 test/monniaux/profiling/test_profiling.cm
 delete mode 100644 test/monniaux/profiling/test_profiling.i
 delete mode 100644 test/monniaux/profiling/test_profiling.ltl.1
 delete mode 100644 test/monniaux/profiling/test_profiling.ltl.2
 delete mode 100644 test/monniaux/profiling/test_profiling.mach
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.0
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.1
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.10
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.11
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.12
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.13
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.14
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.15
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.16
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.17
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.18
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.19
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.2
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.20
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.21
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.22
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.23
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.24
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.25
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.26
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.27
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.28
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.29
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.3
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.30
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.31
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.32
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.4
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.5
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.6
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.7
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.8
 delete mode 100644 test/monniaux/profiling/test_profiling.rtl.9

diff --git a/test/monniaux/profiling/test_profiling.alloctrace b/test/monniaux/profiling/test_profiling.alloctrace
deleted file mode 100644
index b61f6fc2..00000000
--- a/test/monniaux/profiling/test_profiling.alloctrace
+++ /dev/null
@@ -1,83 +0,0 @@
--------------- Initial XTL
-
-f() {
-   16:	(x7, x1) = (X1, X0) using x13, x12; 
-   15:	if (x1 <s 2) goto 14 else goto 13
-   14:	x11 = 1; goto 1
-   13:	x6 = int64[x7 + 8]; 
-   12:	X0 = x6; X0 = call "atoi"(X0); x10 = X0; 
-   11:	
-   10:	if (x10 <=s 0) goto 9 else goto 4
-    9:	if (x10 ==s 0) goto 6 else goto 8
-    8:	x3 = "__stringlit_1" + 0; 
-    7:	X0 = x3; X0 = call "printf"(X0); goto 2
-    6:	x9 = "__stringlit_2" + 0; 
-    5:	X0 = x9; X0 = call "printf"(X0); goto 2
-    4:	x5 = "__stringlit_3" + 0; 
-    3:	X0 = x5; X0 = call "printf"(X0); 
-    2:	x11 = 0; 
-    1:	X0 = x11; return X0
-}
-
------------------- Unspillable variables --------------
-
-x12 x13 
-
--------------- After initial register allocation
-
-f() {
-   16:	(x7{X1}, x1{X0}) = (X1, X0) using x13{X2}, x12{D0}; 
-{ x1 x7 }
-   15:	if (x1{X0} <s 2) goto 14 else goto 13
-{ x7 }
-   14:	x11{X0} = 1; goto 1
-{ x11 }
-   13:	x6{X0} = int64[x7{X1} + 8]; 
-{ x6 }
-   12:	X0 = x6{X0}; X0 = call "atoi"(X0); x10{X0} = X0; 
-{ x10 }
-   11:	
-{ x10 }
-   10:	if (x10{X0} <=s 0) goto 9 else goto 4
-{ x10 }
-    9:	if (x10{X0} ==s 0) goto 6 else goto 8
-{ }
-    8:	x3{X0} = "__stringlit_1" + 0; 
-{ x3 }
-    7:	X0 = x3{X0}; X0 = call "printf"(X0); goto 2
-{ }
-    6:	x9{X0} = "__stringlit_2" + 0; 
-{ x9 }
-    5:	X0 = x9{X0}; X0 = call "printf"(X0); goto 2
-{ }
-    4:	x5{X0} = "__stringlit_3" + 0; 
-{ x5 }
-    3:	X0 = x5{X0}; X0 = call "printf"(X0); 
-{ }
-    2:	x11{X0} = 0; 
-{ x11 }
-    1:	X0 = x11{X0}; return X0
-{ }
-}
-
--------------- Candidate allocation
-
-f() {
-   16:	
-   15:	if (X0 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	X0 = 1; goto 1
-   13:	X0 = int64[X1 + 8]; 
-   12:	call "atoi"; 
-   11:	
-   10:	if (X0 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (X0 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	X0 = "__stringlit_1" + 0; 
-    7:	call "printf"; goto 2
-    6:	X0 = "__stringlit_2" + 0; 
-    5:	call "printf"; goto 2
-    4:	X0 = "__stringlit_3" + 0; 
-    3:	call "printf"; 
-    2:	X0 = 0; 
-    1:	return
-}
-
diff --git a/test/monniaux/profiling/test_profiling.cm b/test/monniaux/profiling/test_profiling.cm
deleted file mode 100644
index 2a352510..00000000
--- a/test/monniaux/profiling/test_profiling.cm
+++ /dev/null
@@ -1,112 +0,0 @@
-var "__stringlit_2" readonly {int8 122,int8 101,int8 114,int8 111,int8 10,int8 0}
-var "__stringlit_1" readonly {int8 110,int8 101,int8 103,int8 97,int8 116,int8 105,int8 118,int8 101,int8 10,int8 0}
-var "__stringlit_3" readonly {int8 112,int8 111,int8 115,int8 105,int8 116,int8 105,int8 118,int8 101,int8 10,int8 0}
-
-extern "__builtin_ais_annot" = builtin "__builtin_ais_annot" : long -> void
-extern "__builtin_expect" = builtin "__builtin_expect" : long -> long -> long
-extern "__builtin_bswap64" = builtin "__builtin_bswap64" : long -> long
-extern "__builtin_bswap" = builtin "__builtin_bswap" : int -> int
-extern "__builtin_bswap32" = builtin "__builtin_bswap32" : int -> int
-extern "__builtin_bswap16" = builtin "__builtin_bswap16" : int -> int16u
-extern "__builtin_clz" = builtin "__builtin_clz" : int -> int
-extern "__builtin_clzl" = builtin "__builtin_clzl" : long -> int
-extern "__builtin_clzll" = builtin "__builtin_clzll" : long -> int
-extern "__builtin_ctz" = builtin "__builtin_ctz" : int -> int
-extern "__builtin_ctzl" = builtin "__builtin_ctzl" : long -> int
-extern "__builtin_ctzll" = builtin "__builtin_ctzll" : long -> int
-extern "__builtin_fabs" = builtin "__builtin_fabs" : float -> float
-extern "__builtin_fabsf" = builtin "__builtin_fabsf" : single -> single
-extern "__builtin_fsqrt" = builtin "__builtin_fsqrt" : float -> float
-extern "__builtin_sqrt" = builtin "__builtin_sqrt" : float -> float
-extern "__builtin_memcpy_aligned" = builtin "__builtin_memcpy_aligned" :
-         long -> long -> long -> long -> void
-extern "__builtin_sel" = builtin "__builtin_sel" : int -> void
-extern "__builtin_annot" = builtin "__builtin_annot" : long -> void
-extern "__builtin_annot_intval" = builtin "__builtin_annot_intval" : long ->
-         int -> int
-extern "__builtin_membar" = builtin "__builtin_membar" : void
-extern "__builtin_va_start" = builtin "__builtin_va_start" : long -> void
-extern "__builtin_va_arg" = builtin "__builtin_va_arg" : long -> int -> void
-extern "__builtin_va_copy" = builtin "__builtin_va_copy" : long -> long ->
-         void
-extern "__builtin_va_end" = builtin "__builtin_va_end" : long -> void
-extern "__compcert_va_int32" = extern "__compcert_va_int32" : long -> int
-extern "__compcert_va_int64" = extern "__compcert_va_int64" : long -> long
-extern "__compcert_va_float64" = extern "__compcert_va_float64" : long ->
-         float
-extern "__compcert_va_composite" = extern "__compcert_va_composite" : long ->
-         long -> long
-extern "__compcert_i64_dtos" = runtime "__compcert_i64_dtos" : float -> long
-extern "__compcert_i64_dtou" = runtime "__compcert_i64_dtou" : float -> long
-extern "__compcert_i64_stod" = runtime "__compcert_i64_stod" : long -> float
-extern "__compcert_i64_utod" = runtime "__compcert_i64_utod" : long -> float
-extern "__compcert_i64_stof" = runtime "__compcert_i64_stof" : long -> single
-extern "__compcert_i64_utof" = runtime "__compcert_i64_utof" : long -> single
-extern "__compcert_i64_sdiv" = runtime "__compcert_i64_sdiv" : long ->
-         long -> long
-extern "__compcert_i64_udiv" = runtime "__compcert_i64_udiv" : long ->
-         long -> long
-extern "__compcert_i64_smod" = runtime "__compcert_i64_smod" : long ->
-         long -> long
-extern "__compcert_i64_umod" = runtime "__compcert_i64_umod" : long ->
-         long -> long
-extern "__compcert_i64_shl" = runtime "__compcert_i64_shl" : long -> int ->
-         long
-extern "__compcert_i64_shr" = runtime "__compcert_i64_shr" : long -> int ->
-         long
-extern "__compcert_i64_sar" = runtime "__compcert_i64_sar" : long -> int ->
-         long
-extern "__compcert_i64_smulh" = runtime "__compcert_i64_smulh" : long ->
-         long -> long
-extern "__compcert_i64_umulh" = runtime "__compcert_i64_umulh" : long ->
-         long -> long
-extern "__compcert_i32_sdiv" = runtime "__compcert_i32_sdiv" : int -> int ->
-         int
-extern "__compcert_i32_udiv" = runtime "__compcert_i32_udiv" : int -> int ->
-         int
-extern "__compcert_i32_smod" = runtime "__compcert_i32_smod" : int -> int ->
-         int
-extern "__compcert_i32_umod" = runtime "__compcert_i32_umod" : int -> int ->
-         int
-extern "__compcert_f32_div" = runtime "__compcert_f32_div" : single ->
-         single -> single
-extern "__compcert_f64_div" = runtime "__compcert_f64_div" : float ->
-         float -> float
-extern "__builtin_fence" = builtin "__builtin_fence" : void
-extern "__builtin_cls" = builtin "__builtin_cls" : int -> int
-extern "__builtin_clsl" = builtin "__builtin_clsl" : long -> int
-extern "__builtin_clsll" = builtin "__builtin_clsll" : long -> int
-extern "__builtin_fmadd" = builtin "__builtin_fmadd" : float -> float ->
-         float -> float
-extern "__builtin_fmsub" = builtin "__builtin_fmsub" : float -> float ->
-         float -> float
-extern "__builtin_fnmadd" = builtin "__builtin_fnmadd" : float -> float ->
-         float -> float
-extern "__builtin_fnmsub" = builtin "__builtin_fnmsub" : float -> float ->
-         float -> float
-extern "__builtin_fmax" = builtin "__builtin_fmax" : float -> float -> float
-extern "__builtin_fmin" = builtin "__builtin_fmin" : float -> float -> float
-extern "__builtin_debug" = extern "__builtin_debug" : int -> void
-extern "atoi" = extern "atoi" : long -> int
-extern "printf" = extern "printf" : long -> int
-"main"('argc', 'argv') : int -> long -> int
-{
-  var 'i', '$71';
-  if ('argc' < 2) {
-    return 1;
-  }
-  '$71' = "atoi"(int64['argv' +l 8LL *l longofint 1]) : long -> int;
-  'i' = '$71';
-  if ('i' > 0) {
-    "printf"("__stringlit_3") : long -> int;
-  } else {
-    if ('i' == 0) {
-      "printf"("__stringlit_2") : long -> int;
-    } else {
-      "printf"("__stringlit_1") : long -> int;
-    }
-  }
-  return 0;
-  return 0;
-}
-
diff --git a/test/monniaux/profiling/test_profiling.i b/test/monniaux/profiling/test_profiling.i
deleted file mode 100644
index 35c67916..00000000
--- a/test/monniaux/profiling/test_profiling.i
+++ /dev/null
@@ -1,747 +0,0 @@
-# 1 "test_profiling.c"
-# 1 "<built-in>"
-# 1 "<command-line>"
-# 1 "/usr/aarch64-linux-gnu/include/stdc-predef.h" 1 3
-# 1 "<command-line>" 2
-# 1 "test_profiling.c"
-# 1 "/usr/aarch64-linux-gnu/include/stdlib.h" 1 3
-# 25 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/libc-header-start.h" 1 3
-# 33 "/usr/aarch64-linux-gnu/include/bits/libc-header-start.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/features.h" 1 3
-# 461 "/usr/aarch64-linux-gnu/include/features.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/sys/cdefs.h" 1 3
-# 452 "/usr/aarch64-linux-gnu/include/sys/cdefs.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/wordsize.h" 1 3
-# 453 "/usr/aarch64-linux-gnu/include/sys/cdefs.h" 2 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/long-double.h" 1 3
-# 454 "/usr/aarch64-linux-gnu/include/sys/cdefs.h" 2 3
-# 462 "/usr/aarch64-linux-gnu/include/features.h" 2 3
-# 485 "/usr/aarch64-linux-gnu/include/features.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/gnu/stubs.h" 1 3
-
-
-
-
-# 1 "/usr/aarch64-linux-gnu/include/bits/wordsize.h" 1 3
-# 6 "/usr/aarch64-linux-gnu/include/gnu/stubs.h" 2 3
-
-
-# 1 "/usr/aarch64-linux-gnu/include/gnu/stubs-lp64.h" 1 3
-# 9 "/usr/aarch64-linux-gnu/include/gnu/stubs.h" 2 3
-# 486 "/usr/aarch64-linux-gnu/include/features.h" 2 3
-# 34 "/usr/aarch64-linux-gnu/include/bits/libc-header-start.h" 2 3
-# 26 "/usr/aarch64-linux-gnu/include/stdlib.h" 2 3
-
-
-
-
-
-# 1 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stddef.h" 1 3
-# 67 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stddef.h" 3
-
-# 67 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stddef.h" 3
-typedef unsigned long size_t;
-# 101 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stddef.h" 3
-typedef signed int wchar_t;
-# 32 "/usr/aarch64-linux-gnu/include/stdlib.h" 2 3
-
-
-# 55 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 1 3
-# 23 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/long-double.h" 1 3
-# 24 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 2 3
-# 80 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 3
-typedef long double _Float128;
-# 95 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 1 3
-# 24 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/long-double.h" 1 3
-# 25 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 2 3
-# 214 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 3
-typedef float _Float32;
-# 251 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 3
-typedef double _Float64;
-# 268 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 3
-typedef double _Float32x;
-# 285 "/usr/aarch64-linux-gnu/include/bits/floatn-common.h" 3
-typedef long double _Float64x;
-# 96 "/usr/aarch64-linux-gnu/include/bits/floatn.h" 2 3
-# 56 "/usr/aarch64-linux-gnu/include/stdlib.h" 2 3
-
-
-typedef struct
-  {
-    int quot;
-    int rem;
-  } div_t;
-
-
-
-typedef struct
-  {
-    long int quot;
-    long int rem;
-  } ldiv_t;
-
-
-
-
-
- typedef struct
-  {
-    long long int quot;
-    long long int rem;
-  } lldiv_t;
-# 97 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern size_t __ctype_get_mb_cur_max (void) ;
-
-
-
-extern double atof (const char *__nptr)
-     ;
-
-extern int atoi (const char *__nptr)
-     ;
-
-extern long int atol (const char *__nptr)
-     ;
-
-
-
- extern long long int atoll (const char *__nptr)
-     ;
-
-
-
-extern double strtod (const char *restrict __nptr,
-        char **restrict __endptr)
-     ;
-
-
-
-extern float strtof (const char *restrict __nptr,
-       char **restrict __endptr) ;
-
-extern long double strtold (const char *restrict __nptr,
-       char **restrict __endptr)
-     ;
-# 176 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern long int strtol (const char *restrict __nptr,
-   char **restrict __endptr, int __base)
-     ;
-
-extern unsigned long int strtoul (const char *restrict __nptr,
-      char **restrict __endptr, int __base)
-     ;
-# 199 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-
-extern long long int strtoll (const char *restrict __nptr,
-         char **restrict __endptr, int __base)
-     ;
-
-
-extern unsigned long long int strtoull (const char *restrict __nptr,
-     char **restrict __endptr, int __base)
-     ;
-# 453 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern int rand (void) ;
-
-extern void srand (unsigned int __seed) ;
-# 539 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern void *malloc (size_t __size)
-     ;
-
-extern void *calloc (size_t __nmemb, size_t __size)
-     ;
-
-
-
-
-
-
-extern void *realloc (void *__ptr, size_t __size)
-     ;
-# 565 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern void free (void *__ptr) ;
-# 591 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern void abort (void) ;
-
-
-
-extern int atexit (void (*__func) (void)) ;
-# 617 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern void exit (int __status) ;
-# 629 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern void _Exit (int __status) ;
-
-
-
-
-extern char *getenv (const char *__name) ;
-# 784 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern int system (const char *__command) ;
-# 808 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-typedef int (*__compar_fn_t) (const void *, const void *);
-# 820 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern void *bsearch (const void *__key, const void *__base,
-        size_t __nmemb, size_t __size, __compar_fn_t __compar)
-     ;
-
-
-
-
-
-
-
-extern void qsort (void *__base, size_t __nmemb, size_t __size,
-     __compar_fn_t __compar) ;
-# 840 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern int abs (int __x) ;
-extern long int labs (long int __x) ;
-
-
- extern long long int llabs (long long int __x)
-     ;
-
-
-
-
-
-
-extern div_t div (int __numer, int __denom)
-     ;
-extern ldiv_t ldiv (long int __numer, long int __denom)
-     ;
-
-
- extern lldiv_t lldiv (long long int __numer,
-        long long int __denom)
-     ;
-# 922 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-extern int mblen (const char *__s, size_t __n) ;
-
-
-extern int mbtowc (wchar_t *restrict __pwc,
-     const char *restrict __s, size_t __n) ;
-
-
-extern int wctomb (char *__s, wchar_t __wchar) ;
-
-
-
-extern size_t mbstowcs (wchar_t *restrict __pwcs,
-   const char *restrict __s, size_t __n) ;
-
-extern size_t wcstombs (char *restrict __s,
-   const wchar_t *restrict __pwcs, size_t __n)
-     ;
-# 1013 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/stdlib-float.h" 1 3
-# 1014 "/usr/aarch64-linux-gnu/include/stdlib.h" 2 3
-# 1023 "/usr/aarch64-linux-gnu/include/stdlib.h" 3
-
-# 2 "test_profiling.c" 2
-# 1 "/usr/aarch64-linux-gnu/include/stdio.h" 1 3
-# 27 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/libc-header-start.h" 1 3
-# 28 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
-
-
-
-
-
-# 1 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stddef.h" 1 3
-# 34 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
-
-
-# 1 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stdarg.h" 1 3
-# 43 "/opt/CompCert/kvx-work/2021-04-12_e37d655d/aarch64-linux/lib/compcert/include/stdarg.h" 3
-typedef __builtin_va_list __gnuc_va_list;
-# 37 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
-
-# 1 "/usr/aarch64-linux-gnu/include/bits/types.h" 1 3
-# 27 "/usr/aarch64-linux-gnu/include/bits/types.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/wordsize.h" 1 3
-# 28 "/usr/aarch64-linux-gnu/include/bits/types.h" 2 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/timesize.h" 1 3
-# 19 "/usr/aarch64-linux-gnu/include/bits/timesize.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/wordsize.h" 1 3
-# 20 "/usr/aarch64-linux-gnu/include/bits/timesize.h" 2 3
-# 29 "/usr/aarch64-linux-gnu/include/bits/types.h" 2 3
-
-
-typedef unsigned char __u_char;
-typedef unsigned short int __u_short;
-typedef unsigned int __u_int;
-typedef unsigned long int __u_long;
-
-
-typedef signed char __int8_t;
-typedef unsigned char __uint8_t;
-typedef signed short int __int16_t;
-typedef unsigned short int __uint16_t;
-typedef signed int __int32_t;
-typedef unsigned int __uint32_t;
-
-typedef signed long int __int64_t;
-typedef unsigned long int __uint64_t;
-
-
-
-
-
-
-typedef __int8_t __int_least8_t;
-typedef __uint8_t __uint_least8_t;
-typedef __int16_t __int_least16_t;
-typedef __uint16_t __uint_least16_t;
-typedef __int32_t __int_least32_t;
-typedef __uint32_t __uint_least32_t;
-typedef __int64_t __int_least64_t;
-typedef __uint64_t __uint_least64_t;
-
-
-
-typedef long int __quad_t;
-typedef unsigned long int __u_quad_t;
-
-
-
-
-
-
-
-typedef long int __intmax_t;
-typedef unsigned long int __uintmax_t;
-# 141 "/usr/aarch64-linux-gnu/include/bits/types.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/typesizes.h" 1 3
-# 142 "/usr/aarch64-linux-gnu/include/bits/types.h" 2 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/time64.h" 1 3
-# 143 "/usr/aarch64-linux-gnu/include/bits/types.h" 2 3
-
-
-typedef unsigned long int __dev_t;
-typedef unsigned int __uid_t;
-typedef unsigned int __gid_t;
-typedef unsigned long int __ino_t;
-typedef unsigned long int __ino64_t;
-typedef unsigned int __mode_t;
-typedef unsigned int __nlink_t;
-typedef long int __off_t;
-typedef long int __off64_t;
-typedef int __pid_t;
-typedef struct { int __val[2]; } __fsid_t;
-typedef long int __clock_t;
-typedef unsigned long int __rlim_t;
-typedef unsigned long int __rlim64_t;
-typedef unsigned int __id_t;
-typedef long int __time_t;
-typedef unsigned int __useconds_t;
-typedef long int __suseconds_t;
-
-typedef int __daddr_t;
-typedef int __key_t;
-
-
-typedef int __clockid_t;
-
-
-typedef void * __timer_t;
-
-
-typedef int __blksize_t;
-
-
-
-
-typedef long int __blkcnt_t;
-typedef long int __blkcnt64_t;
-
-
-typedef unsigned long int __fsblkcnt_t;
-typedef unsigned long int __fsblkcnt64_t;
-
-
-typedef unsigned long int __fsfilcnt_t;
-typedef unsigned long int __fsfilcnt64_t;
-
-
-typedef long int __fsword_t;
-
-typedef long int __ssize_t;
-
-
-typedef long int __syscall_slong_t;
-
-typedef unsigned long int __syscall_ulong_t;
-
-
-
-typedef __off64_t __loff_t;
-typedef char *__caddr_t;
-
-
-typedef long int __intptr_t;
-
-
-typedef unsigned int __socklen_t;
-
-
-
-
-typedef int __sig_atomic_t;
-# 39 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/types/__fpos_t.h" 1 3
-
-
-
-
-# 1 "/usr/aarch64-linux-gnu/include/bits/types/__mbstate_t.h" 1 3
-# 13 "/usr/aarch64-linux-gnu/include/bits/types/__mbstate_t.h" 3
-typedef struct
-{
-  int __count;
-  union
-  {
-    unsigned int __wch;
-    char __wchb[4];
-  } __value;
-} __mbstate_t;
-# 6 "/usr/aarch64-linux-gnu/include/bits/types/__fpos_t.h" 2 3
-
-
-
-
-typedef struct _G_fpos_t
-{
-  __off_t __pos;
-  __mbstate_t __state;
-} __fpos_t;
-# 40 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/types/__fpos64_t.h" 1 3
-# 10 "/usr/aarch64-linux-gnu/include/bits/types/__fpos64_t.h" 3
-typedef struct _G_fpos64_t
-{
-  __off64_t __pos;
-  __mbstate_t __state;
-} __fpos64_t;
-# 41 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/types/__FILE.h" 1 3
-
-
-
-struct _IO_FILE;
-typedef struct _IO_FILE __FILE;
-# 42 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/types/FILE.h" 1 3
-
-
-
-struct _IO_FILE;
-
-
-typedef struct _IO_FILE FILE;
-# 43 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/types/struct_FILE.h" 1 3
-# 35 "/usr/aarch64-linux-gnu/include/bits/types/struct_FILE.h" 3
-struct _IO_FILE;
-struct _IO_marker;
-struct _IO_codecvt;
-struct _IO_wide_data;
-
-
-
-
-typedef void _IO_lock_t;
-
-
-
-
-
-struct _IO_FILE
-{
-  int _flags;
-
-
-  char *_IO_read_ptr;
-  char *_IO_read_end;
-  char *_IO_read_base;
-  char *_IO_write_base;
-  char *_IO_write_ptr;
-  char *_IO_write_end;
-  char *_IO_buf_base;
-  char *_IO_buf_end;
-
-
-  char *_IO_save_base;
-  char *_IO_backup_base;
-  char *_IO_save_end;
-
-  struct _IO_marker *_markers;
-
-  struct _IO_FILE *_chain;
-
-  int _fileno;
-  int _flags2;
-  __off_t _old_offset;
-
-
-  unsigned short _cur_column;
-  signed char _vtable_offset;
-  char _shortbuf[1];
-
-  _IO_lock_t *_lock;
-
-
-
-
-
-
-
-  __off64_t _offset;
-
-  struct _IO_codecvt *_codecvt;
-  struct _IO_wide_data *_wide_data;
-  struct _IO_FILE *_freeres_list;
-  void *_freeres_buf;
-  size_t __pad5;
-  int _mode;
-
-  char _unused2[15 * sizeof (int) - 4 * sizeof (void *) - sizeof (size_t)];
-};
-# 44 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
-# 84 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-typedef __fpos_t fpos_t;
-# 133 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-# 1 "/usr/aarch64-linux-gnu/include/bits/stdio_lim.h" 1 3
-# 134 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
-
-
-
-extern FILE *stdin;
-extern FILE *stdout;
-extern FILE *stderr;
-
-
-
-
-
-
-extern int remove (const char *__filename) ;
-
-extern int rename (const char *__old, const char *__new) ;
-# 173 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern FILE *tmpfile (void) ;
-# 187 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern char *tmpnam (char *__s) ;
-# 213 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int fclose (FILE *__stream);
-
-
-
-
-extern int fflush (FILE *__stream);
-# 246 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern FILE *fopen (const char *restrict __filename,
-      const char *restrict __modes) ;
-
-
-
-
-extern FILE *freopen (const char *restrict __filename,
-        const char *restrict __modes,
-        FILE *restrict __stream) ;
-# 304 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern void setbuf (FILE *restrict __stream, char *restrict __buf) ;
-
-
-
-extern int setvbuf (FILE *restrict __stream, char *restrict __buf,
-      int __modes, size_t __n) ;
-# 326 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int fprintf (FILE *restrict __stream,
-      const char *restrict __format, ...);
-
-
-
-
-extern int printf (const char *restrict __format, ...);
-
-extern int sprintf (char *restrict __s,
-      const char *restrict __format, ...) ;
-
-
-
-
-
-extern int vfprintf (FILE *restrict __s, const char *restrict __format,
-       __gnuc_va_list __arg);
-
-
-
-
-extern int vprintf (const char *restrict __format, __gnuc_va_list __arg);
-
-extern int vsprintf (char *restrict __s, const char *restrict __format,
-       __gnuc_va_list __arg) ;
-
-
-
-extern int snprintf (char *restrict __s, size_t __maxlen,
-       const char *restrict __format, ...)
-     ;
-
-extern int vsnprintf (char *restrict __s, size_t __maxlen,
-        const char *restrict __format, __gnuc_va_list __arg)
-     ;
-# 391 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int fscanf (FILE *restrict __stream,
-     const char *restrict __format, ...) ;
-
-
-
-
-extern int scanf (const char *restrict __format, ...) ;
-
-extern int sscanf (const char *restrict __s,
-     const char *restrict __format, ...) ;
-# 416 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int __isoc99_fscanf (FILE *restrict __stream,
-       const char *restrict __format, ...) ;
-extern int __isoc99_scanf (const char *restrict __format, ...) ;
-extern int __isoc99_sscanf (const char *restrict __s,
-       const char *restrict __format, ...) ;
-# 432 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int vfscanf (FILE *restrict __s, const char *restrict __format,
-      __gnuc_va_list __arg)
-     ;
-
-
-
-
-
-extern int vscanf (const char *restrict __format, __gnuc_va_list __arg)
-     ;
-
-
-extern int vsscanf (const char *restrict __s,
-      const char *restrict __format, __gnuc_va_list __arg)
-     ;
-# 465 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int __isoc99_vfscanf (FILE *restrict __s,
-        const char *restrict __format,
-        __gnuc_va_list __arg) ;
-extern int __isoc99_vscanf (const char *restrict __format,
-       __gnuc_va_list __arg) ;
-extern int __isoc99_vsscanf (const char *restrict __s,
-        const char *restrict __format,
-        __gnuc_va_list __arg) ;
-# 485 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int fgetc (FILE *__stream);
-extern int getc (FILE *__stream);
-
-
-
-
-
-extern int getchar (void);
-# 521 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int fputc (int __c, FILE *__stream);
-extern int putc (int __c, FILE *__stream);
-
-
-
-
-
-extern int putchar (int __c);
-# 564 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern char *fgets (char *restrict __s, int __n, FILE *restrict __stream)
-     ;
-# 577 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern char *gets (char *__s) ;
-# 626 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int fputs (const char *restrict __s, FILE *restrict __stream);
-
-
-
-
-
-extern int puts (const char *__s);
-
-
-
-
-
-
-extern int ungetc (int __c, FILE *__stream);
-
-
-
-
-
-
-extern size_t fread (void *restrict __ptr, size_t __size,
-       size_t __n, FILE *restrict __stream) ;
-
-
-
-
-extern size_t fwrite (const void *restrict __ptr, size_t __size,
-        size_t __n, FILE *restrict __s);
-# 684 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int fseek (FILE *__stream, long int __off, int __whence);
-
-
-
-
-extern long int ftell (FILE *__stream) ;
-
-
-
-
-extern void rewind (FILE *__stream);
-# 731 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int fgetpos (FILE *restrict __stream, fpos_t *restrict __pos);
-
-
-
-
-extern int fsetpos (FILE *__stream, const fpos_t *__pos);
-# 757 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern void clearerr (FILE *__stream) ;
-
-extern int feof (FILE *__stream) ;
-
-extern int ferror (FILE *__stream) ;
-# 775 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern void perror (const char *__s);
-
-
-
-
-
-# 1 "/usr/aarch64-linux-gnu/include/bits/sys_errlist.h" 1 3
-# 782 "/usr/aarch64-linux-gnu/include/stdio.h" 2 3
-# 858 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-extern int __uflow (FILE *);
-extern int __overflow (FILE *, int);
-# 873 "/usr/aarch64-linux-gnu/include/stdio.h" 3
-
-# 3 "test_profiling.c" 2
-
-
-# 4 "test_profiling.c"
-int main(int argc, char **argv) {
-  if (argc < 2) return 1;
-  int i = atoi(argv[1]);
-  if (i > 0) {
-    printf("positive\n");
-  } else if (i==0) {
-    printf("zero\n");
-  } else {
-    printf("negative\n");
-  }
-  return 0;
-}
diff --git a/test/monniaux/profiling/test_profiling.ltl.1 b/test/monniaux/profiling/test_profiling.ltl.1
deleted file mode 100644
index fdfb7fe0..00000000
--- a/test/monniaux/profiling/test_profiling.ltl.1
+++ /dev/null
@@ -1,19 +0,0 @@
-main() {
-   16:	
-   15:	if (X0 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	X0 = 1; goto 1
-   13:	X0 = int64[X1 + 8]; 
-   12:	call "atoi"; 
-   11:	
-   10:	if (X0 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (X0 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	X0 = "__stringlit_1" + 0; 
-    7:	call "printf"; goto 2
-    6:	X0 = "__stringlit_2" + 0; 
-    5:	call "printf"; goto 2
-    4:	X0 = "__stringlit_3" + 0; 
-    3:	call "printf"; 
-    2:	X0 = 0; 
-    1:	return
-}
-
diff --git a/test/monniaux/profiling/test_profiling.ltl.2 b/test/monniaux/profiling/test_profiling.ltl.2
deleted file mode 100644
index f9be9feb..00000000
--- a/test/monniaux/profiling/test_profiling.ltl.2
+++ /dev/null
@@ -1,19 +0,0 @@
-main() {
-goto 15   16:	
-   15:	if (X0 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	X0 = 1; goto 1
-   13:	X0 = int64[X1 + 8]; 
-   12:	call "atoi"; goto 10
-   11:	
-   10:	if (X0 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (X0 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	X0 = "__stringlit_1" + 0; 
-    7:	call "printf"; goto 2
-    6:	X0 = "__stringlit_2" + 0; 
-    5:	call "printf"; goto 2
-    4:	X0 = "__stringlit_3" + 0; 
-    3:	call "printf"; 
-    2:	X0 = 0; 
-    1:	return
-}
-
diff --git a/test/monniaux/profiling/test_profiling.mach b/test/monniaux/profiling/test_profiling.mach
deleted file mode 100644
index 31124d94..00000000
--- a/test/monniaux/profiling/test_profiling.mach
+++ /dev/null
@@ -1,20 +0,0 @@
-main() {
-	if (X0 <s 2) goto 14
-	X0 = int64[X1 + 8]
-	call "atoi"
-	if (X0 <=s 0) goto 9
-	X0 = "__stringlit_3" + 0
-	call "printf"
-	goto 2
-   14:	X0 = 1
-	goto 1
-    9:	if (X0 ==s 0) goto 6
-	X0 = "__stringlit_1" + 0
-	call "printf"
-	goto 2
-    6:	X0 = "__stringlit_2" + 0
-	call "printf"
-    2:	X0 = 0
-    1:	return
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.0 b/test/monniaux/profiling/test_profiling.rtl.0
deleted file mode 100644
index d5ce096d..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.0
+++ /dev/null
@@ -1,23 +0,0 @@
-main(x2, x1) {
-   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
-   15:	x5 = 1
-	goto 1
-   14:	x12 = int64[x1 + 8]
-   13:	x3 = "atoi"(x12)
-   12:	x4 = x3
-   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
-   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
-    9:	x10 = "__stringlit_1" + 0
-    8:	x11 = "printf"(x10)
-	goto 3
-    7:	x8 = "__stringlit_2" + 0
-    6:	x9 = "printf"(x8)
-	goto 3
-    5:	x6 = "__stringlit_3" + 0
-    4:	x7 = "printf"(x6)
-    3:	x5 = 0
-	goto 1
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.1 b/test/monniaux/profiling/test_profiling.rtl.1
deleted file mode 100644
index d5ce096d..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.1
+++ /dev/null
@@ -1,23 +0,0 @@
-main(x2, x1) {
-   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
-   15:	x5 = 1
-	goto 1
-   14:	x12 = int64[x1 + 8]
-   13:	x3 = "atoi"(x12)
-   12:	x4 = x3
-   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
-   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
-    9:	x10 = "__stringlit_1" + 0
-    8:	x11 = "printf"(x10)
-	goto 3
-    7:	x8 = "__stringlit_2" + 0
-    6:	x9 = "printf"(x8)
-	goto 3
-    5:	x6 = "__stringlit_3" + 0
-    4:	x7 = "printf"(x6)
-    3:	x5 = 0
-	goto 1
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.10 b/test/monniaux/profiling/test_profiling.rtl.10
deleted file mode 100644
index 8b268c84..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.10
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.11 b/test/monniaux/profiling/test_profiling.rtl.11
deleted file mode 100644
index 8b268c84..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.11
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.12 b/test/monniaux/profiling/test_profiling.rtl.12
deleted file mode 100644
index 8b268c84..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.12
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.13 b/test/monniaux/profiling/test_profiling.rtl.13
deleted file mode 100644
index 8b268c84..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.13
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.14 b/test/monniaux/profiling/test_profiling.rtl.14
deleted file mode 100644
index 8b268c84..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.14
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.15 b/test/monniaux/profiling/test_profiling.rtl.15
deleted file mode 100644
index 8b268c84..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.15
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.16 b/test/monniaux/profiling/test_profiling.rtl.16
deleted file mode 100644
index 8b268c84..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.16
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.17 b/test/monniaux/profiling/test_profiling.rtl.17
deleted file mode 100644
index 8b268c84..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.17
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.18 b/test/monniaux/profiling/test_profiling.rtl.18
deleted file mode 100644
index 8b268c84..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.18
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.19 b/test/monniaux/profiling/test_profiling.rtl.19
deleted file mode 100644
index 091878ec..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.19
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.2 b/test/monniaux/profiling/test_profiling.rtl.2
deleted file mode 100644
index d5ce096d..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.2
+++ /dev/null
@@ -1,23 +0,0 @@
-main(x2, x1) {
-   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
-   15:	x5 = 1
-	goto 1
-   14:	x12 = int64[x1 + 8]
-   13:	x3 = "atoi"(x12)
-   12:	x4 = x3
-   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
-   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
-    9:	x10 = "__stringlit_1" + 0
-    8:	x11 = "printf"(x10)
-	goto 3
-    7:	x8 = "__stringlit_2" + 0
-    6:	x9 = "printf"(x8)
-	goto 3
-    5:	x6 = "__stringlit_3" + 0
-    4:	x7 = "printf"(x6)
-    3:	x5 = 0
-	goto 1
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.20 b/test/monniaux/profiling/test_profiling.rtl.20
deleted file mode 100644
index 091878ec..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.20
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.21 b/test/monniaux/profiling/test_profiling.rtl.21
deleted file mode 100644
index 091878ec..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.21
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.22 b/test/monniaux/profiling/test_profiling.rtl.22
deleted file mode 100644
index 9102f74f..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.22
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	nop
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.23 b/test/monniaux/profiling/test_profiling.rtl.23
deleted file mode 100644
index 9102f74f..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.23
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	nop
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.24 b/test/monniaux/profiling/test_profiling.rtl.24
deleted file mode 100644
index 9102f74f..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.24
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	nop
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.25 b/test/monniaux/profiling/test_profiling.rtl.25
deleted file mode 100644
index 9102f74f..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.25
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	nop
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.26 b/test/monniaux/profiling/test_profiling.rtl.26
deleted file mode 100644
index 9102f74f..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.26
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	nop
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.27 b/test/monniaux/profiling/test_profiling.rtl.27
deleted file mode 100644
index 9102f74f..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.27
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	nop
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.28 b/test/monniaux/profiling/test_profiling.rtl.28
deleted file mode 100644
index 9102f74f..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.28
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	nop
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.29 b/test/monniaux/profiling/test_profiling.rtl.29
deleted file mode 100644
index 9102f74f..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.29
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	nop
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.3 b/test/monniaux/profiling/test_profiling.rtl.3
deleted file mode 100644
index d5ce096d..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.3
+++ /dev/null
@@ -1,23 +0,0 @@
-main(x2, x1) {
-   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
-   15:	x5 = 1
-	goto 1
-   14:	x12 = int64[x1 + 8]
-   13:	x3 = "atoi"(x12)
-   12:	x4 = x3
-   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
-   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
-    9:	x10 = "__stringlit_1" + 0
-    8:	x11 = "printf"(x10)
-	goto 3
-    7:	x8 = "__stringlit_2" + 0
-    6:	x9 = "printf"(x8)
-	goto 3
-    5:	x6 = "__stringlit_3" + 0
-    4:	x7 = "printf"(x6)
-    3:	x5 = 0
-	goto 1
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.30 b/test/monniaux/profiling/test_profiling.rtl.30
deleted file mode 100644
index 9102f74f..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.30
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	nop
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.31 b/test/monniaux/profiling/test_profiling.rtl.31
deleted file mode 100644
index 9102f74f..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.31
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	nop
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.32 b/test/monniaux/profiling/test_profiling.rtl.32
deleted file mode 100644
index 9102f74f..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.32
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	nop
-   10:	if (x3 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x3 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.4 b/test/monniaux/profiling/test_profiling.rtl.4
deleted file mode 100644
index d5ce096d..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.4
+++ /dev/null
@@ -1,23 +0,0 @@
-main(x2, x1) {
-   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
-   15:	x5 = 1
-	goto 1
-   14:	x12 = int64[x1 + 8]
-   13:	x3 = "atoi"(x12)
-   12:	x4 = x3
-   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
-   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
-    9:	x10 = "__stringlit_1" + 0
-    8:	x11 = "printf"(x10)
-	goto 3
-    7:	x8 = "__stringlit_2" + 0
-    6:	x9 = "printf"(x8)
-	goto 3
-    5:	x6 = "__stringlit_3" + 0
-    4:	x7 = "printf"(x6)
-    3:	x5 = 0
-	goto 1
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.5 b/test/monniaux/profiling/test_profiling.rtl.5
deleted file mode 100644
index d5ce096d..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.5
+++ /dev/null
@@ -1,23 +0,0 @@
-main(x2, x1) {
-   16:	if (x2 <s 2) goto 15 else goto 14 (prediction: none)
-   15:	x5 = 1
-	goto 1
-   14:	x12 = int64[x1 + 8]
-   13:	x3 = "atoi"(x12)
-   12:	x4 = x3
-   11:	if (x4 >s 0) goto 5 else goto 10 (prediction: none)
-   10:	if (x4 ==s 0) goto 7 else goto 9 (prediction: none)
-    9:	x10 = "__stringlit_1" + 0
-    8:	x11 = "printf"(x10)
-	goto 3
-    7:	x8 = "__stringlit_2" + 0
-    6:	x9 = "printf"(x8)
-	goto 3
-    5:	x6 = "__stringlit_3" + 0
-    4:	x7 = "printf"(x6)
-    3:	x5 = 0
-	goto 1
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.6 b/test/monniaux/profiling/test_profiling.rtl.6
deleted file mode 100644
index 2f75aa61..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.6
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: none)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 >s 0) goto 4 else goto 9 (prediction: none)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.7 b/test/monniaux/profiling/test_profiling.rtl.7
deleted file mode 100644
index 2f75aa61..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.7
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: none)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 >s 0) goto 4 else goto 9 (prediction: none)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.8 b/test/monniaux/profiling/test_profiling.rtl.8
deleted file mode 100644
index 8b268c84..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.8
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
diff --git a/test/monniaux/profiling/test_profiling.rtl.9 b/test/monniaux/profiling/test_profiling.rtl.9
deleted file mode 100644
index 8b268c84..00000000
--- a/test/monniaux/profiling/test_profiling.rtl.9
+++ /dev/null
@@ -1,21 +0,0 @@
-main(x2, x1) {
-   15:	if (x2 <s 2) goto 14 else goto 13 (prediction: fallthrough)
-   14:	x5 = 1
-	goto 1
-   13:	x12 = int64[x1 + 8]
-   12:	x3 = "atoi"(x12)
-   11:	x4 = x3
-   10:	if (x4 <=s 0) goto 9 else goto 4 (prediction: fallthrough)
-    9:	if (x4 ==s 0) goto 6 else goto 8 (prediction: none)
-    8:	x10 = "__stringlit_1" + 0
-    7:	x11 = "printf"(x10)
-	goto 2
-    6:	x8 = "__stringlit_2" + 0
-    5:	x9 = "printf"(x8)
-	goto 2
-    4:	x6 = "__stringlit_3" + 0
-    3:	x7 = "printf"(x6)
-    2:	x5 = 0
-    1:	return x5
-}
-
-- 
cgit 


From d53cc13b6e47843ebaf4b23c8b03dcef34f331f1 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 13 Apr 2021 15:04:34 +0200
Subject: Adding distinction between kvx-cos and kvx-mbr (for trapping loads)

---
 Makefile                 |  1 +
 configure                |  1 +
 cparser/Machine.ml       | 12 ++++++++++--
 cparser/Machine.mli      |  3 ++-
 driver/Configuration.ml  |  1 +
 driver/Configuration.mli |  3 +++
 driver/Frontend.ml       |  5 ++++-
 7 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index fd0595d4..62635d70 100644
--- a/Makefile
+++ b/Makefile
@@ -297,6 +297,7 @@ compcert.ini: Makefile.config
 	 echo "linker_options=$(CLINKER_OPTIONS)";\
          echo "arch=$(ARCH)"; \
          echo "model=$(MODEL)"; \
+	       echo "os=$(OS)"; \
          echo "abi=$(ABI)"; \
          echo "endianness=$(ENDIANNESS)"; \
          echo "system=$(SYSTEM)"; \
diff --git a/configure b/configure
index 812ad6f7..e8ebb6f8 100755
--- a/configure
+++ b/configure
@@ -710,6 +710,7 @@ HAS_STANDARD_HEADERS=$has_standard_headers
 INSTALL_COQDEV=$install_coqdev
 LIBMATH=$libmath
 MODEL=$model
+OS=${os:-unspecified}
 SYSTEM=$system
 RESPONSEFILE=$responsefile
 LIBRARY_FLOCQ=$library_Flocq
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 73b71ea0..4f5a93d2 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -242,7 +242,7 @@ let rv64 =
                    struct_passing_style = SP_ref_callee; (* Wrong *)
                    struct_return_style = SR_ref } (* to check *)
 
-let kvx =
+let kvxbase =
   { name = "kvx";
     char_signed = true;
     wchar_signed = true;
@@ -275,7 +275,15 @@ let kvx =
     supports_unaligned_accesses = true;
     struct_passing_style = SP_value32_ref_callee;
     struct_return_style = SR_int1to4;
-    has_non_trapping_loads = true;
+    has_non_trapping_loads = false;
+}
+
+let kvxcos =
+  { kvxbase with has_non_trapping_loads = false;
+}
+
+let kvxmbr =
+  { kvxbase with has_non_trapping_loads = true;
 }
 
 let aarch64 =
diff --git a/cparser/Machine.mli b/cparser/Machine.mli
index 54436758..07b55832 100644
--- a/cparser/Machine.mli
+++ b/cparser/Machine.mli
@@ -88,7 +88,8 @@ val arm_littleendian : t
 val arm_bigendian : t
 val rv32 : t
 val rv64 : t
-val kvx : t
+val kvxmbr : t
+val kvxcos : t
 val aarch64 : t
 
 val gcc_extensions : t -> t
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 1d40214a..ecc2aba6 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -126,6 +126,7 @@ let arch =
   | "powerpc"|"arm"|"x86"|"riscV"|"kvx"|"aarch64" as a -> a
   | v -> bad_config "arch" [v]
 let model = get_config_string "model"
+let os = get_config_string "os"
 let abi = get_config_string "abi"
 let is_big_endian =
   match get_config_string "endianness" with
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index a71da72d..75e547ff 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -19,6 +19,9 @@ val model: string
 val abi: string
   (** ABI to use *)
 
+val os: string
+  (** ABI to use *)
+
 val is_big_endian: bool
   (** Endianness to use *)
 
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index c99da945..c8890046 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -117,7 +117,10 @@ let init () =
     | "riscV"   -> if Configuration.model = "64"
                    then Machine.rv64
                    else Machine.rv32
-    | "kvx" -> Machine.kvx
+    | "kvx" -> if Configuration.os = "cos" then Machine.kvxcos
+               else if Configuration.os = "mbr" then Machine.kvxmbr
+               else (Printf.eprintf "Configuration OS = %s\n" Configuration.os;
+                 failwith "Wrong OS configuration for KVX")
     | "aarch64" -> Machine.aarch64
     | _         -> assert false
   end;
-- 
cgit 


From 47eaaa2360337ed2b518f276a616529895da63e8 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 13 Apr 2021 15:05:01 +0200
Subject: Recording of prediction stats with COMPCERT_PROFILING_STATS
 environment flag

It only works correctly if both profiling and static prediction are
used: it then compares both and gives stats in COMPCERT_PREDICT_STATS
file.

The stats are of the form:
  total correct mispredicts missed

total = number of total CBs encountered
correct = number of correct predictions
mispredicts = times when static prediction did a wrong guess (predicted
    the opposite from profiling, or predicted Some _ when profiling said
    None)
missed = times when static prediction was not able to give a verdict,
       though the profiling gave one
---
 backend/Duplicateaux.ml | 126 +++++++++++++++++++++++++++++++++++-------------
 1 file changed, 93 insertions(+), 33 deletions(-)

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index b3635527..62805d5b 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -24,6 +24,45 @@ open Maps
 open Camlcoq
 open DebugPrint
 
+let stats_oc = ref None
+
+let set_stats_oc () =
+  try
+    let name = Sys.getenv "COMPCERT_PREDICT_STATS" in
+    let oc = open_out_gen [Open_append; Open_creat; Open_text] 0o666 name in
+    stats_oc := Some oc
+  with Not_found -> ()
+
+(* number of total CBs *)
+let stats_nb_total = ref 0
+(* we predicted the same thing as the profiling *)
+let stats_nb_correct_predicts = ref 0
+(* we predicted something (say Some true), but the profiling predicted the opposite (say Some false, or None) *)
+let stats_nb_mispredicts = ref 0
+(* we did not predict anything (None) even though the profiling did predict something *)
+let stats_nb_missed_opportunities = ref 0
+
+let reset_stats () = begin
+  stats_nb_total := 0;
+  stats_nb_correct_predicts := 0;
+  stats_nb_mispredicts := 0;
+  stats_nb_missed_opportunities := 0;
+end
+
+let incr theref = theref := !theref + 1
+
+let has_some o = match o with Some _ -> true | None -> false
+
+let stats_oc_recording () = has_some !stats_oc
+
+let write_stats_oc () =
+  match !stats_oc with
+  | None -> ()
+  | Some oc -> begin
+      Printf.fprintf oc "%d %d %d %d\n" !stats_nb_total !stats_nb_correct_predicts !stats_nb_mispredicts !stats_nb_missed_opportunities;
+      close_out oc
+    end
+
 let get_loop_headers = LICMaux.get_loop_headers
 let get_some = LICMaux.get_some
 let rtl_successors = LICMaux.rtl_successors
@@ -397,28 +436,27 @@ let get_directions f code entrypoint = begin
     (* debug "\n"; *)
     List.iter (fun n ->
       match (get_some @@ PTree.get n code) with
-      | Icond (cond, lr, ifso, ifnot, pred) ->
-          (match pred with Some _ -> debug "RTL node %d already has prediction information\n" (P.to_int n)
-          | None ->
-          (* debug "Analyzing %d.." (P.to_int n); *)
-          let heuristics = [ do_opcode_heuristic;
-            do_return_heuristic; do_loop2_heuristic loop_info n; do_loop_heuristic; do_call_heuristic;
-             (* do_store_heuristic *) ] in
-          let preferred = ref None in
-          begin
-            debug "Deciding condition for RTL node %d\n" (P.to_int n);
-            List.iter (fun do_heur ->
-              match !preferred with
-              | None -> preferred := do_heur code cond ifso ifnot is_loop_header
-              | Some _ -> ()
-            ) heuristics;
-            directions := PTree.set n !preferred !directions;
-            (match !preferred with | Some false -> debug "\tFALLTHROUGH\n"
-                                   | Some true -> debug "\tBRANCH\n"
-                                   | None -> debug "\tUNSURE\n");
-            debug "---------------------------------------\n"
-          end
-          )
+      | Icond (cond, lr, ifso, ifnot, pred) -> begin
+          if stats_oc_recording () || not @@ has_some pred then
+            (* debug "Analyzing %d.." (P.to_int n); *)
+            let heuristics = [ do_opcode_heuristic;
+              do_return_heuristic; do_loop2_heuristic loop_info n; do_loop_heuristic; do_call_heuristic;
+               (* do_store_heuristic *) ] in
+            let preferred = ref None in
+            begin
+              debug "Deciding condition for RTL node %d\n" (P.to_int n);
+              List.iter (fun do_heur ->
+                match !preferred with
+                | None -> preferred := do_heur code cond ifso ifnot is_loop_header
+                | Some _ -> ()
+              ) heuristics;
+              directions := PTree.set n !preferred !directions;
+              (match !preferred with | Some false -> debug "\tFALLTHROUGH\n"
+                                     | Some true -> debug "\tBRANCH\n"
+                                     | None -> debug "\tUNSURE\n");
+              debug "---------------------------------------\n"
+            end
+        end
       | _ -> ()
     ) bfs_order;
     !directions
@@ -426,11 +464,28 @@ let get_directions f code entrypoint = begin
 end
 
 let update_direction direction = function
-| Icond (cond, lr, n, n', pred) ->
+| Icond (cond, lr, n, n', pred) -> begin
+    (* Counting stats from profiling *)
+    if stats_oc_recording () then begin
+      incr stats_nb_total;
+      match pred, direction with
+      | None, None -> incr stats_nb_correct_predicts
+      | None, Some _ -> incr stats_nb_mispredicts
+      | Some _, None -> incr stats_nb_missed_opportunities
+      | Some false, Some false -> incr stats_nb_correct_predicts
+      | Some false, Some true -> incr stats_nb_mispredicts
+      | Some true, Some false -> incr stats_nb_mispredicts
+      | Some true, Some true -> incr stats_nb_correct_predicts
+    end;
+
     (* only update if there is no prior existing branch prediction *)
     (match pred with
     | None -> Icond (cond, lr, n, n', direction)
-    | Some _ -> Icond (cond, lr, n, n', pred) )
+    | Some _ -> begin
+        Icond (cond, lr, n, n', pred) 
+      end
+    )
+    end
 | i -> i
 
 (* Uses branch prediction to write prediction annotations in Icond *)
@@ -1026,15 +1081,20 @@ let static_predict f =
   let entrypoint = f.fn_entrypoint in
   let code = f.fn_code in
   let revmap = make_identity_ptree code in
-  let code =
-    if !Clflags.option_fpredict then
-      update_directions f code entrypoint
-    else code in
-  let code =
-    if !Clflags.option_fpredict then
-      invert_iconds code
-    else code in
-  ((code, entrypoint), revmap)
+  begin
+    reset_stats ();
+    set_stats_oc ();
+    let code =
+      if !Clflags.option_fpredict then
+        update_directions f code entrypoint
+      else code in
+    write_stats_oc ();
+    let code =
+      if !Clflags.option_fpredict then
+        invert_iconds code
+      else code in
+    ((code, entrypoint), revmap)
+  end
 
 let unroll_single f =
   let entrypoint = f.fn_entrypoint in
-- 
cgit 


From 5500fccca01d097f70a5cc708daf07395626fd6b Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 13 Apr 2021 16:09:55 +0200
Subject: Adding overpredicts

---
 backend/Duplicateaux.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 62805d5b..c8690d46 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -37,16 +37,19 @@ let set_stats_oc () =
 let stats_nb_total = ref 0
 (* we predicted the same thing as the profiling *)
 let stats_nb_correct_predicts = ref 0
-(* we predicted something (say Some true), but the profiling predicted the opposite (say Some false, or None) *)
+(* we predicted something (say Some true), but the profiling predicted the opposite (say Some false) *)
 let stats_nb_mispredicts = ref 0
 (* we did not predict anything (None) even though the profiling did predict something *)
 let stats_nb_missed_opportunities = ref 0
+(* we predicted something (say Some true) but the profiling preferred not to predict anything (None) *)
+let stats_nb_overpredict = ref 0
 
 let reset_stats () = begin
   stats_nb_total := 0;
   stats_nb_correct_predicts := 0;
   stats_nb_mispredicts := 0;
   stats_nb_missed_opportunities := 0;
+  stats_nb_overpredict := 0;
 end
 
 let incr theref = theref := !theref + 1
@@ -59,7 +62,7 @@ let write_stats_oc () =
   match !stats_oc with
   | None -> ()
   | Some oc -> begin
-      Printf.fprintf oc "%d %d %d %d\n" !stats_nb_total !stats_nb_correct_predicts !stats_nb_mispredicts !stats_nb_missed_opportunities;
+      Printf.fprintf oc "%d %d %d %d %d\n" !stats_nb_total !stats_nb_correct_predicts !stats_nb_mispredicts !stats_nb_missed_opportunities !stats_nb_overpredict;
       close_out oc
     end
 
@@ -470,7 +473,7 @@ let update_direction direction = function
       incr stats_nb_total;
       match pred, direction with
       | None, None -> incr stats_nb_correct_predicts
-      | None, Some _ -> incr stats_nb_mispredicts
+      | None, Some _ -> incr stats_nb_overpredict
       | Some _, None -> incr stats_nb_missed_opportunities
       | Some false, Some false -> incr stats_nb_correct_predicts
       | Some false, Some true -> incr stats_nb_mispredicts
-- 
cgit 


From 4b61b0985faecdf9c3f873b965bfb207acfc0150 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 13 Apr 2021 17:17:15 +0200
Subject: Adding more precise heuristic measures

---
 backend/Duplicateaux.ml | 64 +++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 62 insertions(+), 2 deletions(-)

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index c8690d46..1f1ebe9f 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -44,12 +44,35 @@ let stats_nb_missed_opportunities = ref 0
 (* we predicted something (say Some true) but the profiling preferred not to predict anything (None) *)
 let stats_nb_overpredict = ref 0
 
+(* heuristic specific counters *)
+let wrong_opcode = ref 0
+let wrong_return = ref 0
+let wrong_loop2 = ref 0
+let wrong_loop = ref 0
+let wrong_call = ref 0
+
+let right_opcode = ref 0
+let right_return = ref 0
+let right_loop2 = ref 0
+let right_loop = ref 0
+let right_call = ref 0
+
 let reset_stats () = begin
   stats_nb_total := 0;
   stats_nb_correct_predicts := 0;
   stats_nb_mispredicts := 0;
   stats_nb_missed_opportunities := 0;
   stats_nb_overpredict := 0;
+  wrong_opcode := 0;
+  wrong_return := 0;
+  wrong_loop2 := 0;
+  wrong_loop := 0;
+  wrong_call := 0;
+  right_opcode := 0;
+  right_return := 0;
+  right_loop2 := 0;
+  right_loop := 0;
+  right_call := 0;
 end
 
 let incr theref = theref := !theref + 1
@@ -62,7 +85,12 @@ let write_stats_oc () =
   match !stats_oc with
   | None -> ()
   | Some oc -> begin
-      Printf.fprintf oc "%d %d %d %d %d\n" !stats_nb_total !stats_nb_correct_predicts !stats_nb_mispredicts !stats_nb_missed_opportunities !stats_nb_overpredict;
+      Printf.fprintf oc "%d %d %d %d %d %d %d %d %d %d %d %d %d %d %d\n" !stats_nb_total
+        !stats_nb_correct_predicts !stats_nb_mispredicts !stats_nb_missed_opportunities
+        !stats_nb_overpredict
+        !wrong_opcode !wrong_return !wrong_loop2 !wrong_loop !wrong_call
+        !right_opcode !right_return !right_loop2 !right_loop !right_call
+        ;
       close_out oc
     end
 
@@ -446,11 +474,43 @@ let get_directions f code entrypoint = begin
               do_return_heuristic; do_loop2_heuristic loop_info n; do_loop_heuristic; do_call_heuristic;
                (* do_store_heuristic *) ] in
             let preferred = ref None in
+            let current_heuristic = ref 0 in
             begin
               debug "Deciding condition for RTL node %d\n" (P.to_int n);
               List.iter (fun do_heur ->
                 match !preferred with
-                | None -> preferred := do_heur code cond ifso ifnot is_loop_header
+                | None -> begin
+                  preferred := do_heur code cond ifso ifnot is_loop_header;
+                  if stats_oc_recording () then begin
+                    (* Getting stats about mispredictions from each heuristic *)
+                    (match !preferred, pred with
+                      | Some false, Some true
+                      | Some true, Some false
+                      (* | Some _, None  *) (* Uncomment for overpredicts *)
+                          -> begin
+                          match !current_heuristic with
+                          | 0 -> incr wrong_opcode
+                          | 1 -> incr wrong_return
+                          | 2 -> incr wrong_loop2
+                          | 3 -> incr wrong_loop
+                          | 4 -> incr wrong_call
+                          | _ -> failwith "Shouldn't happen"
+                          end
+                      | Some false, Some false
+                      | Some true, Some true -> begin
+                          match !current_heuristic with
+                          | 0 -> incr right_opcode
+                          | 1 -> incr right_return
+                          | 2 -> incr right_loop2
+                          | 3 -> incr right_loop
+                          | 4 -> incr right_call
+                          | _ -> failwith "Shouldn't happen"
+                          end
+                      | _ -> ()
+                    );
+                    incr current_heuristic
+                    end
+                  end 
                 | Some _ -> ()
               ) heuristics;
               directions := PTree.set n !preferred !directions;
-- 
cgit 


From a05f92785ffa93e4001d2a2e9a630351593fabc2 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Fri, 16 Apr 2021 18:39:17 +0200
Subject: fix broken link in index-kvx.html

---
 doc/index-kvx.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/index-kvx.html b/doc/index-kvx.html
index 6d56cbdb..62afb423 100644
--- a/doc/index-kvx.html
+++ b/doc/index-kvx.html
@@ -278,7 +278,7 @@ This IR is generic over the processor, even if currently, only used for KVX.
   </TD>
   <TD>RTL to RTL</TD>
   <TD><A HREF="html/compcert.backend.Duplicate.html">Duplicate</A> (generic checker)</TD>
-  <TD><A HREF="html/compcert.scheduling.Duplicateproof.html">Duplicateproof</A> (generic proof)<BR>
+  <TD><A HREF="html/compcert.backend.Duplicateproof.html">Duplicateproof</A> (generic proof)<BR>
     <a href="html/compcert.backend.Duplicatepasses.html">Duplicatepasses</a> (several passes from several oracles)</TD>
 </TR>
 <TR valign="top" style="color:#000000">
-- 
cgit