Skip to content

clean up runtime #107

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Kraks merged 3 commits into from
Aug 15, 2026
Merged

clean up runtime #107

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8a3be80
clean up runtime
Kraks Aug 15, 2026
e13327e
further clean up
Kraks Aug 15, 2026
98ea727
fix
Kraks Aug 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 0 additions & 12 deletions headers/gensym.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,25 +45,13 @@
#include <gensym/args.hpp>
#include <gensym/cli.hpp>

#ifdef PURE_STATE
#include <gensym/state_pure.hpp>
#endif
#ifdef IMPURE_STATE
#include <gensym/state_tsnt.hpp>
#endif

#include <gensym/smt_checker.hpp>
#include <gensym/branch.hpp>
#include <gensym/misc.hpp>

#ifdef PURE_STATE
#include <gensym/external_pure.hpp>
#endif

#ifdef IMPURE_STATE
#include <gensym/external_imp.hpp>
#endif

#include <gensym/external.hpp>

#endif
171 changes: 0 additions & 171 deletions headers/gensym/branch.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<std::monostate()>& f) {
if (can_par_tp()) {
tp.add_task(ssid, f);
return std::monostate{};
}
return f();
}

inline immer::flex_vector<std::pair<SS, PtrVal>>
sym_exec_br(SS ss, unsigned int block_id, PtrVal t_cond, PtrVal f_cond,
immer::flex_vector<std::pair<SS, PtrVal>> (*tf)(SS),
immer::flex_vector<std::pair<SS, PtrVal>> (*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<immer::flex_vector<std::pair<SS, PtrVal>>> tf_res =
create_async<immer::flex_vector<std::pair<SS, PtrVal>>>([&]{
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<std::monostate(SS, std::function<std::monostate(SS, PtrVal)>)> tf,
std::function<std::monostate(SS, std::function<std::monostate(SS, PtrVal)>)> ff,
std::function<std::monostate(SS, PtrVal)> 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<std::pair<SS, PtrVal>>
array_lookup(SS ss, PtrVal base, PtrVal offset, size_t esize) {
immer::flex_vector_transient<std::pair<SS, PtrVal>> result;
auto baseloc = std::dynamic_pointer_cast<LocV>(base);

if (auto offint = std::dynamic_pointer_cast<IntV>(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<SymV>(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<std::monostate(SS, PtrVal)> k) {
auto baseloc = std::dynamic_pointer_cast<LocV>(base);

if (auto offint = std::dynamic_pointer_cast<IntV>(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<SymV>(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<std::monostate(SS&, PtrVal)>),
SS ss, std::function<std::monostate(SS&, PtrVal)> k) {
Expand Down Expand Up @@ -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
Loading
Loading