search

AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
766 stars 97 forks source link

Add support for pointers larger than 64 bits #1031

Open FlashSheridan opened 5 months ago

FlashSheridan commented 5 months ago

ir/memory.cpp:199 and tools/transform.cpp:904 assert bits_program_pointer <= 64, the former with a comment:

TODO: support pointers larger than 64 bits.

Changing the assertions for this and non-0 address spaces allowed me to test some of our simple IR, but ran into multiple assertion failures (apparently involving null pointers) on more realistic IR. (Discussion at “Add support for non-0 address spaces #877.”)

Hels15 commented 4 months ago

@FlashSheridan Hi, Could you tell me the current state of this issue? I'm looking for contributing opportunities and would appreciate it if you'd be able to give me an update on this. Thank you.

nunoplopes commented 4 months ago

@Hels15 this is not an easy thing to fix.

FlashSheridan commented 4 months ago

@FlashSheridan Hi, Could you tell me the current state of this issue? I'm looking for contributing opportunities and would appreciate it if you'd be able to give me an update on this. Thank you.

I could send you my logs and notes, plus the internal instructions on our wiki for seeking a small amount of wheat among a huge amount of chaff. I can’t claim to have made any significant progress; excerpt: “Finished analyzing pre-death output from Alive2 on the IR from CpuConstraintPoly.sol [largest Solidity contract in era-compiler-tests]. Only two non-trivial validations,” [among 20,422 files]. I agree that it is not an easy issue.

Hels15 commented 4 months ago

@FlashSheridan Hi, Could you tell me the current state of this issue? I'm looking for contributing opportunities and would appreciate it if you'd be able to give me an update on this. Thank you.

I could send you my logs and notes, plus the internal instructions on our wiki for seeking a small amount of wheat among a huge amount of chaff. I can’t claim to have made any significant progress; excerpt: “Finished analyzing pre-death output from Alive2 on the IR from CpuConstraintPoly.sol [largest Solidity contract in era-compiler-tests]. Only two non-trivial validations,” [among 20,422 files]. I agree that it is not an easy issue.

I would highly appreciate that, although as Nuno pointed out before it is quite unlikely that I can contribute something valuable to this topic, if it's not too much of a business feel free to send me those notes, but don't bother too much of it as I'm afraid it's quite "useless" for me at the time. Thank you.

FlashSheridan commented 4 months ago

I would highly appreciate that, …

A couple of days ago I emailed some extracts from the second version of our wiki, to the address for the organization on your GitHub profile. (I have a “mail me” link on the new URL in my GitHub profile, http://flash-sheridan.name. POBox is killing my old URL for life, http://pobox.com/~flash, this month.)