Changeset 2454


Ignore:
Timestamp:
Nov 12, 2012, 4:39:56 PM (7 years ago)
Author:
campbell
Message:

More misc notes on clight->cminor.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • etc/campbell/dev-notes/2012-10-31-clight-to-cminor.txt

    r2434 r2454  
    1717We can restrict the valid environments and memories according to this mapping.
    1818Rereading the CompCert mm paper, remember that values need to be mapped
    19 according to the variable mapping too, extend the embedding on function calls,
    20 and ensure that we only provide mappings for used blocks.
     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.
    2122
    2223Object sizes
     
    3435suffice.  Note that we'd still end up checking the stack frame size later in the
    3536compilation chain, though, as the frames become larger due to spilling.
     37
     38
     39
     40Variable characterisation (globals not in local env, stack/var are, stack
     41│                          allocations disjoint)
     42
     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
Note: See TracChangeset for help on using the changeset viewer.