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

one instance of SummaryReporting gone

Browse Source 
Summary:
By far the most annoying thing to migrate. There will be a bunch of
these diffs.

Reviewed By: dulmarod

Differential Revision: D21261635

fbshipit-source-id: 0f290dd96
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent 616a534a44
commit 540a2a7749
4 changed files with 66 additions and 60 deletions
Show Stats Download Patch File Download Diff File

38
infer/src/biabduction/Abs.ml
Unescape View File

@ -1006,7 +1006,7 @@ let check_observer_is_unsubscribed_deallocation tenv prop e =
() ()
let check_junk pname tenv prop = let check_junk {InterproceduralAnalysis.proc_desc; err_log; tenv} prop =
let leaks_reported = ref [] in let leaks_reported = ref [] in
let remove_junk_once fp_part fav_root sigma = let remove_junk_once fp_part fav_root sigma =
let id_considered_reachable = let id_considered_reachable =
@ -1138,7 +1138,9 @@ let check_junk pname tenv prop =
let report_leak () = let report_leak () =
if not report_and_continue then raise exn if not report_and_continue then raise exn
else ( else (
SummaryReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ; BiabductionReporting.log_issue_deprecated_using_state
(Procdesc.get_attributes proc_desc)
err_log Exceptions.Error exn ;
leaks_reported := alloc_attribute :: !leaks_reported ) leaks_reported := alloc_attribute :: !leaks_reported )
in in
if not ignore_leak then report_leak () ; if not ignore_leak then report_leak () ;
@ -1254,19 +1256,20 @@ let abstract_spec pname tenv spec =
(** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the (** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the
junk, otherwise raise a Leak exception. *) junk, otherwise raise a Leak exception. *)
let abstract_junk pname tenv prop = let abstract_junk analysis_data prop =
Absarray.array_abstraction_performed := false ; Absarray.array_abstraction_performed := false ;
check_junk pname tenv prop check_junk analysis_data prop
(** Remove redundant elements in an array, and check for junk afterwards *) (** Remove redundant elements in an array, and check for junk afterwards *)
let remove_redundant_array_elements pname tenv prop = let remove_redundant_array_elements ({InterproceduralAnalysis.tenv; _} as analysis_data) prop =
Absarray.array_abstraction_performed := false ; Absarray.array_abstraction_performed := false ;
let prop' = Absarray.remove_redundant_elements tenv prop in let prop' = Absarray.remove_redundant_elements tenv prop in
check_junk pname tenv prop' check_junk analysis_data prop'
let abstract_prop pname tenv ~(rename_primed : bool) ~(from_abstract_footprint : bool) p = let abstract_prop ({InterproceduralAnalysis.tenv; _} as analysis_data) ~(rename_primed : bool)
~(from_abstract_footprint : bool) p =
Absarray.array_abstraction_performed := false ; Absarray.array_abstraction_performed := false ;
let pure_abs_p = abstract_pure_part tenv ~from_abstract_footprint:true p in let pure_abs_p = abstract_pure_part tenv ~from_abstract_footprint:true p in
let array_abs_p = let array_abs_p =
@ -1278,7 +1281,7 @@ let abstract_prop pname tenv ~(rename_primed : bool) ~(from_abstract_footprint :
let abs_p = abs_rules_apply tenv array_abs_p in let abs_p = abs_rules_apply tenv array_abs_p in
let abs_p = abstract_gc tenv abs_p in let abs_p = abstract_gc tenv abs_p in
(* abstraction might enable more gc *) (* abstraction might enable more gc *)
let abs_p = check_junk pname tenv abs_p in let abs_p = check_junk analysis_data abs_p in
let ren_abs_p = let ren_abs_p =
if rename_primed then Prop.prop_rename_primed_footprint_vars tenv abs_p else abs_p if rename_primed then Prop.prop_rename_primed_footprint_vars tenv abs_p else abs_p
in in
@ -1344,29 +1347,30 @@ let set_footprint_for_abs (p : 'a Prop.t) (p_foot : 'a Prop.t) local_stack_pvars
(** Abstract the footprint of prop *) (** Abstract the footprint of prop *)
let abstract_footprint pname (tenv : Tenv.t) (prop : Prop.normal Prop.t) : Prop.normal Prop.t = let abstract_footprint ({InterproceduralAnalysis.tenv; _} as analysis_data)
(prop : Prop.normal Prop.t) : Prop.normal Prop.t =
let p, added_local_vars = extract_footprint_for_abs prop in let p, added_local_vars = extract_footprint_for_abs prop in
let p_abs = let p_abs =
abstract_prop pname tenv ~rename_primed:false ~from_abstract_footprint:true abstract_prop analysis_data ~rename_primed:false ~from_abstract_footprint:true
(Prop.normalize tenv p) (Prop.normalize tenv p)
in in
let prop' = set_footprint_for_abs prop p_abs added_local_vars in let prop' = set_footprint_for_abs prop p_abs added_local_vars in
Prop.normalize tenv prop' Prop.normalize tenv prop'
let abstract_ pname pay tenv p = let abstract_ analysis_data pay p =
if pay then SymOp.pay () ; if pay then SymOp.pay () ;
(* pay one symop *) (* pay one symop *)
let p' = if !BiabductionConfig.footprint then abstract_footprint pname tenv p else p in let p' = if !BiabductionConfig.footprint then abstract_footprint analysis_data p else p in
abstract_prop pname tenv ~rename_primed:true ~from_abstract_footprint:false p' abstract_prop analysis_data ~rename_primed:true ~from_abstract_footprint:false p'
let abstract pname tenv p = abstract_ pname true tenv p let abstract analysis_data p = abstract_ analysis_data true p
let abstract_no_symop pname tenv p = abstract_ pname false tenv p let abstract_no_symop analysis_data p = abstract_ analysis_data false p
let lifted_abstract pname tenv pset = let lifted_abstract ({InterproceduralAnalysis.tenv; _} as analysis_data) pset =
let f p = if Prover.check_inconsistency tenv p then None else Some (abstract pname tenv p) in let f p = if Prover.check_inconsistency tenv p then None else Some (abstract analysis_data p) in
let abstracted_pset = Propset.map_option tenv f pset in let abstracted_pset = Propset.map_option tenv f pset in
abstracted_pset abstracted_pset

13
infer/src/biabduction/Abs.mli
Unescape View File

@ -13,7 +13,8 @@ open! IStd
(** Abstraction rules discovered *) (** Abstraction rules discovered *)
type rules type rules
val abstract : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t val abstract :
BiabductionSummary.t InterproceduralAnalysis.t -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Abstract a proposition. *) (** Abstract a proposition. *)
val abstract_spec : val abstract_spec :
@ -21,21 +22,23 @@ val abstract_spec :
(** Normalizes names and applies simplifications, soem of which require looking at both pre and (** Normalizes names and applies simplifications, soem of which require looking at both pre and
post. *) post. *)
val abstract_junk : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t val abstract_junk :
BiabductionSummary.t InterproceduralAnalysis.t -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the (** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the
junk, otherwise raise a Leak exception. *) junk, otherwise raise a Leak exception. *)
val abstract_no_symop : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t val abstract_no_symop :
BiabductionSummary.t InterproceduralAnalysis.t -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Abstract a proposition but don't pay a SymOp *) (** Abstract a proposition but don't pay a SymOp *)
val get_current_rules : unit -> rules val get_current_rules : unit -> rules
(** Get the current rules discoveres *) (** Get the current rules discoveres *)
val lifted_abstract : Procname.t -> Tenv.t -> Propset.t -> Propset.t val lifted_abstract : BiabductionSummary.t InterproceduralAnalysis.t -> Propset.t -> Propset.t
(** Abstract each proposition in [propset] *) (** Abstract each proposition in [propset] *)
val remove_redundant_array_elements : val remove_redundant_array_elements :
Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t BiabductionSummary.t InterproceduralAnalysis.t -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Remove redundant elements in an array, and check for junk afterwards *) (** Remove redundant elements in an array, and check for junk afterwards *)
val reset_current_rules : unit -> unit val reset_current_rules : unit -> unit

