Skip to content

Convert assert calls to INVARIANTs #4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jul 6, 2018
Merged

Convert assert calls to INVARIANTs #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/cbmc/bmc_cover.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -227,7 +227,7 @@ bool bmc_covert::operator()()
{
if(it->is_assert())
{
assert(it->source.pc->is_assert());
PRECONDITION(it->source.pc->is_assert());
const and_exprt c(
literal_exprt(it->guard_literal), literal_exprt(!it->cond_literal));
literalt l_c=solver.convert(c);
Expand All @@ -247,7 +247,8 @@ bool bmc_covert::operator()()
cover_goals.add(l);
}

assert(cover_goals.size()==goal_map.size());
INVARIANT(cover_goals.size()==goal_map.size(),
"We add coverage for each goal");

status() << "Running " << solver.decision_procedure_text() << eom;

Expand Down
3 changes: 2 additions & 1 deletion src/cbmc/cbmc_solvers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,8 @@ Author: Daniel Kroening, [email protected]
/// \return An smt2_dect::solvert giving the solver to use.
smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
{
assert(options.get_bool_option("smt2"));
// we shouldn't get here if this option isn't set
PRECONDITION(options.get_bool_option("smt2"));
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm this is not really a precondition of the function. I think in general it is fine to use INVARIANT even as the first statement in a function. But in the rest of the cbmc code base there are lots of PRECONDITION statements too that IMO should be INVARIANTSs instead.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you explain what you mean by "not a precondition"? While the value in here isn't really needed for anything in the function, it's certainly something that should be true when we enter this function right?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm I'm probably interpreting preconditions to narrowly. I basically took the view that a precondition is something that absolutely needs to hold when calling a function for it not to crash or produce garbage output. Like a function that unconditionally dereferences a pointer would have ptr != nullptr as a precondition, or a function that converts a string representing a binary number to an integer needs to get a string that contains only characters '0' and '1' (if it does not have built-in checks for this).

But currently in the codebase we have several preconditions that are more of the kind "here's something that happens to hold when we enter this function as it's currently used but it's not necessarily related to the function itself". Technically the functions could be used in different ways in the future and for those uses the preconditions might not apply anymore.

But the present case above seems somewhat like a corner case so I don't mind if we leave it as a PRECONDITION.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, but we should probably dig up what the intended meaning is and get everyone to agree to it.


smt2_dect::solvert s=smt2_dect::solvert::GENERIC;

Expand Down
4 changes: 2 additions & 2 deletions src/cbmc/cbmc_solvers.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,13 +71,13 @@ class cbmc_solverst:public messaget

prop_convt &prop_conv() const
{
assert(prop_conv_ptr!=nullptr);
PRECONDITION(prop_conv_ptr!=nullptr);
return *prop_conv_ptr;
}

propt &prop() const
{
assert(prop_ptr!=nullptr);
PRECONDITION(prop_ptr!=nullptr);
return *prop_ptr;
}

Expand Down
4 changes: 2 additions & 2 deletions src/cbmc/fault_localization.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ fault_localizationt::get_failed_property()
bool fault_localizationt::check(const lpointst &lpoints,
const lpoints_valuet &value)
{
assert(value.size()==lpoints.size());
PRECONDITION(value.size()==lpoints.size());
bvt assumptions;
lpoints_valuet::const_iterator v_it=value.begin();
for(const auto &l : lpoints)
Expand Down Expand Up @@ -142,7 +142,7 @@ void fault_localizationt::run(irep_idt goal_id)
{
// find failed property
failed=get_failed_property();
assert(failed!=bmc.equation.SSA_steps.end());
PRECONDITION(failed!=bmc.equation.SSA_steps.end());

if(goal_id==ID_nil)
goal_id=failed->source.pc->source_location.get_property_id();
Expand Down
20 changes: 13 additions & 7 deletions src/cbmc/symex_coverage.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,15 +139,17 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
const symex_coveraget::coveraget &coverage):
coverage_recordt("method")
{
assert(gf_it->second.body_available());
PRECONDITION(gf_it->second.body_available());

// identify the file name, inlined functions aren't properly
// accounted for
goto_programt::const_targett end_function=
--gf_it->second.body.instructions.end();
assert(end_function->is_end_function());
INVARIANT(end_function->is_end_function(),
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could use DATA_INVARIANT

"Last instruction in a function body is end function");
file_name=end_function->source_location.get_file();
assert(!file_name.empty());
INVARIANT(!file_name.empty(),
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could use DATA_INVARIANT

"Should have a valid source location");

// compute the maximum coverage of individual source-code lines
coverage_lines_mapt coverage_lines_map;
Expand Down Expand Up @@ -260,11 +262,14 @@ void goto_program_coverage_recordt::compute_coverage_lines(
for(const auto &cov : c_entry->second)
std::cerr << cov.second.succ->location_number << '\n';
}
assert(c_entry->second.size()==1 || is_branch);
INVARIANT(c_entry->second.size()==1 || is_branch,
"Instructions other than branch instructions have exactly 1 successor");

for(const auto &cov : c_entry->second)
{
assert(cov.second.num_executions>0);
INVARIANT(cov.second.num_executions>0,
// FIXME I don't know what this means
"Number of executions most be positive");

if(entry.first->second.hits==0)
++lines_covered;
Expand All @@ -275,7 +280,8 @@ void goto_program_coverage_recordt::compute_coverage_lines(
if(is_branch)
{
auto cond_entry=entry.first->second.conditions.find(it);
assert(cond_entry!=entry.first->second.conditions.end());
INVARIANT(cond_entry!=entry.first->second.conditions.end(),
"Branch should have condition");

if(it->get_target()==cov.second.succ)
{
Expand Down Expand Up @@ -439,7 +445,7 @@ bool symex_coveraget::generate_report(
const goto_functionst &goto_functions,
const std::string &path) const
{
assert(!path.empty());
PRECONDITION(!path.empty());

if(path=="-")
return output_report(goto_functions, std::cout);
Expand Down