From 77865559f5ec0972729b05f70dcd160c6846391a Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Mon, 24 May 2021 05:05:31 -0700
Subject: [PATCH] [pulse] model realloc(3)

Summary:
Let's model all the dynamic memory management functions as they all work
together and are important for a lot of C projects.

Reviewed By: ezgicicek

Differential Revision: D28543008

fbshipit-source-id: f130e1ab6
---
 infer/src/pulse/PulseModels.ml                | 16 +++++++++++++++
 infer/tests/codetoanalyze/c/pulse/issues.exp  |  2 ++
 .../codetoanalyze/c/pulse/issues.exp-isl      |  2 ++
 .../tests/codetoanalyze/c/pulse/memory_leak.c | 20 +++++++++++++++++++
 4 files changed, 40 insertions(+)

diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 824a18812..095574303 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -227,6 +227,21 @@ module C = struct
   let malloc_not_null size_exp = malloc_not_null_common ~size_exp_opt:(Some size_exp)
 
   let malloc_not_null_no_param = malloc_not_null_common ~size_exp_opt:None
+
+  let realloc pointer size : model =
+   fun data astate ->
+    free pointer data astate
+    |> List.concat_map ~f:(fun result ->
+           let<*> exec_state = result in
+           match (exec_state : ExecutionDomain.t) with
+           | ContinueProgram astate ->
+               malloc size data astate
+           | ExitProgram _
+           | AbortProgram _
+           | LatentAbortProgram _
+           | LatentInvalidAccess _
+           | ISLLatentMemoryError _ ->
+               [Ok exec_state] )
 end
 
 module ObjCCoreFoundation = struct
@@ -1398,6 +1413,7 @@ module ProcNameDispatcher = struct
       ( transfer_ownership_matchers @ abort_matchers
       @ [ +BuiltinDecl.(match_builtin free) <>$ capt_arg_payload $--> C.free
         ; +BuiltinDecl.(match_builtin malloc) <>$ capt_exp $--> C.malloc
+        ; -"realloc" <>$ capt_arg_payload $+ capt_exp $--> C.realloc
         ; +BuiltinDecl.(match_builtin __delete) <>$ capt_arg_payload $--> Cplusplus.delete
         ; +BuiltinDecl.(match_builtin __new)
           <>$ capt_exp
diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp
index b1a410575..41b882a96 100644
--- a/infer/tests/codetoanalyze/c/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/c/pulse/issues.exp
@@ -22,6 +22,8 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_out_parameter_local_mutation_bad, 3,
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `malloc_via_ptr` here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `malloc_via_ptr` here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc_via_ptr`,is the null pointer,returned,return from call to `malloc_via_ptr`,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/memory_leak.c, realloc_no_check_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,in call to `realloc_wrapper`,in call to `realloc` (modelled),is the null pointer,returned,return from call to `realloc_wrapper`,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/memory_leak.c, realloc_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `realloc_wrapper` here,allocated by `realloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp-isl b/infer/tests/codetoanalyze/c/pulse/issues.exp-isl
index 43d635216..9d5a3ef3b 100644
--- a/infer/tests/codetoanalyze/c/pulse/issues.exp-isl
+++ b/infer/tests/codetoanalyze/c/pulse/issues.exp-isl
@@ -22,6 +22,8 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_out_parameter_local_mutation_bad, 3,
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `malloc_via_ptr` here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `malloc_via_ptr` here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc_via_ptr`,is the null pointer,returned,return from call to `malloc_via_ptr`,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/memory_leak.c, realloc_no_check_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,in call to `realloc_wrapper`,in call to `realloc` (modelled),is the null pointer,returned,return from call to `realloc_wrapper`,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/memory_leak.c, realloc_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `realloc_wrapper` here,allocated by `realloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
diff --git a/infer/tests/codetoanalyze/c/pulse/memory_leak.c b/infer/tests/codetoanalyze/c/pulse/memory_leak.c
index f87e6135d..24698e6f5 100644
--- a/infer/tests/codetoanalyze/c/pulse/memory_leak.c
+++ b/infer/tests/codetoanalyze/c/pulse/memory_leak.c
@@ -101,3 +101,23 @@ void report_leak_in_correct_line_bad(int* x) {
   }
   free(x);
 }
+
+void* realloc_wrapper(void* p, size_t size) { return realloc(p, size); }
+
+void realloc_free_ok() {
+  int* p = (int*)malloc(sizeof(int));
+  int* q = realloc_wrapper(p, sizeof(int));
+  free(q);
+}
+
+void realloc_no_free_bad() {
+  int* p = (int*)malloc(sizeof(int));
+  int* q = realloc_wrapper(p, sizeof(int));
+}
+
+void realloc_no_check_bad() {
+  int* p = (int*)malloc(sizeof(int));
+  int* q = realloc_wrapper(p, sizeof(int));
+  *q = 42;
+  free(q);
+}