add pointer refinement
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -333,6 +333,27 @@ expr Pointer::get_alloc_type() const {
return get_value("blk_kind", m.local_blk_kind, expr::mkUInt(0, 2));
}
+expr Pointer::is_heap_allocated() const {
+ return get_alloc_type() != NON_HEAP;
+}
+
+expr Pointer::refined(const Pointer &other) const {
+ // This refers to a block that was malloc'ed within the function
+ expr local = other.is_heap_allocated();
+ local &= other.is_block_alive();
+ local &= other.block_size().uge(block_size());
+ local &= block_refined(other);
+
+ local = (is_heap_allocated() && is_block_alive()).implies(local);
+
+ return expr::mkIf(is_local(), local, *this == other);
+}
+
+expr Pointer::block_refined(const Pointer &other) const {
+ // TODO
+ return true;
+}
+
expr Pointer::is_readonly() const {
return !is_local() && expr::mkUF("blk_readonly", { get_short_bid() }, false);
}

MODIFY
ir/memory.h
ir/memory.h
@@ -92,6 +92,10 @@ public:
CXX_NEW,
};
smt::expr get_alloc_type() const;
+ smt::expr is_heap_allocated() const;
+
+ smt::expr refined(const Pointer &other) const;
+ smt::expr block_refined(const Pointer &other) const;
const Memory& getMemory() const { return m; }

MODIFY
ir/type.cpp
ir/type.cpp
@@ -252,7 +252,8 @@ void VoidType::fixup(const Model &m) {
}
pair<expr, expr>
-VoidType::refines(const StateValue &src, const StateValue &tgt) const {
+VoidType::refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const {
return { true, true };
}
@@ -308,7 +309,8 @@ expr IntType::enforceIntType(unsigned bits) const {
}
pair<expr, expr>
-IntType::refines(const StateValue &src, const StateValue &tgt) const {
+IntType::refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const {
return { src.non_poison.implies(tgt.non_poison),
(src.non_poison && tgt.non_poison).implies(src.value == tgt.value) };
}
@@ -419,7 +421,8 @@ expr FloatType::enforceFloatType() const {
}
pair<expr, expr>
-FloatType::refines(const StateValue &src, const StateValue &tgt) const {
+FloatType::refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const {
expr non_poison = src.non_poison && tgt.non_poison;
return { src.non_poison.implies(tgt.non_poison),
(non_poison && !src.value.isNaN()).implies(src.value == tgt.value) };
@@ -514,9 +517,13 @@ expr PtrType::enforcePtrType() const {
}
pair<expr, expr>
-PtrType::refines(const StateValue &src, const StateValue &tgt) const {
+PtrType::refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const {
+ Pointer p(src_s.getMemory(), src.value);
+ Pointer q(tgt_s.getMemory(), tgt.value);
+
return { src.non_poison.implies(tgt.non_poison),
- (src.non_poison && tgt.non_poison).implies(src.value == tgt.value) };
+ (src.non_poison && tgt.non_poison).implies(p.refined(q)) };
}
pair<expr, vector<expr>> PtrType::mkInput(State &s, const char *name) const {
@@ -666,10 +673,12 @@ StateValue AggregateType::fromBV(StateValue v) const {
}
pair<expr, expr>
-AggregateType::refines(const StateValue &src, const StateValue &tgt) const {
+AggregateType::refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const {
set<expr> poison, value;
for (unsigned i = 0; i < elements; ++i) {
- auto [p, v] = children[i]->refines(extract(src, i), extract(tgt, i));
+ auto [p, v] = children[i]->refines(src_s, tgt_s, extract(src, i),
+ extract(tgt, i));
poison.insert(move(p));
value.insert(move(v));
}
@@ -1011,8 +1020,9 @@ StateValue SymbolicType::fromBV(StateValue val) const {
}
pair<expr, expr>
-SymbolicType::refines(const StateValue &src, const StateValue &tgt) const {
- DISPATCH(refines(src, tgt), UNREACHABLE());
+SymbolicType::refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const {
+ DISPATCH(refines(src_s, tgt_s, src, tgt), UNREACHABLE());
}
pair<expr, vector<expr>>

MODIFY
ir/type.h
ir/type.h
@@ -98,7 +98,8 @@ public:
// returns pair of refinement constraints for <poison, !poison && value>
virtual std::pair<smt::expr, smt::expr>
- refines(const IR::StateValue &src, const IR::StateValue &tgt) const = 0;
+ refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const = 0;
virtual std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const = 0;
@@ -123,7 +124,8 @@ public:
smt::expr getTypeConstraints() const override;
void fixup(const smt::Model &m) override;
std::pair<smt::expr, smt::expr>
- refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
+ refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -149,7 +151,8 @@ public:
bool isIntType() const override;
smt::expr enforceIntType(unsigned bits = 0) const override;
std::pair<smt::expr, smt::expr>
- refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
+ refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -186,7 +189,8 @@ public:
smt::expr fromBV(smt::expr e) 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;
+ refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -212,7 +216,8 @@ public:
bool isPtrType() const override;
smt::expr enforcePtrType() const override;
std::pair<smt::expr, smt::expr>
- refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
+ refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -252,7 +257,8 @@ public:
smt::expr fromBV(smt::expr e) 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;
+ refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -345,7 +351,8 @@ public:
smt::expr fromBV(smt::expr e) const override;
IR::StateValue fromBV(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
- refines(const IR::StateValue &a, const IR::StateValue &b) const override;
+ refines(State &src_s, State &tgt_s, const StateValue &src,
+ const StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -273,7 +273,7 @@ static void check_refinement(Errors &errs, Transform &t,
expr pre_src = src_state.getPre();
expr pre_tgt = tgt_state.getPre();
- auto [poison_cnstr, value_cnstr] = type.refines(a, b);
+ auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);
expr dom = dom_a && dom_b;
Solver::check({

add pointer refinement