Merge pull request #549 from romainbrenguier/string-refinement-dependencies

Cleaning dependencies of the string solver

Author: kroening

src/solvers/refinement/refined_string_type.cpp

@@ -10,10 +10,10 @@ Author: Romain Brenguier, [email protected]
 
 \*******************************************************************/
 
-#include <solvers/refinement/refined_string_type.h>
-#include <ansi-c/string_constant.h>
 #include <util/cprover_prefix.h>
 
+#include "refined_string_type.h"
+
 /*******************************************************************\
 
 Constructor: refined_string_typet::refined_string_typet
@@ -22,11 +22,12 @@ Constructor: refined_string_typet::refined_string_typet
 
 \*******************************************************************/
 
-refined_string_typet::refined_string_typet(typet char_type)
+refined_string_typet::refined_string_typet(
+  const typet &index_type, const typet &char_type)
 {
-  infinity_exprt infinite_index(refined_string_typet::index_type());
+  infinity_exprt infinite_index(index_type);
   array_typet char_array(char_type, infinite_index);
-  components().emplace_back("length", refined_string_typet::index_type());
+  components().emplace_back("length", index_type);
   components().emplace_back("content", char_array);
 }
 

src/solvers/refinement/refined_string_type.h

@@ -17,14 +17,12 @@ Author: Romain Brenguier, [email protected]
 #include <util/std_expr.h>
 #include <util/arith_tools.h>
 #include <util/expr_util.h>
-#include <ansi-c/c_types.h>
-#include <java_bytecode/java_types.h>
 
 // Internal type used for string refinement
 class refined_string_typet: public struct_typet
 {
 public:
-  explicit refined_string_typet(typet char_type);
+  refined_string_typet(const typet &index_type, const typet &char_type);
 
   // Type for the content (list of characters) of a string
   const array_typet &get_content_type() const
@@ -33,7 +31,7 @@ class refined_string_typet: public struct_typet
     return to_array_type(components()[1].type());
   }
 
-  const typet &get_char_type()
+  const typet &get_char_type() const
   {
     assert(components().size()==2);
     return components()[0].type();
@@ -44,16 +42,6 @@ class refined_string_typet: public struct_typet
     return get_content_type().size().type();
   }
 
-  static typet index_type()
-  {
-    return signed_int_type();
-  }
-
-  static typet java_index_type()
-  {
-    return java_int_type();
-  }
-
   // For C the unrefined string type is __CPROVER_string, for java it is a
   // pointer to a struct with tag java.lang.String
 
@@ -67,22 +55,6 @@ class refined_string_typet: public struct_typet
 
   static bool is_java_char_sequence_type(const typet &type);
 
-  static typet get_char_type(const exprt &expr)
-  {
-    if(is_c_string_type(expr.type()))
-      return char_type();
-    else
-      return java_char_type();
-  }
-
-  static typet get_index_type(const exprt &expr)
-  {
-    if(is_c_string_type(expr.type()))
-      return index_type();
-    else
-      return java_index_type();
-  }
-
   static bool is_unrefined_string_type(const typet &type)
   {
     return (

src/solvers/refinement/string_constraint.h

@@ -111,16 +111,16 @@ class string_not_contains_constraintt: public exprt
 {
 public:
   // string_not contains_constraintt are formula of the form:
-  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
+  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s0[x+y] != s1[y]
 
   string_not_contains_constraintt(
     exprt univ_lower_bound,
     exprt univ_bound_sup,
     exprt premise,
     exprt exists_bound_inf,
     exprt exists_bound_sup,
-    exprt s0,
-    exprt s1) :
+    const string_exprt &s0,
+    const string_exprt &s1):
   exprt(ID_string_not_contains_constraint)
   {
     copy_to_operands(univ_lower_bound, univ_bound_sup, premise);
@@ -153,14 +153,14 @@ class string_not_contains_constraintt: public exprt
     return operands()[4];
   }
 
-  const exprt &s0() const
+  const string_exprt &s0() const
   {
-    return operands()[5];
+    return to_string_expr(operands()[5]);
   }
 
-  const exprt &s1() const
+  const string_exprt &s1() const
   {
-    return operands()[6];
+    return to_string_expr(operands()[6]);
   }
 };
 

src/solvers/refinement/string_constraint_generator.h

@@ -13,9 +13,8 @@ Author: Romain Brenguier, [email protected]
 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
 
-#include <ansi-c/c_types.h>
+#include <util/string_expr.h>
 #include <solvers/refinement/refined_string_type.h>
-#include <solvers/refinement/string_expr.h>
 #include <solvers/refinement/string_constraint.h>
 
 class string_constraint_generatort
@@ -26,33 +25,18 @@ class string_constraint_generatort
   // to the axiom list.
 
   string_constraint_generatort():
-    mode(ID_unknown), refined_string_type(char_type())
+    mode(ID_unknown)
   { }
 
   void set_mode(irep_idt _mode)
   {
     // only C and java modes supported
     assert((_mode==ID_java) || (_mode==ID_C));
     mode=_mode;
-    refined_string_type=refined_string_typet(get_char_type());
   }
 
   irep_idt &get_mode() { return mode; }
 
-  typet get_char_type() const;
-  typet get_index_type() const
-  {
-    if(mode==ID_java)
-      return refined_string_typet::java_index_type();
-    assert(mode==ID_C);
-    return refined_string_typet::index_type();
-  }
-
-  const refined_string_typet &get_refined_string_type() const
-  {
-    return refined_string_type;
-  }
-
   // Axioms are of three kinds: universally quantified string constraint,
   // not contains string constraints and simple formulas.
   std::list<exprt> axioms;
@@ -73,9 +57,14 @@ class string_constraint_generatort
     return index_exprt(witness.at(c), univ_val);
   }
 
