language_filest is not a messaget

tautschnig · tautschnig · commit 542ac3ae7400 · 2021-05-07T12:58:14.000Z
Pass a message handler as an argument to several of its functions, but do not
construct a messaget object without a configured message handler as that is
deprecated.
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
@@ -60,7 +60,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)
@@ -159,7 +158,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_source_file_exceptiont("CONVERSION ERROR");
     }
@@ -205,7 +204,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_source_file_exceptiont("CONVERSION ERROR");
     }
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
@@ -623,14 +623,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
@@ -84,7 +84,6 @@ goto_modelt initialize_goto_model(
   }
 
   language_filest language_files;
-  language_files.set_message_handler(message_handler);
 
   goto_modelt goto_model;
 
@@ -129,7 +128,7 @@ goto_modelt initialize_goto_model(
 
     msg.status() << "Converting" << messaget::eom;
 
-    if(language_files.typecheck(goto_model.symbol_table))
+    if(language_files.typecheck(goto_model.symbol_table, message_handler))
     {
       throw invalid_source_file_exceptiont("CONVERSION ERROR");
     }
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_tablet &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;
   }
 
@@ -204,36 +208,43 @@ bool language_filest::interfaces(
 bool language_filest::typecheck_module(
   symbol_tablet &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_tablet &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;
   }
 
@@ -250,14 +261,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
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/message.h>
 #include <util/symbol_table_base.h>
 
+class message_handlert;
 class language_filet;
 class languaget;
 class symbol_tablet;
@@ -59,7 +60,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;
@@ -102,14 +103,22 @@ 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_tablet &symbol_table);
 
   bool
-  typecheck(symbol_tablet &symbol_table, const bool keep_file_local = false);
+
+  typecheck(
+    symbol_tablet &symbol_table,
+    const bool keep_file_local,
+    message_handlert &message_handler);
+  bool typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)
+  {
+    return typecheck(symbol_table, false, message_handler);
+  }
 
   bool final(symbol_table_baset &symbol_table);
 
