Skip to content

Turn get_may, set_may, etc into irep_ids #4639

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.

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 9, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
28 changes: 13 additions & 15 deletions src/analyses/custom_bitvector_analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -450,10 +450,9 @@ void custom_bitvector_domaint::transform(
const auto &code = instruction.get_other();
const irep_idt &statement = code.get_statement();

if(statement=="set_may" ||
statement=="set_must" ||
statement=="clear_may" ||
statement=="clear_must")
if(
statement == ID_set_may || statement == ID_set_must ||
statement == ID_clear_may || statement == ID_clear_must)
{
DATA_INVARIANT(
code.operands().size() == 2, "set/clear_may/must has two operands");
Expand All @@ -463,13 +462,13 @@ void custom_bitvector_domaint::transform(
// initialize to make Visual Studio happy
modet mode = modet::SET_MUST;

if(statement=="set_must")
if(statement == ID_set_must)
mode=modet::SET_MUST;
else if(statement=="clear_must")
else if(statement == ID_clear_must)
mode=modet::CLEAR_MUST;
else if(statement=="set_may")
else if(statement == ID_set_may)
mode=modet::SET_MAY;
else if(statement=="clear_may")
else if(statement == ID_clear_may)
mode=modet::CLEAR_MAY;
else
UNREACHABLE;
Expand Down Expand Up @@ -687,8 +686,7 @@ void custom_bitvector_domaint::erase_blank_vectors(bitst &bits)

bool custom_bitvector_domaint::has_get_must_or_may(const exprt &src)
{
if(src.id()=="get_must" ||
src.id()=="get_may")
if(src.id() == ID_get_must || src.id() == ID_get_may)
return true;

forall_operands(it, src)
Expand All @@ -702,7 +700,7 @@ exprt custom_bitvector_domaint::eval(
const exprt &src,
custom_bitvector_analysist &custom_bitvector_analysis) const
{
if(src.id()=="get_must" || src.id()=="get_may")
if(src.id() == ID_get_must || src.id() == ID_get_may)
{
if(src.operands().size()==2)
{
Expand All @@ -717,15 +715,15 @@ exprt custom_bitvector_domaint::eval(
if(pointer.is_constant() &&
to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all
{
if(src.id()=="get_may")
if(src.id() == ID_get_may)
{
for(const auto &bit : may_bits)
if(get_bit(bit.second, bit_nr))
return true_exprt();

return false_exprt();
}
else if(src.id()=="get_must")
else if(src.id() == ID_get_must)
{
return false_exprt();
}
Expand All @@ -739,9 +737,9 @@ exprt custom_bitvector_domaint::eval(

bool value=false;

if(src.id()=="get_must")
if(src.id() == ID_get_must)
value=get_bit(v.must_bits, bit_nr);
else if(src.id()=="get_may")
else if(src.id() == ID_get_may)
value=get_bit(v.may_bits, bit_nr);

if(value)
Expand Down
4 changes: 2 additions & 2 deletions src/ansi-c/c_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2074,7 +2074,7 @@ exprt c_typecheck_baset::do_special_functions(
typecheck_function_call_arguments(expr);

binary_predicate_exprt get_must_expr(
expr.arguments()[0], "get_must", expr.arguments()[1]);
expr.arguments()[0], ID_get_must, expr.arguments()[1]);
get_must_expr.add_source_location()=source_location;

return std::move(get_must_expr);
Expand All @@ -2091,7 +2091,7 @@ exprt c_typecheck_baset::do_special_functions(
typecheck_function_call_arguments(expr);

binary_predicate_exprt get_may_expr(
expr.arguments()[0], "get_may", expr.arguments()[1]);
expr.arguments()[0], ID_get_may, expr.arguments()[1]);
get_may_expr.add_source_location()=source_location;

return std::move(get_may_expr);
Expand Down
7 changes: 3 additions & 4 deletions src/ansi-c/expr2c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2911,8 +2911,7 @@ std::string expr2ct::convert_code(
if(statement==ID_array_replace)
return convert_code_array_replace(src, indent);

if(statement=="set_may" ||
statement=="set_must")
if(statement == ID_set_may || statement == ID_set_must)
return indent_str(indent) + convert_function(src, id2string(statement)) +
";";

Expand Down Expand Up @@ -3451,10 +3450,10 @@ std::string expr2ct::convert_with_precedence(
else if(src.id()==ID_pointer_object)
return convert_function(src, "POINTER_OBJECT");

else if(src.id()=="get_must")
else if(src.id() == ID_get_must)
return convert_function(src, CPROVER_PREFIX "get_must");

else if(src.id()=="get_may")
else if(src.id() == ID_get_may)
return convert_function(src, CPROVER_PREFIX "get_may");

else if(src.id()=="object_value")
Expand Down
10 changes: 5 additions & 5 deletions src/goto-analyzer/taint_analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,7 @@ void taint_analysist::instrument(
{
case taint_parse_treet::rulet::SOURCE:
{
codet code_set_may("set_may");
codet code_set_may{ID_set_may};
code_set_may.operands().resize(2);
code_set_may.op0() = where;
code_set_may.op1() =
Expand All @@ -174,10 +174,10 @@ void taint_analysist::instrument(

case taint_parse_treet::rulet::SINK:
{
binary_predicate_exprt get_may(
binary_predicate_exprt get_may{
where,
"get_may",
address_of_exprt(string_constantt(rule.taint)));
ID_get_may,
address_of_exprt(string_constantt(rule.taint))};
goto_programt::targett t =
insert_before.add(goto_programt::make_assertion(
not_exprt(get_may), instruction.source_location));
Expand All @@ -189,7 +189,7 @@ void taint_analysist::instrument(

case taint_parse_treet::rulet::SANITIZER:
{
codet code_clear_may("clear_may");
codet code_clear_may{ID_clear_may};
code_clear_may.operands().resize(2);
code_clear_may.op0() = where;
code_clear_may.op1() =
Expand Down
6 changes: 3 additions & 3 deletions src/goto-instrument/thread_instrumentation.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -41,10 +41,10 @@ void thread_exit_instrumentation(goto_programt &goto_program)
const string_constantt mutex_locked_string("mutex-locked");

// NULL is any
binary_predicate_exprt get_may(
binary_predicate_exprt get_may{
null_pointer_exprt(pointer_type(empty_typet())),
"get_may",
address_of_exprt(mutex_locked_string));
ID_get_may,
address_of_exprt(mutex_locked_string)};

*end = goto_programt::make_assertion(not_exprt(get_may), source_location);

Expand Down
6 changes: 6 additions & 0 deletions src/util/irep_ids.def
Original file line number Diff line number Diff line change
Expand Up @@ -722,6 +722,12 @@ IREP_ID_ONE(to_member)
IREP_ID_ONE(pointer_to_member)
IREP_ID_ONE(tuple)
IREP_ID_ONE(function_body)
IREP_ID_ONE(get_may)
IREP_ID_ONE(set_may)
IREP_ID_ONE(clear_may)
IREP_ID_ONE(get_must)
IREP_ID_ONE(set_must)
IREP_ID_ONE(clear_must)

// Projects depending on this code base that wish to extend the list of
// available ids should provide a file local_irep_ids.def in their source tree
Expand Down