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

[liveness] Handles live variables in catch block

Browse Source 
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
master
Sungkeun Cho 4 years ago committed by Facebook GitHub Bot
parent 8e1ea769ea
commit b004a7f510
17 changed files with 265 additions and 68 deletions
Show Stats Download Patch File Download Diff File

6
infer/src/IR/Sil.ml
Unescape View File

@ -28,6 +28,7 @@ type if_kind =
type instr_metadata = type instr_metadata =
| Abstract of Location.t | Abstract of Location.t
(** a good place to apply abstraction, mostly used in the biabduction analysis *) (** 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 *) | ExitScope of Var.t list * Location.t (** remove temporaries and dead program variables *)
| Nullify of Pvar.t * Location.t (** nullify stack variable *) | Nullify of Pvar.t * Location.t (** nullify stack variable *)
| Skip (** no-op *) | 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 let location_of_instr_metadata = function
| Abstract loc | Abstract loc
| CatchEntry {loc}
| ExitScope (_, loc) | ExitScope (_, loc)
| Nullify (_, loc) | Nullify (_, loc)
| TryEntry {loc} | TryEntry {loc}
@ -113,7 +115,7 @@ let location_of_instr = function
let exps_of_instr_metadata = function let exps_of_instr_metadata = function
| Abstract _ -> | Abstract _ | CatchEntry _ ->
[] []
| ExitScope (vars, _) -> | ExitScope (vars, _) ->
List.map ~f:Var.to_exp 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 let pp_instr_metadata pe f = function
| Abstract loc -> | Abstract loc ->
F.fprintf f "APPLY_ABSTRACTION; [%a]" Location.pp loc F.fprintf f "APPLY_ABSTRACTION; [%a]" Location.pp loc
| CatchEntry {loc} ->
F.fprintf f "CATCH_ENTRY; [%a]" Location.pp loc
| ExitScope (vars, loc) -> | ExitScope (vars, loc) ->
F.fprintf f "EXIT_SCOPE(%a); [%a]" (Pp.seq ~sep:"," Var.pp) vars Location.pp loc F.fprintf f "EXIT_SCOPE(%a); [%a]" (Pp.seq ~sep:"," Var.pp) vars Location.pp loc
| Nullify (pvar, loc) -> | Nullify (pvar, loc) ->

1
infer/src/IR/Sil.mli
Unescape View File

@ -27,6 +27,7 @@ type if_kind =
type instr_metadata = type instr_metadata =
| Abstract of Location.t | Abstract of Location.t
(** a good place to apply abstraction, mostly used in the biabduction analysis *) (** 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 *) | ExitScope of Var.t list * Location.t (** remove temporaries and dead program variables *)
| Nullify of Pvar.t * Location.t (** nullify stack variable *) | Nullify of Pvar.t * Location.t (** nullify stack variable *)
| Skip (** no-op *) | Skip (** no-op *)

2
infer/src/backend/ClosureSubstSpecializedMethod.ml
Unescape View File

@ -124,7 +124,7 @@ let rec exec_exp pname e =
let exec_metadata pname metadata = let exec_metadata pname metadata =
let open Sil in let open Sil in
match metadata with match metadata with
| Abstract _ | Skip | TryEntry _ | TryExit _ -> | Abstract _ | CatchEntry _ | Skip | TryEntry _ | TryExit _ ->
metadata metadata
| ExitScope (vars, loc) -> | ExitScope (vars, loc) ->
let updated = ref false in let updated = ref false in

9
infer/src/backend/preanal.ml
Unescape View File