10
infer/src/biabduction/SymExec.ml
Unescape View File

@ -1455,8 +1455,7 @@ let rec sym_exec
if Prover.check_inconsistency tenv prop_ then ret_old_path [] if Prover.check_inconsistency tenv prop_ then ret_old_path []
else else
ret_old_path ret_old_path
[ Abs.remove_redundant_array_elements current_pname tenv [Abs.remove_redundant_array_elements analysis_data (Abs.abstract analysis_data prop_)]
(Abs.abstract current_pname tenv prop_) ]
| Sil.Metadata (ExitScope (dead_vars, _)) -> | Sil.Metadata (ExitScope (dead_vars, _)) ->
let dead_ids = List.filter_map dead_vars ~f:Var.get_ident in let dead_ids = List.filter_map dead_vars ~f:Var.get_ident in
ret_old_path [Prop.exist_quantify tenv dead_ids prop_] ret_old_path [Prop.exist_quantify tenv dead_ids prop_]
@ -1854,9 +1853,8 @@ and proc_call (callee_pdesc, callee_summary)
(** perform symbolic execution for a single prop, and check for junk *) (** perform symbolic execution for a single prop, and check for junk *)
and sym_exec_wrapper ({InterproceduralAnalysis.tenv; _} as analysis_data) handle_exn proc_cfg instr and sym_exec_wrapper ({InterproceduralAnalysis.tenv; _} as analysis_data) handle_exn instr
((prop : Prop.normal Prop.t), path) : Paths.PathSet.t = ((prop : Prop.normal Prop.t), path) : Paths.PathSet.t =
let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
let prop_primed_to_normal p = let prop_primed_to_normal p =
(* Rename primed vars with fresh normal vars, and return them *) (* Rename primed vars with fresh normal vars, and return them *)
let ids_primed = let ids_primed =
@ -1912,7 +1910,7 @@ and sym_exec_wrapper ({InterproceduralAnalysis.tenv; _} as analysis_data) handle
(* but force them into either branch *) (* but force them into either branch *)
p' p'
| _ -> | _ ->
check_deallocate_static_memory (Abs.abstract_junk pname tenv p') check_deallocate_static_memory (Abs.abstract_junk analysis_data p')
in in
L.d_str "Instruction " ; L.d_str "Instruction " ;
Sil.d_instr instr ; Sil.d_instr instr ;
@ -1966,7 +1964,7 @@ let node handle_exn analysis_data proc_cfg (node : ProcCfg.Exceptional.Node.t)
Sil.d_instr instr ; Sil.d_instr instr ;
L.d_strln " due to exception" ; L.d_strln " due to exception" ;
Paths.PathSet.from_renamed_list [(p, tr)] ) Paths.PathSet.from_renamed_list [(p, tr)] )
else sym_exec_wrapper analysis_data handle_exn proc_cfg instr (p, tr) else sym_exec_wrapper analysis_data handle_exn instr (p, tr)
in in
Paths.PathSet.union pset2 pset1 Paths.PathSet.union pset2 pset1
in in

