Merge branch 'master' into mem-oob-analysis

.github/workflows/coverage.yml

@@ -28,7 +28,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:

.github/workflows/docker.yml

@@ -35,7 +35,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
         uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action

.github/workflows/docs.yml

@@ -30,7 +30,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Check for undocumented modules
         run: python scripts/goblint-lib-modules.py

.github/workflows/indentation.yml

@@ -20,7 +20,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
 

.github/workflows/locked.yml

@@ -30,7 +30,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -101,7 +101,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -141,7 +141,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:

.github/workflows/metadata.yml

@@ -19,7 +19,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Validate CITATION.cff
         uses: docker://citationcff/cffconvert:latest
@@ -36,7 +36,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
         uses: actions/setup-node@v3

.github/workflows/options.yml

@@ -15,7 +15,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
         uses: actions/setup-node@v3

.github/workflows/semgrep.yml

@@ -16,10 +16,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Run semgrep
-        run: semgrep scan --sarif --output=semgrep.sarif
+        run: semgrep scan --config .semgrep/ --sarif > semgrep.sarif
 
       - name: Upload SARIF file to GitHub Advanced Security Dashboard
         uses: github/codeql-action/upload-sarif@v2

.github/workflows/unlocked.yml

@@ -45,7 +45,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
@@ -131,7 +131,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
@@ -208,7 +208,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
         uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
@@ -246,7 +246,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2

.semgrep/tracing.yml

@@ -9,6 +9,7 @@ rules:
         - pattern: Messages.traceu
         - pattern: Messages.traceli
       - pattern-not-inside: if Messages.tracing then ...
+      - pattern-not-inside: if Messages.tracing && ... then ...
     message: trace functions should only be called if tracing is enabled at compile time
     languages: [ocaml]
     severity: WARNING

conf/bench-yaml-validate.json

@@ -52,14 +52,6 @@
       "tokens": true
     }
   },
-  "witness": {
-    "enabled": false,
-    "invariant": {
-      "loop-head": true,
-      "after-lock": true,
-      "other": false
-    }
-  },
   "sem": {
     "unknown_function": {
       "invalidate": {

conf/bench-yaml.json

@@ -48,20 +48,6 @@
       ]
     }
   },
