Merge pull request #5587 from tautschnig/messaget-language_filest

kroening · web-flow · commit 098ec1ebe668 · 2022-12-16T10:26:58.000Z
language_filest is not a messaget
diff --git a/jbmc/src/java_bytecode/lazy_goto_functions_map.h b/jbmc/src/java_bytecode/lazy_goto_functions_map.h
@@ -173,7 +173,8 @@ class lazy_goto_functions_mapt final
     symbol_table_baset &function_symbol_table) const
   {
     // Fill in symbol table entry body if not already done
-    language_files.convert_lazy_method(name, function_symbol_table);
+    language_files.convert_lazy_method(
+      name, function_symbol_table, message_handler);
 
     underlying_mapt::iterator it = goto_functions.find(name);
     if(it != goto_functions.end())
diff --git a/jbmc/src/java_bytecode/lazy_goto_model.cpp b/jbmc/src/java_bytecode/lazy_goto_model.cpp
@@ -57,7 +57,6 @@ lazy_goto_modelt::lazy_goto_modelt(
       driver_program_generate_function_body),
     message_handler(message_handler)
 {
-  language_files.set_message_handler(message_handler);
 }
 
 lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
@@ -154,7 +153,7 @@ void lazy_goto_modelt::initialize(
 
     msg.status() << "Converting" << messaget::eom;
 
-    if(language_files.typecheck(symbol_table))
+    if(language_files.typecheck(symbol_table, message_handler))
     {
       throw invalid_input_exceptiont("CONVERSION ERROR");
     }
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
@@ -620,14 +620,14 @@ bool compilet::write_bin_object_file(
 optionalt<symbol_tablet> compilet::parse_source(const std::string &file_name)
 {
   language_filest language_files;
-  language_files.set_message_handler(log.get_message_handler());
 
   if(parse(file_name, language_files))
     return {};
 
   // we just typecheck one file here
   symbol_tablet file_symbol_table;
-  if(language_files.typecheck(file_symbol_table, keep_file_local))
+  if(language_files.typecheck(
+       file_symbol_table, keep_file_local, log.get_message_handler()))
   {
     log.error() << "CONVERSION ERROR" << messaget::eom;
     return {};
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
@@ -111,7 +111,7 @@ void initialize_from_source_files(
 
     msg.status() << "Converting" << messaget::eom;
 
-    if(language_files.typecheck(symbol_table))
+    if(language_files.typecheck(symbol_table, message_handler))
     {
       throw invalid_input_exceptiont("CONVERSION ERROR");
     }
@@ -203,10 +203,7 @@ goto_modelt initialize_goto_model(
   }
 
   language_filest language_files;
-  language_files.set_message_handler(message_handler);
-
   goto_modelt goto_model;
-
   initialize_from_source_files(
     sources, options, language_files, goto_model.symbol_table, message_handler);
 
diff --git a/src/langapi/language_file.cpp b/src/langapi/language_file.cpp
@@ -48,8 +48,10 @@ void language_filest::show_parse(std::ostream &out)
     file.second.language->show_parse(out);
 }
 
-bool language_filest::parse()
+bool language_filest::parse(message_handlert &message_handler)
 {
+  messaget log(message_handler);
+
   for(auto &file : file_map)
   {
     // open file
@@ -58,7 +60,7 @@ bool language_filest::parse()
 
     if(!infile)
     {
-      error() << "Failed to open " << file.first << eom;
+      log.error() << "Failed to open " << file.first << messaget::eom;
       return true;
     }
 
@@ -68,7 +70,7 @@ bool language_filest::parse()
 
     if(language.parse(infile, file.first))
     {
-      error() << "Parsing of " << file.first << " failed" << eom;
+      log.error() << "Parsing of " << file.first << " failed" << messaget::eom;
       return true;
     }
 
@@ -82,7 +84,8 @@ bool language_filest::parse()
 
 bool language_filest::typecheck(
   symbol_table_baset &symbol_table,
-  const bool keep_file_local)
+  const bool keep_file_local,
+  message_handlert &message_handler)
 {
   // typecheck interfaces
 
@@ -153,7 +156,8 @@ bool language_filest::typecheck(
 
   for(auto &module : module_map)
   {
-    if(typecheck_module(symbol_table, module.second, keep_file_local))
+    if(typecheck_module(
+         symbol_table, module.second, keep_file_local, message_handler))
       return true;
   }
 
@@ -203,36 +207,43 @@ bool language_filest::interfaces(symbol_table_baset &symbol_table)
 bool language_filest::typecheck_module(
   symbol_table_baset &symbol_table,
   const std::string &module,
-  const bool keep_file_local)
+  const bool keep_file_local,
+  message_handlert &message_handler)
 {
   // check module map
 
   module_mapt::iterator it=module_map.find(module);
 
   if(it==module_map.end())
   {
-    error() << "found no file that provides module " << module << eom;
+    messaget log(message_handler);
+    log.error() << "found no file that provides module " << module
+                << messaget::eom;
     return true;
   }
 
-  return typecheck_module(symbol_table, it->second, keep_file_local);
+  return typecheck_module(
+    symbol_table, it->second, keep_file_local, message_handler);
 }
 
 bool language_filest::typecheck_module(
   symbol_table_baset &symbol_table,
   language_modulet &module,
-  const bool keep_file_local)
+  const bool keep_file_local,
+  message_handlert &message_handler)
 {
   // already typechecked?
 
   if(module.type_checked)
     return false;
 
+  messaget log(message_handler);
+
   // already in progress?
 
   if(module.in_progress)
   {
-    error() << "circular dependency in " << module.name << eom;
+    log.error() << "circular dependency in " << module.name << messaget::eom;
     return true;
   }
 
@@ -249,14 +260,15 @@ bool language_filest::typecheck_module(
       it!=dependency_set.end();
       it++)
   {
-    module.in_progress = !typecheck_module(symbol_table, *it, keep_file_local);
+    module.in_progress =
+      !typecheck_module(symbol_table, *it, keep_file_local, message_handler);
     if(module.in_progress == false)
       return true;
   }
 
   // type check it
 
-  status() << "Type-checking " << module.name << eom;
+  log.status() << "Type-checking " << module.name << messaget::eom;
 
   if(module.file->language->can_keep_file_local())
   {
diff --git a/src/langapi/language_file.h b/src/langapi/language_file.h
@@ -17,9 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <string>
 #include <unordered_set>
 
-#include <util/message.h>
 #include <util/symbol_table_base.h>
 
+class message_handlert;
 class language_filet;
 class languaget;
 
@@ -58,7 +58,7 @@ class language_filet final
   ~language_filet();
 };
 
-class language_filest:public messaget
+class language_filest
 {
 private:
   typedef std::map<std::string, language_filet> file_mapt;
@@ -101,15 +101,23 @@ class language_filest:public messaget
     file_map.clear();
   }
 
-  bool parse();
+  bool parse(message_handlert &message_handler);
 
   void show_parse(std::ostream &out);
 
   bool generate_support_functions(symbol_table_baset &symbol_table);
 
-  bool typecheck(
+  bool
+
+  typecheck(
     symbol_table_baset &symbol_table,
-    const bool keep_file_local = false);
+    const bool keep_file_local,
+    message_handlert &message_handler);
+  bool
+  typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler)
+  {
+    return typecheck(symbol_table, false, message_handler);
+  }
 
   bool final(symbol_table_baset &symbol_table);
 
@@ -120,7 +128,8 @@ class language_filest:public messaget
   // for this to be legal.
   void convert_lazy_method(
     const irep_idt &id,
-    symbol_table_baset &symbol_table)
+    symbol_table_baset &symbol_table,
+    message_handlert &message_handler)
   {
     PRECONDITION(symbol_table.has_symbol(id));
     lazy_method_mapt::iterator it=lazy_method_map.find(id);
@@ -144,12 +153,14 @@ class language_filest:public messaget
   bool typecheck_module(
     symbol_table_baset &symbol_table,
     language_modulet &module,
-    const bool keep_file_local);
+    const bool keep_file_local,
+    message_handlert &message_handler);
 
   bool typecheck_module(
     symbol_table_baset &symbol_table,
     const std::string &module,
-    const bool keep_file_local);
+    const bool keep_file_local,
+    message_handlert &message_handler);
 };
 
 #endif // CPROVER_UTIL_LANGUAGE_FILE_H
diff --git a/unit/testing-utils/get_goto_model_from_c.cpp b/unit/testing-utils/get_goto_model_from_c.cpp
@@ -44,7 +44,6 @@ goto_modelt get_goto_model_from_c(std::istream &in)
   }
 
   language_filest language_files;
-  language_files.set_message_handler(null_message_handler);
 
   language_filet &language_file = language_files.add_file("");
 
@@ -66,7 +65,8 @@ goto_modelt get_goto_model_from_c(std::istream &in)
   goto_modelt goto_model;
 
   {
-    const bool error = language_files.typecheck(goto_model.symbol_table);
+    const bool error =
+      language_files.typecheck(goto_model.symbol_table, null_message_handler);
 
     if(error)
       throw invalid_input_exceptiont("typechecking failed");

Original file line number	Diff line number	Diff line change
`@@ -173,7 +173,8 @@ class lazy_goto_functions_mapt final`
`173`	`173`	`symbol_table_baset &function_symbol_table) const`
`174`	`174`	`{`
`175`	`175`	`// Fill in symbol table entry body if not already done`
`176`		`- language_files.convert_lazy_method(name, function_symbol_table);`
	`176`	`+ language_files.convert_lazy_method(`
	`177`	`+ name, function_symbol_table, message_handler);`
`177`	`178`
`178`	`179`	`underlying_mapt::iterator it = goto_functions.find(name);`
`179`	`180`	`if(it != goto_functions.end())`
Original file line number	Diff line number	Diff line change
`@@ -57,7 +57,6 @@ lazy_goto_modelt::lazy_goto_modelt(`
`57`	`57`	`driver_program_generate_function_body),`
`58`	`58`	`message_handler(message_handler)`
`59`	`59`	`{`
`60`		`- language_files.set_message_handler(message_handler);`
`61`	`60`	`}`
`62`	`61`
`63`	`62`	`lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)`
`@@ -154,7 +153,7 @@ void lazy_goto_modelt::initialize(`
`154`	`153`
`155`	`154`	`msg.status() << "Converting" << messaget::eom;`
`156`	`155`
`157`		`- if(language_files.typecheck(symbol_table))`
	`156`	`+ if(language_files.typecheck(symbol_table, message_handler))`
`158`	`157`	`{`
`159`	`158`	`throw invalid_input_exceptiont("CONVERSION ERROR");`
`160`	`159`	`}`
Original file line number	Diff line number	Diff line change
`@@ -111,7 +111,7 @@ void initialize_from_source_files(`
`111`	`111`
`112`	`112`	`msg.status() << "Converting" << messaget::eom;`
`113`	`113`
`114`		`- if(language_files.typecheck(symbol_table))`
	`114`	`+ if(language_files.typecheck(symbol_table, message_handler))`
`115`	`115`	`{`
`116`	`116`	`throw invalid_input_exceptiont("CONVERSION ERROR");`
`117`	`117`	`}`
`@@ -203,10 +203,7 @@ goto_modelt initialize_goto_model(`
`203`	`203`	`}`
`204`	`204`
`205`	`205`	`language_filest language_files;`
`206`		`- language_files.set_message_handler(message_handler);`
`207`		`-`
`208`	`206`	`goto_modelt goto_model;`
`209`		`-`
`210`	`207`	`initialize_from_source_files(`
`211`	`208`	`sources, options, language_files, goto_model.symbol_table, message_handler);`
`212`	`209`
Original file line number	Diff line number	Diff line change
`@@ -48,8 +48,10 @@ void language_filest::show_parse(std::ostream &out)`
`48`	`48`	`file.second.language->show_parse(out);`
`49`	`49`	`}`
`50`	`50`
`51`		`-bool language_filest::parse()`
	`51`	`+bool language_filest::parse(message_handlert &message_handler)`
`52`	`52`	`{`
	`53`	`+ messaget log(message_handler);`
	`54`	`+`
`53`	`55`	`for(auto &file : file_map)`
`54`	`56`	`{`
`55`	`57`	`// open file`
`@@ -58,7 +60,7 @@ bool language_filest::parse()`
`58`	`60`
`59`	`61`	`if(!infile)`
`60`	`62`	`{`
`61`		`- error() << "Failed to open " << file.first << eom;`
	`63`	`+ log.error() << "Failed to open " << file.first << messaget::eom;`
`62`	`64`	`return true;`
`63`	`65`	`}`
`64`	`66`
`@@ -68,7 +70,7 @@ bool language_filest::parse()`
`68`	`70`
`69`	`71`	`if(language.parse(infile, file.first))`
`70`	`72`	`{`
`71`		`- error() << "Parsing of " << file.first << " failed" << eom;`
	`73`	`+ log.error() << "Parsing of " << file.first << " failed" << messaget::eom;`
`72`	`74`	`return true;`
`73`	`75`	`}`
`74`	`76`
`@@ -82,7 +84,8 @@ bool language_filest::parse()`
`82`	`84`
`83`	`85`	`bool language_filest::typecheck(`
`84`	`86`	`symbol_table_baset &symbol_table,`
`85`		`- const bool keep_file_local)`
	`87`	`+ const bool keep_file_local,`
	`88`	`+ message_handlert &message_handler)`
`86`	`89`	`{`
`87`	`90`	`// typecheck interfaces`
`88`	`91`
`@@ -153,7 +156,8 @@ bool language_filest::typecheck(`
`153`	`156`
`154`	`157`	`for(auto &module : module_map)`
`155`	`158`	`{`
`156`		`- if(typecheck_module(symbol_table, module.second, keep_file_local))`
	`159`	`+ if(typecheck_module(`
	`160`	`+ symbol_table, module.second, keep_file_local, message_handler))`
`157`	`161`	`return true;`
`158`	`162`	`}`
`159`	`163`
`@@ -203,36 +207,43 @@ bool language_filest::interfaces(symbol_table_baset &symbol_table)`
`203`	`207`	`bool language_filest::typecheck_module(`
`204`	`208`	`symbol_table_baset &symbol_table,`
`205`	`209`	`const std::string &module,`
`206`		`- const bool keep_file_local)`
	`210`	`+ const bool keep_file_local,`
	`211`	`+ message_handlert &message_handler)`
`207`	`212`	`{`
`208`	`213`	`// check module map`
`209`	`214`
`210`	`215`	`module_mapt::iterator it=module_map.find(module);`
`211`	`216`
`212`	`217`	`if(it==module_map.end())`
`213`	`218`	`{`
`214`		`- error() << "found no file that provides module " << module << eom;`
	`219`	`+ messaget log(message_handler);`
	`220`	`+ log.error() << "found no file that provides module " << module`
	`221`	`+ << messaget::eom;`
`215`	`222`	`return true;`
`216`	`223`	`}`
`217`	`224`
`218`		`- return typecheck_module(symbol_table, it->second, keep_file_local);`
	`225`	`+ return typecheck_module(`
	`226`	`+ symbol_table, it->second, keep_file_local, message_handler);`
`219`	`227`	`}`
`220`	`228`
`221`	`229`	`bool language_filest::typecheck_module(`
`222`	`230`	`symbol_table_baset &symbol_table,`
`223`	`231`	`language_modulet &module,`
`224`		`- const bool keep_file_local)`
	`232`	`+ const bool keep_file_local,`
	`233`	`+ message_handlert &message_handler)`
`225`	`234`	`{`
`226`	`235`	`// already typechecked?`
`227`	`236`
`228`	`237`	`if(module.type_checked)`
`229`	`238`	`return false;`
`230`	`239`
	`240`	`+ messaget log(message_handler);`
	`241`	`+`
`231`	`242`	`// already in progress?`
`232`	`243`
`233`	`244`	`if(module.in_progress)`
`234`	`245`	`{`
`235`		`- error() << "circular dependency in " << module.name << eom;`
	`246`	`+ log.error() << "circular dependency in " << module.name << messaget::eom;`
`236`	`247`	`return true;`
`237`	`248`	`}`
`238`	`249`
`@@ -249,14 +260,15 @@ bool language_filest::typecheck_module(`
`249`	`260`	`it!=dependency_set.end();`
`250`	`261`	`it++)`
`251`	`262`	`{`
`252`		`- module.in_progress = !typecheck_module(symbol_table, *it, keep_file_local);`
	`263`	`+ module.in_progress =`
	`264`	`+ !typecheck_module(symbol_table, *it, keep_file_local, message_handler);`
`253`	`265`	`if(module.in_progress == false)`
`254`	`266`	`return true;`
`255`	`267`	`}`
`256`	`268`
`257`	`269`	`// type check it`
`258`	`270`
`259`		`- status() << "Type-checking " << module.name << eom;`
	`271`	`+ log.status() << "Type-checking " << module.name << messaget::eom;`
`260`	`272`
`261`	`273`	`if(module.file->language->can_keep_file_local())`
`262`	`274`	`{`
Original file line number	Diff line number	Diff line change
`@@ -44,7 +44,6 @@ goto_modelt get_goto_model_from_c(std::istream &in)`
`44`	`44`	`}`
`45`	`45`
`46`	`46`	`language_filest language_files;`
`47`		`- language_files.set_message_handler(null_message_handler);`
`48`	`47`
`49`	`48`	`language_filet &language_file = language_files.add_file("");`
`50`	`49`
`@@ -66,7 +65,8 @@ goto_modelt get_goto_model_from_c(std::istream &in)`
`66`	`65`	`goto_modelt goto_model;`
`67`	`66`
`68`	`67`	`{`
`69`		`- const bool error = language_files.typecheck(goto_model.symbol_table);`
	`68`	`+ const bool error =`
	`69`	`+ language_files.typecheck(goto_model.symbol_table, null_message_handler);`
`70`	`70`
`71`	`71`	`if(error)`
`72`	`72`	`throw invalid_input_exceptiont("typechecking failed");`