From 3141c490a1de19612b6e5b13ec5a003c96987f53 Mon Sep 17 00:00:00 2001 From: Mordan Vitalii Date: Thu, 14 Mar 2024 00:57:53 +0800 Subject: [PATCH 1/6] Add support for several notes for the same edge Issue #61 --- scripts/mea/et/internal_witness.py | 6 +++++- scripts/mea/et/parser.py | 4 +++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/scripts/mea/et/internal_witness.py b/scripts/mea/et/internal_witness.py index 80cb416..3c155a3 100644 --- a/scripts/mea/et/internal_witness.py +++ b/scripts/mea/et/internal_witness.py @@ -145,13 +145,17 @@ def add_entry_node_id(self, node_id): self._entry_node_id = node_id # noinspection PyUnusedLocal - def add_edge(self, source, target): + def add_edge(self, source, target, template_edge=None): # pylint: disable=unused-argument # TODO: check coherence of source and target. edge = {} self._edges.append(edge) 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): diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py index 826005b..c235dbb 100644 --- a/scripts/mea/et/parser.py +++ b/scripts/mea/et/parser.py @@ -315,7 +315,9 @@ 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._logger.debug(f"Add verifier {tag}: '{note_desc}' for edge {_edge}") + new_edge = self.internal_witness.add_edge(source_node_id, target_node_id, _edge) + new_edge[tag] = note_desc self.internal_witness.is_notes = True elif data_key == 'env': _edge['env'] = self.internal_witness.process_comment(data.text) From c3fd90d814c3eb0ccc1f04c875bc022dfc6e9a6a Mon Sep 17 00:00:00 2001 From: Mordan Vitalii Date: Thu, 14 Mar 2024 11:19:43 +0800 Subject: [PATCH 2/6] Insert notes comments before target edge --- scripts/mea/et/internal_witness.py | 17 ++++++++++------- scripts/mea/et/parser.py | 4 ++-- 2 files changed, 12 insertions(+), 9 deletions(-) diff --git a/scripts/mea/et/internal_witness.py b/scripts/mea/et/internal_witness.py index 3c155a3..34fe03e 100644 --- a/scripts/mea/et/internal_witness.py +++ b/scripts/mea/et/internal_witness.py @@ -144,14 +144,17 @@ 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, template_edge=None): - # 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 == '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'): diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py index c235dbb..5046be1 100644 --- a/scripts/mea/et/parser.py +++ b/scripts/mea/et/parser.py @@ -242,7 +242,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map): 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 @@ -316,7 +316,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map): elif data_key in ('note', 'warning'): tag, note_desc = self.internal_witness.process_note(data_key, data.text) self._logger.debug(f"Add verifier {tag}: '{note_desc}' for edge {_edge}") - new_edge = self.internal_witness.add_edge(source_node_id, target_node_id, _edge) + new_edge = self.internal_witness.add_edge(target_node_id, _edge) new_edge[tag] = note_desc self.internal_witness.is_notes = True elif data_key == 'env': From e3c8ce48ee5492dd01e7605d07e5aa2516d8c336 Mon Sep 17 00:00:00 2001 From: Mordan Vitalii Date: Thu, 14 Mar 2024 11:22:00 +0800 Subject: [PATCH 3/6] Use tags for witness types --- scripts/mea/et/internal_witness.py | 9 ++++++--- scripts/mea/et/parser.py | 10 +++++----- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/scripts/mea/et/internal_witness.py b/scripts/mea/et/internal_witness.py index 34fe03e..3f44114 100644 --- 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 index 5046be1..9d6585f 100644 --- 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 From 46a14238492c0e8a18cb3b220002e14d8292be8b Mon Sep 17 00:00:00 2001 From: Mordan Vitalii Date: Thu, 14 Mar 2024 11:28:35 +0800 Subject: [PATCH 4/6] Remove unused variable 'source_node_id' --- scripts/mea/et/parser.py | 1 - 1 file changed, 1 deletion(-) diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py index 9d6585f..47fe020 100644 --- a/scripts/mea/et/parser.py +++ b/scripts/mea/et/parser.py @@ -234,7 +234,6 @@ 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: From 25412e55e982ab71bea5b66f82fadc1a48930a70 Mon Sep 17 00:00:00 2001 From: Mordan Vitalii Date: Thu, 14 Mar 2024 12:18:35 +0800 Subject: [PATCH 5/6] Duplicate notes edge after they have been fully created --- scripts/mea/et/parser.py | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py index 47fe020..678620e 100644 --- a/scripts/mea/et/parser.py +++ b/scripts/mea/et/parser.py @@ -248,6 +248,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map): 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': @@ -314,16 +315,20 @@ 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) - 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 + 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: self._logger.warning(f'Edge data key {data_key} is not supported') unsupported_edge_data_keys[data_key] = None + 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 + if invariant and invariant_scope: self.internal_witness.add_invariant(invariant, invariant_scope) From 8b54ad83ea91354e77c9194af3b3807b6b573451 Mon Sep 17 00:00:00 2001 From: Mordan Vitalii Date: Fri, 15 Mar 2024 11:00:43 +0800 Subject: [PATCH 6/6] Fix uninitialised thread id --- scripts/mea/et/parser.py | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py index 678620e..cbd4a54 100644 --- a/scripts/mea/et/parser.py +++ b/scripts/mea/et/parser.py @@ -322,13 +322,6 @@ def __parse_witness_edges(self, graph, sink_nodes_map): self._logger.warning(f'Edge data key {data_key} is not supported') unsupported_edge_data_keys[data_key] = None - 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 - if invariant and invariant_scope: self.internal_witness.add_invariant(invariant, invariant_scope) @@ -380,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: