Skip to content

Commit

Permalink
Merge branch 'master' into affineeq-refine
Browse files Browse the repository at this point in the history
  • Loading branch information
DrMichaelPetter authored Dec 17, 2024
2 parents 6bd7861 + b68df11 commit 18effef
Show file tree
Hide file tree
Showing 96 changed files with 7,788 additions and 3,968 deletions.
139 changes: 139 additions & 0 deletions conf/svcomp-ghost.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,139 @@
{
"ana": {
"sv-comp": {
"enabled": true,
"functions": true
},
"int": {
"def_exc": true,
"enums": false,
"interval": true
},
"float": {
"interval": true,
"evaluate_math_functions": true
},
"activated": [
"base",
"threadid",
"threadflag",
"threadreturn",
"mallocWrapper",
"mutexEvents",
"mutex",
"access",
"race",
"escape",
"expRelation",
"mhp",
"assert",
"var_eq",
"symb_locks",
"region",
"thread",
"threadJoins",
"abortUnless",
"mutexGhosts",
"pthreadMutexType"
],
"path_sens": [
"mutex",
"malloc_null",
"uninit",
"expsplit",
"activeSetjmp",
"memLeak",
"threadflag"
],
"context": {
"widen": false
},
"base": {
"arrays": {
"domain": "partitioned"
},
"invariant": {
"local": false,
"global": true
}
},
"relation": {
"invariant": {
"local": false,
"global": true,
"one-var": false
}
},
"apron": {
"invariant": {
"diff-box": true
}
},
"var_eq": {
"invariant": {
"enabled": false
}
},
"race": {
"free": false,
"call": false
},
"autotune": {
"enabled": true,
"activated": [
"singleThreaded",
"mallocWrappers",
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
"noOverflows",
"termination",
"tmpSpecialAnalysis"
]
}
},
"exp": {
"region-offsets": true
},
"solver": "td3",
"sem": {
"unknown_function": {
"spawn": false
},
"int": {
"signed_overflow": "assume_none"
},
"null-pointer": {
"dereference": "assume_none"
}
},
"witness": {
"graphml": {
"enabled": false
},
"yaml": {
"enabled": true,
"format-version": "2.1",
"entry-types": [
"flow_insensitive_invariant",
"ghost_instrumentation"
]
},
"invariant": {
"loop-head": true,
"after-lock": true,
"other": true,
"accessed": false,
"exact": true,
"all-locals": false,
"flow_insensitive-as": "invariant_set-location_invariant"
}
},
"pre": {
"enabled": false
}
}
298 changes: 298 additions & 0 deletions docs/artifact-descriptions/vmcai25.md

Large diffs are not rendered by default.

