search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
424 stars 91 forks source link

verif_incr should prove that it restores an uninitialized counter #769

Open andrew-appel opened 2 months ago

andrew-appel commented 2 months ago

Let's consider three versions of verif_incr: (1) master branch (VST 2.14), lib/test/verif_incr (2) vst_on_iris branch, progs64/verif_incr (3) vst_on_iris branch, lib/test/verif_incr

Right now, in (1) the proof body_compute2 proves a postcondition in which the counter is recombined from its various split shares. The proof in (2) does not do this, it has a postcondition of simply "main_post" which does not care about the SEP clause.

To port VSTlib to VST 3.0, I copied the body_main proof from (2) into the body_compute proof in (3), but there's an admit at the very end for the recombining of shares. @mansky1 , can you fix this in lib/test/verif_incr?

While you're at it, you could refactor the program and proof in progs64/verif_incr with a compute function as in lib/test/verif_incr. Eventually, we should eliminate the duplication between these two copies of verif_incr.

mansky1 commented 2 months ago

I believe it's fixed now, and I refactored the progs version to more closely match the lib version (I didn't split out main into a separate file, though).