From 8a4194930b6b18fa4080fe22c27f3ef954acf77a Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Tue, 7 Jul 2026 10:23:12 +0000 Subject: [PATCH] fix(explorer): fall back to concrete trace values in annotation TargetDriver When Z3's model omits a symbolic input (unconstrained on the solved path; its int bounds arrive as literal "(assert true)"), the annotation driver serialized "-Dswat.assignment.X=None", crashing the executor in the next round with NumberFormatException: For input string: "None". Register the branch inputs with their real DSE indices and keep the concrete value recorded in the trace as fallback, mirroring svcomp/SymbolicStorage. Also skip emitting an assignment when no value is known at all, so the executor keeps the target's original value instead of parsing garbage. Co-Authored-By: Claude Fable 5 --- symbolic-explorer/driver/SymbolicStorage.py | 29 +++++++++++++++++++++ symbolic-explorer/driver/TargetDriver.py | 10 ++++++- 2 files changed, 38 insertions(+), 1 deletion(-) diff --git a/symbolic-explorer/driver/SymbolicStorage.py b/symbolic-explorer/driver/SymbolicStorage.py index 8ea14fc..9b802c6 100755 --- a/symbolic-explorer/driver/SymbolicStorage.py +++ b/symbolic-explorer/driver/SymbolicStorage.py @@ -55,6 +55,35 @@ def register_vars(self, sym_vars: [str], indices: [int] = None) -> None: self.vars[int(v.idx)] = v logger.info(f'[EXPLORER] Registered symbolic variable {v.dType.name}_{v.idx}') + def register_inputs(self, inputs) -> None: + """Register symbolic variables from the inputs recorded in a trace. + + Unlike register_vars(), this keeps the concrete value observed during the + execution as fallback and uses the variable's real DSE index (parsed from + its name). If the solver's model omits a variable (e.g. it is unconstrained + on the solved path), the fallback value is used instead of emitting a + literal 'None' assignment, which would crash the executor. + Mirrors svcomp/SymbolicStorage.register_vars(). + + Args: + inputs: List of data.trace.Input objects (e.g. a branch node's inputs). + """ + for input in inputs: + dtype, _, idx = input.name.rpartition('_') + if not idx.isdigit(): + # Auxiliary inputs such as array-length variables ("[I_0_length") + # are not assignable and carry no DSE index. + logger.debug(f'[EXPLORER] Skipping auxiliary input {input.name}') + continue + try: + v = SymbolicVar(dtype=DataTypes(dtype), idx=int(idx)) + except ValueError: + logger.warning(f'[EXPLORER] Skipping input {input.name} with unknown type {dtype}') + continue + v.value = input.value + self.vars[v.idx] = v + logger.info(f'[EXPLORER] Registered symbolic variable {v.dType.name}_{v.idx} (trace value: {v.value})') + def init_values(self): for var in self.vars.values(): match var.dType: diff --git a/symbolic-explorer/driver/TargetDriver.py b/symbolic-explorer/driver/TargetDriver.py index 159680c..9b9ebf9 100644 --- a/symbolic-explorer/driver/TargetDriver.py +++ b/symbolic-explorer/driver/TargetDriver.py @@ -70,6 +70,8 @@ def build_command(self, mem: int = 32) -> [str]: # Add symbolic value assignments (if we have them) for var in self.sym_storage.vars.values(): val = var.newValue if var.newValue is not None else var.value + if val is None: + continue # no known value; the executor keeps the target's original value # Use swat.assignment prefix (read by Intrinsics.retrieveAssignments()) cmd.insert(1, f'-Dswat.assignment.{var.dType.value}_{var.idx}={val}') @@ -95,6 +97,12 @@ def add_values(self, cmd: [str]) -> [str]: else: val = var.newValue var.value = var.newValue + if val is None: + # Neither a solver value nor a concrete fallback is known; skipping the + # assignment lets the executor keep the target's original value instead + # of crashing on parsing a literal 'None'. + logger.error(f'[EXPLORER] No value known for {var.dType.value}_{var.idx}, skipping assignment') + continue if self.args.mode == "args": cmd.append(f'{val}') else: @@ -200,7 +208,7 @@ def retrieve_solution(self): sol_viz = [f'{key}: {val["plain_value"]}' for key, val in sol.items()] logger.info(f'[EXPLORER] Found new solution: {sol_viz}') - self.sym_storage.register_vars([var.name.split('_')[0] for var in symbolic_vars]) + self.sym_storage.register_inputs(symbolic_vars) self.sym_storage.store_solution(sol) return Action.SYMBOLICNEXT