Changeset 557


Ignore:
Timestamp:
Feb 17, 2011, 2:52:34 PM (6 years ago)
Author:
mulligan
Message:

Emulator fixed for Wilmer

Location:
Deliverables/D4.1
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ASMInterpret.ml

    r454 r557  
    941941;;
    942942
    943 let half_add_with_overflow = assert false;;
    944 
    945943let assembly p =
    946944 let datalabels,_ =
     
    959957      | `Mov (_,_) -> pc, labels, costs
    960958      | `Jmp _
    961       | `Call _ -> (snd (half_add_with_overflow pc (BitVectors.vect_of_int 3 `Sixteen))), labels, costs  (*CSC: very stupid: always expand to worst opcode *)
     959      | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), labels, costs  (*CSC: very stupid: always expand to worst opcode *)
    962960      | `WithLabel i ->
    963961          let fake_addr _ = `REL (zero `Eight) in
     
    965963          let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in
    966964           assert (fake_jump = i');
    967            (snd (half_add_with_overflow pc pc'),labels, costs)
     965           (snd (half_add pc pc'),labels, costs)
    968966      | #instruction as i ->
    969967        let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
    970968         assert (i = i');
    971          (snd (half_add_with_overflow pc pc'),labels, costs)
     969         (snd (half_add pc pc'),labels, costs)
    972970   ) (BitVectors.zero `Sixteen,StringMap.empty,WordMap.empty) p.ASM.code
    973971 in
  • Deliverables/D4.1/ITP-Paper/itp-2011.bib

    r555 r557  
    125125
    126126@misc
     127{ cerco-report:2011,
     128  title = {D4.1: executable formal semantics of machine code},
     129  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1.pdf}},
     130  year = {2011},
     131  key = {{CerCo-report}}
     132}
     133
     134@misc
    127135{ mcu8051ide:2010,
    128136  title = {{MCU 8051 IDE} 1.3.11},
     
    151159@misc
    152160{ siemens:2011,
    153   title = {Siemens Semiconductor Group 8051 derivative instruction set},
     161  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
    154162  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
    155163  year = {2011},
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r556 r557  
    222222In Section~\ref{sect.conclusions} we conclude the paper.
    223223
    224 In Appendices~\ref{sect.listing.main.ocaml.functions} and~\ref{sect.listing.main.matita.functions} we provide a brief overview of the main functions in our implementation, and describe at a high level what they do.
    225 
    226224%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    227225% SECTION                                                                      %
     
    233231Matita's syntax is largely straightforward to those familiar with Coq or O'Caml.
    234232The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically.
     233
     234A full account of the formalisation can be found in~\cite{cerco-report:2011}.
    235235
    236236\subsection{Development strategy}
     
    282282The formalization of MCS-51 must deal with bytes (8 bits), words (16 bits) but also with more exoteric quantities (7 bits, 3 bits, 9 bits).
    283283To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans.
    284 In our O'Caml emulator, we `faked' bitvectors using phantom types implemented with polymorphic variants\cite{phantom_types_ocaml}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
     284In our O'Caml emulator, we `faked' bitvectors using phantom types~\cite{leijen:domain:1999} implemented with polymorphic variants~\cite{garrigue:programming:1998}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
    285285From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes.
    286286However, the module's interface (right column) enforces the size invariants in the rest of the code.
     
    734734\bibliography{itp-2011.bib}
    735735
     736\end{document}
     737
    736738\newpage
    737739
Note: See TracChangeset for help on using the changeset viewer.