From e3e33a26c5ddb7c7747da67aa36fd56d0386f3c8 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 10 Mar 2020 20:50:25 +0100
Subject: printing created hashes

---
 backend/CSE3analysisaux.ml | 56 ++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 54 insertions(+), 2 deletions(-)

(limited to 'backend/CSE3analysisaux.ml')

diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index 26f19fd6..8229a76d 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -6,6 +6,33 @@ open Camlcoq
 let flatten_eq eq =
   ((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);;
 
+let imp_add_i_j s i j =
+  s := PMap.set i (PSet.add j (PMap.get i !s)) !s;;
+
+let string_of_chunk = function
+    | AST.Mint8signed -> "int8signed"
+    | AST.Mint8unsigned -> "int8unsigned"
+    | AST.Mint16signed -> "int16signed"
+    | AST.Mint16unsigned -> "int16unsigned"
+    | AST.Mint32 -> "int32"
+    | AST.Mint64 -> "int64"
+    | AST.Mfloat32 -> "float32"
+    | AST.Mfloat64 -> "float64"
+    | AST.Many32 -> "any32"
+    | AST.Many64 -> "any64";;
+
+let print_reg channel i =
+  Printf.fprintf channel "r%d" i;;
+
+let print_eq channel id (lhs, sop, args) =
+  Printf.printf "%d: " id;
+  match sop with
+  | SOp op ->
+     Printf.printf "%a = %a\n" print_reg lhs (PrintOp.print_operation print_reg) (op, args)
+  | SLoad(chunk, addr) ->
+     Printf.printf "%a = %s @ %a\n" print_reg lhs (string_of_chunk chunk)
+       (PrintOp.print_addressing print_reg) (addr, args);;
+
 let preanalysis (f : RTL.coq_function) =
   let cur_eq_id = ref 0
   and cur_catalog = ref PTree.empty
@@ -20,8 +47,33 @@ let preanalysis (f : RTL.coq_function) =
     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 *)
+  let mutating_eq_find_oracle node eq : P.t option =
+    let (flat_eq_lhs, flat_eq_op, flat_eq_args) as flat_eq = flatten_eq eq in
+    match Hashtbl.find_opt eq_table flat_eq with
+    | Some x -> Some x
+    | None ->
+       incr cur_eq_id;
+       let id = !cur_eq_id in
+       let coq_id = P.of_int id in
+       begin
+         print_eq stderr id flat_eq;
+         Hashtbl.add eq_table flat_eq coq_id;
+         Hashtbl.add rhs_table (flat_eq_op, flat_eq_args)
+           (PSet.add coq_id
+              (match Hashtbl.find_opt rhs_table (flat_eq_op, flat_eq_args) with
+               | None -> PSet.empty
+               | Some s -> s));
+         List.iter
+           (fun reg -> imp_add_i_j cur_kill_reg reg coq_id)
+           (eq.eq_lhs :: eq.eq_args);
+         (if eq_depends_on_mem eq
+          then cur_kill_mem := PSet.add coq_id !cur_kill_mem);
+         (match eq.eq_op, eq.eq_args with
+          | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves eq.eq_lhs coq_id
+          | _, _ -> ());
+         Some coq_id
+       end
+  in
   ignore 
     (internal_analysis
       { eq_catalog     = (fun eq_id -> PTree.get eq_id !cur_catalog);
-- 
cgit