Create is_digit_with_radix()

Produces an expression which checks if a character is a valid digit
with respect to a particular radix. Includes a unit test.

Author: Owen Jones

src/solvers/refinement/string_constraint_generator.h

@@ -328,4 +328,6 @@ class string_constraint_generatort
   bool is_constant_string(const string_exprt &expr) const;
 };
 
+exprt is_digit_with_radix(exprt chr, exprt radix);
+
 #endif

src/solvers/refinement/string_constraint_generator_valueof.cpp

@@ -490,3 +490,41 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
   }
   return i;
 }
+
+/// Check if a character is a digit with respect to the given radix, e.g. if the
+/// radix is 10 then check if the character is in the range 0-9.
+/// \param chr: the character
+/// \param radix:  the radix
+/// \return an expression for the condition
+exprt is_digit_with_radix(exprt chr, exprt radix)
+{
+  const typet &char_type=chr.type();
+  exprt zero_char=from_integer('0', char_type);
+  exprt nine_char=from_integer('9', char_type);
+  exprt a_char=from_integer('a', char_type);
+  exprt A_char=from_integer('A', char_type);
+
+  and_exprt is_digit_when_radix_le_10(
+    binary_relation_exprt(chr, ID_ge, zero_char),
+    binary_relation_exprt(
+      chr, ID_lt, plus_exprt(zero_char, typecast_exprt(radix, char_type))));
+
+  minus_exprt radix_minus_ten(
+    typecast_exprt(radix, char_type), from_integer(10, char_type));
+
+  or_exprt is_digit_when_radix_gt_10(
+    and_exprt(
+      binary_relation_exprt(chr, ID_ge, zero_char),
+      binary_relation_exprt(chr, ID_le, nine_char)),
+    and_exprt(
+      binary_relation_exprt(chr, ID_ge, a_char),
+      binary_relation_exprt(chr, ID_lt, plus_exprt(a_char, radix_minus_ten))),
+    and_exprt(
+      binary_relation_exprt(chr, ID_ge, A_char),
+      binary_relation_exprt(chr, ID_lt, plus_exprt(A_char, radix_minus_ten))));
+
+  return if_exprt(
+    binary_relation_exprt(radix, ID_le, from_integer(10, radix.type())),
+    is_digit_when_radix_le_10,
+    is_digit_when_radix_gt_10);
+}

unit/Makefile

@@ -2,6 +2,7 @@
 
 SRC = unit_tests.cpp \
       catch_example.cpp \
+      solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \
       # Empty last line
 
 INCLUDES= -I ../src/ -I.
@@ -16,14 +17,15 @@ LIBS += ../src/ansi-c/ansi-c$(LIBEXT) \
         ../src/cpp/cpp$(LIBEXT) \
         ../src/json/json$(LIBEXT) \
         ../src/linking/linking$(LIBEXT) \
-        ../src/util/util$(LIBEXT) \
-        ../src/big-int/big-int$(LIBEXT) \
         ../src/goto-programs/goto-programs$(LIBEXT) \
         ../src/pointer-analysis/pointer-analysis$(LIBEXT) \
         ../src/langapi/langapi$(LIBEXT) \
         ../src/assembler/assembler$(LIBEXT) \
         ../src/analyses/analyses$(LIBEXT) \
         ../src/solvers/solvers$(LIBEXT) \
+        ../src/java_bytecode/java_bytecode$(LIBEXT) \
+        ../src/util/util$(LIBEXT) \
+        ../src/big-int/big-int$(LIBEXT) \
         # Empty last line
 
 TESTS = unit_tests$(EXEEXT) \

unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp

@@ -0,0 +1,74 @@
+/*******************************************************************\
+
+ Module: Unit tests for is_digit_with_radix in
+   solvers/refinement/string_constraint_generator_valueof.cpp
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <catch.hpp>
+
+#include <solvers/refinement/string_constraint_generator.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+#include <util/simplify_expr.h>
+#include <util/std_types.h>
+
+SCENARIO("is_digit_with_radix",
+  "[core][solvers][refinement][string_constraint_generator_valueof]")
+{
+  typet char_type=unsignedbv_typet(16);
+  typet int_type=signedbv_typet(32);
+  symbol_tablet symtab;
+  namespacet ns(symtab);
+
+  WHEN("Radix 10")
+  {
+    int radix=10;
+    REQUIRE(true_exprt()==simplify_expr(
+      is_digit_with_radix(
+        from_integer('0', char_type),
+        from_integer(radix, int_type)), ns));
+    REQUIRE(true_exprt()==simplify_expr(
+      is_digit_with_radix(
+        from_integer('9', char_type),
+        from_integer(radix, int_type)), ns));
+    REQUIRE(false_exprt()==simplify_expr(
+      is_digit_with_radix(
+        from_integer('a', char_type),
+        from_integer(radix, int_type)), ns));
+  }
+  WHEN("Radix 8")
+  {
+    int radix=8;
+    REQUIRE(true_exprt()==simplify_expr(
+      is_digit_with_radix(
+        from_integer('7', char_type),
+        from_integer(radix, int_type)), ns));
+    REQUIRE(false_exprt()==simplify_expr(
+      is_digit_with_radix(
+        from_integer('8', char_type),
+        from_integer(radix, int_type)), ns));
+  }
+  WHEN("Radix 16")
+  {
+    int radix=16;
+    REQUIRE(true_exprt()==simplify_expr(
+      is_digit_with_radix(
+        from_integer('a', char_type),
+        from_integer(radix, int_type)), ns));
+    REQUIRE(true_exprt()==simplify_expr(
+      is_digit_with_radix(
+        from_integer('A', char_type),
+        from_integer(radix, int_type)), ns));
+    REQUIRE(true_exprt()==simplify_expr(
+      is_digit_with_radix(
+        from_integer('f', char_type),
+        from_integer(radix, int_type)), ns));
+    REQUIRE(false_exprt()==simplify_expr(
+      is_digit_with_radix(
+        from_integer('g', char_type),
+        from_integer(radix, int_type)), ns));
+  }
+}