Module SideWPointSelect.UnstableCalled

Widen if any called var (not just y) is no longer stable. Expensive!

Parameters

module HM : Batteries.Hashtbl.S with type key = S.v
module VS : Batteries.Set.S with type elt = S.v

Signature

type data
val create_data : (S.v -> bool) -> (S.v -> S.v -> unit) -> data

Create data required by this widening point selection strategy. The parameters are not necessarily used by all strategies.

  • parameter is_stable

    This callback should return whether an unknown is stable.

  • parameter add_infl

    Allows the strategy to record additional influences. This is mainly intended for strategies like unstable-self, which records the influence of a side-effecting unknown x to the leaf y.

val notify_side : data -> S.v option -> S.v -> unit

Notifies this strategy that a side-effect has occured. This allows the strategy to adapt its internal data structure.

  • parameter data

    The internal state of this strategy

  • parameter x

    The optional source of the side-effect

  • parameter y

    The leaf receiving the side-effect

val record_destabilized_vs : bool

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 by the solver.

val veto_widen : data -> unit HM.t -> VS.t -> S.v option -> S.v -> 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.

  • parameter data

    The internal state of this strategy

  • parameter called

    Set of called unknowns

  • parameter old_sides

    Prior side-effects to leaf y

  • parameter x

    Optional source of the side-effect

  • parameter y

    Side-effected leaf y

  • returns

    true: widening will not be applied; false: widening might be applied

val should_mark_wpoint : data -> unit HM.t -> VS.t -> S.v option -> S.v -> bool option -> bool

The value of the leaf has grown. Should it be marked a widening point? Widening points are widened when their value grows, unless vetoed. Even if this function is called, leaf y might already be a widening point from an earlier side-effect.

  • parameter data

    The internal state of this strategy

  • parameter called

    Set of called unknowns

  • parameter old_sides

    Prior side-effects to leaf y

  • parameter x

    Optional source of the side-effect

  • parameter y

    Side-effected leaf y

  • parameter destabilized_vs

    Optional destabilization info, described in record_destabilized_vs

  • returns

    true: mark as widening point; false: do not mark as widening point