Effect.Sort
Effect sorts.
The sort of an effect holds static information that is common to all effects of that sort.
We distinguish two kinds of effects - ctrl
effects that affect which instructions will be executed next and data
effects that affect only the values in the computer storage.
The unit
effect represents an effect that is a mixture of ctrl
and data
effects.
type +'a t = 'a sort
val top : unit t
top
is a set of all possible effects.
This sort indicates that the statement can have any effect.
val bot : 'a t
bot
is an empty set of effects.
This sort indicates that the statement doesn't have any observable effects, thus it could be coerced to any other sort.
val order : 'a t -> 'b t -> KB.Order.partial
order xs ys
orders effects by the order of inclusion.
xs
is before ys
if ys
includes all effects of xs
, otherwise.