Make the explorer robust: iterative tree, lock safety, crashes end UNKNOWN

symbolic-explorer/SymbolicExplorer.py

@@ -1,4 +1,5 @@
 import argparse
+import os
 import sys
 import threading
 from urllib.request import Request
@@ -59,7 +60,17 @@ def run_passive(self):
 
     def run_sv_comp(self):
         driver = SVCompDriver(args)
-        driver.run()
+        try:
+            driver.run()
+        except BaseException:
+            # The driver reports UNKNOWN for a failed exploration itself; this catches what fails
+            # around it. Without it the HTTP server would keep the process alive until the time limit.
+            log.get_logger().exception('[SVCOMP] The SV-COMP driver failed')
+            if not driver.verdict_reported:
+                log.get_verdict_logger().info(f'[VERDICT {driver.verification_category.value}] == DONT-KNOW')
+            for handler in log.get_logger().handlers:
+                handler.flush()
+            os._exit(1)
 
     def run_http(self):
         driver = HTTPDriver(self.args)

symbolic-explorer/constraint/ConstraintService.py

@@ -54,22 +54,29 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp
         None: The result is the side effect of adding data to the database.
         """
 
-        # logger.info(f'[CONSTRAINT SERVICE] Received trace: {[t.__str__() for t in trace]}')
-        trace_parsed: List[Branch | Special] = Parser.parse_trace(trace, trace_id=trace_id)
-        logger.info(f'[CONSTRAINT SERVICE] Parsed trace: {[t.__str__() for t in trace_parsed]}')
-        logger.info(f'[CONSTRAINT SERVICE] Parsed trace branches: {[t.__str__() for t in trace_parsed if isinstance(t, Branch)]}')
-        inputs_parsed: List[Input] = Parser.parse_inputs(inputs)
-        # logger.info(f'[CONSTRAINT SERVICE] Parsed inputs: {[i.__str__() for i in inputs_parsed]}')
-        ufs_parsed: List[UF] = Parser.parse_ufs(ufs)
-        # Flatten the missing-invocation DTOs into plain dicts so the Database/Tree stay decoupled
-        # from the pydantic request models.
-        missing_invocations_data = [item.model_dump() for item in (missing_invocations or [])]
-        # The witness data of this execution (plain dicts as well); the Database keeps the latest.
-        witness_data = {
-            'trace_id': trace_id,
-            'nondet_returns': [item.model_dump() for item in (nondet_returns or [])],
-            'violation': violation.model_dump() if violation is not None else None,
-        }
-        # Adding the trace and inputs to the database for the specified endpoint.
-        Database.instance().add_trace(endpoint_id, trace_id, trace_parsed, inputs_parsed, ufs_parsed, symbolic_context_loss, symbolic_precision_loss, reference_semantic_change, missing_invocations_data, witness_data, approximate_model)
-        logger.info(f'[CONSTRAINT SERVICE] Added trace {trace_id} to endpoint {endpoint_id}')
+        try:
+            # logger.info(f'[CONSTRAINT SERVICE] Received trace: {[t.__str__() for t in trace]}')
+            trace_parsed: List[Branch | Special] = Parser.parse_trace(trace, trace_id=trace_id)
+            logger.info(f'[CONSTRAINT SERVICE] Parsed trace: {[t.__str__() for t in trace_parsed]}')
+            logger.info(f'[CONSTRAINT SERVICE] Parsed trace branches: {[t.__str__() for t in trace_parsed if isinstance(t, Branch)]}')
+            inputs_parsed: List[Input] = Parser.parse_inputs(inputs)
+            # logger.info(f'[CONSTRAINT SERVICE] Parsed inputs: {[i.__str__() for i in inputs_parsed]}')
+            ufs_parsed: List[UF] = Parser.parse_ufs(ufs)
+            # Flatten the missing-invocation DTOs into plain dicts so the Database/Tree stay decoupled
+            # from the pydantic request models.
+            missing_invocations_data = [item.model_dump() for item in (missing_invocations or [])]
+            # The witness data of this execution (plain dicts as well); the Database keeps the latest.
+            witness_data = {
+                'trace_id': trace_id,
+                'nondet_returns': [item.model_dump() for item in (nondet_returns or [])],
+                'violation': violation.model_dump() if violation is not None else None,
+            }
+            # Adding the trace and inputs to the database for the specified endpoint.
+            Database.instance().add_trace(endpoint_id, trace_id, trace_parsed, inputs_parsed, ufs_parsed, symbolic_context_loss, symbolic_precision_loss, reference_semantic_change, missing_invocations_data, witness_data, approximate_model)
+            logger.info(f'[CONSTRAINT SERVICE] Added trace {trace_id} to endpoint {endpoint_id}')
+        except Exception as e:
+            # A trace that cannot be added must not end the run silently, nor let it go on as if the
+            # tree were complete: the driver reports UNKNOWN for it (SVCompDriver).
+            logger.exception(f'[CONSTRAINT SERVICE] Could not add trace {trace_id} to endpoint {endpoint_id}')
+            Database.instance().record_trace_ingest_failure(endpoint_id, f'trace {trace_id}: {type(e).__name__}: {e}',
+                                                            reference_semantic_change)

symbolic-explorer/data/BinaryExecutionTree/Node.py

@@ -32,16 +32,17 @@ class Node:
             (e.g. '...instruction.CLINIT'); None for 'Branch' nodes.
 
     Raises:
-        ValueError: If the trace argument is None or empty, indicating that the node cannot be created.
+        ValueError: If no trace element is given, indicating that the node cannot be created.
     """
 
