From 1d7b6deeeed8b6d40ef6750106a67c716e7c6c1c Mon Sep 17 00:00:00 2001 From: John Regehr Date: Tue, 22 Sep 2026 16:30:24 -0600 Subject: [PATCH 1/3] work --- ir/type.cpp | 7 ++-- ir/type.h | 2 + llvm_util/cmd_args_def.h | 7 ++++ llvm_util/cmd_args_list.h | 6 +++ llvm_util/llvm2alive.cpp | 38 ++++++++++++++++--- llvm_util/utils.cpp | 19 +++++++--- .../vector/scalable/byval-call.srctgt.ll | 15 ++++++++ .../vector/scalable/gep-stride-fail.srctgt.ll | 14 +++++++ .../vector/scalable/gep-stride.srctgt.ll | 12 ++++++ .../scalable/large-vector-cap.srctgt.ll | 11 ++++++ .../vector/scalable/large-vector.srctgt.ll | 14 +++++++ .../scalable/shufflevector-splat.srctgt.ll | 12 ++++++ .../splat-insertelement-fail.srctgt.ll | 14 +++++++ .../scalable/splat-insertelement.srctgt.ll | 14 +++++++ .../vscale-intrinsic-narrow.srctgt.ll | 13 +++++++ .../scalable/vscale-intrinsic.srctgt.ll | 13 +++++++ tests/unit/vector/scalablevector2.opt | 2 +- tests/unit/vector/scalablevector3.opt | 2 +- tools/alive.cpp | 14 +++++-- tools/alive_parser.cpp | 13 +++++++ 20 files changed, 224 insertions(+), 18 deletions(-) create mode 100644 tests/alive-tv/vector/scalable/byval-call.srctgt.ll create mode 100644 tests/alive-tv/vector/scalable/gep-stride-fail.srctgt.ll create mode 100644 tests/alive-tv/vector/scalable/gep-stride.srctgt.ll create mode 100644 tests/alive-tv/vector/scalable/large-vector-cap.srctgt.ll create mode 100644 tests/alive-tv/vector/scalable/large-vector.srctgt.ll create mode 100644 tests/alive-tv/vector/scalable/shufflevector-splat.srctgt.ll create mode 100644 tests/alive-tv/vector/scalable/splat-insertelement-fail.srctgt.ll create mode 100644 tests/alive-tv/vector/scalable/splat-insertelement.srctgt.ll create mode 100644 tests/alive-tv/vector/scalable/vscale-intrinsic-narrow.srctgt.ll create mode 100644 tests/alive-tv/vector/scalable/vscale-intrinsic.srctgt.ll diff --git a/ir/type.cpp b/ir/type.cpp index 66ee2588e..f6d7841ee 100644 --- a/ir/type.cpp +++ b/ir/type.cpp @@ -20,7 +20,8 @@ using namespace std; static constexpr unsigned var_type_bits = 3; static constexpr unsigned var_bw_bits = 11; -static constexpr unsigned var_vector_elements = 16; +static constexpr unsigned var_elements_bits = 16; +static_assert(IR::max_vector_elements == (1u << var_elements_bits) - 1); namespace IR { @@ -808,8 +809,8 @@ AggregateType::AggregateType(string &&name, vector &&vchildren, } expr AggregateType::numElements() const { - return defined ? expr::mkUInt(elements, var_vector_elements) : - var("elements", var_vector_elements); + return defined ? expr::mkUInt(elements, var_elements_bits) : + var("elements", var_elements_bits); } unsigned AggregateType::numPaddingsConst() const { diff --git a/ir/type.h b/ir/type.h index 009ee5811..46eb9994f 100644 --- a/ir/type.h +++ b/ir/type.h @@ -18,6 +18,8 @@ namespace smt { class Model; } namespace IR { +static constexpr unsigned max_vector_elements = 65535; + class AggregateType; class FloatType; class IntType; diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h index fd4443bc6..bb1dc8539 100644 --- a/llvm_util/cmd_args_def.h +++ b/llvm_util/cmd_args_def.h @@ -24,6 +24,13 @@ config::debug = opt_debug; config::quiet = opt_quiet; config::max_offset_bits = opt_max_offset_in_bits; config::max_sizet_bits = opt_max_sizet_in_bits; +if (opt_single_vscale == 0 || + (opt_single_vscale & (opt_single_vscale - 1)) != 0) { + cerr << "Alive2: " LLVM_ARGS_PREFIX + "single-vscale must be a positive power of two!" << endl; + exit(1); +} +config::vscale_value = opt_single_vscale; if ((config::disallow_ub_exploitation = opt_disallow_ub_exploitation)) { config::disable_undef_input = true; diff --git a/llvm_util/cmd_args_list.h b/llvm_util/cmd_args_list.h index 49fbd01a5..efa5ccb16 100644 --- a/llvm_util/cmd_args_list.h +++ b/llvm_util/cmd_args_list.h @@ -185,4 +185,10 @@ llvm::cl::opt opt_disallow_ub_exploitation( llvm::cl::desc("Disallow UB exploitation by optimizations (default=allow)"), llvm::cl::init(false), llvm::cl::cat(alive_cmdargs)); +llvm::cl::opt opt_single_vscale(LLVM_ARGS_PREFIX "single-vscale", + llvm::cl::desc("Check scalable vectors at this one concrete vscale, " + "which must be a power of two (default=2)"), + llvm::cl::init(2), llvm::cl::value_desc("value"), + llvm::cl::cat(alive_cmdargs)); + } diff --git a/llvm_util/llvm2alive.cpp b/llvm_util/llvm2alive.cpp index c79ddf3c1..3a55828df 100644 --- a/llvm_util/llvm2alive.cpp +++ b/llvm_util/llvm2alive.cpp @@ -5,6 +5,7 @@ #include "ir/x86_intrinsics.h" #include "llvm_util/known_fns.h" #include "llvm_util/utils.h" +#include "util/config.h" #include "util/sort.h" #include "llvm/ADT/SmallVector.h" #include "llvm/Analysis/MemoryBuiltins.h" @@ -640,7 +641,9 @@ class llvm2alive_ : public llvm::InstVisitor> { auto ofs_ty = llvm::IntegerType::get(i.getContext(), 64); if (auto opvty = dyn_cast(opty)) { - assert(!isa(opvty)); + // TODO: scalable splat struct indices + if (isa(opvty)) + return error(i); vector offsets; for (unsigned i = 0; i < opvty->getElementCount().getKnownMinValue(); @@ -668,7 +671,11 @@ class llvm2alive_ : public llvm::InstVisitor> { continue; } - gep->addIdx(I.getSequentialElementStride(DL()).getKnownMinValue(), *op); + auto stride = I.getSequentialElementStride(DL()); + auto size = stride.getKnownMinValue(); + if (stride.isScalable()) + size *= uint64_t(config::vscale_value); + gep->addIdx(size, *op); } return gep; } @@ -1235,6 +1242,21 @@ class llvm2alive_ : public llvm::InstVisitor> { addNoundefAssumes(i, {a, b}); return make_unique(*a, *b); } + case llvm::Intrinsic::vscale: { + auto ty = llvm_type2alive(i.getType()); + if (!ty) + return error(i); + llvm::Constant *constant; + if (ty->bits() < 32 && (config::vscale_value >> ty->bits()) != 0) + constant = llvm::PoisonValue::get(i.getType()); + else + constant = llvm::ConstantInt::get(i.getType(), config::vscale_value); + auto val = get_operand(constant); + if (!val) + return error(i); + ret = make_unique(*ty, value_name(i), *val, UnaryOp::Copy); + break; + } // do nothing intrinsics case llvm::Intrinsic::dbg_declare: @@ -1346,8 +1368,11 @@ class llvm2alive_ : public llvm::InstVisitor> { RetTy visitShuffleVectorInst(llvm::ShuffleVectorInst &i) { PARSE_BINOP(); vector mask; - for (auto m : i.getShuffleMask()) - mask.push_back(m); + + unsigned replicate = i.getType()->isScalableTy() ? config::vscale_value : 1; + auto sm = i.getShuffleMask(); + for (unsigned j = 0; j < replicate; ++j) + mask.insert(mask.end(), sm.begin(), sm.end()); return make_unique(*ty, value_name(i), *a, *b, std::move(mask)); } @@ -1599,7 +1624,10 @@ class llvm2alive_ : public llvm::InstVisitor> { attrs.set(ParamAttrs::ByVal); auto ty = aset.getByValType(); auto asz = DL().getTypeAllocSize(ty); - attrs.blockSize = max(attrs.blockSize, asz.getKnownMinValue()); + auto size = asz.getKnownMinValue(); + if (asz.isScalable()) + size *= uint64_t(config::vscale_value); + attrs.blockSize = max(attrs.blockSize, size); attrs.set(ParamAttrs::Align); attrs.align = max(attrs.align, DL().getABITypeAlign(ty).value()); diff --git a/llvm_util/utils.cpp b/llvm_util/utils.cpp index 502d388fe..5fd00268a 100644 --- a/llvm_util/utils.cpp +++ b/llvm_util/utils.cpp @@ -4,6 +4,8 @@ #include "llvm_util/utils.h" #include "ir/constant.h" #include "ir/function.h" +#include "ir/type.h" +#include "util/config.h" #include "llvm/ADT/StringExtras.h" #include "llvm/IR/Constants.h" #include "llvm/IR/DataLayout.h" @@ -207,8 +209,8 @@ Type* llvm_type2alive(const llvm::Type *ty) { } return cache.get(); } - // TODO: non-fixed sized vectors - case llvm::Type::FixedVectorTyID: { + case llvm::Type::FixedVectorTyID: + case llvm::Type::ScalableVectorTyID: { auto &cache = type_cache[ty]; if (!cache) { auto vty = cast(ty); @@ -216,8 +218,15 @@ Type* llvm_type2alive(const llvm::Type *ty) { auto ety = llvm_type2alive(vty->getElementType()); if (!ety || elems > 1024) return nullptr; + uint64_t count = elems; + if (vty->isScalableTy()) + count *= util::config::vscale_value; + if (!count || count > max_vector_elements) { + *out << "ERROR: Vector type is too large\n"; + return nullptr; + } cache = make_unique("ty_" + to_string(type_id_counter++), - elems, *ety); + elems, *ety, vty->isScalableTy()); } return cache.get(); } @@ -303,7 +312,7 @@ Value* get_operand(llvm::Value *v, return nullptr; // automatic splat of constant values - if (auto vty = dyn_cast(v->getType()); + if (auto vty = dyn_cast(v->getType()); vty && isa(v)) { llvm::Value *llvm_splat = nullptr; if (auto cnst = dyn_cast(v)) { @@ -320,7 +329,7 @@ Value* get_operand(llvm::Value *v, if (!splat) return nullptr; - vector vals(vty->getNumElements(), splat); + vector vals(ty->getAsAggregateType()->numElementsConst(), splat); auto val = make_unique(*ty, std::move(vals)); auto ret = val.get(); current_fn->addConstant(std::move(val)); diff --git a/tests/alive-tv/vector/scalable/byval-call.srctgt.ll b/tests/alive-tv/vector/scalable/byval-call.srctgt.ll new file mode 100644 index 000000000..374f005eb --- /dev/null +++ b/tests/alive-tv/vector/scalable/byval-call.srctgt.ll @@ -0,0 +1,15 @@ +; TEST-ARGS: --single-vscale=2 +; CHECK: Transformation seems to be correct! +; CHECK-NOT: ERROR: + +declare void @consume(ptr) + +define void @src(ptr %p) { + call void @consume(ptr byval() %p) + ret void +} + +define void @tgt(ptr %p) { + call void @consume(ptr byval([32 x i8]) align 16 %p) + ret void +} diff --git a/tests/alive-tv/vector/scalable/gep-stride-fail.srctgt.ll b/tests/alive-tv/vector/scalable/gep-stride-fail.srctgt.ll new file mode 100644 index 000000000..e5ad9d98a --- /dev/null +++ b/tests/alive-tv/vector/scalable/gep-stride-fail.srctgt.ll @@ -0,0 +1,14 @@ +; TEST-ARGS: --single-vscale=2 +; ERROR: Target is more poisonous than source + +define @src(ptr align 4 dereferenceable(32) %p) { + %q = getelementptr , ptr %p, i64 1 + %r = load , ptr %q, align 4 + ret %r +} + +define @tgt(ptr align 4 dereferenceable(32) %p) { + %q = getelementptr i8, ptr %p, i64 8 + %r = load , ptr %q, align 4 + ret %r +} diff --git a/tests/alive-tv/vector/scalable/gep-stride.srctgt.ll b/tests/alive-tv/vector/scalable/gep-stride.srctgt.ll new file mode 100644 index 000000000..db5ab9067 --- /dev/null +++ b/tests/alive-tv/vector/scalable/gep-stride.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --single-vscale=2 +; CHECK: Transformation seems to be correct! + +define ptr @src(ptr %p) { + %q = getelementptr , ptr %p, i64 1, i64 1 + ret ptr %q +} + +define ptr @tgt(ptr %p) { + %q = getelementptr i8, ptr %p, i64 20 + ret ptr %q +} diff --git a/tests/alive-tv/vector/scalable/large-vector-cap.srctgt.ll b/tests/alive-tv/vector/scalable/large-vector-cap.srctgt.ll new file mode 100644 index 000000000..36b0251dd --- /dev/null +++ b/tests/alive-tv/vector/scalable/large-vector-cap.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --single-vscale=2048 +; SKIP-IDENTITY +; ERROR: Vector type is too large + +define @src( %v) { + ret %v +} + +define @tgt( %v) { + ret %v +} diff --git a/tests/alive-tv/vector/scalable/large-vector.srctgt.ll b/tests/alive-tv/vector/scalable/large-vector.srctgt.ll new file mode 100644 index 000000000..c4a6f1971 --- /dev/null +++ b/tests/alive-tv/vector/scalable/large-vector.srctgt.ll @@ -0,0 +1,14 @@ +; TEST-ARGS: --quiet --disable-undef-input --single-vscale=1024 +; CHECK: Transformation seems to be correct! +; CHECK-NOT: ERROR: + +; 32 minimum lanes at vscale 1024 is 32768 realized lanes, inside the limit on +; an aggregate's element count. +define i1 @src() { + ret i1 false +} + +define i1 @tgt() { + %r = extractelement zeroinitializer, i32 32767 + ret i1 %r +} diff --git a/tests/alive-tv/vector/scalable/shufflevector-splat.srctgt.ll b/tests/alive-tv/vector/scalable/shufflevector-splat.srctgt.ll new file mode 100644 index 000000000..d310ff079 --- /dev/null +++ b/tests/alive-tv/vector/scalable/shufflevector-splat.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --single-vscale=4 +; CHECK: Transformation seems to be correct! + +define @src( %vec) { + %insert = insertelement %vec, i32 0, i32 0 + %shuf = shufflevector %insert, poison, zeroinitializer + ret %shuf +} + +define @tgt( %vec) { + ret zeroinitializer +} diff --git a/tests/alive-tv/vector/scalable/splat-insertelement-fail.srctgt.ll b/tests/alive-tv/vector/scalable/splat-insertelement-fail.srctgt.ll new file mode 100644 index 000000000..ff930fac7 --- /dev/null +++ b/tests/alive-tv/vector/scalable/splat-insertelement-fail.srctgt.ll @@ -0,0 +1,14 @@ +; TEST-ARGS: --single-vscale=4 +; ERROR: Value mismatch + +define @src( %vec) { + %vec1 = insertelement %vec, i32 0, i32 0 + %vec2 = insertelement %vec1, i32 0, i32 1 + %vec3 = insertelement %vec2, i32 0, i32 2 + %result = insertelement %vec3, i32 0, i32 3 + ret %result +} + +define @tgt( %vec) { + ret zeroinitializer +} diff --git a/tests/alive-tv/vector/scalable/splat-insertelement.srctgt.ll b/tests/alive-tv/vector/scalable/splat-insertelement.srctgt.ll new file mode 100644 index 000000000..33b98b4c4 --- /dev/null +++ b/tests/alive-tv/vector/scalable/splat-insertelement.srctgt.ll @@ -0,0 +1,14 @@ +; TEST-ARGS: --single-vscale=2 +; CHECK: Transformation seems to be correct! + +define @src( %vec) { + %vec1 = insertelement %vec, i32 0, i32 0 + %vec2 = insertelement %vec1, i32 0, i32 1 + %vec3 = insertelement %vec2, i32 0, i32 2 + %result = insertelement %vec3, i32 0, i32 3 + ret %result +} + +define @tgt( %vec) { + ret zeroinitializer +} diff --git a/tests/alive-tv/vector/scalable/vscale-intrinsic-narrow.srctgt.ll b/tests/alive-tv/vector/scalable/vscale-intrinsic-narrow.srctgt.ll new file mode 100644 index 000000000..41ffc9228 --- /dev/null +++ b/tests/alive-tv/vector/scalable/vscale-intrinsic-narrow.srctgt.ll @@ -0,0 +1,13 @@ +; TEST-ARGS: --single-vscale=2 +; ERROR: Target is more poisonous than source + +declare i1 @llvm.vscale.i1() + +define i1 @src() { + ret i1 true +} + +define i1 @tgt() { + %v = call i1 @llvm.vscale.i1() + ret i1 %v +} diff --git a/tests/alive-tv/vector/scalable/vscale-intrinsic.srctgt.ll b/tests/alive-tv/vector/scalable/vscale-intrinsic.srctgt.ll new file mode 100644 index 000000000..d7aa4cbd0 --- /dev/null +++ b/tests/alive-tv/vector/scalable/vscale-intrinsic.srctgt.ll @@ -0,0 +1,13 @@ +; TEST-ARGS: --single-vscale=4 +; CHECK: Transformation seems to be correct! + +declare i64 @llvm.vscale.i64() + +define i64 @src() { + %v = call i64 @llvm.vscale.i64() + ret i64 %v +} + +define i64 @tgt() { + ret i64 4 +} diff --git a/tests/unit/vector/scalablevector2.opt b/tests/unit/vector/scalablevector2.opt index a9e76241b..6941b4a28 100644 --- a/tests/unit/vector/scalablevector2.opt +++ b/tests/unit/vector/scalablevector2.opt @@ -1,4 +1,4 @@ -; TEST-ARGS: -vscale:2 +; TEST-ARGS: -single-vscale:2 ; CHECK: ; CHECK: Transformation seems to be correct! diff --git a/tests/unit/vector/scalablevector3.opt b/tests/unit/vector/scalablevector3.opt index e4c49c840..0e862bd11 100644 --- a/tests/unit/vector/scalablevector3.opt +++ b/tests/unit/vector/scalablevector3.opt @@ -1,4 +1,4 @@ -; TEST-ARGS: -vscale:1 +; TEST-ARGS: -single-vscale:1 ; CHECK: ; ERROR: Target is more poisonous than source for i4 %r diff --git a/tools/alive.cpp b/tools/alive.cpp index 6d9a71dd1..4e3c20188 100644 --- a/tools/alive.cpp +++ b/tools/alive.cpp @@ -36,7 +36,8 @@ static void show_help() { " -skip-smt\t\tSkip all SMT queries\n" " -disable-poison-input\tAssume input variables can never be poison\n" " -disable-undef-input\tAssume input variables can never be undef\n" - " -vscale:x\t\tSet vscale value for scalable vectors (default: 1)\n" + " -single-vscale:x\tCheck scalable vectors at this one concrete vscale,\n" + "\t\t\ta power of two (default: 2)\n" " -h / --help / -v / --version\tShow this help\n"; } @@ -77,8 +78,15 @@ int main(int argc, char **argv) { config::disable_undef_input = true; else if (arg == "-disable-poison-input") config::disable_poison_input = true; - else if (arg.compare(0, 8, "-vscale:") == 0 && arg.size() > 8) - config::vscale_value = strtoul(arg.substr(8).data(), nullptr, 10); + else if (arg.compare(0, 15, "-single-vscale:") == 0 && arg.size() > 15) { + config::vscale_value = strtoul(arg.substr(15).data(), nullptr, 10); + if (config::vscale_value == 0 || + (config::vscale_value & (config::vscale_value - 1)) != 0) { + cerr << "single-vscale must be a positive power of two!\n\n"; + show_help(); + return -1; + } + } else if (arg == "-h" || arg == "--help" || arg == "-v" || arg == "--version") { show_help(); diff --git a/tools/alive_parser.cpp b/tools/alive_parser.cpp index 0427504e4..45a379d96 100644 --- a/tools/alive_parser.cpp +++ b/tools/alive_parser.cpp @@ -4,9 +4,11 @@ #include "tools/alive_parser.h" #include "ir/constant.h" #include "ir/precondition.h" +#include "ir/type.h" #include "ir/value.h" #include "tools/alive_lexer.h" #include "util/compiler.h" +#include "util/config.h" #include #include #include @@ -377,6 +379,17 @@ static Type& parse_vector_type() { unsigned elements = yylval.num; Type &elemTy = parse_scalar_type(); tokenizer.ensure(CSGT); + + // A scalable vector is realized at the configured vscale, so its element + // count can exceed what the SMT encoding holds even when the minimum can't. + uint64_t count = elements; + if (scalable) + count *= util::config::vscale_value; + if (count == 0 || count > max_vector_elements) + error("Vector type must have between 1 and " + + to_string(max_vector_elements) + " elements; got: " + + to_string(count)); + return *vector_types.emplace_back( make_unique("vty_" + to_string(vector_types.size()), elements, elemTy, scalable)).get(); From e32b1bf02506262f071fd89ee28c6c893a67c73a Mon Sep 17 00:00:00 2001 From: John Regehr Date: Tue, 22 Sep 2026 16:36:27 -0600 Subject: [PATCH 2/3] work --- llvm_util/llvm2alive.cpp | 3 ++- .../vector/scalable/gep-stride-fail.srctgt.ll | 14 -------------- .../vector/scalable/large-vector.srctgt.ll | 14 -------------- .../scalable/splat-insertelement-fail.srctgt.ll | 14 -------------- .../vector/scalable/splat-insertelement.srctgt.ll | 14 -------------- .../scalable/vscale-intrinsic-narrow.srctgt.ll | 13 ------------- tools/alive_parser.cpp | 2 -- 7 files changed, 2 insertions(+), 72 deletions(-) delete mode 100644 tests/alive-tv/vector/scalable/gep-stride-fail.srctgt.ll delete mode 100644 tests/alive-tv/vector/scalable/large-vector.srctgt.ll delete mode 100644 tests/alive-tv/vector/scalable/splat-insertelement-fail.srctgt.ll delete mode 100644 tests/alive-tv/vector/scalable/splat-insertelement.srctgt.ll delete mode 100644 tests/alive-tv/vector/scalable/vscale-intrinsic-narrow.srctgt.ll diff --git a/llvm_util/llvm2alive.cpp b/llvm_util/llvm2alive.cpp index 3a55828df..e7d61a0dc 100644 --- a/llvm_util/llvm2alive.cpp +++ b/llvm_util/llvm2alive.cpp @@ -605,7 +605,8 @@ class llvm2alive_ : public llvm::InstVisitor> { } auto typesz = DL().getTypeAllocSize(i.getAllocatedType()); - if (typesz.isScalable()) // TODO: scalable vectors not supported + // TODO: scalable alloca + if (typesz.isScalable()) return error(i); auto size = make_intconst(typesz, 64); diff --git a/tests/alive-tv/vector/scalable/gep-stride-fail.srctgt.ll b/tests/alive-tv/vector/scalable/gep-stride-fail.srctgt.ll deleted file mode 100644 index e5ad9d98a..000000000 --- a/tests/alive-tv/vector/scalable/gep-stride-fail.srctgt.ll +++ /dev/null @@ -1,14 +0,0 @@ -; TEST-ARGS: --single-vscale=2 -; ERROR: Target is more poisonous than source - -define @src(ptr align 4 dereferenceable(32) %p) { - %q = getelementptr , ptr %p, i64 1 - %r = load , ptr %q, align 4 - ret %r -} - -define @tgt(ptr align 4 dereferenceable(32) %p) { - %q = getelementptr i8, ptr %p, i64 8 - %r = load , ptr %q, align 4 - ret %r -} diff --git a/tests/alive-tv/vector/scalable/large-vector.srctgt.ll b/tests/alive-tv/vector/scalable/large-vector.srctgt.ll deleted file mode 100644 index c4a6f1971..000000000 --- a/tests/alive-tv/vector/scalable/large-vector.srctgt.ll +++ /dev/null @@ -1,14 +0,0 @@ -; TEST-ARGS: --quiet --disable-undef-input --single-vscale=1024 -; CHECK: Transformation seems to be correct! -; CHECK-NOT: ERROR: - -; 32 minimum lanes at vscale 1024 is 32768 realized lanes, inside the limit on -; an aggregate's element count. -define i1 @src() { - ret i1 false -} - -define i1 @tgt() { - %r = extractelement zeroinitializer, i32 32767 - ret i1 %r -} diff --git a/tests/alive-tv/vector/scalable/splat-insertelement-fail.srctgt.ll b/tests/alive-tv/vector/scalable/splat-insertelement-fail.srctgt.ll deleted file mode 100644 index ff930fac7..000000000 --- a/tests/alive-tv/vector/scalable/splat-insertelement-fail.srctgt.ll +++ /dev/null @@ -1,14 +0,0 @@ -; TEST-ARGS: --single-vscale=4 -; ERROR: Value mismatch - -define @src( %vec) { - %vec1 = insertelement %vec, i32 0, i32 0 - %vec2 = insertelement %vec1, i32 0, i32 1 - %vec3 = insertelement %vec2, i32 0, i32 2 - %result = insertelement %vec3, i32 0, i32 3 - ret %result -} - -define @tgt( %vec) { - ret zeroinitializer -} diff --git a/tests/alive-tv/vector/scalable/splat-insertelement.srctgt.ll b/tests/alive-tv/vector/scalable/splat-insertelement.srctgt.ll deleted file mode 100644 index 33b98b4c4..000000000 --- a/tests/alive-tv/vector/scalable/splat-insertelement.srctgt.ll +++ /dev/null @@ -1,14 +0,0 @@ -; TEST-ARGS: --single-vscale=2 -; CHECK: Transformation seems to be correct! - -define @src( %vec) { - %vec1 = insertelement %vec, i32 0, i32 0 - %vec2 = insertelement %vec1, i32 0, i32 1 - %vec3 = insertelement %vec2, i32 0, i32 2 - %result = insertelement %vec3, i32 0, i32 3 - ret %result -} - -define @tgt( %vec) { - ret zeroinitializer -} diff --git a/tests/alive-tv/vector/scalable/vscale-intrinsic-narrow.srctgt.ll b/tests/alive-tv/vector/scalable/vscale-intrinsic-narrow.srctgt.ll deleted file mode 100644 index 41ffc9228..000000000 --- a/tests/alive-tv/vector/scalable/vscale-intrinsic-narrow.srctgt.ll +++ /dev/null @@ -1,13 +0,0 @@ -; TEST-ARGS: --single-vscale=2 -; ERROR: Target is more poisonous than source - -declare i1 @llvm.vscale.i1() - -define i1 @src() { - ret i1 true -} - -define i1 @tgt() { - %v = call i1 @llvm.vscale.i1() - ret i1 %v -} diff --git a/tools/alive_parser.cpp b/tools/alive_parser.cpp index 45a379d96..dbf55a1ed 100644 --- a/tools/alive_parser.cpp +++ b/tools/alive_parser.cpp @@ -380,8 +380,6 @@ static Type& parse_vector_type() { Type &elemTy = parse_scalar_type(); tokenizer.ensure(CSGT); - // A scalable vector is realized at the configured vscale, so its element - // count can exceed what the SMT encoding holds even when the minimum can't. uint64_t count = elements; if (scalable) count *= util::config::vscale_value; From c38db4bec0ce5aa70224039deda98a676ed8eca0 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 23 Sep 2026 08:39:48 +0100 Subject: [PATCH 3/3] simplify --- llvm_util/cmd_args_def.h | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h index bb1dc8539..5ecbee14b 100644 --- a/llvm_util/cmd_args_def.h +++ b/llvm_util/cmd_args_def.h @@ -1,6 +1,8 @@ // Copyright (c) 2018-present The Alive2 Authors. // Distributed under the MIT license that can be found in the LICENSE file. +#include + #ifdef ARGS_SRC_TGT config::src_unroll_cnt = opt_src_unrolling_factor; config::tgt_unroll_cnt = opt_tgt_unrolling_factor; @@ -24,8 +26,8 @@ config::debug = opt_debug; config::quiet = opt_quiet; config::max_offset_bits = opt_max_offset_in_bits; config::max_sizet_bits = opt_max_sizet_in_bits; -if (opt_single_vscale == 0 || - (opt_single_vscale & (opt_single_vscale - 1)) != 0) { + +if (!std::has_single_bit(opt_single_vscale)) { cerr << "Alive2: " LLVM_ARGS_PREFIX "single-vscale must be a positive power of two!" << endl; exit(1);