@ -347,8 +347,9 @@ module Liveness = struct
(VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify) (VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify)
| Sil.Metadata (VariableLifetimeBegins (pvar, _, _)) -> | Sil.Metadata (VariableLifetimeBegins (pvar, _, _)) ->
(VarDomain.add (Var.of_pvar pvar) active_defs, to_nullify) (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 astate
| Sil.Metadata (Nullify _) -> | Sil.Metadata (Nullify _) ->
L.(die InternalError) L.(die InternalError)
@ -377,7 +378,7 @@ module Liveness = struct
in in
let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc 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 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 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 *) (* 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 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 process summary tenv =
let proc_desc = Summary.get_proc_desc summary in let proc_desc = Summary.get_proc_desc summary in
let liveness_proc_cfg = BackwardCfg.from_pdesc proc_desc 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 let liveness_inv_map = LivenessAnalysis.exec_cfg liveness_proc_cfg proc_desc ~initial in
add_nullify_instrs summary tenv liveness_inv_map add_nullify_instrs summary tenv liveness_inv_map
end end

9
infer/src/biabduction/Predicates.ml
Unescape View File

@ -1015,7 +1015,14 @@ let instr_sub_ids ~sub_id_binders f (instr : Sil.instr) : Sil.instr =
in in
let vars' = IList.map_changed ~equal:phys_equal ~f:sub_var vars 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)) 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 instr

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

@ -1348,7 +1348,7 @@ let rec sym_exec
| 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_]
| Sil.Metadata (Skip | TryEntry _ | TryExit _ | VariableLifetimeBegins _) -> | Sil.Metadata (CatchEntry _ | Skip | TryEntry _ | TryExit _ | VariableLifetimeBegins _) ->
ret_old_path [prop_] ret_old_path [prop_]

10
infer/src/bufferoverrun/bufferOverrunAnalysis.ml
Unescape View File

@ -434,8 +434,14 @@ module TransferFunctions = struct
mem mem
| Metadata (ExitScope (dead_vars, _)) -> | Metadata (ExitScope (dead_vars, _)) ->
Dom.Mem.remove_temps (List.filter_map dead_vars ~f:Var.get_ident) mem 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 mem

69
infer/src/checkers/liveness.ml
Unescape View File

@ -12,7 +12,66 @@ module L = Logging
(** backward analysis for computing set of maybe-live variables at each program point *) (** backward analysis for computing set of maybe-live variables at each program point *)
module VarSet = AbstractDomain.FiniteSet (Var) 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 *) (** only kill pvars that are local; don't kill those that can escape *)
let is_always_in_scope proc_desc pvar = let is_always_in_scope proc_desc pvar =
@ -157,6 +216,12 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct
in in
Domain.remove (Var.of_id ret_id) astate Domain.remove (Var.of_id ret_id) astate
|> exp_add_live call_exp |> add_live_actuals actuals_to_read |> 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 _ -> | Sil.Metadata _ ->
astate astate
@ -254,7 +319,7 @@ let ignored_constants =
let checker {IntraproceduralAnalysis.proc_desc; err_log} = let checker {IntraproceduralAnalysis.proc_desc; err_log} =
let passed_by_ref_invariant_map = get_passed_by_ref_invariant_map proc_desc in let passed_by_ref_invariant_map = get_passed_by_ref_invariant_map proc_desc in
let cfg = CFG.from_pdesc 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 = ... } (* 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. 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 *) use dead stores to a "sentinel" value as a heuristic for ignoring this case *)

12
infer/src/checkers/liveness.mli
Unescape View File

@ -6,9 +6,17 @@
*) *)
open! IStd 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) : module PreAnalysisTransferFunctions (CFG : ProcCfg.S) :
TransferFunctions.SIL TransferFunctions.SIL

7
infer/src/clang/cTrans.ml
Unescape View File

