update barvinok for conversion to isl code generator

[ppn.git] / domain.cc

#include "suif_inc.h"
#include <algorithm>
#include <sstream>
#include "domain.h"

const char * k_static_root;
const char * k_stmt;
const char * k_if_annote;
const char * k_domain_symtab;
const char * k_iteration_domain;
const char *k_for_annote;
const char *k_array_bounds;
const char *k_set_in_scope;

void symtab_ann::add_var(var_sym *var)
{
    if (vars.find(var) == vars.end())
        vars[var] = new Param_Iterator(var->name());
}

void symtab_ann::add_var(named_lin_ineq *nlq)
{
        if (!nlq)
                return;
        for (int i = 1; i < nlq->n(); ++i)
                add_var(nlq->names()[i].var());
}

var_sym *symtab_ann::create_tmp()
{
        var_sym *tmp = symtab->new_unique_var(type_signed);
        add_var(tmp);
        vars[tmp]->temp = true;
        return tmp;
}

void
domain_constructor::recurse(tree_node * tn)
{
    unsigned n = tn->num_child_lists();
    for (unsigned i = 0; i < n; ++i)
        construct(tn->child_list_num(i));
}

SRelation * domain_constructor::reorder(SRelation * c)
{
    Relation r = copy(*(Relation*)c);
    r = Extend_Set(r, level);
    for (int i = 0; i < level; ++i) {
        EQ_Handle e = r.and_with_EQ();
        e.update_coef(r.get_local(sa->vars[its[i]]), -1);
        e.update_coef(r.set_var(i+1), 1);
        r = Project(r, sa->vars[its[i]]);
    }
    return new SRelation(r, sa);
}

/* Replace c, with only named constraints, by an actual
 * map from the iterators and nested accesses to the array dimensions.
 *
 * Each of the input and output dimensions is equated to the
 * corresponding parameter in c.
 *
 * output is the number of output variables (array dimensions)
 */
SRelation *domain_constructor::reorder(SRelation *c,
        const std::vector<var_sym *> &nested_vars, int output)
{
        Relation r = copy(*(Relation*)c);
        r = Extend_Domain(r, level + nested_vars.size());
        r = Extend_Range(r, output);

        for (int i = 0; i < level; ++i) {
                EQ_Handle e = r.and_with_EQ();
                e.update_coef(r.get_local(sa->vars[its[i]]), -1);
                e.update_coef(r.input_var(1 + i), 1);
                r = Project(r, sa->vars[its[i]]);
        }

        for (int i = 0; i < nested_vars.size(); ++i) {
                EQ_Handle e = r.and_with_EQ();
                e.update_coef(r.get_local(sa->vars[nested_vars[i]]), -1);
                e.update_coef(r.input_var(1 + level + i), 1);
                r = Project(r, sa->vars[nested_vars[i]]);
        }

        for (int i = 0; i < output; ++i) {
                EQ_Handle e = r.and_with_EQ();
                e.update_coef(r.get_local(sa->vars[out[i]]), -1);
                e.update_coef(r.output_var(1 + i), 1);
                r = Project(r, sa->vars[out[i]]);
        }

        SRelation *s = new SRelation(r, sa, c->nested);
        delete c;

        return s;
}

/* In the process of extracting a messy index, update the equality
 * encoded in the first two inequalities of "nli" with
 * "f" times the result of the expression "in".
 *
 * If "in" represents an array access, then the access is added
 * to "nested" and a new variable and a new column are constructed
 * that correspond to this nested access.
 *
 * If "in" represents an integer division "d = f/m", with m a constant,
 * then we first construct a relation for d = f.  The first two rows
 * then contain
 *                      -d + f >= 0
 *                       d - f >= 0
 * These are updated to
 *                      -m d + f >= 0
 *                       m d - f + m - 1 >= 0
 *
 * i.e.,
 *                      m d <= f <= m d + m - 1
 *
 * Finally, the original equality is updated with f * d and the above
 * constraints are added to the constraint set.
 */
void domain_constructor::extract_messy_index(SRelation *map,
        Constraint_Handle &h, instruction *in, int f)
{
        switch (in->opcode()) {
        case io_ldc: {
                in_ldc *ins = dynamic_cast<in_ldc *>(in);
                f *= ins->value().integer();
                h.update_const(f);
                break;
        }
        case io_add:
                extract_messy_index(map, h, in->src_op(0), f);
                extract_messy_index(map, h, in->src_op(1), f);
                break;
        case io_sub:
                extract_messy_index(map, h, in->src_op(0), f);
                extract_messy_index(map, h, in->src_op(1), -f);
                break;
        case io_neg:
                extract_messy_index(map, h, in->src_op(0), -f);
                break;
        case io_lod: {
                stmt_node *node;
                operand r = in->src_op(0);
                node = extract_stmt_node(r, false);
                assert(node);
                node->var = sa->create_tmp();
                node->op = r;
                map->nested.push_back(node);
                h.update_coef(map->get_local(sa->vars[node->var]), f);
                break;
        }
        case io_mul: {
                operand op1 = in->src_op(0);
                operand op2 = in->src_op(1);
                if (op1.kind() == OPER_INSTR &&
                    op1.instr()->opcode() == io_ldc) {
                        in_ldc *ins = dynamic_cast<in_ldc *>(op1.instr());
                        f *= ins->value().integer();
                        extract_messy_index(map, h, op2, f);
                        break;
                }
                if (op2.kind() == OPER_INSTR &&
                    op2.instr()->opcode() == io_ldc) {
                        in_ldc *ins = dynamic_cast<in_ldc *>(op2.instr());
                        f *= ins->value().integer();
                        extract_messy_index(map, h, op1, f);
                        break;
                }
                in->print(stderr);
                assert(0);
        }
        case io_div: {
                operand op2 = in->src_op(1);
                assert(op2.kind() == OPER_INSTR &&
                        op2.instr()->opcode() == io_ldc);
                in_ldc *ins = dynamic_cast<in_ldc *>(op2.instr());
                int mod = ins->value().integer();
                assert(mod > 0);

                Variable_ID q = map->e->declare();
                h.update_coef(q, f);

                /* e - m f >= 0 */
                GEQ_Handle g1 = map->f->add_GEQ();
                g1.update_coef(q, -mod);
                extract_messy_index(map, g1, in->src_op(0), 1);

                /* -e + m f + m-1 >= 0 */
                GEQ_Handle g2 = map->f->add_GEQ();
                g2.update_coef(q, mod);
                g2.update_const(mod - 1);
                extract_messy_index(map, g2, in->src_op(0), -1);

                break;
        }
        default:
                in->print(stderr);
                assert(0);
        }
}

static bool data_dependent(var_sym *v, symtab_ann *sa)
{
        return sa->vars.find(v) != sa->vars.end() &&
               sa->vars[v]->assigned && !sa->vars[v]->iterator;
}

/* Return true if any variable in the index expression
 * has been assigned a value and is not currently used as
 * an iterator.
 */
static bool data_dependent(access_vector *av, symtab_ann *sa)
{
        if (av->too_messy)
                return false;
        access_list_iter iter(&av->conregs);
        while (!iter.is_empty()) {
                var_sym *v = (var_sym *)iter.step()->var();
                if (data_dependent(v, sa))
                        return true;
        }
        return false;
}

/* In the process of extracting a messy index, update the equality
 * encoded in the first two inequalities of "nli" with
 * "f" times the value of "op".
 *
 * If "op" is an expression, update the equality with f times the
 * result of the expression.
 * If "op" is a symbol, update the corresponding column in the equality.
 */
