Skip to content

Replace 3-valued char by enum #1289

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 2 commits into from
Sep 3, 2017
Merged

Replace 3-valued char by enum #1289

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4466408
Replace 3-valued char by enum
tautschnig Aug 23, 2017
48845af
Interpreter: constify mp_integer typed address parameters
tautschnig Aug 23, 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
13 changes: 8 additions & 5 deletions src/goto-programs/interpreter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -503,7 +503,9 @@ exprt interpretert::get_value(
}
return result;
}
if(use_non_det && (memory[offset].initialized>=0))
if(use_non_det &&
memory[offset].initialized!=
memory_cellt::initializedt::WRITTEN_BEFORE_READ)
return side_effect_expr_nondett(type);
mp_vectort rhs;
rhs.push_back(memory[offset].value);
Expand Down Expand Up @@ -681,15 +683,16 @@ void interpretert::execute_assign()
size_t size=get_size(code_assign.lhs().type());
for(size_t i=0; i<size; i++)
{
memory[address+i].initialized=-1;
memory[address+i].initialized=
memory_cellt::initializedt::READ_BEFORE_WRITTEN;
}
}
}
}

/// sets the memory at address with the given rhs value (up to sizeof(rhs))
void interpretert::assign(
mp_integer address,
const mp_integer &address,
const mp_vectort &rhs)
{
for(size_t i=0; i<rhs.size(); i++)
Expand All @@ -706,8 +709,8 @@ void interpretert::assign(
<< "\n" << eom;
}
cell.value=rhs[i];
if(cell.initialized==0)
cell.initialized=1;
if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
cell.initialized=memory_cellt::initializedt::WRITTEN_BEFORE_READ;
}
}
}
Expand Down
22 changes: 14 additions & 8 deletions src/goto-programs/interpreter_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,12 +161,18 @@ class interpretert:public messaget
public:
memory_cellt() :
value(0),
initialized(0)
initialized(initializedt::UNKNOWN)
{}
mp_integer value;
// Initialized is annotated even during reads
enum class initializedt
{
UNKNOWN,
WRITTEN_BEFORE_READ,
READ_BEFORE_WRITTEN
};
// Set to 1 when written-before-read, -1 when read-before-written
mutable char initialized;
mutable initializedt initialized;
};

typedef sparse_vectort<memory_cellt> memoryt;
Expand Down Expand Up @@ -210,19 +216,19 @@ class interpretert:public messaget
void clear_input_flags();

void allocate(
mp_integer address,
const mp_integer &address,
size_t size);

void assign(
mp_integer address,
const mp_integer &address,
const mp_vectort &rhs);

void read(
mp_integer address,
const mp_integer &address,
mp_vectort &dest) const;

void read_unbounded(
mp_integer address,
const mp_integer &address,
mp_vectort &dest) const;

virtual void command();
Expand Down Expand Up @@ -273,12 +279,12 @@ class interpretert:public messaget

bool byte_offset_to_memory_offset(
const typet &source_type,
mp_integer byte_offset,
const mp_integer &byte_offset,
mp_integer &result);

bool memory_offset_to_byte_offset(
const typet &source_type,
mp_integer cell_offset,
const mp_integer &cell_offset,
mp_integer &result);

void evaluate(
Expand Down
35 changes: 19 additions & 16 deletions src/goto-programs/interpreter_evaluate.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
/// reads a memory address and loads it into the dest variable marks cell as
/// read before written if cell has never been written
void interpretert::read(
mp_integer address,
const mp_integer &address,
mp_vectort &dest) const
{
// copy memory region
Expand All @@ -36,8 +36,8 @@ void interpretert::read(
{
const memory_cellt &cell=memory[integer2size_t(address+i)];
value=cell.value;
if(cell.initialized==0)
cell.initialized=-1;
if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
cell.initialized=memory_cellt::initializedt::READ_BEFORE_WRITTEN;
}
else
value=0;
Expand All @@ -47,7 +47,7 @@ void interpretert::read(
}

void interpretert::read_unbounded(
mp_integer address,
const mp_integer &address,
mp_vectort &dest) const
{
// copy memory region
Expand All @@ -64,8 +64,8 @@ void interpretert::read_unbounded(
{
const memory_cellt &cell=memory[integer2size_t(address+i)];
value=cell.value;
if(cell.initialized==0)
cell.initialized=-1;
if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
cell.initialized=memory_cellt::initializedt::READ_BEFORE_WRITTEN;
}
else
value=0;
Expand All @@ -76,7 +76,7 @@ void interpretert::read_unbounded(

/// reserves memory block of size at address
void interpretert::allocate(
mp_integer address,
const mp_integer &address,
size_t size)
{
// clear memory region
Expand All @@ -86,7 +86,7 @@ void interpretert::allocate(
{
memory_cellt &cell=memory[integer2size_t(address+i)];
cell.value=0;
cell.initialized=0;
cell.initialized=memory_cellt::initializedt::UNKNOWN;
}
}
}
Expand All @@ -96,8 +96,9 @@ void interpretert::clear_input_flags()
{
for(auto &cell : memory)
{
if(cell.second.initialized>0)
cell.second.initialized=0;
if(cell.second.initialized==
memory_cellt::initializedt::WRITTEN_BEFORE_READ)
cell.second.initialized=memory_cellt::initializedt::UNKNOWN;
}
}

Expand Down Expand Up @@ -147,7 +148,7 @@ bool interpretert::count_type_leaves(const typet &ty, mp_integer &result)
/// \return Offset into a vector of interpreter values; returns true on error
bool interpretert::byte_offset_to_memory_offset(
const typet &source_type,
mp_integer offset,
const mp_integer &offset,
mp_integer &result)
{
if(source_type.id()==ID_struct)
Expand Down Expand Up @@ -227,7 +228,7 @@ bool interpretert::byte_offset_to_memory_offset(
/// \return The corresponding byte offset. Returns true on error
bool interpretert::memory_offset_to_byte_offset(
const typet &source_type,
mp_integer cell_offset,
const mp_integer &full_cell_offset,
mp_integer &result)
{
if(source_type.id()==ID_struct)
Expand All @@ -236,6 +237,7 @@ bool interpretert::memory_offset_to_byte_offset(
const struct_typet::componentst &components=st.components();
member_offset_iterator offsets(st, ns);
mp_integer previous_member_sizes;
mp_integer cell_offset=full_cell_offset;
for(; offsets->first<components.size() && offsets->second!=-1; ++offsets)
{
const auto &component_type=components[offsets->first].type();
Expand Down Expand Up @@ -277,13 +279,14 @@ bool interpretert::memory_offset_to_byte_offset(
mp_integer elem_count;
if(count_type_leaves(at.subtype(), elem_count))
return true;
mp_integer this_idx=cell_offset/elem_count;
mp_integer this_idx=full_cell_offset/elem_count;
if(this_idx>=array_size_vec[0])
return true;
mp_integer subtype_result;
bool ret=
memory_offset_to_byte_offset(at.subtype(),
cell_offset%elem_count,
memory_offset_to_byte_offset(
at.subtype(),
full_cell_offset%elem_count,
subtype_result);
result=subtype_result+(elem_size*this_idx);
return ret;
Expand All @@ -292,7 +295,7 @@ bool interpretert::memory_offset_to_byte_offset(
{
// Primitive type.
result=0;
return cell_offset!=0;
return full_cell_offset!=0;
}
}

Expand Down