Skip to content

Complete journalling symbol table #1558

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 7 commits into from
Nov 15, 2017
Merged

Complete journalling symbol table #1558

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
8035397
Style improvements
NathanJPhillips Nov 3, 2017
2ef1c94
Fix bug where move from const symbol collections
NathanJPhillips Nov 2, 2017
cdbac8c
Sort output of symbol_tablet::show
NathanJPhillips Nov 3, 2017
7aa80ad
Remove lookup_impl - it won't work for recording symbol table and add…
NathanJPhillips Nov 3, 2017
a2b45e3
Update to journalling symbol table
NathanJPhillips Nov 3, 2017
3e42a8d
Add comment on has_symbol
NathanJPhillips Nov 3, 2017
69d1a52
Added usages of base class symbol table
NathanJPhillips Nov 3, 2017
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
20 changes: 10 additions & 10 deletions src/java_bytecode/java_bytecode_instrument.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,20 +28,20 @@ class java_bytecode_instrumentt:public messaget
{
public:
java_bytecode_instrumentt(
symbol_tablet &_symbol_table,
symbol_table_baset &_symbol_table,
const bool _throw_runtime_exceptions,
message_handlert &_message_handler):
messaget(_message_handler),
symbol_table(_symbol_table),
throw_runtime_exceptions(_throw_runtime_exceptions),
message_handler(_message_handler)
{
}
message_handlert &_message_handler)
: messaget(_message_handler),
symbol_table(_symbol_table),
throw_runtime_exceptions(_throw_runtime_exceptions),
message_handler(_message_handler)
{
}

void operator()(exprt &expr);

protected:
symbol_tablet &symbol_table;
symbol_table_baset &symbol_table;
const bool throw_runtime_exceptions;
message_handlert &message_handler;

Expand Down Expand Up @@ -577,7 +577,7 @@ void java_bytecode_instrumentt::operator()(exprt &expr)
/// this flag is set to true.
/// \param message_handler: stream to report status and warnings
void java_bytecode_instrument_symbol(
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
symbolt &symbol,
const bool throw_runtime_exceptions,
message_handlert &message_handler)
Expand Down
2 changes: 1 addition & 1 deletion src/java_bytecode/java_bytecode_instrument.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Date: June 2017
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H

void java_bytecode_instrument_symbol(
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
symbolt &symbol,
const bool throw_runtime_exceptions,
message_handlert &_message_handler);
Expand Down
2 changes: 1 addition & 1 deletion src/java_bytecode/java_bytecode_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
#include <util/cprover_prefix.h>
#include <util/c_types.h>

