source: etc/campbell/dev-notes/2012-10-31-clight-to-cminor.txt

Last change on this file was 2482, checked in by campbell, 7 years ago

Note about front-end simulations

File size: 4.4 KB
1[There were a few notes in 2012-10-18-front-end-correctness.txt too.]
3Variable mapping
6The stage has a mapping var_types that tells us where each variable should live,
7either as a global (in both Clight and Cminor), at a particular position on the
8stack or as a local variable in the environment (both in Cminor, in Clight they
9are an entry in the environment which gives a memory block for that variable).
11There are some properties of that mapping that should hold:
13- globals are present in the global environment and not the local environment
14  (local variables may shadow globals)
15- positions on the stack should be unique
17We can restrict the valid environments and memories according to this mapping.
18Rereading the CompCert mm paper, remember that values need to be mapped
19according to the memory mapping too (I previous wrote the variable mapping,
20but that doesn't provide the memory block mapping), extend the embedding on
21function calls, and ensure that we only provide mappings for used blocks.
23Object sizes
26I don't think we do any checks for excessively large objects and we *might*
27get into trouble here due to overflow.  I'm not entirely sure about that though,
28because signed and unsigned addition are the same with two's complement.  Even
29with excessively sized arrays I think we end up squashing the offset in the
30Clight pointer arithmetic.
32Fitting this in with the memory model changes might be more difficult (because
33we might wrap to the start of the stack frame rather than the array).  Adding a
34check that the stack size returned by characterise_vars fits in memory might
35suffice.  Note that we'd still end up checking the stack frame size later in the
36compilation chain, though, as the frames become larger due to spilling.
40Variable characterisation (globals not in local env, stack/var are, stack
41│                          allocations disjoint)
43├→ Memory mapping (needs to update mapping on fn entry for new environment,
44│  │               provide equivalent memory on exit; determines value mapping)
45│  │
46├──┼→ Expression correctness
47│  │   │                         temporary variables (Local only; not in memory)
48│  │   ↓                          extends env on the fly - may have to assume   
49└──┴→ Statement correctness    ←  some overapproximation in simulation         
50       │ (need to carry some knowledge about break/continue destinations in
51       │  simulation)
52       │
53       └→ Program correctness
55More stuff:
56- On function entry we store parameters that have stack allocated to them - so
57  calls will have to do several steps to get back to the simulation relation
58- The simulation relation will need to relate the continuations for loops in
59  Clight with a list of facts about where the entry/exit labels in Cminor go,
60  as there is no corresponding information in Cminor continuations/stacks.
62[22nd Nov:]
64Form of the simulations:
66To ensure that we can find the RTLabs measurable subtrace that we're interested
67in which corresponds to the Clight measurable subtrace that we started with we
68need to
69 - ensure that function calls and returns are preserved
70 - show that we have states corresponding to the start and end states from the
71   Clight subtrace; that is, the combined simulation relation between Clight
72   and RTLabs states should include the start of each subtrace, and the ends.
74We could take a leaf out of the back-end structured trace lifting and obtain
75results based on classifying states:
77- From an other/jump state that isn't cost labelled, some 𝑛 steps over
78  other/jump states that are not cost labelled are simulated by 𝑚 other/jump
79  steps (possibly containing labelled states that are exposed during the
80  translation of expressions)
81- a step from a call state is simulated by 𝑚 steps from a call state (all of
82  which are other except for the initial call)
83- a step from a return state is simulated by 𝑚 steps from a return state
84  (all of which are other except for the initial return)
85- a step from a cost labelled state is simulated by a single step from a cost
86  labelled state
88This should be sufficient to show that the prefix before a measurable Clight
89subtrace is simulated by the RTLabs program, the first state of the subtrace
90is in the relation with it's counterpart, and the measurable subtrace is
91simulated by the RTLabs subtrace, neatly finishing at end states which are in
92the relation.
Note: See TracBrowser for help on using the repository browser.