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/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/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..ab41335944 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.,
@@ -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 7df4167acd..23cc297439 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -506,99 +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 IntConf =
-struct
- let n () = max_int
- let names x = Format.asprintf "%d" x
-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))
- 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\n%a\n" 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 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, get_int "ana.context.gas_value"
- let exitstate v = S.exitstate v, get_int "ana.context.gas_value"
- 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 ()))}
-
- 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)
-
- 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
- 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
- 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 ->
- let (d,i) = ctx.local in
- (i <= 0)
- | _ -> 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
-
-
module type Increment =
sig
val increment: increment_data option
@@ -632,8 +539,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 =
diff --git a/src/framework/contextGasLifter.ml b/src/framework/contextGasLifter.ml
new file mode 100644
index 0000000000..adb55aa7a2
--- /dev/null
+++ b/src/framework/contextGasLifter.ml
@@ -0,0 +1,141 @@
+(** 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
+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
+
+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\n%a\n" Base1.printXml x Base2.printXml y
+ end
+ 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
+ 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..f5b07e2b35
--- /dev/null
+++ b/src/framework/contextGasLifter.mli
@@ -0,0 +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)
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 5e92282210..7ea144e1d1 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 (
@@ -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) (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)
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. *)
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
+}