big change: cbmc now uses --all-properties as the default
This commit is contained in:
parent
b4f3819447
commit
95f4a47a27
|
@ -59,10 +59,10 @@ domains</a>. More detail on automatically generated properties is provided
|
|||
<a href="properties.shtml">here</a>.</p>
|
||||
|
||||
<p class="justified">
|
||||
Note that automatically generated properties need not necessarily correspond
|
||||
to bugs – these are just <i>potential</i> flaws, as abstract
|
||||
interpretation might be imprecise. Whether one of these properties
|
||||
holds or corresponds to a bug needs to be determined by further analysis.
|
||||
Note that these automatically generated properties need not necessarily
|
||||
correspond to bugs – these are just <i>potential</i> flaws, as
|
||||
abstract interpretation might be imprecise. Whether these properties
|
||||
hold or correspond to actual bugs needs to be determined by further analysis.
|
||||
</p>
|
||||
|
||||
<p class="justified">
|
||||
|
@ -87,17 +87,40 @@ holds. Let's run the decision procedure:</p>
|
|||
</code>
|
||||
|
||||
<p class="justified">
|
||||
CBMC transforms the equation you have seen before into CNF and passes it
|
||||
to a SAT solver (more background on this step is in the book
|
||||
on <a href="http://www.decision-procedures.org/">Decision Procedures</a>).
|
||||
CBMC can now detect that the equation is actually not valid,
|
||||
and thus, there is a bug in the program. It prints a counterexample trace,
|
||||
i.e., a program trace that ends in a state which violates the property. In
|
||||
our example, the program trace ends in the faulty array access. It also
|
||||
shows the values the input variables must have for the bug to occur. In this
|
||||
example, <code>argc</code> must be one to trigger the out-of-bounds array access.
|
||||
If you add a branch to the example that requires that <code>argc>=3</code>,
|
||||
the bug is fixed and CBMC will report a successful verification run.</p>
|
||||
CBMC transforms the equation you have seen before into CNF and passes it to
|
||||
a SAT solver (more background on this step is in the book on <a
|
||||
href="http://www.decision-procedures.org/">Decision Procedures</a>). It
|
||||
then determines which of the properties that it has generated for the
|
||||
program hold and which do not. Using the SAT solver, CBMC detects that the
|
||||
property for the object bounds of <code>argv</code> does not hold, and will
|
||||
thus print a line as follows:
|
||||
</p>
|
||||
|
||||
<code>
|
||||
[main.pointer_dereference.6] dereference failure: object bounds in argv[(signed long int)2]: FAILED
|
||||
</code>
|
||||
|
||||
<h3>Counterexample Traces</h3>
|
||||
|
||||
<p class="justified">
|
||||
Let us have a closer look at this property and why it fails. To aid the
|
||||
understanding of the problem, CBMC can generate a <i>counterexample
|
||||
trace</i> for failed properties. To obtain this trace, run
|
||||
</P
|
||||
|
||||
<code>
|
||||
cbmc file1.c --bounds-check --pointer-check --property main.pointer_dereference.6
|
||||
</code>
|
||||
|
||||
<p class="justified">
|
||||
CBMC then prints a counterexample trace, i.e., a program trace that begins
|
||||
with <code>main</code> and ends in a state which violates the property. In
|
||||
our example, the program trace ends in the faulty array access. It also
|
||||
shows the values the input variables must have for the bug to occur. In
|
||||
this example, <code>argc</code> must be one to trigger the out-of-bounds
|
||||
array access. If you add a branch to the example that requires that
|
||||
<code>argc>=3</code>, the bug is fixed and CBMC will report that all
|
||||
properties are OK.</p>
|
||||
|
||||
<h3>Verifying Modules</h3>
|
||||
|
||||
|
@ -129,14 +152,21 @@ In order to set the entry point to the <code>sum</code> function, run
|
|||
cbmc file2.c --function sum --bounds-check
|
||||
</code>
|
||||
|
||||
<p class="justified">
|
||||
It is often necessary to build a suitable <i>harness</i> for the function
|
||||
in order to set up the environment appropriately.
|
||||
</p>
|
||||
|
||||
<h3>Loop Unwinding</h3>
|
||||
|
||||
<p class="justified">
|
||||
You will note that CBMC unwinds the <code>for</code> loop in the program.
|
||||
As CBMC performs Bounded Model Checking, all loops have to have a finite
|
||||
upper run-time bound in order to guarantee that all bugs are found. CBMC
|
||||
can optionally check that enough unwinding is performed. As an example, consider
|
||||
the program <a href="binsearch.c">binsearch.c</a>:</p>
|
||||
When running the previous example, you will have noted that CBMC unwinds the
|
||||
<code>for</code> loop in the program. As CBMC performs Bounded Model
|
||||
Checking, all loops have to have a finite upper run-time bound in order to
|
||||
guarantee that all bugs are found. CBMC can optionally check that enough
|
||||
unwinding is performed. As an example, consider the program <a
|
||||
href="binsearch.c">binsearch.c</a>:
|
||||
</p>
|
||||
|
||||
<hr>
|
||||
<code>
|
||||
|
@ -171,10 +201,13 @@ command line argument:</p>
|
|||
<p class="justified">
|
||||
CBMC verifies that verifies the array accesses are within the bounds; note
|
||||
that this actually depends on the result of the right shift. In addition,
|
||||
as CBMC is given the option <code>--unwinding-assertions</code>, it also
|
||||
checks that enough unwinding is done, i.e., it proves a run-time bound. For
|
||||
any lower unwinding bound, there are traces that require more loop
|
||||
iterations. Thus, CBMC will produce an appropriate counterexample.
|
||||
as CBMC is given the option
|
||||
<nobr><code>--unwinding-assertions</code></nobr>, it also checks that enough
|
||||
unwinding is done, i.e., it proves a run-time bound. For any lower
|
||||
unwinding bound, there are traces that require more loop iterations. Thus,
|
||||
CBMC will report that the unwinding assertion has failed. As usual, a counterexample
|
||||
trace that documents this can be obtained with the option
|
||||
<code>--property</code>.
|
||||
</p>
|
||||
|
||||
<h3>Unbounded Loops</h3>
|
||||
|
@ -244,7 +277,7 @@ the number of program steps to be processed.</li>
|
|||
Given the option <code>--unwinding-assertions</code>, CBMC checks whether
|
||||
the arugment to <code>--unwind</code> is large enough to cover all program
|
||||
paths. If the argument is too small, CBMC will detect that not enough
|
||||
unwinding is done and aborts with an unwinding assertion violation.
|
||||
unwinding is done reports that an unwinding assertion has failed.
|
||||
</p>
|
||||
|
||||
<p class="justified">
|
||||
|
|
|
@ -3,7 +3,6 @@ main.c
|
|||
--pointer-check
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^Counterexample:$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -3,7 +3,6 @@ main.c
|
|||
--pointer-check
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^Counterexample:$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -2,7 +2,6 @@ CORE
|
|||
main.c
|
||||
--pointer-check
|
||||
^SIGNAL=0$
|
||||
^Counterexample:$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -2,7 +2,6 @@ CORE
|
|||
main.c
|
||||
--pointer-check
|
||||
^SIGNAL=0$
|
||||
^Counterexample:$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -3,8 +3,6 @@ main.c
|
|||
--pointer-check --bounds-check
|
||||
^SIGNAL=0$
|
||||
^EXIT=10$
|
||||
^Counterexample:$
|
||||
^ dereference failure: object bounds in .*$
|
||||
^VERIFICATION FAILED$
|
||||
^\[.*\] dereference failure: object bounds in \*p: FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -2,7 +2,7 @@ CORE
|
|||
main.c
|
||||
--signed-overflow-check
|
||||
^SIGNAL=0$
|
||||
^Counterexample:$
|
||||
^\[.*\] arithmetic overflow on signed + in .*: FAILED$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -2,7 +2,6 @@ CORE
|
|||
main.c
|
||||
--pointer-check --bounds-check --function f
|
||||
^SIGNAL=0$
|
||||
^Counterexample:$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -2,7 +2,6 @@ CORE
|
|||
main.c
|
||||
--pointer-check --bounds-check
|
||||
^SIGNAL=0$
|
||||
^Counterexample:$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -3,7 +3,6 @@ main.c
|
|||
--pointer-check --bounds-check
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^Counterexample:$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -3,7 +3,6 @@ main.c
|
|||
|
||||
^SIGNAL=0$
|
||||
^\*\*\*\* WARNING: no body for function f$
|
||||
^Counterexample:$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -3,7 +3,6 @@ main.c
|
|||
|
||||
^SIGNAL=0$
|
||||
^\*\*\*\* WARNING: no body for function asd$
|
||||
^Counterexample:$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -3,7 +3,7 @@ main.c
|
|||
--unwind 1 --unwinding-assertions
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION FAILED$
|
||||
^ unwinding assertion loop 0$
|
||||
^\[.*] assertion g == 0: OK$
|
||||
^\[.*] unwinding assertion loop 0: FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -259,9 +259,15 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
|
|||
<< cover_goals.iterations() << " iteration"
|
||||
<< (cover_goals.iterations()==1?"":"s")
|
||||
<< ")" << eom;
|
||||
|
||||
bool safe=(cover_goals.number_covered()==0);
|
||||
|
||||
if(safe)
|
||||
bmc.report_success(); // legacy, might go away
|
||||
else
|
||||
bmc.report_failure(); // legacy, might go away
|
||||
|
||||
return (cover_goals.number_covered()==0)?
|
||||
safety_checkert::SAFE:safety_checkert::UNSAFE;
|
||||
return safe?safety_checkert::SAFE:safety_checkert::UNSAFE;
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
|
|
@ -557,9 +557,28 @@ safety_checkert::resultt bmct::decide(
|
|||
{
|
||||
prop_conv.set_message_handler(get_message_handler());
|
||||
|
||||
if(options.get_bool_option("all-properties"))
|
||||
if(options.get_bool_option("stop-on-fail"))
|
||||
return stop_on_fail(goto_functions, prop_conv);
|
||||
else
|
||||
return all_properties(goto_functions, prop_conv);
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: bmct::stop_on_fail
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
safety_checkert::resultt bmct::stop_on_fail(
|
||||
const goto_functionst &goto_functions,
|
||||
prop_convt &prop_conv)
|
||||
{
|
||||
switch(run_decision_procedure(prop_conv))
|
||||
{
|
||||
case decision_proceduret::D_UNSATISFIABLE:
|
||||
|
|
|
@ -92,6 +92,9 @@ protected:
|
|||
virtual resultt all_properties(
|
||||
const goto_functionst &goto_functions,
|
||||
prop_convt &solver);
|
||||
virtual resultt stop_on_fail(
|
||||
const goto_functionst &goto_functions,
|
||||
prop_convt &solver);
|
||||
virtual void show_vcc(std::ostream &out);
|
||||
virtual void show_program();
|
||||
virtual void report_success();
|
||||
|
|
|
@ -177,11 +177,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
|
|||
else
|
||||
options.set_option("simplify", true);
|
||||
|
||||
if(cmdline.isset("all-claims") || // will go away
|
||||
cmdline.isset("all-properties")) // use this one
|
||||
options.set_option("all-properties", true);
|
||||
if(cmdline.isset("stop-on-fail") ||
|
||||
cmdline.isset("property"))
|
||||
options.set_option("stop-on-fail", true);
|
||||
else
|
||||
options.set_option("all-properties", false);
|
||||
options.set_option("stop-on-fail", false);
|
||||
|
||||
if(cmdline.isset("unwind"))
|
||||
options.set_option("unwind", cmdline.get_value("unwind"));
|
||||
|
@ -1060,8 +1060,9 @@ void cbmc_parse_optionst::help()
|
|||
" cbmc file.c ... source file names\n"
|
||||
"\n"
|
||||
"Analysis options:\n"
|
||||
" --all-properties check and report status of all properties\n"
|
||||
" --show-properties show the properties, but don't run analysis\n"
|
||||
" --property id only check one specific property\n"
|
||||
" --stop-on-fail stop analysis once a failed property is detected\n"
|
||||
"\n"
|
||||
"C/C++ frontend options:\n"
|
||||
" -I path set include path (C/C++)\n"
|
||||
|
@ -1101,6 +1102,7 @@ void cbmc_parse_optionst::help()
|
|||
" --round-to-plus-inf rounding towards plus infinity\n"
|
||||
" --round-to-minus-inf rounding towards minus infinity\n"
|
||||
" --round-to-zero rounding towards zero\n"
|
||||
" --function name set main function name\n"
|
||||
"\n"
|
||||
"Program representations:\n"
|
||||
" --show-parse-tree show parse tree\n"
|
||||
|
@ -1130,8 +1132,6 @@ void cbmc_parse_optionst::help()
|
|||
" --nondet-static add nondeterministic initialization of variables with static lifetime\n"
|
||||
"\n"
|
||||
"BMC options:\n"
|
||||
" --function name set main function name\n"
|
||||
" --property id only check one specific property\n"
|
||||
" --program-only only show program expression\n"
|
||||
" --show-loops show the loops in the program\n"
|
||||
" --depth nr limit search depth\n"
|
||||
|
|
|
@ -53,7 +53,7 @@ class optionst;
|
|||
"(string-abstraction)(no-arch)(arch):" \
|
||||
"(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
|
||||
"(graphml-cex):(json-cex):" \
|
||||
"(floatbv)(all-claims)(all-properties)(decide)" // legacy, and will eventually disappear
|
||||
"(floatbv)(all-properties)" // legacy, and will eventually disappear
|
||||
|
||||
class cbmc_parse_optionst:
|
||||
public parse_options_baset,
|
||||
|
|
Loading…
Reference in New Issue