-  "witness": {
-    "enabled": false,
-    "yaml": {
-      "enabled": true
-    },
-    "invariant": {
-      "exact": false,
-      "exclude-vars": [
-        "tmp\\(___[0-9]+\\)?",
-        "cond",
-        "RETURN"
-      ]
-    }
-  },
   "sem": {
     "unknown_function": {
       "invalidate": {

conf/svcomp-yaml-validate.json

@@ -12,6 +12,10 @@
     "float": {
       "interval": true
     },
+    "apron": {
+      "domain": "polyhedra",
+      "strengthening": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -31,6 +35,7 @@
       "region",
       "thread",
       "threadJoins",
+      "apron",
       "unassume"
     ],
     "context": {
@@ -74,14 +79,6 @@
   "exp": {
     "region-offsets": true
   },
-  "witness": {
-    "enabled": false,
-    "invariant": {
-      "loop-head": true,
-      "after-lock": false,
-      "other": false
-    }
-  },
   "solver": "td3",
   "sem": {
     "unknown_function": {

conf/svcomp-yaml.json

@@ -12,6 +12,10 @@
     "float": {
       "interval": true
     },
+    "apron": {
+      "domain": "polyhedra",
+      "strengthening": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -30,7 +34,8 @@
       "symb_locks",
       "region",
       "thread",
-      "threadJoins"
+      "threadJoins",
+      "apron"
     ],
     "context": {
       "widen": false
@@ -76,6 +81,9 @@
       "enabled": true
     },
     "invariant": {
+      "loop-head": true,
+      "other": false,
+      "accessed": false,
       "exact": false,
       "exclude-vars": [
         "tmp\\(___[0-9]+\\)?",

src/analyses/base.ml

@@ -397,6 +397,8 @@ struct
           Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.zero else match eq p1 p2 with Some x when x -> ID.of_int ik BI.one | _ -> bool_top ik)
         | Ne ->
           Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.one else match eq p1 p2 with Some x when x -> ID.of_int ik BI.zero | _ -> bool_top ik)
+        | IndexPI when AD.to_string p2 = ["all_index"] ->
+          addToAddrOp p1 (ID.top_of (Cilfacade.ptrdiff_ikind ()))
         | _ -> VD.top ()
       end
     (* For other values, we just give up! *)
@@ -1053,7 +1055,6 @@ struct
            else if AD.may_be_null adr
            then M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer");
           AD.map (add_offset_varinfo (convert_offset a gs st ofs)) adr
-        | Bot -> AD.bot ()
         | _ ->
           M.debug ~category:Analyzer "Failed evaluating %a to lvalue" d_lval lval;
           AD.unknown_ptr
@@ -2303,10 +2304,18 @@ struct
             then AD.join addr AD.null_ptr (* calloc can fail and return NULL *)
             else addr in
           let ik = Cilfacade.ptrdiff_ikind () in
-          let blobsize = ID.mul (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st size) (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st n) in
-          (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
-          set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
-                                                         (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
+          let sizeval = eval_int (Analyses.ask_of_ctx ctx) gs st size in
+          let countval = eval_int (Analyses.ask_of_ctx ctx) gs st n in
+          if ID.to_int countval = Some Z.one then (
+            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false));
+          (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var)))]
+          )
+          else (
+            let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
+            (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
+            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
+                                                          (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
+          )
         | _ -> st
       end
     | Realloc { ptr = p; size }, _ ->

src/analyses/unassumeAnalysis.ml

@@ -111,7 +111,7 @@ struct
           Locator.ES.iter (fun n ->
               let fundec = Node.find_fundec n in
 
-              match InvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs with
+              match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with
               | Ok inv_exp ->
                 M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
                 NH.add invs n {exp = inv_exp; uuid}
@@ -157,12 +157,12 @@ struct
           Locator.ES.iter (fun n ->
               let fundec = Node.find_fundec n in
 
-              match InvariantParser.parse_cil inv_parser ~fundec ~loc pre_cabs with
+              match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc pre_cabs with
               | Ok pre_exp ->
                 M.debug ~category:Witness ~loc:msgLoc "located precondition to %a: %a" CilType.Fundec.pretty fundec Cil.d_exp pre_exp;
                 FH.add fun_pres fundec pre_exp;
 
-                begin match InvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs with
+                begin match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with
                   | Ok inv_exp ->
                     M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
                     if not (NH.mem pre_invs n) then

src/analyses/varEq.ml

@@ -291,7 +291,7 @@ struct
            | Question (b, t, f, _) -> lval_may_change_pt b bl || lval_may_change_pt t bl || lval_may_change_pt f bl
     in
     let r =
-      if Cil.isConstant b then false
+      if Cil.isConstant b || Cil.isConstant a then false
       else if Queries.LS.is_top bls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) bls
       then ((*Messages.warn ~category:Analyzer "No PT-set: switching to types ";*) type_may_change_apt a )
       else Queries.LS.exists (lval_may_change_pt a) bls

src/cdomains/apron/apronDomain.apron.ml

@@ -693,16 +693,16 @@ struct
 
   let join x y =
     (* just to optimize joining folds, which start with bot *)
-    if is_bot x then
+    if is_bot x then (* TODO: also for non-empty env *)
       y
-    else if is_bot y then
+    else if is_bot y then (* TODO: also for non-empty env *)
       x
     else (
       if M.tracing then M.traceli "apron" "join %a %a\n" pretty x pretty y;
       let j = join x y in
       if M.tracing then M.trace "apron" "j = %a\n" pretty j;
       let j =
-        if strengthening_enabled then
+        if strengthening_enabled then (* TODO: skip if same envs? *)
           strengthening j x y
         else
           j

src/cdomains/intDomain.ml

@@ -760,7 +760,7 @@ struct
       norm ik @@ Some (l2,u2) |> fst
   let widen ik x y =
     let r = widen ik x y in
-    if M.tracing then M.tracel "int" "interval widen %a %a -> %a\n" pretty x pretty y pretty r;
+    if M.tracing && not (equal x y) then M.tracel "int" "interval widen %a %a -> %a\n" pretty x pretty y pretty r;
     assert (leq x y); (* TODO: remove for performance reasons? *)
     r
 

src/cdomains/valueDomain.ml

@@ -115,7 +115,7 @@ struct
     | _ -> false
 
   let is_mutex_type (t: typ): bool = match t with
-    | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t"
+    | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t" || info.tname = "pthread_cond_t"
     | TInt (IInt, attr) -> hasAttribute "mutex" attr
     | _ -> false
 

src/domains/partitionDomain.ml

@@ -115,18 +115,23 @@ struct
       for_all (fun p -> exists (B.leq p) y) x
 
   let pretty_diff () (y, x) =
-    (* based on DisjointDomain.PairwiseSet *)
-    let x_not_leq = filter (fun p ->
-        not (exists (fun q -> B.leq p q) y)
-      ) x
-    in
-    let p_not_leq = choose x_not_leq in
-    GoblintCil.Pretty.(
-      dprintf "%a:\n" B.pretty p_not_leq
-      ++
-      fold (fun q acc ->
-          dprintf "not leq %a because %a\n" B.pretty q B.pretty_diff (p_not_leq, q) ++ acc
-        ) y nil
+    if E.is_top x then (
+      GoblintCil.Pretty.(dprintf "%a not leq bot" pretty y)
+    )
+    else (
+      (* based on DisjointDomain.PairwiseSet *)
+      let x_not_leq = filter (fun p ->
+          not (exists (fun q -> B.leq p q) y)
+        ) x
+      in
+      let p_not_leq = choose x_not_leq in
+      GoblintCil.Pretty.(
+        dprintf "%a:\n" B.pretty p_not_leq
+        ++
+        fold (fun q acc ->
+            dprintf "not leq %a because %a\n" B.pretty q B.pretty_diff (p_not_leq, q) ++ acc
+          ) y nil
+      )
     )
 
   let meet xs ys = if is_bot xs || is_bot ys then bot () else