From ee595026f318b0a3f32056cf316bb27319dfcf15 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 22:54:04 +0000 Subject: [PATCH 1/6] Add choice branches: executor-added branches that enumerate an operand's values Same infrastructure as the object-array index search: a branch the executor records itself, flipped by the explorer like any other, with no counterpart in the static pre-analysis graph. Co-Authored-By: Claude Opus 5.5 --- .../swat/symbolic/trace/BranchElement.java | 4 ++++ .../its/swat/symbolic/trace/DTOBuilder.java | 3 ++- .../symbolic/trace/SymbolicTraceHandler.java | 19 ++++++++++++++++ .../swat/symbolic/trace/dto/BranchDTO.java | 10 +++++++++ .../data/BinaryExecutionTree/Node.py | 2 ++ symbolic-explorer/data/trace/Branch.py | 4 +++- .../parse/DataTransferObjects.py | 3 +++ symbolic-explorer/parse/TraceParser.py | 3 ++- symbolic-explorer/strategy/DFS.py | 6 +++-- symbolic-explorer/tests/test_sa_walk.py | 22 ++++++++++++++++++- 10 files changed, 70 insertions(+), 6 deletions(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java index 08399f79..a91f3a87 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java @@ -21,6 +21,10 @@ final class BranchElement extends Element { // an array SWAT does not track. It keeps the explorer's walk of that graph in step, but has no // symbolic constraint, so the explorer never tries to flip it. private final boolean concreteOnly; + // A branch the executor adds itself to enumerate the values of a symbolic operand (e.g. which + // element of an object array a symbolic index selects). The static pre-analysis graph has no + // such branch, so the explorer flips it but does not walk the graph over it. + @lombok.Setter private boolean choice; // Where the branch is, for the explorer to check and resynchronise its walk of the static // pre-analysis graph (see BranchKeys): the branch's key, or null if its instruction has none, diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java index e272cf71..5988153a 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java @@ -143,7 +143,8 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage } } trace.add(new BranchDTO(be.getIid(), constraint, be.isBranched(), be.isConcreteOnly()) - .place(be.getKey(), be.getPops(), be.getPushes(), be.isCallback())); + .place(be.getKey(), be.getPops(), be.getPushes(), be.isCallback()) + .choice(be.isChoice())); } else if (el instanceof SpecialElement se) { trace.add(new BranchDTO(se.getIid(), se.getInst())); } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java index d8e1b62c..87f66412 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java @@ -67,6 +67,25 @@ public void checkAndSetBranch(boolean result, BooleanFormula constraint, long ii symbolicTrace.addTraceElement(current); } + /** + * Records a branch the executor adds itself to enumerate the values of a symbolic operand, e.g. + * one step of the search for the element a symbolic array index selects. It is a branch like + * any other for the explorer, which flips it to try the other values, but the static + * pre-analysis graph has no counterpart for it. + * + * @param result Whether {@code constraint} holds on this execution + * @param constraint The condition branched on + * @param iid The iid of the instruction the operand belongs to + * @param suffix Tells the instruction's branches apart in their keys + */ + public void addChoiceBranch(boolean result, BooleanFormula constraint, long iid, String suffix) throws NoThreadContextException { + FormulaManager fmgr = ThreadHandler.getSolverContext(Thread.currentThread().getId()).getFormulaManager(); + BranchElement branch = new BranchElement(result, result ? constraint : fmgr.getBooleanFormulaManager().not(constraint), iid); + branch.setChoice(true); + place(branch, iid, suffix); + symbolicTrace.addTraceElement(branch); + } + /** Records where a branch is: its key and the change of the frame stack since the last branch. */ private static void place(BranchElement branch, long iid, String suffix) throws NoThreadContextException { String key = BranchKeys.keyOf(iid); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java index 5a917bb2..6475567c 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java @@ -32,6 +32,16 @@ public class BranchDTO { @com.fasterxml.jackson.annotation.JsonInclude(com.fasterxml.jackson.annotation.JsonInclude.Include.NON_DEFAULT) private boolean callback; + // See BranchElement: a branch the executor adds that the static pre-analysis graph does not have. + @SuppressWarnings("unused") + @com.fasterxml.jackson.annotation.JsonInclude(com.fasterxml.jackson.annotation.JsonInclude.Include.NON_DEFAULT) + private boolean choice; + + public BranchDTO choice(boolean choice) { + this.choice = choice; + return this; + } + public BranchDTO place(String key, int pops, java.util.List pushes, boolean callback) { this.key = key; this.pops = pops; diff --git a/symbolic-explorer/data/BinaryExecutionTree/Node.py b/symbolic-explorer/data/BinaryExecutionTree/Node.py index 5a1fd91b..b82ef17c 100755 --- a/symbolic-explorer/data/BinaryExecutionTree/Node.py +++ b/symbolic-explorer/data/BinaryExecutionTree/Node.py @@ -62,6 +62,7 @@ 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 + self.choice = False # added by the executor to enumerate an operand's values: not in the SA graph # Validate trace argument if trace is None or len(trace) == 0: @@ -92,6 +93,7 @@ def __init__(self, parent: Optional['Node'], trace: list, inputs: List[Input], u self.pops = branch.pops self.pushes = branch.pushes self.callback = branch.callback + self.choice = branch.choice self.constraint[branch.trace_id] = branch.constraint # Determine whether the branch was taken or skipped and assign child if branch.has_branched: diff --git a/symbolic-explorer/data/trace/Branch.py b/symbolic-explorer/data/trace/Branch.py index afc93cc8..227934fe 100755 --- a/symbolic-explorer/data/trace/Branch.py +++ b/symbolic-explorer/data/trace/Branch.py @@ -14,7 +14,7 @@ class Branch: """ def __init__(self, id: int, trace_id: str, has_branched: bool, constraint: str, concrete_only: bool = False, - key: str | None = None, pops: int = 0, pushes: tuple = (), callback: bool = False): + key: str | None = None, pops: int = 0, pushes: tuple = (), callback: bool = False, choice: bool = False): """ Initializes a new instance of the Branch class. @@ -37,6 +37,8 @@ def __init__(self, id: int, trace_id: str, has_branched: bool, constraint: str, self.pushes = pushes # In application code that library code called back, which the SA graph does not have. self.callback = callback + # Added by the executor to enumerate the values of a symbolic operand; not in the SA graph. + self.choice = choice def __str__(self): return f'[(B) - {self.id} - ({"T" if self.has_branched else "F"})]' \ No newline at end of file diff --git a/symbolic-explorer/parse/DataTransferObjects.py b/symbolic-explorer/parse/DataTransferObjects.py index 68be5da1..7355e590 100644 --- a/symbolic-explorer/parse/DataTransferObjects.py +++ b/symbolic-explorer/parse/DataTransferObjects.py @@ -19,6 +19,9 @@ class TraceItem(BaseModel): pushes: list[Optional[str]] = [] # Recorded in application code that library code called back: not in the SA graph. callback: bool = False + # A branch the executor adds to enumerate the values of a symbolic operand (e.g. the element a + # symbolic array index selects): flipped like any other, but not in the SA graph. + choice: bool = False class UFItem(BaseModel): definition: str diff --git a/symbolic-explorer/parse/TraceParser.py b/symbolic-explorer/parse/TraceParser.py index 8b005c7d..439c9843 100755 --- a/symbolic-explorer/parse/TraceParser.py +++ b/symbolic-explorer/parse/TraceParser.py @@ -23,7 +23,8 @@ def parse_trace(trace: List[TraceItem], trace_id: str) -> List[Branch | Special] key=branch.key, pops=branch.pops, pushes=tuple(branch.pushes), - callback=branch.callback)) + callback=branch.callback, + choice=branch.choice)) else: _trace.append(Special(id=branch.iid, trace_id=trace_id, diff --git a/symbolic-explorer/strategy/DFS.py b/symbolic-explorer/strategy/DFS.py index b8d52078..ffc490ef 100755 --- a/symbolic-explorer/strategy/DFS.py +++ b/symbolic-explorer/strategy/DFS.py @@ -57,7 +57,9 @@ def dfs(visited: set[Node], tree, node: Node | Leaf | None, solved_branches: set # If clinit_depth > 0, we do not have corresponding SA information, so pretend that there is no SA and DON'T WALK the SA graph. # Likewise for a branch in application code that library code called back: the graph walks # over the library call, so the walk holds its place until the callback returns. - mask_sa_node = clinit_depth > 0 or node.callback + # A choice branch (the executor's search for the element a symbolic index selects) has no + # graph node either: both of its sides continue from the walk's current place. + mask_sa_node = clinit_depth > 0 or node.callback or node.choice # Get information on interesting paths. If sa_node is None, all paths should be considered interesting if sa_node and not mask_sa_node: @@ -81,7 +83,7 @@ def dfs(visited: set[Node], tree, node: Node | Leaf | None, solved_branches: set skip_is_interesting = mask_sa_node or (sa_node is None) or is_interesting(sa_node.get_fallthrough_child(), sa_stack) branch_is_interesting = mask_sa_node or (sa_node is None) or is_interesting(sa_node.get_branched_child(), sa_stack) - logger.info(f"[DFS] @{node.id}/{("CALLBACK" if node.callback else "CLINIT") if mask_sa_node else sa_node and sa_node.id} ({"branched" if node.branched else ""}{"skipped" if node.skipped else ""}): skip_is_interesting={skip_is_interesting}, branch_is_interesting={branch_is_interesting}") + logger.info(f"[DFS] @{node.id}/{("CALLBACK" if node.callback else "CHOICE" if node.choice else "CLINIT") if mask_sa_node else sa_node and sa_node.id} ({"branched" if node.branched else ""}{"skipped" if node.skipped else ""}): skip_is_interesting={skip_is_interesting}, branch_is_interesting={branch_is_interesting}") # Add the node itself, if eligible if (node.skipped is None and skip_is_interesting) or (node.branched is None and branch_is_interesting): diff --git a/symbolic-explorer/tests/test_sa_walk.py b/symbolic-explorer/tests/test_sa_walk.py index d1977625..21c0074f 100644 --- a/symbolic-explorer/tests/test_sa_walk.py +++ b/symbolic-explorer/tests/test_sa_walk.py @@ -95,7 +95,7 @@ def load(self) -> SAGraph: os.unlink(path) -def branch_node(name, skipped=None, branched=None, key=None, pops=0, pushes=(), callback=False): +def branch_node(name, skipped=None, branched=None, key=None, pops=0, pushes=(), callback=False, choice=False): """A tree node for one branch event; `None` children are unexplored sides.""" n = Node.__new__(Node) n.parent = None @@ -109,6 +109,7 @@ def branch_node(name, skipped=None, branched=None, key=None, pops=0, pushes=(), n.pops = pops n.pushes = pushes n.callback = callback + n.choice = choice n.constraint = {} n.skipped = skipped n.branched = branched @@ -543,6 +544,25 @@ def test_callback_branches_are_masked(self): _, desyncs = self.run_dfs(tree, g) self.assertEqual(len(desyncs), 1) + def test_choice_branches_are_masked(self): + g = self.graph() + plain, _ = self.run_dfs(self.tree(), g) + # Before f is called, an access at a symbolic index adds two choice branches the graph does + # not have, one with an unexplored side. Masked, the walk holds its place over them, and + # they are still solver targets. + tree = self.tree() + nf = tree.skipped + ch2 = branch_node('ch2', skipped=None, branched=nf, key='M|1|aaload|0#idx1', choice=True) + ch1 = branch_node('ch1', skipped=ch2, branched=leaf(), key='M|1|aaload|0#idx0', choice=True) + tree.skipped = ch1 + found, desyncs = self.run_dfs(tree, g) + self.assertEqual(desyncs, []) + self.assertEqual(found, plain | {'ch2'}) + for n in (ch1, ch2): + n.choice = False + _, desyncs = self.run_dfs(tree, g) + self.assertEqual(len(desyncs), 1) + def test_open_ordinal_matches_any_on_its_line(self): g = self.graph() g.nodes['bf'].key = 'F|10|if|*' From 4c79e6902f8be0b9034d5515400104d31e9a9a42 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:03:08 +0000 Subject: [PATCH 2/6] Model Integer/Long toString and toUnsignedString with a radix The digits of a constant radix up to 10 are encoded as str.from_int of the integer with the same decimal digits, which Z3 decides directly; the per-digit concatenation cut to a symbolic length timed out or gave models that violate the constraint (Integer.toBinaryString diverged). toBinaryString and toOctalString now use the same encoding. A symbolic radix is pinned to its concrete value by choice branches (binary search over 2..36 on the radix after the JDK's fallback to 10), so the conversion is exact on each path with a constant radix. Co-Authored-By: Claude Opus 5.5 --- .../symbolic/invoke/java/lang/BitOps.java | 11 +- .../invoke/java/lang/IntegerInvocation.java | 30 +-- .../invoke/java/lang/LongInvocation.java | 30 +-- .../invoke/java/lang/NumberStrings.java | 246 ++++++++++++++++++ 4 files changed, 281 insertions(+), 36 deletions(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStrings.java diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BitOps.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BitOps.java index 4562dcd0..1ad13ad0 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BitOps.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BitOps.java @@ -92,8 +92,13 @@ static BitvectorFormula compare(SolverContext ctx, BitvectorFormula x, Bitvector * The unsigned value of {@code x} in radix 2^shift without leading zeros ("0" for zero), as * Integer/Long.toBinaryString (shift 1), toOctalString (shift 3) and toHexString (shift 4): the * string of all digits (each one str.from_code of its value), from the highest non-zero digit on. + * Radixes up to 8 only have decimal digits and use the str.from_int encoding of {@link + * NumberStrings}, which the solver handles far better. */ static StringFormula toUnsignedPowerOfTwoString(SolverContext ctx, BitvectorFormula x, int width, int shift) { + if (shift <= 3) { + return NumberStrings.unsignedDigits(ctx, x, width, 1 << shift); + } BitvectorFormulaManager bv = ctx.getFormulaManager().getBitvectorFormulaManager(); BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); StringFormulaManager smgr = ctx.getFormulaManager().getStringFormulaManager(); @@ -106,10 +111,8 @@ static StringFormula toUnsignedPowerOfTwoString(SolverContext ctx, BitvectorForm int lo = k * shift; int hi = Math.min(lo + shift, width) - 1; IntegerFormula digit = bv.toIntegerFormula(bv.extract(x, hi, lo), false); - IntegerFormula code = shift < 4 - ? imgr.add(digit, imgr.makeNumber('0')) - : imgr.add(digit, bmgr.ifThenElse(imgr.greaterThan(digit, imgr.makeNumber(9)), - imgr.makeNumber('a' - 10), imgr.makeNumber('0'))); + IntegerFormula code = imgr.add(digit, bmgr.ifThenElse(imgr.greaterThan(digit, imgr.makeNumber(9)), + imgr.makeNumber('a' - 10), imgr.makeNumber('0'))); chars.add(0, smgr.fromCodePoint(code)); if (k > 0) { start = bmgr.ifThenElse(bv.equal(bv.extract(x, hi, lo), c(bv, hi - lo + 1, 0)), diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/IntegerInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/IntegerInvocation.java index ab6e95f1..4b388a22 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/IntegerInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/IntegerInvocation.java @@ -1,5 +1,6 @@ package de.uzl.its.swat.symbolic.invoke.java.lang; +import de.uzl.its.swat.common.exceptions.NoThreadContextException; import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.symbolic.value.PlaceHolder; @@ -16,7 +17,7 @@ public class IntegerInvocation { - public static Value invokeStaticMethod(String name, Value[] args, Type[] desc) throws ValueConversionException, NotImplementedException { + public static Value invokeStaticMethod(String name, Value[] args, Type[] desc) throws ValueConversionException, NotImplementedException, NoThreadContextException { return switch (name) { case "bitCount" -> invokeBitCount(args); case "compare" -> invokeCompare(args); @@ -749,14 +750,16 @@ private static IntValue sum(IntValue a, IntValue b) { * type, likely a missing implementation */ private static Value invokeToString(Value[] args) - throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException { + throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException, NoThreadContextException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; - if (args.length == 1 && args[0] instanceof IntValue iv) { - return toString(iv); + if (args.length == 1) { + return args[0] instanceof IntValue iv ? toString(iv) : PlaceHolder.instance; } - // toString with radix not yet supported - return PlaceHolder.instance; + IntValue i = args[0].asIntValue(); + int radix = NumberStrings.selectRadix(args[1].asIntValue()); + return new StringValue(i.context, Integer.toString(i.concrete, radix), + NumberStrings.toString(i.context, i.formula, 32, true, radix), ObjectValue.ADDRESS_UNKNOWN); } /** @@ -840,18 +843,13 @@ private static LongValue toUnsignedLong(IntValue x) { * type, likely a missing implementation */ private static Value invokeToUnsignedString(Value[] args) - throws IndexOutOfBoundsException, ValueConversionException { + throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException, NoThreadContextException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; - if (args.length == 1 && args[0] instanceof IntValue i) { - // the decimal digits of the unsigned value; the radix variant is not modelled - SolverContext ctx = i.context; - StringFormulaManager sfm = ctx.getFormulaManager().getStringFormulaManager(); - BitvectorFormulaManager bvmgr = ctx.getFormulaManager().getBitvectorFormulaManager(); - return new StringValue(ctx, Integer.toUnsignedString(i.concrete), - sfm.toStringFormula(bvmgr.toIntegerFormula(i.formula, false)), ObjectValue.ADDRESS_UNKNOWN); - } - return PlaceHolder.instance; + IntValue i = args[0].asIntValue(); + int radix = args.length == 1 ? 10 : NumberStrings.selectRadix(args[1].asIntValue()); + return new StringValue(i.context, Integer.toUnsignedString(i.concrete, radix), + NumberStrings.toString(i.context, i.formula, 32, false, radix), ObjectValue.ADDRESS_UNKNOWN); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/LongInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/LongInvocation.java index bac192bc..b046e8ca 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/LongInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/LongInvocation.java @@ -1,5 +1,6 @@ package de.uzl.its.swat.symbolic.invoke.java.lang; +import de.uzl.its.swat.common.exceptions.NoThreadContextException; import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; @@ -27,7 +28,7 @@ public class LongInvocation { String name, Value[] args, Type[] desc, - SymbolicTraceHandler symbolicTraceHandler) throws ValueConversionException, NotImplementedException { + SymbolicTraceHandler symbolicTraceHandler) throws ValueConversionException, NotImplementedException, NoThreadContextException { return switch (name) { case "bitCount" -> invokeBitCount(args); case "compare" -> invokeCompare(args); @@ -761,14 +762,16 @@ private static LongValue sum(LongValue a, LongValue b) { * type, likely a missing implementation */ private static Value invokeToString(Value[] args) - throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException { + throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException, NoThreadContextException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; - if (args.length == 1 && args[0] instanceof LongValue lv) { - return toString(lv); + if (args.length == 1) { + return args[0] instanceof LongValue lv ? toString(lv) : PlaceHolder.instance; } - // toString with radix not yet supported - return PlaceHolder.instance; + LongValue l = args[0].asLongValue(); + int radix = NumberStrings.selectRadix(args[1].asIntValue()); + return new StringValue(l.context, Long.toString(l.concrete, radix), + NumberStrings.toString(l.context, l.formula, 64, true, radix), ObjectValue.ADDRESS_UNKNOWN); } /** @@ -821,18 +824,13 @@ private static StringValue toString(LongValue l) { * type, likely a missing implementation */ private static Value invokeToUnsignedString(Value[] args) - throws IndexOutOfBoundsException, ValueConversionException { + throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException, NoThreadContextException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; - if (args.length == 1 && args[0] instanceof LongValue i) { - // the decimal digits of the unsigned value; the radix variant is not modelled - SolverContext ctx = i.context; - StringFormulaManager sfm = ctx.getFormulaManager().getStringFormulaManager(); - BitvectorFormulaManager bvmgr = ctx.getFormulaManager().getBitvectorFormulaManager(); - return new StringValue(ctx, Long.toUnsignedString(i.concrete), - sfm.toStringFormula(bvmgr.toIntegerFormula(i.formula, false)), ObjectValue.ADDRESS_UNKNOWN); - } - return PlaceHolder.instance; + LongValue l = args[0].asLongValue(); + int radix = args.length == 1 ? 10 : NumberStrings.selectRadix(args[1].asIntValue()); + return new StringValue(l.context, Long.toUnsignedString(l.concrete, radix), + NumberStrings.toString(l.context, l.formula, 64, false, radix), ObjectValue.ADDRESS_UNKNOWN); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStrings.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStrings.java new file mode 100644 index 00000000..940e3d18 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStrings.java @@ -0,0 +1,246 @@ +package de.uzl.its.swat.symbolic.invoke.java.lang; + +import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue; +import de.uzl.its.swat.thread.ThreadHandler; +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.List; +import org.sosy_lab.java_smt.api.BitvectorFormula; +import org.sosy_lab.java_smt.api.BitvectorFormulaManager; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.IntegerFormulaManager; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.StringFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; + +/** + * Exact encodings of the integral number-to-string conversions: Integer/Long/Short/Byte toString, + * toUnsignedString and their radix variants, and the string conversion of numbers in string + * concatenation. Every method takes a bit-vector of the given width and returns the string the JDK + * produces for it, digit for digit. + * + *

