// Copyright 2013-2019 Stanford University
//
// Licensed under the Apache License, Version 2.0 (the License);
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an AS IS BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.


#include "src/symstate/bitvector.h"
#include "src/symstate/pretty_visitor.h"

#include <sstream>

using namespace std;
using namespace stoke;

thread_local SymMemoryManager* SymBitVector::memory_manager_ = NULL;
uint64_t SymBitVector::tmp_counter_ = 0;

#ifdef STOKE_UF_MULTIPLICATION
std::map<size_t, SymFunction*> SymBitVector::multiplication_functions_;
#endif


/* Various constructors */
SymBitVector SymBitVector::constant(uint16_t size, uint64_t value) {
  return SymBitVector(new SymBitVectorConstant(size, value));
}
/*
SymBitVector SymBitVector::constant(cpputil::BitVector v) {
  SymBitVector result;
  for(size_t i = 0; i < v.size()/8; ++i) {
    result = result || v.get_fixed_byte(i);
  }
  return result;
}*/
SymBitVector SymBitVector::var(uint16_t size, string name) {
  return SymBitVector(new SymBitVectorVar(size, name));
}
SymBitVector SymBitVector::tmp_var(uint16_t size) {
  stringstream name;
  name << "TMP_BV_" << size << "_" << tmp_counter_;
  tmp_counter_++;
  return SymBitVector(new SymBitVectorVar(size, name.str()));
}
SymBitVector SymBitVector::from_bool(const SymBool& b) {
  auto c0 = SymBitVector::constant(1,0);
  auto c1 = SymBitVector::constant(1,1);
  return SymBitVector(new SymBitVectorIte(b.ptr, c1.ptr, c0.ptr));
}

/* Bit Vector Operators */
SymBitVector SymBitVector::operator&(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorAnd(ptr, other.ptr));
}

SymBitVector SymBitVector::operator||(const SymBitVector& other) const {
  if (!other.ptr) {
    return *this;
  }
  if (!ptr) {
    return other;
  }
  return SymBitVector(new SymBitVectorConcat(ptr, other.ptr));
}

SymBitVector SymBitVector::operator/(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorDiv(ptr, other.ptr));
}

SymBitVector SymBitVector::operator-(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorMinus(ptr, other.ptr));
}

SymBitVector SymBitVector::operator%(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorMod(ptr, other.ptr));
}

SymBitVector SymBitVector::operator*(const SymBitVector& other) const {
#ifdef STOKE_UF_MULTIPLICATION
  uint16_t bits = width();
  auto mf = multiplication_functions_[bits];
  if (mf == nullptr) {
    stringstream name;
    name << "bv_multiply_" << bits;
    mf = new SymFunction(name.str(), bits, { bits, bits });
    multiplication_functions_[bits] = mf;
  }
  return (*mf)(*this, other);
#else
  return SymBitVector(new SymBitVectorMult(ptr, other.ptr));
#endif
}

SymBitVector SymBitVector::operator!() const {
  return SymBitVector(new SymBitVectorNot(ptr));
}

SymBitVector SymBitVector::operator|(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorOr(ptr, other.ptr));
}

SymBitVector SymBitVector::operator+(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorPlus(ptr, other.ptr));
}

SymBitVector SymBitVector::rol(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorRotateLeft(ptr, other.ptr));
}

SymBitVector SymBitVector::ror(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorRotateRight(ptr, other.ptr));
}

SymBitVector SymBitVector::operator<<(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorShiftLeft(ptr, other.ptr));
}

SymBitVector SymBitVector::operator>>(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorShiftRight(ptr, other.ptr));
}

SymBitVector SymBitVector::operator<<(uint64_t shift) const {
  auto size = ptr->width_;

  auto constant = SymBitVector::constant(size, shift);
  return (*this << constant);
}

SymBitVector SymBitVector::operator>>(uint64_t shift) const {
  auto size = ptr->width_;

  auto constant = SymBitVector::constant(size, shift);
  return (*this >> constant);
}

SymBitVector SymBitVector::s_div(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorSignDiv(ptr, other.ptr));
}

