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

Save global state for abstraction for on-demand.

Browse Source 
Reviewed By: sblackshear

Differential Revision: D2971122

fb-gh-sync-id: f7600f0
shipit-source-id: f7600f0
master
Cristiano Calcagno 9 years ago committed by facebook-github-bot-5
parent 90489d7f54
commit 16402cddc0
13 changed files with 182 additions and 464 deletions
Show Stats Download Patch File Download Diff File

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

@ -562,14 +562,34 @@ let discover_para_dll tenv p =
| None -> paras
| Some para -> if already_defined para paras then paras else para :: paras in
IList.fold_left f [] candidates
(****************** Start of Predicate Discovery ******************)
(****************** End of Predicate Discovery ******************)
(****************** Start of the ADT abs_rules ******************)
type para_ty = SLL of Sil.hpara | DLL of Sil.hpara_dll
(** Type of parameter for abstraction rules *)
type para_ty =
| SLL of Sil.hpara
| DLL of Sil.hpara_dll
(** Rule set: a list of rules of a given type *)
type rule_set = para_ty * rule list
type abs_rules = { mutable ar_default : rule_set list }
type rules = rule_set list
module Global =
struct
let current_rules : rules ref =
ref []
end
let get_current_rules () =
!Global.current_rules
let set_current_rules rules =
Global.current_rules := rules
let reset_current_rules () =
Global.current_rules := []
let eqs_sub subst eqs =
IList.map (fun (e1, e2) -> (Sil.exp_sub subst e1, Sil.exp_sub subst e2)) eqs
@ -658,30 +678,6 @@ let hpara_special_cases_dll hpara : Sil.hpara_dll list =
let special_cases = sigma_special_cases hpara.Sil.evars_dll hpara.Sil.body_dll in
IList.map update_para special_cases
let abs_rules : abs_rules = { ar_default = [] }
let abs_rules_reset () =
abs_rules.ar_default <- []
let abs_rules_add rule_set : unit =
(*
let _ = match (fst rule_set) with
| SLL hpara -> L.out "@.@....Added Para: %a@.@." pp_hpara hpara
| DLL _ -> ()
in
*)
abs_rules.ar_default <- abs_rules.ar_default@[rule_set]
let abs_rules_add_sll (para: Sil.hpara) : unit =
let rules = mk_rules_for_sll para in
let rule_set = (SLL para, rules) in
abs_rules_add rule_set
let abs_rules_add_dll (para: Sil.hpara_dll) : unit =
let rules = mk_rules_for_dll para in
let rule_set = (DLL para, rules) in
abs_rules_add rule_set
let abs_rules_apply_rsets (rsets: rule_set list) (p_in: Prop.normal Prop.t) : Prop.normal Prop.t =
let apply_rule (changed, p) r =
match (sigma_rewrite p r) with
@ -700,7 +696,7 @@ let abs_rules_apply_rsets (rsets: rule_set list) (p_in: Prop.normal Prop.t) : Pr
let abs_rules_apply_lists tenv (p_in: Prop.normal Prop.t) : Prop.normal Prop.t =
let new_rsets = ref [] in
let def_rsets = abs_rules.ar_default in
let old_rsets = get_current_rules () in
let rec discover_then_abstract p =
let (closed_paras_sll, closed_paras_dll) =
let paras_sll = discover_para tenv p in
@ -723,18 +719,26 @@ let abs_rules_apply_lists tenv (p_in: Prop.normal Prop.t) : Prop.normal Prop.t =
(closed_paras_sll, closed_paras_dll)
end in
let (todo_paras_sll, todo_paras_dll) =
let eq_sll para = function (SLL para', _) -> Match.hpara_iso para para' | _ -> false in
let eq_dll para = function (DLL para', _) -> Match.hpara_dll_iso para para' | _ -> false in
let eq_sll para rset = match rset with
| (SLL para', _) -> Match.hpara_iso para para'
| _ -> false in
let eq_dll para rset = match rset with
| (DLL para', _) -> Match.hpara_dll_iso para para'
| _ -> false in
let filter_sll para =
not (IList.exists (eq_sll para) def_rsets) && not (IList.exists (eq_sll para) !new_rsets) in
not (IList.exists (eq_sll para) old_rsets) &&
not (IList.exists (eq_sll para) !new_rsets) in
let filter_dll para =
not (IList.exists (eq_dll para) def_rsets) && not (IList.exists (eq_dll para) !new_rsets) in
not (IList.exists (eq_dll para) old_rsets) &&
not (IList.exists (eq_dll para) !new_rsets) in
let todo_paras_sll = IList.filter filter_sll closed_paras_sll in
let todo_paras_dll = IList.filter filter_dll closed_paras_dll in
(todo_paras_sll, todo_paras_dll) in
let f_recurse () =
let todo_rsets_sll = IList.map (fun para -> (SLL para, mk_rules_for_sll para)) todo_paras_sll in
let todo_rsets_dll = IList.map (fun para -> (DLL para, mk_rules_for_dll para)) todo_paras_dll in
let todo_rsets_sll =
IList.map (fun para -> (SLL para, mk_rules_for_sll para)) todo_paras_sll in
let todo_rsets_dll =
IList.map (fun para -> (DLL para, mk_rules_for_dll para)) todo_paras_dll in
new_rsets := !new_rsets @ todo_rsets_sll @ todo_rsets_dll;
let p' = abs_rules_apply_rsets todo_rsets_sll p in
let p'' = abs_rules_apply_rsets todo_rsets_dll p' in
@ -742,203 +746,16 @@ let abs_rules_apply_lists tenv (p_in: Prop.normal Prop.t) : Prop.normal Prop.t =
match todo_paras_sll, todo_paras_dll with
| [], [] -> p
| _ -> f_recurse () in
let p1 = abs_rules_apply_rsets def_rsets p_in in
let p2 = if !Config.on_the_fly then discover_then_abstract p1 else p1
in
abs_rules.ar_default <- (def_rsets@(!new_rsets));
let p1 = abs_rules_apply_rsets old_rsets p_in in
let p2 = discover_then_abstract p1 in
let new_rules = old_rsets @ !new_rsets in
set_current_rules new_rules;
p2
let abs_rules_apply tenv (p_in: Prop.normal Prop.t) : Prop.normal Prop.t =
abs_rules_apply_lists tenv p_in
(****************** End of the ADT abs_rules ******************)
(****************** Start of fns that add rules during preprocessing ******************)
let is_simply_recursive tenv tname =
let typ = match Sil.tenv_lookup tenv tname with
| None -> assert false
| Some typ -> typ in
let filter (_, t, _) = match t with
| Sil.Tvar _ | Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tenum _ ->
false
| Sil.Tptr (Sil.Tvar tname', _) ->
Typename.equal tname tname'
| Sil.Tptr _ | Sil.Tstruct _ | Sil.Tarray _ ->
false in
match typ with
| Sil.Tvar _ ->
assert false (* there should be no indirection *)
| Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ | Sil.Tenum _ ->
None
| Sil.Tstruct { Sil.instance_fields } ->
begin
match (IList.filter filter instance_fields) with
| [(fld, _, _)] -> Some fld
| _ -> None
end
| Sil.Tarray _ ->
None
let create_hpara_from_tname_flds tenv tname nfld sflds eflds inst =
let typ = match Sil.tenv_lookup tenv tname with
| Some typ -> typ
| None -> assert false in
let id_base = Ident.create_fresh Ident.kprimed in
let id_next = Ident.create_fresh Ident.kprimed in
let ids_shared = IList.map (fun _ -> Ident.create_fresh Ident.kprimed) sflds in
let ids_exist = IList.map (fun _ -> Ident.create_fresh Ident.kprimed) eflds in
let exp_base = Sil.Var id_base in
let fld_sexps =
let ids = id_next :: (ids_shared @ ids_exist) in
let flds = nfld :: (sflds @ eflds) in
let f fld id = (fld, Sil.Eexp (Sil.Var id, inst)) in
try IList.map2 f flds ids with Invalid_argument _ -> assert false in
let strexp_para = Sil.Estruct (fld_sexps, inst) in
let ptsto_para = Prop.mk_ptsto exp_base strexp_para (Sil.Sizeof (typ, Sil.Subtype.exact)) in
Prop.mk_hpara id_base id_next ids_shared ids_exist [ptsto_para]
let create_dll_hpara_from_tname_flds tenv tname flink blink sflds eflds inst =
let typ = match Sil.tenv_lookup tenv tname with
| Some typ -> typ
| None -> assert false in
let id_iF = Ident.create_fresh Ident.kprimed in
let id_oB = Ident.create_fresh Ident.kprimed in
let id_oF = Ident.create_fresh Ident.kprimed in
let ids_shared = IList.map (fun _ -> Ident.create_fresh Ident.kprimed) sflds in
let ids_exist = IList.map (fun _ -> Ident.create_fresh Ident.kprimed) eflds in
let exp_iF = Sil.Var id_iF in
let fld_sexps =
let ids = id_oF:: id_oB :: (ids_shared @ ids_exist) in
let flds = flink:: blink:: (sflds @ eflds) in
let f fld id = (fld, Sil.Eexp (Sil.Var id, inst)) in
try IList.map2 f flds ids with Invalid_argument _ -> assert false in
let strexp_para = Sil.Estruct (fld_sexps, inst) in
let ptsto_para = Prop.mk_ptsto exp_iF strexp_para (Sil.Sizeof (typ, Sil.Subtype.exact)) in
Prop.mk_dll_hpara id_iF id_oB id_oF ids_shared ids_exist [ptsto_para]
let create_hpara_two_ptsto tname1 tenv nfld1 dfld tname2 nfld2 inst =
let typ1 = match Sil.tenv_lookup tenv tname1 with
| Some typ -> typ
| None -> assert false in
let typ2 = match Sil.tenv_lookup tenv tname2 with
| Some typ -> typ
| None -> assert false in
let id_base = Ident.create_fresh Ident.kprimed in
let id_next = Ident.create_fresh Ident.kprimed in
let id_exist = Ident.create_fresh Ident.kprimed in
let exp_base = Sil.Var id_base in
let exp_exist = Sil.Var id_exist in
let fld_sexps1 =
let ids = [id_next; id_exist] in
let flds = [nfld1; dfld] in
let f fld id = (fld, Sil.Eexp (Sil.Var id, inst)) in
try IList.map2 f flds ids with Invalid_argument _ -> assert false in
let fld_sexps2 =
[(nfld2, Sil.Eexp (Sil.exp_zero, inst))] in
let strexp_para1 = Sil.Estruct (fld_sexps1, inst) in
let strexp_para2 = Sil.Estruct (fld_sexps2, inst) in
let ptsto_para1 = Prop.mk_ptsto exp_base strexp_para1 (Sil.Sizeof (typ1, Sil.Subtype.exact)) in
let ptsto_para2 = Prop.mk_ptsto exp_exist strexp_para2 (Sil.Sizeof (typ2, Sil.Subtype.exact)) in
Prop.mk_hpara id_base id_next [] [id_exist] [ptsto_para1; ptsto_para2]
let create_hpara_dll_two_ptsto tenv tname1 flink_fld1 blink_fld1 dfld tname2 nfld2 inst =
let typ1 = match Sil.tenv_lookup tenv tname1 with
| Some typ -> typ
| None -> assert false in
let typ2 = match Sil.tenv_lookup tenv tname2 with
| Some typ -> typ
| None -> assert false in
let id_cell = Ident.create_fresh Ident.kprimed in
let id_blink = Ident.create_fresh Ident.kprimed in
let id_flink = Ident.create_fresh Ident.kprimed in
let id_exist = Ident.create_fresh Ident.kprimed in
let exp_cell = Sil.Var id_cell in
let exp_exist = Sil.Var id_exist in
let fld_sexps1 =
let ids = [ id_blink; id_flink; id_exist] in
let flds = [ blink_fld1; flink_fld1; dfld] in
let f fld id = (fld, Sil.Eexp (Sil.Var id, inst)) in
try IList.map2 f flds ids with Invalid_argument _ -> assert false in
let fld_sexps2 =
[(nfld2, Sil.Eexp (Sil.exp_zero, inst))] in
let strexp_para1 = Sil.Estruct (fld_sexps1, inst) in
let strexp_para2 = Sil.Estruct (fld_sexps2, inst) in
let ptsto_para1 = Prop.mk_ptsto exp_cell strexp_para1 (Sil.Sizeof (typ1, Sil.Subtype.exact)) in
let ptsto_para2 = Prop.mk_ptsto exp_exist strexp_para2 (Sil.Sizeof (typ2, Sil.Subtype.exact)) in
Prop.mk_dll_hpara id_cell id_blink id_flink [] [id_exist] [ptsto_para1; ptsto_para2]
let create_hpara_from_tname_twoflds_hpara tenv tname fld_next fld_down para inst =
let typ = match Sil.tenv_lookup tenv tname with
| Some typ -> typ
| None -> assert false in
let id_base = Ident.create_fresh Ident.kprimed in
let id_next = Ident.create_fresh Ident.kprimed in
let id_down = Ident.create_fresh Ident.kprimed in
let exp_base = Sil.Var id_base in
let exp_next = Sil.Var id_next in
let exp_down = Sil.Var id_down in
let strexp = Sil.Estruct ([(fld_next, Sil.Eexp (exp_next, inst)); (fld_down, Sil.Eexp (exp_down, inst))], inst) in
let ptsto = Prop.mk_ptsto exp_base strexp (Sil.Sizeof (typ, Sil.Subtype.exact)) in
let lseg = Prop.mk_lseg Sil.Lseg_PE para exp_down Sil.exp_zero [] in
let body = [ptsto; lseg] in
Prop.mk_hpara id_base id_next [] [id_down] body
let create_hpara_dll_from_tname_twoflds_hpara tenv tname fld_flink fld_blink fld_down para inst =
let typ = match Sil.tenv_lookup tenv tname with
| Some typ -> typ
| None -> assert false in
let id_cell = Ident.create_fresh Ident.kprimed in
let id_blink = Ident.create_fresh Ident.kprimed in
let id_flink = Ident.create_fresh Ident.kprimed in
let id_down = Ident.create_fresh Ident.kprimed in
let exp_cell = Sil.Var id_cell in
let exp_blink = Sil.Var id_blink in
let exp_flink = Sil.Var id_flink in
let exp_down = Sil.Var id_down in
let strexp = Sil.Estruct ([(fld_blink, Sil.Eexp (exp_blink, inst)); (fld_flink, Sil.Eexp (exp_flink, inst)); (fld_down, Sil.Eexp (exp_down, inst))], inst) in
let ptsto = Prop.mk_ptsto exp_cell strexp (Sil.Sizeof (typ, Sil.Subtype.exact)) in
let lseg = Prop.mk_lseg Sil.Lseg_PE para exp_down Sil.exp_zero [] in
let body = [ptsto; lseg] in
Prop.mk_dll_hpara id_cell id_blink id_flink [] [id_down] body
let tname_list = Typename.TN_typedef (Mangled.from_string "list")
let name_down = Ident.create_fieldname (Mangled.from_string "down") 0
let tname_HSlist2 = Typename.TN_typedef (Mangled.from_string "HSlist2")
let name_next = Ident.create_fieldname (Mangled.from_string "next") 0
let tname_dllist = Typename.TN_typedef (Mangled.from_string "dllist")
let name_Flink = Ident.create_fieldname (Mangled.from_string "Flink") 0
let name_Blink = Ident.create_fieldname (Mangled.from_string "Blink") 0
let tname_HOdllist = Typename.TN_typedef (Mangled.from_string "HOdllist")
let create_absrules_from_tdecl tenv tname =
if (not (!Config.on_the_fly)) && Typename.equal tname tname_HSlist2 then
(* L.out "@[.... Adding Abstraction Rules for Nested Lists ....@\n@."; *)
let para1 = create_hpara_from_tname_flds tenv tname_list name_down [] [] Sil.inst_abstraction in
let para2 = create_hpara_from_tname_flds tenv tname_HSlist2 name_next [name_down] [] Sil.inst_abstraction in
let para_nested = create_hpara_from_tname_twoflds_hpara tenv tname_HSlist2 name_next name_down para1 Sil.inst_abstraction in
let para_nested_base = create_hpara_two_ptsto tname_HSlist2 tenv name_next name_down tname_list name_down Sil.inst_abstraction in
IList.iter abs_rules_add_sll [para_nested_base; para2; para_nested]
else if (not (!Config.on_the_fly)) && Typename.equal tname tname_dllist then
(* L.out "@[.... Adding Abstraction Rules for Doubly-linked Lists ....@\n@."; *)
let para = create_dll_hpara_from_tname_flds tenv tname_dllist name_Flink name_Blink [] [] Sil.inst_abstraction in
abs_rules_add_dll para
else if (not (!Config.on_the_fly)) && Typename.equal tname tname_HOdllist then
(* L.out "@[.... Adding Abstraction Rules for High-Order Doubly-linked Lists ....@\n@."; *)
let para1 = create_hpara_from_tname_flds tenv tname_list name_down [] [] Sil.inst_abstraction in
let para2 = create_dll_hpara_from_tname_flds tenv tname_HOdllist name_Flink name_Blink [name_down] [] Sil.inst_abstraction in
let para_nested = create_hpara_dll_from_tname_twoflds_hpara tenv tname_HOdllist name_Flink name_Blink name_down para1 Sil.inst_abstraction in
let para_nested_base = create_hpara_dll_two_ptsto tenv tname_HOdllist name_Flink name_Blink name_down tname_list name_down Sil.inst_abstraction in
IList.iter abs_rules_add_dll [para_nested_base; para2; para_nested]
else if (not (!Config.on_the_fly)) then
match is_simply_recursive tenv tname with
| None -> ()
| Some (fld) ->
(* L.out "@[.... Adding Abstraction Rules ....@\n@."; *)
let para = create_hpara_from_tname_flds tenv tname fld [] [] Sil.inst_abstraction in
abs_rules_add_sll para
else ()
(****************** End of fns that add rules during preprocessing ******************)
(****************** Start of Main Abstraction Functions ******************)
let abstract_pure_part p ~(from_abstract_footprint: bool) =
let do_pure pure =
@ -1446,24 +1263,3 @@ let lifted_abstract pname tenv pset =
abstracted_pset
(***************** End of Main Abstraction Functions *****************)
(*
(** return a reachability function based on whether an id appears in several hpreds *)
let reachable_when_in_several_hpreds sigma : Ident.t -> bool =
(* map id to hpreds in which it occurs *)
let (id_hpred_map : HpredSet.t IdMap.t ref) = ref IdMap.empty in
let add_id_hpred id hpred =
try
let hpred_set = IdMap.find id !id_hpred_map in
id_hpred_map := IdMap.add id (HpredSet.add hpred hpred_set) !id_hpred_map
with
| Not_found -> id_hpred_map := IdMap.add id (HpredSet.singleton hpred) !id_hpred_map in
let add_hpred hpred =
let fav = Sil.fav_new () in
Sil.hpred_fav_add fav hpred;
IList.iter (fun id -> add_id_hpred id hpred) (Sil.fav_to_list fav) in
let id_in_several_hpreds id =
HpredSet.cardinal (IdMap.find id !id_hpred_map) > 1 in
IList.iter add_hpred sigma;
id_in_several_hpreds
*)

32
infer/src/backend/abs.mli
Unescape View File

@ -10,26 +10,34 @@
(** Implementation of Abstraction Functions *)
(** Create abstraction rules from the definition of a type *)
val create_absrules_from_tdecl : Sil.tenv -> Typename.t -> unit
(** Check whether the prop contains junk.
If it does, and [Config.allowleak] is true, remove the junk, otherwise raise a Leak exception. *)
val abstract_junk : ?original_prop:Prop.normal Prop.t -> Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Remove redundant elements in an array, and check for junk afterwards *)
val remove_redundant_array_elements :
Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Abstraction rules discovered *)
type rules
(** Abstract a proposition. *)
val abstract : Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Check whether the prop contains junk.
If it does, and [Config.allowleak] is true, remove the junk,
otherwise raise a Leak exception. *)
val abstract_junk :
?original_prop:Prop.normal Prop.t ->
Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Abstract a proposition but don't pay a SymOp *)
val abstract_no_symop : Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Get the current rules discoveres *)
val get_current_rules : unit -> rules
(** Abstract each proposition in [propset] *)
val lifted_abstract : Procname.t -> Sil.tenv -> Propset.t -> Propset.t
val abs_rules_reset : unit -> unit
(** Remove redundant elements in an array, and check for junk afterwards *)
val remove_redundant_array_elements :
Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Reset the abstraction rules discovered *)
val reset_current_rules : unit -> unit
val get_cycle : Sil.hpred -> Prop.normal Prop.t -> ((Sil.strexp * Sil.typ) * Ident.fieldname * Sil.strexp) list
(** Set the current rules discovered *)
val set_current_rules : rules -> unit

