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

[Uninit][8/13] Rename UninitVars to MaybeUninitVars

Browse Source 
Reviewed By: jeremydubreil

Differential Revision: D10250193

fbshipit-source-id: bd4cd332f
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 5679105c15
commit 62b1f39540
2 changed files with 82 additions and 62 deletions
Show Stats Download Patch File Download Diff File

74
infer/src/checkers/uninit.ml
Unescape View File

@ -12,9 +12,9 @@ module L = Logging
(** Forward analysis to compute uninitialized variables at each program point *) (** Forward analysis to compute uninitialized variables at each program point *)
module D = UninitDomain.Domain module D = UninitDomain.Domain
module UninitVars = AbstractDomain.FiniteSet (AccessExpression) module MaybeUninitVars = UninitDomain.MaybeUninitVars
module AliasedVars = AbstractDomain.FiniteSet (UninitDomain.VarPair) module AliasedVars = AbstractDomain.FiniteSet (UninitDomain.VarPair)
module RecordDomain = UninitDomain.Record (UninitVars) (AliasedVars) (D) module RecordDomain = UninitDomain.Record (MaybeUninitVars) (AliasedVars) (D)
module Payload = SummaryPayload.Make (struct module Payload = SummaryPayload.Make (struct
type t = UninitDomain.Summary.t type t = UninitDomain.Summary.t
@ -63,13 +63,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let get_formals pname = Ondemand.get_proc_desc pname |> Option.map ~f:Procdesc.get_formals let get_formals pname = Ondemand.get_proc_desc pname |> Option.map ~f:Procdesc.get_formals
let should_report_var pdesc tenv uninit_vars access_expr = let should_report_var pdesc tenv maybe_uninit_vars access_expr =
let base = AccessExpression.get_base access_expr in let base = AccessExpression.get_base access_expr in
match (AccessExpression.get_typ access_expr tenv, base) with match (AccessExpression.get_typ access_expr tenv, base) with
| Some typ, (Var.ProgramVar pv, _) -> | Some typ, (Var.ProgramVar pv, _) ->
(not (Pvar.is_frontend_tmp pv)) (not (Pvar.is_frontend_tmp pv))
&& (not (Procdesc.is_captured_var pdesc pv)) && (not (Procdesc.is_captured_var pdesc pv))
&& D.mem access_expr uninit_vars && should_report_on_type typ && MaybeUninitVars.mem access_expr maybe_uninit_vars
&& should_report_on_type typ
| _, _ -> | _, _ ->
false false
@ -99,14 +100,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|| is_array_element_passed_by_ref callee_formals t access_expr idx || is_array_element_passed_by_ref callee_formals t access_expr idx
let report_on_function_params pdesc tenv uninit_vars actuals loc summary callee_formals_opt = let report_on_function_params pdesc tenv maybe_uninit_vars actuals loc summary callee_formals_opt
=
List.iteri List.iteri
~f:(fun idx e -> ~f:(fun idx e ->
match e with match e with
| HilExp.AccessExpression access_expr -> | HilExp.AccessExpression access_expr ->
let _, t = AccessExpression.get_base access_expr in let _, t = AccessExpression.get_base access_expr in
if if
should_report_var pdesc tenv uninit_vars access_expr should_report_var pdesc tenv maybe_uninit_vars access_expr
&& (not (Typ.is_pointer t)) && (not (Typ.is_pointer t))
&& not && not
(Option.exists callee_formals_opt ~f:(fun callee_formals -> (Option.exists callee_formals_opt ~f:(fun callee_formals ->
@ -160,9 +162,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Some {pre= initialized_formal_params; post= _} -> ( | Some {pre= initialized_formal_params; post= _} -> (
match init_nth_actual_param call idx initialized_formal_params with match init_nth_actual_param call idx initialized_formal_params with
| Some nth_formal -> | Some nth_formal ->
let acc' = D.remove access_expr acc in let acc' = MaybeUninitVars.remove access_expr acc in
let base = AccessExpression.get_base access_expr in let base = AccessExpression.get_base access_expr in
if remove_fields then D.remove_init_fields base nth_formal acc' initialized_formal_params if remove_fields then
MaybeUninitVars.remove_init_fields base nth_formal acc' initialized_formal_params
else acc' else acc'
| _ -> | _ ->
acc ) acc )
@ -195,13 +198,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in in
match instr with match instr with
| Assign (lhs_access_expr, rhs_expr, loc) -> | Assign (lhs_access_expr, rhs_expr, loc) ->
let uninit_vars' = D.remove lhs_access_expr astate.uninit_vars in let maybe_uninit_vars' = MaybeUninitVars.remove lhs_access_expr astate.maybe_uninit_vars in
let uninit_vars = let maybe_uninit_vars =
if AccessExpression.is_base lhs_access_expr then if AccessExpression.is_base lhs_access_expr then
(* if we assign to the root of a struct then we need to remove all the fields *) (* if we assign to the root of a struct then we need to remove all the fields *)
let lhs_base = AccessExpression.get_base lhs_access_expr in let lhs_base = AccessExpression.get_base lhs_access_expr in
D.remove_all_fields tenv lhs_base uninit_vars' |> D.remove_dereference_access lhs_base MaybeUninitVars.remove_all_fields tenv lhs_base maybe_uninit_vars'
else uninit_vars' |> MaybeUninitVars.remove_dereference_access lhs_base
else maybe_uninit_vars'
in in
let prepost = update_prepost lhs_access_expr rhs_expr in let prepost = update_prepost lhs_access_expr rhs_expr in
(* check on lhs_typ to avoid false positive when assigning a pointer to another *) (* check on lhs_typ to avoid false positive when assigning a pointer to another *)
@ -214,33 +218,35 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in in
( match rhs_expr with ( match rhs_expr with
| AccessExpression rhs_access_expr -> | AccessExpression rhs_access_expr ->
if should_report_var pdesc tenv uninit_vars rhs_access_expr && is_lhs_not_a_pointer if
should_report_var pdesc tenv maybe_uninit_vars rhs_access_expr
&& is_lhs_not_a_pointer
then report_intra rhs_access_expr loc summary then report_intra rhs_access_expr loc summary
| _ -> | _ ->
() ) ; () ) ;
{astate with uninit_vars; prepost} {astate with maybe_uninit_vars; prepost}
| Call (_, Direct callee_pname, _, _, _) | Call (_, Direct callee_pname, _, _, _)
when Typ.Procname.equal callee_pname BuiltinDecl.objc_cpp_throw -> when Typ.Procname.equal callee_pname BuiltinDecl.objc_cpp_throw ->
{astate with uninit_vars= D.empty} {astate with maybe_uninit_vars= MaybeUninitVars.empty}
| Call (_, HilInstr.Direct call, [HilExp.AccessExpression (AddressOf (Base base))], _, _) | Call (_, HilInstr.Direct call, [HilExp.AccessExpression (AddressOf (Base base))], _, _)
when is_dummy_constructor_of_a_struct call -> when is_dummy_constructor_of_a_struct call ->
(* if it's a default constructor, we use the following heuristic: we assume that it initializes (* if it's a default constructor, we use the following heuristic: we assume that it initializes
correctly all fields when there is an implementation of the constructor that initilizes at least one correctly all fields when there is an implementation of the constructor that initilizes at least one
field. If there is no explicit implementation we cannot assume fields are initialized *) field. If there is no explicit implementation we cannot assume fields are initialized *)
if function_initializes_some_formal_params pdesc call then if function_initializes_some_formal_params pdesc call then
let uninit_vars' = let maybe_uninit_vars' =
(* in HIL/SIL the default constructor has only one param: the struct *) (* in HIL/SIL the default constructor has only one param: the struct *)
D.remove_all_fields tenv base astate.uninit_vars MaybeUninitVars.remove_all_fields tenv base astate.maybe_uninit_vars
in in
{astate with uninit_vars= uninit_vars'} {astate with maybe_uninit_vars= maybe_uninit_vars'}
else astate else astate
| Call (_, call, actuals, _, loc) -> | Call (_, call, actuals, _, loc) ->
(* in case of intraprocedural only analysis we assume that parameters passed by reference (* in case of intraprocedural only analysis we assume that parameters passed by reference
to a function will be initialized inside that function *) to a function will be initialized inside that function *)
let pname_opt = match call with Direct pname -> Some pname | Indirect _ -> None in let pname_opt = match call with Direct pname -> Some pname | Indirect _ -> None in
let callee_formals_opt = Option.bind pname_opt ~f:get_formals in let callee_formals_opt = Option.bind pname_opt ~f:get_formals in
let uninit_vars = let maybe_uninit_vars =
List.foldi ~init:astate.uninit_vars actuals ~f:(fun idx acc actual_exp -> List.foldi ~init:astate.maybe_uninit_vars actuals ~f:(fun idx acc actual_exp ->
match actual_exp with match actual_exp with
| HilExp.AccessExpression access_expr -> ( | HilExp.AccessExpression access_expr -> (
let access_expr_to_remove = let access_expr_to_remove =
@ -249,7 +255,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
match AccessExpression.get_base access_expr with match AccessExpression.get_base access_expr with
| _, {Typ.desc= Tarray _} | _, {Typ.desc= Tarray _}
when Option.exists pname_opt ~f:Models.is_initializing_all_args -> when Option.exists pname_opt ~f:Models.is_initializing_all_args ->
D.remove access_expr acc MaybeUninitVars.remove access_expr acc
| _, t | _, t
(* Access to a field of a struct or an element of an array by reference *) (* Access to a field of a struct or an element of an array by reference *)
when Option.exists when Option.exists
@ -259,39 +265,43 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Some pname when Config.uninit_interproc -> | Some pname when Config.uninit_interproc ->
remove_initialized_params pdesc pname acc idx access_expr_to_remove false remove_initialized_params pdesc pname acc idx access_expr_to_remove false
| _ -> | _ ->
D.remove access_expr_to_remove acc ) MaybeUninitVars.remove access_expr_to_remove acc )
| base | base
when Option.value_map ~default:false ~f:Typ.Procname.is_constructor pname_opt when Option.value_map ~default:false ~f:Typ.Procname.is_constructor pname_opt
-> ->
D.remove_all_fields tenv base (D.remove access_expr_to_remove acc) MaybeUninitVars.remove_all_fields tenv base
(MaybeUninitVars.remove access_expr_to_remove acc)
| (_, {Typ.desc= Tptr _}) as base -> ( | (_, {Typ.desc= Tptr _}) as base -> (
match pname_opt with match pname_opt with
| Some pname when Config.uninit_interproc -> | Some pname when Config.uninit_interproc ->
remove_initialized_params pdesc pname acc idx access_expr_to_remove true remove_initialized_params pdesc pname acc idx access_expr_to_remove true
| _ -> | _ ->
D.remove access_expr_to_remove acc MaybeUninitVars.remove access_expr_to_remove acc
|> D.remove_all_fields tenv base |> D.remove_all_array_elements base |> MaybeUninitVars.remove_all_fields tenv base
|> D.remove_dereference_access base ) |> MaybeUninitVars.remove_all_array_elements base
|> MaybeUninitVars.remove_dereference_access base )
| _ -> | _ ->
acc ) acc )
| HilExp.Closure (_, apl) -> | HilExp.Closure (_, apl) ->
(* remove the captured variables of a block/lambda *) (* remove the captured variables of a block/lambda *)
List.fold List.fold
~f:(fun acc' (base, _) -> D.remove (AccessExpression.Base base) acc') ~f:(fun acc' (base, _) ->
MaybeUninitVars.remove (AccessExpression.Base base) acc' )
~init:acc apl ~init:acc apl
| _ -> | _ ->
acc ) acc )
in in
( match call with ( match call with
| Direct _ -> | Direct _ ->
report_on_function_params pdesc tenv uninit_vars actuals loc summary callee_formals_opt report_on_function_params pdesc tenv maybe_uninit_vars actuals loc summary
callee_formals_opt
| Indirect _ -> | Indirect _ ->
() ) ; () ) ;
{astate with uninit_vars} {astate with maybe_uninit_vars}
| Assume (expr, _, _, loc) -> | Assume (expr, _, _, loc) ->
( match expr with ( match expr with
| AccessExpression rhs_access_expr -> | AccessExpression rhs_access_expr ->
if should_report_var pdesc tenv astate.uninit_vars rhs_access_expr then if should_report_var pdesc tenv astate.maybe_uninit_vars rhs_access_expr then
report_intra rhs_access_expr loc summary report_intra rhs_access_expr loc summary
| _ -> | _ ->
() ) ; () ) ;
@ -337,9 +347,9 @@ end
let checker {Callbacks.tenv; summary; proc_desc} : Summary.t = let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
(* start with empty set of uninit local vars and empty set of init formal params *) (* start with empty set of uninit local vars and empty set of init formal params *)
let uninit_vars = Initial.get_locals tenv proc_desc in let maybe_uninit_vars = Initial.get_locals tenv proc_desc in
let initial = let initial =
{ RecordDomain.uninit_vars= UninitVars.of_list uninit_vars { RecordDomain.maybe_uninit_vars= MaybeUninitVars.of_list maybe_uninit_vars
; aliased_vars= AliasedVars.empty ; aliased_vars= AliasedVars.empty
; prepost= {UninitDomain.pre= D.empty; post= D.empty} } ; prepost= {UninitDomain.pre= D.empty; post= D.empty} }
in in

70
infer/src/checkers/uninitDomain.ml
Unescape View File

@ -7,12 +7,12 @@
open! IStd open! IStd
module F = Format module F = Format
module Domain = AbstractDomain.InvertedSet (AccessExpression)
(** Forward analysis to compute uninitialized variables at each program point *) module MaybeUninitVars = struct
module Domain = struct include AbstractDomain.FiniteSet (AccessExpression)
include AbstractDomain.InvertedSet (AccessExpression)
let remove_init_fields base formal_var uninit_vars init_fields = let remove_init_fields base formal_var maybe_uninit_vars init_fields =
let subst_formal_actual_fields actual_base_var initialized_fields = let subst_formal_actual_fields actual_base_var initialized_fields =
map map
(fun access_expr -> (fun access_expr ->
@ -34,39 +34,39 @@ module Domain = struct
in in
match base with match base with
| actual_base_var, {Typ.desc= Tptr ({Typ.desc= Tstruct _}, _) | Tstruct _} -> | actual_base_var, {Typ.desc= Tptr ({Typ.desc= Tstruct _}, _) | Tstruct _} ->
diff uninit_vars (subst_formal_actual_fields actual_base_var init_fields) diff maybe_uninit_vars (subst_formal_actual_fields actual_base_var init_fields)
| _ -> | _ ->
uninit_vars maybe_uninit_vars
let remove_all_fields tenv base uninit_vars = let remove_all_fields tenv base maybe_uninit_vars =
match base with match base with
| _, {Typ.desc= Tptr ({Typ.desc= Tstruct name_struct}, _)} | _, {Typ.desc= Tstruct name_struct} | _, {Typ.desc= Tptr ({Typ.desc= Tstruct name_struct}, _)} | _, {Typ.desc= Tstruct name_struct}
-> ( -> (
match Tenv.lookup tenv name_struct with match Tenv.lookup tenv name_struct with
| Some {fields} -> | Some {fields} ->
List.fold fields ~init:uninit_vars ~f:(fun acc (fn, _, _) -> List.fold fields ~init:maybe_uninit_vars ~f:(fun acc (fn, _, _) ->
remove (AccessExpression.FieldOffset (Base base, fn)) acc ) remove (AccessExpression.FieldOffset (Base base, fn)) acc )
| _ -> | _ ->
uninit_vars ) maybe_uninit_vars )
| _ -> | _ ->
uninit_vars maybe_uninit_vars
let remove_dereference_access base uninit_vars = let remove_dereference_access base maybe_uninit_vars =
match base with match base with
| _, {Typ.desc= Tptr _} -> | _, {Typ.desc= Tptr _} ->
remove (AccessExpression.Dereference (Base base)) uninit_vars remove (AccessExpression.Dereference (Base base)) maybe_uninit_vars
| _ -> | _ ->
uninit_vars maybe_uninit_vars
let remove_all_array_elements base uninit_vars = let remove_all_array_elements base maybe_uninit_vars =
match base with match base with
| _, {Typ.desc= Tptr (elt, _)} -> | _, {Typ.desc= Tptr (elt, _)} ->
remove (AccessExpression.ArrayOffset (Base base, elt, [])) uninit_vars remove (AccessExpression.ArrayOffset (Base base, elt, [])) maybe_uninit_vars
| _ -> | _ ->
uninit_vars maybe_uninit_vars
end end
type 'a prepost = {pre: 'a; post: 'a} type 'a prepost = {pre: 'a; post: 'a}
@ -83,15 +83,19 @@ module Record
(Domain3 : AbstractDomain.S) = (Domain3 : AbstractDomain.S) =
struct struct
type astate = type astate =
{uninit_vars: Domain1.astate; aliased_vars: Domain2.astate; prepost: Domain3.astate prepost} { maybe_uninit_vars: Domain1.astate
; aliased_vars: Domain2.astate
; prepost: Domain3.astate prepost }
let ( <= ) ~lhs ~rhs = let ( <= ) ~lhs ~rhs =
if phys_equal lhs rhs then true if phys_equal lhs rhs then true
else else
let {uninit_vars= lhs_uv; aliased_vars= lhs_av; prepost= {pre= lhs_pre; post= lhs_post}} = let {maybe_uninit_vars= lhs_uv; aliased_vars= lhs_av; prepost= {pre= lhs_pre; post= lhs_post}}
=
lhs lhs
in in
let {uninit_vars= rhs_uv; aliased_vars= rhs_av; prepost= {pre= rhs_pre; post= rhs_post}} = let {maybe_uninit_vars= rhs_uv; aliased_vars= rhs_av; prepost= {pre= rhs_pre; post= rhs_post}}
=
rhs rhs
in in
Domain1.( <= ) ~lhs:lhs_uv ~rhs:rhs_uv Domain1.( <= ) ~lhs:lhs_uv ~rhs:rhs_uv
@ -103,9 +107,13 @@ struct
let join astate1 astate2 = let join astate1 astate2 =
if phys_equal astate1 astate2 then astate1 if phys_equal astate1 astate2 then astate1
else else
let {uninit_vars= uv1; aliased_vars= av1; prepost= {pre= pre1; post= post1}} = astate1 in let {maybe_uninit_vars= uv1; aliased_vars= av1; prepost= {pre= pre1; post= post1}} =
let {uninit_vars= uv2; aliased_vars= av2; prepost= {pre= pre2; post= post2}} = astate2 in astate1
{ uninit_vars= Domain1.join uv1 uv2 in
let {maybe_uninit_vars= uv2; aliased_vars= av2; prepost= {pre= pre2; post= post2}} =
astate2
in
{ maybe_uninit_vars= Domain1.join uv1 uv2
; aliased_vars= Domain2.join av1 av2 ; aliased_vars= Domain2.join av1 av2
; prepost= {pre= Domain3.join pre1 pre2; post= Domain3.join post1 post2} } ; prepost= {pre= Domain3.join pre1 pre2; post= Domain3.join post1 post2} }
@ -113,24 +121,26 @@ struct
let widen ~prev ~next ~num_iters = let widen ~prev ~next ~num_iters =
if phys_equal prev next then prev if phys_equal prev next then prev
else else
let {uninit_vars= prev_uv; aliased_vars= prev_av; prepost= {pre= prev_pre; post= prev_post}} let { maybe_uninit_vars= prev_uv
= ; aliased_vars= prev_av
; prepost= {pre= prev_pre; post= prev_post} } =
prev prev
in in
let {uninit_vars= next_uv; aliased_vars= next_av; prepost= {pre= next_pre; post= next_post}} let { maybe_uninit_vars= next_uv
= ; aliased_vars= next_av
; prepost= {pre= next_pre; post= next_post} } =
next next
in in
{ uninit_vars= Domain1.widen ~prev:prev_uv ~next:next_uv ~num_iters { maybe_uninit_vars= Domain1.widen ~prev:prev_uv ~next:next_uv ~num_iters
; aliased_vars= Domain2.widen ~prev:prev_av ~next:next_av ~num_iters ; aliased_vars= Domain2.widen ~prev:prev_av ~next:next_av ~num_iters
; prepost= ; prepost=
{ pre= Domain3.widen ~prev:prev_pre ~next:next_pre ~num_iters { pre= Domain3.widen ~prev:prev_pre ~next:next_pre ~num_iters
; post= Domain3.widen ~prev:prev_post ~next:next_post ~num_iters } } ; post= Domain3.widen ~prev:prev_post ~next:next_post ~num_iters } }
let pp fmt {uninit_vars= uv; aliased_vars= av; prepost= {pre; post}} = let pp fmt {maybe_uninit_vars= uv; aliased_vars= av; prepost= {pre; post}} =
F.fprintf fmt "@\n uninit_vars: %a @\n aliased_vars: %a @\n prepost: (%a, %a)" Domain1.pp uv F.fprintf fmt "@\n maybe_uninit_vars: %a @\n aliased_vars: %a @\n prepost: (%a, %a)" Domain1.pp
Domain2.pp av Domain3.pp pre Domain3.pp post uv Domain2.pp av Domain3.pp pre Domain3.pp post
end end
module Summary = struct module Summary = struct

Write Preview
Loading…
Cancel
Save