Skip to content

Commit 9b2e9fc

Browse files
peterschrammelpeterschrammel
committed
Generalize get_goto_model for symex-driven lazy loading
reduces code duplication
1 parent 7da990c commit 9b2e9fc

File tree

2 files changed

+62
-63
lines changed

2 files changed

+62
-63
lines changed

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 60 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -552,32 +552,27 @@ int jbmc_parse_optionst::doit()
552552
return 6;
553553
}
554554

555+
std::unique_ptr<abstract_goto_modelt> goto_model_ptr;
556+
int get_goto_program_ret = get_goto_program(goto_model_ptr, options);
557+
if(get_goto_program_ret != -1)
558+
return get_goto_program_ret;
559+
555560
if(!cmdline.isset("symex-driven-lazy-loading"))
556561
{
557-
std::unique_ptr<goto_modelt> goto_model_ptr;
558-
int get_goto_program_ret=get_goto_program(goto_model_ptr, options);
559-
if(get_goto_program_ret!=-1)
560-
return get_goto_program_ret;
561-
562-
goto_modelt &goto_model = *goto_model_ptr;
563-
564-
if(cmdline.isset("property"))
565-
::set_properties(goto_model, cmdline.get_values("property"));
566-
567562
if(
568563
options.get_bool_option("program-only") ||
569564
options.get_bool_option("show-vcc"))
570565
{
571566
if(options.get_bool_option("paths"))
572567
{
573568
all_properties_verifiert<java_single_path_symex_only_checkert> verifier(
574-
options, ui_message_handler, goto_model);
569+
options, ui_message_handler, *goto_model_ptr);
575570
(void)verifier();
576571
}
577572
else
578573
{
579574
all_properties_verifiert<java_multi_path_symex_only_checkert> verifier(
580-
options, ui_message_handler, goto_model);
575+
options, ui_message_handler, *goto_model_ptr);
581576
(void)verifier();
582577
}
583578

@@ -591,13 +586,13 @@ int jbmc_parse_optionst::doit()
591586
if(options.get_bool_option("paths"))
592587
{
593588
stop_on_fail_verifiert<java_single_path_symex_checkert> verifier(
594-
options, ui_message_handler, goto_model);
589+
options, ui_message_handler, *goto_model_ptr);
595590
(void)verifier();
596591
}
597592
else
598593
{
599594
stop_on_fail_verifiert<java_multi_path_symex_checkert> verifier(
600-
options, ui_message_handler, goto_model);
595+
options, ui_message_handler, *goto_model_ptr);
601596
(void)verifier();
602597
}
603598

@@ -612,7 +607,7 @@ int jbmc_parse_optionst::doit()
612607
{
613608
verifier = util_make_unique<
614609
stop_on_fail_verifiert<java_single_path_symex_checkert>>(
615-
options, ui_message_handler, goto_model);
610+
options, ui_message_handler, *goto_model_ptr);
616611
}
617612
else if(
618613
options.get_bool_option("stop-on-fail") &&
@@ -623,13 +618,13 @@ int jbmc_parse_optionst::doit()
623618
verifier =
624619
util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
625620
java_multi_path_symex_checkert>>(
626-
options, ui_message_handler, goto_model);
621+
options, ui_message_handler, *goto_model_ptr);
627622
}
628623
else
629624
{
630625
verifier = util_make_unique<
631626
stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
632-
options, ui_message_handler, goto_model);
627+
options, ui_message_handler, *goto_model_ptr);
633628
}
634629
}
635630
else if(
@@ -638,7 +633,7 @@ int jbmc_parse_optionst::doit()
638633
{
639634
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
640635
java_single_path_symex_checkert>>(
641-
options, ui_message_handler, goto_model);
636+
options, ui_message_handler, *goto_model_ptr);
642637
}
643638
else if(
644639
!options.get_bool_option("stop-on-fail") &&
@@ -649,13 +644,13 @@ int jbmc_parse_optionst::doit()
649644
verifier =
650645
util_make_unique<all_properties_verifier_with_fault_localizationt<
651646
java_multi_path_symex_checkert>>(
652-
options, ui_message_handler, goto_model);
647+
options, ui_message_handler, *goto_model_ptr);
653648
}
654649
else
655650
{
656651
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
657652
java_multi_path_symex_checkert>>(
658-
options, ui_message_handler, goto_model);
653+
options, ui_message_handler, *goto_model_ptr);
659654
}
660655
}
661656
else
@@ -665,7 +660,7 @@ int jbmc_parse_optionst::doit()
665660
// The `configure_bmc` callback passed will enable enum-unwind-static if
666661
// applicable.
667662
return bmct::do_language_agnostic_bmc(
668-
options, goto_model, ui_message_handler, configure_bmc);
663+
options, *goto_model_ptr, ui_message_handler, configure_bmc);
669664
}
670665

