[infer] Delete Formula.normalize

Reviewed By: skcho

Differential Revision: D58814273

fbshipit-source-id: db00efb17ed7b24228c4c526fc9e98eef0101052

infer/src/pulse/PulseAbductiveDomain.ml

@@ -1895,20 +1895,12 @@ module Summary = struct
   let of_post_ proc_name (proc_attrs : ProcAttributes.t) location astate0 =
     let open SatUnsat.Import in
     let astate = astate0 in
-    (* NOTE: we normalize (to strengthen the equality relation used by canonicalization) then
-       canonicalize *before* garbage collecting unused addresses in case we detect any last-minute
-       contradictions about addresses we are about to garbage collect *)
-    let* path_condition, new_eqs = Formula.normalize ~location astate.path_condition in
-    let astate = {astate with path_condition} in
-    let* astate, error = incorporate_new_eqs astate new_eqs in
     let astate_before_filter = astate in
     (* do not store the decompiler in the summary and make sure we only use the original one by
        marking it invalid *)
     let astate = {astate with decompiler= Decompiler.invalid} in
     let* astate, live_addresses, dead_addresses, new_eqs = filter_for_summary proc_name astate in
-    let+ astate, error =
-      match error with None -> incorporate_new_eqs astate new_eqs | Some _ -> Sat (astate, error)
-    in
+    let+ astate, error = incorporate_new_eqs astate new_eqs in
     match error with
     | None -> (
       (* NOTE: it's important for correctness that we check leaks last because we are going to carry

infer/src/pulse/PulseFormula.ml

@@ -889,13 +889,6 @@ module Term = struct
     fold_map_direct_subterms t ~init:() ~f:(fun () t' -> ((), f t')) |> snd
 
 
-  let rec fold_map_subterms t ~init ~f =
-    let acc, t' =
-      fold_map_direct_subterms t ~init ~f:(fun acc t' -> fold_map_subterms t' ~init:acc ~f)
-    in
-    f acc t'
-
-
   let satunsat_map_direct_subterms t ~f =
     let exception FoundUnsat in
     try
@@ -905,10 +898,6 @@ module Term = struct
     with FoundUnsat -> Unsat
 
 
-  let fold_subterms t ~init ~f = fold_map_subterms t ~init ~f:(fun acc t' -> (f acc t', t')) |> fst
-
-  let map_subterms t ~f = fold_map_subterms t ~init:() ~f:(fun () t' -> ((), f t')) |> snd
-
   let rec fold_subst_variables ~init ~f_subst ?(f_post = fun ~prev:_ acc t -> (acc, t)) t =
     match t with
     | Var v ->
@@ -1516,14 +1505,6 @@ 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 fold_variables atom ~init ~f =
     fold_terms atom ~init ~f:(fun acc t -> Term.fold_variables t ~init:acc ~f)
 
@@ -1549,9 +1530,6 @@ 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
     | LessEqual (t1, t2) ->
         LessEqual (t1, t2)
@@ -2262,10 +2240,6 @@ module Formula = struct
 
     val set_intervals : intervals -> t -> t
 
-    val reset_atoms : t -> t
-
-    val reset_term_eqs : t -> t
-
     val unsafe_mk :
          var_eqs:var_eqs
       -> const_eqs:Term.t Var.Map.t
@@ -2759,12 +2733,6 @@ module Formula = struct
 
     let set_intervals intervals phi = {phi with intervals}
 
-    let reset_atoms phi = {phi with atoms= Atom.Set.empty; atoms_occurrences= Var.Map.empty}
-
-    let reset_term_eqs phi =
-      {phi with term_eqs= Term.VarMap.empty; term_eqs_occurrences= Var.Map.empty}
-
-
     let unsafe_mk ~var_eqs ~const_eqs ~type_constraints ~linear_eqs ~term_eqs ~tableau ~intervals
         ~atoms ~linear_eqs_occurrences ~tableau_occurrences ~term_eqs_occurrences ~atoms_occurrences
         =
@@ -4062,65 +4030,6 @@ module DynamicTypes = struct
           else None
 
 
-  let really_simplify formula =
-    let simplify_term (t : Term.t) =
-      match t with
-      | IsInstanceOf {var= v; typ; nullable} -> (
-        match evaluate_instanceof formula v typ nullable with None -> t | Some t' -> t' )
-      | t ->
-          t
-    in
-    let simplify_atom atom = Atom.map_subterms ~f:simplify_term atom in
-    let open SatUnsat.Import in
-    let old_atoms = formula.phi.atoms in
-    let* phi, new_eqs =
-      let f t v acc_phi =
-        let* acc_phi in
-        let t = simplify_term t in
-        Formula.Normalizer.and_var_term v t acc_phi
-      in
-      Formula.term_eqs_fold f formula.phi
-        (Sat (formula.phi |> Formula.reset_term_eqs |> Formula.reset_atoms, RevList.empty))
-    in
-    let+ phi, new_eqs =
-      let f atom acc_phi =
-        let* acc_phi in
-        let atom = simplify_atom atom in
-        Formula.Normalizer.and_atom atom acc_phi
-      in
-      Atom.Set.fold f old_atoms (Sat (phi, new_eqs))
-    in
-    ({formula with phi}, new_eqs)
-
-
-  let has_instanceof formula =
-    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
-    Formula.term_eqs_exists (fun t _v -> in_term t) formula.phi
-    || Atom.Set.exists in_atom formula.phi.atoms
-
-
-  (* The previous summary-time simplification wipes out v1 = InstanceOf(v2,t) when we can evaluate the term, which messes with
-     the distinction between latent and manifest errors (if v2 is an argument). I tried hacks to keep the
-     intensional information, but they're unconvincing and a waste of effort, since we ultimately aim to remove the simplification
-     phase anyway. Instead, we just log situations in which the simplification would lead to Unsat, as those are ones in which the
-     new on-the-fly propagation is deficient. If none show up, we can safely remove simplification.
-  *)
-  let simplify ?location formula =
-    if has_instanceof formula then
-      match really_simplify formula with
-      | Unsat ->
-          L.d_printfln ~color:Pp.Orange "WARNING: Summary-time simplify returned Unsat on %a" pp
-            formula ;
-          ScubaLogging.log_message_with_location ~label:"summary_unsat"
-            ~loc:(Option.value_map location ~default:"missing" ~f:Location.to_string)
-            ~message:"summary-time normalization returned Unsat"
-      | Sat _ ->
-          ()
-    else () ;
-    Sat (formula, RevList.empty)
-
-
   (* TODO: fix messy separation between (new) InstanceOf and (old) DynamicTypes - not sure where to put the next definition *)
   let and_callee_type_constraints v type_constraints_foreign (phi, new_eqs) =
     match type_constraints_foreign with
@@ -4185,13 +4094,6 @@ let and_equal_instanceof v1 v2 t ~nullable formula =
   Sat (formula, new_eqs')
 
 
-let normalize ?location formula =
-  (* Sat (formula, RevList.empty) *)
-  Debug.p "@\n@\n***NORMALIZING NOW***@\n@\n" ;
-  (* normalization happens incrementally except for dynamic types (TODO) *)
-  DynamicTypes.simplify ?location formula
-
-
 let and_dynamic_type v t ?source_file formula =
   let v = (Formula.get_repr formula.phi v :> Var.t) in
   let tenv = PulseContext.tenv_exn () in
@@ -4593,15 +4495,14 @@ end
 
 let simplify ~precondition_vocabulary ~keep formula =
   let open SatUnsat.Import in
-  let* formula, new_eqs = normalize formula in
   L.d_printfln_escaped "@[Simplifying %a@ wrt %a (keep),@ with prunables=%a@]" pp formula Var.Set.pp
     keep Var.Set.pp precondition_vocabulary ;
   (* get rid of as many variables as possible *)
   let* formula = QuantifierElimination.eliminate_vars ~precondition_vocabulary ~keep formula in
   (* TODO: doing [QuantifierElimination.eliminate_vars; DeadVariables.eliminate] a few times may
      eliminate even more variables *)
   let+ formula, live_vars = DeadVariables.eliminate ~precondition_vocabulary ~keep formula in
-  (formula, live_vars, new_eqs)
+  (formula, live_vars, RevList.empty)
 
 
 let is_known_non_pointer formula v = Formula.is_non_pointer formula.phi v

infer/src/pulse/PulseFormula.mli

@@ -90,9 +90,6 @@ val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> (t * new
 
 (** {3 Operations} *)
 
-val normalize : ?location:Location.t -> t -> (t * new_eqs) SatUnsat.t
-(** think a bit harder about the formula *)
-
 val simplify :
   precondition_vocabulary:Var.Set.t -> keep:Var.Set.t -> t -> (t * Var.Set.t * new_eqs) SatUnsat.t
 

infer/src/pulse/PulseTopl.ml

@@ -343,7 +343,6 @@ end = struct
             let* path_condition, new_eqs_a =
               Formula.prune_binop ~negated:false op l r path_condition
             in
-            let* path_condition, new_eqs_b = Formula.normalize path_condition in
             let new_eqs =
               let new_eqs = RevList.empty in
               let new_eqs =
@@ -358,7 +357,7 @@ end = struct
                     new_eqs
               in
               let ( ++ ) = RevList.append in
-              new_eqs ++ new_eqs_a ++ new_eqs_b
+              new_eqs ++ new_eqs_a
             in
             let* heap =
               let incorporate_eq heap (eq : Formula.new_eq) =

infer/src/pulse/unit/PulseFormulaTest.ml

@@ -192,7 +192,7 @@ let nil_typ = Typ.mk (Tstruct (ErlangType Nil))
 
 let cons_typ = Typ.mk (Tstruct (ErlangType Cons))
 
-let normalize_with phi init_phi = test ~f:(fun phi -> normalize phi >>| fst) phi init_phi
+let normalize_with phi init_phi = test ~f:(fun phi -> Sat phi) phi init_phi
 
 let normalize phi = normalize_with phi ttrue