deleted context gas from C, is just tracked in ctx.local; updated tes…

…tcases

src/framework/constraints.ml

@@ -500,29 +500,28 @@ end
 module NoContext = struct let name = "no context" end
 module IntConf = 
 struct
-  let n () = get_int "ana.context.ctx_gas_value" + 1
+  let n () = max_int
   let names x = Format.asprintf "%d" x
 end
 
 (** Lifts a [Spec] with the context gas variable. For every function call the context gas is reduced. 
     If the context gas is 0, the remaining function calls are analyzed context insensitively (before the analysis is context sensitive) *)
 module ContextGasLifter (S:Spec)
   : Spec with module D = Lattice.Prod (S.D) (Lattice.Chain (IntConf)) 
-          and module C = Printable.Prod (Printable.Option (S.C) (NoContext)) (Printable.Chain (IntConf))
+          and module C = Printable.Option (S.C) (NoContext)
           and module G = S.G
 =
 struct
   include S
 
-  module Context_Gas_Prod (Base1: Printable.S) (Base2: Printable.S) = 
+  module Context_Gas_Prod (Base1: Lattice.S) (Base2: Lattice.S) = 
   struct 
-    include Printable.Prod (Base1) (Base2)
+    include Lattice.Prod (Base1) (Base2)
     let printXml f (x,y) =
       BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\nContext Gas Value\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base1.name ())) Base1.printXml x Base2.printXml y
   end
-
-  module D = Lattice.Prod (S.D) (Lattice.Chain (IntConf))
-  module C = Context_Gas_Prod (Printable.Option (S.C) (NoContext)) (Printable.Chain (IntConf))
+  module D = Context_Gas_Prod (S.D) (Lattice.Chain (IntConf))
+  module C = Printable.Option (S.C) (NoContext)
   module G = S.G
   module V = S.V
   module P =
@@ -532,17 +531,15 @@ struct
   end
 
   (* returns context gas value of the given ctx *)
-  let cg_val ctx = 
-    (* snd ctx.local = snd (ctx.context ()), but ctx.local must be used here due to initialization *)
-    snd ctx.local
+  let cg_val ctx = snd ctx.local
 
   let name () = S.name ()^" with context gas"
-  let startstate v = S.startstate v, (get_int "ana.context.ctx_gas_value")
-  let exitstate v = S.exitstate v, (get_int "ana.context.ctx_gas_value") (* TODO: probably doesn't matter*)
+  let startstate v = S.startstate v, get_int "ana.context.ctx_gas_value"
+  let exitstate v = S.exitstate v, get_int "ana.context.ctx_gas_value" (* TODO: probably doesn't matter*)
   let morphstate v (d,i) = S.morphstate v d, i
 
   let context fd (d,i) = 
-    if i <= 0 then (None, 0) else ((Some (S.context fd d)), i)
+    if i <= 0 then None else Some (S.context fd d)
 
   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) 
@@ -551,7 +548,7 @@ struct
                  ; 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 (fst (ctx.context ())))}
+                 ; context = (fun () -> Option.get (ctx.context ()))}
 
   let enter ctx r f args =
     let liftmap_tup = List.map (fun (x,y) -> (x, cg_val ctx), (y, max 0 (cg_val ctx - 1))) in
@@ -561,8 +558,6 @@ struct
     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 liftmap f ctx = List.map (fun (x) -> (x, cg_val ctx)) f
-
   let sync ctx reason                             = S.sync (conv ctx) reason, cg_val ctx
   let query ctx q                                 = S.query (conv ctx) q
   let assign ctx lval expr                        = S.assign (conv ctx) lval expr, cg_val ctx
@@ -573,9 +568,9 @@ struct
   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 x -> fst x)) (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 x -> fst x)) (fst es) f_ask, cg_val ctx
-  let paths_as_set ctx                            = liftmap (S.paths_as_set (conv ctx)) 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 x -> x)) (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 x -> x)) (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

tests/regression/80-context_gas/01-basic_tests_bound_sens.c

@@ -0,0 +1,16 @@
+// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 10
+// Basic examples
+
+int f(int x, int y)
+{
+    if (x == 0)
+    {
+        return y;
+    }
+    return f(x - 1, y - 1);
+}
+
+int main()
+{
+    __goblint_check(f(8, 8) == 0); // boundary (included)
+}

tests/regression/80-context_gas/02-basic_tests_bound_ins.c

@@ -0,0 +1,16 @@
+// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 10
+// Basic examples
+
+int f(int x, int y)
+{
+    if (x == 0)
+    {
+        return y;
+    }
+    return f(x - 1, y - 1);
+}
+
+int main()
+{
+    __goblint_check(f(9, 9) == 0); // UNKNOWN //boundary (excluded)
+}

tests/regression/80-context_gas/03-contextGas0.c

@@ -4,20 +4,12 @@ int f(int x, int y)
 {
     if (x == 0)
     {
-
         return y;
     }
-    return f(--x, --y);
+    return f(x - 1, y - 1);
 }
 
 int main()
 {
-    int y = f(0, 0);
-    __goblint_check(y == 0); // UNKNOWN
-
-    int y = f(5, 5);
-    __goblint_check(y == 0); // UNKNOWN
-
-    int y = f(1000, 1000);
-    __goblint_check(y == 0); // UNKNOWN
+    __goblint_check(f(1000, 1000) == 0); // UNKNOWN
 }

tests/regression/80-context_gas/04-contextGasNeg.c

@@ -4,20 +4,12 @@ int f(int x, int y)
 {
     if (x == 0)
     {
-
         return y;
     }
-    return f(--x, --y);
+    return f(x - 1, y - 1);
 }
 
 int main()
 {
-    int y = f(0, 0);
-    __goblint_check(y == 0); // UNKNOWN
-
-    int y = f(5, 5);
-    __goblint_check(y == 0); // UNKNOWN
-
-    int y = f(1000, 1000);
-    __goblint_check(y == 0); // UNKNOWN
+    __goblint_check(f(5, 5) == 0); // UNKNOWN
 }

tests/regression/80-context_gas/05-circle_call_sens.c

@@ -0,0 +1,44 @@
+// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 15
+// Checks if recursion in loops is handled properly
+#include <stdio.h>
+
+int f(int i);
+
+int g(int i)
+{
+    if (i == 0)
+    {
+        return 1;
+    }
+    if (i > 0)
+    {
+        return f(i + 1);
+    }
+    return 11;
+}
+
+int f(int i)
+{
+    if (i == 0)
+    {
+        return 2;
+    }
+    if (i > 0)
+    {
+        return g(i - 2) + g(i - 3);
+    }
+    return 12;
+}
+
+int main(void)
+{
+    __goblint_check(f(0) == 2);
+    __goblint_check(f(7) == 101);
+    __goblint_check(f(9) == 265);
+    __goblint_check(f(10) == 429);
+
+    __goblint_check(g(0) == 1);
+    __goblint_check(g(3) == 25);
+    __goblint_check(g(6) == 101);
+    __goblint_check(g(8) == 265);
+}