emulator/multivm/multivm_base.ma emulator/status/status_setter.ma
compiler/environment.ma common/string.ma compiler/ast_type.ma
emulator/read_write/IP2022_read_write.ma emulator/read_write/read_write_base.ma emulator/status/status_setter.ma
-emulator/translation/translation_base.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma
+emulator/translation/translation_base.ma common/option.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma
compiler/ast_base_type.ma common/comp.ma compiler/ast_base_type_base.ma num/bool_lemmas.ma
emulator/opcodes/IP2022_table.ma common/list.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.ma
emulator/status/HC05_status.ma emulator/status/HC05_status_base.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/translation/translation_base.ma".
+
+(* ******************************************************* *)
+(* TRADUZIONE MCU+PSEUDO+MODALITA'+ARGOMENTI → ESADECIMALE *)
+(* ******************************************************* *)
+
+(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
+ninductive Freescale_MA_check : Freescale_instr_mode → Type ≝
+ maINH : Freescale_MA_check MODE_INH
+| maINHA : Freescale_MA_check MODE_INHA
+| maINHX : Freescale_MA_check MODE_INHX
+| maINHH : Freescale_MA_check MODE_INHH
+| maINHX0ADD : Freescale_MA_check MODE_INHX0ADD
+| maINHX1ADD : byte8 → Freescale_MA_check MODE_INHX1ADD
+| maINHX2ADD : word16 → Freescale_MA_check MODE_INHX2ADD
+| maIMM1 : byte8 → Freescale_MA_check MODE_IMM1
+| maIMM1EXT : byte8 → Freescale_MA_check MODE_IMM1EXT
+| maIMM2 : word16 → Freescale_MA_check MODE_IMM2
+| maDIR1 : byte8 → Freescale_MA_check MODE_DIR1
+| maDIR2 : word16 → Freescale_MA_check MODE_DIR2
+| maIX0 : Freescale_MA_check MODE_IX0
+| maIX1 : byte8 → Freescale_MA_check MODE_IX1
+| maIX2 : word16 → Freescale_MA_check MODE_IX2
+| maSP1 : byte8 → Freescale_MA_check MODE_SP1
+| maSP2 : word16 → Freescale_MA_check MODE_SP2
+| maDIR1_to_DIR1 : byte8 → byte8 → Freescale_MA_check MODE_DIR1_to_DIR1
+| maIMM1_to_DIR1 : byte8 → byte8 → Freescale_MA_check MODE_IMM1_to_DIR1
+| maIX0p_to_DIR1 : byte8 → Freescale_MA_check MODE_IX0p_to_DIR1
+| maDIR1_to_IX0p : byte8 → Freescale_MA_check MODE_DIR1_to_IX0p
+| maINHA_and_IMM1 : byte8 → Freescale_MA_check MODE_INHA_and_IMM1
+| maINHX_and_IMM1 : byte8 → Freescale_MA_check MODE_INHX_and_IMM1
+| maIMM1_and_IMM1 : byte8 → byte8 → Freescale_MA_check MODE_IMM1_and_IMM1
+| maDIR1_and_IMM1 : byte8 → byte8 → Freescale_MA_check MODE_DIR1_and_IMM1
+| maIX0_and_IMM1 : byte8 → Freescale_MA_check MODE_IX0_and_IMM1
+| maIX0p_and_IMM1 : byte8 → Freescale_MA_check MODE_IX0p_and_IMM1
+| maIX1_and_IMM1 : byte8 → byte8 → Freescale_MA_check MODE_IX1_and_IMM1
+| maIX1p_and_IMM1 : byte8 → byte8 → Freescale_MA_check MODE_IX1p_and_IMM1
+| maSP1_and_IMM1 : byte8 → byte8 → Freescale_MA_check MODE_SP1_and_IMM1
+| maDIRn : ∀n.byte8 → Freescale_MA_check (MODE_DIRn n)
+| maDIRn_and_IMM1 : ∀n.byte8 → byte8 → Freescale_MA_check (MODE_DIRn_and_IMM1 n)
+| maTNY : ∀e.Freescale_MA_check (MODE_TNY e)
+| maSRT : ∀t.Freescale_MA_check (MODE_SRT t)
+.
+
+(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
+ MA_check i → list (t_byte8 m) *)
+ndefinition Freescale_args_picker ≝
+λm.λi:Freescale_instr_mode.λargs:Freescale_MA_check i.
+ match args with
+ (* inherent: legale se nessun operando *)
+ [ maINH ⇒ nil ?
+ | maINHA ⇒ nil ?
+ | maINHX ⇒ nil ?
+ | maINHH ⇒ nil ?
+ (* inherent address: legale se nessun operando/1 byte/1 word *)
+ | maINHX0ADD ⇒ nil ?
+ | maINHX1ADD b ⇒ [ TByte m b ]
+ | maINHX2ADD w ⇒ [ TByte m (cnH ? w); TByte m (cnL ? w) ]
+ (* _0/1/2: legale se nessun operando/1 byte/1 word *)
+ | maIMM1 b ⇒ [ TByte m b ]
+ | maIMM1EXT b ⇒ [ TByte m b ]
+ | maIMM2 w ⇒ [ TByte m (cnH ? w); TByte m (cnL ? w) ]
+ | maDIR1 b ⇒ [ TByte m b ]
+ | maDIR2 w ⇒ [ TByte m (cnH ? w); TByte m (cnL ? w) ]
+ | maIX0 ⇒ nil ?
+ | maIX1 b ⇒ [ TByte m b ]
+ | maIX2 w ⇒ [ TByte m (cnH ? w); TByte m (cnL ? w) ]
+ | maSP1 b ⇒ [ TByte m b ]
+ | maSP2 w ⇒ [ TByte m (cnH ? w); TByte m (cnL ? w) ]
+ (* movimento: legale se 2 operandi byte *)
+ | maDIR1_to_DIR1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maIMM1_to_DIR1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maIX0p_to_DIR1 b ⇒ [ TByte m b]
+ | maDIR1_to_IX0p b ⇒ [ TByte m b]
+ (* cbeq/dbnz: legale se 1/2 operandi byte *)
+ | maINHA_and_IMM1 b ⇒ [ TByte m b]
+ | maINHX_and_IMM1 b ⇒ [ TByte m b]
+ | maIMM1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maDIR1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maIX0_and_IMM1 b ⇒ [ TByte m b]
+ | maIX0p_and_IMM1 b ⇒ [ TByte m b]
+ | maIX1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maIX1p_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maSP1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ (* DIRn: legale se 1 operando byte *)
+ | maDIRn _ b ⇒ [ TByte m b]
+ (* DIRn_and_IMM1: legale se 2 operandi byte *)
+ | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ (* TNY: legale se nessun operando *)
+ | maTNY _ ⇒ nil ?
+ (* SRT: legale se nessun operando *)
+ | maSRT _ ⇒ nil ?
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/translation/translation_base.ma".
+
+(* ******************************************************* *)
+(* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
+(* ******************************************************* *)
+
+(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
+ninductive IP2022_MA_check : IP2022_instr_mode → Type ≝
+ maINH : IP2022_MA_check MODE_INH
+| maIMM3 : ∀n.IP2022_MA_check (MODE_IMM3 n)
+| maIMM8 : byte8 → IP2022_MA_check MODE_IMM8
+| maIMM13 : ∀t.byte8 → IP2022_MA_check (MODE_IMM13 t)
+| maFR0_and_W : byte8 → IP2022_MA_check MODE_FR0_and_W
+| maFR1_and_W : byte8 → IP2022_MA_check MODE_FR1_and_W
+| maW_and_FR0 : byte8 → IP2022_MA_check MODE_W_and_FR0
+| maW_and_FR1 : byte8 → IP2022_MA_check MODE_W_and_FR1
+| maFR0n : ∀n.byte8 → IP2022_MA_check (MODE_FR0n n)
+| maFR1n : ∀n.byte8 → IP2022_MA_check (MODE_FR1n n)
+.
+
+(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
+ MA_check i → list (t_byte8 m) *)
+ndefinition IP2022_args_picker ≝
+λi:IP2022_instr_mode.λargs:IP2022_MA_check i.
+ match args with
+ [ maINH ⇒ nil ?
+ | maIMM3 _ ⇒ nil ?
+ | maIMM8 b ⇒ [ TByte IP2022 b ]
+ | maIMM13 _ b ⇒ [ TByte IP2022 b ]
+ | maFR0_and_W b ⇒ [ TByte IP2022 b ]
+ | maFR1_and_W b ⇒ [ TByte IP2022 b ]
+ | maW_and_FR0 b ⇒ [ TByte IP2022 b ]
+ | maW_and_FR1 b ⇒ [ TByte IP2022 b ]
+ | maFR0n _ b ⇒ [ TByte IP2022 b ]
+ | maFR1n _ b ⇒ [ TByte IP2022 b ]
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/translation/Freescale_translation.ma".
+include "emulator/translation/IP2022_translation.ma".
+
+(* ******************************************************* *)
+(* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
+(* ******************************************************* *)
+
+(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
+ndefinition MA_check ≝
+λmcu:mcu_type.
+ match mcu
+ return λm.(aux_im_type m) → Type
+ with
+ [ HC05 ⇒ Freescale_MA_check
+ | HC08 ⇒ Freescale_MA_check
+ | HCS08 ⇒ Freescale_MA_check
+ | RS08 ⇒ Freescale_MA_check
+ | IP2022 ⇒ IP2022_MA_check
+ ].
+
+(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
+ MA_check i → list (t_byte8 m) *)
+ndefinition args_picker ≝
+λmcu:mcu_type.
+ match mcu
+ return λm.Πi:(aux_im_type m).MA_check m i → ?
+ with
+ [ HC05 ⇒ Freescale_args_picker HC05
+ | HC08 ⇒ Freescale_args_picker HC08
+ | HCS08 ⇒ Freescale_args_picker HCS08
+ | RS08 ⇒ Freescale_args_picker RS08
+ | IP2022 ⇒ IP2022_args_picker
+ ].
+
+(* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
+nlet rec bytes_of_pseudo_instr_mode_param_aux (m:mcu_type) (o:aux_pseudo_type m) (i:aux_im_type m) (p:MA_check m i)
+ (param:list (aux_table_type m)) on param ≝
+ match param with
+ [ nil ⇒ None ? | cons hd tl ⇒
+ match (eqc ? o (fst4T … hd)) ⊗ (eqc ? i (snd4T … hd)) with
+ [ true ⇒ match thd4T … hd with
+ [ Byte isab ⇒
+ Some ? ([ (TByte m isab) ]@(args_picker m i p))
+ | Word isaw ⇒
+ Some ? ([ (TByte m (cnH ? isaw)) ; (TByte m (cnL ? isaw)) ]@(args_picker m i p))
+ ]
+ | false ⇒ bytes_of_pseudo_instr_mode_param_aux m o i p tl ]].
+
+ndefinition bytes_of_pseudo_instr_mode_param ≝
+λm:mcu_type.λo:aux_pseudo_type m.λi:aux_im_type m.λp:MA_check m i.
+bytes_of_pseudo_instr_mode_param_aux m o i p (opcode_table m).
+
+(* ****************************** *)
+(* APPROCCIO COMPILAZIONE AL VOLO *)
+(* ****************************** *)
+
+(* ausiliario di compile *)
+ndefinition defined_option ≝
+ λT:Type.λo:option T.
+ match o with
+ [ None ⇒ False
+ | Some _ ⇒ True
+ ].
+
+(* compila solo se l'intera istruzione+modalita'+argomenti ha riscontro nelle tabelle *)
+ndefinition compile ≝
+λmcu:mcu_type.λi:aux_im_type mcu.λop:aux_pseudo_type mcu.λarg:MA_check mcu i.
+ match bytes_of_pseudo_instr_mode_param mcu op i arg
+ return λres:option ?.defined_option ? res → ?
+ with
+ [ None ⇒ λp:defined_option ? (None ?).False_rect_Type0 ? p
+ | Some x ⇒ λp:defined_option ? (Some ? x).x
+ ].
+
+(* detipatore del compilato: (t_byte8 m) → byte8 *)
+nlet rec source_to_byte8_aux (m:mcu_type) (p2:list byte8) (p1:list (t_byte8 m)) on p1 ≝
+ match p1 with
+ [ nil ⇒ p2
+ | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_aux m (p2@[b]) tl ]
+ ].
+
+ndefinition source_to_byte8 ≝ λm:mcu_type.source_to_byte8_aux m [].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/opcodes/pseudo.ma".
+include "common/option.ma".
+include "emulator/opcodes/HC05_table.ma".
+include "emulator/opcodes/HC08_table.ma".
+include "emulator/opcodes/HCS08_table.ma".
+include "emulator/opcodes/RS08_table.ma".
+include "emulator/opcodes/IP2022_table.ma".
+
+(* ***************************** *)
+(* TRADUZIONE ESADECIMALE → INFO *)
+(* ***************************** *)
+
+(* accesso alla tabella della ALU prescelta *)
+ndefinition opcode_table ≝
+λm:mcu_type.
+ match m
+ return λm:mcu_type.list (aux_table_type m)
+ with
+ [ HC05 ⇒ opcode_table_HC05
+ | HC08 ⇒ opcode_table_HC08
+ | HCS08 ⇒ opcode_table_HCS08
+ | RS08 ⇒ opcode_table_RS08
+ | IP2022 ⇒ opcode_table_IP2022
+ ].
+
+(* traduzione mcu+esadecimale → info *)
+(* NB: la ricerca per byte non matcha con una word con lo stesso byte superiore uguale *)
+(* NB: per matchare una word (precode+code) bisogna passare una word *)
+(* NB: il risultato e' sempre un'opzione, NON esiste un dummy opcode tipo UNKNOWN/ILLEGAL *)
+nlet rec full_info_of_word16_aux (m:mcu_type) (borw:byte8_or_word16) (param:list (aux_table_type m)) on param ≝
+ match param with
+ [ nil ⇒ None ?
+ | cons hd tl ⇒
+ match thd4T … hd with
+ [ Byte b ⇒ match borw with
+ [ Byte borw' ⇒ match eqc ? borw' b with
+ [ true ⇒ Some ? hd
+ | false ⇒ full_info_of_word16_aux m borw tl ]
+ | Word _ ⇒ full_info_of_word16_aux m borw tl ]
+ | Word w ⇒ match borw with
+ [ Byte _ ⇒ full_info_of_word16_aux m borw tl
+ | Word borw' ⇒ match eqc ? borw' w with
+ [ true ⇒ Some ? hd
+ | false ⇒ full_info_of_word16_aux m borw tl ]
+ ]]].
+
+ndefinition full_info_of_word16 ≝
+λm:mcu_type.λborw:byte8_or_word16.
+full_info_of_word16_aux m borw (opcode_table m).
+
+(* introduzione di un tipo byte8 dipendente dall'mcu_type (phantom type) *)
+ninductive t_byte8 (m:mcu_type) : Type ≝
+ TByte : byte8 → t_byte8 m.
+
+ndefinition eq_tbyte8 ≝
+λm.λtb1,tb2:t_byte8 m.
+ match tb1 with
+ [ TByte b1 ⇒ match tb2 with
+ [ TByte b2 ⇒ eqc ? b1 b2 ]].
projects / helm.git / commitdiff