Give languaget a private typecheck method

This is to avoid breaking the API while introducing a new parameter,
symbols_to_keep. This parameter will be used in a later commit that will
prevent the typecheck method from stripping out user-requested symbols.

Author: karkhaz

src/ansi-c/ansi_c_language.cpp

@@ -105,7 +105,8 @@ bool ansi_c_languaget::parse(
 
 bool ansi_c_languaget::typecheck(
   symbol_tablet &symbol_table,
-  const std::string &module)
+  const std::string &module,
+  const bool keep_file_local)
 {
   symbol_tablet new_symbol_table;
 

src/ansi-c/ansi_c_language.h

@@ -53,7 +53,19 @@ class ansi_c_languaget:public languaget
 
   bool typecheck(
     symbol_tablet &symbol_table,
-    const std::string &module) override;
+    const std::string &module,
+    const bool keep_file_local) override;
+
+  bool can_keep_file_local() override
+  {
+    return true;
+  }
+
+  bool
+  typecheck(symbol_tablet &symbol_table, const std::string &module) override
+  {
+    return typecheck(symbol_table, module, true);
+  }
 
   void show_parse(std::ostream &out) override;
 

src/langapi/language.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 #include <unordered_set>
 
+#include <util/invariant.h>
 #include <util/message.h>
 #include <util/std_types.h>
 #include <util/symbol.h>
@@ -123,6 +124,32 @@ class languaget:public messaget
     symbol_tablet &symbol_table,
     const std::string &module)=0;
 
+  /// \brief Is it possible to call three-argument typecheck() on this object?
+  virtual bool can_keep_file_local()
+  {
+    return false;
+  }
+
+  /// \brief typecheck without removing specified entries from the symbol table
+  ///
+  /// Some concrete subclasses of \ref languaget discard unused symbols from a
+  /// goto binary as part of typechecking it. This function allows the caller
+  /// to specify a list of symbols that should be kept, even if that language's
+  /// typecheck() implementation would normally discard those symbols.
+  ///
+  /// This function should only be called on objects for which a call to
+  /// can_keep_symbols() returns `true`.
+  virtual bool typecheck(
+    symbol_tablet &symbol_table,
+    const std::string &module,
+    const bool keep_file_local)
+  {
+    INVARIANT(
+      false,
+      "three-argument typecheck should only be called for files written"
+      " in a language that allows file-local symbols, like C");
+  }
+
   // language id / description
 
   virtual std::string id() const = 0;

src/langapi/language_file.cpp

@@ -82,7 +82,9 @@ bool language_filest::parse()
   return false;
 }
 
-bool language_filest::typecheck(symbol_tablet &symbol_table)
+bool language_filest::typecheck(
+  symbol_tablet &symbol_table,
+  const bool keep_file_local)
 {
   // typecheck interfaces
 
@@ -129,8 +131,16 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
   {
     if(file.second.modules.empty())
     {
-      if(file.second.language->typecheck(symbol_table, ""))
-        return true;
+      if(file.second.language->can_keep_file_local())
+      {
+        if(file.second.language->typecheck(symbol_table, "", keep_file_local))
+          return true;
+      }
+      else
+      {
+        if(file.second.language->typecheck(symbol_table, ""))
+          return true;
+      }
       // register lazy methods.
       // TODO: learn about modules and generalise this
       // to module-providing languages if required.
@@ -145,7 +155,7 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
 
   for(auto &module : module_map)
   {
-    if(typecheck_module(symbol_table, module.second))
+    if(typecheck_module(symbol_table, module.second, keep_file_local))
       return true;
   }
 
@@ -195,7 +205,8 @@ bool language_filest::interfaces(
 
 bool language_filest::typecheck_module(
   symbol_tablet &symbol_table,
-  const std::string &module)
+  const std::string &module,
+  const bool keep_file_local)
 {
   // check module map
 
@@ -207,12 +218,13 @@ bool language_filest::typecheck_module(
     return true;
   }
 
-  return typecheck_module(symbol_table, it->second);
+  return typecheck_module(symbol_table, it->second, keep_file_local);
 }
 
 bool language_filest::typecheck_module(
   symbol_tablet &symbol_table,
-  language_modulet &module)
+  language_modulet &module,
+  const bool keep_file_local)
 {
   // already typechecked?
 
@@ -240,23 +252,29 @@ bool language_filest::typecheck_module(
       it!=dependency_set.end();
       it++)
   {
-    if(typecheck_module(symbol_table, *it))
-    {
-      module.in_progress=false;
+    module.in_progress = !typecheck_module(symbol_table, *it, keep_file_local);
+    if(module.in_progress == false)
       return true;
-    }
   }
 
   // type check it
 
   status() << "Type-checking " << module.name << eom;
 
-  if(module.file->language->typecheck(symbol_table, module.name))
+  if(module.file->language->can_keep_file_local())
   {
-    module.in_progress = false;
-    return true;
+    module.in_progress = !module.file->language->typecheck(
+      symbol_table, module.name, keep_file_local);
+  }
+  else
+  {
+    module.in_progress =
+      !module.file->language->typecheck(symbol_table, module.name);
   }
 
+  if(!module.in_progress)
+    return true;
+
   module.type_checked=true;
   module.in_progress=false;
 

src/langapi/language_file.h

@@ -107,7 +107,8 @@ class language_filest:public messaget
 
   bool generate_support_functions(symbol_tablet &symbol_table);
 
-  bool typecheck(symbol_tablet &symbol_table);
+  bool
+  typecheck(symbol_tablet &symbol_table, const bool keep_file_local = false);
 
   bool final(symbol_table_baset &symbol_table);
 
@@ -141,11 +142,13 @@ class language_filest:public messaget
 protected:
   bool typecheck_module(
     symbol_tablet &symbol_table,
-    language_modulet &module);
+    language_modulet &module,
+    const bool keep_file_local);
 
   bool typecheck_module(
     symbol_tablet &symbol_table,
-    const std::string &module);
+    const std::string &module,
+    const bool keep_file_local);
 };
 
 #endif // CPROVER_UTIL_LANGUAGE_FILE_H