Skip to content
This repository has been archived by the owner on Oct 14, 2022. It is now read-only.

WIP: Proper handling of thread information in witness linter #51

Draft
wants to merge 5 commits into
base: main
Choose a base branch
from
Draft

WIP: Proper handling of thread information in witness linter #51

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7cee89e
Adjust thread handling, check callstack validity for threads separately.
SvenUmbricht Oct 20, 2021
0e83be8
Reenable check for thread existance.
SvenUmbricht Oct 21, 2021
1b98925
If no thread id is given assume main thread.
SvenUmbricht Oct 21, 2021
8779d3f
Remove implicit assumptions when checking callstack validity.
SvenUmbricht Oct 29, 2021
617c40b
Remove unnecessary variable.
SvenUmbricht Nov 3, 2021
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
172 changes: 83 additions & 89 deletions lint/witnesslint/linter.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -37,6 +37,8 @@
"CHECK( init(main()), LTL(F end) )",
]

MAIN_THREAD_ID = "0"

WITNESS_VALID = 0
WITNESS_FAULTY = 1
NO_WITNESS = 5
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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):
"""
Expand Down Expand Up @@ -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
)
Expand Down Expand Up @@ -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(
Expand All @@ -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
Expand Down Expand Up @@ -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")
Expand All @@ -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:
Expand All @@ -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(
Expand All @@ -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:
Expand Down Expand Up @@ -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()
Expand Down
9 changes: 9 additions & 0 deletions lint/witnesslint/witness.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down