65
infer/src/biabduction/interproc.ml
Unescape View File

@ -166,19 +166,20 @@ let path_set_checkout_todo (wl : Worklist.t) (node : Procdesc.Node.t) : Paths.Pa
(* =============== END of the edge_set object =============== *) (* =============== END of the edge_set object =============== *)
let collect_do_abstract_pre pname tenv (pset : Propset.t) : Propset.t = let collect_do_abstract_pre analysis_data (pset : Propset.t) : Propset.t =
if !BiabductionConfig.footprint then if !BiabductionConfig.footprint then
BiabductionConfig.run_in_re_execution_mode (Abs.lifted_abstract pname tenv) pset BiabductionConfig.run_in_re_execution_mode (Abs.lifted_abstract analysis_data) pset
else Abs.lifted_abstract pname tenv pset else Abs.lifted_abstract analysis_data pset
let collect_do_abstract_post pname tenv (pathset : Paths.PathSet.t) : Paths.PathSet.t = let collect_do_abstract_post ({InterproceduralAnalysis.tenv; _} as analysis_data)
(pathset : Paths.PathSet.t) : Paths.PathSet.t =
if !BiabductionConfig.footprint then if !BiabductionConfig.footprint then
L.die InternalError L.die InternalError
"Interproc.collect_do_abstract_post ignores the _fp part of propositions, so it should only \ "Interproc.collect_do_abstract_post ignores the _fp part of propositions, so it should only \
be used during re-execution." ; be used during re-execution." ;
let abstract_o p = let abstract_o p =
if Prover.check_inconsistency tenv p then None else Some (Abs.abstract pname tenv p) if Prover.check_inconsistency tenv p then None else Some (Abs.abstract analysis_data p)
in in
Paths.PathSet.map_option abstract_o pathset Paths.PathSet.map_option abstract_o pathset
@ -192,7 +193,8 @@ let do_meet_pre tenv pset =
(** Find the preconditions in the current spec table, apply meet then join, and return the joined (** Find the preconditions in the current spec table, apply meet then join, and return the joined
preconditions *) preconditions *)
let collect_preconditions proc_name tenv summary : Prop.normal BiabductionSummary.Jprop.t list = let collect_preconditions ({InterproceduralAnalysis.tenv; _} as analysis_data) summary :
Prop.normal BiabductionSummary.Jprop.t list =
let collect_do_abstract_one tenv prop = let collect_do_abstract_one tenv prop =
if !BiabductionConfig.footprint then if !BiabductionConfig.footprint then
BiabductionConfig.run_in_re_execution_mode (Abs.abstract_no_symop tenv) prop BiabductionConfig.run_in_re_execution_mode (Abs.abstract_no_symop tenv) prop
@ -208,15 +210,15 @@ let collect_preconditions proc_name tenv summary : Prop.normal BiabductionSummar
let f p = Prop.prop_normal_vars_to_primed_vars tenv p in let f p = Prop.prop_normal_vars_to_primed_vars tenv p in
Propset.map tenv f pset Propset.map tenv f pset
in in
L.d_printfln "#### Extracted footprint of %a: ####" Procname.pp proc_name ; L.d_printfln "#### Extracted footprint ####" ;
L.d_increase_indent () ; L.d_increase_indent () ;
Propset.d Prop.prop_emp pset' ; Propset.d Prop.prop_emp pset' ;
L.d_decrease_indent () ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_ln () ; L.d_ln () ;
let pset'' = collect_do_abstract_pre proc_name tenv pset' in let pset'' = collect_do_abstract_pre analysis_data pset' in
let plist_meet = do_meet_pre tenv pset'' in let plist_meet = do_meet_pre tenv pset'' in
L.d_printfln "#### Footprint of %a after Meet ####" Procname.pp proc_name ; L.d_printfln "#### Footprint after Meet ####" ;
L.d_increase_indent () ; L.d_increase_indent () ;
Propgraph.d_proplist Prop.prop_emp plist_meet ; Propgraph.d_proplist Prop.prop_emp plist_meet ;
L.d_decrease_indent () ; L.d_decrease_indent () ;
@ -227,7 +229,7 @@ let collect_preconditions proc_name tenv summary : Prop.normal BiabductionSummar
let jplist = do_join_pre tenv plist_meet in let jplist = do_join_pre tenv plist_meet in
L.d_decrease_indent () ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_printfln "#### Footprint of %a after Join ####" Procname.pp proc_name ; L.d_printfln "#### Footprint after Join ####" ;
L.d_increase_indent () ; L.d_increase_indent () ;
BiabductionSummary.Jprop.d_list ~shallow:false jplist ; BiabductionSummary.Jprop.d_list ~shallow:false jplist ;
L.d_decrease_indent () ; L.d_decrease_indent () ;
@ -235,18 +237,16 @@ let collect_preconditions proc_name tenv summary : Prop.normal BiabductionSummar
let jplist' = let jplist' =
List.map ~f:(BiabductionSummary.Jprop.map (Prop.prop_rename_primed_footprint_vars tenv)) jplist List.map ~f:(BiabductionSummary.Jprop.map (Prop.prop_rename_primed_footprint_vars tenv)) jplist
in in
L.d_printfln "#### Renamed footprint of %a: ####" Procname.pp proc_name ; L.d_printfln "#### Renamed footprint ####" ;
L.d_increase_indent () ; L.d_increase_indent () ;
BiabductionSummary.Jprop.d_list ~shallow:false jplist' ; BiabductionSummary.Jprop.d_list ~shallow:false jplist' ;
L.d_decrease_indent () ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
let jplist'' = let jplist'' =
let f p = let f p = Prop.prop_primed_vars_to_normal_vars tenv (collect_do_abstract_one analysis_data p) in
Prop.prop_primed_vars_to_normal_vars tenv (collect_do_abstract_one proc_name tenv p)
in
List.map ~f:(BiabductionSummary.Jprop.map f) jplist' List.map ~f:(BiabductionSummary.Jprop.map f) jplist'
in in
L.d_printfln "#### Abstracted footprint of %a: ####" Procname.pp proc_name ; L.d_printfln "#### Abstracted footprint ####" ;
L.d_increase_indent () ; L.d_increase_indent () ;
BiabductionSummary.Jprop.d_list ~shallow:false jplist'' ; BiabductionSummary.Jprop.d_list ~shallow:false jplist'' ;
L.d_decrease_indent () ; L.d_decrease_indent () ;
@ -274,8 +274,8 @@ let propagate (wl : Worklist.t) pname ~is_exception (pset : Paths.PathSet.t)
(** propagate a set of results, including exceptions and divergence *) (** propagate a set of results, including exceptions and divergence *)
let propagate_nodes_divergence tenv (proc_cfg : ProcCfg.Exceptional.t) (pset : Paths.PathSet.t) let propagate_nodes_divergence ({InterproceduralAnalysis.tenv; _} as analysis_data)
curr_node (wl : Worklist.t) = (proc_cfg : ProcCfg.Exceptional.t) (pset : Paths.PathSet.t) curr_node (wl : Worklist.t) =
let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in
if if
@ -287,7 +287,7 @@ let propagate_nodes_divergence tenv (proc_cfg : ProcCfg.Exceptional.t) (pset : P
let diverging_states = State.get_diverging_states_node () in let diverging_states = State.get_diverging_states_node () in
let prop_incons = let prop_incons =
let mk_incons prop = let mk_incons prop =
let p_abs = Abs.abstract pname tenv prop in let p_abs = Abs.abstract analysis_data prop in
let p_zero = Prop.set p_abs ~sub:Predicates.sub_empty ~sigma:[] in let p_zero = Prop.set p_abs ~sub:Predicates.sub_empty ~sigma:[] in
Prop.normalize tenv (Prop.set p_zero ~pi:[Predicates.Aneq (Exp.zero, Exp.zero)]) Prop.normalize tenv (Prop.set p_zero ~pi:[Predicates.Aneq (Exp.zero, Exp.zero)])
in in
@ -391,7 +391,7 @@ let forward_tabulate ({InterproceduralAnalysis.tenv; _} as analysis_data) proc_c
Exceptions.print_exception_html "Failure of symbolic execution: " exn ; Exceptions.print_exception_html "Failure of symbolic execution: " exn ;
let pre_opt = let pre_opt =
(* precondition leading to error, if any *) (* precondition leading to error, if any *)
State.get_normalized_pre (Abs.abstract_no_symop pname) State.get_normalized_pre (fun _tenv -> Abs.abstract_no_symop analysis_data)
in in
( match pre_opt with ( match pre_opt with
| Some pre -> | Some pre ->
@ -433,7 +433,7 @@ let forward_tabulate ({InterproceduralAnalysis.tenv; _} as analysis_data) proc_c
try try
State.reset_diverging_states_node () ; State.reset_diverging_states_node () ;
let pset = do_symbolic_execution analysis_data proc_cfg handle_exn curr_node prop path in let pset = do_symbolic_execution analysis_data proc_cfg handle_exn curr_node prop path in
propagate_nodes_divergence tenv proc_cfg pset curr_node wl ; propagate_nodes_divergence analysis_data proc_cfg pset curr_node wl ;
L.d_decrease_indent () ; L.d_decrease_indent () ;
L.d_ln () L.d_ln ()
with exn -> with exn ->
@ -528,7 +528,7 @@ let compute_visited vset =
(* Extract specs from a pathset, after the footprint phase. The postconditions will be thrown away (* Extract specs from a pathset, after the footprint phase. The postconditions will be thrown away
by the re-execution phase, but they are first used to detect custom errors. *) by the re-execution phase, but they are first used to detect custom errors. *)
let extract_specs tenv pdesc pathset : Prop.normal BiabductionSummary.spec list = let extract_specs analysis_data tenv pdesc pathset : Prop.normal BiabductionSummary.spec list =
if not !BiabductionConfig.footprint then if not !BiabductionConfig.footprint then
L.die InternalError L.die InternalError
"Interproc.extract_specs should not be used for footprint but not for re-execution, because \ "Interproc.extract_specs should not be used for footprint but not for re-execution, because \
@ -546,7 +546,7 @@ let extract_specs tenv pdesc pathset : Prop.normal BiabductionSummary.spec list
let pre_post_list = let pre_post_list =
let f (prop, path) = let f (prop, path) =
let _remaining, prop = PropUtil.remove_locals_formals tenv pdesc prop in let _remaining, prop = PropUtil.remove_locals_formals tenv pdesc prop in
let prop = Abs.abstract (Procdesc.get_proc_name pdesc) tenv prop in let prop = Abs.abstract analysis_data prop in
let pre, post = Prop.extract_spec prop in let pre, post = Prop.extract_spec prop in
let pre = Prop.normalize tenv (Prop.prop_sub sub pre) in let pre = Prop.normalize tenv (Prop.prop_sub sub pre) in
let post = PropUtil.remove_seed_vars tenv (Prop.prop_sub sub post) in let post = PropUtil.remove_seed_vars tenv (Prop.prop_sub sub post) in
@ -574,7 +574,8 @@ let extract_specs tenv pdesc pathset : Prop.normal BiabductionSummary.spec list
List.map ~f:mk_spec pre_post_list List.map ~f:mk_spec pre_post_list
let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * BiabductionSummary.Visitedset.t = let collect_postconditions analysis_data wl tenv proc_cfg :
Paths.PathSet.t * BiabductionSummary.Visitedset.t =
let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
let pathset = collect_analysis_result tenv wl proc_cfg in let pathset = collect_analysis_result tenv wl proc_cfg in
(* Assuming C++ developers use RAII, remove resources from the constructor posts *) (* Assuming C++ developers use RAII, remove resources from the constructor posts *)
@ -597,7 +598,7 @@ let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * BiabductionSumma
L.d_ln () ; L.d_ln () ;
let res = let res =
try try
let pathset = collect_do_abstract_post pname tenv pathset in let pathset = collect_do_abstract_post analysis_data pathset in
let pathset_diverging = State.get_diverging_states_proc () in let pathset_diverging = State.get_diverging_states_proc () in
let visited = let visited =
let vset = vset_add_pathset Procdesc.NodeSet.empty pathset in let vset = vset_add_pathset Procdesc.NodeSet.empty pathset in
@ -722,7 +723,7 @@ let execute_filter_prop ({InterproceduralAnalysis.tenv; _} as analysis_data) pro
Prop.d_prop (BiabductionSummary.Jprop.to_prop precondition) ; Prop.d_prop (BiabductionSummary.Jprop.to_prop precondition) ;
L.d_ln () ; L.d_ln () ;
let posts, visited = let posts, visited =
let pset, visited = collect_postconditions wl tenv proc_cfg in let pset, visited = collect_postconditions analysis_data wl tenv proc_cfg in
let plist = let plist =
List.map List.map
~f:(fun (p, path) -> (PropUtil.remove_seed_vars tenv p, path)) ~f:(fun (p, path) -> (PropUtil.remove_seed_vars tenv p, path))
@ -796,7 +797,7 @@ let perform_analysis_phase ({InterproceduralAnalysis.proc_desc; tenv} as analysi
pname ; pname ;
let results = collect_analysis_result tenv wl proc_cfg in let results = collect_analysis_result tenv wl proc_cfg in
let specs = let specs =
try extract_specs tenv (ProcCfg.Exceptional.proc_desc proc_cfg) results try extract_specs analysis_data tenv (ProcCfg.Exceptional.proc_desc proc_cfg) results
with Exceptions.Leak _ -> with Exceptions.Leak _ ->
let exn = let exn =
Exceptions.Internal_error Exceptions.Internal_error
@ -1047,7 +1048,8 @@ let transition_footprint_re_exe summary tenv joined_pres : BiabductionSummary.t
(** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for the procedures enabled after the (** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for the procedures enabled after the
analysis of [proc_name] *) analysis of [proc_name] *)
let perform_transition proc_cfg tenv proc_name summary = let perform_transition ({InterproceduralAnalysis.tenv; _} as analysis_data) proc_cfg proc_name
summary =
let transition summary = let transition summary =
(* disable exceptions for leaks and protect against any other errors *) (* disable exceptions for leaks and protect against any other errors *)
let joined_pres = let joined_pres =
@ -1063,13 +1065,12 @@ let perform_transition proc_cfg tenv proc_name summary =
with_start_node_session ~f:(fun () -> with_start_node_session ~f:(fun () ->
try try
BiabductionConfig.allow_leak := true ; BiabductionConfig.allow_leak := true ;
let res = collect_preconditions proc_name tenv summary in let res = collect_preconditions analysis_data summary in
BiabductionConfig.allow_leak := allow_leak ; BiabductionConfig.allow_leak := allow_leak ;
res res
with exn when SymOp.exn_not_failure exn -> with exn when SymOp.exn_not_failure exn ->
BiabductionConfig.allow_leak := allow_leak ; BiabductionConfig.allow_leak := allow_leak ;
L.(debug Analysis Medium) L.debug Analysis Medium "Error in collect_preconditions for %a@." Procname.pp proc_name ;
"Error in collect_preconditions for %a@." Procname.pp proc_name ;
let error = Exceptions.recognize_exception exn in let error = Exceptions.recognize_exception exn in
let err_str = "exception raised " ^ error.name.IssueType.unique_id in let err_str = "exception raised " ^ error.name.IssueType.unique_id in
L.(debug Analysis Medium) "Error: %s %a@." err_str L.pp_ocaml_pos_opt error.ocaml_pos ; L.(debug Analysis Medium) "Error: %s %a@." err_str L.pp_ocaml_pos_opt error.ocaml_pos ;
@ -1082,13 +1083,13 @@ let perform_transition proc_cfg tenv proc_name summary =
else summary else summary
let analyze_procedure_aux ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) : let analyze_procedure_aux ({InterproceduralAnalysis.proc_desc; _} as analysis_data) :
BiabductionSummary.t = BiabductionSummary.t =
let proc_name = Procdesc.get_proc_name proc_desc in let proc_name = Procdesc.get_proc_name proc_desc in
let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in
let summaryfp = let summaryfp =
BiabductionConfig.run_in_footprint_mode (analyze_proc analysis_data None) proc_cfg BiabductionConfig.run_in_footprint_mode (analyze_proc analysis_data None) proc_cfg
|> perform_transition proc_cfg tenv proc_name |> perform_transition analysis_data proc_cfg proc_name
in in
let summaryre = let summaryre =
BiabductionConfig.run_in_re_execution_mode BiabductionConfig.run_in_re_execution_mode

Write Preview
Loading…
Cancel
Save