From 59413cb4018d09fb3b641a49ab062bc933d5274c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 10 Mar 2020 19:56:30 +0100 Subject: starts compiling but still fake --- backend/CSE3analysisaux.ml | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 backend/CSE3analysisaux.ml (limited to 'backend/CSE3analysisaux.ml') diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml new file mode 100644 index 00000000..26f19fd6 --- /dev/null +++ b/backend/CSE3analysisaux.ml @@ -0,0 +1,36 @@ +open CSE3analysis +open Maps +open HashedSet +open Camlcoq + +let flatten_eq eq = + ((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);; + +let preanalysis (f : RTL.coq_function) = + let cur_eq_id = ref 0 + and cur_catalog = ref PTree.empty + and eq_table = Hashtbl.create 100 + and rhs_table = Hashtbl.create 100 + and cur_kill_reg = ref (PMap.init PSet.empty) + and cur_kill_mem = ref PSet.empty + and cur_moves = ref (PMap.init PSet.empty) in + let eq_find_oracle node eq = + Hashtbl.find_opt eq_table (flatten_eq eq) + and rhs_find_oracle node sop args = + match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with + | None -> PSet.empty + | Some s -> s in + let mutating_eq_find_oracle node eq = + incr cur_eq_id; None in (* FIXME *) + ignore + (internal_analysis + { eq_catalog = (fun eq_id -> PTree.get eq_id !cur_catalog); + eq_find_oracle = mutating_eq_find_oracle; + eq_rhs_oracle = rhs_find_oracle ; + eq_kill_reg = (fun reg -> PMap.get reg !cur_kill_reg); + eq_kill_mem = (fun () -> !cur_kill_mem); + eq_moves = (fun reg -> PMap.get reg !cur_moves) + } f); + { hint_eq_catalog = !cur_catalog; + hint_eq_find_oracle= eq_find_oracle; + hint_eq_rhs_oracle = rhs_find_oracle };; -- cgit