void java_internal_additions(symbol_tablet &dest)
void java_internal_additions(symbol_table_baset &dest)
{
// add __CPROVER_rounding_mode

Expand Down
4 changes: 2 additions & 2 deletions src/java_bytecode/java_bytecode_internal_additions.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,8 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INTERNAL_ADDITIONS_H
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INTERNAL_ADDITIONS_H

#include <util/symbol_table.h>
#include <util/symbol_table_base.h>

void java_internal_additions(symbol_tablet &dest);
void java_internal_additions(symbol_table_baset &dest);

#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INTERNAL_ADDITIONS_H
4 changes: 2 additions & 2 deletions src/java_bytecode/java_bytecode_language.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -355,7 +355,7 @@ void java_bytecode_languaget::convert_lazy_method(
/// generated by string_preprocess.
/// \param context: a symbol table
void java_bytecode_languaget::replace_string_methods(
symbol_tablet &context)
symbol_table_baset &context)
Copy link
Member

Choose a reason for hiding this comment

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

Why do you generalise to the base class here, but not in the other methods?

Copy link
Contributor

Choose a reason for hiding this comment

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

Daniel's instructions: minimise churn by only messing with those functions we have a use for at the moment. Since we're only observing symbol table changes callable from ::typecheck and languaget::final, the result is some methods continuing to take a symbol_tablet. The first user, if one ever comes along, can take responsibility for generalising them.

Copy link
Member

Choose a reason for hiding this comment

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

However, this PR should at least work with current TG. I'll list the necessary extensions below.

{
// Symbols that have code type are potentialy to be replaced
std::list<symbolt> code_symbols;
Expand Down Expand Up @@ -386,7 +386,7 @@ void java_bytecode_languaget::replace_string_methods(
}
}

bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
bool java_bytecode_languaget::final(symbol_table_baset &symbol_table)
{
PRECONDITION(language_options_initialized);

Expand Down
5 changes: 2 additions & 3 deletions src/java_bytecode/java_bytecode_language.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,10 +108,9 @@ class java_bytecode_languaget:public languaget
symbol_tablet &context,
const std::string &module) override;

void replace_string_methods(symbol_tablet &context);
void replace_string_methods(symbol_table_baset &context);

virtual bool final(
symbol_tablet &context) override;
virtual bool final(symbol_table_baset &context) override;

void show_parse(std::ostream &out) override;

Expand Down
16 changes: 8 additions & 8 deletions src/java_bytecode/java_entry_point.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ Author: Daniel Kroening, [email protected]
#include "java_types.h"
#include "java_utils.h"

static void create_initialize(symbol_tablet &symbol_table)
static void create_initialize(symbol_table_baset &symbol_table)
{
// If __CPROVER_initialize already exists, replace it. It may already exist
// if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.
Expand Down Expand Up @@ -89,8 +89,8 @@ static bool is_non_null_library_global(const irep_idt &symbolid)
return non_null_globals.count(symbolid);
}

void java_static_lifetime_init(
symbol_tablet &symbol_table,
static void java_static_lifetime_init(
symbol_table_baset &symbol_table,
const source_locationt &source_location,
bool assume_init_pointers_not_null,
const object_factory_parameterst &object_factory_parameters,
Expand Down Expand Up @@ -162,7 +162,7 @@ void java_static_lifetime_init(
exprt::operandst java_build_arguments(
const symbolt &function,
code_blockt &init_code,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
bool assume_init_pointers_not_null,
object_factory_parameterst object_factory_parameters,
const select_pointer_typet &pointer_type_selector)
Expand Down Expand Up @@ -246,7 +246,7 @@ void java_record_outputs(
const symbolt &function,
const exprt::operandst &main_arguments,
code_blockt &init_code,
symbol_tablet &symbol_table)
symbol_table_baset &symbol_table)
{
const code_typet::parameterst &parameters=
to_code_type(function.type).parameters();
Expand Down Expand Up @@ -319,7 +319,7 @@ void java_record_outputs(
}

main_function_resultt get_main_symbol(
symbol_tablet &symbol_table,
const symbol_table_baset &symbol_table,
const irep_idt &main_class,
message_handlert &message_handler,
bool allow_no_body)
Expand Down Expand Up @@ -445,7 +445,7 @@ main_function_resultt get_main_symbol(
///
/// \returns true if error occurred on entry point search
bool java_entry_point(
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const irep_idt &main_class,
message_handlert &message_handler,
bool assume_init_pointers_not_null,
Expand Down Expand Up @@ -500,7 +500,7 @@ bool java_entry_point(
/// \returns true if error occurred on entry point search, false otherwise
bool generate_java_start_function(
const symbolt &symbol,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
message_handlert &message_handler,
bool assume_init_pointers_not_null,
const object_factory_parameterst& object_factory_parameters,
Expand Down
8 changes: 4 additions & 4 deletions src/java_bytecode/java_entry_point.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]
#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL "uncaught_exception'"

bool java_entry_point(
class symbol_tablet &symbol_table,
class symbol_table_baset &symbol_table,
const irep_idt &main_class,
class message_handlert &message_handler,
bool assume_init_pointers_not_null,
Expand Down Expand Up @@ -61,14 +61,14 @@ struct main_function_resultt

/// Figures out the entry point of the code to verify
main_function_resultt get_main_symbol(
symbol_tablet &symbol_table,
const symbol_table_baset &symbol_table,
const irep_idt &main_class,
message_handlert &,
bool allow_no_body=false);
bool allow_no_body = false);

bool generate_java_start_function(
const symbolt &symbol,
class symbol_tablet &symbol_table,
class symbol_table_baset &symbol_table,
class message_handlert &message_handler,
bool assume_init_pointers_not_null,
const object_factory_parameterst& object_factory_parameters,
Expand Down
26 changes: 13 additions & 13 deletions src/java_bytecode/java_object_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,10 +35,10 @@ Author: Daniel Kroening, [email protected]
#include "java_root_class.h"

static symbolt &new_tmp_symbol(
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const source_locationt &loc,
const typet &type,
const std::string &prefix="tmp_object_factory")
const std::string &prefix = "tmp_object_factory")
{
return get_fresh_aux_symbol(
type,
Expand Down Expand Up @@ -69,7 +69,7 @@ class java_object_factoryt
std::unordered_set<irep_idt, irep_id_hash> recursion_set;

/// The symbol table.
symbol_tablet &symbol_table;
symbol_table_baset &symbol_table;

/// A namespace built from exclusively one symbol table - the one above.
namespacet ns;
Expand Down Expand Up @@ -102,9 +102,9 @@ class java_object_factoryt
std::vector<const symbolt *> &_symbols_created,
const source_locationt &loc,
const object_factory_parameterst _object_factory_parameters,
symbol_tablet &_symbol_table,
const select_pointer_typet &pointer_type_selector):
symbols_created(_symbols_created),
symbol_table_baset &_symbol_table,
const select_pointer_typet &pointer_type_selector)
: symbols_created(_symbols_created),
loc(loc),
object_factory_parameters(_object_factory_parameters),
symbol_table(_symbol_table),
Expand Down Expand Up @@ -182,7 +182,7 @@ class java_object_factoryt
exprt allocate_dynamic_object(
const exprt &target_expr,
const typet &allocate_type,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const source_locationt &loc,
code_blockt &output_code,
std::vector<const symbolt *> &symbols_created,
Expand Down Expand Up @@ -241,7 +241,7 @@ exprt allocate_dynamic_object(
/// \param output_code: code block to which the necessary code is added
void allocate_dynamic_object_with_decl(
const exprt &target_expr,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const source_locationt &loc,
code_blockt &output_code)
{
Expand Down Expand Up @@ -543,7 +543,7 @@ codet initialize_nondet_string_struct(
const exprt &obj,
const std::size_t &max_nondet_string_length,
const source_locationt &loc,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
bool printable)
{
PRECONDITION(
Expand Down Expand Up @@ -636,7 +636,7 @@ static bool add_nondet_string_pointer_initialization(
const exprt &expr,
const std::size_t &max_nondet_string_length,
bool printable,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const source_locationt &loc,
code_blockt &code)
{
Expand Down Expand Up @@ -1361,7 +1361,7 @@ exprt object_factory(
const irep_idt base_name,
code_blockt &init_code,
bool allow_null,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const object_factory_parameterst &parameters,
allocation_typet alloc_type,
const source_locationt &loc,
Expand Down Expand Up @@ -1457,7 +1457,7 @@ exprt object_factory(
void gen_nondet_init(
const exprt &expr,
code_blockt &init_code,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const source_locationt &loc,
bool skip_classid,
allocation_typet alloc_type,
Expand Down Expand Up @@ -1521,7 +1521,7 @@ exprt object_factory(
void gen_nondet_init(
const exprt &expr,
code_blockt &init_code,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const source_locationt &loc,
bool skip_classid,
allocation_typet alloc_type,
Expand Down
14 changes: 7 additions & 7 deletions src/java_bytecode/java_object_factory.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ exprt object_factory(
const irep_idt base_name,
code_blockt &init_code,
bool allow_null,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const object_factory_parameterst &parameters,
allocation_typet alloc_type,
const source_locationt &location,
Expand All @@ -117,7 +117,7 @@ enum class update_in_placet
void gen_nondet_init(
const exprt &expr,
code_blockt &init_code,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const source_locationt &loc,
bool skip_classid,
allocation_typet alloc_type,
Expand All @@ -129,7 +129,7 @@ void gen_nondet_init(
void gen_nondet_init(
const exprt &expr,
code_blockt &init_code,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const source_locationt &loc,
bool skip_classid,
allocation_typet alloc_type,
Expand All @@ -140,23 +140,23 @@ void gen_nondet_init(
exprt allocate_dynamic_object(
const exprt &target_expr,
const typet &allocate_type,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const source_locationt &loc,
code_blockt &output_code,
std::vector<const symbolt *> &symbols_created,
bool cast_needed=false);
bool cast_needed = false);

void allocate_dynamic_object_with_decl(
const exprt &target_expr,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const source_locationt &loc,
code_blockt &output_code);

codet initialize_nondet_string_struct(
const exprt &obj,
const std::size_t &max_nondet_string_length,
const source_locationt &loc,
symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
bool printable);

#endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
Loading