Changeset 520


Ignore:
Timestamp:
Feb 15, 2011, 3:37:52 PM (6 years ago)
Author:
mulligan
Message:

more changes

File:
1 edited

Legend:

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

    r519 r520  
    255255\label{subsect.representing.memory}
    256256
     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
     261
    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.
    341346
     347% Show example of pattern matching with polymorphic variants
     348
    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.
    442449
     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.
     474
     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
    465479
    466480%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.