From b004a7f5107a07d05d052cb643308956a6722f4c Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 12 Mar 2021 06:45:28 -0800 Subject: [PATCH] [liveness] Handles live variables in catch block Summary: This diff handles live variables in catch blocks. To do that, this diff adds another metadata, `CatchEntry`. Domain change: The domain is changed to ``` (normal:variables) x (exn:try_id->variables) ``` `exn` is a map from try-catch-id to a set of live variables that are live at the corresponding entry of catch blocks. Semantics change: It is a backward analysis. * on `CatchEntry`: It updates `exn` with `try_id` and current `normal`. * on `Call`: As of now, we assume all function calls can raise an exception. Therefore, it copies all live variables in `exn` to `normal`. * on `TryEntry`: It removes corresponding `try_id` from `exn`. Reviewed By: jvillard Differential Revision: D26952755 fbshipit-source-id: 1da854a89 --- infer/src/IR/Sil.ml | 6 +- infer/src/IR/Sil.mli | 1 + .../backend/ClosureSubstSpecializedMethod.ml | 2 +- infer/src/backend/preanal.ml | 9 ++- infer/src/biabduction/Predicates.ml | 9 ++- infer/src/biabduction/SymExec.ml | 2 +- .../bufferoverrun/bufferOverrunAnalysis.ml | 10 ++- infer/src/checkers/liveness.ml | 69 +++++++++++++++- infer/src/checkers/liveness.mli | 12 ++- infer/src/clang/cTrans.ml | 7 +- infer/src/cost/cost.ml | 1 + infer/src/nullsafe/typeCheck.ml | 10 ++- infer/src/pulse/Pulse.ml | 10 ++- infer/src/unit/livenessTests.ml | 81 +++++++++++-------- .../cpp/liveness/dead_stores.cpp | 53 +++++++++++- .../codetoanalyze/cpp/liveness/issues.exp | 4 +- .../cpp/shared/exceptions/Exceptions.cpp.dot | 47 ++++++++--- 17 files changed, 265 insertions(+), 68 deletions(-) diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index a847b089e..c8a51846c 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -28,6 +28,7 @@ type if_kind = type instr_metadata = | Abstract of Location.t (** a good place to apply abstraction, mostly used in the biabduction analysis *) + | CatchEntry of {try_id: int; loc: Location.t} (** entry of C++ catch blocks *) | ExitScope of Var.t list * Location.t (** remove temporaries and dead program variables *) | Nullify of Pvar.t * Location.t (** nullify stack variable *) | Skip (** no-op *) @@ -94,6 +95,7 @@ let pp_exp_typ pe f (e, t) = F.fprintf f "%a:%a" (Exp.pp_diff pe) e (Typ.pp pe) let location_of_instr_metadata = function | Abstract loc + | CatchEntry {loc} | ExitScope (_, loc) | Nullify (_, loc) | TryEntry {loc} @@ -113,7 +115,7 @@ let location_of_instr = function let exps_of_instr_metadata = function - | Abstract _ -> + | Abstract _ | CatchEntry _ -> [] | ExitScope (vars, _) -> List.map ~f:Var.to_exp vars @@ -161,6 +163,8 @@ let if_kind_to_string = function let pp_instr_metadata pe f = function | Abstract loc -> F.fprintf f "APPLY_ABSTRACTION; [%a]" Location.pp loc + | CatchEntry {loc} -> + F.fprintf f "CATCH_ENTRY; [%a]" Location.pp loc | ExitScope (vars, loc) -> F.fprintf f "EXIT_SCOPE(%a); [%a]" (Pp.seq ~sep:"," Var.pp) vars Location.pp loc | Nullify (pvar, loc) -> diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index f88ab89e5..fffc18d64 100644 --- a/infer/src/IR/Sil.mli +++ b/infer/src/IR/Sil.mli @@ -27,6 +27,7 @@ type if_kind = type instr_metadata = | Abstract of Location.t (** a good place to apply abstraction, mostly used in the biabduction analysis *) + | CatchEntry of {try_id: int; loc: Location.t} (** entry of C++ catch blocks *) | ExitScope of Var.t list * Location.t (** remove temporaries and dead program variables *) | Nullify of Pvar.t * Location.t (** nullify stack variable *) | Skip (** no-op *) diff --git a/infer/src/backend/ClosureSubstSpecializedMethod.ml b/infer/src/backend/ClosureSubstSpecializedMethod.ml index 2f4c5fc29..0de03de11 100644 --- a/infer/src/backend/ClosureSubstSpecializedMethod.ml +++ b/infer/src/backend/ClosureSubstSpecializedMethod.ml @@ -124,7 +124,7 @@ let rec exec_exp pname e = let exec_metadata pname metadata = let open Sil in match metadata with - | Abstract _ | Skip | TryEntry _ | TryExit _ -> + | Abstract _ | CatchEntry _ | Skip | TryEntry _ | TryExit _ -> metadata | ExitScope (vars, loc) -> let updated = ref false in diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index cfb330d8b..68d4a789a 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -347,8 +347,9 @@ module Liveness = struct (VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify) | Sil.Metadata (VariableLifetimeBegins (pvar, _, _)) -> (VarDomain.add (Var.of_pvar pvar) active_defs, to_nullify) - | Sil.Store _ | Prune _ | Metadata (Abstract _ | ExitScope _ | Skip | TryEntry _ | TryExit _) - -> + | Sil.Store _ + | Prune _ + | Metadata (Abstract _ | CatchEntry _ | ExitScope _ | Skip | TryEntry _ | TryExit _) -> astate | Sil.Metadata (Nullify _) -> L.(die InternalError) @@ -377,7 +378,7 @@ module Liveness = struct in let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in let nullify_proc_data = {ProcData.summary; tenv; extras= liveness_inv_map} in - let initial = (VarDomain.empty, VarDomain.empty) in + let initial = (VarDomain.bottom, VarDomain.bottom) in let nullify_inv_map = NullifyAnalysis.exec_cfg nullify_proc_cfg nullify_proc_data ~initial in (* only nullify pvars that are local; don't nullify those that can escape *) let is_local pvar = not (Liveness.is_always_in_scope proc_desc pvar) in @@ -432,7 +433,7 @@ module Liveness = struct let process summary tenv = let proc_desc = Summary.get_proc_desc summary in let liveness_proc_cfg = BackwardCfg.from_pdesc proc_desc in - let initial = Liveness.Domain.empty in + let initial = Liveness.Domain.bottom in let liveness_inv_map = LivenessAnalysis.exec_cfg liveness_proc_cfg proc_desc ~initial in add_nullify_instrs summary tenv liveness_inv_map end diff --git a/infer/src/biabduction/Predicates.ml b/infer/src/biabduction/Predicates.ml index 0055a3efe..71bb48237 100644 --- a/infer/src/biabduction/Predicates.ml +++ b/infer/src/biabduction/Predicates.ml @@ -1015,7 +1015,14 @@ let instr_sub_ids ~sub_id_binders f (instr : Sil.instr) : Sil.instr = in let vars' = IList.map_changed ~equal:phys_equal ~f:sub_var vars in if phys_equal vars vars' then instr else Metadata (ExitScope (vars', loc)) - | Metadata (Abstract _ | Nullify _ | Skip | TryEntry _ | TryExit _ | VariableLifetimeBegins _) -> + | Metadata + ( Abstract _ + | CatchEntry _ + | Nullify _ + | Skip + | TryEntry _ + | TryExit _ + | VariableLifetimeBegins _ ) -> instr diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 5841d6fd4..b9c9b1307 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -1348,7 +1348,7 @@ let rec sym_exec | Sil.Metadata (ExitScope (dead_vars, _)) -> let dead_ids = List.filter_map dead_vars ~f:Var.get_ident in ret_old_path [Prop.exist_quantify tenv dead_ids prop_] - | Sil.Metadata (Skip | TryEntry _ | TryExit _ | VariableLifetimeBegins _) -> + | Sil.Metadata (CatchEntry _ | Skip | TryEntry _ | TryExit _ | VariableLifetimeBegins _) -> ret_old_path [prop_] diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 583036c2c..223d4e782 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -434,8 +434,14 @@ module TransferFunctions = struct mem | Metadata (ExitScope (dead_vars, _)) -> Dom.Mem.remove_temps (List.filter_map dead_vars ~f:Var.get_ident) mem - | Metadata (Abstract _ | Nullify _ | Skip | TryEntry _ | TryExit _ | VariableLifetimeBegins _) - -> + | Metadata + ( Abstract _ + | CatchEntry _ + | Nullify _ + | Skip + | TryEntry _ + | TryExit _ + | VariableLifetimeBegins _ ) -> mem diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 1b1f45541..48b3eaf4e 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -12,7 +12,66 @@ module L = Logging (** backward analysis for computing set of maybe-live variables at each program point *) module VarSet = AbstractDomain.FiniteSet (Var) -module Domain = VarSet + +module Exn = struct + include AbstractDomain.Map (Int) (VarSet) + + let union = union (fun _ v1 v2 -> Some (VarSet.union v1 v2)) + + let diff = + merge (fun _ v1 v2 -> + match (v1, v2) with + | None, _ | Some _, None -> + v1 + | Some v1, Some v2 -> + let r = VarSet.diff v1 v2 in + Option.some_if (not (VarSet.is_bottom r)) r ) +end + +module Domain = struct + type t = {normal: VarSet.t; exn: Exn.t} + + let pp f {normal; exn} = F.fprintf f "@[@[normal:%a@],@ @[exn:%a@]@]" VarSet.pp normal Exn.pp exn + + let leq ~lhs ~rhs = + VarSet.leq ~lhs:lhs.normal ~rhs:rhs.normal && Exn.leq ~lhs:lhs.exn ~rhs:rhs.exn + + + let join x y = {normal= VarSet.join x.normal y.normal; exn= Exn.join x.exn y.exn} + + let widen ~prev ~next ~num_iters = + { normal= VarSet.widen ~prev:prev.normal ~next:next.normal ~num_iters + ; exn= Exn.widen ~prev:prev.exn ~next:next.exn ~num_iters } + + + let bottom = {normal= VarSet.bottom; exn= Exn.bottom} + + let is_bottom {normal; exn} = VarSet.is_bottom normal && Exn.is_bottom exn + + let update_normal ~f x = {x with normal= f x.normal} + + let add var = update_normal ~f:(VarSet.add var) + + let remove var = update_normal ~f:(VarSet.remove var) + + let map_normal ~f x = f x.normal + + let mem var = map_normal ~f:(VarSet.mem var) + + let fold f x init = map_normal ~f:(fun normal -> VarSet.fold f normal init) x + + let union x y = {normal= VarSet.union x.normal y.normal; exn= Exn.union x.exn y.exn} + + let diff x y = {normal= VarSet.diff x.normal y.normal; exn= Exn.diff x.exn y.exn} + + let catch_entry try_id x = {normal= VarSet.empty; exn= Exn.add try_id x.normal x.exn} + + let try_entry try_id x = {x with exn= Exn.remove try_id x.exn} + + let add_live_in_catch x = + { x with + normal= Exn.fold (fun _ live_in_catch acc -> VarSet.join acc live_in_catch) x.exn x.normal } +end (** only kill pvars that are local; don't kill those that can escape *) let is_always_in_scope proc_desc pvar = @@ -157,6 +216,12 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct in Domain.remove (Var.of_id ret_id) astate |> exp_add_live call_exp |> add_live_actuals actuals_to_read + |> (* assume that all function calls can throw for now *) + Domain.add_live_in_catch + | Sil.Metadata (CatchEntry {try_id}) -> + Domain.catch_entry try_id astate + | Sil.Metadata (TryEntry {try_id}) -> + Domain.try_entry try_id astate | Sil.Metadata _ -> astate @@ -254,7 +319,7 @@ let ignored_constants = let checker {IntraproceduralAnalysis.proc_desc; err_log} = let passed_by_ref_invariant_map = get_passed_by_ref_invariant_map proc_desc in let cfg = CFG.from_pdesc proc_desc in - let invariant_map = CheckerAnalyzer.exec_cfg cfg proc_desc ~initial:Domain.empty in + let invariant_map = CheckerAnalyzer.exec_cfg cfg proc_desc ~initial:Domain.bottom in (* we don't want to report in harmless cases like int i = 0; if (...) { i = ... } else { i = ... } that create an intentional dead store as an attempt to imitate default value semantics. use dead stores to a "sentinel" value as a heuristic for ignoring this case *) diff --git a/infer/src/checkers/liveness.mli b/infer/src/checkers/liveness.mli index 1791b1892..2378fdfcd 100644 --- a/infer/src/checkers/liveness.mli +++ b/infer/src/checkers/liveness.mli @@ -6,9 +6,17 @@ *) open! IStd -module VarSet : module type of AbstractDomain.FiniteSet (Var) +module Domain : sig + include AbstractDomain.WithBottom -module Domain = VarSet + val add : Var.t -> t -> t + + val fold : (Var.t -> 'a -> 'a) -> t -> 'a -> 'a + + val union : t -> t -> t + + val diff : t -> t -> t +end module PreAnalysisTransferFunctions (CFG : ProcCfg.S) : TransferFunctions.SIL diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index ed38d43cf..57b8b6a93 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -2180,8 +2180,13 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s Procdesc.create_node procdesc try_loc (Stmt_node CXXTry) [Metadata (TryExit {try_id; loc= try_loc})] in + let catch_entry_node = + Procdesc.create_node procdesc try_loc (Stmt_node CXXTry) + [Metadata (CatchEntry {try_id; loc= try_loc})] + in Procdesc.set_succs try_exit_node ~normal:(Some trans_state.succ_nodes) - ~exn:(Some catch_start_nodes) ; + ~exn:(Some [catch_entry_node]) ; + Procdesc.set_succs catch_entry_node ~normal:(Some catch_start_nodes) ~exn:None ; (* add catch block as exceptional successor to end of try block. not ideal, but we will at least reach the code in the catch block this way *) (* TODO (T28898377): instead, we should extend trans_state with a list of maybe-throwing diff --git a/infer/src/cost/cost.ml b/infer/src/cost/cost.ml index 26afb66ce..1572ec757 100644 --- a/infer/src/cost/cost.ml +++ b/infer/src/cost/cost.ml @@ -216,6 +216,7 @@ module InstrBasicCostWithReason = struct CostDomain.unit_cost_atomic_operation | Sil.Metadata ( Abstract _ + | CatchEntry _ | ExitScope _ | Nullify _ | Skip diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index b129aaa44..bb5f4ebf5 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -1220,8 +1220,14 @@ let typecheck_instr ({IntraproceduralAnalysis.proc_desc= curr_pdesc; tenv; _} as TypeState.remove_id id astate ~descr:"ExitScope" | Var.ProgramVar _ -> astate ) - | Sil.Metadata (Abstract _ | Nullify _ | Skip | TryEntry _ | TryExit _ | VariableLifetimeBegins _) - -> + | Sil.Metadata + ( Abstract _ + | CatchEntry _ + | Nullify _ + | Skip + | TryEntry _ + | TryExit _ + | VariableLifetimeBegins _ ) -> typestate | Sil.Load {id; e; typ; loc} -> typecheck_expr_for_errors analysis_data ~nullsafe_mode find_canonical_duplicate calls_this diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 365ddd5b7..2cee99739 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -367,8 +367,14 @@ module PulseTransferFunctions = struct remove_vars vars_to_remove astates | Metadata (VariableLifetimeBegins (pvar, typ, location)) when not (Pvar.is_global pvar) -> [PulseOperations.realloc_pvar tenv pvar typ location astate |> Domain.continue] - | Metadata (Abstract _ | VariableLifetimeBegins _ | Nullify _ | Skip | TryEntry _ | TryExit _) - -> + | Metadata + ( Abstract _ + | CatchEntry _ + | Nullify _ + | Skip + | TryEntry _ + | TryExit _ + | VariableLifetimeBegins _ ) -> [ContinueProgram astate] ) diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index 51e4235ee..25df8b436 100644 --- a/infer/src/unit/livenessTests.ml +++ b/infer/src/unit/livenessTests.ml @@ -12,7 +12,7 @@ module TestInterpreter = let tests = let open OUnit2 in let open AnalyzerTester.StructuredSil in - let assert_empty = invariant "{ }" in + let assert_empty = invariant "normal:{ }, exn:{ }" in let fun_ptr_typ = Typ.mk (Tptr (Typ.mk Tfun, Pk_pointer)) in let closure_exp captured_pvars = let mk_captured_var str = @@ -27,80 +27,95 @@ let tests = Exp.zero in let test_list = - [ ("basic_live", [invariant "{ b }"; id_assign_var "a" "b"]) + [ ("basic_live", [invariant "normal:{ b }, exn:{ }"; id_assign_var "a" "b"]) ; ( "basic_live_then_dead" - , [assert_empty; var_assign_int "b" 1; invariant "{ b }"; id_assign_var "a" "b"] ) + , [ assert_empty + ; var_assign_int "b" 1 + ; invariant "normal:{ b }, exn:{ }" + ; id_assign_var "a" "b" ] ) ; ( "iterative_live" - , [ invariant "{ b, f, d }" + , [ invariant "normal:{ b, f, d }, exn:{ }" ; id_assign_var "e" "f" - ; invariant "{ b, d }" + ; invariant "normal:{ b, d }, exn:{ }" ; id_assign_var "c" "d" - ; invariant "{ b }" + ; invariant "normal:{ b }, exn:{ }" ; id_assign_var "a" "b" ] ) ; ( "live_kill_live" - , [ invariant "{ b }" + , [ invariant "normal:{ b }, exn:{ }" ; id_assign_var "c" "b" ; assert_empty ; var_assign_int "b" 1 - ; invariant "{ b }" + ; invariant "normal:{ b }, exn:{ }" ; id_assign_var "a" "b" ] ) - ; ("basic_live_load", [invariant "{ y$0 }"; id_assign_id "x" "y"]) + ; ("basic_live_load", [invariant "normal:{ y$0 }, exn:{ }"; id_assign_id "x" "y"]) ; ( "basic_live_then_kill_load" - , [invariant "{ z$0 }"; id_assign_id "y" "z"; invariant "{ y$0 }"; id_assign_id "x" "y"] ) + , [ invariant "normal:{ z$0 }, exn:{ }" + ; id_assign_id "y" "z" + ; invariant "normal:{ y$0 }, exn:{ }" + ; id_assign_id "x" "y" ] ) ; ( "set_id" , (* this is *x = y, which is a read of both x and y *) - [invariant "{ x$0, y$0 }"; id_set_id "x" "y"] ) + [invariant "normal:{ x$0, y$0 }, exn:{ }"; id_set_id "x" "y"] ) ; ( "if_exp_live" - , [assert_empty; var_assign_int "x" 1; invariant "{ x }"; If (var_of_str "x", [], [])] ) + , [ assert_empty + ; var_assign_int "x" 1 + ; invariant "normal:{ x }, exn:{ }" + ; If (var_of_str "x", [], []) ] ) ; ( "while_exp_live" - , [assert_empty; var_assign_int "x" 1; invariant "{ x }"; While (var_of_str "x", [])] ) - ; ("call_params_live", [invariant "{ b, a, c }"; call_unknown ["a"; "b"; "c"]]) + , [ assert_empty + ; var_assign_int "x" 1 + ; invariant "normal:{ x }, exn:{ }" + ; While (var_of_str "x", []) ] ) + ; ("call_params_live", [invariant "normal:{ b, a, c }, exn:{ }"; call_unknown ["a"; "b"; "c"]]) ; ( "dead_after_call_with_retval" , [ assert_empty ; call_unknown ~return:("y", Typ.mk (Tint IInt)) [] - ; invariant "{ y$0 }" + ; invariant "normal:{ y$0 }, exn:{ }" ; id_assign_id "x" "y" ] ) ; ( "closure_captured_live" - , [invariant "{ b$0, c$0 }"; var_assign_exp ~rhs_typ:fun_ptr_typ "a" (closure_exp ["b"; "c"])] - ) - ; ("if_conservative_live1", [invariant "{ b }"; If (unknown_cond, [id_assign_var "a" "b"], [])]) + , [ invariant "normal:{ b$0, c$0 }, exn:{ }" + ; var_assign_exp ~rhs_typ:fun_ptr_typ "a" (closure_exp ["b"; "c"]) ] ) + ; ( "if_conservative_live1" + , [invariant "normal:{ b }, exn:{ }"; If (unknown_cond, [id_assign_var "a" "b"], [])] ) ; ( "if_conservative_live2" - , [invariant "{ b, d }"; If (unknown_cond, [id_assign_var "a" "b"], [id_assign_var "c" "d"])] - ) + , [ invariant "normal:{ b, d }, exn:{ }" + ; If (unknown_cond, [id_assign_var "a" "b"], [id_assign_var "c" "d"]) ] ) ; ( "if_conservative_kill" - , [ invariant "{ b }" + , [ invariant "normal:{ b }, exn:{ }" ; If (unknown_cond, [var_assign_int "b" 1], []) - ; invariant "{ b }" + ; invariant "normal:{ b }, exn:{ }" ; id_assign_var "a" "b" ] ) ; ( "if_conservative_kill_live" - , [ invariant "{ b, d }" + , [ invariant "normal:{ b, d }, exn:{ }" ; If (unknown_cond, [var_assign_int "b" 1], [id_assign_var "c" "d"]) - ; invariant "{ b }" + ; invariant "normal:{ b }, exn:{ }" ; id_assign_var "a" "b" ] ) ; ( "if_precise1" , [ assert_empty ; If ( unknown_cond - , [var_assign_int "b" 1; invariant "{ b }"; id_assign_var "a" "b"] - , [var_assign_int "d" 1; invariant "{ d }"; id_assign_var "c" "d"] ) ] ) + , [var_assign_int "b" 1; invariant "normal:{ b }, exn:{ }"; id_assign_var "a" "b"] + , [var_assign_int "d" 1; invariant "normal:{ d }, exn:{ }"; id_assign_var "c" "d"] ) ] + ) ; ( "if_precise2" , [ assert_empty ; If (unknown_cond, [var_assign_int "b" 2], [var_assign_int "b" 1]) - ; invariant "{ b }" + ; invariant "normal:{ b }, exn:{ }" ; id_assign_var "a" "b" ] ) - ; ("loop_as_if1", [invariant "{ b }"; While (unknown_cond, [id_assign_var "a" "b"])]) + ; ( "loop_as_if1" + , [invariant "normal:{ b }, exn:{ }"; While (unknown_cond, [id_assign_var "a" "b"])] ) ; ( "loop_as_if2" - , [ invariant "{ b }" + , [ invariant "normal:{ b }, exn:{ }" ; While (unknown_cond, [var_assign_int "b" 1]) - ; invariant "{ b }" + ; invariant "normal:{ b }, exn:{ }" ; id_assign_var "a" "b" ] ) ; ( "loop_before_after" - , [ invariant "{ b, d }" + , [ invariant "normal:{ b, d }, exn:{ }" ; While (unknown_cond, [id_assign_var "b" "d"]) - ; invariant "{ b }" + ; invariant "normal:{ b }, exn:{ }" ; id_assign_var "a" "b" ] ) ] |> TestInterpreter.create_tests (fun summary -> Summary.get_proc_desc summary) - ~initial:Liveness.Domain.empty + ~initial:Liveness.Domain.bottom in "liveness_test_suite" >::: test_list diff --git a/infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp b/infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp index 95aca7c6d..bc21f9076 100644 --- a/infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp +++ b/infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp @@ -403,7 +403,7 @@ class Exceptions { return 0; } - int FN_unreachable_catch_bad() { + int unreachable_catch_bad() { int i = 1; try { } catch (...) { @@ -455,7 +455,7 @@ class Exceptions { // currently, the only transition to the catch block is at the end of the try // block. See T28898377 - int FP_read_in_catch_tricky_ok(bool b1, bool b2) { + int read_in_catch_tricky_ok(bool b1, bool b2) { int i = 1; try { if (b1) { @@ -538,6 +538,55 @@ class Exceptions { } return 3; } + + int read_in_catch_ok() { + int x; + try { + x = 10; + maybe_throw(); + x = 20; + } catch (...) { + return x; + } + return x; + } + + int not_read_in_catch_bad() { + int x; + try { + x = 10; + maybe_throw(); + x = 20; + } catch (...) { + return 0; + } + return x; + } + + int read_only_in_catch_bad() { + int x; + try { + x = 10; + maybe_throw(); + x = 20; + } catch (...) { + return x; + } + return 0; + } + + void never_throw() {} + + int FN_read_only_in_unreachable_catch_bad() { + int x; + try { + x = 10; + never_throw(); + } catch (...) { + return x; + } + return 0; + } }; void init_in_binop_bad(int x) { x = -x & ~int{0}; } diff --git a/infer/tests/codetoanalyze/cpp/liveness/issues.exp b/infer/tests/codetoanalyze/cpp/liveness/issues.exp index 692931a64..3a0113669 100644 --- a/infer/tests/codetoanalyze/cpp/liveness/issues.exp +++ b/infer/tests/codetoanalyze/cpp/liveness/issues.exp @@ -1,5 +1,7 @@ -codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::Exceptions::FP_read_in_catch_tricky_ok, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value] codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::Exceptions::dead_in_catch_bad, 4, DEAD_STORE, no_bucket, ERROR, [Write of unused value] +codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::Exceptions::not_read_in_catch_bad, 3, DEAD_STORE, no_bucket, ERROR, [Write of unused value] +codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::Exceptions::read_only_in_catch_bad, 5, DEAD_STORE, no_bucket, ERROR, [Write of unused value] +codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::Exceptions::unreachable_catch_bad, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value] codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::FP_assign_array_tricky2_ok, 3, DEAD_STORE, no_bucket, ERROR, [Write of unused value] codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::binaryConditional_bad, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value] codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::binaryConditional_bad, 4, DEAD_STORE, no_bucket, ERROR, [Write of unused value] diff --git a/infer/tests/codetoanalyze/cpp/shared/exceptions/Exceptions.cpp.dot b/infer/tests/codetoanalyze/cpp/shared/exceptions/Exceptions.cpp.dot index 44bf541fa..e4b84a484 100644 --- a/infer/tests/codetoanalyze/cpp/shared/exceptions/Exceptions.cpp.dot +++ b/infer/tests/codetoanalyze/cpp/shared/exceptions/Exceptions.cpp.dot @@ -39,11 +39,15 @@ digraph cfg { "FN_deref_null_after_catch_bad#4627123003703707696.43441e3badf1bb571cbe770f9d51a51c_10" -> "FN_deref_null_after_catch_bad#4627123003703707696.43441e3badf1bb571cbe770f9d51a51c_3" ; - "FN_deref_null_after_catch_bad#4627123003703707696.43441e3badf1bb571cbe770f9d51a51c_10" -> "FN_deref_null_after_catch_bad#4627123003703707696.43441e3badf1bb571cbe770f9d51a51c_9" [color="red" ]; + "FN_deref_null_after_catch_bad#4627123003703707696.43441e3badf1bb571cbe770f9d51a51c_10" -> "FN_deref_null_after_catch_bad#4627123003703707696.43441e3badf1bb571cbe770f9d51a51c_11" [color="red" ]; +"FN_deref_null_after_catch_bad#4627123003703707696.43441e3badf1bb571cbe770f9d51a51c_11" [label="11: CXXTry \n CATCH_ENTRY; [line 46, column 3]\n " shape="box"] + + + "FN_deref_null_after_catch_bad#4627123003703707696.43441e3badf1bb571cbe770f9d51a51c_11" -> "FN_deref_null_after_catch_bad#4627123003703707696.43441e3badf1bb571cbe770f9d51a51c_9" ; "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_1" [label="1: Start FN_deref_null_in_catch_bad\nFormals: \nLocals: 0$?%__sil_tmp__temp_construct_n$1:std::runtime_error 0$?%__sil_tmpSIL_materialize_temp__n$0:std::runtime_error const i:int* \n " color=yellow style=filled] - "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_1" -> "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_10" ; + "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_1" -> "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_11" ; "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_2" [label="2: Exit FN_deref_null_in_catch_bad \n " color=yellow style=filled] @@ -75,15 +79,19 @@ digraph cfg { "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_9" -> "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_3" ; - "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_9" -> "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_7" [color="red" ]; -"FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_10" [label="10: DeclStmt \n VARIABLE_DECLARED(i:int*); [line 36, column 3]\n *&i:int*=null [line 36, column 3]\n " shape="box"] + "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_9" -> "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_10" [color="red" ]; +"FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_10" [label="10: CXXTry \n CATCH_ENTRY; [line 37, column 3]\n " shape="box"] - "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_10" -> "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_6" ; + "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_10" -> "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_7" ; +"FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_11" [label="11: DeclStmt \n VARIABLE_DECLARED(i:int*); [line 36, column 3]\n *&i:int*=null [line 36, column 3]\n " shape="box"] + + + "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_11" -> "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_6" ; "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_1" [label="1: Start FN_multiple_catches_bad\nFormals: b:_Bool\nLocals: 0$?%__sil_tmp__temp_construct_n$2:std::length_error 0$?%__sil_tmpSIL_materialize_temp__n$1:std::length_error const 0$?%__sil_tmp__temp_construct_n$9:std::range_error 0$?%__sil_tmpSIL_materialize_temp__n$8:std::range_error const j:int* i:int* \n " color=yellow style=filled] - "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_1" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_18" ; + "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_1" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_19" ; "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_2" [label="2: Exit FN_multiple_catches_bad \n " color=yellow style=filled] @@ -144,16 +152,20 @@ digraph cfg { "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_16" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_3" ; - "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_16" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_14" [color="red" ]; - "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_16" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_12" [color="red" ]; -"FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_17" [label="17: DeclStmt \n VARIABLE_DECLARED(j:int*); [line 57, column 3]\n *&j:int*=null [line 57, column 3]\n " shape="box"] + "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_16" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_17" [color="red" ]; +"FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_17" [label="17: CXXTry \n CATCH_ENTRY; [line 58, column 3]\n " shape="box"] + + + "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_17" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_14" ; + "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_17" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_12" ; +"FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_18" [label="18: DeclStmt \n VARIABLE_DECLARED(j:int*); [line 57, column 3]\n *&j:int*=null [line 57, column 3]\n " shape="box"] - "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_17" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_11" ; -"FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_18" [label="18: DeclStmt \n VARIABLE_DECLARED(i:int*); [line 56, column 3]\n *&i:int*=null [line 56, column 3]\n " shape="box"] + "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_18" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_11" ; +"FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_19" [label="19: DeclStmt \n VARIABLE_DECLARED(i:int*); [line 56, column 3]\n *&i:int*=null [line 56, column 3]\n " shape="box"] - "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_18" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_17" ; + "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_19" -> "FN_multiple_catches_bad#4595182522053295670.680a793e449c2d7439ff6441ca69fa98_18" ; "basic_throw_ok#10529188890980782893.c9e1b8dd080b2621cfca65612331859d_1" [label="1: Start basic_throw_ok\nFormals: \nLocals: 0$?%__sil_tmp__temp_construct_n$1:std::runtime_error 0$?%__sil_tmpSIL_materialize_temp__n$0:std::runtime_error const \n " color=yellow style=filled] @@ -266,6 +278,11 @@ digraph cfg { "deref_null#11536394632240553702.ea4eed042da22ab7ceb619ec1b7f73bb_6" -> "deref_null#11536394632240553702.ea4eed042da22ab7ceb619ec1b7f73bb_2" ; + "deref_null#11536394632240553702.ea4eed042da22ab7ceb619ec1b7f73bb_6" -> "deref_null#11536394632240553702.ea4eed042da22ab7ceb619ec1b7f73bb_7" [color="red" ]; +"deref_null#11536394632240553702.ea4eed042da22ab7ceb619ec1b7f73bb_7" [label="7: CXXTry \n CATCH_ENTRY; [line 19, column 3]\n " shape="box"] + + + "deref_null#11536394632240553702.ea4eed042da22ab7ceb619ec1b7f73bb_7" -> "deref_null#11536394632240553702.ea4eed042da22ab7ceb619ec1b7f73bb_2" ; "main.fad58de7366495db4650cfefac2fcd61_1" [label="1: Start main\nFormals: \nLocals: \n " color=yellow style=filled] @@ -293,5 +310,9 @@ digraph cfg { "main.fad58de7366495db4650cfefac2fcd61_7" -> "main.fad58de7366495db4650cfefac2fcd61_2" ; - "main.fad58de7366495db4650cfefac2fcd61_7" -> "main.fad58de7366495db4650cfefac2fcd61_6" [color="red" ]; + "main.fad58de7366495db4650cfefac2fcd61_7" -> "main.fad58de7366495db4650cfefac2fcd61_8" [color="red" ]; +"main.fad58de7366495db4650cfefac2fcd61_8" [label="8: CXXTry \n CATCH_ENTRY; [line 73, column 3]\n " shape="box"] + + + "main.fad58de7366495db4650cfefac2fcd61_8" -> "main.fad58de7366495db4650cfefac2fcd61_6" ; }