[pulse] use after free

Summary: Model `free` like `delete`.

Reviewed By: mbouaziz, skcho

Differential Revision: D10509332

fbshipit-source-id: fe4249601

infer/src/checkers/PulseDomain.ml

@@ -155,7 +155,11 @@ module Domain : AbstractDomain.S with type astate = t = struct
 
       let compare_size _ _ = 0
 
-      let merge ~from ~to_ = if Config.debug_mode then to_ := Set.union !from !to_
+      let merge ~from ~to_ =
+        (* building the actual set is only useful to display what equalities where discovered in the
+           HTML debug output *)
+        if Config.debug_mode then to_ := Set.union !from !to_
+
 
       let pp f x = Set.pp f !x
     end

infer/src/checkers/PulseInvalidation.ml

@@ -11,6 +11,7 @@ module L = Logging
 type cause =
   | CppDelete of AccessExpression.t
   | CppDestructor of Typ.Procname.t * AccessExpression.t
+  | CFree of AccessExpression.t
   | StdVectorPushBack of AccessExpression.t
 [@@deriving compare]
 
@@ -21,6 +22,8 @@ let issue_type_of_cause = function
       IssueType.use_after_delete
   | CppDestructor _ ->
       IssueType.use_after_lifetime
+  | CFree _ ->
+      IssueType.use_after_free
   | StdVectorPushBack _ ->
       IssueType.use_after_lifetime
 
@@ -33,6 +36,9 @@ let pp f ({cause; location}[@warning "+9"]) =
   | CppDestructor (proc_name, access_expr) ->
       F.fprintf f "invalidated by destructor call `%a(%a)` at %a" Typ.Procname.pp proc_name
         AccessExpression.pp access_expr Location.pp location
+  | CFree access_expr ->
+      F.fprintf f "invalidated by call to `free(%a)` at %a" AccessExpression.pp access_expr
+        Location.pp location
   | StdVectorPushBack access_expr ->
       F.fprintf f "potentially invalidated by call to `std::vector::push_back(%a, ..)` at %a"
         AccessExpression.pp access_expr Location.pp location

infer/src/checkers/PulseInvalidation.mli

@@ -9,6 +9,7 @@ open! IStd
 type cause =
   | CppDelete of AccessExpression.t
   | CppDestructor of Typ.Procname.t * AccessExpression.t
+  | CFree of AccessExpression.t
   | StdVectorPushBack of AccessExpression.t
 [@@deriving compare]
 

infer/src/checkers/PulseModels.ml

@@ -16,6 +16,16 @@ type exec_fun =
 
 type model = exec_fun
 
+module C = struct
+  let free : model =
+   fun location ~ret:_ ~actuals astate ->
+    match actuals with
+    | [AccessExpression deleted_access] ->
+        PulseDomain.invalidate (CFree deleted_access) location deleted_access astate
+    | _ ->
+        Ok astate
+end
+
 module Cplusplus = struct
   let delete : model =
    fun location ~ret:_ ~actuals astate ->
@@ -89,6 +99,7 @@ end
 let builtins_dispatcher =
   let builtins =
     [ (BuiltinDecl.__delete, Cplusplus.delete)
+    ; (BuiltinDecl.free, C.free)
     ; (BuiltinDecl.__placement_new, Cplusplus.placement_new) ]
   in
   let builtins_map =

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

@@ -28,4 +28,5 @@ codetoanalyze/cpp/ownership/use_after_destructor.cpp, reinit_after_explicit_dest
 codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 61, column 3 here,accessed `*(s.f)` here]
 codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `C_~C(&(c))` at line 186, column 3 here,accessed `pc->f` here]
 codetoanalyze/cpp/pulse/join.cpp, visit_list, 11, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 21, column 5 here,accessed `*(result)` here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(x), ..)` at line 13, column 3 here,accessed `*(y)` here]

infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp

@@ -0,0 +1,12 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <stdlib.h>
+
+int use_after_free_simple_bad(int* x) {
+  free(x);
+  return *x;
+}