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

@@ -315,24 +315,50 @@ module PulseTransferFunctions = struct
             let* astate, (rhs_addr, rhs_history) =
               PulseOperations.eval NoAccess loc rhs_exp astate
             in
+            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
-            let* astate =
+                Ok (false, [(astate, lhs_addr_hist)])
+            in
+            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.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
+                [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]
+                    astate :: acc )
             | _ ->
-                Ok [astate]
+                Ok astates
           in
           report_on_error analysis_data result
       | Prune (condition, loc, _is_then_branch, _if_kind) ->

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
 

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 *)