void domain_constructor::extract_messy_index(SRelation *map,
        Constraint_Handle &h, operand op, int f)
{
        if (op.is_expr()) {
                extract_messy_index(map, h, op.instr(), f);
                return;
        }

        assert(op.is_symbol());
        assert(!op.symbol()->type()->is_ptr());

        if (data_dependent(op.symbol(), sa)) {
                stmt_node *node;
                node = extract_stmt_node(op, false);
                assert(node);
                node->var = sa->create_tmp();
                node->op = op;
                map->nested.push_back(node);
                h.update_coef(map->get_local(sa->vars[node->var]), f);
        } else {
                sa->add_var(op.symbol());
                h.update_coef(map->get_local(sa->vars[op.symbol()]), f);
        }
}

/* Construct and return an access relation for some kinds of messy
 * indices.  In particular, handle indices with nested array accesses.
 * If anything unexpected appears, we currently just abort.
 * Any nested array access is appended to "nested".
 * "out" is the variable that represents the array index "index"
 * in the returned access relation.
 *
 * The first two rows of the returned named_lin_ineq are two
 * opposite inequalities representing an equality.
 */
SRelation *domain_constructor::extract_messy_index(operand index, var_sym *out)
{
        int pos;

        named_lin_ineq *nli = new named_lin_ineq;
        SRelation *map = new SRelation(sa, nli);
        EQ_Handle g = map->f->add_EQ();
        g.update_coef(map->get_local(sa->vars[out]), -1);
        extract_messy_index(map, g, index, 1);
        return map;
}

stmt_access *domain_constructor::create_access(dep_instr_annote *di, bool write)
{
        instruction *in = di->my_instr;
        assert(in->opcode() == io_array);
        in_array *ina = (in_array *)in;
        assert(ina->base_op().is_instr());
        var_sym *array;
        switch (ina->base_op().instr()->opcode()) {
        case io_ldc: {
                in_ldc *ldc = (in_ldc *) ina->base_op().instr();
                assert(ldc->value().kind() == im_symbol);
                assert(ldc->value().symbol()->kind() == SYM_VAR);
                array = (var_sym *)ldc->value().symbol();
                break;
        }
        case io_cvt: {
                instruction *in = ina->base_op().instr();
                assert(in->src_op(0).kind() == OPER_SYM);
                assert(in->src_op(0).symbol()->kind() == SYM_VAR);
                array = (var_sym *)in->src_op(0).symbol();
                break;
        }
        default:
                assert(0);
        }

        named_lin_ineq *nlq = new named_lin_ineq();
        SRelation *map = new SRelation(sa, nlq);
        array_info_iter iter(di->ai);
        int i;
        for(i = 0; !iter.is_empty(); ++i) {
                if (i >= out.size())
                        out.push_back(sa->create_tmp());

                access_vector * av = iter.step();
                bool messy = av->too_messy || data_dependent(av, sa);
                if (messy && !write) {
                        SRelation *old = map;
                        SRelation *m;
                        m = extract_messy_index(ina->index(i), out[i]);
                        map = map->Intersection(m);
                        delete m;
                        delete old;
                        continue;
                }
                if (messy)
                        in->print();
                assert(!messy);

                /* Treat all non-induction variables in access vector
                 * as parameters.  However, if the variable has
                 * been assigned a value before, then it cannot be
                 * a parameter.
                 */
                access_list_iter iter(&av->conregs);
                while (!iter.is_empty()) {
                        var_sym *v = (var_sym *)iter.step()->var();
                        if (sa->vars.find(v) != sa->vars.end())
                                assert(!sa->vars[v]->assigned ||
                                       sa->vars[v]->iterator);
                        sa->add_var(v);
                }

                map->intersect(named_lin_ineq::mk_named_lin_ineq(*av, out[i],
                                                              FALSE));
                map->intersect(named_lin_ineq::mk_named_lin_ineq(*av, out[i],
                                                              TRUE));
        }

        return new stmt_access(write, map, array, i);
}

/* Returns stmt_access if it's an access already analyzed by SUIF */
stmt_access *domain_constructor::check_access(instruction *in, bool write)
{
        dep_instr_annote *di =
                (dep_instr_annote *)in->peek_annote(k_dep_instr_annote);
        if (!di)
                return NULL;

        return create_access(di, write);
}

/* Is it ok to write to (write = true) or read from (write = false)
 * variable scalar?
 * It is not ok to write to a variable that is currently being used
 * as an iterator.
 * It is also not ok to read from a variable that is not an iterator
 * and that has once been written (making it not a parameter), but
 * that currently does not have a known value (because it has been
 * used as an iterator after the last write).
 */
static bool is_access_ok(symtab_ann *sa, var_sym *scalar, bool write)
{
        Param_Iterator *var = sa->vars[scalar];
        if (write && var->iterator)
                return false;
        if (!write && !var->iterator && !var->valid_for_read)
                return false;
        return true;
}

/* Check whether ct contains any invalid nodes or data dependent
 * accesses.
 * If so, then this condition tree shouldn't be considered as
 * a known value.
 */
static bool invalid_or_data_dependent(condition_tree *ct, symtab_ann *sa)
{
        switch (ct->type) {
        case ctt_invalid:
        case ctt_lod:
                return true;
        case ctt_cst:
                return false;
        case ctt_add:
        case ctt_sub:
                return invalid_or_data_dependent(ct->left, sa) ||
                       invalid_or_data_dependent(ct->right, sa);
        case ctt_mul:
                return invalid_or_data_dependent(ct->right, sa);
        case ctt_neg:
        case ctt_rem:
        case ctt_floord:
                return invalid_or_data_dependent(ct->left, sa);
        case ctt_sym:
                return data_dependent(ct->var, sa);
        }
        assert(0);
}

/* Check whether ct contains any invalid nodes.
 */
static bool invalid(condition_tree *ct, symtab_ann *sa)
{
        switch (ct->type) {
        case ctt_invalid:
                return true;
        case ctt_lod:
        case ctt_cst:
        case ctt_sym:
                return false;
        case ctt_add:
        case ctt_sub:
        case ctt_min:
        case ctt_max:
                return invalid(ct->left, sa) ||
                       invalid(ct->right, sa);
        case ctt_mul:
                return invalid(ct->right, sa);
        case ctt_neg:
        case ctt_rem:
        case ctt_floord:
        case ctt_ceild:
                return invalid(ct->left, sa);
        }
        assert(0);
}

stmt_node *domain_constructor::extract_stmt_node(operand &op, bool write,
                                                 instruction *parent)
{
        if (op.is_expr())
                return extract_stmt_node(op.instr());

        if (!op.is_symbol()) {
                op.print(stderr);
                assert(0);
        }

        if (op.symbol()->type()->is_ptr())
                return NULL;
        named_lin_ineq *a = new named_lin_ineq();
        var_sym *array = op.symbol();
        int output = 0;
        bool iterator_access = false;
        if (sa->vars.find(array) != sa->vars.end()) {
                if (!is_access_ok(sa, array, write)) {
                        if (parent)
                                parent->print(stderr);
                }
                assert(is_access_ok(sa, array, write));
                iterator_access = !sa->vars[array]->assigned ||
                                  sa->vars[array]->iterator;
        }
        if (write) {
                sa->add_var(array);
                sa->vars[array]->assigned = true;
                sa->vars[array]->value =
                        construct_condition_tree_expr(parent, verbose);
                if (invalid(sa->vars[array]->value, sa)) {
                        delete sa->vars[array]->value;
                        sa->vars[array]->value = NULL;
                } else {
                        if (scope)
                                scope->append_annote(k_set_in_scope, array);
                        sa->vars[array]->valid_for_read = true;
                }
                iterator_access = false;
        }
        if (iterator_access) {
                /* an iterator or a parameter */
                /* set inequalities to "out[0] = array */
                if (out.size() == 0)
                        out.push_back(sa->create_tmp());
                a->ineqs().init(2,1);
                a->names().init(1);
                a->add_col(name_table_entry(array), 1);
                a->add_col(name_table_entry(out[0]), 2);
                a->ineqs()[0][1] = 1;
                a->ineqs()[0][2] = -1;
                a->ineqs()[1][1] = -1;
                a->ineqs()[1][2] = 1;
                array = NULL;
                output = 1;
        }
        SRelation *map = new SRelation(sa, a);
        return new stmt_access(write, map, array, output);
}

