diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 2c0922292..4484febd6 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -467,7 +467,7 @@ val pulse_cut_to_one_path_procedures_pattern : Str.regexp option val pulse_intraprocedural_only : bool -val pulse_isl : bool [@@warning "-32"] +val pulse_isl : bool val pulse_max_disjuncts : int diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index e4d0a3ea5..f4e38415b 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -163,9 +163,9 @@ let extract_impurity tenv pname formals (exec_state : ExecutionDomain.t) : Impur match exec_state with | ExitProgram astate -> ((astate :> AbductiveDomain.t), true) - | ContinueProgram astate -> + | ContinueProgram astate | ISLLatentMemoryError astate -> (astate, false) - | ISLLatentMemoryError astate | AbortProgram astate | LatentAbortProgram {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 8055db11d..51d8f2b62 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -24,7 +24,7 @@ let exec_list_of_list_result = function let report_on_error {InterproceduralAnalysis.proc_desc; err_log} result = PulseReport.report_error proc_desc err_log result - >>| (fun post -> [ExecutionDomain.ContinueProgram post]) + >>| List.map ~f:(fun post -> ExecutionDomain.ContinueProgram post) |> exec_list_of_list_result @@ -285,13 +285,27 @@ module PulseTransferFunctions = struct | ExitProgram _ -> (* program already exited, simply propagate the exited state upwards *) [astate] - | ContinueProgram astate -> ( + | ContinueProgram ({isl_status= ISLError} as astate) -> ( + match instr with + | Prune (_, _, is_then_branch, _) when is_then_branch -> + [] + | _ -> + [ContinueProgram astate] ) + | ContinueProgram ({isl_status= ISLOk} as astate) -> ( match instr with | Load {id= lhs_id; e= rhs_exp; loc} -> (* [lhs_id := *rhs_exp] *) let result = - let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in - PulseOperations.write_id lhs_id rhs_addr_hist astate + let+ astate_rhs_addr_hists = + if Config.pulse_isl then + let+ astate_rhs_addr_hists = PulseOperations.eval_deref_isl loc rhs_exp astate in + astate_rhs_addr_hists + else + let+ astate_rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in + [astate_rhs_addr_hist] + in + List.map astate_rhs_addr_hists ~f:(fun (astate, rhs_addr_hist) -> + PulseOperations.write_id lhs_id rhs_addr_hist astate ) in report_on_error analysis_data result | Store {e1= lhs_exp; e2= rhs_exp; loc} -> @@ -313,9 +327,12 @@ module PulseTransferFunctions = struct in match lhs_exp with | Lvar pvar when Pvar.is_return pvar -> - PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate + let+ astate = + PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate + in + [astate] | _ -> - Ok astate + Ok [astate] in report_on_error analysis_data result | Prune (condition, loc, _is_then_branch, _if_kind) -> @@ -339,7 +356,11 @@ module PulseTransferFunctions = struct astate :: astates | ContinueProgram astate -> let astate = - PulseOperations.remove_vars vars location astate + ( match PulseOperations.remove_vars vars location astate with + | Ok astate -> + Ok [astate] + | Error _ as error -> + error ) |> report_on_error analysis_data in List.rev_append astate astates ) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index b24179b17..0e3cf477c 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -86,24 +86,40 @@ end (** represents the inferred pre-condition at each program point, biabduction style *) module PreDomain : BaseDomainSig = PostDomain +module PostStatus = struct + type t = ISLOk | ISLError [@@deriving equal] + + let pp f s = + match s with + | ISLOk -> + F.pp_print_string f "ISLOk:" + | ISLError -> + F.pp_print_string f "ISLError:" +end + (** biabduction-style pre/post state + skipped calls *) type t = { post: PostDomain.t (** state at the current program point*) ; pre: PreDomain.t (** inferred pre at the current program point *) ; topl: (PulseTopl.state[@yojson.opaque]) ; skipped_calls: SkippedCalls.t (** set of skipped calls *) - ; path_condition: PathCondition.t } + ; path_condition: PathCondition.t + ; isl_status: (PostStatus.t[@yojson.opaque]) } [@@deriving yojson_of] -let pp f {post; pre; topl; path_condition; skipped_calls} = - F.fprintf f "@[%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp path_condition - PostDomain.pp post PreDomain.pp pre SkippedCalls.pp skipped_calls PulseTopl.pp_state topl +let pp f {post; pre; topl; path_condition; skipped_calls; isl_status} = + F.fprintf f "@[%a@;%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp + path_condition PostStatus.pp isl_status PostDomain.pp post PreDomain.pp pre SkippedCalls.pp + skipped_calls PulseTopl.pp_state topl +let set_isl_error_status astate = {astate with isl_status= PostStatus.ISLError} + let set_path_condition path_condition astate = {astate with path_condition} let leq ~lhs ~rhs = SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls + && PostStatus.equal lhs.isl_status rhs.isl_status && match BaseDomain.isograph_map BaseDomain.empty_mapping @@ -154,7 +170,8 @@ module Stack = struct ; pre ; topl= astate.topl ; skipped_calls= astate.skipped_calls - ; path_condition= astate.path_condition } + ; path_condition= astate.path_condition + ; isl_status= astate.isl_status } , addr_hist ) @@ -271,6 +288,53 @@ module AddressAttributes = struct let find_opt address astate = BaseAddressAttributes.find_opt address (astate.post :> base_domain).attrs + + + let check_valid_isl 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 -> ( + match + BaseAddressAttributes.get_must_be_valid_or_allocated_isl addr + (astate.post :> BaseDomain.t).attrs + with + | None -> + let is_eq_null = PathCondition.is_known_zero astate.path_condition addr in + let null_astates = + if PathCondition.is_known_neq_zero astate.path_condition addr then [] + else + let null_attr = + Attribute.Invalid (Invalidation.ConstantDereference IntLit.zero, access_trace) + in + let null_astate = + {astate with isl_status= (if null_noop then astate.isl_status else ISLError)} + |> add_one addr null_attr + in + let null_astate = + if is_eq_null then null_astate else abduce_attribute addr null_attr null_astate + in + [null_astate] + in + if is_eq_null then Ok null_astates + else + let valid_astate = + let abdalloc = Attribute.ISLAbduced access_trace in + let valid_attr = Attribute.MustBeValid access_trace in + add_one addr abdalloc astate |> abduce_attribute addr valid_attr + |> abduce_attribute addr abdalloc + in + let invalid_free = + (*C or Cpp?*) + let invalid_attr = Attribute.Invalid (CFree, access_trace) in + {astate with isl_status= ISLError} + |> abduce_attribute addr invalid_attr + |> add_one addr invalid_attr + in + Ok ([valid_astate; invalid_free] @ null_astates) + | Some _ -> + Ok [astate] ) + | Some (invalidation, invalidation_trace) -> + Error (invalidation, invalidation_trace, {astate with isl_status= ISLError}) end module Memory = struct @@ -314,7 +378,8 @@ module Memory = struct ; pre= PreDomain.update astate.pre ~heap:foot_heap ; topl= astate.topl ; skipped_calls= astate.skipped_calls - ; path_condition= astate.path_condition } + ; path_condition= astate.path_condition + ; isl_status= astate.isl_status } , addr_hist_dst ) @@ -361,31 +426,58 @@ let mk_initial proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in let location = Procdesc.get_loc proc_desc in let formals_and_captured = - let init_var mangled = + let init_var mangled typ = let pvar = Pvar.mk mangled proc_name in - (Var.of_pvar pvar, (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)])) + ( Var.of_pvar pvar + , typ + , (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) ) in let formals = - Procdesc.get_formals proc_desc |> List.map ~f:(fun (mangled, _) -> init_var mangled) + Procdesc.get_formals proc_desc |> List.map ~f:(fun (mangled, typ) -> init_var mangled typ) in let captured = - Procdesc.get_captured proc_desc |> List.map ~f:(fun {CapturedVar.name} -> init_var name) + Procdesc.get_captured proc_desc + |> List.map ~f:(fun {CapturedVar.name; CapturedVar.typ} -> init_var name typ) in captured @ formals in let initial_stack = List.fold formals_and_captured ~init:(PreDomain.empty :> BaseDomain.t).stack - ~f:(fun stack (formal, addr_loc) -> BaseStack.add formal addr_loc stack) + ~f:(fun stack (formal, _, addr_loc) -> BaseStack.add formal addr_loc stack) in - let pre = - let initial_heap = - List.fold formals_and_captured ~init:(PreDomain.empty :> base_domain).heap - ~f:(fun heap (_, (addr, _)) -> BaseMemory.register_address addr heap) + let initial_heap = + let register heap (_, _, (addr, _)) = BaseMemory.register_address addr heap in + let isl_register_and_add_edge heap ((_, typ, (addr, _)) as arg) = + let heap = register heap arg in + match typ.Typ.desc with + | Typ.Tptr _ -> + let addr_dst = AbstractValue.mk_fresh () in + BaseMemory.add_edge addr Dereference (addr_dst, []) heap + |> BaseMemory.register_address addr_dst + | _ -> + heap in - PreDomain.update ~stack:initial_stack ~heap:initial_heap PreDomain.empty + List.fold formals_and_captured ~init:(PreDomain.empty :> base_domain).heap + ~f:(if Config.pulse_isl then isl_register_and_add_edge else register) + in + let initial_attrs = + if Config.pulse_isl then + List.fold formals_and_captured ~init:(PreDomain.empty :> base_domain).attrs + ~f:(fun attrs (_, _, (addr, _)) -> + BaseAddressAttributes.add_one addr (MustBeValid (Immediate {location; history= []})) attrs ) + else (PreDomain.empty :> base_domain).attrs + in + let pre = + PreDomain.update ~stack:initial_stack ~heap:initial_heap ~attrs:initial_attrs PreDomain.empty in let locals = Procdesc.get_locals proc_desc in - let post = PostDomain.update ~stack:initial_stack PostDomain.empty in + let initial_heap, initial_attrs = + if Config.pulse_isl then (initial_heap, initial_attrs) + else ((PreDomain.empty :> base_domain).heap, (PreDomain.empty :> base_domain).attrs) + in + let post = + PostDomain.update ~stack:initial_stack ~heap:initial_heap ~attrs:initial_attrs PostDomain.empty + in let post = List.fold locals ~init:post ~f:(fun (acc : PostDomain.t) {ProcAttributes.name; typ} -> set_uninitialized_post (`LocalDecl (Pvar.mk name proc_name, None)) typ location acc ) @@ -394,7 +486,8 @@ let mk_initial proc_desc = ; post ; topl= PulseTopl.start () ; skipped_calls= SkippedCalls.empty - ; path_condition= PathCondition.true_ } + ; path_condition= PathCondition.true_ + ; isl_status= ISLOk } let add_skipped_call pname trace astate = @@ -435,7 +528,10 @@ let discard_unreachable ({pre; post} as astate) = let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var) -let set_post_edges addr edges astate = Memory.map_post_heap astate ~f:(BaseMemory.add addr edges) +let set_post_edges addr edges astate = + if BaseMemory.Edges.is_empty edges then astate + else Memory.map_post_heap astate ~f:(BaseMemory.add addr edges) + (* {3 Helper functions to traverse the two maps at once } *) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 6ac589593..582bb0dba 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -52,18 +52,25 @@ module PostDomain : BaseDomainSig collapse into one. * *) module PreDomain : BaseDomainSig +module PostStatus : sig + type t = ISLOk | ISLError [@@deriving equal] +end + (** biabduction-style pre/post state + skipped calls *) type t = private { post: PostDomain.t (** state at the current program point*) ; pre: PreDomain.t (** inferred pre at the current program point *) ; topl: PulseTopl.state (** state at of the Topl monitor at the current program point *) ; skipped_calls: SkippedCalls.t (** set of skipped calls *) - ; path_condition: PathCondition.t (** arithmetic facts *) } + ; path_condition: PathCondition.t (** arithmetic facts *) + ; isl_status: PostStatus.t (** isl summary status *) } val leq : lhs:t -> rhs:t -> bool val pp : Format.formatter -> t -> unit +val set_isl_error_status : t -> t + val mk_initial : Procdesc.t -> t val get_pre : t -> BaseDomain.t @@ -147,6 +154,13 @@ module AddressAttributes : sig val std_vector_reserve : AbstractValue.t -> t -> t val find_opt : AbstractValue.t -> t -> Attributes.t option + + val check_valid_isl : + Trace.t + -> AbstractValue.t + -> ?null_noop:bool + -> t + -> (t list, Invalidation.t * Trace.t * t) result end val is_local : Var.t -> t -> bool diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 537f8dc73..5eb2aa1f4 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -32,6 +32,7 @@ module Attribute = struct | DynamicType of Typ.Name.t | EndOfCollection | Invalid of Invalidation.t * Trace.t + | ISLAbduced of Trace.t | MustBeInitialized of Trace.t | MustBeValid of Trace.t | StdVectorReserve @@ -72,6 +73,8 @@ module Attribute = struct let end_of_collection_rank = Variants.to_rank EndOfCollection + let isl_abduced_rank = Variants.to_rank (ISLAbduced dummy_trace) + let uninitialized_rank = Variants.to_rank Uninitialized let must_be_initialized_rank = Variants.to_rank (MustBeInitialized dummy_trace) @@ -100,6 +103,8 @@ module Attribute = struct F.fprintf f "Invalid %a" (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation)) trace + | ISLAbduced trace -> + F.fprintf f "ISLAbduced %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "ISLAbduced")) trace | MustBeInitialized trace -> F.fprintf f "MustBeInitialized %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "read")) @@ -174,6 +179,13 @@ module Attributes = struct (procname, trace) ) + let get_isl_abduced attrs = + Set.find_rank attrs Attribute.isl_abduced_rank + |> Option.map ~f:(fun attr -> + let[@warning "-8"] (Attribute.ISLAbduced trace) = attr in + trace ) + + let get_dynamic_type attrs = Set.find_rank attrs Attribute.dynamic_type_rank |> Option.map ~f:(fun attr -> @@ -196,13 +208,13 @@ include Attribute let is_suitable_for_pre = function | MustBeValid _ | MustBeInitialized _ -> true + | Invalid _ | Allocated _ | ISLAbduced _ -> + Config.pulse_isl | AddressOfCppTemporary _ | AddressOfStackVariable _ - | Allocated _ | Closure _ | DynamicType _ | EndOfCollection - | Invalid _ | StdVectorReserve | Uninitialized | WrittenTo _ -> @@ -212,6 +224,8 @@ let is_suitable_for_pre = function let map_trace ~f = function | Allocated (procname, trace) -> Allocated (procname, f trace) + | ISLAbduced trace -> + ISLAbduced (f trace) | Invalid (invalidation, trace) -> Invalid (invalidation, f trace) | MustBeValid trace -> diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 8a7fb4aef..9a3faebc1 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -19,6 +19,7 @@ type t = | DynamicType of Typ.Name.t | EndOfCollection | 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 | StdVectorReserve @@ -48,6 +49,8 @@ module Attributes : sig val get_invalid : t -> (Invalidation.t * Trace.t) option + val get_isl_abduced : t -> Trace.t option + val get_must_be_valid : t -> Trace.t option val get_written_to : t -> Trace.t option diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 0f9b713be..f983af7ab 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -112,8 +112,22 @@ let initialize address attrs = let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name +let get_invalid = get_attribute Attributes.get_invalid + let get_must_be_valid = get_attribute Attributes.get_must_be_valid +let get_must_be_valid_or_allocated_isl address attrs = + match get_must_be_valid address attrs with + | Some trace -> + Some trace + | None -> ( + match get_attribute Attributes.get_allocation address attrs with + | Some (_, trace) -> + Some trace + | None -> + get_attribute Attributes.get_isl_abduced address attrs ) + + let get_must_be_initialized = get_attribute Attributes.get_must_be_initialized let std_vector_reserve address memory = add_one address Attribute.StdVectorReserve memory diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 7a44e4728..4d09930da 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -37,8 +37,12 @@ val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location. 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 option +val get_must_be_valid_or_allocated_isl : AbstractValue.t -> t -> Trace.t option + val get_must_be_initialized : AbstractValue.t -> t -> Trace.t option val std_vector_reserve : AbstractValue.t -> t -> t diff --git a/infer/src/pulse/PulseCItv.ml b/infer/src/pulse/PulseCItv.ml index b04f5fa65..a61db360b 100644 --- a/infer/src/pulse/PulseCItv.ml +++ b/infer/src/pulse/PulseCItv.ml @@ -174,6 +174,13 @@ let is_equal_to_zero = function false +let is_not_equal_to_zero = function + | Outside (l, u) -> + IntLit.iszero l && IntLit.iszero u + | _ -> + false + + let as_int = function Between (Int l, Int u) when IntLit.eq l u -> IntLit.to_int l | _ -> None let has_empty_intersection a1 a2 = diff --git a/infer/src/pulse/PulseCItv.mli b/infer/src/pulse/PulseCItv.mli index 3a52ed98c..e74401aa1 100644 --- a/infer/src/pulse/PulseCItv.mli +++ b/infer/src/pulse/PulseCItv.mli @@ -15,6 +15,9 @@ val equal_to : IntLit.t -> t val is_equal_to_zero : t -> bool +val is_not_equal_to_zero : t -> bool +(** whether this is literally [≠0] *) + val as_int : t -> int option (** [as_int v] returns [Some x] if [v] is known to be [x] *) diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 43d261729..d2433988f 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -21,7 +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 + | ISLLatentMemoryError of 'abductive_domain_t [@@deriving yojson_of] type t = AbductiveDomain.t base_t @@ -32,11 +32,10 @@ let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc) let leq ~lhs ~rhs = match (lhs, rhs) with - | AbortProgram astate1, AbortProgram astate2 - | ISLLatentMemoryError astate1, ISLLatentMemoryError astate2 - | ExitProgram astate1, ExitProgram astate2 -> + | AbortProgram astate1, AbortProgram astate2 | ExitProgram astate1, ExitProgram astate2 -> AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) - | ContinueProgram astate1, ContinueProgram astate2 -> + | ContinueProgram astate1, ContinueProgram astate2 + | ISLLatentMemoryError astate1, ISLLatentMemoryError astate2 -> AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2 | ( LatentAbortProgram {astate= astate1; latent_issue= issue1} , LatentAbortProgram {astate= astate2; latent_issue= issue2} ) -> @@ -50,7 +49,7 @@ let pp fmt = function | ContinueProgram astate -> AbductiveDomain.pp fmt astate | ISLLatentMemoryError astate -> - F.fprintf fmt "{ISLLatentMemoryError %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) + F.fprintf fmt "{ISLLatentMemoryError %a}" AbductiveDomain.pp astate | ExitProgram astate -> F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) | AbortProgram astate -> @@ -67,12 +66,9 @@ let pp fmt = function (* 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 *) let get_astate : t -> AbductiveDomain.t = function - | ContinueProgram astate -> + | ContinueProgram astate | ISLLatentMemoryError astate -> astate - | ISLLatentMemoryError astate - | ExitProgram astate - | AbortProgram astate - | LatentAbortProgram {astate} -> + | ExitProgram astate | AbortProgram astate | LatentAbortProgram {astate} -> (astate :> AbductiveDomain.t) @@ -84,15 +80,13 @@ let summary_of_posts_common ~continue_program pdesc posts = List.filter_mapi posts ~f:(fun i exec_state -> L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ; match exec_state with - | ContinueProgram astate -> ( + | ContinueProgram astate | ISLLatentMemoryError astate -> ( match AbductiveDomain.summary_of_post pdesc astate with | Unsat -> None | 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 -> @@ -102,7 +96,12 @@ let summary_of_posts_common ~continue_program pdesc posts = let summary_of_posts = - summary_of_posts_common ~continue_program:(fun astate -> ContinueProgram astate) + summary_of_posts_common ~continue_program:(fun astate -> + match (astate :> AbductiveDomain.t).isl_status with + | ISLOk -> + ContinueProgram astate + | ISLError -> + ISLLatentMemoryError astate ) let force_exit_program = diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index 197632cb9..33ba700dc 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -17,7 +17,7 @@ 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 + | ISLLatentMemoryError of 'abductive_domain_t (** represents the state at the program point that might cause an error; used for {!Config.pulse_isl} *) diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 3282066e0..308966147 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -36,6 +36,38 @@ let check_addr_access access_mode location (address, history) astate = Ok astate +let check_and_abduce_addr_access_isl access_mode location (address, history) ?(null_noop = false) + astate = + let access_trace = Trace.Immediate {location; history} in + let* astates = + AddressAttributes.check_valid_isl access_trace address ~null_noop astate + |> Result.map_error ~f:(fun (invalidation, invalidation_trace, astate) -> + ( Diagnostic.AccessToInvalidAddress + {calling_context= []; invalidation; invalidation_trace; access_trace} + , astate ) ) + in + match access_mode with + | Read -> + List.fold_result astates ~init:[] ~f:(fun astates astate -> + match AddressAttributes.check_initialized access_trace address astate with + | Error _ -> + Error + ( Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace} + , AbductiveDomain.set_isl_error_status astate ) + | Ok ok_astate -> + Ok (ok_astate :: astates) ) + | Write -> + Ok + (List.map astates ~f:(fun astate -> + match astate.AbductiveDomain.isl_status with + | ISLOk -> + AbductiveDomain.initialize address astate + | ISLError -> + astate )) + | NoAccess -> + Ok astates + + module Closures = struct module Memory = AbductiveDomain.Memory @@ -115,6 +147,21 @@ let eval_access mode location addr_hist access astate = Memory.eval_edge addr_hist access astate +let eval_access_biad_isl mode location addr_hist access astate = + let map_ok addr_hist access astates = + List.map + ~f:(fun astate -> + match astate.AbductiveDomain.isl_status with + | ISLOk -> + Memory.eval_edge addr_hist access astate + | ISLError -> + (astate, addr_hist) ) + astates + in + let+ astates = check_and_abduce_addr_access_isl mode location addr_hist astate in + map_ok addr_hist access astates + + let eval mode location exp0 astate = let rec eval mode exp astate = match (exp : Exp.t) with @@ -196,6 +243,61 @@ let eval_deref location exp astate = Memory.eval_edge addr_hist Dereference astate +let eval_structure_isl 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 (HilExp.Access.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+ astates = + eval_access_biad_isl mode loc addr_hist + (HilExp.Access.ArrayAccess (StdTyp.void, fst addr_hist_index)) + astate + in + (false, astates) + | _ -> + let+ astate, (addr, history) = eval mode loc exp astate in + (true, [(astate, (addr, history))]) + + +let eval_deref_biad_isl location access addr_hist astate = + let+ astates = check_and_abduce_addr_access_isl Read location addr_hist astate in + List.map + ~f:(fun astate -> + match astate.AbductiveDomain.isl_status with + | ISLOk -> + Memory.eval_edge addr_hist access astate + | ISLError -> + (astate, addr_hist) ) + astates + + +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_function (astate, addr_hist) = + if is_structured then eval_deref_biad_isl location Dereference addr_hist astate + else + let+ astate = eval_deref location exp astate in + [astate] + in + List.fold ls_astate_addr_hist ~init:(Ok []) ~f:(fun acc ((astate, _) as astate_addr) -> + match acc with + | Ok acc_astates -> ( + match astate.AbductiveDomain.isl_status with + | ISLOk -> + let+ astates = eval_deref_function astate_addr in + acc_astates @ astates + | ISLError -> + Ok (acc_astates @ [astate_addr]) ) + | Error _ as a -> + a ) + + let realloc_pvar pvar typ location astate = let addr = AbstractValue.mk_fresh () in let astate = @@ -487,19 +589,15 @@ 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))) - | ISLLatentMemoryError astate - | AbortProgram astate - | ExitProgram astate - | LatentAbortProgram {astate} -> + | ISLLatentMemoryError astate -> + map_call_result astate ~f:(fun astate -> Sat (Ok (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 _ -> + | ContinueProgram _ | ISLLatentMemoryError _ -> assert false | AbortProgram _ -> Ok (AbortProgram astate_summary) diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 181883fa3..667931ed2 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -43,6 +43,9 @@ val prune : Location.t -> condition:Exp.t -> t -> t access_result val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result (** Like [eval] but evaluates [*exp]. *) +val eval_deref_isl : + Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) list access_result + val eval_access : access_mode -> Location.t diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index 6011a349c..71e04ca7b 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -401,6 +401,10 @@ let is_known_zero phi v = || Formula.is_known_zero phi.formula v +let is_known_neq_zero phi v = + CItvs.find_opt v phi.citvs |> Option.exists ~f:CItv.is_not_equal_to_zero + + let is_unsat_cheap phi = phi.is_unsat let is_unsat_expensive phi = diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index b070564ea..37c147ca4 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/infer/src/pulse/PulsePathCondition.mli @@ -62,6 +62,11 @@ val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> t * new_ val is_known_zero : t -> AbstractValue.t -> bool (** [is_known_zero phi t] returns [true] if [phi |- t = 0], [false] if we don't know for sure *) +val is_known_neq_zero : t -> AbstractValue.t -> bool +(** [is_known_neq_zero phi t] returns [true] if [phi |- t != 0], [false] if we don't know for sure *) + +(* this only consults the concrete intervals domain for now *) + val is_unsat_cheap : t -> bool (** whether the state contains a contradiction, call this as often as you want *)