#include <stdlib.h>
#include <string.h>

#include "cbmcLLRBContext.h"

/* for CBMC */
extern void enumerateInputs_stub(struct Context*);
extern void verifySpecification_stub(struct Context*);

/* definitions from llrb */
extern void meta(struct Context*, enum Code next);
extern void put_stub(struct Context*);
extern void replaceNode_stub(struct Context*);
extern void insertNode_stub(struct Context*);
extern void rotateLeft_stub(struct Context*);
extern void rotateRight_stub(struct Context*);
extern void colorFlip_stub(struct Context*);
extern void fixUp_stub(struct Context*);
extern void changeReference_stub(struct Context*);
extern void insert1_stub(struct Context*);
extern void insert2_stub(struct Context*);
extern void insert3_stub(struct Context*);
extern void insert4_stub(struct Context*);
extern void insert4_1_stub(struct Context*);
extern void insert4_2_stub(struct Context*);
extern void insert5_stub(struct Context*);
extern void stackClear_stub(struct Context*);
extern void get_stub(struct Context*);
extern void search_stub(struct Context*);
extern void delete_stub(struct Context*);
extern void delete1_stub(struct Context*);
extern void delete2_stub(struct Context*);
extern void delete3_stub(struct Context*);
extern void replaceNodeForDelete1_stub(struct Context*);
extern void replaceNodeForDelete2_stub(struct Context*);
extern void findMax1_stub(struct Context*);
extern void findMax2_stub(struct Context*);
extern void deleteCase1_stub(struct Context*);
extern void deleteCase2_stub(struct Context*);
extern void deleteCase3_stub(struct Context*);
extern void deleteCase4_stub(struct Context*);
extern void deleteCase5_stub(struct Context*);
extern void deleteCase6_stub(struct Context*);
extern void exitCode(struct Context*);

/* for allocator */
extern void allocator(struct Context* context);


void initLLRBContext(struct Context* context, enum Code next) {
    context->codeNum   = Exit;

    context->heapLimit = sizeof(union Data)*ALLOCATE_SIZE;
    context->code      = malloc(sizeof(void*)*(context->codeNum+1));
    context->data      = malloc(sizeof(union Data*)*ALLOCATE_SIZE);
    context->heapStart = malloc(context->heapLimit);
    memset(context->heapStart, 0, context->heapLimit);

    context->code[EnumerateInputs]     = enumerateInputs_stub;;
    context->code[VerifySpecification] = verifySpecification_stub;

    /* definitions from llrb */
    context->code[Put]           = put_stub;
    context->code[Replace]       = replaceNode_stub;
    context->code[Insert]        = insertNode_stub;
    context->code[RotateL]       = rotateLeft_stub;
    context->code[RotateR]       = rotateRight_stub;
    context->code[InsertCase1]   = insert1_stub;
    context->code[InsertCase2]   = insert2_stub;
    context->code[InsertCase3]   = insert3_stub;
    context->code[InsertCase4]   = insert4_stub;
    context->code[InsertCase4_1] = insert4_1_stub;
    context->code[InsertCase4_2] = insert4_2_stub;
    context->code[InsertCase5]   = insert5_stub;
    context->code[StackClear]    = stackClear_stub;
    context->code[Exit]          = exitCode;

    context->heap = context->heapStart;

    context->data[Allocate] = context->heap;
    context->heap += sizeof(struct Allocate);

    context->data[Tree] = context->heap;
    context->heap += sizeof(struct Tree);

    context->data[Node] = context->heap;
    context->heap += sizeof(struct Node);

    context->dataNum = Node;

    struct Tree* tree = &context->data[Tree]->tree;
    tree->root = 0;
    tree->current = 0;
    tree->deleted = 0;

    context->node_stack = stack_init(sizeof(struct Node*), 1000);
    context->code_stack = stack_init(sizeof(enum Code), 1000);

    context->loopCount = 0;

    return meta(context, next);
}