Merge pull request #618 from goblint/ldv-races

ldv-benchmarks races benchmarking

conf/ldv-races.json

@@ -0,0 +1,65 @@
+{
+  "pre": {
+    "cppflags": [
+      "-DGOBLINT_NO_PTHREAD_ONCE",
+      "-DGOBLINT_NO_QSORT",
+      "-DGOBLINT_NO_BSEARCH"
+    ]
+  },
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutex",
+      "access",
+      "escape",
+      "expRelation",
+      "mhp"
+    ],
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc"
+      ]
+    }
+  },
+  "witness": {
+    "id": "enumerate",
+    "unknown": false
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    }
+  }
+}

src/analyses/varEq.ml

@@ -401,7 +401,10 @@ struct
       | None -> None
       | Some st ->
         let vs = ask.f (Queries.ReachableFrom e) in
-        Some (Queries.LS.join vs st)
+        if Queries.LS.is_top vs then
+          None
+        else
+          Some (Queries.LS.join vs st)
     in
     List.fold_right reachable es (Some (Queries.LS.empty ()))
 
@@ -495,6 +498,8 @@ struct
         D.B.fold remove_reachable2 es st
       in
       D.fold remove_reachable1 ctx.local ctx.local
+      (* TODO: do something like this instead to be sound? *)
+      (* List.fold_left (fun st e -> remove_exp (Analyses.ask_of_ctx ctx) e st) ctx.local (Queries.LS.fold (fun lval acc -> mkAddrOf (Lval.CilLval.to_lval lval) :: acc) rs []) *)
 
   let unknown_fn ctx lval f args =
     let args =

src/cdomains/apron/apronDomain.apron.ml

@@ -147,11 +147,7 @@ struct
   module Bounds = Bounds(Man)
   exception Unsupported_CilExp
 
-  (* TODO: move this into some general place *)
-  let is_cast_injective from_type to_type =
-    let (from_min, from_max) = IntDomain.Size.range (Cilfacade.get_ikind from_type) in
-    let (to_min, to_max) = IntDomain.Size.range (Cilfacade.get_ikind to_type) in
-    BI.compare to_min from_min <= 0 && BI.compare from_max to_max <= 0
+
 
   let texpr1_expr_of_cil_exp d env =
     (* recurse without env argument *)
@@ -182,7 +178,7 @@ struct
             Binop (Div, texpr1_expr_of_cil_exp e1, texpr1_expr_of_cil_exp e2, Int, Zero)
           | BinOp (Mod, e1, e2, _) ->
             Binop (Mod, texpr1_expr_of_cil_exp e1, texpr1_expr_of_cil_exp e2, Int, Near)
-          | CastE (TInt _ as t, e) when is_cast_injective (Cilfacade.typeOf e) t -> (* TODO: unnecessary cast check due to overflow check below? or maybe useful in general to also assume type bounds based on argument types? *)
+          | CastE (TInt _ as t, e) when IntDomain.Size.is_cast_injective ~from_type:(Cilfacade.typeOf e) ~to_type:t -> (* TODO: unnecessary cast check due to overflow check below? or maybe useful in general to also assume type bounds based on argument types? *)
             Unop (Cast, texpr1_expr_of_cil_exp e, Int, Zero) (* TODO: what does Apron Cast actually do? just for floating point and rounding? *)
           | _ ->
             raise Unsupported_CilExp

src/cdomains/intDomain.ml

@@ -410,6 +410,12 @@ module Size = struct (* size in bits as int, range as int64 *)
     let x = if isSigned ik then minus_big_int (shift_left_big_int unit_big_int a) (* -2^a *) else zero_big_int in
     let y = sub_big_int (shift_left_big_int unit_big_int b) unit_big_int in (* 2^b - 1 *)
     x,y
+
+  let is_cast_injective ~from_type ~to_type =
+    let (from_min, from_max) = range (Cilfacade.get_ikind from_type) in
+    let (to_min, to_max) = range (Cilfacade.get_ikind to_type) in
+    BI.compare to_min from_min <= 0 && BI.compare from_max to_max <= 0
+
   let cast t x = (* TODO: overflow is implementation-dependent! *)
     let a,b = range t in
     let c = card t in

