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

#include <fxos/analysis.h>
#include <fxos/util/log.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 if(t == static_cast<int>(ProgramStateDiff::Target::CallStandard)) {
        for(int i = 0; i < 7; 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 ProgramStateDiff::str() const
{
    if(m_target == static_cast<int>(Target::None))
        return "()";
    if(m_target == static_cast<int>(Target::Unknown))
        return "⊤";
    if(m_target == static_cast<int>(Target::CallStandard))
        return "call(std)";

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

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

static u32 computeConstantOperand(Instruction const &ins, AsmOperand const &op)
{
    Binary const &binary = ins.parentBinary();
    u32 target;

    assert(op.isConstant() && "analysis of constant operands is out of sync");

    switch(op.kind()) {
    case AsmOperand::PcRel:
        target = op.getPCRelativeTarget(ins.address());

        if(!binary.vspace().covers(target, op.opsize())) {
            FxOS_log(ERR, "constant operand reads out of vspace bounds");
            return -1;
        }
        if(op.opsize() == 1)
            return binary.vspace().read_i8(target);
        if(op.opsize() == 2)
            return binary.vspace().read_i16(target);
        if(op.opsize() == 4)
            return binary.vspace().read_i32(target);

        FxOS_log(ERR, "PcRel operand with no opsize");
        return -1;

    case AsmOperand::PcJump:
    case AsmOperand::PcAddr:
        return op.getPCRelativeTarget(ins.address());

    case AsmOperand::Imm:
        return op.imm();

    default:
        assert(false && "not a constant operand");
        __builtin_unreachable();
    }
}

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

    AsmInstruction asmins = ins.opcode();

    switch(asmins.operation()) {

    /* Moves */
    case AsmInstruction::SH_mov:
    case AsmInstruction::SH_ldc:
    case AsmInstruction::SH_lds:
    case AsmInstruction::SH_stc:
    case AsmInstruction::SH_sts:
    case AsmInstruction::SH_mova: {
        AsmOperand src = asmins.operand(0);
        AsmOperand dst = asmins.operand(1);

        if(!dst.isReg())
            diff.setNoop();
        else if(src.isConstant()) {
            RelConst c = RCD.constant(computeConstantOperand(ins, src));
            diff.setRegisterUpdate(dst.base().getR(), c);
        }
        else
            diff.setRegisterTouched(dst.base().getR());
        break;
    }

    /* Opaque instructions with one operand and one output */
    case AsmInstruction::SH_dt:
    case AsmInstruction::SH_movt:
    case AsmInstruction::SH_rotl:
    case AsmInstruction::SH_rotr:
    case AsmInstruction::SH_rotcl:
    case AsmInstruction::SH_rotcr:
    case AsmInstruction::SH_shal:
    case AsmInstruction::SH_shar:
    case AsmInstruction::SH_shll:
    case AsmInstruction::SH_shlr:
    case AsmInstruction::SH_shll2:
    case AsmInstruction::SH_shlr2:
    case AsmInstruction::SH_shll8:
    case AsmInstruction::SH_shlr8:
    case AsmInstruction::SH_shll16:
    case AsmInstruction::SH_shlr16: {
        AsmOperand op = asmins.operand(0);
        assert(op.isReg());

        if(op.base().getR() >= 0)
            diff.setRegisterTouched(op.base().getR());
        else
            diff.setNoop();
        break;
    }

    /* Opaque instructions with two operands and one output */
    case AsmInstruction::SH_add:
    case AsmInstruction::SH_addc:
    case AsmInstruction::SH_addv:
    case AsmInstruction::SH_and:
    case AsmInstruction::SH_div1:
    case AsmInstruction::SH_exts:
    case AsmInstruction::SH_extu:
    case AsmInstruction::SH_neg:
    case AsmInstruction::SH_negc:
    case AsmInstruction::SH_not:
    case AsmInstruction::SH_or:
    case AsmInstruction::SH_shad:
    case AsmInstruction::SH_shld:
    case AsmInstruction::SH_sub:
    case AsmInstruction::SH_subc:
    case AsmInstruction::SH_subv:
    case AsmInstruction::SH_swap:
    case AsmInstruction::SH_xor:
    case AsmInstruction::SH_xtrct: {
        AsmOperand op = asmins.operand(1);

        if(op.isReg() && op.base().getR() >= 0)
            diff.setRegisterTouched(op.base().getR());
        else
            diff.setNoop();
        break;
    }

    /* No-op instructions that affect state not modeled by the analysis */
    case AsmInstruction::SH_clrs:
    case AsmInstruction::SH_clrt:
    case AsmInstruction::SH_clrmac:
    case AsmInstruction::SH_div0u:
    case AsmInstruction::SH_ldtlb:
    case AsmInstruction::SH_nop:
    case AsmInstruction::SH_rte:
    case AsmInstruction::SH_rts:
    case AsmInstruction::SH_sets:
    case AsmInstruction::SH_sett:
    case AsmInstruction::SH_sleep:
    case AsmInstruction::SH_cmp_pl:
    case AsmInstruction::SH_cmp_pz:
    case AsmInstruction::SH_cmp_eq:
    case AsmInstruction::SH_cmp_hs:
    case AsmInstruction::SH_cmp_ge:
    case AsmInstruction::SH_cmp_hi:
    case AsmInstruction::SH_cmp_gt:
    case AsmInstruction::SH_cmp_str:
    case AsmInstruction::SH_div0s:
    case AsmInstruction::SH_dmuls:
    case AsmInstruction::SH_dmulu:
    case AsmInstruction::SH_mul:
    case AsmInstruction::SH_muls:
    case AsmInstruction::SH_mulu:
    case AsmInstruction::SH_tst:
    case AsmInstruction::SH_jmp:
    case AsmInstruction::SH_pref:
    case AsmInstruction::SH_tas:
    case AsmInstruction::SH_mac:
    case AsmInstruction::SH_braf:
    case AsmInstruction::SH_bf:
    case AsmInstruction::SH_bf_s:
    case AsmInstruction::SH_bt:
    case AsmInstruction::SH_bt_s:
    case AsmInstruction::SH_bra:
    case AsmInstruction::SH_trapa:
    case AsmInstruction::SH_icbi:
    case AsmInstruction::SH_ocbi:
    case AsmInstruction::SH_ocbp:
    case AsmInstruction::SH_ocbwb:
    case AsmInstruction::SH_prefi:
    case AsmInstruction::SH_synco:
        diff.setNoop();
        break;

    case AsmInstruction::SH_bsr:
    case AsmInstruction::SH_bsrf:
    case AsmInstruction::SH_jsr:
        diff.setCallStandard();
        break;

    case AsmInstruction::SH_movco:
    case AsmInstruction::SH_movli:
    case AsmInstruction::SH_movua:
    case AsmInstruction::SH_movca:
        diff.setUnknown();
        break;
    }

    for(auto op: ins.opcode().operands()) {
        /* TODO: Properly handle pre-decr/post-dec */
        if(op.kind() == AsmOperand::PreDec || op.kind() == AsmOperand::PostInc)
            diff.setUnknown();
    }

    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 == f.entryBlockIndex())
            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 = VBS[i].entry;

            for(int predIndex: bb.predecessorsByIndex())
                VBS[i].nextEntry.joinWith(VBS[predIndex].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 */