sym-exec v5: - Added last added condition status saving support - Save only conditions with symbolic elements - Added support for printing expression tree - Save origin of symbolic values so we can identify it later - Fixed constant values' bits construction - Define destination var if it is not define - Fixed addition and subtraction - Added some utility functions - Fixed condition adding - Added Cast expression support - Added comments for some functions

6 files changed, 427 insertions, 151 deletions

diff --git a/gcc/sym-exec/condition.h b/gcc/sym-exec/condition.h
index 5c595197551..687ebbf787d 100644
--- a/gcc/sym-exec/condition.h
+++ b/gcc/sym-exec/condition.h
@@ -16,6 +16,15 @@ enum condition_type
 };
 
 
+enum condition_status
+{
+  CS_NO_COND,
+  CS_TRUE,
+  CS_FALSE,
+  CS_SYM
+};
+
+
 class bit_condition : public bit_expression
 {
  private:
diff --git a/gcc/sym-exec/expression-is-a-helper.h b/gcc/sym-exec/expression-is-a-helper.h
index 90a5917c843..dafc91c1597 100644
--- a/gcc/sym-exec/expression-is-a-helper.h
+++ b/gcc/sym-exec/expression-is-a-helper.h
@@ -2,7 +2,6 @@
 #define SYM_EXEC_EXPRESSION_IS_A_HELPER_H
 
 #include "condition.h"
-#include "is-a.h"
 
 
 /* Defining test functions for value conversion via dyn_cast.  */
diff --git a/gcc/sym-exec/expression.cc b/gcc/sym-exec/expression.cc
index 8b9a1feb6e7..0065c13b05b 100644
--- a/gcc/sym-exec/expression.cc
+++ b/gcc/sym-exec/expression.cc
@@ -2,8 +2,6 @@
    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"
 #include "expression-is-a-helper.h"
 
 
@@ -60,6 +58,8 @@ bit_complement_expression::bit_complement_expression (value *right)
 {
   this->left = nullptr;
   this->right = right;
+  op_sign[0] = '!';
+  op_sign[1] = '\0';
 }
 
 
@@ -101,6 +101,9 @@ bit_expression::copy (const bit_expression *expr)
 
   if (expr->right)
     right = expr->right->copy ();
+
+  op_sign[0] = (expr->op_sign)[0];
+  op_sign[1] = (expr->op_sign)[1];
 }
 
 
@@ -164,6 +167,8 @@ bit_xor_expression::bit_xor_expression (value *left, value *right)
 {
   this->left = left;
   this->right = right;
+  op_sign[0] = '^';
+  op_sign[1] = '\0';
 }
 
 
@@ -177,6 +182,8 @@ bit_and_expression::bit_and_expression (value *left, value *right)
 {
   this->left = left;
   this->right = right;
+  op_sign[0] = '&';
+  op_sign[1] = '\0';
 }
 
 
@@ -190,6 +197,8 @@ bit_or_expression::bit_or_expression (value *left, value *right)
 {
   this->left = left;
   this->right = right;
+  op_sign[0] = '|';
+  op_sign[0] = '\0';
 }
 
 
@@ -203,6 +212,8 @@ shift_right_expression::shift_right_expression (value *left, value *right)
 {
   this->left = left;
   this->right = right;
+  op_sign[0] = '>';
+  op_sign[1] = '>';
 }
 
 
@@ -217,6 +228,8 @@ shift_left_expression::shift_left_expression (value *left, value *right)
 {
   this->left = left;
   this->right = right;
+  op_sign[0] = '<';
+  op_sign[1] = '<';
 }
 
 
@@ -230,6 +243,8 @@ add_expression::add_expression (value *left, value *right)
 {
   this->left = left;
   this->right = right;
+  op_sign[0] = '+';
+  op_sign[1] = '\0';
 }
 
 
@@ -243,6 +258,8 @@ sub_expression::sub_expression (value *left, value *right)
 {
   this->left = left;
   this->right = right;
+  op_sign[0] = '-';
+  op_sign[1] = '\0';
 }
 
 
@@ -320,3 +337,66 @@ sub_expression::get_type () const
 {
   return value_type::SUB_EXPRESSION;
 }
+
+
+tree
+symbolic_bit::get_origin ()
+{
+  return origin;
+}
+
+
+void
+symbolic_bit::print ()
+{
+  if (dump_file)
+    {
+      print_generic_expr (dump_file, origin, dump_flags);
+      fprintf (dump_file, "[%lu]", index);
+    }
+}
+
+
+void
+bit::print ()
+{
+  if (dump_file)
+    fprintf (dump_file, "%u", val);
+}
+
+
+void
+bit_expression::print ()
+{
+  if (dump_file)
+    {
+      fprintf (dump_file, "(");
+      if (left)
+	left->print ();
+      else
+	fprintf (dump_file, "null");
+
+      fprintf (dump_file, " %.2s ", op_sign);
+
+      if (right)
+	right->print ();
+      else
+	fprintf (dump_file, "null");
+
+      fprintf (dump_file, ")");
+    }
+}
+
+
+void
+bit_complement_expression::print ()
+{
+  if (dump_file)
+    {
+      fprintf (dump_file, "%.2s", op_sign);
+      if (right)
+	right->print ();
+      else
+	fprintf (dump_file, "null");
+    }
+}
\ No newline at end of file
diff --git a/gcc/sym-exec/expression.h b/gcc/sym-exec/expression.h
index 25a85aa5e0d..9d03a4e2467 100644
--- a/gcc/sym-exec/expression.h
+++ b/gcc/sym-exec/expression.h
@@ -5,6 +5,26 @@
 #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 "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"
