From 724602ec0d61409ade052a4605ab004c98e06d95 Mon Sep 17 00:00:00 2001 From: Alborz Jelvani Date: Mon, 13 Apr 2026 16:02:10 -0400 Subject: [PATCH 1/7] added support for individual loop unroll bounds --- ir/function.cpp | 46 ++++++++++++++++++++++++++++++++++++--- ir/function.h | 2 +- llvm_util/cmd_args_def.h | 12 ++++++---- llvm_util/cmd_args_list.h | 20 +++++++++-------- tools/transform.cpp | 4 ++-- util/config.cpp | 5 +++-- util/config.h | 5 +++-- 7 files changed, 71 insertions(+), 23 deletions(-) diff --git a/ir/function.cpp b/ir/function.cpp index fb1c1085d..aaf8598d6 100644 --- a/ir/function.cpp +++ b/ir/function.cpp @@ -11,6 +11,7 @@ #include #include #include +#include using namespace smt; using namespace util; @@ -575,8 +576,8 @@ static auto getPhiPredecessors(const Function &F) { return map; } -void Function::unroll(unsigned k) { - if (k == 0) +void Function::unroll(vector unroll_bounds) { + if (unroll_bounds.size() == 0) return; LoopAnalysis la(*this); @@ -600,6 +601,40 @@ void Function::unroll(unsigned k) { auto users = getUsers(); auto phi_preds = getPhiPredecessors(*this); + vector loop_headers_in_order; + + for (auto *bb : BB_order) { // BB_order maintains the code order + auto it = forest.find(bb); + if (it != forest.end()) { + // bb is a loop header + loop_headers_in_order.emplace_back(bb); + } + } + + // check size of loop unroll bounds is valid + if (loop_headers_in_order.size() != unroll_bounds.size()) { + + // check if unroll_bounds has only one element, if so, use that for all loop + // headers + if (unroll_bounds.size() == 1) { + unsigned bound = unroll_bounds.front(); + unroll_bounds.clear(); + unroll_bounds.resize(loop_headers_in_order.size(), bound); + } else { + std::cerr << "Error: Number of loop headers does not match number of unroll bounds.\n" + << "Number of loop headers: " << loop_headers_in_order.size() << "\n" + << "Number of unroll bounds: " << unroll_bounds.size() << std::endl; + exit(1); + } + } + + // map loop header -> unroll bound + unordered_map unroll_bound_map; + for (size_t i = 0; i < loop_headers_in_order.size(); ++i) { + auto *header = loop_headers_in_order[i]; + unroll_bound_map[header] = unroll_bounds[i]; + } + // traverse each loop tree in post-order while (!worklist.empty()) { auto [header, height, flag] = worklist.back(); @@ -658,7 +693,7 @@ void Function::unroll(unsigned k) { for (unsigned i = 0; i < height; ++i) { name_prefix += "#1"; } - for (unsigned unroll = 2; unroll <= k; ++unroll) { + for (unsigned unroll = 2; unroll <= unroll_bound_map[header]; ++unroll) { string suffix = name_prefix + '#' + to_string(unroll); for (auto *bb : loop_bbs) { auto &copies = bbmap.at(bb); @@ -667,6 +702,11 @@ void Function::unroll(unsigned k) { } } + if (unroll_bounds.size()>1) + { + unroll_bounds.erase(unroll_bounds.begin()); + } + // Clone the header once more so that the last iteration of the loop can // exit. Otherwise the last iteration would be wasted. // Here we assume the header is an exit, as that's the common case. diff --git a/ir/function.h b/ir/function.h index 3f840f866..3eb8a52f8 100644 --- a/ir/function.h +++ b/ir/function.h @@ -224,7 +224,7 @@ class Function final { const std::vector &src_glbs); void topSort(); - void unroll(unsigned k); + void unroll(std::vector unroll_bounds); void print(std::ostream &os, bool print_header = true) const; friend std::ostream &operator<<(std::ostream &os, const Function &f); diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h index fd4443bc6..19321eea8 100644 --- a/llvm_util/cmd_args_def.h +++ b/llvm_util/cmd_args_def.h @@ -2,11 +2,15 @@ // Distributed under the MIT license that can be found in the LICENSE file. #ifdef ARGS_SRC_TGT -config::src_unroll_cnt = opt_src_unrolling_factor; -config::tgt_unroll_cnt = opt_tgt_unrolling_factor; +std::vector unroll_src(opt_src_unrolling_factor.begin(), opt_src_unrolling_factor.end()); +std::vector unroll_tgt(opt_tgt_unrolling_factor.begin(), opt_tgt_unrolling_factor.end()); +config::src_unroll_bounds = unroll_src; +config::tgt_unroll_bounds = unroll_tgt; #else -config::src_unroll_cnt = opt_unrolling_factor; -config::tgt_unroll_cnt = opt_unrolling_factor; +std::vector unroll_src = {opt_unrolling_factor}; +std::vector unroll_tgt = {opt_unrolling_factor}; +config::src_unroll_bounds = unroll_src; +config::tgt_unroll_bounds = unroll_tgt; #endif config::disable_undef_input = opt_disable_undef; config::disable_poison_input = opt_disable_poison; diff --git a/llvm_util/cmd_args_list.h b/llvm_util/cmd_args_list.h index b732ec92a..5a1210228 100644 --- a/llvm_util/cmd_args_list.h +++ b/llvm_util/cmd_args_list.h @@ -19,17 +19,19 @@ llvm::cl::list opt_funcs(LLVM_ARGS_PREFIX "func", set func_names; #ifdef ARGS_SRC_TGT -llvm::cl::opt opt_src_unrolling_factor(LLVM_ARGS_PREFIX "src-unroll", - llvm::cl::desc("Unrolling factor for src function (default=0)"), - llvm::cl::init(0), llvm::cl::cat(alive_cmdargs)); +llvm::cl::list opt_src_unrolling_factor(LLVM_ARGS_PREFIX "src-unroll", + llvm::cl::desc("Unrolling factors for src function (default=0)"), + llvm::cl::CommaSeparated, + llvm::cl::cat(alive_cmdargs)); -llvm::cl::opt opt_tgt_unrolling_factor(LLVM_ARGS_PREFIX "tgt-unroll", - llvm::cl::desc("Unrolling factor for tgt function (default=0)"), - llvm::cl::init(0), llvm::cl::cat(alive_cmdargs)); +llvm::cl::list opt_tgt_unrolling_factor(LLVM_ARGS_PREFIX "tgt-unroll", + llvm::cl::desc("Unrolling factors for tgt function (default=0)"), + llvm::cl::CommaSeparated, + llvm::cl::cat(alive_cmdargs)); #else -llvm::cl::opt opt_unrolling_factor(LLVM_ARGS_PREFIX "unroll", - llvm::cl::desc("Unrolling factor (default=0)"), - llvm::cl::init(0), llvm::cl::cat(alive_cmdargs)); + llvm::cl::opt opt_unrolling_factor(LLVM_ARGS_PREFIX "unroll", + llvm::cl::desc("Unrolling factor (default=0)"), + llvm::cl::cat(alive_cmdargs)); #endif llvm::cl::opt opt_disable_undef(LLVM_ARGS_PREFIX "disable-undef-input", diff --git a/tools/transform.cpp b/tools/transform.cpp index ee5810678..4fbc4592c 100644 --- a/tools/transform.cpp +++ b/tools/transform.cpp @@ -1976,8 +1976,8 @@ void Transform::preprocess() { // bits_program_pointer is used by unroll. Initialize it in advance initBitsProgramPointer(*this); - src.unroll(config::src_unroll_cnt); - tgt.unroll(config::tgt_unroll_cnt); + src.unroll(config::src_unroll_bounds); + tgt.unroll(config::tgt_unroll_bounds); } void Transform::print(ostream &os, const TransformPrintOpts &opt) const { diff --git a/util/config.cpp b/util/config.cpp index 632b72561..c00cfb67b 100644 --- a/util/config.cpp +++ b/util/config.cpp @@ -3,6 +3,7 @@ #include "util/config.h" #include +#include using namespace std; @@ -20,8 +21,8 @@ bool fail_if_src_is_ub = false; bool disallow_ub_exploitation = false; bool debug = false; bool quiet = false; -unsigned src_unroll_cnt = 0; -unsigned tgt_unroll_cnt = 0; +std::vector src_unroll_bounds; +std::vector tgt_unroll_bounds; unsigned max_offset_bits = 64; unsigned max_sizet_bits = 64; diff --git a/util/config.h b/util/config.h index 6cf2314ff..6fbed3509 100644 --- a/util/config.h +++ b/util/config.h @@ -5,6 +5,7 @@ #include #include +#include namespace util::config { @@ -33,9 +34,9 @@ extern bool debug; extern bool quiet; -extern unsigned src_unroll_cnt; +extern std::vector src_unroll_bounds; -extern unsigned tgt_unroll_cnt; +extern std::vector tgt_unroll_bounds; // The maximum number of bits to use for offset computations. Note that this may // impact correctness, if values involved in offset computations exceed the From 458beff325809d567978a96cf9996e983a636750 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 27 Apr 2026 09:36:35 +0100 Subject: [PATCH 2/7] Update cmd_args_list.h --- llvm_util/cmd_args_list.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/llvm_util/cmd_args_list.h b/llvm_util/cmd_args_list.h index 5a1210228..aae6fef13 100644 --- a/llvm_util/cmd_args_list.h +++ b/llvm_util/cmd_args_list.h @@ -29,8 +29,8 @@ llvm::cl::list opt_tgt_unrolling_factor(LLVM_ARGS_PREFIX "tgt-unroll", llvm::cl::CommaSeparated, llvm::cl::cat(alive_cmdargs)); #else - llvm::cl::opt opt_unrolling_factor(LLVM_ARGS_PREFIX "unroll", - llvm::cl::desc("Unrolling factor (default=0)"), +llvm::cl::opt opt_unrolling_factor(LLVM_ARGS_PREFIX "unroll", + llvm::cl::desc("Unrolling factor (default=0)"), llvm::cl::cat(alive_cmdargs)); #endif From 54b01710b3dddd0a30ad7b2e2c64bfb308056864 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 27 Apr 2026 09:37:07 +0100 Subject: [PATCH 3/7] . --- util/config.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/util/config.h b/util/config.h index 6fbed3509..8683cb12a 100644 --- a/util/config.h +++ b/util/config.h @@ -3,8 +3,8 @@ // Copyright (c) 2018-present The Alive2 Authors. // Distributed under the MIT license that can be found in the LICENSE file. -#include #include +#include #include namespace util::config { From 95113f5ab66827c508aa741020b8b6c9bd4631ee Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 27 Apr 2026 09:37:33 +0100 Subject: [PATCH 4/7] edit --- ir/function.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ir/function.cpp b/ir/function.cpp index aaf8598d6..6da182ab4 100644 --- a/ir/function.cpp +++ b/ir/function.cpp @@ -9,9 +9,9 @@ #include "util/unionfind.h" #include #include +#include #include #include -#include using namespace smt; using namespace util; From a103683000cbd10f57670ff32a7e44ecf6b87d30 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 27 Apr 2026 09:39:21 +0100 Subject: [PATCH 5/7] Initialize unrolling factor to 0 in cmd_args_list --- llvm_util/cmd_args_list.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/llvm_util/cmd_args_list.h b/llvm_util/cmd_args_list.h index aae6fef13..bf4b8e0c9 100644 --- a/llvm_util/cmd_args_list.h +++ b/llvm_util/cmd_args_list.h @@ -31,7 +31,7 @@ llvm::cl::list opt_tgt_unrolling_factor(LLVM_ARGS_PREFIX "tgt-unroll", #else llvm::cl::opt opt_unrolling_factor(LLVM_ARGS_PREFIX "unroll", llvm::cl::desc("Unrolling factor (default=0)"), - llvm::cl::cat(alive_cmdargs)); + llvm::cl::init(0), llvm::cl::cat(alive_cmdargs)); #endif llvm::cl::opt opt_disable_undef(LLVM_ARGS_PREFIX "disable-undef-input", From 41aec85b74717622ae477c574ed8bd80252c7678 Mon Sep 17 00:00:00 2001 From: alborz <50643329+jelvani@users.noreply.github.com> Date: Tue, 28 Apr 2026 17:36:51 -0400 Subject: [PATCH 6/7] Fix formatting of if statement in function.cpp --- ir/function.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/ir/function.cpp b/ir/function.cpp index 6da182ab4..d3e5e6257 100644 --- a/ir/function.cpp +++ b/ir/function.cpp @@ -702,8 +702,7 @@ void Function::unroll(vector unroll_bounds) { } } - if (unroll_bounds.size()>1) - { + if (unroll_bounds.size() > 1) { unroll_bounds.erase(unroll_bounds.begin()); } From dbba62e752ba12d0e0e7a1dd2991c90c4a762364 Mon Sep 17 00:00:00 2001 From: alborz <50643329+jelvani@users.noreply.github.com> Date: Tue, 28 Apr 2026 18:01:16 -0400 Subject: [PATCH 7/7] removed temps and copies --- llvm_util/cmd_args_def.h | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h index 19321eea8..7d09d6d0d 100644 --- a/llvm_util/cmd_args_def.h +++ b/llvm_util/cmd_args_def.h @@ -2,15 +2,11 @@ // Distributed under the MIT license that can be found in the LICENSE file. #ifdef ARGS_SRC_TGT -std::vector unroll_src(opt_src_unrolling_factor.begin(), opt_src_unrolling_factor.end()); -std::vector unroll_tgt(opt_tgt_unrolling_factor.begin(), opt_tgt_unrolling_factor.end()); -config::src_unroll_bounds = unroll_src; -config::tgt_unroll_bounds = unroll_tgt; +config::src_unroll_bounds = std::vector(opt_src_unrolling_factor.begin(), opt_src_unrolling_factor.end()); +config::tgt_unroll_bounds = std::vector(opt_tgt_unrolling_factor.begin(), opt_tgt_unrolling_factor.end()); #else -std::vector unroll_src = {opt_unrolling_factor}; -std::vector unroll_tgt = {opt_unrolling_factor}; -config::src_unroll_bounds = unroll_src; -config::tgt_unroll_bounds = unroll_tgt; +config::src_unroll_bounds = std::vector({opt_unrolling_factor}); +config::tgt_unroll_bounds = std::vector({opt_unrolling_factor}); #endif config::disable_undef_input = opt_disable_undef; config::disable_poison_input = opt_disable_poison;