source: extracted/frontEndOps.ml @ 2716

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

...

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