/*
** Copyright (C) 2018 Martin Brain
**
** This program is free software: you can redistribute it and/or modify
** it under the terms of the GNU General Public License as published by
** the Free Software Foundation, either version 3 of the License, or
** (at your option) any later version.
** 
** This program is distributed in the hope that it will be useful,
** but WITHOUT ANY WARRANTY; without even the implied warranty of
** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
** GNU General Public License for more details.
** 
** You should have received a copy of the GNU General Public License
** along with this program.  If not, see <http://www.gnu.org/licenses/>.
*/

#include "symfpu/baseTypes/cprover_exprt.h"

#include <util/simplify_expr.h>
#include <util/namespace.h>
#include <util/symbol_table.h>

#include <solvers/symfpu/boolbv_graph.h>
#include <solvers/symfpu/boolbv_symfpu.h>

#define THERE_BE_DRAGONS

#ifdef THERE_BE_DRAGONS
// GCC needs LINKFLAGS="-rdynamic" to give function names in the backtrace
#include <execinfo.h>
#include <cxxabi.h>
#endif

namespace symfpu {
  namespace cprover_exprt {

    #define BITS 32

    roundingMode traits::RNE (void) {
      return roundingMode(from_integer(0/*ieee_floatt::ROUND_TO_EVEN*/, signedbv_typet(BITS)));
    }
    
    roundingMode traits::RNA (void) {
      return roundingMode(from_integer(4, signedbv_typet(BITS)));
    }
    
    roundingMode traits::RTP (void) {
      return roundingMode(from_integer(2/*ieee_floatt::ROUND_TO_PLUS_INF*/, signedbv_typet(BITS)));
    }
    
    roundingMode traits::RTN (void) {
      return roundingMode(from_integer(1/*ieee_floatt::ROUND_TO_MINUS_INF*/, signedbv_typet(BITS)));
    }

    roundingMode traits::RTZ (void) {
      return roundingMode(from_integer(3/*ieee_floatt::ROUND_TO_ZERO*/, signedbv_typet(BITS)));
    }

#ifdef THERE_BE_DRAGONS
    // The following code is evil and insane
    // It exists to add labels in code generated by boolbvt_graph.h

    struct demangledName {
      std::string path;
      std::string mangledName;
      std::string demangledName;
      std::string remainder;
    };

/// Attempts to demangle the function name assuming the glibc
/// format of stack entry:
///
/// path '(' mangledName '+' offset ') [' address ']\0'
///
/// \param out: The output stream
/// \param stack_entry: Description of the stack_entry
///
/// \return True <=> the entry has been successfully demangled and printed.

    static demangledName demangle(const std::string &stack_entry)
    {
      demangledName return_value = {"Not found", "Not found", "Not found", stack_entry};

      std::string working(stack_entry);

      std::string::size_type start=working.rfind('(');  // Path may contain '(' !
      std::string::size_type end=working.find('+', start);

      return_value.path = working.substr(0, start - 1);
      
      if(start!=std::string::npos &&
	 end!=std::string::npos &&
	 start+1<=end-1)
      {
	std::string::size_type length=end-(start+1);
	std::string mangled(working.substr(start+1, length));
	return_value.mangledName = mangled;
	
	int demangle_success=1;
	char * demangled =
	  abi::__cxa_demangle(mangled.c_str(), nullptr, nullptr, &demangle_success);

	if(demangle_success==0)
	{
	  return_value.demangledName = demangled;
	}
	else
	{
	  return_value.demangledName = "Demangle failed";
	}
      } else {
	return_value.mangledName = "Mangled name not found";
	return_value.demangledName = "Nothing to demangle";	  
      }

      return_value.remainder = working.substr(end + 1);

      return return_value;
    }

    typedef std::pair<std::string, std::string> creation_context;
    
    static creation_context find_creation_context (void) {
      void * stack[50] = {};
      
      std::size_t entries = backtrace(stack, sizeof(stack) / sizeof(void *));
      char **description = backtrace_symbols(stack, entries);
    
      std::string locationPrefix;
      std::string locationPostfix;

      // Start at the right place to avoid the C shim which doesn't decode
      #define MAGIC_START 4

      // Avoid the introspection of this code
      #define MAGIC_END 3
      for(std::size_t i=entries - MAGIC_START; i>MAGIC_END; i--)
      {
	demangledName d = demangle(description[i]);

	if (d.demangledName.find("symfpu::") == 0 &&
	    // !(d.demangledName.find("symfpu::cprover_exprt") == 0) &&  
	    d.demangledName.find("symfpu::ite") == std::string::npos &&
	    d.demangledName.find("symfpu::ITE") == std::string::npos &&
	    d.demangledName.find("symfpu::unpackedFloat") != std::string::npos
	    )
	{
	  locationPrefix += "subgraph \"cluster_" + d.demangledName + "\" {\n";
	  locationPrefix += "label = \"" + d.demangledName + "\"\n";
	  locationPostfix += "}\n";
	}
      }
      free(description);

      return creation_context(locationPrefix, locationPostfix);
    }

