Added separate function for everything assignment-like, distinguished between regular and correct returns, added apron test

Author: Ronald Judin

src/analyses/ocaml.ml

@@ -13,7 +13,9 @@ module VarinfoSet = SetDomain.Make(CilType.Varinfo)
 (** "Fake" variable to handle returning from a function *)
 let return_varinfo = dummyFunDec.svar
 (** Flag for first function entered *)
-let first_function = true
+let first_function = (emptyFunction "@first").svar
+(** Flag for deregistering at return *)
+let to_deregister = (emptyFunction "@dereg").svar
 
 module Spec : Analyses.MCPSpec =
 struct
@@ -106,22 +108,22 @@ struct
     | TNamed (info, attr) -> info.tname = "value"
     | _ -> false
 
+  let assignment (v:varinfo) (rval:exp) (state:D.t) (warning:string): D.t =
+    (* If rval is a pointer, checks whether rval is accounted for, handles assignment to v accordingly *)    
+    if Cil.isPointerType (Cil.typeOf rval) || is_value_type (Cil.typeOf rval) then
+      if exp_accounted_for state rval then
+        if exp_registered state rval then D.add_a v (D.add_r v state)
+        else D.add_a v (D.remove_r v state)
+      else (M.info "%s" warning; D.remove_a v state)
+    else D.add_a v (D.add_r v state)
+
   (* 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 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. *)
-
-      if Cil.isPointerType (Cil.typeOf rval) || is_value_type (Cil.typeOf rval) then
-        if exp_accounted_for state rval then
-          if exp_registered state rval then D.add_a v (D.add_r v state)
-          else D.add_a v (D.remove_r v state)
-        else (M.info "The above is being assigned"; D.remove_a v state)
-      else D.add_a v (D.add_r v state)
+    | Var v,_ -> assignment v rval state "The above is being assigned"
     | _ -> state
 
   (** Handles conditional branching yielding truth value [tv]. *)
