[unnecessary copy] Distinguish copy construction or assignment for mo…

…vable issue types

Reviewed By: ggwg

Differential Revision: D37483979

fbshipit-source-id: 51fe7bdd7c266f730d849d236e682976c455ed19

infer/man/man1/infer-full.txt

@@ -592,6 +592,8 @@ OPTIONS
              PULSE_UNINITIALIZED_VALUE_LATENT (disabled by default),
              PULSE_UNNECESSARY_COPY (disabled by default),
              PULSE_UNNECESSARY_COPY_ASSIGNMENT (disabled by default),
+             PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (disabled by
+           default),
              PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),

infer/man/man1/infer-report.txt

@@ -262,6 +262,8 @@ OPTIONS
              PULSE_UNINITIALIZED_VALUE_LATENT (disabled by default),
              PULSE_UNNECESSARY_COPY (disabled by default),
              PULSE_UNNECESSARY_COPY_ASSIGNMENT (disabled by default),
+             PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (disabled by
+           default),
              PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),

infer/man/man1/infer.txt

@@ -592,6 +592,8 @@ OPTIONS
              PULSE_UNINITIALIZED_VALUE_LATENT (disabled by default),
              PULSE_UNNECESSARY_COPY (disabled by default),
              PULSE_UNNECESSARY_COPY_ASSIGNMENT (disabled by default),
+             PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (disabled by
+           default),
              PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),

infer/src/base/IssueType.ml

@@ -1063,6 +1063,12 @@ let unnecessary_copy_assignment_pulse =
     ~user_documentation:"See [PULSE_UNNECESSARY_COPY](#pulse_unnecessary_copy)."
 
 
+let unnecessary_copy_assignment_movable_pulse =
+  register ~enabled:false ~id:"PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE" Error Pulse
+    ~hum:"Unnecessary Copy Assignment Movable"
+    ~user_documentation:"See [PULSE_UNNECESSARY_COPY_MOVABLE](#pulse_unnecessary_copy_movable)."
+
+
 let unnecessary_copy_movable_pulse =
   register ~enabled:false ~id:"PULSE_UNNECESSARY_COPY_MOVABLE" Error Pulse
     ~hum:"Unnecessary Copy Movable"

infer/src/base/IssueType.mli

@@ -368,6 +368,8 @@ val unnecessary_copy_pulse : t
 
 val unnecessary_copy_assignment_pulse : t
 
+val unnecessary_copy_assignment_movable_pulse : t
+
 val unnecessary_copy_movable_pulse : t
 
 val unreachable_code_after : t

infer/src/pulse/PulseAttribute.ml

@@ -89,13 +89,24 @@ module Attribute = struct
 
   module TaintSanitizedSet = PrettyPrintable.MakePPSet (TaintSanitized)
 
+  module CopyOrigin = struct
+    type t = CopyCtor | CopyAssignment [@@deriving compare, equal]
+
+    let pp fmt = function
+      | CopyCtor ->
+          F.fprintf fmt "copied"
+      | CopyAssignment ->
+          F.fprintf fmt "copy assigned"
+  end
+
   module CopiedInto = struct
-    type t = IntoVar of Var.t | IntoField of Fieldname.t [@@deriving compare, equal]
+    type t = IntoVar of Var.t | IntoField of {field: Fieldname.t; from: CopyOrigin.t}
+    [@@deriving compare, equal]
 
     let pp fmt = function
       | IntoVar var ->
           Var.pp fmt var
-      | IntoField field ->
+      | IntoField {field} ->
           Fieldname.pp fmt field
   end
 

infer/src/pulse/PulseAttribute.mli

@@ -50,8 +50,15 @@ end
 
 module TaintSanitizedSet : PrettyPrintable.PPSet with type elt = TaintSanitized.t
 
+module CopyOrigin : sig
+  type t = CopyCtor | CopyAssignment [@@deriving compare, equal]
+
+  val pp : Formatter.t -> t -> unit
+end
+
 module CopiedInto : sig
-  type t = IntoVar of Var.t | IntoField of Fieldname.t [@@deriving compare, equal]
+  type t = IntoVar of Var.t | IntoField of {field: Fieldname.t; from: CopyOrigin.t}
+  [@@deriving compare, equal]
 
   val pp : F.formatter -> t -> unit
 end

infer/src/pulse/PulseDiagnostic.ml

