OCaml C-stub analysis

Author: Ronald Judin

src/analyses/base.ml

@@ -2736,6 +2736,29 @@ struct
           set_many ~man st ((eval_lv ~man st lv, (Cilfacade.typeOfLval lv), VD.Address addr) :: blob_set)
         | _ -> st
       end
+    | OCamlAlloc wosize, _ ->
+      (*begin match lv with
+        | Some lv ->
+          let heap_var = AD.unknown_ptr (*AD.of_var (heap_var false ctx)*) in
+          let sizeval = eval_int ~ctx st wosize in
+          set_many ~ctx st [
+            (heap_var, TVoid [], Blob (VD.bot (), sizeval, true));
+            (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address heap_var)
+          ]
+        | _ -> st
+        end*)
+      let open Queries.AllocationLocation in
+      begin
+        (* The behavior for alloc(0) is implementation defined. Here, we rely on the options specified for the malloc also applying to alloca. *)
+        match lv with
+        | Some lv ->
+          let loc = Heap in
+          let (heap_var, addr) = alloc loc wosize in
+          (* ignore @@ printf "alloca will allocate %a bytes\n" ID.pretty (eval_int ~man size); *)
+          let blob_set = Option.map_default (fun heap_var -> [(heap_var, TVoid [], VD.Blob (VD.bot (), eval_int ~man st wosize, ZeroInit.malloc))]) [] heap_var in
+          set_many ~man st ((eval_lv ~man st lv, (Cilfacade.typeOfLval lv), VD.Address addr) :: blob_set)
+        | _ -> st
+      end
     | Calloc { count = n; size }, _ ->
       begin match lv with
         | Some lv -> (* array length is set to one, as num*size is done when turning into `Calloc *)

src/analyses/ocaml.ml

@@ -0,0 +1,203 @@
+(** Simple interprocedural analysis of OCaml C-stubs ([ocaml]). *)
+
+(* Goblint documentation: https://goblint.readthedocs.io/en/latest/ *)
+(* Helpful link on CIL: https://goblint.github.io/cil/ *)
+(* TODO: Write tests and test them with `ruby scripts/update_suite.rb group ocaml` *)
+(* after removing the `SKIP` from the beginning of the tests in tests/regression/90-ocaml/{01-bagnall.c,04-o_inter.c} *)
+
+open GoblintCil
+open Analyses
+
+module VarinfoSet = SetDomain.Make(CilType.Varinfo)
+
+(* Use to check if a specific function is a sink / source *)
+(* Sources take value-typed arguments *)
+(* Sinks may trigger garbage collection *)
+let is_sink varinfo = Cil.hasAttribute "ocaml_sink" varinfo.vattr
+let is_source varinfo = Cil.hasAttribute "ocaml_source" varinfo.vattr
+
+
+(** "Fake" variable to handle returning from a function *)
+let return_varinfo = dummyFunDec.svar
+
+module Spec : Analyses.MCPSpec =
+struct
+  include Analyses.DefaultSpec
+
+  let name () = "ocaml"
+  module D =
+  struct
+    (* The first set contains variables of type value that are definitely in order. The second contains definitely registered variables. *)
+    module P = Lattice.Prod (VarinfoSet) (VarinfoSet)
+    include P
+
+    let empty () = (VarinfoSet.empty (), VarinfoSet.empty ())
+
+    (* After garbage collection, the second set is written to the first set *)
+    let after_gc (accounted, registered) = (registered, registered)
+
+    let mem_a v (accounted, registered) =
+      VarinfoSet.mem v accounted
+
+    let mem_r v (accounted, registered) =
+      VarinfoSet.mem v registered
+
+    let add_a v (accounted, registered) =
+      (VarinfoSet.add v accounted, registered)
+
+    let add_r v (accounted, registered) =
+      (accounted, VarinfoSet.add v registered)
+
+    let remove_a v (accounted, registered) =
+      (VarinfoSet.remove v accounted, registered)
+
+    let remove_r v (accounted, registered) =
+      (accounted, VarinfoSet.remove v registered)
+  end
+  module C = Printable.Unit
+
+  (* We are context insensitive in this analysis *)
+  let context ctx _ _ = ()
+  let startcontext () = ()
+
+
+  (** Determines whether an expression [e] is healthy, given a [state]. *)
+  let rec exp_accounted_for (state:D.t) (e:Cil.exp) = match e with
+    (* Recurse over the structure in the expression, returning true if all varinfo appearing in the expression is accounted for *)
+    | AddrOf v
+    | StartOf v
+    | Lval v -> lval_accounted_for state v
+    | BinOp (_,e1,e2,_) -> exp_accounted_for state e1 && exp_accounted_for state e2
+    | Real e
+    | Imag e
+    | SizeOfE e
+    | AlignOfE e
+    | CastE (_,e)
+    | UnOp (_,e,_) -> exp_accounted_for state e
+    | SizeOf _ | SizeOfStr _ | Const _  | AlignOf _ | AddrOfLabel _ -> false
+    | Question (b, t, f, _) -> exp_accounted_for state b && exp_accounted_for state t && exp_accounted_for state f
+  and lval_accounted_for state = function
+    | (Var v, _) ->
+      (* Checks whether variable v is accounted for *) (*false*)
+      if D.mem_a v state then true else let _ = M.warn "Value %a might be garbage collected" CilType.Varinfo.pretty v in false
+    | _ ->
+      (* The Gemara asks: is using an offset safe for the expression? The Gemara answers: by default, no. We assume our language has no pointers *)
+      false
+
+  (* transfer functions *)
+
+  (** Handles assignment of [rval] to [lval]. *)
+  let assign ctx (lval:lval) (rval:exp) : D.t =
+    let state = ctx.local in
+    match lval with
+    | Var v,_ ->
+      (* If lval is of type value, checks whether rval is accounted for, handles assignment to v accordingly *) (* state *)
+      if exp_accounted_for state rval then D.add_a v state
+      else D.remove_a v state
+    | _ -> state
+
+  (** Handles conditional branching yielding truth value [tv]. *)
+  let branch ctx (exp:exp) (tv:bool) : D.t =
+    (* Nothing needs to be done *)
+    ctx.local
+
+  (** Handles going from start node of function [f] into the function body of [f].
+      Meant to handle e.g. initializiation of local variables. *)
+  let body ctx (f:fundec) : D.t =
+    (* The (non-formals) locals are initially accounted for *)
+    let state = ctx.local in
+    List.fold_left (fun st v -> D.add_a v st) state f.sformals
+
+  (** Handles the [return] statement, i.e. "return exp" or "return", in function [f]. *)
+  let return ctx (exp:exp option) (f:fundec) : D.t =
+    let state = ctx.local in
+    match exp with
+    | Some e ->
+      (* Checks that value returned is accounted for. *)
+      (* Return_varinfo is used in place of a "real" variable. *)
+      (* state *)
+      if exp_accounted_for state e then D.add_a return_varinfo state
+      else let _ = M.warn "Value returned might be garbage collected" in D.remove_a return_varinfo state
+    | None -> state
+
+  (** For a function call "lval = f(args)" or "f(args)",
+      [enter] returns a caller state, and the initial state of the callee.
+      In [enter], the caller state can usually be returned unchanged, as [combine_env] and [combine_assign] (below)
+      will compute the caller state after the function call, given the return state of the callee. *)
+  let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+    let caller_state = ctx.local in
+    (* Create list of (formal, actual_exp)*)
+    (*
+    let zipped = List.combine f.sformals args in
+    (* TODO: For the initial callee_state, collect formal parameters where the actual is healthy. *)
+    let callee_state = List.fold_left (fun ts (f,a) ->
+        if exp_accounted_for caller_state a
+        then D.add f ts (* TODO: Change accumulator ts here? *)
+        else D.remove f ts)
+        (D.bot ())
+        zipped in
+    *)
+    (* TODO: Should this be checked with locals or formals, and how exactly? Likely with locals. *)
+    let callee_state = caller_state in
+    (* first component is state of caller, second component is state of callee *)
+    [caller_state, callee_state]
+
+  (** For a function call "lval = f(args)" or "f(args)",
+      computes the global environment state of the caller after the call.
+      Argument [callee_local] is the state of [f] at its return node. *)
+  let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
+    (* Nothing needs to be done *)
+    ctx.local
+
+  (** For a function call "lval = f(args)" or "f(args)",
+      computes the state of the caller after assigning the return value from the call.
+      Argument [callee_local] is the state of [f] at its return node. *)
+  let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
+    let caller_state = ctx.local in
+    (* Records whether lval was accounted for. *) (* caller_state *)
+    match lval with (* The variable returned is played by return_varinfo *)
+    | Some (Var v, _) -> if D.mem_a return_varinfo callee_local then D.add_a v caller_state
+      else let _ = M.warn "Returned value may be garbage-collected" in D.remove_a v caller_state
+    | _ -> caller_state
+
+  (** For a call to a _special_ function f "lval = f(args)" or "f(args)",
+      computes the caller state after the function call.
+      For this analysis, source and sink functions will be considered _special_ and have to be treated here. *)
+  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let caller_state = ctx.local in
+    (* TODO: Check if f is a sink / source and handle it appropriately *)
+    (* To warn about a potential issue in the code, use M.warn. *)
+    (* caller_state *)
+    let desc = LibraryFunctions.find f in
+    match desc.special arglist with
+    (* TODO: Add a source function that registers variables and add the non-buggy Bagnall code to the test. *)
+    | OCamlAlloc size_exp ->
+      (* Garbage collection may trigger here and overwrite unregistered variables *)
+      let _ = M.info "Garbage collection triggers" in (match lval with
+          | Some (Var v, _) -> D.add_a v (D.after_gc caller_state)
+          | _ ->
+            (* if not (List.for_all (exp_accounted_for caller_state) arglist) then let _ = M.warn "GC might delete value" in D.empty () else *) D.empty ()
+        )
+    | _ ->
+      List.iter (fun e -> ignore (exp_accounted_for caller_state e)) arglist; (* Just to trigger warnings for arguments passed to sinks/sources *)
+      if is_source f then match lval with (* Assigning the source's result makes the variable accounted for. *)
+        | Some (Var v, _) -> D.add_a v caller_state
+        | _ -> caller_state
+      else
+      if is_sink f then (* Warns if unaccounted variables reach the function. Empties the state of unregistered variables. *)
+        let _ = M.info "Garbage collection triggers" in match lval with
+        | Some (Var v, _) -> D.add_a v (D.after_gc caller_state)
+        | _ ->
+          (* if not (List.for_all (exp_accounted_for caller_state) arglist) then let _ = M.warn "GC might delete value" in D.empty () else *)
+          D.after_gc caller_state
+      else caller_state
+
+  (* You may leave these alone *)
+  let startstate v = D.bot ()
+  let threadenter ctx ~multiple lval f args = [D.top ()]
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
+  let exitstate  v = D.top ()
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)

src/config/options.schema.json

@@ -1501,7 +1501,8 @@
               "pcre",
               "zlib",
               "liblzma",
-              "legacy"
+              "legacy",
+              "ocaml"
             ]
           },
           "default": [
@@ -1513,7 +1514,8 @@
             "linux-userspace",
             "goblint",
             "ncurses",
-            "legacy"
+            "legacy",
+            "ocaml"
           ]
         }
       },

src/util/library/libraryDesc.ml

@@ -47,6 +47,7 @@ type math =
 type special =
   | Alloca of Cil.exp
   | Malloc of Cil.exp
+  | OCamlAlloc of Cil.exp
   | Calloc of { count: Cil.exp; size: Cil.exp; }
   | Realloc of { ptr: Cil.exp; size: Cil.exp; }
   | Free of Cil.exp

src/util/library/libraryFunctions.ml

@@ -1242,6 +1242,13 @@ let legacy_libs_misc_list: (string * LibraryDesc.t) list = LibraryDsl.[
   ]
 [@@coverage off]
 
+let ocaml_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+    ("caml_copy_double", unknown [drop "nptr" []]);
+    (* Eeskuju: ("malloc", special [__ "size" []] @@ fun size -> Malloc size); *)
+    ("caml_alloc_small", special [__ "wosize" []; __ "tag" []] @@ fun wosize tag -> OCamlAlloc wosize);
+  ]
+[@@coverage off]
+
 let libraries = Hashtbl.of_list [
     ("c", c_descs_list @ math_descs_list);
     ("posix", posix_descs_list);
@@ -1259,6 +1266,7 @@ let libraries = Hashtbl.of_list [
     ("zlib", zlib_descs_list);
     ("liblzma", liblzma_descs_list);
     ("legacy", legacy_libs_misc_list);
+    ("ocaml", ocaml_descs_list)
   ]
 
 let libraries =

tests/regression/90-ocaml/01-bagnall.c

@@ -0,0 +1,50 @@
+// PARAM: --set "ana.activated[+]" ocaml --set "mainfun[+]" "pringo_LXM_copy" --set "mainfun[+]" "pringo_LXM_copy_correct" --set "mainfun[+]" "pringo_LXM_init_unboxed" --disable warn.imprecise --set "exp.extraspecials[+]" printInt
+
+// Buggy code from https://github.com/xavierleroy/pringo/issues/6 where value v is not registered.
+
+// putchar from the standard library is marked as a sink
+
+#include <stdint.h>
+#include <string.h>
+#include <caml/mlvalues.h>
+#include <caml/alloc.h>
+#include <caml/memory.h>
+
+/* A small definition of the LXM state so sizeof works - from AI */
+struct LXM_state { uint64_t a; uint64_t x[2]; uint64_t s; };
+
+/* Minimal macros to mimic expected behaviour */
+#define Wsizeof(ty) ((sizeof(ty) + sizeof(value) - 1) / sizeof(value))
+#define LXM_val(v) ((struct LXM_state *) Data_abstract_val(v))
+
+#define CAMLparam1(x) __goblint_caml_param1(&x)
+#define CAMLreturn(x) return (x) // From AI - CAMLreturn needs some variable named caml__frame, which is not available in our mock CAMLparam1, so we mock the return as well.
+
+/*CAMLextern value caml_alloc_small (mlsize_t wosize, tag_t)  __attribute__((__ocaml_sink__));*/
+
+CAMLprim value pringo_LXM_copy(value v)
+{
+  value res = caml_alloc_small(Wsizeof(struct LXM_state), Abstract_tag);
+  memcpy(LXM_val(res), LXM_val(v), sizeof(struct LXM_state));
+  return res;
+}
+
+CAMLprim value pringo_LXM_copy_correct(value v)
+{
+  CAMLparam1(v);
+  value res = caml_alloc_small(Wsizeof(struct LXM_state), Abstract_tag);
+  memcpy(LXM_val(res), LXM_val(v), sizeof(struct LXM_state));
+  CAMLreturn(res);
+}
+
+CAMLprim value pringo_LXM_init_unboxed(uint64_t i1, uint64_t i2,
+                                       uint64_t i3, uint64_t i4)
+{
+  value v = caml_alloc_small(Wsizeof(struct LXM_state), Abstract_tag);
+  struct LXM_state * st = LXM_val(v);
+  st->a = i1 | 1;    /* must be odd */
+  st->x[0] = i2 != 0 ? i2 : 1; /* must be nonzero */
+  st->x[1] = i3 != 0 ? i3 : 2; /* must be nonzero */
+  st->s = i4;
+  return v;
+}