From a669f3dca84ff9d66e945cdb70b233acec4ea1a7 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Thu, 6 Jun 2019 19:03:25 +0200 Subject: [PATCH 01/21] Implemented follow and merge decision --- selfie.c | 654 ++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 624 insertions(+), 30 deletions(-) diff --git a/selfie.c b/selfie.c index fbd9d964..2941d1fc 100644 --- a/selfie.c +++ b/selfie.c @@ -181,6 +181,7 @@ void printf6(char* s, char* a1, char* a2, char* a3, char* a4, char* a5, char* a6 void sprintf1(char* b, char* s, char* a1); void sprintf2(char* b, char* s, char* a1, char* a2); void sprintf3(char* b, char* s, char* a1, char* a2, char* a3); +void sprintf4(char* b, char* s, char* a1, char* a2, char* a3, char* a4); uint64_t round_up(uint64_t n, uint64_t m); @@ -1195,6 +1196,8 @@ void init_replay_engine() { uint64_t* load_symbolic_memory(uint64_t vaddr); void store_symbolic_memory(uint64_t vaddr, uint64_t val, char* sym, char* var, uint64_t bits); +void copy_symbolic_memory(uint64_t* from_context, uint64_t* to_context); +void delete_word_from_symbolic_memory(uint64_t vaddr); uint64_t is_symbolic_value(uint64_t* sword); @@ -1238,6 +1241,23 @@ char* smt_variable(char* prefix, uint64_t bits); char* smt_unary(char* opt, char* op); char* smt_binary(char* opt, char* op1, char* op2); +char* smt_ternary(char* opt, char* op1, char* op2, char* op3); + +uint64_t find_merge_location(uint64_t beq_imm); + +void add_mergeable_context(uint64_t* context); +uint64_t* get_mergeable_context(); + +void add_waiting_context(uint64_t* context); +uint64_t* get_waiting_context(); + +void add_prologue_start_and_corresponding_merge_location(uint64_t prologue_start, uint64_t merge_location); +uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue_start); +uint64_t is_start_of_procedure_prologue(uint64_t prologue_start); + +void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t location); +void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context); +uint64_t* merge_if_possible_and_get_next_context(uint64_t* context); // ------------------------ GLOBAL VARIABLES ----------------------- @@ -1256,6 +1276,20 @@ uint64_t* reg_sym = (uint64_t*) 0; // symbolic values in registers as strings in char* smt_name = (char*) 0; // name of SMT-LIB file uint64_t smt_fd = 0; // file descriptor of open SMT-LIB file +uint64_t* mergeable_contexts = (uint64_t*) 0; // contexts that have reached their merge location +uint64_t* waiting_contexts = (uint64_t*) 0; // contexts that were created at a symbolic beq instruction and are waiting to be executed +uint64_t* prologues_and_corresponding_merge_locations = (uint64_t*) 0; // stack which stores possible function prologues and their corresponding merge locations + +uint64_t* current_mergeable_context = (uint64_t*) 0; // current context with which the active context can possibly be merged + +uint64_t in_recursion = 0; +uint64_t prologue_and_corresponding_merge_location = 0; +uint64_t prologue_start = 0; + +// ------------------------ GLOBAL CONSTANTS ----------------------- + +uint64_t BEQ_LIMIT = 100; // limit of symbolic beq instructions on any given path + // ----------------------------------------------------------------- // -------------------------- INTERPRETER -------------------------- // ----------------------------------------------------------------- @@ -1319,6 +1353,7 @@ uint64_t EXCEPTION_TIMER = 3; uint64_t EXCEPTION_INVALIDADDRESS = 4; uint64_t EXCEPTION_DIVISIONBYZERO = 5; uint64_t EXCEPTION_UNKNOWNINSTRUCTION = 6; +uint64_t EXCEPTION_MERGE = 7; uint64_t* EXCEPTIONS; // strings representing exceptions @@ -1388,6 +1423,7 @@ void init_interpreter() { *(EXCEPTIONS + EXCEPTION_INVALIDADDRESS) = (uint64_t) "invalid address"; *(EXCEPTIONS + EXCEPTION_DIVISIONBYZERO) = (uint64_t) "division by zero"; *(EXCEPTIONS + EXCEPTION_UNKNOWNINSTRUCTION) = (uint64_t) "unknown instruction"; + *(EXCEPTIONS + EXCEPTION_MERGE) = (uint64_t) "merge interrupt"; } void reset_interpreter() { @@ -1429,8 +1465,8 @@ void reset_profiler() { uint64_t* new_context(); -void init_context(uint64_t* context, uint64_t* parent, uint64_t* vctxt); -void copy_context(uint64_t* original, uint64_t location, char* condition, uint64_t depth); +void init_context(uint64_t* context, uint64_t* parent, uint64_t* vctxt); +uint64_t* copy_context(uint64_t* original, uint64_t location, char* condition, uint64_t depth); uint64_t* find_context(uint64_t* parent, uint64_t* vctxt); @@ -1462,7 +1498,8 @@ uint64_t* delete_context(uint64_t* context, uint64_t* from); // | 17 | path condition | pointer to path condition // | 18 | symbolic memory | pointer to symbolic memory // | 19 | symbolic regs | pointer to symbolic registers -// | 20 | related context | pointer to list of contexts of related branches +// | 20 | beq counter | number of executed symbolic beq instructions +// | 21 | merge location | program location at which the context can possibly be merged (later) // +----+-----------------+ uint64_t* allocate_context() { @@ -1470,7 +1507,7 @@ uint64_t* allocate_context() { } uint64_t* allocate_symbolic_context() { - return smalloc(7 * SIZEOFUINT64STAR + 9 * SIZEOFUINT64 + 4 * SIZEOFUINT64STAR + 1 * SIZEOFUINT64); + return smalloc(7 * SIZEOFUINT64STAR + 9 * SIZEOFUINT64 + 3 * SIZEOFUINT64STAR + 3 * SIZEOFUINT64); } uint64_t next_context(uint64_t* context) { return (uint64_t) context; } @@ -1511,7 +1548,8 @@ uint64_t get_execution_depth(uint64_t* context) { return *(context char* get_path_condition(uint64_t* context) { return (char*) *(context + 17); } uint64_t* get_symbolic_memory(uint64_t* context) { return (uint64_t*) *(context + 18); } uint64_t* get_symbolic_regs(uint64_t* context) { return (uint64_t*) *(context + 19); } -uint64_t* get_related_context(uint64_t* context) { return (uint64_t*) *(context + 20); } +uint64_t get_beq_counter(uint64_t* context) { return *(context + 20); } +uint64_t get_merge_location(uint64_t* context) { return *(context + 21); } void set_next_context(uint64_t* context, uint64_t* next) { *context = (uint64_t) next; } void set_prev_context(uint64_t* context, uint64_t* prev) { *(context + 1) = (uint64_t) prev; } @@ -1534,7 +1572,8 @@ void set_execution_depth(uint64_t* context, uint64_t depth) { *(context + 16) void set_path_condition(uint64_t* context, char* path) { *(context + 17) = (uint64_t) path; } void set_symbolic_memory(uint64_t* context, uint64_t* memory) { *(context + 18) = (uint64_t) memory; } void set_symbolic_regs(uint64_t* context, uint64_t* regs) { *(context + 19) = (uint64_t) regs; } -void set_related_context(uint64_t* context, uint64_t* related) { *(context + 20) = (uint64_t) related; } +void set_beq_counter(uint64_t* context, uint64_t counter) { *(context + 20) = counter; } +void set_merge_location(uint64_t* context, uint64_t location) { *(context + 21) = location; } // ----------------------------------------------------------------- // -------------------------- MICROKERNEL -------------------------- @@ -1592,6 +1631,7 @@ uint64_t handle_system_call(uint64_t* context); uint64_t handle_page_fault(uint64_t* context); uint64_t handle_division_by_zero(uint64_t* context); uint64_t handle_timer(uint64_t* context); +uint64_t handle_merge(uint64_t* context); uint64_t handle_exception(uint64_t* context); @@ -1619,6 +1659,7 @@ uint64_t* MY_CONTEXT = (uint64_t*) 0; uint64_t DONOTEXIT = 0; uint64_t EXIT = 1; +uint64_t MERGE = 2; uint64_t EXITCODE_NOERROR = 0; uint64_t EXITCODE_BADARGUMENTS = 1; @@ -2552,6 +2593,16 @@ void sprintf3(char* b, char* s, char* a1, char* a2, char* a3) { output_cursor = 0; } +void sprintf4(char* b, char* s, char* a1, char* a2, char* a3, char* a4) { + output_buffer = b; + output_cursor = 0; + + printf4(s, a1, a2, a3, a4);put_character(0); + + output_buffer = (char*) 0; + output_cursor = 0; +} + uint64_t round_up(uint64_t n, uint64_t m) { if (n % m == 0) return n; @@ -7376,14 +7427,35 @@ void constrain_beq() { print_code_context_for_instruction(pc); println(); - copy_context(current_context, - pc + INSTRUCTIONSIZE, - smt_binary("and", pvar, smt_unary("not", bvar)), - max_execution_depth - timer); + // increase the number of executed symbolic beq instructions + set_beq_counter(current_context, get_beq_counter(current_context) + 1); + + if (get_beq_counter(current_context) < BEQ_LIMIT) { + // save symbolic memory so that it is copied correctly afterwards + set_symbolic_memory(current_context, symbolic_memory); + + // the copied context is executed later and takes the other path + add_waiting_context(copy_context(current_context, pc + imm, smt_binary("and", pvar, bvar), max_execution_depth - timer)); - path_condition = smt_binary("and", pvar, bvar); + path_condition = smt_binary("and", pvar, smt_unary("not", bvar)); - pc = pc + imm; + set_merge_location(current_context, find_merge_location(imm)); + + // check if a context is waiting to be merged + if (current_mergeable_context != (uint64_t*) 0) { + // we cannot merge with this one (yet), so we add it back to the stack of mergeable contexts + add_mergeable_context(current_mergeable_context); + current_mergeable_context = (uint64_t*) 0; + } + + pc = pc + INSTRUCTIONSIZE; + } else { + // if the limit of symbolic beq instructions is reached, the path still continues until it has reached its + // maximal execution depth, but only by following the true case of the next encountered symbolic beq instructions + path_condition = smt_binary("and", pvar, bvar); + + pc = pc + imm; + } } void print_jal() { @@ -7657,6 +7729,9 @@ void store_symbolic_memory(uint64_t vaddr, uint64_t val, char* sym, char* var, u sword = allocate_symbolic_memory_word(); + // we 'delete' the word, if it already exists in the symbolic memory + delete_word_from_symbolic_memory(vaddr); + set_next_word(sword, symbolic_memory); set_word_address(sword, vaddr); set_word_value(sword, val); @@ -7677,6 +7752,51 @@ void store_symbolic_memory(uint64_t vaddr, uint64_t val, char* sym, char* var, u symbolic_memory = sword; } +void copy_symbolic_memory(uint64_t* from_context, uint64_t* to_context) { + uint64_t* sword; + uint64_t* sword_copy; + uint64_t* symbolic_memory_copy; + uint64_t* previous; + + sword = get_symbolic_memory(from_context); + symbolic_memory_copy = (uint64_t*) 0; + + while (sword) { + sword_copy = allocate_symbolic_memory_word(); + + set_word_address(sword_copy, get_word_address(sword)); + set_word_value(sword_copy, get_word_value(sword)); + set_word_symbolic(sword_copy, get_word_symbolic(sword)); + set_number_of_bits(sword_copy, get_number_of_bits(sword)); + + if (previous != (uint64_t*) 0) + set_next_word(previous, sword_copy); + + if (symbolic_memory_copy == (uint64_t*) 0) + symbolic_memory_copy = sword_copy; + + previous = sword_copy; + sword = get_next_word(sword); + } + + set_next_word(sword_copy, 0); + set_symbolic_memory(to_context, symbolic_memory_copy); +} + +void delete_word_from_symbolic_memory(uint64_t vaddr) { + uint64_t* sword; + + sword = symbolic_memory; + + while (sword) { + if (get_word_address(sword) == vaddr) + // note: we do not really delete the word, we just set the virtual address to -1 + set_word_address(sword, -1); + + sword = get_next_word(sword); + } +} + uint64_t is_symbolic_value(uint64_t* sword) { return get_word_symbolic(sword) != (char*) 0; } @@ -7765,6 +7885,379 @@ char* smt_binary(char* opt, char* op1, char* op2) { return string; } +char* smt_ternary(char* opt, char* op1, char* op2, char* op3) { + char* string; + + string = string_alloc(1 + string_length(opt) + 1 + string_length(op1) + 1 + string_length(op2) + 1 + string_length(op3) + 1); + + sprintf4(string, "(%s %s %s %s)", opt, op1, op2, op3); + + return string; +} + +uint64_t find_merge_location(uint64_t beq_imm) { + uint64_t original_pc; + uint64_t original_imm; + uint64_t merge_location; + + // assert: the current instruction is a symbolic beq instruction + original_pc = pc; + original_imm = imm; + + // examine last instruction before target location of the beq instruction + pc = pc + (beq_imm - INSTRUCTIONSIZE); + + // we need to know which instruction it is + fetch(); + decode(); + + if (is != JAL) + // no jal instruction -> end of if without else branch + // merge is directly at target location of the beq instruction possible + merge_location = original_pc + beq_imm; + else { + if (signed_less_than(imm, 0) == 0) { + // jal with positive imm -> end of if with else branch + // we have to skip the else branch in order to merge afterwards + merge_location = pc + imm; + + pc = original_pc + INSTRUCTIONSIZE; + } else + // jal with negative imm -> end of loop body + // merge is only outside of the loop possible + merge_location = pc + INSTRUCTIONSIZE; + } + + // we need to check if we are inside of a recursion before we reach the merge location + // if we are, we merge only when the recursion is finished + while (pc != merge_location) { + fetch(); + decode(); + + if (is == JAL) + if (is_start_of_procedure_prologue(pc + imm)) { + in_recursion = 1; + merge_location = get_merge_location_from_corresponding_prologue_start(pc + imm); + } + + pc = pc + INSTRUCTIONSIZE; + } + + // restore the original program state + pc = original_pc; + imm = original_imm; + + return merge_location; +} + +void add_mergeable_context(uint64_t* context) { + uint64_t* entry; + + entry = smalloc(2 * SIZEOFUINT64STAR); + + *(entry + 0) = (uint64_t) mergeable_contexts; + *(entry + 1) = (uint64_t) context; + + mergeable_contexts = entry; +} + +uint64_t* get_mergeable_context() { + uint64_t* head; + + if (mergeable_contexts == (uint64_t*) 0) + return (uint64_t*) 0; + + head = mergeable_contexts; + mergeable_contexts = (uint64_t*) *(head + 0); + + return (uint64_t*) *(head + 1); +} + +void add_waiting_context(uint64_t* context) { + uint64_t* entry; + + entry = smalloc(2 * SIZEOFUINT64STAR); + + *(entry + 0) = (uint64_t) waiting_contexts; + *(entry + 1) = (uint64_t) context; + + waiting_contexts = entry; +} + +uint64_t* get_waiting_context() { + uint64_t* head; + + if (waiting_contexts == (uint64_t*) 0) + return (uint64_t*) 0; + + head = waiting_contexts; + waiting_contexts = (uint64_t*) *(head + 0); + + return (uint64_t*) *(head + 1); +} + +void add_prologue_start_and_corresponding_merge_location(uint64_t prologue_start, uint64_t merge_location) { + uint64_t* entry; + + entry = prologues_and_corresponding_merge_locations; + + // do not add duplicates + while (entry) { + if (*(entry + 1) == prologue_start) + return; + + entry = (uint64_t*) *(entry + 0); + } + + entry = smalloc(3 * SIZEOFUINT64STAR); + + *(entry + 0) = (uint64_t) prologues_and_corresponding_merge_locations; + *(entry + 1) = (uint64_t) prologue_start; + *(entry + 2) = (uint64_t) merge_location; + + prologues_and_corresponding_merge_locations = entry; +} + +uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue_start) { + uint64_t* entry; + + entry = prologues_and_corresponding_merge_locations; + + while (entry) { + if (*(entry + 1) == prologue_start) + return (uint64_t) *(entry + 2); + + entry = (uint64_t*) *(entry + 0); + } + + return -1; +} + +uint64_t is_start_of_procedure_prologue(uint64_t prologue_start) { + return (get_merge_location_from_corresponding_prologue_start(prologue_start) != (uint64_t) -1); +} + +void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t location) { + print("; merging two contexts at "); + print_code_context_for_instruction(location); + println(); + + if (prologues_and_corresponding_merge_locations != (uint64_t*) 0) + if (get_pc(active_context) == *(prologues_and_corresponding_merge_locations + 2)) + // we have finished the recursion + in_recursion = 0; + + // merging the symbolic store + merge_symbolic_store(active_context, mergeable_context); + + // merging the path condition + path_condition = smt_binary("or", get_path_condition(active_context), get_path_condition(mergeable_context)); + set_path_condition(active_context, path_condition); + + current_mergeable_context = get_mergeable_context(); + + // it may be possible that more contexts can be merged + if (current_mergeable_context != (uint64_t*) 0) + if (pc == get_pc(current_mergeable_context)) + merge(active_context, current_mergeable_context, pc); +} + +void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context) { + uint64_t* sword_from_active_context; + uint64_t* sword_from_mergeable_context; + uint64_t i; + + sword_from_active_context = symbolic_memory; + // merging the symbolic memory + while (sword_from_active_context) { + // check if the word has not already been 'deleted' (note: 'deleted' would mean a virtual address of -1) + if (get_word_address(sword_from_active_context) != (uint64_t) -1) { + sword_from_mergeable_context = get_symbolic_memory(mergeable_context); + + while (sword_from_mergeable_context) { + if (get_word_address(sword_from_active_context) == get_word_address(sword_from_mergeable_context)) { + if (get_word_symbolic(sword_from_active_context) != (char*) 0) { + if (get_word_symbolic(sword_from_mergeable_context) != (char*) 0) { + if (get_word_symbolic(sword_from_active_context) != get_word_symbolic(sword_from_mergeable_context)) { + // merge symbolic values if they are different + set_word_symbolic(sword_from_active_context, + smt_ternary("ite", + get_path_condition(active_context), + get_word_symbolic(sword_from_active_context), + get_word_symbolic(sword_from_mergeable_context) + ) + ); + + // 'delete' the word since it does not need to be merged again + set_word_address(sword_from_mergeable_context, -1); + } + } else { + // merge symbolic value and concrete value + set_word_symbolic(sword_from_active_context, + smt_ternary("ite", + get_path_condition(active_context), + get_word_symbolic(sword_from_active_context), + bv_constant(get_word_value(sword_from_mergeable_context)) + ) + ); + + // 'delete' the word since it does not need to be merged again + set_word_address(sword_from_mergeable_context, -1); + } + } else { + if (get_word_symbolic(sword_from_mergeable_context) != (char*) 0) { + // merge concrete value and symbolic value + set_word_symbolic(sword_from_active_context, + smt_ternary("ite", + get_path_condition(active_context), + bv_constant(get_word_value(sword_from_active_context)), + get_word_symbolic(sword_from_mergeable_context) + ) + ); + + // 'delete' the word since it does not need to be merged again + set_word_address(sword_from_mergeable_context, -1); + } else { + if (get_word_value(sword_from_active_context) != get_word_value(sword_from_mergeable_context)) { + // merge concrete values if they are different + set_word_symbolic(sword_from_active_context, + smt_ternary("ite", + get_path_condition(active_context), + bv_constant(get_word_value(sword_from_active_context)), + bv_constant(get_word_value(sword_from_mergeable_context)) + ) + ); + + // 'delete' the word since it does not need to be merged again + set_word_address(sword_from_mergeable_context, -1); + } + } + } + } + + sword_from_mergeable_context = get_next_word(sword_from_mergeable_context); + } + } + + sword_from_active_context = get_next_word(sword_from_active_context); + } + + // the active context contains now the merged symbolic memory + set_symbolic_memory(active_context, symbolic_memory); + + i = 0; + + // merging the symbolic registers + while (i < NUMBEROFREGISTERS) { + if (*(get_symbolic_regs(active_context) + i) != 0) { + if (*(get_symbolic_regs(mergeable_context) + i) != 0) { + if (*(get_symbolic_regs(active_context) + i) != *(get_symbolic_regs(mergeable_context) + i)) + // merge symbolic values if they are different + *(reg_sym + i) = (uint64_t) smt_ternary("ite", + get_path_condition(active_context), + (char*) *(get_symbolic_regs(active_context) + i), + (char*) *(get_symbolic_regs(mergeable_context) + i) + ); + } else + // merge symbolic value and concrete value + *(reg_sym + i) = (uint64_t) smt_ternary("ite", + get_path_condition(active_context), + (char*) *(get_symbolic_regs(active_context) + i), + bv_constant(*(get_regs(mergeable_context) + i)) + ); + } else { + if (*(get_symbolic_regs(mergeable_context) + i) != 0) + // merge concrete value and symbolic value + *(reg_sym + i) = (uint64_t) smt_ternary("ite", + get_path_condition(active_context), + bv_constant(*(get_regs(active_context) + i)), + (char*) *(get_symbolic_regs(mergeable_context) + i) + ); + else + if (*(get_regs(active_context) + i) != *(get_regs(mergeable_context) + i)) + // merge concrete values if they are different + *(reg_sym + i) = (uint64_t) smt_ternary("ite", + get_path_condition(active_context), + bv_constant(*(get_regs(active_context) + i)), + bv_constant(*(get_regs(mergeable_context) + i)) + ); + } + + i = i + 1; + } + + set_symbolic_regs(active_context, reg_sym); +} + +uint64_t* merge_if_possible_and_get_next_context(uint64_t* context) { + uint64_t merge_not_finished; + uint64_t mergeable; + uint64_t pauseable; + + merge_not_finished = 1; + + while (merge_not_finished) { + mergeable = 1; + pauseable = 1; + + if (context == (uint64_t*) 0) { + // break out of the loop + mergeable = 0; + pauseable = 0; + } else + symbolic_memory = get_symbolic_memory(context); + + // check if the context can be merged with one or more mergeable contexts + while (mergeable) { + if (current_mergeable_context == (uint64_t*) 0) + current_mergeable_context = get_mergeable_context(); + + if (current_mergeable_context != (uint64_t*) 0) { + if (get_pc(context) == get_pc(current_mergeable_context)) + merge(context, current_mergeable_context, get_pc(context)); + else + mergeable = 0; + } else + mergeable = 0; + } + + // check if the context has reached a merge location and needs to be paused + while (pauseable) { + if (get_pc(context) == get_merge_location(context)) { + add_mergeable_context(context); + context = get_waiting_context(); + + // break out of the loop + if (context == (uint64_t*) 0) { + mergeable = 0; + pauseable = 0; + } + + } else { + if (current_mergeable_context == (uint64_t*) 0) + current_mergeable_context = get_mergeable_context(); + + if (current_mergeable_context != (uint64_t*) 0) + if (get_pc(context) == get_pc(current_mergeable_context)) + mergeable = 1; + + pauseable = 0; + } + } + + if (mergeable == 0) + if (pauseable == 0) + merge_not_finished = 0; + } + + // check if there are contexts which have been paused and were not merged yet + if (context == (uint64_t*) 0) + context = get_mergeable_context(); + + return context; +} + + // ----------------------------------------------------------------- // -------------------------- INTERPRETER -------------------------- // ----------------------------------------------------------------- @@ -8084,6 +8577,9 @@ void execute_debug() { } void execute_symbolically() { + uint64_t pc_after_jal; + uint64_t pc_before_jal; + // assert: 1 <= is <= number of RISC-U instructions if (is == ADDI) { constrain_addi(); @@ -8113,9 +8609,54 @@ void execute_symbolically() { do_sltu(); } else if (is == BEQ) constrain_beq(); - else if (is == JAL) + else if (is == JAL) { + pc_before_jal = pc; do_jal(); - else if (is == JALR) { + + pc_after_jal = pc; + + // we need to check if we jump into a recursion + fetch(); + decode(); + + if (is == ADDI) { + pc = pc + INSTRUCTIONSIZE; + fetch(); + decode(); + + if (is == SD) { + pc = pc + INSTRUCTIONSIZE; + fetch(); + decode(); + + if (is == ADDI) { + pc = pc + INSTRUCTIONSIZE; + fetch(); + decode(); + + if (is == SD) { + pc = pc + INSTRUCTIONSIZE; + fetch(); + decode(); + + // note: this check is not completely sufficient to determine a prologue of a procedure + // we would still have to check the registers, however, for the sake of simplicity this has been omitted + // we assume that we have identified a prologue of a procedure + if (is == ADDI) + // if we are already in a recursion, we do not change the merge location since we only merge when the recursion is finished + if (in_recursion == 0) { + prologue_and_corresponding_merge_location = pc_before_jal + 4 * INSTRUCTIONSIZE; + prologue_start = pc_after_jal; + add_prologue_start_and_corresponding_merge_location(prologue_start, prologue_and_corresponding_merge_location); + } + + } + } + } + } + + pc = pc_after_jal; + } else if (is == JALR) { constrain_jalr(); do_jalr(); } else if (is == LUI) { @@ -8139,6 +8680,20 @@ void interrupt() { timer = 1; } } + + if (symbolic) { + if (current_mergeable_context != (uint64_t*) 0) + // if both contexts are at the same program location, they can be merged + if (pc == get_pc(current_mergeable_context)) + merge(current_context, current_mergeable_context, pc); + + // check if the current context has reached a merge location + if (pc == get_merge_location(current_context)) + if (get_exception(current_context) == EXCEPTION_NOEXCEPTION) + // only throw exception if no other is pending + // TODO: handle multiple pending exceptions + throw_exception(EXCEPTION_MERGE, 0); + } } void run_until_exception() { @@ -8302,11 +8857,12 @@ void init_context(uint64_t* context, uint64_t* parent, uint64_t* vctxt) { set_path_condition(context, "true"); set_symbolic_memory(context, (uint64_t*) 0); set_symbolic_regs(context, zalloc(NUMBEROFREGISTERS * REGISTERSIZE)); - set_related_context(context, (uint64_t*) 0); + set_beq_counter(context, 0); + set_merge_location(context, -1); } } -void copy_context(uint64_t* original, uint64_t location, char* condition, uint64_t depth) { +uint64_t* copy_context(uint64_t* original, uint64_t location, char* condition, uint64_t depth) { uint64_t* context; uint64_t r; @@ -8338,7 +8894,10 @@ void copy_context(uint64_t* original, uint64_t location, char* condition, uint64 set_execution_depth(context, depth); set_path_condition(context, condition); - set_symbolic_memory(context, symbolic_memory); + set_beq_counter(context, get_beq_counter(original)); + set_merge_location(context, get_merge_location(original)); + + copy_symbolic_memory(original, context); set_symbolic_regs(context, smalloc(NUMBEROFREGISTERS * REGISTERSIZE)); @@ -8350,9 +8909,9 @@ void copy_context(uint64_t* original, uint64_t location, char* condition, uint64 r = r + 1; } - set_related_context(context, symbolic_contexts); - symbolic_contexts = context; + + return context; } uint64_t* find_context(uint64_t* parent, uint64_t* vctxt) { @@ -8819,18 +9378,26 @@ uint64_t handle_timer(uint64_t* context) { set_exception(context, EXCEPTION_NOEXCEPTION); if (symbolic) { - print("(push 1)\n"); + print(";(push 1)\n"); - printf1("(assert (not %s)); timeout in ", path_condition); + printf1(";(assert (not %s)); timeout in ", path_condition); print_code_context_for_instruction(pc); - print("\n(check-sat)\n(get-model)\n(pop 1)\n"); + print("\n;(check-sat)\n;(get-model)\n;(pop 1)\n"); return EXIT; } else return DONOTEXIT; } +uint64_t handle_merge(uint64_t* context) { + add_mergeable_context(current_context); + + set_exception(context, EXCEPTION_NOEXCEPTION); + + return MERGE; +} + uint64_t handle_exception(uint64_t* context) { uint64_t exception; @@ -8844,6 +9411,8 @@ uint64_t handle_exception(uint64_t* context) { return handle_division_by_zero(context); else if (exception == EXCEPTION_TIMER) return handle_timer(context); + else if (exception == EXCEPTION_MERGE) + return handle_merge(context); else { printf2("%s: context %s throws uncaught ", selfie_name, get_name(context)); print_exception(exception, get_faulting_page(context)); @@ -9060,8 +9629,9 @@ char* replace_extension(char* filename, char* extension) { } uint64_t monster(uint64_t* to_context) { - uint64_t timeout; + uint64_t timeout; uint64_t* from_context; + uint64_t exception; print("monster\n"); @@ -9094,7 +9664,7 @@ uint64_t monster(uint64_t* to_context) { print("(set-option :incremental true)\n"); print("(set-logic QF_BV)\n\n"); - timeout = max_execution_depth; + timeout = max_execution_depth - get_execution_depth(to_context); while (1) { from_context = mipster_switch(to_context, timeout); @@ -9105,14 +9675,34 @@ uint64_t monster(uint64_t* to_context) { timeout = TIMEROFF; } else { - if (handle_exception(from_context) == EXIT) { - if (symbolic_contexts) { - to_context = symbolic_contexts; + exception = handle_exception(from_context); - timeout = get_execution_depth(to_context); + if (exception == EXIT) { + // if a context is currently waiting to be merged, we need to switch to this one + if (current_mergeable_context != (uint64_t*) 0) { + // update the merge location, so the 'new' context can be merged later + set_merge_location(current_mergeable_context, get_merge_location(current_context)); - symbolic_contexts = get_related_context(symbolic_contexts); - } else { + to_context = current_mergeable_context; + + // if no context is currently waiting to be merged, we switch to the next waiting context + } else + to_context = get_waiting_context(); + + // it may be possible that there are no waiting contexts, but mergeable contexts + if (to_context == (uint64_t*) 0) { + to_context = get_mergeable_context(); + + if (to_context) + // update the merge location, so the 'new' context can be merged later + set_merge_location(to_context, get_merge_location(current_context)); + } + + to_context = merge_if_possible_and_get_next_context(to_context); + + if (to_context) + timeout = max_execution_depth - get_execution_depth(to_context); + else { print("\n(exit)"); output_name = (char*) 0; @@ -9124,6 +9714,10 @@ uint64_t monster(uint64_t* to_context) { return EXITCODE_NOERROR; } + } else if (exception == MERGE) { + to_context = merge_if_possible_and_get_next_context(get_waiting_context()); + + timeout = max_execution_depth - get_execution_depth(to_context); } else { timeout = timer; From 0c4457170547ddec6b6c6eb876ae7e8e6804c960 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Thu, 6 Jun 2019 20:27:46 +0200 Subject: [PATCH 02/21] Fixed some memory issues --- selfie.c | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/selfie.c b/selfie.c index 2941d1fc..27c0689d 100644 --- a/selfie.c +++ b/selfie.c @@ -1414,7 +1414,7 @@ uint64_t* stores_per_instruction = (uint64_t*) 0; // number of executed stores p // ------------------------- INITIALIZATION ------------------------ void init_interpreter() { - EXCEPTIONS = smalloc((EXCEPTION_UNKNOWNINSTRUCTION + 1) * SIZEOFUINT64STAR); + EXCEPTIONS = smalloc((EXCEPTION_MERGE + 1) * SIZEOFUINT64STAR); *(EXCEPTIONS + EXCEPTION_NOEXCEPTION) = (uint64_t) "no exception"; *(EXCEPTIONS + EXCEPTION_PAGEFAULT) = (uint64_t) "page fault"; @@ -7759,7 +7759,10 @@ void copy_symbolic_memory(uint64_t* from_context, uint64_t* to_context) { uint64_t* previous; sword = get_symbolic_memory(from_context); + + sword_copy = (uint64_t*) 0; symbolic_memory_copy = (uint64_t*) 0; + previous = (uint64_t*) 0; while (sword) { sword_copy = allocate_symbolic_memory_word(); From 39a6f45f2a961d76d6755117380f38413ace519a Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Thu, 6 Jun 2019 21:24:23 +0200 Subject: [PATCH 03/21] Adjusted Makefile --- Makefile | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Makefile b/Makefile index cdda0091..949119d5 100755 --- a/Makefile +++ b/Makefile @@ -88,8 +88,7 @@ qemu: selfie.m selfie.s # Test boolector SMT solver boolector: smt boolector manuscript/code/symbolic/simple-assignment.smt -e 0 > selfie_boolector.sat - [ $$(grep ^sat$$ selfie_boolector.sat | wc -l) -eq 2 ] - [ $$(grep ^unsat$$ selfie_boolector.sat | wc -l) -eq 1 ] + [ $$(grep ^sat$$ selfie_boolector.sat | wc -l) -eq 1 ] # Test btormc bounded model checker btormc: mc From a2acce36b03dc873775b20a3407a720051fabd98 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Mon, 10 Jun 2019 13:42:36 +0200 Subject: [PATCH 04/21] Adjusted beq limit and added support for enabling/disabling merging --- selfie.c | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/selfie.c b/selfie.c index 27c0689d..8d844e40 100644 --- a/selfie.c +++ b/selfie.c @@ -1276,6 +1276,8 @@ uint64_t* reg_sym = (uint64_t*) 0; // symbolic values in registers as strings in char* smt_name = (char*) 0; // name of SMT-LIB file uint64_t smt_fd = 0; // file descriptor of open SMT-LIB file +uint64_t merge_enabled = 1; // enable or disable the merging + uint64_t* mergeable_contexts = (uint64_t*) 0; // contexts that have reached their merge location uint64_t* waiting_contexts = (uint64_t*) 0; // contexts that were created at a symbolic beq instruction and are waiting to be executed uint64_t* prologues_and_corresponding_merge_locations = (uint64_t*) 0; // stack which stores possible function prologues and their corresponding merge locations @@ -1288,7 +1290,7 @@ uint64_t prologue_start = 0; // ------------------------ GLOBAL CONSTANTS ----------------------- -uint64_t BEQ_LIMIT = 100; // limit of symbolic beq instructions on any given path +uint64_t BEQ_LIMIT = 35; // limit of symbolic beq instructions on any given path // ----------------------------------------------------------------- // -------------------------- INTERPRETER -------------------------- @@ -7439,7 +7441,9 @@ void constrain_beq() { path_condition = smt_binary("and", pvar, smt_unary("not", bvar)); - set_merge_location(current_context, find_merge_location(imm)); + // set the merge location only when merging is enabled + if (merge_enabled) + set_merge_location(current_context, find_merge_location(imm)); // check if a context is waiting to be merged if (current_mergeable_context != (uint64_t*) 0) { From 6ded1008938c40f8ba48a907881c14bb8a2f9467 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Mon, 10 Jun 2019 13:45:14 +0200 Subject: [PATCH 05/21] Merging is disabled if the path condition becomes too large --- selfie.c | 34 +++++++++++++++++++++++++++++----- 1 file changed, 29 insertions(+), 5 deletions(-) diff --git a/selfie.c b/selfie.c index 8d844e40..2eb6e290 100644 --- a/selfie.c +++ b/selfie.c @@ -1290,7 +1290,8 @@ uint64_t prologue_start = 0; // ------------------------ GLOBAL CONSTANTS ----------------------- -uint64_t BEQ_LIMIT = 35; // limit of symbolic beq instructions on any given path +uint64_t BEQ_LIMIT = 35; // limit of symbolic beq instructions on any given path +uint64_t MAX_PATH_CONDITION_LENGTH = 1000000; // ----------------------------------------------------------------- // -------------------------- INTERPRETER -------------------------- @@ -8045,6 +8046,16 @@ uint64_t is_start_of_procedure_prologue(uint64_t prologue_start) { } void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t location) { + // do not merge if merging is disabled + if (merge_enabled == 0) { + if (current_mergeable_context != (uint64_t*) 0) { + add_mergeable_context(current_mergeable_context); + current_mergeable_context = (uint64_t*) 0; + } + + return; + } + print("; merging two contexts at "); print_code_context_for_instruction(location); println(); @@ -8057,6 +8068,10 @@ void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t locat // merging the symbolic store merge_symbolic_store(active_context, mergeable_context); + // disable merging if the path condition becomes too large + if (string_length(smt_binary("or", get_path_condition(active_context), get_path_condition(mergeable_context))) > MAX_PATH_CONDITION_LENGTH) + merge_enabled = 0; + // merging the path condition path_condition = smt_binary("or", get_path_condition(active_context), get_path_condition(mergeable_context)); set_path_condition(active_context, path_condition); @@ -8201,7 +8216,10 @@ uint64_t* merge_if_possible_and_get_next_context(uint64_t* context) { uint64_t mergeable; uint64_t pauseable; - merge_not_finished = 1; + if (merge_enabled) + merge_not_finished = 1; + else + merge_not_finished = 0; while (merge_not_finished) { mergeable = 1; @@ -8220,9 +8238,12 @@ uint64_t* merge_if_possible_and_get_next_context(uint64_t* context) { current_mergeable_context = get_mergeable_context(); if (current_mergeable_context != (uint64_t*) 0) { - if (get_pc(context) == get_pc(current_mergeable_context)) - merge(context, current_mergeable_context, get_pc(context)); - else + if (get_pc(context) == get_pc(current_mergeable_context)) { + if (merge_enabled) + merge(context, current_mergeable_context, get_pc(context)); + else + mergeable = 0; + } else mergeable = 0; } else mergeable = 0; @@ -8261,6 +8282,9 @@ uint64_t* merge_if_possible_and_get_next_context(uint64_t* context) { if (context == (uint64_t*) 0) context = get_mergeable_context(); + if (merge_enabled == 0) + merge_not_finished = 0; + return context; } From 2bfd949273839e94075d3b5cd52fa146003783c2 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Tue, 11 Jun 2019 14:10:19 +0200 Subject: [PATCH 06/21] Introduced constants to indicate the status of a symbolic memory word --- selfie.c | 108 ++++++++++++++++++++++++++++++------------------------- 1 file changed, 59 insertions(+), 49 deletions(-) diff --git a/selfie.c b/selfie.c index 2eb6e290..6b4c9c6a 100644 --- a/selfie.c +++ b/selfie.c @@ -1290,6 +1290,9 @@ uint64_t prologue_start = 0; // ------------------------ GLOBAL CONSTANTS ----------------------- +uint64_t DELETED = -1; // indicates that a symbolic memory word has been deleted +uint64_t MERGED = -2; // indicates that a symbolic memory word has been merged + uint64_t BEQ_LIMIT = 35; // limit of symbolic beq instructions on any given path uint64_t MAX_PATH_CONDITION_LENGTH = 1000000; @@ -7798,8 +7801,12 @@ void delete_word_from_symbolic_memory(uint64_t vaddr) { while (sword) { if (get_word_address(sword) == vaddr) - // note: we do not really delete the word, we just set the virtual address to -1 - set_word_address(sword, -1); + /* we indicate that this word has been deleted in order to avoid finding + outdated values when searching the symbolic memory later on + + note: the word is not actually deleted, rather the word address is changed + to an address that indicates that the word should be considered as deleted */ + set_word_address(sword, DELETED); sword = get_next_word(sword); } @@ -8092,72 +8099,75 @@ void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context) sword_from_active_context = symbolic_memory; // merging the symbolic memory while (sword_from_active_context) { - // check if the word has not already been 'deleted' (note: 'deleted' would mean a virtual address of -1) - if (get_word_address(sword_from_active_context) != (uint64_t) -1) { - sword_from_mergeable_context = get_symbolic_memory(mergeable_context); - - while (sword_from_mergeable_context) { - if (get_word_address(sword_from_active_context) == get_word_address(sword_from_mergeable_context)) { - if (get_word_symbolic(sword_from_active_context) != (char*) 0) { - if (get_word_symbolic(sword_from_mergeable_context) != (char*) 0) { - if (get_word_symbolic(sword_from_active_context) != get_word_symbolic(sword_from_mergeable_context)) { - // merge symbolic values if they are different + // check if the word has not already been deleted + if (get_word_address(sword_from_active_context) != (uint64_t) DELETED) { + // check if the word has not already been merged + if (get_word_address(sword_from_active_context) != (uint64_t) MERGED) { + sword_from_mergeable_context = get_symbolic_memory(mergeable_context); + + while (sword_from_mergeable_context) { + if (get_word_address(sword_from_active_context) == get_word_address(sword_from_mergeable_context)) { + if (get_word_symbolic(sword_from_active_context) != (char*) 0) { + if (get_word_symbolic(sword_from_mergeable_context) != (char*) 0) { + if (get_word_symbolic(sword_from_active_context) != get_word_symbolic(sword_from_mergeable_context)) { + // merge symbolic values if they are different + set_word_symbolic(sword_from_active_context, + smt_ternary("ite", + get_path_condition(active_context), + get_word_symbolic(sword_from_active_context), + get_word_symbolic(sword_from_mergeable_context) + ) + ); + + // indicate that the word has been merged since it does not need to be merged again + set_word_address(sword_from_mergeable_context, MERGED); + } + } else { + // merge symbolic value and concrete value set_word_symbolic(sword_from_active_context, smt_ternary("ite", get_path_condition(active_context), get_word_symbolic(sword_from_active_context), - get_word_symbolic(sword_from_mergeable_context) + bv_constant(get_word_value(sword_from_mergeable_context)) ) ); - // 'delete' the word since it does not need to be merged again - set_word_address(sword_from_mergeable_context, -1); + // indicate that the word has been merged since it does not need to be merged again + set_word_address(sword_from_mergeable_context, MERGED); } } else { - // merge symbolic value and concrete value - set_word_symbolic(sword_from_active_context, - smt_ternary("ite", - get_path_condition(active_context), - get_word_symbolic(sword_from_active_context), - bv_constant(get_word_value(sword_from_mergeable_context)) - ) - ); - - // 'delete' the word since it does not need to be merged again - set_word_address(sword_from_mergeable_context, -1); - } - } else { - if (get_word_symbolic(sword_from_mergeable_context) != (char*) 0) { - // merge concrete value and symbolic value - set_word_symbolic(sword_from_active_context, - smt_ternary("ite", - get_path_condition(active_context), - bv_constant(get_word_value(sword_from_active_context)), - get_word_symbolic(sword_from_mergeable_context) - ) - ); - - // 'delete' the word since it does not need to be merged again - set_word_address(sword_from_mergeable_context, -1); - } else { - if (get_word_value(sword_from_active_context) != get_word_value(sword_from_mergeable_context)) { - // merge concrete values if they are different + if (get_word_symbolic(sword_from_mergeable_context) != (char*) 0) { + // merge concrete value and symbolic value set_word_symbolic(sword_from_active_context, smt_ternary("ite", get_path_condition(active_context), - bv_constant(get_word_value(sword_from_active_context)), - bv_constant(get_word_value(sword_from_mergeable_context)) + bv_constant(get_word_value(sword_from_active_context)), + get_word_symbolic(sword_from_mergeable_context) ) ); - // 'delete' the word since it does not need to be merged again - set_word_address(sword_from_mergeable_context, -1); + // indicate that the word has been merged since it does not need to be merged again + set_word_address(sword_from_mergeable_context, MERGED); + } else { + if (get_word_value(sword_from_active_context) != get_word_value(sword_from_mergeable_context)) { + // merge concrete values if they are different + set_word_symbolic(sword_from_active_context, + smt_ternary("ite", + get_path_condition(active_context), + bv_constant(get_word_value(sword_from_active_context)), + bv_constant(get_word_value(sword_from_mergeable_context)) + ) + ); + + // indicate that the word has been merged since it does not need to be merged again + set_word_address(sword_from_mergeable_context, MERGED); + } } } } - } - sword_from_mergeable_context = get_next_word(sword_from_mergeable_context); + sword_from_mergeable_context = get_next_word(sword_from_mergeable_context); + } } } From d8f5b0a38c36000860774501a10f56f1c53c769e Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Tue, 11 Jun 2019 14:43:15 +0200 Subject: [PATCH 07/21] Program state is restored correctly and clarified comments --- selfie.c | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/selfie.c b/selfie.c index 6b4c9c6a..21813f64 100644 --- a/selfie.c +++ b/selfie.c @@ -7451,7 +7451,7 @@ void constrain_beq() { // check if a context is waiting to be merged if (current_mergeable_context != (uint64_t*) 0) { - // we cannot merge with this one (yet), so we add it back to the stack of mergeable contexts + // we cannot merge with this one (yet), so we push it back onto the stack of mergeable contexts add_mergeable_context(current_mergeable_context); current_mergeable_context = (uint64_t*) 0; } @@ -7933,24 +7933,29 @@ uint64_t find_merge_location(uint64_t beq_imm) { else { if (signed_less_than(imm, 0) == 0) { // jal with positive imm -> end of if with else branch + // (the selfie compiler emits a jal instruction with a positive immediate value if it sees an else branch) // we have to skip the else branch in order to merge afterwards merge_location = pc + imm; pc = original_pc + INSTRUCTIONSIZE; } else // jal with negative imm -> end of loop body - // merge is only outside of the loop possible + // (the selfie compiler emits a jal instruction with a negative immediate value at + // the end of the loop body in order to jump back to the loop condition) + // merge is only outside of the loop body possible merge_location = pc + INSTRUCTIONSIZE; } // we need to check if we are inside of a recursion before we reach the merge location - // if we are, we merge only when the recursion is finished while (pc != merge_location) { fetch(); decode(); if (is == JAL) if (is_start_of_procedure_prologue(pc + imm)) { + // if we are inside of a recursion (nested arbitrarily deep), + // we merge only after the entire recursion has been finished (i.e. the program + // has reached a program location which is not part of any recursion) in_recursion = 1; merge_location = get_merge_location_from_corresponding_prologue_start(pc + imm); } @@ -7961,6 +7966,8 @@ uint64_t find_merge_location(uint64_t beq_imm) { // restore the original program state pc = original_pc; imm = original_imm; + fetch(); + decode(); return merge_location; } From e81a440c4412837e4e1b2516939332e18314a5c4 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Tue, 11 Jun 2019 14:47:47 +0200 Subject: [PATCH 08/21] Removed unnecessary output --- selfie.c | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/selfie.c b/selfie.c index 21813f64..e64917be 100644 --- a/selfie.c +++ b/selfie.c @@ -9426,13 +9426,9 @@ uint64_t handle_timer(uint64_t* context) { set_exception(context, EXCEPTION_NOEXCEPTION); if (symbolic) { - print(";(push 1)\n"); - - printf1(";(assert (not %s)); timeout in ", path_condition); + printf1("; timeout in ", path_condition); print_code_context_for_instruction(pc); - print("\n;(check-sat)\n;(get-model)\n;(pop 1)\n"); - return EXIT; } else return DONOTEXIT; From 19460da3dcf86300576616313e2135cbdd61d669 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Tue, 11 Jun 2019 15:22:23 +0200 Subject: [PATCH 09/21] Fixed a small issue --- selfie.c | 1 + 1 file changed, 1 insertion(+) diff --git a/selfie.c b/selfie.c index e64917be..749a1917 100644 --- a/selfie.c +++ b/selfie.c @@ -9428,6 +9428,7 @@ uint64_t handle_timer(uint64_t* context) { if (symbolic) { printf1("; timeout in ", path_condition); print_code_context_for_instruction(pc); + println(); return EXIT; } else From c14603dac36b4a44d296b6f59066deb69a6bbd49 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Tue, 11 Jun 2019 17:21:37 +0200 Subject: [PATCH 10/21] Simplified and improved handling of recursing --- selfie.c | 114 +++++++++++++++++++++++++------------------------------ 1 file changed, 51 insertions(+), 63 deletions(-) diff --git a/selfie.c b/selfie.c index 749a1917..790bb71b 100644 --- a/selfie.c +++ b/selfie.c @@ -1253,7 +1253,7 @@ uint64_t* get_waiting_context(); void add_prologue_start_and_corresponding_merge_location(uint64_t prologue_start, uint64_t merge_location); uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue_start); -uint64_t is_start_of_procedure_prologue(uint64_t prologue_start); +uint64_t already_called_procedure(uint64_t prologue_start); void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t location); void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context); @@ -1280,13 +1280,12 @@ uint64_t merge_enabled = 1; // enable or disable the merging uint64_t* mergeable_contexts = (uint64_t*) 0; // contexts that have reached their merge location uint64_t* waiting_contexts = (uint64_t*) 0; // contexts that were created at a symbolic beq instruction and are waiting to be executed -uint64_t* prologues_and_corresponding_merge_locations = (uint64_t*) 0; // stack which stores possible function prologues and their corresponding merge locations +uint64_t* prologues_and_corresponding_merge_locations = (uint64_t*) 0; // stack which stores procedure prologues and their corresponding merge locations uint64_t* current_mergeable_context = (uint64_t*) 0; // current context with which the active context can possibly be merged -uint64_t in_recursion = 0; -uint64_t prologue_and_corresponding_merge_location = 0; -uint64_t prologue_start = 0; +uint64_t in_recursion = 0; +uint64_t recursive_merge_location = 0; // ------------------------ GLOBAL CONSTANTS ----------------------- @@ -7927,22 +7926,28 @@ uint64_t find_merge_location(uint64_t beq_imm) { decode(); if (is != JAL) - // no jal instruction -> end of if without else branch - // merge is directly at target location of the beq instruction possible + /* no jal instruction -> end of if without else branch + merge is directly at target location of the beq instruction possible + + note: this is a dependency on the selfie compiler */ merge_location = original_pc + beq_imm; else { if (signed_less_than(imm, 0) == 0) { - // jal with positive imm -> end of if with else branch - // (the selfie compiler emits a jal instruction with a positive immediate value if it sees an else branch) - // we have to skip the else branch in order to merge afterwards + /* jal with positive imm -> end of if with else branch + we have to skip the else branch in order to merge afterwards + + note: this is a dependency on the selfie compiler + the selfie compiler emits a jal instruction with a positive immediate value if it sees an else branch) */ merge_location = pc + imm; pc = original_pc + INSTRUCTIONSIZE; } else - // jal with negative imm -> end of loop body - // (the selfie compiler emits a jal instruction with a negative immediate value at - // the end of the loop body in order to jump back to the loop condition) - // merge is only outside of the loop body possible + /* jal with negative imm -> end of loop body + merge is only outside of the loop body possible + + note: this is a dependency on the selfie compiler + the selfie compiler emits a jal instruction with a negative immediate value at + the end of the loop body in order to jump back to the loop condition */ merge_location = pc + INSTRUCTIONSIZE; } @@ -7952,12 +7957,18 @@ uint64_t find_merge_location(uint64_t beq_imm) { decode(); if (is == JAL) - if (is_start_of_procedure_prologue(pc + imm)) { - // if we are inside of a recursion (nested arbitrarily deep), - // we merge only after the entire recursion has been finished (i.e. the program - // has reached a program location which is not part of any recursion) + // if we are inside of a recursion (nested arbitrarily deep), + // we merge only after the entire recursion has been finished (i.e. the program + // has reached a program location which is not part of any recursion) + if (already_called_procedure(pc + imm)) { + if (in_recursion) + merge_location = recursive_merge_location; + else { + recursive_merge_location = get_merge_location_from_corresponding_prologue_start(pc + imm); + merge_location = recursive_merge_location; + } + in_recursion = 1; - merge_location = get_merge_location_from_corresponding_prologue_start(pc + imm); } pc = pc + INSTRUCTIONSIZE; @@ -8055,7 +8066,7 @@ uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue_ return -1; } -uint64_t is_start_of_procedure_prologue(uint64_t prologue_start) { +uint64_t already_called_procedure(uint64_t prologue_start) { return (get_merge_location_from_corresponding_prologue_start(prologue_start) != (uint64_t) -1); } @@ -8625,8 +8636,10 @@ void execute_debug() { } void execute_symbolically() { - uint64_t pc_after_jal; + uint64_t prologue_start; + uint64_t corresponding_merge_location; uint64_t pc_before_jal; + uint64_t jal_rd; // assert: 1 <= is <= number of RISC-U instructions if (is == ADDI) { @@ -8659,51 +8672,20 @@ void execute_symbolically() { constrain_beq(); else if (is == JAL) { pc_before_jal = pc; - do_jal(); - - pc_after_jal = pc; + jal_rd = rd; - // we need to check if we jump into a recursion - fetch(); - decode(); - - if (is == ADDI) { - pc = pc + INSTRUCTIONSIZE; - fetch(); - decode(); - - if (is == SD) { - pc = pc + INSTRUCTIONSIZE; - fetch(); - decode(); - - if (is == ADDI) { - pc = pc + INSTRUCTIONSIZE; - fetch(); - decode(); - - if (is == SD) { - pc = pc + INSTRUCTIONSIZE; - fetch(); - decode(); - - // note: this check is not completely sufficient to determine a prologue of a procedure - // we would still have to check the registers, however, for the sake of simplicity this has been omitted - // we assume that we have identified a prologue of a procedure - if (is == ADDI) - // if we are already in a recursion, we do not change the merge location since we only merge when the recursion is finished - if (in_recursion == 0) { - prologue_and_corresponding_merge_location = pc_before_jal + 4 * INSTRUCTIONSIZE; - prologue_start = pc_after_jal; - add_prologue_start_and_corresponding_merge_location(prologue_start, prologue_and_corresponding_merge_location); - } - - } - } + do_jal(); + // note: this is a dependency on the selfie compiler + // the selfie compiler uses jal with the RA register to call a procedure + if (jal_rd == REG_RA) + // if we are already in a recursion, we do not add a new merge location since we only merge when the + // recursion is finished (i.e. the program has reached a program location which is not part of any recursion) + if (in_recursion == 0) { + corresponding_merge_location = pc_before_jal + INSTRUCTIONSIZE; + prologue_start = pc; + add_prologue_start_and_corresponding_merge_location(prologue_start, corresponding_merge_location); } - } - pc = pc_after_jal; } else if (is == JALR) { constrain_jalr(); do_jalr(); @@ -8730,6 +8712,12 @@ void interrupt() { } if (symbolic) { + if (in_recursion == 0) + if (prologues_and_corresponding_merge_locations != (uint64_t*) 0) + if (pc == *(prologues_and_corresponding_merge_locations + 2)) + // pop prologue off the stack if we have finished the function + prologues_and_corresponding_merge_locations = (uint64_t*) *(prologues_and_corresponding_merge_locations + 0); + if (current_mergeable_context != (uint64_t*) 0) // if both contexts are at the same program location, they can be merged if (pc == get_pc(current_mergeable_context)) From 0da1e0d822f724f7541dea3f50c19adaee79d75f Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Tue, 11 Jun 2019 18:29:45 +0200 Subject: [PATCH 11/21] Polished some comments and improved recursion handling --- selfie.c | 23 ++++++++++------------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/selfie.c b/selfie.c index 790bb71b..8cc230be 100644 --- a/selfie.c +++ b/selfie.c @@ -1253,7 +1253,7 @@ uint64_t* get_waiting_context(); void add_prologue_start_and_corresponding_merge_location(uint64_t prologue_start, uint64_t merge_location); uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue_start); -uint64_t already_called_procedure(uint64_t prologue_start); +uint64_t currently_in_this_procedure(uint64_t prologue_start); void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t location); void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context); @@ -7801,7 +7801,7 @@ void delete_word_from_symbolic_memory(uint64_t vaddr) { while (sword) { if (get_word_address(sword) == vaddr) /* we indicate that this word has been deleted in order to avoid finding - outdated values when searching the symbolic memory later on + outdated values when searching the symbolic memory note: the word is not actually deleted, rather the word address is changed to an address that indicates that the word should be considered as deleted */ @@ -7937,7 +7937,7 @@ uint64_t find_merge_location(uint64_t beq_imm) { we have to skip the else branch in order to merge afterwards note: this is a dependency on the selfie compiler - the selfie compiler emits a jal instruction with a positive immediate value if it sees an else branch) */ + the selfie compiler emits a jal instruction with a positive immediate value if it sees an else branch */ merge_location = pc + imm; pc = original_pc + INSTRUCTIONSIZE; @@ -7957,17 +7957,14 @@ uint64_t find_merge_location(uint64_t beq_imm) { decode(); if (is == JAL) - // if we are inside of a recursion (nested arbitrarily deep), + // if we are inside of a (arbitrarily deep nested) recursion, // we merge only after the entire recursion has been finished (i.e. the program // has reached a program location which is not part of any recursion) - if (already_called_procedure(pc + imm)) { - if (in_recursion) - merge_location = recursive_merge_location; - else { + if (currently_in_this_procedure(pc + imm)) { + if (in_recursion == 0) recursive_merge_location = get_merge_location_from_corresponding_prologue_start(pc + imm); - merge_location = recursive_merge_location; - } + merge_location = recursive_merge_location; in_recursion = 1; } @@ -8066,7 +8063,7 @@ uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue_ return -1; } -uint64_t already_called_procedure(uint64_t prologue_start) { +uint64_t currently_in_this_procedure(uint64_t prologue_start) { return (get_merge_location_from_corresponding_prologue_start(prologue_start) != (uint64_t) -1); } @@ -8087,7 +8084,7 @@ void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t locat if (prologues_and_corresponding_merge_locations != (uint64_t*) 0) if (get_pc(active_context) == *(prologues_and_corresponding_merge_locations + 2)) - // we have finished the recursion + // we have finished the recursion (i.e. the program has reached a program location which is not part of any recursion) in_recursion = 0; // merging the symbolic store @@ -8715,7 +8712,7 @@ void interrupt() { if (in_recursion == 0) if (prologues_and_corresponding_merge_locations != (uint64_t*) 0) if (pc == *(prologues_and_corresponding_merge_locations + 2)) - // pop prologue off the stack if we have finished the function + // pop prologue off the stack if we have finished the procedure prologues_and_corresponding_merge_locations = (uint64_t*) *(prologues_and_corresponding_merge_locations + 0); if (current_mergeable_context != (uint64_t*) 0) From fd9dafd9bc88a6de51714fa47d485af02b496720 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Thu, 13 Jun 2019 21:42:21 +0200 Subject: [PATCH 12/21] Polished some comments and removed unnecessary variable --- selfie.c | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/selfie.c b/selfie.c index 8cc230be..2784408c 100644 --- a/selfie.c +++ b/selfie.c @@ -7736,7 +7736,7 @@ void store_symbolic_memory(uint64_t vaddr, uint64_t val, char* sym, char* var, u sword = allocate_symbolic_memory_word(); - // we 'delete' the word, if it already exists in the symbolic memory + // we mark the word as deleted, if it already exists in the symbolic memory delete_word_from_symbolic_memory(vaddr); set_next_word(sword, symbolic_memory); @@ -7800,7 +7800,7 @@ void delete_word_from_symbolic_memory(uint64_t vaddr) { while (sword) { if (get_word_address(sword) == vaddr) - /* we indicate that this word has been deleted in order to avoid finding + /* we mark this word as deleted in order to avoid finding outdated values when searching the symbolic memory note: the word is not actually deleted, rather the word address is changed @@ -7911,12 +7911,10 @@ char* smt_ternary(char* opt, char* op1, char* op2, char* op3) { uint64_t find_merge_location(uint64_t beq_imm) { uint64_t original_pc; - uint64_t original_imm; uint64_t merge_location; // assert: the current instruction is a symbolic beq instruction original_pc = pc; - original_imm = imm; // examine last instruction before target location of the beq instruction pc = pc + (beq_imm - INSTRUCTIONSIZE); @@ -7973,7 +7971,6 @@ uint64_t find_merge_location(uint64_t beq_imm) { // restore the original program state pc = original_pc; - imm = original_imm; fetch(); decode(); @@ -8134,7 +8131,7 @@ void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context) ) ); - // indicate that the word has been merged since it does not need to be merged again + // we mark the word as merged since it does not need to be merged again set_word_address(sword_from_mergeable_context, MERGED); } } else { @@ -8147,7 +8144,7 @@ void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context) ) ); - // indicate that the word has been merged since it does not need to be merged again + // we mark the word as merged since it does not need to be merged again set_word_address(sword_from_mergeable_context, MERGED); } } else { @@ -8161,7 +8158,7 @@ void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context) ) ); - // indicate that the word has been merged since it does not need to be merged again + // we mark the word as merged since it does not need to be merged again set_word_address(sword_from_mergeable_context, MERGED); } else { if (get_word_value(sword_from_active_context) != get_word_value(sword_from_mergeable_context)) { @@ -8174,7 +8171,7 @@ void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context) ) ); - // indicate that the word has been merged since it does not need to be merged again + // we mark the word as merged since it does not need to be merged again set_word_address(sword_from_mergeable_context, MERGED); } } From cf7a50842bfefc8389a7efd9c9306f7cd6a68c71 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Thu, 13 Jun 2019 22:11:58 +0200 Subject: [PATCH 13/21] Improved recursion handling --- selfie.c | 69 ++++++++++++++++++++++++++++++++------------------------ 1 file changed, 39 insertions(+), 30 deletions(-) diff --git a/selfie.c b/selfie.c index 2784408c..a57b6c0d 100644 --- a/selfie.c +++ b/selfie.c @@ -1251,9 +1251,9 @@ uint64_t* get_mergeable_context(); void add_waiting_context(uint64_t* context); uint64_t* get_waiting_context(); -void add_prologue_start_and_corresponding_merge_location(uint64_t prologue_start, uint64_t merge_location); -uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue_start); -uint64_t currently_in_this_procedure(uint64_t prologue_start); +void add_prologue_start_and_corresponding_merge_location(uint64_t prologue_start, uint64_t merge_location, uint64_t* context); +uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue_start, uint64_t* context); +uint64_t currently_in_this_procedure(uint64_t prologue_start, uint64_t* context); void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t location); void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context); @@ -1280,13 +1280,9 @@ uint64_t merge_enabled = 1; // enable or disable the merging uint64_t* mergeable_contexts = (uint64_t*) 0; // contexts that have reached their merge location uint64_t* waiting_contexts = (uint64_t*) 0; // contexts that were created at a symbolic beq instruction and are waiting to be executed -uint64_t* prologues_and_corresponding_merge_locations = (uint64_t*) 0; // stack which stores procedure prologues and their corresponding merge locations uint64_t* current_mergeable_context = (uint64_t*) 0; // current context with which the active context can possibly be merged -uint64_t in_recursion = 0; -uint64_t recursive_merge_location = 0; - // ------------------------ GLOBAL CONSTANTS ----------------------- uint64_t DELETED = -1; // indicates that a symbolic memory word has been deleted @@ -1505,6 +1501,9 @@ uint64_t* delete_context(uint64_t* context, uint64_t* from); // | 19 | symbolic regs | pointer to symbolic registers // | 20 | beq counter | number of executed symbolic beq instructions // | 21 | merge location | program location at which the context can possibly be merged (later) +// | 22 | prologues | pointer to a stack that stores the prologues of procedures within which the context is currently located +// | 23 | in recursion | if the value is 1, then the context is currently in a recursion +// | 24 | outside rec loc | program location at which the context has finished the recursion // +----+-----------------+ uint64_t* allocate_context() { @@ -1512,7 +1511,7 @@ uint64_t* allocate_context() { } uint64_t* allocate_symbolic_context() { - return smalloc(7 * SIZEOFUINT64STAR + 9 * SIZEOFUINT64 + 3 * SIZEOFUINT64STAR + 3 * SIZEOFUINT64); + return smalloc(7 * SIZEOFUINT64STAR + 9 * SIZEOFUINT64 + 4 * SIZEOFUINT64STAR + 5 * SIZEOFUINT64); } uint64_t next_context(uint64_t* context) { return (uint64_t) context; } @@ -1555,6 +1554,9 @@ uint64_t* get_symbolic_memory(uint64_t* context) { return (uint64_t*) *(context uint64_t* get_symbolic_regs(uint64_t* context) { return (uint64_t*) *(context + 19); } uint64_t get_beq_counter(uint64_t* context) { return *(context + 20); } uint64_t get_merge_location(uint64_t* context) { return *(context + 21); } +uint64_t* get_prologues(uint64_t* context) { return (uint64_t*) *(context + 22); } +uint64_t get_in_recursion(uint64_t* context) { return *(context + 23); } +uint64_t get_outside_rec_loc(uint64_t* context) { return *(context + 24); } void set_next_context(uint64_t* context, uint64_t* next) { *context = (uint64_t) next; } void set_prev_context(uint64_t* context, uint64_t* prev) { *(context + 1) = (uint64_t) prev; } @@ -1579,6 +1581,9 @@ void set_symbolic_memory(uint64_t* context, uint64_t* memory) { *(context + 18) void set_symbolic_regs(uint64_t* context, uint64_t* regs) { *(context + 19) = (uint64_t) regs; } void set_beq_counter(uint64_t* context, uint64_t counter) { *(context + 20) = counter; } void set_merge_location(uint64_t* context, uint64_t location) { *(context + 21) = location; } +void set_prologues(uint64_t* context, uint64_t* prologues) { *(context + 22) = (uint64_t) prologues; } +void set_in_recursion(uint64_t* context, uint64_t in_rec) { *(context + 23) = in_rec; } +void set_outside_rec_loc(uint64_t* context, uint64_t location) { *(context + 24) = location; } // ----------------------------------------------------------------- // -------------------------- MICROKERNEL -------------------------- @@ -7958,12 +7963,12 @@ uint64_t find_merge_location(uint64_t beq_imm) { // if we are inside of a (arbitrarily deep nested) recursion, // we merge only after the entire recursion has been finished (i.e. the program // has reached a program location which is not part of any recursion) - if (currently_in_this_procedure(pc + imm)) { - if (in_recursion == 0) - recursive_merge_location = get_merge_location_from_corresponding_prologue_start(pc + imm); + if (currently_in_this_procedure(pc + imm, current_context)) { + if (get_in_recursion(current_context) == 0) + set_outside_rec_loc(current_context, get_merge_location_from_corresponding_prologue_start(pc + imm, current_context)); - merge_location = recursive_merge_location; - in_recursion = 1; + merge_location = get_outside_rec_loc(current_context); + set_in_recursion(current_context, 1); } pc = pc + INSTRUCTIONSIZE; @@ -8023,10 +8028,10 @@ uint64_t* get_waiting_context() { return (uint64_t*) *(head + 1); } -void add_prologue_start_and_corresponding_merge_location(uint64_t prologue_start, uint64_t merge_location) { +void add_prologue_start_and_corresponding_merge_location(uint64_t prologue_start, uint64_t merge_location, uint64_t* context) { uint64_t* entry; - entry = prologues_and_corresponding_merge_locations; + entry = get_prologues(context); // do not add duplicates while (entry) { @@ -8038,17 +8043,17 @@ void add_prologue_start_and_corresponding_merge_location(uint64_t prologue_start entry = smalloc(3 * SIZEOFUINT64STAR); - *(entry + 0) = (uint64_t) prologues_and_corresponding_merge_locations; + *(entry + 0) = (uint64_t) get_prologues(context); *(entry + 1) = (uint64_t) prologue_start; *(entry + 2) = (uint64_t) merge_location; - prologues_and_corresponding_merge_locations = entry; + set_prologues(context, entry); } -uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue_start) { +uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue_start, uint64_t* context) { uint64_t* entry; - entry = prologues_and_corresponding_merge_locations; + entry = get_prologues(context); while (entry) { if (*(entry + 1) == prologue_start) @@ -8060,8 +8065,8 @@ uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue_ return -1; } -uint64_t currently_in_this_procedure(uint64_t prologue_start) { - return (get_merge_location_from_corresponding_prologue_start(prologue_start) != (uint64_t) -1); +uint64_t currently_in_this_procedure(uint64_t prologue_start, uint64_t* context) { + return (get_merge_location_from_corresponding_prologue_start(prologue_start, context) != (uint64_t) -1); } void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t location) { @@ -8079,10 +8084,10 @@ void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t locat print_code_context_for_instruction(location); println(); - if (prologues_and_corresponding_merge_locations != (uint64_t*) 0) - if (get_pc(active_context) == *(prologues_and_corresponding_merge_locations + 2)) + if (get_prologues(active_context) != (uint64_t*) 0) + if (get_pc(active_context) == *(get_prologues(active_context) + 2)) // we have finished the recursion (i.e. the program has reached a program location which is not part of any recursion) - in_recursion = 0; + set_in_recursion(active_context, 0); // merging the symbolic store merge_symbolic_store(active_context, mergeable_context); @@ -8674,10 +8679,10 @@ void execute_symbolically() { if (jal_rd == REG_RA) // if we are already in a recursion, we do not add a new merge location since we only merge when the // recursion is finished (i.e. the program has reached a program location which is not part of any recursion) - if (in_recursion == 0) { + if (get_in_recursion(current_context) == 0) { corresponding_merge_location = pc_before_jal + INSTRUCTIONSIZE; prologue_start = pc; - add_prologue_start_and_corresponding_merge_location(prologue_start, corresponding_merge_location); + add_prologue_start_and_corresponding_merge_location(prologue_start, corresponding_merge_location, current_context); } } else if (is == JALR) { @@ -8706,11 +8711,11 @@ void interrupt() { } if (symbolic) { - if (in_recursion == 0) - if (prologues_and_corresponding_merge_locations != (uint64_t*) 0) - if (pc == *(prologues_and_corresponding_merge_locations + 2)) + if (get_in_recursion(current_context) == 0) + if (get_prologues(current_context) != (uint64_t*) 0) + if (pc == *(get_prologues(current_context) + 2)) // pop prologue off the stack if we have finished the procedure - prologues_and_corresponding_merge_locations = (uint64_t*) *(prologues_and_corresponding_merge_locations + 0); + set_prologues(current_context, (uint64_t*) *(get_prologues(current_context) + 0)); if (current_mergeable_context != (uint64_t*) 0) // if both contexts are at the same program location, they can be merged @@ -8929,6 +8934,10 @@ uint64_t* copy_context(uint64_t* original, uint64_t location, char* condition, u copy_symbolic_memory(original, context); + set_prologues(context, get_prologues(original)); + set_in_recursion(context, get_in_recursion(original)); + set_outside_rec_loc(context, get_outside_rec_loc(original)); + set_symbolic_regs(context, smalloc(NUMBEROFREGISTERS * REGISTERSIZE)); r = 0; From fda20f64e3e27bb0170d26939a05fa9a1448d973 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Fri, 14 Jun 2019 20:34:30 +0200 Subject: [PATCH 14/21] Implemented check for division by zero --- selfie.c | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/selfie.c b/selfie.c index a57b6c0d..497acf85 100644 --- a/selfie.c +++ b/selfie.c @@ -7020,6 +7020,13 @@ void constrain_add_sub_mul_divu_remu_sltu(char* operator) { op2 = bv_constant(*(registers + rs2)); *(reg_sym + rd) = (uint64_t) smt_binary(operator, op1, op2); + + // checking for division by zero + if (string_compare(operator, "bvudiv")) { + print("(push 1)\n"); + printf2("(assert (and %s %s)); check if a division by zero is possible", path_condition, smt_binary("=", op2, bv_constant(0))); + print("\n(check-sat)\n(get-model)\n(pop 1)\n"); + } } } @@ -9404,6 +9411,16 @@ uint64_t handle_division_by_zero(uint64_t* context) { replay_trace(); set_exit_code(context, EXITCODE_NOERROR); + } else if (symbolic) { + // check if this division by zero is reachable + print("(push 1)\n"); + printf1("(assert %s); divison-by-zero error detected; check if this division by zero is reachable", path_condition); + print("\n(check-sat)\n(get-model)\n(pop 1)\n"); + + // we terminate the exeuction of the context, because if the location is not reachable, + // the rest of the path is not reachable either, and otherwise + // the execution would be terminated by this error anyway + set_exit_code(context, EXITCODE_DIVISIONBYZERO); } else { printf1("%s: division by zero\n", selfie_name); From a4a8cda07a80fdd2e129cd5555c348dd722c04e7 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Sat, 15 Jun 2019 11:57:59 +0200 Subject: [PATCH 15/21] Fixed a spelling mistake --- selfie.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/selfie.c b/selfie.c index 497acf85..ca948581 100644 --- a/selfie.c +++ b/selfie.c @@ -9414,7 +9414,7 @@ uint64_t handle_division_by_zero(uint64_t* context) { } else if (symbolic) { // check if this division by zero is reachable print("(push 1)\n"); - printf1("(assert %s); divison-by-zero error detected; check if this division by zero is reachable", path_condition); + printf1("(assert %s); division by zero detected; check if this division by zero is reachable", path_condition); print("\n(check-sat)\n(get-model)\n(pop 1)\n"); // we terminate the exeuction of the context, because if the location is not reachable, From 852d692697d72e9d657f6edf9f9e35a6c7ef1a5e Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Sat, 15 Jun 2019 12:07:26 +0200 Subject: [PATCH 16/21] Implemented check for invalid memory access --- selfie.c | 37 +++++++++++++++++++------------------ 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/selfie.c b/selfie.c index ca948581..de47c208 100644 --- a/selfie.c +++ b/selfie.c @@ -7234,16 +7234,9 @@ void constrain_ld() { // and individually *(loads_per_instruction + a) = *(loads_per_instruction + a) + 1; - } else { + } else // invalid concrete memory address - printf3("%s: invalid concrete memory address %x in ld instruction at %x", selfie_name, - (char*) vaddr, - (char*) pc); - print_code_line_number_for_instruction(pc, entry_point); - println(); - - exit(EXITCODE_SYMBOLICEXECUTIONERROR); - } + throw_exception(EXCEPTION_INVALIDADDRESS, vaddr); } void print_sd() { @@ -7366,16 +7359,9 @@ void constrain_sd() { // and individually *(stores_per_instruction + a) = *(stores_per_instruction + a) + 1; - } else { + } else // invalid concrete memory address - printf3("%s: invalid concrete memory address %x in sd instruction at %x", selfie_name, - (char*) vaddr, - (char*) pc); - print_code_line_number_for_instruction(pc, entry_point); - println(); - - exit(EXITCODE_SYMBOLICEXECUTIONERROR); - } + throw_exception(EXCEPTION_INVALIDADDRESS, vaddr); } void print_beq() { @@ -9467,6 +9453,21 @@ uint64_t handle_exception(uint64_t* context) { else if (exception == EXCEPTION_MERGE) return handle_merge(context); else { + if (symbolic) + if (exception == EXCEPTION_INVALIDADDRESS) { + // check if this invalid memory access is reachable + print("(push 1)\n"); + printf1("(assert %s); invalid memory access detected; check if this invalid memory access is reachable", path_condition); + print("\n(check-sat)\n(get-model)\n(pop 1)\n"); + + set_exit_code(context, EXITCODE_SYMBOLICEXECUTIONERROR); + + // we terminate the exeuction of the context, because if the location is not reachable, + // the rest of the path is not reachable either, and otherwise + // the execution would be terminated by this error anyway + return EXIT; + } + printf2("%s: context %s throws uncaught ", selfie_name, get_name(context)); print_exception(exception, get_faulting_page(context)); println(); From c41b6dac77ef692504bc4758cb5060fcdaec19f5 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Sat, 15 Jun 2019 12:35:17 +0200 Subject: [PATCH 17/21] Removed disabling of merging for large path conditions --- selfie.c | 4 ---- 1 file changed, 4 deletions(-) diff --git a/selfie.c b/selfie.c index de47c208..396107ed 100644 --- a/selfie.c +++ b/selfie.c @@ -8085,10 +8085,6 @@ void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t locat // merging the symbolic store merge_symbolic_store(active_context, mergeable_context); - // disable merging if the path condition becomes too large - if (string_length(smt_binary("or", get_path_condition(active_context), get_path_condition(mergeable_context))) > MAX_PATH_CONDITION_LENGTH) - merge_enabled = 0; - // merging the path condition path_condition = smt_binary("or", get_path_condition(active_context), get_path_condition(mergeable_context)); set_path_condition(active_context, path_condition); From 357aa7cdfc22ed0db2f5033d3ac1b801d0ffa08d Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Thu, 20 Jun 2019 12:54:31 +0200 Subject: [PATCH 18/21] Implemented (partially) shared symbolic memory --- selfie.c | 382 +++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 316 insertions(+), 66 deletions(-) diff --git a/selfie.c b/selfie.c index 396107ed..d1b5f327 100644 --- a/selfie.c +++ b/selfie.c @@ -1196,8 +1196,8 @@ void init_replay_engine() { uint64_t* load_symbolic_memory(uint64_t vaddr); void store_symbolic_memory(uint64_t vaddr, uint64_t val, char* sym, char* var, uint64_t bits); -void copy_symbolic_memory(uint64_t* from_context, uint64_t* to_context); -void delete_word_from_symbolic_memory(uint64_t vaddr); +uint64_t* find_word_in_unshared_symbolic_memory(uint64_t vaddr); +void update_begin_of_shared_symbolic_memory(uint64_t* context); uint64_t is_symbolic_value(uint64_t* sword); @@ -1256,7 +1256,10 @@ uint64_t get_merge_location_from_corresponding_prologue_start(uint64_t prologue uint64_t currently_in_this_procedure(uint64_t prologue_start, uint64_t* context); void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t location); -void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context); +void merge_symbolic_memory_and_registers(uint64_t* active_context, uint64_t* mergeable_context); +void merge_symbolic_memory_of_active_context(uint64_t* active_context, uint64_t* mergeable_context); +void merge_symbolic_memory_of_mergeable_context(uint64_t* active_context, uint64_t* mergeable_context); +void merge_registers(uint64_t* active_context, uint64_t* mergeable_context); uint64_t* merge_if_possible_and_get_next_context(uint64_t* context); // ------------------------ GLOBAL VARIABLES ----------------------- @@ -1285,8 +1288,9 @@ uint64_t* current_mergeable_context = (uint64_t*) 0; // curren // ------------------------ GLOBAL CONSTANTS ----------------------- -uint64_t DELETED = -1; // indicates that a symbolic memory word has been deleted -uint64_t MERGED = -2; // indicates that a symbolic memory word has been merged +uint64_t DELETED = -1; // indicates that a symbolic memory word has been deleted +uint64_t MERGED = -2; // indicates that a symbolic memory word has been merged +uint64_t BEGIN_OF_SHARED_SYMBOLIC_MEMORY = -3; // indicates the begin of the shared symbolic memory space uint64_t BEQ_LIMIT = 35; // limit of symbolic beq instructions on any given path uint64_t MAX_PATH_CONDITION_LENGTH = 1000000; @@ -1504,6 +1508,7 @@ uint64_t* delete_context(uint64_t* context, uint64_t* from); // | 22 | prologues | pointer to a stack that stores the prologues of procedures within which the context is currently located // | 23 | in recursion | if the value is 1, then the context is currently in a recursion // | 24 | outside rec loc | program location at which the context has finished the recursion +// | 25 | merge partner | pointer to the context from which this context was created // +----+-----------------+ uint64_t* allocate_context() { @@ -1511,7 +1516,7 @@ uint64_t* allocate_context() { } uint64_t* allocate_symbolic_context() { - return smalloc(7 * SIZEOFUINT64STAR + 9 * SIZEOFUINT64 + 4 * SIZEOFUINT64STAR + 5 * SIZEOFUINT64); + return smalloc(7 * SIZEOFUINT64STAR + 9 * SIZEOFUINT64 + 5 * SIZEOFUINT64STAR + 5 * SIZEOFUINT64); } uint64_t next_context(uint64_t* context) { return (uint64_t) context; } @@ -1557,6 +1562,7 @@ uint64_t get_merge_location(uint64_t* context) { return *(context uint64_t* get_prologues(uint64_t* context) { return (uint64_t*) *(context + 22); } uint64_t get_in_recursion(uint64_t* context) { return *(context + 23); } uint64_t get_outside_rec_loc(uint64_t* context) { return *(context + 24); } +uint64_t* get_merge_partner(uint64_t* context) { return (uint64_t*) *(context + 25); } void set_next_context(uint64_t* context, uint64_t* next) { *context = (uint64_t) next; } void set_prev_context(uint64_t* context, uint64_t* prev) { *(context + 1) = (uint64_t) prev; } @@ -1584,6 +1590,7 @@ void set_merge_location(uint64_t* context, uint64_t location) { *(context + 21) void set_prologues(uint64_t* context, uint64_t* prologues) { *(context + 22) = (uint64_t) prologues; } void set_in_recursion(uint64_t* context, uint64_t in_rec) { *(context + 23) = in_rec; } void set_outside_rec_loc(uint64_t* context, uint64_t location) { *(context + 24) = location; } +void set_merge_partner(uint64_t* context, uint64_t* partner) { *(context + 25) = (uint64_t) partner; } // ----------------------------------------------------------------- // -------------------------- MICROKERNEL -------------------------- @@ -7732,12 +7739,16 @@ uint64_t* load_symbolic_memory(uint64_t vaddr) { void store_symbolic_memory(uint64_t vaddr, uint64_t val, char* sym, char* var, uint64_t bits) { uint64_t* sword; - sword = allocate_symbolic_memory_word(); + // we overwrite values, if they already exist in the unshared symbolic memory space, so that there are no duplicates in any unshared symbolic memory space + sword = find_word_in_unshared_symbolic_memory(vaddr); - // we mark the word as deleted, if it already exists in the symbolic memory - delete_word_from_symbolic_memory(vaddr); + // new value in this unshared symbolic memory space + if (sword == (uint64_t*) 0) { + sword = allocate_symbolic_memory_word(); + set_next_word(sword, symbolic_memory); + symbolic_memory = sword; + } - set_next_word(sword, symbolic_memory); set_word_address(sword, vaddr); set_word_value(sword, val); @@ -7753,57 +7764,38 @@ void store_symbolic_memory(uint64_t vaddr, uint64_t val, char* sym, char* var, u set_word_symbolic(sword, 0); set_number_of_bits(sword, bits); - - symbolic_memory = sword; } -void copy_symbolic_memory(uint64_t* from_context, uint64_t* to_context) { +uint64_t* find_word_in_unshared_symbolic_memory(uint64_t vaddr) { uint64_t* sword; - uint64_t* sword_copy; - uint64_t* symbolic_memory_copy; - uint64_t* previous; - - sword = get_symbolic_memory(from_context); - sword_copy = (uint64_t*) 0; - symbolic_memory_copy = (uint64_t*) 0; - previous = (uint64_t*) 0; + sword = get_symbolic_memory(current_context); while (sword) { - sword_copy = allocate_symbolic_memory_word(); - - set_word_address(sword_copy, get_word_address(sword)); - set_word_value(sword_copy, get_word_value(sword)); - set_word_symbolic(sword_copy, get_word_symbolic(sword)); - set_number_of_bits(sword_copy, get_number_of_bits(sword)); - - if (previous != (uint64_t*) 0) - set_next_word(previous, sword_copy); - - if (symbolic_memory_copy == (uint64_t*) 0) - symbolic_memory_copy = sword_copy; + if (get_word_address(sword) == BEGIN_OF_SHARED_SYMBOLIC_MEMORY) + return (uint64_t*) 0; + if (get_word_address(sword) == vaddr) + return sword; - previous = sword_copy; sword = get_next_word(sword); } - set_next_word(sword_copy, 0); - set_symbolic_memory(to_context, symbolic_memory_copy); + return (uint64_t*) 0; } -void delete_word_from_symbolic_memory(uint64_t vaddr) { +void update_begin_of_shared_symbolic_memory(uint64_t* context) { uint64_t* sword; - sword = symbolic_memory; + if (context == (uint64_t*) 0) + return; - while (sword) { - if (get_word_address(sword) == vaddr) - /* we mark this word as deleted in order to avoid finding - outdated values when searching the symbolic memory + sword = get_symbolic_memory(context); - note: the word is not actually deleted, rather the word address is changed - to an address that indicates that the word should be considered as deleted */ + while (sword) { + if (get_word_address(sword) == BEGIN_OF_SHARED_SYMBOLIC_MEMORY) { set_word_address(sword, DELETED); + return; + } sword = get_next_word(sword); } @@ -8083,35 +8075,60 @@ void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t locat set_in_recursion(active_context, 0); // merging the symbolic store - merge_symbolic_store(active_context, mergeable_context); + merge_symbolic_memory_and_registers(active_context, mergeable_context); // merging the path condition path_condition = smt_binary("or", get_path_condition(active_context), get_path_condition(mergeable_context)); set_path_condition(active_context, path_condition); + if (get_execution_depth(mergeable_context) > get_execution_depth(active_context)) + set_execution_depth(active_context, get_execution_depth(mergeable_context)); + current_mergeable_context = get_mergeable_context(); // it may be possible that more contexts can be merged if (current_mergeable_context != (uint64_t*) 0) if (pc == get_pc(current_mergeable_context)) merge(active_context, current_mergeable_context, pc); + +} + +void merge_symbolic_memory_and_registers(uint64_t* active_context, uint64_t* mergeable_context) { + // merging the symbolic memory + merge_symbolic_memory_of_active_context(active_context, mergeable_context); + merge_symbolic_memory_of_mergeable_context(active_context, mergeable_context); + + // merging the registers + merge_registers(active_context, mergeable_context); + + // the shared symbolic memory space needs needs to be updated since the other context was merged into the active context + update_begin_of_shared_symbolic_memory(active_context); } -void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context) { +void merge_symbolic_memory_of_active_context(uint64_t* active_context, uint64_t* mergeable_context) { uint64_t* sword_from_active_context; uint64_t* sword_from_mergeable_context; - uint64_t i; + uint64_t in_unshared_symbolic_memory; sword_from_active_context = symbolic_memory; - // merging the symbolic memory + while (sword_from_active_context) { + // we need to stop at the end of the unshared symbolic memory space of the active context + if (get_word_address(sword_from_active_context) == BEGIN_OF_SHARED_SYMBOLIC_MEMORY) + return; + // check if the word has not already been deleted if (get_word_address(sword_from_active_context) != (uint64_t) DELETED) { - // check if the word has not already been merged + // check if the word has not already been merged if (get_word_address(sword_from_active_context) != (uint64_t) MERGED) { sword_from_mergeable_context = get_symbolic_memory(mergeable_context); + in_unshared_symbolic_memory = 1; while (sword_from_mergeable_context) { + // we need to know if we are in the unshared symbolic memory space of the mergeable context + if (get_word_address(sword_from_mergeable_context) == BEGIN_OF_SHARED_SYMBOLIC_MEMORY) + in_unshared_symbolic_memory = 0; + if (get_word_address(sword_from_active_context) == get_word_address(sword_from_mergeable_context)) { if (get_word_symbolic(sword_from_active_context) != (char*) 0) { if (get_word_symbolic(sword_from_mergeable_context) != (char*) 0) { @@ -8125,8 +8142,12 @@ void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context) ) ); - // we mark the word as merged since it does not need to be merged again - set_word_address(sword_from_mergeable_context, MERGED); + // we mark the word as merged so that we do not merge it again when merging from the side of the mergeable context + if (in_unshared_symbolic_memory) + set_word_address(sword_from_mergeable_context, MERGED); + + // we need to break out of the loop + sword_from_mergeable_context = (uint64_t*) - 1; } } else { // merge symbolic value and concrete value @@ -8138,8 +8159,12 @@ void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context) ) ); - // we mark the word as merged since it does not need to be merged again - set_word_address(sword_from_mergeable_context, MERGED); + // we mark the word as merged so that we do not merge it again when merging from the side of the mergeable context + if (in_unshared_symbolic_memory) + set_word_address(sword_from_mergeable_context, MERGED); + + // we need to break out of the loop + sword_from_mergeable_context = (uint64_t*) - 1; } } else { if (get_word_symbolic(sword_from_mergeable_context) != (char*) 0) { @@ -8152,8 +8177,12 @@ void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context) ) ); - // we mark the word as merged since it does not need to be merged again - set_word_address(sword_from_mergeable_context, MERGED); + // we mark the word as merged so that we do not merge it again when merging from the side of the mergeable context + if (in_unshared_symbolic_memory) + set_word_address(sword_from_mergeable_context, MERGED); + + // we need to break out of the loop + sword_from_mergeable_context = (uint64_t*) - 1; } else { if (get_word_value(sword_from_active_context) != get_word_value(sword_from_mergeable_context)) { // merge concrete values if they are different @@ -8165,26 +8194,208 @@ void merge_symbolic_store(uint64_t* active_context, uint64_t* mergeable_context) ) ); - // we mark the word as merged since it does not need to be merged again - set_word_address(sword_from_mergeable_context, MERGED); + // we mark the word as merged so that we do not merge it again when merging from the side of the mergeable context + if (in_unshared_symbolic_memory) + set_word_address(sword_from_mergeable_context, MERGED); + + // we need to break out of the loop + sword_from_mergeable_context = (uint64_t*) - 1; } } } } - - sword_from_mergeable_context = get_next_word(sword_from_mergeable_context); + if (sword_from_mergeable_context == (uint64_t*) - 1) + sword_from_mergeable_context = (uint64_t*) 0; + else + sword_from_mergeable_context = get_next_word(sword_from_mergeable_context); } } } sword_from_active_context = get_next_word(sword_from_active_context); } +} + +void merge_symbolic_memory_of_mergeable_context(uint64_t* active_context, uint64_t* mergeable_context) { + uint64_t* sword_from_active_context; + uint64_t* sword_from_mergeable_context; + uint64_t* sword; + uint64_t* additional_memory; + uint64_t shared_symbolic_memory_depth; + + additional_memory = symbolic_memory; + sword_from_mergeable_context = get_symbolic_memory(mergeable_context); + + while (sword_from_mergeable_context) { + // we need to stop at the end of the unshared symbolic memory space of the mergeable context + if (get_word_address(sword_from_mergeable_context) == BEGIN_OF_SHARED_SYMBOLIC_MEMORY) { + symbolic_memory = additional_memory; + + // the active context contains now the merged symbolic memory + set_symbolic_memory(active_context, symbolic_memory); + return; + } + + // check if the word has not already been deleted + if (get_word_address(sword_from_mergeable_context) != (uint64_t) DELETED) { + // check if the word has not already been merged + if (get_word_address(sword_from_mergeable_context) != (uint64_t) MERGED) { + sword_from_active_context = symbolic_memory; + shared_symbolic_memory_depth = 0; + + while (sword_from_active_context) { + // we need to know how far we are into the shared symbolic memory space + if (get_word_address(sword_from_active_context) == (uint64_t) BEGIN_OF_SHARED_SYMBOLIC_MEMORY) + shared_symbolic_memory_depth = shared_symbolic_memory_depth + 1; + + if (get_word_address(sword_from_active_context) == get_word_address(sword_from_mergeable_context)) { + if (get_word_symbolic(sword_from_active_context) != (char*) 0) { + if (get_word_symbolic(sword_from_mergeable_context) != (char*) 0) { + if (get_word_symbolic(sword_from_active_context) != get_word_symbolic(sword_from_mergeable_context)) { + // merge symbolic values if they are different + if (shared_symbolic_memory_depth < 2) + set_word_symbolic(sword_from_active_context, + smt_ternary("ite", + get_path_condition(active_context), + get_word_symbolic(sword_from_active_context), + get_word_symbolic(sword_from_mergeable_context) + ) + ); + else { + // if we are too far into the shared symbolic memory space, we must not overwrite the value, + // but insert it into the unshared symbolic memory space of the active context + sword = allocate_symbolic_memory_word(); + set_word_address(sword, get_word_address(sword_from_active_context)); + set_word_value(sword, get_word_value(sword_from_active_context)); + set_number_of_bits(sword, get_number_of_bits(sword_from_active_context)); + set_word_symbolic(sword, + smt_ternary("ite", + get_path_condition(active_context), + get_word_symbolic(sword_from_active_context), + get_word_symbolic(sword_from_mergeable_context) + ) + ); + set_next_word(sword, additional_memory); + } + + // we need to break out of the loop + sword_from_active_context = (uint64_t*) - 1; + } + } else { + // merge symbolic value and concrete value + if (shared_symbolic_memory_depth < 2) + set_word_symbolic(sword_from_active_context, + smt_ternary("ite", + get_path_condition(active_context), + get_word_symbolic(sword_from_active_context), + bv_constant(get_word_value(sword_from_mergeable_context)) + ) + ); + else { + // if we are too far into the shared symbolic memory space, we must not overwrite the value, + // but insert it into the unshared symbolic memory space of the active context + sword = allocate_symbolic_memory_word(); + set_word_address(sword, get_word_address(sword_from_active_context)); + set_word_value(sword, get_word_value(sword_from_active_context)); + set_number_of_bits(sword, get_number_of_bits(sword_from_active_context)); + set_word_symbolic(sword, + smt_ternary("ite", + get_path_condition(active_context), + get_word_symbolic(sword_from_active_context), + bv_constant(get_word_value(sword_from_mergeable_context)) + ) + ); + set_next_word(sword, additional_memory); + } + + // we need to break out of the loop + sword_from_active_context = (uint64_t*) - 1; + } + } else { + if (get_word_symbolic(sword_from_mergeable_context) != (char*) 0) { + // merge concrete value and symbolic value + if (shared_symbolic_memory_depth < 2) + set_word_symbolic(sword_from_active_context, + smt_ternary("ite", + get_path_condition(active_context), + bv_constant(get_word_value(sword_from_active_context)), + get_word_symbolic(sword_from_mergeable_context) + ) + ); + else { + // if we are too far into the shared symbolic memory space, we must not overwrite the value, + // but insert it into the unshared symbolic memory space of the active context + sword = allocate_symbolic_memory_word(); + set_word_address(sword, get_word_address(sword_from_active_context)); + set_word_value(sword, get_word_value(sword_from_active_context)); + set_number_of_bits(sword, get_number_of_bits(sword_from_active_context)); + set_word_symbolic(sword, + smt_ternary("ite", + get_path_condition(active_context), + bv_constant(get_word_value(sword_from_active_context)), + get_word_symbolic(sword_from_mergeable_context) + ) + ); + set_next_word(sword, additional_memory); + } + + // we need to break out of the loop + sword_from_active_context = (uint64_t*) - 1; + } else { + if (get_word_value(sword_from_active_context) != get_word_value(sword_from_mergeable_context)) { + // merge concrete values if they are different + if (shared_symbolic_memory_depth < 2) + set_word_symbolic(sword_from_active_context, + smt_ternary("ite", + get_path_condition(active_context), + bv_constant(get_word_value(sword_from_active_context)), + bv_constant(get_word_value(sword_from_mergeable_context)) + ) + ); + else { + // if we are too far into the shared symbolic memory space, we must not overwrite the value, + // but insert it into the unshared symbolic memory space of the active context + sword = allocate_symbolic_memory_word(); + set_word_address(sword, get_word_address(sword_from_active_context)); + set_word_value(sword, get_word_value(sword_from_active_context)); + set_number_of_bits(sword, get_number_of_bits(sword_from_active_context)); + set_word_symbolic(sword, + smt_ternary("ite", + get_path_condition(active_context), + bv_constant(get_word_value(sword_from_active_context)), + bv_constant(get_word_value(sword_from_mergeable_context)) + ) + ); + set_next_word(sword, additional_memory); + } + + // we need to break out of the loop + sword_from_active_context = (uint64_t*) - 1; + } + } + } + } + if (sword_from_active_context == (uint64_t*) - 1) + sword_from_active_context = (uint64_t*) 0; + else + sword_from_active_context = get_next_word(sword_from_active_context); + } + } + } + sword_from_mergeable_context = get_next_word(sword_from_mergeable_context); + } + + symbolic_memory = additional_memory; // the active context contains now the merged symbolic memory - set_symbolic_memory(active_context, symbolic_memory); + set_symbolic_memory(active_context, symbolic_memory); +} - i = 0; +void merge_registers(uint64_t* active_context, uint64_t* mergeable_context) { + uint64_t i; + i = 0; + // merging the symbolic registers while (i < NUMBEROFREGISTERS) { if (*(get_symbolic_regs(active_context) + i) != 0) { @@ -8264,13 +8475,24 @@ uint64_t* merge_if_possible_and_get_next_context(uint64_t* context) { } else mergeable = 0; } - + // check if the context has reached a merge location and needs to be paused while (pauseable) { if (get_pc(context) == get_merge_location(context)) { - add_mergeable_context(context); + current_mergeable_context = context; context = get_waiting_context(); - + + if (context) { + if (get_pc(context) == get_pc(current_mergeable_context)) { + pauseable = 0; + mergeable = 1; + } + else { + add_mergeable_context(current_mergeable_context); + current_mergeable_context = (uint64_t*) 0; + } + } + // break out of the loop if (context == (uint64_t*) 0) { mergeable = 0; @@ -8284,7 +8506,7 @@ uint64_t* merge_if_possible_and_get_next_context(uint64_t* context) { if (current_mergeable_context != (uint64_t*) 0) if (get_pc(context) == get_pc(current_mergeable_context)) mergeable = 1; - + pauseable = 0; } } @@ -8883,11 +9105,16 @@ void init_context(uint64_t* context, uint64_t* parent, uint64_t* vctxt) { set_symbolic_regs(context, zalloc(NUMBEROFREGISTERS * REGISTERSIZE)); set_beq_counter(context, 0); set_merge_location(context, -1); + set_prologues(context, (uint64_t*) 0); + set_in_recursion(context, 0); + set_outside_rec_loc(context, 0); + set_merge_partner(context, (uint64_t*) 0); } } uint64_t* copy_context(uint64_t* original, uint64_t location, char* condition, uint64_t depth) { uint64_t* context; + uint64_t* begin_of_shared_symbolic_memory; uint64_t r; context = new_context(); @@ -8921,7 +9148,25 @@ uint64_t* copy_context(uint64_t* original, uint64_t location, char* condition, u set_beq_counter(context, get_beq_counter(original)); set_merge_location(context, get_merge_location(original)); - copy_symbolic_memory(original, context); + begin_of_shared_symbolic_memory = allocate_symbolic_memory_word(); + + // mark begin of shared symbolic memory space in the copied context + set_next_word(begin_of_shared_symbolic_memory, get_symbolic_memory(original)); + set_word_address(begin_of_shared_symbolic_memory, BEGIN_OF_SHARED_SYMBOLIC_MEMORY); + + // begin of the unshared symbolic memory space of the copied context + set_symbolic_memory(context, begin_of_shared_symbolic_memory); + + begin_of_shared_symbolic_memory = allocate_symbolic_memory_word(); + + // mark begin of shared symbolic memory space in the original context + set_next_word(begin_of_shared_symbolic_memory, get_symbolic_memory(original)); + set_word_address(begin_of_shared_symbolic_memory, BEGIN_OF_SHARED_SYMBOLIC_MEMORY); + + // begin of the unshared symbolic memory space of the original context + set_symbolic_memory(original, begin_of_shared_symbolic_memory); + + symbolic_memory = get_symbolic_memory(original); set_prologues(context, get_prologues(original)); set_in_recursion(context, get_in_recursion(original)); @@ -8929,6 +9174,8 @@ uint64_t* copy_context(uint64_t* original, uint64_t location, char* condition, u set_symbolic_regs(context, smalloc(NUMBEROFREGISTERS * REGISTERSIZE)); + set_merge_partner(context, original); + r = 0; while (r < NUMBEROFREGISTERS) { @@ -9728,6 +9975,9 @@ uint64_t monster(uint64_t* to_context) { exception = handle_exception(from_context); if (exception == EXIT) { + // we need to update the end of the shared symbolic memory of the corresponding context + update_begin_of_shared_symbolic_memory(get_merge_partner(from_context)); + // if a context is currently waiting to be merged, we need to switch to this one if (current_mergeable_context != (uint64_t*) 0) { // update the merge location, so the 'new' context can be merged later From 2b92a4d1eca63dd1e0fad0ae1a1bd30a0124c20c Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Mon, 1 Jul 2019 10:29:25 +0200 Subject: [PATCH 19/21] Execution depth is now incremented correctly --- selfie.c | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/selfie.c b/selfie.c index d1b5f327..253b51c3 100644 --- a/selfie.c +++ b/selfie.c @@ -1471,7 +1471,7 @@ void reset_profiler() { uint64_t* new_context(); void init_context(uint64_t* context, uint64_t* parent, uint64_t* vctxt); -uint64_t* copy_context(uint64_t* original, uint64_t location, char* condition, uint64_t depth); +uint64_t* copy_context(uint64_t* original, uint64_t location, char* condition); uint64_t* find_context(uint64_t* parent, uint64_t* vctxt); @@ -7445,7 +7445,7 @@ void constrain_beq() { set_symbolic_memory(current_context, symbolic_memory); // the copied context is executed later and takes the other path - add_waiting_context(copy_context(current_context, pc + imm, smt_binary("and", pvar, bvar), max_execution_depth - timer)); + add_waiting_context(copy_context(current_context, pc + imm, smt_binary("and", pvar, bvar))); path_condition = smt_binary("and", pvar, smt_unary("not", bvar)); @@ -8910,6 +8910,9 @@ void interrupt() { if (timer != TIMEROFF) { timer = timer - 1; + if (symbolic) + set_execution_depth(current_context, get_execution_depth(current_context) + 1); + if (timer == 0) { if (get_exception(current_context) == EXCEPTION_NOEXCEPTION) // only throw exception if no other is pending @@ -9112,7 +9115,7 @@ void init_context(uint64_t* context, uint64_t* parent, uint64_t* vctxt) { } } -uint64_t* copy_context(uint64_t* original, uint64_t location, char* condition, uint64_t depth) { +uint64_t* copy_context(uint64_t* original, uint64_t location, char* condition) { uint64_t* context; uint64_t* begin_of_shared_symbolic_memory; uint64_t r; @@ -9143,7 +9146,7 @@ uint64_t* copy_context(uint64_t* original, uint64_t location, char* condition, u set_virtual_context(context, get_virtual_context(original)); set_name(context, get_name(original)); - set_execution_depth(context, depth); + set_execution_depth(context, get_execution_depth(original)); set_path_condition(context, condition); set_beq_counter(context, get_beq_counter(original)); set_merge_location(context, get_merge_location(original)); From cef00684682f0c26fe7132408d90a1c985cd411f Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Mon, 1 Jul 2019 11:00:28 +0200 Subject: [PATCH 20/21] Removed unnecessary variable --- selfie.c | 1 - 1 file changed, 1 deletion(-) diff --git a/selfie.c b/selfie.c index 253b51c3..aded1927 100644 --- a/selfie.c +++ b/selfie.c @@ -1293,7 +1293,6 @@ uint64_t MERGED = -2; // indicates that a symbolic memo uint64_t BEGIN_OF_SHARED_SYMBOLIC_MEMORY = -3; // indicates the begin of the shared symbolic memory space uint64_t BEQ_LIMIT = 35; // limit of symbolic beq instructions on any given path -uint64_t MAX_PATH_CONDITION_LENGTH = 1000000; // ----------------------------------------------------------------- // -------------------------- INTERPRETER -------------------------- From dc0cf1e477372b12336cdcbc30d05f48c84e5125 Mon Sep 17 00:00:00 2001 From: ChrisEdel Date: Thu, 25 Jul 2019 12:18:51 +0200 Subject: [PATCH 21/21] Improved comments on the limit of beq instructions --- selfie.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/selfie.c b/selfie.c index aded1927..35b48e63 100644 --- a/selfie.c +++ b/selfie.c @@ -1292,7 +1292,7 @@ uint64_t DELETED = -1; // indicates that a symbolic memo uint64_t MERGED = -2; // indicates that a symbolic memory word has been merged uint64_t BEGIN_OF_SHARED_SYMBOLIC_MEMORY = -3; // indicates the begin of the shared symbolic memory space -uint64_t BEQ_LIMIT = 35; // limit of symbolic beq instructions on any given path +uint64_t BEQ_LIMIT = 35; // limit of symbolic beq instructions on each part of the path between two merge locations // ----------------------------------------------------------------- // -------------------------- INTERPRETER -------------------------- @@ -7461,8 +7461,8 @@ void constrain_beq() { pc = pc + INSTRUCTIONSIZE; } else { - // if the limit of symbolic beq instructions is reached, the path still continues until it has reached its - // maximal execution depth, but only by following the true case of the next encountered symbolic beq instructions + // if the limit of symbolic beq instructions is reached, the part of the path still continues until it can be merged or has reached its + // maximal execution depth, respectively, but only by following the true case of the next encountered symbolic beq instructions path_condition = smt_binary("and", pvar, bvar); pc = pc + imm;