diff options
| -rw-r--r-- | backend/CSE3analysisaux.ml | 56 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 |
2 files changed, 55 insertions, 3 deletions
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); diff --git a/extraction/extraction.v b/extraction/extraction.v index 61c7c746..bf51da42 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -193,7 +193,7 @@ Set Extraction AccessOpaque. Cd "extraction". Separate Extraction - CSE3analysis.internal_analysis CSE3.run + CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem CSE3.run Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env |