]> gcc.gnu.org Git - gcc.git/commitdiff
sym-exec v3: - Refactored code and fixed style - Added util functions - Fixed express...
authormatevos <matevosmehrabyan@gmail.com>
Fri, 18 Nov 2022 14:30:18 +0000 (18:30 +0400)
committerJeff Law <jlaw@ventanamicro>
Tue, 21 Mar 2023 15:03:18 +0000 (09:03 -0600)
gcc/sym-exec/expression.cc
gcc/sym-exec/expression.h
gcc/sym-exec/state.cc
gcc/sym-exec/state.h
gcc/symb-execute-all-paths.cc
gcc/symb-execute-all-paths.h

index 5bf46367796130d68df568642325515eec2ab2fd..8b9a1feb6e71a0bec5c89a7fc04a96c3e62d9fbe 100644 (file)
@@ -63,6 +63,22 @@ bit_complement_expression::bit_complement_expression (value *right)
 }
 
 
+bit_complement_expression::bit_complement_expression (
+       const bit_complement_expression& expr)
+{
+  bit_expression::copy (&expr);
+}
+
+
+bit_expression::~bit_expression ()
+{
+  delete left;
+  left = nullptr;
+  delete right;
+  right = nullptr;
+}
+
+
 value*
 symbolic_bit::copy () const
 {
@@ -144,13 +160,6 @@ bit_complement_expression::copy () const
 }
 
 
-bit_complement_expression::bit_complement_expression (
-       const bit_complement_expression& expr)
-{
-  bit_expression::copy (&expr);
-}
-
-
 bit_xor_expression::bit_xor_expression (value *left, value *right)
 {
   this->left = left;
index 45c327599daf8af094df37bf35821ce81d9d6d85..25a85aa5e0dec5c58362a7d06b0433f9a9ba605e 100644 (file)
@@ -94,6 +94,8 @@ class bit_expression : public value {
   value *get_left ();
   value *get_right ();
 
+  ~bit_expression ();
+
   void set_left (value *expr);
   void set_right (value *expr);
   value *copy () const = 0;
index 7caffbcd87fc40590cd6c2a8ef6dabde4263a37d..7a308ea2c71e08015a3f3592ad5c480f0e0240c7 100644 (file)
 #include "vec.h"
 #include "hash-set.h"
 #include "condition.h"
-//#include "expression.h"
+
+
+state::state ()
+{
+}
+
+
+state::state (const state& s)
+{
+  for (auto iter = s.var_states.begin (); iter != s.var_states.end (); ++iter)
+    {
+      vec < value * > bits;
+      bits.create ((*iter).second.length ());
+      for (size_t i = 0; i < (*iter).second.length (); i++)
+       bits.quick_push ((*iter).second[i]->copy ());
+
+      var_states.put ((*iter).first, bits);
+    }
+
+  for (auto iter = s.conditions.begin (); iter != s.conditions.end (); ++iter)
+    conditions.add (as_a<bit_expression *> ((*iter)->copy ()));
+}
+
+
+state::~state ()
+{
+  clear_states ();
+  clear_conditions ();
+}
 
 
 /* Checks whether state for variable with specified name already
    exists or not.  */
 
 bool
-State::is_declared (tree var)
+state::is_declared (tree var)
 {
   return var_states.get (var) != NULL;
 }
 
 
+vec<value*> *
+state::get_bits (tree var)
+{
+  return var_states.get (var);
+}
+
+
+const hash_set<bit_expression *>&
+state::get_conditions ()
+{
+  return conditions;
+}
+
+
+void
+state::check_args_compatibility (tree arg1, tree arg2, tree dest)
+{
+  gcc_assert ((is_declared (arg1) || TREE_CODE (arg1) == INTEGER_CST)
+             && (is_declared (arg2) || TREE_CODE (arg2) == INTEGER_CST)
+             && is_declared (dest));
+  gcc_assert ((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));
+}
+
+
+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;
+    }
+
+  return bits;
+}
+
+
+void
+state::free_bits (vec<value*> * bits) const
+{
+  if (bits == nullptr || !bits->exists ())
+    return;
+
+  for (size_t i = 0; i < bits->length (); i++)
+    {
+      delete (*bits)[i];
+      (*bits)[i] = nullptr;
+    }
+}
+
+
+bool
+state::add_var_state (tree var, vec<value*> * vstate)
+{
+  vec<value* > bits;
+  bits.create (vstate->length ());
+  for (size_t i = 0; i < vstate->length (); i++)
+    bits.quick_push ((*vstate)[i]->copy ());
+
+  free_bits (var_states.get (var));
+  return var_states.put (var, bits);
+}
+
+
+bool
+state::add_condition (bit_expression* cond)
+{
+  return conditions.add (as_a<bit_expression*> (cond->copy ()));
+}
+
+
+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;
+}
+
+
+void
+state::clear_states ()
+{
+  for (auto iter = var_states.begin (); iter != var_states.end (); ++iter)
+    {
+      vec < value * > *bits = &(*iter).second;
+      for (size_t i = 0; i < bits->length (); i++)
+       delete (*bits)[i];
+    }
+
+  var_states.empty ();
+}
+
+
+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 *
-State::and_sym_bits (const value * var1, const value * var2) const
+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
+state::and_var_const (const value * var1, const bit * const_bit) const
 {
   if (const_bit->get_val () == 1)
     return var1->copy ();
@@ -43,7 +185,7 @@ State::and_var_const (const value * var1, const bit * const_bit) const
 /* performs AND operation for 2 constant bit operands.  */
 
 bit *
-State::and_const_bits (const bit * const_bit1, const bit * const_bit2) const
+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);
@@ -55,15 +197,16 @@ State::and_const_bits (const bit * const_bit1, const bit * const_bit2) const
 /* performs OR operation for 2 symbolic_bit operands.  */
 
 value *
