From b6544eace7e8d805165537d953c3b93da8927df1 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 8 Aug 2016 09:46:27 -0700 Subject: [PATCH] Remove redundant normalization Summary: There is no need to call exp_normalize on the sub-expressions of arguments to atom_normalize, as it calls exp_normalize on its sub-expressions. Reviewed By: cristianoc Differential Revision: D3669390 fbshipit-source-id: 468b6b1 --- infer/src/backend/prop.ml | 30 ++++++++---------------------- 1 file changed, 8 insertions(+), 22 deletions(-) diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 386f942b3..b19e02040 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1464,35 +1464,21 @@ let prop_is_emp p = match p.sigma with (** {2 Functions for changing and generating propositions} *) +(** Construct an atom. *) +let mk_atom atom = + Config.run_with_abs_val_equal_zero (fun () -> atom_normalize Sil.sub_empty atom) () + (** Sil.Construct a disequality. *) -let mk_neq e1 e2 = - Config.run_with_abs_val_equal_zero - (fun () -> - let ne1 = exp_normalize Sil.sub_empty e1 in - let ne2 = exp_normalize Sil.sub_empty e2 in - atom_normalize Sil.sub_empty (Sil.Aneq (ne1, ne2))) () +let mk_neq e1 e2 = mk_atom (Aneq (e1, e2)) (** Sil.Construct an equality. *) -let mk_eq e1 e2 = - Config.run_with_abs_val_equal_zero - (fun () -> - let ne1 = exp_normalize Sil.sub_empty e1 in - let ne2 = exp_normalize Sil.sub_empty e2 in - atom_normalize Sil.sub_empty (Sil.Aeq (ne1, ne2))) () +let mk_eq e1 e2 = mk_atom (Aeq (e1, e2)) (** Construct a pred. *) -let mk_pred a e = - Config.run_with_abs_val_equal_zero - (fun () -> - let ne = exp_normalize Sil.sub_empty e in - atom_normalize Sil.sub_empty (Apred (a, ne))) () +let mk_pred a e = mk_atom (Apred (a, e)) (** Construct a negated pred. *) -let mk_npred a e = - Config.run_with_abs_val_equal_zero - (fun () -> - let ne = exp_normalize Sil.sub_empty e in - atom_normalize Sil.sub_empty (Anpred (a, ne))) () +let mk_npred a e = mk_atom (Anpred (a, e)) (** Construct a points-to predicate for a single program variable. If [expand_structs] is true, initialize the fields of structs with fresh variables. *)