[pulse] explicit isl error specs for free/delete

Summary: explicit Ok/Error summaries: bi-abduction for free/delete

Reviewed By: jvillard

Differential Revision: D25847708

fbshipit-source-id: 20aa2c45b

infer/src/pulse/PulseModels.ml

@@ -128,8 +128,14 @@ module Misc = struct
       let invalidation =
         match operation with `Free -> Invalidation.CFree | `Delete -> Invalidation.CppDelete
       in
-      let+ astate = PulseOperations.invalidate location invalidation deleted_access astate in
+      if Config.pulse_isl then
-      [ExecutionDomain.ContinueProgram astate]
+        let+ astates =
+          PulseOperations.invalidate_biad_isl location invalidation deleted_access astate
+        in
+        List.map astates ~f:(fun astate -> ExecutionDomain.ContinueProgram astate)
+      else
+        let+ astate = PulseOperations.invalidate location invalidation deleted_access astate in
+        [ExecutionDomain.ContinueProgram astate]
 end
 
 module C = struct

infer/src/pulse/PulseOperations.ml

@@ -367,6 +367,20 @@ let invalidate location cause addr_trace astate =
   >>| AddressAttributes.invalidate addr_trace cause location
 
 
+let invalidate_biad_isl location cause (address, history) astate =
+  let+ astates =
+    check_and_abduce_addr_access_isl NoAccess location (address, history) ~null_noop:true astate
+  in
+  List.map
+    ~f:(fun astate ->
+      match astate.AbductiveDomain.isl_status with
+      | ISLOk ->
+          AddressAttributes.invalidate (address, history) cause location astate
+      | ISLError ->
+          astate )
+    astates
+
+
 let invalidate_access location cause ref_addr_hist access astate =
   let astate, (addr_obj, _) = Memory.eval_edge ref_addr_hist access astate in
   invalidate location cause (addr_obj, snd ref_addr_hist) astate

infer/src/pulse/PulseOperations.mli

@@ -117,6 +117,11 @@ val invalidate :
   Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
 (** record that the address is invalid *)
 
+val invalidate_biad_isl :
+  Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t list access_result
+(** record that the address is invalid. If the address has not been allocated, abduce ISL specs for
+    both invalid (null, free, unint) and allocated heap. *)
+
 val allocate : Procname.t -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t
 
 val add_dynamic_type : Typ.Name.t -> AbstractValue.t -> t -> t