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

@@ -257,60 +257,57 @@ static exprt get_component_in_struct(const struct_exprt &expr,
 /// 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
 /// \param message: message handler for warnings
 /// \param ns: namespace
 /// \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) {
+add_axioms_for_format_specifier(
+  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()
@@ -330,9 +327,15 @@ add_axioms_for_format_specifier(symbol_generatort &fresh_symbol,
   {
     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);
+    auto format_specifier_result = add_axioms_for_format_specifier(
+      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());
@@ -417,8 +420,16 @@ 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);
       }