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 several notes for the same edge #63

Merged
merged 6 commits into from
Mar 15, 2024
Merged

Add support for several notes for the same edge #63

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
3141c49
Add support for several notes for the same edge
vmordan Mar 13, 2024
c3fd90d
Insert notes comments before target edge
vmordan Mar 14, 2024
e3c8ce4
Use tags for witness types
vmordan Mar 14, 2024
46a1423
Remove unused variable 'source_node_id'
vmordan Mar 14, 2024
25412e5
Duplicate notes edge after they have been fully created
vmordan Mar 14, 2024
8b54ad8
Fix uninitialised thread id
vmordan Mar 15, 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
28 changes: 19 additions & 9 deletions scripts/mea/et/internal_witness.py
View file
Open in desktop
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
Open in desktop
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
Loading