source: src/Clight/README @ 1603

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

Update C-semantics README.

File size: 5.5 KB
Line 
1Status of matita port of CompCert 1.6 C semantics
2=================================================
3
4Last seen working with matita svn r11115.
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.  For the C semantics deliverable these (unnecessary) properties
10  have been commented out.
11
12- The memory model is executable; some small tests can be found in
13  test/memorymodel.ma.
14
15- The Clight syntax file has been ported, minus a few lemmas that are not used
16  by the semantics.
17
18- The small-step inductively defined Clight semantics has been ported.
19
20- A collection of definitions and lemmas that probably ought to be in
21  matita's standard library can be found in extralib.ma.
22
23- Some of the theory about machine integers (i.e., integers modulo) are
24  given as axioms in Integers.ma.  Proving them should be routine now that
25  we have a binary representation of integers.  The CompCert version is given
26  as a functor on the word size - we don't have an equivalent of this yet.
27
28* The executable semantics can be found in Cexec.ma, which uses the
29  error monad in Errors.ma and the resumption monad defined in IOMonad.ma.
30
31* The patch in acc-0.1.spaces.patch adds a -ma option to the prototype
32  compiler which outputs a matita file containing the Clight program as
33  a definition usable by the semantics.  It also adds parsing support for
34  the memory space extensions (__data and friends).
35
36* The patch in compcert-1.7.1-matita.patch adds a -dmatita option to
37  output a matita file containing a definition for the C program.
38  Note that there must be a "main" function.  (This was made against
39  1.7.1 for convenience - the Clight syntax is the same as 1.6.)
40  This is an older version of the prototype compiler patch, and lacks the
41  memory extensions.
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
51Normalization of term containing large definitions (such as some of the
52Integers library) can be prohibitive.  This is a particular problem because
53ndestruct currently normalizes the goal and every hypothesis that is rewritten.
54For ndestruct, getting rid of irrelevant information (e.g., replacing the goal
55with False) sometimes helps, an extra lemma can be used, or the definitions
56can make careful use of 'nlet rec' to prevent reduction.
57
58Some of the pattern matching in the C syntax has had to be unfolded in
59a rather unpleasant way (where matching on pairs was used in the original).
60
61The use of records in place of modules is a little delicate: large records
62tend to use a lot of memory and processor at the moment, and the names of the
63fields tend to clash a lot.
64
65The lack of sections has been replaced by duplicating the variables in some
66places, and adding a record in others.
67
68The meminj_no_overlap definition in Mem.ma uses the logical Or explicitly
69rather than the ∨ notation to regain reasonable performance. (This is
70presumably due to disambiguation - the notation is also used for booleans.)
71
72There are a couple of places in Mem.ma where rewriting had to be done carefully
73to avoid assertions during unification; I'm not really sure what the problem
74is.
75
76Detail per-file
77---------------
78
79AST.ma
80
81  Program transformation sections mostly left alone.
82
83CexecComplete.ma  [new]
84
85  Completeness of steps of executable semantics wrt inductive
86
87CexecEquiv.ma  [new]
88
89  Equivalence of complete executions to inductive semantics
90
91Cexec.ma  [new]
92
93  Definition of executable semantics
94
95CexecSound.ma
96
97  Soundness of individual steps of executable semantics wrt inductive
98
99Coqlib.ma
100
101  Only essential parts:
102  - align
103  - some 2^n lemmas (which could go into the binary libraries)
104  - option_map
105  - parts of list disjointness and non-repetition
106
107CostLabel.ma  [new]
108
109  Definition of cost labels
110
111Csem.ma
112
113  The small step semantics have been ported.  None of the big step semantics or
114  the equivalence proof has been ported.
115
116Csyntax.ma
117
118  Everything except for a few minor definitions / lemmas that are not required
119  by the semantics.
120
121Errors.ma
122
123  Only a basic definition without error messages.
124
125Events.ma
126
127  Most of the definitions; haven't needed many of the lemmas yet.
128
129extralib.ma  [new]
130
131  Definitions which probably belong in the matita libraries, if anywhere.
132
133Floats.ma
134
135  Axiomatised, but so was the original!  Likely to be removed because we do
136  not intend to support floating point.
137
138Globalenvs.ma
139
140  Basic definition only; sufficient for animating the semantics.
141
142Integers.ma
143
144  The operations have been ported, although the results about them generally
145  have not.  The equality results have been left axiomatised because they
146  require proof irrelevance because each integer carries a proof that it is
147  in range.  The use of the Coq module system to abstract over the word size
148  has been left out for now.
149
150IOMonad.ma  [new]
151
152  Definition and properties of the resumption+error monad for I/O.
153
154Maps.ma
155
156  Only a basic definition.
157
158Mem.ma
159
160  Everything except for omega in proofs.
161
162Smallstep.ma
163
164  Ported definitions for multiple steps and program behaviour; left
165  alternative definitions, some lemmas, plus most of the simulations sections
166  for later.
167
168Values.ma
169
170  The definitions about operations relevant to the Clight semantics have been
171  ported.  The other definitions and most of the lemmas still remain to be done.
172
173
Note: See TracBrowser for help on using the repository browser.