Validation fails on Ubuntu 20.04

[ya0guang]

Issue

Generally speaking, MIRAI cannot work well on Ubuntu 20.04. It cannot verify for some programs. So I tried to run validate.sh and it failed on the integration test. I was thinking it's because of my environment is not clean enough, so I also tried to use it in docker (ubuntu:latest) and it also failed.

Steps to Reproduce

1. Start a container of ubuntu:latest and run necessary components like pkg-config, z3, openssl and clang

2. Insatll MIRAI following the steps documented in documentation/linux.md

3. Run validate.sh

Expected Behavior

exit without error

Actual Results

error: test failed, to rerun pass '-p mirai --test integration_tests'

Caused by:
  process didn't exit successfully: `/home/v_chenhongbo04/MIRAI/target/debug/deps/integration_tests-a0b61660615a641b` (signal: 11, SIGSEGV: invalid memory reference)

Environment

rustc 1.60.0-nightly (bfe156467 2022-01-22)

[ya0guang]

Update:

I can run MIRAI successfully on MacOS. I guess MIRAI itself works but some dependency cause the problem.

[hermanventer]

MIRAI runs on Ubuntu (20.04.3 LTS) for every PR (see https://github.com/facebookexperimental/MIRAI/blob/main/.github/workflows/rust.yml).

The relevant action installs Z3 via sudo apt-get install libz3-dev, which installs 4.8.7-4build1.

This seems to be in line with https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Linux.md,
so it would interesting to find out what the problem is.

If you are running on a small container, it could be an out of memory condition. Alternatively, if the core count is small and the cores run slowly, it could be a time-out problem.

In general, it is good idea to do static analysis using the beefiest machine you can lay your hands on.

[ya0guang]

Thanks for your response! I just checked the CI and it seems validate.sh is not executed explicitly in the workflow. So I spent some time to make a reproducible snippet in container.

I'm using ubuntu:20.04 docker image and I just tried again to reproduce this error. This is what I've done for installing MIRAI and run the test script:

# start container
docker run -it ubuntu:20.04
# dependencies
apt update && apt install git libz3-dev curl gcc pkg-config libssl-dev clang -y
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
source $HOME/.cargo/env
# MIRAI
git clone https://github.com/facebookexperimental/MIRAI.git
cd MIRAI
./setup.sh
cargo install  --path ./checker
./validate.sh

Error message:

error: test failed, to rerun pass '-p mirai --test integration_tests'

Caused by:
  process didn't exit successfully: `/MIRAI/target/debug/deps/integration_tests-8e64ebb5ee31264b` (signal: 11, SIGSEGV: invalid memory reference)

real    0m4.836s
user    1m36.167s
sys     0m19.887s

I'm running on a server so I guess it's not likely because of memory, since the same error also occurs on the host machine. Please let me know if there is some unexpected steps or additional information is needed!

[hermanventer]

I can run your test script on my MacBook, see the paste: https://pastebin.com/iJP8D7Jx

My guess is that this is a resource limitation error that causes Z3 to to crash.

[ya0guang]

Thanks for updating me. I think you encountered the same failure as me. If you'd like to explain more details about this error maybe I can also provide some help to fix this!

[hermanventer]

I did not encounter any failures. If you can investigate some more on your side it may help resolve the issue.

[ya0guang]

Sorry for the misunderstanding. I double checked your paste and yes I didn't find an error occurrence. I also tried it on my Mac and the error occurred again. My paste is here: https://pastebin.com/81VL7mLX

I'm comparing yours and mine and trying to see if there is anything strange.

BTW my MacBook is of 16G RAM. May I know what's yours? I want to try if it's because of lack of memory since I also filed on a server with huge RAM.

[ya0guang]

Update:

It seems the error is because of limited resource. I re-execute the validate script on my Mac without using a container, it prints:

running 1 test
Unexpected error: "The analysis of this function timed out". Expected: [] (at MultiSpan { primary_spans: [tests/run-pass/vecdeque_drain.rs:14:24: 14:46 (#0)], span_labels: [] })
error: test failed: tests/run-pass/vecdeque_drain.rs

error: aborting due to previous error

test run_pass has been running for over 60 seconds
Unexpected error: "The analysis of this function timed out". Expected: [] (at MultiSpan { primary_spans: [tests/run-pass/vecdeque_pop_front.rs:21:1: 21:2 (#0)], span_labels: [] })
error: test failed: tests/run-pass/vecdeque_pop_front.rs

error: aborting due to previous error

test run_pass ... FAILED

failures:

---- run_pass stdout ----
resolving ../target/debug/deps/libmirai_annotations-fceb8359d1c48f91.rlib
resolving ../target/debug/deps/libcontracts-c1dfb5d1267e4b0e.dylib
tests/run-pass/vecdeque_drain.rs failed
tests/run-pass/vecdeque_pop_front.rs failed
thread 'run_pass' panicked at 'assertion failed: `(left == right)`
  left: `2`,
 right: `0`', checker/tests/integration_tests.rs:64:5
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace


failures:
    run_pass

test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out; finished in 68.11s

error: test failed, to rerun pass '-p mirai --test integration_tests'

[hermanventer]

The two tests that time out do quite a lot of work. If you are running then on a smaller, slower machine, it is not surprising that it will time out. Time-outs can also happen when Z3 diverges, which could be a versioning issue. I observed that tests that timed out in the past started working after updating Z3.

[ya0guang]

Thank you for the explanation!

[ya0guang]

The errors still exists on the latest commit. So I would reopen this issue. Manually install Z3 may solve this issue.

[hermanventer]

I'm seeing tests failing on my mac book, which has 32 GB of RAM, whereas they all pass on the CI machines, which only have 20 GB. Closing apps on my local machine to free up memory reduces the failing tests, but three of them still fail. The version of Z3 that I use does not seem to matter. And since things used to work just fine on my machine (without any changes to MIRAI or Z3), I suspect that this may be due to an OS update. The CI machines still run on version 11.6.4 (my machine is 12.3).

Fixing this by optimizing MIRAI will take time and effort. Meanwhile, I'll disable the tests that fail for me so that my local environment stays sane.