From f7804325dbb5b51820edefe5d5ffff89809fe35c Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Sat, 6 Feb 2010 13:13:17 +0000 Subject: [PATCH] freescale porting --- .../matita/contribs/ng_assembly2/depends | 2 +- .../translation/Freescale_translation.ma | 115 ++++++++++++++++++ .../translation/IP2022_translation.ma | 58 +++++++++ .../emulator/translation/translation.ma | 104 ++++++++++++++++ .../emulator/translation/translation_base.ma | 81 ++++++++++++ 5 files changed, 359 insertions(+), 1 deletion(-) create mode 100755 helm/software/matita/contribs/ng_assembly2/emulator/translation/Freescale_translation.ma create mode 100755 helm/software/matita/contribs/ng_assembly2/emulator/translation/IP2022_translation.ma create mode 100755 helm/software/matita/contribs/ng_assembly2/emulator/translation/translation.ma create mode 100755 helm/software/matita/contribs/ng_assembly2/emulator/translation/translation_base.ma diff --git a/helm/software/matita/contribs/ng_assembly2/depends b/helm/software/matita/contribs/ng_assembly2/depends index fc6f53f6b..a1fff45d7 100644 --- a/helm/software/matita/contribs/ng_assembly2/depends +++ b/helm/software/matita/contribs/ng_assembly2/depends @@ -35,7 +35,7 @@ emulator/opcodes/RS08_table_tests.ma emulator/opcodes/RS08_table.ma emulator/opc 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 diff --git a/helm/software/matita/contribs/ng_assembly2/emulator/translation/Freescale_translation.ma b/helm/software/matita/contribs/ng_assembly2/emulator/translation/Freescale_translation.ma new file mode 100755 index 000000000..98d182310 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly2/emulator/translation/Freescale_translation.ma @@ -0,0 +1,115 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ? + ]. diff --git a/helm/software/matita/contribs/ng_assembly2/emulator/translation/IP2022_translation.ma b/helm/software/matita/contribs/ng_assembly2/emulator/translation/IP2022_translation.ma new file mode 100755 index 000000000..a207c7c93 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly2/emulator/translation/IP2022_translation.ma @@ -0,0 +1,58 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ] + ]. diff --git a/helm/software/matita/contribs/ng_assembly2/emulator/translation/translation.ma b/helm/software/matita/contribs/ng_assembly2/emulator/translation/translation.ma new file mode 100755 index 000000000..6c31b186e --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly2/emulator/translation/translation.ma @@ -0,0 +1,104 @@ +(**************************************************************************) +(* ___ *) +(* ||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 []. diff --git a/helm/software/matita/contribs/ng_assembly2/emulator/translation/translation_base.ma b/helm/software/matita/contribs/ng_assembly2/emulator/translation/translation_base.ma new file mode 100755 index 000000000..b16dffd6e --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly2/emulator/translation/translation_base.ma @@ -0,0 +1,81 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ]]. -- 2.39.2