671666
const resultt result = (*verifier)();
@@ -674,31 +669,8 @@ int jbmc_parse_optionst::doit()
674669
}
675670
else
676671
{
677-
// Use symex-driven lazy loading:
678-
lazy_goto_modelt lazy_goto_model =
679-
lazy_goto_modelt::from_handler_object(*this, options, ui_message_handler);
680-
lazy_goto_model.initialize(cmdline.args, options);
681-
682-
class_hierarchy =
683-
util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
684-
685-
// The precise wording of this error matches goto-symex's complaint when no
686-
// __CPROVER_start exists (if we just go ahead and run it anyway it will
687-
// trip an invariant when it tries to load it)
688-
if(!lazy_goto_model.symbol_table.has_symbol(goto_functionst::entry_point()))
689-
{
690-
log.error() << "the program has no entry point";
691-
return 6;
692-
}
693-
694-
// Add failed symbols for any symbol created prior to loading any
695-
// particular function:
696-
add_failed_symbols(lazy_goto_model.symbol_table);
697-
698-
if(cmdline.isset("validate-goto-model"))
699-
{
700-
lazy_goto_model.validate();
701-
}
672+
lazy_goto_modelt &lazy_goto_model =
673+
dynamic_cast<lazy_goto_modelt &>(*goto_model_ptr);
702674

703675
// Provide show-goto-functions and similar dump functions after symex
704676
// executes. If --paths is active, these dump routines run after every
@@ -722,7 +694,7 @@ int jbmc_parse_optionst::doit()
722694
}
723695

724696
int jbmc_parse_optionst::get_goto_program(
725-
std::unique_ptr<goto_modelt> &goto_model,
697+
std::unique_ptr<abstract_goto_modelt> &goto_model_ptr,
726698
const optionst &options)
727699
{
728700
lazy_goto_modelt lazy_goto_model = lazy_goto_modelt::from_handler_object(
@@ -743,31 +715,57 @@ int jbmc_parse_optionst::get_goto_program(
743715
// particular function:
744716
add_failed_symbols(lazy_goto_model.symbol_table);
745717

718+
if(!cmdline.isset("symex-driven-lazy-loading"))
719+
{
746720
log.status() << "Generating GOTO Program" << messaget::eom;
747721
lazy_goto_model.load_all_functions();
748722

749-
// show symbol table or list symbols
750-
if(show_loaded_symbols(lazy_goto_model))
751-
return CPROVER_EXIT_SUCCESS;
723+
// show symbol table or list symbols
724+
if(show_loaded_symbols(lazy_goto_model))
725+
return CPROVER_EXIT_SUCCESS;
752726

753-
// Move the model out of the local lazy_goto_model
754-
// and into the caller's goto_model
755-
goto_model = lazy_goto_modelt::process_whole_model_and_freeze(
756-
std::move(lazy_goto_model));
757-
if(goto_model == nullptr)
758-
return 6;
727+
// Move the model out of the local lazy_goto_model
728+
// and into the caller's goto_model
729+
goto_model_ptr = lazy_goto_modelt::process_whole_model_and_freeze(
730+
std::move(lazy_goto_model));
731+
if(goto_model_ptr == nullptr)
732+
return 6;
759733

760-
if(cmdline.isset("validate-goto-model"))
761-
{
762-
goto_model->validate();
734+
goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
735+
736+
if(cmdline.isset("validate-goto-model"))
737+
{
738+
goto_model.validate();
739+
}
740+
741+
if(show_loaded_functions(goto_model))
742+
return CPROVER_EXIT_SUCCESS;
743+
744+
if(cmdline.isset("property"))
745+
::set_properties(goto_model, cmdline.get_values("property"));
763746
}
747+
else
748+
{
749+
// The precise wording of this error matches goto-symex's complaint when no
750+
// __CPROVER_start exists (if we just go ahead and run it anyway it will
751+
// trip an invariant when it tries to load it)
752+
if(!lazy_goto_model.symbol_table.has_symbol(goto_functionst::entry_point()))
753+
{
754+
error() << "the program has no entry point";
755+
return 6;
756+
}
764757

765-
if(show_loaded_functions(*goto_model))
766-
return CPROVER_EXIT_SUCCESS;
758+
if(cmdline.isset("validate-goto-model"))
759+
{
760+
lazy_goto_model.validate();
761+
}
767762

768-
log.status() << config.object_bits_info() << messaget::eom;
763+
goto_model_ptr =
764+
util_make_unique<lazy_goto_modelt>(std::move(lazy_goto_model));
769765
}
770766

767+
log.status() << config.object_bits_info() << messaget::eom;
768+
771769
return -1; // no error, continue
772770
}
773771

‎jbmc/src/jbmc/jbmc_parse_options.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,8 @@ class jbmc_parse_optionst : public parse_options_baset
125125

126126
void get_command_line_options(optionst &);
127127
int get_goto_program(
128-
std::unique_ptr<goto_modelt> &goto_model, const optionst &);
128+
std::unique_ptr<abstract_goto_modelt> &goto_model,
129+
const optionst &);
129130
bool show_loaded_functions(const abstract_goto_modelt &goto_model);
130131
bool show_loaded_symbols(const abstract_goto_modelt &goto_model);
131132
};

0 commit comments

Comments
 (0)