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

[pulse][4/5] add a path context to record timestamps

Browse Source 
Summary:
Add a new `PathContext.t` component to the abstract state. For now it
tracks only the current "timestamp" of symbolic execution inside the
procedure, i.e. which step of symbolic execution we are in (bumped by 1
each time we've executed one instruction). In the future this will also
hold, eg, which conditionals we've been through on the path (for
reporting traces with that information).

Most of the diff is about propagating the path context through many of
the APIs.

We use timestamps only in `MustBeValid` attributes to report the first
incorrect access in a function call for now.

Reviewed By: skcho

Differential Revision: D28674726

fbshipit-source-id: 2cd825e73
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent 4bad4bf63c
commit df9a7bbc81
24 changed files with 792 additions and 564 deletions
Show Stats Download Patch File Download Diff File

11
infer/src/absint/AbstractDomain.ml
Unescape View File

@ -175,7 +175,7 @@ module TopLifted (Domain : S) = struct
let pp = TopLiftedUtils.pp ~pp:Domain.pp
end
module Pair (Domain1 : S) (Domain2 : S) = struct
module PairNoJoin (Domain1 : NoJoin) (Domain2 : NoJoin) = struct
type t = Domain1.t * Domain2.t
let leq ~lhs ~rhs =
@ -183,6 +183,12 @@ module Pair (Domain1 : S) (Domain2 : S) = struct
else Domain1.leq ~lhs:(fst lhs) ~rhs:(fst rhs) && Domain2.leq ~lhs:(snd lhs) ~rhs:(snd rhs)
let pp fmt astate = Pp.pair ~fst:Domain1.pp ~snd:Domain2.pp fmt astate
end
module Pair (Domain1 : S) (Domain2 : S) = struct
include PairNoJoin (Domain1) (Domain2)
let join astate1 astate2 =
if phys_equal astate1 astate2 then astate1
else
@ -199,9 +205,6 @@ module Pair (Domain1 : S) (Domain2 : S) = struct
( Domain1.widen ~prev:(fst prev) ~next:(fst next) ~num_iters
, Domain2.widen ~prev:(snd prev) ~next:(snd next) ~num_iters )
prev next
let pp fmt astate = Pp.pair ~fst:Domain1.pp ~snd:Domain2.pp fmt astate
end
module Flat (V : PrettyPrintable.PrintableEquatableType) = struct

2
infer/src/absint/AbstractDomain.mli
Unescape View File

@ -83,6 +83,8 @@ end
(** Cartesian product of two domains. *)
module Pair (Domain1 : S) (Domain2 : S) : S with type t = Domain1.t * Domain2.t
module PairNoJoin (Domain1 : NoJoin) (Domain2 : NoJoin) : NoJoin with type t = Domain1.t * Domain2.t
(** Flat abstract domain: Bottom, Top, and non-comparable elements in between *)
module Flat (V : PrettyPrintable.PrintableEquatableType) : sig
include WithBottom

94
infer/src/pulse/Pulse.ml
Unescape View File

