(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* 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:nat)
+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 (S c) tl
+ [ 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:nat)
+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 (S c) tl
+ [ 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:nat)
+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 (S c) tl
+ [ 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:nat)
+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_instrmode (snd4T … hd) i with
- [ true ⇒ get_mode_count m i (S c) tl
+ | 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
]
].
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_instrmode i hd with
+ | 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:nat)
+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_instrmode i (snd4T … hd)) with
- [ true ⇒ get_OpIm_count m o i (S c) tl
+ (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_opcode ≝ λP.
+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 TXA ⊗ P TXS ⊗ P WAIT.
(* iteratore sulle modalita' *)
-ndefinition forall_instr_mode ≝ λP.
+ndefinition forall_im ≝ λP.
P MODE_INH
⊗ P MODE_INHA
⊗ P MODE_INHX
⊗ forall_oct (λo. P (MODE_DIRn o))
⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o))
-⊗ forall_exadecim (λe. P (MODE_TNY e))
-⊗ forall_bitrigesim (λt. P (MODE_SRT t)).
+⊗ forall_ex (λe. P (MODE_TNY e))
+⊗ forall_bit (λt. P (MODE_SRT t)).