Skip to content

Move make_allocate_code utility function #4349

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 6 commits into from
Mar 8, 2019
Merged

Move make_allocate_code utility function #4349

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
8681117
Move make_allocate_code to allocate_objectst
antlechner Mar 7, 2019
c44f47b
Make function return type more specific
antlechner Mar 7, 2019
3de7678
Use make_allocate_code in allocate_objectst
antlechner Mar 7, 2019
daec9b4
Move Doxygen to header
antlechner Mar 7, 2019
ed86ec5
Use new side_effect_exprt constructor
antlechner Mar 8, 2019
b2e9778
Tidy up documentation of make_allocate_code
antlechner Mar 8, 2019
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
12 changes: 0 additions & 12 deletions jbmc/src/java_bytecode/java_object_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1194,18 +1194,6 @@ void java_object_factoryt::allocate_nondet_length_array(
assignments.add(assign);
}

/// Create code allocating object of size `size` and assigning it to `lhs`
/// \param lhs : pointer which will be allocated
/// \param size : size of the object
/// \return code allocation object and assigning `lhs`
codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
{
side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location());
alloc.add_to_operands(size);
alloc.add_to_operands(false_exprt());
return code_assignt(lhs, alloc);
}

/// Create code to nondeterministically initialize arrays of primitive type.
/// The code produced is of the form (for an array of type TYPE):
/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Expand Down
2 changes: 0 additions & 2 deletions jbmc/src/java_bytecode/java_object_factory.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,6 +126,4 @@ void gen_nondet_init(
const java_object_factory_parameterst &object_factory_parameters,
update_in_placet update_in_place);

codet make_allocate_code(const symbol_exprt &lhs, const exprt &size);

#endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
1 change: 0 additions & 1 deletion jbmc/src/java_bytecode/java_string_library_preprocess.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ Date: April 2017
#include <util/string_expr.h>

#include "java_types.h"
#include "java_object_factory.h"
#include "java_utils.h"

#include "java_string_library_preprocess.h"
Expand Down
17 changes: 9 additions & 8 deletions src/util/allocate_objects.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -159,12 +159,6 @@ exprt allocate_objectst::allocate_dynamic_object(
auto object_size = size_of_expr(allocate_type, ns);
INVARIANT(object_size.has_value(), "Size of objects should be known");

// malloc expression
side_effect_exprt malloc_expr(
ID_allocate, pointer_type(allocate_type), source_location);
malloc_expr.copy_to_operands(object_size.value());
malloc_expr.copy_to_operands(false_exprt());

// create a symbol for the malloc expression so we can initialize
// without having to do it potentially through a double-deref, which
// breaks the to-SSA phase.
Expand All @@ -178,8 +172,8 @@ exprt allocate_objectst::allocate_dynamic_object(

symbols_created.push_back(&malloc_sym);

code_assignt assign(malloc_sym.symbol_expr(), malloc_expr);
assign.add_source_location() = source_location;
code_assignt assign =
make_allocate_code(malloc_sym.symbol_expr(), object_size.value());
output_code.add(assign);

exprt malloc_symbol_expr = typecast_exprt::conditional_cast(
Expand Down Expand Up @@ -271,3 +265,10 @@ void allocate_objectst::mark_created_symbols_as_input(code_blockt &init_code)
init_code.add(std::move(input_code));
}
}

code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
{
side_effect_exprt alloc{
ID_allocate, {size, false_exprt()}, lhs.type(), lhs.source_location()};
return code_assignt(lhs, alloc);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd do return code_assignt{lhs, std::move(alloc)};

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why? Wouldn't return-value optimisation take care of this?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AFAIK not, because it's a named object. (But also it won't make any difference until #3502 is merged, and even then it will not make a measurable difference.)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see, so the pass-by-value constructor for code_assignt doesn't exist yet but hopefully will in the future, when your PR is merged. In that case I'll leave it as it is for now as it'll be less confusing to make this kind of change in several places at once after your PR got merged.

}
6 changes: 6 additions & 0 deletions src/util/allocate_objects.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,4 +95,10 @@ class allocate_objectst
const irep_idt &basename_prefix);
};

/// Create code allocating an object of size `size` and assigning it to `lhs`
/// \param lhs: pointer which will be allocated
/// \param size: size of the object
/// \return code allocating the object and assigning it to `lhs`
code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size);

#endif // CPROVER_UTIL_ALLOCATE_OBJECTS_H