-  symbol_exprt fresh_exist_index(const irep_idt &prefix);
-  symbol_exprt fresh_univ_index(const irep_idt &prefix);
+  static unsigned next_symbol_id;
+
+  static symbol_exprt fresh_symbol(
+    const irep_idt &prefix, const typet &type=bool_typet());
+  symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type);
+  symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type);
   symbol_exprt fresh_boolean(const irep_idt &prefix);
+  string_exprt fresh_string(const refined_string_typet &type);
 
   // We maintain a map from symbols to strings.
   std::map<irep_idt, string_exprt> symbol_to_string;
@@ -95,7 +84,7 @@ class string_constraint_generatort
   exprt add_axioms_for_function_application(
     const function_application_exprt &expr);
 
-  constant_exprt constant_char(int i) const;
+  static constant_exprt constant_char(int i, const typet &char_type);
 
 private:
   // The integer with the longest string is Integer.MIN_VALUE which is -2^31,
@@ -107,7 +96,7 @@ class string_constraint_generatort
   const std::size_t MAX_FLOAT_LENGTH=15;
   const std::size_t MAX_DOUBLE_LENGTH=30;
 
-  irep_idt extract_java_string(const symbol_exprt &s) const;
+  static irep_idt extract_java_string(const symbol_exprt &s);
 
   exprt axiom_for_is_positive_index(const exprt &x);
 
@@ -123,7 +112,6 @@ class string_constraint_generatort
   exprt add_axioms_for_contains(const function_application_exprt &f);
   exprt add_axioms_for_equals(const function_application_exprt &f);
   exprt add_axioms_for_equals_ignore_case(const function_application_exprt &f);
-  exprt add_axioms_for_data(const function_application_exprt &f);
 
   // Add axioms corresponding to the String.hashCode java function
   // The specification is partial: the actual value is not actually computed
@@ -153,7 +141,8 @@ class string_constraint_generatort
   string_exprt add_axioms_for_concat_float(const function_application_exprt &f);
   string_exprt add_axioms_for_concat_code_point(
     const function_application_exprt &f);
-  string_exprt add_axioms_for_constant(irep_idt sval);
+  string_exprt add_axioms_for_constant(
+    irep_idt sval, const refined_string_typet &ref_type);
   string_exprt add_axioms_for_delete(
     const string_exprt &str, const exprt &start, const exprt &end);
   string_exprt add_axioms_for_delete(const function_application_exprt &expr);
@@ -173,15 +162,19 @@ class string_constraint_generatort
     const function_application_exprt &f);
   string_exprt add_axioms_from_literal(const function_application_exprt &f);
   string_exprt add_axioms_from_int(const function_application_exprt &f);
