String refine preprocessing

src/goto-programs/string_refine_preprocess.h

@@ -0,0 +1,225 @@
+/*******************************************************************\
+
+Module: Preprocess a goto-programs so that calls to the java String
+        library are recognized by the PASS algorithm
+
+Author: Romain Brenguier
+
+Date:   September 2016
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_STRING_REFINE_PREPROCESS_H
+#define CPROVER_GOTO_PROGRAMS_STRING_REFINE_PREPROCESS_H
+
+#include <goto-programs/goto_model.h>
+#include <util/ui_message.h>
+
+class string_refine_preprocesst:public messaget
+{
+ public:
+  string_refine_preprocesst(
+    symbol_tablet &, goto_functionst &, message_handlert &);
+
+ private:
+  namespacet ns;
+  symbol_tablet & symbol_table;
+  goto_functionst & goto_functions;
+
+  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 is_java_string_pointer_type(const typet &type);
+
+  static bool is_java_string_type(const typet &type);
+
+  static bool is_java_string_builder_type(const typet &type);
+
+  static bool is_java_string_builder_pointer_type(const typet &type);
+
+  static bool is_java_char_sequence_type(const typet &type);
+
+  symbol_exprt fresh_array(
+    const typet &type, const source_locationt &location);
+  symbol_exprt fresh_string(
+    const typet &type, const source_locationt &location);
+
+  // get the data member of a java string
+  static exprt get_data(const exprt &string, const typet &data_type)
+  {
+    return member_exprt(string, "data", data_type);
+  }
+
+  // get the length member of a java string
+  exprt get_length(const exprt &string, const typet &length_type)
+  {
+    return member_exprt(string, "length", length_type);
+  }
+
+  // type of pointers to string
+  pointer_typet jls_ptr;
+  exprt replace_string(const exprt &in);
+  exprt replace_string_in_assign(const exprt &in);
+
+  void insert_assignments(
+    goto_programt &goto_program,
+    goto_programt::targett &target,
+    irep_idt function,
+    source_locationt location,
+    const std::list<code_assignt> &va);
+
+  exprt replace_string_pointer(const exprt &in);
+
+  // Replace string builders by expression of the mapping and make
+  // assignments for strings as string_exprt
+  exprt::operandst process_arguments(
+    goto_programt &goto_program,
+    goto_programt::targett &target,
+    const exprt::operandst &arguments,
+    const source_locationt &location,
+    const std::string &signature="");
+
+  // Signature of the named function if it is defined in the signature map,
+  // empty string otherwise
+  std::string function_signature(const irep_idt &function_id);
+
+  void declare_function(irep_idt function_name, const typet &type);
+
+  void get_data_and_length_type_of_string(
+    const exprt &expr, typet &data_type, typet &length_type);
+
+  function_application_exprt build_function_application(
+    const irep_idt &function_name,
+    const typet &type,
+    const source_locationt &location,
+    const exprt::operandst &arguments);
+
+  void make_normal_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 &arguments,
+    const source_locationt &location,
+    const std::string &signature="");
+
+  void make_string_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 &arguments,
+    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(
+    goto_programt &goto_program,
+    goto_programt::targett &target,
+    const exprt &lhs,
+    const exprt &argument,
+    const source_locationt &location);
+
+  void make_string_function(
+    goto_programt &goto_program,
+    goto_programt::targett &target,
+    const irep_idt &function_name,
+    const std::string &signature,
+    bool assign_first_arg=false,
+    bool skip_first_arg=false);
+
+  void make_string_function(
+    goto_programt &goto_program,
+    goto_programt::targett &target,
+    const exprt &lhs,
+    const code_typet &function_type,
+    const irep_idt &function_name,
+    const exprt::operandst &arguments,
+    const source_locationt &location,
+    const std::string &signature);
+
+  void make_string_function_call(
+    goto_programt &goto_program,
+    goto_programt::targett &target,
+    const irep_idt &function_name,
+    const std::string &signature);
+
+  void make_string_function_side_effect(
+    goto_programt &goto_program,
+    goto_programt::targett &target,
+    const irep_idt &function_name,
+    const std::string &signature);
+
+  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);
+};
+
+#endif

src/solvers/refinement/string_constraint.h

@@ -15,7 +15,7 @@ Author: Romain Brenguier, [email protected]
 
 #include <langapi/language_ui.h>
 #include <solvers/refinement/bv_refinement.h>
-#include <solvers/refinement/refined_string_type.h>
+#include <util/refined_string_type.h>
 
 class string_constraintt: public exprt
 {

src/solvers/refinement/string_constraint_generator.h

@@ -14,7 +14,7 @@ Author: Romain Brenguier, [email protected]
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
 
 #include <util/string_expr.h>
-#include <solvers/refinement/refined_string_type.h>
+#include <util/refined_string_type.h>
 #include <solvers/refinement/string_constraint.h>
 
 class string_constraint_generatort

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -132,7 +132,7 @@ string_exprt string_constraint_generatort::add_axioms_from_literal(
   else
   {
     // Java string constant
-    assert(refined_string_typet::is_unrefined_string_type(arg.type()));
+    assert(arg.id()==ID_symbol);
     const exprt &s=arg.op0();
 
     // It seems the value of the string is lost,