add support for load/store of floats
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1247,7 +1247,7 @@ void Load::print(std::ostream &os) const {
StateValue Load::toSMT(State &s) const {
auto &[p, np] = s[ptr];
s.addUB(np);
- return s.getMemory().load(p, getType().bits(), align);
+ return s.getMemory().load(p, getType(), align);
}
expr Load::getTypeConstraints(const Function &f) const {
@@ -1267,7 +1267,7 @@ void Store::print(std::ostream &os) const {
StateValue Store::toSMT(State &s) const {
auto &[p, np] = s[ptr];
s.addUB(np);
- s.getMemory().store(p, s[val], align);
+ s.getMemory().store(p, s[val], val.getType(), align);
return {};
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -203,16 +203,30 @@ void Memory::free(const expr &ptr) {
// TODO
}
-void Memory::store(const expr &p, const StateValue &v, unsigned align) {
- unsigned bits = v.value.bits();
+void Memory::store(const expr &p, const StateValue &v, Type &type,
+ unsigned align) {
+ expr val = v.value;
+ expr poison = v.non_poison.toBVBool();
+
+ if (type.isIntType()) {
+ // do nothing
+ } else if (type.isFloatType()) {
+ val = val.float2BV();
+ } else if (type.isPtrType()) {
+ // TODO
+ val = expr();
+ } else {
+ UNREACHABLE();
+ }
+
+ unsigned bits = val.bits();
unsigned bytes = divide_up(bits, 8);
+ val = val.zext(bytes * 8 - bits);
+
Pointer ptr(*this, p);
ptr.is_dereferenceable(bytes, align);
- expr poison = v.non_poison.toBVBool();
- expr val = v.value.zext(bytes * 8 - bits);
-
for (unsigned i = 0; i < bytes; ++i) {
// FIXME: right now we store in little-endian; consider others?
expr data = val.extract((i + 1) * 8 - 1, i * 8);
@@ -221,7 +235,8 @@ void Memory::store(const expr &p, const StateValue &v, unsigned align) {
}
}
-StateValue Memory::load(const expr &p, unsigned bits, unsigned align) {
+StateValue Memory::load(const expr &p, Type &type, unsigned align) {
+ auto bits = type.bits();
unsigned bytes = divide_up(bits, 8);
Pointer ptr(*this, p);
ptr.is_dereferenceable(bytes, align);
@@ -245,7 +260,19 @@ StateValue Memory::load(const expr &p, unsigned bits, unsigned align) {
first = false;
}
- return { val.trunc(bits), move(non_poison) };
+ val = val.trunc(bits);
+ if (type.isIntType()) {
+ // do nothing
+ } else if (type.isFloatType()) {
+ val = val.BV2float(type.getDummyValue());
+ } else if (type.isPtrType()) {
+ // TODO
+ val = expr();
+ } else {
+ UNREACHABLE();
+ }
+
+ return { move(val), move(non_poison) };
}
void Memory::memset(const expr &p, const StateValue &val, const expr &bytes,

MODIFY
ir/memory.h
ir/memory.h
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/state_value.h"
+#include "ir/type.h"
#include "smt/expr.h"
#include <ostream>
#include <string>
@@ -98,8 +99,9 @@ public:
smt::expr alloc(const smt::expr &bytes, unsigned align, bool local);
void free(const smt::expr &ptr);
- void store(const smt::expr &ptr, const StateValue &val, unsigned align);
- StateValue load(const smt::expr &ptr, unsigned bits, unsigned align);
+ void store(const smt::expr &ptr, const StateValue &val, Type &type,
+ unsigned align);
+ StateValue load(const smt::expr &ptr, Type &type, unsigned align);
void memset(const smt::expr &ptr, const StateValue &val,
const smt::expr &bytes, unsigned align);

add support for load/store of floats