https://gcc.gnu.org/g:148e20466c2c246df9472efed0f2ae94cb65a0f8

commit r15-5848-g148e20466c2c246df9472efed0f2ae94cb65a0f8
Author: Matevos Mehrabyan <matevosmehrab...@gmail.com>
Date:   Mon Nov 11 13:00:10 2024 -0700

    [PATCH v6 09/12] Add symbolic execution support.
    
    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.
            * sym-exec/sym-exec-condition.cc: New file.
            * sym-exec/sym-exec-condition.h: New file.
            * sym-exec/sym-exec-expr-is-a-helper.h: New file.
            * sym-exec/sym-exec-expression.cc: New file.
            * sym-exec/sym-exec-expression.h: New file.
            * sym-exec/sym-exec-state.cc: New file.
            * sym-exec/sym-exec-state.h: New file.
    
            Co-authored-by: Mariam Arutunian <mariamarutun...@gmail.com>

Diff:
---
 gcc/Makefile.in                          |    3 +
 gcc/configure                            |    2 +-
 gcc/sym-exec/sym-exec-condition.cc       |   86 ++
 gcc/sym-exec/sym-exec-condition.h        |   63 +
 gcc/sym-exec/sym-exec-expr-is-a-helper.h |  287 ++++
 gcc/sym-exec/sym-exec-expression.cc      |  490 +++++++
 gcc/sym-exec/sym-exec-expression.h       |  332 +++++
 gcc/sym-exec/sym-exec-state.cc           | 2321 ++++++++++++++++++++++++++++++
 gcc/sym-exec/sym-exec-state.h            |  471 ++++++
 9 files changed, 4054 insertions(+), 1 deletion(-)

