Merge branch 'master' into issue-1374-2

conf/svcomp2var.json

@@ -0,0 +1,146 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins" ,
+      "lin2vareq"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc",
+        "ldv_kzalloc"
+      ]
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "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": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true,
+      "exclude-vars": [
+        "tmp\\(___[0-9]+\\)?",
+        "cond",
+        "RETURN",
+        "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+        ".*____CPAchecker_TMP_[0-9]+",
+        "__VERIFIER_assert__cond",
+        "__ksymtab_.*",
+        "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+      ]
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}

docs/developer-guide/debugging.md

@@ -13,25 +13,25 @@ Goblint extensively uses [CIL's `Pretty`](https://people.eecs.berkeley.edu/~necu
 * Logging CIL values (e.g. an expression `exp`) using the corresponding pretty-printer `d_exp` from `Cil` module:
 
 ```ocaml
-Logs.debug "A CIL exp: %a\n" d_exp exp;
+Logs.debug "A CIL exp: %a" d_exp exp;
 ```
 
 * Logging Goblint's `Printable` values (e.g. a domain `D` element `d`) using the corresponding pretty-printer `D.pretty`:
 
 ```ocaml
-Logs.debug "A domain element: %a\n" D.pretty d;
+Logs.debug "A domain element: %a" D.pretty d;
 ```
 
 * Logging primitives (e.g. OCaml ints, strings, etc) using the standard [OCaml `Printf`](https://ocaml.org/api/Printf.html) specifiers:
 
 ```ocaml
-Logs.debug "An int and a string: %d %s\n" 42 "magic";
+Logs.debug "An int and a string: %d %s" 42 "magic";
 ```
 
 * Logging lists of pretty-printables (e.g. expressions list `exps`) using `d_list`:
 
 ```ocaml
-Logs.debug "Some expressions: %a\n" (d_list ", " d_exp) exps;
+Logs.debug "Some expressions: %a" (d_list ", " d_exp) exps;
 ```
 
 
@@ -42,7 +42,7 @@ Recompile with tracing enabled: `./scripts/trace_on.sh`.
 
 Instead of logging use a tracing function from the `Messages` module, which is often aliased to just `M` (and pick a relevant name instead of `mything`):
 ```ocaml
-if M.tracing then M.trace "mything" "A domain element: %a\n" D.pretty d;
+if M.tracing then M.trace "mything" "A domain element: %a" D.pretty d;
 ```
 
 Then run Goblint with the additional argument `--trace mything`.

dune-project

@@ -26,11 +26,11 @@
     (ocaml (>= 4.10))
     (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.
     (batteries (>= 3.5.1))
-    (zarith (>= 1.8))
+    (zarith (>= 1.10))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))
     ppx_deriving
-    ppx_deriving_hash
+    (ppx_deriving_hash (>= 0.1.2))
     (ppx_deriving_yojson (>= 3.7.0))
     (ounit2 :with-test)
     (qcheck-ounit :with-test)

goblint.opam

@@ -24,11 +24,11 @@ depends: [
   "ocaml" {>= "4.10"}
   "goblint-cil" {>= "2.0.3"}
   "batteries" {>= "3.5.1"}
-  "zarith" {>= "1.8"}
+  "zarith" {>= "1.10"}
   "yojson" {>= "2.0.0"}
   "qcheck-core" {>= "0.19"}
   "ppx_deriving"
-  "ppx_deriving_hash"
+  "ppx_deriving_hash" {>= "0.1.2"}
   "ppx_deriving_yojson" {>= "3.7.0"}
   "ounit2" {with-test}
   "qcheck-ounit" {with-test}

goblint.opam.locked

@@ -82,7 +82,7 @@ depends: [
   "pp" {= "1.1.2"}
   "ppx_derivers" {= "1.2.1"}
   "ppx_deriving" {= "5.2.1"}
-  "ppx_deriving_hash" {= "0.1.1"}
+  "ppx_deriving_hash" {= "0.1.2"}
   "ppx_deriving_yojson" {= "3.7.0"}
   "ppxlib" {= "0.28.0"}
   "qcheck-core" {= "0.20"}

src/analyses/abortUnless.ml

@@ -11,7 +11,7 @@ struct
 
   let name () = "abortUnless"
   module D = BoolDomain.MustBool
-  module C = Lattice.Unit
+  module C = Printable.Unit
 
   let context _ _ = ()
 

src/analyses/accessAnalysis.ml

@@ -14,7 +14,7 @@ struct
   let name () = "access"
 
   module D = Lattice.Unit
-  module C = Lattice.Unit
+  module C = Printable.Unit
 
   module V =
   struct
@@ -32,7 +32,7 @@ struct
     emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
 
   let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (e:exp) =
-    if M.tracing then M.trace "access" "do_access %a %a %B\n" d_exp e AccessKind.pretty kind reach;
+    if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach;
     let reach_or_mpt: _ Queries.t = if reach then ReachableFrom e else MayPointTo e in
     let ad = ctx.ask reach_or_mpt in
     ctx.emit (Access {exp=e; ad; kind; reach})
@@ -42,15 +42,15 @@ struct
       + [deref=true], [reach=false] - Access [exp] by dereferencing once (may-point-to), used for lval writes and shallow special accesses.
       + [deref=true], [reach=true] - Access [exp] by dereferencing transitively (reachable), used for deep special accesses. *)
   let access_one_top ?(force=false) ?(deref=false) ctx (kind: AccessKind.t) reach exp =
-    if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)\n" CilType.Exp.pretty exp AccessKind.pretty kind reach deref;
+    if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)" CilType.Exp.pretty exp AccessKind.pretty kind reach deref;
     if force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) then (
       if deref && Cil.isPointerType (Cilfacade.typeOf exp) then (* avoid dereferencing integers to unknown pointers, which cause many spurious type-based accesses *)
         do_access ctx kind reach exp;
-      if M.tracing then M.tracei "access" "distribute_access_exp\n";
+      if M.tracing then M.tracei "access" "distribute_access_exp";
       Access.distribute_access_exp (do_access ctx Read false) exp;
-      if M.tracing then M.traceu "access" "distribute_access_exp\n";
+      if M.tracing then M.traceu "access" "distribute_access_exp";
     );
