Skip to content

Commit

Permalink
Add a quick fix for src code links
Browse files Browse the repository at this point in the history
  • Loading branch information
vmordan committed Oct 3, 2023
1 parent 1cee6d3 commit 4b000ae
Showing 1 changed file with 48 additions and 10 deletions.
58 changes: 48 additions & 10 deletions scripts/mea/et/parser.py
Original file line number Diff line number Diff line change
Expand Up @@ -208,6 +208,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
is_source_file = False
is_entry_point = False

src_files_offset = dict()
for edge in graph.findall('graphml:edge', self.WITNESS_NS):

source_node_id = edge.attrib.get('source')
Expand Down Expand Up @@ -302,6 +303,19 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
if invariant and invariant_scope:
self.internal_witness.add_invariant(invariant, invariant_scope)

def _get_src_file():
if start_offset and self.global_program_file:
res_src_file = self.global_program_file
elif 'file' in _edge:
res_src_file = self.internal_witness.get_file_name(_edge['file'])
if not res_src_file and self.global_program_file:
res_src_file = self.global_program_file
elif self.global_program_file:
res_src_file = self.global_program_file
else:
res_src_file = None
return res_src_file

if "source" not in _edge:
_edge['source'] = ""
if 'enter' in _edge:
Expand All @@ -312,16 +326,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
if 'assumption' in _edge:
_edge['source'] = _edge['assumption']
elif 'start line' in _edge:
if start_offset and self.global_program_file:
src_file = self.global_program_file
elif 'file' in _edge:
src_file = self.internal_witness.get_file_name(_edge['file'])
if not src_file and self.global_program_file:
src_file = self.global_program_file
elif self.global_program_file:
src_file = self.global_program_file
else:
src_file = None
src_file = _get_src_file()
if src_file:
with open(src_file, encoding='utf8') as src_obj:
if start_offset:
Expand All @@ -344,6 +349,29 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
counter += 1
if condition == 'condition-false':
_edge['source'] = f"!({_edge['source']})"
elif 'start line' in _edge:
src_file = _get_src_file()
if src_file and src_file not in src_files_offset:
with open(src_file, encoding='utf8') as src_obj:
counter = 1
offset = 0
for line in src_obj.readlines():
if counter == _edge['start line']:
line = line.rstrip().lstrip()
if 'condition' in _edge:
res = re.match(r'[^(]*\((.+)\)[^)]*', line)
if res:
line = res.group(1)
if _edge['source'] == line:
src_files_offset[src_file] = 0
elif offset:
src_files_offset[src_file] = offset
break
elif _edge['start line'] - counter < 10:
line = line.rstrip().lstrip()
if _edge['source'] == line:
offset = counter - _edge['start line']
counter += 1

if 'thread' not in _edge:
_edge['thread'] = "0"
Expand All @@ -352,4 +380,14 @@ def __parse_witness_edges(self, graph, sink_nodes_map):

edges_num += 1

for edge in self.internal_witness.get_edges():
if 'file' not in edge or 'start line' not in edge:
continue
res_src_file = self.internal_witness.get_file_name(edge['file'])
if res_src_file not in src_files_offset:
continue
offset = src_files_offset[res_src_file]
if offset:
edge['start line'] += offset

self._logger.debug(f'Parse {edges_num} edges and {sink_edges_num} sink edges')

0 comments on commit 4b000ae

Please sign in to comment.