diff --git a/gcc/Makefile.in b/gcc/Makefile.in
index 4cfe383ba8a1..d250b4cb0a63 100644
--- a/gcc/Makefile.in
+++ b/gcc/Makefile.in
@@ -1731,6 +1731,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 bab4181a940f..d21b33e2b6c0 100755
--- a/gcc/configure
+++ b/gcc/configure
@@ -36295,7 +36295,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 000000000000..fef03d04d555
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-condition.cc
@@ -0,0 +1,86 @@
+/* Everything defined here is used for representing conditions for bits
+   and their status.
+   Copyright (C) 2022-2024 Free Software Foundation, Inc.
+   Contributed by Matevos Mehrabyan <matevosmehrab...@gmail.com>
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it under
+the terms of the GNU General Public License as published by the Free
+Software Foundation; either version 3, or (at your option) any later
+version.
+
+GCC is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.  */
+
+#include "sym-exec-condition.h"
+
+/* Constructor where the first argument is the bit left to the condition sign,
+   the second argument is the bit right to the condition sign and the third
+   argument is the code of the condition.  */
+
+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;
+}
+
+
+/* Copy constructor.  */
+
+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 000000000000..ee5b8703f484
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-condition.h
@@ -0,0 +1,63 @@
+/* Everything defined here is used for representing conditions for bits
+   and their status.
+   Copyright (C) 2022-2024 Free Software Foundation, Inc.
+   Contributed by Matevos Mehrabyan <matevosmehrab...@gmail.com>
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it under
+the terms of the GNU General Public License as published by the Free
+Software Foundation; either version 3, or (at your option) any later
+version.
+
+GCC is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.  */
+
+
+#ifndef SYM_EXEC_CONDITION_H
+#define SYM_EXEC_CONDITION_H
+
+#include "sym-exec-expression.h"
+
+/* Enum representing condition status.  */
+
+enum condition_status {
+  CS_NO_COND,
+  CS_TRUE,
+  CS_FALSE,
+  CS_SYM
+};
+
+/* Class used for describing and storing condition for a single bit.  */
+
+class bit_condition : public bit_expression {
+ private:
+  /* Condition's code.  */
+  tree_code m_code;
+
+  /* Prints the condition's sign.  */
+  void print_expr_sign ();
+
+ public:
+  /* Constructor where the first argument is the bit left to the condition 
sign,
+     the second argument is the bit right to the condition sign and the third
+     argument is the code of the condition.  */
+  bit_condition (value_bit *left, value_bit *right, tree_code type);
+
+  /* Copy constructor.  */
+  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 000000000000..1a262b47fad6
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-expr-is-a-helper.h
@@ -0,0 +1,287 @@
+/* Defining test functions for value conversion via dyn_cast.
+   Copyright (C) 2022-2024 Free Software Foundation, Inc.
+   Contributed by Matevos Mehrabyan <matevosmehrab...@gmail.com>
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it under
+the terms of the GNU General Public License as published by the Free
+Software Foundation; either version 3, or (at your option) any later
+version.
+
+GCC is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.  */
+
+
+#ifndef SYM_EXEC_EXPRESSION_IS_A_HELPER_H
+#define SYM_EXEC_EXPRESSION_IS_A_HELPER_H
+
+#include "sym-exec-condition.h"
+
+/* Test function used by dyn_cast checks if the value_bit is of
+   the value_type::SYMBOLIC_BIT type.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<symbolic_bit *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::SYMBOLIC_BIT;
+}
+
+
+/* Test function used by dyn_cast checks if the value_bit is of
+   the value_type::BIT type.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<bit *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT;
+}
+
+
+/* Test function used by dyn_cast checks if the value_bit
+   is a bit_expression.  */
+
+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;
+}
+
+
+/* Test function used by dyn_cast checks if the value_bit
+   is a bit_and_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_and_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT_AND_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the value_bit
+   is a bit_or_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_or_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT_OR_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the value_bit
+   is a bit_xor_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_xor_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT_XOR_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the value_bit
+   is a bit_complement_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_complement_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT_COMPLEMENT_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the value_bit
+   is a shift_left_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_left_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::SHIFT_LEFT_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the value_bit
+   is a shift_right_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_right_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::SHIFT_RIGHT_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the value_bit
+   is an add_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<add_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::ADD_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the value_bit
+   is a sub_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<sub_expression *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::SUB_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the value_bit
+   is a bit_condition.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_condition *>::test (value_bit *ptr)
+{
+  return ptr->get_type () == value_type::BIT_CONDITION;
+}
+
+
+/* Test function used by dyn_cast checks if the bit_expression
+   is a bit_and_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_and_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::BIT_AND_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the bit_expression
+   is a bit_or_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_or_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::BIT_OR_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the bit_expression
+   is a bit_xor_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_xor_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::BIT_XOR_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the bit_expression
+   is a bit_complement_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_complement_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::BIT_COMPLEMENT_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the bit_expression
+   is a shift_left_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_left_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::SHIFT_LEFT_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the bit_expression
+   is a shift_right_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_right_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::SHIFT_RIGHT_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the bit_expression
+   is a add_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<add_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::ADD_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the bit_expression
+   is a sub_expression.  */
+
+template<>
+template<>
+inline bool
+is_a_helper<sub_expression *>::test (bit_expression *ptr)
+{
+  return ptr->get_type () == value_type::SUB_EXPRESSION;
+}
+
+
+/* Test function used by dyn_cast checks if the bit_expression
+   is a bit_condition_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 000000000000..8abae6a993ff
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-expression.cc
@@ -0,0 +1,490 @@
+/* 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.
+   Copyright (C) 2022-2024 Free Software Foundation, Inc.
+   Contributed by Matevos Mehrabyan <matevosmehrab...@gmail.com>
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it under
+the terms of the GNU General Public License as published by the Free
+Software Foundation; either version 3, or (at your option) any later
+version.
+
+GCC is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.  */
+
+#include "sym-exec-expr-is-a-helper.h"
+
+/* Returns type of the bit.  */
+
+value_type
+value_bit::get_type () const
+{
+  return m_type;
+}
+
+
+/* Constructor that sets the bit's initial position and its origin.  */
+
+symbolic_bit::symbolic_bit (size_t i, tree orig)
+    : value_bit (i), m_origin (orig)
+{
+  m_type = SYMBOLIC_BIT;
+}
+
+
+/* Constructor that sets m_val to the specified value.  */
+
+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;
+}
+
+
+/* Constructor that sets the left and right side bits
+   of the bit_complement_expression sign.  */
+
+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;
+}
+
+
+/* Copy constructor for bit_complement_expression.  */
+
+bit_complement_expression::bit_complement_expression (
+  const bit_complement_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+/* Destructor for bit_expression.  */
+
+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);
+}
+
+
+/* Constructor that sets the left and right side bits
+   of the bit_xor_expression sign.  */
+
+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;
+}
+
+
+/* Copy constructor for bit_xor_expression.  */
+
+bit_xor_expression::bit_xor_expression (const bit_xor_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+/* Constructor that sets the left and right side bits
+   of the bit_and_expression sign.  */
+
+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;
+}
+
+
+/* Copy constructor for bit_and_expression.  */
+
+bit_and_expression::bit_and_expression (const bit_and_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+/* Constructor that sets the left and right side bits
+   of the bit_or_expression sign.  */
+
+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;
+}
+
+
+/* Copy constructor for bit_or_expression.  */
+
+bit_or_expression::bit_or_expression (const bit_or_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+/* Constructor that sets the left and right side bits
+   of the shift_right_expression sign.  */
+
+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;
+}
+
+
+/* Copy constructor for shift_right_expression.  */
+
+shift_right_expression::shift_right_expression (
+  const shift_right_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+/* Constructor that sets the left and right side bits
+   of the shift_left_expression sign.  */
+
+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;
+}
+
+
+/* Copy constructor for shift_left_expression.  */
+
+shift_left_expression::shift_left_expression (const shift_left_expression 
&expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+/* Constructor that sets the left and right side bits
+   of the add_expression sign.  */
+
+add_expression::add_expression (value_bit *left, value_bit *right)
+{
+  this->m_left = left;
+  this->m_right = right;
+  m_type = ADD_EXPRESSION;
+}
+
+
+/* Copy constructor for add_expression.  */
+
+add_expression::add_expression (const add_expression &expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+/* Constructor that sets the left and right side bits
+   of the sub_expression sign.  */
+
+sub_expression::sub_expression (value_bit *left, value_bit *right)
+{
+  this->m_left = left;
+  this->m_right = right;
+  m_type = SUB_EXPRESSION;
+}
+
+
+/* Copy constructor for 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 000000000000..610088c9637a
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-expression.h
@@ -0,0 +1,332 @@
+/* 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.
+   Copyright (C) 2022-2024 Free Software Foundation, Inc.
+   Contributed by Matevos Mehrabyan <matevosmehrab...@gmail.com>
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it under
+the terms of the GNU General Public License as published by the Free
+Software Foundation; either version 3, or (at your option) any later
+version.
+
+GCC is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.  */
+
+#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:
+
+  /* Default constructor.  Sets m_index 0.  */
+  value_bit () : m_index (0)
+  {};
+
+  /* Constructor that sets m_index to the specified value.  */
+  value_bit (size_t i) : m_index (i)
+  {};
+
+  /* Copy constructor for value_bit.  */
+  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;
+
+  /* Destructor.  */
+  virtual ~value_bit () = default;
+};
+
+
+/* Represents value of a single bit of symbolic marked variables.  */
+
+class symbolic_bit : public value_bit {
+  /* The Origin of the bit.  */
+  tree m_origin = nullptr;
+
+ public:
+  /* Constructor that sets the bit's initial position and its origin.  */
+  symbolic_bit (size_t i, tree orig);
+
+  /* Copy constructor for symbolic_bit.  */
+  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:
+  /* Constructor that sets m_val to the specified value.  */
+  bit (unsigned char i);
+
+  /* Copy constructor for bit.  */
+  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:
+  /* The bit left to the expression sign.  */
+  value_bit *m_left = nullptr;
+
+  /* The bit right to the expression sign.  */
+  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 ();
+
+  /* Destructor for bit_expression.  */
+  ~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:
+  /* Constructor that sets the left and right side bits
+     of the bit_xor_expression sign.  */
+  bit_xor_expression (value_bit *left, value_bit *right);
+
+  /* Copy constructor for bit_xor_expression.  */
+  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:
+  /* Constructor that sets the left and right side bits
+     of the bit_and_expression sign.  */
+  bit_and_expression (value_bit *left, value_bit *right);
+
+  /* Copy constructor for bit_and_expression.  */
+  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:
+  /* Constructor that sets the left and right side bits
+     of the bit_or_expression sign.  */
+  bit_or_expression (value_bit *left, value_bit *right);
+
+  /* Copy constructor for bit_or_expression.  */
+  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:
+  /* Constructor that sets the left and right side bits
+     of the shift_right_expression sign.  */
+  shift_right_expression (value_bit *left, value_bit *right);
+
+  /* Copy constructor for shift_right_expression.  */
+  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:
+  /* Constructor that sets the left and right side bits
+     of the shift_left_expression sign.  */
+  shift_left_expression (value_bit *left, value_bit *right);
+
+  /* Copy constructor for shift_left_expression.  */
+  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:
+  /* Constructor that sets the left and right side bits
+     of the add_expression sign.  */
+  add_expression (value_bit *left, value_bit *right);
+
+  /* Copy constructor for add_expression.  */
+  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:
+  /* Constructor that sets the left and right side bits
+     of the sub_expression sign.  */
+  sub_expression (value_bit *left, value_bit *right);
+
+  /* Copy constructor for sub_expression.  */
+  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:
+  /* Constructor that sets the left and right side bits
+     of the bit_complement_expression sign.  */
+  bit_complement_expression (value_bit *right);
+
+  /* Copy constructor for bit_complement_expression.  */
+  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 000000000000..85e6093c362e
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-state.cc
@@ -0,0 +1,2321 @@
+/* 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.
+   Copyright (C) 2022-2024 Free Software Foundation, Inc.
+   Contributed by Matevos Mehrabyan <matevosmehrab...@gmail.com>
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it under
+the terms of the GNU General Public License as published by the Free
+Software Foundation; either version 3, or (at your option) any later
+version.
+
+GCC is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.  */
+
+/* This symbolic executor is designed to handle operations on the bit level.
+   It can save values of variables on the bit level.  For example byte x = 9
+   would be represented by the bit-vector x = <0, 0, 0, 0, 1, 0, 1, 0> of
+   size 8.  Variables without values will be represented by bit-vectors of
+   symbolic bits: x = <x[size - 1], ..., x[1], x[0]> where x[i] is the value
+   of bit i of variable x.
+
+   Operations are also performed on the bit level.  For example, for operation
+   z = x & y
+   where
+   x = <x[size - 1], ..., x[1], x[0]>
+   y = <y[size - 1], ..., y[1], y[0]>
+   z will have the value
+   z = <x[size - 1] & y[size - 1], ..., x[1] & y[1], x[0] & y[0]>
+
+   Each bit of variable can be accessed and examined separately if needed.
+   Moreover, it does basic optimizations in place.
+   For example, for operation
+   z = x | y
+   where
+   x = <x[size - 1], ..., x[1], x[0]>,
+   y = <1, ..., 0, 1>,
+   z will have the value
+   z = <1, ..., x[1], 1>
+   as x | 0 == x and x | 1 == 1
+
+   Besides variables, the symbolic executor can also store
+   conditions on the bit level.
+   For example, for x == y
+   It would add {x[size - 1] == y[size - 1], ..., x[1] == y[1], x[0] == y[0]}
+   conditions.
+
+   For a more complex condition x > y, it would add
+   {x[size - 1] > y[size - 1] || (x[size - 1] == y[size -1]
+       && (x[size - 2] > y[size - 2] || (x[size - 2] == y[size - 2]
+               && ... (x[0] >= y[0])...)}
+
+   The symbolic executor doesn't run by itself.  Instead, it must be dictated
+   what to do.  This makes it flexible and allows for various pre- and
+   post-processing tasks.  Developers adding new operation support must 
consider
+   that the operation must be represented on the bit level.  Because of
+   this restriction, it may be hard to add support for some operations.
+
+   To use the symbolic executor, you must create a state object.  It is the 
main
+   object that contains variables as bit-vectors and conditions.
+   It is the state object that provides operations for symbolic execution.
+
+   If you are going to execute multiple execution paths, you should clone
+   the state at branching instructions and execute one state for the execution
+   path where the branching condition evaluates to 'true', and
+   the other state for the execution path where the branching condition
+   evaluates to 'false'.  Besides that, you should add the corresponding
+   conditions to states if you need them.
+
+   Variables are stored in the state's 'var_states' field.  It maps the tree
+   object of the variable to its bit-vector.  Path conditions are stored in
+   the 'conditions' field.
+
+   To declare a variable, you should use 'declare_if_needed' method of state.
+   It declares the variable if it was not previously declared.
+   'create_val_for_const' is used for constant declaration.
+
+   The list of supported operations can be found in 'state::do_operation'
+   method.  It calls the corresponding operation based on the specified
+   tree_code operation.  This is the method that you should use to dictate
+   to the symbolic executor what operations to perform.  You can execute the
+   desired operations explicitly if needed.  Variables for participant
+   operands will be created implicitly if it was not previously declared.
+   To add conditions to the state, you should use 'state::add_*_cond' methods.
+
+   A sample usage of the symbolic executor:
+
+   // Example.
+
+   unsigned char foo (unsigned char x, unsigned char y)
+   {
+     unsigned char D.2352;
+     unsigned char result;
+
+     result = x & y;
+     result = result | 9;
+     if (result == 23) goto <D.2350>; else goto <D.2351>;
+     <D.2350>:
+     result = result ^ y;
+     <D.2351>:
+     D.2352 = result;
+     return D.2352;
+   }
+
+   // Now, we create the initial state and add the variables to it.
+   state s;
+   s.declare_if_needed (x, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (x))));
+   s.declare_if_needed (y, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (y))));
+   s.declare_if_needed (d_2352, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (d_2352))));
+   s.declare_if_needed (result, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (result))));
+
+   s.do_operation (BIT_AND_EXPR, x, y, result);
+   s.do_operation (BIT_OR_EXPR, result, 9, result);
+
+   state s2 (s);  // We duplicate the state to save values for each branch.
+   s.add_equal_cond (result, 23);
+   s2.add_not_equal_cond (result, 23);
+
+   s.do_operation (BIT_XOR_EXPR, result, y, result);
+   s.do_assign (result, d_2352);
+   s2.do_assign (result, d_2352);
+
+   // Now, we have variable values for each execution branch, and we can 
examine
+   // them to make decisions.
+
+   value * res = s.get_value (result);
+   if (is_a<bit_expression *> ((*res)[0]))
+   {
+     bit_expression * expr = is_a<bit_expression *> ((*res)[0]);
+     if (is_a<bit *> (expr->get_left ())
+        && as_a<bit *> (expr->get_left ())->get_val () == 0)
+     {
+       ... // Do something.
+     }
+   }
+
+   A more general usage would be to iterate over instructions and
+   call the executor:
+
+   state s;
+   ...
+
+   for (inst : instructions)
+   {
+     enum tree_code rhs_code = gimple_assign_rhs_code (inst);
+     tree op1 = gimple_assign_rhs1 (gs);
+     tree op2 = gimple_assign_rhs2 (gs);
+     tree lhs = gimple_assign_lhs (gs);
+     s.do_operation (rhs_code, op1, op2, lhs);
+     ...
+   }
+
+   */
+
+#include "sym-exec-state.h"
+
+/* Returns the minimum of A, B, C.  */
+
+size_t min (size_t a, size_t b, size_t c)
+{
+  size_t min = (a < b ? a : b);
+  return min < c ? min : c;
+}
+
+
+/* Copy constructor for state.  It copies all variables and conditions
+   of the given state.  */
+
+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 ()));
+}
+
+
+/* Destructor for state.  */
+
+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;
+    }
+
+}
+
+
+/* Multiplies given values.  The result is stored in dest.  */
+
+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;
+}
+
+
+/* Constructor for value.  The first argument is the size of the bit-vector
+   and the second argument is the sign of the number.  */
+
+value::value (unsigned size, bool is_unsigned) : is_unsigned (is_unsigned)
+{
+  number.create (size);
+}
+
+
+/* Copy constructor for value.  */
+
+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);
+}
+
+
+/* Destructor for value.  */
+
+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 000000000000..e9e68b6478a5
--- /dev/null
+++ b/gcc/sym-exec/sym-exec-state.h
@@ -0,0 +1,471 @@
+/* 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.
+   Copyright (C) 2022-2024 Free Software Foundation, Inc.
+   Contributed by Matevos Mehrabyan <matevosmehrab...@gmail.com>
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it under
+the terms of the GNU General Public License as published by the Free
+Software Foundation; either version 3, or (at your option) any later
+version.
+
+GCC is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.  */
+
+
+#ifndef SYM_EXEC_STATE_H
+#define SYM_EXEC_STATE_H
+
+#define MAX_VALUE_SIZE 64
+
+#include "sym-exec-expr-is-a-helper.h"
+
+/* Struct used for representing values.  */
+
+struct value {
+ private:
+  /* bit-vector that represents the value.  */
+  vec<value_bit *> number;
+
+ public:
+  /* Used for denoting whether the number is unsigned.  */
+  const bool is_unsigned;
+
+  /* Constructor for value.  The first argument is the size of the bit-vector
+     and the second argument is the sign of the number.  */
+  value (unsigned size, bool is_unsigned);
+
+  /* Copy constructor for value.  */
+  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;
+
+  /* Destructor for value.  */
+  ~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:
+  /* Default constructor for state.  */
+  state () = default;
+
+  /* Destructor for state.  */
+  ~state ();
+
+  /* Adds an empty state for the given variable.  */
+  bool decl_var (tree name, unsigned size);
+
+  /* Copy constructor for state.  It copies all variables and conditions
+     of the given state.  */
+  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 ();
+};
+
+
+/* Returns the minimum of A, B, C.  */
+
+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.  */

Reply via email to