    static void apply_creation_context_rec (const creation_context &ct, exprt &e) {
      e.set("#creation_open", ct.first);
      e.set("#creation_close", ct.second);

      // In some cases multiple exprts have been created between tags.
      // Naive recursion is bad!
      Forall_operands(e_it, e)
      {
	if (e_it->get_comments().find("#creation_open") == e_it->get_comments().end())
	  apply_creation_context_rec(ct, *e_it);
      }
      return;
    }
    
    static exprt apply_creation_context (const exprt &e) {
      creation_context ct = find_creation_context();
      
      exprt ei(e);
      
      if (ct.first.empty())
	return ei;

      apply_creation_context_rec(ct, ei);

      return ei;
    }
    
#endif

    exprt proposition::tag (const exprt &e) const {
      #ifdef THERE_BE_DRAGONS
      if (boolbv_grapht::graph_enable)
	return apply_creation_context(e);
      #endif
      return e;
    }

    template <bool isSigned>
    exprt bitVector<isSigned>::tag (const exprt &e) const {
      #ifdef THERE_BE_DRAGONS
      if (boolbv_grapht::graph_enable)
	return apply_creation_context(e);
      #endif
      return e;
    }
    
    // Instantiate
    template exprt bitVector<true>::tag (const exprt &e) const;
    template exprt bitVector<false>::tag (const exprt &e) const;
    

#define INLINESIMP

    // Inline simplification as simplify_expr does not scale


    // Just to reduce the visual clutter
    exprt simplify_local_constant_fold (const exprt e) {
      if (e.id() == ID_constant) {
	return e;

      } else {
	/*
	exprt check_target(e);

	while (check_target.id() == ID_typecast ||
	       check_target.id() == ID_extractbits)
	{
	  check_target = check_target.op0();
	}
	
	forall_operands(it, check_target)
	*/
	forall_operands(it, e)
	{
	  if ((*it).id() != ID_constant)
	    return e;
	}

	symbol_tablet s;
	namespacet n(s);
	return simplify_expr(e, n);
      }
    }
    
    
    exprt simplify_if (const if_exprt i) {
      const exprt cond(i.cond());
      const exprt true_case(i.true_case());
      const exprt false_case(i.false_case());
      
      // Start with the simple ones
      if (cond.is_true() || (true_case == false_case)) {
	return true_case;
	  
      } else if (cond.is_false()) {
	return false_case;
	  
      } else { 
	// Compact if's
	if (true_case.id() == ID_if) {
	  if_exprt l(to_if_expr(true_case));
	  
	  if (l.true_case() == false_case) {
	    return simplify_if(if_exprt(and_exprt(cond, not_exprt(l.cond())),
					l.false_case(),
					false_case));
	  } else if (l.false_case() == false_case) {
	    return simplify_if(if_exprt(and_exprt(cond, l.cond()),
					l.true_case(),
					false_case));
	  }
	  
	} else if (false_case.id() == ID_if) {
	  if_exprt l(to_if_expr(false_case));
	  
	  if (l.true_case() == true_case) {
	    return simplify_if(if_exprt(and_exprt(not_exprt(cond), not_exprt(l.cond())),
					l.false_case(),
					true_case));
	  } else if (l.false_case() == true_case) {
	    return simplify_if(if_exprt(and_exprt(not_exprt(cond), l.cond()),
					l.true_case(),
					true_case));
	  }
	}
      }

      return i;
    }

