source: driver/extracted/policyFront.ml @ 3106

Last change on this file since 3106 was 3106, checked in by sacerdot, 7 years ago

New extraction.

File size: 27.8 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open Status
32
33open BitVectorTrie
34
35open String
36
37open Integers
38
39open AST
40
41open LabelledObjects
42
43open Proper
44
45open PositiveMap
46
47open Deqsets
48
49open ErrorMessages
50
51open PreIdentifiers
52
53open Errors
54
55open Lists
56
57open Positive
58
59open Identifiers
60
61open CostLabel
62
63open ASM
64
65open Exp
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open FoldStuff
78
79open BitVector
80
81open Arithmetic
82
83open Fetch
84
85open Assembly
86
87type ppc_pc_map =
88  (Nat.nat, (Nat.nat, Assembly.jump_length) Types.prod
89  BitVectorTrie.bitVectorTrie) Types.prod
90
91(** val jmpeqb :
92    Assembly.jump_length -> Assembly.jump_length -> Bool.bool **)
93let jmpeqb j1 j2 =
94  match j1 with
95  | Assembly.Short_jump ->
96    (match j2 with
97     | Assembly.Short_jump -> Bool.True
98     | Assembly.Absolute_jump -> Bool.False
99     | Assembly.Long_jump -> Bool.False)
100  | Assembly.Absolute_jump ->
101    (match j2 with
102     | Assembly.Short_jump -> Bool.False
103     | Assembly.Absolute_jump -> Bool.True
104     | Assembly.Long_jump -> Bool.False)
105  | Assembly.Long_jump ->
106    (match j2 with
107     | Assembly.Short_jump -> Bool.False
108     | Assembly.Absolute_jump -> Bool.False
109     | Assembly.Long_jump -> Bool.True)
110
111(** val expand_relative_jump_internal_unsafe :
112    Assembly.jump_length -> (ASM.subaddressing_mode -> ASM.subaddressing_mode
113    ASM.preinstruction) -> ASM.instruction List.list **)
114let expand_relative_jump_internal_unsafe jmp_len i =
115  match jmp_len with
116  | Assembly.Short_jump ->
117    List.Cons ((ASM.RealInstruction
118      (i (ASM.RELATIVE
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
124      (i (ASM.RELATIVE
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)))))
134
135(** val strip_target :
136    ASM.identifier ASM.preinstruction -> (ASM.subaddressing_mode ->
137    ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum **)
138let 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))
184
185(** val expand_relative_jump_unsafe :
186    Assembly.jump_length -> ASM.identifier ASM.preinstruction ->
187    ASM.instruction List.list **)
188let 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)
192
193(** val expand_pseudo_instruction_unsafe :
194    Assembly.jump_length -> ASM.pseudo_instruction -> ASM.instruction
195    List.list **)
196let 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)
200| ASM.Jmp jmp ->
201  (match jmp_len with
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)))))
226| ASM.Call call ->
227  (match jmp_len with
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) ->
239  (match d with
240   | Types.Inl x ->
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)))))))))))))))))
245     in
246     List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
247     (Types.Inr { Types.fst = ASM.DPTR; Types.snd = address }))))), List.Nil)
248   | Types.Inr pr ->
249     let v = ASM.DATA
250       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
251         (Nat.S Nat.O)))))))))
252     in
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
257      | ASM.DIRECT b1 ->
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 *))
263      | ASM.REGISTER r ->
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))
267      | ASM.ACC_A ->
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 *))) __)
285
286(** val instruction_size_jmplen :
287    Assembly.jump_length -> ASM.pseudo_instruction -> Nat.nat **)
288let instruction_size_jmplen jmp_len i =
289  let mapped =
290    List.map Assembly.assembly1 (expand_pseudo_instruction_unsafe jmp_len i)
291  in
292  let flattened = List.flatten mapped in
293  let pc_len = List.length flattened in pc_len
294
295(** val max_length :
296    Assembly.jump_length -> Assembly.jump_length -> Assembly.jump_length **)
297let max_length j1 j2 =
298  match j1 with
299  | Assembly.Short_jump ->
300    (match j2 with
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 ->
305    (match j2 with
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
310
311(** val dec_jmple :
312    Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum **)
313let dec_jmple x y =
314  match x with
315  | Assembly.Short_jump ->
316    (match y with
317     | Assembly.Short_jump -> Types.Inr __
318     | Assembly.Absolute_jump -> Types.Inl __
319     | Assembly.Long_jump -> Types.Inl __)
320  | Assembly.Absolute_jump ->
321    (match y with
322     | Assembly.Short_jump -> Types.Inr __
323     | Assembly.Absolute_jump -> Types.Inr __
324     | Assembly.Long_jump -> Types.Inl __)
325  | Assembly.Long_jump ->
326    (match y with
327     | Assembly.Short_jump -> Types.Inr __
328     | Assembly.Absolute_jump -> Types.Inr __
329     | Assembly.Long_jump -> Types.Inr __)
330
331(** val dec_eq_jump_length :
332    Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum **)
333let dec_eq_jump_length a b =
334  match a with
335  | Assembly.Short_jump ->
336    (match b with
337     | Assembly.Short_jump -> Types.Inl __
338     | Assembly.Absolute_jump -> Types.Inr __
339     | Assembly.Long_jump -> Types.Inr __)
340  | Assembly.Absolute_jump ->
341    (match b with
342     | Assembly.Short_jump -> Types.Inr __
343     | Assembly.Absolute_jump -> Types.Inl __
344     | Assembly.Long_jump -> Types.Inr __)
345  | Assembly.Long_jump ->
346    (match b with
347     | Assembly.Short_jump -> Types.Inr __
348     | Assembly.Absolute_jump -> Types.Inr __
349     | Assembly.Long_jump -> Types.Inl __)
350
351(** val create_label_map :
352    ASM.labelled_instruction List.list -> Fetch.label_map Types.sig0 **)
353let create_label_map program =
354  (Fetch.create_label_cost_map program).Types.fst
355
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 **)
359let select_reljump_length labels old_sigma inc_sigma ppc lbl ins_len =
360  let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
361  in
362  let { Types.fst = src; Types.snd = dest } =
363    match Nat.leb paddr ppc with
364    | Bool.True ->
365      let pc = inc_sigma.Types.fst in
366      let addr =
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
374      in
375      { 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) }
382    | Bool.False ->
383      let pc =
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
391      in
392      let addr =
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
400      in
401      { 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) }
408  in
409  let { Types.fst = sj_possible; Types.snd = disp } =
410    Assembly.short_jump_cond src dest
411  in
412  (match sj_possible with
413   | Bool.True -> Assembly.Short_jump
414   | Bool.False -> Assembly.Long_jump)
415
416(** val select_call_length :
417    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
418    -> Assembly.jump_length **)
419let select_call_length labels old_sigma inc_sigma ppc lbl =
420  let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
421  in
422  let { Types.fst = src; Types.snd = dest } =
423    match Nat.leb paddr ppc with
424    | Bool.True ->
425      let pc = inc_sigma.Types.fst in
426      let addr =
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
434      in
435      { 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))));
439      Types.snd =
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) }
443    | Bool.False ->
444      let pc =
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
452      in
453      let addr =
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
461      in
462      { 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))));
466      Types.snd =
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) }
470  in
471  let { Types.fst = aj_possible; Types.snd = disp } =
472    Assembly.absolute_jump_cond src dest
473  in
474  (match aj_possible with
475   | Bool.True -> Assembly.Absolute_jump
476   | Bool.False -> Assembly.Long_jump)
477
478(** val select_jump_length :
479    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
480    -> Assembly.jump_length **)
481let select_jump_length labels old_sigma inc_sigma ppc lbl =
482  let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
483  in
484  let { Types.fst = src; Types.snd = dest } =
485    match Nat.leb paddr ppc with
486    | Bool.True ->
487      let pc = inc_sigma.Types.fst in
488      let addr =
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
496      in
497      { 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))));
501      Types.snd =
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) }
505    | Bool.False ->
506      let pc =
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
514      in
515      let addr =
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
523      in
524      { 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))));
528      Types.snd =
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) }
532  in
533  let { Types.fst = sj_possible; Types.snd = disp } =
534    Assembly.short_jump_cond src dest
535  in
536  (match sj_possible with
537   | Bool.True -> Assembly.Short_jump
538   | Bool.False -> select_call_length labels old_sigma inc_sigma ppc lbl)
539
540(** val destination_of :
541    ASM.identifier ASM.preinstruction -> ASM.identifier Types.option **)
542let 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
581
582(** val length_of : ASM.identifier ASM.preinstruction -> Nat.nat **)
583let length_of = function
584| ASM.ADD (x, x0) -> Nat.O
585| ASM.ADDC (x, x0) -> Nat.O
586| ASM.SUBB (x, x0) -> Nat.O
587| ASM.INC x -> Nat.O
588| ASM.DEC x -> Nat.O
589| ASM.MUL (x, x0) -> Nat.O
590| ASM.DIV (x, x0) -> Nat.O
591| ASM.DA x -> 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))
600| ASM.DJNZ (x, j) ->
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)))
622| ASM.ANL x -> Nat.O
623| ASM.ORL x -> Nat.O
624| ASM.XRL x -> Nat.O
625| ASM.CLR x -> Nat.O
626| ASM.CPL x -> Nat.O
627| ASM.RL x -> Nat.O
628| ASM.RLC x -> Nat.O
629| ASM.RR x -> Nat.O
630| ASM.RRC x -> Nat.O
631| ASM.SWAP x -> Nat.O
632| ASM.MOV x -> Nat.O
633| ASM.MOVX x -> Nat.O
634| ASM.SETB x -> Nat.O
635| ASM.PUSH x -> Nat.O
636| ASM.POP x -> Nat.O
637| ASM.XCH (x, x0) -> Nat.O
638| ASM.XCHD (x, x0) -> Nat.O
639| ASM.RET -> Nat.O
640| ASM.RETI -> Nat.O
641| ASM.NOP -> Nat.O
642| ASM.JMP x -> Nat.O
643
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 **)
647let 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
651   | Types.Some j ->
652     Types.Some
653       (select_reljump_length labels old_sigma inc_sigma ppc j ins_len))
654
655(** val jump_expansion_start :
656    ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
657    ppc_pc_map Types.option Types.sig0 **)
658let jump_expansion_start program labels =
659  (let { Types.fst = ignore; Types.snd = final_policy } =
660     Types.pi1
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
664         (fun _ ->
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
668         let sacc =
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
672         in
673         { Types.fst = sacc; Types.snd = { Types.fst = (Nat.plus pc isize);
674         Types.snd =
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) } }))
679           __) { Types.fst =
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;
683         Types.snd =
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)))))))))))))))))) } })
693   in
694  (fun _ ->
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)) __)) __
701
Note: See TracBrowser for help on using the repository browser.