Skip to content
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

assembler_parsert: construct with message handler #8139

Merged
merged 1 commit into from
Feb 6, 2024
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 doc/architectural/goto-program-transformations.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,8 @@ This pass goes through the goto model and removes or lowers instances of
assembly intructions. Assembly instructions are stored in instances of the
`other` instruction.

The implementation of this pass is called via the \ref remove_asm(goto_modelt &)
The implementation of this pass is called via the
\ref remove_asm(goto_modelt &, message_handlert &)
function. For full documentation of this pass see \ref remove_asm.h

<em>This pass has no predecessor.</em>
Expand Down
24 changes: 19 additions & 5 deletions src/assembler/assembler_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,12 +8,26 @@

#include "assembler_parser.h"

assembler_parsert assembler_parser;
char *yyassemblerget_text(void *);

extern char *yyassemblertext;

int yyassemblererror(const std::string &error)
int yyassemblererror(

Check warning on line 13 in src/assembler/assembler_parser.cpp

View check run for this annotation

Codecov / codecov/patch

src/assembler/assembler_parser.cpp#L13

Added line #L13 was not covered by tests
assembler_parsert &assembler_parser,
void *scanner,
const std::string &error)
{
assembler_parser.parse_error(error, yyassemblertext);
assembler_parser.parse_error(error, yyassemblerget_text(scanner));

Check warning on line 18 in src/assembler/assembler_parser.cpp

View check run for this annotation

Codecov / codecov/patch

src/assembler/assembler_parser.cpp#L18

Added line #L18 was not covered by tests
return 0;
}

int yyassemblerlex_init_extra(assembler_parsert *, void **);
int yyassemblerlex(void *);
int yyassemblerlex_destroy(void *);

bool assembler_parsert::parse()
{
void *scanner;
yyassemblerlex_init_extra(this, &scanner);
yyassemblerlex(scanner);
yyassemblerlex_destroy(scanner);
return false;
}
19 changes: 6 additions & 13 deletions src/assembler/assembler_parser.h
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,8 @@

#include <list>

int yyassemblerlex();
int yyassemblererror(const std::string &error);
void assembler_scanner_init();
class assembler_parsert;
int yyassemblererror(assembler_parsert &, void *, const std::string &error);

class assembler_parsert:public parsert
{
Expand All @@ -37,24 +36,18 @@
instructions.push_back(instructiont());
}

assembler_parsert()
explicit assembler_parsert(message_handlert &message_handler)
: parsert(message_handler)
{
}

virtual bool parse()
{
yyassemblerlex();
return false;
}
bool parse() override;

virtual void clear()
void clear() override

Check warning on line 46 in src/assembler/assembler_parser.h

View check run for this annotation

Codecov / codecov/patch

src/assembler/assembler_parser.h#L46

Added line #L46 was not covered by tests
{
parsert::clear();
instructions.clear();
// assembler_scanner_init();
}
};

extern assembler_parsert assembler_parser;

