From 7cee89e7ad44824757b77b746be96e8e1f5dfc1c Mon Sep 17 00:00:00 2001 From: Sven Umbricht Date: Wed, 20 Oct 2021 12:28:33 +0200 Subject: [PATCH 1/5] Adjust thread handling, check callstack validity for threads separately. --- lint/witnesslint/linter.py | 93 ++++++++++++++++---------------------- 1 file changed, 40 insertions(+), 53 deletions(-) diff --git a/lint/witnesslint/linter.py b/lint/witnesslint/linter.py index f2ce079..2e2cc2c 100644 --- a/lint/witnesslint/linter.py +++ b/lint/witnesslint/linter.py @@ -11,10 +11,9 @@ [1]: github.com/sosy-lab/sv-witnesses/blob/master/README.md """ -__version__ = "1.0" +__version__ = "1.1" import argparse -import collections import hashlib import re import sys @@ -37,6 +36,8 @@ "CHECK( init(main()), LTL(F end) )", ] +MAIN_THREAD_ID = "0" + WITNESS_VALID = 0 WITNESS_FAULTY = 1 NO_WITNESS = 5 @@ -191,48 +192,58 @@ def check_character_offset(self, offset, pos): elif int(offset) < 0 or int(offset) >= self.program_info["num_chars"]: logging.warning("{} is not a valid character offset".format(offset), pos) - def check_function_stack(self, transitions, start_node): + def check_function_stack(self): """ - Performs DFS on the given transitions to make sure that all + Performs DFS on the transitions of the witness automaton to make sure that all possible paths have a consistent order of function entries and exits. """ - to_visit = [(start_node, [])] + to_visit = [(self.witness.entry_node, MAIN_THREAD_ID, [])] + for thread in self.witness.threads: + start_node = self.witness.threads[thread] + if start_node: + to_visit.append((start_node, thread, [])) visited = set() while to_visit: - current_node, current_stack = to_visit.pop() - if current_node in visited: + current_node, current_thread, current_stack = to_visit.pop() + if (current_node, current_thread) in visited: continue - visited.add(current_node) - if current_node not in transitions and current_stack: + visited.add((current_node, current_thread)) + if ( + current_node, + current_thread, + ) not in self.witness.transitions and current_stack: logging.warning( - "No leaving transition for node {} but not all " - "functions have been left".format(current_node) + "No leaving transition for thread {0} at node {1} but not all " + "functions have been left".format(current_thread, current_node) ) - for outgoing in transitions.get(current_node, []): + for outgoing in self.witness.transitions.get( + (current_node, current_thread), [] + ): function_stack = current_stack[:] if outgoing[2] is not None and outgoing[2] != outgoing[1]: if not function_stack: logging.warning( "Trying to return from function '{0}' in transition " - "{1} -> {2} but currently not in a function".format( - outgoing[2], current_node, outgoing[0] + "{1} -> {2} for thread {3} but currently not in a function".format( + outgoing[2], current_node, outgoing[0], current_thread ) ) - elif outgoing[2] == current_stack[-1]: + elif outgoing[2] == function_stack[-1]: function_stack.pop() else: logging.warning( "Trying to return from function '{0}' in transition " - "{1} -> {2} but currently in function {3}".format( + "{1} -> {2} for thread {3} but currently in function {4}".format( outgoing[2], current_node, outgoing[0], + current_thread, function_stack[-1], ) ) if outgoing[1] is not None and outgoing[1] != outgoing[2]: function_stack.append(outgoing[1]) - to_visit.append((outgoing[0], function_stack)) + to_visit.append((outgoing[0], current_thread, function_stack)) def handle_data(self, data, parent): """ @@ -304,10 +315,7 @@ def handle_node_data(self, data, key, parent): elif data.text == "true": node_id = parent.attrib.get("id") if node_id is not None: - if ( - node_id in self.witness.transition_sources - or node_id in self.witness.transitions - ): + if node_id in self.witness.transition_sources: logging.warning( "Sink node should have no leaving edges", data.sourceline ) @@ -436,28 +444,8 @@ def handle_edge_data(self, data, key, parent): data.sourceline, ) elif key == witness.ENTERFUNCTION: - for child in parent: - child.text = child.text.strip() - if ( - child.tag.rpartition("}")[2] == witness.DATA - and child.attrib.get(witness.KEY) == witness.THREADID - and child.text in self.witness.threads - and self.witness.threads[child.text] is None - ): - self.witness.threads[child.text] = data.text - break self.check_functionname(data.text, data.sourceline) elif key in ["returnFrom", witness.RETURNFROMFUNCTION]: - for child in parent: - child.text = child.text.strip() - if ( - child.tag.rpartition("}")[2] == witness.DATA - and child.attrib.get(witness.KEY) == witness.THREADID - and child.text in self.witness.threads - and self.witness.threads[child.text] == data.text - ): - del self.witness.threads[child.text] - break self.check_functionname(data.text, data.sourceline) elif key == witness.THREADID: # Check disabled for SV-COMP'21 as questions about the specification @@ -477,7 +465,7 @@ def handle_edge_data(self, data, key, parent): # ) pass else: - self.witness.threads[data.text] = None + self.witness.threads[data.text] = parent.attrib.get("target") elif self.witness.defined_keys.get(key) == witness.EDGE: # Other, tool-specific keys are allowed as long as they have been defined pass @@ -710,9 +698,7 @@ def handle_edge(self, edge): logging.warning( "Sink node should have no leaving edges", edge.sourceline ) - if not self.options.strictChecking: - # Otherwise this information is stored in self.witness.transitions - self.witness.transition_sources.add(source) + self.witness.transition_sources.add(source) if source not in self.witness.node_ids: self.check_existence_later.add(source) target = edge.attrib.get("target") @@ -726,7 +712,7 @@ def handle_edge(self, edge): if target not in self.witness.node_ids: self.check_existence_later.add(target) if self.options.strictChecking: - enter, return_from = (None, None) + enter, return_from, thread_id = (None, None, None) for child in edge: child.text = child.text.strip() if child.tag.rpartition("}")[2] == witness.DATA: @@ -736,6 +722,8 @@ def handle_edge(self, edge): enter = child.text elif key in ["returnFrom", witness.RETURNFROMFUNCTION]: return_from = child.text + elif key == witness.THREADID: + thread_id = child.text else: logging.warning( "Edge has unexpected child element of type '{}'".format( @@ -744,12 +732,14 @@ def handle_edge(self, edge): child.sourceline, ) if source and target: - if source in self.witness.transitions: - self.witness.transitions[source].append( + if (source, thread_id) in self.witness.transitions: + self.witness.transitions[(source, thread_id)].append( (target, enter, return_from) ) else: - self.witness.transitions[source] = [(target, enter, return_from)] + self.witness.transitions[(source, thread_id)] = [ + (target, enter, return_from) + ] else: for child in edge: if child.tag.rpartition("}")[2] == witness.DATA: @@ -881,10 +871,7 @@ def final_checks(self): if node_id not in self.witness.node_ids: logging.warning("Node {} has not been declared".format(node_id)) if self.options.strictChecking: - self.check_function_stack( - collections.OrderedDict(sorted(self.witness.transitions.items())), - self.witness.entry_node, - ) + self.check_function_stack() if self.program_info is not None: for check in self.check_later: check() From 0e83be88f5bf196002c2166fb550ed20dea836e5 Mon Sep 17 00:00:00 2001 From: Sven Umbricht Date: Thu, 21 Oct 2021 11:05:01 +0200 Subject: [PATCH 2/5] Reenable check for thread existance. --- lint/witnesslint/linter.py | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/lint/witnesslint/linter.py b/lint/witnesslint/linter.py index 2e2cc2c..203cdbc 100644 --- a/lint/witnesslint/linter.py +++ b/lint/witnesslint/linter.py @@ -448,15 +448,11 @@ def handle_edge_data(self, data, key, parent): elif key in ["returnFrom", witness.RETURNFROMFUNCTION]: self.check_functionname(data.text, data.sourceline) elif key == witness.THREADID: - # Check disabled for SV-COMP'21 as questions about the specification - # need to be resolved first, see - # https://gitlab.com/sosy-lab/sv-comp/archives-2021/-/issues/30 - # if data.text not in self.witness.threads: - # logging.warning( - # "Thread with id {} doesn't exist".format(data.text), - # data.sourceline, - # ) - pass + if data.text not in self.witness.threads and data.text != MAIN_THREAD_ID: + logging.warning( + "Thread with id {} doesn't exist".format(data.text), + data.sourceline, + ) elif key == witness.CREATETHREAD: if data.text in self.witness.threads: # logging.warning( From 1b98925dee7451a670102499086a21b333d4e555 Mon Sep 17 00:00:00 2001 From: Sven Umbricht Date: Thu, 21 Oct 2021 11:07:08 +0200 Subject: [PATCH 3/5] If no thread id is given assume main thread. --- lint/witnesslint/linter.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lint/witnesslint/linter.py b/lint/witnesslint/linter.py index 203cdbc..47ab70e 100644 --- a/lint/witnesslint/linter.py +++ b/lint/witnesslint/linter.py @@ -708,7 +708,7 @@ def handle_edge(self, edge): if target not in self.witness.node_ids: self.check_existence_later.add(target) if self.options.strictChecking: - enter, return_from, thread_id = (None, None, None) + enter, return_from, thread_id = (None, None, MAIN_THREAD_ID) for child in edge: child.text = child.text.strip() if child.tag.rpartition("}")[2] == witness.DATA: From 8779d3fee73d13dd2e2614a384b754cbb82b61e5 Mon Sep 17 00:00:00 2001 From: Sven Umbricht Date: Fri, 29 Oct 2021 13:55:05 +0200 Subject: [PATCH 4/5] Remove implicit assumptions when checking callstack validity. --- lint/witnesslint/linter.py | 135 ++++++++++++++++++++---------------- lint/witnesslint/witness.py | 9 +++ 2 files changed, 84 insertions(+), 60 deletions(-) diff --git a/lint/witnesslint/linter.py b/lint/witnesslint/linter.py index 47ab70e..9d409eb 100644 --- a/lint/witnesslint/linter.py +++ b/lint/witnesslint/linter.py @@ -18,6 +18,7 @@ import re import sys +from copy import deepcopy from lxml import etree # noqa: S410 does not matter from . import logger as logging @@ -124,6 +125,32 @@ def create_arg_parser(): return parser +class Callstack: + + def __init__(self): + self.function_stack = [] + self.touched = False + + def enter(self, function): + self.touched = True + self.function_stack.append(function) + + def return_from(self, function): + if self.function_stack and self.function_stack[-1] == function: + self.function_stack.pop() + return True + return False + + +class State: + + def __init__(self, node, thread_ids, callstacks, visited): + self.node = node + self.thread_ids = thread_ids + self.callstacks = callstacks + self.visited = visited + + class WitnessLinter: """ Contains methods that check different parts of a witness for consistency @@ -192,58 +219,44 @@ def check_character_offset(self, offset, pos): elif int(offset) < 0 or int(offset) >= self.program_info["num_chars"]: logging.warning("{} is not a valid character offset".format(offset), pos) - def check_function_stack(self): - """ - Performs DFS on the transitions of the witness automaton to make sure that all - possible paths have a consistent order of function entries and exits. - """ - to_visit = [(self.witness.entry_node, MAIN_THREAD_ID, [])] - for thread in self.witness.threads: - start_node = self.witness.threads[thread] - if start_node: - to_visit.append((start_node, thread, [])) - visited = set() + def check_transitions(self): + to_visit = [State(self.witness.entry_node, {MAIN_THREAD_ID}, {MAIN_THREAD_ID: Callstack()}, {})] while to_visit: - current_node, current_thread, current_stack = to_visit.pop() - if (current_node, current_thread) in visited: - continue - visited.add((current_node, current_thread)) - if ( - current_node, - current_thread, - ) not in self.witness.transitions and current_stack: - logging.warning( - "No leaving transition for thread {0} at node {1} but not all " - "functions have been left".format(current_thread, current_node) - ) - for outgoing in self.witness.transitions.get( - (current_node, current_thread), [] - ): - function_stack = current_stack[:] - if outgoing[2] is not None and outgoing[2] != outgoing[1]: - if not function_stack: - logging.warning( - "Trying to return from function '{0}' in transition " - "{1} -> {2} for thread {3} but currently not in a function".format( - outgoing[2], current_node, outgoing[0], current_thread - ) - ) - elif outgoing[2] == function_stack[-1]: - function_stack.pop() - else: - logging.warning( - "Trying to return from function '{0}' in transition " - "{1} -> {2} for thread {3} but currently in function {4}".format( - outgoing[2], - current_node, - outgoing[0], - current_thread, - function_stack[-1], - ) - ) - if outgoing[1] is not None and outgoing[1] != outgoing[2]: - function_stack.append(outgoing[1]) - to_visit.append((outgoing[0], current_thread, function_stack)) + state = to_visit.pop() + for transition in self.witness.transitions.get(state.node, []): + if transition.target in state.visited and state.node in state.visited and state.visited[state.node] > state.visited[transition.target]: + # TODO: For now we ignore backwards edges if they have been taken before + continue + assert transition.thread_id is not None + if transition.thread_id not in state.thread_ids: + logging.warning("Thread {0} does not exist at transition {1} -> {2}".format(transition.thread_id, state.node, transition.target)) + else: + callstacks = deepcopy(state.callstacks) + current_callstack = callstacks[transition.thread_id] + if transition.return_from: + if not current_callstack.return_from(transition.return_from): + logging.warning("Trying to return from function '{0}' in transition " + "{1} -> {2} for thread {3} but not currently in that function".format( + transition.return_from, state.node, transition.target, transition.thread_id)) + if transition.enter: + # TODO: Should this be illegal if the return_from cleared the function stack? + current_callstack.enter(transition.enter) + + new_thread_ids = state.thread_ids.copy() + if not current_callstack.function_stack and current_callstack.touched: + new_thread_ids.remove(transition.thread_id) + del callstacks[transition.thread_id] + if transition.create_thread: + if transition.create_thread in state.thread_ids: + logging.warning("Creating thread {0} in transition {1} -> {2}, but thread " + "with id {0} already exists".format(transition.create_thread, state.node, transition.target)) + else: + new_thread_ids.add(transition.create_thread) + callstacks[transition.create_thread] = Callstack() + new_visited = state.visited.copy() + if state.node not in state.visited: + new_visited[state.node] = len(state.visited) + to_visit.append(State(transition.target, new_thread_ids, callstacks, new_visited)) def handle_data(self, data, parent): """ @@ -708,7 +721,10 @@ def handle_edge(self, edge): if target not in self.witness.node_ids: self.check_existence_later.add(target) if self.options.strictChecking: - enter, return_from, thread_id = (None, None, MAIN_THREAD_ID) + enter = None + return_from = None + thread_id = MAIN_THREAD_ID + create_thread = None for child in edge: child.text = child.text.strip() if child.tag.rpartition("}")[2] == witness.DATA: @@ -720,6 +736,8 @@ def handle_edge(self, edge): return_from = child.text elif key == witness.THREADID: thread_id = child.text + elif key == witness.CREATETHREAD: + create_thread = child.text else: logging.warning( "Edge has unexpected child element of type '{}'".format( @@ -728,14 +746,11 @@ def handle_edge(self, edge): child.sourceline, ) if source and target: - if (source, thread_id) in self.witness.transitions: - self.witness.transitions[(source, thread_id)].append( - (target, enter, return_from) - ) + transition = witness.Transition(target, enter, return_from, thread_id, create_thread) + if source in self.witness.transitions: + self.witness.transitions[source].append(transition) else: - self.witness.transitions[(source, thread_id)] = [ - (target, enter, return_from) - ] + self.witness.transitions[source] = [transition] else: for child in edge: if child.tag.rpartition("}")[2] == witness.DATA: @@ -867,7 +882,7 @@ def final_checks(self): if node_id not in self.witness.node_ids: logging.warning("Node {} has not been declared".format(node_id)) if self.options.strictChecking: - self.check_function_stack() + self.check_transitions() if self.program_info is not None: for check in self.check_later: check() diff --git a/lint/witnesslint/witness.py b/lint/witnesslint/witness.py index 6a92519..736182b 100644 --- a/lint/witnesslint/witness.py +++ b/lint/witnesslint/witness.py @@ -82,6 +82,15 @@ ) +class Transition: + def __init__(self, target, enter, return_from, thread_id, create_thread): + self.target = target + self.enter = enter + self.return_from = return_from + self.thread_id = thread_id + self.create_thread = create_thread + + class Witness: def __init__(self, witness_file): self.witness_file = witness_file From 617c40be3d6fb86954fb0c768430f313f52c3a2a Mon Sep 17 00:00:00 2001 From: Sven Umbricht Date: Wed, 3 Nov 2021 10:34:44 +0100 Subject: [PATCH 5/5] Remove unnecessary variable. --- lint/witnesslint/linter.py | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/lint/witnesslint/linter.py b/lint/witnesslint/linter.py index 9d409eb..4bc8b85 100644 --- a/lint/witnesslint/linter.py +++ b/lint/witnesslint/linter.py @@ -144,9 +144,8 @@ def return_from(self, function): class State: - def __init__(self, node, thread_ids, callstacks, visited): + def __init__(self, node, callstacks, visited): self.node = node - self.thread_ids = thread_ids self.callstacks = callstacks self.visited = visited @@ -220,7 +219,7 @@ def check_character_offset(self, offset, pos): logging.warning("{} is not a valid character offset".format(offset), pos) def check_transitions(self): - to_visit = [State(self.witness.entry_node, {MAIN_THREAD_ID}, {MAIN_THREAD_ID: Callstack()}, {})] + to_visit = [State(self.witness.entry_node, {MAIN_THREAD_ID: Callstack()}, {})] while to_visit: state = to_visit.pop() for transition in self.witness.transitions.get(state.node, []): @@ -228,7 +227,7 @@ def check_transitions(self): # TODO: For now we ignore backwards edges if they have been taken before continue assert transition.thread_id is not None - if transition.thread_id not in state.thread_ids: + if transition.thread_id not in state.callstacks: logging.warning("Thread {0} does not exist at transition {1} -> {2}".format(transition.thread_id, state.node, transition.target)) else: callstacks = deepcopy(state.callstacks) @@ -242,21 +241,18 @@ def check_transitions(self): # TODO: Should this be illegal if the return_from cleared the function stack? current_callstack.enter(transition.enter) - new_thread_ids = state.thread_ids.copy() if not current_callstack.function_stack and current_callstack.touched: - new_thread_ids.remove(transition.thread_id) del callstacks[transition.thread_id] if transition.create_thread: - if transition.create_thread in state.thread_ids: + if transition.create_thread in state.callstacks: logging.warning("Creating thread {0} in transition {1} -> {2}, but thread " "with id {0} already exists".format(transition.create_thread, state.node, transition.target)) else: - new_thread_ids.add(transition.create_thread) callstacks[transition.create_thread] = Callstack() new_visited = state.visited.copy() if state.node not in state.visited: new_visited[state.node] = len(state.visited) - to_visit.append(State(transition.target, new_thread_ids, callstacks, new_visited)) + to_visit.append(State(transition.target, callstacks, new_visited)) def handle_data(self, data, parent): """