@ -2180,8 +2180,13 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
Procdesc.create_node procdesc try_loc (Stmt_node CXXTry) Procdesc.create_node procdesc try_loc (Stmt_node CXXTry)
[Metadata (TryExit {try_id; loc= try_loc})] [Metadata (TryExit {try_id; loc= try_loc})]
in 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) 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 (* 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 *) least reach the code in the catch block this way *)
(* TODO (T28898377): instead, we should extend trans_state with a list of maybe-throwing (* TODO (T28898377): instead, we should extend trans_state with a list of maybe-throwing

1
infer/src/cost/cost.ml
Unescape View File

@ -216,6 +216,7 @@ module InstrBasicCostWithReason = struct
CostDomain.unit_cost_atomic_operation CostDomain.unit_cost_atomic_operation
| Sil.Metadata | Sil.Metadata
( Abstract _ ( Abstract _
| CatchEntry _
| ExitScope _ | ExitScope _
| Nullify _ | Nullify _
| Skip | Skip

10
infer/src/nullsafe/typeCheck.ml
Unescape View File

@ -1220,8 +1220,14 @@ let typecheck_instr ({IntraproceduralAnalysis.proc_desc= curr_pdesc; tenv; _} as
TypeState.remove_id id astate ~descr:"ExitScope" TypeState.remove_id id astate ~descr:"ExitScope"
| Var.ProgramVar _ -> | Var.ProgramVar _ ->
astate ) astate )
| Sil.Metadata (Abstract _ | Nullify _ | Skip | TryEntry _ | TryExit _ | VariableLifetimeBegins _) | Sil.Metadata
-> ( Abstract _
| CatchEntry _
| Nullify _
| Skip
| TryEntry _
| TryExit _
| VariableLifetimeBegins _ ) ->
typestate typestate
| Sil.Load {id; e; typ; loc} -> | Sil.Load {id; e; typ; loc} ->
typecheck_expr_for_errors analysis_data ~nullsafe_mode find_canonical_duplicate calls_this typecheck_expr_for_errors analysis_data ~nullsafe_mode find_canonical_duplicate calls_this

10
infer/src/pulse/Pulse.ml
Unescape View File

@ -367,8 +367,14 @@ module PulseTransferFunctions = struct
remove_vars vars_to_remove astates remove_vars vars_to_remove astates
| Metadata (VariableLifetimeBegins (pvar, typ, location)) when not (Pvar.is_global pvar) -> | Metadata (VariableLifetimeBegins (pvar, typ, location)) when not (Pvar.is_global pvar) ->
[PulseOperations.realloc_pvar tenv pvar typ location astate |> Domain.continue] [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] ) [ContinueProgram astate] )

81
infer/src/unit/livenessTests.ml
Unescape View File

@ -12,7 +12,7 @@ module TestInterpreter =
let tests = let tests =
let open OUnit2 in let open OUnit2 in
let open AnalyzerTester.StructuredSil 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 fun_ptr_typ = Typ.mk (Tptr (Typ.mk Tfun, Pk_pointer)) in
let closure_exp captured_pvars = let closure_exp captured_pvars =
let mk_captured_var str = let mk_captured_var str =
@ -27,80 +27,95 @@ let tests =
Exp.zero Exp.zero
in in
let test_list = 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" ; ( "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" ; ( "iterative_live"
, [ invariant "{ b, f, d }" , [ invariant "normal:{ b, f, d }, exn:{ }"
; id_assign_var "e" "f" ; id_assign_var "e" "f"
; invariant "{ b, d }" ; invariant "normal:{ b, d }, exn:{ }"
; id_assign_var "c" "d" ; id_assign_var "c" "d"
; invariant "{ b }" ; invariant "normal:{ b }, exn:{ }"
; id_assign_var "a" "b" ] ) ; id_assign_var "a" "b" ] )
; ( "live_kill_live" ; ( "live_kill_live"
, [ invariant "{ b }" , [ invariant "normal:{ b }, exn:{ }"
; id_assign_var "c" "b" ; id_assign_var "c" "b"
; assert_empty ; assert_empty
; var_assign_int "b" 1 ; var_assign_int "b" 1
; invariant "{ b }" ; invariant "normal:{ b }, exn:{ }"
; id_assign_var "a" "b" ] ) ; 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" ; ( "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" ; ( "set_id"
, (* this is *x = y, which is a read of both x and y *) , (* 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" ; ( "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" ; ( "while_exp_live"
, [assert_empty; var_assign_int "x" 1; invariant "{ x }"; While (var_of_str "x", [])] ) , [ assert_empty
; ("call_params_live", [invariant "{ b, a, c }"; call_unknown ["a"; "b"; "c"]]) ; 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" ; ( "dead_after_call_with_retval"
, [ assert_empty , [ assert_empty
; call_unknown ~return:("y", Typ.mk (Tint IInt)) [] ; call_unknown ~return:("y", Typ.mk (Tint IInt)) []
; invariant "{ y$0 }" ; invariant "normal:{ y$0 }, exn:{ }"
; id_assign_id "x" "y" ] ) ; id_assign_id "x" "y" ] )
; ( "closure_captured_live" ; ( "closure_captured_live"
, [invariant "{ b$0, c$0 }"; var_assign_exp ~rhs_typ:fun_ptr_typ "a" (closure_exp ["b"; "c"])] , [ invariant "normal:{ b$0, c$0 }, exn:{ }"
) ; 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"], [])]) ; ( "if_conservative_live1"
, [invariant "normal:{ b }, exn:{ }"; If (unknown_cond, [id_assign_var "a" "b"], [])] )
; ( "if_conservative_live2" ; ( "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" ; ( "if_conservative_kill"
, [ invariant "{ b }" , [ invariant "normal:{ b }, exn:{ }"
; If (unknown_cond, [var_assign_int "b" 1], []) ; If (unknown_cond, [var_assign_int "b" 1], [])
; invariant "{ b }" ; invariant "normal:{ b }, exn:{ }"
; id_assign_var "a" "b" ] ) ; id_assign_var "a" "b" ] )
; ( "if_conservative_kill_live" ; ( "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"]) ; If (unknown_cond, [var_assign_int "b" 1], [id_assign_var "c" "d"])
; invariant "{ b }" ; invariant "normal:{ b }, exn:{ }"
; id_assign_var "a" "b" ] ) ; id_assign_var "a" "b" ] )
; ( "if_precise1" ; ( "if_precise1"
, [ assert_empty , [ assert_empty
; If ; If
( unknown_cond ( unknown_cond
, [var_assign_int "b" 1; invariant "{ b }"; id_assign_var "a" "b"] , [var_assign_int "b" 1; invariant "normal:{ b }, exn:{ }"; id_assign_var "a" "b"]
, [var_assign_int "d" 1; invariant "{ d }"; id_assign_var "c" "d"] ) ] ) , [var_assign_int "d" 1; invariant "normal:{ d }, exn:{ }"; id_assign_var "c" "d"] ) ]
)
; ( "if_precise2" ; ( "if_precise2"
, [ assert_empty , [ assert_empty
; If (unknown_cond, [var_assign_int "b" 2], [var_assign_int "b" 1]) ; If (unknown_cond, [var_assign_int "b" 2], [var_assign_int "b" 1])
; invariant "{ b }" ; invariant "normal:{ b }, exn:{ }"
; id_assign_var "a" "b" ] ) ; 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" ; ( "loop_as_if2"
, [ invariant "{ b }" , [ invariant "normal:{ b }, exn:{ }"
; While (unknown_cond, [var_assign_int "b" 1]) ; While (unknown_cond, [var_assign_int "b" 1])
; invariant "{ b }" ; invariant "normal:{ b }, exn:{ }"
; id_assign_var "a" "b" ] ) ; id_assign_var "a" "b" ] )
; ( "loop_before_after" ; ( "loop_before_after"
, [ invariant "{ b, d }" , [ invariant "normal:{ b, d }, exn:{ }"
; While (unknown_cond, [id_assign_var "b" "d"]) ; While (unknown_cond, [id_assign_var "b" "d"])
; invariant "{ b }" ; invariant "normal:{ b }, exn:{ }"
; id_assign_var "a" "b" ] ) ] ; id_assign_var "a" "b" ] ) ]
|> TestInterpreter.create_tests |> TestInterpreter.create_tests
(fun summary -> Summary.get_proc_desc summary) (fun summary -> Summary.get_proc_desc summary)
~initial:Liveness.Domain.empty ~initial:Liveness.Domain.bottom
in in
"liveness_test_suite" >::: test_list "liveness_test_suite" >::: test_list

