Move AggregateConst to AggregateValue
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -70,40 +70,6 @@ StateValue FloatConst::toSMT(State &s) const {
}
-static string agg_const_str(vector<Value*> &vals) {
- string r = "{ ";
- bool first = true;
- for (auto val : vals) {
- if (!first)
- r += ", ";
- r += val->getName();
- first = false;
- }
- return r + " }";
-}
-
-AggregateConst::AggregateConst(Type &type, vector<Value*> &&vals)
- : Constant(type, agg_const_str(vals)), vals(move(vals)) {}
-
-StateValue AggregateConst::toSMT(State &s) const {
- vector<StateValue> state_vals;
- for (auto val : vals) {
- state_vals.emplace_back(val->toSMT(s));
- }
- return getType().getAsAggregateType()->aggregateVals(state_vals);
-}
-
-expr AggregateConst::getTypeConstraints() const {
- expr r = Value::getTypeConstraints();
- vector<Type*> types;
- for (auto val : vals) {
- types.emplace_back(&val->getType());
- r &= val->getTypeConstraints();
- }
- return r && getType().enforceAggregateType(&types);
-}
-
-
StateValue ConstantInput::toSMT(State &s) const {
auto type = getType().getDummyValue(false).value;
return { expr::mkVar(getName().c_str(), type), true };

MODIFY
ir/constant.h
ir/constant.h
@@ -42,17 +42,6 @@ public:
};
-class AggregateConst final : public Constant {
- std::vector<Value*> vals;
-public:
- AggregateConst(Type &type, std::vector<Value*> &&vals);
- auto& getVals() const { return vals; }
-
- StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
-};
-
-
class ConstantInput final : public Constant {
public:
ConstantInput(Type &type, std::string &&name)

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2093,7 +2093,7 @@ StateValue ShuffleVector::toSMT(State &s) const {
auto &vect1 = s[*v1];
auto &vect2 = s[*v2];
- auto &mask_vector = static_cast<AggregateConst*>(mask)->getVals();
+ auto &mask_vector = static_cast<AggregateValue*>(mask)->getVals();
for (unsigned i = 0, e = mty->numElementsConst(); i != e; ++i) {
auto mask = mask_vector[i];

MODIFY
ir/value.cpp
ir/value.cpp
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include "ir/instr.h"
#include "ir/value.h"
#include "smt/expr.h"
#include "util/compiler.h"
@@ -135,6 +136,50 @@ StateValue Input::toSMT(State &s) const {
: expr::mkIf(type.extract(1, 1) == 0, non_poison, poison) };
}
+
+static string agg_str(vector<Value*> &vals) {
+ string r = "{ ";
+ bool first = true;
+ for (auto val : vals) {
+ if (!first)
+ r += ", ";
+ r += val->getName();
+ first = false;
+ }
+ return r + " }";
+}
+
+
+AggregateValue::AggregateValue(Type &type, vector<Value*> &&vals)
+ : Value(type, agg_str(vals)), vals(move(vals)) {}
+
+StateValue AggregateValue::toSMT(State &s) const {
+ vector<StateValue> state_vals;
+ for (auto val : vals) {
+ state_vals.emplace_back(val->toSMT(s));
+ }
+ return getType().getAsAggregateType()->aggregateVals(state_vals);
+}
+
+expr AggregateValue::getTypeConstraints() const {
+ expr r = Value::getTypeConstraints();
+ vector<Type*> types;
+ for (auto val : vals) {
+ types.emplace_back(&val->getType());
+ if (dynamic_cast<const Instr*>(val))
+ // Instr's type constraints are already generated by BasicBlock's
+ // getTypeConstraints()
+ continue;
+ r &= val->getTypeConstraints();
+ }
+ return r && getType().enforceAggregateType(&types);
+}
+
+void AggregateValue::print(std::ostream &os) const {
+ UNREACHABLE();
+}
+
+
expr Input::getTyVar() const {
string tyname = "ty_" + smt_name;
return expr::mkVar(tyname.c_str(), 2);

MODIFY
ir/value.h
ir/value.h
@@ -95,6 +95,17 @@ public:
};
+class AggregateValue final : public Value {
+ std::vector<Value*> vals;
+public:
+ AggregateValue(Type &type, std::vector<Value*> &&vals);
+ auto& getVals() const { return vals; }
+ smt::expr getTypeConstraints() const override;
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+};
+
+
class Input final : public Value {
std::string smt_name;
public:

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -237,7 +237,7 @@ Value* get_operand(llvm::Value *v,
else
return nullptr;
}
- auto val = make_unique<AggregateConst>(*ty, move(vals));
+ auto val = make_unique<AggregateValue>(*ty, move(vals));
auto ret = val.get();
current_fn->addConstant(move(val));
return ret;
@@ -251,7 +251,7 @@ Value* get_operand(llvm::Value *v,
else
return nullptr;
}
- auto val = make_unique<AggregateConst>(*ty, move(vals));
+ auto val = make_unique<AggregateValue>(*ty, move(vals));
auto ret = val.get();
current_fn->addConstant(move(val));
return ret;
@@ -265,7 +265,7 @@ Value* get_operand(llvm::Value *v,
else
return nullptr;
}
- auto val = make_unique<AggregateConst>(*ty, move(vals));
+ auto val = make_unique<AggregateValue>(*ty, move(vals));
auto ret = val.get();
current_fn->addConstant(move(val));
return ret;

ADD
tests/alive-tv/constexpr/aggregate.src.ll
+@a = constant i32 0
+@x = constant { i8*, i8* } { i8* bitcast (i32* @a to i8*), i8* bitcast (i32* @a to i8*) }
+
+define i8* @f() {
+ %a = load { i8*, i8* }, { i8*, i8* }* @x
+ %b = extractvalue {i8*, i8*} %a, 0
+ ret i8* %b
+}
+

ADD
tests/alive-tv/constexpr/aggregate.tgt.ll
+@a = constant i32 0
+@x = constant { i8*, i8* } { i8* bitcast (i32* @a to i8*), i8* bitcast (i32* @a to i8*) }
+
+define i8* @f() {
+ ret i8* bitcast (i32* @a to i8*)
+}
+

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -483,7 +483,7 @@ static Value& parse_vector_constant(Type &type) {
tokenizer.ensure(CSGT);
- auto c = make_unique<AggregateConst>(type, move(vals));
+ auto c = make_unique<AggregateValue>(type, move(vals));
auto ret = c.get();
fn->addConstant(move(c));
return *ret;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -331,7 +331,7 @@ static bool has_nullptr(const Value *v) {
// undef pointer points to the nullblk
return true;
- if (auto agg = dynamic_cast<const AggregateConst*>(v)) {
+ if (auto agg = dynamic_cast<const AggregateValue*>(v)) {
for (auto val : agg->getVals()) {
if (has_nullptr(val))
return true;

Move AggregateConst to AggregateValue (#199) (#200)