From b148e207ed7df3b65727ec504db3cf1e90442258 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 20 Sep 2024 17:11:37 +0200
Subject: [PATCH 01/16] Modularize out details of the current approach

---
 src/framework/constraints.ml | 64 ++++++++++++++++++++++++++----------
 src/framework/control.ml     |  2 +-
 2 files changed, 48 insertions(+), 18 deletions(-)

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 7df4167acd..ef84326be4 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -513,10 +513,41 @@ struct
   let names x = Format.asprintf "%d" x
 end
 
+module type Gas = sig
+  module M:Lattice.S
+  val startgas: unit -> M.t
+  val is_exhausted: fundec -> M.t -> bool
+  val is_any_exhausted: M.t -> bool
+  val callee_gas: fundec -> M.t -> M.t
+  val thread_gas: varinfo -> M.t -> M.t
+end
+
+module GlobalGas:Gas = struct
+  module M = Lattice.Chain (IntConf)
+  let startgas () = get_int "ana.context.gas_value"
+
+  let is_any_exhausted v = v <= 0
+  let is_exhausted _  = is_any_exhausted
+
+  (* callee gas = caller gas - 1 *)
+  let callee_gas f v = max 0 (v - 1)
+  let thread_gas f v =  max 0 (v - 1)
+end
+
+module PerFunctionGas:Gas = struct
+  module M = Lattice.Chain (IntConf)
+  let startgas () = get_int "ana.context.gas_value"
+  let is_exhausted f v = v <= 0
+  let is_any_exhausted v = v <= 0
+  let callee_gas f v = max 0 (v - 1)
+  let thread_gas f v =  max 0 (v - 1)
+end
+
+
 (** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
     For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
-module ContextGasLifter (S:Spec)
-  : Spec with module D = Lattice.Prod (S.D) (Lattice.Chain (IntConf))
+module ContextGasLifter (Gas:Gas) (S:Spec)
+  : Spec with module D = Lattice.Prod (S.D) (Gas.M)
           and module C = Printable.Option (S.C) (NoContext)
           and module G = S.G
 =
@@ -529,7 +560,7 @@ struct
     let printXml f (x,y) =
       BatPrintf.fprintf f "\n%a<analysis name=\"context gas value\">\n%a\n</analysis>" Base1.printXml x Base2.printXml y
   end
-  module D = Context_Gas_Prod (S.D) (Lattice.Chain (IntConf)) (* Product of S.D and an integer, tracking the context gas value *)
+  module D = Context_Gas_Prod (S.D) (Gas.M) (* Product of S.D and an integer, tracking the context gas value *)
   module C = Printable.Option (S.C) (NoContext)
   module G = S.G
   module V = S.V
@@ -549,37 +580,36 @@ struct
 
   let startcontext () = Some (S.startcontext ())
   let name () = S.name ()^" with context gas"
-  let startstate v = S.startstate v, get_int "ana.context.gas_value"
-  let exitstate v = S.exitstate v, get_int "ana.context.gas_value"
+  let startstate v = S.startstate v, Gas.startgas ()
+  let exitstate v = S.exitstate v, Gas.startgas ()
   let morphstate v (d,i) = S.morphstate v d, i
 
   let conv (ctx:(D.t,G.t,C.t,V.t) ctx): (S.D.t,G.t,S.C.t,V.t)ctx =
-    if (cg_val ctx <= 0)
-    then {ctx with local = fst ctx.local
-                 ; split = (fun d es -> ctx.split (d, cg_val ctx) es)
-                 ; context = (fun () -> ctx_failwith "no context (contextGas = 0)")}
-    else {ctx with local = fst ctx.local
-                 ; split = (fun d es -> ctx.split (d, cg_val ctx) es)
-                 ; context = (fun () -> Option.get (ctx.context ()))}
+    {ctx with local = fst ctx.local
+            ; split = (fun d es -> ctx.split (d, cg_val ctx) es)
+            ; context = (fun () -> match ctx.context () with Some c -> c | None -> ctx_failwith "no context (contextGas = 0)")}
 
   let context ctx fd (d,i) =
     (* only keep context if the context gas is greater zero *)
-    if i <= 0 then None else Some (S.context (conv ctx) fd d)
+    if Gas.is_exhausted fd i then
+      None
+    else
+      Some (S.context (conv ctx) fd d)
 
   let enter ctx r f args =
-    (* callee gas = caller gas - 1 *)
-    let liftmap_tup = List.map (fun (x,y) -> (x, cg_val ctx), (y, max 0 (cg_val ctx - 1))) in
+    let liftmap_tup = List.map (fun (x,y) -> (x, cg_val ctx), (y, Gas.callee_gas f (cg_val ctx))) in
     liftmap_tup (S.enter (conv ctx) r f args)
 
   let threadenter ctx ~multiple lval f args =
-    let liftmap f = List.map (fun (x) -> (x, max 0 (cg_val ctx - 1))) f in
+    let liftmap d = List.map (fun (x) -> (x, Gas.thread_gas f (cg_val ctx))) d in
     liftmap (S.threadenter (conv ctx) ~multiple lval f args)
 
   let query ctx (type a) (q: a Queries.t):a Queries.result =
     match q with
     | Queries.GasExhausted ->
+      (* The query is only used in a way where overapproximating gas exhaustion is not harmful *)
       let (d,i) = ctx.local in
-      (i <= 0)
+      Gas.is_any_exhausted i
     | _ -> S.query (conv ctx) q
 
   let sync ctx reason                             = S.sync (conv ctx) reason, cg_val ctx
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 5e92282210..f28feb6a1e 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -23,7 +23,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
   let module S1 =
     (val
       (module MCP.MCP2 : Spec)
-      |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter)
+      |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter(GlobalGas))
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)

From 05520ec9db47b3cc4706bf9eab3ff90c78667b8a Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 20 Sep 2024 17:59:46 +0200
Subject: [PATCH 02/16] Actually rely on lattice structure for gas

---
 src/framework/constraints.ml | 28 ++++++++++++++--------------
 src/framework/control.ml     |  7 ++++++-
 2 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index ef84326be4..b257d529d8 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -507,10 +507,9 @@ struct
 end
 
 module NoContext = struct let name = "no context" end
-module IntConf =
-struct
-  let n () = max_int
-  let names x = Format.asprintf "%d" x
+
+module type GasVal = sig
+  val n: unit -> int
 end
 
 module type Gas = sig
@@ -522,9 +521,9 @@ module type Gas = sig
   val thread_gas: varinfo -> M.t -> M.t
 end
 
