diff mbox series

[RFC/RFA,v6,09/12] Add symbolic execution support.

Message ID CAE65F3O3yMH_A20Ck=vYL=iMYdfJajgUD=wXD=-5CV-R1-n-VA@mail.gmail.com
State New
Headers show
Series CRC optimization. | expand

Commit Message

Mariam Arutunian Nov. 9, 2024, 6:40 p.m. UTC
Gives an opportunity to execute the code on bit level,
assigning symbolic values to the variables which don't have initial values.
Supports only CRC specific operations.

Example:

uint8_t crc;
uint8_t pol = 1;
crc = crc ^ pol;

during symbolic execution crc's value will be:
crc(8), crc(7), ... crc(1), crc(0) ^ 1

  gcc/

    * Makefile.in (OBJS): Add sym-exec/sym-exec-expression.o,
    sym-exec/sym-exec-state.o, sym-exec/sym-exec-condition.o.
    * configure (sym-exec): New subdir.

  gcc/sym-exec/

    * sym-exec-condition.cc: New file.
    * sym-exec-condition.h: New file.
    * sym-exec-expression-is-a-helper.h: New file.
    * sym-exec-expression.cc: New file.
    * sym-exec-expression.h: New file.
    * sym-exec-state.cc: New file.
    * sym-exec-state.h: New file.

Signed-off-by: Mariam Arutunian <mariamarutunian@gmail.com>
Author: Matevos Mehrabyan <matevosmehrabyan@gmail.com>
Co-authored-by: Mariam Arutunian <mariamarutunian@gmail.com>
Mentored-by: Jeff Law <jlaw@ventanamicro.com>
diff mbox series

Patch

---
 gcc/Makefile.in                          |    3 +
 gcc/configure                            |    2 +-
 gcc/sym-exec/sym-exec-condition.cc       |   59 +
 gcc/sym-exec/sym-exec-condition.h        |   33 +
 gcc/sym-exec/sym-exec-expr-is-a-helper.h |  204 ++
 gcc/sym-exec/sym-exec-expression.cc      |  426 +++++
 gcc/sym-exec/sym-exec-expression.h       |  260 +++
 gcc/sym-exec/sym-exec-state.cc           | 2148 ++++++++++++++++++++++
 gcc/sym-exec/sym-exec-state.h            |  436 +++++
 9 files changed, 3570 insertions(+), 1 deletion(-)
 create mode 100644 gcc/sym-exec/sym-exec-condition.cc
 create mode 100644 gcc/sym-exec/sym-exec-condition.h
 create mode 100644 gcc/sym-exec/sym-exec-expr-is-a-helper.h
 create mode 100644 gcc/sym-exec/sym-exec-expression.cc
 create mode 100644 gcc/sym-exec/sym-exec-expression.h
 create mode 100644 gcc/sym-exec/sym-exec-state.cc
 create mode 100644 gcc/sym-exec/sym-exec-state.h

diff --git a/gcc/Makefile.in b/gcc/Makefile.in
index a7054eda9c5..6eab34d62bb 100644
--- a/gcc/Makefile.in
+++ b/gcc/Makefile.in
@@ -1718,6 +1718,9 @@  OBJS = \
 	tree-logical-location.o \
 	tree-loop-distribution.o \
 	gimple-crc-optimization.o \
+	sym-exec/sym-exec-expression.o \
+	sym-exec/sym-exec-state.o \
+	sym-exec/sym-exec-condition.o \
 	tree-nested.o \
 	tree-nrv.o \
 	tree-object-size.o \
diff --git a/gcc/configure b/gcc/configure
index 3d301b6ecd3..c781f4c24b6 100755
--- a/gcc/configure
+++ b/gcc/configure
@@ -36232,7 +36232,7 @@  $as_echo "$as_me: executing $ac_file commands" >&6;}
     "depdir":C) $SHELL $ac_aux_dir/mkinstalldirs $DEPDIR ;;
     "gccdepdir":C)
   ${CONFIG_SHELL-/bin/sh} $ac_aux_dir/mkinstalldirs build/$DEPDIR
-  for lang in $subdirs c-family common analyzer text-art rtl-ssa
+  for lang in $subdirs c-family common analyzer text-art rtl-ssa sym-exec
   do
       ${CONFIG_SHELL-/bin/sh} $ac_aux_dir/mkinstalldirs $lang/$DEPDIR
   done ;;
