Skip to content

symbol_exprt C++-style API #8824

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

Open
kroening wants to merge 1 commit into
base: develop
Choose a base branch
from
+821 −821
Open

symbol_exprt C++-style API #8824

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
3 changes: 1 addition & 2 deletions jbmc/src/java_bytecode/character_refine_preprocess.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1292,8 +1292,7 @@ codet character_refine_preprocesst::replace_character_call(
{
if(code.function().id()==ID_symbol)
{
const irep_idt &function_id=
to_symbol_expr(code.function()).get_identifier();
const irep_idt &function_id = to_symbol_expr(code.function()).identifier();
auto it=conversion_table.find(function_id);
if(it!=conversion_table.end())
return (it->second)(code);
Expand Down
13 changes: 6 additions & 7 deletions jbmc/src/java_bytecode/ci_lazy_methods.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,11 +69,10 @@ static bool references_class_model(const exprt &expr)

for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)
{
if(can_cast_expr<symbol_exprt>(*it) &&
it->type() == class_type &&
has_suffix(
id2string(to_symbol_expr(*it).get_identifier()),
JAVA_CLASS_MODEL_SUFFIX))
if(
can_cast_expr<symbol_exprt>(*it) && it->type() == class_type &&
has_suffix(
id2string(to_symbol_expr(*it).identifier()), JAVA_CLASS_MODEL_SUFFIX))
{
return true;
}
Expand Down Expand Up @@ -527,8 +526,8 @@ void ci_lazy_methodst::gather_needed_globals(
// on an opaque type (i.e. we don't have the class definition at this point)
// and will be created during the typecheck phase.
// We don't mark it as 'needed' as it doesn't exist yet to keep.
const auto findit=
symbol_table.symbols.find(to_symbol_expr(e).get_identifier());
const auto findit =
symbol_table.symbols.find(to_symbol_expr(e).identifier());
if(findit!=symbol_table.symbols.end() &&
findit->second.is_static_lifetime)
{
Expand Down
22 changes: 11 additions & 11 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,7 +206,7 @@ exprt java_bytecode_convert_methodt::variable(
const variablet &var=
find_variable_for_slot(address, var_list);

if(!var.symbol_expr.get_identifier().empty())
if(!var.symbol_expr.identifier().empty())
return var.symbol_expr;

// an unnamed local variable
Expand Down Expand Up @@ -952,7 +952,7 @@ static void gather_symbol_live_ranges(
const auto &symexpr=to_symbol_expr(e);
auto findit = result.emplace(
std::piecewise_construct,
std::forward_as_tuple(symexpr.get_identifier()),
std::forward_as_tuple(symexpr.identifier()),
std::forward_as_tuple(symexpr, pc, 1));
if(!findit.second)
{
Expand Down Expand Up @@ -1895,9 +1895,9 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
// Add anonymous locals to the symtab:
for(const auto &var : used_local_names)
{
symbolt new_symbol{var.get_identifier(), var.type(), ID_java};
symbolt new_symbol{var.identifier(), var.type(), ID_java};
new_symbol.base_name=var.get(ID_C_base_name);
new_symbol.pretty_name=strip_java_namespace_prefix(var.get_identifier());
new_symbol.pretty_name = strip_java_namespace_prefix(var.identifier());
new_symbol.is_file_local=true;
new_symbol.is_thread_local=true;
new_symbol.is_lvalue=true;
Expand Down Expand Up @@ -1982,11 +1982,11 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)

for(const auto &v : tmp_vars)
vars_to_process.push_back(
&temporary_variable_live_ranges.at(v.get_identifier()));
&temporary_variable_live_ranges.at(v.identifier()));

for(const auto &v : used_local_names)
vars_to_process.push_back(
&temporary_variable_live_ranges.at(v.get_identifier()));
&temporary_variable_live_ranges.at(v.identifier()));

for(const auto vp : vars_to_process)
{
Expand All @@ -2012,7 +2012,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
if(v.is_parameter)
continue;
// Skip anonymous variables:
if(v.symbol_expr.get_identifier().empty())
if(v.symbol_expr.identifier().empty())
continue;
auto &block = get_block_for_pcrange(
root,
Expand Down Expand Up @@ -2674,7 +2674,7 @@ code_blockt java_bytecode_convert_methodt::convert_putstatic(
"stack_static_field",
block,
bytecode_write_typet::STATIC_FIELD,
symbol_expr.get_identifier());
symbol_expr.identifier());
block.add(code_assignt(symbol_expr, op[0]));
return block;
}
Expand Down Expand Up @@ -2834,7 +2834,7 @@ code_blockt java_bytecode_convert_methodt::convert_iinc(
"stack_iinc",
block,
bytecode_write_typet::VARIABLE,
to_symbol_expr(locvar).get_identifier());
to_symbol_expr(locvar).identifier());

const exprt arg1_int_type =
typecast_exprt::conditional_cast(arg1, java_int_type());
Expand Down Expand Up @@ -3039,7 +3039,7 @@ code_blockt java_bytecode_convert_methodt::convert_store(
const source_locationt &location)
{
const exprt var = variable(arg0, statement[0], address);
const irep_idt &var_name = to_symbol_expr(var).get_identifier();
const irep_idt &var_name = to_symbol_expr(var).identifier();

code_blockt block;
block.add_source_location() = location;
Expand Down Expand Up @@ -3390,7 +3390,7 @@ void java_bytecode_convert_methodt::save_stack_entries(
[&identifier](const exprt &expr) {
const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
return !symbol_expr ? tvt::unknown()
: tvt(symbol_expr->get_identifier() == identifier);
: tvt(symbol_expr->identifier() == identifier);
};

// Function that checks whether the expression is a dereference
Expand Down
6 changes: 3 additions & 3 deletions jbmc/src/java_bytecode/java_bytecode_language.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -518,10 +518,10 @@ static symbol_exprt get_or_create_class_literal_symbol(
symbol_exprt symbol_expr(
id2string(class_id) + JAVA_CLASS_MODEL_SUFFIX,
java_lang_Class);
if(!symbol_table.has_symbol(symbol_expr.get_identifier()))
if(!symbol_table.has_symbol(symbol_expr.identifier()))
{
symbolt new_class_symbol{
symbol_expr.get_identifier(), symbol_expr.type(), ID_java};
symbol_expr.identifier(), symbol_expr.type(), ID_java};
INVARIANT(
new_class_symbol.name.starts_with("java::"),
"class identifier should have 'java::' prefix");
Expand Down Expand Up @@ -1241,7 +1241,7 @@ static void notify_static_method_calls(
const symbol_exprt *fn_sym =
expr_try_dynamic_cast<symbol_exprt>(fn_call->function());
if(fn_sym)
needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
needed_lazy_methods->add_needed_method(fn_sym->identifier());
}
else if(
it->id() == ID_side_effect &&
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_bytecode_parser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -636,7 +636,7 @@ void java_bytecode_parsert::get_annotation_value_class_refs(const exprt &value)
{
if(const auto &symbol_expr = expr_try_dynamic_cast<symbol_exprt>(value))
{
const irep_idt &value_id = symbol_expr->get_identifier();
const irep_idt &value_id = symbol_expr->identifier();
get_class_refs_rec(*java_type_from_string(id2string(value_id)));
}
else if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(value))
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ void java_bytecode_typecheckt::typecheck_expr_java_new_array(

void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt &expr)
{
const irep_idt &identifier = expr.get_identifier();
const irep_idt &identifier = expr.identifier();

// the java_bytecode_convert_class and java_bytecode_convert_method made sure
// "identifier" exists in the symbol table
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_trace_validation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ Author: Jeannie Moulton
bool check_symbol_structure(const exprt &expr)
{
const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr);
return symbol && !symbol->get_identifier().empty();
return symbol && !symbol->identifier().empty();
}

/// \return true iff the expression is a symbol or is an expression whose first
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/lift_clinit_calls.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ codet lift_clinit_calls(codet input)
const auto callee = expr_try_dynamic_cast<symbol_exprt>(
to_code_function_call(*code).function()))
{
if(is_clinit_wrapper_function(callee->get_identifier()))
if(is_clinit_wrapper_function(callee->identifier()))
{
clinit_wrappers_called.push_back(*callee);
// Replace call with skip:
Expand Down
6 changes: 3 additions & 3 deletions jbmc/src/java_bytecode/remove_exceptions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,8 +200,8 @@ bool remove_exceptionst::function_or_callees_may_throw(
DATA_INVARIANT(
function_expr.id()==ID_symbol,
"identifier expected to be a symbol");
const irep_idt &function_name=
to_symbol_expr(function_expr).get_identifier();
const irep_idt &function_name =
to_symbol_expr(function_expr).identifier();
if(function_may_throw(function_name))
return true;
}
Expand Down Expand Up @@ -441,7 +441,7 @@ remove_exceptionst::instrument_function_call(

DATA_INVARIANT(
function.id() == ID_symbol, "function call expected to be a symbol");
const irep_idt &callee_id = to_symbol_expr(function).get_identifier();
const irep_idt &callee_id = to_symbol_expr(function).identifier();

if(function_may_throw(callee_id))
{
Expand Down
11 changes: 5 additions & 6 deletions jbmc/src/java_bytecode/replace_java_nondet.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ static nondet_instruction_infot
is_nondet_returning_object(const code_function_callt &function_call)
{
const auto &function_symbol = to_symbol_expr(function_call.function());
const auto function_name = id2string(function_symbol.get_identifier());
const auto function_name = id2string(function_symbol.identifier());
const std::regex reg(
R"(.*org\.cprover\.CProver\.nondet)"
R"((?:Boolean|Byte|Char|Short|Int|Long|Float|Double|With(out)?Null.*))");
Expand Down Expand Up @@ -108,7 +108,7 @@ get_nondet_instruction_info(const goto_programt::const_targett &instr)
static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier)
{
return expr.id() == ID_symbol &&
to_symbol_expr(expr).get_identifier() == identifier;
to_symbol_expr(expr).identifier() == identifier;
}

/// Return whether the expression is a typecast with the specified identifier.
Expand All @@ -129,7 +129,7 @@ static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier)
}
const auto &op_symbol = to_symbol_expr(typecast.op());
// Return whether the typecast has the expected operand
return op_symbol.get_identifier() == identifier;
return op_symbol.identifier() == identifier;
}

/// Return whether the instruction is an assignment, and the rhs is a symbol or
Expand Down Expand Up @@ -214,7 +214,7 @@ static goto_programt::targett check_and_replace_target(
irep_idt return_identifier;
if(remove_returns_not_run)
{
return_identifier = to_symbol_expr(target->call_lhs()).get_identifier();
return_identifier = to_symbol_expr(target->call_lhs()).identifier();
}
else
{
Expand All @@ -236,8 +236,7 @@ static goto_programt::targett check_and_replace_target(
}

// Otherwise it's the temporary variable.
return_identifier =
to_symbol_expr(return_value_assignment).get_identifier();
return_identifier = to_symbol_expr(return_value_assignment).identifier();
}

// Look for the assignment of the temporary return variable into our target
Expand Down
2 changes: 1 addition & 1 deletion jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ static bool is_call_to(
const exprt &callee_expr = inst->call_function();
if(callee_expr.id() != ID_symbol)
return false;
return to_symbol_expr(callee_expr).get_identifier() == callee;
return to_symbol_expr(callee_expr).identifier() == callee;
}

static bool is_assume_false(goto_programt::const_targett inst)
Expand Down
7 changes: 4 additions & 3 deletions jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,10 @@ Author: Diffblue Ltd.
static bool contains_symbol_reference(const exprt &expr, const irep_idt &id)
{
return std::any_of(
expr.depth_begin(), expr.depth_end(), [id](const exprt &e) {
return e.id() == ID_symbol && to_symbol_expr(e).get_identifier() == id;
});
expr.depth_begin(),
expr.depth_end(),
[id](const exprt &e)
{ return e.id() == ID_symbol && to_symbol_expr(e).identifier() == id; });
}

SCENARIO(
Expand Down
6 changes: 3 additions & 3 deletions jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ void validate_lambda_assignment(

const symbol_exprt &rhs_symbol = require_expr::require_symbol(rhs_value.op());

const irep_idt &tmp_object_symbol = rhs_symbol.get_identifier();
const irep_idt &tmp_object_symbol = rhs_symbol.identifier();

const auto tmp_object_assignments =
require_goto_statements::find_pointer_assignments(
Expand Down Expand Up @@ -135,8 +135,8 @@ void validate_lambda_assignment(
if(it->id() == ID_symbol)
{
symbol_exprt &symbol_expr = to_symbol_expr(it.mutate());
const irep_idt simple_id = symbol_expr.get_identifier();
symbol_expr.set_identifier(variable_prefix + id2string(simple_id));
const irep_idt simple_id = symbol_expr.identifier();
symbol_expr.identifier(variable_prefix + id2string(simple_id));
}
}
}
Expand Down
9 changes: 4 additions & 5 deletions jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -320,8 +320,7 @@ SCENARIO(
{
if(
symbol_expr->source_location().get_java_bytecode_index() == "0" &&
symbol_expr->get_identifier() ==
"java::ClassReadingStaticField.x")
symbol_expr->identifier() == "java::ClassReadingStaticField.x")
found = true;
}
});
Expand Down Expand Up @@ -1029,12 +1028,12 @@ TEST_CASE(
// Assert side effects on variables
REQUIRE(variables.size() == 3);
REQUIRE(
variables[0][0].symbol_expr.get_identifier() ==
variables[0][0].symbol_expr.identifier() ==
id2string(method_id) + "::this");
REQUIRE(
variables[1][0].symbol_expr.get_identifier() ==
variables[1][0].symbol_expr.identifier() ==
id2string(method_id) + "::this$0");
REQUIRE(
variables[2][0].symbol_expr.get_identifier() ==
variables[2][0].symbol_expr.identifier() ==
id2string(method_id) + "::other");
}
9 changes: 3 additions & 6 deletions jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,8 +90,7 @@ SCENARIO(
REQUIRE(annotations.size() == 1);
const auto &annotation = annotations.front();
const auto &element_value_pair = annotation.element_value_pairs.front();
const auto &id =
to_symbol_expr(element_value_pair.value).get_identifier();
const auto &id = to_symbol_expr(element_value_pair.value).identifier();
const auto &java_type = java_type_from_string(id2string(id));
const std::string &class_name = id2string(
to_struct_tag_type(to_reference_type(*java_type).base_type())
Expand All @@ -116,8 +115,7 @@ SCENARIO(
REQUIRE(annotations.size() == 1);
const auto &annotation = annotations.front();
const auto &element_value_pair = annotation.element_value_pairs.front();
const auto &id =
to_symbol_expr(element_value_pair.value).get_identifier();
const auto &id = to_symbol_expr(element_value_pair.value).identifier();
const auto &java_type = java_type_from_string(id2string(id));
REQUIRE(*java_type == java_byte_type());
}
Expand All @@ -138,8 +136,7 @@ SCENARIO(
REQUIRE(annotations.size() == 1);
const auto &annotation = annotations.front();
const auto &element_value_pair = annotation.element_value_pairs.front();
const auto &id =
to_symbol_expr(element_value_pair.value).get_identifier();
const auto &id = to_symbol_expr(element_value_pair.value).identifier();
const auto &java_type = java_type_from_string(id2string(id));
REQUIRE(*java_type == java_void_type());
}
Expand Down
2 changes: 1 addition & 1 deletion jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ void validate_nondet_method_removed(
if(function.id() != ID_symbol)
continue;

const irep_idt function_id = to_symbol_expr(function).get_identifier();
const irep_idt function_id = to_symbol_expr(function).identifier();
if(
function_id ==
"java::org.cprover.CProver.nondetWithoutNull:()"
Expand Down
Loading
Loading