Make add_axioms_for_format accept string arguments

Add the possibility to pass argument to the builtin format functtion as
strings instead structs with fields.

Author: romainbrenguier

src/solvers/strings/string_constraint_generator_format.cpp

@@ -316,8 +316,8 @@ add_axioms_for_format_specifier(
     return {res, std::move(return_code.second)};
   case format_specifiert::STRING:
   {
-    auto string_expr =
-      get_string_expr(array_pool, get_arg("string_expr"));
+    const exprt arg_string = get_arg("string_expr");
+    const array_string_exprt string_expr = to_array_string_expr(arg_string);
     return {std::move(string_expr), {}};
   }
   case format_specifiert::HASHCODE:
@@ -380,6 +380,69 @@ add_axioms_for_format_specifier(
   }
 }
 
+/// Deserialize an argument for format from an \p string
+exprt format_arg_from_string(
+  const array_string_exprt &string, const irep_idt &id)
+{
+  if(id == "string_expr")
+    return string;
+  if(id == ID_int)
+  {
+    // Assume the string has length 4
+    // (int64)string.content[0] << 48 | (int64) string.content[1] << 32 |
+    // (int64)string.content[2] << 16 | (int64) string.content[3]
+    const signedbv_typet type{64};
+    return bitor_exprt{
+      bitor_exprt{
+        shl_exprt{
+          typecast_exprt(
+            index_exprt(
+              string.content(), from_integer(0, string.length().type())),
+            type),
+          48},
+        shl_exprt{
+          typecast_exprt{
+            index_exprt{string.content(),
+                        from_integer(1, string.length().type())},
+            type},
+          32}
+      },
+      bitor_exprt{
+        shl_exprt{
+          typecast_exprt(
+            index_exprt(
+              string.content(), from_integer(1, string.length().type())),
+            type),
+          16},
+        typecast_exprt{
+          index_exprt{string.content(),
+                      from_integer(3, string.length().type())},
+          type}}
+    };
+  }
+  if(id == ID_char)
+  {
+    // We assume the string has length exactly 1 and return:
+    // (unsigned16)string.content[0]
+    const unsignedbv_typet type{16};
+    return typecast_exprt{
+      index_exprt(string.content(), from_integer(0, string.length().type())),
+      type};
+  }
+  if(id == ID_boolean)
+  {
+    // We assume the string already corresponds to the result
+    return string;
+  }
+  if(id == ID_float)
+  {
+    // Deserialize an int and cast to float
+    const exprt as_int = format_arg_from_string(string, ID_int);
+    return typecast_exprt{as_int, floatbv_typet{}};
+  }
+  UNHANDLED_CASE;
+}
+
 /// Parse `s` and add axioms ensuring the output corresponds to the output of
 /// String.format.
 /// \param fresh_symbol: generator of fresh symbols
@@ -421,7 +484,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
         {
           INVARIANT(
             arg_count < args.size(), "number of format must match specifiers");
-          arg = to_struct_expr(args[arg_count++]);
+          arg = args[arg_count++];
         }
         else
         {
@@ -434,12 +497,28 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
           arg = to_struct_expr(args[fs.index - 1]);
         }
 
+        std::function<exprt(const irep_idt &)> get_arg;
+        if(is_refined_string_type(arg.type()))
+        {
+          const array_string_exprt string_arg =
+            get_string_expr(array_pool, arg);
+          get_arg = [string_arg](const irep_idt &id){
+            return format_arg_from_string(string_arg, id);
+          };
+        }
+        else
+        {
+          INVARIANT(
+            arg.id() == ID_struct,
+            "format argument should be a string or a struct");
+          get_arg = [&](const irep_idt &id){
+            return get_component_in_struct(to_struct_expr(arg), id);
+          };
+        }
         auto result = add_axioms_for_format_specifier(
           fresh_symbol,
           fs,
-          [&](const irep_idt &id) {
-            return get_component_in_struct(to_struct_expr(arg), id);
-          },
+          get_arg,
           index_type,
           char_type,
           array_pool,