Deleted is_sink and is_source, added checking for pointers, added tracking and warning to special, experimented with SplitBranch

Author: Ronald Judin

src/analyses/ocaml.ml

@@ -10,13 +10,6 @@ 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
 
@@ -84,12 +77,12 @@ struct
     | AlignOfE e
     | CastE (_,e)
     | UnOp (_,e,_) -> exp_accounted_for state e
-    | SizeOf _ | SizeOfStr _ | Const _  | AlignOf _ | AddrOfLabel _ -> false
+    | SizeOf _ | SizeOfStr _ | Const _  | AlignOf _ | AddrOfLabel _ -> true
     | 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 || not (D.mem_t v state) then true else let _ = M.warn "Value %a might be garbage collected" CilType.Varinfo.pretty v in false
+      if D.mem_a v state || not (D.mem_t v state) then true else (M.warn "Value %a might be garbage collected" CilType.Varinfo.pretty v; 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
@@ -123,11 +116,15 @@ struct
     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
-        if exp_tracked state rval then D.add_a v (D.add_t v state)
-        else D.add_a v (D.remove_t v state)
-      else let _ = M.info "The above is being assigned" in D.remove_a v (D.add_t v state)
+      (* 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)
+          else D.add_a v (D.remove_t v state) (* TODO: Is add_a necessary for untracked variables? *)
+        else (M.info "The above is being assigned"; D.remove_a v (D.add_t v state))
+      else D.remove_t v state
     | _ -> state
 
   (** Handles conditional branching yielding truth value [tv]. *)
@@ -152,7 +149,7 @@ struct
       (* TODO: Consider how the return_varinfo needs to be tracked. *)
       (* 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
+      else (M.warn "Value returned might be garbage collected"; D.remove_a return_varinfo state)
     | None -> state
 
   (** For a function call "lval = f(args)" or "f(args)",
@@ -193,7 +190,7 @@ struct
     (* TODO: Consider how the return_varinfo needs to be tracked. *)
     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
+      else (M.warn "Returned value may be garbage-collected"; D.remove_a v caller_state)
     | _ -> caller_state
 
   (** For a call to a _special_ function f "lval = f(args)" or "f(args)",
@@ -206,34 +203,25 @@ struct
     (* caller_state *)
     let desc = LibraryFunctions.find f in
     match desc.special arglist with
-    (* Variables are registered with a Param macro. *)
     | OCamlParam params ->
-      List.fold_left (fun state param -> let _ = M.info "We reach here" in
+      (* 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, _) -> let _ = M.info "Address of" in
-                         D.add_r v state
+                       | AddrOf (Var v, _) -> M.debug "Address of";
+                         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 *)
-      let _ = M.debug "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 ()
-        )
+      (* Garbage collection may trigger here and overwrite unregistered variables. *)
+      M.debug "Garbage collection triggers";
+      List.iter (fun e -> ignore (exp_accounted_for caller_state e)) arglist; (* Just to trigger warnings *)
+      (match lval with
+       | Some (Var v, _) -> D.add_a v (D.add_t v (D.after_gc caller_state))
+       | _ -> D.after_gc caller_state
+      )
     | _ ->
-      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.debug "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
+      List.iter (fun e -> ignore (exp_accounted_for caller_state e)) arglist; (* Just to trigger warnings for arguments passed to special functions *)
+      caller_state
 
   (* You may leave these alone *)
   let startstate v = D.bot ()

src/util/library/libraryFunctions.ml

@@ -1247,6 +1247,8 @@ 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); *)
     ("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_3", special [__ "tag" []; __ "arg1" [r]; __ "arg2" [r]; __ "arg3" [r]] @@ fun tag _arg1 _arg2 _arg3 -> OCamlAlloc (GoblintCil.integer 3));
     ("__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/03-demimarie.c tests/regression/90-ocaml/03-obenour.ctests/regression/90-ocaml/03-demimarie.c renamed to tests/regression/90-ocaml/03-obenour.c

@@ -1,6 +1,6 @@
 // PARAM: --set "ana.activated[+]" ocaml --set "mainfun[+]" "caml_gc_counters" --set "mainfun[+]" "caml_gc_counters_correct" --disable warn.imprecise --set "exp.extraspecials[+]" printInt
 
-// OCaml code fixed by Demi Marie Obenour in https://github.com/ocaml/ocaml/pull/13370, before and after the fix.
+// Buggy code from https://github.com/ocaml/ocaml/pull/13370 where some local variables are not registered.
 
 #include <caml/mlvalues.h>
 #include <caml/alloc.h>
@@ -11,10 +11,12 @@
 
 #define CAMLparam0() __goblint_caml_param0()
 #define CAMLparam1(x) __goblint_caml_param1(&x)
-#define CAMLlocal1(x) __goblint_caml_param1(&x) // The local and param functions behave the same for our purposes, registering variables.
-#define CAMLlocal3(x, y, z) __goblint_caml_param3(&x, &y, &z)
+#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.
 
 CAMLprim value caml_gc_counters(value v)
 {
@@ -23,10 +25,13 @@ CAMLprim value caml_gc_counters(value v)
 
   /* get a copy of these before allocating anything... */
   double minwords = caml_gc_minor_words_unboxed();
-  double prowords = (double)Caml_state->stat_promoted_words;
+  /*double prowords = (double)Caml_state->stat_promoted_words;
   double majwords = Caml_state->stat_major_words +
-                    (double) Caml_state->allocated_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;
 
+  // Evaluating one argument could erase the next variables.
   res = caml_alloc_3(0,
     caml_copy_double(minwords),
     caml_copy_double(prowords),
@@ -41,9 +46,11 @@ CAMLprim value caml_gc_counters_correct(value v)
 
   /* get a copy of these before allocating anything... */
   double minwords = caml_gc_minor_words_unboxed();
-  double prowords = (double)Caml_state->stat_promoted_words;
+  /*double prowords = (double)Caml_state->stat_promoted_words;
   double majwords = Caml_state->stat_major_words +
-                    (double) Caml_state->allocated_words;
+                    (double) Caml_state->allocated_words;*/
+  double prowords = 0;
+  double majwords = 0;
 
   minwords_ = caml_copy_double(minwords);
   prowords_ = caml_copy_double(prowords);