@@ -78,7 +78,7 @@ type t =
       { copied_into: PulseAttribute.CopiedInto.t
       ; typ: Typ.t
       ; location: Location.t
-      ; from: PulseNonDisjunctiveDomain.CopyOrigin.t }
+      ; from: PulseAttribute.CopyOrigin.t }
 [@@deriving equal]
 
 let get_location = function
@@ -367,30 +367,30 @@ let get_message diagnostic =
       F.asprintf "`%a` flows to taint sink %a%a" Decompiler.pp_expr expr Taint.pp sink pp_sanitizers
         sanitizers
   | UnnecessaryCopy {copied_into; typ; location; from} -> (
-      let open PulseNonDisjunctiveDomain in
+      let open PulseAttribute in
       let suppression_msg =
         "If this copy was intentional, consider adding the word `copy` into the variable name to \
          suppress this warning"
       in
       let suggestion_msg =
-        match from with
-        | CopyOrigin.CopyCtor ->
+        match (from : CopyOrigin.t) with
+        | CopyCtor ->
             "try using a reference `&`"
-        | CopyOrigin.CopyAssignment ->
+        | CopyAssignment ->
             "try getting a reference to it or move it if possible"
       in
       match copied_into with
       | IntoVar _ ->
           F.asprintf
             "%a variable `%a` with type `%a` is not modified after it is copied on %a. To avoid \
              the copy, %s. %s."
-            CopyOrigin.pp from PulseAttribute.CopiedInto.pp copied_into (Typ.pp_full Pp.text) typ
-            Location.pp_line location suggestion_msg suppression_msg
-      | IntoField fname ->
+            CopyOrigin.pp from CopiedInto.pp copied_into (Typ.pp_full Pp.text) typ Location.pp_line
+            location suggestion_msg suppression_msg
+      | IntoField {field; from} ->
           F.asprintf
-            "Field `%a` with type `%a` is copied into from an rvalue-ref here but is not modified \
+            "Field `%a` with type `%a` is %a into from an rvalue-ref here but is not modified \
              afterwards. Rather than copying into it, try moving into it instead."
-            Fieldname.pp fname (Typ.pp_full Pp.text) typ )
+            Fieldname.pp field (Typ.pp_full Pp.text) typ CopyOrigin.pp from )
 
 
 let add_errlog_header ~nesting ~title location errlog =
@@ -559,7 +559,7 @@ let get_trace = function
   | UnnecessaryCopy {location; from} ->
       let nesting = 0 in
       [ Errlog.make_trace_element nesting location
-          (F.asprintf "%a here" PulseNonDisjunctiveDomain.CopyOrigin.pp from)
+          (F.asprintf "%a here" PulseAttribute.CopyOrigin.pp from)
           [] ]
 
 
@@ -580,11 +580,13 @@ let get_issue_type ~latent issue_type =
       IssueType.retain_cycle
   | StackVariableAddressEscape _, false ->
       IssueType.stack_variable_address_escape
-  | UnnecessaryCopy {copied_into= PulseAttribute.CopiedInto.IntoField _}, false ->
+  | UnnecessaryCopy {copied_into= IntoField {from= CopyAssignment}}, false ->
+      IssueType.unnecessary_copy_assignment_movable_pulse
+  | UnnecessaryCopy {copied_into= IntoField {from= CopyCtor}}, false ->
       IssueType.unnecessary_copy_movable_pulse
-  | UnnecessaryCopy {from= PulseNonDisjunctiveDomain.CopyOrigin.CopyCtor}, false ->
+  | UnnecessaryCopy {from= CopyCtor}, false ->
       IssueType.unnecessary_copy_pulse
-  | UnnecessaryCopy {from= PulseNonDisjunctiveDomain.CopyOrigin.CopyAssignment}, false ->
+  | UnnecessaryCopy {from= CopyAssignment}, false ->
       IssueType.unnecessary_copy_assignment_pulse
   | ( ( MemoryLeak _
       | ResourceLeak _

infer/src/pulse/PulseDiagnostic.mli

@@ -84,7 +84,7 @@ type t =
       { copied_into: PulseAttribute.CopiedInto.t
       ; typ: Typ.t
       ; location: Location.t
-      ; from: PulseNonDisjunctiveDomain.CopyOrigin.t }
+      ; from: PulseAttribute.CopyOrigin.t }
 [@@deriving equal]
 
 val aborts_execution : t -> bool

infer/src/pulse/PulseNonDisjunctiveDomain.ml

@@ -26,18 +26,9 @@ module BaseMemory = PulseBaseMemory
 
     Then we compare the snapshot heap with the current heap (see {!PulseNonDisjunctiveOperations}.) *)
 
