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

[pulse] change ISLOk/ISLError inside states into actual Ok/Error outside states

Browse Source 
Summary:
This changes the results. I think it's because we cut short paths to
ISL errors sooner now, before they are duplicated and moved. I could not
really assess what was going on though so could be wrong.

On OpenSSL 1.0.2d:
Before: 106 issues
After:   90 issues

Reviewed By: ezgicicek

Differential Revision: D26822331

fbshipit-source-id: e861e7fc2
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent 3aaa28f993
commit 341c08d9fd
15 changed files with 148 additions and 194 deletions
Show Stats Download Patch File Download Diff File

4
infer/src/checkers/impurity.ml
Unescape View File

@ -164,9 +164,9 @@ let extract_impurity tenv pname formals (exec_state : ExecutionDomain.t) : Impur
match exec_state with match exec_state with
| ExitProgram astate -> | ExitProgram astate ->
((astate :> AbductiveDomain.t), true) ((astate :> AbductiveDomain.t), true)
| ContinueProgram astate | ISLLatentMemoryError astate -> | ContinueProgram astate ->
(astate, false) (astate, false)
| AbortProgram astate | LatentAbortProgram {astate} -> | AbortProgram astate | LatentAbortProgram {astate} | ISLLatentMemoryError astate ->
((astate :> AbductiveDomain.t), false) ((astate :> AbductiveDomain.t), false)
in in
let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in

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