#endif // CPROVER_ASSEMBLER_ASSEMBLER_PARSER_H
30 changes: 21 additions & 9 deletions src/assembler/remove_asm.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,13 @@ Date: December 2014
class remove_asmt
{
public:
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
: symbol_table(_symbol_table), goto_functions(_goto_functions)
remove_asmt(
symbol_tablet &_symbol_table,
goto_functionst &_goto_functions,
message_handlert &message_handler)
: symbol_table(_symbol_table),
goto_functions(_goto_functions),
message_handler(message_handler)
{
}

Expand All @@ -44,6 +49,7 @@ class remove_asmt
protected:
symbol_tablet &symbol_table;
goto_functionst &goto_functions;
message_handlert &message_handler;

void process_function(const irep_idt &, goto_functionst::goto_functiont &);

Expand Down Expand Up @@ -228,7 +234,7 @@ void remove_asmt::process_instruction_gcc(
const irep_idt &i_str = to_string_constant(code.asm_text()).value();

std::istringstream str(id2string(i_str));
assembler_parser.clear();
assembler_parsert assembler_parser{message_handler};
assembler_parser.in = &str;
assembler_parser.parse();

Expand Down Expand Up @@ -399,7 +405,7 @@ void remove_asmt::process_instruction_msc(
const irep_idt &i_str = to_string_constant(code.op0()).value();

std::istringstream str(id2string(i_str));
assembler_parser.clear();
assembler_parsert assembler_parser{message_handler};
assembler_parser.in = &str;
assembler_parser.parse();

Expand Down Expand Up @@ -544,13 +550,17 @@ void remove_asmt::process_function(
remove_skip(goto_function.body);
}

/// \copybrief remove_asm(goto_modelt &)
/// \copybrief remove_asm(goto_modelt &, message_handlert &)
///
/// \param goto_functions: The goto functions
/// \param symbol_table: The symbol table
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
/// \param message_handler: Message handler
void remove_asm(
goto_functionst &goto_functions,
symbol_tablet &symbol_table,
message_handlert &message_handler)
{
remove_asmt rem(symbol_table, goto_functions);
remove_asmt rem(symbol_table, goto_functions, message_handler);
rem();
}

Expand All @@ -561,9 +571,11 @@ void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
/// Unrecognised assembly instructions are ignored.
///
/// \param goto_model: The goto model
void remove_asm(goto_modelt &goto_model)
/// \param message_handler: Message handler
void remove_asm(goto_modelt &goto_model, message_handlert &message_handler)
{
remove_asm(goto_model.goto_functions, goto_model.symbol_table);
remove_asm(
goto_model.goto_functions, goto_model.symbol_table, message_handler);
}

bool has_asm(const goto_functionst &goto_functions)
Expand Down
5 changes: 3 additions & 2 deletions src/assembler/remove_asm.h
Original file line number Diff line number Diff line change
Expand Up @@ -54,11 +54,12 @@ Date: December 2014

class goto_functionst;
class goto_modelt;
class message_handlert;
class symbol_tablet;

void remove_asm(goto_functionst &, symbol_tablet &);
void remove_asm(goto_functionst &, symbol_tablet &, message_handlert &);

void remove_asm(goto_modelt &);
void remove_asm(goto_modelt &, message_handlert &);

/// returns true iff the given goto functions use asm instructions
bool has_asm(const goto_functionst &);
Expand Down
17 changes: 4 additions & 13 deletions src/assembler/scanner.l
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
%option noinput
%option nounistd
%option never-interactive
%option noyywrap
%option reentrant
%option extra-type="assembler_parsert *"

%{

Expand All @@ -13,7 +16,7 @@
#pragma warning(disable:4005)
#endif

#define PARSER assembler_parser
#define PARSER (*yyextra)
#define YYSTYPE unsigned
#undef ECHO
#define ECHO
Expand Down Expand Up @@ -60,14 +63,6 @@ string_lit ("L"|"u"|"U"|"u8")?["]{s_char}*["]
%x GRAMMAR
%x LINE_COMMENT

%{
void assemlber_scanner_init()
{
YY_FLUSH_BUFFER;
BEGIN(0);
}
%}

%%

<INITIAL>.|\n { BEGIN(GRAMMAR);
Expand Down Expand Up @@ -109,7 +104,3 @@ void assemlber_scanner_init()
}

<<EOF>> { yyterminate(); /* done! */ }

%%

int yywrap() { return 1; }
4 changes: 2 additions & 2 deletions src/cbmc/cbmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -883,7 +883,7 @@
{
// Remove inline assembler; this needs to happen before
// adding the library.
remove_asm(goto_model);
remove_asm(goto_model, log.get_message_handler());

// add the library
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
Expand All @@ -895,7 +895,7 @@
// library functions may introduce inline assembler
while(has_asm(goto_model))
{
remove_asm(goto_model);
remove_asm(goto_model, log.get_message_handler());

Check warning on line 898 in src/cbmc/cbmc_parse_options.cpp

View check run for this annotation

Codecov / codecov/patch

src/cbmc/cbmc_parse_options.cpp#L898

Added line #L898 was not covered by tests
link_to_library(
goto_model, log.get_message_handler(), cprover_cpp_library_factory);
link_to_library(
Expand Down
4 changes: 2 additions & 2 deletions src/goto-analyzer/goto_analyzer_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -698,7 +698,7 @@
{
// Remove inline assembler; this needs to happen before
// adding the library.
remove_asm(goto_model);
remove_asm(goto_model, ui_message_handler);

// add the library
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
Expand All @@ -708,7 +708,7 @@
// library functions may introduce inline assembler
while(has_asm(goto_model))
{
remove_asm(goto_model);
remove_asm(goto_model, ui_message_handler);

Check warning on line 711 in src/goto-analyzer/goto_analyzer_parse_options.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-analyzer/goto_analyzer_parse_options.cpp#L711

Added line #L711 was not covered by tests
link_to_library(
goto_model, ui_message_handler, cprover_cpp_library_factory);
link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
Expand Down
4 changes: 2 additions & 2 deletions src/goto-diff/goto_diff_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@
{
// Remove inline assembler; this needs to happen before
// adding the library.
remove_asm(goto_model);
remove_asm(goto_model, ui_message_handler);

// add the library
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
Expand All @@ -186,7 +186,7 @@
// library functions may introduce inline assembler
while(has_asm(goto_model))
{
remove_asm(goto_model);
remove_asm(goto_model, ui_message_handler);

Check warning on line 189 in src/goto-diff/goto_diff_parse_options.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-diff/goto_diff_parse_options.cpp#L189

Added line #L189 was not covered by tests
link_to_library(
goto_model, ui_message_handler, cprover_cpp_library_factory);
link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
Expand Down
6 changes: 3 additions & 3 deletions src/goto-instrument/goto_instrument_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -949,7 +949,7 @@
log.status() << "Virtual function removal" << messaget::eom;
remove_virtual_functions(goto_model);
log.status() << "Cleaning inline assembler statements" << messaget::eom;
remove_asm(goto_model);
remove_asm(goto_model, log.get_message_handler());
}

/// Remove function pointers that can be resolved by analysing const variables
Expand Down Expand Up @@ -1065,7 +1065,7 @@

// remove inline assembler as that may yield further library function calls
// that need to be resolved
remove_asm(goto_model);
remove_asm(goto_model, ui_message_handler);

// add the library
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
Expand All @@ -1076,7 +1076,7 @@
// library functions may introduce inline assembler
while(has_asm(goto_model))
{
remove_asm(goto_model);
remove_asm(goto_model, ui_message_handler);

Check warning on line 1079 in src/goto-instrument/goto_instrument_parse_options.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-instrument/goto_instrument_parse_options.cpp#L1079

Added line #L1079 was not covered by tests
link_to_library(
goto_model, ui_message_handler, cprover_cpp_library_factory);
link_to_library(
Expand Down
4 changes: 2 additions & 2 deletions src/goto-synthesizer/cegis_verifier.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -84,15 +84,15 @@
void cegis_verifiert::preprocess_goto_model()
{
// Preprocess `goto_model`. Copied from `cbmc_parse_options.cpp`.
remove_asm(goto_model);
remove_asm(goto_model, log.get_message_handler());
link_to_library(
goto_model, log.get_message_handler(), cprover_cpp_library_factory);
link_to_library(
goto_model, log.get_message_handler(), cprover_c_library_factory);
// library functions may introduce inline assembler
while(has_asm(goto_model))
{
remove_asm(goto_model);
remove_asm(goto_model, log.get_message_handler());

Check warning on line 95 in src/goto-synthesizer/cegis_verifier.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-synthesizer/cegis_verifier.cpp#L95

Added line #L95 was not covered by tests
link_to_library(
goto_model, log.get_message_handler(), cprover_cpp_library_factory);
link_to_library(
Expand Down
4 changes: 2 additions & 2 deletions src/libcprover-cpp/api.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -178,7 +178,7 @@
bool api_sessiont::preprocess_model() const
{
// Remove inline assembler; this needs to happen before adding the library.
remove_asm(*implementation->model);
remove_asm(*implementation->model, *implementation->message_handler);

// add the library
messaget log{*implementation->message_handler};
Expand All @@ -191,7 +191,7 @@
// library functions may introduce inline assembler
while(has_asm(*implementation->model))
{
remove_asm(*implementation->model);
remove_asm(*implementation->model, *implementation->message_handler);

Check warning on line 194 in src/libcprover-cpp/api.cpp

View check run for this annotation

Codecov / codecov/patch

src/libcprover-cpp/api.cpp#L194

Added line #L194 was not covered by tests
link_to_library(
*implementation->model,
*implementation->message_handler,
Expand Down
Loading