diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-01 17:18:50 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-01 17:18:50 +0200 |
commit | 34bb4b19299e21e87871c7159567ac425c70e6b4 (patch) | |
tree | 017443c2bcb31f5a9e52e2db43f0c2e078d16258 /backend/LICMaux.ml | |
parent | aebbc43842ec0c49058b718c685e08edf11ce614 (diff) | |
download | compcert-kvx-34bb4b19299e21e87871c7159567ac425c70e6b4.tar.gz compcert-kvx-34bb4b19299e21e87871c7159567ac425c70e6b4.zip |
toy example for injecting code
Diffstat (limited to 'backend/LICMaux.ml')
-rw-r--r-- | backend/LICMaux.ml | 31 |
1 files changed, 29 insertions, 2 deletions
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;; |