Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for Klever EMG comments in JSON format #55

Merged
merged 5 commits into from
Feb 20, 2024
+22 −4
Merged

Add support for Klever EMG comments in JSON format #55

Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7d44687
Add initial support for EMG comments in JSON format
vmordan Feb 16, 2024
8e3e2e9
Use entry_point tag for main functions
vmordan Feb 19, 2024
df15d26
Correct debug message
vmordan Feb 19, 2024
00660bf
Fix double EMG comments
vmordan Feb 19, 2024
3da1944
Add todo
vmordan Feb 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions scripts/mea/et/internal_witness.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 = []
Expand Down Expand Up @@ -268,6 +269,10 @@ 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 warning {env} for statement from '{file}:{start_line}'")
vmordan marked this conversation as resolved.
Show resolved Hide resolved
edge['env'] = self.process_comment(env)
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}'")
Expand All @@ -293,6 +298,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):
Expand All @@ -312,6 +318,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)
Expand Down
Loading