Changeset 520

Feb 15, 2011, 3:37:52 PM (11 years ago)

more changes

1 edited


  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r519 r520  
     257% Different memory spaces are addressed with different sized pointers, and may use different addressing modes
     258% Many-many map between addressing modes and memory spaces (e.g. DIRECT can be used to address low internal RAM and SFRs)
     259% Maybe show snippet of get/set_arg_8?
     260% Discuss overlapping memory: we implement as if disjoint memory spaces, but when we get/set we handle overlapping cases
    257262The MCS-51 has numerous different types of memory.
    258263In our prototype implementation, we simply used a map datastructure from the O'Caml standard library.
    340345For instance, the \texttt{MOV} instruction, can be invoked using one of sixteen combinations of addressing modes.
     347% Show example of pattern matching with polymorphic variants
    342349Such non-orthogonality in the instruction set was handled with the use of polymorphic variants in the O'Caml emulator.
    343350For instance, we introduced types corresponding to each addressing mode:
    441448We see that the constructor \texttt{ADD} expects two parameters, the first being the accumulator A (\texttt{acc\_a}), and the second being one of a register, direct, indirect or data addressing mode.
     450% One of these coercions opens up a proof obligation which needs discussing
     451% Have lemmas proving that if an element is a member of a sub, then it is a member of a superlist, and so on
    443452The final, missing component is a pair of type coercions from \texttt{addressing\_mode} to \texttt{subaddressing\_mode} and from \texttt{subaddressing\_mode} to \texttt{Type$\lbrack0\rbrack$}, respectively.
    444453The previous machinery allows us to state in the type of a function what addressing modes that function expects.
    463472All other cases are discharged by the catch-all at the bottom of the match expression.
    464473Attempting to match against another addressing mode not indicated in the type (for example, \texttt{REGISTER}) will produce a type-error.
     475% Note the execute_1 function which leaves open over 200 proof obligations which we can close automatically, provided we have the lemmas mentioned above
     476% Give an example of the type of proof obligations left open?
     477% Talk about extraction to O'Caml code, which hopefully will allow us to extract back to using polymorphic variants, or when extracting vectors we could extract using phantom types
     478% Discuss alternative approaches, i.e. Sigma types to piece together smaller types into larger ones, as opposed to using a predicate to `cut out' pieces of a larger type, which is what we did
Note: See TracChangeset for help on using the changeset viewer.