From b95aaefb371020cc6dce2a346fefc99ad7c92747 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 7 Jul 2016 08:47:58 -0700 Subject: [PATCH] make --abs-val great again Summary: `Config.abs_val` was always set to 2 instead of taking its value from the option. Reviewed By: jberdine Differential Revision: D3515024 fbshipit-source-id: fa27396 --- infer/src/backend/config.ml | 83 ++++++++++++++++++------------------- infer/src/backend/prop.ml | 36 +++++----------- 2 files changed, 52 insertions(+), 67 deletions(-) diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 0f5d3e6c6..4197f24d0 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -1071,48 +1071,6 @@ and ( ("Matcher or list of matchers for methods that should be considered expensive " ^ "by the performance critical checker.")) -(** Global variables *) - -let set_reference_and_call_function reference value f x = - let saved = !reference in - let restore () = - reference := saved in - try - reference := value; - let res = f x in - restore (); - res - with - | exn -> - restore (); - raise exn - -(** Flag for footprint discovery mode *) -let footprint = ref true - -let run_in_footprint_mode f x = - set_reference_and_call_function footprint true f x - -let run_in_re_execution_mode f x = - set_reference_and_call_function footprint false f x - -(** Set in the middle of forcing delayed prints *) -let forcing_delayed_prints = ref false - -(** Number of lines of code in original file *) -let nLOC = ref 0 - -(** if true, user simple pretty printing *) -let pp_simple = ref true - -let reset_abs_val = - let abs_val_default = !abs_val in - fun () -> - abs_val := abs_val_default - -let run_with_abs_val_equal_zero f x = - set_reference_and_call_function abs_val 0 f x - (** Configuration values specified by environment variables *) @@ -1276,6 +1234,7 @@ let print_usage_exit () = let anon_args = IList.rev !anon_args and rest = !rest and abs_struct = !abs_struct +and abs_val_orig = !abs_val and absolute_paths = !absolute_paths and allow_specs_cleanup = !allow_specs_cleanup and analysis_path_regex_whitelist_options = @@ -1425,3 +1384,43 @@ let patterns_suppress_warnings = | None -> if CLOpt.(current_exe <> Java) then [] else error ("Error: The option " ^ suppress_warnings_annotations_long ^ " was not provided") + +(** Global variables *) + +let set_reference_and_call_function reference value f x = + let saved = !reference in + let restore () = + reference := saved in + try + reference := value; + let res = f x in + restore (); + res + with + | exn -> + restore (); + raise exn + +(** Flag for footprint discovery mode *) +let footprint = ref true + +let run_in_footprint_mode f x = + set_reference_and_call_function footprint true f x + +let run_in_re_execution_mode f x = + set_reference_and_call_function footprint false f x + +(** Set in the middle of forcing delayed prints *) +let forcing_delayed_prints = ref false + +(** Number of lines of code in original file *) +let nLOC = ref 0 + +(** if true, user simple pretty printing *) +let pp_simple = ref true + +let reset_abs_val () = + abs_val := abs_val_orig + +let run_with_abs_val_equal_zero f x = + set_reference_and_call_function abs_val 0 f x diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 422221a40..5e001523a 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -839,16 +839,8 @@ let texp_normalize sub exp = match exp with | Sil.Sizeof (typ, len, st) -> Sil.Sizeof (typ, Option.map (exp_normalize sub) len, st) | _ -> exp_normalize sub exp -let run_with_abs_val_eq_zero f = - let abs_val_old = !Config.abs_val in - Config.abs_val := 0; - let res = f () in - Config.abs_val := abs_val_old; - res - let exp_normalize_noabs sub exp = - run_with_abs_val_eq_zero - (fun () -> exp_normalize sub exp) + Config.run_with_abs_val_equal_zero (exp_normalize sub) exp (** Return [true] if the atom is an inequality *) let atom_is_inequality = function @@ -1372,8 +1364,7 @@ let footprint_normalize prop = { prop with foot_pi = npi'; foot_sigma = nsigma' } let exp_normalize_prop prop exp = - run_with_abs_val_eq_zero - (fun () -> exp_normalize prop.sub exp) + Config.run_with_abs_val_equal_zero (exp_normalize prop.sub) exp let lexp_normalize_prop p lexp = let root = Sil.root_of_lexp lexp in @@ -1408,24 +1399,19 @@ let exp_collapse_consecutive_indices_prop typ exp = end let atom_normalize_prop prop atom = - run_with_abs_val_eq_zero - (fun () -> atom_normalize prop.sub atom) + Config.run_with_abs_val_equal_zero (atom_normalize prop.sub) atom let strexp_normalize_prop prop strexp = - run_with_abs_val_eq_zero - (fun () -> strexp_normalize prop.sub strexp) + Config.run_with_abs_val_equal_zero (strexp_normalize prop.sub) strexp let hpred_normalize_prop prop hpred = - run_with_abs_val_eq_zero - (fun () -> hpred_normalize prop.sub hpred) + Config.run_with_abs_val_equal_zero (hpred_normalize prop.sub) hpred let sigma_normalize_prop prop sigma = - run_with_abs_val_eq_zero - (fun () -> sigma_normalize prop.sub sigma) + Config.run_with_abs_val_equal_zero (sigma_normalize prop.sub) sigma let pi_normalize_prop prop pi = - run_with_abs_val_eq_zero - (fun () -> pi_normalize prop.sub prop.sigma pi) + Config.run_with_abs_val_equal_zero (pi_normalize prop.sub prop.sigma) pi (** {2 Compaction} *) (** Return a compact representation of the prop *) @@ -1466,19 +1452,19 @@ let prop_is_emp p = match p.sigma with (** Sil.Construct a disequality. *) let mk_neq e1 e2 = - run_with_abs_val_eq_zero + 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))) + atom_normalize Sil.sub_empty (Sil.Aneq (ne1, ne2))) () (** Sil.Construct an equality. *) let mk_eq e1 e2 = - run_with_abs_val_eq_zero + 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))) + atom_normalize Sil.sub_empty (Sil.Aeq (ne1, ne2))) () (** Construct a points-to predicate for a single program variable. If [expand_structs] is true, initialize the fields of structs with fresh variables. *)