introduce code_with_contract_typet

This documents an existing, informal, variant of code_typet, which is
decorated with predicates for code contracts.

Author: kroening

src/ansi-c/c_typecheck_base.cpp

@@ -754,15 +754,19 @@ void c_typecheck_baset::typecheck_declaration(
       typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_ensures);
       parameter_map.clear();
 
-      irept assigns_to_add = contract.find(ID_C_spec_assigns);
+      exprt assigns_to_add =
+        static_cast<const exprt &>(contract.find(ID_C_spec_assigns));
       if(assigns_to_add.is_not_nil())
-        new_symbol.type.add(ID_C_spec_assigns) = assigns_to_add;
-      irept requires_to_add = contract.find(ID_C_spec_requires);
+        to_code_with_contract_type(new_symbol.type).assigns() = assigns_to_add;
+      exprt requires_to_add =
+        static_cast<const exprt &>(contract.find(ID_C_spec_requires));
       if(requires_to_add.is_not_nil())
-        new_symbol.type.add(ID_C_spec_requires) = requires_to_add;
-      irept ensures_to_add = contract.find(ID_C_spec_ensures);
+        to_code_with_contract_type(new_symbol.type).requires() =
+          requires_to_add;
+      exprt ensures_to_add =
+        static_cast<const exprt &>(contract.find(ID_C_spec_ensures));
       if(ensures_to_add.is_not_nil())
-        new_symbol.type.add(ID_C_spec_ensures) = ensures_to_add;
+        to_code_with_contract_type(new_symbol.type).ensures() = ensures_to_add;
     }
   }
 }

src/goto-instrument/code_contracts.cpp

