Make more general interval_constraint function in util.

It is undesirable to have dependencies on the string solver, so
char_printable_constraintss has been moved into util and made more general.

Author: jeannielynnmoulton

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_functions.h>
-#include <solvers/strings/string_constraint_generator.h>
+#include <util/interval_constraint.h>
 
 #include "generic_parameter_specialization_map_keys.h"
 #include "java_root_class.h"
@@ -304,10 +304,19 @@ class recursion_set_entryt
   }
 };
 
-/// A range of the form [low_char]-[high-char] that represents the set of
-/// printable characters for the string-printable option. The printable
-/// characters are in the range U+0020-U+007E, i.e. ' ' to '~'
-const char printable_char_range[] = " -~";
+/// 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.
 ///
@@ -425,7 +434,7 @@ void initialize_nondet_string_fields(
     add_character_set_constraint(
       array_pointer,
       length_expr,
-      printable_char_range,
+      integer_interval_to_string(printable_char_range),
       symbol_table,
       loc,
       function_id,
@@ -1054,7 +1063,7 @@ void java_object_factoryt::gen_nondet_init(
     if(type == java_char_type() && object_factory_parameters.string_printable)
     {
       assignments.add(
-        code_assumet(char_range_constraints(expr, printable_char_range)));
+        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_string_library_preprocess.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.h

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

src/solvers/strings/string_constraint_generator.h

@@ -111,11 +111,6 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix(
   const namespacet &ns,
   array_poolt &array_pool);
 
-/// Given an exprt and a string representing a character range of the form
-/// [low_char]-[high_char], return an and_exprt that represents restricting
-/// the selection of the character to the range.
-exprt char_range_constraints(const exprt &expr, const std::string &char_range);
-
 string_constraintst add_constraint_on_characters(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &s,

src/solvers/strings/string_constraint_generator_main.cpp

@@ -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)
@@ -114,23 +115,6 @@ void merge(string_constraintst &result, string_constraintst other)
     std::back_inserter(result.not_contains));
 }
 
-exprt char_range_constraints(const exprt &expr, const std::string &char_range)
-{
-  // Parse char_set
-  PRECONDITION(char_range.length() == 3);
-  PRECONDITION(char_range[1] == '-');
-  const char &low_char = char_range[0];
-  const char &high_char = char_range[2];
-  INVARIANT(
-    low_char <= high_char,
-    "The lower character must be smaller or equal to the high character.");
-
-  // expr >= low_char && expr <= high_char
-  return and_exprt(
-    binary_relation_exprt(expr, ID_ge, from_integer(low_char, expr.type())),
-    binary_relation_exprt(expr, ID_le, from_integer(high_char, expr.type())));
-}
-
 /// Add constraint on characters of a string.
 ///
 /// This constraint is
@@ -153,14 +137,19 @@ string_constraintst add_constraint_on_characters(
   const std::string &char_set,
   array_poolt &array_pool)
 {
+  // Parse char_set
+  PRECONDITION(char_set.length() == 3);
+  PRECONDITION(char_set[1] == '-');
+  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 string_constraintt sc(
     qvar,
     zero_if_negative(start),
     zero_if_negative(end),
-    char_range_constraints(chr, char_set));
+    interval_constraint(chr, char_range));
   return {{}, {sc}, {}};
 }
 

src/util/Makefile

@@ -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/interval_constraint.cpp

@@ -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.h

@@ -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

unit/Makefile

@@ -50,7 +50,6 @@ SRC += analyses/ai/ai.cpp \
        solvers/prop/bdd_expr.cpp \
        solvers/sat/satcheck_minisat2.cpp \
        solvers/strings/array_pool/array_pool.cpp \
-       solvers/strings/string_constraint_generator_main/char_range_constraints.cpp \
        solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
        solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp \
@@ -69,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/solvers/strings/string_constraint_generator_main/char_range_constraints.cpp

@@ -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");
+      }
+    }
+  }
+}