From 319ac60769975ca56158c9a1d157974251f27db2 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Thu, 20 Nov 2025 09:34:31 +0100 Subject: [PATCH 1/3] initial narrowing-by-meet --- src/analyses/apron/apronAnalysis.apron.ml | 19 ++++- src/config/options.schema.json | 6 ++ src/lifters/narrowingGas.ml | 96 +++++++++++++++++++++++ 3 files changed, 120 insertions(+), 1 deletion(-) create mode 100644 src/lifters/narrowingGas.ml diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index ccb38876cd..45d625a6a4 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -15,7 +15,24 @@ let spec_module: (module MCPSpec) Lazy.t = let name () = "apron" end in - (module Spec) + let narrowing_gas = GobConfig.get_int "ana.apron.narrowing_gas" in + if (narrowing_gas > 0) then + let module Narrowed = + struct + module PolyhedraChainParams: Printable.ChainParams = + struct + let n () = narrowing_gas + let names = string_of_int + end + include NarrowingGas.DLifter (Spec) (PolyhedraChainParams) + module A = Spec.A + let access = Spec.access + let name () = "apron" + end + in + (module Narrowed) + else + (module Spec) ) let get_spec (): (module MCPSpec) = diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 52f98ac84c..511307c2ab 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -932,6 +932,12 @@ "enum": ["octagon", "interval", "polyhedra", "affeq"], "default": "octagon" }, + "narrowing_gas": { + "title": "ana.apron.narrowing_gas", + "description": "Per state perform narrowing via meet as long as gas is left (0 to disable)", + "type": "integer", + "default": 0 + }, "threshold_widening": { "title": "ana.apron.threshold_widening", "description": diff --git a/src/lifters/narrowingGas.ml b/src/lifters/narrowingGas.ml new file mode 100644 index 0000000000..e0e0bfa730 --- /dev/null +++ b/src/lifters/narrowingGas.ml @@ -0,0 +1,96 @@ +(** narrowing delay with counters. + + Abstract elements are paired with an integer counter, indicating how many times narrowing has been delayed. + Lifted abstract elements are only narrowed if the counter exceeds a predefined limit (gas). *) + +open Batteries +open Lattice +open Analyses + +module LocalChainParams: Printable.ChainParams = +struct + let n () = GobConfig.get_int "ana.narrowing.gas" + let names = string_of_int +end + +module GlobalChainParams: Printable.ChainParams = +struct + let n () = GobConfig.get_int "ana.narrowing.gas" + let names = string_of_int +end + +module Dom (Base: S) (ChainParams: Printable.ChainParams) = +struct + module Chain = Printable.Chain (ChainParams) + include Printable.Prod (Base) (Chain) + + let lift d = (d, 0) + let unlift (d, _) = d + + let bot () = (Base.bot (), 0) + let is_bot (b, _) = Base.is_bot b + let top () = (Base.top (), ChainParams.n ()) + let is_top (b, _) = Base.is_top b + + let leq (b1, _) (b2, _) = Base.leq b1 b2 + + (** All operations keep maximal counter. *) + let join (b1, i1) (b2, i2) = (Base.join b1 b2, max i1 i2) + let meet (b1, i1) (b2, i2) = (Base.meet b1 b2, max i1 i2) + let widen (b1, i1) (b2, i2) = (Base.widen b1 b2, max i1 i2) + let narrow (b1, i1) (b2, i2) = + let i' = max i1 i2 in + if i' <= ChainParams.n () then + (Base.meet b1 b2, i' + 1) (* Stop narrowing when counter exceeds limit. *) + else + (Base.narrow b1 b2, i') + + let pretty_diff () ((b1, _), (b2, _)) = + Base.pretty_diff () (b1, b2) (* Counters cannot violate leq. *) +end + + +(** Lift {!S} to use widening delay for local states. + + All transfer functions reset the counter to 0, so counting only happens between old and new values at a local unknown. *) +module DLifter (S: Spec) (C: Printable.ChainParams): Spec = +struct + module DD (D: Lattice.S) = + struct + include Dom (D) (C) + + let printXml f (b, i) = + BatPrintf.fprintf f "%a%a" D.printXml b Chain.printXml i + end + + module NameLifter = + struct + let lift_name x = x ^ " with narrowing count" + end + include SpecLifters.DomainLifter (NameLifter) (DD) (S) + + (* Redefine morphstate and paths_as_set to keep counter instead of resetting to 0. *) + + let morphstate v (d, l) = (S.morphstate v d, l) + + let paths_as_set man = + List.map (fun x -> (x, snd man.local)) @@ S.paths_as_set (conv man) +end + +(** Lift {!S} to use widening delay for global unknowns. *) +module GLifter (S: Spec): Spec = +struct + module GG (G: Lattice.S) = + struct + include Dom (G) (GlobalChainParams) + + let printXml f (b, i) = + BatPrintf.fprintf f "%a%a" G.printXml b Chain.printXml i + end + + module NameLifter = + struct + let lift_name x = x ^ " with narrowing count" + end + include SpecLifters.GlobalDomainLifter (NameLifter) (GG) (S) +end From 4ae786f85b58bdd1d7f17c7e397cff31d834133e Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 21 Nov 2025 10:27:31 +0100 Subject: [PATCH 2/3] added regtest --- src/analyses/apron/apronAnalysis.apron.ml | 5 ++-- src/lifters/narrowingGas.ml | 2 +- .../89-apron3/04-polyhedra-narrowing1.c | 28 +++++++++++++++++++ 3 files changed, 32 insertions(+), 3 deletions(-) create mode 100644 tests/regression/89-apron3/04-polyhedra-narrowing1.c diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index 45d625a6a4..2240dbe02b 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -15,7 +15,8 @@ let spec_module: (module MCPSpec) Lazy.t = let name () = "apron" end in - let narrowing_gas = GobConfig.get_int "ana.apron.narrowing_gas" in + let narrowing_gas = GobConfig.get_int "ana.apron.narrowing_gas" + in if (narrowing_gas > 0) then let module Narrowed = struct @@ -27,7 +28,7 @@ let spec_module: (module MCPSpec) Lazy.t = include NarrowingGas.DLifter (Spec) (PolyhedraChainParams) module A = Spec.A let access = Spec.access - let name () = "apron" + let name = Spec.name end in (module Narrowed) diff --git a/src/lifters/narrowingGas.ml b/src/lifters/narrowingGas.ml index e0e0bfa730..181a6b06ff 100644 --- a/src/lifters/narrowingGas.ml +++ b/src/lifters/narrowingGas.ml @@ -40,7 +40,7 @@ struct let widen (b1, i1) (b2, i2) = (Base.widen b1 b2, max i1 i2) let narrow (b1, i1) (b2, i2) = let i' = max i1 i2 in - if i' <= ChainParams.n () then + if i' < ChainParams.n () then (Base.meet b1 b2, i' + 1) (* Stop narrowing when counter exceeds limit. *) else (Base.narrow b1 b2, i') diff --git a/tests/regression/89-apron3/04-polyhedra-narrowing1.c b/tests/regression/89-apron3/04-polyhedra-narrowing1.c new file mode 100644 index 0000000000..940b6d9f2a --- /dev/null +++ b/tests/regression/89-apron3/04-polyhedra-narrowing1.c @@ -0,0 +1,28 @@ +// SKIP TODO TERM PARAM: --set ana.apron.narrowing_gas 1 --set ana.activated[+] apron --set ana.apron.domain polyhedra +// Apron is not precise enough for some nested loops +#include +#include + +int loops0(){ + int i, j, k; + int a = 0; + for (i = 500; i >= 1; i--) + { + a++; + __goblint_check(a + i - 501 == 0); // needs 1x narrowing or octagons + int b = 0; + for (j = i; j >= 1; j--) + { + __goblint_check(a + b + j == 501); // needs 1x narrowing, octagons insufficient + b++; + } + } + return 0; +} + +int main() +{ + loops0(); + + return 0; +} From 514df801a038e948e622d216c4c24a4296d544ca Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 21 Nov 2025 10:46:21 +0100 Subject: [PATCH 3/3] cleaned up regtest --- tests/regression/89-apron3/04-polyhedra-narrowing1.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/89-apron3/04-polyhedra-narrowing1.c b/tests/regression/89-apron3/04-polyhedra-narrowing1.c index 940b6d9f2a..8d77311c16 100644 --- a/tests/regression/89-apron3/04-polyhedra-narrowing1.c +++ b/tests/regression/89-apron3/04-polyhedra-narrowing1.c @@ -1,4 +1,4 @@ -// SKIP TODO TERM PARAM: --set ana.apron.narrowing_gas 1 --set ana.activated[+] apron --set ana.apron.domain polyhedra +// SKIP PARAM: --set ana.apron.narrowing_gas 1 --set ana.activated[+] apron --set ana.apron.domain polyhedra // Apron is not precise enough for some nested loops #include #include