Skip to content

Commit 4315c29

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #3969 from peterschrammel/single-path-symex-checker
Single-path symex checker [blocks: #3976]
2 parents 39174a6 + 1f9f475 commit 4315c29

18 files changed

+1097
-257
lines changed

‎jbmc/src/java_bytecode/java_single_path_symex_checker.h

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
/*******************************************************************\
2+
3+
Module: Goto Checker using Single Path Symbolic Execution for Java
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Goto Checker using Single Path Symbolic Execution for Java
11+
12+
#ifndef CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_CHECKER_H
13+
#define CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_CHECKER_H
14+
15+
#include <goto-checker/single_path_symex_checker.h>
16+
17+
#include "java_bmc_util.h"
18+
19+
class java_single_path_symex_checkert : public single_path_symex_checkert
20+
{
21+
public:
22+
java_single_path_symex_checkert(
23+
const optionst &options,
24+
ui_message_handlert &ui_message_handler,
25+
abstract_goto_modelt &goto_model)
26+
: single_path_symex_checkert(options, ui_message_handler, goto_model)
27+
{
28+
}
29+
30+
void setup_symex(symex_bmct &symex) override
31+
{
32+
single_path_symex_checkert::setup_symex(symex);
33+
java_setup_symex(options, goto_model, symex);
34+
}
35+
};
36+
37+
#endif // CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_CHECKER_H

‎jbmc/src/java_bytecode/java_single_path_symex_only_checker.h

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
/*******************************************************************\
2+
3+
Module: Goto Checker using Single Path Symbolic Execution for Java
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Goto Checker using Single Path Symbolic Execution for Java
11+
12+
#ifndef CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
13+
#define CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
14+
15+
#include <goto-checker/single_path_symex_only_checker.h>
16+
17+
#include "java_bmc_util.h"
18+
19+
class java_single_path_symex_only_checkert
20+
: public single_path_symex_only_checkert
21+
{
22+
public:
23+
java_single_path_symex_only_checkert(
24+
const optionst &options,
25+
ui_message_handlert &ui_message_handler,
26+
abstract_goto_modelt &goto_model)
27+
: single_path_symex_only_checkert(options, ui_message_handler, goto_model)
28+
{
29+
}
30+
31+
void setup_symex(symex_bmct &symex) override
32+
{
33+
single_path_symex_only_checkert::setup_symex(symex);
34+
java_setup_symex(options, goto_model, symex);
35+
}
36+
};
37+
38+
#endif // CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 48 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,8 @@ Author: Daniel Kroening, [email protected]
6666
#include <java_bytecode/java_enum_static_init_unwind_handler.h>
6767
#include <java_bytecode/java_multi_path_symex_checker.h>
6868
#include <java_bytecode/java_multi_path_symex_only_checker.h>
69+
#include <java_bytecode/java_single_path_symex_checker.h>
70+
#include <java_bytecode/java_single_path_symex_only_checker.h>
6971
#include <java_bytecode/remove_exceptions.h>
7072
#include <java_bytecode/remove_instanceof.h>
7173
#include <java_bytecode/remove_java_new.h>
@@ -559,46 +561,79 @@ int jbmc_parse_optionst::doit()
559561
options.get_bool_option("program-only") ||
560562
options.get_bool_option("show-vcc"))
561563
{
562-
if(!options.get_bool_option("paths"))
564+
if(options.get_bool_option("paths"))
565+
{
566+
all_properties_verifiert<java_single_path_symex_only_checkert> verifier(
567+
options, ui_message_handler, goto_model);
568+
(void)verifier();
569+
}
570+
else
563571
{
564572
all_properties_verifiert<java_multi_path_symex_only_checkert> verifier(
565573
options, ui_message_handler, goto_model);
566574
(void)verifier();
567-
return CPROVER_EXIT_SUCCESS;
568575
}
576+
577+
return CPROVER_EXIT_SUCCESS;
569578
}
570579

571580
if(
572581
options.get_bool_option("dimacs") ||
573582
!options.get_option("outfile").empty())
574583
{
575-
if(!options.get_bool_option("paths"))
584+
if(options.get_bool_option("paths"))
585+
{
586+
stop_on_fail_verifiert<java_single_path_symex_checkert> verifier(
587+
options, ui_message_handler, goto_model);
588+
(void)verifier();
589+
}
590+
else
576591
{
577-
stop_on_fail_verifiert<multi_path_symex_checkert> verifier(
592+
stop_on_fail_verifiert<java_multi_path_symex_checkert> verifier(
578593
options, ui_message_handler, goto_model);
579594
(void)verifier();
580-
return CPROVER_EXIT_SUCCESS;
581595
}
596+
597+
return CPROVER_EXIT_SUCCESS;
582598
}
583599

584600
std::unique_ptr<goto_verifiert> verifier = nullptr;
585601

586602
if(
587-
!options.get_bool_option("paths") && !options.is_set("cover") &&
588-
!options.get_bool_option("dimacs") &&
603+
!options.is_set("cover") && !options.get_bool_option("dimacs") &&
589604
options.get_option("outfile").empty())
590605
{
591606
if(options.get_bool_option("stop-on-fail"))
592607
{
593-
verifier = util_make_unique<
594-
stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
595-
options, ui_message_handler, goto_model);
608+
if(options.get_bool_option("paths"))
609+
{
610+
verifier = util_make_unique<
611+
stop_on_fail_verifiert<java_single_path_symex_checkert>>(
612+
options, ui_message_handler, goto_model);
613+
}
614+
else
615+
{
616+
verifier = util_make_unique<
617+
stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
618+
options, ui_message_handler, goto_model);
619+
}
596620
}
597621
else
598622
{
599-
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
600-
java_multi_path_symex_checkert>>(
601-
options, ui_message_handler, goto_model);
623+
if(options.get_bool_option("paths"))
624+
{
625+
verifier =
626+
util_make_unique<all_properties_verifier_with_trace_storaget<
627+
java_single_path_symex_checkert>>(
628+
options, ui_message_handler, goto_model);
629+
}
630+
else
631+
{
632+
verifier =
633+
util_make_unique<all_properties_verifier_with_trace_storaget<
634+
java_multi_path_symex_checkert>>(
635+
options, ui_message_handler, goto_model);
636+
}
602637
}
603638
}
604639

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 44 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,8 @@ Author: Daniel Kroening, [email protected]
4040
#include <goto-checker/multi_path_symex_checker.h>
4141
#include <goto-checker/multi_path_symex_only_checker.h>
4242
#include <goto-checker/properties.h>
43+
#include <goto-checker/single_path_symex_checker.h>
44+
#include <goto-checker/single_path_symex_only_checker.h>
4345
#include <goto-checker/stop_on_fail_verifier.h>
4446

4547
#include <goto-programs/adjust_float_expressions.h>
@@ -559,25 +561,39 @@ int cbmc_parse_optionst::doit()
559561
options.get_bool_option("program-only") ||
560562
options.get_bool_option("show-vcc"))
561563
{
562-
if(!options.get_bool_option("paths"))
564+
if(options.get_bool_option("paths"))
565+
{
566+
all_properties_verifiert<single_path_symex_only_checkert> verifier(
567+
options, ui_message_handler, goto_model);
568+
(void)verifier();
569+
}
570+
else
563571
{
564572
all_properties_verifiert<multi_path_symex_only_checkert> verifier(
565573
options, ui_message_handler, goto_model);
566574
(void)verifier();
567-
return CPROVER_EXIT_SUCCESS;
568575
}
576+
577+
return CPROVER_EXIT_SUCCESS;
569578
}
570579

571580
if(
572581
options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
573582
{
574-
if(!options.get_bool_option("paths"))
583+
if(options.get_bool_option("paths"))
584+
{
585+
stop_on_fail_verifiert<single_path_symex_checkert> verifier(
586+
options, ui_message_handler, goto_model);
587+
(void)verifier();
588+
}
589+
else
575590
{
576591
stop_on_fail_verifiert<multi_path_symex_checkert> verifier(
577592
options, ui_message_handler, goto_model);
578593
(void)verifier();
579-
return CPROVER_EXIT_SUCCESS;
580594
}
595+
596+
return CPROVER_EXIT_SUCCESS;
581597
}
582598

583599
if(options.is_set("cover"))
@@ -596,20 +612,36 @@ int cbmc_parse_optionst::doit()
596612
std::unique_ptr<goto_verifiert> verifier = nullptr;
597613

598614
if(
599-
!options.get_bool_option("paths") && !options.is_set("cover") &&
600-
!options.get_bool_option("dimacs") && options.get_option("outfile").empty())
615+
!options.is_set("cover") && !options.get_bool_option("dimacs") &&
616+
options.get_option("outfile").empty())
601617
{
602618
if(options.get_bool_option("stop-on-fail"))
603619
{
604-
verifier =
605-
util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
606-
options, ui_message_handler, goto_model);
620+
if(options.get_bool_option("paths"))
621+
{
622+
verifier =
623+
util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
624+
options, ui_message_handler, goto_model);
625+
}
626+
else
627+
{
628+
verifier =
629+
util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
630+
options, ui_message_handler, goto_model);
631+
}
607632
}
608633
else
609634
{
610-
verifier = util_make_unique<
611-
all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>>(
612-
options, ui_message_handler, goto_model);
635+
if(options.get_bool_option("paths"))
636+
{
637+
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
638+
single_path_symex_checkert>>(options, ui_message_handler, goto_model);
639+
}
640+
else
641+
{
642+
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
643+
multi_path_symex_checkert>>(options, ui_message_handler, goto_model);
644+
}
613645
}
614646
}
615647

‎src/goto-checker/Makefile

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,15 @@ SRC = bmc_util.cpp \
22
counterexample_beautification.cpp \
33
cover_goals_report_util.cpp \
44
incremental_goto_checker.cpp \
5+
goto_symex_property_decider.cpp \
56
goto_trace_storage.cpp \
67
goto_verifier.cpp \
78
multi_path_symex_checker.cpp \
89
multi_path_symex_only_checker.cpp \
910
properties.cpp \
1011
report_util.cpp \
12+
single_path_symex_checker.cpp \
13+
single_path_symex_only_checker.cpp \
1114
solver_factory.cpp \
1215
symex_coverage.cpp \
1316
symex_bmc.cpp \

‎src/goto-checker/bmc_util.cpp

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -269,3 +269,104 @@ void update_status_of_not_checked_properties(
269269
}
270270
}
271271
}
272+
273+
void update_status_of_unknown_properties(
274+
propertiest &properties,
275+
std::unordered_set<irep_idt> &updated_properties)
276+
{
277+
for(auto &property_pair : properties)
278+
{
279+
if(property_pair.second.status == property_statust::UNKNOWN)
280+
{
281+
// This could have any status except NOT_CHECKED.
282+
// We consider them PASS because we do verification modulo bounds.
283+
property_pair.second.status = property_statust::PASS;
284+
updated_properties.insert(property_pair.first);
285+
}
286+
}
287+
}
288+
289+
void output_coverage_report(
290+
const std::string &cov_out,
291+
const abstract_goto_modelt &goto_model,
292+
const symex_bmct &symex,
293+
ui_message_handlert &ui_message_handler)
294+
{
295+
if(
296+
!cov_out.empty() &&
297+
symex.output_coverage_report(goto_model.get_goto_functions(), cov_out))
298+
{
299+
messaget log(ui_message_handler);
300+
log.error() << "Failed to write symex coverage report to '" << cov_out
301+
<< "'" << messaget::eom;
302+
}
303+
}
304+
305+
static void postprocess_equation(
306+
symex_bmct &symex,
307+
symex_target_equationt &equation,
308+
const optionst &options,
309+
const namespacet &ns,
310+
ui_message_handlert &ui_message_handler)
311+
{
312+
// add a partial ordering, if required
313+
if(equation.has_threads())
314+
{
315+
std::unique_ptr<memory_model_baset> memory_model =
316+
get_memory_model(options, ns);
317+
memory_model->set_message_handler(ui_message_handler);
318+
(*memory_model)(equation);
319+
}
320+
321+
messaget log(ui_message_handler);
322+
log.statistics() << "size of program expression: "
323+
<< equation.SSA_steps.size() << " steps" << messaget::eom;
324+
325+
slice(symex, equation, ns, options, ui_message_handler);
326+
327+
if(options.get_bool_option("validate-ssa-equation"))
328+
{
329+
symex.validate(validation_modet::INVARIANT);
330+
}
331+
}
332+
333+
void perform_symex(
334+
abstract_goto_modelt &goto_model,
335+
symex_bmct &symex,
336+
symbol_tablet &symex_symbol_table,
337+
symex_target_equationt &equation,
338+
const optionst &options,
339+
const namespacet &ns,
340+
ui_message_handlert &ui_message_handler)
341+
{
342+
auto get_goto_function =
343+
[&goto_model](
344+
const irep_idt &id) -> const goto_functionst::goto_functiont & {
345+
return goto_model.get_goto_function(id);
346+
};
347+
348+
symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
349+
350+
postprocess_equation(symex, equation, options, ns, ui_message_handler);
351+
}
352+
353+
void perform_symex(
354+
abstract_goto_modelt &goto_model,
355+
symex_bmct &symex,
356+
path_storaget::patht &resume,
357+
symbol_tablet &symex_symbol_table,
358+
const optionst &options,
359+
const namespacet &ns,
360+
ui_message_handlert &ui_message_handler)
361+
{
362+
auto get_goto_function =
363+
[&goto_model](
364+
const irep_idt &id) -> const goto_functionst::goto_functiont & {
365+
return goto_model.get_goto_function(id);
366+
};
367+
368+
symex.resume_symex_from_saved_state(
369+
get_goto_function, resume.state, &resume.equation, symex_symbol_table);
370+
371+
postprocess_equation(symex, resume.equation, options, ns, ui_message_handler);
372+
}

0 commit comments

Comments
 (0)