diff --git a/lint/witnesslint/linter.py b/lint/witnesslint/linter.py index f2ce079..4bc8b85 100644 --- a/lint/witnesslint/linter.py +++ b/lint/witnesslint/linter.py @@ -11,14 +11,14 @@ [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 +from copy import deepcopy from lxml import etree # noqa: S410 does not matter from . import logger as logging @@ -37,6 +37,8 @@ "CHECK( init(main()), LTL(F end) )", ] +MAIN_THREAD_ID = "0" + WITNESS_VALID = 0 WITNESS_FAULTY = 1 NO_WITNESS = 5 @@ -123,6 +125,31 @@ 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, callstacks, visited): + self.node = node + self.callstacks = callstacks + self.visited = visited + + class WitnessLinter: """ Contains methods that check different parts of a witness for consistency @@ -191,48 +218,41 @@ 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): - """ - Performs DFS on the given transitions to make sure that all - possible paths have a consistent order of function entries and exits. - """ - to_visit = [(start_node, [])] - visited = set() + def check_transitions(self): + to_visit = [State(self.witness.entry_node, {MAIN_THREAD_ID: Callstack()}, {})] while to_visit: - current_node, current_stack = to_visit.pop() - if current_node in visited: - continue - visited.add(current_node) - if current_node not in transitions and current_stack: - logging.warning( - "No leaving transition for node {} but not all " - "functions have been left".format(current_node) - ) - for outgoing in transitions.get(current_node, []): - 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] - ) - ) - elif outgoing[2] == current_stack[-1]: - function_stack.pop() - else: - logging.warning( - "Trying to return from function '{0}' in transition " - "{1} -> {2} but currently in function {3}".format( - outgoing[2], - current_node, - outgoing[0], - 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)) + 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.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) + 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) + + if not current_callstack.function_stack and current_callstack.touched: + del callstacks[transition.thread_id] + if transition.create_thread: + 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: + 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, callstacks, new_visited)) def handle_data(self, data, parent): """ @@ -304,10 +324,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,39 +453,15 @@ 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 - # 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( @@ -477,7 +470,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 +703,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 +717,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 = (None, None) + 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: @@ -736,6 +730,10 @@ 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 + elif key == witness.CREATETHREAD: + create_thread = child.text else: logging.warning( "Edge has unexpected child element of type '{}'".format( @@ -744,12 +742,11 @@ def handle_edge(self, edge): child.sourceline, ) if source and target: + transition = witness.Transition(target, enter, return_from, thread_id, create_thread) if source in self.witness.transitions: - self.witness.transitions[source].append( - (target, enter, return_from) - ) + self.witness.transitions[source].append(transition) else: - self.witness.transitions[source] = [(target, enter, return_from)] + self.witness.transitions[source] = [transition] else: for child in edge: if child.tag.rpartition("}")[2] == witness.DATA: @@ -881,10 +878,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_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