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

more of the less SummaryReporting

Browse Source 
Summary: argh

Reviewed By: dulmarod

Differential Revision: D21261639

fbshipit-source-id: b6a969c75
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent d5c8a38fc3
commit 8dabbd5eda
4 changed files with 135 additions and 102 deletions
Show Stats Download Patch File Download Diff File

10
infer/src/biabduction/BuiltinDefn.ml
Unescape View File

@ -471,7 +471,8 @@ let execute_free_ tenv mk ?(mark_as_freed = true) loc acc iter =
(* should not happen *)
let execute_free_nonzero_ mk ?(mark_as_freed = true) pdesc tenv instr prop lexp typ loc =
let execute_free_nonzero_ mk ?(mark_as_freed = true)
({InterproceduralAnalysis.tenv; _} as analysis_data) instr prop lexp typ loc =
try
match Prover.is_root tenv prop lexp lexp with
| None ->
@ -482,7 +483,7 @@ let execute_free_nonzero_ mk ?(mark_as_freed = true) pdesc tenv instr prop lexp
List.fold
~f:(execute_free_ tenv mk ~mark_as_freed loc)
~init:[]
(Rearrange.rearrange pdesc tenv lexp typ prop loc)
(Rearrange.rearrange analysis_data lexp typ prop loc)
in
List.rev prop_list
with Rearrange.ARRAY_ACCESS ->
@ -499,7 +500,8 @@ let execute_free_nonzero_ mk ?(mark_as_freed = true) pdesc tenv instr prop lexp
let execute_free mk ?(mark_as_freed = true)
{Builtin.analysis_data= {proc_desc; tenv}; instr; prop_; path; args; loc} : Builtin.ret_typ =
{Builtin.analysis_data= {proc_desc; tenv} as analysis_data; instr; prop_; path; args; loc} :
Builtin.ret_typ =
match args with
| [(lexp, typ)] ->
let pname = Procdesc.get_proc_name proc_desc in
@ -517,7 +519,7 @@ let execute_free mk ?(mark_as_freed = true)
@ (* model: if 0 then skip else execute_free_nonzero_ *)
List.concat_map
~f:(fun p ->
execute_free_nonzero_ mk ~mark_as_freed proc_desc tenv instr p
execute_free_nonzero_ mk ~mark_as_freed analysis_data instr p
(Prop.exp_normalize_prop tenv p lexp)
typ loc )
prop_nonzero

150
infer/src/biabduction/Rearrange.ml
Unescape View File

