Skip to content

Commit

Permalink
asm mode: allow refinement of a memory byte with a ptr with an integer
Browse files Browse the repository at this point in the history
Type punning through memory is perfectly fine in asm
  • Loading branch information
nunoplopes committed Dec 5, 2023
1 parent 3e1e364 commit 1352eaa
Show file tree
Hide file tree
Showing 3 changed files with 43 additions and 9 deletions.
36 changes: 27 additions & 9 deletions ir/memory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -274,6 +274,11 @@ expr Byte::nonptrNonpoison() const {
return p.extract(start + bits_poison_per_byte - 1, start);
}

expr Byte::boolNonptrNonpoison() const {
expr np = nonptrNonpoison();
return np == expr::mkInt(-1, np);
}

expr Byte::nonptrValue() const {
if (!does_int_mem_access)
return expr::mkUInt(0, bits_byte);
Expand Down Expand Up @@ -317,9 +322,6 @@ expr Byte::forceCastToInt() const {
}

expr Byte::refined(const Byte &other) const {
if (eq(other))
return true;

// refinement if offset had non-ptr value
expr v1 = nonptrValue();
expr v2 = other.nonptrValue();
Expand Down Expand Up @@ -348,20 +350,36 @@ expr Byte::refined(const Byte &other) const {
}
}

// fast path: if we didn't do any ptr store, then all ptrs in memory were
// already there and don't need checking
expr is_ptr = isPtr();
expr is_ptr2 = other.isPtr();
bool asm_mode = other.m.getState().getFn().has(FnAttrs::Asm);
expr ptr_cnstr;
if (!does_ptr_store || is_ptr.isFalse() || is_ptr2.isFalse()) {

// fast path: if we didn't do any ptr store, then all ptrs in memory were
// already there and don't need checking
if (!does_ptr_store || is_ptr.isFalse() || (!asm_mode && is_ptr2.isFalse())) {
ptr_cnstr = *this == other;
} else {
ptr_cnstr = !ptrNonpoison() ||
// allow ptr -> int type punning in asm mode
expr extra = false;
if (asm_mode) {
extra = !is_ptr2 &&
other.boolNonptrNonpoison() &&
forceCastToInt() == v2;
}
ptr_cnstr = ptrNonpoison().implies(
(other.ptrNonpoison() &&
ptrByteoffset() == other.ptrByteoffset() &&
ptr().refined(other.ptr()));
ptr().refined(other.ptr())) ||
extra);
}
return expr::mkIf(is_ptr == is_ptr2,

expr same_type = is_ptr == is_ptr2;
// allow ptr -> int type punning in asm mode
if (asm_mode)
same_type = is_ptr || !is_ptr2;

return expr::mkIf(same_type,
expr::mkIf(is_ptr, ptr_cnstr, int_cnstr),
// allow null ptr <-> zero
isPoison() ||
Expand Down
1 change: 1 addition & 0 deletions ir/memory.h
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ class Byte {
smt::expr ptrValue() const;
smt::expr ptrByteoffset() const;
smt::expr nonptrNonpoison() const;
smt::expr boolNonptrNonpoison() const;
smt::expr nonptrValue() const;
smt::expr isPoison() const;
smt::expr nonPoison() const;
Expand Down
15 changes: 15 additions & 0 deletions tests/alive-tv/asm/store-ptr.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
; TEST-ARGS: -tgt-is-asm
; SKIP-IDENTITY

@dst = external global i64
@ptr = external global ptr

define void @src() {
store ptr @dst, ptr @ptr, align 8
ret void
}

define void @tgt() {
store i64 ptrtoint (ptr @dst to i64), ptr @ptr, align 8
ret void
}

0 comments on commit 1352eaa

Please sign in to comment.