Refactor array access into a separate function
This does not save many lines of code, but the way we access arrays using pointer arithmetic can be a bit confusing and it makes sense to abstract it away and keep the documentation of why we do things this way in one place.
This commit is contained in:
parent
c57a1321ed
commit
2088544ca4
|
@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
||||||
|
|
||||||
#include "java_object_factory.h"
|
#include "java_object_factory.h"
|
||||||
|
|
||||||
|
#include <util/array_element_from_pointer.h>
|
||||||
#include <util/expr_initializer.h>
|
#include <util/expr_initializer.h>
|
||||||
#include <util/nondet.h>
|
#include <util/nondet.h>
|
||||||
#include <util/nondet_bool.h>
|
#include <util/nondet_bool.h>
|
||||||
|
@ -1200,10 +1201,10 @@ void java_object_factoryt::array_loop_init_code(
|
||||||
assignments.add(std::move(max_test));
|
assignments.add(std::move(max_test));
|
||||||
}
|
}
|
||||||
|
|
||||||
const dereference_exprt arraycellref{
|
const dereference_exprt element_at_counter =
|
||||||
plus_exprt{array_init_symexpr, counter_expr}};
|
array_element_from_pointer(array_init_symexpr, counter_expr);
|
||||||
|
|
||||||
bool new_item_is_primitive = arraycellref.type().id() != ID_pointer;
|
bool new_item_is_primitive = element_at_counter.type().id() != ID_pointer;
|
||||||
|
|
||||||
// Use a temporary to initialise a new, or update an existing, non-primitive.
|
// Use a temporary to initialise a new, or update an existing, non-primitive.
|
||||||
// This makes it clearer that in a sequence like
|
// This makes it clearer that in a sequence like
|
||||||
|
@ -1213,17 +1214,17 @@ void java_object_factoryt::array_loop_init_code(
|
||||||
exprt init_expr;
|
exprt init_expr;
|
||||||
if(new_item_is_primitive)
|
if(new_item_is_primitive)
|
||||||
{
|
{
|
||||||
init_expr = arraycellref;
|
init_expr = element_at_counter;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
init_expr = allocate_objects.allocate_automatic_local_object(
|
init_expr = allocate_objects.allocate_automatic_local_object(
|
||||||
arraycellref.type(), "new_array_item");
|
element_at_counter.type(), "new_array_item");
|
||||||
|
|
||||||
// If we're updating an existing array item, read the existing object that
|
// If we're updating an existing array item, read the existing object that
|
||||||
// we (may) alter:
|
// we (may) alter:
|
||||||
if(update_in_place != update_in_placet::NO_UPDATE_IN_PLACE)
|
if(update_in_place != update_in_placet::NO_UPDATE_IN_PLACE)
|
||||||
assignments.add(code_assignt(init_expr, arraycellref));
|
assignments.add(code_assignt(init_expr, element_at_counter));
|
||||||
}
|
}
|
||||||
|
|
||||||
// MUST_UPDATE_IN_PLACE only applies to this object.
|
// MUST_UPDATE_IN_PLACE only applies to this object.
|
||||||
|
@ -1249,7 +1250,7 @@ void java_object_factoryt::array_loop_init_code(
|
||||||
{
|
{
|
||||||
// We used a temporary variable to update or initialise an array item;
|
// We used a temporary variable to update or initialise an array item;
|
||||||
// now write it into the array:
|
// now write it into the array:
|
||||||
assignments.add(code_assignt(arraycellref, init_expr));
|
assignments.add(code_assignt(element_at_counter, init_expr));
|
||||||
}
|
}
|
||||||
|
|
||||||
exprt java_one=from_integer(1, java_int_type());
|
exprt java_one=from_integer(1, java_int_type());
|
||||||
|
@ -1389,11 +1390,9 @@ bool java_object_factoryt::gen_nondet_enum_init(
|
||||||
allocate_objects,
|
allocate_objects,
|
||||||
assignments);
|
assignments);
|
||||||
|
|
||||||
// Generate statement using pointer arithmetic to access array element:
|
const dereference_exprt element_at_index =
|
||||||
// expr = (expr.type())*(enum_array_expr + index_expr);
|
array_element_from_pointer(enum_array_expr, index_expr);
|
||||||
plus_exprt plus(enum_array_expr, index_expr);
|
code_assignt enum_assign(expr, typecast_exprt(element_at_index, expr.type()));
|
||||||
const dereference_exprt arraycellref(plus);
|
|
||||||
code_assignt enum_assign(expr, typecast_exprt(arraycellref, expr.type()));
|
|
||||||
assignments.add(enum_assign);
|
assignments.add(enum_assign);
|
||||||
|
|
||||||
return true;
|
return true;
|
||||||
|
|
|
@ -0,0 +1,33 @@
|
||||||
|
/*******************************************************************\
|
||||||
|
|
||||||
|
Module: Element access in a pointer array
|
||||||
|
|
||||||
|
Author: Diffblue Ltd.
|
||||||
|
|
||||||
|
\*******************************************************************/
|
||||||
|
|
||||||
|
#ifndef CPROVER_UTIL_ARRAY_ELEMENT_FROM_POINTER_H
|
||||||
|
#define CPROVER_UTIL_ARRAY_ELEMENT_FROM_POINTER_H
|
||||||
|
|
||||||
|
#include "std_expr.h"
|
||||||
|
|
||||||
|
/// Generate statement using pointer arithmetic to access the element at the
|
||||||
|
/// given index of a pointer array:
|
||||||
|
/// `*(pointer + index)`
|
||||||
|
/// Arrays are sometimes (always in JBMC) represented as a pointer to their
|
||||||
|
/// first element, especially when their length in uncertain, as the length is
|
||||||
|
/// part of any array type. But we know the type of the first element of the
|
||||||
|
/// array, so we work with that instead.
|
||||||
|
/// \param pointer: pointer to the first element of an array
|
||||||
|
/// \param index: index of the element to access
|
||||||
|
/// \return expression representing the (\p index)'th element of the array
|
||||||
|
dereference_exprt
|
||||||
|
array_element_from_pointer(const exprt &pointer, const exprt &index)
|
||||||
|
{
|
||||||
|
PRECONDITION(can_cast_type<pointer_typet>(pointer.type()));
|
||||||
|
PRECONDITION(
|
||||||
|
index.type().id() == ID_signedbv || index.type().id() == ID_unsignedbv);
|
||||||
|
return dereference_exprt{plus_exprt{pointer, index}};
|
||||||
|
}
|
||||||
|
|
||||||
|
#endif // CPROVER_UTIL_ARRAY_ELEMENT_FROM_POINTER_H
|
Loading…
Reference in New Issue