History

verification/rvgen: Remove the old state variables

The state variables (states, initial_state, final_states) only capture the states' names and have less information than their Lark-based counterparts. Switch to use the new state variables and delete these old ones.

Nam Cao committed 4 months ago

Commit 7edaba01 parent cad252d3 files · +13 −14Browse files

Unified · Split

3 files
  1. tools/verification/rvgen/rvgen/automata.py +4 −5
  2. tools/verification/rvgen/rvgen/dot2c.py +5 −5
  3. tools/verification/rvgen/rvgen/dot2k.py +4 −4
tools/verification/rvgen/rvgen/automata.py+4−5
@@ -411,8 +411,7 @@ class Automata: · 410 unmodified lines
411 self.__dot_lines = self.__open_dot()411 self.__dot_lines = self.__open_dot()
412 self.__parse_tree = ParseTree(file_path)412 self.__parse_tree = ParseTree(file_path)
413 self.transitions = self.__parse_transitions()413 self.transitions = self.__parse_transitions()
414 self._states, self._initial_state, self._final_states = self.__parse_states()414 self.states, self.initial_state, self.final_states = self.__parse_states()
415 self.states, self.initial_state, self.final_states = self.__get_state_variables()
416 self.env_types = {}415 self.env_types = {}
417 self.env_stored = set()416 self.env_stored = set()
418 self.constraint_vars = set()417 self.constraint_vars = set()
@@ -603,7 +602,7 @@ class Automata: · 184 unmodified lines
603 envs.append(c.env)602 envs.append(c.env)
604 self.__extract_env_var(c)603 self.__extract_env_var(c)
605 604
606 for state in self._states:605 for state in self.states:
607 if state.inv:606 if state.inv:
608 envs.append(state.inv.env)607 envs.append(state.inv.env)
609 self.__extract_env_var(state.inv)608 self.__extract_env_var(state.inv)
@@ -639,7 +638,7 @@ class Automata: · 29 unmodified lines
639 def __create_matrix(self) -> list[list[str]]:638 def __create_matrix(self) -> list[list[str]]:
640 # transform the array into a dictionary639 # transform the array into a dictionary
641 events = self.events640 events = self.events
642 states = [s.name for s in self._states]641 states = [s.name for s in self.states]
643 events_dict = {}642 events_dict = {}
644 states_dict = {}643 states_dict = {}
645 nr_event = 0644 nr_event = 0
@@ -675,7 +674,7 @@ class Automata: · 29 unmodified lines
675 for j in range(len(self.states)):674 for j in range(len(self.states)):
676 if self.function[j][i] != self.invalid_state_str:675 if self.function[j][i] != self.invalid_state_str:
677 curr_event_used += 1676 curr_event_used += 1
678 if self.function[j][i] == self.initial_state:677 if self.function[j][i] == self.initial_state.name:
679 curr_event_will_init += 1678 curr_event_will_init += 1
680 if self.function[0][i] != self.invalid_state_str:679 if self.function[0][i] != self.invalid_state_str:
681 curr_event_from_init = True680 curr_event_from_init = True
tools/verification/rvgen/rvgen/dot2c.py+5−5
@@ -29,10 +29,10 @@ class Dot2c(Automata): · 28 unmodified lines
29 29
30 def __get_enum_states_content(self) -> list[str]:30 def __get_enum_states_content(self) -> list[str]:
31 buff = []31 buff = []
32 buff.append(f"\t{self.initial_state}{self.enum_suffix},")32 buff.append(f"\t{self.initial_state.name}{self.enum_suffix},")
33 for state in self.states:33 for state in self.states:
34 if state != self.initial_state:34 if state != self.initial_state:
35 buff.append(f"\t{state}{self.enum_suffix},")35 buff.append(f"\t{state.name}{self.enum_suffix},")
36 buff.append(f"\tstate_max{self.enum_suffix},")36 buff.append(f"\tstate_max{self.enum_suffix},")
37 37
38 return buff38 return buff
@@ -142,7 +142,7 @@ class Dot2c(Automata): · 103 unmodified lines
142 def format_aut_init_states_string(self) -> list[str]:142 def format_aut_init_states_string(self) -> list[str]:
143 buff = []143 buff = []
144 buff.append("\t.state_names = {")144 buff.append("\t.state_names = {")
145 buff.append(self.__get_string_vector_per_line_content(self.states))145 buff.append(self.__get_string_vector_per_line_content([s.name for s in self.states]))
146 buff.append("\t},")146 buff.append("\t},")
147 147
148 return buff148 return buff
@@ -159,7 +159,7 @@ class Dot2c(Automata): · 10 unmodified lines
159 return buff159 return buff
160 160
161 def __get_max_strlen_of_states(self) -> int:161 def __get_max_strlen_of_states(self) -> int:
162 max_state_name = len(max(self.states, key=len))162 max_state_name = max((len(s.name) for s in self.states))
163 return max(max_state_name, len(self.invalid_state_str))163 return max(max_state_name, len(self.invalid_state_str))
164 164
165 def get_aut_init_function(self) -> str:165 def get_aut_init_function(self) -> str:
@@ -199,7 +199,7 @@ class Dot2c(Automata): · 33 unmodified lines
199 return buff199 return buff
200 200
201 def get_aut_init_initial_state(self) -> str:201 def get_aut_init_initial_state(self) -> str:
202 return self.initial_state202 return self.initial_state.name
203 203
204 def format_aut_init_initial_state(self) -> list[str]:204 def format_aut_init_initial_state(self) -> list[str]:
205 buff = []205 buff = []
tools/verification/rvgen/rvgen/dot2k.py+4−4
@@ -179,7 +179,7 @@ class ha2k(dot2k): · 178 unmodified lines
179 self.trace_h = self._read_template_file("trace_hybrid.h")179 self.trace_h = self._read_template_file("trace_hybrid.h")
180 self.has_invariant = False180 self.has_invariant = False
181 self.has_guard = False181 self.has_guard = False
182 for state in self._states:182 for state in self.states:
183 if state.inv:183 if state.inv:
184 self.has_invariant = True184 self.has_invariant = True
185 for transition in self.transitions:185 for transition in self.transitions:
@@ -318,7 +318,7 @@ f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, · 132 unmodified lines
318{{"""]318{{"""]
319 319
320 _else = ""320 _else = ""
321 for state in self._states:321 for state in self.states:
322 if not state.inv:322 if not state.inv:
323 continue323 continue
324 324
@@ -386,7 +386,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon, · 61 unmodified lines
386 buff.append(f"\tif ({condition_str})\n\t\treturn;")386 buff.append(f"\tif ({condition_str})\n\t\treturn;")
387 387
388 _else = ""388 _else = ""
389 for state in self._states:389 for state in self.states:
390 inv = state.inv390 inv = state.inv
391 if not inv:391 if not inv:
392 continue392 continue
@@ -395,7 +395,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon, · 2 unmodified lines
395 buff.append(f"\t\t{inv};")395 buff.append(f"\t\t{inv};")
396 _else = "else "396 _else = "else "
397 397
398 for state in self._states:398 for state in self.states:
399 inv = state.inv399 inv = state.inv
400 if not inv:400 if not inv:
401 continue401 continue