//---------------------------------------------------------------------------//
//  1100101 |_ mov #0, r4         __                                         //
//     11   |_ <0xb380 %5c4>     / _|_ _____ ___                             //
//     0110 |_ 3.50 -> 3.60     |  _\ \ / _ (_-<                             //
//          |_ base# + offset   |_| /_\_\___/__/                             //
//---------------------------------------------------------------------------//

#include <fxos/analysis.h>
#include <fmt/core.h>
#include <cassert>

namespace FxOS {

void ProgramState::setFunctionInit()
{
    // TODO: Analysis: Set symbolic parameters at function entry
    for(int i = 0; i < 16; i++)
        m_regs[i] = RelConstDomain().top();
}

void ProgramState::setBottom()
{
    for(int i = 0; i < 16; i++)
        m_regs[i] = RelConstDomain().bottom();
}

void ProgramState::applyDiff(ProgramStateDiff const &diff)
{
    RelConstDomain RCD;
    int t = diff.target();

    if(t == static_cast<int>(ProgramStateDiff::Target::None)) {
        /* Nothing */
    }
    else if(t == static_cast<int>(ProgramStateDiff::Target::Unknown)) {
        for(int i = 0; i < 16; i++)
            m_regs[i] = RCD.top();
    }
    else {
        assert((unsigned)t < 16 && "invalid register target");
        m_regs[t] = diff.value();
    }
}

void ProgramState::joinWith(ProgramState const &other)
{
    RelConstDomain RCD;

    for(int i = 0; i < 16; i++) {
        m_regs[i] = RCD.join(m_regs[i], other.getRegister(i));
    }
}

bool ProgramState::le(ProgramState const &other) const
{
    RelConstDomain RCD;

    for(int i = 0; i < 16; i++) {
        if(!RCD.le(m_regs[i], other.getRegister(i)))
            return false;
    }
    return true;
}

std::string ProgramState::str(int indentLength) const
{
    std::string indent(indentLength, ' ');
    std::string str;

    /* Registers */
    for(int i = 0; i < 16; i++) {
        if(i % 4 == 0) {
            str += (i > 0 ? "\n" : "");
            str += indent;
        }
        else
            str += "   ";

        str += fmt::format("r{}:{}", i, m_regs[i].str());
    }

    return str + "\n";
}

std::string ProgramStateDiff::str() const
{
    if(m_target == static_cast<int>(Target::None))
        return "()";
    if(m_target == static_cast<int>(Target::Unknown))
        return "⊤";

    return fmt::format("r{} ← {}", m_target, m_value.str());
}

/* Information stored for each block during the fixpoint iteration */
struct BlockStates
{
    ProgramState entry;
    std::vector<ProgramStateDiff> diffs;
    ProgramState exit;
    ProgramState nextEntry;
};

static ProgramStateDiff interpretInstruction(
    Instruction const &ins, ProgramState const &PS)
{
    RelConstDomain RCD;
    ProgramStateDiff diff;
    diff.setUnknown();

    // TODO: Do this properly
    u16 opc = ins.opcode().opcode;
    if((opc & 0xf000) == 0xe000) {
        int reg = (opc >> 8) & 0xf;
        int val = (int8_t)opc;
        diff.setRegisterUpdate(reg, RCD.constant(val));
    }

    return diff;
}

static void interpretBlock(BasicBlock const &bb, BlockStates &states)
{
    ProgramState PS(states.entry);
    states.diffs.clear();

    for(Instruction const &i: bb) {
        ProgramStateDiff diff = interpretInstruction(i, PS);
        states.diffs.push_back(diff);
        PS.applyDiff(diff);
    }

    states.exit = PS;
}

std::unique_ptr<StaticFunctionAnalysis> analyzeFunction(Function const &f)
{
    std::vector<BlockStates> VBS;

    /* Initialize all blocks' entry states */
    for(uint i = 0; i < f.blockCount(); i++) {
        BlockStates BS;
        if(i == 0)
            BS.entry.setFunctionInit();
        else
            BS.entry.setBottom();
        VBS.push_back(BS);
    }

    /* The naive iteration strategy */
    while(true) {
        /* Interpret all blocks on their current states */
        for(uint i = 0; i < f.blockCount(); i++)
            interpretBlock(f.basicBlockByIndex(i), VBS[i]);

        /* Compute the next entry state for each block */
        for(uint i = 0; i < f.blockCount(); i++) {
            BasicBlock const &bb = f.basicBlockByIndex(i);
            VBS[i].nextEntry.setBottom();

            for(int succIndex: bb.successorsByIndex())
                VBS[i].nextEntry.joinWith(VBS[succIndex].exit);
        }

        /* Determine whether a fixpoint has been reached yet */
        bool pfp = std::all_of(VBS.begin(), VBS.end(),
            [](BlockStates &BS) { return BS.nextEntry.le(BS.entry); });

        if(pfp)
            break;

        /* Switch to next state */
        for(uint i = 0; i < f.blockCount(); i++)
            VBS[i].entry = VBS[i].nextEntry;
    }

    auto an = std::make_unique<StaticFunctionAnalysis>();
    for(uint i = 0; i < f.blockCount(); i++) {
        StaticFunctionAnalysis::Block B;
        B.entry = VBS[i].entry;
        B.diffs = std::move(VBS[i].diffs);
        an->blocks.push_back(std::move(B));
    }

    return an;
}

} /* namespace FxOS */