Symbolically execute potential CRC loops and check whether the loop
actually calculates CRC (uses LFSR matching).
Calculated CRC and created LFSR are compared on each iteration of the
potential CRC loop.

  gcc/

    * Makefile.in (OBJS): Add crc-verification.o.
    * crc-verification.cc: New file.
    * crc-verification.h: New file.
    * gimple-crc-optimization.cc (loop_calculates_crc): New function.
    (is_output_crc): Likewise.
    (swap_crc_and_data_if_needed): Likewise.
    (get_output_phi): Likewise.
    (execute): Add check whether potential CRC loop calculates CRC.

  gcc/sym-exec/

    * state.cc (create_reversed_lfsr): New function.
    (create_forward_lfsr): Likewise.
    (last_set_bit): Likewise.
    (create_lfsr): Likewise.
    * state.h (is_bit_vector): Reorder, make the function public and static.
    (create_reversed_lfsr): New static function declaration.
    (create_forward_lfsr): New static function declaration.

Signed-off-by: Mariam Arutunian <mariamarutun...@gmail.com>
diff --git a/gcc/Makefile.in b/gcc/Makefile.in
index aab909c3510..1996a60078c 100644
--- a/gcc/Makefile.in
+++ b/gcc/Makefile.in
@@ -1716,6 +1716,7 @@ OBJS = \
 	tree-iterator.o \
 	tree-logical-location.o \
 	tree-loop-distribution.o \
+	crc-verification.o \
 	gimple-crc-optimization.o \
 	sym-exec/expression.o \
 	sym-exec/state.o \
