diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index 8acd11abb..37d2a1dcc 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -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 diff --git a/infer/src/checkers/uninitDomain.ml b/infer/src/checkers/uninitDomain.ml index 6c3900a04..46e4957c0 100644 --- a/infer/src/checkers/uninitDomain.ml +++ b/infer/src/checkers/uninitDomain.ml @@ -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