Merge pull request diffblue#5 from thk123/feature/c-opaque-method-stubs

Implementing getting the method stub generation for C

Author: peterschrammel

src/ansi-c/ansi_c_language.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_util.h>
 #include <util/config.h>
 #include <util/get_base_name.h>
+#include <util/symbol.h>
 
 #include <linking/linking.h>
 #include <linking/remove_internal_symbols.h>
@@ -65,6 +66,103 @@ void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
 
 /*******************************************************************\
 
+Function: ansi_c_languaget::generate_opaque_stub_body
+
+  Inputs:
+          symbol - the function symbol which is opaque
+          symbol_table - the symbol table
+
+ Outputs: The identifier of the return variable. ID_nil if the function
+          doesn't return anything.
+
+ Purpose: To generate the stub function for the opaque function in
+          question. The identifier is used in the flag to the interpreter
+          that the function is opaque. In C, providing the function returns
+          something, the id will be to_return_function_name.
+          The GOTO code will simply create a NONDET instruction as the
+          return value.
+
+\*******************************************************************/
+
+irep_idt ansi_c_languaget::generate_opaque_stub_body(
+  symbolt &symbol,
+  symbol_tablet &symbol_table)
+{
+  code_blockt new_instructions;
+  code_typet &function_type=to_code_type(symbol.type);
+  const typet &return_type=function_type.return_type();
+
+  if(return_type.id()!=ID_nil)
+  {
+    // Build an auxillary symbol to store the return value for
+    // this function
+    auxiliary_symbolt return_symbol;
+    return_symbol.name=get_stub_return_symbol_name(symbol.name);
+    return_symbol.base_name=return_symbol.name;
+    return_symbol.mode=ID_C;
+    return_symbol.type=return_type;
+
+    // Put this symbol into the symbol table
+    symbolt *symbol_ptr=nullptr;
+    symbol_table.move(return_symbol, symbol_ptr);
+    assert(symbol_ptr);
+
+    // Assign a NONDET expression to the temporary symbol
+    symbol_exprt temp_return_symbol(symbol_ptr->name, return_type);
+    exprt return_symbol_expr=side_effect_expr_nondett(return_type);
+    code_declt temp_return_decl(temp_return_symbol);
+    temp_return_decl.copy_to_operands(return_symbol_expr);
+
+    // Add the temporary symbol declaration and the return expression
+    // to the body for the stubbed function
+    new_instructions.copy_to_operands(temp_return_decl);
+    new_instructions.copy_to_operands(code_returnt(temp_return_symbol));
+    symbol.value=new_instructions;
+    return symbol_ptr->name;
+  }
+
+  return ID_nil;
+}
+
+/*******************************************************************\
+
+Function: ansi_c_languaget::build_stub_parameter_symbol
+
+  Inputs:
+          function_symbol - the symbol of an opaque function
+          parameter_index - the index of the parameter within the
+                            the parameter list
+          parameter_type - the type of the parameter
+
+ Outputs: A named symbol to be added to the symbol table representing
+          one of the parameters in this opaque function.
+
+ Purpose: To build the parameter symbol and choose its name. For C
+          we do not have to worry about this pointers so can just
+          name the parameters according to index.
+          Builds a parameter with name stub_ignored_arg0,...
+
+\*******************************************************************/
+
+parameter_symbolt ansi_c_languaget::build_stub_parameter_symbol(
+  const symbolt &function_symbol,
+  size_t parameter_index,
+  const code_typet::parametert &parameter)
+{
+  irep_idt base_name="stub_ignored_arg"+i2string(parameter_index);
+  irep_idt identifier=id2string(function_symbol.name)+"::"+id2string(base_name);
+
+  parameter_symbolt parameter_symbol;
+  parameter_symbol.base_name=base_name;
+  parameter_symbol.mode=ID_C;
+  parameter_symbol.name=identifier;
+  parameter_symbol.type=parameter.type();
+
+  return parameter_symbol;
+}
+
+/*******************************************************************\
+
 Function: ansi_c_languaget::preprocess
 
   Inputs:
@@ -194,6 +292,8 @@ Function: ansi_c_languaget::final
 
 bool ansi_c_languaget::final(symbol_tablet &symbol_table)
 {
+  generate_opaque_method_stubs(symbol_table);
+
   if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
     return true;
 

src/ansi-c/ansi_c_language.h

@@ -15,6 +15,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "ansi_c_parse_tree.h"
 
+class symbolt;
+class symbol_tablet;
+
 /*! \brief TO_BE_DOCUMENTED
     \ingroup gr_ansi_c
 */
