Primitive malloc freshness analysis

src/analyses/base.ml

@@ -131,6 +131,13 @@ struct
   (* Evaluating Cil's unary operators. *)
   let evalunop op typ = function
     | `Int v1 -> `Int (ID.cast_to (Cilfacade.get_ikind typ) (unop_ID op v1))
+    | `Address a when op = LNot ->
+      if AD.is_null a then
+        `Int (ID.of_bool (Cilfacade.get_ikind typ) true)
+      else if AD.is_not_null a then
+        `Int (ID.of_bool (Cilfacade.get_ikind typ) false)
+      else
+        `Int (ID.top_of (Cilfacade.get_ikind typ))
     | `Bot -> `Bot
     | _ -> VD.top ()
 
@@ -1813,6 +1820,11 @@ struct
         if M.tracing then M.tracel "branchosek" "A The branch %B is dead!\n" tv;
         raise Deadcode
       end
+    (* for some reason refine () can refine these, but not raise Deadcode in struct *)
+    | `Address ad when tv && AD.is_null ad ->
+      raise Deadcode
+    | `Address ad when not tv && AD.is_not_null ad ->
+      raise Deadcode
     | `Bot ->
       if M.tracing then M.traceu "branch" "The branch %B is dead!\n" tv;
       if M.tracing then M.tracel "branchosek" "B The branch %B is dead!\n" tv;

src/analyses/libraryFunctions.ml

@@ -39,6 +39,11 @@ let classify' fn exps =
       | size::_ -> `Malloc size
       | _ -> strange_arguments ()
     end
+  | "ZSTD_customMalloc" -> (* only used with extraspecials *)
+    begin match exps with
+      | size::_ -> `Malloc size
+      | _ -> strange_arguments ()
+    end
   | "kzalloc" ->
     begin match exps with
       | size::_ -> `Calloc (Cil.one, size)
@@ -49,6 +54,11 @@ let classify' fn exps =
       | n::size::_ -> `Calloc (n, size)
       | _ -> strange_arguments ()
     end
+  | "ZSTD_customCalloc" -> (* only used with extraspecials *)
+    begin match exps with
+      | size::_ -> `Calloc (Cil.one, size)
+      | _ -> strange_arguments ()
+    end
   | "realloc" ->
     begin match exps with
       | p::size::_ -> `Realloc (p, size)

src/analyses/mallocFresh.ml

@@ -0,0 +1,71 @@
+open Prelude.Ana
+open Analyses
+
+
+module Spec =
+struct
+  include Analyses.IdentitySpec
+
+  (* must fresh variables *)
+  module D = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)) (* need bot (top) for hoare widen *)
+  module C = D
+
+  let name () = "mallocFresh"
+
+  let startstate _ = D.empty ()
+  let exitstate _ = D.empty ()
+
+  let assign_lval (ask: Queries.ask) lval local =
+    match ask.f (MayPointTo (AddrOf lval)) with
+    | ls when Queries.LS.is_top ls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) ls ->
+      D.empty ()
+    | ls when Queries.LS.exists (fun (v, _) -> not (D.mem v local) && (v.vglob || ThreadEscape.has_escaped ask v)) ls ->
+      D.empty ()
+    | _ ->
+      local
+
+  let assign ctx lval rval =
+    assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
+
+  let combine ctx lval f fd args context f_local =
+    match lval with
+    | None -> f_local
+    | Some lval -> assign_lval (Analyses.ask_of_ctx ctx) lval f_local
+
+  let special ctx lval f args =
+    match LibraryFunctions.classify f.vname args with
+    | `Malloc _
+    | `Calloc _
+    | `Realloc _ ->
+      begin match ctx.ask HeapVar with
+        | `Lifted var -> D.add var ctx.local
+        | _ -> ctx.local
+      end
+    | _ ->
+      match lval with
+      | None -> ctx.local
+      | Some lval -> assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
+
+  let threadenter ctx lval f args =
+    [D.empty ()]
+
+  let threadspawn ctx lval f args fctx =
+    D.empty ()
+
+  module A =
+  struct
+    include BoolDomain.Bool
+    let name () = "fresh"
+    let may_race f1 f2 = not (f1 || f2)
+    let should_print f = f
+  end
+  let access ctx (a: Queries.access) =
+    match a with
+    | Memory {var_opt = Some v; _} ->
+      D.mem v ctx.local
+    | _ ->
+      false
+end
+
+let _ =
+  MCP.register_analysis ~dep:["mallocWrapper"] (module Spec : MCPSpec)

src/analyses/symbLocks.ml

@@ -80,6 +80,8 @@ struct
       D.add (Analyses.ask_of_ctx ctx) (List.hd arglist) ctx.local
     | `Unlock ->
       D.remove (Analyses.ask_of_ctx ctx) (List.hd arglist) ctx.local
+    | `Unknown "ZSTD_customFree" -> (* only used with extraspecials *)
+      ctx.local
     | `Unknown fn when VarEq.safe_fn fn ->
       Messages.warn "Assume that %s does not change lockset." fn;
       ctx.local

tests/regression/03-practical/25-zstd-customMem.c

@@ -0,0 +1,32 @@
+// Extracted from zstd
+#include <stddef.h>
+#include <assert.h>
+
+typedef void* (*ZSTD_allocFunction) (void* opaque, size_t size);
+typedef void  (*ZSTD_freeFunction) (void* opaque, void* address);
+typedef struct { ZSTD_allocFunction customAlloc; ZSTD_freeFunction customFree; void* opaque; } ZSTD_customMem;
+
+ZSTD_customMem const ZSTD_defaultCMem = { NULL, NULL, NULL };
+
+#define ZSTD_malloc(s) malloc(s)
+
+void* ZSTD_customMalloc(size_t size, ZSTD_customMem customMem)
+{
+    if (customMem.customAlloc) // WARN (dead branch)
+        return customMem.customAlloc(customMem.opaque, size);
+    return ZSTD_malloc(size);
+}
+
+int* ZSTD_createCCtx_advanced(ZSTD_customMem customMem)
+{
+  if ((!customMem.customAlloc) ^ (!customMem.customFree)) // WARN (dead branch)
+    return NULL;
+
+  return ZSTD_customMalloc(sizeof(int), customMem);
+}
+
+int main() {
+  int *p = ZSTD_createCCtx_advanced(ZSTD_defaultCMem);
+  assert(p != NULL);
+  return 0;
+}