diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-11 12:55:40 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-11 12:56:55 +0100 |
| commit | ca1536a5d9e850cf9c86a70f421412d2c7bdff38 (patch) | |
| tree | 937a61cee71ca6cc42e5a053dfad0c843a35eae7 /backend/CSE3analysisaux.ml | |
| parent | 2231fe82a807cebab5cae495ed08cda17810efdc (diff) | |
| download | compcert-kvx-ca1536a5d9e850cf9c86a70f421412d2c7bdff38.tar.gz compcert-kvx-ca1536a5d9e850cf9c86a70f421412d2c7bdff38.zip | |
fix in catalog handling
Diffstat (limited to 'backend/CSE3analysisaux.ml')
| -rw-r--r-- | backend/CSE3analysisaux.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 2e7d7063..f3c7d9b9 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -32,6 +32,11 @@ let print_eq channel (lhs, sop, args) = Printf.printf "%a = %s @ %a\n" print_reg lhs (string_of_chunk chunk) (PrintOp.print_addressing print_reg) (addr, args);; +let print_set s = + Printf.printf "{ "; + List.iter (fun i -> Printf.printf "%d; " (P.to_int i)) (PSet.elements s); + Printf.printf "}\n";; + let preanalysis (f : RTL.coq_function) = let cur_eq_id = ref 0 and cur_catalog = ref PTree.empty @@ -52,12 +57,13 @@ let preanalysis (f : RTL.coq_function) = | Some x -> Some x | None -> - (* FIXME print_eq stderr flat_eq; *) + (* TODO print_eq stderr flat_eq; *) incr cur_eq_id; let id = !cur_eq_id in let coq_id = P.of_int id in begin Hashtbl.add eq_table flat_eq coq_id; + (cur_catalog := PTree.set coq_id eq !cur_catalog); 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 |