AliveToolkit / alive2

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

Bypass assume_welldefined to handle metadata correctly #1044

Closed dtcxzyw closed 1 month ago

dtcxzyw commented 1 month ago

See the following code: https://github.com/AliveToolkit/alive2/blob/22bc6f2791796708cbcfc99935992145f4ae2800/llvm_util/llvm2alive.cpp#L113-L123

alive2 returns node assume_welldefined instead of the original value when noundef exists. https://github.com/AliveToolkit/alive2/blob/22bc6f2791796708cbcfc99935992145f4ae2800/llvm_util/llvm2alive.cpp#L1754-L1763 However, alive_i will be set to assume_welldefined, which causes type checks to fail when handing metadata of a call. This patch bypasses assume_welldefined to set alive_i to the original value.

Fixes https://github.com/AliveToolkit/alive2/issues/1043.