From 30d61f4329f87c8bacd2c96978e500940ed2d98c Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 29 Apr 2020 02:59:57 -0700 Subject: [PATCH] Tabulation free of SummaryReporting Summary: more progress Reviewed By: dulmarod Differential Revision: D21261640 fbshipit-source-id: 6fb86ff64 --- infer/src/biabduction/Tabulation.ml | 41 ++++++++++++++++------------- 1 file changed, 23 insertions(+), 18 deletions(-) diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 67550980b..fb7c0a0d3 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -383,7 +383,8 @@ let post_process_sigma tenv (sigma : Predicates.hpred list) loc : Predicates.hpr (** check for interprocedural path errors in the post *) -let check_path_errors_in_post tenv caller_pname post post_path = +let check_path_errors_in_post {InterproceduralAnalysis.proc_desc= caller_pdesc; err_log; tenv} post + post_path = let check_attr atom = match atom with | Predicates.Apred (Adiv0 path_pos, [e]) -> @@ -400,7 +401,9 @@ let check_path_errors_in_post tenv caller_pname post post_path = in State.set_path new_path path_pos_opt ; let exn = Exceptions.Divide_by_zero (desc, __POS__) in - SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning caller_pname exn ) + let attrs = Procdesc.get_attributes caller_pdesc in + BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Warning exn + ) | _ -> () in @@ -409,8 +412,8 @@ let check_path_errors_in_post tenv caller_pname post post_path = (** Post process the instantiated post after the function call so that [x.f |-> se] becomes [x |-> { f: se }]. Also, update any Aresource attributes to refer to the caller *) -let post_process_post tenv caller_pname callee_pname loc actual_pre - ((post : Prop.exposed Prop.t), post_path) = +let post_process_post ({InterproceduralAnalysis.tenv; _} as analysis_data) callee_pname loc + actual_pre ((post : Prop.exposed Prop.t), post_path) = let actual_pre_has_freed_attribute e = match Attribute.get_resource tenv actual_pre e with | Some (Apred (Aresource {ra_kind= Rrelease}, _)) -> @@ -434,7 +437,7 @@ let post_process_post tenv caller_pname callee_pname loc actual_pre let pi' = List.map ~f:atom_update_alloc_attribute prop'.Prop.pi in (* update alloc attributes to refer to the caller *) let post' = Prop.set prop' ~pi:pi' in - check_path_errors_in_post tenv caller_pname post' post_path ; + check_path_errors_in_post analysis_data post' post_path ; (post', post_path) @@ -775,9 +778,8 @@ let include_subtrace callee_pname = (** combine the spec's post with a splitting and actual precondition *) -let combine tenv ret_id (posts : ('a Prop.t * Paths.Path.t) list) actual_pre path_pre split - caller_pdesc callee_pname loc = - let caller_pname = Procdesc.get_proc_name caller_pdesc in +let combine ({InterproceduralAnalysis.proc_desc= caller_pdesc; tenv; _} as analysis_data) ret_id + (posts : ('a Prop.t * Paths.Path.t) list) actual_pre path_pre split callee_pname loc = let instantiated_post = let posts' = if !BiabductionConfig.footprint && List.is_empty posts then @@ -793,8 +795,8 @@ let combine tenv ret_id (posts : ('a Prop.t * Paths.Path.t) list) actual_pre pat in List.map ~f:(fun (p, path) -> - post_process_post tenv caller_pname callee_pname loc actual_pre - (Prop.prop_sub split.sub p, path) ) + post_process_post analysis_data callee_pname loc actual_pre (Prop.prop_sub split.sub p, path) + ) posts' in L.d_increase_indent () ; @@ -878,6 +880,7 @@ let combine tenv ret_id (posts : ('a Prop.t * Paths.Path.t) list) actual_pre pat | Predicates.Hpointsto (_, Eexp (e', inst), _) when exp_is_exn e' -> (* resuls is an exception: set in caller *) let p = Prop.prop_iter_remove_curr_then_to_prop tenv iter' in + let caller_pname = Procdesc.get_proc_name caller_pdesc in prop_set_exn tenv caller_pname p (Eexp (e', inst)) | Predicates.Hpointsto (_, Eexp (e', _), _) -> let p = Prop.prop_iter_remove_curr_then_to_prop tenv iter' in @@ -1070,8 +1073,9 @@ let add_missing_field_to_tenv ~missing_sigma exe_env caller_tenv callee_pname hp (** Perform symbolic execution for a single spec *) -let exe_spec ({InterproceduralAnalysis.exe_env; tenv; _} as analysis_data) ret_id (n, nspecs) - caller_pdesc callee_pname loc prop path_pre (spec : Prop.exposed BiabductionSummary.spec) +let exe_spec + ({InterproceduralAnalysis.exe_env; proc_desc= caller_pdesc; err_log; tenv} as analysis_data) + ret_id (n, nspecs) callee_pname loc prop path_pre (spec : Prop.exposed BiabductionSummary.spec) actual_params formal_params callee_summary : abduction_res = let caller_pname = Procdesc.get_proc_name caller_pdesc in let posts = mk_posts tenv prop callee_pname spec.BiabductionSummary.posts in @@ -1127,14 +1131,15 @@ let exe_spec ({InterproceduralAnalysis.exe_env; tenv; _} as analysis_data) ret_i missing_sigma_objc_class callee_summary ) ; let log_check_exn check = let exn = get_check_exn tenv check callee_pname loc __POS__ in - SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning caller_pname exn + let attrs = Procdesc.get_attributes caller_pdesc in + BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Warning exn in let do_split () = process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_fld missing_fld frame_typ missing_typ in let report_valid_res split = - match combine tenv ret_id posts actual_pre path_pre split caller_pdesc callee_pname loc with + match combine analysis_data ret_id posts actual_pre path_pre split callee_pname loc with | None -> Invalid_res Cannot_combine | Some results -> @@ -1373,8 +1378,8 @@ let exe_call_postprocess tenv ret_id callee_pname callee_attrs loc results = (** Execute the function call and return the list of results with return value *) -let exe_function_call ({InterproceduralAnalysis.proc_desc= caller_pdesc; tenv} as analysis_data) - ~callee_attributes ~callee_pname ~callee_summary ~ret_id loc ~actuals prop path = +let exe_function_call ({InterproceduralAnalysis.tenv; _} as analysis_data) ~callee_attributes + ~callee_pname ~callee_summary ~ret_id loc ~actuals prop path = let spec_list, formal_params = spec_find_rename callee_attributes (BiabductionSummary.get_specs callee_summary) in @@ -1384,8 +1389,8 @@ let exe_function_call ({InterproceduralAnalysis.proc_desc= caller_pdesc; tenv} a Prop.d_prop prop ; L.d_ln () ; let exe_one_spec (n, spec) = - exe_spec analysis_data ret_id (n, nspecs) caller_pdesc callee_pname loc prop path spec actuals - formal_params callee_attributes + exe_spec analysis_data ret_id (n, nspecs) callee_pname loc prop path spec actuals formal_params + callee_attributes in let results = List.map ~f:exe_one_spec spec_list in exe_call_postprocess tenv ret_id callee_pname callee_attributes loc results