src/cdomains/intDomain.mli

@@ -334,6 +334,7 @@ module Size : sig
   (** The biggest type we support for integers. *)
   val top_typ         : Cil.typ
   val range           : Cil.ikind -> Z.t * Z.t
+  val is_cast_injective : from_type:Cil.typ -> to_type:Cil.typ -> bool
   val bits            : Cil.ikind -> int * int
 end
 

src/cdomains/regionDomain.ml

@@ -201,7 +201,7 @@ struct
   let assign (lval: lval) (rval: exp) (st: t): t =
     (*    let _ = printf "%a = %a\n" (printLval plainCilPrinter) lval (printExp plainCilPrinter) rval in *)
     let t = Cilfacade.typeOf rval in
-    if isPointerType t then begin
+    if isPointerType t then begin (* TODO: this currently allows function pointers, e.g. in iowarrior, but should it? *)
       match eval_exp (Lval lval), eval_exp rval with
       (* TODO: should offs_x matter? *)
       | Some (deref_x, x,offs_x), Some (deref_y,y,offs_y) ->

src/cdomains/valueDomain.ml

@@ -272,7 +272,7 @@ struct
     | TInt (ik,_), TFloat (fk,_) (* does a1 fit into ik's range? *)
     | TFloat (fk,_), TInt (ik,_) (* can a1 be represented as fk? *)
       -> false (* TODO precision *)
-    | _ -> bitsSizeOf t2 >= bitsSizeOf t1
+    | _ -> IntDomain.Size.is_cast_injective ~from_type:t1 ~to_type:t2 && bitsSizeOf t2 >= bitsSizeOf t1
   (*| _ -> false*)
 
   let ptr_ikind () = match !upointType with TInt (ik,_) -> ik | _ -> assert false

src/util/options.schema.json

@@ -1723,6 +1723,12 @@
       "title": "witness",
       "type": "object",
       "properties": {
+        "enabled": {
+          "title": "witness.enabled",
+          "description": "Output witness",
+          "type": "boolean",
+          "default": true
+        },
         "path": {
           "title": "witness.path",
           "description": "Witness output path",

src/witness/witness.ml

@@ -591,7 +591,8 @@ struct
 
     print_task_result (module TaskResult);
 
-    if TaskResult.result <> Result.Unknown || get_bool "witness.unknown" then (
+    (* TODO: use witness.enabled elsewhere as well *)
+    if get_bool "witness.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.unknown") then (
       let witness_path = get_string "witness.path" in
       Stats.time "write" (write_file witness_path (module Task)) (module TaskResult)
     )

tests/regression/06-symbeq/32-var_eq-unknown-invalidate.c

@@ -0,0 +1,25 @@
+// PARAM: --set ana.activated[+] var_eq
+// ldv-benchmarks: u__linux-concurrency_safety__drivers---net---ethernet---ethoc.ko.cil.c
+#include <assert.h>
+
+struct resource {
+   char const *name ;
+   unsigned long flags ;
+   struct resource *parent ;
+   struct resource *sibling ;
+   struct resource *child ;
+};
+
+struct resource *magic();
+
+int main() {
+  struct resource *res = (struct resource *)0;
+  res = magic();
+
+  if (res == (struct resource *)0)
+    assert(1); // reachable
+  else
+    assert(1); // TODO reachable
+
+  return 0;
+}

tests/regression/21-casts/04-neg-to-unsigned-invariant.c

@@ -0,0 +1,14 @@
+// PARAM: --enable ana.int.def_exc --enable ana.int.interval
+// ldv-benchmarks: u__linux-concurrency_safety__drivers---net---ethernet---amd---pcnet32.ko.c
+#include <assert.h>
+
+int main() {
+  int debug_value = -1;
+
+  if ((unsigned int)debug_value > 31U)
+    assert(1); // reachable
+  else
+    assert(1); // NOWARN (unreachable)
+
+  return 0;
+}