Merge branch 'master' into issue_1328

Author: DrMichaelPetter

.github/workflows/docker.yml

@@ -59,7 +59,7 @@ jobs:
 
       - name: Build Docker image
         id: build
-        uses: docker/build-push-action@v5
+        uses: docker/build-push-action@v6
         with:
           context: .
           load: true # load into docker instead of immediately pushing
@@ -72,7 +72,7 @@ jobs:
         run: docker run --rm -v $(pwd):/data ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ steps.meta.outputs.version }} /data/tests/regression/04-mutex/01-simple_rc.c # run image by version in case multiple tags
 
       - name: Push Docker image
-        uses: docker/build-push-action@v5
+        uses: docker/build-push-action@v6
         with:
           context: .
           push: true

.github/workflows/unlocked.yml

@@ -165,7 +165,7 @@ jobs:
 
       - name: Build dev Docker image
         id: build
-        uses: docker/build-push-action@v5
+        uses: docker/build-push-action@v6
         with:
           context: .
           target: dev

.zenodo.json

@@ -23,6 +23,11 @@
       "affiliation": "Technische Universität München",
       "orcid": "0009-0009-9644-7475"
     },
+    {
+      "name": "Holter, Karoliine",
+      "affiliation": "University of Tartu",
+      "orcid": "0009-0008-3725-4131"
+    },
     {
       "name": "Vogler, Ralf",
       "affiliation": "Technische Universität München"

CITATION.cff

@@ -21,6 +21,10 @@ authors: # same authors as in .zenodo.json and dune-project
     family-names: Tilscher
     affiliation: "Technische Universität München"
     orcid: "https://orcid.org/0009-0009-9644-7475"
+  - given-names: Karoliine
+    family-names: Holter
+    affiliation: "University of Tartu"
+    orcid: "https://orcid.org/0009-0008-3725-4131"
   - given-names: Ralf
     family-names: Vogler
     affiliation: "Technische Universität München"

conf/examples/medium-program.json

@@ -9,6 +9,7 @@
       "base",
       "threadid",
       "threadflag",
+      "threadreturn",
       "mallocWrapper",
       "mutexEvents",
       "mutex",
@@ -18,6 +19,7 @@
       "expRelation",
       "mhp",
       "assert",
+      "pthreadMutexType",
       "var_eq",
       "symb_locks",
       "region",

conf/examples/very-precise.json

@@ -22,6 +22,7 @@
       "base",
       "threadid",
       "threadflag",
+      "threadreturn",
       "mallocWrapper",
       "mutexEvents",
       "mutex",
@@ -31,6 +32,7 @@
       "expRelation",
       "mhp",
       "assert",
+      "pthreadMutexType",
       "var_eq",
       "symb_locks",
       "region",

docs/user-guide/assumptions.md

@@ -17,3 +17,22 @@ _NB! This list is likely incomplete._
 
     See [PR #1414](https://github.com/goblint/analyzer/pull/1414).
 
+2.  Pointer arithmetic does not overflow.
+
+    [C11's N1570][n1570] at 6.5.6.8 states that
+
+    > When an expression that has integer type is added to or subtracted from a pointer, the result has the type of the pointer operand.
+    > [...]
+    > the evaluation shall not produce an overflow; otherwise, the behavior is undefined.
+
+    after a long list of defined behaviors.
+
+    Goblint does not report overflow and out-of-bounds pointer arithmetic (when the pointer _is not dereferenced_).
+    This affects the overflow analysis (SV-COMP no-overflow property) in the `base` analysis.
+
+    This _does not_ affect the `memOutOfBounds` analysis (SV-COMP valid-memsafety property), which is for undefined behavior from _dereferencing_ such out-of-bounds pointers.
+
+    See [PR #1511](https://github.com/goblint/analyzer/pull/1511).
+
+
+[n1570]: https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf

dune-project

@@ -15,13 +15,26 @@
 (source (github goblint/analyzer))
 (homepage "https://goblint.in.tum.de")
 (documentation "https://goblint.readthedocs.io/en/latest/")
-(authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff
+(authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Karoliine Holter" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff
 (maintainers "Simmo Saan <[email protected]>" "Michael Schwarz <[email protected]>" "Karoliine Holter")
 (license MIT)
 
 (package
   (name goblint)
   (synopsis "Static analysis framework for C")
+  (description "\
+Goblint is a sound static analysis framework for C programs using abstract interpretation.
+It specializes in thread-modular verification of multi-threaded programs, especially regarding data races.
+Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses.
+")
+  (tags (
+    "program analysis"
+    "program verification"
+    "static analysis"
+    "abstract interpretation"
+    "C"
+    "data race analysis"
+    "concurrency"))
   (depends
     (ocaml (>= 4.14))
     (goblint-cil (>= 2.0.3)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.

goblint.opam

@@ -1,6 +1,11 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 synopsis: "Static analysis framework for C"
+description: """
+Goblint is a sound static analysis framework for C programs using abstract interpretation.
+It specializes in thread-modular verification of multi-threaded programs, especially regarding data races.
+Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses.
+"""
 maintainer: [
   "Simmo Saan <[email protected]>"
   "Michael Schwarz <[email protected]>"
@@ -11,11 +16,21 @@ authors: [
   "Michael Schwarz"
   "Julian Erhard"
   "Sarah Tilscher"
+  "Karoliine Holter"
   "Ralf Vogler"
   "Kalmer Apinis"
   "Vesal Vojdani"
 ]
 license: "MIT"
+tags: [
+  "program analysis"
+  "program verification"
+  "static analysis"
+  "abstract interpretation"
+  "C"
+  "data race analysis"
+  "concurrency"
+]
 homepage: "https://goblint.in.tum.de"
 doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"

goblint.opam.locked

@@ -12,6 +12,7 @@ authors: [
   "Michael Schwarz"
   "Julian Erhard"
   "Sarah Tilscher"
+  "Karoliine Holter"
   "Ralf Vogler"
   "Kalmer Apinis"
   "Vesal Vojdani"
@@ -142,3 +143,16 @@ pin-depends: [
   ]
 ]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
+description: """\
+Goblint is a sound static analysis framework for C programs using abstract interpretation.
+It specializes in thread-modular verification of multi-threaded programs, especially regarding data races.
+Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses."""
+tags: [
+  "program analysis"
+  "program verification"
+  "static analysis"
+  "abstract interpretation"
+  "C"
+  "data race analysis"
+  "concurrency"
+]

src/analyses/apron/relationAnalysis.apron.ml

@@ -756,7 +756,7 @@ struct
 
   let sync ctx reason =
     (* After the solver is finished, store the results (for later comparison) *)
-    if !AnalysisState.postsolving then begin
+    if !AnalysisState.postsolving && GobConfig.get_string "exp.relation.prec-dump" <> "" then begin
       let keep_local = GobConfig.get_bool "ana.relation.invariant.local" in
       let keep_global = GobConfig.get_bool "ana.relation.invariant.global" in
 

src/analyses/base.ml

@@ -261,6 +261,8 @@ struct
       (* adds n to the last offset *)
       let rec addToOffset n (t:typ option) = function
         | `Index (i, `NoOffset) ->
+          (* Binary operations on pointer types should not generate warnings in SV-COMP *)
+          GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
           (* If we have arrived at the last Offset and it is an Index, we add our integer to it *)
           `Index(IdxDom.add i (iDtoIdx n), `NoOffset)
         | `Field (f, `NoOffset) ->

src/analyses/mutexTypeAnalysis.ml

@@ -12,16 +12,17 @@ struct
 
   let name () = "pthreadMutexType"
 
-  (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *)
-  module O = Offset.Unit
-
-  module V = struct
-    include Printable.Prod(CilType.Varinfo)(O) (* TODO: use Mval.Unit *)
+  module V =
+  struct
+    (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *)
+    include Mval.Unit
     let is_write_only _ = false
   end
 
   module G = MAttr
 
+  module O = Offset.Unit
+
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
     match lval with

src/analyses/unassumeAnalysis.ml

@@ -85,7 +85,9 @@ struct
 
     let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with
       | Ok yaml -> yaml
-      | Error (`Msg m) -> failwith ("Yaml_unix.of_file: " ^ m)
+      | Error (`Msg m) ->
+        Logs.error "Yaml_unix.of_file: %s" m;
+        Svcomp.errorwith "witness missing"
     in
     let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in
 

src/autoTune.ml

@@ -186,7 +186,7 @@ let enableAnalyses anas =
 (*escape is also still enabled, because otherwise we get a warning*)
 (*does not consider dynamic calls!*)
 
-let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"]
+let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"]
 let reduceThreadAnalyses () =
   let isThreadCreate = function
     | LibraryDesc.ThreadCreate _ -> true

src/build-info/dune

@@ -15,7 +15,7 @@
   (target configVersion.ml)
   (mode (promote (until-clean) (only configVersion.ml))) ; replace existing file in source tree, even if releasing (only overrides)
   (deps (universe)) ; do not cache, always regenerate
-  (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = \"%s\"'")))))
+  (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = Sys.opaque_identity \"%s\"'")))))
 
 (rule
   (target configProfile.ml)
@@ -31,7 +31,7 @@
   (target configDatetime.ml)
   (mode (promote (until-clean) (only configDatetime.ml))) ; replace existing file in source tree, even if releasing (only overrides)
   (deps (universe)) ; do not cache, always regenerate
-  (action (pipe-stdout (bash "date +\"%Y-%m-%dT%H:%M:%S\" || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet datetime = \"%s\"'")))))
+  (action (pipe-stdout (bash "date +\"%Y-%m-%dT%H:%M:%S\" || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet datetime = Sys.opaque_identity \"%s\"'")))))
 
 (env
   (_

src/cdomain/value/cdomains/offset.ml

@@ -213,7 +213,7 @@ struct
         let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset  in
         let bits_offset = idx_of_int bits_offset in
         let remaining_offset = offset_to_index_offset ~typ:field.ftype o in
-        Idx.add bits_offset remaining_offset
+        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bits_offset remaining_offset
       | `Index (x, o) ->
         let (item_typ, item_size_in_bits) =
           match Option.map unrollType typ with
@@ -223,9 +223,10 @@ struct
           | _ ->
             (None, Idx.top ())
         in
-        let bits_offset = Idx.mul item_size_in_bits x in
+        (* Binary operations on offsets should not generate overflow warnings in SV-COMP *)
+        let bits_offset = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.mul item_size_in_bits x in
         let remaining_offset = offset_to_index_offset ?typ:item_typ o in
-        Idx.add bits_offset remaining_offset
+        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bits_offset remaining_offset
     in
     offset_to_index_offset ?typ offs
 

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

@@ -158,7 +158,7 @@ module EqualitiesConjunction = struct
             let (newref,offs,divi) = (get_rhs d head) in
             let (coeff,y) = BatOption.get newref in
             let (y,yrhs) = inverse head (coeff,y,offs,divi) in (* reassemble yrhs out of components *)
-            let shifted_cluster =  (List.fold (fun map i -> 
+            let shifted_cluster =  (List.fold (fun map i ->
                 let irhs = (get_rhs d i) in (* old entry is i = irhs *)
                 Rhs.subst yrhs y irhs |>    (* new entry for i is irhs [yrhs/y] *)
                 set_rhs map i
@@ -222,7 +222,7 @@ module EqualitiesConjunction = struct
        | Some (coeff,j), ((Some (coeff1,h1), o1, divi1) as oldi)->
          (match get_rhs ts j with
           (* ts[x_j]=o2/d2             ========>  ... *)
-          | (None            , o2, divi2) -> 
+          | (None            , o2, divi2) ->
             let newxi  = Rhs.subst (None,o2,divi2) j (Some (coeff,j),offs,divi) in
             let newxh1 = snd @@ inverse i (coeff1,h1,o1,divi1) in
             let newxh1 = Rhs.subst newxi i newxh1 in
@@ -251,7 +251,7 @@ module EqualitiesConjunction = struct
     else (* var_i = var_i, i.e. it may occur on the rhs of other equalities *)
       (* so now, we transform with the inverse of the transformer: *)
       let inv = snd (inverse i (coeff,j,offs,divi)) in
-      IntMap.fold (fun k v acc -> 
+      IntMap.fold (fun k v acc ->
           match v with
           | (Some (c,x),o,d) when x=i-> set_rhs acc k (Rhs.subst inv i v)
           | _ -> acc
@@ -281,7 +281,7 @@ struct
     let multiply a b =
       (* if one of them is a constant, then multiply. Otherwise, the expression is not linear *)
       match a, b with
-      | [(None,coeff, divi)], c 
+      | [(None,coeff, divi)], c
       | c, [(None,coeff, divi)] -> multiply_with_Q coeff divi c
       | _ -> raise NotLinearExpr
     in
@@ -314,7 +314,7 @@ struct
     | x -> Some(x)
 
   (** convert and simplify (wrt. reference variables) a texpr into a tuple of a list of monomials (coeff,varidx,divi) and a (constant/divi) *)
-  let simplified_monomials_from_texp (t: t) texp = 
+  let simplified_monomials_from_texp (t: t) texp =
     BatOption.bind (monomials_from_texp t texp)
       (fun monomiallist ->
          let d = Option.get t.d in
@@ -323,7 +323,7 @@ struct
            | None -> let gcdee = Z.gcd adiv divi in exprcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi)
            | Some (coeff,idx) -> let (somevar,someoffs,somedivi)=Rhs.subst (EConj.get_rhs d idx) idx (v,offs,divi) in (* normalize! *)
              let newcache = Option.map_default (fun (coef,ter) -> IMap.add ter Q.((IMap.find_default zero ter exprcache) + make coef somedivi) exprcache) exprcache somevar in
-             let gcdee = Z.gcd adiv divi in 
+             let gcdee = Z.gcd adiv divi in
              (newcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi))
          in
          let (expr,constant) = List.fold_left accumulate_constants (IMap.empty,(Z.zero,Z.one)) monomiallist in (* abstract simplification of the guard wrt. reference variables *)
@@ -339,7 +339,7 @@ struct
     BatOption.bind (simplified_monomials_from_texp t texp )
       (fun (sum_of_terms, (constant,divisor)) ->
          (match sum_of_terms with
-          | [] -> Some (None, constant,divisor) 
+          | [] -> Some (None, constant,divisor)
           | [(coeff,var,divi)] -> Some (Rhs.canonicalize (Some (Z.mul divisor coeff,var), Z.mul constant divi,Z.mul divisor divi))
           |_ -> None))
 
@@ -447,7 +447,7 @@ struct
     let t1 = change_d t1 sup_env ~add:true ~del:false in
     let t2 = change_d t2 sup_env ~add:true ~del:false in
     match t1.d, t2.d with
-    | Some d1', Some d2' -> 
+    | Some d1', Some d2' ->
       EConj.IntMap.fold (fun lhs rhs map -> meet_with_one_conj map lhs rhs) (snd d2') t1 (* even on sparse d2, this will chose the relevant conjs to meet with*)
     | _ -> {d = None; env = sup_env}
 
@@ -489,7 +489,7 @@ struct
          - lhs itself
          - criteria A and B that characterize equivalence class, depending on the reference variable and the affine expression parameters wrt. each EConj
          - rhs1
-         - rhs2 
+         - rhs2
            however, we have to account for the sparseity of EConj maps by manually patching holes with default values *)
       let joinfunction lhs rhs1 rhs2 =
         (
@@ -516,15 +516,15 @@ struct
       let varentry ci offi ch offh xh =
         let (coeff,off,d) = Q.(ci,(offi*ch)-(ci*offh),ch) in (* compute new rhs in Q *)
         let (coeff,off,d) = Z.(coeff.num*d.den*off.den,off.num*d.den*coeff.den,d. num*coeff.den*off.den) in (* convert that back into Z *)
-        Rhs.canonicalize (Some(coeff,xh),off,d) 
+        Rhs.canonicalize (Some(coeff,xh),off,d)
       in
       (* ci1 = a*ch1+b /\ ci2 = a*ch2+b *)
       (* ===> a = (ci1-ci2)/(ch1-ch2) b = ci2-a*ch2 *)
-      let constentry ci1 ci2 ch1 ch2 xh = 
+      let constentry ci1 ci2 ch1 ch2 xh =
         let a = Q.((ci1-ci2) / (ch1-ch2)) in
         let b = Q.(ci2 - a*ch2) in
         Rhs.canonicalize (Some (Z.(a.num*b.den),xh),Z.(b.num*a.den) ,Z.(a.den*b.den) ) in
-      let iterate map l = 
+      let iterate map l =
         match l with
         | (_, _, _, rhs                  , rhs'                 ) :: t when Rhs.equal rhs rhs' -> List.fold (fun acc (x,_,_,rh,_)      -> EConj.set_rhs acc x rh) map l
         | (h, _, _, ((Some (ch,_),oh,dh)), ((Some _,_,_)       )) :: t -> List.fold (fun acc (i,_,_,(monom,oi,di),_)         -> EConj.set_rhs acc i (varentry   Q.(make (fst@@Option.get monom) di)   Q.(make oi di)   Q.(make ch dh)   Q.(make oh dh)   h)) map t