princetonuniversity/vst

Verified Software Toolchain

with contributions from

Andrew W. Appel, Lennart Beringer, Robert Dockins, Josiah Dodds, Aquinas Hobor, Jean-Marie Madiot, Gordon Stewart, Qinxiang Cao, Qinshi Wang, and others.

The LICENSE file has information about copyright, licensing, and permissions.

How to install:

See here for instructions.

Documentation:

Our webpage describes the goals of the project and has links to many related publications.

For an introduction to how to use Verifiable C, read the manual, or consult Software Foundations Volume 5: Verifiable C for a tutorial with exercises.

Program Logics for Certified Compilers, by Andrew W. Appel et al., Cambridge University Press, 2014. Available in hardcover.

vst's Issues

Prove REFLEXIVITYTAC_msubst_sound

Will require reified msubst proof

Write canceller tactic

Improve go_lower0

I've seen at least one case where go_lower does quite a bit of autorewriting after go_lower0 has already made the goal trivially solvable (_ |-- !!True). It might be worth trying to solve these at this point.

I saw this in the call to entailer after semac_SC_set is applied, which could probably be quick_typecheck instead

field_address reasoning lemmas

In the sha proofs, there are various places with reasoning about field_address. You can find these places by looking for uses of field_clarify and field_at_compatible',
or by unfoldings of field_address. I expect that those proofs could be made much simpler and nicer if we design the right schemas for reasoning about field_address, then prove lemmas to support those schemas.

Also, consider the command p=c->data,
where data is an array field of the c struct.
This currently produces a postcondition where p is described using an offset_val,
but it would be really nice if p could be described (automatically) using field_address.
There may be other similar cases.

Optimize set_reif_eq2 proof

This is the proof that the denotation of set_reif is the same as the denotation of reified set....

exprD' tus tvs (typtree typ) tr = Some val ->
exprD' tus tvs (typtree typ) (App (App (Inj (inr (Data (fset typ i)))) vr) tr)  =
exprD' tus tvs (typtree typ) (set_reif i vr tr typ).

Looks like it's going to take around 45 minutes if I liberally sprinkle abstract. Use of Gregory's autorewrite library is probably at least part of the issue. I'm open to input on how much of a priority this is. There will be at least 2 other proofs that take at least this long by the time the soundness proof is finished. Probably more, because I think @QinxiangCao will be adding some reified functions.

Make local2ptree complete

So that the following lemma in symexe.v can be proved:

Lemma local2ptree_eq :
forall (P : list Prop) (Q : list (environ -> Prop))
         (R : list (environ -> mpred)) (T1 : PTree.t val)
         (T2 : PTree.t (type * val)) (Q' : list (environ -> Prop)),
       local2ptree Q T1 T2 Q' ->
       PROPx P (LOCALx Q (SEPx R))
       = PROPx P (LOCALx (LocalD T1 T2 Q') (SEPx R)).
Admitted.

Clarify what structured-data predicates to use in ref manual

It would be great if the refcard gave more information about when to use each of the 3 structured-data predicates.

My current understanding is

• array_at use only when you need to join-split arrays, for example a program like mergesort on arrays
• field_at use when you want to load or store from the middle of a data-structure
• data_at use if you are only going to load or store from the top level of the data-structure

Can you use field_at whenever you would use data_at but at a slight cost of convenience?

CBV for listspec

Now to reflect expressions with listspec we will need defined, not QED proofs for the soundness of equality on c types and positives. This means changing the end of the proof in expr, and redoing the proof of soundness for Peqb

Remove/limit typechecker

In order to to run benchmarks (#1).

forward_call gives bad error message when return type mismatches

http://stackoverflow.com/questions/27462765/tactic-failure-use-forward-call-w-method-signature/27485590

When a funspec's parameter/return types fail to match the actual C program's function declaration, then forward_call fails with the wrong error message: it complains about the witness type instead.

[tested in VST 1.5]

data_at, field_address

Let these lemmas work:

field_at t path v p = data_at _ v (field_address 1 t path p)
array_at t path lo hi v p = data_at _ v (field_address (hi - lo) t (ArraySubsc lo :: path) p)

field_compatible n t (ArraySubsc i :: path) = field_compatible 1 t path /\ 0 <= i /\ i + n <= sz

Prove soundness of symexe tactic

Prove soundness of Applying set

Proof of applying set is currently stuck on #16

Rtac version of nth solver

Given p, write a Rtac to find an (t_root, n), such that

nth_error R n = Some (data_at sh t_root v p)

by scanning R.

forward_while should give error message when expression fails to symbolically evaluate

In the attached example, forward_while fails because there is no "temp _n n" in the loop invariant. There should be a useful error message.

need_while_error_message.zip

Make reified load also work with top level, dynamically sized arrays

Currently reified symbolic execution (possibly incorrectly) guesses that the type of the relevant data_at is going to be the same as the type of the expression. This is correct unless the load is from a pointer to an array, in which case the type of the data_at will be different.

For now this will result in an unsolvable entailment. The solution is to do a mini-cancellation (on the pointer of the data_at) by checking equality with the pointers of all data_at in the precondition. The type of the data_at can then be supplied to the lemma application.

Reifying the c type and just letting cancellation deal with it is not a valid solution to this problem, because there is another variable that is dependent on the c type. Because of this, the lemma must be parameterized over the c type.

Prove REFLEXIVITY_DENOTE sound

for #11

Symbolic execution for load rule

Compilation error when running `make_version` during build process on OS X

I am trying to build VST (in conjunction with reading Programming Logics for Certified Compilers) on the latest version OS X (10.10) and I get the following error when running make_version:

...
sh util/make_version
date: illegal option -- -
usage: date [-jnu] [-d dst] [-r seconds] [-t west] [-v[+|-]val[ymwdHMS]] ...
            [-f fmt date | [[[mm]dd]HH]MM[[cc]yy][.ss]] [+format]
COQC version.v
File ".../VST-1.5.3/version.v", line 2, characters 0-1:
Error: No focused proof (No proof-editing in progress).
make: *** [version.vo] Error 1

This happens both on the latest stable release and the git master branch.
I believe this is due to the make_version script being dependent on the GNU versions of the date and echo commands.

I think there might be multiple ways to mitigate this problem:

• Making a note in the BUILD_ORGANIZATION file stating that one needs to install coreutils using MacPorts or Homebrew and somehow replace the date and echo calls with gdate and gecho calls (or link the date and echo commands to the custom version)
• or Making a portable sh or python script that is not dependent on underlying OS as the make_version script is now

I am willing to provide a PR if there is any solution preferred and no one else makes one.

Prove rmsubst sound

for #31

Write a Rtac version of hoist_later_in_pre

Write a Rtac version of hoist_later_in_pre to connect all set, load rule together.

checking for loads in `forward` is too eager

In the statement

Sset _v (Efield (Ederef e t) _tail t'

forward complains:

The_expression_or_parameter_list_must_not_contain_any_loads_but_the_following_subexpression_is_an_implicit_or_explicit_load_Please_refactor_this_stament_of_your_program

It is probably because forward1 it is checking with no_loads_expr that no loads appear in (Ederef e t). What it should probably do is only checking that no loads appear in e.

Clean up forward.v

There are lots of huge comments and lemmas in forward.v that could be removed or put in more appropriate files.

Reify assertD load lemma

Don't export proof irrelevance and existential extentionality as hints to auto

msl/coqlib2 has

Hint Extern 1 (@eq _ _ _) => exact (proof_irr _ _).

and one for extensionality. These should at least be given database names so they aren't used by default.

Prove the soundness of applying load rule in rtac

The difficulty here is that the reified version of reptype is involved, unlike proving the sounding of set rule.

Remove elements_remove

Elements_remove is unprovable, if PTree.elements does not ensure the order of elements.

Stackframe_of_freeable_blocks in veric/semax_call.v should be reproved without using elements_remove.

A proof theory for stronger

list_cell, list_cell_eq

In progs/verif_reverse.v, the Lemma list_cell_eq is unproved.
I think the solution is to change the definition of list_cell (in list_dt.v)
using field_except_at instead of magic wand.

local variables in function-spec postcondition

When the user puts parameters or local variables other than ret_temp into a function postcondition, this is automatically wrong. The system should give a warning about that a.s.a.p. (perhaps in the start_function tactic), as a helpful diagnosis.

Exponential blow up in Rtac load store rules

Current version of reptype_reptyp will unfold the whole reptype structure. When a subgoal is reflect back, reptype_reptyp is unfolded, thus Coq got a exponentially sized term.

Two potential solutions.

1: put fst, snd into cbv_denote, and change (let (x, _) := t in x) back to (Fst t) at the end.

2: redefined reptype_reptyp by eq_rect_r.

field_at_compatible

The lemma field_at_compatible needs to be proved.
Also, that lemma and field_address_compatible need to be moved into the appropriate file in floyd.
Right now they're at the beginning of sha/sha_lemmas.v.

Prove semax_set_localD

In file mc_reify/set_reif.v

A set rule with field_address

Consider

struct t {
int a[10];
struct s {
int b1, b2;
} b;
} x;

int * p;
struct s {
int b1, b2;
} * q;

p = t.a;
q = &(t.b);

Create "round-trip" tactic

Tactic to reify, symexe, reflect all in one command. Requires #11

Run Benchmarks

Set tactic not working

seems to be a failure in the application of the set lemma

globalenv vs Genv.globalenv

New compcert use globalenv on top level while previous versions use Genv.globalenv.

Now, some proof in compcert is still based on Genv.globalenv. We should clean that somehow in the future.

Reroot, fold_data_at

In principle, users should not unfold a data_at when doing load/store operations. Reroot_field/reroot_array is used before function call and fold_data_at is used after function.

unfold_data_at/unfold_field_at and split_array are also offered for manual operations.
array_at_len_0 and array_at_len_1 might also be useful.
field_at_data_at and array_at_data_at are the reroot lemmas and users can also use them for manual operations.

Unfold_data_at (also unfold_field_at): unfold one layer down. Leaf cases cannot be unfolded. Array cases are unfolded to array_at.
split_array split an array into two parts.
reroot tactics will (1) apply unfold and split recursively (2) rewrite field_at_data_at or array_at_data_at to finish the reroot process.
fold_data_at will (1) find all related field_address and field_address0 and reverse related data_at back to field_at or array_at (2) fold data_at back recursively

array_seg_reroot_lemma too strict

The array_seg_reroot_lemma (in floyd/array_lemmas.v) does not permit
empty array segments. That is, it requires lo<hi instead of lo<=hi.
This is a real problem for proving programs correct; it is the cause
of several admits in the sha proofs. (This will be in my next commit,
not yet in the repo.) To find examples, look for the comment
(* array_seg_reroot_lemma too strict? )
in sha/verif_sha.v

Tactic for solving msubst

Currently msbust goals are reified as rmsubst which simplifies to an expr. This only worked in my examples because they don't do any PTree lookups. It won't work with the PTrees because the variables can't be instantiated. That is we have a subgoal in our reified lemma that looks like:

rmsubst_eval_expr (var 1) (var 2) ...

and we expected the vars to be instantiated, while this is obviously impossible because they are arguments to a function.

Instead we should reify as

App App fmsubst_eval_expr (var 1) (var 2)

so the vars can be instantiated. We will then solve the goal with a special tactic that uses rmsubst_eval_expr

examples/cont makefile

On 12/15/2014 8:11 PM, [email protected] wrote:

Just wanted to let you know that the [cont] directory makefile doesn’t seem to work as is on my system. I needed to add [-I path/to/compcert -as compcert] to the command line flags for [coqc].

Write tactic to apply load rule in Rtac

In order to finish #8 .

forward_if tactic is not documented in the Verifiable C manual

according to Miles Yucht

Fold id names

When we reflect, identifier names e.g. _p will be unfolded into positives. Here are a couple of solutions

1. create ptree in start_function mapping positives to "folded positives", supply this to the denotation function
2. create list of pairs in start_function tactic with the same mapping. Use change in ltac to replace the unfolded values

Prove reified set function correct

Requires changing reified-set function to return a reified set on failure. The function must always typecheck

Rewrite some proofs to use reified tactics

which ones needs to be determined. Obviously SHA is a decent choice, but will the slow entailments hide the improvement to forward?

This is progress towards #1

Write load RTac

Prove REFLEXIVITY_sound

For #11

Write assertD (super-super-canonical) lemma for load