Corrections to the string solver

src/goto-programs/string_refine_preprocess.h

@@ -14,6 +14,7 @@ Date:   September 2016
 
 #include <goto-programs/goto_model.h>
 #include <util/ui_message.h>
+#include <util/string_expr.h>
 
 class string_refine_preprocesst:public messaget
 {
@@ -29,28 +30,21 @@ class string_refine_preprocesst:public messaget
   typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash> id_mapt;
   typedef std::unordered_map<exprt, exprt, irep_hash> expr_mapt;
 
-  // String builders maps the different names of a same StringBuilder object
-  // to a unique expression.
-  expr_mapt string_builders;
-
   // Map name of Java string functions to there equivalent in the solver
   id_mapt side_effect_functions;
   id_mapt string_functions;
   id_mapt c_string_functions;
   id_mapt string_function_calls;
-  id_mapt string_of_char_array_functions;
-  id_mapt string_of_char_array_function_calls;
-  id_mapt side_effect_char_array_functions;
 
   std::unordered_map<irep_idt, std::string, irep_id_hash> signatures;
-  expr_mapt hidden_strings;
-  expr_mapt java_to_cprover_strings;
 
   // unique id for each newly created symbols
   int next_symbol_id;
 
   void initialize_string_function_table();
 
+  static bool check_java_type(const typet &type, const std::string &tag);
+
   static bool is_java_string_pointer_type(const typet &type);
 
   static bool is_java_string_type(const typet &type);
@@ -61,6 +55,20 @@ class string_refine_preprocesst:public messaget
 
   static bool is_java_char_sequence_type(const typet &type);
 
+  static bool is_java_char_sequence_pointer_type(const typet &type);
+
+  static bool is_java_char_array_type(const typet &type);
+
+  static bool is_java_char_array_pointer_type(const typet &type);
+
+  static bool implements_java_char_sequence(const typet &type)
+  {
+      return
+        is_java_char_sequence_pointer_type(type) ||
+        is_java_string_builder_pointer_type(type) ||
+        is_java_string_pointer_type(type);
+  }
+
   symbol_exprt fresh_array(
     const typet &type, const source_locationt &location);
   symbol_exprt fresh_string(
@@ -110,6 +118,9 @@ class string_refine_preprocesst:public messaget
   void get_data_and_length_type_of_string(
     const exprt &expr, typet &data_type, typet &length_type);
 
+  void get_data_and_length_type_of_char_array(
+    const exprt &expr, typet &data_type, typet &length_type);
+
   function_application_exprt build_function_application(
     const irep_idt &function_name,
     const typet &type,
@@ -136,27 +147,16 @@ class string_refine_preprocesst:public messaget
     const source_locationt &location,
     const std::string &signature);
 
-  void make_assign(
-    goto_programt &goto_program,
-    goto_programt::targett &target,
-    const exprt &lhs,
-    const code_typet &function_type,
-    const irep_idt &function_name,
-    const exprt::operandst &arg,
-    const source_locationt &loc,
-    const std::string &sig);
-
   exprt make_cprover_string_assign(
     goto_programt &goto_program,
     goto_programt::targett &target,
     const exprt &rhs,
     const source_locationt &location);
 
-  void make_string_copy(
+  string_exprt make_cprover_char_array_assign(
     goto_programt &goto_program,
     goto_programt::targett &target,
-    const exprt &lhs,
-    const exprt &argument,
+    const exprt &rhs,
     const source_locationt &location);
 
   void make_string_function(
@@ -192,33 +192,6 @@ class string_refine_preprocesst:public messaget
   void make_to_char_array_function(
     goto_programt &goto_program, goto_programt::targett &);
 
-  exprt make_cprover_char_array_assign(
-    goto_programt &goto_program,
-    goto_programt::targett &target,
-    const exprt &rhs,
-    const source_locationt &location);
-
-  void make_char_array_function(
-    goto_programt &goto_program,
-    goto_programt::targett &target,
-    const irep_idt &function_name,
-    const std::string &signature,
-    std::size_t index,
-    bool assign_first_arg=false,
-    bool skip_first_arg=false);
-
-  void make_char_array_function_call(
-    goto_programt &goto_program,
-    goto_programt::targett &target,
-    const irep_idt &function_name,
-    const std::string &signature);
-
-  void make_char_array_side_effect(
-    goto_programt &goto_program,
-    goto_programt::targett &target,
-    const irep_idt &function_name,
-    const std::string &signature);
-
   void replace_string_calls(goto_functionst::function_mapt::iterator f_it);
 };
 

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -50,7 +50,16 @@ class java_bytecode_convert_classt:public messaget
       convert(parse_tree.parsed_class);
     else if(string_refinement_enabled &&
             parse_tree.parsed_class.name=="java.lang.String")
-      add_string_type();
+      add_string_type("java.lang.String");
+    else if(string_refinement_enabled &&
+            parse_tree.parsed_class.name=="java.lang.StringBuilder")
+      add_string_type("java.lang.StringBuilder");
+    else if(string_refinement_enabled &&
+            parse_tree.parsed_class.name=="java.lang.CharSequence")
+      add_string_type("java.lang.CharSequence");
+    else if(string_refinement_enabled &&
+            parse_tree.parsed_class.name=="java.lang.StringBuffer")
+      add_string_type("java.lang.StringBuffer");
     else
       generate_class_stub(parse_tree.parsed_class.name);
   }
@@ -72,7 +81,7 @@ class java_bytecode_convert_classt:public messaget
 
   void generate_class_stub(const irep_idt &class_name);
   void add_array_types();
-  void add_string_type();
+  void add_string_type(const irep_idt &class_name);
 };
 
 /*******************************************************************\
@@ -406,15 +415,17 @@ bool java_bytecode_convert_class(
 
 Function: java_bytecode_convert_classt::add_string_type
 
+  Inputs: a name for the class such as "java.lang.String"
+
  Purpose: Implements the java.lang.String type in the case that
           we provide an internal implementation.
 
 \*******************************************************************/
 
-void java_bytecode_convert_classt::add_string_type()
+void java_bytecode_convert_classt::add_string_type(const irep_idt &class_name)
 {
   class_typet string_type;
-  string_type.set_tag("java.lang.String");
+  string_type.set_tag(class_name);
   string_type.components().resize(3);
   string_type.components()[0].set_name("@java.lang.Object");
   string_type.components()[0].set_pretty_name("@java.lang.Object");
@@ -432,8 +443,8 @@ void java_bytecode_convert_classt::add_string_type()
   string_type.add_base(symbol_typet("java::java.lang.Object"));
 
   symbolt string_symbol;
-  string_symbol.name="java::java.lang.String";
-  string_symbol.base_name="java.lang.String";
+  string_symbol.name="java::"+id2string(class_name);
+  string_symbol.base_name=id2string(class_name);
   string_symbol.type=string_type;
   string_symbol.is_type=true;
 
@@ -445,8 +456,8 @@ void java_bytecode_convert_classt::add_string_type()
   symbolt string_equals_symbol;
   string_equals_symbol.name=
     "java::java.lang.String.equals:(Ljava/lang/Object;)Z";
-  string_equals_symbol.base_name="java.lang.String.equals";
-  string_equals_symbol.pretty_name="java.lang.String.equals";
+  string_equals_symbol.base_name=id2string(class_name)+".equals";
+  string_equals_symbol.pretty_name=id2string(class_name)+".equals";
   string_equals_symbol.mode=ID_java;
 
   code_typet string_equals_type;

src/solvers/refinement/string_constraint.h

@@ -48,7 +48,6 @@ class string_constraintt: public exprt
     return operands()[4];
   }
 
-
  private:
   string_constraintt();
 

src/solvers/refinement/string_constraint_generator.h

@@ -14,6 +14,7 @@ Author: Romain Brenguier, [email protected]
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
 
 #include <util/string_expr.h>
+#include <util/replace_expr.h>
 #include <util/refined_string_type.h>
 #include <solvers/refinement/string_constraint.h>
 
@@ -65,21 +66,20 @@ class string_constraint_generatort
   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);
