diff --git a/scripts/mea/core.py b/scripts/mea/core.py index d63ad58..e2acb54 100644 --- a/scripts/mea/core.py +++ b/scripts/mea/core.py @@ -154,7 +154,7 @@ def __convert_call_tree_filter(error_trace: dict, args: dict = None) -> list: # TODO: check this in core (one node for call and return edges). double_funcs = {} for edge in error_trace['edges']: - if 'env' in edge: + if 'entry_point' in edge: continue if 'enter' in edge and 'return' in edge: double_funcs[edge['enter']] = edge['return'] diff --git a/scripts/mea/et/internal_witness.py b/scripts/mea/et/internal_witness.py index 74544a9..2eec0af 100644 --- a/scripts/mea/et/internal_witness.py +++ b/scripts/mea/et/internal_witness.py @@ -61,6 +61,7 @@ def __init__(self, logger): self._model_funcs = {} self._spec_funcs = {} self._env_models = {} + self._env_models_json = {} self._notes = {} self._asserts = {} self._actions = [] @@ -259,6 +260,7 @@ def process_verifier_notes(self): f"'{self._resolve_function(func_id)}'") edge['note'] = self.process_comment(note) if func_id in self._env_models: + # TODO: not supported anymore env_note = self._env_models[func_id] self._logger.debug(f"Add note {env_note} for environment function '" f"{self._resolve_function(func_id)}'") @@ -268,6 +270,11 @@ def process_verifier_notes(self): note = self._notes[file_id][start_line] self._logger.debug(f"Add note {note} for statement from '{file}:{start_line}'") edge['note'] = self.process_comment(note) + elif file_id in self._env_models_json and start_line in self._env_models_json[file_id]: + env = self._env_models_json[file_id][start_line] + self._logger.debug(f"Add EMG comment '{env}' for operation from '{file}:{start_line}'") + edge['env'] = self.process_comment(env) + del self._env_models_json[file_id][start_line] elif file_id in self._asserts and start_line in self._asserts[file_id]: warn = self._asserts[file_id][start_line] self._logger.debug(f"Add warning {warn} for statement from '{file}:{start_line}'") @@ -293,6 +300,7 @@ def process_verifier_notes(self): def _parse_model_comments(self): self._logger.info('Parse model comments from source files referred by witness') emg_comment = re.compile(r'/\*\sLDV\s(.*)\s\*/') + emg_comment_json = re.compile(r'/\*\sEMG_ACTION\s({.*})\s\*/') for file_id, file in self.files: if not os.path.isfile(file): @@ -312,6 +320,16 @@ def _parse_model_comments(self): data = json.loads(match.group(1)) self._add_emg_comment(file_id, line, data) + # Try match JSON EMG comment + match = emg_comment_json.search(text) + if match: + data = json.loads(match.group(1)) + if "comment" in data: + if file_id not in self._env_models_json: + self._env_models_json[file_id] = {} + self._env_models_json[file_id][line + 1] = data["comment"] + # TODO: parse other arguments as well + # Match rest comments match = re.search( rf'/\*\s+({self.MODEL_COMMENT_TYPES})\s+(\S+)\s+(.*)\*/', text) @@ -414,7 +432,7 @@ def final_checks(self, entry_point="main"): 'enter': self.add_function(entry_point), 'start line': 0, 'file': 0, - 'env': 'entry point', + 'entry_point': 'entry point', 'source': f"{entry_point}()" } if not self._threads: diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py index c697217..826005b 100644 --- a/scripts/mea/et/parser.py +++ b/scripts/mea/et/parser.py @@ -275,7 +275,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map): if self.entry_point == function_name: self.internal_witness.is_main_function = True if self.internal_witness.witness_type == 'violation': - _edge['env'] = "entry point" + _edge['entry_point'] = "entry point" is_entry_point = True else: self.internal_witness.is_main_function = True @@ -285,7 +285,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map): _edge['enter'] = func_id if not is_entry_point and \ self.internal_witness.witness_type == 'violation': - _edge['env'] = "entry point" + _edge['entry_point'] = "entry point" self.internal_witness.add_thread("decl") is_entry_point = True elif data_key == 'returnFrom':