@ -25,7 +25,7 @@ let rec list_rev_and_concat l1 l2 =
(** Check whether the index is out of bounds. If the length is - 1, no check is performed. If the
index is provably out of bound, a bound error is given. If the length is a constant and the
index is not provably in bound, a warning is given. *)
let check_bad_index tenv pname p len index loc =
let check_bad_index {InterproceduralAnalysis.proc_desc; err_log; tenv} pname p len index loc =
let len_is_constant = match len with Exp.Const _ -> true | _ -> false in
let index_provably_out_of_bound () =
let index_too_large = Prop.mk_inequality tenv (Exp.BinOp (Binop.Le, len, index)) in
@ -55,7 +55,9 @@ let check_bad_index tenv pname p len index loc =
Exceptions.Array_out_of_bounds_l1
(Errdesc.explain_array_access pname tenv deref_str p loc, __POS__)
in
SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
let proc_attrs = Procdesc.get_attributes proc_desc in
BiabductionReporting.log_issue_deprecated_using_state proc_attrs err_log Exceptions.Warning
exn
else if len_is_constant then
let deref_str = Localise.deref_str_array_bound len_const_opt index_const_opt in
let desc = Errdesc.explain_array_access pname tenv deref_str p loc in
@ -63,18 +65,21 @@ let check_bad_index tenv pname p len index loc =
if index_has_bounds () then Exceptions.Array_out_of_bounds_l2 (desc, __POS__)
else Exceptions.Array_out_of_bounds_l3 (desc, __POS__)
in
SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
let proc_attrs = Procdesc.get_attributes proc_desc in
BiabductionReporting.log_issue_deprecated_using_state proc_attrs err_log Exceptions.Warning
exn
(** Perform bounds checking *)
let bounds_check tenv pname prop len e =
let bounds_check analysis_data pname prop len e =
if Config.trace_rearrange then (
L.d_str "Bounds check index:" ; Exp.d_exp e ; L.d_str " len: " ; Exp.d_exp len ; L.d_ln () ) ;
check_bad_index tenv pname prop len e
check_bad_index analysis_data pname prop len e
let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp (t : Typ.t)
(off : Predicates.offset list) inst : Predicates.atom list * Predicates.strexp * Typ.t =
let rec create_struct_values analysis_data pname tenv orig_prop footprint_part kind max_stamp
(t : Typ.t) (off : Predicates.offset list) inst :
Predicates.atom list * Predicates.strexp * Typ.t =
if Config.trace_rearrange then (
L.d_increase_indent () ;
L.d_strln "entering create_struct_values" ;
@ -104,7 +109,8 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
match List.find ~f:(fun (f', _, _) -> Fieldname.equal f f') (fields @ statics) with
| Some (_, t', _) ->
let atoms', se', res_t' =
create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst
create_struct_values analysis_data pname tenv orig_prop footprint_part kind max_stamp
t' off' inst
in
let se = Predicates.Estruct ([(f, se')], inst) in
let replace_typ_of_f (f', t', a') =
@ -121,7 +127,8 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
fail t off __POS__ )
| Tstruct _, Off_index e :: off' ->
let atoms', se', res_t' =
create_struct_values pname tenv orig_prop footprint_part kind max_stamp t off' inst
create_struct_values analysis_data pname tenv orig_prop footprint_part kind max_stamp t
off' inst
in
let e' = Absarray.array_clean_new_index footprint_part e in
let len = Exp.Var (new_id ()) in
@ -136,9 +143,10 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
| [] ->
([], Predicates.Earray (len, [], inst), t)
| Predicates.Off_index e :: off' ->
bounds_check tenv pname orig_prop len e (AnalysisState.get_loc_exn ()) ;
bounds_check analysis_data pname orig_prop len e (AnalysisState.get_loc_exn ()) ;
let atoms', se', res_t' =
create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst
create_struct_values analysis_data pname tenv orig_prop footprint_part kind max_stamp
t' off' inst
in
let e' = Absarray.array_clean_new_index footprint_part e in
let se = Predicates.Earray (len, [(e', se')], inst) in
@ -160,7 +168,8 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
in
let len = Exp.Var (new_id ()) in
let atoms', se', res_t' =
create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst
create_struct_values analysis_data pname tenv orig_prop footprint_part kind max_stamp t'
off' inst
in
let e' = Absarray.array_clean_new_index footprint_part e in
let se = Predicates.Earray (len, [(e', se')], inst) in
@ -183,18 +192,20 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
flds and do the case - analysis for array accesses. This does not catch the array - bounds
errors. If we want to implement the checks for array bounds errors, we need to change this
function. *)
let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se (typ : Typ.t)
(off : Predicates.offset list) inst =
let rec strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part kind max_stamp se
(typ : Typ.t) (off : Predicates.offset list) inst =
let new_id () = incr max_stamp ; Ident.create kind !max_stamp in
match (off, se, typ.desc) with
| [], Predicates.Eexp _, _ | [], Predicates.Estruct _, _ ->
[([], se, typ)]
| [], Predicates.Earray _, _ ->
let off_new = Predicates.Off_index Exp.zero :: off in
strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part kind max_stamp se typ
off_new inst
| Off_fld _ :: _, Predicates.Earray _, Tarray _ ->
let off_new = Predicates.Off_index Exp.zero :: off in
strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part kind max_stamp se typ
off_new inst
| Off_fld (f, _) :: off', Predicates.Estruct (fsel, inst'), Tstruct name -> (
match Tenv.lookup tenv name with
| Some ({fields; statics} as struct_typ) -> (
@ -203,8 +214,8 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp
match List.find ~f:(fun (f', _) -> Fieldname.equal f f') fsel with
| Some (_, se') ->
let atoms_se_typ_list' =
strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se' typ' off'
inst
strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part kind max_stamp
se' typ' off' inst
in
let replace acc (res_atoms', res_se', res_typ') =
let replace_fse ((f1, _) as ft1) =
@ -226,7 +237,8 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp
List.fold ~f:replace ~init:[] atoms_se_typ_list'
| None ->
let atoms', se', res_typ' =
create_struct_values pname tenv orig_prop footprint_part kind max_stamp typ' off' inst
create_struct_values analysis_data pname tenv orig_prop footprint_part kind max_stamp
typ' off' inst
in
let res_fsel' =
List.sort ~compare:[%compare: Fieldname.t * Predicates.strexp] ((f, se') :: fsel)
@ -258,17 +270,17 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp
in
let se_new = Predicates.Earray (len, [(Exp.zero, se)], inst) in
let typ_new = Typ.mk_array typ in
strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off
inst
strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part kind max_stamp se_new
typ_new off inst
| ( Off_index e :: off'
, Predicates.Earray (len, esel, inst_arr)
, Tarray {elt= typ'; length= len_for_typ'; stride} ) -> (
bounds_check tenv pname orig_prop len e (AnalysisState.get_loc_exn ()) ;
bounds_check analysis_data pname orig_prop len e (AnalysisState.get_loc_exn ()) ;
match List.find ~f:(fun (e', _) -> Exp.equal e e') esel with
| Some (_, se') ->
let atoms_se_typ_list' =
strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se' typ' off'
inst
strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part kind max_stamp
se' typ' off' inst
in
let replace acc (res_atoms', res_se', res_typ') =
let replace_ise ise = if Exp.equal e (fst ise) then (e, res_se') else ise in
@ -282,14 +294,14 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp
in
List.fold ~f:replace ~init:[] atoms_se_typ_list'
| None ->
array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp len esel
len_for_typ' typ' typ e off' inst_arr inst )
array_case_analysis_index analysis_data pname tenv orig_prop footprint_part kind max_stamp
len esel len_for_typ' typ' typ e off' inst_arr inst )
| _, _, _ ->
raise (Exceptions.Bad_footprint __POS__)
and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp array_len
array_cont typ_array_len typ_cont typ_array index off inst_arr inst =
and array_case_analysis_index analysis_data pname tenv orig_prop footprint_part kind max_stamp
array_len array_cont typ_array_len typ_cont typ_array index off inst_arr inst =
let check_sound t' =
if not (Typ.equal typ_cont t' || List.is_empty array_cont) then
raise (Exceptions.Bad_footprint __POS__)
@ -310,7 +322,8 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
[([], array_default, typ_default)]
else if !BiabductionConfig.footprint then (
let atoms, elem_se, elem_typ =
create_struct_values pname tenv orig_prop footprint_part kind max_stamp typ_cont off inst
create_struct_values analysis_data pname tenv orig_prop footprint_part kind max_stamp typ_cont
off inst
in
check_sound elem_typ ;
let cont_new =
@ -324,7 +337,8 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
if array_is_full then []
else
let atoms, elem_se, elem_typ =
create_struct_values pname tenv orig_prop footprint_part kind max_stamp typ_cont off inst
create_struct_values analysis_data pname tenv orig_prop footprint_part kind max_stamp
typ_cont off inst
in
check_sound elem_typ ;
let cont_new =
@ -339,8 +353,8 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
List.concat (List.rev (res_new :: acc))
| ((i, se) as ise) :: isel_unseen ->
let atoms_se_typ_list =
strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se typ_cont off
inst
strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part kind max_stamp
se typ_cont off inst
in
let atoms_se_typ_list' =
List.fold
@ -386,7 +400,7 @@ let laundry_offset_for_footprint max_stamp offs_in =
laundry [] [] offs_in
let strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se te
let strexp_extend_values analysis_data pname tenv orig_prop footprint_part kind max_stamp se te
(off : Predicates.offset list) inst =
let typ = Exp.texp_to_typ None te in
let off', laundry_atoms =
@ -404,7 +418,8 @@ let strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se t
Predicates.d_offset_list off' ;
L.d_strln (if footprint_part then " FP" else " RE") ) ;
let atoms_se_typ_list =
strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se typ off' inst
strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part kind max_stamp se typ
off' inst
in
let atoms_se_typ_list_filtered =
let check_neg_atom atom = Prover.check_atom tenv Prop.prop_emp (Prover.atom_negate tenv atom) in
@ -432,7 +447,7 @@ let collect_root_offset exp =
(** Exp.Construct a points-to predicate for an expression, to add to a footprint. *)
let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst :
let mk_ptsto_exp_footprint analysis_data pname tenv orig_prop (lexp, typ) max_stamp inst :
Predicates.hpred * Predicates.hpred * Predicates.atom list =
let root, off = collect_root_offset lexp in
if not (exp_has_only_footprint_ids root) then
@ -462,16 +477,16 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst :
(Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype}) )
| _, [], Typ.Tfun ->
let atoms, se, typ =
create_struct_values pname tenv orig_prop footprint_part Ident.kfootprint max_stamp typ
off0 inst
create_struct_values analysis_data pname tenv orig_prop footprint_part Ident.kfootprint
max_stamp typ off0 inst
in
( atoms
, Prop.mk_ptsto tenv root se (Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype})
)
| _ ->
let atoms, se, typ =
create_struct_values pname tenv orig_prop footprint_part Ident.kfootprint max_stamp typ
off0 inst
create_struct_values analysis_data pname tenv orig_prop footprint_part Ident.kfootprint
max_stamp typ off0 inst
in
( atoms
, Prop.mk_ptsto tenv root se (Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype})
@ -517,7 +532,7 @@ let prop_iter_check_fields_ptsto_shallow tenv iter lexp =
(** [prop_iter_extend_ptsto iter lexp] extends the current psto predicate in [iter] with enough
fields to follow the path in [lexp] -- field splitting model. It also materializes all indices
accessed in lexp. *)
let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
let prop_iter_extend_ptsto analysis_data pname tenv orig_prop iter lexp inst =
if Config.trace_rearrange then (
L.d_str "entering prop_iter_extend_ptsto lexp: " ;
Exp.d_exp lexp ;
@ -527,8 +542,8 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
let extend_footprint_pred = function
| Predicates.Hpointsto (e, se, te) ->
let atoms_se_te_list =
strexp_extend_values pname tenv orig_prop true Ident.kfootprint (ref max_stamp) se te
offset inst
strexp_extend_values analysis_data pname tenv orig_prop true Ident.kfootprint
(ref max_stamp) se te offset inst
in
List.map
~f:(fun (atoms', se', te') -> (atoms', Predicates.Hpointsto (e, se', te')))
@ -537,8 +552,8 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
match hpara.Predicates.body with
| Predicates.Hpointsto (e', se', te') :: body_rest ->
let atoms_se_te_list =
strexp_extend_values pname tenv orig_prop true Ident.kfootprint (ref max_stamp) se' te'
offset inst
strexp_extend_values analysis_data pname tenv orig_prop true Ident.kfootprint
(ref max_stamp) se' te' offset inst
in
let atoms_body_list =
List.map
@ -588,8 +603,8 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
in
let iter_list =
let atoms_se_te_list =
strexp_extend_values pname tenv orig_prop false extend_kind (ref max_stamp) se te offset
inst
strexp_extend_values analysis_data pname tenv orig_prop false extend_kind (ref max_stamp) se
te offset inst
in
List.map ~f:(atoms_se_te_to_iter e) atoms_se_te_list
in
@ -666,10 +681,10 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
with the allowed footprint variables. Then, change it into a iterator. This function ensures
that [root(lexp): typ] is the current hpred of the iterator. typ is the type of the root of
lexp. *)
let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst =
let prop_iter_add_hpred_footprint_to_prop analysis_data pname tenv prop (lexp, typ) inst =
let max_stamp = Prop.max_stamp ~f:Ident.is_footprint prop in
let ptsto, ptsto_foot, atoms =
mk_ptsto_exp_footprint pname tenv prop (lexp, typ) (ref max_stamp) inst
mk_ptsto_exp_footprint analysis_data pname tenv prop (lexp, typ) (ref max_stamp) inst
in
L.d_strln "++++ Adding footprint frame" ;
Prop.d_prop (Prop.prop_hpred_star Prop.prop_emp ptsto) ;
@ -697,7 +712,7 @@ let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst =
(** Add a pointsto for [root(lexp): typ] to the iterator and to the footprint, if it's compatible
with the allowed footprint variables. This function ensures that [root(lexp): typ] is the
current hpred of the iterator. typ is the type of the root of lexp. *)
let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst =
let prop_iter_add_hpred_footprint analysis_data pname tenv orig_prop iter (lexp, typ) inst =
if Config.trace_rearrange then (
L.d_strln "entering prop_iter_add_hpred_footprint" ;
L.d_str "lexp: " ;
@ -708,7 +723,7 @@ let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst =
L.d_ln () ) ;
let max_stamp = Prop.prop_iter_max_stamp ~f:Ident.is_footprint iter in
let ptsto, ptsto_foot, atoms =
mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) (ref max_stamp) inst
mk_ptsto_exp_footprint analysis_data pname tenv orig_prop (lexp, typ) (ref max_stamp) inst
in
L.d_strln "++++ Adding footprint frame" ;
Prop.d_prop (Prop.prop_hpred_star Prop.prop_emp ptsto) ;
@ -757,7 +772,7 @@ let pp_rearrangement_error message prop lexp =
(** do re-arrangement for an iter whose current element is a pointsto *)
let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
let iter_rearrange_ptsto analysis_data pname tenv orig_prop iter lexp inst =
if Config.trace_rearrange then (
L.d_increase_indent () ;
L.d_strln "entering iter_rearrange_ptsto" ;
@ -780,15 +795,16 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
raise (Exceptions.Missing_fld (fld, __POS__))
in
let res =
if !BiabductionConfig.footprint then prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst
if !BiabductionConfig.footprint then
prop_iter_extend_ptsto analysis_data pname tenv orig_prop iter lexp inst
else (
check_field_splitting () ;
match Prop.prop_iter_current tenv iter with
| Predicates.Hpointsto (e, se, te), offset ->
let max_stamp = Prop.prop_iter_max_stamp iter in
let atoms_se_te_list =
strexp_extend_values pname tenv orig_prop false Ident.kprimed (ref max_stamp) se te
offset inst
strexp_extend_values analysis_data pname tenv orig_prop false Ident.kprimed
(ref max_stamp) se te offset inst
in
let handle_case (atoms', se', te') =
let iter' =
@ -968,7 +984,8 @@ let type_at_offset tenv texp off =
(** Check that the size of a type coming from an instruction does not exceed the size of the type
from the pointsto predicate For example, that a pointer to int is not used to assign to a char *)
let check_type_size tenv pname prop texp off typ_from_instr =
let check_type_size {InterproceduralAnalysis.proc_desc; err_log; tenv} pname prop texp off
typ_from_instr =
L.d_strln ~color:Orange "check_type_size" ;
L.d_str "off: " ;
Predicates.d_offset_list off ;
@ -991,7 +1008,8 @@ let check_type_size tenv pname prop texp off typ_from_instr =
Exceptions.Pointer_size_mismatch
(Errdesc.explain_dereference pname tenv deref_str prop loc, __POS__)
in
SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
let attrs = Procdesc.get_attributes proc_desc in
BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Warning exn
| None ->
L.d_str "texp: " ; Exp.d_texp_full texp ; L.d_ln ()
@ -1003,7 +1021,7 @@ let check_type_size tenv pname prop texp off typ_from_instr =
prove the inconsistency of prop, * only after unrolling some predicates in prop. This function
ensures * that the theorem prover cannot prove the inconsistency of any of the * new iters in
the result. *)
let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst :
let rec iter_rearrange analysis_data pname tenv lexp typ_from_instr prop iter inst :
Predicates.offset list Prop.prop_iter list =
let rec root_typ_of_offsets = function
| Predicates.Off_fld (f, fld_typ) :: _ -> (
@ -1049,7 +1067,7 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst :
let default_case_iter (iter' : unit Prop.prop_iter) =
if Config.trace_rearrange then L.d_strln "entering default_case_iter" ;
if !BiabductionConfig.footprint then
prop_iter_add_hpred_footprint pname tenv prop iter' (lexp, typ) inst
prop_iter_add_hpred_footprint analysis_data pname tenv prop iter' (lexp, typ) inst
else if Config.array_level >= 1 && (not !BiabductionConfig.footprint) && Exp.pointer_arith lexp
then rearrange_arith tenv lexp prop
else (
@ -1060,7 +1078,10 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst :
let f_one_iter iter' =
let prop' = Prop.prop_iter_to_prop tenv iter' in
if Prover.check_inconsistency tenv prop' then []
else iter_rearrange pname tenv (Prop.lexp_normalize_prop tenv prop' lexp) typ prop' iter' inst
else
iter_rearrange analysis_data pname tenv
(Prop.lexp_normalize_prop tenv prop' lexp)
typ prop' iter' inst
in
let rec f_many_iters iters_lst = function
| [] ->
@ -1089,8 +1110,8 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst :
| Some iter -> (
match Prop.prop_iter_current tenv iter with
| Predicates.Hpointsto (_, _, texp), off ->
if Config.type_size then check_type_size tenv pname prop texp off typ_from_instr ;
iter_rearrange_ptsto pname tenv prop iter lexp inst
if Config.type_size then check_type_size analysis_data pname prop texp off typ_from_instr ;
iter_rearrange_ptsto analysis_data pname tenv prop iter lexp inst
| Predicates.Hlseg (Lseg_NE, para, e1, e2, elist), _ ->
iter_rearrange_ne_lseg tenv recurse_on_iters iter para e1 e2 elist
| Predicates.Hlseg (Lseg_PE, para, e1, e2, elist), _ ->
@ -1365,7 +1386,8 @@ let check_call_to_objc_block_error tenv pdesc prop fun_exp loc =
(** [rearrange lexp prop] rearranges [prop] into the form [prop' * lexp|->strexp:typ]. It returns an
iterator with [lexp |-> strexp: typ] as current predicate and the path (an [offsetlist]) which
leads to [lexp] as the iterator state. *)
let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc :
let rearrange ?(report_deref_errors = true)
({InterproceduralAnalysis.proc_desc= pdesc; tenv} as analysis_data) lexp typ prop loc :
Predicates.offset list Prop.prop_iter list =
let nlexp =
match Prop.exp_normalize_prop tenv prop lexp with
@ -1391,9 +1413,9 @@ let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc :
match Prop.prop_iter_create prop with
| None ->
if !BiabductionConfig.footprint then
[prop_iter_add_hpred_footprint_to_prop pname tenv prop (nlexp, typ) inst]
[prop_iter_add_hpred_footprint_to_prop analysis_data pname tenv prop (nlexp, typ) inst]
else (
pp_rearrangement_error "sigma is empty" prop nlexp ;
raise (Exceptions.Symexec_memory_error __POS__) )
| Some iter ->
iter_rearrange pname tenv nlexp typ prop iter inst
iter_rearrange analysis_data pname tenv nlexp typ prop iter inst

3
infer/src/biabduction/Rearrange.mli
Unescape View File

@ -26,8 +26,7 @@ val check_call_to_objc_block_error :
val rearrange :
?report_deref_errors:bool
-> Procdesc.t
-> Tenv.t
-> BiabductionSummary.t InterproceduralAnalysis.t
-> Exp.t
-> Typ.t
-> Prop.normal Prop.t

74
infer/src/biabduction/SymExec.ml
Unescape View File

@ -55,7 +55,7 @@ let unroll_type tenv (typ : Typ.t) (off : Predicates.offset) =
should run strexp_extend_value in rearrange.ml for the same strexp and offlist, so that all the
necessary extensions of strexp are done before this function. If the tool follows this protocol,
it will never hit the assert false cases for field and array accesses. *)
let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist
let rec apply_offlist analysis_data tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist
(f : Exp.t option -> Exp.t) inst lookup_inst =
let pp_error () =
L.d_strln ".... Invalid Field ...." ;
@ -96,12 +96,12 @@ let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, ty
(f None, Prop.create_strexp_of_type tenv Prop.Fld_init typ None inst, typ, None) )
| [], Predicates.Earray _, _ ->
let offlist' = Predicates.Off_index Exp.zero :: offlist in
apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist' f inst
lookup_inst
apply_offlist analysis_data tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist' f
inst lookup_inst
| Predicates.Off_fld _ :: _, Predicates.Earray _, _ ->
let offlist_new = Predicates.Off_index Exp.zero :: offlist in
apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist_new f inst
lookup_inst
apply_offlist analysis_data tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist_new
f inst lookup_inst
| ( Predicates.Off_fld (fld, fld_typ) :: offlist'
, Predicates.Estruct (fsel, inst')
, Typ.Tstruct name ) -> (
@ -111,8 +111,8 @@ let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, ty
match List.find ~f:(fun fse -> Fieldname.equal fld (fst fse)) fsel with
| Some (_, se') ->
let res_e', res_se', res_t', res_pred_insts_op' =
apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, se', t') offlist' f inst
lookup_inst
apply_offlist analysis_data tenv p fp_root nullify_struct (root_lexp, se', t')
offlist' f inst lookup_inst
in
let replace_fse fse = if Fieldname.equal fld (fst fse) then (fld, res_se') else fse in
let res_se = Predicates.Estruct (List.map ~f:replace_fse fsel, inst') in
@ -140,8 +140,8 @@ let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, ty
match List.find ~f:(fun ese -> Prover.check_equal tenv p nidx (fst ese)) esel with
| Some (idx_ese', se') ->
let res_e', res_se', res_t', res_pred_insts_op' =
apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, se', t') offlist' f inst
lookup_inst
apply_offlist analysis_data tenv p fp_root nullify_struct (root_lexp, se', t') offlist'
f inst lookup_inst
in
let replace_ese ese = if Exp.equal idx_ese' (fst ese) then (idx_ese', res_se') else ese in
let res_se = Predicates.Earray (len, List.map ~f:replace_ese esel, inst1) in
@ -171,12 +171,12 @@ let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, ty
prover with [p]. Finally, before running this function, the tool should run strexp_extend_value
in rearrange.ml for the same se and offlist, so that all the necessary extensions of se are done
before this function. *)
let ptsto_lookup pdesc tenv p (lexp, se, sizeof) offlist id =
let ptsto_lookup analysis_data tenv p (lexp, se, sizeof) offlist id =
let f = function Some exp -> exp | None -> Exp.Var id in
let fp_root = match lexp with Exp.Var id -> Ident.is_footprint id | _ -> false in
let lookup_inst = ref None in
let e', se', typ', pred_insts_op' =
apply_offlist pdesc tenv p fp_root false (lexp, se, sizeof.Exp.typ) offlist f
apply_offlist analysis_data tenv p fp_root false (lexp, se, sizeof.Exp.typ) offlist f
Predicates.inst_lookup lookup_inst
in
let lookup_uninitialized =
@ -198,13 +198,13 @@ let ptsto_lookup pdesc tenv p (lexp, se, sizeof) offlist id =
proposition [p], so it is ok call prover with [p]. Finally, before running this function, the
tool should run strexp_extend_value in rearrange.ml for the same se and offlist, so that all the
necessary extensions of se are done before this function. *)
let ptsto_update pdesc tenv p (lexp, se, sizeof) offlist exp =
let ptsto_update analysis_data tenv p (lexp, se, sizeof) offlist exp =
let f _ = exp in
let fp_root = match lexp with Exp.Var id -> Ident.is_footprint id | _ -> false in
let lookup_inst = ref None in
let _, se', typ', pred_insts_op' =
let pos = State.get_path_pos () in
apply_offlist pdesc tenv p fp_root true (lexp, se, sizeof.Exp.typ) offlist f
apply_offlist analysis_data tenv p fp_root true (lexp, se, sizeof.Exp.typ) offlist f
(State.get_inst_update pos) lookup_inst
in
let ptsto' = Prop.mk_ptsto tenv lexp se' (Exp.Sizeof {sizeof with typ= typ'}) in
@ -957,7 +957,9 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nonnull_annot typ cal
else add_ret_non_null ret_exp typ prop
let execute_load ?(report_deref_errors = true) pname pdesc tenv id rhs_exp typ loc prop_ =
let execute_load ?(report_deref_errors = true) pname
({InterproceduralAnalysis.proc_desc= pdesc; tenv; _} as analysis_data) id rhs_exp typ loc prop_
=
let execute_load_ acc_in iter =
let iter_ren = Prop.prop_iter_make_id_primed tenv id iter in
let prop_ren = Prop.prop_iter_to_prop tenv iter_ren in
@ -1010,7 +1012,7 @@ let execute_load ?(report_deref_errors = true) pname pdesc tenv id rhs_exp typ l
| None -> (
try
let iter_list =
Rearrange.rearrange ~report_deref_errors pdesc tenv n_rhs_exp' typ prop loc
Rearrange.rearrange ~report_deref_errors analysis_data n_rhs_exp' typ prop loc
in
List.rev (List.fold ~f:execute_load_ ~init:[] iter_list)
with Exceptions.Symexec_memory_error _ ->
@ -1033,8 +1035,9 @@ let load_ret_annots pname =
Annot.Item.empty
let execute_store ?(report_deref_errors = true) pname pdesc tenv lhs_exp typ rhs_exp loc prop_ =
let execute_store_ pdesc tenv rhs_exp acc_in iter =
let execute_store ?(report_deref_errors = true) pname
({InterproceduralAnalysis.tenv; _} as analysis_data) lhs_exp typ rhs_exp loc prop_ =
let execute_store_ analysis_data tenv rhs_exp acc_in iter =
let lexp, strexp, sizeof, offlist =
match Prop.prop_iter_current tenv iter with
| Predicates.Hpointsto (lexp, strexp, Exp.Sizeof sizeof), offlist ->
@ -1044,7 +1047,7 @@ let execute_store ?(report_deref_errors = true) pname pdesc tenv lhs_exp typ rhs
in
let p = Prop.prop_iter_to_prop tenv iter in
let new_ptsto, pred_insts_op =
ptsto_update pdesc tenv p (lexp, strexp, sizeof) offlist rhs_exp
ptsto_update analysis_data tenv p (lexp, strexp, sizeof) offlist rhs_exp
in
let update acc (pi, sigma) =
let sigma' = new_ptsto :: sigma in
@ -1063,9 +1066,11 @@ let execute_store ?(report_deref_errors = true) pname pdesc tenv lhs_exp typ rhs
let n_rhs_exp, prop = check_arith_norm_exp tenv pname rhs_exp prop_' in
let prop = Attribute.replace_objc_null tenv prop n_lhs_exp n_rhs_exp in
let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_lhs_exp in
let iter_list = Rearrange.rearrange ~report_deref_errors pdesc tenv n_lhs_exp' typ prop loc in
let iter_list =
Rearrange.rearrange ~report_deref_errors analysis_data n_lhs_exp' typ prop loc
in
let prop_list =
List.rev (List.fold ~f:(execute_store_ pdesc tenv n_rhs_exp) ~init:[] iter_list)
List.rev (List.fold ~f:(execute_store_ analysis_data tenv n_rhs_exp) ~init:[] iter_list)
in
prop_list
with Rearrange.ARRAY_ACCESS -> if Int.equal Config.array_level 0 then assert false else [prop_]
@ -1222,9 +1227,9 @@ let rec sym_exec
in
match instr with
| Sil.Load {id; e= rhs_exp; root_typ= typ; loc} ->
execute_load current_pname current_pdesc tenv id rhs_exp typ loc prop_ |> ret_old_path
execute_load current_pname analysis_data id rhs_exp typ loc prop_ |> ret_old_path
| Sil.Store {e1= lhs_exp; root_typ= typ; e2= rhs_exp; loc} ->
execute_store current_pname current_pdesc tenv lhs_exp typ rhs_exp loc prop_ |> ret_old_path
execute_store current_pname analysis_data lhs_exp typ rhs_exp loc prop_ |> ret_old_path
| Sil.Prune (cond, loc, true_branch, ik) ->
let prop__ = Attribute.nullify_exp_with_objc_null tenv prop_ cond in
let check_condition_always_true_false () =
@ -1385,8 +1390,8 @@ let rec sym_exec
(* If it's an ObjC getter or setter, call the builtin rather than skipping *)
handle_objc_instance_method_call n_actual_params prop tenv
(fst ret_id_typ) current_pdesc resolved_pname path (fun () ->
sym_exec_objc_accessor resolved_pname objc_accessor ret_type tenv
(fst ret_id_typ) current_pdesc callee_pname loc n_actual_params
sym_exec_objc_accessor resolved_pname objc_accessor ret_type
(fst ret_id_typ) analysis_data callee_pname loc n_actual_params
prop path )
| None when model_as_malloc ret_type resolved_pname ->
(* If it's an alloc model, call alloc rather than skipping *)
@ -1723,7 +1728,8 @@ and check_variadic_sentinel_if_present ({Builtin.prop_; path; proc_name} as buil
[(prop_, path)]
and sym_exec_objc_getter field ret_typ tenv ret_id pdesc pname loc args prop =
and sym_exec_objc_getter field ret_typ ret_id ({InterproceduralAnalysis.tenv; _} as analysis_data)
pname loc args prop =
let field_name, _, _ = field in
L.d_printfln "No custom getter found. Executing the ObjC builtin getter with ivar %a."
Fieldname.pp field_name ;
@ -1733,13 +1739,14 @@ and sym_exec_objc_getter field ret_typ tenv ret_id pdesc pname loc args prop =
| {desc= Tptr (({desc= Tstruct struct_name} as typ), _)} ) ) ] ->
Tenv.add_field tenv struct_name field ;
let field_access_exp = Exp.Lfield (lexp, field_name, typ) in
execute_load ~report_deref_errors:false pname pdesc tenv ret_id field_access_exp ret_typ loc
prop
execute_load ~report_deref_errors:false pname analysis_data ret_id field_access_exp ret_typ
loc prop
| _ ->
raise (Exceptions.Wrong_argument_number __POS__)
and sym_exec_objc_setter field _ tenv _ pdesc pname loc args prop =
and sym_exec_objc_setter field _ _ ({InterproceduralAnalysis.tenv; _} as analysis_data) pname loc
args prop =
let field_name, _, _ = field in
L.d_printfln "No custom setter found. Executing the ObjC builtin setter with ivar %a."
Fieldname.pp field_name ;
@ -1750,13 +1757,15 @@ and sym_exec_objc_setter field _ tenv _ pdesc pname loc args prop =
:: (lexp2, typ2) :: _ ->
Tenv.add_field tenv struct_name field ;
let field_access_exp = Exp.Lfield (lexp1, field_name, typ1) in
execute_store ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop
execute_store ~report_deref_errors:false pname analysis_data field_access_exp typ2 lexp2 loc
prop
| _ ->
raise (Exceptions.Wrong_argument_number __POS__)
and sym_exec_objc_accessor callee_pname property_accesor ret_typ tenv ret_id pdesc _ loc args prop
path : Builtin.ret_typ =
and sym_exec_objc_accessor callee_pname property_accesor ret_typ ret_id
({InterproceduralAnalysis.proc_desc= pdesc} as analysis_data) _ loc args prop path :
Builtin.ret_typ =
let f_accessor =
match property_accesor with
| ProcAttributes.Objc_getter field ->
@ -1773,7 +1782,8 @@ and sym_exec_objc_accessor callee_pname property_accesor ret_typ tenv ret_id pde
(Procname.to_simplified_string callee_pname)
in
let path = Paths.Path.add_description path path_description in
f_accessor ret_typ tenv ret_id pdesc cur_pname loc args prop |> List.map ~f:(fun p -> (p, path))
f_accessor ret_typ ret_id analysis_data cur_pname loc args prop
|> List.map ~f:(fun p -> (p, path))
and sym_exec_alloc_model analysis_data pname ret_typ ret_id_typ loc prop path : Builtin.ret_typ =

Write Preview
Loading…
Cancel
Save