From 4b5b13c23ce5e5fd43a9a1929eeec8d42b8c2ea2 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 13 Dec 2024 09:59:59 +0000 Subject: [PATCH] fix #1144: crash to broken local block count if different in src/tgt --- ir/memory.cpp | 2 -- ir/memory.h | 2 ++ tests/alive-tv/memory/local-blk-count.srctgt.ll | 13 +++++++++++++ 3 files changed, 15 insertions(+), 2 deletions(-) create mode 100644 tests/alive-tv/memory/local-blk-count.srctgt.ll diff --git a/ir/memory.cpp b/ir/memory.cpp index 326e9012f..a41bbc471 100644 --- a/ir/memory.cpp +++ b/ir/memory.cpp @@ -122,7 +122,6 @@ static expr mk_block_if(const expr &cond, expr then, expr els) { } -static unsigned next_local_bid; static unsigned next_const_bid; static unsigned next_global_bid; static unsigned next_ptr_input; @@ -1682,7 +1681,6 @@ void Memory::mkAxioms(const Memory &tgt) const { void Memory::resetGlobals() { next_const_bid = has_null_block; next_global_bid = has_null_block + num_consts_src; - next_local_bid = 0; next_ptr_input = 0; } diff --git a/ir/memory.h b/ir/memory.h index f41857627..9fe18b3f9 100644 --- a/ir/memory.h +++ b/ir/memory.h @@ -154,6 +154,8 @@ class Memory { smt::expr non_local_block_liveness; // BV w/ 1 bit per bid (1 if live) smt::expr local_block_liveness; + unsigned next_local_bid = 0; + // TODO: change from short idx to arg number smt::expr has_stored_arg; // (short idx, short offset) -> bool diff --git a/tests/alive-tv/memory/local-blk-count.srctgt.ll b/tests/alive-tv/memory/local-blk-count.srctgt.ll new file mode 100644 index 000000000..2df899640 --- /dev/null +++ b/tests/alive-tv/memory/local-blk-count.srctgt.ll @@ -0,0 +1,13 @@ +define void @src(ptr %0, i32 %1) { + %3 = call ptr @memrchr(ptr %0, i32 %1, i64 7) + ret void +} + +define void @tgt(ptr %0, i32 %1) { + %stack = call ptr @myalloc() + call ptr @memrchr(ptr %0, i32 %1, i64 7) + ret void +} + +declare ptr @memrchr(ptr, i32, i64) +declare ptr @myalloc() allockind("alloc")