Initialize return_code for all builtin_functions

Author: romainbrenguier

src/solvers/refinement/string_builtin_function.cpp

@@ -18,8 +18,10 @@ static array_string_exprt make_string(
 
 string_transformation_builtin_functiont::
   string_transformation_builtin_functiont(
+    const exprt &return_code,
     const std::vector<exprt> &fun_args,
     array_poolt &array_pool)
+  : string_builtin_functiont(return_code)
 {
   PRECONDITION(fun_args.size() > 2);
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
@@ -55,8 +57,10 @@ optionalt<exprt> string_transformation_builtin_functiont::eval(
 }
 
 string_insertion_builtin_functiont::string_insertion_builtin_functiont(
+  const exprt &return_code,
   const std::vector<exprt> &fun_args,
   array_poolt &array_pool)
+  : string_builtin_functiont(return_code)
 {
   PRECONDITION(fun_args.size() > 4);
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
@@ -69,8 +73,10 @@ string_insertion_builtin_functiont::string_insertion_builtin_functiont(
 }
 
 string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(
+  const exprt &return_code,
   const std::vector<exprt> &fun_args,
   array_poolt &array_pool)
+  : string_insertion_builtin_functiont(return_code)
 {
   PRECONDITION(fun_args.size() >= 4 && fun_args.size() <= 6);
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
@@ -209,9 +215,10 @@ optionalt<exprt> string_insertion_builtin_functiont::eval(
 }
 
 string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(
+  const exprt &return_code,
   const function_application_exprt &f,
   array_poolt &array_pool)
-  : function_application(f)
+  : string_builtin_functiont(return_code), function_application(f)
 {
   const std::vector<exprt> &fun_args = f.arguments();
   std::size_t i = 0;

src/solvers/refinement/string_builtin_function.h

@@ -38,8 +38,16 @@ class string_builtin_functiont
   virtual exprt
   add_constraints(string_constraint_generatort &constraint_generator) const = 0;
 
-protected:
+  exprt return_code;
+
+private:
   string_builtin_functiont() = default;
+
+protected:
+  explicit string_builtin_functiont(const exprt &return_code)
+    : return_code(return_code)
+  {
+  }
 };
 
 /// String builtin_function transforming one string into another
@@ -49,14 +57,14 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
   array_string_exprt result;
   array_string_exprt input;
   std::vector<exprt> args;
-  exprt return_code;
 
   /// Constructor from arguments of a function application.
   /// The arguments in `fun_args` should be in order:
   /// an integer `result.length`, a character pointer `&result[0]`,
   /// a string `arg1` of type refined_string_typet, and potentially some
   /// arguments of primitive types.
   string_transformation_builtin_functiont(
+    const exprt &return_code,
     const std::vector<exprt> &fun_args,
     array_poolt &array_pool);
 
@@ -88,9 +96,10 @@ class string_concat_char_builtin_functiont
   /// an integer `result.length`, a character pointer `&result[0]`,
   /// a string `arg1` of type refined_string_typet, and a character.
   string_concat_char_builtin_functiont(
+    const exprt &return_code,
     const std::vector<exprt> &fun_args,
     array_poolt &array_pool)
-    : string_transformation_builtin_functiont(fun_args, array_pool)
+    : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
   {
   }
 
@@ -117,7 +126,6 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   array_string_exprt input1;
   array_string_exprt input2;
   std::vector<exprt> args;
-  exprt return_code;
 
   /// Constructor from arguments of a function application.
   /// The arguments in `fun_args` should be in order:
@@ -126,6 +134,7 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   /// a string `arg2` of type refined_string_typet,
   /// and potentially some arguments of primitive types.
   string_insertion_builtin_functiont(
+    const exprt &return_code,
     const std::vector<exprt> &fun_args,
     array_poolt &array_pool);
 
@@ -162,7 +171,10 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   };
 
 protected:
-  string_insertion_builtin_functiont() = default;
+  explicit string_insertion_builtin_functiont(const exprt &return_code)
+    : string_builtin_functiont(return_code)
+  {
+  }
 };
 
 class string_concatenation_builtin_functiont final
@@ -176,6 +188,7 @@ class string_concatenation_builtin_functiont final
   /// a string `arg2` of type refined_string_typet,
   /// optionally followed by an integer `start` and an integer `end`.
   string_concatenation_builtin_functiont(
+    const exprt &return_code,
     const std::vector<exprt> &fun_args,
     array_poolt &array_pool);
 
@@ -240,6 +253,7 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
   std::vector<exprt> args;
 
   string_builtin_function_with_no_evalt(
+    const exprt &return_code,
     const function_application_exprt &f,
     array_poolt &array_pool);
 

src/solvers/refinement/string_refinement_util.cpp

@@ -167,6 +167,7 @@ equation_symbol_mappingt::find_equations(const exprt &expr)
 /// \return a unique pointer to the created object
 static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
   const function_application_exprt &fun_app,
+  const exprt &return_code,
   array_poolt &array_pool)
 {
   const auto name = expr_checked_cast<symbol_exprt>(fun_app.function());
@@ -175,18 +176,18 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
 
   if(id == ID_cprover_string_insert_func)
     return util_make_unique<string_insertion_builtin_functiont>(
-      fun_app.arguments(), array_pool);
+      return_code, fun_app.arguments(), array_pool);
 
   if(id == ID_cprover_string_concat_func)
     return util_make_unique<string_concatenation_builtin_functiont>(
-      fun_app.arguments(), array_pool);
+      return_code, fun_app.arguments(), array_pool);
 
   if(id == ID_cprover_string_concat_char_func)
     return util_make_unique<string_concat_char_builtin_functiont>(
-      fun_app.arguments(), array_pool);
+      return_code, fun_app.arguments(), array_pool);
 
   return util_make_unique<string_builtin_function_with_no_evalt>(
-    fun_app.arguments(), array_pool);
+    return_code, fun_app, array_pool);
 }
 
 string_dependenciest::string_nodet &
@@ -322,7 +323,9 @@ bool add_node(
   if(!fun_app)
     return false;
 
-  auto builtin_function = to_string_builtin_function(*fun_app, array_pool);
+  auto builtin_function =
+    to_string_builtin_function(*fun_app, equation.lhs(), array_pool);
+
   CHECK_RETURN(builtin_function != nullptr);
   const auto &builtin_function_node = dependencies.make_node(builtin_function);
   // Warning: `builtin_function` has been emptied and should not be used anymore