-State::or_sym_bits (const value * var1, const value * var2) const
+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
+state::or_var_const (const value * var1, const bit * const_bit) const
 {
   if (const_bit->get_val () == 0)
     return var1->copy ();
@@ -71,10 +214,11 @@ State::or_var_const (const value * var1, const bit * const_bit) const
   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
+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);
@@ -86,7 +230,7 @@ State::or_const_bits (const bit * const_bit1, const bit * const_bit2) const
 /* Adds an empty state for the given variable.  */
 
 bool
-State::decl_var (tree var, unsigned size)
+state::decl_var (tree var, unsigned size)
 {
   if (is_declared (var))
     return false;
@@ -103,7 +247,7 @@ State::decl_var (tree var, unsigned size)
 /* Returns size of the given variable.  */
 
 unsigned
-State::get_var_size (tree var)
+state::get_var_size (tree var)
 {
   vec < value * > *content = var_states.get (var);
   if (content == NULL)
@@ -117,7 +261,7 @@ State::get_var_size (tree var)
    represented as sequence of symbolic bits.  */
 
 bool
-State::make_symbolic (tree var, unsigned size)
+state::make_symbolic (tree var, unsigned size)
 {
   if (is_declared (var))
     return false;
@@ -133,139 +277,181 @@ State::make_symbolic (tree var, unsigned size)
 }
 
 
+void
+state::do_binary_operation (tree arg1, tree arg2, tree dest,
+                           binary_func bin_func)
+{
+  check_args_compatibility (arg1, arg2, dest);
+  vec<value*> * arg1_bits = var_states.get (arg1);
+  vec<value*> arg1_const_bits (vNULL);
+  if (arg1_bits == NULL && TREE_CODE (arg1) == INTEGER_CST)
+    {
+      arg1_const_bits = create_bits_for_const (arg1,
+                               var_states.get (dest)->length ());
+      arg1_bits = &arg1_const_bits;
+    }
+
+  vec<value*> * arg2_bits = var_states.get (arg2);
+  vec<value*> arg2_const_bits (vNULL);
+  if (arg2_bits == NULL && TREE_CODE (arg2) == INTEGER_CST)
+    {
+      arg2_const_bits = create_bits_for_const (arg2,
+                               var_states.get (dest)->length ());
+      arg2_bits = &arg2_const_bits;
+    }
+
+  (this->*bin_func)(arg1_bits, arg2_bits, dest);
+  free_bits (&arg1_const_bits);
+  free_bits (&arg2_const_bits);
+}
+
+
 /* Does bit-level AND operation for given variables.  */
 
 void
-State::do_and (tree arg1, tree arg2, tree dest)
+state::do_and (tree arg1, tree arg2, tree dest)
 {
-  gcc_assert (!(is_declared (arg1) || is_declared (arg2)
-               || is_declared (dest)));
-  gcc_assert (get_var_size (arg1) == get_var_size (dest)
-             && get_var_size (arg2) == get_var_size (dest));
+  do_binary_operation (arg1, arg2, dest, &state::do_and);
+}
 
+
+void
+state::do_and (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree 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 * arg1_bit = (*var_states.get (arg1))[i];
-    value * arg2_bit = (*var_states.get (arg2))[i];
+    {
+      value *result = nullptr;
+      value *arg1_bit = (*arg1_bits)[i];
+      value *arg2_bit = (*arg2_bits)[i];
 
-    if (is_a<bit *> (arg1_bit) && is_a<bit *> (arg2_bit))
-      result = and_const_bits (as_a<bit *> (arg1_bit), as_a<bit *> (arg2_bit));
+      if (is_a<bit *> (arg1_bit) && is_a<bit *> (arg2_bit))
+       result = and_const_bits (as_a<bit *> (arg1_bit),
+                                as_a<bit *> (arg2_bit));
 
-    else if (is_a<bit *> (arg1_bit) && (is_a<symbolic_bit *> (arg2_bit)
-                                       || (is_a<bit_expression *> (arg2_bit))))
-      result = and_var_const (arg2_bit, as_a<bit *> (arg1_bit));
+      else if (is_a<bit *> (arg1_bit)
+              && (is_a<symbolic_bit *> (arg2_bit)
+                  || (is_a<bit_expression *> (arg2_bit))))
+       result = and_var_const (arg2_bit, as_a<bit *> (arg1_bit));
 
-    else if ((is_a<symbolic_bit *> (arg1_bit)
-             || (is_a<bit_expression *> (arg1_bit))) && is_a<bit *> (arg2_bit))
-      result = and_var_const (arg1_bit, as_a<bit *> (arg2_bit));
+      else if ((is_a<symbolic_bit *> (arg1_bit)
+               || (is_a<bit_expression *> (arg1_bit)))
+              && is_a<bit *> (arg2_bit))
+       result = and_var_const (arg1_bit, as_a<bit *> (arg2_bit));
 
-    else
-      result = and_sym_bits (arg1_bit, arg2_bit);
+      else
+       result = and_sym_bits (arg1_bit, arg2_bit);
 
-    delete (*var_states.get (dest))[i];
-    (*var_states.get (dest))[i] = result;
-  }
+      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)
+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));
+  do_binary_operation (arg1, arg2, dest, &state::do_or);
+}
 
