extracted/stacksize.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Relations
   6
   7 open Nat
   8
   9 open Hints_declaration
  10
  11 open Core_notation
  12
  13 open Pts
  14
  15 open Logic
  16
  17 open Types
  18
  19 open List
  20
  21 open Hide
  22
  23 open Integers
  24
  25 open AST
  26
  27 open Division
  28
  29 open Exp
  30
  31 open Arithmetic
  32
  33 open Extranat
  34
  35 open Vector
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Z
  42
  43 open BitVectorZ
  44
  45 open Pointers
  46
  47 open Coqlib
  48
  49 open Values
  50
  51 open Events
  52
  53 open IOMonad
  54
  55 open IO
  56
  57 open Sets
  58
  59 open Listb
  60
  61 open Proper
  62
  63 open PositiveMap
  64
  65 open Deqsets
  66
  67 open ErrorMessages
  68
  69 open PreIdentifiers
  70
  71 open Errors
  72
  73 open Extralib
  74
  75 open Setoids
  76
  77 open Monad
  78
  79 open Option
  80
  81 open Div_and_mod
  82
  83 open Russell
  84
  85 open Util
  86
  87 open Lists
  88
  89 open Positive
  90
  91 open Identifiers
  92
  93 open CostLabel
  94
  95 open Jmeq
  96
  97 open StructuredTraces
  98
  99 type 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 **)
 105 let 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 **)
 111 let 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 **)
 117 let 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 **)
 123 let 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 **)
 129 let 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 **)
 135 let 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 **)
 141 let 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 **)
 146 let 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 **)
 151 let 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 **)
 156 let 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 **)
 161 let 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 -> __ **)
 165 let 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 -> __ **)
 172 let 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
 178 type stacksize_info = { current : Nat.nat; maximum : Nat.nat }
 179
 180 (** val stacksize_info_rect_Type4 :
 181     (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
 182 let 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 **)
 188 let 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 **)
 194 let 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 **)
 200 let 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 **)
 206 let 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 **)
 212 let 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 **)
 217 let rec current xxx =
 218   xxx.current
 219
 220 (** val maximum : stacksize_info -> Nat.nat **)
 221 let rec maximum xxx =
 222   xxx.maximum
 223
 224 (** val stacksize_info_inv_rect_Type4 :
 225     stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
 226 let 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 **)
 231 let 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 **)
 236 let 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 **)
 241 let 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 **)
 246 let 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 -> __ **)
 250 let 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 -> __ **)
 256 let 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 **)
 264 let 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 **)
 284 let 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 **)
 298 let 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 **)
 307 let 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