Skip to content

Remove now-unused bitvector conversion exceptions #4691

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
May 30, 2019
Merged

Remove now-unused bitvector conversion exceptions #4691

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
47 changes: 0 additions & 47 deletions src/goto-symex/equation_conversion_exceptions.h
View file
Open in desktop

This file was deleted.

100 changes: 17 additions & 83 deletions src/goto-symex/symex_target_equation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,13 +14,9 @@ Author: Daniel Kroening, [email protected]

#include <util/format_expr.h>
#include <util/std_expr.h>
#include <util/throw_with_nested.h>
#include <util/unwrap_nested_exception.h>

#include <solvers/decision_procedure.h>
#include <solvers/flattening/bv_conversion_exceptions.h>

#include "equation_conversion_exceptions.h"
#include "goto_symex_state.h"
#include "ssa_step.h"

Expand Down Expand Up @@ -329,24 +325,15 @@ void symex_target_equationt::constraint(

void symex_target_equationt::convert(decision_proceduret &decision_procedure)
{
try
{
convert_guards(decision_procedure);
convert_assignments(decision_procedure);
convert_decls(decision_procedure);
convert_assumptions(decision_procedure);
convert_assertions(decision_procedure);
convert_goto_instructions(decision_procedure);
convert_function_calls(decision_procedure);
convert_io(decision_procedure);
convert_constraints(decision_procedure);
}
catch(const equation_conversion_exceptiont &conversion_exception)
{
// unwrap the except and throw like normal
const std::string full_error = unwrap_exception(conversion_exception);
throw full_error;
}
convert_guards(decision_procedure);
convert_assignments(decision_procedure);
convert_decls(decision_procedure);
convert_assumptions(decision_procedure);
convert_assertions(decision_procedure);
convert_goto_instructions(decision_procedure);
convert_function_calls(decision_procedure);
convert_io(decision_procedure);
convert_constraints(decision_procedure);
}

void symex_target_equationt::convert_assignments(
Expand Down Expand Up @@ -376,17 +363,8 @@ void symex_target_equationt::convert_decls(
{
// The result is not used, these have no impact on
// the satisfiability of the formula.
try
{
decision_procedure.handle(step.cond_expr);
step.converted = true;
}
catch(const bitvector_conversion_exceptiont &)
{
util_throw_with_nested(
equation_conversion_exceptiont(
"Error converting decls for step", step));
}
decision_procedure.handle(step.cond_expr);
step.converted = true;
}
}
}
Expand All @@ -405,16 +383,7 @@ void symex_target_equationt::convert_guards(
mstream << messaget::eom;
});

try
{
step.guard_handle = decision_procedure.handle(step.guard);
}
catch(const bitvector_conversion_exceptiont &)
{
util_throw_with_nested(
equation_conversion_exceptiont(
"Error converting guard for step", step));
}
step.guard_handle = decision_procedure.handle(step.guard);
}
}
}
Expand All @@ -436,16 +405,7 @@ void symex_target_equationt::convert_assumptions(
mstream << messaget::eom;
});

try
{
step.cond_handle = decision_procedure.handle(step.cond_expr);
}
catch(const bitvector_conversion_exceptiont &)
{
util_throw_with_nested(
equation_conversion_exceptiont(
"Error converting assumptions for step", step));
}
step.cond_handle = decision_procedure.handle(step.cond_expr);
}
}
}
Expand All @@ -468,16 +428,7 @@ void symex_target_equationt::convert_goto_instructions(
mstream << messaget::eom;
});

try
{
step.cond_handle = decision_procedure.handle(step.cond_expr);
}
catch(const bitvector_conversion_exceptiont &)
{
util_throw_with_nested(
equation_conversion_exceptiont(
"Error converting goto instructions for step", step));
}
step.cond_handle = decision_procedure.handle(step.cond_expr);
}
}
}
Expand All @@ -495,16 +446,8 @@ void symex_target_equationt::convert_constraints(
mstream << messaget::eom;
});

