Model number-to-string conversions with a radix, fix toBinaryString divergence

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)),

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);
     }
 
     /**

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);
     }
 
     /**