1 files changed, 162 insertions, 0 deletions
diff --git a/gcc/crc-verification.h b/gcc/crc-verification.h
new file mode 100644
index 0000000..d802f4d
--- /dev/null
+++ b/gcc/crc-verification.h
@@ -0,0 +1,162 @@
+/* Execute symbolically all paths of the loop.
+   Copyright (C) 2022-2024 Free Software Foundation, Inc.
+   Contributed by Mariam Arutunian <mariamarutunian@gmail.com>
+
+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