+
+void
+state::do_or (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest)
+{
   /* Creating OR expressions for every bit pair of given arguments
-   and store them as a new state for given destination.  */
+     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 * arg1_bit = (*var_states.get (arg1))[i];
-    value * arg2_bit = (*var_states.get (arg2))[i];
+    {
+      value *result = nullptr;
+      value *arg1_bit = (*arg1_bits)[i];
+      value *arg2_bit = (*arg2_bits)[i];
 
-    if (is_a<bit *> (arg1_bit) && is_a<bit *> (arg2_bit))
-      result = or_const_bits (as_a<bit *> (arg1_bit), as_a<bit *> (arg2_bit));
+      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<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 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);
+      else
+       result = or_sym_bits (arg1_bit, arg2_bit);
 
-    delete (*var_states.get (dest))[i];
-    (*var_states.get (dest))[i] = result;
-  }
+      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)
+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));
+  do_binary_operation (arg1, arg2, dest, &state::do_xor);
+}
+
 
+void
+state::do_xor (vec<value*> * arg1_bits, vec<value *> * arg2_bits, tree dest)
+{
   for (size_t i = 0; i < get_var_size (dest); i++)
-  {
-    value *result = nullptr;
-    value * arg1_bit = (*var_states.get (arg1))[i];
-    value * arg2_bit = (*var_states.get (arg2))[i];
+    {
+      value *result = nullptr;
+      value *arg1_bit = (*arg1_bits)[i];
+      value *arg2_bit = (*arg2_bits)[i];
 
-    if (is_a<bit *> (arg1_bit) && is_a<bit *> (arg2_bit))
-      result = xor_const_bits (as_a<bit *> (arg1_bit), as_a<bit *> (arg2_bit));
+      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<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 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);
+      else
+       result = xor_sym_bits (arg1_bit, arg2_bit);
 
-    delete (*var_states.get (dest))[i];
-    (*var_states.get (dest))[i] = result;
-  }
+      delete (*var_states.get (dest))[i];
+      (*var_states.get (dest))[i] = result;
+    }
 }
 
 
 /* Shifts value_vector right by shift_value bits.  */
 
 vec <value *>
-State::shift_right_by_const (const vec <value *> * value_vector,
+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);
+  if (value_vector->length () <= shift_value)
+    for (size_t i = 0; i < value_vector->length (); i++)
+      shift_result.quick_push (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);
-  }
+    {
+      size_t i = 0;
+      for (; i < value_vector->length () - shift_value; ++i)
+       shift_result.quick_push (((*value_vector)[shift_value + i])->copy ());
+
+      for (; i < value_vector->length (); ++i)
+       shift_result.quick_push (new bit (0));
+    }
   return shift_result;
 }
 
@@ -273,7 +459,7 @@ State::shift_right_by_const (const vec <value *> * value_vector,
 /* Checks if all vector elements are const_bit_expressions.  */
 
 bool
-State::is_bit_vector (vec <value *>* value_vector)
+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])))
@@ -285,14 +471,14 @@ State::is_bit_vector (vec <value *>* value_vector)
 /* Returns the value of the number represented as a bit vector.  */
 
 size_t
-State::get_value (vec <value *> * bit_vector)
+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;
-  }
+    {
+      bit *cur_elem = dyn_cast<bit *> ((*bit_vector)[i]);
+      number = (number | cur_elem->get_val ()) << 1;
+    }
 
   return number;
 }
@@ -301,143 +487,187 @@ State::get_value (vec <value *> * bit_vector)
 /* shift_left operation.  Case: var2 is a sym_bit.  */
 
 void
-State::shift_left_sym_bits (tree var1, tree var2, tree dest)
+state::shift_left_sym_bits (vec<value*> * arg1_bits, vec<value*> * arg2_bits,
+                           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;
-  }
+    {
+      value *var1_elem = (*arg1_bits)[i];
+      value *var2_elem = (*arg2_bits)[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)
+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));
+  do_binary_operation (arg1, arg2, dest, &state::do_shift_left);
+}
+
 
-  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++)
+void
+state::do_shift_left (vec<value*> * arg1_bits, vec<value*> * arg2_bits,
+                     tree dest)
+{
+  if (is_bit_vector (arg2_bits))
     {
-      delete (*var_states.get (dest))[i];
-      (*var_states.get (dest))[i] = result[i];
+      size_t shift_value = get_value (arg2_bits);
+      vec < value * > result = shift_left_by_const (arg1_bits, 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);
+    shift_left_sym_bits (arg1_bits, arg2_bits, dest);
 }
 
 
+
 /* Does shift_right operation for given variables.  */
 
 void
-State::do_shift_right (tree arg1, tree arg2, tree dest)
+state::do_shift_right (tree arg1, tree arg2, tree dest)
 {
-  gcc_assert (!(is_declared (arg1) || is_declared (arg2)
-               || is_declared (dest)));
-  gcc_assert (get_var_size (arg1) == get_var_size (dest)
-             && get_var_size (arg2) == get_var_size (dest));
+  do_binary_operation (arg1, arg2, dest, &state::do_shift_right);
+}
 
+
+void
+state::do_shift_right (vec<value*> * arg1_bits, vec<value*> * arg2_bits,
+                      tree dest)
+{
   /* TODO: Add support for signed var shift.  */
-  if (is_bit_vector (var_states.get (arg2)))
-  {
-    size_t shift_value = get_value (var_states.get (arg2));
-    vec <value *> result = shift_right_by_const (var_states.get (arg1),
-                                                shift_value);
-    for (size_t i = 0; i < get_var_size (dest); i++)
+  if (is_bit_vector (arg2_bits))
     {
-      delete (*var_states.get (dest))[i];
-      (*var_states.get (dest))[i] = result[i];
+      size_t shift_value = get_value (arg2_bits);
+      vec < value * > result = shift_right_by_const (arg1_bits, 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);
+    shift_right_sym_bits (arg1_bits, arg2_bits, dest);
 }
 
 
 /* Adds two variables.  */
 
 void
-State::do_add (tree arg1, tree arg2, tree dest)
+state::do_add (tree arg1, tree arg2, tree dest)
 {
-  gcc_assert (!(is_declared (arg1) || is_declared (arg2)
-               || is_declared (dest)));
-  gcc_assert (get_var_size (dest)
-             == (get_var_size (arg1) > get_var_size (arg2)
-                 ? get_var_size (arg1) : get_var_size (arg2)));
+  do_binary_operation (arg1, arg2, dest, &state::do_add);
+}
+
 
+void
+state::do_add (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest)
+{
   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;
-  }
+    {
+      value *new_val = new add_expression ((*arg1_bits)[i]->copy (),
+                                          (*arg2_bits)[i]->copy ());
+      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)
+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));
+  do_binary_operation (arg1, arg2, dest, &state::do_sub);
+}
+
 
