diff --git a/scripts/mea/et/internal_witness.py b/scripts/mea/et/internal_witness.py index 7937a04..9eec141 100644 --- a/scripts/mea/et/internal_witness.py +++ b/scripts/mea/et/internal_witness.py @@ -74,7 +74,7 @@ def __init__(self, logger): self._actions = [] self._callback_actions = [] self.aux_funcs = {} - self.emg_comments = {} + self.cif_comments = {} self._threads = [] self.witness_type = None self.invariants = {} @@ -191,11 +191,6 @@ def _add_aux_func(self, identifier, is_callback, formal_arg_names): self.aux_funcs[identifier] = {'is callback': is_callback, 'formal arg names': formal_arg_names} - def _add_emg_comment(self, file, line, data): - if file not in self.emg_comments: - self.emg_comments[file] = {} - self.emg_comments[file][line] = data - def _resolve_file_id(self, file): return self._files.index(file) @@ -284,6 +279,9 @@ def process_verifier_notes(self): self._logger.debug(f"Add note {env_note} for environment function '" f"{self._resolve_function(func_id)}'") edge['env'] = self.process_comment(env_note) + if func_id in self.cif_comments: + edge['env'] = self.process_comment(self.cif_comments[func_id]) + edge['env_instrumented'] = True if file_id in self._env_funcs_openers: if last_opened_line > 0 and start_line - last_opened_line <= MAX_SEARCH_DISTANCE_FOR_EMG_COMMENT: @@ -382,7 +380,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\*/') + cif_comment = re.compile(r'/\* CIF Original function "(\S+)". Instrumenting function "(\S+)". \*/') emg_comment_json = re.compile(r'/\*\sEMG_ACTION\s({.*})\s\*/') for file_id, file in self.files: @@ -396,12 +394,11 @@ def _parse_model_comments(self): for text in file_obj: line += 1 - # Try match EMG comment - # Expect comment like /* TYPE Instance Text */ - match = emg_comment.search(text) + match = cif_comment.search(text) if match: - data = json.loads(match.group(1)) - self._add_emg_comment(file_id, line, data) + orig_func = match.group(1) + instrumented_func = self.add_function(match.group(2)) + self.cif_comments[instrumented_func] = f"Instrumented function '{orig_func}'" # Try match JSON EMG comment match = emg_comment_json.search(text)