From 02d413061af489c237badfc7a81070f5baab9b1a Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Tue, 13 Jul 2021 22:19:09 -0700 Subject: [PATCH] [pulse] More careful simplification of instanceof. Summary: This fixes a bug that caused imprecise tracking of dynamic types. Suppose we knew term_eqs: (x instanceof T)=v1 (y instanceof T)=v2 0=v2 attrs: x has DynamicType T y has DynamicType T The simplification used to produce term_eqs: 1=v1 0=v2 That's because term_eqs is a map and 1 can appear at most once as a key. Note that the missing fact (1=v2) contradicts (0=v2). The imprecision came from not noticing such contradictions. Most of these imprecisions were observed in Erlang tests. The fix is to go from using Term.VarMap to the smarter functions in PulseFormula.Normalizer. Reviewed By: jvillard Differential Revision: D29541209 fbshipit-source-id: e4e077c87 --- infer/src/pulse/PulseFormula.ml | 82 +++++++++++-------- infer/src/pulse/unit/PulseFormulaTest.ml | 32 +++++++- .../codetoanalyze/erlang/nonmatch/issues.exp | 8 +- .../erlang/nonmatch/src/case_expression.erl | 2 +- .../erlang/nonmatch/src/function.erl | 10 +-- .../erlang/nonmatch/src/match.erl | 10 +-- 6 files changed, 88 insertions(+), 56 deletions(-) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 1ae12271f..287db2cd5 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -511,10 +511,6 @@ module Term = struct let map_subterms t ~f = fold_map_subterms t ~init:() ~f:(fun () t' -> ((), f t')) |> snd - let iter_subterms t ~f = Container.iter ~fold:fold_subterms t ~f - - let exists_subterm t ~f = Container.exists ~iter:iter_subterms t ~f - let rec fold_subst_variables t ~init ~f = match t with | Var v -> @@ -888,6 +884,14 @@ module Atom = struct let fold_terms atom ~init ~f = fold_map_terms atom ~init ~f:(fun acc t -> (f acc t, t)) |> fst + let fold_subterms atom ~init ~f = + fold_terms atom ~init ~f:(fun acc t -> Term.fold_subterms t ~init:acc ~f) + + + let iter_subterms atom ~f = Container.iter ~fold:fold_subterms atom ~f + + let exists_subterm atom ~f = Container.exists ~iter:iter_subterms atom ~f + let equal t1 t2 = Equal (t1, t2) let less_equal t1 t2 = LessEqual (t1, t2) @@ -907,6 +911,7 @@ module Atom = struct let map_terms atom ~f = fold_map_terms atom ~init:() ~f:(fun () t -> ((), f t)) |> snd + (* Preseves physical equality if [f] does. *) let map_subterms atom ~f = map_terms atom ~f:(fun t -> Term.map_subterms t ~f) let to_term : t -> Term.t = function @@ -1185,7 +1190,7 @@ module Formula = struct val normalize_atom : t -> Atom.t -> Atom.t option SatUnsat.t - val normalize : t -> (t * new_eqs) SatUnsat.t + val normalize : t * new_eqs -> (t * new_eqs) SatUnsat.t val implies_atom : t -> Atom.t -> bool @@ -1530,7 +1535,7 @@ module Formula = struct (* interface *) - let normalize phi = normalize_with_fuel ~fuel:base_fuel (phi, []) + let normalize phi_new_eqs = normalize_with_fuel ~fuel:base_fuel phi_new_eqs let and_atom atom phi_new_eqs = and_atom atom phi_new_eqs >>| snd @@ -1632,47 +1637,54 @@ module DynamicTypes = struct Term.of_bool is_instanceof ) - let simplify tenv ~get_dynamic_type phi = - let simplify_is_instance_of (t : Term.t) = + let really_simplify tenv ~get_dynamic_type phi = + let simplify_term (t : Term.t) = match t with | IsInstanceOf (v, typ) -> ( match evaluate_instanceof tenv ~get_dynamic_type v typ with None -> t | Some t' -> t' ) | t -> t in - let changed = ref false in - let term_eqs = - if - Term.VarMap.exists - (fun t _ -> Term.exists_subterm t ~f:(function IsInstanceOf _ -> true | _ -> false)) - phi.both.term_eqs - then - (* slow path: reconstruct everything *) - Term.VarMap.fold - (fun t v term_eqs' -> - let t' = Term.map_subterms t ~f:simplify_is_instance_of in - changed := !changed || not (phys_equal t t') ; - Term.VarMap.add t' v term_eqs' ) - phi.both.term_eqs Term.VarMap.empty - else (* fast path: nothing to do *) phi.both.term_eqs + let simplify_atom atom = Atom.map_subterms ~f:simplify_term atom in + let open SatUnsat.Import in + let old_term_eqs = phi.both.term_eqs in + let old_atoms = phi.both.atoms in + let both = {phi.both with term_eqs= Term.VarMap.empty; atoms= Atom.Set.empty} in + let* both, new_eqs = + let f t v acc_both = + let* acc_both = acc_both in + let t = simplify_term t in + Formula.Normalizer.and_var_term v t acc_both + in + Term.VarMap.fold f old_term_eqs (Sat (both, [])) in - let atoms = - Atom.Set.map - (fun atom -> - Atom.map_subterms atom ~f:(fun t -> - let t' = simplify_is_instance_of t in - changed := !changed || not (phys_equal t t') ; - t' ) ) - phi.both.atoms + let+ both, new_eqs = + let f atom acc_both = + let* acc_both = acc_both in + let atom = simplify_atom atom in + Formula.Normalizer.and_atom atom acc_both + in + Atom.Set.fold f old_atoms (Sat (both, new_eqs)) in - if !changed then {phi with both= {phi.both with atoms; term_eqs}} else phi + ({phi with both}, new_eqs) + + + let has_instanceof phi = + let in_term (t : Term.t) = match t with IsInstanceOf _ -> true | _ -> false in + let in_atom atom = Atom.exists_subterm atom ~f:in_term in + Term.VarMap.exists (fun t _v -> in_term t) phi.both.term_eqs + || Atom.Set.exists in_atom phi.both.atoms + + + let simplify tenv ~get_dynamic_type phi = + if has_instanceof phi then really_simplify tenv ~get_dynamic_type phi else Sat (phi, []) end let normalize tenv ~get_dynamic_type phi = let open SatUnsat.Import in - let phi = DynamicTypes.simplify tenv ~get_dynamic_type phi in - let* both, new_eqs = Formula.Normalizer.normalize phi.both in - let* known, _ = Formula.Normalizer.normalize phi.known in + let* phi, new_eqs = DynamicTypes.simplify tenv ~get_dynamic_type phi in + let* both, new_eqs = Formula.Normalizer.normalize (phi.both, new_eqs) in + let* known, _ = Formula.Normalizer.normalize (phi.known, new_eqs) in let+ pruned = Atom.Set.fold (fun atom pruned_sat -> diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml index 060b6af87..40846288d 100644 --- a/infer/src/pulse/unit/PulseFormulaTest.ml +++ b/infer/src/pulse/unit/PulseFormulaTest.ml @@ -44,6 +44,11 @@ let of_binop bop f1 f2 phi = (phi, AbstractValueOperand v) +let instanceof typ x_var y_var phi = + let+ phi, _new_eqs = and_equal_instanceof y_var x_var typ phi in + phi + + let ( + ) f1 f2 phi = of_binop (PlusA None) f1 f2 phi let ( - ) f1 f2 phi = of_binop (MinusA None) f1 f2 phi @@ -126,10 +131,18 @@ let dummy_tenv = Tenv.create () let dummy_get_dynamic_type _ = None -let normalize phi = - test ~f:(fun phi -> normalize dummy_tenv ~get_dynamic_type:dummy_get_dynamic_type phi >>| fst) phi +let nil_typ = Typ.mk (Tstruct (ErlangType Nil)) + +let cons_typ = Typ.mk (Tstruct (ErlangType Cons)) + +let normalize_with ~get_dynamic_type phi = + test ~f:(fun phi -> normalize dummy_tenv ~get_dynamic_type phi >>| fst) phi +let normalize phi = normalize_with ~get_dynamic_type:dummy_get_dynamic_type phi + +let normalize_with_all_types_Nil phi = normalize_with ~get_dynamic_type:(fun _ -> Some nil_typ) phi + let simplify ~keep phi = let keep = AbstractValue.Set.of_list keep in test phi ~f:(fun phi -> @@ -141,6 +154,21 @@ let simplify ~keep phi = let%test_module "normalization" = ( module struct + let%expect_test _ = + normalize_with_all_types_Nil + (instanceof nil_typ x_var z_var && instanceof nil_typ y_var w_var && z = i 0) ; + [%expect {|unsat|}] + + let%expect_test _ = + normalize_with_all_types_Nil + (instanceof nil_typ x_var z_var && instanceof nil_typ y_var w_var && w = i 0) ; + [%expect {|unsat|}] + + let%expect_test _ = + normalize_with_all_types_Nil + (instanceof cons_typ x_var y_var && instanceof nil_typ x_var y_var) ; + [%expect {|unsat|}] + let%expect_test _ = normalize (x < y) ; [%expect diff --git a/infer/tests/codetoanalyze/erlang/nonmatch/issues.exp b/infer/tests/codetoanalyze/erlang/nonmatch/issues.exp index d9fe5e3c9..260371b9e 100644 --- a/infer/tests/codetoanalyze/erlang/nonmatch/issues.exp +++ b/infer/tests/codetoanalyze/erlang/nonmatch/issues.exp @@ -8,11 +8,9 @@ codetoanalyze/erlang/nonmatch/src/case_guards.erl, test_accepts_positive2_Bad/0, codetoanalyze/erlang/nonmatch/src/case_guards.erl, test_accepts_positive_Bad/0, -15, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `accepts_positive/1`,no pattern match here] codetoanalyze/erlang/nonmatch/src/function.erl, assert_empty/1, 0, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [*** LATENT ***,no pattern match here] codetoanalyze/erlang/nonmatch/src/function.erl, assert_second_is_nil/1, 0, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [*** LATENT ***,no pattern match here] -codetoanalyze/erlang/nonmatch/src/function.erl, fp_list_match_test_secondnil1_Ok/0, -17, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `assert_second_is_nil/1`,no pattern match here] -codetoanalyze/erlang/nonmatch/src/function.erl, fp_list_match_test_secondnil2_Ok/0, -20, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `assert_second_is_nil/1`,no pattern match here] codetoanalyze/erlang/nonmatch/src/function.erl, list_match_test_empty2_Bad/0, -12, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `assert_empty/1`,no pattern match here] codetoanalyze/erlang/nonmatch/src/function.erl, list_match_test_empty3_Bad/0, -14, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `assert_empty/1`,no pattern match here] -codetoanalyze/erlang/nonmatch/src/function.erl, list_match_test_secondnil3_Bad/0, -22, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `assert_second_is_nil/1`,no pattern match here] +codetoanalyze/erlang/nonmatch/src/function.erl, list_match_test_secondnil3_Bad/0, -20, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `assert_second_is_nil/1`,no pattern match here] codetoanalyze/erlang/nonmatch/src/function.erl, list_match_test_tail3_Bad/0, -8, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `tail/1`,no pattern match here] codetoanalyze/erlang/nonmatch/src/function.erl, tail/1, 0, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [*** LATENT ***,no pattern match here] codetoanalyze/erlang/nonmatch/src/function_guards.erl, accepts_positive/1, 0, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [*** LATENT ***,no pattern match here] @@ -24,11 +22,9 @@ codetoanalyze/erlang/nonmatch/src/function_guards.erl, test_accepts_positive_Bad codetoanalyze/erlang/nonmatch/src/function_guards.erl, test_possible_exception_Bad/0, -37, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `possible_exception/1`,no pattern match here] codetoanalyze/erlang/nonmatch/src/if_expression.erl, accepts_positive/1, 1, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [*** LATENT ***,no pattern match here] codetoanalyze/erlang/nonmatch/src/if_expression.erl, test_accepts_positive_Bad/0, -13, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `accepts_positive/1`,no pattern match here] -codetoanalyze/erlang/nonmatch/src/match.erl, fp_match_test_c_Ok/0, 1, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [no pattern match here] -codetoanalyze/erlang/nonmatch/src/match.erl, fp_match_test_d_Ok/0, -13, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `tail/1`,no pattern match here] codetoanalyze/erlang/nonmatch/src/match.erl, match_test_b_Bad/0, 1, CONSTANT_ADDRESS_DEREFERENCE, no_bucket, WARNING, [in call to `two/0`,is the constant 2,assigned,returned,return from call to `two/0`,invalid access occurs here] codetoanalyze/erlang/nonmatch/src/match.erl, match_test_b_Bad/0, 1, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [no pattern match here] -codetoanalyze/erlang/nonmatch/src/match.erl, match_test_e_Bad/0, -17, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `tail/1`,no pattern match here] +codetoanalyze/erlang/nonmatch/src/match.erl, match_test_e_Bad/0, -15, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `tail/1`,no pattern match here] codetoanalyze/erlang/nonmatch/src/match.erl, match_test_g_Bad/0, 7, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `only_accepts_one/1`,no pattern match here] codetoanalyze/erlang/nonmatch/src/match.erl, only_accepts_one/1, 0, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [*** LATENT ***,no pattern match here] codetoanalyze/erlang/nonmatch/src/match.erl, tail/1, 0, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [*** LATENT ***,no pattern match here] diff --git a/infer/tests/codetoanalyze/erlang/nonmatch/src/case_expression.erl b/infer/tests/codetoanalyze/erlang/nonmatch/src/case_expression.erl index 7dd54d782..7af4c0192 100644 --- a/infer/tests/codetoanalyze/erlang/nonmatch/src/case_expression.erl +++ b/infer/tests/codetoanalyze/erlang/nonmatch/src/case_expression.erl @@ -22,7 +22,7 @@ case_simple(X) -> tail_with_case(X) -> case X of - [_|T] -> T + [_ | T] -> T end. case_test_simple1_Ok() -> diff --git a/infer/tests/codetoanalyze/erlang/nonmatch/src/function.erl b/infer/tests/codetoanalyze/erlang/nonmatch/src/function.erl index 515367cd0..852cce157 100644 --- a/infer/tests/codetoanalyze/erlang/nonmatch/src/function.erl +++ b/infer/tests/codetoanalyze/erlang/nonmatch/src/function.erl @@ -12,8 +12,8 @@ list_match_test_empty1_Ok/0, list_match_test_empty2_Bad/0, list_match_test_empty3_Bad/0, - fp_list_match_test_secondnil1_Ok/0, - fp_list_match_test_secondnil2_Ok/0, + list_match_test_secondnil1_Ok/0, + list_match_test_secondnil2_Ok/0, list_match_test_secondnil3_Bad/0 ]). @@ -35,11 +35,9 @@ list_match_test_empty2_Bad() -> list_match_test_empty3_Bad() -> assert_empty([1, 2]). -% FP (T94492137) -fp_list_match_test_secondnil1_Ok() -> +list_match_test_secondnil1_Ok() -> assert_second_is_nil([1, [], 2]). -% FP (T94492137) -fp_list_match_test_secondnil2_Ok() -> +list_match_test_secondnil2_Ok() -> assert_second_is_nil([1, []]). list_match_test_secondnil3_Bad() -> assert_second_is_nil([1, [2], 3]). diff --git a/infer/tests/codetoanalyze/erlang/nonmatch/src/match.erl b/infer/tests/codetoanalyze/erlang/nonmatch/src/match.erl index 05d6c40f2..cf1f2a029 100644 --- a/infer/tests/codetoanalyze/erlang/nonmatch/src/match.erl +++ b/infer/tests/codetoanalyze/erlang/nonmatch/src/match.erl @@ -8,8 +8,8 @@ -export([ match_test_a_Ok/0, match_test_b_Bad/0, - fp_match_test_c_Ok/0, - fp_match_test_d_Ok/0, + match_test_c_Ok/0, + match_test_d_Ok/0, match_test_e_Bad/0, match_test_f_Ok/0, match_test_g_Bad/0 @@ -23,12 +23,10 @@ match_test_a_Ok() -> match_test_b_Bad() -> [_ | _] = two(). -% FP (T94492137) -fp_match_test_c_Ok() -> +match_test_c_Ok() -> [_X, _Y] = [1, 2]. -% FP (T94492137) -fp_match_test_d_Ok() -> +match_test_d_Ok() -> [_ | Xs] = [1, 2], tail(Xs).