//---
// fxos.domains: Abstract interpretation domains
//---

#ifndef FXOS_DOMAINS_H
#define FXOS_DOMAINS_H

#include <cstdint>
#include <string>

namespace FxOS {

/* An abstract domain over a user-defined lattice. */
template<typename T>
class AbstractDomain
{
public:
	/* Bottom and Top constants */
	virtual T bottom() const noexcept = 0;
	virtual T top()    const noexcept = 0;

	/* Construct abstract value from integer constant */
	virtual T constant(uint32_t value) const noexcept = 0;
	/* Check if value is constant */
	virtual bool is_constant(T) const noexcept = 0;
	/* Unpack a constant */
	virtual uint32_t constant_value(T) const = 0;

	/* Basic arithmetic. Division and modulo are both non-trivial
	   instruction sequences usually isolated in easily-identifiable
	   subroutines, so we don't care about them. */
	virtual T minus(T)     const noexcept = 0;
	virtual T add(T, T)    const noexcept = 0;
	virtual T sub(T, T)    const noexcept = 0;
	virtual T smul(T, T)   const noexcept = 0;
	virtual T umul(T, T)   const noexcept = 0;

	/* Sign extensions */
	virtual T extub(T)     const noexcept = 0;
	virtual T extsb(T)     const noexcept = 0;
	virtual T extuw(T)     const noexcept = 0;
	virtual T extsw(T)     const noexcept = 0;

	/* Logical operations */
	virtual T lnot(T)      const noexcept = 0;
	virtual T land(T, T)   const noexcept = 0;
	virtual T lor(T, T)    const noexcept = 0;
	virtual T lxor(T, T)   const noexcept = 0;

	/* Comparisons. This operation proceeds in two steps:
	   * First call cmp(x, y) to check if the values are comparable. If
	     this returns false, the test result should be Top.
	   * If the values are comparable, call cmpu(x, y) or cmps(x, y), which
	     returns a negative number if x < y, 0 if x == y, and a positive
	     number if x > y. */
	virtual bool cmp(T, T) const noexcept = 0;
	virtual int cmpu(T, T) const noexcept = 0;
	virtual int cmps(T, T) const noexcept = 0;
};

//---
// Domain of relative constants
//---

/* 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 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_DOMAINS_H */