Add support for Klever EMG comments in JSON format (#55)

* Add initial support for EMG comments in JSON format
ispras · Feb 20, 2024 · 6fd989e · 6fd989e
1 parent e608a90
commit 6fd989e
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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':