SymBitVector SymBitVector::extend(uint16_t size) const {
  return sign_extend(size);
}
SymBitVector SymBitVector::sign_extend(uint16_t size) const {
  if (size <= width())
    return *this;
  return SymBitVector(new SymBitVectorSignExtend(ptr, size));
}

SymBitVector SymBitVector::zero_extend(uint16_t size) const {
  auto old_size = width();
  if (old_size < size) {
    auto diff = size-old_size;
    return SymBitVector::constant(diff, 0) || *this;
  } else {
    return *this;
  }
}

SymBitVector SymBitVector::s_mod(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorSignMod(ptr, other.ptr));
}

SymBitVector SymBitVector::s_shr(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorSignShiftRight(ptr, other.ptr));
}

SymBitVector SymBitVector::operator-() const {
  return SymBitVector(new SymBitVectorUMinus(ptr));
}

SymBitVector SymBitVector::operator^(const SymBitVector& other) const {
  return SymBitVector(new SymBitVectorXor(ptr, other.ptr));
}

/* Parity */
SymBool SymBitVector::parity() const {

  // Step 1: get my size
  uint16_t size = (*this).width();

  // Step 2: iterate over my bits and xor them together
  SymBool parity = (*this)[0];
  for (size_t i = 1; i < size; ++i) {
    parity = parity ^ (*this)[i];
  }

  // Step 3: flip
  return !parity;
}

/* Indexing */
SymBitVector SymBitVector::IndexHelper::operator[](uint16_t index) const {
  return SymBitVector(new SymBitVectorExtract(bv_.ptr, index_, index));
}

SymBitVector::IndexHelper::operator SymBool() const {
  return (*this)[index_] == SymBitVector::constant(1,1);
}

/* Bit Vector Comparison Operators */
SymBool SymBitVector::operator==(const SymBitVector& other) const {
  return SymBool(new SymBoolEq(ptr, other.ptr));
}

SymBool SymBitVector::operator>=(const SymBitVector& other) const {
  return SymBool(new SymBoolGe(ptr, other.ptr));
}

SymBool SymBitVector::operator>(const SymBitVector& other) const {
  return SymBool(new SymBoolGt(ptr, other.ptr));
}

SymBool SymBitVector::operator<=(const SymBitVector& other) const {
  return SymBool(new SymBoolLe(ptr, other.ptr));
}

SymBool SymBitVector::operator<(const SymBitVector& other) const {
  return SymBool(new SymBoolLt(ptr, other.ptr));
}

SymBool SymBitVector::operator!=(const SymBitVector& other) const {
  return !(*this == other);
}

SymBool SymBitVector::s_ge(const SymBitVector& other) const {
  return SymBool(new SymBoolSignGe(ptr, other.ptr));
}

SymBool SymBitVector::s_gt(const SymBitVector& other) const {
  return SymBool(new SymBoolSignGt(ptr, other.ptr));
}

SymBool SymBitVector::s_le(const SymBitVector& other) const {
  return SymBool(new SymBoolSignLe(ptr, other.ptr));
}

SymBool SymBitVector::s_lt(const SymBitVector& other) const {
  return SymBool(new SymBoolSignLt(ptr, other.ptr));
}

/** Get the type */
SymBitVector::Type SymBitVector::type() const {
  if (ptr)
    return ptr->type();
  else
    return NONE;
}

/** Get the bit width. */
uint16_t SymBitVector::width() const {
  if (ptr)
    return ptr->width_;
  else
    return 0;
}

/* equality */
bool SymBitVector::equals(const SymBitVector& other) const {
  if (ptr && other.ptr)
    return ptr->equals(other.ptr);
  else
    return ptr == other.ptr;
}

bool SymBitVectorArrayLookup::equals(const SymBitVectorAbstract * other) const {
  if (other->type() != this->type()) return false;
  auto cast = static_cast<const SymBitVectorArrayLookup * const>(other);
  return a_->equals(cast->a_) && key_->equals(cast->key_);
}



/* Output overload */
std::ostream& std::operator<< (std::ostream& out, const stoke::SymBitVector& bv) {
  SymPrettyVisitor spv(out);
  spv(bv);
  return out;
}

