Skip to content

Commit

Permalink
guardable UB: flag mem access of poison/undef ptrs
Browse files Browse the repository at this point in the history
  • Loading branch information
nunoplopes committed Aug 22, 2023
1 parent 2e57d13 commit 4bd483b
Show file tree
Hide file tree
Showing 4 changed files with 38 additions and 2 deletions.
2 changes: 1 addition & 1 deletion ir/instr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3215,7 +3215,7 @@ StateValue Assume::toSMT(State &s) const {
// assume(ptr)
const auto &vptr = s.getAndAddPoisonUB(*args[0]);
Pointer ptr(s.getMemory(), vptr.value);
s.addUB(!ptr.isNull());
s.addGuardableUB(!ptr.isNull());
break;
}
}
Expand Down
6 changes: 5 additions & 1 deletion ir/state.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -588,7 +588,11 @@ State::getAndAddPoisonUB(const Value &val, bool undef_ub_too,
}

// If val is an aggregate, all elements should be non-poison
addUB(not_poison_except_padding(val.getType(), sv.non_poison));
expr np = not_poison_except_padding(val.getType(), sv.non_poison);
if (ptr_compare)
addGuardableUB(std::move(np));
else
addUB(std::move(np));
}

check_enough_tmp_slots();
Expand Down
16 changes: 16 additions & 0 deletions tests/alive-tv/non-ub-exploitation/nonnull_metadata.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
; TEST-ARGS: -disallow-ub-exploitation
; SKIP-IDENTITY

define i1 @src(ptr %x) {
%y = load ptr, ptr %x, !nonnull !1
%c = icmp eq ptr %y, null
ret i1 %c
}

define i1 @tgt(ptr %x) {
ret i1 false
}

!1 = !{}

; ERROR: Source has guardable UB
16 changes: 16 additions & 0 deletions tests/alive-tv/non-ub-exploitation/range_metadata.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
; TEST-ARGS: -disallow-ub-exploitation
; SKIP-IDENTITY

define i1 @src(ptr %x) {
%y = load i8, ptr %x, !range !1
%c = icmp eq i8 %y, 9
ret i1 %c
}

define i1 @tgt(ptr %x) {
ret i1 false
}

!1 = !{i8 0, i8 5}

; ERROR: Source returns poison

0 comments on commit 4bd483b

Please sign in to comment.