# Changeset 520

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

more changes

File:
1 edited

### Legend:

Unmodified
 r519 \label{subsect.representing.memory} % Different memory spaces are addressed with different sized pointers, and may use different addressing modes % Many-many map between addressing modes and memory spaces (e.g. DIRECT can be used to address low internal RAM and SFRs) % Maybe show snippet of get/set_arg_8? % Discuss overlapping memory: we implement as if disjoint memory spaces, but when we get/set we handle overlapping cases The MCS-51 has numerous different types of memory. In our prototype implementation, we simply used a map datastructure from the O'Caml standard library. For instance, the \texttt{MOV} instruction, can be invoked using one of sixteen combinations of addressing modes. % Show example of pattern matching with polymorphic variants Such non-orthogonality in the instruction set was handled with the use of polymorphic variants in the O'Caml emulator. For instance, we introduced types corresponding to each addressing mode: We 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. % One of these coercions opens up a proof obligation which needs discussing % Have lemmas proving that if an element is a member of a sub, then it is a member of a superlist, and so on The 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. The previous machinery allows us to state in the type of a function what addressing modes that function expects. All other cases are discharged by the catch-all at the bottom of the match expression. Attempting to match against another addressing mode not indicated in the type (for example, \texttt{REGISTER}) will produce a type-error. % Note the execute_1 function which leaves open over 200 proof obligations which we can close automatically, provided we have the lemmas mentioned above % Give an example of the type of proof obligations left open? % 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 % 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%