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).