reloading and exploiting seems to work

1 files changed, 30 insertions, 0 deletions

diff --git a/backend/ProfilingExploit.v b/backend/ProfilingExploit.v
new file mode 100644
index 00000000..cfca1a12
--- /dev/null
+++ b/backend/ProfilingExploit.v
@@ -0,0 +1,30 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL.
+
+Local Open Scope positive.
+
+Parameter function_id : function -> AST.profiling_id.
+Parameter branch_id : AST.profiling_id -> node -> AST.profiling_id.
+Parameter condition_oracle : AST.profiling_id -> option bool.
+
+Definition transf_instr (f_id : AST.profiling_id)
+           (pc : node) (i : instruction) : instruction :=
+  match i with
+  | Icond cond args ifso ifnot None =>
+    Icond cond args ifso ifnot (condition_oracle (branch_id f_id pc))
+  | _ => i
+  end.
+
+Definition transf_function (f : function) : function :=
+  {| fn_sig := f.(fn_sig);
+     fn_params := f.(fn_params);
+     fn_stacksize := f.(fn_stacksize);
+     fn_code := PTree.map (transf_instr (function_id f)) f.(fn_code);
+     fn_entrypoint := f.(fn_entrypoint) |}.
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.