Encode polarity of predicates into atom tag

Summary:
Change representation of pure predicate applications to distinguish
between positive and negative literals using the Apred and Anpred
constructors instead of a boolean field.

This representation is more compact, and is uniform with the treatment
of equalities and disequalities.  Some code is simpler, but there isn't
much in it.

Reviewed By: cristianoc

Differential Revision: D3669387

fbshipit-source-id: 07cdea6

infer/src/IR/Cfg.re

@@ -962,7 +962,8 @@ let remove_abducted_retvars p =>
             fun
             | Sil.Aeq lhs rhs
             | Sil.Aneq lhs rhs => exp_contains lhs || exp_contains rhs
-            | Sil.Apred _ _ e => exp_contains e
+            | Sil.Apred _ e
+            | Sil.Anpred _ e => exp_contains e
           )
           pi
       };

infer/src/IR/Sil.re

@@ -203,7 +203,8 @@ type offset = | Off_fld of Ident.fieldname Typ.t | Off_index of exp;
 type atom =
   | Aeq of exp exp /** equality */
   | Aneq of exp exp /** disequality */
-  | Apred of bool attribute exp /** possibly negated predicate symbol applied to an exp */;
+  | Apred of attribute exp /** predicate symbol applied to an exp */
+  | Anpred of attribute exp /** negated predicate symbol applied to an exp */;
 
 
 /** kind of lseg or dllseg predicates */
@@ -704,11 +705,16 @@ let atom_compare a b =>
       }
     | (Aneq _, _) => (-1)
     | (_, Aneq _) => 1
-    | (Apred b1 a1 e1, Apred b2 a2 e2) =>
-      let n = bool_compare b1 b2;
+    | (Apred a1 e1, Apred a2 e2) =>
+      let n = attribute_compare a1 a2;
       if (n != 0) {
         n
       } else {
+        exp_compare e1 e2
+      }
+    | (Apred _, _) => (-1)
+    | (_, Apred _) => 1
+    | (Anpred a1 e1, Anpred a2 e2) =>
       let n = attribute_compare a1 a2;
       if (n != 0) {
         n
@@ -716,7 +722,6 @@ let atom_compare a b =>
         exp_compare e1 e2
       }
     }
-    }
   };
 
 let atom_equal x y => atom_compare x y == 0;
@@ -1281,7 +1286,8 @@ let pp_atom pe0 f a => {
     | PP_HTML => F.fprintf f "%a != %a" (pp_exp pe) e1 (pp_exp pe) e2
     | PP_LATEX => F.fprintf f "%a{\\neq}%a" (pp_exp pe) e1 (pp_exp pe) e2
     }
-  | Apred b a e => F.fprintf f "%s%s(%a)" (b ? "" : "!") (attribute_to_string pe a) (pp_exp pe) e
+  | Apred a e => F.fprintf f "%s(%a)" (attribute_to_string pe a) (pp_exp pe) e
+  | Anpred a e => F.fprintf f "!%s(%a)" (attribute_to_string pe a) (pp_exp pe) e
   };
   color_post_wrapper changed pe0 f
 };
@@ -1936,7 +1942,8 @@ let atom_expmap (f: exp => exp) =>
   fun
   | Aeq e1 e2 => Aeq (f e1) (f e2)
   | Aneq e1 e2 => Aneq (f e1) (f e2)
-  | Apred b a e => Apred b a (f e);
+  | Apred a e => Apred a (f e)
+  | Anpred a e => Anpred a (f e);
 
 let atom_list_expmap (f: exp => exp) (alist: list atom) => IList.map (atom_expmap f) alist;
 
@@ -2073,7 +2080,8 @@ let atom_fpv =
   fun
   | Aeq e1 e2 => exp_fpv e1 @ exp_fpv e2
   | Aneq e1 e2 => exp_fpv e1 @ exp_fpv e2
-  | Apred _ _ e => exp_fpv e;
+  | Apred _ e
+  | Anpred _ e => exp_fpv e;
 
 let rec strexp_fpv =
   fun
@@ -2284,7 +2292,8 @@ let atom_fav_add fav =>
       exp_fav_add fav e1;
       exp_fav_add fav e2
     }
-  | Apred _ _ e => exp_fav_add fav e;
+  | Apred _ e
+  | Anpred _ e => exp_fav_add fav e;
 
 let atom_fav = fav_imperative_to_functional atom_fav_add;
 
@@ -3204,19 +3213,7 @@ let exp_replace_exp epairs e =>
   | Not_found => e
   };
 
