Skip to content

Commit

Permalink
Fixed locals and current_memory not having symbolic values
Browse files Browse the repository at this point in the history 
assert(false) was added to some places just to stop the execution once we run a currently unsupported instruction
  • Loading branch information
@MaartenS11
MaartenS11 committed Nov 14, 2023
1 parent 0b1c169 commit 603ed51
Show file tree
Hide file tree
Showing 4 changed files with 41 additions and 15 deletions.
1 change: 0 additions & 1 deletion src/Debug/debugger.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -912,7 +912,6 @@ void Debugger::freeState(Module *m, uint8_t *interruptData) {
m->memory.bytes.clear();
}
m->memory_resize(pages);
m->memory.pages = pages;
// }
// else{
// //TODO fill memory.bytes with zeros
Expand Down
40 changes: 31 additions & 9 deletions src/Interpreter/instructions.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,25 @@ Block *pop_block(Module *m) {
return frame->block;
}

z3::expr encode_as_symbolic(Module *m, StackValue *stack_value) {
z3::expr val = m->ctx.bv_val(0, 32); // Default value.
switch (stack_value->value_type) {
case I32:
val = m->ctx.bv_val(stack_value->value.int32, 32);
break;
case I64:
val = m->ctx.bv_val(stack_value->value.int64, 64);
break;
case F32:
val = m->ctx.fpa_val(stack_value->value.f32);
break;
case F64:
val = m->ctx.fpa_val(stack_value->value.f64);
break;
}
return val;
}