-module CopyOrigin = struct
-  type t = CopyCtor | CopyAssignment [@@deriving compare, equal]
-
-  let pp fmt = function
-    | CopyCtor ->
-        F.fprintf fmt "copied"
-    | CopyAssignment ->
-        F.fprintf fmt "copy assigned"
-end
-
 type copy_spec_t =
-  | Copied of {typ: Typ.t; location: Location.t; heap: BaseMemory.t; from: CopyOrigin.t}
+  | Copied of
+      {typ: Typ.t; location: Location.t; heap: BaseMemory.t; from: PulseAttribute.CopyOrigin.t}
   | Modified
 [@@deriving equal]
 
@@ -62,8 +53,8 @@ module CopySpec = struct
 
   let pp fmt = function
     | Copied {typ; heap; location; from} ->
-        Format.fprintf fmt " %a (%a) at %a with heap= %a" CopyOrigin.pp from pp_typ typ Location.pp
-          location BaseMemory.pp heap
+        Format.fprintf fmt " %a (%a) at %a with heap= %a" PulseAttribute.CopyOrigin.pp from pp_typ
+          typ Location.pp location BaseMemory.pp heap
     | Modified ->
         Format.fprintf fmt "modified"
 end
@@ -176,10 +167,12 @@ let add_var copied_var ~source_addr_opt (res : copy_spec_t) astate =
     copy_map= CopyMap.add {copied_into= IntoVar copied_var; source_addr_opt} res astate.copy_map }
 
 
-let add_field copied_field ~source_addr_opt (res : copy_spec_t) astate =
+let add_field copied_field from ~source_addr_opt (res : copy_spec_t) astate =
   { astate with
-    copy_map= CopyMap.add {copied_into= IntoField copied_field; source_addr_opt} res astate.copy_map
-  }
+    copy_map=
+      CopyMap.add
+        {copied_into= IntoField {field= copied_field; from}; source_addr_opt}
+        res astate.copy_map }
 
 
 let is_checked_via_dtor var {destructor_checked} = DestructorChecked.mem var destructor_checked

infer/src/pulse/PulseNonDisjunctiveDomain.mli

@@ -8,21 +8,22 @@
 open! IStd
 module BaseMemory = PulseBaseMemory
 
-module CopyOrigin : sig
-  type t = CopyCtor | CopyAssignment [@@deriving compare, equal]
-
-  val pp : Formatter.t -> t -> unit
-end
-
 type copy_spec_t =
-  | Copied of {typ: Typ.t; location: Location.t; heap: BaseMemory.t; from: CopyOrigin.t}
+  | Copied of
+      {typ: Typ.t; location: Location.t; heap: BaseMemory.t; from: PulseAttribute.CopyOrigin.t}
   | Modified
 
 include AbstractDomain.WithBottom
 
 val add_var : Var.t -> source_addr_opt:PulseAbstractValue.t option -> copy_spec_t -> t -> t
 
-val add_field : Fieldname.t -> source_addr_opt:PulseAbstractValue.t option -> copy_spec_t -> t -> t
+val add_field :
+     Fieldname.t
+  -> PulseAttribute.CopyOrigin.t
+  -> source_addr_opt:PulseAbstractValue.t option
+  -> copy_spec_t
+  -> t
+  -> t
 
 val checked_via_dtor : Var.t -> t -> t
 
@@ -33,7 +34,8 @@ val mark_copy_as_modified :
   -> t
   -> t
 
-val get_copied : t -> (PulseAttribute.CopiedInto.t * Typ.t * Location.t * CopyOrigin.t) list
+val get_copied :
+  t -> (PulseAttribute.CopiedInto.t * Typ.t * Location.t * PulseAttribute.CopyOrigin.t) list
 
 val is_checked_via_dtor : Var.t -> t -> bool
 

infer/src/pulse/PulseNonDisjunctiveOperations.ml