-module GlobalGas:Gas = struct
-  module M = Lattice.Chain (IntConf)
-  let startgas () = get_int "ana.context.gas_value"
+module GlobalGas(GasVal:GasVal):Gas = struct
+  module M = Lattice.Chain (struct include GasVal let names x = Format.asprintf "%d" x end)
+  let startgas () = M.top () (*  get_int "ana.context.gas_value" *)
 
   let is_any_exhausted v = v <= 0
   let is_exhausted _  = is_any_exhausted
@@ -534,13 +533,14 @@ module GlobalGas:Gas = struct
   let thread_gas f v =  max 0 (v - 1)
 end
 
-module PerFunctionGas:Gas = struct
-  module M = Lattice.Chain (IntConf)
-  let startgas () = get_int "ana.context.gas_value"
-  let is_exhausted f v = v <= 0
-  let is_any_exhausted v = v <= 0
-  let callee_gas f v = max 0 (v - 1)
-  let thread_gas f v =  max 0 (v - 1)
+module PerFunctionGas(GasVal:GasVal):Gas = struct
+  module V = Lattice.Chain (struct include GasVal let names x = Format.asprintf "%d" x end)
+  module M = MapDomain.MapTop_LiftBot(CilType.Fundec)(V)
+  let startgas () = M.empty ()  (* get_int "ana.context.gas_value" *)
+  let is_exhausted f v = (* v <= 0 *) true
+  let is_any_exhausted v = (* v <= 0 *) true
+  let callee_gas f v = v  (* max 0 (v - 1) *)
+  let thread_gas f v = v (*  max 0 (v - 1) *)
 end
 
 
diff --git a/src/framework/control.ml b/src/framework/control.ml
index f28feb6a1e..68c31768c6 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -20,10 +20,15 @@ let spec_module: (module Spec) Lazy.t = lazy (
   let open Batteries in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
+  let module GasVal = struct
+    (* Chain lattice has elements [0,n-1], but we want [0,gas_value] *)
+    let n () = get_int "ana.context.gas_value" + 1
+  end
+  in
   let module S1 =
     (val
       (module MCP.MCP2 : Spec)
-      |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter(GlobalGas))
+      |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter(GlobalGas(GasVal)))
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)

From dc84b4a533100bac8c1390e61f03a5e35fe931bb Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 20 Sep 2024 18:09:39 +0200
Subject: [PATCH 03/16] Add PerFunctionGas module

---
 src/framework/constraints.ml | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index b257d529d8..5bc83fbe13 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -530,16 +530,18 @@ module GlobalGas(GasVal:GasVal):Gas = struct
 
   (* callee gas = caller gas - 1 *)
   let callee_gas f v = max 0 (v - 1)
-  let thread_gas f v =  max 0 (v - 1)
+  let thread_gas f v = max 0 (v - 1)
 end
 
 module PerFunctionGas(GasVal:GasVal):Gas = struct
-  module V = Lattice.Chain (struct include GasVal let names x = Format.asprintf "%d" x end)
-  module M = MapDomain.MapTop_LiftBot(CilType.Fundec)(V)
-  let startgas () = M.empty ()  (* get_int "ana.context.gas_value" *)
-  let is_exhausted f v = (* v <= 0 *) true
-  let is_any_exhausted v = (* v <= 0 *) true
-  let callee_gas f v = v  (* max 0 (v - 1) *)
+  module G = Lattice.Chain (struct include GasVal let names x = Format.asprintf "%d" x end)
+  module M = MapDomain.MapTop_LiftBot(CilType.Fundec)(G)
+  let startgas () = M.empty ()
+  let is_exhausted f v = GobOption.exists (fun g -> g <= 0) (M.find_opt f v)  (* v <= 0 *)
+  let is_any_exhausted v = M.exists (fun _ g -> g <=0) v
+  let callee_gas f v =
+    let c = Option.default (G.top ()) (M.find_opt f v) in
+    M.add f (max 0 c-1) v
   let thread_gas f v = v (*  max 0 (v - 1) *)
 end
 

From 300a195840ef9d4db014aaef9de6f3c1224fb563 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 20 Sep 2024 18:13:18 +0200
Subject: [PATCH 04/16] Complete `thread_gas`

---
 src/framework/constraints.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 5bc83fbe13..ce10393d06 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -542,7 +542,12 @@ module PerFunctionGas(GasVal:GasVal):Gas = struct
   let callee_gas f v =
     let c = Option.default (G.top ()) (M.find_opt f v) in
     M.add f (max 0 c-1) v
-  let thread_gas f v = v (*  max 0 (v - 1) *)
+  let thread_gas f v =
+    match Cilfacade.find_varinfo_fundec f with
+    | fd ->
+      callee_gas fd v
+    | exception Not_found ->
+      callee_gas Cil.dummyFunDec v
 end
 
 

From 33aee5adde94fe4af03d0f39cb7a819f83d43bad Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 20 Sep 2024 18:25:07 +0200
Subject: [PATCH 05/16] Expose context gas scope via option

---
 src/config/options.schema.json | 8 ++++++++
 src/framework/control.ml       | 3 ++-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 7b07c3ca35..03b3d28fa8 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -998,6 +998,14 @@
               "type": "integer",
               "default": -1
             },
