Std.EffEffect analysis.
Effect analysis describes how an expression computation interacts with the outside world. By the outside world we understand the whole of the CPU state (including the hidden state) and the memory. We distinguish, so far, between the following sorts of effects:
An expression that doesn't have effects or coeffects is idempotent and can be moved arbitrary in a tree, removed or substituted. An expression that has only coeffects is generative and can be reproduced without a significant change of semantics.
Examples:
x ^ x, x+1, x - have coeffects;x[y] - has both effects (may raise pagefault) and coeffects;7 * 8, 42 - have no effects.val none : tan expression doesn't have any effects
val read : tan expression reads a register (nonvirtual) variable.
val load : tan expression loads a value from a memory
val store : tan expression stores a value in a memory
val raise : tan expression raises a CPU exception
val reads : t -> boolreads eff if read in eff
val loads : t -> boolloads eff if load in eff
val stores : t -> boolstores eff if load in eff
val raises : t -> boolraises eff if raise in eff
val has_effects : t -> boolhas_effects eff if stores eff || raises eff
val has_coeffects : t -> boolhas_coeffects eff if loads eff || reads eff
compute x computes a set of effects produced by x. The result is a sound overapproximation of the real effects, i.e., if an effect is computed then it may really happen, but if it is not computed, then it is proved that it is not possible for the expression to have this effect.
The analysis applies a simple abstract interpretation to approximate arithmetic and prove an absence of the division by zero. The load/store/read analysis is more precise than the division by zero, as the only source of the imprecision is a presence of conditional expressions.
Requires: normalized and simplified expression.
Warning: the above should be either relaxed or expressed in the type system.