Refactoring to allow for new verification back ends

[JakuJ]

Related to #1321 – this PR aims to abstract away the notion of a verification back end behind an enum, in order to facilitate implementation of new back ends.

Had to make env on viper::Verifier public to do this. I cannot put the call to program.to_viper() in viper since that would be a cyclic dependency to prusti-common, and returning an AstFactory from some method would cause E0502 on call to viper.verify().

[vakaras]

Could you please move all the Java things into Backend::Viper? For example, the construction of the Viper object, build Viper program closure, etc.

[fpoli]

the construction of the Viper object

We just discussed this with Vytautas: it should be enough to store Viper inside an Arc<Lazy<..>> instead of inside Arc<..> as it is now. There us no need to move the local variable somewhere else. See the Lazy documentation.

[fpoli]

If you remove the verification_context: &'v VerificationContext<'t> argument and make it a field of `

enum Backend<'v> {
    Viper { verifier: viper::Verifier<'v>, verification_context: Rc<VerificationContext<'v>> }
}

then making the env field public should no longer be needed. Let us know if this suggestion causes weird lifetime errors.

[fpoli]

etc

The ast_utils.with_local_frame(16, || { .. }) wrapper can be moved too inside the Backend::verify method, so that it's used only for the Viper verifiers.

[JakuJ]

I made it so that the viper object is now initialized lazily, both on the server as well as in the prusti-viper package. Reorganized code around the backend call. Let me know how it looks now.

[vakaras]

Looks good to me.

@fpoli Could you please check that Lazy is used as you intended?

[fpoli]

Lazy is perfect, thanks! The dump disappeared and the log messages need to be updated, then it's good to be merged.

[fpoli]

I rebased on master.

[vakaras]

The CI failure seems to be unrelated to this PR. @fpoli If you agree, please merge.