start a very simple memory model
MODIFY
CMakeLists.txt
CMakeLists.txt
@@ -48,7 +48,9 @@ set(IR_SRCS
ir/constant.cpp
ir/function.cpp
ir/instr.cpp
+ ir/memory.cpp
ir/state.cpp
+ ir/state_value.cpp
ir/type.cpp
ir/value.cpp
)

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -247,32 +247,32 @@ StateValue BinOp::toSMT(State &s) const {
case SAdd_Overflow:
val = a + b;
- val = val.concat(expr::toBVBool(!a.add_no_soverflow(b)));
+ val = val.concat((!a.add_no_soverflow(b)).toBVBool());
break;
case UAdd_Overflow:
val = a + b;
- val = val.concat(expr::toBVBool(!a.add_no_uoverflow(b)));
+ val = val.concat((!a.add_no_uoverflow(b)).toBVBool());
break;
case SSub_Overflow:
val = a - b;
- val = val.concat(expr::toBVBool(!a.sub_no_soverflow(b)));
+ val = val.concat((!a.sub_no_soverflow(b)).toBVBool());
break;
case USub_Overflow:
val = a - b;
- val = val.concat(expr::toBVBool(!a.sub_no_uoverflow(b)));
+ val = val.concat((!a.sub_no_uoverflow(b)).toBVBool());
break;
case SMul_Overflow:
val = a * b;
- val = val.concat(expr::toBVBool(!a.mul_no_soverflow(b)));
+ val = val.concat((!a.mul_no_soverflow(b)).toBVBool());
break;
case UMul_Overflow:
val = a * b;
- val = val.concat(expr::toBVBool(!a.mul_no_uoverflow(b)));
+ val = val.concat((!a.mul_no_uoverflow(b)).toBVBool());
break;
case ExtractValue:
@@ -899,9 +899,9 @@ void Load::print(std::ostream &os) const {
}
StateValue Load::toSMT(State &s) const {
- // TODO
- s.addUB({});
- return {};
+ auto &[p, np] = s[ptr];
+ s.addUB(np);
+ return s.getMemory().load(p, getType().bits());
}
expr Load::getTypeConstraints(const Function &f) const {
@@ -919,8 +919,9 @@ void Store::print(std::ostream &os) const {
}
StateValue Store::toSMT(State &s) const {
- // TODO
- s.addUB({});
+ auto &[p, np] = s[ptr];
+ s.addUB(np);
+ s.getMemory().store(p, s[val]);
return {};
}

ADD
ir/memory.cpp
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "ir/memory.h"
+#include "ir/state.h"
+#include "util/compiler.h"
+
+using namespace smt;
+using namespace std;
+using namespace util;
+
+namespace {
+struct Pointer {
+ IR::Memory &m;
+ // [offset, local_bid, nonlocal_bid]
+ const expr &p;
+
+ Pointer(IR::Memory *m, const expr &p) : m(*m), p(p) {}
+
+ expr get_offset() const {
+ // FIXME
+ return p.extract(0, 0);
+ }
+
+ const expr& operator()() const {
+ return p;
+ }
+
+ void operator++(void) {
+ // TODO
+ }
+
+ void is_dereferenceable(unsigned bytes) {
+ // TODO
+ }
+};
+}
+
+namespace IR {
+
+Memory::Memory(State &state) : state(state) {
+ unsigned bits_bids = bits_for_local_bid + bits_for_nonlocal_bid;
+ blocks_size = expr::mkArray("blks_size",
+ expr::mkUInt(0, bits_bids),
+ expr::mkUInt(0, bits_size_t));
+
+ blocks_val = expr::mkArray("blks_val",
+ expr::mkUInt(0, bits_bids + bits_for_offset),
+ expr::mkUInt(0, 8 + 1)); // 1 byte + 1 bit poison
+}
+
+void Memory::store(const expr &p, const StateValue &v) {
+ unsigned bits = v.value.bits();
+ unsigned bytes = divide_up(bits, 8);
+
+ Pointer ptr(this, p);
+ ptr.is_dereferenceable(bytes);
+
+ 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?
+ blocks_val = blocks_val.store(ptr(),
+ poison.concat(val.extract((i+1)*8 - 1, i*8)));
+ ++ptr;
+ }
+}
+
+StateValue Memory::load(const expr &p, unsigned bits) {
+ unsigned bytes = divide_up(bits, 8);
+ Pointer ptr(this, p);
+ ptr.is_dereferenceable(bytes);
+
+ expr val, non_poison;
+ bool first = true;
+
+ for (unsigned i = 0; i < bytes; ++i) {
+ expr pair = blocks_val.load(ptr());
+ expr v = pair.extract(7, 0);
+ expr p = pair.extract(8, 8) == expr::mkUInt(1, 1);
+
+ if (first) {
+ val = move(v);
+ non_poison = move(p);
+ } else {
+ val = v.concat(val);
+ non_poison &= p;
+ }
+ first = false;
+ ++ptr;
+ }
+
+ return { val.trunc(bits), move(non_poison) };
+}
+
+Memory Memory::ite(const expr &cond, const Memory &then, const Memory &els) {
+ // TODO
+ return then;
+}
+
+}

ADD
ir/memory.h
+#pragma once
+
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "ir/state_value.h"
+#include "smt/expr.h"
+
+namespace IR {
+
+class State;
+
+class Memory {
+ State &state;
+
+ // FIXME: these should be tuned per function
+ unsigned bits_for_offset = 32;
+ unsigned bits_for_local_bid = 8;
+ unsigned bits_for_nonlocal_bid = 8;
+ unsigned bits_size_t = 64;
+
+ smt::expr blocks_size; // array: bid -> size in bytes
+ smt::expr blocks_val; // array: (bid, offset) -> StateValue
+
+public:
+ Memory(State &state);
+
+ void store(const smt::expr &ptr, const StateValue &val);
+ StateValue load(const smt::expr &ptr, unsigned bits);
+
+ static Memory ite(const smt::expr &cond, const Memory &then,
+ const Memory &els);
+};
+
+}

MODIFY
ir/state.cpp
ir/state.cpp
#include "ir/state.h"
#include "ir/function.h"
-#include "smt/expr.h"
#include "smt/smt.h"
#include <cassert>
@@ -12,17 +11,7 @@ using namespace std;
namespace IR {
-StateValue StateValue::mkIf(const expr &cond, const StateValue &then,
- const StateValue &els) {
- return { expr::mkIf(cond, then.value, els.value),
- expr::mkIf(cond, then.non_poison, els.non_poison) };
-}
-
-ostream& operator<<(ostream &os, const StateValue &val) {
- return os << val.value << " / " << val.non_poison;
-}
-
-State::State(const Function &f) : f(f) {
+State::State(const Function &f) : f(f), memory(*this) {
predecessor_domain[&f.getFirstBB()].try_emplace(nullptr, true, set<expr>());
}

MODIFY
ir/state.h
ir/state.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include "ir/memory.h"
+#include "ir/state_value.h"
#include "smt/expr.h"
#include <array>
#include <ostream>
@@ -17,30 +19,6 @@ namespace IR {
struct LoopInCFGDetected : public std::exception {};
struct OutOfMemory : public std::exception {};
-
-struct StateValue {
- smt::expr value, non_poison;
-
- StateValue() {}
- StateValue(smt::expr &&value, smt::expr &&non_poison)
- : value(std::move(value)), non_poison(std::move(non_poison)) {}
-
- static StateValue mkIf(const smt::expr &cond, const StateValue &then,
- const StateValue &els);
-
- bool eq(const StateValue &other) const {
- return value.eq(other.value) && non_poison.eq(other.non_poison);
- }
-
- StateValue
- subst(const std::vector<std::pair<smt::expr, smt::expr>> &repls) const {
- return { value.subst(repls), non_poison.subst(repls) };
- }
-
- friend std::ostream& operator<<(std::ostream &os, const StateValue &val);
-};
-
-
class Value;
class BasicBlock;
class Function;
@@ -67,6 +45,7 @@ private:
// temp state
DomainTy domain;
+ Memory memory;
std::set<smt::expr> undef_vars;
std::array<StateValue, 32> tmp_values;
unsigned i_tmp_values = 0; // next available position in tmp_values
@@ -98,6 +77,7 @@ public:
void addUndefVar(const smt::expr &var);
void resetUndefVars();
+ auto& getMemory() { return memory; }
auto& getFn() const { return f; }
const auto& getValues() const { return values; }
const auto& getQuantVars() const { return quantified_vars; }

ADD
ir/state_value.cpp
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "ir/state_value.h"
+
+using namespace smt;
+using namespace std;
+
+namespace IR {
+
+StateValue StateValue::mkIf(const expr &cond, const StateValue &then,
+ const StateValue &els) {
+ return { expr::mkIf(cond, then.value, els.value),
+ expr::mkIf(cond, then.non_poison, els.non_poison) };
+}
+
+bool StateValue::eq(const StateValue &other) const {
+ return value.eq(other.value) && non_poison.eq(other.non_poison);
+}
+
+StateValue StateValue::subst(const vector<pair<expr, expr>> &repls) const {
+ return { value.subst(repls), non_poison.subst(repls) };
+}
+
+ostream& operator<<(ostream &os, const StateValue &val) {
+ return os << val.value << " / " << val.non_poison;
+}
+
+}

ADD
ir/state_value.h
+#pragma once
+
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "smt/expr.h"
+#include <utility>
+#include <vector>
+
+namespace IR {
+
+struct StateValue {
+ smt::expr value, non_poison;
+
+ StateValue() {}
+ StateValue(smt::expr &&value, smt::expr &&non_poison)
+ : value(std::move(value)), non_poison(std::move(non_poison)) {}
+
+ static StateValue mkIf(const smt::expr &cond, const StateValue &then,
+ const StateValue &els);
+
+ bool eq(const StateValue &other) const;
+
+ StateValue
+ subst(const std::vector<std::pair<smt::expr, smt::expr>> &repls) const;
+
+ friend std::ostream& operator<<(std::ostream &os, const StateValue &val);
+};
+
+}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -185,11 +185,6 @@ expr expr::mkBoolVar(const char *name) {
return ::mkVar(name, Z3_mk_bool_sort(ctx()));
}
-expr expr::toBVBool(const expr &e) {
- auto sort = mkBVSort(1);
- return mkIf(e, mkUInt(1, sort), mkUInt(0, sort));
-}
-
expr expr::IntSMin(unsigned bits) {
assert(bits > 0);
static_assert(sizeof(unsigned long long) == 8);
@@ -956,6 +951,9 @@ expr expr::extract(unsigned high, unsigned low) const {
C();
assert(high >= low && high < bits());
+ if (low == 0 && high == bits()-1)
+ return *this;
+
{
expr sub;
unsigned high_2, low_2;
@@ -975,7 +973,13 @@ expr expr::extract(unsigned high, unsigned low) const {
return Z3_mk_extract(ctx(), high, low, ast());
}
+expr expr::toBVBool() const {
+ auto sort = mkBVSort(1);
+ return mkIf(*this, mkUInt(1, sort), mkUInt(0, sort));
+}
+
expr expr::mkUF(const char *name, const vector<expr> &args, const expr &range) {
+ C2(range);
auto num_args = args.size();
vector<Z3_ast> z3_args;
vector<Z3_sort> z3_sorts;
@@ -994,6 +998,21 @@ expr expr::mkUF(const char *name, const vector<expr> &args, const expr &range){
return Z3_mk_app(ctx(), decl, num_args, z3_args.data());
}
+expr expr::mkArray(const char *name, const expr &domain, const expr &range) {
+ C2(domain, range);
+ return ::mkVar(name, Z3_mk_array_sort(ctx(), domain.sort(), range.sort()));
+}
+
+expr expr::store(const expr &idx, const expr &val) const {
+ C(idx, val);
+ return Z3_mk_store(ctx(), ast(), idx(), val());
+}
+
+expr expr::load(const expr &idx) const {
+ C(idx);
+ return Z3_mk_select(ctx(), ast(), idx());
+}
+
expr expr::mkIf(const expr &cond, const expr &then, const expr &els) {
C2(cond, then, els);
if (cond.isTrue() || then.eq(els))

MODIFY
smt/expr.h
smt/expr.h
@@ -75,7 +75,6 @@ public:
static expr mkInt(const char *n, unsigned bits);
static expr mkVar(const char *name, unsigned bits);
static expr mkBoolVar(const char *name);
- static expr toBVBool(const expr &e);
static expr IntSMin(unsigned bits);
static expr IntSMax(unsigned bits);
@@ -190,11 +189,17 @@ public:
expr concat(const expr &rhs) const;
expr extract(unsigned high, unsigned low) const;
+ expr toBVBool() const;
+
// we don't expose SMT expr types, so range must be passed as a dummy value
// of the desired type
static expr mkUF(const char *name, const std::vector<expr> &args,
const expr &range);
+ static expr mkArray(const char *name, const expr &domain, const expr &range);
+ expr store(const expr &idx, const expr &val) const;
+ expr load(const expr &idx) const;
+
static expr mkIf(const expr &cond, const expr &then, const expr &els);
static expr mkForAll(const std::set<expr> &vars, expr &&val);

MODIFY
util/compiler.cpp
util/compiler.cpp
@@ -61,4 +61,8 @@ unsigned num_trailing_zeros(uint64_t n) {
#endif
}
+uint64_t divide_up(uint64_t n, uint64_t amount) {
+ return (n + amount - 1) / amount;
+}
+
}

MODIFY
util/compiler.h
util/compiler.h
@@ -46,4 +46,6 @@ unsigned num_sign_bits(uint64_t n);
unsigned num_leading_zeros(uint64_t n);
unsigned num_trailing_zeros(uint64_t n);
+uint64_t divide_up(uint64_t n, uint64_t amount); // division with ceiling
+
}

start a very simple memory model