#include <iostream>

#include "llvm/IR/InstrTypes.h"
#include "llvm/IR/Instruction.h"

#include "SymbolicInterpreter.h"

#define ADD         13      ///    +
#define SUB         15      ///    -
#define MUL         17      ///    *
#define SDIV        20      ///    /
#define SREM        23      ///    %

#define ICMP_EQ     32  ///< equal
#define ICMP_NE     33  ///< not equal
#define ICMP_SGT    38  ///< signed greater than
#define ICMP_SGE    39  ///< signed greater or equal
#define ICMP_SLT    40  ///< signed less than
#define ICMP_SLE    41  ///< signed less or equal
#define ICMP_UGT    34  ///< unsigned greater than
#define ICMP_UGE    35  ///< unsigned greater or equal
#define ICMP_ULT    36  ///< unsigned less than
#define ICMP_ULE    37  ///< unsigned less or equal

extern SymbolicInterpreter SI;
using namespace z3;
using namespace std;
/**
 * Implement your transfer functions.
 */

/// DSE_Alloca(getRegisterId(%x),%x)
/// Reg(%x) => 0x1000
extern "C" void __DSE_Alloca__(int R, int *Ptr) {
    expr e = SI.getContext().int_val(*Ptr);
    auto address = Address(R);
    SI.getMemory().insert(make_pair(address, e));
}

extern "C" void __DSE_Store__(int *X) {
    expr e = SI.getStack().top();
    SI.getStack().pop();
    if(e.to_string().at(0) == 'R'){
        e = SI.getMemory().at(e);
    }
    auto address = Address(X);
    SI.getMemory().insert(make_pair(address, e));
    SI.getMemory().at(address) = e;
}

extern "C" void __DSE_Load__(int Y, int *X) {
    expr e = SI.getMemory().at(Address(X));
    auto address = Address(Y);
    SI.getMemory().insert(make_pair(address, e));
    SI.getMemory().at(address) = e;
}

extern "C" void __DSE_Label__(int RID, int BID, int label){
    expr el = SI.getMemory().at(Address(RID));
    auto address = Address(BID);
    expr t = SI.getContext().bool_val(true);
    expr f = SI.getContext().bool_val(false);
    if(label){
        SI.getMemory().insert(make_pair(address, el == t));
        SI.getMemory().at(address) = (el == t);
    } else{
        SI.getMemory().insert(make_pair(address, el == f));
        SI.getMemory().at(address) = (el == f);
    }
}

extern "C" void __DSE_Loop__(int Type){
    expr type = SI.getContext().int_val(Type);
    SI.getStack().push(type);
}

extern "C" void __DSE_ICmp__(int R, int Op) {
    expr el = SI.getStack().top();
    SI.getStack().pop();
    expr er = SI.getStack().top();
    SI.getStack().pop();
    if(el.to_string().at(0) == 'R'){
        el = SI.getMemory().at(el);
    }
    if(er.to_string().at(0) == 'R'){
        er = SI.getMemory().at(er);
    }
    expr res = el == er;
    switch (Op) {
        case ICMP_EQ:
            res = el == er;
            break;
        case ICMP_NE:
            res = el != er;
            break;
        case ICMP_SLT:
            res = el < er;
            break;
        case ICMP_SLE:
            res = el <= er;
            break;
        case ICMP_SGT:
            res = el > er;
            break;
        case ICMP_SGE:
            res = el >= er;
        default:
            break;
    }
    auto address = Address(R);
    SI.getMemory().insert(make_pair(address, res));
    SI.getMemory().at(address) = res;
}

extern "C" void __DSE_BinOp__(int R, int Op) {
    expr el = SI.getStack().top();
    SI.getStack().pop();
    expr er = SI.getStack().top();
    SI.getStack().pop();
    if(el.to_string().at(0) == 'R'){
        el = SI.getMemory().at(el);
    }
    if(er.to_string().at(0) == 'R'){
        er = SI.getMemory().at(er);
    }
    expr res = el + er;
    switch (Op) {
        case ADD:
            res = el + er;
            break;
        case SUB:
            res = el - er;
            break;
        case MUL:
            res = el * er;
            break;
        case SDIV:
            res = el / er;
            break;
        case SREM:
            res = el % er;
            break;
        default:
            break;
    }
    auto address = Address(R);
    SI.getMemory().insert(make_pair(address, res));
    SI.getMemory().at(address) = res;
}
