1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "freescale_tests/medium_tests_tools.ma".
24 include "common/list_utility.ma".
25 include "common/nat_to_num.ma".
27 (* ************************ *)
28 (* HCS08GB60 String Reverse *)
29 (* ************************ *)
31 (* versione ridotta, in cui non si riazzerano gli elementi di counters *)
32 ndefinition dTest_HCS08_sReverse_source : word16 → (list byte8) ≝
34 let m ≝ HCS08 in source_to_byte8 m (
35 (* BEFORE: A=0x00 H:X=0x0D4B SP=0x0D4A PC=0x18E0 Z=true *)
37 (* static unsigned char dati[3072]={...};
39 void swap(unsigned char *a, unsigned char *b)
40 { unsigned char tmp=*a; *a=*b; *b=tmp; return; } *)
42 (* [0x18C8] allineamento *) (compile m ? NOP maINH I) @
44 (* argomenti: HX e [0x0D49-A], passaggio ibrido reg, stack *)
45 (* [0x18C9] PSHX *) (compile m ? PSHX maINH I) @
46 (* [0x18CA] PSHH *) (compile m ? PSHH maINH I) @
47 (* [0x18CB] LDHX 5,SP *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
48 (* [0x18CE] LDA ,X *) (compile m ? LDA maIX0 I) @
49 (* [0x18CF] LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
50 (* [0x18D2] PSHA *) (compile m ? PSHA maINH I) @
51 (* [0x18D3] LDA ,X *) (compile m ? LDA maIX0 I) @
52 (* [0x18D4] LDHX 6,SP *) (compile m ? LDHX (maSP1 〈x0,x6〉) I) @
53 (* [0x18D7] STA ,X *) (compile m ? STA maIX0 I) @
54 (* [0x18D8] LDHX 2,SP *) (compile m ? LDHX (maSP1 〈x0,x2〉) I) @
55 (* [0x18DB] PULA *) (compile m ? PULA maINH I) @
56 (* [0x18DC] STA ,X *) (compile m ? STA maIX0 I) @
57 (* [0x18DD] AIS #2 *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
58 (* [0x18DF] RTS *) (compile m ? RTS maINH I) @
62 unsigned int pos=0,limit=0;
64 for(limit=3072;pos<(limit/2);pos++)
65 { swap(&dati[pos],&dati[limit-pos-1]); } *)
67 (* [0x18E0] LDHX #elems *) (compile m ? LDHX (maIMM2 elems) I) @
68 (* [0x18E3] STHX 4,SP *) (compile m ? STHX (maSP1 〈x0,x4〉) I) @
69 (* [0x18E6] BRA *+52 ; 191A *) (compile m ? BRA (maIMM1 〈x3,x2〉) I) @
70 (* [0x18E8] TSX *) (compile m ? TSX maINH I) @
71 (* [0x18E9] LDA 2,X *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
72 (* [0x18EB] ADD #0x00 *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
73 (* [0x18ED] PSHA *) (compile m ? PSHA maINH I) @
74 (* [0x18EE] LDA 1,X *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
75 (* [0x18F0] ADC #0x01 *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
76 (* [0x18F2] PSHA *) (compile m ? PSHA maINH I) @
77 (* [0x18F3] LDA 4,X *) (compile m ? LDA (maIX1 〈x0,x4〉) I) @
78 (* [0x18F5] SUB 2,X *) (compile m ? SUB (maIX1 〈x0,x2〉) I) @
79 (* [0x18F7] STA ,X *) (compile m ? STA maIX0 I) @
80 (* [0x18F8] LDA 3,X *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
81 (* [0x18FA] SBC 1,X *) (compile m ? SBC (maIX1 〈x0,x1〉) I) @
82 (* [0x18FC] PSHA *) (compile m ? PSHA maINH I) @
83 (* [0x18FD] LDX ,X *) (compile m ? LDX maIX0 I) @
84 (* [0x18FE] PULH *) (compile m ? PULH maINH I) @
85 (* [0x18FF] AIX #-1 *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
86 (* [0x1901] TXA *) (compile m ? TXA maINH I) @
87 (* [0x1902] ADD #0x00 *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
88 (* [0x1904] PSHH *) (compile m ? PSHH maINH I) @
89 (* [0x1905] TSX *) (compile m ? TSX maINH I) @
90 (* [0x1906] STA 3,X *) (compile m ? STA (maIX1 〈x0,x3〉) I) @
91 (* [0x1908] PULA *) (compile m ? PULA maINH I) @
92 (* [0x1909] ADC #0x01 *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
93 (* [0x190B] LDX 3,X *) (compile m ? LDX (maIX1 〈x0,x3〉) I) @
94 (* [0x190D] PSHA *) (compile m ? PSHA maINH I) @
95 (* [0x190E] PULH *) (compile m ? PULH maINH I) @
96 (* [0x190F] BSR *-70 ; 18C9 *) (compile m ? BSR (maIMM1 〈xB,x8〉) I) @
97 (* [0x1911] AIS #2 *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
98 (* [0x1913] TSX *) (compile m ? TSX maINH I) @
99 (* [0x1914] INC 2,X *) (compile m ? INC (maIX1 〈x0,x2〉) I) @
100 (* [0x1916] BNE *+4 ; 191A *) (compile m ? BNE (maIMM1 〈x0,x2〉) I) @
101 (* [0x1918] INC 1,X *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
102 (* [0x191A] TSX *) (compile m ? TSX maINH I) @
103 (* [0x191B] LDA 3,X *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
104 (* [0x191D] PSHA *) (compile m ? PSHA maINH I) @
105 (* [0x191E] PULH *) (compile m ? PULH maINH I) @
106 (* [0x191F] LSRA *) (compile m ? LSR maINHA I) @
107 (* [0x1920] TSX *) (compile m ? TSX maINH I) @
108 (* [0x1921] LDX 4,X *) (compile m ? LDX (maIX1 〈x0,x4〉) I) @
109 (* [0x1923] RORX *) (compile m ? ROR maINHX I) @
110 (* [0x1924] PSHA *) (compile m ? PSHA maINH I) @
111 (* [0x1925] PULH *) (compile m ? PULH maINH I) @
112 (* [0x1926] CPHX 2,SP *) (compile m ? CPHX (maSP1 〈x0,x2〉) I) @
113 (* [0x1929] BHI *-65 ; 18E8 *) (compile m ? BHI (maIMM1 〈xB,xD〉) I)
116 attraverso simulazione in CodeWarrior si puo' enunciare che dopo
117 42+79*n+5*(n>>9) ci sara' il reverse di n byte (PARI) e
121 (* creazione del processore+caricamento+impostazione registri *)
122 ndefinition dTest_HCS08_sReverse_status ≝
128 set_acc_8_low_reg HCS08 t (* A<-A_op *)
129 (set_z_flag HCS08 t (* Z<-true *)
130 (setweak_sp_reg HCS08 t (* SP<-0x0D4A *)
131 (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
132 (set_pc_reg HCS08 t (* PC<-0x18E0 *)
133 (start_of_mcu_version_HCS08 MC9S08GB60 t
134 (load_from_source_at t (* carica data in RAM:dTest_HCS08_RAM *)
135 (load_from_source_at t (zero_memory t) (* carica source in ROM:dTest_HCS08_prog *)
136 (dTest_HCS08_sReverse_source elems) dTest_HCS08_prog)
137 data dTest_HCS08_RAM)
138 (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08GB60) t)
139 (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
140 false false false false false false) (* non deterministici tutti a 0 *)
141 (mk_word16 (mk_byte8 x1 x8) (mk_byte8 xE x0)))
143 (mk_word16 (mk_byte8 x0 xD) (mk_byte8 x4 xA)))
147 (* parametrizzazione dell'enunciato del teorema *)
148 (* primo sbozzo: confronto esecuzione con hexdump... *)
149 nlemma dTest_HCS08_sReverse_dump_aux ≝
150 λt:memory_impl.λstring:list byte8.
151 (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
152 (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
153 (* 2) la stringa deve avere lunghezza pari *)
154 ((and_b8 (w16l (byte8_strlen string)) 〈x0,x1〉) = 〈x0,x0〉) ∧
155 (* 3) match di esecuzione su tempo in forma di tempo esatto *)
156 (match execute HCS08 t
157 (* parametri IN: t,H:X,strlen(string),string *)
158 (TickOK ? (dTest_HCS08_sReverse_status t 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
159 (* tempo di esecuzione 42+79*n+5*(n>>9) *)
160 (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with
161 [ TickERR s _ ⇒ None ?
162 (* azzeramento tutta RAM tranne dati *)
163 | TickSUSP s _ ⇒ None ?
164 | TickOK s ⇒ Some ? (byte8_hexdump t (mem_desc HCS08 t s) dTest_HCS08_RAM (len_list ? string))
166 Some ? (reverse_list ? string)).
168 (* confronto esecuzione con hexdump... *)
170 lemma dTest_HCS08_sReverse_dump :
171 dTest_HCS08_sReverse_dump_aux MEM_TREE dTest_random_32.
172 unfold dTest_HCS08_sReverse_dump_aux;
174 [ split; [ normalize in ⊢ (%); autobatch ] reflexivity ]
179 (* parametrizzazione dell'enunciato del teorema *)
180 (* dimostrazione senza svolgimento degli stati *)
181 nlemma dTest_HCS08_sReverse_aux ≝
182 λt:memory_impl.λstring:list byte8.
183 (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
184 (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
185 (* 2) la stringa deve avere lunghezza pari *)
186 ((and_b8 (w16l (byte8_strlen string)) 〈x0,x1〉) = 〈x0,x0〉) ∧
187 (* 3) match di esecuzione su tempo in forma di tempo esatto *)
188 (match execute HCS08 t
189 (* parametri IN: t,H:X,strlen(string),string *)
190 (TickOK ? (dTest_HCS08_sReverse_status t 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
191 (* tempo di esecuzione 42+79*n+5*(n>>9) *)
192 (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with
193 [ TickERR s _ ⇒ None ?
194 (* azzeramento tutta RAM tranne dati *)
195 | TickSUSP s _ ⇒ None ?
196 | TickOK s ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
198 Some ? (set_pc_reg HCS08 t
199 (dTest_HCS08_sReverse_status t (fst … (shr_b8 (w16h (byte8_strlen string)))) (fst … (shr_w16 (byte8_strlen string))) (byte8_strlen string) (reverse_list ? string))
200 (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB)))).
203 lemma dTest_HCS08_sReverse :
204 dTest_HCS08_sReverse_aux MEM_TREE dTest_random_32.
205 unfold dTest_HCS08_sReverse_aux;
207 [ split; [ normalize in ⊢ (%); autobatch ] reflexivity ]
209 rewrite > (breakpoint HCS08 MEM_TREE (TickOK ? (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32)) 3 (39+79*byte8_strlen dTest_random_32+5*(byte8_strlen dTest_random_32/512))) in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
210 letin status0 ≝ (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32);
211 change in ⊢ (? ? match ? ? ? (? ? ? % ?) ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with
213 rewrite > (execute_HCS08_LDHX_maIMM2 MEM_TREE status0 〈x0,x0〉 〈x2,x0〉) in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
214 [ 2,3,4,5: reflexivity; ]
216 letin status1 ≝ (set_pc_reg HCS08 MEM_TREE (setweak_v_flag HCS08 MEM_TREE (setweak_n_flag HCS08 MEM_TREE (set_z_flag HCS08 MEM_TREE (set_alu HCS08 MEM_TREE (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32) (set_indX_16_reg_HC08 (alu HCS08 MEM_TREE (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32)) 〈〈x0,x0〉:〈x2,x0〉〉)) (eq_w16 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈〈x0,x0〉:〈x2,x0〉〉)) false) (filtered_plus_w16 HCS08 MEM_TREE (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32) (get_pc_reg HCS08 MEM_TREE (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32)) 3));
217 change in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with (TickOK ? status1);
219 rewrite > (breakpoint HCS08 MEM_TREE (TickOK ? status1) 5 (34+79*byte8_strlen dTest_random_32+5*(byte8_strlen dTest_random_32/512))) in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
220 change in ⊢ (? ? match ? ? ? (? ? ? % ?) ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with (TickOK ? status1);
221 rewrite > (execute_HCS08_STHX_maSP1 status1 〈x0,x4〉)
222 in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
223 [ 2,3,4,5,6,7: reflexivity; ]
230 ndefinition sReverseCalc ≝
232 match execute HCS08 MEM_TREE
233 (TickOK ? (dTest_HCS08_sReverse_status MEM_TREE 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
234 (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with
235 [ TickERR s _ ⇒ None ?
236 | TickSUSP s _ ⇒ None ?
237 | TickOK s ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
240 ndefinition sReverseNoCalc ≝
242 Some ? (set_pc_reg HCS08 MEM_TREE
243 (dTest_HCS08_sReverse_status MEM_TREE (fst … (shr_b8 (w16h (byte8_strlen string))))
244 (fst … (shr_w16 (byte8_strlen string)))
245 (byte8_strlen string) (reverse_list ? string))
246 (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB))).
248 ndefinition sReverseCalc32 ≝ sReverseCalc dTest_random_32.
249 ndefinition sReverseCalc64 ≝ sReverseCalc dTest_random_64.
250 ndefinition sReverseCalc128 ≝ sReverseCalc dTest_random_128.
251 ndefinition sReverseCalc256 ≝ sReverseCalc dTest_random_256.
252 ndefinition sReverseCalc512 ≝ sReverseCalc dTest_random_512.
253 ndefinition sReverseCalc1024 ≝ sReverseCalc dTest_random_1024.
254 ndefinition sReverseCalc2048 ≝ sReverseCalc dTest_random_2048.
255 ndefinition sReverseCalc3072 ≝ sReverseCalc dTest_random_3072.
257 ndefinition sReverseNoCalc32 ≝ sReverseNoCalc dTest_random_32.
258 ndefinition sReverseNoCalc64 ≝ sReverseNoCalc dTest_random_64.
259 ndefinition sReverseNoCalc128 ≝ sReverseNoCalc dTest_random_128.
260 ndefinition sReverseNoCalc256 ≝ sReverseNoCalc dTest_random_256.
261 ndefinition sReverseNoCalc512 ≝ sReverseNoCalc dTest_random_512.
262 ndefinition sReverseNoCalc1024 ≝ sReverseNoCalc dTest_random_1024.
263 ndefinition sReverseNoCalc2048 ≝ sReverseNoCalc dTest_random_2048.
264 ndefinition sReverseNoCalc3072 ≝ sReverseNoCalc dTest_random_3072.
266 (* *********************** *)
267 (* HCS08GB60 Counting Sort *)
268 (* *********************** *)
270 (* versione ridotta, in cui non si riazzerano gli elementi di counters *)
271 ndefinition dTest_HCS08_cSort_source : word16 → (list byte8) ≝
273 let m ≝ HCS08 in source_to_byte8 m (
274 (* BEFORE: A=0x00 H:X=0x0F4C SP=0x0F4B PC=0x18C8 Z=true *)
276 (* /* IPOTESI: INIT VARIABILI+ARRAY GIA' ESEGUITO */
277 static unsigned int counters[256]={ campitura di 0 };
278 static unsigned char dati[3072]={ dati random };
280 void CountingSort(void)
282 unsigned int index=0,position=0; *)
284 (* /* TESI: CODICE DA ESEGUIRE
286 /* calcolo del # ripetizioni degli elementi byte */
287 for(;index<3072;index++)
288 { counters[dati[index]]++; } *)
290 (* [0x18C8] BRA *+31;18E7 *) (compile m ? BRA (maIMM1 〈x1,xD〉) I) @
291 (* [0x18CA] LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
292 (* [0x18CD] LDA 256,X *) (compile m ? LDA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
293 (* [0x18D0] LSLA *) (compile m ? ASL maINHA I) @
294 (* [0x18D1] CLRX *) (compile m ? CLR maINHX I) @
295 (* [0x18D2] ROLX *) (compile m ? ROL maINHX I) @
296 (* [0x18D3] ADD #0x00 *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
297 (* [0x18D5] PSHA *) (compile m ? PSHA maINH I) @
298 (* [0x18D6] TXA *) (compile m ? TXA maINH I) @
299 (* [0x18D7] ADC #0x0D *) (compile m ? ADC (maIMM1 〈x0,xD〉) I) @
300 (* [0x18D9] PSHA *) (compile m ? PSHA maINH I) @
301 (* [0x18DA] PULH *) (compile m ? PULH maINH I) @
302 (* [0x18DB] PULX *) (compile m ? PULX maINH I) @
303 (* [0x18DC] INC 1,X *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
304 (* [0x18DE] BNE *+3 *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
305 (* [0x18E0] INC ,X *) (compile m ? INC maIX0 I) @
306 (* [0x18E1] TSX *) (compile m ? TSX maINH I) @
307 (* [0x18E2] INC 1,X *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
308 (* [0x18E4] BNE *+3 *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
309 (* [0x18E6] INC ,X *) (compile m ? INC maIX0 I) @
310 (* [0x18E7] LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
311 (* [0x18EA] CPHX #elems *) (compile m ? CPHX (maIMM2 elems) I) @ (* dimensione dei dati al massimo 0x0C00 *)
312 (* [0x18ED] BCS *-35;18CA *) (compile m ? BCS (maIMM1 〈xD,xB〉) I) @
314 (* /* sovrascrittura di dati per produrre la versione ordinata */
315 for(index=0;index<256;index++)
317 while(counters[index]--)
318 { dati[position++]=index; }
321 (* [0x18EF] TSX *) (compile m ? TSX maINH I) @
322 (* [0x18F0] CLR 1,X *) (compile m ? CLR (maIX1 〈x0,x1〉) I) @
323 (* [0x18F2] CLR ,X *) (compile m ? CLR maIX0 I) @
324 (* [0x18F3] BRA *+16 *) (compile m ? BRA (maIMM1 〈x0,xE〉) I) @
325 (* [0x18F5] TSX *) (compile m ? TSX maINH I) @
326 (* [0x18F6] LDA 1,X *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
327 (* [0x18F8] LDHX 3,SP *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
328 (* [0x18FB] STA 256,X *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
329 (* [0x18FE] AIX #1 *) (compile m ? AIX (maIMM1 〈x0,x1〉) I) @
330 (* [0x1900] STHX 3,SP *) (compile m ? STHX (maSP1 〈x0,x3〉) I) @
331 (* [0x1903] TSX *) (compile m ? TSX maINH I) @
332 (* [0x1904] LDX 1,X *) (compile m ? LDX (maIX1 〈x0,x1〉) I) @
333 (* [0x1906] LSLX *) (compile m ? ASL maINHX I) @
334 (* [0x1907] LDA 1,SP *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
335 (* [0x190A] ROLA *) (compile m ? ROL maINHA I) @
336 (* [0x190B] PSHA *) (compile m ? PSHA maINH I) @
337 (* [0x190C] PULH *) (compile m ? PULH maINH I) @
338 (* [0x190D] PSHX *) (compile m ? PSHX maINH I) @
339 (* [0x190E] LDHX 3328,X *) (compile m ? LDHX (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
340 (* [0x1912] PSHX *) (compile m ? PSHX maINH I) @
341 (* [0x1913] PSHH *) (compile m ? PSHH maINH I) @
342 (* [0x1914] AIX #-1 *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
343 (* [0x1916] PSHH *) (compile m ? PSHH maINH I) @
344 (* [0x1917] PSHA *) (compile m ? PSHA maINH I) @
345 (* [0x1918] PULH *) (compile m ? PULH maINH I) @
346 (* [0x1919] PSHX *) (compile m ? PSHX maINH I) @
347 (* [0x191A] LDX 5,SP *) (compile m ? LDX (maSP1 〈x0,x5〉) I) @
348 (* [0x191D] PULA *) (compile m ? PULA maINH I) @
349 (* [0x191E] STA 3329,X *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x1〉〉) I) @
350 (* [0x1921] PULA *) (compile m ? PULA maINH I) @
351 (* [0x1922] STA 3328,X *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
352 (* [0x1925] PULH *) (compile m ? PULH maINH I) @
353 (* [0x1926] PULX *) (compile m ? PULX maINH I) @
354 (* [0x1927] CPHX #0x0000 *) (compile m ? CPHX (maIMM2 〈〈x0,x0〉:〈x0,x0〉〉) I) @
355 (* [0x192A] PULH *) (compile m ? PULH maINH I) @
356 (* [0x192B] BNE *-54 *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
357 (* [0x192D] TSX *) (compile m ? TSX maINH I) @
358 (* [0x192E] INC 1,X *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
359 (* [0x1930] BNE *+3 *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
360 (* [0x1932] INC ,X *) (compile m ? INC maIX0 I) @
361 (* [0x1933] LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
362 (* [0x1936] CPHX #0x0100 *) (compile m ? CPHX (maIMM2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
363 (* [0x1939] BNE *-54 *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
364 (* [0x193B] STOP *) (compile m ? STOP maINH I)
367 attraverso simulazione in CodeWarrior si puo' enunciare che dopo
368 25700+150n si sara' entrati in stato STOP corrispondente con ordinamento
369 di n byte, A=0xFF H:X=0x0100 *)
372 (* creazione del processore+caricamento+impostazione registri *)
373 ndefinition dTest_HCS08_cSort_status ≝
380 setweak_i_flag HCS08 t (* I<-I_op *)
381 (set_acc_8_low_reg HCS08 t (* A<-A_op *)
382 (set_z_flag HCS08 t (* Z<-true *)
383 (setweak_sp_reg HCS08 t (* SP<-0x0F4B *)
384 (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
385 (set_pc_reg HCS08 t (* PC<-dTest_HCS08_prog *)
386 (start_of_mcu_version_HCS08
388 (load_from_source_at t (* carica data in RAM:dTest_HCS08_RAM *)
389 (load_from_source_at t (zero_memory t) (* carica source in ROM:dTest_HCS08_prog *)
390 (dTest_HCS08_cSort_source elems) dTest_HCS08_prog)
391 data dTest_HCS08_RAM)
392 (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08GB60) t)
393 (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
394 false false false false false false) (* non deterministici tutti a 0 *)
397 (mk_word16 (mk_byte8 x0 xF) (mk_byte8 x4 xB)))
402 (* parametrizzazione dell'enunciato del teorema parziale *)
403 nlemma dTest_HCS08_cSort_aux ≝
404 λt:memory_impl.λstring:list byte8.
405 (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
406 (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
407 (* 2) match di esecuzione su tempo in forma di upperbound *)
408 (match execute HCS08 t
409 (* parametri IN: t,A,H:X,strlen(string),string *)
410 (TickOK ? (dTest_HCS08_cSort_status t true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
411 (* tempo di esecuzione 25700+150*n *)
412 (((nat256 + nat1) * nat100)+((nat50 * nat3) * (len_list ? string))) with
413 [ TickERR s _ ⇒ None ?
414 (* azzeramento tutta RAM tranne dati *)
415 | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
418 Some ? (set_pc_reg HCS08 t
419 (dTest_HCS08_cSort_status t false 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string))
420 (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x3 xC)))).
422 (* dimostrazione senza svolgimento degli stati *)
424 lemma dTest_HCS08_cSort :
425 dTest_HCS08_cSort_aux MEM_TREE dTest_random_32.
426 unfold dTest_HCS08_cSort_aux;
428 [ normalize in ⊢ (%); autobatch ]
433 ndefinition cSortCalc ≝
435 match execute HCS08 MEM_TREE
436 (TickOK ? (dTest_HCS08_cSort_status MEM_TREE true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
437 (((nat256 + nat1) * nat100)+((nat50 * nat3) * (len_list ? string))) with
438 [ TickERR s _ ⇒ None ?
439 | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
443 ndefinition cSortNoCalc ≝
445 Some ? (set_pc_reg HCS08 MEM_TREE
446 (dTest_HCS08_cSort_status MEM_TREE false 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string))
447 (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x3 xC))).
449 ndefinition cSortCalc32 ≝ cSortCalc dTest_random_32.
450 ndefinition cSortCalc64 ≝ cSortCalc dTest_random_64.
451 ndefinition cSortCalc128 ≝ cSortCalc dTest_random_128.
452 ndefinition cSortCalc256 ≝ cSortCalc dTest_random_256.
453 ndefinition cSortCalc512 ≝ cSortCalc dTest_random_512.
454 ndefinition cSortCalc1024 ≝ cSortCalc dTest_random_1024.
455 ndefinition cSortCalc2048 ≝ cSortCalc dTest_random_2048.
456 ndefinition cSortCalc3072 ≝ cSortCalc dTest_random_3072.
458 ndefinition cSortNoCalc32 ≝ cSortNoCalc dTest_random_32.
459 ndefinition cSortNoCalc64 ≝ cSortNoCalc dTest_random_64.
460 ndefinition cSortNoCalc128 ≝ cSortNoCalc dTest_random_128.
461 ndefinition cSortNoCalc256 ≝ cSortNoCalc dTest_random_256.
462 ndefinition cSortNoCalc512 ≝ cSortNoCalc dTest_random_512.
463 ndefinition cSortNoCalc1024 ≝ cSortNoCalc dTest_random_1024.
464 ndefinition cSortNoCalc2048 ≝ cSortNoCalc dTest_random_2048.
465 ndefinition cSortNoCalc3072 ≝ cSortNoCalc dTest_random_3072.
467 (* ********************** *)
468 (* HCS08GB60 numeri aurei *)
469 (* ********************** *)
471 (* versione ridotta, in cui non si riazzerano gli elementi di counters *)
472 ndefinition dTest_HCS08_gNum_source : word16 → (list byte8) ≝
474 let m ≝ HCS08 in source_to_byte8 m (
475 (* BEFORE: A=0x00 HX=0x1A00 PC=0x18BE SP=0x016F Z=1 (I=1) *)
478 static unsigned int result[16]={ 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0 };
479 word result[16] = 0x0100
481 void goldenNumbers(void)
483 unsigned int res_pos=0,tested_num=0,divisor=0;
484 unsigned long int acc=0;
487 (* [0x18BE] AIS #-10 *) (compile m ? AIS (maIMM1 〈xF,x6〉) I) @
488 (* [0x18C0] TSX *) (compile m ? TSX maINH I) @
489 (* [0x18C1] CLR 9,x *) (compile m ? CLR (maIX1 〈x0,x9〉) I) @
490 (* [0x18C3] CLR 8,X *) (compile m ? CLR (maIX1 〈x0,x8〉) I) @
491 (* [0x18C5] CLR 1,X *) (compile m ? CLR (maIX1 〈x0,x1〉) I) @
492 (* [0x18C7] CLR ,X *) (compile m ? CLR maIX0 I) @
493 (* [0x18C8] CLR 3,X *) (compile m ? CLR (maIX1 〈x0,x3〉) I) @
494 (* [0x18CA] CLR 2,X *) (compile m ? CLR (maIX1 〈x0,x2〉) I) @
495 (* [0x18CC] JSR 0x1951 *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈x5,x1〉〉) I) @
498 for(tested_num=1;tested_num<2;tested_num++)
502 (* [0x18CF] STHX 1,SP *) (compile m ? STHX (maSP1 〈x0,x1〉) I) @
503 (* [0x18D2] BRA *+116 ; 0x1946 *) (compile m ? BRA (maIMM1 〈x7,x2〉) I) @
504 (* [0x18D4] BSR *+125 ; 0x1951 *) (compile m ? BSR (maIMM1 〈x7,xB〉) I) @
505 (* [0x18D6] STHX 3,SP *) (compile m ? STHX (maSP1 〈x0,x3〉) I) @
508 for(acc=0,divisor=1;divisor<tested_num;divisor++)
510 if(!(tested_num%divisor))
515 (* [0x18D9] BRA *+61 ; 0x1916 *) (compile m ? BRA (maIMM1 〈x3,xB〉) I) @
516 (* [0x18DB] LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
517 (* [0x18DE] PSHX *) (compile m ? PSHX maINH I) @
518 (* [0x18DF] PSHH *) (compile m ? PSHH maINH I) @
519 (* [0x18E0] LDHX 5,SP *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
520 (* [0x18E3] JSR 0x1A1A *) (compile m ? JSR (maIMM2 〈〈x1,xA〉:〈x1,xA〉〉) I) @
521 (* [0x18E6] AIS #2 *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
522 (* [0x18E8] CPHX #0x0000 *) (compile m ? CPHX (maIMM2 〈〈x0,x0〉:〈x0,x0〉〉) I) @
523 (* [0x18EB] BNE *+33 ; 0x190C *) (compile m ? BNE (maIMM1 〈x1,xF〉) I) @
524 (* [0x18ED] TSX *) (compile m ? TSX maINH I) @
525 (* [0x18EE] LDA 3,X *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
526 (* [0x18F0] LDX 2,X *) (compile m ? LDX (maIX1 〈x0,x2〉) I) @
527 (* [0x18F2] PSHA *) (compile m ? PSHA maINH I) @
528 (* [0x18F3] PSHX *) (compile m ? PSHX maINH I) @
529 (* [0x18F4] CLRA *) (compile m ? CLR maINHA I) @
530 (* [0x18F5] PSHA *) (compile m ? PSHA maINH I) @
531 (* [0x18F6] PSHA *) (compile m ? PSHA maINH I) @
532 (* [0x18F7] TSX *) (compile m ? TSX maINH I) @
533 (* [0x18F8] PSHX *) (compile m ? PSHX maINH I) @
534 (* [0x19F9] PSHH *) (compile m ? PSHH maINH I) @
535 (* [0x18FA] AIX #8 *) (compile m ? AIX (maIMM1 〈x0,x8〉) I) @
536 (* [0x18FC] PSHX *) (compile m ? PSHX maINH I) @
537 (* [0x18FD] PSHH *) (compile m ? PSHH maINH I) @
538 (* [0x18FE] LDHX 3,SP *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
539 (* [0x1901] JSR 0x1A2A *) (compile m ? JSR (maIMM2 〈〈x1,xA〉:〈x2,xA〉〉) I) @
540 (* [0x1904] TSX *) (compile m ? TSX maINH I) @
541 (* [0x1905] AIX #14 *) (compile m ? AIX (maIMM1 〈x0,xE〉) I) @
542 (* [0x1907] JSR 0x1A30 *) (compile m ? JSR (maIMM2 〈〈x1,xA〉:〈x3,x0〉〉) I) @
543 (* [0x190A] AIS #6 *) (compile m ? AIS (maIMM1 〈x0,x6〉) I) @
544 (* [0x190C] STA 0x1800 !COP! *) (compile m ? STA (maDIR2 〈〈x0,xC〉:〈x0,x0〉〉) I) @
545 (* [0x190F] TSX *) (compile m ? TSX maINH I) @
546 (* [0x1910] INC 3,X *) (compile m ? INC (maIX1 〈x0,x3〉) I) @
547 (* [0x1912] BNE *+4 ; 0x1916 *) (compile m ? BNE (maIMM1 〈x0,x2〉) I) @
548 (* [0x1914] INC 2,X *) (compile m ? INC (maIX1 〈x0,x2〉) I) @
549 (* [0x1916] LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
550 (* [0x1919] CPHX 3,SP *) (compile m ? CPHX (maSP1 〈x0,x3〉) I) @
551 (* [0x191C] BHI *-65 ; 0x18DB *) (compile m ? BHI (maIMM1 〈xB,xD〉) I) @
555 { result[res_pos++]=tested_num; }
560 (* [0x191E] CPHX 7,SP *) (compile m ? CPHX (maSP1 〈x0,x7〉) I) @
561 (* [0x1921] BNE *+31 ; 0x1940 *) (compile m ? BNE (maIMM1 〈x1,xD〉) I) @
562 (* [0x1923] LDHX 5,SP *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
563 (* [0x1926] BNE *+26 ; 0x1940 *) (compile m ? BNE (maIMM1 〈x1,x8〉) I) @
564 (* [0x1928] LDHX 9,SP *) (compile m ? LDHX (maSP1 〈x0,x9〉) I) @
565 (* [0x192B] PSHX *) (compile m ? PSHX maINH I) @
566 (* [0x192C] AIX #1 *) (compile m ? AIX (maIMM1 〈x0,x1〉) I) @
567 (* [0x192E] STHX 10,SP *) (compile m ? STHX (maSP1 〈x0,xA〉) I) @
568 (* [0x1931] PULX *) (compile m ? PULX maINH I) @
569 (* [0x1932] LSLX *) (compile m ? ASL maINHX I) @
570 (* [0x1933] LDA 2,SP *) (compile m ? LDA (maSP1 〈x0,x2〉) I) @
571 (* [0x1936] CLRH *) (compile m ? CLR maINHH I) @
572 (* [0x1937] STA 257,X *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x1〉〉) I) @
573 (* [0x193A] LDA 1,SP *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
574 (* [0x193D] STA 256,X *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
575 (* [0x1940] TSX *) (compile m ? TSX maINH I) @
576 (* [0x1941] INC 1,X *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
577 (* [0x1943] BNE *+3 ; 0x1946 *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
578 (* [0x1945] INC ,X *) (compile m ? INC maIX0 I) @
579 (* [0x1946] LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
580 (* [0x1949] CPHX #elems *) (compile m ? CPHX (maIMM2 elems) I) @
581 (* [0x194C] BCS *-120 ; 0x18D4 *) (compile m ? BCS (maIMM1 〈x8,x6〉) I) @
582 (* [0x194E] AIS #10 *) (compile m ? AIS (maIMM1 〈x0,xA〉) I) @
583 (* [0x1950] STOP ->1951 !FINE! *) (compile m ? STOP maINH I) @
584 (* [0x1951] CLRX *) (compile m ? CLR maINHX I) @
585 (* [0x1952] CLRH *) (compile m ? CLR maINHH I) @
586 (* [0x1953] STHX 9,SP *) (compile m ? STHX (maSP1 〈x0,x9〉) I) @
587 (* [0x1956] CLRH *) (compile m ? CLR maINHH I) @
588 (* [0x1957] STHX 7,SP *) (compile m ? STHX (maSP1 〈x0,x7〉) I) @
589 (* [0x195A] INCX *) (compile m ? INC maINHX I) @
590 (* [0x195B] RTS *) (compile m ? RTS maINH I) @
593 static void _PUSH_ARGS_L(void) { ... }
596 (* [0x195C] LDA 3,X *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
597 (* [0x195E] PSHA *) (compile m ? PSHA maINH I) @
598 (* [0x195F] LDA 2,X *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
599 (* [0x1961] PSHA *) (compile m ? PSHA maINH I) @
600 (* [0x1962] LDHX ,X *) (compile m ? LDHX maIX0 I) @
601 (* [0x1964] PSHX *) (compile m ? PSHX maINH I) @
602 (* [0x1965] PSHH *) (compile m ? PSHH maINH I) @
603 (* [0x1966] LDHX 7,SP *) (compile m ? LDHX (maSP1 〈x0,x7〉) I) @
604 (* [0x1969] LDA 3,X *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
605 (* [0x196B] STA 17,SP *) (compile m ? STA (maSP1 〈x1,x1〉) I) @
606 (* [0x196E] LDA 2,X *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
607 (* [0x1970] STA 16,SP *) (compile m ? STA (maSP1 〈x1,x0〉) I) @
608 (* [0x1973] LDHX ,X *) (compile m ? LDHX maIX0 I) @
609 (* [0x1975] STHX 14,SP *) (compile m ? STHX (maSP1 〈x0,xE〉) I) @
610 (* [0x1978] LDHX 5,SP *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
611 (* [0x197B] JMP ,X *) (compile m ? JMP maINHX0ADD I) @
614 static void _ENTER_BINARY_L(void) { ... }
617 (* [0x197C] PSHA *) (compile m ? PSHA maINH I) @
618 (* [0x197D] PSHX *) (compile m ? PSHX maINH I) @
619 (* [0x197E] PSHH *) (compile m ? PSHH maINH I) @
620 (* [0x197F] PSHX *) (compile m ? PSHX maINH I) @
621 (* [0x1980] PSHH *) (compile m ? PSHH maINH I) @
622 (* [0x1981] LDHX 6,SP *) (compile m ? LDHX (maSP1 〈x0,x6〉) I) @
623 (* [0x1984] PSHX *) (compile m ? PSHX maINH I) @
624 (* [0x1985] PSHH *) (compile m ? PSHH maINH I) @
625 (* [0x1986] LDHX 10,SP *) (compile m ? LDHX (maSP1 〈x0,xA〉) I) @
626 (* [0x1989] STHX 8,SP *) (compile m ? STHX (maSP1 〈x0,x8〉) I) @
627 (* [0x198C] LDHX 12,SP *) (compile m ? LDHX (maSP1 〈x0,xC〉) I) @
628 (* [0x198F] JMP 0x195C *) (compile m ? JMP (maIMM2 〈〈x1,x9〉:〈x5,xC〉〉) I) @
631 static void _IDIVMOD (char dummy_sgn, int j, int dummy, int i, ...) { ... }
634 (* [0x1992] TST 4,SP *) (compile m ? TST (maSP1 〈x0,x4〉) I) @
635 (* [0x1995] BNE *+28 ; 0x19B1 *) (compile m ? BNE (maIMM1 〈x1,xA〉) I) @
636 (* [0x1997] TSX *) (compile m ? TSX maINH I) @
637 (* [0x1998] LDA 7,X *) (compile m ? LDA (maIX1 〈x0,x7〉) I) @
638 (* [0x199A] LDX 4,X *) (compile m ? LDX (maIX1 〈x0,x4〉) I) @
639 (* [0x199C] CLRH *) (compile m ? CLR maINHH I) @
640 (* [0x199D] DIV *) (compile m ? DIV maINH I) @
641 (* [0x199E] STA 4,SP *) (compile m ? STA (maSP1 〈x0,x4〉) I) @
642 (* [0x19A1] LDA 9,SP *) (compile m ? LDA (maSP1 〈x0,x9〉) I) @
643 (* [0x19A4] DIV *) (compile m ? DIV maINH I) @
644 (* [0x19A5] STA 5,SP *) (compile m ? STA (maSP1 〈x0,x5〉) I) @
645 (* [0x19A8] CLR 8,SP *) (compile m ? CLR (maSP1 〈x0,x8〉) I) @
646 (* [0x19AB] PSHH *) (compile m ? PSHH maINH I) @
647 (* [0x19AC] PULA *) (compile m ? PULA maINH I) @
648 (* [0x19AD] STA 9,SP *) (compile m ? STA (maSP1 〈x0,x9〉) I) @
649 (* [0x19B0] RTS *) (compile m ? RTS maINH I) @
650 (* [0x19B1] CLRA *) (compile m ? CLR maINHA I) @
651 (* [0x19B2] PSHA *) (compile m ? PSHA maINH I) @
652 (* [0x19B3] LDX #0x08 *) (compile m ? LDX (maIMM1 〈x0,x8〉) I) @
653 (* [0x19B5] CLC *) (compile m ? CLC maINH I) @
654 (* [0x19B6] ROL 10,SP *) (compile m ? ROL (maSP1 〈x0,xA〉) I) @
655 (* [0x19B9] ROL 9,SP *) (compile m ? ROL (maSP1 〈x0,x9〉) I) @
656 (* [0x19BC] ROL 1,SP *) (compile m ? ROL (maSP1 〈x0,x1〉) I) @
657 (* [0x19BF] LDA 5,SP *) (compile m ? LDA (maSP1 〈x0,x5〉) I) @
658 (* [0x19C2] CMP 1,SP *) (compile m ? CMP (maSP1 〈x0,x1〉) I) @
659 (* [0x19C5] BHI *+31 ; 0x19E4 *) (compile m ? BHI (maIMM1 〈x1,xD〉) I) @
660 (* [0x19C7] BNE *+10 ; 0x19D1 *) (compile m ? BNE (maIMM1 〈x0,x8〉) I) @
661 (* [0x19C9] LDA 6,SP *) (compile m ? LDA (maSP1 〈x0,x6〉) I) @
662 (* [0x19CC] CMP 9,SP *) (compile m ? CMP (maSP1 〈x0,x9〉) I) @
663 (* [0x19CF] BHI *+21 ; 0x19E4 *) (compile m ? BHI (maIMM1 〈x1,x3〉) I) @
664 (* [0x19D1] LDA 9,SP *) (compile m ? LDA (maSP1 〈x0,x9〉) I) @
665 (* [0x19D4] SUB 6,SP *) (compile m ? SUB (maSP1 〈x0,x6〉) I) @
666 (* [0x19D7] STA 9,SP *) (compile m ? STA (maSP1 〈x0,x9〉) I) @
667 (* [0x19DA] LDA 1,SP *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
668 (* [0x19DD] SBC 5,SP *) (compile m ? SBC (maSP1 〈x0,x5〉) I) @
669 (* [0x19E0] STA 1,SP *) (compile m ? STA (maSP1 〈x0,x1〉) I) @
670 (* [0x19E3] SEC *) (compile m ? SEC maINH I) @
671 (* [0x19E4] DBNZX *-46 ; 0x19B6 *) (compile m ? DBNZ (maINHX_and_IMM1 〈xD,x0〉) I) @
672 (* [0x19E6] LDA 10,SP *) (compile m ? LDA (maSP1 〈x0,xA〉) I) @
673 (* [0x19E9] ROLA *) (compile m ? ROL maINHA I) @
674 (* [0x19EA] STA 6,SP *) (compile m ? STA (maSP1 〈x0,x6〉) I) @
675 (* [0x19ED] LDA 9,SP *) (compile m ? LDA (maSP1 〈x0,x9〉) I) @
676 (* [0x19F0] STA 10,SP *) (compile m ? STA (maSP1 〈x0,xA〉) I) @
677 (* [0x19F3] PULA *) (compile m ? PULA maINH I) @
678 (* [0x19F4] STA 8,SP *) (compile m ? STA (maSP1 〈x0,x8〉) I) @
679 (* [0x19F7] CLR 4,SP *) (compile m ? CLR (maSP1 〈x0,x4〉) I) @
680 (* [0x19FA] RTS *) (compile m ? RTS maINH I) @
683 static void _LADD_k_is_k_plus_j(_PARAM_BINARY_L) { ... }
686 (* [0x19FB] TSX *) (compile m ? TSX maINH I) @
687 (* [0x19FC] LDA 18,X *) (compile m ? LDA (maIX1 〈x1,x2〉) I) @
688 (* [0x19FE] ADD 5,X *) (compile m ? ADD (maIX1 〈x0,x5〉) I) @
689 (* [0x1A00] STA 18,X *) (compile m ? STA (maIX1 〈x1,x2〉) I) @
690 (* [0x1A02] LDA 17,X *) (compile m ? LDA (maIX1 〈x1,x1〉) I) @
691 (* [0x1A04] ADC 4,X *) (compile m ? ADC (maIX1 〈x0,x4〉) I) @
692 (* [0x1A06] STA 17,X *) (compile m ? STA (maIX1 〈x1,x1〉) I) @
693 (* [0x1A08] LDA 16,X *) (compile m ? LDA (maIX1 〈x1,x0〉) I) @
694 (* [0x1A0A] ADC 3,X *) (compile m ? ADC (maIX1 〈x0,x3〉) I) @
695 (* [0x1A0C] STA 16,X *) (compile m ? STA (maIX1 〈x1,x0〉) I) @
696 (* [0x1A0E] LDA 15,X *) (compile m ? LDA (maIX1 〈x0,xF〉) I) @
697 (* [0x1A10] ADC 2,X *) (compile m ? ADC (maIX1 〈x0,x2〉) I) @
698 (* [0x1A12] STA 15,X *) (compile m ? STA (maIX1 〈x0,xF〉) I) @
699 (* [0x1A14] AIS #10 *) (compile m ? AIS (maIMM1 〈x0,xA〉) I) @
700 (* [0x1A16] PULH *) (compile m ? PULH maINH I) @
701 (* [0x1A17] PULX *) (compile m ? PULX maINH I) @
702 (* [0x1A18] PULA *) (compile m ? PULA maINH I) @
703 (* [0x1A19] RTS *) (compile m ? RTS maINH I) @
706 void _IMODU_STAR08(int i, ...) { ... }
709 (* [0x1A1A] AIS #-2 *) (compile m ? AIS (maIMM1 〈xF,xE〉) I) @
710 (* [0x1A1C] STHX 1,SP *) (compile m ? STHX (maSP1 〈x0,x1〉) I) @
711 (* [0x1A1F] PSHA *) (compile m ? PSHA maINH I) @
712 (* [0x1A20] JSR 0x1992 *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈x9,x2〉〉) I) @
713 (* [0x1A23] PULA *) (compile m ? PULA maINH I) @
714 (* [0x1A24] AIS #2 *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
715 (* [0x1A26] LDHX 3,SP *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
716 (* [0x1A29] RTS *) (compile m ? RTS maINH I) @
719 void _LADD(void) { ... }
722 (* [0x1A2A] JSR 0x197C *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈x7,xC〉〉) I) @
723 (* [0x1A2D] JSR 0x19FB *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈xF,xB〉〉) I) @
726 void _POP32(void) { ... }
729 (* [0x1A30] PSHA *) (compile m ? PSHA maINH I) @
730 (* [0x1A31] LDA 4,SP *) (compile m ? LDA (maSP1 〈x0,x4〉) I) @
731 (* [0x1A34] STA ,X *) (compile m ? STA maIX0 I) @
732 (* [0x1A35] LDA 5,SP *) (compile m ? LDA (maSP1 〈x0,x5〉) I) @
733 (* [0x1A38] STA 1,X *) (compile m ? STA (maIX1 〈x0,x1〉) I) @
734 (* [0x1A3A] LDA 6,SP *) (compile m ? LDA (maSP1 〈x0,x6〉) I) @
735 (* [0x1A3D] STA 2,X *) (compile m ? STA (maIX1 〈x0,x2〉) I) @
736 (* [0x1A3F] LDA 7,SP *) (compile m ? LDA (maSP1 〈x0,x7〉) I) @
737 (* [0x1A42] STA 3,X *) (compile m ? STA (maIX1 〈x0,x3〉) I) @
738 (* [0x1A44] PULA *) (compile m ? PULA maINH I) @
739 (* [0x1A45] PULH *) (compile m ? PULH maINH I) @
740 (* [0x1A46] PULX *) (compile m ? PULX maINH I) @
741 (* [0x1A47] AIS #4 *) (compile m ? AIS (maIMM1 〈x0,x4〉) I) @
742 (* [0x1A49] JMP ,X *) (compile m ? JMP maINHX0ADD I)
744 (* attraverso simulazione in CodeWarrior si puo' enunciare che dopo
745 80+(65*n*(n+1)*(n+2))/6 si sara' entrati in stato STOP corrispondente
746 AFTER: HX=num PC=0x1951 I=0 *)
749 (* creazione del processore+caricamento+impostazione registri *)
750 ndefinition dTest_HCS08_gNum_status ≝
759 setweak_i_flag HCS08 t (* I<-I_op *)
760 (set_acc_8_low_reg HCS08 t (* A<-A_op *)
761 (set_z_flag HCS08 t (* Z<-true *)
762 (setweak_sp_reg HCS08 t (* SP<-0x016F *)
763 (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
764 (set_pc_reg HCS08 t (* PC<-PC_op *)
765 (start_of_mcu_version_HCS08
767 (load_from_source_at t (* carica data in RAM:dTest_HCS08_RAM *)
768 (load_from_source_at t (zero_memory t) (* carica source in ROM:addr *)
769 (dTest_HCS08_cSort_source elems) addr)
770 data dTest_HCS08_RAM)
771 (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08GB60) t)
772 (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
773 false false false false false false) (* non deterministici tutti a 0 *)
776 (mk_word16 (mk_byte8 x0 x1) (mk_byte8 x6 xF)))
781 (* NUMERI AUREI: Somma divisori(x)=x, fino a 0xFFFF sono 6/28/496/8128 *)
782 ndefinition dTest_HCS08_gNum_aurei ≝
783 λnum:word16.match gt_w16 num 〈〈x1,xF〉:〈xC,x0〉〉 with
784 [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x1,xC〉 ; 〈x0,x1〉 ; 〈xF,x0〉 ; 〈x1,xF〉 ; 〈xC,x0〉 ]
785 | false ⇒ match gt_w16 num 〈〈x0,x1〉:〈xF,x0〉〉 with
786 [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x1,xC〉 ; 〈x0,x1〉 ; 〈xF,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
787 | false ⇒ match gt_w16 num 〈〈x0,x0〉:〈x1,xC〉〉 with
788 [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x1,xC〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
789 | false ⇒ match gt_w16 num 〈〈x0,x0〉:〈x0,x6〉〉 with
790 [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
791 | false ⇒ [ 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
795 ] @ [ 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉
796 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉
797 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ].
799 (* esecuzione execute k*(n+2) *)
800 nlet rec dTest_HCS08_gNum_execute1 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
802 [ TickERR s' error ⇒ TickERR ? s' error
803 | TickSUSP s' susp ⇒ TickSUSP ? s' susp
804 | TickOK s' ⇒ match n with
806 | S n' ⇒ dTest_HCS08_gNum_execute1 m t (execute m t (TickOK ? s') (ntot + nat2)) n' ntot ]
809 (* esecuzione execute k*(n+1)*(n+2) *)
810 nlet rec dTest_HCS08_gNum_execute2 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
812 [ TickERR s' error ⇒ TickERR ? s' error
813 | TickSUSP s' susp ⇒ TickSUSP ? s' susp
814 | TickOK s' ⇒ match n with
816 | S n' ⇒ dTest_HCS08_gNum_execute2 m t (dTest_HCS08_gNum_execute1 m t (TickOK ? s') (ntot + nat1) ntot) n' ntot ]
819 (* esecuzione execute k*n*(n+1)*(n+2) *)
820 nlet rec dTest_HCS08_gNum_execute3 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
822 [ TickERR s' error ⇒ TickERR ? s' error
823 | TickSUSP s' susp ⇒ TickSUSP ? s' susp
824 | TickOK s' ⇒ match n with
826 | S n' ⇒ dTest_HCS08_gNum_execute3 m t (dTest_HCS08_gNum_execute2 m t (TickOK ? s') ntot ntot) n' ntot ]
829 (* esecuzione execute 80+11*n*(n+1)*(n+2) *)
830 ndefinition dTest_HCS08_gNum_execute4 ≝
831 λm:mcu_type.λt:memory_impl.λs:tick_result (any_status m t).λntot:nat.
833 [ TickERR s' error ⇒ TickERR ? s' error
834 | TickSUSP s' susp ⇒ TickSUSP ? s' susp
835 | TickOK s' ⇒ execute m t (dTest_HCS08_gNum_execute3 m t (TickOK ? s') nat11 ntot) nat80
838 (* parametrizzazione dell'enunciato del teorema parziale *)
839 nlemma dTest_HCS08_gNum_aux ≝
840 λt:memory_impl.λnum:word16.
841 (* 2) match di esecuzione su tempo in forma di upperbound *)
842 match dTest_HCS08_gNum_execute4 HCS08 t
843 (TickOK ? (dTest_HCS08_gNum_status t true 〈x0,x0〉 〈〈x1,xA〉:〈x0,x0〉〉 〈〈x1,x8〉:〈xB,xE〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num dTest_zeros))
844 (* tempo di esecuzione 80+11*n*(n+1)*(n+2) *)
845 (nat_of_w16 num) with
846 [ TickERR s _ ⇒ None ?
847 (* azzeramento tutta RAM tranne dati *)
848 | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
851 Some ? (dTest_HCS08_gNum_status t false 〈x0,x0〉 num 〈〈x1,x9〉:〈x5,x1〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num (dTest_HCS08_gNum_aurei num)).
853 ndefinition gNumCalc ≝
855 match dTest_HCS08_gNum_execute4 HCS08 MEM_TREE
856 (TickOK ? (dTest_HCS08_gNum_status MEM_TREE true 〈x0,x0〉 〈〈x1,xA〉:〈x0,x0〉〉 〈〈x1,x8〉:〈xB,xE〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num dTest_zeros))
857 (nat_of_w16 num) with
858 [ TickERR s _ ⇒ None ?
859 | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
863 ndefinition gNumNoCalc ≝
865 Some ? (dTest_HCS08_gNum_status MEM_TREE false 〈x0,x0〉 num 〈〈x1,x9〉:〈x5,x1〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num (dTest_HCS08_gNum_aurei num)).
867 ndefinition gNumCalc1 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x1〉〉.
868 ndefinition gNumCalc2 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x2〉〉.
869 ndefinition gNumCalc5 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x5〉〉.
870 ndefinition gNumCalc10 ≝ gNumCalc 〈〈x0,x0〉:〈x0,xA〉〉.
871 ndefinition gNumCalc20 ≝ gNumCalc 〈〈x0,x0〉:〈x1,x4〉〉.
872 ndefinition gNumCalc50 ≝ gNumCalc 〈〈x0,x0〉:〈x3,x2〉〉.
873 ndefinition gNumCalc100 ≝ gNumCalc 〈〈x0,x0〉:〈x6,x4〉〉.
874 ndefinition gNumCalc250 ≝ gNumCalc 〈〈x0,x0〉:〈xF,xA〉〉.
875 ndefinition gNumCalc500 ≝ gNumCalc 〈〈x0,x1〉:〈xF,x4〉〉.
876 ndefinition gNumCalc1000 ≝ gNumCalc 〈〈x0,x3〉:〈xE,x8〉〉.
878 ndefinition gNumNoCalc1 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x1〉〉.
879 ndefinition gNumNoCalc2 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x2〉〉.
880 ndefinition gNumNoCalc5 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x5〉〉.
881 ndefinition gNumNoCalc10 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,xA〉〉.
882 ndefinition gNumNoCalc20 ≝ gNumNoCalc 〈〈x0,x0〉:〈x1,x4〉〉.
883 ndefinition gNumNoCalc50 ≝ gNumNoCalc 〈〈x0,x0〉:〈x3,x2〉〉.
884 ndefinition gNumNoCalc100 ≝ gNumNoCalc 〈〈x0,x0〉:〈x6,x4〉〉.
885 ndefinition gNumNoCalc250 ≝ gNumNoCalc 〈〈x0,x0〉:〈xF,xA〉〉.
886 ndefinition gNumNoCalc500 ≝ gNumNoCalc 〈〈x0,x1〉:〈xF,x4〉〉.
887 ndefinition gNumNoCalc1000 ≝ gNumNoCalc 〈〈x0,x3〉:〈xE,x8〉〉.