static stmt *add_access(stmt *s, stmt_node *out)
{
        stmt_access *acc = dynamic_cast<stmt_access *>(out);
        if (!acc) {
                delete s;
                return NULL;
        }
        acc->write = true;
        s->out.push_back(acc);
        return s;
}

/*
 * Returns NULL if instruction is not ok
 * Checks currently incomplete
 */
stmt *domain_constructor::extract_stmt(tree_instr *t)
{
        stmt_node *out = NULL;
        instruction *i = t->instr();
        stmt_node *node;

        if (i->opcode() == io_str || i->opcode() == io_memcpy) {
                out = extract_stmt_node(i->src_op(0).instr());
                if (!out)
                        return NULL;
                operand r = i->src_op(1);
                node = extract_stmt_node(r, false);
        } else
                node = extract_stmt_node(i);

        if (!node) {
                if (out)
                        delete out;
                return NULL;
        }

        stmt *s = new stmt;
        s->tree = node;

        if (out)
                s = add_access(s, out);
        if (!s)
                return NULL;

        for (unsigned n = 0; n < i->num_dsts(); n++) {
                operand r = i->dst_op(n);
                if (r.is_null())
                        continue;
                stmt_node *dst = extract_stmt_node(r, true, i);
                s = add_access(s, dst);
                if (!s)
                        return NULL;
        }

        return s;
}

static char *immed2str(immed im)
{
        std::ostringstream strm;

        switch (im.kind()) {
        case im_int:
                strm << im.integer();
                break;
        case im_float:
                strm << im.flt();
                break;
        default:
                fprintf(stderr, "unsupported immed type: %d\n", im.kind());
                assert(0);
        }

        return strdup(strm.str().c_str());
}

static const char *instr_name(instruction *i)
{
        if (i->opcode() == io_cal) {
                in_cal *cal = dynamic_cast<in_cal *>(i);
                in_ldc *ldc = dynamic_cast<in_ldc *>(cal->addr_op().instr());
                assert(ldc->value().symbol()->is_proc());
                proc_sym *proc = dynamic_cast<proc_sym *>(ldc->value().symbol());
                return proc->name();
        }
        if (i->opcode() == io_str || i->opcode() == io_cpy)
                return "";
        if (i->opcode() == io_ldc) {
                in_ldc *ins = dynamic_cast<in_ldc *>(i);
                return immed2str(ins->value());
        }
        if (i->opcode() == io_add)
                return "+";
        if (i->opcode() == io_sub)
                return "-";
        if (i->opcode() == io_mul)
                return "*";
        if (i->opcode() == io_div)
                return "/";
        if (i->opcode() == io_rem)
                return "%";
        if (i->opcode() == io_neg)
                return "-";
        if (i->opcode() == io_sl)
                return "<";
        fprintf(stderr, "unrecognized instruction\n");
        i->print(stderr);
        return NULL;
}

stmt_node *domain_constructor::extract_stmt_node(instruction *i)
{
        stmt_node *node;

        node = check_access(i, false);
        if (node)
                return node;

        if (i->opcode() == io_lod) {
                operand r = i->src_op(0);
                return extract_stmt_node(r, false);
        }

        if (i->opcode() == io_cal) {
                in_cal *cal = dynamic_cast<in_cal *>(i);
                return extract_stmt_node_cal(cal);
        }

        const char *name = instr_name(i);
        if (!name)
                return NULL;

        stmt_call *call = new stmt_call(name);

        for (unsigned n = 0; n < i->num_srcs(); n++) {
                operand r = i->src_op(n);
                /* Second operand of io_cpy is null operand */
                if (r.is_null())
                        continue;
                node = extract_stmt_node(r, false);
                if (!node) {
                        delete call;
                        return NULL;
                }
                call->arg.push_back(node);
        }

        return call;
}

stmt_node *domain_constructor::extract_stmt_node_cal(in_cal *cal)
{
        const char *name = instr_name(cal);
        if (!name)
                return NULL;

        stmt_call *call = new stmt_call(name);

        in_ldc *ldc = dynamic_cast<in_ldc *>(cal->addr_op().instr());
        assert(ldc->value().symbol()->is_proc());
        proc_sym *proc = dynamic_cast<proc_sym *>(ldc->value().symbol());
        func_type *type = proc->type();
        if (!type->args_known()) {
                type = type->clone();
                type->set_num_args(cal->num_args());
                proc->set_type(type);
                for (unsigned n = 0; n < type->num_args(); ++n)
                        type->set_arg_type(n, type_signed);
                type->set_return_type(type_signed);
                tp->proc()->file()->parent()->globals()->add_type(type);
        }
        for (unsigned n = 0; n < type->num_args(); ++n) {
                stmt_node *node;
                type_node *atype = type->args_known() ? type->arg_type(n) : NULL;
                operand op = cal->argument(n);
                if (!atype || !atype->is_ptr()) {
                        node = extract_stmt_node(op, false);
                        if (!node) {
                                delete call;
                                return NULL;
                        }
                        call->arg.push_back(node);
                        continue;
                }
                /* if the function expects a pointer
                 * consider data of which the address is taken
                 * to be input if the type is pointer to const
                 * and output otherwise.
                 */
                ptr_type *ptr = static_cast<ptr_type *>(atype);
                type_node *base = ptr->ref_type();
                boolean write = !base->is_const();

                if (op.instr()->opcode() == io_cvt)
                        op = op.instr()->src_op(0);
                node = check_access(op.instr(), write);
                if (node) {
                        call->arg.push_back(node);
                        continue;
                }

                in_ldc *ldc = dynamic_cast<in_ldc *>(op.instr());
                assert(ldc);
                assert(ldc->value().kind() == im_symbol);
                assert(ldc->value().symbol()->kind() == SYM_VAR);
                var_sym *var = static_cast<var_sym*>(ldc->value().symbol());

                named_lin_ineq *a = new named_lin_ineq();
                SRelation *map = new SRelation(sa, a);
                node = new stmt_access(write, map, var, 0);
                call->arg.push_back(node);
        }

        return call;
}

void domain_constructor::set_prefix_and_iterator(int prefix_value, var_sym *iterator)
{
    if (plevel >= prefix.size())
        prefix.push_back(prefix_value);
    else
        prefix[plevel] = prefix_value;

    if (!iterator && level < its.size() && its[level]->parent() == sa->symtab)
        return;
    if (!iterator)
        iterator = sa->symtab->new_unique_var(type_signed);
    if (level >= its.size())
        its.push_back(iterator);
    else
        its[level] = iterator;
    sa->add_var(its[level]);
    sa->vars[its[level]]->iterator = true;
}

void domain_constructor::construct_broken_up_loop(for_ann *fa)
{
    SRelation *oldc = c;
    c = fa->bounds->Intersection(oldc);

    set_prefix_and_iterator(-1, fa->iterator);

    ++level;
    ++plevel;
    construct(fa->body);
    --plevel;
    --level;

    delete c;
    c = oldc;
}

/* Create 1D set with given lower and upper bounds.
 */
static SRelation *set_from_bounds(int lb, int ub, symtab_ann *sa)
{
        Relation r(1);

        GEQ_Handle e1 = r.and_with_GEQ();
        e1.update_coef(r.set_var(1), 1);
        e1.update_const(-lb);
        GEQ_Handle e2 = r.and_with_GEQ();
        e2.update_coef(r.set_var(1), -1);
        e2.update_const(ub);

        return new SRelation(r, sa);
}

/* Convert integer or string immed to int.
 * Return non-zero if immed is not a string or an integer.
 */
static int immed_to_int(immed im, int *i)
{
        switch (im.kind()) {
        case im_int:
                *i = im.integer();
                return 0;
        case im_string:
                *i = strtol(im.string(), NULL, 0);
                return 0;
        }
        return 1;
}

/* Given a "value_bounds" pragma, check that it is of the form
 *
 *      #pragma value_bounds name_of_array lower_bound upper_bound
 *
 * where lower_bound and upper_bound may be integers or strings.
 * Note that a minus sign followed by digits in a pragma is not interpreted
 * as a negative number by SUIF.
 * If so, add an SRelation annote to the array expressing the given bounds.
 */
void domain_constructor::apply_value_bounds(annote *an)
{
        immed_list *ims = an->immeds();
        sym_node *sym;
        int lb, ub;

        if (ims->count() != 4)
                goto error;
        if ((*ims)[1].kind() != im_symbol)
                goto error;
        sym = (*ims)[1].symbol();
        if (sym->kind() != SYM_VAR)
                goto error;
        if (immed_to_int((*ims)[2], &lb))
                goto error;
        if (immed_to_int((*ims)[3], &ub))
                goto error;
        sym->append_annote(k_array_bounds, set_from_bounds(lb, ub, sa));

        return;
error:
        fprintf(stderr, "invalid value_bounds pragma\n");
}

/* Check for any interesting pragmas associated to the given instruction.
 * In particular, check for value_bounds pragmas.
 */
void domain_constructor::check_pragmas(instruction *in)
{
        const char *k_C_pragma = lexicon->enter("C pragma")->sp;
        annote_list_iter anli(in->annotes());
        while (!anli.is_empty()) {
                annote *an = anli.step();
                if (an->name() != k_C_pragma)
                        continue;
                immed_list *ims = an->immeds();
                if (!(*ims)[0].is_string())
                        continue;
                if (strcmp((*ims)[0].string(), "value_bounds") == 0)
                        apply_value_bounds(an);
        }
}

/* Construct an iteration domain annote from a stmt annote attached
 * to obj and the current constraints on the iterators and attach
 * the annote to obj.
 * insn is the intruction that gave rise to the statement
 * and may be NULL if there is no clearly identifiable such instruction.
 */
void domain_constructor::add_iteration_domain(suif_object *obj,
                                                instruction *insn)
{
        stmt *s = (stmt *)obj->peek_annote(k_stmt);

        s->reorder(this);

        SRelation *o = reorder(c);

        domain_ann *da;
        int line = source_line_num(obj);
        da = new domain_ann(insn, o, level, plevel, its, prefix, s, line);
        obj->append_annote(k_iteration_domain, da);
}

void
domain_constructor::construct(tree_node * tn)
{
    switch (tn->kind()) {
    case TREE_INSTR: {
        for_ann *fa = (for_ann *)tn->peek_annote(k_for_annote);
        if (fa) {
            construct_broken_up_loop(fa);
            break;
        }
        tree_instr *in = (tree_instr*)tn;
        switch (in->instr()->opcode()) {
        case io_mrk:
            check_pragmas(in->instr());
            break;
        default:
            assert(0);
        case io_memcpy:
        case io_cpy:
        case io_str:
        case io_lod:
        case io_cvt:
        case io_ldc:
        case io_add:
        case io_sub:
        case io_mul:
        case io_div:
        case io_rem:
        case io_cal:
            root = in->instr();
            add_iteration_domain(root, root);
        }
        break;
    }
    case TREE_FOR: {
        for_ann *fa = (for_ann *)tn->peek_annote(k_for_annote);
        if (fa) {
            construct_broken_up_loop(fa);
            break;
        }
        SRelation * oldc = new SRelation(*c);
        dep_for_annote * df = 
                (dep_for_annote *)tn->peek_annote(k_dep_for_annote);
        tree_for * tf = df->my_for;
        immed idx(tf->index());
        c->intersect(named_lin_ineq::mk_named_lin_ineq(*df->lb, idx, TRUE));
        c->intersect(named_lin_ineq::mk_named_lin_ineq(*df->ub, idx, FALSE));

        set_prefix_and_iterator(-1, tf->index());

        ++level;
        ++plevel;
        construct(tf->body());
        --plevel;
        --level;

        delete c;
        c = oldc;
        break;
    }
    case TREE_LOOP: {
        /* We only get here if the loop was determined to be a simple infinite loop */
        SRelation * oldc = new SRelation(*c);
        tree_loop *tl = static_cast<tree_loop *>(tn);

        set_prefix_and_iterator(-1);
        c->set_infinite(its[level]);

        ++level;
        ++plevel;
        construct(tl->body());
        --plevel;
        --level;

        delete c;
        c = oldc;
        break;
    }
    case TREE_IF: {
        tree_if * ti = (tree_if *)tn;
        SRelation * oldc = c;

        if (tn->peek_annote(k_stmt)) {
                add_iteration_domain(tn, NULL);
                break;
        }

        SRelation * s = (SRelation *)tn->peek_annote(k_if_annote);
        /* The if is not annotated, so it must be the second part
         * of a broken down loop we discovered during the scan phase.
         */
        if (!s)
            break;
        c = s->Intersection(oldc);

        construct(ti->then_part());

        delete c;

        if (ti->else_part()->is_empty()) {
            c = oldc;
            break;
        }

        c = oldc->Difference(s);

        construct(ti->else_part());

        delete c;

        c = oldc;
        break;
    }
    default:
        recurse(tn);
        break;
    }
}

void
domain_constructor::construct(tree_node_list * tnl)
{
    set_prefix_and_iterator(0);

    tree_node_list_iter tnli(tnl);
    for (int i = 0; !tnli.is_empty(); ++i) {
        tree_node *t = tnli.step();

        SRelation * oldc = new SRelation(*c);

        if (oldstyle)
            c->fix(its[level], i);
        prefix[plevel] = i;

        if (oldstyle)
            ++level;
        ++plevel;
        construct(t);
        --plevel;
        if (oldstyle)
            --level;

        delete c;
        c = oldc;
    }
}

void domain_constructor::visit(tree_node *t)
{
    if (!t->peek_annote(k_static_root))
        return;

    c = new SRelation(sa);
    level = 0;
    plevel = 0;
    construct(t);
    delete c;
}

static void visit (tree_node *t, void *d)
{
    ((domain_constructor *)d)->visit(t);
}

void domain_constructor::construct()
{
    tp->map(::visit, (void *) this);
}

bool guard_constructor::fill_q(Constraint_Handle& h, condition_tree *ct, int mult)
{
        switch(ct->type) {
        case ctt_cst:
                h.update_const(mult * ct->val);
                break;
        case ctt_add:
                if (!fill_q(h, ct->left, mult))
                    return false;
                if (!fill_q(h, ct->right, mult))
                    return false;
                break;
        case ctt_sub:
                if (!fill_q(h, ct->left, mult))
                    return false;
                if (!fill_q(h, ct->right, -mult))
                    return false;
                break;
        case ctt_sym: {
                sa->add_var(ct->var);
                Param_Iterator *var = sa->vars[ct->var];
                if (var->value)
                        return fill_q(h, var->value, mult);
                if (var->iterator || !var->assigned) {
                        h.update_coef(s->get_local(sa->vars[ct->var]), mult);
                        break;
                }
                if (!dc)
                        return false;
                stmt_node *node;
                operand op(ct->var);
                node = dc->extract_stmt_node(op, false);
                if (!node)
                        return false;
                node->var = sa->create_tmp();
                node->op = op;
                s->nested.push_back(node);
                h.update_coef(s->get_local(sa->vars[node->var]), mult);
                break;
        }
        case ctt_mul:
                assert(ct->left->type == ctt_cst);
                return fill_q(h, ct->right, mult * ct->left->val);
        case ctt_neg:
                if (!fill_q(h, ct->left, -mult))
                    return false;
                break;
        case ctt_rem: {
                assert(ct->right->type == ctt_cst);
                int mod = ct->right->val; 

                Variable_ID q = s->e->declare();
                Variable_ID r = s->e->declare();
                h.update_coef(r, mult);

                /* r >= 0 */
                GEQ_Handle g1 = s->f->add_GEQ();
                g1.update_coef(r, 1);

                /* r <= mod-1 */
                GEQ_Handle g2 = s->f->add_GEQ();
                g2.update_coef(r, -1);
                g2.update_const(mod-1);

                /* mod * q + r = op1 */
                EQ_Handle g3 = s->f->add_EQ();
                g3.update_coef(r, -1);
                g3.update_coef(q, -mod);
                if (!fill_q(g3, ct->left, 1))
                        return false;
                break;
        }
        case ctt_floord: {
                /* f = floor(e/m) */
                assert(ct->right->type == ctt_cst);
                int mod = ct->right->val; 

                Variable_ID q = s->e->declare();
                h.update_coef(q, mult);

                /* e - m f >= 0 */
                GEQ_Handle g1 = s->f->add_GEQ();
                g1.update_coef(q, -mod);
                if (!fill_q(g1, ct->left, 1))
                        return false;

                /* -e + m f + m-1 >= 0 */
                GEQ_Handle g2 = s->f->add_GEQ();
                g2.update_coef(q, mod);
                g2.update_const(mod - 1);
                if (!fill_q(g2, ct->left, -1))
                        return false;

                break;
        }
        case ctt_lod: {
                stmt_node *node;
                if (!dc)
                        return false;
                node = dc->extract_stmt_node(ct->op, false);
                if (!node)
                        return false;
                node->var = sa->create_tmp();
                node->op = ct->op;
                s->nested.push_back(node);
                h.update_coef(s->get_local(sa->vars[node->var]), mult);
                return true;
        }
        default:
                assert(0);
        }

        return true;
}

bool guard_constructor::construct_guard(condition_tree *ct, F_And *f)
{
        switch (ct->type) {
        case ctt_invalid:
                return false;
        case ctt_ge: {
                GEQ_Handle g = f->add_GEQ();
                return fill_q(g, ct->left, 1);
        }
        case ctt_eq: {
                EQ_Handle g = f->add_EQ();
                return fill_q(g, ct->left, 1);
        }
        case ctt_or: {
                F_Or *o = f->add_or();
                if (!construct_guard(ct->left, o->add_and()))
                        return false;
                return construct_guard(ct->right, o->add_and());
        }
        case ctt_and: {
                if (!construct_guard(ct->left, f->add_and()))
                        return false;
                return construct_guard(ct->right, f->add_and());
        }
        default:
                assert(0);
        }
}

/* Replace each ctt_sym node in the tree that has a value associated
 * with it in the symtab_ann with this value.
 */
static condition_tree *substitute_values(condition_tree *ct, symtab_ann *sa)
{
        if (ct->type == ctt_sym && sa->vars.find(ct->var) != sa->vars.end()) {
                Param_Iterator *var = sa->vars[ct->var];
                if (var->value) {
                        delete ct;
                        return var->value->dup();
                }
        }
        if (ct->left)
                ct->left = substitute_values(ct->left, sa);
        if (ct->right)
                ct->right = substitute_values(ct->right, sa);
        return ct;
}

bool guard_constructor::construct_guard(instruction *ins)
{
        condition_tree *ct = construct_condition_tree(ins, verbose);
        ct = substitute_values(ct, sa);
        ct->eliminate_minmax();
        bool ok = construct_guard(ct, s->f);
        delete ct;
        return ok;
}

static void set_truth_value(suif_object *o, SRelation *sr,
                            tree_if *ti, tree_node_list *tnl)
{
    if (tnl == ti->then_part()) {
        SRelation *s = (SRelation *)ti->peek_annote(k_if_annote);
        assert(s);
        SRelation *news = sr->Intersection(s);
        delete sr;
        sr = news;
    }
    if (tnl == ti->else_part()) {
        SRelation *s = (SRelation *)ti->peek_annote(k_if_annote);
        assert(s);
        SRelation *news = sr->Difference(s);
        delete sr;
        sr = news;
    }
    SRelation *s = (SRelation *)o->get_annote(k_if_annote);
    if (s) {
        SRelation *news = sr->Union(s);
        delete sr;
        delete s;
        sr = news;
    }
    o->append_annote(k_if_annote, sr);
}

/* Construct a guard from tnl and attach it to ti.
 * If allow_nested is set, then the domain_constructor is passed
 * to the guard_constructor, so that it can construct nested accesses.
 */
boolean domain_constructor::construct_guard(tree_if *ti, tree_node_list *tnl,
        bool allow_nested)
{
    tree_node_list_iter tnli(tnl);

    for (int i = 0; !tnli.is_empty(); ++i) {
        tree_node *tn = tnli.step();
        switch (tn->kind()) {
        case TREE_INSTR: {
            tree_instr *in = (tree_instr*)tn;
            switch (in->instr()->opcode()) {
            case io_btrue:
            case io_bfalse: {
                in_bj *bj = (in_bj *)in->instr();
                operand op = bj->src_op();
                SRelation *sr = NULL;
                switch (op.kind()) {
                case OPER_INSTR: {
                    instruction * ins = op.instr();
                    guard_constructor gc(sa, verbose,
                                         allow_nested ? this : NULL);
                    bool ok = gc.construct_guard(ins);
                    if (ok) {
                        if (in->instr()->opcode() == io_bfalse)
                            sr = new SRelation(*gc.s);
                        else
                            sr = gc.s->Complement();
                    }
                    break;
                }
                case OPER_SYM: {
                    sym_node *v= op.symbol();
                    SRelation *s = (SRelation *)v->peek_annote(k_if_annote);
                    assert(s);
                    if (in->instr()->opcode() == io_bfalse)
                        sr = new SRelation(*s);
                    else
                        sr = s->Complement();
                    break;
                }
                default:
                    assert(0);
                }
                assert(tnl == ti->header());
                if (sr)
                    ti->append_annote(k_if_annote, sr);
                return sr != NULL;
            }
            case io_seq:
            case io_sl:
            case io_sle: {
                guard_constructor gc(sa, verbose, allow_nested ? this : NULL);
                boolean ok = gc.construct_guard(in->instr());
                assert(in->instr()->dst_op().kind() == OPER_SYM);
                sym_node* v = in->instr()->dst_op().symbol();
                if (ok)
                    set_truth_value(v, new SRelation(*gc.s), ti, tnl);
                else
                    return ok;
                break;
            }
            case io_cpy: {
                assert(in->instr()->dst_op().kind() == OPER_SYM);
                sym_node* vd = in->instr()->dst_op().symbol();
                assert(in->instr()->src_op(0).kind() == OPER_SYM);
                sym_node* vs = in->instr()->src_op(0).symbol();
                SRelation *s = (SRelation *)vs->peek_annote(k_if_annote);
                assert(s);
                set_truth_value(vd, new SRelation(*s), ti, tnl);
                break;
            }
            case io_mrk:
                break;
            default:
                if (verbose) {
                    fprintf(stderr, "Unhandled guard:\n");
                    in->instr()->print(stderr);
                }
                return false;
            }
            break;
        }
        case TREE_IF: {
            tree_if *ti = (tree_if *) tn;
            bool ok = construct_guard(ti, ti->header(), allow_nested) &&
                      construct_guard(ti, ti->then_part(), allow_nested) &&
                      construct_guard(ti, ti->else_part(), allow_nested);
            if (!ok)
                return ok;
            break;
        }
        default:
            return false;
        }
    }
    return true;
}

/* Check if the bound computed by SUIF is ok.
 * First, if SUIF return NULL, then the bound is obviously not OK.
 * Second, if any of the variables involved is not an iterator
 * or a parameter, but a variable with a fixed value assigned, then
 * we need to substitute that value and so the bound computed
 * by SUIF is not OK.
 */
static bool valid_bound(symtab_ann *sa, named_lin_ineq *nlq)
{
        if (!nlq)
                return false;

        for (int i = 1; i < nlq->names().n(); ++i) {
                var_sym *v = nlq->names()[i].var();
                if (sa->vars.find(v) == sa->vars.end())
                        continue;
                if (sa->vars[v]->value)
                        return false;
        }

        return true;
}

/* If tnl contains a signle top level assignement, then
 * return the corresponding instruction.  Otherwise, return NULL.
 */
static instruction *single_assignment(tree_node_list *tnl)
{
        tree_instr *in;
        tree_node_list_iter tnli(tnl);
        for (int i = 0; !tnli.is_empty(); ++i) {
                tree_node *tn = tnli.step();
                if (tn->kind() != TREE_INSTR)
                        return NULL;
                in = (tree_instr*)tn;
                if (in->instr()->opcode() == io_mrk)
                        continue;
                break;
        }
        if (!tnli.is_empty())
                return NULL;

        switch (in->instr()->opcode()) {
        case io_ldc:
        case io_lod:
        case io_memcpy:
        case io_str:
                return in->instr();
        }

        return NULL;
}

static bool equal(operand op1, operand op2)
{
    if (op1.kind() != op2.kind())
        return false;
    switch (op1.kind()) {
    case OPER_INSTR: {
        if (op1.instr()->opcode() != op2.instr()->opcode())
            return false;
        if (op1.instr()->opcode() == io_ldc) {
            in_ldc *in1 = dynamic_cast<in_ldc *>(op1.instr());
            in_ldc *in2 = dynamic_cast<in_ldc *>(op2.instr());
            if (in1->value() != in2->value())
                return false;
        }
        for (unsigned n = 0; n < op1.instr()->num_srcs(); n++) {
            if (!equal(op1.instr()->src_op(n), op2.instr()->src_op(n)))
                return false;
        }
        break;
    }
    case OPER_SYM:
        return op1.symbol() == op2.symbol();
    case OPER_NULL:
        return true;
    default:
        return false;
    }
    return true;
}

/* Add the data dependent conditions in c to all accesses in n.
 */
static void add_data_dependent_conditions(stmt_node *n, SRelation *c)
{
        if (n->is_access()) {
                stmt_access *a = static_cast<stmt_access *>(n);
                SRelation *map = c->Intersection(a->map);
                delete a->map;
                a->map = map;
        } else {
                stmt_call *call = static_cast<stmt_call *>(n);
                for (int i = 0; i < call->arg.size(); ++i)
                        add_data_dependent_conditions(call->arg[i], c);
        }
}

/* Return the operand that identifies the write of the assignment instruction i.
 */
static operand write_op(instruction *i)
{
        switch (i->opcode()) {
        case io_ldc:
        case io_lod:
                return i->dst_op(0);
        case io_memcpy:
        case io_str:
                return i->src_op(0);
        }
        assert(0);
}

/* Return a stmt_node corresponding to the read performed
 * in the assignment instruction i.
 */
stmt_node *domain_constructor::read_stmt(instruction *i)
{
        switch (i->opcode()) {
        case io_ldc:
        case io_lod:
                return extract_stmt_node(i);
        case io_memcpy:
        case io_str: {
                operand r = i->src_op(1);
                return extract_stmt_node(r, false);
        }
        }
        assert(0);
}

/* Return an "iterator" access, that accesses the constant "1"
 * when the conditions c1 hold and the constant "0" when the
 * conditions c0 hold.  That is, assuming c0 is the complement
 * of c1, return an access that encodes the conditions c1.
 */
stmt_access *domain_constructor::data_dependent_test_cond(
        SRelation *c1, SRelation *c0)
{
        if (out.size() == 0)
                out.push_back(sa->create_tmp());
        sa->add_var(out[0]);

        Relation r(0,0);
        EQ_Handle g;

        SRelation *s1 = new SRelation(r, sa);
        s1->e = s1->add_exists();
        s1->f = s1->e->add_and();
        g = s1->f->add_EQ();
        g.update_const(1);
        g.update_coef(s1->get_local(sa->vars[out[0]]), -1);

        SRelation *t1 = s1->Intersection(c1);
        delete s1;

        SRelation *s0 = new SRelation(r, sa);
        s0->e = s0->add_exists();
        s0->f = s0->e->add_and();
        g = s0->f->add_EQ();
        g.update_const(0);
        g.update_coef(s0->get_local(sa->vars[out[0]]), -1);

        SRelation *t0 = s0->Intersection(c0);
        delete s0;

        SRelation *c = t0->Union(t1);
        delete t0;
        delete t1;

        return new stmt_access(false, c, NULL, 1);
}

/* Check if the if "ti" represents a data dependent assignment
 * and if so, attach the corresponding data dependent statement
 * to this node.
 *
 * A data dependent assignment is an assignment of the form
 *
 *      if (data dependent conditions)
 *              a = f(...);
 *      else
 *              a = g(...);
 *
 * The data dependent statement constructed is of the form
 *
 *      a = #test(data dependent conditions, f(...), g(...))
 *
 * where all the access relations in f have been updated to
 * include the data dependent conditions and all those in g
 * have been updated to include the negation of these conditions.
 * Note that this means that the access relations may only
 * select a subset of the iteration domains.
 * The data dependent conditions are therefore also explicitly
 * encoded in the first argument.
 *
 * We first check that the then and else branches each contain
 * a single assignment.
 * Both assignments should assign to the same scalar or array element.
 * We then see if we can analyze the conditions, allowing for nested accesses,
 * and if so construct the #test statement.
 */
bool domain_constructor::is_data_dependent_assignment(tree_if *ti)
{
        instruction *in_then, *in_else;

        in_then = single_assignment(ti->then_part());
        in_else = single_assignment(ti->else_part());

        if (!in_then || !in_else)
                return false;

        if (in_then->num_dsts() != in_else->num_dsts())
                return false;

        operand then_write = write_op(in_then);
        operand else_write = write_op(in_else);

        if (!equal(then_write, else_write))
                return false;

        bool ok = construct_guard(ti, ti->header(), true);
        if (!ok)
                return false;

        SRelation *sr = (SRelation *)ti->peek_annote(k_if_annote);
        assert(sr);

        stmt_node *out;
        out = extract_stmt_node(then_write, true, in_then);
        if (!out)
                return false;

        stmt_node *node_then = read_stmt(in_then);
        if (!node_then) {
                delete out;
                return false;
        }
        stmt_node *node_else = read_stmt(in_else);
        if (!node_else) {
                delete out;
                delete node_then;
                return false;
        }

        add_data_dependent_conditions(node_then, sr);

        SRelation *c = sr->Complement();
        add_data_dependent_conditions(node_else, c);
        stmt_access *cond = data_dependent_test_cond(sr, c);
        delete c;

        stmt_call *test = new stmt_call("#test");
        test->arg.push_back(cond);
        test->arg.push_back(node_then);
        test->arg.push_back(node_else);

        stmt *s = new stmt;
        s->tree = test;
        s = add_access(s, out);

        ti->append_annote(k_stmt, s);

        return true;
}

