---
 gcc/Makefile.in                |    1 +
 gcc/crc-verification.cc        | 1298 ++++++++++++++++++++++++++++++++
 gcc/crc-verification.h         |  161 ++++
 gcc/gimple-crc-optimization.cc |  327 +++++++-
 gcc/sym-exec/sym-exec-state.cc |  101 +++
 gcc/sym-exec/sym-exec-state.h  |   11 +
 6 files changed, 1897 insertions(+), 2 deletions(-)
 create mode 100644 gcc/crc-verification.cc
 create mode 100644 gcc/crc-verification.h

diff --git a/gcc/Makefile.in b/gcc/Makefile.in
index 6eab34d62bb..6b8a37a180c 100644
--- a/gcc/Makefile.in
+++ b/gcc/Makefile.in
@@ -1717,6 +1717,7 @@ OBJS = \
 	tree-iterator.o \
 	tree-logical-location.o \
 	tree-loop-distribution.o \
+	crc-verification.o \
 	gimple-crc-optimization.o \
 	sym-exec/sym-exec-expression.o \
 	sym-exec/sym-exec-state.o \
diff --git a/gcc/crc-verification.cc b/gcc/crc-verification.cc
new file mode 100644
index 00000000000..a556bc92467
--- /dev/null
+++ b/gcc/crc-verification.cc
@@ -0,0 +1,1298 @@
+/* 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;
+
+  if (gimple_num_ops (gs) != 2 && gimple_num_ops (gs) != 3)
+    {
+      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;
+    }
+
+  tree op1 = gimple_assign_rhs1 (gs);
+  tree op2 = nullptr;
+
+  if (gimple_num_ops (gs) == 3)
+    op2 = gimple_assign_rhs2 (gs);
+
+  state *current_state = m_states.last ();
+  return current_state->do_operation (rhs_code, op1, op2, lhs);
+}
+
+/* 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_operation (VAR_DECL, rhs, nullptr, 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, class loop *crc_loop)
+{
+  basic_block bb = crc_loop->header;
+  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;
+
+      tree inital_val = PHI_ARG_DEF_FROM_EDGE (phi,
+					       loop_preheader_edge (crc_loop));
+      if (TREE_CODE (inital_val) == 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_operation (VAR_DECL, inital_val,
+			       nullptr, 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,
+				 class loop *crc_loop)
+{
+  basic_block bb = crc_loop->header;
+  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;
+      tree inital_val = PHI_ARG_DEF_FROM_EDGE (phi,
+					       loop_preheader_edge (crc_loop));
+      if (TREE_CODE (inital_val) == INTEGER_CST)
+	{
+	  tree input_tree = PHI_ARG_DEF_FROM_EDGE (phi,
+						   loop_latch_edge (crc_loop));
+	  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_operation (VAR_DECL, calc_num_tree, nullptr, lhs);
+	    }
+	}
+    }
+  return true;
+}
+
+/* Create initial state of the CRC_LOOP's 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 (class loop *crc_loop)
+{
+  state *curr_state = new state;
+  if (!m_final_states.is_empty ())
+    {
+      if (!assign_calc_vals_to_header_phis (m_final_states, curr_state,
+					    crc_loop))
+	return nullptr;
+      state::remove_states (&m_final_states);
+    }
+  else
+    assign_known_vals_to_header_phis (curr_state, crc_loop);
+  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");
+
+  state *curr_state = create_initial_state (m_crc_loop);
+  if (!curr_state)
+    return false;
+
+  m_states.quick_push (curr_state);
+
+  auto_vec<edge> stack (m_crc_loop->num_nodes);
+
+  basic_block header_bb = m_crc_loop->header;
+  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, class loop *crc_loop,
+			    gphi *crc_phi, gphi *data_phi,
+			    bool is_shift_left)
+{
+  basic_block bb = crc_loop->header;
+  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_operation (VAR_DECL,
+					  build_zero_cst (TREE_TYPE (lhs)),
+					  nullptr, lhs);
+	}
+      else
+	{
+	  edge loop_preheader = loop_preheader_edge (crc_loop);
+	  tree inital_val = PHI_ARG_DEF_FROM_EDGE (phi, loop_preheader);
+	  if (TREE_CODE (inital_val) == 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_operation (VAR_DECL, inital_val,
+					      nullptr, 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_operation (VAR_DECL,
+					      build_zero_cst (TREE_TYPE (lhs)),
+					      nullptr, 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 (), m_crc_loop, 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,
+					    tree calculated_crc,
+					    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 ();
+
+  /* CALCULATED_CRC contains the value of the polynomial
+     after one iteration of the loop.  */
+  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 (tree calculated_crc, state *curr_state)
+{
+  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, tree calculated_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 (calculated_crc, final_states[0]);
+  value *crc_not_xor_value = get_crc_val (calculated_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..4aa275d625e
--- /dev/null
+++ b/gcc/crc-verification.h
@@ -0,0 +1,161 @@
+/* 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/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 the loop's 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 (class loop *);
+
+/* 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 *, tree, 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, tree, const vec<state *> &);
+
+
+#endif //GCC_CRC_VERIFICATION
diff --git a/gcc/gimple-crc-optimization.cc b/gcc/gimple-crc-optimization.cc
index c67b0fd38c3..a05aaf9f217 100644
--- a/gcc/gimple-crc-optimization.cc
+++ b/gcc/gimple-crc-optimization.cc
@@ -31,9 +31,19 @@ along with GCC; see the file COPYING3.  If not see
 #include "tree-cfg.h"
 #include "cfgloop.h"
 #include "tree-scalar-evolution.h"
+#include "crc-verification.h"
 
 class crc_optimization {
  private:
+  /* Record of statements already seen.  */
+  bitmap m_visited_stmts;
+
+  /* Input CRC of the loop.  */
+  tree m_crc_arg;
+
+  /* Input data of the loop.  */
+  tree m_data_arg;
+
   /* The statement doing shift 1 operation before/after xor operation.  */
   gimple *m_shift_stmt;
 
@@ -47,6 +57,9 @@ class crc_optimization {
   /* The loop, which probably calculates CRC.  */
   class loop *m_crc_loop;
 
+  /* Polynomial used in CRC calculation.  */
+  unsigned HOST_WIDE_INT m_polynomial;
+
   /* Depending on the value of M_IS_BIT_FORWARD, may be forward or reversed CRC.
      If M_IS_BIT_FORWARD, then it is bit-forward implementation,
      otherwise bit-reversed.  */
@@ -65,6 +78,15 @@ 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).
      This may filter out some real CRCs, where more than one condition
@@ -179,9 +201,33 @@ 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);
+
+  /* Validates CRC and data arguments and
+   sets them for potential CRC loop replacement.
+
+   The function extracts the CRC and data arguments from PHI nodes and
+   performs several checks to ensure that the CRC and data are suitable for
+   replacing the CRC loop with a more efficient implementation.
+
+  Returns true if the arguments are valid and the loop replacement is possible,
+  false otherwise.  */
+  bool validate_crc_and_data ();
+
+  /* Convert polynomial to unsigned HOST_WIDE_INT.  */
+  void construct_constant_polynomial (value *polynomial);
+
+  /* Returns phi statement which may hold the calculated CRC.  */
+  gphi *get_output_phi ();
+
  public:
   crc_optimization () : m_visited_stmts (BITMAP_ALLOC (NULL)),
-			m_crc_loop (nullptr)
+			m_crc_loop (nullptr), m_polynomial (0)
   {
     set_initial_values ();
   }
@@ -705,6 +751,8 @@ crc_optimization::cond_depends_on_crc (auto_vec<gimple *>& stmts)
 void
 crc_optimization::set_initial_values ()
 {
+  m_crc_arg = nullptr;
+  m_data_arg = nullptr;
   m_shift_stmt = nullptr;
   m_phi_for_crc = nullptr;
   m_phi_for_data = nullptr;
@@ -933,6 +981,240 @@ 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.  */
+      tree calculated_crc = PHI_ARG_DEF_FROM_EDGE (output_crc,
+						   single_exit (m_crc_loop));
+      if (!all_states_match_lfsr (lfsr, m_is_bit_forward, calculated_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)
+{
+  tree crc_of_exit
+    = PHI_ARG_DEF_FROM_EDGE (output_crc, single_exit (m_crc_loop));
+  tree crc_of_latch
+    = PHI_ARG_DEF_FROM_EDGE (m_phi_for_crc, loop_latch_edge (m_crc_loop));
+  if (crc_of_exit == crc_of_latch)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	{
+	  fprintf (dump_file, "Output CRC is ");
+	  print_gimple_expr (dump_file, (gimple *) output_crc, dump_flags);
+	  fprintf (dump_file, "\n");
+	}
+      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)
+{
+  tree crc_of_exit
+    = PHI_ARG_DEF_FROM_EDGE (output_crc, single_exit (m_crc_loop));
+  edge crc_loop_latch = loop_latch_edge (m_crc_loop);
+  if (crc_of_exit != PHI_ARG_DEF_FROM_EDGE (m_phi_for_crc, crc_loop_latch))
+    {
+      if (m_phi_for_data
+	  && crc_of_exit == PHI_ARG_DEF_FROM_EDGE (m_phi_for_data,
+						   crc_loop_latch))
+	{
+	  std::swap (m_phi_for_crc, m_phi_for_data);
+	}
+    }
+}
+
+/* Validates CRC and data arguments and
+   sets them for potential CRC loop replacement.
+
+   The function extracts the CRC and data arguments from PHI nodes and
+   performs several checks to ensure that the CRC and data are suitable for
+   replacing the CRC loop with a more efficient implementation.
+
+  Returns true if the arguments are valid and the loop replacement is possible,
+  false otherwise.  */
+
+bool crc_optimization::validate_crc_and_data ()
+{
+  /* Set m_crc_arg and check if fits in word_mode.  */
+  gcc_assert (m_phi_for_crc);
+  m_crc_arg = PHI_ARG_DEF_FROM_EDGE (m_phi_for_crc,
+				     loop_preheader_edge (m_crc_loop));
+  gcc_assert (m_crc_arg);
+
+  if (GET_MODE_SIZE (TYPE_MODE (TREE_TYPE (m_crc_arg))).to_constant ()
+      > GET_MODE_SIZE (word_mode))
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file, "word_mode is less than CRC mode.\n");
+      return false;
+    }
+
+  unsigned HOST_WIDE_INT
+  data_size = tree_to_uhwi (m_crc_loop->nb_iterations) + 1;
+  /* We don't support the case where data is larger than the CRC.  */
+  if (TYPE_PRECISION (TREE_TYPE (m_crc_arg)) < data_size)
+    return false;
+
+  /* Set m_data_arg if a PHI node for data exists,
+     and check its size against loop iterations.
+     This is the case when data and CRC are XOR-ed in the loop.  */
+  if (m_phi_for_data)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+	fprintf (dump_file,
+		 "Data and CRC are xor-ed in the for loop.  Initializing data "
+		 "with its value.\n");
+      m_data_arg = PHI_ARG_DEF_FROM_EDGE (m_phi_for_data,
+					  loop_preheader_edge (m_crc_loop));
+      gcc_assert (m_data_arg);
+      if (TYPE_PRECISION (TREE_TYPE (m_data_arg)) != data_size)
+	{
+	  if (dump_file && (dump_flags & TDF_DETAILS))
+	    fprintf (dump_file,
+		     "Loop iteration number and data's size differ.\n");
+	  return false;
+	}
+	return true;
+    }
+  return true;
+}
+
+/* Convert polynomial to unsigned HOST_WIDE_INT.  */
+
+void
+crc_optimization::construct_constant_polynomial (value *polynomial)
+{
+  m_polynomial = 0;
+  for (unsigned i = 0; i < (*polynomial).length (); i++)
+    {
+      value_bit *const_bit;
+      if (m_is_bit_forward)
+	const_bit = (*polynomial)[(*polynomial).length () - 1 - i];
+      else
+	const_bit = (*polynomial)[i];
+      m_polynomial <<= 1;
+      m_polynomial ^= (as_a<bit *> (const_bit))->get_val () ? 1 : 0;
+    }
+}
+
+/* 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)
 {
@@ -948,7 +1230,48 @@ 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)
+	    break;
+
+	  swap_crc_and_data_if_needed (output_crc);
+	  if (!is_output_crc (output_crc))
+	    break;
+	  if (!validate_crc_and_data ())
+	    break;
+
+	  edge loop_latch = loop_latch_edge (m_crc_loop);
+	  tree calced_crc = PHI_ARG_DEF_FROM_EDGE (m_phi_for_crc, loop_latch);
+	  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,
+							      calced_crc,
+							      m_is_bit_forward);
+
+	  value *polynom_value = calc_polynom.second;
+	  /* Stop analysis if we couldn't get the polynomial's value.  */
+	  if (!polynom_value)
+	    break;
+
+	  /* Stop analysis in case optimize_size is specified
+	     and table-based would be generated.  This check is only needed for
+	     TARGET_CRC case, as polynomial's value isn't known in the
+	     beginning.  */
+	  construct_constant_polynomial (polynom_value);
+
+	  if (!loop_calculates_crc (output_crc, calc_polynom))
+	    break;
+
+	  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/sym-exec-state.cc b/gcc/sym-exec/sym-exec-state.cc
index 15df4d6a87e..5962a3d0bf2 100644
--- a/gcc/sym-exec/sym-exec-state.cc
+++ b/gcc/sym-exec/sym-exec-state.cc
@@ -1894,6 +1894,55 @@ state::print_value (value *var)
 }
 
 
+/* 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
@@ -1908,6 +1957,58 @@ last_set_bit (const value &polynomial)
 }
 
 
+/* 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/sym-exec-state.h b/gcc/sym-exec/sym-exec-state.h
index 5a3f9ebbbff..2fd4805f46a 100644
--- a/gcc/sym-exec/sym-exec-state.h
+++ b/gcc/sym-exec/sym-exec-state.h
@@ -247,6 +247,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;
 
@@ -374,6 +382,9 @@ class state {
 
   /* Returns status of last added condition.  */
   condition_status get_last_cond_status ();
+
+  /* Create LFSR value.  */
+  static value *create_lfsr (tree crc, value *polynomial, bool is_bit_forward);
 };
 
 
-- 
2.25.1