@@ -147,12 +147,8 @@ static void check_apply_invariants(
 bool code_contractst::has_contract(const irep_idt fun_name)
 {
   const symbolt &function_symbol = ns.lookup(fun_name);
-  const code_typet &type = to_code_type(function_symbol.type);
-  if(type.find(ID_C_spec_assigns).is_not_nil())
-    return true;
-
-  return type.find(ID_C_spec_requires).is_not_nil() ||
-         type.find(ID_C_spec_ensures).is_not_nil();
+  const auto &type = to_code_with_contract_type(function_symbol.type);
+  return type.has_contract();
 }
 
 bool code_contractst::apply_function_contract(
@@ -171,12 +167,12 @@ bool code_contractst::apply_function_contract(
   // components.
   const irep_idt &function = to_symbol_expr(call.function()).get_identifier();
   const symbolt &function_symbol = ns.lookup(function);
-  const code_typet &type = to_code_type(function_symbol.type);
+  const auto &type = to_code_with_contract_type(function_symbol.type);
 
   // Isolate each component of the contract.
-  exprt assigns = static_cast<const exprt &>(type.find(ID_C_spec_assigns));
-  exprt requires = static_cast<const exprt &>(type.find(ID_C_spec_requires));
-  exprt ensures = static_cast<const exprt &>(type.find(ID_C_spec_ensures));
+  exprt assigns = type.assigns();
+  exprt requires = type.requires();
+  exprt ensures = type.ensures();
 
   // Check to see if the function  contract actually constrains its effect on
   // the program state; if not, return.
@@ -359,9 +355,8 @@ void code_contractst::populate_assigns_references(
   goto_programt &created_decls,
   std::vector<exprt> &created_references)
 {
-  const code_typet &type = to_code_type(function_symbol.type);
-  const exprt &assigns =
-    static_cast<const exprt &>(type.find(ID_C_spec_assigns));
+  const auto &type = to_code_with_contract_type(function_symbol.type);
+  const exprt &assigns = type.assigns();
 
   const exprt::operandst &targets = assigns.operands();
   for(const exprt &curr_op : targets)
@@ -475,7 +470,7 @@ void code_contractst::instrument_call_statement(
     }
 
     exprt called_assigns =
-      static_cast<const exprt &>(called_sym.type.find(ID_C_spec_assigns));
+      to_code_with_contract_type(called_sym.type).assigns();
     if(called_assigns.is_nil()) // Called function has no assigns clause
     {
       // Fail if called function has no assigns clause.
@@ -618,9 +613,9 @@ bool code_contractst::add_pointer_checks(const std::string &function_name)
 
   const irep_idt function_id(function_name);
   const symbolt &function_symbol = ns.lookup(function_id);
-  const code_typet &type = to_code_type(function_symbol.type);
+  const auto &type = to_code_with_contract_type(function_symbol.type);
 
-  exprt assigns = static_cast<const exprt &>(type.find(ID_C_spec_assigns));
+  exprt assigns = type.assigns();
 
   // Return if there are no reference checks to perform.
   if(assigns.is_nil())
@@ -752,14 +747,11 @@ void code_contractst::add_contract_check(
   PRECONDITION(!dest.instructions.empty());
 
   const symbolt &function_symbol = ns.lookup(mangled_fun);
-  const code_typet &code_type = to_code_type(function_symbol.type);
-
-  const exprt &assigns =
-    static_cast<const exprt &>(code_type.find(ID_C_spec_assigns));
-  const exprt &requires =
-    static_cast<const exprt &>(code_type.find(ID_C_spec_requires));
-  const exprt &ensures =
-    static_cast<const exprt &>(code_type.find(ID_C_spec_ensures));
+  const auto &code_type = to_code_with_contract_type(function_symbol.type);
+
+  const exprt &assigns = code_type.assigns();
+  const exprt &requires = code_type.requires();
+  const exprt &ensures = code_type.ensures();
   INVARIANT(
     ensures.is_not_nil() || assigns.is_not_nil(),
     "Code contract enforcement is trivial without an ensures or assigns "

src/util/c_types.h

@@ -327,6 +327,88 @@ inline c_enum_tag_typet &to_c_enum_tag_type(typet &type)
   return static_cast<c_enum_tag_typet &>(type);
 }
 
+class code_with_contract_typet : public code_typet
+{
+public:
+  /// Constructs a new 'code with contract' type, i.e., a function type
+  /// decorated with a function contract.
+  /// \param _parameters: The vector of function parameters.
+  /// \param _return_type: The return type.
+  code_with_contract_typet(parameterst _parameters, typet _return_type)
+    : code_typet(std::move(_parameters), std::move(_return_type))
+  {
+  }
+
+  bool has_contract() const
+  {
+    return assigns().is_not_nil() || requires().is_not_nil() ||
+           ensures().is_not_nil();
+  }
+
+  const exprt &assigns() const
+  {
+    return static_cast<const exprt &>(find(ID_C_spec_assigns));
+  }
+
+  exprt &assigns()
+  {
+    return static_cast<exprt &>(add(ID_C_spec_assigns));
+  }
+
+  const exprt &requires() const
+  {
+    return static_cast<const exprt &>(find(ID_C_spec_requires));
+  }
+
+  exprt &requires()
+  {
+    return static_cast<exprt &>(add(ID_C_spec_requires));
+  }
+
+  const exprt &ensures() const
+  {
+    return static_cast<const exprt &>(find(ID_C_spec_ensures));
+  }
+
+  exprt &ensures()
+  {
+    return static_cast<exprt &>(add(ID_C_spec_ensures));
+  }
+};
+
+/// Check whether a reference to a typet is a \ref code_typet.
+/// \param type: Source type.
+/// \return True if \p type is a \ref code_typet.
+template <>
+inline bool can_cast_type<code_with_contract_typet>(const typet &type)
+{
+  return type.id() == ID_code;
+}
+
+/// \brief Cast a typet to a \ref code_with_contract_typet
+///
+/// This is an unchecked conversion. \a type must be known to be \ref
+/// code_with_contract_typet. Will fail with a precondition violation if type
+/// doesn't match.
+///
+/// \param type: Source type.
+/// \return Object of type \ref code_with_contract_typet.
+inline const code_with_contract_typet &
+to_code_with_contract_type(const typet &type)
+{
+  PRECONDITION(can_cast_type<code_with_contract_typet>(type));
+  code_with_contract_typet::check(type);
+  return static_cast<const code_with_contract_typet &>(type);
+}
+
+/// \copydoc to_code_type(const typet &)
+inline code_with_contract_typet &to_code_with_contract_type(typet &type)
+{
+  PRECONDITION(can_cast_type<code_with_contract_typet>(type));
+  code_with_contract_typet::check(type);
+  return static_cast<code_with_contract_typet &>(type);
+}
+
 bitvector_typet index_type();
 bitvector_typet enum_constant_type();
 signedbv_typet signed_int_type();