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 4b055b7 and 5484ca7.
• 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?

[fpoli]

Could you move this script into the scripts folder?

[fpoli]

What is the use case of this new PRUSTI_NATIVE_VERIFIER?

[JakuJ]

Grouping all required flags into one, to facilitate switching between the backends. Alternatively I could check if viper_backend == "Lithium".

Why an environment variable? For some reason if I do

if settings.get_bool("native_verifier").unwrap_or(false) {
   ...
}

at the end (after the -P arguments) and provide it via cargo-prusti -- -Pnative_verifier=true it breaks everything, including the building of prusti-contracts 🤨

[fpoli]

There are various reasons why I'd suggest to undo this change and look for another solution:

• The native_verifier and viper_backend flags are partially overlapping.
• The code checks the environment variable PRUSTI_NATIVE_VERIFIER, but does not work if the same flag is set via -P. This goes against the current design of the configuration flags.
• Changing the default of some flags depending on the value of some flags looks like the kind of thing that easily leads to surprises and hard-to-debug issues. We were forced to do it in one case (DEFAULT_PRUSTI_*) because of the way cargo works, but in this PR I think that we have more freedom to choose a better solution.

If Lithium requires a specific set of flags, what about just implementing runtime checks like we do here? Moreover, if a set of tests require a long combination of flags, what about adding one entry here, with a new test folder such as prusti-tests/tests/verify_lithium?