Skip to content

Commit c74d257

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #3968 from peterschrammel/cover-verifier
Add cover goals verifier [blocks: 3969]
2 parents 178802d + 969f5d6 commit c74d257

16 files changed

+523
-6
lines changed

‎jbmc/unit/Makefile

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -85,9 +85,7 @@ java-testing-utils-clean:
8585
BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
8686
$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
8787
$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
88-
$(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
8988
$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
90-
$(CPROVER_DIR)/src/cbmc/xml_interface$(OBJEXT) \
9189
$(CPROVER_DIR)/src/jsil/expr2jsil$(OBJEXT) \
9290
$(CPROVER_DIR)/src/jsil/jsil_convert$(OBJEXT) \
9391
$(CPROVER_DIR)/src/jsil/jsil_entry_point$(OBJEXT) \

‎regression/cbmc-cover/assertion1/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--cover assertion
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 9 function main: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 13 function main: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 9 function main assertion: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 13 function main assertion: SATISFIED$
88
--
99
^warning: ignoring

‎src/cbmc/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
SRC = all_properties.cpp \
22
bmc.cpp \
33
bmc_cover.cpp \
4+
c_test_input_generator.cpp \
45
cbmc_languages.cpp \
56
cbmc_main.cpp \
67
cbmc_parse_options.cpp \

‎src/cbmc/c_test_input_generator.cpp

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
/*******************************************************************\
2+
3+
Module: Test Input Generator for C
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Test Input Generator for C
11+
12+
#include "c_test_input_generator.h"
13+
14+
#include <goto-checker/goto_trace_storage.h>
15+
16+
#include <langapi/language_util.h>
17+
18+
#include <util/json.h>
19+
#include <util/json_irep.h>
20+
#include <util/options.h>
21+
#include <util/string_utils.h>
22+
#include <util/xml.h>
23+
#include <util/xml_irep.h>
24+
25+
#include <goto-programs/json_expr.h>
26+
#include <goto-programs/json_goto_trace.h>
27+
#include <goto-programs/xml_expr.h>
28+
#include <goto-programs/xml_goto_trace.h>
29+
30+
c_test_input_generatort::c_test_input_generatort(
31+
ui_message_handlert &ui_message_handler,
32+
const optionst &options)
33+
: ui_message_handler(ui_message_handler), options(options)
34+
{
35+
}
36+
37+
void test_inputst::output_plain_text(
38+
std::ostream &out,
39+
const namespacet &ns,
40+
const goto_tracet &goto_trace) const
41+
{
42+
const auto input_assignments =
43+
make_range(goto_trace.steps)
44+
.filter([](const goto_trace_stept &step) { return step.is_input(); })
45+
.map([ns](const goto_trace_stept &step) {
46+
return id2string(step.io_id) + '=' +
47+
from_expr(ns, step.function_id, step.io_args.front());
48+
});
49+
join_strings(out, input_assignments.begin(), input_assignments.end(), ", ");
50+
out << '\n';
51+
}
52+
53+
json_objectt test_inputst::to_json(
54+
const namespacet &ns,
55+
const goto_tracet &goto_trace,
56+
bool print_trace) const
57+
{
58+
json_objectt json_result;
59+
json_arrayt &json_inputs = json_result["inputs"].make_array();
60+
61+
for(const auto &step : goto_trace.steps)
62+
{
63+
if(step.is_input())
64+
{
65+
json_objectt json_input({{"id", json_stringt(step.io_id)}});
66+
if(step.io_args.size() == 1)
67+
json_input["value"] =
68+
json(step.io_args.front(), ns, ns.lookup(step.function_id).mode);
69+
json_inputs.push_back(std::move(json_input));
70+
}
71+
}
72+
73+
json_arrayt goal_refs;
74+
for(const auto &goal_id : goto_trace.get_all_property_ids())
75+
{
76+
goal_refs.push_back(json_stringt(goal_id));
77+
}
78+
json_result["coveredGoals"] = std::move(goal_refs);
79+
return json_result;
80+
}
81+
82+
xmlt test_inputst::to_xml(
83+
const namespacet &ns,
84+
const goto_tracet &goto_trace,
85+
bool print_trace) const
86+
{
87+
xmlt xml_result("test");
88+
if(print_trace)
89+
{
90+
convert(ns, goto_trace, xml_result.new_element());
91+
}
92+
else
93+
{
94+
xmlt &xml_test = xml_result.new_element("inputs");
95+
96+
for(const auto &step : goto_trace.steps)
97+
{
98+
if(step.is_input())
99+
{
100+
xmlt &xml_input = xml_test.new_element("input");
101+
xml_input.set_attribute("id", id2string(step.io_id));
102+
if(step.io_args.size() == 1)
103+
xml_input.new_element("value") = xml(step.io_args.front(), ns);
104+
}
105+
}
106+
}
107+
108+
for(const auto &goal_id : goto_trace.get_all_property_ids())
109+
{
110+
xmlt &xml_goal = xml_result.new_element("goal");
111+
xml_goal.set_attribute("id", id2string(goal_id));
112+
}
113+
114+
return xml_result;
115+
}
116+
117+
test_inputst c_test_input_generatort::
118+
operator()(const goto_tracet &goto_trace, const namespacet &ns)
119+
{
120+
test_inputst test_inputs;
121+
return test_inputs;
122+
}
123+
124+
void c_test_input_generatort::operator()(const goto_trace_storaget &traces)
125+
{
126+
const namespacet &ns = traces.get_namespace();
127+
const bool print_trace = options.get_bool_option("trace");
128+
messaget log(ui_message_handler);
129+
switch(ui_message_handler.get_ui())
130+
{
131+
case ui_message_handlert::uit::PLAIN:
132+
log.result() << "\nTest suite:\n";
133+
for(const auto trace : traces.all())
134+
{
135+
test_inputst test_inputs = (*this)(trace, ns);
136+
test_inputs.output_plain_text(log.result(), ns, trace);
137+
}
138+
log.result() << messaget::eom;
139+
break;
140+
case ui_message_handlert::uit::JSON_UI:
141+
{
142+
if(log.status().tellp() > 0)
143+
log.status() << messaget::eom; // force end of previous message
144+
json_stream_objectt &json_result =
145+
ui_message_handler.get_json_stream().push_back_stream_object();
146+
json_stream_arrayt &tests_array =
147+
json_result.push_back_stream_array("tests");
148+
149+
for(const auto trace : traces.all())
150+
{
151+
test_inputst test_inputs = (*this)(trace, ns);
152+
tests_array.push_back(test_inputs.to_json(ns, trace, print_trace));
153+
}
154+
break;
155+
}
156+
case ui_message_handlert::uit::XML_UI:
157+
for(const auto trace : traces.all())
158+
{
159+
test_inputst test_inputs = (*this)(trace, ns);
160+
log.result() << test_inputs.to_xml(ns, trace, print_trace);
161+
}
162+
break;
163+
}
164+
}

‎src/cbmc/c_test_input_generator.h

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
/*******************************************************************\
2+
3+
Module: Test Input Generator for C
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Test Input Generator for C
11+
12+
#ifndef CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H
13+
#define CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H
14+
15+
#include <iosfwd>
16+
17+
#include <util/ui_message.h>
18+
19+
class goto_tracet;
20+
class goto_trace_storaget;
21+
class json_objectt;
22+
class namespacet;
23+
class optionst;
24+
25+
class test_inputst
26+
{
27+
public:
28+
/// Outputs the test inputs in plain text format
29+
void output_plain_text(
30+
std::ostream &out,
31+
const namespacet &ns,
32+
const goto_tracet &goto_trace) const;
33+
34+
/// Returns the test inputs in JSON format
35+
/// including the trace if desired
36+
json_objectt to_json(
37+
const namespacet &ns,
38+
const goto_tracet &goto_trace,
39+
bool print_trace) const;
40+
41+
/// Returns the test inputs in XML format
42+
/// including the trace if desired
43+
xmlt to_xml(
44+
const namespacet &ns,
45+
const goto_tracet &goto_trace,
46+
bool print_trace) const;
47+
};
48+
49+
class c_test_input_generatort
50+
{
51+
public:
52+
c_test_input_generatort(
53+
ui_message_handlert &ui_message_handler,
54+
const optionst &options);
55+
56+
/// Extracts test inputs for all traces and outputs them
57+
void operator()(const goto_trace_storaget &);
58+
59+
protected:
60+
ui_message_handlert &ui_message_handler;
61+
const optionst &options;
62+
63+
/// Extracts test inputs from the given \p goto_trace
64+
test_inputst operator()(const goto_tracet &goto_trace, const namespacet &ns);
65+
};
66+
67+
#endif // CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com
3636
#include <goto-checker/all_properties_verifier.h>
3737
#include <goto-checker/all_properties_verifier_with_trace_storage.h>
3838
#include <goto-checker/bmc_util.h>
39+
#include <goto-checker/cover_goals_verifier_with_trace_storage.h>
3940
#include <goto-checker/multi_path_symex_checker.h>
4041
#include <goto-checker/multi_path_symex_only_checker.h>
4142
#include <goto-checker/properties.h>
@@ -73,6 +74,7 @@ Author: Daniel Kroening, kroening@kroening.com
7374

7475
#include <langapi/mode.h>
7576

77+
#include "c_test_input_generator.h"
7678
#include "xml_interface.h"
7779

7880
cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
@@ -578,6 +580,19 @@ int cbmc_parse_optionst::doit()
578580
}
579581
}
580582

583+
if(options.is_set("cover"))
584+
{
585+
cover_goals_verifier_with_trace_storaget<multi_path_symex_checkert>
586+
verifier(options, ui_message_handler, goto_model);
587+
(void)verifier();
588+
verifier.report();
589+
590+
c_test_input_generatort test_generator(ui_message_handler, options);
591+
test_generator(verifier.get_traces());
592+
593+
return CPROVER_EXIT_SUCCESS;
594+
}
595+
581596
std::unique_ptr<goto_verifiert> verifier = nullptr;
582597

583598
if(
@@ -607,6 +622,7 @@ int cbmc_parse_optionst::doit()
607622

608623
resultt result = (*verifier)();
609624
verifier->report();
625+
610626
return result_to_exit_code(result);
611627
}
612628

‎src/goto-checker/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
SRC = bmc_util.cpp \
22
counterexample_beautification.cpp \
3+
cover_goals_report_util.cpp \
34
incremental_goto_checker.cpp \
45
goto_trace_storage.cpp \
56
goto_verifier.cpp \

‎src/goto-checker/README.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,12 @@ There are the following variants of goto verifiers at the moment:
6262
\ref all_properties_verifier_with_trace_storaget,
6363
\ref all_properties_verifiert does not require to store any traces.
6464
A trace ends at a violated property.
65+
* \ref cover_goals_verifier_with_trace_storaget : Determines the status of
66+
all properties, but full traces with potentially several failing properties
67+
(e.g. coverage goals) are stored and results reported after the
68+
verification algorithm has terminated.
69+
The reporting uses 'goals' rather than 'property' terminology. I.e.
70+
a failing property means 'success' and a passing property 'failed'.
6571

6672
There are the following variants of incremental goto checkers at the moment:
6773
* \ref multi_path_symex_checkert : The default mode of goto-symex. It explores

0 commit comments

Comments
 (0)