#include "blocks.h"
#include "flow.h"
#include "optimise.h"

static void block(Block b);
static void verifyLiveness();
static void verifyLDepths(Block block);
int do_verify = 0;
static char* name;

void verify(char* _name) {
    if (do_verify) {
        LOG(("Verifiying %s\n", _name));
        name = _name;
        flow_applyToBlocks(block);
        if (0) 
            flow_applyToBlocks(verifyLDepths);
        verifyLiveness();
    }
}

#define CHECK(x) {int i; i = (x); if(i) return i; }
#define CHECK_VREG(x) {Node i; i = (x); if(i) return i; }

static Node temps(Node p, Node* lastTemp, int forward) {
    int generic;
    if (p == NULL)
        return NULL;
    generic = generic(p->op);
    if (generic == STACK || generic == VREG || generic == COPY) {
        if (*lastTemp) {
            if (forward) {
                if((*lastTemp)->x.next != p || p->x.prev != (*lastTemp)) {
                    return p;   
                }
            } else {
                if((*lastTemp)->x.prev != p || p->x.next != (*lastTemp)) {
                    return p;   
                }
            }
        }
        *lastTemp = p;
    } else {
        if (generic == ASGN) {
            int kidop = generic(p->kids[0]->op);
            if (kidop == VREG || kidop == STACK)
            if (p->kids[0]->x.defn == 0) {
                fprintf(stderr, "Assignment not marked");
                return p->kids[0];
            }
        } 
        CHECK_VREG(temps(p->kids[1-forward], lastTemp, forward));
        CHECK_VREG(temps(p->kids[forward], lastTemp, forward));
    }
    return NULL;
}

static int treeDepth(Node p, int* depth);

static void block_printDepths(Block b) {
    Node p, end;
    int depth = block_getStartEDepth(b);
    int invalid = 0;
    end = block_lastNode(b)->x.next;
    fprintf(stderr, "Verify failed in %s\n", name);
    fprintf(stderr, "Function: %s\n", cfunc->name);
    for (p = block_firstNode(b); p != end; p = p->x.next) {
        prettytree(p);
        if (invalid) {
            fprintf(stderr, "Depth invalid\n");
        } else {
            invalid = treeDepth(p, &depth);
            fprintf(stderr, "Depth: %d\n", depth);
        }
    }
}

static void linkageFailure(Node n1, Node n2, Node tree, Block b) {
    int forwardOK;
    Node pointedTo;
    fprintf(stderr, "Linkage failure in %s\n", name);
    prettytree(n1);
    fprintf(stderr, "is not linked to...\n");
    prettytree(n2);
    forwardOK = n1->x.next == n2;
    fprintf(stderr, "%s link is broken and points to ...\n", forwardOK ? "Backward" : "Forward");
    pointedTo = forwardOK ? n2->x.prev : n1->x.next;
    if (pointedTo)
        prettytree(pointedTo);
    else 
        fprintf(stderr, "NULL\n");
    fprintf(stderr, "In tree:\n");
    prettytree(tree);
    fprintf(stderr, "In block:\n");
    block_print(b, stderr);
    exit(-1);
}

static void checkLinkage(Block block) {
    Node p, start, end, lastTemp, x;
    int count = 0;
    // Forward
    end = block_lastNode(block)->x.next;
    for (p = block_firstNode(block); p != end; p = p->x.next) {
        count++;    
        if (count > 10000) {
            fprintf(stderr, "Block contains over 100 000 trees - Probably looped linkage.\n");
            prettytree(p);
            exit(-1);
        }
    }
    // And back again    
    start = block_firstNode(block)->x.prev;
    for (p = block_lastNode(block); p != start; p = p->x.prev);
//    assert(p == NULL);
    // Check temps are linked.
    lastTemp = NULL;
    for (p = block_firstNode(block); p != end; p = p->x.next) {
        if (x = temps(p, &lastTemp, 1)) {
            linkageFailure(lastTemp, x, p, block);
        }
    }
    lastTemp = NULL;
    for (p = block_lastNode(block); p != start; p = p->x.prev) {
        if (x = temps(p, &lastTemp, 0)) {
            linkageFailure(lastTemp, x, p, block);
        }
    }
}

