search

jetafese / btor2mlir

Bᴛᴏʀ2MLIR: A Format and Toolchain for Hardware Verification
9 stars 4 forks source link

btor2mlir-opt assertion failed with Btor2 circuits containing array #28

Closed Po-Chun-Chien closed 4 months ago

Po-Chun-Chien commented 5 months ago

(follow up https://github.com/agurfinkel/btor2mlir/issues/40)

I ran the below steps (using the commands from get_cex_seahorn.sh) to translate the Btor2 circuit array_swap.btor2 (obtained from HWMCC 2020 benchmark set) to the Btor2 dialect of LLVM. A docker image built from commit 3456250 was used.

  1. btor2mlir-translate --import-btor array_swap.btor2 >array_swap.mlir
  2. btor2mlir-opt --convert-btornd-to-llvm --convert-btor-to-vector --convert-arith-to-llvm --convert-std-to-llvm --convert-btor-to-llvm --convert-vector-to-llvm array_swap.mlir >array_swap.mlir.opt

The 2nd step failed with the following messages:

Converting array type to mem cell
btor2mlir-opt: /opt/btor2mlir/lib/Conversion/BtorToVector/BtorToVector.cpp:144: virtual mlir::LogicalResult (anonymous namespace)::WriteOpLowering::matchAndRewrite(mlir::btor::WriteOp, mlir::ConvertOpToLLVMPattern<mlir::btor::WriteOp>::OpAdaptor, mlir::ConversionPatternRewriter &) const: Assertion `writeOp.use_empty() && "include the liveness analysis pass"' failed.
PLEASE submit a bug report to https://github.com/llvm/llvm-project/issues/ and include the crash backtrace.
Stack dump:
0.  Program arguments: btor2mlir-opt --convert-btornd-to-llvm --convert-btor-to-vector --convert-arith-to-llvm --convert-std-to-llvm --convert-btor-to-llvm --convert-vector-to-llvm array_swap.mlir
Stack dump without symbol names (ensure you have llvm-symbolizer in your PATH or set the environment var `LLVM_SYMBOLIZER_PATH` to point to it):
/usr/lib/llvm-14/lib/libLLVM-14.so.1(_ZN4llvm3sys15PrintStackTraceERNS_11raw_ostreamEi+0x31)[0x7f24da4c0d01]
/usr/lib/llvm-14/lib/libLLVM-14.so.1(_ZN4llvm3sys17RunSignalHandlersEv+0xee)[0x7f24da4bea3e]
/usr/lib/llvm-14/lib/libLLVM-14.so.1(+0xe40236)[0x7f24da4c1236]
/lib/x86_64-linux-gnu/libc.so.6(+0x42520)[0x7f24d9164520]
/lib/x86_64-linux-gnu/libc.so.6(pthread_kill+0x12c)[0x7f24d91b8a7c]
/lib/x86_64-linux-gnu/libc.so.6(raise+0x16)[0x7f24d9164476]
/lib/x86_64-linux-gnu/libc.so.6(abort+0xd3)[0x7f24d914a7f3]
/lib/x86_64-linux-gnu/libc.so.6(+0x2871b)[0x7f24d914a71b]
/lib/x86_64-linux-gnu/libc.so.6(+0x39e96)[0x7f24d915be96]
btor2mlir-opt(+0xee70a0)[0x562e6957b0a0]
btor2mlir-opt(+0xee6fbb)[0x562e6957afbb]
btor2mlir-opt(+0xf61910)[0x562e695f5910]
btor2mlir-opt(+0xf9e814)[0x562e69632814]
btor2mlir-opt(+0xf6ba57)[0x562e695ffa57]
btor2mlir-opt(+0xf64dd4)[0x562e695f8dd4]
btor2mlir-opt(+0xf68474)[0x562e695fc474]
btor2mlir-opt(+0xef2436)[0x562e69586436]
btor2mlir-opt(+0xfa2d8e)[0x562e69636d8e]
btor2mlir-opt(+0xfa5a88)[0x562e69639a88]
btor2mlir-opt(+0xf06ced)[0x562e6959aced]
btor2mlir-opt(+0xf04e49)[0x562e69598e49]
btor2mlir-opt(+0xf04b06)[0x562e69598b06]
btor2mlir-opt(+0xf056e4)[0x562e695996e4]
btor2mlir-opt(+0x42f46c)[0x562e68ac346c]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90)[0x7f24d914bd90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80)[0x7f24d914be40]
btor2mlir-opt(+0x42f2e5)[0x562e68ac32e5]
Aborted (core dumped)

I've also tried several different Btor2 tasks with array, they all failed with a similar error message.

jetafese commented 5 months ago

For handling btor2 arrays, you will need to use the array passes. The readme will be updated soon but here's the recommended passes to get you on your way:

btor2mlir-opt --btor-liveness --convert-btornd-to-llvm --convert-btor-to-memref --convert-memref-to-llvm --convert-arith-to-llvm --convert-btor-to-llvm --convert-std-to-llvm --convert-vector-to-llvm --resolve-casts file.mlir

Here is the breakdown: --btor-liveness: this pass will run our transformation from immutable to mutable writes based on a liveness analysis --convert-btornd-to-llvm: takes care of our non-deterministically assigned states and inputs --convert-btor-to-memref --convert-memref-to-llvm: converts arrays to their llvm equivalents the rest of the passes are what you are familiar with from the bitvector cases

Hope this helps!

Po-Chun-Chien commented 4 months ago

Hi, sorry for the late reply. I was caught up in other things.

With the additional command-line flags, I was able to translate array_swap.btor2 into LLVM-IR.

However, I also encounter different problems with other Btor2 circuits.

The following were obtained from Btor2MLIR at commit 2e06dec3. (I could not build the latest commit 45f1751e due to /opt/btor2mlir/prevail does not contain a CMakeLists.txt file)

Converting mann-2019/safe_linked_list_fifo_n2d4.{btor2 => mlir} ...
Running 'btor2mlir-translate --import-btor /benchmarks/array/btor2/mann-2019/safe_linked_list_fifo_n2d4.btor2 >/benchmarks/array/mlir/mann-2019/safe_linked_list_fifo_n2d4.mlir'
Converting mann-2019/safe_linked_list_fifo_n2d4.{mlir => mlir.opt} ...
Running 'btor2mlir-opt --btor-liveness --convert-btornd-to-llvm --convert-btor-to-memref --convert-memref-to-llvm --convert-arith-to-llvm --convert-btor-to-llvm --convert-std-to-llvm --convert-vector-to-llvm --resolve-casts /benchmarks/array/mlir/mann-2019/safe_linked_list_fifo_n2d4.mlir >/benchmarks/array/mlir/mann-2019/safe_linked_list_fifo_n2d4.mlir.opt'
/benchmarks/array/mlir/mann-2019/safe_linked_list_fifo_n2d4.mlir:132:12: error: operand #0 does not dominate this use
    %237 = btor.read %235[%223] : !btor.array<<1>, <2>>, !btor.bv<2>
           ^
/benchmarks/array/mlir/mann-2019/safe_linked_list_fifo_n2d4.mlir:132:12: note: see current operation: %235 = "btor.read"(%275, %223) : (!btor.array<<1>, <2>>, !btor.bv<1>) -> !btor.bv<2>
/benchmarks/array/mlir/mann-2019/safe_linked_list_fifo_n2d4.mlir:128:12: note: operand defined here (op in the same block)
    %233 = btor.write %232, %112[%222] : !btor.array<<1>, <2>>
           ^
Converting wolf-2018A/VexRiscv-regch0-15-p0-array.{btor2 => mlir} ...
Running 'btor2mlir-translate --import-btor /benchmarks/array/btor2/wolf-2018A/VexRiscv-regch0-15-p0-array.btor2 >/benchmarks/array/mlir/wolf-2018A/VexRiscv-regch0-15-p0-array.mlir'
Converting wolf-2018A/VexRiscv-regch0-15-p0-array.{mlir => mlir.opt} ...
Running 'btor2mlir-opt --btor-liveness --convert-btornd-to-llvm --convert-btor-to-memref --convert-memref-to-llvm --convert-arith-to-llvm --convert-btor-to-llvm --convert-std-to-llvm --convert-vector-to-llvm --resolve-casts /benchmarks/array/mlir/wolf-2018A/VexRiscv-regch0-15-p0-array.mlir >/benchmarks/array/mlir/wolf-2018A/VexRiscv-regch0-15-p0-array.mlir.opt'
Converting array type to mem cell
Converting array type to mem cell
/benchmarks/array/mlir/wolf-2018A/VexRiscv-regch0-15-p0-array.mlir:104:12: error: failed to legalize operation 'btor.nd_array' that was explicitly marked illegal
    %100 = btor.nd_array 103 : !btor.array<<5>, <32>>
           ^
/benchmarks/array/mlir/wolf-2018A/VexRiscv-regch0-15-p0-array.mlir:104:12: note: see current operation: %680 = "btor.nd_array"() {id = 103 : ui64} : () -> !btor.array<<5>, <32>>

The following process hangs.

Converting wolf-2019A/picorv32_mutAX_mem-p0.{btor2 => mlir} ...
Running 'btor2mlir-translate --import-btor /benchmarks/array/btor2/wolf-2019A/picorv32_mutAX_mem-p0.btor2 >/benchmarks/array/mlir/wolf-2019A/picorv32_mutAX_mem-p0.mlir'
Converting wolf-2019A/picorv32_mutAX_mem-p0.{mlir => mlir.opt} ...
Running 'btor2mlir-opt --btor-liveness --convert-btornd-to-llvm --convert-btor-to-memref --convert-memref-to-llvm --convert-arith-to-llvm --convert-btor-to-llvm --convert-std-to-llvm --convert-vector-to-llvm --resolve-casts /benchmarks/array/mlir/wolf-2019A/picorv32_mutAX_mem-p0.mlir >/benchmarks/array/mlir/wolf-2019A/picorv32_mutAX_mem-p0.mlir.opt'
Converting array type to mem cell
Converting array type to mem cell
jetafese commented 4 months ago

The commit you are using is the right one for your needs. I have taken a look at your examples and here are some ways forward:

  1. I was not able to find the linked list problem in the HMCC20 benchmarks. Give me some time to look into why the pipeline is breaking.
  2. For this case, since the array is quite small, you will need to add our handler for small arrays: --convert-btor-to-vector --convert-vector-to-llvm right after --convert-btor-to-memref --convert-memref-to-llvm
  3. The same advice as above goes for the third problem as well.