+void
+state::do_sub (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree 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;
-  }
+    {
+      value *new_val = new sub_expression ((*arg1_bits)[i]->copy (),
+                                          (*arg2_bits)[i]->copy ());
+      delete (*var_states.get (dest))[i];
+      (*var_states.get (dest))[i] = new_val;
+    }
 }
 
 
 /* Negates given variable.  */
 
 void
-State::do_complement (tree arg, tree dest)
+state::do_complement (tree arg, tree dest)
 {
-  gcc_assert (!(is_declared (arg) || is_declared (dest)));
+  gcc_assert (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]);
+    {
+      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;
-  }
+      delete (*var_states.get (dest))[i];
+      (*var_states.get (dest))[i] = result;
+    }
+}
+
+
+void
+state::do_assign (tree arg, tree dest)
+{
+  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))
+    {
+      for (size_t i = 0; i < dest_bits->length (); i++)
+       {
+         value *new_val = nullptr;
+         if (i < bits->length ())
+           new_val = (*bits)[i]->copy ();
+         else
+           new_val = new bit (0);
+
+         delete (*dest_bits)[i];
+         (*dest_bits)[i] = new_val;
+       }
+    }
+  /* 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
+      = create_bits_for_const (arg, dest_bits->length ());
+      for (size_t i = 0; i < dest_bits->length (); i++)
+       {
+         delete (*dest_bits)[i];
+         (*dest_bits)[i] = arg_bits[i];
+       }
+    }
+  else
+    gcc_assert (false);
 }
 
 
 /* Performs NOT operation for constant bit.  */
 
 bit *
-State::complement_const_bit (const bit * const_bit) const
+state::complement_const_bit (const bit * const_bit) const
 {
   return new bit (1u ^ const_bit->get_val ());
 }
@@ -446,7 +676,7 @@ State::complement_const_bit (const bit * const_bit) const
 /* Performs NOT operation for symbolic_bit.  */
 
 value *
-State::complement_sym_bit (const value * var) const
+state::complement_sym_bit (const value * var) const
 {
   return new bit_complement_expression (var->copy ());
 }
@@ -455,82 +685,82 @@ State::complement_sym_bit (const value * var) const
 /* Performs XOR operation for 2 symbolic_bit operands.  */
 
 value *
