source: extracted/frontEndOps.ml @ 3009

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

New extraction.

File size: 56.8 KB
RevLine 
[2601]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
[2717]21open Exp
22
[2601]23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
[2649]39open ErrorMessages
40
[2601]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 **)
[3001]101let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_6050 = function
102| Ointconst (sz, sg, x_6052) -> h_Ointconst sz sg x_6052
103| Oaddrsymbol (x_6054, x_6053) -> h_Oaddrsymbol x_6054 x_6053
104| Oaddrstack x_6055 -> h_Oaddrstack x_6055
[2601]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 **)
[3001]109let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_6059 = function
110| Ointconst (sz, sg, x_6061) -> h_Ointconst sz sg x_6061
111| Oaddrsymbol (x_6063, x_6062) -> h_Oaddrsymbol x_6063 x_6062
112| Oaddrstack x_6064 -> h_Oaddrstack x_6064
[2601]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 **)
[3001]117let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_6068 = function
118| Ointconst (sz, sg, x_6070) -> h_Ointconst sz sg x_6070
119| Oaddrsymbol (x_6072, x_6071) -> h_Oaddrsymbol x_6072 x_6071
120| Oaddrstack x_6073 -> h_Oaddrstack x_6073
[2601]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 **)
[3001]125let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_6077 = function
126| Ointconst (sz, sg, x_6079) -> h_Ointconst sz sg x_6079
127| Oaddrsymbol (x_6081, x_6080) -> h_Oaddrsymbol x_6081 x_6080
128| Oaddrstack x_6082 -> h_Oaddrstack x_6082
[2601]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 **)
[3001]133let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_6086 = function
134| Ointconst (sz, sg, x_6088) -> h_Ointconst sz sg x_6088
135| Oaddrsymbol (x_6090, x_6089) -> h_Oaddrsymbol x_6090 x_6089
136| Oaddrstack x_6091 -> h_Oaddrstack x_6091
[2601]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 **)
[3001]141let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_6095 = function
142| Ointconst (sz, sg, x_6097) -> h_Ointconst sz sg x_6097
143| Oaddrsymbol (x_6099, x_6098) -> h_Oaddrsymbol x_6099 x_6098
144| Oaddrstack x_6100 -> h_Oaddrstack x_6100
[2601]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 **)
[3001]213let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_6170 x_6169 = function
[2601]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 **)
[3001]229let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_6181 x_6180 = function
[2601]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 **)
[3001]245let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_6192 x_6191 = function
[2601]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 **)
[3001]261let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_6203 x_6202 = function
[2601]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 **)
[3001]277let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_6214 x_6213 = function
[2601]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 **)
[3001]293let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_6225 x_6224 = function
[2601]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 **)
[3001]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_6330 x_6329 x_6328 = function
[2601]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
[3001]442| Ocmp (sz, sg, sg', x_6332) -> h_Ocmp sz sg sg' x_6332
443| Ocmpu (sz, sg', x_6333) -> h_Ocmpu sz sg' x_6333
[2601]444| Oaddpi sz -> h_Oaddpi sz
445| Oaddip sz -> h_Oaddip sz
446| Osubpi sz -> h_Osubpi sz
447| Osubpp sz -> h_Osubpp sz
[3001]448| Ocmpp (sg', x_6334) -> h_Ocmpp sg' x_6334
[2601]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 **)
[3001]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_6357 x_6356 x_6355 = function
[2601]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
[3001]477| Ocmp (sz, sg, sg', x_6359) -> h_Ocmp sz sg sg' x_6359
478| Ocmpu (sz, sg', x_6360) -> h_Ocmpu sz sg' x_6360
[2601]479| Oaddpi sz -> h_Oaddpi sz
480| Oaddip sz -> h_Oaddip sz
481| Osubpi sz -> h_Osubpi sz
482| Osubpp sz -> h_Osubpp sz
[3001]483| Ocmpp (sg', x_6361) -> h_Ocmpp sg' x_6361
[2601]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 **)
[3001]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_6384 x_6383 x_6382 = function
[2601]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
[3001]512| Ocmp (sz, sg, sg', x_6386) -> h_Ocmp sz sg sg' x_6386
513| Ocmpu (sz, sg', x_6387) -> h_Ocmpu sz sg' x_6387
[2601]514| Oaddpi sz -> h_Oaddpi sz
515| Oaddip sz -> h_Oaddip sz
516| Osubpi sz -> h_Osubpi sz
517| Osubpp sz -> h_Osubpp sz
[3001]518| Ocmpp (sg', x_6388) -> h_Ocmpp sg' x_6388
[2601]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 **)
[3001]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_6411 x_6410 x_6409 = function
[2601]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
[3001]547| Ocmp (sz, sg, sg', x_6413) -> h_Ocmp sz sg sg' x_6413
548| Ocmpu (sz, sg', x_6414) -> h_Ocmpu sz sg' x_6414
[2601]549| Oaddpi sz -> h_Oaddpi sz
550| Oaddip sz -> h_Oaddip sz
551| Osubpi sz -> h_Osubpi sz
552| Osubpp sz -> h_Osubpp sz
[3001]553| Ocmpp (sg', x_6415) -> h_Ocmpp sg' x_6415
[2601]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 **)
[3001]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_6438 x_6437 x_6436 = function
[2601]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
[3001]582| Ocmp (sz, sg, sg', x_6440) -> h_Ocmp sz sg sg' x_6440
583| Ocmpu (sz, sg', x_6441) -> h_Ocmpu sz sg' x_6441
[2601]584| Oaddpi sz -> h_Oaddpi sz
585| Oaddip sz -> h_Oaddip sz
586| Osubpi sz -> h_Osubpi sz
587| Osubpp sz -> h_Osubpp sz
[3001]588| Ocmpp (sg', x_6442) -> h_Ocmpp sg' x_6442
[2601]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 **)
[3001]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_6465 x_6464 x_6463 = function
[2601]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
[3001]617| Ocmp (sz, sg, sg', x_6467) -> h_Ocmp sz sg sg' x_6467
618| Ocmpu (sz, sg', x_6468) -> h_Ocmpu sz sg' x_6468
[2601]619| Oaddpi sz -> h_Oaddpi sz
620| Oaddip sz -> h_Oaddip sz
621| Osubpi sz -> h_Osubpi sz
622| Osubpp sz -> h_Osubpp sz
[3001]623| Ocmpp (sg', x_6469) -> h_Ocmpp sg' x_6469
[2601]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)
[2773]825         Pointers.zero_offset (AST.repr AST.I16 ofs)) }))
[2601]826| Oaddrstack ofs ->
827  Types.Some (Values.Vptr { Pointers.pblock = sp; Pointers.poff =
828    (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
[2773]829      Pointers.zero_offset (AST.repr AST.I16 ofs)) })
[2601]830
831(** val eval_unop :
832    AST.typ -> AST.typ -> unary_operation -> Values.val0 -> Values.val0
833    Types.option **)
[2773]834let eval_unop t t' op arg =
835  match op with
[2601]836  | Ocastint (sz, sg, sz', sg') ->
837    (match sg with
[2773]838     | AST.Signed -> Types.Some (Values.sign_ext sz' arg)
839     | AST.Unsigned -> Types.Some (Values.zero_ext sz' arg))
[2601]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
[2773]855          | Bool.True -> AST.repr sz (Nat.S Nat.O)
[2601]856          | Bool.False -> BitVector.zero (AST.bitsize_of_intsize sz))))
857     | Values.Vnull ->
[2773]858       Types.Some (Values.Vint (sz, (AST.repr sz (Nat.S Nat.O))))
[2601]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
[2773]868           (Values.mone sz1))))
[2601]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 ->
[3001]1002       (match Pointers.eq_block (Pointers.pblock ptr1)
1003                (Pointers.pblock ptr2) with
[2601]1004        | Bool.True ->
1005          Types.Some (Values.Vint (sz,
1006            (Pointers.sub_offset (AST.bitsize_of_intsize sz)
[3001]1007              (Pointers.poff ptr1) (Pointers.poff ptr2))))
[2601]1008        | Bool.False -> Types.None))
1009
1010(** val ev_mul : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1011let ev_mul v1 v2 =
1012  match v1 with
1013  | Values.Vundef -> Types.None
1014  | Values.Vint (sz1, n1) ->
1015    (match v2 with
1016     | Values.Vundef -> Types.None
1017     | Values.Vint (sz2, n2) ->
1018       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1019         (sz2,
1020         (Arithmetic.short_multiplication (AST.bitsize_of_intsize sz2) n10
1021           n2)))) Types.None
1022     | Values.Vnull -> Types.None
1023     | Values.Vptr x -> Types.None)
1024  | Values.Vnull -> Types.None
1025  | Values.Vptr x -> Types.None
1026
1027(** val ev_divs : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1028let ev_divs v1 v2 =
1029  match v1 with
1030  | Values.Vundef -> Types.None
1031  | Values.Vint (sz1, n1) ->
1032    (match v2 with
1033     | Values.Vundef -> Types.None
1034     | Values.Vint (sz2, n2) ->
1035       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1036         Types.option_map (fun x -> Values.Vint (sz2, x))
1037           (Arithmetic.division_s (AST.bitsize_of_intsize sz2) n10 n2))
1038         Types.None
1039     | Values.Vnull -> Types.None
1040     | Values.Vptr x -> Types.None)
1041  | Values.Vnull -> Types.None
1042  | Values.Vptr x -> Types.None
1043
1044(** val ev_mods : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1045let ev_mods v1 v2 =
1046  match v1 with
1047  | Values.Vundef -> Types.None
1048  | Values.Vint (sz1, n1) ->
1049    (match v2 with
1050     | Values.Vundef -> Types.None
1051     | Values.Vint (sz2, n2) ->
1052       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1053         Types.option_map (fun x -> Values.Vint (sz2, x))
1054           (Arithmetic.modulus_s (AST.bitsize_of_intsize sz2) n10 n2))
1055         Types.None
1056     | Values.Vnull -> Types.None
1057     | Values.Vptr x -> Types.None)
1058  | Values.Vnull -> Types.None
1059  | Values.Vptr x -> Types.None
1060
1061(** val ev_divu : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1062let ev_divu v1 v2 =
1063  match v1 with
1064  | Values.Vundef -> Types.None
1065  | Values.Vint (sz1, n1) ->
1066    (match v2 with
1067     | Values.Vundef -> Types.None
1068     | Values.Vint (sz2, n2) ->
1069       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1070         Types.option_map (fun x -> Values.Vint (sz2, x))
1071           (Arithmetic.division_u
1072             (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1073               Nat.O)))))))
1074               (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S (Nat.S
1075                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n10 n2))
1076         Types.None
1077     | Values.Vnull -> Types.None
1078     | Values.Vptr x -> Types.None)
1079  | Values.Vnull -> Types.None
1080  | Values.Vptr x -> Types.None
1081
1082(** val ev_modu : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1083let ev_modu v1 v2 =
1084  match v1 with
1085  | Values.Vundef -> Types.None
1086  | Values.Vint (sz1, n1) ->
1087    (match v2 with
1088     | Values.Vundef -> Types.None
1089     | Values.Vint (sz2, n2) ->
1090       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1091         Types.option_map (fun x -> Values.Vint (sz2, x))
1092           (Arithmetic.modulus_u
1093             (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1094               Nat.O)))))))
1095               (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S (Nat.S
1096                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n10 n2))
1097         Types.None
1098     | Values.Vnull -> Types.None
1099     | Values.Vptr x -> Types.None)
1100  | Values.Vnull -> Types.None
1101  | Values.Vptr x -> Types.None
1102
1103(** val ev_and : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1104let ev_and v1 v2 =
1105  match v1 with
1106  | Values.Vundef -> Types.None
1107  | Values.Vint (sz1, n1) ->
1108    (match v2 with
1109     | Values.Vundef -> Types.None
1110     | Values.Vint (sz2, n2) ->
1111       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1112         (sz2,
1113         (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2))))
1114         Types.None
1115     | Values.Vnull -> Types.None
1116     | Values.Vptr x -> Types.None)
1117  | Values.Vnull -> Types.None
1118  | Values.Vptr x -> Types.None
1119
1120(** val ev_or : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1121let ev_or v1 v2 =
1122  match v1 with
1123  | Values.Vundef -> Types.None
1124  | Values.Vint (sz1, n1) ->
1125    (match v2 with
1126     | Values.Vundef -> Types.None
1127     | Values.Vint (sz2, n2) ->
1128       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1129         (sz2,
1130         (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
1131           n2)))) Types.None
1132     | Values.Vnull -> Types.None
1133     | Values.Vptr x -> Types.None)
1134  | Values.Vnull -> Types.None
1135  | Values.Vptr x -> Types.None
1136
1137(** val ev_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1138let ev_xor v1 v2 =
1139  match v1 with
1140  | Values.Vundef -> Types.None
1141  | Values.Vint (sz1, n1) ->
1142    (match v2 with
1143     | Values.Vundef -> Types.None
1144     | Values.Vint (sz2, n2) ->
1145       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1146         (sz2,
1147         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
1148           n2)))) Types.None
1149     | Values.Vnull -> Types.None
1150     | Values.Vptr x -> Types.None)
1151  | Values.Vnull -> Types.None
1152  | Values.Vptr x -> Types.None
1153
1154(** val ev_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1155let ev_shl v1 v2 =
1156  match v1 with
1157  | Values.Vundef -> Types.None
1158  | Values.Vint (sz1, n1) ->
1159    (match v2 with
1160     | Values.Vundef -> Types.None
1161     | Values.Vint (sz2, n2) ->
1162       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1163                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1164                  (AST.bitsize_of_intsize sz1)) with
1165        | Bool.True ->
1166          Types.Some (Values.Vint (sz1,
1167            (Vector.shift_left (AST.bitsize_of_intsize sz1)
1168              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1169              n1 Bool.False)))
1170        | Bool.False -> Types.None)
1171     | Values.Vnull -> Types.None
1172     | Values.Vptr x -> Types.None)
1173  | Values.Vnull -> Types.None
1174  | Values.Vptr x -> Types.None
1175
1176(** val ev_shr : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1177let ev_shr v1 v2 =
1178  match v1 with
1179  | Values.Vundef -> Types.None
1180  | Values.Vint (sz1, n1) ->
1181    (match v2 with
1182     | Values.Vundef -> Types.None
1183     | Values.Vint (sz2, n2) ->
1184       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1185                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1186                  (AST.bitsize_of_intsize sz1)) with
1187        | Bool.True ->
1188          Types.Some (Values.Vint (sz1,
1189            (Vector.shift_right
1190              (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1191                Nat.O)))))))
1192                (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1193                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
1194              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1195              n1
1196              (Vector.head'
1197                (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1198                  Nat.O)))))))
1199                  (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1200                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n1))))
1201        | Bool.False -> Types.None)
1202     | Values.Vnull -> Types.None
1203     | Values.Vptr x -> Types.None)
1204  | Values.Vnull -> Types.None
1205  | Values.Vptr x -> Types.None
1206
1207(** val ev_shru : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1208let ev_shru v1 v2 =
1209  match v1 with
1210  | Values.Vundef -> Types.None
1211  | Values.Vint (sz1, n1) ->
1212    (match v2 with
1213     | Values.Vundef -> Types.None
1214     | Values.Vint (sz2, n2) ->
1215       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1216                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1217                  (AST.bitsize_of_intsize sz1)) with
1218        | Bool.True ->
1219          Types.Some (Values.Vint (sz1,
1220            (Vector.shift_right
1221              (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1222                Nat.O)))))))
1223                (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1224                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
1225              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1226              n1 Bool.False)))
1227        | Bool.False -> Types.None)
1228     | Values.Vnull -> Types.None
1229     | Values.Vptr x -> Types.None)
1230  | Values.Vnull -> Types.None
1231  | Values.Vptr x -> Types.None
1232
1233(** val fEtrue : Values.val0 **)
1234let fEtrue =
[2773]1235  Values.Vint (AST.I8, (AST.repr AST.I8 (Nat.S Nat.O)))
[2601]1236
1237(** val fEfalse : Values.val0 **)
1238let fEfalse =
[2773]1239  Values.Vint (AST.I8, (AST.repr AST.I8 Nat.O))
[2601]1240
1241(** val fE_of_bool : Bool.bool -> Values.val0 **)
1242let fE_of_bool = function
1243| Bool.True -> fEtrue
1244| Bool.False -> fEfalse
1245
1246(** val ev_cmp_match : Integers.comparison -> Values.val0 Types.option **)
1247let ev_cmp_match = function
1248| Integers.Ceq -> Types.Some fEtrue
1249| Integers.Cne -> Types.Some fEfalse
1250| Integers.Clt -> Types.None
1251| Integers.Cle -> Types.None
1252| Integers.Cgt -> Types.None
1253| Integers.Cge -> Types.None
1254
1255(** val ev_cmp_mismatch : Integers.comparison -> Values.val0 Types.option **)
1256let ev_cmp_mismatch = function
1257| Integers.Ceq -> Types.Some fEfalse
1258| Integers.Cne -> Types.Some fEtrue
1259| Integers.Clt -> Types.None
1260| Integers.Cle -> Types.None
1261| Integers.Cgt -> Types.None
1262| Integers.Cge -> Types.None
1263
1264(** val ev_cmp :
1265    Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
1266    Types.option **)
1267let ev_cmp c v1 v2 =
1268  match v1 with
1269  | Values.Vundef -> Types.None
1270  | Values.Vint (sz1, n1) ->
1271    (match v2 with
1272     | Values.Vundef -> Types.None
1273     | Values.Vint (sz2, n2) ->
1274       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
1275         (fE_of_bool (Values.cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)))
1276         Types.None
1277     | Values.Vnull -> Types.None
1278     | Values.Vptr x -> Types.None)
1279  | Values.Vnull -> Types.None
1280  | Values.Vptr x -> Types.None
1281
1282(** val ev_cmpp :
[2773]1283    GenMem.mem -> Integers.comparison -> Values.val0 -> Values.val0 ->
[2601]1284    Values.val0 Types.option **)
1285let ev_cmpp m c v1 v2 =
1286  match v1 with
1287  | Values.Vundef -> Types.None
1288  | Values.Vint (x, x0) -> Types.None
1289  | Values.Vnull ->
1290    (match v2 with
1291     | Values.Vundef -> Types.None
1292     | Values.Vint (x, x0) -> Types.None
1293     | Values.Vnull -> ev_cmp_match c
1294     | Values.Vptr x -> ev_cmp_mismatch c)
1295  | Values.Vptr ptr1 ->
1296    (match v2 with
1297     | Values.Vundef -> Types.None
1298     | Values.Vint (x, x0) -> Types.None
1299     | Values.Vnull -> ev_cmp_mismatch c
1300     | Values.Vptr ptr2 ->
1301       (match Bool.andb (FrontEndMem.valid_pointer m ptr1)
1302                (FrontEndMem.valid_pointer m ptr2) with
1303        | Bool.True ->
[3001]1304          (match Pointers.eq_block (Pointers.pblock ptr1)
1305                   (Pointers.pblock ptr2) with
[2601]1306           | Bool.True ->
1307             Types.Some
1308               (fE_of_bool
[3001]1309                 (Values.cmp_offset c (Pointers.poff ptr1)
1310                   (Pointers.poff ptr2)))
[2601]1311           | Bool.False -> ev_cmp_mismatch c)
1312        | Bool.False -> Types.None))
1313
1314(** val ev_cmpu :
1315    Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
1316    Types.option **)
1317let ev_cmpu c v1 v2 =
1318  match v1 with
1319  | Values.Vundef -> Types.None
1320  | Values.Vint (sz1, n1) ->
1321    (match v2 with
1322     | Values.Vundef -> Types.None
1323     | Values.Vint (sz2, n2) ->
1324       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
1325         (fE_of_bool (Values.cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)))
1326         Types.None
1327     | Values.Vnull -> Types.None
1328     | Values.Vptr x -> Types.None)
1329  | Values.Vnull -> Types.None
1330  | Values.Vptr x -> Types.None
1331
1332(** val eval_binop :
[2773]1333    GenMem.mem -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
[2601]1334    Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1335let eval_binop m t1 t2 t' = function
1336| Oadd (x, x0) -> ev_add
1337| Osub (x, x0) -> ev_sub
1338| Omul (x, x0) -> ev_mul
1339| Odiv x -> ev_divs
1340| Odivu x -> ev_divu
1341| Omod x -> ev_mods
1342| Omodu x -> ev_modu
1343| Oand (x, x0) -> ev_and
1344| Oor (x, x0) -> ev_or
1345| Oxor (x, x0) -> ev_xor
1346| Oshl (x, x0) -> ev_shl
1347| Oshr (x, x0) -> ev_shr
1348| Oshru (x, x0) -> ev_shru
1349| Ocmp (x, x0, x1, c) -> ev_cmp c
1350| Ocmpu (x, x0, c) -> ev_cmpu c
1351| Oaddpi x -> ev_addpi
1352| Oaddip x -> (fun x0 y -> ev_addpi y x0)
1353| Osubpi x -> ev_subpi
1354| Osubpp sz -> ev_subpp sz
1355| Ocmpp (x, c) -> ev_cmpp m c
1356
Note: See TracBrowser for help on using the repository browser.