@@ -13,7 +13,7 @@ open PulseBasicInterface
 let get_modeled_as_returning_copy_opt proc_name =
   Option.value_map ~default:None Config.pulse_model_returns_copy_pattern ~f:(fun r ->
       let s = Procname.to_string proc_name in
-      if Str.string_match r s 0 then Some PulseNonDisjunctiveDomain.CopyOrigin.CopyCtor else None )
+      if Str.string_match r s 0 then Some Attribute.CopyOrigin.CopyCtor else None )
 
 
 let get_copied_and_source copy_type path rest_args location from (disjunct : AbductiveDomain.t) =
@@ -84,13 +84,14 @@ let add_copies path location call_exp actuals astates astate_non_disj =
                          Option.value_map source_addr_typ_opt ~default:disjunct
                            ~f:(fun (source_addr, _) ->
                              AddressAttributes.add_one source_addr
-                               (CopiedInto (Attribute.CopiedInto.IntoField field)) disjunct
+                               (CopiedInto (Attribute.CopiedInto.IntoField {field; from}))
+                               disjunct
                              |> AddressAttributes.add_one copy_addr
                                   (SourceOriginOfCopy
                                      { source= source_addr
                                      ; is_const_ref= Typ.is_const_reference source_typ } ) )
                        in
-                       ( NonDisjDomain.add_field field
+                       ( NonDisjDomain.add_field field from
                            ~source_addr_opt:(Option.map source_addr_typ_opt ~f:fst)
                            copied astate_non_disj
                        , ExecutionDomain.continue disjunct' )
@@ -106,9 +107,9 @@ let add_copies path location call_exp actuals astates astate_non_disj =
             (astate_non_disj, exec_state) )
   in
   let copy_from_fn pname =
-    let open PulseNonDisjunctiveDomain in
-    if Procname.is_copy_ctor pname then Some CopyOrigin.CopyCtor
-    else if Procname.is_copy_assignment pname then Some CopyOrigin.CopyAssignment
+    let open Attribute.CopyOrigin in
+    if Procname.is_copy_ctor pname then Some CopyCtor
+    else if Procname.is_copy_assignment pname then Some CopyAssignment
     else None
   in
   let astate_n, astates = aux (copy_from_fn, Fn.id) astate_non_disj astates in

infer/tests/build_systems/pulse_messages/issues.exp

@@ -25,7 +25,7 @@ build_systems/pulse_messages/optional.cpp, optional_empty_access::latent, 38, 13
 build_systems/pulse_messages/optional.cpp, optional_empty_access::make_latent_manifest, 48, 31, ERROR, OPTIONAL_EMPTY_ACCESS, The call to `optional_empty_access::propagate_latent_3_latent` ends up calling `optional_empty_access::latent` (after 2 more calls) and may trigger the following issue: call to `optional_empty_access::propagate_latent_3_latent()` eventually accesses memory that is assigned an empty value during the call to `optional_empty_access::propagate_latent_3_latent()` on line 37.
 build_systems/pulse_messages/unnecessary_copy.cpp, copy_decl_bad, 20, 14, ERROR, PULSE_UNNECESSARY_COPY, copied variable `cpy` with type `A` is not modified after it is copied on line 20. To avoid the copy, try using a reference `&`. If this copy was intentional, consider adding the word `copy` into the variable name to suppress this warning.
 build_systems/pulse_messages/unnecessary_copy.cpp, copy_assignment_bad, 27, 3, ERROR, PULSE_UNNECESSARY_COPY_ASSIGNMENT, copy assigned variable `c` with type `A` is not modified after it is copied on line 27. To avoid the copy, try getting a reference to it or move it if possible. If this copy was intentional, consider adding the word `copy` into the variable name to suppress this warning.
-build_systems/pulse_messages/unnecessary_copy.cpp, Test::unnecessary_copy_moveable_bad, 33, 47, ERROR, PULSE_UNNECESSARY_COPY_MOVABLE, Field `mem_a` with type `A` is copied into from an rvalue-ref here but is not modified afterwards. Rather than copying into it, try moving into it instead.
+build_systems/pulse_messages/unnecessary_copy.cpp, Test::unnecessary_copy_moveable_bad, 33, 47, ERROR, PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE, Field `mem_a` with type `A` is copy assigned into from an rvalue-ref here but is not modified afterwards. Rather than copying into it, try moving into it instead.
 build_systems/pulse_messages/use_after_free.c, uaf_intraprocedural_bad, 12, 11, ERROR, USE_AFTER_FREE, accessing memory that was invalidated by call to `free()` on line 11.
 build_systems/pulse_messages/use_after_free.c, free_wrapper_uaf_bad, 19, 11, ERROR, USE_AFTER_FREE, accessing memory that was invalidated by call to `free()` during the call to `free_wrapper()` on line 18.
 build_systems/pulse_messages/use_after_free.c, uaf_via_deref_bad, 26, 3, ERROR, USE_AFTER_FREE, call to `deref_int()` eventually accesses memory that was invalidated by call to `free()` on line 25.

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -246,8 +246,8 @@ codetoanalyze/cpp/pulse/unnecessary_copy.cpp, constructor_bad, 2, PULSE_UNNECESS
 codetoanalyze/cpp/pulse/unnecessary_copy.cpp, copy_assignment_bad, 2, PULSE_UNNECESSARY_COPY_ASSIGNMENT, no_bucket, ERROR, [copy assigned here]
 codetoanalyze/cpp/pulse/unnecessary_copy.cpp, copy_and_move_bad, 1, PULSE_UNNECESSARY_COPY, no_bucket, ERROR, [copied here]
 codetoanalyze/cpp/pulse/unnecessary_copy.cpp, WrapperArr::WrapperArr, 0, PULSE_UNNECESSARY_COPY_MOVABLE, no_bucket, ERROR, [copied here]
-codetoanalyze/cpp/pulse/unnecessary_copy.cpp, WrapperArr::unnecessary_copy_moveable_bad, 1, PULSE_UNNECESSARY_COPY_MOVABLE, no_bucket, ERROR, [copy assigned here]
-codetoanalyze/cpp/pulse/unnecessary_copy.cpp, WrapperArr::unnecessary_copy_moveable_copy_mod_bad, 1, PULSE_UNNECESSARY_COPY_MOVABLE, no_bucket, ERROR, [copy assigned here]
+codetoanalyze/cpp/pulse/unnecessary_copy.cpp, WrapperArr::unnecessary_copy_moveable_bad, 1, PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE, no_bucket, ERROR, [copy assigned here]
+codetoanalyze/cpp/pulse/unnecessary_copy.cpp, WrapperArr::unnecessary_copy_moveable_copy_mod_bad, 1, PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE, no_bucket, ERROR, [copy assigned here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),assigned,invalid access occurs here]

