source: extracted/frontEndOps.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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