#include <fxos/domains.h>
#include <fxos/util.h>
#include <fxos/lang.h>
#include <stdexcept>

namespace FxOS {

//---
// Quick helpers
//---

auto const Top = RelConst::Top;
auto const Bottom = RelConst::Bottom;

/* General prelude that propagates Top, then Bottom */
#define special(r1, r2) {					\
	if((r1).spe == Top || (r2).spe == Top) return top();	\
	if((r1).spe || (r2).spe) return bottom();		\
}

RelConst RelConstDomain::bottom() const noexcept
{
	RelConst b {};
	b.spe = Bottom;
	return b;
}

RelConst RelConstDomain::top() const noexcept
{
	RelConst b {};
	b.spe = Top;
	return b;
}

RelConst RelConstDomain::constant(uint32_t value) const noexcept
{
	RelConst b {};
	b.uval = value;
	return b;
}

bool RelConstDomain::is_constant(RelConst r) const noexcept
{
	return r.base == 0;
}

//---
// Basic arithmetic
//---

RelConst RelConstDomain::minus(RelConst r) const noexcept
{
	/* Propagate Bottom and Top */
	if(r.spe) return r;
	/* This domain does not support multiplicative coefficients for the
	   base. If the base is non-zero, return Top. */
	if(r.base) return top();

	r.ival = -r.ival;
	return r;
}

RelConst RelConstDomain::add(RelConst r1, RelConst r2) const noexcept
{
	special(r1, r2);

	/* This domain does not support cumulative bases. The sum can only be
	   represented if at least one of the values has no base */
	if(r1.base && r2.base) return top();

	RelConst r;
	r.base = r1.base | r2.base;
	r.uval = r1.uval + r2.uval;
	return r;
}

RelConst RelConstDomain::sub(RelConst r1, RelConst r2) const noexcept
{
	/* This domain does not support difference between bases. The
	   difference can only be represented in a few restricted cases. */
	special(r1, r2);

	/* If r2 has no base, keep r1's base. */
	if(!r2.base)
	{
		r1.uval -= r2.uval;
		return r1;
	}

	/* If r2 has exactly the same base as r1, cancel it. */
	if(r1.base == r2.base)
	{
		r1.base = 0;
		r1.uval -= r2.uval;
		return r1;
	}

	/* Otherwise, the result cannot be represented. */
	return top();
}

RelConst RelConstDomain::smul(RelConst r1, RelConst r2) const noexcept
{
	/* No base can be multiplied except by 1. Typically there will be no
	   such constant because it would be optimized away. */
	special(r1, r2);

	/* Give up if there is any base */
	if(r1.base || r2.base) return top();

	/* Multiply with sign */
	r1.ival *= r2.ival;
	return r1;
}

RelConst RelConstDomain::umul(RelConst r1, RelConst r2) const noexcept
{
	special(r1, r2);
	if(r1.base || r2.base) return top();

	r1.uval *= r2.uval;
	return r1;
}

//---
// Sign extensions
//---

RelConst RelConstDomain::extub(RelConst r) const noexcept
{
	/* The representation does not support sign extensions on bases, so we
	   just return top whenever there is one. */
	if(r.spe) return r;
	if(r.base) return top();

	r.uval = (uint8_t)r.uval;
	return r;
}

RelConst RelConstDomain::extsb(RelConst r) const noexcept
{
	if(r.spe) return r;
	if(r.base) return top();

	r.ival = (int8_t)r.ival;
	return r;
}

RelConst RelConstDomain::extuw(RelConst r) const noexcept
{
	if(r.spe) return r;
	if(r.base) return top();

	r.uval = (uint16_t)r.uval;
	return r;
}

RelConst RelConstDomain::extsw(RelConst r) const noexcept
{
	if(r.spe) return r;
	if(r.base) return top();

	r.ival = (int16_t)r.ival;
	return r;
}

//---
// Logical operations
//---

RelConst RelConstDomain::lnot(RelConst r) const noexcept
{
	/* Don't try to catch very special cases */
	if(r.spe) return r;
	if(r.base) return top();

	r.uval = ~r.uval;
	return r;
}

RelConst RelConstDomain::land(RelConst r1, RelConst r2) const noexcept
{
	special(r1, r2);
	if(r1.base || r2.base) return top();

	r1.uval &= r2.uval;
	return r1;
}

RelConst RelConstDomain::lor(RelConst r1, RelConst r2) const noexcept
{
	special(r1, r2);
	if(r1.base || r2.base) return top();

	r1.uval |= r2.uval;
	return r1;
}

RelConst RelConstDomain::lxor(RelConst r1, RelConst r2) const noexcept
{
	special(r1, r2);
	if(r1.base || r2.base) return top();

	r1.uval ^= r2.uval;
	return r1;
}

//---
// Comparisons
//---

/* TODO: RelConst comparison improvements using typing

   Two values base+d1 and base+d2 (sharing the same base) can be proven to
   compare as unsigned if the base has a known type and d1 and d2 are smaller
   than the size of that type. This derives from the implicit assumption that a
   full object cannot cross from P4 space to P0. */

bool RelConstDomain::cmp(RelConst r1, RelConst r2) const noexcept
{
	/* Not very good */
	return (r1.base == 0 && r2.base == 0);
}

int RelConstDomain::cmpu(RelConst r1, RelConst r2) const noexcept
{
	/* We can't just subtract because of overflows (information is lost
	   because we don't have the V bit) */
	return (r1.uval > r2.uval) - (r1.uval < r2.uval);
}

int RelConstDomain::cmps(RelConst r1, RelConst r2) const noexcept
{
	return (r1.ival > r2.ival) - (r1.ival < r2.ival);
}

//---
// Other functions
//---

RelConst::operator bool () const noexcept
{
	return !spe;
}

std::string RelConst::str() const noexcept
{
	using RegName = CpuRegister::CpuRegisterName;

	if(!base && !uval) return "0";
	if(spe == Bottom) return "Bottom";
	if(spe == Top) return "Top";

	std::string str;
	if(arg) str = format("arg%d", arg);
	if(org) str = format("org_%s", CpuRegister((RegName)org).str());
	if(reg) str = CpuRegister((RegName)org).str();

	if(!uval) return str;

	if(ival >= -256 && ival < 256)
	{
		uint32_t v = 0;
		if(str.size() && ival > 0) str += "+", v = ival;
		if(str.size() && ival < 0) str += "-", v = -ival;

		return str + format("%d", v);
	}
	else
	{
		return str + format("%08x", uval);
	}
}

} /* namespace FxOS */