Improve memory efficiency by deleting Z3_context on drop of Z3Solver

[davidsemakula]

Description

Fixes some OOM (Out of Memory) issues when analyzing crates with a lot of entry points and/or deep call graphs causing errors of the form

error: could not compile `...`

Caused by:
  process didn't exit successfully: `...`

Fixes # (issue)

These issues from the old repo are likely related/fixed:
facebookexperimental/MIRAI#1241
facebookexperimental/MIRAI#1257

Type of change

• Bug fix (non-breaking change which fixes an issue)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to not work as expected)
• API change with a documentation update
• Additional test coverage
• Code cleanup or just keeping up with the latest Rustc nightly

How Has This Been Tested?

This has been tested by running MIRAI's integration tests with the memory limit for Z3 set to 1 GB.
With the memory limit set, the test suite succeeds with this patch applied, while it exits unsuccessfully (with a SIGSEGV exit code on macOS) without this patch.

Integration tests where run with:

./install_mirai.sh
CARGO_INCREMENTAL="0" RUSTFLAGS="-Zprofile -Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests" cargo test --all -- --test-threads=1

One way to set the Z3 memory limit is to use the code snippet below in Z3Solver::new

let memory_max_size = CString::new("memory_max_size").unwrap().into_raw();
let mb = CString::new("1024").unwrap().into_raw();
z3_sys::Z3_global_param_set(memory_max_size, mb);

In some cases I've tested, this solves OOM issues for some analyses where memory usage exploded to as much as 32 GB, while the same analysis can complete with a memory limit as low as 512 MB with this patch applied (with 1 GB being sufficient typically).

Checklist:

• Fork the repo and create your branch from main.
• If you've added code that should be tested, add tests.
• If you've changed APIs, update the documentation.
• Ensure the test suite passes.
• Make sure your code lints.

[hermanventer]

Thanks, this looks good. I'll merge it once I've figured out how to fix the CI failures.

[davidsemakula]

Looks like they're due to a cargo_metadata update, I'm gonna add a commit that tries to fix it

[davidsemakula]

@hermanventer I've added CI fixes