static int checkDuplicate(Node p) {
    if (p == NULL)
        return 0;
    if (p->x.duplicate) {
        fprintf(stderr, "Verify failed in %s\n", name);
        fprintf(stderr, "Duplicate Node ");
        prettytree(p);
        return 1;
    }
    p->x.duplicate = 1;
    return checkDuplicate(p->kids[0]) | checkDuplicate(p->kids[1]);
}

static void resetDuplicate(Node p) {
   if (p == NULL)
       return;
   p->x.duplicate = 0;
   resetDuplicate(p->kids[0]);
   resetDuplicate(p->kids[1]);
}

static void verifyLiveness() {
    int i, j, size;
    LOG(("Verifying liveness\n"));
    size = flow_size();
    for (i = 0; i < size; i++) {
        Block b = flow_block(i);
        BitSet test = set_clone(block_livein(b));
        BitSet children;
//       set_addSet(test, block_use(b));
//        set_removeSet(test, block_def(b));
//        assert(set_equals(test, block_livein(b)));
        set_clear(test);
        set_addSet(test, block_use(b));
        set_addSet(test, block_def(b));
        assert(set_size(test) == set_size(block_use(b)) + set_size(block_def(b)));
        set_clear(test);
        children = flow_children(i);
        FOR_EACH(j, children) {
             Block child = flow_block(j);
             set_addSet(test, block_livein(child));
        }
        if (!set_equals(test, block_liveout(b))) {
            fprintf(stderr, "Verify failed in %s\n", name);
            fprintf(stderr, "Incorrect liveness in block\n");
            flow_printNode(i, stderr);
            fprintf(stderr, "Children liveness:\n");
            children = flow_children(i);
            FOR_EACH(j, children) {
                fprintf(stderr, "Child %d live-in: ", j);
                set_print(stderr, block_livein(flow_block(j)));
                fprintf(stderr, "\n");
            }
            exit(-1);
        }
    }
}

static void noDuplicates(Block block) {
    Node p, end;
    end = block_lastNode(block)->x.next;
    for (p = block_firstNode(block); p != end; p = p->x.next) {
        resetDuplicate(p);  
    }
    for (p = block_firstNode(block); p != end; p = p->x.next) {
        if (checkDuplicate(p)) {
            fprintf(stderr, "in\n");
            prettytree(p);
            exit(-1);
        }
    }
    for (p = block_firstNode(block); p != end; p = p->x.next) {
        resetDuplicate(p);  
    }
}

int node_size(Node p) {
    int result = 0;
    if (opsize(p->op) <= IR->ptrmetric.size || optype(p->op) == B) {
        return result + 1;
    } else {
        return result + 2;
    }
}

#define CHECK_DEPTH(p) {int i = getEDepth(p) - (*depth) - (*p_depth); if (i) return i; }