@@ -120,7 +129,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 +154,14 @@ class language_filest:public messaget
   bool typecheck_module(
     symbol_tablet &symbol_table,
     language_modulet &module,
-    const bool keep_file_local);
+    const bool keep_file_local,
+    message_handlert &message_handler);
 
   bool typecheck_module(
     symbol_tablet &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_source_file_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
`@@ -60,7 +60,6 @@ lazy_goto_modelt::lazy_goto_modelt(`
`60`	`60`	`driver_program_generate_function_body),`
`61`	`61`	`message_handler(message_handler)`
`62`	`62`	`{`
`63`		`- language_files.set_message_handler(message_handler);`
`64`	`63`	`}`
`65`	`64`
`66`	`65`	`lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)`
`@@ -159,7 +158,7 @@ void lazy_goto_modelt::initialize(`
`159`	`158`
`160`	`159`	`msg.status() << "Converting" << messaget::eom;`
`161`	`160`
`162`		`- if(language_files.typecheck(symbol_table))`
	`161`	`+ if(language_files.typecheck(symbol_table, message_handler))`
`163`	`162`	`{`
`164`	`163`	`throw invalid_source_file_exceptiont("CONVERSION ERROR");`
`165`	`164`	`}`
`@@ -205,7 +204,7 @@ void lazy_goto_modelt::initialize(`
`205`	`204`
`206`	`205`	`msg.status() << "Converting" << messaget::eom;`
`207`	`206`
`208`		`- if(language_files.typecheck(symbol_table))`
	`207`	`+ if(language_files.typecheck(symbol_table, message_handler))`
`209`	`208`	`{`
`210`	`209`	`throw invalid_source_file_exceptiont("CONVERSION ERROR");`
`211`	`210`	`}`
Original file line number	Diff line number	Diff line change
`@@ -84,7 +84,6 @@ goto_modelt initialize_goto_model(`
`84`	`84`	`}`
`85`	`85`
`86`	`86`	`language_filest language_files;`
`87`		`- language_files.set_message_handler(message_handler);`
`88`	`87`
`89`	`88`	`goto_modelt goto_model;`
`90`	`89`
`@@ -129,7 +128,7 @@ goto_modelt initialize_goto_model(`
`129`	`128`
`130`	`129`	`msg.status() << "Converting" << messaget::eom;`
`131`	`130`
`132`		`- if(language_files.typecheck(goto_model.symbol_table))`
	`131`	`+ if(language_files.typecheck(goto_model.symbol_table, message_handler))`
`133`	`132`	`{`
`134`	`133`	`throw invalid_source_file_exceptiont("CONVERSION ERROR");`
`135`	`134`	`}`
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_tablet &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`
`@@ -204,36 +208,43 @@ bool language_filest::interfaces(`
`204`	`208`	`bool language_filest::typecheck_module(`
`205`	`209`	`symbol_tablet &symbol_table,`
`206`	`210`	`const std::string &module,`
`207`		`- const bool keep_file_local)`
	`211`	`+ const bool keep_file_local,`
	`212`	`+ message_handlert &message_handler)`
`208`	`213`	`{`
`209`	`214`	`// check module map`
`210`	`215`
`211`	`216`	`module_mapt::iterator it=module_map.find(module);`
`212`	`217`
`213`	`218`	`if(it==module_map.end())`
`214`	`219`	`{`
`215`		`- error() << "found no file that provides module " << module << eom;`
	`220`	`+ messaget log(message_handler);`
	`221`	`+ log.error() << "found no file that provides module " << module`
	`222`	`+ << messaget::eom;`
`216`	`223`	`return true;`
`217`	`224`	`}`
`218`	`225`
`219`		`- return typecheck_module(symbol_table, it->second, keep_file_local);`
	`226`	`+ return typecheck_module(`
	`227`	`+ symbol_table, it->second, keep_file_local, message_handler);`
`220`	`228`	`}`
`221`	`229`
`222`	`230`	`bool language_filest::typecheck_module(`
`223`	`231`	`symbol_tablet &symbol_table,`
`224`	`232`	`language_modulet &module,`
`225`		`- const bool keep_file_local)`
	`233`	`+ const bool keep_file_local,`
	`234`	`+ message_handlert &message_handler)`
`226`	`235`	`{`
`227`	`236`	`// already typechecked?`
`228`	`237`
`229`	`238`	`if(module.type_checked)`
`230`	`239`	`return false;`
`231`	`240`
	`241`	`+ messaget log(message_handler);`
	`242`	`+`
`232`	`243`	`// already in progress?`
`233`	`244`
`234`	`245`	`if(module.in_progress)`
`235`	`246`	`{`
`236`		`- error() << "circular dependency in " << module.name << eom;`
	`247`	`+ log.error() << "circular dependency in " << module.name << messaget::eom;`
`237`	`248`	`return true;`
`238`	`249`	`}`
`239`	`250`
`@@ -250,14 +261,15 @@ bool language_filest::typecheck_module(`
`250`	`261`	`it!=dependency_set.end();`
`251`	`262`	`it++)`
`252`	`263`	`{`
`253`		`- module.in_progress = !typecheck_module(symbol_table, *it, keep_file_local);`
	`264`	`+ module.in_progress =`
	`265`	`+ !typecheck_module(symbol_table, *it, keep_file_local, message_handler);`
`254`	`266`	`if(module.in_progress == false)`
`255`	`267`	`return true;`
`256`	`268`	`}`
`257`	`269`
`258`	`270`	`// type check it`
`259`	`271`
`260`		`- status() << "Type-checking " << module.name << eom;`
	`272`	`+ log.status() << "Type-checking " << module.name << messaget::eom;`
`261`	`273`
`262`	`274`	`if(module.file->language->can_keep_file_local())`
`263`	`275`	`{`
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_source_file_exceptiont("typechecking failed");`