Add string type support to SMT back-end

src/ansi-c/goto-conversion/goto_check_c.cpp

@@ -1597,6 +1597,48 @@ void goto_check_ct::bounds_check_index(
   std::string name = array_name(expr.array());
 
   const exprt &index = expr.index();
+  const exprt &array_size = array_type.id() == ID_array
+                              ? to_array_type(array_type).size()
+                              : to_vector_type(array_type).size();
+
+  // Mathematical types (integer, natural) are used for unbounded arrays (e.g.,
+  // heap models). Also, arrays with no known size (nil) cannot be meaningfully
+  // bounds-checked via byte offsets. In either case, for arrays accessed via a
+  // symbol or nested index, just check that the index is non-negative.
+  if(
+    index.type().id() == ID_integer ||
+    index.type().id() == ID_natural ||
+    array_size.is_nil())
+  {
+    if(
+      index.type().id() != ID_unsignedbv &&
+      index.type().id() != ID_natural &&
+      (index.type().id() == ID_integer ||
+       index.type().id() == ID_signedbv) &&
+      (expr.array().id() == ID_symbol || expr.array().id() == ID_index))
+    {
+      const auto i = numeric_cast<mp_integer>(index);
+
+      if(!i.has_value() || *i < 0)
+      {
+        exprt zero = from_integer(0, index.type());
+
+        binary_relation_exprt inequality(index, ID_ge, std::move(zero));
+
+        add_guarded_property(
+          inequality,
+          name + " lower bound",
+          "array bounds",
+          true, // fatal
+          expr.find_source_location(),
+          expr,
+          guard);
+      }
+    }
+
+    return;
+  }
+
   object_descriptor_exprt ode;
   ode.build(expr, ns);
 

src/solvers/smt2/smt2_conv.cpp

@@ -2707,8 +2707,66 @@ void smt2_convt::convert_expr(const exprt &expr)
   else if(expr.id() == ID_function_application)
   {
     const auto &function_application_expr = to_function_application_expr(expr);
+
+    // Check for string operations by looking at the function symbol name
+    std::string fn_name;
+    if(function_application_expr.function().id() == ID_symbol)
+      fn_name = id2string(
+        to_symbol_expr(function_application_expr.function()).get_identifier());
+
+    // Map Strata function names to SMT-LIB names for string/regex ops
+    std::string smt_name;
+    if(fn_name == "Str.Concat")
+      smt_name = "str.++";
+    else if(fn_name == "Str.Length")
+      smt_name = "str.len";
+    else if(fn_name == "Str.Substr")
+      smt_name = "str.substr";
+    else if(fn_name == "Str.ToRegEx")
+      smt_name = "str.to_re";
+    else if(fn_name == "Str.InRegEx")
+      smt_name = "str.in_re";
+    else if(fn_name == "Re.AllChar")
+      smt_name = "re.allchar";
+    else if(fn_name == "Re.All")
+      smt_name = "re.all";
+    else if(fn_name == "Re.Range")
+      smt_name = "re.range";
+    else if(fn_name == "Re.Concat")
+      smt_name = "re.concat";
+    else if(fn_name == "Re.Star")
+      smt_name = "re.*";
+    else if(fn_name == "Re.Plus")
+      smt_name = "re.+";
+    else if(fn_name == "Re.Loop")
+      smt_name = "re.loop";
+    else if(fn_name == "Re.Union")
+      smt_name = "re.union";
+    else if(fn_name == "Re.Inter")
+      smt_name = "re.inter";
+    else if(fn_name == "Re.Comp")
+      smt_name = "re.comp";
+    else if(fn_name == "Re.None")
+      smt_name = "re.none";
+
+    if(!smt_name.empty())
+    {
+      const auto &args = function_application_expr.arguments();
+      if(args.empty())
+        out << smt_name;
+      else
+      {
+        out << '(' << smt_name;
+        for(const auto &arg : args)
+        {
+          out << ' ';
+          convert_expr(arg);
+        }
+        out << ')';
+      }
+    }
     // do not use parentheses if there function is a constant
-    if(function_application_expr.arguments().empty())
+    else if(function_application_expr.arguments().empty())
     {
       convert_expr(function_application_expr.function());
     }
@@ -3763,6 +3821,19 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
     out << "(_ bv" << (value_int - range_type.get_from()) << " " << width
         << ")";
   }
+  else if(expr_type.id()==ID_string)
+  {
+    const std::string &value = id2string(expr.get_value());
+    out << "\"";
+    for(char c : value)
+    {
+      if(c == '"')
+        out << "\"\"";
+      else
+        out << c;
+    }
+    out << "\"";
+  }
   else
     UNEXPECTEDCASE("unknown constant: "+expr_type.id_string());
 }
@@ -5991,6 +6062,10 @@ void smt2_convt::convert_type(const typet &type)
       UNEXPECTEDCASE("unsuppored range type");
     out << "(_ BitVec " << address_bits(size) << ")";
   }
+  else if(type.id()==ID_string)
+    out << "String";
+  else if(type.id()==ID_regex)
+    out << "RegLan";
   else
   {
     UNEXPECTEDCASE("unsupported type: "+type.id_string());

src/util/irep_ids.def

@@ -160,6 +160,7 @@ IREP_ID_TWO(C_default_value, #default_value)
 IREP_ID_ONE(base_name)
 IREP_ID_TWO(C_base_name, #base_name)
 IREP_ID_ONE(string)
+IREP_ID_ONE(regex)
 IREP_ID_ONE(is_cstring)
 IREP_ID_TWO(C_string_constant, #string_constant)
 IREP_ID_ONE(string_constant)