-  string_exprt add_axioms_from_int(const exprt &i, size_t max_size);
-  string_exprt add_axioms_from_int_hex(const exprt &i);
+  string_exprt add_axioms_from_int(
+    const exprt &i, size_t max_size, const refined_string_typet &ref_type);
+  string_exprt add_axioms_from_int_hex(
+    const exprt &i, const refined_string_typet &ref_type);
   string_exprt add_axioms_from_int_hex(const function_application_exprt &f);
   string_exprt add_axioms_from_long(const function_application_exprt &f);
   string_exprt add_axioms_from_long(const exprt &i, size_t max_size);
   string_exprt add_axioms_from_bool(const function_application_exprt &f);
-  string_exprt add_axioms_from_bool(const exprt &i);
+  string_exprt add_axioms_from_bool(
+    const exprt &i, const refined_string_typet &ref_type);
   string_exprt add_axioms_from_char(const function_application_exprt &f);
-  string_exprt add_axioms_from_char(const exprt &i);
+  string_exprt add_axioms_from_char(
+    const exprt &i, const refined_string_typet &ref_type);
   string_exprt add_axioms_from_char_array(const function_application_exprt &f);
   string_exprt add_axioms_from_char_array(
     const exprt &length,
@@ -257,7 +250,8 @@ class string_constraint_generatort
   // TODO: not working correctly at the moment
   string_exprt add_axioms_for_value_of(const function_application_exprt &f);
 
-  string_exprt add_axioms_for_code_point(const exprt &code_point);
+  string_exprt add_axioms_for_code_point(
+    const exprt &code_point, const refined_string_typet &ref_type);
   string_exprt add_axioms_for_java_char_array(const exprt &char_array);
   string_exprt add_axioms_for_if(const if_exprt &expr);
   exprt add_axioms_for_char_literal(const function_application_exprt &f);
@@ -287,9 +281,6 @@ class string_constraint_generatort
   // Tells which language is used. C and Java are supported
   irep_idt mode;
 
-  // Type of strings used in the refinement
-  refined_string_typet refined_string_type;
-
   // assert that the number of argument is equal to nb and extract them
   static const function_application_exprt::argumentst &args(
     const function_application_exprt &expr, size_t nb)
@@ -299,7 +290,7 @@ class string_constraint_generatort
     return args;
   }
 
-  exprt int_of_hex_char(exprt chr) const;
+  exprt int_of_hex_char(const exprt &chr) const;
   exprt is_high_surrogate(const exprt &chr) const;
   exprt is_low_surrogate(const exprt &chr) const;
   static exprt character_equals_ignore_case(

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -23,9 +23,9 @@ Function: string_constraint_generatort::add_axioms_for_code_point
 \*******************************************************************/
 
 string_exprt string_constraint_generatort::add_axioms_for_code_point(
-  const exprt &code_point)
+  const exprt &code_point, const refined_string_typet &ref_type)
 {
-  string_exprt res(get_char_type());
+  string_exprt res=fresh_string(ref_type);
   const typet &type=code_point.type();
   assert(type.id()==ID_signedbv);
 
@@ -50,21 +50,21 @@ string_exprt string_constraint_generatort::add_axioms_for_code_point(
   implies_exprt a2(not_exprt(small), res.axiom_for_has_length(2));
   axioms.push_back(a2);
 
-  typecast_exprt code_point_as_char(code_point, get_char_type());
+  typecast_exprt code_point_as_char(code_point, ref_type.get_char_type());
   implies_exprt a3(small, equal_exprt(res[0], code_point_as_char));
   axioms.push_back(a3);
 
   plus_exprt first_char(
     hexD800, div_exprt(minus_exprt(code_point, hex010000), hex0400));
   implies_exprt a4(
     not_exprt(small),
-    equal_exprt(res[0], typecast_exprt(first_char, get_char_type())));
+    equal_exprt(res[0], typecast_exprt(first_char, ref_type.get_char_type())));
   axioms.push_back(a4);
 
   plus_exprt second_char(hexDC00, mod_exprt(code_point, hex0400));
   implies_exprt a5(
     not_exprt(small),
-    equal_exprt(res[1], typecast_exprt(second_char, get_char_type())));
+    equal_exprt(res[1], typecast_exprt(second_char, ref_type.get_char_type())));
   axioms.push_back(a5);
 
   return res;
