1 files changed, 112 insertions, 0 deletions
diff --git a/backend/RTLTunnelingaux.ml b/backend/RTLTunnelingaux.ml
new file mode 100644
index 00000000..9333e357
--- /dev/null
+++ b/backend/RTLTunnelingaux.ml
@@ -0,0 +1,112 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé  Grenoble-INP, VERIMAG             *)
+(*           TODO: Proper author information                   *)
+(*                                                             *)
+(*  Copyright VERIMAG. All rights reserved.                    *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(*
+
+This file implements the [branch_target] oracle that identifies "nop" branches in a RTL function,
+and computes their target node with the distance (ie the number of cummulated nops) toward this target.
+
+See [RTLTunneling.v]
+
+*)
+
+open Coqlib
+open RTL
+open Maps
+open Camlcoq
+open Tunnelinglibs
+
+module LANG = struct
+  type code_unit = RTL.instruction
+  type funct = RTL.coq_function
+end
+
+module OPT = struct
+  let langname = "RTL"
+  let limit_tunneling = None
+  let debug_flag = ref false
+  let final_dump = false
+end
+
+module Partial = Tunnelinglibs.Tunneling(LANG)(OPT)
+
+module FUNS = struct
+  let build_simplified_cfg c acc pc i =
+    match i with
+    | Inop s ->
+       let ns = get_node c s in
+       set_branch c pc ns;
+       incr nopcounter;
+       acc
+    | Icond (_, _, s1, s2, _) ->
+       c.num_rems <- c.num_rems + 1;
+       let ns1 = get_node c s1 in
+       let ns2 = get_node c s2 in
+       let npc = get_node c pc in
+       npc.inst <- COND(ns1, ns2);
+       npc::acc
+    | _ -> acc
+
+  let print_code_unit c println (pc, i) =
+    match i with
+    | Inop s -> (if println then Partial.debug "\n");
+        Partial.debug "%d:Inop %d %s\n" pc (P.to_int s) (string_of_labeli c.nodes pc);
+        false
+    | Icond (_, _, s1, s2, _) -> (if println then Partial.debug "\n");
+        Partial.debug "%d:Icond (%d,%d) %s\n" pc (P.to_int s1) (P.to_int s2) (string_of_labeli c.nodes pc);
+        false
+    | _ -> Partial.debug "%d " pc;
+        true
+
+  let fn_code f = f.fn_code
+  let fn_entrypoint f = f.fn_entrypoint
+
+
+  (*************************************************************)
+  (* Copy-paste of the extracted code of the verifier          *)
+  (* with [raise (BugOnPC (P.to_int pc))] instead of [Error.*] *)
+
+  let check_code_unit td pc i =
+    match PTree.get pc td with
+    | Some p ->
+        let (tpc, dpc) = p in
+        let dpc0 = dpc in begin
+          match i with
+          | Inop s ->
+            let (ts, ds) = get td s in
+            if peq tpc ts
+            then if zlt ds dpc0
+                 then ()
+                 else raise (BugOnPC (P.to_int pc))
+            else raise (BugOnPC (P.to_int pc))
+          | Icond (_, _, s1, s2, _) ->
+            let (ts1, ds1) = get td s1 in
+            let (ts2, ds2) = get td s2 in
+            if peq tpc ts1
+            then if peq tpc ts2
+                 then if zlt ds1 dpc0
+                      then if zlt ds2 dpc0
+                           then ()
+                           else raise (BugOnPC (P.to_int pc))
+                      else raise (BugOnPC (P.to_int pc))
+                 else raise (BugOnPC (P.to_int pc))
+            else raise (BugOnPC (P.to_int pc))
+          | _ ->
+            raise (BugOnPC (P.to_int pc)) end
+    | None -> ()
+
+end
+
+module T = Partial.T(FUNS)
+let branch_target = T.branch_target
+