Use tags for witness types

ispras · Mar 14, 2024 · e3c8ce4 · e3c8ce4
1 parent c3fd90d
commit e3c8ce4
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 8 deletions.
diff --git a/scripts/mea/et/internal_witness.py b/scripts/mea/et/internal_witness.py
@@ -31,6 +31,9 @@
 TAG_LEVEL = "level"
 TAG_VALUE = "value"
 
+WITNESS_TYPE_VIOLATION = "violation"
+WITNESS_TYPE_CORRECTNESS = "correctness"
+
 
 # Capitalize first letters of attribute names.
 def capitalize_attr_names(attrs):
@@ -152,7 +155,7 @@ def add_edge(self, target, template_edge=None):
         else:
             # Here we just create a new edge
             self._edges.append(edge)
-        if self.witness_type == 'correctness':
+        if self.witness_type == WITNESS_TYPE_CORRECTNESS:
             if target in self.invariants:
                 edge['invariants'] = self.invariants[target]
         if template_edge:
@@ -300,7 +303,7 @@ def process_verifier_notes(self):
                             edge['note'] = self.process_comment(note)
                             break
 
-        if not warn_edges and self.witness_type == 'violation':
+        if not warn_edges and self.witness_type == WITNESS_TYPE_VIOLATION:
             if self._edges:
                 last_edge = self._edges[-1]
                 if 'note' in last_edge:
@@ -431,7 +434,7 @@ def add_thread(self, thread_id: str):
 
     def final_checks(self, entry_point="main"):
         # Check for warnings
-        if self.witness_type == 'violation':
+        if self.witness_type == WITNESS_TYPE_VIOLATION:
             if not self.is_call_stack:
                 self._warnings.append('No call stack (please add tags "enterFunction" and '
                                       '"returnFrom" to improve visualization)')

diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py
@@ -26,7 +26,7 @@
 import re
 from xml.etree import ElementTree
 
-from mea.et.internal_witness import InternalWitness
+from mea.et.internal_witness import InternalWitness, WITNESS_TYPE_VIOLATION, WITNESS_TYPE_CORRECTNESS
 
 
 class WitnessParser:
@@ -147,9 +147,9 @@ def _parse_witness(self, witness):
             elif key == 'witness-type':
                 witness_type = data.text
                 if witness_type == 'correctness_witness':
-                    self.internal_witness.witness_type = 'correctness'
+                    self.internal_witness.witness_type = WITNESS_TYPE_CORRECTNESS
                 elif witness_type == 'violation_witness':
-                    self.internal_witness.witness_type = 'violation'
+                    self.internal_witness.witness_type = WITNESS_TYPE_VIOLATION
                 else:
                     self._logger.warning(f"Unsupported witness type: {witness_type}")
             elif key == 'specification':
@@ -274,7 +274,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
                             if self.entry_point:
                                 if self.entry_point == function_name:
                                     self.internal_witness.is_main_function = True
-                                    if self.internal_witness.witness_type == 'violation':
+                                    if self.internal_witness.witness_type == WITNESS_TYPE_VIOLATION:
                                         _edge['entry_point'] = "entry point"
                                         is_entry_point = True
                             else:
@@ -284,7 +284,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
                         func_id = self.internal_witness.resolve_function_id(function_name)
                         _edge['enter'] = func_id
                         if not is_entry_point and \
-                                self.internal_witness.witness_type == 'violation':
+                                self.internal_witness.witness_type == WITNESS_TYPE_VIOLATION:
                             _edge['entry_point'] = "entry point"
                             self.internal_witness.add_thread("decl")
                             is_entry_point = True