A digit string that only has decimal digits (radix 10 and below) is the str.from_int of the + * integer whose decimal digits it has. Z3 decides str.from_int directly, whereas a concatenation of + * one string per digit, cut to a symbolic length, makes even an equality with a constant time out + * or yield a model that violates the constraint. Only radixes above 10 need per-digit characters. + */ +public final class NumberStrings { + + private NumberStrings() {} + + /** + * The decimal string of {@code x}, read as a signed or an unsigned number of {@code width} bits. + * str.from_int is undefined ("") for negative numbers, so a negative value is "-" followed by + * the digits of its magnitude 2^width - x. + */ + public static StringFormula decimal(SolverContext ctx, BitvectorFormula x, int width, boolean signed) { + FormulaManager fmgr = ctx.getFormulaManager(); + BitvectorFormulaManager bv = fmgr.getBitvectorFormulaManager(); + StringFormulaManager smgr = fmgr.getStringFormulaManager(); + IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + IntegerFormula unsigned = bv.toIntegerFormula(x, false); + if (!signed) { + return smgr.toStringFormula(unsigned); + } + IntegerFormula magnitude = imgr.subtract(imgr.makeNumber(BigInteger.ONE.shiftLeft(width)), unsigned); + return fmgr.getBooleanFormulaManager().ifThenElse( + bv.lessThan(x, bv.makeBitvector(width, 0), true), + smgr.concat(smgr.makeString("-"), smgr.toStringFormula(magnitude)), + smgr.toStringFormula(unsigned)); + } + + /** + * The string of {@code x} in {@code radix} (2 to 36, see {@link #normaliseRadix}), as + * Integer/Long.toString(x, radix) for a signed and toUnsignedString(x, radix) for an unsigned + * {@code x}: the digits of the magnitude without leading zeros ("0" for zero), digits above 9 as + * the letters a to z, and "-" in front of a negative value. + */ + public static StringFormula toString(SolverContext ctx, BitvectorFormula x, int width, boolean signed, int radix) { + assert radix >= Character.MIN_RADIX && radix <= Character.MAX_RADIX : "[SWAT] Radix out of range: " + radix; + if (radix == 10) { + return decimal(ctx, x, width, signed); + } + if (!signed) { + return unsignedDigits(ctx, x, width, radix); + } + FormulaManager fmgr = ctx.getFormulaManager(); + BitvectorFormulaManager bv = fmgr.getBitvectorFormulaManager(); + BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager(); + StringFormulaManager smgr = fmgr.getStringFormulaManager(); + BooleanFormula negative = bv.lessThan(x, bv.makeBitvector(width, 0), true); + // as an unsigned number, -MIN_VALUE is the magnitude of MIN_VALUE + BitvectorFormula magnitude = bmgr.ifThenElse(negative, bv.negate(x), x); + StringFormula digits = unsignedDigits(ctx, magnitude, width, radix); + return bmgr.ifThenElse(negative, smgr.concat(smgr.makeString("-"), digits), digits); + } + + /** The radix the JDK uses for {@code radix}: radixes outside 2 to 36 mean 10. */ + public static int normaliseRadix(int radix) { + return radix < Character.MIN_RADIX || radix > Character.MAX_RADIX ? 10 : radix; + } + + /** + * The radix a call with the radix argument {@code radix} converts to, after {@link + * #normaliseRadix}. A symbolic radix is pinned to its concrete value by choice branches: a + * binary search over 2 to 36 on the normalised radix, one branch {@code radix < mid} per step, + * each taken as the concrete radix says. The conversion is then exact on this path with a + * constant radix, and the explorer reaches the other radixes by flipping the branches. (A + * formula that chooses between the radixes itself is exact too, but no solver query on it + * finishes.) + * + * @param radix The radix argument + * @return The normalised concrete radix + */ + public static int selectRadix(IntValue radix) throws NoThreadContextException { + int concrete = normaliseRadix(radix.concrete); + SolverContext ctx = radix.context; + FormulaManager fmgr = ctx.getFormulaManager(); + try { + if (fmgr.extractVariables(fmgr.simplify(radix.formula)).isEmpty()) { + return concrete; + } + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + } + BitvectorFormulaManager bv = fmgr.getBitvectorFormulaManager(); + BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager(); + BitvectorFormula r = radix.formula; + BitvectorFormula normalised = bmgr.ifThenElse( + bmgr.or(bv.lessThan(r, bv.makeBitvector(32, Character.MIN_RADIX), true), + bv.greaterThan(r, bv.makeBitvector(32, Character.MAX_RADIX), true)), + bv.makeBitvector(32, 10), r); + long threadId = Thread.currentThread().getId(); + // the call site of the conversion: its frame is the active one while the model runs + long iid = ThreadHandler.getSymbolicVisitor(threadId).getStack().getActiveFrame().getCallSite(); + int lo = Character.MIN_RADIX; + int hi = Character.MAX_RADIX + 1; + int step = 0; + while (hi - lo > 1) { + int mid = lo + (hi - lo) / 2; + boolean below = concrete < mid; + BooleanFormula constraint = bv.lessThan(normalised, bv.makeBitvector(32, mid), true); + ThreadHandler.getSymbolicTraceHandler(threadId).addChoiceBranch(below, constraint, iid, "#radix" + step++); + if (below) { + hi = mid; + } else { + lo = mid; + } + } + return concrete; + } + + /** + * The digits of the unsigned value of {@code m} in {@code radix} (2 to 36, not 10 for a value + * that str.from_int handles directly), without leading zeros ("0" for zero). + */ + static StringFormula unsignedDigits(SolverContext ctx, BitvectorFormula m, int width, int radix) { + int shift = Integer.numberOfTrailingZeros(radix); + boolean powerOfTwo = Integer.bitCount(radix) == 1; + if (radix == 10) { + return decimal(ctx, m, width, false); + } + if (radix < 10) { + return decimalDigitString(ctx, digits(ctx, m, width, radix)); + } + if (powerOfTwo) { + return BitOps.toUnsignedPowerOfTwoString(ctx, m, width, shift); + } + return letterDigitString(ctx, m, width, radix, digits(ctx, m, width, radix)); + } + + /** The number of digits of the largest unsigned value of {@code width} bits in {@code radix}. */ + private static int digitCount(int width, int radix) { + BigInteger max = BigInteger.ONE.shiftLeft(width).subtract(BigInteger.ONE); + BigInteger r = BigInteger.valueOf(radix); + int n = 1; + for (BigInteger p = r; p.compareTo(max) <= 0; p = p.multiply(r)) { + n++; + } + return n; + } + + /** + * The digits of the unsigned value of {@code m} in {@code radix}, least significant first, each + * a bit-vector of width at most 6 (the number of digits {@link #digitCount}). Power-of-two + * digits are bit fields; the others come from a chain of divisions by the constant radix, which + * repeats no subterm (q_k only appears in q_k+1 and in digit k). + */ + private static List digits(SolverContext ctx, BitvectorFormula m, int width, int radix) { + BitvectorFormulaManager bv = ctx.getFormulaManager().getBitvectorFormulaManager(); + int n = digitCount(width, radix); + List digits = new ArrayList<>(n); + if (Integer.bitCount(radix) == 1) { + int shift = Integer.numberOfTrailingZeros(radix); + for (int k = 0; k < n; k++) { + int lo = k * shift; + digits.add(bv.extract(m, Math.min(lo + shift, width) - 1, lo)); + } + return digits; + } + BitvectorFormula r = bv.makeBitvector(width, radix); + BitvectorFormula q = m; + for (int k = 0; k < n; k++) { + digits.add(bv.extract(bv.remainder(q, r, false), 5, 0)); + if (k < n - 1) { + q = bv.divide(q, r, false); + } + } + return digits; + } + + /** + * The string of decimal digits {@code digits} (least significant first, each below 10) without + * leading zeros: str.from_int of the sum of digit_k * 10^k. + */ + private static StringFormula decimalDigitString(SolverContext ctx, List digits) { + FormulaManager fmgr = ctx.getFormulaManager(); + BitvectorFormulaManager bv = fmgr.getBitvectorFormulaManager(); + IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + List terms = new ArrayList<>(digits.size()); + BigInteger power = BigInteger.ONE; + for (BitvectorFormula digit : digits) { + terms.add(imgr.multiply(bv.toIntegerFormula(digit, false), imgr.makeNumber(power))); + power = power.multiply(BigInteger.TEN); + } + return fmgr.getStringFormulaManager().toStringFormula(imgr.sum(terms)); + } + + /** + * The string of the radix-{@code radix} digits {@code digits} of {@code m} (least significant + * first), digits above 9 as the letters a to z: all digits as characters, from the most + * significant non-zero one on. + */ + private static StringFormula letterDigitString(SolverContext ctx, BitvectorFormula m, int width, int radix, + List digits) { + FormulaManager fmgr = ctx.getFormulaManager(); + BitvectorFormulaManager bv = fmgr.getBitvectorFormulaManager(); + BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager(); + IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + StringFormulaManager smgr = fmgr.getStringFormulaManager(); + int n = digits.size(); + List chars = new ArrayList<>(n); + // index (from the left) of the first character of the result + IntegerFormula start = imgr.makeNumber(n - 1); + BigInteger power = BigInteger.ONE; + for (int k = 0; k < n; k++) { + // the character code in 8 bits: digit + '0' or digit - 10 + 'a' + BitvectorFormula digit = bv.extend(digits.get(k), 8 - bv.getLength(digits.get(k)), false); + BitvectorFormula code = bv.add(digit, bmgr.ifThenElse( + bv.greaterThan(digit, bv.makeBitvector(8, 9), false), + bv.makeBitvector(8, 'a' - 10), bv.makeBitvector(8, '0'))); + chars.add(0, smgr.fromCodePoint(bv.toIntegerFormula(code, false))); + if (k > 0) { + // m >= radix^k: digit k is not a leading zero + start = bmgr.ifThenElse( + bv.greaterOrEquals(m, bv.makeBitvector(width, power), false), + imgr.makeNumber(n - 1 - k), start); + } + power = power.multiply(BigInteger.valueOf(radix)); + } + return smgr.substring(smgr.concat(chars), start, imgr.subtract(imgr.makeNumber(n), start)); + } +} From 3c8ea300e07cd9c253b20ed775899277ed3e251e Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:03:08 +0000 Subject: [PATCH 3/6] Fix the string of a negative long or short in concatenation LongValue/ShortValue.asStringValue used str.from_int of the signed value, which is "" for a negative number; StringBuilder.append(long) and string concatenation of a long or short now get the '-' and the digits of the magnitude. Co-Authored-By: Claude Opus 5.5 --- .../value/primitive/numeric/integral/LongValue.java | 6 +++--- .../value/primitive/numeric/integral/ShortValue.java | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java index 36c157ef..369e184f 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java @@ -1,5 +1,6 @@ package de.uzl.its.swat.symbolic.value.primitive.numeric.integral; +import de.uzl.its.swat.symbolic.invoke.java.lang.NumberStrings; import de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue; @@ -402,12 +403,11 @@ public DoubleValue asDoubleValue() { @Override public StringValue asStringValue() { - // String theory requires IntegerFormula, so convert BV to Int - NumeralFormula.IntegerFormula intFormula = bvmgr.toIntegerFormula(formula, true); + // str.from_int of a negative number is "", so the sign is handled separately return new StringValue( this.context, String.valueOf(concrete), - context.getFormulaManager().getStringFormulaManager().toStringFormula(intFormula), + NumberStrings.decimal(context, formula, 64, true), -1); } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java index 16645268..1980d170 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java @@ -1,5 +1,6 @@ package de.uzl.its.swat.symbolic.value.primitive.numeric.integral; +import de.uzl.its.swat.symbolic.invoke.java.lang.NumberStrings; import de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue; @@ -219,12 +220,11 @@ public ShortObjectValue asObjectValue() { @Override public StringValue asStringValue() { - // String theory requires IntegerFormula, so convert BV to Int - NumeralFormula.IntegerFormula intFormula = bvmgr.toIntegerFormula(formula, true); + // str.from_int of a negative number is "", so the sign is handled separately return new StringValue( this.context, String.valueOf(concrete), - context.getFormulaManager().getStringFormulaManager().toStringFormula(intFormula), + NumberStrings.decimal(context, formula, 16, true), -1); } From b701046c1de26b175bb0967c0891f6223efa2b15 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:03:08 +0000 Subject: [PATCH 4/6] Convert floats and doubles to their concrete string String.valueOf(float/double), StringBuilder.append(F/D) and string concatenation threw NotImplementedException, which ended the run even for a concrete value. The string is now the concrete one; a symbolic value records context loss, as no exact encoding of the shortest decimal representation is practical. Co-Authored-By: Claude Opus 5.5 --- .../numeric/floatingpoint/DoubleValue.java | 23 +++++++++++++++---- .../numeric/floatingpoint/FloatValue.java | 23 +++++++++++++++---- 2 files changed, 38 insertions(+), 8 deletions(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java index 0bacd823..e4737b72 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java @@ -1,5 +1,8 @@ package de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint; +import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; +import de.uzl.its.swat.thread.ThreadHandler; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BitvectorFormulaManager; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -441,10 +444,22 @@ public LongValue asLongValue() { return D2L(); } - //@Override - //public StringValue asStringValue() { - // return new StringValue(context, String.valueOf(concrete), -1); - //} + /** + * The string of the concrete value, as String.valueOf(double). The shortest decimal string that + * identifies the value has no practical exact encoding, so a symbolic value loses its link to + * the string: context loss. + */ + @Override + public StringValue asStringValue() { + if (isSymbolic()) { + try { + ThreadHandler.getSymbolicTraceHandler(Thread.currentThread().getId()).recordSymbolicContextLoss(); + } catch (NoThreadContextException e) { + throw new IllegalStateException("[SWAT] No thread context for a symbolic double", e); + } + } + return new StringValue(context, String.valueOf(concrete), ObjectValue.ADDRESS_UNKNOWN); + } @Override public DoubleObjectValue asObjectValue(){ diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java index 2f14df0e..992d7bee 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java @@ -1,5 +1,8 @@ package de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint; +import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; +import de.uzl.its.swat.thread.ThreadHandler; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BitvectorFormulaManager; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -391,10 +394,22 @@ public DoubleValue asDoubleValue() { return F2D(); } - //@Override - //public StringValue asStringValue() { - // return new StringValue(context, String.valueOf(concrete), -1); - //} + /** + * The string of the concrete value, as String.valueOf(float). The shortest decimal string that + * identifies the value has no practical exact encoding, so a symbolic value loses its link to + * the string: context loss. + */ + @Override + public StringValue asStringValue() { + if (isSymbolic()) { + try { + ThreadHandler.getSymbolicTraceHandler(Thread.currentThread().getId()).recordSymbolicContextLoss(); + } catch (NoThreadContextException e) { + throw new IllegalStateException("[SWAT] No thread context for a symbolic float", e); + } + } + return new StringValue(context, String.valueOf(concrete), ObjectValue.ADDRESS_UNKNOWN); + } @Override public FloatObjectValue asObjectValue(){ From f4486e333234d707504f61db0ddf562c260c0ef7 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:03:08 +0000 Subject: [PATCH 5/6] Solve program branches before choice branches A choice branch enumerates another value of an operand (e.g. another radix) and restarts from there; the program's own branches on the path come first, in DFS order otherwise. Co-Authored-By: Claude Opus 5.5 --- symbolic-explorer/driver/SVCompDriver.py | 7 ++++++- symbolic-explorer/tests/test_solver_rlimit.py | 12 ++++++++++-- 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a6c70f11..99325f8e 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -356,12 +356,17 @@ def solve_candidates(self, candidates: list[Node]) -> tuple[Node | None, dict, b the ones that ran out are tried again, until one is SAT or all are decided. A branch that runs out even at MAX_RLIMIT is given up on. + Choice branches (which the executor adds to enumerate the values of a symbolic operand, + e.g. a radix) go after the program's own branches of the same level: a program branch + leads somewhere new on the path it is on, while a choice branch starts over with another + value of the operand. + The limit only serves to let other branches go first. So once a retry pass is left with a single branch, that one is solved without a limit: escalating it step by step would only redo the same work at each step. """ gave_up = False - pending = sorted(candidates, key=lambda b: self.rlimit_level.get(b.gid, 0)) + pending = sorted(candidates, key=lambda b: (self.rlimit_level.get(b.gid, 0), b.choice)) retry = False while pending: limited = [] diff --git a/symbolic-explorer/tests/test_solver_rlimit.py b/symbolic-explorer/tests/test_solver_rlimit.py index 288d0e7f..0c0f60aa 100644 --- a/symbolic-explorer/tests/test_solver_rlimit.py +++ b/symbolic-explorer/tests/test_solver_rlimit.py @@ -20,8 +20,8 @@ BASE = 1000 -def branch(gid): - return SimpleNamespace(gid=gid, id=gid) +def branch(gid, choice=False): + return SimpleNamespace(gid=gid, id=gid, choice=choice) class FakeSolver: @@ -52,6 +52,14 @@ def solve(self, d, candidates, solver): with mock.patch.object(svcomp.StrategyService, 'solve_branch', side_effect=solver): return d.solve_candidates(candidates) + def test_choice_branches_come_after_program_branches(self): + # 1 is a choice branch (e.g. another radix), 2 a branch of the program: both SAT, 2 first. + d = self.driver(rlimit=None) + s = FakeSolver({}, {1: SATResult.SAT, 2: SATResult.SAT}) + found, sol, gave_up = self.solve(d, [branch(1, choice=True), branch(2)], s) + self.assertEqual(found.gid, 2) + self.assertEqual(s.calls, [(2, None)]) + def test_cheap_queries_come_before_retries(self): # 1 needs 20x the base limit, 2 is UNSAT, 3 is SAT: 3 is found before 1 is retried. d = self.driver() From 2b6ba3160c4fefe918ec7b54c2b52bde038a8217 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:05:16 +0000 Subject: [PATCH 6/6] Test the number-to-string models against the JDK Every radix 2..36 and radixes outside that range on edge values for Integer/Long toString and toUnsignedString, the one-argument variants, the string of numbers in concatenation, and a forked-agent test of the radix choice branches. Co-Authored-By: Claude Opus 5.5 --- .../invoke/java/lang/NumberStringsSpec.groovy | 209 ++++++++++++++++++ .../java/lang/RadixChoiceAgentSpec.groovy | 85 +++++++ .../test/resources/targets/radix/Main.java | 13 ++ 3 files changed, 307 insertions(+) create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStringsSpec.groovy create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/RadixChoiceAgentSpec.groovy create mode 100644 symbolic-executor/src/test/resources/targets/radix/Main.java diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStringsSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStringsSpec.groovy new file mode 100644 index 00000000..cf3715cc --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStringsSpec.groovy @@ -0,0 +1,209 @@ +package de.uzl.its.swat.symbolic.invoke.java.lang + +import de.uzl.its.swat.symbolic.value.PlaceHolder +import de.uzl.its.swat.symbolic.value.Value +import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.ByteValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.LongValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.ShortValue +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue +import org.sosy_lab.common.ShutdownManager +import org.sosy_lab.common.configuration.Configuration +import org.sosy_lab.common.log.BasicLogManager +import org.sosy_lab.java_smt.SolverContextFactory +import org.sosy_lab.java_smt.api.BitvectorFormulaManager +import org.sosy_lab.java_smt.api.BooleanFormula +import org.sosy_lab.java_smt.api.BooleanFormulaManager +import org.sosy_lab.java_smt.api.FloatingPointFormulaManager +import org.sosy_lab.java_smt.api.FormulaType +import org.sosy_lab.java_smt.api.SolverContext +import org.sosy_lab.java_smt.api.StringFormulaManager +import spock.lang.Shared +import spock.lang.Specification + +/** + * Compares the number-to-string models with the JDK on edge values: every radix from 2 to 36 and + * radixes outside that range (which the JDK treats as 10). The number is a fresh variable fixed to + * the input, the radix a constant (a symbolic radix is pinned to a constant by choice branches, + * which need a running executor). The model must agree with the JDK in its concrete string and in + * every solution of its formula. + */ +class NumberStringsSpec extends Specification { + + @Shared SolverContext ctx + @Shared BitvectorFormulaManager bv + @Shared BooleanFormulaManager bm + @Shared FloatingPointFormulaManager fp + @Shared StringFormulaManager sm + @Shared int varCount = 0 + + static final List INTS = [0, -1, 1, Integer.MIN_VALUE, Integer.MAX_VALUE, Integer.MIN_VALUE + 1, + 9, 10, 35, 36, -36, 255, 256, 1295, 1296, 0x12345678, 0x87654321 as int, -1440] + static final List LONGS = [0L, -1L, 1L, Long.MIN_VALUE, Long.MAX_VALUE, Long.MIN_VALUE + 1, 35L, 36L, + 0xffffffffL, 0x100000000L, Integer.MIN_VALUE as long, 0x123456789abcdef0L, + 0xfedcba9876543210L, 47009447931686273L] + static final List RADIXES = (2..36) + [-1, 0, 1, 37, Integer.MIN_VALUE, Integer.MAX_VALUE] + static final List SHORTS = [0, -1, 1, Short.MIN_VALUE, Short.MAX_VALUE, 10, -10, 0x1234, -0x1234].collect { (short) it } + static final List BYTES = [0, -1, 1, Byte.MIN_VALUE, Byte.MAX_VALUE, 10, -10].collect { (byte) it } + + def setupSpec() { + ctx = SolverContextFactory.createSolverContext( + Configuration.defaultConfiguration(), + BasicLogManager.create(Configuration.defaultConfiguration()), + ShutdownManager.create().getNotifier(), + SolverContextFactory.Solvers.Z3) + bv = ctx.getFormulaManager().getBitvectorFormulaManager() + bm = ctx.getFormulaManager().getBooleanFormulaManager() + fp = ctx.getFormulaManager().getFloatingPointFormulaManager() + sm = ctx.getFormulaManager().getStringFormulaManager() + } + + def cleanupSpec() { + ctx.close() + } + + // A symbolic argument with the given value: a fresh variable, and the constraint fixing it. + List symbolic(Object v) { + String name = "n" + (varCount++) + switch (v) { + case Integer: + def x = bv.makeVariable(32, name) + return [new IntValue(ctx, v as int, x), bv.equal(x, bv.makeBitvector(32, v as long))] + case Long: + def x = bv.makeVariable(64, name) + return [new LongValue(ctx, v as long, x), bv.equal(x, bv.makeBitvector(64, v as long))] + case Short: + def x = bv.makeVariable(16, name) + return [new ShortValue(ctx, v as short, x), bv.equal(x, bv.makeBitvector(16, v as long))] + case Byte: + def x = bv.makeVariable(8, name) + return [new ByteValue(ctx, v as byte, x), bv.equal(x, bv.makeBitvector(8, v as long))] + } + throw new IllegalArgumentException(v.getClass().toString()) + } + + IntValue constant(int radix) { + new IntValue(ctx, radix, bv.makeBitvector(32, radix)) + } + + /** The mismatch of {@code res} with {@code expected}, or null: the concrete string and every solution. */ + String mismatch(Value res, String expected, List fixing) { + if (res == PlaceHolder.instance || !(res instanceof StringValue)) { + return "no model" + } + if (res.concrete != expected) { + return "concrete ${res.concrete} != ${expected}" + } + def prover = ctx.newProverEnvironment() + try { + fixing.each { prover.addConstraint(it) } + prover.addConstraint(bm.not(sm.equal(res.formula, sm.makeString(expected)))) + return prover.isUnsat() ? null : "formula admits a string other than ${expected}" + } finally { + prover.close() + } + } + + /** Runs {@code model(number, radix)} on all numbers and radixes and returns the mismatches. */ + List radixMismatches(List numbers, Closure model, Closure jdk) { + def errors = [] + for (def n : numbers) { + for (int r : RADIXES) { + def sym = symbolic(n) + def err = mismatch(model(sym[0], constant(r)), jdk(n, r), [sym[1]]) + if (err != null) errors << "${n}, radix ${r}: ${err}" + } + } + errors + } + + def "Integer.toString(int, int) agrees with the JDK"() { + expect: + radixMismatches(INTS, { x, r -> IntegerInvocation.invokeStaticMethod("toString", [x, r] as Value[], null) }, + { int x, int r -> Integer.toString(x, r) }) == [] + } + + def "Integer.toUnsignedString(int, int) agrees with the JDK"() { + expect: + radixMismatches(INTS, { x, r -> IntegerInvocation.invokeStaticMethod("toUnsignedString", [x, r] as Value[], null) }, + { int x, int r -> Integer.toUnsignedString(x, r) }) == [] + } + + def "Long.toString(long, int) agrees with the JDK"() { + expect: + radixMismatches(LONGS, { x, r -> LongInvocation.invokeStaticMethod("toString", [x, r] as Value[], null, null) }, + { long x, int r -> Long.toString(x, r) }) == [] + } + + def "Long.toUnsignedString(long, int) agrees with the JDK"() { + expect: + radixMismatches(LONGS, { x, r -> LongInvocation.invokeStaticMethod("toUnsignedString", [x, r] as Value[], null, null) }, + { long x, int r -> Long.toUnsignedString(x, r) }) == [] + } + + def "#type.#name agrees with the JDK"() { + expect: + values.findAll { v -> + def sym = symbolic(v) + mismatch(model(sym[0]), jdk(v), [sym[1]]) != null + } == [] + + where: + type | name | values | model | jdk + "Integer" | "toString" | INTS | { x -> IntegerInvocation.invokeStaticMethod("toString", [x] as Value[], null) } | { int x -> Integer.toString(x) } + "Integer" | "toUnsignedString" | INTS | { x -> IntegerInvocation.invokeStaticMethod("toUnsignedString", [x] as Value[], null) } | { int x -> Integer.toUnsignedString(x) } + "Integer" | "toBinaryString" | INTS | { x -> IntegerInvocation.invokeStaticMethod("toBinaryString", [x] as Value[], null) } | { int x -> Integer.toBinaryString(x) } + "Integer" | "toOctalString" | INTS | { x -> IntegerInvocation.invokeStaticMethod("toOctalString", [x] as Value[], null) } | { int x -> Integer.toOctalString(x) } + "Long" | "toString" | LONGS | { x -> LongInvocation.invokeStaticMethod("toString", [x] as Value[], null, null) } | { long x -> Long.toString(x) } + "Long" | "toUnsignedString" | LONGS | { x -> LongInvocation.invokeStaticMethod("toUnsignedString", [x] as Value[], null, null) }| { long x -> Long.toUnsignedString(x) } + "Long" | "toBinaryString" | LONGS | { x -> LongInvocation.invokeStaticMethod("toBinaryString", [x] as Value[], null, null) } | { long x -> Long.toBinaryString(x) } + "Long" | "toOctalString" | LONGS | { x -> LongInvocation.invokeStaticMethod("toOctalString", [x] as Value[], null, null) } | { long x -> Long.toOctalString(x) } + "Short" | "toString" | SHORTS | { x -> ShortInvocation.invokeStaticMethod("toString", [x] as Value[], null) } | { short x -> Short.toString(x) } + "Byte" | "toString" | BYTES | { x -> ByteInvocation.invokeStaticMethod("toString", [x] as Value[], null, null) } | { byte x -> Byte.toString(x) } + } + + def "the string of a #type in concatenation agrees with String.valueOf"() { + expect: + values.findAll { v -> + def sym = symbolic(v) + mismatch(sym[0].asStringValue(), String.valueOf(v), [sym[1]]) != null + } == [] + + where: + type | values + "int" | INTS + "long" | LONGS + "short" | SHORTS + } + + def "a concrete #type converts to the string of String.valueOf"() { + expect: + values.findAll { v -> + mismatch(value(v).asStringValue(), String.valueOf(v), []) != null + } == [] + + where: + type | values | value + "double" | [0.0d, -0.0d, 1.0d, 33.333d, 1e-109d, Double.MAX_VALUE, Double.NaN, Double.NEGATIVE_INFINITY] | { double d -> new DoubleValue(ctx, d, fp.makeNumber(d, FormulaType.getDoublePrecisionFloatingPointType())) } + "float" | [0.0f, -0.0f, 1.0f, 2.5f, 2.4012912E30f, Float.MIN_VALUE, Float.NaN, Float.POSITIVE_INFINITY] | { float f -> new FloatValue(ctx, f, fp.makeNumber(f, FormulaType.getSinglePrecisionFloatingPointType())) } + } + + def "a radix outside 2 to 36 means 10"() { + expect: + NumberStrings.normaliseRadix(radix) == expected + + where: + radix | expected + Integer.MIN_VALUE | 10 + -1 | 10 + 0 | 10 + 1 | 10 + 2 | 2 + 10 | 10 + 36 | 36 + 37 | 10 + Integer.MAX_VALUE | 10 + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/RadixChoiceAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/RadixChoiceAgentSpec.groovy new file mode 100644 index 00000000..6c4705c7 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/RadixChoiceAgentSpec.groovy @@ -0,0 +1,85 @@ +package de.uzl.its.swat.symbolic.invoke.java.lang + +import com.fasterxml.jackson.databind.ObjectMapper +import spock.lang.Specification + +import javax.tools.ToolProvider +import java.nio.file.Files +import java.nio.file.Path +import java.util.concurrent.TimeUnit + +/** + * L2 (forked agent): a conversion with a symbolic radix branches on the radix (a binary search over + * 2 to 36 after the JDK's fallback to 10), so that the conversion is exact with a constant radix + * and the explorer reaches the other radixes by flipping the branches. Runs via the {@code + * agentTest} Gradle task (needs the agent jar from {@code copyJar}). + */ +class RadixChoiceAgentSpec extends Specification { + + static final Path AGENT_JAR = Path.of("lib", "symbolic-executor.jar").toAbsolutePath() + static final Path NATIVE_LIBS = Path.of("..", "libs", "java-library-path").toAbsolutePath() + static final Path TARGETS = Path.of("src", "test", "resources", "targets").toAbsolutePath() + + def "radix #radix is searched in #steps.size() steps, as its concrete value says"() { + given: + def classes = Files.createTempDirectory("swat-radix-spec") + compile(classes) + + when: + def trace = parseTrace(run(classes, ["-Dswat.input.I_0=-1295", "-Dswat.input.I_1=" + radix])) + def choices = trace.trace.findAll { it.choice } + + then: "binary search over [2, 37): the branch radix < mid of each step" + choices*.branched == steps + choices*.key.collect { it.substring(it.indexOf('#')) } == (0.. inputs) { + def java = Path.of(System.getProperty("java.home"), "bin", "java").toString() + def cmd = [java, + "-javaagent:${AGENT_JAR}".toString(), + "-Djava.library.path=${NATIVE_LIBS}".toString(), + "-Dconfig.path=/nonexistent/swat.cfg", + "-Dinstrumentation.transformer=SV_COMP", + "-Dsolver.mode=PRINT", + "-DexitOnError=false", + "-DlogShadowStateToConsole=false"] + inputs + + ["-cp", classes.toString(), "-ea", "Main"] + def proc = new ProcessBuilder(cmd).directory(classes.toFile()).redirectErrorStream(true).start() + def out = proc.inputStream.text + assert proc.waitFor(5, TimeUnit.MINUTES): "target did not finish:\n${out}" + return out + } + + /** The TraceDTO is the single pretty-printed JSON object whose braces start at column 0. */ + private static Map parseTrace(String out) { + int start = out.indexOf("\n{\n") + int end = out.indexOf("\n}\n", start) + assert start >= 0 && end > start: "no trace JSON in output:\n${out}" + return new ObjectMapper().readValue(out.substring(start + 1, end + 2), Map) + } +} diff --git a/symbolic-executor/src/test/resources/targets/radix/Main.java b/symbolic-executor/src/test/resources/targets/radix/Main.java new file mode 100644 index 00000000..f6dfe50e --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/radix/Main.java @@ -0,0 +1,13 @@ +import org.sosy_lab.sv_benchmarks.Verifier; + +/** Integer.toString(int, int) with a symbolic number and a symbolic radix (see RadixChoiceAgentSpec). */ +public class Main { + public static void main(String[] args) { + int x = Verifier.nondetInt(); + int radix = Verifier.nondetInt(); + String s = Integer.toString(x, radix); + if (s.equals("-zz")) { + System.out.println("found"); + } + } +}