diff --git a/gcc/crc-verification.cc b/gcc/crc-verification.cc
new file mode 100644
index 00000000000..0922199d377
--- /dev/null
+++ b/gcc/crc-verification.cc
@@ -0,0 +1,1331 @@
+/* Execute symbolically all paths of the loop.
+   Calculate the value of the polynomial by executing loop with real values to
+   create LFSR state.
+   After each iteration check that final states of calculated CRC values match
+   determined LFSR.
+   Copyright (C) 2022-2024 Free Software Foundation, Inc.
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it under
+the terms of the GNU General Public License as published by the Free
+Software Foundation; either version 3, or (at your option) any later
+version.
+
+GCC is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.   */
+
+#include "crc-verification.h"
+#include "config.h"
+#include "system.h"
+#include "coretypes.h"
+#include "backend.h"
+#include "tree.h"
+#include "gimple.h"
+#include "ssa.h"
+#include "gimple-iterator.h"
+#include "tree-cfg.h"
+#include "cfganal.h"
+#include "tree-ssa-loop.h"
+
+/* Check whether defined variable is used outside the loop, only
+   CRC's definition is allowed to be used outside the loop.  */
+
+bool
+crc_symbolic_execution::is_used_outside_the_loop (tree def)
+{
+  imm_use_iterator imm_iter;
+  gimple *use_stmt;
+  FOR_EACH_IMM_USE_STMT (use_stmt, imm_iter, def)
+    {
+      if (!flow_bb_inside_loop_p (m_crc_loop, use_stmt->bb))
+	{
+	  if (is_a<gphi *> (use_stmt)
+	      && as_a<gphi *> (use_stmt) == m_output_crc)
+	    return false;
+	  if (dump_file)
+	    fprintf (dump_file, "Defined variable is used outside the loop.\n");
+	  return true;
+	}
+    }
+  return false;
+}
+
+/* Calculate value of the rhs operation of GS assigment statement
+   and assign it to lhs variable.  */
+
+bool
+crc_symbolic_execution::execute_assign_statement (const gassign *gs)
+{
+  enum tree_code rhs_code = gimple_assign_rhs_code (gs);
+  tree lhs = gimple_assign_lhs (gs);
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file, "lhs type : %s \n",
+	     get_tree_code_name (TREE_CODE (lhs)));
+
+  /* This will filter some normal cases too.  Ex.  usage of array.  */
+  if (TREE_CODE (lhs) != SSA_NAME)
+    return false;
+
+  /* Check uses only when m_output_crc is known.  */
+  if (m_output_crc)
+    if (is_used_outside_the_loop (lhs))
+      return false;
+
+  state *current_state = m_states.last ();
+
+  if (gimple_num_ops (gs) == 2)
+    {
+      tree op1 = gimple_assign_rhs1 (gs);
+      switch (rhs_code)
+	{
+	  case BIT_NOT_EXPR:
+	    return current_state->do_complement (op1, lhs);
+	  case NOP_EXPR:
+	  case SSA_NAME:
+	  case VAR_DECL:
+	  case INTEGER_CST:
+	    return current_state->do_assign (op1, lhs);
+	  default:
+	    {
+	      if (dump_file)
+		fprintf (dump_file,
+			 "Warning, encountered unsupported unary operation "
+			 "with %s code while executing assign statement!\n",
+			 get_tree_code_name (rhs_code));
+	      return false;
+	    }
+	}
+    }
+  else if (gimple_num_ops (gs) == 3)
+    {
+      tree op1 = gimple_assign_rhs1 (gs);
+      tree op2 = gimple_assign_rhs2 (gs);
+      switch (rhs_code)
+	{
+	  case LSHIFT_EXPR:
+	    return current_state->do_shift_left (op1, op2, lhs);
+	  case RSHIFT_EXPR:
+	    return current_state->do_shift_right (op1, op2, lhs);
+	  case BIT_AND_EXPR:
+	    return current_state->do_and (op1, op2, lhs);
+	  case BIT_IOR_EXPR:
+	    return current_state->do_or (op1, op2, lhs);
+	  case BIT_XOR_EXPR:
+	    return current_state->do_xor (op1, op2, lhs);
+	  case PLUS_EXPR:
+	    return current_state->do_add (op1, op2, lhs);
+	  case MINUS_EXPR:
+	    return current_state->do_sub (op1, op2, lhs);
+	  case MULT_EXPR:
+	    return current_state->do_mul (op1, op2, lhs);
+	  default:
+	    {
+	      if (dump_file)
+		fprintf (dump_file,
+			 "Warning, encountered unsupported binary operation "
+			 "with %s code while executing assign statement!\n",
+			 get_tree_code_name (rhs_code));
+	      return false;
+	    }
+	}
+    }
+  else
+    {
+      if (dump_file)
+	fprintf (dump_file,
+		 "Warning, encountered unsupported operation, "
+		 "with %s code while executing assign statement!\n",
+		 get_tree_code_name (rhs_code));
+      return false;
+    }
+  return true;
+}
+
+/* Add E edge into the STACK if it doesn't have an immediate
+   successor edge going to the loop header.
+
+   When loop counter is checked in the if condition,
+   we mustn't continue on real path as we want to stop the execution before
+   the second iteration.  */
+
+bool
+crc_symbolic_execution::add_edge (edge e, auto_vec<edge> &stack)
+{
+  if (EDGE_COUNT (e->dest->succs) == 0)
+    return false;
+
+  edge next_bb_edge = EDGE_SUCC (e->dest, 0);
+  if (next_bb_edge && next_bb_edge->dest == m_crc_loop->header)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Completed one iteration.  "
+			    "Won't iterate loop once more, yet.\n");
+
+      return keep_states ();
+    }
+  else
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Adding the edge into the stack.\n");
+
+      /* If the result of the condition is true/false,
+	 continue execution only by the true/false branch.  */
+      stack.quick_push (e);
+    }
+  return true;
+}
+
+/* Add next basic blocks of the conditional block COND_BB
+   for the execution path into the STACK.
+   If the condition depends on symbolic values, keep both edges.
+   If the condition is true, keep true edge, else - false edge.
+   Returns true if addition succeeds.  Otherwise - false.  */
+
+bool
+crc_symbolic_execution::add_next_bbs (basic_block cond_bb,
+				      state *new_branch_state,
+				      auto_vec<edge> &stack)
+{
+  edge true_edge;
+  edge false_edge;
+  extract_true_false_edges_from_block (cond_bb, &true_edge, &false_edge);
+
+  /* When the condition depends on symbolic values.  */
+  if (new_branch_state->get_last_cond_status () == CS_SYM)
+    {
+      /* Supported CRC cases may have only two states.  */
+      if (m_states.length () == 2)
+	{
+	  if (dump_file && (dump_flags & TDF_DETAILS))
+	    fprintf (dump_file, "Going to add a new state, "
+				"but there's already two states.\n");
+	  return false;
+	}
+      /* Add true branch's state into the states.
+	 False branch's state will be kept in the current state.  */
+      m_states.quick_push (new_branch_state);
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Adding true and false edges into the stack.\n");
+
+      /* Add outgoing edges to the stack.  */
+      stack.quick_push (false_edge);
+      stack.quick_push (true_edge);
+
+      return true;
+    }
+  /* When the condition evaluates to true.  */
+  else if (new_branch_state->get_last_cond_status () == CS_TRUE)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Condition is true.\n");
+      add_edge (true_edge, stack);
+    }
+  /* When the condition evaluates to false.  */
+  else if (new_branch_state->get_last_cond_status () == CS_FALSE)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Condition is false.\n");
+      add_edge (false_edge, stack);
+    }
+  else
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Something went wrong "
+			    "during handling conditional statement.\n");
+      return false;
+    }
+
+  /* When we continue execution of only one path,
+     there's no need of new state.  */
+  delete new_branch_state;
+  return true;
+}
+
+/* Add conditions depending on symbolic variables in the states.
+
+   Keep conditions of each branch execution in its state.
+     Ex.
+       if (a == 0)  // a's value is unknown
+
+       new_branch_state.keep (a==0)
+       current_state.keep (a!=0)
+
+     The condition is kept in the bit level.
+     For ex.
+     If a's size is 8 and its value is {symb_a, 0, 0, 0, 0, 0, 0, 0},
+     then for a == 0 we'll have symb_a == 0 condition.  */
+
+bool
+crc_symbolic_execution::add_condition (const gcond *cond,
+				       state *current_state,
+				       state *new_branch_state)
+{
+  tree lhs = gimple_cond_lhs (cond);
+  tree rhs = gimple_cond_rhs (cond);
+  switch (gimple_cond_code (cond))
+    {
+      case EQ_EXPR:
+	{
+	  new_branch_state->add_equal_cond (lhs, rhs);
+	  if (new_branch_state->get_last_cond_status () == CS_SYM)
+	    current_state->add_not_equal_cond (lhs, rhs);
+	  return true;
+	}
+      case NE_EXPR:
+	{
+	  new_branch_state->add_not_equal_cond (lhs, rhs);
+	  if (new_branch_state->get_last_cond_status () == CS_SYM)
+	    current_state->add_equal_cond (lhs, rhs);
+	  return true;
+	}
+      case GT_EXPR:
+	{
+	  new_branch_state->add_greater_than_cond (lhs, rhs);
+	  if (new_branch_state->get_last_cond_status () == CS_SYM)
+	    current_state->add_less_or_equal_cond (lhs, rhs);
+	  return true;
+	}
+      case LT_EXPR:
+	{
+	  new_branch_state->add_less_than_cond (lhs, rhs);
+	  if (new_branch_state->get_last_cond_status () == CS_SYM)
+	    current_state->add_greater_or_equal_cond (lhs, rhs);
+	  return true;
+	}
+      case GE_EXPR:
+	{
+	  new_branch_state->add_greater_or_equal_cond (lhs, rhs);
+	  if (new_branch_state->get_last_cond_status () == CS_SYM)
+	    current_state->add_less_than_cond (lhs, rhs);
+	  return true;
+	}
+      case LE_EXPR:
+	{
+	  new_branch_state->add_less_or_equal_cond (lhs, rhs);
+	  if (new_branch_state->get_last_cond_status () == CS_SYM)
+	    current_state->add_greater_than_cond (lhs, rhs);
+	  return true;
+	}
+      default:
+	{
+	  if (dump_file && (dump_flags & TDF_DETAILS))
+	    fprintf (dump_file, "Unsupported condition.\n");
+	  return false;
+	}
+    }
+}
+
+/* Create new states for true and false branches.
+   Keep conditions in new created states.  */
+
+bool
+crc_symbolic_execution::resolve_condition (const gcond *cond,
+					   auto_vec<edge> &stack)
+{
+  state *current_state = m_states.last ();
+  state *new_branch_state = new state (*current_state);
+
+  /* Create new states and for true and false branches keep corresponding
+     conditions.  */
+  if (!add_condition (cond, current_state, new_branch_state))
+    return false;
+
+  /* Add true and false edges to the stack.  */
+  return add_next_bbs (cond->bb, new_branch_state, stack);
+}
+
+/* If final states are less than two, add new FINAL_STATE and return true.
+   Otherwise, return false.
+   Supported CRC cases may not have more than two final states.  */
+bool crc_symbolic_execution::add_final_state (state *final_state)
+{
+  if (m_final_states.length () < 2)
+      m_final_states.quick_push (final_state);
+  else
+    {
+      if (dump_file)
+	fprintf (dump_file,
+		 "There are already two final states\n");
+      return false;
+    }
+    return true;
+}
+
+/* Keep the state of the executed path in final states.  */
+
+bool crc_symbolic_execution::keep_states ()
+{
+  if (m_states.is_empty ())
+    return false;
+
+  if (!add_final_state (m_states.last ()))
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Couldn't add final state.\n");
+      return false;
+    }
+
+  m_states.pop ();
+  return true;
+}
+
+/* Execute gimple statements of BB.
+   Keeping values of variables in the state.  */
+
+bool
+crc_symbolic_execution::execute_bb_gimple_statements (basic_block bb,
+						      auto_vec<edge> &stack)
+{
+  for (gimple_stmt_iterator bsi = gsi_start_bb (bb);
+       !gsi_end_p (bsi); gsi_next (&bsi))
+    {
+      gimple *gs = gsi_stmt (bsi);
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	{
+	  fprintf (dump_file, "Executing ");
+	  print_gimple_stmt (dump_file, gs, dump_flags);
+	}
+      switch (gimple_code (gs))
+	{
+	  case GIMPLE_ASSIGN:
+	    {
+	      if (!execute_assign_statement (as_a<const gassign *> (gs)))
+		return false;
+	      break;
+	    }
+	  case GIMPLE_COND:
+	    {
+	      return resolve_condition (as_a<const gcond *> (gs), stack);
+	    }
+	  /* Just skip debug statements.  */
+	  case GIMPLE_DEBUG:
+	    break;
+	  default:
+	    {
+	      if (dump_file)
+		fprintf (dump_file,
+			 "Warning, encountered unsupported statement, "
+			 "while executing gimple statements!\n");
+	      return false;
+	    }
+	}
+    }
+
+  /* Add each outgoing edge of the current block to the stack,
+     despite the edges going to the loop header.
+     This code isn't reachable if the last statement of the basic block
+     is a conditional statement or return statement.
+     Those cases are handled separately.
+     We mustn't encounter edges going to the CRC loop header.  */
+
+  edge out_edge;
+  edge_iterator ei;
+  FOR_EACH_EDGE (out_edge, ei, bb->succs)
+    if (out_edge->dest != m_crc_loop->header)
+      stack.quick_push (out_edge);
+    else
+      return false;
+
+  return true;
+}
+
+/* Assign values of phi instruction to its result.
+   Keep updated values in the state.  */
+
+bool
+crc_symbolic_execution::execute_bb_phi_statements (basic_block bb,
+						   edge incoming_edge)
+{
+  for (gphi_iterator gsi = gsi_start_phis (bb); !gsi_end_p (gsi);
+       gsi_next (&gsi))
+    {
+      gphi *phi = gsi.phi ();
+      tree lhs = gimple_phi_result (phi);
+
+      /* Check uses only when m_output_crc is known.  */
+      if (m_output_crc)
+	if (is_used_outside_the_loop (lhs))
+	  return false;
+
+      /* Don't consider virtual operands.  */
+      if (virtual_operand_p (lhs))
+	continue;
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	{
+	  fprintf (dump_file, "Determining the value "
+			      "for the following phi.\n");
+	  print_gimple_stmt (dump_file, phi, dump_flags);
+	}
+
+      tree rhs = PHI_ARG_DEF_FROM_EDGE (phi, incoming_edge);
+
+      state *current_state = m_states.last ();
+      if (!current_state->do_assign (rhs, lhs))
+	return false;
+    }
+  return true;
+}
+
+/* Execute all statements of BB.
+   Keeping values of variables in the state.  */
+
+bool
+crc_symbolic_execution::execute_bb_statements (basic_block bb,
+					       edge incoming_edge,
+					       auto_vec<edge> &stack)
+{
+  if (!execute_bb_phi_statements (bb, incoming_edge))
+    return false;
+
+  return execute_bb_gimple_statements (bb, stack);
+}
+
+/* If the phi statements' result variables have initial constant value in the
+   beginning of the loop, initialize those variables.  */
+
+void
+assign_known_vals_to_header_phis (state *state, basic_block bb)
+{
+  for (gphi_iterator gsi = gsi_start_phis (bb); !gsi_end_p (gsi);
+       gsi_next (&gsi))
+    {
+
+      gphi *phi = gsi.phi ();
+      tree lhs = gimple_phi_result (phi);
+
+      /* Don't consider virtual operands.  */
+      if (virtual_operand_p (lhs))
+	continue;
+
+      if (TREE_CODE (PHI_ARG_DEF (phi, phi->nargs - 1)) == INTEGER_CST)
+	{
+	  if (dump_file && (dump_flags & TDF_DETAILS))
+	    {
+	      fprintf (dump_file, "First value of phi is a constant, "
+				  "assigning the number to ");
+	      print_generic_expr (dump_file, lhs, dump_flags);
+	      fprintf (dump_file, " variable.\n");
+	    }
+	  state->do_assign (PHI_ARG_DEF (phi, phi->nargs - 1), lhs);
+	}
+    }
+}
+
+/* If the phi statements' result variables have initial constant value in the
+   beginning of the loop, initialize those variables with
+   the value calculated during the previous iteration.  */
+
+bool
+assign_calc_vals_to_header_phis (const vec<state *> &prev_states,
+				 state *curr_state,
+				 basic_block bb)
+{
+  for (gphi_iterator gsi = gsi_start_phis (bb); !gsi_end_p (gsi);
+       gsi_next (&gsi))
+    {
+      gphi *phi = gsi.phi ();
+      tree lhs = gimple_phi_result (phi);
+
+      /* Don't consider virtual operands.  */
+      if (virtual_operand_p (lhs))
+	continue;
+
+      if (TREE_CODE (PHI_ARG_DEF (phi, phi->nargs - 1)) == INTEGER_CST)
+	{
+	  tree input_tree = PHI_ARG_DEF (phi, 0);
+	  value * val_st1 = prev_states[0]->get_value (input_tree),
+	      *val_st2 = prev_states[1]->get_value (input_tree);
+	  if (!state::is_bit_vector (val_st1)
+	      || !state::is_bit_vector (val_st2))
+	    {
+	      if (dump_file && (dump_flags & TDF_DETAILS))
+		{
+		  fprintf (dump_file, "The calculated values of  ");
+		  print_generic_expr (dump_file, input_tree, dump_flags);
+		  fprintf (dump_file, " variable is not constant.\n");
+		}
+	      return false;
+	    }
+	  else if (!state::check_const_value_equality (val_st1, val_st2))
+	    {
+	      if (dump_file && (dump_flags & TDF_DETAILS))
+		{
+		  fprintf (dump_file, "The calculated values of  ");
+		  print_generic_expr (dump_file, input_tree, dump_flags);
+		  fprintf (dump_file, " variable is different in the previous "
+				      "iteration paths.\n");
+		}
+	      return false;
+	    }
+	  else
+	    {
+	      if (dump_file && (dump_flags & TDF_DETAILS))
+		{
+		  fprintf (dump_file, "Assigning calculated number to ");
+		  print_generic_expr (dump_file, lhs, dump_flags);
+		  fprintf (dump_file, " variable.\n");
+		}
+	      unsigned HOST_WIDE_INT calc_number
+		  = state::make_number (val_st1);
+	      tree calc_num_tree = build_int_cstu (TREE_TYPE (lhs),
+						   calc_number);
+	      curr_state->do_assign (calc_num_tree, lhs);
+	    }
+	}
+    }
+  return true;
+}
+
+/* Create initial state of header BB variables which have constant values.
+   If it is the first iteration of the loop, initialise variables with the
+   initial values, otherwise initialise the variable with the value calculated
+   during the previous execution.  */
+
+state *
+crc_symbolic_execution::create_initial_state (basic_block bb)
+{
+  state *curr_state = new state;
+  if (!m_final_states.is_empty ())
+    {
+      if (!assign_calc_vals_to_header_phis (m_final_states, curr_state, bb))
+	return nullptr;
+      state::remove_states (&m_final_states);
+    }
+  else
+    assign_known_vals_to_header_phis (curr_state, bb);
+  return curr_state;
+}
+
+/* Symbolically execute the CRC loop, doing one iteration.  */
+
+bool
+crc_symbolic_execution::symb_execute_crc_loop ()
+{
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file, "\n\nExecuting the loop with symbolic values.\n\n");
+
+  basic_block header_bb = m_crc_loop->header;
+  state *curr_state = create_initial_state (header_bb);
+  if (!curr_state)
+    return false;
+
+  m_states.quick_push (curr_state);
+
+  auto_vec<edge> stack (m_crc_loop->num_nodes);
+
+  if (!execute_bb_gimple_statements (header_bb, stack))
+    return false;
+
+  /* Successor BB's are added into the stack
+     from the execute_bb_gimple_statements function.  */
+  while (!stack.is_empty ())
+    {
+      /* Look at the edge on the top of the stack.  */
+      edge e = stack.last ();
+      stack.pop ();
+
+      /* Get destination block of the edge.  */
+      basic_block dest_bb = e->dest;
+
+      /* Execute only basic blocks of the m_crc_loop.
+	 At the end of the execution path save states in final states.  */
+      if (!flow_bb_inside_loop_p (m_crc_loop, dest_bb))
+	{
+	  m_is_last_iteration = true;
+	  if (!keep_states ())
+	    return false;
+	  continue;
+	}
+
+      /* Execute statements.  */
+      if (!execute_bb_statements (dest_bb, e, stack))
+	return false;
+    }
+  return true;
+}
+
+/* Determine which bit of the DATA must be 1.
+   We assume that last bit must be 1.  */
+
+unsigned HOST_WIDE_INT
+determine_index (tree data, bool is_shift_left)
+{
+  if (is_shift_left)
+   /* This won't work correctly in the case when data's size is larger,
+      but MSB is checked for the middle bit.  */
+    return tree_to_uhwi (TYPE_SIZE (TREE_TYPE (data))) - 1;
+  return 0;
+}
+
+/* Assign appropriate values to data, CRC
+   and other phi results to calculate the polynomial.  */
+
+void
+assign_vals_to_header_phis (state *polynomial_state, basic_block bb,
+			    gphi *crc_phi, gphi *data_phi,
+			    bool is_shift_left)
+{
+  for (gphi_iterator gsi = gsi_start_phis (bb); !gsi_end_p (gsi);
+       gsi_next (&gsi))
+    {
+
+      gphi *phi = gsi.phi ();
+      tree lhs = gimple_phi_result (phi);
+
+      /* Don't consider virtual operands.  */
+      if (virtual_operand_p (lhs))
+	continue;
+
+      if ((data_phi && phi == data_phi) || (!data_phi && phi == crc_phi))
+	{
+	  if (dump_file && (dump_flags & TDF_DETAILS))
+	    {
+	      fprintf (dump_file, "Assigning the required value to ");
+	      print_generic_expr (dump_file, lhs, dump_flags);
+	      fprintf (dump_file, " variable.\n");
+	    }
+	  polynomial_state->do_assign_pow2 (lhs,
+					    determine_index (lhs,
+							     is_shift_left));
+	}
+      else if (phi == crc_phi)
+	{
+	  if (dump_file && (dump_flags & TDF_DETAILS))
+	    {
+	      fprintf (dump_file, "Assigning 0 value to ");
+	      print_generic_expr (dump_file, lhs, dump_flags);
+	      fprintf (dump_file, " variable.\n");
+	    }
+	  polynomial_state->do_assign (build_zero_cst (TREE_TYPE (lhs)), lhs);
+	}
+      else if (TREE_CODE (PHI_ARG_DEF (phi, phi->nargs - 1)) == INTEGER_CST)
+	{
+	  if (dump_file && (dump_flags & TDF_DETAILS))
+	    {
+	      fprintf (dump_file, "First value of phi is a constant, "
+				  "assigning the number to ");
+	      print_generic_expr (dump_file, lhs, dump_flags);
+	      fprintf (dump_file, " variable.\n");
+	    }
+	  polynomial_state->do_assign (PHI_ARG_DEF (phi, phi->nargs - 1), lhs);
+	}
+      else
+	{
+	  if (dump_file && (dump_flags & TDF_DETAILS))
+	    {
+	      fprintf (dump_file, "First value of phi isn't constant, "
+				  "assigning to ");
+	      print_generic_expr (dump_file, lhs, dump_flags);
+	      fprintf (dump_file, " variable.\n");
+	    }
+	  polynomial_state->do_assign (build_zero_cst (TREE_TYPE (lhs)), lhs);
+	}
+    }
+}
+
+/* Execute the loop, which calculates CRC with initial values,
+   to calculate the polynomial.  */
+
+bool
+crc_symbolic_execution::execute_crc_loop (gphi *crc_phi,
+					  gphi *data_phi,
+					  bool is_shift_left)
+{
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file, "\n\nTrying to calculate the polynomial.\n\n");
+
+  m_states.quick_push (new state);
+
+  basic_block bb = m_crc_loop->header;
+  assign_vals_to_header_phis (m_states.last (), bb, crc_phi, data_phi,
+			      is_shift_left);
+
+  auto_vec<edge> stack (m_crc_loop->num_nodes);
+
+  if (!execute_bb_gimple_statements (bb, stack))
+    return false;
+
+  /* stack may not be empty.  Successor BB's are added into the stack
+     from the execute_bb_gimple_statements function.  */
+  while (!stack.is_empty ())
+    {
+      /* Look at the edge on the top of the stack.  */
+      edge e = stack.last ();
+      stack.pop ();
+
+      /* Get dest block of the edge.  */
+      basic_block bb = e->dest;
+
+      /* Execute only basic blocks of the m_crc_loop.  */
+      if (!flow_bb_inside_loop_p (m_crc_loop, bb))
+	continue;
+
+      /* Execute statements.  */
+      if (!execute_bb_statements (bb, e, stack))
+	return false;
+    }
+
+  if (m_final_states.length () != 1)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "The number of states is not one when executed "
+			    "the loop for calculating the polynomial.\n");
+      return false;
+    }
+  return true;
+}
+
+/* Return true if all bits of the POLYNOMIAL are constants (0 or 1).
+   Otherwise return false.  */
+
+bool
+polynomial_is_known (const value *polynomial)
+{
+  for (size_t i = 0; i < polynomial->length (); i++)
+    {
+      if (!is_a<bit *> ((*polynomial)[i]))
+	return false;
+    }
+  return true;
+}
+
+/* Execute the loop, which is expected to calculate CRC,
+   to extract polynomial, assigning real numbers to CRC and data.
+   Returns a pair, first value of the pair is the tree containing
+   the value of the polynomial, second is the calculated polynomial.
+   The pair may contain nullptr.  */
+
+std::pair <tree, value *>
+crc_symbolic_execution::extract_polynomial (gphi *crc_phi, gphi *data_phi,
+					    bool is_shift_left)
+{
+  if (!execute_crc_loop (crc_phi, data_phi, is_shift_left))
+    return std::make_pair (nullptr, nullptr);
+
+  if (m_final_states.length () != 1)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "The number of states isn't one "
+			    "after executing the loop.\n");
+      return std::make_pair (nullptr, nullptr);
+    }
+  state *polynomial_state = m_final_states.last ();
+
+  /* Get the tree which will contain the value of the polynomial
+     at the end of the loop.  */
+  tree calculated_crc = PHI_ARG_DEF (crc_phi, 0);
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "Getting the value of ");
+      print_generic_expr (dump_file, calculated_crc, dump_flags);
+      fprintf (dump_file, " variable.\n");
+    }
+
+  /* Get the value (bit vector) of the tree (it may be the polynomial).  */
+  value *polynomial = polynomial_state->get_value (calculated_crc);
+  if (!polynomial)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Polynomial's value is null.\n");
+      return std::make_pair (nullptr, nullptr);
+    }
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      /* Note: It may not be the real polynomial.
+	 If it's a bit reflected CRC,
+	 then to get a real polynomial,
+	 it must be reflected and 1 bit added.  */
+      fprintf (dump_file, "Polynomial's value is ");
+      state::print_value (polynomial);
+    }
+
+  /* Check that polynomial's all bits are constants.  */
+  if (!polynomial_is_known (polynomial))
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Polynomial's value is not constant.\n");
+      return std::make_pair (nullptr, nullptr);
+    }
+
+  return std::make_pair (calculated_crc, polynomial);
+}
+
+
+/**************************** LFSR MATCHING *********************************/
+
+
+/* Return true if CONST_BIT value equals to 1.
+   Otherwise, return false.  */
+
+bool
+is_one (value_bit *const_bit)
+{
+  return is_a<bit *> (const_bit)
+	 && (as_a<bit *> (const_bit))->get_val () == 1;
+}
+
+/* Return true if BIT is symbolic,
+   its index is same as LFSR bit's index (LFSR_BIT_INDEX)
+   and the origin is same as CRC_ORIGIN.  */
+
+bool
+is_a_valid_symb (value_bit *bit, tree crc_origin, size_t lfsr_bit_index)
+{
+  if (!is_a<symbolic_bit *> (bit))
+    return false;
+
+  symbolic_bit *sym_bit = as_a<symbolic_bit *> (bit);
+  bool is_correct_index = (sym_bit->get_index () == lfsr_bit_index);
+  bool is_same_crc_origin = (sym_bit->get_origin () == crc_origin);
+  return is_correct_index && is_same_crc_origin;
+}
+
+/* Return true if the BIT is a valid crc[LFSR_BIT_INDEX] ^ 1,
+   where i is a whole number and left part's origin is same as CRC_ORIGIN.
+   LFSR_BIT_INDEX is the index of the LFSR bit from the same position as in CRC.
+
+   If there is lfsr[8] at LFSR value vectors' 9-th bit,
+   when in the CRC vectors' 9-th bit's value must be
+   crc[8].
+
+   Otherwise, return false.  */
+
+bool
+is_a_valid_xor_one (value_bit *bit, tree crc_origin, size_t lfsr_bit_index)
+{
+  if (is_a<bit_xor_expression *> (bit))
+    {
+      bit_xor_expression *xor_exp = as_a<bit_xor_expression *> (bit);
+      if (is_one (xor_exp->get_right ()))
+	return is_a_valid_symb (xor_exp->get_left (), crc_origin,
+				lfsr_bit_index);
+      return false;
+    }
+  return false;
+}
+
+/* Return true, if CONDITION_EXP checks CRC's MSB/LSB value
+   (under which xor is/not done).
+   Otherwise, return false.  */
+
+bool
+may_be_xors_condition (tree crc_origin, value_bit *condition_exp,
+		       size_t sb_index)
+{
+  if (!crc_origin)
+    return false;
+
+  if (!condition_exp)
+    return false;
+
+  /* The CONDITION_EXP of CRC may be a symbolic bit, if CRC is xor-ed with
+     the data, and updated CRC's significant bit is checked.
+     So, the CONDITION_EXP will be CRC's condition if it's origin is the same as
+     CRC_ORIGIN, and it's index equals to checked significant bit's index.  */
+  if (is_a<symbolic_bit *> (condition_exp))
+    {
+      symbolic_bit *condition_symbolic = as_a<symbolic_bit *> (condition_exp);
+      return crc_origin == condition_symbolic->get_origin ()
+	     && sb_index == condition_symbolic->get_index ();
+    }
+    /* The CONDITION_EXP of CRC may be a bit_xor_expression,
+       if CRC and data are xor-ed only for significant bit's check.
+       I.e.  CONDITION_EXP in this case may be crc[]^data[].
+       So, the CONDITION_EXP will be CRC's condition if it's left or right
+       part's origin is the same as CRC_ORIGIN, and it's index equals to checked
+       significant bit's index.  */
+  else if (is_a<bit_xor_expression *> (condition_exp))
+    {
+      bit_xor_expression *condition_xor_exp = as_a<bit_xor_expression *>
+	  (condition_exp);
+      if (!(is_a<symbolic_bit *> (condition_xor_exp->get_left ())
+	    && is_a<symbolic_bit *> (condition_xor_exp->get_right ())))
+	return false;
+
+      symbolic_bit *cond_left
+	  = as_a<symbolic_bit *> (condition_xor_exp->get_left ());
+      symbolic_bit *cond_right
+	  = as_a<symbolic_bit *> (condition_xor_exp->get_right ());
+      bool cond_left_is_crc = (crc_origin == cond_left->get_origin ()
+			       && sb_index == cond_left->get_index ());
+      bool cond_right_is_crc = (crc_origin == cond_right->get_origin ()
+				&& sb_index == cond_right->get_index ());
+      return cond_left_is_crc || cond_right_is_crc;
+    }
+  return false;
+}
+
+/* Check whether the condition is checked for significant bit being 0 or 1.
+   If IS_ONE is 1, when check whether the significant bit is 1 (xor branch),
+   if 0, whether the significant bit is 0 (not xor branch).  */
+
+bool
+is_crc_xor_condition (tree crc_origin, unsigned char is_one,
+		      size_t sb_index, state *final_state)
+{
+  /* The CRC cases we detect must contain only one condition related to CRC.  */
+  if (final_state->get_conditions ().elements () != 1)
+    return false;
+
+  auto condition_iter = final_state->get_conditions ().begin ();
+  if (!is_a<bit_condition *> (*condition_iter))
+    return false;
+
+  /* If the condition is for checking MSB/LSB, then
+     if is_one is 1 and the condition is for checking MSB/LSB being one, or
+     if is_one is 0 and condition is for checking MSB/LSB being 0
+     return true, otherwise - false.  */
+  value_bit *cond_exp = (*condition_iter)->get_left ();
+  if (may_be_xors_condition (crc_origin, cond_exp, sb_index))
+    {
+      if (!is_a<bit *> ((*condition_iter)->get_right ()))
+	return false;
+
+      bit_condition *condition = as_a<bit_condition *> (*condition_iter);
+      unsigned char comparison_val
+	  = as_a<bit *> ((*condition_iter)->get_right ())->get_val ();
+      if (condition->get_code () == EQ_EXPR)
+	return comparison_val == is_one;
+      if (condition->get_code () == NE_EXPR)
+	return comparison_val != is_one;
+      return false;
+    }
+  return false;
+}
+
+/* Check whether LSB/MSB of LFSR and calculated (maybe)CRC match.
+   If MSB is checked in the CRC loop, then here we check LSB, or vice versa.
+   CHECKED_SB_VALUE indicates which state of CRC value is checked.
+   If the CHECKED_SB_VALUE is 1 - then xor-ed CRC value is checked,
+   otherwise, not xor-ed is checked.  */
+
+bool
+given_sb_match (value_bit *crc, value_bit *lfsr,
+		unsigned short checked_sb_value)
+{
+  /* If LFSR's MSB/LSB value is a constant (0 or 1),
+     then CRC's MSB/LSB must have the same value.  */
+  if (is_a<bit *> (lfsr))
+    {
+      if (!((is_a<bit *> (crc)
+	     && as_a<bit *> (crc)->get_val ()
+		== as_a<bit *> (lfsr)->get_val ())))
+	return false;
+      return true;
+    }
+    /* If LFSR's MSB/LSB value is a symbolic_bit
+       (that means MSB/LSB of the polynomial is 1),
+       then CRC's MSB/LSB must be equal to CHECKED_SB_VALUE.  */
+  else if (is_a<symbolic_bit *> (lfsr))
+    {
+      if (!(is_a<bit *> (crc)
+	    && (as_a<bit *> (crc)->get_val () == checked_sb_value)))
+	return false;
+      return true;
+    }
+  return false;
+}
+
+/* Check whether significant bit of LFSR and calculated (maybe)CRC match.  */
+
+bool
+sb_match (const value *lfsr, const value *crc_value, size_t sb_index,
+	  size_t it_end, unsigned short value)
+{
+  /* If it's bit-forward CRC, check 0 bit's value.  */
+  if (sb_index == it_end - 1)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Checking 0 bit.\n");
+
+      if (!given_sb_match ((*crc_value)[0], (*lfsr)[0], value))
+	return false;
+    }
+    /* If it's bit-reversed CRC, check last bit's value.  */
+  else if (sb_index == 0)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Checking %zu bit.\n", it_end);
+
+      if (!given_sb_match ((*crc_value)[it_end], (*lfsr)[it_end], value))
+	return false;
+    }
+  else
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Significant bit index is incorrect.\n");
+    }
+  return true;
+}
+
+/* Match the CRC to the LFSR, where CRC's all bit values are
+   symbolic_bit or symbolic_bit ^ 1, besides MSB/LSB (it may be constant).  */
+
+bool
+lfsr_and_crc_bits_match (const value *lfsr, const value *crc_state,
+			 tree crc_origin, size_t i, size_t it_end,
+			 size_t sb_index, unsigned short checked_sb_value)
+{
+
+  /* Check whether significant bits of LFSR and CRC match.  */
+  if (!sb_match (lfsr, crc_state, sb_index, it_end, checked_sb_value))
+    return false;
+
+  for (; i < it_end; i++)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Checking %zu bit.\n", i);
+
+      /* Check the case when in lfsr we have LFSR (i)^LFSR (SBi),
+	 where 0<i<LFSR_size and SBi is the index of MSB/LSB (LFSR_size-1/0).
+	 In that case in crc_state (resulting CRC)
+	 we must have crc (i) ^ 1 case, when condition is true
+	 and crc (i) when condition is false,
+	 (as CRC is xor-ed with the polynomial only if the LSB/MSB is one)
+	 where k is a whole number.  */
+      if (is_a<bit_xor_expression *> ((*lfsr)[i]))
+	{
+	  size_t index = (as_a<bit_xor_expression *> ((*lfsr)[i]))->get_left ()
+	      ->get_index ();
+	  /* Check CRC value of xor branch.  */
+	  if (checked_sb_value == 1)
+	    {
+	      if (!(is_a_valid_xor_one ((*crc_state)[i], crc_origin, index)))
+		return false;
+	    }
+	  else /* Check CRC value of not xor branch.  */
+	    {
+	      if (!(is_a_valid_symb ((*crc_state)[i], crc_origin, index)))
+		return false;
+	    }
+	}
+	/* Check the case when in LFSR we have LFSR (i), where 0<i<LFSR_size.
+	   In that case in resulting CRC we must have crc (i) case,
+	   when condition is true or condition is false.
+	   If we have just LFSR (i), that means polynomial's i +/- 1 bit is 0,
+	   so despite CRC is xor-ed or not, we will have crc (i).  */
+      else if (is_a<symbolic_bit *> ((*lfsr)[i]))
+	{
+	  size_t index = (as_a<symbolic_bit *> ((*lfsr)[i]))->get_index ();
+	  if (!(is_a_valid_symb ((*crc_state)[i], crc_origin, index)))
+	    return false;
+	}
+      else
+	{
+	  if (dump_file && (dump_flags & TDF_DETAILS))
+	    fprintf (dump_file, "Not expected expression in LFSR.\n");
+	  return false;
+	}
+    }
+  return true;
+}
+
+/* Return origin of CRC_BIT.
+   The first tree in loop, from which CRC's calculation is started.  */
+
+tree
+get_origin_of_crc_from_symb_bit (value_bit *crc_bit)
+{
+  if (is_a<symbolic_bit *> (crc_bit))
+    return as_a<symbolic_bit *> (crc_bit)->get_origin ();
+  return nullptr;
+}
+
+/* Return origin of CRC_BIT.  The first tree in loop, from which CRC's
+   calculation is started.  If the CRC_BIT is symbolic value, return its origin,
+   otherwise return its left part's origin (right must be 1 if its CRC's
+   value). */
+
+tree
+get_origin_of_crc (value_bit *crc_bit)
+{
+  tree origin = get_origin_of_crc_from_symb_bit (crc_bit);
+  if (origin)
+    return origin;
+  else if (is_a<bit_xor_expression *> (crc_bit))
+    {
+      value_bit *crc_bit_left
+	  = as_a<bit_xor_expression *> (crc_bit)->get_left ();
+      return get_origin_of_crc_from_symb_bit (crc_bit_left);
+    }
+  return nullptr;
+}
+
+/* Determine and initialize significant bit index
+   (if MSB is checked for CRC, then it's LSB index, and vice versa)
+   and the remaining part's begin and end.
+   SB_INDEX is the significant bit index.
+   IT_BEG is the beginning of the remaining part.
+   IT_END is the end of the remaining part.  */
+
+void
+init_sb_index_and_other_part_begin_end (size_t &it_beg, size_t &it_end,
+					size_t &sb_index, size_t crc_size,
+					bool is_bit_forward)
+{
+  it_end = crc_size;
+  if (is_bit_forward)
+    {
+      sb_index = it_end - 1;
+      it_beg = 1;
+    }
+  else
+    {
+      it_beg = 0;
+      sb_index = 0;
+      --it_end;
+    }
+}
+
+/* Return true if CRC_STATE matches the LFSR, otherwise - false.
+   LFSR - is created LFSR value for the given polynomial and CRC size.
+   CRC_STATE - contains CRC's calculated value and execution path condition.
+   IT_BEG and IT_END - are the border indexes of the value to be matched.
+   SB_INDEX - is the significant bit index of the CRC value,
+	      which will be checked separately.
+	      IF MSB is checked for CRC, when sb_index will be the index of LSB.
+	      Otherwise, will be the index of MSB.
+   CHECKED_SB_VALUE - is the significant bit's value (used for CRC's condition).
+	      If CHECKED_SB_VALUE is 1, it indicates that CRC_STATE is
+	      xor-ed path's state.
+	      If CHECKED_SB_VALUE is 0, then CRC_STATE is the state of the
+	      not xor branch.  */
+
+bool
+lfsr_matches_crc_state (const value *lfsr, state *crc_state, value *crc_value,
+			size_t it_beg, size_t it_end, size_t sb_index,
+			unsigned short checked_sb_value)
+{
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "Starting to match the following CRC value: ");
+      state::print_value (crc_value);
+    }
+
+  /* Get the origin (name) of the calculated CRC value.
+     All bits must have the same origin.  */
+  tree crc_origin = get_origin_of_crc ((*crc_value)[it_beg]);
+  if (!crc_origin)
+    return false;
+
+  if (!is_crc_xor_condition (crc_origin, checked_sb_value, sb_index, crc_state))
+    return false;
+
+  /* Check whether CRC_VALUE and LFSR bits match.  */
+  return lfsr_and_crc_bits_match (lfsr, crc_value, crc_origin,
+				  it_beg, it_end, sb_index, checked_sb_value);
+}
+
+/* Return true if in the CRC_VALUE exists xor expression.
+   Otherwise, return false.  */
+
+bool
+is_xor_state (value *crc_value, size_t it_beg, size_t it_end)
+{
+   for (unsigned j = it_beg; j < it_end; ++j)
+     if ((*crc_value)[j]->get_type () == BIT_XOR_EXPRESSION)
+       return true;
+   return false;
+}
+
+/* Keep the value of calculated CRC.  */
+
+value *
+get_crc_val (const gphi *crc_phi, state *curr_state)
+{
+  tree calculated_crc = PHI_ARG_DEF (crc_phi, 0);
+
+  if (!calculated_crc)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Couldn't get the potential CRC variable.\n");
+      return nullptr;
+    }
+
+  /* When the calculated CRC is constant, it's not possible to determine
+     whether the CRC has been calculated.  */
+  if (TREE_CODE (calculated_crc) == INTEGER_CST)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Calculated CRC is a constant.\n");
+      return nullptr;
+    }
+
+  /* Get calculated return value.  */
+  value * crc_value = curr_state->get_value (calculated_crc);
+
+  if (!crc_value)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "CRC is not in the state.\n");
+      return nullptr;
+    }
+  return crc_value;
+}
+
+/* Return true if all states from the FINAL_STATES match the LFSR,
+   otherwise - false.  */
+
+bool
+all_states_match_lfsr (value *lfsr, bool is_bit_forward, gphi *output_crc,
+		       const vec<state *> &final_states)
+{
+  if (final_states.length () != 2)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "The final states count isn't two.\n");
+      return false;
+    }
+
+  value *crc_xor_value = get_crc_val (output_crc, final_states[0]);
+  value *crc_not_xor_value = get_crc_val (output_crc, final_states[1]);
+
+  /* LFSR's size must be equal to CRC's size.  */
+  if ((crc_xor_value->length () != lfsr->length ())
+      || (crc_not_xor_value->length () != lfsr->length ()))
+    return false;
+
+  /* Depending on whether it is bit-forward or reversed CRC,
+     determine in which significant bit new value is added,
+     to examine that bit separately.
+     If in the CRC algorithm MSB (sb_index) is checked to be one for xor,
+     then here we check LSB separately (marginal bit).
+     If LSB (sb_index) is checked, then we separate MSB (marginal bit).  */
+  size_t it_beg, it_end, sb_index;
+  init_sb_index_and_other_part_begin_end (it_beg, it_end, sb_index,
+					  crc_xor_value->length (),
+					  is_bit_forward);
+
+    size_t xor_st_index = 0, not_xor_st_index = 1;
+  /* If first is not xor's state,
+     then the second state is assumed to be xor's state.  */
+  if (!is_xor_state (crc_xor_value, it_beg, it_end))
+    {
+      std::swap (crc_xor_value, crc_not_xor_value);
+      xor_st_index = 1;
+      not_xor_st_index = 0;
+    }
+
+  /*  If xor-ed CRC value doesn't match the LFSR value, return false.  */
+  if (!lfsr_matches_crc_state (lfsr, final_states[xor_st_index], crc_xor_value,
+			       it_beg, it_end, sb_index, 1))
+    return false;
+
+  /*  If not xor-ed CRC value doesn't match the LFSR value, return false.  */
+  if (!lfsr_matches_crc_state (lfsr, final_states[not_xor_st_index],
+			       crc_not_xor_value, it_beg, it_end, sb_index, 0))
+    return false;
+
+  return true;
+}
\ No newline at end of file
diff --git a/gcc/crc-verification.h b/gcc/crc-verification.h
new file mode 100644
index 00000000000..7a3d4e77a64
--- /dev/null
+++ b/gcc/crc-verification.h
@@ -0,0 +1,160 @@
+/* Execute symbolically all paths of the loop.
+   Copyright (C) 2022-2024 Free Software Foundation, Inc.
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it under
+the terms of the GNU General Public License as published by the Free
+Software Foundation; either version 3, or (at your option) any later
+version.
+
+GCC is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.   */
+
+#ifndef GCC_CRC_VERIFICATION
+#define GCC_CRC_VERIFICATION
+
+#include "config.h"
+#include "system.h"
+#include "coretypes.h"
+#include "backend.h"
+#include "cfgloop.h"
+#include "sym-exec/state.h"
+
+class crc_symbolic_execution {
+
+ private:
+  /* A vector of states to keep the current state of each executed path.  */
+  vec<state *> m_states;
+
+  /* A vector of final states
+     to keep the returned_value and path conditions.  */
+  vec<state *> m_final_states;
+
+  /* Potential CRC loop, which must be executed symbolically,
+     to check whether it calculates CRC.  */
+  class loop *m_crc_loop;
+
+  /* Output CRC from the last block of the loop.  */
+  gphi *m_output_crc;
+
+  /* Indicates whether the loop execution brought to loop exit.
+     I.e. the condition of the loop is false.  */
+  bool m_is_last_iteration;
+
+  /* Returns true if the variable is used outside the loop.
+     Otherwise, returns false.  */
+  bool is_used_outside_the_loop (tree);
+
+  /* Add next basic blocks of the conditional block
+     for the execution path into the stack.
+     If the condition depends on symbolic values, keep both edges.
+     If the condition is true, keep true edge, else - false edge.
+     Returns true if addition succeed.  Otherwise - false.  */
+  bool add_next_bbs (basic_block, state *, auto_vec<edge> &);
+
+  /* Keep conditions depending on symbolic variables in the states.  */
+  static bool add_condition (const gcond *, state *, state *);
+
+  /* The function adds E edge into the STACK if it doesn't have an immediate
+     successor back edge.
+
+     When loop counter is checked in the if condition,
+     we mustn't continue on real path as we want to stop the execution before
+     the second iteration.  */
+  bool add_edge (edge, auto_vec<edge> &);
+
+  /* Create new state for true and false branch.
+     Keep conditions in new created states.  */
+  bool resolve_condition (const gcond *, auto_vec<edge> &);
+
+  /* If final states are less than two, adds new FINAL_STATE and returns true.
+   Otherwise, returns false.
+   In CRC cases we detect may not occur more than two final states.  */
+  bool add_final_state (state *);
+
+  /* Keep the state of the executed path in final states.  */
+  bool keep_states ();
+
+  bool execute_assign_statement (const gassign *);
+
+  /* Execute gimple statements of the basic block.
+     Keeping values of variables in the state.  */
+  bool execute_bb_gimple_statements (basic_block, auto_vec<edge> &);
+
+  /* Assign values of phi instruction to its result.
+     Keep updated values in the state.  */
+  bool execute_bb_phi_statements (basic_block, edge);
+
+  /* Execute all statements of the basic block.
+    Keeping values of variables in the state.  */
+  bool execute_bb_statements (basic_block, edge, auto_vec<edge> &);
+
+  /* Create initial state of header BB variables which have constant values.
+   If it is the first iteration of the loop, initialise variables with the
+   initial values, otherwise initialise the variable with the value calculated
+   during the previous execution.  */
+  state *create_initial_state (basic_block);
+
+/* Traverse function fun's all paths from the first basic block to the last.
+   Each time iterate loops only once.
+   Symbolically execute statements of each path.  */
+  bool traverse_function (function *);
+
+  /* Execute the loop, which calculates crc with initial values,
+   to calculate the polynomial.  */
+  bool execute_crc_loop (gphi *, gphi *, bool);
+
+ public:
+
+  /* Returns calculated polynomial by executing the loop
+     with concrete values.
+     First value of the pair is the tree containing the value of the polynomial,
+     second is the calculated polynomial.  The pair may contain nullptr.  */
+  std::pair <tree, value *>
+  extract_polynomial (gphi *, gphi *, bool);
+
+  /* Symbolically execute the CRC loop, doing one iteration.  */
+  bool symb_execute_crc_loop ();
+
+  const vec<state *> &get_final_states ()
+  {
+    return m_final_states;
+  }
+
+  bool is_last_iteration ()
+  {
+    return m_is_last_iteration;
+  }
+
+  crc_symbolic_execution (class loop *loop, gphi * output_crc) :
+      m_crc_loop (loop), m_output_crc (output_crc), m_is_last_iteration (false)
+  {
+    /* Reserve memory for the vectors of states.  */
+    int max_states = 2;
+    m_states.create (max_states);
+    m_final_states.create (max_states);
+  }
+
+  ~crc_symbolic_execution ()
+  {
+    /* Free memory.  */
+    state::clear_states (&m_states);
+    state::clear_states (&m_final_states);
+  }
+};
+
+
+/**************************** LFSR MATCHING *********************************/
+
+/* Returns true if all states match the LFSR, otherwise - false.  */
+bool all_states_match_lfsr (value *, bool, gphi *, const vec<state *> &);
+
+
+#endif //GCC_CRC_VERIFICATION
diff --git a/gcc/gimple-crc-optimization.cc b/gcc/gimple-crc-optimization.cc
index 4a17fa75930..039506c1059 100644
--- a/gcc/gimple-crc-optimization.cc
+++ b/gcc/gimple-crc-optimization.cc
@@ -34,6 +34,7 @@ along with GCC; see the file COPYING3.  If not see
 #include "gimple-range.h"
 #include "tree-scalar-evolution.h"
 #include "hwint.h"
