fix side_wide_gas off by one and gas with sides-local

src/solver/td3.ml

@@ -468,9 +468,6 @@ module Base =
           if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %s) from %a: %a -> %a" S.Var.pretty_trace y (format_wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty old S.Dom.pretty tmp;
           if tracing && not (S.Dom.is_bot old) then trace "solchange" "side to %a (wpx: %s) from %a: %a" S.Var.pretty_trace y (format_wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty_diff (tmp, old);
 
-          (* y has grown. Reduce widening gas! *)
-          reduce_gas y;
-
           let sided = match x with
             | Some x ->
               let sided = VS.mem x old_sides in
@@ -488,13 +485,13 @@ module Base =
               mark_wpoint y default_side_widen_gas
             )
           in
-          match side_widen with
+          (match side_widen with
           | "always" -> (* Any side-effect after the first one will be widened which will unnecessarily lose precision. *)
             wpoint_if true
           | "never" -> (* On side-effect cycles, this should terminate via the outer `solver` loop. TODO check. *)
             ()
-          | "sides-local" -> (* Never make globals widening points in this strategy, the widening check happens by checking sides *)
-            ()
+          | "sides-local" -> (* Always mark wpoint: sides-local will veto widening, if there have been no previous side-effects from this unknown *)
+            wpoint_if true
           | "sides" ->
             (* if there already was a `side x y d` that changed rho[y] and now again, we make y a wpoint *)
             (* x caused more than one update to y. >=3 partial context calls will be precise since sides come from different x. TODO this has 8 instead of 5 phases of `solver` for side_cycle.c *)
@@ -516,7 +513,10 @@ module Base =
             wpoint_if @@ not (HM.mem stable y)
           | "unstable_called" -> (* TODO test/remove. Widen if any called var (not just y) is no longer stable. Expensive! *)
             wpoint_if @@ exists_key (neg (HM.mem stable)) called (* this is very expensive since it folds over called! see https://github.com/goblint/analyzer/issues/265#issuecomment-880748636 *)
-          | x -> failwith ("Unknown value '" ^ x ^ "' for option solvers.td3.side_widen!")
+          | x -> failwith ("Unknown value '" ^ x ^ "' for option solvers.td3.side_widen!"));
+
+          (* y has grown. Reduce widening gas! *)
+          reduce_gas y;
         )
       and init x =
         if tracing then trace "sol2" "init %a" S.Var.pretty_trace x;

tests/regression/81-widening_gas/01-side_widen_gas.c

@@ -1,9 +1,6 @@
-// PARAM: --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 3 --enable ana.int.interval
+// PARAM: --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 4 --enable ana.int.interval
 #include <pthread.h>
 #include <goblint.h>
-/* side_widen_gas of 3 effectively means that an unknown may increase 4 times:
- * once to identify the global as a widening point, which initializes the gas to 3,
- * and then three more times, using up the gas. */
 
 int a = 0;
 int b = 0;

tests/regression/81-widening_gas/01-side_widen_gas.t

@@ -1,4 +1,8 @@
-  $ goblint --trace gas --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 3 --enable ana.int.interval 01-side_widen_gas.c 2> tmp > /dev/null
+Problem: this only works when goblint is built with tracing enabled...
+Should this kind of test on trace data even exist?
+  $ goblint --trace gas --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 4 --enable ana.int.interval 01-side_widen_gas.c 2> tmp > /dev/null
+  $ grep -E 'reducing gas.*:(a|b|c):.*4 -> 3$' tmp | wc -l
+  6
   $ grep -E 'reducing gas.*:(a|b|c):.*3 -> 2$' tmp | wc -l
   6
   $ grep -E 'reducing gas.*:(a|b|c):.*2 -> 1$' tmp | wc -l