Merge pull request #4868 from jeannielynnmoulton/jeannie/CharacterPrintable

--string-printable option also forces chars to be printable

Author: jeannielynnmoulton

jbmc/regression/strings-smoke-tests/java_string_printable/Test.class

@@ -18,4 +18,39 @@ public static boolean check_char(String s, char c) {
         assert(b);
         return b;
     }
+
+    public static boolean printable_char(char c) {
+      boolean b = c >= ' ' && c <= '~';
+      assert(b);
+      return b;
+    }
+
+    public char charField;
+
+    public boolean test_char_field() {
+      boolean b = charField >= ' ' && charField <= '~';
+      assert(b);
+      return b;
+    }
+
+    public static boolean printable_char_array(char[] c) {
+      if(c.length != 3 || c == null)
+        return false;
+      boolean b0 = c[0] >= ' ' && c[0] <= '~';
+      boolean b1 = c[1] >= ' ' && c[1] <= '~';
+      boolean b2 = c[2] >= ' ' && c[2] <= '~';
+      assert(b0 || b1 || b2);
+      return b0 || b1 || b2;
+    }
+
+    public static char charStaticField = 'a';
+
+     public boolean test_char_field_static() {
+      if(charStaticField == 'a')
+        return false;
+      boolean b = charStaticField >= ' ' && charStaticField <= '~';
+      assert(b);
+      return b;
+    }
+
 }

jbmc/regression/strings-smoke-tests/java_string_printable/Test.java

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--function Test.check_char --max-nondet-string-length 100
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+Shows that the assertion can be violated when string-printable is not enabled

jbmc/regression/strings-smoke-tests/java_string_printable/test_nonprintable_char.desc

@@ -0,0 +1,11 @@
+FUTURE
+Test.class
+--function Test.printable_char_array --max-nondet-string-length 100
+assertion.* file Test.java line 42 .* FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+Shows that the assertion can be violated when string-printable is not enabled
+for character arrays
+
+The constraint has not been implemented for char arrays.

jbmc/regression/strings-smoke-tests/java_string_printable/test_nonprintable_char_array.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.test_char_field --max-nondet-string-length 100
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+Shows that the assertion can be violated when string-printable is not enabled
+for character field

jbmc/regression/strings-smoke-tests/java_string_printable/test_nonprintable_char_field.desc

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.test_char_field_static --max-nondet-string-length 100 --nondet-static
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+Shows that the assertion can be violated when string-printable is not enabled
+for character static field

jbmc/regression/strings-smoke-tests/java_string_printable/test_nonprintable_char_field_static.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--function Test.check_char --max-nondet-string-length 100 --string-printable
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+Shows that the assertion cannot be violated when string-printable is enabled

jbmc/regression/strings-smoke-tests/java_string_printable/test_printable_char.desc

@@ -0,0 +1,12 @@
+FUTURE
+Test.class
+--function Test.printable_char_array --max-nondet-string-length 100 --string-printable
+^EXIT=10$
+^SIGNAL=0$
+--
+assertion.* file Test.java line 42 .* FAILURE
+--
+Shows that the assertion can be violated when string-printable is not enabled
+for character arrays
+
+The constraint has not been implemented for char arrays.

jbmc/regression/strings-smoke-tests/java_string_printable/test_printable_char_array.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.test_char_field --max-nondet-string-length 100 --string-printable
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+Shows that the assertion cannot be violated when string-printable is enabled for
+character field

jbmc/regression/strings-smoke-tests/java_string_printable/test_printable_char_field.desc

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.test_char_field_static --max-nondet-string-length 100 --string-printable --nondet-static
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+Shows that the assertion cannot be violated when string-printable is enabled for
+character static field

jbmc/regression/strings-smoke-tests/java_string_printable/test_printable_char_field_static.desc

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_functions.h>
+#include <util/interval_constraint.h>
 
 #include "generic_parameter_specialization_map_keys.h"
 #include "java_root_class.h"
@@ -303,6 +304,20 @@ class recursion_set_entryt
   }
 };
 
+/// Interval that represents the printable character range
+/// range U+0020-U+007E, i.e. ' ' to '~'
+const integer_intervalt printable_char_range(' ', '~');
+
+/// Converts and \ref integer_intervalt to a a string of the for [lower]-[upper]
+static irep_idt integer_interval_to_string(const integer_intervalt &interval)
+{
+  std::string result;
+  result += numeric_cast_v<char>(interval.lower);
+  result += "-";
+  result += numeric_cast_v<char>(interval.upper);
+  return result;
+}
+
 /// Initialise length and data fields for a nondeterministic String structure.
 ///
 /// If the structure is not a nondeterministic structure, the call results in
