19 open Hints_declaration
88 (Nat.nat, (Nat.nat, Assembly.jump_length) Types.prod
89 BitVectorTrie.bitVectorTrie) Types.prod
92 Assembly.jump_length -> Assembly.jump_length -> Bool.bool **)
95 | Assembly.Short_jump ->
97 | Assembly.Short_jump -> Bool.True
98 | Assembly.Absolute_jump -> Bool.False
99 | Assembly.Long_jump -> Bool.False)
100 | Assembly.Absolute_jump ->
102 | Assembly.Short_jump -> Bool.False
103 | Assembly.Absolute_jump -> Bool.True
104 | Assembly.Long_jump -> Bool.False)
105 | Assembly.Long_jump ->
107 | Assembly.Short_jump -> Bool.False
108 | Assembly.Absolute_jump -> Bool.False
109 | Assembly.Long_jump -> Bool.True)
111 (** val expand_relative_jump_internal_unsafe :
112 Assembly.jump_length -> (ASM.subaddressing_mode -> ASM.subaddressing_mode
113 ASM.preinstruction) -> ASM.instruction List.list **)
114 let expand_relative_jump_internal_unsafe jmp_len i =
116 | Assembly.Short_jump ->
117 List.Cons ((ASM.RealInstruction
119 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
120 (Nat.S Nat.O)))))))))))), List.Nil)
121 | Assembly.Absolute_jump -> List.Nil
122 | Assembly.Long_jump ->
123 List.Cons ((ASM.RealInstruction
125 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
126 (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S Nat.O)))))),
127 (List.Cons ((ASM.SJMP (ASM.RELATIVE
128 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
129 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S Nat.O)))))),
130 (List.Cons ((ASM.LJMP (ASM.ADDR16
131 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
132 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
133 Nat.O))))))))))))))))))), List.Nil)))))
135 (** val strip_target :
136 ASM.identifier ASM.preinstruction -> (ASM.subaddressing_mode ->
137 ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum **)
138 let strip_target = function
139 | ASM.ADD (arg1, arg2) ->
140 Types.Inr (ASM.RealInstruction (ASM.ADD (arg1, arg2)))
141 | ASM.ADDC (arg1, arg2) ->
142 Types.Inr (ASM.RealInstruction (ASM.ADDC (arg1, arg2)))
143 | ASM.SUBB (arg1, arg2) ->
144 Types.Inr (ASM.RealInstruction (ASM.SUBB (arg1, arg2)))
145 | ASM.INC arg -> Types.Inr (ASM.RealInstruction (ASM.INC arg))
146 | ASM.DEC arg -> Types.Inr (ASM.RealInstruction (ASM.DEC arg))
147 | ASM.MUL (arg1, arg2) ->
148 Types.Inr (ASM.RealInstruction (ASM.MUL (arg1, arg2)))
149 | ASM.DIV (arg1, arg2) ->
150 Types.Inr (ASM.RealInstruction (ASM.DIV (arg1, arg2)))
151 | ASM.DA arg -> Types.Inr (ASM.RealInstruction (ASM.DA arg))
152 | ASM.JC x -> Types.Inl (fun x0 -> ASM.JC x0)
153 | ASM.JNC x -> Types.Inl (fun x0 -> ASM.JNC x0)
154 | ASM.JB (baddr, x) -> Types.Inl (fun x0 -> ASM.JB (baddr, x0))
155 | ASM.JNB (baddr, x) -> Types.Inl (fun x0 -> ASM.JNB (baddr, x0))
156 | ASM.JBC (baddr, x) -> Types.Inl (fun x0 -> ASM.JBC (baddr, x0))
157 | ASM.JZ x -> Types.Inl (fun x0 -> ASM.JZ x0)
158 | ASM.JNZ x -> Types.Inl (fun x0 -> ASM.JNZ x0)
159 | ASM.CJNE (addr, x) -> Types.Inl (fun x0 -> ASM.CJNE (addr, x0))
160 | ASM.DJNZ (addr, x) -> Types.Inl (fun x0 -> ASM.DJNZ (addr, x0))
161 | ASM.ANL arg -> Types.Inr (ASM.RealInstruction (ASM.ANL arg))
162 | ASM.ORL arg -> Types.Inr (ASM.RealInstruction (ASM.ORL arg))
163 | ASM.XRL arg -> Types.Inr (ASM.RealInstruction (ASM.XRL arg))
164 | ASM.CLR arg -> Types.Inr (ASM.RealInstruction (ASM.CLR arg))
165 | ASM.CPL arg -> Types.Inr (ASM.RealInstruction (ASM.CPL arg))
166 | ASM.RL arg -> Types.Inr (ASM.RealInstruction (ASM.RL arg))
167 | ASM.RLC arg -> Types.Inr (ASM.RealInstruction (ASM.RLC arg))
168 | ASM.RR arg -> Types.Inr (ASM.RealInstruction (ASM.RR arg))
169 | ASM.RRC arg -> Types.Inr (ASM.RealInstruction (ASM.RRC arg))
170 | ASM.SWAP arg -> Types.Inr (ASM.RealInstruction (ASM.SWAP arg))
171 | ASM.MOV arg -> Types.Inr (ASM.RealInstruction (ASM.MOV arg))
172 | ASM.MOVX arg -> Types.Inr (ASM.RealInstruction (ASM.MOVX arg))
173 | ASM.SETB arg -> Types.Inr (ASM.RealInstruction (ASM.SETB arg))
174 | ASM.PUSH arg -> Types.Inr (ASM.RealInstruction (ASM.PUSH arg))
175 | ASM.POP arg -> Types.Inr (ASM.RealInstruction (ASM.POP arg))
176 | ASM.XCH (arg1, arg2) ->
177 Types.Inr (ASM.RealInstruction (ASM.XCH (arg1, arg2)))
178 | ASM.XCHD (arg1, arg2) ->
179 Types.Inr (ASM.RealInstruction (ASM.XCHD (arg1, arg2)))
180 | ASM.RET -> Types.Inr (ASM.RealInstruction ASM.RET)
181 | ASM.RETI -> Types.Inr (ASM.RealInstruction ASM.RETI)
182 | ASM.NOP -> Types.Inr (ASM.RealInstruction ASM.NOP)
183 | ASM.JMP dst -> Types.Inr (ASM.RealInstruction (ASM.JMP dst))
185 (** val expand_relative_jump_unsafe :
186 Assembly.jump_length -> ASM.identifier ASM.preinstruction ->
187 ASM.instruction List.list **)
188 let expand_relative_jump_unsafe jmp_len i =
189 match strip_target i with
190 | Types.Inl jmp -> expand_relative_jump_internal_unsafe jmp_len jmp
191 | Types.Inr instr -> List.Cons (instr, List.Nil)
193 (** val expand_pseudo_instruction_unsafe :
194 Assembly.jump_length -> ASM.pseudo_instruction -> ASM.instruction
196 let expand_pseudo_instruction_unsafe jmp_len = function
197 | ASM.Instruction instr -> expand_relative_jump_unsafe jmp_len instr
198 | ASM.Comment comment -> List.Nil
199 | ASM.Cost cost -> List.Cons ((ASM.RealInstruction ASM.NOP), List.Nil)
202 | Assembly.Short_jump ->
203 List.Cons ((ASM.SJMP (ASM.RELATIVE
204 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
205 (Nat.S Nat.O))))))))))), List.Nil)
206 | Assembly.Absolute_jump ->
207 List.Cons ((ASM.AJMP (ASM.ADDR11
208 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
209 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))), List.Nil)
210 | Assembly.Long_jump ->
211 List.Cons ((ASM.LJMP (ASM.ADDR16
212 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
213 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
214 Nat.O))))))))))))))))))), List.Nil))
215 | ASM.Jnz (acc, dst1, dst2) ->
216 List.Cons ((ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE
217 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
218 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S Nat.O))))))),
219 (List.Cons ((ASM.LJMP (ASM.ADDR16
220 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
221 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
222 Nat.O))))))))))))))))))), (List.Cons ((ASM.LJMP (ASM.ADDR16
223 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
224 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
225 Nat.O))))))))))))))))))), List.Nil)))))
228 | Assembly.Short_jump -> List.Nil
229 | Assembly.Absolute_jump ->
230 List.Cons ((ASM.ACALL (ASM.ADDR11
231 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
232 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))), List.Nil)
233 | Assembly.Long_jump ->
234 List.Cons ((ASM.LCALL (ASM.ADDR16
235 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
236 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
237 Nat.O))))))))))))))))))), List.Nil))
238 | ASM.Mov (d, trgt, off) ->
241 let address = ASM.DATA16
242 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
243 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
244 Nat.O)))))))))))))))))
246 List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
247 (Types.Inr { Types.fst = ASM.DPTR; Types.snd = address }))))), List.Nil)
250 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
251 (Nat.S Nat.O)))))))))
253 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
254 ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
255 Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr,
256 Vector.VEmpty)))))) pr.Types.fst with
258 (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
259 (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b1);
260 Types.snd = v })))))), List.Nil))
261 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
262 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
264 (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
265 (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
266 (ASM.REGISTER r); Types.snd = v }))))))), List.Nil))
268 (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
269 (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst =
270 ASM.ACC_A; Types.snd = v }))))))), List.Nil))
271 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
272 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
273 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
274 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
275 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
276 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
277 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
278 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
279 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
280 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
281 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
282 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
283 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
284 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
286 (** val instruction_size_jmplen :
287 Assembly.jump_length -> ASM.pseudo_instruction -> Nat.nat **)
288 let instruction_size_jmplen jmp_len i =
290 List.map Assembly.assembly1 (expand_pseudo_instruction_unsafe jmp_len i)
292 let flattened = List.flatten mapped in
293 let pc_len = List.length flattened in pc_len
296 Assembly.jump_length -> Assembly.jump_length -> Assembly.jump_length **)
297 let max_length j1 j2 =
299 | Assembly.Short_jump ->
301 | Assembly.Short_jump -> Assembly.Short_jump
302 | Assembly.Absolute_jump -> Assembly.Long_jump
303 | Assembly.Long_jump -> Assembly.Long_jump)
304 | Assembly.Absolute_jump ->
306 | Assembly.Short_jump -> Assembly.Long_jump
307 | Assembly.Absolute_jump -> Assembly.Absolute_jump
308 | Assembly.Long_jump -> Assembly.Long_jump)
309 | Assembly.Long_jump -> Assembly.Long_jump
312 Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum **)
315 | Assembly.Short_jump ->
317 | Assembly.Short_jump -> Types.Inr __
318 | Assembly.Absolute_jump -> Types.Inl __
319 | Assembly.Long_jump -> Types.Inl __)
320 | Assembly.Absolute_jump ->
322 | Assembly.Short_jump -> Types.Inr __
323 | Assembly.Absolute_jump -> Types.Inr __
324 | Assembly.Long_jump -> Types.Inl __)
325 | Assembly.Long_jump ->
327 | Assembly.Short_jump -> Types.Inr __
328 | Assembly.Absolute_jump -> Types.Inr __
329 | Assembly.Long_jump -> Types.Inr __)
331 (** val dec_eq_jump_length :
332 Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum **)
333 let dec_eq_jump_length a b =
335 | Assembly.Short_jump ->
337 | Assembly.Short_jump -> Types.Inl __
338 | Assembly.Absolute_jump -> Types.Inr __
339 | Assembly.Long_jump -> Types.Inr __)
340 | Assembly.Absolute_jump ->
342 | Assembly.Short_jump -> Types.Inr __
343 | Assembly.Absolute_jump -> Types.Inl __
344 | Assembly.Long_jump -> Types.Inr __)
345 | Assembly.Long_jump ->
347 | Assembly.Short_jump -> Types.Inr __
348 | Assembly.Absolute_jump -> Types.Inr __
349 | Assembly.Long_jump -> Types.Inl __)
351 (** val create_label_map :
352 ASM.labelled_instruction List.list -> Fetch.label_map Types.sig0 **)
353 let create_label_map program =
354 (Fetch.create_label_cost_map program).Types.fst
356 (** val select_reljump_length :
357 Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
358 -> Nat.nat -> Assembly.jump_length **)
359 let select_reljump_length labels old_sigma inc_sigma ppc lbl ins_len =
360 let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
362 let { Types.fst = src; Types.snd = dest } =
363 match Nat.leb paddr ppc with
365 let pc = inc_sigma.Types.fst in
367 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
368 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
369 (Nat.S Nat.O))))))))))))))))
370 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
371 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
372 (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
373 { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
376 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
377 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
378 Nat.O)))))))))))))))) (Nat.plus pc ins_len)); Types.snd =
379 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
380 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
381 Nat.O)))))))))))))))) addr) }
384 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
385 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
386 (Nat.S Nat.O))))))))))))))))
387 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
388 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
389 (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
390 { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
393 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
394 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
395 (Nat.S Nat.O))))))))))))))))
396 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
397 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
398 (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
399 { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
402 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
403 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
404 Nat.O)))))))))))))))) (Nat.plus pc ins_len)); Types.snd =
405 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
406 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
407 Nat.O)))))))))))))))) addr) }
409 let { Types.fst = sj_possible; Types.snd = disp } =
410 Assembly.short_jump_cond src dest
412 (match sj_possible with
413 | Bool.True -> Assembly.Short_jump
414 | Bool.False -> Assembly.Long_jump)
416 (** val select_call_length :
417 Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
418 -> Assembly.jump_length **)
419 let select_call_length labels old_sigma inc_sigma ppc lbl =
420 let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
422 let { Types.fst = src; Types.snd = dest } =
423 match Nat.leb paddr ppc with
425 let pc = inc_sigma.Types.fst in
427 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
428 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
429 (Nat.S Nat.O))))))))))))))))
430 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
431 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
432 (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
433 { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
436 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
437 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
438 Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
440 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
441 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
442 Nat.O)))))))))))))))) addr) }
445 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
446 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
447 (Nat.S Nat.O))))))))))))))))
448 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
449 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
450 (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
451 { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
454 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
455 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
456 (Nat.S Nat.O))))))))))))))))
457 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
458 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
459 (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
460 { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
463 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
464 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
465 Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
467 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
468 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
469 Nat.O)))))))))))))))) addr) }
471 let { Types.fst = aj_possible; Types.snd = disp } =
472 Assembly.absolute_jump_cond src dest
474 (match aj_possible with
475 | Bool.True -> Assembly.Absolute_jump
476 | Bool.False -> Assembly.Long_jump)
478 (** val select_jump_length :
479 Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
480 -> Assembly.jump_length **)
481 let select_jump_length labels old_sigma inc_sigma ppc lbl =
482 let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
484 let { Types.fst = src; Types.snd = dest } =
485 match Nat.leb paddr ppc with
487 let pc = inc_sigma.Types.fst in
489 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
490 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
491 (Nat.S Nat.O))))))))))))))))
492 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
493 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
494 (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
495 { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
498 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
499 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
500 Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
502 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
503 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
504 Nat.O)))))))))))))))) addr) }
507 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
508 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
509 (Nat.S Nat.O))))))))))))))))
510 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
511 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
512 (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
513 { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
516 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
517 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
518 (Nat.S Nat.O))))))))))))))))
519 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
520 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
521 (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
522 { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
525 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
526 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
527 Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
529 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
530 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
531 Nat.O)))))))))))))))) addr) }
533 let { Types.fst = sj_possible; Types.snd = disp } =
534 Assembly.short_jump_cond src dest
536 (match sj_possible with
537 | Bool.True -> Assembly.Short_jump
538 | Bool.False -> select_call_length labels old_sigma inc_sigma ppc lbl)
540 (** val destination_of :
541 ASM.identifier ASM.preinstruction -> ASM.identifier Types.option **)
542 let destination_of = function
543 | ASM.ADD (x, x0) -> Types.None
544 | ASM.ADDC (x, x0) -> Types.None
545 | ASM.SUBB (x, x0) -> Types.None
546 | ASM.INC x -> Types.None
547 | ASM.DEC x -> Types.None
548 | ASM.MUL (x, x0) -> Types.None
549 | ASM.DIV (x, x0) -> Types.None
550 | ASM.DA x -> Types.None
551 | ASM.JC j -> Types.Some j
552 | ASM.JNC j -> Types.Some j
553 | ASM.JB (x, j) -> Types.Some j
554 | ASM.JNB (x, j) -> Types.Some j
555 | ASM.JBC (x, j) -> Types.Some j
556 | ASM.JZ j -> Types.Some j
557 | ASM.JNZ j -> Types.Some j
558 | ASM.CJNE (x, j) -> Types.Some j
559 | ASM.DJNZ (x, j) -> Types.Some j
560 | ASM.ANL x -> Types.None
561 | ASM.ORL x -> Types.None
562 | ASM.XRL x -> Types.None
563 | ASM.CLR x -> Types.None
564 | ASM.CPL x -> Types.None
565 | ASM.RL x -> Types.None
566 | ASM.RLC x -> Types.None
567 | ASM.RR x -> Types.None
568 | ASM.RRC x -> Types.None
569 | ASM.SWAP x -> Types.None
570 | ASM.MOV x -> Types.None
571 | ASM.MOVX x -> Types.None
572 | ASM.SETB x -> Types.None
573 | ASM.PUSH x -> Types.None
574 | ASM.POP x -> Types.None
575 | ASM.XCH (x, x0) -> Types.None
576 | ASM.XCHD (x, x0) -> Types.None
577 | ASM.RET -> Types.None
578 | ASM.RETI -> Types.None
579 | ASM.NOP -> Types.None
580 | ASM.JMP x -> Types.None
582 (** val length_of : ASM.identifier ASM.preinstruction -> Nat.nat **)
583 let length_of = function
584 | ASM.ADD (x, x0) -> Nat.O
585 | ASM.ADDC (x, x0) -> Nat.O
586 | ASM.SUBB (x, x0) -> Nat.O
589 | ASM.MUL (x, x0) -> Nat.O
590 | ASM.DIV (x, x0) -> Nat.O
592 | ASM.JC j -> Nat.S (Nat.S Nat.O)
593 | ASM.JNC j -> Nat.S (Nat.S Nat.O)
594 | ASM.JB (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
595 | ASM.JNB (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
596 | ASM.JBC (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
597 | ASM.JZ j -> Nat.S (Nat.S Nat.O)
598 | ASM.JNZ j -> Nat.S (Nat.S Nat.O)
599 | ASM.CJNE (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
601 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
602 ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)))) x with
603 | ASM.DIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
604 | ASM.INDIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
605 | ASM.EXT_INDIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
606 | ASM.REGISTER x0 -> Nat.S (Nat.S Nat.O)
607 | ASM.ACC_A -> Nat.S (Nat.S (Nat.S Nat.O))
608 | ASM.ACC_B -> Nat.S (Nat.S (Nat.S Nat.O))
609 | ASM.DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
610 | ASM.DATA x0 -> Nat.S (Nat.S (Nat.S Nat.O))
611 | ASM.DATA16 x0 -> Nat.S (Nat.S (Nat.S Nat.O))
612 | ASM.ACC_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
613 | ASM.ACC_PC -> Nat.S (Nat.S (Nat.S Nat.O))
614 | ASM.EXT_INDIRECT_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
615 | ASM.INDIRECT_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
616 | ASM.CARRY -> Nat.S (Nat.S (Nat.S Nat.O))
617 | ASM.BIT_ADDR x0 -> Nat.S (Nat.S (Nat.S Nat.O))
618 | ASM.N_BIT_ADDR x0 -> Nat.S (Nat.S (Nat.S Nat.O))
619 | ASM.RELATIVE x0 -> Nat.S (Nat.S (Nat.S Nat.O))
620 | ASM.ADDR11 x0 -> Nat.S (Nat.S (Nat.S Nat.O))
621 | ASM.ADDR16 x0 -> Nat.S (Nat.S (Nat.S Nat.O)))
631 | ASM.SWAP x -> Nat.O
633 | ASM.MOVX x -> Nat.O
634 | ASM.SETB x -> Nat.O
635 | ASM.PUSH x -> Nat.O
637 | ASM.XCH (x, x0) -> Nat.O
638 | ASM.XCHD (x, x0) -> Nat.O
644 (** val jump_expansion_step_instruction :
645 Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
646 ASM.preinstruction -> Assembly.jump_length Types.option **)
647 let jump_expansion_step_instruction labels old_sigma inc_sigma ppc i =
648 let ins_len = length_of i in
649 (match destination_of i with
650 | Types.None -> Types.None
653 (select_reljump_length labels old_sigma inc_sigma ppc j ins_len))
655 (** val jump_expansion_start :
656 ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
657 ppc_pc_map Types.option Types.sig0 **)
658 let jump_expansion_start program labels =
659 (let { Types.fst = ignore; Types.snd = final_policy } =
661 (FoldStuff.foldl_strong (Types.pi1 program)
662 (fun prefix x tl _ acc_pol ->
663 (let { Types.fst = acc; Types.snd = p } = Types.pi1 acc_pol in
665 let { Types.fst = pc; Types.snd = sigma } = p in
666 let { Types.fst = label; Types.snd = instr } = x in
667 let isize = instruction_size_jmplen Assembly.Short_jump instr in
669 Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
670 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
671 (Nat.S Nat.O)))))))))))))))) acc
673 { Types.fst = sacc; Types.snd = { Types.fst = (Nat.plus pc isize);
675 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
676 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
677 (Nat.S Nat.O)))))))))))))))) sacc { Types.fst =
678 (Nat.plus pc isize); Types.snd = Assembly.Short_jump } sigma) } }))
680 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
681 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
682 Nat.O))))))))))))))))); Types.snd = { Types.fst = Nat.O;
684 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
685 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
686 (Nat.S Nat.O))))))))))))))))
687 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
688 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
689 (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O;
690 Types.snd = Assembly.Short_jump } (BitVectorTrie.Stub (Nat.S
691 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
692 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } })
695 (match Util.gtb final_policy.Types.fst
696 (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
697 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
698 (Nat.S (Nat.S Nat.O))))))))))))))))) with
699 | Bool.True -> (fun _ -> Types.None)
700 | Bool.False -> (fun _ -> Types.Some final_policy)) __)) __