search

AliveToolkit / alive2

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

Issue that cannot see SMT query. #1036

Closed IamYJLee closed 1 month ago

IamYJLee commented 1 month ago

[ Environments ]

[ Error ]

File: /tmp/z3-20230512-6211-15w19iu/z3-z3-4.12.2/src/ast/converters/model_converter.cpp
Line: 27
Failed to verify: e
4.12.2.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

[ Descriptions ]

I tried to see an SMT query on a verification failure case below, but I received an error and cannot see an SMT query. I would like to know why this error is occurs. Also, is there any resource I can refer to on how to understand the logs when a verification failure occurs?

Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

Example:
ptr nocapture nowrite noundef %.block_descriptor = pointer(non-local, block_id=2, offset=2, attrs=3)

Source:
  >> Jump to %entry
ptr %block.capture.addr = pointer(non-local, block_id=2, offset=34, attrs=3)
ptr %0 = pointer(non-local, block_id=2, offset=18)
ptr %forwarding = pointer(non-local, block_id=2, offset=26)
ptr %1 = pointer(non-local, block_id=7, offset=16)
ptr %value = pointer(non-local, block_id=7, offset=40)
ptr %2 = pointer(non-local, block_id=4, offset=1)
ptr %block.capture.addr1 = pointer(non-local, block_id=2, offset=42, attrs=3)
i32 %3 = #x00000000 (0)
i32 %call = function did not return!

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >   size: 0 align: 4    alloc type: 0   alive: false    address: 0
Block 1 >   size: 5 align: 1    alloc type: 0   alive: true address: 9  const
Block 2 >   size: 46    align: 1    alloc type: 0   alive: false    address: 14
Block 3 >   size: 0 align: 1    alloc type: 0   alive: true address: 1
Block 4 >   size: 0 align: 1    alloc type: 0   alive: true address: 3
Block 5 >   size: 0 align: 1    alloc type: 0   alive: true address: 14
Block 6 >   size: 0 align: 1    alloc type: 0   alive: true address: 2
Block 7 >   size: 53    align: 1    alloc type: 0   alive: true address: 72
Block 8 >   align: 4    alive: true
Block 9 >   size: 4 align: 4    alloc type: 0   alive: true address: 4  const
Block 10 >  size: 4 align: 4    alloc type: 0   alive: true address: 192    const
Block 11 >  size: 4 align: 4    alloc type: 0   alive: true address: 128    const
Block 12 >  size: 4 align: 4    alloc type: 0   alive: true address: 60 const

LOCAL BLOCKS:
Block 16 >  size: 0 align: 4    alloc type: 0   alive: false    address: 0

Target:
  >> Jump to %entry
i32 %0 = #x00000008 (8)
i32 %1 = #x00000000 (0)
i32 %2 = #x00000008 (8)
i32 %3 = #x00000009 (9)
i1 %4 = #x0 (0)
  >> Jump to %originalBB
ptr %block.capture.addr = pointer(non-local, block_id=2, offset=34, attrs=3)
ptr %12 = pointer(non-local, block_id=2, offset=18)
ptr %forwarding = pointer(non-local, block_id=2, offset=26)
ptr %13 = pointer(non-local, block_id=7, offset=16)
ptr %value = pointer(non-local, block_id=7, offset=40)
ptr %14 = poison
ptr %block.capture.addr1 = pointer(non-local, block_id=2, offset=42, attrs=3)
i32 %15 = #x00000000 (0)
i32 %call = function did not return!

TARGET MEMORY STATE
===================
LOCAL BLOCKS:
Block 16 >  size: 0 align: 4    alloc type: 0   alive: false    address: 0
Block 17 >  size: 5 align: 1    alloc type: 0   alive: false    address: 9
nunoplopes commented 1 month ago

Ok, so what happened is that an assertion failed in Z3. Can you try the latest version of Z3 to see if it still happens?