+  string_exprt get_string_expr(const exprt &expr);
+  string_exprt convert_java_string_to_string_exprt(
+    const exprt &underlying);
+  plus_exprt plus_exprt_with_overflow_check(const exprt &op1, const exprt &op2);
 
-  // We maintain a map from symbols to strings.
-  std::map<irep_idt, string_exprt> symbol_to_string;
+  // Maps unresolved symbols to the string_exprt that was created for them
+  std::map<irep_idt, string_exprt> unresolved_symbols;
 
-  string_exprt find_or_add_string_of_symbol(const symbol_exprt &sym);
 
-  void assign_to_symbol(
-    const symbol_exprt &sym, const string_exprt &expr)
-  {
-    symbol_to_string[sym.get_identifier()]=expr;
-  }
+  string_exprt find_or_add_string_of_symbol(
+    const symbol_exprt &sym,
+    const refined_string_typet &ref_type);
 
-  string_exprt add_axioms_for_string_expr(const exprt &expr);
-  void set_string_symbol_equal_to_expr(
-    const symbol_exprt &sym, const exprt &str);
+  string_exprt add_axioms_for_refined_string(const exprt &expr);
 
   exprt add_axioms_for_function_application(
     const function_application_exprt &expr);
@@ -96,6 +96,8 @@ class string_constraint_generatort
   const std::size_t MAX_FLOAT_LENGTH=15;
   const std::size_t MAX_DOUBLE_LENGTH=30;
 
+  std::map<function_application_exprt, exprt> function_application_cache;
+
   static irep_idt extract_java_string(const symbol_exprt &s);
 
   exprt axiom_for_is_positive_index(const exprt &x);
@@ -117,6 +119,9 @@ class string_constraint_generatort
   // The specification is partial: the actual value is not actually computed
   // but we ensure that hash codes of equal strings are equal.
   exprt add_axioms_for_hash_code(const function_application_exprt &f);