19
infer/src/backend/config.ml
Unescape View File

@ -134,7 +134,12 @@ let abs_struct = ref 1
1 = evaluate all expressions abstractly.
2 = 1 + abstract constant integer values during join.
*)
let abs_val = ref 2
let abs_val_default = 2
let abs_val =
ref abs_val_default
let reset_abs_val () =
abs_val := abs_val_default
(** if true, completely ignore the possibility that errors can be caused by unknown procedures
* during the symbolic execution phase *)
@ -244,18 +249,9 @@ let nelseg = ref false
(** Flag to activate nonstop mode: the analysis continues after in encounters errors *)
let nonstop = ref false
(** Flag for the on-the-fly predicate discovery *)
let on_the_fly = ref true
(** if true, skip the re-execution phase *)
let only_footprint = ref false
(** flag: only analyze procedures which were analyzed before but have no specs *)
let only_nospecs = ref false
(** flag: only analyze procedures dependent on previous skips which now have a .specs file *)
let only_skips = ref false
(** if true, user simple pretty printing *)
let pp_simple = ref true
@ -268,9 +264,6 @@ let print_using_diff = ref true
(** path of the project results directory *)
let results_dir = ref default_results_dir
(** If not "", only consider functions recursively called by function [!slice_fun] *)
let slice_fun = ref ""
(** Flag to tune the level of abstracting the postconditions of specs discovered
by the footprint analysis.
0 = nothing special.

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

@ -2023,32 +2023,3 @@ let propset_meet_generate_pre pset =
let plist_old = Propset.to_proplist pset in
let plist_new = Propset.to_proplist pset_new in
plist_new @ plist_old
(*
let epset_add e e' set =
match (Sil.exp_compare e e') with
| i when i <= 0 -> EPset.add (e, e') set
| _ -> EPset.add (e', e) set
let run_without_absval f e1 e2 =
let old_abs_val = !Config.abs_val in
let new_abs_val = if old_abs_val = 0 then 0 else 1 in
try
begin
Config.abs_val := new_abs_val;
let e = f e1 e2 in
Config.abs_val := old_abs_val;
e
end
with exn ->
begin
Config.abs_val := old_abs_val;
raise exn
end
let exp_partial_join_without_absval e1 e2 =
run_without_absval exp_partial_join e1 e2
let exp_partial_meet_without_absval e1 e2 =
run_without_absval exp_partial_meet e1 e2
*)

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

@ -348,25 +348,6 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit =
(proc_is_done call_graph) (Cg.get_nonrecursive_dependents call_graph pname) &&
(Specs.get_timestamp (Specs.get_summary_unsafe "main_algorithm" pname) = 0
|| not (proc_is_up_to_date call_graph pname)) in
let filter_out_ondemand pname =
let to_analyze =
if !Config.ondemand_enabled then
try
let cfg = Exe_env.get_cfg exe_env pname in
match Cfg.Procdesc.find_from_name cfg pname with
| Some pdesc ->
let reactive_changed =
if !Config.reactive_mode
then (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.changed
else true in
reactive_changed && (* in reactive mode, only analyze changed procedures *)
Ondemand.procedure_should_be_analyzed pdesc pname
| None ->
true
with Not_found -> true
else
true in
not to_analyze in
let process_one_proc ((pname, _) as elem) =
DB.current_source :=
(Specs.get_summary_unsafe "main_algorithm" pname)
@ -379,15 +360,14 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit =
(Specs.pp_summary pe_text whole_seconds)
(Specs.get_summary_unsafe "main_algorithm" pname)
end;
if filter_out call_graph pname ||
filter_out_ondemand pname
if filter_out exe_env pname
then
post_process_procs exe_env [pname]
else
begin
max_timeout := max (Specs.get_iterations pname) !max_timeout;
Specs.update_dependency_map pname;
process_result exe_env elem (analyze_proc exe_env elem);
process_result exe_env elem (analyze_proc exe_env pname);
end in
while not (WeightedPnameSet.is_empty !G.wpnames_todo) do
begin
@ -413,7 +393,7 @@ type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary
type process_result = Exe_env.t -> WeightedPname.t -> Specs.summary -> unit
type filter_out = Cg.t -> Procname.t -> bool
type filter_out = Exe_env.t -> Procname.t -> bool
(** Execute [analyze_proc] respecting dependencies between procedures,
and apply [process_result] to the result of the analysis.
@ -452,5 +432,4 @@ let interprocedural_algorithm
let exn' = Exceptions.Internal_error (Localise.verbatim_desc err_str) in
Reporting.log_error pname exn';
post_process_procs exe_env [pname] in
main_algorithm
exe_env (fun exe_env (n, _) -> analyze_proc exe_env n) filter_out process_result
main_algorithm exe_env analyze_proc filter_out process_result

2
infer/src/backend/fork.mli
Unescape View File

@ -38,7 +38,7 @@ type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary
type process_result = Exe_env.t -> (Procname.t * Cg.in_out_calls) -> Specs.summary -> unit
type filter_out = Cg.t -> Procname.t -> bool
type filter_out = Exe_env.t -> Procname.t -> bool
(** Execute [analyze_proc] respecting dependencies between procedures,
and apply [process_result] to the result of the analysis.

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

@ -280,16 +280,6 @@ let arg_desc =
Some "n",
"set the max number of procedures in each cluster (default n=2000)"
;
"-only_nospecs",
Arg.Set Config.only_nospecs,
None,
" only analyze procedures which were analyzed before but have no specs"
;
"-only_skips",
Arg.Set Config.only_skips,
None,
" only analyze procedures dependent on previous skips which now have a .specs file"
;
"-seconds_per_iteration",
Arg.Set_int seconds_per_iteration,
Some "n",

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

@ -158,25 +158,25 @@ let path_set_checkout_todo (wl : Worklist.t) (node: Cfg.node) : Paths.PathSet.t
(* =============== END of the edge_set object =============== *)
let collect_do_abstract_pre pname tenv (pset : Propset.t) : Propset.t =
if !Config.footprint then begin
Config.footprint := false;
let pset' = Abs.lifted_abstract pname tenv pset in
Config.footprint := true;
pset'
end
else Abs.lifted_abstract pname tenv pset
if !Config.footprint
then
run_with_footprint_false
(Abs.lifted_abstract pname tenv)
pset
else
Abs.lifted_abstract pname tenv pset
let collect_do_abstract_post pname tenv (pathset : Paths.PathSet.t) : Paths.PathSet.t =
let abs_option p =
if Prover.check_inconsistency p then None
else Some (Abs.abstract pname tenv p) in
if !Config.footprint then begin
Config.footprint := false;
let pathset' = Paths.PathSet.map_option abs_option pathset in
Config.footprint := true;
pathset'
end
else Paths.PathSet.map_option abs_option pathset
if !Config.footprint
then
run_with_footprint_false
(Paths.PathSet.map_option abs_option)
pathset
else
Paths.PathSet.map_option abs_option pathset
let do_join_pre plist =
Dom.proplist_collapse_pre plist
@ -196,12 +196,13 @@ let do_meet_pre pset =
(** Find the preconditions in the current spec table, apply meet then join, and return the joined preconditions *)
let collect_preconditions pname tenv proc_name : Prop.normal Specs.Jprop.t list =
let collect_do_abstract_one tenv prop =
if !Config.footprint then begin
Config.footprint := false;
let prop' = Abs.abstract_no_symop tenv prop in
Config.footprint := true;
prop' end
else Abs.abstract_no_symop tenv prop in
if !Config.footprint
then
run_with_footprint_false
(Abs.abstract_no_symop tenv)
prop
else
Abs.abstract_no_symop tenv prop in
let pres = IList.map (fun spec -> Specs.Jprop.to_prop spec.Specs.pre) (Specs.get_specs proc_name) in
let pset = Propset.from_proplist pres in
let pset' =
@ -969,12 +970,13 @@ let set_current_language proc_desc =
let language = (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.language in
Config.curr_language := language
(** reset counters before analysing a procedure *)
let reset_global_counters proc_desc =
(** reset global values before analysing a procedure *)
let reset_global_values proc_desc =
Config.reset_abs_val ();
Ident.NameGenerator.reset ();
SymOp.reset_total ();
reset_prop_metrics ();
Abs.abs_rules_reset ();
Abs.reset_current_rules ();
set_current_language proc_desc
(* Collect all pairs of the kind (precondition, runtime exception) from a summary *)
@ -1112,7 +1114,7 @@ let analyze_proc exe_env (proc_name: Procname.t) : Specs.summary =
let proc_desc = match Cfg.Procdesc.find_from_name cfg proc_name with
| Some proc_desc -> proc_desc
| None -> assert false in
reset_global_counters proc_desc;
reset_global_values proc_desc;
let go, get_results = perform_analysis_phase cfg tenv proc_name proc_desc in
let res = Fork.Timeout.exe_timeout (Specs.get_iterations proc_name) go () in
let specs, phase = get_results () in
@ -1179,52 +1181,25 @@ let process_result (exe_env: Exe_env.t) (proc_name, calls) (_summ: Specs.summary
let procs_done = Fork.procs_become_done call_graph proc_name in
Fork.post_process_procs exe_env procs_done
(** Return true if the analysis of [proc_name] should be
skipped. Called by the parent process before attempting to analyze a
proc. *)
let filter_out (call_graph: Cg.t) (proc_name: Procname.t) : bool =
if !Config.trace_anal then L.err "===filter_out@.";
let slice_out = (* filter out if slicing is active and [proc_name] not in slice *)
(!Config.slice_fun <> "") &&
(Procname.compare (Procname.from_string_c_fun !Config.slice_fun) proc_name != 0) &&
(Cg.node_defined call_graph proc_name) &&
not (Cg.calls_recursively call_graph (Procname.from_string_c_fun !Config.slice_fun) proc_name) in
slice_out
let check_skipped_procs procs_and_defined_children =
let skipped_procs = ref Procname.Set.empty in
let proc_check_skips (pname, _) =
let process_skip () =
let call_stats =
(Specs.get_summary_unsafe "check_skipped_procs" pname).Specs.stats.Specs.call_stats in
let do_tr_elem pn = function
| Specs.CallStats.CR_skip, _ ->
skipped_procs := Procname.Set.add pn !skipped_procs
| _ -> () in
let do_call (pn, _) (tr: Specs.CallStats.trace) = IList.iter (do_tr_elem pn) tr in
Specs.CallStats.iter do_call call_stats in
if Specs.summary_exists pname then process_skip () in
IList.iter proc_check_skips procs_and_defined_children;
let skipped_procs_with_summary =
Procname.Set.filter Specs.summary_exists !skipped_procs in
skipped_procs_with_summary
(** create a function to filter procedures which were skips but now have a .specs file *)
let filter_skipped_procs cg procs_and_defined_children =
let skipped_procs_with_summary = check_skipped_procs procs_and_defined_children in
let filter (pname, _) =
let calls_recurs pn =
let r = try Cg.calls_recursively cg pname pn with Not_found -> false in
L.err "calls recursively %a %a: %b@." Procname.pp pname Procname.pp pn r;
r in
Procname.Set.exists calls_recurs skipped_procs_with_summary in
filter
(** create a function to filter procedures which were analyzed before but had no specs *)
let filter_nospecs (pname, _) =
if Specs.summary_exists pname
then Specs.get_specs pname = []
else false
let filter_out_ondemand exe_env proc_name =
let to_analyze =
if !Config.ondemand_enabled then
try
let cfg = Exe_env.get_cfg exe_env proc_name in
match Cfg.Procdesc.find_from_name cfg proc_name with
| Some pdesc ->
let reactive_changed =
if !Config.reactive_mode
then (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.changed
else true in
reactive_changed && (* in reactive mode, only analyze changed procedures *)
Ondemand.procedure_should_be_analyzed pdesc proc_name
| None ->
true
with Not_found -> true
else
true in
not to_analyze
(** Perform the analysis of an exe_env *)
let do_analysis exe_env =
@ -1248,22 +1223,15 @@ let do_analysis exe_env =
let attributes =
{ (Cfg.Procdesc.get_attributes pdesc) with
ProcAttributes.err_log = static_err_log; } in
Specs.init_summary (dep, nodes, proc_flags, calls, None, attributes) in
Specs.init_summary
(dep, nodes, proc_flags,
calls, None, attributes) in
let filter =
if !Config.only_skips then (filter_skipped_procs cg procs_and_defined_children)
else if !Config.only_nospecs then filter_nospecs
else (fun _ -> true) in
IList.iter
(fun ((pn, _) as x) ->
let should_init () =
Config.analyze_models ||
not !Config.ondemand_enabled ||
Specs.get_summary pn = None in
if filter x &&
should_init ()
if should_init ()
then init_proc x)
procs_and_defined_children;
@ -1287,7 +1255,7 @@ let do_analysis exe_env =
{ Ondemand.analyze_ondemand; get_proc_desc; } in
Ondemand.set_callbacks callbacks;
Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out;
Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out_ondemand;
Ondemand.unset_callbacks ()

15
infer/src/backend/interproc.mli
Unescape View File

@ -10,21 +10,6 @@
(** Interprocedural Analysis *)
(** Analyze [proc_name] and return the updated summary. Use module
{!Timeout } to call {!perform_analysis_phase } with a time limit, and
then return the updated summary. Executed as a child process. *)
val analyze_proc : Exe_env.t -> Procname.t -> Specs.summary
(** Process the result of the analysis of [proc_name]: update the
returned summary and add it to the spec table. Executed in the
parent process as soon as a child process returns a result. *)
val process_result : Exe_env.t -> (Procname.t * Cg.in_out_calls) -> Specs.summary -> unit
(** Return true if the analysis of [proc_name] should be
skipped. Called by the parent process before attempting to analyze a
proc. *)
val filter_out : Cg.t -> Procname.t -> bool
(** Perform the analysis of an exe_env *)
val do_analysis : Exe_env.t -> unit

6
infer/src/backend/ondemand.ml
Unescape View File

@ -87,6 +87,8 @@ let procedure_should_be_analyzed curr_pdesc proc_name =
type global_state =
{
abs_val : int;
abstraction_rules : Abs.rules;
current_source : DB.source_file;
delayed_prints : L.print_action list;
footprint_mode : bool;
@ -97,6 +99,8 @@ type global_state =
let save_global_state () =
{
abs_val = !Config.abs_val;
abstraction_rules = Abs.get_current_rules ();
current_source = !DB.current_source;
delayed_prints = L.get_delayed_prints ();
footprint_mode = !Config.footprint;
@ -106,6 +110,8 @@ let save_global_state () =
}
let restore_global_state st =
Config.abs_val := st.abs_val;
Abs.set_current_rules st.abstraction_rules;
DB.current_source := st.current_source;
L.set_delayed_prints st.delayed_prints;
Config.footprint := st.footprint_mode;

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

@ -501,16 +501,6 @@ let check_already_dereferenced pname cond prop =
Reporting.log_warning pname ~pre: pre_opt exn
| None -> ()
let run_with_abs_val_eq_zero f =
let abs_val_old = !Config.abs_val in
Config.abs_val := 0;
let res = try f () with
| exn ->
Config.abs_val := abs_val_old;
raise exn in
Config.abs_val := abs_val_old;
res
(** Check whether symbolic execution de-allocated a stack variable or a constant string, raising an exception in that case *)
let check_deallocate_static_memory prop_after =
let check_deallocated_attribute = function
@ -1204,14 +1194,12 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
| Sil.Declare_locals (ptl, _) ->
let sigma_locals =
let add_None (x, y) = (x, Sil.Sizeof (y, Sil.Subtype.exact), None) in
let fp_mode = !Config.footprint in
Config.footprint := false; (* no footprint vars for locals *)
let sigma_locals =
let sigma_locals () =
IList.map
(Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_initial)
(IList.map add_None ptl) in
Config.footprint := fp_mode;
sigma_locals in
run_with_footprint_false (* 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
ret_old_path [prop']
@ -1598,17 +1586,25 @@ and sym_exec_wrapper handle_exn cfg tenv pdesc instr ((prop: Prop.normal Prop.t)
let curr_node = State.get_node () in
match Cfg.Node.get_kind curr_node with
| Cfg.Node.Prune_node _ when not (node_has_abstraction curr_node) ->
(* don't check for leaks in prune nodes, unless there is abstraction anyway, but force them into either branch *)
(* don't check for leaks in prune nodes, unless there is abstraction anyway,*)
(* but force them into either branch *)
p'
| _ ->
check_deallocate_static_memory (Abs.abstract_junk ~original_prop: p pname tenv p') in
L.d_str "Instruction "; Sil.d_instr instr; L.d_ln ();
let prop', fav_normal = pre_process_prop prop in
let res_list = run_with_abs_val_eq_zero (* no exp abstraction during sym exe *)
(fun () ->
sym_exec cfg tenv pdesc instr prop' path) in
let res_list_nojunk = IList.map (fun (p, path) -> (post_process_result fav_normal p path, path)) res_list in
let results = IList.map (fun (p, path) -> (Prop.prop_rename_primed_footprint_vars p, path)) res_list_nojunk in
let res_list =
run_with_abs_val_equal_zero (* no exp abstraction during sym exe *)
(fun () -> sym_exec cfg tenv pdesc instr prop' path)
() in
let res_list_nojunk =
IList.map
(fun (p, path) -> (post_process_result fav_normal p path, path))
res_list in
let results =
IList.map
(fun (p, path) -> (Prop.prop_rename_primed_footprint_vars p, path))
res_list_nojunk in
L.d_strln "Instruction Returns";
Propgraph.d_proplist prop (IList.map fst results); L.d_ln ();
State.mark_instr_ok ();
@ -1616,8 +1612,11 @@ and sym_exec_wrapper handle_exn cfg tenv pdesc instr ((prop: Prop.normal Prop.t)
with exn when Exceptions.handle_exception exn && !Config.footprint ->
handle_exn exn; (* calls State.mark_instr_fail *)
if !Config.nonstop
then (Paths.PathSet.from_renamed_list [(prop, path)]) (* in nonstop mode treat the instruction as skip *)
else Paths.PathSet.empty
then
(* in nonstop mode treat the instruction as skip *)
(Paths.PathSet.from_renamed_list [(prop, path)])
else
Paths.PathSet.empty
(** {2 Lifted Abstract Transfer Functions} *)

25
infer/src/backend/utils.ml
Unescape View File

@ -757,11 +757,6 @@ let reserved_arg_desc =
Some "n",
"set right margin for the pretty printing functions"
;
"-slice_fun",
Arg.Set_string Config.slice_fun,
None,
"analyze only functions recursively called by function given as argument"
;
"-spec_abs_level",
Arg.Set_int Config.spec_abs_level,
Some "n",
@ -981,3 +976,23 @@ let string_append_crc_cutoff ?(cutoff=100) ?(key="") name =
let name_for_crc = name ^ key in
string_crc_hex32 name_for_crc in
name_up_to_cutoff ^ "." ^ crc_str
let run_with_val reference value f x =
let saved = !reference in
let restore () =
reference := saved in
try
reference := value;
let res = f x in
restore ();
res
with
| exn ->
restore ();
raise exn
let run_with_footprint_false f x =
run_with_val Config.footprint false f x
let run_with_abs_val_equal_zero f x =
run_with_val Config.abs_val 0 f x

8
infer/src/backend/utils.mli
Unescape View File

@ -367,3 +367,11 @@ val analyzers: analyzer list
val string_of_analyzer: analyzer -> string
val analyzer_of_string: string -> analyzer
(** Call f x with Config.footprint set to false.
Restore the initial value of footprint also in case of exception. *)
val run_with_footprint_false : ('a -> 'b) -> 'a -> 'b
(** Call f x with Config.abs_val set to zero.
Restore the initial value also in case of exception. *)
val run_with_abs_val_equal_zero : ('a -> 'b) -> 'a -> 'b

Write Preview
Loading…
Cancel
Save