[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

@@ -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 really_simplify tenv ~get_dynamic_type phi =
-    let simplify_is_instance_of (t : Term.t) =
+    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 simplify_atom atom = Atom.map_subterms ~f:simplify_term atom in
-    let term_eqs =
+    let open SatUnsat.Import in
-      if
+    let old_term_eqs = phi.both.term_eqs in
-        Term.VarMap.exists
+    let old_atoms = phi.both.atoms in
-          (fun t _ -> Term.exists_subterm t ~f:(function IsInstanceOf _ -> true | _ -> false))
+    let both = {phi.both with term_eqs= Term.VarMap.empty; atoms= Atom.Set.empty} in
-          phi.both.term_eqs
+    let* both, new_eqs =
-      then
+      let f t v acc_both =
-        (* slow path: reconstruct everything *)
+        let* acc_both = acc_both in
-        Term.VarMap.fold
+        let t = simplify_term t in
-          (fun t v term_eqs' ->
+        Formula.Normalizer.and_var_term v t acc_both
-            let t' = Term.map_subterms t ~f:simplify_is_instance_of in
+      in
-            changed := !changed || not (phys_equal t t') ;
+      Term.VarMap.fold f old_term_eqs (Sat (both, []))
-            Term.VarMap.add t' v term_eqs' )
-          phi.both.term_eqs Term.VarMap.empty
-      else (* fast path: nothing to do *) phi.both.term_eqs
     in
-    let atoms =
+    let+ both, new_eqs =
-      Atom.Set.map
+      let f atom acc_both =
-        (fun atom ->
+        let* acc_both = acc_both in
-          Atom.map_subterms atom ~f:(fun t ->
+        let atom = simplify_atom atom in
-              let t' = simplify_is_instance_of t in
+        Formula.Normalizer.and_atom atom acc_both
-              changed := !changed || not (phys_equal t t') ;
+      in
-              t' ) )
+      Atom.Set.fold f old_atoms (Sat (both, new_eqs))
-        phi.both.atoms
     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* phi, new_eqs = DynamicTypes.simplify tenv ~get_dynamic_type phi in
-  let* both, new_eqs = Formula.Normalizer.normalize phi.both in
+  let* both, new_eqs = Formula.Normalizer.normalize (phi.both, new_eqs) in
-  let* known, _ = Formula.Normalizer.normalize phi.known in
+  let* known, _ = Formula.Normalizer.normalize (phi.known, new_eqs) in
   let+ pruned =
     Atom.Set.fold
       (fun atom pruned_sat ->

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 =
+let nil_typ = Typ.mk (Tstruct (ErlangType Nil))
-  test ~f:(fun phi -> normalize dummy_tenv ~get_dynamic_type:dummy_get_dynamic_type phi >>| fst) phi
+
+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

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]

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

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,
+    list_match_test_secondnil1_Ok/0,
-    fp_list_match_test_secondnil2_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)
+list_match_test_secondnil1_Ok() ->
-fp_list_match_test_secondnil1_Ok() ->
     assert_second_is_nil([1, [], 2]).
-% FP (T94492137)
+list_match_test_secondnil2_Ok() ->
-fp_list_match_test_secondnil2_Ok() ->
     assert_second_is_nil([1, []]).
 list_match_test_secondnil3_Bad() ->
     assert_second_is_nil([1, [2], 3]).

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,
+    match_test_c_Ok/0,
-    fp_match_test_d_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)
+match_test_c_Ok() ->
-fp_match_test_c_Ok() ->
     [_X, _Y] = [1, 2].
 
-% FP (T94492137)
+match_test_d_Ok() ->
-fp_match_test_d_Ok() ->
     [_ | Xs] = [1, 2],
     tail(Xs).