From 92341d8ffc17538558ee7be3730137c60e7a45b2 Mon Sep 17 00:00:00 2001 From: Loc Le Date: Fri, 8 Jan 2021 02:02:38 -0800 Subject: [PATCH] isl summary for memory store Summary: This diff is to generate ISL summaries for memory write. Reviewed By: jvillard Differential Revision: D25769320 fbshipit-source-id: 7d7a54c60 --- infer/src/pulse/Pulse.ml | 52 +++++++++++++++++++++-------- infer/src/pulse/PulseOperations.ml | 18 ++++++++++ infer/src/pulse/PulseOperations.mli | 17 ++++++++++ 3 files changed, 74 insertions(+), 13 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 51d8f2b62..2864e6c82 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -315,24 +315,50 @@ module PulseTransferFunctions = struct let* astate, (rhs_addr, rhs_history) = PulseOperations.eval NoAccess loc rhs_exp astate in - let* astate, lhs_addr_hist = PulseOperations.eval Write loc lhs_exp astate in - let* astate = - PulseOperations.write_deref loc ~ref:lhs_addr_hist - ~obj:(rhs_addr, event :: rhs_history) - astate - in - let astate = - if Topl.is_deep_active () then topl_store_step loc ~lhs:lhs_exp ~rhs:rhs_exp astate - else astate + let* is_structured, ls_astate_lhs_addr_hist = + if Config.pulse_isl then PulseOperations.eval_structure_isl Write loc lhs_exp astate + else + let* astate, lhs_addr_hist = PulseOperations.eval Write loc lhs_exp astate in + Ok (false, [(astate, lhs_addr_hist)]) in - match lhs_exp with - | Lvar pvar when Pvar.is_return pvar -> + let write_function lhs_addr_hist astate = + if is_structured then + PulseOperations.write_deref_biad_isl loc ~ref:lhs_addr_hist Dereference + ~obj:(rhs_addr, event :: rhs_history) + astate + else let+ astate = - PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate + PulseOperations.write_deref loc ~ref:lhs_addr_hist + ~obj:(rhs_addr, event :: rhs_history) + astate in [astate] + in + let* astates = + List.fold_result ls_astate_lhs_addr_hist ~init:[] + ~f:(fun acc_astates (astate, lhs_addr_hist) -> + match (Config.pulse_isl, astate.AbductiveDomain.isl_status) with + | false, _ | true, ISLOk -> + let+ astates = write_function lhs_addr_hist astate in + List.rev_append astates acc_astates + | true, ISLError -> + Ok (astate :: acc_astates) ) + in + let astates = + if Topl.is_deep_active () then + List.map astates ~f:(fun astate -> + topl_store_step loc ~lhs:lhs_exp ~rhs:rhs_exp astate ) + else astates + in + match lhs_exp with + | Lvar pvar when Pvar.is_return pvar -> + List.fold_result astates ~init:[] ~f:(fun acc astate -> + let+ astate = + PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate + in + astate :: acc ) | _ -> - Ok [astate] + Ok astates in report_on_error analysis_data result | Prune (condition, loc, _is_then_branch, _if_kind) -> diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 308966147..ad1002c06 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -320,10 +320,28 @@ let write_access location addr_trace_ref access addr_trace_obj 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 + List.fold_result astates ~init:[] ~f:(fun acc ast -> + let astate = + match ast.AbductiveDomain.isl_status with + | ISLOk -> + Memory.add_edge addr_trace_ref access addr_trace_obj location ast + | ISLError -> + ast + in + Ok (astate :: acc) ) + + 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_biad_isl 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 + + 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 diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 667931ed2..ab6fde32d 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -38,6 +38,15 @@ val eval : Return an error state if it traverses some known invalid address or if the end destination is known to be invalid. *) +val eval_structure_isl : + access_mode + -> Location.t + -> Exp.t + -> t + -> (bool * (t * (AbstractValue.t * ValueHistory.t)) list) access_result +(** 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 access_result val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result @@ -96,6 +105,14 @@ val write_deref : -> t access_result (** write the edge [ref --*--> obj] *) +val write_deref_biad_isl : + Location.t + -> ref:AbstractValue.t * ValueHistory.t + -> AbstractValue.t HilExp.Access.t + -> obj:AbstractValue.t * ValueHistory.t + -> t + -> t list access_result + val invalidate : Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result (** record that the address is invalid *)