+            "gas_scope": {
+              "title": "ana.context.gas_scope",
+              "description":
+                "Whether the gas should be  'global' (default) or per 'function'",
+              "type": "string",
+              "enum": ["global","function"],
+              "default": "global"
+            },
             "callString_length": {
               "title": "ana.context.callString_length",
               "description": "Length of the call string that should be used as context for the call_string and/or call_site analyses. In case the value is zero, the analysis is context-insensitive. For a negative value, an infinite call string is used! For this option to have an effect, one of the analyses in `callstring.ml` must be activated.",
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 68c31768c6..df57878035 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -28,7 +28,8 @@ let spec_module: (module Spec) Lazy.t = lazy (
   let module S1 =
     (val
       (module MCP.MCP2 : Spec)
-      |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter(GlobalGas(GasVal)))
+      |> lift (get_int "ana.context.gas_value" >= 0 && get_string "ana.context.gas_scope" = "global") (module ContextGasLifter(GlobalGas(GasVal)))
+      |> lift (get_int "ana.context.gas_value" >= 0 && get_string "ana.context.gas_scope" = "function") (module ContextGasLifter(PerFunctionGas(GasVal)))
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)

From 3c0ff8c927558a574c7454c6d08d9e8b445d1ebe Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 20 Sep 2024 18:38:07 +0200
Subject: [PATCH 06/16] Two regresion tests

---
 tests/regression/80-context_gas/23-per-fun.c  | 29 ++++++++++++
 .../regression/80-context_gas/24-per-fun-ex.c | 44 +++++++++++++++++++
 2 files changed, 73 insertions(+)
 create mode 100644 tests/regression/80-context_gas/23-per-fun.c
 create mode 100644 tests/regression/80-context_gas/24-per-fun-ex.c

diff --git a/tests/regression/80-context_gas/23-per-fun.c b/tests/regression/80-context_gas/23-per-fun.c
new file mode 100644
index 0000000000..1f64317b0f
--- /dev/null
+++ b/tests/regression/80-context_gas/23-per-fun.c
@@ -0,0 +1,29 @@
+// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 3 --set ana.context.gas_scope function
+int nr(int x, int y) {
+    // Non-recursive, but would fail with global scope as gas for f is exhausted
+    __goblint_check(x==y);
+}
+
+int f(int x, int y)
+{
+    int top;
+    if (x == 0)
+    {
+        return y;
+    }
+
+    if(top) {
+        nr(5,5);
+    } else {
+        nr(6,6);
+    }
+
+    return f(x - 1, y - 1);
+}
+
+int main()
+{
+    // main -> f(3,3) -> f(2,2) -> f(1,1) -> f(0,0) -> return 0
+    // 4 recursive calls -> boundary (excluded)
+    __goblint_check(f(3, 3) == 0); // UNKNOWN
+}
diff --git a/tests/regression/80-context_gas/24-per-fun-ex.c b/tests/regression/80-context_gas/24-per-fun-ex.c
new file mode 100644
index 0000000000..ab5d203c45
--- /dev/null
+++ b/tests/regression/80-context_gas/24-per-fun-ex.c
@@ -0,0 +1,44 @@
+// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 3 --set ana.context.gas_scope function
+int nr(int x, int y) {
+    // Non-recursive, but would fail with global scope as gas for f is exhausted
+    __goblint_check(x==y);
+}
+
+// Checks that gas is also applied to further functions
+int g(int x, int y)
+{
+    int top;
+    if (x < -100000)
+    {
+        return y;
+    }
+
+    if(top) {
+        nr(5,5);
+    } else {
+        nr(6,6);
+    }
+
+    return g(x - 1, y - 1);
+}
+
+int f(int x, int y)
+{
+    int top;
+
+    if (x == 0)
+    {
+        return y;
+    }
+
+    g(x,y);
+
+    return f(x - 1, y - 1);
+}
+
+int main()
+{
+    // main -> f(3,3) -> f(2,2) -> f(1,1) -> f(0,0) -> return 0
+    // 4 recursive calls -> boundary (excluded)
+    __goblint_check(f(3, 3) == 0); // UNKNOWN
+}

From a70c17295e19e8b1568e402ca953fe4bea445087 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 22 Sep 2024 13:46:47 +0200
Subject: [PATCH 07/16] Give JoinCall `f` as an argument to avoid having to
 overaproxximate gas status

---
 src/analyses/apron/relationAnalysis.apron.ml |  2 +-
 src/analyses/apron/relationPriv.apron.ml     | 18 +++++++-------
 src/analyses/base.ml                         |  2 +-
 src/analyses/basePriv.ml                     | 26 ++++++++++----------
 src/analyses/basePriv.mli                    |  2 +-
 src/analyses/commonPriv.ml                   |  4 +--
 src/analyses/mCP.ml                          |  4 +--
 src/domains/queries.ml                       | 14 ++++++-----
 src/framework/analyses.ml                    |  2 +-
 src/framework/constraints.ml                 | 11 +++------
 10 files changed, 42 insertions(+), 43 deletions(-)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index cb8e8731d9..da14dfff1d 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -772,7 +772,7 @@ struct
       PCU.RH.replace results ctx.node new_value;
     end;
     WideningTokens.with_local_side_tokens (fun () ->
-        Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread])
+        Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread])
       )
 
   let init marshal =
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index ff771e692e..15df394d54 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -36,7 +36,7 @@ module type S =
     val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t
     val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t
 
-    val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> relation_components_t
+    val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread] -> relation_components_t
 
     val escape: Node.t -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> EscapeDomain.EscapedVars.t -> relation_components_t
     val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> relation_components_t
@@ -113,10 +113,10 @@ struct
     match reason with
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation () ->
+    | `JoinCall _ when ConfCheck.branched_thread_creation () ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Normal
     | `Init
     | `Thread
@@ -385,10 +385,10 @@ struct
       end
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Normal
     | `Init
     | `Thread ->
@@ -674,10 +674,10 @@ struct
       end
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Normal
     | `Init
     | `Thread ->
@@ -1230,10 +1230,10 @@ struct
     | `Return -> st (* TODO: implement? *)
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Normal
     | `Init
     | `Thread ->
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index a69b3a2b23..a1f0b3b08f 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -453,7 +453,7 @@ struct
     else
       ctx.local
 
-  let sync ctx reason = sync' (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread]) ctx
+  let sync ctx reason = sync' (reason :> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread]) ctx
 
   let publish_all ctx reason =
     ignore (sync' reason ctx)
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 08413d54b1..946b8f8cc5 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -31,7 +31,7 @@ sig
   val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t
   val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t
 
-  val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseComponents (D).t
+  val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread] -> BaseComponents (D).t
 
   val escape: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseComponents (D).t
   val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> BaseComponents (D).t
@@ -322,10 +322,10 @@ struct
     match reason with
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Return
     | `Normal
     | `Init
@@ -433,10 +433,10 @@ struct
     match reason with
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Return
     | `Normal
     | `Init
@@ -802,10 +802,10 @@ struct
     match reason with
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Return
     | `Normal
     | `Init
@@ -1055,7 +1055,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
@@ -1111,7 +1111,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
@@ -1183,7 +1183,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
@@ -1342,7 +1342,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
@@ -1521,7 +1521,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
@@ -1704,7 +1704,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
diff --git a/src/analyses/basePriv.mli b/src/analyses/basePriv.mli
index 40e50c2a69..edcf70ec98 100644
--- a/src/analyses/basePriv.mli
+++ b/src/analyses/basePriv.mli
@@ -20,7 +20,7 @@ sig
   val lock: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t
   val unlock: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t
 