@ -268,13 +268,7 @@ module PulseTransferFunctions = struct
| ExitProgram _ -> | ExitProgram _ ->
(* program already exited, simply propagate the exited state upwards *) (* program already exited, simply propagate the exited state upwards *)
[astate] [astate]
| ContinueProgram ({isl_status= ISLError} as astate) -> ( | ContinueProgram astate -> (
match instr with
| Prune (_, _, is_then_branch, _) when is_then_branch ->
[]
| _ ->
[ContinueProgram astate] )
| ContinueProgram ({isl_status= ISLOk} as astate) -> (
match instr with match instr with
| Load {id= lhs_id; e= rhs_exp; loc} -> | Load {id= lhs_id; e= rhs_exp; loc} ->
(* [lhs_id := *rhs_exp] *) (* [lhs_id := *rhs_exp] *)
@ -315,11 +309,7 @@ module PulseTransferFunctions = struct
let astates = let astates =
List.concat_map ls_astate_lhs_addr_hist ~f:(fun result -> List.concat_map ls_astate_lhs_addr_hist ~f:(fun result ->
let<*> astate, lhs_addr_hist = result in let<*> astate, lhs_addr_hist = result in
match (Config.pulse_isl, astate.AbductiveDomain.isl_status) with write_function lhs_addr_hist astate )
| false, _ | true, ISLOk ->
write_function lhs_addr_hist astate
| true, ISLError ->
[Ok astate] )
in in
let astates = let astates =
if Topl.is_deep_active () then if Topl.is_deep_active () then

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

@ -89,42 +89,25 @@ end
(** represents the inferred pre-condition at each program point, biabduction style *) (** represents the inferred pre-condition at each program point, biabduction style *)
module PreDomain : BaseDomainSig = PostDomain module PreDomain : BaseDomainSig = PostDomain
type isl_status = ISLOk | ISLError [@@deriving compare, equal, yojson_of]
let pp_isl_status f s =
if Config.pulse_isl then
match s with
| ISLOk ->
F.pp_print_string f "ISLOk:"
| ISLError ->
F.pp_print_string f "ISLError:"
else ()
(* see documentation in this file's .mli *) (* see documentation in this file's .mli *)
type t = type t =
{ post: PostDomain.t { post: PostDomain.t
; pre: PreDomain.t ; pre: PreDomain.t
; path_condition: PathCondition.t ; path_condition: PathCondition.t
; topl: (PulseTopl.state[@yojson.opaque]) ; topl: (PulseTopl.state[@yojson.opaque])
; skipped_calls: SkippedCalls.t ; skipped_calls: SkippedCalls.t }
; isl_status: isl_status }
[@@deriving compare, equal, yojson_of] [@@deriving compare, equal, yojson_of]
let pp f {post; pre; topl; path_condition; skipped_calls; isl_status} = let pp f {post; pre; topl; path_condition; skipped_calls} =
F.fprintf f "@[<v>%a@;%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp F.fprintf f "@[<v>%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp path_condition
path_condition pp_isl_status isl_status PostDomain.pp post PreDomain.pp pre SkippedCalls.pp PostDomain.pp post PreDomain.pp pre SkippedCalls.pp skipped_calls PulseTopl.pp_state topl
skipped_calls PulseTopl.pp_state topl
let set_isl_status status astate = {astate with isl_status= status}
let set_path_condition path_condition astate = {astate with path_condition} let set_path_condition path_condition astate = {astate with path_condition}
let leq ~lhs ~rhs = let leq ~lhs ~rhs =
phys_equal lhs rhs phys_equal lhs rhs
|| SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls || SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls
&& ((not Config.pulse_isl) || equal_isl_status lhs.isl_status rhs.isl_status)
&& PathCondition.equal lhs.path_condition rhs.path_condition && PathCondition.equal lhs.path_condition rhs.path_condition
&& &&
match match
@ -198,8 +181,7 @@ module Stack = struct
; pre ; pre
; topl= astate.topl ; topl= astate.topl
; skipped_calls= astate.skipped_calls ; skipped_calls= astate.skipped_calls
; path_condition= astate.path_condition ; path_condition= astate.path_condition }
; isl_status= astate.isl_status }
, addr_hist ) , addr_hist )
@ -379,16 +361,13 @@ module AddressAttributes = struct
let null_attr = let null_attr =
Attribute.Invalid (Invalidation.ConstantDereference IntLit.zero, access_trace) Attribute.Invalid (Invalidation.ConstantDereference IntLit.zero, access_trace)
in in
let null_astate = let null_astate = add_one addr null_attr astate in
{astate with isl_status= (if null_noop then astate.isl_status else ISLError)}
|> add_one addr null_attr
in
let null_astate = let null_astate =
if is_eq_null then null_astate else abduce_attribute addr null_attr null_astate if is_eq_null then null_astate else abduce_attribute addr null_attr null_astate
in in
[null_astate] if null_noop then [Ok null_astate] else [Error (`ISLError null_astate)]
in in
if is_eq_null then Ok null_astates if is_eq_null then null_astates
else else
let valid_astate = let valid_astate =
let abdalloc = Attribute.ISLAbduced access_trace in let abdalloc = Attribute.ISLAbduced access_trace in
@ -399,15 +378,13 @@ module AddressAttributes = struct
let invalid_free = let invalid_free =
(*C or Cpp?*) (*C or Cpp?*)
let invalid_attr = Attribute.Invalid (CFree, access_trace) in let invalid_attr = Attribute.Invalid (CFree, access_trace) in
{astate with isl_status= ISLError} abduce_attribute addr invalid_attr astate |> add_one addr invalid_attr
|> abduce_attribute addr invalid_attr
|> add_one addr invalid_attr
in in
Ok ([valid_astate; invalid_free] @ null_astates) Ok valid_astate :: Error (`ISLError invalid_free) :: null_astates
| Some _ -> | Some _ ->
Ok [astate] ) [Ok astate] )
| Some (invalidation, invalidation_trace) -> | Some (invalidation, invalidation_trace) ->
Error (invalidation, invalidation_trace, {astate with isl_status= ISLError}) [Error (`InvalidAccess (invalidation, invalidation_trace, astate))]
end end
module Memory = struct module Memory = struct
@ -451,8 +428,7 @@ module Memory = struct
; pre= PreDomain.update astate.pre ~heap:foot_heap ; pre= PreDomain.update astate.pre ~heap:foot_heap
; topl= astate.topl ; topl= astate.topl
; skipped_calls= astate.skipped_calls ; skipped_calls= astate.skipped_calls
; path_condition= astate.path_condition ; path_condition= astate.path_condition }
; isl_status= astate.isl_status }
, addr_hist_dst ) , addr_hist_dst )
@ -587,8 +563,7 @@ let mk_initial tenv proc_desc =
; post ; post
; topl= PulseTopl.start () ; topl= PulseTopl.start ()
; skipped_calls= SkippedCalls.empty ; skipped_calls= SkippedCalls.empty
; path_condition= PathCondition.true_ ; path_condition= PathCondition.true_ }
; isl_status= ISLOk }
let add_skipped_call pname trace astate = let add_skipped_call pname trace astate =

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

@ -54,16 +54,6 @@ module PostDomain : BaseDomainSig
collapse into one. * *) collapse into one. * *)
module PreDomain : BaseDomainSig module PreDomain : BaseDomainSig
(** Execution status, similar to {!PulseExecutionDomain} but for ISL (Incorrectness Separation
Logic) mode, where {!PulseExecutionDomain.ContinueProgram} can also contain "error specs" that
describe what happens when some addresses are invalid explicitly instead of relying on
[MustBeValid] attributes. *)
type isl_status =
| ISLOk (** ok triple: the program executes without error *)
| ISLError
(** Error specification: an invalid address recorded in the precondition will cause an error *)
[@@deriving equal]
(** pre/post on a single program path *) (** pre/post on a single program path *)
type t = private type t = private
{ post: PostDomain.t (** state at the current program point*) { post: PostDomain.t (** state at the current program point*)
@ -74,15 +64,13 @@ type t = private
; topl: PulseTopl.state ; topl: PulseTopl.state
(** state at of the Topl monitor at the current program point, when Topl is enabled *) (** state at of the Topl monitor at the current program point, when Topl is enabled *)
; skipped_calls: SkippedCalls.t (** metadata: procedure calls for which no summary was found *) ; skipped_calls: SkippedCalls.t (** metadata: procedure calls for which no summary was found *)
; isl_status: isl_status } }
[@@deriving equal] [@@deriving equal]
val leq : lhs:t -> rhs:t -> bool val leq : lhs:t -> rhs:t -> bool
val pp : Format.formatter -> t -> unit val pp : Format.formatter -> t -> unit
val set_isl_status : isl_status -> t -> t
val mk_initial : Tenv.t -> Procdesc.t -> t val mk_initial : Tenv.t -> Procdesc.t -> t
val get_pre : t -> BaseDomain.t val get_pre : t -> BaseDomain.t
@ -176,7 +164,7 @@ module AddressAttributes : sig
-> AbstractValue.t -> AbstractValue.t
-> ?null_noop:bool -> ?null_noop:bool
-> t -> t
-> (t list, Invalidation.t * Trace.t * t) result -> (t, [> `ISLError of t | `InvalidAccess of Invalidation.t * Trace.t * t]) result list
end end
val is_local : Var.t -> t -> bool val is_local : Var.t -> t -> bool

7
infer/src/pulse/PulseAccessResult.ml
Unescape View File

@ -9,7 +9,9 @@ open! IStd
open PulseBasicInterface open PulseBasicInterface
module AbductiveDomain = PulseAbductiveDomain module AbductiveDomain = PulseAbductiveDomain
type 'astate error = ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} type 'astate error =
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ISLError of 'astate
type ('a, 'astate) base_t = ('a, 'astate error) result type ('a, 'astate) base_t = ('a, 'astate error) result
@ -21,3 +23,6 @@ let to_summary tenv proc_desc error =
| ReportableError {astate; diagnostic} -> | ReportableError {astate; diagnostic} ->
let+ astate = AbductiveDomain.summary_of_post tenv proc_desc astate in let+ astate = AbductiveDomain.summary_of_post tenv proc_desc astate in
ReportableError {astate; diagnostic} ReportableError {astate; diagnostic}
| ISLError astate ->
let+ astate = AbductiveDomain.summary_of_post tenv proc_desc astate in
ISLError astate

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

@ -9,7 +9,9 @@ open! IStd
open PulseBasicInterface open PulseBasicInterface
module AbductiveDomain = PulseAbductiveDomain module AbductiveDomain = PulseAbductiveDomain
type 'astate error = ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} type 'astate error =
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ISLError of 'astate
type ('a, 'astate) base_t = ('a, 'astate error) result type ('a, 'astate) base_t = ('a, 'astate error) result

28
infer/src/pulse/PulseExecutionDomain.ml
Unescape View File

@ -21,7 +21,7 @@ type 'abductive_domain_t base_t =
| ExitProgram of AbductiveDomain.summary | ExitProgram of AbductiveDomain.summary
| AbortProgram of AbductiveDomain.summary | AbortProgram of AbductiveDomain.summary
| LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
| ISLLatentMemoryError of 'abductive_domain_t | ISLLatentMemoryError of AbductiveDomain.summary
[@@deriving equal, compare, yojson_of] [@@deriving equal, compare, yojson_of]
type t = AbductiveDomain.t base_t type t = AbductiveDomain.t base_t
@ -34,10 +34,11 @@ let leq ~lhs ~rhs =
phys_equal lhs rhs phys_equal lhs rhs
|| ||
match (lhs, rhs) with match (lhs, rhs) with
| AbortProgram astate1, AbortProgram astate2 | ExitProgram astate1, ExitProgram astate2 -> | AbortProgram astate1, AbortProgram astate2
AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) | ExitProgram astate1, ExitProgram astate2
| ContinueProgram astate1, ContinueProgram astate2
| ISLLatentMemoryError astate1, ISLLatentMemoryError astate2 -> | ISLLatentMemoryError astate1, ISLLatentMemoryError astate2 ->
AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t)
| ContinueProgram astate1, ContinueProgram astate2 ->
AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2 AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
| ( LatentAbortProgram {astate= astate1; latent_issue= issue1} | ( LatentAbortProgram {astate= astate1; latent_issue= issue1}
, LatentAbortProgram {astate= astate2; latent_issue= issue2} ) -> , LatentAbortProgram {astate= astate2; latent_issue= issue2} ) ->
@ -51,7 +52,7 @@ let pp fmt = function
| ContinueProgram astate -> | ContinueProgram astate ->
AbductiveDomain.pp fmt astate AbductiveDomain.pp fmt astate
| ISLLatentMemoryError astate -> | ISLLatentMemoryError astate ->
F.fprintf fmt "{ISLLatentMemoryError %a}" AbductiveDomain.pp astate F.fprintf fmt "{ISLLatentMemoryError %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t)
| ExitProgram astate -> | ExitProgram astate ->
F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t)
| AbortProgram astate -> | AbortProgram astate ->
@ -68,9 +69,12 @@ let pp fmt = function
(* do not export this function as there lies wickedness: clients should generally care about what (* do not export this function as there lies wickedness: clients should generally care about what
kind of state they are manipulating so let's not encourage them not to *) kind of state they are manipulating so let's not encourage them not to *)
let get_astate : t -> AbductiveDomain.t = function let get_astate : t -> AbductiveDomain.t = function
| ContinueProgram astate | ISLLatentMemoryError astate -> | ContinueProgram astate ->
astate astate
| ExitProgram astate | AbortProgram astate | LatentAbortProgram {astate} -> | ExitProgram astate
| AbortProgram astate
| LatentAbortProgram {astate}
| ISLLatentMemoryError astate ->
(astate :> AbductiveDomain.t) (astate :> AbductiveDomain.t)
@ -79,7 +83,7 @@ let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_st
type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of] type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of]
let summary_of_post_common tenv ~continue_program proc_desc = function let summary_of_post_common tenv ~continue_program proc_desc = function
| ContinueProgram astate | ISLLatentMemoryError astate -> ( | ContinueProgram astate -> (
match AbductiveDomain.summary_of_post tenv proc_desc astate with match AbductiveDomain.summary_of_post tenv proc_desc astate with
| Unsat -> | Unsat ->
None None
@ -92,17 +96,15 @@ let summary_of_post_common tenv ~continue_program proc_desc = function
Some (ExitProgram astate) Some (ExitProgram astate)
| LatentAbortProgram {astate; latent_issue} -> | LatentAbortProgram {astate; latent_issue} ->
Some (LatentAbortProgram {astate; latent_issue}) Some (LatentAbortProgram {astate; latent_issue})
| ISLLatentMemoryError astate ->
Some (ISLLatentMemoryError astate)
let summary_of_posts tenv proc_desc posts = let summary_of_posts tenv proc_desc posts =
List.filter_mapi posts ~f:(fun i exec_state -> List.filter_mapi posts ~f:(fun i exec_state ->
L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ; L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
summary_of_post_common tenv proc_desc exec_state ~continue_program:(fun astate -> summary_of_post_common tenv proc_desc exec_state ~continue_program:(fun astate ->
match (astate :> AbductiveDomain.t).isl_status with ContinueProgram astate ) )
| ISLOk ->
ContinueProgram astate
| ISLError ->
ISLLatentMemoryError astate ) )
let force_exit_program tenv proc_desc post = let force_exit_program tenv proc_desc post =

2
infer/src/pulse/PulseExecutionDomain.mli
Unescape View File

@ -17,7 +17,7 @@ type 'abductive_domain_t base_t =
(** represents the state at the program point that caused an error *) (** represents the state at the program point that caused an error *)
| LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
(** this path leads to an error but we don't have conclusive enough data to report it yet *) (** this path leads to an error but we don't have conclusive enough data to report it yet *)
| ISLLatentMemoryError of 'abductive_domain_t | ISLLatentMemoryError of AbductiveDomain.summary
(** represents the state at the program point that might cause an error; used for (** represents the state at the program point that might cause an error; used for
{!Config.pulse_isl} *) {!Config.pulse_isl} *)

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

@ -637,43 +637,39 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call
let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location
{AbductiveDomain.pre; _} pre_astate astate = {AbductiveDomain.pre; _} pre_astate astate =
match astate.AbductiveDomain.isl_status with AbstractValue.Map.fold
| ISLOk -> (fun addr_pre (addr_caller, hist_caller) astate_result ->
Ok astate let mk_access_trace callee_access_trace =
| ISLError -> Trace.ViaCall
AbstractValue.Map.fold { in_call= callee_access_trace
(fun addr_pre (addr_caller, hist_caller) astate_result -> ; f= Call callee_proc_name
let mk_access_trace callee_access_trace = ; location= call_location
Trace.ViaCall ; history= hist_caller }
{ in_call= callee_access_trace in
; f= Call callee_proc_name match astate_result with
; location= call_location | Error _ ->
; history= hist_caller } astate_result
in | Ok astate -> (
match astate_result with match
| Error _ -> BaseAddressAttributes.get_invalid addr_caller
(pre_astate.AbductiveDomain.post :> BaseDomain.t).attrs
with
| None ->
astate_result
| Some (invalidation, invalidation_trace) -> (
match BaseAddressAttributes.get_invalid addr_pre (pre :> BaseDomain.t).attrs with
| None ->
astate_result astate_result
| Ok astate -> ( | Some (_, callee_access_trace) ->
match let access_trace = mk_access_trace callee_access_trace in
BaseAddressAttributes.get_invalid addr_caller L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
(pre_astate.AbductiveDomain.post :> BaseDomain.t).attrs Error
with (AccessResult.ReportableError
| None -> { diagnostic=
astate_result Diagnostic.AccessToInvalidAddress
| Some (invalidation, invalidation_trace) -> ( {calling_context= []; invalidation; invalidation_trace; access_trace}
match BaseAddressAttributes.get_invalid addr_pre (pre :> BaseDomain.t).attrs with ; astate }) ) ) )
| None -> invalid_addr_callers (Ok astate)
astate_result
| Some (_, callee_access_trace) ->
let access_trace = mk_access_trace callee_access_trace in
L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
Error
(AccessResult.ReportableError
{ diagnostic=
Diagnostic.AccessToInvalidAddress
{calling_context= []; invalidation; invalidation_trace; access_trace}
; astate= AbductiveDomain.set_isl_status ISLError astate }) ) ) )
invalid_addr_callers (Ok astate)
(* - read all the pre, assert validity of addresses and materializes *everything* (to throw stuff (* - read all the pre, assert validity of addresses and materializes *everything* (to throw stuff
@ -690,7 +686,7 @@ let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location
the noise that this will introduce since we don't care about values. For instance, if the pre the noise that this will introduce since we don't care about values. For instance, if the pre
is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is
to bake in some value analysis. *) to bake in some value analysis. *)
let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_prepost:pre_post
~captured_vars_with_actuals ~formals ~actuals astate = ~captured_vars_with_actuals ~formals ~actuals astate =
L.d_printfln "Applying pre/post for %a(%a):@\n%a" Procname.pp callee_proc_name 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 ; (Pp.seq ~sep:"," Var.pp) formals AbductiveDomain.pp pre_post ;
@ -718,10 +714,13 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post
L.d_printfln "Pre applied successfully. call_state=%a" pp_call_state call_state ; L.d_printfln "Pre applied successfully. call_state=%a" pp_call_state call_state ;
match match
let open IResult.Let_syntax in let open IResult.Let_syntax in
(* only call [check_all_valid] when ISL is not active: the ISL mode generates explicit error
specs (which we recognize here using [is_isl_error_prepost]) instead of relying on
[check_all_valid], whereas the "normal" mode encodes some error specs implicitly in the
ContinueProgram ok specs *)
let* astate = let* astate =
if Config.pulse_isl then if Config.pulse_isl then
Ok if is_isl_error_prepost then Error (AccessResult.ISLError astate) else Ok astate
(AbductiveDomain.set_isl_status pre_post.AbductiveDomain.isl_status call_state.astate)
else check_all_valid callee_proc_name call_location pre_post call_state else check_all_valid callee_proc_name call_location pre_post call_state
in in
(* reset [visited] *) (* reset [visited] *)
@ -741,7 +740,7 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post
else call_state.astate else call_state.astate
in in
let+ astate = let+ astate =
if Config.pulse_isl then if is_isl_error_prepost then
isl_check_all_invalid invalid_subst callee_proc_name call_location pre_post pre_astate isl_check_all_invalid invalid_subst callee_proc_name call_location pre_post pre_astate
astate astate
else Ok astate else Ok astate

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

@ -10,7 +10,8 @@ open PulseBasicInterface
open PulseDomainInterface open PulseDomainInterface
val apply_prepost : val apply_prepost :
Procname.t is_isl_error_prepost:bool
-> Procname.t
-> Location.t -> Location.t
-> callee_prepost:AbductiveDomain.t -> callee_prepost:AbductiveDomain.t
-> captured_vars_with_actuals:(Var.t * (AbstractValue.t * ValueHistory.t)) list -> captured_vars_with_actuals:(Var.t * (AbstractValue.t * ValueHistory.t)) list

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

@ -49,3 +49,5 @@ let should_report (access_error : AbductiveDomain.summary PulseAccessResult.erro
| ReadUninitializedValue latent -> | ReadUninitializedValue latent ->
if is_manifest astate then `ReportNow (astate, diagnostic) if is_manifest astate then `ReportNow (astate, diagnostic)
else `DelayReport (astate, ReadUninitializedValue latent) ) else `DelayReport (astate, ReadUninitializedValue latent) )
| ISLError astate ->
`ISLDelay astate

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

@ -23,6 +23,7 @@ val to_diagnostic : t -> Diagnostic.t
val should_report : val should_report :
AbductiveDomain.summary PulseAccessResult.error AbductiveDomain.summary PulseAccessResult.error
-> [> `DelayReport of AbductiveDomain.summary * t -> [> `DelayReport of AbductiveDomain.summary * t
| `ReportNow of AbductiveDomain.summary * Diagnostic.t ] | `ReportNow of AbductiveDomain.summary * Diagnostic.t
| `ISLDelay of AbductiveDomain.summary ]
val add_call : CallEvent.t * Location.t -> t -> t val add_call : CallEvent.t * Location.t -> t -> t

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

@ -20,10 +20,11 @@ module Import = struct
| ExitProgram of AbductiveDomain.summary | ExitProgram of AbductiveDomain.summary
| AbortProgram of AbductiveDomain.summary | AbortProgram of AbductiveDomain.summary
| LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
| ISLLatentMemoryError of 'abductive_domain_t | ISLLatentMemoryError of AbductiveDomain.summary
type 'astate base_error = 'astate AccessResult.error = type 'astate base_error = 'astate AccessResult.error =
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ISLError of 'astate
include IResult.Let_syntax include IResult.Let_syntax
@ -63,33 +64,31 @@ let check_addr_access access_mode location (address, history) astate =
let check_and_abduce_addr_access_isl access_mode location (address, history) ?(null_noop = false) let check_and_abduce_addr_access_isl access_mode location (address, history) ?(null_noop = false)
astate = astate =
let access_trace = Trace.Immediate {location; history} in let access_trace = Trace.Immediate {location; history} in
match AddressAttributes.check_valid_isl access_trace address ~null_noop astate with AddressAttributes.check_valid_isl access_trace address ~null_noop astate
| Error (invalidation, invalidation_trace, astate) -> |> List.map ~f:(function
[ Error | Error (`InvalidAccess (invalidation, invalidation_trace, astate)) ->
(ReportableError Error
{ diagnostic= (ReportableError
Diagnostic.AccessToInvalidAddress { diagnostic=
{calling_context= []; invalidation; invalidation_trace; access_trace} Diagnostic.AccessToInvalidAddress
; astate }) ] {calling_context= []; invalidation; invalidation_trace; access_trace}
| Ok astates -> ( ; astate })
match access_mode with | Error (`ISLError astate) ->
| Read -> Error (ISLError astate)
List.map astates ~f:(fun astate -> | Ok astate -> (
AddressAttributes.check_initialized access_trace address astate match access_mode with
|> Result.map_error ~f:(fun () -> | Read ->
ReportableError AddressAttributes.check_initialized access_trace address astate
{ diagnostic= |> Result.map_error ~f:(fun () ->
Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace} ReportableError
; astate= AbductiveDomain.set_isl_status ISLError astate } ) ) { diagnostic=
| Write -> Diagnostic.ReadUninitializedValue
List.map astates ~f:(fun astate -> {calling_context= []; trace= access_trace}
match astate.AbductiveDomain.isl_status with ; astate } )
| ISLOk -> | Write ->
Ok (AbductiveDomain.initialize address astate) Ok (AbductiveDomain.initialize address astate)
| ISLError -> | NoAccess ->
Ok astate ) Ok astate ) )
| NoAccess ->
List.map ~f:(fun astate -> Ok astate) astates )
module Closures = struct module Closures = struct
@ -175,11 +174,7 @@ let eval_access_biad_isl mode location addr_hist access astate =
let map_ok addr_hist access results = let map_ok addr_hist access results =
List.map results ~f:(fun result -> List.map results ~f:(fun result ->
let+ astate = result in let+ astate = result in
match astate.AbductiveDomain.isl_status with Memory.eval_edge addr_hist access astate )
| ISLOk ->
Memory.eval_edge addr_hist access astate
| ISLError ->
(astate, addr_hist) )
in in
let results = check_and_abduce_addr_access_isl mode location addr_hist astate in let results = check_and_abduce_addr_access_isl mode location addr_hist astate in
map_ok addr_hist access results map_ok addr_hist access results
@ -290,14 +285,10 @@ let eval_structure_isl mode loc exp astate =
let eval_deref_biad_isl location access addr_hist astate = let eval_deref_biad_isl location access addr_hist astate =
let astates = check_and_abduce_addr_access_isl Read location addr_hist astate in check_and_abduce_addr_access_isl Read location addr_hist astate
List.map astates ~f:(fun astate -> |> List.map ~f:(fun result ->
let+ astate = astate in let+ astate = result in
match astate.AbductiveDomain.isl_status with Memory.eval_edge addr_hist access astate )
| ISLOk ->
Memory.eval_edge addr_hist access astate
| ISLError ->
(astate, addr_hist) )
let eval_deref_isl location exp astate = let eval_deref_isl location exp astate =
@ -307,12 +298,8 @@ let eval_deref_isl location exp astate =
else [eval_deref location exp astate] else [eval_deref location exp astate]
in in
List.concat_map ls_astate_addr_hist ~f:(fun result -> List.concat_map ls_astate_addr_hist ~f:(fun result ->
let<*> ((astate, _) as astate_addr) = result in let<*> astate_addr = result in
match astate.AbductiveDomain.isl_status with eval_deref_function astate_addr )
| ISLOk ->
eval_deref_function astate_addr
| ISLError ->
[Ok astate_addr] )
let realloc_pvar tenv pvar typ location astate = let realloc_pvar tenv pvar typ location astate =
@ -338,14 +325,10 @@ let write_access location addr_trace_ref access addr_trace_obj astate =
let write_access_biad_isl location addr_trace_ref access addr_trace_obj astate = let write_access_biad_isl location addr_trace_ref access addr_trace_obj astate =
check_and_abduce_addr_access_isl Write location addr_trace_ref astate let astates = check_and_abduce_addr_access_isl Write location addr_trace_ref astate in
|> List.map ~f:(fun result -> List.map astates ~f:(fun result ->
let+ astate = result in let+ astate = result in
match astate.AbductiveDomain.isl_status with Memory.add_edge addr_trace_ref access addr_trace_obj location astate )
| ISLOk ->
Memory.add_edge addr_trace_ref access addr_trace_obj location astate
| ISLError ->
astate )
let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate = let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate =
@ -386,11 +369,7 @@ let invalidate_biad_isl location cause (address, history) astate =
check_and_abduce_addr_access_isl NoAccess location (address, history) ~null_noop:true astate check_and_abduce_addr_access_isl NoAccess location (address, history) ~null_noop:true astate
|> List.map ~f:(fun result -> |> List.map ~f:(fun result ->
let+ astate = result in let+ astate = result in
match astate.AbductiveDomain.isl_status with AddressAttributes.invalidate (address, history) cause location astate )
| ISLOk ->
AddressAttributes.invalidate (address, history) cause location astate
| ISLError ->
astate )
let invalidate_access location cause ref_addr_hist access astate = let invalidate_access location cause ref_addr_hist access astate =
@ -636,10 +615,10 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate =
let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
~captured_vars_with_actuals ~formals ~actuals astate = ~captured_vars_with_actuals ~formals ~actuals astate =
let map_call_result callee_prepost ~f = let map_call_result ~is_isl_error_prepost callee_prepost ~f =
match match
PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals PulseInterproc.apply_prepost ~is_isl_error_prepost callee_pname call_loc ~callee_prepost
~formals ~actuals astate ~captured_vars_with_actuals ~formals ~actuals astate
with with
| (Sat (Error _) | Unsat) as path_result -> | (Sat (Error _) | Unsat) as path_result ->
path_result path_result
@ -658,11 +637,10 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
let open SatUnsat.Import in let open SatUnsat.Import in
match callee_exec_state with match callee_exec_state with
| ContinueProgram astate -> | ContinueProgram astate ->
map_call_result astate ~f:(fun astate -> Sat (Ok (ContinueProgram astate))) map_call_result ~is_isl_error_prepost:false astate ~f:(fun astate ->
| ISLLatentMemoryError astate -> Sat (Ok (ContinueProgram astate)) )
map_call_result astate ~f:(fun astate -> Sat (Ok (ISLLatentMemoryError astate)))
| AbortProgram astate | ExitProgram astate | LatentAbortProgram {astate} -> | AbortProgram astate | ExitProgram astate | LatentAbortProgram {astate} ->
map_call_result map_call_result ~is_isl_error_prepost:false
(astate :> AbductiveDomain.t) (astate :> AbductiveDomain.t)
~f:(fun astate -> ~f:(fun astate ->
let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in
@ -685,7 +663,15 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
| `DelayReport (astate, latent_issue) -> | `DelayReport (astate, latent_issue) ->
Ok (LatentAbortProgram {astate; latent_issue}) Ok (LatentAbortProgram {astate; latent_issue})
| `ReportNow (astate, diagnostic) -> | `ReportNow (astate, diagnostic) ->
Error (ReportableError {diagnostic; astate= (astate :> AbductiveDomain.t)}) ) ) Error (ReportableError {diagnostic; astate= (astate :> AbductiveDomain.t)})
| `ISLDelay astate ->
Error (ISLError (astate :> AbductiveDomain.t)) ) )
| ISLLatentMemoryError astate ->
map_call_result ~is_isl_error_prepost:true
(astate :> AbductiveDomain.t)
~f:(fun astate ->
let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in
Ok (ISLLatentMemoryError astate_summary) )
let get_captured_actuals location ~captured_vars ~actual_closure astate = let get_captured_actuals location ~captured_vars ~actual_closure astate =

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