-let atom_replace_exp epairs =>
-  fun
-  | Aeq e1 e2 => {
-      let e1' = exp_replace_exp epairs e1;
-      let e2' = exp_replace_exp epairs e2;
-      Aeq e1' e2'
-    }
-  | Aneq e1 e2 => {
-      let e1' = exp_replace_exp epairs e1;
-      let e2' = exp_replace_exp epairs e2;
-      Aneq e1' e2'
-    }
-  | Apred b a e => Apred b a (exp_replace_exp epairs e);
+let atom_replace_exp epairs atom => atom_expmap (fun e => exp_replace_exp epairs e) atom;
 
 let rec strexp_replace_exp epairs =>
   fun

infer/src/IR/Sil.rei

@@ -197,7 +197,8 @@ type offset = | Off_fld of Ident.fieldname Typ.t | Off_index of exp;
 type atom =
   | Aeq of exp exp /** equality */
   | Aneq of exp exp /** disequality */
-  | Apred of bool attribute exp /** possibly negated predicate symbol applied to an exp */;
+  | Apred of attribute exp /** predicate symbol applied to an exp */
+  | Anpred of attribute exp /** negated predicate symbol applied to an exp */;
 
 
 /** kind of lseg or dllseg predicates */

infer/src/backend/abs.ml

@@ -788,8 +788,8 @@ let abstract_pure_part p ~(from_abstract_footprint: bool) =
                 | Sil.Const _ -> a :: pi
                 | _ -> pi)
            | Sil.Aneq (Var _, _)
-           | Sil.Apred (_, _, Var _) -> a :: pi
-           | Sil.Aeq _ | Aneq _ | Apred _ -> pi
+           | Sil.Apred (_, Var _) | Anpred (_, Var _) -> a :: pi
+           | Sil.Aeq _ | Aneq _ | Apred _ | Anpred _ -> pi
         )
         [] pi_filtered in
     IList.rev new_pure in
@@ -820,7 +820,7 @@ let abstract_gc p =
         let no_fav_e1 = Sil.fav_is_empty fav_e1 in
         let no_fav_e2 = Sil.fav_is_empty fav_e2 in
         (no_fav_e1 || intersect_e1 ()) && (no_fav_e2 || intersect_e2 ())
-    | Sil.Apred (_, _, e) ->
+    | Sil.Apred (_, e) | Anpred (_, e) ->
         let fav_e = Sil.exp_fav e in
         Sil.fav_is_empty fav_e
         ||

infer/src/backend/dom.ml

@@ -718,9 +718,13 @@ end = struct
           when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
             build_other_atoms (fun e0 -> Prop.mk_neq e0 e') side e
 
-        | Sil.Apred (b, a, (Var id as e))
+        | Sil.Apred (a, (Var id as e))
           when not (Ident.is_normal id) ->
-            build_other_atoms (fun e0 -> Prop.mk_pred b a e0) side e
+            build_other_atoms (fun e0 -> Prop.mk_pred a e0) side e
+
+        | Sil.Anpred (a, (Var id as e))
+          when not (Ident.is_normal id) ->
+            build_other_atoms (fun e0 -> Prop.mk_npred a e0) side e
 
         | Sil.Aeq((Sil.Var id as e), e') | Sil.Aeq(e', (Sil.Var id as e))
           when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
@@ -738,7 +742,7 @@ end = struct
             let construct e0 = Prop.mk_inequality (Sil.BinOp(Binop.Lt, e', e0)) in
             build_other_atoms construct side e
 
-        | Sil.Aeq _ | Aneq _ | Apred _ -> None
+        | Sil.Aeq _ | Aneq _ | Apred _ | Anpred _ -> None
       end
 
   type data_opt = ExtFresh | ExtDefault of Sil.exp
@@ -1670,7 +1674,7 @@ let pi_partial_join mode
         true
     | Sil.Aneq _ -> false
     | Sil.Aeq _ as e -> Prop.atom_is_inequality e
-    | Sil.Apred (_, _, e) ->
+    | Sil.Apred (_, e) | Anpred (_, e) ->
         exp_is_const e in
   begin
     if Config.trace_join then begin

infer/src/backend/dotty.ml

@@ -1309,7 +1309,9 @@ let atom_to_xml_light (a: Sil.atom) : Io_infer.Xml.node =
     | Sil.Aneq _ ->
         "disequality"
     | Sil.Apred _ ->
-        "pred" in
+        "pred"
+    | Sil.Anpred _ ->
+        "npred" in
   Io_infer.Xml.create_tree "stack-variable" [("type", kind_info); ("instance", atom_to_xml_string a)] []
 
 let xml_pure_info prop =

infer/src/backend/prop.ml

@@ -1034,8 +1034,10 @@ let atom_normalize sub a0 =
         handle_boolean_operation true e1 e2
     | Sil.Aneq (e1, e2) ->
         handle_boolean_operation false e1 e2
-    | Sil.Apred (b, a, e) ->
-        Sil.Apred (b, a, exp_normalize sub e) in
+    | Sil.Apred (a, e) ->
+        Sil.Apred (a, exp_normalize sub e)
+    | Sil.Anpred (a, e) ->
+        Sil.Anpred (a, exp_normalize sub e) in
   if atom_is_inequality a' then inequality_normalize a' else a'
 
 (** Negate an atom *)
@@ -1046,7 +1048,8 @@ let atom_negate = function
       mk_inequality (Sil.exp_le e2 e1)
   | Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2)
   | Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2)
-  | Sil.Apred (b, a, e) -> Sil.Apred (not b, a, e)
+  | Sil.Apred (a, e) -> Sil.Anpred (a, e)
+  | Sil.Anpred (a, e) -> Sil.Apred (a, e)
 
 let rec strexp_normalize sub se =
   match se with
@@ -1478,11 +1481,18 @@ let mk_eq e1 e2 =
        atom_normalize Sil.sub_empty (Sil.Aeq (ne1, ne2))) ()
 
 (** Construct a pred. *)
