From a8ce65b22139b2521984616a6889770401558f1d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 8 Aug 2016 09:46:01 -0700 Subject: [PATCH] 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 | 3 +- infer/src/IR/Sil.re | 49 +++++++++++++-------------- infer/src/IR/Sil.rei | 3 +- infer/src/backend/abs.ml | 6 ++-- infer/src/backend/dom.ml | 12 ++++--- infer/src/backend/dotty.ml | 4 ++- infer/src/backend/prop.ml | 60 +++++++++++++++++++++------------ infer/src/backend/prop.mli | 7 ++-- infer/src/backend/propgraph.ml | 8 +++-- infer/src/backend/prover.ml | 8 ++--- infer/src/backend/tabulation.ml | 4 +-- 11 files changed, 96 insertions(+), 68 deletions(-) diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index 7415bc21e..098adbb7e 100644 --- a/infer/src/IR/Cfg.re +++ b/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 }; diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 2bba6f256..13e609ef4 100644 --- a/infer/src/IR/Sil.re +++ b/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,17 +705,21 @@ 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 { - let n = attribute_compare a1 a2; - if (n != 0) { - n - } else { - exp_compare e1 e2 - } + exp_compare e1 e2 + } + | (Apred _, _) => (-1) + | (_, Apred _) => 1 + | (Anpred a1 e1, Anpred a2 e2) => + let n = attribute_compare a1 a2; + if (n != 0) { + n + } else { + exp_compare e1 e2 } } }; @@ -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 diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index fec0a30e9..5c7694c0e 100644 --- a/infer/src/IR/Sil.rei +++ b/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 */ diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 462a22375..90b731d5e 100644 --- a/infer/src/backend/abs.ml +++ b/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 || diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 1bc249c0c..5f455cc2f 100644 --- a/infer/src/backend/dom.ml +++ b/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 diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index f8f4e6b0c..9168c52be 100644 --- a/infer/src/backend/dotty.ml +++ b/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 = diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 22d2232c0..2fbb0487a 100644 --- a/infer/src/backend/prop.ml +++ b/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) -> diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index fd5ab1fcd..6fd65102f 100644 --- a/infer/src/backend/prop.mli +++ b/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 : diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml index 096bbf298..1d3bdf540 100644 --- a/infer/src/backend/propgraph.ml +++ b/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 diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 0e7afca7b..71d0526da 100644 --- a/infer/src/backend/prover.ml +++ b/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 diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 1f1e73da7..179a12f13 100644 --- a/infer/src/backend/tabulation.ml +++ b/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