Skip to content

Commit

Permalink
Use mp_integer more extensively in interpreter
Browse files Browse the repository at this point in the history
  • Loading branch information
@reuk
reuk committed Sep 5, 2017
1 parent e578136 commit b860c26
Show file tree
Hide file tree
Showing 4 changed files with 46 additions and 44 deletions.
40 changes: 20 additions & 20 deletions src/goto-programs/interpreter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -393,7 +393,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());
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 @@ -420,7 +420,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 @@ -434,7 +434,7 @@ irep_idt interpretert::get_component_id(
{
if(offset<=0)
return it->id();
size_t size=get_size(it->type());
auto size=get_size(it->type());
offset-=size;
}
return object;
Expand All @@ -453,7 +453,7 @@ typet interpretert::get_type(const irep_idt &id) const
/// type
exprt interpretert::get_value(
const typet &type,
std::size_t offset,
uint64_t offset,
bool use_non_det)
{
const typet real_type=ns.follow(type);
Expand All @@ -468,7 +468,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());
auto size=get_size(it->type());
const exprt operand=get_value(it->type(), offset);
offset+=size;
result.copy_to_operands(operand);
Expand All @@ -480,7 +480,7 @@ 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());
auto subtype_size=get_size(type.subtype());
std::size_t count;
if(size_expr.id()!=ID_constant)
{
Expand Down Expand Up @@ -518,7 +518,7 @@ exprt interpretert::get_value(
exprt interpretert::get_value(
const typet &type,
mp_vectort &rhs,
std::size_t offset)
uint64_t offset)
{
const typet real_type=ns.follow(type);
PRECONDITION(!rhs.empty());
Expand All @@ -533,7 +533,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());
auto size=get_size(expr.type());
const exprt operand=get_value(expr.type(), rhs, offset);
offset+=size;
result.copy_to_operands(operand);
Expand All @@ -546,7 +546,7 @@ 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());
auto subtype_size=get_size(type.subtype());
unsigned count;
if(unbounded_size(type))
{
Expand Down Expand Up @@ -606,7 +606,7 @@ exprt interpretert::get_value(
// We want the symbol pointed to
std::size_t address=integer2size_t(rhs[offset]);
irep_idt identifier=address_to_identifier(address);
size_t offset=address_to_offset(address);
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 Down Expand Up @@ -652,7 +652,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());
auto size=get_size(code_assign.lhs().type());

if(size!=rhs.size())
error() << "!! failed to obtain rhs ("
Expand Down Expand Up @@ -681,7 +681,7 @@ void interpretert::execute_assign()
if(side_effect.get_statement()==ID_nondet)
{
unsigned address=integer2unsigned(evaluate_address(code_assign.lhs()));
size_t size=get_size(code_assign.lhs().type());
auto size=get_size(code_assign.lhs().type());
for(size_t i=0; i<size; i++)
{
memory[address+i].initialized=
Expand Down Expand Up @@ -863,7 +863,7 @@ void interpretert::build_memory_map()

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

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

if(size!=0)
{
std::size_t address=memory.size();
auto address=memory.size();
memory.resize(address+size);
memory_map[symbol.name]=address;
inverse_memory_map[address]=symbol.name;
Expand Down Expand Up @@ -916,13 +916,13 @@ mp_integer interpretert::build_memory_map(
const typet &type)
{
typet alloc_type=concretize_type(type);
size_t size=get_size(alloc_type);
auto size=get_size(alloc_type);
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 @@ -934,7 +934,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 @@ -976,7 +976,7 @@ uint64_t interpretert::get_size(const typet &type)
const struct_typet::componentst &components=
to_struct_type(type).components();

unsigned sum=0;
uint64_t sum=0;

for(const auto &comp : components)
{
Expand Down Expand Up @@ -1068,7 +1068,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
28 changes: 14 additions & 14 deletions src/goto-programs/interpreter_class.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,13 +103,13 @@ class interpretert:public messaget

const goto_functionst &goto_functions;

typedef std::unordered_map<irep_idt, std::size_t, irep_id_hash> memory_mapt;
typedef std::map<std::size_t, irep_idt> inverse_memory_mapt;
typedef std::unordered_map<irep_idt, mp_integer, irep_id_hash> memory_mapt;
typedef std::map<mp_integer, irep_idt> inverse_memory_mapt;
memory_mapt memory_map;
inverse_memory_mapt inverse_memory_map;

const inverse_memory_mapt::value_type &address_to_object_record(
std::size_t address) const
const mp_integer &address) const
{
auto lower_bound=inverse_memory_map.lower_bound(address);
if(lower_bound->first!=address)
Expand All @@ -120,34 +120,34 @@ class interpretert:public messaget
return *lower_bound;
}

irep_idt address_to_identifier(std::size_t address) const
irep_idt address_to_identifier(const mp_integer &address) const
{
return address_to_object_record(address).second;
}

std::size_t address_to_offset(std::size_t address) const
mp_integer address_to_offset(const mp_integer &address) const
{
return address-(address_to_object_record(address).first);
}

std::size_t base_address_to_alloc_size(std::size_t address) const
mp_integer base_address_to_alloc_size(const mp_integer &address) const
{
PRECONDITION(address_to_offset(address)==0);
auto upper_bound=inverse_memory_map.upper_bound(address);
std::size_t next_alloc_address=
mp_integer next_alloc_address=
upper_bound==inverse_memory_map.end() ?
memory.size() :
upper_bound->first;
return next_alloc_address-address;
}

std::size_t base_address_to_actual_size(std::size_t address) const
uint64_t base_address_to_actual_size(const mp_integer &address) const
{
auto memory_iter=memory.find(address);
if(memory_iter==memory.end())
return 0;
std::size_t ret=0;
std::size_t alloc_size=base_address_to_alloc_size(address);
mp_integer alloc_size=base_address_to_alloc_size(address);
while(memory_iter!=memory.end() && memory_iter->first<(address+alloc_size))
{
++ret;
Expand Down Expand Up @@ -186,7 +186,7 @@ class interpretert:public messaget
// properties need to be mutable to avoid making all calls nonconst
mutable memoryt memory;

std::size_t stack_pointer;
mp_integer stack_pointer;

void build_memory_map();
void build_memory_map(const symbolt &symbol);
Expand All @@ -195,13 +195,13 @@ class interpretert:public messaget
bool unbounded_size(const typet &);
uint64_t get_size(const typet &type);

irep_idt get_component_id(const irep_idt &object, unsigned offset);
irep_idt get_component_id(const irep_idt &object, mp_integer offset);
typet get_type(const irep_idt &id) const;
exprt get_value(
const typet &type,
std::size_t offset=0,
uint64_t offset=0,
bool use_non_det=false);
exprt get_value(const typet &type, mp_vectort &rhs, std::size_t offset=0);
exprt get_value(const typet &type, mp_vectort &rhs, uint64_t offset=0);
exprt get_value(const irep_idt &id);

void step();
Expand Down Expand Up @@ -240,7 +240,7 @@ class interpretert:public messaget
goto_functionst::function_mapt::const_iterator return_function;
mp_integer return_value_address;
memory_mapt local_map;
unsigned old_stack_pointer;
mp_integer old_stack_pointer;
};

typedef std::stack<stack_framet> call_stackt;
Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/interpreter_evaluate.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,10 +52,10 @@ void interpretert::read_unbounded(
{
// copy memory region
std::size_t address_val=integer2size_t(address);
const std::size_t offset=address_to_offset(address_val);
const auto offset=address_to_offset(address_val);
const std::size_t alloc_size=
base_address_to_actual_size(address_val-offset);
const std::size_t to_read=alloc_size-offset;
const auto to_read=alloc_size-offset;
for(size_t i=0; i<to_read; i++)
{
mp_integer value;
Expand Down
18 changes: 10 additions & 8 deletions src/util/sparse_vector.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,42 +13,44 @@ Author: Romain Brenguier
#define CPROVER_UTIL_SPARSE_VECTOR_H

#include "invariant.h"
#include "mp_arith.h"

#include <cstdint>
#include <map>

template<class T> class sparse_vectort
{
protected:
typedef std::map<uint64_t, T> underlyingt;
typedef std::map<mp_integer, T> underlyingt;
typedef typename underlyingt::key_type key_type;
underlyingt underlying;
uint64_t _size;
mp_integer _size;

public:
sparse_vectort() :
_size(0) {}

const T &operator[](uint64_t idx) const
const T &operator[](const key_type &idx) const
{
INVARIANT(idx<_size, "index out of range");
return underlying[idx];
}

T &operator[](uint64_t idx)
T &operator[](const key_type &idx)
{
INVARIANT(idx<_size, "index out of range");
return underlying[idx];
}

uint64_t size() const
mp_integer size() const
{
return _size;
}

void resize(uint64_t new_size)
void resize(mp_integer new_size)
{
INVARIANT(new_size>=_size, "sparse vector can't be shrunk (yet)");
_size=new_size;
_size=std::move(new_size);
}

typedef typename underlyingt::iterator iteratort;
Expand All @@ -60,7 +62,7 @@ template<class T> class sparse_vectort
iteratort end() { return underlying.end(); }
const_iteratort end() const { return underlying.end(); }

const_iteratort find(uint64_t idx) { return underlying.find(idx); }
const_iteratort find(const mp_integer &idx) { return underlying.find(idx); }
};

#endif // CPROVER_UTIL_SPARSE_VECTOR_H

0 comments on commit b860c26

Please sign in to comment.