@@ -133,16 +135,14 @@ struct
   (** 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
-    (* It is assumed that the startstate's values are not nptrs. *)
-    let state = List.fold_left (fun st v -> if first_function && is_value_type v.vtype then
-                       (ctx.emit (Events.SplitBranch (Cil.Lval (Cil.var v), true)); D.add_a v st)
-                     else D.add_a v (D.add_r v st))
-      state f.sformals in
+    (* It is assumed that the startstate's values are not nptrs. This avoids warnings from other analyses. *)
+    if D.mem_r first_function state then
+      List.iter (fun v -> (if is_value_type v.vtype then
+                             (ctx.emit (Events.SplitBranch (Cil.Lval (Cil.var v), true)))))
+        f.sformals;
     (* TODO: Is there a way without a flag to only emit at the start? *)
-    let first_function = false in
-    state
+    D.remove_r first_function state
 
   (** Handles the [return] statement, i.e. "return exp" or "return", in function [f]. *)
   let return ctx (exp:exp option) (f:fundec) : D.t =
@@ -151,17 +151,11 @@ struct
     | Some e ->
       (* Checks that value returned is accounted for. *)
       (* Return_varinfo is used in place of a "real" variable. *)
-      (* TODO: Consider how the return_varinfo needs to be tracked. *)
-      let return_state =
-        if Cil.isPointerType (Cil.typeOf e) || is_value_type (Cil.typeOf e) then
-          if exp_accounted_for state e then
-            if exp_registered state e then D.add_a return_varinfo (D.add_r return_varinfo state)
-            else D.add_a return_varinfo (D.remove_r return_varinfo state)
-          else (M.warn "Value returned might be garbage collected"; D.remove_a return_varinfo state)
-        else D.add_a return_varinfo (D.add_r return_varinfo state)
-      in
-      (* Remove this function's formals and locals *)
-      List.fold_left (fun st v -> D.remove_a v (D.remove_r v st)) return_state (f.sformals @ f.slocals)
+      let return_state = assignment return_varinfo e state "The above is being returned" in
+      (* Remove this function's formals and locals if correctly returned *)
+      D.remove_r to_deregister (if D.mem_r to_deregister return_state then
+                                  List.fold_left (fun st v -> D.remove_a v (D.remove_r v st)) return_state (f.sformals @ f.slocals)
+                                else return_state)
     | None -> state
 
   (** For a function call "lval = f(args)" or "f(args)",
@@ -173,16 +167,13 @@ struct
     List.iter (fun e -> ignore (exp_accounted_for caller_state e)) args;
     (* Entering a function doesn't change the caller state *)
     let callee_state = List.fold_left2 (fun st v rval ->
-      (* At the start, arguments are accounted for and not registered. *)
-      if rval == MyCFG.unknown_exp then D.add_a v (D.remove_r v st) else
-      (* Arguments of inner functions inherit the caller's state. *)
-      if Cil.isPointerType (Cil.typeOf rval) || is_value_type (Cil.typeOf rval) then
-        if exp_accounted_for st rval then
-          if exp_registered st rval then D.add_a v (D.add_r v st)
-          else D.add_a v (D.remove_r v st)
-        else (M.info "The above is being assigned"; D.remove_a v st)
-      else D.add_a v (D.add_r v st))
-      caller_state f.sformals args in
+        (* At the start, arguments are accounted for and not registered. The first_function flag is added.*)
+        if rval == MyCFG.unknown_exp then
+          if is_value_type v.vtype then D.add_r first_function (D.add_a v (D.remove_r v st))
+          else D.add_a v (D.add_r v st)
+          (* Arguments of inner functions inherit the caller's state. *)
+        else assignment v rval st "Entering function with possibly deleted argument")
+        caller_state f.sformals args in
     (* first component is state of caller, second component is state of callee *)
     [caller_state, callee_state]
 
@@ -201,15 +192,15 @@ struct
     let caller_state = ctx.local in
     (* Records whether lval was accounted for. Registration for v must already be handled. *)
     (* TODO: What happens if a pointer to a value is returned? *)
-    (* TODO: Rethink type checking with return_varinfo. *)
     match lval with (* The variable returned is played by return_varinfo *)
     | Some (Var v, _) ->
       let state =
-        if Cil.isPointerType return_varinfo.vtype || is_value_type return_varinfo.vtype then
-          if D.mem_a return_varinfo callee_local then
-            if D.mem_r return_varinfo callee_local then D.add_a v (D.add_r v caller_state)
+        (* TODO: It never warns about being combined. Is there a problem with the svar type? *)
+        if Cil.isPointerType f.svar.vtype || is_value_type f.svar.vtype then
+          if D.mem_a return_varinfo caller_state then
+            if D.mem_r return_varinfo caller_state then D.add_a v (D.add_r v caller_state)
             else D.add_a v (D.remove_r v caller_state)
-          else (M.warn "Returned value may be garbage-collected"; D.remove_a v caller_state)
+          else (M.info "The above is being combined"; D.remove_a v caller_state)
         else D.add_a v (D.add_r v caller_state) in
       D.remove_a return_varinfo (D.remove_r return_varinfo state)
     | _ -> caller_state
@@ -219,7 +210,6 @@ struct
       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
@@ -238,6 +228,10 @@ struct
        | Some (Var v, _) -> D.add_a v (D.after_gc caller_state)
        | _ -> D.after_gc caller_state
       )
+    (* TODO: Does not deregister, but queues it. This is unsound if deregistration is done before returning instead of at the same time. *)
+    | OCamlReturn ->
+      (* Marks a function as deregistering at return *)
+      D.add_r to_deregister caller_state
     | _ -> caller_state
 
   (* You may leave these alone *)

src/util/library/libraryDesc.ml

@@ -50,6 +50,7 @@ type special =
   | OCamlAlloc of Cil.exp
   (* TODO: Rethink OCamlParam's placement. *)
   | OCamlParam of Cil.exp list
+  | OCamlReturn
   | 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

@@ -1247,6 +1247,7 @@ let ocaml_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("caml_copy_double", special [drop "nptr" []] (OCamlAlloc (GoblintCil.integer 1)));
     (* Example: ("malloc", special [__ "size" []] @@ fun size -> Malloc size); *)
     ("caml_alloc_small", special [__ "wosize" []; __ "tag" []] @@ fun wosize tag -> OCamlAlloc wosize);
+    ("camlidl_apron_policy_ptr_c2ml", special [drop "nptr" []] (OCamlAlloc (GoblintCil.integer 1)));
     ("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));
@@ -1257,6 +1258,7 @@ let ocaml_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__goblint_caml_param3", special [__ "param1" []; __ "param2" []; __ "param3" []] @@ fun param1 param2 param3 -> OCamlParam [param1; param2; param3]);
     ("__goblint_caml_param4", special [__ "param1" []; __ "param2" []; __ "param3" []; __ "param4" []] @@ fun param1 param2 param3 param4 -> OCamlParam [param1; param2; param3; param4]);
     ("__goblint_caml_param5", special [__ "param1" []; __ "param2" []; __ "param3" []; __ "param4" []; __ "param5" []] @@ fun param1 param2 param3 param4 param5 -> OCamlParam [param1; param2; param3; param4; param5]);
+    ("__goblint_caml_return", special [] @@ OCamlReturn);
   ]
 [@@coverage off]
 

tests/regression/90-ocaml/05-lateparam.c

@@ -1,6 +1,7 @@
 // PARAM: --set "ana.activated[+]" ocaml --disable warn.imprecise --set "exp.extraspecials[+]" printInt
 
 // Artificial test where the argument v is registered after GC could delete it.
+// TODO: Add late local as well.
 
 #include <stdint.h>
 #include <string.h>

tests/regression/90-ocaml/06-nested.c

@@ -29,7 +29,7 @@ CAMLprim value pringo_LXM_copy_1(value v)
 { 
   value res = caml_alloc_small(Wsizeof(struct LXM_state), Abstract_tag);
   memcpy(LXM_val(res), LXM_val(v), sizeof(struct LXM_state)); // WARN
-  return v;
+  return v; // WARN
 }
 
 CAMLprim value pringo_LXM_copy_2(value v)
@@ -41,6 +41,14 @@ CAMLprim value pringo_LXM_copy_2(value v)
   CAMLreturn(res);
 }
 
+CAMLprim value pringo_LXM_copy_3(value v)
+{
+  value res = caml_alloc_small(Wsizeof(struct LXM_state), Abstract_tag);
+  value r = pringo_LXM_copy_1(v); // WARN
+  memcpy(LXM_val(res), LXM_val(r), sizeof(struct LXM_state));
+  CAMLreturn(res);
+}
+
 CAMLprim value pringo_LXM_init_unboxed(uint64_t i1, uint64_t i2,
                                        uint64_t i3, uint64_t i4)
 {

tests/regression/90-ocaml/07-apron.c

@@ -0,0 +1,54 @@
+// PARAM: --set "ana.activated[+]" ocaml --disable warn.imprecise --set "exp.extraspecials[+]" printInt
+
+// Buggy code from https://github.com/antoinemine/apron/pull/112 where v and v2 are initialised as 0.
+// TODO: It should warn when a value initialised as 0 is used without being registered after a garbage collection.
+
+#include <stdint.h>
+#include <string.h>
+#include <caml/mlvalues.h>
+#include <caml/alloc.h>
+#include <caml/memory.h>
+#include "goblint_caml.h"
+
+// In place of value, it was ap_policy_optr*.
+CAMLprim value camlidl_apron_policy_optr_c2ml(value p)
+{
+  if (p==NULL){
+    return Val_int(0);
+  } else {
+    value v,v2=0;
+    Begin_roots1(v2);
+    v2 = camlidl_apron_policy_ptr_c2ml(p);
+    v = caml_alloc_small(1,0);
+    Field(v,0) = v2;
+    End_roots();
+    return v;
+  }
+}
+
+CAMLprim value camlidl_apron_policy_optr_c2ml_correct(value p)
+{
+  if (p==NULL){
+    return Val_int(0);
+  } else {
+    value v,v2 = Val_unit;
+    Begin_roots1(v2);
+    v2 = camlidl_apron_policy_ptr_c2ml(p);
+    v = caml_alloc_small(1,0);
+    Field(v,0) = v2;
+    End_roots();
+    return v;
+  }
+}
+
+
+// This function basically allocates memory with caml_alloc_custom and is simulated with OCamlParam in libraryfunctions.ml.
+/*CAMLprim value camlidl_apron_policy_ptr_c2ml(ap_policy_ptr* p)
+{
+  value v;
+  assert((*p)->pman!=NULL);
+  v = caml_alloc_custom(&camlidl_apron_custom_policy_ptr, sizeof(ap_policy_ptr),
+		   0,1);
+  *((ap_policy_ptr *) Data_custom_val(v)) = *p;
+  return v;
+}*/

tests/regression/90-ocaml/goblint_caml.h

@@ -37,7 +37,13 @@ struct LXM_state { uint64_t a; uint64_t x[2]; uint64_t s; };
 #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)
 
 #undef CAMLreturn
-#define CAMLreturn(x) return (x) // The real CAMLreturn needs some variable named caml__frame, which is not available in our redefinitions above.
+#define CAMLreturn(x) __goblint_caml_return(); return (x) // The real CAMLreturn needs some variable named caml__frame, which is not available in our redefinitions above.
+
+// Marking roots is like registering and deregistering them.
+#undef Begin_roots1
+#undef End_roots
+#define Begin_roots1(x) __goblint_caml_param1(&x)
+#define End_roots() __goblint_caml_return()
 
 // 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)