/* Move up to old_scope and remove any assignments that
 * have been performed inside the current scope (if it
 * is different from old_scope).
 */
void domain_constructor::leave_scope(tree_node *old_scope)
{
        if (old_scope == scope)
                return;
        annote_list_iter anli(scope->annotes());
        while (!anli.is_empty()) {
                annote *an = anli.step();
                if (an->name() != k_set_in_scope)
                        continue;
                var_sym *array = (var_sym *)an->data();
                if (sa->vars[array]->value)
                        delete sa->vars[array]->value;
                sa->vars[array]->value = NULL;
        }
        scope = old_scope;
}

boolean domain_constructor::scan(tree_node * tn)
{
    boolean ok = true;
    stmt *stmt = NULL;
    tree_node *old_scope = scope;

    switch (tn->kind()) {
    case TREE_INSTR: {
        tree_instr *in = (tree_instr*)tn;
        switch (in->instr()->opcode()) {
        case io_memcpy:
        case io_cpy:
        case io_str:
        case io_lod:
        case io_cvt:
        case io_ldc:
        case io_add:
        case io_sub:
        case io_mul:
        case io_div:
        case io_rem:
        case io_cal:
            root = in->instr();
            stmt = extract_stmt(in);
            if (stmt)
                root->append_annote(k_stmt, stmt);
            ok = stmt != NULL;
            break;
        case io_mrk:
            break;
        default:
            if (verbose) {
                fprintf(stderr, "Unhandled instruction:\n");
                in->instr()->print(stderr);
            }
            ok = false;
            break;
        }
        break;
    }
    case TREE_IF: {
        scope = tn;
        tree_if *ti = (tree_if *) tn;
        boolean guard_ok;
        guard_ok = construct_guard(ti, ti->header(), NULL);
        if (guard_ok)
                ok = scan(ti->then_part()) && scan(ti->else_part());
        else
                ok = is_data_dependent_assignment(ti);
        break;
    }
    case TREE_FOR: {
        scope = tn;
        dep_for_annote * df = 
                (dep_for_annote *)tn->peek_annote(k_dep_for_annote);
        named_lin_ineq *lb, *ub;
        tree_for * tf = df->my_for;
        sa->add_var(tf->index());
        sa->vars[tf->index()]->iterator = true;
        sa->vars[tf->index()]->valid_for_read = true;
        delete sa->vars[tf->index()]->value;
        sa->vars[tf->index()]->value = NULL;
        immed idx(tf->index());
        lb = named_lin_ineq::mk_named_lin_ineq(*df->lb, idx, TRUE);
        ub = named_lin_ineq::mk_named_lin_ineq(*df->ub, idx, FALSE);
        sa->add_var(lb);
        sa->add_var(ub);
        ok = valid_bound(sa, lb) && valid_bound(sa, ub);
        if (lb)
            delete lb;
        if (ub)
            delete ub;
        if (!ok) {
            instruction *lower = new in_rrr(io_sle, tf->index()->type(),
                operand(), tf->lb_op().clone(), operand(tf->index()));
            guard_constructor gc_lower(sa, verbose, NULL);
            ok = gc_lower.construct_guard(lower);
            delete lower;
            if (!ok)
                break;

            instruction *upper = new in_rrr(io_sle, tf->index()->type(),
                operand(), operand(tf->index()), tf->ub_op().clone());
            guard_constructor gc_upper(sa, verbose, NULL);
            ok = gc_upper.construct_guard(upper);
            delete upper;
            if (!ok)
                break;

            Relation I = Intersection(*gc_lower.s, *gc_upper.s);
            tn->append_annote(k_for_annote,
                new for_ann(new SRelation(I, sa), tf->index(), tf->body()));
        }
        ok = scan(tf->body());
        sa->vars[tf->index()]->iterator = false;
        if (sa->vars[tf->index()]->assigned)
            sa->vars[tf->index()]->valid_for_read = false;
        break;
    }
    case TREE_LOOP: {
        scope = tn;
        /* We only accept infinite loops */
        tree_loop *tl = static_cast<tree_loop *>(tn);
        tree_node_list *tnl = tl->test();
        tree_node_list_iter tnli(tnl);
        bool infinite_loop = false;

        /* Simple test for infinite loop:
         * a loop whose test jumps right back to the top of the loop.
         */
        while (!tnli.is_empty()) {
            tree_node *t = tnli.step();
            if (t->kind() != TREE_INSTR)
                break;
            tree_instr *in = static_cast<tree_instr*>(t);
            if (in->instr()->opcode() == io_mrk)
                continue;
            if (in->instr()->opcode() != io_jmp)
                break;
            in_bj *bj = static_cast<in_bj *>(in->instr());
            if (bj->target() != tl->toplab())
                break;
            infinite_loop = true;
            break;
        }
        ok = infinite_loop && scan(tl->body());
        break;
    }
    default:
        unsigned n = tn->num_child_lists();
        for (unsigned i = 0; ok && i < n; ++i)
            ok = scan(tn->child_list_num(i));
    }
    leave_scope(old_scope);

    return ok;
}

/* If the tree_node_list consists entirely of zero or more marks and
 * exactly one test, return the test.  Otherwise return NULL.
 */
static tree_instr *if_test(tree_node_list *tnl)
{
    tree_instr *test = NULL;
    tree_node_list_iter tnli(tnl);
    for (int i = 0; !tnli.is_empty(); ++i) {
        tree_node *tn = tnli.step();
        switch (tn->kind()) {
        case TREE_INSTR: {
            tree_instr *in = (tree_instr*)tn;
            switch (in->instr()->opcode()) {
            case io_btrue:
            case io_bfalse:
                if (!test)
                    test = in;
                else
                    return NULL;
                break;
            case io_mrk:
                break;
            default:
                return NULL;
            }
            break;
        }
        default:
            return NULL;
        }
    }
    return test;
}

/* If the tree_node_list consists out of an increment followed by a test,
 * possibly interspersed by marks, then return true and put a pointer to
 * the increment and the test in inc and test.
 * Otherwise return false.
 */
static bool loop_extract_increment_and_test(tree_node_list *tnl,
                                            tree_instr **inc, tree_instr **test)
{
    *inc = NULL;
    *test = NULL;
    tree_node_list_iter tnli(tnl);
    for (int i = 0; !tnli.is_empty(); ++i) {
        tree_node *tn = tnli.step();
        switch (tn->kind()) {
        case TREE_INSTR: {
            tree_instr *in = (tree_instr*)tn;
            switch (in->instr()->opcode()) {
            case io_add:
                if (!*inc)
                    *inc = in;
                else
                    return false;
                break;
            case io_btrue:
            case io_bfalse:
                if (*inc && !*test)
                    *test = in;
                else
                    return false;
                break;
            case io_mrk:
                break;
            default:
                return false;
            }
            break;
        }
        default:
            return false;
        }
    }
    return true;
}

/* Return true if instruction "i" contains an increment on
 * the variable "iterator".
 */
static bool is_increment_on(instruction *i, var_sym *iterator)
{
    if (i->opcode() != io_add)
        return false;
    if (!i->dst_op(0).is_symbol())
        return false;
    if (i->dst_op(0).symbol() != iterator)
        return false;
    if (!i->src_op(0).is_symbol())
        return false;
    if (i->src_op(0).symbol() != iterator)
        return false;
    if (!i->src_op(1).is_instr())
        return false;
    if (i->src_op(1).instr()->opcode() != io_ldc)
        return false;
    in_ldc *ins = dynamic_cast<in_ldc *>(i->src_op(1).instr());
    if (!ins->value().is_integer())
        return false;
    if (ins->value().integer() != 1)
        return false;
    return true;
}

