Refactor module Prop by moving normalization functions into module Normalize.

Summary:
Refactor module Prop disentangling the various normalization functions, and moving them inside a new module Normalize.
There is quite a reshuffling of functions, including some dead code removal, but there should be no computational difference.

Reviewed By: jvillard

Differential Revision: D3696491

fbshipit-source-id: 68dd719

infer/src/backend/dom.ml

@@ -1629,7 +1629,7 @@ let pi_partial_join mode
     | Some (n', e') -> Exp.equal e e' && IntLit.lt n n' in
   let join_atom_check_pre p a =
     (* check for atoms in pre mode: fail if the negation is implied by the other side *)
-    let not_a = Prop.atom_negate a in
+    let not_a = Prover.atom_negate a in
     if (Prover.check_atom p not_a) then
       (L.d_str "join_atom_check failed on "; Sil.d_atom a; L.d_ln (); raise IList.Fail) in
   let join_atom_check_attribute p a =

infer/src/backend/interproc.ml

@@ -616,6 +616,40 @@ let forward_tabulate tenv wl =
   L.d_strln ".... Work list empty. Stop ...."; L.d_ln ()
 
 
+(** if possible, produce a (fieldname, typ) path from one of the [src_exps] to [sink_exp] using
+    [reachable_hpreds]. *)
+let get_fld_typ_path_opt src_exps sink_exp_ reachable_hpreds_ =
+  let strexp_matches target_exp = function
+    | (_, Sil.Eexp (e, _)) -> Exp.equal target_exp e
+    | _ -> false in
+  let extend_path hpred (sink_exp, path, reachable_hpreds) = match hpred with
+    | Sil.Hpointsto (lhs, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) ->
+        (try
+           let fld, _ = IList.find (fun fld -> strexp_matches sink_exp fld) flds in
+           let reachable_hpreds' = Sil.HpredSet.remove hpred reachable_hpreds in
+           (lhs, (Some fld, typ) :: path, reachable_hpreds')
+         with Not_found -> (sink_exp, path, reachable_hpreds))
+    | Sil.Hpointsto (lhs, Sil.Earray (_, elems, _), Exp.Sizeof (typ, _, _)) ->
+        if IList.exists (fun pair -> strexp_matches sink_exp pair) elems
+        then
+          let reachable_hpreds' = Sil.HpredSet.remove hpred reachable_hpreds in
+          (* None means "no field name" ~=~ nameless array index *)
+          (lhs, (None, typ) :: path, reachable_hpreds')
+        else (sink_exp, path, reachable_hpreds)
+    | _ -> (sink_exp, path, reachable_hpreds) in
+  (* terminates because [reachable_hpreds] is shrinking on each recursive call *)
+  let rec get_fld_typ_path sink_exp path reachable_hpreds =
+    let (sink_exp', path', reachable_hpreds') =
+      Sil.HpredSet.fold extend_path reachable_hpreds (sink_exp, path, reachable_hpreds) in
+    if Exp.Set.mem sink_exp' src_exps
+    then Some path'
+    else
+    if Sil.HpredSet.cardinal reachable_hpreds' >= Sil.HpredSet.cardinal reachable_hpreds
+    then None (* can't find a path from [src_exps] to [sink_exp] *)
+    else get_fld_typ_path sink_exp' path' reachable_hpreds' in
+  get_fld_typ_path sink_exp_ [] reachable_hpreds_
+
+
 (** report an error if any Context is reachable from a static field *)
 let report_context_leaks pname sigma tenv =
   (* report an error if an expression in [context_exps] is reachable from [field_strexp] *)
@@ -628,7 +662,7 @@ let report_context_leaks pname sigma tenv =
       (fun (context_exp, struct_typ) ->
          if Exp.Set.mem context_exp reachable_exps then
            let leak_path =
-             match Prop.get_fld_typ_path_opt fld_exps context_exp reachable_hpreds with
+             match get_fld_typ_path_opt fld_exps context_exp reachable_hpreds with
              | Some path -> path
              | None -> assert false (* a path must exist in order for a leak to be reported *) in
            let err_desc =

infer/src/backend/prop.mli

@@ -163,9 +163,6 @@ val atom_exp_le_const : Sil.atom -> (Exp.t * IntLit.t) option
 (** If the atom is [n<e] return [n,e] *)
 val atom_const_lt_exp : Sil.atom -> (IntLit.t * Exp.t) option
 
-(** Negate an atom *)
-val atom_negate : Sil.atom -> Sil.atom
-
 (** Normalize [exp] using the pure part of [prop].  Later, we should
     change this such that the normalization exposes offsets of [exp]
     as much as possible. *)
@@ -292,19 +289,6 @@ val prop_set_footprint : 'a t -> 'b t -> exposed t
 (** Expand PE listsegs if the flag is on. *)
 val prop_expand : normal t -> normal t list
 
-(** translate a logical and/or operation
-    taking care of the non-strict semantics for side effects *)
-val trans_land_lor :
-  Binop.t -> (Ident.t list * Sil.instr list) * Exp.t ->
-  (Ident.t list * Sil.instr list) * Exp.t -> Location.t ->
-  (Ident.t list * Sil.instr list) * Exp.t
-
-(** translate an if-then-else expression *)
-val trans_if_then_else :
-  (Ident.t list * Sil.instr list) * Exp.t -> (Ident.t list * Sil.instr list) * Exp.t ->
-  (Ident.t list * Sil.instr list) * Exp.t -> Location.t ->
-  (Ident.t list * Sil.instr list) * Exp.t
-
 (** {2 Functions for existentially quantifying and unquantifying variables} *)
 
 (** Existentially quantify the [ids] in [prop]. *)
@@ -401,15 +385,6 @@ val hpred_get_targets : Sil.hpred -> Exp.Set.t
     [exps] *)
 val compute_reachable_hpreds : hpred list -> Exp.Set.t -> Sil.HpredSet.t * Exp.Set.t
 
-
-(** if possible, produce a (fieldname, typ) path from one of the [src_exps] to [snk_exp] using
-    [reachable_hpreds]. *)
-val get_fld_typ_path_opt : Exp.Set.t -> Exp.t -> Sil.HpredSet.t ->
-  (Ident.fieldname option * Typ.t) list option
-
-(** filter [pi] by removing the pure atoms that do not contain an expression in [exps] *)
-val compute_reachable_atoms : pi -> Exp.Set.t -> pi
-
 (** {2 Internal modules} *)
 
 module Metrics : sig

infer/src/backend/prover.ml

@@ -45,6 +45,17 @@ let rec is_java_class = function
   | Typ.Tarray (inner_typ, _) | Tptr (inner_typ, _) -> is_java_class inner_typ
   | _ -> false
 
+(** Negate an atom *)
+let atom_negate = function
+  | Sil.Aeq (Exp.BinOp (Binop.Le, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
+      Prop.mk_inequality (Exp.lt e2 e1)
+  | Sil.Aeq (Exp.BinOp (Binop.Lt, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
+      Prop.mk_inequality (Exp.le e2 e1)
+  | Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2)
+  | Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2)
+  | Sil.Apred (a, es) -> Sil.Anpred (a, es)
+  | Sil.Anpred (a, es) -> Sil.Apred (a, es)
+
 (** {2 Ordinary Theorem Proving} *)
 
 let (++) = IntLit.add
@@ -2143,7 +2154,7 @@ let check_array_bounds (sub1, sub2) prop =
           | _ -> [Exp.BinOp(Binop.PlusA, len2, Exp.minus_one)] (* only check len *) in
         IList.iter (fail_if_le len1) indices_to_check
     | ProverState.BCfrom_pre _atom ->
-        let atom_neg = Prop.atom_negate (Sil.atom_sub sub2 _atom) in
+        let atom_neg = atom_negate (Sil.atom_sub sub2 _atom) in
         (* L.d_strln_color Orange "BCFrom_pre"; Sil.d_atom atom_neg; L.d_ln (); *)
         if check_atom prop atom_neg then check_failed atom_neg in
   IList.iter check_bound (ProverState.get_bounds_checks ())
@@ -2243,7 +2254,7 @@ let is_cover cases =
     match cases with
     | [] -> check_inconsistency_pi acc_pi
     | (pi, _):: cases' ->
-        IList.for_all (fun a -> _is_cover ((Prop.atom_negate a) :: acc_pi) cases') pi in
+        IList.for_all (fun a -> _is_cover ((atom_negate a) :: acc_pi) cases') pi in
   _is_cover [] cases
 
 exception NO_COVER

infer/src/backend/prover.mli

@@ -14,6 +14,9 @@ open! Utils
 
 open Sil
 
+(** Negate an atom *)
+val atom_negate : Sil.atom -> Sil.atom
+
 (** {2 Ordinary Theorem Proving} *)
 
 (** Check [ |- e=0].  Result [false] means "don't know". *)

infer/src/backend/rearrange.ml

@@ -399,7 +399,7 @@ let strexp_extend_values
     _strexp_extend_values
       pname tenv orig_prop footprint_part kind max_stamp se typ off' inst in
   let atoms_se_typ_list_filtered =
-    let check_neg_atom atom = Prover.check_atom Prop.prop_emp (Prop.atom_negate atom) in
+    let check_neg_atom atom = Prover.check_atom Prop.prop_emp (Prover.atom_negate atom) in
     let check_not_inconsistent (atoms, _, _) = not (IList.exists check_neg_atom atoms) in
     IList.filter check_not_inconsistent atoms_se_typ_list in
   if Config.trace_rearrange then L.d_strln "exiting strexp_extend_values";