Arrays Bounds Check Elimination (ABC)
			 in the Mono Runtime

	       Massimiliano Mantione (mass@ximian.com)

Here "abc" stays for "array bounds check", or "array bound checks", or
some combination of the two.

* Usage

	Simply use the "abcrem" optimization invoking mono.

	To see if bound checks are actually removed, use "mono -v" and
	grep for "ARRAY-ACCESS" in the output, there should be a
	message for each check that has been removed.
	
	To trace the algorithm execution, use "-v -v -v", and be
	prepared to be totally submersed by debugging messages...

* Effectiveness

	The abc removal code can now always remove bound checks from
	"clean" array scans in loops, and generally anyway there are
	clear conditions that already state that the index is "safe".
	
	To be clearer, and give an idea of what the algorithm can and
	cannot do without describing it in detail... keep in mind that
	only "redunant" checks cannot be removed. By "redundant", I
	mean "already explicitly checked" in the method code.
	
	Unfortunately, analyzing complex expressions is not so easy
	(see below for details), so the capabilities of this "abc
	remover" are limited.
	
	These are simple guidelines:

	- Only expressions of the following kinds are handled:
	  - constant
	  - variable [+/- constant]
	- Only comparisons between "handled" expressions are understood.
	- "switch" statements are not yet handled.
	
	This means that code like this will be handled well:
	
		for (int i = 0; i < a.Length; i++) {
			a [i] = .....
		}
		
	The "i" variable could be declared out of the "for", the "for"
	could be a "while", and maybe even implemented with "goto",
	the array could be scanned in reverse order, and everything
	would still work.

	I could have a temporary variable storing the array length,
	and check on it inside the loop, and the abc removal would
	still occurr, like this:
	
		int i = 0;
		int l = a.Length;
		while ( i < l ) {
			a [i] ......
		}
		
	or this:
	
		int l = a.Length;
		for (int i = l; i > 0; i--) {
			a [i] = .....
		}
		
	The following two examples would work:
	
		for (int i = 0; i < (a.Length -1); i++) .....
		for (int i = 0; i < a.Length; i += 2) .....
		
	But just something like this
	
		int delta = -1;
		for (int i = 0; i < (a.Length + delta); i++) .....
		
	or like this
	
		int delta = +2;
		for (int i = 0; i < a.Length; i += delta) .....
		
	would not work, the check would stay there. (unless
	a combination of cfold, consprop and copyprop is used, too,
	which would make the constant value of "delta" explicit).
	
	Just to make you understand how things are tricky... this would work!
	
		int limit = a.Length - 1;
		for (int i = 0; i < limit; i++) {
			a [i] = .....
		}
		
	A detailed explanation of the reason why things are done like
	this is given below.
	
