add support for input ptrs
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -93,6 +93,16 @@ Memory::Memory(State &state) : state(&state) {
assert(bits_for_offset <= bits_size_t);
}
+pair<expr, vector<expr>> Memory::mkInput(const char *name) {
+ unsigned bits = bits_for_nonlocal_bid + bits_for_offset;
+ expr var = expr::mkVar(name, bits);
+ // [offset, local_bid, nonlocal_bid]
+ expr offset = var.extract(bits - 1, bits_for_nonlocal_bid);
+ expr bid = var.extract(bits_for_nonlocal_bid - 1, 0);
+ expr val = offset.concat(expr::mkUInt(0, bits_for_local_bid).concat(bid));
+ return { move(val), { var } };
+}
+
expr Memory::alloc(const expr &bytes, unsigned align, bool local) {
Pointer p(*this, last_bid++, local);
// TODO: handle alignment

MODIFY
ir/memory.h
ir/memory.h
#include "ir/state_value.h"
#include "smt/expr.h"
+#include <utility>
+#include <vector>
namespace IR {
@@ -60,6 +62,8 @@ class Memory {
public:
Memory(State &state);
+ std::pair<smt::expr, std::vector<smt::expr>> mkInput(const char *name);
+
smt::expr alloc(const smt::expr &bytes, unsigned align, bool local);
void free(const smt::expr &ptr);

MODIFY
ir/type.cpp
ir/type.cpp
@@ -397,8 +397,7 @@ expr PtrType::enforcePtrType() const {
}
pair<expr, vector<expr>> PtrType::mkInput(State &s, const char *name) const {
- // TODO
- return {};
+ return s.getMemory().mkInput(name);
}
void PtrType::print(ostream &os) const {
@@ -576,8 +575,18 @@ const StructType* StructType::getAsStructType() const {
}
pair<expr, vector<expr>> StructType::mkInput(State &s, const char *name) const {
- // TODO
- return {};
+ expr val;
+ vector<expr> vars;
+ unsigned num = 0;
+
+ for (auto c : children) {
+ string c_name = string(name) + "#" + to_string(num);
+ auto [v, vs] = c->mkInput(s, c_name.c_str());
+ val = num == 0 ? v : val.concat(v);
+ vars.insert(vars.end(), vs.begin(), vs.end());
+ ++num;
+ }
+ return { move(val), move(vars) };
}
void StructType::print(ostream &os) const {

add support for input ptrs