Widening gas

[Red-Panda64]

Description

This PR adds widening gas to the td3 solver. Widening gas permits an unknown to grow N times and still be combined with the regular join. Only once the unknown runs out of gas, the widening operator is used. Widening gas can be applied to regular unknowns and leaf unknowns.
Additionally, this PR extracts the side_widen strategies out of the main solve routine and wraps them in an interface.

Config Options

The gas budget for regular unknowns is controlled via solvers.td3.widen_gas, whereas leaves are controlled via solvers.td3.side_widen_gas. Both config options are 0 by default, effectively disabling the feature.
When widening points are configured to be reset with the solvers.td3.remove-wpoint option, this too resets that wpoints gas.

New side_widen Interface and Gas for Leaves

Widening gas co-exists with the other side-widening strategies.
Side widen strategies are meant to determine, when a leaf becomes a widening point. After a leaf has been selected as widening point, future updates to its value are applied with the widen operator. The widening gas can again be used to postpone this:
After a leaf has been marked as widening point, its gas counter is decreased for every increase to its value. Once it hits 0, widening is applied.

There is one exception, namely the side_widen strategy sides-local. It does not mark widening points, instead widening only if the incoming side-effect is larger than a previous side-effect that came from the same unknown. This has been adapted to work with widening gas like so: every time that the sides-local strategy would widen, the gas is decremented.

Functions of the new interface:

module type WPointSelect =
    sig
      type data

      (** Create data required by this widening point selection strategy.
          The parameters are not necessarily used by all strategies. 
      *)
      val create_data: (S.v -> bool) -> (S.v -> S.v -> unit) -> data
      (** Notifies this strategy that a side-effect has occured.
          This allows the strategy to adapt its internal data structure.
      *)
      val notify_side: data -> S.v option -> S.v -> unit
      (** Whether the destabilization of the side-effected var should record the destabilization
          of called variables and start variables. This information should be passed to [should_mark_wpoint].
      *)
      val record_destabilized_vs: bool
      (** This strategy can decide to prevent widening.
          Note that, if this strategy does not veto, this does not mean that widening
          will necessarily be performed. Nor does a call to this function imply that
          the value of the leaf has grown.
      *)
      val veto_widen: data -> unit HM.t -> VS.t -> S.v option -> S.v -> bool
      (** The value of the leaf has grown. Should it be marked a widening point?
          Even if this function is called, leaf y might already be a widening point
          from an earlier side-effect.
      *)
      val should_mark_wpoint: data -> unit HM.t -> VS.t -> S.v option -> S.v -> bool option -> bool
    end

Note that notify_side is needed for unstable-self, which records side-effects in the infl set. veto_widen is necessary to implement the above behavior for sides-local. record_destabilized_vs is currently only used by the cycle strategy. It indicates, whether the more expensive version of destabilize needs to be called, which also records whether a called or start variable was destabilized.

[sim642]

Why does this need to be inside the solver? This sounds like widening delay, which can be completely solver-independent and can be implemented simply as a lifting of a domain (overriding its widen).

[michael-schwarz]

@sim642 One could implement a similar feature as a domain lifter, yes. However, the effect would be subtly different: Here the delay (gas) is applied per unknown, whereas tracking it in the domain would mean that the gas value is propagated, e.g., between different loops, or that a complicated mechanism tracking not just one gas value but several inside a map would be required.
In the scope of this thesis, we investigate ideas for integrating a widening gas into the solver as a generalization of its automatic widening point detection which aims to be completely transparent to the writer of the analyses.
We are particularly interested in the values at globals here (but include it for locals for the sake of completeness). @Red-Panda64 will later on also implement a narrowing on globals in order to compare both approaches to having more precise globals.
The strategy of having delays tracked inside the domain is also interesting, and it may be worth comparing the impacts of both some time after the thesis is finished.

[sim642]

@sim642 One could implement a similar feature as a domain lifter, yes. However, the effect would be subtly different: Here the delay (gas) is applied per unknown, whereas tracking it in the domain would mean that the gas value is propagated, e.g., between different loops, or that a complicated mechanism tracking not just one gas value but several inside a map would be required.

I think the standard implementation is just domain lifting where transfer functions set the counter to 0, so none of such propagation occurs.

I'm again worried about the monolithic growth of the TD3 solver. For a long time we've wanted to undo that monolithic structure into a more modular one. While nobody has worked on decomposing the existing solver, at some point we decided to not worsen the problem and implement new things modularly. For example, DepVals is just a lifter for the solver and this could easily be as well.

