@@ -1722,6 +1722,9 @@ OBJS = \
tree-logical-location.o \
tree-loop-distribution.o \
gimple-crc-optimization.o \
+ sym-exec/sym-exec-expression.o \
+ sym-exec/sym-exec-state.o \
+ sym-exec/sym-exec-condition.o \
tree-nested.o \
tree-nrv.o \
tree-object-size.o \
@@ -36203,7 +36203,7 @@ $as_echo "$as_me: executing $ac_file commands" >&6;}
"depdir":C) $SHELL $ac_aux_dir/mkinstalldirs $DEPDIR ;;
"gccdepdir":C)
${CONFIG_SHELL-/bin/sh} $ac_aux_dir/mkinstalldirs build/$DEPDIR
- for lang in $subdirs c-family common analyzer text-art rtl-ssa
+ for lang in $subdirs c-family common analyzer text-art rtl-ssa sym-exec
do
${CONFIG_SHELL-/bin/sh} $ac_aux_dir/mkinstalldirs $lang/$DEPDIR
done ;;
new file mode 100644
@@ -0,0 +1,59 @@
+#include "sym-exec-condition.h"
+
+bit_condition::bit_condition (value_bit *left, value_bit *right, tree_code code)
+{
+ this->m_left = left;
+ this->m_right = right;
+ this->m_code = code;
+ m_type = BIT_CONDITION;
+}
+
+
+bit_condition::bit_condition (const bit_condition &expr)
+{
+ bit_expression::copy (&expr);
+ m_code = expr.get_code ();
+}
+
+
+/* Returns the condition's code. */
+
+tree_code
+bit_condition::get_code () const
+{
+ return m_code;
+}
+
+
+/* Returns a copy of the condition. */
+
+value_bit *
+bit_condition::copy () const
+{
+ return new bit_condition (*this);
+}
+
+
+/* Prints the condition's sign. */
+
+void
+bit_condition::print_expr_sign ()
+{
+ switch (m_code)
+ {
+ case GT_EXPR:
+ fprintf (dump_file, " > ");
+ break;
+ case LT_EXPR:
+ fprintf (dump_file, " < ");
+ break;
+ case EQ_EXPR:
+ fprintf (dump_file, " == ");
+ break;
+ case NE_EXPR:
+ fprintf (dump_file, " != ");
+ break;
+ default:
+ fprintf (dump_file, " ? ");
+ }
+}
\ No newline at end of file
new file mode 100644
@@ -0,0 +1,33 @@
+#ifndef SYM_EXEC_CONDITION_H
+#define SYM_EXEC_CONDITION_H
+
+#include "sym-exec-expression.h"
+
+enum condition_status {
+ CS_NO_COND,
+ CS_TRUE,
+ CS_FALSE,
+ CS_SYM
+};
+
+
+class bit_condition : public bit_expression {
+ private:
+ /* Condition's code. */
+ tree_code m_code;
+
+ /* Prints the condition's sign. */
+ void print_expr_sign ();
+
+ public:
+ bit_condition (value_bit *left, value_bit *right, tree_code type);
+ bit_condition (const bit_condition &expr);
+
+ /* Returns the condition's code. */
+ tree_code get_code () const;
+
+ /* Returns a copy of the condition. */
+ value_bit *copy () const;
+};
+
+#endif /* SYM_EXEC_CONDITION_H. */
\ No newline at end of file
new file mode 100644
@@ -0,0 +1,204 @@
+#ifndef SYM_EXEC_EXPRESSION_IS_A_HELPER_H
+#define SYM_EXEC_EXPRESSION_IS_A_HELPER_H
+
+#include "sym-exec-condition.h"
+
+/* Defining test functions for value conversion via dyn_cast. */
+
+template<>
+template<>
+inline bool
+is_a_helper<symbolic_bit *>::test (value_bit *ptr)
+{
+ return ptr->get_type () == value_type::SYMBOLIC_BIT;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit *>::test (value_bit *ptr)
+{
+ return ptr->get_type () == value_type::BIT;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_expression *>::test (value_bit *ptr)
+{
+ value_type type = ptr->get_type ();
+ return type == value_type::BIT_AND_EXPRESSION
+ || type == value_type::BIT_OR_EXPRESSION
+ || type == value_type::BIT_XOR_EXPRESSION
+ || type == value_type::BIT_COMPLEMENT_EXPRESSION
+ || type == value_type::SHIFT_RIGHT_EXPRESSION
+ || type == value_type::SHIFT_LEFT_EXPRESSION
+ || type == value_type::ADD_EXPRESSION
+ || type == value_type::SUB_EXPRESSION
+ || type == value_type::BIT_CONDITION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_and_expression *>::test (value_bit *ptr)
+{
+ return ptr->get_type () == value_type::BIT_AND_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_or_expression *>::test (value_bit *ptr)
+{
+ return ptr->get_type () == value_type::BIT_OR_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_xor_expression *>::test (value_bit *ptr)
+{
+ return ptr->get_type () == value_type::BIT_XOR_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_complement_expression *>::test (value_bit *ptr)
+{
+ return ptr->get_type () == value_type::BIT_COMPLEMENT_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_left_expression *>::test (value_bit *ptr)
+{
+ return ptr->get_type () == value_type::SHIFT_LEFT_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_right_expression *>::test (value_bit *ptr)
+{
+ return ptr->get_type () == value_type::SHIFT_RIGHT_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<add_expression *>::test (value_bit *ptr)
+{
+ return ptr->get_type () == value_type::ADD_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<sub_expression *>::test (value_bit *ptr)
+{
+ return ptr->get_type () == value_type::SUB_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_condition *>::test (value_bit *ptr)
+{
+ return ptr->get_type () == value_type::BIT_CONDITION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_and_expression *>::test (bit_expression *ptr)
+{
+ return ptr->get_type () == value_type::BIT_AND_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_or_expression *>::test (bit_expression *ptr)
+{
+ return ptr->get_type () == value_type::BIT_OR_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_xor_expression *>::test (bit_expression *ptr)
+{
+ return ptr->get_type () == value_type::BIT_XOR_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_complement_expression *>::test (bit_expression *ptr)
+{
+ return ptr->get_type () == value_type::BIT_COMPLEMENT_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_left_expression *>::test (bit_expression *ptr)
+{
+ return ptr->get_type () == value_type::SHIFT_LEFT_EXPRESSION;
+}
+
+template<>
+template<>
+inline bool
+is_a_helper<shift_right_expression *>::test (bit_expression *ptr)
+{
+ return ptr->get_type () == value_type::SHIFT_RIGHT_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<add_expression *>::test (bit_expression *ptr)
+{
+ return ptr->get_type () == value_type::ADD_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<sub_expression *>::test (bit_expression *ptr)
+{
+ return ptr->get_type () == value_type::SUB_EXPRESSION;
+}
+
+
+template<>
+template<>
+inline bool
+is_a_helper<bit_condition *>::test (bit_expression *ptr)
+{
+ return ptr->get_type () == value_type::BIT_CONDITION;
+}
+
+#endif /* SYM_EXEC_EXPRESSION_IS_A_HELPER_H. */
\ No newline at end of file
new file mode 100644
@@ -0,0 +1,426 @@
+/* Every class defined here represents a single bit value of a variable.
+ Every variable will be represented as a vector of these classes which later
+ will be used for bit-level symbolic execution. */
+
+#include "sym-exec-expr-is-a-helper.h"
+
+/* Returns type of the bit. */
+
+value_type
+value_bit::get_type () const
+{
+ return m_type;
+}
+
+
+symbolic_bit::symbolic_bit (size_t i, tree orig)
+ : value_bit (i), m_origin (orig)
+{
+ m_type = SYMBOLIC_BIT;
+}
+
+
+bit::bit (unsigned char i) : m_val (i)
+{
+ m_type = BIT;
+}
+
+
+/* Returns left operand of the expression. */
+
+value_bit *
+bit_expression::get_left ()
+{
+ return m_left;
+}
+
+
+/* Returns right operand of the expression. */
+
+value_bit *
+bit_expression::get_right ()
+{
+ return m_right;
+}
+
+
+/* Sets left operand of the expression. */
+
+void
+bit_expression::set_left (value_bit *expr)
+{
+ m_left = expr;
+}
+
+
+/* Sets right operand of the expression. */
+
+void
+bit_expression::set_right (value_bit *expr)
+{
+ m_right = expr;
+}
+
+
+/* Returns the bit's initial index in bit-vector. */
+
+size_t
+value_bit::get_index () const
+{
+ return m_index;
+}
+
+
+/* Returns the value of the bit. */
+
+unsigned char
+bit::get_val () const
+{
+ return m_val;
+}
+
+
+/* Sets the value of the bit. */
+
+void
+bit::set_val (unsigned char new_val)
+{
+ m_val = new_val;
+}
+
+
+bit_complement_expression::bit_complement_expression (value_bit *right)
+{
+ /* As complement has only one argument, we use only the m_right. */
+ this->m_left = nullptr;
+ this->m_right = right;
+ m_type = BIT_COMPLEMENT_EXPRESSION;
+}
+
+
+bit_complement_expression::bit_complement_expression (
+ const bit_complement_expression &expr)
+{
+ bit_expression::copy (&expr);
+}
+
+
+bit_expression::~bit_expression ()
+{
+ delete m_left;
+ m_left = nullptr;
+ delete m_right;
+ m_right = nullptr;
+}
+
+
+/* Returns a copy of the bit. */
+
+value_bit *
+symbolic_bit::copy () const
+{
+ return new symbolic_bit (*this);
+}
+
+
+/* Return a copy of the bit. */
+
+value_bit *
+bit::copy () const
+{
+ return new bit (*this);
+}
+
+
+/* Copies the given expression to it by copying the left and right operands. */
+
+void
+bit_expression::copy (const bit_expression *expr)
+{
+ if (expr->m_left)
+ m_left = expr->m_left->copy ();
+
+ if (expr->m_right)
+ m_right = expr->m_right->copy ();
+
+ m_type = expr->m_type;
+}
+
+
+/* Returns a copy of the expression. */
+
+value_bit *
+bit_xor_expression::copy () const
+{
+ return new bit_xor_expression (*this);
+}
+
+
+/* Returns a copy of the expression. */
+
+value_bit *
+bit_and_expression::copy () const
+{
+ return new bit_and_expression (*this);
+}
+
+
+/* Returns a copy of the expression. */
+
+value_bit *
+bit_or_expression::copy () const
+{
+ return new bit_or_expression (*this);
+}
+
+
+/* Returns a copy of the expression. */
+
+value_bit *
+shift_right_expression::copy () const
+{
+ return new shift_right_expression (*this);
+}
+
+
+/* Returns a copy of the expression. */
+
+value_bit *
+shift_left_expression::copy () const
+{
+ return new shift_left_expression (*this);
+}
+
+
+/* Returns a copy of the expression. */
+
+value_bit *
+add_expression::copy () const
+{
+ return new add_expression (*this);
+}
+
+
+/* Returns a copy of the expression. */
+
+value_bit *
+sub_expression::copy () const
+{
+ return new sub_expression (*this);
+}
+
+
+/* Returns a copy of the expression. */
+
+value_bit *
+bit_complement_expression::copy () const
+{
+ return new bit_complement_expression (*this);
+}
+
+
+bit_xor_expression::bit_xor_expression (value_bit *left, value_bit *right)
+{
+ this->m_left = left;
+ this->m_right = right;
+ m_type = BIT_XOR_EXPRESSION;
+}
+
+
+bit_xor_expression::bit_xor_expression (const bit_xor_expression &expr)
+{
+ bit_expression::copy (&expr);
+}
+
+
+bit_and_expression::bit_and_expression (value_bit *left, value_bit *right)
+{
+ this->m_left = left;
+ this->m_right = right;
+ m_type = BIT_AND_EXPRESSION;
+}
+
+
+bit_and_expression::bit_and_expression (const bit_and_expression &expr)
+{
+ bit_expression::copy (&expr);
+}
+
+
+bit_or_expression::bit_or_expression (value_bit *left, value_bit *right)
+{
+ this->m_left = left;
+ this->m_right = right;
+ m_type = BIT_OR_EXPRESSION;
+}
+
+
+bit_or_expression::bit_or_expression (const bit_or_expression &expr)
+{
+ bit_expression::copy (&expr);
+}
+
+
+shift_right_expression::shift_right_expression (value_bit *left,
+ value_bit *right)
+{
+ this->m_left = left;
+ this->m_right = right;
+ m_type = SHIFT_RIGHT_EXPRESSION;
+}
+
+
+shift_right_expression::shift_right_expression (
+ const shift_right_expression &expr)
+{
+ bit_expression::copy (&expr);
+}
+
+
+shift_left_expression::shift_left_expression (value_bit *left, value_bit *right)
+{
+ this->m_left = left;
+ this->m_right = right;
+ m_type = SHIFT_LEFT_EXPRESSION;
+}
+
+
+shift_left_expression::shift_left_expression (const shift_left_expression &expr)
+{
+ bit_expression::copy (&expr);
+}
+
+
+add_expression::add_expression (value_bit *left, value_bit *right)
+{
+ this->m_left = left;
+ this->m_right = right;
+ m_type = ADD_EXPRESSION;
+}
+
+
+add_expression::add_expression (const add_expression &expr)
+{
+ bit_expression::copy (&expr);
+}
+
+
+sub_expression::sub_expression (value_bit *left, value_bit *right)
+{
+ this->m_left = left;
+ this->m_right = right;
+ m_type = SUB_EXPRESSION;
+}
+
+
+sub_expression::sub_expression (const sub_expression &expr)
+{
+ bit_expression::copy (&expr);
+}
+
+
+/* Returns the origin of the bit, to whom it belongs. */
+
+tree
+symbolic_bit::get_origin ()
+{
+ return m_origin;
+}
+
+
+/* Prints the bit. */
+
+void
+symbolic_bit::print ()
+{
+ if (dump_file)
+ {
+ print_generic_expr (dump_file, m_origin, dump_flags);
+ fprintf (dump_file, "[%zu]", m_index);
+ }
+}
+
+
+/* Prints the bit. */
+
+void
+bit::print ()
+{
+ if (dump_file)
+ fprintf (dump_file, "%u", m_val);
+}
+
+
+/* Depending on the expression, prints its sign. */
+
+void
+bit_expression::print_expr_sign ()
+{
+ switch (m_type)
+ {
+ case BIT_XOR_EXPRESSION:
+ fprintf (dump_file, " ^ ");
+ break;
+ case BIT_AND_EXPRESSION:
+ fprintf (dump_file, " & ");
+ break;
+ case BIT_OR_EXPRESSION:
+ fprintf (dump_file, " | ");
+ break;
+ case SHIFT_RIGHT_EXPRESSION:
+ fprintf (dump_file, " >> ");
+ break;
+ case SHIFT_LEFT_EXPRESSION:
+ fprintf (dump_file, " << ");
+ break;
+ case ADD_EXPRESSION:
+ fprintf (dump_file, " + ");
+ break;
+ case SUB_EXPRESSION:
+ fprintf (dump_file, " - ");
+ break;
+ default:
+ fprintf (dump_file, " ?? ");
+ }
+}
+
+
+/* Prints the expression. */
+
+void
+bit_expression::print ()
+{
+ if (dump_file)
+ {
+ fprintf (dump_file, "(");
+ if (m_left)
+ m_left->print ();
+ else
+ fprintf (dump_file, "null");
+
+ print_expr_sign ();
+
+ if (m_right)
+ m_right->print ();
+ else
+ fprintf (dump_file, "null");
+
+ fprintf (dump_file, ")");
+ }
+}
+
+
+/* Prints the expression. */
+
+void
+bit_complement_expression::print ()
+{
+ if (dump_file)
+ {
+ fprintf (dump_file, "!");
+ if (m_right)
+ m_right->print ();
+ else
+ fprintf (dump_file, "null");
+ }
+}
\ No newline at end of file
new file mode 100644
@@ -0,0 +1,260 @@
+/* Every class defined here represents a single bit value of a variable.
+ Every variable will be represented as a vector of these classes which later
+ will be used for bit-level symbolic execution. */
+
+#ifndef SYM_EXEC_EXPRESSION_H
+#define SYM_EXEC_EXPRESSION_H
+
+#include "config.h"
+#include "system.h"
+#include "coretypes.h"
+#include "backend.h"
+#include "tree.h"
+#include "hwint.h"
+#include "gimple-pretty-print.h"
+#include "is-a.h"
+#include "vec.h"
+#include "hash-map.h"
+#include "hash-set.h"
+#include "stddef.h"
+
+/* Enum used for identifying the class of the bit. */
+
+enum value_type {
+ SYMBOLIC_BIT,
+ BIT,
+ BIT_XOR_EXPRESSION,
+ BIT_AND_EXPRESSION,
+ BIT_OR_EXPRESSION,
+ BIT_COMPLEMENT_EXPRESSION,
+ SHIFT_RIGHT_EXPRESSION,
+ SHIFT_LEFT_EXPRESSION,
+ ADD_EXPRESSION,
+ SUB_EXPRESSION,
+ BIT_CONDITION
+};
+
+/* Base class for single bit value. */
+
+class value_bit {
+ protected:
+ /* This will help us to understand where is moved the bit
+ from its initial position. */
+ const size_t m_index;
+
+ /* Type of the bit. Used by type checkers. */
+ value_type m_type;
+
+ public:
+ value_bit () : m_index (0)
+ {};
+ value_bit (size_t i) : m_index (i)
+ {};
+ value_bit (const value_bit &val) : m_index (val.m_index)
+ {};
+
+ /* Returns the bit's initial index in bit-vector. */
+ size_t get_index () const;
+
+ /* Returns type of the bit. */
+ value_type get_type () const;
+
+ /* This will support deep copy of objects' values. */
+ virtual value_bit *copy () const = 0;
+
+ /* Prints the bit. Inherited classes must implement it. */
+ virtual void print () = 0;
+ virtual ~value_bit () = default;
+};
+
+/* Represents value of a single bit of symbolic marked variables. */
+
+class symbolic_bit : public value_bit {
+ tree m_origin = nullptr;
+
+ public:
+ symbolic_bit (size_t i, tree orig);
+ symbolic_bit (const symbolic_bit &sym_bit) : symbolic_bit (sym_bit.m_index,
+ sym_bit.m_origin)
+ {};
+
+ /* Returns a copy of the bit. */
+ value_bit *copy () const;
+
+ /* Prints the bit. */
+ void print ();
+
+ /* Returns the origin of the bit, to whom it belongs. */
+ tree get_origin ();
+};
+
+
+/* Represents value of a single bit. */
+
+class bit : public value_bit {
+ private:
+ /* This is the value of a bit. It must be either 1 or 0. */
+ unsigned char m_val = 0;
+
+ public:
+ bit (unsigned char i);
+ bit (const bit &b) : bit (b.m_val)
+ {};
+
+ /* Returns the value of the bit. */
+ unsigned char get_val () const;
+
+ /* Sets the value of the bit. */
+ void set_val (unsigned char new_val);
+
+ /* Return a copy of the bit. */
+ value_bit *copy () const;
+
+ /* Prints the bit. */
+ void print ();
+};
+
+
+/* Bit-level base expression class. In general expressions consist of
+ two operands. Here we named them m_left and m_right. */
+
+class bit_expression : public value_bit {
+ protected:
+ value_bit *m_left = nullptr;
+ value_bit *m_right = nullptr;
+
+ /* Copies the given expression to it by copying
+ the left and right operands. */
+ void copy (const bit_expression *expr);
+
+ /* Depending on the expression, prints its sign. */
+ virtual void print_expr_sign ();
+
+ public:
+
+ /* Returns left operand of the expression. */
+ value_bit *get_left ();
+
+ /* Returns right operand of the expression. */
+ value_bit *get_right ();
+
+ ~bit_expression ();
+
+ /* Sets left operand of the expression. */
+ void set_left (value_bit *expr);
+
+ /* Sets right operand of the expression. */
+ void set_right (value_bit *expr);
+
+ /* Returns a deep copy of the expression. */
+ value_bit *copy () const = 0;
+
+ /* Prints the expression. */
+ void print ();
+};
+
+
+/* Bit-level XOR expression. XOR operation on two variables (when one of
+ them is symbolic) can be represented by XOR operations on
+ each of their bits. */
+
+class bit_xor_expression : public bit_expression {
+ public:
+ bit_xor_expression (value_bit *left, value_bit *right);
+ bit_xor_expression (const bit_xor_expression &expr);
+
+ /* Returns a copy of the expression. */
+ value_bit *copy () const;
+};
+
+
+/* Bit-level AND expression. AND operation on two variables (when one of
+ them is symbolic) can be represented by AND operations on
+ each of their bits. */
+
+class bit_and_expression : public bit_expression {
+ public:
+ bit_and_expression (value_bit *left, value_bit *right);
+ bit_and_expression (const bit_and_expression &expr);
+
+ /* Returns a copy of the expression. */
+ value_bit *copy () const;
+};
+
+
+/* Bit-level OR expression. OR operation on two variables (when one of
+ them is symbolic) can be represented by OR operations on
+ each of their bits. */
+
+class bit_or_expression : public bit_expression {
+ public:
+ bit_or_expression (value_bit *left, value_bit *right);
+ bit_or_expression (const bit_or_expression &expr);
+
+ /* Returns a copy of the expression. */
+ value_bit *copy () const;
+};
+
+
+/* SHIFT_RIGHT expression. Result must be stored bit by bit. */
+
+class shift_right_expression : public bit_expression {
+ public:
+ shift_right_expression (value_bit *left, value_bit *right);
+ shift_right_expression (const shift_right_expression &expr);
+
+ /* Returns a copy of the expression. */
+ value_bit *copy () const;
+};
+
+
+/* SHIFT_LEFT expression. Result must be stored bit by bit. */
+
+class shift_left_expression : public bit_expression {
+ public:
+ shift_left_expression (value_bit *left, value_bit *right);
+ shift_left_expression (const shift_left_expression &expr);
+
+ /* Returns a copy of the expression. */
+ value_bit *copy () const;
+};
+
+
+/* ADD expression. Result must be stored bit by bit. */
+
+class add_expression : public bit_expression {
+ public:
+ add_expression (value_bit *left, value_bit *right);
+ add_expression (const add_expression &expr);
+
+ /* Returns a copy of the expression. */
+ value_bit *copy () const;
+};
+
+
+/* SUB expression. Result must be stored bit by bit. */
+
+class sub_expression : public bit_expression {
+ public:
+ sub_expression (value_bit *left, value_bit *right);
+ sub_expression (const sub_expression &expr);
+
+ /* Returns a copy of the expression. */
+ value_bit *copy () const;
+};
+
+/* Bit-level negation expression. */
+
+class bit_complement_expression : public bit_expression {
+ public:
+ bit_complement_expression (value_bit *right);
+ bit_complement_expression (const bit_complement_expression &expr);
+
+ /* Returns a copy of the expression. */
+ value_bit *copy () const;
+
+ /* Prints the expression. */
+ void print ();
+};
+
+#endif /* SYM_EXEC_EXPRESSION_H. */
\ No newline at end of file
new file mode 100644
@@ -0,0 +1,2148 @@
+/* State will store states of variables for a function's single execution path.
+ It will be used for bit-level symbolic execution to determine values of bits
+ of function's return value and symbolic marked arguments. */
+
+#include "sym-exec-state.h"
+
+size_t min (size_t a, size_t b, size_t c)
+{
+ size_t min = (a < b ? a : b);
+ return min < c ? min : c;
+}
+
+
+state::state (const state &s)
+{
+ for (auto iter = s.var_states.begin (); iter != s.var_states.end (); ++iter)
+ {
+ value val ((*iter).second.length (), (*iter).second.is_unsigned);
+ for (size_t i = 0; i < (*iter).second.length (); i++)
+ val.push ((*iter).second[i]->copy ());
+
+ var_states.put ((*iter).first, val);
+ }
+
+ for (auto iter = s.conditions.begin (); iter != s.conditions.end (); ++iter)
+ conditions.add (as_a<bit_expression *> ((*iter)->copy ()));
+}
+
+
+state::~state ()
+{
+ clear_conditions ();
+}
+
+
+/* Checks whether state for variable with specified name already
+ exists or not. */
+
+bool
+state::is_declared (tree var)
+{
+ return var_states.get (var) != NULL;
+}
+
+
+/* Declares given variable if it has not been declared yet. */
+
+void
+state::declare_if_needed (tree var, size_t size)
+{
+ if (TREE_CODE (var) != INTEGER_CST && !is_declared (var))
+ {
+ make_symbolic (var, size);
+ if (dump_file && (dump_flags & TDF_DETAILS))
+ {
+ fprintf (dump_file,
+ "Declaring var ");
+ print_generic_expr (dump_file, var, dump_flags);
+ fprintf (dump_file,
+ " with size %zd\n", size);
+ }
+ }
+}
+
+
+/* Get value of the given variable. */
+
+value *
+state::get_value (tree var)
+{
+ return var_states.get (var);
+}
+
+
+/* Get the value of the tree, which is in the beginning of the var_states. */
+
+value *
+state::get_first_value ()
+{
+ return &(*(var_states.begin ())).second;
+}
+
+
+/* Returns the list of conditions in the state. */
+
+const hash_set<bit_expression *> &
+state::get_conditions ()
+{
+ return conditions;
+}
+
+
+/* Checks if sizes of arguments and destination are compatible. */
+
+bool
+state::check_args_compatibility (tree arg1, tree arg2, tree dest)
+{
+ if (!(get_var_size (arg1) == get_var_size (dest)
+ || TREE_CODE (arg1) == INTEGER_CST)
+ || !(get_var_size (arg2) == get_var_size (dest)
+ || TREE_CODE (arg2) == INTEGER_CST))
+ {
+ if (dump_file && (dump_flags & TDF_DETAILS))
+ fprintf (dump_file, "Sym-Exec: Incompatible destination"
+ "and argument sizes.\n");
+
+ return false;
+ }
+
+ return true;
+}
+
+
+/* Creates value for given constant tree. */
+
+value
+state::create_val_for_const (tree var, size_t size)
+{
+ unsigned HOST_WIDE_INT val = TYPE_UNSIGNED (TREE_TYPE (var))
+ ? tree_to_uhwi (var) : tree_to_shwi (var);
+ value result (size, TYPE_UNSIGNED (TREE_TYPE (var)));
+
+ for (size_t i = 0; i < size; i++)
+ {
+ result.push (new bit (val & 1));
+ val >>= 1;
+ }
+
+ return result;
+}
+
+
+/* Adds the given variable to state. */
+
+bool
+state::add_var_state (tree var, value *vstate)
+{
+ size_t size = vstate->length ();
+ value val (size, vstate->is_unsigned);
+ for (size_t i = 0; i < size; i++)
+ val.push ((*vstate)[i]->copy ());
+
+ return var_states.put (var, val);
+}
+
+
+/* Adds the given condition to the state. */
+
+bool
+state::add_condition (bit_expression *cond)
+{
+ return conditions.add (as_a<bit_expression *> (cond->copy ()));
+}
+
+
+/* Bulk add the given conditions to the state. */
+
+bool
+state::bulk_add_conditions (const hash_set<bit_expression *> &conds)
+{
+ bool status = true;
+ for (auto iter = conds.begin (); iter != conds.end (); ++iter)
+ status &= add_condition (*iter);
+
+ return status;
+}
+
+
+/* Remove all states from the states' vector. */
+
+void
+state::remove_states (vec<state *> *states)
+{
+ while (!states->is_empty ())
+ {
+ delete states->last ();
+ states->pop ();
+ }
+}
+
+
+/* Remove all states from the states' vector and release the vector. */
+
+void
+state::clear_states (vec<state *> *states)
+{
+ remove_states (states);
+ states->release ();
+}
+
+
+/* Removes all variables added to the state. */
+
+void
+state::clear_var_states ()
+{
+ var_states.empty ();
+}
+
+
+/* Removes all conditions added to the state. */
+
+void
+state::clear_conditions ()
+{
+ for (auto iter = conditions.begin (); iter != conditions.end (); ++iter)
+ delete (*iter);
+ conditions.empty ();
+}
+
+
+/* Performs AND operation for 2 symbolic_bit operands. */
+
+value_bit *
+state::and_sym_bits (const value_bit *var1, const value_bit *var2)
+{
+ return new bit_and_expression (var1->copy (), var2->copy ());
+}
+
+
+/* Performs AND operation for a symbolic_bit and const_bit operands. */
+
+value_bit *
+state::and_var_const (const value_bit *var1, const bit *const_bit)
+{
+ if (const_bit->get_val () == 1)
+ return var1->copy ();
+
+ return new bit (0);
+}
+
+
+/* Performs AND operation for 2 constant bit operands. */
+
+bit *
+state::and_const_bits (const bit *const_bit1, const bit *const_bit2)
+{
+ if (const_bit1->get_val () == const_bit2->get_val ())
+ return new bit (*const_bit1);
+
+ return new bit (0);
+}
+
+
+/* Performs OR operation for 2 symbolic_bit operands. */
+
+value_bit *
+state::or_sym_bits (const value_bit *var1, const value_bit *var2)
+{
+ return new bit_or_expression (var1->copy (), var2->copy ());
+}
+
+
+/* Performs OR operation for a symbolic_bit and a constant bit operands. */
+
+value_bit *
+state::or_var_const (const value_bit *var1, const bit *const_bit)
+{
+ if (const_bit->get_val () == 0)
+ return var1->copy ();
+
+ return new bit (1);
+}
+
+
+/* Performs OR operation for 2 constant bit operands. */
+
+bit *
+state::or_const_bits (const bit *const_bit1, const bit *const_bit2)
+{
+ if (const_bit1->get_val () == const_bit2->get_val ())
+ return new bit (*const_bit1);
+
+ return new bit (1);
+}
+
+
+/* Adds an empty state for the given variable. */
+
+bool
+state::decl_var (tree var, unsigned size)
+{
+ if (is_declared (var))
+ return false;
+
+ value val (size, TYPE_UNSIGNED (TREE_TYPE (var)));
+ for (unsigned i = 0; i < size; i++)
+ val.push (nullptr);
+
+ return var_states.put (var, val);
+}
+
+
+/* Returns size of the given variable. */
+
+unsigned
+state::get_var_size (tree var)
+{
+ value *content = var_states.get (var);
+ if (content == NULL)
+ return 0;
+
+ return content->allocated ();
+}
+
+
+/* Adds a variable with unknown value to state. Such variables are
+ represented as sequence of symbolic bits. */
+
+bool
+state::make_symbolic (tree var, unsigned size)
+{
+ if (is_declared (var))
+ return false;
+
+ value val (size, TYPE_UNSIGNED (TREE_TYPE (var)));
+ /* Initialize each bit of a variable with unknown value. */
+ for (size_t i = 0; i < size; i++)
+ val.push (new symbolic_bit (i, var));
+
+ return var_states.put (var, val);
+}
+
+
+/* Performs AND operation on two bits. */
+
+value_bit *
+state::and_two_bits (value_bit *arg1, value_bit *arg2)
+{
+ value_bit *result = nullptr;
+
+ if (is_a<bit *> (arg1) && is_a<bit *> (arg2))
+ result = and_const_bits (as_a<bit *> (arg1), as_a<bit *> (arg2));
+
+ else if (is_a<bit *> (arg1) && (is_a<symbolic_bit *> (arg2)
+ || (is_a<bit_expression *> (arg2))))
+ result = and_var_const (arg2, as_a<bit *> (arg1));
+
+ else if ((is_a<symbolic_bit *> (arg1)
+ || (is_a<bit_expression *> (arg1))) && is_a<bit *> (arg2))
+ result = and_var_const (arg1, as_a<bit *> (arg2));
+
+ else
+ result = and_sym_bits (arg1, arg2);
+
+ return result;
+}
+
+
+/* A wrapper for operations on two bits.
+ Operation and operands are passed as arguments. */
+
+value_bit *
+state::operate_bits (bit_func bit_op, value_bit *bit1, value_bit *bit2,
+ value_bit **)
+{
+ return (bit_op) (bit1, bit2);
+}
+
+
+/* A wrapper for operations on three bits.
+ Operation and operands are passed as arguments. */
+
+value_bit *
+state::operate_bits (bit_func3 bit_op, value_bit *bit1, value_bit *bit2,
+ value_bit **bit3)
+{
+ return (bit_op) (bit1, bit2, bit3);
+}
+
+
+/* Does preprocessing and postprocessing for expressions with tree operands.
+ Handles value creation for constant and their removement in the end. */
+
+bool
+state::do_binary_operation (tree arg1, tree arg2, tree dest,
+ binary_func bin_func)
+{
+ declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+ declare_if_needed (arg1, var_states.get (dest)->allocated ());
+ declare_if_needed (arg2, var_states.get (dest)->allocated ());
+
+ if (!check_args_compatibility (arg1, arg2, dest))
+ return false;
+
+ size_t dest_size = var_states.get (dest)->length ();
+
+ value *arg1_val = var_states.get (arg1);
+ value arg1_const_val (dest_size, false);
+ if (arg1_val == NULL && TREE_CODE (arg1) == INTEGER_CST)
+ {
+ arg1_const_val = create_val_for_const (arg1, dest_size);
+ arg1_val = &arg1_const_val;
+ }
+
+ value *arg2_val = var_states.get (arg2);
+ value arg2_const_val (dest_size, false);
+ if (arg2_val == NULL && TREE_CODE (arg2) == INTEGER_CST)
+ {
+ arg2_const_val = create_val_for_const (arg2, dest_size);
+ arg2_val = &arg2_const_val;
+ }
+
+ (this->*bin_func) (arg1_val, arg2_val, dest);
+ print_value (var_states.get (dest));
+ return true;
+}
+
+
+/* Performs AND operation on given values. The result is stored in dest. */
+
+void
+state::do_and (value *arg1, value *arg2, tree dest)
+{
+ /* Creating AND expressions for every bit pair of given arguments
+ and store them as a new state for given destination. */
+
+ operate (arg1, arg2, nullptr, dest, &state::and_two_bits);
+}
+
+
+/* Performs OR operation on two bits. */
+
+value_bit *
+state::or_two_bits (value_bit *arg1_bit, value_bit *arg2_bit)
+{
+ value_bit *result = nullptr;
+
+ if (is_a<bit *> (arg1_bit) && is_a<bit *> (arg2_bit))
+ result = or_const_bits (as_a<bit *> (arg1_bit), as_a<bit *> (arg2_bit));
+
+ else if (is_a<bit *> (arg1_bit) && (is_a<symbolic_bit *> (arg2_bit)
+ || is_a<bit_expression *> (arg2_bit)))
+ result = or_var_const (arg2_bit, as_a<bit *> (arg1_bit));
+
+ else if ((is_a<symbolic_bit *> (arg1_bit)
+ || is_a<bit_expression *> (arg1_bit))
+ && is_a<bit *> (arg2_bit))
+ result = or_var_const (arg1_bit, as_a<bit *> (arg2_bit));
+
+ else
+ result = or_sym_bits (arg1_bit, arg2_bit);
+
+ return result;
+}
+
+
+/* Performs OR operation on given values. The result is stored in dest. */
+
+void
+state::do_or (value *arg1, value *arg2, tree dest)
+{
+ /* Creating OR expressions for every bit pair of given arguments
+ and store them as a new state for given destination. */
+ operate (arg1, arg2, nullptr, dest, &state::or_two_bits);
+}
+
+
+/* Performs XOR operation on two bits. */
+
+value_bit *
+state::xor_two_bits (value_bit *arg1_bit, value_bit *arg2_bit)
+{
+ value_bit *result = nullptr;
+
+ if (is_a<bit *> (arg1_bit) && is_a<bit *> (arg2_bit))
+ result = xor_const_bits (as_a<bit *> (arg1_bit), as_a<bit *> (arg2_bit));
+
+ else if (is_a<bit *> (arg1_bit) && (is_a<symbolic_bit *> (arg2_bit)
+ || is_a<bit_expression *> (arg2_bit)))
+ result = xor_var_const (arg2_bit, as_a<bit *> (arg1_bit));
+
+ else if ((is_a<symbolic_bit *> (arg1_bit)
+ || is_a<bit_expression *> (arg1_bit))
+ && is_a<bit *> (arg2_bit))
+ result = xor_var_const (arg1_bit, as_a<bit *> (arg2_bit));
+
+ else
+ result = xor_sym_bits (arg1_bit, arg2_bit);
+
+ return result;
+}
+
+
+/* Performs XOR operation on given values. The result is stored in dest. */
+
+void
+state::do_xor (value *arg1, value *arg2, tree dest)
+{
+ operate (arg1, arg2, nullptr, dest, &state::xor_two_bits);
+}
+
+
+/* Shifts value right by size of shift_value. */
+
+value *
+state::shift_right_by_const (value *var, size_t shift_value)
+{
+ value *shift_result = new value (var->length (), var->is_unsigned);
+ if (var->length () <= shift_value)
+ for (size_t i = 0; i < var->length (); i++)
+ shift_result->push (new bit (0));
+ else
+ {
+ size_t i = 0;
+ for (; i < var->length () - shift_value; ++i)
+ shift_result->push (((*var)[shift_value + i])->copy ());
+
+ for (; i < var->length (); ++i)
+ shift_result->push (var->is_unsigned ? new bit (0)
+ : var->last ()->copy ());
+ }
+ return shift_result;
+}
+
+
+/* Checks if all bits of the given value have constant bit type. */
+
+bool
+state::is_bit_vector (const value *var)
+{
+ if (var == nullptr || !var->exists ())
+ return false;
+
+ for (size_t i = 0; i < var->length (); i++)
+ if (!(is_a<bit *> ((*var)[i])))
+ return false;
+ return true;
+}
+
+
+/* Returns the number represented by the value. */
+
+unsigned HOST_WIDE_INT
+state::make_number (const value *var)
+{
+ unsigned HOST_WIDE_INT
+ number = 0;
+ int value_size = var->length ();
+ for (int i = value_size - 1; i >= 0; i--)
+ {
+ if (is_a<bit *> ((*var)[i]))
+ number = (number << 1) | as_a<bit *> ((*var)[i])->get_val ();
+ else
+ return 0;
+ }
+ return number;
+}
+
+
+/* Shift_left operation. Case: var2 is a symbolic value. */
+
+value_bit *
+state::shift_left_sym_bits (value_bit *var1, value_bit *var2)
+{
+ return new shift_left_expression (var1->copy (), var2->copy ());
+}
+
+
+/* Performs shift left operation on given values.
+ The result is stored in dest. */
+
+void
+state::do_shift_left (value *arg1, value *arg2, tree dest)
+{
+ if (is_bit_vector (arg2))
+ {
+ size_t shift_value = make_number (arg2);
+ value *result = shift_left_by_const (arg1, shift_value);
+ for (size_t i = 0; i < get_var_size (dest); i++)
+ {
+ delete (*var_states.get (dest))[i];
+ (*var_states.get (dest))[i] = (*result)[i]->copy ();
+ }
+ delete result;
+ }
+ else
+ operate (arg1, arg2, nullptr, dest, &state::shift_left_sym_bits);
+}
+
+
+/* Performs shift right operation on given values.
+ The result is stored in dest. */
+
+void
+state::do_shift_right (value *arg1, value *arg2, tree dest)
+{
+ if (is_bit_vector (arg2))
+ {
+ size_t shift_value = make_number (arg2);
+ value *result = shift_right_by_const (arg1, shift_value);
+ for (size_t i = 0; i < get_var_size (dest); i++)
+ {
+ delete (*var_states.get (dest))[i];
+ (*var_states.get (dest))[i] = (*result)[i]->copy ();
+ }
+
+ delete result;
+ }
+ else
+ operate (arg1, arg2, nullptr, dest, &state::shift_right_sym_bits);
+}
+
+
+/* Adds two bits and carry value.
+ Resturn result and stores new carry bit in "carry". */
+
+value_bit *
+state::full_adder (value_bit *var1, value_bit *var2, value_bit **carry)
+{
+ value_bit *new_carry = and_two_bits (var1, var2);
+ value_bit *sum = xor_two_bits (var1, var2);
+
+ value_bit *result = xor_two_bits (sum, *carry);
+ value_bit *sum_and_carry = and_two_bits (sum, *carry);
+
+ delete *carry;
+ delete sum;
+
+ *carry = or_two_bits (sum_and_carry, new_carry);
+
+ delete sum_and_carry;
+ delete new_carry;
+
+ return result;
+}
+
+
+/* Adds given values. The result is stored in dest. */
+
+void
+state::do_add (value *arg1, value *arg2, tree dest)
+{
+ value_bit *carry = new bit (0);
+ operate (arg1, arg2, &carry, dest, &state::full_adder);
+ delete carry;
+}
+
+
+/* Returns the additive inverse of the given number. */
+
+value *
+state::additive_inverse (const value *number)
+{
+ value *result = new value (number->length (), number->is_unsigned);
+ value one (number->length (), number->is_unsigned);
+
+ size_t size = number->length ();
+ one.push (new bit (1));
+ result->push (complement_a_bit ((*number)[0]));
+
+ for (size_t i = 1; i < size; i++)
+ {
+ one.push (new bit (0));
+ result->push (complement_a_bit ((*number)[i]));
+ }
+
+ value_bit *carry = new bit (0);
+ for (size_t i = 0; i < size; ++i)
+ {
+ value_bit *cur_bit = (*result)[i];
+ (*result)[i] = full_adder (cur_bit, one[i], &carry);
+ delete cur_bit;
+ }
+
+ delete carry;
+ return result;
+}
+
+
+/* Subtracks second value from the first. The result is stored in dest. */
+
+void
+state::do_sub (value *arg1, value *arg2, tree dest)
+{
+ value *neg_arg2 = additive_inverse (arg2);
+ do_add (arg1, neg_arg2, dest);
+ delete neg_arg2;
+}
+
+
+/* Performs complement operation on a bit. */
+
+value_bit *
+state::complement_a_bit (value_bit *var)
+{
+ value_bit *result = nullptr;
+ if (is_a<bit *> (var))
+ result = complement_const_bit (as_a<bit *> (var));
+ else
+ result = complement_sym_bit (var);
+
+ return result;
+}
+
+
+/* Negates given variable. */
+
+bool
+state::do_complement (tree arg, tree dest)
+{
+ declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+ declare_if_needed (arg, var_states.get (dest)->allocated ());
+
+ /* Creating complement expressions for every bit the given argument
+ and store it as a new state for given destination. */
+ size_t iter_count = min (get_var_size (dest), get_var_size (arg),
+ get_var_size (arg));
+
+ size_t i = 0;
+ for (; i < iter_count; i++)
+ {
+ value_bit *result = complement_a_bit ((*var_states.get (arg))[i]);
+ delete (*var_states.get (dest))[i];
+ (*var_states.get (dest))[i] = result;
+ }
+
+ if (i >= get_var_size (dest))
+ {
+ print_value (var_states.get (dest));
+ return true;
+ }
+
+ for (; i < get_var_size (dest); i++)
+ {
+ delete (*var_states.get (dest))[i];
+ bit tmp (0);
+ (*var_states.get (dest))[i] = complement_a_bit (&tmp);
+ }
+
+ print_value (var_states.get (dest));
+ return true;
+}
+
+
+/* Does Assignment. */
+
+bool
+state::do_assign (tree arg, tree dest)
+{
+ declare_if_needed (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+ if (TREE_CODE (arg) != INTEGER_CST)
+ declare_if_needed (arg, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (arg))));
+ else
+ declare_if_needed (arg, var_states.get (dest)->allocated ());
+
+ value *dest_val = var_states.get (dest);
+
+ /* If the argument is already defined, then we must just copy its bits. */
+ if (auto arg_val = var_states.get (arg))
+ {
+ for (size_t i = 0; i < dest_val->length (); i++)
+ {
+ value_bit *new_val = nullptr;
+ if (i < arg_val->length ())
+ new_val = (*arg_val)[i]->copy ();
+ else
+ new_val = new bit (0);
+
+ delete (*dest_val)[i];
+ (*dest_val)[i] = new_val;
+ }
+ }
+ /* If the argument is a constant, we must save it as sequence of bits. */
+ else if (TREE_CODE (arg) == INTEGER_CST)
+ {
+ value arg_val
+ = create_val_for_const (arg, dest_val->length ());
+ for (size_t i = 0; i < dest_val->length (); i++)
+ {
+ delete (*dest_val)[i];
+ (*dest_val)[i] = arg_val[i]->copy ();
+ }
+ }
+ else
+ {
+ if (dump_file && (dump_flags & TDF_DETAILS))
+ fprintf (dump_file, "Sym-Exec: Unsupported assignment"
+ " for given argument.\n");
+
+ return false;
+ }
+
+ print_value (var_states.get (dest));
+ return true;
+}
+
+
+/* Assigns pow 2 value. */
+
+bool
+state::do_assign_pow2 (tree dest, unsigned pow)
+{
+ value *dest_val = var_states.get (dest);
+ unsigned dest_size = dest_val ? dest_val->allocated ()
+ : tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest)));
+ if (pow > dest_size)
+ {
+ if (dump_file && (dump_flags & TDF_DETAILS))
+ fprintf (dump_file, "Sym-Exec: pow %u of 2 won't fit in"
+ " specified destination\n", pow);
+ return false;
+ }
+
+ if (!dest_val)
+ {
+ decl_var (dest, tree_to_uhwi (TYPE_SIZE (TREE_TYPE (dest))));
+ dest_val = var_states.get (dest);
+ }
+ else
+ dest_val->free_bits ();
+
+ for (unsigned i = 0; i < dest_val->length (); i++)
+ {
+ if (i == pow)
+ (*dest_val)[i] = new bit (1);
+ else
+ (*dest_val)[i] = new bit (0);
+ }
+
+ print_value (dest_val);
+ return true;
+}
+
+
+/* Performs NOT operation for constant bit. */
+
+bit *
+state::complement_const_bit (const bit *const_bit)
+{
+ return new bit (1u ^ const_bit->get_val ());
+}
+
+
+/* Performs NOT operation for symbolic_bit. */
+
+value_bit *
+state::complement_sym_bit (const value_bit *var)
+{
+ return new bit_complement_expression (var->copy ());
+}
+
+
+/* Performs XOR operation for 2 symbolic_bit operands. */
+
+value_bit *
+state::xor_sym_bits (const value_bit *var1, const value_bit *var2)
+{
+ value_bit *var2_copy = var2->copy ();
+ bit_expression *node2_with_const_child = nullptr;
+ bit_expression *parent_of_node2_with_child = nullptr;
+ get_parent_with_const_child (var2_copy, node2_with_const_child,
+ parent_of_node2_with_child);
+
+ if (node2_with_const_child != nullptr)
+ {
+ value_bit *var1_copy = var1->copy ();
+ bit_expression *node1_with_const_child = nullptr;
+ bit_expression *parent_of_node1_with_child = nullptr;
+ get_parent_with_const_child (var1_copy, node1_with_const_child,
+ parent_of_node1_with_child);
+
+ /* If both subtrees have constant bit nodes,
+ we can merge them together. */
+ if (node1_with_const_child != nullptr)
+ {
+ value_bit *var1_reformed = nullptr;
+ value_bit *var2_reformed = nullptr;
+
+ /* If var1's const bit is in its left subtree. */
+ value_bit *var1_left = node1_with_const_child->get_left ();
+ if (var1_left != nullptr && is_a<bit *> (var1_left))
+ {
+ var1_reformed = node1_with_const_child->get_right ()->copy ();
+ value_bit *var2_left = node2_with_const_child->get_left ();
+
+ /* If var2's const bit is in its left subtree. */
+ if (var2_left != nullptr && is_a<bit *> (var2_left))
+ var2_reformed = node2_with_const_child->get_right ()->copy ();
+ else /* Var2's const bit is in its right subtree. */
+ var2_reformed = node2_with_const_child->get_left ()->copy ();
+ }
+ else /* Var1's const bit is in its right subtree. */
+ {
+ var1_reformed = node1_with_const_child->get_left ()->copy ();
+ value_bit *var2_left = node2_with_const_child->get_left ();
+
+ /* If var2's const bit is in its left subtree. */
+ if (var2_left != nullptr && is_a<bit *> (var2_left))
+ var2_reformed = node2_with_const_child->get_right ()->copy ();
+ else /* Var2's const bit is in its right subtree. */
+ var2_reformed = node2_with_const_child->get_left ()->copy ();
+ }
+
+ if (parent_of_node1_with_child)
+ {
+ parent_of_node1_with_child->get_left ()
+ == node1_with_const_child
+ ? parent_of_node1_with_child->set_left (var1_reformed)
+ : parent_of_node1_with_child->set_right (var1_reformed);
+ delete node1_with_const_child;
+ }
+ else
+ {
+ delete var1_copy;
+ var1_copy = var1_reformed;
+ }
+
+ if (parent_of_node2_with_child)
+ {
+ parent_of_node2_with_child->get_left ()
+ == node2_with_const_child
+ ? parent_of_node2_with_child->set_left (var2_reformed)
+ : parent_of_node2_with_child->set_right (var2_reformed);
+ delete node2_with_const_child;
+ }
+ else
+ {
+ delete var2_copy;
+ var2_copy = var2_reformed;
+ }
+
+ return new bit_xor_expression (var1_copy, var2_copy);
+ }
+ delete var1_copy;
+ }
+
+ delete var2_copy;
+ return new bit_xor_expression (var1->copy (), var2->copy ());
+}
+
+
+/* Performs XOR operation for 2 constant bit operands. */
+
+bit *
+state::xor_const_bits (const bit *const_bit1, const bit *const_bit2)
+{
+ return new bit (const_bit1->get_val () ^ const_bit2->get_val ());
+}
+
+
+/* Performs XOR operation for a symbolic_bit and const_bit operands. */
+
+value_bit *
+state::xor_var_const (const value_bit *var, const bit *const_bit)
+{
+ if (const_bit->get_val () == 0)
+ return var->copy ();
+
+ value_bit *var_copy = var->copy ();
+ bit_expression *node_with_const_child = nullptr;
+ bit_expression *tmp = nullptr;
+ get_parent_with_const_child (var_copy, node_with_const_child, tmp);
+
+ if (node_with_const_child != nullptr)
+ {
+ value_bit *left = node_with_const_child->get_left ();
+ if (left != nullptr && is_a<bit *> (left))
+ {
+ bit *new_left = xor_const_bits (as_a<bit *> (left), const_bit);
+ delete left;
+ node_with_const_child->set_left (new_left);
+ }
+ else
+ {
+ value_bit *right = node_with_const_child->get_right ();
+ bit *new_right = xor_const_bits (as_a<bit *> (right), const_bit);
+ delete right;
+ node_with_const_child->set_right (new_right);
+ }
+ return var_copy;
+ }
+
+ delete var_copy;
+ return new bit_xor_expression (var->copy (), const_bit->copy ());
+}
+
+
+/* Return node which has a const bit child. Traversal is done based
+ on safe branching. */
+
+void
+state::get_parent_with_const_child (value_bit *root, bit_expression *&parent,
+ bit_expression *&parent_of_parent)
+{
+ parent_of_parent = nullptr;
+ parent = nullptr;
+
+ if (!is_a<bit_expression *> (root))
+ return;
+
+ bit_expression *expr_root = as_a<bit_expression *> (root);
+ hash_set < bit_expression * > nodes_to_consider;
+ nodes_to_consider.add (expr_root);
+
+ hash_map < bit_expression * , bit_expression * > node_to_parent;
+ node_to_parent.put (expr_root, nullptr);
+
+ /* Traversing expression tree:
+ considering only comutative expression nodes. */
+ while (!nodes_to_consider.is_empty ())
+ {
+ bit_expression *cur_element = *nodes_to_consider.begin ();
+ nodes_to_consider.remove (cur_element);
+
+ value_bit *left = cur_element->get_left ();
+ value_bit *right = cur_element->get_right ();
+
+ if ((left != nullptr && is_a<bit *> (left))
+ || (right != nullptr && is_a<bit *> (right)))
+ {
+ parent = cur_element;
+ parent_of_parent = *node_to_parent.get (cur_element);
+ }
+
+ if (left != nullptr && is_a<bit_xor_expression *> (left))
+ {
+ nodes_to_consider.add (as_a<bit_expression *> (left));
+ node_to_parent.put (as_a<bit_expression *> (left), cur_element);
+ }
+
+ if (right != nullptr && is_a<bit_xor_expression *> (right))
+ {
+ nodes_to_consider.add (as_a<bit_expression *> (right));
+ node_to_parent.put (as_a<bit_expression *> (right), cur_element);
+ }
+ }
+}
+
+
+/* Shifts number left by size of shift_value. */
+
+value *
+state::shift_left_by_const (const value *number, size_t shift_value)
+{
+ value *shift_result = new value (number->length (), number->is_unsigned);
+ if (number->length () <= shift_value)
+ for (size_t i = 0; i < number->length (); i++)
+ shift_result->push (new bit (0));
+
+ else
+ {
+ size_t i = 0;
+ for (; i < shift_value; ++i)
+ shift_result->push (new bit (0));
+ for (size_t j = 0; i < number->length (); ++i, j++)
+ shift_result->push (((*number)[j])->copy ());
+ }
+ return shift_result;
+}
+
+
+/* Shift_right operation. Case: var2 is a symbolic value. */
+
+value_bit *
+state::shift_right_sym_bits (value_bit *var1, value_bit *var2)
+{
+ return new shift_right_expression (var1->copy (), var2->copy ());
+}
+
+
+/* Adds two values, stores the result in the first one. */
+
+void
+state::add_numbers (value *var1, const value *var2)
+{
+ value_bit *carry = new bit (0);
+ for (unsigned i = 0; i < var1->length (); i++)
+ {
+ value_bit *temp = (*var1)[i];
+ (*var1)[i] = full_adder ((*var1)[i], (*var2)[i], &carry);
+ delete temp;
+ }
+ delete carry;
+}
+
+
+/* ANDs every bit of the vector with var_bit, stroes the result in var1. */
+
+void
+state::and_number_bit (value *var1, value_bit *var_bit)
+{
+ for (unsigned i = 0; i < var1->length (); i++)
+ {
+ value_bit *tmp = (*var1)[i];
+ (*var1)[i] = and_two_bits ((*var1)[i], var_bit);
+ delete tmp;
+ }
+
+}
+
+
+void
+state::do_mul (value *arg1, value *arg2, tree dest)
+{
+ value *shifted = new value (*arg1);
+ value *dest_val = var_states.get (dest);
+
+ for (unsigned i = 0; i < dest_val->length (); i++)
+ {
+ delete (*dest_val)[i];
+ (*dest_val)[i] = new bit (0);
+ }
+
+ for (unsigned i = arg2->length (); i != 0; --i)
+ {
+ if (is_a<bit *> ((*arg2)[i - 1])
+ && as_a<bit *> ((*arg2)[i - 1])->get_val () != 0)
+ add_numbers (dest_val, shifted);
+ else if (is_a<symbolic_bit *> ((*arg2)[i - 1]))
+ {
+ and_number_bit (shifted, as_a<symbolic_bit *> ((*arg2)[i - 1]));
+ add_numbers (dest_val, shifted);
+ }
+
+ value *temp = shifted;
+ shifted = shift_left_by_const (shifted, 1);
+ delete temp;
+ }
+ delete shifted;
+}
+
+
+/* Checks whether the given two constant values are equal. */
+
+bool
+state::check_const_value_equality (value *arg1, value *arg2)
+{
+ for (size_t i = 0; i < arg1->length (); i++)
+ if (as_a<bit *> ((*arg1)[i])->get_val ()
+ != as_a<bit *> ((*arg2)[i])->get_val ())
+ return false;
+ return true;
+}
+
+
+/* Adds EQUAL condition of given variables to state. */
+
+bool
+state::add_equal_cond (tree arg1, tree arg2)
+{
+ return add_binary_cond (arg1, arg2, &state::add_equal_cond);
+}
+
+
+/* Adds equality condition for two values. */
+
+void
+state::add_equal_cond (value *arg1, value *arg2)
+{
+
+ /* If both arguments are constants then we can evaluate it. */
+ if (is_bit_vector (arg1) && is_bit_vector (arg2))
+ {
+ bool result = check_const_value_equality (arg1, arg2);
+ last_cond_status = result ? condition_status::CS_TRUE
+ : condition_status::CS_FALSE;
+ return;
+ }
+
+ /* When some of bits are constants and they differ by value,
+ then we can evalate it to be false. */
+ for (size_t i = 0; i < arg1->length (); i++)
+ {
+ if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i])
+ && as_a<bit *> ((*arg1)[i])->get_val ()
+ != as_a<bit *> ((*arg2)[i])->get_val ())
+ {
+ last_cond_status = condition_status::CS_FALSE;
+ return;
+ }
+ }
+
+ for (size_t i = 0; i < arg1->length (); i++)
+ {
+ /* If there is a constant bit pair, then they are equal
+ as we checked not equality above. */
+ if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i]))
+ continue;
+
+ conditions.add (new bit_condition ((*arg1)[i]->copy (),
+ (*arg2)[i]->copy (),
+ EQ_EXPR));
+ }
+ last_cond_status = condition_status::CS_SYM;
+}
+
+
+/* Checks whether the given two constant values are not equal. */
+
+bool
+state::check_const_value_are_not_equal (value *arg1, value *arg2)
+{
+ for (size_t i = 0; i < arg1->length (); i++)
+ if (as_a<bit *> ((*arg1)[i])->get_val ()
+ != as_a<bit *> ((*arg2)[i])->get_val ())
+ return true;
+ return false;
+}
+
+
+/* Adds NOT EQUAL condition of given variables to state. */
+
+bool
+state::add_not_equal_cond (tree arg1, tree arg2)
+{
+ return add_binary_cond (arg1, arg2, &state::add_not_equal_cond);
+}
+
+
+/* Adds not equal condition for two values. */
+
+void
+state::add_not_equal_cond (value *arg1, value *arg2)
+{
+ if (is_bit_vector (arg1) && is_bit_vector (arg2))
+ {
+ bool result = check_const_value_are_not_equal (arg1, arg2);
+ last_cond_status = result ? condition_status::CS_TRUE
+ : condition_status::CS_FALSE;
+ return;
+ }
+
+ /* When some of bits are constants and they differ by value,
+ then we can evalate it to be true. */
+ for (size_t i = 0; i < arg1->length (); i++)
+ {
+ if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i])
+ && as_a<bit *> ((*arg1)[i])->get_val ()
+ != as_a<bit *> ((*arg2)[i])->get_val ())
+ {
+ last_cond_status = condition_status::CS_TRUE;
+ return;
+ }
+ }
+
+ bit_expression *prev = nullptr;
+ for (size_t i = 0; i < arg1->length (); i++)
+ {
+ /* If there is a constant bit pair, then they are equal
+ as we checked not equality above. */
+ if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i]))
+ continue;
+
+ bit_condition *new_cond = new bit_condition ((*arg1)[i]->copy (),
+ (*arg2)[i]->copy (),
+ NE_EXPR);
+ if (prev)
+ prev = new bit_or_expression (prev, new_cond);
+ else
+ prev = new_cond;
+ }
+
+ last_cond_status = condition_status::CS_SYM;
+ conditions.add (prev);
+}
+
+
+/* Checks whether the first given constant value
+ is greater than the second one. */
+
+bool
+state::check_const_value_is_greater_than (value *arg1, value *arg2)
+{
+ for (int i = arg1->length () - 1; i >= 0; i--)
+ {
+ if (as_a<bit *> ((*arg1)[i])->get_val ()
+ > as_a<bit *> ((*arg2)[i])->get_val ())
+ return true;
+ else if (as_a<bit *> ((*arg1)[i])->get_val ()
+ < as_a<bit *> ((*arg2)[i])->get_val ())
+ return false;
+ }
+ return false;
+}
+
+
+/* Adds GREATER THAN condition of given variables to state. */
+
+bool
+state::add_greater_than_cond (tree arg1, tree arg2)
+{
+ return add_binary_cond (arg1, arg2, &state::add_greater_than_cond);
+}
+
+
+/* Adds greater than condition for two values. */
+
+void
+state::add_greater_than_cond (value *arg1, value *arg2)
+{
+ if (is_bit_vector (arg1) && is_bit_vector (arg2))
+ {
+ bool result = check_const_value_is_greater_than (arg1, arg2);
+ last_cond_status = result ? condition_status::CS_TRUE
+ : condition_status::CS_FALSE;
+ return;
+ }
+
+ if (is_bit_vector (arg2) && is_a<bit *> (arg1->last ())
+ && make_number (arg2) == 0 && !arg1->is_unsigned)
+ {
+ if (as_a<bit *> (arg1->last ())->get_val () == 1)
+ last_cond_status = condition_status::CS_FALSE;
+ else
+ {
+ for (size_t i = 0; i < arg1->length (); i++)
+ if (is_a<bit *> ((*arg1)[i])
+ && as_a<bit *> ((*arg1)[i])->get_val ())
+ {
+ last_cond_status = condition_status::CS_TRUE;
+ return;
+ }
+ }
+ }
+
+ bit_expression *gt_cond = construct_great_than_cond (arg1, arg2);
+ if (gt_cond)
+ {
+ /* Otherwise its status is already set. */
+ last_cond_status = condition_status::CS_SYM;
+ conditions.add (gt_cond);
+ }
+}
+
+
+/* Constructs expression trees of greater than condition for given values. */
+
+bit_expression *
+state::construct_great_than_cond (value *arg1, value *arg2)
+{
+ bit_expression *prev = nullptr;
+ int i = arg1->length () - 1;
+ for (; i >= 0; i--)
+ {
+ if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i]))
+ {
+ if (as_a<bit *> ((*arg1)[i])->get_val ()
+ > as_a<bit *> ((*arg2)[i])->get_val ())
+ {
+ if (!prev)
+ last_cond_status = condition_status::CS_TRUE;
+ return prev;
+ }
+ else if (as_a<bit *> ((*arg1)[i])->get_val ()
+ < as_a<bit *> ((*arg2)[i])->get_val ())
+ {
+ if (prev)
+ {
+ bit_expression *ret_val
+ = as_a<bit_expression *> (prev->get_left ()->copy ());
+ delete prev;
+ return ret_val;
+ }
+ else
+ {
+ last_cond_status = condition_status::CS_FALSE;
+ return nullptr;
+ }
+ }
+ }
+ else
+ {
+ bit_condition *gt_cond
+ = new bit_condition ((*arg1)[i]->copy (), (*arg2)[i]->copy (),
+ GT_EXPR);
+ bit_expression *expr = nullptr;
+ if (i)
+ {
+ bit_condition *eq_cond
+ = new bit_condition ((*arg1)[i]->copy (), (*arg2)[i]->copy (),
+ EQ_EXPR);
+ expr = new bit_or_expression (gt_cond, eq_cond);
+ }
+ else
+ expr = gt_cond;
+
+ if (prev)
+ prev = new bit_and_expression (expr, prev);
+ else
+ prev = expr;
+ }
+ }
+
+ return prev;
+}
+
+
+/* Checks whether the first given constant value
+ is less than the second one. */
+
+bool
+state::check_const_value_is_less_than (value *arg1, value *arg2)
+{
+ for (int i = arg1->length () - 1; i >= 0; i--)
+ {
+ if (as_a<bit *> ((*arg1)[i])->get_val ()
+ < as_a<bit *> ((*arg2)[i])->get_val ())
+ return true;
+ else if (as_a<bit *> ((*arg1)[i])->get_val ()
+ > as_a<bit *> ((*arg2)[i])->get_val ())
+ return false;
+ }
+ return false;
+}
+
+
+/* Adds LESS THAN condition of given variables to state. */
+
+bool
+state::add_less_than_cond (tree arg1, tree arg2)
+{
+ return add_binary_cond (arg1, arg2, &state::add_less_than_cond);
+}
+
+
+/* Adds less than condition for two values. */
+
+void
+state::add_less_than_cond (value *arg1, value *arg2)
+{
+ if (is_bit_vector (arg1) && is_bit_vector (arg2)
+ && (make_number (arg2) != 0 || arg1->is_unsigned))
+ {
+ bool result = check_const_value_is_less_than (arg1, arg2);
+ last_cond_status = result ? condition_status::CS_TRUE
+ : condition_status::CS_FALSE;
+ return;
+ }
+
+ last_cond_status = condition_status::CS_SYM;
+ if (is_bit_vector (arg2) && make_number (arg2) == 0 && !arg1->is_unsigned)
+ {
+ if (is_a<bit *> (arg1->last ()))
+ {
+ if (as_a<bit *> (arg1->last ())->get_val () == 1)
+ last_cond_status = condition_status::CS_TRUE;
+ else
+ last_cond_status = condition_status::CS_FALSE;
+ }
+ else
+ conditions.add (new bit_condition (arg1->last ()->copy (), new bit (1),
+ EQ_EXPR));
+
+ return;
+ }
+
+ bit_expression *lt_cond = construct_less_than_cond (arg1, arg2);
+ if (lt_cond)
+ /* Otherwise its status is already set. */
+ conditions.add (lt_cond);
+}
+
+
+/* Constructs expression trees of less than condition for given values. */
+
+bit_expression *
+state::construct_less_than_cond (value *arg1, value *arg2)
+{
+ bit_expression *prev = nullptr;
+ int i = arg1->length () - 1;
+ for (; i >= 0; i--)
+ {
+ if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i]))
+ {
+ if (as_a<bit *> ((*arg1)[i])->get_val ()
+ < as_a<bit *> ((*arg2)[i])->get_val ())
+ {
+ if (!prev)
+ last_cond_status = condition_status::CS_TRUE;
+ return prev;
+ }
+ else if (as_a<bit *> ((*arg1)[i])->get_val ()
+ > as_a<bit *> ((*arg2)[i])->get_val ())
+ {
+ if (prev)
+ {
+ bit_expression *ret_val
+ = as_a<bit_expression *> (prev->get_left ()->copy ());
+ delete prev;
+ return ret_val;
+ }
+ else
+ {
+ last_cond_status = condition_status::CS_FALSE;
+ return nullptr;
+ }
+ }
+ }
+ else
+ {
+ bit_condition *lt_cond
+ = new bit_condition ((*arg1)[i]->copy (), (*arg2)[i]->copy (),
+ LT_EXPR);
+ bit_expression *expr = nullptr;
+ if (i)
+ {
+ bit_condition *eq_cond
+ = new bit_condition ((*arg1)[i]->copy (), (*arg2)[i]->copy (),
+ EQ_EXPR);
+ expr = new bit_or_expression (lt_cond, eq_cond);
+ }
+ else
+ expr = lt_cond;
+
+ if (prev)
+ prev = new bit_and_expression (expr, prev);
+ else
+ prev = expr;
+ }
+ }
+
+ return prev;
+}
+
+
+/* Adds GREATER OR EQUAL condition of given variables to state. */
+
+bool
+state::add_greater_or_equal_cond (tree arg1, tree arg2)
+{
+ return add_binary_cond (arg1, arg2, &state::add_greater_or_equal_cond);
+}
+
+
+/* Adds greater or equal condition for two values. */
+
+void
+state::add_greater_or_equal_cond (value *arg1, value *arg2)
+{
+ if (is_bit_vector (arg1) && is_bit_vector (arg2)
+ && (make_number (arg2) != 0 || arg1->is_unsigned))
+ {
+ bool is_greater_than = check_const_value_is_greater_than (arg1,
+ arg2);
+ bool is_equal = check_const_value_equality (arg1, arg2);
+ last_cond_status = (is_greater_than | is_equal)
+ ? condition_status::CS_TRUE
+ : condition_status::CS_FALSE;
+ return;
+ }
+
+ last_cond_status = condition_status::CS_SYM;
+ if (is_bit_vector (arg2) && make_number (arg2) == 0 && !arg1->is_unsigned)
+ {
+ if (is_a<bit *> (arg1->last ()))
+ {
+ if (as_a<bit *> (arg1->last ())->get_val () == 1)
+ last_cond_status = condition_status::CS_FALSE;
+ else
+ last_cond_status = condition_status::CS_TRUE;
+ }
+ else
+ conditions.add (new bit_condition (arg1->last ()->copy (), new bit (0),
+ EQ_EXPR));
+
+ return;
+ }
+
+ bit_expression *eq_cond = construct_equal_cond (arg1, arg2);
+ if (!eq_cond)
+ return;
+
+ bit_expression *gt_cond = construct_great_than_cond (arg1, arg2);
+ if (gt_cond)
+ /* Otherwise its status is already set. */
+ conditions.add (new bit_or_expression (eq_cond, gt_cond));
+}
+
+
+/* Adds LESS OR EQUAL condition of given variables to state. */
+
+bool
+state::add_less_or_equal_cond (tree arg1, tree arg2)
+{
+ return add_binary_cond (arg1, arg2, &state::add_less_or_equal_cond);
+}
+
+
+/* Adds less or equal condition for two values. */
+
+void
+state::add_less_or_equal_cond (value *arg1, value *arg2)
+{
+ if (is_bit_vector (arg1) && is_bit_vector (arg2))
+ {
+ bool is_less_than = check_const_value_is_less_than (arg1, arg2);
+ bool is_equal = check_const_value_equality (arg1, arg2);
+ last_cond_status = (is_less_than | is_equal)
+ ? condition_status::CS_TRUE
+ : condition_status::CS_FALSE;
+ return;
+ }
+
+ last_cond_status = condition_status::CS_SYM;
+ bit_expression *eq_cond = construct_equal_cond (arg1, arg2);
+ if (!eq_cond)
+ return;
+
+ bit_expression *lt_cond = construct_less_than_cond (arg1, arg2);
+ if (lt_cond)
+ /* Otherwise its status is already set. */
+ conditions.add (new bit_or_expression (eq_cond, lt_cond));
+}
+
+
+/* Adds a bool condition to state. */
+
+bool
+state::add_bool_cond (tree arg)
+{
+ if (!is_declared (arg))
+ {
+ if (dump_file && (dump_flags & TDF_DETAILS))
+ fprintf (dump_file, "Sym-Exec: Argument must be declared "
+ "for bool condition.\n");
+
+ return false;
+ }
+
+ value *arg_bits = var_states.get (arg);
+ for (size_t i = 0; i < arg_bits->length (); i++)
+ if (is_a<bit *> ((*arg_bits)[i])
+ && as_a<bit *> ((*arg_bits)[i])->get_val () != 0)
+ {
+ last_cond_status = condition_status::CS_TRUE;
+ print_conditions ();
+ return true;
+ }
+
+ if (is_bit_vector (arg_bits))
+ {
+ last_cond_status = condition_status::CS_FALSE;
+ print_conditions ();
+ return true;
+ }
+
+ bit_expression *prev = nullptr;
+ for (size_t i = 0; i < arg_bits->length (); i++)
+ {
+ if (is_a<bit *> ((*arg_bits)[i]))
+ continue;
+
+ bit_condition *not_eq_cond
+ = new bit_condition ((*arg_bits)[i], new bit (0), NE_EXPR);
+ if (prev)
+ prev = new bit_or_expression (not_eq_cond, prev);
+ else
+ prev = not_eq_cond;
+ }
+
+ last_cond_status = condition_status::CS_SYM;
+ conditions.add (prev);
+ print_conditions ();
+ return true;
+}
+
+
+/* Does preprocessing and postprocessing for condition adding.
+ Handles value creation for constants and their removement in the end. */
+
+bool
+state::add_binary_cond (tree arg1, tree arg2, binary_cond_func cond_func)
+{
+ bool arg1_is_declared = is_declared (arg1);
+ bool arg2_is_declared = is_declared (arg2);
+
+ if (!arg1_is_declared && !arg2_is_declared)
+ {
+ if (dump_file && (dump_flags & TDF_DETAILS))
+ fprintf (dump_file, "Sym-Exec: At least one of arguments must be"
+ " declared for adding the condition.\n");
+
+ return false;
+ }
+
+ if (arg1_is_declared)
+ declare_if_needed (arg2, var_states.get (arg1)->length ());
+
+ if (arg2_is_declared)
+ declare_if_needed (arg1, var_states.get (arg2)->length ());
+
+ value *arg1_val = var_states.get (arg1);
+ value arg1_const_val (MAX_VALUE_SIZE, false);
+
+ if (arg1_val == NULL && TREE_CODE (arg1) == INTEGER_CST)
+ {
+ arg1_const_val = create_val_for_const (arg1,
+ var_states.get (arg2)->length ());
+ arg1_val = &arg1_const_val;
+ }
+
+ value *arg2_val = var_states.get (arg2);
+ value arg2_const_val (MAX_VALUE_SIZE, false);
+ if (arg2_val == NULL && TREE_CODE (arg2) == INTEGER_CST)
+ {
+ arg2_const_val = create_val_for_const (arg2,
+ var_states.get (arg1)->length ());
+ arg2_val = &arg2_const_val;
+ }
+
+ (this->*cond_func) (arg1_val, arg2_val);
+ print_conditions ();
+ return true;
+}
+
+
+/* Constructs expression trees of equal condition for given values. */
+
+bit_expression *
+state::construct_equal_cond (value *arg1, value *arg2)
+{
+ /* If both arguments are constants then we can evaluate it. */
+ if (is_bit_vector (arg1) && is_bit_vector (arg2))
+ {
+ bool result = check_const_value_equality (arg1, arg2);
+ last_cond_status = result ? condition_status::CS_TRUE
+ : condition_status::CS_FALSE;
+ return nullptr;
+ }
+
+ /* When some bits are constants, and they differ by value,
+ then we can evaluate it to be false. */
+ for (size_t i = 0; i < arg1->length (); i++)
+ {
+ if (is_a<bit *> ((*arg1)[i]) && is_a<bit *> ((*arg2)[i])
+ && as_a<bit *> ((*arg1)[i])->get_val ()
+ != as_a<bit *> ((*arg2)[i])->get_val ())
+ {
+ last_cond_status = condition_status::CS_FALSE;
+ return nullptr;
+ }
+ }
+
+ bit_expression *prev = nullptr;
+ for (size_t i = 0; i < arg1->length (); i++)
+ {
+ bit_condition *eq_expr = new bit_condition ((*arg1)[i]->copy (),
+ (*arg2)[i]->copy (), EQ_EXPR);
+ if (prev)
+ prev = new bit_and_expression (eq_expr, prev);
+ else
+ prev = eq_expr;
+ }
+
+ return prev;
+}
+
+
+value::value (unsigned size, bool is_unsigned) : is_unsigned (is_unsigned)
+{
+ number.create (size);
+}
+
+
+value::value (const value &other) : is_unsigned (other.is_unsigned)
+{
+ number.create (other.length ());
+ for (size_t i = 0; i < other.length (); ++i)
+ {
+ value_bit *temp = other[i] ? other[i]->copy () : other[i];
+ number.quick_push (temp);
+ }
+}
+
+
+/* Returns pushed bits count. */
+
+unsigned
+value::length () const
+{
+ return number.length ();
+}
+
+
+/* Wrapper of vec<..>::operator[] for the bit-vector. */
+
+value_bit *&
+value::operator[] (unsigned i)
+{
+ return number[i];
+}
+
+
+/* Assignment operator. If the specified value's size is smaller,
+ then 0 constant bit will be assigned to the remaining upper bits. */
+
+value &
+value::operator= (const value &other)
+{
+ unsigned smallest = number.allocated () < other.length ()
+ ? number.allocated () : other.length ();
+
+ for (size_t i = 0; i < smallest; i++)
+ if (i < number.length ())
+ {
+ delete number[i];
+ number[i] = other[i]->copy ();
+ }
+ else
+ number.quick_push (other[i]->copy ());
+
+ for (size_t i = smallest; i < number.allocated (); i++)
+ if (i < number.length ())
+ {
+ delete number[i];
+ number[i] = other.is_unsigned ? new bit (0)
+ : other[other.length () - 1]->copy ();
+ }
+ else
+ number.quick_push (other.is_unsigned
+ ? new bit (0) : other[other.length () - 1]->copy ());
+
+ return (*this);
+}
+
+
+/* Wrapper of vec<..>::operator[] const for the bit-vector. */
+
+value_bit *
+value::operator[] (unsigned i) const
+{
+ return number[i];
+}
+
+
+/* Wrapper of vec<..>.exists for the bit-vector. */
+
+bool
+value::exists () const
+{
+ return number.exists ();
+}
+
+
+/* Returns the size in bits. */
+
+unsigned
+value::allocated () const
+{
+ return number.allocated ();
+}
+
+
+/* Returns a reference the last bit. */
+
+value_bit *&
+value::last ()
+{
+ return number.last ();
+}
+
+
+/* Make a copy of given bits. */
+
+vec<value_bit *> *
+state::make_copy (vec<value_bit *> *bits)
+{
+ vec < value_bit * > *copied_bits = new vec<value_bit *> ();
+ copied_bits->create (bits->length ());
+ for (size_t i = 0; i < bits->length (); i++)
+ copied_bits->quick_push ((*bits)[i]->copy ());
+
+ return copied_bits;
+}
+
+
+/* Returns status of last added condition. */
+
+condition_status
+state::get_last_cond_status ()
+{
+ return last_cond_status;
+}
+
+
+/* Prints the given value. */
+
+void
+state::print_value (value *var)
+{
+ if (!dump_file || !(dump_flags & TDF_DETAILS))
+ return;
+
+ fprintf (dump_file, "{");
+ for (int i = var->length () - 1; i >= 0; i--)
+ {
+ (*var)[i]->print ();
+
+ if (i)
+ fprintf (dump_file, ", ");
+ }
+ fprintf (dump_file, "}\n");
+}
+
+
+/* Get the last 1 bit index. */
+
+size_t
+last_set_bit (const value &polynomial)
+{
+ for (size_t i = 0; i < polynomial.length (); ++i)
+ {
+ if (as_a<bit *> (polynomial[polynomial.length () - i - 1])->get_val ())
+ return polynomial.length () - i - 1;
+ }
+ return 0;
+}
+
+
+/* Prints added conditions. */
+
+void
+state::print_conditions ()
+{
+ if (!dump_file || !(dump_flags & TDF_DETAILS))
+ return;
+
+ fprintf (dump_file, "Conditions {");
+ auto iter = conditions.begin ();
+ while (true)
+ {
+ if (iter != conditions.end ())
+ {
+ (*iter)->print ();
+ ++iter;
+ }
+
+ if (iter != conditions.end ())
+ fprintf (dump_file, ", ");
+ else
+ break;
+ }
+ fprintf (dump_file, "}\n");
+}
+
+
+/* Pushes the given bit to the end of the bit vector. */
+
+value_bit **
+value::push (value_bit *elem)
+{
+ return number.quick_push (elem);
+}
+
+
+value::~value ()
+{
+ free_bits ();
+ number.release ();
+}
+
+
+/* Removes given sequence of bits. */
+
+void
+value::free_bits ()
+{
+ if (!number.exists ())
+ return;
+
+ for (size_t i = 0; i < number.length (); i++)
+ {
+ delete number[i];
+ number[i] = nullptr;
+ }
+}
+
+
+/* For the given value_bit, iterates over its expression tree, complements
+ those bit which came from the given origin. */
+
+value_bit *
+state::complement_bits_with_origin (value_bit *root, tree origin)
+{
+ /* Be careful. This function doesn't make a full copy of the bit. */
+ if (!is_a<bit_expression *> (root))
+ {
+ if (is_a<symbolic_bit *> (root)
+ && as_a<symbolic_bit *> (root)->get_origin () == origin)
+ root = new bit_complement_expression (root);
+
+ return root;
+ }
+
+ bit_expression *expr_root = as_a<bit_expression *> (root);
+ hash_set <value_bit *> nodes_to_consider;
+ nodes_to_consider.add (expr_root);
+ hash_map <value_bit *, value_bit *> node_to_parent;
+ node_to_parent.put (expr_root, nullptr);
+
+ /* Traversing expression tree. */
+ while (!nodes_to_consider.is_empty ())
+ {
+ value_bit *cur_element = *nodes_to_consider.begin ();
+ nodes_to_consider.remove (cur_element);
+
+ if (is_a<symbolic_bit *> (cur_element))
+ {
+ if (as_a<symbolic_bit *> (cur_element)->get_origin () != origin)
+ continue;
+
+ bit_expression *parent
+ = as_a<bit_expression *> (*node_to_parent.get (cur_element));
+ if (is_a<bit_complement_expression *> (parent))
+ {
+ value_bit *parent_of_parent = *node_to_parent.get (parent);
+ if (parent_of_parent)
+ {
+ bit_expression *parent_of_parent_expr
+ = as_a<bit_expression *> (parent_of_parent);
+ parent->set_right (nullptr);
+ delete parent;
+ parent_of_parent_expr->get_left () == parent
+ ? parent_of_parent_expr->set_left (cur_element)
+ : parent_of_parent_expr->set_right (cur_element);
+ }
+ else
+ {
+ /* Parent is our root. */
+ as_a<bit_expression *> (root)->set_right (nullptr);
+ delete root;
+ root = cur_element;
+ }
+ }
+ else
+ {
+ value_bit* new_bit = new bit_complement_expression (cur_element);
+ parent->get_left () == cur_element ? parent->set_left (new_bit)
+ : parent->set_right (new_bit);
+ }
+ continue;
+ }
+
+ bit_expression* cur_elem_expr = as_a<bit_expression *> (cur_element);
+ value_bit *left = cur_elem_expr->get_left ();
+ value_bit *right = cur_elem_expr->get_right ();
+ if (left != nullptr && !is_a<bit *> (left))
+ {
+ nodes_to_consider.add (left);
+ node_to_parent.put (left, cur_element);
+ }
+
+ if (right != nullptr && !is_a<bit *> (right))
+ {
+ nodes_to_consider.add (right);
+ node_to_parent.put (right, cur_element);
+ }
+ }
+
+ return root;
+}
+
+
+/* Iterates over every bit of the given value and complements their
+ expression trees' those bits, that came from the given origin. */
+
+void
+state::complement_val_bits_with_origin (value *val, tree origin)
+{
+ for (size_t i = 0; i < val->length (); i++)
+ {
+ (*val)[i] = complement_bits_with_origin ((*val)[i], origin);
+ }
+}
+
+
+/* Complements all bits of all values that came from the given origin. */
+
+void
+state::complement_all_vars_bits_with_origin (tree origin)
+{
+ for (auto iter = var_states.begin (); iter != var_states.end (); ++iter)
+ {
+ complement_val_bits_with_origin (&(*iter).second, origin);
+ }
+}
+
+
+/* Complements all bits with the given origin of all added conditions. */
+
+void
+state::complement_conditions_with_origin (tree origin)
+{
+ hash_set<bit_expression *> updated_conditions;
+ for (auto iter = conditions.begin (); iter != conditions.end (); ++iter)
+ updated_conditions.add (as_a<bit_expression *> (
+ complement_bits_with_origin (*iter, origin)));
+
+ conditions.empty ();
+ for (auto iter = updated_conditions.begin ();
+ iter != updated_conditions.end (); ++iter)
+ conditions.add (*iter);
+}
+
+
+/* Complements all bits with the given origin of all values
+ and added conditions. */
+
+void
+state::complement_state_with_origin (tree origin)
+{
+ complement_all_vars_bits_with_origin (origin);
+ complement_conditions_with_origin (origin);
+}
+
+
+/* Performs the specified operation on passed variables. */
+
+bool
+state::do_operation (tree_code op_code, tree arg1, tree arg2, tree dest)
+{
+ switch (op_code)
+ {
+ case BIT_NOT_EXPR:
+ return do_complement (arg1, dest);
+ case NOP_EXPR:
+ case SSA_NAME:
+ case VAR_DECL:
+ case INTEGER_CST:
+ return do_assign (arg1, dest);
+ case LSHIFT_EXPR:
+ return do_binary_operation (arg1, arg2, dest, &state::do_shift_left);
+ case RSHIFT_EXPR:
+ return do_binary_operation (arg1, arg2, dest, &state::do_shift_right);
+ case BIT_AND_EXPR:
+ return do_binary_operation (arg1, arg2, dest, &state::do_and);
+ case BIT_IOR_EXPR:
+ return do_binary_operation (arg1, arg2, dest, &state::do_or);
+ case BIT_XOR_EXPR:
+ return do_binary_operation (arg1, arg2, dest, &state::do_xor);
+ case PLUS_EXPR:
+ return do_binary_operation (arg1, arg2, dest, &state::do_add);
+ case MINUS_EXPR:
+ return do_binary_operation (arg1, arg2, dest, &state::do_sub);
+ case MULT_EXPR:
+ return do_binary_operation (arg1, arg2, dest, &state::do_mul);
+ default:
+ {
+ if (dump_file)
+ fprintf (dump_file,
+ "Warning, encountered unsupported operation "
+ "with %s code while executing assign statement!\n",
+ get_tree_code_name (op_code));
+ return false;
+ }
+ }
+}
new file mode 100644
@@ -0,0 +1,436 @@
+/* State will store states of variables for a function's single execution path.
+ It will be used for bit-level symbolic execution to determine values of bits
+ of function's return value and symbolic marked arguments. */
+
+
+#ifndef SYM_EXEC_STATE_H
+#define SYM_EXEC_STATE_H
+
+#define MAX_VALUE_SIZE 64
+
+#include "sym-exec-expr-is-a-helper.h"
+
+struct value {
+ private:
+ vec<value_bit *> number;
+
+ public:
+ const bool is_unsigned;
+
+ value (unsigned size, bool is_unsigned);
+ value (const value &other);
+
+ /* Pushes the given bit to the end of the bit-vector. */
+ value_bit **push (value_bit *elem);
+
+ /* Returns pushed bits count. */
+ unsigned length () const;
+
+ /* Returns a reference the last bit. */
+ value_bit *&last ();
+
+ /* Returns the size in bits. */
+ unsigned allocated () const;
+
+ /* Wrapper of vec<..>.exists for the bit-vector. */
+ bool exists () const;
+
+ /* Wrapper of vec<..>::operator[] for the bit-vector. */
+ value_bit *&operator[] (unsigned i);
+
+ /* Assignment operator. If the specified value's size is smaller,
+ then 0 constant bit will be assigned to the remaining upper bits. */
+ value &operator= (const value &other);
+
+ /* Wrapper of vec<..>::operator[] const for the bit-vector. */
+ value_bit *operator[] (unsigned i) const;
+ ~value ();
+
+ /* Removes given sequence of bits. */
+ void free_bits ();
+};
+
+/* Stores states of variables' values on bit-level. */
+
+class state {
+ typedef void (state::*binary_func) (value *arg1, value *arg2, tree dest);
+ typedef value_bit *(*bit_func) (value_bit *bit1, value_bit *bit2);
+ typedef value_bit *(*bit_func3) (value_bit *var1, value_bit *var2,
+ value_bit **var3);
+ typedef void (state::*binary_cond_func) (value *arg1, value *arg2);
+
+ private:
+
+ /* Here is stored values by bits of each variable. */
+ hash_map<tree, value> var_states;
+
+ /* Here is stored conditions of symbolic bits. */
+ hash_set<bit_expression *> conditions;
+
+ /* The result of last added condition. */
+ condition_status last_cond_status = condition_status::CS_NO_COND;
+
+ /* Creates value for given constant tree. */
+ static value create_val_for_const (tree var, size_t size);
+
+ /* Checks if sizes of arguments and destination are compatible. */
+ bool check_args_compatibility (tree arg1, tree arg2, tree dest);
+
+ /* Adds equality condition for two values. */
+ void add_equal_cond (value *arg1, value *arg2);
+
+ /* Adds not equal condition for two values. */
+ void add_not_equal_cond (value *arg1, value *arg2);
+
+ /* Adds greater than condition for two values. */
+ void add_greater_than_cond (value *arg1, value *arg2);
+
+ /* Adds less than condition for two values. */
+ void add_less_than_cond (value *arg1, value *arg2);
+
+ /* Adds greater or equal condition for two values. */
+ void add_greater_or_equal_cond (value *arg1, value *arg2);
+
+ /* Adds less or equal condition for two values. */
+ void add_less_or_equal_cond (value *arg1, value *arg2);
+
+ /* Does preprocessing and postprocessing for condition adding.
+ Handles value creation for constants and their removement in the end. */
+ bool add_binary_cond (tree arg1, tree arg2, binary_cond_func cond_func);
+
+ /* Constructs expression trees of greater than condition for given values. */
+ bit_expression *construct_great_than_cond (value *arg1, value *arg2);
+
+ /* Constructs expression trees of less than condition for given values. */
+ bit_expression *construct_less_than_cond (value *arg1, value *arg2);
+
+ /* Constructs expression trees of equal condition for given values. */
+ bit_expression *construct_equal_cond (value *arg1, value *arg2);
+
+ /* A wrapper for operations on two bits.
+ Operation and operands are passed as arguments. */
+ static value_bit *operate_bits (bit_func bit_op, value_bit *bit1,
+ value_bit *bit2, value_bit **bit3);
+
+ /* A wrapper for operations on three bits.
+ Operation and operands are passed as arguments. */
+ static value_bit *operate_bits (bit_func3 bit_op, value_bit *bit1,
+ value_bit *bit2, value_bit **bit3);
+
+ /* Performs the given operation on passed arguments.
+ The result is stored in dest. */
+ template<class func>
+ void operate (value *arg1, value *arg2, value_bit **bit_arg, tree dest,
+ func bit_op);
+
+ /* Does preprocessing and postprocessing for expressions with tree operands.
+ Handles value creation for constant and their removement in the end. */
+ bool do_binary_operation (tree arg1, tree arg2, tree dest,
+ binary_func bin_func);
+
+ /* Performs AND operation on given values. The result is stored in dest. */
+ void do_and (value *arg1, value *arg2, tree dest);
+
+ /* Performs OR operation on given values. The result is stored in dest. */
+ void do_or (value *arg1, value *arg2, tree dest);
+
+ /* Performs XOR operation on given values. The result is stored in dest. */
+ void do_xor (value *arg1, value *arg2, tree dest);
+
+ /* Performs shift right operation on given values.
+ The result is stored in dest. */
+ void do_shift_right (value *arg1, value *arg2, tree dest);
+
+ /* Performs shift left operation on given values.
+ The result is stored in dest. */
+ void do_shift_left (value *arg1, value *arg2, tree dest);
+
+ /* Adds given values. The result is stored in dest. */
+ void do_add (value *arg1, value *arg2, tree dest);
+
+ /* Subtracks second value from the first. The result is stored in dest. */
+ void do_sub (value *arg1, value *arg2, tree dest);
+
+ /* Performs AND operation on two bits. */
+ static value_bit *and_two_bits (value_bit *arg1, value_bit *arg2);
+
+ /* ANDs every bit of the value with var_bit, stroes the result in var1. */
+ void and_number_bit (value *var1, value_bit *var_bit);
+
+ /* Multiplies given values. The result is stored in dest. */
+ void do_mul (value *arg1, value *arg2, tree dest);
+
+ /* Performs AND operation for 2 symbolic_bit operands. */
+ static value_bit *and_sym_bits (const value_bit *var1,
+ const value_bit *var2);
+
+ /* Performs AND operation for a symbolic_bit and const_bit operands. */
+ static value_bit *and_var_const (const value_bit *var1,
+ const bit *const_bit);
+
+ /* Performs AND operation for 2 constant bit operands. */
+ static bit *and_const_bits (const bit *const_bit1, const bit *const_bit2);
+
+ /* Performs OR operation on two bits. */
+ static value_bit *or_two_bits (value_bit *arg1_bit, value_bit *arg2_bit);
+
+ /* Performs OR operation for 2 symbolic_bit operands. */
+ static value_bit *or_sym_bits (const value_bit *var1,
+ const value_bit *var2);
+
+ /* Performs OR operation for a symbolic_bit and a constant bit operands. */
+ static value_bit *or_var_const (const value_bit *var1,
+ const bit *const_bit);
+
+ /* Performs OR operation for 2 constant bit operands. */
+ static bit *or_const_bits (const bit *const_bit1, const bit *const_bit2);
+
+ /* Performs complement operation on a bit. */
+ static value_bit *complement_a_bit (value_bit *var);
+
+ /* Performs NOT operation for constant bit. */
+ static bit *complement_const_bit (const bit *const_bit);
+
+ /* Performs NOT operation for symbolic_bit. */
+ static value_bit *complement_sym_bit (const value_bit *var);
+
+ /* Performs XOR operation on two bits. */
+ static value_bit *xor_two_bits (value_bit *var1, value_bit *var2);
+
+ /* Performs XOR operation for 2 symbolic_bit operands. */
+ static value_bit *xor_sym_bits (const value_bit *var1,
+ const value_bit *var2);
+
+ /* Performs XOR operation for 2 constant bit operands. */
+ static bit *xor_const_bits (const bit *const_bit1, const bit *const_bit2);
+
+ /* Performs XOR operation for a symbolic_bit and const_bit operands. */
+ static value_bit *xor_var_const (const value_bit *var,
+ const bit *const_bit);
+
+ /* Shift_right operation. Case: var2 is a symbolic value. */
+ static value_bit *shift_right_sym_bits (value_bit *var1, value_bit *var2);
+
+ /* Shift_left operation. Case: var2 is a symbolic value. */
+ static value_bit *shift_left_sym_bits (value_bit *var1, value_bit *var2);
+
+ /* Shifts var right by size of shift_value. */
+ value *shift_right_by_const (value *var, size_t shift_value);
+
+ /* Return node which has a const bit child. Traversal is done based
+ on safe branching. */
+ static void get_parent_with_const_child (value_bit *root,
+ bit_expression *&parent,
+ bit_expression *&parent_of_parent);
+
+ /* Checks whether state for variable with specified name already
+ exists or not. */
+ bool is_declared (tree var);
+
+ /* Declares given variable if it has not been declared yet. */
+ void declare_if_needed (tree var, size_t size);
+
+ /* Shifts number left by size of shift_value. */
+ value *shift_left_by_const (const value *number, size_t shift_value);
+
+ /* Adds two bits and carry value.
+ Resturn result and stores new carry bit in "carry". */
+ static value_bit *full_adder (value_bit *var1, value_bit *var2,
+ value_bit **carry);
+
+ /* Returns the additive inverse of the given number. */
+ value *additive_inverse (const value *number);
+
+ /* Adds two values, stores the result in the first one. */
+ void add_numbers (value *var1, const value *var2);
+
+ /* Make a copy of given bits. */
+ static vec<value_bit *> *make_copy (vec<value_bit *> *bits);
+
+ public:
+ state () = default;
+
+ ~state ();
+
+ /* Adds an empty state for the given variable. */
+ bool decl_var (tree name, unsigned size);
+
+ state (const state &s);
+
+ /* Adds the given variable to state. */
+ bool add_var_state (tree var, value *state);
+
+ /* Remove all states from the states' vector. */
+ static void remove_states (vec<state *> *states);
+
+ /* Remove all states from the states' vector and release the vector. */
+ static void clear_states (vec<state *> *states);
+
+ /* Removes all variables added to the state. */
+ void clear_var_states ();
+
+ /* Removes all conditions added to the state. */
+ void clear_conditions ();
+
+ /* Adds the given condition to the state. */
+ bool add_condition (bit_expression *cond);
+
+ /* Bulk add the given conditions to the state. */
+ bool bulk_add_conditions (const hash_set<bit_expression *> &conds);
+
+ /* Get value of the given variable. */
+ value *get_value (tree var);
+
+ /* Get the value of the tree, which is in the beginning of the var_states. */
+ value *get_first_value ();
+
+ /* Returns the list of conditions in the state. */
+ const hash_set<bit_expression *> &get_conditions ();
+
+ /* Adds a variable with unknown value to state. Such variables are
+ represented as sequence of symbolic bits. */
+ bool make_symbolic (tree var, unsigned size);
+
+ /* Returns size of the given variable. */
+ unsigned get_var_size (tree var);
+
+ /* Prints the given value. */
+ static void print_value (value *var);
+
+ /* Prints added conditions. */
+ void print_conditions ();
+
+ /* Returns the number represented by the value. */
+ static unsigned HOST_WIDE_INT
+ make_number (const value *var);
+
+ /* Checks if all bits of the given value have constant bit type. */
+ static bool is_bit_vector (const value *var);
+
+ /* Performs the specified operation on passed variables. */
+ bool do_operation (tree_code op_code, tree arg1, tree arg2, tree dest);
+
+ /* Does Assignment. */
+ bool do_assign (tree arg, tree dest);
+
+ /* Assigns pow 2 value. */
+ bool do_assign_pow2 (tree dest, unsigned pow);
+
+ /* Negates given variable. */
+ bool do_complement (tree arg, tree dest);
+
+ /* Adds EQUAL condition of given variables to state. */
+ bool add_equal_cond (tree arg1, tree arg2);
+
+ /* Adds NOT EQUAL condition of given variables to state. */
+ bool add_not_equal_cond (tree arg1, tree arg2);
+
+ /* Adds GREATER THAN condition of given variables to state. */
+ bool add_greater_than_cond (tree arg1, tree arg2);
+
+ /* Adds LESS THAN condition of given variables to state. */
+ bool add_less_than_cond (tree arg1, tree arg2);
+
+ /* Adds GREATER OR EQUAL condition of given variables to state. */
+ bool add_greater_or_equal_cond (tree arg1, tree arg2);
+
+ /* Adds LESS OR EQUAL condition of given variables to state. */
+ bool add_less_or_equal_cond (tree arg1, tree arg2);
+
+ /* Adds a bool condition to state. */
+ bool add_bool_cond (tree arg);
+
+ /* Checks whether the given two constant values are equal. */
+ static bool check_const_value_equality (value *arg1, value *arg2);
+
+ /* Checks whether the given two constant values are not equal. */
+ static bool check_const_value_are_not_equal (value *arg1, value *arg2);
+
+ /* Checks whether the first given constant value
+ is greater than the second one. */
+ static bool check_const_value_is_greater_than (value *arg1, value *arg2);
+
+ /* Checks whether the first given constant value
+ is less than the second one. */
+ static bool check_const_value_is_less_than (value *arg1, value *arg2);
+
+ /* For the given value_bit, iterates over its expression tree, complements
+ those bit which came from the given origin. */
+ static value_bit *complement_bits_with_origin (value_bit *root, tree origin);
+
+ /* Iterates over every bit of the given value and complements their
+ expression trees' those bits, that came from the given origin. */
+ static void complement_val_bits_with_origin (value *val, tree origin);
+
+ /* Complements all bits of all values that came from the given origin. */
+ void complement_all_vars_bits_with_origin (tree origin);
+
+ /* Complements all bits with the given origin of all added conditions. */
+ void complement_conditions_with_origin (tree origin);
+
+ /* Complements all bits with the given origin of all values
+ and added conditions. */
+ void complement_state_with_origin (tree origin);
+
+ /* Returns status of last added condition. */
+ condition_status get_last_cond_status ();
+};
+
+
+size_t min (size_t a, size_t b, size_t c);
+
+
+/* Performs the given operation on passed arguments.
+ The result is stored in dest. */
+
+template<class func>
+void
+state::operate (value *arg1, value *arg2, value_bit **bit_arg, tree dest,
+ func bit_op)
+{
+ value *dest_var = var_states.get (dest);
+ size_t min_iter = min (arg1->length (), arg2->length (), dest_var->length ());
+
+ size_t i = 0;
+ for (; i < min_iter; i++)
+ {
+ value_bit *temp = (*var_states.get (dest))[i];
+ (*var_states.get (dest))[i] = operate_bits (bit_op, (*arg1)[i],
+ (*arg2)[i], bit_arg);
+ delete temp;
+ }
+
+ if (i >= dest_var->length ())
+ return;
+
+ value *biggest = arg1;
+ value_bit *sign_bit = (*arg2)[i - 1];
+ if (arg2->length () > arg1->length ())
+ {
+ biggest = arg2;
+ sign_bit = (*arg1)[i - 1];
+ }
+
+ min_iter = min (biggest->length (), dest_var->length (), dest_var->length ());
+ for (; i < min_iter; i++)
+ {
+ value_bit *temp = (*var_states.get (dest))[i];
+ (*var_states.get (dest))[i] = operate_bits (bit_op, (*biggest)[i],
+ sign_bit, bit_arg);
+ delete temp;
+ }
+
+ if (i >= dest_var->length ())
+ return;
+
+ sign_bit = (*biggest)[i - 1];
+ for (; i < dest_var->length (); i++)
+ {
+ value_bit *temp = (*var_states.get (dest))[i];
+ (*var_states.get (dest))[i] = operate_bits (bit_op, sign_bit, sign_bit,
+ bit_arg);
+ delete temp;
+ }
+}
+
+#endif /* SYM_EXEC_STATE_H. */
Add symbolic execution support. Gives an opportunity to execute the code on bit level, assigning symbolic values to the variables which don't have initial values. Supports only CRC specific operations. Example: uint8_t crc; uint8_t pol = 1; crc = crc ^ pol; during symbolic execution crc's value will be: crc(8), crc(7), ... crc(1), crc(0) ^ 1 gcc/ * Makefile.in (OBJS): Add sym-exec/sym-exec-expression.o, sym-exec/sym-exec-state.o, sym-exec/sym-exec-condition.o. * configure (sym-exec): New subdir. gcc/sym-exec/ * sym-exec-condition.cc: New file. * sym-exec-condition.h: New file. * sym-exec-expression-is-a-helper.h: New file. * sym-exec-expression.cc: New file. * sym-exec-expression.h: New file. * sym-exec-state.cc: New file. * sym-exec-state.h: New file.