Macros redefined in goblint_caml, SplitBranch checks type

Author: Ronald Judin

src/analyses/ocaml.ml

@@ -118,7 +118,7 @@ struct
     | Var v,_ ->
       (* If rval is a pointer, checks whether rval is accounted for, handles assignment to v accordingly *) (* state *)
       (* Emits an event for the variable v not being zero. *)
-      ctx.emit (Events.SplitBranch (Cil.BinOp (Cil.Eq, Cil.Lval lval, Cil.zero, Cil.intType), false));
+
       if Cil.isPointerType (Cil.typeOf rval) then
         if exp_accounted_for state rval then
           if exp_tracked state rval then D.add_a v (D.add_t v state)
@@ -137,7 +137,14 @@ struct
   let body ctx (f:fundec) : D.t =
     (* The (non-formals) locals are tracked and initially accounted for *)
     let state = ctx.local in
-    List.fold_left (fun st v -> D.add_a v (D.add_t v st)) state f.sformals
+    (* It is assumed that value-typed arguments are never nptrs. *)
+    let is_value_type (t:typ): bool = match t with
+      | TNamed (info, attr) -> info.tname = "value"
+      | _ -> false in
+    List.fold_left (fun st v -> if is_value_type v.vtype then
+                       (ctx.emit (Events.SplitBranch (Cil.Lval (Cil.var v), true)); D.add_a v (D.add_t v st))
+                     else D.add_a v (D.add_t 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 =
@@ -205,12 +212,10 @@ struct
     match desc.special arglist with
     | OCamlParam params ->
       (* Variables are registered with a Param macro. Such variables are also tracked. *)
-      List.fold_left (fun state param -> M.debug "We reach here";
-                       match param with
-                       | AddrOf (Var v, _) -> M.debug "Address of";
-                         D.add_r v (D.add_t v state)
-                       | _ -> state
-                     ) caller_state params
+      List.fold_left (fun state param -> match param with
+          | AddrOf (Var v, _) -> D.add_r v (D.add_t v state)
+          | _ -> state
+        ) caller_state params
     | OCamlAlloc size_exp ->
       (* Garbage collection may trigger here and overwrite unregistered variables. *)
       M.debug "Garbage collection triggers";

src/util/library/libraryFunctions.ml

@@ -1245,10 +1245,12 @@ let legacy_libs_misc_list: (string * LibraryDesc.t) list = LibraryDsl.[
 
 let ocaml_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("caml_copy_double", special [drop "nptr" []] (OCamlAlloc (GoblintCil.integer 1)));
-    (* Eeskuju: ("malloc", special [__ "size" []] @@ fun size -> Malloc size); *)
+    (* Example: ("malloc", special [__ "size" []] @@ fun size -> Malloc size); *)
     ("caml_alloc_small", special [__ "wosize" []; __ "tag" []] @@ fun wosize tag -> OCamlAlloc wosize);
-    (* TODO: This specification is not correct because it doesn't warn where it should. Also rethink the argument names. *)
+    ("caml_alloc_2", special [__ "tag" []; __ "arg1" [r]; __ "arg2" [r]] @@ fun tag _arg1 _arg2 -> OCamlAlloc (GoblintCil.integer 2));
     ("caml_alloc_3", special [__ "tag" []; __ "arg1" [r]; __ "arg2" [r]; __ "arg3" [r]] @@ fun tag _arg1 _arg2 _arg3 -> OCamlAlloc (GoblintCil.integer 3));
+    ("caml_alloc_4", special [__ "tag" []; __ "arg1" [r]; __ "arg2" [r]; __ "arg3" [r]; __ "arg4" [r]] @@ fun tag _arg1 _arg2 _arg3 _arg4 -> OCamlAlloc (GoblintCil.integer 4));
+    ("caml_alloc_5", special [__ "tag" []; __ "arg1" [r]; __ "arg2" [r]; __ "arg3" [r]; __ "arg4" [r]; __ "arg5" [r]] @@ fun tag _arg1 _arg2 _arg3 _arg4 _arg5 -> OCamlAlloc (GoblintCil.integer 5));
     ("__goblint_caml_param0", special [] @@ OCamlParam []);
     ("__goblint_caml_param1", special [__ "param" []] @@ fun param -> OCamlParam [param]);
     ("__goblint_caml_param2", special [__ "param1" []; __ "param2" []] @@ fun param1 param2 -> OCamlParam [param1; param2]);

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

@@ -6,19 +6,7 @@
 #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__));*/
+#include "goblint_caml.h"
 
 CAMLprim value pringo_LXM_copy(value v)
 {

tests/regression/90-ocaml/02-floatops.c

@@ -2,17 +2,6 @@
 
 // Code from stubs.c in src/common/cdomains/floatOps that should be correct despite missing CAMLparam, as discussed in https://github.com/goblint/analyzer/issues/1371.
 
-/* 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.
-
-
 #define _GNU_SOURCE // necessary for M_PI to be defined
 #include <stdio.h>
 #include <math.h>
@@ -21,6 +10,7 @@
 #include <assert.h>
 #include <caml/mlvalues.h>
 #include <caml/alloc.h>
+#include "goblint_caml.h"
 
 // Order must match with round_mode in floatOps.ml
 enum round_mode

tests/regression/90-ocaml/03-obenour.c

@@ -1,22 +1,10 @@
 // PARAM: --set "ana.activated[+]" ocaml --set "mainfun[+]" "caml_gc_counters" --set "mainfun[+]" "caml_gc_counters_correct" --disable warn.imprecise --set "exp.extraspecials[+]" printInt
 
-// Buggy code from https://github.com/ocaml/ocaml/pull/13370 where some local variables are not registered.
+// Buggy code from https://github.com/ocaml/ocaml/pull/13370 where unregistered temporary variables may be garbage-collected.
 
 #include <caml/mlvalues.h>
 #include <caml/alloc.h>
-
-/* 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 CAMLparam0() __goblint_caml_param0()
-#define CAMLparam1(x) __goblint_caml_param1(&x)
-#define CAMLlocal1(x) value x = Val_unit; __goblint_caml_param1(&x) // The local and param functions behave the same for our purposes, registering variables.
-#define CAMLlocal3(x, y, z) value x = Val_unit; value y = Val_unit; value z = Val_unit; __goblint_caml_param3(&x, &y, &z)
-#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.
-
-// A reference to caml_gc_minor_words_unboxed can be found in _opam/lib/ocaml/ml/gc.ml.
-#define caml_gc_minor_words_unboxed() (0.0) // TODO: Put a value here that's in the OCaml heap.
+#include "goblint_caml.h"
 
 CAMLprim value caml_gc_counters(value v)
 {
@@ -28,10 +16,9 @@ CAMLprim value caml_gc_counters(value v)
   /*double prowords = (double)Caml_state->stat_promoted_words;
   double majwords = Caml_state->stat_major_words +
                     (double) Caml_state->allocated_words;*/
-  double prowords = v; // It does not find the Caml_state so dummy values are used for the test. The argument v, which is otherwise unused, is used as the dummy value because it allows for simulating the variables' registration.
-  double majwords = v;
+  double prowords = 0; // It does not find the Caml_state so dummy values are used for the test.
+  double majwords = 0;
 
-  // Evaluating one argument could erase the next variables.
   res = caml_alloc_3(0,
     caml_copy_double(minwords),
     caml_copy_double(prowords),

tests/regression/90-ocaml/goblint_caml.h

@@ -0,0 +1,27 @@
+/* Redefinitions of caml macros for the C-stub analysis. This file replaces caml/memory.h in tests' imports. */
+
+/* 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))
+
+// Param and local macros redefined to register variables as GC roots, and CAMLreturn mocked to work with them.
+#define CAMLparam0() __goblint_caml_param0()
+#define CAMLparam1(x) __goblint_caml_param1(&x)
+#define CAMLparam2(x, y) __goblint_caml_param2(&x, &y)
+#define CAMLparam3(x, y, z) __goblint_caml_param3(&x, &y, &z)
+#define CAMLparam4(x, y, z, w) __goblint_caml_param4(&x, &y, &z, &w)
+#define CAMLparam5(x, y, z, w, v) __goblint_caml_param5(&x, &y, &z, &w, &v)
+
+#define CAMLlocal1(x) value x = Val_unit; __goblint_caml_param1(&x) // The local and param functions behave the same for our purposes, registering variables.
+#define CAMLlocal2(x, y) value x = Val_unit; value y = Val_unit; __goblint_caml_param2(&x, &y)
+#define CAMLlocal3(x, y, z) value x = Val_unit; value y = Val_unit; value z = Val_unit; __goblint_caml_param3(&x, &y, &z)
+#define CAMLlocal4(x, y, z, w) value x = Val_unit; value y = Val_unit; value z = Val_unit; value w = Val_unit; __goblint_caml_param4(&x, &y, &z, &w)
+#define CAMLlocal5(x, y, z, w, v) value x = Val_unit; value y = Val_unit; value z = Val_unit; value w = Val_unit; value v = Val_unit; __goblint_caml_param5(&x, &y, &z, &w, &v)
+
+#define CAMLreturn(x) return (x) // The real CAMLreturn needs some variable named caml__frame, which is not available in our redefinitions above.
+
+// A reference to caml_gc_minor_words_unboxed can be found in _opam/lib/ocaml/ml/gc.ml.
+#define caml_gc_minor_words_unboxed() (0.0)