Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
7 changes: 4 additions & 3 deletions ir/type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -808,8 +809,8 @@ AggregateType::AggregateType(string &&name, vector<Type*> &&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 {
Expand Down
2 changes: 2 additions & 0 deletions ir/type.h
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ namespace smt { class Model; }

namespace IR {

static constexpr unsigned max_vector_elements = 65535;

class AggregateType;
class FloatType;
class IntType;
Expand Down
9 changes: 9 additions & 0 deletions llvm_util/cmd_args_def.h
Original file line number Diff line number Diff line change
@@ -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 <bit>

#ifdef ARGS_SRC_TGT
config::src_unroll_cnt = opt_src_unrolling_factor;
config::tgt_unroll_cnt = opt_tgt_unrolling_factor;
Expand All @@ -25,6 +27,13 @@ config::quiet = opt_quiet;
config::max_offset_bits = opt_max_offset_in_bits;
config::max_sizet_bits = opt_max_sizet_in_bits;

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);
}
config::vscale_value = opt_single_vscale;

if ((config::disallow_ub_exploitation = opt_disallow_ub_exploitation)) {
config::disable_undef_input = true;
config::disable_poison_input = true;
Expand Down
6 changes: 6 additions & 0 deletions llvm_util/cmd_args_list.h
Original file line number Diff line number Diff line change
Expand Up @@ -185,4 +185,10 @@ llvm::cl::opt<bool> 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<unsigned> 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));

}
41 changes: 35 additions & 6 deletions llvm_util/llvm2alive.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -604,7 +605,8 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
}

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);
Expand Down Expand Up @@ -640,7 +642,9 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
auto ofs_ty = llvm::IntegerType::get(i.getContext(), 64);

if (auto opvty = dyn_cast<llvm::VectorType>(opty)) {
assert(!isa<llvm::ScalableVectorType>(opvty));
// TODO: scalable splat struct indices
if (isa<llvm::ScalableVectorType>(opvty))
return error(i);
vector<llvm::Constant *> offsets;

for (unsigned i = 0; i < opvty->getElementCount().getKnownMinValue();
Expand Down Expand Up @@ -668,7 +672,11 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
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;
}
Expand Down Expand Up @@ -1235,6 +1243,21 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
addNoundefAssumes(i, {a, b});
return make_unique<VaCopy>(*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<UnaryOp>(*ty, value_name(i), *val, UnaryOp::Copy);
break;
}

// do nothing intrinsics
case llvm::Intrinsic::dbg_declare:
Expand Down Expand Up @@ -1346,8 +1369,11 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
RetTy visitShuffleVectorInst(llvm::ShuffleVectorInst &i) {
PARSE_BINOP();
vector<unsigned> 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<ShuffleVector>(*ty, value_name(i), *a, *b, std::move(mask));
}
Expand Down Expand Up @@ -1599,7 +1625,10 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
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());
Expand Down
19 changes: 14 additions & 5 deletions llvm_util/utils.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -207,17 +209,24 @@ 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<llvm::VectorType>(ty);
auto elems = vty->getElementCount().getKnownMinValue();
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<VectorType>("ty_" + to_string(type_id_counter++),
elems, *ety);
elems, *ety, vty->isScalableTy());
}
return cache.get();
}
Expand Down Expand Up @@ -303,7 +312,7 @@ Value* get_operand(llvm::Value *v,
return nullptr;

// automatic splat of constant values
if (auto vty = dyn_cast<llvm::FixedVectorType>(v->getType());
if (auto vty = dyn_cast<llvm::VectorType>(v->getType());
vty && isa<llvm::ConstantInt, llvm::ConstantFP>(v)) {
llvm::Value *llvm_splat = nullptr;
if (auto cnst = dyn_cast<llvm::ConstantInt>(v)) {
Expand All @@ -320,7 +329,7 @@ Value* get_operand(llvm::Value *v,
if (!splat)
return nullptr;

vector<Value*> vals(vty->getNumElements(), splat);
vector<Value*> vals(ty->getAsAggregateType()->numElementsConst(), splat);
auto val = make_unique<AggregateValue>(*ty, std::move(vals));
auto ret = val.get();
current_fn->addConstant(std::move(val));
Expand Down
15 changes: 15 additions & 0 deletions tests/alive-tv/vector/scalable/byval-call.srctgt.ll
Original file line number Diff line number Diff line change
@@ -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(<vscale x 4 x i32>) %p)
ret void
}

define void @tgt(ptr %p) {
call void @consume(ptr byval([32 x i8]) align 16 %p)
ret void
}
12 changes: 12 additions & 0 deletions tests/alive-tv/vector/scalable/gep-stride.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
; TEST-ARGS: --single-vscale=2
; CHECK: Transformation seems to be correct!

define ptr @src(ptr %p) {
%q = getelementptr <vscale x 2 x i32>, ptr %p, i64 1, i64 1
ret ptr %q
}

define ptr @tgt(ptr %p) {
%q = getelementptr i8, ptr %p, i64 20
ret ptr %q
}
11 changes: 11 additions & 0 deletions tests/alive-tv/vector/scalable/large-vector-cap.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
; TEST-ARGS: --single-vscale=2048
; SKIP-IDENTITY
; ERROR: Vector type is too large

define <vscale x 64 x i1> @src(<vscale x 64 x i1> %v) {
ret <vscale x 64 x i1> %v
}

define <vscale x 64 x i1> @tgt(<vscale x 64 x i1> %v) {
ret <vscale x 64 x i1> %v
}
12 changes: 12 additions & 0 deletions tests/alive-tv/vector/scalable/shufflevector-splat.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
; TEST-ARGS: --single-vscale=4
; CHECK: Transformation seems to be correct!

define <vscale x 2 x i32> @src(<vscale x 2 x i32> %vec) {
%insert = insertelement <vscale x 2 x i32> %vec, i32 0, i32 0
%shuf = shufflevector <vscale x 2 x i32> %insert, <vscale x 2 x i32> poison, <vscale x 2 x i32> zeroinitializer
ret <vscale x 2 x i32> %shuf
}

define <vscale x 2 x i32> @tgt(<vscale x 2 x i32> %vec) {
ret <vscale x 2 x i32> zeroinitializer
}
13 changes: 13 additions & 0 deletions tests/alive-tv/vector/scalable/vscale-intrinsic.srctgt.ll
Original file line number Diff line number Diff line change
@@ -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
}
2 changes: 1 addition & 1 deletion tests/unit/vector/scalablevector2.opt
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
; TEST-ARGS: -vscale:2
; TEST-ARGS: -single-vscale:2
; CHECK: <vscale:2 x 2 x i4>
; CHECK: Transformation seems to be correct!

Expand Down
2 changes: 1 addition & 1 deletion tests/unit/vector/scalablevector3.opt
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
; TEST-ARGS: -vscale:1
; TEST-ARGS: -single-vscale:1
; CHECK: <vscale:1 x 2 x i4>
; ERROR: Target is more poisonous than source for i4 %r

Expand Down
14 changes: 11 additions & 3 deletions tools/alive.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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";
}

Expand Down Expand Up @@ -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();
Expand Down
11 changes: 11 additions & 0 deletions tools/alive_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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 <cassert>
#include <memory>
#include <unordered_map>
Expand Down Expand Up @@ -377,6 +379,15 @@ static Type& parse_vector_type() {
unsigned elements = yylval.num;
Type &elemTy = parse_scalar_type();
tokenizer.ensure(CSGT);

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<VectorType>("vty_" + to_string(vector_types.size()),
elements, elemTy, scalable)).get();
Expand Down
Loading