fix #1144: crash to broken local block count if different in src/tgt

AliveToolkit · Dec 13, 2024 · 4b5b13c · 4b5b13c
1 parent 323fe76
commit 4b5b13c
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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")