infer/tests/codetoanalyze/cpp/pulse/issues.exp-11

@@ -254,8 +254,8 @@ codetoanalyze/cpp/pulse/unnecessary_copy.cpp, constructor_bad, 2, PULSE_UNNECESS
 codetoanalyze/cpp/pulse/unnecessary_copy.cpp, copy_assignment_bad, 2, PULSE_UNNECESSARY_COPY_ASSIGNMENT, no_bucket, ERROR, [copy assigned here]
 codetoanalyze/cpp/pulse/unnecessary_copy.cpp, copy_and_move_bad, 1, PULSE_UNNECESSARY_COPY, no_bucket, ERROR, [copied here]
 codetoanalyze/cpp/pulse/unnecessary_copy.cpp, WrapperArr::WrapperArr, 0, PULSE_UNNECESSARY_COPY_MOVABLE, no_bucket, ERROR, [copied here]
-codetoanalyze/cpp/pulse/unnecessary_copy.cpp, WrapperArr::unnecessary_copy_moveable_bad, 1, PULSE_UNNECESSARY_COPY_MOVABLE, no_bucket, ERROR, [copy assigned here]
-codetoanalyze/cpp/pulse/unnecessary_copy.cpp, WrapperArr::unnecessary_copy_moveable_copy_mod_bad, 1, PULSE_UNNECESSARY_COPY_MOVABLE, no_bucket, ERROR, [copy assigned here]
+codetoanalyze/cpp/pulse/unnecessary_copy.cpp, WrapperArr::unnecessary_copy_moveable_bad, 1, PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE, no_bucket, ERROR, [copy assigned here]
+codetoanalyze/cpp/pulse/unnecessary_copy.cpp, WrapperArr::unnecessary_copy_moveable_copy_mod_bad, 1, PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE, no_bucket, ERROR, [copy assigned here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),assigned,invalid access occurs here]