@ -25,7 +25,7 @@ let report_topl_errors proc_desc err_log summary =
module PulseTransferFunctions = struct
module CFG = ProcCfg.Normal
module Domain = ExecutionDomain
module Domain = AbstractDomain.PairNoJoin (PathContext) (ExecutionDomain)
type analysis_data = PulseSummary.t InterproceduralAnalysis.t
@ -33,18 +33,18 @@ module PulseTransferFunctions = struct
AnalysisCallbacks.proc_resolve_attributes pname |> Option.map ~f:Pvar.get_pvar_formals
let interprocedural_call {InterproceduralAnalysis.analyze_dependency; tenv; proc_desc} ret
let interprocedural_call {InterproceduralAnalysis.analyze_dependency; tenv; proc_desc} path ret
callee_pname call_exp actuals call_loc astate =
match callee_pname with
| Some callee_pname when not Config.pulse_intraprocedural_only ->
let formals_opt = get_pvar_formals callee_pname in
let callee_data = analyze_dependency callee_pname in
PulseCallOperations.call tenv ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname
~ret ~actuals ~formals_opt astate
PulseCallOperations.call tenv path ~caller_proc_desc:proc_desc ~callee_data call_loc
callee_pname ~ret ~actuals ~formals_opt astate
| _ ->
(* dereference call expression to catch nil issues *)
let<*> astate, _ =
PulseOperations.eval_deref ~must_be_valid_reason:BlockCall call_loc call_exp astate
PulseOperations.eval_deref path ~must_be_valid_reason:BlockCall call_loc call_exp astate
in
L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ;
let astate =
@ -72,15 +72,15 @@ module PulseTransferFunctions = struct
(** [out_of_scope_access_expr] has just gone out of scope and in now invalid *)
let exec_object_out_of_scope call_loc (pvar, typ) exec_state =
let exec_object_out_of_scope path call_loc (pvar, typ) exec_state =
match (exec_state : ExecutionDomain.t) with
| ContinueProgram astate ->
let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in
let* astate, out_of_scope_base =
PulseOperations.eval NoAccess call_loc (Exp.Lvar pvar) astate
PulseOperations.eval path NoAccess call_loc (Exp.Lvar pvar) astate
in
(* invalidate [&x] *)
PulseOperations.invalidate
PulseOperations.invalidate path
(StackAddress (Var.of_pvar pvar, []))
call_loc gone_out_of_scope out_of_scope_base astate
>>| ExecutionDomain.continue
@ -102,7 +102,7 @@ module PulseTransferFunctions = struct
let topl_event = PulseTopl.Call {return; arguments; procname} in
AbductiveDomain.Topl.small_step loc topl_event astate
in
let do_one_exec_state (exec_state : Domain.t) : Domain.t =
let do_one_exec_state (exec_state : ExecutionDomain.t) : ExecutionDomain.t =
match exec_state with
| ContinueProgram astate ->
ContinueProgram (do_astate astate)
@ -116,12 +116,12 @@ module PulseTransferFunctions = struct
List.map ~f:(Result.map ~f:do_one_exec_state) exec_state_res
let topl_store_step loc ~lhs ~rhs:_ astate =
let topl_store_step path loc ~lhs ~rhs:_ astate =
match (lhs : Exp.t) with
| Lindex (arr, index) ->
(let open IResult.Let_syntax in
let* _astate, (aw_array, _history) = PulseOperations.eval Read loc arr astate in
let+ _astate, (aw_index, _history) = PulseOperations.eval Read loc index astate in
let* _astate, (aw_array, _history) = PulseOperations.eval path Read loc arr astate in
let+ _astate, (aw_index, _history) = PulseOperations.eval path Read loc index astate in
let topl_event = PulseTopl.ArrayWrite {aw_array; aw_index} in
AbductiveDomain.Topl.small_step loc topl_event astate)
|> Result.ok (* don't emit Topl event if evals fail *) |> Option.value ~default:astate
@ -129,9 +129,9 @@ module PulseTransferFunctions = struct
astate
let dispatch_call ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) ret
let dispatch_call ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) path ret
call_exp actuals call_loc flags astate =
let<*> astate, callee_pname = PulseOperations.eval_proc_name call_loc call_exp astate in
let<*> astate, callee_pname = PulseOperations.eval_proc_name path call_loc call_exp astate in
(* special case for objc dispatch models *)
let callee_pname, actuals =
match callee_pname with
@ -148,7 +148,7 @@ module PulseTransferFunctions = struct
let<*> astate, rev_func_args =
List.fold_result actuals ~init:(astate, [])
~f:(fun (astate, rev_func_args) (actual_exp, actual_typ) ->
let+ astate, actual_evaled = PulseOperations.eval Read call_loc actual_exp astate in
let+ astate, actual_evaled = PulseOperations.eval path Read call_loc actual_exp astate in
( astate
, ProcnameDispatcher.Call.FuncArg.
{exp= actual_exp; arg_payload= actual_evaled; typ= actual_typ}
@ -176,7 +176,7 @@ module PulseTransferFunctions = struct
in
PulseCallOperations.conservatively_initialize_args arg_values astate
in
model {analysis_data; callee_procname; location= call_loc; ret} astate
model {analysis_data; path; callee_procname; location= call_loc; ret} astate
| None ->
PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;
let only_actuals_evaled =
@ -184,7 +184,7 @@ module PulseTransferFunctions = struct
(arg_payload, typ) )
in
let r =
interprocedural_call analysis_data ret callee_pname call_exp only_actuals_evaled
interprocedural_call analysis_data path ret callee_pname call_exp only_actuals_evaled
call_loc astate
in
PerfEvent.(log (fun logger -> log_end_event logger ())) ;
@ -204,7 +204,7 @@ module PulseTransferFunctions = struct
| Some pvar_typ ->
L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ;
List.map exec_states_res ~f:(fun exec_state ->
exec_state >>= exec_object_out_of_scope call_loc pvar_typ )
exec_state >>= exec_object_out_of_scope path call_loc pvar_typ )
| None ->
exec_states_res
in
@ -244,10 +244,11 @@ module PulseTransferFunctions = struct
is that some memory could be freed in dealloc, and we would be reporting a leak on it if we
didn't call it. *)
let execute_injected_dealloc_calls
({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) vars astate location =
({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) path vars astate
location =
let used_ids = Stack.keys astate |> List.filter_map ~f:(fun var -> Var.get_ident var) in
Ident.update_name_generator used_ids ;
let call_dealloc (astate_list : Domain.t list) (ret_id, id, typ, dealloc) =
let call_dealloc (astate_list : ExecutionDomain.t list) (ret_id, id, typ, dealloc) =
let ret = (ret_id, StdTyp.void) in
let call_flags = CallFlags.default in
let call_exp = Exp.Const (Cfun dealloc) in
@ -256,7 +257,7 @@ module PulseTransferFunctions = struct
L.d_printfln ~color:Pp.Orange "@\nExecuting injected instr:%a@\n@."
(Sil.pp_instr Pp.text ~print_types:true)
call_instr ;
List.concat_map astate_list ~f:(fun (astate : Domain.t) ->
List.concat_map astate_list ~f:(fun (astate : ExecutionDomain.t) ->
match astate with
| ISLLatentMemoryError _
| AbortProgram _
@ -265,7 +266,7 @@ module PulseTransferFunctions = struct
| LatentInvalidAccess _ ->
[astate]
| ContinueProgram astate ->
dispatch_call analysis_data ret call_exp actuals location call_flags astate
dispatch_call analysis_data path ret call_exp actuals location call_flags astate
|> PulseReport.report_exec_results tenv proc_desc err_log location )
in
let dynamic_types_unreachable =
@ -280,9 +281,9 @@ module PulseTransferFunctions = struct
(astates, ret_vars)
let exec_instr_aux (astate : Domain.t)
let exec_instr_aux path (astate : ExecutionDomain.t)
({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) _cfg_node
(instr : Sil.instr) : Domain.t list =
(instr : Sil.instr) : ExecutionDomain.t list =
match astate with
| AbortProgram _ | ISLLatentMemoryError _ | LatentAbortProgram _ | LatentInvalidAccess _ ->
[astate]
@ -294,17 +295,17 @@ module PulseTransferFunctions = struct
| Load {id= lhs_id; e= rhs_exp; loc} ->
(* [lhs_id := *rhs_exp] *)
let deref_rhs astate =
let result =
let results =
if Config.pulse_isl then
PulseOperations.eval_deref_isl loc rhs_exp astate
PulseOperations.eval_deref_isl path loc rhs_exp astate
|> List.map ~f:(fun result ->
let+ astate, rhs_addr_hist = result in
PulseOperations.write_id lhs_id rhs_addr_hist astate )
else
[ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in
[ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref path loc rhs_exp astate in
PulseOperations.write_id lhs_id rhs_addr_hist astate) ]
in
PulseReport.report_results tenv proc_desc err_log loc result
PulseReport.report_results tenv proc_desc err_log loc results
in
let set_global_astates =
match rhs_exp with
@ -320,7 +321,7 @@ module PulseTransferFunctions = struct
let call_flags = CallFlags.default in
let ret_id_void = (Ident.create_fresh Ident.knormal, StdTyp.void) in
let no_error_states =
dispatch_call analysis_data ret_id_void (Const (Cfun proc_name)) [] loc
dispatch_call analysis_data path ret_id_void (Const (Cfun proc_name)) [] loc
call_flags astate
|> List.filter_map ~f:(function
| Ok (ContinueProgram astate) ->
@ -347,21 +348,22 @@ module PulseTransferFunctions = struct
in
let result =
let<*> astate, (rhs_addr, rhs_history) =
PulseOperations.eval NoAccess loc rhs_exp astate
PulseOperations.eval path NoAccess loc rhs_exp astate
in
let<*> is_structured, ls_astate_lhs_addr_hist =
if Config.pulse_isl then PulseOperations.eval_structure_isl Write loc lhs_exp astate
if Config.pulse_isl then
PulseOperations.eval_structure_isl path Write loc lhs_exp astate
else
let+ astate, lhs_addr_hist = PulseOperations.eval Write loc lhs_exp astate in
let+ astate, lhs_addr_hist = PulseOperations.eval path Write loc lhs_exp astate in
(false, [Ok (astate, lhs_addr_hist)])
in
let write_function lhs_addr_hist astate =
if is_structured then
PulseOperations.write_deref_biad_isl loc ~ref:lhs_addr_hist Dereference
PulseOperations.write_deref_biad_isl path loc ~ref:lhs_addr_hist Dereference
~obj:(rhs_addr, event :: rhs_history)
astate
else
[ PulseOperations.write_deref loc ~ref:lhs_addr_hist
[ PulseOperations.write_deref path loc ~ref:lhs_addr_hist
~obj:(rhs_addr, event :: rhs_history)
astate ]
in
@ -374,7 +376,7 @@ module PulseTransferFunctions = struct
if Topl.is_active () then
List.map astates ~f:(fun result ->
let+ astate = result in
topl_store_step loc ~lhs:lhs_exp ~rhs:rhs_exp astate )
topl_store_step path loc ~lhs:lhs_exp ~rhs:rhs_exp astate )
else astates
in
match lhs_exp with
@ -387,7 +389,7 @@ module PulseTransferFunctions = struct
in
PulseReport.report_results tenv proc_desc err_log loc result
| Prune (condition, loc, _is_then_branch, _if_kind) ->
(let<*> astate = PulseOperations.prune loc ~condition astate in
(let<*> astate = PulseOperations.prune path loc ~condition astate in
if PulseArithmetic.is_unsat_cheap astate then
(* [condition] is known to be unsatisfiable: prune path *)
[]
@ -396,11 +398,11 @@ module PulseTransferFunctions = struct
[Ok (ContinueProgram astate)])
|> PulseReport.report_exec_results tenv proc_desc err_log loc
| Call (ret, call_exp, actuals, loc, call_flags) ->
dispatch_call analysis_data ret call_exp actuals loc call_flags astate
dispatch_call analysis_data path ret call_exp actuals loc call_flags astate
|> PulseReport.report_exec_results tenv proc_desc err_log loc
| Metadata (ExitScope (vars, location)) ->
let remove_vars vars astates =
List.map astates ~f:(fun (exec_state : Domain.t) ->
List.map astates ~f:(fun (exec_state : ExecutionDomain.t) ->
match exec_state with
| ISLLatentMemoryError _
| AbortProgram _
@ -417,7 +419,7 @@ module PulseTransferFunctions = struct
(* Here we add and execute calls to dealloc for Objective-C objects
before removing the variables *)
let astates, ret_vars =
execute_injected_dealloc_calls analysis_data vars astate location
execute_injected_dealloc_calls analysis_data path vars astate location
in
(* OPTIM: avoid re-allocating [vars] when [ret_vars] is empty
(in particular if no ObjC objects are involved), but otherwise
@ -428,7 +430,7 @@ module PulseTransferFunctions = struct
in
remove_vars vars_to_remove astates
| Metadata (VariableLifetimeBegins (pvar, typ, location)) when not (Pvar.is_global pvar) ->
[PulseOperations.realloc_pvar tenv pvar typ location astate |> Domain.continue]
[PulseOperations.realloc_pvar tenv pvar typ location astate |> ExecutionDomain.continue]
| Metadata
( Abstract _
| CatchEntry _
@ -440,11 +442,13 @@ module PulseTransferFunctions = struct
[ContinueProgram astate] )
let exec_instr astate analysis_data cfg_node instr =
let exec_instr (path, astate) analysis_data cfg_node instr : Domain.t list =
(* Sometimes instead of stopping on contradictions a false path condition is recorded
instead. Prune these early here so they don't spuriously count towards the disjunct limit. *)
exec_instr_aux astate analysis_data cfg_node instr
|> List.filter ~f:(fun exec_state -> not (Domain.is_unsat_cheap exec_state))
exec_instr_aux path astate analysis_data cfg_node instr
|> List.filter_map ~f:(fun exec_state ->
if ExecutionDomain.is_unsat_cheap exec_state then None
else Some (PathContext.post_exec_instr path, exec_state) )
let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"
@ -469,9 +473,11 @@ let with_debug_exit_node proc_desc ~f =
let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) =
AbstractValue.State.reset () ;
let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in
let initial = [initial_astate] in
let initial = [(PathContext.initial, initial_astate)] in
match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with
| Some posts ->
(* forget path contexts, we don't propagate them across functions *)
let posts = List.map ~f:snd posts in
with_debug_exit_node proc_desc ~f:(fun () ->
let updated_posts =
PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts

30
infer/src/pulse/PulseAbductiveDomain.ml
Unescape View File

@ -143,7 +143,7 @@ module Stack = struct
if phys_equal new_post astate.post then astate else {astate with post= new_post}
let eval location origin var astate =
let eval path location origin var astate =
match BaseStack.find_opt var (astate.post :> base_domain).stack with
| Some addr_hist ->
(astate, addr_hist)
@ -160,7 +160,7 @@ module Stack = struct
if Config.pulse_isl then
let access_trace = Trace.Immediate {location; history= []} in
BaseAddressAttributes.add_one addr
(MustBeValid (access_trace, None))
(MustBeValid (path.PathContext.timestamp, access_trace, None))
(astate.post :> base_domain).attrs
else (astate.post :> base_domain).attrs
in
@ -236,10 +236,12 @@ module AddressAttributes = struct
if phys_equal new_pre astate.pre then astate else {astate with pre= new_pre}
let check_valid ?must_be_valid_reason access_trace addr astate =
let check_valid path ?must_be_valid_reason access_trace addr astate =
let+ () = BaseAddressAttributes.check_valid addr (astate.post :> base_domain).attrs in
(* if [address] is in [pre] and it should be valid then that fact goes in the precondition *)
abduce_attribute addr (MustBeValid (access_trace, must_be_valid_reason)) astate
abduce_attribute addr
(MustBeValid (path.PathContext.timestamp, access_trace, must_be_valid_reason))
astate
let check_initialized access_trace addr astate =
@ -323,11 +325,11 @@ module AddressAttributes = struct
map_post_attrs astate ~f:(BaseAddressAttributes.add_unreachable_at addr location)
let replace_must_be_valid_reason reason addr astate =
let replace_must_be_valid_reason path reason addr astate =
match BaseAddressAttributes.get_must_be_valid addr (astate.pre :> base_domain).attrs with
| Some (trace, _reason) ->
| Some (_timestamp, trace, _reason) ->
remove_must_be_valid_attr addr astate
|> abduce_attribute addr (MustBeValid (trace, Some reason))
|> abduce_attribute addr (MustBeValid (path.PathContext.timestamp, trace, Some reason))
| None ->
astate
@ -365,7 +367,7 @@ module AddressAttributes = struct
BaseAddressAttributes.find_opt address (astate.post :> base_domain).attrs
let check_valid_isl access_trace addr ?(null_noop = false) astate =
let check_valid_isl path access_trace addr ?(null_noop = false) astate =
L.d_printfln "*****check_valid_isl: addr*** %a@\n" AbstractValue.pp addr ;
match BaseAddressAttributes.get_invalid addr (astate.post :> BaseDomain.t).attrs with
| None ->
@ -389,7 +391,9 @@ module AddressAttributes = struct
else
let valid_astate =
let abdalloc = Attribute.ISLAbduced access_trace in
let valid_attr = Attribute.MustBeValid (access_trace, None) in
let valid_attr =
Attribute.MustBeValid (path.PathContext.timestamp, access_trace, None)
in
add_one addr abdalloc astate |> abduce_attribute addr valid_attr
|> abduce_attribute addr abdalloc
in
@ -476,7 +480,7 @@ let rec set_uninitialized_post tenv src typ location ?(fields_prefix = RevList.e
let attrs =
if Config.pulse_isl then
BaseAddressAttributes.add_one addr
(MustBeValid (Immediate {location; history= []}, None))
(MustBeValid (PathContext.t0, Immediate {location; history= []}, None))
attrs
else attrs
in
@ -562,7 +566,7 @@ let mk_initial tenv proc_desc =
List.fold formals_and_captured ~init:(PreDomain.empty :> base_domain).attrs
~f:(fun attrs (_, _, (addr, _)) ->
BaseAddressAttributes.add_one addr
(MustBeValid (Immediate {location; history= []}, None))
(MustBeValid (PathContext.t0, Immediate {location; history= []}, None))
attrs )
else BaseDomain.empty.attrs
in
@ -941,8 +945,8 @@ let incorporate_new_eqs astate new_eqs =
L.d_printfln "Not clear why %a should be allocated in the first place, giving up"
AbstractValue.pp v ;
Stop Unsat
| Some must_be_valid ->
Stop (Sat (astate, Some (v, must_be_valid))) )
| Some (_, trace, reason_opt) ->
Stop (Sat (astate, Some (v, (trace, reason_opt)))) )
| EqZero _ (* [v] not allocated *) ->
Continue (astate, error) )

17
infer/src/pulse/PulseAbductiveDomain.mli
Unescape View File

@ -68,7 +68,13 @@ module Stack : sig
val find_opt : Var.t -> t -> BaseStack.value option
val eval : Location.t -> ValueHistory.t -> Var.t -> t -> t * (AbstractValue.t * ValueHistory.t)
val eval :
PathContext.t
-> Location.t
-> ValueHistory.t
-> Var.t
-> t
-> t * (AbstractValue.t * ValueHistory.t)
(** return the value of the variable in the stack or create a fresh one if needed *)
val mem : Var.t -> t -> bool
@ -114,7 +120,8 @@ module AddressAttributes : sig
val add_attrs : AbstractValue.t -> Attributes.t -> t -> t
val check_valid :
?must_be_valid_reason:Invalidation.must_be_valid_reason
PathContext.t
-> ?must_be_valid_reason:Invalidation.must_be_valid_reason
-> Trace.t
-> AbstractValue.t
-> t
@ -124,7 +131,8 @@ module AddressAttributes : sig
val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
val replace_must_be_valid_reason : Invalidation.must_be_valid_reason -> AbstractValue.t -> t -> t
val replace_must_be_valid_reason :
PathContext.t -> Invalidation.must_be_valid_reason -> AbstractValue.t -> t -> t
val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
@ -149,7 +157,8 @@ module AddressAttributes : sig
val find_opt : AbstractValue.t -> t -> Attributes.t option
val check_valid_isl :
Trace.t
PathContext.t
-> Trace.t
-> AbstractValue.t
-> ?null_noop:bool
-> t

25
infer/src/pulse/PulseAttribute.ml
Unescape View File

@ -7,6 +7,7 @@
open! IStd
module F = Format
module Invalidation = PulseInvalidation
module PathContext = PulsePathContext
module Trace = PulseTrace
module ValueHistory = PulseValueHistory
@ -34,7 +35,7 @@ module Attribute = struct
| Invalid of Invalidation.t * Trace.t
| ISLAbduced of Trace.t
| MustBeInitialized of Trace.t
| MustBeValid of Trace.t * Invalidation.must_be_valid_reason option
| MustBeValid of PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option
| StdVectorReserve
| Uninitialized
| UnreachableAt of Location.t
@ -64,7 +65,7 @@ module Attribute = struct
Variants.to_rank (Invalid (Invalidation.ConstantDereference IntLit.zero, dummy_trace))
let must_be_valid_rank = Variants.to_rank (MustBeValid (dummy_trace, None))
let must_be_valid_rank = Variants.to_rank (MustBeValid (PathContext.t0, dummy_trace, None))
let std_vector_reserve_rank = Variants.to_rank StdVectorReserve
@ -128,10 +129,11 @@ module Attribute = struct
F.fprintf f "MustBeInitialized %a"
(Trace.pp ~pp_immediate:(pp_string_if_debug "read"))
trace
| MustBeValid (trace, reason) ->
F.fprintf f "MustBeValid %a (%a)"
| MustBeValid (timestamp, trace, reason) ->
F.fprintf f "MustBeValid(%a, %a, t=%d)"
(Trace.pp ~pp_immediate:(pp_string_if_debug "access"))
trace Invalidation.pp_must_be_valid_reason reason
(timestamp :> int)
| StdVectorReserve ->
F.pp_print_string f "std::vector::reserve()"
| Uninitialized ->
@ -176,7 +178,7 @@ module Attribute = struct
true
let add_call proc_name call_location caller_history attr =
let add_call path proc_name call_location caller_history attr =
let add_call_to_trace in_call =
Trace.ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call}
in
@ -197,8 +199,8 @@ module Attribute = struct
Invalid (invalidation, add_call_to_trace trace)
| ISLAbduced trace ->
ISLAbduced (add_call_to_trace trace)
| MustBeValid (trace, reason) ->
MustBeValid (add_call_to_trace trace, reason)
| MustBeValid (_timestamp, trace, reason) ->
MustBeValid (path.PathContext.timestamp, add_call_to_trace trace, reason)
| MustBeInitialized trace ->
MustBeInitialized (add_call_to_trace trace)
| WrittenTo trace ->
@ -227,8 +229,8 @@ module Attributes = struct
let get_must_be_valid attrs =
Set.find_rank attrs Attribute.must_be_valid_rank
|> Option.map ~f:(fun attr ->
let[@warning "-8"] (Attribute.MustBeValid (trace, reason)) = attr in
(trace, reason) )
let[@warning "-8"] (Attribute.MustBeValid (timestamp, trace, reason)) = attr in
(timestamp, trace, reason) )
let get_written_to attrs =
@ -335,8 +337,9 @@ module Attributes = struct
Set.add acc attr1 )
let add_call proc_name call_location caller_history attrs =
Set.map attrs ~f:(fun attr -> Attribute.add_call proc_name call_location caller_history attr)
let add_call path proc_name call_location caller_history attrs =
Set.map attrs ~f:(fun attr ->
Attribute.add_call path proc_name call_location caller_history attr )
include Set

8
infer/src/pulse/PulseAttribute.mli
Unescape View File

@ -7,6 +7,7 @@
open! IStd
module F = Format
module Invalidation = PulseInvalidation
module PathContext = PulsePathContext
module Trace = PulseTrace
module ValueHistory = PulseValueHistory
@ -21,7 +22,7 @@ type t =
| Invalid of Invalidation.t * Trace.t
| ISLAbduced of Trace.t (** The allocation is abduced so as the analysis could run normally *)
| MustBeInitialized of Trace.t
| MustBeValid of Trace.t * Invalidation.must_be_valid_reason option
| MustBeValid of PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option
| StdVectorReserve
| Uninitialized
| UnreachableAt of Location.t
@ -53,7 +54,8 @@ module Attributes : sig
val get_isl_abduced : t -> Trace.t option
val get_must_be_valid : t -> (Trace.t * Invalidation.must_be_valid_reason option) option
val get_must_be_valid :
t -> (PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option) option
val get_written_to : t -> Trace.t option
@ -75,5 +77,5 @@ module Attributes : sig
(** While applying a spec, replacing ISLAbduced by Allocated and Invalidation.Cfree by
Invalidation.delete, if applicable *)
val add_call : Procname.t -> Location.t -> ValueHistory.t -> t -> t
val add_call : PathContext.t -> Procname.t -> Location.t -> ValueHistory.t -> t -> t
end

4
infer/src/pulse/PulseBaseAddressAttributes.ml
Unescape View File

@ -118,8 +118,8 @@ let remove_isl_abduced_attr address memory =
let remove_must_be_valid_attr address memory =
match get_attribute Attributes.get_must_be_valid address memory with
| Some (trace, reason) ->
remove_one address (Attribute.MustBeValid (trace, reason)) memory
| Some (timestamp, trace, reason) ->
remove_one address (Attribute.MustBeValid (timestamp, trace, reason)) memory
| None ->
memory

4
infer/src/pulse/PulseBaseAddressAttributes.mli
Unescape View File

@ -42,7 +42,9 @@ val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
val get_invalid : AbstractValue.t -> t -> (Invalidation.t * Trace.t) option
val get_must_be_valid :
AbstractValue.t -> t -> (Trace.t * Invalidation.must_be_valid_reason option) option
AbstractValue.t
-> t
-> (PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option) option
val is_must_be_valid_or_allocated_isl : AbstractValue.t -> t -> bool

2
infer/src/pulse/PulseBasicInterface.ml
Unescape View File

@ -16,6 +16,7 @@ module CallEvent = PulseCallEvent
module Diagnostic = PulseDiagnostic
module Invalidation = PulseInvalidation
module PathCondition = PulsePathCondition
module PathContext = PulsePathContext
module SatUnsat = PulseSatUnsat
module SkippedCalls = PulseSkippedCalls
module Trace = PulseTrace
@ -36,6 +37,7 @@ include struct
[@@deprecated "use the short form Invalidation instead"]
module PulsePathCondition = PulsePathCondition
[@@deprecated "use the short form PathCondition instead"]
module PulsePathContext = PulsePathContext [@@deprecated "use the short form PathContext instead"]
module PulseSkippedCalls = PulseSkippedCalls
[@@deprecated "use the short form SkippedCalls instead"]
module PulseTrace = PulseTrace [@@deprecated "use the short form Trace instead"]

18
infer/src/pulse/PulseCallOperations.ml
Unescape View File

@ -83,11 +83,11 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate =
|> havoc_ret ret |> add_skipped_proc
let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
let apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
~captured_vars_with_actuals ~formals ~actuals astate =
let map_call_result ~is_isl_error_prepost callee_prepost ~f =
match
PulseInterproc.apply_prepost ~is_isl_error_prepost callee_pname call_loc ~callee_prepost
PulseInterproc.apply_prepost path ~is_isl_error_prepost callee_pname call_loc ~callee_prepost
~captured_vars_with_actuals ~formals ~actuals astate
with
| (Sat (Error _) | Unsat) as path_result ->
@ -194,8 +194,8 @@ let conservatively_initialize_args arg_values ({AbductiveDomain.post} as astate)
AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate
let call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc_desc exec_states
(astate : AbductiveDomain.t) =
let call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals callee_proc_desc
exec_states (astate : AbductiveDomain.t) =
let formals =
Procdesc.get_formals callee_proc_desc
|> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar)
@ -211,7 +211,7 @@ let call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc
| (actual_closure, _) :: _
when not (Procname.is_objc_block callee_pname || List.is_empty captured_vars) ->
(* Assumption: the first parameter will be a closure *)
PulseOperations.get_captured_actuals call_loc ~captured_vars ~actual_closure astate
PulseOperations.get_captured_actuals path call_loc ~captured_vars ~actual_closure astate
| _ ->
Ok (astate, [])
in
@ -228,7 +228,7 @@ let call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc
else
(* apply all pre/post specs *)
match
apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_state
~captured_vars_with_actuals ~formals ~actuals ~ret astate
with
| Unsat ->
@ -238,7 +238,7 @@ let call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc
post :: posts )
let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc
let call tenv path ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc
callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) =
(* a special case for objc nil messaging *)
let unknown_objc_nil_messaging astate_unknown procdesc =
@ -254,7 +254,7 @@ let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) op
(ExecutionDomain.mk_initial tenv procdesc)
|> Option.value_map ~default:[] ~f:(fun nil_summary ->
let<*> nil_astate = nil_summary in
call_aux tenv caller_proc_desc call_loc callee_pname ret actuals procdesc
call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals procdesc
([ContinueProgram nil_astate] :> ExecutionDomain.t list)
astate )
in
@ -262,7 +262,7 @@ let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) op
in
match callee_data with
| Some (callee_proc_desc, exec_states) ->
call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc_desc
call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals callee_proc_desc
(exec_states :> ExecutionDomain.t list)
astate
| None ->

1
infer/src/pulse/PulseCallOperations.mli
Unescape View File

@ -13,6 +13,7 @@ type t = AbductiveDomain.t
val call :
Tenv.t
-> PathContext.t
-> caller_proc_desc:Procdesc.t
-> callee_data:(Procdesc.t * PulseSummary.t) option
-> Location.t

205
infer/src/pulse/PulseInterproc.ml
Unescape View File

@ -84,14 +84,14 @@ let pp_contradiction fmt = function
exception Contradiction of contradiction
let fold_globals_of_stack call_loc stack call_state ~f =
let fold_globals_of_stack path call_loc stack call_state ~f =
Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold BaseStack.fold)
stack ~init:call_state ~f:(fun call_state (var, stack_value) ->
match var with
| Var.ProgramVar pvar when Pvar.is_global pvar ->
let call_state, addr_hist_caller =
let astate, var_value =
Stack.eval call_loc
Stack.eval path call_loc
[ValueHistory.VariableAccessed (pvar, call_loc)]
var call_state.astate
in
@ -252,8 +252,8 @@ let materialize_pre_for_parameters callee_proc_name call_location pre_post ~form
result
let materialize_pre_for_globals callee_proc_name call_location pre_post call_state =
fold_globals_of_stack call_location (pre_post.AbductiveDomain.pre :> BaseDomain.t).stack
let materialize_pre_for_globals path callee_proc_name call_location pre_post call_state =
fold_globals_of_stack path call_location (pre_post.AbductiveDomain.pre :> BaseDomain.t).stack
call_state ~f:(fun _var ~stack_value:(addr_pre, _) ~addr_hist_caller call_state ->
materialize_pre_from_address callee_proc_name call_location
~pre:(pre_post.AbductiveDomain.pre :> BaseDomain.t)
@ -281,11 +281,11 @@ let conjoin_callee_arith pre_post call_state =
else {call_state with astate; subst}
let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state =
let apply_arithmetic_constraints path callee_proc_name call_location pre_post call_state =
let open IResult.Let_syntax in
let one_address_sat callee_attrs (addr_caller, caller_history) call_state =
let attrs_caller =
Attributes.add_call callee_proc_name call_location caller_history callee_attrs
Attributes.add_call path callee_proc_name call_location caller_history callee_attrs
in
let astate = AddressAttributes.abduce_and_add addr_caller attrs_caller call_state.astate in
if phys_equal astate call_state.astate then call_state else {call_state with astate}
@ -332,8 +332,8 @@ let apply_arithmetic_constraints callee_proc_name call_location pre_post call_st
call_state.subst call_state
let materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals
~actuals call_state =
let materialize_pre path callee_proc_name call_location pre_post ~captured_vars_with_actuals
~formals ~actuals call_state =
PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ;
let r =
let open IResult.Let_syntax in
@ -342,10 +342,10 @@ let materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_
call_state
>>= materialize_pre_for_captured_vars callee_proc_name call_location pre_post
~captured_vars_with_actuals
>>= materialize_pre_for_globals callee_proc_name call_location pre_post
>>= materialize_pre_for_globals path callee_proc_name call_location pre_post
>>= (* ...then relational arithmetic constraints in the callee's attributes will make sense in
terms of the caller's values *)
apply_arithmetic_constraints callee_proc_name call_location pre_post
apply_arithmetic_constraints path callee_proc_name call_location pre_post
in
PerfEvent.(log (fun logger -> log_end_event logger ())) ;
r
@ -386,11 +386,11 @@ let delete_edges_in_callee_pre_from_caller ~edges_pre_opt addr_caller call_state
(subst, post_edges) )
let record_post_cell callee_proc_name call_loc ~edges_pre_opt
let record_post_cell path callee_proc_name call_loc ~edges_pre_opt
~cell_callee_post:(edges_callee_post, attrs_callee_post) (addr_caller, hist_caller) call_state =
let call_state =
let attrs_post_caller =
Attributes.add_call callee_proc_name call_loc hist_caller attrs_callee_post
Attributes.add_call path callee_proc_name call_loc hist_caller attrs_callee_post
in
let astate =
if Config.pulse_isl then
@ -427,8 +427,8 @@ let record_post_cell callee_proc_name call_loc ~edges_pre_opt
; astate= AbductiveDomain.set_post_edges addr_caller edges_post_caller call_state.astate }
let rec record_post_for_address callee_proc_name call_loc ({AbductiveDomain.pre; _} as pre_post)
~addr_callee ~addr_hist_caller call_state =
let rec record_post_for_address path callee_proc_name call_loc
({AbductiveDomain.pre; _} as pre_post) ~addr_callee ~addr_hist_caller call_state =
L.d_printfln "%a<->%a" AbstractValue.pp addr_callee AbstractValue.pp (fst addr_hist_caller) ;
match visit call_state ~pre:(pre :> BaseDomain.t) ~addr_callee ~addr_hist_caller with
| `AlreadyVisited, call_state ->
@ -454,7 +454,7 @@ let rec record_post_for_address callee_proc_name call_loc ({AbductiveDomain.pre;
Attributes.replace_isl_abduced attrs_post attrs_caller
else attrs_post
in
record_post_cell callee_proc_name call_loc ~edges_pre_opt addr_hist_caller
record_post_cell path callee_proc_name call_loc ~edges_pre_opt addr_hist_caller
~cell_callee_post:(edges_post, attrs_post) call_state
in
Memory.Edges.fold ~init:call_state_after_post edges_post
@ -463,11 +463,11 @@ let rec record_post_for_address callee_proc_name call_loc ({AbductiveDomain.pre;
call_state_subst_find_or_new call_state addr_callee_dest
~default_hist_caller:(snd addr_hist_caller)
in
record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:addr_callee_dest
~addr_hist_caller:addr_hist_curr_dest call_state ) )
record_post_for_address path callee_proc_name call_loc pre_post
~addr_callee:addr_callee_dest ~addr_hist_caller:addr_hist_curr_dest call_state ) )
let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual:(actual, typ)
let record_post_for_actual path callee_proc_name call_loc pre_post ~formal ~actual:(actual, typ)
call_state =
L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractValue.pp (fst actual) ;
match
@ -479,7 +479,7 @@ let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual:(a
deref_non_c_struct addr_formal_pre typ
(pre_post.AbductiveDomain.pre :> BaseDomain.t).BaseDomain.heap
in
record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre
record_post_for_address path callee_proc_name call_loc pre_post ~addr_callee:formal_pre
~addr_hist_caller:actual call_state
with
| Some call_state ->
@ -488,7 +488,7 @@ let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual:(a
call_state
let record_post_for_return callee_proc_name call_loc pre_post call_state =
let record_post_for_return path callee_proc_name call_loc pre_post call_state =
let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in
match BaseStack.find_opt return_var (pre_post.AbductiveDomain.post :> BaseDomain.t).stack with
| None ->
@ -517,13 +517,14 @@ let record_post_for_return callee_proc_name call_loc pre_post call_state =
L.d_printfln_escaped "Recording POST from [return] <-> %a" AbstractValue.pp
(fst return_caller_addr_hist) ;
let call_state =
record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:return_callee
record_post_for_address path callee_proc_name call_loc pre_post ~addr_callee:return_callee
~addr_hist_caller:return_caller_addr_hist call_state
in
(call_state, Some return_caller_addr_hist) )
let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state =
let apply_post_for_parameters path callee_proc_name call_location pre_post ~formals ~actuals
call_state =
(* for each [(formal_i, actual_i)] pair, do [post_i = post union subst(graph reachable from
formal_i in post)], deleting previous info when comparing pre and post shows a difference
(TODO: record in the pre when a location is written to instead of just comparing values
@ -531,7 +532,8 @@ let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~
post but nuke other fields in the meantime? is that possible?). *)
match
List.fold2 formals actuals ~init:call_state ~f:(fun call_state formal actual ->
record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual call_state )
record_post_for_actual path callee_proc_name call_location pre_post ~formal ~actual
call_state )
with
| Unequal_lengths ->
(* should have been checked before by [materialize_pre] *)
@ -540,18 +542,18 @@ let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~
call_state
let apply_post_for_captured_vars callee_proc_name call_location pre_post ~captured_vars_with_actuals
call_state =
let apply_post_for_captured_vars path callee_proc_name call_location pre_post
~captured_vars_with_actuals call_state =
List.fold captured_vars_with_actuals ~init:call_state ~f:(fun call_state (formal, actual) ->
record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual call_state )
record_post_for_actual path callee_proc_name call_location pre_post ~formal ~actual call_state )
let apply_post_for_globals callee_proc_name call_location pre_post call_state =
let apply_post_for_globals path callee_proc_name call_location pre_post call_state =
match
fold_globals_of_stack call_location (pre_post.AbductiveDomain.pre :> BaseDomain.t).stack
fold_globals_of_stack path call_location (pre_post.AbductiveDomain.pre :> BaseDomain.t).stack
call_state ~f:(fun _var ~stack_value:(addr_callee, _) ~addr_hist_caller call_state ->
Ok
(record_post_for_address callee_proc_name call_location pre_post ~addr_callee
(record_post_for_address path callee_proc_name call_location pre_post ~addr_callee
~addr_hist_caller call_state) )
with
| Error _ ->
@ -560,7 +562,7 @@ let apply_post_for_globals callee_proc_name call_location pre_post call_state =
call_state
let record_post_remaining_attributes callee_proc_name call_loc pre_post call_state =
let record_post_remaining_attributes path callee_proc_name call_loc pre_post call_state =
BaseAddressAttributes.fold
(fun addr_callee attrs call_state ->
if AddressSet.mem addr_callee call_state.visited then
@ -571,7 +573,7 @@ let record_post_remaining_attributes callee_proc_name call_loc pre_post call_sta
| None ->
(* callee address has no meaning for the caller *) call_state
| Some (addr_caller, history) ->
let attrs' = Attributes.add_call callee_proc_name call_loc history attrs in
let attrs' = Attributes.add_call path callee_proc_name call_loc history attrs in
let astate = AddressAttributes.abduce_and_add addr_caller attrs' call_state.astate in
{call_state with astate} )
(pre_post.AbductiveDomain.post :> BaseDomain.t).attrs call_state
@ -587,20 +589,21 @@ let record_skipped_calls callee_proc_name call_loc pre_post call_state =
{call_state with astate}
let apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals ~actuals
call_state =
let apply_post path callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals
~actuals call_state =
let open IResult.Let_syntax in
PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ;
let r =
let call_state, return_caller =
apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state
|> apply_post_for_captured_vars callee_proc_name call_location pre_post
apply_post_for_parameters path callee_proc_name call_location pre_post ~formals ~actuals
call_state
|> apply_post_for_captured_vars path callee_proc_name call_location pre_post
~captured_vars_with_actuals
|> apply_post_for_globals callee_proc_name call_location pre_post
|> record_post_for_return callee_proc_name call_location pre_post
|> apply_post_for_globals path callee_proc_name call_location pre_post
|> record_post_for_return path callee_proc_name call_location pre_post
in
let+ call_state =
record_post_remaining_attributes callee_proc_name call_location pre_post call_state
record_post_remaining_attributes path callee_proc_name call_location pre_post call_state
|> record_skipped_calls callee_proc_name call_location pre_post
|> conjoin_callee_arith pre_post
in
@ -610,50 +613,78 @@ let apply_post callee_proc_name call_location pre_post ~captured_vars_with_actua
r
let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call_state =
AddressMap.fold
(fun addr_pre (addr_caller, hist_caller) astate_result ->
let mk_access_trace callee_access_trace =
Trace.ViaCall
{ in_call= callee_access_trace
; f= Call callee_proc_name
; location= call_location
; history= hist_caller }
in
let open IResult.Let_syntax in
let* astate = astate_result in
let* astate =
match BaseAddressAttributes.get_must_be_valid addr_pre (pre :> BaseDomain.t).attrs with
let check_all_valid path callee_proc_name call_location {AbductiveDomain.pre; _} call_state =
(* collect all the checks to perform then do each check in timestamp order to make sure we report
the first issue if any *)
let addresses_to_check =
AddressMap.fold
(fun addr_pre addr_hist_caller to_check ->
let to_check =
match BaseAddressAttributes.get_must_be_valid addr_pre (pre :> BaseDomain.t).attrs with
| None ->
to_check
| Some must_be_valid_data ->
(addr_hist_caller, `MustBeValid must_be_valid_data) :: to_check
in
match
BaseAddressAttributes.get_must_be_initialized addr_pre (pre :> BaseDomain.t).attrs
with
| None ->
astate_result
| Some (callee_access_trace, must_be_valid_reason) ->
let access_trace = mk_access_trace callee_access_trace in
AddressAttributes.check_valid access_trace addr_caller astate
|> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
AccessResult.ReportableError
{ diagnostic=
Diagnostic.AccessToInvalidAddress
{ calling_context= []
; invalidation
; invalidation_trace
; access_trace
; must_be_valid_reason }
; astate } )
in
match BaseAddressAttributes.get_must_be_initialized addr_pre (pre :> BaseDomain.t).attrs with
| None ->
astate_result
| Some callee_access_trace ->
let access_trace = mk_access_trace callee_access_trace in
AddressAttributes.check_initialized access_trace addr_caller astate
|> Result.map_error ~f:(fun () ->
L.d_printfln "ERROR: caller's %a is uninitialized!" AbstractValue.pp addr_caller ;
AccessResult.ReportableError
{ diagnostic=
Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace}
; astate } ) )
call_state.subst (Ok call_state.astate)
to_check
| Some must_be_init_data ->
(addr_hist_caller, `MustBeInitialized must_be_init_data) :: to_check )
call_state.subst []
in
let timestamp_of_check = function
| `MustBeValid (timestamp, _, _) ->
Some timestamp
| `MustBeInitialized _ ->
None
in
List.sort addresses_to_check ~compare:(fun (_, check1) (_, check2) ->
match (timestamp_of_check check1, timestamp_of_check check2) with
| Some t1, Some t2 ->
(* smaller timestamp first *) PathContext.compare_timestamp t1 t2
(* with a timestamp first (gone soon when MustBeInitialized will get a timestamp too), otherwise dummy comparison *)
| None, None ->
0
| Some _, None ->
-1
| None, Some _ ->
1 )
|> List.fold_result ~init:call_state.astate ~f:(fun astate ((addr_caller, hist_caller), check) ->
let mk_access_trace callee_access_trace =
Trace.ViaCall
{ in_call= callee_access_trace
; f= Call callee_proc_name
; location= call_location
; history= hist_caller }
in
match check with
| `MustBeValid (_timestamp, callee_access_trace, must_be_valid_reason) ->
let access_trace = mk_access_trace callee_access_trace in
AddressAttributes.check_valid path access_trace addr_caller astate
|> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
AccessResult.ReportableError
{ diagnostic=
Diagnostic.AccessToInvalidAddress
{ calling_context= []
; invalidation
; invalidation_trace
; access_trace
; must_be_valid_reason }
; astate } )
| `MustBeInitialized callee_access_trace ->
let access_trace = mk_access_trace callee_access_trace in
AddressAttributes.check_initialized access_trace addr_caller astate
|> Result.map_error ~f:(fun () ->
L.d_printfln "ERROR: caller's %a is uninitialized!" AbstractValue.pp addr_caller ;
AccessResult.ReportableError
{ diagnostic=
Diagnostic.ReadUninitializedValue
{calling_context= []; trace= access_trace}
; astate } ) )
let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location
@ -704,7 +735,7 @@ let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location
- for each actual, write the post for that actual
- if aliasing is introduced at any time then give up *)
let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_prepost:pre_post
let apply_prepost path ~is_isl_error_prepost callee_proc_name call_location ~callee_prepost:pre_post
~captured_vars_with_actuals ~formals ~actuals astate =
L.d_printfln "Applying pre/post for %a(%a):@\n%a" Procname.pp callee_proc_name
(Pp.seq ~sep:"," Var.pp) formals AbductiveDomain.pp pre_post ;
@ -717,8 +748,8 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p
in
(* read the precondition *)
match
materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals
~actuals empty_call_state
materialize_pre path callee_proc_name call_location pre_post ~captured_vars_with_actuals
~formals ~actuals empty_call_state
with
| exception Contradiction reason ->
(* can't make sense of the pre-condition in the current context: give up on that particular
@ -738,7 +769,7 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p
ContinueProgram ok specs *)
let* astate =
if Config.pulse_isl then Ok astate
else check_all_valid callee_proc_name call_location pre_post call_state
else check_all_valid path callee_proc_name call_location pre_post call_state
in
(* reset [visited] *)
let invalid_subst = call_state.invalid_subst in
@ -746,8 +777,8 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p
let call_state = {call_state with astate; visited= AddressSet.empty} in
(* apply the postcondition *)
let* call_state, return_caller =
apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals
~actuals call_state
apply_post path callee_proc_name call_location pre_post ~captured_vars_with_actuals
~formals ~actuals call_state
in
let astate =
if Topl.is_active () then

3
infer/src/pulse/PulseInterproc.mli
Unescape View File

@ -10,7 +10,8 @@ open PulseBasicInterface
open PulseDomainInterface
val apply_prepost :
is_isl_error_prepost:bool
PathContext.t
-> is_isl_error_prepost:bool
-> Procname.t
-> Location.t
-> callee_prepost:AbductiveDomain.t

578
infer/src/pulse/PulseModels.ml
View File

File diff suppressed because it is too large Load Diff

1
infer/src/pulse/PulseModels.mli
Unescape View File

@ -10,6 +10,7 @@ open PulseDomainInterface
type model_data =
{ analysis_data: PulseSummary.t InterproceduralAnalysis.t
; path: PathContext.t
; callee_procname: Procname.t
; location: Location.t
; ret: Ident.t * Typ.t }

31
infer/src/pulse/PulseObjectiveCSummary.ml
Unescape View File

@ -15,7 +15,7 @@ let mk_objc_self_pvar proc_desc =
Pvar.mk Mangled.self proc_name
let init_fields_zero tenv location ~zero addr typ astate =
let init_fields_zero tenv path location ~zero addr typ astate =
let get_fields typ =
match typ.Typ.desc with
| Tstruct struct_name ->
@ -31,7 +31,7 @@ let init_fields_zero tenv location ~zero addr typ astate =
let acc, field_addr = Memory.eval_edge addr (FieldAccess field) acc in
init_fields_zero_helper field_addr field_typ acc )
| None ->
PulseOperations.write_deref location ~ref:addr ~obj:zero astate
PulseOperations.write_deref path location ~ref:addr ~obj:zero astate
in
init_fields_zero_helper addr typ astate
@ -39,10 +39,11 @@ let init_fields_zero tenv location ~zero addr typ astate =
let mk_objc_method_nil_summary_aux tenv proc_desc astate =
(* Constructs summary {self = 0} {return = self}.
This allows us to connect invalidation with invalid access in the trace *)
let path = PathContext.initial in
let location = Procdesc.get_loc proc_desc in
let self = mk_objc_self_pvar proc_desc in
let* astate, (self_value, self_history) =
PulseOperations.eval_deref location (Lvar self) astate
PulseOperations.eval_deref path location (Lvar self) astate
in
let* astate = PulseArithmetic.prune_eq_zero self_value astate in
let event = ValueHistory.NilMessaging location in
@ -51,14 +52,16 @@ let mk_objc_method_nil_summary_aux tenv proc_desc astate =
| Some (last_formal, {desc= Tptr (typ, _)}) when Mangled.is_return_param last_formal ->
let ret_param_var = Procdesc.get_ret_param_var proc_desc in
let* astate, ret_param_var_addr_hist =
PulseOperations.eval_deref location (Lvar ret_param_var) astate
PulseOperations.eval_deref path location (Lvar ret_param_var) astate
in
init_fields_zero tenv location ~zero:updated_self_value_hist ret_param_var_addr_hist typ
init_fields_zero tenv path location ~zero:updated_self_value_hist ret_param_var_addr_hist typ
astate
| _ ->
let ret_var = Procdesc.get_ret_var proc_desc in
let* astate, ret_var_addr_hist = PulseOperations.eval Write location (Lvar ret_var) astate in
PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:updated_self_value_hist
let* astate, ret_var_addr_hist =
PulseOperations.eval path Write location (Lvar ret_var) astate
in
PulseOperations.write_deref path location ~ref:ret_var_addr_hist ~obj:updated_self_value_hist
astate
@ -88,7 +91,9 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log}
match astate with
| ContinueProgram astate ->
let result =
let* astate, value = PulseOperations.eval_deref location (Lvar self) astate in
let* astate, value =
PulseOperations.eval_deref PathContext.initial location (Lvar self) astate
in
PulseArithmetic.prune_positive (fst value) astate
in
PulseReport.report_result tenv proc_desc err_log location result
@ -111,6 +116,7 @@ let append_objc_actual_self_positive procdesc self_actual astate =
let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_log} astate =
let path = PathContext.initial in
let location = Procdesc.get_loc proc_desc in
let self = mk_objc_self_pvar proc_desc in
let proc_name = Procdesc.get_proc_name proc_desc in
@ -119,12 +125,9 @@ let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_lo
when not (Procdesc.is_ret_type_pod proc_desc) ->
let result =
(* add reason for must be valid to be because the return type is non pod *)
let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in
let astate =
AddressAttributes.replace_must_be_valid_reason Invalidation.SelfOfNonPODReturnMethod
(fst value) astate
in
astate
let+ astate, value = PulseOperations.eval_deref path location (Lvar self) astate in
AddressAttributes.replace_must_be_valid_reason path SelfOfNonPODReturnMethod (fst value)
astate
in
PulseReport.report_result tenv proc_desc err_log location result
| ContinueProgram _, _

184
infer/src/pulse/PulseOperations.ml
Unescape View File

@ -50,10 +50,10 @@ end
include Import
let check_addr_access ?must_be_valid_reason access_mode location (address, history) astate =
let check_addr_access path ?must_be_valid_reason access_mode location (address, history) astate =
let access_trace = Trace.Immediate {location; history} in
let* astate =
AddressAttributes.check_valid ?must_be_valid_reason access_trace address astate
AddressAttributes.check_valid path ?must_be_valid_reason access_trace address astate
|> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
ReportableError
{ diagnostic=
@ -79,10 +79,10 @@ let check_addr_access ?must_be_valid_reason access_mode location (address, histo
Ok astate
let check_and_abduce_addr_access_isl access_mode location (address, history) ?(null_noop = false)
astate =
let check_and_abduce_addr_access_isl path access_mode location (address, history)
?(null_noop = false) astate =
let access_trace = Trace.Immediate {location; history} in
AddressAttributes.check_valid_isl access_trace address ~null_noop astate
AddressAttributes.check_valid_isl path access_trace address ~null_noop astate
|> List.map ~f:(fun access_result ->
let* astate = AccessResult.of_abductive_access_result access_trace access_result in
match access_mode with
@ -137,7 +137,7 @@ module Closures = struct
Memory.Edges.add (HilExp.Access.FieldAccess (mk_fake_field ~id mode)) (addr, trace) edges )
let check_captured_addresses action lambda_addr (astate : t) =
let check_captured_addresses path action lambda_addr (astate : t) =
match AbductiveDomain.find_post_cell_opt lambda_addr astate with
| None ->
Ok astate
@ -147,7 +147,7 @@ module Closures = struct
| Attribute.Closure _ ->
IContainer.iter_result ~fold:Memory.Edges.fold edges ~f:(fun (access, addr_trace) ->
if is_captured_by_ref_fake_access access then
let+ _ = check_addr_access Read action addr_trace astate in
let+ _ = check_addr_access path Read action addr_trace astate in
()
else Ok () )
| _ ->
@ -172,50 +172,52 @@ module Closures = struct
(astate, closure_addr_hist)
end
let eval_var location hist var astate = Stack.eval location hist var astate
let eval_access ?must_be_valid_reason mode location addr_hist access astate =
let+ astate = check_addr_access ?must_be_valid_reason mode location addr_hist astate in
let eval_access path ?must_be_valid_reason mode location addr_hist access astate =
let+ astate = check_addr_access path ?must_be_valid_reason mode location addr_hist astate in
Memory.eval_edge addr_hist access astate
let eval_deref_access ?must_be_valid_reason mode location addr_hist access astate =
let* astate, addr_hist = eval_access Read location addr_hist access astate in
eval_access ?must_be_valid_reason mode location addr_hist Dereference astate
let eval_deref_access path ?must_be_valid_reason mode location addr_hist access astate =
let* astate, addr_hist = eval_access path Read location addr_hist access astate in
eval_access path ?must_be_valid_reason mode location addr_hist Dereference astate
let eval_access_biad_isl mode location addr_hist access astate =
let eval_access_biad_isl path mode location addr_hist access astate =
let map_ok addr_hist access results =
List.map results ~f:(fun result ->
let+ astate = result in
Memory.eval_edge addr_hist access astate )
in
let results = check_and_abduce_addr_access_isl mode location addr_hist astate in
let results = check_and_abduce_addr_access_isl path mode location addr_hist astate in
map_ok addr_hist access results
let eval mode location exp0 astate =
let rec eval mode exp astate =
let eval path mode location exp0 astate =
let rec eval path mode exp astate =
match (exp : Exp.t) with
| Var id ->
Ok (eval_var location (* error in case of missing history? *) [] (Var.of_id id) astate)
Ok
(Stack.eval path location (* error in case of missing history? *) [] (Var.of_id id)
astate)
| Lvar pvar ->
Ok
(eval_var location
(Stack.eval path location
[ValueHistory.VariableAccessed (pvar, location)]
(Var.of_pvar pvar) astate)
| Lfield (exp', field, _) ->
let* astate, addr_hist = eval Read exp' astate in
eval_access mode location addr_hist (FieldAccess field) astate
let* astate, addr_hist = eval path Read exp' astate in
eval_access path mode location addr_hist (FieldAccess field) astate
| Lindex (exp', exp_index) ->
let* astate, addr_hist_index = eval Read exp_index astate in
let* astate, addr_hist = eval Read exp' astate in
eval_access mode location addr_hist (ArrayAccess (StdTyp.void, fst addr_hist_index)) astate
let* astate, addr_hist_index = eval path Read exp_index astate in
let* astate, addr_hist = eval path Read exp' astate in
eval_access path mode location addr_hist
(ArrayAccess (StdTyp.void, fst addr_hist_index))
astate
| Closure {name; captured_vars} ->
let+ astate, rev_captured =
List.fold_result captured_vars ~init:(astate, [])
~f:(fun (astate, rev_captured) (capt_exp, captured_as, _, mode) ->
let+ astate, addr_trace = eval Read capt_exp astate in
let+ astate, addr_trace = eval path Read capt_exp astate in
(astate, (captured_as, addr_trace, mode) :: rev_captured) )
in
Closures.record location name (List.rev rev_captured) astate
@ -223,7 +225,7 @@ let eval mode location exp0 astate =
(* function pointers are represented as closures with no captured variables *)
Ok (Closures.record location proc_name [] astate)
| Cast (_, exp') ->
eval mode exp' astate
eval path mode exp' astate
| Const (Cint i) ->
let v = AbstractValue.Constants.get_int i in
let invalidation = Invalidation.ConstantDereference i in
@ -235,14 +237,14 @@ let eval mode location exp0 astate =
in
(astate, (v, [ValueHistory.Invalidated (invalidation, location)]))
| UnOp (unop, exp, _typ) ->
let* astate, (addr, hist) = eval Read exp astate in
let* astate, (addr, hist) = eval path Read exp astate in
let unop_addr = AbstractValue.mk_fresh () in
let+ astate = PulseArithmetic.eval_unop unop_addr unop addr astate in
(astate, (unop_addr, hist))
| BinOp (bop, e_lhs, e_rhs) ->
let* astate, (addr_lhs, hist_lhs) = eval Read e_lhs astate in
let* astate, (addr_lhs, hist_lhs) = eval path Read e_lhs astate in
(* NOTE: keeping track of only [hist_lhs] into the binop is not the best *)
let* astate, (addr_rhs, _hist_rhs) = eval Read e_rhs astate in
let* astate, (addr_rhs, _hist_rhs) = eval path Read e_rhs astate in
let binop_addr = AbstractValue.mk_fresh () in
let+ astate =
PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs)
@ -252,24 +254,24 @@ let eval mode location exp0 astate =
| Const _ | Sizeof _ | Exn _ ->
Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
in
eval mode exp0 astate
eval path mode exp0 astate
let eval_to_operand mode location exp astate =
let eval_to_operand path mode location exp astate =
match (exp : Exp.t) with
| Const (Cint i) ->
Ok (astate, PulseArithmetic.LiteralOperand i)
| exp ->
let+ astate, (value, _) = eval mode location exp astate in
let+ astate, (value, _) = eval path mode location exp astate in
(astate, PulseArithmetic.AbstractValueOperand value)
let prune location ~condition astate =
let prune path location ~condition astate =
let rec prune_aux ~negated exp astate =
match (exp : Exp.t) with
| BinOp (bop, exp_lhs, exp_rhs) ->
let* astate, lhs_op = eval_to_operand Read location exp_lhs astate in
let* astate, rhs_op = eval_to_operand Read location exp_rhs astate in
let* astate, lhs_op = eval_to_operand path Read location exp_lhs astate in
let* astate, rhs_op = eval_to_operand path Read location exp_rhs astate in
PulseArithmetic.prune_binop ~negated bop lhs_op rhs_op astate
| UnOp (LNot, exp', _) ->
prune_aux ~negated:(not negated) exp' astate
@ -279,53 +281,53 @@ let prune location ~condition astate =
prune_aux ~negated:false condition astate
let eval_deref ?must_be_valid_reason location exp astate =
let* astate, addr_hist = eval Read location exp astate in
let+ astate = check_addr_access ?must_be_valid_reason Read location addr_hist astate in
let eval_deref path ?must_be_valid_reason location exp astate =
let* astate, addr_hist = eval path Read location exp astate in
let+ astate = check_addr_access path ?must_be_valid_reason Read location addr_hist astate in
Memory.eval_edge addr_hist Dereference astate
let eval_proc_name location call_exp astate =
let eval_proc_name path location call_exp astate =
match (call_exp : Exp.t) with
| Const (Cfun proc_name) | Closure {name= proc_name} ->
Ok (astate, Some proc_name)
| _ ->
let+ astate, (f, _) = eval Read location call_exp astate in
let+ astate, (f, _) = eval path Read location call_exp astate in
(astate, AddressAttributes.get_closure_proc_name f astate)
let eval_structure_isl mode loc exp astate =
let eval_structure_isl path mode loc exp astate =
match (exp : Exp.t) with
| Lfield (exp', field, _) ->
let+ astate, addr_hist = eval mode loc exp' astate in
let astates = eval_access_biad_isl mode loc addr_hist (FieldAccess field) astate in
let+ astate, addr_hist = eval path mode loc exp' astate in
let astates = eval_access_biad_isl path mode loc addr_hist (FieldAccess field) astate in
(false, astates)
| Lindex (exp', exp_index) ->
let* astate, addr_hist_index = eval mode loc exp_index astate in
let+ astate, addr_hist = eval mode loc exp' astate in
let* astate, addr_hist_index = eval path mode loc exp_index astate in
let+ astate, addr_hist = eval path mode loc exp' astate in
let astates =
eval_access_biad_isl mode loc addr_hist
eval_access_biad_isl path mode loc addr_hist
(ArrayAccess (StdTyp.void, fst addr_hist_index))
astate
in
(false, astates)
| _ ->
let+ astate, (addr, history) = eval mode loc exp astate in
let+ astate, (addr, history) = eval path mode loc exp astate in
(true, [Ok (astate, (addr, history))])
let eval_deref_biad_isl location access addr_hist astate =
check_and_abduce_addr_access_isl Read location addr_hist astate
let eval_deref_biad_isl path location access addr_hist astate =
check_and_abduce_addr_access_isl path Read location addr_hist astate
|> List.map ~f:(fun result ->
let+ astate = result in
Memory.eval_edge addr_hist access astate )
let eval_deref_isl location exp astate =
let<*> is_structured, ls_astate_addr_hist = eval_structure_isl Read location exp astate in
let eval_deref_isl path location exp astate =
let<*> is_structured, ls_astate_addr_hist = eval_structure_isl path Read location exp astate in
let eval_deref_function (astate, addr_hist) =
if is_structured then eval_deref_biad_isl location Dereference addr_hist astate
else [eval_deref location exp astate]
if is_structured then eval_deref_biad_isl path location Dereference addr_hist astate
else [eval_deref path location exp astate]
in
List.concat_map ls_astate_addr_hist ~f:(fun result ->
let<*> astate_addr = result in
@ -349,42 +351,44 @@ let havoc_id id loc_opt astate =
else astate
let write_access location addr_trace_ref access addr_trace_obj astate =
check_addr_access Write location addr_trace_ref astate
let write_access path location addr_trace_ref access addr_trace_obj astate =
check_addr_access path Write location addr_trace_ref astate
>>| Memory.add_edge addr_trace_ref access addr_trace_obj location
let write_access_biad_isl location addr_trace_ref access addr_trace_obj astate =
let astates = check_and_abduce_addr_access_isl Write location addr_trace_ref astate in
let write_access_biad_isl path location addr_trace_ref access addr_trace_obj astate =
let astates = check_and_abduce_addr_access_isl path Write location addr_trace_ref astate in
List.map astates ~f:(fun result ->
let+ astate = result in
Memory.add_edge addr_trace_ref access addr_trace_obj location astate )
let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate =
write_access location addr_trace_ref Dereference addr_trace_obj astate
let write_deref path location ~ref:addr_trace_ref ~obj:addr_trace_obj astate =
write_access path location addr_trace_ref Dereference addr_trace_obj astate
let write_deref_biad_isl location ~ref:(addr_ref, addr_ref_history) access ~obj:addr_trace_obj
let write_deref_biad_isl path location ~ref:(addr_ref, addr_ref_history) access ~obj:addr_trace_obj
astate =
write_access_biad_isl location (addr_ref, addr_ref_history) access addr_trace_obj astate
write_access_biad_isl path location (addr_ref, addr_ref_history) access addr_trace_obj astate
let write_field location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate =
write_access location addr_trace_ref (FieldAccess field) addr_trace_obj astate
let write_field path location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate =
write_access path location addr_trace_ref (FieldAccess field) addr_trace_obj astate
let write_deref_field location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate =
let* astate, addr_hist = eval_access Read location addr_trace_ref (FieldAccess field) astate in
write_deref location ~ref:addr_hist ~obj:addr_trace_obj astate
let write_deref_field path location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate =
let* astate, addr_hist =
eval_access path Read location addr_trace_ref (FieldAccess field) astate
in
write_deref path location ~ref:addr_hist ~obj:addr_trace_obj astate
let write_arr_index location ~ref:addr_trace_ref ~index ~obj:addr_trace_obj astate =
write_access location addr_trace_ref (ArrayAccess (StdTyp.void, index)) addr_trace_obj astate
let write_arr_index path location ~ref:addr_trace_ref ~index ~obj:addr_trace_obj astate =
write_access path location addr_trace_ref (ArrayAccess (StdTyp.void, index)) addr_trace_obj astate
let havoc_deref_field location addr_trace field trace_obj astate =
write_deref_field location ~ref:addr_trace field
let havoc_deref_field path location addr_trace field trace_obj astate =
write_deref_field path location ~ref:addr_trace field
~obj:(AbstractValue.mk_fresh (), trace_obj)
astate
@ -405,10 +409,10 @@ type invalidation_access =
| StackAddress of Var.t * ValueHistory.t
| UntraceableAccess
let record_invalidation access_path location cause astate =
let record_invalidation path access_path location cause astate =
match access_path with
| StackAddress (x, hist0) ->
let astate, (addr, hist) = Stack.eval location hist0 x astate in
let astate, (addr, hist) = Stack.eval path location hist0 x astate in
Stack.add x (addr, Invalidated (cause, location) :: hist) astate
| MemoryAccess {pointer; access; hist_obj_default} ->
let addr_obj, hist_obj =
@ -425,40 +429,40 @@ let record_invalidation access_path location cause astate =
astate
let invalidate access_path location cause addr_trace astate =
check_addr_access NoAccess location addr_trace astate
let invalidate path access_path location cause addr_trace astate =
check_addr_access path NoAccess location addr_trace astate
>>| AddressAttributes.invalidate addr_trace cause location
>>| record_invalidation access_path location cause
>>| record_invalidation path access_path location cause
let invalidate_biad_isl location cause (address, history) astate =
check_and_abduce_addr_access_isl NoAccess location (address, history) ~null_noop:true astate
let invalidate_biad_isl path location cause (address, history) astate =
check_and_abduce_addr_access_isl path NoAccess location (address, history) ~null_noop:true astate
|> List.map ~f:(fun result ->
let+ astate = result in
AddressAttributes.invalidate (address, history) cause location astate )
let invalidate_access location cause ref_addr_hist access astate =
let invalidate_access path location cause ref_addr_hist access astate =
let astate, (addr_obj, hist_obj) = Memory.eval_edge ref_addr_hist access astate in
invalidate
invalidate path
(MemoryAccess {pointer= ref_addr_hist; access; hist_obj_default= hist_obj})
location cause
(addr_obj, snd ref_addr_hist)
astate
let invalidate_deref_access location cause ref_addr_hist access astate =
let invalidate_deref_access path location cause ref_addr_hist access astate =
let astate, addr_hist = Memory.eval_edge ref_addr_hist access astate in
let astate, (addr_obj, hist_obj) = Memory.eval_edge addr_hist Dereference astate in
invalidate
invalidate path
(MemoryAccess {pointer= ref_addr_hist; access; hist_obj_default= hist_obj})
location cause
(addr_obj, snd ref_addr_hist)
astate
let invalidate_array_elements location cause addr_trace astate =
let+ astate = check_addr_access NoAccess location addr_trace astate in
let invalidate_array_elements path location cause addr_trace astate =
let+ astate = check_addr_access path NoAccess location addr_trace astate in
match Memory.find_opt (fst addr_trace) astate with
| None ->
astate
@ -467,15 +471,15 @@ let invalidate_array_elements location cause addr_trace astate =
match (access : Memory.Access.t) with
| ArrayAccess _ as access ->
AddressAttributes.invalidate dest_addr_trace cause location astate
|> record_invalidation
|> record_invalidation path
(MemoryAccess {pointer= addr_trace; access; hist_obj_default= snd dest_addr_trace})
location cause
| _ ->
astate )
let shallow_copy location addr_hist astate =
let+ astate = check_addr_access Read location addr_hist astate in
let shallow_copy path location addr_hist astate =
let+ astate = check_addr_access path Read location addr_hist astate in
let cell =
match AbductiveDomain.find_post_cell_opt (fst addr_hist) astate with
| None ->
@ -668,13 +672,13 @@ let remove_vars vars location astate =
Stack.remove_vars vars astate
let get_captured_actuals location ~captured_vars ~actual_closure astate =
let* astate, this_value_addr = eval_access Read location actual_closure Dereference astate in
let get_captured_actuals path location ~captured_vars ~actual_closure astate =
let* astate, this_value_addr = eval_access path Read location actual_closure Dereference astate in
let+ _, astate, captured_vars_with_actuals =
List.fold_result captured_vars ~init:(0, astate, [])
~f:(fun (id, astate, captured) (var, mode, typ) ->
let+ astate, captured_actual =
eval_access Read location this_value_addr
eval_access path Read location this_value_addr
(FieldAccess (Closures.mk_fake_field ~id mode))
astate
in

83
infer/src/pulse/PulseOperations.mli
Unescape View File

@ -68,7 +68,8 @@ include module type of Import
type t = AbductiveDomain.t
val check_addr_access :
?must_be_valid_reason:Invalidation.must_be_valid_reason
PathContext.t
-> ?must_be_valid_reason:Invalidation.must_be_valid_reason
-> access_mode
-> Location.t
-> AbstractValue.t * ValueHistory.t
@ -77,12 +78,18 @@ val check_addr_access :
(** Check that the [address] is not known to be invalid *)
module Closures : sig
val check_captured_addresses : Location.t -> AbstractValue.t -> t -> t AccessResult.t
val check_captured_addresses :
PathContext.t -> Location.t -> AbstractValue.t -> t -> t AccessResult.t
(** assert the validity of the addresses captured by the lambda *)
end
val eval :
access_mode -> Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t
PathContext.t
-> access_mode
-> Location.t
-> Exp.t
-> t
-> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t
(** Use the stack and heap to evaluate the given expression down to an abstract address representing
its value.
@ -90,7 +97,8 @@ val eval :
known to be invalid. *)
val eval_structure_isl :
access_mode
PathContext.t
-> access_mode
-> Location.t
-> Exp.t
-> t
@ -98,10 +106,11 @@ val eval_structure_isl :
(** Similar to eval but apply to data structures and ISL abduction. Return a list of abduced states
(ISLOk and ISLErs); The boolean indicates whether it is data structures or not. *)
val prune : Location.t -> condition:Exp.t -> t -> t AccessResult.t
val prune : PathContext.t -> Location.t -> condition:Exp.t -> t -> t AccessResult.t
val eval_deref :
?must_be_valid_reason:Invalidation.must_be_valid_reason
PathContext.t
-> ?must_be_valid_reason:Invalidation.must_be_valid_reason
-> Location.t
-> Exp.t
-> t
@ -109,10 +118,15 @@ val eval_deref :
(** Like [eval] but evaluates [*exp]. *)
val eval_deref_isl :
Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t list
PathContext.t
-> Location.t
-> Exp.t
-> t
-> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t list
val eval_access :
?must_be_valid_reason:Invalidation.must_be_valid_reason
PathContext.t
-> ?must_be_valid_reason:Invalidation.must_be_valid_reason
-> access_mode
-> Location.t
-> AbstractValue.t * ValueHistory.t
@ -123,7 +137,8 @@ val eval_access :
so dereferences it according to the access. *)
val eval_deref_access :
?must_be_valid_reason:Invalidation.must_be_valid_reason
PathContext.t
-> ?must_be_valid_reason:Invalidation.must_be_valid_reason
-> access_mode
-> Location.t
-> AbstractValue.t * ValueHistory.t
@ -132,12 +147,14 @@ val eval_deref_access :
-> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t
(** Like [eval_access] but does additional dereference. *)
val eval_proc_name : Location.t -> Exp.t -> t -> (t * Procname.t option) AccessResult.t
val eval_proc_name :
PathContext.t -> Location.t -> Exp.t -> t -> (t * Procname.t option) AccessResult.t
val havoc_id : Ident.t -> ValueHistory.t -> t -> t
val havoc_deref_field :
Location.t
PathContext.t
-> Location.t
-> AbstractValue.t * ValueHistory.t
-> Fieldname.t
-> ValueHistory.t
@ -150,7 +167,8 @@ val realloc_pvar : Tenv.t -> Pvar.t -> Typ.t -> Location.t -> t -> t
val write_id : Ident.t -> AbstractValue.t * ValueHistory.t -> t -> t
val write_field :
Location.t
PathContext.t
-> Location.t
-> ref:AbstractValue.t * ValueHistory.t
-> Fieldname.t
-> obj:AbstractValue.t * ValueHistory.t
@ -159,7 +177,8 @@ val write_field :
(** write the edge [ref --.field--> obj] *)
val write_deref_field :
Location.t
PathContext.t
-> Location.t
-> ref:AbstractValue.t * ValueHistory.t
-> Fieldname.t
-> obj:AbstractValue.t * ValueHistory.t
@ -168,7 +187,8 @@ val write_deref_field :
(** write the edge [ref --.field--> _ --*--> obj] *)
val write_arr_index :
Location.t
PathContext.t
-> Location.t
-> ref:AbstractValue.t * ValueHistory.t
-> index:AbstractValue.t
-> obj:AbstractValue.t * ValueHistory.t
@ -177,7 +197,8 @@ val write_arr_index :
(** write the edge [ref\[index\]--> obj] *)
val write_deref :
Location.t
PathContext.t
-> Location.t
-> ref:AbstractValue.t * ValueHistory.t
-> obj:AbstractValue.t * ValueHistory.t
-> t
@ -185,7 +206,8 @@ val write_deref :
(** write the edge [ref --*--> obj] *)
val write_deref_biad_isl :
Location.t
PathContext.t
-> Location.t
-> ref:AbstractValue.t * ValueHistory.t
-> AbstractValue.t HilExp.Access.t
-> obj:AbstractValue.t * ValueHistory.t
@ -204,7 +226,8 @@ type invalidation_access =
| UntraceableAccess (** we don't know where the value came from; avoid using if possible *)
val invalidate :
invalidation_access
PathContext.t
-> invalidation_access
-> Location.t
-> Invalidation.t
-> AbstractValue.t * ValueHistory.t
@ -213,7 +236,12 @@ val invalidate :
(** record that the address is invalid *)
val invalidate_biad_isl :
Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t list
PathContext.t
-> Location.t
-> Invalidation.t
-> AbstractValue.t * ValueHistory.t
-> t
-> t AccessResult.t list
(** record that the address is invalid. If the address has not been allocated, abduce ISL specs for
both invalid (null, free, unint) and allocated heap. *)
@ -224,7 +252,8 @@ val add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t
val remove_allocation_attr : AbstractValue.t -> t -> t
val invalidate_access :
Location.t
PathContext.t
-> Location.t
-> Invalidation.t
-> AbstractValue.t * ValueHistory.t
-> BaseMemory.Access.t
@ -233,7 +262,8 @@ val invalidate_access :
(** record that what the address points via the access to is invalid *)
val invalidate_deref_access :
Location.t
PathContext.t
-> Location.t
-> Invalidation.t
-> AbstractValue.t * ValueHistory.t
-> BaseMemory.Access.t
@ -242,11 +272,17 @@ val invalidate_deref_access :
(** Like [invalidate_access] but invalidates dereferenced address. *)
val invalidate_array_elements :
Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t
PathContext.t
-> Location.t
-> Invalidation.t
-> AbstractValue.t * ValueHistory.t
-> t
-> t AccessResult.t
(** record that all the array elements that address points to is invalid *)
val shallow_copy :
Location.t
PathContext.t
-> Location.t
-> AbstractValue.t * ValueHistory.t
-> t
-> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t
@ -262,7 +298,8 @@ val check_address_escape :
Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t AccessResult.t
val get_captured_actuals :
Location.t
PathContext.t
-> Location.t
-> captured_vars:(Var.t * CapturedVar.capture_mode * Typ.t) list
-> actual_closure:AbstractValue.t * ValueHistory.t
-> t

24
infer/src/pulse/PulsePathContext.ml
Unescape View File

@ -0,0 +1,24 @@
(*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
module F = Format
type timestamp = int [@@deriving compare]
let t0 = 0
type t = {timestamp: timestamp}
(** path contexts is metadata that do not contribute to the semantics *)
let leq ~lhs:_ ~rhs:_ = true
let pp fmt ({timestamp}[@warning "+9"]) = F.fprintf fmt "timestamp= %d" timestamp
let initial = {timestamp= 0}
let post_exec_instr {timestamp} = {timestamp= timestamp + 1}

24
infer/src/pulse/PulsePathContext.mli
Unescape View File

@ -0,0 +1,24 @@
(*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
module F = Format
type timestamp = private int [@@deriving compare]
val t0 : timestamp
type t = {timestamp: timestamp (** step number *)}
val leq : lhs:t -> rhs:t -> bool
val initial : t
val post_exec_instr : t -> t
(** call this after each step of the symbolic execution to update the path information *)
val pp : F.formatter -> t -> unit

2
infer/tests/codetoanalyze/c/pulse/issues.exp
Unescape View File

@ -38,7 +38,7 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un
codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, report_correct_error_among_multiple_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `several_dereferences_ok` here,parameter `x` of several_dereferences_ok,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, report_correct_error_among_multiple_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `several_dereferences_ok` here,parameter `z` of several_dereferences_ok,invalid access occurs here]
codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `l` of access_use_after_free_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `l` of access_use_after_free_bad,invalid access occurs here]
codetoanalyze/c/pulse/traces.c, call_makes_null_deref_manifest_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `something_about_strings_latent`,null pointer dereference part of the trace starts here,in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]

3
infer/tests/codetoanalyze/c/pulse/nullptr.c
Unescape View File

@ -122,9 +122,12 @@ void null_alias_bad(int* x) {
*x = 42;
}
void dereference(int* p) { *p; }
void several_dereferences_ok(int* x, int* y, int* z) {
int* p = x;
*z = 52;
dereference(y);
*y = 42;
*x = 32;
*x = 777;

2
infer/tests/codetoanalyze/objc/pulse/issues.exp
Unescape View File

@ -13,6 +13,6 @@ codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.assignNilBad, 5, NIL_BLOCK_CALL,
codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.paramAssignNilBad:, 3, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.paramReassignNilBad:, 6, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,assigned,assigned,invalid access occurs here]
codetoanalyze/objc/pulse/NPENilBlocks.m, calldoSomethingThenCallbackWithNilBad, 2, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,when calling `BlockA.doSomethingThenCallback:` here,parameter `my_block` of BlockA.doSomethingThenCallback:,invalid access occurs here]
codetoanalyze/objc/pulse/uninit.m, Uninit.call_setter_c_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `x` created,when calling `Uninit.setS:` here,parameter `s` of Uninit.setS:,read to uninitialized value occurs here]
codetoanalyze/objc/pulse/uninit.m, Uninit.call_setter_c_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `y` created,when calling `Uninit.setS:` here,parameter `s` of Uninit.setS:,read to uninitialized value occurs here]
codetoanalyze/objc/pulse/use_after_free.m, PulseTest.use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of PulseTest.use_after_free_simple_in_objc_method_bad:,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of PulseTest.use_after_free_simple_in_objc_method_bad:,invalid access occurs here]
codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]

Write Preview
Loading…
Cancel
Save