pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Clean up API to access components of propositions.

Browse Source 
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
master
Cristiano Calcagno 8 years ago committed by Facebook Github Bot 0
parent 89270c558c
commit b48ec1ac93
17 changed files with 340 additions and 475 deletions
Show Stats Download Patch File Download Diff File

18
infer/src/IR/Cfg.re
Unescape View File

@ -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')
};

31
infer/src/backend/Attribute.ml
Unescape View File

@ -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 ->

64
infer/src/backend/abs.ml
Unescape View File

@ -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 =

75
infer/src/backend/absarray.ml
Unescape View File

@ -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)
*)

54
infer/src/backend/dom.ml
Unescape View File

@ -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

35
infer/src/backend/dotty.ml
Unescape View File

@ -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

12
infer/src/backend/errdesc.ml
Unescape View File

@ -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

29
infer/src/backend/interproc.ml
Unescape View File

@ -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.

54
infer/src/backend/modelBuiltins.ml
Unescape View File

@ -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

228
infer/src/backend/prop.ml
Unescape View File

@ -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
*)

42
infer/src/backend/prop.mli
Unescape View File

@ -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

10
infer/src/backend/propgraph.ml
Unescape View File

@ -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

41
infer/src/backend/prover.ml
Unescape View File

@ -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

18
infer/src/backend/rearrange.ml
Unescape View File

@ -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 =

38
infer/src/backend/symExec.ml
Unescape View File

@ -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

64
infer/src/backend/tabulation.ml
Unescape View File

@ -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 =

2
infer/src/backend/taint.ml
Unescape View File

@ -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

Write Preview
Loading…
Cancel
Save