+#include "crc-verification.h"
 #include "internal-fn.h"
 #include "tree-into-ssa.h"
 #include "tree-ssa-loop-manip.h"
@@ -46,7 +47,6 @@ along with GCC; see the file COPYING3.  If not see
 #include "tree-ssa-dce.h"
 #include "tree-cfgcleanup.h"
 #include "tree.h"
-#include "gimple-pretty-print.h"
 
 class crc_optimization {
  private:
@@ -81,6 +81,14 @@ class crc_optimization {
      Xor must be done under the condition of MSB/LSB being 1.  */
   bool loop_may_calculate_crc (class loop *loop);
 
+  /* Symbolically executes the loop and checks that LFSR and resulting states
+     match.
+     Returns true if it is verified that the loop calculates CRC.
+     Otherwise, return false.
+     OUTPUT_CRC is the phi statement which will hold the calculated CRC value
+     after the loop exit.  */
+  bool loop_calculates_crc (gphi *output_crc,
+			    std::pair<tree, value *> calc_polynom);
 
   /* Returns true if there is only two conditional blocks in the loop
      (one may be for the CRC bit check and the other for the loop counter).
@@ -191,6 +199,16 @@ class crc_optimization {
   /* Prints extracted details of CRC calculation.  */
   void dump_crc_information ();
 
+  /* Returns true if OUTPUT_CRC's result is the input of m_phi_for_crc.
+     Otherwise, returns false.  */
+  bool is_output_crc (gphi *output_crc);
+
+  /* Swaps m_phi_for_crc and m_phi_for_data if they are mixed.  */
+  void swap_crc_and_data_if_needed (gphi *output_crc);
+
+  /* Returns phi statement which may hold the calculated CRC.  */
+  gphi *get_output_phi ();
+
  public:
   unsigned int execute (function *fun);
 };
@@ -898,6 +916,155 @@ crc_optimization::loop_may_calculate_crc (class loop *loop)
   return false;
 }
 