12 changes: 6 additions & 6 deletions goblint.opam
Original file line number Diff line number Diff line change
Expand Up @@ -96,14 +96,14 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
# on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
# also remember to generate/adjust goblint.opam.locked!
available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
# pin-depends: [
# published goblint-cil 2.0.5 is currently up-to-date, so no pin needed
# [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
pin-depends: [
# published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
[ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
# [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
[ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
# [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
# ]
[ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
]
depexts: [
["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
]
Expand Down
14 changes: 14 additions & 0 deletions goblint.opam.locked
Original file line number Diff line number Diff line change
Expand Up @@ -137,6 +137,20 @@ conflicts: [
post-messages: [
"Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
]
pin-depends: [
[
"goblint-cil.2.0.5"
"git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd"
]
[
"camlidl.1.12"
"git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0"
]
[
"apron.v0.9.15"
"git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a"
]
]
depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
description: """\
Goblint is a sound static analysis framework for C programs using abstract interpretation.
Expand Down
12 changes: 6 additions & 6 deletions goblint.opam.template
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
# on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
# also remember to generate/adjust goblint.opam.locked!
available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
# pin-depends: [
# published goblint-cil 2.0.5 is currently up-to-date, so no pin needed
# [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
pin-depends: [
# published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
[ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
# [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
[ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
# [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
# ]
[ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
]
depexts: [
["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
]
Expand Down
2 changes: 1 addition & 1 deletion gobview
Submodule gobview updated 2 files
+1 −1 gobview.opam.locked
+0 −2 src/dune
1 change: 1 addition & 0 deletions mkdocs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -41,3 +41,4 @@ nav:
- "🇸 SAS '21": artifact-descriptions/sas21.md
- "🇪 ESOP '23": artifact-descriptions/esop23.md
- "🇻 VMCAI '24": artifact-descriptions/vmcai24.md
- "🇻 VMCAI '25": artifact-descriptions/vmcai25.md
7 changes: 7 additions & 0 deletions scripts/goblint-lib-modules.py
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,13 @@

"MessageCategory", # included in Messages
"PreValueDomain", # included in ValueDomain
"IntervalDomain", # included in IntDomain
"IntervalSetDomain", # included in IntDomain
"DefExcDomain", # included in IntDomain
"EnumsDomain", # included in IntDomain
"CongruenceDomain", # included in IntDomain
"IntDomTuple", # included in IntDomain
"WitnessGhostVar", # included in WitnessGhost

"ConfigVersion",
"ConfigProfile",
Expand Down
12 changes: 12 additions & 0 deletions src/analyses/apron/relationAnalysis.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -634,6 +634,15 @@ struct
)
|> Enum.fold (fun acc x -> Invariant.(acc && of_exp x)) Invariant.none

let query_invariant_global ctx g =
if GobConfig.get_bool "ana.relation.invariant.global" && ctx.ask (GhostVarAvailable Multithreaded) then (
let var = WitnessGhost.to_varinfo Multithreaded in
let inv = Priv.invariant_global (Analyses.ask_of_ctx ctx) ctx.global g in
Invariant.(of_exp (UnOp (LNot, Lval (GoblintCil.var var), GoblintCil.intType)) || inv) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
)
else
Invariant.none

let query ctx (type a) (q: a Queries.t): a Queries.result =
let open Queries in
let st = ctx.local in
Expand All @@ -655,6 +664,9 @@ struct
let vf' x = vf (Obj.repr x) in
Priv.iter_sys_vars ctx.global vq vf'
| Queries.Invariant context -> query_invariant ctx context
| Queries.InvariantGlobal g ->
let g: V.t = Obj.obj g in
query_invariant_global ctx g
| _ -> Result.top q


Expand Down
42 changes: 42 additions & 0 deletions src/analyses/apron/relationPriv.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,9 @@ module type S =
val thread_return: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> ThreadIdDomain.Thread.t -> relation_components_t -> relation_components_t
val iter_sys_vars: (V.t -> G.t) -> VarQuery.t -> V.t VarQuery.f -> unit (** [Queries.IterSysVars] for apron. *)

val invariant_global: Q.ask -> (V.t -> G.t) -> V.t -> Invariant.t
(** Returns flow-insensitive invariant for global unknown. *)

val invariant_vars: Q.ask -> (V.t -> G.t) -> relation_components_t -> varinfo list
(** Returns global variables which are privatized. *)

Expand Down Expand Up @@ -137,6 +140,7 @@ struct
{rel = RD.top (); priv = startstate ()}

let iter_sys_vars getg vq vf = ()
let invariant_global ask getg g = Invariant.none
let invariant_vars ask getg st = []

let init () = ()
Expand Down Expand Up @@ -424,6 +428,7 @@ struct
{rel = getg (); priv = startstate ()}

let iter_sys_vars getg vq vf = () (* TODO: or report singleton global for any Global query? *)
let invariant_global ask getg g = Invariant.none
let invariant_vars ask getg st = protected_vars ask (* TODO: is this right? *)

let finalize () = ()
Expand Down Expand Up @@ -708,6 +713,41 @@ struct

let init () = ()
let finalize () = ()

let invariant_global (ask: Q.ask) (getg: V.t -> G.t): V.t -> Invariant.t = function
| `Left m' -> (* mutex *)
let atomic = LockDomain.MustLock.equal m' (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in
if atomic || ask.f (GhostVarAvailable (Locked m')) then (
(* filters like query_invariant *)
let one_var = GobConfig.get_bool "ana.relation.invariant.one-var" in
let exact = GobConfig.get_bool "witness.invariant.exact" in

let rel = keep_only_protected_globals ask m' (get_m_with_mutex_inits ask getg m') in (* Could be more precise if mutex_inits invariant is added by disjunction instead of joining abstract values. *)
let inv =
RD.invariant rel
|> List.enum
|> Enum.filter_map (fun (lincons1: Apron.Lincons1.t) ->
(* filter one-vars and exact *)
(* TODO: exact filtering doesn't really work with octagon because it returns two SUPEQ constraints instead *)
if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
RD.cil_exp_of_lincons1 lincons1
|> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp))
else
None
)
|> Enum.fold (fun acc x -> Invariant.(acc && of_exp x)) Invariant.none
in
if atomic then
inv
else (
let var = WitnessGhost.to_varinfo (Locked m') in
Invariant.(of_exp (Lval (GoblintCil.var var)) || inv) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
)
)
else
Invariant.none
| g -> (* global *)
Invariant.none (* Could output unprotected one-variable (so non-relational) invariants, but probably not very useful. [BasePriv] does those anyway. *)
end

(** May written variables. *)
Expand Down Expand Up @@ -1275,6 +1315,8 @@ struct
| _ -> ()

let finalize () = ()

let invariant_global ask getg g = Invariant.none
end

module TracingPriv = functor (Priv: S) -> functor (RD: RelationDomain.RD) ->
Expand Down
Loading

0 comments on commit 18effef

Please sign in to comment.