Merge pull request #7117 from diffblue/is_cstring

add __CPROVER_is_cstring(p) and __CPROVER_cstrlen(p)

Author: kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2316,6 +2316,52 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(is_list_expr);
   }
+  else if(identifier == CPROVER_PREFIX "is_cstring")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << "is_cstring expects one operand" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    if(expr.arguments()[0].type().id() != ID_pointer)
+    {
+      error().source_location = expr.arguments()[0].source_location();
+      error() << "is_cstring expects a pointer operand" << eom;
+      throw 0;
+    }
+
+    is_cstring_exprt is_cstring_expr(expr.arguments()[0]);
+    is_cstring_expr.add_source_location() = source_location;
+
+    return std::move(is_cstring_expr);
+  }
+  else if(identifier == CPROVER_PREFIX "cstrlen")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << "cstrlen expects one operand" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    if(expr.arguments()[0].type().id() != ID_pointer)
+    {
+      error().source_location = expr.arguments()[0].source_location();
+      error() << "cstrlen expects a pointer operand" << eom;
+      throw 0;
+    }
+
+    unary_exprt cstrlen_expr("cstrlen", expr.arguments()[0], size_type());
+    cstrlen_expr.add_source_location() = source_location;
+
+    return std::move(cstrlen_expr);
+  }
   else if(identifier==CPROVER_PREFIX "is_zero_string")
   {
     if(expr.arguments().size()!=1)

src/ansi-c/cprover_builtin_headers.h

@@ -13,6 +13,8 @@ _Bool __CPROVER_is_zero_string(const void *);
 // a singly-linked null-terminated dynamically-allocated list
 __CPROVER_bool __CPROVER_is_list();
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
+__CPROVER_bool __CPROVER_is_cstring(const char *);
+__CPROVER_size_t __CPROVER_cstrlen(const char *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
 __CPROVER_bool __CPROVER_r_ok();
 __CPROVER_bool __CPROVER_w_ok();

src/util/irep_ids.def

@@ -153,6 +153,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(is_cstring)
 IREP_ID_TWO(C_string_constant, #string_constant)
 IREP_ID_ONE(string_constant)
 IREP_ID_ONE(width)

src/util/pointer_expr.h

@@ -1059,6 +1059,62 @@ inline void validate_expr(const object_size_exprt &value)
     "Object size expression must have pointer typed operand.");
 }
 
+/// A predicate that indicates that a zero-terminated string
+/// starts at the given address
+class is_cstring_exprt : public unary_predicate_exprt
+{
+public:
+  explicit is_cstring_exprt(exprt address)
+    : unary_predicate_exprt(ID_is_cstring, std::move(address))
+  {
+    PRECONDITION(as_const(*this).address().type().id() == ID_pointer);
+  }
+
+  exprt &address()
+  {
+    return op0();
+  }
+
+  const exprt &address() const
+  {
+    return op0();
+  }
+};
+
+template <>
+inline bool can_cast_expr<is_cstring_exprt>(const exprt &base)
+{
+  return base.id() == ID_is_cstring;
+}
+
+inline void validate_expr(const is_cstring_exprt &value)
+{
+  validate_operands(value, 1, "is_cstring must have one operand");
+}
+
+/// \brief Cast an exprt to a \ref is_cstring_exprt
+///
+/// \a expr must be known to be \ref is_cstring_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref is_cstring_exprt
+inline const is_cstring_exprt &to_is_cstring_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_is_cstring);
+  const is_cstring_exprt &ret = static_cast<const is_cstring_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_is_cstring_expr(const exprt &)
+inline is_cstring_exprt &to_is_cstring_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_is_cstring);
+  is_cstring_exprt &ret = static_cast<is_cstring_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 /// A predicate that indicates that the object pointed to is live
 class live_object_exprt : public unary_predicate_exprt
 {