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

Factoring out the implementations for letderef and set

Browse Source 
Summary: public First in a series of diffs fixing the __nullable checker for obj-c, which currently reports false positives on property accesses via getters and setters. To fix this problem, we need a special implementation of letderef and set for property accesses that don't report NPE errors. Factoring out the execution of these instructions from the main symbolic executor will make this easier.

Reviewed By: jeremydubreil

Differential Revision: D2763923

fb-gh-sync-id: 883a184
master
Sam Blackshear 9 years ago committed by facebook-github-bot-1
parent 812ac265a8
commit a82588ba8a
1 changed files with 148 additions and 152 deletions
Show Stats Download Patch File Download Diff File

290
infer/src/backend/symExec.ml
Unescape View File

@ -262,57 +262,6 @@ let update_iter iter pi sigma =
let iter' = Prop.prop_iter_update_current_by_list iter sigma in
IList.fold_left (Prop.prop_iter_add_atom false) iter' pi
let execute_letderef pdesc tenv id rhs_exp acc_in iter =
let iter_ren = Prop.prop_iter_make_id_primed id iter in
let prop_ren = Prop.prop_iter_to_prop iter_ren in
match Prop.prop_iter_current iter_ren with
| (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, st)), offlist) ->
let contents, new_ptsto, pred_insts_op, lookup_uninitialized =
ptsto_lookup false pdesc tenv prop_ren (lexp, strexp, typ, st) offlist id in
let update acc (pi, sigma) =
let pi' = Sil.Aeq (Sil.Var(id), contents):: pi in
let sigma' = new_ptsto:: sigma in
let iter' = update_iter iter_ren pi' sigma' in
let prop' = Prop.prop_iter_to_prop iter' in
let prop'' =
if lookup_uninitialized
then
Prop.add_or_replace_exp_attribute prop' (Sil.Var id) (Sil.Adangling Sil.DAuninit)
else prop' in
prop'' :: acc in
begin
match pred_insts_op with
| None -> update acc_in ([],[])
| Some pred_insts -> IList.rev (IList.fold_left update acc_in pred_insts)
end
| (Sil.Hpointsto _, _) ->
Errdesc.warning_err (State.get_loc ()) "no offset access in execute_letderef -- treating as skip@.";
(Prop.prop_iter_to_prop iter_ren) :: acc_in
(* The implementation of this case means that we
ignore this dereferencing operator. When the analyzer treats
numerical information and arrays more precisely later, we
should change the implementation here. *)
| _ -> assert false
let execute_set pdesc tenv rhs_exp acc_in iter =
let (lexp, strexp, typ, st, offlist) =
match Prop.prop_iter_current iter with
| (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, st)), offlist) -> (lexp, strexp, typ, st, offlist)
| _ -> assert false in
let p = Prop.prop_iter_to_prop iter in
let new_ptsto, pred_insts_op =
ptsto_update false pdesc tenv p (lexp, strexp, typ, st) offlist rhs_exp in
let update acc (pi, sigma) =
let sigma' = new_ptsto:: sigma in
let iter' = update_iter iter pi sigma' in
let prop' = Prop.prop_iter_to_prop iter' in
prop' :: acc in
match pred_insts_op with
| None -> update acc_in ([],[])
| Some pred_insts -> IList.fold_left update acc_in pred_insts
(** Module for builtin functions with their symbolic execution handler *)
module Builtin = struct
type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list
@ -831,36 +780,99 @@ let do_error_checks node_opt instr pname pdesc = match node_opt with
| None ->
()
(** Execute [instr] with a symbolic heap [prop].*)
let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
: (Prop.normal Prop.t * Paths.Path.t) list =
let pname = Cfg.Procdesc.get_proc_name pdesc in
State.set_instr _instr; (* mark instruction last seen *)
State.set_prop_tenv_pdesc _prop tenv pdesc; (* mark prop,tenv,pdesc last seen *)
SymOp.pay(); (* pay one symop *)
let ret_old_path pl = (* return the old path unchanged *)
IList.map (fun p -> (p, path)) pl in
let instr = match _instr with
| Sil.Call (ret, exp, par, loc, call_flags) ->
let exp' = Prop.exp_normalize_prop _prop exp in
let instr' = match exp' with
| Sil.Const (Sil.Ctuple (e1 :: el)) -> (* closure: combine arguments to call *)
let e1' = Prop.exp_normalize_prop _prop e1 in
let par' = IList.map (fun e -> (e, Sil.Tvoid)) el in
Sil.Call (ret, e1', par' @ par, loc, call_flags)
| _ ->
Sil.Call (ret, exp', par, loc, call_flags) in
instr'
| _ -> _instr in
match instr with
| Sil.Letderef (id, rhs_exp, typ, loc) ->
let add_to_footprint abducted_pv typ prop =
let abducted_lvar = Sil.Lvar abducted_pv in
let fresh_fp_var = Sil.Var (Ident.create_fresh Ident.kfootprint) in
let lvar_pt_fpvar =
let sizeof_exp = Sil.Sizeof (typ, Sil.Subtype.subtypes) in
Prop.mk_ptsto abducted_lvar (Sil.Eexp (fresh_fp_var, Sil.Inone)) sizeof_exp in
let sigma_fp = Prop.get_sigma_footprint prop in
(Prop.normalize (Prop.replace_sigma_footprint (lvar_pt_fpvar :: sigma_fp) prop), fresh_fp_var)
let add_constraints_on_retval pdesc prop ret_exp typ callee_pname callee_loc =
if Procname.is_infer_undefined callee_pname then prop
else
let is_rec_call pname = (* TODO: (t7147096) extend this to detect mutual recursion *)
Procname.equal pname (Cfg.Procdesc.get_proc_name pdesc) in
let already_has_abducted_retval p abducted_ret_pv =
IList.exists
(fun hpred -> match hpred with
| Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ret_pv
| _ -> false)
(Prop.get_sigma_footprint p) in
(* find an hpred [abducted_pvar] |-> A in [prop] and add [exp] = A to prop *)
let bind_exp_to_abducted_val exp_to_bind abducted_pvar prop =
let bind_exp prop = function
| Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (rhs, _), _)
when Sil.pvar_equal pv abducted_pvar ->
Prop.conjoin_eq exp_to_bind rhs prop
| _ -> prop in
IList.fold_left bind_exp prop (Prop.get_sigma prop) in
(* To avoid obvious false positives, assume skip functions do not return null pointers *)
let add_ret_non_null exp typ prop =
match typ with
| Sil.Tptr _ -> Prop.conjoin_neq exp Sil.exp_zero prop
| _ -> prop in
let add_tainted_post ret_exp callee_pname prop =
Prop.add_or_replace_exp_attribute prop ret_exp (Sil.Ataint callee_pname) in
if !Config.angelic_execution && not (is_rec_call callee_pname) then
(* introduce a fresh program variable to allow abduction on the return value *)
let abducted_ret_pv = Sil.mk_pvar_abducted_ret callee_pname callee_loc in
(* prevent introducing multiple abducted retvals for a single call site in a loop *)
if already_has_abducted_retval prop abducted_ret_pv then prop
else
let prop' =
if !Config.footprint then
let (prop', fresh_fp_var) = add_to_footprint abducted_ret_pv typ prop in
Prop.conjoin_eq ~footprint: true ret_exp fresh_fp_var prop'
else
(* bind return id to the abducted value pointed to by the pvar we introduced *)
bind_exp_to_abducted_val ret_exp abducted_ret_pv prop in
let prop'' = add_ret_non_null ret_exp typ prop' in
if !Config.taint_analysis && Taint.returns_secret callee_pname then
add_tainted_post ret_exp callee_pname prop''
else prop''
else add_ret_non_null ret_exp typ prop
let execute_letderef pname pdesc tenv id rhs_exp typ loc prop_ =
let execute_letderef_ pdesc tenv id rhs_exp loc acc_in iter =
let iter_ren = Prop.prop_iter_make_id_primed id iter in
let prop_ren = Prop.prop_iter_to_prop iter_ren in
match Prop.prop_iter_current iter_ren with
| (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, st)), offlist) ->
let contents, new_ptsto, pred_insts_op, lookup_uninitialized =
ptsto_lookup false pdesc tenv prop_ren (lexp, strexp, typ, st) offlist id in
let update acc (pi, sigma) =
let pi' = Sil.Aeq (Sil.Var(id), contents):: pi in
let sigma' = new_ptsto:: sigma in
let iter' = update_iter iter_ren pi' sigma' in
let prop' = Prop.prop_iter_to_prop iter' in
let prop'' =
if lookup_uninitialized then
Prop.add_or_replace_exp_attribute prop' (Sil.Var id) (Sil.Adangling Sil.DAuninit)
else prop' in
prop'' :: acc in
begin
match pred_insts_op with
| None -> update acc_in ([],[])
| Some pred_insts -> IList.rev (IList.fold_left update acc_in pred_insts)
end
| (Sil.Hpointsto _, _) ->
Errdesc.warning_err loc "no offset access in execute_letderef -- treating as skip@.";
(Prop.prop_iter_to_prop iter_ren) :: acc_in
| _ ->
(* The implementation of this case means that we
ignore this dereferencing operator. When the analyzer treats
numerical information and arrays more precisely later, we
should change the implementation here. *)
assert false in
try
let n_rhs_exp, prop = exp_norm_check_arith pname _prop rhs_exp in
let n_rhs_exp, prop = exp_norm_check_arith pname prop_ rhs_exp in
let n_rhs_exp' = Prop.exp_collapse_consecutive_indices_prop prop typ n_rhs_exp in
match check_constant_string_dereference n_rhs_exp' with
| Some value ->
ret_old_path [Prop.conjoin_eq (Sil.Var id) value prop]
[Prop.conjoin_eq (Sil.Var id) value prop]
| None ->
let exp_get_undef_attr exp =
let fold_undef_pname callee_opt attr =
@ -876,31 +888,70 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
| _ -> prop
else prop in
let iter_list = Rearrange.rearrange pdesc tenv n_rhs_exp' typ prop' loc in
let prop_list =
IList.fold_left (execute_letderef pdesc tenv id n_rhs_exp') [] iter_list in
ret_old_path (IList.rev prop_list)
with
| Rearrange.ARRAY_ACCESS ->
IList.rev (IList.fold_left (execute_letderef_ pdesc tenv id n_rhs_exp' loc) [] iter_list)
with Rearrange.ARRAY_ACCESS ->
if (!Config.array_level = 0) then assert false
else
let undef = Sil.exp_get_undefined false in
ret_old_path [Prop.conjoin_eq (Sil.Var id) undef _prop]
end
| Sil.Set (lhs_exp, typ, rhs_exp, loc) ->
begin
[Prop.conjoin_eq (Sil.Var id) undef prop_]
let execute_set pname pdesc tenv lhs_exp typ rhs_exp loc prop_ =
let execute_set_ pdesc tenv rhs_exp acc_in iter =
let (lexp, strexp, typ, st, offlist) =
match Prop.prop_iter_current iter with
| (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, st)), offlist) ->
(lexp, strexp, typ, st, offlist)
| _ -> assert false in
let p = Prop.prop_iter_to_prop iter in
let new_ptsto, pred_insts_op =
ptsto_update false pdesc tenv p (lexp, strexp, typ, st) offlist rhs_exp in
let update acc (pi, sigma) =
let sigma' = new_ptsto:: sigma in
let iter' = update_iter iter pi sigma' in
let prop' = Prop.prop_iter_to_prop iter' in
prop' :: acc in
match pred_insts_op with
| None -> update acc_in ([],[])
| Some pred_insts -> IList.fold_left update acc_in pred_insts in
try
let n_lhs_exp, _prop' = exp_norm_check_arith pname _prop lhs_exp in
let n_lhs_exp, _prop' = exp_norm_check_arith pname prop_ lhs_exp in
let n_rhs_exp, prop = exp_norm_check_arith pname _prop' rhs_exp in
let prop = Prop.replace_objc_null prop n_lhs_exp n_rhs_exp in
let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop prop typ n_lhs_exp in
let iter_list = Rearrange.rearrange pdesc tenv n_lhs_exp' typ prop loc in
let prop_list = IList.fold_left (execute_set pdesc tenv n_rhs_exp) [] iter_list in
ret_old_path (IList.rev prop_list)
with
| Rearrange.ARRAY_ACCESS ->
IList.rev (IList.fold_left (execute_set_ pdesc tenv n_rhs_exp) [] iter_list)
with Rearrange.ARRAY_ACCESS ->
if (!Config.array_level = 0) then assert false
else ret_old_path [_prop]
end
else [prop_]
(** Execute [instr] with a symbolic heap [prop].*)
let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
: (Prop.normal Prop.t * Paths.Path.t) list =
let pname = Cfg.Procdesc.get_proc_name pdesc in
State.set_instr _instr; (* mark instruction last seen *)
State.set_prop_tenv_pdesc _prop tenv pdesc; (* mark prop,tenv,pdesc last seen *)
SymOp.pay(); (* pay one symop *)
let ret_old_path pl = (* return the old path unchanged *)
IList.map (fun p -> (p, path)) pl in
let instr = match _instr with
| Sil.Call (ret, exp, par, loc, call_flags) ->
let exp' = Prop.exp_normalize_prop _prop exp in
let instr' = match exp' with
| Sil.Const (Sil.Ctuple (e1 :: el)) -> (* closure: combine arguments to call *)
let e1' = Prop.exp_normalize_prop _prop e1 in
let par' = IList.map (fun e -> (e, Sil.Tvoid)) el in
Sil.Call (ret, e1', par' @ par, loc, call_flags)
| _ ->
Sil.Call (ret, exp', par, loc, call_flags) in
instr'
| _ -> _instr in
match instr with
| Sil.Letderef (id, rhs_exp, typ, loc) ->
execute_letderef pname pdesc tenv id rhs_exp typ loc _prop
|> ret_old_path
| Sil.Set (lhs_exp, typ, rhs_exp, loc) ->
execute_set pname pdesc tenv lhs_exp typ rhs_exp loc _prop
|> ret_old_path
| Sil.Prune (cond, loc, true_branch, ik) ->
let check_condition_always_true_false () =
let report_condition_always_true_false i =
@ -1098,61 +1149,6 @@ and sym_exec_generated mask_errors cfg tenv pdesc instrs ppl =
let f plist instr = IList.flatten (IList.map (exe_instr instr) plist) in
IList.fold_left f ppl instrs
and add_to_footprint abducted_pv typ prop =
let abducted_lvar = Sil.Lvar abducted_pv in
let fresh_fp_var = Sil.Var (Ident.create_fresh Ident.kfootprint) in
let lvar_pt_fpvar =
let sizeof_exp = Sil.Sizeof (typ, Sil.Subtype.subtypes) in
Prop.mk_ptsto abducted_lvar (Sil.Eexp (fresh_fp_var, Sil.Inone)) sizeof_exp in
let sigma_fp = Prop.get_sigma_footprint prop in
(Prop.normalize (Prop.replace_sigma_footprint (lvar_pt_fpvar :: sigma_fp) prop), fresh_fp_var)
and add_constraints_on_retval pdesc prop ret_exp typ callee_pname callee_loc =
if Procname.is_infer_undefined callee_pname then prop
else
let is_rec_call pname = (* TODO: (t7147096) extend this to detect mutual recursion *)
Procname.equal pname (Cfg.Procdesc.get_proc_name pdesc) in
let already_has_abducted_retval p abducted_ret_pv =
IList.exists
(fun hpred -> match hpred with
| Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ret_pv
| _ -> false)
(Prop.get_sigma_footprint p) in
(* find an hpred [abducted_pvar] |-> A in [prop] and add [exp] = A to prop *)
let bind_exp_to_abducted_val exp_to_bind abducted_pvar prop =
let bind_exp prop = function
| Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (rhs, _), _)
when Sil.pvar_equal pv abducted_pvar ->
Prop.conjoin_eq exp_to_bind rhs prop
| _ -> prop in
IList.fold_left bind_exp prop (Prop.get_sigma prop) in
(* To avoid obvious false positives, assume skip functions do not return null pointers *)
let add_ret_non_null exp typ prop =
match typ with
| Sil.Tptr _ -> Prop.conjoin_neq exp Sil.exp_zero prop
| _ -> prop in
let add_tainted_post ret_exp callee_pname prop =
Prop.add_or_replace_exp_attribute prop ret_exp (Sil.Ataint callee_pname) in
if !Config.angelic_execution && not (is_rec_call callee_pname) then
(* introduce a fresh program variable to allow abduction on the return value *)
let abducted_ret_pv = Sil.mk_pvar_abducted_ret callee_pname callee_loc in
(* prevent introducing multiple abducted retvals for a single call site in a loop *)
if already_has_abducted_retval prop abducted_ret_pv then prop
else
let prop' =
if !Config.footprint then
let (prop', fresh_fp_var) = add_to_footprint abducted_ret_pv typ prop in
Prop.conjoin_eq ~footprint: true ret_exp fresh_fp_var prop'
else
(* bind return id to the abducted value pointed to by the pvar we introduced *)
bind_exp_to_abducted_val ret_exp abducted_ret_pv prop in
let prop'' = add_ret_non_null ret_exp typ prop' in
if !Config.taint_analysis && Taint.returns_secret callee_pname then
add_tainted_post ret_exp callee_pname prop''
else prop''
else add_ret_non_null ret_exp typ prop
and add_constraints_on_actuals_by_ref prop actuals_by_ref callee_pname callee_loc =
(* replace an hpred of the form actual_var |-> _ with new_hpred in prop *)
let replace_actual_hpred actual_var new_hpred prop =

Write Preview
Loading…
Cancel
Save