53
infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp
Unescape View File

@ -403,7 +403,7 @@ class Exceptions {
return 0; return 0;
} }
int FN_unreachable_catch_bad() { int unreachable_catch_bad() {
int i = 1; int i = 1;
try { try {
} catch (...) { } catch (...) {
@ -455,7 +455,7 @@ class Exceptions {
// currently, the only transition to the catch block is at the end of the try // currently, the only transition to the catch block is at the end of the try
// block. See T28898377 // 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; int i = 1;
try { try {
if (b1) { if (b1) {
@ -538,6 +538,55 @@ class Exceptions {
} }
return 3; 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}; } void init_in_binop_bad(int x) { x = -x & ~int{0}; }

4
infer/tests/codetoanalyze/cpp/liveness/issues.exp
Unescape View File

@ -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::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::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, 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] codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::binaryConditional_bad, 4, DEAD_STORE, no_bucket, ERROR, [Write of unused value]

47
infer/tests/codetoanalyze/cpp/shared/exceptions/Exceptions.cpp.dot
Unescape View File

@ -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_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" [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] "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_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_9" -> "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_10" [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_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_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_10" -> "FN_deref_null_in_catch_bad#9297890526029657977.c83eec7c9ab8ce2e38ddbc08f8c3dfeb_6" ;
"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" [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] "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_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_17" [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: CXXTry \n CATCH_ENTRY; [line 58, column 3]\n " shape="box"]
"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_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] "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_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] "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_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" ;
} }

Write Preview
Loading…
Cancel
Save