+#include "hash-set.h"
 #include "stddef.h"
 
 
@@ -42,6 +62,7 @@ class value {
   /* This will support deep copy of objects' values.  */
   virtual value *copy () const = 0;
   virtual value_type get_type () const = 0;
+  virtual void print () = 0;
   virtual ~value ()
   {};
 };
@@ -50,14 +71,19 @@ class value {
 /* Represents value of a single bit of symbolic marked variables.  */
 
 class symbolic_bit : public value {
+  tree origin = nullptr;
+
  public:
-  symbolic_bit (size_t i) : value (i)
+  symbolic_bit (size_t i, tree orig) : value (i), origin (orig)
   {};
-  symbolic_bit (const symbolic_bit &sym_bit) : symbolic_bit (sym_bit.index)
+  symbolic_bit (const symbolic_bit &sym_bit) : symbolic_bit (sym_bit.index,
+							     sym_bit.origin)
   {};
 
   value *copy () const;
+  void print ();
   value_type get_type () const;
+  tree get_origin ();
 };
 
 
@@ -77,6 +103,7 @@ class bit : public value {
   void set_val (unsigned char new_val);
   value *copy () const;
   value_type get_type () const;
+  void print ();
 };
 
 
@@ -87,6 +114,7 @@ class bit_expression : public value {
  protected:
   value *left = nullptr;
   value *right = nullptr;
+  char op_sign[2];
 
   void copy (const bit_expression *expr);
 
@@ -100,6 +128,7 @@ class bit_expression : public value {
   void set_right (value *expr);
   value *copy () const = 0;
   value_type get_type () const = 0;
+  void print ();
 };
 
 
@@ -193,6 +222,7 @@ class bit_complement_expression : public bit_expression {
   bit_complement_expression (const bit_complement_expression &expr);
   value *copy () const;
   value_type get_type () const;
+  void print ();
 };
 
 
diff --git a/gcc/sym-exec/state.cc b/gcc/sym-exec/state.cc
index 800dd8f13c5..809e0a91b5d 100644
--- a/gcc/sym-exec/state.cc
+++ b/gcc/sym-exec/state.cc
@@ -2,11 +2,7 @@
    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 "condition.h"
 
 
 state::state ()
@@ -70,17 +66,11 @@ state::get_conditions ()
 }
 
 
+/* Checks if sizes of arguments and destination are compatible.  */
+
 bool
 state::check_args_compatibility (tree arg1, tree arg2, tree dest)
 {
-  if (!is_declared (dest))
-    {
-      if (dump_file && (dump_flags & TDF_DETAILS))
-	fprintf (dump_file, "Sym-Exec: Destination var is not declared.\n");
-
-      return false;
-    }
-
   if (!(get_var_size (arg1) == get_var_size (dest)
        || TREE_CODE (arg1) == INTEGER_CST)
       || !(get_var_size (arg2) == get_var_size (dest)
@@ -97,24 +87,27 @@ state::check_args_compatibility (tree arg1, tree arg2, tree dest)
 }
 
 
+/* Creates bit sequence of given constant tree.  */
+
 vec<value*>
 state::create_bits_for_const (tree var, size_t size) const
 {
   HOST_WIDE_INT val = tree_to_shwi (var);
-  unsigned HOST_WIDE_INT pos_bit = 1;
-
   vec<value *> bits;
   bits.create (size);
+
   for (size_t i = 0; i < size; i++)
     {
-      bits.quick_push (new bit (val & pos_bit));
-      pos_bit >>= 1;
+      bits.quick_push (new bit (val & 1));
+      val >>= 1;
     }
 
   return bits;
 }
 
 
+/* Removes given sequence of bits.  */
+
 void
 state::free_bits (vec<value*> * bits) const
 {
@@ -293,7 +286,7 @@ state::make_symbolic (tree var, unsigned 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));
+    bits.quick_push (new symbolic_bit (i, var));
 
   return var_states.put (var, bits);
 }
@@ -324,16 +317,21 @@ state::and_two_bits (value *arg1_bit, value* arg2_bit) const
 }
 
 
+/* Does preprocessing and postprocessing for expressions with tree operands.
+   Handles bit sequence creation for constant values
+   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;
 
-  declare_if_needed (arg1, var_states.get (dest)->length ());
-  declare_if_needed (arg2, var_states.get (dest)->length ());
-
   vec<value*> * arg1_bits = var_states.get (arg1);
   vec<value*> arg1_const_bits (vNULL);
   if (arg1_bits == NULL && TREE_CODE (arg1) == INTEGER_CST)
@@ -356,6 +354,7 @@ state::do_binary_operation (tree arg1, tree arg2, tree dest,
   free_bits (&arg1_const_bits);
   free_bits (&arg2_const_bits);
 
+  print_bits (var_states.get (dest));
   return true;
 }
 
@@ -522,15 +521,15 @@ state::is_bit_vector (const vec <value *>* bits)
 
 /* Returns the value of the number represented as a bit vector.  */
 
-size_t
-state::get_value (const vec <value *> * binary_value)
+unsigned HOST_WIDE_INT
+state::get_value (const vec <value *> * bits_value)
 {
-  size_t number = 0;
-  if (binary_value->length () <= sizeof (size_t))
-    for (unsigned i = 0; i < binary_value->length (); i++)
+  unsigned HOST_WIDE_INT number = 0;
+  if (bits_value->length () <= sizeof (size_t))
+    for (unsigned i = 0; i < bits_value->length (); i++)
       {
-	if (is_a<bit *> ((*binary_value)[i]))
-	  number = (number | as_a<bit*> ((*binary_value)[i])->get_val ()) << 1;
+	if (is_a<bit *> ((*bits_value)[i]))
+	  number = (number | as_a<bit*> ((*bits_value)[i])->get_val ()) << 1;
 	else
 	  return 0;
       }
@@ -652,7 +651,7 @@ void
 state::do_add (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest)
 {
   value * carry = new bit (0);
-  for (size_t i =  get_var_size (dest) - 1; i != 0; --i)
+  for (size_t i = 0; i < get_var_size (dest); ++i)
     {
       value * temp = (*var_states.get (dest))[i];
       (*var_states.get (dest))[i] = full_adder ((*arg1_bits)[i],
@@ -667,26 +666,26 @@ state::do_add (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest)
 /* Returns the additive inverse of the number stored in number verctor.  */
 
 vec < value * > *
-state::additive_inverse (const vec < value * > *number)
+state::additive_inverse (const vec <value *> *number)
 {
-  vec < value * > * result = new vec < value * > ();
-  vec < value * > * one = new vec < value * > ();
+  vec <value *> * result = new vec <value *> ();
+  vec <value *> * one = new vec <value *> ();
 
   result->create (number->length ());
   one->create (number -> length ());
+
   size_t vec_len = number->length ();
+  one->quick_push (new bit (1));
+  result->quick_push (complement_a_bit ((*number)[0]->copy ()));
 
-  for (size_t i = 0; i < vec_len; i++)
+  for (size_t i = 1; i < vec_len; i++)
     {
-      if (i == vec_len - 1)
-	one->quick_push (new bit (1));
-      else
-	one->quick_push (new bit (0));
+      one->quick_push (new bit (0));
       result->quick_push (complement_a_bit ((*number)[i]->copy ()));
     }
 
   value * carry = new bit (0);
-  for (size_t i = vec_len - 1; i != 0; --i)
+  for (size_t i = 0; i < vec_len; ++i)
     (*result)[i] = full_adder ((*result)[i], (*one)[i], carry);
 
   delete carry;
@@ -707,7 +706,6 @@ void
 state::do_sub (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest)
 {
   vec < value * > * neg_arg2 = additive_inverse (arg2_bits);
-
   do_add (arg1_bits, neg_arg2, dest);
 
   free_bits (neg_arg2);
@@ -736,15 +734,9 @@ state::complement_a_bit (value *var) const
 bool
 state::do_complement (tree arg, tree dest)
 {
-  if (!is_declared (dest))
-    {
-      if (dump_file && (dump_flags & TDF_DETAILS))
-	fprintf (dump_file, "Sym-Exec: Destination var is not declared.\n");
+  declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+  declare_if_needed (arg, var_states.get (dest)->allocated ());
 
-      return false;
-    }
-
-  declare_if_needed (arg, var_states.get (dest)->length ());
   if (get_var_size (arg) != get_var_size (dest))
     {
       if (dump_file && (dump_flags & TDF_DETAILS))
@@ -764,6 +756,7 @@ state::do_complement (tree arg, tree dest)
       (*var_states.get (dest))[i] = result;
     }
 
+  print_bits (var_states.get (dest));
   return true;
 }
 
@@ -771,16 +764,10 @@ state::do_complement (tree arg, tree dest)
 bool
 state::do_assign (tree arg, tree dest)
 {
-  if (!is_declared (dest))
-    {
-      if (dump_file && (dump_flags & TDF_DETAILS))
-	fprintf (dump_file, "Sym-Exec: Destination var is not declared.\n");
-
-      return false;
-    }
-
-  declare_if_needed (arg, var_states.get (dest)->length ());
+  declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+  declare_if_needed (arg, var_states.get (dest)->allocated ());
   vec<value*> * dest_bits = var_states.get (dest);
+
   /* If the argument is already defined, then we must just copy its bits.  */
   if (auto bits = var_states.get (arg))
     {
@@ -799,7 +786,7 @@ state::do_assign (tree arg, tree dest)
   /* If the argument is a constant, we must save it as sequence of bits.  */
   else if (TREE_CODE (arg) == INTEGER_CST)
     {
-      vec < value * > arg_bits
+      vec <value *> arg_bits
       = create_bits_for_const (arg, dest_bits->length ());
       for (size_t i = 0; i < dest_bits->length (); i++)
 	{
@@ -815,6 +802,44 @@ state::do_assign (tree arg, tree dest)
 
       return false;
     }
+
+  print_bits (var_states.get (dest));
+  return true;
+}
+
+
+/* Assigns pow 2 value.  */
+
+bool
+state::do_assign_pow2 (tree dest, unsigned pow)
+{
+  vec<value *> * dest_bits = var_states.get (dest);
+  unsigned dest_size = dest_bits ? dest_bits->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_bits)
+    {
+      decl_var (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+      dest_bits = var_states.get (dest);
+    }
+  else
+    free_bits (dest_bits);
+
+  for (unsigned i = 0; i < dest_bits->length (); i++)
+    {
+      if (i == pow)
+	(*dest_bits)[i] = new bit (1);
+      else
+	(*dest_bits)[i] = new bit (0);
+    }
+
   return true;
 }
 
@@ -1013,7 +1038,7 @@ state::is_safe_branching (value* node) const
 /* Shifts number left by shift_value bits.  */
 
 vec <value *> *
-state::shift_left_by_const (const vec < value * > * number,
+state::shift_left_by_const (const vec <value *> * number,
 			    size_t shift_value)
 {
   vec <value *> *shift_result = new vec< value * > ();
@@ -1052,10 +1077,10 @@ state::shift_right_sym_bits (vec<value*> * arg1_bits, vec<value*> * arg2_bits,
 }
 
 
-/* Adds two vectors, stores the result in the first one.  */
+/* Adds two variables, stores the result in the first one.  */
 
 void
-state::add_numbers (vec< value * > *var1, const vec< value * > *var2)
+state::add_numbers (vec<value *> *var1, const vec<value *> *var2)
 {
   value * carry = new bit (0);
   for (unsigned i = 0; i < var1->length (); i++)
@@ -1095,9 +1120,8 @@ state::do_mul (tree arg1, tree arg2, tree dest)
 void
 state::do_mul (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest)
 {
-  vec <value *> *shifted = new vec <value *> ();
-  vec_copy_construct (shifted, arg1_bits, arg1_bits->length ());
   vec <value *> * dest_bits = var_states.get (dest);
+  vec <value *> * shifted = make_copy (arg1_bits);
 
   for (unsigned i = 0; i < dest_bits->length (); i++)
     {
@@ -1105,26 +1129,21 @@ state::do_mul (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest)
       (*dest_bits)[i] = new bit (0);
     }
 
-  for (unsigned i = arg2_bits->length () - 1; i != 0; --i)
+  for (unsigned i = arg2_bits->length (); i != 0; --i)
     {
-      if (is_a<bit *> ((*arg2_bits)[i]))
-	{
-	  if (as_a<bit *> ((*arg2_bits)[i])->get_val () != 0)
-	  add_numbers (dest_bits, shifted);
-	}
-      else if (is_a<symbolic_bit *> ((*arg2_bits)[i]))
+      if (is_a<bit *> ((*arg2_bits)[i - 1])
+	  && as_a<bit *> ((*arg2_bits)[i - 1])->get_val () != 0)
+	add_numbers (dest_bits, shifted);
+      else if (is_a<symbolic_bit *> ((*arg2_bits)[i - 1]))
 	{
-	  and_number_bit (shifted, as_a<symbolic_bit *> ((*arg2_bits)[i]));
+	  and_number_bit (shifted, as_a<symbolic_bit *> ((*arg2_bits)[i - 1]));
 	  add_numbers (dest_bits, shifted);
 	}
-
-      vec <value *> *temp = shifted;
+      vec <value *> * temp = shifted;
       shifted = shift_left_by_const (shifted, 1);
-
       free_bits (temp);
       delete temp;
     }
-
   free_bits (shifted);
   delete shifted;
 }
@@ -1135,7 +1154,8 @@ state::check_const_bit_equality (vec<value *> * arg1_bits,
 				 vec<value *> * arg2_bits) const
 {
   for (size_t i = 1; i < arg1_bits->length (); i++)
-    if ((*arg1_bits)[i] != (*arg2_bits)[i])
+    if (as_a<bit *>((*arg1_bits)[i])->get_val ()
+	!= as_a<bit *>((*arg2_bits)[i])->get_val ())
       return false;
   return true;
 }
@@ -1148,15 +1168,16 @@ state::add_equal_cond (tree arg1, tree arg2)
 }
 
 
+/* Adds equality condition for two sequences of bits.  */
+
 void
 state::add_equal_cond (vec<value*> * arg1_bits, vec<value*> * arg2_bits)
 {
   if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
     {
       bool result = check_const_bit_equality (arg1_bits, arg2_bits);
-      conditions.add (new bit_condition (nullptr, nullptr,
-					 result ? condition_type::IS_TRUE
-						: condition_type::IS_FALSE));
+      last_cond_status = result ? condition_status::CS_TRUE
+				: condition_status::CS_FALSE;
       return;
     }
   for (size_t i = 0; i < arg1_bits->length (); i++)
@@ -1165,6 +1186,7 @@ state::add_equal_cond (vec<value*> * arg1_bits, vec<value*> * arg2_bits)
 					 (*arg2_bits)[i]->copy (),
 					 condition_type::EQUAL));
     }
+  last_cond_status = condition_status::CS_SYM;
 }
 
 
@@ -1173,7 +1195,8 @@ state::check_const_bit_are_not_equal (vec<value *> * arg1_bits,
 				      vec<value *> * arg2_bits) const
 {
   for (size_t i = 0; i < arg1_bits->length (); i++)
-    if ((*arg1_bits)[i] != (*arg2_bits)[i])
+    if (as_a<bit *>((*arg1_bits)[i])->get_val ()
+	!= as_a<bit*>((*arg2_bits)[i])->get_val ())
       return true;
   return false;
 }
@@ -1186,15 +1209,16 @@ state::add_not_equal_cond (tree arg1, tree arg2)
 }
 
 
+/* Adds not equal condition for two sequences of bits.  */
+
 void
 state::add_not_equal_cond (vec<value*> * arg1_bits, vec<value*> * arg2_bits)
 {
   if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
     {
       bool result = check_const_bit_are_not_equal (arg1_bits, arg2_bits);
-      conditions.add (new bit_condition (nullptr, nullptr,
-					 result ? condition_type::IS_TRUE
-						: condition_type::IS_FALSE));
+      last_cond_status = result ? condition_status::CS_TRUE
+				: condition_status::CS_FALSE;
       return;
     }
 
@@ -1209,6 +1233,8 @@ state::add_not_equal_cond (vec<value*> * arg1_bits, vec<value*> * arg2_bits)
       else
 	prev = new_cond;
     }
+
+  last_cond_status = condition_status::CS_SYM;
   conditions.add (prev);
 }
 
@@ -1219,9 +1245,11 @@ state::check_const_bit_is_greater_than (vec<value *> * arg1_bits,
 {
   for (int i = arg1_bits->length () - 1; i >= 0; i--)
     {
-      if ((*arg1_bits)[i] > (*arg2_bits)[i])
+      if (as_a<bit *>((*arg1_bits)[i])->get_val ()
+	  > as_a<bit *>((*arg2_bits)[i])->get_val ())
 	return true;
-      else if ((*arg1_bits)[i] < (*arg2_bits)[i])
+      else if (as_a<bit *>((*arg1_bits)[i])->get_val ()
+	       < as_a<bit *>((*arg2_bits)[i])->get_val ())
 	return false;
     }
   return false;
@@ -1235,6 +1263,8 @@ state::add_greater_than_cond (tree arg1, tree arg2)
 }
 
 
+/* Adds greater than condition for two sequences of bits.  */
+
 void
 state::add_greater_than_cond (vec<value*> * arg1_bits,
 			      vec<value*> * arg2_bits)
@@ -1242,16 +1272,19 @@ state::add_greater_than_cond (vec<value*> * arg1_bits,
   if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
     {
       bool result = check_const_bit_is_greater_than (arg1_bits, arg2_bits);
-      conditions.add (new bit_condition (nullptr, nullptr,
-					 result ? condition_type::IS_TRUE
-						: condition_type::IS_FALSE));
+      last_cond_status = result ? condition_status::CS_TRUE
+				: condition_status::CS_FALSE;
       return;
     }
 
+  last_cond_status = condition_status::CS_SYM;
   conditions.add (construct_great_than_cond (arg1_bits, arg2_bits));
 }
 
 
+/* Constructs expression trees of greater than condition
+   for given sequences of bits.  */
+
 bit_expression*
 state::construct_great_than_cond (vec<value*> * arg1_bits,
 				  vec<value*> * arg2_bits)
@@ -1286,9 +1319,11 @@ state::check_const_bit_is_less_than (vec<value *> * arg1_bits,
 {
   for (int i = arg1_bits->length () - 1; i >= 0; i--)
     {
-      if ((*arg1_bits)[i] < (*arg2_bits)[i])
+      if (as_a<bit *>((*arg1_bits)[i])->get_val ()
+	  < as_a<bit *>((*arg2_bits)[i])->get_val ())
 	return true;
-      else if ((*arg1_bits)[i] > (*arg2_bits)[i])
+      else if (as_a<bit *>((*arg1_bits)[i])->get_val ()
+	       > as_a<bit *>((*arg2_bits)[i])->get_val ())
 	return false;
     }
   return false;
@@ -1302,22 +1337,27 @@ state::add_less_than_cond (tree arg1, tree arg2)
 }
 
 
+/* Adds less than condition for two sequences of bits.  */
+
 void
 state::add_less_than_cond (vec<value*> * arg1_bits, vec<value*> * arg2_bits)
 {
   if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
     {
       bool result = check_const_bit_is_less_than (arg1_bits, arg2_bits);
-      conditions.add (new bit_condition (nullptr, nullptr,
-					 result ? condition_type::IS_TRUE
-						: condition_type::IS_FALSE));
+      last_cond_status = result ? condition_status::CS_TRUE
+				: condition_status::CS_FALSE;
       return;
     }
 
+  last_cond_status = condition_status::CS_SYM;
   conditions.add (construct_less_than_cond (arg1_bits, arg2_bits));
 }
 
 
+/* Constructs expression trees of less than condition
+   for given sequences of bits.  */
+
 bit_expression*
 state::construct_less_than_cond (vec<value*> * arg1_bits,
 				 vec<value*> * arg2_bits)
@@ -1353,6 +1393,8 @@ state::add_greater_or_equal_cond (tree arg1, tree arg2)
 }
 
 
+/* Adds greater or equal condition for two sequences of bits.  */
+
 void
 state::add_greater_or_equal_cond (vec<value*> * arg1_bits,
 				  vec<value*> * arg2_bits)
@@ -1362,19 +1404,21 @@ state::add_greater_or_equal_cond (vec<value*> * arg1_bits,
       bool is_greater_than = check_const_bit_is_greater_than (arg1_bits,
 							      arg2_bits);
       bool is_equal = check_const_bit_equality (arg1_bits, arg2_bits);
-      conditions.add (new bit_condition (nullptr, nullptr,
-					 (is_greater_than | is_equal)
-					 ? condition_type::IS_TRUE
-					 : condition_type::IS_FALSE));
+      last_cond_status = (is_greater_than | is_equal)
+			 ? condition_status::CS_TRUE
+			 : condition_status::CS_FALSE;
       return;
     }
 
+  last_cond_status = condition_status::CS_SYM;
   conditions.add (
 	new bit_or_expression (construct_great_than_cond (arg1_bits, arg2_bits),
 			       construct_equal_cond (arg1_bits, arg2_bits)));
 }
 
 
+/* Adds less or equal condition for two sequences of bits.  */
+
 bool
 state::add_less_or_equal_cond (tree arg1, tree arg2)
 {
@@ -1390,13 +1434,13 @@ state::add_less_or_equal_cond (vec<value*> * arg1_bits,
     {
       bool is_less_than = check_const_bit_is_less_than (arg1_bits, arg2_bits);
       bool is_equal = check_const_bit_equality (arg1_bits, arg2_bits);
-      conditions.add (new bit_condition (nullptr, nullptr,
-					 (is_less_than | is_equal)
-					 ? condition_type::IS_TRUE
-					 : condition_type::IS_FALSE));
+      last_cond_status = (is_less_than | is_equal)
+			 ? condition_status::CS_TRUE
+			 : condition_status::CS_FALSE;
       return;
     }
 
+  last_cond_status = condition_status::CS_SYM;
   conditions.add (
 	new bit_or_expression (construct_less_than_cond (arg1_bits, arg2_bits),
 			       construct_equal_cond (arg1_bits, arg2_bits)));
@@ -1417,14 +1461,14 @@ state::add_bool_cond (tree arg)
   vec<value *> * arg_bits = var_states.get (arg);
   if (is_bit_vector (arg_bits))
     {
-      condition_type result = condition_type::IS_FALSE;
+      last_cond_status = condition_status::CS_FALSE;
       for (size_t i = 0; i < arg_bits->length (); i++)
-	if ((*arg_bits)[i] != 0)
+	if (as_a<bit *>((*arg_bits)[i])->get_val () != 0)
 	  {
-	    result = condition_type::IS_TRUE;
+	    last_cond_status = condition_status::CS_TRUE;
 	    break;
 	  }
-      conditions.add (new bit_condition (nullptr, nullptr, result));
+      return true;
     }
 
   bit_expression* prev = nullptr;
@@ -1439,11 +1483,16 @@ state::add_bool_cond (tree arg)
 	prev = not_eq_cond;
     }
 
+  last_cond_status = condition_status::CS_SYM;
   conditions.add (prev);
   return true;
 }
 
 
+/* Does preprocessing and postprocessing for condition adding.
+   Handles bit sequence creation for constant values
+   and their removement in the end.  */
+
 bool
 state::add_binary_cond (tree arg1, tree arg2, binary_cond_func cond_func)
 {
@@ -1490,6 +1539,9 @@ state::add_binary_cond (tree arg1, tree arg2, binary_cond_func cond_func)
 }
 
 
+/* Constructs expression trees of equal condition
+   for given sequences of bits.  */
+
 bit_expression*
 state::construct_equal_cond (vec<value*> * arg1_bits,
 			     vec<value*> * arg2_bits)
@@ -1515,11 +1567,12 @@ state::construct_equal_cond (vec<value*> * arg1_bits,
 bool
 state::do_mem_ref (tree arg1, tree dest)
 {
-  if (!is_declared (arg1) || !is_declared (dest))
+  declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+  if (!is_declared (arg1))
     {
       if (dump_file && (dump_flags & TDF_DETAILS))
-	fprintf (dump_file, "Sym-Exec: For memory reference, both destination"
-			    "and argument must be declared\n");
+	fprintf (dump_file, "Sym-Exec: For memory reference"
+			    " argument must be declared\n");
 
       return false;
     }
@@ -1528,9 +1581,10 @@ state::do_mem_ref (tree arg1, tree dest)
     {
       delete (*var_states.get (dest))[i];
       // TODO: Find a better way.
-      (*var_states.get (dest))[i] = new symbolic_bit (i);
+      (*var_states.get (dest))[i] = new symbolic_bit (i, arg1);
     }
 
+  print_bits (var_states.get (dest));
   return true;
 }
 
@@ -1540,11 +1594,12 @@ state::do_mem_ref (tree arg1, tree dest)
 bool
 state::do_pointer_plus (tree arg1, tree arg2, tree dest)
 {
-  if (!is_declared (arg1) || !is_declared (arg2) || !is_declared (dest))
+  declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+  if (!is_declared (arg1) || !is_declared (arg2))
     {
       if (dump_file && (dump_flags & TDF_DETAILS))
-	fprintf (dump_file, "Sym-Exec: For pointer addition destination"
-			    "and arguments must be declared\n");
+	fprintf (dump_file, "Sym-Exec: For pointer addition "
+			    "arguments must be declared\n");
 
       return false;
     }
@@ -1562,11 +1617,12 @@ state::do_pointer_plus (tree arg1, tree arg2, tree dest)
 bool
 state::do_pointer_diff (tree arg1, tree arg2, tree dest)
 {
-  if (!is_declared (arg1) || !is_declared (arg2) || !is_declared (dest))
+  declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+  if (!is_declared (arg1) || !is_declared (arg2))
     {
       if (dump_file && (dump_flags & TDF_DETAILS))
-	fprintf (dump_file, "Sym-Exec: For pointer subtraction destination"
-			    "and arguments must be declared\n");
+	fprintf (dump_file, "Sym-Exec: For pointer subtraction "
+			    "arguments must be declared\n");
 
       return false;
     }
@@ -1577,3 +1633,88 @@ state::do_pointer_diff (tree arg1, tree arg2, tree dest)
 
   return do_sub (arg1, arg2, dest);
 }
+
+
+vec<value *> *
+state::make_copy (vec<value *> *bits) const
+{
+  vec<value *> * copied_bits = new vec<value*> ();
+  copied_bits->create (bits->length ());
+  for (size_t i = 0; i < bits->length (); i++)
+    copied_bits->quick_push ((*bits)[i]->copy ());
+
+  return copied_bits;
+}
+
+
+condition_status
+state::get_last_cond_status ()
+{
+  return last_cond_status;
+}
+
+
+void
+state::print_bits (vec<value *> * bits)
+{
+  if (!dump_file || !(dump_flags & TDF_DETAILS))
+    return;
+
+  fprintf (dump_file, "{");
+  for (int i = bits->length () - 1; i >= 0; i--)
+    {
+      (*bits)[i]->print ();
+
+      if (i)
+	fprintf (dump_file, ", ");
+    }
+  fprintf (dump_file, "}\n");
+}
+
+
+
+size_t min (size_t a, size_t b, size_t c)
+{
+  size_t min = (a < b ? a : b);
+  return min < c ? min : c;
+}
+
+
+/* Casts arg_bits to cast_size size, stores value in dest.  */
+
+bool
+state::do_cast (tree var, tree dest, size_t cast_size)
+{
+  declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+  if (!is_declared (var))
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Sym-Exec: For cast operantion "
+			    "argument must be declared\n");
+
+      return false;
+    }
+
+  //TODO: add case for signed numbers
+
+  vec<value *> *arg = var_states.get (var);
+  vec<value *> *dest_bits = var_states.get (dest);
+
+  size_t arg_size = min (arg->length (), dest_bits->length (), cast_size);
+
+  for (size_t i = 0; i < arg_size; i++)
+    {
+      value *temp = (*dest_bits)[i];
+      (*dest_bits)[i] = (*arg)[i]->copy ();
+      delete temp;
+    }
+
+  value * sign_bit = arg->last ();
+  for (size_t i = arg_size; i < dest_bits->length (); i++)
+    {
+      value *temp = (*dest_bits)[i];
+      (*dest_bits)[i] = sign_bit->copy ();
+      delete temp;
+    }
+  return true;
+}
diff --git a/gcc/sym-exec/state.h b/gcc/sym-exec/state.h
index f074a9a63a2..c2f53ce9077 100644
--- a/gcc/sym-exec/state.h
+++ b/gcc/sym-exec/state.h
@@ -6,27 +6,6 @@
 #ifndef SYM_EXEC_STATE_H
 #define SYM_EXEC_STATE_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"
-#include "hash-set.h"
-#include "expression.h"
 #include "expression-is-a-helper.h"
 
 
@@ -43,42 +22,64 @@ class state {
   /* Here is stored values of bit of each variable.  */
   hash_map<tree, vec < value * >> var_states;
 
+  /* Here is stored conditions of symbolic bits.  */
   hash_set<bit_expression *> conditions;
 
-  /* Performs AND operation on two bits.  */
-  value * and_two_bits (value *var1, value* var2) const;
+  /* The result of last added condition.  */
+  condition_status last_cond_status = condition_status::CS_NO_COND;
 
+  /* Creates bit sequence of given constant tree.  */
   vec<value*> create_bits_for_const (tree var, size_t size) const;
 
+  /* Removes given sequence of bits.  */
   void free_bits (vec<value*> * bits) const;
 
+  /* Checks if sizes of arguments and destination are compatible.  */
   bool check_args_compatibility (tree arg1, tree arg2, tree dest);
 
+  /* Adds equality condition for two sequences of bits.  */
   void add_equal_cond (vec<value*> * arg1_bits, vec<value*> * arg2_bits);
 
+  /* Adds not equal condition for two sequences of bits.  */
   void add_not_equal_cond (vec<value*> * arg1_bits, vec<value*> * arg2_bits);
 
+  /* Adds greater than condition for two sequences of bits.  */
   void add_greater_than_cond (vec<value*> * arg1_bits, vec<value*> * arg2_bits);
 
+  /* Adds less than condition for two sequences of bits.  */
   void add_less_than_cond (vec<value*> * arg1_bits, vec<value*> * arg2_bits);
 
+  /* Adds greater or equal condition for two sequences of bits.  */
   void add_greater_or_equal_cond (vec<value*> * arg1_bits,
 				  vec<value*> * arg2_bits);
 
+  /* Adds less or equal condition for two sequences of bits.  */
   void add_less_or_equal_cond (vec<value*> * arg1_bits,
 			       vec<value*> * arg2_bits);
 
+  /* Does preprocessing and postprocessing for condition adding.
+     Handles bit sequence creation for constant values
+     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 sequences of bits.  */
   bit_expression* construct_great_than_cond (vec<value*> * arg1_bits,
 					     vec<value*> * arg2_bits);
 
+  /* Constructs expression trees of less than condition
+     for given sequences of bits.  */
   bit_expression* construct_less_than_cond (vec<value*> * arg1_bits,
 					    vec<value*> * arg2_bits);
 
+  /* Constructs expression trees of equal condition
+     for given sequences of bits.  */
   bit_expression* construct_equal_cond (vec<value*> * arg1_bits,
 					vec<value*> * arg2_bits);
 
+  /* Does preprocessing and postprocessing for expressions with tree operands.
+     Handles bit sequence creation for constant values
+     and their removement in the end.  */
   bool do_binary_operation (tree arg1, tree arg2, tree dest,
 			    binary_func bin_func);
 
@@ -98,6 +99,15 @@ class state {
 
   void do_sub (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest);
 
+  /* Casts arg_bits to cast_size size, stores value in dest.  */
+  bool do_cast (tree arg, tree dest, size_t cast_size);
+
+  /* Performs AND operation on two bits.  */
+  value *and_two_bits (value *arg1_bit, value* arg2_bit) const;
+
+  /* ANDs every bit of the vector with var_bit, stroes the result in var1.  */
+  void and_number_bit (vec<value *> *var1, value *var_bit);
+
   void do_mul (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest);
 
   /* Performs AND operation for 2 symbolic_bit operands.  */
@@ -110,7 +120,7 @@ class state {
   bit *and_const_bits (const bit * const_bit1, const bit * const_bit2) const;
 
   /* Performs OR operation on two bits.  */
-  value * or_two_bits (value *var1, value* var2) const;
+  value *or_two_bits (value *arg1_bit, value* arg2_bit) const;
 
   /* Performs OR operation for 2 symbolic_bit operands.  */
   value *or_sym_bits (const value * var1, const value * var2) const;
@@ -168,14 +178,11 @@ class state {
   void declare_if_needed (tree var, size_t size);
 
  /* Shifts value_vector left by shift_value bits.  */
-  vec <value *> *shift_left_by_const (const vec <value *> *arg_vector,
+  vec <value *> *shift_left_by_const (const vec <value *> * number,
 				      size_t shift_value);
 
   /* Checks if all vector elements are const_bit_expressions.  */
-  bool is_bit_vector (const vec <value *> *value_vector);
-
-  /* returns the value of the number represented as a bit vector.  */
-  size_t get_value (const vec <value *> *bit_vector);
+  bool is_bit_vector (const vec <value *> *bits);
 
   /* Adds two bits and carry value.
      Resturn result and stores new carry bit in "carry".  */
@@ -184,11 +191,10 @@ class state {
   /* Returns the additive inverse of the number stored in number verctor.  */
   vec <value *> * additive_inverse (const vec <value *> *number);
 
-  /* ANDs every bit of the vector with var_bit, stroes the result in var1.  */
-  void and_number_bit (vec<value *> *var1, value *var_bit);
-
   /* Adds two vectors, stores the result in the first one.  */
-  void add_numbers (vec< value * > *var1, const vec< value * > *var2);
+  void add_numbers (vec<value *> *var1, const vec<value *> *var2);
+
+  vec<value *> * make_copy (vec<value *> *bits) const;
 
  public:
    state ();
@@ -221,6 +227,11 @@ class state {
   /* Returns size of the given variable.  */
   unsigned get_var_size (tree var);
 
+  static void print_bits (vec<value *> * bits);
+
+  /* returns the value of the number represented as a bit vector.  */
+  static unsigned HOST_WIDE_INT get_value (const vec <value *> *bit_vector);
+
   /* Does bit-level XOR operation for given variables.  */
   bool do_xor (tree arg1, tree arg2, tree dest);
 
@@ -232,6 +243,9 @@ class state {
 
   bool do_assign (tree arg, tree dest);
 
+  /* Assigns pow 2 value.  */
+  bool do_assign_pow2 (tree dest, unsigned pow);
+
   /* Does shift_left operation for given variables.  */
   bool do_shift_left (tree arg1, tree arg2, tree dest);
 
@@ -284,6 +298,9 @@ class state {
 
   bool check_const_bit_is_less_than (vec<value *> * arg1_bits,
 				     vec<value *> * arg2_bits) const;
+
+  /* Returns status of last added condition.  */
+  condition_status get_last_cond_status ();
 };
 
 #endif /* SYM_EXEC_STATE_H.  */