diff --git a/headers/gensym.hpp b/headers/gensym.hpp index 2067458a..5ab08ac5 100644 --- a/headers/gensym.hpp +++ b/headers/gensym.hpp @@ -45,25 +45,13 @@ #include #include -#ifdef PURE_STATE -#include -#endif -#ifdef IMPURE_STATE #include -#endif #include #include #include -#ifdef PURE_STATE -#include -#endif - -#ifdef IMPURE_STATE #include -#endif - #include #endif diff --git a/headers/gensym/branch.hpp b/headers/gensym/branch.hpp index 68566533..8053fb57 100644 --- a/headers/gensym/branch.hpp +++ b/headers/gensym/branch.hpp @@ -3,176 +3,6 @@ // Note: we should be able to generate these functions too -#ifdef PURE_STATE - -inline std::monostate async_exec_block(uint64_t ssid, const std::function& f) { - if (can_par_tp()) { - tp.add_task(ssid, f); - return std::monostate{}; - } - return f(); -} - -inline immer::flex_vector> -sym_exec_br(SS ss, unsigned int block_id, PtrVal t_cond, PtrVal f_cond, - immer::flex_vector> (*tf)(SS), - immer::flex_vector> (*ff)(SS)) { - auto [tbr_sat, fbr_sat] = check_branch(ss.get_PC(), t_cond); - if ((tbr_sat == solver_result::sat) && (fbr_sat == solver_result::sat)) { - // both branches are sat - cov().inc_path(1); - SS tbr_ss = ss.add_PC(t_cond); - SS fbr_ss = ss.fork().add_PC(f_cond); - if (can_par_async()) { - std::future>> tf_res = - create_async>>([&]{ - cov().inc_branch(block_id, 0); - return tf(tbr_ss); - }); - cov().inc_branch(block_id, 1); - auto ff_res = ff(fbr_ss); - return tf_res.get() + ff_res; - } else { - cov().inc_branch(block_id, 0); - cov().inc_branch(block_id, 1); - return tf(tbr_ss) + ff(fbr_ss); - } - } else if (tbr_sat == solver_result::sat) { - cov().inc_branch(block_id, 0); - SS tbr_ss = ss.add_PC(t_cond); - return tf(tbr_ss); - } else if (fbr_sat == solver_result::sat) { - cov().inc_branch(block_id, 1); - SS fbr_ss = ss.add_PC(f_cond); - return ff(fbr_ss); - } else { - ABORT("Both branches are unsat!"); - } -} - -inline std::monostate -sym_exec_br_k(SS ss, unsigned int block_id, PtrVal t_cond, PtrVal f_cond, - std::function)> tf, - std::function)> ff, - std::function k) { - auto [tbr_sat, fbr_sat] = check_branch(ss.get_PC(), t_cond); - if ((tbr_sat == solver_result::sat) && (fbr_sat == solver_result::sat)) { - cov().inc_path(1); - SS tbr_ss = ss.add_PC(t_cond); - SS fbr_ss = ss.fork().add_PC(f_cond); - if (can_par_tp()) { - tp.add_task(tbr_ss.get_ssid(), [tf, block_id, tbr_ss=std::move(tbr_ss), k]{ - cov().inc_branch(block_id, 0); - return tf(tbr_ss, k); - }); - tp.add_task(fbr_ss.get_ssid(), [ff, block_id, fbr_ss=std::move(fbr_ss), k]{ - cov().inc_branch(block_id, 1); - return ff(fbr_ss, k); - }); - return std::monostate{}; - } else { - cov().inc_branch(block_id, 0); - tf(tbr_ss, k); - cov().inc_branch(block_id, 1); - ff(fbr_ss, k); - return std::monostate{}; - } - } else if (tbr_sat == solver_result::sat) { - cov().inc_branch(block_id, 0); - SS tbr_ss = ss.add_PC(t_cond); - return tf(tbr_ss, k); - } else if (fbr_sat == solver_result::sat) { - cov().inc_branch(block_id, 1); - SS fbr_ss = ss.add_PC(f_cond); - return ff(fbr_ss, k); - } else { - ABORT("Both branches are unsat!"); - } -} - -// Todo : check offset out of bound -inline immer::flex_vector> -array_lookup(SS ss, PtrVal base, PtrVal offset, size_t esize) { - immer::flex_vector_transient> result; - auto baseloc = std::dynamic_pointer_cast(base); - - if (auto offint = std::dynamic_pointer_cast(offset)) { - // base may not be a locv, ie a bad pointer - result.push_back(std::make_pair(ss, base + (offint->as_signed() * esize))); - } else if (auto offsym = std::dynamic_pointer_cast(offset)) { - int cnt = 0; - int lower_bound = ((int)(baseloc->base - baseloc->l)) / esize; - int higher_bound = ((int)(baseloc->base + baseloc->size - baseloc->l)) / esize - 1; - ASSERT(higher_bound >= lower_bound, "Bad bound"); - int possible_num = (higher_bound - lower_bound) + 1; - - auto low_cond = int_op_2(iOP::op_sge, offsym, make_IntV(lower_bound, offsym->get_bw())); - auto high_cond = int_op_2(iOP::op_sle, offsym, make_IntV(higher_bound, offsym->get_bw())); - auto pc2 = ss.get_PC().add(low_cond).add(high_cond); - auto res = get_sat_value(pc2, offsym); - while (res.first) { - cnt++; - int offset_val = res.second; - auto t_cond = int_op_2(iOP::op_eq, offsym, make_IntV(offset_val, offsym->get_bw())); - if (1 == cnt) { - result.push_back(std::make_pair(ss.add_PC(t_cond), baseloc + (offset_val*esize))); - } else { - result.push_back(std::make_pair(ss.fork().add_PC(t_cond), baseloc + (offset_val*esize))); - } - pc2 = pc2.add(SymV::neg(t_cond)); - res = get_sat_value(pc2, offsym); - } - ASSERT(cnt > 0, "No satisfiable offset value"); - cov().inc_path(cnt - 1); - } else ABORT("Error: unknown array offset kind."); - - return result.persistent(); -} - -inline std::monostate -array_lookup_k(SS ss, PtrVal base, PtrVal offset, size_t esize, - std::function k) { - auto baseloc = std::dynamic_pointer_cast(base); - - if (auto offint = std::dynamic_pointer_cast(offset)) { - // base may not be a locv, ie a bad pointer - k(ss, base + (offint->as_signed() * esize)); - } - else if (auto offsym = std::dynamic_pointer_cast(offset)) { - int cnt = 0; - int lower_bound = ((int)(baseloc->base - baseloc->l)) / esize; - int higher_bound = ((int)(baseloc->base + baseloc->size - baseloc->l)) / esize - 1; - ASSERT(higher_bound >= lower_bound, "Bad bound"); - int possible_num = (higher_bound - lower_bound) + 1; - - auto low_cond = int_op_2(iOP::op_sge, offsym, make_IntV(lower_bound, offsym->get_bw())); - auto high_cond = int_op_2(iOP::op_sle, offsym, make_IntV(higher_bound, offsym->get_bw())); - auto pc2 = ss.get_PC().add(low_cond).add(high_cond); - auto res = get_sat_value(pc2, offsym); - while (res.first) { - cnt++; - int offset_val = res.second; - auto t_cond = int_op_2(iOP::op_eq, offsym, make_IntV(offset_val, offsym->get_bw())); - auto new_loc = baseloc + (offset_val*esize); - auto new_ss = (1 == cnt) ? ss.add_PC(t_cond) : ss.fork().add_PC(t_cond); - if (can_par_tp()) { - tp.add_task(new_ss.get_ssid(), [new_loc=std::move(new_loc), new_ss=std::move(new_ss), k]{ return k(new_ss, new_loc); }); - } else { - k(new_ss, new_loc); - } - pc2 = pc2.add(SymV::neg(t_cond)); - res = get_sat_value(pc2, offsym); - } - ASSERT(cnt > 0, "No satisfiable offset value"); - cov().inc_path(cnt - 1); - } else ABORT("Error: unknown array offset kind."); - return std::monostate{}; -} - -#endif - -#ifdef IMPURE_STATE - inline std::monostate async_exec_block( std::monostate (*f)(SS&, std::function), SS ss, std::function k) { @@ -360,6 +190,5 @@ array_lookup_k(SS& ss, PtrVal base, PtrVal offset, size_t esize, } else ABORT("Error: unknown array offset kind."); return std::monostate{}; } -#endif #endif diff --git a/headers/gensym/external_pure.hpp b/headers/gensym/external_pure.hpp deleted file mode 100644 index 7c48a67b..00000000 --- a/headers/gensym/external_pure.hpp +++ /dev/null @@ -1,637 +0,0 @@ -#ifndef GS_EXTERNAL_PURE_HEADER -#define GS_EXTERNAL_PURE_HEADER - -#include "external_shared.hpp" - -/******************************************************************************/ - -template -inline T __gs_assert(SS& state, List& args, __Cont k, __Halt h) { - auto v = args.at(0); - auto i = v->to_IntV(); - if (i) { - if (i->i == 0) { - // concrete false - generate the test and ``halt'' - std::cout << "Warning: assert violates; abort and generate test.\n"; - return h(state, { make_IntV(-1) }); - } - return k(state, make_IntV(1, 32)); - } - // otherwise add a symbolic condition that constraints it to be true - // undefined/error if v is a value of other types - - auto [fls_sat, tru_sat] = check_branch(state.get_PC(), SymV::neg(v)); // check if v == 1 is not valid - if (fls_sat) { - std::cout << "Warning: assert violates; abort and generate test.\n"; - return h(state, { make_IntV(-1, 32) }); - } - return k(state.add_PC(v), make_IntV(1, 32)); -} - -/******************************************************************************/ - -template -inline T __gs_assume(SS& state, List& args, __Cont k, __Halt h) { - auto v = args.at(0); - auto i = v->to_IntV(); - if (i) { - if (i->i == 0) { - // concrete false - generate the test and ``halt'' - std::cout << "Warning: assume violates; abort and generate test.\n"; - return h(state, { make_IntV(-1, 32) }); - } - return k(state, make_IntV(1, 32)); - } - ASSERT(std::dynamic_pointer_cast(v) != nullptr, "Non-Symv"); - // otherwise add a symbolic condition that constraints it to be true - // undefined/error if v is a value of other types - auto [tru_sat, fls_sat] = check_branch(state.get_PC(), v); // check if v == 1 is satisfiable - if (!tru_sat) { - std::cout << "Warning: assume violates; abort and generate test.\n"; - return h(state, { make_IntV(-1) }); // check if v == 1 is satisfiable - } - return k(state.add_PC(v), make_IntV(1, 32)); -} - -/******************************************************************************/ - -template -inline T __make_symbolic(SS& state, List& args, __Cont k) { - PtrVal loc = args.at(0); - ASSERT(std::dynamic_pointer_cast(loc) != nullptr, "Non-location value"); - IntData len = proj_IntV(args.at(1)); - ASSERT(len > 0, "Invalid length"); - ASSERT(2 == args.size() || 3 == args.size(), "Too much arguments for make_symbolic"); - std::string object_name = (2 == args.size()) ? fresh("unnamed") : state.get_unique_name(get_string_at(state, args.at(2))); - SS res = state.add_symbolic(object_name, len, false); - //std::cout << "sym array size: " << proj_LocV_size(loc) << "\n"; - for (int i = 0; i < len; i++) { - res = res.update_simpl(loc + i, make_SymV(object_name + "_" + std::to_string(i), 8)); - } - return k(res, make_IntV(0)); -} - -inline List make_symbolic(SS state, List args) { - return __make_symbolic>(state, args, [](auto s, auto v) { return List{{s, v}}; }); -} - -inline std::pair make_symbolic_det(SS state, List args) { - return __make_symbolic>(state, args, [](auto s, auto v) { return std::make_pair(s, v); }); -} - -inline std::monostate make_symbolic(SS state, List args, Cont k) { - return __make_symbolic(state, args, [&k](auto s, auto v) { return k(s, v); }); -} - -template -inline T __make_symbolic_whole(SS& state, List& args, __Cont k) { - PtrVal loc = args.at(0); - ASSERT(std::dynamic_pointer_cast(loc) != nullptr, "Non-location value"); - IntData sz = proj_IntV(args.at(1)); - ASSERT(sz > 0, "Invalid length"); - ASSERT(2 == args.size() || 3 == args.size(), "Too much arguments for make_symbolic"); - std::string object_name = (2 == args.size()) ? fresh("unnamed") : state.get_unique_name(get_string_at(state, args.at(2))); - SS res = state.add_symbolic(object_name, sz, true).update(loc, make_SymV(object_name, sz*8), sz); - return k(res, make_IntV(0)); -} - -inline List make_symbolic_whole(SS state, List args) { - return __make_symbolic_whole>(state, args, [](auto s, auto v) { return List{{s, v}}; }); -} - -inline std::pair make_symbolic_whole_det(SS state, List args) { - return __make_symbolic_whole>(state, args, [](auto s, auto v) { return std::make_pair(s, v); }); -} - -inline std::monostate make_symbolic_whole(SS state, List args, Cont k) { - return __make_symbolic_whole(state, args, [&k](auto s, auto v) { return k(s, v); }); -} - -/******************************************************************************/ - -template -inline T __malloc(SS& state, List& args, __Cont k) { - auto size = args.at(0); - if (auto symvite = std::dynamic_pointer_cast(size)) { - ASSERT(iOP::op_ite == symvite->rator, "Invalid memory read by symv index"); - auto cond = (*symvite)[0]; - auto v_t = (*symvite)[1]; - auto v_f = (*symvite)[2]; - auto [tbr_sat, fbr_sat] = check_branch(state.get_PC(), cond); - auto t_args = List{v_t}; - auto f_args = List{v_f}; - if (tbr_sat && fbr_sat) { - cov().inc_path(1); - SS tbr_ss = state.add_PC(cond); - SS fbr_ss = state.fork().add_PC(SymV::neg(cond)); - return __malloc(tbr_ss, t_args, k) + __malloc(fbr_ss, f_args, k); - } else if (tbr_sat) { - SS tbr_ss = state.add_PC(cond); - return __malloc(tbr_ss, t_args, k); - } else if (fbr_sat) { - SS fbr_ss = state.add_PC(SymV::neg(cond)); - return __malloc(fbr_ss, f_args, k); - } else { - ABORT("no feasible path"); - } - } else { - IntData bytes = proj_IntV(size); - auto emptyMem = List(bytes, make_UnInitV()); - PtrVal memLoc = make_LocV(state.heap_size(), LocV::kHeap, bytes); - if (exlib_failure_branch) - return k(state.heap_append(emptyMem), memLoc) + k(state, make_LocV_null()); - return k(state.heap_append(emptyMem), memLoc); - } -} - -inline List malloc(SS state, List args) { - return __malloc>(state, args, [](auto s, auto v) { return List{{s, v}}; }); -} - -inline std::monostate malloc(SS state, List args, Cont k) { - // TODO: in the thread pool version, we should add task into the pool when forking - return __malloc(state, args, [&k](auto s, auto v) { return k(s, v); }); -} - -/******************************************************************************/ - -template -inline T __memalign(SS& state, List& args, __Cont k) { - size_t alignment = proj_IntV(args.at(0)); - size_t bytes = proj_IntV(args.at(1)); - auto fillmem = List((((state.heap_size() + (alignment - 1)) / alignment) * alignment) - state.heap_size(), make_UnInitV()); - auto emptyMem = List(bytes, make_UnInitV()); - auto fill_state = state.heap_append(fillmem); - ASSERT(0 == fill_state.heap_size() % alignment, "non-aligned address"); - PtrVal memLoc = make_LocV(fill_state.heap_size(), LocV::kHeap, bytes); - if (exlib_failure_branch) - return k(fill_state.heap_append(emptyMem), memLoc) + k(state, make_LocV_null()); - return k(fill_state.heap_append(emptyMem), memLoc); -} - -inline List memalign(SS state, List args) { - return __memalign>(state, args, [](auto s, auto v) { return List{{s, v}}; }); -} - -inline std::monostate memalign(SS state, List args, Cont k) { - return __memalign(state, args, [&k](auto s, auto v) { return k(s, v); }); -} - -/******************************************************************************/ - -template -inline T __realloc(SS& state, List& args, __Cont k) { - IntData bytes = proj_IntV(args.at(1)); - auto emptyMem = List(bytes, make_UnInitV()); - PtrVal memLoc = make_LocV(state.heap_size(), LocV::kHeap, bytes); - SS res = state.heap_append(emptyMem); - if (!is_LocV_null(args.at(0))) { - Addr src = proj_LocV(args.at(0)); - IntData prevBytes = proj_LocV_size(args.at(0)); - for (int i = 0; i < prevBytes; i++) { - res = res.update_simpl(memLoc + i, res.heap_lookup(src + i)); - } - } - return k(res, memLoc); -} - -inline List realloc(SS state, List args) { - return __realloc>(state, args, [](auto s, auto v) { return List{{s, v}}; }); -} - -inline std::monostate realloc(SS state, List args, Cont k) { - return __realloc(state, args, [&k](auto s, auto v) { return k(s, v); }); -} - -/******************************************************************************/ - -template -inline T __reallocarray(SS& state, List& args, __Cont k) { - IntData nmemb = proj_IntV(args.at(1)); - IntData size = proj_IntV(args.at(2)); - ASSERT(size > 0 && nmemb > 0, "Invalid nmemb and size"); - IntData bytes = nmemb * size; - auto emptyMem = List(bytes, make_UnInitV()); - PtrVal memLoc = make_LocV(state.heap_size(), LocV::kHeap, bytes); - SS res = state.heap_append(emptyMem); - if (!is_LocV_null(args.at(0))) { - Addr src = proj_LocV(args.at(0)); - IntData prevBytes = proj_LocV_size(args.at(0)); - for (int i = 0; i < prevBytes; i++) { - res = res.update_simpl(memLoc + i, res.heap_lookup(src + i)); - } - } - return k(res, memLoc); -} - -inline List reallocarray(SS state, List args) { - return __reallocarray>(state, args, [](auto s, auto v) { return List{{s, v}}; }); -} - -inline std::monostate reallocarray(SS state, List args, Cont k) { - return __reallocarray(state, args, [&k](auto s, auto v) { return k(s, v); }); -} - -/******************************************************************************/ - -template -inline T __calloc(SS& state, List& args, __Cont k) { - IntData nmemb = proj_IntV(args.at(0)); - IntData size = proj_IntV(args.at(1)); - ASSERT(size > 0 && nmemb > 0, "Invalid nmemb and size"); - auto emptyMem = List(nmemb * size, make_IntV(0, 8)); - - PtrVal memLoc = make_LocV(state.heap_size(), LocV::kHeap, nmemb * size); - if (exlib_failure_branch) - return k(state.heap_append(emptyMem), memLoc) + k(state, make_LocV_null()); - return k(state.heap_append(emptyMem), memLoc); -} - -inline List calloc(SS state, List args) { - return __calloc>(state, args, [](auto s, auto v) { return List{{s, v}}; }); -} - -inline std::monostate calloc(SS state, List args, Cont k) { - // TODO: in the thread pool version, we should add task into the pool when forking - return __calloc(state, args, [&k](auto s, auto v) { return k(s, v); }); -} - -/******************************************************************************/ - -template -inline T __llvm_memcpy(SS& state, List& args, __Cont k) { - PtrVal dest = args.at(0); - PtrVal src = args.at(1); - PtrVal size = args.at(2); - IntData bytes_int; - // Todo (Ruiqi): should we fork here - if (auto symvite = std::dynamic_pointer_cast(size)) { - ASSERT(iOP::op_ite == symvite->rator, "Invalid memory read by symv index"); - auto cond = (*symvite)[0]; - auto v_t = (*symvite)[1]; - auto v_f = (*symvite)[2]; - auto [tbr_sat, fbr_sat] = check_branch(state.get_PC(), cond); - ASSERT((!tbr_sat || !fbr_sat) && (tbr_sat || fbr_sat), "Should already forked before, only one path is feasible"); - bytes_int = tbr_sat ? proj_IntV(v_t) : proj_IntV(v_f); - if (auto srcite = std::dynamic_pointer_cast(src)) { - ASSERT(iOP::op_ite == srcite->rator && (*srcite)[0] == cond, "Inconsistent ite src and size"); - src = tbr_sat ? (*srcite)[1] : (*srcite)[2]; - } - } - else - bytes_int = proj_IntV(size); - ASSERT(std::dynamic_pointer_cast(dest) != nullptr, "Non-location value"); - ASSERT(std::dynamic_pointer_cast(src) != nullptr, "Non-location value"); - SS res = state; - for (int i = 0; i < bytes_int; i++) { - res = res.update_simpl(dest + i, res.at_simpl(src + i)); - } - return k(res, IntV0_32); -} - -inline List llvm_memcpy(SS state, List args) { - return __llvm_memcpy>(state, args, [](auto s, auto v) { return List{{s, v}}; }); -} - -inline std::monostate llvm_memcpy(SS state, List args, Cont k) { - return __llvm_memcpy(state, args, [&k](auto s, auto v) { return k(s, v); }); -} - -/******************************************************************************/ - -template -inline T __llvm_memmove(SS& state, List& args, __Cont k) { - PtrVal dest = args.at(0); - PtrVal src = args.at(1); - ASSERT(std::dynamic_pointer_cast(dest) != nullptr, "Non-location value"); - ASSERT(std::dynamic_pointer_cast(src) != nullptr, "Non-location value"); - SS res = state; - IntData bytes_int = proj_IntV(args.at(2)); - auto temp_mem = TrList{}; - for (int i = 0; i < bytes_int; i++) { - temp_mem.push_back(res.at_simpl(src + i)); - } - for (int i = 0; i < bytes_int; i++) { - res = res.update_simpl(dest + i, temp_mem.at(i)); - } - return k(res, IntV0_32); -} - -inline List llvm_memmove(SS state, List args) { - return __llvm_memmove>(state, args, [](auto s, auto v) { return List{{s, v}}; }); -} - -inline std::monostate llvm_memmove(SS state, List args, Cont k) { - return __llvm_memmove(state, args, [&k](auto s, auto v) { return k(s, v); }); -} - -/******************************************************************************/ - -template -inline T __llvm_memset(SS& state, List& args, __Cont k) { - PtrVal dest = args.at(0); - IntData bytes_int = proj_IntV(args.at(2)); - ASSERT(std::dynamic_pointer_cast(dest) != nullptr, "Non-location value"); - SS res = state; - for (int i = 0; i < bytes_int; i++) { - res = res.update_simpl(dest + i, make_UnInitV()); - } - return k(res, IntV0_32); -} - -inline List llvm_memset(SS state, List args) { - return __llvm_memset>(state, args, [](auto s, auto v) { return List{{s, v}}; }); -} - -inline std::monostate llvm_memset(SS state, List args, Cont k) { - return __llvm_memset(state, args, [&k](auto s, auto v) { return k(s, v); }); -} - -/******************************************************************************/ - -inline SS copy_native2state(SS state, PtrVal ptr, char* buf, int size) { - ASSERT(buf && size > 0, "Invalid native buffer"); - SS res = state; - for (int i = 0; i < size; ) { - auto old_val = state.at_simpl(ptr + i); - if (old_val) { - if (std::dynamic_pointer_cast(old_val) || std::dynamic_pointer_cast(old_val)) { - ABORT("unhandled ptrval: shadowv && LocV"); - } - auto bytes_num = old_val->get_byte_size(); - ASSERT(bytes_num > 0, "Invalid bytes"); - // All bytes must be concrete IntV - if (std::dynamic_pointer_cast(old_val)) { - #ifdef GENSYM_SYMBOLIC_UNINIT - // add constraint on symbolic variable to be equal to concrete - for (int j = 0; j < bytes_num; j++) { - auto eq_constraint = int_op_2(iOP::op_eq, state.at_simpl(ptr + i), make_IntV(buf[i], 8)); - res = res.add_PC(eq_constraint); - i++; - if (i >= size) break; - } - #else - i += bytes_num; - #endif - } else { - for (int j = 0; j < bytes_num; j++) { - res = res.update_simpl(ptr + i, make_IntV(buf[i], 8)); - i++; - if (i >= size) break; - } - } - } else { - res = res.update_simpl(ptr + i, make_IntV(buf[i], 8)); - i++; - } - } - return res; -} - -inline SS writeback_pointer_arg(SS state, PtrVal loc, void* buf) { - if (is_LocV_null(loc)) { - ASSERT(nullptr == buf, "allocate memory for null locv"); - return state; - } - ASSERT(std::dynamic_pointer_cast(loc), "Non LocV"); - size_t count = get_pointer_realsize(loc); - SS res = copy_native2state(state, loc, (char*)buf, count); - free(buf); - return res; -} - -class ShadowMemEntry { - private: - char* buf; - public: - size_t size; - PtrVal mem_addr; - ShadowMemEntry(PtrVal addr, size_t size) : buf(new char[size+1]), mem_addr(addr), size(size) { - ASSERT(std::dynamic_pointer_cast(addr) != nullptr, "Non-location value"); - memset(buf, 0, size+1); - } - ~ShadowMemEntry() { delete buf; } - SS writeback(SS& state) { return copy_native2state(state, mem_addr, buf, size); } - void readbuf(SS& state) { copy_state2native(state, mem_addr, buf, size); } - char* getbuf() { return buf; } -}; - -template -inline T __syscall(SS& state, List& args, __Cont k) { - PtrVal x = args.at(0); - auto x_i = std::dynamic_pointer_cast(x); - ASSERT(x_i && (64 == x_i->bw), "syscall's argument must be concrete and must be long (i64)!"); - long syscall_number = x_i->as_signed(); - long retval = -1; - - // Save errno - errno = proj_IntV(state.at(state.error_loc(), 4)); - - SS res = state; - switch (syscall_number) { -#if defined(__x86_64__) || defined(__i386__) - case __NR_read: { - int fd = get_int_arg(state, args.at(1)); - ASSERT(0 == fd, "syscall read can only read from stdin, other fd should use pread64\n"); - size_t count = get_int_arg(state, args.at(3)); - ShadowMemEntry temp(args.at(2), count); - retval = syscall(__NR_read, fd, temp.getbuf(), count); - if (retval >= 0) res = temp.writeback(res); - break; - } - case __NR_write: { - int fd = get_int_arg(state, args.at(1)); - ASSERT((1 == fd) || (2 == fd) ,"syscall write can only write to stdout and stderr, other fd should use pwrite64\n"); - size_t count = get_int_arg(state, args.at(3)); - ShadowMemEntry temp(args.at(2), count); - temp.readbuf(res); - retval = syscall(__NR_write, fd, temp.getbuf(), count); - break; - } - case __NR_open: { - ASSERT(3 == args.size() || 4 == args.size(), "open has 2 or 3 arguments"); - mode_t mode = 4 == args.size() ? get_int_arg(state, args.at(3)) : 0; - int flags = get_int_arg(state, args.at(2)); - std::string pathname = get_string_arg(state, args.at(1)); - //std::cout << "pathname: " << pathname << " flags: " << flags << " mode: " << mode << std::endl; - retval = syscall(__NR_open, pathname.c_str(), flags, mode); - break; - } - case __NR_close: { - int fd = get_int_arg(state, args.at(1)); - retval = syscall(__NR_close, fd); - break; - } - case __NR_stat: { - std::string pathname = get_string_arg(state, args.at(1)); - size_t count = sizeof(struct stat64); - ShadowMemEntry temp(args.at(2), count); - retval = syscall(__NR_stat, pathname.c_str(), temp.getbuf()); - if (retval >= 0) res = temp.writeback(res); - break; - } - case __NR_fstat: { - int fd = get_int_arg(state, args.at(1)); - size_t count = sizeof(struct stat64); - ShadowMemEntry temp(args.at(2), count); - retval = syscall(__NR_fstat, fd, temp.getbuf()); - if (retval >= 0) res = temp.writeback(res); - break; - } - case __NR_lstat: { - std::string pathname = get_string_arg(state, args.at(1)); - size_t count = sizeof(struct stat64); - ShadowMemEntry temp(args.at(2), count); - retval = syscall(__NR_lstat, pathname.c_str(), temp.getbuf()); - if (retval >= 0) res = temp.writeback(res); - break; - } - case __NR_lseek: { - int fd = get_int_arg(state, args.at(1)); - off64_t offset = get_int_arg(state, args.at(2)); - int whence = get_int_arg(state, args.at(3)); - retval = syscall(__NR_lseek, fd, offset, whence); - break; - } - case __NR_ioctl: { - int fd = get_int_arg(state, args.at(1)); - unsigned long request = get_int_arg(state, args.at(2)); - auto buf = std::dynamic_pointer_cast(args.at(3)); - size_t count = buf->size - (buf->l - buf->base); - ShadowMemEntry temp(buf, count); - retval = syscall(__NR_ioctl, fd, request, temp.getbuf()); - //std::cout << "ioctl: " << " fd: " << fd << " request: " << request << " buf: " << std::string(temp.getbuf()) << " count: " << count << " result: " << retval << std::endl; - if (retval >= 0) res = temp.writeback(res); - break; - } - case __NR_pread64: { - int fd = get_int_arg(state, args.at(1)); - ASSERT(fd > 2, "can not call pread/pwrite on stdin, stdout and stderr\n"); - size_t count = get_int_arg(state, args.at(3)); - off64_t offset = get_int_arg(state, args.at(4)); - ShadowMemEntry temp(args.at(2), count); - //std::cout << "pread: " << " fd: " << fd << " buf: " << std::string(temp.getbuf()) << " count: " << count << " offset: " << offset << std::endl; - retval = syscall(__NR_pread64, fd, temp.getbuf(), count, offset); - if (retval >= 0) res = temp.writeback(res); - break; - } - case __NR_pwrite64: { - int fd = get_int_arg(state, args.at(1)); - ASSERT(fd > 2, "can not call pread/pwrite on stdin, stdout and stderr\n"); - size_t count = get_int_arg(state, args.at(3)); - off64_t offset = get_int_arg(state, args.at(4)); - ShadowMemEntry temp(args.at(2), count); - temp.readbuf(res); - //std::cout << "pwrite: " << " fd: " << fd << " buf: " << std::string(temp.getbuf()) << " count: " << count << " offset: " << offset << std::endl; - retval = syscall(__NR_pwrite64, fd, temp.getbuf(), count, offset); - break; - } - case __NR_ftruncate: { - int fd = get_int_arg(state, args.at(1)); - off_t length = get_int_arg(state, args.at(2)); - retval = syscall(__NR_ftruncate, fd, length); - break; - } - case __NR_getcwd: { - size_t count = get_int_arg(state, args.at(2)); - ASSERT(count > 0, "empty buffer for getcwd"); - ASSERT(!is_LocV_null(args.at(1)), "null buffer pointer"); - ShadowMemEntry temp(args.at(1), count); - retval = syscall(__NR_getcwd, temp.getbuf(), count); - if (retval >= 0) res = temp.writeback(res); - break; - } - case __NR_access: - case __NR_select: - case __NR_fcntl: - case __NR_fsync: - case __NR_chdir: - case __NR_fchdir: - case __NR_readlink: - case __NR_chmod: - case __NR_fchmod: - case __NR_chown: - case __NR_fchown: - case __NR_statfs: - case __NR_fstatfs: - case __NR_getdents64: - case __NR_utimes: - case __NR_openat: - case __NR_futimesat: - case __NR_newfstatat: -#endif - default: - ABORT("Unsupported Systemcall"); - break; - } - - // Write back errno - res = res.update(res.error_loc(), make_IntV(errno, 32), 4); - //std::cout << "syscall_num: " << syscall_number << " retval: " << retval << std::endl; - - return k(res, make_IntV(retval, 64)); -} - -inline List syscall(SS state, List args) { - return __syscall>(state, args, [](auto s, auto v) { return List{{s, v}}; }); -} - -inline std::monostate syscall(SS state, List args, Cont k) { - return __syscall(state, args, [&k](auto s, auto v) { return k(s, v); }); -} - -/******************************************************************************/ - -// FIXME: vaargs and refactor -// args 0: LocV to {i32, i32, i8*, i8*} -// in memory {4, 4, 8, 8} -template -inline T __llvm_va_start(SS& state, List& args, __Cont k) { - PtrVal va_list = args.at(0); - ASSERT(std::dynamic_pointer_cast(va_list) != nullptr, "Non-location value"); - PtrVal va_arg = state.vararg_loc(); - SS res = state; - res = res.update(va_list + 0, IntV0_32, 4); - res = res.update(va_list + 4, IntV0_32, 4); - res = res.update(va_list + 8, va_arg + 48, 8); - res = res.update(va_list + 16, va_arg, 8); - return k(res, IntV0_32); -} -template -inline T __llvm_va_end(SS& state, List& args, __Cont k) { - PtrVal va_list = args.at(0); - ASSERT(std::dynamic_pointer_cast(va_list) != nullptr, "Non-location value"); - SS res = state; - auto loc0 = make_LocV_null(); - res = res.update(va_list + 0, IntV0_32, 4); - res = res.update(va_list + 4, IntV0_32, 4); - res = res.update(va_list + 8, loc0, 8); - res = res.update(va_list + 16, loc0, 8); - return k(res, IntV0_32); -} -template -inline T __llvm_va_copy(SS& state, List& args, __Cont k) { - PtrVal dst_va_list = args.at(0); - PtrVal src_va_list = args.at(1); - ASSERT(std::dynamic_pointer_cast(dst_va_list) != nullptr, "Dest valist Non-location value"); - ASSERT(std::dynamic_pointer_cast(src_va_list) != nullptr, "Src valist Non-location value"); - ASSERT(std::dynamic_pointer_cast(state.at(src_va_list + 16, 8)) != nullptr, "Src valist must be initialized"); - SS res = state; - res = res.update(dst_va_list + 0, state.at(src_va_list + 0, 4), 4); - res = res.update(dst_va_list + 4, state.at(src_va_list + 4, 4), 4); - res = res.update(dst_va_list + 8, state.at(src_va_list + 8, 8), 8); - res = res.update(dst_va_list + 16, state.at(src_va_list + 16, 8), 8); - return k(res, IntV0_32); -} - -/******************************************************************************/ - -template -inline T __gs_prefer_cex(SS& state, List& args, __Cont k) { - ASSERT(2 == args.size(), "Invalid number of arguments for gs_prefer_cex"); - auto cond = args.at(1); - ASSERT(std::dynamic_pointer_cast(cond) != nullptr, "Not a symbolic expression"); - return k(state.add_cex(cond), make_IntV(0)); -} - -#endif diff --git a/headers/gensym/external_shared.hpp b/headers/gensym/external_shared.hpp index 5012cbe7..c9a670b4 100644 --- a/headers/gensym/external_shared.hpp +++ b/headers/gensym/external_shared.hpp @@ -7,13 +7,7 @@ * behavior of `SS`, then it probably should be put here. */ -#ifdef PURE_STATE -using Cont = std::function; -#endif - -#ifdef IMPURE_STATE using Cont = std::function; -#endif template using __Cont = std::function; template using __Halt = std::function)>; diff --git a/headers/gensym/metadata.hpp b/headers/gensym/metadata.hpp index 61f2f7cf..21f9accd 100644 --- a/headers/gensym/metadata.hpp +++ b/headers/gensym/metadata.hpp @@ -30,20 +30,6 @@ class MetaData: public Printable { return ss.str(); } -#ifdef PURE_STATE - MetaData add_incoming_block(BlockLabel blabel) { - return MetaData(ssid, blabel, has_cover_new, sym_objs, preferred_cex); - } - MetaData cover_block(BlockLabel new_bb) { - bool is_covernew = cov().is_uncovered(new_bb); - cov().inc_block(new_bb); - return MetaData(ssid, bb, has_cover_new | is_covernew, sym_objs, preferred_cex); - } - MetaData add_symbolic(const std::string& name, int size, bool is_whole) { - return MetaData(ssid, bb, has_cover_new, sym_objs.push_back(SymObj(name, size, is_whole)), preferred_cex); } - MetaData add_cex(const PtrVal& cex) { return MetaData(ssid, bb, has_cover_new, sym_objs, preferred_cex.push_back(cex)); } -#endif -#ifdef IMPURE_STATE void add_incoming_block(BlockLabel blabel) { bb = blabel; } void cover_block(BlockLabel new_bb) { bool is_cover_new = cov().is_uncovered(new_bb); @@ -56,7 +42,6 @@ class MetaData: public Printable { void add_cex(const PtrVal& cex) { preferred_cex = preferred_cex.push_back(cex); } -#endif }; #endif diff --git a/headers/gensym/state_imp.hpp b/headers/gensym/state_imp.hpp deleted file mode 100644 index b9d38a4f..00000000 --- a/headers/gensym/state_imp.hpp +++ /dev/null @@ -1,589 +0,0 @@ -#ifndef GS_STATE_IMP_HEADER -#define GS_STATE_IMP_HEADER - -/* Note: This file has been deprecated! */ - -/* Memory, stack, and symbolic state representation */ - -// Note (5/17): now using a byte-oriented layout -template -class PreMem { - protected: - M&& move_this() { return std::move(*((M*)this)); } - std::vector mem; - public: - PreMem(std::vector mem) : mem(std::move(mem)) {} - size_t size() { return mem.size(); } - V at(size_t idx) { return mem[idx]; } - M&& update(size_t idx, V val) { - mem.at(idx) = val; - return move_this(); - } - M&& append(V val) { - mem.push_back(val); - return move_this(); - } - M&& append(V val, size_t padding) { - size_t idx = mem.size(); - return alloc(padding + 1).update(idx, val); - } - M&& append(const std::vector& vs) { - mem.insert(mem.end(), vs.begin(), vs.end()); - return move_this(); - } - M&& alloc(size_t size) { - mem.resize(mem.size() + size, make_UnInitV()); - return move_this(); - } - M&& take(size_t keep) { - mem.resize(keep); - return move_this(); - } - M slice(size_t idx, size_t len) { - auto off = mem.begin() + idx; - return M(std::vector(off, off + len)); - } - // PreMem drop(size_t d) { return PreMem(mem.drop(d)); } - const std::vector& get_mem() { return mem; } -}; - -class Mem: public PreMem { - // endian-ness: https://stackoverflow.com/questions/46289636/z3-endian-ness-mixup-between-extract-and-concat - static PtrVal q_extract(PtrVal v0, size_t b0, size_t b, size_t e, size_t e0) { - return bv_extract(v0, (e - b0) * 8 - 1, (b - b0) * 8); - } - - static PtrVal q_concat(PtrVal v1, PtrVal v2) { - return int_op_2(iOP::op_concat, v2, v1); - } - - struct Segment { - PtrVal val; size_t begin, size, end; - Segment(PtrVal v, size_t b, size_t s): val(v), begin(b), size(s), end(b + s) { } - // assume intersection; no checks - Segment intersect(const Segment &rhs) const { - size_t b = std::max(begin, rhs.begin), e = std::min(end, rhs.end); - PtrVal v = (begin < b || e < end) ? q_extract(val, begin, b, e, end) : val; - return {v, b, e - b}; - } - Segment left_sub(const Segment &rhs) const { - PtrVal v = (rhs.begin > begin) ? q_extract(val, begin, begin, rhs.begin, end) : nullptr; - return {v, begin, rhs.begin}; - } - Segment right_sub(const Segment &lhs) const { - PtrVal v = (lhs.end < end) ? q_extract(val, begin, lhs.end, end, end) : nullptr; - return {v, lhs.end, end}; - } - }; - - Segment lookup(size_t idx, size_t size) const { - auto cur = mem[idx]; - if (!cur) { - size_t sz = 1; - while (sz < size && !mem[idx + sz]) sz++; - return { cur, idx, sz }; - } - while (std::dynamic_pointer_cast(cur)) cur = mem[--idx]; - return { cur, idx, size_t(cur->get_bw() + 7) / 8 }; - } - - bool is_intact(const Segment &seg) const { - for (size_t idx = seg.begin; idx < seg.end; ) { - auto s = lookup(idx, seg.end - idx); - if (s.begin < seg.begin || s.end > seg.end) - return false; - idx = s.end; - } - return true; - } - - void write_back(const Segment &seg, PtrVal v) { - mem[seg.begin] = v; - if (!seg.val) - for (size_t i = seg.begin + 1; i < seg.end; i++) - mem[i] = make_ShadowV(); - } - - static void possible_partial_undef(PtrVal &v) { - assert(v); - } - -public: - Mem(std::vector mem) : PreMem(std::move(mem)) {} - using PreMem::at; - using PreMem::update; - - PtrVal at(size_t idx, int size) { - auto first = lookup(idx, size); - auto part = first.intersect({nullptr, idx, size_t(size)}); - auto cur = part.val; - if (part.size < size) { - auto next = at(idx + part.size, size - part.size); - possible_partial_undef(cur); - possible_partial_undef(next); - cur = q_concat(cur, next); - } - return cur; - } - - Mem&& update(size_t idx, PtrVal val, int size) { - Segment newval {val, idx, size_t(size)}; - if (is_intact(newval)) { - for (idx = newval.begin; idx < newval.end; ) { - auto curval = lookup(idx, newval.end - idx); - auto v = (curval.begin == newval.begin) ? newval.val : make_ShadowV(); - write_back(curval, v); - idx = curval.end; - } - } - else { - for (idx = newval.begin; idx < newval.end; ) { - // load current - auto curval = lookup(idx, newval.end - idx); - auto newcur = newval.intersect(curval); - auto v_new = newcur.val; - auto v_head = curval.left_sub(newcur).val; - if (v_head) v_new = q_concat(v_head, v_new); - auto v_tail = curval.right_sub(newcur).val; - if (v_tail) v_new = q_concat(v_new, v_tail); - // store & step - write_back(curval, v_new); - idx = curval.end; - } - } - return move_this(); - } -}; - -class Frame { - public: - using Env = std::map; - using Cont = std::function; - Cont cont; - private: - Env env; - public: - Frame(Cont ct): cont(ct), env() {} - Frame(Env env) : env(std::move(env)) {} - Frame() : env(std::map{}) {} - size_t size() { return env.size(); } - PtrVal lookup_id(Id id) const { return env.at(id); } - Frame&& assign(Id id, PtrVal v) { - env.insert_or_assign(id, v); - return std::move(*this); - } - Frame&& assign_seq(const std::vector& ids, const std::vector& vals) { - for (size_t i = 0; i < ids.size(); i++) { - env.insert_or_assign(ids[i], vals[i]); - } - return std::move(*this); - } -}; - -class Stack { - private: - Mem mem; - std::vector env; - PtrVal errno_location; - public: - Stack(Mem mem, std::vector env, PtrVal errno_location) : mem(std::move(mem)), env(std::move(env)), errno_location(std::move(errno_location)) {} - size_t mem_size() { return mem.size(); } - size_t frame_depth() { return env.size(); } - PtrVal vararg_loc() { return env[env.size()-2].lookup_id(vararg_id); } - Stack&& init_error_loc() { - auto error_addr = mem.size(); - mem.alloc(8); - mem.update(error_addr, make_IntV(0, 32), 4); - errno_location = make_LocV(error_addr, LocV::kStack, 4); - return std::move(*this); - } - PtrVal error_loc() { return errno_location; } - typename Frame::Cont pop(size_t keep) { - auto &it = env.at(env.size() - 1); - auto ret = it.cont; - mem.take(keep); - env.resize(env.size() - 1); - return ret; - } - Stack&& push() { - return push(Frame()); - } - Stack&& push(Frame f) { - env.push_back(std::move(f)); - return std::move(*this); - } - - Stack&& push(std::function cont) { - return push(Frame(cont)); - } - - Stack&& assign(Id id, PtrVal val) { - env.back().assign(id, val); - return std::move(*this); - } - Stack&& assign_seq(const std::vector& ids, std::vector vals) { - // varargs - size_t id_size = ids.size(); - if (id_size > 0) { - if (ids.back() == vararg_id) { - auto msize = mem.size(); - for (size_t i = id_size - 1; i < vals.size(); i++) { - // FIXME: magic value 8, as vararg is retrived from +8 address - mem.append(vals[i], 7); - } - if (mem.size() == msize) mem.alloc(8); - vals.resize(id_size - 1); - vals.push_back(make_LocV(msize, LocV::kStack, mem.size() - msize)); - } - env.back().assign_seq(ids, vals); - } - return std::move(*this); - } - PtrVal lookup_id(Id id) { return env.back().lookup_id(id); } - - PtrVal at(size_t idx) { return mem.at(idx); } - PtrVal at(size_t idx, int size) { return mem.at(idx, size); } - PtrVal at_struct(size_t idx, int size) { - auto ret = make_simple(mem.slice(idx, size).get_mem()); - return hashconsing(ret); - } - Stack&& update(size_t idx, PtrVal val) { - mem.update(idx, val); - return std::move(*this); - } - Stack&& update(size_t idx, PtrVal val, int size) { - mem.update(idx, val, size); - return std::move(*this); - } - Stack&& alloc(size_t size) { - mem.alloc(size); - return std::move(*this); - } -}; - -class PC { - private: - std::vector pc; - public: - PC(std::vector pc) : pc(std::move(pc)) {} - PC&& add(PtrVal e) { - pc.push_back(e); - return std::move(*this); - } - PC&& add_set(const std::set& new_pc) { - pc.insert(pc.end(), new_pc.begin(), new_pc.end()); - return std::move(*this); - } - PC&& add_set(const List& new_pc) { - pc.insert(pc.end(), new_pc.begin(), new_pc.end()); - return std::move(*this); - } - PC&& pop_back() { - pc.pop_back(); - return std::move(*this); - } - const std::vector& get_path_conds() { return pc; } - PtrVal get_last_cond() { - if (pc.size() > 0) return pc.back(); - return nullptr; - } - PC&& replace_last_cond(PtrVal e) { - if (pc.size() == 0) return std::move(*this); - pc[pc.size()-1] = e; - return std::move(*this); - } - void print() { print_set(pc); } -}; - -#include "metadata.hpp" - -class SS { - private: - Mem heap; - Stack stack; - PC pc; - MetaData meta; - FS fs; - public: - SS(Mem heap, Stack stack, PC pc, MetaData meta) : - heap(std::move(heap)), stack(std::move(stack)), pc(std::move(pc)), meta(std::move(meta)), fs(initial_fs) {} - SS(Mem heap, Stack stack, PC pc, MetaData meta, FS fs) : - heap(std::move(heap)), stack(std::move(stack)), pc(std::move(pc)), meta(std::move(meta)), fs(std::move(fs)) {} - SS(List heap, Stack stack, PC pc, MetaData meta) : - heap(std::move(std::vector(heap.begin(), heap.end()))), stack(std::move(stack)), pc(std::move(pc)), meta(std::move(meta)), fs(initial_fs) {} - SS fork() { return SS(heap, stack, pc, std::move(meta.fork()), fs); } - SS copy() { return *this; } - PtrVal env_lookup(Id id) { return stack.lookup_id(id); } - size_t heap_size() { return heap.size(); } - size_t stack_size() { return stack.mem_size(); } - size_t fresh_stack_addr() { return stack_size(); } - size_t frame_depth() { return frame_depth(); } - PtrVal at(PtrVal addr) { - auto loc = std::dynamic_pointer_cast(addr); - ASSERT(loc != nullptr, "Lookup an non-address value"); - if (loc->k == LocV::kStack) return stack.at(loc->l); - return heap.at(loc->l); - } - PtrVal at(PtrVal addr, int size) { - auto loc = std::dynamic_pointer_cast(addr); - if (loc != nullptr) { - if (loc->k == LocV::kStack) return stack.at(loc->l, size); - return heap.at(loc->l, size); - } else if (auto symloc = std::dynamic_pointer_cast(addr)) { - // TODO GW: should refactor this piece of code, strive for readability and maintainability - ASSERT(symloc != nullptr && symloc->size >= size, "Lookup an non-address value"); - std::vector> result; - auto offsym = std::dynamic_pointer_cast(symloc->off); - ASSERT(offsym && (offsym->get_bw() == addr_index_bw), "Invalid sym offset"); - bool reach_limit = (max_sym_array_size > 0) && (symloc->size >= max_sym_array_size); - bool resolve_once = reach_limit || (SymLocStrategy::one == symloc_strategy); - if (resolve_once || SymLocStrategy::feasible == symloc_strategy) { - int cnt_bound = -1; - int cnt = 0; - if (resolve_once) - cnt_bound = 1; - auto low_cond = int_op_2(iOP::op_sge, offsym, make_IntV(0, addr_index_bw)); - auto high_cond = int_op_2(iOP::op_sle, offsym, make_IntV(symloc->size - size, addr_index_bw)); - auto pc2 = pc; - pc2.add(low_cond).add(high_cond); - auto res = get_sat_value(pc2, offsym); - while (res.first) { - cnt++; - int offset_val = res.second; - auto t_cond = int_op_2(iOP::op_eq, offsym, make_IntV(offset_val, offsym->get_bw())); - result.push_back(std::make_pair(t_cond, offset_val)); - if (cnt_bound == cnt) - break; - pc2.add(SymV::neg(t_cond)); - res = get_sat_value(pc2, offsym); - } - ASSERT(cnt > 0, "No satisfiable offset value"); - } else { - ASSERT(SymLocStrategy::all == symloc_strategy, "Bad symloc strategy"); - for (int offset_val=0; offset_val <= (symloc->size - size); offset_val++) { - auto t_cond = int_op_2(iOP::op_eq, offsym, make_IntV(offset_val, offsym->get_bw())); - result.push_back(std::make_pair(t_cond, offset_val)); - } - } - PtrVal read_res = nullptr; - for(auto it = result.rbegin(); it != result.rend(); ++it) { - auto val = at(make_LocV(symloc->base, symloc->k, symloc->size, it->second), size); - if (result.rbegin() == it) { - read_res = val; - } else { - read_res = ite(it->first, val, read_res); - } - } - ASSERT(read_res, "Bad result"); - // TODO: should we modify the pc to add the in-bound constraints - return read_res; - } else if (auto symvite = std::dynamic_pointer_cast(addr)) { - ASSERT(iOP::op_ite == symvite->rator, "Invalid memory read by symv index"); - return ite((*symvite)[0], at((*symvite)[1], size), at((*symvite)[2], size)); - } - ABORT("dereferenceing a nullptr"); - } - PtrVal at_struct(PtrVal addr, int size) { - auto loc = std::dynamic_pointer_cast(addr); - ASSERT(loc != nullptr, "Lookup an non-address value"); - if (loc->k == LocV::kStack) return stack.at_struct(loc->l, size); - auto ret = make_simple(heap.slice(loc->l, size).get_mem()); - return hashconsing(ret); - } - List at_seq(PtrVal addr, int count) { - auto s = std::dynamic_pointer_cast(at_struct(addr, count)); - ASSERT(s, "failed to read struct"); - return s->fs; - } - PtrVal heap_lookup(size_t addr) { return heap.at(addr, -1); } - uint64_t get_ssid() { return meta.ssid; } - BlockLabel incoming_block() { return meta.bb; } - bool has_cover_new() {return meta.has_cover_new; } - List get_sym_objs() { return meta.sym_objs; } - int count_name(const std::string& name) { return meta.count_name(name); } - std::string get_unique_name(const std::string& name) { - unsigned id = 0; - std::string uniqueName = name; - while (meta.count_name(uniqueName)) { - uniqueName = name + "_" + std::to_string(++id); - } - return uniqueName; - } - List get_preferred_cex() { return meta.preferred_cex; } - SS&& alloc_stack(size_t size) { - stack.alloc(size); - return std::move(*this); - } - SS&& alloc_heap(size_t size) { - heap.alloc(size); - return std::move(*this); - } - SS&& update(PtrVal addr, PtrVal val) { - auto loc = std::dynamic_pointer_cast(addr); - ASSERT(loc != nullptr, "Lookup an non-address value"); - if (loc->k == LocV::kStack) - stack.update(loc->l, val); - else - heap.update(loc->l, val); - return std::move(*this); - } - SS&& update(PtrVal addr, PtrVal val, int size) { - auto loc = std::dynamic_pointer_cast(addr); - ASSERT(loc != nullptr, "Lookup an non-address value"); - if (loc->k == LocV::kStack) - stack.update(loc->l, val, size); - else - heap.update(loc->l, val, size); - return std::move(*this); - } - SS&& update_seq(PtrVal addr, List vals) { - for (int i = 0; i < vals.size(); i++) { - update(addr + i, vals.at(i)); - } - return std::move(*this); - } - SS&& push() { - stack.push(); - return std::move(*this); - } - SS&& push(std::function cont) { - stack.push(cont); - return std::move(*this); - } - typename Frame::Cont pop(size_t keep) { - return stack.pop(keep); - } - SS&& assign(Id id, PtrVal val) { - stack.assign(id, val); - return std::move(*this); - } - SS&& assign_seq(const std::vector& ids, std::vector vals) { - stack.assign_seq(ids, std::move(vals)); - return std::move(*this); - } - SS&& assign_seq(List ids, List vals) { - return assign_seq( - std::vector(ids.begin(), ids.end()), - std::vector(vals.begin(), vals.end())); - } - SS&& heap_append(const std::vector& vals) { - heap.append(vals); - return std::move(*this); - } - SS&& heap_append(List vals) { - return heap_append(std::vector(vals.begin(), vals.end())); - } - SS&& add_PC(PtrVal e) { - pc.add(e); - return std::move(*this); - } - SS&& add_PC_cet(const std::set& s) { - pc.add_set(s); - return std::move(*this); - } - SS&& add_PC_set(const List& s) { - std::set cs(s.begin(), s.end()); - pc.add_set(cs); - return std::move(*this); - } - SS&& add_incoming_block(BlockLabel blabel) { - meta.add_incoming_block(blabel); - return std::move(*this); - } - SS&& cover_block(BlockLabel new_bb) { - meta.cover_block(new_bb); - return std::move(*this); - } - SS&& add_symbolic(const std::string& name, int size, bool is_whole) { - //ASSERT(0 == meta.count_name(name), "non unique name"); - meta.add_symbolic(name, size, is_whole); - return std::move(*this); - } - SS&& add_cex(const PtrVal& cex) { - meta.add_cex(cex); - return std::move(*this); - } - SS&& init_arg() { - ASSERT(stack.mem_size() == 0, "Stack is not new"); - // Todo: Can adapt argv to be located somewhere other than 0 as well. - // Configure a global LocV pointing to it. - unsigned num_args = cli_argv.size(); - // allocate space for the array of pointers - // with additional ternimating null for empty envp array - // and an additional terminating null that uclibc seems to expect for the ELF header. - // Todo: support non-empty envp - auto stack_ptr = make_LocV(stack.mem_size(), LocV::kStack, (num_args + 3) * 8); - alloc_stack((num_args + 3) * 8); - - // copy each argument onto the stack, and update the pointers - for (int i = 0; i < num_args; ++i) { - auto arg = cli_argv.at(i); - auto addr = stack_size(); // top of the stack - alloc_stack(arg.size()); - auto arg_ptr = make_LocV(addr, LocV::kStack, arg.size()); - update_seq(arg_ptr, arg); // copy the values to the newly allocated space - update(stack_ptr + (8 * i), arg_ptr); // copy the pointer value - } - update(stack_ptr + (8 * num_args), make_LocV_null()); // terminate the array of pointers - update(stack_ptr + (8 * (num_args + 1)), make_LocV_null()); // terminate the empty envp array - update(stack_ptr + (8 * (num_args + 2)), make_LocV_null()); // additional terminating null that uclibc seems to expect for the ELF header - return std::move(*this); - } - PC& get_PC() { return pc; } - PC copy_PC() { return pc; } - void set_PC(PC _pc) { pc = _pc; } - const std::vector& get_path_conds() { return pc.get_path_conds(); } - // TODO temp solution - PtrVal vararg_loc() { return stack.vararg_loc(); } - SS&& init_error_loc() { - stack.init_error_loc(); - return std::move(*this); - } - PtrVal error_loc() { return stack.error_loc(); } - void set_fs(FS new_fs) { fs = new_fs; } - FS get_fs() { return fs; } -}; - -using SSVal = std::pair; - -inline const Mem mt_mem = Mem(std::vector{}); -inline const Stack mt_stack = Stack(mt_mem, std::vector{}, nullptr); -inline const PC mt_pc = PC(std::vector{}); -inline const uint64_t mt_ssid = 1; -inline const BlockLabel mt_bb = 0; -inline const MetaData mt_meta = MetaData(mt_ssid, mt_bb, false, List{}, List{}); -inline const SS mt_ss = SS(mt_mem, mt_stack, mt_pc, mt_meta); - -inline const List mt_path_result = List{}; - -using func_t = List (*)(SS&, List); - -inline PtrVal make_FunV(func_t f) { - auto ret = make_simple>(f); - return hashconsing(ret); -} - -inline List direct_apply(PtrVal v, SS ss, List args) { - auto f = std::dynamic_pointer_cast>(v); - if (f) return f->f(ss, args); - ABORT("direct_apply: not applicable"); -} - -using func_cps_t = std::monostate (*)(SS&, List, std::function); - -inline PtrVal make_CPSFunV(func_cps_t f) { - auto ret = make_simple>(f); - return hashconsing(ret); -} - -inline std::monostate cps_apply(PtrVal v, SS ss, List args, std::function k) { - auto f = std::dynamic_pointer_cast>(v); - if (f) return f->f(ss, args, k); - ABORT("cps_apply: not applicable"); -} - -inline std::monostate cont_apply(std::function cont, SS& ss, PtrVal val) { - return cont(ss, val); -} - -#endif diff --git a/headers/gensym/state_pure.hpp b/headers/gensym/state_pure.hpp deleted file mode 100644 index 44eca084..00000000 --- a/headers/gensym/state_pure.hpp +++ /dev/null @@ -1,645 +0,0 @@ -#ifndef GS_STATE_PURE_HEADER -#define GS_STATE_PURE_HEADER - -/* Memory, stack, and symbolic state representation */ - -// Note (5/17): now using a byte-oriented layout - -template -class PreMem: public Printable { - protected: - List mem; - public: - std::string toString() const override { - std::ostringstream ss; - ss << "PreMem("; - for (int i = 0; i < mem.size(); i++) { - auto ptrval = mem.at(i); - ss << i << ": " << ptrval_to_string(ptrval) << ", "; - } - ss << ")"; - return ss.str(); - } - PreMem(List mem) : mem(mem) {} - size_t size() { return mem.size(); } - V at(size_t idx) { return mem.at(idx); } - M update(size_t idx, const V& val) { - ASSERT(idx < mem.size(), "PreMem update index out of bound"); - return M(mem.set(idx, val)); - } - M append(V val) { return M(mem.push_back(val)); } - M append(V val, size_t padding) { - size_t idx = mem.size(); - return M(alloc(padding + 1).update(idx, val)); - } - M append(List vs) { return M(mem + vs); } - M alloc(size_t size) { - auto m = mem.transient(); - for (int i = 0; i < size; i++) { m.push_back(make_UnInitV()); } - return M(m.persistent()); - } - M take(size_t keep) { return M(mem.take(keep)); } - M drop(size_t d) { return M(mem.drop(d)); } - List get_mem() { return mem; } -}; - -/* Mem0 is the base memory model that assumes integer/symbolic values are - * stored as sequences of bytes (following little endian), i.e. every IntV/SymV - * in an instance of Mem0 has `bw` of 8. - * LocV/FunV values are stored with additional ``shadow'' values, which don't - * store information but simply serve as placeholders, prohibiting reading or - * updating a fragment of a location/function value. - * This version also disallows reading uninitialized values (represented by nullptr), - * which might be overly constrained. - */ -class Mem0 : public PreMem { -private: - bool is_well_formed() const { - size_t i = 0; - while (i < mem.size()) { - auto v = mem.at(i); - if (std::dynamic_pointer_cast(v) || - std::dynamic_pointer_cast(v)) { - ASSERT(v->get_bw() <= 8, "Bitwidth too large"); - i += 1; - } else if (std::dynamic_pointer_cast(v)) { - // FIXME: function value - //std::dynamic_pointer_cast(v)) { - for (int j = i+1; j <= i + 7; j++) { - ASSERT(std::dynamic_pointer_cast(mem.at(j)), - "Loc/Fun value does not properly shadow its region"); - } - i += 7; - } else if (auto fun_v = std::dynamic_pointer_cast(v)) { - for (int j = i+1; j <= i + 3; j++) { - ASSERT(std::dynamic_pointer_cast(mem.at(j)), - "Float value does not properly shadow its region"); - } - i += 3; - } else if (v == nullptr) { - std::cout << "Warning: nullptr at " << i << " of an Mem0\n"; - i += 1; - } else { - ABORT("Unknown value"); - } - } - return true; - } -public: - using PreMem::at; - using PreMem::update; - Mem0(List mem) : PreMem(mem) {} - PtrVal at(size_t idx, size_t byte_size) { - auto val = mem.at(idx); - if (std::dynamic_pointer_cast(val) || std::dynamic_pointer_cast(val)) - return Value::from_bytes(Vec::slice(mem, idx, byte_size)); - ASSERT(val != nullptr, "Reading an uninitialized (nullptr) value"); - ASSERT(!std::dynamic_pointer_cast(val), "Reading a shadowed value"); - return val; - } - Mem0 update(size_t idx, const PtrVal& val, size_t byte_size) { - ASSERT(!std::dynamic_pointer_cast(mem.at(idx)), "Updating a shadowed value"); - ASSERT(val->get_byte_size() == byte_size, "Mismatched value and size to write"); - auto bytes = val->to_bytes(); - ASSERT(bytes.size() == byte_size, "Size of byte-representation of value not equal to argument byte_size"); - auto mem = this->mem.transient(); - for (size_t i = 0; i < byte_size; i++) { mem.set(idx+i, bytes.at(i)); } - return Mem0(mem.persistent()); - } -}; - -/* MemIdxShadow only works with _indexed_ shadow values. - */ -class MemIdxShadow : public PreMem { -public: - using PreMem::at; - using PreMem::update; - MemIdxShadow(List mem) : PreMem(mem) {} - PtrVal at(size_t idx, size_t byte_size) { - auto val = mem.at(idx); - if (std::dynamic_pointer_cast(val) || std::dynamic_pointer_cast(val)) { - auto val_size = val->get_byte_size(); - if (val_size == byte_size) return val; - if (val_size > byte_size) return Value::from_bytes(val->to_bytes().take(byte_size)); - if (val_size < byte_size) return Value::from_bytes_shadow(Vec::slice(mem, idx, byte_size)); - } - if (auto sv = std::dynamic_pointer_cast(val)) { - auto src = mem.at(idx + sv->offset); - ASSERT(!std::dynamic_pointer_cast(src), "Reading shadow of a LocV"); // XXX function too - auto src_bytes = src->to_bytes().drop(-sv->offset); - if (src_bytes.size() == byte_size) return Value::from_bytes(std::move(src_bytes)); - if (src_bytes.size() > byte_size) return Value::from_bytes(src_bytes.take(byte_size)); - if (src_bytes.size() < byte_size) - return Value::from_bytes_shadow(src_bytes + Vec::slice(mem, idx+src_bytes.size(), byte_size-src_bytes.size())); - } - ASSERT(val != nullptr, "Reading a nullptr value"); - return val; - } - MemIdxShadow update(size_t idx, const PtrVal& val, size_t byte_size) { - ASSERT(val->get_byte_size() == byte_size, "Mismatched value and size to write: " << val->get_byte_size() << " vs " << byte_size); - auto old_val = mem.at(idx); - auto mem = this->mem.transient(); - if (auto sv = std::dynamic_pointer_cast(old_val)) { - auto src_idx = idx + sv->offset; - auto src = mem.at(src_idx); - auto src_bytes = src->to_bytes(); - // We don't need to write the whole byte seq of src, since the part of it will be overwritten anyway - for (size_t i = 0; i < abs(sv->offset); i++) { mem.set(src_idx+i, src_bytes.at(i)); } - for (size_t i = abs(sv->offset)+byte_size; i < src_bytes.size(); i++) { mem.set(src_idx+i, src_bytes.at(i)); } - } - auto bytes = val->to_bytes_shadow(); - for (size_t i = 0; i < byte_size; i++) { - auto w = mem.at(idx + i); - if (w && byte_size-i < w->get_byte_size()) { - ASSERT(std::dynamic_pointer_cast(w) || std::dynamic_pointer_cast(w), "Overwriting a LocV or FunV"); - // Some value to be overwritten is extended beyond byte_size, needs to reify its shadowed value - auto w_bytes = w->to_bytes(); - // We don't need to write the whole byte seq of w, since the left-hand side part of it will be overwritten anyway - for (size_t j = byte_size-i; j < w_bytes.size(); j++) { mem.set(idx + i + j, w_bytes.at(j)); } - } - mem.set(idx + i, bytes.at(i)); - } - return MemIdxShadow(mem.persistent()); - } -}; - -class MemShadow: public PreMem { - // endian-ness: https://stackoverflow.com/questions/46289636/z3-endian-ness-mixup-between-extract-and-concat - static PtrVal q_extract(PtrVal v0, size_t b0, size_t b, size_t e, size_t e0) { - return bv_extract(v0, (e - b0) * 8 - 1, (b - b0) * 8); - } - - static PtrVal q_concat(PtrVal v1, PtrVal v2) { - return int_op_2(iOP::op_concat, v2, v1); - } - - struct Segment { - PtrVal val; size_t begin, size, end; - Segment(PtrVal v, size_t b, size_t s): val(v), begin(b), size(s), end(b + s) { } - // assume intersection; no checks - Segment intersect(const Segment &rhs) const { - size_t b = std::max(begin, rhs.begin), e = std::min(end, rhs.end); - PtrVal v = (begin < b || e < end) ? q_extract(val, begin, b, e, end) : val; - return {v, b, e - b}; - } - Segment left_sub(const Segment &rhs) const { - PtrVal v = (rhs.begin > begin) ? q_extract(val, begin, begin, rhs.begin, end) : nullptr; - return {v, begin, rhs.begin}; - } - Segment right_sub(const Segment &lhs) const { - PtrVal v = (lhs.end < end) ? q_extract(val, begin, lhs.end, end, end) : nullptr; - return {v, lhs.end, end}; - } - }; - - Segment lookup(size_t idx, size_t size) const { - auto cur = mem.at(idx); - if (!cur) { - size_t sz = 1; - while (sz < size && !mem.at(idx + sz)) sz++; - return { cur, idx, sz }; - } - while (std::dynamic_pointer_cast(cur)) cur = mem.at(--idx); - return { cur, idx, size_t(cur->get_bw() + 7) / 8 }; - } - - bool is_intact(const Segment &seg) const { - for (size_t idx = seg.begin; idx < seg.end; ) { - auto s = lookup(idx, seg.end - idx); - if (s.begin < seg.begin || s.end > seg.end) - return false; - idx = s.end; - } - return true; - } - - using ListTransient = List::transient_type; - static void write_back(ListTransient &mem, const Segment &seg, PtrVal v) { - mem.set(seg.begin, v); - if (!seg.val) - for (size_t i = seg.begin + 1; i < seg.end; i++) - mem.set(i, make_ShadowV()); - } - - static void possible_partial_undef(PtrVal &v) { - assert(v); - } - -public: - MemShadow(List mem) : PreMem(mem) { } - using PreMem::at; - using PreMem::update; - - PtrVal at(size_t idx, int size) { - auto first = lookup(idx, size); - auto part = first.intersect({nullptr, idx, size_t(size)}); - auto cur = part.val; - if (part.size < size) { - auto next = at(idx + part.size, size - part.size); - possible_partial_undef(cur); - possible_partial_undef(next); - cur = q_concat(cur, next); - } - return cur; - } - - MemShadow update(size_t idx, const PtrVal& val, int size) { - auto mem = this->mem.transient(); - Segment newval {val, idx, size_t(size)}; - if (is_intact(newval)) { - for (idx = newval.begin; idx < newval.end; ) { - auto curval = lookup(idx, newval.end - idx); - auto v = (curval.begin == newval.begin) ? newval.val : make_ShadowV(); - write_back(mem, curval, v); - idx = curval.end; - } - } - else { - for (idx = newval.begin; idx < newval.end; ) { - // load current - auto curval = lookup(idx, newval.end - idx); - auto newcur = newval.intersect(curval); - auto v_new = newcur.val; - auto v_head = curval.left_sub(newcur).val; - if (v_head) v_new = q_concat(v_head, v_new); - auto v_tail = curval.right_sub(newcur).val; - if (v_tail) v_new = q_concat(v_new, v_tail); - // store & step - write_back(mem, curval, v_new); - idx = curval.end; - } - } - return MemShadow(mem.persistent()); - } -}; - -//using Mem = MemIdxShadow; -using Mem = MemShadow; - -class Frame: public Printable { - public: - using Env = immer::map; - private: - Env env; - public: - std::string toString() const override { - std::ostringstream ss; - ss << "Frame("; - for (auto p : env) { - ss << p.first << ": " << ptrval_to_string(p.second) << ", "; - } - ss << ")"; - return ss.str(); - } - Frame(Env env) : env(env) {} - Frame() : env(immer::map{}) {} - size_t size() { return env.size(); } - PtrVal lookup_id(Id id) const { return env.at(id); } - Frame assign(Id id, const PtrVal& v) const { return Frame(env.insert({id, v})); } - Frame assign_seq(List ids, List vals) const { - Env env1 = env; - for (size_t i = 0; i < ids.size(); i++) { - env1 = env1.insert({ids.at(i), vals.at(i)}); - } - return Frame(env1); - } -}; - -class Stack: public Printable { - private: - Mem mem; - List env; - PtrVal errno_location; - public: - std::string toString() const override { - std::ostringstream ss; - ss << "Stack(" << - "mem=" << mem << ", " << - "env=" << vec_to_string(env) << - " errno_location=" << *errno_location << - ")"; - return ss.str(); - } - Stack(Mem mem, List env, PtrVal errno_location) : mem(mem), env(env), errno_location(errno_location) {} - size_t mem_size() { return mem.size(); } - size_t frame_depth() { return env.size(); } - PtrVal vararg_loc() { return env.at(env.size()-2).lookup_id(vararg_id); } - Stack init_error_loc() { - auto updated_mem = mem; - auto error_addr = mem.size(); - updated_mem = updated_mem.alloc(8); - updated_mem = updated_mem.update(error_addr, make_IntV(0, 32), 4); - auto error_loc = make_LocV(error_addr, LocV::kStack, 4); - return Stack(updated_mem, env, error_loc); - } - PtrVal error_loc() { return errno_location; } - Stack pop(size_t keep) { return Stack(mem.take(keep), env.take(env.size()-1), errno_location); } - Stack push() { return Stack(mem, env.push_back(Frame()), errno_location); } - Stack push(Frame f) { return Stack(mem, env.push_back(f), errno_location); } - - Stack assign(Id id, const PtrVal& val) { - return Stack(mem, env.update(env.size()-1, [&](auto f) { return f.assign(id, val); }), errno_location); - } - Stack assign_seq(List ids, List vals) { - // varargs - size_t id_size = ids.size(); - if (id_size == 0) return Stack(mem, env, errno_location); - if (ids.at(id_size - 1) == vararg_id) { - auto updated_mem = mem; - for (size_t i = id_size - 1; i < vals.size(); i++) { - // FIXME: magic value 8, as vararg is retrived from +8 address - updated_mem = updated_mem.append(vals.at(i), 7); - } - if (updated_mem.size() == mem.size()) updated_mem = updated_mem.alloc(8); - auto updated_vals = vals.take(id_size - 1).push_back(make_LocV(mem.size(), LocV::kStack, updated_mem.size() - mem.size())); - return Stack(updated_mem, env.update(env.size()-1, [&](auto f) { return f.assign_seq(ids, updated_vals); }), errno_location); - } else { - return Stack(mem, env.update(env.size()-1, [&](auto f) { return f.assign_seq(ids, vals); }), errno_location); - } - } - PtrVal lookup_id(Id id) { return env.back().lookup_id(id); } - - PtrVal at(size_t idx) { return mem.at(idx); } - PtrVal at(size_t idx, int size) { return mem.at(idx, size); } - PtrVal at_struct(size_t idx, int size) { - auto ret = make_simple(mem.take(idx + size).drop(idx).get_mem()); - return hashconsing(ret); - } - Stack update(size_t idx, const PtrVal& val) { return Stack(mem.update(idx, val), env, errno_location); } - Stack update(size_t idx, const PtrVal& val, int size) { return Stack(mem.update(idx, val, size), env, errno_location); } - Stack alloc(size_t size) { return Stack(mem.alloc(size), env, errno_location); } -}; - -#include "unionfind.hpp" - -class PC: public Printable { - public: - List conds; - UnionFind uf; - immer::set_transient vars; - - PC(List conds) : conds(conds) { - auto start = steady_clock::now(); - for (auto& c : conds) { - for (auto& v : c->to_SymV()->vars) { - vars.insert(v); - uf.join(v, c); - } - } - auto end = steady_clock::now(); - cons_indep_time += duration_cast(end - start).count(); - } - PC add(const PtrVal& e) { return PC(conds.push_back(e)); } - bool contains(PtrVal e) { - return uf.parent.find(e) != nullptr; - } - List& get_path_conds() { return conds; } - PtrVal get_last_cond() { - if (conds.size() > 0) return conds.back(); - return nullptr; - } - std::string toString() const override { - std::ostringstream ss; - ss << "PC(" << vec_to_string(conds) << ")"; - return ss.str(); - } -}; - -#include "metadata.hpp" - -class SS: public Printable { - private: - Mem heap; - Stack stack; - PC pc; - MetaData meta; - FS fs; - public: - std::string toString() const override { - std::ostringstream ss; - ss << "SS(" << - "stack => {{ " << stack << " }}, " << - "heap => {{ " << heap << " }}, " << - "pc => {{ " << pc << " }}, " << - "meta => {{ " << meta << " }}, " << - "fs => {{ " << fs << " }}, " << - ")"; - return ss.str(); - } - SS(Mem heap, Stack stack, PC pc, MetaData meta) : heap(heap), stack(stack), pc(pc), meta(meta), fs(initial_fs) {} - SS(Mem heap, Stack stack, PC pc, MetaData meta, FS fs) : heap(heap), stack(stack), pc(pc), meta(meta), fs(fs) {} - SS fork() { return SS(heap, stack, pc, meta.fork(), fs); } - PtrVal env_lookup(Id id) { return stack.lookup_id(id); } - size_t heap_size() { return heap.size(); } - size_t stack_size() { return stack.mem_size(); } - size_t fresh_stack_addr() { return stack_size(); } - size_t frame_depth() { return frame_depth(); } - PtrVal at_symloc(simple_ptr symloc, size_t size) { - ASSERT(symloc != nullptr && symloc->size >= size, "Lookup an non-address value"); - std::vector> result; - auto offsym = std::dynamic_pointer_cast(symloc->off); - ASSERT(offsym && (offsym->get_bw() == addr_index_bw), "Invalid sym offset"); - bool reach_limit = (max_sym_array_size > 0) && (symloc->size >= max_sym_array_size); - bool resolve_once = reach_limit || (SymLocStrategy::one == symloc_strategy); - if (resolve_once || SymLocStrategy::feasible == symloc_strategy) { - int cnt_bound = -1; - int cnt = 0; - if (resolve_once) - cnt_bound = 1; - auto low_cond = int_op_2(iOP::op_sge, offsym, make_IntV(0, addr_index_bw)); - auto high_cond = int_op_2(iOP::op_sle, offsym, make_IntV(symloc->size - size, addr_index_bw)); - auto pc2 = pc.add(low_cond).add(high_cond); - auto res = get_sat_value(pc2, offsym); - while (res.first) { - cnt++; - int offset_val = res.second; - auto t_cond = int_op_2(iOP::op_eq, offsym, make_IntV(offset_val, offsym->get_bw())); - result.push_back(std::make_pair(t_cond, offset_val)); - if (cnt_bound == cnt) - break; - pc2 = pc2.add(SymV::neg(t_cond)); - res = get_sat_value(pc2, offsym); - } - ASSERT(cnt > 0, "No satisfiable offset value"); - } else { - ASSERT(SymLocStrategy::all == symloc_strategy, "Bad symloc strategy"); - for (int offset_val=0; offset_val <= (symloc->size - size); offset_val++) { - auto t_cond = int_op_2(iOP::op_eq, offsym, make_IntV(offset_val, offsym->get_bw())); - result.push_back(std::make_pair(t_cond, offset_val)); - } - } - PtrVal read_res = nullptr; - for(auto it = result.rbegin(); it != result.rend(); ++it) { - auto val = at(make_LocV(symloc->base, symloc->k, symloc->size, it->second), size); - if (result.rbegin() == it) { - read_res = val; - } else { - read_res = ite(it->first, val, read_res); - } - } - ASSERT(read_res, "Bad result"); - // Todo: should we modify the pc to add the in-bound constraints - return read_res; - } - PtrVal at_simpl(const PtrVal& addr) { - auto loc = std::dynamic_pointer_cast(addr); - ASSERT(loc != nullptr, "Lookup an non-address value"); - if (loc->k == LocV::kStack) return stack.at(loc->l); - return heap.at(loc->l); - } - PtrVal at(const PtrVal& addr, size_t size) { - auto loc = std::dynamic_pointer_cast(addr); - if (loc != nullptr) { - if (loc->k == LocV::kStack) return stack.at(loc->l, size); - return heap.at(loc->l, size); - } - if (auto symloc = std::dynamic_pointer_cast(addr)) return at_symloc(symloc, size); - if (auto symvite = std::dynamic_pointer_cast(addr)) { - ASSERT(iOP::op_ite == symvite->rator, "Invalid memory read by symv index"); - return ite((*symvite)[0], at((*symvite)[1], size), at((*symvite)[2], size)); - } - ABORT("dereferenceing a nullptr"); - } - PtrVal at_struct(const PtrVal& addr, size_t size) { - auto loc = std::dynamic_pointer_cast(addr); - ASSERT(loc != nullptr, "Lookup an non-address value"); - if (loc->k == LocV::kStack) return stack.at_struct(loc->l, size); - auto ret = make_simple(heap.take(loc->l + size).drop(loc->l).get_mem()); - return hashconsing(ret); - } - List at_seq(const PtrVal& addr, size_t count) { - auto s = std::dynamic_pointer_cast(at_struct(addr, count)); - ASSERT(s, "failed to read struct"); - return s->fs; - } - PtrVal heap_lookup(size_t addr) { return heap.at(addr, -1); } - uint64_t get_ssid() { return meta.ssid; } - BlockLabel incoming_block() { return meta.bb; } - bool has_cover_new() {return meta.has_cover_new; } - List get_sym_objs() { return meta.sym_objs; } - int count_name(const std::string& name) { return meta.count_name(name); } - std::string get_unique_name(const std::string& name) { - unsigned id = 0; - std::string uniqueName = name; - while (meta.count_name(uniqueName)) { - uniqueName = name + "_" + std::to_string(++id); - } - return uniqueName; - } - List get_preferred_cex() { return meta.preferred_cex; } - SS alloc_stack(size_t size) { return SS(heap, stack.alloc(size), pc, meta, fs); } - SS alloc_heap(size_t size) { return SS(heap.alloc(size), stack, pc, meta, fs); } - SS update_simpl(const PtrVal& addr, const PtrVal& val) { - auto loc = std::dynamic_pointer_cast(addr); - ASSERT(loc != nullptr, "Lookup an non-address value"); - if (loc->k == LocV::kStack) return SS(heap, stack.update(loc->l, val), pc, meta, fs); - return SS(heap.update(loc->l, val), stack, pc, meta, fs); - } - SS update(const PtrVal& addr, const PtrVal& val, size_t size) { - auto loc = std::dynamic_pointer_cast(addr); - ASSERT(loc != nullptr, "Lookup an non-address value"); - if (loc->k == LocV::kStack) return SS(heap, stack.update(loc->l, val, size), pc, meta, fs); - return SS(heap.update(loc->l, val, size), stack, pc, meta, fs); - } - SS update_seq(PtrVal addr, List vals) { - SS updated_ss = *this; - for (int i = 0; i < vals.size(); i++) { - updated_ss = updated_ss.update_simpl(addr + i, vals.at(i)); - } - return updated_ss; - } - SS push() { return SS(heap, stack.push(), pc, meta, fs); } - SS pop(size_t keep) { return SS(heap, stack.pop(keep), pc, meta, fs); } - SS assign(Id id, const PtrVal& val) { return SS(heap, stack.assign(id, val), pc, meta, fs); } - SS assign_seq(List ids, List vals) { - return SS(heap, stack.assign_seq(ids, vals), pc, meta, fs); - } - SS heap_append(List vals) { - return SS(heap.append(vals), stack, pc, meta, fs); - } - SS add_PC(const PtrVal& e) { return SS(heap, stack, pc.add(e), meta, fs); } - SS add_incoming_block(BlockLabel blabel) { return SS(heap, stack, pc, meta.add_incoming_block(blabel), fs); } - SS cover_block(BlockLabel new_bb) { return SS(heap, stack, pc, meta.cover_block(new_bb), fs); } - SS add_symbolic(const std::string& name, int size, bool is_whole) { - //ASSERT(0 == meta.count_name(name), "non unique name"); - return SS(heap, stack, pc, meta.add_symbolic(name, size, is_whole), fs); - } - SS add_cex(const PtrVal& cex) { return SS(heap, stack, pc, meta.add_cex(cex), fs); } - SS init_arg() { - ASSERT(stack.mem_size() == 0, "Stack is not new"); - // Todo: Can adapt argv to be located somewhere other than 0 as well. - // Configure a global LocV pointing to it. - - SS updated_ss = *this; - - unsigned num_args = cli_argv.size(); - // allocate space for the array of pointers - // with additional ternimating null for empty envp array - // and an additional terminating null that uclibc seems to expect for the ELF header. - // Todo: support non-empty envp - int stack_ptr_sz = (num_args + 3) * 8; - auto stack_ptr = make_LocV(stack.mem_size(), LocV::kStack, stack_ptr_sz, 0); // top of the stack - updated_ss = updated_ss.alloc_stack(stack_ptr_sz); - - // copy each argument onto the stack, and update the pointers - for (int i = 0; i < num_args; ++i) { - auto arg = cli_argv.at(i); - auto arg_ptr = make_LocV(updated_ss.stack_size(), LocV::kStack, arg.size(), 0); // top of the stack - updated_ss = updated_ss.alloc_stack(arg.size()); - updated_ss = updated_ss.update_seq(arg_ptr, arg); // copy the values to the newly allocated space - updated_ss = updated_ss.update_simpl(stack_ptr + (8 * i), arg_ptr); // copy the pointer value - } - updated_ss = updated_ss.update_simpl(stack_ptr + (8 * num_args), make_LocV_null()); // terminate the array of pointers - updated_ss = updated_ss.update_simpl(stack_ptr + (8 * (num_args + 1)), make_LocV_null()); // terminate the empty envp array - updated_ss = updated_ss.update_simpl(stack_ptr + (8 * (num_args + 2)), make_LocV_null()); // additional terminating null that uclibc seems to expect for the ELF header - - return updated_ss; - } - SS init_error_loc() { return SS(heap, stack.init_error_loc(), pc, meta, fs); } - PC& get_PC() { return pc; } - PC copy_PC() { return pc; } - // TODO temp solution - PtrVal vararg_loc() { return stack.vararg_loc(); } - PtrVal error_loc() { return stack.error_loc(); } - void set_fs(FS new_fs) { fs = new_fs; } - FS get_fs() { return fs; } -}; - -using SSVal = std::pair; - -inline const Mem mt_mem = Mem(List{}); -inline const Stack mt_stack = Stack(mt_mem, List{}, nullptr); -inline const PC mt_pc = PC(List{}); -inline const uint64_t mt_ssid = 1; -inline const BlockLabel mt_bb = 0; -inline const MetaData mt_meta = MetaData(mt_ssid, mt_bb, false, List{}, List{}); -inline const SS mt_ss = SS(mt_mem, mt_stack, mt_pc, mt_meta); -inline const List mt_path_result = List{}; - -using func_t = List (*)(SS, List); - -inline PtrVal make_FunV(func_t f) { - auto ret = make_simple>(f); - return hashconsing(ret); -} - -inline List direct_apply(const PtrVal& v, const SS& ss, List args) { - auto f = std::dynamic_pointer_cast>(v); - if (f) return f->f(ss, args); - ABORT("direct_apply: not applicable"); -} - -using func_cps_t = std::monostate (*)(SS, List, std::function); - -inline PtrVal make_CPSFunV(func_cps_t f) { - auto ret = make_simple>(f); - return hashconsing(ret); -} - -inline std::monostate cps_apply(const PtrVal& v, const SS& ss, List args, std::function k) { - auto f = std::dynamic_pointer_cast>(v); - if (f) return f->f(ss, args, k); - ABORT("cps_apply: not applicable"); -} - -#endif diff --git a/runtime/runtime.cpp b/runtime/runtime.cpp index fcc02d01..db6edcfb 100644 --- a/runtime/runtime.cpp +++ b/runtime/runtime.cpp @@ -1,6 +1,5 @@ #include -#define IMPURE_STATE #include namespace gensym::runtime::v1 { diff --git a/src/main/scala/gensym/Driver.scala b/src/main/scala/gensym/Driver.scala index be52d528..8d3faf67 100644 --- a/src/main/scala/gensym/Driver.scala +++ b/src/main/scala/gensym/Driver.scala @@ -382,12 +382,6 @@ trait GenSym { } } -/* -trait PureState { self: GenSym => - override def extraFlags = "-D PURE_STATE" -} -*/ - trait ImpureState { self: GenSym => override def extraFlags = "-D IMPURE_STATE" } diff --git a/src/test/scala/gensym/OptExperiment.scala b/src/test/scala/gensym/OptExperiment.scala index 0ab36b05..e0422fb2 100644 --- a/src/test/scala/gensym/OptExperiment.scala +++ b/src/test/scala/gensym/OptExperiment.scala @@ -52,11 +52,10 @@ class Optimization extends TestGS { } } -/* // Test algorithm benchmarks class TestImpCPSOpt extends Optimization { val gs = new ImpCPSGS - Config.enableOpt + Global.config.enableOpt testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/kmpmatcher.ll"), "kmp_Opt", "@main", noArg, "--cons-indep --solver=z3", nPath(4181))) testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/mergesort.ll"), "mergeSort_Opt", "@main", noArg, "--cons-indep --solver=z3", nPath(5040))) testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/bubblesort.ll"), "bubbleSort_Opt", "@main", noArg, "--cons-indep --solver=z3", nPath(720))) @@ -65,35 +64,9 @@ class TestImpCPSOpt extends Optimization { testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/quicksort.ll"), "quicksort_Opt", "@main", noArg, "--cons-indep --solver=z3", nPath(5040))) } -class TestPureCPSOpt extends Optimization { - val gs = new PureCPSGS - Config.enableOpt - - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/mergesort.ll"), "mergeSort_Opt", "@main", noArg, "--solver=z3", nPath(5040))) - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/bubblesort.ll"), "bubbleSort_Opt", "@main", noArg, "--solver=z3", nPath(720))) - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/knapsack.ll"), "knapsack_Opt", "@main", noArg, "--solver=z3", nPath(1666))) - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/kmpmatcher.ll"), "kmp_Opt", "@main", noArg, "--solver=z3", nPath(4181))) - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/nqueen.ll"), "nqueen_Opt", "@main", noArg, "--solver=z3", nPath(1363))) - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/quicksort.ll"), "quicksort_Opt", "@main", noArg, "--solver=z3", nPath(5040))) -} -*/ - -/* -class TestPureCPSNoOpt extends Optimization { - val gs = new PureCPSGS - Config.disableOpt - - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/mergesort.ll"), "mergeSort_NoOpt", "@main", noArg, noOpt, nPath(5040))) - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/bubblesort.ll"), "bubbleSort_NoOpt", "@main", noArg, noOpt, nPath(720))) - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/knapsack.ll"), "knapsack_NoOpt", "@main", noArg, noOpt, nPath(1666))) - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/kmpmatcher.ll"), "kmp_NoOpt", "@main", noArg, noOpt, nPath(4181))) - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/nqueen.ll"), "nqueen_NoOpt", "@main", noArg, noOpt, nPath(1363))) - testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/quicksort.ll"), "quicksort_NoOpt", "@main", noArg, noOpt, nPath(5040))) -} - class TestImpCPSNoOpt extends Optimization { val gs = new ImpCPSGS - Config.disableOpt + Global.config.disableOpt testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/mergesort.ll"), "mergeSort_NoOpt", "@main", noArg, noOpt, nPath(5040))) testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/bubblesort.ll"), "bubbleSort_NoOpt", "@main", noArg, noOpt, nPath(720))) testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/knapsack.ll"), "knapsack_NoOpt", "@main", noArg, noOpt, nPath(1666))) @@ -101,4 +74,3 @@ class TestImpCPSNoOpt extends Optimization { testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/nqueen.ll"), "nqueen_NoOpt", "@main", noArg, noOpt, nPath(1363))) testGS(N, gs, TestPrg(parseFile("benchmarks/opt-experiments/quicksort.ll"), "quicksort_NoOpt", "@main", noArg, noOpt, nPath(5040))) } -*/ diff --git a/src/test/scala/gensym/TestGS.scala b/src/test/scala/gensym/TestGS.scala index 2df2dc7f..740399c8 100644 --- a/src/test/scala/gensym/TestGS.scala +++ b/src/test/scala/gensym/TestGS.scala @@ -209,6 +209,8 @@ class Playground extends TestGS { val gs = new ImpCPSGS val rtOpt = "--thread=1 --solver=z3" - val cases = TestCases.symbolicLarge + val cases = TestCases.coreutils.map { t => + t.copy(runOpt = t.runOpt ++ Seq("--solver=z3")) + } testGS(gs, cases) }