Skip to content

Avoid integer truncation #1330

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

Closed
wants to merge 3 commits into from
Closed

Avoid integer truncation #1330

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
e578136
Avoid integer truncation
reuk Sep 2, 2017
b860c26
Use mp_integer more extensively in interpreter
reuk Sep 5, 2017
661e095
Stop using unsigned and uint64_t in interpreter
reuk Sep 5, 2017
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
102 changes: 52 additions & 50 deletions src/goto-programs/interpreter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,13 @@ Author: Daniel Kroening, [email protected]
#include "interpreter.h"

#include <cctype>
#include <cstdint>
#include <cstdio>
#include <iostream>
#include <fstream>
#include <algorithm>
#include <string.h>
#include <type_traits>

#include <util/invariant.h>
#include <util/std_types.h>
Expand Down Expand Up @@ -392,7 +394,7 @@ void interpretert::execute_other()
mp_vectort tmp, rhs;
evaluate(pc->code.op1(), tmp);
mp_integer address=evaluate_address(pc->code.op0());
size_t size=get_size(pc->code.op0().type());
const auto size=get_size(pc->code.op0().type());
while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
if(size!=rhs.size())
error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
Expand All @@ -419,7 +421,7 @@ void interpretert::execute_decl()
/// \par parameters: an object and a memory offset
irep_idt interpretert::get_component_id(
const irep_idt &object,
unsigned offset)
mp_integer offset)
{
const symbolt &symbol=ns.lookup(object);
const typet real_type=ns.follow(symbol.type);
Expand All @@ -433,7 +435,7 @@ irep_idt interpretert::get_component_id(
{
if(offset<=0)
return it->id();
size_t size=get_size(it->type());
const auto size=get_size(it->type());
offset-=size;
}
return object;
Expand All @@ -452,7 +454,7 @@ typet interpretert::get_type(const irep_idt &id) const
/// type
exprt interpretert::get_value(
const typet &type,
std::size_t offset,
mp_integer offset,
bool use_non_det)
{
const typet real_type=ns.follow(type);
Expand All @@ -467,7 +469,7 @@ exprt interpretert::get_value(
for(struct_typet::componentst::const_iterator it=components.begin();
it!=components.end(); it++)
{
size_t size=get_size(it->type());
const auto size=get_size(it->type());
const exprt operand=get_value(it->type(), offset);
offset+=size;
result.copy_to_operands(operand);
Expand All @@ -479,8 +481,8 @@ exprt interpretert::get_value(
// Get size of array
exprt result=array_exprt(to_array_type(real_type));
const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
size_t subtype_size=get_size(type.subtype());
std::size_t count;
const auto subtype_size=get_size(type.subtype());
mp_integer count=0;
if(size_expr.id()!=ID_constant)
{
count=base_address_to_actual_size(offset)/subtype_size;
Expand All @@ -489,12 +491,12 @@ exprt interpretert::get_value(
{
mp_integer mp_count;
to_integer(size_expr, mp_count);
count=integer2size_t(mp_count);
count=mp_count;
}

// Retrieve the value for each member in the array
result.reserve_operands(count);
for(unsigned i=0; i<count; i++)
result.reserve_operands(integer2size_t(count));
for(decltype(count) i=0; i<count; ++i)
{
const exprt operand=get_value(
type.subtype(),
Expand All @@ -517,7 +519,7 @@ exprt interpretert::get_value(
exprt interpretert::get_value(
const typet &type,
mp_vectort &rhs,
std::size_t offset)
mp_integer offset)
{
const typet real_type=ns.follow(type);
PRECONDITION(!rhs.empty());
Expand All @@ -532,7 +534,7 @@ exprt interpretert::get_value(
result.reserve_operands(components.size());
for(const struct_union_typet::componentt &expr : components)
{
size_t size=get_size(expr.type());
const auto size=get_size(expr.type());
const exprt operand=get_value(expr.type(), rhs, offset);
offset+=size;
result.copy_to_operands(operand);
Expand All @@ -545,8 +547,8 @@ exprt interpretert::get_value(
const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));

// Get size of array
size_t subtype_size=get_size(type.subtype());
unsigned count;
const auto subtype_size=get_size(type.subtype());
mp_integer count;
if(unbounded_size(type))
{
count=base_address_to_actual_size(offset)/subtype_size;
Expand All @@ -555,12 +557,12 @@ exprt interpretert::get_value(
{
mp_integer mp_count;
to_integer(size_expr, mp_count);
count=integer2unsigned(mp_count);
count=mp_count;
}

// Retrieve the value for each member in the array
result.reserve_operands(count);
for(unsigned i=0; i<count; i++)
result.reserve_operands(integer2size_t(count));
for(std::remove_const<decltype(count)>::type i=0; i<count; ++i)
{
const exprt operand=get_value(type.subtype(), rhs,
offset+i*subtype_size);
Expand All @@ -571,41 +573,41 @@ exprt interpretert::get_value(
else if(real_type.id()==ID_floatbv)
{
ieee_floatt f(to_floatbv_type(type));
f.unpack(rhs[offset]);
f.unpack(rhs[integer2size_t(offset)]);
return f.to_expr();
}
else if(real_type.id()==ID_fixedbv)
{
fixedbvt f;
f.from_integer(rhs[offset]);
f.from_integer(rhs[integer2size_t(offset)]);
return f.to_expr();
}
else if(real_type.id()==ID_bool)
{
if(rhs[offset]!=0)
if(rhs[integer2size_t(offset)]!=0)
return true_exprt();
else
false_exprt();
}
else if(real_type.id()==ID_c_bool)
{
return from_integer(rhs[offset]!=0?1:0, type);
return from_integer(rhs[integer2size_t(offset)]!=0?1:0, type);
}
else if((real_type.id()==ID_pointer) || (real_type.id()==ID_address_of))
{
if(rhs[offset]==0)
if(rhs[integer2size_t(offset)]==0)
{
// NULL pointer
constant_exprt result(type);
result.set_value(ID_NULL);
return result;
}
if(rhs[offset]<memory.size())
if(rhs[integer2size_t(offset)]<memory.size())
{
// We want the symbol pointed to
std::size_t address=integer2size_t(rhs[offset]);
const auto address=rhs[integer2size_t(offset)];
irep_idt identifier=address_to_identifier(address);
size_t offset=address_to_offset(address);
const auto offset=address_to_offset(address);
const typet type=get_type(identifier);
exprt symbol_expr(ID_symbol, type);
symbol_expr.set(ID_identifier, identifier);
Expand All @@ -624,19 +626,19 @@ exprt interpretert::get_value(
return index_expr;
}

error() << "interpreter: invalid pointer " << rhs[offset]
error() << "interpreter: invalid pointer " << rhs[integer2size_t(offset)]
<< " > object count " << memory.size() << eom;
throw "interpreter: reading from invalid pointer";
}
else if(real_type.id()==ID_string)
{
// Strings are currently encoded by their irep_idt ID.
return constant_exprt(
irep_idt::make_from_table_index(rhs[offset].to_long()),
irep_idt::make_from_table_index(rhs[integer2size_t(offset)].to_long()),
type);
}
// Retrieve value of basic data type
return from_integer(rhs[offset], type);
return from_integer(rhs[integer2size_t(offset)], type);
}

/// executes the assign statement at the current pc value
Expand All @@ -651,7 +653,7 @@ void interpretert::execute_assign()
if(!rhs.empty())
{
mp_integer address=evaluate_address(code_assign.lhs());
size_t size=get_size(code_assign.lhs().type());
const auto size=get_size(code_assign.lhs().type());

if(size!=rhs.size())
error() << "!! failed to obtain rhs ("
Expand Down Expand Up @@ -679,9 +681,9 @@ void interpretert::execute_assign()
side_effect_exprt side_effect=to_side_effect_expr(code_assign.rhs());
if(side_effect.get_statement()==ID_nondet)
{
unsigned address=integer2unsigned(evaluate_address(code_assign.lhs()));
size_t size=get_size(code_assign.lhs().type());
for(size_t i=0; i<size; i++)
const auto address=evaluate_address(code_assign.lhs());
const auto size=get_size(code_assign.lhs().type());
for(std::remove_const<decltype(size)>::type i=0; i<size; ++i)
{
memory[address+i].initialized=
memory_cellt::initializedt::READ_BEFORE_WRITTEN;
Expand All @@ -699,7 +701,7 @@ void interpretert::assign(
{
if((address+i)<memory.size())
{
std::size_t address_val=integer2size_t(address+i);
const auto address_val=address+i;
memory_cellt &cell=memory[address_val];
if(show)
{
Expand Down Expand Up @@ -749,7 +751,7 @@ void interpretert::execute_function_call()
// Retrieve the empty last trace step struct we pushed for this step
// of the interpreter run to fill it with the corresponding data
goto_trace_stept &trace_step=steps.get_last_step();
std::size_t address=integer2size_t(a);
const auto address=a;
#if 0
const memory_cellt &cell=memory[address];
#endif
Expand Down Expand Up @@ -798,7 +800,7 @@ void interpretert::execute_function_call()
for(const auto &id : locals)
{
const symbolt &symbol=ns.lookup(id);
frame.local_map[id]=integer2unsigned(build_memory_map(id, symbol.type));
frame.local_map[id]=build_memory_map(id, symbol.type);
}

// assign the arguments
Expand Down Expand Up @@ -862,7 +864,7 @@ void interpretert::build_memory_map()

void interpretert::build_memory_map(const symbolt &symbol)
{
size_t size=0;
mp_integer size=0;

if(symbol.type.id()==ID_code)
{
Expand All @@ -875,7 +877,7 @@ void interpretert::build_memory_map(const symbolt &symbol)

if(size!=0)
{
std::size_t address=memory.size();
const auto address=memory.size();
memory.resize(address+size);
memory_map[symbol.name]=address;
inverse_memory_map[address]=symbol.name;
Expand Down Expand Up @@ -915,13 +917,13 @@ mp_integer interpretert::build_memory_map(
const typet &type)
{
typet alloc_type=concretize_type(type);
size_t size=get_size(alloc_type);
auto it=dynamic_types.find(id);
auto size=get_size(alloc_type);
const auto it=dynamic_types.find(id);

if(it!=dynamic_types.end())
{
std::size_t address=memory_map[id];
std::size_t current_size=base_address_to_alloc_size(address);
const auto address=memory_map[id];
const auto current_size=base_address_to_alloc_size(address);
// current size <= size already recorded
if(size<=current_size)
return memory_map[id];
Expand All @@ -933,7 +935,7 @@ mp_integer interpretert::build_memory_map(
if(size==0)
size=1; // This is a hack to create existence

std::size_t address=memory.size();
const auto address=memory.size();
memory.resize(address+size);
memory_map[id]=address;
inverse_memory_map[address]=id;
Expand Down Expand Up @@ -965,7 +967,7 @@ bool interpretert::unbounded_size(const typet &type)
/// get allocated 2^32 address space each (of a 2^64 sized space).
/// \param type: a structured type
/// \return Size of the given type
size_t interpretert::get_size(const typet &type)
mp_integer interpretert::get_size(const typet &type)
{
if(unbounded_size(type))
return 2ULL << 32ULL;
Expand All @@ -975,7 +977,7 @@ size_t interpretert::get_size(const typet &type)
const struct_typet::componentst &components=
to_struct_type(type).components();

unsigned sum=0;
mp_integer sum=0;

for(const auto &comp : components)
{
Expand All @@ -992,7 +994,7 @@ size_t interpretert::get_size(const typet &type)
const union_typet::componentst &components=
to_union_type(type).components();

size_t max_size=0;
mp_integer max_size=0;

for(const auto &comp : components)
{
Expand All @@ -1008,7 +1010,7 @@ size_t interpretert::get_size(const typet &type)
{
const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));

size_t subtype_size=get_size(type.subtype());
const auto subtype_size=get_size(type.subtype());

mp_vectort i;
evaluate(size_expr, i);
Expand All @@ -1020,7 +1022,7 @@ size_t interpretert::get_size(const typet &type)
mp_integer size_mp;
bool ret=to_integer(size_const, size_mp);
CHECK_RETURN(!ret);
return subtype_size*integer2unsigned(size_mp);
return subtype_size*size_mp;
}
return subtype_size;
}
Expand All @@ -1036,7 +1038,7 @@ exprt interpretert::get_value(const irep_idt &id)
// The dynamic type and the static symbol type may differ for VLAs,
// where the symbol carries a size expression and the dynamic type
// registry contains its actual length.
auto findit=dynamic_types.find(id);
const auto findit=dynamic_types.find(id);
typet get_type;
if(findit!=dynamic_types.end())
get_type=findit->second;
Expand All @@ -1046,7 +1048,7 @@ exprt interpretert::get_value(const irep_idt &id)
symbol_exprt symbol_expr(id, get_type);
mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);

return get_value(get_type, integer2size_t(whole_lhs_object_address));
return get_value(get_type, whole_lhs_object_address);
}

void interpreter(
Expand All @@ -1067,7 +1069,7 @@ void interpretert::print_memory(bool input_flags)
{
for(const auto &cell_address : memory)
{
std::size_t i=cell_address.first;
const auto i=cell_address.first;
const memory_cellt &cell=cell_address.second;
const auto identifier=address_to_identifier(i);
const auto offset=address_to_offset(i);
Expand Down
Loading