source: driver/extracted/assembly.mli @ 3106

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

New extraction.

File size: 4.1 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 BitVectorTrie
32
33open String
34
35open Integers
36
37open AST
38
39open LabelledObjects
40
41open Proper
42
43open PositiveMap
44
45open Deqsets
46
47open ErrorMessages
48
49open PreIdentifiers
50
51open Errors
52
53open Lists
54
55open Positive
56
57open Identifiers
58
59open CostLabel
60
61open ASM
62
63open Exp
64
65open Setoids
66
67open Monad
68
69open Option
70
71open Extranat
72
73open Vector
74
75open FoldStuff
76
77open BitVector
78
79open Arithmetic
80
81open Fetch
82
83open Status
84
85type jump_length =
86| Short_jump
87| Absolute_jump
88| Long_jump
89
90val jump_length_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
91
92val jump_length_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
93
94val jump_length_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
95
96val jump_length_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
97
98val jump_length_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
99
100val jump_length_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
101
102val jump_length_inv_rect_Type4 :
103  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
104
105val jump_length_inv_rect_Type3 :
106  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
107
108val jump_length_inv_rect_Type2 :
109  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
110
111val jump_length_inv_rect_Type1 :
112  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
113
114val jump_length_inv_rect_Type0 :
115  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
116
117val jump_length_discr : jump_length -> jump_length -> __
118
119val jump_length_jmdiscr : jump_length -> jump_length -> __
120
121val short_jump_cond :
122  BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
123  Types.prod
124
125val absolute_jump_cond :
126  BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
127  Types.prod
128
129val assembly_preinstruction :
130  ('a1 -> BitVector.byte) -> 'a1 ASM.preinstruction -> Bool.bool
131  Vector.vector List.list
132
133val assembly1 : ASM.instruction -> Bool.bool Vector.vector List.list
134
135val expand_relative_jump_internal :
136  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
137  (BitVector.word -> Bool.bool) -> ASM.identifier -> BitVector.word ->
138  (ASM.subaddressing_mode -> ASM.subaddressing_mode ASM.preinstruction) ->
139  ASM.instruction List.list
140
141val expand_relative_jump :
142  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
143  (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier
144  ASM.preinstruction -> ASM.instruction List.list
145
146val is_code : AST.region -> Bool.bool
147
148val expand_pseudo_instruction :
149  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
150  (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
151  (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
152  ASM.instruction List.list
153
154val assembly_1_pseudoinstruction :
155  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
156  (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
157  (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
158  (Nat.nat, Bool.bool Vector.vector List.list) Types.prod
159
160val instruction_size :
161  (ASM.identifier -> BitVector.word) -> (ASM.identifier -> (AST.region,
162  BitVector.word) Types.prod) -> (BitVector.word -> BitVector.word) ->
163  (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction
164  -> Nat.nat
165
166val assembly :
167  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
168  (BitVector.word -> Bool.bool) -> ASM.labelled_object_code Types.sig0
169
170val ticks_of_instruction : ASM.instruction -> Nat.nat
171
172val ticks_of0 :
173  ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
174  (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
175  BitVector.word -> ASM.pseudo_instruction -> (Nat.nat, Nat.nat) Types.prod
176
177val ticks_of :
178  ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
179  (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
180  BitVector.word -> (Nat.nat, Nat.nat) Types.prod
181
Note: See TracBrowser for help on using the repository browser.