AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
719 stars 93 forks source link

Add support for getelementptr nusw and nuw flags (WIP) #1047

Closed nikic closed 1 month ago

nikic commented 1 month ago

I'm struggling to make this actually work, test 4 and 5 currently fail. The problem is that for these flags we can't just require no overflow on the offset, we need to consider the address. However, the offset is one bit smaller than the offset, so we don't get the correct overflow properties. Some advice would be welcome.

nunoplopes commented 1 month ago

I think this test case is not correct:

define ptr @src4(ptr %x, i8 %i, i8 %j) {
  %p = gep nuw ptr %x, 1 x i8 %i, 1 x i8 %j
  ret ptr %p
}
=>
define ptr @tgt4(ptr %x, i8 %i, i8 %j) {
  %i.j = add nuw i8 %i, %j
  %p = gep nuw ptr %x, 1 x i8 %i.j
  ret ptr %p
}

Say that %i nd %j are two large positive numbers (e.g. 0x7f).Adding then produces a negative number. Sine gep indexes are sign extended, tgt will add a very large number, while src added two small numbers. nuw with gep is probably only useful when indexes have the same bitwidth as pointers (alive says the transformation is correct with i64 fwiw).

nikic commented 1 month ago

@nunoplopes The test case uses a p:8:8 data layout, so i8 is the full pointer index size. I agree it would not be correct if the type doesn't match the pointer index size.

nunoplopes commented 1 month ago

@nunoplopes The test case uses a p:8:8 data layout, so i8 is the full pointer index size. I agree it would not be correct if the type doesn't match the pointer index size.

Ups, I missed that bit. I was forcing the pointer size.

nunoplopes commented 1 month ago

There you go:

diff --git a/tools/transform.cpp b/tools/transform.cpp
index 59d58571..ace87307 100644
--- a/tools/transform.cpp
+++ b/tools/transform.cpp
@@ -1215,7 +1215,8 @@ static void calculateAndInitConstants(Transform &t) {
   // as an (unsound) optimization, we fix the first bit of the addr for
   // local/non-local if both exist (to reduce axiom fml size)
   bool has_local_bit = (num_locals_src || num_locals_tgt) && num_nonlocals;
-  bits_ptr_address = min(max(bits_size_t, bits_ptr_address) + has_local_bit,
+  bits_ptr_address = min(max(max(bits_for_offset, bits_size_t),
+                             bits_ptr_address) + has_local_bit,
                          bits_program_pointer);

   if (config::tgt_is_asm)
nikic commented 1 month ago

Thanks! With that, I think I have a working implementation now.

nunoplopes commented 1 month ago

thank you! 🙏