2008-08-11 Zoltan Varga <vargaz@gmail.com>
[mono.git] / mono / mini / abcremoval.c
index 5eee046b8339507d50971f0b5f74302a6d3857bd..8331ce84fbe92dedc24e51da4ecf09ed97313fbb 100644 (file)
 #include <mono/metadata/mempool.h>
 #include <mono/metadata/opcodes.h>
 
-#include "mini.h"
+#include "config.h"
+
+#ifndef DISABLE_SSA
+
 #include "inssel.h"
 
 #include "abcremoval.h"
 
-extern guint8 mono_burg_arity [];
+#if SIZEOF_VOID_P == 8
+#define OP_PCONST OP_I8CONST
+#else
+#define OP_PCONST OP_ICONST
+#endif
+
 
 #define TRACE_ABC_REMOVAL (verbose_level > 2)
 #define REPORT_ABC_REMOVAL (verbose_level > 0)
 
-#define CHEAT_AND_REMOVE_ALL_CHECKS 0
-
+/*
+ * A little hack for the verbosity level.
+ * The verbosity level is stored in the cfg, but not all functions that must
+ * print something see the cfg, so we store the verbosity level here at the
+ * beginning of the algorithm.
+ * This is not thread safe (does not handle correctly different verbosity
+ * levels in different threads), and is not exact in case of dynamic changes
+ * of the verbosity level...
+ * Anyway, this is not needed, all that can happen is that something more
+ * (or less) is logged, the result is in any case correct.
+ */
 static int verbose_level;
 
-#if (!CHEAT_AND_REMOVE_ALL_CHECKS)
-
-
-#define IS_SUMMARIZED_VALUE_CONSTANT(value) ((value).value_type==MONO_CONSTANT_SUMMARIZED_VALUE)
-#define IS_SUMMARIZED_VALUE_VARIABLE(value) ((value).value_type==MONO_VARIABLE_SUMMARIZED_VALUE)
 
 #define RELATION_BETWEEN_VALUES(value,related_value) (\
        ((value) > (related_value))? MONO_GT_RELATION :\
        (((value) < (related_value))? MONO_LT_RELATION : MONO_EQ_RELATION))
 
 #define MAKE_VALUE_ANY(v) do{\
-               (v)->relation_with_zero = MONO_ANY_RELATION;\
-               (v)->relation_with_one = MONO_ANY_RELATION;\
-               (v)->relation_with_value = MONO_ANY_RELATION;\
-               (v)->value_type = MONO_CONSTANT_SUMMARIZED_VALUE;\
-               (v)->value.constant = 0;\
+               (v).type = MONO_ANY_SUMMARIZED_VALUE;\
+       } while (0)
+
+#define MAKE_VALUE_RELATION_ANY(r) do{\
+               (r)->relation = MONO_ANY_RELATION;\
+               MAKE_VALUE_ANY((r)->related_value);\
+       } while (0)
+
+#define INITIALIZE_VALUE_RELATION(r) do{\
+               MAKE_VALUE_RELATION_ANY((r));\
+               (r)->next = NULL;\
        } while (0)
 
 #define MONO_NEGATED_RELATION(r) ((~(r))&MONO_ANY_RELATION)
 #define MONO_SYMMETRIC_RELATION(r) (((r)&MONO_EQ_RELATION)|(((r)&MONO_LT_RELATION)<<1)|((r&MONO_GT_RELATION)>>1))
 
-#define RELATION_ADDS_INFORMATION(r,r_maybe_adds_information) ((r)&(~(r_maybe_adds_information)))
-
-unsigned char propagated_relations_table [] = {
-       #include "propagated_relations_table.def"
-       MONO_ANY_RELATION
-};
-#define PROPAGATED_RELATION(r,r_to_propagate) (propagated_relations_table [((r)<<3)|(r_to_propagate)])
 
 
 static void
