AliveToolkit / alive2

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

Errors about unsupported instruction `invoke` #1026

Closed HKalbasi closed 6 months ago

HKalbasi commented 6 months ago

Hi. I'm trying to play with alive2 by running alive-tv on two versions of llvm-ir generated by cargo rustc -- --emit=llvm-ir by modifying the source manually, and I'm getting these errors:

ERROR: Unsupported metadata: 40
ERROR: Could not translate '_ZN3std10sys_common9backtrace28__rust_begin_short_backtrace17h169359a4ffe8a86cE' to Alive IR
ERROR: Unsupported instruction:   %8 = invoke i8 @_ZN4core3ops8function6FnOnce9call_once17h2c0ee2eefb117f8eE(ptr
ERROR: Could not translate '_ZN4core3cmp6min_by17h26626f8feca9c1d6E' to Alive IR
ERROR: Unsupported instruction:   %_0 = invoke i32 @"_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h7646
ERROR: Could not translate '_ZN4core3ops8function6FnOnce9call_once17h1189e0850fa2887eE' to Alive IR
ERROR: Unsupported attribute: sret({ { ptr, i64 }, { ptr, i64 } })
ERROR: Could not translate '_ZN4core5slice29_$LT$impl$u20$$u5b$T$u5d$$GT$12split_at_mut17h6cf71fe476a818fdE' to Alive IR
ERROR: Unsupported instruction:   %_55 = invoke i64 @"_ZN49_$LT$usize$u20$as$u20$core..iter..range..Step$GT$17fo
ERROR: Could not translate '_ZN4core5slice4sort11insert_head17h884dbbef3143b0b8E' to Alive IR
ERROR: Unsupported instruction:   %26 = invoke { i64, i64 } @"_ZN89_$LT$core..ops..range..Range$LT$T$GT$$u20$as$
ERROR: Could not translate '_ZN4core5slice4sort11insert_tail17h6b9cc55d36d4a875E' to Alive IR
ERROR: Unsupported instruction:   %_25 = invoke zeroext i1 @_ZN4core3ops8function5FnMut8call_mut17h03226717e3759
ERROR: Could not translate '_ZN4core5slice4sort15partition_equal17h6bbfba7220be56b9E' to Alive IR
ERROR: Unsupported instruction:   %_236 = invoke i64 @"_ZN49_$LT$usize$u20$as$u20$core..iter..range..Step$GT$17f
ERROR: Could not translate '_ZN4core5slice4sort19partition_in_blocks17hd2a0b1ffc237bdd8E' to Alive IR
ERROR: Unsupported instruction:   %17 = invoke { i64, i64 } @"_ZN89_$LT$core..ops..range..Range$LT$T$GT$$u20$as$
ERROR: Could not translate '_ZN4core5slice4sort8heapsort17ha4c57e82bb98be52E' to Alive IR
ERROR: Unsupported instruction:   %_24 = invoke zeroext i1 @_ZN4core3ops8function5FnMut8call_mut17h03226717e3759
ERROR: Could not translate '_ZN4core5slice4sort9partition17h58a9e2f74cd61b76E' to Alive IR
ERROR: Unsupported instruction:   invoke void @_ZN4core5slice4sort7recurse17h1409c5ce0c1c98c8E(ptr align 4 %v.0,
ERROR: Could not translate '_ZN4core5slice4sort9quicksort17hb7a09077856c72c8E' to Alive IR
ERROR: Unsupported instruction:   %2 = load volatile i8, ptr @__rustc_debug_gdb_scripts_section__, align 1
ERROR: Could not translate 'main' to Alive IR

Most of them are complaining about Unsupported instruction: %x = invoke except the ERROR: Unsupported metadata: 40 and ERROR: Unsupported instruction: %2 = load volatile ones. I have no experience with alive2 and llvm-ir, so I'm probably doing something wrong. Any guidance on how to address these issues would be greatly appreciated.

nunoplopes commented 6 months ago

You are doing nothing wrong. 'invoke' and 'volatile' aren't supported currently. There's no ETA to implement them, sorry.

HKalbasi commented 6 months ago

Thanks for quick response! Is there any way to work around these issues? For example by replacing them with instructions with similar semantics?

nunoplopes commented 6 months ago

Not really. If it was that simple we would have already implemented them :)

volatile load/stores can be replaced with a function call. invoke can also be replaced with a function call. But you are going to miss bugs potentially. But maybe it's better than nothing?

HKalbasi commented 5 months ago

Yes I want exactly this (supporting this at cost of missing bugs potentially). I will try to implement it and see how it goes. Thank you!