From c1907f7ca0fa11b3a0cddeff121a03440173287e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 10 Feb 2013 21:04:12 +0000 Subject: [PATCH] context -> symbol_table --- src/ebmc/cegar/bmc_cegar.cpp | 2 +- src/ebmc/cegar/bmc_cegar.h | 8 +-- src/ebmc/coverage/induction_coverage.cpp | 8 +-- src/ebmc/coverage/interpolation_coverage.cpp | 10 ++-- src/ebmc/ebmc_base.cpp | 34 ++++-------- src/ebmc/ebmc_solvers.cpp | 20 +++---- .../interpolation/compute-interpolant.cpp | 4 +- src/ebmc/interpolation/interpolation_expr.cpp | 20 +++---- .../interpolation/interpolation_netlist.cpp | 14 ++--- .../interpolation_netlist_vmcai.cpp | 22 ++++---- src/ebmc/interpolation/interpolation_word.cpp | 26 +++++----- src/ebmc/k_induction.cpp | 6 +-- src/ebmc/output_verilog.cpp | 40 +++++++------- src/ebmc/output_verilog.h | 14 ++--- src/ebmc/parseoptions.cpp | 4 +- src/ebmc/show_trans.cpp | 4 +- src/hw-cbmc/gen_interface.cpp | 20 +++---- src/hw-cbmc/gen_interface.h | 4 +- src/hw-cbmc/hw_bmc.h | 4 +- src/hw-cbmc/map_vars.cpp | 52 +++++++++---------- src/hw-cbmc/map_vars.h | 4 +- src/hw-cbmc/parseoptions.cpp | 12 ++--- src/smvlang/smv_language.cpp | 4 +- src/smvlang/smv_language.h | 2 +- src/smvlang/smv_typecheck.cpp | 50 +++++++++--------- src/smvlang/smv_typecheck.h | 4 +- src/trans/counterexample.cpp | 4 +- src/trans/netlist_trans.cpp | 26 +++++----- src/trans/netlist_trans.h | 4 +- src/trans/property.h | 2 +- src/trans/show_modules.cpp | 4 +- src/trans/show_modules.h | 4 +- src/trans/trans_trace.cpp | 4 +- src/trans/var_map.h | 2 +- src/verilog/verilog2expr.cpp | 2 +- src/verilog/verilog2expr.h | 2 +- src/verilog/verilog_context.cpp | 10 ++-- src/verilog/verilog_flattening.cpp | 16 +++--- src/verilog/verilog_flattening.h | 12 ++--- src/verilog/verilog_interfaces.cpp | 32 ++++++------ src/verilog/verilog_language.cpp | 8 +-- src/verilog/verilog_language.h | 4 +- src/verilog/verilog_module_instance.cpp | 16 +++--- ...rilog_context.h => verilog_symbol_table.h} | 12 ++--- src/verilog/verilog_synthesis.cpp | 40 +++++++------- src/verilog/verilog_synthesis.h | 12 ++--- src/verilog/verilog_typecheck.cpp | 30 +++++------ src/verilog/verilog_typecheck.h | 18 +++---- src/verilog/verilog_typecheck_base.h | 2 +- src/vhdl/vhdl2expr.cpp | 2 +- src/vhdl/vhdl2expr.h | 2 +- src/vhdl/vhdl_language.cpp | 8 +-- src/vhdl/vhdl_language.h | 4 +- src/vhdl/vhdl_typecheck.h | 4 +- 54 files changed, 333 insertions(+), 345 deletions(-) rename src/verilog/{verilog_context.h => verilog_symbol_table.h} (66%) diff --git a/src/ebmc/cegar/bmc_cegar.cpp b/src/ebmc/cegar/bmc_cegar.cpp index 67ab56d..cb78465 100644 --- a/src/ebmc/cegar/bmc_cegar.cpp +++ b/src/ebmc/cegar/bmc_cegar.cpp @@ -231,7 +231,7 @@ void bmc_cegart::make_netlist() try { convert_trans_to_netlist( - context, main_module, + symbol_table, main_module, properties, concrete_netlist, message); } diff --git a/src/ebmc/cegar/bmc_cegar.h b/src/ebmc/cegar/bmc_cegar.h index 308e64b..0e7b48a 100644 --- a/src/ebmc/cegar/bmc_cegar.h +++ b/src/ebmc/cegar/bmc_cegar.h @@ -17,13 +17,13 @@ class bmc_cegart { public: bmc_cegart( - contextt &_context, + symbol_tablet &_symbol_table, const irep_idt &_main_module, messaget &_message, const std::list &_properties, bool _verbose): - context(_context), - ns(_context), + symbol_table(_symbol_table), + ns(_symbol_table), main_module(_main_module), message(_message), properties(_properties), @@ -34,7 +34,7 @@ public: void bmc_cegar(); protected: - contextt &context; + symbol_tablet &symbol_table; const namespacet ns; const irep_idt &main_module; messaget &message; diff --git a/src/ebmc/coverage/induction_coverage.cpp b/src/ebmc/coverage/induction_coverage.cpp index 0603df4..56b8aad 100644 --- a/src/ebmc/coverage/induction_coverage.cpp +++ b/src/ebmc/coverage/induction_coverage.cpp @@ -271,7 +271,7 @@ void induction_coveraget::remove_covered(const bmc_mapt &bmc_map, solver.set_assumptions(assumptions); propt::resultt dec_result = solver.prop_solve(); - namespacet ns(context); + namespacet ns(symbol_table); switch(dec_result) { @@ -388,7 +388,7 @@ void induction_coveraget::remove_not_covered_from_scratch(const bmc_mapt &bmc_ma induction_test_from_scratch.total_tests++; propt::resultt dec_result = solver.prop_solve(); - namespacet ns(context); + namespacet ns(symbol_table); switch(dec_result) { @@ -544,7 +544,7 @@ induction_resultt induction_coveraget::is_inductive(bool force, satcheckt &interpolator, bool assume) { - namespacet ns(context); + namespacet ns(symbol_table); bmc_mapt netlist_bmc_map_induction; netlist_bmc_map_induction.map_timeframes(netlist, 2, interpolator); //vars in tf 0 and 1 @@ -681,7 +681,7 @@ literalt induction_coveraget::unwind( induction_resultt induction_coveraget::is_inductive1(bool force, satcheck_minisat_normal_prooft &interpolator) { - namespacet ns(context); + namespacet ns(symbol_table); interpolator.set_partition_id(1); bmc_mapt netlist_bmc_map_induction; diff --git a/src/ebmc/coverage/interpolation_coverage.cpp b/src/ebmc/coverage/interpolation_coverage.cpp index a66034b..26ba91e 100644 --- a/src/ebmc/coverage/interpolation_coverage.cpp +++ b/src/ebmc/coverage/interpolation_coverage.cpp @@ -166,7 +166,7 @@ int interpolation_coveraget::iteration() status("Iteration "+i2string(iteration_number)+ ", bound="+i2string(bound)); - namespacet ns(context); + namespacet ns(symbol_table); interpolatort interpolator; boolbvt solver(ns, interpolator); solver.equality_propagation=false; @@ -314,7 +314,7 @@ int interpolation_coveraget::induction_step() { status("Induction Step"); - namespacet ns(context); + namespacet ns(symbol_table); interpolatort satcheck; boolbvt solver(ns, satcheck); @@ -379,7 +379,7 @@ int interpolation_coveraget::induction_step() bool interpolation_coveraget::check_partition_one_implies_interpolant(const bit_interpolantt ¤t_inter) { - namespacet ns(context); + namespacet ns(symbol_table); interpolatort interpolator; boolbvt solver(ns, interpolator); @@ -417,7 +417,7 @@ bool interpolation_coveraget::check_partition_one_implies_interpolant(const bit_ bool interpolation_coveraget::check_partition_two_and_interpolant(const bit_interpolantt ¤t_inter) { - namespacet ns(context); + namespacet ns(symbol_table); interpolatort interpolator; boolbvt solver(ns, interpolator); @@ -494,7 +494,7 @@ else { propt::resultt dec_result = solver.prop_solve(); - namespacet ns(context); + namespacet ns(symbol_table); switch(dec_result) { diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp index 64fdbbd..2edbc55 100644 --- a/src/ebmc/ebmc_base.cpp +++ b/src/ebmc/ebmc_base.cpp @@ -69,7 +69,7 @@ Function: ebmc_baset::show_trace void ebmc_baset::show_trace(const trans_tracet &trans_trace) { - namespacet ns(context); + namespacet ns(symbol_table); if(cmdline.isset("vcd")) { @@ -125,7 +125,7 @@ int ebmc_baset::finish(prop_convt &solver) { result("SAT: bug found"); - namespacet ns(context); + namespacet ns(symbol_table); trans_tracet trans_trace; compute_trans_trace( @@ -189,7 +189,7 @@ int ebmc_baset::finish(const bmc_mapt &bmc_map, propt &solver) { result("SAT: bug found"); - namespacet ns(context); + namespacet ns(symbol_table); trans_tracet trans_trace; compute_trans_trace( @@ -255,7 +255,7 @@ void ebmc_baset::unwind( unsigned _bound, bool initial_state) { - const namespacet ns(context); + const namespacet ns(symbol_table); ::unwind(*trans_expr, *this, solver, _bound, ns, initial_state); } @@ -281,7 +281,7 @@ void ebmc_baset::check_property(prop_convt &solver, bool convert_only) unwind(solver); - namespacet ns(context); + namespacet ns(symbol_table); property( prop_expr_list, @@ -336,7 +336,7 @@ Function: ebmc_baset::parse_property bool ebmc_baset::parse_property( const std::string &property) { - namespacet ns(context); + namespacet ns(symbol_table); languagest languages(ns, get_language_from_mode(main_symbol->mode)); @@ -388,10 +388,10 @@ bool ebmc_baset::get_model_properties() { forall_symbol_module_map( it, - context.symbol_module_map, + symbol_table.symbol_module_map, main_symbol->name) { - namespacet ns(context); + namespacet ns(symbol_table); const symbolt &symbol=ns.lookup(it->second); if(symbol.is_property) @@ -506,7 +506,7 @@ bool ebmc_baset::get_main() try { - main_symbol=&get_module(context, module, get_message_handler()); + main_symbol=&get_module(symbol_table, module, get_message_handler()); trans_expr=&to_trans_expr(main_symbol->value); } @@ -639,15 +639,6 @@ void ebmc_baset::report_success() switch(get_ui()) { - case ui_message_handlert::OLD_GUI: - std::cout << "SUCCESS" << std::endl - << "Verification successful" << std::endl - << "" << std::endl - << "" << std::endl - << "" << std::endl - << "" << std::endl; - break; - case ui_message_handlert::PLAIN: break; @@ -683,9 +674,6 @@ void ebmc_baset::report_failure() switch(get_ui()) { - case ui_message_handlert::OLD_GUI: - break; - case ui_message_handlert::PLAIN: break; @@ -742,7 +730,7 @@ int ebmc_baset::get_model() if(cmdline.isset("show-modules")) { - show_modules(context, get_ui()); + show_modules(symbol_table, get_ui()); return 0; } @@ -893,7 +881,7 @@ void ebmc_baset::make_netlist(netlistt &netlist) try { convert_trans_to_netlist( - context, main_symbol->name, prop_expr_list, netlist, *this); + symbol_table, main_symbol->name, prop_expr_list, netlist, *this); } catch(const std::string &error_str) diff --git a/src/ebmc/ebmc_solvers.cpp b/src/ebmc/ebmc_solvers.cpp index c791a41..a9c4199 100644 --- a/src/ebmc/ebmc_solvers.cpp +++ b/src/ebmc/ebmc_solvers.cpp @@ -89,7 +89,7 @@ Function: ebmc_baset::do_dplib int ebmc_baset::do_dplib() { - const namespacet ns(context); + const namespacet ns(symbol_table); if(cmdline.isset("outfile")) { @@ -126,7 +126,7 @@ Function: ebmc_baset::do_smt1 int ebmc_baset::do_smt1() { - const namespacet ns(context); + const namespacet ns(symbol_table); if(cmdline.isset("outfile")) { @@ -175,7 +175,7 @@ Function: ebmc_baset::do_smt2 int ebmc_baset::do_smt2() { - const namespacet ns(context); + const namespacet ns(symbol_table); if(cmdline.isset("outfile")) { @@ -224,7 +224,7 @@ Function: ebmc_baset::do_z3 int ebmc_baset::do_z3() { - const namespacet ns(context); + const namespacet ns(symbol_table); smt1_dect smt1_dec( ns, @@ -250,7 +250,7 @@ Function: ebmc_baset::do_cvc3 int ebmc_baset::do_cvc3() { - const namespacet ns(context); + const namespacet ns(symbol_table); smt1_dect smt1_dec( ns, @@ -276,7 +276,7 @@ Function: ebmc_baset::do_yices int ebmc_baset::do_yices() { - const namespacet ns(context); + const namespacet ns(symbol_table); smt1_dect smt1_dec( ns, @@ -302,7 +302,7 @@ Function: ebmc_baset::do_boolector int ebmc_baset::do_boolector() { - const namespacet ns(context); + const namespacet ns(symbol_table); smt1_dect smt1_dec( ns, @@ -332,7 +332,7 @@ int ebmc_baset::do_sat() if(cmdline.isset("no-netlist")) { - const namespacet ns(context); + const namespacet ns(symbol_table); boolbvt boolbv(ns, satcheck); return do_ebmc(boolbv, false); } @@ -355,7 +355,7 @@ Function: ebmc_baset::do_prover int ebmc_baset::do_prover() { #ifdef HAVE_PROVER - const namespacet ns(context); + const namespacet ns(symbol_table); prover_satt prover_sat(ns); return do_ebmc(prover_sat, false); #else @@ -379,7 +379,7 @@ Function: ebmc_baset::do_lifter int ebmc_baset::do_lifter() { #ifdef HAVE_PROVER - const namespacet ns(context); + const namespacet ns(symbol_table); liftert lifter(ns); return do_ebmc(lifter.prop_conv(), false); #else diff --git a/src/ebmc/interpolation/compute-interpolant.cpp b/src/ebmc/interpolation/compute-interpolant.cpp index 13fa086..10228cf 100644 --- a/src/ebmc/interpolation/compute-interpolant.cpp +++ b/src/ebmc/interpolation/compute-interpolant.cpp @@ -53,7 +53,7 @@ static void reverse_partitions( std::cout << i_bit_2 << std::endl; satcheckt solver1; - // namespacet ns(context); + // namespacet ns(symbol_table); i_bit_1.add_variables(solver1); i_bit_2.add_variables(solver1); @@ -78,7 +78,7 @@ static void reverse_partitions( } satcheckt solver2; - // namespacet ns(context); + // namespacet ns(symbol_table); i_bit_1.add_variables(solver2); i_bit_2.add_variables(solver2); diff --git a/src/ebmc/interpolation/interpolation_expr.cpp b/src/ebmc/interpolation/interpolation_expr.cpp index dfddc56..d5b23d6 100644 --- a/src/ebmc/interpolation/interpolation_expr.cpp +++ b/src/ebmc/interpolation/interpolation_expr.cpp @@ -91,7 +91,7 @@ int interpolationt::check_initial_state() satcheckt satcheck; boolbvt solver(satcheck); - namespacet ns(context); + namespacet ns(symbol_table); // check if I AND !P is satisfiable @@ -222,7 +222,7 @@ void interpolationt::build_variable_map( it!=symbols.end(); it++) { - namespacet ns(context); + namespacet ns(symbol_table); //const symbolt &symbol=ns.lookup(*it); //exprt e0(symbol_expr(symbol)); @@ -283,7 +283,7 @@ int interpolationt::iteration() return 1; } - namespacet ns(context); + namespacet ns(symbol_table); interpolatort interpolator; boolbvt solver(interpolator); solver.equality_propagation=false; @@ -411,7 +411,7 @@ bool interpolationt::reached_fixedpoint() if(new_interpolant.is_false()) return true; satcheckt solver; - namespacet ns(context); + namespacet ns(symbol_table); // "old" set of states status("interpolants.size() " + i2string(interpolants.size())); @@ -587,7 +587,7 @@ void interpolationt::build_partition1( prop_convt &solver) { status("build_partition1"); - namespacet ns(context); + namespacet ns(symbol_table); if(interpolants.empty()) { @@ -629,7 +629,7 @@ void interpolationt::build_partition2( prop_convt &solver) { status("build_partition2"); - namespacet ns(context); + namespacet ns(symbol_table); unsigned no_timeframes=bound+1; const exprt &op_invar=trans_expr->invar(); @@ -664,7 +664,7 @@ void interpolationt::build_property( status("build_property"); - namespacet ns(context); + namespacet ns(symbol_table); unsigned no_timeframes=bound+1; unsigned start; @@ -755,7 +755,7 @@ bool interpolationt::check_partition_one_implies_interpolant() if(new_interpolant.is_false()) return false; - namespacet ns(context); + namespacet ns(symbol_table); satcheckt solver; boolbvt boolbv(solver); boolbv.equality_propagation=false; @@ -825,7 +825,7 @@ bool interpolationt::check_partition_two_and_interpolant() if(new_interpolant.is_false()) return false; - namespacet ns(context); + namespacet ns(symbol_table); satcheckt solver; boolbvt boolbv(solver); boolbv.equality_propagation=false; @@ -860,7 +860,7 @@ int interpolationt::induction_step() { status("Induction Step"); - namespacet ns(context); + namespacet ns(symbol_table); satcheckt satcheck; boolbvt solver(satcheck); diff --git a/src/ebmc/interpolation/interpolation_netlist.cpp b/src/ebmc/interpolation/interpolation_netlist.cpp index 2e47807..e6cd141 100644 --- a/src/ebmc/interpolation/interpolation_netlist.cpp +++ b/src/ebmc/interpolation/interpolation_netlist.cpp @@ -126,7 +126,7 @@ int interpolationt_netlist::check_initial_state() { satcheckt satcheck; - namespacet ns(context); + namespacet ns(symbol_table); boolbvt solver(ns,satcheck); // check if I AND !P is satisfiable @@ -198,7 +198,7 @@ int interpolationt_netlist::iteration() ", bound="+i2string(bound)); //see if induction succeeds - namespacet ns(context); + namespacet ns(symbol_table); interpolatort interpolator; boolbvt solver(ns, interpolator); solver.equality_propagation=false; @@ -324,7 +324,7 @@ bool interpolationt_netlist::reached_fixedpoint() } */ satcheckt solver; - namespacet ns(context); + namespacet ns(symbol_table); bmc_mapt netlist_bmc_map_check; netlist_bmc_map_check.map_timeframes(working_netlist, bound+1, solver); @@ -816,7 +816,7 @@ int interpolationt_netlist::induction_step() { status("Induction Step"); - namespacet ns(context); + namespacet ns(symbol_table); interpolatort satcheck; boolbvt solver(ns, satcheck); @@ -928,7 +928,7 @@ void interpolationt_netlist::get_strengthened_interpolant( bool interpolationt_netlist::check_partition_one_implies_interpolant(const bit_interpolantt ¤t_inter) { - namespacet ns(context); + namespacet ns(symbol_table); interpolatort interpolator; boolbvt solver(ns, interpolator); @@ -961,7 +961,7 @@ bool interpolationt_netlist::check_partition_one_implies_interpolant(const bit_i bool interpolationt_netlist::check_partition_two_and_interpolant(const bit_interpolantt ¤t_inter) { - namespacet ns(context); + namespacet ns(symbol_table); interpolatort interpolator; boolbvt solver(ns, interpolator); @@ -1029,7 +1029,7 @@ else { // build_property(solver, bmc_map); propt::resultt dec_result = solver.prop_solve(); - namespacet ns(context); + namespacet ns(symbol_table); switch(dec_result) { diff --git a/src/ebmc/interpolation/interpolation_netlist_vmcai.cpp b/src/ebmc/interpolation/interpolation_netlist_vmcai.cpp index 379b7a0..690fb87 100644 --- a/src/ebmc/interpolation/interpolation_netlist_vmcai.cpp +++ b/src/ebmc/interpolation/interpolation_netlist_vmcai.cpp @@ -185,7 +185,7 @@ int interpolationt_netlist_vmcai::forward_iteration() status("Iteration "+i2string(forward_iteration_number)+ ", bound="+i2string(bound)); - namespacet ns(context); + namespacet ns(symbol_table); interpolatort interpolator; boolbvt solver(interpolator); solver.equality_propagation=false; @@ -301,7 +301,7 @@ bool interpolationt_netlist_vmcai::reached_fixedpoint( } satcheckt solver; - namespacet ns(context); + namespacet ns(symbol_table); netlist_bmc_mapt netlist_bmc_map_check; netlist_bmc_map_check.map_timeframes(netlist, bound+1, solver); @@ -549,7 +549,7 @@ void interpolationt_netlist_vmcai::build_forward_property( { status("interpolationt_netlist_vmcai::build_property"); - // namespacet ns(context); + // namespacet ns(symbol_table); unsigned no_timeframes=bound+1; prop_bv.clear(); @@ -580,7 +580,7 @@ void interpolationt_netlist_vmcai::build_forward_property( bool interpolationt_netlist_vmcai::is_property() { satcheckt solver; - namespacet ns(context); + namespacet ns(symbol_table); boolbvt solverbv(solver); netlist_bmc_mapt netlist_bmc_map_init; @@ -653,7 +653,7 @@ int interpolationt_netlist_vmcai::check_forward_reachable_states() return 0; } std::cout << "checking forward reachable states\n"; - namespacet ns(context); + namespacet ns(symbol_table); satcheckt satcheck; boolbvt solver(satcheck); unsigned check_bound = 2; @@ -717,7 +717,7 @@ int interpolationt_netlist_vmcai::Refine_Interpolant( bool forward) { std::vector *fault_locations = forward ? &forward_fault_locations : &backward_fault_locations; - namespacet ns(context); + namespacet ns(symbol_table); status("SAT::Refine Interpolant"); if(forward) forward_refinement = true; @@ -900,7 +900,7 @@ int interpolationt_netlist_vmcai::backward_iteration() status("Iteration "+i2string(backward_iteration_number)+ ", bound="+i2string(bound)); - namespacet ns(context); + namespacet ns(symbol_table); interpolatort interpolator; boolbvt solver(interpolator); solver.equality_propagation=false; @@ -975,7 +975,7 @@ int interpolationt_netlist_vmcai::backward_iteration() int interpolationt_netlist_vmcai::check_backward_reachable_states() { - namespacet ns(context); + namespacet ns(symbol_table); satcheckt satcheck; boolbvt solver(satcheck); unsigned check_bound = 2; @@ -1038,7 +1038,7 @@ void interpolationt_netlist_vmcai::build_backward_property( { status("build_property"); - namespacet ns(context); + namespacet ns(symbol_table); prop_bv.clear(); bvt all_prop_bv; @@ -1069,7 +1069,7 @@ void interpolationt_netlist_vmcai::build_backward_partition1(interpolatort &solv ::unwind(netlist, netlist_bmc_map, *this, solver, false, bound); ::unwind(netlist, netlist_bmc_map, *this, solver, false, bound-1); - namespacet ns(context); + namespacet ns(symbol_table); bvt all_prop_bv; for(unsigned p_no=0; p_noback(); satcheckt solver; - namespacet ns(context); + namespacet ns(symbol_table); netlist_bmc_mapt netlist_bmc_map_check; netlist_bmc_map_check.map_timeframes(netlist, bound+1, solver); diff --git a/src/ebmc/interpolation/interpolation_word.cpp b/src/ebmc/interpolation/interpolation_word.cpp index ff5c401..457e31d 100644 --- a/src/ebmc/interpolation/interpolation_word.cpp +++ b/src/ebmc/interpolation/interpolation_word.cpp @@ -177,7 +177,7 @@ int interpolationt_word::check_initial_state() { status("Checking initial state"); - namespacet ns(context); + namespacet ns(symbol_table); satcheckt satcheck; boolbvt solver(ns, satcheck); @@ -305,7 +305,7 @@ void interpolationt_word::build_variable_map( it!=symbols.end(); it++) { - namespacet ns(context); + namespacet ns(symbol_table); exprt e0(*it); exprt e1(*it); @@ -394,7 +394,7 @@ int interpolationt_word::iteration() return 1; } - namespacet ns(context); + namespacet ns(symbol_table); interpolatort interpolator; boolbvt solver(ns, interpolator); solver.equality_propagation=false; @@ -540,7 +540,7 @@ bool interpolationt_word::reached_fixedpoint() if(new_interpolant.is_false()) return true; satcheckt solver; - namespacet ns(context); + namespacet ns(symbol_table); boolbvt prop_conv(ns, solver); build_variable_map(prop_conv); // "old" set of states @@ -661,7 +661,7 @@ void interpolationt_word::get_interpolant( // interpolant = do_word_interpolation.get_interpolant(1); } - namespacet ns(context); + namespacet ns(symbol_table); simplify(interpolant, ns); /* { @@ -716,7 +716,7 @@ void interpolationt_word::build_partition1( prop_convt &solver) { status("build_partition1"); - namespacet ns(context); + namespacet ns(symbol_table); if(interpolants.empty()) { @@ -761,7 +761,7 @@ void interpolationt_word::build_partition2( prop_convt &solver) { status("build_partition2"); - namespacet ns(context); + namespacet ns(symbol_table); unsigned no_timeframes=bound+1; const exprt &op_invar=trans_expr->invar(); @@ -798,7 +798,7 @@ void interpolationt_word::build_property( status("build_property"); - namespacet ns(context); + namespacet ns(symbol_table); unsigned no_timeframes=bound+1; unsigned start; @@ -889,7 +889,7 @@ int interpolationt_word::induction_step() { status("Induction Step"); - namespacet ns(context); + namespacet ns(symbol_table); satcheckt satcheck; boolbvt solver(ns, satcheck); @@ -1032,7 +1032,7 @@ void interpolationt_word::instantiate_with_if_lifting(prop_convt &solver, { exprt tmp(expr); - namespacet ns(context); + namespacet ns(symbol_table); // std::cout << "tmp is " << tmp.pretty() << std::endl; rewrite_ift rewrite_if(tmp); rewrite_if(); @@ -1048,7 +1048,7 @@ literalt interpolationt_word::instantiate_convert_with_if_lifting(prop_convt &so { exprt tmp(expr); - namespacet ns(context); + namespacet ns(symbol_table); rewrite_ift rewrite_if(tmp); rewrite_if(); @@ -1063,7 +1063,7 @@ bool interpolationt_word::check_partition_one_implies_interpolant(const exprt &t if(t.is_false()) return false; - namespacet ns(context); + namespacet ns(symbol_table); satcheckt solver; boolbvt boolbv(ns, solver); // boolbv.equality_propagation=false; @@ -1131,7 +1131,7 @@ bool interpolationt_word::check_partition_two_and_interpolant(const exprt &t) if(t.is_false()) return false; - namespacet ns(context); + namespacet ns(symbol_table); satcheckt solver; boolbvt boolbv(ns, solver); boolbv.equality_propagation=false; diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp index f257c94..4c73c3e 100644 --- a/src/ebmc/k_induction.cpp +++ b/src/ebmc/k_induction.cpp @@ -106,7 +106,7 @@ int k_inductiont::induction_base() status("Induction Base"); satcheckt satcheck; - namespacet ns(context); + namespacet ns(symbol_table); boolbvt solver(ns, satcheck); unwind(solver, bound+1, true); @@ -129,7 +129,7 @@ int k_inductiont::induction_base() { result("SAT: bug found"); - namespacet ns(context); + namespacet ns(symbol_table); trans_tracet trans_trace; compute_trans_trace( @@ -186,7 +186,7 @@ int k_inductiont::induction_step() { status("Induction Step"); - namespacet ns(context); + namespacet ns(symbol_table); satcheckt satcheck; boolbvt solver(ns, satcheck); diff --git a/src/ebmc/output_verilog.cpp b/src/ebmc/output_verilog.cpp index c74abc1..f35f0c2 100644 --- a/src/ebmc/output_verilog.cpp +++ b/src/ebmc/output_verilog.cpp @@ -328,7 +328,7 @@ void output_verilog_rtlt::assign_symbol( throw 0; } - const symbolt &symbol=namespacet(context).lookup(symbol_expr); + const symbolt &symbol=namespacet(symbol_table).lookup(symbol_expr); if(symbol.is_state_var) { @@ -378,7 +378,7 @@ void output_verilog_rtlt::convert_expr(const exprt &expr) expr2verilogt expr2verilog; // simplify first - namespacet ns(context); + namespacet ns(symbol_table); exprt tmp(expr); simplify(tmp,ns); @@ -459,10 +459,10 @@ std::string output_verilog_netlistt::symbol_string(const exprt &expr) else if(expr.id()==ID_symbol) { const irep_idt &identifier=expr.get(ID_identifier); - contextt::symbolst::const_iterator s_it= - context.symbols.find(identifier); + symbol_tablet::symbolst::const_iterator s_it= + symbol_table.symbols.find(identifier); - if(s_it==context.symbols.end()) + if(s_it==symbol_table.symbols.end()) { err_location(expr); str << "symbol " << identifier << " not found" @@ -481,10 +481,10 @@ std::string output_verilog_netlistt::symbol_string(const exprt &expr) else if(expr.id()==ID_next_symbol) { const irep_idt &identifier=expr.get(ID_identifier); - contextt::symbolst::const_iterator s_it= - context.symbols.find(identifier); + symbol_tablet::symbolst::const_iterator s_it= + symbol_table.symbols.find(identifier); - if(s_it==context.symbols.end()) + if(s_it==symbol_table.symbols.end()) { err_location(expr); str << "symbol " << identifier << " not found" @@ -654,14 +654,14 @@ void output_verilog_netlistt::latches(const irep_idt &module) { bool found=false; - forall_symbol_module_map(m_it, context.symbol_module_map, module) + forall_symbol_module_map(m_it, symbol_table.symbol_module_map, module) { const irep_idt &identifier=m_it->second; - contextt::symbolst::const_iterator s_it= - context.symbols.find(identifier); + symbol_tablet::symbolst::const_iterator s_it= + symbol_table.symbols.find(identifier); - if(s_it==context.symbols.end()) + if(s_it==symbol_table.symbols.end()) { str << "failed to find symbol " << identifier << std::endl; @@ -705,14 +705,14 @@ void output_verilog_rtlt::latches(const irep_idt &module) { bool found=false; - forall_symbol_module_map(m_it, context.symbol_module_map, module) + forall_symbol_module_map(m_it, symbol_table.symbol_module_map, module) { const irep_idt &identifier=m_it->second; - contextt::symbolst::const_iterator s_it= - context.symbols.find(identifier); + symbol_tablet::symbolst::const_iterator s_it= + symbol_table.symbols.find(identifier); - if(s_it==context.symbols.end()) + if(s_it==symbol_table.symbols.end()) { str << "failed to find symbol " << identifier << std::endl; @@ -753,14 +753,14 @@ void output_verilog_baset::wires(const irep_idt &module) { bool found=false; - forall_symbol_module_map(m_it, context.symbol_module_map, module) + forall_symbol_module_map(m_it, symbol_table.symbol_module_map, module) { const irep_idt &identifier=m_it->second; - contextt::symbolst::const_iterator s_it= - context.symbols.find(identifier); + symbol_tablet::symbolst::const_iterator s_it= + symbol_table.symbols.find(identifier); - if(s_it==context.symbols.end()) + if(s_it==symbol_table.symbols.end()) { str << "failed to find symbol " << identifier << std::endl; diff --git a/src/ebmc/output_verilog.h b/src/ebmc/output_verilog.h index eeafdc2..fb570ed 100644 --- a/src/ebmc/output_verilog.h +++ b/src/ebmc/output_verilog.h @@ -16,11 +16,11 @@ class output_verilog_baset:public message_streamt { public: output_verilog_baset( - const contextt &_context, + const symbol_tablet &_symbol_table, std::ostream &_out, message_handlert &_message_handler): message_streamt(_message_handler), - context(_context), out(_out) + symbol_table(_symbol_table), out(_out) { } @@ -29,7 +29,7 @@ public: protected: // common - const contextt &context; + const symbol_tablet &symbol_table; std::ostream &out; unsigned count; @@ -62,10 +62,10 @@ class output_verilog_netlistt:public output_verilog_baset { public: output_verilog_netlistt( - const contextt &_context, + const symbol_tablet &_symbol_table, std::ostream &_out, message_handlert &_message_handler): - output_verilog_baset(_context, _out, _message_handler) + output_verilog_baset(_symbol_table, _out, _message_handler) { } @@ -90,10 +90,10 @@ class output_verilog_rtlt:public output_verilog_baset { public: output_verilog_rtlt( - const contextt &_context, + const symbol_tablet &_symbol_table, std::ostream &_out, message_handlert &_message_handler): - output_verilog_baset(_context, _out, _message_handler) + output_verilog_baset(_symbol_table, _out, _message_handler) { } diff --git a/src/ebmc/parseoptions.cpp b/src/ebmc/parseoptions.cpp index 8b026ee..f30219d 100644 --- a/src/ebmc/parseoptions.cpp +++ b/src/ebmc/parseoptions.cpp @@ -64,8 +64,8 @@ int ebmc_parseoptionst::doit() if(cmdline.isset("cegar")) { #if 0 - namespacet ns(context); - var_mapt var_map(context, main_symbol->name); + namespacet ns(symbol_table); + var_mapt var_map(symbol_table, main_symbol->name); bmc_cegart bmc_cegar( var_map, diff --git a/src/ebmc/show_trans.cpp b/src/ebmc/show_trans.cpp index 2c60029..61389b5 100644 --- a/src/ebmc/show_trans.cpp +++ b/src/ebmc/show_trans.cpp @@ -90,7 +90,7 @@ Function: show_transt::show_trans_verilog_netlist int show_transt::show_trans_verilog_netlist(std::ostream &out) { output_verilog_netlistt output_verilog( - context, out, get_message_handler()); + symbol_table, out, get_message_handler()); try { @@ -134,7 +134,7 @@ Function: show_transt::show_trans_verilog_rtl int show_transt::show_trans_verilog_rtl(std::ostream &out) { output_verilog_rtlt output_verilog( - context, out, get_message_handler()); + symbol_table, out, get_message_handler()); try { diff --git a/src/hw-cbmc/gen_interface.cpp b/src/hw-cbmc/gen_interface.cpp index 750f95e..6549e03 100644 --- a/src/hw-cbmc/gen_interface.cpp +++ b/src/hw-cbmc/gen_interface.cpp @@ -19,15 +19,15 @@ Author: Daniel Kroening, kroening@kroening.com class gen_interfacet { public: - gen_interfacet(contextt &_context, + gen_interfacet(symbol_tablet &_symbol_table, std::ostream &_out, std::ostream &_err): - context(_context), out(_out), err(_err) { } + symbol_table(_symbol_table), out(_out), err(_err) { } void gen_interface(const symbolt &module, bool have_bound); protected: - contextt &context; + symbol_tablet &symbol_table; std::ostream &out, &err; std::set modules_done; @@ -58,10 +58,10 @@ Function: gen_interfacet::lookup symbolt &gen_interfacet::lookup(const irep_idt &identifier) { - contextt::symbolst::iterator it= - context.symbols.find(identifier); + symbol_tablet::symbolst::iterator it= + symbol_table.symbols.find(identifier); - if(it==context.symbols.end()) + if(it==symbol_table.symbols.end()) { err << "failed to find identifier " << identifier << std::endl; throw 0; @@ -215,7 +215,7 @@ void gen_interfacet::gen_module( std::set::iterator in_progress_it=modules_in_progress.insert(module.name).first; - forall_symbol_module_map(it, context.symbol_module_map, module.name) + forall_symbol_module_map(it, symbol_table.symbol_module_map, module.name) { const symbolt &symbol=lookup(it->second); @@ -233,7 +233,7 @@ void gen_interfacet::gen_module( os << "struct module_" << module.base_name << " {" << std::endl; - forall_symbol_module_map(it, context.symbol_module_map, module.name) + forall_symbol_module_map(it, symbol_table.symbol_module_map, module.name) { const symbolt &symbol=lookup(it->second); @@ -327,12 +327,12 @@ Function: gen_interfacet::gen_interface \*******************************************************************/ void gen_interface( - contextt &context, + symbol_tablet &symbol_table, const symbolt &module, bool have_bound, std::ostream &out, std::ostream &err) { - gen_interfacet gen_interface(context, out, err); + gen_interfacet gen_interface(symbol_table, out, err); gen_interface.gen_interface(module, have_bound); } diff --git a/src/hw-cbmc/gen_interface.h b/src/hw-cbmc/gen_interface.h index 8183510..5c02b0a 100644 --- a/src/hw-cbmc/gen_interface.h +++ b/src/hw-cbmc/gen_interface.h @@ -11,10 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include void gen_interface( - contextt &context, + symbol_tablet &symbol_table, const symbolt &module, bool have_bound, std::ostream &out, diff --git a/src/hw-cbmc/hw_bmc.h b/src/hw-cbmc/hw_bmc.h index 7dfc429..28e4ae7 100644 --- a/src/hw-cbmc/hw_bmc.h +++ b/src/hw-cbmc/hw_bmc.h @@ -16,9 +16,9 @@ class hw_bmct:public bmct public: hw_bmct( const optionst &_options, - const contextt &_context, + const symbol_tablet &_symbol_table, message_handlert &_message_handler): - bmct(_options, _context, _message_handler) + bmct(_options, _symbol_table, _message_handler) { } diff --git a/src/hw-cbmc/map_vars.cpp b/src/hw-cbmc/map_vars.cpp index 7417250..7f51f39 100644 --- a/src/hw-cbmc/map_vars.cpp +++ b/src/hw-cbmc/map_vars.cpp @@ -60,17 +60,17 @@ void instantiate_symbol(exprt &expr, unsigned timeframe) class map_varst:public message_streamt { public: - map_varst(contextt &_context, expr_listt &_constraints, + map_varst(symbol_tablet &_symbol_table, expr_listt &_constraints, message_handlert &_message, unsigned _no_timeframes): message_streamt(_message), - context(_context), constraints(_constraints), + symbol_table(_symbol_table), constraints(_constraints), no_timeframes(_no_timeframes) { } void map_vars(const irep_idt &module); protected: - contextt &context; + symbol_tablet &symbol_table; expr_listt &constraints; unsigned no_timeframes; std::set top_level_inputs; @@ -115,7 +115,7 @@ protected: mp_integer s; if(to_integer(size_expr, s)) { - namespacet ns(context); + namespacet ns(symbol_table); str << "failed to convert array size `" << from_expr(ns, "", size_expr) << "'"; error(); @@ -140,10 +140,10 @@ Function: map_varst::lookup symbolt &map_varst::lookup(const irep_idt &identifier) { - contextt::symbolst::iterator it= - context.symbols.find(identifier); + symbol_tablet::symbolst::iterator it= + symbol_table.symbols.find(identifier); - if(it==context.symbols.end()) + if(it==symbol_table.symbols.end()) { str << "failed to find identifier `" << identifier << "'"; @@ -239,7 +239,7 @@ bool map_varst::array_types_eq( return true; } - namespacet ns(context); + namespacet ns(symbol_table); const typet &s1=ns.follow(type1.subtype()); const typet &s2=ns.follow(type2.subtype()); @@ -275,7 +275,7 @@ bool map_varst::check_types_rec( const typet &type2, std::string &error_msg) { - namespacet ns(context); + namespacet ns(symbol_table); if(type1.id()==ID_symbol) return check_types_rec(ns.follow(type1), type2, error_msg); @@ -353,7 +353,7 @@ void map_varst::add_constraint_rec( const exprt &program_symbol, const exprt &module_symbol) { - namespacet ns(context); + namespacet ns(symbol_table); const typet &t1=ns.follow(program_symbol.type()); const typet &t2=ns.follow(module_symbol.type()); @@ -402,7 +402,7 @@ void map_varst::map_var( // rhs: symbol exprt e2=symbol_exprt(module_symbol.name, module_symbol.type); - namespacet ns(context); + namespacet ns(symbol_table); ns.follow_macros(e2); instantiate_symbol(e2, transition); @@ -423,7 +423,7 @@ Function: map_varst::add_array const symbolt &map_varst::add_array(symbolt &symbol) { - const namespacet ns(context); + const namespacet ns(symbol_table); const typet &full_type=ns.follow(symbol.type); @@ -449,8 +449,8 @@ const symbolt &map_varst::add_array(symbolt &symbol) new_symbol.base_name=id2string(new_symbol.base_name)+"_array"; symbolt *p; - if(context.move(new_symbol, p)) - throw "context.move() failed"; + if(symbol_table.move(new_symbol, p)) + throw "symbol_table.move() failed"; // change initialization exprt symbol_expr(ID_symbol, p->type); @@ -520,7 +520,7 @@ void map_varst::map_var_rec( const exprt &expr, const symbolt::hierarchyt &hierarchy) { - const namespacet ns(context); + const namespacet ns(symbol_table); const typet &expr_type=ns.follow(expr.type()); const struct_typet &struct_type=to_struct_type(expr_type); const struct_typet::componentst &components=struct_type.components(); @@ -546,7 +546,7 @@ void map_varst::map_var_rec( std::list symbols; - forall_symbol_module_map(s_it, context.symbol_module_map, main_module) + forall_symbol_module_map(s_it, symbol_table.symbol_module_map, main_module) { const symbolt &s=lookup(s_it->second); if(s.type.id()==ID_module) continue; @@ -617,7 +617,7 @@ void map_varst::map_var( // check types - const namespacet ns(context); + const namespacet ns(symbol_table); const typet &type1=ns.follow(program_symbol.type()); const typet &type2=ns.follow(module_symbol.type); @@ -670,7 +670,7 @@ Function: map_varst::map_vars Outputs: - Purpose: Looks through context for external ANSI-C symbols + Purpose: Looks through symbol_table for external ANSI-C symbols Calls map_var to find mapping to HDL \*******************************************************************/ @@ -688,14 +688,14 @@ void map_varst::map_vars(const irep_idt &module) timeframe_symbol.is_lvalue=true; timeframe_symbol.value=gen_zero(index_type()); - context.move(timeframe_symbol); + symbol_table.move(timeframe_symbol); } const symbolt &module_symbol=lookup(module); irep_idt struct_symbol; - Forall_symbols(it, context.symbols) + Forall_symbols(it, symbol_table.symbols) { if(it->second.mode==ID_C || it->second.mode==ID_cpp || @@ -739,7 +739,7 @@ void map_varst::map_vars(const irep_idt &module) exprt timeframe_expr=from_integer(0, index_type()); - namespacet ns(context); + namespacet ns(symbol_table); exprt expr(ID_index, ns.follow(symbol_expr.type()).subtype()); expr.move_to_operands(symbol_expr, timeframe_expr); @@ -749,7 +749,7 @@ void map_varst::map_vars(const irep_idt &module) map_var_rec(module_symbol.name, expr, hierarchy); } - Forall_symbols(it, context.symbols) + Forall_symbols(it, symbol_table.symbols) { if(it->second.mode==ID_C || it->second.mode==ID_cpp || @@ -760,13 +760,13 @@ void map_varst::map_vars(const irep_idt &module) if(base_name=="next_timeframe" && it->second.type.id()==ID_code) { - namespacet ns(context); + namespacet ns(symbol_table); add_next_timeframe(it->second, struct_symbol, top_level_inputs, ns); } else if(base_name=="set_inputs" && it->second.type.id()==ID_code) { - namespacet ns(context); + namespacet ns(symbol_table); add_set_inputs(it->second, struct_symbol, top_level_inputs, ns); } } @@ -786,12 +786,12 @@ Function: map_vars \*******************************************************************/ void map_vars( - contextt &context, + symbol_tablet &symbol_table, const irep_idt &module, expr_listt &constraints, message_handlert &message, unsigned no_timeframes) { - map_varst map_vars(context, constraints, message, no_timeframes); + map_varst map_vars(symbol_table, constraints, message, no_timeframes); map_vars.map_vars(module); } diff --git a/src/hw-cbmc/map_vars.h b/src/hw-cbmc/map_vars.h index 9f76421..abd790f 100644 --- a/src/hw-cbmc/map_vars.h +++ b/src/hw-cbmc/map_vars.h @@ -11,11 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include void map_vars( - contextt &context, + symbol_tablet &symbol_table, const irep_idt &module, expr_listt &constraints, message_handlert &message, diff --git a/src/hw-cbmc/parseoptions.cpp b/src/hw-cbmc/parseoptions.cpp index c8187ac..9ff7675 100644 --- a/src/hw-cbmc/parseoptions.cpp +++ b/src/hw-cbmc/parseoptions.cpp @@ -66,7 +66,7 @@ int hw_cbmc_parseoptionst::doit() if(cmdline.isset("vcd")) options.set_option("vcd", cmdline.getval("vcd")); - hw_bmct bmc(options, context, ui_message_handler); + hw_bmct bmc(options, symbol_table, ui_message_handler); set_verbosity(bmc); set_verbosity(*this); @@ -85,7 +85,7 @@ int hw_cbmc_parseoptionst::doit() if(cmdline.isset("show-claims")) { - const namespacet ns(context); + const namespacet ns(symbol_table); show_claims(ns, get_ui(), goto_functions); return 0; } @@ -123,11 +123,11 @@ bool hw_cbmc_parseoptionst::get_modules(bmct &bmc) try { const symbolt &symbol= - get_module(context, module, get_message_handler()); + get_module(symbol_table, module, get_message_handler()); if(cmdline.isset("gen-interface")) { - gen_interface(context, symbol, true, std::cout, std::cerr); + gen_interface(symbol_table, symbol, true, std::cout, std::cerr); return true; } @@ -147,7 +147,7 @@ bool hw_cbmc_parseoptionst::get_modules(bmct &bmc) status("Mapping variables"); map_vars( - context, + symbol_table, symbol.name, hw_bmc.bmc_constraints, ui_message_handler, @@ -163,7 +163,7 @@ bool hw_cbmc_parseoptionst::get_modules(bmct &bmc) } else if(cmdline.isset("show-modules")) { - show_modules(context, get_ui()); + show_modules(symbol_table, get_ui()); return true; } diff --git a/src/smvlang/smv_language.cpp b/src/smvlang/smv_language.cpp index 84770c4..c28bb20 100644 --- a/src/smvlang/smv_language.cpp +++ b/src/smvlang/smv_language.cpp @@ -116,11 +116,11 @@ Function: smv_languaget::typecheck \*******************************************************************/ bool smv_languaget::typecheck( - contextt &context, + symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler) { - return smv_typecheck(smv_parse_tree, context, module, message_handler); + return smv_typecheck(smv_parse_tree, symbol_table, module, message_handler); } /*******************************************************************\ diff --git a/src/smvlang/smv_language.h b/src/smvlang/smv_language.h index 12b6cb6..3d716d3 100644 --- a/src/smvlang/smv_language.h +++ b/src/smvlang/smv_language.h @@ -34,7 +34,7 @@ public: std::set &module_set); virtual bool typecheck( - contextt &context, + symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler); diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 7d9d713..294b691 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -26,13 +26,13 @@ class smv_typecheckt:public typecheckt public: smv_typecheckt( smv_parse_treet &_smv_parse_tree, - contextt &_context, + symbol_tablet &_symbol_table, const std::string &_module, bool _do_spec, message_handlert &_message_handler): typecheckt(_message_handler), smv_parse_tree(_smv_parse_tree), - context(_context), + symbol_table(_symbol_table), module(_module), do_spec(_do_spec) { @@ -65,7 +65,7 @@ public: protected: smv_parse_treet &smv_parse_tree; - contextt &context; + symbol_tablet &symbol_table; const std::string &module; bool do_spec; @@ -246,10 +246,10 @@ void smv_typecheckt::instantiate( const exprt::operandst &operands, const irept &location) { - contextt::symbolst::const_iterator s_it= - context.symbols.find(identifier); + symbol_tablet::symbolst::const_iterator s_it= + symbol_table.symbols.find(identifier); - if(s_it==context.symbols.end()) + if(s_it==symbol_table.symbols.end()) { err_location(location); str << "submodule `" @@ -295,12 +295,12 @@ void smv_typecheckt::instantiate( std::set var_identifiers; - forall_symbol_module_map(v_it, context.symbol_module_map, identifier) + forall_symbol_module_map(v_it, symbol_table.symbol_module_map, identifier) { - contextt::symbolst::const_iterator s_it2= - context.symbols.find(v_it->second); + symbol_tablet::symbolst::const_iterator s_it2= + symbol_table.symbols.find(v_it->second); - if(s_it2==context.symbols.end()) + if(s_it2==symbol_table.symbols.end()) { str << "symbol `" << v_it->second << "' not found"; throw 0; @@ -325,7 +325,7 @@ void smv_typecheckt::instantiate( var_identifiers.insert(symbol.name); - context.move(symbol); + symbol_table.move(symbol); } } @@ -336,10 +336,10 @@ void smv_typecheckt::instantiate( v_it!=var_identifiers.end(); v_it++) { - contextt::symbolst::iterator s_it2= - context.symbols.find(*v_it); + symbol_tablet::symbolst::iterator s_it2= + symbol_table.symbols.find(*v_it); - if(s_it2==context.symbols.end()) + if(s_it2==symbol_table.symbols.end()) { str << "symbol `" << *v_it << "' not found"; throw 0; @@ -584,9 +584,9 @@ void smv_typecheckt::typecheck( if(define_map.find(identifier)!=define_map.end()) convert_define(identifier); - contextt::symbolst::iterator s_it=context.symbols.find(identifier); + symbol_tablet::symbolst::iterator s_it=symbol_table.symbols.find(identifier); - if(s_it==context.symbols.end()) + if(s_it==symbol_table.symbols.end()) { err_location(expr); str << "variable `" << identifier << "' not found"; @@ -1173,7 +1173,7 @@ void smv_typecheckt::convert(smv_parse_treet::mc_varst &vars) symbol.is_state_var=false; symbol.type=var.type; - context.add(symbol); + symbol_table.add(symbol); } } @@ -1202,9 +1202,9 @@ void smv_typecheckt::collect_define(const exprt &expr) const irep_idt &identifier=op0.get(ID_identifier); - contextt::symbolst::iterator it=context.symbols.find(identifier); + symbol_tablet::symbolst::iterator it=symbol_table.symbols.find(identifier); - if(it==context.symbols.end()) + if(it==symbol_table.symbols.end()) { str << "collect_define failed to find symbol `" << identifier << "'"; @@ -1253,9 +1253,9 @@ void smv_typecheckt::convert_define(const irep_idt &identifier) throw 0; } - contextt::symbolst::iterator it=context.symbols.find(identifier); + symbol_tablet::symbolst::iterator it=symbol_table.symbols.find(identifier); - if(it==context.symbols.end()) + if(it==symbol_table.symbols.end()) { str << "convert_define failed to find symbol `" << identifier << "'"; @@ -1372,7 +1372,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module) Forall_operands(it, trans) gen_and(*it); - context.move(module_symbol); + symbol_table.move(module_symbol); // spec @@ -1394,7 +1394,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module) spec_symbol.value=it->expr; spec_symbol.location=it->location; - context.move(spec_symbol); + symbol_table.move(spec_symbol); } } } @@ -1438,13 +1438,13 @@ Function: smv_typecheck bool smv_typecheck( smv_parse_treet &smv_parse_tree, - contextt &context, + symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler, bool do_spec) { smv_typecheckt smv_typecheck( - smv_parse_tree, context, module, do_spec, message_handler); + smv_parse_tree, symbol_table, module, do_spec, message_handler); return smv_typecheck.typecheck_main(); } diff --git a/src/smvlang/smv_typecheck.h b/src/smvlang/smv_typecheck.h index 9212ca7..a3e79c7 100644 --- a/src/smvlang/smv_typecheck.h +++ b/src/smvlang/smv_typecheck.h @@ -9,14 +9,14 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SMV_TYPECHECK_H #define CPROVER_SMV_TYPECHECK_H -#include +#include #include #include "smv_parse_tree.h" bool smv_typecheck( smv_parse_treet &smv_parse_tree, - contextt &context, + symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler, bool do_spec=true); diff --git a/src/trans/counterexample.cpp b/src/trans/counterexample.cpp index 10684df..851e51e 100644 --- a/src/trans/counterexample.cpp +++ b/src/trans/counterexample.cpp @@ -113,9 +113,9 @@ void show_state( std::cout << "Transition system state " << timeframe << "\n"; std::cout << "----------------------------------------------------\n"; - const contextt &context=ns.get_context(); + const symbol_tablet &symbol_table=ns.get_symbol_table(); - forall_symbol_module_map(it, context.symbol_module_map, module) + forall_symbol_module_map(it, symbol_table.symbol_module_map, module) { const symbolt &symbol=ns.lookup(it->second); diff --git a/src/trans/netlist_trans.cpp b/src/trans/netlist_trans.cpp index a619e1d..91eacd6 100644 --- a/src/trans/netlist_trans.cpp +++ b/src/trans/netlist_trans.cpp @@ -31,11 +31,11 @@ class convert_trans_to_netlistt { public: convert_trans_to_netlistt( - contextt &_context, + symbol_tablet &_symbol_table, netlistt &_dest, messaget &_message): - context(_context), - ns(_context), + symbol_table(_symbol_table), + ns(_symbol_table), dest(_dest), message(_message) { @@ -46,7 +46,7 @@ public: const std::list &properties); protected: - contextt &context; + symbol_tablet &symbol_table; const namespacet ns; netlistt &dest; messaget &message; @@ -153,14 +153,14 @@ literalt convert_trans_to_netlistt::new_input() { irep_idt id="convert::input"; - if(context.symbols.find(id)==context.symbols.end()) + if(symbol_table.symbols.find(id)==symbol_table.symbols.end()) { symbolt symbol; symbol.name=id; symbol.type=bool_typet(); symbol.is_input=true; symbol.base_name="input"; - context.move(symbol); + symbol_table.move(symbol); } var_mapt::vart &var=dest.var_map.map[id]; @@ -191,13 +191,13 @@ void convert_trans_to_netlistt::map_vars( { boolbv_widtht boolbv_width(ns); - forall_symbol_module_map(it, context.symbol_module_map, + forall_symbol_module_map(it, symbol_table.symbol_module_map, module) { - contextt::symbolst::const_iterator s_it= - context.symbols.find(it->second); + symbol_tablet::symbolst::const_iterator s_it= + symbol_table.symbols.find(it->second); - if(s_it==context.symbols.end()) + if(s_it==symbol_table.symbols.end()) continue; const symbolt &symbol=s_it->second; @@ -285,7 +285,7 @@ void convert_trans_to_netlistt::operator()( } } - const symbolt &module_symbol=namespacet(context).lookup(module); + const symbolt &module_symbol=namespacet(symbol_table).lookup(module); const transt &trans=to_trans_expr(module_symbol.value); // build the net-list @@ -744,13 +744,13 @@ Function: convert_trans_to_netlist \*******************************************************************/ void convert_trans_to_netlist( - contextt &context, + symbol_tablet &symbol_table, const irep_idt &module, const std::list &properties, netlistt &dest, messaget &message) { - convert_trans_to_netlistt c(context, dest, message); + convert_trans_to_netlistt c(symbol_table, dest, message); c(module, properties); } diff --git a/src/trans/netlist_trans.h b/src/trans/netlist_trans.h index ce26814..05c805a 100644 --- a/src/trans/netlist_trans.h +++ b/src/trans/netlist_trans.h @@ -11,11 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include void convert_trans_to_netlist( - contextt &context, + symbol_tablet &symbol_table, const irep_idt &module, const std::list &properties, class netlistt &dest, diff --git a/src/trans/property.h b/src/trans/property.h index 057f6eb..de2fa66 100644 --- a/src/trans/property.h +++ b/src/trans/property.h @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_TRANS_PROPERTY_H #define CPROVER_TRANS_PROPERTY_H -#include +#include #include #include diff --git a/src/trans/show_modules.cpp b/src/trans/show_modules.cpp index 00f21b2..8bb9b99 100644 --- a/src/trans/show_modules.cpp +++ b/src/trans/show_modules.cpp @@ -28,12 +28,12 @@ Function: show_modules \*******************************************************************/ void show_modules( - const contextt &context, + const symbol_tablet &symbol_table, ui_message_handlert::uit ui) { unsigned count=0; - forall_symbols(it, context.symbols) + forall_symbols(it, symbol_table.symbols) { const symbolt &symbol=it->second; diff --git a/src/trans/show_modules.h b/src/trans/show_modules.h index 95aa795..b95abac 100644 --- a/src/trans/show_modules.h +++ b/src/trans/show_modules.h @@ -10,10 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_TRANS_SHOW_MODULES_H #include -#include +#include void show_modules( - const contextt &context, + const symbol_tablet &symbol_table, ui_message_handlert::uit ui); #endif diff --git a/src/trans/trans_trace.cpp b/src/trans/trans_trace.cpp index f9af9ec..24ce792 100644 --- a/src/trans/trans_trace.cpp +++ b/src/trans/trans_trace.cpp @@ -117,12 +117,12 @@ void compute_trans_trace( for(unsigned t=0; tsecond); diff --git a/src/trans/var_map.h b/src/trans/var_map.h index b3c74cb..58b2894 100644 --- a/src/trans/var_map.h +++ b/src/trans/var_map.h @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include "bv_varid.h" diff --git a/src/verilog/verilog2expr.cpp b/src/verilog/verilog2expr.cpp index 8ecc5a6..582e103 100644 --- a/src/verilog/verilog2expr.cpp +++ b/src/verilog/verilog2expr.cpp @@ -1,7 +1,7 @@ #include "verilog2expr.h" bool verilog2expr(const string &code, exprt &expr, - const contextt &context, + const symbol_tablet &symbol_table, const sequentt &sequent, string &msg) { diff --git a/src/verilog/verilog2expr.h b/src/verilog/verilog2expr.h index c001649..a9092e8 100644 --- a/src/verilog/verilog2expr.h +++ b/src/verilog/verilog2expr.h @@ -1,7 +1,7 @@ #include "sequent.h" bool verilog2expr(const string &code, exprt &expr, - const contextt &context, + const symbol_tablet &symbol_table, const sequentt &sequent, string &msg); diff --git a/src/verilog/verilog_context.cpp b/src/verilog/verilog_context.cpp index 3f1dec6..a41f7cd 100644 --- a/src/verilog/verilog_context.cpp +++ b/src/verilog/verilog_context.cpp @@ -6,11 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include "verilog_context.h" +#include "verilog_symbol_table.h" /*******************************************************************\ -Function: verilog_contextt::context_lookup +Function: verilog_symbol_tablet::symbol_table_lookup Inputs: @@ -20,11 +20,11 @@ Function: verilog_contextt::context_lookup \*******************************************************************/ -symbolt &verilog_contextt::context_lookup(const irep_idt &identifier) +symbolt &verilog_symbol_tablet::symbol_table_lookup(const irep_idt &identifier) { - contextt::symbolst::iterator it=context.symbols.find(identifier); + symbol_tablet::symbolst::iterator it=symbol_table.symbols.find(identifier); - if(it==context.symbols.end()) + if(it==symbol_table.symbols.end()) throw "symbol "+id2string(identifier)+" not found"; return it->second; diff --git a/src/verilog/verilog_flattening.cpp b/src/verilog/verilog_flattening.cpp index a496d14..cb44483 100644 --- a/src/verilog/verilog_flattening.cpp +++ b/src/verilog/verilog_flattening.cpp @@ -244,12 +244,12 @@ void verilog_flatteningt::flatten_inst(verilog_instt &inst) { const irep_idt &identifier=inst.get("module"); - // must be in context + // must be in symbol_table const symbolt &symbol=lookup(identifier); // make sure it's flat already verilog_flattening( - context, identifier, get_message_handler(), options); + symbol_table, identifier, get_message_handler(), options); assert(symbol.value.id()=="flat_verilog_module"); @@ -283,7 +283,7 @@ void verilog_flatteningt::flatten_inst( std::list new_symbols; replace_mapt replace_map; - forall_symbol_module_map(it, context.symbol_module_map, symbol.module) + forall_symbol_module_map(it, symbol_table.symbol_module_map, symbol.module) { const symbolt &symbol=lookup(it->second); @@ -313,7 +313,7 @@ void verilog_flatteningt::flatten_inst( new_symbol.name=full_identifier; - if(context.add(new_symbol)) + if(symbol_table.add(new_symbol)) { str << "name collision during module instantiation: " << new_symbol.name; @@ -341,7 +341,7 @@ void verilog_flatteningt::flatten_inst( it!=new_symbols.end(); it++) { - symbolt &symbol=context_lookup(*it); + symbolt &symbol=symbol_table_lookup(*it); replace_symbols(replace_map, symbol.value); } @@ -433,7 +433,7 @@ Function: verilog_flatteningt::typecheck void verilog_flatteningt::typecheck() { - symbolt &symbol=context_lookup(module); + symbolt &symbol=symbol_table_lookup(module); // done already? if(symbol.value.id()=="flat_verilog_module") return; flatten_module(symbol); @@ -452,12 +452,12 @@ Function: verilog_flattening \*******************************************************************/ bool verilog_flattening( - contextt &context, + symbol_tablet &symbol_table, const irep_idt &module, message_handlert &message_handler, const optionst &options) { verilog_flatteningt verilog_flattening( - context, module, options, message_handler); + symbol_table, module, options, message_handler); return verilog_flattening.typecheck_main(); } diff --git a/src/verilog/verilog_flattening.h b/src/verilog/verilog_flattening.h index 902a8a2..8cd1f1f 100644 --- a/src/verilog/verilog_flattening.h +++ b/src/verilog/verilog_flattening.h @@ -22,10 +22,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "verilog_typecheck_base.h" -#include "verilog_context.h" +#include "verilog_symbol_table.h" bool verilog_flattening( - contextt &context, + symbol_tablet &symbol_table, const irep_idt &module, message_handlert &message_handler, const optionst &options); @@ -44,17 +44,17 @@ bool verilog_flattening( class verilog_flatteningt: public verilog_typecheck_baset, - public verilog_contextt + public verilog_symbol_tablet { public: verilog_flatteningt( - contextt &_context, + symbol_tablet &_symbol_table, const irep_idt &_module, const optionst &_options, message_handlert &_message_handler): verilog_typecheck_baset(ns, _message_handler), - verilog_contextt(_context), - ns(_context), + verilog_symbol_tablet(_symbol_table), + ns(_symbol_table), options(_options), module(_module) { diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index 8473476..2981291 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -138,7 +138,7 @@ void verilog_typecheckt::interface_ports(irept::subt &ports) symbolt *s; - if(context.move(new_symbol, s)) + if(symbol_table.move(new_symbol, s)) { err_location(decl.op0()); str << "port `" << name << "' is also declared"; @@ -211,7 +211,7 @@ void verilog_typecheckt::interface_function_or_task( id2string(symbol.module)+"."+ id2string(symbol.base_name); - if(context.move(symbol, new_symbol)) + if(symbol_table.move(symbol, new_symbol)) { err_location(decl); str << "symbol `" << symbol.base_name @@ -239,7 +239,7 @@ void verilog_typecheckt::interface_function_or_task( id2string(new_symbol->name)+"."+ id2string(new_symbol->base_name); - context.move(return_symbol); + symbol_table.move(return_symbol); } // do the declarations within the task/function @@ -377,9 +377,9 @@ void verilog_typecheckt::interface_function_or_task_decl(const verilog_declt &de if(input || output) { - contextt::symbolst::iterator s_it= - context.symbols.find(function_or_task_name); - assert(s_it!=context.symbols.end()); + symbol_tablet::symbolst::iterator s_it= + symbol_table.symbols.find(function_or_task_name); + assert(s_it!=symbol_table.symbols.end()); symbolt &function_or_task_symbol=s_it->second; code_typet::argumentst &arguments= to_code_type(function_or_task_symbol.type).arguments(); @@ -392,10 +392,10 @@ void verilog_typecheckt::interface_function_or_task_decl(const verilog_declt &de argument.set(ID_input, input); } - contextt::symbolst::iterator result= - context.symbols.find(symbol.name); + symbol_tablet::symbolst::iterator result= + symbol_table.symbols.find(symbol.name); - if(result!=context.symbols.end()) + if(result!=symbol_table.symbols.end()) { err_location(decl); str << "symbol `" << symbol.base_name @@ -403,7 +403,7 @@ void verilog_typecheckt::interface_function_or_task_decl(const verilog_declt &de throw 0; } - context.add(symbol); + symbol_table.add(symbol); } } @@ -527,11 +527,11 @@ void verilog_typecheckt::interface_module_decl(const verilog_declt &decl) id2string(symbol.module)+"."+ id2string(symbol.base_name); - contextt::symbolst::iterator result= - context.symbols.find(symbol.name); + symbol_tablet::symbolst::iterator result= + symbol_table.symbols.find(symbol.name); - if(result==context.symbols.end()) - context.add(symbol); + if(result==symbol_table.symbols.end()) + symbol_table.add(symbol); else { symbolt &osymbol=result->second; @@ -604,7 +604,7 @@ void verilog_typecheckt::interface_parameter(const exprt &expr) symbolt *new_symbol; - if(context.move(symbol, new_symbol)) + if(symbol_table.move(symbol, new_symbol)) { err_location(expr); str << "conflicting definition of symbol `" @@ -691,7 +691,7 @@ void verilog_typecheckt::interface_inst( id2string(symbol.base_name); symbol.value.set(ID_module, identifier); - if(context.add(symbol)) + if(symbol_table.add(symbol)) { err_location(op); str << "duplicate definition of identifier `" diff --git a/src/verilog/verilog_language.cpp b/src/verilog/verilog_language.cpp index 10fb0fc..cf86c05 100644 --- a/src/verilog/verilog_language.cpp +++ b/src/verilog/verilog_language.cpp @@ -156,18 +156,18 @@ Function: verilog_languaget::typecheck \*******************************************************************/ bool verilog_languaget::typecheck( - contextt &context, + symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler) { if(module=="") return false; - if(verilog_typecheck(parse_tree, context, module, message_handler)) + if(verilog_typecheck(parse_tree, symbol_table, module, message_handler)) return true; message_handler.print(9, "Synthesis"); - if(verilog_synthesis(context, module, message_handler, options)) + if(verilog_synthesis(symbol_table, module, message_handler, options)) return true; return false; @@ -186,7 +186,7 @@ Function: verilog_languaget::interfaces \*******************************************************************/ bool verilog_languaget::interfaces( - contextt &context, + symbol_tablet &symbol_table, message_handlert &message_handler) { return false; diff --git a/src/verilog/verilog_language.h b/src/verilog/verilog_language.h index e72c6d7..196d663 100644 --- a/src/verilog/verilog_language.h +++ b/src/verilog/verilog_language.h @@ -36,11 +36,11 @@ public: std::set &module_set); virtual bool interfaces( - contextt &context, + symbol_tablet &symbol_table, message_handlert &message_handler); virtual bool typecheck( - contextt &context, + symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler); diff --git a/src/verilog/verilog_module_instance.cpp b/src/verilog/verilog_module_instance.cpp index 7216e8d..3439ca2 100644 --- a/src/verilog/verilog_module_instance.cpp +++ b/src/verilog/verilog_module_instance.cpp @@ -131,10 +131,10 @@ void verilog_typecheckt::module_instance( // find base symbol - contextt::symbolst::const_iterator it= - context.symbols.find(module_identifier); + symbol_tablet::symbolst::const_iterator it= + symbol_table.symbols.find(module_identifier); - if(it==context.symbols.end()) + if(it==symbol_table.symbols.end()) { err_location(location); str << "module not found" << std::endl; @@ -175,8 +175,8 @@ void verilog_typecheckt::module_instance( module_identifier+=suffix; - if(context.symbols.find(module_identifier)!= - context.symbols.end()) + if(symbol_table.symbols.find(module_identifier)!= + symbol_table.symbols.end()) return; // done already // create symbol @@ -194,11 +194,11 @@ void verilog_typecheckt::module_instance( // throw away old stuff symbol.value.clear(); - // put symbol in context + // put symbol in symbol_table symbolt *new_symbol; - if(context.move(symbol, new_symbol)) + if(symbol_table.move(symbol, new_symbol)) { err_location(location); str << "duplicate definition of module " @@ -208,7 +208,7 @@ void verilog_typecheckt::module_instance( // recursive call - verilog_typecheckt verilog_typecheck(*new_symbol, context, get_message_handler()); + verilog_typecheckt verilog_typecheck(*new_symbol, symbol_table, get_message_handler()); if(verilog_typecheck.typecheck_main()) throw 0; diff --git a/src/verilog/verilog_context.h b/src/verilog/verilog_symbol_table.h similarity index 66% rename from src/verilog/verilog_context.h rename to src/verilog/verilog_symbol_table.h index 280921f..7324891 100644 --- a/src/verilog/verilog_context.h +++ b/src/verilog/verilog_symbol_table.h @@ -9,11 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_VERILOG_CONTEXT_H #define CPROVER_VERILOG_CONTEXT_H -#include +#include /*******************************************************************\ - Class: verilog_contextt + Class: verilog_symbol_tablet Inputs: @@ -23,16 +23,16 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -class verilog_contextt +class verilog_symbol_tablet { public: - verilog_contextt(contextt &_context):context(_context) + verilog_symbol_tablet(symbol_tablet &_symbol_table):symbol_table(_symbol_table) { } protected: - contextt &context; - symbolt &context_lookup(const irep_idt &identifier); + symbol_tablet &symbol_table; + symbolt &symbol_table_lookup(const irep_idt &identifier); }; #endif diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 0f4daf8..7dfa3a3 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -557,7 +557,7 @@ void verilog_synthesist::replace_by_wire( new_symbol.name=id2string(base.name)+"_"+i2string(c); new_symbol.base_name=id2string(base.base_name)+"_"+i2string(c); } - while(context.symbols.find(new_symbol.name)!=context.symbols.end()); + while(symbol_table.symbols.find(new_symbol.name)!=symbol_table.symbols.end()); new_symbol.type=what.type(); new_symbol.module=base.module; @@ -571,7 +571,7 @@ void verilog_synthesist::replace_by_wire( assignment.next.value=what; new_wires.insert(new_symbol.name); - if(context.move(new_symbol)) + if(symbol_table.move(new_symbol)) throw "failed to add replace_by_wire symbol"; what=symbol_expr; @@ -774,10 +774,10 @@ symbolt &verilog_synthesist::assignment_symbol(const exprt &lhs) const irep_idt &identifier=e->get(ID_identifier); - contextt::symbolst::iterator it= - context.symbols.find(identifier); + symbol_tablet::symbolst::iterator it= + symbol_table.symbols.find(identifier); - if(it==context.symbols.end()) + if(it==symbol_table.symbols.end()) { str << "assignment failed to find symbol `" << identifier @@ -981,12 +981,12 @@ void verilog_synthesist::synth_inst( { const irep_idt &identifier=statement.get(ID_module); - // must be in context + // must be in symbol_table const symbolt &symbol=lookup(identifier); // make sure it's synthesized already verilog_synthesis( - context, identifier, get_message_handler(), options); + symbol_table, identifier, get_message_handler(), options); forall_operands(it, statement) expand_inst(symbol, *it, trans); @@ -1191,7 +1191,7 @@ void verilog_synthesist::expand_inst( std::list new_symbols; - forall_symbol_module_map(it, context.symbol_module_map, symbol.module) + forall_symbol_module_map(it, symbol_table.symbol_module_map, symbol.module) { const symbolt &symbol=lookup(it->second); @@ -1219,7 +1219,7 @@ void verilog_synthesist::expand_inst( new_symbol.name=full_identifier; - if(context.add(new_symbol)) + if(symbol_table.add(new_symbol)) { str << "name collision during module instantiation: " << new_symbol.name << std::endl; @@ -1244,7 +1244,7 @@ void verilog_synthesist::expand_inst( it!=new_symbols.end(); it++) { - symbolt &symbol=context_lookup(*it); + symbolt &symbol=symbol_table_lookup(*it); replace_symbols(replace_map, symbol.value); } @@ -1652,7 +1652,7 @@ void verilog_synthesist::synth_assert( } const irep_idt &identifier=statement.get(ID_identifier); - symbolt &symbol=context_lookup(identifier); + symbolt &symbol=symbol_table_lookup(identifier); synth_expr(symbol.value, S_CURRENT); } @@ -1679,7 +1679,7 @@ void verilog_synthesist::synth_assert_module_item( } const irep_idt &identifier=module_item.get(ID_identifier); - symbolt &symbol=context_lookup(identifier); + symbolt &symbol=symbol_table_lookup(identifier); construct=C_OTHER; @@ -2098,9 +2098,9 @@ void verilog_synthesist::synth_event_guard( irep_idt identifier="conf::clock_enable_mode"; - // check context for clock guard + // check symbol_table for clock guard - if(context.symbols.find(identifier)!=context.symbols.end()) + if(symbol_table.symbols.find(identifier)!=symbol_table.symbols.end()) { // found! we make it a guard @@ -2616,7 +2616,7 @@ void verilog_synthesist::synth_assignments(transt &trans) it!=local_symbols.end(); it++) { - symbolt &symbol=context_lookup(*it); + symbolt &symbol=symbol_table_lookup(*it); if(symbol.is_state_var && !symbol.is_macro) { @@ -2656,7 +2656,7 @@ void verilog_synthesist::synth_assignments(transt &trans) it!=new_wires.end(); it++) { - symbolt &symbol=context_lookup(*it); + symbolt &symbol=symbol_table_lookup(*it); assignmentt &assignment=assignments[symbol.name]; synth_assignments(symbol, CURRENT, @@ -2853,7 +2853,7 @@ void verilog_synthesist::convert_module_items(symbolt &symbol) // find out about symbols of this module - forall_symbol_module_map(it, context.symbol_module_map, module) + forall_symbol_module_map(it, symbol_table.symbol_module_map, module) local_symbols.insert(it->second); // do the module items @@ -2912,7 +2912,7 @@ Function: verilog_synthesist::typecheck void verilog_synthesist::typecheck() { - symbolt &symbol=context_lookup(module); + symbolt &symbol=symbol_table_lookup(module); if(symbol.value.id()==ID_trans) return; // done already convert_module_items(symbol); } @@ -2930,12 +2930,12 @@ Function: verilog_synthesis \*******************************************************************/ bool verilog_synthesis( - contextt &context, + symbol_tablet &symbol_table, const irep_idt &module, message_handlert &message_handler, const optionst &options) { verilog_synthesist verilog_synthesis( - context, module, options, message_handler); + symbol_table, module, options, message_handler); return verilog_synthesis.typecheck_main(); } diff --git a/src/verilog/verilog_synthesis.h b/src/verilog/verilog_synthesis.h index 6f1a6f1..63b9642 100644 --- a/src/verilog/verilog_synthesis.h +++ b/src/verilog/verilog_synthesis.h @@ -21,10 +21,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "verilog_typecheck_base.h" -#include "verilog_context.h" +#include "verilog_symbol_table.h" bool verilog_synthesis( - contextt &context, + symbol_tablet &symbol_table, const irep_idt &module, message_handlert &message_handler, const optionst &options); @@ -43,17 +43,17 @@ bool verilog_synthesis( class verilog_synthesist: public verilog_typecheck_baset, - public verilog_contextt + public verilog_symbol_tablet { public: verilog_synthesist( - contextt &_context, + symbol_tablet &_symbol_table, const irep_idt &_module, const optionst &_options, message_handlert &_message_handler): verilog_typecheck_baset(ns, _message_handler), - verilog_contextt(_context), - ns(_context), + verilog_symbol_tablet(_symbol_table), + ns(_symbol_table), options(_options), value_map(NULL), module(_module), diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 6e60024..42fdebd 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -284,14 +284,14 @@ void verilog_typecheckt::convert_function_or_task(verilog_declt &decl) id2string(module_identifier)+"."+ id2string(decl.get_identifier()); - contextt::symbolst::iterator result= - context.symbols.find(identifier); + symbol_tablet::symbolst::iterator result= + symbol_table.symbols.find(identifier); - if(result==context.symbols.end()) + if(result==symbol_table.symbols.end()) { err_location(decl); str << "expected to find " << decl_class << " symbol `" - << identifier << "' in context"; + << identifier << "' in symbol_table"; throw 0; } @@ -369,7 +369,7 @@ void verilog_typecheckt::convert_decl(verilog_declt &decl) lhs.set(ID_identifier, identifier); - symbolt &symbol=context_lookup(identifier); + symbolt &symbol=symbol_table_lookup(identifier); convert_expr(rhs); propagate_type(rhs, symbol.type); lhs.type()=symbol.type; @@ -861,8 +861,8 @@ void verilog_typecheckt::convert_assert(exprt &statement) id2string(module_identifier)+ ".property."+id2string(base_name); - if(context.symbols.find(full_identifier)!= - context.symbols.end()) + if(symbol_table.symbols.find(full_identifier)!= + symbol_table.symbols.end()) { err_location(statement); str << "property identifier `" << base_name << "' already used"; @@ -884,7 +884,7 @@ void verilog_typecheckt::convert_assert(exprt &statement) symbol.location=statement.find_location(); symbolt *new_symbol; - context.move(symbol, new_symbol); + symbol_table.move(symbol, new_symbol); } /*******************************************************************\ @@ -1398,7 +1398,7 @@ bool verilog_typecheckt::implicit_wire( symbol.type=typet(ID_bool); // TODO: other types? symbolt *new_symbol; - context.move(symbol, new_symbol); + symbol_table.move(symbol, new_symbol); symbol_ptr=new_symbol; return false; @@ -1436,7 +1436,7 @@ Function: verilog_typecheck bool verilog_typecheck( const verilog_parse_treet &parse_tree, - contextt &context, + symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler) { @@ -1452,7 +1452,7 @@ bool verilog_typecheck( return true; } - return verilog_typecheck(context, it->second->verilog_module, message_handler); + return verilog_typecheck(symbol_table, it->second->verilog_module, message_handler); } /*******************************************************************\ @@ -1468,7 +1468,7 @@ Function: verilog_typecheck \*******************************************************************/ bool verilog_typecheck( - contextt &context, + symbol_tablet &symbol_table, const verilog_modulet &verilog_module, message_handlert &message_handler) { @@ -1487,11 +1487,11 @@ bool verilog_typecheck( symbol.type.add(ID_module_source)=verilog_module.to_irep(); - // put symbol in context + // put symbol in symbol_table symbolt *new_symbol; - if(context.move(symbol, new_symbol)) + if(symbol_table.move(symbol, new_symbol)) { message_streamt message_stream(message_handler); message_stream.str << "duplicate definition of module " @@ -1500,6 +1500,6 @@ bool verilog_typecheck( throw 0; } - verilog_typecheckt verilog_typecheck(*new_symbol, context, message_handler); + verilog_typecheckt verilog_typecheck(*new_symbol, symbol_table, message_handler); return verilog_typecheck.typecheck_main(); } diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h index bc3b912..fa05288 100644 --- a/src/verilog/verilog_typecheck.h +++ b/src/verilog/verilog_typecheck.h @@ -10,28 +10,28 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_VERILOG_TYPECHECK_H #include -#include +#include #include #include #include #include "verilog_typecheck_expr.h" #include "verilog_parse_tree.h" -#include "verilog_context.h" +#include "verilog_symbol_table.h" bool verilog_typecheck( const verilog_parse_treet &parse_tree, - contextt &context, + symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler); bool verilog_typecheck( - contextt &context, + symbol_tablet &symbol_table, const verilog_modulet &verilog_module, message_handlert &message_handler); bool verilog_typecheck( - contextt &context, + symbol_tablet &symbol_table, const std::string &module_identifier, const exprt::operandst ¶meters, message_handlert &message_handler); @@ -50,16 +50,16 @@ bool verilog_typecheck( class verilog_typecheckt: public verilog_typecheck_exprt, - public verilog_contextt + public verilog_symbol_tablet { public: verilog_typecheckt( symbolt &_module_symbol, - contextt &_context, + symbol_tablet &_symbol_table, message_handlert &_message_handler): verilog_typecheck_exprt(ns, _message_handler), - verilog_contextt(_context), - ns(_context), + verilog_symbol_tablet(_symbol_table), + ns(_symbol_table), module_symbol(_module_symbol), assertion_counter(0) {} diff --git a/src/verilog/verilog_typecheck_base.h b/src/verilog/verilog_typecheck_base.h index 2d56362..8dffea6 100644 --- a/src/verilog/verilog_typecheck_base.h +++ b/src/verilog/verilog_typecheck_base.h @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_VERILOG_TYPECHEK_BASE_H #define CPROVER_VERILOG_TYPECHEK_BASE_H -#include +#include #include #include #include diff --git a/src/vhdl/vhdl2expr.cpp b/src/vhdl/vhdl2expr.cpp index 305a3bc..32f4011 100644 --- a/src/vhdl/vhdl2expr.cpp +++ b/src/vhdl/vhdl2expr.cpp @@ -1,7 +1,7 @@ #include "vhdl2expr.h" bool vhdl2expr(const string &code, exprt &expr, - const contextt &context, + const symbol_tablet &symbol_table, const sequentt &sequent, string &msg) { diff --git a/src/vhdl/vhdl2expr.h b/src/vhdl/vhdl2expr.h index 601b1f8..2b677dc 100644 --- a/src/vhdl/vhdl2expr.h +++ b/src/vhdl/vhdl2expr.h @@ -1,7 +1,7 @@ #include "sequent.h" bool vhdl2expr(const string &code, exprt &expr, - const contextt &context, + const symbol_tablet &symbol_table, const sequentt &sequent, string &msg); diff --git a/src/vhdl/vhdl_language.cpp b/src/vhdl/vhdl_language.cpp index 0efcbfd..7a630d2 100644 --- a/src/vhdl/vhdl_language.cpp +++ b/src/vhdl/vhdl_language.cpp @@ -148,19 +148,19 @@ Function: vhdl_languaget::typecheck \*******************************************************************/ bool vhdl_languaget::typecheck( - contextt &context, + symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler) { if(module=="") return false; #if 0 - if(vhdl_typecheck(parse_tree, context, module, message_handler)) + if(vhdl_typecheck(parse_tree, symbol_table, module, message_handler)) return true; message_handler.print(9, "Synthesis"); - if(vhdl_synthesis(context, module, message_handler, options)) + if(vhdl_synthesis(symbol_table, module, message_handler, options)) return true; #endif @@ -180,7 +180,7 @@ Function: vhdl_languaget::interfaces \*******************************************************************/ bool vhdl_languaget::interfaces( - contextt &context, + symbol_tablet &symbol_table, message_handlert &message_handler) { return false; diff --git a/src/vhdl/vhdl_language.h b/src/vhdl/vhdl_language.h index 0fbeed5..96172d2 100644 --- a/src/vhdl/vhdl_language.h +++ b/src/vhdl/vhdl_language.h @@ -36,11 +36,11 @@ public: std::set &module_set); virtual bool interfaces( - contextt &context, + symbol_tablet &symbol_table, message_handlert &message_handler); virtual bool typecheck( - contextt &context, + symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler); diff --git a/src/vhdl/vhdl_typecheck.h b/src/vhdl/vhdl_typecheck.h index 34f5c90..e76a41f 100644 --- a/src/vhdl/vhdl_typecheck.h +++ b/src/vhdl/vhdl_typecheck.h @@ -9,9 +9,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_VHDL_TYPECHECK_H #define CPROVER_VHDL_TYPECHECK_H -#include "context.h" +#include "symbol_table.h" -bool convert_vhdl(void *root, contextt &context, std::string &error); +bool convert_vhdl(void *root, symbol_tablet &symbol_table, std::string &error); #endif