static int nodeDepth(Node p, int* depth, int* p_depth) {
    int start = *depth;
    if (p == NULL)
        return 0;
    switch(generic(p->op)) {
    case ASGN:
        CHECK(nodeDepth(p->kids[0], depth, p_depth));
        CHECK(nodeDepth(p->kids[1], depth, p_depth));
 /*       switch(generic(p->kids[0]->op)) {
        case VREG: 
        case ADDRL: case ADDRF: case ADDRG: case STACK:
            CHECK(nodeDepth(p->kids[1], depth, p_depth));
            CHECK(nodeDepth(p->kids[0], depth, p_depth));
            break;
        default:
            CHECK(nodeDepth(p->kids[0], depth, p_depth));
            CHECK(nodeDepth(p->kids[1], depth, p_depth));
        } */
        *depth = start;
        return 0;
    case ARG:
        CHECK(nodeDepth(p->kids[0], depth, p_depth));
        (*p_depth) += node_size(p);
        return 0;
    case VREG: case STACK: case COPY:
        CHECK_DEPTH(p);
        break;
    case TUCK:
        CHECK(nodeDepth(p->kids[0], depth, p_depth));
        break;
    case CALL:
        CHECK(nodeDepth(p->kids[0], depth, p_depth));
        if (p->kids[1]) {
            nodeDepth(p->kids[1], depth, p_depth);
        }
        (*p_depth) = 0;
        break; 
    case INDIR:
        CHECK(nodeDepth(p->kids[0], depth, p_depth));
        (*depth) += NODE_SIZE(p) - 1;
        break;
    case BCOM: case CVF: case CVI: case CVP: case CVU: case NEG:
        CHECK(nodeDepth(p->kids[0], depth, p_depth));
        break;
    case ADDRL: case ADDRF: case ADDRG: 
        (*depth)++;
        break;
    case CNST:
        (*depth) += NODE_SIZE(p);
        break;
    case ADD: case BAND: case BOR: case BXOR: case DIV: case LSH: case MOD:
    case RSH: case SUB: case MUL:
        CHECK(nodeDepth(p->kids[0], depth, p_depth));
        CHECK(nodeDepth(p->kids[1], depth, p_depth));
        break;
    case RET:
        if (p->kids[0]) {
            nodeDepth(p->kids[0], depth, p_depth);
        }
        return 0;
    case LT: case EQ: case NE: case LE: case GT: case GE:
        CHECK(nodeDepth(p->kids[0], depth, p_depth));
        CHECK(nodeDepth(p->kids[1], depth, p_depth));
        *depth = start;
        return 0;
    case LABEL:
        return 0;
    case JUMP:
        CHECK(nodeDepth(p->kids[0], depth, p_depth));
        *depth = start;
        return 0;
    case NOOP:
        return 0;
    default:
        fprintf(stderr, "%s at %d\n", opname(p->op), __LINE__);
        exit(-1);
    }
    *depth = start + node_size(p);
    return 0;
}

static int treeDepth(Node p, int* depth) {
    int start = 0;
    int x = nodeDepth(p, &start, depth);
    if (x) {
        if (start != 0)
            *depth += start;
    } 
    return x;
}

#define CHECK_L_DEPTH(p) {int i = (p)->x.l_depth - (*depth); if (i) { prettytree(p); return i; } }

static int lAsgn(Node p, int* depth) {
    if (p == NULL)
        return 0;
    switch(generic(p->op)) {
    case VREG: 
        CHECK_L_DEPTH(p);
        return 0;
    case ADDRL: case ADDRG: 
        return 0;
    case STACK:
        (*depth)++;
        return 0;
    default:
        fprintf(stderr, "%s at %d\n", opname(p->op), __LINE__);
        exit(-1);
        return -1; // Keep compiler happy.
    }
}

static int treeLDepth(Node p, int* depth) {
    if (p == NULL)
        return 0;
    switch(generic(p->op)) {
    case ASGN:
        CHECK(treeLDepth(p->kids[0], depth));
        switch(generic(p->kids[1]->op)) {
        case VREG: case ADDRL: case ADDRG: case STACK:
            CHECK(lAsgn(p->kids[1], depth));
            break;
        default:
            CHECK(treeLDepth(p->kids[1], depth));
        }
        return 0;
    case TUCK:
//        CHECK_L_DEPTH(p);
        (*depth)++;
        return 0;
    case INDIR:       
        switch(generic(p->kids[0]->op)) {
        case STACK:
            CHECK_L_DEPTH(p->kids[0]);
            (*depth)-= NODE_SIZE(p);
            return 0;
        case VREG: case COPY:
            CHECK_L_DEPTH(p->kids[0]);
        case ADDRL: case ADDRG:
            return 0;         
        default:
            CHECK(treeLDepth(p->kids[0], depth));
            return 0;
        }
    case VREG: case COPY:
        CHECK_L_DEPTH(p);
        return 0;
    default:
        if (p->kids[0]) {
            CHECK(treeLDepth(p->kids[0], depth));
            if (p->kids[1])
                CHECK(treeLDepth(p->kids[1], depth));
        }
        return 0;
    }
}

