sym-exec v2: - Done refactoring in expression.* and state.* - Added is-a-helper test functions for expression classes - Added initial version of conditions

9 files changed, 802 insertions, 236 deletions

diff --git a/gcc/Makefile.in b/gcc/Makefile.in
index d67213d0d2d..0365e599cfa 100644
--- a/gcc/Makefile.in
+++ b/gcc/Makefile.in
@@ -1651,6 +1651,7 @@ OBJS = \
 	gimple-crc-optimization.o \
 	sym-exec/expression.o \
 	sym-exec/state.o \
+	sym-exec/condition.o \
 	tree-nested.o \
 	tree-nrv.o \
 	tree-object-size.o \
diff --git a/gcc/gimple-crc-optimization.cc b/gcc/gimple-crc-optimization.cc
index e57b3bc71af..faed3efb1e1 100644
--- a/gcc/gimple-crc-optimization.cc
+++ b/gcc/gimple-crc-optimization.cc
@@ -34,7 +34,7 @@ along with GCC; see the file COPYING3.  If not see
 #include "gimple-range.h"
 #include "tree-scalar-evolution.h"
 #include "hwint.h"
-#include "gimple-pretty-print.h"
+#include "gimple-pretty-print.h
 
 class crc_optimization {
  private:
diff --git a/gcc/sym-exec/condition.cc b/gcc/sym-exec/condition.cc
new file mode 100644
index 00000000000..dc42cf9c221
--- /dev/null
+++ b/gcc/sym-exec/condition.cc
@@ -0,0 +1,37 @@
+#include "condition.h"
+
+
+bit_condition::bit_condition (value* left, value* right, condition_type type)
+{
+  this->left = left;
+  this->right = right;
+  this->type = type;
+}
+
+
+bit_condition::bit_condition (const bit_condition &expr)
+{
+  bit_expression::copy (&expr);
+  type = expr.get_cond_type ();
+}
+
+
+condition_type
+bit_condition::get_cond_type () const
+{
+  return type;
+}
+
+
+value *
+bit_condition::copy () const
+{
+  return new bit_condition (*this);
+}
+
+
+value_type
+bit_condition::get_type () const
+{
+  return value_type::BIT_CONDITION;
+}
\ No newline at end of file
diff --git a/gcc/sym-exec/condition.h b/gcc/sym-exec/condition.h
new file mode 100644
index 00000000000..5c595197551
--- /dev/null
+++ b/gcc/sym-exec/condition.h
@@ -0,0 +1,35 @@
+#ifndef SYM_EXEC_CONDITION_H
+#define SYM_EXEC_CONDITION_H
+
+#include "expression.h"
+
+enum condition_type
+{
+  GREAT_THAN,
+  LESS_THAN,
+  NOT_ZERO,
+  EQUAL,
+  NOT_EQUAL,
+  GREAT_OR_EQUAL,
+  IS_FALSE,
+  IS_TRUE
+};
+
+
+class bit_condition : public bit_expression
+{
+ private:
+  condition_type type;
+
+ public:
+  bit_condition (value* left, value* right, condition_type type);
+  bit_condition (const bit_condition &expr);
+  condition_type get_cond_type () const;
+  value *copy () const;
+  value_type get_type () const;
+};
+
+
+
+
+#endif /* SYM_EXEC_CONDITION_H.  */
\ No newline at end of file
diff --git a/gcc/sym-exec/expression-is-a-helper.h b/gcc/sym-exec/expression-is-a-helper.h
new file mode 100644
index 00000000000..9cf50e90698
--- /dev/null
+++ b/gcc/sym-exec/expression-is-a-helper.h
@@ -0,0 +1,116 @@
+#ifndef SYM_EXEC_EXPRESSION_IS_A_HELPER_H
+#define SYM_EXEC_EXPRESSION_IS_A_HELPER_H
+
+#include "expression.h"
+#include "is-a.h"
+
+
+/* Defining test functions for value conversion via dyn_cast.  */
+
+template <>
+template <>
+inline bool
+is_a_helper <symbolic_bit *>::test (value * ptr)
+{
+  return ptr->get_type () == value_type::SYMBOLIC_BIT;
+}
+
+
+template <>
+template <>
+inline bool
+is_a_helper <bit *>::test (value * ptr)
+{
+  return ptr->get_type () == value_type::BIT;
+}
+
+
+template <>
+template <>
+inline bool
+is_a_helper <bit_expression *>::test (value * 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;
+}
+
+
+template <>
+template <>
+inline bool
+is_a_helper <bit_and_expression *>::test (value * ptr)
+{
+  return ptr->get_type () == value_type::BIT_AND_EXPRESSION;
+}
+
+
+template <>
+template <>
+inline bool
+is_a_helper <bit_or_expression *>::test (value * ptr)
+{
+  return ptr->get_type () == value_type::BIT_OR_EXPRESSION;
+}
+
+
+template <>
+template <>
+inline bool
+is_a_helper <bit_xor_expression *>::test (value * ptr)
+{
+  return ptr->get_type () == value_type::BIT_XOR_EXPRESSION;
+}
+
+
+template <>
+template <>
+inline bool
+is_a_helper <bit_complement_expression *>::test (value * ptr)
+{
+  return ptr->get_type () == value_type::BIT_COMPLEMENT_EXPRESSION;
+}
+
+
+template <>
+template <>
+inline bool
+is_a_helper <shift_left_expression *>::test (value * ptr)
+{
+  return ptr->get_type () == value_type::SHIFT_LEFT_EXPRESSION;
+}
+
+
+template <>
+template <>
+inline bool
+is_a_helper <shift_right_expression *>::test (value * ptr)
+{
+  return ptr->get_type () == value_type::SHIFT_RIGHT_EXPRESSION;
+}
+
+
+template <>
+template <>
+inline bool
+is_a_helper <add_expression *>::test (value * ptr)
+{
+  return ptr->get_type () == value_type::ADD_EXPRESSION;
+}
+
+
+template <>
+template <>
+inline bool
+is_a_helper <sub_expression *>::test (value * ptr)
+{
+  return ptr->get_type () == value_type::SUB_EXPRESSION;
+}
+
+#endif /* SYM_EXEC_EXPRESSION_IS_A_HELPER_H.  */
\ No newline at end of file
diff --git a/gcc/sym-exec/expression.cc b/gcc/sym-exec/expression.cc
index e2aad4b483e..5bf46367796 100644
--- a/gcc/sym-exec/expression.cc
+++ b/gcc/sym-exec/expression.cc
@@ -4,13 +4,7 @@
 
 #include "stddef.h"
 #include "expression.h"
-
-
-bit_expression::bit_expression (value* left, value* right)
-{
-  this->left = left;
-  this->right = right;
-}
+#include "expression-is-a-helper.h"
 
 
 value *
@@ -62,9 +56,11 @@ bit::set_val (unsigned char new_val)
 }
 
 
