C Support Changes

regression/.gitignore

@@ -0,0 +1 @@
+tests.log

src/ansi-c/ansi_c_language.cpp

@@ -196,6 +196,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/expr2c.cpp

@@ -518,28 +518,40 @@ std::string expr2ct::convert_rec(
   }
   else if(src.id()==ID_symbol)
   {
-    const typet &followed=ns.follow(src);
+    symbol_typet symbolic_type=to_symbol_type(src);
+    const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);
 
-    if(followed.id()==ID_struct)
+    // Providing we have a valid identifer, we can just use that rather than
+    // trying to find the concrete type
+    if(typedef_identifer!="")
     {
-      std::string dest=q+"struct";
-      const irep_idt &tag=to_struct_type(followed).get_tag();
-      if(tag!="")
-        dest+=" "+id2string(tag);
-      dest+=d;
-      return dest;
+      return q+id2string(typedef_identifer)+d;
     }
-    else if(followed.id()==ID_union)
+    else
     {
-      std::string dest=q+"union";
-      const irep_idt &tag=to_union_type(followed).get_tag();
-      if(tag!="")
-        dest+=" "+id2string(tag);
-      dest+=d;
-      return dest;
+      const typet &followed=ns.follow(src);
+
+      if(followed.id()==ID_struct)
+      {
+        std::string dest=q+"struct";
+        const irep_idt &tag=to_struct_type(followed).get_tag();
+        if(tag!="")
+          dest+=" "+id2string(tag);
+        dest+=d;
+        return dest;
+      }
+      else if(followed.id()==ID_union)
+      {
+        std::string dest=q+"union";
+        const irep_idt &tag=to_union_type(followed).get_tag();
+        if(tag!="")
+          dest+=" "+id2string(tag);
+        dest+=d;
+        return dest;
+      }
+      else
+        return convert_rec(followed, new_qualifiers, declarator);
     }
-    else
-      return convert_rec(followed, new_qualifiers, declarator);
   }
   else if(src.id()==ID_struct_tag)
   {

src/langapi/language_ui.cpp

@@ -183,6 +183,10 @@ bool language_uit::final()
 {
   language_files.set_message_handler(*message_handler);
 
+  // Enable/disable stub generation for opaque methods
+  bool stubs_enabled=_cmdline.isset("generate-opaque-stubs");
+  language_files.set_should_generate_opaque_method_stubs(stubs_enabled);
+
   if(language_files.final(symbol_table))
   {
     if(get_ui()==ui_message_handlert::PLAIN)

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,209 @@ bool languaget::type_to_name(
   name=type.pretty();
   return false;
 }
+
+/*******************************************************************\
+
+Function: languaget::set_should_generate_opaque_method_stubs
+
+  Inputs:
+          should_generate_stubs - Should stub generation be enabled
+
+ Outputs:
+
+ Purpose: Turn on or off stub generation.
+
+\*******************************************************************/
+void languaget::set_should_generate_opaque_method_stubs(
+  bool should_generate_stubs)
+{
+  generate_opaque_stubs=should_generate_stubs;
+}
+
+/*******************************************************************\
+
+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. This will only happen if
+          generate_opaque_stubs is enabled.
+
+\*******************************************************************/
+
+void languaget::generate_opaque_method_stubs(symbol_tablet &symbol_table)
+{
+  if(generate_opaque_stubs)
+  {
+    system_symbols=system_library_symbolst();
+
+    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)
+{
+  std::set<std::string> headers;
+  // Don't create stubs for symbols like:
+  // __CPROVER_blah (which aren't real external functions)
+  // and strstr (which we will model for ourselves later)
+  bool is_internal=system_symbols.is_symbol_internal_symbol(symbol, headers);
+
+  return !symbol.is_type &&
+    symbol.value.id()==ID_nil &&
+    symbol.type.id()==ID_code &&
+    !is_internal;
+}
+
+/*******************************************************************\
+
+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,9 @@ Author: Daniel Kroening, [email protected]
 #include <set>
 #include <iosfwd>
 #include <string>
+#include <util/symbol.h>
+#include <util/std_types.h>
+#include <goto-programs/system_library_symbols.h>
 
 #include "message.h"
 
@@ -110,9 +113,34 @@ class languaget:public messaget
 
   virtual languaget *new_language()=0;
 
+  void set_should_generate_opaque_method_stubs(bool should_generate_stubs);
+
   // constructor / destructor
 
   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);
+
+  bool generate_opaque_stubs;
+
+private:
+  bool is_symbol_opaque_function(const symbolt &symbol);
+  void generate_opaque_parameter_symbols(
+    symbolt &function_symbol,
+    symbol_tablet &symbol_table);
+
+  system_library_symbolst system_symbols;
 };
 #endif // CPROVER_UTIL_LANGUAGE_H

src/util/language_file.cpp

@@ -93,6 +93,28 @@ void language_filest::show_parse(std::ostream &out)
 
 /*******************************************************************\
 
+Function: language_filest::set_should_generate_opqaue_method_stubs
+
+  Inputs:
+          should_generate_stubs - Should stub generation be enabled
+
+ Outputs:
+
+ Purpose: Turn on or off stub generation for all the languages
+
+\*******************************************************************/
+
+void language_filest::set_should_generate_opaque_method_stubs(
+  bool stubs_enabled)
+{
+  for(file_mapt::value_type &language_file_entry : file_map)
+  {
+    languaget *language=language_file_entry.second.language;
+    language->set_should_generate_opaque_method_stubs(stubs_enabled);
+  }
+}
+
+/*******************************************************************\
 Function: language_filest::parse
 
   Inputs:

src/util/language_file.h

@@ -75,6 +75,8 @@ class language_filest:public messaget
     file_map.clear();
   }
 
+  void set_should_generate_opaque_method_stubs(bool stubs_enabled);
+
   bool parse();
 
   void show_parse(std::ostream &out);