source: driver/extracted/stacksize.ml @ 3106

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

New extraction

File size: 8.5 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open Hide
22
23open Integers
24
25open AST
26
27open Division
28
29open Exp
30
31open Arithmetic
32
33open Extranat
34
35open Vector
36
37open FoldStuff
38
39open BitVector
40
41open Z
42
43open BitVectorZ
44
45open Pointers
46
47open Coqlib
48
49open Values
50
51open Events
52
53open IOMonad
54
55open IO
56
57open Sets
58
59open Listb
60
61open Proper
62
63open PositiveMap
64
65open Deqsets
66
67open ErrorMessages
68
69open PreIdentifiers
70
71open Errors
72
73open Extralib
74
75open Setoids
76
77open Monad
78
79open Option
80
81open Div_and_mod
82
83open Russell
84
85open Util
86
87open Lists
88
89open Positive
90
91open Identifiers
92
93open CostLabel
94
95open Jmeq
96
97open StructuredTraces
98
99type call_ud =
100| Up of AST.ident
101| Down of AST.ident
102
103(** val call_ud_rect_Type4 :
104    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
105let rec call_ud_rect_Type4 h_up h_down = function
106| Up x_23575 -> h_up x_23575
107| Down x_23576 -> h_down x_23576
108
109(** val call_ud_rect_Type5 :
110    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
111let rec call_ud_rect_Type5 h_up h_down = function
112| Up x_23580 -> h_up x_23580
113| Down x_23581 -> h_down x_23581
114
115(** val call_ud_rect_Type3 :
116    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
117let rec call_ud_rect_Type3 h_up h_down = function
118| Up x_23585 -> h_up x_23585
119| Down x_23586 -> h_down x_23586
120
121(** val call_ud_rect_Type2 :
122    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
123let rec call_ud_rect_Type2 h_up h_down = function
124| Up x_23590 -> h_up x_23590
125| Down x_23591 -> h_down x_23591
126
127(** val call_ud_rect_Type1 :
128    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
129let rec call_ud_rect_Type1 h_up h_down = function
130| Up x_23595 -> h_up x_23595
131| Down x_23596 -> h_down x_23596
132
133(** val call_ud_rect_Type0 :
134    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
135let rec call_ud_rect_Type0 h_up h_down = function
136| Up x_23600 -> h_up x_23600
137| Down x_23601 -> h_down x_23601
138
139(** val call_ud_inv_rect_Type4 :
140    call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
141let call_ud_inv_rect_Type4 hterm h1 h2 =
142  let hcut = call_ud_rect_Type4 h1 h2 hterm in hcut __
143
144(** val call_ud_inv_rect_Type3 :
145    call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
146let call_ud_inv_rect_Type3 hterm h1 h2 =
147  let hcut = call_ud_rect_Type3 h1 h2 hterm in hcut __
148
149(** val call_ud_inv_rect_Type2 :
150    call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
151let call_ud_inv_rect_Type2 hterm h1 h2 =
152  let hcut = call_ud_rect_Type2 h1 h2 hterm in hcut __
153
154(** val call_ud_inv_rect_Type1 :
155    call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
156let call_ud_inv_rect_Type1 hterm h1 h2 =
157  let hcut = call_ud_rect_Type1 h1 h2 hterm in hcut __
158
159(** val call_ud_inv_rect_Type0 :
160    call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
161let call_ud_inv_rect_Type0 hterm h1 h2 =
162  let hcut = call_ud_rect_Type0 h1 h2 hterm in hcut __
163
164(** val call_ud_discr : call_ud -> call_ud -> __ **)
165let call_ud_discr x y =
166  Logic.eq_rect_Type2 x
167    (match x with
168     | Up a0 -> Obj.magic (fun _ dH -> dH __)
169     | Down a0 -> Obj.magic (fun _ dH -> dH __)) y
170
171(** val call_ud_jmdiscr : call_ud -> call_ud -> __ **)
172let call_ud_jmdiscr x y =
173  Logic.eq_rect_Type2 x
174    (match x with
175     | Up a0 -> Obj.magic (fun _ dH -> dH __)
176     | Down a0 -> Obj.magic (fun _ dH -> dH __)) y
177
178type stacksize_info = { current : Nat.nat; maximum : Nat.nat }
179
180(** val stacksize_info_rect_Type4 :
181    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
182let rec stacksize_info_rect_Type4 h_mk_stacksize_info x_23636 =
183  let { current = current0; maximum = maximum0 } = x_23636 in
184  h_mk_stacksize_info current0 maximum0
185
186(** val stacksize_info_rect_Type5 :
187    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
188let rec stacksize_info_rect_Type5 h_mk_stacksize_info x_23638 =
189  let { current = current0; maximum = maximum0 } = x_23638 in
190  h_mk_stacksize_info current0 maximum0
191
192(** val stacksize_info_rect_Type3 :
193    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
194let rec stacksize_info_rect_Type3 h_mk_stacksize_info x_23640 =
195  let { current = current0; maximum = maximum0 } = x_23640 in
196  h_mk_stacksize_info current0 maximum0
197
198(** val stacksize_info_rect_Type2 :
199    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
200let rec stacksize_info_rect_Type2 h_mk_stacksize_info x_23642 =
201  let { current = current0; maximum = maximum0 } = x_23642 in
202  h_mk_stacksize_info current0 maximum0
203
204(** val stacksize_info_rect_Type1 :
205    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
206let rec stacksize_info_rect_Type1 h_mk_stacksize_info x_23644 =
207  let { current = current0; maximum = maximum0 } = x_23644 in
208  h_mk_stacksize_info current0 maximum0
209
210(** val stacksize_info_rect_Type0 :
211    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
212let rec stacksize_info_rect_Type0 h_mk_stacksize_info x_23646 =
213  let { current = current0; maximum = maximum0 } = x_23646 in
214  h_mk_stacksize_info current0 maximum0
215
216(** val current : stacksize_info -> Nat.nat **)
217let rec current xxx =
218  xxx.current
219
220(** val maximum : stacksize_info -> Nat.nat **)
221let rec maximum xxx =
222  xxx.maximum
223
224(** val stacksize_info_inv_rect_Type4 :
225    stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
226let stacksize_info_inv_rect_Type4 hterm h1 =
227  let hcut = stacksize_info_rect_Type4 h1 hterm in hcut __
228
229(** val stacksize_info_inv_rect_Type3 :
230    stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
231let stacksize_info_inv_rect_Type3 hterm h1 =
232  let hcut = stacksize_info_rect_Type3 h1 hterm in hcut __
233
234(** val stacksize_info_inv_rect_Type2 :
235    stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
236let stacksize_info_inv_rect_Type2 hterm h1 =
237  let hcut = stacksize_info_rect_Type2 h1 hterm in hcut __
238
239(** val stacksize_info_inv_rect_Type1 :
240    stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
241let stacksize_info_inv_rect_Type1 hterm h1 =
242  let hcut = stacksize_info_rect_Type1 h1 hterm in hcut __
243
244(** val stacksize_info_inv_rect_Type0 :
245    stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
246let stacksize_info_inv_rect_Type0 hterm h1 =
247  let hcut = stacksize_info_rect_Type0 h1 hterm in hcut __
248
249(** val stacksize_info_discr : stacksize_info -> stacksize_info -> __ **)
250let stacksize_info_discr x y =
251  Logic.eq_rect_Type2 x
252    (let { current = a0; maximum = a1 } = x in
253    Obj.magic (fun _ dH -> dH __ __)) y
254
255(** val stacksize_info_jmdiscr : stacksize_info -> stacksize_info -> __ **)
256let stacksize_info_jmdiscr x y =
257  Logic.eq_rect_Type2 x
258    (let { current = a0; maximum = a1 } = x in
259    Obj.magic (fun _ dH -> dH __ __)) y
260
261(** val update_stacksize_info :
262    (AST.ident -> Nat.nat Types.option) -> stacksize_info -> call_ud
263    List.list -> stacksize_info **)
264let update_stacksize_info stacksizes =
265  let get_stacksize = fun f ->
266    match stacksizes f with
267    | Types.None -> Nat.O
268    | Types.Some n -> n
269  in
270  let f = fun ud acc ->
271    match ud with
272    | Up i ->
273      let new_stack = Nat.plus (get_stacksize i) acc.current in
274      let new_max = Nat.max acc.maximum new_stack in
275      { current = new_stack; maximum = new_max }
276    | Down i ->
277      let new_stack = Nat.minus acc.current (get_stacksize i) in
278      { current = new_stack; maximum = acc.maximum }
279  in
280  List.foldr f
281
282(** val extract_call_ud_from_observables :
283    StructuredTraces.intensional_event List.list -> call_ud List.list **)
284let extract_call_ud_from_observables =
285  let f = fun ev ->
286    match ev with
287    | StructuredTraces.IEVcost x -> List.Nil
288    | StructuredTraces.IEVcall i -> List.Cons ((Up i), List.Nil)
289    | StructuredTraces.IEVtailcall (i, j) ->
290      List.Cons ((Down i), (List.Cons ((Up j), List.Nil)))
291    | StructuredTraces.IEVret i -> List.Cons ((Down i), List.Nil)
292  in
293  List.foldr (fun ev -> List.append (f ev)) List.Nil
294
295(** val extract_call_ud_from_tlr :
296    StructuredTraces.abstract_status -> __ -> __ ->
297    StructuredTraces.trace_label_return -> AST.ident -> call_ud List.list **)
298let extract_call_ud_from_tlr s st1 st2 tlr curr =
299  extract_call_ud_from_observables
300    (Types.pi1
301      (StructuredTraces.observables_trace_label_return s st1 st2 tlr curr))
302
303(** val extract_call_ud_from_tll :
304    StructuredTraces.trace_ends_with_ret -> StructuredTraces.abstract_status
305    -> __ -> __ -> StructuredTraces.trace_label_label -> AST.ident -> call_ud
306    List.list **)
307let extract_call_ud_from_tll s fl st1 st2 tll curr =
308  extract_call_ud_from_observables
309    (Types.pi1
310      (StructuredTraces.observables_trace_label_label fl s st1 st2 tll curr))
311
Note: See TracBrowser for help on using the repository browser.