source: C-semantics/README @ 14

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

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

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, or an extra lemma can be used.
55
56Some of the pattern matching in the C syntax has had to be unfolded in
57a rather unpleasant way (where matching on pairs was used in the original).
58
59The use of records in place of modules is a little delicate: large records
60tend to use a lot of memory and processor at the moment, and the names of the
61fields tend to clash a lot.
62
63The lack of sections has been replaced by duplicating the variables in some
64places, and adding a record in others.
65
66The meminj_no_overlap definition in Mem.ma uses the logical Or explicitly
67rather than the ∨ notation to regain reasonable performance. (This is
68presumably due to disambiguation - the notation is also used for booleans.)
69
70There are a couple of places in Mem.ma where rewriting had to be done carefully
71to avoid assertions during unification; I'm not really sure what the problem
72is.
73
74Detail per-file
75---------------
76
77AST.ma
78
79  Program transformation sections left alone.
80
81Coqlib.ma
82
83  Only essential parts:
84  - align
85  - some 2^n lemmas (which could go into the binary libraries)
86  - option_map
87  - parts of list disjointness and non-repetition
88
89Csem.ma
90
91  The small step semantics have been ported.  None of the big step semantics or
92  the equivalence proof has been ported.
93
94Csyntax.ma
95
96  Everything except for a few minor definitions / lemmas that are not required
97  by the semantics.
98
99Errors.ma
100
101  Only a basic definition without error messages.
102
103Events.ma
104
105  Most of the definitions; haven't needed many of the lemmas yet.
106
107Floats.ma
108
109  Axiomatised, but so was the original!
110
111Globalenvs.ma
112
113  Basic definition only.
114
115Integers.ma
116
117  Most of the operations have been ported, although some have been left as
118  axioms because the underlying operation is not present.  The use of the
119  Coq module system to abstract over the word size has been left out for
120  now.
121
122Maps.ma
123
124  Only a basic definition.
125
126Mem.ma
127
128  Everything except for omega in proofs.
129
130Smallstep.ma
131
132  Ported definitions for multiple steps and program behaviour; left
133  alternative definitions, some lemmas, plus simulations sections for later.
134
135Values.ma
136
137  The definitions about values which don't rely on arithmetics operations that
138  haven't been ported yet are done.  The other definitions and most of the
139  lemmas still remain to be done.
140
141
Note: See TracBrowser for help on using the repository browser.