Merge pull request #712 from goblint/realloc

Add `realloc` support

src/analyses/base.ml

@@ -213,6 +213,19 @@ struct
       | Some (x, o) -> Addr.from_var_offset (x, addToOffset n (Some x.vtype) o)
       | None -> default addr
     in
+    let addToAddrOp p n =
+      match op with
+      (* For array indexing e[i] and pointer addition e + i we have: *)
+      | IndexPI | PlusPI ->
+        `Address (AD.map (addToAddr n) p)
+      (* Pointer subtracted by a value (e-i) is very similar *)
+      (* Cast n to the (signed) ptrdiff_ikind, then add the its negated value. *)
+      | MinusPI ->
+        let n = ID.neg (ID.cast_to (Cilfacade.ptrdiff_ikind ()) n) in
+        `Address (AD.map (addToAddr n) p)
+      | Mod -> `Int (ID.top_of (Cilfacade.ptrdiff_ikind ())) (* we assume that address is actually casted to int first*)
+      | _ -> `Address AD.top_ptr
+    in
     (* The main function! *)
     match a1,a2 with
     (* For the integer values, we apply the domain operator *)
@@ -226,19 +239,13 @@ struct
       `Int (match ID.to_bool n, AD.to_bool p with
           | Some a, Some b -> ID.of_bool ik (op=Eq && a=b || op=Ne && a<>b)
           | _ -> bool_top ik)
-    | `Address p, `Int n  -> begin
-        match op with
-        (* For array indexing e[i] and pointer addition e + i we have: *)
-        | IndexPI | PlusPI ->
-          `Address (AD.map (addToAddr n) p)
-        (* Pointer subtracted by a value (e-i) is very similar *)
-        (* Cast n to the (signed) ptrdiff_ikind, then add the its negated value. *)
-        | MinusPI ->
-          let n = ID.neg (ID.cast_to (Cilfacade.ptrdiff_ikind ()) n) in
-          `Address (AD.map (addToAddr n) p)
-        | Mod -> `Int (ID.top_of (Cilfacade.ptrdiff_ikind ())) (* we assume that address is actually casted to int first*)
-        | _ -> `Address AD.top_ptr
-      end
+    | `Address p, `Int n  ->
+      addToAddrOp p n
+    | `Address p, `Top ->
+      (* same as previous, but with Unknown instead of int *)
+      (* TODO: why does this even happen in zstd-thread-pool-add? *)
+      let n = ID.top_of (Cilfacade.ptrdiff_ikind ()) in (* pretend to have unknown ptrdiff int instead *)
+      addToAddrOp p n
     (* If both are pointer values, we can subtract them and well, we don't
      * bother to find the result in most cases, but it's an integer. *)
     | `Address p1, `Address p2 -> begin
@@ -715,17 +722,22 @@ struct
           let cast_ok = function
             | Addr (x, o) ->
               begin
-                match Cil.getInteger (sizeOf t), Cil.getInteger (sizeOf (get_type_addr (x, o))) with
-                | Some i1, Some i2 -> Cilint.compare_cilint i1 i2 <= 0
-                | _ ->
-                  if contains_vla t || contains_vla (get_type_addr (x, o)) then
-                    begin
-                      (* TODO: Is this ok? *)
-                      M.warn "Casting involving a VLA is assumed to work";
-                      true
-                    end
-                  else
-                    false
+                let at = get_type_addr (x, o) in
+                if M.tracing then M.tracel "evalint" "cast_ok %a %a %a\n" Addr.pretty (Addr (x, o)) CilType.Typ.pretty (Cil.unrollType x.vtype) CilType.Typ.pretty at;
+                if at = TVoid [] then (* HACK: cast from alloc variable is always fine *)
+                  true
+                else
+                  match Cil.getInteger (sizeOf t), Cil.getInteger (sizeOf at) with
+                  | Some i1, Some i2 -> Cilint.compare_cilint i1 i2 <= 0
+                  | _ ->
+                    if contains_vla t || contains_vla (get_type_addr (x, o)) then
+                      begin
+                        (* TODO: Is this ok? *)
+                        M.warn "Casting involving a VLA is assumed to work";
+                        true
+                      end
+                    else
+                      false
               end
             | NullPtr | UnknownPtr -> true (* TODO: are these sound? *)
             | _ -> false
@@ -2304,6 +2316,39 @@ struct
                                   (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), `Address (add_null (AD.from_var_offset (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
         | _ -> st
       end
+    | `Realloc (p, size) ->
+      begin match lv with
+        | Some lv ->
+          let ask = Analyses.ask_of_ctx ctx in
+          let p_rv = eval_rv ask gs st p in
+          let p_addr =
+            match p_rv with
+            | `Address a -> a
+            (* TODO: don't we already have logic for this? *)
+            | `Int i when ID.to_int i = Some BI.zero -> AD.null_ptr
+            | `Int i -> AD.top_ptr
+            | _ -> AD.top_ptr (* TODO: why does this ever happen? *)
+          in
+          let p_addr' = AD.remove NullPtr p_addr in (* realloc with NULL is same as malloc, remove to avoid unknown value from NullPtr access *)
+          let p_addr_get = get ask gs st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *)
+          let size_int = eval_int ask gs st size in
+          let heap_val = `Blob (p_addr_get, size_int, true) in (* copy old contents with new size *)
+          let heap_addr = AD.from_var (heap_var ctx) in
+          let heap_addr' =
+            if get_bool "sem.malloc.fail" then
+              AD.join heap_addr AD.null_ptr
+            else
+              heap_addr
+          in
+          let lv_addr = eval_lv ask gs st lv in
+          set_many ~ctx ask gs st [
+            (heap_addr, TVoid [], heap_val);
+            (lv_addr, Cilfacade.typeOfLval lv, `Address heap_addr');
+          ]
+          (* TODO: free (i.e. invalidate) old blob if successful? *)
+        | None ->
+          st
+      end
     | `Unknown "__goblint_unknown" ->
       begin match args with
         | [Lval lv] | [CastE (_,AddrOf lv)] ->

src/analyses/libraryFunctions.ml

@@ -153,6 +153,12 @@ struct
     | `Read  -> o
     | `Free  -> i
 
+  let readsFrees rs fs a x =
+    match a with
+    | `Write -> []
+    | `Read  -> keep rs x
+    | `Free  -> keep fs x
+
   let onlyReads ns a x =
     match a with
     | `Write -> []
@@ -452,7 +458,7 @@ let invalidate_actions = [
     "rand", readsAll; (*safe*)
     "gethostname", writesAll; (*unsafe*)
     "fork", readsAll; (*safe*)
-    "realloc", writesAll;(*unsafe*)
+    "realloc", readsFrees [0; 1] [0]; (* read+free first argument, read second argument *)
     "setrlimit", readsAll; (*safe*)
     "getrlimit", writes [2]; (*keep [2]*)
     "sem_init", readsAll; (*safe*)

src/analyses/region.ml

@@ -151,10 +151,11 @@ struct
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     match LibraryFunctions.classify f.vname arglist with
-    | `Malloc _ | `Calloc _ -> begin
+    | `Malloc _ | `Calloc _ | `Realloc _ -> begin
         match ctx.local, lval with
         | `Lifted reg, Some lv ->
           let old_regpart = ctx.global () in
+          (* TODO: should realloc use arg region if failed/in-place? *)
           let regpart, reg = Reg.assign_bullet lv (old_regpart, reg) in
           if not (RegPart.leq regpart old_regpart) then
             ctx.sideg () regpart;

src/cdomains/valueDomain.ml

@@ -329,8 +329,8 @@ struct
           end
     in
     let one_addr = let open Addr in function
-        | Addr ({ vtype = TVoid _; _} as v, offs) -> (* we had no information about the type (e.g. malloc), so we add it *)
-          Addr ({ v with vtype = t }, offs)
+        | Addr ({ vtype = TVoid _; _} as v, offs) when not (Cilfacade.isCharType t) -> (* we had no information about the type (e.g. malloc), so we add it; ignore for casts to char* since they're special conversions (N1570 6.3.2.3.7) *)
+          Addr ({ v with vtype = t }, offs) (* HACK: equal varinfo with different type, causes inconsistencies down the line, when we again assume vtype being "right", but joining etc gives no consideration to which type version to keep *)
         | Addr (v, o) as a ->
           begin try Addr (v, (adjust_offs v o None)) (* cast of one address by adjusting the abstract offset *)
             with CastError s -> (* don't know how to handle this cast :( *)
@@ -690,6 +690,7 @@ struct
     |                 t , `Blob n       -> `Blob (Blobs.invalidate_value ask t n)
     |                 _ , `List n       -> `Top
     |                 _ , `Thread _     -> state (* TODO: no top thread ID set! *)
+    | _, `Bot -> `Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *)
     |                 t , _             -> top_value t
 
 

src/util/cilfacade.ml

@@ -31,6 +31,11 @@ let get_stmtLoc stmt =
     get_labelsLoc stmt.labels
   | _ -> get_stmtkindLoc stmt.skind
 
+(** Is character type (N1570 6.2.5.15)? *)
+let isCharType = function
+  | TInt ((IChar | ISChar | IUChar), _) -> true
+  | _ -> false
+
 
 let init () =
   initCIL ();

tests/regression/02-base/76-realloc.c

@@ -0,0 +1,52 @@
+// PARAM: --enable ana.race.free
+#include <stdlib.h>
+#include <assert.h>
+#include <pthread.h>
+
+void test1_f() {
+  assert(1); // reachable
+}
+
+void test1() {
+  void (**fpp)(void) = malloc(sizeof(void(**)(void)));
+  *fpp = &test1_f;
+
+  fpp = realloc(fpp, sizeof(void(**)(void))); // same size
+
+  // (*fpp)();
+  void (*fp)(void) = *fpp;
+  fp(); // should call test1_f
+}
+
+void* test2_f(void *arg) {
+  int *p = arg;
+  *p = 1; // RACE!
+  return NULL;
+}
+
+void test2() {
+  int *p = malloc(sizeof(int));
+  pthread_t id;
+  pthread_create(&id, NULL, test2_f, p);
+  realloc(p, sizeof(int)); // RACE!
+}
+
+void* test3_f(void *arg) {
+  int *p = arg;
+  int x = *p; // RACE!
+  return NULL;
+}
+
+void test3() {
+  int *p = malloc(sizeof(int));
+  pthread_t id;
+  pthread_create(&id, NULL, test3_f, p);
+  realloc(p, sizeof(int)); // RACE!
+}
+
+int main() {
+  test1();
+  test2();
+  test3();
+  return 0;
+}