If it does, then try running with -smt-log. That records all interactions with Z3 in a file so we can replicate the issue without Alive2 (running z3 -log file.log should replicate the crash).

IamYJLee commented 1 month ago

Thanks for your advice.

I got a different error, as shown below, when trying with the latest version of Z3 (https://github.com/Z3Prover/z3/releases/tag/z3-4.13.0).

Transformation doesn't verify! (not unsound)
ERROR: SMT Error: unclassified exception
nunoplopes commented 1 month ago

We really need more information in order to debug this. Either send me the input you're giving to alive or the z3 log.

IamYJLee commented 1 month ago

z3_log.txt.zip

Please confirm the log of z3. I tried to running z3 -v:5 -log z3_log.txt and the log is z3_log_log.txt.zip

And i tried to run z3 -v:10000 -log z3_log.txt and can see the message as below. This is probably caused by exceeding resource limits. (in z3 source code)

(tactic-exception "canceled")
max. heap size : 218.646 Mbytes
time : 5848.15
nunoplopes commented 1 month ago

This is what I get when running the log:

nuno@Laptop:~$ z3 -log z3_log.txt
Alive2 36dd875a-dirty
[z3 exception]: expecting object at position 1 but got uint64
[z3 exception]: expecting object at position 1 but got string
[z3 exception]: invalid argument reference
[z3 exception]: invalid argument reference
[z3 exception]: invalid argument reference
[z3 exception]: expecting object at position 1 but got string
[z3 exception]: invalid argument reference
Segmentation fault

Are you running on a 32-bit machine?

IamYJLee commented 1 month ago

No, I am running on a 64-bit machine. Here is the kernel information of my machine.

Darwin YoungJunui-MacBookPro.local 23.4.0 Darwin Kernel Version 23.4.0: Wed Feb 21 21:45:49 PST 2024; root:xnu-10063.101.15~2/RELEASE_ARM64_T6020 arm64

I also confirmed the same error (Segmentation fault). This error occurred while running Z3 version 4.12.2 using a Z3 log that was created with version 4.13.0. However, the Z3 log works correctly when executed with Z3 version 4.13.0.

IamYJLee commented 1 month ago

Attached are the Z3 logs, which were created by their respective versions of Z3. z3_log_4.12.2.txt.zip z3_log_4.13.0.txt.zip

nunoplopes commented 1 month ago

This log is just too big. I left it running for an hour and didn't finish. Please reduce the input (use llvm-reduce or something like that). Also, comment the checks in tools/transforms.cpp and leave just the check that triggers the model validation failure. Without further steps on your side, I'm afraid I can't help; it's just impractical to debug something this big.

nunoplopes commented 1 month ago

So I fixed a small bug in Z3 when printing stats. But the log you provide doesn't trigger the model converter issue. I really need another log to be able to debug this.

IamYJLee commented 1 month ago

Following your guide, I am trying to reduce the size of the log. How is the fixed printing stats problem(https://github.com/Z3Prover/z3/commit/18a95d89c6b16994ff07d31e5059e79b007f6c4e) related to this issue? And I am not sure which version of Z3 I should use. Because the results differ between Z3 v4.12.2 and v4.13.0 when the opt_smt_verbose option is turned off.

On the v4.12.2

Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

On the v4.13.0

Transformation doesn't verify! (not unsound)
ERROR: SMT Error: unclassified exception
nunoplopes commented 1 month ago

Following your guide, I am trying to reduce the size of the log. How is the fixed printing stats problem(Z3Prover/z3@18a95d8) related to this issue?

Replaying your log would crash in debug mode. That's all. But that's a minor issue.

And I am not sure which version of Z3 I should use. Because the results differ between Z3 v4.12.2 and v4.13.0 when the opt_smt_verbose option is turned off.

Ideally the latest from git. The issue you're seeing with the model converter may have been fixed already.

IamYJLee commented 1 month ago

I have confirmed normal operation under the following conditions.

I confirmed that the model converter has already been fixed. Thank you for your advice.