Skip to content

Cleanup of error handling of some of the files under goto-programs #2904

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 2 commits into from
Sep 20, 2018
+145 −190
Merged

Cleanup of error handling of some of the files under goto-programs #2904

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fe4a218
Convert asserts and throws to INVARIANTs for files starting with g
Aug 24, 2018
c952f55
Remove some preconditions and appropriately type the expressions.
NlightNFotis Sep 8, 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
53 changes: 22 additions & 31 deletions src/goto-programs/goto_convert_exceptions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,12 +18,10 @@ void goto_convertt::convert_msc_try_finally(
goto_programt &dest,
const irep_idt &mode)
{
if(code.operands().size()!=2)
{
error().source_location=code.find_source_location();
error() << "msc_try_finally expects two arguments" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
code.operands().size() == 2,
"msc_try_finally expects two arguments",
code.find_source_location());

goto_programt tmp;
tmp.add_instruction(SKIP)->source_location=code.source_location();
Expand Down Expand Up @@ -57,12 +55,10 @@ void goto_convertt::convert_msc_try_except(
goto_programt &dest,
const irep_idt &mode)
{
if(code.operands().size()!=3)
{
error().source_location=code.find_source_location();
error() << "msc_try_except expects three arguments" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
code.operands().size() == 3,
"msc_try_except expects three arguments",
code.find_source_location());

convert(to_code(code.op0()), dest, mode);

Expand All @@ -74,12 +70,8 @@ void goto_convertt::convert_msc_leave(
goto_programt &dest,
const irep_idt &mode)
{
if(!targets.leave_set)
{
error().source_location=code.find_source_location();
error() << "leave without target" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
targets.leave_set, "leave without target", code.find_source_location());

// need to process destructor stack
for(std::size_t d=targets.destructor_stack.size();
Expand All @@ -101,7 +93,10 @@ void goto_convertt::convert_try_catch(
goto_programt &dest,
const irep_idt &mode)
{
assert(code.operands().size()>=2);
INVARIANT_WITH_DIAGNOSTICS(
code.operands().size() >= 2,
"try_catch expects at least two arguments",
code.find_source_location());

// add the CATCH-push instruction to 'dest'
goto_programt::targett catch_push_instruction=dest.add_instruction();
Expand Down Expand Up @@ -159,12 +154,10 @@ void goto_convertt::convert_CPROVER_try_catch(
goto_programt &dest,
const irep_idt &mode)
{
if(code.operands().size()!=2)
{
error().source_location=code.find_source_location();
error() << "CPROVER_try_catch expects two arguments" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
code.operands().size() == 2,
"CPROVER_try_catch expects two arguments",
code.find_source_location());

// this is where we go after 'throw'
goto_programt tmp;
Expand Down Expand Up @@ -235,12 +228,10 @@ void goto_convertt::convert_CPROVER_try_finally(
goto_programt &dest,
const irep_idt &mode)
{
if(code.operands().size()!=2)
{
error().source_location=code.find_source_location();
error() << "CPROVER_try_finally expects two arguments" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
code.operands().size() == 2,
"CPROVER_try_finally expects two arguments",
code.find_source_location());

// first put 'finally' code onto destructor stack
targets.destructor_stack.push_back(to_code(code.op1()));
Expand Down
146 changes: 57 additions & 89 deletions src/goto-programs/goto_convert_side_effect.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,12 +60,10 @@ void goto_convertt::remove_assignment(
statement==ID_assign_bitxor ||
statement==ID_assign_bitor)
{
if(expr.operands().size()!=2)
{
error().source_location=expr.find_source_location();
error() << statement << " takes two arguments" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
expr.operands().size() == 2,
id2string(statement) + " expects two arguments",
expr.find_source_location());

irep_idt new_id;

Expand Down Expand Up @@ -93,10 +91,7 @@ void goto_convertt::remove_assignment(
new_id=ID_bitor;
else
{
error().source_location=expr.find_source_location();
error() << "assignment `" << statement << "' not yet supported"
<< eom;
throw 0;
UNREACHABLE;
}

exprt rhs;
Expand Down Expand Up @@ -143,17 +138,16 @@ void goto_convertt::remove_pre(
bool result_is_used,
const irep_idt &mode)
{
if(expr.operands().size()!=1)
{
error().source_location=expr.find_source_location();
error() << "preincrement/predecrement must have one operand" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
expr.operands().size() == 1,
"preincrement/predecrement must have one operand",
expr.find_source_location());

const irep_idt statement=expr.get_statement();

assert(statement==ID_preincrement ||
statement==ID_predecrement);
DATA_INVARIANT(
statement == ID_preincrement || statement == ID_predecrement,
"expects preincrement or predecrement");

exprt rhs;
rhs.add_source_location()=expr.source_location();
Expand Down Expand Up @@ -198,9 +192,7 @@ void goto_convertt::remove_pre(
constant_type=op_type;
else
{
error().source_location=expr.find_source_location();
error() << "no constant one of type " << op_type.pretty() << eom;
throw 0;
UNREACHABLE;
}

exprt constant=from_integer(1, constant_type);
Expand Down Expand Up @@ -235,18 +227,16 @@ void goto_convertt::remove_post(

// we have ...(op++)...

if(expr.operands().size()!=1)
{
error().source_location=expr.find_source_location();
error() << "postincrement/postdecrement must have one operand"
<< eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
expr.operands().size() == 1,
"postincrement/postdecrement must have one operand",
expr.find_source_location());

const irep_idt statement=expr.get_statement();

assert(statement==ID_postincrement ||
statement==ID_postdecrement);
DATA_INVARIANT(
statement == ID_postincrement || statement == ID_postdecrement,
"expects postincrement or postdecrement");

exprt rhs;
rhs.add_source_location()=expr.source_location();
Expand Down Expand Up @@ -291,9 +281,7 @@ void goto_convertt::remove_post(
constant_type=op_type;
else
{
error().source_location=expr.find_source_location();
error() << "no constant one of type " << op_type.pretty() << eom;
throw 0;
UNREACHABLE;
}

exprt constant;
Expand Down Expand Up @@ -338,9 +326,13 @@ void goto_convertt::remove_function_call(
const irep_idt &mode,
bool result_is_used)
{
INVARIANT_WITH_DIAGNOSTICS(
expr.operands().size() == 2,
"function_call expects two operands",
expr.find_source_location());

if(!result_is_used)
{
assert(expr.operands().size()==2);
code_function_callt call(nil_exprt(), expr.op0(), expr.op1().operands());
call.add_source_location()=expr.source_location();
convert_function_call(call, dest, mode);
Expand All @@ -350,20 +342,10 @@ void goto_convertt::remove_function_call(

// get name of function, if available

if(expr.id()!=ID_side_effect ||
expr.get(ID_statement)!=ID_function_call)
{
error().source_location=expr.find_source_location();
error() << "expected function call" << eom;
throw 0;
}

if(expr.operands().empty())
{
error().source_location=expr.find_source_location();
error() << "function_call expects at least one operand" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
expr.id() == ID_side_effect && expr.get(ID_statement) == ID_function_call,
"expects function call",
expr.find_source_location());

std::string new_base_name = "return_value";
irep_idt new_symbol_mode = mode;
Expand Down Expand Up @@ -445,7 +427,7 @@ void goto_convertt::remove_cpp_delete(
side_effect_exprt &expr,
goto_programt &dest)
{
assert(expr.operands().size()==1);
DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand");

codet tmp(expr.get_statement());
tmp.add_source_location()=expr.source_location();
Expand Down Expand Up @@ -498,13 +480,10 @@ void goto_convertt::remove_temporary_object(
goto_programt &dest)
{
const irep_idt &mode = expr.get(ID_mode);
if(expr.operands().size()!=1 &&
!expr.operands().empty())
{
error().source_location=expr.find_source_location();
error() << "temporary_object takes 0 or 1 operands" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
expr.operands().size() <= 1,
"temporary_object takes zero or one operands",
expr.find_source_location());

symbolt &new_symbol = new_tmp_symbol(
expr.type(), "obj", dest, expr.find_source_location(), mode);
Expand All @@ -518,7 +497,10 @@ void goto_convertt::remove_temporary_object(

if(expr.find(ID_initializer).is_not_nil())
{
assert(expr.operands().empty());
INVARIANT_WITH_DIAGNOSTICS(
expr.operands().empty(),
"temporary_object takes zero operands",
expr.find_source_location());
exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
replace_new_object(new_symbol.symbol_expr(), initializer);

Expand All @@ -539,19 +521,15 @@ void goto_convertt::remove_statement_expression(
// The expression is copied into a temporary before the
// scope is destroyed.

if(expr.operands().size()!=1)
{
error().source_location=expr.find_source_location();
error() << "statement_expression takes 1 operand" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
expr.operands().size() == 1,
"statement_expression takes one operand",
expr.find_source_location());

if(expr.op0().id()!=ID_code)
{
error().source_location=expr.op0().find_source_location();
error() << "statement_expression takes code as operand" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
expr.op0().id() == ID_code,
"statement_expression takes code as operand",
expr.find_source_location());

codet &code=to_code(expr.op0());

Expand All @@ -562,20 +540,15 @@ void goto_convertt::remove_statement_expression(
return;
}

if(code.get_statement()!=ID_block)
{
error().source_location=code.find_source_location();
error() << "statement_expression takes block as operand" << eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
code.get_statement() == ID_block,
"statement_expression takes block as operand",
code.find_source_location());

if(code.operands().empty())
{
error().source_location=expr.find_source_location();
error() << "statement_expression takes non-empty block as operand"
<< eom;
throw 0;
}
INVARIANT_WITH_DIAGNOSTICS(
!code.operands().empty(),
"statement_expression takes non-empty block as operand",
expr.find_source_location());

// get last statement from block, following labels
codet &last=to_code_block(code).find_last_statement();
Expand Down Expand Up @@ -604,10 +577,7 @@ void goto_convertt::remove_statement_expression(
}
else
{
error() << "statement_expression expects expression as "
<< "last statement, but got `"
<< last.get(ID_statement) << "'" << eom;
throw 0;
UNREACHABLE;
}

{
Expand Down Expand Up @@ -683,8 +653,6 @@ void goto_convertt::remove_side_effect(
}
else
{
error().source_location=expr.find_source_location();
error() << "cannot remove side effect (" << statement << ")" << eom;
throw 0;
UNREACHABLE;
}
}
Loading