IntDomain code optimizations

README.md

@@ -1,4 +1,5 @@
 # Goblint
+
 [![locked workflow status](https://github.com/goblint/analyzer/actions/workflows/locked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/locked.yml)
 [![unlocked workflow status](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml)
 [![docker workflow status](https://github.com/goblint/analyzer/actions/workflows/docker.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/docker.yml)
@@ -10,45 +11,57 @@
 Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/en/latest/) or [GitHub](./docs/).
 
 ## Installing
+
 Both for using an up-to-date version of Goblint or developing it, the best way is to install from source by cloning this repository.
 
 ### Linux
+
 1. Install [opam](https://opam.ocaml.org/doc/Install.html).
 2. Make sure the following are installed: `git`, `patch`, `m4`, `autoconf`, `libgmp-dev`, `libmpfr-dev` and `pkg-config`.
 3. Run `make setup` to install OCaml and dependencies via opam.
+   1. In case Goblint needs to be compiled with `flambda` optimizations, then run `make setup-flambda` instead
 4. Run `make` to build Goblint itself.
 5. Run `make install` to install Goblint into the opam switch for usage via switch's `PATH`.
 
 ### MacOS
+
 1. Install GCC with `brew install gcc` (first run `xcode-select --install` if you don't want to build it from source). Goblint requires GCC while macOS's default `cpp` is Clang, which will not work.
 2. ONLY for M1 (ARM64) processor: homebrew changed its install location from `/usr/local/` to `/opt/homebrew/`. For packages to find their dependecies execute `sudo ln -s /opt/homebrew/{include,lib} /usr/local/`.
 3. Continue using Linux instructions (the formulae in brew for `patch`, `libgmp-dev`, `libmpfr-dev` are `gpatch`, `gmp`, `mpfr`, respectively).
 
 ### Windows
+
 1. Install [WSL2](https://docs.microsoft.com/en-us/windows/wsl/install-win10). Goblint is not compatible with WSL1.
 2. Continue using Linux instructions in WSL.
 
 ### Other
-* **[opam](https://opam.ocaml.org/packages/goblint/)**. Install [opam](https://opam.ocaml.org/doc/Install.html) and run `opam install goblint`.
-* **[devcontainer](./.devcontainer/).** Select "Reopen in Container" in VS Code and continue with `make` using Linux instructions in devcontainer.
-* **[Docker (GitHub Container Registry)](https://github.com/goblint/analyzer/pkgs/container/analyzer)**. Run `docker pull ghcr.io/goblint/analyzer:latest` (or `:nightly`).
-* **Docker (repository).** Clone and run `docker build -t goblint .`.
-* **Vagrant.** Clone and run `vagrant up && vagrant ssh`.
 
+- **[opam](https://opam.ocaml.org/packages/goblint/)**. Install [opam](https://opam.ocaml.org/doc/Install.html) and run `opam install goblint`.
+- **[devcontainer](./.devcontainer/).** Select "Reopen in Container" in VS Code and continue with `make` using Linux instructions in devcontainer.
+- **[Docker (GitHub Container Registry)](https://github.com/goblint/analyzer/pkgs/container/analyzer)**. Run `docker pull ghcr.io/goblint/analyzer:latest` (or `:nightly`).
+- **Docker (repository).** Clone and run `docker build -t goblint .`.
+- **Vagrant.** Clone and run `vagrant up && vagrant ssh`.
 
 ## Running
+
 To confirm that building worked, you can try running Goblint as follows:
+
 ```
 ./goblint tests/regression/04-mutex/01-simple_rc.c
 ```
+
 To confirm that installation into the opam switch worked, you can try running Goblint as follows:
+
 ```
 goblint tests/regression/04-mutex/01-simple_rc.c
 ```
+
 To confirm that the Docker container worked, you can try running Goblint as follows:
+
 ```
 docker run -it --rm -v $(pwd):/data goblint /data/tests/regression/04-mutex/01-simple_rc.c
 ```
+
 If pulled from GitHub Container Registry, use the container name `ghcr.io/goblint/analyzer:latest` (or `:nightly`) instead.
 
 For further information, see [documentation](https://goblint.readthedocs.io/en/latest/user-guide/running/).

make.sh

@@ -11,6 +11,14 @@ opam_setup() {
   opam switch -y create . --deps-only ocaml-variants.4.14.0+options ocaml-option-flambda --locked
 }
 
+opam_setup_flambda() {
+  set -x
+  opam init -y -a --bare $SANDBOXING # sandboxing is disabled in travis and docker
+  opam update
+  # Note: the `--update-invariant` option is needed for replacement of the previous ocaml compiler switch invariant of Goblint
+  opam switch -y create . --deps-only ocaml-variants.4.14.0+options ocaml-option-flambda --locked --update-invariant
+}
+
 rule() {
   case $1 in
     # new rules using dune
@@ -77,6 +85,12 @@ rule() {
       echo "For running the regression tests you also need: ruby, gem, curl"
       echo "For reference see ./Dockerfile or ./scripts/travis-ci.sh"
       opam_setup
+    ;; setup-flambda)
+      echo "Make sure you have the following installed: opam >= 2.0.0, git, patch, m4, autoconf, libgmp-dev, libmpfr-dev, pkg-config"
+      echo "For the --html output you also need: javac, ant, dot (graphviz)"
+      echo "For running the regression tests you also need: ruby, gem, curl"
+      echo "For reference see ./Dockerfile or ./scripts/travis-ci.sh"
+      opam_setup_flambda
     ;; dev)
       eval $(opam env)
       echo "Installing opam packages for development..."

src/analyses/base.ml

@@ -133,7 +133,6 @@ struct
     in
     let a = if GobConfig.get_bool "annotation.goblint_array_domain" then array_attr else None in
     VD.project ask p a value
-
   let project ask p_opt cpa fundec =
     CPA.mapi (fun varinfo value -> project_val ask (attributes_varinfo varinfo fundec) p_opt value (is_privglob varinfo)) cpa
 

src/cdomains/intDomain.ml

@@ -15,6 +15,54 @@ exception Unknown
 exception Error
 exception ArithmeticOnIntegerBot of string
 
+
+
+
+(** Define records that hold mutable variables representing different Configuration values.
+  * These values are used to keep track of whether or not the corresponding Config values are en-/disabled  *)
+type ana_int_config_values = {
+  mutable interval_threshold_widening : bool option;
+  mutable interval_narrow_by_meet : bool option;
+  mutable def_exc_widen_by_join : bool option;
+  mutable interval_threshold_widening_constants : string option;
+  mutable refinement : string option;
+}
+
+let ana_int_config: ana_int_config_values = {
+  interval_threshold_widening = None;
+  interval_narrow_by_meet = None;
+  def_exc_widen_by_join = None;
+  interval_threshold_widening_constants = None;
+  refinement = None;
+}
+
+let get_interval_threshold_widening () =
+  if ana_int_config.interval_threshold_widening = None then 
+    ana_int_config.interval_threshold_widening <- Some (get_bool "ana.int.interval_threshold_widening");
+  Option.get ana_int_config.interval_threshold_widening
+
+let get_interval_narrow_by_meet () =
+  if ana_int_config.interval_narrow_by_meet = None then
+    ana_int_config.interval_narrow_by_meet <- Some (get_bool "ana.int.interval_narrow_by_meet");
+  Option.get ana_int_config.interval_narrow_by_meet
+
+let get_def_exc_widen_by_join () = 
+  if ana_int_config.def_exc_widen_by_join = None then 
+    ana_int_config.def_exc_widen_by_join <- Some (get_bool "ana.int.def_exc_widen_by_join");
+  Option.get ana_int_config.def_exc_widen_by_join
+
+let get_interval_threshold_widening_constants () =
+  if ana_int_config.interval_threshold_widening_constants = None then
+    ana_int_config.interval_threshold_widening_constants <- Some (get_string "ana.int.interval_threshold_widening_constants");
+  Option.get ana_int_config.interval_threshold_widening_constants
+
+let get_refinement () =
+  if ana_int_config.refinement = None then
+    ana_int_config.refinement <- Some (get_string "ana.int.refinement");
+  Option.get ana_int_config.refinement
+
+
+
 (** Whether for a given ikind, we should compute with wrap-around arithmetic.
   *  Always for unsigned types, for signed types if 'sem.int.signed_overflow' is 'assume_wraparound'  *)
 let should_wrap ik = not (Cil.isSigned ik) || get_string "sem.int.signed_overflow" = "assume_wraparound"
@@ -616,15 +664,15 @@ struct
     | None, z | z, None -> z
     | Some (l0,u0), Some (l1,u1) ->
       let (min_ik, max_ik) = range ik in
-      let threshold = get_bool "ana.int.interval_threshold_widening" in
+      let threshold = get_interval_threshold_widening () in
       let upper_threshold u =
-        let ts = if GobConfig.get_string "ana.int.interval_threshold_widening_constants" = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in
+        let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in
         let u = Ints_t.to_bigint u in
         let t = List.find_opt (fun x -> Z.compare u x <= 0) ts in
         BatOption.map_default Ints_t.of_bigint max_ik t
       in
       let lower_threshold l =
-        let ts = if GobConfig.get_string "ana.int.interval_threshold_widening_constants" = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in
+        let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in
         let l = Ints_t.to_bigint l in
         let t = List.find_opt (fun x -> Z.compare l x >= 0) ts in
         BatOption.map_default Ints_t.of_bigint min_ik t
@@ -649,8 +697,9 @@ struct
       let ur = if Ints_t.compare max_ik x2 = 0 then y2 else x2 in
       norm ik @@ Some (lr,ur)
 
+
   let narrow ik x y =
-    if get_bool "ana.int.interval_narrow_by_meet" then
+    if get_interval_narrow_by_meet () then
       meet ik x y
     else
       narrow ik x y
@@ -1412,8 +1461,9 @@ struct
 
   let join ik = join' ik
 
+
   let widen ik x y =
-    if get_bool "ana.int.def_exc_widen_by_join" then
+    if get_def_exc_widen_by_join () then
       join' ik x y
     else if equal x y then
       x
@@ -2752,7 +2802,7 @@ module IntDomTupleImpl = struct
 
   let refine ik ((a, b, c, d ) : t ) : t =
     let dt = ref (a, b, c, d) in
-    (match GobConfig.get_string "ana.int.refinement" with
+    (match get_refinement () with
       | "never" -> ()
       | "once" ->
          List.iter (fun f -> dt := f !dt) (refine_functions ik);