-  val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t
+  val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t
 
   val escape: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseDomain.BaseComponents (D).t
   val enter_multithreaded: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> BaseDomain.BaseComponents (D).t
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 003cdfa96c..915b3da063 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -61,7 +61,7 @@ struct
       true
 
   (** Whether branched thread creation at start nodes of procedures needs to be handled by [sync `JoinCall] of privatization. *)
-  let branched_thread_creation_at_call (ask:Queries.ask) =
+  let branched_thread_creation_at_call (ask:Queries.ask) f =
     let threadflag_active = List.mem "threadflag" (GobConfig.get_string_list "ana.activated") in
     if threadflag_active then
       let sens = GobConfig.get_string_list "ana.ctx_sens" in
@@ -74,7 +74,7 @@ struct
       if not threadflag_ctx_sens then
         true
       else
-        ask.f (Queries.GasExhausted)
+        ask.f (Queries.GasExhausted f)
     else
       true
 end
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index e4c0e261e4..6212b6de90 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -318,10 +318,10 @@ struct
              f (Result.top ()) (!base_id, spec !base_id, assoc !base_id ctx.local) *)
           | Queries.DYojson ->
             `Lifted (D.to_yojson ctx.local)
-          | Queries.GasExhausted ->
+          | Queries.GasExhausted f ->
             if (get_int "ana.context.gas_value" >= 0) then
               (* There is a lifter above this that will answer it, save to ask *)
-              ctx.ask (Queries.GasExhausted)
+              ctx.ask (Queries.GasExhausted f)
             else
               (* Abort to avoid infinite recursion *)
               false
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 5fbb244874..b0ede0cfbf 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -124,9 +124,9 @@ type _ t =
   | MustTermLoop: stmt -> MustBool.t t
   | MustTermAllLoops: MustBool.t t
   | IsEverMultiThreaded: MayBool.t t
-  | TmpSpecial:  Mval.Exp.t -> ML.t t
+  | TmpSpecial: Mval.Exp.t -> ML.t t
   | MaySignedOverflow: exp -> MayBool.t t
-  | GasExhausted: MustBool.t t
+  | GasExhausted: CilType.Fundec.t ->  MustBool.t t
 
 type 'a result = 'a
 
@@ -197,7 +197,7 @@ struct
     | IsEverMultiThreaded -> (module MayBool)
     | TmpSpecial _ -> (module ML)
     | MaySignedOverflow  _ -> (module MayBool)
-    | GasExhausted -> (module MustBool)
+    | GasExhausted _ -> (module MustBool)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -267,7 +267,7 @@ struct
     | IsEverMultiThreaded -> MayBool.top ()
     | TmpSpecial _ -> ML.top ()
     | MaySignedOverflow _ -> MayBool.top ()
-    | GasExhausted -> MustBool.top ()
+    | GasExhausted _ -> MustBool.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -334,7 +334,7 @@ struct
     | Any (TmpSpecial _) -> 56
     | Any (IsAllocVar _) -> 57
     | Any (MaySignedOverflow _) -> 58
-    | Any GasExhausted -> 59
+    | Any (GasExhausted _) -> 59
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -389,6 +389,7 @@ struct
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
       | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2
       | Any (MaySignedOverflow e1), Any (MaySignedOverflow e2) -> CilType.Exp.compare e1 e2
+      | Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2
       (* only argumentless queries should remain *)
       | _, _ -> Stdlib.compare (order a) (order b)
 
@@ -431,6 +432,7 @@ struct
     | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start
     | Any (TmpSpecial lv) -> Mval.Exp.hash lv
     | Any (MaySignedOverflow e) -> CilType.Exp.hash e
+    | Any (GasExhausted f) -> CilType.Fundec.hash f
     (* IterSysVars:                                                                    *)
     (*   - argument is a function and functions cannot be compared in any meaningful way. *)
     (*   - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *)
@@ -494,7 +496,7 @@ struct
     | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded"
     | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv
     | Any (MaySignedOverflow e) -> Pretty.dprintf "MaySignedOverflow %a" CilType.Exp.pretty e
-    | Any GasExhausted -> Pretty.dprintf "GasExhausted"
+    | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f
 end
 
 let to_value_domain_ask (ask: ask) =
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 717507802f..bb494382d7 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -208,7 +208,7 @@ sig
   val context: (D.t, G.t, C.t, V.t) ctx -> fundec -> D.t -> C.t
   val startcontext: unit -> C.t
 
-  val sync  : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `JoinCall | `Return] -> D.t
+  val sync  : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return] -> D.t
   val query : (D.t, G.t, C.t, V.t) ctx -> 'a Queries.t -> 'a Queries.result
 
   (** A transfer function which handles the assignment of a rval to a lval, i.e.,
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index ce10393d06..b1c3919bd4 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -516,7 +516,6 @@ module type Gas = sig
   module M:Lattice.S
   val startgas: unit -> M.t
   val is_exhausted: fundec -> M.t -> bool
-  val is_any_exhausted: M.t -> bool
   val callee_gas: fundec -> M.t -> M.t
   val thread_gas: varinfo -> M.t -> M.t
 end
@@ -525,7 +524,6 @@ module GlobalGas(GasVal:GasVal):Gas = struct
   module M = Lattice.Chain (struct include GasVal let names x = Format.asprintf "%d" x end)
   let startgas () = M.top () (*  get_int "ana.context.gas_value" *)
 
-  let is_any_exhausted v = v <= 0
   let is_exhausted _  = is_any_exhausted
 
   (* callee gas = caller gas - 1 *)
@@ -538,7 +536,6 @@ module PerFunctionGas(GasVal:GasVal):Gas = struct
   module M = MapDomain.MapTop_LiftBot(CilType.Fundec)(G)
   let startgas () = M.empty ()
   let is_exhausted f v = GobOption.exists (fun g -> g <= 0) (M.find_opt f v)  (* v <= 0 *)
-  let is_any_exhausted v = M.exists (fun _ g -> g <=0) v
   let callee_gas f v =
     let c = Option.default (G.top ()) (M.find_opt f v) in
     M.add f (max 0 c-1) v
@@ -613,10 +610,10 @@ struct
 
   let query ctx (type a) (q: a Queries.t):a Queries.result =
     match q with
-    | Queries.GasExhausted ->
+    | Queries.GasExhausted f ->
       (* The query is only used in a way where overapproximating gas exhaustion is not harmful *)
       let (d,i) = ctx.local in
-      Gas.is_any_exhausted i
+      Gas.is_exhausted f i
     | _ -> S.query (conv ctx) q
 
   let sync ctx reason                             = S.sync (conv ctx) reason, cg_val ctx
@@ -669,8 +666,8 @@ struct
     match ctx.prev_node, Cfg.prev ctx.prev_node with
     | _, _ :: _ :: _ -> (* Join in CFG. *)
       S.sync ctx `Join
-    | FunctionEntry _, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *)
-      S.sync ctx `JoinCall
+    | FunctionEntry f, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *)
+      S.sync ctx (`JoinCall f)
     | _, _ -> S.sync ctx `Normal
 
   let side_context sideg f c =

From 1c2c428680c00e27c01abcb34fcb3f462a26aa1c Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 22 Sep 2024 13:48:18 +0200
Subject: [PATCH 08/16] Outdated comment

---
 src/framework/constraints.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index b1c3919bd4..1794443bd1 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -611,7 +611,6 @@ struct
   let query ctx (type a) (q: a Queries.t):a Queries.result =
     match q with
     | Queries.GasExhausted f ->
-      (* The query is only used in a way where overapproximating gas exhaustion is not harmful *)
       let (d,i) = ctx.local in
       Gas.is_exhausted f i
     | _ -> S.query (conv ctx) q

From d2fc47671fcaa2daba7dad032dabeda98fc17171 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 22 Sep 2024 13:50:54 +0200
Subject: [PATCH 09/16] Fix compilation

---
 src/framework/constraints.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 1794443bd1..b9553b974a 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -524,7 +524,7 @@ module GlobalGas(GasVal:GasVal):Gas = struct
   module M = Lattice.Chain (struct include GasVal let names x = Format.asprintf "%d" x end)
   let startgas () = M.top () (*  get_int "ana.context.gas_value" *)
 
-  let is_exhausted _  = is_any_exhausted
+  let is_exhausted _ v  = v <= 0
 
   (* callee gas = caller gas - 1 *)
   let callee_gas f v = max 0 (v - 1)

From 5ea31d5d9533d5eee5a644237c388e5346f09e41 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 22 Sep 2024 14:16:02 +0200
Subject: [PATCH 10/16] I won the fight with first-class modules

---
 src/framework/control.ml | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index df57878035..96b7ff41d4 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -18,18 +18,23 @@ let spec_module: (module Spec) Lazy.t = lazy (
   let arg_enabled = get_bool "witness.graphml.enabled" || get_bool "exp.arg.enabled" in
   let termination_enabled = List.mem "termination" (get_string_list "ana.activated") in (* check if loop termination analysis is enabled*)
   let open Batteries in
+  let gas () =
+    let module GasVal = struct
+      (* Chain lattice has elements [0,n-1], but we want [0,gas_value] *)
+      let n () = get_int "ana.context.gas_value" + 1
+    end
+    in
+    if get_string "ana.context.gas_scope" = "global" then
+      (module GlobalGas(GasVal):Gas)
+    else
+      (module PerFunctionGas(GasVal):Gas)
+  in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
-  let module GasVal = struct
-    (* Chain lattice has elements [0,n-1], but we want [0,gas_value] *)
-    let n () = get_int "ana.context.gas_value" + 1
-  end
-  in
   let module S1 =
     (val
       (module MCP.MCP2 : Spec)
-      |> lift (get_int "ana.context.gas_value" >= 0 && get_string "ana.context.gas_scope" = "global") (module ContextGasLifter(GlobalGas(GasVal)))
-      |> lift (get_int "ana.context.gas_value" >= 0 && get_string "ana.context.gas_scope" = "function") (module ContextGasLifter(PerFunctionGas(GasVal)))
+      |> lift (get_int "ana.context.gas_value" >= 0) (let (module Gas) = gas () in (module ContextGasLifter(Gas)))
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)

From d421731e55c78505c769247ebeb63f4d75a64b4c Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 22 Sep 2024 14:57:00 +0200
Subject: [PATCH 11/16] Comment why `top` is maximal gas.

Co-authored-by: Julian Erhard <julian.erhard@tum.de>
---
 src/framework/constraints.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index b9553b974a..5ba9f034c2 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -522,7 +522,7 @@ end
 
 module GlobalGas(GasVal:GasVal):Gas = struct
   module M = Lattice.Chain (struct include GasVal let names x = Format.asprintf "%d" x end)
-  let startgas () = M.top () (*  get_int "ana.context.gas_value" *)
+  let startgas () = M.top () (* M.top () yields maximal gas value *)
 
   let is_exhausted _ v  = v <= 0
 

From 3ee79bf980bee30691884652d76d795c338588c7 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 22 Sep 2024 15:23:07 +0200
Subject: [PATCH 12/16] Embrace dynamic nature of everything

---
 src/framework/analyses.ml    |  2 +
 src/framework/constraints.ml | 71 ++++++++++++++++++++----------------
 src/framework/control.ml     | 15 +-------
 3 files changed, 43 insertions(+), 45 deletions(-)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index bb494382d7..ab41335944 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -274,6 +274,8 @@ sig
   val event : (D.t, G.t, C.t, V.t) ctx -> Events.t -> (D.t, G.t, C.t, V.t) ctx -> D.t
 end
 
+module type Spec2Spec = functor (S: Spec) -> Spec
+
 module type MCPA =
 sig
   include Printable.S
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 5ba9f034c2..167ad08484 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -508,10 +508,6 @@ end
 
 module NoContext = struct let name = "no context" end
 
-module type GasVal = sig
-  val n: unit -> int
-end
-
 module type Gas = sig
   module M:Lattice.S
   val startgas: unit -> M.t
@@ -520,34 +516,6 @@ module type Gas = sig
   val thread_gas: varinfo -> M.t -> M.t
 end
 
-module GlobalGas(GasVal:GasVal):Gas = struct
-  module M = Lattice.Chain (struct include GasVal let names x = Format.asprintf "%d" x end)
-  let startgas () = M.top () (* M.top () yields maximal gas value *)
-
-  let is_exhausted _ v  = v <= 0
-
-  (* callee gas = caller gas - 1 *)
-  let callee_gas f v = max 0 (v - 1)
-  let thread_gas f v = max 0 (v - 1)
-end
-
-module PerFunctionGas(GasVal:GasVal):Gas = struct
-  module G = Lattice.Chain (struct include GasVal let names x = Format.asprintf "%d" x end)
-  module M = MapDomain.MapTop_LiftBot(CilType.Fundec)(G)
-  let startgas () = M.empty ()
-  let is_exhausted f v = GobOption.exists (fun g -> g <= 0) (M.find_opt f v)  (* v <= 0 *)
-  let callee_gas f v =
-    let c = Option.default (G.top ()) (M.find_opt f v) in
-    M.add f (max 0 c-1) v
-  let thread_gas f v =
-    match Cilfacade.find_varinfo_fundec f with
-    | fd ->
-      callee_gas fd v
-    | exception Not_found ->
-      callee_gas Cil.dummyFunDec v
-end
-
-
 (** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
     For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
 module ContextGasLifter (Gas:Gas) (S:Spec)
@@ -631,6 +599,45 @@ struct
   let event ctx e octx                            = S.event (conv ctx) e (conv octx), cg_val ctx
 end
 
+let get_gas_lifter () =
+  let module GasChain = Lattice.Chain (struct
+      (* Chain lattice has elements [0,n-1], but we want [0,gas_value] *)
+      let n () = get_int "ana.context.gas_value" + 1
+      let names x = Format.asprintf "%d" x
+    end)
+  in
+  if get_string "ana.context.gas_scope" = "global" then
+    let module GlobalGas:Gas = struct
+      module M = GasChain
+      let startgas () = M.top () (* M.top () yields maximal gas value *)
+
+      let is_exhausted _ v  = v <= 0
+
+      (* callee gas = caller gas - 1 *)
+      let callee_gas f v = max 0 (v - 1)
+      let thread_gas f v = max 0 (v - 1)
+    end
+    in
+    (module ContextGasLifter(GlobalGas):Spec2Spec)
+  else
+    let module PerFunctionGas:Gas = struct
+      module G = GasChain
+      module M = MapDomain.MapTop_LiftBot(CilType.Fundec)(G)
+      let startgas () = M.empty ()
+      let is_exhausted f v = GobOption.exists (fun g -> g <= 0) (M.find_opt f v)  (* v <= 0 *)
+      let callee_gas f v =
+        let c = Option.default (G.top ()) (M.find_opt f v) in
+        M.add f (max 0 c-1) v
+      let thread_gas f v =
+        match Cilfacade.find_varinfo_fundec f with
+        | fd ->
+          callee_gas fd v
+        | exception Not_found ->
+          callee_gas Cil.dummyFunDec v
+    end
+    in
+    (module ContextGasLifter(PerFunctionGas):Spec2Spec)
+
 
 module type Increment =
 sig
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 96b7ff41d4..856695e690 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -10,7 +10,7 @@ open ConstrSys
 open GobConfig
 open Constraints
 
-module type S2S = functor (X : Spec) -> Spec
+module type S2S = Spec2Spec
 
 (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
 let spec_module: (module Spec) Lazy.t = lazy (
@@ -18,23 +18,12 @@ let spec_module: (module Spec) Lazy.t = lazy (
   let arg_enabled = get_bool "witness.graphml.enabled" || get_bool "exp.arg.enabled" in
   let termination_enabled = List.mem "termination" (get_string_list "ana.activated") in (* check if loop termination analysis is enabled*)
   let open Batteries in
-  let gas () =
-    let module GasVal = struct
-      (* Chain lattice has elements [0,n-1], but we want [0,gas_value] *)
-      let n () = get_int "ana.context.gas_value" + 1
-    end
-    in
-    if get_string "ana.context.gas_scope" = "global" then
-      (module GlobalGas(GasVal):Gas)
-    else
-      (module PerFunctionGas(GasVal):Gas)
-  in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
   let module S1 =
     (val
       (module MCP.MCP2 : Spec)
-      |> lift (get_int "ana.context.gas_value" >= 0) (let (module Gas) = gas () in (module ContextGasLifter(Gas)))
+      |> lift (get_int "ana.context.gas_value" >= 0) (Constraints.get_gas_lifter ())
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)

From 426ec6964f777e3901952569916dd4eb63295cf3 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 22 Sep 2024 15:31:39 +0200
Subject: [PATCH 13/16] Make `contextGasLifter` its own module

---
 src/framework/constraints.ml       | 133 ---------------------------
 src/framework/contextGasLifter.ml  | 140 +++++++++++++++++++++++++++++
 src/framework/contextGasLifter.mli |   1 +
 src/framework/control.ml           |   2 +-
 4 files changed, 142 insertions(+), 134 deletions(-)
 create mode 100644 src/framework/contextGasLifter.ml
 create mode 100644 src/framework/contextGasLifter.mli

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 167ad08484..23cc297439 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -506,139 +506,6 @@ struct
   let event (ctx:(D.t,G.t,C.t,V.t) ctx) (e:Events.t) (octx:(D.t,G.t,C.t,V.t) ctx):D.t = lift_fun ctx D.lift S.event ((|>) (conv octx) % (|>) e) `Bot
 end
 
-module NoContext = struct let name = "no context" end
-
-module type Gas = sig
-  module M:Lattice.S
-  val startgas: unit -> M.t
-  val is_exhausted: fundec -> M.t -> bool
-  val callee_gas: fundec -> M.t -> M.t
-  val thread_gas: varinfo -> M.t -> M.t
-end
-
-(** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
-    For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
-module ContextGasLifter (Gas:Gas) (S:Spec)
-  : Spec with module D = Lattice.Prod (S.D) (Gas.M)
-          and module C = Printable.Option (S.C) (NoContext)
-          and module G = S.G
-=
-struct
-  include S
-
-  module Context_Gas_Prod (Base1: Lattice.S) (Base2: Lattice.S) =
-  struct
-    include Lattice.Prod (Base1) (Base2)
-    let printXml f (x,y) =
-      BatPrintf.fprintf f "\n%a<analysis name=\"context gas value\">\n%a\n</analysis>" Base1.printXml x Base2.printXml y
-  end
-  module D = Context_Gas_Prod (S.D) (Gas.M) (* Product of S.D and an integer, tracking the context gas value *)
-  module C = Printable.Option (S.C) (NoContext)
-  module G = S.G
-  module V = S.V
-  module P =
-  struct
-    include S.P
-    let of_elt (x, _) = of_elt x
-  end
-
-  (* returns context gas value of the given ctx *)
-  let cg_val ctx = snd ctx.local
-
-  type marshal = S.marshal
-  let init = S.init
-  let finalize = S.finalize
-
-
-  let startcontext () = Some (S.startcontext ())
-  let name () = S.name ()^" with context gas"
-  let startstate v = S.startstate v, Gas.startgas ()
-  let exitstate v = S.exitstate v, Gas.startgas ()
-  let morphstate v (d,i) = S.morphstate v d, i
-
-  let conv (ctx:(D.t,G.t,C.t,V.t) ctx): (S.D.t,G.t,S.C.t,V.t)ctx =
-    {ctx with local = fst ctx.local
-            ; split = (fun d es -> ctx.split (d, cg_val ctx) es)
-            ; context = (fun () -> match ctx.context () with Some c -> c | None -> ctx_failwith "no context (contextGas = 0)")}
-
-  let context ctx fd (d,i) =
-    (* only keep context if the context gas is greater zero *)
-    if Gas.is_exhausted fd i then
-      None
-    else
-      Some (S.context (conv ctx) fd d)
-
-  let enter ctx r f args =
-    let liftmap_tup = List.map (fun (x,y) -> (x, cg_val ctx), (y, Gas.callee_gas f (cg_val ctx))) in
-    liftmap_tup (S.enter (conv ctx) r f args)
-
-  let threadenter ctx ~multiple lval f args =
-    let liftmap d = List.map (fun (x) -> (x, Gas.thread_gas f (cg_val ctx))) d in
-    liftmap (S.threadenter (conv ctx) ~multiple lval f args)
-
-  let query ctx (type a) (q: a Queries.t):a Queries.result =
-    match q with
-    | Queries.GasExhausted f ->
-      let (d,i) = ctx.local in
-      Gas.is_exhausted f i
-    | _ -> S.query (conv ctx) q
-
-  let sync ctx reason                             = S.sync (conv ctx) reason, cg_val ctx
-  let assign ctx lval expr                        = S.assign (conv ctx) lval expr, cg_val ctx
-  let vdecl ctx v                                 = S.vdecl (conv ctx) v, cg_val ctx
-  let body ctx fundec                             = S.body (conv ctx) fundec, cg_val ctx
-  let branch ctx e tv                             = S.branch (conv ctx) e tv, cg_val ctx
-  let return ctx r f                              = S.return (conv ctx) r f, cg_val ctx
-  let asm ctx                                     = S.asm (conv ctx), cg_val ctx
-  let skip ctx                                    = S.skip (conv ctx), cg_val ctx
-  let special ctx r f args                        = S.special (conv ctx) r f args, cg_val ctx
-  let combine_env ctx r fe f args fc es f_ask     = S.combine_env (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
-  let combine_assign ctx r fe f args fc es f_ask  = S.combine_assign (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
-  let paths_as_set ctx                            = List.map (fun (x) -> (x, cg_val ctx)) @@ S.paths_as_set (conv ctx)
-  let threadspawn ctx ~multiple lval f args fctx  = S.threadspawn (conv ctx) ~multiple lval f args (conv fctx), cg_val ctx
-  let event ctx e octx                            = S.event (conv ctx) e (conv octx), cg_val ctx
-end
-
-let get_gas_lifter () =
-  let module GasChain = Lattice.Chain (struct
-      (* Chain lattice has elements [0,n-1], but we want [0,gas_value] *)
-      let n () = get_int "ana.context.gas_value" + 1
-      let names x = Format.asprintf "%d" x
-    end)
-  in
-  if get_string "ana.context.gas_scope" = "global" then
-    let module GlobalGas:Gas = struct
-      module M = GasChain
-      let startgas () = M.top () (* M.top () yields maximal gas value *)
-
-      let is_exhausted _ v  = v <= 0
-
-      (* callee gas = caller gas - 1 *)
-      let callee_gas f v = max 0 (v - 1)
-      let thread_gas f v = max 0 (v - 1)
-    end
-    in
-    (module ContextGasLifter(GlobalGas):Spec2Spec)
-  else
-    let module PerFunctionGas:Gas = struct
-      module G = GasChain
-      module M = MapDomain.MapTop_LiftBot(CilType.Fundec)(G)
-      let startgas () = M.empty ()
-      let is_exhausted f v = GobOption.exists (fun g -> g <= 0) (M.find_opt f v)  (* v <= 0 *)
-      let callee_gas f v =
-        let c = Option.default (G.top ()) (M.find_opt f v) in
-        M.add f (max 0 c-1) v
-      let thread_gas f v =
-        match Cilfacade.find_varinfo_fundec f with
-        | fd ->
-          callee_gas fd v
-        | exception Not_found ->
-          callee_gas Cil.dummyFunDec v
-    end
-    in
-    (module ContextGasLifter(PerFunctionGas):Spec2Spec)
-
-
 module type Increment =
 sig
   val increment: increment_data option
diff --git a/src/framework/contextGasLifter.ml b/src/framework/contextGasLifter.ml
new file mode 100644
index 0000000000..155eae2d78
--- /dev/null
+++ b/src/framework/contextGasLifter.ml
@@ -0,0 +1,140 @@
+open Batteries
+open GoblintCil
+open MyCFG
+open Analyses
+open ConstrSys
+open GobConfig
+
+module M = Messages
+
+module NoContext = struct let name = "no context" end
+
+module type Gas = sig
+  module M:Lattice.S
+  val startgas: unit -> M.t
+  val is_exhausted: fundec -> M.t -> bool
+  val callee_gas: fundec -> M.t -> M.t
+  val thread_gas: varinfo -> M.t -> M.t
+end
+
+(** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
+    For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
+module ContextGasLifter (Gas:Gas) (S:Spec)
+  : Spec with module D = Lattice.Prod (S.D) (Gas.M)
+          and module C = Printable.Option (S.C) (NoContext)
+          and module G = S.G
+=
+struct
+  include S
+
+  module Context_Gas_Prod (Base1: Lattice.S) (Base2: Lattice.S) =
+  struct
+    include Lattice.Prod (Base1) (Base2)
+    let printXml f (x,y) =
+      BatPrintf.fprintf f "\n%a<analysis name=\"context gas value\">\n%a\n</analysis>" Base1.printXml x Base2.printXml y
+  end
+  module D = Context_Gas_Prod (S.D) (Gas.M) (* Product of S.D and an integer, tracking the context gas value *)
+  module C = Printable.Option (S.C) (NoContext)
+  module G = S.G
+  module V = S.V
+  module P =
+  struct
+    include S.P
+    let of_elt (x, _) = of_elt x
+  end
+
+  (* returns context gas value of the given ctx *)
+  let cg_val ctx = snd ctx.local
+
+  type marshal = S.marshal
+  let init = S.init
+  let finalize = S.finalize
+
+
+  let startcontext () = Some (S.startcontext ())
+  let name () = S.name ()^" with context gas"
+  let startstate v = S.startstate v, Gas.startgas ()
+  let exitstate v = S.exitstate v, Gas.startgas ()
+  let morphstate v (d,i) = S.morphstate v d, i
+
+  let conv (ctx:(D.t,G.t,C.t,V.t) ctx): (S.D.t,G.t,S.C.t,V.t)ctx =
+    {ctx with local = fst ctx.local
+            ; split = (fun d es -> ctx.split (d, cg_val ctx) es)
+            ; context = (fun () -> match ctx.context () with Some c -> c | None -> ctx_failwith "no context (contextGas = 0)")}
+
+  let context ctx fd (d,i) =
+    (* only keep context if the context gas is greater zero *)
+    if Gas.is_exhausted fd i then
+      None
+    else
+      Some (S.context (conv ctx) fd d)
+
+  let enter ctx r f args =
+    let liftmap_tup = List.map (fun (x,y) -> (x, cg_val ctx), (y, Gas.callee_gas f (cg_val ctx))) in
+    liftmap_tup (S.enter (conv ctx) r f args)
+
+  let threadenter ctx ~multiple lval f args =
+    let liftmap d = List.map (fun (x) -> (x, Gas.thread_gas f (cg_val ctx))) d in
+    liftmap (S.threadenter (conv ctx) ~multiple lval f args)
+
+  let query ctx (type a) (q: a Queries.t):a Queries.result =
+    match q with
+    | Queries.GasExhausted f ->
+      let (d,i) = ctx.local in
+      Gas.is_exhausted f i
+    | _ -> S.query (conv ctx) q
+
+  let sync ctx reason                             = S.sync (conv ctx) reason, cg_val ctx
+  let assign ctx lval expr                        = S.assign (conv ctx) lval expr, cg_val ctx
+  let vdecl ctx v                                 = S.vdecl (conv ctx) v, cg_val ctx
+  let body ctx fundec                             = S.body (conv ctx) fundec, cg_val ctx
+  let branch ctx e tv                             = S.branch (conv ctx) e tv, cg_val ctx
+  let return ctx r f                              = S.return (conv ctx) r f, cg_val ctx
+  let asm ctx                                     = S.asm (conv ctx), cg_val ctx
+  let skip ctx                                    = S.skip (conv ctx), cg_val ctx
+  let special ctx r f args                        = S.special (conv ctx) r f args, cg_val ctx
+  let combine_env ctx r fe f args fc es f_ask     = S.combine_env (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
+  let combine_assign ctx r fe f args fc es f_ask  = S.combine_assign (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
+  let paths_as_set ctx                            = List.map (fun (x) -> (x, cg_val ctx)) @@ S.paths_as_set (conv ctx)
+  let threadspawn ctx ~multiple lval f args fctx  = S.threadspawn (conv ctx) ~multiple lval f args (conv fctx), cg_val ctx
+  let event ctx e octx                            = S.event (conv ctx) e (conv octx), cg_val ctx
+end
+
+let get_gas_lifter () =
+  let module GasChain = Lattice.Chain (struct
+      (* Chain lattice has elements [0,n-1], but we want [0,gas_value] *)
+      let n () = get_int "ana.context.gas_value" + 1
+      let names x = Format.asprintf "%d" x
+    end)
+  in
+  if get_string "ana.context.gas_scope" = "global" then
+    let module GlobalGas:Gas = struct
+      module M = GasChain
+      let startgas () = M.top () (* M.top () yields maximal gas value *)
+
+      let is_exhausted _ v  = v <= 0
+
+      (* callee gas = caller gas - 1 *)
+      let callee_gas f v = max 0 (v - 1)
+      let thread_gas f v = max 0 (v - 1)
+    end
+    in
+    (module ContextGasLifter(GlobalGas):Spec2Spec)
+  else
+    let module PerFunctionGas:Gas = struct
+      module G = GasChain
+      module M = MapDomain.MapTop_LiftBot(CilType.Fundec)(G)
+      let startgas () = M.empty ()
+      let is_exhausted f v = GobOption.exists (fun g -> g <= 0) (M.find_opt f v)  (* v <= 0 *)
+      let callee_gas f v =
+        let c = Option.default (G.top ()) (M.find_opt f v) in
+        M.add f (max 0 c-1) v
+      let thread_gas f v =
+        match Cilfacade.find_varinfo_fundec f with
+        | fd ->
+          callee_gas fd v
+        | exception Not_found ->
+          callee_gas Cil.dummyFunDec v
+    end
+    in
+    (module ContextGasLifter(PerFunctionGas):Spec2Spec)
diff --git a/src/framework/contextGasLifter.mli b/src/framework/contextGasLifter.mli
new file mode 100644
index 0000000000..4f8ce4fb72
--- /dev/null
+++ b/src/framework/contextGasLifter.mli
@@ -0,0 +1 @@
+val get_gas_lifter : unit -> (module Analyses.Spec2Spec)
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 856695e690..7ea144e1d1 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -23,7 +23,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
   let module S1 =
     (val
       (module MCP.MCP2 : Spec)
-      |> lift (get_int "ana.context.gas_value" >= 0) (Constraints.get_gas_lifter ())
+      |> lift (get_int "ana.context.gas_value" >= 0) (ContextGasLifter.get_gas_lifter ())
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)

From 7112baffc61ce6b4883ab409f8734bba34594f97 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 22 Sep 2024 15:35:11 +0200
Subject: [PATCH 14/16] Document context gas lifter

---
 src/framework/contextGasLifter.ml | 5 +++--
 src/goblint_lib.ml                | 1 +
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/framework/contextGasLifter.ml b/src/framework/contextGasLifter.ml
index 155eae2d78..6a991b1f58 100644
--- a/src/framework/contextGasLifter.ml
+++ b/src/framework/contextGasLifter.ml
@@ -1,3 +1,6 @@
+(** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
+    For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
+
 open Batteries
 open GoblintCil
 open MyCFG
@@ -17,8 +20,6 @@ module type Gas = sig
   val thread_gas: varinfo -> M.t -> M.t
 end
 
-(** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
-    For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
 module ContextGasLifter (Gas:Gas) (S:Spec)
   : Spec with module D = Lattice.Prod (S.D) (Gas.M)
           and module C = Printable.Option (S.C) (NoContext)
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 8013d9b2fe..1743e87bea 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -26,6 +26,7 @@ module Constraints = Constraints
 module AnalysisState = AnalysisState
 module AnalysisStateUtil = AnalysisStateUtil
 module ControlSpecC = ControlSpecC
+module ContextGasLifter = ContextGasLifter
 
 (** Master control program (MCP) is the analysis specification for the dynamic product of activated analyses. *)
 

From d76e40ec0312fa044318a41eea398efe4ba01830 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 23 Sep 2024 10:45:41 +0200
Subject: [PATCH 15/16] Duplicate module synopsis

---
 src/framework/contextGasLifter.mli | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/framework/contextGasLifter.mli b/src/framework/contextGasLifter.mli
index 4f8ce4fb72..f5b07e2b35 100644
--- a/src/framework/contextGasLifter.mli
+++ b/src/framework/contextGasLifter.mli
@@ -1 +1,5 @@
+(** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
+    For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
+
+(** Gets the appropriate lifter (either local or per-function). Should only be called when context gas is active. *)
 val get_gas_lifter : unit -> (module Analyses.Spec2Spec)

From c4c9c89e0446ff2619deb961525583f4d37e4f44 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 23 Sep 2024 10:48:11 +0200
Subject: [PATCH 16/16] Update outdated comment

---
 src/framework/contextGasLifter.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/framework/contextGasLifter.ml b/src/framework/contextGasLifter.ml
index 6a991b1f58..adb55aa7a2 100644
--- a/src/framework/contextGasLifter.ml
+++ b/src/framework/contextGasLifter.ml
@@ -34,7 +34,7 @@ struct
     let printXml f (x,y) =
       BatPrintf.fprintf f "\n%a<analysis name=\"context gas value\">\n%a\n</analysis>" Base1.printXml x Base2.printXml y
   end
-  module D = Context_Gas_Prod (S.D) (Gas.M) (* Product of S.D and an integer, tracking the context gas value *)
+  module D = Context_Gas_Prod (S.D) (Gas.M) (* Product of S.D and a value from the gas module, tracking the context gas value *)
   module C = Printable.Option (S.C) (NoContext)
   module G = S.G
   module V = S.V