[Red-Panda64]

This seems like a policy discussion, so I cannot really say much.
However, as @michael-schwarz said, the widening gas will probably mainly be meaningful for globals, so it's good to control the gas of globals and locals independently. This would be difficult to do when baking it not the domain, right?

[sim642]

However, as @michael-schwarz said, the widening gas will probably mainly be meaningful for globals, so it's good to control the gas of globals and locals independently. This would be difficult to do when baking it not the domain, right?

I think it would even be easier: one can choose whether to wrap an analysis's module D or/and module G with such a lifter. Either at a global level or even on a per-analysis level.

[sim642]

We discussed this during GobCon and here's the summary.

Currently, module type WPointSelect and all of its various implementations are somewhat deep in the Td3.Base module itself, but the logic that they implement is rather independent of the solver as a whole. They seem to be more-or-less functions on constraint system unknowns (S.v).
It would be good if they could be hoisted up (e.g. line 42 of td3.ml). It was pointed out that they still depend on S.v type and S.Var module for some operations, so they might need to be turned into functors with S.Var as the argument to make such hoisting possible. Hopefully this is then possible.

The change from wpoint: unit HM.t to wpoint_gas: int HM.t isn't much of a concern. Especially because unit HM.t stores unit values (basically ints 0) for values already, so this generalizes the data structure for all of the widenings but shouldn't incur any overhead to the cases when no gas is used.

Some small style improvements should also be done to make this merge-ready. It was mentioned that there are some parentheses which are unneeded (e.g. around if .. then conditions).

[Red-Panda64]

I have extracted the modules out of td3.Base. For now, I have placed them in their own module in src/solver. Since this directory so far only contains solver implementations, I am not sure if it is a good place for them. However, I cannot really see any other place they would belong, because they exclusively affect the solving algorithm. Any opinions on this?

but the logic that they implement is rather independent of the solver as a whole.

So far, no other solver implements these strategies, so I have left the selection of the concrete implementation in td3. In their current form, I would not say that the strategies are really independent from td3. Some of the functions/strategies need td3-specific details, like an add_infl function, or data structures like the stable and called sets. I think it would be preferable to have them out of the td3.Base module but inside td3.

[sim642]

What is this comment about?

[Red-Panda64]

My comment is strangely worded, but I think it is odd that should_widen or previously HM.mem wpoint x is re-evaluated here.
Specifically, let wp = should_widen x before evaluating eq is used to determine, whether widening should be applied. The result of should_widen may have changed through eq, yet I would assume the value that is logged should reflect the value that is used for the actual widening decision.

But if using the updated value, I should be logging with format_wpoint, which will not only show whether x is a wpoint, but also how much gas it has.

[sim642]

Is it right to swap HM.mem wpoint for should_widen here?
This case is taken when in the widening phase the value has stabilized and thus should be switched to narrowing.
If I understand correctly, this now means that if all the widening has isn't used up at x (because should_widen requires it to be 0), then the solver doesn't switch to narrowing at all.

Previously the notions of "widening point" and "should apply widening now" more-or-less coincided, but with gas they no longer do. I think places like this that check HM.mem wpoint but don't actually call widen based on that should still check for "widening point", not "should apply widening now".

[Red-Panda64]

I think it should be appropriate to use should_widen here. If x is a widening point with gas, that means it was never widened. If it was not widened, then narrowing would be pointless.

On the other hand, using HM.mem wpoint would also not be harmful either, nor would narrowing cause a large overhead if x does not change. I can change it to a membership check, if you prefer

[Red-Panda64]

Ah, I guess you are right, narrowing could still have an effect due to some non-monotonicity.

[sim642]

Same HM.mem wpoint thing here. This seems to be just starting a new widening phase.

[sim642]

This leq check is not present in SidesLocal.veto_widen.

[Red-Panda64]

That is true, but if b is less or equal to a, widening should have no effect, right?

[sim642]

I have extracted the modules out of td3.Base. For now, I have placed them in their own module in src/solver. Since this directory so far only contains solver implementations, I am not sure if it is a good place for them. However, I cannot really see any other place they would belong, because they exclusively affect the solving algorithm. Any opinions on this?

It would've been fine to leave them in td3.ml, but a separate file might even be better. That directory already has other solver-specific helper modules anyway (e.g. SolverBox).