diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-23 09:00:46 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-23 09:00:46 +0200 |
| commit | dc43cc3371f7837cff5b8d1fd536aba54e99232f (patch) | |
| tree | d9b69f7051ab6d4888e363c56063cd56b6d8eb6c /backend/CSE3analysisaux.ml | |
| parent | 14388a6be6cf7aac50f2af4ff29fe9726ad83435 (diff) | |
| download | compcert-kvx-dc43cc3371f7837cff5b8d1fd536aba54e99232f.tar.gz compcert-kvx-dc43cc3371f7837cff5b8d1fd536aba54e99232f.zip | |
CSE3analysisaux: pp_rhs
Diffstat (limited to 'backend/CSE3analysisaux.ml')
| -rw-r--r-- | backend/CSE3analysisaux.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 23e20ea8..0260f3b1 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -37,6 +37,14 @@ let print_set s = List.iter (fun i -> Printf.printf "%d; " (P.to_int i)) (PSet.elements s); Printf.printf "}\n";; +let pp_rhs oc (sop, args) = + match sop with + | SOp op -> PrintOp.print_operation PrintRTL.reg oc (op, args) + | SLoad(chunk, addr) -> + Printf.fprintf oc "%s[%a]" + (PrintAST.name_of_chunk chunk) + (PrintOp.print_addressing PrintRTL.reg) (addr, args);; + let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let cur_eq_id = ref 0 and cur_catalog = ref PTree.empty @@ -48,6 +56,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let eq_find_oracle node eq = Hashtbl.find_opt eq_table (flatten_eq eq) and rhs_find_oracle node sop args = + (* Printf.printf "query for %a\n" pp_rhs (sop, args); *) match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with | None -> PSet.empty | Some s -> s in |