X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fopcode.ma;h=47312085f146a5c58f104da6e63ddc4a27b17897;hb=84b0d9386906e5bf13bf3d0e6ea736e05ac9e8b8;hp=27a49f1208b3c427424dcbe2805c690332c0d07e;hpb=5806e0aa438ae85f09c93c93ba9f53d9663d7420;p=helm.git diff --git a/helm/software/matita/library/freescale/opcode.ma b/helm/software/matita/library/freescale/opcode.ma index 27a49f120..47312085f 100644 --- a/helm/software/matita/library/freescale/opcode.ma +++ b/helm/software/matita/library/freescale/opcode.ma @@ -24,9 +24,6 @@ (* data ultima modifica 15/11/2007 *) (* ********************************************************************** *) -set "baseuri" "cic:/matita/freescale/opcode/". - -(*include "/media/VIRTUOSO/freescale/aux_bases.ma".*) include "freescale/aux_bases.ma". (* ********************************************** *) @@ -51,8 +48,17 @@ inductive instr_mode: Type ≝ (* INHERENT = nessun operando (H implicito) *) | MODE_INHH : instr_mode + (* INHERENT_ADDRESS = nessun operando (HX implicito) *) +| MODE_INHX0ADD : instr_mode + (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *) +| MODE_INHX1ADD : instr_mode + (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *) +| MODE_INHX2ADD : instr_mode + (* IMMEDIATE = operando valore immediato byte = 0xbb *) | MODE_IMM1 : instr_mode + (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *) +| MODE_IMM1EXT : instr_mode (* IMMEDIATE = operando valore immediato word = 0xwwww *) | MODE_IMM2 : instr_mode (* DIRECT = operando offset byte = [0x00bb] *) @@ -329,40 +335,45 @@ definition magic_of_instr_mode ≝ | MODE_INHA ⇒ 〈x0,x1〉 | MODE_INHX ⇒ 〈x0,x2〉 | MODE_INHH ⇒ 〈x0,x3〉 - -| MODE_IMM1 ⇒ 〈x0,x4〉 -| MODE_IMM2 ⇒ 〈x0,x5〉 -| MODE_DIR1 ⇒ 〈x0,x6〉 -| MODE_DIR2 ⇒ 〈x0,x7〉 -| MODE_IX0 ⇒ 〈x0,x8〉 -| MODE_IX1 ⇒ 〈x0,x9〉 -| MODE_IX2 ⇒ 〈x0,xA〉 -| MODE_SP1 ⇒ 〈x0,xB〉 -| MODE_SP2 ⇒ 〈x0,xC〉 - -| MODE_DIR1_to_DIR1 ⇒ 〈x0,xD〉 -| MODE_IMM1_to_DIR1 ⇒ 〈x0,xE〉 -| MODE_IX0p_to_DIR1 ⇒ 〈x0,xF〉 -| MODE_DIR1_to_IX0p ⇒ 〈x1,x0〉 - -| MODE_INHA_and_IMM1 ⇒ 〈x1,x1〉 -| MODE_INHX_and_IMM1 ⇒ 〈x1,x2〉 -| MODE_IMM1_and_IMM1 ⇒ 〈x1,x3〉 -| MODE_DIR1_and_IMM1 ⇒ 〈x1,x4〉 -| MODE_IX0_and_IMM1 ⇒ 〈x1,x5〉 -| MODE_IX0p_and_IMM1 ⇒ 〈x1,x6〉 -| MODE_IX1_and_IMM1 ⇒ 〈x1,x7〉 -| MODE_IX1p_and_IMM1 ⇒ 〈x1,x8〉 -| MODE_SP1_and_IMM1 ⇒ 〈x1,x9〉 - - (* 26-33: bisogna considerare l'operando implicito *) -| MODE_DIRn o ⇒ plus_b8nc 〈x1,xA〉 〈x0,(exadecim_of_oct o)〉 - (* 34-41: bisogna considerare l'operando implicito *) -| MODE_DIRn_and_IMM1 o ⇒ plus_b8nc 〈x2,x2〉 〈x0,(exadecim_of_oct o)〉 - (* 42-57: bisogna considerare l'operando implicito *) -| MODE_TNY e ⇒ plus_b8nc 〈x2,xA〉 〈x0,e〉 - (* 58-99: bisogna considerare gli operandi impliciti *) -| MODE_SRT t ⇒ plus_b8nc 〈x3,xA〉 (byte8_of_bitrigesim t) + +| MODE_INHX0ADD ⇒ 〈x0,x4〉 +| MODE_INHX1ADD ⇒ 〈x0,x5〉 +| MODE_INHX2ADD ⇒ 〈x0,x6〉 + +| MODE_IMM1 ⇒ 〈x0,x7〉 +| MODE_IMM1EXT ⇒ 〈x0,x8〉 +| MODE_IMM2 ⇒ 〈x0,x9〉 +| MODE_DIR1 ⇒ 〈x0,xA〉 +| MODE_DIR2 ⇒ 〈x0,xB〉 +| MODE_IX0 ⇒ 〈x0,xC〉 +| MODE_IX1 ⇒ 〈x0,xD〉 +| MODE_IX2 ⇒ 〈x0,xE〉 +| MODE_SP1 ⇒ 〈x0,xF〉 +| MODE_SP2 ⇒ 〈x1,x0〉 + +| MODE_DIR1_to_DIR1 ⇒ 〈x1,x1〉 +| MODE_IMM1_to_DIR1 ⇒ 〈x1,x2〉 +| MODE_IX0p_to_DIR1 ⇒ 〈x1,x3〉 +| MODE_DIR1_to_IX0p ⇒ 〈x1,x4〉 + +| MODE_INHA_and_IMM1 ⇒ 〈x1,x5〉 +| MODE_INHX_and_IMM1 ⇒ 〈x1,x6〉 +| MODE_IMM1_and_IMM1 ⇒ 〈x1,x7〉 +| MODE_DIR1_and_IMM1 ⇒ 〈x1,x8〉 +| MODE_IX0_and_IMM1 ⇒ 〈x1,x9〉 +| MODE_IX0p_and_IMM1 ⇒ 〈x1,xA〉 +| MODE_IX1_and_IMM1 ⇒ 〈x1,xB〉 +| MODE_IX1p_and_IMM1 ⇒ 〈x1,xC〉 +| MODE_SP1_and_IMM1 ⇒ 〈x1,xD〉 + + (* 27-34: bisogna considerare l'operando implicito *) +| MODE_DIRn o ⇒ plus_b8nc 〈x1,xE〉 〈x0,(exadecim_of_oct o)〉 + (* 35-42: bisogna considerare l'operando implicito *) +| MODE_DIRn_and_IMM1 o ⇒ plus_b8nc 〈x2,x6〉 〈x0,(exadecim_of_oct o)〉 + (* 43-58: bisogna considerare l'operando implicito *) +| MODE_TNY e ⇒ plus_b8nc 〈x2,xE〉 〈x0,e〉 + (* 59-100: bisogna considerare gli operandi impliciti *) +| MODE_SRT t ⇒ plus_b8nc 〈x3,xE〉 (byte8_of_bitrigesim t) ]. (* confronto fra instr_mode *) @@ -401,13 +412,57 @@ let rec get_word_count (m:mcu_type) (b:byte8) (c:nat) ] ]. +(* su tutta la lista quante volte compare lo pseudocodice *) +let rec get_pseudo_count (m:mcu_type) (o:opcode) (c:nat) + (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝ + match l with + [ nil ⇒ c + | cons hd tl ⇒ match fst4T ???? hd with + [ anyOP o' ⇒ match eqop m (anyOP m o) (anyOP m o') with + [ true ⇒ get_pseudo_count m o (S c) tl + | false ⇒ get_pseudo_count m o c tl + ] + ] + ]. + +(* su tutta la lista quante volte compare la modalita' *) +let rec get_mode_count (m:mcu_type) (i:instr_mode) (c:nat) + (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝ + match l with + [ nil ⇒ c + | cons hd tl ⇒ match eqim (snd4T ???? hd) i with + [ true ⇒ get_mode_count m i (S c) tl + | false ⇒ get_mode_count m i c tl + ] + ]. + (* b e' non implementato? *) -let rec test_not_impl (b:byte8) (l:list byte8) on l ≝ +let rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝ match l with [ nil ⇒ false | cons hd tl ⇒ match eq_b8 b hd with [ true ⇒ true - | false ⇒ test_not_impl b tl + | false ⇒ test_not_impl_byte b tl + ] + ]. + +(* o e' non implementato? *) +let rec test_not_impl_pseudo (o:opcode) (l:list opcode) on l ≝ + match l with + [ nil ⇒ false + | cons hd tl ⇒ match eqop HC05 (anyOP HC05 o) (anyOP HC05 hd) with + [ true ⇒ true + | false ⇒ test_not_impl_pseudo o tl + ] + ]. + +(* i e' non implementato? *) +let rec test_not_impl_mode (i:instr_mode) (l:list instr_mode) on l ≝ + match l with + [ nil ⇒ false + | cons hd tl ⇒ match eqim i hd with + [ true ⇒ true + | false ⇒ test_not_impl_mode i tl ] ]. @@ -442,33 +497,38 @@ definition forall_opcode ≝ λP. (* iteratore sulle modalita' *) definition forall_instr_mode ≝ λP. P MODE_INH -⊗ P MODE_INHA -⊗ P MODE_INHX +⊗ P MODE_INHA +⊗ P MODE_INHX ⊗ P MODE_INHH -⊗ P MODE_IMM1 -⊗ P MODE_IMM2 -⊗ P MODE_DIR1 +⊗ P MODE_INHX0ADD +⊗ P MODE_INHX1ADD +⊗ P MODE_INHX2ADD + +⊗ P MODE_IMM1 +⊗ P MODE_IMM1EXT +⊗ P MODE_IMM2 +⊗ P MODE_DIR1 ⊗ P MODE_DIR2 -⊗ P MODE_IX0 -⊗ P MODE_IX1 -⊗ P MODE_IX2 -⊗ P MODE_SP1 +⊗ P MODE_IX0 +⊗ P MODE_IX1 +⊗ P MODE_IX2 +⊗ P MODE_SP1 ⊗ P MODE_SP2 -⊗ P MODE_DIR1_to_DIR1 +⊗ P MODE_DIR1_to_DIR1 ⊗ P MODE_IMM1_to_DIR1 -⊗ P MODE_IX0p_to_DIR1 +⊗ P MODE_IX0p_to_DIR1 ⊗ P MODE_DIR1_to_IX0p -⊗ P MODE_INHA_and_IMM1 -⊗ P MODE_INHX_and_IMM1 +⊗ P MODE_INHA_and_IMM1 +⊗ P MODE_INHX_and_IMM1 ⊗ P MODE_IMM1_and_IMM1 -⊗ P MODE_DIR1_and_IMM1 -⊗ P MODE_IX0_and_IMM1 +⊗ P MODE_DIR1_and_IMM1 +⊗ P MODE_IX0_and_IMM1 ⊗ P MODE_IX0p_and_IMM1 -⊗ P MODE_IX1_and_IMM1 -⊗ P MODE_IX1p_and_IMM1 +⊗ P MODE_IX1_and_IMM1 +⊗ P MODE_IX1p_and_IMM1 ⊗ P MODE_SP1_and_IMM1 ⊗ forall_oct (λo. P (MODE_DIRn o))