source: C-semantics/README @ 15

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

Make some definitions more normalization friendly by a little 'nlet rec'
abuse.

File size: 4.6 KB
Line 
1Status of matita port of CompCert 1.6 C semantics
2=================================================
3
4Last seen working with matita svn r10890.
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
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.
32
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
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
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 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!
111
112Globalenvs.ma
113
114  Basic definition only.
115
116Integers.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
123Maps.ma
124
125  Only a basic definition.
126
127Mem.ma
128
129  Everything except for omega in proofs.
130
131Smallstep.ma
132
133  Ported definitions for multiple steps and program behaviour; left
134  alternative definitions, some lemmas, plus simulations sections for later.
135
136Values.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.
141
142
Note: See TracBrowser for help on using the repository browser.