From af781ed684c538cfa98ef0d35a9d258fec62e495 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 20 Jun 2024 12:56:40 +0300
Subject: [PATCH 01/25] Enable ana.float.evaluate_math_functions in svcomp24
 and svcomp confs

This is needed for sv-benchmarks Juliet no-overflow tasks involving sqrt.
We used this at SV-COMP 2024, before the option existed.
---
 conf/svcomp.json            | 3 ++-
 conf/svcomp24-validate.json | 3 ++-
 conf/svcomp24.json          | 3 ++-
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/conf/svcomp.json b/conf/svcomp.json
index 467d294bdd..d2bea96040 100644
--- a/conf/svcomp.json
+++ b/conf/svcomp.json
@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",
diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json
index 7832ffa6af..d83b1767a4 100644
--- a/conf/svcomp24-validate.json
+++ b/conf/svcomp24-validate.json
@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",
diff --git a/conf/svcomp24.json b/conf/svcomp24.json
index 7e30554ceb..1c60f84920 100644
--- a/conf/svcomp24.json
+++ b/conf/svcomp24.json
@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",

From 3ff00aea295c6e7386323efc88f38d1a046cbdbc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 20 Jun 2024 13:00:36 +0300
Subject: [PATCH 02/25] Add tests for imaxabs

---
 .../39-signed-overflows/11-imaxabs.c          | 24 +++++++++++++++++++
 .../39-signed-overflows/12-imaxabs-sqrt.c     | 12 ++++++++++
 2 files changed, 36 insertions(+)
 create mode 100644 tests/regression/39-signed-overflows/11-imaxabs.c
 create mode 100644 tests/regression/39-signed-overflows/12-imaxabs-sqrt.c

diff --git a/tests/regression/39-signed-overflows/11-imaxabs.c b/tests/regression/39-signed-overflows/11-imaxabs.c
new file mode 100644
index 0000000000..dce200a146
--- /dev/null
+++ b/tests/regression/39-signed-overflows/11-imaxabs.c
@@ -0,0 +1,24 @@
+//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial
+#include<stdlib.h>
+#include <stdint.h>
+#include <inttypes.h>
+int main() {
+    int64_t data;
+    if (data > (-0x7fffffffffffffff - 1))
+    {
+        if (imaxabs(data) < 100)
+        {
+            __goblint_check(data < 100); // TODO
+            __goblint_check(-100 < data); // TODO
+            int64_t result = data * data; // TODO NOWARN
+        }
+
+        if(imaxabs(data) <= 100)
+        {
+            __goblint_check(data <= 100); // TODO
+            __goblint_check(-100 <= data); // TODO
+            int64_t result = data * data; // TODO NOWARN
+        }
+    }
+    return 8;
+}
diff --git a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c
new file mode 100644
index 0000000000..b121645b27
--- /dev/null
+++ b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c
@@ -0,0 +1,12 @@
+//PARAM: --enable ana.int.interval --enable ana.float.interval --enable ana.float.evaluate_math_functions --set ana.activated[+] tmpSpecial
+#include<math.h>
+#include <stdint.h>
+#include <inttypes.h>
+int main() {
+    int64_t data;
+    if (data > (-0x7fffffffffffffff - 1) && imaxabs((intmax_t)data) <= sqrtl(0x7fffffffffffffffLL))
+    {
+        int64_t result = data * data; // TODO NOWARN
+    }
+    return 8;
+}

From 2653e2ea22dd9d012a10e008f3189e1061d2c344 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 20 Jun 2024 13:02:26 +0300
Subject: [PATCH 03/25] Add hacky imaxabs support

