make -disable-poison-input also make initial memory non-poisonous
useful for verification of isel
MODIFY
ir/memory.cpp
ir/memory.cpp
#include "ir/value.h"
#include "smt/solver.h"
#include "util/compiler.h"
+#include "util/config.h"
#include <array>
#include <numeric>
#include <string>
@@ -1047,12 +1048,22 @@ static expr mk_liveness_array() {
}
void Memory::mkNonlocalValAxioms(bool skip_consts) {
- if (!does_ptr_mem_access)
- return;
-
expr offset
= expr::mkFreshVar("#off", expr::mkUInt(0, Pointer::bitsShortOffset()));
+ // Users may request the initial memory to be non-poisonous
+ if (config::disable_poison_input && state->isSource()) {
+ for (auto &block : non_local_block_val) {
+ if (isInitialMemBlock(block.val))
+ state->addAxiom(
+ expr::mkForAll({ offset },
+ !Byte(*this, block.val.load(offset)).isPoison()));
+ }
+ }
+
+ if (!does_ptr_mem_access)
+ return;
+
for (unsigned i = has_null_block + skip_consts * num_consts_src,
e = numNonlocals(); i != e; ++i) {
Byte byte(*this, non_local_block_val[i].val.load(offset));

ADD
tests/alive-tv/memory/nonpoisoninit.srctgt.ll
+; TEST-ARGS: -disable-poison-input
+
+define i8 @src(ptr %p) {
+ %v = load i8, ptr %p
+ ret i8 0
+}
+
+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 0
+}
+

make -disable-poison-input also make initial memory non-poisonous
useful for verification of isel