Inserting runtime checks into MIR based on expiration locations

compiler
1

Hello everyone,

I am currently working on a Rust verifier and am trying to insert runtime checks for specifications into the MIR. For one particular feature of this verifier (called pledges), I have the goal of inserting checks for certain conditions once a specific borrow expires.

We are using the rust compiler interface, and for verification we can identify the locations in mir_promoted where borrows expire and do static analysis, however to check these conditions at runtime I ran into some problems. In particular, to insert these runtime checks I need to override one of the compiler queries such that modifications reach the generated executable, but all the available options I see are problematic.

  • I can not modify mir_promoted since modifications rely on the results of the borrow checker, which requires mir_promoted to be constructed already.
  • I can modify mir_drops_elaborated_and_const_checked, however the locations of expiring borrows identified in mir_promoted are no longer accurate.

Are there any solutions to these problems that do not require forking the rust compiler?

  • for example, if I could invalidate the mir_promoted query at some point after our analysis and cause it to return a modified version that would certainly be a solution but so far I didn't find a way to achieve this
  • Is there maybe some other way of tracking the locations of statements between mir_promoted and mir_drops_elaborated_and_const_checked? Looking at the mir passes that are performed between those two representations I think this is probably not feasible, or only heuristically, but maybe I am missing something?

I would appreciate any insights on this problem enormously!

2

Hey, I'm interested, do you have a Github repository?

3

Yeah sure, thanks a lot! The verifier is Prusti and my current fork is here: link.

I mean you can see my changes to it, but to give some pointers, in prusti/src/callback.rs I override the mir_drops_elaborated.. query and pass some static information to it. The query itself is implemented in prusti/src/mir_modify.rs, currently to execute runtime checks for postconditions, preconditions, pledges (at locations that are usually off by one, which is the problem I have, and I think in theory the locations can even point to the wrong block) and some other checks. Also note that my changes are definitely still very messy!

The repo also contains instructions on how to compile it in case you plan on doing that, but to get executables you will need to set at least this flag:

  • export PRUSTI_FULL_COMPILATION=true, otherwise prusti stops after verification without producing an executable.

I also have a repo containing various examples here. Some examples involving pledges can be found at prusti-exampes/translation/pledges, some of them contain comments when certain checks should be executed.

Prusti also has a Zulip chat and in case you want to reach out there, I should be available very regularly: https://prusti.zulipchat.com/login/.

Thanks a lot for your interest, and I look forward to potential ideas for a solution.

4

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.