From be101b6bb4713f04e0a9d4a92f093e9493cc4c95 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 29 Apr 2020 02:59:05 -0700 Subject: [PATCH] split off parts of State unrelated to biabduction Summary: `State` is used by the AI framework, which isn't supposed to know about biabduction/. Split the biabduction-specific parts into biabduction/State.ml and keep the rest in absint/AnalysisState.ml. Reviewed By: ngorogiannis Differential Revision: D21257470 fbshipit-source-id: e01d1fed3 --- infer/src/absint/AbstractInterpreter.ml | 1 - infer/src/absint/AnalysisState.ml | 60 +++++++++++++++++++ infer/src/absint/AnalysisState.mli | 48 +++++++++++++++ infer/src/absint/exe_env.ml | 4 +- infer/src/backend/errdesc.ml | 18 +++--- infer/src/backend/ondemand.ml | 9 ++- infer/src/biabduction/Abs.ml | 2 +- infer/src/biabduction/BiabductionReporting.ml | 14 +++-- infer/src/biabduction/BuiltinDefn.ml | 2 +- infer/src/biabduction/Prover.ml | 2 +- infer/src/biabduction/Rearrange.ml | 21 ++++--- infer/src/biabduction/RetainCycles.ml | 6 +- infer/src/biabduction/State.ml | 49 +++------------ infer/src/biabduction/State.mli | 27 --------- infer/src/biabduction/SymExec.ml | 17 +++--- infer/src/biabduction/Tabulation.ml | 10 ++-- infer/src/biabduction/Timeout.ml | 2 +- infer/src/biabduction/interproc.ml | 12 ++-- infer/src/nullsafe/eradicate.ml | 4 +- infer/src/nullsafe/eradicateChecks.ml | 2 +- infer/src/nullsafe/typeErr.ml | 2 +- 21 files changed, 185 insertions(+), 127 deletions(-) create mode 100644 infer/src/absint/AnalysisState.ml create mode 100644 infer/src/absint/AnalysisState.mli diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 03f3ec73f..6b4b1df63 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -8,7 +8,6 @@ open! IStd module F = Format module L = Logging -module AnalysisState = State type exec_node_schedule_result = ReachedFixPoint | DidNotReachFixPoint diff --git a/infer/src/absint/AnalysisState.ml b/infer/src/absint/AnalysisState.ml new file mode 100644 index 000000000..7f9b4c7bf --- /dev/null +++ b/infer/src/absint/AnalysisState.ml @@ -0,0 +1,60 @@ +(* + * Copyright (c) 2009-2013, Monoidics ltd. + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +(** State of symbolic execution *) + +type t = + { mutable last_instr: Sil.instr option (** Last instruction seen *) + ; mutable last_node: Procdesc.Node.t option (** Last node seen *) + ; mutable last_session: int (** Last session seen *) } + +let initial () = {last_instr= None; last_node= None; last_session= 0} + +(** Global state *) +let gs = ref (initial ()) + +let get_instr () = !gs.last_instr + +let set_instr instr = !gs.last_instr <- Some instr + +let get_node_exn () = Option.value_exn !gs.last_node + +let get_node () = !gs.last_node + +let set_node (node : Procdesc.Node.t) = + !gs.last_instr <- None ; + !gs.last_node <- Some node + + +let get_session () = !gs.last_session + +let set_session (session : int) = !gs.last_session <- session + +let get_loc_exn () = + match !gs.last_instr with + | Some instr -> + Sil.location_of_instr instr + | None -> + get_node_exn () |> Procdesc.Node.get_loc + + +let get_loc () = + match !gs.last_instr with Some instr -> Some (Sil.location_of_instr instr) | None -> None + + +(** Return the old state, and revert the current state to the initial one. *) +let save () = + let old = !gs in + gs := initial () ; + old + + +(** Restore the old state. *) +let restore st = gs := st diff --git a/infer/src/absint/AnalysisState.mli b/infer/src/absint/AnalysisState.mli new file mode 100644 index 000000000..6aa206f16 --- /dev/null +++ b/infer/src/absint/AnalysisState.mli @@ -0,0 +1,48 @@ +(* + * Copyright (c) 2009-2013, Monoidics ltd. + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +(** State of symbolic execution *) + +type t + +val get_instr : unit -> Sil.instr option +(** Get last instruction seen in symbolic execution *) + +val get_loc_exn : unit -> Location.t +(** Get last location seen in symbolic execution *) + +val get_loc : unit -> Location.t option +(** Get last location seen in symbolic execution *) + +val get_node_exn : unit -> Procdesc.Node.t +(** Get last node seen in symbolic execution *) + +val get_node : unit -> Procdesc.Node.t option +(** Get last node seen in symbolic execution *) + +val get_session : unit -> int +(** Get last session seen in symbolic execution *) + +val set_instr : Sil.instr -> unit +(** Set last instruction seen in symbolic execution *) + +val set_node : Procdesc.Node.t -> unit +(** Set last node seen in symbolic execution *) + +val set_session : int -> unit +(** Set last session seen in symbolic execution *) + +(** {2 State management} *) + +val restore : t -> unit +(** Restore the old state. *) + +val save : unit -> t +(** Return the old state, and revert the current state to the initial one. *) diff --git a/infer/src/absint/exe_env.ml b/infer/src/absint/exe_env.ml index b2c187fb1..0741000d1 100644 --- a/infer/src/absint/exe_env.ml +++ b/infer/src/absint/exe_env.ml @@ -107,11 +107,11 @@ let get_column_value ~value_on_java ~file_data_to_value ~column_name exe_env pro | Some v -> v | None -> - let loc_opt = State.get_loc () in + let loc_opt = AnalysisState.get_loc () in L.die InternalError "get_column_value: %s not found for %a%a" column_name Procname.pp proc_name pp_loc_opt loc_opt ) | None -> - let loc_opt = State.get_loc () in + let loc_opt = AnalysisState.get_loc () in L.die InternalError "get_column_value: file_data not found for %a%a" Procname.pp proc_name pp_loc_opt loc_opt ) diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index cfecb5324..b6e2fa1ae 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -453,9 +453,9 @@ let find_typ_without_ptr prop pvar = variable nullify, blame the variable. If it is an abstraction, blame any variable nullify at the current node. If there is an alloc attribute, print the function call and line number. *) let explain_leak tenv hpred prop alloc_att_opt bucket = - let instro = State.get_instr () in - let loc = State.get_loc_exn () in - let node = State.get_node_exn () in + let instro = AnalysisState.get_instr () in + let loc = AnalysisState.get_loc_exn () in + let node = AnalysisState.get_node_exn () in let node_instrs = Procdesc.Node.get_instrs node in let hpred_typ_opt = find_hpred_typ hpred in let value_str_from_pvars_vpath pvars vpath = @@ -503,7 +503,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = L.d_str "explain_leak: current instruction is Nullify for pvar " ; Pvar.d pvar ; L.d_ln () ) ; - match exp_lv_dexp tenv (State.get_node_exn ()) (Exp.Lvar pvar) with + match exp_lv_dexp tenv (AnalysisState.get_node_exn ()) (Exp.Lvar pvar) with | Some de when not (DExp.has_tmp_var de) -> Some (DExp.to_string de) | _ -> @@ -944,7 +944,7 @@ let explain_access_ proc_name tenv ?(use_buckets = false) ?(outermost_array = fa ?(outermost_dereference = false) ?(is_nullable = false) ?(is_premature_nil = false) deref_str prop loc = let find_exp_dereferenced () = - match State.get_instr () with + match AnalysisState.get_instr () with | Some (Sil.Store {e1= e}) -> if verbose then ( L.d_str "explain_dereference Sil.Store " ; @@ -974,7 +974,7 @@ let explain_access_ proc_name tenv ?(use_buckets = false) ?(outermost_array = fa | _ -> None in - let node = State.get_node_exn () in + let node = AnalysisState.get_node_exn () in match find_exp_dereferenced () with | None -> if verbose then L.d_strln "_explain_access: find_exp_dereferenced returned None" ; @@ -1026,9 +1026,9 @@ let dexp_apply_pvar_off dexp pvar_off = (** Produce a description of the nth parameter of the function call, if the current instruction is a function call with that parameter *) let explain_nth_function_parameter proc_name tenv use_buckets deref_str prop n pvar_off = - let node = State.get_node_exn () in - let loc = State.get_loc_exn () in - match State.get_instr () with + let node = AnalysisState.get_node_exn () in + let loc = AnalysisState.get_loc_exn () in + match AnalysisState.get_instr () with | Some (Sil.Call (_, _, args, _, _)) -> ( try let arg = fst (List.nth_exn args (n - 1)) in diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 17496422f..9d11d2b1a 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -97,7 +97,8 @@ type global_state = ; proc_analysis_time: (Mtime.Span.t * string) option (** the time elapsed doing [status] so far *) ; pulse_address_generator: PulseAbstractValue.State.t - ; symexec_state: State.t } + ; absint_state: AnalysisState.t + ; biabduction_state: State.t } let save_global_state () = Timeout.suspend_existing_timeout ~keep_symop_total:false ; @@ -112,7 +113,8 @@ let save_global_state () = Option.map !current_taskbar_status ~f:(fun (t0, status) -> (Mtime.span t0 (Mtime_clock.now ()), status) ) ; pulse_address_generator= PulseAbstractValue.State.get () - ; symexec_state= State.save_state () } + ; absint_state= AnalysisState.save () + ; biabduction_state= State.save_state () } let restore_global_state st = @@ -123,7 +125,8 @@ let restore_global_state st = Printer.curr_html_formatter := st.html_formatter ; Ident.NameGenerator.set_current st.name_generator ; PulseAbstractValue.State.set st.pulse_address_generator ; - State.restore_state st.symexec_state ; + AnalysisState.restore st.absint_state ; + State.restore_state st.biabduction_state ; current_taskbar_status := Option.map st.proc_analysis_time ~f:(fun (suspended_span, status) -> (* forget about the time spent doing a nested analysis and resend the status of the outer diff --git a/infer/src/biabduction/Abs.ml b/infer/src/biabduction/Abs.ml index 4037710b8..37eba949b 100644 --- a/infer/src/biabduction/Abs.ml +++ b/infer/src/biabduction/Abs.ml @@ -990,7 +990,7 @@ let check_observer_is_unsubscribed_deallocation tenv prop e = | _ -> None in - let loc = State.get_loc_exn () in + let loc = AnalysisState.get_loc_exn () in match Attribute.get_observer tenv prop e with | Some (Apred (Aobserver, _)) -> ( match pvar_opt with diff --git a/infer/src/biabduction/BiabductionReporting.ml b/infer/src/biabduction/BiabductionReporting.ml index 2f0f761ce..98e0a5568 100644 --- a/infer/src/biabduction/BiabductionReporting.ml +++ b/infer/src/biabduction/BiabductionReporting.ml @@ -13,11 +13,11 @@ let log_issue_deprecated_using_state severity proc_name ?node ?loc ?ltr exn = match Summary.OnDisk.get proc_name with | Some summary -> let node = - let node = match node with None -> State.get_node_exn () | Some node -> node in + let node = match node with None -> AnalysisState.get_node_exn () | Some node -> node in Errlog.BackendNode {node} in - let session = State.get_session () in - let loc = match loc with None -> State.get_loc_exn () | Some loc -> loc in + let session = AnalysisState.get_session () in + let loc = match loc with None -> AnalysisState.get_loc_exn () | Some loc -> loc in let ltr = match ltr with None -> State.get_loc_trace () | Some ltr -> ltr in Reporting.log_issue_from_summary severity (Summary.get_attributes summary) summary.Summary.err_log ~node ~session ~loc ~ltr exn @@ -31,11 +31,13 @@ let log_issue_deprecated_using_state severity proc_name ?node ?loc ?ltr exn = let log_error_using_state proc_desc err_log exn = if !BiabductionConfig.footprint then let node' = - match State.get_node () with Some n -> n | None -> Procdesc.get_start_node proc_desc + match AnalysisState.get_node () with Some n -> n | None -> Procdesc.get_start_node proc_desc in let node = Errlog.BackendNode {node= node'} in - let session = State.get_session () in - let loc = match State.get_loc () with Some l -> l | None -> Procdesc.Node.get_loc node' in + let session = AnalysisState.get_session () in + let loc = + match AnalysisState.get_loc () with Some l -> l | None -> Procdesc.Node.get_loc node' + in let ltr = State.get_loc_trace () in let attrs = Procdesc.get_attributes proc_desc in Reporting.log_issue_from_summary Exceptions.Error attrs err_log ~node ~session ~loc ~ltr exn diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index c60af8db7..0c06f660a 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -32,7 +32,7 @@ let mk_empty_array len = Predicates.Earray (len, [], Predicates.inst_none) return a null pointer deref *) let mk_empty_array_rearranged len = Predicates.Earray - (len, [], Predicates.inst_rearrange true (State.get_loc_exn ()) (State.get_path_pos ())) + (len, [], Predicates.inst_rearrange true (AnalysisState.get_loc_exn ()) (State.get_path_pos ())) let extract_array_type typ = diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index 91c81de39..68dd9683c 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -835,7 +835,7 @@ let check_atom tenv prop a0 = if Config.smt_output then ( let key = get_smt_key a prop_no_fp in let key_filename = - let source = (State.get_loc_exn ()).file in + let source = (AnalysisState.get_loc_exn ()).file in DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source) [key ^ ".cns"] in let outc = Out_channel.create (DB.filename_to_string key_filename) in diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index b3aa59bed..cb00fc866 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -136,7 +136,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp | [] -> ([], Predicates.Earray (len, [], inst), t) | Predicates.Off_index e :: off' -> - bounds_check tenv pname orig_prop len e (State.get_loc_exn ()) ; + bounds_check tenv pname orig_prop len e (AnalysisState.get_loc_exn ()) ; let atoms', se', res_t' = create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst in @@ -263,7 +263,7 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp | ( Off_index e :: off' , Predicates.Earray (len, esel, inst_arr) , Tarray {elt= typ'; length= len_for_typ'; stride} ) -> ( - bounds_check tenv pname orig_prop len e (State.get_loc_exn ()) ; + bounds_check tenv pname orig_prop len e (AnalysisState.get_loc_exn ()) ; match List.find ~f:(fun (e', _) -> Exp.equal e e') esel with | Some (_, se') -> let atoms_se_typ_list' = @@ -444,7 +444,7 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst : L.internal_error "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp ; let deref_str = Localise.deref_str_dangling None in let err_desc = - Errdesc.explain_dereference pname tenv deref_str orig_prop (State.get_loc_exn ()) + Errdesc.explain_dereference pname tenv deref_str orig_prop (AnalysisState.get_loc_exn ()) in raise (Exceptions.Dangling_pointer_dereference (false, err_desc, __POS__)) ) ; let off_foot, eqs = laundry_offset_for_footprint max_stamp off in @@ -986,7 +986,7 @@ let check_type_size tenv pname prop texp off typ_from_instr = && not (Prover.check_type_size_leq typ_from_instr typ_of_object) then let deref_str = Localise.deref_str_pointer_size_mismatch typ_from_instr typ_of_object in - let loc = State.get_loc_exn () in + let loc = AnalysisState.get_loc_exn () in let exn = Exceptions.Pointer_size_mismatch (Errdesc.explain_dereference pname tenv deref_str prop loc, __POS__) @@ -1254,7 +1254,9 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc = match attribute_opt with | Some (Apred (Adangling dk, _)) -> let deref_str = Localise.deref_str_dangling (Some dk) in - let err_desc = Errdesc.explain_dereference pname tenv deref_str prop (State.get_loc_exn ()) in + let err_desc = + Errdesc.explain_dereference pname tenv deref_str prop (AnalysisState.get_loc_exn ()) + in raise (Exceptions.Dangling_pointer_dereference (true, err_desc, __POS__)) | Some (Apred (Aundef _, _)) -> () @@ -1294,7 +1296,7 @@ let check_call_to_objc_block_error tenv pdesc prop fun_exp loc = (* when e is a temp var, try to find the pvar defining e*) match e with | Exp.Var id -> ( - match Errdesc.find_ident_assignment (State.get_node_exn ()) id with + match Errdesc.find_ident_assignment (AnalysisState.get_node_exn ()) id with | Some (_, e') -> e' | None -> @@ -1304,9 +1306,9 @@ let check_call_to_objc_block_error tenv pdesc prop fun_exp loc = in let get_exp_called () = (* Exp called in the block's function call*) - match State.get_instr () with + match AnalysisState.get_instr () with | Some (Sil.Call (_, Var id, _, _, _)) -> - Errdesc.find_ident_assignment (State.get_node_exn ()) id + Errdesc.find_ident_assignment (AnalysisState.get_node_exn ()) id | _ -> None in @@ -1384,7 +1386,8 @@ let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc : Prop.d_prop prop ; L.d_ln () ; L.d_ln () ; - if report_deref_errors then check_dereference_error tenv pdesc prop nlexp (State.get_loc_exn ()) ; + if report_deref_errors then + check_dereference_error tenv pdesc prop nlexp (AnalysisState.get_loc_exn ()) ; let pname = Procdesc.get_proc_name pdesc in match Prop.prop_iter_create prop with | None -> diff --git a/infer/src/biabduction/RetainCycles.ml b/infer/src/biabduction/RetainCycles.ml index b137d9625..5b04ff8ae 100644 --- a/infer/src/biabduction/RetainCycles.ml +++ b/infer/src/biabduction/RetainCycles.ml @@ -12,7 +12,7 @@ let desc_retain_cycle tenv (cycle : RetainCyclesType.t) = Logging.d_strln "Proposition with retain cycle:" ; let do_edge index_ edge = let index = index_ + 1 in - let node = State.get_node_exn () in + let node = AnalysisState.get_node_exn () in let from_exp_str edge_obj = let type_str = let typ_str = Typ.to_string edge_obj.rc_from.rc_node_typ in @@ -230,7 +230,9 @@ let exn_retain_cycle tenv cycle = Utils.create_dir rc_dotty_dir ; let rc_dotty_file = Filename.temp_file ~in_dir:rc_dotty_dir "rc" ".dot" in RetainCyclesType.write_dotty_to_file rc_dotty_file cycle ) ; - let desc = Localise.desc_retain_cycle retain_cycle (State.get_loc_exn ()) (Some cycle_dotty) in + let desc = + Localise.desc_retain_cycle retain_cycle (AnalysisState.get_loc_exn ()) (Some cycle_dotty) + in Exceptions.Retain_cycle (desc, __POS__) diff --git a/infer/src/biabduction/State.ml b/infer/src/biabduction/State.ml index 5bda8d791..fbbd34b4e 100644 --- a/infer/src/biabduction/State.ml +++ b/infer/src/biabduction/State.ml @@ -30,22 +30,16 @@ type t = (** Diverging states since the last reset for the node *) ; mutable diverging_states_proc: Paths.PathSet.t (** Diverging states since the last reset for the procedure *) - ; mutable last_instr: Sil.instr option (** Last instruction seen *) - ; mutable last_node: Procdesc.Node.t option (** Last node seen *) ; mutable last_path: (Paths.Path.t * PredSymb.path_pos option) option (** Last path seen *) ; mutable last_prop_tenv_pdesc: (Prop.normal Prop.t * Tenv.t * Procdesc.t) option (** Last prop,tenv,pdesc seen *) - ; mutable last_session: int (** Last session seen *) ; failure_map: failure_stats NodeHash.t (** Map visited nodes to failure statistics *) } let initial () = { diverging_states_node= Paths.PathSet.empty ; diverging_states_proc= Paths.PathSet.empty - ; last_instr= None - ; last_node= None ; last_path= None ; last_prop_tenv_pdesc= None - ; last_session= 0 ; failure_map= NodeHash.create 1 } @@ -83,24 +77,6 @@ let get_diverging_states_node () = !gs.diverging_states_node let get_diverging_states_proc () = !gs.diverging_states_proc -let get_instr () = !gs.last_instr - -let get_node_exn () = Option.value_exn !gs.last_node - -let get_node () = !gs.last_node - -let get_loc_exn () = - match !gs.last_instr with - | Some instr -> - Sil.location_of_instr instr - | None -> - get_node_exn () |> Procdesc.Node.get_loc - - -let get_loc () = - match !gs.last_instr with Some instr -> Some (Sil.location_of_instr instr) | None -> None - - (** normalize the list of instructions by renaming let-bound ids *) let instrs_normalize instrs = let bound_ids = @@ -166,14 +142,14 @@ let mk_find_duplicate_nodes : Procdesc.t -> Procdesc.Node.t -> Procdesc.NodeSet. let get_inst_update pos = - let loc = get_loc_exn () in + let loc = AnalysisState.get_loc_exn () in Predicates.inst_update loc pos let get_path () = match !gs.last_path with | None -> - (Paths.Path.start (get_node_exn ()), None) + (Paths.Path.start (AnalysisState.get_node_exn ()), None) | Some (path, pos_opt) -> (path, pos_opt) @@ -215,8 +191,6 @@ let get_normalized_pre (abstract_fun : Tenv.t -> Prop.normal Prop.t -> Prop.norm Some (extract_pre prop tenv pdesc abstract_fun) -let get_session () = !gs.last_session - let get_path_pos () = let pname = match get_prop_tenv_pdesc () with @@ -225,7 +199,7 @@ let get_path_pos () = | None -> Procname.from_string_c_fun "unknown_procedure" in - let nid = Procdesc.Node.get_id (get_node_exn ()) in + let nid = Procdesc.Node.get_id (AnalysisState.get_node_exn ()) in (pname, (nid :> int)) @@ -244,14 +218,14 @@ let mark_execution_end node = let mark_instr_ok () = - let fs = get_failure_stats (get_node_exn ()) in + let fs = get_failure_stats (AnalysisState.get_node_exn ()) in fs.instr_ok <- fs.instr_ok + 1 let mark_instr_fail exn = - let loc = get_loc_exn () in - let node = get_node_exn () in - let session = get_session () in + let loc = AnalysisState.get_loc_exn () in + let node = AnalysisState.get_node_exn () in + let session = AnalysisState.get_session () in let loc_trace = get_loc_trace () in let fs = get_failure_stats node in if is_none fs.first_failure then @@ -277,15 +251,6 @@ let process_execution_failures (log_issue : log_issue) pname = NodeHash.iter do_failure !gs.failure_map -let set_instr (instr : Sil.instr) = !gs.last_instr <- Some instr - let set_path path pos_opt = !gs.last_path <- Some (path, pos_opt) let set_prop_tenv_pdesc prop tenv pdesc = !gs.last_prop_tenv_pdesc <- Some (prop, tenv, pdesc) - -let set_node (node : Procdesc.Node.t) = - !gs.last_instr <- None ; - !gs.last_node <- Some node - - -let set_session (session : int) = !gs.last_session <- session diff --git a/infer/src/biabduction/State.mli b/infer/src/biabduction/State.mli index 613982605..f0ac66954 100644 --- a/infer/src/biabduction/State.mli +++ b/infer/src/biabduction/State.mli @@ -25,24 +25,9 @@ val get_diverging_states_proc : unit -> Paths.PathSet.t val get_inst_update : PredSymb.path_pos -> Predicates.inst (** Get update instrumentation for the current loc *) -val get_instr : unit -> Sil.instr option -(** Get last instruction seen in symbolic execution *) - -val get_loc_exn : unit -> Location.t -(** Get last location seen in symbolic execution *) - -val get_loc : unit -> Location.t option -(** Get last location seen in symbolic execution *) - val get_loc_trace : unit -> Errlog.loc_trace (** Get the location trace of the last path seen in symbolic execution *) -val get_node_exn : unit -> Procdesc.Node.t -(** Get last node seen in symbolic execution *) - -val get_node : unit -> Procdesc.Node.t option -(** Get last node seen in symbolic execution *) - val get_normalized_pre : (Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t) -> Prop.normal Prop.t option (** return the normalized precondition extracted form the last prop seen, if any the abstraction @@ -57,9 +42,6 @@ val get_path_pos : unit -> PredSymb.path_pos val get_prop_tenv_pdesc : unit -> (Prop.normal Prop.t * Tenv.t * Procdesc.t) option (** Get last last prop,tenv,pdesc seen in symbolic execution *) -val get_session : unit -> int -(** Get last session seen in symbolic execution *) - val mark_execution_end : Procdesc.Node.t -> unit (** Mark the end of symbolic execution of a node *) @@ -94,17 +76,8 @@ val restore_state : t -> unit val save_state : unit -> t (** Return the old state, and revert the current state to the initial one. *) -val set_instr : Sil.instr -> unit -(** Set last instruction seen in symbolic execution *) - -val set_node : Procdesc.Node.t -> unit -(** Set last node seen in symbolic execution *) - val set_path : Paths.Path.t -> PredSymb.path_pos option -> unit (** Get last path seen in symbolic execution *) val set_prop_tenv_pdesc : Prop.normal Prop.t -> Tenv.t -> Procdesc.t -> unit (** Set last prop,tenv,pdesc seen in symbolic execution *) - -val set_session : int -> unit -(** Set last session seen in symbolic execution *) diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 6e6111bda..815f82de4 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -405,7 +405,8 @@ let check_arith_norm_exp tenv pname exp prop = match Attribute.find_arithmetic_problem tenv (State.get_path_pos ()) prop exp with | Some (Attribute.Div0 div), prop' -> let desc = - Errdesc.explain_divide_by_zero tenv div (State.get_node_exn ()) (State.get_loc_exn ()) + Errdesc.explain_divide_by_zero tenv div (AnalysisState.get_node_exn ()) + (AnalysisState.get_loc_exn ()) in let exn = Exceptions.Divide_by_zero (desc, __POS__) in BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ; @@ -413,7 +414,7 @@ let check_arith_norm_exp tenv pname exp prop = | Some (Attribute.UminusUnsigned (e, typ)), prop' -> let desc = Errdesc.explain_unary_minus_applied_to_unsigned_expression tenv e typ - (State.get_node_exn ()) (State.get_loc_exn ()) + (AnalysisState.get_node_exn ()) (AnalysisState.get_loc_exn ()) in let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, __POS__) in BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ; @@ -470,8 +471,8 @@ let check_already_dereferenced tenv pname cond prop = match dereferenced_line with | Some (id, (n, _)) -> let desc = - Errdesc.explain_null_test_after_dereference tenv (Exp.Var id) (State.get_node_exn ()) n - (State.get_loc_exn ()) + Errdesc.explain_null_test_after_dereference tenv (Exp.Var id) + (AnalysisState.get_node_exn ()) n (AnalysisState.get_loc_exn ()) in let exn = Exceptions.Null_test_after_dereference (desc, __POS__) in BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn @@ -1174,7 +1175,7 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t (Prop.normal Prop.t * Paths.Path.t) list = let current_pdesc = Summary.get_proc_desc current_summary in let current_pname = Procdesc.get_proc_name current_pdesc in - State.set_instr instr_ ; + AnalysisState.set_instr instr_ ; (* mark instruction last seen *) State.set_prop_tenv_pdesc prop_ tenv current_pdesc ; (* mark prop,tenv,pdesc last seen *) @@ -1264,7 +1265,7 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t in match Prop.exp_normalize_prop tenv Prop.prop_emp cond with | Exp.Const (Const.Cint i) when report_condition_always_true_false i -> - let node = State.get_node_exn () in + let node = AnalysisState.get_node_exn () in let desc = Errdesc.explain_condition_always_true_false tenv i cond node loc in let exn = Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__) @@ -1824,7 +1825,7 @@ and proc_call exe_env callee_summary | (e, t_e) :: etl', _ :: tl' -> (e, t_e) :: comb etl' tl' | _, [] -> - Errdesc.warning_err (State.get_loc_exn ()) + Errdesc.warning_err (AnalysisState.get_loc_exn ()) "likely use of variable-arguments function, or function prototype missing@." ; L.d_warning "likely use of variable-arguments function, or function prototype missing" ; L.d_ln () ; @@ -1917,7 +1918,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr let instr_is_abstraction = function Sil.Metadata (Abstract _) -> true | _ -> false in Instrs.exists ~f:instr_is_abstraction (ProcCfg.Exceptional.instrs node) in - let curr_node = State.get_node_exn () in + let curr_node = AnalysisState.get_node_exn () in match ProcCfg.Exceptional.Node.kind curr_node with | Procdesc.Node.Prune_node _ when not (node_has_abstraction curr_node) -> (* don't check for leaks in prune nodes, unless there is abstraction anyway,*) diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 5e1858a93..2f725f1d3 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -302,7 +302,8 @@ let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre fo let desc use_buckets deref_str = let error_desc = Errdesc.explain_dereference_as_caller_expression caller_pname tenv ~use_buckets deref_str - actual_pre spec_pre e (State.get_node_exn ()) (State.get_loc_exn ()) formal_params + actual_pre spec_pre e (AnalysisState.get_node_exn ()) (AnalysisState.get_loc_exn ()) + formal_params in L.d_strln ~color:Red "found error in dereference" ; L.d_strln "spec_pre:" ; @@ -392,7 +393,8 @@ let check_path_errors_in_post tenv caller_pname post post_path = | Predicates.Apred (Adiv0 path_pos, [e]) -> if Prover.check_zero tenv e then ( let desc = - Errdesc.explain_divide_by_zero tenv e (State.get_node_exn ()) (State.get_loc_exn ()) + Errdesc.explain_divide_by_zero tenv e (AnalysisState.get_node_exn ()) + (AnalysisState.get_loc_exn ()) in let new_path, path_pos_opt = let current_path, _ = State.get_path () in @@ -989,8 +991,8 @@ let inconsistent_actualpre_missing tenv actual_pre split_opt = let class_cast_exn tenv pname_opt texp1 texp2 exp ml_loc = let desc = - Errdesc.explain_class_cast_exception tenv pname_opt texp1 texp2 exp (State.get_node_exn ()) - (State.get_loc_exn ()) + Errdesc.explain_class_cast_exception tenv pname_opt texp1 texp2 exp + (AnalysisState.get_node_exn ()) (AnalysisState.get_loc_exn ()) in Exceptions.Class_cast_exception (desc, ml_loc) diff --git a/infer/src/biabduction/Timeout.ml b/infer/src/biabduction/Timeout.ml index 39d86f98e..1bfcd1dc6 100644 --- a/infer/src/biabduction/Timeout.ml +++ b/infer/src/biabduction/Timeout.ml @@ -117,6 +117,6 @@ let exe_timeout f x = None ) ~finally:resume_previous_timeout with SymOp.Analysis_failure_exe kind -> - let loc = State.get_loc () |> Option.value ~default:Location.dummy in + let loc = AnalysisState.get_loc () |> Option.value ~default:Location.dummy in Errdesc.warning_err loc "TIMEOUT: %a@." SymOp.pp_failure_kind kind ; Some kind diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 644d7ad39..4cc4f4d54 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -265,7 +265,7 @@ let propagate (wl : Worklist.t) pname ~is_exception (pset : Paths.PathSet.t) let f prop path edgeset_curr = let exn_opt = if is_exception then Tabulation.prop_get_exn_name pname prop else None in Paths.PathSet.add_renamed_prop prop - (Paths.Path.extend curr_node exn_opt (State.get_session ()) path) + (Paths.Path.extend curr_node exn_opt (AnalysisState.get_session ()) path) edgeset_curr in Paths.PathSet.fold f pset Paths.PathSet.empty @@ -283,7 +283,7 @@ let propagate_nodes_divergence tenv (proc_cfg : ProcCfg.Exceptional.t) (pset : P !BiabductionConfig.footprint && not (Paths.PathSet.is_empty (State.get_diverging_states_node ())) then ( - Errdesc.warning_err (State.get_loc_exn ()) "Propagating Divergence@." ; + Errdesc.warning_err (AnalysisState.get_loc_exn ()) "Propagating Divergence@." ; let exit_node = ProcCfg.Exceptional.exit_node proc_cfg in let diverging_states = State.get_diverging_states_node () in let prop_incons = @@ -356,8 +356,8 @@ exception RE_EXE_ERROR let pp_name fmt = F.pp_print_string fmt "interproc" let do_before_node session node = - State.set_node node ; - State.set_session session ; + AnalysisState.set_node node ; + AnalysisState.set_session session ; L.reset_delayed_prints () ; Printer.node_start_session ~pp_name node (session :> int) @@ -416,7 +416,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl = | None -> () ) ; L.d_strln "SIL INSTR:" ; - Procdesc.Node.d_instrs ~highlight:(State.get_instr ()) curr_node ; + Procdesc.Node.d_instrs ~highlight:(AnalysisState.get_instr ()) curr_node ; L.d_ln () ; BiabductionReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ; State.mark_instr_fail exn @@ -442,7 +442,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl = L.d_increase_indent () ; Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv pathset_todo) ; L.d_strln ".... Instructions: ...." ; - Procdesc.Node.d_instrs ~highlight:(State.get_instr ()) curr_node ; + Procdesc.Node.d_instrs ~highlight:(AnalysisState.get_instr ()) curr_node ; L.d_ln () ; L.d_ln () in diff --git a/infer/src/nullsafe/eradicate.ml b/infer/src/nullsafe/eradicate.ml index fb719cbb8..8d040e3c3 100644 --- a/infer/src/nullsafe/eradicate.ml +++ b/infer/src/nullsafe/eradicate.ml @@ -53,7 +53,7 @@ let callback1 tenv find_canonical_duplicate calls_this checks idenv curr_pname c let ret_implicitly_nullable = String.equal (PatternMatch.get_type_name ret_annotated_type.typ) "java.lang.Void" in - State.set_node exit_node ; + AnalysisState.set_node exit_node ; if not (List.is_empty checks.TypeCheck.check_ret_type) then List.iter ~f:(fun f -> f curr_pname curr_pdesc ret_annotated_type.typ typ_found_opt loc) @@ -81,7 +81,7 @@ let callback1 tenv find_canonical_duplicate calls_this checks idenv curr_pname c let do_node tenv node typestate = NodePrinter.with_session ~pp_name node ~f:(fun () -> - State.set_node node ; + AnalysisState.set_node node ; if Config.write_html then L.d_printfln "before:@\n%a@\n" TypeState.pp typestate ; let TypeCheck.{normal_flow_typestate; exception_flow_typestates} = TypeCheck.typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index 9fb6e8057..f27da0c4b 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -232,7 +232,7 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc curr_constructor_pdesc start_node ~nullsafe_mode ~typestates_for_curr_constructor_and_all_initializer_methods ~typestates_for_all_constructors_incl_current loc : unit = - State.set_node start_node ; + AnalysisState.set_node start_node ; if Procname.is_constructor curr_constructor_pname then match PatternMatch.get_this_type_nonstatic_methods_only diff --git a/infer/src/nullsafe/typeErr.ml b/infer/src/nullsafe/typeErr.ml index ea4a2580c..6e6556903 100644 --- a/infer/src/nullsafe/typeErr.ml +++ b/infer/src/nullsafe/typeErr.ml @@ -365,7 +365,7 @@ let report_forall_issues_and_reset st_report_error ~nullsafe_mode proc_desc = match (instr_ref_opt, get_forall err_instance) with | Some instr_ref, is_forall -> let node = InstrRef.get_node instr_ref in - State.set_node node ; + AnalysisState.set_node node ; if is_forall && err_state.always then report_now_if_reportable st_report_error err_instance err_state.loc ~nullsafe_mode proc_desc