source: driver/extracted/frontEndOps.ml @ 3106

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

New extraction

File size: 56.9 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open Extralib
10
11open Lists
12
13open Identifiers
14
15open Integers
16
17open AST
18
19open Division
20
21open Exp
22
23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
39open ErrorMessages
40
41open Option
42
43open Setoids
44
45open Monad
46
47open Positive
48
49open PreIdentifiers
50
51open Errors
52
53open Div_and_mod
54
55open Jmeq
56
57open Russell
58
59open Util
60
61open Bool
62
63open Relations
64
65open Nat
66
67open List
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Types
78
79open Coqlib
80
81open Values
82
83open FrontEndVal
84
85open Hide
86
87open ByteValues
88
89open GenMem
90
91open FrontEndMem
92
93type constant =
94| Ointconst of AST.intsize * AST.signedness * AST.bvint
95| Oaddrsymbol of AST.ident * Nat.nat
96| Oaddrstack of Nat.nat
97
98(** val constant_rect_Type4 :
99    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
100    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
101let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13118 = function
102| Ointconst (sz, sg, x_13120) -> h_Ointconst sz sg x_13120
103| Oaddrsymbol (x_13122, x_13121) -> h_Oaddrsymbol x_13122 x_13121
104| Oaddrstack x_13123 -> h_Oaddrstack x_13123
105
106(** val constant_rect_Type5 :
107    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
108    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
109let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13127 = function
110| Ointconst (sz, sg, x_13129) -> h_Ointconst sz sg x_13129
111| Oaddrsymbol (x_13131, x_13130) -> h_Oaddrsymbol x_13131 x_13130
112| Oaddrstack x_13132 -> h_Oaddrstack x_13132
113
114(** val constant_rect_Type3 :
115    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
116    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
117let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13136 = function
118| Ointconst (sz, sg, x_13138) -> h_Ointconst sz sg x_13138
119| Oaddrsymbol (x_13140, x_13139) -> h_Oaddrsymbol x_13140 x_13139
120| Oaddrstack x_13141 -> h_Oaddrstack x_13141
121
122(** val constant_rect_Type2 :
123    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
124    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
125let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13145 = function
126| Ointconst (sz, sg, x_13147) -> h_Ointconst sz sg x_13147
127| Oaddrsymbol (x_13149, x_13148) -> h_Oaddrsymbol x_13149 x_13148
128| Oaddrstack x_13150 -> h_Oaddrstack x_13150
129
130(** val constant_rect_Type1 :
131    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
132    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
133let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13154 = function
134| Ointconst (sz, sg, x_13156) -> h_Ointconst sz sg x_13156
135| Oaddrsymbol (x_13158, x_13157) -> h_Oaddrsymbol x_13158 x_13157
136| Oaddrstack x_13159 -> h_Oaddrstack x_13159
137
138(** val constant_rect_Type0 :
139    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
140    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
141let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13163 = function
142| Ointconst (sz, sg, x_13165) -> h_Ointconst sz sg x_13165
143| Oaddrsymbol (x_13167, x_13166) -> h_Oaddrsymbol x_13167 x_13166
144| Oaddrstack x_13168 -> h_Oaddrstack x_13168
145
146(** val constant_inv_rect_Type4 :
147    AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
148    -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
149    __ -> __ -> 'a1) -> 'a1 **)
150let constant_inv_rect_Type4 x1 hterm h1 h2 h3 =
151  let hcut = constant_rect_Type4 h1 h2 h3 x1 hterm in hcut __ __
152
153(** val constant_inv_rect_Type3 :
154    AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
155    -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
156    __ -> __ -> 'a1) -> 'a1 **)
157let constant_inv_rect_Type3 x1 hterm h1 h2 h3 =
158  let hcut = constant_rect_Type3 h1 h2 h3 x1 hterm in hcut __ __
159
160(** val constant_inv_rect_Type2 :
161    AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
162    -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
163    __ -> __ -> 'a1) -> 'a1 **)
164let constant_inv_rect_Type2 x1 hterm h1 h2 h3 =
165  let hcut = constant_rect_Type2 h1 h2 h3 x1 hterm in hcut __ __
166
167(** val constant_inv_rect_Type1 :
168    AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
169    -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
170    __ -> __ -> 'a1) -> 'a1 **)
171let constant_inv_rect_Type1 x1 hterm h1 h2 h3 =
172  let hcut = constant_rect_Type1 h1 h2 h3 x1 hterm in hcut __ __
173
174(** val constant_inv_rect_Type0 :
175    AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
176    -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
177    __ -> __ -> 'a1) -> 'a1 **)
178let constant_inv_rect_Type0 x1 hterm h1 h2 h3 =
179  let hcut = constant_rect_Type0 h1 h2 h3 x1 hterm in hcut __ __
180
181(** val constant_discr : AST.typ -> constant -> constant -> __ **)
182let constant_discr a1 x y =
183  Logic.eq_rect_Type2 x
184    (match x with
185     | Ointconst (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
186     | Oaddrsymbol (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
187     | Oaddrstack a0 -> Obj.magic (fun _ dH -> dH __)) y
188
189(** val constant_jmdiscr : AST.typ -> constant -> constant -> __ **)
190let constant_jmdiscr a1 x y =
191  Logic.eq_rect_Type2 x
192    (match x with
193     | Ointconst (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
194     | Oaddrsymbol (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
195     | Oaddrstack a0 -> Obj.magic (fun _ dH -> dH __)) y
196
197type unary_operation =
198| Ocastint of AST.intsize * AST.signedness * AST.intsize * AST.signedness
199| Onegint of AST.intsize * AST.signedness
200| Onotbool of AST.typ * AST.intsize * AST.signedness
201| Onotint of AST.intsize * AST.signedness
202| Oid of AST.typ
203| Optrofint of AST.intsize * AST.signedness
204| Ointofptr of AST.intsize * AST.signedness
205
206(** val unary_operation_rect_Type4 :
207    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
208    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
209    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
210    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
211    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
212    unary_operation -> 'a1 **)
213let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13238 x_13237 = function
214| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
215| Onegint (sz, sg) -> h_Onegint sz sg
216| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
217| Onotint (sz, sg) -> h_Onotint sz sg
218| Oid t -> h_Oid t
219| Optrofint (sz, sg) -> h_Optrofint sz sg
220| Ointofptr (sz, sg) -> h_Ointofptr sz sg
221
222(** val unary_operation_rect_Type5 :
223    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
224    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
225    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
226    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
227    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
228    unary_operation -> 'a1 **)
229let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13249 x_13248 = function
230| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
231| Onegint (sz, sg) -> h_Onegint sz sg
232| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
233| Onotint (sz, sg) -> h_Onotint sz sg
234| Oid t -> h_Oid t
235| Optrofint (sz, sg) -> h_Optrofint sz sg
236| Ointofptr (sz, sg) -> h_Ointofptr sz sg
237
238(** val unary_operation_rect_Type3 :
239    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
240    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
241    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
242    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
243    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
244    unary_operation -> 'a1 **)
245let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13260 x_13259 = function
246| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
247| Onegint (sz, sg) -> h_Onegint sz sg
248| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
249| Onotint (sz, sg) -> h_Onotint sz sg
250| Oid t -> h_Oid t
251| Optrofint (sz, sg) -> h_Optrofint sz sg
252| Ointofptr (sz, sg) -> h_Ointofptr sz sg
253
254(** val unary_operation_rect_Type2 :
255    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
256    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
257    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
258    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
259    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
260    unary_operation -> 'a1 **)
261let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13271 x_13270 = function
262| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
263| Onegint (sz, sg) -> h_Onegint sz sg
264| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
265| Onotint (sz, sg) -> h_Onotint sz sg
266| Oid t -> h_Oid t
267| Optrofint (sz, sg) -> h_Optrofint sz sg
268| Ointofptr (sz, sg) -> h_Ointofptr sz sg
269
270(** val unary_operation_rect_Type1 :
271    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
272    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
273    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
274    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
275    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
276    unary_operation -> 'a1 **)
277let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13282 x_13281 = function
278| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
279| Onegint (sz, sg) -> h_Onegint sz sg
280| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
281| Onotint (sz, sg) -> h_Onotint sz sg
282| Oid t -> h_Oid t
283| Optrofint (sz, sg) -> h_Optrofint sz sg
284| Ointofptr (sz, sg) -> h_Ointofptr sz sg
285
286(** val unary_operation_rect_Type0 :
287    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
288    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
289    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
290    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
291    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
292    unary_operation -> 'a1 **)
293let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13293 x_13292 = function
294| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
295| Onegint (sz, sg) -> h_Onegint sz sg
296| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
297| Onotint (sz, sg) -> h_Onotint sz sg
298| Oid t -> h_Oid t
299| Optrofint (sz, sg) -> h_Optrofint sz sg
300| Ointofptr (sz, sg) -> h_Ointofptr sz sg
301
302(** val unary_operation_inv_rect_Type4 :
303    AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
304    -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
305    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
306    AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
307    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
308    __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
309    __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
310    'a1 **)
311let unary_operation_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
312  let hcut = unary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
313  hcut __ __ __
314
315(** val unary_operation_inv_rect_Type3 :
316    AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
317    -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
318    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
319    AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
320    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
321    __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
322    __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
323    'a1 **)
324let unary_operation_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
325  let hcut = unary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
326  hcut __ __ __
327
328(** val unary_operation_inv_rect_Type2 :
329    AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
330    -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
331    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
332    AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
333    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
334    __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
335    __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
336    'a1 **)
337let unary_operation_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
338  let hcut = unary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
339  hcut __ __ __
340
341(** val unary_operation_inv_rect_Type1 :
342    AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
343    -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
344    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
345    AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
346    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
347    __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
348    __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
349    'a1 **)
350let unary_operation_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
351  let hcut = unary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
352  hcut __ __ __
353
354(** val unary_operation_inv_rect_Type0 :
355    AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
356    -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
357    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
358    AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
359    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
360    __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
361    __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
362    'a1 **)
363let unary_operation_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
364  let hcut = unary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
365  hcut __ __ __
366
367(** val unary_operation_discr :
368    AST.typ -> AST.typ -> unary_operation -> unary_operation -> __ **)
369let unary_operation_discr a1 a2 x y =
370  Logic.eq_rect_Type2 x
371    (match x with
372     | Ocastint (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
373     | Onegint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
374     | Onotbool (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
375     | Onotint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
376     | Oid a0 -> Obj.magic (fun _ dH -> dH __)
377     | Optrofint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
378     | Ointofptr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
379
380(** val unary_operation_jmdiscr :
381    AST.typ -> AST.typ -> unary_operation -> unary_operation -> __ **)
382let unary_operation_jmdiscr a1 a2 x y =
383  Logic.eq_rect_Type2 x
384    (match x with
385     | Ocastint (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
386     | Onegint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
387     | Onotbool (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
388     | Onotint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
389     | Oid a0 -> Obj.magic (fun _ dH -> dH __)
390     | Optrofint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
391     | Ointofptr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
392
393type binary_operation =
394| Oadd of AST.intsize * AST.signedness
395| Osub of AST.intsize * AST.signedness
396| Omul of AST.intsize * AST.signedness
397| Odiv of AST.intsize
398| Odivu of AST.intsize
399| Omod of AST.intsize
400| Omodu of AST.intsize
401| Oand of AST.intsize * AST.signedness
402| Oor of AST.intsize * AST.signedness
403| Oxor of AST.intsize * AST.signedness
404| Oshl of AST.intsize * AST.signedness
405| Oshr of AST.intsize * AST.signedness
406| Oshru of AST.intsize * AST.signedness
407| Ocmp of AST.intsize * AST.signedness * AST.signedness * Integers.comparison
408| Ocmpu of AST.intsize * AST.signedness * Integers.comparison
409| Oaddpi of AST.intsize
410| Oaddip of AST.intsize
411| Osubpi of AST.intsize
412| Osubpp of AST.intsize
413| Ocmpp of AST.signedness * Integers.comparison
414
415(** val binary_operation_rect_Type4 :
416    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
417    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
418    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
419    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
420    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
421    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
422    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
423    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
424    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
425    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
426    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
427    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
428let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13398 x_13397 x_13396 = function
429| Oadd (sz, sg) -> h_Oadd sz sg
430| Osub (sz, sg) -> h_Osub sz sg
431| Omul (sz, sg) -> h_Omul sz sg
432| Odiv sz -> h_Odiv sz
433| Odivu sz -> h_Odivu sz
434| Omod sz -> h_Omod sz
435| Omodu sz -> h_Omodu sz
436| Oand (sz, sg) -> h_Oand sz sg
437| Oor (sz, sg) -> h_Oor sz sg
438| Oxor (sz, sg) -> h_Oxor sz sg
439| Oshl (sz, sg) -> h_Oshl sz sg
440| Oshr (sz, sg) -> h_Oshr sz sg
441| Oshru (sz, sg) -> h_Oshru sz sg
442| Ocmp (sz, sg, sg', x_13400) -> h_Ocmp sz sg sg' x_13400
443| Ocmpu (sz, sg', x_13401) -> h_Ocmpu sz sg' x_13401
444| Oaddpi sz -> h_Oaddpi sz
445| Oaddip sz -> h_Oaddip sz
446| Osubpi sz -> h_Osubpi sz
447| Osubpp sz -> h_Osubpp sz
448| Ocmpp (sg', x_13402) -> h_Ocmpp sg' x_13402
449
450(** val binary_operation_rect_Type5 :
451    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
452    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
453    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
454    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
455    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
456    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
457    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
458    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
459    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
460    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
461    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
462    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
463let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13425 x_13424 x_13423 = function
464| Oadd (sz, sg) -> h_Oadd sz sg
465| Osub (sz, sg) -> h_Osub sz sg
466| Omul (sz, sg) -> h_Omul sz sg
467| Odiv sz -> h_Odiv sz
468| Odivu sz -> h_Odivu sz
469| Omod sz -> h_Omod sz
470| Omodu sz -> h_Omodu sz
471| Oand (sz, sg) -> h_Oand sz sg
472| Oor (sz, sg) -> h_Oor sz sg
473| Oxor (sz, sg) -> h_Oxor sz sg
474| Oshl (sz, sg) -> h_Oshl sz sg
475| Oshr (sz, sg) -> h_Oshr sz sg
476| Oshru (sz, sg) -> h_Oshru sz sg
477| Ocmp (sz, sg, sg', x_13427) -> h_Ocmp sz sg sg' x_13427
478| Ocmpu (sz, sg', x_13428) -> h_Ocmpu sz sg' x_13428
479| Oaddpi sz -> h_Oaddpi sz
480| Oaddip sz -> h_Oaddip sz
481| Osubpi sz -> h_Osubpi sz
482| Osubpp sz -> h_Osubpp sz
483| Ocmpp (sg', x_13429) -> h_Ocmpp sg' x_13429
484
485(** val binary_operation_rect_Type3 :
486    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
487    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
488    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
489    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
490    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
491    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
492    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
493    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
494    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
495    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
496    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
497    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
498let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13452 x_13451 x_13450 = function
499| Oadd (sz, sg) -> h_Oadd sz sg
500| Osub (sz, sg) -> h_Osub sz sg
501| Omul (sz, sg) -> h_Omul sz sg
502| Odiv sz -> h_Odiv sz
503| Odivu sz -> h_Odivu sz
504| Omod sz -> h_Omod sz
505| Omodu sz -> h_Omodu sz
506| Oand (sz, sg) -> h_Oand sz sg
507| Oor (sz, sg) -> h_Oor sz sg
508| Oxor (sz, sg) -> h_Oxor sz sg
509| Oshl (sz, sg) -> h_Oshl sz sg
510| Oshr (sz, sg) -> h_Oshr sz sg
511| Oshru (sz, sg) -> h_Oshru sz sg
512| Ocmp (sz, sg, sg', x_13454) -> h_Ocmp sz sg sg' x_13454
513| Ocmpu (sz, sg', x_13455) -> h_Ocmpu sz sg' x_13455
514| Oaddpi sz -> h_Oaddpi sz
515| Oaddip sz -> h_Oaddip sz
516| Osubpi sz -> h_Osubpi sz
517| Osubpp sz -> h_Osubpp sz
518| Ocmpp (sg', x_13456) -> h_Ocmpp sg' x_13456
519
520(** val binary_operation_rect_Type2 :
521    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
522    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
523    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
524    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
525    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
526    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
527    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
528    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
529    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
530    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
531    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
532    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
533let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13479 x_13478 x_13477 = function
534| Oadd (sz, sg) -> h_Oadd sz sg
535| Osub (sz, sg) -> h_Osub sz sg
536| Omul (sz, sg) -> h_Omul sz sg
537| Odiv sz -> h_Odiv sz
538| Odivu sz -> h_Odivu sz
539| Omod sz -> h_Omod sz
540| Omodu sz -> h_Omodu sz
541| Oand (sz, sg) -> h_Oand sz sg
542| Oor (sz, sg) -> h_Oor sz sg
543| Oxor (sz, sg) -> h_Oxor sz sg
544| Oshl (sz, sg) -> h_Oshl sz sg
545| Oshr (sz, sg) -> h_Oshr sz sg
546| Oshru (sz, sg) -> h_Oshru sz sg
547| Ocmp (sz, sg, sg', x_13481) -> h_Ocmp sz sg sg' x_13481
548| Ocmpu (sz, sg', x_13482) -> h_Ocmpu sz sg' x_13482
549| Oaddpi sz -> h_Oaddpi sz
550| Oaddip sz -> h_Oaddip sz
551| Osubpi sz -> h_Osubpi sz
552| Osubpp sz -> h_Osubpp sz
553| Ocmpp (sg', x_13483) -> h_Ocmpp sg' x_13483
554
555(** val binary_operation_rect_Type1 :
556    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
557    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
558    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
559    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
560    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
561    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
562    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
563    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
564    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
565    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
566    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
567    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
568let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13506 x_13505 x_13504 = function
569| Oadd (sz, sg) -> h_Oadd sz sg
570| Osub (sz, sg) -> h_Osub sz sg
571| Omul (sz, sg) -> h_Omul sz sg
572| Odiv sz -> h_Odiv sz
573| Odivu sz -> h_Odivu sz
574| Omod sz -> h_Omod sz
575| Omodu sz -> h_Omodu sz
576| Oand (sz, sg) -> h_Oand sz sg
577| Oor (sz, sg) -> h_Oor sz sg
578| Oxor (sz, sg) -> h_Oxor sz sg
579| Oshl (sz, sg) -> h_Oshl sz sg
580| Oshr (sz, sg) -> h_Oshr sz sg
581| Oshru (sz, sg) -> h_Oshru sz sg
582| Ocmp (sz, sg, sg', x_13508) -> h_Ocmp sz sg sg' x_13508
583| Ocmpu (sz, sg', x_13509) -> h_Ocmpu sz sg' x_13509
584| Oaddpi sz -> h_Oaddpi sz
585| Oaddip sz -> h_Oaddip sz
586| Osubpi sz -> h_Osubpi sz
587| Osubpp sz -> h_Osubpp sz
588| Ocmpp (sg', x_13510) -> h_Ocmpp sg' x_13510
589
590(** val binary_operation_rect_Type0 :
591    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
592    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
593    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
594    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
595    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
596    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
597    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
598    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
599    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
600    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
601    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
602    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
603let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13533 x_13532 x_13531 = function
604| Oadd (sz, sg) -> h_Oadd sz sg
605| Osub (sz, sg) -> h_Osub sz sg
606| Omul (sz, sg) -> h_Omul sz sg
607| Odiv sz -> h_Odiv sz
608| Odivu sz -> h_Odivu sz
609| Omod sz -> h_Omod sz
610| Omodu sz -> h_Omodu sz
611| Oand (sz, sg) -> h_Oand sz sg
612| Oor (sz, sg) -> h_Oor sz sg
613| Oxor (sz, sg) -> h_Oxor sz sg
614| Oshl (sz, sg) -> h_Oshl sz sg
615| Oshr (sz, sg) -> h_Oshr sz sg
616| Oshru (sz, sg) -> h_Oshru sz sg
617| Ocmp (sz, sg, sg', x_13535) -> h_Ocmp sz sg sg' x_13535
618| Ocmpu (sz, sg', x_13536) -> h_Ocmpu sz sg' x_13536
619| Oaddpi sz -> h_Oaddpi sz
620| Oaddip sz -> h_Oaddip sz
621| Osubpi sz -> h_Osubpi sz
622| Osubpp sz -> h_Osubpp sz
623| Ocmpp (sg', x_13537) -> h_Ocmpp sg' x_13537
624
625(** val binary_operation_inv_rect_Type4 :
626    AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
627    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
628    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
629    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
630    __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
631    (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
632    -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
633    -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
634    -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
635    -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
636    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
637    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
638    (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
639    -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
640    Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
641    -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
642    -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
643    __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
644    __ -> __ -> __ -> 'a1) -> 'a1 **)
645let binary_operation_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
646  let hcut =
647    binary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
648      h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
649  in
650  hcut __ __ __ __
651
652(** val binary_operation_inv_rect_Type3 :
653    AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
654    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
655    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
656    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
657    __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
658    (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
659    -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
660    -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
661    -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
662    -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
663    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
664    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
665    (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
666    -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
667    Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
668    -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
669    -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
670    __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
671    __ -> __ -> __ -> 'a1) -> 'a1 **)
672let binary_operation_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
673  let hcut =
674    binary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
675      h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
676  in
677  hcut __ __ __ __
678
679(** val binary_operation_inv_rect_Type2 :
680    AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
681    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
682    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
683    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
684    __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
685    (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
686    -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
687    -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
688    -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
689    -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
690    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
691    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
692    (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
693    -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
694    Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
695    -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
696    -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
697    __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
698    __ -> __ -> __ -> 'a1) -> 'a1 **)
699let binary_operation_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
700  let hcut =
701    binary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
702      h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
703  in
704  hcut __ __ __ __
705
706(** val binary_operation_inv_rect_Type1 :
707    AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
708    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
709    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
710    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
711    __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
712    (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
713    -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
714    -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
715    -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
716    -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
717    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
718    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
719    (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
720    -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
721    Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
722    -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
723    -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
724    __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
725    __ -> __ -> __ -> 'a1) -> 'a1 **)
726let binary_operation_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
727  let hcut =
728    binary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
729      h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
730  in
731  hcut __ __ __ __
732
733(** val binary_operation_inv_rect_Type0 :
734    AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
735    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
736    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
737    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
738    __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
739    (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
740    -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
741    -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
742    -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
743    -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
744    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
745    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
746    (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
747    -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
748    Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
749    -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
750    -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
751    __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
752    __ -> __ -> __ -> 'a1) -> 'a1 **)
753let binary_operation_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
754  let hcut =
755    binary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
756      h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
757  in
758  hcut __ __ __ __
759
760(** val binary_operation_discr :
761    AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation ->
762    __ **)
763let binary_operation_discr a1 a2 a3 x y =
764  Logic.eq_rect_Type2 x
765    (match x with
766     | Oadd (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
767     | Osub (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
768     | Omul (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
769     | Odiv a0 -> Obj.magic (fun _ dH -> dH __)
770     | Odivu a0 -> Obj.magic (fun _ dH -> dH __)
771     | Omod a0 -> Obj.magic (fun _ dH -> dH __)
772     | Omodu a0 -> Obj.magic (fun _ dH -> dH __)
773     | Oand (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
774     | Oor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
775     | Oxor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
776     | Oshl (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
777     | Oshr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
778     | Oshru (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
779     | Ocmp (a0, a10, a20, a30) -> Obj.magic (fun _ dH -> dH __ __ __ __)
780     | Ocmpu (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
781     | Oaddpi a0 -> Obj.magic (fun _ dH -> dH __)
782     | Oaddip a0 -> Obj.magic (fun _ dH -> dH __)
783     | Osubpi a0 -> Obj.magic (fun _ dH -> dH __)
784     | Osubpp a0 -> Obj.magic (fun _ dH -> dH __)
785     | Ocmpp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
786
787(** val binary_operation_jmdiscr :
788    AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation ->
789    __ **)
790let binary_operation_jmdiscr a1 a2 a3 x y =
791  Logic.eq_rect_Type2 x
792    (match x with
793     | Oadd (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
794     | Osub (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
795     | Omul (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
796     | Odiv a0 -> Obj.magic (fun _ dH -> dH __)
797     | Odivu a0 -> Obj.magic (fun _ dH -> dH __)
798     | Omod a0 -> Obj.magic (fun _ dH -> dH __)
799     | Omodu a0 -> Obj.magic (fun _ dH -> dH __)
800     | Oand (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
801     | Oor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
802     | Oxor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
803     | Oshl (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
804     | Oshr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
805     | Oshru (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
806     | Ocmp (a0, a10, a20, a30) -> Obj.magic (fun _ dH -> dH __ __ __ __)
807     | Ocmpu (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
808     | Oaddpi a0 -> Obj.magic (fun _ dH -> dH __)
809     | Oaddip a0 -> Obj.magic (fun _ dH -> dH __)
810     | Osubpi a0 -> Obj.magic (fun _ dH -> dH __)
811     | Osubpp a0 -> Obj.magic (fun _ dH -> dH __)
812     | Ocmpp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
813
814(** val eval_constant :
815    AST.typ -> (AST.ident -> Pointers.block Types.option) -> Pointers.block
816    -> constant -> Values.val0 Types.option **)
817let eval_constant t find_symbol sp = function
818| Ointconst (sz, sg, n) -> Types.Some (Values.Vint (sz, n))
819| Oaddrsymbol (s, ofs) ->
820  (match find_symbol s with
821   | Types.None -> Types.None
822   | Types.Some b ->
823     Types.Some (Values.Vptr { Pointers.pblock = b; Pointers.poff =
824       (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
825         Pointers.zero_offset (AST.repr AST.I16 ofs)) }))
826| Oaddrstack ofs ->
827  Types.Some (Values.Vptr { Pointers.pblock = sp; Pointers.poff =
828    (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
829      Pointers.zero_offset (AST.repr AST.I16 ofs)) })
830
831(** val eval_unop :
832    AST.typ -> AST.typ -> unary_operation -> Values.val0 -> Values.val0
833    Types.option **)
834let eval_unop t t' op arg =
835  match op with
836  | Ocastint (sz, sg, sz', sg') ->
837    (match sg with
838     | AST.Signed -> Types.Some (Values.sign_ext sz' arg)
839     | AST.Unsigned -> Types.Some (Values.zero_ext sz' arg))
840  | Onegint (sz, sg) ->
841    (match arg with
842     | Values.Vundef -> Types.None
843     | Values.Vint (sz1, n1) ->
844       Types.Some (Values.Vint (sz1,
845         (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz1) n1)))
846     | Values.Vnull -> Types.None
847     | Values.Vptr x -> Types.None)
848  | Onotbool (t0, sz, sg) ->
849    (match arg with
850     | Values.Vundef -> Types.None
851     | Values.Vint (sz1, n1) ->
852       Types.Some (Values.Vint (sz,
853         (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
854                  (BitVector.zero (AST.bitsize_of_intsize sz1)) with
855          | Bool.True -> AST.repr sz (Nat.S Nat.O)
856          | Bool.False -> BitVector.zero (AST.bitsize_of_intsize sz))))
857     | Values.Vnull ->
858       Types.Some (Values.Vint (sz, (AST.repr sz (Nat.S Nat.O))))
859     | Values.Vptr x0 ->
860       Types.Some (Values.Vint (sz,
861         (BitVector.zero (AST.bitsize_of_intsize sz)))))
862  | Onotint (sz, sg) ->
863    (match arg with
864     | Values.Vundef -> Types.None
865     | Values.Vint (sz1, n1) ->
866       Types.Some (Values.Vint (sz1,
867         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz1) n1
868           (Values.mone sz1))))
869     | Values.Vnull -> Types.None
870     | Values.Vptr x -> Types.None)
871  | Oid t0 -> Types.Some arg
872  | Optrofint (sz, sg) ->
873    (match arg with
874     | Values.Vundef -> Types.None
875     | Values.Vint (sz1, n1) ->
876       (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
877                (BitVector.zero (AST.bitsize_of_intsize sz1)) with
878        | Bool.True -> Types.Some Values.Vnull
879        | Bool.False -> Types.None)
880     | Values.Vnull -> Types.None
881     | Values.Vptr x -> Types.None)
882  | Ointofptr (sz, sg) ->
883    (match arg with
884     | Values.Vundef -> Types.None
885     | Values.Vint (x, x0) -> Types.None
886     | Values.Vnull ->
887       Types.Some (Values.Vint (sz,
888         (BitVector.zero (AST.bitsize_of_intsize sz))))
889     | Values.Vptr x -> Types.None)
890
891(** val eval_compare_mismatch :
892    Integers.comparison -> Values.val0 Types.option **)
893let eval_compare_mismatch = function
894| Integers.Ceq -> Types.Some Values.vfalse
895| Integers.Cne -> Types.Some Values.vtrue
896| Integers.Clt -> Types.None
897| Integers.Cle -> Types.None
898| Integers.Cgt -> Types.None
899| Integers.Cge -> Types.None
900
901(** val ev_add : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
902let ev_add v1 v2 =
903  match v1 with
904  | Values.Vundef -> Types.None
905  | Values.Vint (sz1, n1) ->
906    (match v2 with
907     | Values.Vundef -> Types.None
908     | Values.Vint (sz2, n2) ->
909       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
910         (sz2, (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))))
911         Types.None
912     | Values.Vnull -> Types.None
913     | Values.Vptr x -> Types.None)
914  | Values.Vnull -> Types.None
915  | Values.Vptr x -> Types.None
916
917(** val ev_sub : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
918let ev_sub v1 v2 =
919  match v1 with
920  | Values.Vundef -> Types.None
921  | Values.Vint (sz1, n1) ->
922    (match v2 with
923     | Values.Vundef -> Types.None
924     | Values.Vint (sz2, n2) ->
925       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
926         (sz2,
927         (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2))))
928         Types.None
929     | Values.Vnull -> Types.None
930     | Values.Vptr x -> Types.None)
931  | Values.Vnull -> Types.None
932  | Values.Vptr x -> Types.None
933
934(** val ev_addpi : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
935let ev_addpi v1 v2 =
936  match v1 with
937  | Values.Vundef -> Types.None
938  | Values.Vint (x, x0) -> Types.None
939  | Values.Vnull ->
940    (match v2 with
941     | Values.Vundef -> Types.None
942     | Values.Vint (sz2, n2) ->
943       (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
944                (BitVector.zero (AST.bitsize_of_intsize sz2)) with
945        | Bool.True -> Types.Some Values.Vnull
946        | Bool.False -> Types.None)
947     | Values.Vnull -> Types.None
948     | Values.Vptr x -> Types.None)
949  | Values.Vptr ptr1 ->
950    (match v2 with
951     | Values.Vundef -> Types.None
952     | Values.Vint (sz2, n2) ->
953       Types.Some (Values.Vptr
954         (Pointers.shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2))
955     | Values.Vnull -> Types.None
956     | Values.Vptr x -> Types.None)
957
958(** val ev_subpi : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
959let ev_subpi v1 v2 =
960  match v1 with
961  | Values.Vundef -> Types.None
962  | Values.Vint (x, x0) -> Types.None
963  | Values.Vnull ->
964    (match v2 with
965     | Values.Vundef -> Types.None
966     | Values.Vint (sz2, n2) ->
967       (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
968                (BitVector.zero (AST.bitsize_of_intsize sz2)) with
969        | Bool.True -> Types.Some Values.Vnull
970        | Bool.False -> Types.None)
971     | Values.Vnull -> Types.None
972     | Values.Vptr x -> Types.None)
973  | Values.Vptr ptr1 ->
974    (match v2 with
975     | Values.Vundef -> Types.None
976     | Values.Vint (sz2, n2) ->
977       Types.Some (Values.Vptr
978         (Pointers.neg_shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2))
979     | Values.Vnull -> Types.None
980     | Values.Vptr x -> Types.None)
981
982(** val ev_subpp :
983    AST.intsize -> Values.val0 -> Values.val0 -> Values.val0 Types.option **)
984let ev_subpp sz v1 v2 =
985  match v1 with
986  | Values.Vundef -> Types.None
987  | Values.Vint (x, x0) -> Types.None
988  | Values.Vnull ->
989    (match v2 with
990     | Values.Vundef -> Types.None
991     | Values.Vint (x, x0) -> Types.None
992     | Values.Vnull ->
993       Types.Some (Values.Vint (sz,
994         (BitVector.zero (AST.bitsize_of_intsize sz))))
995     | Values.Vptr x -> Types.None)
996  | Values.Vptr ptr1 ->
997    (match v2 with
998     | Values.Vundef -> Types.None
999     | Values.Vint (x, x0) -> Types.None
1000     | Values.Vnull -> Types.None
1001     | Values.Vptr ptr2 ->
1002       (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
1003        | Bool.True ->
1004          Types.Some (Values.Vint (sz,
1005            (Pointers.sub_offset (AST.bitsize_of_intsize sz)
1006              ptr1.Pointers.poff ptr2.Pointers.poff)))
1007        | Bool.False -> Types.None))
1008
1009(** val ev_mul : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1010let ev_mul v1 v2 =
1011  match v1 with
1012  | Values.Vundef -> Types.None
1013  | Values.Vint (sz1, n1) ->
1014    (match v2 with
1015     | Values.Vundef -> Types.None
1016     | Values.Vint (sz2, n2) ->
1017       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1018         (sz2,
1019         (Arithmetic.short_multiplication (AST.bitsize_of_intsize sz2) n10
1020           n2)))) Types.None
1021     | Values.Vnull -> Types.None
1022     | Values.Vptr x -> Types.None)
1023  | Values.Vnull -> Types.None
1024  | Values.Vptr x -> Types.None
1025
1026(** val ev_divs : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1027let ev_divs v1 v2 =
1028  match v1 with
1029  | Values.Vundef -> Types.None
1030  | Values.Vint (sz1, n1) ->
1031    (match v2 with
1032     | Values.Vundef -> Types.None
1033     | Values.Vint (sz2, n2) ->
1034       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1035         Types.option_map (fun x -> Values.Vint (sz2, x))
1036           (Arithmetic.division_s (AST.bitsize_of_intsize sz2) n10 n2))
1037         Types.None
1038     | Values.Vnull -> Types.None
1039     | Values.Vptr x -> Types.None)
1040  | Values.Vnull -> Types.None
1041  | Values.Vptr x -> Types.None
1042
1043(** val ev_mods : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1044let ev_mods v1 v2 =
1045  match v1 with
1046  | Values.Vundef -> Types.None
1047  | Values.Vint (sz1, n1) ->
1048    (match v2 with
1049     | Values.Vundef -> Types.None
1050     | Values.Vint (sz2, n2) ->
1051       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1052         Types.option_map (fun x -> Values.Vint (sz2, x))
1053           (Arithmetic.modulus_s (AST.bitsize_of_intsize sz2) n10 n2))
1054         Types.None
1055     | Values.Vnull -> Types.None
1056     | Values.Vptr x -> Types.None)
1057  | Values.Vnull -> Types.None
1058  | Values.Vptr x -> Types.None
1059
1060(** val ev_divu : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1061let ev_divu v1 v2 =
1062  match v1 with
1063  | Values.Vundef -> Types.None
1064  | Values.Vint (sz1, n1) ->
1065    (match v2 with
1066     | Values.Vundef -> Types.None
1067     | Values.Vint (sz2, n2) ->
1068       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1069         Types.option_map (fun x -> Values.Vint (sz2, x))
1070           (Arithmetic.division_u
1071             (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1072               Nat.O)))))))
1073               (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S (Nat.S
1074                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n10 n2))
1075         Types.None
1076     | Values.Vnull -> Types.None
1077     | Values.Vptr x -> Types.None)
1078  | Values.Vnull -> Types.None
1079  | Values.Vptr x -> Types.None
1080
1081(** val ev_modu : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1082let ev_modu v1 v2 =
1083  match v1 with
1084  | Values.Vundef -> Types.None
1085  | Values.Vint (sz1, n1) ->
1086    (match v2 with
1087     | Values.Vundef -> Types.None
1088     | Values.Vint (sz2, n2) ->
1089       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1090         Types.option_map (fun x -> Values.Vint (sz2, x))
1091           (Arithmetic.modulus_u
1092             (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1093               Nat.O)))))))
1094               (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S (Nat.S
1095                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n10 n2))
1096         Types.None
1097     | Values.Vnull -> Types.None
1098     | Values.Vptr x -> Types.None)
1099  | Values.Vnull -> Types.None
1100  | Values.Vptr x -> Types.None
1101
1102(** val ev_and : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1103let ev_and v1 v2 =
1104  match v1 with
1105  | Values.Vundef -> Types.None
1106  | Values.Vint (sz1, n1) ->
1107    (match v2 with
1108     | Values.Vundef -> Types.None
1109     | Values.Vint (sz2, n2) ->
1110       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1111         (sz2,
1112         (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2))))
1113         Types.None
1114     | Values.Vnull -> Types.None
1115     | Values.Vptr x -> Types.None)
1116  | Values.Vnull -> Types.None
1117  | Values.Vptr x -> Types.None
1118
1119(** val ev_or : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1120let ev_or v1 v2 =
1121  match v1 with
1122  | Values.Vundef -> Types.None
1123  | Values.Vint (sz1, n1) ->
1124    (match v2 with
1125     | Values.Vundef -> Types.None
1126     | Values.Vint (sz2, n2) ->
1127       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1128         (sz2,
1129         (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
1130           n2)))) Types.None
1131     | Values.Vnull -> Types.None
1132     | Values.Vptr x -> Types.None)
1133  | Values.Vnull -> Types.None
1134  | Values.Vptr x -> Types.None
1135
1136(** val ev_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1137let ev_xor v1 v2 =
1138  match v1 with
1139  | Values.Vundef -> Types.None
1140  | Values.Vint (sz1, n1) ->
1141    (match v2 with
1142     | Values.Vundef -> Types.None
1143     | Values.Vint (sz2, n2) ->
1144       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1145         (sz2,
1146         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
1147           n2)))) Types.None
1148     | Values.Vnull -> Types.None
1149     | Values.Vptr x -> Types.None)
1150  | Values.Vnull -> Types.None
1151  | Values.Vptr x -> Types.None
1152
1153(** val ev_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1154let ev_shl v1 v2 =
1155  match v1 with
1156  | Values.Vundef -> Types.None
1157  | Values.Vint (sz1, n1) ->
1158    (match v2 with
1159     | Values.Vundef -> Types.None
1160     | Values.Vint (sz2, n2) ->
1161       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1162                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1163                  (AST.bitsize_of_intsize sz1)) with
1164        | Bool.True ->
1165          Types.Some (Values.Vint (sz1,
1166            (Vector.shift_left (AST.bitsize_of_intsize sz1)
1167              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1168              n1 Bool.False)))
1169        | Bool.False -> Types.None)
1170     | Values.Vnull -> Types.None
1171     | Values.Vptr x -> Types.None)
1172  | Values.Vnull -> Types.None
1173  | Values.Vptr x -> Types.None
1174
1175(** val ev_shr : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1176let ev_shr v1 v2 =
1177  match v1 with
1178  | Values.Vundef -> Types.None
1179  | Values.Vint (sz1, n1) ->
1180    (match v2 with
1181     | Values.Vundef -> Types.None
1182     | Values.Vint (sz2, n2) ->
1183       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1184                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1185                  (AST.bitsize_of_intsize sz1)) with
1186        | Bool.True ->
1187          Types.Some (Values.Vint (sz1,
1188            (Vector.shift_right
1189              (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1190                Nat.O)))))))
1191                (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1192                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
1193              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1194              n1
1195              (Vector.head'
1196                (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1197                  Nat.O)))))))
1198                  (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1199                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n1))))
1200        | Bool.False -> Types.None)
1201     | Values.Vnull -> Types.None
1202     | Values.Vptr x -> Types.None)
1203  | Values.Vnull -> Types.None
1204  | Values.Vptr x -> Types.None
1205
1206(** val ev_shru : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1207let ev_shru v1 v2 =
1208  match v1 with
1209  | Values.Vundef -> Types.None
1210  | Values.Vint (sz1, n1) ->
1211    (match v2 with
1212     | Values.Vundef -> Types.None
1213     | Values.Vint (sz2, n2) ->
1214       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1215                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1216                  (AST.bitsize_of_intsize sz1)) with
1217        | Bool.True ->
1218          Types.Some (Values.Vint (sz1,
1219            (Vector.shift_right
1220              (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1221                Nat.O)))))))
1222                (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1223                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
1224              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1225              n1 Bool.False)))
1226        | Bool.False -> Types.None)
1227     | Values.Vnull -> Types.None
1228     | Values.Vptr x -> Types.None)
1229  | Values.Vnull -> Types.None
1230  | Values.Vptr x -> Types.None
1231
1232(** val fEtrue : Values.val0 **)
1233let fEtrue =
1234  Values.Vint (AST.I8, (AST.repr AST.I8 (Nat.S Nat.O)))
1235
1236(** val fEfalse : Values.val0 **)
1237let fEfalse =
1238  Values.Vint (AST.I8, (AST.repr AST.I8 Nat.O))
1239
1240(** val fE_of_bool : Bool.bool -> Values.val0 **)
1241let fE_of_bool = function
1242| Bool.True -> fEtrue
1243| Bool.False -> fEfalse
1244
1245(** val ev_cmp_match : Integers.comparison -> Values.val0 Types.option **)
1246let ev_cmp_match = function
1247| Integers.Ceq -> Types.Some fEtrue
1248| Integers.Cne -> Types.Some fEfalse
1249| Integers.Clt -> Types.None
1250| Integers.Cle -> Types.None
1251| Integers.Cgt -> Types.None
1252| Integers.Cge -> Types.None
1253
1254(** val ev_cmp_mismatch : Integers.comparison -> Values.val0 Types.option **)
1255let ev_cmp_mismatch = function
1256| Integers.Ceq -> Types.Some fEfalse
1257| Integers.Cne -> Types.Some fEtrue
1258| Integers.Clt -> Types.None
1259| Integers.Cle -> Types.None
1260| Integers.Cgt -> Types.None
1261| Integers.Cge -> Types.None
1262
1263(** val ev_cmp :
1264    Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
1265    Types.option **)
1266let ev_cmp c v1 v2 =
1267  match v1 with
1268  | Values.Vundef -> Types.None
1269  | Values.Vint (sz1, n1) ->
1270    (match v2 with
1271     | Values.Vundef -> Types.None
1272     | Values.Vint (sz2, n2) ->
1273       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
1274         (fE_of_bool (Values.cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)))
1275         Types.None
1276     | Values.Vnull -> Types.None
1277     | Values.Vptr x -> Types.None)
1278  | Values.Vnull -> Types.None
1279  | Values.Vptr x -> Types.None
1280
1281(** val ev_cmpp :
1282    GenMem.mem -> Integers.comparison -> Values.val0 -> Values.val0 ->
1283    Values.val0 Types.option **)
1284let ev_cmpp m c v1 v2 =
1285  match v1 with
1286  | Values.Vundef -> Types.None
1287  | Values.Vint (x, x0) -> Types.None
1288  | Values.Vnull ->
1289    (match v2 with
1290     | Values.Vundef -> Types.None
1291     | Values.Vint (x, x0) -> Types.None
1292     | Values.Vnull -> ev_cmp_match c
1293     | Values.Vptr x -> ev_cmp_mismatch c)
1294  | Values.Vptr ptr1 ->
1295    (match v2 with
1296     | Values.Vundef -> Types.None
1297     | Values.Vint (x, x0) -> Types.None
1298     | Values.Vnull -> ev_cmp_mismatch c
1299     | Values.Vptr ptr2 ->
1300       (match Bool.andb (FrontEndMem.valid_pointer m ptr1)
1301                (FrontEndMem.valid_pointer m ptr2) with
1302        | Bool.True ->
1303          (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
1304           | Bool.True ->
1305             Types.Some
1306               (fE_of_bool
1307                 (Values.cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff))
1308           | Bool.False -> ev_cmp_mismatch c)
1309        | Bool.False -> Types.None))
1310
1311(** val ev_cmpu :
1312    Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
1313    Types.option **)
1314let ev_cmpu c v1 v2 =
1315  match v1 with
1316  | Values.Vundef -> Types.None
1317  | Values.Vint (sz1, n1) ->
1318    (match v2 with
1319     | Values.Vundef -> Types.None
1320     | Values.Vint (sz2, n2) ->
1321       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
1322         (fE_of_bool (Values.cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)))
1323         Types.None
1324     | Values.Vnull -> Types.None
1325     | Values.Vptr x -> Types.None)
1326  | Values.Vnull -> Types.None
1327  | Values.Vptr x -> Types.None
1328
1329(** val eval_binop :
1330    GenMem.mem -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
1331    Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1332let eval_binop m t1 t2 t' = function
1333| Oadd (x, x0) -> ev_add
1334| Osub (x, x0) -> ev_sub
1335| Omul (x, x0) -> ev_mul
1336| Odiv x -> ev_divs
1337| Odivu x -> ev_divu
1338| Omod x -> ev_mods
1339| Omodu x -> ev_modu
1340| Oand (x, x0) -> ev_and
1341| Oor (x, x0) -> ev_or
1342| Oxor (x, x0) -> ev_xor
1343| Oshl (x, x0) -> ev_shl
1344| Oshr (x, x0) -> ev_shr
1345| Oshru (x, x0) -> ev_shru
1346| Ocmp (x, x0, x1, c) -> ev_cmp c
1347| Ocmpu (x, x0, c) -> ev_cmpu c
1348| Oaddpi x -> ev_addpi
1349| Oaddip x -> (fun x0 y -> ev_addpi y x0)
1350| Osubpi x -> ev_subpi
1351| Osubpp sz -> ev_subpp sz
1352| Ocmpp (x, c) -> ev_cmpp m c
1353
Note: See TracBrowser for help on using the repository browser.