@@ -88,8 +88,8 @@ Function: string_constraint_generatort::is_high_surrogate
 exprt string_constraint_generatort::is_high_surrogate(const exprt &chr) const
 {
   return and_exprt(
-    binary_relation_exprt(chr, ID_ge, constant_char(0xD800)),
-    binary_relation_exprt(chr, ID_le, constant_char(0xDBFF)));
+    binary_relation_exprt(chr, ID_ge, constant_char(0xD800, chr.type())),
+    binary_relation_exprt(chr, ID_le, constant_char(0xDBFF, chr.type())));
 }
 
 /*******************************************************************\
@@ -110,8 +110,8 @@ Function: string_constraint_generatort::is_low_surrogate
 exprt string_constraint_generatort::is_low_surrogate(const exprt &chr) const
 {
   return and_exprt(
-    binary_relation_exprt(chr, ID_ge, constant_char(0xDC00)),
-    binary_relation_exprt(chr, ID_le, constant_char(0xDFFF)));
+    binary_relation_exprt(chr, ID_ge, constant_char(0xDC00, chr.type())),
+    binary_relation_exprt(chr, ID_le, constant_char(0xDFFF, chr.type())));
 }
 
 /*******************************************************************\
@@ -163,8 +163,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at(
   string_exprt str=add_axioms_for_string_expr(args(f, 2)[0]);
   const exprt &pos=args(f, 2)[1];
 
-  symbol_exprt result=string_exprt::fresh_symbol("char", return_type);
-  exprt index1=from_integer(1, get_index_type());
+  symbol_exprt result=fresh_symbol("char", return_type);
+  exprt index1=from_integer(1, str.length().type());
   const exprt &char1=str[pos];
   const exprt &char2=str[plus_exprt(pos, index1)];
   exprt char1_as_int=typecast_exprt(char1, return_type);
@@ -198,13 +198,13 @@ exprt string_constraint_generatort::add_axioms_for_code_point_before(
   assert(args.size()==2);
   typet return_type=f.type();
   assert(return_type.id()==ID_signedbv);
-  symbol_exprt result=string_exprt::fresh_symbol("char", return_type);
+  symbol_exprt result=fresh_symbol("char", return_type);
   string_exprt str=add_axioms_for_string_expr(args[0]);
 
   const exprt &char1=
-    str[minus_exprt(args[1], from_integer(2, get_index_type()))];
+    str[minus_exprt(args[1], from_integer(2, str.length().type()))];
   const exprt &char2=
-    str[minus_exprt(args[1], from_integer(1, get_index_type()))];
+    str[minus_exprt(args[1], from_integer(1, str.length().type()))];
   exprt char1_as_int=typecast_exprt(char1, return_type);
   exprt char2_as_int=typecast_exprt(char2, return_type);
 
@@ -238,10 +238,9 @@ exprt string_constraint_generatort::add_axioms_for_code_point_count(
   const exprt &begin=args(f, 3)[1];
   const exprt &end=args(f, 3)[2];
   const typet &return_type=f.type();
-  symbol_exprt result=
-    string_exprt::fresh_symbol("code_point_count", return_type);
+  symbol_exprt result=fresh_symbol("code_point_count", return_type);
   minus_exprt length(end, begin);
-  div_exprt minimum(length, from_integer(2, get_index_type()));
+  div_exprt minimum(length, from_integer(2, length.type()));
   axioms.push_back(binary_relation_exprt(result, ID_le, length));
   axioms.push_back(binary_relation_exprt(result, ID_ge, minimum));
 
@@ -270,8 +269,7 @@ exprt string_constraint_generatort::add_axioms_for_offset_by_code_point(
   const exprt &index=args(f, 3)[1];
   const exprt &offset=args(f, 3)[2];
   const typet &return_type=f.type();
-  symbol_exprt result=
-    string_exprt::fresh_symbol("offset_by_code_point", return_type);
+  symbol_exprt result=fresh_symbol("offset_by_code_point", return_type);
 
   exprt minimum=plus_exprt(index, offset);
   exprt maximum=plus_exprt(index, plus_exprt(offset, offset));