Skip to content

use optional for unknown pointer offset sizes #2137

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 1 commit into from
Sep 30, 2018
Merged

use optional for unknown pointer offset sizes #2137

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
106 changes: 68 additions & 38 deletions src/analyses/goto_rw.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,10 +99,14 @@ void rw_range_sett::get_objects_complex_imag(
{
const exprt &op = expr.op();

range_spect sub_size =
to_range_spect(pointer_offset_bits(op.type().subtype(), ns));
assert(sub_size>0);
range_spect offset = range_start == -1 ? 0 : sub_size;
auto subtype_bits = pointer_offset_bits(op.type().subtype(), ns);
CHECK_RETURN(subtype_bits.has_value());

range_spect sub_size = to_range_spect(*subtype_bits);
CHECK_RETURN(sub_size > 0);

range_spect offset=
(range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;

get_objects_rec(mode, op, range_start + offset, size);
}
Expand Down Expand Up @@ -173,8 +177,9 @@ void rw_range_sett::get_objects_shift(
{
const exprt simp_distance=simplify_expr(shift.distance(), ns);

range_spect src_size=
to_range_spect(pointer_offset_bits(shift.op().type(), ns));
auto op_bits = pointer_offset_bits(shift.op().type(), ns);

range_spect src_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;

mp_integer dist;
if(range_start==-1 ||
Expand Down Expand Up @@ -230,15 +235,18 @@ void rw_range_sett::get_objects_member(

const struct_typet &struct_type=to_struct_type(type);

range_spect offset=
to_range_spect(
member_offset_bits(
struct_type,
expr.get_component_name(),
ns));
auto offset_bits =
member_offset_bits(struct_type, expr.get_component_name(), ns);

if(offset!=-1)
offset+=range_start;
range_spect offset;

if(offset_bits.has_value())
{
offset = to_range_spect(*offset_bits);
offset += range_start;
}
else
offset = -1;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: use ? : as above instead of the if ... else

Copy link
Member Author

Choose a reason for hiding this comment

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

Merged with next branch


get_objects_rec(mode, expr.struct_op(), offset, size);
}
Expand All @@ -259,15 +267,17 @@ void rw_range_sett::get_objects_index(
{
const vector_typet &vector_type=to_vector_type(type);

sub_size=
to_range_spect(pointer_offset_bits(vector_type.subtype(), ns));
auto subtype_bits = pointer_offset_bits(vector_type.subtype(), ns);

sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
}
else if(type.id()==ID_array)
{
const array_typet &array_type=to_array_type(type);

sub_size=
to_range_spect(pointer_offset_bits(array_type.subtype(), ns));
auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);

sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
}
else
return;
Expand Down Expand Up @@ -302,10 +312,13 @@ void rw_range_sett::get_objects_array(
const array_typet &array_type=
to_array_type(ns.follow(expr.type()));

range_spect sub_size=
to_range_spect(pointer_offset_bits(array_type.subtype(), ns));
auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);

range_spect sub_size;

if(sub_size==-1)
if(subtype_bits.has_value())
sub_size = to_range_spect(*subtype_bits);
else
{
forall_operands(it, expr)
get_objects_rec(mode, *it, 0, -1);
Expand Down Expand Up @@ -342,17 +355,20 @@ void rw_range_sett::get_objects_struct(
const struct_typet &struct_type=
to_struct_type(ns.follow(expr.type()));

range_spect full_size=
to_range_spect(pointer_offset_bits(struct_type, ns));
auto struct_bits = pointer_offset_bits(struct_type, ns);

range_spect full_size =
struct_bits.has_value() ? to_range_spect(*struct_bits) : -1;

range_spect offset=0;
range_spect full_r_s=range_start==-1 ? 0 : range_start;
range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;

forall_operands(it, expr)
{
range_spect sub_size=
to_range_spect(pointer_offset_bits(it->type(), ns));
auto it_bits = pointer_offset_bits(it->type(), ns);

range_spect sub_size = it_bits.has_value() ? to_range_spect(*it_bits) : -1;

if(offset==-1)
{
Expand Down Expand Up @@ -401,8 +417,9 @@ void rw_range_sett::get_objects_typecast(
{
const exprt &op=tc.op();

range_spect new_size=
to_range_spect(pointer_offset_bits(op.type(), ns));
auto op_bits = pointer_offset_bits(op.type(), ns);

range_spect new_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;

if(range_start==-1)
new_size=-1;
Expand Down Expand Up @@ -537,8 +554,11 @@ void rw_range_sett::get_objects_rec(
{
const symbol_exprt &symbol=to_symbol_expr(expr);
const irep_idt identifier=symbol.get_identifier();
range_spect full_size=
to_range_spect(pointer_offset_bits(symbol.type(), ns));

auto symbol_bits = pointer_offset_bits(symbol.type(), ns);

range_spect full_size =
symbol_bits.has_value() ? to_range_spect(*symbol_bits) : -1;

if(full_size==0 ||
(full_size>0 && range_start>=full_size))
Expand Down Expand Up @@ -584,8 +604,10 @@ void rw_range_sett::get_objects_rec(

void rw_range_sett::get_objects_rec(get_modet mode, const exprt &expr)
{
range_spect size=
to_range_spect(pointer_offset_bits(expr.type(), ns));
auto expr_bits = pointer_offset_bits(expr.type(), ns);

range_spect size = expr_bits.has_value() ? to_range_spect(*expr_bits) : -1;

get_objects_rec(mode, expr, 0, size);
}

Expand Down Expand Up @@ -614,16 +636,24 @@ void rw_range_set_value_sett::get_objects_dereference(
exprt object=deref;
dereference(target, object, ns, value_sets);

range_spect new_size=
to_range_spect(pointer_offset_bits(object.type(), ns));
auto type_bits = pointer_offset_bits(object.type(), ns);

if(range_start==-1 || new_size<=range_start)
new_size=-1;
else
range_spect new_size;

if(type_bits.has_value())
{
new_size-=range_start;
new_size=std::min(size, new_size);
new_size = to_range_spect(*type_bits);

if(range_start == -1 || new_size <= range_start)
new_size = -1;
else
{
new_size -= range_start;
new_size = std::min(size, new_size);
}
}
else
new_size = -1;

// value_set_dereferencet::build_reference_to will turn *p into
// DYNAMIC_OBJECT(p) ? *p : invalid_objectN
Expand Down
8 changes: 5 additions & 3 deletions src/analyses/reaching_definitions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -210,9 +210,11 @@ void rd_range_domaint::transform_function_call(
if(identifier.empty())
continue;

range_spect size=
to_range_spect(pointer_offset_bits(param.type(), ns));
gen(from, identifier, 0, size);
auto param_bits = pointer_offset_bits(param.type(), ns);
if(param_bits.has_value())
gen(from, identifier, 0, to_range_spect(*param_bits));
else
gen(from, identifier, 0, -1);
}
}
else
Expand Down
6 changes: 3 additions & 3 deletions src/ansi-c/expr2c.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3617,9 +3617,9 @@ std::string expr2ct::convert_with_precedence(
else if(src.id()==ID_bswap)
return convert_function(
src,
"__builtin_bswap"+
integer2string(pointer_offset_bits(src.op0().type(), ns)),
precedence=16);
"__builtin_bswap" +
integer2string(*pointer_offset_bits(src.op0().type(), ns)),
precedence = 16);

else if(src.id()==ID_isnormal)
return convert_function(src, "isnormal", precedence=16);
Expand Down
20 changes: 10 additions & 10 deletions src/ansi-c/padding.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ mp_integer alignment(const typet &type, const namespacet &ns)
type.id()==ID_c_bool ||
type.id()==ID_pointer)
{
result=pointer_offset_size(type, ns);
result = *pointer_offset_size(type, ns);
}
else if(type.id()==ID_c_enum)
result=alignment(type.subtype(), ns);
Expand Down Expand Up @@ -229,9 +229,9 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
else
{
// keep track of offset
const mp_integer size = pointer_offset_size(it->type(), ns);
if(size >= 1)
offset += size;
const auto size = pointer_offset_size(it->type(), ns);
if(size.has_value() && *size >= 1)
offset += *size;
}
}
}
Expand Down Expand Up @@ -375,10 +375,10 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
}
}

mp_integer size=pointer_offset_size(it_type, ns);
auto size = pointer_offset_size(it_type, ns);

if(size!=-1)
offset+=size;
if(size.has_value())
offset += *size;
}

// any explicit alignment for the struct?
Expand Down Expand Up @@ -435,9 +435,9 @@ void add_padding(union_typet &type, const namespacet &ns)
// check per component, and ignore those without fixed size
for(const auto &c : type.components())
{
mp_integer s=pointer_offset_bits(c.type(), ns);
if(s>0)
size_bits=std::max(size_bits, s);
auto s = pointer_offset_bits(c.type(), ns);
if(s.has_value())
size_bits = std::max(size_bits, *s);
}

// Is the union packed?
Expand Down
6 changes: 3 additions & 3 deletions src/ansi-c/type2name.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,9 +86,9 @@ static std::string pointer_offset_bits_as_string(
const typet &type,
const namespacet &ns)
{
mp_integer bits = pointer_offset_bits(type, ns);
CHECK_RETURN(bits != -1);
return integer2string(bits);
auto bits = pointer_offset_bits(type, ns);
CHECK_RETURN(bits.has_value());
return integer2string(*bits);
}

static bool parent_is_sym_check=false;
Expand Down
12 changes: 6 additions & 6 deletions src/goto-instrument/alignment_checks.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,12 +51,12 @@ void print_struct_alignment_problems(
{
const typet &it_type = it_next->type();
const namespacet ns(symbol_table);
mp_integer size = pointer_offset_size(it_type, ns);
auto size = pointer_offset_size(it_type, ns);

if(size < 0)
if(!size.has_value())
throw "type of unknown size:\n" + it_type.pretty();

cumulated_length += size;
cumulated_length += *size;
// [it_mem;it_next] cannot be covered by an instruction
if(cumulated_length > config.ansi_c.memory_operand_size)
{
Expand Down Expand Up @@ -92,13 +92,13 @@ void print_struct_alignment_problems(
#if 0
const namespacet ns(symbol_table);
const array_typet array=to_array_type(symbol_pair.second.type);
const mp_integer size=
const auto size=
pointer_offset_size(array.subtype(), ns);

if(size<0)
if(!size.has_value())
throw "type of unknown size:\n"+it_type.pretty();

if(2*integer2long(size)<=config.ansi_c.memory_operand_size)
if(2*integer2long(*size)<=config.ansi_c.memory_operand_size)
{
out << "\nWARNING: "
<< "declaration of an array at "
Expand Down
6 changes: 3 additions & 3 deletions src/goto-instrument/count_eloc.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -191,9 +191,9 @@ void print_global_state_size(const goto_modelt &goto_model)
continue;
}

const mp_integer bits = pointer_offset_bits(symbol.type, ns);
if(bits > 0)
total_size += bits;
const auto bits = pointer_offset_bits(symbol.type, ns);
if(bits.has_value() && bits.value() > 0)
total_size += bits.value();
}

std::cout << "Total size of global objects: " << total_size << " bits\n";
Expand Down
Loading