    exprt proposition::simplify (const exprt &e) const {
#ifndef INLINESIMP
      return e;
#endif
      exprt r(simplify_local_constant_fold(e));
      if (r.id() == ID_constant)
	return r;

      if (e.id() == ID_if) {
	exprt s(simplify_if(to_if_expr(e)));

	// Additional simplifications for Boolean things
	if (s.id() == ID_if) {
	  if_exprt i(to_if_expr(s));

	  if (i.true_case().is_true()) {
	    return simplify(or_exprt(i.cond(), i.false_case()));
	    
	  } else if (i.true_case().is_false()) {
	    return simplify(and_exprt(not_exprt(i.cond()), i.false_case()));
	    
	  } else if (i.false_case().is_true()) {
	    return simplify(or_exprt(not_exprt(i.cond()), i.true_case()));
	    
	  } else if (i.false_case().is_false()) {
	    return simplify(and_exprt(i.cond(), i.true_case()));
	    
	  }

	  assert(!i.cond().is_constant());
	  assert(!i.true_case().is_constant());
	  assert(!i.false_case().is_constant());
	}

	return s;
	
      } else if (e.id() == ID_not) {
	if (e.op0().id() == ID_not) {
	  return simplify(e.op0().op0());
	}
	
      } else if (e.id() == ID_and) {
	exprt::operandst operands(e.operands());

	size_t i = 0;
	while (i < operands.size()) {
	  if (operands[i].is_true()) {
	    operands.erase(operands.begin() + i);
	    
	  } else if (operands[i].is_false()) {
	    return operands[i];
	    
	  } else if (operands[i].id() == ID_and) {
	    exprt::operandst appendMe(operands[i].operands());
	    for (size_t j = 0; j < appendMe.size(); ++j) {
	      operands.push_back(appendMe[j]);
	    }
	    operands.erase(operands.begin() + i);
	    
	  } else if (operands[i].id() == ID_not &&
		     operands[i].op0().id() == ID_or) {
	    exprt::operandst negateMe(operands[i].op0().operands());
	    for (size_t j = 0; j < negateMe.size(); ++j) {
	      operands.push_back(not_exprt(negateMe[j]));
	    }
	    operands.erase(operands.begin() + i);

	  } else {
	    bool duplicate = false;

	    for (size_t j = 0; j < i; ++j) {
	      if (operands[j] == operands[i]) {
		duplicate = true;
		break;
	      }
	    }

	    if (duplicate) {
	      operands.erase(operands.begin() + i);
	    } else {
	      ++i;
	    }
	  }
	}

	if (operands.size() == 0) {
	  return true_exprt();
	} else if (operands.size() == 1) {
	  return operands[0];
	} else {
	  return conjunction(operands);
	}

      } else if (e.id() == ID_or) {
	exprt::operandst operands(e.operands());

	size_t i = 0;
	while (i < operands.size()) {
	  if (operands[i].is_false()) {
	    operands.erase(operands.begin() + i);
	    
	  } else if (operands[i].is_true()) {
	    return operands[i];
	    
	  } else if (operands[i].id() == ID_or) {
	    exprt::operandst appendMe(operands[i].operands());
	    for (size_t j = 0; j < appendMe.size(); ++j) {
	      operands.push_back(appendMe[j]);
	    }
	    operands.erase(operands.begin() + i);
	    
	  } else if (operands[i].id() == ID_not &&
		     operands[i].op0().id() == ID_and) {
	    exprt::operandst negateMe(operands[i].op0().operands());
	    for (size_t j = 0; j < negateMe.size(); ++j) {
	      operands.push_back(not_exprt(negateMe[j]));
	    }
	    operands.erase(operands.begin() + i);

	  } else {
	    bool duplicate = false;

	    for (size_t j = 0; j < i; ++j) {
	      if (operands[j] == operands[i]) {
		duplicate = true;
		break;
	      }
	    }

	    if (duplicate) {
	      operands.erase(operands.begin() + i);
	    } else {
	      ++i;
	    }
	  }
	}

	if (operands.size() == 0) {
	  return false_exprt();
	} else if (operands.size() == 1) {
	  return operands[0];
	} else {
	  return disjunction(operands);
	}

      } else if (e.id() == ID_equal) {
	if (e.op0() == e.op1())
	  return true_exprt();
      }
      
      return e;
    }

    template <bool isSigned>
    exprt bitVector<isSigned>::simplify (const exprt &e) const {
#ifndef INLINESIMP
      return e;
#endif

      exprt r(simplify_local_constant_fold(e));
      if (r.id() == ID_constant)
	return r;
      
      if (e.id() == ID_if) {
	return simplify_if(to_if_expr(e));
      }
      
      return e;
    }
    
    // Instantiate
    template exprt bitVector<true>::simplify (const exprt &e) const;
    template exprt bitVector<false>::simplify (const exprt &e) const;
  }


  // Use improved version of some of the operations
#ifndef SYMFPU_WORDLEVEL_ENCODINGS
  template <>
  cprover_exprt::traits::ubv orderEncode<cprover_exprt::traits, cprover_exprt::traits::ubv> (const cprover_exprt::traits::ubv &b) {
    return orderEncodeBitwise<cprover_exprt::traits, cprover_exprt::traits::ubv>(b);
  }

  template <>
  stickyRightShiftResult<cprover_exprt::traits> stickyRightShift (const cprover_exprt::traits::ubv &input, const cprover_exprt::traits::ubv &shiftAmount) {
    return stickyRightShiftBitwise<cprover_exprt::traits>(input, shiftAmount);
  }
#endif
  
  template <>
  void probabilityAnnotation<cprover_exprt::traits, cprover_exprt::traits::prop> (const cprover_exprt::traits::prop &p, const probability &pr) {
    boolbv_symfput::probablity_annotations.insert(std::make_pair(p, pr));
    return;
  }

}