#define PRINT_BLOCK 1

static void verifyLDepths(Block block) {
    Node p, end;
    int l_depth, block_start;
    l_depth = block_start = block_getStartLDepth(block);
    end = block_lastNode(block)->x.next;
    for (p = block_firstNode(block); p != end; p = p->x.next) {
        int d = treeLDepth(p, &l_depth);
        if (d) {
            fprintf(stderr, "Verify failed in tree:\n");
            prettytree(p);
            fprintf(stderr, "\nL-depth at block start: %d. Computed l-depth: %d. Marked l-depth %d.\n",
                            block_start, l_depth, d + l_depth);
            fprintf(stderr, "In block:\n");
            block_printDepths(block);
            exit(-1);
        }
    }
    if (l_depth != block_getEndLDepth(block)) {
        fprintf(stderr, "Final l-depth is incorrect. Calculated %d. Marked %d\n", l_depth, block_getEndLDepth(block)); 
        fprintf(stderr, "Verify failed in block:\n");
        block_printDepths(block);
        exit(-1);
    }
}

void verifyDepths(Block block) {
    Node p, end;
    int e_depth, block_start;
    e_depth = block_start = block_getStartEDepth(block);
    end = block_lastNode(block)->x.next;
    for (p = block_firstNode(block); p != end; p = p->x.next) {
        int d = treeDepth(p, &e_depth);
        if (d) {
            fprintf(stderr, "Verify failed in tree:\n");
            prettytree(p);
            fprintf(stderr, "\nDepth at block start: %d. Computed e-depth: %d. Marked e-depth %d.\n",
                            block_start, e_depth, d + e_depth);
            fprintf(stderr, "In block:\n");
            block_printDepths(block);
            exit(-1);
        }
    }
}

int verify_delve(Node p) {
    if (generic(p->op) == STACK || generic(p->op) == COPY) {
        if (p->syms[1] == NULL) {
            fprintf(stderr, "No delve marked in ");
            return 1;               
        } else if (getDelve(p) > IR->x.depth) {
            fprintf(stderr, "Delve too deep in");
            return 1;
        }
    } else {
        if (p->kids[0] && verify_delve(p->kids[0]))
            return 1;
        if (p->kids[1] && verify_delve( p->kids[1]))
            return 1;
    }
    return 0;
}

void verifyDelve(Block b) {
    Node p, end;
    end = block_lastNode(b)->x.next;
    for (p = block_firstNode(b); p != end; p = p->x.next) {
        if (verify_delve(p)) {
            prettytree(p);
            fprintf(stderr, "In block\n");
            block_printDepths(b);
            exit(-1);
        }
    }
}

void verifyDefn(Block b) {
    Node p, end;
    LOG(("Verfiying defns\n"));
    end = block_lastNode(b)->x.next;
    for (p = block_firstNode(b); p != end; p = p->x.next) {
        if (generic(p->op) == ASGN) {
            Node kid = p->kids[0];
            if (kid->x.defn == 0 && kid->op == VREG+P) {
                fprintf(stderr, "Definition not marked\n");
                prettytree(p);
                if (p->kids[1]->x.defn) {
                    fprintf(stderr, "Rvalue marked as defn\n");
                }
                exit(-1);
            }           
        }
    }
}

static void block(Block b) {
    verifyDelve(b);
    verifyDefn(b);
    checkLinkage(b);
    noDuplicates(b);
    verifyDepths(b);
}