+  // To each string on which hash_code was called we associate a symbol
+  // representing the return value of the hash_code function.
+  std::map<string_exprt, exprt> hash_code_of_string;
 
   exprt add_axioms_for_is_empty(const function_application_exprt &f);
   exprt add_axioms_for_is_prefix(
@@ -224,7 +229,9 @@ class string_constraint_generatort
   // the start for negative number
   string_exprt add_axioms_from_float(const function_application_exprt &f);
   string_exprt add_axioms_from_float(
-    const exprt &f, bool double_precision=false);
+    const exprt &f,
+    const refined_string_typet &ref_type,
+    bool double_precision);
 
   // Add axioms corresponding to the String.valueOf(D) java function
   // TODO: the specifications is only partial
@@ -253,6 +260,7 @@ class string_constraint_generatort
   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);
+  exprt add_axioms_for_char_pointer(const function_application_exprt &fun);
   string_exprt add_axioms_for_if(const if_exprt &expr);
   exprt add_axioms_for_char_literal(const function_application_exprt &f);
 
@@ -270,6 +278,8 @@ class string_constraint_generatort
     const function_application_exprt &f);
 
   exprt add_axioms_for_parse_int(const function_application_exprt &f);
+  exprt add_axioms_for_correct_number_format(
+    const string_exprt &str, std::size_t max_size=10);
   exprt add_axioms_for_to_char_array(const function_application_exprt &f);
   exprt add_axioms_for_compare_to(const function_application_exprt &f);
 
@@ -278,6 +288,9 @@ class string_constraint_generatort
   // string pointers
   symbol_exprt add_axioms_for_intern(const function_application_exprt &f);
 
+  // Pool used for the intern method
+  std::map<string_exprt, symbol_exprt> intern_of_string;
+
   // Tells which language is used. C and Java are supported
   irep_idt mode;
 
@@ -293,14 +306,8 @@ class string_constraint_generatort
   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(
+  exprt character_equals_ignore_case(
     exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z);
-
-  // Pool used for the intern method
-  std::map<string_exprt, symbol_exprt> pool;
-
-  // Used to determine whether hashcode should be equal
-  std::map<string_exprt, symbol_exprt> hash;
 };
 
 #endif

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -160,17 +160,18 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at(
 {
   typet return_type=f.type();
   assert(return_type.id()==ID_signedbv);
-  string_exprt str=add_axioms_for_string_expr(args(f, 2)[0]);
+  string_exprt str=get_string_expr(args(f, 2)[0]);
   const exprt &pos=args(f, 2)[1];
 
   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)];
+  const exprt &char2=str[plus_exprt_with_overflow_check(pos, index1)];
   exprt char1_as_int=typecast_exprt(char1, return_type);
   exprt char2_as_int=typecast_exprt(char2, return_type);
   exprt pair=pair_value(char1_as_int, char2_as_int, return_type);
-  exprt is_low=is_low_surrogate(str[plus_exprt(pos, index1)]);
+  exprt is_low=is_low_surrogate(
+    str[plus_exprt_with_overflow_check(pos, index1)]);
   exprt return_pair=and_exprt(is_high_surrogate(str[pos]), is_low);
 
   axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
@@ -199,7 +200,7 @@ exprt string_constraint_generatort::add_axioms_for_code_point_before(
   typet return_type=f.type();
   assert(return_type.id()==ID_signedbv);
   symbol_exprt result=fresh_symbol("char", return_type);
-  string_exprt str=add_axioms_for_string_expr(args[0]);
+  string_exprt str=get_string_expr(args[0]);
 
   const exprt &char1=
     str[minus_exprt(args[1], from_integer(2, str.length().type()))];
@@ -234,7 +235,7 @@ Function: string_constraint_generatort::add_axioms_for_code_point_count
 exprt string_constraint_generatort::add_axioms_for_code_point_count(
   const function_application_exprt &f)
 {
-  string_exprt str=add_axioms_for_string_expr(args(f, 3)[0]);
+  string_exprt str=get_string_expr(args(f, 3)[0]);
   const exprt &begin=args(f, 3)[1];
   const exprt &end=args(f, 3)[2];
   const typet &return_type=f.type();
@@ -265,14 +266,15 @@ Function: string_constraint_generatort::add_axioms_for_offset_by_code_point
 exprt string_constraint_generatort::add_axioms_for_offset_by_code_point(
   const function_application_exprt &f)
 {
-  string_exprt str=add_axioms_for_string_expr(args(f, 3)[0]);
+  string_exprt str=get_string_expr(args(f, 3)[0]);
   const exprt &index=args(f, 3)[1];
   const exprt &offset=args(f, 3)[2];
   const typet &return_type=f.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));
+  exprt minimum=plus_exprt_with_overflow_check(index, offset);
+  exprt maximum=plus_exprt_with_overflow_check(
+    index, plus_exprt_with_overflow_check(offset, offset));
   axioms.push_back(binary_relation_exprt(result, ID_le, maximum));
   axioms.push_back(binary_relation_exprt(result, ID_ge, minimum));