+/* Symbolically executes the loop and checks that LFSR and resulting states
+   match.
+   Returns true if it is verified that the loop calculates CRC.
+   Otherwise, return false.
+   OUTPUT_CRC is the phi statement which will hold the calculated CRC value
+   after the loop exit.  */
+
+bool
+crc_optimization::loop_calculates_crc (gphi *output_crc,
+				       std::pair<tree, value *> calc_polynom)
+{
+  /* Create LFSR state using extracted polynomial.  */
+  value * lfsr = state::create_lfsr (calc_polynom.first, calc_polynom.second,
+				     m_is_bit_forward);
+  if (!lfsr)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Couldn't create LFSR!\n");
+      return false;
+    }
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "\nLFSR value is \n");
+      state::print_value (lfsr);
+    }
+
+  /* Execute the loop with symbolic values
+     (symbolic value is assigned to the variable when its value isn't known)
+     to keep states, for further comparison.  */
+  bool is_crc = true;
+  crc_symbolic_execution loop_executor (m_crc_loop, output_crc);
+  while (!loop_executor.is_last_iteration ())
+    {
+      if (!loop_executor.symb_execute_crc_loop ())
+	{
+	  if (dump_file)
+	    fprintf (dump_file, "\nCRC verification didn't succeed "
+				"during symbolic execution!\n");
+	  is_crc = false;
+	  break;
+	}
+
+      /* Check whether LFSR and obtained states are same.  */
+      if (!all_states_match_lfsr (lfsr, m_is_bit_forward, output_crc,
+				 loop_executor.get_final_states ()))
+	{
+	  if (dump_file && (dump_flags & TDF_DETAILS))
+	    fprintf (dump_file, "Returned state and LFSR differ.\n");
+	  is_crc = false;
+	  break;
+	}
+    }
+  delete lfsr;
+  return is_crc;
+}
+
+/* Returns true if OUTPUT_CRC's result is the input of M_PHI_FOR_CRC.
+  Otherwise, returns false.  */
+
+bool
+crc_optimization::is_output_crc (gphi *output_crc)
+{
+  if (PHI_ARG_DEF (output_crc, 0) == PHI_ARG_DEF (m_phi_for_crc, 0))
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	{
+	  fprintf (dump_file, "Output CRC is ");
+	  print_gimple_expr (dump_file, (gimple *) output_crc, dump_flags);
+	}
+      return true;
+    }
+  else
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Output CRC and determined input CRC "
+			    "differ.\n");
+      return false;
+    }
+}
+
+/* Swaps M_PHI_FOR_CRC and M_PHI_FOR_DATA if they are mixed.  */
+
+void
+crc_optimization::swap_crc_and_data_if_needed (gphi *output_crc)
+{
+  if (PHI_ARG_DEF (output_crc, 0) != PHI_ARG_DEF (m_phi_for_crc, 0))
+    {
+      if (m_phi_for_data
+	  && PHI_ARG_DEF (output_crc, 0) == PHI_ARG_DEF (m_phi_for_data, 0))
+	{
+	  std::swap (m_phi_for_crc, m_phi_for_data);
+	}
+    }
+}
+
+/* Returns phi statement which may hold the calculated CRC.  */
+
+gphi *
+crc_optimization::get_output_phi ()
+{
+  edge loop_exit = single_exit (m_crc_loop);
+  if (!loop_exit)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "The loop doesn't have single exit.\n");
+      return nullptr;
+    }
+  basic_block bb = loop_exit->dest;
+  gphi *output_crc = nullptr;
+  int phi_count = 0;
+
+  /* We are only interested in cases when there is only one phi at the
+   loop exit, and that phi can potentially represent the CRC.
+   If there are other phis present, it indicates that additional values are
+   being calculated within the loop that are used outside it.  */
+  for (gphi_iterator gsi = gsi_start_phis (bb); !gsi_end_p (gsi);
+       gsi_next (&gsi))
+    {
+      tree phi_result = gimple_phi_result (gsi.phi ());
+
+      /* Don't consider virtual operands.  */
+      if (!virtual_operand_p (phi_result))
+	{
+	  if (phi_count < 1)
+	    {
+	      output_crc = gsi.phi ();
+	      phi_count++;
+	    }
+	  else
+	    {
+	      if (dump_file && (dump_flags & TDF_DETAILS))
+		fprintf (dump_file, "There is more than one output phi.\n");
+	      return nullptr;
+	    }
+	}
+    }
+
+  if (output_crc)
+    {
+      if (gimple_phi_num_args (output_crc) == 1)
+	return output_crc;
+    }
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file, "Couldn't determine output CRC.\n");
+  return nullptr;
+}
+
 unsigned int
 crc_optimization::execute (function *fun)
 {
@@ -913,7 +1080,37 @@ crc_optimization::execute (function *fun)
   for (auto loop: loop_list)
     {
       /* Perform initial checks to filter out non-CRCs.  */
-      loop_may_calculate_crc (loop);
+      if (loop_may_calculate_crc (loop))
+	{
+	  /* Get the phi which will hold the calculated CRC.  */
+	  gphi *output_crc = get_output_phi ();
+	  if (!output_crc)
+	    return 0;
+
+	  swap_crc_and_data_if_needed (output_crc);
+	  if (!is_output_crc (output_crc))
+	    return 0;
+
+	  crc_symbolic_execution execute_loop (m_crc_loop, nullptr);
+	  /* Execute the loop assigning specific values to CRC and data
+	     for extracting the polynomial.  */
+	  std::pair <tree, value *>
+	      calc_polynom = execute_loop.extract_polynomial (m_phi_for_crc,
+							      m_phi_for_data,
+							      m_is_bit_forward);
+
+	  value *polynom_value = calc_polynom.second;
+	  /* Stop analysis if we couldn't get the polynomial's value.  */
+	  if (!polynom_value)
+	    return 0;
+
+	  if (!loop_calculates_crc (output_crc, calc_polynom))
+	    return 0;
+
+	  if (dump_file)
+	    fprintf (dump_file, "The loop with %d header BB index "
+				"calculates CRC!\n", m_crc_loop->header->index);
+	}
     }
   return 0;
 }
