Lithium: a Rust-native back end

[JakuJ]

This is a draft PR outlining the work on a new Rust-native back end for Prusti, developed in connection to my Master's thesis. The aim is to, among others, evaluate the performance benefits of going straight from CFG to SMT-LIB and decoupling from Viper.

The project is in its initial stages and so the code is highly volatile. Everything is subject to change. The purpose of this PR is to give Prusti developers an overview of the work being done in order to avoid double work, conflicts etc.

[fpoli]

Wow, thanks! I'm not sure why the CI is not running. Even if it's a draft, I was wondering if you considered moving native_verifier outside viper, because the API of a Viper and a native one have various differences (e.g. parsing command line parameters, the type of the Program, depending on the JVM...).

[JakuJ]

I think the CI doesn't run because of the merge conflicts. I'll move the code to a separate create as soon as I figure out how to avoid circular dependencies.

[vakaras]

The PR looks like a good start. I think that once it is cleaned up, we should merge it in with a stub native verifier so that we do not need to worry about getting large conflicts.

cc @Aurel300 @JonasAlaif @fpoli

[Aurel300]

We'll probably soon get some merge conflicts in prusti-server since Cedric and Joseph will be finishing the IDE improvements project soon.

[vakaras]

@JakuJ In our meeting, we discussed what would be the best way to proceed and agreed that the work should be split into two PRs:

1. A clean-up PR that prepares code to allow easily adding a new backend. This PR should be merged as soon as possible to avoid conflicts.
2. A PR that implements the actual backend – this PR would be merged only if this project worked out.

The clean-up PR should add VerificationBackend enum to prusti-server that abstracts over Viper and your new backend. We decided that an enum will be a cleaner solution for now than having a Verifier trait, which I suggested before.

enum VerificationBackend {
    Viper(viper::Viper),
//    Lithium(lithium::Lithium), – only added later once the backend is ready
}

impl VerificationBackend {
    pub fn verify(&self, program: vir::Program) -> VerificationResult {
        match self { /* delegate */ }
    }
}

Notice that the verify method takes the VIR program (that is either legacy or low) as input. This means that all JAVA stuff should happen inside the verify method.

[fpoli]

• Use git rebase -i master to remove 4b055b7b4edb49a03141732dc1a64285129b9dcc and 5484ca74c2d742325f4933a61d4c0e20fc5c403c.
• Remove .DS_Store (from the history of the PR, not in a new commit) and add it to .gitignore.

[fpoli]

Is there a clear advantage in splitting backend-common out of viper? All its current content (java exceptions, verification results, silicon counterexamples) can still be seen as part of Viper, and I'd avoid one more top-level folder if it's not necessary.

[JakuJ]

A test or two are still failing, but I'm going to switch from draft mode now. I suppose some quality-of-life improvements are necessary for the general public to find this usable, in particular:

• [ ] Better error handling and error messages
• [ ] A single configuration flag to run the native back end, instead of modifying half the config.rs file

I'll be chipping away at these improvements when I have the time, and in the meantime I would appreciate a code review.

[fpoli]

I notice that the PR runs cargo fmt on prusti-viper, but from the diff it's difficult to see if you made more changes in there. Could you try to reformat prusti-viper on the master branch, opening a single-commit PR that we can immediately merge, and rebasing at the same time this PR on top of that commit?