Merge branch 'master' into master

conf/svcomp-ghost.json

@@ -81,7 +81,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp-validate.json

@@ -59,7 +59,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp.json

@@ -58,7 +58,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp23.json

@@ -63,7 +63,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp24-validate.json

@@ -79,7 +79,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp24.json

@@ -78,7 +78,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp25-validate.json

@@ -59,7 +59,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp25.json

@@ -58,7 +58,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp2var.json

@@ -78,7 +78,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

dune-project

@@ -58,7 +58,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (sha (>= 1.12))
     (fileutils (>= 0.6.4))
     cpu
-    arg-complete
+    (arg-complete (>= 0.2.1))
     (yaml (>= 3.0.0))
     uuidm
     catapult

goblint.opam

@@ -58,7 +58,7 @@ depends: [
   "sha" {>= "1.12"}
   "fileutils" {>= "0.6.4"}
   "cpu"
-  "arg-complete"
+  "arg-complete" {>= "0.2.1"}
   "yaml" {>= "3.0.0"}
   "uuidm"
   "catapult"

goblint.opam.locked

@@ -24,7 +24,7 @@ bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "angstrom" {= "0.16.0"}
   "apron" {= "v0.9.15"}
-  "arg-complete" {= "0.1.0"}
+  "arg-complete" {= "0.2.1"}
   "astring" {= "0.8.5"}
   "base-bigarray" {= "base"}
   "base-bytes" {= "base"}

make.sh

@@ -101,7 +101,7 @@ rule() {
       fi
       cd webapp && npm install && npm start
     ;; jar)
-      echo "Make sure you have the following installed: javac, ant"
+      echo "Make sure you have the following installed: javac, ant, dot (from graphviz)"
       if test ! -e "g2html/build.xml"; then
         git submodule update --init --recursive g2html
       fi

scripts/bash-completion.sh

@@ -6,10 +6,27 @@
 # Permanent usage:
 #   Run: echo "source $(readlink -f .)/scripts/bash-completion.sh" >> ~/.bash_completion
 
+# Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
+# Copied & modified from standard __ltrim_colon_completions
+__ltrim_equal_completions()
+{
+    if [[ $1 == *=* && $COMP_WORDBREAKS == *=* ]]; then
+        # Remove equal-word prefix from COMPREPLY items
+        local equal_word=${1%"${1##*=}"}
+        local i=${#COMPREPLY[*]}
+        while ((i-- > 0)); do
+            COMPREPLY[i]=${COMPREPLY[i]#"$equal_word"}
+        done
+    fi
+}
+
 _goblint ()
 {
     IFS=$'\n'
-    COMPREPLY=($(${COMP_WORDS[0]} --complete "${COMP_WORDS[@]:1:COMP_CWORD}"))
+    local words cword cur
+    _get_comp_words_by_ref -n = cur words cword # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
+    COMPREPLY=($(${words[0]} --complete "${words[@]:1:cword}"))
+    __ltrim_equal_completions "$cur" # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
 }
 
 complete -o default -F _goblint goblint
@@ -26,7 +43,10 @@ _regtest ()
             COMPREPLY=($(ls -1 tests/regression/${COMP_WORDS[1]}-* | sed -n -r 's/([0-9][0-9])-.*/\1/p' | grep "^${COMP_WORDS[2]}"))
             ;;
         *)
-            COMPREPLY=($($(dirname ${COMP_WORDS[0]})/goblint --complete "${COMP_WORDS[@]:3:COMP_CWORD}"))
+            local words cword cur
+            _get_comp_words_by_ref -n = cur words cword # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
+            COMPREPLY=($($(dirname ${words[0]})/goblint --complete "${words[@]:3:cword}"))
+            __ltrim_equal_completions "$cur" # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
             ;;
     esac
 }

scripts/creduce/branches.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+set -e
+
+gcc -c -Werror=implicit-function-declaration ./bad.c
+
+GOBLINTDIR="/home/simmo/dev/goblint/sv-comp/goblint"
+OPTS="--conf $GOBLINTDIR/conf/svcomp.json --set ana.specification $GOBLINTDIR/../sv-benchmarks/c/properties/unreach-call.prp bad.c --enable pre.enabled"
+LOG="goblint.log"
+
+$GOBLINTDIR/goblint $OPTS -v &> $LOG
+
+grep -F "Both branches dead" $LOG

scripts/goblint-lib-modules.py

@@ -53,6 +53,7 @@
     "DefExcDomain", # included in IntDomain
     "EnumsDomain", # included in IntDomain
     "CongruenceDomain", # included in IntDomain
+    "BitfieldDomain", #included in IntDomain
     "IntDomTuple", # included in IntDomain
     "WitnessGhostVar", # included in WitnessGhost
 

src/analyses/apron/relationAnalysis.apron.ml

@@ -465,17 +465,15 @@ struct
 
   (* Give the set of reachables from argument. *)
   let reachables (ask: Queries.ask) es =
-    let reachable e st =
-      match st with
-      | None -> None
-      | Some st ->
+    let reachable acc e =
+      Option.bind acc (fun st ->
         let ad = ask.f (Queries.ReachableFrom e) in
         if Queries.AD.is_top ad then
           None
         else
-          Some (Queries.AD.join ad st)
+          Some (Queries.AD.join ad st))
     in
-    List.fold_right reachable es (Some (Queries.AD.empty ()))
+    List.fold_left reachable (Some (Queries.AD.empty ())) es
 
 
   let forget_reachable man st es =
@@ -484,9 +482,8 @@ struct
       match reachables ask es with
       | None ->
         (* top reachable, so try to invalidate everything *)
-        RD.vars st.rel
-        |> List.filter_map RV.to_cil_varinfo
-        |> List.map Cil.var
+        let to_cil_lval x = Option.map Cil.var @@ RV.to_cil_varinfo x in
+        RD.vars st.rel |> List.filter_map to_cil_lval
       | Some ad ->
         let to_cil addr rs =
           match addr with
@@ -521,14 +518,10 @@ struct
     match desc.special args, f.vname with
     | Assert { exp; refine; _ }, _ -> assert_fn man exp refine
     | ThreadJoin { thread = id; ret_var = retvar }, _ ->
-      (
-        (* Forget value that thread return is assigned to *)
-        let st' = forget_reachable man st [retvar] in
-        let st' = Priv.thread_join ask man.global id st' in
-        match r with
-        | Some lv -> invalidate_one ask man st' lv
-        | None -> st'
-      )
+      (* Forget value that thread return is assigned to *)
+      let st' = forget_reachable man st [retvar] in
+      let st' = Priv.thread_join ask man.global id st' in
+      Option.map_default (invalidate_one ask man st') st' r
     | ThreadExit _, _ ->
       begin match ThreadId.get_current ask with
         | `Lifted tid ->
@@ -543,11 +536,10 @@ struct
       let id = List.hd args in
       Priv.thread_join ~force:true ask man.global id st
     | Rand, _ ->
-      (match r with
-       | Some lv ->
+      Option.map_default (fun lv ->
          let st = invalidate_one ask man st lv in
          assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
-       | None -> st)
+        ) st r
     | _, _ ->
       let lvallist e =
         match ask.f (Queries.MayPointTo e) with
@@ -575,10 +567,7 @@ struct
       let shallow_lvals = List.concat_map lvallist shallow_addrs in
       let st' = List.fold_left (invalidate_one ask man) st' shallow_lvals in
       (* invalidate lval if present *)
-      match r with
-      | Some lv -> invalidate_one ask man st' lv
-      | None -> st'
-
+      Option.map_default (invalidate_one ask man st') st' r
 
   let query_invariant man context =
     let keep_local = GobConfig.get_bool "ana.relation.invariant.local" in

src/analyses/base.ml

@@ -271,8 +271,8 @@ struct
           let n_offset = iDtoIdx n in
           begin match t with
             | Some t ->
-              let (f_offset_bits, _) = bitsOffset t (Field (f, NoOffset)) in
-              let f_offset = IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int (f_offset_bits / 8)) in
+              let f_offset_bytes = Cilfacade.bytesOffsetOnly t (Field (f, NoOffset)) in
+              let f_offset = IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int f_offset_bytes) in
               begin match IdxDom.(to_bool (eq f_offset (neg n_offset))) with
                 | Some true -> `NoOffset
                 | _ -> `Field (f, `Index (n_offset, `NoOffset))
@@ -518,7 +518,7 @@ struct
   (* From a list of values, presumably arguments to a function, simply extract
    * the pointer arguments. *)
   let get_ptrs (vals: value list): address list =
-    let f (x:value) acc = match x with
+    let f acc (x:value) = match x with
       | Address adrs when AD.is_top adrs ->
         M.info ~category:Unsound "Unknown address given as function argument"; acc
       | Address adrs when AD.to_var_may adrs = [] -> acc
@@ -528,7 +528,7 @@ struct
       | Top -> M.info ~category:Unsound "Unknown value type given as function argument"; acc
       | _ -> acc
     in
-    List.fold_right f vals []
+    List.fold_left f [] vals
 
   let rec reachable_from_value ask (value: value) (t: typ) (description: string)  =
     let empty = AD.empty () in
@@ -572,7 +572,7 @@ struct
     if M.tracing then M.traceli "reachability" "Checking reachable arguments from [%a]!" (d_list ", " AD.pretty) args;
     let empty = AD.empty () in
     (* We begin looking at the parameters: *)
-    let argset = List.fold_right (AD.join) args empty in
+    let argset = List.fold_left (AD.join) empty args in
     let workset = ref argset in
     (* And we keep a set of already visited variables *)
     let visited = ref empty in
@@ -624,6 +624,8 @@ struct
 
   let drop_intervalSet = CPA.map (function Int x -> Int (ID.no_intervalSet x) | x -> x )
 
+  let drop_bitfield = CPA.map (function Int x -> Int (ID.no_bitfield x) | x -> x )
+
   let context man (fd: fundec) (st: store): store =
     let f keep drop_fn (st: store) = if keep then st else { st with cpa = drop_fn st.cpa} in
     st |>
@@ -634,6 +636,7 @@ struct
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.int" ~removeAttr:"base.no-int" ~keepAttr:"base.int" fd) drop_ints
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.interval" ~removeAttr:"base.no-interval" ~keepAttr:"base.interval" fd) drop_interval
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.interval_set" ~removeAttr:"base.no-interval_set" ~keepAttr:"base.interval_set" fd) drop_intervalSet
+    %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.bitfield" ~removeAttr:"base.no-bitfield" ~keepAttr:"base.bitfield" fd) drop_bitfield
 
 
   let reachable_top_pointers_types man (ps: AD.t) : Queries.TS.t =
@@ -2286,8 +2289,7 @@ struct
       ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x)
     in
     let size_of_type_in_bytes typ =
-      let typ_size_in_bytes = (bitsSizeOf typ) / 8 in
-      intdom_of_int typ_size_in_bytes
+      intdom_of_int (Cilfacade.bytesSizeOf typ)
     in
     if points_to_heap_only man ptr then
       (* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *)

src/analyses/baseInvariant.ml

@@ -395,27 +395,46 @@ struct
             | Le, Some false -> meet_bin (ID.starting ikind (Z.succ l2)) (ID.ending ikind (Z.pred u1))
             | _, _ -> a, b)
          | _ -> a, b)
-      | BOr | BXor as op->
-        if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
+      | BOr ->
         (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)
-        a, b
+        if PrecisionUtil.get_bitfield () then
+          (* refinement based on the following idea: bit set to one in c and set to zero in b must be one in a and bit set to zero in c must be zero in a too (analogously for b) *)
+          let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_bor (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in
+          ID.meet a (ID.of_bitfield ikind (az, ao)), ID.meet b (ID.of_bitfield ikind (bz, bo))
+        else
+          (if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
+           (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)
+           (a, b)
+          )
+      | BXor ->
+        (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)
+        meet_com ID.logxor
       | LAnd ->
         if ID.to_bool c = Some true then
           meet_bin c c
         else
           a, b
-      | BAnd as op ->
+      | BAnd ->
         (* we only attempt to refine a here *)
+        let b_int = ID.to_int b in
         let a =
-          match ID.to_int b with
+          match b_int with
           | Some x when Z.equal x Z.one ->
             (match ID.to_bool c with
              | Some true -> ID.meet a (ID.of_congruence ikind (Z.one, Z.of_int 2))
              | Some false -> ID.meet a (ID.of_congruence ikind (Z.zero, Z.of_int 2))
-             | None -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a 1 = %a" d_binop op ID.pretty c; a)
-          | _ -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a %a = %a" d_binop op ID.pretty b ID.pretty c; a
+             | None -> a)
+          | _ -> a
         in
-        a, b
+        if PrecisionUtil.get_bitfield () then
+          (* refinement based on the following idea: bit set to zero in c and set to one in b must be zero in a and bit set to one in c must be one in a too (analogously for b) *)
+          let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_band (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in
+          ID.meet a (ID.of_bitfield ikind (az, ao)), ID.meet b (ID.of_bitfield ikind (bz, bo))
+        else if b_int = None then
+          (if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
+           (a, b)
+          )
+        else a, b
       | op ->
         if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
         a, b