From c6237f5f9fc49b07cef92cb2e6e15093648bd118 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= <ezgi@fb.com>
Date: Tue, 10 Mar 2020 02:03:42 -0700
Subject: [PATCH] [pulse] Add model for Object.clone()

Summary: This diff adds a model for Java's `Object.clone()` method (similar to existing shallow_copy).

Reviewed By: jvillard

Differential Revision: D20341073

fbshipit-source-id: 30ae40fe7
---
 infer/src/pulse/PulseModels.ml                    | 11 +++++++++++
 .../java/impurity/PurityModeled.java              | 15 +++++++++++++++
 2 files changed, 26 insertions(+)

diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index f3a3a27ec..654761212 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -240,6 +240,16 @@ module StdAtomicInteger = struct
     [PulseOperations.write_id ret_id (old_int, event :: old_hist) astate]
 end
 
+module JavaObject = struct
+  (* naively modeled as shallow copy. *)
+  let clone src_pointer_hist : model =
+   fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
+    let event = ValueHistory.Call {f= Model "Object.clone"; location; in_call= []} in
+    let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in
+    let+ astate, obj_copy = PulseOperations.shallow_copy location obj astate in
+    [PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate]
+end
+
 module StdBasicString = struct
   let internal_string =
     Fieldname.make
@@ -406,6 +416,7 @@ module ProcNameDispatcher = struct
       ; -"std" &:: "function" &:: "operator()" $ capt_arg_payload $++$--> StdFunction.operator_call
       ; -"std" &:: "function" &:: "operator=" $ capt_arg_payload $+ capt_arg_payload
         $--> Misc.shallow_copy "std::function::operator="
+      ; +PatternMatch.implements_lang "Object" &:: "clone" $ capt_arg_payload $--> JavaObject.clone
       ; -"std" &:: "atomic" &:: "atomic" <>$ capt_arg_payload $+ capt_arg_payload
         $--> StdAtomicInteger.constructor
       ; -"std" &:: "__atomic_base" &:: "fetch_add" <>$ capt_arg_payload $+ capt_arg_payload
diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java
index f7dd01313..11e3e7316 100644
--- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java
+++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java
@@ -96,4 +96,19 @@ class PurityModeled {
       System.nanoTime();
     }
   }
+
+  enum Color {
+    RED,
+    GREEN,
+    BLUE; // values() calls clone
+  }
+
+  public void enum_iter_pure() {
+    for (Color c : Color.values()) {}
+  }
+
+  void clone_pure(ArrayList<String> list) {
+    ArrayList<String> cloned = (ArrayList<String>) list.clone();
+    cloned.add(""); // no change the list
+  }
 }