source: C-semantics/README @ 400

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

Minor changes for the new version of matita.

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