Context Gas per Function ⛽

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.",

src/framework/constraints.ml

@@ -507,16 +507,54 @@ 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
+  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(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 *)
+  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 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 =
+    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 (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 +567,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 +587,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

src/framework/control.ml

@@ -20,10 +20,16 @@ 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)
+      |> 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)

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
+}

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
+}