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

[uninit] convert to HIL

Browse Source 
Summary: This will make it easier to generalize the checker to handling uninitialized struct fields.

Reviewed By: ddino

Differential Revision: D6099484

fbshipit-source-id: b9c534b
master
Sam Blackshear 7 years ago committed by Facebook Github Bot
parent 3c48a3f38a
commit b826b16a6f
1 changed files with 75 additions and 152 deletions
Show Stats Download Patch File Download Diff File

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

@ -30,11 +30,75 @@ end)
let intraprocedural_only = true
module TransferFunctions (CFG : ProcCfg.S) = struct
module CFG = CFG
module Domain = RecordDomain
type extras = FormalMap.t
let exec_instr (astate: Domain.astate) {ProcData.extras} _ (instr: HilInstr.t) =
match instr with
| Assign (((lhs_var, _), _), HilExp.AccessPath ((rhs_var, rhs_typ as rhs_base), _), _)
-> let uninit_vars = D.remove lhs_var astate.uninit_vars in
let prepost =
if FormalMap.is_formal rhs_base extras
&& match rhs_typ.desc with Typ.Tptr _ -> true | _ -> false
then
let pre' = D.add rhs_var (fst astate.prepost) in
let post = snd astate.prepost in
(pre', post)
else astate.prepost
in
{astate with uninit_vars; prepost}
| Assign (((lhs_var, _), _), _, _)
-> let uninit_vars = D.remove lhs_var astate.uninit_vars in
{astate with uninit_vars}
| Call (_, _, actuals, _, _)
-> (* in case of intraprocedural only analysis we assume that parameters passed by reference
to a function will be initialized inside that function *)
let uninit_vars =
List.fold
~f:(fun acc actual_exp ->
match actual_exp with
| HilExp.AccessPath ((actual_var, {Typ.desc= Tptr _}), _)
-> D.remove actual_var acc
| _
-> acc)
~init:astate.uninit_vars actuals
in
{astate with uninit_vars}
| Assume _
-> astate
end
module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Normal)
module Analyzer = AbstractInterpreter.Make (CFG) (LowerHil.MakeDefault (TransferFunctions))
let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary =
let cfg = CFG.from_pdesc proc_desc in
(* 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 =
List.map
~f:(fun (name, _) ->
let pvar = Pvar.mk name (Procdesc.get_proc_name proc_desc) in
Var.of_pvar pvar)
(Procdesc.get_locals cfg)
in
let init =
( { RecordDomain.uninit_vars= UninitVars.of_list uninit_vars
; RecordDomain.aliased_vars= AliasedVars.empty
; RecordDomain.prepost= (D.empty, D.empty) }
, IdAccessPathMapDomain.empty )
in
let invariant_map =
Analyzer.exec_cfg cfg (ProcData.make proc_desc tenv formal_map) ~initial:init ~debug:true
in
(* Check if an expression is in set of variables *)
let exp_in_set exp vset =
let _, pvars = Exp.get_vars exp in
List.exists ~f:(fun pv -> D.mem (Var.of_pvar pv) vset) pvars
in
let zip_actual_formal_params callee_pname actual_params =
match Ondemand.get_proc_desc callee_pname with
| Some pdesc
@ -43,7 +107,7 @@ let zip_actual_formal_params callee_pname actual_params =
(List.zip actual formals, actual)
| _
-> (None, [])
in
let deref_actual_params callee_pname actual_params deref_formal_params =
match zip_actual_formal_params callee_pname actual_params with
| None, _
@ -54,149 +118,6 @@ let deref_actual_params callee_pname actual_params deref_formal_params =
let fe = Exp.Lvar (Pvar.mk f callee_pname) in
if exp_in_set fe deref_formal_params then a :: acc else acc)
~init:[] assoc_actual_formal
module TransferFunctions (CFG : ProcCfg.S) = struct
module CFG = CFG
(* a state is a pair: ({set of uninitialized locals}, {set of written formal params}) *)
(* module Domain = AbstractDomain.Pair (UninitVars) (PrePost)*)
module Domain = RecordDomain
type extras = ProcData.no_extras
let apply_fun_exp_set f exp vset =
let _, pvars = Exp.get_vars exp in
List.fold ~f:(fun acc_set pvar -> f (Var.of_pvar pvar) acc_set) ~init:vset pvars
let exp_add_set exp vset = apply_fun_exp_set D.add exp vset
let exp_remove_set exp vset = apply_fun_exp_set D.remove exp vset
let set_difference set1 set2 =
List.fold ~f:(fun acc_set e -> exp_remove_set e acc_set) ~init:set1 set2
(* check if its a basic type *)
let rec is_basic_typ t =
match t.Typ.desc with
| Typ.Tint _ | Typ.Tfloat _ | Typ.Tvoid
-> true
| Typ.Tptr (t', _)
-> is_basic_typ t'
| _
-> false
(* returns the formal parameter of a procedure that have a pointer type *)
let ptr_formals pdesc =
let proc_name = Procdesc.get_proc_name pdesc in
let is_ptr (_, t) = match t.Typ.desc with Typ.Tptr _ -> true | _ -> false in
let pfs = List.filter ~f:is_ptr (Procdesc.get_formals pdesc) in
List.map ~f:(fun (name, _) -> Exp.Lvar (Pvar.mk name proc_name)) pfs
(* Update the set of written formals when it finds a sequence
n$0=*&i;
....
*n$0=..;
*)
let update_state_formal node pdesc formal_set =
let ptr_formals = ptr_formals pdesc in
let ids_assigned_to_formals, dereferenced_ids =
List.fold
~f:(fun (acc1, acc2) (i, _) ->
match i with
| Sil.Load (lhs_id, rhs_exp, _, _) when List.mem ptr_formals rhs_exp ~equal:Exp.equal
-> ((lhs_id, rhs_exp) :: acc1, acc2)
| Sil.Store (Exp.Var lhs_id, _, _, _)
-> (acc1, lhs_id :: acc2)
| _
-> (acc1, acc2))
(CFG.instr_ids node) ~init:([], [])
in
List.fold
~f:(fun acc_set (id, formal_param) ->
if List.mem dereferenced_ids id ~equal:Ident.equal then exp_add_set formal_param acc_set
else acc_set)
ids_assigned_to_formals ~init:formal_set
let exec_instr
( {Domain.uninit_vars= uninit; Domain.aliased_vars= _; Domain.prepost= pre, wformals} as
astate ) {ProcData.pdesc} node = function
| Sil.Load (_, rhs_exp, _, _)
-> let post = update_state_formal node pdesc wformals in
let set_ptr_formals = ptr_formals pdesc in
let pre' =
if List.mem set_ptr_formals ~equal:Exp.equal rhs_exp && not (exp_in_set rhs_exp post)
then exp_add_set rhs_exp pre
else pre
in
{astate with prepost= (pre', post)}
| Sil.Store (lhs_exp, _, rhs_exp, _)
-> if exp_in_set rhs_exp uninit then astate
else {astate with Domain.uninit_vars= exp_remove_set lhs_exp uninit}
| Sil.Call (ret_id, Exp.Const Const.Cfun callee_pname, actual_params, _, _)
when not intraprocedural_only
-> (
let astate' =
Option.value_map
~f:(fun (ret_id, _) ->
{astate with Domain.uninit_vars= exp_remove_set (Exp.Var ret_id) uninit})
~default:astate ret_id
in
match
( zip_actual_formal_params callee_pname actual_params
, Summary.read_summary pdesc callee_pname )
with
| (Some assoc_actual_formal, actual), Some {pre= _; post= wformals_callee}
-> let initialized_actual_params =
List.filter
~f:(fun a ->
match List.Assoc.find assoc_actual_formal ~equal:Exp.equal a with
| Some fp
-> D.mem (Var.of_pvar (Pvar.mk fp callee_pname)) wformals_callee
| None
-> false)
actual
in
let uninit' = set_difference uninit initialized_actual_params in
{astate with Domain.uninit_vars= uninit'; Domain.prepost= astate'.prepost}
| _, _
-> L.(debug Linters Medium)
"Warning: unable to deal with callee '%s' summary@\n"
(Typ.Procname.to_string callee_pname) ;
astate' )
| Sil.Call (_, _, actual_params, _, _)
-> (* in case of intraprocedural only analysis we assume that parameters
passed by reference to a function will be initialized inside that function *)
let actual_passed_by_ref =
List.fold
~f:(fun acc (e, t) -> match t.Typ.desc with Typ.Tptr _ -> e :: acc | _ -> acc)
~init:[] actual_params
in
let uninit' = set_difference uninit actual_passed_by_ref in
{astate with Domain.uninit_vars= uninit'}
| Sil.Declare_locals (pvar_list, _)
-> List.fold
~f:(fun astate_acc (pvar, t) ->
if is_basic_typ t then
{ astate_acc with
Domain.uninit_vars= D.add (Var.of_pvar pvar) astate_acc.Domain.uninit_vars }
else astate_acc)
~init:astate pvar_list
| Sil.Remove_temps _ | Sil.Abstract _ | Sil.Nullify _ | Sil.Prune _
-> astate
end
module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Normal)
module Analyzer = AbstractInterpreter.Make (CFG) (TransferFunctions)
let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary =
let cfg = CFG.from_pdesc proc_desc in
(* start with empty set of uninit local vars and empty set of init formal params *)
let init =
{ RecordDomain.uninit_vars= UninitVars.empty
; RecordDomain.aliased_vars= AliasedVars.empty
; RecordDomain.prepost= (D.empty, D.empty) }
in
let invariant_map =
Analyzer.exec_cfg cfg (ProcData.make_default proc_desc tenv) ~initial:init ~debug:true
in
let report_uninit_value uninit_vars instr =
let report message loc =
@ -240,9 +161,10 @@ let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary =
| Some node_id -> (
match Analyzer.extract_pre node_id invariant_map with
| Some
{ RecordDomain.uninit_vars= uninitialized_vars
( { RecordDomain.uninit_vars= uninitialized_vars
; RecordDomain.aliased_vars= _
; RecordDomain.prepost= _ }
, _ )
-> report_uninit_value uninitialized_vars instr
| None
-> () )
@ -252,7 +174,8 @@ let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary =
List.iter (CFG.nodes cfg) ~f:report_on_node ;
match Analyzer.extract_post (CFG.id (CFG.exit_node cfg)) invariant_map with
| Some
{RecordDomain.uninit_vars= _; RecordDomain.aliased_vars= _; RecordDomain.prepost= pre, post}
( {RecordDomain.uninit_vars= _; RecordDomain.aliased_vars= _; RecordDomain.prepost= pre, post}
, _ )
-> Summary.update_summary {pre; post} summary
| None
-> if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then (

Write Preview
Loading…
Cancel
Save