diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index ccb38876cd..2240dbe02b 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -15,7 +15,25 @@ 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 = Spec.name + 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..181a6b06ff --- /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 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..8d77311c16 --- /dev/null +++ b/tests/regression/89-apron3/04-polyhedra-narrowing1.c @@ -0,0 +1,28 @@ +// 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 + +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; +}