Refactor add_axioms_for_format_specifier

This makes it accept a function as argument, which gives for possible
types the corresponding value of the argument.
This will allow us to adapt more easily to a change in the way the
arguments of format are given: they are now given as a struct but we
want to have the possibility to give them as a string.

Author: romainbrenguier

src/solvers/strings/string_constraint_generator_format.cpp

@@ -258,7 +258,8 @@ get_component_in_struct(const struct_exprt &expr, irep_idt component_name)
 /// specifier.
 /// \param fresh_symbol: generator of fresh symbols
 /// \param fs: a format specifier
-/// \param arg: a struct containing the possible value of the argument to format
+/// \param get_arg: a function returning the possible value of the argument to
+///   format given their type.
 /// \param index_type: type for indexes in strings
 /// \param char_type: type of characters
 /// \param array_pool: pool of arrays representing strings
@@ -267,61 +268,42 @@ get_component_in_struct(const struct_exprt &expr, irep_idt component_name)
 /// \return String expression representing the output of String.format.
 static std::pair<array_string_exprt, string_constraintst>
 add_axioms_for_format_specifier(
-  symbol_generatort &fresh_symbol,
-  const format_specifiert &fs,
-  const struct_exprt &arg,
-  const typet &index_type,
-  const typet &char_type,
-  array_poolt &array_pool,
-  const messaget &message,
-  const namespacet &ns)
-{
+    symbol_generatort &fresh_symbol, const format_specifiert &fs,
+    const std::function<exprt(const irep_idt &)> &get_arg,
+    const typet &index_type, const typet &char_type, array_poolt &array_pool,
+    const messaget &message, const namespacet &ns) {
   string_constraintst constraints;
   const array_string_exprt res = array_pool.fresh_string(index_type, char_type);
   std::pair<exprt, string_constraintst> return_code;
   switch(fs.conversion)
   {
   case format_specifiert::DECIMAL_INTEGER:
-    return_code = add_axioms_for_string_of_int(
-      res, get_component_in_struct(arg, ID_int), 0, ns);
+    return_code = add_axioms_for_string_of_int(res, get_arg(ID_int), 0, ns);
     return {res, std::move(return_code.second)};
   case format_specifiert::HEXADECIMAL_INTEGER:
-    return_code =
-      add_axioms_from_int_hex(res, get_component_in_struct(arg, ID_int));
+    return_code = add_axioms_from_int_hex(res, get_arg(ID_int));
     return {res, std::move(return_code.second)};
   case format_specifiert::SCIENTIFIC:
     return_code = add_axioms_from_float_scientific_notation(
-      fresh_symbol,
-      res,
-      get_component_in_struct(arg, ID_float),
-      array_pool,
-      ns);
+        fresh_symbol, res, get_arg(ID_float), array_pool, ns);
     return {res, std::move(return_code.second)};
   case format_specifiert::DECIMAL_FLOAT:
     return_code = add_axioms_for_string_of_float(
-      fresh_symbol,
-      res,
-      get_component_in_struct(arg, ID_float),
-      array_pool,
-      ns);
+        fresh_symbol, res, get_arg(ID_float), array_pool, ns);
     return {res, std::move(return_code.second)};
   case format_specifiert::CHARACTER:
-    return_code =
-      add_axioms_from_char(res, get_component_in_struct(arg, ID_char));
+    return_code = add_axioms_from_char(res, get_arg(ID_char));
     return {res, std::move(return_code.second)};
   case format_specifiert::BOOLEAN:
-    return_code =
-      add_axioms_from_bool(res, get_component_in_struct(arg, ID_boolean));
+    return_code = add_axioms_from_bool(res, get_arg(ID_boolean));
     return {res, std::move(return_code.second)};
   case format_specifiert::STRING:
   {
-    auto string_expr =
-      get_string_expr(array_pool, get_component_in_struct(arg, "string_expr"));
+    auto string_expr = get_string_expr(array_pool, get_arg("string_expr"));
     return {std::move(string_expr), {}};
   }
   case format_specifiert::HASHCODE:
-    return_code = add_axioms_for_string_of_int(
-      res, get_component_in_struct(arg, "hashcode"), 0, ns);
+    return_code = add_axioms_for_string_of_int(res, get_arg("hashcode"), 0, ns);
     return {res, std::move(return_code.second)};
   case format_specifiert::LINE_SEPARATOR:
     // TODO: the constant should depend on the system: System.lineSeparator()
@@ -342,14 +324,8 @@ add_axioms_for_format_specifier(
     format_specifiert fs_lower = fs;
     fs_lower.conversion = tolower(fs.conversion);
     auto format_specifier_result = add_axioms_for_format_specifier(
-      fresh_symbol,
-      fs_lower,
-      arg,
-      index_type,
-      char_type,
-      array_pool,
-      message,
-      ns);
+        fresh_symbol, fs_lower, get_arg, index_type, char_type, array_pool,
+        message, ns);
 
     const exprt return_code_upper_case =
       fresh_symbol("return_code_upper_case", get_return_code_type());
@@ -434,14 +410,11 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
         }
 
         auto result = add_axioms_for_format_specifier(
-          fresh_symbol,
-          fs,
-          to_struct_expr(arg),
-          index_type,
-          char_type,
-          array_pool,
-          message,
-          ns);
+            fresh_symbol, fs,
+            [&](const irep_idt &id) {
+              return get_component_in_struct(to_struct_expr(arg), id);
+            },
+            index_type, char_type, array_pool, message, ns);
         merge(constraints, std::move(result.second));
         intermediary_strings.push_back(result.first);
       }