* The Algorithm

	This array bound check removal (abc removal) algorithm is
	based on symbolic execution concepts. I handle the removal
	like an "unreachable code elimination" (and in fact the
	optimization could be extended to remove also other
	unreachable sections of code, due to branches that "always go
	the same way").
	
	In symbolic execution, variables do not have actual (numeric)
	values, but instead symbolic expressions (like "a", or "x+y").
	Also, branch conditions are handled like symbolic conditions
	(like "i<k"), which state relations between variable values.
	
	The SSA representation inside mini is somewhat close to a
	symbolic representation of the execution of the compiled
	method.
	
	Particularly, the representation of variable values is exactly
	a symbolic one. It is enough to find all CEE_STIND_*
	instructions which store to a local variable, and their second
	argument is exactly the variable value.  Actually, "cfg->vars
	[<variable-index>]->def" should contain exactly those store
	instructions, and the "get_variable_value_from_ssa_store"
	function extracts the variable value from there.
	
	On the other hand, the conditions under which each basic block
	is executed are not made fully explicit.
	
	However, it is not difficult to make them so.

	Each BB that has more than one exit BB, in practice must end
	either with a conditional branch instruction or with a switch
	instruction.
	
	In the first case, the BB has exactly two exit BBs, and their
	execution conditions are easy to get from the condition of the
	branch (see the "get_relation_from_branch_instruction"
	function, and expecially the end of "analyze_block" in
	abcremoval.c.

	If there is a switch, the jump condition of every exit BB is
	the equality of the switch argument with the particular index
	associated with its case (but the current implementation does
	not handle switch statements yet).
	
	These individual conditions are in practice associated to each
	arc that connects BBs in the CFG (with the simple case that
	unconditional branches have a "TRUE" condition, because they
	always happen).
	
	So, for each BB, its *proper* entry condition is the union of
	all the conditions associated to arcs that enter the BB. The
	"union" is like a logical "or", in the sense that either of
	the condition could be true, they are not necessarily all
	true. This means that if I can enter a BB in two ways, and in
	one case I know that "x>0", and in the other that "x==0",
	actually in the BB I know that "x>=0", which is a weaker
	condition (the union of the two).
	
	Also, the *complete* entry condition for a BB is the
	"intersection" of all the entry conditions of its
	dominators. This is true because each dominator is the only
	way to reach the BB, so the entry condition of each dominator
	must be true if the control flow reached the BB. This
	translates to the logical "and" of all the "proper" conditions
	of the BBs met walking up in the dominator tree. So, if one
	says "x>0", and another "x==1", then I know that "x==1", which
	is a stronger condition (the intersection of the two).

	Note that, if the two conditions were "x>0" and "x==0", then
	the block would be unreachable (the intersection is empty),
	because some branch is impossible.
	
	Another observation is that, inside each BB, every variable is
	subject to the complete entry condition of that very same BB,
	and not the one in which it is defined (with the "complete
	entry condition" being the thing I defined before, sorry if
	these terms "proper" and "complete" are strange, I found
	nothing better).

	This happens because the branch conditions are related to the
	control flow.  I can define "i=a", and if I am in a BB where
	"a>0", then "i>0", but not otherwise.
	
	So, intuitively, if the available conditions say "i>=0", and i
	is used as an index in an array access, then the lower bound
	check can be omitted.  If the condition also says
	"(i>=0)&&(i<array.length)", the abc removal can occur.
	
	So, a complete solution to the problem of abc removal would be
	the following: for each array access, build a system of
	equations containing:

		[1] all the symbolic variable definitions
	
		[2] the complete entry condition of the BB in which
		the array access occurs
		
		[3] the two "goal functions" ("index >=0" and "index <
		array.length")
		
	If the system is valid for *each possible* variable value, then the goal
	functions are always true, and the abc can be removed.
	
	All this discussion is useful to give a precise specification
	to the problem we are trying to solve.

	The trouble is that, in the general case, the resulting system
	of equations is like a predicate in first order logic, which
	is semi-decidable, and its general solution is anyway too
	complex to be attempted in a JIT compiler (which should not
	contain a full fledged theorem prover).
	
	Therefore, we must cut some corner.
	
	There is also another big problem, which is caused by
	"recursive" symbolic definitions. These definition can (and
	generally do) happen every time there is a loop. For instance,
	in the following piece of code:
	
		for ( int i = 0; i < array.length; i++ ) {
			Console.WriteLine( "array [i] = " + array [i] );
		}
		
	one of the definitions of i is a PHI that can be either 0 or
	"i + 1".
	
	Now, we know that mathematically "i = i + 1" does not make
	sense, and in fact symbolic values are not "equations", they
	are "symbolic definitions".
	
	The actual symbolic value of i is a generic "n", where "n" is
	the number of iterations of the loop, but this is terrible to
	handle (and in more complex examples the symbolic value of i
	simply cannot be written, because i is calculated in an
	iterative way).
	
	However, the definition "i = i + 1" tells us something about
	i: it tells us that i "grows". So (from the PHI definition) we
	know that i is either 0, or "grows". This is enough to tell
	that "i>=0", which is what we want!  It is important to note
	that recursive definitions can only occurr inside PHI
	definitions, because actually a variable cannot be defined
	*only* in terms of itself!
	
	At this point, I can explain which corners I want to cut to
	make the problem solvable. It will not remove all the abc that
	could theoretically be removed, but at least it will work.
	
	The easiest way to cut corners is to only handle expressions
	which are "reasonably simple", and ignore the rest.

	Keep in mind that ignoring an expression is not harmful in
	itself.  The algorithm will be simply "less powerful", because
	it will ignore conditions that could have caused to the
	removal of an abc, but will not remove checks "by mistake" (so
	the resulting code will be in any case correct).
	
	The expressions we handle are the following (all of integer
	type):

		- constant
		- variable
		- variable + constant
		- constant + variable
		- variable - constant
		
	And, of course, PHI definitions.

	Any other expression causes the introduction of an "any" value
	in the evaluation, which makes all values that depend from it
	unknown as well.
	
	We will call these kind of definitions "summarizable"
	definitions.
	
	In a first attempt, we can consider only branch conditions
	that have the simplest possible form (the comparison of two
	summarizable expressions).
	
	We can also simplify the effect of variable definitions,
	keeping only what is relevant to know: their value range with
	respect to zero and with respect to the length of the array we
	are currently handling.
	
	One particular note on PHI functions: they work (obviously)
	like the logical "or" of their definitions, and therefore are
	equivalent to the "logical or" of the summarization of their
	definitions.
	
	About recursive definitions (which, believe me, are the worst
	thing in all this mess), we handle only "monotonic" ones. That
	is, we try to understand if the recursive definition (which,
	as we said above, must happen because of a loop) always
	"grows" or "gets smaller". In all other cases, we decide we
	cannot handle it.
	
	One critical thing, once we have defined all these data
	structures, is how the evaluation is actually performed.
	
	In a first attempt I coded a "brute force" approach, which for
	each BB tried to examine all possible conditions between all
	variables, filling a sort of "evaluation matrix". The problem
	was that the complexity of this evaluation was quadratic (or
	worse) on the number of variables, and that many wariables
	were examined even if they were not involved in any array
	access.
	
	Following the ABCD paper:

		  http://citeseer.ist.psu.edu/bodik00abcd.html

	I rewrote the algorithm in a more "sparse" way.

	Now, the main data structure is a graph of relations between
	variables, and each attempt to remove a check performs a
	traversal of the graph, looking for a path from the index to
	the array length that satisfies the properties "index >= 0"
	and "index < length". If such a path is found, the check is
	removed. It is true that in theory *each* traversal has a
	complexity which is exponential on the number of variables,
	but in practice the graph is not very connected, so the
	traversal terminates quickly.
	
	
	Then, the algorithm to optimize one method looks like this:

		[1] Preparation:

		    [1a] Build the SSA representation.

		    [1b] Prepare the evaluation graph (empty)

		    [1b] Summarize each varible definition, and put
		         the resulting relations in the evaluation
		         graph

		[2] Analyze each BB, starting from the entry point and
		    following the dominator tree:

		    [2a] Summarize its entry condition, and put the resulting relations
		         in the evaluation graph (this is the reason
			 why the BBs are examined following the
			 dominator tree, so that conditions are added
			 to the graph in a "cumulative" way)

		    [2b] Scan the BB instructions, and for each array
			 access perform step [3]

		    [2c] Process children BBs following the dominator
			 tree (step [2])

		    [2d] Remove from the evaluation area the conditions added at step [2a]
		         (so that backtracking along the tree the area
			 is properly cleared)

		[3] Attempt the removal:

		    [3a] Summarize the index expression, to see if we can handle it; there
		         are three cases: the index is either a
			 constant, or a variable (with an optional
			 delta) or cannot be handled (is a "any")

		    [3b] If the index can be handled, traverse the evaluation area searching
		         a path from the index variable to the array
			 length (if the index is a constant, just
			 examine the array length to see if it has
			 some relation with this constant)

		    [3c] Use the results of step [3b] to decide if the check is redundant