symb_exec v1: - Added gcc/sym-exec/expression.h/.cc and gcc/sym-exec/state.h/cc. State is for keeping functionvariables' states on a path. Expression file contains classes for keeping values.

6 files changed, 1178 insertions, 1 deletions

diff --git a/gcc/Makefile.in b/gcc/Makefile.in
index c9bce29..48043b0 100644
--- a/gcc/Makefile.in
+++ b/gcc/Makefile.in
@@ -1648,6 +1648,8 @@ OBJS = \
 	tree-logical-location.o \
 	tree-loop-distribution.o \
 	gimple-crc-optimization.o \
+	sym-exec/expression.o \
+	sym-exec/state.o \
 	tree-nested.o \
 	tree-nrv.o \
 	tree-object-size.o \
diff --git a/gcc/configure b/gcc/configure
index 254f9b6..0389a39 100755
--- a/gcc/configure
+++ b/gcc/configure
@@ -33932,7 +33932,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 rtl-ssa
+  for lang in $subdirs c-family common analyzer rtl-ssa sym-exec
   do
       ${CONFIG_SHELL-/bin/sh} $ac_aux_dir/mkinstalldirs $lang/$DEPDIR
   done ;;
diff --git a/gcc/sym-exec/expression.cc b/gcc/sym-exec/expression.cc
new file mode 100644
index 0000000..e2aad4b
--- /dev/null
+++ b/gcc/sym-exec/expression.cc
@@ -0,0 +1,168 @@
+/* Every class defined here represents a single bit value of a variable.
+   Every variable will be represented as a vector of these classes which later
+   will be used for bit-level symbolic execution.  */
+
+#include "stddef.h"
+#include "expression.h"
+
+
+bit_expression::bit_expression (value* left, value* right)
+{
+  this->left = left;
+  this->right = right;
+}
+
+
+value *
+bit_expression::get_left ()
+{
+  return left;
+}
+
+
+value *
+bit_expression::get_right ()
+{
+  return right;
+}
+
+
+void
+bit_expression::set_left (value *expr)
+{
+  left = expr;
+}
+
+
+void
+bit_expression::set_right (value *expr)
+{
+  right = expr;
+}
+
+
+size_t
+value::get_index () const
+{
+  return index;
+}
+
+
+unsigned char
+bit::get_val () const
+{
+  return val;
+}
+
+
+void
+bit::set_val (unsigned char new_val)
+{
+  val = new_val;
+}
+
+
+bit_complement_expression::bit_complement_expression (value *right) :
+  bit_expression (nullptr, right)
+{}
+
+
+value*
+symbolic_bit::copy () const
+{
+  return new symbolic_bit (*this);
+}
+
+
+value *
+bit::copy () const
+{
+  return new bit (*this);
+}
+
+
+bit_expression::bit_expression (const bit_expression &expr)
+{
+  if (expr.left)
+    {
+      left = expr.left->copy ();
+    }
+
+  if (expr.right)
+    {
+      right = expr.right->copy ();
+    }
+}
+
+
+value *
+bit_expression::copy () const
+{
+  return new bit_expression (*this);
+}
+
+
+value *
+bit_xor_expression::copy () const
+{
+  return bit_expression::copy ();
+}
+
+
+value *
+bit_and_expression::copy () const
+{
+  return bit_expression::copy ();
+}
+
+
+value *
+bit_or_expression::copy () const
+{
+  return bit_expression::copy ();
+}
+
+
+value *
+shift_right_expression::copy () const
+{
+  return bit_expression::copy ();
+}
+
+
+value *
+shift_left_expression::copy () const
+{
+  return bit_expression::copy ();
+}
+
+
+value *
+add_expression::copy () const
+{
+  return bit_expression::copy ();
+}
+
+
+value *
+sub_expression::copy () const
+{
+  return bit_expression::copy ();
+}
+
+
+value *
+bit_complement_expression::copy () const
+{
+  return bit_expression::copy ();
+}
+
+
+bit_expression::~bit_expression ()
+{
+  delete left;
+  left = nullptr;
+
+  delete right;
+  right = nullptr;
+}
diff --git a/gcc/sym-exec/expression.h b/gcc/sym-exec/expression.h
new file mode 100644
index 0000000..0cb7a6c
--- /dev/null
+++ b/gcc/sym-exec/expression.h
@@ -0,0 +1,194 @@
+/* Every class defined here represents a single bit value of a variable.
+   Every variable will be represented as a vector of these classes which later
+   will be used for bit-level symbolic execution.  */
+
+#ifndef SYM_EXEC_EXPRESSION_H
+#define SYM_EXEC_EXPRESSION_H
+
+#include "stddef.h"
+
+/* Base class for single bit value.  */
+
+class value {
+ protected:
+  /* This will help us to understand where is moved the bit
+     from its initial position.  */
+  const size_t index;
+
+ public:
+  value () : index (0)
+  {};
+  value (size_t i) : index (i)
+  {};
+  value (value &val) : index (val.index)
+  {};
+  size_t get_index () const;
+
+  /* This will support deep copy of objects' values.  */
+  virtual value *copy () const = 0;
+  virtual ~value ()
+  {};
+};
+
+
+/* Represents value of a single bit of symbolic marked variables.  */
+
+class symbolic_bit : public value {
+ public:
+  symbolic_bit (size_t i) : value (i)
+  {};
+  symbolic_bit (const symbolic_bit &sym_bit) : symbolic_bit (sym_bit.index)
+  {};
+
+  value *copy () const;
+};
+
+
+/* Represents value of a single bit.  */
+
+class bit : public value {
+ private:
+  /* This is the value of a bit.  It must be either 1 or 0.  */
+  unsigned char val = 0;
+
+ public:
+  bit (unsigned char i) : val (i)
+  {};
+  bit (const bit &b) : bit (b.val)
+  {};
+  unsigned char get_val () const;
+  void set_val (unsigned char new_val);
+  value *copy () const;
+};
+
+
+/* Bit-level base expression class.  In general expressions consist of
+   two operands.  Here we named them left and right.  */
+
+class bit_expression : public value {
+ protected:
+  value *left = nullptr;
+  value *right = nullptr;
+
+ public:
+  bit_expression () : left (nullptr), right (nullptr)
+  {};
+  bit_expression (value *left, value *right);
+
+  bit_expression (const bit_expression &expr);
+
+  value *get_left ();
+  value *get_right ();
+
+  void set_left (value *expr);
+  void set_right (value *expr);
+  value *copy () const;
+  virtual ~bit_expression ();
+};
+
+
+/* Bit-level XOR expression.  XOR operation on two variables (when one of
+   them is symbolic) can be represented by XOR operations on
+   each of their bits.  */
+
+class bit_xor_expression : public bit_expression {
+ public:
+  bit_xor_expression (value *left, value *right) : bit_expression (left, right)
+  {};
+  bit_xor_expression (const bit_xor_expression &expr) : bit_expression (expr)
+  {};
+  value *copy () const;
+};
+
+
+/* Bit-level AND expression.  AND operation on two variables (when one of
+   them is symbolic) can be represented by AND operations on
+   each of their bits.  */
+
+class bit_and_expression : public bit_expression {
+ public:
+  bit_and_expression (value *left, value *right) : bit_expression (left, right)
+  {};
+  bit_and_expression (const bit_and_expression &expr) : bit_expression (expr)
+  {};
+  value *copy () const;
+};
+
+
+/* Bit-level OR expression.  OR operation on two variables (when one of
+   them is symbolic) can be represented by OR operations on
+   each of their bits.  */
+
+class bit_or_expression : public bit_expression {
+ public:
+  bit_or_expression (value *left, value *right) : bit_expression (left, right)
+  {};
+  bit_or_expression (bit_or_expression &expr) : bit_expression (expr)
+  {};
+  value *copy () const;
+};
+
+
+/* SHIFT_RIGHT expression.  Result must be stored bit by bit.  */
+
+class shift_right_expression : public bit_expression {
+ public:
+  shift_right_expression (value *left, value *right) : bit_expression (left,
+								       right)
+  {};
+  shift_right_expression (const shift_right_expression &expr)
+			 : bit_expression (expr)
+  {};
+  value *copy () const;
+};
+
+
+/* SHIFT_LEFT expression.  Result must be stored bit by bit.  */
+
+class shift_left_expression : public bit_expression {
+ public:
+  shift_left_expression (value *left, value *right) : bit_expression (left,
+								      right)
+  {};
+  shift_left_expression (const shift_left_expression &expr)
+			: bit_expression (expr)
+  {};
+  value *copy () const;
+};
+
+
+/* ADD expression.  Result must be stored bit by bit.  */
+
+class add_expression : public bit_expression {
+ public:
+  add_expression (value *left, value *right) : bit_expression (left, right)
+  {};
+  add_expression (const add_expression &expr) : bit_expression (expr)
+  {};
+  value *copy () const;
+};
+
+
+/* SUB expression.  Result must be stored bit by bit.  */
+
+class sub_expression : public bit_expression {
+ public:
+  sub_expression (value *left, value *right) : bit_expression (left, right)
+  {};
+  sub_expression (const sub_expression &expr) : bit_expression (expr)
+  {};
+  value *copy () const;
+};
+
+/* Bit-level negation expression.  */
+
+class bit_complement_expression : public bit_expression {
+ public:
+  bit_complement_expression (value *right);
+  bit_complement_expression (const bit_complement_expression &expr)
+  			    : bit_expression (expr)
+  {};
+  value *copy () const;
+};
+
+#endif /* SYM_EXEC_EXPRESSION_H.  */
diff --git a/gcc/sym-exec/state.cc b/gcc/sym-exec/state.cc
new file mode 100644
index 0000000..8081e30
--- /dev/null
+++ b/gcc/sym-exec/state.cc
@@ -0,0 +1,676 @@
+/* State will store states of variables for a function's single execution path.
+   It will be used for bit-level symbolic execution to determine values of bits
+   of function's return value and symbolic marked arguments.  */
+
+#include "stddef.h"
+#include "state.h"
+#include "vec.h"
+#include "hash-set.h"
+#include "expression.h"
+
+
+/* Checks whether state for variable with specified name already
+   exists or not.  */
+
+bool
+State::is_declared (tree *var)
+{
+  return var_states.get (var) != NULL;
+}
+
+
+/* performs AND operation for 2 symbolic_bit operands.  */
+
+value *
+State::and_sym_bits (const value * var1, const value * var2) const
+{
+  return new bit_and_expression (var1->copy (), var2->copy ());
+}
+
+/* performs AND operation for a symbolic_bit and const_bit operands.  */
+
+value *
+State::and_var_const (const value * var1, const bit * const_bit) const
+{
+  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) const
+{
+  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 *
+State::or_sym_bits (const value * var1, const value * var2) const
+{
+  return new bit_or_expression (var1->copy (), var2->copy ());
+}
+
+/* performs OR operation for a symbolic_bit and a constant bit operands.  */
+
+value *
+State::or_var_const (const value * var1, const bit * const_bit) const
+{
+  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) const
+{
+  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;
+
+  vec < value * > content;
+  content.create (size);
+  for (unsigned i = 0; i < size; i++)
+    content.quick_push (nullptr);
+
+  return var_states.put (var, content);
+}
+
+
+/* Returns size of the given variable.  */
+
+unsigned
+State::get_var_size (tree *var)
+{
+  vec < value * > *content = var_states.get (var);
+  if (content == NULL)
+    return 0;
+
+  return content->length ();
+}
+
+
+/* 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;
+
+  vec < value * > bits;
+  bits.create (size);
+
+  /* Initialize each bit of a variable with unknown value.  */
+  for (size_t i = 0; i < size; i++)
+    bits.quick_push (new symbolic_bit (i));
+
+  return var_states.put (var, bits);
+}
+
+
+/* Does bit-level AND operation for given variables.  */
+
+void
+State::do_and (tree* arg1, tree* arg2, tree* dest)
+{
+  gcc_assert (!(is_declared (arg1) || is_declared (arg2)
+		|| is_declared (dest)));
+  gcc_assert (get_var_size (arg1) == get_var_size (dest)
+	      && get_var_size (arg2) == get_var_size (dest));
+
+  /* Creating AND expressions for every bit pair of given arguments
+     and store them as a new state for given destination.  */
+
+  for (size_t i = 0; i < get_var_size (dest); i++)
+  {
+    value *result = nullptr;
+    value *sym_bit1 = dyn_cast<symbolic_bit *> ((*var_states.get (arg1))[i]);
+    if (sym_bit1 == nullptr)
+      sym_bit1 = dyn_cast<bit_expression *> ((*var_states.get (arg1))[i]);
+
+    value *sym_bit2 = dyn_cast<symbolic_bit *> ((*var_states.get (arg2))[i]);
+    if (sym_bit2 == nullptr)
+      sym_bit2 = dyn_cast<bit_expression *> ((*var_states.get (arg2))[i]);
+
+    bit *const_bit1 = dyn_cast<bit *> ((*var_states.get (arg1))[i]);
+    bit *const_bit2 = dyn_cast<bit *> ((*var_states.get (arg2))[i]);
+
+    if (sym_bit1 && sym_bit2)
+      result = and_sym_bits (sym_bit1, sym_bit2);
+    else if (sym_bit1 && const_bit2)
+      result = and_var_const (sym_bit1, const_bit2);
+    else if (const_bit1 && sym_bit2)
+      result = and_var_const (sym_bit2, const_bit1);
+    else if (const_bit1 && const_bit2)
+      result = and_const_bits (const_bit1, const_bit2);
+    else
+      gcc_assert (true);
+
+    delete (*var_states.get (dest))[i];
+    (*var_states.get (dest))[i] = result;
+  }
+}
+
+
+/* Does bit-level OR operation for given variables.  */
+
+void
+State::do_or (tree* arg1, tree* arg2, tree* dest)
+{
+  gcc_assert (!(is_declared (arg1) || is_declared (arg2)
+		|| is_declared (dest)));
+  gcc_assert (get_var_size (arg1) == get_var_size (dest)
+	      && get_var_size (arg2) == get_var_size (dest));
+
+  /* Creating OR expressions for every bit pair of given arguments
+   and store them as a new state for given destination.  */
+  for (size_t i = 0; i < get_var_size (dest); i++)
+  {
+    value *result = nullptr;
+    value *sym_bit1 = dyn_cast<symbolic_bit *> ((*var_states.get (arg1))[i]);
+    if (sym_bit1 == nullptr)
+      sym_bit1 = dyn_cast<bit_expression *> ((*var_states.get (arg1))[i]);
+
+    value *sym_bit2 = dyn_cast<symbolic_bit *> ((*var_states.get (arg2))[i]);
+    if (sym_bit2 == nullptr)
+      sym_bit2 = dyn_cast<bit_expression *> ((*var_states.get (arg2))[i]);
+
+    bit *const_bit1 = dyn_cast<bit *> ((*var_states.get (arg1))[i]);
+    bit *const_bit2 = dyn_cast<bit *> ((*var_states.get (arg2))[i]);
+
+    if (sym_bit1 && sym_bit2)
+      result = or_sym_bits (sym_bit1, sym_bit2);
+    else if (sym_bit1 && const_bit2)
+      result = or_var_const (sym_bit1, const_bit2);
+    else if (const_bit1 && sym_bit2)
+      result = or_var_const (sym_bit2, const_bit1);
+    else if (const_bit1 && const_bit2)
+      result = or_const_bits (const_bit1, const_bit2);
+    else
+      gcc_assert (true);
+
+    delete (*var_states.get (dest))[i];
+    (*var_states.get (dest))[i] = result;
+  }
+}
+
+
+/* Does bit-level XOR operation for given variables.  */
+
+void
+State::do_xor (tree *arg1, tree *arg2, tree *dest)
+{
+  gcc_assert (!(is_declared (arg1) || is_declared (arg2)
+		|| is_declared (dest)));
+  gcc_assert (get_var_size (arg1) == get_var_size (dest)
+	      && get_var_size (arg2) == get_var_size (dest));
+
+  for (size_t i = 0; i < get_var_size (dest); i++)
+  {
+    value *result = nullptr;
+    value *sym_bit1 = dyn_cast<symbolic_bit *> ((*var_states.get (arg1))[i]);
+    if (sym_bit1 == nullptr)
+      sym_bit1 = dyn_cast<bit_expression *> ((*var_states.get (arg1))[i]);
+
+    value *sym_bit2 = dyn_cast<symbolic_bit *> ((*var_states.get (arg2))[i]);
+    if (sym_bit2 == nullptr)
+      sym_bit2 = dyn_cast<bit_expression *> ((*var_states.get (arg2))[i]);
+
+    bit *const_bit1 = dyn_cast<bit *> ((*var_states.get (arg1))[i]);
+    bit *const_bit2 = dyn_cast<bit *> ((*var_states.get (arg2))[i]);
+
+    if (sym_bit1 && sym_bit2)
+      result = xor_sym_bits (sym_bit1, sym_bit2);
+    else if (sym_bit1 && const_bit2)
+      result = xor_var_const (sym_bit1, const_bit2);
+    else if (const_bit1 && sym_bit2)
+      result = xor_var_const (sym_bit2, const_bit1);
+    else if (const_bit1 && const_bit2)
+      result = xor_const_bits (const_bit1, const_bit2);
+    else
+      gcc_assert (true);
+
+    delete (*var_states.get (dest))[i];
+    (*var_states.get (dest))[i] = result;
+  }
+}
+
+
+/* Shifts value_vector left by shift_value bits.  */
+
+vec <value *>
+State::shift_left_by_const (const vec < value * > * value_vector,
+			    size_t shift_value)
+{
+  vec <value *> shift_result;
+  shift_result.create (value_vector->length ());
+  if (shift_result.length () <= shift_value)
+    for (size_t i = 0; i < shift_result.length (); i++)
+      shift_result[i] = new bit (0);
+  else
+  {
+    size_t i = 0;
+    for ( ; i < shift_result.length () - shift_value; ++i)
+      shift_result[i] = ((*value_vector)[shift_value + i])->copy ();
+
+    for ( ; i < shift_result.length (); ++i)
+      shift_result[i] = new bit (0);
+  }
+  return shift_result;
+}
+
+
+/* Checks if all vector elements are const_bit_expressions.  */
+
+bool
+State::is_bit_vector (vec <value *>* value_vector)
+{
+  for (size_t i = 0; i < value_vector->length (); i++)
+    if (!(is_a <bit *> ((*value_vector)[i])))
+	return false;
+  return true;
+}
+
+
+/* returns the value of the number represented as a bit vector.  */
+
+size_t
+State::get_value (vec <value *> * bit_vector)
+{
+  size_t number = 0;
+  for (int i = bit_vector->length () - 1; i >= 0; --i)
+  {
+    bit * cur_elem = dyn_cast<bit *> ((*bit_vector)[i]);
+    number = (number | cur_elem->get_val ()) << 1;
+  }
+
+  return number;
+}
+
+
+/* shift_left operation.  Case: var2 is a sym_bit.  */
+
+void
+State::shift_left_sym_bits (tree * var1, tree * var2, tree * dest)
+{
+  for (size_t i = 0; i < get_var_size (dest); i++)
+  {
+    value * var1_elem = (*var_states.get (var1))[i];
+    value * var2_elem = (*var_states.get (var2))[i];
+    value * new_elem = new shift_left_expression (var1_elem->copy (),
+						  var2_elem->copy ());
+    delete (*var_states.get (dest))[i];
+    (*var_states.get (dest))[i] = new_elem;
+  }
+}
+
+
+/* Does SHIFT_LEFT operation for given variables.  */
+
+void
+State::do_shift_left (tree * arg1, tree * arg2, tree * dest)
+{
+  gcc_assert (!(is_declared (arg1) || is_declared (arg2)
+		|| is_declared (dest)));
+  gcc_assert (get_var_size (arg1) == get_var_size (dest)
+  	      && get_var_size (arg2) == get_var_size (dest));
+
+  if (is_bit_vector (var_states.get (arg2)))
+  {
+    size_t shift_value = get_value (var_states.get (arg2));
+    vec <value *> result = shift_left_by_const (var_states.get (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];
+    }
+  }
+  else
+    shift_left_sym_bits (arg1, arg2, dest);
+}
+
+
+/* Does SHIFT_RIGHT operation for given variables.  */
+
+void
+State::do_shift_right (tree * arg1, tree * arg2, tree * dest)
+{
+  gcc_assert (!(is_declared (arg1) || is_declared (arg2)
+		|| is_declared (dest)));
+  gcc_assert (get_var_size (arg1) == get_var_size (dest)
+	      && get_var_size (arg2) == get_var_size (dest));
+
+  if (is_bit_vector (var_states.get (arg2)))
+  {
+    size_t shift_value = get_value (var_states.get (arg2));
+    vec <value *> result = shift_right_by_const (var_states.get (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];
+    }
+  }
+  else
+    shift_right_sym_bits (arg1, arg2, dest);
+}
+
+
+/* Adds two variables.  */
+
+void
+State::do_add (tree *arg1, tree *arg2, tree *dest)
+{
+  gcc_assert (!(is_declared (arg1) || is_declared (arg2)
+		|| is_declared (dest)));
+  gcc_assert (get_var_size (dest)
+	      == (get_var_size (arg1) > get_var_size (arg2)
+		  ? get_var_size (arg1) : get_var_size (arg2)));
+
+  for (size_t i = 0; i < get_var_size (dest); i++)
+  {
+    value * new_val = new add_expression ((*var_states.get (arg1))[i],
+					  (*var_states.get (arg2))[i]);
+    delete (*var_states.get (dest))[i];
+    (*var_states.get (dest))[i] = new_val;
+  }
+}
+
+
+/* Does subtraction.  */
+
+void
+State::do_sub (tree *arg1, tree *arg2, tree *dest)
+{
+  gcc_assert (!(is_declared (arg1) || is_declared (arg2)
+		|| is_declared (dest)));
+  gcc_assert (get_var_size (arg1) == get_var_size (dest)
+	      && get_var_size (arg2) == get_var_size (dest));
+
+  for (size_t i = 0; i < get_var_size (dest); i++)
+  {
+    value * new_val = new sub_expression ((*var_states.get (arg1))[i],
+					  (*var_states.get (arg2))[i]);
+    delete (*var_states.get (dest))[i];
+    (*var_states.get (dest))[i] = new_val;
+  }
+}
+
+
+/* Negates given variable.  */
+
+void
+State::do_complement (tree *arg, tree *dest)
+{
+  gcc_assert (!(is_declared (arg) || is_declared (dest)));
+  gcc_assert (get_var_size (arg) == get_var_size (dest));
+
+  /* Creating complement expressions for every bit the given argument
+     and store it as a new state for given destination.  */
+  for (size_t i = 0; i < get_var_size (dest); i++)
+  {
+    value *result = nullptr;
+    bit* const_bit = dyn_cast<bit *> ((*var_states.get (arg))[i]);
+    if (const_bit)
+      result = complement_const_bit (const_bit);
+    else
+      result = complement_sym_bit ((*var_states.get (arg))[i]);
+
+    delete (*var_states.get (dest))[i];
+    (*var_states.get (dest))[i] = result;
+  }
+}
+
+
+/* performs NOT operation for constant bit.  */
+
+bit *
+State::complement_const_bit (const bit * const_bit) const
+{
+  return new bit (1u - const_bit->get_val ());
+}
+
+
+/* performs NOT operation for symbolic_bit.  */
+
+value *
+State::complement_sym_bit (const value * var) const
+{
+  return new bit_complement_expression (var->copy ());
+}
+
+
+/* performs XOR operation for 2 symbolic_bit operands.  */
+
+value *
+State::xor_sym_bits (const value * var1, const value * var2) const
+{
+  value * var2_copy = var2->copy ();
+  bit_expression * var2_node_with_const_child
+      = get_parent_with_const_child (var2_copy);
+
+  if (var2_node_with_const_child != nullptr)
+  {
+    value * var1_copy = var1->copy ();
+    bit_expression * var1_node_with_const_child
+	= get_parent_with_const_child (var1_copy);
+
+    if (var1_node_with_const_child != nullptr)
+    {
+      value * var1_left = var1_node_with_const_child->get_left ();
+      if (var1_left != nullptr && dyn_cast<bit *> (var1_left) != nullptr)
+      {
+	value * var2_left = var2_node_with_const_child->get_left ();
+	if (var2_left != nullptr && dyn_cast<bit *> (var2_left) != nullptr)
+	{
+	  bit * new_left = xor_const_bits (dyn_cast<bit *> (var1_left),
+					   dyn_cast<bit *> (var2_left));
+	  delete var2_left;
+	  var2_node_with_const_child->set_left (nullptr);
+
+	  delete var1_left;
+	  var1_node_with_const_child->set_left (new_left);
+	}
+	else
+	{
+	  value * var2_right = var2_node_with_const_child->get_right ();
+	  bit * new_left = xor_const_bits (dyn_cast<bit *> (var1_left),
+					   dyn_cast<bit *> (var2_right));
+	  delete var2_right;
+	  var2_node_with_const_child->set_right (nullptr);
+
+	  delete var1_left;
+	  var1_node_with_const_child->set_left (new_left);
+	}
+      }
+
+      else
+      {
+	value * var1_right = var1_node_with_const_child->get_right ();
+	value * var2_left = var2_node_with_const_child->get_left ();
+	if (var2_left != nullptr && dyn_cast<bit *> (var2_left) != nullptr)
+	{
+	  bit * new_right = xor_const_bits (dyn_cast<bit *> (var1_left),
+					    dyn_cast<bit *> (var2_left));
+	  delete var2_left;
+	  var2_node_with_const_child->set_left (nullptr);
+
+	  delete var1_right;
+	  var1_node_with_const_child->set_right (new_right);
+	}
+	else
+	{
+	  value * var2_right = var2_node_with_const_child->get_right ();
+	  bit * new_right = xor_const_bits (dyn_cast<bit *> (var1_right),
+					    dyn_cast<bit *> (var2_right));
+	  delete var2_right;
+	  var2_node_with_const_child->set_right (nullptr);
+
+	  delete var1_right;
+	  var1_node_with_const_child->set_right (new_right);
+	}
+      }
+
+      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) const
+{
+  return new bit (const_bit1->get_val () ^ const_bit2->get_val ());
+}
+
+
+/* performs XOR operation for a symbolic_bit and const_bit operands.  */
+
+value *
+State::xor_var_const (const value * var, const bit * const_bit) const
+{
+  value * var_copy = var->copy ();
+  bit_expression * node_with_const_child
+      = get_parent_with_const_child (var_copy);
+  if (node_with_const_child != nullptr)
+  {
+    value * left = node_with_const_child->get_left ();
+    if (left != nullptr && dyn_cast<bit *> (left) != nullptr)
+    {
+      bit * new_left = xor_const_bits (dyn_cast<bit *> (left), const_bit);
+      delete left;
+      node_with_const_child->set_left (new_left);
+    }
+    else
+    {
+      value * right = node_with_const_child->get_right ();
+      bit * new_right = xor_const_bits (dyn_cast<bit *> (right), const_bit);
+      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.  */
+
+bit_expression *
+State::get_parent_with_const_child (value* root) const
+{
+  const bit_expression * expr = dyn_cast<const bit_expression *> (root);
+  if (expr == nullptr)
+    return nullptr;
+
+  bit_expression* expr_root = dyn_cast<bit_expression *> (expr->copy ());
+  hash_set<bit_expression *> nodes_to_consider;
+  nodes_to_consider.add (expr_root);
+
+  while (!nodes_to_consider.is_empty ())
+  {
+    bit_expression* cur_element = *nodes_to_consider.begin ();
+    nodes_to_consider.remove (cur_element);
+
+    value* left = cur_element->get_left ();
+    value* right = cur_element->get_right ();
+
+    if ((left != nullptr && dyn_cast<bit *> (left) != nullptr)
+	|| (right != nullptr && dyn_cast<bit *> (right) != nullptr))
+      return cur_element;
+
+    if (left != nullptr && is_safe_branching (left))
+      nodes_to_consider.add (dyn_cast<bit_expression *> (left));
+
+    if (right != nullptr && is_safe_branching (right))
+      nodes_to_consider.add (dyn_cast<bit_expression *> (right));
+  }
+}
+
+
+/* Checks if node is AND, OR or XOR expression.  */
+
+bool
+State::is_safe_branching (value* node) const
+{
+  return dyn_cast<bit_and_expression *> (node) != nullptr
+	 || dyn_cast<bit_or_expression *> (node) != nullptr
+	 || dyn_cast<bit_xor_expression *> (node) != nullptr;
+}
+
+
+/* Shifts value_vector right by shift_value bits.  */
+
+vec <value *>
+State::shift_right_by_const (const vec < value * > * value_vector,
+			     size_t shift_value)
+{
+  vec <value *> shift_result;
+  shift_result.create (value_vector->length ());
+  if (shift_result.length () <= shift_value)
+    for (size_t i = 0; i < shift_result.length (); i++)
+      {
+	shift_result[i] = new bit (0);
+      }
+  else
+    {
+      size_t i = 0;
+      for ( ; i < shift_result.length () - shift_value; ++i)
+	shift_result[i] = new bit (0);
+
+      for (size_t j = 0; i < shift_result.length (); ++i, ++j)
+	shift_result[i] = ((*value_vector)[j])->copy ();
+    }
+  return shift_result;
+}
+
+
+/* shift_right operation.  Case: var2 is a sym_bit.  */
+
+void
+State::shift_right_sym_bits (tree * var1, tree * var2, tree * dest)
+{
+  for (size_t i = 0; i < get_var_size (dest); i++)
+    {
+      value * var1_elem = (*var_states.get (var1))[i];
+      value * var2_elem = (*var_states.get (var2))[i];
+      value * new_elem = new shift_right_expression (var1_elem->copy (),
+						     var2_elem->copy ());
+      delete (*var_states.get (dest))[i];
+      (*var_states.get (dest))[i] = new_elem;
+    }
+}
diff --git a/gcc/sym-exec/state.h b/gcc/sym-exec/state.h
new file mode 100644
index 0000000..fd6d6d3
--- /dev/null
+++ b/gcc/sym-exec/state.h
@@ -0,0 +1,137 @@
+/* State will store states of variables for a function's single execution path.
+   It will be used for bit-level symbolic execution to determine values of bits
+   of function's return value and symbolic marked arguments.  */
+
+
+#ifndef SYM_EXEC_STATE_H
+#define SYM_EXEC_STATE_H
+
+#include "expression.h"
+#include "config.h"
+#include "system.h"
+#include "coretypes.h"
+#include "backend.h"
+#include "tree.h"
+#include "gimple.h"
+#include "tree-pass.h"
+#include "ssa.h"
+#include "gimple-iterator.h"
+#include "tree-cfg.h"
+#include "tree-ssa-loop-niter.h"
+#include "cfgloop.h"
+#include "gimple-range.h"
+#include "tree-scalar-evolution.h"
+#include "hwint.h"
+#include "gimple-pretty-print.h"
+#include "is-a.h"
+#include "vec.h"
+#include "hash-map.h"
+
+/* Stores states of variables' values on bit-level.  */
+
+class State {
+ private:
+  /* Here is stored values of bit of each variable.  */
+  hash_map<tree *, vec < value * >> var_states;
+
+  /* Performs AND operation for 2 symbolic_bit operands.  */
+  value *and_sym_bits (const value * var1, const value * var2) const;
+
+  /* Performs AND operation for a symbolic_bit and const_bit operands.  */
+  value *and_var_const (const value * var1, const bit * const_bit) const;
+
+  /* Performs AND operation for 2 constant bit operands.  */
+  bit *and_const_bits (const bit * const_bit1, const bit * const_bit2) const;
+
+  /* Performs OR operation for 2 symbolic_bit operands.  */
+  value *or_sym_bits (const value * var1, const value * var2) const;
+
+  /* Performs OR operation for a symbolic_bit and a constant bit operands.  */
+  value *or_var_const (const value * var1, const bit * const_bit) const;
+
+  /* Performs OR operation for 2 constant bit operands.  */
+  bit *or_const_bits (const bit * const_bit1, const bit * const_bit2) const;
+
+  /* Performs NOT operation for constant bit.  */
+  bit *complement_const_bit (const bit * const_bit) const;
+
+  /* Performs NOT operation for symbolic_bit.  */
+  value *complement_sym_bit (const value * var) const;
+
+  /* Performs XOR operation for 2 symbolic_bit operands.  */
+  value *xor_sym_bits (const value * var1, const value * var2) const;
+
+  /* Performs XOR operation for 2 constant bit operands.  */
+  bit *xor_const_bits (const bit * const_bit1, const bit * const_bit2) const;
+
+  /* Performs XOR operation for a symbolic_bit and const_bit operands.  */
+  value *xor_var_const (const value * var, const bit * const_bit) const;
+
+  /* Return node which has a const bit child.  Traversal is done based
+     on safe branching.  */
+  bit_expression* get_parent_with_const_child (value* root) const;
+
+  /* Checks if node is AND, OR or XOR expression.  */
+  bool is_safe_branching (value* node) const;
+
+  /* Checks whether state for variable with specified name already
+     exists or not.  */
+  bool is_declared (tree *var);
+
+ public:
+  /* Adds an empty state for the given variable.  */
+  bool decl_var (tree *name, unsigned size);
+
+  /* Adds a variable with unknown value to state.  Such variables are
+     represented as sequence of symbolic bits.  */
+  bool make_symbolic (tree *var, unsigned size);
+
+  /* Returns size of the given variable.  */
+  unsigned get_var_size (tree *var);
+
+  /* Does bit-level XOR operation for given variables.  */
+  void do_xor (tree *arg1, tree *arg2, tree *dest);
+
+  /* Does bit-level AND operation for given variables.  */
+  void do_and (tree *arg1, tree *arg2, tree *dest);
+
+  /* Does bit-level OR operation for given variables.  */
+  void do_or (tree *arg1, tree *arg2, tree *dest);
+
+  /* Shifts value_vector left by shift_value bits.  */
+  vec <value *> shift_left_by_const (const vec <value *> * value_vector,
+				     size_t shift_value);
+
+  /* Checks if all vector elements are const_bit_expressions.  */
+  bool is_bit_vector (vec <value *> * value_vector);
+
+  /* returns the value of the number represented as a bit vector.  */
+  size_t get_value (vec <value *> *  bit_vector);
+
+  /* shift_left operation.  Case: var2 is a sym_bit.  */
+  void shift_left_sym_bits (tree * var1, tree * var2, tree * dest);
+
+  /* Does SHIFT_LEFT operation for given variables.  */
+  void do_shift_left (tree *arg1, tree *arg2, tree *dest);
+
+  /* Shifts value_vector right by shift_value bits.  */
+  vec <value *> shift_right_by_const (const vec <value *> * value_vector,
+				      size_t shift_value);
+
+  /* shift_right operation.  Case: var2 is a sym_bit.  */
+  void shift_right_sym_bits (tree * var1, tree * var2, tree * dest);
+
+  /* Does SHIFT_RIGHT operation for given variables.  */
+  void do_shift_right (tree *arg1, tree *arg2, tree *dest);
+
+  /* Adds two variables.  */
+  void do_add (tree *arg1, tree *arg2, tree *dest);
+
+  /* Does subtraction.  */
+  void do_sub (tree *arg1, tree *arg2, tree *dest);
+
+  /* Negates given variable.  */
+  void do_complement (tree *arg, tree *dest);
+};
+
+#endif /* SYM_EXEC_STATE_H.  */