@@ -84,147 +95,137 @@ print_relation (int relation) {
 
 static void
 print_summarized_value (MonoSummarizedValue *value) {
-       printf ("relation_with_zero: ");
-       print_relation (value->relation_with_zero);
-       printf ("\n");
-       printf ("relation_with_one: ");
-       print_relation (value->relation_with_one);
-       printf ("\n");
-       printf ("relation_with_value: ");
-       print_relation (value->relation_with_value);
-       printf ("\n");
-       switch (value->value_type) {
+       switch (value->type) {
+       case MONO_ANY_SUMMARIZED_VALUE:
+               printf ("ANY");
+               break;
        case MONO_CONSTANT_SUMMARIZED_VALUE:
-               printf ("Constant value: %d\n", value->value.constant);
+               printf ("CONSTANT %d", value->value.constant.value);
                break;
        case MONO_VARIABLE_SUMMARIZED_VALUE:
-               printf ("Variable value: %d\n", value->value.variable);
+               printf ("VARIABLE %d, delta %d", value->value.variable.variable, value->value.variable.delta);
                break;
        case MONO_PHI_SUMMARIZED_VALUE: {
-               int i;
-               printf ("PHI value: (");
-               for (i = 0; i < *(value->value.phi_variables); i++) {
-                       if (i) printf (",");
-                       printf ("%d", *(value->value.phi_variables + i + 1));
+               int phi;
+               printf ("PHI (");
+               for (phi = 0; phi < value->value.phi.number_of_alternatives; phi++) {
+                       if (phi) printf (",");
+                       printf ("%d", value->value.phi.phi_alternatives [phi]);
                }
-               printf (")\n");
+               printf (")");
                break;
        }
        default:
-               printf ("Unknown value type: %d\n", value->value_type);
+               g_assert_not_reached ();
        }
 }
 
 static void
-print_branch_condition (MonoBranchCondition *condition, int n) {
-       printf ("Branch condition %d, on variable %d\n", n, condition->variable);
-       print_summarized_value (&(condition->value));
+print_summarized_value_relation (MonoSummarizedValueRelation *relation) {
+       printf ("Relation ");
+       print_relation (relation->relation);
+       printf (" with value ");
+       print_summarized_value (&(relation->related_value));
 }
 
+#if 0
 static void
-print_branch_data (MonoBranchData *branch, int n) {
-       int i;
-       printf ("Branch %d, destination BB %d [dfn %d], conditions %d\n",
-               n, branch->destination_block->block_num, branch->destination_block->dfn, branch->number_of_conditions);
-       for (i = 0; i < branch->number_of_conditions; i++) {
-               print_branch_condition (&(branch->conditions [i]), i);
-       }
-}
-
-static void
-print_summarized_block (MonoSummarizedBasicBlock *block) {
-       int i;
-       printf ("Summarization of BB %d [dfn %d] (has array accesses: %d), branches: %d\n",
-               block->block->block_num, block->block->dfn, block->has_array_access_instructions, block->number_of_branches);
-       for (i = 0; i < block->number_of_branches; i++) {
-               print_branch_data (&(block->branches [i]), i);
+print_summarized_value_relation_chain (MonoSummarizedValueRelation *relation) {
+       printf ("Relations:\n");
+       while (relation) {
+               print_summarized_value_relation (relation);
+               printf ("\n");
+               relation = relation->next;
        }
 }
+#endif
 
 static void
-print_variable_relations (MonoVariableRelations *relations, gssize variable, int n) {
-       int i;
-       int significantRelations = 0;
-       for (i = 0; i < n; i++) {
-               if (relations->relations_with_variables [i] != MONO_ANY_RELATION) {
-                       significantRelations++;
+print_evaluation_context_status (MonoRelationsEvaluationStatus status) {
+       if (status == MONO_RELATIONS_EVALUATION_NOT_STARTED) {
+               printf ("EVALUATION_NOT_STARTED");
+       } else {
+               gboolean print_or = FALSE;
+               
+               printf ("(");
+               if (status & MONO_RELATIONS_EVALUATION_IN_PROGRESS) {
+                       if (print_or) printf ("|");
+                       printf ("EVALUATION_IN_PROGRESS");
+                       print_or = TRUE;
                }
-       }
-       if ((relations->relation_with_zero != MONO_ANY_RELATION) ||
-                       (relations->relation_with_one != MONO_ANY_RELATION) ||
-                       (significantRelations > 0)) {
-               printf ("Relations for variable %d:\n", variable);
-               if (relations->relation_with_zero != MONO_ANY_RELATION) {
-                       printf ("relation_with_zero: ");
-                       print_relation (relations->relation_with_zero);
-                       printf ("\n");
+               if (status & MONO_RELATIONS_EVALUATION_COMPLETED) {
+                       if (print_or) printf ("|");
+                       printf ("EVALUATION_COMPLETED");
+                       print_or = TRUE;
                }
-               if (relations->relation_with_one != MONO_ANY_RELATION) {
-                       printf ("relation_with_one: ");
-                       print_relation (relations->relation_with_one);
-                       printf ("\n");
+               if (status & MONO_RELATIONS_EVALUATION_IS_RECURSIVELY_ASCENDING) {
+                       if (print_or) printf ("|");
+                       printf ("RECURSIVELY_ASCENDING");
+                       print_or = TRUE;
                }
-               if (significantRelations > 0) {
-                       printf ("relations_with_variables (%d significant)\n", significantRelations);
-                       for (i = 0; i < n; i++) {
-                               if (relations->relations_with_variables [i] != MONO_ANY_RELATION) {
-                                       printf ("relation with variable %d: ", i);
-                                       print_relation (relations->relations_with_variables [i]);
-                                       printf ("\n");
-                               }
-                       }
+               if (status & MONO_RELATIONS_EVALUATION_IS_RECURSIVELY_DESCENDING) {
+                       if (print_or) printf ("|");
+                       printf ("RECURSIVELY_DESCENDING");
+                       print_or = TRUE;
                }
+               if (status & MONO_RELATIONS_EVALUATION_IS_RECURSIVELY_INDEFINITE) {
+                       if (print_or) printf ("|");
+                       printf ("RECURSIVELY_INDEFINITE");
+                       print_or = TRUE;
+               }
+               printf (")");
        }
 }
 
+
 static void
-print_all_variable_relations (MonoVariableRelationsEvaluationArea *evaluation_area) {
-       int i;
-       printf ("relations in evaluation area:\n");
-       for (i = 0; i < evaluation_area->cfg->num_varinfo; i++) {
-               print_variable_relations (&(evaluation_area->variable_relations [i]), i, evaluation_area->cfg->num_varinfo);
+print_evaluation_context_ranges (MonoRelationsEvaluationRanges *ranges) {
+       printf ("(ranges: zero [%d,%d], variable [%d,%d])", ranges->zero.lower, ranges->zero.upper, ranges->variable.lower, ranges->variable.upper);
+}
+
+static void
+print_evaluation_context (MonoRelationsEvaluationContext *context) {
+       printf ("Context status: ");
+       print_evaluation_context_status (context->status);
+       if (context->status & (MONO_RELATIONS_EVALUATION_IN_PROGRESS|MONO_RELATIONS_EVALUATION_COMPLETED)) {
+               print_evaluation_context_ranges (&(context->ranges));
        }
+       printf ("\n");
 }
 
+#if 0
+static void
+print_evaluation_area (MonoVariableRelationsEvaluationArea *area) {
+       int i;
+       printf ("Dump of evaluation area (%d variables):\n", area->cfg->num_varinfo);
+       for (i = 0; i < area->cfg->num_varinfo; i++) {
+               printf ("Variable %d: ", i);
+               print_evaluation_context (&(area->contexts [i]));
+               print_summarized_value_relation_chain (&(area->relations [i]));
+       }
+}
 
-static MonoValueRelation
-relation_for_sum_of_variable_and_constant (
-               MonoValueRelation variable_relation, MonoValueRelation constant_relation_with_zero) {
-       switch (variable_relation) {
-       case MONO_EQ_RELATION:
-               return constant_relation_with_zero;
-       case MONO_GE_RELATION:
-               if (constant_relation_with_zero & MONO_LT_RELATION) {
-                       return MONO_ANY_RELATION;
-               } else {
-                       return constant_relation_with_zero;
-               }
-       case MONO_LE_RELATION:
-               if (constant_relation_with_zero & MONO_GT_RELATION) {
-                       return MONO_ANY_RELATION;
-               } else {
-                       return constant_relation_with_zero;
-               }
-       case MONO_GT_RELATION:
-               if (constant_relation_with_zero & MONO_LT_RELATION) {
-                       return MONO_ANY_RELATION;
-               } else {
-                       return MONO_GT_RELATION;
-               }
-       case MONO_LT_RELATION:
-               if (constant_relation_with_zero & MONO_GT_RELATION) {
-                       return MONO_ANY_RELATION;
-               } else {
-                       return MONO_LE_RELATION;
-               }
-       default:
-               g_assert_not_reached ();
-               return MONO_ANY_RELATION;
+static void
+print_evaluation_area_contexts (MonoVariableRelationsEvaluationArea *area) {
+       int i;
+       printf ("Dump of evaluation area contexts (%d variables):\n", area->cfg->num_varinfo);
+       for (i = 0; i < area->cfg->num_varinfo; i++) {
+               printf ("Variable %d: ", i);
+               print_evaluation_context (&(area->contexts [i]));
        }
 }
+#endif
 
+/*
+ * Given a MonoInst, if it is a store to a variable return the MonoInst that
+ * represents the stored value.
+ * If anything goes wrong, return NULL.
+ * store: the MonoInst that should be a store
+ * expected_variable_index: the variable where the value should be stored
+ * return: either the stored value, or NULL
+ */
 static MonoInst *
-get_variable_value_from_ssa_store (MonoInst *store, int expected_variable_index) {
+get_variable_value_from_store_instruction (MonoInst *store, int expected_variable_index) {
        switch (store->opcode) {
        case CEE_STIND_REF:
        case CEE_STIND_I:
@@ -235,12 +236,12 @@ get_variable_value_from_ssa_store (MonoInst *store, int expected_variable_index)
        case CEE_STIND_R4:
        case CEE_STIND_R8:
                if (TRACE_ABC_REMOVAL) {
-                       printf ("Store instruction found...\n");
+                       printf ("[store instruction found]");
                }
-               if (store->inst_left->opcode == OP_LOCAL) {
+               if ((store->inst_left->opcode == OP_LOCAL) || (store->inst_left->opcode == OP_ARG)) {
                        int variable_index = store->inst_left->inst_c0;
                        if (TRACE_ABC_REMOVAL) {
-                               printf ("Value put in local %d (expected %d)\n", variable_index, expected_variable_index);
+                               printf ("[value put in local %d (expected %d)]", variable_index, expected_variable_index);
                        }
                        if (variable_index == expected_variable_index) {
                                return store->inst_right;
@@ -258,122 +259,263 @@ get_variable_value_from_ssa_store (MonoInst *store, int expected_variable_index)
        }
 }
 
+/*
+ * Check if the delta of an integer variable value is safe with respect
+ * to the variable size in bytes and its kind (signed or unsigned).
+ * If the delta is not safe, make the value an "any".
+ */
+static void
+check_delta_safety (MonoVariableRelationsEvaluationArea *area, MonoSummarizedValue *value) {
+       if (value->type == MONO_VARIABLE_SUMMARIZED_VALUE) {
+               int variable = value->value.variable.variable;
+               int delta = value->value.variable.delta;
+               if ((area->variable_value_kind [variable]) & MONO_UNSIGNED_VALUE_FLAG) {
+                       if (delta < 0) {
+                               MAKE_VALUE_ANY (*value);
+                       }
+               } else {
+                       if (((area->variable_value_kind [variable]) & MONO_INTEGER_VALUE_SIZE_BITMASK) < 4) {
+                               MAKE_VALUE_ANY (*value);
+                       } else if (delta > 16) {
+                               MAKE_VALUE_ANY (*value);
+                       }
+               }
+       }
+}
+
+/* Prototype, definition comes later */
 static void
-summarize_value (MonoInst *value, MonoSummarizedValue *result) {
+summarize_array_value (MonoVariableRelationsEvaluationArea *area, MonoInst *value, MonoSummarizedValue *result, gboolean is_array_type);
+
+/*
+ * Given a MonoInst representing an integer value, store it in "summarized" form.
+ * result_value_kind: the "expected" kind of result;
+ * result: the "summarized" value
+ * returns the "actual" kind of result, if guessable (otherwise MONO_UNKNOWN_INTEGER_VALUE)
+ */
+static MonoIntegerValueKind
+summarize_integer_value (MonoVariableRelationsEvaluationArea *area, MonoInst *value, MonoSummarizedValue *result, MonoIntegerValueKind result_value_kind) {
+       MonoIntegerValueKind value_kind;
+       
+       if (value->type == STACK_I8) {
+               value_kind = MONO_INTEGER_VALUE_SIZE_8;
+       } else if (value->type == STACK_I4) {
+               value_kind = MONO_INTEGER_VALUE_SIZE_4;
+       } else {
+               value_kind = MONO_UNKNOWN_INTEGER_VALUE;
+       }
+
        switch (value->opcode) {
        case OP_ICONST:
-               result->relation_with_zero = RELATION_BETWEEN_VALUES (value->inst_c0, 0);
-               result->relation_with_one = RELATION_BETWEEN_VALUES (abs (value->inst_c0), 1);
-               result->relation_with_value = MONO_EQ_RELATION;
-               result->value_type = MONO_CONSTANT_SUMMARIZED_VALUE;
-               result->value.constant = value->inst_c0;
+               result->type = MONO_CONSTANT_SUMMARIZED_VALUE;
+               result->value.constant.value = value->inst_c0;
                break;
        case OP_LOCAL:
        case OP_ARG:
-               result->relation_with_zero = MONO_ANY_RELATION;
-               result->relation_with_one = MONO_ANY_RELATION;
-               result->relation_with_value = MONO_EQ_RELATION;
-               result->value_type = MONO_VARIABLE_SUMMARIZED_VALUE;
-               result->value.variable = value->inst_c0;
+               result->type = MONO_VARIABLE_SUMMARIZED_VALUE;
+               result->value.variable.variable = value->inst_c0;
+               result->value.variable.delta = 0;
+               value_kind = area->variable_value_kind [value->inst_c0];
                break;
-       case CEE_LDIND_I4: {
+       case CEE_LDIND_I1:
+               value_kind = MONO_INTEGER_VALUE_SIZE_1;
+               goto handle_load;
+       case CEE_LDIND_U1:
+               value_kind = MONO_UNSIGNED_INTEGER_VALUE_SIZE_1;
+               goto handle_load;
+       case CEE_LDIND_I2:
+               value_kind = MONO_INTEGER_VALUE_SIZE_2;
+               goto handle_load;
+       case CEE_LDIND_U2:
+               value_kind = MONO_UNSIGNED_INTEGER_VALUE_SIZE_2;
+               goto handle_load;
+       case CEE_LDIND_I4:
+               value_kind = MONO_INTEGER_VALUE_SIZE_4;
+               goto handle_load;
+       case CEE_LDIND_U4:
+               value_kind = MONO_UNSIGNED_INTEGER_VALUE_SIZE_4;
+               goto handle_load;
+       case CEE_LDIND_I8:
+               value_kind = MONO_INTEGER_VALUE_SIZE_8;
+               goto handle_load;
+       case CEE_LDIND_I:
+               value_kind = SIZEOF_VOID_P;
+handle_load:
                if ((value->inst_left->opcode == OP_LOCAL) || (value->inst_left->opcode == OP_ARG)) {
-                       summarize_value (value->inst_left, result);
+                       value_kind = summarize_integer_value (area, value->inst_left, result, result_value_kind);
                } else {
-                       MAKE_VALUE_ANY (result);
+                       MAKE_VALUE_ANY (*result);
                }
                break;
-       }
-       case CEE_LDIND_REF:
-               if ((value->inst_left->opcode == OP_LOCAL) || (value->inst_left->opcode == OP_ARG)) {
-                       summarize_value (value->inst_left, result);
+       case CEE_ADD: {
+               MonoSummarizedValue left_value;
+               MonoSummarizedValue right_value;
+               summarize_integer_value (area, value->inst_left, &left_value, result_value_kind);
+               summarize_integer_value (area, value->inst_right, &right_value, result_value_kind);
+               
+               if (left_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) {
+                       if (right_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) {
+                               result->type = MONO_VARIABLE_SUMMARIZED_VALUE;
+                               result->value.variable.variable = left_value.value.variable.variable;
+                               result->value.variable.delta = left_value.value.variable.delta + right_value.value.constant.value;
+                       } else {
+                               MAKE_VALUE_ANY (*result);
+                       }
+               } else if (right_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) {
+                       if (left_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) {
+                               result->type = MONO_VARIABLE_SUMMARIZED_VALUE;
+                               result->value.variable.variable = right_value.value.variable.variable;
+                               result->value.variable.delta = left_value.value.constant.value + right_value.value.variable.delta;
+                       } else {
+                               MAKE_VALUE_ANY (*result);
+                       }
+               } else if ((right_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) && (left_value.type == MONO_CONSTANT_SUMMARIZED_VALUE)) {
+                       /* This should not happen if constant folding has been done */
+                       result->type = MONO_CONSTANT_SUMMARIZED_VALUE;
+                       result->value.constant.value = left_value.value.constant.value + right_value.value.constant.value;
                } else {
-                       MAKE_VALUE_ANY (result);
+                       MAKE_VALUE_ANY (*result);
+               }
+               if (result->type == MONO_VARIABLE_SUMMARIZED_VALUE) {
+                       check_delta_safety (area, result);
                }
                break;
-       case CEE_ADD:
+       }
        case CEE_SUB: {
                MonoSummarizedValue left_value;
                MonoSummarizedValue right_value;
-               summarize_value (value->inst_left, &left_value);
-               summarize_value (value->inst_right, &right_value);
-
-               if (IS_SUMMARIZED_VALUE_VARIABLE (left_value)) {
-                       if (IS_SUMMARIZED_VALUE_CONSTANT (right_value)&& (right_value.value.constant   = 1)) {
-                               MonoValueRelation constant_relation_with_zero = right_value.relation_with_zero;
-                               if (value->opcode == CEE_SUB) {
-                                       constant_relation_with_zero = MONO_SYMMETRIC_RELATION (constant_relation_with_zero);
-                               }
-                               result->relation_with_value = relation_for_sum_of_variable_and_constant (
-                                       left_value.relation_with_value, constant_relation_with_zero);
-                               if (result->relation_with_value != MONO_ANY_RELATION) {
-                                       result->relation_with_zero = MONO_ANY_RELATION;
-                                       result->relation_with_one = MONO_ANY_RELATION;
-                                       result->value_type = MONO_VARIABLE_SUMMARIZED_VALUE;
-                                       result->value.variable = left_value.value.variable;
-                               } else {
-                                       MAKE_VALUE_ANY (result);
-                               }
-                       } else {
-                               MAKE_VALUE_ANY (result);
-                       }
-               } else if (IS_SUMMARIZED_VALUE_VARIABLE (right_value)) {
-                       if (IS_SUMMARIZED_VALUE_CONSTANT (left_value)&& (left_value.value.constant == 1)) {
-                               MonoValueRelation constant_relation_with_zero = left_value.relation_with_zero;
-                               if (value->opcode == CEE_SUB) {
-                                       constant_relation_with_zero = MONO_SYMMETRIC_RELATION (constant_relation_with_zero);
-                               }
-                               result->relation_with_value = relation_for_sum_of_variable_and_constant (
-                                       right_value.relation_with_value, constant_relation_with_zero);
-                               if (result->relation_with_value != MONO_ANY_RELATION) {
-                                       result->relation_with_zero = MONO_ANY_RELATION;
-                                       result->relation_with_one = MONO_ANY_RELATION;
-                                       result->value_type = MONO_VARIABLE_SUMMARIZED_VALUE;
-                                       result->value.variable = right_value.value.variable;
-                               } else {
-                                       MAKE_VALUE_ANY (result);
-                               }
+               summarize_integer_value (area, value->inst_left, &left_value, result_value_kind);
+               summarize_integer_value (area, value->inst_right, &right_value, result_value_kind);
+
+               if (left_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) {
+                       if (right_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) {
+                               result->type = MONO_VARIABLE_SUMMARIZED_VALUE;
+                               result->value.variable.variable = left_value.value.variable.variable;
+                               result->value.variable.delta = left_value.value.variable.delta - right_value.value.constant.value;
                        } else {
-                               MAKE_VALUE_ANY (result);
+                               MAKE_VALUE_ANY (*result);
                        }
-               } else if (IS_SUMMARIZED_VALUE_CONSTANT (right_value)&& IS_SUMMARIZED_VALUE_CONSTANT (left_value)) {
+               } else if ((right_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) && (left_value.type == MONO_CONSTANT_SUMMARIZED_VALUE)) {
                        /* This should not happen if constant folding has been done */
-                       if (right_value.relation_with_value == MONO_EQ_RELATION && left_value.relation_with_value == MONO_EQ_RELATION) {
-                               int constant;
-                               if (value->opcode == CEE_ADD) {
-                                       constant = right_value.value.constant + left_value.value.constant;
+                       result->type = MONO_CONSTANT_SUMMARIZED_VALUE;
+                       result->value.constant.value = left_value.value.constant.value - right_value.value.constant.value;
+               } else {
+                       MAKE_VALUE_ANY (*result);
+               }
+               if (result->type == MONO_VARIABLE_SUMMARIZED_VALUE) {
+                       check_delta_safety (area, result);
+               }
+               break;
+       }
+       case CEE_AND: {
+               MonoSummarizedValue left_value;
+               MonoSummarizedValue right_value;
+               int constant_operand_value;
+
+               summarize_integer_value (area, value->inst_left, &left_value, result_value_kind);
+               summarize_integer_value (area, value->inst_right, &right_value, result_value_kind);
+
+               if (left_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) {
+                       constant_operand_value = left_value.value.constant.value;
+               } else if (right_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) {
+                       constant_operand_value = right_value.value.constant.value;
+               } else {
+                       constant_operand_value = 0;
+               }
+               
+               if (constant_operand_value > 0) {
+                       if (constant_operand_value <= 0xff) {
+                               if ((result_value_kind & MONO_INTEGER_VALUE_SIZE_BITMASK) > 1) {
+                                       value_kind = MONO_UNSIGNED_INTEGER_VALUE_SIZE_1;
                                }
-                               else {
-                                       constant = right_value.value.constant - left_value.value.constant;
+                       } else if (constant_operand_value <= 0xffff) {
+                               if ((result_value_kind & MONO_INTEGER_VALUE_SIZE_BITMASK) > 2) {
+                                       value_kind = MONO_UNSIGNED_INTEGER_VALUE_SIZE_2;
                                }
-                               result->relation_with_zero = RELATION_BETWEEN_VALUES (constant, 0);
-                               result->relation_with_one = RELATION_BETWEEN_VALUES (abs (constant), 1);
-                               result->relation_with_value = MONO_EQ_RELATION;
-                               result->value_type = MONO_CONSTANT_SUMMARIZED_VALUE;
-                               result->value.constant = constant;
-                       } else {
-                               MAKE_VALUE_ANY (result);
                        }
-               } else {
-                       MAKE_VALUE_ANY (result);
                }
+               
+               MAKE_VALUE_ANY (*result);
                break;
        }
-       case CEE_NEWARR:
-               summarize_value (value->inst_newa_len, result);
+       case CEE_CONV_I1:
+       case CEE_CONV_OVF_I1:
+       case CEE_CONV_OVF_I1_UN:
+               value_kind = MONO_INTEGER_VALUE_SIZE_1;
+               MAKE_VALUE_ANY (*result);
+               break;
+       case CEE_CONV_U1:
+       case CEE_CONV_OVF_U1:
+               value_kind = MONO_UNSIGNED_INTEGER_VALUE_SIZE_1;
+               MAKE_VALUE_ANY (*result);
+               break;
+       case CEE_CONV_I2:
+       case CEE_CONV_OVF_I2:
+       case CEE_CONV_OVF_I2_UN:
+               value_kind = MONO_INTEGER_VALUE_SIZE_2;
+               MAKE_VALUE_ANY (*result);
+               break;
+       case CEE_CONV_U2:
+       case CEE_CONV_OVF_U2:
+               value_kind = MONO_UNSIGNED_INTEGER_VALUE_SIZE_2;
+               MAKE_VALUE_ANY (*result);
                break;
        case CEE_LDLEN:
-               summarize_value (value->inst_left, result);
+               summarize_array_value (area, value->inst_left, result, TRUE);
+               value_kind = MONO_UNSIGNED_INTEGER_VALUE_SIZE_4;
+               break;
+       case OP_LCONV_TO_I4:
+               value_kind = summarize_integer_value (area, value->inst_left, result, result_value_kind);
                break;
        case OP_PHI:
-               result->relation_with_zero = MONO_ANY_RELATION;
-               result->relation_with_one = MONO_ANY_RELATION;
-               result->relation_with_value = MONO_EQ_RELATION;
-               result->value_type = MONO_PHI_SUMMARIZED_VALUE;
-               result->value.phi_variables = value->inst_phi_args;
+               result->type = MONO_PHI_SUMMARIZED_VALUE;
+               result->value.phi.number_of_alternatives = *(value->inst_phi_args);
+               result->value.phi.phi_alternatives = value->inst_phi_args + 1;
                break;
        default:
-               MAKE_VALUE_ANY (result);
+               MAKE_VALUE_ANY (*result);
+       }
+       return value_kind;
+}
+
+/*
+ * Given a MonoInst representing an array value, store it in "summarized" form.
+ * result: the "summarized" value
+ * is_array_type: TRUE of we are *sure* that an eventual OP_PCONST will point
+ * to a MonoArray (this can happen for already initialized readonly static fields,
+ * in which case we will get the array length directly from the MonoArray)
+ */
+static void
+summarize_array_value (MonoVariableRelationsEvaluationArea *area, MonoInst *value, MonoSummarizedValue *result, gboolean is_array_type) {
+       switch (value->opcode) {
+       case OP_LOCAL:
+       case OP_ARG:
+               result->type = MONO_VARIABLE_SUMMARIZED_VALUE;
+               result->value.variable.variable = value->inst_c0;
+               result->value.variable.delta = 0;
+               break;
+       case CEE_LDIND_REF:
+               summarize_array_value (area, value->inst_left, result, FALSE);
+               break;
+       case CEE_NEWARR:
+               summarize_integer_value (area, value->inst_newa_len, result, MONO_UNKNOWN_INTEGER_VALUE);
+               break;
+       case OP_PCONST:
+               if ((is_array_type) && (value->inst_p0 != NULL)) {
+                       MonoArray *array = (MonoArray *) (value->inst_p0);
+                       result->type = MONO_CONSTANT_SUMMARIZED_VALUE;
+                       result->value.constant.value = array->max_length;
+               } else {
+                       MAKE_VALUE_ANY (*result);
+               }
+               break;
+       case OP_PHI:
+               result->type = MONO_PHI_SUMMARIZED_VALUE;
+               result->value.phi.number_of_alternatives = *(value->inst_phi_args);
+               result->value.phi.phi_alternatives = value->inst_phi_args + 1;
+               break;
+       default:
+               MAKE_VALUE_ANY (*result);
        }
 }
 
@@ -397,652 +539,929 @@ get_relation_from_branch_instruction (int opcode) {
        case CEE_BNE_UN:
                return MONO_NE_RELATION;
        default:
-               g_assert_not_reached ();
                return MONO_ANY_RELATION;
        }
 }
 
-static int
-contains_array_access (MonoInst *inst) {
-       if (inst->opcode == CEE_LDELEMA) { /* Handle OP_LDELEMA2D, too */
-               return 1;
-       }
-
-       if (mono_burg_arity [inst->opcode]) {
-               if (contains_array_access (inst->inst_left)) {
-                       return 1;
-               }
-               if (mono_burg_arity [inst->opcode] > 1) {
-                       return contains_array_access (inst->inst_right);
-               }
-       }
-       return 0;
-}
-
+/*
+ * Given a BB, find its entry condition and put its relations in a
+ * "MonoAdditionalVariableRelationsForBB" structure.
+ * bb: the BB
+ * relations: the resulting relations (entry condition of the given BB)
+ */
 static void
-analyze_block (MonoBasicBlock *bb, MonoVariableRelationsEvaluationArea *evaluation_area) {
-       MonoSummarizedBasicBlock *b = &(evaluation_area->blocks [bb->dfn]);
-       MonoInst *current_inst = bb->code;
-       MonoInst *last_inst = NULL;
-       int inst_index = 0;
-       
-       if (TRACE_ABC_REMOVAL) {
-               printf ("Analyzing block %d [dfn %d]\n", bb->block_num, bb->dfn);
-       }
+get_relations_from_previous_bb (MonoVariableRelationsEvaluationArea *area, MonoBasicBlock *bb, MonoAdditionalVariableRelationsForBB *relations) {
+       MonoBasicBlock *in_bb;
+       MonoInst *branch;
+       MonoValueRelation branch_relation;
+       MonoValueRelation symmetric_relation;
        
-       g_assert (bb->dfn < evaluation_area->cfg->num_bblocks);
-       b->has_array_access_instructions = 0;
-       b->block = bb;
+       INITIALIZE_VALUE_RELATION (&(relations->relation1.relation));
+       relations->relation1.relation.relation_is_static_definition = FALSE;
+       relations->relation1.insertion_point = NULL;
+       relations->relation1.variable = -1;
+       INITIALIZE_VALUE_RELATION (&(relations->relation2.relation));
+       relations->relation2.relation.relation_is_static_definition = FALSE;
+       relations->relation2.insertion_point = NULL;
+       relations->relation2.variable = -1;
        
-       while (current_inst != NULL) {
-               if (TRACE_ABC_REMOVAL) {
-                       printf ("Analyzing instruction %d\n", inst_index);
-                       inst_index++;
-               }
-               
-               if (contains_array_access (current_inst)) {
-                       b->has_array_access_instructions = 1;
-               }
-               
-               if (current_inst->next == NULL) {
-                       last_inst = current_inst;
-               }
-               current_inst = current_inst->next;
-       }
        
-       if (last_inst != NULL) {
-               switch (last_inst->opcode) {
-               case CEE_BEQ:
-               case CEE_BLT:
-               case CEE_BLE:
-               case CEE_BGT:
-               case CEE_BGE:
-               case CEE_BNE_UN:
-               case CEE_BLT_UN:
-               case CEE_BLE_UN:
-               case CEE_BGT_UN:
-               case CEE_BGE_UN:
-                       if (last_inst->inst_left->opcode == OP_COMPARE) {
-                               int number_of_variables = 0;
-                               int current_variable = 0;
-                               
-                               MonoSummarizedValue left_value;
-                               MonoSummarizedValue right_value;
-                               MonoValueRelation relation = get_relation_from_branch_instruction (last_inst->opcode);
-                               MonoValueRelation symmetric_relation = MONO_SYMMETRIC_RELATION (relation);
-                               summarize_value (last_inst->inst_left->inst_left, &left_value);
-                               summarize_value (last_inst->inst_left->inst_right, &right_value);
-                               /* It is actually possible to handle some more case... */
-                               if ((left_value.relation_with_value == MONO_EQ_RELATION) &&
-                                       (right_value.relation_with_value == MONO_EQ_RELATION)) {
-                                       if (left_value.value_type == MONO_VARIABLE_SUMMARIZED_VALUE)number_of_variables++;
-                                       if (right_value.value_type == MONO_VARIABLE_SUMMARIZED_VALUE)number_of_variables++;
-                                       if (number_of_variables > 0) {
-                                               MonoBranchData *branch_true;
-                                               MonoBranchData *branch_false;
-
-                                               b->number_of_branches = 2;
-                                               b->branches = (MonoBranchData*) mono_mempool_alloc (
-                                                       evaluation_area->pool, sizeof (MonoBranchData) * 2);
-                                               branch_true = &(b->branches [0]);
-                                               branch_true->destination_block = last_inst->inst_true_bb;
-                                               branch_true->number_of_conditions = number_of_variables;
-                                               branch_true->conditions = (MonoBranchCondition*)
-                                                       mono_mempool_alloc (evaluation_area->pool, sizeof (MonoBranchCondition) * number_of_variables);
-                                               branch_false = &(b->branches [1]);
-                                               branch_false->destination_block = last_inst->inst_false_bb;
-                                               branch_false->number_of_conditions = number_of_variables;
-                                               branch_false->conditions = (MonoBranchCondition*)
-                                                       mono_mempool_alloc (evaluation_area->pool, sizeof (MonoBranchCondition) * number_of_variables);
-                                               if (left_value.value_type == MONO_VARIABLE_SUMMARIZED_VALUE) {
-                                                       MonoBranchCondition *condition_true = &(branch_true->conditions [current_variable]);
-                                                       MonoBranchCondition *condition_false;
-
-                                                       condition_true->variable = left_value.value.variable;
-                                                       condition_true->value = right_value;
-                                                       condition_true->value.relation_with_zero = MONO_ANY_RELATION;
-                                                       condition_true->value.relation_with_one = MONO_ANY_RELATION;
-                                                       condition_true->value.relation_with_value = relation;
-                                                       condition_false = &(branch_false->conditions [current_variable]);
-                                                       condition_false->variable = left_value.value.variable;
-                                                       condition_false->value = right_value;
-                                                       condition_false->value.relation_with_zero = MONO_ANY_RELATION;
-                                                       condition_false->value.relation_with_one = MONO_ANY_RELATION;
-                                                       condition_false->value.relation_with_value = MONO_NEGATED_RELATION (relation);
-                                                       current_variable++;
-                                               }
-                                               if (right_value.value_type == MONO_VARIABLE_SUMMARIZED_VALUE) {
-                                                       MonoBranchCondition *condition_true = &(branch_true->conditions [current_variable]);
-                                                       MonoBranchCondition *condition_false;
-
-                                                       condition_true->variable = right_value.value.variable;
-                                                       condition_true->value = left_value;
-                                                       condition_true->value.relation_with_zero = MONO_ANY_RELATION;
-                                                       condition_true->value.relation_with_one = MONO_ANY_RELATION;
-                                                       condition_true->value.relation_with_value = symmetric_relation;
-                                                       condition_false = &(branch_false->conditions [current_variable]);
-                                                       condition_false->variable = right_value.value.variable;
-                                                       condition_false->value = left_value;
-                                                       condition_false->value.relation_with_zero = MONO_ANY_RELATION;
-                                                       condition_false->value.relation_with_one = MONO_ANY_RELATION;
-                                                       condition_false->value.relation_with_value = MONO_NEGATED_RELATION (symmetric_relation);
-                                               }
-                                       } else {
-                                               b->number_of_branches = 0;
-                                               b->branches = NULL;
-                                       }
+       if (bb->in_count == 1) { /* Should write the code to "sum" conditions... */
+               in_bb = bb->in_bb [0];
+               branch = in_bb->last_ins;
+               if (branch == NULL) return;
+               branch_relation = get_relation_from_branch_instruction (branch->opcode);
+               if ((branch_relation != MONO_ANY_RELATION) && (branch->inst_left->opcode == OP_COMPARE)) {
+                       MonoSummarizedValue left_value;
+                       MonoSummarizedValue right_value;
+                       gboolean code_path;
+
+                       if (branch->inst_true_bb == bb) {
+                               code_path = TRUE;
+                       } else if (branch->inst_false_bb == bb) {
+                               code_path = FALSE;
+                       } else {
+                               code_path = TRUE;
+                               g_assert_not_reached ();
+                       }
+
+                       if (!code_path) {
+                               branch_relation = MONO_NEGATED_RELATION (branch_relation);
+                       }
+                       symmetric_relation = MONO_SYMMETRIC_RELATION (branch_relation);
+
+                       summarize_integer_value (area, branch->inst_left->inst_left, &left_value, MONO_UNKNOWN_INTEGER_VALUE);
+                       summarize_integer_value (area, branch->inst_left->inst_right, &right_value, MONO_UNKNOWN_INTEGER_VALUE);
+
+                       if ((left_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) && ((right_value.type == MONO_VARIABLE_SUMMARIZED_VALUE)||(right_value.type == MONO_CONSTANT_SUMMARIZED_VALUE))) {
+                               relations->relation1.variable = left_value.value.variable.variable;
+                               relations->relation1.relation.relation = branch_relation;
+                               relations->relation1.relation.related_value = right_value;
+                               if (right_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) {
+                                       relations->relation1.relation.related_value.value.constant.value -= left_value.value.variable.delta;
                                } else {
-                                       b->number_of_branches = 0;
-                                       b->branches = NULL;
+                                       relations->relation1.relation.related_value.value.variable.delta -= left_value.value.variable.delta;
+                               }
+                       }
+                       if ((right_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) && ((left_value.type == MONO_VARIABLE_SUMMARIZED_VALUE)||(left_value.type == MONO_CONSTANT_SUMMARIZED_VALUE))) {
+                               relations->relation2.variable = right_value.value.variable.variable;
+                               relations->relation2.relation.relation = symmetric_relation;
+                               relations->relation2.relation.related_value = left_value;
+                               if (left_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) {
+                                       relations->relation2.relation.related_value.value.constant.value -= right_value.value.variable.delta;
+                               } else {
+                                       relations->relation2.relation.related_value.value.variable.delta -= right_value.value.variable.delta;
                                }
-                       } else {
-                               b->number_of_branches = 0;
-                               b->branches = NULL;
                        }
-                       break;
-               case CEE_SWITCH:
-                       /* Should handle switches... */
-                       /* switch_operand = last_inst->inst_right; */
-                       /* number_of_cases = GPOINTER_TO_INT (last_inst->klass); */
-                       /* cases = last_inst->inst_many_bb; */
-                       b->number_of_branches = 0;
-                       b->branches = NULL;
-                       break;
-               default:
-                       b->number_of_branches = 0;
-                       b->branches = NULL;
                }
-       } else {
-               b->number_of_branches = 0;
-               b->branches = NULL;
        }
+}
 
-       if (TRACE_ABC_REMOVAL) {
-               print_summarized_block (b);
+
+/*
+ * Add the given relations to the evaluation area.
+ * area: the evaluation area
+ * change: the relations that must be added
+ */
+static void
+apply_change_to_evaluation_area (MonoVariableRelationsEvaluationArea *area, MonoAdditionalVariableRelation *change) {
+       MonoSummarizedValueRelation *base_relation;
+       
+       if (change->relation.relation != MONO_ANY_RELATION) {
+               base_relation = &(area->relations [change->variable]);
+               while ((base_relation->next != NULL) && (base_relation->next->relation_is_static_definition)) {
+                       base_relation = base_relation->next;
+               }
+               change->insertion_point = base_relation;
+               change->relation.next = base_relation->next;
+               base_relation->next = &(change->relation);
        }
 }
 
-#define SET_VARIABLE_RELATIONS(vr, relation, n)do {\
-       (vr)->relation_with_zero = (relation);\
-       (vr)->relation_with_one = (relation);\
-       memset ((vr)->relations_with_variables,(relation),(n));\
-} while (0);
+/*
+ * Remove the given relation from the evaluation area.
+ * change: the relation that must be removed
+ */
+static void
+remove_change_from_evaluation_area (MonoAdditionalVariableRelation *change) {
+       if (change->insertion_point != NULL) {
+               change->insertion_point->next = change->relation.next;
+               change->relation.next = NULL;
+       }
+}
 
-#define COMBINE_VARIABLE_RELATIONS(operator, vr, related_vr, n)do {\
-       int i;\
-       operator ((vr)->relation_with_zero, (related_vr)->relation_with_zero);\
-       operator ((vr)->relation_with_one, (related_vr)->relation_with_one);\
-       for (i = 0; i < (n); i++) {\
-               operator ((vr)->relations_with_variables [i], (related_vr)->relations_with_variables [i]);\
-       }\
-} while (0);
 
-#define RELATION_ASSIGNMENT(destination,source) (destination)=(source)
-#define RELATION_UNION(destination,source) (destination)|=(source)
-#define RELATION_INTERSECTION(destination,source) (destination)&=(source)
+static void
+clean_contexts (MonoRelationsEvaluationContext *contexts, int number) {
+       int i;
+       for (i = 0; i < number; i++) {
+               contexts [i].status = MONO_RELATIONS_EVALUATION_NOT_STARTED;
+       }
+}
 
 
+/*
+ * Perform the intersection of a range and a constant value (taking into
+ * account the relation that the value has with the range).
+ * range: the range that will be intersected with the value
+ * value: the value that will be intersected with the range
+ * relation: the relation between the range and the value
+ */
+static void
+intersect_value( MonoRelationsEvaluationRange *range, int value, MonoValueRelation relation ) {
+       switch (relation) {
+       case MONO_NO_RELATION:
+               MONO_MAKE_RELATIONS_EVALUATION_RANGE_IMPOSSIBLE (*range);
+               break;
+       case MONO_ANY_RELATION:
+               break;
+       case MONO_EQ_RELATION:
+               MONO_UPPER_EVALUATION_RANGE_INTERSECTION (range->upper, value);
+               MONO_LOWER_EVALUATION_RANGE_INTERSECTION (range->lower, value);
+               break;
+       case MONO_NE_RELATION: {
+               /* IMPROVEMENT Figure this out! (ignoring it is safe anyway) */
+               break;
+       }
+       case MONO_LT_RELATION:
+               MONO_UPPER_EVALUATION_RANGE_INTERSECTION (range->upper, MONO_UPPER_EVALUATION_RANGE_NOT_EQUAL (value));
+               break;
+       case MONO_LE_RELATION:
+               MONO_UPPER_EVALUATION_RANGE_INTERSECTION (range->upper, value);
+               break;
+       case MONO_GT_RELATION:
+               MONO_LOWER_EVALUATION_RANGE_INTERSECTION (range->lower, MONO_LOWER_EVALUATION_RANGE_NOT_EQUAL (value));
+               break;
+       case MONO_GE_RELATION:
+               MONO_LOWER_EVALUATION_RANGE_INTERSECTION (range->lower, value);
+               break;
+       default:
+               g_assert_not_reached();
+       }
+}
+
 
+/*
+ * Perform the intersection of two pairs of ranges (taking into account the
+ * relation between the ranges and a given delta).
+ * ranges: the ranges that will be intersected
+ * other_ranges the other ranges that will be intersected
+ * delta: the delta between the pairs of ranges
+ * relation: the relation between the pairs of ranges
+ */
 static void
-evaluate_variable_relations (gssize variable, MonoVariableRelationsEvaluationArea *evaluation_area, MonoRelationsEvaluationContext *father_context) {
-       MonoVariableRelations *relations = &(evaluation_area->variable_relations [variable]);
-       MonoRelationsEvaluationContext context;
-       if (TRACE_ABC_REMOVAL) {
-               printf ("Applying definition of variable %d\n", variable);
+intersect_ranges( MonoRelationsEvaluationRanges *ranges, MonoRelationsEvaluationRanges *other_ranges, int delta, MonoValueRelation relation ) {
+       if (delta == 0) {
+               switch (relation) {
+               case MONO_NO_RELATION:
+                       MONO_MAKE_RELATIONS_EVALUATION_RANGES_IMPOSSIBLE (*ranges);
+                       break;
+               case MONO_ANY_RELATION:
+                       break;
+               case MONO_EQ_RELATION:
+                       MONO_RELATIONS_EVALUATION_RANGES_INTERSECTION (*ranges, *other_ranges);
+                       break;
+               case MONO_NE_RELATION: {
+                       /* FIXME Figure this out! (ignoring it is safe anyway) */
+                       break;
+               }
+               case MONO_LT_RELATION:
+                       MONO_UPPER_EVALUATION_RANGE_INTERSECTION (ranges->zero.upper, MONO_UPPER_EVALUATION_RANGE_NOT_EQUAL (other_ranges->zero.upper));
+                       MONO_UPPER_EVALUATION_RANGE_INTERSECTION (ranges->variable.upper, MONO_UPPER_EVALUATION_RANGE_NOT_EQUAL (other_ranges->variable.upper));
+                       break;
+               case MONO_LE_RELATION:
+                       MONO_UPPER_EVALUATION_RANGE_INTERSECTION (ranges->zero.upper, other_ranges->zero.upper);
+                       MONO_UPPER_EVALUATION_RANGE_INTERSECTION (ranges->variable.upper, other_ranges->variable.upper);
+                       break;
+               case MONO_GT_RELATION:
+                       MONO_LOWER_EVALUATION_RANGE_INTERSECTION (ranges->zero.lower, MONO_LOWER_EVALUATION_RANGE_NOT_EQUAL (other_ranges->zero.lower));
+                       MONO_LOWER_EVALUATION_RANGE_INTERSECTION (ranges->variable.lower, MONO_LOWER_EVALUATION_RANGE_NOT_EQUAL (other_ranges->variable.lower));
+                       break;
+               case MONO_GE_RELATION:
+                       MONO_LOWER_EVALUATION_RANGE_INTERSECTION (ranges->zero.lower, other_ranges->zero.lower);
+                       MONO_LOWER_EVALUATION_RANGE_INTERSECTION (ranges->variable.lower, other_ranges->variable.lower);
+                       break;
+               default:
+                       g_assert_not_reached();
+               }
+       } else {
+               MonoRelationsEvaluationRanges translated_ranges = *other_ranges;
+               MONO_ADD_DELTA_SAFELY_TO_RANGES (translated_ranges, delta);
+               intersect_ranges( ranges, &translated_ranges, FALSE, relation );
        }
-       context.father_context = father_context;
-       context.variable = variable;
-       switch (relations->evaluation_step) {
+}
+
+/*
+ * Recursive method that traverses the relation graph to evaluate the
+ * relation between two variables.
+ * At the end of the execution, the resulting ranges are in the context of
+ * the "starting" variable.
+ * area: the current evaluation area (it contains the relation graph and
+ *       memory for all the evaluation contexts is already allocated)
+ * variable: starting variable (the value ranges in its context are the result
+ *           of the execution of this procedure)
+ * target_variable: the variable with respect to which the starting variable
+ *                  is evaluated (tipically the starting variable is the index
+ *                  and the target one is the array (which means its length))
+ * father_context: the previous evaluation context in recursive invocations
+ *                 (or NULL for the first invocation)
+ */
+static void
+evaluate_relation_with_target_variable (MonoVariableRelationsEvaluationArea *area, int variable, int target_variable, MonoRelationsEvaluationContext *father_context) {
+       MonoRelationsEvaluationContext *context = &(area->contexts [variable]);
+       
+       // First of all, we check the evaluation status
+       // (what must be done is *very* different in each case)
+       switch (context->status) {
        case MONO_RELATIONS_EVALUATION_NOT_STARTED: {
-               MonoSummarizedValue *value = &(evaluation_area->variable_definitions [variable]);
-               relations->evaluation_step = MONO_RELATIONS_EVALUATION_IN_PROGRESS;
+               MonoSummarizedValueRelation *relation = &(area->relations [variable]);
+               
                if (TRACE_ABC_REMOVAL) {
-                       printf ("Current step is MONO_RELATIONS_EVALUATION_NOT_STARTED, summarized value is:\n");
-                       print_summarized_value (value);
+                       printf ("Evaluating varible %d (target variable %d)\n", variable, target_variable);
+                       print_summarized_value_relation (relation);
+                       printf ("\n");
                }
-               switch (value->value_type) {
-               case MONO_CONSTANT_SUMMARIZED_VALUE:
-                       if (value->relation_with_value == MONO_EQ_RELATION) {
-                               relations->relation_with_zero &= RELATION_BETWEEN_VALUES (value->value.constant, 0);
-                               relations->relation_with_one &= RELATION_BETWEEN_VALUES (abs (value->value.constant), 1);
-                       }
-                       /* Other cases should not happen... */
-                       break;
-               case MONO_VARIABLE_SUMMARIZED_VALUE: {
-                       gssize related_variable = value->value.variable;
-                       relations->relations_with_variables [related_variable] = value->relation_with_value;
-                       evaluate_variable_relations (related_variable, evaluation_area, &context);
-                       if (value->relation_with_value == MONO_EQ_RELATION) {
-                               COMBINE_VARIABLE_RELATIONS (RELATION_INTERSECTION, relations,
-                                       &(evaluation_area->variable_relations [related_variable]), evaluation_area->cfg->num_varinfo);
+               
+               // We properly inizialize the context
+               context->status = MONO_RELATIONS_EVALUATION_IN_PROGRESS;
+               context->father = father_context;
+               MONO_MAKE_RELATIONS_EVALUATION_RANGES_WEAK (context->ranges);
+               
+               // If we have found the target variable, we can set the range
+               // related to it in the context to "equal" (which is [0,0])
+               if (variable == target_variable) {
+                       if (TRACE_ABC_REMOVAL) {
+                               printf ("Target variable reached (%d), continuing to evaluate relations with constants\n", variable);
                        }
-                       /* Other cases should be handled... */
-                       break;
+                       context->ranges.variable.lower = 0;
+                       context->ranges.variable.upper = 0;
                }
-               case MONO_PHI_SUMMARIZED_VALUE:
-                       if (value->relation_with_value == MONO_EQ_RELATION) {
+               
+               // Examine all relations for this variable (scan the list)
+               // The contribute of each relation will be intersected (logical and)
+               while (relation != NULL) {
+                       context->current_relation = relation;
+                       
+                       if (TRACE_ABC_REMOVAL) {
+                               printf ("Processing (%d): ", variable);
+                               print_summarized_value_relation (relation);
+                               printf ("\n");
+                       }
+                       
+                       // We decie what to do according the the type of the related value
+                       switch (relation->related_value.type) {
+                       case MONO_ANY_SUMMARIZED_VALUE:
+                               // No added information, skip it
+                               break;
+                       case MONO_CONSTANT_SUMMARIZED_VALUE:
+                               // Intersect range with constant (taking into account the relation)
+                               intersect_value (&(context->ranges.zero), relation->related_value.value.constant.value, relation->relation);
+                               break;
+                       case MONO_VARIABLE_SUMMARIZED_VALUE:
+                               // Generally, evaluate related variable and intersect ranges.
+                               // However, some check is necessary...
+                               
+                               // If the relation is "ANY", nothing to do (no added information)
+                               if (relation->relation != MONO_ANY_RELATION) {
+                                       int related_variable = relation->related_value.value.variable.variable;
+                                       MonoRelationsEvaluationContext *related_context = &(area->contexts [related_variable]);
+                                       
+                                       // The second condition in the "or" avoids messing with "back edges" in the graph traversal
+                                       // (they are simply ignored instead of triggering the handling of recursion)
+                                       if ( (related_context->status == MONO_RELATIONS_EVALUATION_NOT_STARTED) || !
+                                                       ((related_context->current_relation->related_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) &&
+                                                       (related_context->current_relation->related_value.value.variable.variable == variable))) {
+                                               // Evaluate the related variable
+                                               evaluate_relation_with_target_variable (area, related_variable, target_variable, context);
+                                               
+                                               // Check if we are part of a recursive loop
+                                               if (context->status & MONO_RELATIONS_EVALUATION_IS_RECURSIVE) {
+                                                       if (TRACE_ABC_REMOVAL) {
+                                                               printf ("Recursivity detected for varible %d (target variable %d), status ", variable, target_variable);
+                                                               print_evaluation_context_status (context->status);
+                                                       }
+                                                       
+                                                       // If we are, check if the evaluation of the related variable is complete
+                                                       if (related_context->status == MONO_RELATIONS_EVALUATION_COMPLETED) {
+                                                               // If it is complete, we are part of a recursive definition.
+                                                               // Since it is a *definition* (and definitions are evaluated *before*
+                                                               // conditions because they are first in the list), intersection is not
+                                                               // strictly necessary, we simply copy the ranges and apply the delta
+                                                               context->ranges = related_context->ranges;
+                                                               /* Delta has already been checked for over/under-flow when evaluating values */
+                                                               MONO_ADD_DELTA_SAFELY_TO_RANGES (context->ranges, relation->related_value.value.variable.delta);
+                                                               context->status = MONO_RELATIONS_EVALUATION_COMPLETED;
+                                                               if (TRACE_ABC_REMOVAL) {
+                                                                       printf (", ranges already computed, result: \n");
+                                                                       print_evaluation_context_ranges (&(context->ranges));
+                                                                       printf (" (delta is %d)\n", relation->related_value.value.variable.delta);
+                                                               }
+                                                       } else {
+                                                               // If it is not complete, do nothing (we do not have enough information)
+                                                               if (TRACE_ABC_REMOVAL) {
+                                                                       printf (", ranges not computed\n");
+                                                               }
+                                                       }
+                                               } else {
+                                                       // If we are not (the common case) intersect the result
+                                                       intersect_ranges( &(context->ranges), &(related_context->ranges), relation->related_value.value.variable.delta, relation->relation );
+                                               }
+                                       } else {
+                                               if (TRACE_ABC_REMOVAL) {
+                                                       printf ("Relation is a back-edge in this traversal, skipping\n");
+                                               }
+                                       }
+                               }
+                               break;
+                       case MONO_PHI_SUMMARIZED_VALUE: {
+                               // We must compute all PHI alternatives, combining the results (with a union, which is a logical "or"),
+                               // and intersect this result with the ranges in the context; we must also take into account recursions
+                               // (with loops that can be ascending, descending, or indefinite)
+                               MonoRelationsEvaluationRanges phi_ranges;
                                int phi;
-                               MonoVariableRelations *phi_union = (MonoVariableRelations*) alloca (sizeof (MonoVariableRelations));
-                               phi_union->relations_with_variables = (unsigned char*) alloca (evaluation_area->cfg->num_varinfo);
-                               SET_VARIABLE_RELATIONS (phi_union, MONO_NO_RELATION, evaluation_area->cfg->num_varinfo);
-                               for (phi = 0; phi < *(value->value.phi_variables); phi++) {
-                                       gssize related_variable = value->value.phi_variables [phi+1];
-                                       evaluate_variable_relations (related_variable, evaluation_area, &context);
-                                       COMBINE_VARIABLE_RELATIONS (RELATION_UNION, phi_union,
-                                               &(evaluation_area->variable_relations [related_variable]), evaluation_area->cfg->num_varinfo);
+                               gboolean is_ascending = FALSE;
+                               gboolean is_descending = FALSE;
+                               
+                               MONO_MAKE_RELATIONS_EVALUATION_RANGES_IMPOSSIBLE (phi_ranges);
+                               for (phi = 0; phi < relation->related_value.value.phi.number_of_alternatives; phi++) {
+                                       int phi_alternative = relation->related_value.value.phi.phi_alternatives [phi];
+                                       evaluate_relation_with_target_variable (area, phi_alternative, target_variable, context);
+                                       
+                                       // This means we are part of a recursive loop
+                                       if (context->status & MONO_RELATIONS_EVALUATION_IS_RECURSIVE) {
+                                               if (TRACE_ABC_REMOVAL) {
+                                                       printf ("Recursivity detected for varible %d (target variable %d), status ", variable, target_variable);
+                                                       print_evaluation_context_status (context->status);
+                                                       printf ("\n");
+                                               }
+                                               if (context->status & MONO_RELATIONS_EVALUATION_IS_RECURSIVELY_ASCENDING) {
+                                                       is_ascending = TRUE;
+                                               }
+                                               if (context->status & MONO_RELATIONS_EVALUATION_IS_RECURSIVELY_DESCENDING) {
+                                                       is_descending = TRUE;
+                                               }
+                                               if (context->status & MONO_RELATIONS_EVALUATION_IS_RECURSIVELY_INDEFINITE) {
+                                                       is_ascending = TRUE;
+                                                       is_descending = TRUE;
+                                               }
+                                               
+                                               // Clear "recursivity" bits in the status (recursion has been handled)
+                                               context->status = MONO_RELATIONS_EVALUATION_IN_PROGRESS;
+                                       } else {
+                                               MONO_RELATIONS_EVALUATION_RANGES_UNION (phi_ranges, area->contexts [phi_alternative].ranges);
+                                       }
                                }
-                               if (TRACE_ABC_REMOVAL) {
-                                       printf ("Resulting phi_union is:\n");
-                                       print_variable_relations (phi_union, variable, evaluation_area->cfg->num_varinfo);
+                               
+                               // Apply the effects of all recursive loops
+                               if (is_ascending) {
+                                       phi_ranges.zero.upper = INT_MAX;
+                                       phi_ranges.variable.upper = INT_MAX;
+                               }
+                               if (is_descending) {
+                                       phi_ranges.zero.lower = INT_MIN;
+                                       phi_ranges.variable.lower = INT_MIN;
                                }
-                               COMBINE_VARIABLE_RELATIONS (RELATION_INTERSECTION, relations,
-                                       phi_union, evaluation_area->cfg->num_varinfo);
+                               
+                               // Intersect final result
+                               MONO_RELATIONS_EVALUATION_RANGES_INTERSECTION (context->ranges, phi_ranges);
+                               break;
                        }
-                       /* Other cases should not happen... */
-                       break;
-               default:
-                       g_assert_not_reached ();
+                       default:
+                               g_assert_not_reached();
+                       }
+                       
+                       // Pass to next relation
+                       relation = relation->next;
+               }
+               
+               // Check if any recursivity bits are still in the status, and in any case clear them
+               if (context->status & MONO_RELATIONS_EVALUATION_IS_RECURSIVE) {
+                       if (TRACE_ABC_REMOVAL) {
+                               printf ("Recursivity for varible %d (target variable %d) discards computation, status ", variable, target_variable);
+                               print_evaluation_context_status (context->status);
+                               printf ("\n");
+                       }
+                       // If yes, we did not have enough information (most likely we were evaluated inside a PHI, but we also
+                       // depended on the same PHI, which was still in evaluation...), so clear the status to "NOT_STARTED"
+                       // (if we will be evaluated again, the PHI will be already done, so our evaluation will succeed)
+                       context->status = MONO_RELATIONS_EVALUATION_NOT_STARTED;
+               } else {
+                       if (TRACE_ABC_REMOVAL) {
+                               printf ("Ranges for varible %d (target variable %d) computed: ", variable, target_variable);
+                               print_evaluation_context_ranges (&(context->ranges));
+                               printf ("\n");
+                       }
+                       // If not (the common case) the evaluation is complete, and the result is in the context
+                       context->status = MONO_RELATIONS_EVALUATION_COMPLETED;
                }
                break;
        }
        case MONO_RELATIONS_EVALUATION_IN_PROGRESS: {
-               MonoVariableRelations *recursive_value_relations = NULL;
-               unsigned char recursive_relation = MONO_ANY_RELATION;
-               MonoRelationsEvaluationContext *current_context = context.father_context;
+               // This means we are in a recursive loop
+               MonoRelationsEvaluationContext *current_context = father_context;
+               MonoRelationsEvaluationContext *last_context = context->father;
+               gboolean evaluation_can_be_recursive = TRUE;
+               gboolean evaluation_is_definition = TRUE;
+               int path_value = 0;
+               
                if (TRACE_ABC_REMOVAL) {
-                       printf ("Current step is MONO_RELATIONS_EVALUATION_IN_PROGRESS\n");
+                       printf ("Evaluation of varible %d (target variable %d) already in progress\n", variable, target_variable);
+                       print_evaluation_context (context);
+                       print_summarized_value_relation (context->current_relation);
+                       printf ("\n");
                }
-               relations->definition_is_recursive = 1;
-               while (current_context != NULL && current_context->variable != variable) {
-                       MonoVariableRelations *context_relations = &(evaluation_area->variable_relations [current_context->variable]);
-                       MonoSummarizedValue *context_value = &(evaluation_area->variable_definitions [current_context->variable]);
-                       if (TRACE_ABC_REMOVAL) {
-                               printf ("Backtracing to context %d\n", current_context->variable);
+               
+               // We must check if the loop can be a recursive definition (we scan the whole loop)
+               while (current_context != last_context) {
+                       if (current_context == NULL) {
+                               printf ("Broken recursive ring in ABC removal\n");
+                               g_assert_not_reached ();
                        }
-                       if (recursive_value_relations == NULL) {
-                               if (context_value->relation_with_value != MONO_EQ_RELATION) {
-                                       recursive_value_relations = context_relations;
-                                       recursive_relation = context_value->relation_with_value;
-                                       if (TRACE_ABC_REMOVAL) {
-                                               printf ("Accepted recursive definition, relation is ");
-                                               print_relation (recursive_relation);
-                                               printf ("\n");
-                                       }
+                       
+                       if (current_context->current_relation->relation_is_static_definition) {
+                               if (current_context->current_relation->related_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) {
+                                       /* No need to check path_value for over/under-flow, since delta should be safe */
+                                       path_value += current_context->current_relation->related_value.value.variable.delta;
+                               } else if (current_context->current_relation->related_value.type != MONO_PHI_SUMMARIZED_VALUE) {
+                                       evaluation_can_be_recursive = FALSE;
                                }
                        } else {
-                               if (context_value->relation_with_value != MONO_EQ_RELATION) {
-                                       recursive_relation = MONO_NO_RELATION;
-                                       if (TRACE_ABC_REMOVAL) {
-                                               printf ("Rejected recursive definition, bad relation is ");
-                                               print_relation (context_value->relation_with_value);
-                                               printf ("\n");
-                                       }
-                               }
+                               evaluation_is_definition = FALSE;
+                               evaluation_can_be_recursive = FALSE;
                        }
-                       current_context = current_context->father_context;
+                       
+                       current_context = current_context->father;
                }
-               if (recursive_value_relations != NULL && recursive_relation != MONO_NO_RELATION) {
-                       int i;
-                       /* This should handle "grows" and "decreases" cases */
-                       recursive_value_relations->relation_with_zero &= recursive_relation;
-                       for (i = 0; i < evaluation_area->cfg->num_varinfo; i++) {
-                               recursive_value_relations->relations_with_variables [i] &= recursive_relation;
+               
+               // If this is a recursive definition, we properly flag the status in all the involved contexts
+               if (evaluation_is_definition) {
+                       MonoRelationsEvaluationStatus recursive_status;
+                       if (evaluation_can_be_recursive) {
+                               if (path_value > 0) {
+                                       recursive_status = MONO_RELATIONS_EVALUATION_IS_RECURSIVELY_ASCENDING;
+                               } else if (path_value < 0) {
+                                       recursive_status = MONO_RELATIONS_EVALUATION_IS_RECURSIVELY_DESCENDING;
+                               } else {
+                                       recursive_status = MONO_RELATIONS_EVALUATION_IS_RECURSIVELY_INDEFINITE;
+                               }
+                       } else {
+                               recursive_status = MONO_RELATIONS_EVALUATION_IS_RECURSIVELY_INDEFINITE;
+                       }
+                       
+                       if (TRACE_ABC_REMOVAL) {
+                               printf ("Recursivity accepted (");
+                               print_evaluation_context_status (recursive_status);
+                               printf (")\n");
+                       }
+                       
+                       current_context = father_context;
+                       while (current_context != last_context) {
+                               current_context->status |= recursive_status;
+                               current_context = current_context->father;
+                       }
+               } else {
+                       if (TRACE_ABC_REMOVAL) {
+                               printf ("Recursivity rejected (some relation in the cycle is not a defintion)\n");
                        }
                }
+               break;
+       }
+       case MONO_RELATIONS_EVALUATION_COMPLETED: {
                return;
        }
-       case MONO_RELATIONS_EVALUATION_COMPLETED:
+       default:
                if (TRACE_ABC_REMOVAL) {
-                       printf ("Current step is MONO_RELATIONS_EVALUATION_COMPLETED\n");
+                       printf ("Varible %d (target variable %d) already in a recursive ring, skipping\n", variable, target_variable);
+                       print_evaluation_context (context);
+                       print_summarized_value_relation (context->current_relation);
+                       printf ("\n");
                }
-               return;
-       default:
-               g_assert_not_reached ();
+               break;
        }
-
-       relations->evaluation_step = MONO_RELATIONS_EVALUATION_COMPLETED;
+       
 }
 
-static int
-propagate_relations (MonoVariableRelationsEvaluationArea *evaluation_area) {
-       int changes = 0;
-       gssize variable;
-       for (variable = 0; variable < evaluation_area->cfg->num_varinfo; variable++) {
-               MonoVariableRelations *relations = &(evaluation_area->variable_relations [variable]);
-               gssize related_variable;
-               for (related_variable = 0; related_variable < evaluation_area->cfg->num_varinfo; related_variable++) {
-                       unsigned char relation_with_variable = relations->relations_with_variables [related_variable];
-                       if (relation_with_variable != MONO_ANY_RELATION) {
-                               MonoVariableRelations *related_relations = &(evaluation_area->variable_relations [related_variable]);
-                               gssize variable_related_to_related_variable;
-                               unsigned char new_relation_with_zero = PROPAGATED_RELATION (relation_with_variable, related_relations->relation_with_zero);
-                               if (RELATION_ADDS_INFORMATION (relations->relation_with_zero, new_relation_with_zero)) {
-                                       if (TRACE_ABC_REMOVAL) {
-                                               printf ("RELATION_ADDS_INFORMATION variable %d, related_variable %d, relation_with_zero ",
-                                                       variable, related_variable);
-                                               print_relation (relations->relation_with_zero);
-                                               printf (" - ");
-                                               print_relation (new_relation_with_zero);
-                                               printf (" => ");
-                                       }
-                                       relations->relation_with_zero &= new_relation_with_zero;
-                                       if (TRACE_ABC_REMOVAL) {
-                                               print_relation (relations->relation_with_zero);
-                                               printf ("\n");
-                                       }
-                                       changes++;
+/*
+ * Apply the given value kind to the given range
+ */
+static void apply_value_kind_to_range (MonoRelationsEvaluationRange *range, MonoIntegerValueKind value_kind) {
+       if (value_kind != MONO_UNKNOWN_INTEGER_VALUE) {
+               if (value_kind & MONO_UNSIGNED_VALUE_FLAG) {
+                       if (range->lower < 0) {
+                               range->lower = 0;
+                       }
+                       if ((value_kind & MONO_INTEGER_VALUE_SIZE_BITMASK) == 1) {
+                               if (range->upper > 0xff) {
+                                       range->upper = 0xff;
                                }
-                               for (variable_related_to_related_variable = 0; variable_related_to_related_variable < evaluation_area->cfg->num_varinfo; variable_related_to_related_variable++) {
-                                       unsigned char relation_of_variable = related_relations->relations_with_variables [variable_related_to_related_variable];
-                                       unsigned char relation_with_other_variable = relations->relations_with_variables [variable_related_to_related_variable];
-                                       unsigned char new_relation_with_other_variable = PROPAGATED_RELATION (relation_with_variable, relation_of_variable);
-                                       if (RELATION_ADDS_INFORMATION (relation_with_other_variable, new_relation_with_other_variable)) {
-                                               if (TRACE_ABC_REMOVAL) {
-                                                       printf ("RELATION_ADDS_INFORMATION variable %d, related_variable %d, variable_related_to_related_variable %d, ",
-                                                               variable, related_variable, variable_related_to_related_variable);
-                                                       print_relation (relation_with_variable);
-                                                       printf (" - ");
-                                                       print_relation (new_relation_with_other_variable);
-                                                       printf (" => ");
-                                               }
-                                               relations->relations_with_variables [variable_related_to_related_variable] &= new_relation_with_other_variable;
-                                               if (TRACE_ABC_REMOVAL) {
-                                                       print_relation (relations->relations_with_variables [variable_related_to_related_variable]);
-                                                       printf ("\n");
-                                               }
-                                               changes++;
-                                       }
+                       } else if ((value_kind & MONO_INTEGER_VALUE_SIZE_BITMASK) == 2) {
+                               if (range->upper > 0xffff) {
+                                       range->upper = 0xffff;
+                               }
+                       }
+               } else {
+                       if ((value_kind & MONO_INTEGER_VALUE_SIZE_BITMASK) == 1) {
+                               if (range->lower < -0x80) {
+                                       range->lower = -0x80;
+                               }
+                               if (range->upper > 0x7f) {
+                                       range->upper = 0x7f;
+                               }
+                       } else if ((value_kind & MONO_INTEGER_VALUE_SIZE_BITMASK) == 2) {
+                               if (range->lower < -0x8000) {
+                                       range->lower = -0x8000;
+                               }
+                               if (range->upper > 0x7fff) {
+                                       range->upper = 0x7fff;
                                }
                        }
                }
        }
-       return changes;
 }
 
+/*
+ * Attempt the removal of bounds checks from a MonoInst.
+ * inst: the MonoInst
+ * area: the current evaluation area (it contains the relation graph and
+ *       memory for all the evaluation contexts is already allocated)
+ */
 static void
-remove_abc_from_inst (MonoInst *inst, MonoVariableRelationsEvaluationArea *evaluation_area) {
+remove_abc_from_inst (MonoInst *inst, MonoVariableRelationsEvaluationArea *area) {
        if (inst->opcode == CEE_LDELEMA) {
                MonoInst *array_inst = inst->inst_left;
                MonoInst *index_inst = inst->inst_right;
-               /* Both the array and the index must be local variables */
-               if ((array_inst->opcode == CEE_LDIND_REF) &&
-                               ((array_inst->inst_left->opcode == OP_LOCAL)||(array_inst->inst_left->opcode == OP_ARG)) &&
-                               ((index_inst->opcode == CEE_LDIND_I1) ||
-                               (index_inst->opcode == CEE_LDIND_U1) ||
-                               (index_inst->opcode == CEE_LDIND_I2) ||
-                               (index_inst->opcode == CEE_LDIND_U2) ||
-                               (index_inst->opcode == CEE_LDIND_I4) ||
-                               (index_inst->opcode == CEE_LDIND_U4))&&
-                               ((index_inst->inst_left->opcode == OP_LOCAL)||(index_inst->inst_left->opcode == OP_ARG))) {
-                       gssize array_variable = array_inst->inst_left->inst_c0;
-                       gssize index_variable = index_inst->inst_left->inst_c0;
-                       MonoVariableRelations *index_relations = &(evaluation_area->variable_relations [index_variable]);
-                       if ( (! (index_relations->relation_with_zero & ~MONO_GE_RELATION)) && 
-                                       (! (index_relations->relations_with_variables [array_variable] & ~MONO_LT_RELATION)) ) {
-                               inst->flags |= (MONO_INST_NORANGECHECK);
-                       }
-                       if (TRACE_ABC_REMOVAL) {
-                               if (! (index_relations->relation_with_zero & ~MONO_GE_RELATION)) {
-                                       printf ("ARRAY-ACCESS: Removed lower bound check on array %d with index %d\n", array_variable, index_variable);
-                               } else {
-                                       printf ("ARRAY-ACCESS: Left lower bound check on array %d with index %d\n", array_variable, index_variable);
+               MonoSummarizedValue array_value;
+               MonoSummarizedValue index_value;
+               MonoIntegerValueKind index_value_kind;
+               
+               /* First of all, examine the CEE_LDELEMA operands */
+               summarize_array_value (area, array_inst, &array_value, TRUE);
+               index_value_kind = summarize_integer_value (area, index_inst, &index_value, MONO_UNKNOWN_INTEGER_VALUE);
+               
+               /* If the array is a local variable... */
+               if (array_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) {
+                       int array_variable = array_value.value.variable.variable;
+                       MonoRelationsEvaluationContext *array_context = &(area->contexts [array_variable]);
+                       
+                       if (index_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) {
+                               // The easiest case: we just evaluate the array length, to see if it has some relation
+                               // with the index constant, and act accordingly
+                               
+                               clean_contexts (area->contexts, area->cfg->num_varinfo);
+                               evaluate_relation_with_target_variable (area, array_variable, array_variable, NULL);
+                               
+                               if ((index_value.value.constant.value >= 0) && (index_value.value.constant.value < array_context->ranges.zero.lower)) {
+                                       if (REPORT_ABC_REMOVAL) {
+                                               printf ("ARRAY-ACCESS: removed bounds check on array %d with constant index %d in method %s\n",
+                                                               array_variable, index_value.value.constant.value, mono_method_full_name (area->cfg->method, TRUE));
+                                       }
+                                       inst->flags |= (MONO_INST_NORANGECHECK);
                                }
-                               if (! (index_relations->relations_with_variables [array_variable] & ~MONO_LT_RELATION)) {
-                                       printf ("ARRAY-ACCESS: Removed upper bound check on array %d with index %d\n", array_variable, index_variable);
-                               } else {
-                                       printf ("ARRAY-ACCESS: Left upper bound check on array %d with index %d\n", array_variable, index_variable);
+                       } else if (index_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) {
+                               // The common case: we must evaluate both the index and the array length, and check for relevant
+                               // relations both through variable definitions and as constant definitions
+                               
+                               int index_variable = index_value.value.variable.variable;
+                               MonoRelationsEvaluationContext *index_context = &(area->contexts [index_variable]);
+                               
+                               clean_contexts (area->contexts, area->cfg->num_varinfo);
+                               
+                               evaluate_relation_with_target_variable (area, index_variable, array_variable, NULL);
+                               evaluate_relation_with_target_variable (area, array_variable, array_variable, NULL);
+                               
+                               MONO_SUB_DELTA_SAFELY_FROM_RANGES (index_context->ranges, index_value.value.variable.delta);
+                               /* Apply index value kind */
+                               apply_value_kind_to_range (&(index_context->ranges.zero), index_value_kind);
+                               
+                               if (index_context->ranges.zero.lower >= 0) {
+                                       if (TRACE_ABC_REMOVAL) {
+                                               printf ("ARRAY-ACCESS: Removed lower bound check on array %d with index %d\n", array_variable, index_variable);
+                                       }
+                                       if ((index_context->ranges.variable.upper < 0)||(index_context->ranges.zero.upper < array_context->ranges.zero.lower)) {
+                                               if (REPORT_ABC_REMOVAL) {
+                                                       printf ("ARRAY-ACCESS: removed bounds check on array %d with index %d in method %s\n",
+                                                                       array_variable, index_variable, mono_method_full_name (area->cfg->method, TRUE));
+                                               }
+                                               inst->flags |= (MONO_INST_NORANGECHECK);
+                                       }
+                               }
+                               if (TRACE_ABC_REMOVAL) {
+                                       if (index_context->ranges.variable.upper < 0) {
+                                               printf ("ARRAY-ACCESS: Removed upper bound check (through variable) on array %d with index %d\n", array_variable, index_variable);
+                                       }
+                                       if (index_context->ranges.zero.upper < array_context->ranges.zero.lower) {
+                                               printf ("ARRAY-ACCESS: Removed upper bound check (through constant) on array %d with index %d\n", array_variable, index_variable);
+                                       }
                                }
                        }
-                       if (REPORT_ABC_REMOVAL) {
-                               if (inst->flags & (MONO_INST_NORANGECHECK)) {
-                                       printf ("ARRAY-ACCESS: removed bounds check on array %d with index %d in method %s\n",
-                                               array_variable, index_variable, mono_method_full_name (evaluation_area->cfg->method, TRUE));
+               } else if (array_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) {
+                       if (index_value.type == MONO_CONSTANT_SUMMARIZED_VALUE) {
+                               /* The easiest possible case: constant with constant */
+                               if ((index_value.value.constant.value >= 0) && (index_value.value.constant.value < array_value.value.constant.value)) {
+                                       if (REPORT_ABC_REMOVAL) {
+                                               printf ("ARRAY-ACCESS: removed bounds check on array of constant length %d with constant index %d in method %s\n",
+                                                               array_value.value.constant.value, index_value.value.constant.value, mono_method_full_name (area->cfg->method, TRUE));
+                                       }
+                                       inst->flags |= (MONO_INST_NORANGECHECK);
+                               }
+                       } else if (index_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) {
+                               /* The index has a variable related value, which must be evaluated */
+                               int index_variable = index_value.value.variable.variable;
+                               MonoRelationsEvaluationContext *index_context = &(area->contexts [index_variable]);
+                               
+                               clean_contexts (area->contexts, area->cfg->num_varinfo);
+                               evaluate_relation_with_target_variable (area, index_variable, index_variable, NULL);
+                               /* Apply index value kind */
+                               apply_value_kind_to_range (&(index_context->ranges.zero), index_value_kind);
+                               
+                               if ((index_context->ranges.zero.lower >= 0) && (index_context->ranges.zero.upper < array_value.value.constant.value)) {
+                                       if (REPORT_ABC_REMOVAL) {
+                                               printf ("ARRAY-ACCESS: removed bounds check on array of constant length %d with index %d ranging from %d to %d in method %s\n",
+                                                               array_value.value.constant.value, index_variable, index_context->ranges.zero.lower, index_context->ranges.zero.upper, mono_method_full_name (area->cfg->method, TRUE));
+                                       }
+                                       inst->flags |= (MONO_INST_NORANGECHECK);
+                               }
+                       } else if (index_value_kind != MONO_UNKNOWN_INTEGER_VALUE) {
+                               /* The index has an unknown but bounded value */
+                               MonoRelationsEvaluationRange range;
+                               MONO_MAKE_RELATIONS_EVALUATION_RANGE_WEAK (range);
+                               apply_value_kind_to_range (&range, index_value_kind);
+                               
+                               if ((range.lower >= 0) && (range.upper < array_value.value.constant.value)) {
+                                       if (REPORT_ABC_REMOVAL) {
+                                               printf ("ARRAY-ACCESS: removed bounds check on array of constant length %d with unknown index ranging from %d to %d in method %s\n",
+                                                               array_value.value.constant.value, range.lower, range.upper, mono_method_full_name (area->cfg->method, TRUE));
+                                       }
+                                       inst->flags |= (MONO_INST_NORANGECHECK);
                                }
                        }
                }
        }
-       
+}
+
+/*
+ * Recursively scan a tree of MonoInst looking for array accesses.
+ * inst: the root of the MonoInst tree
+ * area: the current evaluation area (it contains the relation graph and
+ *       memory for all the evaluation contexts is already allocated)
+ */
+static void
+process_inst (MonoInst *inst, MonoVariableRelationsEvaluationArea *area) {
+       if (inst->opcode == CEE_LDELEMA) { /* Handle OP_LDELEMA2D, too */
+               if (TRACE_ABC_REMOVAL) {
+                       printf ("Attempting check removal...\n");
+               }
+               
+               remove_abc_from_inst (inst, area);
+       }
+
        if (mono_burg_arity [inst->opcode]) {
-               remove_abc_from_inst (inst->inst_left, evaluation_area);
+               process_inst (inst->inst_left, area);
                if (mono_burg_arity [inst->opcode] > 1) {
-                       remove_abc_from_inst (inst->inst_right, evaluation_area);
+                       process_inst (inst->inst_right, area);
                }
        }
 }
 
+
+
+
+/*
+ * Process a BB removing bounds checks from array accesses.
+ * It does the following (in sequence):
+ * - Get the BB entry condition
+ * - Add its relations to the relation graph in the evaluation area
+ * - Process all the MonoInst trees in the BB
+ * - Recursively process all the children BBs in the dominator tree
+ * - Remove the relations previously added to the relation graph
+ *
+ * bb: the BB that must be processed
+ * area: the current evaluation area (it contains the relation graph and
+ *       memory for all the evaluation contexts is already allocated)
+ */
 static void
-remove_abc_from_block (MonoSummarizedBasicBlock *b, MonoVariableRelationsEvaluationArea *evaluation_area) {
-       int i;
-       int changes;
-       MonoBasicBlock *bb;
-       MonoInst *current_inst = b->block->code;
+process_block (MonoBasicBlock *bb, MonoVariableRelationsEvaluationArea *area) {
+       int inst_index;
+       MonoInst *current_inst;
+       MonoAdditionalVariableRelationsForBB additional_relations;
+       GSList *dominated_bb;
        
        if (TRACE_ABC_REMOVAL) {
-               printf ("Working on block %d [dfn %d], has_array_access_instructions is %d\n",
-                       b->block->block_num, b->block->dfn, b->has_array_access_instructions);
+               printf ("Processing block %d [dfn %d]...\n", bb->block_num, bb->dfn);
        }
        
-       if (b->has_array_access_instructions) {
-               for (i = 0; i < evaluation_area->cfg->num_varinfo; i++) {
-                       evaluation_area->variable_relations [i].evaluation_step = MONO_RELATIONS_EVALUATION_NOT_STARTED;
-                       evaluation_area->variable_relations [i].definition_is_recursive = 0;
-                       SET_VARIABLE_RELATIONS (&(evaluation_area->variable_relations [i]), MONO_ANY_RELATION, evaluation_area->cfg->num_varinfo);
-               }
-               
-               bb = b->block;
-               while (bb != NULL) {
-                       /* Walk up dominators tree to put conditions in area */
-                       int in_index = 0;
-                       /* for (in_index = 0; in_index < bb->in_count; in_index++) { */
-                       if (bb->in_count == 1) { /* Should write the code to "sum" conditions... */
-                               int out_index;
-                               MonoBasicBlock *in_bb = bb->in_bb [in_index];
-                               MonoSummarizedBasicBlock *in_b = &(evaluation_area->blocks [in_bb->dfn]);
-                               for (out_index = 0; out_index < in_b->number_of_branches; out_index++) {
-                                       if (in_b->branches [out_index].destination_block == bb) {
-                                               MonoBranchData *branch;
-                                               int condition_index;
-                                               if (TRACE_ABC_REMOVAL) {
-                                                       printf ("Applying conditions of branch %d -> %d\n", in_b->block->block_num, bb->block_num);
-                                               }
-                                               branch = &(in_b->branches [out_index]);
-                                               for (condition_index = 0; condition_index < branch->number_of_conditions; condition_index++) {
-                                                       MonoBranchCondition *condition = &(branch->conditions [condition_index]);
-                                                       MonoVariableRelations *relations = &(evaluation_area->variable_relations [condition->variable]);
-                                                       switch (condition->value.value_type) {
-                                                               case MONO_CONSTANT_SUMMARIZED_VALUE: {
-                                                                       if (condition->value.relation_with_value == MONO_EQ_RELATION) {
-                                                                               relations->relation_with_zero &= RELATION_BETWEEN_VALUES (condition->value.value.constant, 0);
-                                                                               relations->relation_with_one &= RELATION_BETWEEN_VALUES (abs (condition->value.value.constant), 1);
-                                                                               if (TRACE_ABC_REMOVAL) {
-                                                                                       printf ("Applied equality condition with constant to variable %d; relatrion with 0: ", condition->variable);
-                                                                                       print_relation (relations->relation_with_zero);
-                                                                                       printf ("\n");
-                                                                               }
-                                                                       } else if (condition->value.value.constant == 0) {
-                                                                               relations->relation_with_zero &= condition->value.relation_with_value;
-                                                                               if (TRACE_ABC_REMOVAL) {
-                                                                                       printf ("Applied relation with 0 to variable %d: ", condition->variable);
-                                                                                       print_relation (relations->relation_with_zero);
-                                                                                       printf ("\n");
-                                                                               }
-                                                                       }
-                                                                       /* Other cases should be handled */
-                                                                       break;
-                                                               }
-                                                               case MONO_VARIABLE_SUMMARIZED_VALUE: {
-                                                                       relations->relations_with_variables [condition->value.value.variable] &= condition->value.relation_with_value;
-                                                                       if (TRACE_ABC_REMOVAL) {
-                                                                               printf ("Applied relation between variables %d and %d: ", condition->variable, condition->value.value.variable);
-                                                                               print_relation (relations->relations_with_variables [condition->value.value.variable]);
-                                                                               printf ("\n");
-                                                                       }
-                                                                       break;
-                                                               }
-                                                               default:
-                                                                       g_assert_not_reached (); /* PHIs are not OK here */
-                                                       }
-                                               }
-                                       }
-                               }
-                       }
-                       bb = bb->idom;
-               }
-               
-               if (TRACE_ABC_REMOVAL) {
-                       printf ("Branch conditions applied... ");
-                       print_all_variable_relations (evaluation_area);
-               }
-               
-               for (i = 0; i < evaluation_area->cfg->num_varinfo; i++) {
-                       evaluate_variable_relations (i, evaluation_area, NULL);
+       get_relations_from_previous_bb (area, bb, &additional_relations);
+       if (TRACE_ABC_REMOVAL) {
+               if (additional_relations.relation1.relation.relation != MONO_ANY_RELATION) {
+                       printf ("Adding relation 1 on variable %d: ", additional_relations.relation1.variable);
+                       print_summarized_value_relation (&(additional_relations.relation1.relation));
+                       printf ("\n");
                }
-               
-               if (TRACE_ABC_REMOVAL) {
-                       printf ("Variable definitions applied... ");
-                       print_all_variable_relations (evaluation_area);
+               if (additional_relations.relation2.relation.relation != MONO_ANY_RELATION) {
+                       printf ("Adding relation 2 on variable %d: ", additional_relations.relation2.variable);
+                       print_summarized_value_relation (&(additional_relations.relation2.relation));
+                       printf ("\n");
                }
-               
-               i = 0;
-               do {
-                       changes = propagate_relations (evaluation_area);
-                       i++;
-                       if (TRACE_ABC_REMOVAL) {
-                               printf ("Propagated %d changes\n", changes);
-                       }
-               } while ((changes > 0) && (i < evaluation_area->cfg->num_varinfo));
-               
+       }
+       apply_change_to_evaluation_area (area, &(additional_relations.relation1));
+       apply_change_to_evaluation_area (area, &(additional_relations.relation2));
+       
+       inst_index = 0;
+       MONO_BB_FOR_EACH_INS (bb, current_inst) {
                if (TRACE_ABC_REMOVAL) {
-                       printf ("Relations fully propagated... ");
-                       print_all_variable_relations (evaluation_area);
+                       printf ("Processing instruction %d\n", inst_index);
+                       inst_index++;
                }
                
-               /* Area is ready, look for array access instructions */
-               if (TRACE_ABC_REMOVAL) {
-                       printf ("Going after array accesses...\n");
-               }
-               while (current_inst != NULL) {
-                       remove_abc_from_inst (current_inst, evaluation_area);
-                       current_inst = current_inst->next;
-               }
+               process_inst (current_inst, area);
+       }
+       
+       
+       if (TRACE_ABC_REMOVAL) {
+               printf ("Processing block %d [dfn %d] done.\n", bb->block_num, bb->dfn);
        }
+       
+       for (dominated_bb = bb->dominated; dominated_bb != NULL; dominated_bb = dominated_bb->next) {
+               process_block ((MonoBasicBlock*) (dominated_bb->data), area);
+       }
+       
+       remove_change_from_evaluation_area (&(additional_relations.relation1));
+       remove_change_from_evaluation_area (&(additional_relations.relation2));
 }
 
+
+
+/**
+ * mono_perform_abc_removal:
+ * @cfg: Control Flow Graph
+ *
+ * Performs the ABC removal from a cfg in SSA form.
+ * It does the following:
+ * - Prepare the evaluation area
+ * - Allocate memory for the relation graph in the evaluation area
+ *   (of course, only for variable definitions) and summarize there all
+ *   variable definitions
+ * - Allocate memory for the evaluation contexts in the evaluation area
+ * - Recursively process all the BBs in the dominator tree (it is enough
+ *   to invoke the processing on the entry BB)
+ * 
+ * cfg: the method code
+ */
 void
 mono_perform_abc_removal (MonoCompile *cfg)
 {
-       MonoVariableRelationsEvaluationArea evaluation_area;
+       MonoVariableRelationsEvaluationArea area;
        int i;
-       verbose_level = cfg->verbose_level;
        
+       verbose_level = cfg->verbose_level;
        
        if (TRACE_ABC_REMOVAL) {
                printf ("Removing array bound checks in %s\n", mono_method_full_name (cfg->method, TRUE));
        }
        
-       if (cfg->num_varinfo > 250) {
-               if (TRACE_ABC_REMOVAL) {
-                       printf ("Too many variables (%d), giving up...\n", cfg->num_varinfo);
-               }
-               return;
-       }
-       
-       evaluation_area.pool = mono_mempool_new ();
-       evaluation_area.cfg = cfg;
-       evaluation_area.variable_relations = (MonoVariableRelations *)
-               mono_mempool_alloc (evaluation_area.pool, sizeof (MonoVariableRelations) * (cfg->num_varinfo));
-       //printf ("Allocated %d bytes for %d variable relations at pointer %p\n",
-       //      sizeof (MonoVariableRelations) * (cfg->num_varinfo), (cfg->num_varinfo), evaluation_area.variable_relations);
-       for (i = 0; i < cfg->num_varinfo; i++ ) {
-               evaluation_area.variable_relations [i].relations_with_variables = (unsigned char *)
-                       mono_mempool_alloc (evaluation_area.pool, (cfg->num_varinfo));
-               //printf ("Allocated %d bytes [%d] at pointer %p\n",
-               //      cfg->num_varinfo, i, evaluation_area.variable_relations [i].relations_with_variables);
-       }
-       evaluation_area.variable_definitions = (MonoSummarizedValue *)
-               mono_mempool_alloc (evaluation_area.pool, sizeof (MonoSummarizedValue) * (cfg->num_varinfo));
-       //printf ("Allocated %d bytes for %d variable definitions at pointer %p\n",
-       //      sizeof (MonoSummarizedValue) * (cfg->num_varinfo), (cfg->num_varinfo), evaluation_area.variable_definitions);
-       if (TRACE_ABC_REMOVAL) {
-               printf ("Method contains %d variables\n", i);
-       }
+       area.cfg = cfg;
+       area.relations = (MonoSummarizedValueRelation *)
+               mono_mempool_alloc (cfg->mempool, sizeof (MonoSummarizedValueRelation) * (cfg->num_varinfo) * 2);
+       area.contexts = (MonoRelationsEvaluationContext *)
+               mono_mempool_alloc (cfg->mempool, sizeof (MonoRelationsEvaluationContext) * (cfg->num_varinfo));
+       area.variable_value_kind = (MonoIntegerValueKind *)
+               mono_mempool_alloc (cfg->mempool, sizeof (MonoIntegerValueKind) * (cfg->num_varinfo));
        for (i = 0; i < cfg->num_varinfo; i++) {
-               if (cfg->vars [i]->def != NULL) {
-                       MonoInst *value = get_variable_value_from_ssa_store (cfg->vars [i]->def, i);
+               area.variable_value_kind [i] = MONO_UNKNOWN_INTEGER_VALUE;
+               area.relations [i].relation = MONO_EQ_RELATION;
+               area.relations [i].relation_is_static_definition = TRUE;
+               area.relations [i].next = NULL;
+               if (MONO_VARINFO (cfg, i)->def != NULL) {
+                       MonoInst *value = get_variable_value_from_store_instruction (MONO_VARINFO (cfg, i)->def, i);
                        if (value != NULL) {
-                               summarize_value (value, evaluation_area.variable_definitions + i);
-                               if (TRACE_ABC_REMOVAL) {
-                                       printf ("Summarized variable %d\n", i);
-                                       print_summarized_value (evaluation_area.variable_definitions + i);
+                               gboolean is_array_type;
+                               MonoIntegerValueKind effective_value_kind;
+                               MonoRelationsEvaluationRange range;
+                               MonoSummarizedValueRelation *type_relation;
+                               
+                               switch (cfg->varinfo [i]->inst_vtype->type) {
+                               case MONO_TYPE_ARRAY:
+                               case MONO_TYPE_SZARRAY:
+                                       is_array_type = TRUE;
+                                       goto handle_array_value;
+                               case MONO_TYPE_OBJECT:
+                                       is_array_type = FALSE;
+handle_array_value:
+                                       summarize_array_value (&area, value, &(area.relations [i].related_value), is_array_type);
+                                       if (TRACE_ABC_REMOVAL) {
+                                               printf ("Summarized variable %d as array (is_array_type = %s): ", i, (is_array_type?"TRUE":"FALSE"));
+                                               print_summarized_value (&(area.relations [i].related_value));
+                                               printf ("\n");
+                                       }
+                                       break;
+                               case MONO_TYPE_I1:
+                                       area.variable_value_kind [i] = MONO_INTEGER_VALUE_SIZE_1;
+                                       goto handle_integer_value;
+                               case MONO_TYPE_U1:
+                                       area.variable_value_kind [i] = MONO_UNSIGNED_INTEGER_VALUE_SIZE_1;
+                                       goto handle_integer_value;
+                               case MONO_TYPE_I2:
+                                       area.variable_value_kind [i] = MONO_INTEGER_VALUE_SIZE_2;
+                                       goto handle_integer_value;
+                               case MONO_TYPE_U2:
+                                       area.variable_value_kind [i] = MONO_UNSIGNED_INTEGER_VALUE_SIZE_2;
+                                       goto handle_integer_value;
+                               case MONO_TYPE_I4:
+                                       area.variable_value_kind [i] = MONO_INTEGER_VALUE_SIZE_4;
+                                       goto handle_integer_value;
+                               case MONO_TYPE_U4:
+                                       area.variable_value_kind [i] = MONO_UNSIGNED_INTEGER_VALUE_SIZE_4;
+                                       goto handle_integer_value;
+                               case MONO_TYPE_I:
+                                       area.variable_value_kind [i] = SIZEOF_VOID_P;
+                                       goto handle_integer_value;
+                               case MONO_TYPE_U:
+                                       area.variable_value_kind [i] = (MONO_UNSIGNED_VALUE_FLAG|SIZEOF_VOID_P);
+                                       goto handle_integer_value;
+                               case MONO_TYPE_I8:
+                                       area.variable_value_kind [i] = MONO_INTEGER_VALUE_SIZE_8;
+                                       goto handle_integer_value;
+                               case MONO_TYPE_U8:
+                                       area.variable_value_kind [i] = MONO_UNSIGNED_INTEGER_VALUE_SIZE_8;
+handle_integer_value:
+                                       effective_value_kind = summarize_integer_value (&area, value, &(area.relations [i].related_value), area.variable_value_kind [i]);
+                                       MONO_MAKE_RELATIONS_EVALUATION_RANGE_WEAK (range);
+                                       apply_value_kind_to_range (&range, area.variable_value_kind [i]);
+                                       apply_value_kind_to_range (&range, effective_value_kind);
+                                       
+                                       if (range.upper < INT_MAX) {
+                                               type_relation = (MonoSummarizedValueRelation *) mono_mempool_alloc (cfg->mempool, sizeof (MonoSummarizedValueRelation));
+                                               type_relation->relation = MONO_LE_RELATION;
+                                               type_relation->related_value.type = MONO_CONSTANT_SUMMARIZED_VALUE;
+                                               type_relation->related_value.value.constant.value = range.upper;
+                                               type_relation->relation_is_static_definition = TRUE;
+                                               type_relation->next = area.relations [i].next;
+                                               area.relations [i].next = type_relation;
+                                               if (TRACE_ABC_REMOVAL) {
+                                                       printf ("[var%d <= %d]", i, range.upper);
+                                               }
+                                       }
+                                       if (range.lower > INT_MIN) {
+                                               type_relation = (MonoSummarizedValueRelation *) mono_mempool_alloc (cfg->mempool, sizeof (MonoSummarizedValueRelation));
+                                               type_relation->relation = MONO_GE_RELATION;
+                                               type_relation->related_value.type = MONO_CONSTANT_SUMMARIZED_VALUE;
+                                               type_relation->related_value.value.constant.value = range.lower;
+                                               type_relation->relation_is_static_definition = TRUE;
+                                               type_relation->next = area.relations [i].next;
+                                               area.relations [i].next = type_relation;
+                                               if (TRACE_ABC_REMOVAL) {
+                                                       printf ("[var%d >= %d]", i, range.lower);
+                                               }
+                                       }
+                                       if (TRACE_ABC_REMOVAL) {
+                                               printf ("Summarized variable %d: ", i);
+                                               print_summarized_value (&(area.relations [i].related_value));
+                                               printf ("\n");
+                                       }
+                                       break;
+                               default:
+                                       MAKE_VALUE_ANY (area.relations [i].related_value);
+                                       if (TRACE_ABC_REMOVAL) {
+                                               printf ("Variable %d not handled (type %d)\n", i, cfg->varinfo [i]->inst_vtype->type);
+                                       }
                                }
                        } else {
-                               MAKE_VALUE_ANY (evaluation_area.variable_definitions + i);
+                               MAKE_VALUE_ANY (area.relations [i].related_value);
                                if (TRACE_ABC_REMOVAL) {
                                        printf ("Definition of variable %d is not a proper store\n", i);
                                }
                        }
                } else {
-                       MAKE_VALUE_ANY (evaluation_area.variable_definitions + i);
+                       MAKE_VALUE_ANY (area.relations [i].related_value);
                        if (TRACE_ABC_REMOVAL) {
                                printf ("Variable %d has no definition, probably it is an argument\n", i);
-                               print_summarized_value (evaluation_area.variable_definitions + i);
                        }
                }
        }
-       
-       evaluation_area.blocks = (MonoSummarizedBasicBlock *)
-               mono_mempool_alloc (evaluation_area.pool, sizeof (MonoSummarizedBasicBlock) * (cfg->num_bblocks));
-       //printf ("Allocated %d bytes for %d blocks at pointer %p\n",
-       //      sizeof (MonoSummarizedBasicBlock) * (cfg->num_bblocks), (cfg->num_bblocks), evaluation_area.blocks);
-       
-       for (i = 0; i < cfg->num_bblocks; i++) {
-               analyze_block (cfg->bblocks [i], &evaluation_area);
-       }
-       
-       for (i = 0; i < cfg->num_bblocks; i++) {
-               remove_abc_from_block (&(evaluation_area.blocks [i]), &evaluation_area);
-       }
-       
-       mono_mempool_destroy (evaluation_area.pool);
-}
-
-#else
-static void remove_abc (MonoInst *inst) {
-       if (inst->opcode == CEE_LDELEMA) {
-               if (TRACE_ABC_REMOVAL||REPORT_ABC_REMOVAL) {
-                       printf ("Performing removal...\n");
+       for (i = 0; i < cfg->num_varinfo; i++) {
+               if (area.relations [i].related_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) {
+                       int related_index = cfg->num_varinfo + i;
+                       int related_variable = area.relations [i].related_value.value.variable.variable;
+                       
+                       area.relations [related_index].relation = MONO_EQ_RELATION;
+                       area.relations [related_index].relation_is_static_definition = TRUE;
+                       area.relations [related_index].related_value.type = MONO_VARIABLE_SUMMARIZED_VALUE;
+                       area.relations [related_index].related_value.value.variable.variable = i;
+                       area.relations [related_index].related_value.value.variable.delta = - area.relations [i].related_value.value.variable.delta;
+                       
+                       area.relations [related_index].next = area.relations [related_variable].next;
+                       area.relations [related_variable].next = &(area.relations [related_index]);
+                       
+                       if (TRACE_ABC_REMOVAL) {
+                               printf ("Added symmetric summarized value for variable variable %d (to %d): ", i, related_variable);
+                               print_summarized_value (&(area.relations [related_index].related_value));
+                               printf ("\n");
+                       }
                }
-               inst->flags |= (MONO_INST_NORANGECHECK);
        }
        
-       if (mono_burg_arity [inst->opcode]) {
-               remove_abc (inst->inst_left);
-               if (mono_burg_arity [inst->opcode] > 1) {
-                       remove_abc (inst->inst_right);
-               }
-       }
+       process_block (cfg->bblocks [0], &area);
 }
 
-void
-mono_perform_abc_removal (MonoCompile *cfg) {
-       verbose_level = cfg->verbose_level;
-       
-       int i;
-       #if (TRACE_ABC_REMOVAL)
-       printf ("Removing array bound checks in %s\n", mono_method_full_name (cfg->method, TRUE));
-       #endif
-       
-       for (i = 0; i < cfg->num_bblocks; i++) {
-               #if (TRACE_ABC_REMOVAL)
-               printf ("  Working on block %d [dfn %d]\n", cfg->bblocks [i]->block_num, i);
-               #endif
-               
-               MonoBasicBlock *bb = cfg->bblocks [i];
-               MonoInst *inst = bb->code;
-               while (inst != NULL) {
-                       remove_abc (inst);
-                       inst = inst->next;
-               }
-       }
-}
-#endif
+#endif /* DISABLE_SSA */
+