Open Red-Panda64 opened 5 months ago
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
).
@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 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.
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?
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.
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 int
s 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).
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.
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
).
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 viasolvers.td3.side_widen_gas
. Both config options are 0 by default, effectively disabling the feature. When widening points are configured to be reset with thesolvers.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 thesides-local
strategy would widen, the gas is decremented.Functions of the new interface:
Note that
notify_side
is needed forunstable-self
, which records side-effects in theinfl
set.veto_widen
is necessary to implement the above behavior forsides-local
.record_destabilized_vs
is currently only used by thecycle
strategy. It indicates, whether the more expensive version ofdestabilize
needs to be called, which also records whether a called or start variable was destabilized.