From b3ce9b18130d83dae6fc36e197e87e5a83bba9eb Mon Sep 17 00:00:00 2001
From: Mordan Vitalii <mordan@ispras.ru>
Date: Fri, 6 Oct 2023 19:35:00 +0700
Subject: [PATCH] Create map from CIL file lines to original sources

---
 scripts/mea/et/parser.py | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py
index 0b15c44..0f7aa56 100644
--- a/scripts/mea/et/parser.py
+++ b/scripts/mea/et/parser.py
@@ -38,6 +38,9 @@ class WitnessParser:
     def __init__(self, logger, witness, source_dir=None):
         self._logger = logger
         self.entry_point = None
+        # TODO: specify this option
+        self._is_read_line_directives = False
+        self.src_files_map = {}
         self.source_dir = source_dir
         self._violation_hints = set()
         self.default_program_file = None  # default source file
@@ -120,6 +123,27 @@ def _parse_witness(self, witness):
                 new_name = self.__check_file_name(data.text)
                 if new_name:
                     self.global_program_file = new_name
+                    if not self._is_read_line_directives:
+                        if not self.src_files_map:
+                            with open(new_name, encoding='utf8') as fd_cil:
+                                line_num = 1
+                                orig_file_id = None
+                                orig_file_line_num = 0
+                                line_preprocessor_directive = re.compile(r'\s*#line\s+(\d+)\s*(.*)')
+                                for line in fd_cil:
+                                    m = line_preprocessor_directive.match(line)
+                                    if m:
+                                        orig_file_line_num = int(m.group(1))
+                                        if m.group(2):
+                                            file_name = m.group(2)[1:-1]
+                                            # Do not treat artificial file references
+                                            if not os.path.basename(file_name) == '<built-in>':
+                                                orig_file_id = self.internal_witness.add_file(file_name)
+                                    else:
+                                        if orig_file_id and orig_file_line_num:
+                                            self.src_files_map[line_num] = (orig_file_id, orig_file_line_num)
+                                        orig_file_line_num += 1
+                                    line_num += 1
             elif key == 'witness-type':
                 witness_type = data.text
                 if witness_type == 'correctness_witness':
@@ -352,4 +376,15 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
 
             edges_num += 1
 
+        if not self._is_read_line_directives:
+            for edge in self.internal_witness.get_edges():
+                if 'start line' in edge:
+                    try:
+                        start_line = edge['start line']
+                        src_file_id, src_file_line = self.src_files_map[start_line]
+                        edge['start line'] = src_file_line
+                        edge['file'] = src_file_id
+                    except KeyError:
+                        pass
+
         self._logger.debug(f'Parse {edges_num} edges and {sink_edges_num} sink edges')