//---------------------------------------------------------------------------//
//  1100101 |_ mov #0, r4         __                                         //
//     11   |_ <0xb380 %5c4>     / _|_ _____ ___                             //
//     0110 |_ 3.50 -> 3.60     |  _\ \ / _ (_-<                             //
//          |_ base# + offset   |_| /_\_\___/__/                             //
//---------------------------------------------------------------------------//
// fxos/ai/RelConst: Abstract domain of relative constants
//
// This abstract domain represents values of the form <base + offset> where
// the base is a register, a symbolic function argument, or the initial value
// of a callee-saved register in a function, and the offset is a constant.
//
// I designed this domain for this particular application, although there are
// surely similar takes in decompilation literature.
//
// For readers not familiar with abstract interpretation, the idea is that one
// can run a program by calculating not the exact values being manipulated,
// but instead approximations ("abstractions") of these. The extra freedom
// provided by the approximation makes it possible to defines methods of
// execution that always terminate, thus analyzing any program in finite time.
// This particular domain does little in the way of approximation, but has
// benefits because of its ability to track some symbolic values.
//---

#ifndef FXOS_AI_RELCONST_H
#define FXOS_AI_RELCONST_H

#include <fxos/ai/AbstractDomain.h>
#include <string>

namespace FxOS {

/* The lattice of relative constants (base + offset) */
struct RelConst
{
    enum { Bottom = 1, Top = 2 };

    /* The following fields concurrently indicate the base. The order of
       resolution is as follows (non-trivial types in parentheses):
       * If [spe] is equal to Bottom or Top, this is the value.
       * If [arg] is non-zero, the value of the arg-th argument is used.
       * If [org] is non-zero, the original value of the associated
         callee-saved register is used. (CpuRegister)
       * If [reg] is non-zero, the base is that register. (CpuRegister)

       For efficiency, checking [base==0] will tell apart plain old
       constants from values with bases (and specials but these are usually
       handled first). */
    union
    {
        struct
        {
            uint8_t spe;
            uint8_t arg;
            uint8_t org;
            uint8_t reg;
        };
        uint32_t base;
    };

    /* The constant value, or offset. The signedness of this value depends
       on the context where it is used:

       * For special values, the members are unused.
       * For [arg] and [org] and [reg] bases with additive offset
         semantics, the signedness has no effect. Operations with
         non-trivial effect on signs such as multiplication are not
         supported with bases.
       * For zero bases, the interpretation is instruction-dependent. */
    union
    {
        int32_t ival;
        uint32_t uval;
    };

    //---
    // RelConst methods
    //---

    /* Default constructors gives zero */
    RelConst() = default;

    /* Evaluates to true if the location is non-trivial, ie. if it is
       neither Top nor Bottom. */
    operator bool() const noexcept;

    /* String representation */
    std::string str() const noexcept;
};

class RelConstDomain: public AbstractDomain<RelConst>
{
public:
    /* Trivial instances */
    RelConstDomain() = default;

    /* Implementation of the AbstractDomain specification */

    RelConst bottom() const noexcept override;
    RelConst top() const noexcept override;

    RelConst constant(uint32_t value) const noexcept override;
    bool is_constant(RelConst) const noexcept override;
    uint32_t constant_value(RelConst) const noexcept override;

    RelConst minus(RelConst) const noexcept override;
    RelConst add(RelConst, RelConst) const noexcept override;
    RelConst sub(RelConst, RelConst) const noexcept override;
    RelConst smul(RelConst, RelConst) const noexcept override;
    RelConst umul(RelConst, RelConst) const noexcept override;

    RelConst extub(RelConst) const noexcept override;
    RelConst extsb(RelConst) const noexcept override;
    RelConst extuw(RelConst) const noexcept override;
    RelConst extsw(RelConst) const noexcept override;

    RelConst lnot(RelConst) const noexcept override;
    RelConst land(RelConst, RelConst) const noexcept override;
    RelConst lor(RelConst, RelConst) const noexcept override;
    RelConst lxor(RelConst, RelConst) const noexcept override;

    bool cmp(RelConst, RelConst) const noexcept override;
    int cmpu(RelConst, RelConst) const noexcept override;
    int cmps(RelConst, RelConst) const noexcept override;
};

} /* namespace FxOS */

#endif /* FXOS_AI_RELCONST_H */