Skip to content

Commit

Permalink
fix #971 (asm mode): improve ptr2int type punning through loads
Browse files Browse the repository at this point in the history
  • Loading branch information
nunoplopes committed Nov 26, 2023
1 parent 8499328 commit 2a4274c
Show file tree
Hide file tree
Showing 5 changed files with 56 additions and 17 deletions.
30 changes: 13 additions & 17 deletions ir/memory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -297,6 +297,13 @@ expr Byte::isZero() const {
return expr::mkIf(isPtr(), ptr().isNull(), nonptrValue() == 0);
}

expr Byte::forceCastToInt() const {
auto offset = ptrByteoffset().zextOrTrunc(bits_ptr_address);
offset = offset * expr::mkUInt(bits_byte, offset);
auto addr = ptr().getAddress().lshr(offset);
return expr::mkIf(isPtr(), addr.trunc(bits_byte), nonptrValue());
}

expr Byte::refined(const Byte &other) const {
if (eq(other))
return true;
Expand Down Expand Up @@ -361,7 +368,7 @@ ostream& operator<<(ostream &os, const Byte &byte) {
if (byte.isPtr().isTrue()) {
if (byte.ptrNonpoison().isTrue()) {
os << byte.ptr() << ", byte offset=";
byte.ptrByteoffset().printSigned(os);
byte.ptrByteoffset().printUnsigned(os);
} else {
os << "poison";
}
Expand Down Expand Up @@ -530,32 +537,21 @@ static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
assert(!toType.isAggregateType() || isNonPtrVector(toType));
auto bitsize = toType.bits();
assert(divide_up(bitsize, bits_byte) == bytes.size());
bool is_asm = m.getState().getFn().getFnAttrs().has(FnAttrs::Asm);

StateValue val;
bool first = true;
IntType ibyteTy("", bits_byte);

for (auto &b: bytes) {
expr isptr = ub_pre(!b.isPtr());
StateValue v(b.nonptrValue(),
ibyteTy.combine_poison(isptr, b.nonptrNonpoison()));
StateValue v(is_asm ? b.forceCastToInt() : b.nonptrValue(),
is_asm ? !b.isPoison()
: ibyteTy.combine_poison(isptr, b.nonptrNonpoison()));
val = first ? std::move(v) : v.concat(val);
first = false;
}
val = toType.fromInt(val.trunc(bitsize, toType.np_bits(true)));

// allow ptr->int type punning in Assembly mode
if (bitsize == bits_program_pointer &&
has_null_block && // a ptr load in src sets this to true
does_ptr_mem_access &&
m.getState().getFn().getFnAttrs().has(FnAttrs::Asm)) {
StateValue ptr_val = bytesToValue(m, bytes, PtrType(0));
ptr_val.value = Pointer(m, ptr_val.value).getAddress();
expr is_ptr = bytes[0].isPtr();
val = StateValue::mkIf(is_ptr, ptr_val.subst(is_ptr, true),
val.subst(is_ptr, false)).simplify();
}
return val;
return toType.fromInt(val.trunc(bitsize, toType.np_bits(true)));
}
}

Expand Down
1 change: 1 addition & 0 deletions ir/memory.h
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ class Byte {
smt::expr nonptrValue() const;
smt::expr isPoison() const;
smt::expr isZero() const; // zero or null
smt::expr forceCastToInt() const;

smt::expr&& operator()() && { return std::move(p); }

Expand Down
15 changes: 15 additions & 0 deletions tests/alive-tv/asm/load-ptr2int-be.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
; TEST-ARGS: -tgt-is-asm

target datalayout = "E"

define i8 @src(ptr %p) {
%q = load ptr, ptr %p
load i8, ptr %q, align 512
ret i8 0
}

define i8 @tgt(ptr %p) {
%p2 = getelementptr i8, ptr %p, i32 7
%v = load i8, ptr %p2
ret i8 %v
}
13 changes: 13 additions & 0 deletions tests/alive-tv/asm/load-ptr2int.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
; TEST-ARGS: -tgt-is-asm

define i8 @src(ptr %p) {
%q = load ptr, ptr %p
load i8, ptr %q, align 512
ret i8 0
}

define i8 @tgt(ptr %p) {
%p2 = getelementptr i8, ptr %p, i32 0
%v = load i8, ptr %p2
ret i8 %v
}
14 changes: 14 additions & 0 deletions tests/alive-tv/asm/load-ptr2int2.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
define i8 @src(ptr %p) {
%v = load i8, ptr %p
ret i8 %v
}

define i8 @tgt(ptr %p) {
%v = load i8, ptr %p
%c = icmp eq i8 %v, 0
br i1 %c, label %then, label %else
then:
ret i8 0
else:
ret i8 %v
}

0 comments on commit 2a4274c

Please sign in to comment.