source: extracted/policyFront.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 27.1 KB
Line 
1open Preamble
2
3open String
4
5open LabelledObjects
6
7open BitVectorTrie
8
9open Exp
10
11open Arithmetic
12
13open Integers
14
15open AST
16
17open CostLabel
18
19open Proper
20
21open PositiveMap
22
23open Deqsets
24
25open ErrorMessages
26
27open PreIdentifiers
28
29open Errors
30
31open Extralib
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Lists
40
41open Positive
42
43open Identifiers
44
45open Extranat
46
47open Vector
48
49open Div_and_mod
50
51open Jmeq
52
53open Russell
54
55open Types
56
57open List
58
59open Util
60
61open FoldStuff
62
63open Bool
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Relations
74
75open Nat
76
77open BitVector
78
79open ASM
80
81open Fetch
82
83open Status
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.identifier0 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.identifier0 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.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.MovSuccessor (dst, ws, lbl) ->
227  let v = ASM.DATA
228    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
229      Nat.O)))))))))
230  in
231  (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
232           (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
233           ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr, Vector.VEmpty))))))
234           dst with
235   | ASM.DIRECT b1 ->
236     (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
237       (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b1); Types.snd =
238       v })))))), List.Nil))
239   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
240   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
241   | ASM.REGISTER r ->
242     (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
243       (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.REGISTER r);
244       Types.snd = v }))))))), List.Nil))
245   | ASM.ACC_A ->
246     (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
247       (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
248       v }))))))), List.Nil))
249   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
250   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
251   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
252   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
253   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
254   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
255   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
256   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
257   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
258   | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
259   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
260   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
261   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
262   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
263| ASM.Call call ->
264  (match jmp_len with
265   | Assembly.Short_jump -> List.Nil
266   | Assembly.Absolute_jump ->
267     List.Cons ((ASM.ACALL (ASM.ADDR11
268       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
269         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))), List.Nil)
270   | Assembly.Long_jump ->
271     List.Cons ((ASM.LCALL (ASM.ADDR16
272       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
273         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
274         Nat.O))))))))))))))))))), List.Nil))
275| ASM.Mov (d, trgt) ->
276  List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inr
277    { Types.fst = ASM.DPTR; Types.snd = (ASM.DATA16
278    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
279      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
280      Nat.O)))))))))))))))))) }))))), List.Nil)
281
282(** val instruction_size_jmplen :
283    Assembly.jump_length -> ASM.pseudo_instruction -> Nat.nat **)
284let instruction_size_jmplen jmp_len i =
285  let mapped =
286    List.map Assembly.assembly1 (expand_pseudo_instruction_unsafe jmp_len i)
287  in
288  let flattened = List.flatten mapped in
289  let pc_len = List.length flattened in pc_len
290
291(** val max_length :
292    Assembly.jump_length -> Assembly.jump_length -> Assembly.jump_length **)
293let max_length j1 j2 =
294  match j1 with
295  | Assembly.Short_jump ->
296    (match j2 with
297     | Assembly.Short_jump -> Assembly.Short_jump
298     | Assembly.Absolute_jump -> Assembly.Long_jump
299     | Assembly.Long_jump -> Assembly.Long_jump)
300  | Assembly.Absolute_jump ->
301    (match j2 with
302     | Assembly.Short_jump -> Assembly.Long_jump
303     | Assembly.Absolute_jump -> Assembly.Absolute_jump
304     | Assembly.Long_jump -> Assembly.Long_jump)
305  | Assembly.Long_jump -> Assembly.Long_jump
306
307(** val dec_jmple :
308    Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum **)
309let dec_jmple x y =
310  match x with
311  | Assembly.Short_jump ->
312    (match y with
313     | Assembly.Short_jump -> Types.Inr __
314     | Assembly.Absolute_jump -> Types.Inl __
315     | Assembly.Long_jump -> Types.Inl __)
316  | Assembly.Absolute_jump ->
317    (match y with
318     | Assembly.Short_jump -> Types.Inr __
319     | Assembly.Absolute_jump -> Types.Inr __
320     | Assembly.Long_jump -> Types.Inl __)
321  | Assembly.Long_jump ->
322    (match y with
323     | Assembly.Short_jump -> Types.Inr __
324     | Assembly.Absolute_jump -> Types.Inr __
325     | Assembly.Long_jump -> Types.Inr __)
326
327(** val dec_eq_jump_length :
328    Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum **)
329let dec_eq_jump_length a b =
330  match a with
331  | Assembly.Short_jump ->
332    (match b with
333     | Assembly.Short_jump -> Types.Inl __
334     | Assembly.Absolute_jump -> Types.Inr __
335     | Assembly.Long_jump -> Types.Inr __)
336  | Assembly.Absolute_jump ->
337    (match b with
338     | Assembly.Short_jump -> Types.Inr __
339     | Assembly.Absolute_jump -> Types.Inl __
340     | Assembly.Long_jump -> Types.Inr __)
341  | Assembly.Long_jump ->
342    (match b with
343     | Assembly.Short_jump -> Types.Inr __
344     | Assembly.Absolute_jump -> Types.Inr __
345     | Assembly.Long_jump -> Types.Inl __)
346
347(** val create_label_map :
348    ASM.labelled_instruction List.list -> Fetch.label_map Types.sig0 **)
349let create_label_map program0 =
350  (Fetch.create_label_cost_map program0).Types.fst
351
352(** val select_reljump_length :
353    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
354    -> Nat.nat -> Assembly.jump_length **)
355let select_reljump_length labels old_sigma inc_sigma ppc lbl ins_len =
356  let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
357  in
358  let { Types.fst = src; Types.snd = dest } =
359    match Nat.leb paddr ppc with
360    | Bool.True ->
361      let pc = inc_sigma.Types.fst in
362      let addr =
363        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
364          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
365          (Nat.S Nat.O))))))))))))))))
366          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
367            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
368            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
369          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
370      in
371      { Types.fst =
372      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
373        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
374        Nat.O)))))))))))))))) (Nat.plus pc ins_len)); Types.snd =
375      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
376        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
377        Nat.O)))))))))))))))) addr) }
378    | Bool.False ->
379      let pc =
380        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
381          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
382          (Nat.S Nat.O))))))))))))))))
383          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
384            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
385            (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
386          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
387      in
388      let addr =
389        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
390          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
391          (Nat.S Nat.O))))))))))))))))
392          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
393            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
394            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
395          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
396      in
397      { Types.fst =
398      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
399        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
400        Nat.O)))))))))))))))) (Nat.plus pc ins_len)); Types.snd =
401      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
402        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
403        Nat.O)))))))))))))))) addr) }
404  in
405  let { Types.fst = sj_possible; Types.snd = disp } =
406    Assembly.short_jump_cond src dest
407  in
408  (match sj_possible with
409   | Bool.True -> Assembly.Short_jump
410   | Bool.False -> Assembly.Long_jump)
411
412(** val select_call_length :
413    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
414    -> Assembly.jump_length **)
415let select_call_length labels old_sigma inc_sigma ppc lbl =
416  let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
417  in
418  let { Types.fst = src; Types.snd = dest } =
419    match Nat.leb paddr ppc with
420    | Bool.True ->
421      let pc = inc_sigma.Types.fst in
422      let addr =
423        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
424          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
425          (Nat.S Nat.O))))))))))))))))
426          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
427            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
428            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
429          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
430      in
431      { Types.fst =
432      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
433        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
434        Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
435      Types.snd =
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)))))))))))))))) addr) }
439    | Bool.False ->
440      let pc =
441        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
442          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
443          (Nat.S Nat.O))))))))))))))))
444          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
445            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
446            (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
447          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
448      in
449      let addr =
450        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
451          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
452          (Nat.S Nat.O))))))))))))))))
453          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
454            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
455            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
456          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
457      in
458      { Types.fst =
459      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
460        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
461        Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
462      Types.snd =
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)))))))))))))))) addr) }
466  in
467  let { Types.fst = aj_possible; Types.snd = disp } =
468    Assembly.absolute_jump_cond src dest
469  in
470  (match aj_possible with
471   | Bool.True -> Assembly.Absolute_jump
472   | Bool.False -> Assembly.Long_jump)
473
474(** val select_jump_length :
475    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
476    -> Assembly.jump_length **)
477let select_jump_length labels old_sigma inc_sigma ppc lbl =
478  let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
479  in
480  let { Types.fst = src; Types.snd = dest } =
481    match Nat.leb paddr ppc with
482    | Bool.True ->
483      let pc = inc_sigma.Types.fst in
484      let addr =
485        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
486          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
487          (Nat.S Nat.O))))))))))))))))
488          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
489            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
490            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
491          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
492      in
493      { Types.fst =
494      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
495        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
496        Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
497      Types.snd =
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)))))))))))))))) addr) }
501    | Bool.False ->
502      let pc =
503        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
504          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
505          (Nat.S Nat.O))))))))))))))))
506          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
507            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
508            (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
509          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
510      in
511      let addr =
512        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
513          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
514          (Nat.S Nat.O))))))))))))))))
515          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
516            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
517            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
518          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
519      in
520      { Types.fst =
521      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
522        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
523        Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
524      Types.snd =
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)))))))))))))))) addr) }
528  in
529  let { Types.fst = sj_possible; Types.snd = disp } =
530    Assembly.short_jump_cond src dest
531  in
532  (match sj_possible with
533   | Bool.True -> Assembly.Short_jump
534   | Bool.False -> select_call_length labels old_sigma inc_sigma ppc lbl)
535
536(** val destination_of :
537    ASM.identifier0 ASM.preinstruction -> ASM.identifier0 Types.option **)
538let destination_of = function
539| ASM.ADD (x, x0) -> Types.None
540| ASM.ADDC (x, x0) -> Types.None
541| ASM.SUBB (x, x0) -> Types.None
542| ASM.INC x -> Types.None
543| ASM.DEC x -> Types.None
544| ASM.MUL (x, x0) -> Types.None
545| ASM.DIV (x, x0) -> Types.None
546| ASM.DA x -> Types.None
547| ASM.JC j -> Types.Some j
548| ASM.JNC j -> Types.Some j
549| ASM.JB (x, j) -> Types.Some j
550| ASM.JNB (x, j) -> Types.Some j
551| ASM.JBC (x, j) -> Types.Some j
552| ASM.JZ j -> Types.Some j
553| ASM.JNZ j -> Types.Some j
554| ASM.CJNE (x, j) -> Types.Some j
555| ASM.DJNZ (x, j) -> Types.Some j
556| ASM.ANL x -> Types.None
557| ASM.ORL x -> Types.None
558| ASM.XRL x -> Types.None
559| ASM.CLR x -> Types.None
560| ASM.CPL x -> Types.None
561| ASM.RL x -> Types.None
562| ASM.RLC x -> Types.None
563| ASM.RR x -> Types.None
564| ASM.RRC x -> Types.None
565| ASM.SWAP x -> Types.None
566| ASM.MOV x -> Types.None
567| ASM.MOVX x -> Types.None
568| ASM.SETB x -> Types.None
569| ASM.PUSH x -> Types.None
570| ASM.POP x -> Types.None
571| ASM.XCH (x, x0) -> Types.None
572| ASM.XCHD (x, x0) -> Types.None
573| ASM.RET -> Types.None
574| ASM.RETI -> Types.None
575| ASM.NOP -> Types.None
576| ASM.JMP x -> Types.None
577
578(** val length_of : ASM.identifier0 ASM.preinstruction -> Nat.nat **)
579let length_of = function
580| ASM.ADD (x, x0) -> Nat.O
581| ASM.ADDC (x, x0) -> Nat.O
582| ASM.SUBB (x, x0) -> Nat.O
583| ASM.INC x -> Nat.O
584| ASM.DEC x -> Nat.O
585| ASM.MUL (x, x0) -> Nat.O
586| ASM.DIV (x, x0) -> Nat.O
587| ASM.DA x -> Nat.O
588| ASM.JC j -> Nat.S (Nat.S Nat.O)
589| ASM.JNC j -> Nat.S (Nat.S Nat.O)
590| ASM.JB (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
591| ASM.JNB (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
592| ASM.JBC (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
593| ASM.JZ j -> Nat.S (Nat.S Nat.O)
594| ASM.JNZ j -> Nat.S (Nat.S Nat.O)
595| ASM.CJNE (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
596| ASM.DJNZ (x, j) ->
597  (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
598           ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)))) x with
599   | ASM.DIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
600   | ASM.INDIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
601   | ASM.EXT_INDIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
602   | ASM.REGISTER x0 -> Nat.S (Nat.S Nat.O)
603   | ASM.ACC_A -> Nat.S (Nat.S (Nat.S Nat.O))
604   | ASM.ACC_B -> Nat.S (Nat.S (Nat.S Nat.O))
605   | ASM.DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
606   | ASM.DATA x0 -> Nat.S (Nat.S (Nat.S Nat.O))
607   | ASM.DATA16 x0 -> Nat.S (Nat.S (Nat.S Nat.O))
608   | ASM.ACC_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
609   | ASM.ACC_PC -> Nat.S (Nat.S (Nat.S Nat.O))
610   | ASM.EXT_INDIRECT_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
611   | ASM.INDIRECT_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
612   | ASM.CARRY -> Nat.S (Nat.S (Nat.S Nat.O))
613   | ASM.BIT_ADDR x0 -> Nat.S (Nat.S (Nat.S Nat.O))
614   | ASM.N_BIT_ADDR x0 -> Nat.S (Nat.S (Nat.S Nat.O))
615   | ASM.RELATIVE x0 -> Nat.S (Nat.S (Nat.S Nat.O))
616   | ASM.ADDR11 x0 -> Nat.S (Nat.S (Nat.S Nat.O))
617   | ASM.ADDR16 x0 -> Nat.S (Nat.S (Nat.S Nat.O)))
618| ASM.ANL x -> Nat.O
619| ASM.ORL x -> Nat.O
620| ASM.XRL x -> Nat.O
621| ASM.CLR x -> Nat.O
622| ASM.CPL x -> Nat.O
623| ASM.RL x -> Nat.O
624| ASM.RLC x -> Nat.O
625| ASM.RR x -> Nat.O
626| ASM.RRC x -> Nat.O
627| ASM.SWAP x -> Nat.O
628| ASM.MOV x -> Nat.O
629| ASM.MOVX x -> Nat.O
630| ASM.SETB x -> Nat.O
631| ASM.PUSH x -> Nat.O
632| ASM.POP x -> Nat.O
633| ASM.XCH (x, x0) -> Nat.O
634| ASM.XCHD (x, x0) -> Nat.O
635| ASM.RET -> Nat.O
636| ASM.RETI -> Nat.O
637| ASM.NOP -> Nat.O
638| ASM.JMP x -> Nat.O
639
640(** val jump_expansion_step_instruction :
641    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
642    ASM.preinstruction -> Assembly.jump_length Types.option **)
643let jump_expansion_step_instruction labels old_sigma inc_sigma ppc i =
644  let ins_len = length_of i in
645  (match destination_of i with
646   | Types.None -> Types.None
647   | Types.Some j ->
648     Types.Some
649       (select_reljump_length labels old_sigma inc_sigma ppc j ins_len))
650
651(** val jump_expansion_start :
652    ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
653    ppc_pc_map Types.option Types.sig0 **)
654let jump_expansion_start program0 labels =
655  let final_policy =
656    FoldStuff.foldl_strong (Types.pi1 program0) (fun prefix0 x tl _ p ->
657      let { Types.fst = pc; Types.snd = sigma0 } = Types.pi1 p in
658      let { Types.fst = label; Types.snd = instr } = x in
659      let isize = instruction_size_jmplen Assembly.Short_jump instr in
660      { Types.fst = (Nat.plus pc isize); Types.snd =
661      (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
662        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
663        Nat.O))))))))))))))))
664        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
665          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
666          (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S (List.length prefix0)))
667        { Types.fst = (Nat.plus pc isize); Types.snd = Assembly.Short_jump }
668        sigma0) }) { Types.fst = Nat.O; Types.snd =
669      (BitVectorTrie.insert (Nat.S (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.O))))))))))))))))
672        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
673          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
674          (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O;
675        Types.snd = Assembly.Short_jump } (BitVectorTrie.Stub (Nat.S (Nat.S
676        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
677        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) }
678  in
679  (match Util.gtb (Types.pi1 final_policy).Types.fst
680           (Exp.exp (Nat.S (Nat.S Nat.O)) (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.S (Nat.S Nat.O))))))))))))))))) with
683   | Bool.True -> (fun _ -> Types.None)
684   | Bool.False -> (fun _ -> Types.Some (Types.pi1 final_policy))) __
685
Note: See TracBrowser for help on using the repository browser.