Legend:
Library
Module
Module type
Parameter
Class
Class type
Effect 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:
coeffects - a value of an expression depends on the outside world, that is further subdivided by the read effect, when an expression reads a CPU register, and the load effect, when an expression an expression accesses the memory.
effects - a value modifies the state of the world, by either storing a value in the memory, or by raising a CPU exception via the division by zero or accessing the memory.
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;
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 arithmetics 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.