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

Uninit nits

Browse Source 
Reviewed By: jvillard

Differential Revision: D10119326

fbshipit-source-id: e2a50bae5
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent ded6bd8ba4
commit aa6f5b2ed5
2 changed files with 40 additions and 31 deletions
Show Stats Download Patch File Download Diff File

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

@ -249,9 +249,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
&& ( (not (is_pointer_assignment tenv access_expr rhs))
|| not (AccessExpression.is_base access_expr) )
then
let pre' = D.add access_expr (fst astate.prepost) in
let post = snd astate.prepost in
(pre', post)
let pre = D.add access_expr astate.prepost.UninitDomain.pre in
{astate.prepost with pre}
else astate.prepost
in
match instr with
@ -362,7 +361,7 @@ end
module CFG = ProcCfg.Normal
module Analyzer = LowerHil.MakeAbstractInterpreter (CFG) (TransferFunctions)
let get_locals cfg tenv pdesc =
let get_locals tenv pdesc =
List.fold
~f:(fun acc (var_data : ProcAttributes.var_data) ->
let pvar = Pvar.mk var_data.name (Procdesc.get_proc_name pdesc) in
@ -390,25 +389,22 @@ let get_locals cfg tenv pdesc =
base_access_expr :: AccessExpression.Dereference base_access_expr :: acc
| _ ->
base_access_expr :: acc )
~init:[] (Procdesc.get_locals cfg)
~init:[] (Procdesc.get_locals pdesc)
let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
let cfg = CFG.from_pdesc proc_desc in
(* 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 formal_map = FormalMap.make proc_desc in
let uninit_vars = get_locals cfg tenv proc_desc in
let uninit_vars = get_locals tenv proc_desc in
let initial =
{ RecordDomain.uninit_vars= UninitVars.of_list uninit_vars
; RecordDomain.aliased_vars= AliasedVars.empty
; RecordDomain.prepost= (D.empty, D.empty) }
; aliased_vars= AliasedVars.empty
; prepost= {UninitDomain.pre= D.empty; post= D.empty} }
in
let proc_data = ProcData.make proc_desc tenv (formal_map, summary) in
match Analyzer.compute_post proc_data ~initial with
| Some
{RecordDomain.uninit_vars= _; RecordDomain.aliased_vars= _; RecordDomain.prepost= pre, post}
->
Payload.update_summary {pre; post} summary
| Some {RecordDomain.prepost} ->
Payload.update_summary prepost summary
| None ->
if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then (
L.internal_error "Uninit analyzer failed to compute post for %a" Typ.Procname.pp

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

@ -11,9 +11,11 @@ module F = Format
(** Forward analysis to compute uninitialized variables at each program point *)
module Domain = AbstractDomain.InvertedSet (AccessExpression)
type 'a prepost = {pre: 'a; post: 'a}
(* pre = set of parameters initialized inside the procedure;
post = set of uninit local variables of the procedure *)
type summary = {pre: Domain.t; post: Domain.t}
type summary = Domain.t prepost
module VarPair = struct
type t = Var.t * Var.t [@@deriving compare]
@ -31,41 +33,52 @@ module Record
(Domain3 : AbstractDomain.S) =
struct
type astate =
{ uninit_vars: Domain1.astate
; aliased_vars: Domain2.astate
; prepost: Domain3.astate * Domain3.astate }
{uninit_vars: Domain1.astate; aliased_vars: Domain2.astate; prepost: Domain3.astate prepost}
let ( <= ) ~lhs:({uninit_vars= lhs_uv; aliased_vars= lhs_av; prepost= lhs_pp} as lhs)
~rhs:({uninit_vars= rhs_uv; aliased_vars= rhs_av; prepost= rhs_pp} as rhs) =
let ( <= ) ~lhs ~rhs =
if phys_equal lhs rhs then true
else
let {uninit_vars= lhs_uv; aliased_vars= lhs_av; prepost= {pre= lhs_pre; post= lhs_post}} =
lhs
in
let {uninit_vars= rhs_uv; aliased_vars= rhs_av; prepost= {pre= rhs_pre; post= rhs_post}} =
rhs
in
Domain1.( <= ) ~lhs:lhs_uv ~rhs:rhs_uv
&& Domain2.( <= ) ~lhs:lhs_av ~rhs:rhs_av
&& Domain3.( <= ) ~lhs:(fst lhs_pp) ~rhs:(fst rhs_pp)
&& Domain3.( <= ) ~lhs:(snd lhs_pp) ~rhs:(snd rhs_pp)
&& Domain3.( <= ) ~lhs:lhs_pre ~rhs:rhs_pre
&& Domain3.( <= ) ~lhs:lhs_post ~rhs:rhs_post
let join ({uninit_vars= uv1; aliased_vars= av1; prepost= pp1} as astate1)
({uninit_vars= uv2; aliased_vars= av2; prepost= pp2} as astate2) =
let join astate1 astate2 =
if phys_equal astate1 astate2 then astate1
else
let {uninit_vars= uv1; aliased_vars= av1; prepost= {pre= pre1; post= post1}} = astate1 in
let {uninit_vars= uv2; aliased_vars= av2; prepost= {pre= pre2; post= post2}} = astate2 in
{ uninit_vars= Domain1.join uv1 uv2
; aliased_vars= Domain2.join av1 av2
; prepost= (Domain3.join (fst pp1) (fst pp2), Domain3.join (snd pp1) (snd pp2)) }
; prepost= {pre= Domain3.join pre1 pre2; post= Domain3.join post1 post2} }
let widen ~prev:({uninit_vars= prev_uv; aliased_vars= prev_av; prepost= prev_pp} as prev)
~next:({uninit_vars= next_uv; aliased_vars= next_av; prepost= next_pp} as next) ~num_iters =
let widen ~prev ~next ~num_iters =
if phys_equal prev next then prev
else
let {uninit_vars= prev_uv; aliased_vars= prev_av; prepost= {pre= prev_pre; post= prev_post}}
=
prev
in
let {uninit_vars= next_uv; aliased_vars= next_av; prepost= {pre= next_pre; post= next_post}}
=
next
in
{ uninit_vars= Domain1.widen ~prev:prev_uv ~next:next_uv ~num_iters
; aliased_vars= Domain2.widen ~prev:prev_av ~next:next_av ~num_iters
; prepost=
( Domain3.widen ~prev:(fst prev_pp) ~next:(fst next_pp) ~num_iters
, Domain3.widen ~prev:(snd prev_pp) ~next:(snd next_pp) ~num_iters ) }
{ pre= Domain3.widen ~prev:prev_pre ~next:next_pre ~num_iters
; post= Domain3.widen ~prev:prev_post ~next:next_post ~num_iters } }
let pp fmt {uninit_vars= uv; aliased_vars= av; prepost= pp} =
let pp fmt {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
Domain2.pp av Domain3.pp (fst pp) Domain3.pp (snd pp)
Domain2.pp av Domain3.pp pre Domain3.pp post
end

Write Preview
Loading…
Cancel
Save