fix crashes related with aggregates load/store
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -296,8 +296,7 @@ StateValue Memory::load(const expr &p, Type &type, unsigned align) {
first = false;
}
- val.value = val.value.trunc(bits);
- return type.fromBV(move(val));
+ return type.fromBV(val.trunc(bits));
}
void Memory::memset(const expr &p, const StateValue &val, const expr &bytes,

MODIFY
ir/state_value.cpp
ir/state_value.cpp
@@ -19,6 +19,11 @@ StateValue StateValue::zext(unsigned amount) const {
non_poison.isBool() ? expr(non_poison) : non_poison.zext(amount) };
}
+StateValue StateValue::trunc(unsigned amount) const {
+ return { value.trunc(amount),
+ non_poison.isBool() ? expr(non_poison) : non_poison.trunc(amount) };
+}
+
StateValue StateValue::zextOrTrunc(unsigned tobw) const {
return
{ value.zextOrTrunc(tobw),

MODIFY
ir/state_value.h
ir/state_value.h
@@ -23,6 +23,7 @@ struct StateValue {
auto bits() const { return value.bits(); }
StateValue zext(unsigned amount) const;
+ StateValue trunc(unsigned amount) const;
StateValue zextOrTrunc(unsigned tobw) const;
StateValue concat(const StateValue &other) const;

MODIFY
ir/type.cpp
ir/type.cpp
@@ -649,6 +649,14 @@ expr AggregateType::enforceAggregateType(vector<Type*> *element_types) const {
return r;
}
+StateValue AggregateType::toBV(StateValue v) const {
+ return v;
+}
+
+StateValue AggregateType::fromBV(StateValue v) const {
+ return v;
+}
+
pair<expr, expr>
AggregateType::refines(const StateValue &src, const StateValue &tgt) const {
set<expr> poison, value;

MODIFY
ir/type.h
ir/type.h
@@ -73,9 +73,9 @@ public:
virtual const StructType* getAsStructType() const;
virtual smt::expr toBV(smt::expr e) const;
- IR::StateValue toBV(IR::StateValue v) const;
+ virtual IR::StateValue toBV(IR::StateValue v) const;
virtual smt::expr fromBV(smt::expr e) const;
- IR::StateValue fromBV(IR::StateValue v) const;
+ virtual IR::StateValue fromBV(IR::StateValue v) const;
// returns pair of refinement constraints for <poison, !poison && value>
virtual std::pair<smt::expr, smt::expr>
@@ -235,6 +235,8 @@ public:
void fixup(const smt::Model &m) override;
smt::expr enforceAggregateType(
std::vector<Type *> *element_types) const override;
+ IR::StateValue toBV(IR::StateValue v) const override;
+ IR::StateValue fromBV(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -258,14 +258,17 @@ bool expr::isFalse() const {
}
bool expr::isZero() const {
+ C();
return eq(mkUInt(0, sort()));
}
bool expr::isOne() const {
+ C();
return eq(mkUInt(1, sort()));
}
bool expr::isAllOnes() const {
+ C();
return eq(mkInt(-1, sort()));
}

fix crashes related with aggregates load/store