-    def __init__(self, parent: Optional['Node'], trace: list, inputs: List[Input], ufs: List[UF]):
+    def __init__(self, parent: Optional['Node'], branch, inputs: List[Input], ufs: List[UF]):
         """
-        Initializes a new instance of the Node class.
+        Initializes a new instance of the Node class for one trace element. Its children are left
+        unset; Tree links the nodes of a trace into a path.
 
         Args:
             parent (Node): The parent node of this node.
-            trace (list): A list of trace elements defining the execution path.
+            branch (Branch | Special): The trace element this node stands for.
             inputs (any): The inputs associated with this node.
             ufs (any): The UFs associated with this node.
         """
@@ -62,20 +63,13 @@ def __init__(self, parent: Optional['Node'], trace: list, inputs: List[Input], u
         self.pops = 0
         self.pushes = ()
         self.callback = False  # in a callback from library code: no counterpart in the SA graph
+        # Whether some trace threw an exception the SA graph does not model right before this node
+        # (an UNMODELLED_EXCEPTION marker, which is not a node of its own, see Tree.structural).
+        self.unmodelled_exception = False
 
-        # Validate trace argument
-        if trace is None or len(trace) == 0:
+        if branch is None:
             raise ValueError(f'Cannot create Node with no branch!')
 
-        # Process the first element of the trace to determine the branch
-        branch = trace.pop(0)
-
-        # Create a child node based on remaining trace elements
-        if len(trace) == 0:
-            child = Leaf(parent=self, inputs=inputs, ufs=ufs)
-        else:
-            child = Node(parent=self, trace=trace, inputs=inputs, ufs=ufs)
-
         # Assign branch details to the node
         self.id = branch.id
         self.trace_id = branch.trace_id
@@ -84,7 +78,6 @@ def __init__(self, parent: Optional['Node'], trace: list, inputs: List[Input], u
         if isinstance(branch, Special):
             self.kind = "Special"
             self.inst = branch.inst
-            self.branched = child
         else:
             self.kind = "Branch"
             self.concrete_only = branch.concrete_only
@@ -93,11 +86,6 @@ def __init__(self, parent: Optional['Node'], trace: list, inputs: List[Input], u
             self.pushes = branch.pushes
             self.callback = branch.callback
             self.constraint[branch.trace_id] = branch.constraint
-            # Determine whether the branch was taken or skipped and assign child
-            if branch.has_branched:
-                self.branched = child
-            else:
-                self.skipped = child
 
     def is_clinit_start(self) -> bool:
         """

symbolic-explorer/data/BinaryExecutionTree/Tree.py

@@ -1,6 +1,6 @@
 from typing import List, Optional, Set, Union
 from data.trace.Branch import Branch
-from data.trace.Special import Special
+from data.trace.Special import Special, UNMODELLED_EXCEPTION
 from data.BinaryExecutionTree.Leaf import Leaf
 from data.BinaryExecutionTree.Node import Node
 from data.trace.Input import Input
@@ -129,65 +129,120 @@ def record_reference_semantic_change(self):
         logger.warning("Reference semantic change recorded: user-de-interned strings compared via Objects.equals")
         self.reference_semantic_change = True
 
-    def add(self, trace: list[Branch | Special], inputs: List[Input], ufs: List[UF]):
+    @staticmethod
+    def structural(trace: list) -> list[tuple]:
         """
-        Adds a branch to the tree based on the provided trace and inputs.
+        The elements of a trace that are levels of the tree, each with whether an
+        UNMODELLED_EXCEPTION marker came right before it.
+
+        The marker is only in the trace of a run that throws, so it cannot be a level of its own:
+        a run that does not throw has some other element at that depth. It is kept on the node
+        after it instead, for the SA walk (see dfs).
+        """
+        elements = []
+        marked = False
+        for element in trace:
+            if getattr(element, 'inst', None) == UNMODELLED_EXCEPTION:
+                marked = True
+                continue
+            elements.append((element, marked))
+            marked = False
+        return elements
+
+    def add(self, trace: list[Branch | Special], inputs: List[Input], ufs: List[UF]) -> bool:
+        """
+        Adds a trace to the tree: follows its path as far as the tree has it already, and appends
+        the rest as a new path.
+
+        If the trace has another element than the tree at some depth, the two runs did the same
+        up to there and then differently without a branch to tell them apart. The tree keeps what
+        it has, the rest of the trace is dropped, and a 'tree_mismatch' execution error records
+        that the search is no longer complete.
 
         Args:
             trace (list): A list of trace elements defining the execution path.
             inputs (any): The inputs associated with the branch being added.
             ufs (any): The UFs associated with the branch being added.
-        """
-        self.root = self.add_recursive(None, self.root, trace.copy(), inputs, ufs)
 
-    def add_recursive(self, parent: Optional[Node], node: Optional[Union[Node, Leaf]], trace: list[Branch | Special], inputs: List[Input], ufs: List[UF]):
+        Returns:
+            bool: Whether the whole trace fitted the tree.
         """
-        Recursively adds nodes or leaves to the tree.
+        elements = self.structural(trace)
+        parent: Optional[Node] = None
+        branched = False  # the side of parent that node is on
+        node = self.root
+        i = 0
+        while i < len(elements) and isinstance(node, Node):
+            element, marked = elements[i]
+            if node.id != element.id or (node.kind == "Special") != isinstance(element, Special):
+                message = f'depth {i}: tree has {node.kind} {node.id}, trace {element}'
+                logger.warning(f"Trace {getattr(element, 'trace_id', '?')} does not fit the tree ({message}), dropping its rest")
+                self.record_execution_error('tree_mismatch', message)
+                return False
+            if marked:
+                node.unmodelled_exception = True
+            if isinstance(element, Branch):
+                node.constraint[element.trace_id] = element.constraint
+            if element.has_branched:
+                if node.branched is None and node.skipped is not None:
+                    logger.info(f"New branch from node {node.id} (branched)")
+            else:
+                if node.skipped is None and node.branched is not None:
+                    logger.info(f"New branch from node {node.id} (skipped)")
+            parent, branched = node, element.has_branched
+            node = node.branched if branched else node.skipped
+            i += 1
 
-        Args:
-            parent (Node): The parent node of the current node.
-            node (Node/Leaf): The current node to add to.
-            trace (list): The remaining trace elements.
-            inputs (any): The inputs associated with the current node.
-            ufs (any): The UFs associated with the current node.
+        if i == len(elements) and node is not None:
+            return True  # the path is in the tree already
 
-        Returns:
-            Node/Leaf: The newly added or modified node or leaf.
+        # node is None or a Leaf: the rest of the trace is a new path, ending in a Leaf
+        for element, marked in elements[i:]:
+            new = Node(parent, element, inputs, ufs)
+            new.unmodelled_exception = marked
+            self._attach(parent, branched, new)
+            parent, branched = new, element.has_branched
+        self._attach(parent, branched, Leaf(parent, inputs, ufs))
+        return True
 
-        Raises:
-            ValueError: If branch IDs in the trace don't match the node's ID.
-        """
-        if node is None:
-            # Create a new Node or Leaf if the current node is None
-            return Node(parent, trace, inputs, ufs) if len(trace) > 0 else Leaf(parent, inputs, ufs)
+    def _attach(self, parent: Optional[Node], branched: bool, child: Union[Node, Leaf]):
+        """Makes child the root, or the given side of parent."""
+        if parent is None:
+            self.root = child
+        elif branched:
+            parent.branched = child
+        else:
+            parent.skipped = child
 
-        if len(trace) > 0:
+    def __deepcopy__(self, memo):
+        """
+        Copies the tree without recursing along its paths, which can be longer than the
+        interpreter's recursion limit allows.
+        """
+        import copy
+        cls = self.__class__
+        result = cls.__new__(cls)
+        memo[id(self)] = result
+        # Copy the nodes shallowly first, so that copying their other attributes below does not
+        # descend into the tree.
+        nodes = []
+        work = [self.root]
+        while work:
+            node = work.pop()
+            if node is None or id(node) in memo:
+                continue
+            memo[id(node)] = copy.copy(node)
+            nodes.append(node)
             if isinstance(node, Node):
-                new_node = trace.pop(0)
-
-                # Ensure branch IDs match
-                if node.id != new_node.id:
-                    raise ValueError(f'Branch id\'s dont match: {node.id} : {new_node.id}')
-
-                # Update constraints for the node
-                if isinstance(new_node, Branch):
-                    node.constraint[new_node.trace_id] = new_node.constraint
-
-                # Recurse into the correct branch based on the trace
-                if new_node.has_branched:
-                    if node.branched is None and node.skipped is not None:
-                        logger.info(f"New branch from node {node.id} (branched)")
-                    node.branched = self.add_recursive(node, node.branched, trace, inputs, ufs)
-                else:
-                    if node.skipped is None and node.branched is not None:
-                        logger.info(f"New branch from node {node.id} (skipped)")
-                    node.skipped = self.add_recursive(node, node.skipped, trace, inputs, ufs)
-            else:
-                # Create a new Node or Leaf if the current node is a Leaf
-                return Node(parent, trace, inputs, ufs) if len(trace) > 0 else Leaf(parent, inputs, ufs)
-
-        return node
-
+                work.append(node.skipped)
+                work.append(node.branched)
+        for node in nodes:
+            new = memo[id(node)]
+            for name, value in node.__dict__.items():
+                new.__dict__[name] = copy.deepcopy(value, memo)
+        for name, value in self.__dict__.items():
+            result.__dict__[name] = copy.deepcopy(value, memo)
+        return result
 
 # VISUALIZATIONS
     def get_constraint_label(self, parent: Node, node: Union[Node, Leaf]):
@@ -199,17 +254,21 @@ def get_constraint_label(self, parent: Node, node: Union[Node, Leaf]):
         return ""
 
     def add_to_dot(self, node: Optional[Union[Node, Leaf]], graph, parent: Optional[Node] = None):
-        """Recursively add nodes and edges to the DOT graph."""
-        if node is not None:
+        """Add the nodes and edges below node to the DOT graph."""
+        work = [(node, parent)]
+        while work:
+            node, parent = work.pop()
+            if node is None:
+                continue
             graph.add_node(node.gid, label=str(node.gid) + ':' + str(node.id))
             if parent is not None:
                 # Add an edge with constraint as a label
                 constraint_label = self.get_constraint_label(parent, node)
                 graph.add_edge(parent.gid, node.gid, label=constraint_label)
 
             if isinstance(node, Node):
-                self.add_to_dot(node.branched, graph, node)
-                self.add_to_dot(node.skipped, graph, node)
+                work.append((node.skipped, node))
+                work.append((node.branched, node))
 
     def plot_tree(self, idx):
        """Plot the tree using Graphviz and save to a file."""