source: C-semantics/README @ 9

Last change on this file since 9 was 9, checked in by campbell, 10 years ago

Enough of an executable semantics to execute a not-quite-trivial program,
plus a patch for compcert to convert C to a matita definition.

File size: 4.7 KB
Line 
1Status of matita port of CompCert 1.6 C semantics
2=================================================
3
4Last seen working with matita svn r10877 with the patch at the bottom of this
5file.
6
7- Most of the memory model has been ported (common/Mem.v -> Mem.ma).
8  The main exception is minor arithmetic results than were proven with
9  omega, which we hope to prove using matita's automation at some
10  point.
11
12- The memory model is executable; some small tests can be found in
13  test/memorymodel.ma.  Note that the handling of integer values is
14  axiomatised, so conversions are not yet evaluated.
15
16- The C syntax has been ported, minus a few lemmas that are not used by
17  the semantics.
18
19- Most of the small-step C semantics has been ported, although much of the
20  underlying arithmetic and environment functions are only present as axioms,
21  including the type of identifiers.
22
23- Nonetheless, this is sufficient to show the semantics of a trivial C program
24  in test/trivial.ma.
25
26- A collection of definitions and lemmas that probably ought to be in
27  matita's standard library can be found in extralib.ma.
28
29- Some of the machine integers (i.e., integers modulo) results are
30  given as axioms in Integers.ma.  Implementing them could be
31  difficult if we keep using a unary representation of integers as
32  formalisation involves constants like 2^32.
33
34* Some experimental work on an executable semantics has been started in
35  Cexec.ma.  At present only a small subset of expressions and statements
36  are handled.
37
38* The patch in compcert-1.7.1-matita.patch adds a -dmatita option to
39  output a matita file containing a definition for the C program.
40  Note that there must be a "main" function.  (This was made against
41  1.7.1 for convenience - the Clight syntax is the same as 1.6.)
42
43There is a more recent version of compcert available with a revised memory
44model that may be more closely suited to our needs.
45
46matita issues and workarounds
47-----------------------------
48
49No unfold tactic yet; use reduction or rewriting instead.
50
51ndestruct often takes too long; getting rid of irrelevant information (e.g.,
52replacing the goal with False) sometimes helps, or an extra lemma can be used.
53
54Some of the pattern matching in the C syntax has had to be unfolded in
55a rather unpleasant way (where matching on pairs was used in the original).
56
57The use of records in place of modules is a little delicate: large records
58tend to use a lot of memory and processor at the moment, and the names of the
59fields tend to clash a lot.
60
61The lack of sections has been replaced by duplicating the variables in some
62places, and adding a record in others.
63
64Detail per-file
65---------------
66
67AST.ma
68
69  No concrete type for ident.
70  Program transformation sections left alone.
71
72Coqlib.ma
73
74  Only essential parts:
75  - "align" is axiomatised
76  - option_map
77  - parts of list disjointness and non-repetition
78
79Csem.ma
80
81  The small step semantics have been ported.  None of the big step semantics or
82  the equivalence proof has been ported.
83
84Csyntax.ma
85
86  Everything except for a few minor definitions / lemmas that are not required
87  by the semantics.
88
89Errors.ma
90
91  Only a basic definition without error messages.
92
93Events.ma
94
95  Most of the definitions; haven't needed many of the lemmas yet.
96
97Floats.ma
98
99  Axiomatised, but so was the original!
100
101Globalenvs.ma
102
103  Basic definition only.
104
105Integers.ma
106
107  Most of the operations have been ported, although some have been left as
108  axioms because the underlying operation is not present.  The use of the
109  Coq module system to abstract over the word size has been left out for
110  now.
111
112Maps.ma
113
114  Only a basic definition.
115
116Mem.ma
117
118  Everything except for omega in proofs.
119
120Smallstep.ma
121
122  Ported definitions for multiple steps and program behaviour; left
123  alternative definitions, some lemmas, plus simulations sections for later.
124
125Values.ma
126
127  The definitions about values which don't rely on arithmetics operations that
128  haven't been ported yet are done.  The other definitions and most of the
129  lemmas still remain to be done.
130
131
132
133
134Index: matita/nlibrary/arithmetics/Z.ma
135===================================================================
136--- matita/nlibrary/arithmetics/Z.ma    (revision 10877)
137+++ matita/nlibrary/arithmetics/Z.ma    (working copy)
138@@ -13,6 +13,7 @@
139 (**************************************************************************)
140 
141 include "arithmetics/nat.ma".
142+include "arithmetics/compare.ma".
143 
144 ninductive Z : Type %G≝%@
145   OZ : Z
146@@ -508,7 +509,7 @@
147    ##[//
148    ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
149    ##|//]
150-##|ncases y;//
151+##|ncases y;/2/
152 ##|ncases y
153    ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
154       nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
Note: See TracBrowser for help on using the repository browser.