diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-14 21:56:30 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-14 21:56:30 +0200 |
| commit | 7c6ce18466ed1de58a0f99c785c777d63a9a6149 (patch) | |
| tree | c1afac8e4b12fc833b4da838abbd38eca3f98be0 /backend/CSE3analysisaux.ml | |
| parent | 1050bb788994cd6944770bf754230f4c90d9442b (diff) | |
| download | compcert-kvx-7c6ce18466ed1de58a0f99c785c777d63a9a6149.tar.gz compcert-kvx-7c6ce18466ed1de58a0f99c785c777d63a9a6149.zip | |
a bit of progress
Diffstat (limited to 'backend/CSE3analysisaux.ml')
| -rw-r--r-- | backend/CSE3analysisaux.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 3e4a6b9e..3990b765 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -67,6 +67,9 @@ let pp_option pp oc = function | None -> output_string oc "none" | Some x -> pp oc x;; +let is_trivial eq = + (eq.eq_op = SOp Op.Omove) && (eq.eq_args = [eq.eq_lhs]);; + let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let cur_eq_id = ref 0 and cur_catalog = ref PTree.empty @@ -76,6 +79,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = and cur_kill_mem = ref PSet.empty and cur_moves = ref (PMap.init PSet.empty) in let eq_find_oracle node eq = + assert (not (is_trivial eq)); let o = Hashtbl.find_opt eq_table (flatten_eq eq) in (if !Clflags.option_debug_compcert > 1 then Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node) |