-bit_complement_expression::bit_complement_expression (value *right) :
-  bit_expression (nullptr, right)
-{}
+bit_complement_expression::bit_complement_expression (value *right)
+{
+  this->left = nullptr;
+  this->right = right;
+}
 
 
 value*
@@ -81,88 +77,237 @@ bit::copy () const
 }
 
 
-bit_expression::bit_expression (const bit_expression &expr)
+void
+bit_expression::copy (const bit_expression *expr)
 {
-  if (expr.left)
-    {
-      left = expr.left->copy ();
-    }
-
-  if (expr.right)
-    {
-      right = expr.right->copy ();
-    }
-}
+  if (expr->left)
+    left = expr->left->copy ();
 
-
-value *
-bit_expression::copy () const
-{
-  return new bit_expression (*this);
+  if (expr->right)
+    right = expr->right->copy ();
 }
 
 
 value *
 bit_xor_expression::copy () const
 {
-  return bit_expression::copy ();
+  return new bit_xor_expression (*this);
 }
 
 
 value *
 bit_and_expression::copy () const
 {
-  return bit_expression::copy ();
+  return new bit_and_expression (*this);
 }
 
 
 value *
 bit_or_expression::copy () const
 {
-  return bit_expression::copy ();
+  return new bit_or_expression (*this);
 }
 
 
 value *
 shift_right_expression::copy () const
 {
-  return bit_expression::copy ();
+  return new shift_right_expression (*this);
 }
 
 
 value *
 shift_left_expression::copy () const
 {
-  return bit_expression::copy ();
+  return new shift_left_expression (*this);
 }
 
 
 value *
 add_expression::copy () const
 {
-  return bit_expression::copy ();
+  return new add_expression (*this);
 }
 
 
 value *
 sub_expression::copy () const
 {
-  return bit_expression::copy ();
+  return new sub_expression (*this);
 }
 
 
 value *
 bit_complement_expression::copy () const
 {
-  return bit_expression::copy ();
+  return new bit_complement_expression (*this);
+}
+
+
+bit_complement_expression::bit_complement_expression (
+	const bit_complement_expression& expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+bit_xor_expression::bit_xor_expression (value *left, value *right)
+{
+  this->left = left;
+  this->right = right;
+}
+
+
+bit_xor_expression::bit_xor_expression (const bit_xor_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+bit_and_expression::bit_and_expression (value *left, value *right)
+{
+  this->left = left;
+  this->right = right;
+}
+
+
+bit_and_expression::bit_and_expression (const bit_and_expression& expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+bit_or_expression::bit_or_expression (value *left, value *right)
+{
+  this->left = left;
+  this->right = right;
+}
+
+
+bit_or_expression::bit_or_expression (const bit_or_expression& expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+shift_right_expression::shift_right_expression (value *left, value *right)
+{
+  this->left = left;
+  this->right = right;
+}
+
+
+shift_right_expression::shift_right_expression (
+	const shift_right_expression& expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+shift_left_expression::shift_left_expression (value *left, value *right)
+{
+  this->left = left;
+  this->right = right;
+}
+
+
+shift_left_expression::shift_left_expression (const shift_left_expression& expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+add_expression::add_expression (value *left, value *right)
+{
+  this->left = left;
+  this->right = right;
+}
+
+
+add_expression::add_expression (const add_expression& expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+sub_expression::sub_expression (value *left, value *right)
+{
+  this->left = left;
+  this->right = right;
+}
+
+
+sub_expression::sub_expression (const sub_expression& expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+value_type
+symbolic_bit::get_type () const
+{
+  return value_type::SYMBOLIC_BIT;
 }
 
 
-bit_expression::~bit_expression ()
+value_type
+bit::get_type () const
 {
-  delete left;
-  left = nullptr;
+  return value_type::BIT;
+}
+
+
+value_type
+bit_and_expression::get_type () const
+{
+  return value_type::BIT_AND_EXPRESSION;
+}
+
+
+value_type
+bit_or_expression::get_type () const
+{
+  return value_type::BIT_OR_EXPRESSION;
+}
+
+
+value_type
+bit_xor_expression::get_type () const
+{
+  return value_type::BIT_XOR_EXPRESSION;
+}
+
 
-  delete right;
-  right = nullptr;
+value_type
+bit_complement_expression::get_type () const
+{
+  return value_type::BIT_COMPLEMENT_EXPRESSION;
+}
+
+
+value_type
+shift_left_expression::get_type () const
+{
+  return value_type::SHIFT_LEFT_EXPRESSION;
+}
+
+
+value_type
+shift_right_expression::get_type () const
+{
+  return value_type::SHIFT_RIGHT_EXPRESSION;
+}
+
+
+value_type
+add_expression::get_type () const
+{
+  return value_type::ADD_EXPRESSION;
+}
+
+
+value_type
+sub_expression::get_type () const
+{
+  return value_type::SUB_EXPRESSION;
 }
diff --git a/gcc/sym-exec/expression.h b/gcc/sym-exec/expression.h
index 0cb7a6c69df..45c327599da 100644
--- a/gcc/sym-exec/expression.h
+++ b/gcc/sym-exec/expression.h
@@ -7,6 +7,21 @@
 
 #include "stddef.h"
 
+
+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 {
@@ -26,6 +41,7 @@ class value {
 
   /* This will support deep copy of objects' values.  */
   virtual value *copy () const = 0;
+  virtual value_type get_type () const = 0;
   virtual ~value ()
   {};
 };
@@ -41,6 +57,7 @@ class symbolic_bit : public value {
   {};
 
   value *copy () const;
+  value_type get_type () const;
 };
 
 
@@ -59,6 +76,7 @@ class bit : public value {
   unsigned char get_val () const;
   void set_val (unsigned char new_val);
   value *copy () const;
+  value_type get_type () const;
 };
 
 
@@ -70,20 +88,16 @@ class bit_expression : public value {
   value *left = nullptr;
   value *right = nullptr;
 
- public:
-  bit_expression () : left (nullptr), right (nullptr)
-  {};
-  bit_expression (value *left, value *right);
-
-  bit_expression (const bit_expression &expr);
+  void copy (const bit_expression *expr);
 
+ public:
   value *get_left ();
   value *get_right ();
 
   void set_left (value *expr);
   void set_right (value *expr);
-  value *copy () const;
-  virtual ~bit_expression ();
+  value *copy () const = 0;
+  value_type get_type () const = 0;
 };
 
 
@@ -93,11 +107,10 @@ class bit_expression : public value {
 
 class bit_xor_expression : public bit_expression {
  public:
-  bit_xor_expression (value *left, value *right) : bit_expression (left, right)
-  {};
-  bit_xor_expression (const bit_xor_expression &expr) : bit_expression (expr)
-  {};
+  bit_xor_expression (value *left, value *right);
+  bit_xor_expression (const bit_xor_expression &expr);
   value *copy () const;
+  value_type get_type () const;
 };
 
 
@@ -107,11 +120,10 @@ class bit_xor_expression : public bit_expression {
 
 class bit_and_expression : public bit_expression {
  public:
-  bit_and_expression (value *left, value *right) : bit_expression (left, right)
-  {};
-  bit_and_expression (const bit_and_expression &expr) : bit_expression (expr)
-  {};
+  bit_and_expression (value *left, value *right);
+  bit_and_expression (const bit_and_expression &expr);
   value *copy () const;
+  value_type get_type () const;
 };
 
 
@@ -121,11 +133,10 @@ class bit_and_expression : public bit_expression {
 
 class bit_or_expression : public bit_expression {
  public:
-  bit_or_expression (value *left, value *right) : bit_expression (left, right)
-  {};
-  bit_or_expression (bit_or_expression &expr) : bit_expression (expr)
-  {};
+  bit_or_expression (value *left, value *right);
+  bit_or_expression (const bit_or_expression &expr);
   value *copy () const;
+  value_type get_type () const;
 };
 
 
@@ -133,13 +144,10 @@ class bit_or_expression : public bit_expression {
 
 class shift_right_expression : public bit_expression {
  public:
-  shift_right_expression (value *left, value *right) : bit_expression (left,
-								       right)
-  {};
-  shift_right_expression (const shift_right_expression &expr)
-			 : bit_expression (expr)
-  {};
+  shift_right_expression (value *left, value *right);
+  shift_right_expression (const shift_right_expression &expr);
   value *copy () const;
+  value_type get_type () const;
 };
 
 
@@ -147,13 +155,10 @@ class shift_right_expression : public bit_expression {
 
 class shift_left_expression : public bit_expression {
  public:
-  shift_left_expression (value *left, value *right) : bit_expression (left,
-								      right)
-  {};
-  shift_left_expression (const shift_left_expression &expr)
-			: bit_expression (expr)
-  {};
+  shift_left_expression (value *left, value *right);
+  shift_left_expression (const shift_left_expression &expr);
   value *copy () const;
+  value_type get_type () const;
 };
 
 
@@ -161,11 +166,10 @@ class shift_left_expression : public bit_expression {
 
 class add_expression : public bit_expression {
  public:
-  add_expression (value *left, value *right) : bit_expression (left, right)
-  {};
-  add_expression (const add_expression &expr) : bit_expression (expr)
-  {};
+  add_expression (value *left, value *right);
+  add_expression (const add_expression &expr);
   value *copy () const;
+  value_type get_type () const;
 };
 
 
@@ -173,11 +177,10 @@ class add_expression : public bit_expression {
 
 class sub_expression : public bit_expression {
  public:
-  sub_expression (value *left, value *right) : bit_expression (left, right)
-  {};
-  sub_expression (const sub_expression &expr) : bit_expression (expr)
-  {};
+  sub_expression (value *left, value *right);
+  sub_expression (const sub_expression &expr);
   value *copy () const;
+  value_type get_type () const;
 };
 
 /* Bit-level negation expression.  */
@@ -185,10 +188,10 @@ class sub_expression : public bit_expression {
 class bit_complement_expression : public bit_expression {
  public:
   bit_complement_expression (value *right);
-  bit_complement_expression (const bit_complement_expression &expr)
-  			    : bit_expression (expr)
-  {};
+  bit_complement_expression (const bit_complement_expression &expr);
   value *copy () const;
+  value_type get_type () const;
 };
 
-#endif /* SYM_EXEC_EXPRESSION_H.  */
+
+#endif /* SYM_EXEC_EXPRESSION_H.  */
\ No newline at end of file
diff --git a/gcc/sym-exec/state.cc b/gcc/sym-exec/state.cc
index 8081e30beff..7caffbcd87f 100644
--- a/gcc/sym-exec/state.cc
+++ b/gcc/sym-exec/state.cc
@@ -6,14 +6,15 @@
 #include "state.h"
 #include "vec.h"
 #include "hash-set.h"
-#include "expression.h"
+#include "condition.h"
+//#include "expression.h"
 
 
 /* Checks whether state for variable with specified name already
    exists or not.  */
 
 bool
-State::is_declared (tree *var)
+State::is_declared (tree var)
 {
   return var_states.get (var) != NULL;
 }
@@ -85,7 +86,7 @@ State::or_const_bits (const bit * const_bit1, const bit * const_bit2) const
 /* Adds an empty state for the given variable.  */
 
 bool
-State::decl_var (tree *var, unsigned size)
+State::decl_var (tree var, unsigned size)
 {
   if (is_declared (var))
     return false;
@@ -102,7 +103,7 @@ State::decl_var (tree *var, unsigned size)
 /* Returns size of the given variable.  */
 
 unsigned
-State::get_var_size (tree *var)
+State::get_var_size (tree var)
 {
   vec < value * > *content = var_states.get (var);
   if (content == NULL)
@@ -116,7 +117,7 @@ State::get_var_size (tree *var)
    represented as sequence of symbolic bits.  */
 
 bool
-State::make_symbolic (tree *var, unsigned size)
+State::make_symbolic (tree var, unsigned size)
 {
   if (is_declared (var))
     return false;
@@ -135,7 +136,7 @@ State::make_symbolic (tree *var, unsigned size)
 /* Does bit-level AND operation for given variables.  */
 
 void
-State::do_and (tree* arg1, tree* arg2, tree* dest)
+State::do_and (tree arg1, tree arg2, tree dest)
 {
   gcc_assert (!(is_declared (arg1) || is_declared (arg2)
 		|| is_declared (dest)));
@@ -148,27 +149,22 @@ State::do_and (tree* arg1, tree* arg2, tree* dest)
   for (size_t i = 0; i < get_var_size (dest); i++)
   {
     value *result = nullptr;
-    value *sym_bit1 = dyn_cast<symbolic_bit *> ((*var_states.get (arg1))[i]);
-    if (sym_bit1 == nullptr)
-      sym_bit1 = dyn_cast<bit_expression *> ((*var_states.get (arg1))[i]);
-
-    value *sym_bit2 = dyn_cast<symbolic_bit *> ((*var_states.get (arg2))[i]);
-    if (sym_bit2 == nullptr)
-      sym_bit2 = dyn_cast<bit_expression *> ((*var_states.get (arg2))[i]);
-
-    bit *const_bit1 = dyn_cast<bit *> ((*var_states.get (arg1))[i]);
-    bit *const_bit2 = dyn_cast<bit *> ((*var_states.get (arg2))[i]);
-
-    if (sym_bit1 && sym_bit2)
-      result = and_sym_bits (sym_bit1, sym_bit2);
-    else if (sym_bit1 && const_bit2)
-      result = and_var_const (sym_bit1, const_bit2);
-    else if (const_bit1 && sym_bit2)
-      result = and_var_const (sym_bit2, const_bit1);
-    else if (const_bit1 && const_bit2)
-      result = and_const_bits (const_bit1, const_bit2);
+    value * arg1_bit = (*var_states.get (arg1))[i];
+    value * arg2_bit = (*var_states.get (arg2))[i];
+
+    if (is_a<bit *> (arg1_bit) && is_a<bit *> (arg2_bit))
+      result = and_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 = and_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 = and_var_const (arg1_bit, as_a<bit *> (arg2_bit));
+
     else
-      gcc_assert (true);
+      result = and_sym_bits (arg1_bit, arg2_bit);
 
     delete (*var_states.get (dest))[i];
     (*var_states.get (dest))[i] = result;
@@ -179,7 +175,7 @@ State::do_and (tree* arg1, tree* arg2, tree* dest)
 /* Does bit-level OR operation for given variables.  */
 
 void
-State::do_or (tree* arg1, tree* arg2, tree* dest)
+State::do_or (tree arg1, tree arg2, tree dest)
 {
   gcc_assert (!(is_declared (arg1) || is_declared (arg2)
 		|| is_declared (dest)));
@@ -191,27 +187,22 @@ State::do_or (tree* arg1, tree* arg2, tree* dest)
   for (size_t i = 0; i < get_var_size (dest); i++)
   {
     value *result = nullptr;
-    value *sym_bit1 = dyn_cast<symbolic_bit *> ((*var_states.get (arg1))[i]);
-    if (sym_bit1 == nullptr)
-      sym_bit1 = dyn_cast<bit_expression *> ((*var_states.get (arg1))[i]);
-
-    value *sym_bit2 = dyn_cast<symbolic_bit *> ((*var_states.get (arg2))[i]);
-    if (sym_bit2 == nullptr)
-      sym_bit2 = dyn_cast<bit_expression *> ((*var_states.get (arg2))[i]);
-
-    bit *const_bit1 = dyn_cast<bit *> ((*var_states.get (arg1))[i]);
-    bit *const_bit2 = dyn_cast<bit *> ((*var_states.get (arg2))[i]);
-
-    if (sym_bit1 && sym_bit2)
-      result = or_sym_bits (sym_bit1, sym_bit2);
-    else if (sym_bit1 && const_bit2)
-      result = or_var_const (sym_bit1, const_bit2);
-    else if (const_bit1 && sym_bit2)
-      result = or_var_const (sym_bit2, const_bit1);
-    else if (const_bit1 && const_bit2)
-      result = or_const_bits (const_bit1, const_bit2);
+    value * arg1_bit = (*var_states.get (arg1))[i];
+    value * arg2_bit = (*var_states.get (arg2))[i];
+
+    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
-      gcc_assert (true);
+      result = or_sym_bits (arg1_bit, arg2_bit);
 
     delete (*var_states.get (dest))[i];
     (*var_states.get (dest))[i] = result;
@@ -222,7 +213,7 @@ State::do_or (tree* arg1, tree* arg2, tree* dest)
 /* Does bit-level XOR operation for given variables.  */
 
 void
-State::do_xor (tree *arg1, tree *arg2, tree *dest)
+State::do_xor (tree arg1, tree arg2, tree dest)
 {
   gcc_assert (!(is_declared (arg1) || is_declared (arg2)
 		|| is_declared (dest)));
@@ -232,27 +223,22 @@ State::do_xor (tree *arg1, tree *arg2, tree *dest)
   for (size_t i = 0; i < get_var_size (dest); i++)
   {
     value *result = nullptr;
-    value *sym_bit1 = dyn_cast<symbolic_bit *> ((*var_states.get (arg1))[i]);
-    if (sym_bit1 == nullptr)
-      sym_bit1 = dyn_cast<bit_expression *> ((*var_states.get (arg1))[i]);
-
-    value *sym_bit2 = dyn_cast<symbolic_bit *> ((*var_states.get (arg2))[i]);
-    if (sym_bit2 == nullptr)
-      sym_bit2 = dyn_cast<bit_expression *> ((*var_states.get (arg2))[i]);
-
-    bit *const_bit1 = dyn_cast<bit *> ((*var_states.get (arg1))[i]);
-    bit *const_bit2 = dyn_cast<bit *> ((*var_states.get (arg2))[i]);
-
-    if (sym_bit1 && sym_bit2)
-      result = xor_sym_bits (sym_bit1, sym_bit2);
-    else if (sym_bit1 && const_bit2)
-      result = xor_var_const (sym_bit1, const_bit2);
-    else if (const_bit1 && sym_bit2)
-      result = xor_var_const (sym_bit2, const_bit1);
-    else if (const_bit1 && const_bit2)
-      result = xor_const_bits (const_bit1, const_bit2);
+    value * arg1_bit = (*var_states.get (arg1))[i];
+    value * arg2_bit = (*var_states.get (arg2))[i];
+
+    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
-      gcc_assert (true);
+      result = xor_sym_bits (arg1_bit, arg2_bit);
 
     delete (*var_states.get (dest))[i];
     (*var_states.get (dest))[i] = result;
@@ -260,11 +246,11 @@ State::do_xor (tree *arg1, tree *arg2, tree *dest)
 }
 
 
-/* Shifts value_vector left by shift_value bits.  */
+/* Shifts value_vector right by shift_value bits.  */
 
 vec <value *>
-State::shift_left_by_const (const vec < value * > * value_vector,
-			    size_t shift_value)
+State::shift_right_by_const (const vec <value *> * value_vector,
+			     size_t shift_value)
 {
   vec <value *> shift_result;
   shift_result.create (value_vector->length ());
@@ -296,7 +282,7 @@ State::is_bit_vector (vec <value *>* value_vector)
 }
 
 
-/* returns the value of the number represented as a bit vector.  */
+/* Returns the value of the number represented as a bit vector.  */
 
 size_t
 State::get_value (vec <value *> * bit_vector)
@@ -315,7 +301,7 @@ State::get_value (vec <value *> * bit_vector)
 /* shift_left operation.  Case: var2 is a sym_bit.  */
 
 void
-State::shift_left_sym_bits (tree * var1, tree * var2, tree * dest)
+State::shift_left_sym_bits (tree var1, tree var2, tree dest)
 {
   for (size_t i = 0; i < get_var_size (dest); i++)
   {
@@ -329,10 +315,10 @@ State::shift_left_sym_bits (tree * var1, tree * var2, tree * dest)
 }
 
 
-/* Does SHIFT_LEFT operation for given variables.  */
+/* Does shift_left operation for given variables.  */
 
 void
-State::do_shift_left (tree * arg1, tree * arg2, tree * dest)
+State::do_shift_left (tree arg1, tree arg2, tree dest)
 {
   gcc_assert (!(is_declared (arg1) || is_declared (arg2)
 		|| is_declared (dest)));
@@ -355,16 +341,17 @@ State::do_shift_left (tree * arg1, tree * arg2, tree * dest)
 }
 
 
-/* Does SHIFT_RIGHT operation for given variables.  */
+/* Does shift_right operation for given variables.  */
 
 void
-State::do_shift_right (tree * arg1, tree * arg2, tree * dest)
+State::do_shift_right (tree arg1, tree arg2, tree dest)
 {
   gcc_assert (!(is_declared (arg1) || is_declared (arg2)
 		|| is_declared (dest)));
   gcc_assert (get_var_size (arg1) == get_var_size (dest)
 	      && get_var_size (arg2) == get_var_size (dest));
 
+  /* TODO: Add support for signed var shift.  */
   if (is_bit_vector (var_states.get (arg2)))
   {
     size_t shift_value = get_value (var_states.get (arg2));
@@ -384,7 +371,7 @@ State::do_shift_right (tree * arg1, tree * arg2, tree * dest)
 /* Adds two variables.  */
 
 void
-State::do_add (tree *arg1, tree *arg2, tree *dest)
+State::do_add (tree arg1, tree arg2, tree dest)
 {
   gcc_assert (!(is_declared (arg1) || is_declared (arg2)
 		|| is_declared (dest)));
@@ -405,7 +392,7 @@ State::do_add (tree *arg1, tree *arg2, tree *dest)
 /* Does subtraction.  */
 
 void
-State::do_sub (tree *arg1, tree *arg2, tree *dest)
+State::do_sub (tree arg1, tree arg2, tree dest)
 {
   gcc_assert (!(is_declared (arg1) || is_declared (arg2)
 		|| is_declared (dest)));
@@ -425,7 +412,7 @@ State::do_sub (tree *arg1, tree *arg2, tree *dest)
 /* Negates given variable.  */
 
 void
-State::do_complement (tree *arg, tree *dest)
+State::do_complement (tree arg, tree dest)
 {
   gcc_assert (!(is_declared (arg) || is_declared (dest)));
   gcc_assert (get_var_size (arg) == get_var_size (dest));
@@ -447,16 +434,16 @@ State::do_complement (tree *arg, tree *dest)
 }
 
 
-/* performs NOT operation for constant bit.  */
+/* Performs NOT operation for constant bit.  */
 
 bit *
 State::complement_const_bit (const bit * const_bit) const
 {
-  return new bit (1u - const_bit->get_val ());
+  return new bit (1u ^ const_bit->get_val ());
 }
 
 
-/* performs NOT operation for symbolic_bit.  */
+/* Performs NOT operation for symbolic_bit.  */
 
 value *
 State::complement_sym_bit (const value * var) const
@@ -465,7 +452,7 @@ State::complement_sym_bit (const value * var) const
 }
 
 
-/* performs XOR operation for 2 symbolic_bit operands.  */
+/* Performs XOR operation for 2 symbolic_bit operands.  */
 
 value *
 State::xor_sym_bits (const value * var1, const value * var2) const
@@ -480,27 +467,30 @@ State::xor_sym_bits (const value * var1, const value * var2) const
     bit_expression * var1_node_with_const_child
 	= get_parent_with_const_child (var1_copy);
 
+    /* If both subtrees have constant bit nodes, we can merge them together.  */
     if (var1_node_with_const_child != nullptr)
     {
+      /* If var1's const bit is in its left subtree.  */
       value * var1_left = var1_node_with_const_child->get_left ();
-      if (var1_left != nullptr && dyn_cast<bit *> (var1_left) != nullptr)
+      if (var1_left != nullptr && is_a<bit *> (var1_left))
       {
+	/* If var2's const bit is in its left subtree.  */
 	value * var2_left = var2_node_with_const_child->get_left ();
-	if (var2_left != nullptr && dyn_cast<bit *> (var2_left) != nullptr)
+	if (var2_left != nullptr && is_a<bit *> (var2_left))
 	{
-	  bit * new_left = xor_const_bits (dyn_cast<bit *> (var1_left),
-					   dyn_cast<bit *> (var2_left));
+	  bit * new_left = xor_const_bits (as_a<bit *> (var1_left),
+					   as_a<bit *> (var2_left));
 	  delete var2_left;
 	  var2_node_with_const_child->set_left (nullptr);
 
 	  delete var1_left;
 	  var1_node_with_const_child->set_left (new_left);
 	}
-	else
+	else /* Var2's const bit is in its right subtree.  */
 	{
 	  value * var2_right = var2_node_with_const_child->get_right ();
-	  bit * new_left = xor_const_bits (dyn_cast<bit *> (var1_left),
-					   dyn_cast<bit *> (var2_right));
+	  bit * new_left = xor_const_bits (as_a<bit *> (var1_left),
+					   as_a<bit *> (var2_right));
 	  delete var2_right;
 	  var2_node_with_const_child->set_right (nullptr);
 
@@ -509,25 +499,26 @@ State::xor_sym_bits (const value * var1, const value * var2) const
 	}
       }
 
-      else
+      else /* Var1's const bit is in its right subtree.  */
       {
 	value * var1_right = var1_node_with_const_child->get_right ();
 	value * var2_left = var2_node_with_const_child->get_left ();
-	if (var2_left != nullptr && dyn_cast<bit *> (var2_left) != nullptr)
+	/* If var2's const bit is in its left subtree.  */
+	if (var2_left != nullptr && is_a<bit *> (var2_left))
 	{
-	  bit * new_right = xor_const_bits (dyn_cast<bit *> (var1_left),
-					    dyn_cast<bit *> (var2_left));
+	  bit * new_right = xor_const_bits (as_a<bit *> (var1_left),
+					    as_a<bit *> (var2_left));
 	  delete var2_left;
 	  var2_node_with_const_child->set_left (nullptr);
 
 	  delete var1_right;
 	  var1_node_with_const_child->set_right (new_right);
 	}
-	else
+	else /* Var2's const bit is in its right subtree.  */
 	{
 	  value * var2_right = var2_node_with_const_child->get_right ();
-	  bit * new_right = xor_const_bits (dyn_cast<bit *> (var1_right),
-					    dyn_cast<bit *> (var2_right));
+	  bit * new_right = xor_const_bits (as_a<bit *> (var1_right),
+					    as_a<bit *> (var2_right));
 	  delete var2_right;
 	  var2_node_with_const_child->set_right (nullptr);
 
@@ -546,7 +537,7 @@ State::xor_sym_bits (const value * var1, const value * var2) const
 }
 
 
-/* performs XOR operation for 2 constant bit operands.  */
+/* Performs XOR operation for 2 constant bit operands.  */
 
 bit *
 State::xor_const_bits (const bit * const_bit1, const bit * const_bit2) const
@@ -555,7 +546,7 @@ State::xor_const_bits (const bit * const_bit1, const bit * const_bit2) const
 }
 
 
-/* performs XOR operation for a symbolic_bit and const_bit operands.  */
+/* Performs XOR operation for a symbolic_bit and const_bit operands.  */
 
 value *
 State::xor_var_const (const value * var, const bit * const_bit) const
@@ -566,16 +557,16 @@ State::xor_var_const (const value * var, const bit * const_bit) const
   if (node_with_const_child != nullptr)
   {
     value * left = node_with_const_child->get_left ();
-    if (left != nullptr && dyn_cast<bit *> (left) != nullptr)
+    if (left != nullptr && is_a<bit *> (left))
     {
-      bit * new_left = xor_const_bits (dyn_cast<bit *> (left), const_bit);
+      bit * new_left = xor_const_bits (as_a<bit *> (left), const_bit);
       delete left;
       node_with_const_child->set_left (new_left);
     }
     else
     {
       value * right = node_with_const_child->get_right ();
-      bit * new_right = xor_const_bits (dyn_cast<bit *> (right), const_bit);
+      bit * new_right = xor_const_bits (as_a<bit *> (right), const_bit);
       delete right;
       node_with_const_child->set_right (new_right);
     }
@@ -593,14 +584,15 @@ State::xor_var_const (const value * var, const bit * const_bit) const
 bit_expression *
 State::get_parent_with_const_child (value* root) const
 {
-  const bit_expression * expr = dyn_cast<const bit_expression *> (root);
-  if (expr == nullptr)
+  if (! is_a<bit_expression *> (root))
     return nullptr;
 
-  bit_expression* expr_root = dyn_cast<bit_expression *> (expr->copy ());
+  bit_expression* expr_root = as_a<bit_expression *> (root->copy ());
   hash_set<bit_expression *> nodes_to_consider;
   nodes_to_consider.add (expr_root);
 
+  /* Traversing expression tree:
+     considering only comutative expression nodes.  */
   while (!nodes_to_consider.is_empty ())
   {
     bit_expression* cur_element = *nodes_to_consider.begin ();
@@ -609,52 +601,50 @@ State::get_parent_with_const_child (value* root) const
     value* left = cur_element->get_left ();
     value* right = cur_element->get_right ();
 
-    if ((left != nullptr && dyn_cast<bit *> (left) != nullptr)
-	|| (right != nullptr && dyn_cast<bit *> (right) != nullptr))
+    if ((left != nullptr && is_a<bit *> (left))
+	|| (right != nullptr && is_a<bit *> (right)))
       return cur_element;
 
     if (left != nullptr && is_safe_branching (left))
-      nodes_to_consider.add (dyn_cast<bit_expression *> (left));
+      nodes_to_consider.add (as_a<bit_expression *> (left));
 
     if (right != nullptr && is_safe_branching (right))
-      nodes_to_consider.add (dyn_cast<bit_expression *> (right));
+      nodes_to_consider.add (as_a<bit_expression *> (right));
   }
+  return nullptr;
 }
 
 
-/* Checks if node is AND, OR or XOR expression.  */
+/* Checks if node is AND, OR or XOR expression as they are comutative.  */
 
 bool
 State::is_safe_branching (value* node) const
 {
-  return dyn_cast<bit_and_expression *> (node) != nullptr
-	 || dyn_cast<bit_or_expression *> (node) != nullptr
-	 || dyn_cast<bit_xor_expression *> (node) != nullptr;
+  return is_a<bit_and_expression *> (node) || is_a<bit_or_expression *> (node)
+	 || is_a<bit_xor_expression *> (node);
 }
 
 
-/* Shifts value_vector right by shift_value bits.  */
+/* Shifts value_vector left by shift_value bits.  */
 
 vec <value *>
-State::shift_right_by_const (const vec < value * > * value_vector,
-			     size_t shift_value)
+State::shift_left_by_const (const vec < value * > * value_vector,
+			    size_t shift_value)
 {
   vec <value *> shift_result;
   shift_result.create (value_vector->length ());
   if (shift_result.length () <= shift_value)
     for (size_t i = 0; i < shift_result.length (); i++)
-      {
 	shift_result[i] = new bit (0);
-      }
   else
-    {
-      size_t i = 0;
-      for ( ; i < shift_result.length () - shift_value; ++i)
-	shift_result[i] = new bit (0);
+  {
+    size_t i = 0;
+    for ( ; i < shift_result.length () - shift_value; ++i)
+      shift_result[i] = new bit (0);
 
-      for (size_t j = 0; i < shift_result.length (); ++i, ++j)
-	shift_result[i] = ((*value_vector)[j])->copy ();
-    }
+    for (size_t j = 0; i < shift_result.length (); ++i, ++j)
+      shift_result[i] = ((*value_vector)[j])->copy ();
+  }
   return shift_result;
 }
 
@@ -662,15 +652,225 @@ State::shift_right_by_const (const vec < value * > * value_vector,
 /* shift_right operation.  Case: var2 is a sym_bit.  */
 
 void
-State::shift_right_sym_bits (tree * var1, tree * var2, tree * dest)
+State::shift_right_sym_bits (tree var1, tree var2, tree dest)
 {
   for (size_t i = 0; i < get_var_size (dest); i++)
+  {
+    value * var1_elem = (*var_states.get (var1))[i];
+    value * var2_elem = (*var_states.get (var2))[i];
+    value * new_elem = new shift_right_expression (var1_elem->copy (),
+						   var2_elem->copy ());
+    delete (*var_states.get (dest))[i];
+    (*var_states.get (dest))[i] = new_elem;
+  }
+}
+
+
+bool
+State::check_const_bit_equality (vec<value *> * arg1_bits,
+				 vec<value *> * arg2_bits) const
+{
+  for (size_t i = 1; i < arg1_bits->length (); i++)
+    if ((*arg1_bits)[i] != (*arg2_bits)[i])
+      return false;
+  return true;
+}
+
+
+void
+State::add_equal_cond (tree arg1, tree arg2)
+{
+  vec<value *> * arg1_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg1);
+
+  if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
+  {
+    bool result = check_const_bit_equality (arg1_bits, arg2_bits);
+    conditions.add (new bit_condition (nullptr, nullptr,
+				       result ? condition_type::IS_TRUE
+						: condition_type::IS_FALSE));
+    return;
+  }
+  else if (is_bit_vector (arg1_bits) && TREE_CODE (arg2) == INTEGER_CST
+	   && (integer_onep (arg2) || integer_zerop (arg2)))
+  {
+    size_t i = 0;
+    if (integer_onep (arg2))
     {
-      value * var1_elem = (*var_states.get (var1))[i];
-      value * var2_elem = (*var_states.get (var2))[i];
-      value * new_elem = new shift_right_expression (var1_elem->copy (),
-						     var2_elem->copy ());
-      delete (*var_states.get (dest))[i];
-      (*var_states.get (dest))[i] = new_elem;
+      conditions.add (new bit_condition ((*arg1_bits)[0]->copy (), new bit (1),
+					 condition_type::EQUAL));
+      i++;
     }
+
+    for ( ; i < arg1_bits->length (); i++)
+      conditions.add (new bit_condition ((*arg1_bits)[i]->copy (), new bit (0),
+					 condition_type::EQUAL));
+  }
+
+  for (size_t i = 0; i < arg1_bits->length (); i++)
+  {
+    conditions.add (new bit_condition ((*arg1_bits)[i]->copy (),
+				       (*arg2_bits)[i]->copy (),
+				       condition_type::EQUAL));
+  }
+}
+
+
+bool
+State::check_const_bit_are_not_equal (vec<value *> * arg1_bits,
+				      vec<value *> * arg2_bits) const
+{
+  for (size_t i = 0; i < arg1_bits->length (); i++)
+    if ((*arg1_bits)[i] != (*arg2_bits)[i])
+      return true;
+  return false;
+}
+
+
+void
+State::add_not_equal_cond (tree arg1, tree arg2)
+{
+  vec<value *> * arg1_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg1);
+
+  if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
+  {
+    bool result = check_const_bit_are_not_equal (arg1_bits, arg2_bits);
+    conditions.add (new bit_condition (nullptr, nullptr,
+				       result ? condition_type::IS_TRUE
+						: condition_type::IS_FALSE));
+    return;
+  }
+
+  /* TODO: add condition when one of arguments is symbolic.  */
+}
+
+
+bool
+State::check_const_bit_is_greater_than (vec<value *> * arg1_bits,
+					vec<value *> * arg2_bits) const
+{
+  for (int i = arg1_bits->length () - 1; i >= 0; i--)
+  {
+    if ((*arg1_bits)[i] > (*arg2_bits)[i])
+      return true;
+    else if ((*arg1_bits)[i] < (*arg2_bits)[i])
+      return false;
+  }
+  return false;
+}
+
+
+void
+State::add_greater_than_cond (tree arg1, tree arg2)
+{
+  vec<value *> * arg1_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg1);
+
+  if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
+  {
+    bool result = check_const_bit_is_greater_than (arg1_bits, arg2_bits);
+    conditions.add (new bit_condition (nullptr, nullptr,
+				       result ? condition_type::IS_TRUE
+						: condition_type::IS_FALSE));
+    return;
+  }
+
+  /* TODO: add condition when one of arguments is symbolic.  */
+}
+
+
+bool
+State::check_const_bit_is_less_than (vec<value *> * arg1_bits,
+				     vec<value *> * arg2_bits) const
+{
+  for (int i = arg1_bits->length () - 1; i >= 0; i--)
+  {
+    if ((*arg1_bits)[i] < (*arg2_bits)[i])
+      return true;
+    else if ((*arg1_bits)[i] > (*arg2_bits)[i])
+      return false;
+  }
+  return false;
+}
+
+
+void
+State::add_less_than_cond (tree arg1, tree arg2)
+{
+  vec<value *> * arg1_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg1);
+
+  if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
+  {
+    bool result = check_const_bit_is_less_than (arg1_bits, arg2_bits);
+    conditions.add (new bit_condition (nullptr, nullptr,
+				       result ? condition_type::IS_TRUE
+						: condition_type::IS_FALSE));
+    return;
+  }
+
+  /* TODO: add condition when one of arguments is symbolic.  */
 }
+
+
+void
+State::add_greater_or_equal_cond (tree arg1, tree arg2)
+{
+  vec<value *> * arg1_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg1);
+
+  if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
+  {
+    bool is_greater_than = check_const_bit_is_greater_than (arg1_bits,
+							    arg2_bits);
+    bool is_equal = check_const_bit_equality (arg1_bits, arg2_bits);
+    conditions.add (new bit_condition (nullptr, nullptr,
+				       (is_greater_than | is_equal)
+				       ? condition_type::IS_TRUE
+					 : condition_type::IS_FALSE));
+    return;
+  }
+
+  /* TODO: add condition when one of arguments is symbolic.  */
+}
+
+
+void
+State::add_less_or_equal_cond (tree arg1, tree arg2)
+{
+  vec<value *> * arg1_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg1);
+
+  if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
+  {
+    bool is_less_than = check_const_bit_is_less_than (arg1_bits, arg2_bits);
+    bool is_equal = check_const_bit_equality (arg1_bits, arg2_bits);
+    conditions.add (new bit_condition (nullptr, nullptr,
+				       (is_less_than | is_equal)
+				       ? condition_type::IS_TRUE
+					 : condition_type::IS_FALSE));
+    return;
+  }
+
+  /* TODO: add condition when one of arguments is symbolic.  */
+}
+
+void
+State::add_bool_cond (tree arg)
+{
+  vec<value *> * arg_bits = var_states.get (arg);
+  condition_type result = condition_type::IS_FALSE;
+  if (is_bit_vector (arg_bits))
+  {
+    for (size_t i = 0; i < arg_bits->length (); i++)
+      if ((*arg_bits)[i] != 0)
+      {
+	result = condition_type::IS_TRUE;
+	break;
+      }
+  }
+  conditions.add (new bit_condition (nullptr, nullptr, result));
+
+  /* TODO: add condition when one of arguments is symbolic.  */
+}
\ No newline at end of file
diff --git a/gcc/sym-exec/state.h b/gcc/sym-exec/state.h
index fd6d6d395dc..7959123e72b 100644
--- a/gcc/sym-exec/state.h
+++ b/gcc/sym-exec/state.h
@@ -6,7 +6,6 @@
 #ifndef SYM_EXEC_STATE_H
 #define SYM_EXEC_STATE_H
 
-#include "expression.h"
 #include "config.h"
 #include "system.h"
 #include "coretypes.h"
@@ -26,13 +25,17 @@
 #include "is-a.h"
 #include "vec.h"
 #include "hash-map.h"
+#include "hash-set.h"
+#include "expression.h"
 
 /* Stores states of variables' values on bit-level.  */
 
 class State {
  private:
   /* Here is stored values of bit of each variable.  */
-  hash_map<tree *, vec < value * >> var_states;
+  hash_map<tree, vec < value * >> var_states;
+
+  hash_set<bit_expression *> conditions;
 
   /* Performs AND operation for 2 symbolic_bit operands.  */
   value *and_sym_bits (const value * var1, const value * var2) const;
@@ -76,27 +79,27 @@ class State {
 
   /* Checks whether state for variable with specified name already
      exists or not.  */
-  bool is_declared (tree *var);
+  bool is_declared (tree var);
 
  public:
   /* Adds an empty state for the given variable.  */
-  bool decl_var (tree *name, unsigned size);
+  bool decl_var (tree name, unsigned size);
 
   /* Adds a variable with unknown value to state.  Such variables are
      represented as sequence of symbolic bits.  */
-  bool make_symbolic (tree *var, unsigned size);
+  bool make_symbolic (tree var, unsigned size);
 
   /* Returns size of the given variable.  */
-  unsigned get_var_size (tree *var);
+  unsigned get_var_size (tree var);
 
   /* Does bit-level XOR operation for given variables.  */
-  void do_xor (tree *arg1, tree *arg2, tree *dest);
+  void do_xor (tree arg1, tree arg2, tree dest);
 
   /* Does bit-level AND operation for given variables.  */
-  void do_and (tree *arg1, tree *arg2, tree *dest);
+  void do_and (tree arg1, tree arg2, tree dest);
 
   /* Does bit-level OR operation for given variables.  */
-  void do_or (tree *arg1, tree *arg2, tree *dest);
+  void do_or (tree arg1, tree arg2, tree dest);
 
   /* Shifts value_vector left by shift_value bits.  */
   vec <value *> shift_left_by_const (const vec <value *> * value_vector,
@@ -105,33 +108,59 @@ class State {
   /* Checks if all vector elements are const_bit_expressions.  */
   bool is_bit_vector (vec <value *> * value_vector);
 
-  /* returns the value of the number represented as a bit vector.  */
+  /* Returns the value of the number represented as a bit vector.  */
   size_t get_value (vec <value *> *  bit_vector);
 
   /* shift_left operation.  Case: var2 is a sym_bit.  */
-  void shift_left_sym_bits (tree * var1, tree * var2, tree * dest);
+  void shift_left_sym_bits (tree var1, tree var2, tree dest);
 
-  /* Does SHIFT_LEFT operation for given variables.  */
-  void do_shift_left (tree *arg1, tree *arg2, tree *dest);
+  /* Does shift_left operation for given variables.  */
+  void do_shift_left (tree arg1, tree arg2, tree dest);
 
   /* Shifts value_vector right by shift_value bits.  */
   vec <value *> shift_right_by_const (const vec <value *> * value_vector,
 				      size_t shift_value);
 
   /* shift_right operation.  Case: var2 is a sym_bit.  */
-  void shift_right_sym_bits (tree * var1, tree * var2, tree * dest);
+  void shift_right_sym_bits (tree var1, tree var2, tree dest);
 
-  /* Does SHIFT_RIGHT operation for given variables.  */
-  void do_shift_right (tree *arg1, tree *arg2, tree *dest);
+  /* Does shift_right operation for given variables.  */
+  void do_shift_right (tree arg1, tree arg2, tree dest);
 
   /* Adds two variables.  */
-  void do_add (tree *arg1, tree *arg2, tree *dest);
+  void do_add (tree arg1, tree arg2, tree dest);
 
   /* Does subtraction.  */
-  void do_sub (tree *arg1, tree *arg2, tree *dest);
+  void do_sub (tree arg1, tree arg2, tree dest);
 
   /* Negates given variable.  */
-  void do_complement (tree *arg, tree *dest);
+  void do_complement (tree arg, tree dest);
+
+  void add_equal_cond (tree arg1, tree arg2);
+
+  void add_not_equal_cond (tree arg1, tree arg2);
+
+  void add_greater_than_cond (tree arg1, tree arg2);
+
+  void add_less_than_cond (tree arg1, tree arg2);
+
+  void add_greater_or_equal_cond (tree arg1, tree arg2);
+
+  void add_less_or_equal_cond (tree arg1, tree arg2);
+
+  void add_bool_cond (tree arg);
+
+  bool check_const_bit_equality (vec<value *> * arg1_bits,
+				 vec<value *> * arg2_bits) const;
+
+  bool check_const_bit_are_not_equal (vec<value *> * arg1_bits,
+				      vec<value *> * arg2_bits) const;
+
+  bool check_const_bit_is_greater_than (vec<value *> * arg1_bits,
+					vec<value *> * arg2_bits) const;
+
+  bool check_const_bit_is_less_than (vec<value *> * arg1_bits,
+				     vec<value *> * arg2_bits) const;
 };
 
 #endif /* SYM_EXEC_STATE_H.  */