From f61425db2990f1454d163a0a82da4970d4fd1103 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 6 Jul 2021 09:30:58 -0700 Subject: [PATCH] [pulse] refactor initial state creation Summary: The creation of the inital state has evolved several times recently, time for a refactor: - do not create then pass the initial state around when callees can create it instead - slightly hackish assertions that creating the initial state conditions cannot fail to simplify the types (could eventually be moved in AbductiveDomain.ml to avoid breaking abstraction layers like this, but trivial enough that it doesn't really matter I think) Reviewed By: skcho Differential Revision: D29550319 fbshipit-source-id: 63919ae71 --- infer/src/pulse/Pulse.ml | 20 +++---- infer/src/pulse/PulseCallOperations.ml | 3 +- infer/src/pulse/PulseExecutionDomain.ml | 2 - infer/src/pulse/PulseExecutionDomain.mli | 2 - infer/src/pulse/PulseObjectiveCSummary.ml | 63 +++++++++------------- infer/src/pulse/PulseObjectiveCSummary.mli | 18 ++----- infer/src/pulse/PulseReport.mli | 16 +++--- 7 files changed, 48 insertions(+), 76 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 124ca61f0..f78f2a081 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -471,25 +471,25 @@ let with_debug_exit_node proc_desc ~f = ~f +let initial tenv proc_desc = + [ ( ContinueProgram (PulseObjectiveCSummary.mk_initial_with_positive_self tenv proc_desc) + , PathContext.initial ) ] + + 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_self_positive = - PulseObjectiveCSummary.append_objc_self_positive analysis_data initial_astate - in - let initial = List.map ~f:(fun initial -> (initial, PathContext.initial)) initial_self_positive in - match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with + match + DisjunctiveAnalyzer.compute_post analysis_data ~initial:(initial tenv proc_desc) proc_desc + with | Some posts -> (* forget path contexts, we don't propagate them across functions *) let posts = List.map ~f:fst posts in with_debug_exit_node proc_desc ~f:(fun () -> - let updated_posts = - PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts - in + let objc_nil_summary = PulseObjectiveCSummary.mk_nil_messaging_summary tenv proc_desc in let summary = PulseSummary.of_posts tenv proc_desc err_log (Procdesc.get_exit_node proc_desc |> Procdesc.Node.get_loc) - updated_posts + (Option.to_list objc_nil_summary @ posts) in report_topl_errors proc_desc err_log summary ; Some summary ) diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index 492ff0ff6..2afd5d8c9 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -285,8 +285,7 @@ let call tenv path ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary. astate_unknown in let result_unknown_nil = - PulseObjectiveCSummary.mk_objc_method_nil_summary tenv procdesc - (ExecutionDomain.mk_initial tenv procdesc) + PulseObjectiveCSummary.mk_nil_messaging_summary tenv procdesc |> Option.value_map ~default:[] ~f:(fun nil_summary -> call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals procdesc [nil_summary] astate ) diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index d6f3f7311..efca0d127 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -32,8 +32,6 @@ type t = AbductiveDomain.t base_t let continue astate = ContinueProgram astate -let mk_initial tenv pdesc = ContinueProgram (AbductiveDomain.mk_initial tenv pdesc) - let leq ~lhs ~rhs = phys_equal lhs rhs || diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index 9c65f584b..d159674da 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -35,8 +35,6 @@ include AbstractDomain.Disjunct with type t := t val continue : AbductiveDomain.t -> t -val mk_initial : Tenv.t -> Procdesc.t -> t - val is_unsat_cheap : t -> bool (** see {!PulsePathCondition.is_unsat_cheap} *) diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index 47925b56b..2c29460a4 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -38,10 +38,11 @@ let init_fields_zero tenv path location ~zero addr typ astate = (** Constructs summary [{self = 0} {return = self}] when [proc_desc] returns a POD type. This allows us to connect invalidation with invalid access in the trace *) -let mk_objc_method_nil_summary_aux tenv proc_desc astate = +let mk_nil_messaging_summary_aux tenv proc_desc = let path = PathContext.initial in let location = Procdesc.get_loc proc_desc in let self = mk_objc_self_pvar proc_desc in + let astate = AbductiveDomain.mk_initial tenv proc_desc in (* HACK: we are operating on an "empty" initial state and do not expect to create any alarms (nothing is Invalid in the initial state) or unsatisfiability (we won't create arithmetic contradictions) *) @@ -71,12 +72,13 @@ let mk_objc_method_nil_summary_aux tenv proc_desc astate = |> assert_ok -let mk_objc_latent_non_POD_nil_messaging tenv proc_desc astate = - (* same HACK as above *) - let assert_ok = function Ok x -> x | Error _ -> assert false in +let mk_latent_non_POD_nil_messaging tenv proc_desc = let path = PathContext.initial in let location = Procdesc.get_loc proc_desc in let self = mk_objc_self_pvar proc_desc in + let astate = AbductiveDomain.mk_initial tenv proc_desc in + (* same HACK as above *) + let assert_ok = function Ok x -> x | Error _ -> assert false in let astate, (self_value, _self_history) = PulseOperations.eval_deref path location (Lvar self) astate |> assert_ok in @@ -94,50 +96,41 @@ let mk_objc_latent_non_POD_nil_messaging tenv proc_desc astate = ; calling_context= [] } -let mk_objc_method_nil_summary tenv proc_desc initial = +let mk_nil_messaging_summary tenv proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in - match (initial, proc_name) with - | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} -> + match proc_name with + | Procname.ObjC_Cpp {kind= ObjCInstanceMethod} -> if Procdesc.is_ret_type_pod proc_desc then (* In ObjC, when a method is called on nil, there is no NPE, the method is actually not called and the return value is 0/false/nil. We create a nil summary to avoid reporting NPE in this case. However, there is an exception in the case where the return type is non-POD. In that case it's UB and we want to report an error. *) - let astate = mk_objc_method_nil_summary_aux tenv proc_desc astate in + let astate = mk_nil_messaging_summary_aux tenv proc_desc in Some (ContinueProgram astate) else - let summary = mk_objc_latent_non_POD_nil_messaging tenv proc_desc astate in + let summary = mk_latent_non_POD_nil_messaging tenv proc_desc in Some summary - | ContinueProgram _, _ - | ExitProgram _, _ - | AbortProgram _, _ - | LatentAbortProgram _, _ - | LatentInvalidAccess _, _ - | ISLLatentMemoryError _, _ -> + | _ -> None -let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} astate = +let mk_initial_with_positive_self tenv proc_desc = 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 - match (astate, proc_name) with - | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} -> - let result = - let* astate, value = - PulseOperations.eval_deref PathContext.initial location (Lvar self) astate - in - PulseArithmetic.and_positive (fst value) astate + let initial_astate = AbductiveDomain.mk_initial tenv proc_desc in + (* same HACK as above *) + let assert_ok = function Ok x -> x | Error _ -> assert false in + match proc_name with + | Procname.ObjC_Cpp {kind= ObjCInstanceMethod} -> + let astate, value = + PulseOperations.eval_deref PathContext.initial location (Lvar self) initial_astate + |> assert_ok in - PulseReport.report_result tenv proc_desc err_log location result - | ContinueProgram _, _ - | ExitProgram _, _ - | AbortProgram _, _ - | LatentAbortProgram _, _ - | LatentInvalidAccess _, _ - | ISLLatentMemoryError _, _ -> - [astate] + PulseArithmetic.and_positive (fst value) astate |> assert_ok + | _ -> + initial_astate let append_objc_actual_self_positive procdesc self_actual astate = @@ -148,11 +141,3 @@ let append_objc_actual_self_positive procdesc self_actual astate = PulseArithmetic.prune_positive self astate ) | _ -> Ok astate - - -let update_objc_method_posts {InterproceduralAnalysis.tenv; proc_desc} ~initial_astate ~posts = - match mk_objc_method_nil_summary tenv proc_desc initial_astate with - | None -> - posts - | Some nil_summary -> - nil_summary :: posts diff --git a/infer/src/pulse/PulseObjectiveCSummary.mli b/infer/src/pulse/PulseObjectiveCSummary.mli index 3dd55787a..b94968feb 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.mli +++ b/infer/src/pulse/PulseObjectiveCSummary.mli @@ -9,24 +9,14 @@ open! IStd open PulseBasicInterface open PulseDomainInterface -val update_objc_method_posts : - PulseSummary.t InterproceduralAnalysis.t - -> initial_astate:ExecutionDomain.t - -> posts:ExecutionDomain.t list - -> ExecutionDomain.t list -(** For ObjC instance methods: appends additional nil summary and replaces must be valid reason for - non-pod return type. Does nothing to posts for other kinds of methods *) - val append_objc_actual_self_positive : Procdesc.t -> ((AbstractValue.t * ValueHistory.t) * Typ.t) option -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t -val append_objc_self_positive : - PulseSummary.t InterproceduralAnalysis.t -> ExecutionDomain.t -> ExecutionDomain.t list -(** For ObjC instance methods: adds path condition `self > 0` to a given post. Does nothing to posts - for other kinds of methods *) +val mk_initial_with_positive_self : Tenv.t -> Procdesc.t -> AbductiveDomain.t +(** The initial state of the analysis, with the additional path condition [self > 0] for Objective-C + instance methods. *) -val mk_objc_method_nil_summary : - Tenv.t -> Procdesc.t -> ExecutionDomain.t -> ExecutionDomain.t option +val mk_nil_messaging_summary : Tenv.t -> Procdesc.t -> ExecutionDomain.t option diff --git a/infer/src/pulse/PulseReport.mli b/infer/src/pulse/PulseReport.mli index c7d0b3b1d..34fd94395 100644 --- a/infer/src/pulse/PulseReport.mli +++ b/infer/src/pulse/PulseReport.mli @@ -8,13 +8,7 @@ open! IStd open PulseDomainInterface -val report_result : - Tenv.t - -> Procdesc.t - -> Errlog.t - -> Location.t - -> AbductiveDomain.t AccessResult.t - -> ExecutionDomain.t list +[@@@warning "-32"] val report_summary_error : Tenv.t @@ -23,6 +17,14 @@ val report_summary_error : -> AbductiveDomain.summary AccessResult.error -> _ ExecutionDomain.base_t +val report_result : + Tenv.t + -> Procdesc.t + -> Errlog.t + -> Location.t + -> AbductiveDomain.t AccessResult.t + -> ExecutionDomain.t list + val report_results : Tenv.t -> Procdesc.t