-State::xor_sym_bits (const value * var1, const value * var2) const
+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 both subtrees have constant bit nodes, we can merge them together.  */
-    if (var1_node_with_const_child != nullptr)
     {
-      /* If var1's const bit is in its left subtree.  */
-      value * var1_left = var1_node_with_const_child->get_left ();
-      if (var1_left != nullptr && is_a<bit *> (var1_left))
-      {
-       /* If var2's const bit is in its left subtree.  */
-       value * var2_left = var2_node_with_const_child->get_left ();
-       if (var2_left != nullptr && is_a<bit *> (var2_left))
-       {
-         bit * new_left = xor_const_bits (as_a<bit *> (var1_left),
-                                          as_a<bit *> (var2_left));
-         delete var2_left;
-         var2_node_with_const_child->set_left (nullptr);
-
-         delete var1_left;
-         var1_node_with_const_child->set_left (new_left);
-       }
-       else /* Var2's const bit is in its right subtree.  */
-       {
-         value * var2_right = var2_node_with_const_child->get_right ();
-         bit * new_left = xor_const_bits (as_a<bit *> (var1_left),
-                                          as_a<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 /* Var1's const bit is in its right subtree.  */
-      {
-       value * var1_right = var1_node_with_const_child->get_right ();
-       value * var2_left = var2_node_with_const_child->get_left ();
-       /* If var2's const bit is in its left subtree.  */
-       if (var2_left != nullptr && is_a<bit *> (var2_left))
-       {
-         bit * new_right = xor_const_bits (as_a<bit *> (var1_left),
-                                           as_a<bit *> (var2_left));
-         delete var2_left;
-         var2_node_with_const_child->set_left (nullptr);
+      value *var1_copy = var1->copy ();
+      bit_expression *var1_node_with_const_child
+       = get_parent_with_const_child (var1_copy);
 
-         delete var1_right;
-         var1_node_with_const_child->set_right (new_right);
-       }
-       else /* Var2's const bit is in its right subtree.  */
+      /* If both subtrees have constant bit nodes,
+        we can merge them together.  */
+      if (var1_node_with_const_child != nullptr)
        {
-         value * var2_right = var2_node_with_const_child->get_right ();
-         bit * new_right = xor_const_bits (as_a<bit *> (var1_right),
-                                           as_a<bit *> (var2_right));
-         delete var2_right;
-         var2_node_with_const_child->set_right (nullptr);
-
-         delete var1_right;
-         var1_node_with_const_child->set_right (new_right);
+         /* If var1's const bit is in its left subtree.  */
+         value *var1_left = var1_node_with_const_child->get_left ();
+         if (var1_left != nullptr && is_a<bit *> (var1_left))
+           {
+             /* If var2's const bit is in its left subtree.  */
+             value *var2_left = var2_node_with_const_child->get_left ();
+             if (var2_left != nullptr && is_a<bit *> (var2_left))
+               {
+                 bit *new_left = xor_const_bits (as_a<bit *> (var1_left),
+                                                 as_a<bit *> (var2_left));
+                 delete var2_left;
+                 var2_node_with_const_child->set_left (nullptr);
+
+                 delete var1_left;
+                 var1_node_with_const_child->set_left (new_left);
+               }
+             else /* Var2's const bit is in its right subtree.  */
+               {
+                 value *var2_right = var2_node_with_const_child->get_right ();
+                 bit *new_left = xor_const_bits (as_a<bit *> (var1_left),
+                                                 as_a<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 /* Var1's const bit is in its right subtree.  */
+           {
+             value *var1_right = var1_node_with_const_child->get_right ();
+             value *var2_left = var2_node_with_const_child->get_left ();
+             /* If var2's const bit is in its left subtree.  */
+             if (var2_left != nullptr && is_a<bit *> (var2_left))
+               {
+                 bit *new_right = xor_const_bits (as_a<bit *> (var1_left),
+                                                  as_a<bit *> (var2_left));
+                 delete var2_left;
+                 var2_node_with_const_child->set_left (nullptr);
+
+                 delete var1_right;
+                 var1_node_with_const_child->set_right (new_right);
+               }
+             else /* Var2's const bit is in its right subtree.  */
+               {
+                 value *var2_right = var2_node_with_const_child->get_right ();
+                 bit *new_right = xor_const_bits (as_a<bit *> (var1_right),
+                                                  as_a<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);
        }
-      }
-
-      return new bit_xor_expression (var1_copy, var2_copy);
+      delete var1_copy;
     }
-    delete var1_copy;
-  }
 
   delete var2_copy;
   return new bit_xor_expression (var1->copy (), var2->copy ());
@@ -540,7 +770,7 @@ State::xor_sym_bits (const value * var1, const value * var2) const
 /* Performs XOR operation for 2 constant bit operands.  */
 
 bit *
-State::xor_const_bits (const bit * const_bit1, const bit * const_bit2) const
+state::xor_const_bits (const bit * const_bit1, const bit * const_bit2) const
 {
   return new bit (const_bit1->get_val () ^ const_bit2->get_val ());
 }
@@ -549,29 +779,29 @@ State::xor_const_bits (const bit * const_bit1, const bit * const_bit2) const
 /* Performs XOR operation for a symbolic_bit and const_bit operands.  */
 
 value *
-State::xor_var_const (const value * var, const bit * const_bit) const
+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);
+  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 && 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 * 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);
+      value *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 *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;
     }
-    return var_copy;
-  }
 
   delete var_copy;
   return new bit_xor_expression (var->copy (), const_bit->copy ());
@@ -582,7 +812,7 @@ State::xor_var_const (const value * var, const bit * const_bit) const
    on safe branching.  */
 
 bit_expression *
-State::get_parent_with_const_child (value* root) const
+state::get_parent_with_const_child (value* root) const
 {
   if (! is_a<bit_expression *> (root))
     return nullptr;
@@ -594,23 +824,23 @@ State::get_parent_with_const_child (value* root) const
   /* 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);
+    {
+      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 ();
+      value *left = cur_element->get_left ();
+      value *right = cur_element->get_right ();
 
-    if ((left != nullptr && is_a<bit *> (left))
-       || (right != nullptr && is_a<bit *> (right)))
-      return cur_element;
+      if ((left != nullptr && is_a<bit *> (left))
+         || (right != nullptr && is_a<bit *> (right)))
+       return cur_element;
 
-    if (left != nullptr && is_safe_branching (left))
-      nodes_to_consider.add (as_a<bit_expression *> (left));
+      if (left != nullptr && is_safe_branching (left))
+       nodes_to_consider.add (as_a<bit_expression *> (left));
 
-    if (right != nullptr && is_safe_branching (right))
-      nodes_to_consider.add (as_a<bit_expression *> (right));
-  }
+      if (right != nullptr && is_safe_branching (right))
+       nodes_to_consider.add (as_a<bit_expression *> (right));
+    }
   return nullptr;
 }
 
@@ -618,7 +848,7 @@ State::get_parent_with_const_child (value* root) const
 /* Checks if node is AND, OR or XOR expression as they are comutative.  */
 
 bool
-State::is_safe_branching (value* node) const
+state::is_safe_branching (value* node) const
 {
   return is_a<bit_and_expression *> (node) || is_a<bit_or_expression *> (node)
         || is_a<bit_xor_expression *> (node);
@@ -628,23 +858,23 @@ State::is_safe_branching (value* node) const
 /* Shifts value_vector left by shift_value bits.  */
 
 vec <value *>
-State::shift_left_by_const (const vec < value * > * value_vector,
+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);
+  if (value_vector->length () <= shift_value)
+    for (size_t i = 0; i < value_vector->length (); i++)
+      shift_result.quick_push (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 ();
-  }
+    {
+      size_t i = 0;
+      for (; i < value_vector->length () - shift_value; ++i)
+       shift_result.quick_push (new bit (0));
+
+      for (size_t j = 0; i < value_vector->length (); ++i, ++j)
+       shift_result.quick_push (((*value_vector)[j])->copy ());
+    }
   return shift_result;
 }
 
@@ -652,22 +882,23 @@ State::shift_left_by_const (const vec < value * > * value_vector,
 /* shift_right operation.  Case: var2 is a sym_bit.  */
 
 void
-State::shift_right_sym_bits (tree var1, tree var2, tree dest)
+state::shift_right_sym_bits (vec<value*> * arg1_bits, vec<value*> * arg2_bits,
+                            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;
-  }
+    {
+      value *var1_elem = (*arg1_bits)[i];
+      value *var2_elem = (*arg2_bits)[i];
+      value *new_elem = new shift_right_expression (var1_elem->copy (),
+                                                   var2_elem->copy ());
+      delete (*var_states.get (dest))[i];
+      (*var_states.get (dest))[i] = new_elem;
+    }
 }
 
 
 bool
-State::check_const_bit_equality (vec<value *> * arg1_bits,
+state::check_const_bit_equality (vec<value *> * arg1_bits,
                                 vec<value *> * arg2_bits) const
 {
   for (size_t i = 1; i < arg1_bits->length (); i++)
@@ -678,46 +909,48 @@ State::check_const_bit_equality (vec<value *> * arg1_bits,
 
 
 void
-State::add_equal_cond (tree arg1, tree arg2)
+state::add_equal_cond (tree arg1, tree arg2)
 {
   vec<value *> * arg1_bits = var_states.get (arg1);
-  vec<value *> * arg2_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg2);
 
   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
+    {
+      bool result = check_const_bit_equality (arg1_bits, arg2_bits);
+      conditions.add (new bit_condition (nullptr, nullptr,
+                                        result ? condition_type::IS_TRUE
                                                : condition_type::IS_FALSE));
-    return;
-  }
+      return;
+    }
   else if (is_bit_vector (arg1_bits) && TREE_CODE (arg2) == INTEGER_CST
           && (integer_onep (arg2) || integer_zerop (arg2)))
-  {
-    size_t i = 0;
-    if (integer_onep (arg2))
     {
-      conditions.add (new bit_condition ((*arg1_bits)[0]->copy (), new bit (1),
-                                        condition_type::EQUAL));
-      i++;
-    }
+      size_t i = 0;
+      if (integer_onep (arg2))
+       {
+         conditions.add (new bit_condition ((*arg1_bits)[0]->copy (),
+                                            new bit (1),
+                                            condition_type::EQUAL));
+         i++;
+       }
 
-    for ( ; i < arg1_bits->length (); i++)
-      conditions.add (new bit_condition ((*arg1_bits)[i]->copy (), new bit (0),
-                                        condition_type::EQUAL));
-  }
+      for (; i < arg1_bits->length (); i++)
+       conditions.add (new bit_condition ((*arg1_bits)[i]->copy (),
+                                          new bit (0),
+                                          condition_type::EQUAL));
+    }
 
   for (size_t i = 0; i < arg1_bits->length (); i++)
-  {
-    conditions.add (new bit_condition ((*arg1_bits)[i]->copy (),
-                                      (*arg2_bits)[i]->copy (),
-                                      condition_type::EQUAL));
-  }
+    {
+      conditions.add (new bit_condition ((*arg1_bits)[i]->copy (),
+                                        (*arg2_bits)[i]->copy (),
+                                        condition_type::EQUAL));
+    }
 }
 
 
 bool
-State::check_const_bit_are_not_equal (vec<value *> * arg1_bits,
+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++)
@@ -728,149 +961,150 @@ State::check_const_bit_are_not_equal (vec<value *> * arg1_bits,
 
 
 void
-State::add_not_equal_cond (tree arg1, tree arg2)
+state::add_not_equal_cond (tree arg1, tree arg2)
 {
   vec<value *> * arg1_bits = var_states.get (arg1);
-  vec<value *> * arg2_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg2);
 
   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
+    {
+      bool result = check_const_bit_are_not_equal (arg1_bits, arg2_bits);
+      conditions.add (new bit_condition (nullptr, nullptr,
+                                        result ? condition_type::IS_TRUE
                                                : condition_type::IS_FALSE));
-    return;
-  }
+      return;
+    }
 
   /* TODO: add condition when one of arguments is symbolic.  */
 }
 
 
 bool
-State::check_const_bit_is_greater_than (vec<value *> * arg1_bits,
+state::check_const_bit_is_greater_than (vec<value *> * arg1_bits,
                                        vec<value *> * arg2_bits) const
 {
   for (int i = arg1_bits->length () - 1; i >= 0; i--)
-  {
-    if ((*arg1_bits)[i] > (*arg2_bits)[i])
-      return true;
-    else if ((*arg1_bits)[i] < (*arg2_bits)[i])
-      return false;
-  }
+    {
+      if ((*arg1_bits)[i] > (*arg2_bits)[i])
+       return true;
+      else if ((*arg1_bits)[i] < (*arg2_bits)[i])
+       return false;
+    }
   return false;
 }
 
 
 void
-State::add_greater_than_cond (tree arg1, tree arg2)
+state::add_greater_than_cond (tree arg1, tree arg2)
 {
   vec<value *> * arg1_bits = var_states.get (arg1);
-  vec<value *> * arg2_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg2);
 
   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
+    {
+      bool result = check_const_bit_is_greater_than (arg1_bits, arg2_bits);
+      conditions.add (new bit_condition (nullptr, nullptr,
+                                        result ? condition_type::IS_TRUE
                                                : condition_type::IS_FALSE));
-    return;
-  }
+      return;
+    }
 
   /* TODO: add condition when one of arguments is symbolic.  */
 }
 
 
 bool
-State::check_const_bit_is_less_than (vec<value *> * arg1_bits,
+state::check_const_bit_is_less_than (vec<value *> * arg1_bits,
                                     vec<value *> * arg2_bits) const
 {
   for (int i = arg1_bits->length () - 1; i >= 0; i--)
-  {
-    if ((*arg1_bits)[i] < (*arg2_bits)[i])
-      return true;
-    else if ((*arg1_bits)[i] > (*arg2_bits)[i])
-      return false;
-  }
+    {
+      if ((*arg1_bits)[i] < (*arg2_bits)[i])
+       return true;
+      else if ((*arg1_bits)[i] > (*arg2_bits)[i])
+       return false;
+    }
   return false;
 }
 
 
 void
-State::add_less_than_cond (tree arg1, tree arg2)
+state::add_less_than_cond (tree arg1, tree arg2)
 {
   vec<value *> * arg1_bits = var_states.get (arg1);
-  vec<value *> * arg2_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg2);
 
   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
+    {
+      bool result = check_const_bit_is_less_than (arg1_bits, arg2_bits);
+      conditions.add (new bit_condition (nullptr, nullptr,
+                                        result ? condition_type::IS_TRUE
                                                : condition_type::IS_FALSE));
-    return;
-  }
+      return;
+    }
 
   /* TODO: add condition when one of arguments is symbolic.  */
 }
 
 
 void
-State::add_greater_or_equal_cond (tree arg1, tree arg2)
+state::add_greater_or_equal_cond (tree arg1, tree arg2)
 {
   vec<value *> * arg1_bits = var_states.get (arg1);
-  vec<value *> * arg2_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg2);
 
   if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
-  {
-    bool is_greater_than = check_const_bit_is_greater_than (arg1_bits,
-                                                           arg2_bits);
-    bool is_equal = check_const_bit_equality (arg1_bits, arg2_bits);
-    conditions.add (new bit_condition (nullptr, nullptr,
-                                      (is_greater_than | is_equal)
-                                      ? condition_type::IS_TRUE
+    {
+      bool is_greater_than = check_const_bit_is_greater_than (arg1_bits,
+                                                             arg2_bits);
+      bool is_equal = check_const_bit_equality (arg1_bits, arg2_bits);
+      conditions.add (new bit_condition (nullptr, nullptr,
+                                        (is_greater_than | is_equal)
+                                        ? condition_type::IS_TRUE
                                         : condition_type::IS_FALSE));
-    return;
-  }
+      return;
+    }
 
   /* TODO: add condition when one of arguments is symbolic.  */
 }
 
 
 void
-State::add_less_or_equal_cond (tree arg1, tree arg2)
+state::add_less_or_equal_cond (tree arg1, tree arg2)
 {
   vec<value *> * arg1_bits = var_states.get (arg1);
-  vec<value *> * arg2_bits = var_states.get (arg1);
+  vec<value *> * arg2_bits = var_states.get (arg2);
 
   if (is_bit_vector (arg1_bits) && is_bit_vector (arg2_bits))
-  {
-    bool is_less_than = check_const_bit_is_less_than (arg1_bits, arg2_bits);
-    bool is_equal = check_const_bit_equality (arg1_bits, arg2_bits);
-    conditions.add (new bit_condition (nullptr, nullptr,
-                                      (is_less_than | is_equal)
-                                      ? condition_type::IS_TRUE
+    {
+      bool is_less_than = check_const_bit_is_less_than (arg1_bits, arg2_bits);
+      bool is_equal = check_const_bit_equality (arg1_bits, arg2_bits);
+      conditions.add (new bit_condition (nullptr, nullptr,
+                                        (is_less_than | is_equal)
+                                        ? condition_type::IS_TRUE
                                         : condition_type::IS_FALSE));
-    return;
-  }
+      return;
+    }
 
   /* TODO: add condition when one of arguments is symbolic.  */
 }
 
+
 void
-State::add_bool_cond (tree arg)
+state::add_bool_cond (tree arg)
 {
   vec<value *> * arg_bits = var_states.get (arg);
   condition_type result = condition_type::IS_FALSE;
   if (is_bit_vector (arg_bits))
-  {
-    for (size_t i = 0; i < arg_bits->length (); i++)
-      if ((*arg_bits)[i] != 0)
-      {
-       result = condition_type::IS_TRUE;
-       break;
-      }
-  }
+    {
+      for (size_t i = 0; i < arg_bits->length (); i++)
+       if ((*arg_bits)[i] != 0)
+         {
+           result = condition_type::IS_TRUE;
+           break;
+         }
+    }
   conditions.add (new bit_condition (nullptr, nullptr, result));
 
   /* TODO: add condition when one of arguments is symbolic.  */
-}
\ No newline at end of file
+}
index c9a0e5fd8e07eed3a84cbe92da99638073394858..3a9808c73db78d70242f26cec3e4fa16bd866c7e 100644 (file)
 #include "expression.h"
 #include "expression-is-a-helper.h"
 
+
 /* Stores states of variables' values on bit-level.  */
 
-class State {
+class state {
+ typedef void (state::*binary_func) (vec<value*> * arg1_bits,
+                                    vec<value*> * arg2_bits, tree dest);
+
  private:
   /* Here is stored values of bit of each variable.  */
   hash_map<tree, vec < value * >> var_states;
 
   hash_set<bit_expression *> conditions;
 
+  vec<value*> create_bits_for_const (tree var, size_t size) const;
+
+  void free_bits (vec<value*> * bits) const;
+
+  void check_args_compatibility (tree arg1, tree arg2, tree dest);
+
+  void do_binary_operation (tree arg1, tree arg2, tree dest,
+                           binary_func bin_func);
+
+  void do_and (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest);
+
+  void do_or (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest);
+
+  void do_xor (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest);
+
+  void do_shift_right (vec<value*> * arg1_bits, vec<value*> * arg2_bits,
+                      tree dest);
+
+  void do_shift_left (vec<value*> * arg1_bits, vec<value*> * arg2_bits,
+                     tree dest);
+
+  void do_add (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest);
+
+  void do_sub (vec<value*> * arg1_bits, vec<value*> * arg2_bits, tree dest);
+
   /* Performs AND operation for 2 symbolic_bit operands.  */
   value *and_sym_bits (const value * var1, const value * var2) const;
 
@@ -71,6 +100,18 @@ class State {
   /* Performs XOR operation for a symbolic_bit and const_bit operands.  */
   value *xor_var_const (const value * var, const bit * const_bit) const;
 
+  /* shift_right operation.  Case: var2 is a sym_bit.  */
+  void shift_right_sym_bits (vec<value*> * arg1_bits, vec<value*> * arg2_bits,
+                            tree dest);
+
+  /* shift_left operation.  Case: var2 is a sym_bit.  */
+  void shift_left_sym_bits (vec<value*> * arg1_bits, vec<value*> * arg2_bits,
+                           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);
+
   /* 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;
@@ -83,9 +124,29 @@ class State {
   bool is_declared (tree var);
 
  public:
+   state ();
+
+  ~state ();
+
   /* Adds an empty state for the given variable.  */
   bool decl_var (tree name, unsigned size);
 
+  state (const state& s);
+
+  bool add_var_state (tree var, vec<value*> * state);
+
+  void clear_states ();
+
+  void clear_conditions ();
+
+  bool add_condition (bit_expression* cond);
+
+  bool bulk_add_conditions (const hash_set<bit_expression*>& conds);
+
+  vec<value*> * get_bits (tree var);
+
+  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);
@@ -102,6 +163,8 @@ class State {
   /* Does bit-level OR operation for given variables.  */
   void do_or (tree arg1, tree arg2, tree dest);
 
+  void do_assign (tree arg, 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);
@@ -112,19 +175,9 @@ class State {
   /* 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);
 
index 355646700674d13fcb056b089a7e4d3c3e3d98b2..888c861f48121f7aaae5c00f9b47dc30c7a98d6f 100644 (file)
@@ -42,7 +42,7 @@ along with GCC; see the file COPYING3.  If not see
    (Not complete).  */
 void
 crc_symb_execution::make_symbolic_func_args_and_sizes (function *fun,
-                                                      State *initial_state)
+                                                      state *initial_state)
 {
   if (dump_file && (dump_flags & TDF_DETAILS))
     fprintf (dump_file, "Making symbolic function's following arguments:\n");
@@ -70,7 +70,7 @@ crc_symb_execution::make_symbolic_func_args_and_sizes (function *fun,
 /* Add declared ssa variables to the state.  */
 void
 crc_symb_execution::add_function_local_ssa_vars (function *fun,
-                                                State *initial_state)
+                                                state *initial_state)
 {
   if (dump_file && (dump_flags & TDF_DETAILS))
     fprintf (dump_file, "\nAdding following ssa name declarations: \n");
@@ -119,7 +119,7 @@ crc_symb_execution::execute_assign_statement (const gassign *gs)
 {
   enum tree_code rhs_code = gimple_assign_rhs_code (gs);
   tree lhs = gimple_assign_lhs (gs);
-  State *current_state = states.last ();
+  state *current_state = states.last ();
   if (gimple_num_ops (gs) == 2 && rhs_code == BIT_NOT_EXPR)
     {
       tree op1 = gimple_assign_rhs1 (gs);
@@ -272,8 +272,8 @@ crc_symb_execution::execute_function (function *fun)
     fprintf (dump_file, "\nExecuting CRC-like function.\n");
 
   /* Create initial state and push into the vector of states.  */
-  states.quick_push (new State);
-  State *initial_state = states.last ();
+  states.quick_push (new state);
+  state *initial_state = states.last ();
 
   make_symbolic_func_args_and_sizes (fun, initial_state);
 
index 0fe42894eba13da9d7b353d17029b6a88d08ac49..08166be24368eb3f4223fe79c1d0119d378770bd 100644 (file)
@@ -43,14 +43,14 @@ class crc_symb_execution {
 
  private:
   /* A vector of states to keep the state of each executed path.  */
-  vec<State*> states;
+  vec<state*> states;
 
 /* Assign symbolic values to the arguments of the function
    and keep in the state.  */
-  static void make_symbolic_func_args_and_sizes (function *, State *);
+  static void make_symbolic_func_args_and_sizes (function *, state *);
 
   /* Add declared ssa variables to the state.  */
-  static void add_function_local_ssa_vars (function *fun, State *initial_state);
+  static void add_function_local_ssa_vars (function *fun, state *initial_state);
 
   void execute_assign_statement (const gassign *);
 
This page took 0.123945 seconds and 5 git commands to generate.