source: C-semantics/README @ 5

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

Add a few execution steps and calculation of the initial state to the
"executable" C semantics.

File size: 3.5 KB
Line 
1Status of matita port of CompCert C semantics
2=============================================
3
4Last seen working with matita svn r10871.
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 could be
30  difficult if we keep using a unary representation of integers as
31  formalisation involves constants like 2^32.
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
37matita issues and workarounds
38-----------------------------
39
40No unfold tactic yet; use reduction or rewriting instead.
41
42ndestruct often takes too long; getting rid of irrelevant information (e.g.,
43replacing the goal with False) sometimes helps, or an extra lemma can be used.
44
45Some of the pattern matching in the C syntax has had to be unfolded in
46a rather unpleasant way (where matching on pairs was used in the original).
47
48The use of records in place of modules is a little delicate: large records
49tend to use a lot of memory and processor at the moment, and the names of the
50fields tend to clash a lot.
51
52The lack of sections has been replaced by duplicating the variables in some
53places, and adding a record in others.
54
55Detail per-file
56---------------
57
58AST.ma
59
60  No concrete type for ident.
61  Program transformation sections left alone.
62
63Coqlib.ma
64
65  Only essential parts:
66  - "align" is axiomatised
67  - option_map
68  - parts of list disjointness and non-repetition
69
70Csem.ma
71
72  The small step semantics have been ported.  None of the big step semantics or
73  the equivalence proof has been ported.
74
75Csyntax.ma
76
77  Everything except for a few minor definitions / lemmas that are not required
78  by the semantics.
79
80Errors.ma
81
82  Only a basic definition without error messages.
83
84Events.ma
85
86  Most of the definitions; haven't needed many of the lemmas yet.
87
88Floats.ma
89
90  Axiomatised, but so was the original!
91
92Globalenvs.ma
93
94  Basic definition only.
95
96Integers.ma
97
98  Most of the operations have been ported, although some have been left as
99  axioms because the underlying operation is not present.  The use of the
100  Coq module system to abstract over the word size has been left out for
101  now.
102
103Maps.ma
104
105  Only a basic definition.
106
107Mem.ma
108
109  Everything except for omega in proofs.
110
111Smallstep.ma
112
113  Ported definitions for multiple steps and program behaviour; left
114  alternative definitions, some lemmas, plus simulations sections for later.
115
116Values.ma
117
118  The definitions about values which don't rely on arithmetics operations that
119  haven't been ported yet are done.  The other definitions and most of the
120  lemmas still remain to be done.
Note: See TracBrowser for help on using the repository browser.