Skip to content

Missing language modes #2111

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
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
27 changes: 13 additions & 14 deletions src/goto-programs/builtin_functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -468,8 +468,8 @@ void goto_convertt::do_cpp_new(
assert(code_type.parameters().size()==1 ||
code_type.parameters().size()==2);

const symbolt &tmp_symbol=
new_tmp_symbol(return_type, "new", dest, rhs.source_location());
const symbolt &tmp_symbol =
new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);

tmp_symbol_expr=tmp_symbol.symbol_expr();

Expand Down Expand Up @@ -499,8 +499,8 @@ void goto_convertt::do_cpp_new(
assert(code_type.parameters().size()==2 ||
code_type.parameters().size()==3);

const symbolt &tmp_symbol=
new_tmp_symbol(return_type, "new", dest, rhs.source_location());
const symbolt &tmp_symbol =
new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);

tmp_symbol_expr=tmp_symbol.symbol_expr();

Expand Down Expand Up @@ -663,13 +663,10 @@ void goto_convertt::do_java_new_array(
// Must directly assign the new array to a temporary
// because goto-symex will notice `x=side_effect_exprt` but not
// `x=typecast_exprt(side_effect_exprt(...))`
symbol_exprt new_array_data_symbol=
symbol_exprt new_array_data_symbol =
new_tmp_symbol(
data_java_new_expr.type(),
"new_array_data",
dest,
location)
.symbol_expr();
data_java_new_expr.type(), "new_array_data", dest, location, ID_java)
.symbol_expr();
goto_programt::targett t_p2=dest.add_instruction(ASSIGN);
t_p2->code=code_assignt(new_array_data_symbol, data_java_new_expr);
t_p2->source_location=location;
Expand Down Expand Up @@ -707,8 +704,9 @@ void goto_convertt::do_java_new_array(

goto_programt tmp;

symbol_exprt tmp_i=
new_tmp_symbol(length.type(), "index", tmp, location).symbol_expr();
symbol_exprt tmp_i =
new_tmp_symbol(length.type(), "index", tmp, location, ID_java)
.symbol_expr();

code_fort for_loop;

Expand All @@ -730,8 +728,9 @@ void goto_convertt::do_java_new_array(
plus_exprt(data, tmp_i), data.type().subtype());

code_blockt for_body;
symbol_exprt init_sym=
new_tmp_symbol(sub_type, "subarray_init", tmp, location).symbol_expr();
symbol_exprt init_sym =
new_tmp_symbol(sub_type, "subarray_init", tmp, location, ID_java)
.symbol_expr();

code_assignt init_subarray(init_sym, sub_java_new);
code_assignt assign_subarray(
Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/goto_clean_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -237,8 +237,8 @@ void goto_convertt::clean_expr(

if(result_is_used)
{
symbolt &new_symbol=
new_tmp_symbol(expr.type(), "if_expr", dest, source_location);
symbolt &new_symbol = new_tmp_symbol(
expr.type(), "if_expr", dest, source_location, expr.get(ID_mode));

code_assignt assignment_true;
assignment_true.lhs()=new_symbol.symbol_expr();
Expand Down
22 changes: 11 additions & 11 deletions src/goto-programs/goto_convert.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2055,16 +2055,16 @@ symbolt &goto_convertt::new_tmp_symbol(
const typet &type,
const std::string &suffix,
goto_programt &dest,
const source_locationt &source_location)
const source_locationt &source_location,
const irep_idt &mode)
{
symbolt &new_symbol=
get_fresh_aux_symbol(
type,
tmp_symbol_prefix,
"tmp_"+suffix,
source_location,
irep_idt(),
symbol_table);
symbolt &new_symbol = get_fresh_aux_symbol(
type,
tmp_symbol_prefix,
"tmp_" + suffix,
source_location,
mode,
symbol_table);

code_declt decl;
decl.symbol()=new_symbol.symbol_expr();
Expand All @@ -2081,8 +2081,8 @@ void goto_convertt::make_temp_symbol(
{
const source_locationt source_location=expr.find_source_location();

symbolt &new_symbol=
new_tmp_symbol(expr.type(), suffix, dest, source_location);
symbolt &new_symbol = new_tmp_symbol(
expr.type(), suffix, dest, source_location, expr.get(ID_mode));

code_assignt assignment;
assignment.lhs()=new_symbol.symbol_expr();
Expand Down
3 changes: 2 additions & 1 deletion src/goto-programs/goto_convert_class.h
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,8 @@ class goto_convertt:public messaget
const typet &type,
const std::string &suffix,
goto_programt &dest,
const source_locationt &);
const source_locationt &,
const irep_idt &mode);

symbol_exprt make_compound_literal(
const exprt &expr,
Expand Down
14 changes: 8 additions & 6 deletions src/goto-programs/goto_convert_side_effect.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -522,10 +522,8 @@ void goto_convertt::remove_temporary_object(
throw 0;
}

symbolt &new_symbol=
new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location());

new_symbol.mode=expr.get(ID_mode);
symbolt &new_symbol = new_tmp_symbol(
expr.type(), "obj", dest, expr.find_source_location(), expr.get(ID_mode));

if(expr.operands().size()==1)
{
Expand Down Expand Up @@ -599,8 +597,12 @@ void goto_convertt::remove_statement_expression(

source_locationt source_location=last.find_source_location();

symbolt &new_symbol=
new_tmp_symbol(expr.type(), "statement_expression", dest, source_location);
symbolt &new_symbol = new_tmp_symbol(
expr.type(),
"statement_expression",
dest,
source_location,
expr.get(ID_mode));

symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
tmp_symbol_expr.add_source_location()=source_location;
Expand Down
7 changes: 5 additions & 2 deletions src/goto-symex/symex_builtin_functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,9 @@ void goto_symext::symex_allocate(

exprt size=code.op0();
typet object_type=nil_typet();
auto function_symbol = outer_symbol_table.lookup(state.source.pc->function);
INVARIANT(function_symbol, "function associated with instruction not found");
const irep_idt &mode = function_symbol->mode;

// is the type given?
if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty)
Expand Down Expand Up @@ -142,7 +145,7 @@ void goto_symext::symex_allocate(
size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
size_symbol.is_lvalue=true;
size_symbol.type=tmp_size.type();
size_symbol.mode=ID_C;
size_symbol.mode = mode;

state.symbol_table.add(size_symbol);

Expand All @@ -161,7 +164,7 @@ void goto_symext::symex_allocate(
value_symbol.is_lvalue=true;
value_symbol.type=object_type;
value_symbol.type.set("#dynamic", true);
value_symbol.mode=ID_C;
value_symbol.mode = mode;

state.symbol_table.add(value_symbol);

Expand Down
1 change: 1 addition & 0 deletions src/java_bytecode/java_bytecode_convert_class.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -740,6 +740,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
symbol.base_name=symbol_type.get(ID_C_base_name);
symbol.is_type=true;
symbol.type = class_type;
symbol.mode = ID_java;
symbol_table.add(symbol);

// Also provide a clone method:
Expand Down
22 changes: 10 additions & 12 deletions src/java_bytecode/java_bytecode_typecheck_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]

#include "java_bytecode_typecheck.h"

#include <util/invariant.h>
#include <util/std_types.h>

void java_bytecode_typecheckt::typecheck_type(typet &type)
Expand All @@ -19,17 +20,12 @@ void java_bytecode_typecheckt::typecheck_type(typet &type)
{
irep_idt identifier=to_symbol_type(type).get_identifier();

symbol_tablet::symbolst::const_iterator s_it=
symbol_table.symbols.find(identifier);

// must exist already in the symbol table
if(s_it==symbol_table.symbols.end())
{
error() << "failed to find type symbol "<< identifier << eom;
throw 0;
}

assert(s_it->second.is_type);
auto type_symbol = symbol_table.lookup(identifier);
DATA_INVARIANT(
type_symbol, "symbol " + id2string(identifier) + " must exist already");
DATA_INVARIANT(
type_symbol->is_type,
"symbol " + id2string(identifier) + " must be a type");
}
else if(type.id()==ID_pointer)
{
Expand All @@ -55,7 +51,9 @@ void java_bytecode_typecheckt::typecheck_type(typet &type)

void java_bytecode_typecheckt::typecheck_type_symbol(symbolt &symbol)
{
assert(symbol.is_type);
DATA_INVARIANT(
symbol.is_type, "symbol " + id2string(symbol.name) + " must be a type");

symbol.mode = ID_java;
typecheck_type(symbol.type);
}
1 change: 1 addition & 0 deletions src/java_bytecode/java_string_library_preprocess.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -247,6 +247,7 @@ void java_string_library_preprocesst::add_string_type(
string_symbol->pretty_name=id2string(class_name);
string_symbol->type=string_type;
string_symbol->is_type=true;
string_symbol->mode = ID_java;
}

/// add a symbol in the table with static lifetime and name containing
Expand Down
10 changes: 8 additions & 2 deletions unit/testing-utils/load_java_class.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@

#include <goto-programs/lazy_goto_model.h>

#include <langapi/mode.h>

#include <java_bytecode/java_bytecode_language.h>
#include <util/file_util.h>

Expand All @@ -37,11 +39,13 @@ symbol_tablet load_java_class_lazy(
free_form_cmdlinet lazy_command_line;
lazy_command_line.add_flag("lazy-methods");

register_language(new_java_bytecode_language);

return load_java_class(
java_class_name,
class_path,
main,
new_java_bytecode_language(),
get_language_from_mode(ID_java),
lazy_command_line);
}

Expand All @@ -59,8 +63,10 @@ symbol_tablet load_java_class(
const std::string &class_path,
const std::string &main)
{
register_language(new_java_bytecode_language);

return load_java_class(
java_class_name, class_path, main, new_java_bytecode_language());
java_class_name, class_path, main, get_language_from_mode(ID_java));
}

/// Go through the process of loading, type-checking and finalising loading a
Expand Down