Skip to content

Replace asserts and throws under goto-symex #6

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

Closed
wants to merge 9 commits into from
Closed

Replace asserts and throws under goto-symex #6

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
16d03d7
Replace asserts and throws with INVARIANT etc.
Jul 10, 2018
526945e
Translate asserts and throws to PRECONDITIONS and INVARIANTS
NlightNFotis Jul 19, 2018
112bd5b
Add changes suggested during code review.
NlightNFotis Jul 23, 2018
c7fb551
Move equation conversion exception to exception utils
NlightNFotis Jul 24, 2018
b43902e
Address the latest review comments.
NlightNFotis Jul 27, 2018
2d913c4
Fixup into second
NlightNFotis Aug 30, 2018
77b43ea
Add into the third one.
NlightNFotis Aug 30, 2018
46aeea4
Some minor fixes
NlightNFotis Aug 30, 2018
f2a7a37
Some more changes.
NlightNFotis Aug 31, 2018
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
6 changes: 4 additions & 2 deletions src/goto-symex/build_goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,8 +91,10 @@ exprt build_full_lhs_rec(
else if(id==ID_byte_extract_little_endian ||
id==ID_byte_extract_big_endian)
{
DATA_INVARIANT(
src_original.operands().size() == 2,
"byte extract expressions require two operands");
exprt tmp=src_original;
assert(tmp.operands().size()==2);
tmp.op0()=build_full_lhs_rec(prop_conv, ns, tmp.op0(), src_ssa.op0());

// re-write into big case-split
Expand Down Expand Up @@ -222,7 +224,7 @@ void build_goto_trace(
else if(it->is_atomic_end() && current_time<0)
current_time*=-1;

assert(current_time>=0);
INVARIANT(current_time>=0, "time keeping inconsistency");
Copy link
Owner

Choose a reason for hiding this comment

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

Again, isn't this a DATA_INVARIANT?

Copy link
Author

Choose a reason for hiding this comment

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

No. This is what the DATA_INVARIANT's documentation says:

// This condition should be used to document that assumptions that are
// made on goto_functions, goto_programs, exprts, etc. being well formed.
// "The data structure is corrupt or malformed"

To my understanding this is to assert properties of fundamental data structures representing the program under analysis. In this case current_time is a local variable that is only required to be consistent during the execution of the function.

Copy link
Owner

Choose a reason for hiding this comment

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

Seems reasonable, thanks.

// move any steps gathered in an atomic section

if(time_before<0)
Expand Down
47 changes: 0 additions & 47 deletions src/goto-symex/equation_conversion_exceptions.h
View file
Open in desktop

This file was deleted.

17 changes: 9 additions & 8 deletions src/goto-symex/goto_symex_state.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,7 @@ void goto_symex_statet::level0t::operator()(

const symbolt *s;
const bool found_l0 = !ns.lookup(obj_identifier, s);
DATA_INVARIANT(
found_l0, "level0: failed to find " + id2string(obj_identifier));
INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
Copy link

Choose a reason for hiding this comment

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

Nice catch, this indeed doesn't seem to meet the definition of DATA_INVARIANT


// don't rename shared variables or functions
if(s->type.id()==ID_code ||
Expand Down Expand Up @@ -187,8 +186,9 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
}
else if(expr.id()==ID_member)
{
if(expr.operands().size()!=1)
throw "member expects one operand";
DATA_INVARIANT(
expr.operands().size() == 1,
"member expression expects one operand");

return constant_propagation_reference(expr.op0());
}
Expand Down Expand Up @@ -496,11 +496,12 @@ void goto_symex_statet::rename(
else if(expr.id()==ID_address_of)
{
DATA_INVARIANT(
expr.operands().size() == 1, "address_of should have a single operand");
rename_address(expr.op0(), ns, level);
expr.type().id() == ID_pointer,
"type of expression required to be pointer");
DATA_INVARIANT(
expr.type().id() == ID_pointer,
"type of address_of should be ID_pointer");
expr.operands().size() == 1,
"address_of should have a single operand");
rename_address(expr.op0(), ns, level);
expr.type().subtype()=expr.op0().type();
}
else
Expand Down
4 changes: 2 additions & 2 deletions src/goto-symex/memory_model_pso.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,8 @@ bool memory_model_psot::program_order_is_relaxed(
partial_order_concurrencyt::event_it e1,
partial_order_concurrencyt::event_it e2) const
{
assert(e1->is_shared_read() || e1->is_shared_write());
assert(e2->is_shared_read() || e2->is_shared_write());
PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
PRECONDITION(e2->is_shared_read() || e2->is_shared_write());

// no po relaxation within atomic sections
if(e1->atomic_section_id!=0 &&
Expand Down
4 changes: 2 additions & 2 deletions src/goto-symex/memory_model_sc.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,8 @@ bool memory_model_sct::program_order_is_relaxed(
partial_order_concurrencyt::event_it e1,
partial_order_concurrencyt::event_it e2) const
{
assert(e1->is_shared_read() || e1->is_shared_write());
assert(e2->is_shared_read() || e2->is_shared_write());
PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
PRECONDITION(e2->is_shared_read() || e2->is_shared_write());

Copy link
Owner

Choose a reason for hiding this comment

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

Not a comment on this change, but "yuck" to this function... it's basically just an assertion in it's own right, or it's using preconditions as control flow/error handling. Might be worth checking where this function is used, because if its used in anyway that doesn't just use it as an assertion, that use-site needs looking at/adjusting.

Copy link

Choose a reason for hiding this comment

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

It seems that this method is an implementation of a virtual method in the base class. For the particular memory model (sequential consistency), just returning false is the correct thing, but for other memory models a nontrivial implementation might be required.

return false;
}
Expand Down
4 changes: 2 additions & 2 deletions src/goto-symex/memory_model_tso.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,8 +39,8 @@ bool memory_model_tsot::program_order_is_relaxed(
partial_order_concurrencyt::event_it e1,
partial_order_concurrencyt::event_it e2) const
{
assert(e1->is_shared_read() || e1->is_shared_write());
assert(e2->is_shared_read() || e2->is_shared_write());
PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
PRECONDITION(e2->is_shared_read() || e2->is_shared_write());

// no po relaxation within atomic sections
if(e1->atomic_section_id!=0 &&
Expand Down
6 changes: 3 additions & 3 deletions src/goto-symex/partial_order_concurrency.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -142,8 +142,8 @@ symbol_exprt partial_order_concurrencyt::clock(
event_it event,
axiomt axiom)
{
PRECONDITION(!numbering.empty());
irep_idt identifier;
assert(!numbering.empty());

if(event->is_shared_write())
identifier=rw_clock_id(event, axiom);
Expand All @@ -163,7 +163,7 @@ symbol_exprt partial_order_concurrencyt::clock(

void partial_order_concurrencyt::build_clock_type()
{
assert(!numbering.empty());
PRECONDITION(!numbering.empty());

std::size_t width = address_bits(numbering.size());
clock_type = unsignedbv_typet(width);
Expand Down Expand Up @@ -198,7 +198,7 @@ exprt partial_order_concurrencyt::before(
binary_relation_exprt(clock(e1, ax), ID_lt, clock(e2, ax)));
}

assert(!ops.empty());
POSTCONDITION(!ops.empty());

return conjunction(ops);
}
Expand Down
18 changes: 12 additions & 6 deletions src/goto-symex/postcondition.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,20 +76,22 @@ bool postconditiont::is_used_address_of(
}
else if(expr.id()==ID_index)
{
assert(expr.operands().size()==2);

DATA_INVARIANT(
expr.operands().size() == 2, "index expression should have two operands");
Copy link
Owner

Choose a reason for hiding this comment

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

Nit: Indentation is wrong?

return
is_used_address_of(expr.op0(), identifier) ||
is_used(expr.op1(), identifier);
}
else if(expr.id()==ID_member)
{
assert(expr.operands().size()==1);
DATA_INVARIANT(
expr.operands().size() == 1, "member expression should only have one operand");
Copy link
Owner

Choose a reason for hiding this comment

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

Nit: Indentation is wrong?

return is_used_address_of(expr.op0(), identifier);
}
else if(expr.id()==ID_dereference)
{
assert(expr.operands().size()==1);
DATA_INVARIANT(
expr.operands().size() == 1, "dereference expression should only have one operand");
Copy link
Owner

Choose a reason for hiding this comment

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

Nit: Indentation again.

return is_used(expr.op0(), identifier);
}

Expand Down Expand Up @@ -155,7 +157,9 @@ bool postconditiont::is_used(
if(expr.id()==ID_address_of)
{
// only do index!
assert(expr.operands().size()==1);
DATA_INVARIANT(
expr.operands().size() == 1,
"address_of expression expected to have one operand at this point");
return is_used_address_of(expr.op0(), identifier);
}
else if(expr.id()==ID_symbol &&
Expand All @@ -169,7 +173,9 @@ bool postconditiont::is_used(
}
else if(expr.id()==ID_dereference)
{
assert(expr.operands().size()==1);
DATA_INVARIANT(
expr.operands().size() == 1,
"dereference expression expected to have one operand");

// aliasing may happen here

Expand Down
17 changes: 12 additions & 5 deletions src/goto-symex/precondition.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,18 +78,21 @@ void preconditiont::compute_address_of(exprt &dest)
}
else if(dest.id()==ID_index)
{
assert(dest.operands().size()==2);
DATA_INVARIANT(
Copy link
Owner

Choose a reason for hiding this comment

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

Indentation looks wrong in all the changes in this file

dest.operands().size() == 2, "index expression expected to have two operands");
compute_address_of(dest.op0());
compute(dest.op1());
}
else if(dest.id()==ID_member)
{
assert(dest.operands().size()==1);
DATA_INVARIANT(
dest.operands().size() == 1, "member expression expected to have one operand");
compute_address_of(dest.op0());
}
else if(dest.id()==ID_dereference)
{
assert(dest.operands().size()==1);
DATA_INVARIANT(
dest.operands().size() == 1, "dereference expression expected to have 1 operand");
compute(dest.op0());
}
}
Expand All @@ -104,12 +107,16 @@ void preconditiont::compute_rec(exprt &dest)
if(dest.id()==ID_address_of)
{
// only do index!
assert(dest.operands().size()==1);
DATA_INVARIANT(
dest.operands().size() == 1,
"address_of expression expected to have one operand at this point");
Copy link
Owner

Choose a reason for hiding this comment

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

"at this point" isn't needed - keep them tight.

compute_address_of(dest.op0());
}
else if(dest.id()==ID_dereference)
{
assert(dest.operands().size()==1);
DATA_INVARIANT(
dest.operands().size() == 1,
"dereference expression expected to have one operand at this point");

Copy link
Owner

Choose a reason for hiding this comment

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

"at this point" isn't needed

const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();

Expand Down
4 changes: 2 additions & 2 deletions src/goto-symex/slice.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)
void symex_slicet::slice_assignment(
symex_target_equationt::SSA_stept &SSA_step)
{
assert(SSA_step.ssa_lhs.id()==ID_symbol);
PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);
Copy link
Owner

Choose a reason for hiding this comment

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

Is this a DATA_INVARIANT?

Copy link
Author

Choose a reason for hiding this comment

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

No, this falls very clearly under the PRECONDITION case according to the documentation in src/util/invariant.h

const irep_idt &id=SSA_step.ssa_lhs.get_identifier();

if(depends.find(id)==depends.end())
Expand All @@ -127,7 +127,7 @@ void symex_slicet::slice_assignment(
void symex_slicet::slice_decl(
symex_target_equationt::SSA_stept &SSA_step)
{
assert(SSA_step.ssa_lhs.id()==ID_symbol);
PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);
Copy link
Owner

Choose a reason for hiding this comment

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

DATA_INVARIANT ?

Copy link
Author

Choose a reason for hiding this comment

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

Again, no, because this makes an assertion about the function arguments as the first thing the function does.

const irep_idt &id=SSA_step.ssa_lhs.get_identifier();

if(depends.find(id)==depends.end())
Expand Down
17 changes: 10 additions & 7 deletions src/goto-symex/slice_by_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,13 @@ void symex_slice_by_tracet::slice_by_trace(
{
exprt g_copy(*i);

DATA_INVARIANT(
g_copy.id() == ID_symbol ||
g_copy.id() == ID_not ||
g_copy.id() == ID_and ||
g_copy.id() == ID_constant,
"guards should only be and, symbol, constant, or `not'");
Copy link

Choose a reason for hiding this comment

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

Previously, this was throwing an exception for ID_and (but the comment suggested that guards can be and). Is this a deliberate change?

Copy link
Author

@NlightNFotis NlightNFotis Jul 24, 2018 •
edited
Loading

Choose a reason for hiding this comment

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

@johnnonweiler No it wasn't (https://github.com/diffblue/cbmc/blob/develop/src/goto-symex/slice_by_trace.cpp#L95). What that did is that it checked if the expression's type is ID_symbol or ID_not which was handled in the first if consequent statement, then it checked if the expression's type is ID_and, which was handled in the second consequent statement (else if (g_copy.id()==ID_and)...) and last it was throwing an exception if the expression's type was anything but a constant (else if (!(g_copy.id()==ID_constant)) - based on the idea that it had checked for the other meaningful types and handled them, and left the constant case unhandled but crashed on anything else).

This INVARIANT does the same thing, just earlier, while it also drops the unneeded exception now.

Copy link

Choose a reason for hiding this comment

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

Sorry @NlightNFotis - I got confused by GitHub hiding a couple of lines in the diff!


if(g_copy.id()==ID_symbol || g_copy.id() == ID_not)
{
g_copy.make_not();
Expand All @@ -92,10 +99,6 @@ void symex_slice_by_tracet::slice_by_trace(
simplify(copy_last, ns);
implications.insert(copy_last);
}
else if(!(g_copy.id()==ID_constant))
{
throw "guards should only be and, symbol, constant, or `not'";
}
}

slice_SSA_steps(equation, implications); // Slice based on implications
Expand Down Expand Up @@ -219,9 +222,9 @@ void symex_slice_by_tracet::parse_events(std::string read_line)
const std::string::size_type vnext=read_line.find(",", vidx);
std::string event=read_line.substr(vidx, vnext - vidx);
eis.insert(event);
if((!alphabet.empty()) &&
((alphabet.count(event)!=0)!=alphabet_parity))
throw "trace uses symbol not in alphabet: "+event;
PRECONDITION(!alphabet.empty());
INVARIANT((alphabet.count(event) != 0) == alphabet_parity,
Copy link
Owner

Choose a reason for hiding this comment

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

DATA_INVARIANT ?

Copy link
Author

Choose a reason for hiding this comment

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

No, this is not a data structure that represents the program under analysis to my understanding (i.e. not an exprt, goto-programt, etc)

"trace uses symbol not in alphabet: " + event);
Copy link
Owner

Choose a reason for hiding this comment

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

Description should describe what is being asserted.... "trace symbol must be in alphabet"

if(vnext==std::string::npos)
break;
vidx=vnext;
Expand Down
Loading