-let mk_pred b a e =
+let mk_pred a e =
   Config.run_with_abs_val_equal_zero
     (fun () ->
        let ne = exp_normalize Sil.sub_empty e in
-       atom_normalize Sil.sub_empty (Apred (b, a, ne))) ()
+       atom_normalize Sil.sub_empty (Apred (a, ne))) ()
+
+(** Construct a negated pred. *)
+let mk_npred a e =
+  Config.run_with_abs_val_equal_zero
+    (fun () ->
+       let ne = exp_normalize Sil.sub_empty e in
+       atom_normalize Sil.sub_empty (Anpred (a, ne))) ()
 
 (** Construct a points-to predicate for a single program variable.
     If [expand_structs] is true, initialize the fields of structs with fresh variables. *)
@@ -1616,8 +1626,8 @@ let compute_reachable_atoms pi exps =
     | _ -> false in
   IList.filter
     (function
-      | Sil.Aeq (lhs, rhs) | Sil.Aneq (lhs, rhs) -> exp_contains lhs || exp_contains rhs
-      | Sil.Apred (_, _, e) -> exp_contains e)
+      | Sil.Aeq (lhs, rhs) | Aneq (lhs, rhs) -> exp_contains lhs || exp_contains rhs
+      | Sil.Apred (_, e) | Anpred (_, e) -> exp_contains e)
     pi
 
 (** Eliminates all empty lsegs from sigma, and collect equalities
@@ -1781,7 +1791,8 @@ let prop_reset_inst inst_map prop =
 
 (** Return the exp and attribute marked in the atom if any, and return None otherwise *)
 let atom_get_exp_attribute = function
-  | Sil.Apred (p, a, e) -> Some (p, a, e)
+  | Sil.Apred (a, e) -> Some (true, a, e)
+  | Sil.Anpred (a, e) -> Some (false, a, e)
   | _ -> None
 
 (** Check whether an atom is used to mark an attribute *)
@@ -1793,7 +1804,8 @@ let get_exp_attributes prop exp =
   let nexp = exp_normalize_prop prop exp in
   let atom_get_attr attributes atom =
     match atom with
-    | Sil.Apred (pol, att, e) when Sil.exp_equal e nexp -> (pol, att) :: attributes
+    | Sil.Apred (att, e) when Sil.exp_equal e nexp -> (true, att) :: attributes
+    | Sil.Anpred (att, e) when Sil.exp_equal e nexp -> (false, att) :: attributes
     | _ -> attributes in
   IList.fold_left atom_get_attr [] prop.pi
 
@@ -1850,17 +1862,18 @@ let get_all_attributes prop =
 
 (** Set an attribute associated to the expression *)
 let set_exp_attribute ?(footprint = false) ?(polarity = true) prop attr exp =
-  prop_atom_and ~footprint prop (Sil.Apred (polarity, attr, exp))
+  prop_atom_and ~footprint prop
+    (if polarity then Sil.Apred (attr, exp) else Sil.Anpred (attr, exp))
 
 (** Replace an attribute associated to the expression *)
 let add_or_replace_exp_attribute_check_changed check_attribute_change prop pol0 att0 exp =
   let nexp = exp_normalize_prop prop exp in
   let atom_map a = match a with
-    | Sil.Apred (_, att, e) ->
+    | Sil.Apred (att, e) | Anpred (att, e) ->
         if Sil.exp_equal nexp e && attributes_in_same_category att att0 then
           begin
             check_attribute_change att att0;
-            Sil.Apred (pol0, att0, e)
+            if pol0 then Sil.Apred (att0, e) else Sil.Anpred (att0, e)
           end
         else a
     | _ -> a in
@@ -1886,8 +1899,12 @@ let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_po
 
 let remove_attribute_by_filter ~f prop =
   let atom_remove atom pi = match atom with
-    | Sil.Apred (pol, att_old, exp) ->
-        if f pol att_old exp then
+    | Sil.Apred (att_old, exp) ->
+        if f true att_old exp then
+          pi
+        else atom:: pi
+    | Sil.Anpred (att_old, exp) ->
+        if f false att_old exp then
           pi
         else atom:: pi
     | _ -> atom:: pi in
@@ -1940,7 +1957,7 @@ let rec nullify_exp_with_objc_null prop exp =
 (** Get all the attributes of the prop *)
 let get_atoms_with_attribute att prop =
   let atom_remove atom autoreleased_atoms = match atom with
-    | Sil.Apred (_, att_old, e) ->
+    | Sil.Apred (att_old, e) | Anpred (att_old, e) ->
         if Sil.attribute_equal att_old att then
           e:: autoreleased_atoms
         else autoreleased_atoms
@@ -1949,15 +1966,14 @@ let get_atoms_with_attribute att prop =
 
 (** Apply f to every resource attribute in the prop *)
 let attribute_map_resource prop f =
-  let pi = get_pi prop in
   let attribute_map e = function
     | Sil.Aresource ra -> Sil.Aresource (f e ra)
     | att -> att in
   let atom_map = function
-    | Sil.Apred (b, att, e) -> Sil.Apred (b, attribute_map e att, e)
+    | Sil.Apred (att, e) -> Sil.Apred (attribute_map e att, e)
+    | Sil.Anpred (att, e) -> Sil.Anpred (attribute_map e att, e)
     | atom -> atom in
-  let pi' = IList.map atom_map pi in
-  replace_pi pi' prop
+  replace_pi (IList.map atom_map (get_pi prop)) prop
 
 (** type for arithmetic problems *)
 type arith_problem =
@@ -2296,8 +2312,10 @@ let atom_captured_ren ren = function
       Sil.Aeq (exp_captured_ren ren e1, exp_captured_ren ren e2)
   | Sil.Aneq (e1, e2) ->
       Sil.Aneq (exp_captured_ren ren e1, exp_captured_ren ren e2)
-  | Sil.Apred (b, a, e) ->
-      Sil.Apred (b, a, exp_captured_ren ren e)
+  | Sil.Apred (a, e) ->
+      Sil.Apred (a, exp_captured_ren ren e)
+  | Sil.Anpred (a, e) ->
+      Sil.Anpred (a, exp_captured_ren ren e)
 
 let rec strexp_captured_ren ren = function
   | Sil.Eexp (e, inst) ->

infer/src/backend/prop.mli

@@ -222,8 +222,11 @@ val mk_neq : exp -> exp -> atom
 (** Construct an equality. *)
 val mk_eq : exp -> exp -> atom
 
-(** Construct a pred. *)
-val mk_pred : bool -> attribute -> exp -> atom
+(** Construct a positive pred. *)
+val mk_pred : attribute -> exp -> atom
+
+(** Construct a negative pred. *)
+val mk_npred : attribute -> exp -> atom
 
 (** create a strexp of the given type, populating the structures if [expand_structs] is true *)
 val create_strexp_of_type :

infer/src/backend/propgraph.ml

@@ -49,7 +49,7 @@ let edge_get_source = function
   | Ehpred (Sil.Hdllseg(_, _, e1, _, _, _, _)) -> e1 (* only one direction supported for now *)
   | Eatom (Sil.Aeq (e1, _)) -> e1
   | Eatom (Sil.Aneq (e1, _)) -> e1
-  | Eatom (Sil.Apred (_, _, e)) -> e
+  | Eatom (Sil.Apred (_, e) | Anpred (_, e)) -> e
   | Esub_entry (x, _) -> Sil.Var x
 
 (** Return the successor nodes of the edge *)
@@ -57,7 +57,7 @@ let edge_get_succs = function
   | Ehpred hpred -> Sil.ExpSet.elements (Prop.hpred_get_targets hpred)
   | Eatom (Sil.Aeq (_, e2)) -> [e2]
   | Eatom (Sil.Aneq (_, e2)) -> [e2]
-  | Eatom (Sil.Apred _) -> []
+  | Eatom (Sil.Apred _ | Anpred _) -> []
   | Esub_entry (_, e) -> [e]
 
 let get_sigma footprint_part g =
@@ -159,7 +159,9 @@ let compute_edge_diff (oldedge: edge) (newedge: edge) : Obj.t list = match olded
       compute_exp_diff e1 e2
   | Eatom (Sil.Aneq (_, e1)), Eatom (Sil.Aneq (_, e2)) ->
       compute_exp_diff e1 e2
-  | Eatom (Sil.Apred (_, _, e1)), Eatom (Sil.Apred (_, _, e2)) ->
+  | Eatom (Sil.Apred (_, e1)), Eatom (Sil.Apred (_, e2)) ->
+      compute_exp_diff e1 e2
+  | Eatom (Sil.Anpred (_, e1)), Eatom (Sil.Anpred (_, e2)) ->
       compute_exp_diff e1 e2
   | Esub_entry (_, e1), Esub_entry (_, e2) ->
       compute_exp_diff e1 e2

infer/src/backend/prover.ml

@@ -364,7 +364,7 @@ end = struct
       | Sil.Aeq (Sil.BinOp (Binop.Lt, e1, e2), Sil.Const (Const.Cint i)) when IntLit.isone i ->
           lts := (e1, e2) :: !lts (* < *)
       | Sil.Aeq _
-      | Sil.Apred _ -> () in
+      | Sil.Apred _ | Anpred _ -> () in
     IList.iter process_atom pi;
     saturate { leqs = !leqs; lts = !lts; neqs = !neqs }
 
@@ -741,7 +741,7 @@ let check_atom prop a0 =
     when IntLit.isone i -> check_lt_normalized prop e1 e2
   | Sil.Aeq (e1, e2) -> check_equal prop e1 e2
   | Sil.Aneq (e1, e2) -> check_disequal prop e1 e2
-  | Sil.Apred _ -> IList.exists (Sil.atom_equal a) (Prop.get_pi prop)
+  | Sil.Apred _ | Anpred _ -> IList.exists (Sil.atom_equal a) (Prop.get_pi prop)
 
 (** Check [prop |- e1<=e2]. Result [false] means "don't know". *)
 let check_le prop e1 e2 =
@@ -859,7 +859,7 @@ let check_inconsistency_base prop =
         (match e1, e2 with
          | Sil.Const c1, Sil.Const c2 -> Const.equal c1 c2
          | _ -> (Sil.exp_compare e1 e2 = 0))
-    | Sil.Apred _ -> false in
+    | Sil.Apred _ | Anpred _ -> false in
   let inconsistent_inequalities () =
     let ineq = Inequalities.from_prop prop in
     (*
@@ -2111,7 +2111,7 @@ let rec pre_check_pure_implication calc_missing subs pi1 pi2 =
         )
   | Sil.Aeq _ :: pi2' -> (* must be an inequality *)
       pre_check_pure_implication calc_missing subs pi1 pi2'
-  | (Sil.Aneq (e, _) | Apred (_, _, e)) :: pi2' ->
+  | (Sil.Aneq (e, _) | Apred (_, e) | Anpred (_, e)) :: pi2' ->
       if calc_missing || (match e with Var v -> Ident.is_primed v | _ -> false) then
         pre_check_pure_implication calc_missing subs pi1 pi2'
       else

infer/src/backend/tabulation.ml

@@ -385,12 +385,12 @@ let post_process_post
     | Some (true, Aresource ({ ra_kind = Rrelease })) -> true
     | _ -> false in
   let atom_update_alloc_attribute = function
-    | Sil.Apred (true, Aresource ra, e)
+    | Sil.Apred (Aresource ra, e)
       when not (ra.Sil.ra_kind = Sil.Rrelease && actual_pre_has_freed_attribute e) ->
         (* unless it was already freed before the call *)
         let vpath, _ = Errdesc.vpath_find post e in
         let ra' = { ra with Sil.ra_pname = callee_pname; Sil.ra_loc = loc; Sil.ra_vpath = vpath } in
-        Sil.Apred (true, Aresource ra', e)
+        Sil.Apred (Aresource ra', e)
     | a -> a in
   let prop' = Prop.replace_sigma (post_process_sigma (Prop.get_sigma post) loc) post in
   let pi' = IList.map atom_update_alloc_attribute (Prop.get_pi prop') in