Skip to content

openssl_aes example proof hangs #1812

Open
@bboston7

Description

@bboston7

The proof in examples/openssl_aes appears to have bit-rotted. I tried running it on Ubuntu 22.04 with the latest what4-solvers solvers, and I used clang-12 to build the bitcode. The proof ran for a few hours before the kernel killed ABC on a machine with 24GB of RAM. SAW-0.9 has the same problem, so this doesn't appear to be a new issue. I'm not sure when the proof broke, or what caused the breakage (off the top of my head, it could be SAW changes, Clang changes, or ABC changes). I also tried changing the proof to use Z3 instead, but it still hung for a few hours before I called it "unlikely to terminate" and killed SAW.

To reproduce the problem, run make in examples/openssl_aes. This will build the bitcode and run the SAW proof.

Metadata

Metadata

Assignees

No one assigned

    Labels

    performanceIssues that involve or include performance problemsregressionSomething that used to work, but now doesn'ttooling: CIIssues involving CI/CD scripts or processestype: bugIssues reporting bugs or unexpected/unwanted behavior

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions