diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml index 36568e6cb2..daa7f224b8 100644 --- a/.github/workflows/docker.yml +++ b/.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 diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index db41ad3007..f1bd399a17 100644 --- a/.github/workflows/unlocked.yml +++ b/.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 diff --git a/.zenodo.json b/.zenodo.json index 22705c2d9c..1e71573948 100644 --- a/.zenodo.json +++ b/.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" diff --git a/CITATION.cff b/CITATION.cff index 25d46cf762..7a93859c54 100644 --- a/CITATION.cff +++ b/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" diff --git a/conf/examples/medium-program.json b/conf/examples/medium-program.json index 2c1e7c7346..5afc1aa2f8 100644 --- a/conf/examples/medium-program.json +++ b/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", diff --git a/conf/examples/very-precise.json b/conf/examples/very-precise.json index 2197335eaf..074d448a85 100644 --- a/conf/examples/very-precise.json +++ b/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", diff --git a/docs/user-guide/assumptions.md b/docs/user-guide/assumptions.md index f77e3b5097..33284ccc00 100644 --- a/docs/user-guide/assumptions.md +++ b/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 diff --git a/dune-project b/dune-project index 878abd3b4f..8d9d53623b 100644 --- a/dune-project +++ b/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 " "Michael Schwarz " "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. diff --git a/goblint.opam b/goblint.opam index 692625c965..e198bf6f3c 100644 --- a/goblint.opam +++ b/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 " "Michael Schwarz " @@ -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" diff --git a/goblint.opam.locked b/goblint.opam.locked index f8de683948..b1d8030c1c 100644 --- a/goblint.opam.locked +++ b/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" +] diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index a42d78d71a..ad99e26b58 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/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 diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 102e22b5a7..29fa74c5a9 100644 --- a/src/analyses/base.ml +++ b/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) -> diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml index 441f2e9953..4a993bbd7d 100644 --- a/src/analyses/mutexTypeAnalysis.ml +++ b/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 diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 265e9c6925..85b33edc79 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/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 diff --git a/src/autoTune.ml b/src/autoTune.ml index 434b4fb0b2..8ec77739e7 100644 --- a/src/autoTune.ml +++ b/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 diff --git a/src/build-info/dune b/src/build-info/dune index 5a64b399a4..e1a45ef8fc 100644 --- a/src/build-info/dune +++ b/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 (_ diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml index 9c9c5c3333..e8cba0afc5 100644 --- a/src/cdomain/value/cdomains/offset.ml +++ b/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 diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 5558bc2c96..3a9e2d3e11 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/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 diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 668b6af5d4..4809e97917 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -140,7 +140,7 @@ struct let expr = (** simplify asks for a constant value of some subexpression e, similar to a constant fold. In particular but not exclusively this query is answered by the 2 var equalities domain itself. This normalizes arbitrary expressions to a point where they - might be able to be represented by means of 2 var equalities + might be able to be represented by means of 2 var equalities This simplification happens during a time, when there are temporary variables a#in and a#out part of the expression, but are not represented in the ctx, thus queries may result in top for these variables. Wrapping this in speculative diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index 1a642c932a..199113a5d8 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -588,7 +588,7 @@ module Prod4 (Base1: S) (Base2: S) (Base3: S) (Base4: S) = struct let arbitrary () = QCheck.quad (Base1.arbitrary ()) (Base2.arbitrary ()) (Base3.arbitrary ()) (Base4.arbitrary ()) end -module PQueue (Base: S) = +module PQueue (Base: S) = struct type t = Base.t BatDeque.dq include Std @@ -604,22 +604,22 @@ struct let rec loop n q = match BatDeque.front q with | None -> () - | Some (x, xs) -> (BatPrintf.fprintf f "%d\n%a\n" n Base.printXml x; + | Some (x, xs) -> (BatPrintf.fprintf f "%d\n%a\n" n Base.printXml x; loop (n+1) (xs)) in BatPrintf.fprintf f "\n\n"; - loop 0 xs; + loop 0 xs; BatPrintf.fprintf f "\n\n" let to_yojson q = `List (BatDeque.to_list @@ BatDeque.map (Base.to_yojson) q) let hash q = BatDeque.fold_left (fun acc x -> (acc + 71) * (Base.hash x)) 11 q let equal q1 q2 = BatDeque.eq ~eq:Base.equal q1 q2 - let compare q1 q2 = + let compare q1 q2 = match BatDeque.front q1, BatDeque.front q2 with | None, None -> 0 | None, Some(_, _) -> -1 | Some(_, _), None -> 1 - | Some(a1, q1'), Some(a2, q2') -> + | Some(a1, q1'), Some(a2, q2') -> let c = Base.compare a1 a2 in if c <> 0 then c else compare q1' q2' diff --git a/src/config/options.schema.json b/src/config/options.schema.json index acf85abed9..d259a6f418 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -344,7 +344,7 @@ "default": [ "expRelation", "base", "threadid", "threadflag", "threadreturn", "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp", - "assert" + "assert", "pthreadMutexType" ] }, "path_sens": { diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index e0e36801ed..7df4167acd 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -713,11 +713,13 @@ struct let tf_assign var edge prev_node lv e getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.assign ctx lv e) !r !spawns + let d = S.assign ctx lv e in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let tf_vdecl var edge prev_node v getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.vdecl ctx v) !r !spawns + let d = S.vdecl ctx v in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let normal_return r fd ctx sideg = let spawning_return = S.return ctx r fd in @@ -732,7 +734,7 @@ struct let tf_ret var edge prev_node ret fd getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - let d = + let d = (* Force transfer function to be evaluated before dereferencing in common_join argument. *) if (CilType.Fundec.equal fd MyCFG.dummy_func || List.mem fd.svar.vname (get_string_list "mainfun")) && get_bool "kernel" @@ -747,11 +749,13 @@ struct let c: unit -> S.C.t = snd var |> Obj.obj in side_context sideg fd (c ()); let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.body ctx fd) !r !spawns + let d = S.body ctx fd in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let tf_test var edge prev_node e tv getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.branch ctx e tv) !r !spawns + let d = S.branch ctx e tv in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let tf_normal_call ctx lv e (f:fundec) args getl sidel getg sideg = let combine (cd, fc, fd) = @@ -870,11 +874,13 @@ struct let tf_asm var edge prev_node getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.asm ctx) !r !spawns + let d = S.asm ctx in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let tf_skip var edge prev_node getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.skip ctx) !r !spawns + let d = S.skip ctx in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let tf var getl sidel getg sideg prev_node edge d = begin match edge with diff --git a/src/framework/control.ml b/src/framework/control.ml index 05fad90caf..5e92282210 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -357,6 +357,7 @@ struct (* real beginning of the [analyze] function *) if get_bool "ana.sv-comp.enabled" then Witness.init (module FileCfg); (* TODO: move this out of analyze_loop *) + YamlWitness.init (); AnalysisState.global_initialization := true; GobConfig.earlyglobs := get_bool "exp.earlyglobs"; @@ -789,15 +790,19 @@ struct ); (* Before SV-COMP, so result can depend on YAML witness validation. *) - if get_string "witness.yaml.validate" <> "" then ( - let module YWitness = YamlWitness.Validator (R) in - YWitness.validate () - ); + let yaml_validate_result = + if get_string "witness.yaml.validate" <> "" then ( + let module YWitness = YamlWitness.Validator (R) in + Some (YWitness.validate ()) + ) + else + None + in if get_bool "ana.sv-comp.enabled" then ( (* SV-COMP and witness generation *) let module WResult = Witness.Result (R) in - WResult.write entrystates + WResult.write yaml_validate_result entrystates ); if get_bool "witness.yaml.enabled" then ( diff --git a/src/goblint.ml b/src/goblint.ml index a687badb8e..52b9bbdfc0 100644 --- a/src/goblint.ml +++ b/src/goblint.ml @@ -83,6 +83,11 @@ let main () = Logs.error "%s" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!")); Goblint_timing.teardown_tef (); exit 124 + | Svcomp.Error msg -> + do_stats (); + Witness.print_svcomp_result ("ERROR (" ^ msg ^ ")"); + Goblint_timing.teardown_tef (); + exit 1 (* We do this since the evaluation order of top-level bindings is not defined, but we want `main` to run after all the other side-effects (e.g. registering analyses/solvers) have happened. *) let () = at_exit main diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 4e678c926e..e7ff2a4d04 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -1246,7 +1246,7 @@ let libraries = descs_tbl ) libraries -let all_library_descs: (string, LibraryDesc.t) Hashtbl.t = +let _all_library_descs: (string, LibraryDesc.t) Hashtbl.t = Hashtbl.fold (fun _ descs_tbl acc -> Hashtbl.merge (fun name desc1 desc2 -> match desc1, desc2 with diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index bb887e6cb1..59a8f01b40 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -60,6 +60,11 @@ struct | Unknown -> "unknown" end +exception Error of string + +let errorwith s = raise (Error s) + + module type TaskResult = sig module Arg: MyARG.S diff --git a/src/witness/witness.ml b/src/witness/witness.ml index fb88c2ce7b..7b0213b601 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -690,25 +690,16 @@ struct Timing.wrap "graphml witness" (write_file witness_path (module Task)) (module TaskResult) ) - let write entrystates = + let write yaml_validate_result entrystates = match !AnalysisState.verified with | Some false -> print_svcomp_result "ERROR (verify)" | _ -> - if get_string "witness.yaml.validate" <> "" then ( - match get_bool "witness.yaml.strict" with - | true when !YamlWitness.cnt_error > 0 -> - print_svcomp_result "ERROR (witness error)" - | true when !YamlWitness.cnt_unsupported > 0 -> - print_svcomp_result "ERROR (witness unsupported)" - | true when !YamlWitness.cnt_disabled > 0 -> - print_svcomp_result "ERROR (witness disabled)" - | _ when !YamlWitness.cnt_refuted > 0 -> - print_svcomp_result (Result.to_string (False None)) - | _ when !YamlWitness.cnt_unconfirmed > 0 -> - print_svcomp_result (Result.to_string Unknown) - | _ -> - write entrystates - ) - else + match yaml_validate_result with + | Some (Stdlib.Error msg) -> + print_svcomp_result ("ERROR (" ^ msg ^ ")") + | Some (Ok (Svcomp.Result.False _ | Unknown as result)) -> + print_svcomp_result (Result.to_string result) + | Some (Ok True) + | None -> write entrystates end diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 42254f30de..7134211d32 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -514,6 +514,15 @@ struct Timing.wrap "yaml witness" write () end +let init () = + match GobConfig.get_string "witness.yaml.validate" with + | "" -> () + | path -> + (* Check witness existence before doing the analysis. *) + if not (Sys.file_exists path) then ( + Logs.error "witness.yaml.validate: %s not found" path; + Svcomp.errorwith "witness missing" + ) module ValidationResult = struct @@ -581,7 +590,9 @@ struct let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.validate")) 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 @@ -840,5 +851,19 @@ struct let certificate_path = GobConfig.get_string "witness.yaml.certificate" in if certificate_path <> "" then - yaml_entries_to_file (List.rev yaml_entries') (Fpath.v certificate_path) + yaml_entries_to_file (List.rev yaml_entries') (Fpath.v certificate_path); + + match GobConfig.get_bool "witness.yaml.strict" with + | true when !cnt_error > 0 -> + Error "witness error" + | true when !cnt_unsupported > 0 -> + Error "witness unsupported" + | true when !cnt_disabled > 0 -> + Error "witness disabled" + | _ when !cnt_refuted > 0 -> + Ok (Svcomp.Result.False None) + | _ when !cnt_unconfirmed > 0 -> + Ok Unknown + | _ -> + Ok True end diff --git a/tests/regression/55-loop-unrolling/12-loop-no-overflows.c b/tests/regression/55-loop-unrolling/12-loop-no-overflows.c new file mode 100644 index 0000000000..03554e06c5 --- /dev/null +++ b/tests/regression/55-loop-unrolling/12-loop-no-overflows.c @@ -0,0 +1,37 @@ +// PARAM: --enable ana.int.interval_set +// extracted from SV-COMP task ldv-memsafety/memleaks_test12-2.i + +typedef unsigned int size_t; +struct ldv_list_head { + struct ldv_list_head *next, *prev; +}; +struct ldv_list_head ldv_global_msg_list = {&(ldv_global_msg_list), &(ldv_global_msg_list)}; +struct ldv_msg { + void *data; + struct ldv_list_head list; +}; + +static inline void __ldv_list_del(struct ldv_list_head *prev, struct ldv_list_head *next) { + next->prev = prev; + prev->next = next; +} + +static inline void ldv_list_del(struct ldv_list_head *entry) { + __ldv_list_del(entry->prev, entry->next); +} + +void ldv_msg_free(struct ldv_msg *msg) { + free(msg->data); + free(msg); +} + +// ldv_destroy_msgs +void main(void) { + struct ldv_msg *msg; + struct ldv_msg *n; + for (msg = ({ const typeof( ((typeof(*msg) *)0)->list ) *__mptr = ((&ldv_global_msg_list)->next); (typeof(*msg) *)( (char *)__mptr - ((size_t) &((typeof(*msg) *)0)->list) ); }), n = ({ const typeof( ((typeof(*(msg)) *)0)->list ) *__mptr = ((msg)->list.next); (typeof(*(msg)) *)( (char *)__mptr - ((size_t) &((typeof(*(msg)) *)0)->list) ); }); &msg->list != (&ldv_global_msg_list); msg = n, n = ({ const typeof( ((typeof(*(n)) *)0)->list ) *__mptr = ((n)->list.next); (typeof(*(n)) *)( (char *)__mptr - ((size_t) &((typeof(*(n)) *)0)->list) ); })) // NOWARN + { + ldv_list_del(&msg->list); + ldv_msg_free(msg); + } +} \ No newline at end of file diff --git a/tests/regression/55-loop-unrolling/13-unrolled-loop-no-overflows.c b/tests/regression/55-loop-unrolling/13-unrolled-loop-no-overflows.c new file mode 100644 index 0000000000..84700ac9da --- /dev/null +++ b/tests/regression/55-loop-unrolling/13-unrolled-loop-no-overflows.c @@ -0,0 +1,72 @@ +// PARAM: --enable ana.int.interval_set +// extracted from SV-COMP task ldv-memsafety/memleaks_test12-2.i with --set exp.unrolling-factor 1 + +typedef unsigned int size_t; +struct ldv_list_head { + struct ldv_list_head *next, *prev; +}; +struct ldv_list_head ldv_global_msg_list = {&(ldv_global_msg_list), &(ldv_global_msg_list)}; +struct ldv_msg { + void *data; + struct ldv_list_head list; +}; + +__inline static void __ldv_list_del(struct ldv_list_head *prev, struct ldv_list_head *next) { + next->prev = prev; + prev->next = next; + return; +} + +__inline static void ldv_list_del(struct ldv_list_head *entry) { + __ldv_list_del(entry->prev, entry->next); + return; +} + +void ldv_msg_free(struct ldv_msg *msg) { + free(msg->data); + free((void *)msg); + return; +} + +// ldv_destroy_msgs +void main(void) { + struct ldv_msg *msg; + struct ldv_msg *n; + struct ldv_list_head const *__mptr; + struct ldv_list_head const *__mptr___0; + struct ldv_list_head const *__mptr___1; + + __mptr = (struct ldv_list_head const *)ldv_global_msg_list.next; + msg = (struct ldv_msg *)((char *)__mptr - (size_t)(&((struct ldv_msg *)0)->list)); + __mptr___0 = (struct ldv_list_head const *)msg->list.next; + n = (struct ldv_msg *)((char *)__mptr___0 - (size_t)(&((struct ldv_msg *)0)->list)); + + if (!((unsigned long)(&msg->list) != (unsigned long)(&ldv_global_msg_list))) { // NOWARN + goto loop_end; + } + + ldv_list_del(&msg->list); + ldv_msg_free(msg); + msg = n; + __mptr___1 = (struct ldv_list_head const *)n->list.next; + n = (struct ldv_msg *)((char *)__mptr___1 - (size_t)(&((struct ldv_msg *)0)->list)); + + loop_continue_0: /* CIL Label */; + { + while (1) { + while_continue: /* CIL Label */; + if (!((unsigned long)(&msg->list) != (unsigned long)(&ldv_global_msg_list))) { + goto while_break; + } + + ldv_list_del(&msg->list); + ldv_msg_free(msg); + msg = n; + __mptr___1 = (struct ldv_list_head const *)n->list.next; + n = (struct ldv_msg *)((char *)__mptr___1 - (size_t)(&((struct ldv_msg *)0)->list)); + } + while_break: /* CIL Label */; + } + loop_end: /* CIL Label */; + return; +} \ No newline at end of file