fix bitcast between vectors and ints
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -740,41 +740,41 @@ void ConversionOp::print(ostream &os) const {
StateValue ConversionOp::toSMT(State &s) const {
auto v = s[*val];
- function<StateValue(const expr &, const Type &)> fn;
+ function<StateValue(expr &&, const Type &)> fn;
switch (op) {
case SExt:
- fn = [](auto &val, auto &to_type) -> StateValue {
+ fn = [](auto &&val, auto &to_type) -> StateValue {
return { val.sext(to_type.bits() - val.bits()), true };
};
break;
case ZExt:
- fn = [](auto &val, auto &to_type) -> StateValue {
+ fn = [](auto &&val, auto &to_type) -> StateValue {
return { val.zext(to_type.bits() - val.bits()), true };
};
break;
case Trunc:
- fn = [](auto &val, auto &to_type) -> StateValue {
+ fn = [](auto &&val, auto &to_type) -> StateValue {
return { val.trunc(to_type.bits()), true };
};
break;
case BitCast:
- fn = [](auto &val, auto &to_type) -> StateValue {
- return { to_type.fromBV(val), true };
+ fn = [](auto &&val, auto &to_type) -> StateValue {
+ return { to_type.fromInt(move(val)), true };
};
break;
case SIntToFP:
- fn = [](auto &val, auto &to_type) -> StateValue {
+ fn = [](auto &&val, auto &to_type) -> StateValue {
return { val.sint2fp(to_type.getDummyValue(false).value), true };
};
break;
case UIntToFP:
- fn = [](auto &val, auto &to_type) -> StateValue {
+ fn = [](auto &&val, auto &to_type) -> StateValue {
return { val.uint2fp(to_type.getDummyValue(false).value), true };
};
break;
case FPToSInt:
- fn = [](auto &val, auto &to_type) -> StateValue {
+ fn = [](auto &&val, auto &to_type) -> StateValue {
return { val.fp2sint(to_type.bits()),
val.foge(expr::IntSMin(to_type.bits()).sint2fp(val)) &&
val.fole(expr::IntSMax(to_type.bits()).sint2fp(val)) &&
@@ -782,7 +782,7 @@ StateValue ConversionOp::toSMT(State &s) const {
};
break;
case FPToUInt:
- fn = [](auto &val, auto &to_type) -> StateValue {
+ fn = [](auto &&val, auto &to_type) -> StateValue {
return { val.fp2uint(to_type.bits()),
val.foge(expr::mkFloat(0, val)) &&
val.fole(expr::IntUMax(to_type.bits()).uint2fp(val)) &&
@@ -790,19 +790,19 @@ StateValue ConversionOp::toSMT(State &s) const {
};
break;
case Ptr2Int:
- fn = [&](auto &val, auto &to_type) -> StateValue {
+ fn = [&](auto &&val, auto &to_type) -> StateValue {
return { s.getMemory().ptr2int(val).zextOrTrunc(to_type.bits()), true };
};
break;
case Int2Ptr:
- fn = [&](auto &val, auto &to_type) -> StateValue {
+ fn = [&](auto &&val, auto &to_type) -> StateValue {
return { s.getMemory().int2ptr(val), true };
};
break;
}
- auto scalar = [&](const StateValue &sv, const Type &to_type) -> StateValue {
- auto [v, np] = fn(sv.value, to_type);
+ auto scalar = [&](StateValue &&sv, const Type &to_type) -> StateValue {
+ auto [v, np] = fn(move(sv.value), to_type);
return { move(v), sv.non_poison && np };
};
@@ -821,16 +821,17 @@ StateValue ConversionOp::toSMT(State &s) const {
auto valty = op == BitCast ? &int_ty : val->getType().getAsAggregateType();
for (unsigned i = 0; i != elems; ++i) {
- vals.emplace_back(scalar(valty->extract(v, i), retty->getChild(i)));
+ unsigned idx = little_endian ? elems - i - 1 : i;
+ vals.emplace_back(scalar(valty->extract(v, idx), retty->getChild(idx)));
}
return retty->aggregateVals(vals);
}
- // turn poison data into boolean, while keeping value in BV
+ // turn poison data into boolean
if (op == BitCast)
- v = IntType("int", getType().bits()).fromBV(v);
+ v.non_poison = v.non_poison == 0;
- return scalar(v, getType());
+ return scalar(move(v), getType());
}
expr ConversionOp::getTypeConstraints(const Function &f) const {

MODIFY
ir/type.cpp
ir/type.cpp
@@ -210,6 +210,14 @@ StateValue Type::toBV(StateValue v) const {
expr::mkIf(v.non_poison, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) };
}
+expr Type::fromBV(expr e) const {
+ return e;
+}
+
+StateValue Type::fromBV(StateValue v) const {
+ return { fromBV(move(v.value)), v.non_poison == 0 };
+}
+
expr Type::toInt(State &s, expr v) const {
return toBV(move(v));
}
@@ -221,12 +229,12 @@ StateValue Type::toInt(State &s, StateValue v) const {
expr::mkIf(v.non_poison, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) };
}
-expr Type::fromBV(expr e) const {
- return e;
+expr Type::fromInt(expr e) const {
+ return fromBV(move(e));
}
-StateValue Type::fromBV(StateValue v) const {
- return { fromBV(v.value), v.non_poison == 0 };
+StateValue Type::fromInt(StateValue v) const {
+ return { fromInt(move(v.value)), v.non_poison == 0 };
}
expr Type::combine_poison(const expr &boolean, const expr &orig) const {
@@ -369,6 +377,26 @@ unsigned FloatType::bits() const {
return float_sizes[fpType].first;
}
+const FloatType* FloatType::getAsFloatType() const {
+ return this;
+}
+
+expr FloatType::toBV(expr e) const {
+ return e.float2BV();
+}
+
+StateValue FloatType::toBV(StateValue v) const {
+ return Type::toBV(move(v));
+}
+
+expr FloatType::fromBV(expr e) const {
+ return e.BV2float(getDummyValue(true).value);
+}
+
+StateValue FloatType::fromBV(StateValue v) const {
+ return Type::fromBV(move(v));
+}
+
expr FloatType::toInt(State &s, expr fp) const {
expr isnan = fp.isNaN();
expr val = fp.float2BV();
@@ -397,26 +425,6 @@ StateValue FloatType::toInt(State &s, StateValue v) const {
return Type::toInt(s, move(v));
}
-const FloatType* FloatType::getAsFloatType() const {
- return this;
-}
-
-expr FloatType::toBV(expr e) const {
- return e.float2BV();
-}
-
-StateValue FloatType::toBV(StateValue v) const {
- return Type::toBV(move(v));
-}
-
-expr FloatType::fromBV(expr e) const {
- return e.BV2float(getDummyValue(true).value);
-}
-
-StateValue FloatType::fromBV(StateValue v) const {
- return Type::fromBV(move(v));
-}
-
expr FloatType::sizeVar() const {
return defined ? expr::mkUInt(bits(), var_bw_bits) : Type::sizeVar();
}
@@ -563,6 +571,22 @@ expr PtrType::enforcePtrType() const {
return true;
}
+expr PtrType::toInt(State &s, expr v) const {
+ return v;
+}
+
+StateValue PtrType::toInt(State &s, StateValue v) const {
+ return Type::toInt(s, move(v));
+}
+
+expr PtrType::fromInt(expr v) const {
+ return v;
+}
+
+StateValue PtrType::fromInt(StateValue v) const {
+ return Type::fromInt(move(v));
+}
+
pair<expr, expr>
PtrType::refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const {
@@ -732,6 +756,14 @@ StateValue AggregateType::toBV(StateValue v) const {
return v;
}
+expr AggregateType::fromBV(expr e) const {
+ return Type::fromBV(move(e));
+}
+
+StateValue AggregateType::fromBV(StateValue v) const {
+ return v;
+}
+
expr AggregateType::toInt(State &s, expr v) const {
UNREACHABLE();
}
@@ -744,17 +776,17 @@ StateValue AggregateType::toInt(State &s, StateValue v) const {
StateValue ret;
for (unsigned i = 0; i < elements; ++i) {
auto vv = children[i]->toInt(s, extract(v, i));
- ret = i == 0 ? move(vv) : ret.concat(vv);
+ ret = i == 0 ? move(vv) : (little_endian ? vv.concat(ret) : ret.concat(vv));
}
return ret;
}
-expr AggregateType::fromBV(expr e) const {
- return Type::fromBV(move(e));
+expr AggregateType::fromInt(expr v) const {
+ UNREACHABLE();
}
-StateValue AggregateType::fromBV(StateValue v) const {
- return v;
+StateValue AggregateType::fromInt(StateValue v) const {
+ UNREACHABLE();
}
pair<expr, expr>
@@ -1117,6 +1149,14 @@ StateValue SymbolicType::toBV(StateValue val) const {
DISPATCH(toBV(move(val)), UNREACHABLE());
}
+expr SymbolicType::fromBV(expr e) const {
+ DISPATCH(fromBV(move(e)), UNREACHABLE());
+}
+
+StateValue SymbolicType::fromBV(StateValue val) const {
+ DISPATCH(fromBV(move(val)), UNREACHABLE());
+}
+
expr SymbolicType::toInt(State &st, expr e) const {
DISPATCH(toInt(st, move(e)), UNREACHABLE());
}
@@ -1125,12 +1165,12 @@ StateValue SymbolicType::toInt(State &st, StateValue val) const {
DISPATCH(toInt(st, move(val)), UNREACHABLE());
}
-expr SymbolicType::fromBV(expr e) const {
- DISPATCH(fromBV(move(e)), UNREACHABLE());
+expr SymbolicType::fromInt(expr e) const {
+ DISPATCH(fromInt(move(e)), UNREACHABLE());
}
-StateValue SymbolicType::fromBV(StateValue val) const {
- DISPATCH(fromBV(move(val)), UNREACHABLE());
+StateValue SymbolicType::fromInt(StateValue val) const {
+ DISPATCH(fromInt(move(val)), UNREACHABLE());
}
pair<expr, expr>

MODIFY
ir/type.h
ir/type.h
@@ -90,11 +90,14 @@ public:
virtual smt::expr toBV(smt::expr e) const;
virtual IR::StateValue toBV(IR::StateValue v) const;
- virtual smt::expr toInt(State &s, smt::expr v) const;
- virtual IR::StateValue toInt(State &s, IR::StateValue v) const;
virtual smt::expr fromBV(smt::expr e) const;
virtual IR::StateValue fromBV(IR::StateValue v) const;
+ virtual smt::expr toInt(State &s, smt::expr v) const;
+ virtual IR::StateValue toInt(State &s, IR::StateValue v) const;
+ virtual smt::expr fromInt(smt::expr v) const;
+ virtual IR::StateValue fromInt(IR::StateValue v) const;
+
// combine existing poison value in BV repr with a new boolean expr
smt::expr combine_poison(const smt::expr &boolean,
const smt::expr &orig) const;
@@ -190,10 +193,10 @@ public:
const FloatType* getAsFloatType() const override;
smt::expr toBV(smt::expr e) const override;
IR::StateValue toBV(IR::StateValue v) const override;
- smt::expr toInt(State &s, smt::expr v) const override;
- IR::StateValue toInt(State &s, IR::StateValue v) const override;
smt::expr fromBV(smt::expr e) const override;
IR::StateValue fromBV(IR::StateValue v) const override;
+ smt::expr toInt(State &s, smt::expr v) const override;
+ IR::StateValue toInt(State &s, IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
@@ -220,6 +223,10 @@ public:
void fixup(const smt::Model &m) override;
bool isPtrType() const override;
smt::expr enforcePtrType() const override;
+ smt::expr toInt(State &s, smt::expr v) const override;
+ IR::StateValue toInt(State &s, IR::StateValue v) const override;
+ smt::expr fromInt(smt::expr v) const override;
+ IR::StateValue fromInt(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
@@ -263,10 +270,12 @@ public:
std::vector<Type *> *element_types) const override;
smt::expr toBV(smt::expr e) const override;
IR::StateValue toBV(IR::StateValue v) const override;
- smt::expr toInt(State &s, smt::expr v) const override;
- IR::StateValue toInt(State &s, IR::StateValue v) const override;
smt::expr fromBV(smt::expr e) const override;
IR::StateValue fromBV(IR::StateValue v) const override;
+ smt::expr toInt(State &s, smt::expr v) const override;
+ IR::StateValue toInt(State &s, IR::StateValue v) const override;
+ smt::expr fromInt(smt::expr v) const override;
+ IR::StateValue fromInt(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
@@ -362,10 +371,12 @@ public:
const StructType* getAsStructType() const override;
smt::expr toBV(smt::expr e) const override;
IR::StateValue toBV(IR::StateValue v) const override;
- smt::expr toInt(State &s, smt::expr v) const override;
- IR::StateValue toInt(State &s, IR::StateValue v) const override;
smt::expr fromBV(smt::expr e) const override;
IR::StateValue fromBV(IR::StateValue v) const override;
+ smt::expr toInt(State &s, smt::expr v) const override;
+ IR::StateValue toInt(State &s, IR::StateValue v) const override;
+ smt::expr fromInt(smt::expr v) const override;
+ IR::StateValue fromInt(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;

fix bitcast between vectors and ints