coq-stdpp:5a73c4edfb423c4cbead774d288d97cabf71e049 commitshttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commits/5a73c4edfb423c4cbead774d288d97cabf71e0492015-02-08T19:38:19+01:00https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/5a73c4edfb423c4cbead774d288d97cabf71e049Update copyright headers.2015-02-08T19:38:19+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/b2109c25442e833f2bb398259a395a3ef0cb81caSupport function pointers and use a state monad in the frontend.2015-02-08T18:22:07+01:00Robbert Krebbersmail@robbertkrebbers.nl
Important changes in the core semantics:
* Types extended with function types. Since function types are a special kind
of pointer types, types now have an additional mutual part called "ptr_type".
* Pointers extended with function pointers. Theses are just names that refer
to an actual function in the function environment.
* Typing environments extended to assign argument and return types to function
names. Before we used a separate environment for these, but since the
argument and return types are already needed to type function pointers, this
environment would appear in pretty much every typing judgment.
As a side-effect, the frontend has been rewritten entirely. The important
changes are:
* Type checking of expressions is more involved: there is a special kind of
expression type corresponding to a function designator.
* To handle things like block scoped extern function, more state-fullness was
needed. To prepare for future extensions, the entire frontend now uses a
state monad.https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/8b7ea9be416d4b7bb3389037ee3007e4b938a6faSupport alignment.2015-02-01T00:23:34+01:00Robbert Krebbersmail@robbertkrebbers.nl
Type environments now describe alignment, this allows to:
* Prove properties about alignment, for example that bit offsets
of addresses are always aligned.
* Support align_of expressions in the frontend.https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/5f7378160512d4cef1246b008e092a70426b704cType punning for lookup/alter on values.2015-01-30T00:30:50+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/5644d68f4f15012ace5d956314cc68ad8b8b982amem_force no longer flattens the entire subobject for "unsigned char"2015-01-29T16:32:43+01:00Robbert Krebbersmail@robbertkrebbers.nladdresses.
The operation "mem_force Γ m a" used to apply the identify function to
pricisely the object "a", even in case "a" is an "unsigned char" address
refering to an individual byte. This caused the ctree substructure of the
entire subobject to disappear and had the undesired effect that:
mem_force Γ a m ⊑{Γ,true@Γm} m
failed to hold (i.e. unused reads cannot be removed).https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/fdcc90dd918e1e34d87fbc6141c2c76dbdbd77bdLet the malloc expression non-deterministically yield NULL.2015-01-27T21:33:30+01:00Robbert Krebbersmail@robbertkrebbers.nl
* This behavior is "implementation defined" and can be turned on and off
using the Boolean field "alloc_can_fail" of the class "Env".
* The expression "EAlloc" is now an r-value of pointer type instead of an
l-value.
* The executable semantics for expressions is now non-deterministic. Hence,
some proofs had to be revised.https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/41c7048e9ecef02b3ec57a352f6083fb98a2cbd8More properties about conversions between natsets and Boolean lists.2015-01-25T16:39:01+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/bf21d0d2bcf5faef7102dc514f3989b79e757493More separation properties, in particular about locking/unlocking.2015-01-25T16:38:51+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/914f32eec7693c255088060e6f52811f2bd760d8More lenient pointer equality.2014-12-23T20:12:23+01:00Robbert Krebbersmail@robbertkrebbers.nl
Pointer equality is now defined using absolute object offsets. The treatment
is similar to CompCert:
* Equality of pointers in the same object is defined provided the object has
not been deallocated.
* Equality of pointers in different objects is defined provided both pointers
have not been deallocated and both are strict (i.e. not end-of-array).
Thus, pointer equality is defined for all pointers that are not-end-of-array
and have not been deallocated. The following examples have defined behavior:
int x, y;
printf("%d\n", &x == &y);
int *p = malloc(sizeof(int)), *q = malloc(sizeof(int));
printf("%d\n", p == q);
struct S { int a; int b; } s, *r = &s;
printf("%d\n", &s.a + 1 == &(r->b));
The following not:
int x, y;
printf("%d\n", &x + 1 == &y);https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/39d73ee8df7d8f0095128dd3b02ca7ae0c5efe37Misc option stuff.2014-12-18T00:42:16+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/26917d003249dcb1a379fc6c5edddefbb5a4ac4aAllow frozen pointer annotations to be refined.2014-12-16T19:21:35+01:00Robbert Krebbersmail@robbertkrebbers.nl
The refinement relation on addresses allows union references to be refined:
(β2 → β1) → RUnion i s β1 ⊆ RUnion i s β2
The result is that frozen values are below their unfrozen variant, which made
it possible to prove that constant propagation (see constant_propagation.v) can
be performed on the level of the memory model.https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/364f5410c1f6d3f033038aa17bb797fd277c5b3cRemove duplicate None decider.2014-11-23T14:55:38+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/da7a14bb509e8c561eff60fe71d17772233327fbMore accurate formalization of integer ranks.2014-11-15T14:51:12+01:00Robbert Krebbersmail@robbertkrebbers.nl
Integers with the same size, are no longer supposed to have the same rank. As a
result, the C integer types (char, short, int, long, long long) are different
(and thus cannot alias) even if they have the same size. We now have to use a
more involved definition of integer promotions and usual arithmetic conversions.
However, this new definition follows the C standard literally.https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/39e490e935bd49d709e8486fd48dc304cf5db41aType class for [maybe_] deconstructors.2014-11-06T22:37:26+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/cc62f6c066bb6ee253e479a21d4ba3a7e883ccbaStronger completeness proof for the executable semantics.2014-10-09T20:08:43-04:00Robbert Krebbersmail@robbertkrebbers.nl
The proof now uses the stronger notion of memory permutation instead of a more
general memory refinement. We have also proven that memory permutations are
symmetric.https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/c5c0d37369613aafd074e4beeba5d3d300a07909Allow memory refinements to behave like simple renaming.2014-10-08T19:54:36-04:00Robbert Krebbersmail@robbertkrebbers.nl
Memory refinements now carry a boolean parameter that has the following
meaning:
[false] : Behave like a simple renaming of memories that merely allows to
permute object identifiers. It does not allow to refine memories
into a more defined version.
[true] : Behave like before. Objects can be injected, and memory contents can
be refined into a more defined variant.
We make refinements parametric in these two variant to avoid code duplication,
and because the [false] variant is a special case of the [true] variant.
For completeness of the executable semantics, we now use the [false] variant.https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/682546592e51552431d4273ad3a4ca8194964d67Fix compilation with Coq 8.4pl4.2014-10-06T21:52:26-04:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/044d309d40bba56e49512c1d99ad64fa1a593e72Completeness of constant expression evaluation.2014-10-02T22:56:24-04:00Robbert Krebbersmail@robbertkrebbers.nl
Also better error messages if a constant expression is expected.https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/dad635d8e7ac5485935ff888c9b22acd8a1cf196Handle storage specifiers property.2014-09-30T16:18:44-04:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/5912f8b1487d1e9547a34e11afbfdd5f465c5ffcLet simplify_equality perform injection less eagerly.2014-09-30T16:17:41-04:00Robbert Krebbersmail@robbertkrebbers.nl
Now it only performs injection on hypotheses of the shape f .. = f ..https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/1aec445120f9a8ba0f7bb8d0862e6b7c54c55facSoundness of constant expression evaluation.2014-09-25T00:16:24+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/34b2d077e85483c7bb168cc01dfda81136070465Pretty printer for N and Z, fresh string generator.2014-09-16T02:55:14+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/1e946119d10cd9476d7d211045b426fd9ff38f70Improve errors now that we use strings for names.2014-09-13T20:08:47+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/70ee147275d787383e8fc0d4f7d26f0289eddd69Use the ascii decider from the stdlib which is extracted correctly.2014-09-12T23:40:17+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/8da8fbc795ced035f8648be246da87e57d174f25Finite maps and finite sets over strings.2014-09-12T15:23:02+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/18e47df669b669ffd76c2691d7c605eb5d9d578fLemmas on Forall3 and tweak list tactics.2014-09-06T14:20:17+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/93de71b273f11cf4d2431d521e0f74f34d0e8d46Clean up ars.v.2014-09-06T14:20:17+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/7df279970018544311942d901eaaa78c8ebe6cb5Add map_Forall3.2014-09-06T14:20:17+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/98e6192842f7c8f855bbbffeaca5b3d68a2fd854Strengthen induction lemma for reflexive transitive closure.2014-09-06T14:20:17+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/6907a08a35f5326ebb531a0ac4aa6a73daebaf07Make collection tactics work with guards.2014-09-03T13:02:40+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/0ec18c143ce3e5f83b54d5dbe8b1e7275be51da6Repeat function on streams.2014-09-03T13:02:20+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/2e1b8a418d12704435232a36383d1c3b43c71eceMisc lemmas on option.2014-09-03T13:02:05+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/fe9771cc617ac34b5066cd1b4e232ac4ace675dbDecider for empty listsets.2014-09-03T13:01:38+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/52a3dc34dd27b2220ec267d24ad8e574fd18f952Prove Forall3_app.2014-09-03T13:01:19+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/dbbda8cb715b5fb4f626a26b1aa76ba616aae3beProve that lockset ⊆ dom memory.2014-08-26T00:21:37+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/7f9c5994dddd04acb2f8bf4253cf4383453a096bModify typing judgments to depend on a description of the types of objects in2014-08-22T10:10:16+02:00Robbert Krebbersmail@robbertkrebbers.nlmemory instead of the whole memory itself.
This has the following advantages:
* Avoid parametrization in {addresses,pointers,pointer_bits,bits}.v
* Make {base_values,values}.v independent of the memory, this makes better
parallelized compilation possible.
* Allow small memories (e.g. singletons as used in separation logic) with
addresses to objects in another part to be typed.
* Some proofs become easier, because the memory environments are preserved
under many operations (insert, force, lock, unlock).
It also as the following disadvantages:
* At all kinds of places we now have explicit casts from memories to memory
environments. This is kind of ugly. Note, we cannot declare memenv_of as a
Coercion because it is non-uniform.
* It is a bit inefficient with respect to the interpreter, because memory
environments are finite functions instead of proper functions, so calling
memenv_of often (which we do) is not too good.https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/7040c0403a1d8aad442baafab71bb84dcc9d525cMake simplify_error_equality a bit faster.2014-08-22T10:09:48+02:00Robbert Krebbersmail@robbertkrebbers.nl
It is still rather slow, though.https://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/d4da6f17d14bea70617d5bb5cf20ebd523dd22c6Add error monad.2014-08-09T03:03:57+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/7b5dd349b34520bcc707c85ba0c6f04f637b744bUpdate README.2014-08-07T21:59:10+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/swasey/coq-stdpp/-/commit/7d197b3e6efe03946ee87a8af4694e3537d124deBreak at 802014-08-06T22:25:14+02:00Robbert Krebbersmail@robbertkrebbers.nl