+++ /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 *)
-(* Ultima modifica: 05/08/2009 *)
-(* *)
-(* ********************************************************************** *)
-
-include "freescale/opcode_base.ma".
-include "common/list.ma".
-
-(* ********************************************* *)
-(* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
-(* ********************************************* *)
-
-(* su tutta la lista quante volte compare il byte *)
-nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16)
- (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
- match l with
- [ nil ⇒ c
- | cons hd tl ⇒ match thd4T … hd with
- [ Byte b' ⇒ match eq_b8 b b' with
- [ true ⇒ get_byte_count m b (succ_w16 c) tl
- | false ⇒ get_byte_count m b c tl
- ]
- | Word _ ⇒ get_byte_count m b c tl
- ]
- ].
-
-(* su tutta la lista quante volte compare la word (0x9E+byte) *)
-nlet rec get_word_count (m:mcu_type) (b:byte8) (c:word16)
- (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
- match l with
- [ nil ⇒ c
- | cons hd tl ⇒ match thd4T … hd with
- [ Byte _ ⇒ get_word_count m b c tl
- | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
- [ true ⇒ get_word_count m b (succ_w16 c) tl
- | false ⇒ get_word_count m b c tl
- ]
- ]
- ].
-
-(* su tutta la lista quante volte compare lo pseudocodice *)
-nlet rec get_pseudo_count (m:mcu_type) (o:opcode) (c:word16)
- (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 eq_op o o' with
- [ true ⇒ get_pseudo_count m o (succ_w16 c) tl
- | false ⇒ get_pseudo_count m o c tl
- ]
- ]
- ].
-
-(* su tutta la lista quante volte compare la modalita' *)
-nlet rec get_mode_count (m:mcu_type) (i:instr_mode) (c:word16)
- (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
- match l with
- [ nil ⇒ c
- | cons hd tl ⇒ match eq_im (snd4T … hd) i with
- [ true ⇒ get_mode_count m i (succ_w16 c) tl
- | false ⇒ get_mode_count m i c tl
- ]
- ].
-
-(* b e' non implementato? *)
-nlet 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_byte b tl
- ]
- ].
-
-(* o e' non implementato? *)
-nlet rec test_not_impl_pseudo (o:opcode) (l:list opcode) on l ≝
- match l with
- [ nil ⇒ false
- | cons hd tl ⇒ match eq_op o hd with
- [ true ⇒ true
- | false ⇒ test_not_impl_pseudo o tl
- ]
- ].
-
-(* i e' non implementato? *)
-nlet rec test_not_impl_mode (i:instr_mode) (l:list instr_mode) on l ≝
- match l with
- [ nil ⇒ false
- | cons hd tl ⇒ match eq_im i hd with
- [ true ⇒ true
- | false ⇒ test_not_impl_mode i tl
- ]
- ].
-
-(* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
-nlet rec get_OpIm_count (m:mcu_type) (o:any_opcode m) (i:instr_mode) (c:word16)
- (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
- match l with
- [ nil ⇒ c
- | cons hd tl ⇒
- match (eq_anyop m o (fst4T … hd)) ⊗
- (eq_im i (snd4T … hd)) with
- [ true ⇒ get_OpIm_count m o i (succ_w16 c) tl
- | false ⇒ get_OpIm_count m o i c tl
- ]
- ].
-
-(* iteratore sugli opcode *)
-ndefinition forall_op ≝ λP.
- P ADC ⊗ P ADD ⊗ P AIS ⊗ P AIX ⊗ P AND ⊗ P ASL ⊗ P ASR ⊗ P BCC ⊗
- P BCLRn ⊗ P BCS ⊗ P BEQ ⊗ P BGE ⊗ P BGND ⊗ P BGT ⊗ P BHCC ⊗ P BHCS ⊗
- P BHI ⊗ P BIH ⊗ P BIL ⊗ P BIT ⊗ P BLE ⊗ P BLS ⊗ P BLT ⊗ P BMC ⊗
- P BMI ⊗ P BMS ⊗ P BNE ⊗ P BPL ⊗ P BRA ⊗ P BRCLRn ⊗ P BRN ⊗ P BRSETn ⊗
- P BSETn ⊗ P BSR ⊗ P CBEQA ⊗ P CBEQX ⊗ P CLC ⊗ P CLI ⊗ P CLR ⊗ P CMP ⊗
- P COM ⊗ P CPHX ⊗ P CPX ⊗ P DAA ⊗ P DBNZ ⊗ P DEC ⊗ P DIV ⊗ P EOR ⊗
- P INC ⊗ P JMP ⊗ P JSR ⊗ P LDA ⊗ P LDHX ⊗ P LDX ⊗ P LSR ⊗ P MOV ⊗
- P MUL ⊗ P NEG ⊗ P NOP ⊗ P NSA ⊗ P ORA ⊗ P PSHA ⊗ P PSHH ⊗ P PSHX ⊗
- P PULA ⊗ P PULH ⊗ P PULX ⊗ P ROL ⊗ P ROR ⊗ P RSP ⊗ P RTI ⊗ P RTS ⊗
- P SBC ⊗ P SEC ⊗ P SEI ⊗ P SHA ⊗ P SLA ⊗ P STA ⊗ P STHX ⊗ P STOP ⊗
- P STX ⊗ P SUB ⊗ P SWI ⊗ P TAP ⊗ P TAX ⊗ P TPA ⊗ P TST ⊗ P TSX ⊗
- P TXA ⊗ P TXS ⊗ P WAIT.
-
-(* iteratore sulle modalita' *)
-ndefinition forall_im ≝ λP.
- P MODE_INH
-⊗ P MODE_INHA
-⊗ P MODE_INHX
-⊗ P MODE_INHH
-
-⊗ 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_SP2
-
-⊗ P MODE_DIR1_to_DIR1
-⊗ P MODE_IMM1_to_DIR1
-⊗ P MODE_IX0p_to_DIR1
-⊗ P MODE_DIR1_to_IX0p
-
-⊗ 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_IX0p_and_IMM1
-⊗ P MODE_IX1_and_IMM1
-⊗ P MODE_IX1p_and_IMM1
-⊗ P MODE_SP1_and_IMM1
-
-⊗ forall_oct (λo. P (MODE_DIRn o))
-⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o))
-⊗ forall_ex (λe. P (MODE_TNY e))
-⊗ forall_bit (λt. P (MODE_SRT t)).
projects / helm.git / blobdiff