@ -27,10 +27,11 @@ module Import : sig
| ExitProgram of AbductiveDomain.summary | ExitProgram of AbductiveDomain.summary
| AbortProgram of AbductiveDomain.summary | AbortProgram of AbductiveDomain.summary
| LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
| ISLLatentMemoryError of 'abductive_domain_t | ISLLatentMemoryError of AbductiveDomain.summary
type 'astate base_error = 'astate AccessResult.error = type 'astate base_error = 'astate AccessResult.error =
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ISLError of 'astate
(** {2 Monadic syntax} *) (** {2 Monadic syntax} *)

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

@ -49,6 +49,8 @@ let report_error tenv proc_desc err_log access_error =
| `DelayReport (astate, latent_issue) -> | `DelayReport (astate, latent_issue) ->
if Config.pulse_report_latent_issues then report_latent_issue proc_desc err_log latent_issue ; if Config.pulse_report_latent_issues then report_latent_issue proc_desc err_log latent_issue ;
LatentAbortProgram {astate; latent_issue} LatentAbortProgram {astate; latent_issue}
| `ISLDelay astate ->
ISLLatentMemoryError astate
let report_exec_results {InterproceduralAnalysis.proc_desc; tenv; err_log} results = let report_exec_results {InterproceduralAnalysis.proc_desc; tenv; err_log} results =

Write Preview
Loading…
Cancel
Save