From 34bb4b19299e21e87871c7159567ac425c70e6b4 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 1 Apr 2020 17:18:50 +0200
Subject: toy example for injecting code

---
 backend/LICMaux.ml | 31 +++++++++++++++++++++++++++++--
 1 file changed, 29 insertions(+), 2 deletions(-)

(limited to 'backend/LICMaux.ml')

diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml
index 542b6ea8..3f7d61b1 100644
--- a/backend/LICMaux.ml
+++ b/backend/LICMaux.ml
@@ -1,4 +1,31 @@
 open RTL;;
+open Camlcoq;;
+open Maps;;
+open Integers;;
 
-let gen_injections (f : function) (max_pc : node) (max_reg : reg) =
-  PTree.empty;;
+type reg = P.t;;
+
+module IntSet = Set.Make(struct type t=int let compare = (-) end);;
+
+let loop_headers (f : coq_function) =
+  PTree.fold (fun (already : IntSet.t)
+                  (coq_pc : node) (instr : instruction) ->
+      let pc = P.to_int coq_pc in
+      List.fold_left (fun (already : IntSet.t) (coq_pc' : node) ->
+          let pc' = P.to_int coq_pc' in
+          if pc' >= pc
+          then IntSet.add pc' already
+          else already) already (successors_instr instr))
+    f.fn_code IntSet.empty;;
+
+let print_loop_headers f =
+  print_endline "Loop headers";
+  IntSet.iter
+    (fun i -> Printf.printf "%d " i)
+    (loop_headers f);
+  print_newline ();;
+
+let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg):
+  (Inject.inj_instr list) PTree.t =
+  let max_reg = P.to_int coq_max_reg in
+  PTree.set coq_max_pc [Inject.INJload(AST.Mint32, (Op.Aindexed (Ptrofs.of_int (Z.of_sint 0))), [P.of_int 1], P.of_int (max_reg+1))] PTree.empty;;
-- 
cgit