[9] | 1 | Status of matita port of CompCert 1.6 C semantics |
---|
| 2 | ================================================= |
---|
[3] | 3 | |
---|
[12] | 4 | Last seen working with matita svn r10890. |
---|
[3] | 5 | |
---|
| 6 | - Most of the memory model has been ported (common/Mem.v -> Mem.ma). |
---|
| 7 | The main exception is minor arithmetic results than were proven with |
---|
| 8 | omega, which we hope to prove using matita's automation at some |
---|
| 9 | point. |
---|
| 10 | |
---|
| 11 | - The memory model is executable; some small tests can be found in |
---|
| 12 | test/memorymodel.ma. Note that the handling of integer values is |
---|
| 13 | axiomatised, so conversions are not yet evaluated. |
---|
| 14 | |
---|
| 15 | - The C syntax has been ported, minus a few lemmas that are not used by |
---|
| 16 | the semantics. |
---|
| 17 | |
---|
| 18 | - Most of the small-step C semantics has been ported, although much of the |
---|
| 19 | underlying arithmetic and environment functions are only present as axioms, |
---|
| 20 | including the type of identifiers. |
---|
| 21 | |
---|
| 22 | - Nonetheless, this is sufficient to show the semantics of a trivial C program |
---|
| 23 | in test/trivial.ma. |
---|
| 24 | |
---|
| 25 | - A collection of definitions and lemmas that probably ought to be in |
---|
| 26 | matita's standard library can be found in extralib.ma. |
---|
| 27 | |
---|
| 28 | - Some of the machine integers (i.e., integers modulo) results are |
---|
[12] | 29 | given as axioms in Integers.ma. Implementing them should be routine now that |
---|
| 30 | we have a binary representation of integers. The CompCert version is given |
---|
| 31 | as a functor on the word size - we don't have an equivalent of this yet. |
---|
[3] | 32 | |
---|
[5] | 33 | * Some experimental work on an executable semantics has been started in |
---|
| 34 | Cexec.ma. At present only a small subset of expressions and statements |
---|
| 35 | are handled. |
---|
| 36 | |
---|
[9] | 37 | * The patch in compcert-1.7.1-matita.patch adds a -dmatita option to |
---|
| 38 | output a matita file containing a definition for the C program. |
---|
| 39 | Note that there must be a "main" function. (This was made against |
---|
| 40 | 1.7.1 for convenience - the Clight syntax is the same as 1.6.) |
---|
| 41 | |
---|
| 42 | There is a more recent version of compcert available with a revised memory |
---|
| 43 | model that may be more closely suited to our needs. |
---|
| 44 | |
---|
[3] | 45 | matita issues and workarounds |
---|
| 46 | ----------------------------- |
---|
| 47 | |
---|
| 48 | No unfold tactic yet; use reduction or rewriting instead. |
---|
| 49 | |
---|
[14] | 50 | Normalization of term containing large definitions (such as some of the |
---|
| 51 | Integers library) can be prohibitive. This is a particular problem because |
---|
| 52 | ndestruct currently normalizes the goal and every hypothesis that is rewritten. |
---|
| 53 | For ndestruct, getting rid of irrelevant information (e.g., replacing the goal |
---|
[15] | 54 | with False) sometimes helps, an extra lemma can be used, or the definitions |
---|
| 55 | can make careful use of 'nlet rec' to prevent reduction. |
---|
[3] | 56 | |
---|
| 57 | Some of the pattern matching in the C syntax has had to be unfolded in |
---|
| 58 | a rather unpleasant way (where matching on pairs was used in the original). |
---|
| 59 | |
---|
| 60 | The use of records in place of modules is a little delicate: large records |
---|
| 61 | tend to use a lot of memory and processor at the moment, and the names of the |
---|
| 62 | fields tend to clash a lot. |
---|
| 63 | |
---|
| 64 | The lack of sections has been replaced by duplicating the variables in some |
---|
| 65 | places, and adding a record in others. |
---|
| 66 | |
---|
[14] | 67 | The meminj_no_overlap definition in Mem.ma uses the logical Or explicitly |
---|
| 68 | rather than the ∨ notation to regain reasonable performance. (This is |
---|
| 69 | presumably due to disambiguation - the notation is also used for booleans.) |
---|
| 70 | |
---|
| 71 | There are a couple of places in Mem.ma where rewriting had to be done carefully |
---|
| 72 | to avoid assertions during unification; I'm not really sure what the problem |
---|
| 73 | is. |
---|
| 74 | |
---|
[3] | 75 | Detail per-file |
---|
| 76 | --------------- |
---|
| 77 | |
---|
| 78 | AST.ma |
---|
| 79 | |
---|
| 80 | Program transformation sections left alone. |
---|
| 81 | |
---|
| 82 | Coqlib.ma |
---|
| 83 | |
---|
| 84 | Only essential parts: |
---|
[12] | 85 | - align |
---|
| 86 | - some 2^n lemmas (which could go into the binary libraries) |
---|
[3] | 87 | - option_map |
---|
| 88 | - parts of list disjointness and non-repetition |
---|
| 89 | |
---|
| 90 | Csem.ma |
---|
| 91 | |
---|
| 92 | The small step semantics have been ported. None of the big step semantics or |
---|
| 93 | the equivalence proof has been ported. |
---|
| 94 | |
---|
| 95 | Csyntax.ma |
---|
| 96 | |
---|
| 97 | Everything except for a few minor definitions / lemmas that are not required |
---|
| 98 | by the semantics. |
---|
| 99 | |
---|
| 100 | Errors.ma |
---|
| 101 | |
---|
| 102 | Only a basic definition without error messages. |
---|
| 103 | |
---|
| 104 | Events.ma |
---|
| 105 | |
---|
| 106 | Most of the definitions; haven't needed many of the lemmas yet. |
---|
| 107 | |
---|
| 108 | Floats.ma |
---|
| 109 | |
---|
| 110 | Axiomatised, but so was the original! |
---|
| 111 | |
---|
| 112 | Globalenvs.ma |
---|
| 113 | |
---|
| 114 | Basic definition only. |
---|
| 115 | |
---|
| 116 | Integers.ma |
---|
| 117 | |
---|
| 118 | Most of the operations have been ported, although some have been left as |
---|
| 119 | axioms because the underlying operation is not present. The use of the |
---|
| 120 | Coq module system to abstract over the word size has been left out for |
---|
| 121 | now. |
---|
| 122 | |
---|
| 123 | Maps.ma |
---|
| 124 | |
---|
| 125 | Only a basic definition. |
---|
| 126 | |
---|
| 127 | Mem.ma |
---|
| 128 | |
---|
[14] | 129 | Everything except for omega in proofs. |
---|
[3] | 130 | |
---|
| 131 | Smallstep.ma |
---|
| 132 | |
---|
| 133 | Ported definitions for multiple steps and program behaviour; left |
---|
| 134 | alternative definitions, some lemmas, plus simulations sections for later. |
---|
| 135 | |
---|
| 136 | Values.ma |
---|
| 137 | |
---|
| 138 | The definitions about values which don't rely on arithmetics operations that |
---|
| 139 | haven't been ported yet are done. The other definitions and most of the |
---|
| 140 | lemmas still remain to be done. |
---|
[9] | 141 | |
---|
| 142 | |
---|