diff --git a/gcc/sym-exec/state.cc b/gcc/sym-exec/state.cc
index 2b735b9cefc..bb4f49b4c9b 100644
--- a/gcc/sym-exec/state.cc
+++ b/gcc/sym-exec/state.cc
@@ -2033,6 +2033,121 @@ state::do_cast (tree var, tree dest, size_t cast_size)
   return true;
 }
 
+/* Create LFSR value for the reversed CRC.  */
+
+void
+state::create_reversed_lfsr (value &lfsr, const value &crc,
+			     const value &polynomial)
+{
+  size_t size = polynomial.length ();
+
+  /* Determine values of all bits, except MSB.  */
+  for (size_t i = 0; i < size - 1; i++)
+    {
+      if (as_a<bit *> (polynomial[i])->get_val ())
+	lfsr.push (state::xor_two_bits (crc[i + 1], crc[0]));
+      else
+	lfsr.push (crc[i + 1]->copy ());
+    }
+
+  /* Determine value of MSB.  */
+  if (as_a<bit *> (polynomial[size - 1])->get_val ())
+    lfsr.push (crc[0]->copy ());
+  else
+    lfsr.push (new bit (0));
+}
+
+
+/* Create LFSR value for the forward CRC.  */
+
+void
+state::create_forward_lfsr (value &lfsr, const value &crc,
+			    const value &polynomial)
+{
+  size_t size = polynomial.length ();
+  /* Determine value of LSB.  */
+  if (as_a<bit *> (polynomial[0])->get_val ())
+    lfsr.push (crc[size - 1]->copy ());
+  else
+    lfsr.push (new bit (0));
+
+  /* Determine values of remaining bits.  */
+  for (size_t i = 1; i < size; i++)
+    {
+      if (as_a<bit *> (polynomial[i])->get_val ())
+	lfsr.push (state::xor_two_bits (crc[i - 1], crc[size - 1]));
+      else
+	lfsr.push (crc[i - 1]->copy ());
+    }
+}
+
+
+/* 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;
+}
+
+
+/* Create LFSR value.  */
+
+value *
+state::create_lfsr (tree crc, value *polynomial, bool is_bit_forward)
+{
+  /* Check size compatibility․  */
+  unsigned HOST_WIDE_INT polynomial_length = polynomial->length ();
+  unsigned HOST_WIDE_INT crc_size = tree_to_uhwi (TYPE_SIZE (TREE_TYPE (crc)));
+  if (crc_size < polynomial_length)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "LFSR state creation: "
+			    "Polynomial doesn't fit into the crc.\n");
+
+      return nullptr;
+    }
+
+  /* Get the minimal byte size to keep the polynomial.
+ Ie, if the last 1 bit of the polynomial is at 6 index, size will be 8.  */
+  size_t required_polynomial_size = ((last_set_bit (*polynomial)/8) + 1) * 8;
+
+  /* Polynomial's length actually equals to the CRC variable's size.
+ Now we detect only those CRC calculation algorithms, where leading 1 of the
+ polynomial isn't kept.  */
+  if (required_polynomial_size == 0
+      || required_polynomial_size != polynomial_length)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "Polynomial's all bits are zeros "
+			    "or the size of the polynomial is uncertain.\n");
+      return nullptr;
+    }
+
+  /* Create vector of symbolic bits for crc.  */
+  value crc_value (polynomial_length, TYPE_UNSIGNED (TREE_TYPE (crc)));
+
+  for (unsigned HOST_WIDE_INT i = 0; i < polynomial_length; i++)
+    crc_value.push (new symbolic_bit (i, crc));
+
+  /* create LFSR vector.  */
+  value *lfsr = new value (polynomial_length, TYPE_UNSIGNED (TREE_TYPE (crc)));
+
+  /* Calculate values for LFSR.  */
+  if (is_bit_forward)
+    create_forward_lfsr (*lfsr, crc_value, *polynomial);
+  else
+    create_reversed_lfsr (*lfsr, crc_value, *polynomial);
+
+  return lfsr;
+}
+
+
 /* Prints added conditions.  */
 
 void
