Cache verification of unchanged methods

[JonasAlaif]

This caching will be implemented at the VerificationRequest level

[JonasAlaif]

With the above changes the Hash of repeated VerificationRequests should always be the same... except for the fact that the fold-unfold "algorithm" is not deterministic, thus some of those statements may be reordered depending on whether it's in a good mood or not.

[fpoli]

With the above changes the Hash of repeated VerificationRequests should always be the same... except for the fact that the fold-unfold "algorithm" is not deterministic, thus some of those statements may be reordered depending on whether it's in a good mood or not.

Bummer. You could try sorting the reqs at the beginning of the fn obtain_all(&mut self, reqs: Vec<Perm>) -> ... function to make that more stable.

[vakaras]

Have you checked whether this does not lead to strange name conflicts in encoded programs that are insanely hard to understand on the source level?

[vakaras]

It would be great to have a bunch of tests that check this.

[JonasAlaif]

I think that might be possible; I'll take a look at creating some test cases for this. However, in general I think this is very hard to avoid with deterministic names - one could just look at the generated Viper code and name another local variable in a way which clashes. The two solutions to avoid this that I see: (A) use hash of the HIR/MIR of the function as a sort of 'spec_id' which could be used in these cases (then if another variable is defined after the fact, this hash will change) or (B) look at all defined variables in scope and pick a name that doesn't clash.

[vakaras]

(B) look at all defined variables in scope and pick a name that doesn't clash.

We could do this when lowering to vir_legacy – at that point, we have all variable names present.

[fpoli]

one could just look at the generated Viper code and name another local variable in a way which clashes

Would that still be possible if we add a prefix quantified_ (or just q_) to all quantified variables?

Even with that, as Vytautas asked I wonder what happens to the encoding of forall x: u32 :: forall x: i32 :: .... Will the Viper names clash?

[Aurel300]

In my WIP branch, quantifier variables are named with format!("_{}_quant_{}", arg_idx, body_def_id.index.index()), where arg_idx is the position in the quantifier's arguments and body_def_id is the DefId of the closure containing the quantifier body. It is a local DefId, so index is the only number we use here.

[JonasAlaif]

@Aurel300 Hmm, but using the DefId is problematic in this case since it won't be stable if other stuff in the file/crate is added/deleted. I'm not exactly sure what position in quantifiers args (arg_idx) means (do you mean that for a forall(|a: i32, b: i32| forall(|c: i32| ...)), then a is 1, b is 2, c is 1?), but could we not use only this, with also a quantifier_nesting_count in the name as well?

[Aurel300]

Yes, it wasn't chosen with caching in mind, and it is still better than the original approach of random UUIDs. A nesting count would work, but I'm not sure it would be easy to introduce? When encoding specifications into Viper expressions we would generally work inside out, so it's hard for the inner forall to know its nesting depth.

[JonasAlaif]

The current vars.pre_id seems to do this now though (at least from looking at the generated Viper), I'm not sure how it's implemented but maybe if we just copied the ideas from that?

[Aurel300]

I thought vars.pre_id corresponded to another specification UUID? Maybe it's being interned somewhere?

[Pointerbender]

I have one small additional feature request for the caching of the verification, if time allows :) Would it be possible to introduce a new Prusti configuration flag that allows to disable the caching for a certain run? The use case for me is that I'm currently trying to tweak the performance of some parts in Prusti, but if the benchmark I'm trying to run is in the cache, then I won't be able to see the actual performance difference 😄 I could also add the configuration flag myself in a separate PR, if that is more convenient :) Thanks!

[JonasAlaif]

@Pointerbender good suggestion, I'll add such a flag.

[fpoli]

Can't wait to use the verification cache on CI :)

[JonasAlaif]

Caching should work quite nicely now.

Saving to disk is done by implementing a destructor here:

prusti-dev/viper/src/verification_result.rs

Lines 129 to 139 in 0eea62c

	impl Drop for CacheData {
	fn drop(&mut self) {
	// Save cache to disk, if changed
	if self.updated {
	let mut save_dir = PathBuf::from(&self.load_loc);
	save_dir.pop();
	fs::create_dir_all(&save_dir).ok();
	self.save_cache(&self.load_loc).ok();
	}
	}
	}

I'm not sure how well that interacts with the Prusti server and IDE plugin?
The test I added still fails in some cases I think.

Error reporting seems to work out of the box with cached results.

I'm going on holiday for two weeks from tomorrow so won't be able to finish merging before I'm back, but I'd be happy to let someone else take over - most of the work should be done (and this branch can be used if needed just fine) and I'll be online if needed.

[JonasAlaif]

The CI is now failing on #827

[fpoli]

The reason the cache is not saved when sending a SIGINT to the server is probably that prusti-server abruptly kills the child server process. Sending Signal::SIGINT should be better.

prusti-dev/prusti-launch/src/lib.rs

Line 207 in be28ed5

killpg(getpgrp(), Signal::SIGKILL).expect("Error killing process tree.");

If we do so, we should also remove the "/F" argument on Windows:

prusti-dev/prusti-launch/src/lib.rs

Line 218 in be28ed5

.args(&["/PID", pid, "/T", "/F"])

(A related issue is #754)

[JonasAlaif]

I tried replacing the SIGKILL with a SIGINT but this doesn't help. I'm pretty sure that killing the process like this doesn't call Rust destructors at all - the only reason caching was working for me is that I was running Prusti without the server (as is the default) and then things are destructed properly. It seems that there are two options:

• Catch SIGINT/SIGTERM in prusti-server and save the cache at that point
• Add the POST /save to prusti-server which should be called before quitting

I've implemented the latter for now as it was easier, but we may want to consider switching in the future (the advantage would be when running prusti-server from the command line rather than IDE)

[tillarnold]

The caching appears to also affect the automatic benchmarks (especially the speedup for Knights_tour.rs is very impressive). Would it maybe be a good idea to set the disable_cache flag for the benchmarks to get more representative results?

[vakaras]

The caching appears to also affect the automatic benchmarks (especially the speedup for Knights_tour.rs is very impressive). Would it maybe be a good idea to set the disable_cache flag for the benchmarks to get more representative results?

Thank you, @tillarnold, for noticing this. @JonasAlaif Could you please fix this?