@@ -417,7 +432,13 @@ void initialize_nondet_string_fields(
   if(printable)
   {
     add_character_set_constraint(
-      array_pointer, length_expr, " -~", symbol_table, loc, function_id, code);
+      array_pointer,
+      length_expr,
+      integer_interval_to_string(printable_char_range),
+      symbol_table,
+      loc,
+      function_id,
+      code);
   }
 }
 
@@ -1039,6 +1060,11 @@ void java_object_factoryt::gen_nondet_init(
     assign.add_source_location() = location;
 
     assignments.add(assign);
+    if(type == java_char_type() && object_factory_parameters.string_printable)
+    {
+      assignments.add(
+        code_assumet(interval_constraint(expr, printable_char_range)));
+    }
     // add assumes to obey numerical restrictions
     if(type != java_boolean_type() && type != java_char_type())
     {

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -669,7 +669,7 @@ void add_array_to_length_association(
 /// belong to the character set.
 /// \param pointer: a character pointer expression
 /// \param length: length of the character sequence pointed by `pointer`
-/// \param char_set: character set given by a range expression consisting of
+/// \param char_range: character set given by a range expression consisting of
 ///   two characters separated by an hyphen. For instance "a-z" denotes all
 ///   lower case ascii letters.
 /// \param symbol_table: the symbol table
@@ -679,7 +679,7 @@ void add_array_to_length_association(
 void add_character_set_constraint(
   const exprt &pointer,
   const exprt &length,
-  const irep_idt &char_set,
+  const irep_idt &char_range,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
   const irep_idt &function_id,
@@ -690,7 +690,7 @@ void add_character_set_constraint(
     java_int_type(), "cnstr_added", loc, function_id, symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
-  const constant_exprt char_set_expr(char_set, string_typet());
+  const constant_exprt char_set_expr(char_range, string_typet());
   code.add(
     code_assign_function_application(
       return_expr,

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -334,7 +334,7 @@ void add_array_to_length_association(
 void add_character_set_constraint(
   const exprt &pointer,
   const exprt &length,
-  const irep_idt &char_set,
+  const irep_idt &char_range,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
   const irep_idt &function_id,

jbmc/src/java_bytecode/java_string_library_preprocess.h

@@ -9,4 +9,5 @@ langapi # should go away
 library
 linking
 miniz
+solvers/strings
 util

jbmc/src/java_bytecode/module_dependencies.txt

@@ -29,6 +29,7 @@ Author: Romain Brenguier, [email protected]
 #include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 #include <util/string_constant.h>
+#include <util/interval_constraint.h>
 
 string_constraint_generatort::string_constraint_generatort(const namespacet &ns)
   : array_pool(fresh_symbol), ns(ns)
@@ -139,17 +140,16 @@ string_constraintst add_constraint_on_characters(
   // Parse char_set
   PRECONDITION(char_set.length() == 3);
   PRECONDITION(char_set[1] == '-');
-  const char &low_char = char_set[0];
-  const char &high_char = char_set[2];
+  const integer_intervalt char_range(char_set[0], char_set[2]);
 
   // Add constraint
   const symbol_exprt qvar = fresh_symbol("char_constr", s.length_type());
   const exprt chr = s[qvar];
-  const and_exprt char_in_set(
-    binary_relation_exprt(chr, ID_ge, from_integer(low_char, chr.type())),
-    binary_relation_exprt(chr, ID_le, from_integer(high_char, chr.type())));
   const string_constraintt sc(
-    qvar, zero_if_negative(start), zero_if_negative(end), char_in_set);
+    qvar,
+    zero_if_negative(start),
+    zero_if_negative(end),
+    interval_constraint(chr, char_range));
   return {{}, {sc}, {}};
 }
 

src/solvers/strings/string_constraint_generator_main.cpp

@@ -41,7 +41,7 @@ Author: Alberto Griggio, [email protected]
 
 #define HELP_STRING_REFINEMENT \
   " --no-refine-strings          turn off string refinement\n" \
-  " --string-printable           restrict to printable strings (experimental)\n" /* NOLINT(*) */ \
+  " --string-printable           restrict to printable strings and characters\n" /* NOLINT(*) */ \
   " --string-non-empty           restrict to non-empty strings (experimental)\n" /* NOLINT(*) */ \
   " --string-input-value st      restrict non-null strings to a fixed value st;\n" /* NOLINT(*) */ \
   "                              the switch can be used multiple times to give\n" /* NOLINT(*) */ \

src/solvers/strings/string_refinement.h

@@ -34,6 +34,7 @@ SRC = allocate_objects.cpp \
       irep_hash_container.cpp \
       irep_ids.cpp \
       irep_serialization.cpp \
+      interval_constraint.cpp \
       invariant_utils.cpp \
       json.cpp \
       json_irep.cpp \

src/util/Makefile

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Interval constraint
+
+Author: Jeannie Moulton
+
+\*******************************************************************/
+
+#include "interval_constraint.h"
+#include "arith_tools.h"
+
+exprt interval_constraint(const exprt &expr, const integer_intervalt &interval)
+{
+  // expr >= lower_bound && expr <= upper_bound
+  return and_exprt(
+    binary_relation_exprt(
+      expr, ID_ge, from_integer(interval.lower, expr.type())),
+    binary_relation_exprt(
+      expr, ID_le, from_integer(interval.upper, expr.type())));
+}

src/util/interval_constraint.cpp

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Interval constraint
+
+Author: Jeannie Moulton
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_INTERVAL_CONSTRAINT_H
+#define CPROVER_UTIL_INTERVAL_CONSTRAINT_H
+
+#include "integer_interval.h"
+
+class exprt;
+
+/// Given an exprt and an integer interval return an exprt that represents
+/// restricting the expression to the range in the interval (inclusive).
+exprt interval_constraint(const exprt &expr, const integer_intervalt &interval);
+
+#endif // CPROVER_UTIL_INTERVAL_CONSTRAINT_H

src/util/interval_constraint.h

@@ -68,6 +68,7 @@ SRC += analyses/ai/ai.cpp \
        util/format_number_range.cpp \
        util/get_base_name.cpp \
        util/graph.cpp \
+       util/interval_constraint.cpp \
        util/irep.cpp \
        util/irep_sharing.cpp \
        util/json_array.cpp \

unit/Makefile

@@ -0,0 +1,80 @@
+/*******************************************************************\
+
+Module: Unit tests for interval_constraint in
+        util/interval_constraint.cpp
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <testing-utils/use_catch.h>
+
+#include <util/interval_constraint.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+
+SCENARIO(
+  "interval_constraint with characters",
+  "[core][util][interval_constraint]")
+{
+  GIVEN("A string representing a character range and an character expression")
+  {
+    const integer_intervalt char_range('a', 'z');
+    const exprt expr{"dummy", unsignedbv_typet(16)};
+
+    WHEN("interval_constraint is called")
+    {
+      const auto result = interval_constraint(expr, char_range);
+
+      THEN(
+        "expect that the result is an and_exprt with two inequality "
+        "expressions representing a <= expr && expr <= z")
+      {
+        REQUIRE(can_cast_expr<and_exprt>(result));
+
+        REQUIRE(result.op0().id() == ID_ge);
+        REQUIRE(result.op0().op0().type() == unsignedbv_typet(16));
+        REQUIRE(can_cast_expr<constant_exprt>(result.op0().op1()));
+        REQUIRE(to_constant_expr(result.op0().op1()).get_value() == "61"); // a
+
+        REQUIRE(result.op1().id() == ID_le);
+        REQUIRE(result.op1().op0().type() == unsignedbv_typet(16));
+        REQUIRE(can_cast_expr<constant_exprt>(result.op1().op1()));
+        REQUIRE(to_constant_expr(result.op1().op1()).get_value() == "7A"); // b
+      }
+    }
+  }
+}
+
+SCENARIO(
+  "interval_constraint with integers",
+  "[core][util][interval_constraint]")
+{
+  GIVEN("A string representing a int range and an int expression")
+  {
+    const integer_intervalt int_range(6, 9);
+    const exprt expr{"dummy", unsignedbv_typet(32)};
+
+    WHEN("interval_constraint is called")
+    {
+      const auto result = interval_constraint(expr, int_range);
+
+      THEN(
+        "expect that the result is an and_exprt with two inequality "
+        "expressions representing 6 <= expr && expr <= 9")
+      {
+        REQUIRE(can_cast_expr<and_exprt>(result));
+
+        REQUIRE(result.op0().id() == ID_ge);
+        REQUIRE(result.op0().op0().type() == unsignedbv_typet(32));
+        REQUIRE(can_cast_expr<constant_exprt>(result.op0().op1()));
+        REQUIRE(to_constant_expr(result.op0().op1()).get_value() == "6");
+
+        REQUIRE(result.op1().id() == ID_le);
+        REQUIRE(result.op1().op0().type() == unsignedbv_typet(32));
+        REQUIRE(can_cast_expr<constant_exprt>(result.op1().op1()));
+        REQUIRE(to_constant_expr(result.op1().op1()).get_value() == "9");
+      }
+    }
+  }
+}