---
 src/util/library/libraryFunctions.ml              |  2 +-
 tests/regression/39-signed-overflows/11-imaxabs.c | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index e7ff2a4d04..df90339c65 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -139,7 +139,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("abs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (IInt, j)) });
     ("labs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) });
     ("llabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILongLong, j)) });
-    ("imaxabs", unknown [drop "j" []]);
+    ("imaxabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) }); (* TODO: look up intmax_t ikind from CIL file *)
     ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
     ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
diff --git a/tests/regression/39-signed-overflows/11-imaxabs.c b/tests/regression/39-signed-overflows/11-imaxabs.c
index dce200a146..47bd26569f 100644
--- a/tests/regression/39-signed-overflows/11-imaxabs.c
+++ b/tests/regression/39-signed-overflows/11-imaxabs.c
@@ -8,16 +8,16 @@ int main() {
     {
         if (imaxabs(data) < 100)
         {
-            __goblint_check(data < 100); // TODO
-            __goblint_check(-100 < data); // TODO
-            int64_t result = data * data; // TODO NOWARN
+            __goblint_check(data < 100);
+            __goblint_check(-100 < data);
+            int64_t result = data * data; // NOWARN
         }
 
         if(imaxabs(data) <= 100)
         {
-            __goblint_check(data <= 100); // TODO
-            __goblint_check(-100 <= data); // TODO
-            int64_t result = data * data; // TODO NOWARN
+            __goblint_check(data <= 100);
+            __goblint_check(-100 <= data);
+            int64_t result = data * data; // NOWARN
         }
     }
     return 8;

From f9765da81d64a99f77c385835c6c0a5c3db419da Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 20 Jun 2024 13:05:26 +0300
Subject: [PATCH 04/25] Add hacky imaxabs sqrt refine support

---
 src/analyses/baseInvariant.ml                          | 3 ++-
 tests/regression/39-signed-overflows/12-imaxabs-sqrt.c | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 51a27e19f8..d5b65a95f4 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -785,7 +785,8 @@ struct
            | TFloat (fk, _), FLongDouble
            | TFloat (FDouble as fk, _), FDouble
            | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
-           | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st)
+           | TInt (ik, _), _ -> inv_exp (Int (FD.to_int ik c)) e st (* TODO: is this cast refinement correct? *)
+           | t, fk -> fallback (fun () -> Pretty.dprintf "CastE: incompatible types %a and %a" CilType.Typ.pretty t CilType.Fkind.pretty fk) st)
         | CastE ((TInt (ik, _)) as t, e), Int c
         | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
           (match eval e st with
diff --git a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c
index b121645b27..46512aed21 100644
--- a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c
+++ b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c
@@ -6,7 +6,7 @@ int main() {
     int64_t data;
     if (data > (-0x7fffffffffffffff - 1) && imaxabs((intmax_t)data) <= sqrtl(0x7fffffffffffffffLL))
     {
-        int64_t result = data * data; // TODO NOWARN
+        int64_t result = data * data; // NOWARN
     }
     return 8;
 }

From a1f0b35703e34da0eda8f3f27ea260a58fd2c85d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 20 Jun 2024 13:15:01 +0300
Subject: [PATCH 05/25] Find intmax_t for imaxabs from program

---
 src/util/library/libraryFunctions.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index df90339c65..689eb17126 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -6,6 +6,16 @@ open GobConfig
 
 module M = Messages
 
+let intmax_t = lazy (
+  let res = ref None in
+  GoblintCil.iterGlobals !Cilfacade.current_file (function
+      | GType ({tname = "intmax_t"; ttype; _}, _) ->
+        res := Some ttype;
+      | _ -> ()
+    );
+  !res
+)
+
 (** C standard library functions.
     These are specified by the C standard. *)
 let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -139,7 +149,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("abs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (IInt, j)) });
     ("labs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) });
     ("llabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILongLong, j)) });
-    ("imaxabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) }); (* TODO: look up intmax_t ikind from CIL file *)
+    ("imaxabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (Cilfacade.get_ikind (Option.get (Lazy.force intmax_t)), j)) });
     ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
     ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)

From 67f8fe9195d3c6a96b01a0a5ceddf05a81fb1ff6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 9 Oct 2024 10:28:06 +0300
Subject: [PATCH 06/25] Add test for invariant_set widening tokens (issue
 #1299)

---
 .../56-witness/64-apron-unassume-set-tokens.c | 18 ++++++
 .../64-apron-unassume-set-tokens.yml          | 59 +++++++++++++++++++
 tests/regression/56-witness/dune              |  3 +-
 3 files changed, 79 insertions(+), 1 deletion(-)
 create mode 100644 tests/regression/56-witness/64-apron-unassume-set-tokens.c
 create mode 100644 tests/regression/56-witness/64-apron-unassume-set-tokens.yml

diff --git a/tests/regression/56-witness/64-apron-unassume-set-tokens.c b/tests/regression/56-witness/64-apron-unassume-set-tokens.c
new file mode 100644
index 0000000000..75a6b5eee5
--- /dev/null
+++ b/tests/regression/56-witness/64-apron-unassume-set-tokens.c
@@ -0,0 +1,18 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 64-apron-unassume-set-tokens.yml --set ana.apron.domain polyhedra --enable ana.widen.tokens
+#include <assert.h>
+// Uses polyhedra instead of octagon such that widening tokens are actually needed by test instead of narrowing.
+// Copied & extended from 56-witness/12-apron-unassume-branch.
+int main() {
+  int i = 0;
+  while (i < 100) {
+    i++;
+  }
+  assert(i == 100);
+
+  int j = 0;
+  while (j < 100) {
+    j++;
+  }
+  assert(j == 100);
+  return 0;
+}
diff --git a/tests/regression/56-witness/64-apron-unassume-set-tokens.yml b/tests/regression/56-witness/64-apron-unassume-set-tokens.yml
new file mode 100644
index 0000000000..8411ed045f
--- /dev/null
+++ b/tests/regression/56-witness/64-apron-unassume-set-tokens.yml
@@ -0,0 +1,59 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "0.1"
+    uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e
+    creation_time: 2022-07-26T09:11:03Z
+    producer:
+      name: Goblint
+      version: heads/yaml-witness-unassume-0-g48503c690-dirty
+      command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression''
+        ''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled''
+        ''64-apron-unassume-set-tokens.c'''
+    task:
+      input_files:
+      - 64-apron-unassume-set-tokens.c
+      input_file_hashes:
+        64-apron-unassume-set-tokens.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 64-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 8
+        column: 3
+        function: main
+      value: 99LL - (long long )i >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 64-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 8
+        column: 3
+        function: main
+      value: (long long )i >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 64-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 14
+        column: 3
+        function: main
+      value: 99LL - (long long )j >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 64-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 14
+        column: 3
+        function: main
+      value: (long long )j >= 0LL
+      format: c_expression
diff --git a/tests/regression/56-witness/dune b/tests/regression/56-witness/dune
index 215e47deb2..f6694c60ec 100644
--- a/tests/regression/56-witness/dune
+++ b/tests/regression/56-witness/dune
@@ -21,7 +21,8 @@
      (run %{update_suite} hh-ex3 -q)
      (run %{update_suite} bh-ex1-poly -q)
      (run %{update_suite} apron-unassume-precheck -q)
-     (run %{update_suite} apron-tracked-global-annot -q)))))
+     (run %{update_suite} apron-tracked-global-annot -q)
+     (run %{update_suite} apron-unassume-set-tokens -q)))))
 
 (cram
  (deps (glob_files *.c) (glob_files ??-*.yml)))

From 7ec6b0578b6da2996114c8f9a60a75cb056fa231 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 8 Oct 2024 17:50:41 +0300
Subject: [PATCH 07/25] Add optional int indices to widening tokens

---
 src/analyses/apron/relationAnalysis.apron.ml |  4 ++--
 src/analyses/base.ml                         |  4 ++--
 src/analyses/unassumeAnalysis.ml             | 12 ++++++------
 src/domains/events.ml                        |  4 ++--
 src/lifters/wideningTokens.ml                |  3 +--
 src/lifters/wideningTokens0.ml               |  6 ++++++
 6 files changed, 19 insertions(+), 14 deletions(-)
 create mode 100644 src/lifters/wideningTokens0.ml

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index da14dfff1d..f82bd37e33 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -701,7 +701,7 @@ struct
       Priv.escape ctx.node (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st escaped
     | Assert exp ->
       assert_fn ctx exp true
-    | Events.Unassume {exp = e; uuids} ->
+    | Events.Unassume {exp = e; tokens} ->
       let e_orig = e in
       let ask = Analyses.ask_of_ctx ctx in
       let e = replace_deref_exps ctx.ask e in
@@ -737,7 +737,7 @@ struct
 
       (* TODO: parallel write_global? *)
       let st =
-        WideningTokens.with_side_tokens (WideningTokens.TS.of_list uuids) (fun () ->
+        WideningTokens.with_side_tokens (WideningTokens.TS.of_list tokens) (fun () ->
             VH.fold (fun v v_in st ->
                 (* TODO: is this sideg fine? *)
                 write_global ask ctx.global ctx.sideg st v v_in
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 1699108394..a5a9fc150e 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -3091,8 +3091,8 @@ struct
       set ~ctx ctx.local (eval_lv ~ctx ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid))
     | Events.Assert exp ->
       assert_fn ctx exp true
-    | Events.Unassume {exp; uuids} ->
-      Timing.wrap "base unassume" (unassume ctx exp) uuids
+    | Events.Unassume {exp; tokens} ->
+      Timing.wrap "base unassume" (unassume ctx exp) tokens
     | Events.Longjmped {lval} ->
       begin match lval with
         | Some lval ->
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 8f8892b8be..348215993b 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -29,7 +29,7 @@ struct
 
   type inv = {
     exp: Cil.exp;
-    uuid: string;
+    token: WideningTokens.Token.t;
   }
 
   let invs: inv NH.t = NH.create 100
@@ -101,7 +101,7 @@ struct
               match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with
               | Ok inv_exp ->
                 M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
-                NH.add invs n {exp = inv_exp; uuid}
+                NH.add invs n {exp = inv_exp; token = (uuid, None)} (* TODO: Some *)
               | Error e ->
                 M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv;
                 M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv
@@ -154,7 +154,7 @@ struct
                     M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
                     if not (NH.mem pre_invs n) then
                       NH.replace pre_invs n (EH.create 10);
-                    EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; uuid}
+                    EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; token = (uuid, None)} (* TODO: Some *)
                   | Error e ->
                     M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv;
                     M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv
@@ -262,9 +262,9 @@ struct
       M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e;
       if not !AnalysisState.postsolving then (
         if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (ctx.ask (EvalInt e)) = Some false) then (
-          let uuids = x.uuid :: List.map (fun {uuid; _} -> uuid) xs in
-          ctx.emit (Unassume {exp = e; uuids});
-          List.iter WideningTokens.add uuids
+          let tokens = x.token :: List.map (fun {token; _} -> token) xs in
+          ctx.emit (Unassume {exp = e; tokens});
+          List.iter WideningTokens.add tokens
         )
       );
       ctx.local
diff --git a/src/domains/events.ml b/src/domains/events.ml
index b194847bac..b3054b8416 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -14,7 +14,7 @@ type t =
   | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *) (* TODO: unused *)
   | UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *)
   | Assert of exp
-  | Unassume of {exp: CilType.Exp.t; uuids: string list}
+  | Unassume of {exp: CilType.Exp.t; tokens: WideningTokens0.Token.t list}
   | Longjmped of {lval: CilType.Lval.t option}
 
 (** Should event be emitted after transfer function raises [Deadcode]? *)
@@ -45,5 +45,5 @@ let pretty () = function
   | Assign {lval; exp} -> dprintf "Assign {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp
   | UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp
   | Assert exp -> dprintf "Assert %a" d_exp exp
-  | Unassume {exp; uuids} -> dprintf "Unassume {exp=%a; uuids=%a}" d_exp exp (docList Pretty.text) uuids
+  | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningTokens0.Token.pretty) tokens
   | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval
diff --git a/src/lifters/wideningTokens.ml b/src/lifters/wideningTokens.ml
index 41bb5d8477..4d60099d7e 100644
--- a/src/lifters/wideningTokens.ml
+++ b/src/lifters/wideningTokens.ml
@@ -6,8 +6,7 @@
 
     @see <http://www2.in.tum.de/bib/files/mihaila13widening.pdf> Mihaila, B., Sepp, A. & Simon, A. Widening as Abstract Domain. *)
 
-(** Widening token. *)
-module Token = Basetype.RawStrings (* Change to variant type if need other tokens than witness UUIDs. *)
+include WideningTokens0
 
 (** Widening token set. *)
 module TS = SetDomain.ToppedSet (Token) (struct let topname = "Top" end)
diff --git a/src/lifters/wideningTokens0.ml b/src/lifters/wideningTokens0.ml
new file mode 100644
index 0000000000..dcbf77424e
--- /dev/null
+++ b/src/lifters/wideningTokens0.ml
@@ -0,0 +1,6 @@
+(** Widening token. *)
+module Token =
+struct
+  (* Change to variant type if need other tokens than witness UUIDs. *)
+  include Printable.Prod (Basetype.RawStrings) (Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end))
+end

From 21c000c71bfae7e31fbc18d83d61a802dd854c03 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 8 Oct 2024 17:55:02 +0300
Subject: [PATCH 08/25] Add invariant_set index to widening token

---
 src/analyses/unassumeAnalysis.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 348215993b..6b5b495233 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -90,7 +90,7 @@ struct
       let uuid = entry.metadata.uuid in
       let target_type = YamlWitnessType.EntryType.entry_type entry.entry_type in
 
-      let unassume_nodes_invariant ~loc ~nodes inv =
+      let unassume_nodes_invariant ~loc ~nodes ?i inv =
         let msgLoc: M.Location.t = CilLocation loc in
         match InvariantParser.parse_cabs inv with
         | Ok inv_cabs ->
@@ -101,7 +101,7 @@ struct
               match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with
               | Ok inv_exp ->
                 M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
-                NH.add invs n {exp = inv_exp; token = (uuid, None)} (* TODO: Some *)
+                NH.add invs n {exp = inv_exp; token = (uuid, i)}
               | Error e ->
                 M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv;
                 M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv
@@ -154,7 +154,7 @@ struct
                     M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
                     if not (NH.mem pre_invs n) then
                       NH.replace pre_invs n (EH.create 10);
-                    EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; token = (uuid, None)} (* TODO: Some *)
+                    EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; token = (uuid, None)}
                   | Error e ->
                     M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv;
                     M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv
@@ -189,42 +189,42 @@ struct
 
       let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
 
-        let unassume_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
+        let unassume_location_invariant ~i (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
           let loc = YamlWitness.loc_of_location location_invariant.location in
           let inv = location_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
           match Locator.find_opt location_locator loc with
           | Some nodes ->
-            unassume_nodes_invariant ~loc ~nodes inv
+            unassume_nodes_invariant ~loc ~nodes ~i inv
           | None ->
             M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
         in
 
-        let unassume_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) =
+        let unassume_loop_invariant ~i (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) =
           let loc = YamlWitness.loc_of_location loop_invariant.location in
           let inv = loop_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
           match Locator.find_opt loop_locator loc with
           | Some nodes ->
-            unassume_nodes_invariant ~loc ~nodes inv
+            unassume_nodes_invariant ~loc ~nodes ~i inv
           | None ->
             M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
         in
 
-        let validate_invariant (invariant: YamlWitnessType.InvariantSet.Invariant.t) =
+        let validate_invariant i (invariant: YamlWitnessType.InvariantSet.Invariant.t) =
           let target_type = YamlWitnessType.InvariantSet.InvariantType.invariant_type invariant.invariant_type in
           match YamlWitness.invariant_type_enabled target_type, invariant.invariant_type with
           | true, LocationInvariant x ->
-            unassume_location_invariant x
+            unassume_location_invariant ~i x
           | true, LoopInvariant x ->
-            unassume_loop_invariant x
+            unassume_loop_invariant ~i x
           | false, (LocationInvariant _ | LoopInvariant _) ->
             M.info_noloc ~category:Witness "disabled invariant of type %s" target_type
         in
 
-        List.iter validate_invariant invariant_set.content
+        List.iteri validate_invariant invariant_set.content
       in
 
       match YamlWitness.entry_type_enabled target_type, entry.entry_type with

From 57a044713a03cd28d199fb16cd4c9b332b31f32d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 9 Oct 2024 10:35:11 +0300
Subject: [PATCH 09/25] Rename widening token modules

---
 src/analyses/apron/relationAnalysis.apron.ml         |  6 +++---
 src/analyses/base.ml                                 |  6 +++---
 src/analyses/mCP.ml                                  | 12 ++++++------
 src/analyses/unassumeAnalysis.ml                     |  4 ++--
 src/domains/events.ml                                |  4 ++--
 src/framework/control.ml                             |  2 +-
 src/goblint_lib.ml                                   |  3 ++-
 src/lifters/wideningToken.ml                         |  4 ++++
 .../{wideningTokens.ml => wideningTokenLifter.ml}    |  2 +-
 src/lifters/wideningTokens0.ml                       |  6 ------
 10 files changed, 24 insertions(+), 25 deletions(-)
 create mode 100644 src/lifters/wideningToken.ml
 rename src/lifters/{wideningTokens.ml => wideningTokenLifter.ml} (99%)
 delete mode 100644 src/lifters/wideningTokens0.ml

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index f82bd37e33..28e365bd97 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -690,7 +690,7 @@ struct
           Priv.lock ask ctx.global st m
         ) st addr
     | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
-      WideningTokens.with_local_side_tokens (fun () ->
+      WideningTokenLifter.with_local_side_tokens (fun () ->
           CommonPriv.lift_unlock ask (fun st m ->
               Priv.unlock ask ctx.global ctx.sideg st m
             ) st addr
@@ -737,7 +737,7 @@ struct
 
       (* TODO: parallel write_global? *)
       let st =
-        WideningTokens.with_side_tokens (WideningTokens.TS.of_list tokens) (fun () ->
+        WideningTokenLifter.with_side_tokens (WideningTokenLifter.TS.of_list tokens) (fun () ->
             VH.fold (fun v v_in st ->
                 (* TODO: is this sideg fine? *)
                 write_global ask ctx.global ctx.sideg st v v_in
@@ -771,7 +771,7 @@ struct
       let new_value = RD.join old_value st in
       PCU.RH.replace results ctx.node new_value;
     end;
-    WideningTokens.with_local_side_tokens (fun () ->
+    WideningTokenLifter.with_local_side_tokens (fun () ->
         Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread])
       )
 
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index a5a9fc150e..fcf720e5eb 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -447,7 +447,7 @@ struct
     in
     if M.tracing then M.tracel "sync" "sync multi=%B earlyglobs=%B" multi !earlyglobs;
     if !earlyglobs || multi then
-      WideningTokens.with_local_side_tokens (fun () ->
+      WideningTokenLifter.with_local_side_tokens (fun () ->
           Priv.sync (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) ctx.local reason
         )
     else
@@ -3058,7 +3058,7 @@ struct
     (* Perform actual [set]-s with final unassumed values.
        This invokes [Priv.write_global], which was suppressed above. *)
     let e_d' =
-      WideningTokens.with_side_tokens (WideningTokens.TS.of_list uuids) (fun () ->
+      WideningTokenLifter.with_side_tokens (WideningTokenLifter.TS.of_list uuids) (fun () ->
           CPA.fold (fun x v acc ->
               let addr: AD.t = AD.of_mval (x, `NoOffset) in
               set ~ctx ~invariant:false acc addr x.vtype v
@@ -3077,7 +3077,7 @@ struct
           Priv.lock ask (priv_getg ctx.global) st m
         ) st addr
     | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
-      WideningTokens.with_local_side_tokens (fun () ->
+      WideningTokenLifter.with_local_side_tokens (fun () ->
           CommonPriv.lift_unlock ask (fun st m ->
               Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st m
             ) st addr
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 6212b6de90..742e796fbd 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -156,20 +156,20 @@ struct
     else
       iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
 
-  let do_sideg ctx (xs:(V.t * (WideningTokens.TS.t * G.t)) list) =
+  let do_sideg ctx (xs:(V.t * (WideningTokenLifter.TS.t * G.t)) list) =
     let side_one v dts =
       let side_one_ts ts d =
         (* Do side effects with the tokens that were active at the time.
            Transfer functions have exited the with_side_token wrappers by now. *)
-        let old_side_tokens = !WideningTokens.side_tokens in
-        WideningTokens.side_tokens := ts;
+        let old_side_tokens = !WideningTokenLifter.side_tokens in
+        WideningTokenLifter.side_tokens := ts;
         Fun.protect (fun () ->
             ctx.sideg v @@ fold_left G.join (G.bot ()) d
           ) ~finally:(fun () ->
-            WideningTokens.side_tokens := old_side_tokens
+            WideningTokenLifter.side_tokens := old_side_tokens
           )
       in
-      iter (uncurry side_one_ts) @@ group_assoc_eq WideningTokens.TS.equal dts
+      iter (uncurry side_one_ts) @@ group_assoc_eq WideningTokenLifter.TS.equal dts
     in
     iter (uncurry side_one) @@ group_assoc_eq V.equal xs
 
@@ -355,7 +355,7 @@ struct
       | None -> (fun ?(multiple=false) v d    -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context."))
     in
     let sideg = match sides with
-      | Some sides -> (fun v g    -> sides  := (v, (!WideningTokens.side_tokens, g)) :: !sides)
+      | Some sides -> (fun v g    -> sides  := (v, (!WideningTokenLifter.side_tokens, g)) :: !sides)
       | None -> (fun v g       -> failwith ("Cannot \"sideg\" in " ^ tfname ^ " context."))
     in
     let emit = match emits with
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 6b5b495233..615dbd3266 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -29,7 +29,7 @@ struct
 
   type inv = {
     exp: Cil.exp;
-    token: WideningTokens.Token.t;
+    token: WideningToken.t;
   }
 
   let invs: inv NH.t = NH.create 100
@@ -264,7 +264,7 @@ struct
         if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (ctx.ask (EvalInt e)) = Some false) then (
           let tokens = x.token :: List.map (fun {token; _} -> token) xs in
           ctx.emit (Unassume {exp = e; tokens});
-          List.iter WideningTokens.add tokens
+          List.iter WideningTokenLifter.add tokens
         )
       );
       ctx.local
diff --git a/src/domains/events.ml b/src/domains/events.ml
index b3054b8416..cf12900c98 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -14,7 +14,7 @@ type t =
   | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *) (* TODO: unused *)
   | UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *)
   | Assert of exp
-  | Unassume of {exp: CilType.Exp.t; tokens: WideningTokens0.Token.t list}
+  | Unassume of {exp: CilType.Exp.t; tokens: WideningToken.t list}
   | Longjmped of {lval: CilType.Lval.t option}
 
 (** Should event be emitted after transfer function raises [Deadcode]? *)
@@ -45,5 +45,5 @@ let pretty () = function
   | Assign {lval; exp} -> dprintf "Assign {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp
   | UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp
   | Assert exp -> dprintf "Assert %a" d_exp exp
-  | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningTokens0.Token.pretty) tokens
+  | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningToken.pretty) tokens
   | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 1d0ebb869b..2566939817 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -39,7 +39,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
       |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
       (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
          Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
-      |> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter)
+      |> lift (get_bool "ana.widen.tokens") (module WideningTokenLifter.Lifter)
       |> lift true (module LongjmpLifter.Lifter)
       |> lift termination_enabled (module RecursionTermLifter.Lifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*)
     )
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 91f9837419..d8fd408151 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -180,7 +180,8 @@ module SpecLifters = SpecLifters
 module LongjmpLifter = LongjmpLifter
 module RecursionTermLifter = RecursionTermLifter
 module ContextGasLifter = ContextGasLifter
-module WideningTokens = WideningTokens
+module WideningToken = WideningToken
+module WideningTokenLifter = WideningTokenLifter
 
 module WitnessConstraints = WitnessConstraints
 
diff --git a/src/lifters/wideningToken.ml b/src/lifters/wideningToken.ml
new file mode 100644
index 0000000000..d780c4e793
--- /dev/null
+++ b/src/lifters/wideningToken.ml
@@ -0,0 +1,4 @@
+(** Widening token for {!WideningTokenLifter}. *)
+
+(* Change to variant type if need other tokens than witness UUIDs. *)
+include Printable.Prod (Basetype.RawStrings) (Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end))
diff --git a/src/lifters/wideningTokens.ml b/src/lifters/wideningTokenLifter.ml
similarity index 99%
rename from src/lifters/wideningTokens.ml
rename to src/lifters/wideningTokenLifter.ml
index 4d60099d7e..634468a9ca 100644
--- a/src/lifters/wideningTokens.ml
+++ b/src/lifters/wideningTokenLifter.ml
@@ -6,7 +6,7 @@
 
     @see <http://www2.in.tum.de/bib/files/mihaila13widening.pdf> Mihaila, B., Sepp, A. & Simon, A. Widening as Abstract Domain. *)
 
-include WideningTokens0
+module Token = WideningToken
 
 (** Widening token set. *)
 module TS = SetDomain.ToppedSet (Token) (struct let topname = "Top" end)
diff --git a/src/lifters/wideningTokens0.ml b/src/lifters/wideningTokens0.ml
deleted file mode 100644
index dcbf77424e..0000000000
--- a/src/lifters/wideningTokens0.ml
+++ /dev/null
@@ -1,6 +0,0 @@
-(** Widening token. *)
-module Token =
-struct
-  (* Change to variant type if need other tokens than witness UUIDs. *)
-  include Printable.Prod (Basetype.RawStrings) (Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end))
-end

From a2817445e67768d30ef86b2ece90b5f00d3ffee5 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 9 Oct 2024 10:38:14 +0300
Subject: [PATCH 10/25] Improve widening token output

---
 src/lifters/wideningToken.ml | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/lifters/wideningToken.ml b/src/lifters/wideningToken.ml
index d780c4e793..0639521038 100644
--- a/src/lifters/wideningToken.ml
+++ b/src/lifters/wideningToken.ml
@@ -1,4 +1,16 @@
 (** Widening token for {!WideningTokenLifter}. *)
 
+module Uuid =
+struct
+  include Basetype.RawStrings
+  let name () = "uuid"
+end
+
+module Index =
+struct
+  include Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end)
+  let name () = "index"
+end
+
 (* Change to variant type if need other tokens than witness UUIDs. *)
-include Printable.Prod (Basetype.RawStrings) (Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end))
+include Printable.Prod (Uuid) (Index)

From 2f5b50fa9081abda073a33b393ef33c282c1ebc4 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 16 Oct 2024 16:51:40 +0300
Subject: [PATCH 11/25] Revert "Add hacky imaxabs sqrt refine support"

This reverts commit f9765da81d64a99f77c385835c6c0a5c3db419da.
---
 src/analyses/baseInvariant.ml                          | 3 +--
 tests/regression/39-signed-overflows/12-imaxabs-sqrt.c | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index d5b65a95f4..51a27e19f8 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -785,8 +785,7 @@ struct
            | TFloat (fk, _), FLongDouble
            | TFloat (FDouble as fk, _), FDouble
            | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
-           | TInt (ik, _), _ -> inv_exp (Int (FD.to_int ik c)) e st (* TODO: is this cast refinement correct? *)
-           | t, fk -> fallback (fun () -> Pretty.dprintf "CastE: incompatible types %a and %a" CilType.Typ.pretty t CilType.Fkind.pretty fk) st)
+           | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st)
         | CastE ((TInt (ik, _)) as t, e), Int c
         | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
           (match eval e st with
diff --git a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c
index 46512aed21..b121645b27 100644
--- a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c
+++ b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c
@@ -6,7 +6,7 @@ int main() {
     int64_t data;
     if (data > (-0x7fffffffffffffff - 1) && imaxabs((intmax_t)data) <= sqrtl(0x7fffffffffffffffLL))
     {
-        int64_t result = data * data; // NOWARN
+        int64_t result = data * data; // TODO NOWARN
     }
     return 8;
 }

From f7a5afa966d6dc4b62748fdb1738f2b2aef2f844 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 16 Oct 2024 17:39:07 +0300
Subject: [PATCH 12/25] Add 39-signed-overflows/13-imaxabs-macos test

---
 .../39-signed-overflows/13-imaxabs-macos.c    | 25 +++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 tests/regression/39-signed-overflows/13-imaxabs-macos.c

diff --git a/tests/regression/39-signed-overflows/13-imaxabs-macos.c b/tests/regression/39-signed-overflows/13-imaxabs-macos.c
new file mode 100644
index 0000000000..745d5b74c4
--- /dev/null
+++ b/tests/regression/39-signed-overflows/13-imaxabs-macos.c
@@ -0,0 +1,25 @@
+//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial
+// 39-signed-overflows/11-imaxabs, but with long long as int64_t instead (https://github.com/goblint/analyzer/pull/1519#issuecomment-2417032186).
+#include<stdlib.h>
+#include <stdint.h>
+#include <inttypes.h>
+int main() {
+    long long data;
+    if (data > (-0x7fffffffffffffff - 1))
+    {
+        if (imaxabs(data) < 100)
+        {
+            __goblint_check(data < 100);
+            __goblint_check(-100 < data);
+            long long result = data * data; // NOWARN
+        }
+
+        if(imaxabs(data) <= 100)
+        {
+            __goblint_check(data <= 100);
+            __goblint_check(-100 <= data);
+            long long result = data * data; // NOWARN
+        }
+    }
+    return 8;
+}

From 62834684764e5e1bc88705f19c54fa22a0d35d64 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 16 Oct 2024 17:55:20 +0300
Subject: [PATCH 13/25] Unroll cast type in BaseInvariant

---
 src/analyses/baseInvariant.ml | 58 +++++++++++++++++++----------------
 1 file changed, 31 insertions(+), 27 deletions(-)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 51a27e19f8..52f0888d3f 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -777,33 +777,37 @@ struct
             | _ -> assert false
           end
         | Const _ , _ -> st (* nothing to do *)
-        | CastE ((TFloat (_, _)), e), Float c ->
-          (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with
-           | TFloat (FLongDouble as fk, _), FFloat
-           | TFloat (FDouble as fk, _), FFloat
-           | TFloat (FLongDouble as fk, _), FDouble
-           | TFloat (fk, _), FLongDouble
-           | TFloat (FDouble as fk, _), FDouble
-           | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
-           | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st)
-        | CastE ((TInt (ik, _)) as t, e), Int c
-        | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
-          (match eval e st with
-           | Int i ->
-             (match unrollType (Cilfacade.typeOf e) with
-              | (TInt(ik_e, _) as t')
-              | (TEnum ({ekind = ik_e; _ }, _) as t') ->
-                if VD.is_dynamically_safe_cast t t' (Int i) then
-                  (* let c' = ID.cast_to ik_e c in *)
-                  (* Suppressing overflow warnings as this is not a computation that comes from the program *)
-                  let res_range = (ID.cast_to ~suppress_ovwarn:true ik (ID.top_of ik_e)) in
-                  let c' = ID.cast_to ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *)
-                  if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
-                  inv_exp (Int c') e st
-                else
-                  fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
-              | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st)
-           | v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
+        | CastE (t, e), c_typed ->
+          begin match Cil.unrollType t, c_typed with
+            | TFloat (_, _), Float c ->
+              (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with
+               | TFloat (FLongDouble as fk, _), FFloat
+               | TFloat (FDouble as fk, _), FFloat
+               | TFloat (FLongDouble as fk, _), FDouble
+               | TFloat (fk, _), FLongDouble
+               | TFloat (FDouble as fk, _), FDouble
+               | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
+               | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st)
+            | (TInt (ik, _) as t), Int c
+            | (TEnum ({ekind = ik; _ }, _) as t), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
+              (match eval e st with
+               | Int i ->
+                 (match unrollType (Cilfacade.typeOf e) with
+                  | (TInt(ik_e, _) as t')
+                  | (TEnum ({ekind = ik_e; _ }, _) as t') ->
+                    if VD.is_dynamically_safe_cast t t' (Int i) then
+                      (* let c' = ID.cast_to ik_e c in *)
+                      (* Suppressing overflow warnings as this is not a computation that comes from the program *)
+                      let res_range = (ID.cast_to ~suppress_ovwarn:true ik (ID.top_of ik_e)) in
+                      let c' = ID.cast_to ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *)
+                      if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
+                      inv_exp (Int c') e st
+                    else
+                      fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
+                  | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st)
+               | v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
+            | _, _ -> fallback (fun () -> Pretty.dprintf "CastE: %a not implemented" d_plainexp (CastE (t, e))) st
+          end
         | e, _ -> fallback (fun () -> Pretty.dprintf "%a not implemented" d_plainexp e) st
     in
     if eval_bool exp st = Some (not tv) then contra st (* we already know that the branch is dead *)

From e12d6df901069f353c7a2a9ff08dfd6130a6507b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 17 Oct 2024 15:26:28 +0300
Subject: [PATCH 14/25] Copy svcomp confs to svcomp25

---
 conf/svcomp25-validate.json | 122 ++++++++++++++++++++++++++++++++++++
 conf/svcomp25.json          | 117 ++++++++++++++++++++++++++++++++++
 2 files changed, 239 insertions(+)
 create mode 100644 conf/svcomp25-validate.json
 create mode 100644 conf/svcomp25.json

diff --git a/conf/svcomp25-validate.json b/conf/svcomp25-validate.json
new file mode 100644
index 0000000000..f0e99057d1
--- /dev/null
+++ b/conf/svcomp25-validate.json
@@ -0,0 +1,122 @@
+{
+  "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",
+      "unassume"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    },
+    "widen": {
+      "tokens": true
+    }
+  },
+  "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": false,
+      "strict": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "location_invariant",
+        "loop_invariant",
+        "invariant_set",
+        "violation_sequence"
+      ],
+      "invariant-types": [
+        "location_invariant",
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": true,
+      "other": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/svcomp25.json b/conf/svcomp25.json
new file mode 100644
index 0000000000..aa3f625da9
--- /dev/null
+++ b/conf/svcomp25.json
@@ -0,0 +1,117 @@
+{
+  "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"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "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
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}

From 6a973802a229367f7112637c0b37d5e979560a8d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 17 Oct 2024 15:28:42 +0300
Subject: [PATCH 15/25] Update sv-comp/archive.sh for 2025

---
 scripts/sv-comp/archive.sh | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/scripts/sv-comp/archive.sh b/scripts/sv-comp/archive.sh
index 37fa2758d9..aefac8f769 100755
--- a/scripts/sv-comp/archive.sh
+++ b/scripts/sv-comp/archive.sh
@@ -4,7 +4,7 @@
 
 make clean
 
-git tag -m "SV-COMP 2024" svcomp24
+git tag -m "SV-COMP 2025" svcomp25
 
 dune build --profile=release src/goblint.exe
 rm -f goblint
@@ -32,8 +32,8 @@ zip goblint/scripts/sv-comp/goblint.zip \
     goblint/lib/libboxD.so \
     goblint/lib/libpolkaMPQ.so \
     goblint/lib/LICENSE.APRON \
-    goblint/conf/svcomp24.json \
-    goblint/conf/svcomp24-validate.json \
+    goblint/conf/svcomp25.json \
+    goblint/conf/svcomp25-validate.json \
     goblint/lib/libc/stub/include/assert.h \
     goblint/lib/goblint/runtime/include/goblint.h \
     goblint/lib/libc/stub/src/stdlib.c \

From d3c5d353cec4b9b875c5a3f12bc09647f4c03bcf Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 18 Oct 2024 12:20:55 +0300
Subject: [PATCH 16/25] Document SV-COMP bench-defs MR

---
 docs/developer-guide/releasing.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/docs/developer-guide/releasing.md b/docs/developer-guide/releasing.md
index 7530d9ad20..aca0749eb9 100644
--- a/docs/developer-guide/releasing.md
+++ b/docs/developer-guide/releasing.md
@@ -77,6 +77,8 @@
 
     This includes: git tag name, git tag message and zipped conf file.
 
+5. Open MR with conf file name to the [bench-defs](https://gitlab.com/sosy-lab/sv-comp/bench-defs) repository.
+
 ### For each prerun
 
 1. Update opam pins:

From b1095fbd71b7360e1a6d7a7d8b9bcc3b790b3bef Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 6 Nov 2024 11:32:06 +0200
Subject: [PATCH 17/25] Add more precise YAML witness generation summary

---
 src/witness/yamlWitness.ml                    | 13 ++++++++++++
 .../03-practical/35-base-mutex-macos.t        |  3 +++
 tests/regression/13-privatized/01-priv_nr.t   |  9 ++++++++
 .../regression/36-apron/12-traces-min-rpb1.t  |  3 +++
 tests/regression/36-apron/52-queuesize.t      |  6 ++++++
 .../11-unrolled-loop-invariant.t              |  3 +++
 tests/regression/56-witness/05-prec-problem.t |  3 +++
 .../56-witness/08-witness-all-locals.t        |  6 ++++++
 .../56-witness/46-top-bool-invariant.t        | 21 +++++++++++++++++++
 .../56-witness/47-top-int-invariant.t         | 21 +++++++++++++++++++
 tests/regression/cfg/foo.t/run.t              |  3 +++
 tests/regression/cfg/issue-1356.t/run.t       |  3 +++
 tests/regression/cfg/loops.t/run.t            |  3 +++
 tests/regression/cfg/pr-758.t/run.t           |  3 +++
 tests/regression/witness/int.t/run.t          |  3 +++
 tests/regression/witness/typedef.t/run.t      |  6 ++++++
 16 files changed, 109 insertions(+)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 2bdd2ced4c..bc31797688 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -249,6 +249,11 @@ struct
 
     let entries = [] in
 
+    let cnt_loop_invariant = ref 0 in
+    let cnt_location_invariant = ref 0 in
+    let cnt_flow_insensitive_invariant = ref 0 in
+    (* TODO: precondition invariants? *)
+
     (* Generate location invariants (without precondition) *)
     let entries =
       if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then (
@@ -268,6 +273,7 @@ struct
               List.fold_left (fun acc inv ->
                   let invariant = Entry.invariant (CilType.Exp.show inv) in
                   let entry = Entry.location_invariant ~task ~location ~invariant in
+                  incr cnt_location_invariant;
                   entry :: acc
                 ) acc invs
             | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
@@ -297,6 +303,7 @@ struct
                 List.fold_left (fun acc inv ->
                     let invariant = Entry.invariant (CilType.Exp.show inv) in
                     let entry = Entry.loop_invariant ~task ~location ~invariant in
+                    incr cnt_loop_invariant;
                     entry :: acc
                   ) acc invs
               | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
@@ -322,6 +329,7 @@ struct
                   List.fold_left (fun acc inv ->
                       let invariant = Entry.invariant (CilType.Exp.show inv) in
                       let entry = Entry.flow_insensitive_invariant ~task ~invariant in
+                      incr cnt_flow_insensitive_invariant;
                       entry :: acc
                     ) acc invs
                 | `Bot | `Top -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *)
@@ -459,6 +467,7 @@ struct
                   List.fold_left (fun acc inv ->
                       let invariant = CilType.Exp.show inv in
                       let invariant = Entry.location_invariant' ~location ~invariant in
+                      incr cnt_location_invariant;
                       invariant :: acc
                     ) acc invs
                 | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
@@ -488,6 +497,7 @@ struct
                     List.fold_left (fun acc inv ->
                         let invariant = CilType.Exp.show inv in
                         let invariant = Entry.loop_invariant' ~location ~invariant in
+                        incr cnt_loop_invariant;
                         invariant :: acc
                       ) acc invs
                   | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
@@ -512,6 +522,9 @@ struct
     let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in (* reverse to make entries in file in the same order as generation messages *)
 
     M.msg_group Info ~category:Witness "witness generation summary" [
+      (Pretty.dprintf "location invariants: %d" !cnt_location_invariant, None);
+      (Pretty.dprintf "loop invariants: %d" !cnt_loop_invariant, None);
+      (Pretty.dprintf "flow-insensitive invariants: %d" !cnt_flow_insensitive_invariant, None);
       (Pretty.dprintf "total generation entries: %d" (List.length yaml_entries), None);
     ];
 
diff --git a/tests/regression/03-practical/35-base-mutex-macos.t b/tests/regression/03-practical/35-base-mutex-macos.t
index 9e5f36d337..1d8a184d4c 100644
--- a/tests/regression/03-practical/35-base-mutex-macos.t
+++ b/tests/regression/03-practical/35-base-mutex-macos.t
@@ -4,6 +4,9 @@
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 1
 
 There should be no invariants about __sig.
diff --git a/tests/regression/13-privatized/01-priv_nr.t b/tests/regression/13-privatized/01-priv_nr.t
index bbc285098a..0186709027 100644
--- a/tests/regression/13-privatized/01-priv_nr.t
+++ b/tests/regression/13-privatized/01-priv_nr.t
@@ -10,6 +10,9 @@
     dead: 0
     total lines: 19
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
   [Info][Race] Memory locations race summary:
     safe: 1
@@ -64,6 +67,9 @@
     dead: 0
     total lines: 19
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
   [Info][Race] Memory locations race summary:
     safe: 1
@@ -118,6 +124,9 @@
     dead: 0
     total lines: 19
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
   [Info][Race] Memory locations race summary:
     safe: 1
diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t
index 5060f505d9..d0cebd6d1c 100644
--- a/tests/regression/36-apron/12-traces-min-rpb1.t
+++ b/tests/regression/36-apron/12-traces-min-rpb1.t
@@ -13,6 +13,9 @@
     write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:14:3-14:8)
     read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:27:3-27:26)
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
   [Info][Race] Memory locations race summary:
     safe: 0
diff --git a/tests/regression/36-apron/52-queuesize.t b/tests/regression/36-apron/52-queuesize.t
index 62851f2ec9..f0a977891a 100644
--- a/tests/regression/36-apron/52-queuesize.t
+++ b/tests/regression/36-apron/52-queuesize.t
@@ -37,6 +37,9 @@ Without diff-box:
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:56:10-56:11)
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:78:12-78:13)
   [Info][Witness] witness generation summary:
+    location invariants: 8
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 8
   [Info][Race] Memory locations race summary:
     safe: 3
@@ -173,6 +176,9 @@ With diff-box:
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:56:10-56:11)
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:78:12-78:13)
   [Info][Witness] witness generation summary:
+    location invariants: 6
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 6
   [Info][Race] Memory locations race summary:
     safe: 3
diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t
index 3a3b7c43cf..860ffae3bd 100644
--- a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t
+++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t
@@ -211,6 +211,9 @@
   [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:9:12-9:19)
   [Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:10-8:16)
   [Info][Witness] witness generation summary:
+    location invariants: 11
+    loop invariants: 5
+    flow-insensitive invariants: 0
     total generation entries: 16
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t
index 733f16269e..51f92ca203 100644
--- a/tests/regression/56-witness/05-prec-problem.t
+++ b/tests/regression/56-witness/05-prec-problem.t
@@ -6,6 +6,9 @@
     total lines: 13
   [Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (05-prec-problem.c:13:12-13:13)
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 6
 
 TODO: Don't generate duplicate entries from each context: should have generated just 3.
diff --git a/tests/regression/56-witness/08-witness-all-locals.t b/tests/regression/56-witness/08-witness-all-locals.t
index fc4462201d..fe6aefefbd 100644
--- a/tests/regression/56-witness/08-witness-all-locals.t
+++ b/tests/regression/56-witness/08-witness-all-locals.t
@@ -4,6 +4,9 @@
     dead: 0
     total lines: 4
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
 
   $ yamlWitnessStrip < witness.yml
@@ -50,6 +53,9 @@ Fewer entries are emitted if locals from nested block scopes are excluded:
     dead: 0
     total lines: 4
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/56-witness/46-top-bool-invariant.t b/tests/regression/56-witness/46-top-bool-invariant.t
index 741b00966f..be41ef58f2 100644
--- a/tests/regression/56-witness/46-top-bool-invariant.t
+++ b/tests/regression/56-witness/46-top-bool-invariant.t
@@ -6,6 +6,9 @@ def_exc only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -40,6 +43,9 @@ interval only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -74,6 +80,9 @@ enums only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 1
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 1
 
   $ yamlWitnessStrip < witness.yml
@@ -97,6 +106,9 @@ congruence only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 0
 
   $ yamlWitnessStrip < witness.yml
@@ -110,6 +122,9 @@ interval_set only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -144,6 +159,9 @@ all:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 1
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 1
 
   $ yamlWitnessStrip < witness.yml
@@ -167,6 +185,9 @@ all without inexact-type-bounds:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 0
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/56-witness/47-top-int-invariant.t b/tests/regression/56-witness/47-top-int-invariant.t
index cdfe65673f..35d5978c00 100644
--- a/tests/regression/56-witness/47-top-int-invariant.t
+++ b/tests/regression/56-witness/47-top-int-invariant.t
@@ -6,6 +6,9 @@ def_exc only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -40,6 +43,9 @@ interval only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -74,6 +80,9 @@ enums only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -108,6 +117,9 @@ congruence only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 0
 
   $ yamlWitnessStrip < witness.yml
@@ -121,6 +133,9 @@ interval_set only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -155,6 +170,9 @@ all:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -189,6 +207,9 @@ all without inexact-type-bounds:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 0
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t
index cd890b7a19..19873d7540 100644
--- a/tests/regression/cfg/foo.t/run.t
+++ b/tests/regression/cfg/foo.t/run.t
@@ -67,6 +67,9 @@
     total lines: 6
   [Warning][Deadcode][CWE-571] condition 'a > 0' (possibly inserted by CIL) is always true (foo.c:3:10-3:20)
   [Info][Witness] witness generation summary:
+    location invariants: 8
+    loop invariants: 2
+    flow-insensitive invariants: 0
     total generation entries: 10
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/cfg/issue-1356.t/run.t b/tests/regression/cfg/issue-1356.t/run.t
index aee9456b61..d1fcb3c7ef 100644
--- a/tests/regression/cfg/issue-1356.t/run.t
+++ b/tests/regression/cfg/issue-1356.t/run.t
@@ -99,6 +99,9 @@
     dead: 0
     total lines: 13
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 0
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/cfg/loops.t/run.t b/tests/regression/cfg/loops.t/run.t
index 6596e7b4a4..1fd19b41fe 100644
--- a/tests/regression/cfg/loops.t/run.t
+++ b/tests/regression/cfg/loops.t/run.t
@@ -219,6 +219,9 @@
     dead: 0
     total lines: 20
   [Info][Witness] witness generation summary:
+    location invariants: 32
+    loop invariants: 21
+    flow-insensitive invariants: 0
     total generation entries: 53
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/cfg/pr-758.t/run.t b/tests/regression/cfg/pr-758.t/run.t
index 58bbb88ce4..082c63e860 100644
--- a/tests/regression/cfg/pr-758.t/run.t
+++ b/tests/regression/cfg/pr-758.t/run.t
@@ -93,6 +93,9 @@
     dead: 0
     total lines: 6
   [Info][Witness] witness generation summary:
+    location invariants: 10
+    loop invariants: 2
+    flow-insensitive invariants: 0
     total generation entries: 12
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/witness/int.t/run.t b/tests/regression/witness/int.t/run.t
index 6b4784ce32..9448ac7855 100644
--- a/tests/regression/witness/int.t/run.t
+++ b/tests/regression/witness/int.t/run.t
@@ -7,6 +7,9 @@
     dead: 0
     total lines: 10
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t
index 55dcc1f911..f9fac0c743 100644
--- a/tests/regression/witness/typedef.t/run.t
+++ b/tests/regression/witness/typedef.t/run.t
@@ -4,6 +4,9 @@
     dead: 0
     total lines: 6
   [Info][Witness] witness generation summary:
+    location invariants: 13
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 13
 
   $ yamlWitnessStrip < witness.yml
@@ -157,6 +160,9 @@
     dead: 0
     total lines: 6
   [Info][Witness] witness generation summary:
+    location invariants: 14
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 14
 
   $ yamlWitnessStrip < witness.yml

From 77190828a810819b5b607c59d1553fc713b1be9d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 6 Nov 2024 11:45:13 +0200
Subject: [PATCH 18/25] Add witness.yaml.strict option description

---
 src/config/options.schema.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 447290b44d..9c1f9e1e76 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -2659,7 +2659,7 @@
             },
             "strict": {
               "title": "witness.yaml.strict",
-              "description": "",
+              "description": "Fail YAML witness validation if there's an error/unsupported/disabled entry.",
               "type": "boolean",
               "default": false
             },

From 546a8d04ede0d6646e1d5b20095c0ae5e2f0a78b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 6 Nov 2024 11:49:17 +0200
Subject: [PATCH 19/25] Update YAML witness validation result for refutation
 under new scoring schema

---
 src/witness/yamlWitness.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index bc31797688..1a8c536da5 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -892,7 +892,9 @@ struct
     | true when !cnt_disabled > 0 ->
       Error "witness disabled"
     | _ when !cnt_refuted > 0 ->
-      Ok (Svcomp.Result.False None)
+      (* Refuted only when assuming the invariant is reachable. *)
+      (* Ok (Svcomp.Result.False None) *) (* Wasn't a problem because valid*->correctness->false gave 0 points under old validator track scoring schema: https://doi.org/10.1007/978-3-031-22308-2_8. *)
+      Ok Svcomp.Result.Unknown (* Now valid*->correctness->false gives 1p (negative) points under new validator track scoring schema: https://doi.org/10.1007/978-3-031-57256-2_15. *)
     | _ when !cnt_unconfirmed > 0 ->
       Ok Unknown
     | _ ->

From 2048122f114dd24acaa0ff8b4fbd431d92c291f8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 6 Nov 2024 11:57:42 +0200
Subject: [PATCH 20/25] Fix YAML witness validate/unassume error with empty
 (unparsable) path

Raised an obscure Invalid_argument exception instead.
---
 src/analyses/unassumeAnalysis.ml | 2 +-
 src/witness/yamlWitness.ml       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 615dbd3266..707e0f4820 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -71,7 +71,7 @@ struct
         | _ -> ()
       );
 
-    let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with
+    let yaml = match GobResult.Syntax.(Fpath.of_string (GobConfig.get_string "witness.yaml.unassume") >>= Yaml_unix.of_file) with
       | Ok yaml -> yaml
       | Error (`Msg m) ->
         Logs.error "Yaml_unix.of_file: %s" m;
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 1a8c536da5..06e355068e 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -608,7 +608,7 @@ struct
 
     let inv_parser = InvariantParser.create FileCfg.file in
 
-    let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.validate")) with
+    let yaml = match GobResult.Syntax.(Fpath.of_string (GobConfig.get_string "witness.yaml.validate") >>= Yaml_unix.of_file) with
       | Ok yaml -> yaml
       | Error (`Msg m) ->
         Logs.error "Yaml_unix.of_file: %s" m;

From 8d8b6752af3d23260a9c5ab080eb26bdf740006d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 14 Nov 2024 17:40:49 +0200
Subject: [PATCH 21/25] Remove outdated comments about new __VERIFIER_nondet
 functions

---
 lib/sv-comp/stub/src/sv-comp.c | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/lib/sv-comp/stub/src/sv-comp.c b/lib/sv-comp/stub/src/sv-comp.c
index 12c04125d6..469a641e73 100644
--- a/lib/sv-comp/stub/src/sv-comp.c
+++ b/lib/sv-comp/stub/src/sv-comp.c
@@ -35,10 +35,10 @@ __VERIFIER_nondet2(unsigned int, u32)
 __VERIFIER_nondet2(unsigned short int, u16) // not in rules
 __VERIFIER_nondet2(unsigned char, u8) // not in rules
 __VERIFIER_nondet2(unsigned char, unsigned_char) // not in rules
-__VERIFIER_nondet2(long long, longlong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
-__VERIFIER_nondet2(unsigned long long, ulonglong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
-__VERIFIER_nondet2(__uint128_t, uint128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
-__VERIFIER_nondet2(__int128_t, int128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
+__VERIFIER_nondet2(long long, longlong)
+__VERIFIER_nondet2(unsigned long long, ulonglong)
+__VERIFIER_nondet2(__uint128_t, uint128)
+__VERIFIER_nondet2(__int128_t, int128)
 __VERIFIER_nondet2(unsigned char, uchar)
 __VERIFIER_nondet2(unsigned int, uint)
 __VERIFIER_nondet2(unsigned long, ulong)

From 6a05022657c9da91e90cea46c0c420650a77fb16 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 18 Nov 2024 13:37:44 +0200
Subject: [PATCH 22/25] Add initial CHANGELOG for SV-COMP 2025

---
 CHANGELOG.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 420cc7145e..6e9fe29306 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,17 @@
+## v2.5.0 (unreleased)
+Functionally equivalent to Goblint in SV-COMP 2025.
+
+### SV-COMP 2025
+* Improve invariants (#1361, #1362, #1375, #1328, #1493, #1356).
+* Simplify invariants (#1436, #1517).
+* Improve YAML witness locations (#1355, #1372, #1400, #1403).
+* Improve autotuner (#1469, #1450, #1612, #1604, #1181).
+* Loop unrolling (#1582, #1583, #1584, #1516, #1590, #1595, #1599).
+* Add abortUnless to svcomp (#1464).
+* Fix spurious overflow warnings (#1511).
+* Add primitive YAML violation witness rejection (#1301, #1512).
+* Machdep support (#54, #1574).
+
 ## v2.4.0
 * Remove unmaintained analyses: spec, file (#1281).
 * Add linear two-variable equalities analysis (#1297, #1412, #1466).

From 152ebb633d32275d8cb9924fd54541c2ac64917b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 18 Nov 2024 13:51:22 +0200
Subject: [PATCH 23/25] Add initial CHANGELOG for v2.5.0

---
 CHANGELOG.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6e9fe29306..aec84573cf 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,10 @@
 ## v2.5.0 (unreleased)
 Functionally equivalent to Goblint in SV-COMP 2025.
 
+* Cleanup (#1095, #1523, #1554, #1575, #1588, #1597, #1614).
+* Reduce hash collisions (#1594, #1602).
+* Context gas per function (#1569, #1570, #1598).
+
 ### SV-COMP 2025
 * Improve invariants (#1361, #1362, #1375, #1328, #1493, #1356).
 * Simplify invariants (#1436, #1517).

From 64981452f455f42cef61de0ab044f3131497db6d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 18 Nov 2024 14:08:10 +0200
Subject: [PATCH 24/25] Add CHANGELOG for v2.5.0

---
 CHANGELOG.md | 23 ++++++++---------------
 1 file changed, 8 insertions(+), 15 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index aec84573cf..cf6a8aa781 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,20 +1,13 @@
 ## v2.5.0 (unreleased)
 Functionally equivalent to Goblint in SV-COMP 2025.
 
-* Cleanup (#1095, #1523, #1554, #1575, #1588, #1597, #1614).
-* Reduce hash collisions (#1594, #1602).
-* Context gas per function (#1569, #1570, #1598).
-
-### SV-COMP 2025
-* Improve invariants (#1361, #1362, #1375, #1328, #1493, #1356).
-* Simplify invariants (#1436, #1517).
-* Improve YAML witness locations (#1355, #1372, #1400, #1403).
-* Improve autotuner (#1469, #1450, #1612, #1604, #1181).
-* Loop unrolling (#1582, #1583, #1584, #1516, #1590, #1595, #1599).
-* Add abortUnless to svcomp (#1464).
-* Fix spurious overflow warnings (#1511).
-* Add primitive YAML violation witness rejection (#1301, #1512).
-* Machdep support (#54, #1574).
+* Add 32bit vs 64bit architecture support (#54, #1574).
+* Add per-function context gas analysis (#1569, #1570, #1598).
+* Adapt automatic static loop unrolling (#1516, #1582, #1583, #1584, #1590, #1595, #1599).
+* Adapt automatic configuration tuning (#1450, #1612, #1181, #1604).
+* Simplify non-relational integer invariants in witnesses (#1517).
+* Fix excessive hash collisions (#1594, #1602).
+* Clean up various code (#1095, #1523, #1554, #1575, #1588, #1597, #1614).
 
 ## v2.4.0
 * Remove unmaintained analyses: spec, file (#1281).
@@ -28,7 +21,7 @@ Functionally equivalent to Goblint in SV-COMP 2025.
 * Fix mutex type analysis unsoundness and enable it by default (#1414, #1416, #1510).
 * Add points-to set refinement on mutex path splitting (#1287, #1343, #1374, #1396, #1407).
 * Improve narrowing operators (#1502, #1540, #1543).
-* Extract automatic configuration tuning for soundness (#1369).
+* Extract automatic configuration tuning for soundness (#1469).
 * Fix many locations in witnesses (#1355, #1372, #1400, #1403).
 * Improve output readability (#1294, #1312, #1405, #1497).
 * Refactor logging (#1117).

From 0ca1bb30f50d12bec84198ae404994c510e37431 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 22 Nov 2024 11:11:34 +0200
Subject: [PATCH 25/25] Add parsing of integer constraints in YAML
 violation_sequence-s

---
 src/util/std/gobYaml.ml        |  2 ++
 src/witness/yamlWitnessType.ml | 26 +++++++++++++++++++++++---
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/util/std/gobYaml.ml b/src/util/std/gobYaml.ml
index 624cdbf1fa..4c8576ade2 100644
--- a/src/util/std/gobYaml.ml
+++ b/src/util/std/gobYaml.ml
@@ -44,3 +44,5 @@ let list = function
 let entries = function
   | `O assoc -> Ok assoc
   | _ -> Error (`Msg "Failed to get entries from non-object value")
+
+let int i = float (float_of_int i)
diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml
index 4fc2029801..c77fadad4c 100644
--- a/src/witness/yamlWitnessType.ml
+++ b/src/witness/yamlWitnessType.ml
@@ -447,15 +447,35 @@ struct
 
   module Constraint =
   struct
+
+    module Value =
+    struct
+      type t =
+        | String of string
+        | Int of int (* Why doesn't format consider ints (for switch branches) as strings here, like everywhere else? *)
+      [@@deriving ord]
+
+      let to_yaml = function
+        | String s -> GobYaml.string s
+        | Int i -> GobYaml.int i
+
+      let of_yaml y =
+        let open GobYaml in
+        match y with
+        | `String s -> Ok (String s)
+        | `Float f -> Ok (Int (int_of_float f))
+        | _ -> Error (`Msg "Expected a string or integer value")
+    end
+
     type t = {
-      value: string;
+      value: Value.t;
       format: string option;
     }
     [@@deriving ord]
 
     let to_yaml {value; format} =
       `O ([
-          ("value", `String value);
+          ("value", Value.to_yaml value);
         ] @ (match format with
           | Some format -> [
               ("format", `String format);
@@ -466,7 +486,7 @@ struct
 
     let of_yaml y =
       let open GobYaml in
-      let+ value = y |> find "value" >>= to_string
+      let+ value = y |> find "value" >>= Value.of_yaml
       and+ format = y |> Yaml.Util.find "format" >>= option_map to_string in
       {value; format}
   end