From b1d371e54d590b5e996d06c9637440e6845febb5 Mon Sep 17 00:00:00 2001 From: Loc Le Date: Mon, 14 Dec 2020 07:23:39 -0800 Subject: [PATCH] Pulse with explicit Ok/Error summaries Reviewed By: jvillard Differential Revision: D25428280 fbshipit-source-id: c6faf58ea --- infer/man/man1/infer-full.txt | 5 +++++ infer/src/base/Config.ml | 24 ++++++++++++++++-------- infer/src/base/Config.mli | 6 ++++-- infer/src/checkers/impurity.ml | 2 +- infer/src/pulse/Pulse.ml | 10 +++++----- infer/src/pulse/PulseExecutionDomain.ml | 14 ++++++++++++-- infer/src/pulse/PulseExecutionDomain.mli | 3 +++ infer/src/pulse/PulseOperations.ml | 8 +++++++- 8 files changed, 53 insertions(+), 19 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 2d3fec0e0..8efbb8fb5 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1767,6 +1767,11 @@ INTERNAL OPTIONS experimentations only. (Conversely: --no-pulse-intraprocedural-only) + --pulse-isl + Activates: [Pulse] Incorrectness Separation Logic (ISL) mode: + explicit Ok/Error summaries are recorded. For experiments only. + (Conversely: --no-pulse-isl) + --pulse-max-disjuncts int Under-approximate after int disjunctions in the domain diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 925d7f39f..78447ad45 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1865,17 +1865,17 @@ and pulse_cut_to_one_path_procedures_pattern = large procedures to prevent too-big states from being produced." -and pulse_recency_limit = - CLOpt.mk_int ~long:"pulse-recency-limit" ~default:32 - "Maximum number of array elements and structure fields to keep track of for a given array \ - address." - - and pulse_intraprocedural_only = CLOpt.mk_bool ~long:"pulse-intraprocedural-only" "Disable inter-procedural analysis in Pulse. Used for experimentations only." +and pulse_isl = + CLOpt.mk_bool ~long:"pulse-isl" ~default:false + "[Pulse] Incorrectness Separation Logic (ISL) mode: explicit Ok/Error summaries are recorded. \ + For experiments only." + + and pulse_max_disjuncts = CLOpt.mk_int ~long:"pulse-max-disjuncts" ~default:20 "Under-approximate after $(i,int) disjunctions in the domain" @@ -1918,6 +1918,12 @@ and pulse_model_transfer_ownership = are method or namespace::method" +and pulse_recency_limit = + CLOpt.mk_int ~long:"pulse-recency-limit" ~default:32 + "Maximum number of array elements and structure fields to keep track of for a given array \ + address." + + and pulse_report_latent_issues = CLOpt.mk_bool ~long:"pulse-report-latent-issues" "Only use for testing, there should be no need to turn this on for regular code analysis. \ @@ -3098,10 +3104,10 @@ and pulse_cut_to_one_path_procedures_pattern = Option.map ~f:Str.regexp !pulse_cut_to_one_path_procedures_pattern -and pulse_recency_limit = !pulse_recency_limit - and pulse_intraprocedural_only = !pulse_intraprocedural_only +and pulse_isl = !pulse_isl + and pulse_max_disjuncts = !pulse_max_disjuncts and pulse_model_abort = !pulse_model_abort @@ -3135,6 +3141,8 @@ and pulse_model_transfer_ownership_namespace, pulse_model_transfer_ownership = List.partition_map ~f:aux models +and pulse_recency_limit = !pulse_recency_limit + and pulse_report_latent_issues = !pulse_report_latent_issues and pulse_widen_threshold = !pulse_widen_threshold diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index b5056ee74..29b6c72d7 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -461,10 +461,10 @@ val project_root : string val pulse_cut_to_one_path_procedures_pattern : Str.regexp option -val pulse_recency_limit : int - val pulse_intraprocedural_only : bool +val pulse_isl : bool [@@warning "-32"] + val pulse_max_disjuncts : int val pulse_model_abort : string list @@ -483,6 +483,8 @@ val pulse_model_transfer_ownership : string list val pulse_report_latent_issues : bool +val pulse_recency_limit : int + val pulse_widen_threshold : int val pure_by_default : bool diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 2aad81d8c..e4d0a3ea5 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -165,7 +165,7 @@ let extract_impurity tenv pname formals (exec_state : ExecutionDomain.t) : Impur ((astate :> AbductiveDomain.t), true) | ContinueProgram astate -> (astate, false) - | AbortProgram astate | LatentAbortProgram {astate} -> + | ISLLatentMemoryError astate | AbortProgram astate | LatentAbortProgram {astate} -> ((astate :> AbductiveDomain.t), false) in let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index f05c3bcc8..af242c1f0 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -105,7 +105,7 @@ module PulseTransferFunctions = struct (* invalidate [&x] *) PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate >>| ExecutionDomain.continue - | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> + | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> Ok exec_state @@ -123,7 +123,7 @@ module PulseTransferFunctions = struct match exec_state with | ContinueProgram astate -> ContinueProgram (do_astate astate) - | AbortProgram _ | LatentAbortProgram _ | ExitProgram _ -> + | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ | ExitProgram _ -> exec_state in Result.map ~f:(List.map ~f:do_one_exec_state) exec_state_res @@ -254,7 +254,7 @@ module PulseTransferFunctions = struct ~f:(fun astates (astate : Domain.t) -> let astate = match astate with - | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> + | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> [astate] | ContinueProgram astate -> dispatch_call analysis_data ret call_exp actuals location call_flags astate @@ -278,7 +278,7 @@ module PulseTransferFunctions = struct let exec_instr_aux (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data) _cfg_node (instr : Sil.instr) : Domain.t list = match astate with - | AbortProgram _ | LatentAbortProgram _ -> + | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ -> (* We can also continue the analysis with the error state here but there might be a risk we would get nonsense. *) [astate] @@ -335,7 +335,7 @@ module PulseTransferFunctions = struct List.fold ~f:(fun astates (astate : Domain.t) -> match astate with - | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> + | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> [astate] | ContinueProgram astate -> let astate = diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 30cc11dde..43d261729 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -21,6 +21,7 @@ type 'abductive_domain_t base_t = | ExitProgram of AbductiveDomain.summary | AbortProgram of AbductiveDomain.summary | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} + | ISLLatentMemoryError of AbductiveDomain.summary [@@deriving yojson_of] type t = AbductiveDomain.t base_t @@ -31,7 +32,9 @@ let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc) let leq ~lhs ~rhs = match (lhs, rhs) with - | AbortProgram astate1, AbortProgram astate2 | ExitProgram astate1, ExitProgram astate2 -> + | AbortProgram astate1, AbortProgram astate2 + | ISLLatentMemoryError astate1, ISLLatentMemoryError astate2 + | ExitProgram astate1, ExitProgram astate2 -> AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) | ContinueProgram astate1, ContinueProgram astate2 -> AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2 @@ -46,6 +49,8 @@ let leq ~lhs ~rhs = let pp fmt = function | ContinueProgram astate -> AbductiveDomain.pp fmt astate + | ISLLatentMemoryError astate -> + F.fprintf fmt "{ISLLatentMemoryError %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) | ExitProgram astate -> F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) | AbortProgram astate -> @@ -64,7 +69,10 @@ let pp fmt = function let get_astate : t -> AbductiveDomain.t = function | ContinueProgram astate -> astate - | ExitProgram astate | AbortProgram astate | LatentAbortProgram {astate} -> + | ISLLatentMemoryError astate + | ExitProgram astate + | AbortProgram astate + | LatentAbortProgram {astate} -> (astate :> AbductiveDomain.t) @@ -83,6 +91,8 @@ let summary_of_posts_common ~continue_program pdesc posts = | Sat astate -> Some (continue_program astate) ) (* already a summary but need to reconstruct the variants to make the type system happy *) + | ISLLatentMemoryError astate -> + Some (ISLLatentMemoryError astate) | AbortProgram astate -> Some (AbortProgram astate) | ExitProgram astate -> diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index e6c2bf4d7..197632cb9 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -17,6 +17,9 @@ type 'abductive_domain_t base_t = (** represents the state at the program point that caused an error *) | 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 *) + | ISLLatentMemoryError of AbductiveDomain.summary + (** represents the state at the program point that might cause an error; used for + {!Config.pulse_isl} *) type t = AbductiveDomain.t base_t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 91ccaeae7..3282066e0 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -487,12 +487,18 @@ let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret match callee_exec_state with | ContinueProgram astate -> map_call_result astate ~f:(fun astate -> Sat (Ok (ContinueProgram astate))) - | AbortProgram astate | ExitProgram astate | LatentAbortProgram {astate} -> + | ISLLatentMemoryError astate + | AbortProgram astate + | ExitProgram astate + | LatentAbortProgram {astate} -> map_call_result (astate :> AbductiveDomain.t) ~f:(fun astate -> let+ astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in match callee_exec_state with + | ISLLatentMemoryError _ -> + (* TODO: check invalid of inter-procedural analysis *) + Ok (ISLLatentMemoryError astate_summary) | ContinueProgram _ -> assert false | AbortProgram _ ->