/* Check whether the pair of successive tree nodes t1 and t2 represent
 * a for loop that was dismantled by snoot.
 * If so, return true and return the body of that for loop in *body.
 *
 * snoot breaks up a for loop of the form
 *
 *      for (init; test; update) {
 *              body
 *      }
 *
 * as
 *
 *      init;
 *      if (test) {
 *              do {
 *                      body;
 *              } while (update, test);
 *      }
 *
 * We check that the first instruction "init" modifies some symbol ("iterator")
 * and that we can recognize "init <= iterator" as a lower bound for a for loop.
 *
 * Then we check that the second instruction is an IF without else part
 * and with a nested LOOP, that the if and the test have the same test,
 * that it involves the iterator and that it can be recognized as an
 * upper bound of a for loop.
 * Finally, the update should increment "iterator".
 *
 * If all these conditions are satisfied, we return true and attach
 * a for_ann to the first instruction, containing the body of the loop,
 * the loop iterator and the lower and upper bounds.
 */
bool domain_constructor::is_broken_up_loop(tree_node *t1, tree_node *t2,
                                    tree_node_list **body, var_sym **iterator)
{
    if (t1->kind() != TREE_INSTR)
        return false;
    if (t2->kind() != TREE_IF)
        return false;
    tree_if *ti = (tree_if *) t2;
    if (ti->else_part()->count())
        return false;
    tree_node_list *if_body = ti->then_part();
    if (if_body->count() != 1)
        return false;
    tree_node *tn = if_body->head()->contents;
    if (tn->kind() != TREE_LOOP)
        return false;
    tree_loop *tl = (tree_loop *) tn;

    tree_instr *init = (tree_instr *)t1;

    if (!init->instr()->dst_op(0).is_symbol())
        return false;

    *iterator = init->instr()->dst_op(0).symbol();

    tree_instr *ti_test = if_test(ti->header());
    if (!ti_test)
        return false;

    tree_instr *tl_inc;
    tree_instr *tl_test;
    if (!loop_extract_increment_and_test(tl->test(), &tl_inc, &tl_test))
        return false;

    if (ti_test->instr()->opcode() != io_bfalse)
        return false;

    if (tl_test->instr()->opcode() != io_btrue)
        return false;

    if (!equal(ti_test->instr()->src_op(0), tl_test->instr()->src_op(0)))
        return false;

    if (!is_increment_on(tl_inc->instr(), *iterator))
        return false;

    if (ti_test->instr()->src_op(0).kind() != OPER_INSTR)
        return false;

    instruction *in = ti_test->instr()->src_op(0).instr();
    if (in->opcode() != io_sl && in->opcode() != io_sle)
        return false;

    if (!in->src_op(0).is_symbol())
        return false;
    if (in->src_op(0).symbol() != *iterator)
        return false;

    sa->add_var(*iterator);
    sa->vars[*iterator]->iterator = true;
    delete sa->vars[*iterator]->value;
    sa->vars[*iterator]->value = NULL;
    sa->vars[*iterator]->valid_for_read = true;

    bool ok;
    guard_constructor gc(sa, verbose, NULL);
    ok = gc.construct_guard(in);
    if (!ok)
        return false;

    instruction *lower = new in_rrr(io_sle, (*iterator)->type(), operand(),
                init->instr()->clone(), operand(*iterator));

    guard_constructor gc_lower(sa, verbose, NULL);
    ok = gc_lower.construct_guard(lower);
    delete lower;
    if (!ok)
        return false;

    Relation I = Intersection(*gc.s, *gc_lower.s);
    *body = tl->body();
    t1->append_annote(k_for_annote,
        new for_ann(new SRelation(I, sa), *iterator, *body));

    return true;
}

boolean domain_constructor::scan(tree_node_list * tnl)
{
    tree_node_list_e *start = NULL;

    tree_node_list_iter tnli(tnl);
    for (int i = 0; !tnli.is_empty(); ++i) {
        tree_node *t = tnli.step();
        tree_node_list *body = NULL;
        var_sym *iterator = NULL;
        bool ok;
        if (!tnli.is_empty() &&
                        is_broken_up_loop(t, tnli.peek(), &body, &iterator)) {
            ok = scan(body);
            sa->vars[iterator]->iterator = false;
            if (sa->vars[iterator]->assigned)
                sa->vars[iterator]->valid_for_read = false;
            tnli.step();
        } else
            ok = scan(t);
        if (ok) {
            if (!start)
                start = t->list_e();
        } else if (start) {
            tree_node *root;

            if (start->next() == t->list_e())
                root = start->contents;
            else {
                block_symtab *st = new block_symtab("static root");
                tnl->scope()->add_child(st);
                tree_node_list *tl = new tree_node_list;
                tree_block *tb = new tree_block(tl, st);
                tnl->insert_before(tb, start);
                tb->proc()->block()->number_instrs();

                tree_node_list_e *next = start->next();
                while (start != t->list_e()) {
                    tnl->remove(start);
                    tl->append(start);
                    start = next;
                    next = start->next();
                }
                root = tb;
            }
            if (!(root->kind() == TREE_INSTR && 
                  ((tree_instr*)root)->instr()->opcode() == io_mrk))
                root->append_annote(k_static_root, new immed_list());

            start = NULL;
        }
    }

    return start == tnl->head();
}

void domain_constructor::scan(context_info *ctx)
{
    sa = new symtab_ann;
    sa->symtab = new global_symtab("statement iterators");
    level = 0;

    std::map<var_sym *, Param_Iterator *>::iterator gi;
    for (gi = ctx->sa->vars.begin(); gi != ctx->sa->vars.end(); ++gi)
            sa->vars[(*gi).first] = (*gi).second;

    tp->append_annote(k_domain_symtab, sa);
    scan(tp->body());
}

void construct_domains(tree_proc * tp, int verbose, int oldstyle, context_info *ctx)
{
    domain_constructor dc(tp, verbose, oldstyle);
    dc.scan(ctx);
    dc.construct();
}

static void free_stmt(void *data)
{
    stmt *s = (stmt *)data;
    delete s;
}

static void
free_domain_ann(void *data)
{
    domain_ann *da = (domain_ann *) data;
    delete da->domain;
    delete da;
}

static void
free_symtab(void *data)
{
    symtab_ann *sa = (symtab_ann *) data;
    delete sa->symtab;
    delete sa;
}

static void free_srelation(void *data)
{
    SRelation *sr = (SRelation *) data;
    delete sr;
}

static void free_for_ann(void *data)
{
    delete (for_ann *) data;
}

void
init(int &argc, char *argv[])
{
    ANNOTE(k_static_root, "pers_static_root", FALSE);
    STRUCT_ANNOTE(k_stmt, "pers_stmt", FALSE,
        NULL, NULL, free_stmt, NULL);
    STRUCT_ANNOTE(k_iteration_domain, "pers_iteration_domain", FALSE,
        NULL, NULL, free_domain_ann, NULL);
    STRUCT_ANNOTE(k_domain_symtab, "pers_domain_symtab", FALSE,
        NULL, NULL, free_symtab, NULL);
    STRUCT_ANNOTE(k_if_annote, "pers_if_annote", FALSE,
        NULL, NULL, free_srelation, NULL);
    STRUCT_ANNOTE(k_for_annote, "pers_for_annote", FALSE,
        NULL, NULL, free_for_ann, NULL);
    STRUCT_ANNOTE(k_array_bounds, "pers_array_bounds", FALSE,
        NULL, NULL, free_srelation, NULL);
    STRUCT_ANNOTE(k_set_in_scope, "pers_set_in_scope", FALSE,
        NULL, NULL, NULL, NULL);
}