source: C-semantics/README @ 12

Last change on this file since 12 was 12, checked in by campbell, 11 years ago

Make memory model tests more readable.
Update README.

File size: 4.1 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
50ndestruct often takes too long; getting rid of irrelevant information (e.g.,
51replacing the goal with False) sometimes helps, or an extra lemma can be used.
52
53Some of the pattern matching in the C syntax has had to be unfolded in
54a rather unpleasant way (where matching on pairs was used in the original).
55
56The use of records in place of modules is a little delicate: large records
57tend to use a lot of memory and processor at the moment, and the names of the
58fields tend to clash a lot.
59
60The lack of sections has been replaced by duplicating the variables in some
61places, and adding a record in others.
62
63Detail per-file
64---------------
65
66AST.ma
67
68  Program transformation sections left alone.
69
70Coqlib.ma
71
72  Only essential parts:
73  - align
74  - some 2^n lemmas (which could go into the binary libraries)
75  - option_map
76  - parts of list disjointness and non-repetition
77
78Csem.ma
79
80  The small step semantics have been ported.  None of the big step semantics or
81  the equivalence proof has been ported.
82
83Csyntax.ma
84
85  Everything except for a few minor definitions / lemmas that are not required
86  by the semantics.
87
88Errors.ma
89
90  Only a basic definition without error messages.
91
92Events.ma
93
94  Most of the definitions; haven't needed many of the lemmas yet.
95
96Floats.ma
97
98  Axiomatised, but so was the original!
99
100Globalenvs.ma
101
102  Basic definition only.
103
104Integers.ma
105
106  Most of the operations have been ported, although some have been left as
107  axioms because the underlying operation is not present.  The use of the
108  Coq module system to abstract over the word size has been left out for
109  now.
110
111Maps.ma
112
113  Only a basic definition.
114
115Mem.ma
116
117  Everything except for omega in proofs.  Much of the transformations sections
118  are commented out until Integers.ma is done properly.
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
Note: See TracBrowser for help on using the repository browser.