diff --git a/gcc/sym-exec/sym-exec-condition.cc b/gcc/sym-exec/sym-exec-condition.cc
new file mode 100644
index 00000000000..ef3f1e3fda5
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-condition.cc
@@ -0,0 +1,59 @@ 
+#include "sym-exec-condition.h"
+
+bit_condition::bit_condition (value_bit *left, value_bit *right, tree_code code)
+{
+  this->m_left = left;
+  this->m_right = right;
+  this->m_code = code;
+  m_type = BIT_CONDITION;
+}
+
+
+bit_condition::bit_condition (const bit_condition &expr)
+{
+  bit_expression::copy (&expr);
+  m_code = expr.get_code ();
+}
+
+
+/* Returns the condition's code.  */
+
+tree_code
+bit_condition::get_code () const
+{
+  return m_code;
+}
+
+
+/* Returns a copy of the condition.  */
+
+value_bit *
+bit_condition::copy () const
+{
+  return new bit_condition (*this);
+}
+
+
+/* Prints the condition's sign.  */
+
+void
+bit_condition::print_expr_sign ()
+{
+  switch (m_code)
+    {
+      case GT_EXPR:
+	fprintf (dump_file, " > ");
+	break;
+      case LT_EXPR:
+	fprintf (dump_file, " < ");
+	break;
+      case EQ_EXPR:
+	fprintf (dump_file, " == ");
+	break;
+      case NE_EXPR:
+	fprintf (dump_file, " != ");
+	break;
+      default:
+	fprintf (dump_file, " ? ");
+    }
+}
\ No newline at end of file
diff --git a/gcc/sym-exec/sym-exec-condition.h b/gcc/sym-exec/sym-exec-condition.h
new file mode 100644
index 00000000000..1d9d59512bb
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-condition.h
@@ -0,0 +1,33 @@ 
+#ifndef SYM_EXEC_CONDITION_H
+#define SYM_EXEC_CONDITION_H
+
+#include "sym-exec-expression.h"
+
+enum condition_status {
+  CS_NO_COND,
+  CS_TRUE,
+  CS_FALSE,
+  CS_SYM
+};
+
+
+class bit_condition : public bit_expression {
+ private:
+  /* Condition's code.  */
+  tree_code m_code;
+
+  /* Prints the condition's sign.  */
+  void print_expr_sign ();
+
+ public:
+  bit_condition (value_bit *left, value_bit *right, tree_code type);
+  bit_condition (const bit_condition &expr);
+
+  /* Returns the condition's code.  */
+  tree_code get_code () const;
+
+  /* Returns a copy of the condition.  */
+  value_bit *copy () const;
+};
+
+#endif /* SYM_EXEC_CONDITION_H.  */
\ No newline at end of file
diff --git a/gcc/sym-exec/sym-exec-expr-is-a-helper.h b/gcc/sym-exec/sym-exec-expr-is-a-helper.h
new file mode 100644
index 00000000000..369213e5146
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-expr-is-a-helper.h
@@ -0,0 +1,204 @@ 
+#ifndef SYM_EXEC_EXPRESSION_IS_A_HELPER_H
+#define SYM_EXEC_EXPRESSION_IS_A_HELPER_H
+
+#include "sym-exec-condition.h"
+
+/* Defining test functions for value conversion via dyn_cast.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<symbolic_bit *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::SYMBOLIC_BIT;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_expression *>::test (value_bit *ptr)
+{
+  value_type type = ptr->get_type ();
+  return type == value_type::BIT_AND_EXPRESSION
+	 || type == value_type::BIT_OR_EXPRESSION
+	 || type == value_type::BIT_XOR_EXPRESSION
+	 || type == value_type::BIT_COMPLEMENT_EXPRESSION
+	 || type == value_type::SHIFT_RIGHT_EXPRESSION
+	 || type == value_type::SHIFT_LEFT_EXPRESSION
+	 || type == value_type::ADD_EXPRESSION
+	 || type == value_type::SUB_EXPRESSION
+	 || type == value_type::BIT_CONDITION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_and_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT_AND_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_or_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT_OR_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_xor_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT_XOR_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_complement_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT_COMPLEMENT_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_left_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::SHIFT_LEFT_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_right_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::SHIFT_RIGHT_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<add_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::ADD_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<sub_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::SUB_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_condition *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT_CONDITION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_and_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::BIT_AND_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_or_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::BIT_OR_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_xor_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::BIT_XOR_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_complement_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::BIT_COMPLEMENT_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_left_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::SHIFT_LEFT_EXPRESSION;
+}
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_right_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::SHIFT_RIGHT_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<add_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::ADD_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<sub_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::SUB_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_condition *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::BIT_CONDITION;
+}
+
+#endif /* SYM_EXEC_EXPRESSION_IS_A_HELPER_H.  */
\ No newline at end of file
diff --git a/gcc/sym-exec/sym-exec-expression.cc b/gcc/sym-exec/sym-exec-expression.cc
new file mode 100644
index 00000000000..d34ebce6d3c
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-expression.cc
@@ -0,0 +1,426 @@ 
+/* Every class defined here represents a single bit value of a variable.
+   Every variable will be represented as a vector of these classes which later
+   will be used for bit-level symbolic execution.  */
+
+#include "sym-exec-expr-is-a-helper.h"
+
+/* Returns type of the bit.  */
+
+value_type
+value_bit::get_type () const
+{
+  return m_type;
+}
+
+
+symbolic_bit::symbolic_bit (size_t i, tree orig)
+    : value_bit (i), m_origin (orig)
+{
+  m_type = SYMBOLIC_BIT;
+}
+
+
+bit::bit (unsigned char i) : m_val (i)
+{
+  m_type = BIT;
+}
+
+
+/* Returns left operand of the expression.  */
+
+value_bit *
+bit_expression::get_left ()
+{
+  return m_left;
+}
+
+
+/* Returns right operand of the expression.  */
+
+value_bit *
+bit_expression::get_right ()
+{
+  return m_right;
+}
+
+
+/* Sets left operand of the expression.  */
+
+void
+bit_expression::set_left (value_bit *expr)
+{
+  m_left = expr;
+}
+
+
+/* Sets right operand of the expression.  */
+
+void
+bit_expression::set_right (value_bit *expr)
+{
+  m_right = expr;
+}
+
+
+/* Returns the bit's initial index in bit-vector.  */
+
+size_t
+value_bit::get_index () const
+{
+  return m_index;
+}
+
+
+/* Returns the value of the bit.  */
+
+unsigned char
+bit::get_val () const
+{
+  return m_val;
+}
+
+
+/* Sets the value of the bit.  */
+
+void
+bit::set_val (unsigned char new_val)
+{
+  m_val = new_val;
+}
+
+
+bit_complement_expression::bit_complement_expression (value_bit *right)
+{
+  /* As complement has only one argument, we use only the m_right.  */
+  this->m_left = nullptr;
+  this->m_right = right;
+  m_type = BIT_COMPLEMENT_EXPRESSION;
+}
+
+
+bit_complement_expression::bit_complement_expression (
+  const bit_complement_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+bit_expression::~bit_expression ()
+{
+  delete m_left;
+  m_left = nullptr;
+  delete m_right;
+  m_right = nullptr;
+}
+
+
+/* Returns a copy of the bit.  */
+
+value_bit *
+symbolic_bit::copy () const
+{
+  return new symbolic_bit (*this);
+}
+
+
+/* Return a copy of the bit.  */
+
+value_bit *
+bit::copy () const
+{
+  return new bit (*this);
+}
+
+
+/* Copies the given expression to it by copying the left and right operands.  */
+
+void
+bit_expression::copy (const bit_expression *expr)
+{
+  if (expr->m_left)
+    m_left = expr->m_left->copy ();
+
+  if (expr->m_right)
+    m_right = expr->m_right->copy ();
+
+  m_type = expr->m_type;
+}
+
+
+/* Returns a copy of the expression.  */
+
+value_bit *
+bit_xor_expression::copy () const
+{
+  return new bit_xor_expression (*this);
+}
+
+
+/* Returns a copy of the expression.  */
+
+value_bit *
+bit_and_expression::copy () const
+{
+  return new bit_and_expression (*this);
+}
+
+
+/* Returns a copy of the expression.  */
+
+value_bit *
+bit_or_expression::copy () const
+{
+  return new bit_or_expression (*this);
+}
+
+
+/* Returns a copy of the expression.  */
+
+value_bit *
+shift_right_expression::copy () const
+{
+  return new shift_right_expression (*this);
+}
+
+
+/* Returns a copy of the expression.  */
+
+value_bit *
+shift_left_expression::copy () const
+{
+  return new shift_left_expression (*this);
+}
+
+
+/* Returns a copy of the expression.  */
+
+value_bit *
+add_expression::copy () const
+{
+  return new add_expression (*this);
+}
+
+
+/* Returns a copy of the expression.  */
+
+value_bit *
+sub_expression::copy () const
+{
+  return new sub_expression (*this);
+}
+
+
+/* Returns a copy of the expression.  */
+
+value_bit *
+bit_complement_expression::copy () const
+{
+  return new bit_complement_expression (*this);
+}
+
+
+bit_xor_expression::bit_xor_expression (value_bit *left, value_bit *right)
+{
+  this->m_left = left;
+  this->m_right = right;
+  m_type = BIT_XOR_EXPRESSION;
+}
+
+
+bit_xor_expression::bit_xor_expression (const bit_xor_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+bit_and_expression::bit_and_expression (value_bit *left, value_bit *right)
+{
+  this->m_left = left;
+  this->m_right = right;
+  m_type = BIT_AND_EXPRESSION;
+}
+
+
+bit_and_expression::bit_and_expression (const bit_and_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+bit_or_expression::bit_or_expression (value_bit *left, value_bit *right)
+{
+  this->m_left = left;
+  this->m_right = right;
+  m_type = BIT_OR_EXPRESSION;
+}
+
+
+bit_or_expression::bit_or_expression (const bit_or_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+shift_right_expression::shift_right_expression (value_bit *left,
+						value_bit *right)
+{
+  this->m_left = left;
+  this->m_right = right;
+  m_type = SHIFT_RIGHT_EXPRESSION;
+}
+
+
+shift_right_expression::shift_right_expression (
+  const shift_right_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+shift_left_expression::shift_left_expression (value_bit *left, value_bit *right)
+{
+  this->m_left = left;
+  this->m_right = right;
+  m_type = SHIFT_LEFT_EXPRESSION;
+}
+
+
+shift_left_expression::shift_left_expression (const shift_left_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+add_expression::add_expression (value_bit *left, value_bit *right)
+{
+  this->m_left = left;
+  this->m_right = right;
+  m_type = ADD_EXPRESSION;
+}
+
+
+add_expression::add_expression (const add_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+sub_expression::sub_expression (value_bit *left, value_bit *right)
+{
+  this->m_left = left;
+  this->m_right = right;
+  m_type = SUB_EXPRESSION;
+}
+
+
+sub_expression::sub_expression (const sub_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+/* Returns the origin of the bit, to whom it belongs.  */
+
+tree
+symbolic_bit::get_origin ()
+{
+  return m_origin;
+}
+
+
+/* Prints the bit.  */
+
+void
+symbolic_bit::print ()
+{
+  if (dump_file)
+    {
+      print_generic_expr (dump_file, m_origin, dump_flags);
+      fprintf (dump_file, "[%zu]", m_index);
+    }
+}
+
+
+/* Prints the bit.  */
+
+void
+bit::print ()
+{
+  if (dump_file)
+    fprintf (dump_file, "%u", m_val);
+}
+
+
+/* Depending on the expression, prints its sign.  */
+
+void
+bit_expression::print_expr_sign ()
+{
+  switch (m_type)
+    {
+      case BIT_XOR_EXPRESSION:
+	fprintf (dump_file, " ^ ");
+	break;
+      case BIT_AND_EXPRESSION:
+	fprintf (dump_file, " & ");
+	break;
+      case BIT_OR_EXPRESSION:
+	fprintf (dump_file, " | ");
+	break;
+      case SHIFT_RIGHT_EXPRESSION:
+	fprintf (dump_file, " >> ");
+	break;
+      case SHIFT_LEFT_EXPRESSION:
+	fprintf (dump_file, " << ");
+	break;
+      case ADD_EXPRESSION:
+	fprintf (dump_file, " + ");
+	break;
+      case SUB_EXPRESSION:
+	fprintf (dump_file, " - ");
+	break;
+      default:
+	fprintf (dump_file, " ?? ");
+    }
+}
+
+
+/* Prints the expression.  */
+
+void
+bit_expression::print ()
+{
+  if (dump_file)
+    {
+      fprintf (dump_file, "(");
+      if (m_left)
+	m_left->print ();
+      else
+	fprintf (dump_file, "null");
+
+      print_expr_sign ();
+
+      if (m_right)
+	m_right->print ();
+      else
+	fprintf (dump_file, "null");
+
+      fprintf (dump_file, ")");
+    }
+}
+
+
+/* Prints the expression.  */
+
+void
+bit_complement_expression::print ()
+{
+  if (dump_file)
+    {
+      fprintf (dump_file, "!");
+      if (m_right)
+	m_right->print ();
+      else
+	fprintf (dump_file, "null");
+    }
+}
\ No newline at end of file
diff --git a/gcc/sym-exec/sym-exec-expression.h b/gcc/sym-exec/sym-exec-expression.h
new file mode 100644
index 00000000000..36b90ffb374
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-expression.h
@@ -0,0 +1,260 @@ 
+/* Every class defined here represents a single bit value of a variable.
+   Every variable will be represented as a vector of these classes which later
+   will be used for bit-level symbolic execution.  */
+
+#ifndef SYM_EXEC_EXPRESSION_H
+#define SYM_EXEC_EXPRESSION_H
+
+#include "config.h"
+#include "system.h"
+#include "coretypes.h"
+#include "backend.h"
+#include "tree.h"
+#include "hwint.h"
+#include "gimple-pretty-print.h"
+#include "is-a.h"
+#include "vec.h"
+#include "hash-map.h"
+#include "hash-set.h"
+#include "stddef.h"
+
+/* Enum used for identifying the class of the bit.  */
+
+enum value_type {
+  SYMBOLIC_BIT,
+  BIT,
+  BIT_XOR_EXPRESSION,
+  BIT_AND_EXPRESSION,
+  BIT_OR_EXPRESSION,
+  BIT_COMPLEMENT_EXPRESSION,
+  SHIFT_RIGHT_EXPRESSION,
+  SHIFT_LEFT_EXPRESSION,
+  ADD_EXPRESSION,
+  SUB_EXPRESSION,
+  BIT_CONDITION
+};
+
+/* Base class for single bit value.  */
+
+class value_bit {
+ protected:
+  /* This will help us to understand where is moved the bit
+     from its initial position.  */
+  const size_t m_index;
+
+  /* Type of the bit.  Used by type checkers.  */
+  value_type m_type;
+
+ public:
+  value_bit () : m_index (0)
+  {};
+  value_bit (size_t i) : m_index (i)
+  {};
+  value_bit (const value_bit &val) : m_index (val.m_index)
+  {};
+
+  /* Returns the bit's initial index in bit-vector.  */
+  size_t get_index () const;
+
+  /* Returns type of the bit.  */
+  value_type get_type () const;
+
+  /* This will support deep copy of objects' values.  */
+  virtual value_bit *copy () const = 0;
+
+  /* Prints the bit.  Inherited classes must implement it.  */
+  virtual void print () = 0;
+  virtual ~value_bit () = default;
+};
+
+/* Represents value of a single bit of symbolic marked variables.  */
+
+class symbolic_bit : public value_bit {
+  tree m_origin = nullptr;
+
+ public:
+  symbolic_bit (size_t i, tree orig);
+  symbolic_bit (const symbolic_bit &sym_bit) : symbolic_bit (sym_bit.m_index,
+							     sym_bit.m_origin)
+  {};
+
+  /* Returns a copy of the bit.  */
+  value_bit *copy () const;
+
+  /* Prints the bit.  */
+  void print ();
+
+  /* Returns the origin of the bit, to whom it belongs.  */
+  tree get_origin ();
+};
+
+
+/* Represents value of a single bit.  */
+
+class bit : public value_bit {
+ private:
+  /* This is the value of a bit.  It must be either 1 or 0.  */
+  unsigned char m_val = 0;
+
+ public:
+  bit (unsigned char i);
+  bit (const bit &b) : bit (b.m_val)
+  {};
+
+  /* Returns the value of the bit.  */
+  unsigned char get_val () const;
+
+  /* Sets the value of the bit.  */
+  void set_val (unsigned char new_val);
+
+  /* Return a copy of the bit.  */
+  value_bit *copy () const;
+
+  /* Prints the bit.  */
+  void print ();
+};
+
+
+/* Bit-level base expression class.  In general expressions consist of
+   two operands.  Here we named them m_left and m_right.  */
+
+class bit_expression : public value_bit {
+ protected:
+  value_bit *m_left = nullptr;
+  value_bit *m_right = nullptr;
+
+  /* Copies the given expression to it by copying
+     the left and right operands.  */
+  void copy (const bit_expression *expr);
+
+  /* Depending on the expression, prints its sign.  */
+  virtual void print_expr_sign ();
+
+ public:
+
+  /* Returns left operand of the expression.  */
+  value_bit *get_left ();
+
+  /* Returns right operand of the expression.  */
+  value_bit *get_right ();
+
+  ~bit_expression ();
+
+  /* Sets left operand of the expression.  */
+  void set_left (value_bit *expr);
+
+  /* Sets right operand of the expression.  */
+  void set_right (value_bit *expr);
+
+  /* Returns a deep copy of the expression.  */
+  value_bit *copy () const = 0;
+
+  /* Prints the expression.  */
+  void print ();
+};
+
+
+/* Bit-level XOR expression.  XOR operation on two variables (when one of
+   them is symbolic) can be represented by XOR operations on
+   each of their bits.  */
+
+class bit_xor_expression : public bit_expression {
+ public:
+  bit_xor_expression (value_bit *left, value_bit *right);
+  bit_xor_expression (const bit_xor_expression &expr);
+
+  /* Returns a copy of the expression.  */
+  value_bit *copy () const;
+};
+
+
+/* Bit-level AND expression.  AND operation on two variables (when one of
+   them is symbolic) can be represented by AND operations on
+   each of their bits.  */
+
+class bit_and_expression : public bit_expression {
+ public:
+  bit_and_expression (value_bit *left, value_bit *right);
+  bit_and_expression (const bit_and_expression &expr);
+
+  /* Returns a copy of the expression.  */
+  value_bit *copy () const;
+};
+
+
+/* Bit-level OR expression.  OR operation on two variables (when one of
+   them is symbolic) can be represented by OR operations on
+   each of their bits.  */
+
+class bit_or_expression : public bit_expression {
+ public:
+  bit_or_expression (value_bit *left, value_bit *right);
+  bit_or_expression (const bit_or_expression &expr);
+
+  /* Returns a copy of the expression.  */
+  value_bit *copy () const;
+};
+
+
+/* SHIFT_RIGHT expression.  Result must be stored bit by bit.  */
+
+class shift_right_expression : public bit_expression {
+ public:
+  shift_right_expression (value_bit *left, value_bit *right);
+  shift_right_expression (const shift_right_expression &expr);
+
+  /* Returns a copy of the expression.  */
+  value_bit *copy () const;
+};
+
+
+/* SHIFT_LEFT expression.  Result must be stored bit by bit.  */
+
+class shift_left_expression : public bit_expression {
+ public:
+  shift_left_expression (value_bit *left, value_bit *right);
+  shift_left_expression (const shift_left_expression &expr);
+
+  /* Returns a copy of the expression.  */
+  value_bit *copy () const;
+};
+
+
+/* ADD expression.  Result must be stored bit by bit.  */
+
+class add_expression : public bit_expression {
+ public:
+  add_expression (value_bit *left, value_bit *right);
+  add_expression (const add_expression &expr);
+
+  /* Returns a copy of the expression.  */
+  value_bit *copy () const;
+};
+
+
+/* SUB expression.  Result must be stored bit by bit.  */
+
+class sub_expression : public bit_expression {
+ public:
+  sub_expression (value_bit *left, value_bit *right);
+  sub_expression (const sub_expression &expr);
+
+  /* Returns a copy of the expression.  */
+  value_bit *copy () const;
+};
+
+/* Bit-level negation expression.  */
+
+class bit_complement_expression : public bit_expression {
+ public:
+  bit_complement_expression (value_bit *right);
+  bit_complement_expression (const bit_complement_expression &expr);
+
+  /* Returns a copy of the expression.  */
+  value_bit *copy () const;
+
+  /* Prints the expression.  */
+  void print ();
+};
+
+#endif /* SYM_EXEC_EXPRESSION_H.  */
\ No newline at end of file
diff --git a/gcc/sym-exec/sym-exec-state.cc b/gcc/sym-exec/sym-exec-state.cc
new file mode 100644
index 00000000000..15df4d6a87e
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-state.cc
@@ -0,0 +1,2148 @@ 
+/* State will store states of variables for a function's single execution path.
+   It will be used for bit-level symbolic execution to determine values of bits
+   of function's return value and symbolic marked arguments.  */
+
+#include "sym-exec-state.h"
+
+size_t min (size_t a, size_t b, size_t c)
+{
+  size_t min = (a < b ? a : b);
+  return min < c ? min : c;
+}
+
+
+state::state (const state &s)
+{
+  for (auto iter = s.var_states.begin (); iter != s.var_states.end (); ++iter)
+    {
+      value val ((*iter).second.length (), (*iter).second.is_unsigned);
+      for (size_t i = 0; i < (*iter).second.length (); i++)
+	val.push ((*iter).second[i]->copy ());
+
+      var_states.put ((*iter).first, val);
+    }
+
+  for (auto iter = s.conditions.begin (); iter != s.conditions.end (); ++iter)
+    conditions.add (as_a<bit_expression *> ((*iter)->copy ()));
+}
+
+
+state::~state ()
+{
+  clear_conditions ();
+}
+
+
+/* Checks whether state for variable with specified name already
+   exists or not.  */
+
+bool
+state::is_declared (tree var)
+{
+  return var_states.get (var) != NULL;
+}
+
+
+/* Declares given variable if it has not been declared yet.  */
+
+void
+state::declare_if_needed (tree var, size_t size)
+{
+  if (TREE_CODE (var) != INTEGER_CST && !is_declared (var))
+    {
+      make_symbolic (var, size);
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	{
+	  fprintf (dump_file,
+		   "Declaring var ");
+	  print_generic_expr (dump_file, var, dump_flags);
+	  fprintf (dump_file,
+		   " with size %zd\n", size);
+	}
+    }
+}
+
+
+/* Get value of the given variable.  */
+
+value *
+state::get_value (tree var)
+{
+  return var_states.get (var);
+}
+
+
+/* Get the value of the tree, which is in the beginning of the var_states.  */
+
+value *
+state::get_first_value ()
+{
+  return &(*(var_states.begin ())).second;
+}
+
+
+/* Returns the list of conditions in the state.  */
+
+const hash_set<bit_expression *> &
+state::get_conditions ()
+{
+  return conditions;
+}
+
+
+/* Checks if sizes of arguments and destination are compatible.  */
+
+bool
+state::check_args_compatibility (tree arg1, tree arg2, tree dest)
+{
+  if (!(get_var_size (arg1) == get_var_size (dest)
+	|| TREE_CODE (arg1) == INTEGER_CST)
+      || !(get_var_size (arg2) == get_var_size (dest)
+	   || TREE_CODE (arg2) == INTEGER_CST))
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Sym-Exec: Incompatible destination"
+			    "and argument sizes.\n");
+
+      return false;
+    }
+
+  return true;
+}
+
+
+/* Creates value for given constant tree.  */
+
+value
+state::create_val_for_const (tree var, size_t size)
+{
+  unsigned HOST_WIDE_INT val = TYPE_UNSIGNED (TREE_TYPE (var))
+			       ? tree_to_uhwi (var) : tree_to_shwi (var);
+  value result (size, TYPE_UNSIGNED (TREE_TYPE (var)));
+
+  for (size_t i = 0; i < size; i++)
+    {
+      result.push (new bit (val & 1));
+      val >>= 1;
+    }
+
+  return result;
+}
+
+
+/* Adds the given variable to state.  */
+
+bool
+state::add_var_state (tree var, value *vstate)
+{
+  size_t size = vstate->length ();
+  value val (size, vstate->is_unsigned);
+  for (size_t i = 0; i < size; i++)
+    val.push ((*vstate)[i]->copy ());
+
+  return var_states.put (var, val);
+}
+
+
+/* Adds the given condition to the state.  */
+
+bool
+state::add_condition (bit_expression *cond)
+{
+  return conditions.add (as_a<bit_expression *> (cond->copy ()));
+}
+
+
+/* Bulk add the given conditions to the state.  */
+
+bool
+state::bulk_add_conditions (const hash_set<bit_expression *> &conds)
+{
+  bool status = true;
+  for (auto iter = conds.begin (); iter != conds.end (); ++iter)
+    status &= add_condition (*iter);
+
+  return status;
+}
+
+
+/* Remove all states from the states' vector.  */
+
+void
+state::remove_states (vec<state *> *states)
+{
+  while (!states->is_empty ())
+    {
+      delete states->last ();
+      states->pop ();
+    }
+}
+
+
+/* Remove all states from the states' vector and release the vector.  */
+
+void
+state::clear_states (vec<state *> *states)
+{
+  remove_states (states);
+  states->release ();
+}
+
+
+/* Removes all variables added to the state.  */
+
+void
+state::clear_var_states ()
+{
+  var_states.empty ();
+}
+
+
+/* Removes all conditions added to the state.  */
+
+void
+state::clear_conditions ()
+{
+  for (auto iter = conditions.begin (); iter != conditions.end (); ++iter)
+    delete (*iter);
+  conditions.empty ();
+}
+
+
+/* Performs AND operation for 2 symbolic_bit operands.  */
+
+value_bit *
+state::and_sym_bits (const value_bit *var1, const value_bit *var2)
+{
+  return new bit_and_expression (var1->copy (), var2->copy ());
+}
+
+
+/* Performs AND operation for a symbolic_bit and const_bit operands.  */
+
+value_bit *
+state::and_var_const (const value_bit *var1, const bit *const_bit)
+{
+  if (const_bit->get_val () == 1)
+    return var1->copy ();
+
+  return new bit (0);
+}
+
+
+/* Performs AND operation for 2 constant bit operands.  */
+
+bit *
+state::and_const_bits (const bit *const_bit1, const bit *const_bit2)
+{
+  if (const_bit1->get_val () == const_bit2->get_val ())
+    return new bit (*const_bit1);
+
+  return new bit (0);
+}
+
+
+/* Performs OR operation for 2 symbolic_bit operands.  */
+
+value_bit *
+state::or_sym_bits (const value_bit *var1, const value_bit *var2)
+{
+  return new bit_or_expression (var1->copy (), var2->copy ());
+}
+
+
+/* Performs OR operation for a symbolic_bit and a constant bit operands.  */
+
+value_bit *
+state::or_var_const (const value_bit *var1, const bit *const_bit)
+{
+  if (const_bit->get_val () == 0)
+    return var1->copy ();
+
+  return new bit (1);
+}
+
+
+/* Performs OR operation for 2 constant bit operands.  */
+
+bit *
+state::or_const_bits (const bit *const_bit1, const bit *const_bit2)
+{
+  if (const_bit1->get_val () == const_bit2->get_val ())
+    return new bit (*const_bit1);
+
+  return new bit (1);
+}
+
+
+/* Adds an empty state for the given variable.  */
+
+bool
+state::decl_var (tree var, unsigned size)
+{
+  if (is_declared (var))
+    return false;
+
+  value val (size, TYPE_UNSIGNED (TREE_TYPE (var)));
+  for (unsigned i = 0; i < size; i++)
+    val.push (nullptr);
+
+  return var_states.put (var, val);
+}
+
+
+/* Returns size of the given variable.  */
+
+unsigned
+state::get_var_size (tree var)
+{
+  value *content = var_states.get (var);
+  if (content == NULL)
+    return 0;
+
+  return content->allocated ();
+}
+
+
+/* Adds a variable with unknown value to state.  Such variables are
+   represented as sequence of symbolic bits.  */
+
+bool
+state::make_symbolic (tree var, unsigned size)
+{
+  if (is_declared (var))
+    return false;
+
+  value val (size, TYPE_UNSIGNED (TREE_TYPE (var)));
+  /* Initialize each bit of a variable with unknown value.  */
+  for (size_t i = 0; i < size; i++)
+    val.push (new symbolic_bit (i, var));
+
+  return var_states.put (var, val);
+}
+
+
+/* Performs AND operation on two bits.  */
+
+value_bit *
+state::and_two_bits (value_bit *arg1, value_bit *arg2)
+{
+  value_bit *result = nullptr;
+
+  if (is_a<bit *> (arg1) && is_a<bit *> (arg2))
+    result = and_const_bits (as_a<bit *> (arg1), as_a<bit *> (arg2));
+
+  else if (is_a<bit *> (arg1) && (is_a<symbolic_bit *> (arg2)
+				  || (is_a<bit_expression *> (arg2))))
+    result = and_var_const (arg2, as_a<bit *> (arg1));
+
+  else if ((is_a<symbolic_bit *> (arg1)
+	    || (is_a<bit_expression *> (arg1))) && is_a<bit *> (arg2))
+    result = and_var_const (arg1, as_a<bit *> (arg2));
+
+  else
+    result = and_sym_bits (arg1, arg2);
+
+  return result;
+}
+
+
+/* A wrapper for operations on two bits.
+   Operation and operands are passed as arguments.  */
+
+value_bit *
+state::operate_bits (bit_func bit_op, value_bit *bit1, value_bit *bit2,
+		     value_bit **)
+{
+  return (bit_op) (bit1, bit2);
+}
+
+
+/* A wrapper for operations on three bits.
+   Operation and operands are passed as arguments.  */
+
+value_bit *
+state::operate_bits (bit_func3 bit_op, value_bit *bit1, value_bit *bit2,
+		     value_bit **bit3)
+{
+  return (bit_op) (bit1, bit2, bit3);
+}
+
+
+/* Does preprocessing and postprocessing for expressions with tree operands.
+   Handles value creation for constant and their removement in the end.  */
+
+bool
+state::do_binary_operation (tree arg1, tree arg2, tree dest,
+			    binary_func bin_func)
+{
+  declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+  declare_if_needed (arg1, var_states.get (dest)->allocated ());
+  declare_if_needed (arg2, var_states.get (dest)->allocated ());
+
+  if (!check_args_compatibility (arg1, arg2, dest))
+    return false;
+
+  size_t dest_size = var_states.get (dest)->length ();
+
+  value *arg1_val = var_states.get (arg1);
+  value arg1_const_val (dest_size, false);
+  if (arg1_val == NULL && TREE_CODE (arg1) == INTEGER_CST)
+    {
+      arg1_const_val = create_val_for_const (arg1, dest_size);
+      arg1_val = &arg1_const_val;
+    }
+
+  value *arg2_val = var_states.get (arg2);
+  value arg2_const_val (dest_size, false);
+  if (arg2_val == NULL && TREE_CODE (arg2) == INTEGER_CST)
+    {
+      arg2_const_val = create_val_for_const (arg2, dest_size);
+      arg2_val = &arg2_const_val;
+    }
+
+  (this->*bin_func) (arg1_val, arg2_val, dest);
+  print_value (var_states.get (dest));
+  return true;
+}
+
+
+/* Performs AND operation on given values.  The result is stored in dest.  */
+
+void
+state::do_and (value *arg1, value *arg2, tree dest)
+{
+  /* Creating AND expressions for every bit pair of given arguments
+     and store them as a new state for given destination.  */
+
+  operate (arg1, arg2, nullptr, dest, &state::and_two_bits);
+}
+
+
+/* Performs OR operation on two bits.  */
+
+value_bit *
+state::or_two_bits (value_bit *arg1_bit, value_bit *arg2_bit)
+{
+  value_bit *result = nullptr;
+
+  if (is_a<bit *> (arg1_bit) && is_a<bit *> (arg2_bit))
+    result = or_const_bits (as_a<bit *> (arg1_bit), as_a<bit *> (arg2_bit));
+
+  else if (is_a<bit *> (arg1_bit) && (is_a<symbolic_bit *> (arg2_bit)
+				      || is_a<bit_expression *> (arg2_bit)))
+    result = or_var_const (arg2_bit, as_a<bit *> (arg1_bit));
+
+  else if ((is_a<symbolic_bit *> (arg1_bit)
+	    || is_a<bit_expression *> (arg1_bit))
+	   && is_a<bit *> (arg2_bit))
+    result = or_var_const (arg1_bit, as_a<bit *> (arg2_bit));
+
+  else
+    result = or_sym_bits (arg1_bit, arg2_bit);
+
+  return result;
+}
+
+
+/* Performs OR operation on given values.  The result is stored in dest.  */
+
+void
+state::do_or (value *arg1, value *arg2, tree dest)
+{
+  /* Creating OR expressions for every bit pair of given arguments
+     and store them as a new state for given destination.  */
+  operate (arg1, arg2, nullptr, dest, &state::or_two_bits);
+}
+
+
+/* Performs XOR operation on two bits.  */
+
+value_bit *
+state::xor_two_bits (value_bit *arg1_bit, value_bit *arg2_bit)
+{
+  value_bit *result = nullptr;
+
+  if (is_a<bit *> (arg1_bit) && is_a<bit *> (arg2_bit))
+    result = xor_const_bits (as_a<bit *> (arg1_bit), as_a<bit *> (arg2_bit));
+
+  else if (is_a<bit *> (arg1_bit) && (is_a<symbolic_bit *> (arg2_bit)
+				      || is_a<bit_expression *> (arg2_bit)))
+    result = xor_var_const (arg2_bit, as_a<bit *> (arg1_bit));
+
+  else if ((is_a<symbolic_bit *> (arg1_bit)
+	    || is_a<bit_expression *> (arg1_bit))
+	   && is_a<bit *> (arg2_bit))
+    result = xor_var_const (arg1_bit, as_a<bit *> (arg2_bit));
+
+  else
+    result = xor_sym_bits (arg1_bit, arg2_bit);
+
+  return result;
+}
+
+
+/* Performs XOR operation on given values.  The result is stored in dest.  */
+
+void
+state::do_xor (value *arg1, value *arg2, tree dest)
+{
+  operate (arg1, arg2, nullptr, dest, &state::xor_two_bits);
+}
+
+
+/* Shifts value right by size of shift_value.  */
+
+value *
+state::shift_right_by_const (value *var, size_t shift_value)
+{
+  value *shift_result = new value (var->length (), var->is_unsigned);
+  if (var->length () <= shift_value)
+    for (size_t i = 0; i < var->length (); i++)
+      shift_result->push (new bit (0));
+  else
+    {
+      size_t i = 0;
+      for (; i < var->length () - shift_value; ++i)
+	shift_result->push (((*var)[shift_value + i])->copy ());
+
+      for (; i < var->length (); ++i)
+	shift_result->push (var->is_unsigned ? new bit (0)
+					     : var->last ()->copy ());
+    }
+  return shift_result;
+}
+
+
+/* Checks if all bits of the given value have constant bit type.  */
+
+bool
+state::is_bit_vector (const value *var)
+{
+  if (var == nullptr || !var->exists ())
+    return false;
+
+  for (size_t i = 0; i < var->length (); i++)
+    if (!(is_a<bit *> ((*var)[i])))
+      return false;
+  return true;
+}
+
+
+/* Returns the number represented by the value.  */
+
+unsigned HOST_WIDE_INT
+state::make_number (const value *var)
+{
+  unsigned HOST_WIDE_INT
+  number = 0;
+  int value_size = var->length ();
+  for (int i = value_size - 1; i >= 0; i--)
+    {
+      if (is_a<bit *> ((*var)[i]))
+	number = (number << 1) | as_a<bit *> ((*var)[i])->get_val ();
+      else
+	return 0;
+    }
+  return number;
+}
+
+
+/* Shift_left operation.  Case: var2 is a symbolic value.  */
+
+value_bit *
+state::shift_left_sym_bits (value_bit *var1, value_bit *var2)
+{
+  return new shift_left_expression (var1->copy (), var2->copy ());
+}
+
+
+/* Performs shift left operation on given values.
+   The result is stored in dest.  */
+
+void
+state::do_shift_left (value *arg1, value *arg2, tree dest)
+{
+  if (is_bit_vector (arg2))
+    {
+      size_t shift_value = make_number (arg2);
+      value *result = shift_left_by_const (arg1, shift_value);
+      for (size_t i = 0; i < get_var_size (dest); i++)
+	{
+	  delete (*var_states.get (dest))[i];
+	  (*var_states.get (dest))[i] = (*result)[i]->copy ();
+	}
+      delete result;
+    }
+  else
+    operate (arg1, arg2, nullptr, dest, &state::shift_left_sym_bits);
+}
+
+
+/* Performs shift right operation on given values.
+   The result is stored in dest.  */
+
+void
+state::do_shift_right (value *arg1, value *arg2, tree dest)
+{
+  if (is_bit_vector (arg2))
+    {
+      size_t shift_value = make_number (arg2);
+      value *result = shift_right_by_const (arg1, shift_value);
+      for (size_t i = 0; i < get_var_size (dest); i++)
+	{
+	  delete (*var_states.get (dest))[i];
+	  (*var_states.get (dest))[i] = (*result)[i]->copy ();
+	}
+
+      delete result;
+    }
+  else
+    operate (arg1, arg2, nullptr, dest, &state::shift_right_sym_bits);
+}
+
+
+/* Adds two bits and carry value.
+   Resturn result and stores new carry bit in "carry".  */
+
+value_bit *
+state::full_adder (value_bit *var1, value_bit *var2, value_bit **carry)
+{
+  value_bit *new_carry = and_two_bits (var1, var2);
+  value_bit *sum = xor_two_bits (var1, var2);
+
+  value_bit *result = xor_two_bits (sum, *carry);
+  value_bit *sum_and_carry = and_two_bits (sum, *carry);
+
+  delete *carry;
+  delete sum;
+
+  *carry = or_two_bits (sum_and_carry, new_carry);
+
+  delete sum_and_carry;
+  delete new_carry;
+
+  return result;
+}
+
+
+/* Adds given values.  The result is stored in dest.  */
+
+void
+state::do_add (value *arg1, value *arg2, tree dest)
+{
+  value_bit *carry = new bit (0);
+  operate (arg1, arg2, &carry, dest, &state::full_adder);
+  delete carry;
+}
+
+
+/* Returns the additive inverse of the given number.  */
+
+value *
+state::additive_inverse (const value *number)
+{
+  value *result = new value (number->length (), number->is_unsigned);
+  value one (number->length (), number->is_unsigned);
+
+  size_t size = number->length ();
+  one.push (new bit (1));
+  result->push (complement_a_bit ((*number)[0]));
+
+  for (size_t i = 1; i < size; i++)
+    {
+      one.push (new bit (0));
+      result->push (complement_a_bit ((*number)[i]));
+    }
+
+  value_bit *carry = new bit (0);
+  for (size_t i = 0; i < size; ++i)
+    {
+      value_bit *cur_bit = (*result)[i];
+      (*result)[i] = full_adder (cur_bit, one[i], &carry);
+      delete cur_bit;
+    }
+
+  delete carry;
+  return result;
+}
+
+
+/* Subtracks second value from the first.  The result is stored in dest.  */
+
+void
+state::do_sub (value *arg1, value *arg2, tree dest)
+{
+  value *neg_arg2 = additive_inverse (arg2);
+  do_add (arg1, neg_arg2, dest);
+  delete neg_arg2;
+}
+
+
+/* Performs complement operation on a bit.  */
+
+value_bit *
+state::complement_a_bit (value_bit *var)
+{
+  value_bit *result = nullptr;
+  if (is_a<bit *> (var))
+    result = complement_const_bit (as_a<bit *> (var));
+  else
+    result = complement_sym_bit (var);
+
+  return result;
+}
+
+
+/* Negates given variable.  */
+
+bool
+state::do_complement (tree arg, tree dest)
+{
+  declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+  declare_if_needed (arg, var_states.get (dest)->allocated ());
+
+  /* Creating complement expressions for every bit the given argument
+     and store it as a new state for given destination.  */
+  size_t iter_count = min (get_var_size (dest), get_var_size (arg),
+			   get_var_size (arg));
+
+  size_t i = 0;
+  for (; i < iter_count; i++)
+    {
+      value_bit *result = complement_a_bit ((*var_states.get (arg))[i]);
+      delete (*var_states.get (dest))[i];
+      (*var_states.get (dest))[i] = result;
+    }
+
+  if (i >= get_var_size (dest))
+    {
+      print_value (var_states.get (dest));
+      return true;
+    }
+
+  for (; i < get_var_size (dest); i++)
+    {
+      delete (*var_states.get (dest))[i];
+      bit tmp (0);
+      (*var_states.get (dest))[i] = complement_a_bit (&tmp);
+    }
+
+  print_value (var_states.get (dest));
+  return true;
+}
+
+
+/* Does Assignment.  */
+
+bool
+state::do_assign (tree arg, tree dest)
+{
+  declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+  if (TREE_CODE (arg) != INTEGER_CST)
+    declare_if_needed (arg, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (arg))));
+  else
+    declare_if_needed (arg, var_states.get (dest)->allocated ());
+
+  value *dest_val = var_states.get (dest);
+
+  /* If the argument is already defined, then we must just copy its bits.  */
+  if (auto arg_val = var_states.get (arg))
+    {
+      for (size_t i = 0; i < dest_val->length (); i++)
+	{
+	  value_bit *new_val = nullptr;
+	  if (i < arg_val->length ())
+	    new_val = (*arg_val)[i]->copy ();
+	  else
+	    new_val = new bit (0);
+
+	  delete (*dest_val)[i];
+	  (*dest_val)[i] = new_val;
+	}
+    }
+    /* If the argument is a constant, we must save it as sequence of bits.  */
+  else if (TREE_CODE (arg) == INTEGER_CST)
+    {
+      value arg_val
+	= create_val_for_const (arg, dest_val->length ());
+      for (size_t i = 0; i < dest_val->length (); i++)
+	{
+	  delete (*dest_val)[i];
+	  (*dest_val)[i] = arg_val[i]->copy ();
+	}
+    }
+  else
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Sym-Exec: Unsupported assignment"
+			    " for given argument.\n");
+
+      return false;
+    }
+
+  print_value (var_states.get (dest));
+  return true;
+}
+
+
+/* Assigns pow 2 value.  */
+
+bool
+state::do_assign_pow2 (tree dest, unsigned pow)
+{
+  value *dest_val = var_states.get (dest);
+  unsigned dest_size = dest_val ? dest_val->allocated ()
+				: tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest)));
+  if (pow > dest_size)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Sym-Exec: pow %u of 2 won't fit in"
+			    " specified destination\n", pow);
+      return false;
+    }
+
+  if (!dest_val)
+    {
+      decl_var (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+      dest_val = var_states.get (dest);
+    }
+  else
+    dest_val->free_bits ();
+
+  for (unsigned i = 0; i < dest_val->length (); i++)
+    {
+      if (i == pow)
+	(*dest_val)[i] = new bit (1);
+      else
+	(*dest_val)[i] = new bit (0);
+    }
+
+  print_value (dest_val);
+  return true;
+}
+
+
+/* Performs NOT operation for constant bit.  */
+
+bit *
+state::complement_const_bit (const bit *const_bit)
+{
+  return new bit (1u ^ const_bit->get_val ());
+}
+
+
+/* Performs NOT operation for symbolic_bit.  */
+
+value_bit *
+state::complement_sym_bit (const value_bit *var)
+{
+  return new bit_complement_expression (var->copy ());
+}
+
+
+/* Performs XOR operation for 2 symbolic_bit operands.  */
+
+value_bit *
+state::xor_sym_bits (const value_bit *var1, const value_bit *var2)
+{
+  value_bit *var2_copy = var2->copy ();
+  bit_expression *node2_with_const_child = nullptr;
+  bit_expression *parent_of_node2_with_child = nullptr;
+  get_parent_with_const_child (var2_copy, node2_with_const_child,
+			       parent_of_node2_with_child);
+
+  if (node2_with_const_child != nullptr)
+    {
+      value_bit *var1_copy = var1->copy ();
+      bit_expression *node1_with_const_child = nullptr;
+      bit_expression *parent_of_node1_with_child = nullptr;
+      get_parent_with_const_child (var1_copy, node1_with_const_child,
+				   parent_of_node1_with_child);
+
+      /* If both subtrees have constant bit nodes,
+	 we can merge them together.  */
+      if (node1_with_const_child != nullptr)
+	{
+	  value_bit *var1_reformed = nullptr;
+	  value_bit *var2_reformed = nullptr;
+
+	  /* If var1's const bit is in its left subtree.  */
+	  value_bit *var1_left = node1_with_const_child->get_left ();
+	  if (var1_left != nullptr && is_a<bit *> (var1_left))
+	    {
+	      var1_reformed = node1_with_const_child->get_right ()->copy ();
+	      value_bit *var2_left = node2_with_const_child->get_left ();
+
+	      /* If var2's const bit is in its left subtree.  */
+	      if (var2_left != nullptr && is_a<bit *> (var2_left))
+		var2_reformed = node2_with_const_child->get_right ()->copy ();
+	      else /* Var2's const bit is in its right subtree.  */
+		var2_reformed = node2_with_const_child->get_left ()->copy ();
+	    }
+	  else /* Var1's const bit is in its right subtree.  */
+	    {
+	      var1_reformed = node1_with_const_child->get_left ()->copy ();
+	      value_bit *var2_left = node2_with_const_child->get_left ();
+
+	      /* If var2's const bit is in its left subtree.  */
+	      if (var2_left != nullptr && is_a<bit *> (var2_left))
+		var2_reformed = node2_with_const_child->get_right ()->copy ();
+	      else /* Var2's const bit is in its right subtree.  */
+		var2_reformed = node2_with_const_child->get_left ()->copy ();
+	    }
+
+	  if (parent_of_node1_with_child)
+	    {
+	      parent_of_node1_with_child->get_left ()
+	      == node1_with_const_child
+	      ? parent_of_node1_with_child->set_left (var1_reformed)
+	      : parent_of_node1_with_child->set_right (var1_reformed);
+	      delete node1_with_const_child;
+	    }
+	  else
+	    {
+	      delete var1_copy;
+	      var1_copy = var1_reformed;
+	    }
+
+	  if (parent_of_node2_with_child)
+	    {
+	      parent_of_node2_with_child->get_left ()
+	      == node2_with_const_child
+	      ? parent_of_node2_with_child->set_left (var2_reformed)
+	      : parent_of_node2_with_child->set_right (var2_reformed);
+	      delete node2_with_const_child;
+	    }
+	  else
+	    {
+	      delete var2_copy;
+	      var2_copy = var2_reformed;
+	    }
+
+	  return new bit_xor_expression (var1_copy, var2_copy);
+	}
+      delete var1_copy;
+    }
+
+  delete var2_copy;
+  return new bit_xor_expression (var1->copy (), var2->copy ());
+}
+
+
+/* Performs XOR operation for 2 constant bit operands.  */
+
+bit *
+state::xor_const_bits (const bit *const_bit1, const bit *const_bit2)
+{
+  return new bit (const_bit1->get_val () ^ const_bit2->get_val ());
+}
+
+
+/* Performs XOR operation for a symbolic_bit and const_bit operands.  */
+
+value_bit *
+state::xor_var_const (const value_bit *var, const bit *const_bit)
+{
+  if (const_bit->get_val () == 0)
+    return var->copy ();
+
+  value_bit *var_copy = var->copy ();
+  bit_expression *node_with_const_child = nullptr;
+  bit_expression *tmp = nullptr;
+  get_parent_with_const_child (var_copy, node_with_const_child, tmp);
+
+  if (node_with_const_child != nullptr)
+    {
+      value_bit *left = node_with_const_child->get_left ();
+      if (left != nullptr && is_a<bit *> (left))
+	{
+	  bit *new_left = xor_const_bits (as_a<bit *> (left), const_bit);
+	  delete left;
+	  node_with_const_child->set_left (new_left);
+	}
+      else
+	{
+	  value_bit *right = node_with_const_child->get_right ();
+	  bit *new_right = xor_const_bits (as_a<bit *> (right), const_bit);
+	  delete right;
+	  node_with_const_child->set_right (new_right);
+	}
+      return var_copy;
+    }
+
+  delete var_copy;
+  return new bit_xor_expression (var->copy (), const_bit->copy ());
+}
+
+
+/* Return node which has a const bit child.  Traversal is done based
+   on safe branching.  */
+
+void
+state::get_parent_with_const_child (value_bit *root, bit_expression *&parent,
+				    bit_expression *&parent_of_parent)
+{
+  parent_of_parent = nullptr;
+  parent = nullptr;
+
+  if (!is_a<bit_expression *> (root))
+    return;
+
+  bit_expression *expr_root = as_a<bit_expression *> (root);
+  hash_set < bit_expression * > nodes_to_consider;
+  nodes_to_consider.add (expr_root);
+
+  hash_map < bit_expression * , bit_expression * > node_to_parent;
+  node_to_parent.put (expr_root, nullptr);
+
+  /* Traversing expression tree:
+     considering only comutative expression nodes.  */
+  while (!nodes_to_consider.is_empty ())
+    {
+      bit_expression *cur_element = *nodes_to_consider.begin ();
+      nodes_to_consider.remove (cur_element);
+
+      value_bit *left = cur_element->get_left ();
+      value_bit *right = cur_element->get_right ();
+
+      if ((left != nullptr && is_a<bit *> (left))
+	  || (right != nullptr && is_a<bit *> (right)))
+	{
+	  parent = cur_element;
+	  parent_of_parent = *node_to_parent.get (cur_element);
+	}
+
+      if (left != nullptr && is_a<bit_xor_expression *> (left))
+	{
+	  nodes_to_consider.add (as_a<bit_expression *> (left));
+	  node_to_parent.put (as_a<bit_expression *> (left), cur_element);
+	}
+
+      if (right != nullptr && is_a<bit_xor_expression *> (right))
+	{
+	  nodes_to_consider.add (as_a<bit_expression *> (right));
+	  node_to_parent.put (as_a<bit_expression *> (right), cur_element);
+	}
+    }
+}
+
+
+/* Shifts number left by size of shift_value.  */
+
+value *
+state::shift_left_by_const (const value *number, size_t shift_value)
+{
+  value *shift_result = new value (number->length (), number->is_unsigned);
+  if (number->length () <= shift_value)
+    for (size_t i = 0; i < number->length (); i++)
+      shift_result->push (new bit (0));
+
+  else
+    {
+      size_t i = 0;
+      for (; i < shift_value; ++i)
+	shift_result->push (new bit (0));
+      for (size_t j = 0; i < number->length (); ++i, j++)
+	shift_result->push (((*number)[j])->copy ());
+    }
+  return shift_result;
+}
+
+
+/* Shift_right operation.  Case: var2 is a symbolic value.  */
+
+value_bit *
+state::shift_right_sym_bits (value_bit *var1, value_bit *var2)
+{
+  return new shift_right_expression (var1->copy (), var2->copy ());
+}
+
+
+/* Adds two values, stores the result in the first one.  */
+
+void
+state::add_numbers (value *var1, const value *var2)
+{
+  value_bit *carry = new bit (0);
+  for (unsigned i = 0; i < var1->length (); i++)
+    {
+      value_bit *temp = (*var1)[i];
+      (*var1)[i] = full_adder ((*var1)[i], (*var2)[i], &carry);
+      delete temp;
+    }
+  delete carry;
+}
+
+
+/* ANDs every bit of the vector with var_bit, stroes the result in var1.  */
+
+void
+state::and_number_bit (value *var1, value_bit *var_bit)
+{
+  for (unsigned i = 0; i < var1->length (); i++)
+    {
+      value_bit *tmp = (*var1)[i];
+      (*var1)[i] = and_two_bits ((*var1)[i], var_bit);
+      delete tmp;
+    }
+
+}
+
+
+void
+state::do_mul (value *arg1, value *arg2, tree dest)
+{
+  value *shifted = new value (*arg1);
+  value *dest_val = var_states.get (dest);
+
+  for (unsigned i = 0; i < dest_val->length (); i++)
+    {
+      delete (*dest_val)[i];
+      (*dest_val)[i] = new bit (0);
+    }
+
+  for (unsigned i = arg2->length (); i != 0; --i)
+    {
+      if (is_a<bit *> ((*arg2)[i - 1])
+	  && as_a<bit *> ((*arg2)[i - 1])->get_val () != 0)
+	add_numbers (dest_val, shifted);
+      else if (is_a<symbolic_bit *> ((*arg2)[i - 1]))
+	{
+	  and_number_bit (shifted, as_a<symbolic_bit *> ((*arg2)[i - 1]));
+	  add_numbers (dest_val, shifted);
+	}
+
+      value *temp = shifted;
+      shifted = shift_left_by_const (shifted, 1);
+      delete temp;
+    }
+  delete shifted;
+}
+
+
+/* Checks whether the given two constant values are equal.  */
+
+bool
+state::check_const_value_equality (value *arg1, value *arg2)
+{
+  for (size_t i = 0; i < arg1->length (); i++)
+    if (as_a<bit *> ((*arg1)[i])->get_val ()
+	!= as_a<bit *> ((*arg2)[i])->get_val ())
+      return false;
+  return true;
+}
+
+
+/* Adds EQUAL condition of given variables to state.  */
+
+bool
+state::add_equal_cond (tree arg1, tree arg2)
+{
+  return add_binary_cond (arg1, arg2, &state::add_equal_cond);
+}
+
+
+/* Adds equality condition for two values.  */
+
+void
+state::add_equal_cond (value *arg1, value *arg2)
+{
+
+  /* If both arguments are constants then we can evaluate it.  */
+  if (is_bit_vector (arg1) && is_bit_vector (arg2))
+    {
+      bool result = check_const_value_equality (arg1, arg2);
+      last_cond_status = result ? condition_status::CS_TRUE
+				: condition_status::CS_FALSE;
+      return;
+    }
+
+  /* When some of bits are constants and they differ by value,
+     then we can evalate it to be false.  */
+  for (size_t i = 0; i < arg1->length (); i++)
+    {
+      if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i])
+	  && as_a<bit *> ((*arg1)[i])->get_val ()
+	     != as_a<bit *> ((*arg2)[i])->get_val ())
+	{
+	  last_cond_status = condition_status::CS_FALSE;
+	  return;
+	}
+    }
+
+  for (size_t i = 0; i < arg1->length (); i++)
+    {
+      /* If there is a constant bit pair, then they are equal
+	 as we checked not equality above.  */
+      if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i]))
+	continue;
+
+      conditions.add (new bit_condition ((*arg1)[i]->copy (),
+					 (*arg2)[i]->copy (),
+					 EQ_EXPR));
+    }
+  last_cond_status = condition_status::CS_SYM;
+}
+
+
+/* Checks whether the given two constant values are not equal.  */
+
+bool
+state::check_const_value_are_not_equal (value *arg1, value *arg2)
+{
+  for (size_t i = 0; i < arg1->length (); i++)
+    if (as_a<bit *> ((*arg1)[i])->get_val ()
+	!= as_a<bit *> ((*arg2)[i])->get_val ())
+      return true;
+  return false;
+}
+
+
+/* Adds NOT EQUAL condition of given variables to state.  */
+
+bool
+state::add_not_equal_cond (tree arg1, tree arg2)
+{
+  return add_binary_cond (arg1, arg2, &state::add_not_equal_cond);
+}
+
+
+/* Adds not equal condition for two values.  */
+
+void
+state::add_not_equal_cond (value *arg1, value *arg2)
+{
+  if (is_bit_vector (arg1) && is_bit_vector (arg2))
+    {
+      bool result = check_const_value_are_not_equal (arg1, arg2);
+      last_cond_status = result ? condition_status::CS_TRUE
+				: condition_status::CS_FALSE;
+      return;
+    }
+
+  /* When some of bits are constants and they differ by value,
+     then we can evalate it to be true.  */
+  for (size_t i = 0; i < arg1->length (); i++)
+    {
+      if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i])
+	  && as_a<bit *> ((*arg1)[i])->get_val ()
+	     != as_a<bit *> ((*arg2)[i])->get_val ())
+	{
+	  last_cond_status = condition_status::CS_TRUE;
+	  return;
+	}
+    }
+
+  bit_expression *prev = nullptr;
+  for (size_t i = 0; i < arg1->length (); i++)
+    {
+      /* If there is a constant bit pair, then they are equal
+	 as we checked not equality above.  */
+      if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i]))
+	continue;
+
+      bit_condition *new_cond = new bit_condition ((*arg1)[i]->copy (),
+						   (*arg2)[i]->copy (),
+						   NE_EXPR);
+      if (prev)
+	prev = new bit_or_expression (prev, new_cond);
+      else
+	prev = new_cond;
+    }
+
+  last_cond_status = condition_status::CS_SYM;
+  conditions.add (prev);
+}
+
+
+/* Checks whether the first given constant value
+   is greater than the second one.  */
+
+bool
+state::check_const_value_is_greater_than (value *arg1, value *arg2)
+{
+  for (int i = arg1->length () - 1; i >= 0; i--)
+    {
+      if (as_a<bit *> ((*arg1)[i])->get_val ()
+	  > as_a<bit *> ((*arg2)[i])->get_val ())
+	return true;
+      else if (as_a<bit *> ((*arg1)[i])->get_val ()
+	       < as_a<bit *> ((*arg2)[i])->get_val ())
+	return false;
+    }
+  return false;
+}
+
+
+/* Adds GREATER THAN condition of given variables to state.  */
+
+bool
+state::add_greater_than_cond (tree arg1, tree arg2)
+{
+  return add_binary_cond (arg1, arg2, &state::add_greater_than_cond);
+}
+
+
+/* Adds greater than condition for two values.  */
+
+void
+state::add_greater_than_cond (value *arg1, value *arg2)
+{
+  if (is_bit_vector (arg1) && is_bit_vector (arg2))
+    {
+      bool result = check_const_value_is_greater_than (arg1, arg2);
+      last_cond_status = result ? condition_status::CS_TRUE
+				: condition_status::CS_FALSE;
+      return;
+    }
+
+  if (is_bit_vector (arg2) && is_a<bit *> (arg1->last ())
+      && make_number (arg2) == 0 && !arg1->is_unsigned)
+    {
+      if (as_a<bit *> (arg1->last ())->get_val () == 1)
+	last_cond_status = condition_status::CS_FALSE;
+      else
+	{
+	  for (size_t i = 0; i < arg1->length (); i++)
+	    if (is_a<bit *> ((*arg1)[i])
+		&& as_a<bit *> ((*arg1)[i])->get_val ())
+	      {
+		last_cond_status = condition_status::CS_TRUE;
+		return;
+	      }
+	}
+    }
+
+  bit_expression *gt_cond = construct_great_than_cond (arg1, arg2);
+  if (gt_cond)
+    {
+      /* Otherwise its status is already set.  */
+      last_cond_status = condition_status::CS_SYM;
+      conditions.add (gt_cond);
+    }
+}
+
+
+/* Constructs expression trees of greater than condition for given values.  */
+
+bit_expression *
+state::construct_great_than_cond (value *arg1, value *arg2)
+{
+  bit_expression *prev = nullptr;
+  int i = arg1->length () - 1;
+  for (; i >= 0; i--)
+    {
+      if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i]))
+	{
+	  if (as_a<bit *> ((*arg1)[i])->get_val ()
+	      > as_a<bit *> ((*arg2)[i])->get_val ())
+	    {
+	      if (!prev)
+		last_cond_status = condition_status::CS_TRUE;
+	      return prev;
+	    }
+	  else if (as_a<bit *> ((*arg1)[i])->get_val ()
+		   < as_a<bit *> ((*arg2)[i])->get_val ())
+	    {
+	      if (prev)
+		{
+		  bit_expression *ret_val
+		    = as_a<bit_expression *> (prev->get_left ()->copy ());
+		  delete prev;
+		  return ret_val;
+		}
+	      else
+		{
+		  last_cond_status = condition_status::CS_FALSE;
+		  return nullptr;
+		}
+	    }
+	}
+      else
+	{
+	  bit_condition *gt_cond
+	    = new bit_condition ((*arg1)[i]->copy (), (*arg2)[i]->copy (),
+				 GT_EXPR);
+	  bit_expression *expr = nullptr;
+	  if (i)
+	    {
+	      bit_condition *eq_cond
+		= new bit_condition ((*arg1)[i]->copy (), (*arg2)[i]->copy (),
+				     EQ_EXPR);
+	      expr = new bit_or_expression (gt_cond, eq_cond);
+	    }
+	  else
+	    expr = gt_cond;
+
+	  if (prev)
+	    prev = new bit_and_expression (expr, prev);
+	  else
+	    prev = expr;
+	}
+    }
+
+  return prev;
+}
+
+
+/* Checks whether the first given constant value
+   is less than the second one.  */
+
+bool
+state::check_const_value_is_less_than (value *arg1, value *arg2)
+{
+  for (int i = arg1->length () - 1; i >= 0; i--)
+    {
+      if (as_a<bit *> ((*arg1)[i])->get_val ()
+	  < as_a<bit *> ((*arg2)[i])->get_val ())
+	return true;
+      else if (as_a<bit *> ((*arg1)[i])->get_val ()
+	       > as_a<bit *> ((*arg2)[i])->get_val ())
+	return false;
+    }
+  return false;
+}
+
+
+/* Adds LESS THAN condition of given variables to state.  */
+
+bool
+state::add_less_than_cond (tree arg1, tree arg2)
+{
+  return add_binary_cond (arg1, arg2, &state::add_less_than_cond);
+}
+
+
+/* Adds less than condition for two values.  */
+
+void
+state::add_less_than_cond (value *arg1, value *arg2)
+{
+  if (is_bit_vector (arg1) && is_bit_vector (arg2)
+      && (make_number (arg2) != 0 || arg1->is_unsigned))
+    {
+      bool result = check_const_value_is_less_than (arg1, arg2);
+      last_cond_status = result ? condition_status::CS_TRUE
+				: condition_status::CS_FALSE;
+      return;
+    }
+
+  last_cond_status = condition_status::CS_SYM;
+  if (is_bit_vector (arg2) && make_number (arg2) == 0 && !arg1->is_unsigned)
+    {
+      if (is_a<bit *> (arg1->last ()))
+	{
+	  if (as_a<bit *> (arg1->last ())->get_val () == 1)
+	    last_cond_status = condition_status::CS_TRUE;
+	  else
+	    last_cond_status = condition_status::CS_FALSE;
+	}
+      else
+	conditions.add (new bit_condition (arg1->last ()->copy (), new bit (1),
+					   EQ_EXPR));
+
+      return;
+    }
+
+  bit_expression *lt_cond = construct_less_than_cond (arg1, arg2);
+  if (lt_cond)
+    /* Otherwise its status is already set.  */
+    conditions.add (lt_cond);
+}
+
+
+/* Constructs expression trees of less than condition for given values.  */
+
+bit_expression *
+state::construct_less_than_cond (value *arg1, value *arg2)
+{
+  bit_expression *prev = nullptr;
+  int i = arg1->length () - 1;
+  for (; i >= 0; i--)
+    {
+      if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i]))
+	{
+	  if (as_a<bit *> ((*arg1)[i])->get_val ()
+	      < as_a<bit *> ((*arg2)[i])->get_val ())
+	    {
+	      if (!prev)
+		last_cond_status = condition_status::CS_TRUE;
+	      return prev;
+	    }
+	  else if (as_a<bit *> ((*arg1)[i])->get_val ()
+		   > as_a<bit *> ((*arg2)[i])->get_val ())
+	    {
+	      if (prev)
+		{
+		  bit_expression *ret_val
+		    = as_a<bit_expression *> (prev->get_left ()->copy ());
+		  delete prev;
+		  return ret_val;
+		}
+	      else
+		{
+		  last_cond_status = condition_status::CS_FALSE;
+		  return nullptr;
+		}
+	    }
+	}
+      else
+	{
+	  bit_condition *lt_cond
+	    = new bit_condition ((*arg1)[i]->copy (), (*arg2)[i]->copy (),
+				 LT_EXPR);
+	  bit_expression *expr = nullptr;
+	  if (i)
+	    {
+	      bit_condition *eq_cond
+		= new bit_condition ((*arg1)[i]->copy (), (*arg2)[i]->copy (),
+				     EQ_EXPR);
+	      expr = new bit_or_expression (lt_cond, eq_cond);
+	    }
+	  else
+	    expr = lt_cond;
+
+	  if (prev)
+	    prev = new bit_and_expression (expr, prev);
+	  else
+	    prev = expr;
+	}
+    }
+
+  return prev;
+}
+
+
+/* Adds GREATER OR EQUAL condition of given variables to state.  */
+
+bool
+state::add_greater_or_equal_cond (tree arg1, tree arg2)
+{
+  return add_binary_cond (arg1, arg2, &state::add_greater_or_equal_cond);
+}
+
+
+/* Adds greater or equal condition for two values.  */
+
+void
+state::add_greater_or_equal_cond (value *arg1, value *arg2)
+{
+  if (is_bit_vector (arg1) && is_bit_vector (arg2)
+      && (make_number (arg2) != 0 || arg1->is_unsigned))
+    {
+      bool is_greater_than = check_const_value_is_greater_than (arg1,
+								arg2);
+      bool is_equal = check_const_value_equality (arg1, arg2);
+      last_cond_status = (is_greater_than | is_equal)
+			 ? condition_status::CS_TRUE
+			 : condition_status::CS_FALSE;
+      return;
+    }
+
+  last_cond_status = condition_status::CS_SYM;
+  if (is_bit_vector (arg2) && make_number (arg2) == 0 && !arg1->is_unsigned)
+    {
+      if (is_a<bit *> (arg1->last ()))
+	{
+	  if (as_a<bit *> (arg1->last ())->get_val () == 1)
+	    last_cond_status = condition_status::CS_FALSE;
+	  else
+	    last_cond_status = condition_status::CS_TRUE;
+	}
+      else
+	conditions.add (new bit_condition (arg1->last ()->copy (), new bit (0),
+					   EQ_EXPR));
+
+      return;
+    }
+
+  bit_expression *eq_cond = construct_equal_cond (arg1, arg2);
+  if (!eq_cond)
+    return;
+
+  bit_expression *gt_cond = construct_great_than_cond (arg1, arg2);
+  if (gt_cond)
+    /* Otherwise its status is already set.  */
+    conditions.add (new bit_or_expression (eq_cond, gt_cond));
+}
+
+
+/* Adds LESS OR EQUAL condition of given variables to state.  */
+
+bool
+state::add_less_or_equal_cond (tree arg1, tree arg2)
+{
+  return add_binary_cond (arg1, arg2, &state::add_less_or_equal_cond);
+}
+
+
+/* Adds less or equal condition for two values.  */
+
+void
+state::add_less_or_equal_cond (value *arg1, value *arg2)
+{
+  if (is_bit_vector (arg1) && is_bit_vector (arg2))
+    {
+      bool is_less_than = check_const_value_is_less_than (arg1, arg2);
+      bool is_equal = check_const_value_equality (arg1, arg2);
+      last_cond_status = (is_less_than | is_equal)
+			 ? condition_status::CS_TRUE
+			 : condition_status::CS_FALSE;
+      return;
+    }
+
+  last_cond_status = condition_status::CS_SYM;
+  bit_expression *eq_cond = construct_equal_cond (arg1, arg2);
+  if (!eq_cond)
+    return;
+
+  bit_expression *lt_cond = construct_less_than_cond (arg1, arg2);
+  if (lt_cond)
+    /* Otherwise its status is already set.  */
+    conditions.add (new bit_or_expression (eq_cond, lt_cond));
+}
+
+
+/* Adds a bool condition to state.  */
+
+bool
+state::add_bool_cond (tree arg)
+{
+  if (!is_declared (arg))
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Sym-Exec: Argument must be declared "
+			    "for bool condition.\n");
+
+      return false;
+    }
+
+  value *arg_bits = var_states.get (arg);
+  for (size_t i = 0; i < arg_bits->length (); i++)
+    if (is_a<bit *> ((*arg_bits)[i])
+	&& as_a<bit *> ((*arg_bits)[i])->get_val () != 0)
+      {
+	last_cond_status = condition_status::CS_TRUE;
+	print_conditions ();
+	return true;
+      }
+
+  if (is_bit_vector (arg_bits))
+    {
+      last_cond_status = condition_status::CS_FALSE;
+      print_conditions ();
+      return true;
+    }
+
+  bit_expression *prev = nullptr;
+  for (size_t i = 0; i < arg_bits->length (); i++)
+    {
+      if (is_a<bit *> ((*arg_bits)[i]))
+	continue;
+
+      bit_condition *not_eq_cond
+	= new bit_condition ((*arg_bits)[i], new bit (0), NE_EXPR);
+      if (prev)
+	prev = new bit_or_expression (not_eq_cond, prev);
+      else
+	prev = not_eq_cond;
+    }
+
+  last_cond_status = condition_status::CS_SYM;
+  conditions.add (prev);
+  print_conditions ();
+  return true;
+}
+
+
+/* Does preprocessing and postprocessing for condition adding.
+   Handles value creation for constants and their removement in the end.  */
+
+bool
+state::add_binary_cond (tree arg1, tree arg2, binary_cond_func cond_func)
+{
+  bool arg1_is_declared = is_declared (arg1);
+  bool arg2_is_declared = is_declared (arg2);
+
+  if (!arg1_is_declared && !arg2_is_declared)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Sym-Exec: At least one of arguments must be"
+			    " declared for adding the condition.\n");
+
+      return false;
+    }
+
+  if (arg1_is_declared)
+    declare_if_needed (arg2, var_states.get (arg1)->length ());
+
+  if (arg2_is_declared)
+    declare_if_needed (arg1, var_states.get (arg2)->length ());
+
+  value *arg1_val = var_states.get (arg1);
+  value arg1_const_val (MAX_VALUE_SIZE, false);
+
+  if (arg1_val == NULL && TREE_CODE (arg1) == INTEGER_CST)
+    {
+      arg1_const_val = create_val_for_const (arg1,
+					     var_states.get (arg2)->length ());
+      arg1_val = &arg1_const_val;
+    }
+
+  value *arg2_val = var_states.get (arg2);
+  value arg2_const_val (MAX_VALUE_SIZE, false);
+  if (arg2_val == NULL && TREE_CODE (arg2) == INTEGER_CST)
+    {
+      arg2_const_val = create_val_for_const (arg2,
+					     var_states.get (arg1)->length ());
+      arg2_val = &arg2_const_val;
+    }
+
+  (this->*cond_func) (arg1_val, arg2_val);
+  print_conditions ();
+  return true;
+}
+
+
+/* Constructs expression trees of equal condition for given values.  */
+
+bit_expression *
+state::construct_equal_cond (value *arg1, value *arg2)
+{
+  /* If both arguments are constants then we can evaluate it.  */
+  if (is_bit_vector (arg1) && is_bit_vector (arg2))
+    {
+      bool result = check_const_value_equality (arg1, arg2);
+      last_cond_status = result ? condition_status::CS_TRUE
+				: condition_status::CS_FALSE;
+      return nullptr;
+    }
+
+  /* When some bits are constants, and they differ by value,
+     then we can evaluate it to be false.  */
+  for (size_t i = 0; i < arg1->length (); i++)
+    {
+      if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i])
+	  && as_a<bit *> ((*arg1)[i])->get_val ()
+	     != as_a<bit *> ((*arg2)[i])->get_val ())
+	{
+	  last_cond_status = condition_status::CS_FALSE;
+	  return nullptr;
+	}
+    }
+
+  bit_expression *prev = nullptr;
+  for (size_t i = 0; i < arg1->length (); i++)
+    {
+      bit_condition *eq_expr = new bit_condition ((*arg1)[i]->copy (),
+						  (*arg2)[i]->copy (), EQ_EXPR);
+      if (prev)
+	prev = new bit_and_expression (eq_expr, prev);
+      else
+	prev = eq_expr;
+    }
+
+  return prev;
+}
+
+
+value::value (unsigned size, bool is_unsigned) : is_unsigned (is_unsigned)
+{
+  number.create (size);
+}
+
+
+value::value (const value &other) : is_unsigned (other.is_unsigned)
+{
+  number.create (other.length ());
+  for (size_t i = 0; i < other.length (); ++i)
+    {
+      value_bit *temp = other[i] ? other[i]->copy () : other[i];
+      number.quick_push (temp);
+    }
+}
+
+
+/* Returns pushed bits count.  */
+
+unsigned
+value::length () const
+{
+  return number.length ();
+}
+
+
+/* Wrapper of vec<..>::operator[] for the bit-vector.  */
+
+value_bit *&
+value::operator[] (unsigned i)
+{
+  return number[i];
+}
+
+
+/* Assignment operator.  If the specified value's size is smaller,
+   then 0 constant bit will be assigned to the remaining upper bits.  */
+
+value &
+value::operator= (const value &other)
+{
+  unsigned smallest = number.allocated () < other.length ()
+		      ? number.allocated () : other.length ();
+
+  for (size_t i = 0; i < smallest; i++)
+    if (i < number.length ())
+      {
+	delete number[i];
+	number[i] = other[i]->copy ();
+      }
+    else
+      number.quick_push (other[i]->copy ());
+
+  for (size_t i = smallest; i < number.allocated (); i++)
+    if (i < number.length ())
+      {
+	delete number[i];
+	number[i] = other.is_unsigned ? new bit (0)
+				      : other[other.length () - 1]->copy ();
+      }
+    else
+      number.quick_push (other.is_unsigned
+			 ? new bit (0) : other[other.length () - 1]->copy ());
+
+  return (*this);
+}
+
+
+/* Wrapper of vec<..>::operator[] const for the bit-vector.  */
+
+value_bit *
+value::operator[] (unsigned i) const
+{
+  return number[i];
+}
+
+
+/* Wrapper of vec<..>.exists for the bit-vector.  */
+
+bool
+value::exists () const
+{
+  return number.exists ();
+}
+
+
+/* Returns the size in bits.  */
+
+unsigned
+value::allocated () const
+{
+  return number.allocated ();
+}
+
+
+/* Returns a reference the last bit.  */
+
+value_bit *&
+value::last ()
+{
+  return number.last ();
+}
+
+
+/* Make a copy of given bits.  */
+
+vec<value_bit *> *
+state::make_copy (vec<value_bit *> *bits)
+{
+  vec < value_bit * > *copied_bits = new vec<value_bit *> ();
+  copied_bits->create (bits->length ());
+  for (size_t i = 0; i < bits->length (); i++)
+    copied_bits->quick_push ((*bits)[i]->copy ());
+
+  return copied_bits;
+}
+
+
+/* Returns status of last added condition.  */
+
+condition_status
+state::get_last_cond_status ()
+{
+  return last_cond_status;
+}
+
+
+/* Prints the given value.  */
+
+void
+state::print_value (value *var)
+{
+  if (!dump_file || !(dump_flags & TDF_DETAILS))
+    return;
+
+  fprintf (dump_file, "{");
+  for (int i = var->length () - 1; i >= 0; i--)
+    {
+      (*var)[i]->print ();
+
+      if (i)
+	fprintf (dump_file, ", ");
+    }
+  fprintf (dump_file, "}\n");
+}
+
+
+/* Get the last 1 bit index.  */
+
+size_t
+last_set_bit (const value &polynomial)
+{
+  for (size_t i = 0; i < polynomial.length (); ++i)
+    {
+      if (as_a<bit *> (polynomial[polynomial.length () - i - 1])->get_val ())
+	return polynomial.length () - i - 1;
+    }
+  return 0;
+}
+
+
+/* Prints added conditions.  */
+
+void
+state::print_conditions ()
+{
+  if (!dump_file || !(dump_flags & TDF_DETAILS))
+    return;
+
+  fprintf (dump_file, "Conditions {");
+  auto iter = conditions.begin ();
+  while (true)
+    {
+      if (iter != conditions.end ())
+	{
+	  (*iter)->print ();
+	  ++iter;
+	}
+
+      if (iter != conditions.end ())
+	fprintf (dump_file, ", ");
+      else
+	break;
+    }
+  fprintf (dump_file, "}\n");
+}
+
+
+/* Pushes the given bit to the end of the bit vector.  */
+
+value_bit **
+value::push (value_bit *elem)
+{
+  return number.quick_push (elem);
+}
+
+
+value::~value ()
+{
+  free_bits ();
+  number.release ();
+}
+
+
+/* Removes given sequence of bits.  */
+
+void
+value::free_bits ()
+{
+  if (!number.exists ())
+    return;
+
+  for (size_t i = 0; i < number.length (); i++)
+    {
+      delete number[i];
+      number[i] = nullptr;
+    }
+}
+
+
+/* For the given value_bit, iterates over its expression tree, complements
+   those bit which came from the given origin.  */
+
+value_bit *
+state::complement_bits_with_origin (value_bit *root, tree origin)
+{
+  /* Be careful.  This function doesn't make a full copy of the bit.  */
+  if (!is_a<bit_expression *> (root))
+    {
+      if (is_a<symbolic_bit *> (root)
+	  && as_a<symbolic_bit *> (root)->get_origin () == origin)
+	root = new bit_complement_expression (root);
+
+      return root;
+    }
+
+  bit_expression *expr_root = as_a<bit_expression *> (root);
+  hash_set <value_bit *> nodes_to_consider;
+  nodes_to_consider.add (expr_root);
+  hash_map <value_bit *, value_bit *> node_to_parent;
+  node_to_parent.put (expr_root, nullptr);
+
+  /* Traversing expression tree.  */
+  while (!nodes_to_consider.is_empty ())
+    {
+      value_bit *cur_element = *nodes_to_consider.begin ();
+      nodes_to_consider.remove (cur_element);
+
+      if (is_a<symbolic_bit *> (cur_element))
+	{
+	  if (as_a<symbolic_bit *> (cur_element)->get_origin () != origin)
+	    continue;
+
+	  bit_expression *parent
+	  = as_a<bit_expression *> (*node_to_parent.get (cur_element));
+	  if (is_a<bit_complement_expression *> (parent))
+	    {
+	      value_bit *parent_of_parent = *node_to_parent.get (parent);
+	      if (parent_of_parent)
+		{
+		  bit_expression *parent_of_parent_expr
+		  = as_a<bit_expression *> (parent_of_parent);
+		  parent->set_right (nullptr);
+		  delete parent;
+		  parent_of_parent_expr->get_left () == parent
+		    ? parent_of_parent_expr->set_left (cur_element)
+		    : parent_of_parent_expr->set_right (cur_element);
+		}
+	      else
+		{
+		  /* Parent is our root.  */
+		  as_a<bit_expression *> (root)->set_right (nullptr);
+		  delete root;
+		  root = cur_element;
+		}
+	    }
+	  else
+	    {
+	      value_bit* new_bit = new bit_complement_expression (cur_element);
+	      parent->get_left () == cur_element ? parent->set_left (new_bit)
+						 : parent->set_right (new_bit);
+	    }
+	  continue;
+	}
+
+      bit_expression* cur_elem_expr = as_a<bit_expression *> (cur_element);
+      value_bit *left = cur_elem_expr->get_left ();
+      value_bit *right = cur_elem_expr->get_right ();
+      if (left != nullptr && !is_a<bit *> (left))
+	{
+	  nodes_to_consider.add (left);
+	  node_to_parent.put (left, cur_element);
+	}
+
+      if (right != nullptr && !is_a<bit *> (right))
+	{
+	  nodes_to_consider.add (right);
+	  node_to_parent.put (right, cur_element);
+	}
+    }
+
+  return root;
+}
+
+
+/* Iterates over every bit of the given value and complements their
+   expression trees' those bits, that came from the given origin.  */
+
+void
+state::complement_val_bits_with_origin (value *val, tree origin)
+{
+  for (size_t i = 0; i < val->length (); i++)
+    {
+      (*val)[i] = complement_bits_with_origin ((*val)[i], origin);
+    }
+}
+
+
+/* Complements all bits of all values that came from the given origin.  */
+
+void
+state::complement_all_vars_bits_with_origin (tree origin)
+{
+  for (auto iter = var_states.begin (); iter != var_states.end (); ++iter)
+    {
+      complement_val_bits_with_origin (&(*iter).second, origin);
+    }
+}
+
+
+/* Complements all bits with the given origin of all added conditions.  */
+
+void
+state::complement_conditions_with_origin (tree origin)
+{
+  hash_set<bit_expression *> updated_conditions;
+  for (auto iter = conditions.begin (); iter != conditions.end (); ++iter)
+    updated_conditions.add (as_a<bit_expression *> (
+      complement_bits_with_origin (*iter, origin)));
+
+  conditions.empty ();
+  for (auto iter = updated_conditions.begin ();
+       iter != updated_conditions.end (); ++iter)
+    conditions.add (*iter);
+}
+
+
+/* Complements all bits with the given origin of all values
+   and added conditions.  */
+
+void
+state::complement_state_with_origin (tree origin)
+{
+  complement_all_vars_bits_with_origin (origin);
+  complement_conditions_with_origin (origin);
+}
+
+
+/* Performs the specified operation on passed variables.  */
+
+bool
+state::do_operation (tree_code op_code, tree arg1, tree arg2, tree dest)
+{
+  switch (op_code)
+    {
+      case BIT_NOT_EXPR:
+	return do_complement (arg1, dest);
+      case NOP_EXPR:
+      case SSA_NAME:
+      case VAR_DECL:
+      case INTEGER_CST:
+	return do_assign (arg1, dest);
+      case LSHIFT_EXPR:
+	return do_binary_operation (arg1, arg2, dest, &state::do_shift_left);
+      case RSHIFT_EXPR:
+	return do_binary_operation (arg1, arg2, dest, &state::do_shift_right);
+      case BIT_AND_EXPR:
+	return do_binary_operation (arg1, arg2, dest, &state::do_and);
+      case BIT_IOR_EXPR:
+	return do_binary_operation (arg1, arg2, dest, &state::do_or);
+      case BIT_XOR_EXPR:
+	return do_binary_operation (arg1, arg2, dest, &state::do_xor);
+      case PLUS_EXPR:
+	return do_binary_operation (arg1, arg2, dest, &state::do_add);
+      case MINUS_EXPR:
+	return do_binary_operation (arg1, arg2, dest, &state::do_sub);
+      case MULT_EXPR:
+	return do_binary_operation (arg1, arg2, dest, &state::do_mul);
+      default:
+	{
+	  if (dump_file)
+	    fprintf (dump_file,
+		     "Warning, encountered unsupported operation "
+		     "with %s code while executing assign statement!\n",
+		     get_tree_code_name (op_code));
+	  return false;
+	}
+    }
+}
diff --git a/gcc/sym-exec/sym-exec-state.h b/gcc/sym-exec/sym-exec-state.h
new file mode 100644
index 00000000000..5a3f9ebbbff
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-state.h
@@ -0,0 +1,436 @@ 
+/* State will store states of variables for a function's single execution path.
+   It will be used for bit-level symbolic execution to determine values of bits
+   of function's return value and symbolic marked arguments.  */
+
+
+#ifndef SYM_EXEC_STATE_H
+#define SYM_EXEC_STATE_H
+
+#define MAX_VALUE_SIZE 64
+
+#include "sym-exec-expr-is-a-helper.h"
+
+struct value {
+ private:
+  vec<value_bit *> number;
+
+ public:
+  const bool is_unsigned;
+
+  value (unsigned size, bool is_unsigned);
+  value (const value &other);
+
+  /* Pushes the given bit to the end of the bit-vector.  */
+  value_bit **push (value_bit *elem);
+
+  /* Returns pushed bits count.  */
+  unsigned length () const;
+
+  /* Returns a reference the last bit.  */
+  value_bit *&last ();
+
+  /* Returns the size in bits.  */
+  unsigned allocated () const;
+
+  /* Wrapper of vec<..>.exists for the bit-vector.  */
+  bool exists () const;
+
+  /* Wrapper of vec<..>::operator[] for the bit-vector.  */
+  value_bit *&operator[] (unsigned i);
+
+  /* Assignment operator.  If the specified value's size is smaller,
+     then 0 constant bit will be assigned to the remaining upper bits.  */
+  value &operator= (const value &other);
+
+  /* Wrapper of vec<..>::operator[] const for the bit-vector.  */
+  value_bit *operator[] (unsigned i) const;
+  ~value ();
+
+  /* Removes given sequence of bits.  */
+  void free_bits ();
+};
+
+/* Stores states of variables' values on bit-level.  */
+
+class state {
+  typedef void (state::*binary_func) (value *arg1, value *arg2, tree dest);
+  typedef value_bit *(*bit_func) (value_bit *bit1, value_bit *bit2);
+  typedef value_bit *(*bit_func3) (value_bit *var1, value_bit *var2,
+				   value_bit **var3);
+  typedef void (state::*binary_cond_func) (value *arg1, value *arg2);
+
+ private:
+
+  /* Here is stored values by bits of each variable.  */
+  hash_map<tree, value> var_states;
+
+  /* Here is stored conditions of symbolic bits.  */
+  hash_set<bit_expression *> conditions;
+
+  /* The result of last added condition.  */
+  condition_status last_cond_status = condition_status::CS_NO_COND;
+
+  /* Creates value for given constant tree.  */
+  static value create_val_for_const (tree var, size_t size);
+
+  /* Checks if sizes of arguments and destination are compatible.  */
+  bool check_args_compatibility (tree arg1, tree arg2, tree dest);
+
+  /* Adds equality condition for two values.  */
+  void add_equal_cond (value *arg1, value *arg2);
+
+  /* Adds not equal condition for two values.  */
+  void add_not_equal_cond (value *arg1, value *arg2);
+
+  /* Adds greater than condition for two values.  */
+  void add_greater_than_cond (value *arg1, value *arg2);
+
+  /* Adds less than condition for two values.  */
+  void add_less_than_cond (value *arg1, value *arg2);
+
+  /* Adds greater or equal condition for two values.  */
+  void add_greater_or_equal_cond (value *arg1, value *arg2);
+
+  /* Adds less or equal condition for two values.  */
+  void add_less_or_equal_cond (value *arg1, value *arg2);
+
+  /* Does preprocessing and postprocessing for condition adding.
+     Handles value creation for constants and their removement in the end.  */
+  bool add_binary_cond (tree arg1, tree arg2, binary_cond_func cond_func);
+
+  /* Constructs expression trees of greater than condition for given values.  */
+  bit_expression *construct_great_than_cond (value *arg1, value *arg2);
+
+  /* Constructs expression trees of less than condition for given values.  */
+  bit_expression *construct_less_than_cond (value *arg1, value *arg2);
+
+  /* Constructs expression trees of equal condition for given values.  */
+  bit_expression *construct_equal_cond (value *arg1, value *arg2);
+
+  /* A wrapper for operations on two bits.
+     Operation and operands are passed as arguments.  */
+  static value_bit *operate_bits (bit_func bit_op, value_bit *bit1,
+				  value_bit *bit2, value_bit **bit3);
+
+  /* A wrapper for operations on three bits.
+     Operation and operands are passed as arguments.  */
+  static value_bit *operate_bits (bit_func3 bit_op, value_bit *bit1,
+				  value_bit *bit2, value_bit **bit3);
+
+  /* Performs the given operation on passed arguments.
+     The result is stored in dest.  */
+  template<class func>
+  void operate (value *arg1, value *arg2, value_bit **bit_arg, tree dest,
+		func bit_op);
+
+  /* Does preprocessing and postprocessing for expressions with tree operands.
+     Handles value creation for constant and their removement in the end.  */
+  bool do_binary_operation (tree arg1, tree arg2, tree dest,
+			    binary_func bin_func);
+
+  /* Performs AND operation on given values.  The result is stored in dest.  */
+  void do_and (value *arg1, value *arg2, tree dest);
+
+  /* Performs OR operation on given values.  The result is stored in dest.  */
+  void do_or (value *arg1, value *arg2, tree dest);
+
+  /* Performs XOR operation on given values.  The result is stored in dest.  */
+  void do_xor (value *arg1, value *arg2, tree dest);
+
+  /* Performs shift right operation on given values.
+     The result is stored in dest.  */
+  void do_shift_right (value *arg1, value *arg2, tree dest);
+
+  /* Performs shift left operation on given values.
+     The result is stored in dest.  */
+  void do_shift_left (value *arg1, value *arg2, tree dest);
+
+  /* Adds given values.  The result is stored in dest.  */
+  void do_add (value *arg1, value *arg2, tree dest);
+
+  /* Subtracks second value from the first.  The result is stored in dest.  */
+  void do_sub (value *arg1, value *arg2, tree dest);
+
+  /* Performs AND operation on two bits.  */
+  static value_bit *and_two_bits (value_bit *arg1, value_bit *arg2);
+
+  /* ANDs every bit of the value with var_bit, stroes the result in var1.  */
+  void and_number_bit (value *var1, value_bit *var_bit);
+
+  /* Multiplies given values.  The result is stored in dest.  */
+  void do_mul (value *arg1, value *arg2, tree dest);
+
+  /* Performs AND operation for 2 symbolic_bit operands.  */
+  static value_bit *and_sym_bits (const value_bit *var1,
+				  const value_bit *var2);
+
+  /* Performs AND operation for a symbolic_bit and const_bit operands.  */
+  static value_bit *and_var_const (const value_bit *var1,
+				   const bit *const_bit);
+
+  /* Performs AND operation for 2 constant bit operands.  */
+  static bit *and_const_bits (const bit *const_bit1, const bit *const_bit2);
+
+  /* Performs OR operation on two bits.  */
+  static value_bit *or_two_bits (value_bit *arg1_bit, value_bit *arg2_bit);
+
+  /* Performs OR operation for 2 symbolic_bit operands.  */
+  static value_bit *or_sym_bits (const value_bit *var1,
+				 const value_bit *var2);
+
+  /* Performs OR operation for a symbolic_bit and a constant bit operands.  */
+  static value_bit *or_var_const (const value_bit *var1,
+				  const bit *const_bit);
+
+  /* Performs OR operation for 2 constant bit operands.  */
+  static bit *or_const_bits (const bit *const_bit1, const bit *const_bit2);
+
+  /* Performs complement operation on a bit.  */
+  static value_bit *complement_a_bit (value_bit *var);
+
+  /* Performs NOT operation for constant bit.  */
+  static bit *complement_const_bit (const bit *const_bit);
+
+  /* Performs NOT operation for symbolic_bit.  */
+  static value_bit *complement_sym_bit (const value_bit *var);
+
+  /* Performs XOR operation on two bits.  */
+  static value_bit *xor_two_bits (value_bit *var1, value_bit *var2);
+
+  /* Performs XOR operation for 2 symbolic_bit operands.  */
+  static value_bit *xor_sym_bits (const value_bit *var1,
+				  const value_bit *var2);
+
+  /* Performs XOR operation for 2 constant bit operands.  */
+  static bit *xor_const_bits (const bit *const_bit1, const bit *const_bit2);
+
+  /* Performs XOR operation for a symbolic_bit and const_bit operands.  */
+  static value_bit *xor_var_const (const value_bit *var,
+				   const bit *const_bit);
+
+  /* Shift_right operation.  Case: var2 is a symbolic value.  */
+  static value_bit *shift_right_sym_bits (value_bit *var1, value_bit *var2);
+
+  /* Shift_left operation.  Case: var2 is a symbolic value.  */
+  static value_bit *shift_left_sym_bits (value_bit *var1, value_bit *var2);
+
+  /* Shifts var right by size of shift_value.  */
+  value *shift_right_by_const (value *var, size_t shift_value);
+
+  /* Return node which has a const bit child.  Traversal is done based
+     on safe branching.  */
+  static void get_parent_with_const_child (value_bit *root,
+					   bit_expression *&parent,
+					   bit_expression *&parent_of_parent);
+
+  /* Checks whether state for variable with specified name already
+     exists or not.  */
+  bool is_declared (tree var);
+
+  /* Declares given variable if it has not been declared yet.  */
+  void declare_if_needed (tree var, size_t size);
+
+  /* Shifts number left by size of shift_value.  */
+  value *shift_left_by_const (const value *number, size_t shift_value);
+
+  /* Adds two bits and carry value.
+     Resturn result and stores new carry bit in "carry".  */
+  static value_bit *full_adder (value_bit *var1, value_bit *var2,
+				value_bit **carry);
+
+  /* Returns the additive inverse of the given number.  */
+  value *additive_inverse (const value *number);
+
+  /* Adds two values, stores the result in the first one.  */
+  void add_numbers (value *var1, const value *var2);
+
+  /* Make a copy of given bits.  */
+  static vec<value_bit *> *make_copy (vec<value_bit *> *bits);
+
+ public:
+  state () = default;
+
+  ~state ();
+
+  /* Adds an empty state for the given variable.  */
+  bool decl_var (tree name, unsigned size);
+
+  state (const state &s);
+
+  /* Adds the given variable to state.  */
+  bool add_var_state (tree var, value *state);
+
+  /* Remove all states from the states' vector.  */
+  static void remove_states (vec<state *> *states);
+
+  /* Remove all states from the states' vector and release the vector.  */
+  static void clear_states (vec<state *> *states);
+
+  /* Removes all variables added to the state.  */
+  void clear_var_states ();
+
+  /* Removes all conditions added to the state.  */
+  void clear_conditions ();
+
+  /* Adds the given condition to the state.  */
+  bool add_condition (bit_expression *cond);
+
+  /* Bulk add the given conditions to the state.  */
+  bool bulk_add_conditions (const hash_set<bit_expression *> &conds);
+
+  /* Get value of the given variable.  */
+  value *get_value (tree var);
+
+  /* Get the value of the tree, which is in the beginning of the var_states.  */
+  value *get_first_value ();
+
+  /* Returns the list of conditions in the state.  */
+  const hash_set<bit_expression *> &get_conditions ();
+
+  /* Adds a variable with unknown value to state.  Such variables are
+     represented as sequence of symbolic bits.  */
+  bool make_symbolic (tree var, unsigned size);
+
+  /* Returns size of the given variable.  */
+  unsigned get_var_size (tree var);
+
+  /* Prints the given value.  */
+  static void print_value (value *var);
+
+  /* Prints added conditions.  */
+  void print_conditions ();
+
+  /* Returns the number represented by the value.  */
+  static unsigned HOST_WIDE_INT
+  make_number (const value *var);
+
+  /* Checks if all bits of the given value have constant bit type.  */
+  static bool is_bit_vector (const value *var);
+
+  /* Performs the specified operation on passed variables.  */
+  bool do_operation (tree_code op_code, tree arg1, tree arg2, tree dest);
+
+  /* Does Assignment.  */
+  bool do_assign (tree arg, tree dest);
+
+  /* Assigns pow 2 value.  */
+  bool do_assign_pow2 (tree dest, unsigned pow);
+
+  /* Negates given variable.  */
+  bool do_complement (tree arg, tree dest);
+
+  /* Adds EQUAL condition of given variables to state.  */
+  bool add_equal_cond (tree arg1, tree arg2);
+
+  /* Adds NOT EQUAL condition of given variables to state.  */
+  bool add_not_equal_cond (tree arg1, tree arg2);
+
+  /* Adds GREATER THAN condition of given variables to state.  */
+  bool add_greater_than_cond (tree arg1, tree arg2);
+
+  /* Adds LESS THAN condition of given variables to state.  */
+  bool add_less_than_cond (tree arg1, tree arg2);
+
+  /* Adds GREATER OR EQUAL condition of given variables to state.  */
+  bool add_greater_or_equal_cond (tree arg1, tree arg2);
+
+  /* Adds LESS OR EQUAL condition of given variables to state.  */
+  bool add_less_or_equal_cond (tree arg1, tree arg2);
+
+  /* Adds a bool condition to state.  */
+  bool add_bool_cond (tree arg);
+
+  /* Checks whether the given two constant values are equal.  */
+  static bool check_const_value_equality (value *arg1, value *arg2);
+
+  /* Checks whether the given two constant values are not equal.  */
+  static bool check_const_value_are_not_equal (value *arg1, value *arg2);
+
+  /* Checks whether the first given constant value
+     is greater than the second one.  */
+  static bool check_const_value_is_greater_than (value *arg1, value *arg2);
+
+  /* Checks whether the first given constant value
+     is less than the second one.  */
+  static bool check_const_value_is_less_than (value *arg1, value *arg2);
+
+  /* For the given value_bit, iterates over its expression tree, complements
+     those bit which came from the given origin.  */
+  static value_bit *complement_bits_with_origin (value_bit *root, tree origin);
+
+  /* Iterates over every bit of the given value and complements their
+     expression trees' those bits, that came from the given origin.  */
+  static void complement_val_bits_with_origin (value *val, tree origin);
+
+  /* Complements all bits of all values that came from the given origin.  */
+  void complement_all_vars_bits_with_origin (tree origin);
+
+  /* Complements all bits with the given origin of all added conditions.  */
+  void complement_conditions_with_origin (tree origin);
+
+  /* Complements all bits with the given origin of all values
+     and added conditions.  */
+  void complement_state_with_origin (tree origin);
+
+  /* Returns status of last added condition.  */
+  condition_status get_last_cond_status ();
+};
+
+
+size_t min (size_t a, size_t b, size_t c);
+
+
+/* Performs the given operation on passed arguments.
+   The result is stored in dest.  */
+
+template<class func>
+void
+state::operate (value *arg1, value *arg2, value_bit **bit_arg, tree dest,
+		func bit_op)
+{
+  value *dest_var = var_states.get (dest);
+  size_t min_iter = min (arg1->length (), arg2->length (), dest_var->length ());
+
+  size_t i = 0;
+  for (; i < min_iter; i++)
+    {
+      value_bit *temp = (*var_states.get (dest))[i];
+      (*var_states.get (dest))[i] = operate_bits (bit_op, (*arg1)[i],
+						  (*arg2)[i], bit_arg);
+      delete temp;
+    }
+
+  if (i >= dest_var->length ())
+    return;
+
+  value *biggest = arg1;
+  value_bit *sign_bit = (*arg2)[i - 1];
+  if (arg2->length () > arg1->length ())
+    {
+      biggest = arg2;
+      sign_bit = (*arg1)[i - 1];
+    }
+
+  min_iter = min (biggest->length (), dest_var->length (), dest_var->length ());
+  for (; i < min_iter; i++)
+    {
+      value_bit *temp = (*var_states.get (dest))[i];
+      (*var_states.get (dest))[i] = operate_bits (bit_op, (*biggest)[i],
+						  sign_bit, bit_arg);
+      delete temp;
+    }
+
+  if (i >= dest_var->length ())
+    return;
+
+  sign_bit = (*biggest)[i - 1];
+  for (; i < dest_var->length (); i++)
+    {
+      value_bit *temp = (*var_states.get (dest))[i];
+      (*var_states.get (dest))[i] = operate_bits (bit_op, sign_bit, sign_bit,
+						  bit_arg);
+      delete temp;
+    }
+}
+
+#endif /* SYM_EXEC_STATE_H.  */
-- 
2.25.1