Branch data Line data Source code
1 : : /* Execute symbolically all paths of the loop.
2 : : Copyright (C) 2022-2024 Free Software Foundation, Inc.
3 : : Contributed by Mariam Arutunian <mariamarutunian@gmail.com>
4 : :
5 : : This file is part of GCC.
6 : :
7 : : GCC is free software; you can redistribute it and/or modify it under
8 : : the terms of the GNU General Public License as published by the Free
9 : : Software Foundation; either version 3, or (at your option) any later
10 : : version.
11 : :
12 : : GCC is distributed in the hope that it will be useful, but WITHOUT ANY
13 : : WARRANTY; without even the implied warranty of MERCHANTABILITY or
14 : : FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
15 : : for more details.
16 : :
17 : : You should have received a copy of the GNU General Public License
18 : : along with GCC; see the file COPYING3. If not see
19 : : <http://www.gnu.org/licenses/>. */
20 : :
21 : : #ifndef GCC_CRC_VERIFICATION
22 : : #define GCC_CRC_VERIFICATION
23 : :
24 : : #include "config.h"
25 : : #include "system.h"
26 : : #include "coretypes.h"
27 : : #include "backend.h"
28 : : #include "cfgloop.h"
29 : : #include "sym-exec/sym-exec-state.h"
30 : :
31 : : class crc_symbolic_execution {
32 : :
33 : : private:
34 : : /* A vector of states to keep the current state of each executed path. */
35 : : vec<state *> m_states;
36 : :
37 : : /* A vector of final states
38 : : to keep the returned_value and path conditions. */
39 : : vec<state *> m_final_states;
40 : :
41 : : /* Potential CRC loop, which must be executed symbolically,
42 : : to check whether it calculates CRC. */
43 : : class loop *m_crc_loop;
44 : :
45 : : /* Output CRC from the last block of the loop. */
46 : : gphi *m_output_crc;
47 : :
48 : : /* Indicates whether the loop execution brought to loop exit.
49 : : I.e. the condition of the loop is false. */
50 : : bool m_is_last_iteration;
51 : :
52 : : /* Returns true if the variable is used outside the loop.
53 : : Otherwise, returns false. */
54 : : bool is_used_outside_the_loop (tree);
55 : :
56 : : /* Add next basic blocks of the conditional block
57 : : for the execution path into the stack.
58 : : If the condition depends on symbolic values, keep both edges.
59 : : If the condition is true, keep true edge, else - false edge.
60 : : Returns true if addition succeed. Otherwise - false. */
61 : : bool add_next_bbs (basic_block, state *, auto_vec<edge> &);
62 : :
63 : : /* Keep conditions depending on symbolic variables in the states. */
64 : : static bool add_condition (const gcond *, state *, state *);
65 : :
66 : : /* The function adds E edge into the STACK if it doesn't have an immediate
67 : : successor back edge.
68 : :
69 : : When loop counter is checked in the if condition,
70 : : we mustn't continue on real path as we want to stop the execution before
71 : : the second iteration. */
72 : : bool add_edge (edge, auto_vec<edge> &);
73 : :
74 : : /* Create new state for true and false branch.
75 : : Keep conditions in new created states. */
76 : : bool resolve_condition (const gcond *, auto_vec<edge> &);
77 : :
78 : : /* If final states are less than two, adds new FINAL_STATE and returns true.
79 : : Otherwise, returns false.
80 : : In CRC cases we detect may not occur more than two final states. */
81 : : bool add_final_state (state *);
82 : :
83 : : /* Keep the state of the executed path in final states. */
84 : : bool keep_states ();
85 : :
86 : : bool execute_assign_statement (const gassign *);
87 : :
88 : : /* Execute gimple statements of the basic block.
89 : : Keeping values of variables in the state. */
90 : : bool execute_bb_gimple_statements (basic_block, auto_vec<edge> &);
91 : :
92 : : /* Assign values of phi instruction to its result.
93 : : Keep updated values in the state. */
94 : : bool execute_bb_phi_statements (basic_block, edge);
95 : :
96 : : /* Execute all statements of the basic block.
97 : : Keeping values of variables in the state. */
98 : : bool execute_bb_statements (basic_block, edge, auto_vec<edge> &);
99 : :
100 : : /* Create initial state of the loop's header BB variables which have constant
101 : : values.
102 : : If it is the first iteration of the loop, initialise variables with the
103 : : initial values, otherwise initialise the variable with the value calculated
104 : : during the previous execution. */
105 : : state *create_initial_state (class loop *);
106 : :
107 : : /* Traverse function fun's all paths from the first basic block to the last.
108 : : Each time iterate loops only once.
109 : : Symbolically execute statements of each path. */
110 : : bool traverse_function (function *);
111 : :
112 : : /* Execute the loop, which calculates crc with initial values,
113 : : to calculate the polynomial. */
114 : : bool execute_crc_loop (gphi *, gphi *, bool);
115 : :
116 : : public:
117 : :
118 : : /* Returns calculated polynomial by executing the loop
119 : : with concrete values.
120 : : First value of the pair is the tree containing the value of the polynomial,
121 : : second is the calculated polynomial. The pair may contain nullptr. */
122 : : std::pair <tree, value *>
123 : : extract_polynomial (gphi *, gphi *, tree, bool);
124 : :
125 : : /* Symbolically execute the CRC loop, doing one iteration. */
126 : : bool symb_execute_crc_loop ();
127 : :
128 : 3021 : const vec<state *> &get_final_states ()
129 : : {
130 : 3021 : return m_final_states;
131 : : }
132 : :
133 : 3240 : bool is_last_iteration ()
134 : : {
135 : 3240 : return m_is_last_iteration;
136 : : }
137 : :
138 : 477 : crc_symbolic_execution (class loop *loop, gphi * output_crc) :
139 : 477 : m_crc_loop (loop), m_output_crc (output_crc), m_is_last_iteration (false)
140 : : {
141 : : /* Reserve memory for the vectors of states. */
142 : 477 : int max_states = 2;
143 : 477 : m_states.create (max_states);
144 : 477 : m_final_states.create (max_states);
145 : 477 : }
146 : :
147 : 477 : ~crc_symbolic_execution ()
148 : : {
149 : : /* Free memory. */
150 : 477 : state::clear_states (&m_states);
151 : 477 : state::clear_states (&m_final_states);
152 : 258 : }
153 : : };
154 : :
155 : :
156 : : /**************************** LFSR MATCHING *********************************/
157 : :
158 : : /* Returns true if all states match the LFSR, otherwise - false. */
159 : : bool all_states_match_lfsr (value *, bool, tree, const vec<state *> &);
160 : :
161 : :
162 : : #endif //GCC_CRC_VERIFICATION
|
