Skip to content

language_filest is not a messaget #5587

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Dec 16, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion jbmc/src/java_bytecode/lazy_goto_functions_map.h
Original file line number Diff line number Diff line change
Expand Up @@ -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())
Expand Down
3 changes: 1 addition & 2 deletions jbmc/src/java_bytecode/lazy_goto_model.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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");
}
Expand Down
4 changes: 2 additions & 2 deletions src/goto-cc/compile.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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 {};
Expand Down
5 changes: 1 addition & 4 deletions src/goto-programs/initialize_goto_model.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,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");
}
Expand Down Expand Up @@ -200,10 +200,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);

Expand Down
36 changes: 24 additions & 12 deletions src/langapi/language_file.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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;
}

Expand All @@ -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;
}

Expand All @@ -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

Expand Down Expand Up @@ -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;
}

Expand Down Expand Up @@ -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;
}

Expand All @@ -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())
{
Expand Down
27 changes: 19 additions & 8 deletions src/langapi/language_file.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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);

Expand All @@ -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);
Expand All @@ -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
4 changes: 2 additions & 2 deletions unit/testing-utils/get_goto_model_from_c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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("");

Expand All @@ -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");
Expand Down