Narrowing gas

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) =

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":

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<analysis name=\"narrow-count\">%a</analysis>" 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<analysis name=\"narrow-count\">%a</analysis>" 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

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 <goblint.h>
+#include <stdio.h>
+
+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;
+}