Skip to content

Make goto_symext::language_mode protected #8646

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.

Sign up for GitHub

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
Sep 15, 2025
Merged

Make goto_symext::language_mode protected #8646

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
26 changes: 4 additions & 22 deletions src/goto-checker/bmc_util.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,8 @@ Author: Daniel Kroening, Peter Schrammel

#include "bmc_util.h"

#include <iostream>
#include <util/json_stream.h>
#include <util/ui_message.h>

#include <goto-programs/graphml_witness.h>
#include <goto-programs/json_goto_trace.h>
Expand All @@ -21,17 +22,13 @@ Author: Daniel Kroening, Peter Schrammel
#include <goto-symex/memory_model_pso.h>
#include <goto-symex/slice.h>
#include <goto-symex/symex_target_equation.h>

#include <linking/static_lifetime_init.h>

#include <solvers/decision_procedure.h>

#include <util/json_stream.h>
#include <util/ui_message.h>

#include "goto_symex_property_decider.h"
#include "symex_bmc.h"

#include <iostream>

void message_building_error_trace(messaget &log)
{
log.status() << "Building error trace" << messaget::eom;
Expand Down Expand Up @@ -175,21 +172,6 @@ get_memory_model(const optionst &options, const namespacet &ns)
}
}

void setup_symex(
symex_bmct &symex,
const namespacet &ns,
ui_message_handlert &ui_message_handler)
{
messaget msg(ui_message_handler);
const symbolt *init_symbol;
if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
symex.language_mode = init_symbol->mode;

msg.status() << "Starting Bounded Model Checking" << messaget::eom;

symex.last_source_location.make_nil();
}

void slice(
symex_bmct &symex,
symex_target_equationt &symex_target_equation,
Expand Down
2 changes: 0 additions & 2 deletions src/goto-checker/bmc_util.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,8 +69,6 @@ void output_graphml(
std::unique_ptr<memory_model_baset>
get_memory_model(const optionst &options, const namespacet &);

void setup_symex(symex_bmct &, const namespacet &, ui_message_handlert &);

void slice(
symex_bmct &,
symex_target_equationt &symex_target_equation,
Expand Down
1 change: 0 additions & 1 deletion src/goto-checker/multi_path_symex_only_checker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,6 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
unwindset.parse_unwind(options.get_option("unwind"));
unwindset.parse_unwindset(
options.get_list_option("unwindset"), goto_model, ui_message_handler);
setup_symex(symex, ns, ui_message_handler);
Copy link
Member

@peterschrammel peterschrammel Sep 12, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you remove this then the virtual function won't even be called...

Copy link
Collaborator Author

@tautschnig tautschnig Sep 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's fine, there is no need for doing so.

}

incremental_goto_checkert::resultt multi_path_symex_only_checkert::
Expand Down
1 change: 0 additions & 1 deletion src/goto-checker/single_loop_incremental_symex_checker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,6 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
unwindset.parse_unwind(options.get_option("unwind"));
unwindset.parse_unwindset(
options.get_list_option("unwindset"), goto_model, ui_message_handler);
setup_symex(symex, ns, ui_message_handler);
Copy link
Member

@peterschrammel peterschrammel Sep 12, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

see above

Copy link
Collaborator Author

@tautschnig tautschnig Sep 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's fine, there is no need for doing so.


// Freeze all symbols if we are using a prop_conv_solvert
prop_conv_solvert *prop_conv_solver = dynamic_cast<prop_conv_solvert *>(
Expand Down
5 changes: 0 additions & 5 deletions src/goto-checker/single_path_symex_only_checker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,11 +152,6 @@ void single_path_symex_only_checkert::equation_output(
}
}

void single_path_symex_only_checkert::setup_symex(symex_bmct &symex)
{
::setup_symex(symex, ns, ui_message_handler);
}

void single_path_symex_only_checkert::update_properties(
propertiest &properties,
std::unordered_set<irep_idt> &updated_properties,
Expand Down
5 changes: 4 additions & 1 deletion src/goto-checker/single_path_symex_only_checker.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,10 @@ class single_path_symex_only_checkert : public incremental_goto_checkert
const symex_bmct &symex,
const symex_target_equationt &equation);

virtual void setup_symex(symex_bmct &symex);
virtual void setup_symex(symex_bmct &symex)
Copy link
Member

@peterschrammel peterschrammel Sep 12, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this even called anywhere now?

Copy link
Collaborator Author

@tautschnig tautschnig Sep 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it's called from initialize_worklist and resume_path in this class. Which is also why this needs to be kept: it will be called more than once in the single-path case. Yet the only actual code being executed is java_setup_symex, and I am wondering whether this needs to be re-done per path, or instead could be done just once when creating symex_bmct?

Copy link
Member

@peterschrammel peterschrammel Sep 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

java_setup_symex just installs a loop_unwind_handler. This should be done only once when creating symex_bmct.

Copy link
Collaborator Author

@tautschnig tautschnig Sep 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, when writing my earlier comment I had failed to consider that initialize_worklist and resume_path actually do create a fresh symex_bmct instance each time, so each time we do need to invoke java_setup_symex. So I'd argue the code is actually ok as it is?!

Copy link
Member

@peterschrammel peterschrammel Sep 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, yes.

{
// deriving classes may do extra work here
}

/// Adds the initial goto-symex state as a path to the worklist
virtual void initialize_worklist();
Expand Down
9 changes: 9 additions & 0 deletions src/goto-checker/symex_bmc.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]

#include <goto-programs/unwindset.h>

#include <linking/static_lifetime_init.h>

#include <limits>

symex_bmct::symex_bmct(
Expand All @@ -33,10 +35,17 @@ symex_bmct::symex_bmct(
options,
path_storage,
guard_manager),
last_source_location(source_locationt::nil()),
record_coverage(!options.get_option("symex-coverage-report").empty()),
unwindset(unwindset),
symex_coverage(ns)
{
const symbolt *init_symbol = outer_symbol_table.lookup(INITIALIZE_FUNCTION);
if(init_symbol)
language_mode = init_symbol->mode;

messaget msg{mh};
msg.status() << "Starting Bounded Model Checking" << messaget::eom;
}

/// show progress
Expand Down
3 changes: 0 additions & 3 deletions src/goto-symex/goto_symex.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -235,13 +235,10 @@ class goto_symext
messaget::mstreamt &
print_callstack_entry(const symex_targett::sourcet &target);

public:

/// language_mode: ID_java, ID_C or another language identifier
/// if we know the source language in use, irep_idt() otherwise.
irep_idt language_mode;

protected:
/// The symbol table associated with the goto-program being executed.
/// This symbol table will not have objects that are dynamically created as
/// part of symbolic execution added to it; those object are stored in the
Expand Down
2 changes: 0 additions & 2 deletions unit/path_strategies.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -425,7 +425,6 @@ void _check_with_strategy(
*worklist,
guard_manager,
unwindset);
setup_symex(symex, ns, ui_message_handler);

symex.initialize_path_storage_from_entry_point_of(
goto_symext::get_goto_function(goto_model),
Expand All @@ -448,7 +447,6 @@ void _check_with_strategy(
*worklist,
guard_manager,
unwindset);
setup_symex(symex, ns, ui_message_handler);

symex_symbol_table = symex.resume_symex_from_saved_state(
goto_symext::get_goto_function(goto_model),
Expand Down
Loading