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 2 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
4 changes: 2 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 @@ -92,7 +92,7 @@ exprt build_full_lhs_rec(
id==ID_byte_extract_big_endian)
{
exprt tmp=src_original;
assert(tmp.operands().size()==2);
PRECONDITION(tmp.operands().size() == 2);
Copy link
Owner

Choose a reason for hiding this comment

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

Minor nit: Why not move the PRECONDITION to be the first line in the block?

Copy link
Owner

Choose a reason for hiding this comment

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

Should this be a DATA_INVARIANT ?

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 +222,7 @@ void build_goto_trace(
else if(it->is_atomic_end() && current_time<0)
current_time*=-1;

assert(current_time>=0);
PRECONDITION(current_time>=0);
Copy link

Choose a reason for hiding this comment

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

This isn't a precondition, this is an invariant that's supposed to be maintained by the current code block.

(Again, difference - Precondition failure is meant to indicate that the function was used incorrectly, whereas most other invariant failures are meant to indicate that the function itself is broken).

// move any steps gathered in an atomic section

if(time_before<0)
Expand Down
13 changes: 4 additions & 9 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,7 @@ 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";
PRECONDITION(expr.operands().size() == 1);
Copy link
Owner

Choose a reason for hiding this comment

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

Surely 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.

By definition this falls between multiple categories of the invariant checks (it falls both under DATA_INVARIANT because it checks fundamental data structures like an exprt in this case, but it also falls under the PRECONDITION case, in that it's asserting whether an argument of the function is correct and the rest of the computation can be sound based on that assertion.

But I can certainly change it to the DATA_INVARIANT in case it makes things a little bit cleaner.


return constant_propagation_reference(expr.op0());
}
Expand Down Expand Up @@ -495,12 +493,9 @@ 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");
PRECONDITION(expr.operands().size() == 1);
Copy link

Choose a reason for hiding this comment

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

No, this should be a DATA_INVARIANT.

rename_address(expr.op0(), ns, level);
DATA_INVARIANT(
expr.type().id() == ID_pointer,
"type of address_of should be ID_pointer");
PRECONDITION(expr.type().id() == ID_pointer);
Copy link

Choose a reason for hiding this comment

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

This should probably be the first thing that's being checked in this block?

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 @@ -143,7 +143,7 @@ symbol_exprt partial_order_concurrencyt::clock(
axiomt axiom)
{
irep_idt identifier;
assert(!numbering.empty());
PRECONDITION(!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
11 changes: 5 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,19 @@ bool postconditiont::is_used_address_of(
}
else if(expr.id()==ID_index)
{
assert(expr.operands().size()==2);

PRECONDITION(expr.operands().size() == 2);
Copy link

Choose a reason for hiding this comment

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

DATA_INVARIANT

return
is_used_address_of(expr.op0(), identifier) ||
is_used(expr.op1(), identifier);
}
else if(expr.id()==ID_member)
{
assert(expr.operands().size()==1);
PRECONDITION(expr.operands().size() == 1);
Copy link

Choose a reason for hiding this comment

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

DATA_INVARIANT

return is_used_address_of(expr.op0(), identifier);
}
else if(expr.id()==ID_dereference)
{
assert(expr.operands().size()==1);
PRECONDITION(expr.operands().size() == 1);
Copy link

Choose a reason for hiding this comment

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

DATA_INVARIANT

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

Expand Down Expand Up @@ -155,7 +154,7 @@ bool postconditiont::is_used(
if(expr.id()==ID_address_of)
{
// only do index!
assert(expr.operands().size()==1);
PRECONDITION(expr.operands().size() == 1);
Copy link

Choose a reason for hiding this comment

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

DATA_INVARIANT

return is_used_address_of(expr.op0(), identifier);
}
else if(expr.id()==ID_symbol &&
Expand All @@ -169,7 +168,7 @@ bool postconditiont::is_used(
}
else if(expr.id()==ID_dereference)
{
assert(expr.operands().size()==1);
PRECONDITION(expr.operands().size() == 1);
Copy link

Choose a reason for hiding this comment

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

DATA_INVARIANT


// aliasing may happen here

Expand Down
10 changes: 5 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,18 @@ void preconditiont::compute_address_of(exprt &dest)
}
else if(dest.id()==ID_index)
{
assert(dest.operands().size()==2);
PRECONDITION(dest.operands().size() == 2);
Copy link

Choose a reason for hiding this comment

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

DATA_INVARIANT

compute_address_of(dest.op0());
compute(dest.op1());
}
else if(dest.id()==ID_member)
{
assert(dest.operands().size()==1);
PRECONDITION(dest.operands().size() == 1);
Copy link

Choose a reason for hiding this comment

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

DATA_INVARIANT

compute_address_of(dest.op0());
}
else if(dest.id()==ID_dereference)
{
assert(dest.operands().size()==1);
PRECONDITION(dest.operands().size() == 1);
Copy link

Choose a reason for hiding this comment

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

DATA_INVARIANT

compute(dest.op0());
}
}
Expand All @@ -104,12 +104,12 @@ void preconditiont::compute_rec(exprt &dest)
if(dest.id()==ID_address_of)
{
// only do index!
assert(dest.operands().size()==1);
PRECONDITION(dest.operands().size() == 1);
Copy link

Choose a reason for hiding this comment

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

DATA_INVARIANT

compute_address_of(dest.op0());
}
else if(dest.id()==ID_dereference)
{
assert(dest.operands().size()==1);
PRECONDITION(dest.operands().size() == 1);
Copy link

Choose a reason for hiding this comment

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

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.

"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
15 changes: 11 additions & 4 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);

INVARIANT(
Copy link

Choose a reason for hiding this comment

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

I'm actually a bit ambivalent about this. Arguably could be a precondition, but since we're not using function args directly we should probably keep this an invariant.

Copy link
Owner

Choose a reason for hiding this comment

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

I'd almost be tempted to say its a 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 @@ -94,7 +101,7 @@ void symex_slice_by_tracet::slice_by_trace(
}
else if(!(g_copy.id()==ID_constant))
{
throw "guards should only be and, symbol, constant, or `not'";
UNHANDLED_CASE;
Copy link
Author

Choose a reason for hiding this comment

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

Some rationale for the changes: This is just for documentation purposes, the INVARIANT above should have crashed it anyway if it's something different.

Copy link

Choose a reason for hiding this comment

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

"// The following should not be used in new code and are only intended
// to migrate documentation and "error handling" in older code"

I don't think this check is even necessary, but if you want to keep it I'd keep it as an unconditional else and have an INVARIANT(g.copy.id() == ID_constant, "blah blah only constants possible after this blah blash").

Copy link
Author

Choose a reason for hiding this comment

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

You're right, I decided to kill it all together.

}
}

Expand Down Expand Up @@ -219,9 +226,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
24 changes: 11 additions & 13 deletions src/goto-symex/symex_assign.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ void goto_symext::symex_assign(

if(statement==ID_function_call)
{
assert(!side_effect_expr.operands().empty());
PRECONDITION(!side_effect_expr.operands().empty());
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?


if(side_effect_expr.op0().id()!=ID_symbol)
throw "symex_assign: expected symbol as function";
Expand Down Expand Up @@ -91,12 +91,12 @@ exprt goto_symext::add_to_lhs(
const exprt &lhs,
const exprt &what)
{
assert(lhs.id()!=ID_symbol);
PRECONDITION(lhs.id() != ID_symbol);
exprt tmp_what=what;

if(tmp_what.id()!=ID_symbol)
{
assert(tmp_what.operands().size()>=1);
PRECONDITION(tmp_what.operands().size() >= 1);
Copy link

Choose a reason for hiding this comment

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

I think it'd be better to make that precondition on what rather than tmp_what. In any case, the if seems to be redundant (not really part of this PR obviously).

Copy link
Author

Choose a reason for hiding this comment

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

I'd rather not, as tmp_what is just a copy, and the if statement is operating on the tmp_what.

Copy link
Owner

Choose a reason for hiding this comment

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

Could be 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.

Yes, but I think it's better left as a PRECONDITION. Does the same thing as the PRECONDITION above it, i.e. asserts function input parameter condition, which according to the documentation of invariant.h falls cleanly under the PRECONDITION case. Unless there are some strong feelings about it, I'd rather not change it.

tmp_what.op0().make_nil();
}

Expand All @@ -106,12 +106,12 @@ exprt goto_symext::add_to_lhs(

while(p->is_not_nil())
{
assert(p->id()!=ID_symbol);
assert(p->operands().size()>=1);
PRECONDITION(p->id()!=ID_symbol);
Copy link

Choose a reason for hiding this comment

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

INVARIANT, because we keep changing p

PRECONDITION(p->operands().size()>=1);
Copy link

Choose a reason for hiding this comment

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

Same here... and I'm slightly concerned this keeps checking for the number of operands... this suggests it's looking for a particular type of operator, but it's really not obvious to me what that is.

p=&p->op0();
}

assert(p->is_nil());
PRECONDITION(p->is_nil());
Copy link

Choose a reason for hiding this comment

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

INVARIANT (established by the previous loop).


*p=tmp_what;
return new_lhs;
Expand Down Expand Up @@ -172,7 +172,7 @@ void goto_symext::symex_assign_rec(
lhs.id()==ID_complex_imag)
{
// this is stuff like __real__ x = 1;
assert(lhs.operands().size()==1);
PRECONDITION(lhs.operands().size() == 1);
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.

Same as above, asserts function input parameters, which makes it clearly a PRECONDITION. Could also be a DATA_INVARIANT, but I don't see a particularly good reason as to why it should be changed, as the DATA_INVARIANT is essentially the same thing, with just an extra comment (which in this case would be completely redundant IMO)


exprt new_rhs=exprt(ID_complex, lhs.op0().type());
new_rhs.operands().resize(2);
Expand Down Expand Up @@ -282,8 +282,7 @@ void goto_symext::symex_assign_typecast(
assignment_typet assignment_type)
{
// these may come from dereferencing on the lhs

assert(lhs.operands().size()==1);
PRECONDITION(lhs.operands().size() == 1);
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.

I don't think so, looks like a pretty clear PRECONDITION to me, unless there's a reason to make it a DATA_INVARIANT that I don't see.


exprt rhs_typecasted=rhs;
rhs_typecasted.make_typecast(lhs.op0().type());
Expand All @@ -305,9 +304,8 @@ void goto_symext::symex_assign_array(
// lhs must be index operand
// that takes two operands: the first must be an array
// the second is the index

if(lhs.operands().size()!=2)
throw "index must have two operands";
DATA_INVARIANT(lhs.operands().size() == 2,
"index_exprt takes two operands: first must be array; second must be the index");
Copy link
Owner

Choose a reason for hiding this comment

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

The message here contains more information that the invariant is actually checking for...
Indentation is also wrong


const exprt &lhs_array=lhs.array();
const exprt &lhs_index=lhs.index();
Expand Down Expand Up @@ -368,7 +366,7 @@ void goto_symext::symex_assign_struct_member(
// typecasts involved? C++ does that for inheritance.
if(lhs_struct.id()==ID_typecast)
{
assert(lhs_struct.operands().size()==1);
PRECONDITION(lhs_struct.operands().size() == 1);
Copy link

Choose a reason for hiding this comment

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

DATA_INVARIANT


if(lhs_struct.op0().id() == ID_null_object)
{
Expand Down
13 changes: 6 additions & 7 deletions src/goto-symex/symex_atomic_section.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,9 +17,9 @@ void goto_symext::symex_atomic_begin(statet &state)
return;

// we don't allow any nesting of atomic sections
if(state.atomic_section_id!=0)
throw "nested atomic section detected at "+
state.source.pc->source_location.as_string();
INVARIANT(state.atomic_section_id == 0,
"nested atomic section detected at " +
Copy link

Choose a reason for hiding this comment

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

I'd suggest changing the message of this to the comment i.e. INVARIANT(..., "we don't allow any nesting of atomic sections")

That said, I'm not 100% certain this should be an invariant rather than an error message...

state.source.pc->source_location.as_string());

state.atomic_section_id=++atomic_section_counter;
state.read_in_atomic_section.clear();
Expand All @@ -36,8 +36,7 @@ void goto_symext::symex_atomic_end(statet &state)
if(state.guard.is_false())
return;

if(state.atomic_section_id==0)
throw "ATOMIC_END unmatched"; // NOLINT(readability/throw)
INVARIANT(state.atomic_section_id != 0, "ATOMIC_END unmatched");
Copy link

Choose a reason for hiding this comment

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

IMHO Invariant messages should explain why the invariant holds, rather than reporting an error message

Copy link
Owner

Choose a reason for hiding this comment

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

Agree with Hannes here.


const unsigned atomic_section_id=state.atomic_section_id;
state.atomic_section_id=0;
Expand All @@ -51,7 +50,7 @@ void goto_symext::symex_atomic_end(statet &state)
r.set_level_2(r_it->second.first);

// guard is the disjunction over reads
assert(!r_it->second.second.empty());
PRECONDITION(!r_it->second.second.empty());
Copy link

Choose a reason for hiding this comment

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

IMHO should be INVARIANT rather than PRECONDITION - arguably involves function arguments, but not directly.

Copy link
Author

Choose a reason for hiding this comment

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

I'd much rather this stays, because it signals assertion over function arguments (iterates over statet &state which is an argument).

Copy link
Owner

Choose a reason for hiding this comment

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

I'd lean towards INVARIANT or DATA_INVARIANT...

guardt read_guard(r_it->second.second.front());
for(std::list<guardt>::const_iterator
it=++(r_it->second.second.begin());
Expand All @@ -77,7 +76,7 @@ void goto_symext::symex_atomic_end(statet &state)
w.set_level_2(state.level2.current_count(w.get_identifier()));

// guard is the disjunction over writes
assert(!w_it->second.empty());
PRECONDITION(!w_it->second.empty());
Copy link

Choose a reason for hiding this comment

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

Same here

Copy link
Owner

Choose a reason for hiding this comment

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

Agree with Hannes here too.

guardt write_guard(w_it->second.front());
for(std::list<guardt>::const_iterator
it=++(w_it->second.begin());
Expand Down
Loading