Skip to content

Commit

Permalink
Add support for several notes for the same edge (#63)
Browse files Browse the repository at this point in the history 
Issue #61
  • Loading branch information
@vmordan
vmordan authored Mar 15, 2024
1 parent 3d65ed0 commit f9f3230
Show file tree
Hide file tree
Showing 2 changed files with 34 additions and 18 deletions.
28 changes: 19 additions & 9 deletions scripts/mea/et/internal_witness.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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):
Expand Down Expand Up @@ -144,14 +147,21 @@ def add_attr(self, name, value, associate, compare):
def add_entry_node_id(self, node_id):
self._entry_node_id = node_id

# noinspection PyUnusedLocal
def add_edge(self, source, target):
# pylint: disable=unused-argument
# TODO: check coherence of source and target.
def add_edge(self, target, template_edge=None):
edge = {}
self._edges.append(edge)
if target in self.invariants:
edge['invariants'] = self.invariants[target]
if template_edge:
# If there is a template edge, then we create a new edge with comment (note, warn, env).
self._edges.insert(len(self._edges) - 1, edge)
else:
# Here we just create a new edge
self._edges.append(edge)
if self.witness_type == WITNESS_TYPE_CORRECTNESS:
if target in self.invariants:
edge['invariants'] = self.invariants[target]
if template_edge:
for key, val in template_edge.items():
if key not in ('warn', 'note', 'env', 'enter', 'return'):
edge[key] = val
return edge

def add_file(self, file_name):
Expand Down Expand Up @@ -293,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:
Expand Down Expand Up @@ -424,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)')
Expand Down
24 changes: 15 additions & 9 deletions scripts/mea/et/parser.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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':
Expand Down Expand Up @@ -234,21 +234,21 @@ def __parse_witness_edges(self, graph, sink_nodes_map):

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

source_node_id = edge.attrib.get('source')
target_node_id = edge.attrib.get('target')

if target_node_id in sink_nodes_map:
sink_edges_num += 1
continue

# Update lists of input and output edges for source and target nodes.
_edge = self.internal_witness.add_edge(source_node_id, target_node_id)
_edge = self.internal_witness.add_edge(target_node_id)

start_offset = 0
end_offset = 0
condition = None
invariant = None
invariant_scope = None
cur_notes = {}
for data in edge.findall('graphml:data', self.WITNESS_NS):
data_key = data.attrib.get('key')
if data_key == 'originfile':
Expand All @@ -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:
Expand All @@ -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
Expand Down Expand Up @@ -315,8 +315,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
end_offset = int(data.text)
elif data_key in ('note', 'warning'):
tag, note_desc = self.internal_witness.process_note(data_key, data.text)
_edge[tag] = note_desc
self.internal_witness.is_notes = True
cur_notes[tag] = note_desc
elif data_key == 'env':
_edge['env'] = self.internal_witness.process_comment(data.text)
elif data_key not in unsupported_edge_data_keys:
Expand Down Expand Up @@ -374,6 +373,13 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
if 'start line' not in _edge:
_edge['start line'] = 0

for tag, note_desc in cur_notes.items():
# Actually there is only one note available.
self._logger.debug(f"Add verifier {tag}: '{note_desc}' for edge {_edge}")
new_edge = self.internal_witness.add_edge(target_node_id, _edge)
new_edge[tag] = note_desc
self.internal_witness.is_notes = True

edges_num += 1

if not self._is_read_line_directives:
Expand Down

0 comments on commit f9f3230

Please sign in to comment.