@@ -73,6 +76,15 @@ class ansi_c_languaget:public languaget
   void modules_provided(std::set<std::string> &modules) override;
 
 protected:
+  virtual irep_idt generate_opaque_stub_body(
+    symbolt &symbol,
+    symbol_tablet &symbol_table) override;
+
+  virtual parameter_symbolt build_stub_parameter_symbol(
+    const symbolt &function_symbol,
+    size_t parameter_index,
+    const code_typet::parametert &parameter) override;
+
   ansi_c_parse_treet parse_tree;
   std::string parse_path;
 };

src/util/language.cpp

@@ -8,6 +8,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "language.h"
 #include "expr.h"
+#include <util/symbol.h>
+#include <util/symbol_table.h>
+#include <util/prefix.h>
+#include <util/cprover_prefix.h>
+#include <util/std_types.h>
 
 /*******************************************************************\
 
@@ -125,3 +130,183 @@ bool languaget::type_to_name(
   name=type.pretty();
   return false;
 }
+
+/*******************************************************************\
+
+Function: languaget::generate_opaque_method_stubs
+
+  Inputs:
+          symbol_table - the symbol table for the program
+
+ Outputs:
+
+ Purpose: When there are opaque methods (e.g. ones where we don't
+          have a body), we create a stub function in the goto
+          program and mark it as opaque so the interpreter fills in
+          appropriate values for it.
+
+\*******************************************************************/
+
+void languaget::generate_opaque_method_stubs(symbol_tablet &symbol_table)
+{
+  for(auto &symbol_entry : symbol_table.symbols)
+  {
+    if(is_symbol_opaque_function(symbol_entry.second))
+    {
+      symbolt &symbol=symbol_entry.second;
+
+      generate_opaque_parameter_symbols(symbol, symbol_table);
+
+      irep_idt return_symbol_id = generate_opaque_stub_body(
+        symbol,
+        symbol_table);
+
+      if(return_symbol_id!=ID_nil)
+      {
+        symbol.type.set("opaque_method_capture_symbol", return_symbol_id);
+      }
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: languaget::generate_opaque_stub_body
+
+  Inputs:
+          symbol - the function symbol which is opaque
+          symbol_table - the symbol table
+
+ Outputs: The identifier of the return variable. ID_nil if the function
+          doesn't return anything.
+
+ Purpose: To generate the stub function for the opaque function in
+          question. The identifier is used in the flag to the interpreter
+          that the function is opaque. This function should be implemented
+          in the languages.
+
+\*******************************************************************/
+
+irep_idt languaget::generate_opaque_stub_body(
+  symbolt &symbol,
+  symbol_tablet &symbol_table)
+{
+  return ID_nil;
+}
+
+/*******************************************************************\
+
+Function: languaget::build_stub_parameter_symbol
+
+  Inputs:
+          function_symbol - the symbol of an opaque function
+          parameter_index - the index of the parameter within the
+                            the parameter list
+          parameter_type - the type of the parameter
+
+ Outputs: A named symbol to be added to the symbol table representing
+          one of the parameters in this opaque function.
+
+ Purpose: To build the parameter symbol and choose its name. This should
+          be implemented in each language.
+
+\*******************************************************************/
+
+parameter_symbolt languaget::build_stub_parameter_symbol(
+  const symbolt &function_symbol,
+  size_t parameter_index,
+  const code_typet::parametert &parameter)
+{
+  error() << "language " << id()
+          << " doesn't implement build_stub_parameter_symbol. "
+          << "This means cannot use opaque functions." << eom;
+
+  return parameter_symbolt();
+}
+
+/*******************************************************************\
+
+Function: languaget::get_stub_return_symbol_name
+
+  Inputs:
+          function_id - the function that has a return value
+
+ Outputs: the identifier to use for the symbol that will store the
+          return value of this function.
+
+ Purpose: To get the name of the symbol to be used for the return value
+          of the function. Generates a name like to_return_function_name
+
+\*******************************************************************/
+
+irep_idt languaget::get_stub_return_symbol_name(const irep_idt &function_id)
+{
+  std::ostringstream return_symbol_name_builder;
+  return_symbol_name_builder << "to_return_" << function_id;
+  return return_symbol_name_builder.str();
+}
+
+
+/*******************************************************************\
+
+Function: languaget::is_symbol_opaque_function
+
+  Inputs:
+          symbol - the symbol to be checked
+
+ Outputs: True if the symbol is an opaque (e.g. non-bodied) function
+
+ Purpose: To identify if a given symbol is an opaque function and
+          hence needs to be stubbed. We explicitly exclude CPROVER
+          functions, if they have no body it is because we haven't
+          generated it yet.
+
+\*******************************************************************/
+
+bool languaget::is_symbol_opaque_function(const symbolt &symbol)
+{
+  // Explictly exclude CPROVER functions since these aren't opaque
+  std::string variable_id_str(symbol.name.c_str());
+  bool is_cprover_function = has_prefix(variable_id_str, CPROVER_PREFIX);
+
+  return !symbol.is_type &&
+    symbol.value.id()==ID_nil &&
+    symbol.type.id()==ID_code &&
+    !is_cprover_function;
+}
+
+/*******************************************************************\
+
+Function: languaget::generate_opaque_parameter_symbols
+
+  Inputs:
+          function_symbol - the symbol of an opaque function
+          symbol_table - the symbol table to add the new parameter
+                         symbols into
+
+ Outputs:
+
+ Purpose: To create stub parameter symbols for each parameter the
+          function has and assign their IDs into the parameters
+          identifier.
+
+\*******************************************************************/
+
+void languaget::generate_opaque_parameter_symbols(
+  symbolt &function_symbol,
+  symbol_tablet &symbol_table)
+{
+  code_typet &function_type = to_code_type(function_symbol.type);
+  code_typet::parameterst &parameters=function_type.parameters();
+  for(std::size_t i=0; i<parameters.size(); ++i)
+  {
+    code_typet::parametert &param=parameters[i];
+    const parameter_symbolt &param_symbol=
+      build_stub_parameter_symbol(function_symbol, i, param);
+
+    param.set_base_name(param_symbol.base_name);
+    param.set_identifier(param_symbol.name);
+
+    symbol_table.add(param_symbol);
+  }
+}

src/util/language.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 #include <set>
 #include <iosfwd>
 #include <string>
+#include <util/symbol.h>
+#include <util/std_types.h>
 
 #include "message.h"
 
@@ -101,5 +103,24 @@ class languaget:public messaget
 
   languaget() { }
   virtual ~languaget() { }
+
+protected:
+  void generate_opaque_method_stubs(symbol_tablet &symbol_table);
+  virtual irep_idt generate_opaque_stub_body(
+    symbolt &symbol,
+    symbol_tablet &symbol_table);
+
+  virtual parameter_symbolt build_stub_parameter_symbol(
+    const symbolt &function_symbol,
+    size_t parameter_index,
+    const code_typet::parametert &parameter);
+
+  static irep_idt get_stub_return_symbol_name(const irep_idt &function_id);
+
+private:
+  bool is_symbol_opaque_function(const symbolt &symbol);
+  void generate_opaque_parameter_symbols(
+    symbolt &function_symbol,
+    symbol_tablet &symbol_table);
 };
 #endif // CPROVER_UTIL_LANGUAGE_H