diff --git a/gcc/sym-exec/state.h b/gcc/sym-exec/state.h
index c8ff065fdaf..b20c8deab2f 100644
--- a/gcc/sym-exec/state.h
+++ b/gcc/sym-exec/state.h
@@ -219,9 +219,6 @@ class state {
   /* Shifts number left by size of shift_value.  */
   value *shift_left_by_const (const value *number, size_t shift_value);
 
-  /* Checks if all bits of the given value have constant bit type.  */
-  bool is_bit_vector (const value *var);
-
   /* 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,
@@ -236,6 +233,14 @@ class state {
   /* Make a copy of given bits.  */
   static vec<value_bit *> *make_copy (vec<value_bit *> *bits);
 
+  /* Create LFSR value for the reversed CRC.  */
+  static void create_reversed_lfsr (value &lfsr, const value &crc,
+				    const value &polynomial);
+
+  /* Create LFSR value for the forward CRC.  */
+  static void create_forward_lfsr (value &lfsr, const value &crc,
+				   const value &polynomial);
+
  public:
   state () = default;
 
@@ -287,6 +292,9 @@ class state {
   /* Prints added conditions.  */
   void print_conditions ();
 
+  /* Checks if all bits of the given value have constant bit type.  */
+  static bool is_bit_vector (const value *var);
+
   /* Returns the number represented by the value.  */
   static unsigned HOST_WIDE_INT
   make_number (const value *var);
-- 
2.25.1

Reply via email to