-    if M.tracing then M.traceu "access" "access_one_top\n"
+    if M.tracing then M.traceu "access" "access_one_top"
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()

src/analyses/activeLongjmp.ml

@@ -5,15 +5,12 @@ open Analyses
 
 module Spec =
 struct
-  include Analyses.IdentitySpec
+  include Analyses.IdentityUnitContextsSpec
 
   let name () = "activeLongjmp"
 
   (* The first component are the longjmp targets, the second are the longjmp callers *)
   module D = JmpBufDomain.ActiveLongjmps
-  module C = Lattice.Unit
-
-  let context _ _ = ()
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     let desc = LibraryFunctions.find f in

src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml

@@ -0,0 +1,31 @@
+(** {{!RelationAnalysis} Relational integer value analysis} using an OCaml implementation of the linear two-variable equalities domain ([lin2vareq]).
+
+    @see <http://doi.acm.org/10.1145/2049706.2049710> A. Flexeder, M. Petter, and H. Seidl Fast Interprocedural Linear Two-Variable Equalities. *)
+
+open Analyses
+include RelationAnalysis
+
+let spec_module: (module MCPSpec) Lazy.t =
+  lazy (
+    let module AD = LinearTwoVarEqualityDomain.D2
+    in
+    let module Priv = (val RelationPriv.get_priv ()) in
+    let module Spec =
+    struct
+      include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil)
+      let name () = "lin2vareq"
+    end
+    in
+    (module Spec)
+  )
+
+let get_spec (): (module MCPSpec) =
+  Lazy.force spec_module
+
+let after_config () =
+  let module Spec = (val get_spec ()) in
+  MCP.register_analysis (module Spec : MCPSpec);
+  GobConfig.set_string "ana.path_sens[+]"  (Spec.name ())
+
+let _ =
+  AfterConfig.register after_config

src/analyses/apron/linearTwoVarEqualityAnalysis.no-apron.ml

@@ -0,0 +1,3 @@
+(* This analysis is empty on purpose. It serves only as an alternative dependency
+   in cases where the actual domain can't be used because of a missing library.
+   It was added because we don't want to fully depend on Apron. *)