From ce1866b6e61472957c13aac891b523712c2e46ae Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 14 Oct 2024 13:06:13 +0200 Subject: [PATCH] Fix per fundec gas --- src/lifters/contextGasLifter.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/lifters/contextGasLifter.ml b/src/lifters/contextGasLifter.ml index 98974d81a1..75bd9f7641 100644 --- a/src/lifters/contextGasLifter.ml +++ b/src/lifters/contextGasLifter.ml @@ -121,12 +121,15 @@ let get_gas_lifter () = (module ContextGasLifter(GlobalGas):Spec2Spec) else let module PerFunctionGas:Gas = struct - module G = GasChain - module M = MapDomain.MapTop_LiftBot(CilType.Fundec)(G) + (* The order is reversed here to ensure that the minimum is used *) + (* 5 join 4 = 4 *) + module G = Lattice.Reverse(GasChain) + (* Missing bindings are bot, i.e., have maximal gas for this function *) + module M = MapDomain.MapBot_LiftTop(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 + let c = Option.default (G.bot ()) (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