try
{
decision_procedure.set_to_true(step.cond_expr);
step.converted = true;
}
catch(const bitvector_conversion_exceptiont &)
{
util_throw_with_nested(equation_conversion_exceptiont(
"Error converting constraints for step", step));
}
decision_procedure.set_to_true(step.cond_expr);
step.converted = true;
}
}
}
Expand Down Expand Up @@ -569,16 +512,7 @@ void symex_target_equationt::convert_assertions(
step.cond_expr);

// do the conversion
try
{
step.cond_handle = decision_procedure.handle(implication);
}
catch(const bitvector_conversion_exceptiont &)
{
util_throw_with_nested(
equation_conversion_exceptiont(
"Error converting assertions for step", step));
}
step.cond_handle = decision_procedure.handle(implication);

// store disjunct
disjuncts.push_back(not_exprt(step.cond_handle));
Expand Down
3 changes: 0 additions & 3 deletions src/solvers/flattening/boolbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,9 +171,6 @@ bvt boolbvt::conversion_failed(const exprt &expr)
/// \param expr: Expression to convert
/// \return A vector of literals corresponding to the outputs of the Boolean
/// circuit
/// \throws bitvector_conversion_exceptiont raised if converting byte_extraction
/// goes wrong.
/// TODO: extend for other types of conversion exception (diffblue/cbmc#2103).
bvt boolbvt::convert_bitvector(const exprt &expr)
{
if(expr.type().id()==ID_bool)
Expand Down
13 changes: 1 addition & 12 deletions src/solvers/flattening/boolbv_byte_extract.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,12 +15,9 @@ Author: Daniel Kroening, [email protected]
#include <util/expr_util.h>
#include <util/pointer_offset_size.h>
#include <util/std_expr.h>
#include <util/throw_with_nested.h>

#include <solvers/lowering/expr_lowering.h>
#include <solvers/lowering/flatten_byte_extract_exceptions.h>

#include "bv_conversion_exceptions.h"
#include "bv_endianness_map.h"

bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
Expand All @@ -45,15 +42,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
// unbounded arrays
if(is_unbounded_array(expr.op().type()))
{
try
{
return convert_bv(lower_byte_extract(expr, ns));
}
catch(const flatten_byte_extract_exceptiont &)
{
util_throw_with_nested(
bitvector_conversion_exceptiont("Can't convert byte_extraction", expr));
}
return convert_bv(lower_byte_extract(expr, ns));
}

const std::size_t width = boolbv_width(expr.type());
Expand Down
13 changes: 1 addition & 12 deletions src/solvers/flattening/boolbv_byte_update.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,9 @@ Author: Daniel Kroening, [email protected]
#include <util/byte_operators.h>
#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/throw_with_nested.h>

#include <solvers/lowering/expr_lowering.h>
#include <solvers/lowering/flatten_byte_extract_exceptions.h>

#include "bv_conversion_exceptions.h"
#include "bv_endianness_map.h"

bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
Expand All @@ -28,15 +25,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
is_unbounded_array(expr.op().type()) ||
is_unbounded_array(expr.value().type()))
{
try
{
return convert_bv(lower_byte_update(expr, ns));
}
catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception)
{
util_throw_with_nested(
bitvector_conversion_exceptiont("Can't convert byte_update", expr));
}
return convert_bv(lower_byte_update(expr, ns));
}

const exprt &op = expr.op();
Expand Down
2 changes: 0 additions & 2 deletions src/solvers/flattening/boolbv_equality.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,6 @@ Author: Daniel Kroening, [email protected]

#include <solvers/lowering/expr_lowering.h>

#include "bv_conversion_exceptions.h"

literalt boolbvt::convert_equality(const equal_exprt &expr)
{
const bool equality_types_match = expr.lhs().type() == expr.rhs().type();
Expand Down
34 changes: 0 additions & 34 deletions src/solvers/flattening/bv_conversion_exceptions.h
View file
Open in desktop

This file was deleted.

2 changes: 0 additions & 2 deletions src/solvers/lowering/byte_operators.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,6 @@ Author: Daniel Kroening, [email protected]
#include <util/simplify_expr.h>
#include <util/string_constant.h>

#include "flatten_byte_extract_exceptions.h"

static exprt bv_to_expr(
const exprt &bitvector_expr,
const typet &target_type,
Expand Down
Loading