From b48ec1ac93e80f3ba50e5e80593e379598aac87c Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Wed, 10 Aug 2016 03:32:37 -0700 Subject: [PATCH] Clean up API to access components of propositions. Summary: Clean up the API to access component of propositions. Use uniform naming for getting and setting components. Reviewed By: jberdine Differential Revision: D3696180 fbshipit-source-id: a8aedb0 --- infer/src/IR/Cfg.re | 18 +-- infer/src/backend/Attribute.ml | 31 ++-- infer/src/backend/abs.ml | 64 ++++---- infer/src/backend/absarray.ml | 75 +++------- infer/src/backend/dom.ml | 54 +++---- infer/src/backend/dotty.ml | 35 +++-- infer/src/backend/errdesc.ml | 12 +- infer/src/backend/interproc.ml | 29 ++-- infer/src/backend/modelBuiltins.ml | 54 +++---- infer/src/backend/prop.ml | 228 +++++++++-------------------- infer/src/backend/prop.mli | 42 ++---- infer/src/backend/propgraph.ml | 10 +- infer/src/backend/prover.ml | 41 +++--- infer/src/backend/rearrange.ml | 18 +-- infer/src/backend/symExec.ml | 38 ++--- infer/src/backend/tabulation.ml | 64 ++++---- infer/src/backend/taint.ml | 2 +- 17 files changed, 340 insertions(+), 475 deletions(-) diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index 8de31709b..d64d2b8c2 100644 --- a/infer/src/IR/Cfg.re +++ b/infer/src/IR/Cfg.re @@ -879,7 +879,7 @@ let get_name_of_objc_static_locals (curr_f: Procdesc.t) p => { | Sil.Hpointsto e _ _ => [local_static e] | _ => [] }; - let vars_sigma = IList.map hpred_local_static (Prop.get_sigma p); + let vars_sigma = IList.map hpred_local_static p.Prop.sigma; IList.flatten (IList.flatten vars_sigma) }; @@ -895,7 +895,7 @@ let get_name_of_objc_block_locals p => { | Sil.Hpointsto e _ _ => [local_blocks e] | _ => [] }; - let vars_sigma = IList.map hpred_local_blocks (Prop.get_sigma p); + let vars_sigma = IList.map hpred_local_blocks p.Prop.sigma; IList.flatten (IList.flatten vars_sigma) }; @@ -903,7 +903,7 @@ let remove_abducted_retvars p => /* compute the hpreds and pure atoms reachable from the set of seed expressions in [exps] */ { let compute_reachable p seed_exps => { - let (sigma, pi) = (Prop.get_sigma p, Prop.get_pi p); + let (sigma, pi) = (p.Prop.sigma, p.Prop.pi); let rec collect_exps exps => fun | Sil.Eexp (Exp.Exn e) _ => Exp.Set.add e exps @@ -986,7 +986,7 @@ let remove_abducted_retvars p => } ) ([], []) - (Prop.get_sigma p); + p.Prop.sigma; let (_, p') = Attribute.deallocate_stack_vars p abducteds; let normal_pvar_set = IList.fold_left @@ -995,7 +995,7 @@ let remove_abducted_retvars p => normal_pvars; /* walk forward from non-abducted pvars, keep everything reachable. remove everything else */ let (sigma_reach, pi_reach) = compute_reachable p' normal_pvar_set; - Prop.normalize (Prop.replace_pi pi_reach (Prop.replace_sigma sigma_reach p')) + Prop.normalize (Prop.set p' pi::pi_reach sigma::sigma_reach) }; let remove_locals (curr_f: Procdesc.t) p => { @@ -1055,9 +1055,9 @@ let remove_seed_vars (prop: Prop.t 'a) :Prop.t Prop.normal => { fun | Sil.Hpointsto (Exp.Lvar pv) _ _ => not (Pvar.is_seed pv) | _ => true; - let sigma = Prop.get_sigma prop; + let sigma = prop.sigma; let sigma' = IList.filter hpred_not_seed sigma; - Prop.normalize (Prop.replace_sigma sigma' prop) + Prop.normalize (Prop.set prop sigma::sigma') }; @@ -1112,9 +1112,9 @@ let remove_seed_captured_vars_block captured_vars prop => { Pvar.is_seed pv && IList.mem is_captured pname captured_vars } | _ => false; - let sigma = Prop.get_sigma prop; + let sigma = prop.Prop.sigma; let sigma' = IList.filter (fun hpred => not (hpred_seed_captured hpred)) sigma; - Prop.normalize (Prop.replace_sigma sigma' prop) + Prop.normalize (Prop.set prop sigma::sigma') }; diff --git a/infer/src/backend/Attribute.ml b/infer/src/backend/Attribute.ml index 80126fbb0..5f58aeb29 100644 --- a/infer/src/backend/Attribute.ml +++ b/infer/src/backend/Attribute.ml @@ -46,11 +46,11 @@ let add_or_replace_check_changed check_attribute_change prop atom0 = natom | atom -> atom in - let pi = Prop.get_pi prop in + let pi = prop.Prop.pi in let pi' = IList.map_changed atom_map pi in if pi == pi' then Prop.prop_atom_and prop natom - else Prop.normalize (Prop.replace_pi pi' prop) + else Prop.normalize (Prop.set prop ~pi:pi') | _ -> prop @@ -63,7 +63,7 @@ let add_or_replace prop atom = let get_all (prop: 'a Prop.t) = let res = ref [] in let do_atom a = if is_pred a then res := a :: !res in - IList.iter do_atom (Prop.get_pi prop); + IList.iter do_atom prop.pi; IList.rev !res (** Get all the attributes of the prop *) @@ -71,7 +71,7 @@ let get_for_symb prop att = IList.filter (function | Sil.Apred (att', _) | Anpred (att', _) -> PredSymb.equal att' att | _ -> false - ) (Prop.get_pi prop) + ) prop.Prop.pi (** Get the attribute associated to the expression, if any *) let get_for_exp (prop: 'a Prop.t) exp = @@ -80,7 +80,7 @@ let get_for_exp (prop: 'a Prop.t) exp = match atom with | Sil.Apred (_, es) | Anpred (_, es) when IList.mem Exp.equal nexp es -> atom :: attributes | _ -> attributes in - IList.fold_left atom_get_attr [] (Prop.get_pi prop) + IList.fold_left atom_get_attr [] prop.pi let get prop exp category = let atts = get_for_exp prop exp in @@ -125,12 +125,12 @@ let has_dangling_uninit prop exp = ) la let filter_atoms ~f prop = - let pi0 = Prop.get_pi prop in + let pi0 = prop.Prop.pi in let pi1 = IList.filter_changed f pi0 in if pi1 == pi0 then prop else - Prop.normalize (Prop.replace_pi pi1 prop) + Prop.normalize (Prop.set prop ~pi:pi1) let remove prop atom = if is_pred atom then @@ -164,12 +164,12 @@ let map_resource prop f = | Sil.Apred (att, ([e] as es)) -> Sil.Apred (attribute_map e att, es) | Sil.Anpred (att, ([e] as es)) -> Sil.Anpred (attribute_map e att, es) | atom -> atom in - let pi0 = Prop.get_pi prop in + let pi0 = prop.Prop.pi in let pi1 = IList.map_changed atom_map pi0 in if pi1 == pi0 then prop else - Prop.normalize (Prop.replace_pi pi1 prop) + Prop.normalize (Prop.set prop ~pi:pi1) (* Replace an attribute OBJC_NULL($n1) with OBJC_NULL(var) when var = $n1, and also sets $n1 = 0 *) @@ -258,7 +258,7 @@ let deallocate_stack_vars (p: 'a Prop.t) pvars = | Sil.Hpointsto (Exp.Lvar v, _, _) -> IList.exists (Pvar.equal v) pvars | _ -> false in - let sigma_stack, sigma_other = IList.partition filter (Prop.get_sigma p) in + let sigma_stack, sigma_other = IList.partition filter p.sigma in let fresh_address_vars = ref [] in (* fresh vars substituted for the address of stack vars *) let stack_vars_address_in_post = ref [] in (* stack vars whose address is still present *) let exp_replace = IList.map (function @@ -267,12 +267,13 @@ let deallocate_stack_vars (p: 'a Prop.t) pvars = fresh_address_vars := (v, freshv) :: !fresh_address_vars; (Exp.Lvar v, Exp.Var freshv) | _ -> assert false) sigma_stack in - let pi1 = IList.map (fun (id, e) -> Sil.Aeq (Exp.Var id, e)) (Sil.sub_to_list (Prop.get_sub p)) in - let pi = IList.map (Sil.atom_replace_exp exp_replace) ((Prop.get_pi p) @ pi1) in + let pi1 = IList.map (fun (id, e) -> Sil.Aeq (Exp.Var id, e)) (Sil.sub_to_list p.sub) in + let pi = IList.map (Sil.atom_replace_exp exp_replace) (p.pi @ pi1) in let p' = Prop.normalize - (Prop.replace_sub Sil.sub_empty - (Prop.replace_sigma (Prop.sigma_replace_exp exp_replace sigma_other) p)) in + (Prop.set p + ~sub:Sil.sub_empty + ~sigma: (Prop.sigma_replace_exp exp_replace sigma_other)) in let p'' = let res = ref p' in let p'_fav = Prop.prop_fav p' in @@ -316,7 +317,7 @@ let find_equal_formal_path e prop = | Some vfs -> Some (Exp.Lfield (vfs, field, Typ.Tvoid)) | None -> None) | _ -> None) fields None - | _ -> None) (Prop.get_sigma prop) None in + | _ -> None) prop.Prop.sigma None in match find_in_sigma e [] with | Some vfs -> Some vfs | None -> diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 4fb80f5e1..b2cc7d056 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -74,7 +74,7 @@ let create_condition_ls ids_private id_base p_leftover (inst: Sil.subst) = let fav_insts_of_public_ids = IList.flatten (IList.map Sil.exp_fav_list insts_of_public_ids) in let fav_insts_of_private_ids = IList.flatten (IList.map Sil.exp_fav_list insts_of_private_ids) in let (fav_p_leftover, _) = - let sigma = Prop.get_sigma p_leftover in + let sigma = p_leftover.Prop.sigma in (sigma_fav_list sigma, sigma_fav_in_pvars_list sigma) in let fpv_inst_of_base = Sil.exp_fpv inst_of_base in let fpv_insts_of_private_ids = IList.flatten (IList.map Sil.exp_fpv insts_of_private_ids) in @@ -441,7 +441,7 @@ let discover_para_roots p root1 next1 root2 next2 : Sil.hpara option = else let corres = [(next1, next2)] in let todos = [(root1, root2)] in - let sigma = Prop.get_sigma p in + let sigma = p.Prop.sigma in match Match.find_partial_iso (Prover.check_equal p) corres todos sigma with | None -> None | Some (new_corres, new_sigma1, _, _) -> @@ -458,7 +458,7 @@ let discover_para_dll_roots p root1 blink1 flink1 root2 blink2 flink2 : Sil.hpar else let corres = [(blink1, blink2); (flink1, flink2)] in let todos = [(root1, root2)] in - let sigma = Prop.get_sigma p in + let sigma = p.Prop.sigma in match Match.find_partial_iso (Prover.check_equal p) corres todos sigma with | None -> None | Some (new_corres, new_sigma1, _, _) -> @@ -497,7 +497,7 @@ let discover_para_candidates tenv p = IList.fold_left f found edges_matched in let new_edges_seen = (e1, e2) :: edges_seen in find_all_consecutive_edges new_found new_edges_seen edges_notseen in - let sigma = Prop.get_sigma p in + let sigma = p.Prop.sigma in get_edges_sigma sigma; find_all_consecutive_edges [] [] !edges @@ -537,7 +537,7 @@ let discover_para_dll_candidates tenv p = IList.fold_left f found edges_matched in let new_edges_seen = (iF, blink, flink) :: edges_seen in find_all_consecutive_edges new_found new_edges_seen edges_notseen in - let sigma = Prop.get_sigma p in + let sigma = p.Prop.sigma in get_edges_sigma sigma; find_all_consecutive_edges [] [] !edges @@ -762,7 +762,7 @@ let abs_rules_apply tenv (p_in: Prop.normal Prop.t) : Prop.normal Prop.t = let abstract_pure_part p ~(from_abstract_footprint: bool) = let do_pure pure = let pi_filtered = - let sigma = Prop.get_sigma p in + let sigma = p.Prop.sigma in let fav_sigma = Prop.sigma_fav sigma in let fav_nonpure = Prop.prop_fav_nonpure p in (* vars in current and footprint sigma *) let filter atom = @@ -795,18 +795,18 @@ let abstract_pure_part p ~(from_abstract_footprint: bool) = IList.rev new_pure in let new_pure = do_pure (Prop.get_pure p) in - let eprop' = Prop.replace_pi new_pure (Prop.replace_sub Sil.sub_empty p) in + let eprop' = Prop.set p ~pi:new_pure ~sub:Sil.sub_empty in let eprop'' = if !Config.footprint && not from_abstract_footprint then - let new_pi_footprint = do_pure (Prop.get_pi_footprint p) in - Prop.replace_pi_footprint new_pi_footprint eprop' + let new_pi_footprint = do_pure p.Prop.pi_fp in + Prop.set eprop' ~pi_fp:new_pi_footprint else eprop' in Prop.normalize eprop'' (** Collect symbolic garbage from pi and sigma *) let abstract_gc p = - let pi = Prop.get_pi p in - let p_without_pi = Prop.normalize (Prop.replace_pi [] p) in + let pi = p.Prop.pi in + let p_without_pi = Prop.normalize (Prop.set p ~pi:[]) in let fav_p_without_pi = Prop.prop_fav p_without_pi in (* let weak_filter atom = let fav_atom = atom_fav atom in @@ -826,7 +826,7 @@ let abstract_gc p = || IList.intersect Ident.compare (Sil.fav_to_list fav_a) (Sil.fav_to_list fav_p_without_pi) in let new_pi = IList.filter strong_filter pi in - let prop = Prop.normalize (Prop.replace_pi new_pi p) in + let prop = Prop.normalize (Prop.set p ~pi:new_pi) in match Prop.prop_iter_create prop with | None -> prop | Some iter -> Prop.prop_iter_to_prop (Prop.prop_iter_gc_fields iter) @@ -878,7 +878,7 @@ let sigma_reachable root_fav sigma = !reach_set let get_cycle root prop = - let sigma = Prop.get_sigma prop in + let sigma = prop.Prop.sigma in let get_points_to e = match e with | Sil.Eexp(e', _) -> @@ -950,8 +950,8 @@ let get_retain_cycle_dotty _prop cycle = Dotty.dotty_prop_to_str _prop cycle | _ -> None -let get_var_retain_cycle _prop = - let sigma = Prop.get_sigma _prop in +let get_var_retain_cycle prop_ = + let sigma = prop_.Prop.sigma in let is_pvar v h = match h with | Sil.Hpointsto (Exp.Lvar _, v', _) when Sil.strexp_equal v v' -> true @@ -985,7 +985,7 @@ let get_var_retain_cycle _prop = match sigma_todo with | [] -> [] | hp:: sigma' -> - let cycle = get_cycle hp _prop in + let cycle = get_cycle hp prop_ in L.d_strln "Filtering pvar in cycle "; let cycle' = IList.flatten (IList.map find_or_block cycle) in if cycle' = [] then do_sigma sigma' @@ -1046,8 +1046,8 @@ let check_observer_is_unsubscribed_deallocation prop e = let check_junk ?original_prop pname tenv prop = let fav_sub_sigmafp = Sil.fav_new () in - Sil.sub_fav_add fav_sub_sigmafp (Prop.get_sub prop); - Prop.sigma_fav_add fav_sub_sigmafp (Prop.get_sigma_footprint prop); + Sil.sub_fav_add fav_sub_sigmafp prop.Prop.sub; + Prop.sigma_fav_add fav_sub_sigmafp prop.Prop.sigma_fp; let leaks_reported = ref [] in let remove_junk_once fp_part fav_root sigma = @@ -1190,11 +1190,13 @@ let check_junk ?original_prop pname tenv prop = let sigma' = remove_junk_once fp_part fav_root sigma in if IList.length sigma' = IList.length sigma then sigma' else remove_junk fp_part fav_root sigma' in - let sigma_new = remove_junk false fav_sub_sigmafp (Prop.get_sigma prop) in - let sigma_fp_new = remove_junk true (Sil.fav_new ()) (Prop.get_sigma_footprint prop) in - if Prop.sigma_equal (Prop.get_sigma prop) sigma_new && Prop.sigma_equal (Prop.get_sigma_footprint prop) sigma_fp_new + let sigma_new = remove_junk false fav_sub_sigmafp prop.Prop.sigma in + let sigma_fp_new = remove_junk true (Sil.fav_new ()) prop.Prop.sigma_fp in + if + Prop.sigma_equal prop.Prop.sigma sigma_new + && Prop.sigma_equal prop.Prop.sigma_fp sigma_fp_new then prop - else Prop.normalize (Prop.replace_sigma sigma_new (Prop.replace_sigma_footprint sigma_fp_new prop)) + else Prop.normalize (Prop.set prop ~sigma:sigma_new ~sigma_fp:sigma_fp_new) (** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the junk, otherwise raise a Leak exception. *) @@ -1242,12 +1244,12 @@ let get_local_stack cur_sigma init_sigma = (** Extract the footprint, add a local stack and return it as a prop *) let extract_footprint_for_abs (p : 'a Prop.t) : Prop.exposed Prop.t * Pvar.t list = - let sigma = Prop.get_sigma p in - let foot_pi = Prop.get_pi_footprint p in - let foot_sigma = Prop.get_sigma_footprint p in - let (local_stack, local_stack_pvars) = get_local_stack sigma foot_sigma in - let p0 = Prop.from_sigma (local_stack @ foot_sigma) in - let p1 = Prop.replace_pi foot_pi p0 in + let sigma = p.Prop.sigma in + let pi_fp = p.Prop.pi_fp in + let sigma_fp = p.Prop.sigma_fp in + let (local_stack, local_stack_pvars) = get_local_stack sigma sigma_fp in + let p0 = Prop.from_sigma (local_stack @ sigma_fp) in + let p1 = Prop.set p0 ~pi:pi_fp in (p1, local_stack_pvars) let remove_local_stack sigma pvars = @@ -1260,10 +1262,10 @@ let remove_local_stack sigma pvars = and sets proposition [p_foot] as footprint of [p]. *) let set_footprint_for_abs (p : 'a Prop.t) (p_foot : 'a Prop.t) local_stack_pvars : Prop.exposed Prop.t = let p_foot_pure = Prop.get_pure p_foot in - let p_foot_sigma = Prop.get_sigma p_foot in + let p_sigma_fp = p_foot.Prop.sigma in let pi = p_foot_pure in - let sigma = remove_local_stack p_foot_sigma local_stack_pvars in - Prop.replace_sigma_footprint sigma (Prop.replace_pi_footprint pi p) + let sigma = remove_local_stack p_sigma_fp local_stack_pvars in + Prop.set p ~pi_fp:pi ~sigma_fp:sigma (** Abstract the footprint of prop *) let abstract_footprint pname (tenv : Tenv.t) (prop : Prop.normal Prop.t) : Prop.normal Prop.t = diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml index dab2ec5e5..dc3c4e32c 100644 --- a/infer/src/backend/absarray.ml +++ b/infer/src/backend/absarray.ml @@ -288,12 +288,12 @@ let prop_update_sigma_and_fp_sigma (p : Prop.normal Prop.t) (update : bool -> sigma -> sigma * bool) : Prop.normal Prop.t * bool = - let sigma', changed = update false (Prop.get_sigma p) in - let ep1 = Prop.replace_sigma sigma' p in + let sigma', changed = update false p.Prop.sigma in + let ep1 = Prop.set p ~sigma:sigma' in let ep2, changed2 = if !Config.footprint then - let sigma_fp', changed' = update true (Prop.get_sigma_footprint ep1) in - (Prop.replace_sigma_footprint sigma_fp' ep1, changed') + let sigma_fp', changed' = update true ep1.Prop.sigma_fp in + (Prop.set ep1 ~sigma_fp:sigma_fp', changed') else (ep1, false) in (Prop.normalize ep2, changed || changed2) @@ -316,8 +316,8 @@ let generic_strexp_abstract r in let find_strexp_to_abstract p0 = let find sigma = StrexpMatch.find sigma can_abstract in - let matchings_cur = find (Prop.get_sigma p0) in - let matchings_fp = find (Prop.get_sigma_footprint p0) in + let matchings_cur = find p0.Prop.sigma in + let matchings_fp = find p0.Prop.sigma_fp in matchings_cur, matchings_fp in let match_select_next (matchings_cur, matchings_fp) = match matchings_cur, matchings_fp with @@ -364,7 +364,7 @@ let index_is_pointed_to (p: Prop.normal Prop.t) (path: StrexpMatch.path) (index: let filter = function | Sil.Hpointsto (_, Sil.Eexp (e, _), _) -> IList.exists (Exp.equal e) pointers | _ -> false in - IList.exists filter (Prop.get_sigma p) + IList.exists filter p.Prop.sigma (** Given [p] containing an array at [path], blur [index] in it *) @@ -381,17 +381,17 @@ let blur_array_index try if !Config.footprint then begin - let sigma_fp = Prop.get_sigma_footprint p in + let sigma_fp = p.Prop.sigma_fp in let matched_fp = StrexpMatch.find_path sigma_fp path in let sigma_fp' = StrexpMatch.replace_index true matched_fp index fresh_index in - Prop.replace_sigma_footprint sigma_fp' p + Prop.set p ~sigma_fp:sigma_fp' end else Prop.expose p with Not_found -> Prop.expose p in let p3 = - let matched = StrexpMatch.find_path (Prop.get_sigma p) path in + let matched = StrexpMatch.find_path p.Prop.sigma path in let sigma' = StrexpMatch.replace_index false matched index fresh_index in - Prop.replace_sigma sigma' p2 in + Prop.set p2 ~sigma:sigma' in let p4 = let index_next = Exp.BinOp(Binop.PlusA, index, Exp.one) in let fresh_index_next = Exp.BinOp (Binop.PlusA, fresh_index, Exp.one) in @@ -550,8 +550,8 @@ let check_after_array_abstraction prop = | Sil.Hlseg _ | Sil.Hdllseg _ -> () in let check_sigma sigma = IList.iter check_hpred sigma in (* check_footprint_pure prop; *) - check_sigma (Prop.get_sigma prop); - check_sigma (Prop.get_sigma_footprint prop) + check_sigma prop.Prop.sigma; + check_sigma prop.Prop.sigma_fp (** Apply array abstraction and check the result *) let abstract_array_check p = @@ -566,11 +566,11 @@ let remove_redundant_elements prop = let fav_curr = Sil.fav_new () in let fav_foot = Sil.fav_new () in Sil.fav_duplicates := true; - Sil.sub_fav_add fav_curr (Prop.get_sub prop); - Prop.pi_fav_add fav_curr (Prop.get_pi prop); - Prop.sigma_fav_add fav_curr (Prop.get_sigma prop); - Prop.pi_fav_add fav_foot (Prop.get_pi_footprint prop); - Prop.sigma_fav_add fav_foot (Prop.get_sigma_footprint prop); + Sil.sub_fav_add fav_curr prop.Prop.sub; + Prop.pi_fav_add fav_curr prop.Prop.pi; + Prop.sigma_fav_add fav_curr prop.Prop.sigma; + Prop.pi_fav_add fav_foot prop.Prop.pi_fp; + Prop.sigma_fav_add fav_foot prop.Prop.sigma_fp; let favl_curr = Sil.fav_to_list fav_curr in let favl_foot = Sil.fav_to_list fav_foot in Sil.fav_duplicates := false; @@ -605,42 +605,9 @@ let remove_redundant_elements prop = Sil.Hpointsto (e, se', te) | hpred -> hpred in let remove_redundant_sigma fp_part sigma = IList.map (remove_redundant_hpred fp_part) sigma in - let sigma' = remove_redundant_sigma false (Prop.get_sigma prop) in - let foot_sigma' = remove_redundant_sigma true (Prop.get_sigma_footprint prop) in + let sigma' = remove_redundant_sigma false prop.Prop.sigma in + let sigma_fp' = remove_redundant_sigma true prop.Prop.sigma_fp in if !modified then - let prop' = Prop.replace_sigma sigma' (Prop.replace_sigma_footprint foot_sigma' prop) in + let prop' = Prop.set prop ~sigma:sigma' ~sigma_fp:sigma_fp' in Prop.normalize prop' else prop - -(* -(** This function uses [update] and transforms the sigma of the - current SH of [p] or that of the footprint of [p], depending on - [footprint_part]. *) -let prop_update_sigma_or_fp_sigma - (footprint_part : bool) (p : Prop.normal Prop.t) (update : bool -> sigma -> sigma * bool) - : Prop.normal Prop.t * bool = - let ep1, changed1 = - if footprint_part then (Prop.expose p, false) - else - let sigma', changed = update false (Prop.get_sigma p) in - (Prop.replace_sigma sigma' p, changed) in - let ep2, changed2 = - if not footprint_part then (ep1, false) - else - begin - (if not !Config.footprint then assert false); (* always run in the footprint mode *) - let sigma_fp', changed = update true (Prop.get_sigma_footprint ep1) in - (Prop.replace_sigma_footprint sigma_fp' ep1, changed) - end in - (Prop.normalize ep2, changed1 || changed2) - -let check_footprint_pure prop = - let fav_pure = Sil.fav_new () in - Prop.pi_fav_add fav_pure (Prop.get_pure prop @ Prop.get_pi_footprint prop); - let fav_sigma = Sil.fav_new () in - Prop.sigma_fav_add fav_sigma (Prop.get_sigma prop @ Prop.get_sigma_footprint prop); - Sil.fav_filter_ident fav_pure Ident.is_footprint; - Sil.fav_filter_ident fav_sigma Ident.is_footprint; - if not (Sil.fav_subset_ident fav_pure fav_sigma) - then (L.d_strln "footprint vars in pure and not in sigma"; report_error prop) -*) diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 859828dcd..0f8c8f8b9 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -1586,7 +1586,7 @@ let pi_partial_join mode | Sil.Hpointsto (_, Sil.Earray (Exp.Const (Const.Cint n), _, _), _) -> (if IntLit.geq n IntLit.one then len_list := n :: !len_list) | _ -> () in - IList.iter do_hpred (Prop.get_sigma prop); + IList.iter do_hpred prop.Prop.sigma; !len_list in let bounds = let bounds1 = get_array_len ep1 in @@ -1718,8 +1718,8 @@ let pi_partial_meet (p: Prop.normal Prop.t) (ep1: 'a Prop.t) (ep2: 'b Prop.t) : let f2 p' atom = Prop.prop_atom_and p' (handle_atom sub2 dom2 atom) in - let pi1 = Prop.get_pi ep1 in - let pi2 = Prop.get_pi ep2 in + let pi1 = ep1.Prop.pi in + let pi2 = ep2.Prop.pi in let p_pi1 = IList.fold_left f1 p pi1 in let p_pi2 = IList.fold_left f2 p_pi1 pi2 in @@ -1730,16 +1730,16 @@ let pi_partial_meet (p: Prop.normal Prop.t) (ep1: 'a Prop.t) (ep2: 'b Prop.t) : let eprop_partial_meet (ep1: 'a Prop.t) (ep2: 'b Prop.t) : 'c Prop.t = SymOp.pay(); (* pay one symop *) - let sigma1 = Prop.get_sigma ep1 in - let sigma2 = Prop.get_sigma ep2 in + let sigma1 = ep1.Prop.sigma in + let sigma2 = ep2.Prop.sigma in let es1 = sigma_get_start_lexps_sort sigma1 in let es2 = sigma_get_start_lexps_sort sigma2 in let es = IList.merge_sorted_nodup Exp.compare [] es1 es2 in let sub_check _ = - let sub1 = Prop.get_sub ep1 in - let sub2 = Prop.get_sub ep2 in + let sub1 = ep1.Prop.sub in + let sub2 = ep2.Prop.sub in let range1 = Sil.sub_range sub1 in let f e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in Sil.sub_equal sub1 sub2 && IList.for_all f range1 in @@ -1750,8 +1750,8 @@ let eprop_partial_meet (ep1: 'a Prop.t) (ep2: 'b Prop.t) : 'c Prop.t = let todos = IList.map (fun x -> (x, x, x)) es in IList.iter Todo.push todos; let sigma_new = sigma_partial_meet sigma1 sigma2 in - let ep = Prop.replace_sigma sigma_new ep1 in - let ep' = Prop.replace_pi [] ep in + let ep = Prop.set ep1 ~sigma:sigma_new in + let ep' = Prop.set ep ~pi:[] in let p' = Prop.normalize ep' in let p'' = pi_partial_meet p' ep1 ep2 in let res = Prop.prop_rename_primed_footprint_vars p'' in @@ -1774,8 +1774,8 @@ let prop_partial_meet p1 p2 = let eprop_partial_join' mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed Prop.t) : Prop.normal Prop.t = SymOp.pay(); (* pay one symop *) - let sigma1 = Prop.get_sigma ep1 in - let sigma2 = Prop.get_sigma ep2 in + let sigma1 = ep1.Prop.sigma in + let sigma2 = ep2.Prop.sigma in let es1 = sigma_get_start_lexps_sort sigma1 in let es2 = sigma_get_start_lexps_sort sigma2 in @@ -1787,8 +1787,8 @@ let eprop_partial_join' mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed Prop. | e1:: es1'', e2:: es2'' -> Exp.equal e1 e2 && expensive_check es1'' es2'' in let sub_common, eqs_from_sub1, eqs_from_sub2 = - let sub1 = Prop.get_sub ep1 in - let sub2 = Prop.get_sub ep2 in + let sub1 = ep1.Prop.sub in + let sub2 = ep2.Prop.sub in let sub_common, sub1_only, sub2_only = Sil.sub_symmetric_difference sub1 sub2 in let sub_common_normal, sub_common_other = let f e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in @@ -1813,13 +1813,13 @@ let eprop_partial_join' mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed Prop. | sigma_new, [], [] -> L.d_strln "sigma_partial_join succeeded"; let ep_sub = - let ep = Prop.replace_pi [] ep1 in - Prop.replace_sub sub_common ep in + let ep = Prop.set ep1 ~pi:[] in + Prop.set ep ~sub:sub_common in let p_sub_sigma = - Prop.normalize (Prop.replace_sigma sigma_new ep_sub) in + Prop.normalize (Prop.set ep_sub ~sigma:sigma_new) in let p_sub_sigma_pi = - let pi1 = (Prop.get_pi ep1) @ eqs_from_sub1 in - let pi2 = (Prop.get_pi ep2) @ eqs_from_sub2 in + let pi1 = ep1.Prop.pi @ eqs_from_sub1 in + let pi2 = ep2.Prop.pi @ eqs_from_sub2 in let pi' = pi_partial_join mode ep1 ep2 pi1 pi2 in L.d_strln "pi_partial_join succeeded"; let pi_from_fresh_vars = FreshVarExp.get_induced_pi () in @@ -1835,17 +1835,17 @@ let footprint_partial_join' (p1: Prop.normal Prop.t) (p2: Prop.normal Prop.t) : let fp1 = Prop.extract_footprint p1 in let fp2 = Prop.extract_footprint p2 in let efp = eprop_partial_join' JoinState.Pre fp1 fp2 in - let fp_pi = (* Prop.get_pure efp in *) - let fp_pi0 = Prop.get_pure efp in + let pi_fp = + let pi_fp0 = Prop.get_pure efp in let f a = Sil.fav_for_all (Sil.atom_fav a) Ident.is_footprint in - IList.filter f fp_pi0 in - let fp_sigma = (* Prop.get_sigma efp in *) - let fp_sigma0 = Prop.get_sigma efp in + IList.filter f pi_fp0 in + let sigma_fp = + let sigma_fp0 = efp.Prop.sigma in let f a = Sil.fav_exists (Sil.hpred_fav a) (fun a -> not (Ident.is_footprint a)) in - if IList.exists f fp_sigma0 then (L.d_strln "failure reason 66"; raise IList.Fail); - fp_sigma0 in - let ep1' = Prop.replace_sigma_footprint fp_sigma (Prop.replace_pi_footprint fp_pi p1) in - let ep2' = Prop.replace_sigma_footprint fp_sigma (Prop.replace_pi_footprint fp_pi p2) in + if IList.exists f sigma_fp0 then (L.d_strln "failure reason 66"; raise IList.Fail); + sigma_fp0 in + let ep1' = Prop.set p1 ~pi_fp ~sigma_fp in + let ep2' = Prop.set p2 ~pi_fp ~sigma_fp in Prop.normalize ep1', Prop.normalize ep2' end diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 135550442..a7bd46339 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -581,7 +581,9 @@ let print_kind f kind = print_stack_info:= true; | Generic_proposition -> if !print_full_prop then - F.fprintf f "\n HEAP%iL0 [label=\"HEAP %i \", style=filled, color= yellow]\n" !dotty_state_count !proposition_counter + F.fprintf f "\n HEAP%iL0 [label=\"HEAP %i \", style=filled, color= yellow]\n" + !dotty_state_count + !proposition_counter | Lambda_pred (no, lev, array) -> match array with | false -> @@ -689,12 +691,12 @@ let rec print_struct f pe e te l coo c = if !print_full_prop then F.fprintf f " node [shape=record]; \n struct%iL%i \ - [label=\"{<%s%iL%i> STRUCT: %a } | %a\" ] fontcolor=%s\n" + [label=\"{<%s%iL%i> STRUCT: %a } | %a\" ] fontcolor=%s\n" n lambda e_no_special_char n lambda (Sil.pp_exp pe) e (struct_to_dotty_str pe coo) l c else F.fprintf f " node [shape=record]; \n struct%iL%i \ - [label=\"{<%s%iL%i> OBJECT: %s } | %a\" ] fontcolor=%s\n" + [label=\"{<%s%iL%i> OBJECT: %s } | %a\" ] fontcolor=%s\n" n lambda e_no_special_char n lambda print_type (struct_to_dotty_str pe coo) l c; F.fprintf f "}\n" @@ -778,7 +780,7 @@ and dotty_pp_state f pe cycle dotnode = (* Build the graph data structure to be printed *) and build_visual_graph f pe p cycle = - let sigma = Prop.get_sigma p in + let sigma = p.Prop.sigma in compute_fields_struct sigma; compute_struct_exp_nodes sigma; (* L.out "@\n@\n Computed fields structs: "; @@ -822,15 +824,15 @@ and pp_dotty f kind (_prop: Prop.normal Prop.t) cycle = let cmap_foot = Propgraph.diff_get_colormap true diff in let pe = { (Prop.prop_update_obj_sub pe_text pre) with pe_cmap_norm = cmap_norm; pe_cmap_foot = cmap_foot } in (* add stack vars from pre *) - let pre_stack = fst (Prop.sigma_get_stack_nonstack true (Prop.get_sigma pre)) in - let prop = Prop.replace_sigma (pre_stack @ Prop.get_sigma _prop) _prop in + let pre_stack = fst (Prop.sigma_get_stack_nonstack true pre.Prop.sigma) in + let prop = Prop.set _prop ~sigma:(pre_stack @ _prop.Prop.sigma) in pe, Prop.normalize prop | _ -> let pe = Prop.prop_update_obj_sub pe_text _prop in pe, _prop in dangling_dotboxes := []; nil_dotboxes :=[]; - set_exps_neq_zero (Prop.get_pi prop); + set_exps_neq_zero prop.Prop.pi; incr dotty_state_count; F.fprintf f "\n subgraph cluster_prop_%i { color=black \n" !proposition_counter; print_kind f kind; @@ -863,10 +865,15 @@ let pp_dotty_one_spec f pre posts = pp_dotty f (Spec_precondition) pre None; invisible_arrows:= false; IList.iter (fun (po, _) -> incr post_counter ; pp_dotty f (Spec_postcondition pre) po None; - for j = 1 to 4 do - F.fprintf f " inv_%i%i%i%i -> state_pi_%i [style=invis]\n" !spec_counter j j j !target_invisible_arrow_pre; - done - ) posts; + for j = 1 to 4 do + F.fprintf f " inv_%i%i%i%i -> state_pi_%i [style=invis]\n" + !spec_counter + j + j + j + !target_invisible_arrow_pre; + done + ) posts; F.fprintf f "\n } \n" (* this is used to print a list of proposition when considered in a path of nodes *) @@ -1276,7 +1283,7 @@ let rec make_visual_heap_edges nodes sigma prop = (* from a prop generate and return visual proposition *) let prop_to_set_of_visual_heaps prop = let result = ref [] in - working_list:=[(!global_node_counter, Prop.get_sigma prop)]; + working_list := [(!global_node_counter, prop.Prop.sigma)]; incr global_node_counter; while (!working_list!=[]) do set_dangling_nodes:=[]; @@ -1381,8 +1388,8 @@ let print_specs_xml signature specs loc fmt = let do_one_spec pre posts n = let add_stack_to_prop _prop = (* add stack vars from pre *) - let pre_stack = fst (Prop.sigma_get_stack_nonstack true (Prop.get_sigma pre)) in - let _prop' = Prop.replace_sigma (pre_stack @ Prop.get_sigma _prop) _prop in + let pre_stack = fst (Prop.sigma_get_stack_nonstack true pre.Prop.sigma) in + let _prop' = Prop.set _prop ~sigma:(pre_stack @ _prop.Prop.sigma) in Prop.normalize _prop' in let jj = ref 0 in let xml_pre = prop_to_xml pre "precondition" !jj in diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index f8c22c62a..3edc774f6 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -482,7 +482,7 @@ let find_typ_without_ptr prop pvar = | Sil.Hpointsto (e, _, te) when Exp.equal e (Exp.Lvar pvar) -> res := Some te | _ -> () in - IList.iter do_hpred (Prop.get_sigma prop); + IList.iter do_hpred prop.Prop.sigma; !res (** Produce a description of a leak by looking at the current state. @@ -641,7 +641,7 @@ let vpath_find prop _exp : DExp.t option * Typ.t option = let filter = function | (ni, Exp.Var id') -> Ident.is_normal ni && Ident.equal id' id | _ -> false in - IList.exists filter (Sil.sub_to_list (Prop.get_sub prop)) in + IList.exists filter (Sil.sub_to_list prop.Prop.sub) in function | Sil.Hpointsto (Exp.Lvar pv, sexp, texp) when (Pvar.is_local pv || Pvar.is_global pv || Pvar.is_seed pv) -> @@ -657,7 +657,7 @@ let vpath_find prop _exp : DExp.t option * Typ.t option = (match do_hpred sigma_acc sigma_todo' hpred with | Some de, typo -> Some de, typo | None, _ -> find (hpred:: sigma_acc) sigma_todo' exp) in - let res = find [] (Prop.get_sigma prop) _exp in + let res = find [] prop.Prop.sigma _exp in if verbose then begin match res with | None, _ -> L.d_str "vpath_find: cannot find "; Sil.d_exp _exp; L.d_ln () @@ -672,7 +672,7 @@ let vpath_find prop _exp : DExp.t option * Typ.t option = (** produce a description of the access from the instrumentation at position [dexp] in [prop] *) let explain_dexp_access prop dexp is_nullable = - let sigma = Prop.get_sigma prop in + let sigma = prop.Prop.sigma in let sexpo_to_inst = function | None -> None | Some (Sil.Eexp (_, inst)) -> Some inst @@ -1017,9 +1017,9 @@ let find_with_exp prop exp = let do_hpred = function | Sil.Hpointsto(Exp.Lvar pv, Sil.Eexp (e, _), _) -> if Exp.equal e exp then found_in_pvar pv - else IList.iter (do_hpred_pointed_by_pvar pv e) (Prop.get_sigma prop) + else IList.iter (do_hpred_pointed_by_pvar pv e) prop.Prop.sigma | _ -> () in - IList.iter do_hpred (Prop.get_sigma prop); + IList.iter do_hpred prop.Prop.sigma; !res (** return a description explaining value [exp] in [prop] in terms of a source expression diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 5a3d7ad2a..f782683fb 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -281,8 +281,8 @@ let propagate_nodes_divergence let prop_incons = let mk_incons prop = let p_abs = Abs.abstract pname tenv prop in - let p_zero = Prop.replace_sigma [] (Prop.replace_sub Sil.sub_empty p_abs) in - Prop.normalize (Prop.replace_pi [Sil.Aneq (Exp.zero, Exp.zero)] p_zero) in + let p_zero = Prop.set p_abs ~sub:Sil.sub_empty ~sigma:[] in + Prop.normalize (Prop.set p_zero ~pi:[Sil.Aneq (Exp.zero, Exp.zero)]) in Paths.PathSet.map mk_incons diverging_states in (L.d_strln_color Orange) "Propagating Divergence -- diverging states:"; Propgraph.d_proplist Prop.prop_emp (Paths.PathSet.to_proplist prop_incons); L.d_ln (); @@ -728,7 +728,7 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list = let pre' = Prop.normalize (Prop.prop_sub sub pre) in if !Config.curr_language = Config.Java && Cfg.Procdesc.get_access pdesc <> PredSymb.Private then - report_context_leaks pname (Prop.get_sigma post) tenv; + report_context_leaks pname post.Prop.sigma tenv; let post' = if Prover.check_inconsistency_base prop then None else Some (Prop.normalize (Prop.prop_sub sub post), path) in @@ -827,15 +827,13 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr let sigma_seed = create_seed_vars (* formals already there plus new ones *) - (Prop.get_sigma prop @ sigma_new_formals) in + (prop.Prop.sigma @ sigma_new_formals) in let sigma = sigma_seed @ sigma_new_formals in let new_pi = - Prop.get_pi prop in + prop.Prop.pi in let prop' = - Prop.replace_pi new_pi (Prop.prop_sigma_star prop sigma) in - Prop.replace_sigma_footprint - (Prop.get_sigma_footprint prop' @ sigma_new_formals) - prop' + Prop.set (Prop.prop_sigma_star prop sigma) ~pi:new_pi in + Prop.set prop' ~sigma_fp:(prop'.Prop.sigma_fp @ sigma_new_formals) (** Construct an initial prop by extending [prop] with locals, and formals if [add_formals] is true as well as seed variables *) @@ -871,9 +869,7 @@ let initial_prop_from_pre tenv curr_f pre = let sub = Sil.sub_of_list sub_list in let pre2 = Prop.prop_sub sub pre in let pre3 = - Prop.replace_sigma_footprint - (Prop.get_sigma pre2) - (Prop.replace_pi_footprint (Prop.get_pure pre2) pre2) in + Prop.set pre2 ~pi_fp:(Prop.get_pure pre2) ~sigma_fp:pre2.Prop.sigma in initial_prop tenv curr_f pre3 false else initial_prop tenv curr_f pre false @@ -1122,14 +1118,13 @@ let remove_this_not_null prop = | Sil.Aneq (Exp.Var v, e) when Ident.equal v var && Exp.equal e Exp.null -> atoms | a -> a:: atoms in - match IList.fold_left collect_hpred (None, []) (Prop.get_sigma prop) with + match IList.fold_left collect_hpred (None, []) prop.Prop.sigma with | None, _ -> prop | Some var, filtered_hpreds -> let filtered_atoms = - IList.fold_left (collect_atom var) [] (Prop.get_pi prop) in - let prop' = Prop.replace_pi filtered_atoms Prop.prop_emp in - let prop'' = Prop.replace_sigma filtered_hpreds prop' in - Prop.normalize prop'' + IList.fold_left (collect_atom var) [] prop.Prop.pi in + let prop' = Prop.set Prop.prop_emp ~pi:filtered_atoms ~sigma:filtered_hpreds in + Prop.normalize prop' (** Is true when the precondition does not contain constrains that can be false at call site. diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index 4f76217b4..3edb8e075 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/modelBuiltins.ml @@ -64,7 +64,7 @@ let add_array_to_prop pdesc prop_ lexp typ = try let hpred = IList.find (function | Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp - | _ -> false) (Prop.get_sigma prop) in + | _ -> false) prop.Prop.sigma in match hpred with | Sil.Hpointsto(_, Sil.Earray (len, _, _), _) -> Some (len, prop) @@ -75,10 +75,10 @@ let add_array_to_prop pdesc prop_ lexp typ = let len = Exp.Var (Ident.create_fresh Ident.kfootprint) in let s = mk_empty_array_rearranged len in let hpred = Prop.mk_ptsto n_lexp s (Exp.Sizeof (arr_typ, Some len, Subtype.exact)) in - let sigma = Prop.get_sigma prop in - let sigma_fp = Prop.get_sigma_footprint prop in - let prop'= Prop.replace_sigma (hpred:: sigma) prop in - let prop''= Prop.replace_sigma_footprint (hpred:: sigma_fp) prop' in + let sigma = prop.Prop.sigma in + let sigma_fp = prop.Prop.sigma_fp in + let prop'= Prop.set prop ~sigma:(hpred:: sigma) in + let prop''= Prop.set prop' ~sigma_fp:(hpred:: sigma_fp) in let prop''= Prop.normalize prop'' in Some (len, prop'') | _ -> None @@ -115,11 +115,11 @@ let execute___set_array_length { Builtin.pdesc; prop_; path; ret_ids; args; } let n_len, prop = check_arith_norm_exp pname len prop__ in let hpred, sigma' = IList.partition (function | Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp - | _ -> false) (Prop.get_sigma prop) in + | _ -> false) prop.Prop.sigma in (match hpred with | [Sil.Hpointsto(e, Sil.Earray(_, esel, inst), t)] -> let hpred' = Sil.Hpointsto (e, Sil.Earray (n_len, esel, inst), t) in - let prop' = Prop.replace_sigma (hpred':: sigma') prop in + let prop' = Prop.set prop ~sigma:(hpred':: sigma') in [(Prop.normalize prop', path)] | _ -> [] (* by construction of prop_a this case is impossible *) )) | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -147,7 +147,7 @@ let create_type tenv n_lexp typ prop = try let _ = IList.find (function | Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp - | _ -> false) (Prop.get_sigma prop) in + | _ -> false) prop.Prop.sigma in prop with Not_found -> let mhpred = @@ -167,15 +167,15 @@ let create_type tenv n_lexp typ prop = | _ -> None in match mhpred with | Some hpred -> - let sigma = Prop.get_sigma prop in - let sigma_fp = Prop.get_sigma_footprint prop in - let prop'= Prop.replace_sigma (hpred:: sigma) prop in + let sigma = prop.Prop.sigma in + let sigma_fp = prop.Prop.sigma_fp in + let prop'= Prop.set prop ~sigma:(hpred:: sigma) in let prop''= let has_normal_variables = Sil.fav_exists (Sil.exp_fav n_lexp) Ident.is_normal in if (is_undefined_opt prop n_lexp) || has_normal_variables then prop' - else Prop.replace_sigma_footprint (hpred:: sigma_fp) prop' in + else Prop.set prop' ~sigma_fp:(hpred:: sigma_fp) in let prop''= Prop.normalize prop'' in prop'' | None -> prop in @@ -201,7 +201,7 @@ let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_ids; args; } try let hpred = IList.find (function | Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp - | _ -> false) (Prop.get_sigma prop) in + | _ -> false) prop.Prop.sigma in match hpred with | Sil.Hpointsto(_, _, texp) -> (return_result texp prop ret_ids), path @@ -221,10 +221,10 @@ let replace_ptsto_texp prop root_e texp = match sigma1 with | [Sil.Hpointsto(e, se, _)] -> (Sil.Hpointsto (e, se, texp)) :: sigma2 | _ -> sigma in - let sigma = Prop.get_sigma prop in - let sigma_fp = Prop.get_sigma_footprint prop in - let prop'= Prop.replace_sigma (process_sigma sigma) prop in - let prop''= Prop.replace_sigma_footprint (process_sigma sigma_fp) prop' in + let sigma = prop.Prop.sigma in + let sigma_fp = prop.Prop.sigma_fp in + let prop'= Prop.set prop ~sigma:(process_sigma sigma) in + let prop''= Prop.set prop' ~sigma_fp:(process_sigma sigma_fp) in Prop.normalize prop'' let execute___instanceof_cast ~instof @@ -254,7 +254,7 @@ let execute___instanceof_cast ~instof try let hpred = IList.find (function | Sil.Hpointsto (e1, _, _) -> Exp.equal e1 val1 - | _ -> false) (Prop.get_sigma prop) in + | _ -> false) prop.Prop.sigma in match hpred with | Sil.Hpointsto (_, _, texp1) -> let pos_type_opt, neg_type_opt = @@ -410,9 +410,9 @@ let execute___get_hidden_field { Builtin.pdesc; prop_; path; ret_ids; args; } set_ret_val(); hpred | _ -> hpred in - let sigma' = IList.map (do_hpred false) (Prop.get_sigma prop) in - let sigma_fp' = IList.map (do_hpred true) (Prop.get_sigma_footprint prop) in - let prop' = Prop.replace_sigma_footprint sigma_fp' (Prop.replace_sigma sigma' prop) in + let sigma' = IList.map (do_hpred false) prop.Prop.sigma in + let sigma_fp' = IList.map (do_hpred true) prop.Prop.sigma_fp in + let prop' = Prop.set prop ~sigma:sigma' ~sigma_fp:sigma_fp' in let prop'' = return_val (Prop.normalize prop') in [(prop'', path)] | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -444,9 +444,9 @@ let execute___set_hidden_field { Builtin.pdesc; prop_; path; args; } let fsel' = (Ident.fieldname_hidden, se) :: fsel in Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp) | _ -> hpred in - let sigma' = IList.map (do_hpred false) (Prop.get_sigma prop) in - let sigma_fp' = IList.map (do_hpred true) (Prop.get_sigma_footprint prop) in - let prop' = Prop.replace_sigma_footprint sigma_fp' (Prop.replace_sigma sigma' prop) in + let sigma' = IList.map (do_hpred false) prop.Prop.sigma in + let sigma_fp' = IList.map (do_hpred true) prop.Prop.sigma_fp in + let prop' = Prop.set prop ~sigma:sigma' ~sigma_fp:sigma_fp' in let prop'' = Prop.normalize prop' in [(prop'', path)] | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -563,7 +563,7 @@ let execute___release_autorelease_pool (try let hpred = IList.find (function | Sil.Hpointsto(e1, _, _) -> Exp.equal e1 exp - | _ -> false) (Prop.get_sigma prop_) in + | _ -> false) prop_.Prop.sigma in match hpred with | Sil.Hpointsto (_, _, Exp.Sizeof (typ, _, _)) -> let res1 = @@ -662,7 +662,7 @@ let execute___objc_cast { Builtin.pdesc; prop_; path; ret_ids; args; } (try let hpred = IList.find (function | Sil.Hpointsto(e1, _, _) -> Exp.equal e1 val1 - | _ -> false) (Prop.get_sigma prop) in + | _ -> false) prop.Prop.sigma in match hpred, texp2 with | Sil.Hpointsto (val1, _, _), Exp.Sizeof _ -> let prop' = replace_ptsto_texp prop val1 texp2 in @@ -816,7 +816,7 @@ let execute___cxx_typeid ({ Builtin.pdesc; tenv; prop_; args; loc} as r) try let hpred = IList.find (function | Sil.Hpointsto (e, _, _) -> Exp.equal e n_lexp - | _ -> false) (Prop.get_sigma prop) in + | _ -> false) prop.Prop.sigma in match hpred with | Sil.Hpointsto (_, _, Exp.Sizeof (dynamic_type, _, _)) -> dynamic_type | _ -> typ diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 310b1cf8d..136fba4ba 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -42,15 +42,15 @@ module Core : sig sigma: sigma; (** spatial part *) sub: Sil.subst; (** substitution *) pi: pi; (** pure part *) - foot_sigma : sigma; (** abduced spatial part *) - foot_pi: pi; (** abduced pure part *) + sigma_fp : sigma; (** abduced spatial part *) + pi_fp: pi; (** abduced pure part *) } (** Proposition [true /\ emp]. *) val prop_emp : normal t (** Set individual fields of the prop. *) - val set : ?sub:Sil.subst -> ?pi:pi -> ?sigma:sigma -> ?foot_pi:pi -> ?foot_sigma:sigma -> + val set : ?sub:Sil.subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma -> 'a t -> exposed t (** Cast an exposed prop to a normalized one by just changing the type *) @@ -70,8 +70,8 @@ end = struct sigma: sigma; (** spatial part *) sub: Sil.subst; (** substitution *) pi: pi; (** pure part *) - foot_sigma : sigma; (** abduced spatial part *) - foot_pi: pi; (** abduced pure part *) + sigma_fp : sigma; (** abduced spatial part *) + pi_fp: pi; (** abduced pure part *) } (** Proposition [true /\ emp]. *) @@ -80,17 +80,17 @@ end = struct sub = Sil.sub_empty; pi = []; sigma = []; - foot_pi = []; - foot_sigma = []; + pi_fp = []; + sigma_fp = []; } - let set ?sub ?pi ?sigma ?foot_pi ?foot_sigma p = + let set ?sub ?pi ?sigma ?pi_fp ?sigma_fp p = let set_ p - ?(sub=p.sub) ?(pi=p.pi) ?(sigma=p.sigma) ?(foot_pi=p.foot_pi) ?(foot_sigma=p.foot_sigma) () + ?(sub=p.sub) ?(pi=p.pi) ?(sigma=p.sigma) ?(pi_fp=p.pi_fp) ?(sigma_fp=p.sigma_fp) () = - { sub; pi; sigma; foot_pi; foot_sigma } + { sub; pi; sigma; pi_fp; sigma_fp } in - set_ p ?sub ?pi ?sigma ?foot_pi ?foot_sigma () + set_ p ?sub ?pi ?sigma ?pi_fp ?sigma_fp () let unsafe_cast_to_normal (p: exposed t) : normal t = (p :> normal t) @@ -140,8 +140,8 @@ let prop_compare p1 p2 = sigma_compare p1.sigma p2.sigma |> next Sil.sub_compare p1.sub p2.sub |> next pi_compare p1.pi p2.pi - |> next sigma_compare p1.foot_sigma p2.foot_sigma - |> next pi_compare p1.foot_pi p2.foot_pi + |> next sigma_compare p1.sigma_fp p2.sigma_fp + |> next pi_compare p1.pi_fp p2.pi_fp (** Check the equality of two propositions *) let prop_equal p1 p2 = @@ -153,11 +153,11 @@ let prop_equal p1 p2 = let pp_footprint _pe f fp = let pe = { _pe with pe_cmap_norm = _pe.pe_cmap_foot } in let pp_pi f () = - if fp.foot_pi != [] then - F.fprintf f "%a ;@\n" (pp_semicolon_seq_oneline pe (Sil.pp_atom pe)) fp.foot_pi in - if fp.foot_pi != [] || fp.foot_sigma != [] then + if fp.pi_fp != [] then + F.fprintf f "%a ;@\n" (pp_semicolon_seq_oneline pe (Sil.pp_atom pe)) fp.pi_fp in + if fp.pi_fp != [] || fp.sigma_fp != [] then F.fprintf f "@\n[footprint@\n @[%a%a@] ]" - pp_pi () (pp_semicolon_seq pe (Sil.pp_hpred pe)) fp.foot_sigma + pp_pi () (pp_semicolon_seq pe (Sil.pp_hpred pe)) fp.sigma_fp let pp_texp_simple pe = match pe.pe_opt with | PP_SIM_DEFAULT -> Sil.pp_texp pe @@ -251,12 +251,6 @@ let d_pi_sigma pi sigma = let d_separator () = if pi != [] && sigma != [] then L.d_strln " *" in d_pi pi; d_separator (); d_sigma sigma -(** Return the sub part of [prop]. *) -let get_sub (p: 'a t) : Sil.subst = p.sub - -(** Return the pi part of [prop]. *) -let get_pi (p: 'a t) : pi = p.pi - let pi_of_subst sub = IList.map (fun (id1, e2) -> Sil.Aeq (Exp.Var id1, e2)) (Sil.sub_to_list sub) @@ -325,16 +319,16 @@ let pp_footprint_simple _pe env f fp = let pp_pure f pi = if pi != [] then F.fprintf f "%a *@\n" (pp_pi pe) pi in - if fp.foot_pi != [] || fp.foot_sigma != [] then + if fp.pi_fp != [] || fp.sigma_fp != [] then F.fprintf f "@\n[footprint@\n @[%a%a@] ]" - pp_pure fp.foot_pi - (pp_sigma_simple pe env) fp.foot_sigma + pp_pure fp.pi_fp + (pp_sigma_simple pe env) fp.sigma_fp (** Create a predicate environment for a prop *) let prop_pred_env prop = let env = Sil.Predicates.empty_env () in IList.iter (Sil.Predicates.process_hpred env) prop.sigma; - IList.iter (Sil.Predicates.process_hpred env) prop.foot_sigma; + IList.iter (Sil.Predicates.process_hpred env) prop.sigma_fp; env (** Pretty print a proposition. *) @@ -342,9 +336,9 @@ let pp_prop pe0 f prop = let pe = prop_update_obj_sub pe0 prop in let latex = pe.pe_kind == PP_LATEX in let do_print f () = - let subl = Sil.sub_to_list (get_sub prop) in + let subl = Sil.sub_to_list prop.sub in (* since prop diff is based on physical equality, we need to extract the sub verbatim *) - let pi = get_pi prop in + let pi = prop.pi in let pp_pure f () = if subl != [] then F.fprintf f "%a ;@\n" (pp_subl pe) subl; if pi != [] then F.fprintf f "%a ;@\n" (pp_pi pe) pi in @@ -413,8 +407,8 @@ let sigma_fav = Sil.fav_imperative_to_functional sigma_fav_add let prop_footprint_fav_add fav prop = - sigma_fav_add fav prop.foot_sigma; - pi_fav_add fav prop.foot_pi + sigma_fav_add fav prop.sigma_fp; + pi_fav_add fav prop.pi_fp (** Find fav of the footprint part of the prop *) let prop_footprint_fav prop = @@ -422,10 +416,10 @@ let prop_footprint_fav prop = let prop_fav_add fav prop = sigma_fav_add fav prop.sigma; - sigma_fav_add fav prop.foot_sigma; + sigma_fav_add fav prop.sigma_fp; Sil.sub_fav_add fav prop.sub; pi_fav_add fav prop.pi; - pi_fav_add fav prop.foot_pi + pi_fav_add fav prop.pi_fp let prop_fav p = Sil.fav_imperative_to_functional prop_fav_add p @@ -433,7 +427,7 @@ let prop_fav p = (** free vars of the prop, excluding the pure part *) let prop_fav_nonpure_add fav prop = sigma_fav_add fav prop.sigma; - sigma_fav_add fav prop.foot_sigma + sigma_fav_add fav prop.sigma_fp (** free vars, except pi and sub, of current and footprint parts *) let prop_fav_nonpure = @@ -455,8 +449,8 @@ let pi_fpv pi = let prop_fpv prop = (Sil.sub_fpv prop.sub) @ (pi_fpv prop.pi) @ - (pi_fpv prop.foot_pi) @ - (sigma_fpv prop.foot_sigma) @ + (pi_fpv prop.pi_fp) @ + (sigma_fpv prop.sigma_fp) @ (sigma_fpv prop.sigma) (** {2 Functions for Subsitition} *) @@ -1383,8 +1377,8 @@ let sigma_normalize sub sigma = (** normalize the footprint part, and rename any primed vars in the footprint with fresh footprint vars *) let footprint_normalize prop = - let nsigma = sigma_normalize Sil.sub_empty prop.foot_sigma in - let npi = pi_normalize Sil.sub_empty nsigma prop.foot_pi in + let nsigma = sigma_normalize Sil.sub_empty prop.sigma_fp in + let npi = pi_normalize Sil.sub_empty nsigma prop.pi_fp in let fp_vars = let fav = pi_fav npi in sigma_fav_add fav nsigma; @@ -1409,7 +1403,7 @@ let footprint_normalize prop = let nsigma' = sigma_normalize Sil.sub_empty (sigma_sub ren_sub nsigma) in let npi' = pi_normalize Sil.sub_empty nsigma' (pi_sub ren_sub npi) in (npi', nsigma') in - set prop ~foot_pi:npi' ~foot_sigma:nsigma' + set prop ~pi_fp:npi' ~sigma_fp:nsigma' let exp_normalize_prop prop exp = Config.run_with_abs_val_equal_zero (exp_normalize prop.sub) exp @@ -1470,18 +1464,6 @@ let prop_compact sh (prop : normal t) : normal t = (** {2 Function for replacing occurrences of expressions.} *) -let replace_pi pi prop: exposed t = - set prop ~pi - -let replace_sigma sigma prop : exposed t = - set prop ~sigma - -let replace_sigma_footprint foot_sigma prop : exposed t = - set prop ~foot_sigma - -let replace_pi_footprint foot_pi prop : exposed t = - set prop ~foot_pi - let sigma_replace_exp epairs sigma = let sigma' = IList.map (Sil.hpred_replace_exp epairs) sigma in sigma_normalize Sil.sub_empty sigma' @@ -1763,13 +1745,13 @@ let rec prop_atom_and ?(footprint=false) (p : normal t) a : normal t = match a' with | Sil.Aeq (Exp.Var i, e) when not (Sil.ident_in_exp i e) -> let mysub = Sil.sub_of_list [(i, e)] in - let foot_sigma' = sigma_normalize mysub p'.foot_sigma in - let foot_pi' = a' :: pi_normalize mysub foot_sigma' p'.foot_pi in + let sigma_fp' = sigma_normalize mysub p'.sigma_fp in + let pi_fp' = a' :: pi_normalize mysub sigma_fp' p'.pi_fp in footprint_normalize - (set p' ~foot_pi:foot_pi' ~foot_sigma:foot_sigma') + (set p' ~pi_fp:pi_fp' ~sigma_fp:sigma_fp') | _ -> footprint_normalize - (set p' ~foot_pi:(a' :: p'.foot_pi)) in + (set p' ~pi_fp:(a' :: p'.pi_fp)) in if predicate_warning then (L.d_warning "dropping non-footprint "; Sil.d_atom a'; L.d_ln ()); unsafe_cast_to_normal p'' end @@ -1783,22 +1765,11 @@ let conjoin_eq ?(footprint = false) exp1 exp2 prop = let conjoin_neq ?(footprint = false) exp1 exp2 prop = prop_atom_and ~footprint prop (Sil.Aneq (exp1, exp2)) -(** Return the spatial part *) -let get_sigma (p: 'a t) : sigma = p.sigma - -(** Return the pure part of the footprint *) -let get_pi_footprint p = - p.foot_pi - -(** Return the spatial part of the footprint *) -let get_sigma_footprint p = - p.foot_sigma - (** Reset every inst in the prop using the given map *) let prop_reset_inst inst_map prop = - let sigma' = IList.map (Sil.hpred_instmap inst_map) (get_sigma prop) in - let sigma_fp' = IList.map (Sil.hpred_instmap inst_map) (get_sigma_footprint prop) in - replace_sigma_footprint sigma_fp' (replace_sigma sigma' prop) + let sigma' = IList.map (Sil.hpred_instmap inst_map) prop.sigma in + let sigma_fp' = IList.map (Sil.hpred_instmap inst_map) prop.sigma_fp in + set prop ~sigma:sigma' ~sigma_fp:sigma_fp' (** {1 Functions for transforming footprints into propositions.} *) @@ -1809,12 +1780,12 @@ let prop_reset_inst inst_map prop = (** Extract the footprint and return it as a prop *) let extract_footprint p = - set prop_emp ~pi:p.foot_pi ~sigma:p.foot_sigma + set prop_emp ~pi:p.pi_fp ~sigma:p.sigma_fp (** Extract the (footprint,current) pair *) let extract_spec (p : normal t) : normal t * normal t = let pre = extract_footprint p in - let post = set p ~foot_pi:[] ~foot_sigma:[] in + let post = set p ~pi_fp:[] ~sigma_fp:[] in (unsafe_cast_to_normal pre, unsafe_cast_to_normal post) (** [prop_set_fooprint p p_foot] sets proposition [p_foot] as footprint of [p]. *) @@ -1823,7 +1794,7 @@ let prop_set_footprint p p_foot = (IList.map (fun (i, e) -> Sil.Aeq(Exp.Var i, e)) (Sil.sub_to_list p_foot.sub)) @ p_foot.pi in - set p ~foot_pi:pi ~foot_sigma:p_foot.sigma + set p ~pi_fp:pi ~sigma_fp:p_foot.sigma (** {2 Functions for renaming primed variables by "canonical names"} *) @@ -1901,11 +1872,11 @@ let sigma_dfs_sort sigma = sigma' let prop_dfs_sort p = - let sigma = get_sigma p in + let sigma = p.sigma in let sigma' = sigma_dfs_sort sigma in - let sigma_fp = get_sigma_footprint p in + let sigma_fp = p.sigma_fp in let sigma_fp' = sigma_dfs_sort sigma_fp in - let p' = set p ~sigma:sigma' ~foot_sigma:sigma_fp' in + let p' = set p ~sigma:sigma' ~sigma_fp:sigma_fp' in (* L.err "@[<2>P SORTED:@\n%a@\n@." pp_prop p'; *) p' @@ -2145,8 +2116,8 @@ let prop_rename_primed_footprint_vars (p : normal t) : normal t = let sub' = sub_captured_ren ren p.sub in let pi' = pi_captured_ren ren p.pi in let sigma' = sigma_captured_ren ren p.sigma in - let foot_pi' = pi_captured_ren ren p.foot_pi in - let foot_sigma' = sigma_captured_ren ren p.foot_sigma in + let pi_fp' = pi_captured_ren ren p.pi_fp in + let sigma_fp' = sigma_captured_ren ren p.sigma_fp in let sub_for_normalize = Sil.sub_empty in (* It is fine to use the empty substituion during normalization @@ -2155,7 +2126,7 @@ let prop_rename_primed_footprint_vars (p : normal t) : normal t = let nsigma' = sigma_normalize sub_for_normalize sigma' in let npi' = pi_normalize sub_for_normalize nsigma' pi' in let p' = footprint_normalize - (set prop_emp ~sub:nsub' ~pi:npi' ~sigma:nsigma' ~foot_pi:foot_pi' ~foot_sigma:foot_sigma') in + (set prop_emp ~sub:nsub' ~pi:npi' ~sigma:nsigma' ~pi_fp:pi_fp' ~sigma_fp:sigma_fp') in unsafe_cast_to_normal p' (** {2 Functions for changing and generating propositions} *) @@ -2172,15 +2143,15 @@ let normalize (eprop : 'a t) : normal t = (set prop_emp ~sigma: (sigma_normalize Sil.sub_empty eprop.sigma)) in let nprop = IList.fold_left prop_atom_and p0 (get_pure eprop) in unsafe_cast_to_normal - (footprint_normalize (set nprop ~foot_pi:eprop.foot_pi ~foot_sigma:eprop.foot_sigma)) + (footprint_normalize (set nprop ~pi_fp:eprop.pi_fp ~sigma_fp:eprop.sigma_fp)) (** Apply subsitution to prop. *) let prop_sub subst (prop: 'a t) : exposed t = let pi = pi_sub subst (prop.pi @ pi_of_subst prop.sub) in let sigma = sigma_sub subst prop.sigma in - let foot_pi = pi_sub subst prop.foot_pi in - let foot_sigma = sigma_sub subst prop.foot_sigma in - set prop_emp ~pi ~sigma ~foot_pi ~foot_sigma + let pi_fp = pi_sub subst prop.pi_fp in + let sigma_fp = sigma_sub subst prop.sigma_fp in + set prop_emp ~pi ~sigma ~pi_fp ~sigma_fp (** Apply renaming substitution to a proposition. *) let prop_ren_sub (ren_sub: Sil.subst) (prop: normal t) : normal t = @@ -2212,9 +2183,9 @@ let prop_expmap (fe: Exp.t -> Exp.t) prop = let f (e, sil_opt) = (fe e, sil_opt) in let pi = IList.map (Sil.atom_expmap fe) prop.pi in let sigma = IList.map (Sil.hpred_expmap f) prop.sigma in - let foot_pi = IList.map (Sil.atom_expmap fe) prop.foot_pi in - let foot_sigma = IList.map (Sil.hpred_expmap f) prop.foot_sigma in - set prop ~pi ~sigma ~foot_pi ~foot_sigma + let pi_fp = IList.map (Sil.atom_expmap fe) prop.pi_fp in + let sigma_fp = IList.map (Sil.hpred_expmap f) prop.sigma_fp in + set prop ~pi ~sigma ~pi_fp ~sigma_fp (** convert identifiers in fav to kind [k] *) let vars_make_unprimed fav prop = @@ -2243,9 +2214,6 @@ let from_pi pi = let from_sigma sigma = set prop_emp ~sigma -let replace_sub sub prop = - set prop ~sub - (** Rename free variables in a prop replacing them with existentially quantified vars *) let prop_rename_fav_with_existentials (p : normal t) : normal t = let fav = Sil.fav_new () in @@ -2269,8 +2237,8 @@ type 'a prop_iter = pit_curr : Sil.hpred; (** current element *) pit_state : 'a; (** state of current element *) pit_new : sigma; (** sigma not yet visited *) - pit_foot_pi : pi; (** pure part of the footprint *) - pit_foot_sigma : sigma; (** sigma part of the footprint *) + pit_pi_fp : pi; (** pure part of the footprint *) + pit_sigma_fp : sigma; (** sigma part of the footprint *) } let prop_iter_create prop = @@ -2283,8 +2251,8 @@ let prop_iter_create prop = pit_curr = hpred; pit_state = (); pit_new = sigma'; - pit_foot_pi = prop.foot_pi; - pit_foot_sigma = prop.foot_sigma } + pit_pi_fp = prop.pi_fp; + pit_sigma_fp = prop.sigma_fp } | _ -> None (** Return the prop associated to the iterator. *) @@ -2296,8 +2264,8 @@ let prop_iter_to_prop iter = ~sub:iter.pit_sub ~pi:iter.pit_pi ~sigma:sigma - ~foot_pi:iter.pit_foot_pi - ~foot_sigma:iter.pit_foot_sigma) in + ~pi_fp:iter.pit_pi_fp + ~sigma_fp:iter.pit_sigma_fp) in IList.fold_left (fun p (footprint, atom) -> prop_atom_and ~footprint: footprint p atom) prop iter.pit_newpi @@ -2318,8 +2286,8 @@ let prop_iter_remove_curr_then_to_prop iter : normal t = ~sub:iter.pit_sub ~pi:iter.pit_pi ~sigma:normalized_sigma - ~foot_pi:iter.pit_foot_pi - ~foot_sigma:iter.pit_foot_sigma in + ~pi_fp:iter.pit_pi_fp + ~sigma_fp:iter.pit_sigma_fp in unsafe_cast_to_normal prop (** Return the current hpred and state. *) @@ -2444,8 +2412,8 @@ let prop_iter_make_id_primed id iter = pit_new = sigma_sub sub_use iter.pit_new } let prop_iter_footprint_fav_add fav iter = - sigma_fav_add fav iter.pit_foot_sigma; - pi_fav_add fav iter.pit_foot_pi + sigma_fav_add fav iter.pit_sigma_fp; + pi_fav_add fav iter.pit_pi_fp (** Find fav of the footprint part of the iterator *) let prop_iter_footprint_fav iter = @@ -2473,11 +2441,11 @@ let prop_iter_noncurr_fav_add fav iter = (** Extract the sigma part of the footprint *) let prop_iter_get_footprint_sigma iter = - iter.pit_foot_sigma + iter.pit_sigma_fp (** Replace the sigma part of the footprint *) let prop_iter_replace_footprint_sigma iter sigma = - { iter with pit_foot_sigma = sigma } + { iter with pit_sigma_fp = sigma } let prop_iter_noncurr_fav iter = Sil.fav_imperative_to_functional prop_iter_noncurr_fav_add iter @@ -2617,14 +2585,14 @@ end = struct complexity *) let prop_size p = let size_current = sigma_size p.sigma in - let size_footprint = sigma_size p.foot_sigma in + let size_footprint = sigma_size p.sigma_fp in max size_current size_footprint (** Approximate the size of the longest chain by counting the max number of |-> with the same type and whose lhs is primed or footprint *) let prop_chain_size p = - let fp_size = pi_size p.foot_pi + sigma_size p.foot_sigma in + let fp_size = pi_size p.pi_fp + sigma_size p.sigma_fp in pi_size p.pi + sigma_size p.sigma + fp_size end (*** END of module Metrics ***) @@ -2673,7 +2641,7 @@ module CategorizePreconditions = struct pi = [] in let check_sigma sigma = IList.for_all hpred_filter sigma in - check_pi (get_pi pre) && check_sigma (get_sigma pre) in + check_pi pre.pi && check_sigma pre.sigma in let pres_no_constraints = IList.filter (check_pre hpred_is_var) preconditions in let pres_only_allocation = IList.filter (check_pre hpred_only_allocation) preconditions in match preconditions, pres_no_constraints, pres_only_allocation with @@ -2686,57 +2654,3 @@ module CategorizePreconditions = struct | _:: _, [], [] -> DataConstraints end - -(* -let pp_lseg_kind f = function - | Sil.Lseg_NE -> F.fprintf f "ne" - | Sil.Lseg_PE -> F.fprintf f "" - -let pi_av_add fav pi = - IList.iter (Sil.atom_av_add fav) pi - -let sigma_av_add fav sigma = - IList.iter (Sil.hpred_av_add fav) sigma - -let prop_av_add fav prop = - Sil.sub_av_add fav prop.sub; - pi_av_add fav prop.pi; - sigma_av_add fav prop.sigma; - pi_av_add fav prop.foot_pi; - sigma_av_add fav prop.foot_sigma - -let prop_av = - Sil.fav_imperative_to_functional prop_av_add - -let rec remove_duplicates_from_sorted special_equal = function - | [] -> [] - | [x] -> [x] - | x:: y:: l -> - if (special_equal x y) - then remove_duplicates_from_sorted special_equal (y:: l) - else x:: (remove_duplicates_from_sorted special_equal (y:: l)) - -(** Replace the sub part of [prop]. *) -let prop_replace_sub sub p = - let nsub = sub_normalize sub in - { p with sub = nsub } - -let unstructured_type = function - | Typ.Tstruct _ | Typ.Tarray _ -> false - | _ -> true - -let rec pp_ren pe f = function - | [] -> () - | [(i, x)] -> F.fprintf f "%a->%a" (Ident.pp pe) i (Ident.pp pe) x - | (i, x):: ren -> F.fprintf f "%a->%a, %a" (Ident.pp pe) i (Ident.pp pe) x (pp_ren pe) ren - -let id_exp_compare (id1, e1) (id2, e2) = - let n = Exp.compare e1 e2 in - if n <> 0 then n - else Ident.compare id1 id2 - -(** Raise an exception if the prop is not normalized *) -let check_prop_normalized prop = - let sigma' = sigma_normalize_prop prop prop.sigma in - if sigma_equal prop.sigma sigma' == false then assert false -*) diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index b69f7f1e3..5f48c5c5c 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -23,7 +23,15 @@ type exposed (** kind for exposed props *) type pi = Sil.atom list type sigma = Sil.hpred list -type 'a t (** the kind 'a should range over [normal] and [exposed] *) +(** the kind 'a should range over [normal] and [exposed] *) +type 'a t = private + { + sigma: sigma; (** spatial part *) + sub: Sil.subst; (** substitution *) + pi: pi; (** pure part *) + sigma_fp : sigma; (** abduced spatial part *) + pi_fp: pi; (** abduced pure part *) + } (** type to describe different strategies for initializing fields of a structure. [No_init] does not initialize any fields of the struct. [Fld_init] initializes the fields of the struct with fresh @@ -266,24 +274,9 @@ val conjoin_eq : ?footprint: bool -> Exp.t -> Exp.t -> normal t -> normal t (** Conjoin [exp1]!=[exp2] with a symbolic heap [prop]. *) val conjoin_neq : ?footprint: bool -> Exp.t -> Exp.t -> normal t -> normal t -(** Return the sub part of [prop]. *) -val get_sub : 'a t -> subst - -(** Return the pi part of [prop]. *) -val get_pi : 'a t -> atom list - (** Return the pure part of [prop]. *) val get_pure : 'a t -> atom list -(** Return the sigma part of [prop] *) -val get_sigma : 'a t -> hpred list - -(** Return the pi part of the footprint of [prop] *) -val get_pi_footprint : 'a t -> atom list - -(** Return the sigma part of the footprint of [prop] *) -val get_sigma_footprint : 'a t -> hpred list - (** Canonicalize the names of primed variables. *) val prop_rename_primed_footprint_vars : normal t -> normal t @@ -329,20 +322,9 @@ val from_pi : pi -> exposed t (** Build an exposed prop from sigma *) val from_sigma : sigma -> exposed t -(** Replace the substitution part of a prop *) -val replace_sub : Sil.subst -> 'a t -> exposed t - -(** Replace the pi part of a prop *) -val replace_pi : pi -> 'a t -> exposed t - -(** Replace the sigma part of a prop *) -val replace_sigma : sigma -> 'a t -> exposed t - -(** Replace the sigma part of the footprint of a prop *) -val replace_sigma_footprint : sigma -> 'a t -> exposed t - -(** Replace the pi part of the footprint of a prop *) -val replace_pi_footprint : pi -> 'a t -> exposed t +(** Set individual fields of the prop. *) +val set : ?sub:Sil.subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma -> + 'a t -> exposed t (** Rename free variables in a prop replacing them with existentially quantified vars *) val prop_rename_fav_with_existentials : normal t -> normal t diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml index aa61dcd47..457152a5c 100644 --- a/infer/src/backend/propgraph.ml +++ b/infer/src/backend/propgraph.ml @@ -62,11 +62,11 @@ let edge_get_succs = function | Esub_entry (_, e) -> [e] let get_sigma footprint_part g = - if footprint_part then Prop.get_sigma_footprint g else Prop.get_sigma g + if footprint_part then g.Prop.sigma_fp else g.Prop.sigma let get_pi footprint_part g = - if footprint_part then Prop.get_pi_footprint g else Prop.get_pi g + if footprint_part then g.Prop.pi_fp else g.Prop.pi let get_subl footprint_part g = - if footprint_part then [] else Sil.sub_to_list (Prop.get_sub g) + if footprint_part then [] else Sil.sub_to_list g.Prop.sub (** [edge_from_source g n footprint_part is_hpred] finds and edge with the given source [n] in prop [g]. [footprint_part] indicates whether to search the edge in the footprint part, and [is_pred] whether it is an hpred edge. *) @@ -214,9 +214,9 @@ let diff_get_colormap footprint_part diff = extracting its local stack vars if the boolean is true. *) let pp_proplist pe0 s (base_prop, extract_stack) f plist = let num = IList.length plist in - let base_stack = fst (Prop.sigma_get_stack_nonstack true (Prop.get_sigma base_prop)) in + let base_stack = fst (Prop.sigma_get_stack_nonstack true base_prop.Prop.sigma) in let add_base_stack prop = - if extract_stack then Prop.replace_sigma (base_stack @ Prop.get_sigma prop) prop + if extract_stack then Prop.set prop ~sigma:(base_stack @ prop.Prop.sigma) else Prop.expose prop in let update_pe_diff (prop: Prop.normal Prop.t) : printenv = if Config.print_using_diff then diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index be087e1a1..c6d667eb5 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -403,8 +403,8 @@ end = struct saturate { leqs = leqs_new; lts = lts_new; neqs = neqs_new } let from_prop prop = - let sigma = Prop.get_sigma prop in - let pi = Prop.get_pi prop in + let sigma = prop.Prop.sigma in + let pi = prop.Prop.pi in let ineq_sigma = from_sigma sigma in let ineq_pi = from_pi pi in saturate (join ineq_sigma ineq_pi) @@ -539,7 +539,7 @@ let check_equal prop e1 e2 = let check_equal_pi () = let eq = Sil.Aeq(n_e1, n_e2) in let n_eq = Prop.atom_normalize_prop prop eq in - let pi = Prop.get_pi prop in + let pi = prop.Prop.pi in IList.exists (Sil.atom_equal n_eq) pi in check_equal () || check_equal_const () || check_equal_pi () @@ -584,7 +584,7 @@ let get_bounds prop _e = (** Check whether [prop |- e1!=e2]. *) let check_disequal prop e1 e2 = - let spatial_part = Prop.get_sigma prop in + let spatial_part = prop.Prop.sigma in let n_e1 = Prop.exp_normalize_prop prop e1 in let n_e2 = Prop.exp_normalize_prop prop e2 in let check_disequal_const () = @@ -720,7 +720,7 @@ let get_smt_key a p = (** Check whether [prop |- a]. False means dont know. *) let check_atom prop a0 = let a = Prop.atom_normalize_prop prop a0 in - let prop_no_fp = Prop.replace_sigma_footprint [] (Prop.replace_pi_footprint [] prop) in + let prop_no_fp = Prop.set prop ~pi_fp:[] ~sigma_fp:[] in if Config.smt_output then begin let key = get_smt_key a prop_no_fp in let key_filename = @@ -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 _ | Anpred _ -> IList.exists (Sil.atom_equal a) (Prop.get_pi prop) + | Sil.Apred _ | Anpred _ -> IList.exists (Sil.atom_equal a) prop.Prop.pi (** Check [prop |- e1<=e2]. Result [false] means "don't know". *) let check_le prop e1 e2 = @@ -751,7 +751,7 @@ let check_le prop e1 e2 = (** Check whether [prop |- allocated(e)]. *) let check_allocatedness prop e = let n_e = Prop.exp_normalize_prop prop e in - let spatial_part = Prop.get_sigma prop in + let spatial_part = prop.Prop.sigma in let f = function | Sil.Hpointsto (base, _, _) -> is_root prop base n_e != None @@ -772,7 +772,7 @@ let compute_upper_bound_of_exp p e = (** Check if two hpreds have the same allocated lhs *) let check_inconsistency_two_hpreds prop = - let sigma = Prop.get_sigma prop in + let sigma = prop.Prop.sigma in let rec f e sigma_seen = function | [] -> false | (Sil.Hpointsto (e1, _, _) as hpred) :: sigma_rest @@ -791,7 +791,7 @@ let check_inconsistency_two_hpreds prop = then let prop' = Prop.normalize (Prop.from_sigma (sigma_seen@sigma_rest)) in let prop_new = Prop.conjoin_eq e1 e2 prop' in - let sigma_new = Prop.get_sigma prop_new in + let sigma_new = prop_new.Prop.sigma in let e_new = Prop.exp_normalize_prop prop_new e in f e_new [] sigma_new else f e (hpred:: sigma_seen) sigma_rest @@ -804,7 +804,7 @@ let check_inconsistency_two_hpreds prop = then let prop' = Prop.normalize (Prop.from_sigma (sigma_seen@sigma_rest)) in let prop_new = Prop.conjoin_eq e1 e3 prop' in - let sigma_new = Prop.get_sigma prop_new in + let sigma_new = prop_new.Prop.sigma in let e_new = Prop.exp_normalize_prop prop_new e in f e_new [] sigma_new else f e (hpred:: sigma_seen) sigma_rest in @@ -824,8 +824,8 @@ let check_inconsistency_two_hpreds prop = (** Inconsistency checking ignoring footprint. *) let check_inconsistency_base prop = - let pi = Prop.get_pi prop in - let sigma = Prop.get_sigma prop in + let pi = prop.Prop.pi in + let sigma = prop.Prop.sigma in let inconsistent_ptsto _ = check_allocatedness prop Exp.zero in let inconsistent_this_self_var () = @@ -965,7 +965,7 @@ end = struct | Sil.Hpointsto (_, Sil.Earray (Exp.Var _ as len, _, _), _) -> Sil.exp_fav_add fav len | _ -> () in - IList.iter do_hpred (Prop.get_sigma prop); + IList.iter do_hpred prop.Prop.sigma; fav let reset lhs rhs = @@ -1728,7 +1728,7 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2 let filter = function | Sil.Hpointsto(e', _, _) -> Exp.equal e' e | _ -> false in - IList.exists filter (Prop.get_sigma prop1) in + IList.exists filter prop1.Prop.sigma in let type_rhs e = let sub_opt = ref None in let filter = function @@ -2033,7 +2033,8 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * match is_constant_string_class subs hpred2' with | Some (s, is_string) -> (* allocate constant string hpred1', do implication, then add hpred1' as missing *) let hpred1' = if is_string then mk_constant_string_hpred s else mk_constant_class_hpred s in - let prop1' = Prop.normalize (Prop.replace_sigma (hpred1' :: Prop.get_sigma prop1) prop1) in + let prop1' = + Prop.normalize (Prop.set prop1 ~sigma:(hpred1' :: prop1.Prop.sigma)) in let subs', frame_prop = hpred_imply tenv calc_index_frame calc_missing subs prop1' sigma2 hpred2' in (* ProverState.add_missing_sigma [hpred1']; *) subs', frame_prop @@ -2068,7 +2069,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * let prepare_prop_for_implication (_, sub2) pi1 sigma1 = let pi1' = (Prop.pi_sub sub2 (ProverState.get_missing_pi ())) @ pi1 in let sigma1' = (Prop.sigma_sub sub2 (ProverState.get_missing_sigma ())) @ sigma1 in - let ep = Prop.replace_sub sub2 (Prop.replace_sigma sigma1' (Prop.from_pi pi1')) in + let ep = Prop.set Prop.prop_emp ~sub:sub2 ~sigma:sigma1' ~pi:pi1' in Prop.normalize ep let imply_pi calc_missing (sub1, sub2) prop pi2 = @@ -2155,10 +2156,10 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2 let filter (id, e) = Ident.is_normal id && Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in let sub1_base = - Sil.sub_filter_pair filter (Prop.get_sub prop1) in + Sil.sub_filter_pair filter prop1.Prop.sub in let pi1, pi2 = Prop.get_pure prop1, Prop.get_pure prop2 in - let sigma1, sigma2 = Prop.get_sigma prop1, Prop.get_sigma prop2 in - let subs = pre_check_pure_implication calc_missing (Prop.get_sub prop1, sub1_base) pi1 pi2 in + let sigma1, sigma2 = prop1.Prop.sigma, prop2.Prop.sigma in + let subs = pre_check_pure_implication calc_missing (prop1.Prop.sub, sub1_base) pi1 pi2 in let pi2_bcheck, pi2_nobcheck = (* find bounds checks implicit in pi2 *) IList.partition ProverState.atom_is_array_bounds_check pi2 in IList.iter (fun a -> ProverState.add_bounds_check (ProverState.BCfrom_pre a)) pi2_bcheck; @@ -2186,7 +2187,7 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2 L.d_strln "Result of Abduction"; L.d_increase_indent 1; d_impl (sub1, sub2) (prop1, prop2); L.d_decrease_indent 1; L.d_ln (); L.d_strln"returning TRUE"; - let frame = Prop.get_sigma frame_prop in + let frame = frame_prop.Prop.sigma in if check_frame_empty && frame != [] then raise (IMPL_EXC("frame not empty", subs, EXC_FALSE)); Some ((sub1, sub2), frame) with diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 3a3b3c665..ebb3db168 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -596,9 +596,9 @@ let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst = Prop.d_prop (Prop.prop_hpred_star Prop.prop_emp ptsto); L.d_ln (); L.d_ln (); let eprop = Prop.expose prop in - let foot_sigma = ptsto_foot :: Prop.get_sigma_footprint eprop in - let nfoot_sigma = Prop.sigma_normalize_prop Prop.prop_emp foot_sigma in - let prop' = Prop.normalize (Prop.replace_sigma_footprint nfoot_sigma eprop) in + let sigma_fp = ptsto_foot :: eprop.Prop.sigma_fp in + let nsigma_fp = Prop.sigma_normalize_prop Prop.prop_emp sigma_fp in + let prop' = Prop.normalize (Prop.set eprop ~sigma_fp:nsigma_fp) in let prop_new = IList.fold_left (Prop.prop_atom_and ~footprint:!Config.footprint) prop' atoms in let iter = match (Prop.prop_iter_create prop_new) with | None -> @@ -766,12 +766,12 @@ let add_guarded_by_constraints prop lexp pdesc = false) flds | _ -> false) - (Prop.get_sigma prop) in + prop.Prop.sigma in Cfg.Procdesc.get_access pdesc <> PredSymb.Private && not (Annotations.pdesc_has_annot pdesc Annotations.visibleForTesting) && not (Procname.java_is_access_method (Cfg.Procdesc.get_proc_name pdesc)) && not (is_accessible_through_local_ref lexp) in - match find_guarded_by_exp guarded_by_str (Prop.get_sigma prop) with + match find_guarded_by_exp guarded_by_str prop.Prop.sigma with | Some (Sil.Eexp (guarded_by_exp, _), typ) -> if is_read_write_lock typ then @@ -824,7 +824,7 @@ let add_guarded_by_constraints prop lexp pdesc = enforce_guarded_access fld typ prop | _ -> (* check for access via alias *) - IList.fold_left hpred_check_flds prop (Prop.get_sigma prop) + IList.fold_left hpred_check_flds prop prop.Prop.sigma (** Add a pointsto for [root(lexp): typ] to the iterator and to the footprint, if it's compatible with the allowed footprint @@ -837,10 +837,10 @@ let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst = L.d_strln "++++ Adding footprint frame"; Prop.d_prop (Prop.prop_hpred_star Prop.prop_emp ptsto); L.d_ln (); L.d_ln (); - let foot_sigma = ptsto_foot :: (Prop.prop_iter_get_footprint_sigma iter) in + let sigma_fp = ptsto_foot :: (Prop.prop_iter_get_footprint_sigma iter) in let iter_foot = Prop.prop_iter_prev_then_insert iter ptsto in let iter_foot_atoms = IList.fold_left (Prop.prop_iter_add_atom (!Config.footprint)) iter_foot atoms in - let iter' = Prop.prop_iter_replace_footprint_sigma iter_foot_atoms foot_sigma in + let iter' = Prop.prop_iter_replace_footprint_sigma iter_foot_atoms sigma_fp in let offsets_default = Sil.exp_get_offsets lexp in Prop.prop_iter_set_state iter' offsets_default @@ -1223,7 +1223,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = | _ -> true in IList.for_all is_strexp_pt_by_nullable_fld flds | _ -> true) - (Prop.get_sigma prop) && + prop.Prop.sigma && !nullable_obj_str <> None in let root = Exp.root_of_lexp lexp in let is_deref_of_nullable = diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 6448d6650..5f2acfa16 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -440,7 +440,7 @@ let check_already_dereferenced pname cond prop = let find_hpred lhs = try Some (IList.find (function | Sil.Hpointsto (e, _, _) -> Exp.equal e lhs - | _ -> false) (Prop.get_sigma prop)) + | _ -> false) prop.Prop.sigma) with Not_found -> None in let rec is_check_zero = function | Exp.Var id -> @@ -532,7 +532,7 @@ let resolve_typename prop receiver_exp = | [] -> None | Sil.Hpointsto(e, _, typexp) :: _ when Exp.equal e receiver_exp -> Some typexp | _ :: hpreds -> loop hpreds in - loop (Prop.get_sigma prop) in + loop prop.Prop.sigma in match typexp_opt with | Some (Exp.Sizeof (Typ.Tstruct { Typ.struct_name = None }, _, _)) -> None | Some (Exp.Sizeof (Typ.Tstruct { Typ.csu = Csu.Class ck; struct_name = Some name }, _, _)) -> @@ -796,8 +796,8 @@ let add_strexp_to_footprint strexp abducted_pv typ prop = let lvar_pt_fpvar = let sizeof_exp = Exp.Sizeof (typ, None, Subtype.subtypes) in Prop.mk_ptsto abducted_lvar strexp sizeof_exp in - let sigma_fp = Prop.get_sigma_footprint prop in - Prop.normalize (Prop.replace_sigma_footprint (lvar_pt_fpvar :: sigma_fp) prop) + let sigma_fp = prop.Prop.sigma_fp in + Prop.normalize (Prop.set prop ~sigma_fp:(lvar_pt_fpvar :: sigma_fp)) let add_to_footprint abducted_pv typ prop = let fresh_fp_var = Exp.Var (Ident.create_fresh Ident.kfootprint) in @@ -824,7 +824,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_ (fun hpred -> match hpred with | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abducted_ret_pv | _ -> false) - (Prop.get_sigma_footprint p) in + p.Prop.sigma_fp in (* find an hpred [abducted] |-> A in [prop] and add [exp] = A to prop *) let bind_exp_to_abducted_val exp_to_bind abducted prop = let bind_exp prop = function @@ -832,7 +832,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_ when Pvar.equal pv abducted -> Prop.conjoin_eq exp_to_bind rhs prop | _ -> prop in - IList.fold_left bind_exp prop (Prop.get_sigma prop) in + IList.fold_left bind_exp prop prop.Prop.sigma in (* To avoid obvious false positives, assume skip functions do not return null pointers *) let add_ret_non_null exp typ prop = if has_nullable_annot @@ -1217,12 +1217,12 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path match IList.partition (function | Sil.Hpointsto (Exp.Lvar pvar', _, _) -> Pvar.equal pvar pvar' - | _ -> false) (Prop.get_sigma eprop) with + | _ -> false) eprop.Prop.sigma with | [Sil.Hpointsto(e, se, typ)], sigma' -> let sigma'' = let se' = execute_nullify_se se in Sil.Hpointsto(e, se', typ):: sigma' in - let eprop_res = Prop.replace_sigma sigma'' eprop in + let eprop_res = Prop.set eprop ~sigma:sigma'' in ret_old_path [Prop.normalize eprop_res] | [], _ -> ret_old_path [prop_] @@ -1252,8 +1252,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path (IList.map add_None ptl) in Config.run_in_re_execution_mode (* no footprint vars for locals *) sigma_locals () in - let sigma' = Prop.get_sigma prop_ @ sigma_locals in - let prop' = Prop.normalize (Prop.replace_sigma sigma' prop_) in + let sigma' = prop_.Prop.sigma @ sigma_locals in + let prop' = Prop.normalize (Prop.set prop_ ~sigma:sigma') in ret_old_path [prop'] | Sil.Stackop _ -> (* this should be handled at the propset level *) assert false @@ -1287,8 +1287,8 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call (function | Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual_var -> new_hpred | hpred -> hpred) - (Prop.get_sigma prop) in - Prop.normalize (Prop.replace_sigma sigma' prop) in + prop.Prop.sigma in + Prop.normalize (Prop.set prop ~sigma:sigma') in if Config.angelic_execution then let add_actual_by_ref_to_footprint prop (actual, actual_typ) = match actual with @@ -1301,7 +1301,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call (fun hpred -> match hpred with | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abducted_ref_pv | _ -> false) - (Prop.get_sigma_footprint p) in + p.Prop.sigma_fp in (* prevent introducing multiple abducted retvals for a single call site in a loop *) if already_has_abducted_retval prop then prop else @@ -1327,8 +1327,8 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call | Sil.Hpointsto (lhs, _, typ_exp) when Exp.equal lhs actual -> Sil.Hpointsto (lhs, abduced_strexp, typ_exp) | hpred -> hpred) - (Prop.get_sigma prop') in - Prop.normalize (Prop.replace_sigma filtered_sigma prop') + prop'.Prop.sigma in + Prop.normalize (Prop.set prop' ~sigma:filtered_sigma) else (* bind actual passed by ref to the abducted value pointed to by the synthetic pvar *) let prop' = @@ -1338,17 +1338,17 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call | Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual -> false | _ -> true) - (Prop.get_sigma prop) in - Prop.normalize (Prop.replace_sigma filtered_sigma prop) in + prop.Prop.sigma in + Prop.normalize (Prop.set prop ~sigma:filtered_sigma) in IList.fold_left (fun p hpred -> match hpred with | Sil.Hpointsto (Exp.Lvar pv, rhs, texp) when Pvar.equal pv abducted_ref_pv -> let new_hpred = Sil.Hpointsto (actual, rhs, texp) in - Prop.normalize (Prop.replace_sigma (new_hpred :: (Prop.get_sigma prop')) p) + Prop.normalize (Prop.set p ~sigma:(new_hpred :: prop'.Prop.sigma)) | _ -> p) prop' - (Prop.get_sigma prop') + prop'.Prop.sigma | _ -> assert false in IList.fold_left add_actual_by_ref_to_footprint prop actuals_by_ref else diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 540218ac6..2037457ce 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -332,7 +332,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = let deref_err_list = IList.fold_left (fun deref_errs hpred -> match check_hpred hpred with | Some reason -> reason :: deref_errs | None -> deref_errs - ) [] (Prop.get_sigma spec_pre) in + ) [] spec_pre.Prop.sigma in match deref_err_list with | [] -> None | deref_err :: _ -> @@ -393,10 +393,10 @@ let post_process_post let ra' = { ra with ra_pname = callee_pname; ra_loc = loc; ra_vpath = vpath } in 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 + let prop' = Prop.set post ~sigma:(post_process_sigma post.Prop.sigma loc) in + let pi' = IList.map atom_update_alloc_attribute prop'.Prop.pi in (* update alloc attributes to refer to the caller *) - let post' = Prop.replace_pi pi' prop' in + let post' = Prop.set prop' ~pi:pi' in check_path_errors_in_post caller_pname post' post_path; post', post_path @@ -571,17 +571,14 @@ let prop_footprint_add_pi_sigma_starfld_sigma extend_pi current_pi new_pi' end else extend_pi (a :: current_pi) new_pi' in - let foot_pi' = extend_pi (Prop.get_pi_footprint prop) pi_new in - match extend_sigma (Prop.get_sigma_footprint prop) sigma_new with + let pi_fp' = extend_pi prop.Prop.pi_fp pi_new in + match extend_sigma prop.Prop.sigma_fp sigma_new with | None -> None | Some sigma' -> - let foot_sigma' = sigma_star_fld sigma' missing_fld in - let foot_sigma'' = sigma_star_typ foot_sigma' missing_typ in - let pi' = pi_new @ Prop.get_pi prop in - let prop' = - Prop.replace_sigma_footprint foot_sigma'' (Prop.replace_pi_footprint foot_pi' prop) in - let prop'' = Prop.replace_pi pi' prop' in - Some (Prop.normalize prop'') + let sigma_fp' = sigma_star_fld sigma' missing_fld in + let sigma_fp'' = sigma_star_typ sigma_fp' missing_typ in + let pi' = pi_new @ prop.Prop.pi in + Some (Prop.normalize (Prop.set prop ~pi:pi' ~pi_fp:pi_fp' ~sigma_fp:sigma_fp'')) (** Check if the attribute change is a mismatch between a kind of allocation and a different kind of deallocation *) @@ -596,11 +593,10 @@ let check_attr_dealloc_mismatch att_old att_new = match att_old, att_new with (** [prop_copy_footprint p1 p2] copies the footprint and pure part of [p1] into [p2] *) let prop_copy_footprint_pure p1 p2 = let p2' = - Prop.replace_sigma_footprint - (Prop.get_sigma_footprint p1) (Prop.replace_pi_footprint (Prop.get_pi_footprint p1) p2) in - let pi2 = Prop.get_pi p2' in + Prop.set p2 ~pi_fp:p1.Prop.pi_fp ~sigma_fp:p1.Prop.sigma_fp in + let pi2 = p2'.Prop.pi in let pi2_attr, pi2_noattr = IList.partition Attribute.is_pred pi2 in - let res_noattr = Prop.replace_pi (Prop.get_pure p1 @ pi2_noattr) p2' in + let res_noattr = Prop.set p2' ~pi:(Prop.get_pure p1 @ pi2_noattr) in let replace_attr prop atom = (* call replace_atom_attribute which deals with existing attibutes *) (* if [atom] represents an attribute [att], add the attribure to [prop] *) if Attribute.is_pred atom then @@ -621,7 +617,7 @@ let prop_is_exn pname prop = | Sil.Hpointsto (e1, Sil.Eexp(e2, _), _) when Exp.equal e1 ret_pvar -> exp_is_exn e2 | _ -> false in - IList.exists is_exn (Prop.get_sigma prop) + IList.exists is_exn prop.Prop.sigma (** when prop is an exception, return the exception name *) let prop_get_exn_name pname prop = @@ -638,7 +634,7 @@ let prop_get_exn_name pname prop = when Exp.equal e1 ret_pvar -> search_exn e2 hpreds | _ :: tl -> find_exn_name hpreds tl in - let hpreds = Prop.get_sigma prop in + let hpreds = prop.Prop.sigma in find_exn_name hpreds hpreds @@ -649,7 +645,7 @@ let lookup_custom_errors prop = | Sil.Hpointsto (Exp.Lvar var, Sil.Eexp (Exp.Const (Const.Cstr error_str), _), _) :: _ when Pvar.equal var Sil.custom_error -> Some error_str | _ :: tl -> search_error tl in - search_error (Prop.get_sigma prop) + search_error prop.Prop.sigma (** set a prop to an exception sexp *) let prop_set_exn pname prop se_exn = @@ -658,8 +654,8 @@ let prop_set_exn pname prop se_exn = | Sil.Hpointsto (e, _, t) when Exp.equal e ret_pvar -> Sil.Hpointsto(e, se_exn, t) | hpred -> hpred in - let sigma' = IList.map map_hpred (Prop.get_sigma prop) in - Prop.normalize (Prop.replace_sigma sigma' prop) + let sigma' = IList.map map_hpred prop.Prop.sigma in + Prop.normalize (Prop.set prop ~sigma:sigma') (** Include a subtrace for a procedure call if the callee is not a model. *) let include_subtrace callee_pname = @@ -678,7 +674,7 @@ let combine if !Config.footprint && posts = [] then (* in case of divergence, produce a prop *) (* with updated footprint and inconsistent current *) - [(Prop.replace_pi [Sil.Aneq (Exp.zero, Exp.zero)] Prop.prop_emp, path_pre)] + [(Prop.set Prop.prop_emp ~pi:[Sil.Aneq (Exp.zero, Exp.zero)], path_pre)] else IList.map (fun (p, path_post) -> @@ -712,9 +708,9 @@ let combine L.d_decrease_indent 1; L.d_ln (); let compute_result post_p = let post_p' = - let post_sigma = sigma_star_fld (Prop.get_sigma post_p) split.frame_fld in + let post_sigma = sigma_star_fld post_p.Prop.sigma split.frame_fld in let post_sigma' = sigma_star_typ post_sigma split.frame_typ in - Prop.replace_sigma post_sigma' post_p in + Prop.set post_p ~sigma:post_sigma' in let post_p1 = Prop.prop_sigma_star (prop_copy_footprint_pure actual_pre post_p') split.frame in let handle_null_case_analysis sigma = @@ -732,10 +728,10 @@ let combine Sil.hpred_list_expmap f sigma in let post_p2 = - let post_p1_sigma = Prop.get_sigma post_p1 in + let post_p1_sigma = post_p1.Prop.sigma in let post_p1_sigma' = handle_null_case_analysis post_p1_sigma in - let post_p1' = Prop.replace_sigma post_p1_sigma' post_p1 in - Prop.normalize (Prop.replace_pi (Prop.get_pi post_p1 @ split.missing_pi) post_p1') in + let post_p1' = Prop.set post_p1 ~sigma:post_p1_sigma' in + Prop.normalize (Prop.set post_p1' ~pi:(post_p1.Prop.pi @ split.missing_pi)) in let post_p3 = (* replace [result|callee] with an aux variable dedicated to this proc *) let callee_ret_pvar = @@ -895,7 +891,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts = | Sil.Hpointsto (Exp.Lvar pvar, Sil.Eexp (e, _), _) when Pvar.is_return pvar -> Prover.check_equal (Prop.normalize prop) e Exp.zero | _ -> false) - (Prop.get_sigma prop) in + prop.Prop.sigma in IList.filter (fun (prop, _) -> not (returns_null prop)) posts else posts in let mk_retval_tainted posts = @@ -929,7 +925,7 @@ let inconsistent_actualpre_missing actual_pre split_opt = (* perform the taint analysis check by comparing the taint atoms in [calling_pi] with the untaint atoms required by the [missing_pi] computed during abduction *) let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_params = - let calling_pi = Prop.get_pi calling_prop in + let calling_pi = calling_prop.Prop.pi in (* get a version of [missing_pi] whose var names match the names in calling pi *) let missing_pi_sub = Prop.pi_sub sub missing_pi in let combined_pi = calling_pi @ missing_pi_sub in @@ -1093,9 +1089,9 @@ let remove_constant_string_class prop = let filter = function | Sil.Hpointsto (Exp.Const (Const.Cstr _ | Const.Cclass _), _, _) -> false | _ -> true in - let sigma = IList.filter filter (Prop.get_sigma prop) in - let sigmafp = IList.filter filter (Prop.get_sigma_footprint prop) in - let prop' = Prop.replace_sigma_footprint sigmafp (Prop.replace_sigma sigma prop) in + let sigma = IList.filter filter prop.Prop.sigma in + let sigmafp = IList.filter filter prop.Prop.sigma_fp in + let prop' = Prop.set prop ~sigma ~sigma_fp:sigmafp in Prop.normalize prop' (** existentially quantify the path identifier generated @@ -1118,7 +1114,7 @@ let prop_pure_to_footprint (p: 'a Prop.t) : Prop.normal Prop.t = if new_footprint_atoms == [] then p else (* add pure fact to footprint *) - Prop.normalize (Prop.replace_pi_footprint (Prop.get_pi_footprint p @ new_footprint_atoms) p) + Prop.normalize (Prop.set p ~pi_fp:(p.Prop.pi_fp @ new_footprint_atoms)) (** post-process the raw result of a function call *) let exe_call_postprocess ret_ids trace_call callee_pname callee_attrs loc results = diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml index cbfda8e88..a21383267 100644 --- a/infer/src/backend/taint.ml +++ b/infer/src/backend/taint.ml @@ -381,4 +381,4 @@ let add_tainting_attribute att pvar_param prop = (Pvar.to_string pvar)); Attribute.add_or_replace prop_acc (Apred (att, [rhs])) | _ -> prop_acc) - prop (Prop.get_sigma prop) + prop prop.Prop.sigma