Skip to content

Commit 4f793eb

Browse files
JohnDumbellJohnDumbell
committed
Wrap incoming symbol tables in suffix-aware versions
1 parent bc30502 commit 4f793eb

File tree

5 files changed

+49
-19
lines changed

5 files changed

+49
-19
lines changed

‎jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
2323
#include <json/json_parser.h>
2424

2525
#include <goto-programs/class_hierarchy.h>
26+
#include <util/symbol_table_builder.h>
2627

2728
#include "java_bytecode_concurrency_instrumentation.h"
2829
#include "java_bytecode_convert_class.h"
@@ -787,8 +788,11 @@ bool java_bytecode_languaget::typecheck(
787788
break;
788789
case LAZY_METHODS_MODE_EAGER:
789790
{
791+
symbol_table_buildert symbol_table_builder =
792+
symbol_table_buildert::wrap(symbol_table);
793+
790794
journalling_symbol_tablet journalling_symbol_table =
791-
journalling_symbol_tablet::wrap(symbol_table);
795+
journalling_symbol_tablet::wrap(symbol_table_builder);
792796

793797
// Convert all synthetic methods:
794798
for(const auto &function_id_and_type : synthetic_methods)
@@ -839,18 +843,21 @@ bool java_bytecode_languaget::generate_support_functions(
839843
{
840844
PRECONDITION(language_options_initialized);
841845

846+
symbol_table_buildert symbol_table_builder =
847+
symbol_table_buildert::wrap(symbol_table);
848+
842849
main_function_resultt res=
843850
get_main_symbol(symbol_table, main_class, get_message_handler());
844851
if(!res.is_success())
845852
return res.is_error();
846853

847854
// Load the main function into the symbol table to get access to its
848855
// parameter names
849-
convert_lazy_method(res.main_function.name, symbol_table);
856+
convert_lazy_method(res.main_function.name, symbol_table_builder);
850857

851858
// generate the test harness in __CPROVER__start and a call the entry point
852859
return java_entry_point(
853-
symbol_table,
860+
symbol_table_builder,
854861
main_class,
855862
get_message_handler(),
856863
assume_inputs_non_null,
@@ -877,12 +884,15 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
877884
symbol_tablet &symbol_table,
878885
method_bytecodet &method_bytecode)
879886
{
887+
symbol_table_buildert symbol_table_builder =
888+
symbol_table_buildert::wrap(symbol_table);
889+
880890
const method_convertert method_converter =
881-
[this, &symbol_table]
891+
[this, &symbol_table_builder]
882892
(const irep_idt &function_id, ci_lazy_methods_neededt lazy_methods_needed)
883893
{
884894
return convert_single_method(
885-
function_id, symbol_table, std::move(lazy_methods_needed));
895+
function_id, symbol_table_builder, std::move(lazy_methods_needed));
886896
};
887897

888898
ci_lazy_methodst method_gather(

‎src/goto-cc/compile.cpp

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ Date: June 2006
2222
#include <util/file_util.h>
2323
#include <util/get_base_name.h>
2424
#include <util/suffix.h>
25+
#include <util/symbol_table_builder.h>
2526
#include <util/tempdir.h>
2627
#include <util/unicode.h>
2728
#include <util/version.h>
@@ -692,37 +693,40 @@ void compilet::add_compiler_specific_defines(configt &config) const
692693

693694
void compilet::convert_symbols(goto_functionst &dest)
694695
{
696+
symbol_table_buildert symbol_table_builder =
697+
symbol_table_buildert::wrap(goto_model.symbol_table);
698+
695699
goto_convert_functionst converter(
696-
goto_model.symbol_table, get_message_handler());
700+
symbol_table_builder, get_message_handler());
697701

698702
// the compilation may add symbols!
699703

700704
symbol_tablet::symbolst::size_type before=0;
701705

702-
while(before != goto_model.symbol_table.symbols.size())
706+
while(before != symbol_table_builder.symbols.size())
703707
{
704-
before = goto_model.symbol_table.symbols.size();
708+
before = symbol_table_builder.symbols.size();
705709

706710
typedef std::set<irep_idt> symbols_sett;
707711
symbols_sett symbols;
708712

709-
for(const auto &named_symbol : goto_model.symbol_table.symbols)
713+
for(const auto &named_symbol : symbol_table_builder.symbols)
710714
symbols.insert(named_symbol.first);
711715

712716
// the symbol table iterators aren't stable
713717
for(const auto &symbol : symbols)
714718
{
715719
symbol_tablet::symbolst::const_iterator s_it =
716-
goto_model.symbol_table.symbols.find(symbol);
717-
CHECK_RETURN(s_it != goto_model.symbol_table.symbols.end());
720+
symbol_table_builder.symbols.find(symbol);
721+
CHECK_RETURN(s_it != symbol_table_builder.symbols.end());
718722

719723
if(
720724
s_it->second.is_function() && !s_it->second.is_compiled() &&
721725
s_it->second.value.is_not_nil())
722726
{
723727
debug() << "Compiling " << s_it->first << eom;
724728
converter.convert_function(s_it->first, dest.function_map[s_it->first]);
725-
goto_model.symbol_table.get_writeable_ref(symbol).set_compiled();
729+
symbol_table_builder.get_writeable_ref(symbol).set_compiled();
726730
}
727731
}
728732
}

‎src/goto-programs/goto_convert.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
1212
#include "goto_convert.h"
1313

1414
#include <util/arith_tools.h>
15+
#include <util/c_types.h>
1516
#include <util/cprover_prefix.h>
1617
#include <util/exception_utils.h>
1718
#include <util/expr_util.h>
@@ -20,8 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
2021
#include <util/simplify_expr.h>
2122
#include <util/std_expr.h>
2223
#include <util/symbol_table.h>
23-
24-
#include <util/c_types.h>
24+
#include <util/symbol_table_builder.h>
2525

2626
#include "goto_convert_class.h"
2727
#include "destructor.h"
@@ -1939,7 +1939,9 @@ void goto_convert(
19391939
message_handlert &message_handler,
19401940
const irep_idt &mode)
19411941
{
1942-
goto_convertt goto_convert(symbol_table, message_handler);
1942+
symbol_table_buildert symbol_table_builder =
1943+
symbol_table_buildert::wrap(symbol_table);
1944+
goto_convertt goto_convert(symbol_table_builder, message_handler);
19431945
goto_convert.goto_convert(code, dest, mode);
19441946
}
19451947

‎src/goto-programs/goto_convert_functions.cpp

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Date: June 2003
1515
#include <util/symbol_table.h>
1616
#include <util/prefix.h>
1717
#include <util/fresh_symbol.h>
18+
#include <util/symbol_table_builder.h>
1819

1920
#include "goto_inline.h"
2021

@@ -217,8 +218,11 @@ void goto_convert(
217218
goto_modelt &goto_model,
218219
message_handlert &message_handler)
219220
{
221+
symbol_table_buildert symbol_table_builder =
222+
symbol_table_buildert::wrap( goto_model.symbol_table);
223+
220224
goto_convert(
221-
goto_model.symbol_table,
225+
symbol_table_builder,
222226
goto_model.goto_functions,
223227
message_handler);
224228
}
@@ -228,7 +232,10 @@ void goto_convert(
228232
goto_functionst &functions,
229233
message_handlert &message_handler)
230234
{
231-
goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
235+
symbol_table_buildert symbol_table_builder =
236+
symbol_table_buildert::wrap(symbol_table);
237+
238+
goto_convert_functionst goto_convert_functions(symbol_table_builder, message_handler);
232239

233240
goto_convert_functions.goto_convert(functions);
234241
}
@@ -239,7 +246,10 @@ void goto_convert(
239246
goto_functionst &functions,
240247
message_handlert &message_handler)
241248
{
242-
goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
249+
symbol_table_buildert symbol_table_builder =
250+
symbol_table_buildert::wrap(symbol_table);
251+
252+
goto_convert_functionst goto_convert_functions(symbol_table_builder, message_handler);
243253

244254
goto_convert_functions.convert_function(
245255
identifier, functions.function_map[identifier]);

‎src/goto-programs/lazy_goto_functions_map.h

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
#include <util/message.h>
1515
#include <langapi/language_file.h>
1616
#include <util/journalling_symbol_table.h>
17+
#include <util/symbol_table_builder.h>
1718

1819
/// Provides a wrapper for a map of lazily loaded goto_functiont.
1920
/// This incrementally builds a goto-functions object, while permitting
@@ -142,8 +143,11 @@ class lazy_goto_functions_mapt final
142143
// const first
143144
reference ensure_function_loaded_internal(const key_type &name) const
144145
{
146+
symbol_table_buildert symbol_table_builder =
147+
symbol_table_buildert::wrap(symbol_table);
148+
145149
journalling_symbol_tablet journalling_table =
146-
journalling_symbol_tablet::wrap(symbol_table);
150+
journalling_symbol_tablet::wrap(symbol_table_builder);
147151
reference named_function=ensure_entry_converted(name, journalling_table);
148152
mapped_type function=named_function.second;
149153
if(processed_functions.count(name)==0)

0 commit comments

Comments
 (0)