From 7c6ce18466ed1de58a0f99c785c777d63a9a6149 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 14 Oct 2020 21:56:30 +0200 Subject: a bit of progress --- backend/CSE3analysisaux.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'backend/CSE3analysisaux.ml') 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) -- cgit