void setup_call(Module *m, uint32_t fidx) {
Block *func = m->functions[fidx];
Type *type = func->type;
Expand Down Expand Up @@ -110,6 +129,7 @@ void setup_call(Module *m, uint32_t fidx) {
m->sp += 1;
m->stack[m->sp].value_type = func->local_value_type[lidx];
m->stack[m->sp].value.uint64 = 0; // Initialize whole union to 0
m->symbolic_stack[m->sp] = encode_as_symbolic(m, &m->stack[m->sp]);
}

// Set program counter to start of function
Expand Down Expand Up @@ -540,7 +560,7 @@ bool i_instr_get_local(Module *m) {
#endif
m->stack[++m->sp] = m->stack[m->fp + arg];
m->symbolic_stack[m->sp] = m->symbolic_stack[m->fp + arg];
std::cout << "local.get " << arg << " = " << m->symbolic_stack[m->sp].value() << std::endl;
//std::cout << "local.get " << arg << " = " << m->symbolic_stack[m->sp].value() << std::endl;
return true;
}

Expand All @@ -550,7 +570,7 @@ bool i_instr_get_local(Module *m) {
bool i_instr_set_local(Module *m) {
int32_t arg = read_LEB_32(&m->pc_ptr);
m->symbolic_stack[m->fp + arg] = m->symbolic_stack[m->sp];
std::cout << "local.set " << arg << " = " << m->symbolic_stack[m->sp].value() << std::endl;
//std::cout << "local.set " << arg << " = " << m->symbolic_stack[m->sp].value() << std::endl;
m->stack[m->fp + arg] = m->stack[m->sp--];
#if TRACE
debug(" - arg: 0x%x, to %s (stack loc: %d)\n", arg,
Expand All @@ -565,7 +585,7 @@ bool i_instr_set_local(Module *m) {
bool i_instr_tee_local(Module *m) {
int32_t arg = read_LEB_32(&m->pc_ptr);
m->stack[m->fp + arg] = m->stack[m->sp];
std::cout << "local.tee " << arg << " = " << m->symbolic_stack[m->sp].value() << std::endl;
//std::cout << "local.tee " << arg << " = " << m->symbolic_stack[m->sp].value() << std::endl;
m->symbolic_stack[m->fp + arg] = m->symbolic_stack[m->sp];
#if TRACE
debug(" - arg: 0x%x, to %s\n", arg, value_repr(&m->stack[m->sp]));
Expand Down Expand Up @@ -607,6 +627,7 @@ bool i_instr_current_memory(Module *m) {
read_LEB_32(&m->pc_ptr); // ignore reserved
m->stack[++m->sp].value_type = I32;
m->stack[m->sp].value.uint32 = m->memory.pages;
m->symbolic_stack[m->sp] = m->memory.pages_symbolic;
return true;
}

Expand All @@ -624,8 +645,7 @@ bool i_instr_grow_memory(Module *m) {
m->stack[m->sp].value.uint32 = static_cast<uint32_t>(-1);
return true;
}
m->memory.pages += delta;
m->memory_resize(m->memory.pages);
m->memory_resize(m->memory.pages + delta);
return true;
}

Expand All @@ -640,8 +660,8 @@ void load(Module *m, uint32_t offset, uint32_t addr) {
for (int i = size - 1; i >= 0; i--) {
expressions.push_back(m->memory.symbolic_bytes[offset + addr + i]);
}
m->symbolic_stack[m->sp] = z3::concat(expressions);
std::cout << "load result = " << m->symbolic_stack[m->sp].value().simplify() << std::endl;
m->symbolic_stack[m->sp] = z3::concat(expressions).simplify();
//std::cout << "load result = " << m->symbolic_stack[m->sp].value().simplify() << std::endl;
}

/**
Expand Down Expand Up @@ -771,11 +791,11 @@ void store(Module *m, uint32_t offset, uint32_t addr, std::pair<StackValue, z3::
m->memory.symbolic_bytes[offset + addr + i] = value.second.extract((i + 1) * 8 - 1, i * 8);
}

std::cout << "store result = ";
/*std::cout << "store result = ";
for (int i = 0; i < size; i++) {
std::cout << m->memory.symbolic_bytes[offset + addr + i].simplify();
}
std::cout << std::endl;
std::cout << std::endl;*/
}

bool i_instr_mem_store(Module *m, uint8_t opcode) {
Expand Down Expand Up @@ -1118,6 +1138,7 @@ bool i_instr_unairy_i32(Module *m, uint8_t opcode) {
return false;
}
m->stack[m->sp].value.uint32 = c;
assert(false);
return true;
}

Expand All @@ -1138,6 +1159,7 @@ bool i_instr_unairy_i64(Module *m, uint8_t opcode) {
return false;
}
m->stack[m->sp].value.uint64 = f;
assert(false);
return true;
}

Expand Down
6 changes: 3 additions & 3 deletions src/Primitives/emulated.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -572,11 +572,11 @@ bool resolve_primitive(char *symbol, Primitive *val) {
return false;
}

Memory external_mem{};
//Memory external_mem{};

bool resolve_external_memory(char *symbol, Memory **val) {
if (!strcmp(symbol, "memory")) {
if (external_mem.bytes.empty()) {
/*if (external_mem.bytes.empty()) {
external_mem.initial = 256;
external_mem.maximum = 256;
external_mem.pages = 256;
Expand All @@ -586,7 +586,7 @@ bool resolve_external_memory(char *symbol, Memory **val) {
//external_mem.bytes.resize(external_mem.pages * PAGE_SIZE, std::pair<uint8_t, z3::expr>(0, ctx.bv_val(0, 8)));
FATAL("TODO: SYMBOLIC EXTERNAL MEMORY");
}
*val = &external_mem;
*val = &external_mem;*/
return true;
}

Expand Down
9 changes: 7 additions & 2 deletions src/WARDuino.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,8 +125,11 @@ struct Memory {
uint32_t pages = 0; // current size (64K pages)
//std::vector<std::pair<uint8_t, z3::expr>> bytes;
std::vector<uint8_t> bytes;
z3::expr symbolic_pages;
std::vector<z3::expr> symbolic_bytes;

explicit Memory(z3::context &ctx) : symbolic_pages(ctx.bv_val(0, 32)) {}

[[nodiscard]] uint8_t read_byte(uint32_t offset) const {
return bytes[offset];
}
Expand Down Expand Up @@ -170,7 +173,8 @@ typedef struct Module {
// same length as byte_count
uint32_t start_function = -1; // function to run on module load
Table table;
Memory memory;
z3::context ctx;
Memory memory = Memory(ctx);
uint32_t global_count = 0; // number of globals
std::vector<StackValue> globals; // globals
std::vector<z3::expr> symbolic_globals; // symbolic globals
Expand All @@ -179,7 +183,6 @@ typedef struct Module {
int sp = -1; // operand stack pointer
int fp = -1; // current frame pointer into stack
std::array<StackValue, STACK_SIZE> stack; // main operand stack
z3::context ctx;
z3::expr path_condition = ctx.bool_val(true);
std::array<std::optional<z3::expr>, STACK_SIZE> symbolic_stack; // symbolic stack
int symbolic_variable_count = 0;
Expand All @@ -191,8 +194,10 @@ typedef struct Module {
char *exception = nullptr; // exception is set when the program fails

void memory_resize(uint32_t new_pages) {
memory.pages = new_pages;
memory.bytes.resize(new_pages * PAGE_SIZE);
memory.symbolic_bytes.resize(new_pages * PAGE_SIZE, ctx.bv_val(0, 8));
memory.symbolic_pages = ctx.bv_val(new_pages, 32);
}
} Module;

Expand Down

0 comments on commit 603ed51

Please sign in to comment.