[pulse] Record writes explicitly as Attributes and get rid of heuristic in is_cell_read_only

Reviewed By: jvillard

Differential Revision: D16543753

fbshipit-source-id: 4c0d9fb41

infer/src/base/CommandLineOption.mli

@@ -211,6 +211,8 @@ val mk_subcommand :
 val args_env_var : string
 (** environment variable use to pass arguments from parent to child processes *)
 
+val strict_mode : bool
+
 val strict_mode_env_var : string
 
 val env_var_sep : char

infer/src/pulse/PulseAbductiveDomain.ml

@@ -169,7 +169,9 @@ module Memory = struct
 
 
   let add_edge addr access new_addr_trace astate =
-    map_post_heap astate ~f:(fun heap -> BaseMemory.add_edge addr access new_addr_trace heap)
+    map_post_heap astate ~f:(fun heap ->
+        BaseMemory.add_edge addr access new_addr_trace heap
+        |> BaseMemory.add_attributes addr (Attributes.singleton WrittenTo) )
 
 
   let find_edge_opt address access astate =
@@ -219,7 +221,9 @@ module Memory = struct
   let find_opt address astate = BaseMemory.find_opt address (astate.post :> base_domain).heap
 
   let set_cell addr cell astate =
-    map_post_heap astate ~f:(fun heap -> BaseMemory.set_cell addr cell heap)
+    map_post_heap astate ~f:(fun heap ->
+        BaseMemory.set_cell addr cell heap
+        |> BaseMemory.add_attributes addr (Attributes.singleton WrittenTo) )
 
 
   module Edges = BaseMemory.Edges
@@ -472,10 +476,9 @@ module PrePost = struct
     match cell_pre_opt with
     | None ->
         false
-    | Some (edges_pre, _) ->
-        ( Attributes.is_empty attrs_post
-        || Attributes.only_contains_address_of_stack_variable attrs_post )
-        && PulseDomain.Memory.Edges.equal
+    | Some (edges_pre, _) when not (Attributes.is_modified attrs_post) ->
+        let are_edges_equal =
+          PulseDomain.Memory.Edges.equal
             (fun (addr_dest_pre, _) (addr_dest_post, _) ->
               (* NOTE: ignores traces
 
@@ -483,6 +486,11 @@ module PrePost = struct
                   the post trace *)
               AbstractAddress.equal addr_dest_pre addr_dest_post )
             edges_pre edges_post
+        in
+        if CommandLineOption.strict_mode then assert are_edges_equal ;
+        are_edges_equal
+    | _ ->
+        false
 
 
   let materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals
@@ -574,6 +582,7 @@ module PrePost = struct
                 {action= trace.action; f= Call proc_name; location}
           ; history= trace.history }
     | MustBeValid _
+    | WrittenTo
     | AddressOfCppTemporary (_, _)
     | AddressOfStackVariable (_, _, _)
     | Closure _
@@ -609,6 +618,7 @@ module PrePost = struct
           post_edges_minus_pre translated_post_edges
       in
       PulseDomain.Memory.set_edges addr_caller edges_post_caller heap
+      |> PulseDomain.Memory.add_attributes addr_caller (PulseDomain.Attributes.singleton WrittenTo)
     in
     let caller_post = Domain.make (call_state.astate.post :> base_domain).stack heap in
     {call_state with subst; astate= {call_state.astate with post= caller_post}}

infer/src/pulse/PulseDomain.ml

@@ -246,6 +246,7 @@ module Attribute = struct
   type t =
     | Invalid of Invalidation.t Trace.t
     | MustBeValid of unit InterprocAction.t
+    | WrittenTo
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t
     | Closure of Typ.Procname.t
@@ -258,6 +259,8 @@ module Attribute = struct
 
   let closure_rank = Variants.to_rank (Closure (Typ.Procname.from_string_c_fun ""))
 
+  let address_is_written_to_rank = Variants.to_rank WrittenTo
+
   let address_of_stack_variable_rank =
     let pname = Typ.Procname.from_string_c_fun "" in
     let var = Var.of_pvar (Pvar.mk (Mangled.from_string "") pname) in
@@ -285,6 +288,8 @@ module Attribute = struct
           (InterprocAction.pp (fun _ () -> ()))
           action Location.pp
           (InterprocAction.to_outer_location action)
+    | WrittenTo ->
+        F.fprintf f "written"
     | AddressOfCppTemporary (var, history) ->
         F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history
     | AddressOfStackVariable (var, history, location) ->
@@ -330,9 +335,9 @@ module Attributes = struct
     Set.find_rank attrs Attribute.std_vector_reserve_rank |> Option.is_some
 
 
-  let only_contains_address_of_stack_variable attrs =
-    Set.is_singleton attrs
-    && Option.is_some (Set.find_rank attrs Attribute.address_of_stack_variable_rank)
+  let is_modified attrs =
+    Option.is_some (Set.find_rank attrs Attribute.address_is_written_to_rank)
+    || Option.is_some (Set.find_rank attrs Attribute.invalid_rank)
 
 
   include Set

infer/src/pulse/PulseDomain.mli

@@ -83,6 +83,7 @@ module Attribute : sig
   type t =
     | Invalid of Invalidation.t Trace.t
     | MustBeValid of unit InterprocAction.t
+    | WrittenTo
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t
     | Closure of Typ.Procname.t
@@ -97,7 +98,7 @@ module Attributes : sig
 
   val get_address_of_stack_variable : t -> (Var.t * ValueHistory.t * Location.t) option
 
-  val only_contains_address_of_stack_variable : t -> bool
+  val is_modified : t -> bool
 end
 
 module AbstractAddress : sig