From 12c582a69855e17a2cf9c7b6cdf7f8e9c71e5341 Mon Sep 17 00:00:00 2001
From: Loc Le <quangll@fb.com>
Date: Fri, 8 Jan 2021 14:07:35 -0800
Subject: [PATCH] [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      | 10 ++++++++--
 infer/src/pulse/PulseOperations.ml  | 14 ++++++++++++++
 infer/src/pulse/PulseOperations.mli |  5 +++++
 3 files changed, 27 insertions(+), 2 deletions(-)

diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 8da884e47..14cdee24d 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/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
-      [ExecutionDomain.ContinueProgram astate]
+      if Config.pulse_isl then
+        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
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index ad1002c06..468798957 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/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
diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli
index ab6fde32d..f07ee12a5 100644
--- a/infer/src/pulse/PulseOperations.mli
+++ b/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