[2730] | 1 | open Preamble |
---|
| 2 | |
---|
[2773] | 3 | open BitVectorTrie |
---|
| 4 | |
---|
[2730] | 5 | open Graphs |
---|
| 6 | |
---|
| 7 | open Order |
---|
| 8 | |
---|
| 9 | open Registers |
---|
| 10 | |
---|
| 11 | open FrontEndOps |
---|
| 12 | |
---|
| 13 | open RTLabs_syntax |
---|
| 14 | |
---|
| 15 | open SmallstepExec |
---|
| 16 | |
---|
| 17 | open CostLabel |
---|
| 18 | |
---|
| 19 | open Events |
---|
| 20 | |
---|
| 21 | open IOMonad |
---|
| 22 | |
---|
| 23 | open IO |
---|
| 24 | |
---|
| 25 | open Extra_bool |
---|
| 26 | |
---|
| 27 | open Coqlib |
---|
| 28 | |
---|
| 29 | open Values |
---|
| 30 | |
---|
| 31 | open FrontEndVal |
---|
| 32 | |
---|
| 33 | open Hide |
---|
| 34 | |
---|
| 35 | open ByteValues |
---|
| 36 | |
---|
| 37 | open Division |
---|
| 38 | |
---|
| 39 | open Z |
---|
| 40 | |
---|
| 41 | open BitVectorZ |
---|
| 42 | |
---|
| 43 | open Pointers |
---|
| 44 | |
---|
| 45 | open GenMem |
---|
| 46 | |
---|
| 47 | open FrontEndMem |
---|
| 48 | |
---|
| 49 | open Proper |
---|
| 50 | |
---|
| 51 | open PositiveMap |
---|
| 52 | |
---|
| 53 | open Deqsets |
---|
| 54 | |
---|
| 55 | open Extralib |
---|
| 56 | |
---|
| 57 | open Lists |
---|
| 58 | |
---|
| 59 | open Identifiers |
---|
| 60 | |
---|
| 61 | open Exp |
---|
| 62 | |
---|
| 63 | open Arithmetic |
---|
| 64 | |
---|
| 65 | open Vector |
---|
| 66 | |
---|
| 67 | open Div_and_mod |
---|
| 68 | |
---|
| 69 | open Util |
---|
| 70 | |
---|
| 71 | open FoldStuff |
---|
| 72 | |
---|
| 73 | open BitVector |
---|
| 74 | |
---|
| 75 | open Extranat |
---|
| 76 | |
---|
| 77 | open Integers |
---|
| 78 | |
---|
| 79 | open AST |
---|
| 80 | |
---|
| 81 | open Globalenvs |
---|
| 82 | |
---|
| 83 | open ErrorMessages |
---|
| 84 | |
---|
| 85 | open Option |
---|
| 86 | |
---|
| 87 | open Setoids |
---|
| 88 | |
---|
| 89 | open Monad |
---|
| 90 | |
---|
| 91 | open Jmeq |
---|
| 92 | |
---|
| 93 | open Russell |
---|
| 94 | |
---|
| 95 | open Positive |
---|
| 96 | |
---|
| 97 | open PreIdentifiers |
---|
| 98 | |
---|
| 99 | open Errors |
---|
| 100 | |
---|
| 101 | open Bool |
---|
| 102 | |
---|
| 103 | open Relations |
---|
| 104 | |
---|
| 105 | open Nat |
---|
| 106 | |
---|
| 107 | open Hints_declaration |
---|
| 108 | |
---|
| 109 | open Core_notation |
---|
| 110 | |
---|
| 111 | open Pts |
---|
| 112 | |
---|
| 113 | open Logic |
---|
| 114 | |
---|
| 115 | open Types |
---|
| 116 | |
---|
| 117 | open List |
---|
| 118 | |
---|
| 119 | open RTLabs_semantics |
---|
| 120 | |
---|
[2773] | 121 | type rTLabs_state = RTLabs_semantics.state |
---|
[2730] | 122 | |
---|
| 123 | type rTLabs_genv = RTLabs_semantics.genv |
---|
| 124 | |
---|
| 125 | open Sets |
---|
| 126 | |
---|
| 127 | open Listb |
---|
| 128 | |
---|
| 129 | open StructuredTraces |
---|
| 130 | |
---|
| 131 | open CostSpec |
---|
| 132 | |
---|
| 133 | open Deqsets_extra |
---|
| 134 | |
---|
[2773] | 135 | (** val status_class_jmdiscr : |
---|
[2730] | 136 | StructuredTraces.status_class -> StructuredTraces.status_class -> __ **) |
---|
[2773] | 137 | let status_class_jmdiscr x y = |
---|
[2730] | 138 | Logic.eq_rect_Type2 x |
---|
| 139 | (match x with |
---|
| 140 | | StructuredTraces.Cl_return -> Obj.magic (fun _ dH -> dH) |
---|
| 141 | | StructuredTraces.Cl_jump -> Obj.magic (fun _ dH -> dH) |
---|
| 142 | | StructuredTraces.Cl_call -> Obj.magic (fun _ dH -> dH) |
---|
| 143 | | StructuredTraces.Cl_tailcall -> Obj.magic (fun _ dH -> dH) |
---|
| 144 | | StructuredTraces.Cl_other -> Obj.magic (fun _ dH -> dH)) y |
---|
| 145 | |
---|
[2773] | 146 | type rTLabs_ext_state = { ras_state : RTLabs_semantics.state; |
---|
[2730] | 147 | ras_fn_stack : Pointers.block List.list } |
---|
| 148 | |
---|
| 149 | (** val rTLabs_ext_state_rect_Type4 : |
---|
[2773] | 150 | RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block |
---|
[2730] | 151 | List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **) |
---|
[2997] | 152 | let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_2496 = |
---|
| 153 | let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2496 in |
---|
[2730] | 154 | h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ |
---|
| 155 | |
---|
| 156 | (** val rTLabs_ext_state_rect_Type5 : |
---|
[2773] | 157 | RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block |
---|
[2730] | 158 | List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **) |
---|
[2997] | 159 | let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_2498 = |
---|
| 160 | let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2498 in |
---|
[2730] | 161 | h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ |
---|
| 162 | |
---|
| 163 | (** val rTLabs_ext_state_rect_Type3 : |
---|
[2773] | 164 | RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block |
---|
[2730] | 165 | List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **) |
---|
[2997] | 166 | let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_2500 = |
---|
| 167 | let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2500 in |
---|
[2730] | 168 | h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ |
---|
| 169 | |
---|
| 170 | (** val rTLabs_ext_state_rect_Type2 : |
---|
[2773] | 171 | RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block |
---|
[2730] | 172 | List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **) |
---|
[2997] | 173 | let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_2502 = |
---|
| 174 | let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2502 in |
---|
[2730] | 175 | h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ |
---|
| 176 | |
---|
| 177 | (** val rTLabs_ext_state_rect_Type1 : |
---|
[2773] | 178 | RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block |
---|
[2730] | 179 | List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **) |
---|
[2997] | 180 | let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_2504 = |
---|
| 181 | let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2504 in |
---|
[2730] | 182 | h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ |
---|
| 183 | |
---|
| 184 | (** val rTLabs_ext_state_rect_Type0 : |
---|
[2773] | 185 | RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block |
---|
[2730] | 186 | List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **) |
---|
[2997] | 187 | let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_2506 = |
---|
| 188 | let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2506 in |
---|
[2730] | 189 | h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ |
---|
| 190 | |
---|
| 191 | (** val ras_state : |
---|
[2773] | 192 | RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state **) |
---|
[2730] | 193 | let rec ras_state ge xxx = |
---|
| 194 | xxx.ras_state |
---|
| 195 | |
---|
| 196 | (** val ras_fn_stack : |
---|
| 197 | RTLabs_semantics.genv -> rTLabs_ext_state -> Pointers.block List.list **) |
---|
| 198 | let rec ras_fn_stack ge xxx = |
---|
| 199 | xxx.ras_fn_stack |
---|
| 200 | |
---|
| 201 | (** val rTLabs_ext_state_inv_rect_Type4 : |
---|
[2773] | 202 | RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state -> |
---|
[2730] | 203 | Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 204 | let rTLabs_ext_state_inv_rect_Type4 x1 hterm h1 = |
---|
| 205 | let hcut = rTLabs_ext_state_rect_Type4 x1 h1 hterm in hcut __ |
---|
| 206 | |
---|
| 207 | (** val rTLabs_ext_state_inv_rect_Type3 : |
---|
[2773] | 208 | RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state -> |
---|
[2730] | 209 | Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 210 | let rTLabs_ext_state_inv_rect_Type3 x1 hterm h1 = |
---|
| 211 | let hcut = rTLabs_ext_state_rect_Type3 x1 h1 hterm in hcut __ |
---|
| 212 | |
---|
| 213 | (** val rTLabs_ext_state_inv_rect_Type2 : |
---|
[2773] | 214 | RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state -> |
---|
[2730] | 215 | Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 216 | let rTLabs_ext_state_inv_rect_Type2 x1 hterm h1 = |
---|
| 217 | let hcut = rTLabs_ext_state_rect_Type2 x1 h1 hterm in hcut __ |
---|
| 218 | |
---|
| 219 | (** val rTLabs_ext_state_inv_rect_Type1 : |
---|
[2773] | 220 | RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state -> |
---|
[2730] | 221 | Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 222 | let rTLabs_ext_state_inv_rect_Type1 x1 hterm h1 = |
---|
| 223 | let hcut = rTLabs_ext_state_rect_Type1 x1 h1 hterm in hcut __ |
---|
| 224 | |
---|
| 225 | (** val rTLabs_ext_state_inv_rect_Type0 : |
---|
[2773] | 226 | RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state -> |
---|
[2730] | 227 | Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 228 | let rTLabs_ext_state_inv_rect_Type0 x1 hterm h1 = |
---|
| 229 | let hcut = rTLabs_ext_state_rect_Type0 x1 h1 hterm in hcut __ |
---|
| 230 | |
---|
| 231 | (** val rTLabs_ext_state_discr : |
---|
| 232 | RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __ **) |
---|
| 233 | let rTLabs_ext_state_discr a1 x y = |
---|
| 234 | Logic.eq_rect_Type2 x |
---|
| 235 | (let { ras_state = a0; ras_fn_stack = a10 } = x in |
---|
| 236 | Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
| 237 | |
---|
| 238 | (** val rTLabs_ext_state_jmdiscr : |
---|
| 239 | RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __ **) |
---|
| 240 | let rTLabs_ext_state_jmdiscr a1 x y = |
---|
| 241 | Logic.eq_rect_Type2 x |
---|
| 242 | (let { ras_state = a0; ras_fn_stack = a10 } = x in |
---|
| 243 | Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
| 244 | |
---|
| 245 | (** val dpi1__o__Ras_state__o__inject : |
---|
| 246 | RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair -> |
---|
[2773] | 247 | RTLabs_semantics.state Types.sig0 **) |
---|
[2730] | 248 | let dpi1__o__Ras_state__o__inject x1 x3 = |
---|
| 249 | x3.Types.dpi1.ras_state |
---|
| 250 | |
---|
| 251 | (** val eject__o__Ras_state__o__inject : |
---|
| 252 | RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 -> |
---|
[2773] | 253 | RTLabs_semantics.state Types.sig0 **) |
---|
[2730] | 254 | let eject__o__Ras_state__o__inject x1 x3 = |
---|
| 255 | (Types.pi1 x3).ras_state |
---|
| 256 | |
---|
| 257 | (** val ras_state__o__inject : |
---|
[2773] | 258 | RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state |
---|
[2730] | 259 | Types.sig0 **) |
---|
| 260 | let ras_state__o__inject x1 x2 = |
---|
| 261 | x2.ras_state |
---|
| 262 | |
---|
| 263 | (** val dpi1__o__Ras_state : |
---|
| 264 | RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair -> |
---|
[2773] | 265 | RTLabs_semantics.state **) |
---|
[2730] | 266 | let dpi1__o__Ras_state x0 x2 = |
---|
| 267 | x2.Types.dpi1.ras_state |
---|
| 268 | |
---|
| 269 | (** val eject__o__Ras_state : |
---|
| 270 | RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 -> |
---|
[2773] | 271 | RTLabs_semantics.state **) |
---|
[2730] | 272 | let eject__o__Ras_state x0 x2 = |
---|
| 273 | (Types.pi1 x2).ras_state |
---|
| 274 | |
---|
| 275 | (** val next_state : |
---|
[2773] | 276 | RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state -> |
---|
[2730] | 277 | Events.trace -> rTLabs_ext_state **) |
---|
| 278 | let next_state ge s s' t = |
---|
| 279 | { ras_state = s'; ras_fn_stack = |
---|
| 280 | ((match s' with |
---|
| 281 | | RTLabs_semantics.State (x, x0, x1) -> (fun _ -> s.ras_fn_stack) |
---|
| 282 | | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) -> |
---|
| 283 | (fun _ -> List.Cons |
---|
| 284 | ((Types.pi1 |
---|
| 285 | (RTLabs_semantics.func_block_of_exec ge s.ras_state t x x0 x1 x2 |
---|
| 286 | x3 x4)), s.ras_fn_stack)) |
---|
| 287 | | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> |
---|
| 288 | (fun _ -> List.tail s.ras_fn_stack) |
---|
| 289 | | RTLabs_semantics.Finalstate x -> (fun _ -> List.Nil)) __) } |
---|
| 290 | |
---|
| 291 | (** val rTLabs_classify : |
---|
[2773] | 292 | RTLabs_semantics.state -> StructuredTraces.status_class **) |
---|
[2730] | 293 | let rTLabs_classify = function |
---|
| 294 | | RTLabs_semantics.State (f, x, x0) -> |
---|
| 295 | (match RTLabs_semantics.next_instruction f with |
---|
| 296 | | RTLabs_syntax.St_skip x1 -> StructuredTraces.Cl_other |
---|
| 297 | | RTLabs_syntax.St_cost (x1, x2) -> StructuredTraces.Cl_other |
---|
| 298 | | RTLabs_syntax.St_const (x1, x2, x3, x4) -> StructuredTraces.Cl_other |
---|
| 299 | | RTLabs_syntax.St_op1 (x1, x2, x3, x4, x5, x6) -> |
---|
| 300 | StructuredTraces.Cl_other |
---|
| 301 | | RTLabs_syntax.St_op2 (x1, x2, x3, x4, x5, x6, x7, x8) -> |
---|
| 302 | StructuredTraces.Cl_other |
---|
| 303 | | RTLabs_syntax.St_load (x1, x2, x3, x4) -> StructuredTraces.Cl_other |
---|
| 304 | | RTLabs_syntax.St_store (x1, x2, x3, x4) -> StructuredTraces.Cl_other |
---|
| 305 | | RTLabs_syntax.St_call_id (x1, x2, x3, x4) -> StructuredTraces.Cl_other |
---|
| 306 | | RTLabs_syntax.St_call_ptr (x1, x2, x3, x4) -> StructuredTraces.Cl_other |
---|
| 307 | | RTLabs_syntax.St_cond (x1, x2, x3) -> StructuredTraces.Cl_jump |
---|
| 308 | | RTLabs_syntax.St_return -> StructuredTraces.Cl_other) |
---|
| 309 | | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) -> |
---|
| 310 | StructuredTraces.Cl_call |
---|
| 311 | | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> StructuredTraces.Cl_return |
---|
| 312 | | RTLabs_semantics.Finalstate x -> StructuredTraces.Cl_other |
---|
| 313 | |
---|
[2773] | 314 | (** val rTLabs_cost : RTLabs_semantics.state -> Bool.bool **) |
---|
[2730] | 315 | let rTLabs_cost = function |
---|
| 316 | | RTLabs_semantics.State (f, fs, m) -> |
---|
| 317 | CostSpec.is_cost_label (RTLabs_semantics.next_instruction f) |
---|
| 318 | | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) -> Bool.False |
---|
| 319 | | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Bool.False |
---|
| 320 | | RTLabs_semantics.Finalstate x -> Bool.False |
---|
| 321 | |
---|
| 322 | (** val rTLabs_cost_label : |
---|
[2773] | 323 | RTLabs_semantics.state -> CostLabel.costlabel Types.option **) |
---|
[2730] | 324 | let rTLabs_cost_label = function |
---|
| 325 | | RTLabs_semantics.State (f, fs, m) -> |
---|
| 326 | CostSpec.cost_label_of (RTLabs_semantics.next_instruction f) |
---|
| 327 | | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) -> Types.None |
---|
| 328 | | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.None |
---|
| 329 | | RTLabs_semantics.Finalstate x -> Types.None |
---|
| 330 | |
---|
| 331 | type rTLabs_pc = |
---|
| 332 | | Rapc_state of Pointers.block * Graphs.label |
---|
| 333 | | Rapc_call of Graphs.label Types.option * Pointers.block |
---|
| 334 | | Rapc_ret of Pointers.block Types.option |
---|
| 335 | | Rapc_fin |
---|
| 336 | |
---|
| 337 | (** val rTLabs_pc_rect_Type4 : |
---|
| 338 | (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option -> |
---|
| 339 | Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 -> |
---|
| 340 | rTLabs_pc -> 'a1 **) |
---|
| 341 | let rec rTLabs_pc_rect_Type4 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function |
---|
[2997] | 342 | | Rapc_state (x_2532, x_2531) -> h_rapc_state x_2532 x_2531 |
---|
| 343 | | Rapc_call (x_2534, x_2533) -> h_rapc_call x_2534 x_2533 |
---|
| 344 | | Rapc_ret x_2535 -> h_rapc_ret x_2535 |
---|
[2730] | 345 | | Rapc_fin -> h_rapc_fin |
---|
| 346 | |
---|
| 347 | (** val rTLabs_pc_rect_Type5 : |
---|
| 348 | (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option -> |
---|
| 349 | Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 -> |
---|
| 350 | rTLabs_pc -> 'a1 **) |
---|
| 351 | let rec rTLabs_pc_rect_Type5 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function |
---|
[2997] | 352 | | Rapc_state (x_2542, x_2541) -> h_rapc_state x_2542 x_2541 |
---|
| 353 | | Rapc_call (x_2544, x_2543) -> h_rapc_call x_2544 x_2543 |
---|
| 354 | | Rapc_ret x_2545 -> h_rapc_ret x_2545 |
---|
[2730] | 355 | | Rapc_fin -> h_rapc_fin |
---|
| 356 | |
---|
| 357 | (** val rTLabs_pc_rect_Type3 : |
---|
| 358 | (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option -> |
---|
| 359 | Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 -> |
---|
| 360 | rTLabs_pc -> 'a1 **) |
---|
| 361 | let rec rTLabs_pc_rect_Type3 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function |
---|
[2997] | 362 | | Rapc_state (x_2552, x_2551) -> h_rapc_state x_2552 x_2551 |
---|
| 363 | | Rapc_call (x_2554, x_2553) -> h_rapc_call x_2554 x_2553 |
---|
| 364 | | Rapc_ret x_2555 -> h_rapc_ret x_2555 |
---|
[2730] | 365 | | Rapc_fin -> h_rapc_fin |
---|
| 366 | |
---|
| 367 | (** val rTLabs_pc_rect_Type2 : |
---|
| 368 | (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option -> |
---|
| 369 | Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 -> |
---|
| 370 | rTLabs_pc -> 'a1 **) |
---|
| 371 | let rec rTLabs_pc_rect_Type2 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function |
---|
[2997] | 372 | | Rapc_state (x_2562, x_2561) -> h_rapc_state x_2562 x_2561 |
---|
| 373 | | Rapc_call (x_2564, x_2563) -> h_rapc_call x_2564 x_2563 |
---|
| 374 | | Rapc_ret x_2565 -> h_rapc_ret x_2565 |
---|
[2730] | 375 | | Rapc_fin -> h_rapc_fin |
---|
| 376 | |
---|
| 377 | (** val rTLabs_pc_rect_Type1 : |
---|
| 378 | (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option -> |
---|
| 379 | Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 -> |
---|
| 380 | rTLabs_pc -> 'a1 **) |
---|
| 381 | let rec rTLabs_pc_rect_Type1 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function |
---|
[2997] | 382 | | Rapc_state (x_2572, x_2571) -> h_rapc_state x_2572 x_2571 |
---|
| 383 | | Rapc_call (x_2574, x_2573) -> h_rapc_call x_2574 x_2573 |
---|
| 384 | | Rapc_ret x_2575 -> h_rapc_ret x_2575 |
---|
[2730] | 385 | | Rapc_fin -> h_rapc_fin |
---|
| 386 | |
---|
| 387 | (** val rTLabs_pc_rect_Type0 : |
---|
| 388 | (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option -> |
---|
| 389 | Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 -> |
---|
| 390 | rTLabs_pc -> 'a1 **) |
---|
| 391 | let rec rTLabs_pc_rect_Type0 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function |
---|
[2997] | 392 | | Rapc_state (x_2582, x_2581) -> h_rapc_state x_2582 x_2581 |
---|
| 393 | | Rapc_call (x_2584, x_2583) -> h_rapc_call x_2584 x_2583 |
---|
| 394 | | Rapc_ret x_2585 -> h_rapc_ret x_2585 |
---|
[2730] | 395 | | Rapc_fin -> h_rapc_fin |
---|
| 396 | |
---|
| 397 | (** val rTLabs_pc_inv_rect_Type4 : |
---|
| 398 | rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> |
---|
| 399 | (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) -> |
---|
| 400 | (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 401 | let rTLabs_pc_inv_rect_Type4 hterm h1 h2 h3 h4 = |
---|
| 402 | let hcut = rTLabs_pc_rect_Type4 h1 h2 h3 h4 hterm in hcut __ |
---|
| 403 | |
---|
| 404 | (** val rTLabs_pc_inv_rect_Type3 : |
---|
| 405 | rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> |
---|
| 406 | (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) -> |
---|
| 407 | (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 408 | let rTLabs_pc_inv_rect_Type3 hterm h1 h2 h3 h4 = |
---|
| 409 | let hcut = rTLabs_pc_rect_Type3 h1 h2 h3 h4 hterm in hcut __ |
---|
| 410 | |
---|
| 411 | (** val rTLabs_pc_inv_rect_Type2 : |
---|
| 412 | rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> |
---|
| 413 | (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) -> |
---|
| 414 | (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 415 | let rTLabs_pc_inv_rect_Type2 hterm h1 h2 h3 h4 = |
---|
| 416 | let hcut = rTLabs_pc_rect_Type2 h1 h2 h3 h4 hterm in hcut __ |
---|
| 417 | |
---|
| 418 | (** val rTLabs_pc_inv_rect_Type1 : |
---|
| 419 | rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> |
---|
| 420 | (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) -> |
---|
| 421 | (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 422 | let rTLabs_pc_inv_rect_Type1 hterm h1 h2 h3 h4 = |
---|
| 423 | let hcut = rTLabs_pc_rect_Type1 h1 h2 h3 h4 hterm in hcut __ |
---|
| 424 | |
---|
| 425 | (** val rTLabs_pc_inv_rect_Type0 : |
---|
| 426 | rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> |
---|
| 427 | (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) -> |
---|
| 428 | (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 429 | let rTLabs_pc_inv_rect_Type0 hterm h1 h2 h3 h4 = |
---|
| 430 | let hcut = rTLabs_pc_rect_Type0 h1 h2 h3 h4 hterm in hcut __ |
---|
| 431 | |
---|
| 432 | (** val rTLabs_pc_discr : rTLabs_pc -> rTLabs_pc -> __ **) |
---|
| 433 | let rTLabs_pc_discr x y = |
---|
| 434 | Logic.eq_rect_Type2 x |
---|
| 435 | (match x with |
---|
| 436 | | Rapc_state (a0, a1) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 437 | | Rapc_call (a0, a1) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 438 | | Rapc_ret a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 439 | | Rapc_fin -> Obj.magic (fun _ dH -> dH)) y |
---|
| 440 | |
---|
| 441 | (** val rTLabs_pc_jmdiscr : rTLabs_pc -> rTLabs_pc -> __ **) |
---|
| 442 | let rTLabs_pc_jmdiscr x y = |
---|
| 443 | Logic.eq_rect_Type2 x |
---|
| 444 | (match x with |
---|
| 445 | | Rapc_state (a0, a1) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 446 | | Rapc_call (a0, a1) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 447 | | Rapc_ret a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 448 | | Rapc_fin -> Obj.magic (fun _ dH -> dH)) y |
---|
| 449 | |
---|
| 450 | (** val rTLabs_pc_eq : rTLabs_pc -> rTLabs_pc -> Bool.bool **) |
---|
| 451 | let rTLabs_pc_eq x y = |
---|
| 452 | match x with |
---|
| 453 | | Rapc_state (b1, l1) -> |
---|
| 454 | (match y with |
---|
| 455 | | Rapc_state (b2, l2) -> |
---|
| 456 | Bool.andb (Pointers.eq_block b1 b2) |
---|
| 457 | (Identifiers.eq_identifier PreIdentifiers.LabelTag l1 l2) |
---|
| 458 | | Rapc_call (x0, x1) -> Bool.False |
---|
| 459 | | Rapc_ret x0 -> Bool.False |
---|
| 460 | | Rapc_fin -> Bool.False) |
---|
| 461 | | Rapc_call (o1, b1) -> |
---|
| 462 | (match y with |
---|
| 463 | | Rapc_state (x0, x1) -> Bool.False |
---|
| 464 | | Rapc_call (o2, b2) -> |
---|
| 465 | Bool.andb |
---|
| 466 | (Deqsets.eqb |
---|
| 467 | (Deqsets.deqOption |
---|
| 468 | (Identifiers.deq_identifier PreIdentifiers.LabelTag)) |
---|
| 469 | (Obj.magic o1) (Obj.magic o2)) (Pointers.eq_block b1 b2) |
---|
| 470 | | Rapc_ret x0 -> Bool.False |
---|
| 471 | | Rapc_fin -> Bool.False) |
---|
| 472 | | Rapc_ret b1 -> |
---|
| 473 | (match y with |
---|
| 474 | | Rapc_state (x0, x1) -> Bool.False |
---|
| 475 | | Rapc_call (x0, x1) -> Bool.False |
---|
| 476 | | Rapc_ret b2 -> |
---|
| 477 | Deqsets.eqb (Deqsets.deqOption Pointers.block_eq) (Obj.magic b1) |
---|
| 478 | (Obj.magic b2) |
---|
| 479 | | Rapc_fin -> Bool.False) |
---|
| 480 | | Rapc_fin -> |
---|
| 481 | (match y with |
---|
| 482 | | Rapc_state (x0, x1) -> Bool.False |
---|
| 483 | | Rapc_call (x0, x1) -> Bool.False |
---|
| 484 | | Rapc_ret x0 -> Bool.False |
---|
| 485 | | Rapc_fin -> Bool.True) |
---|
| 486 | |
---|
| 487 | (** val rTLabs_deqset : Deqsets.deqSet **) |
---|
| 488 | let rTLabs_deqset = |
---|
| 489 | Obj.magic rTLabs_pc_eq |
---|
| 490 | |
---|
| 491 | (** val rTLabs_ext_state_to_pc : |
---|
| 492 | RTLabs_semantics.genv -> rTLabs_ext_state -> __ **) |
---|
| 493 | let rTLabs_ext_state_to_pc ge s = |
---|
| 494 | let { ras_state = s'; ras_fn_stack = stk } = s in |
---|
| 495 | (match s' with |
---|
| 496 | | RTLabs_semantics.State (f, fs, m) -> |
---|
| 497 | (match stk with |
---|
| 498 | | List.Nil -> (fun _ -> assert false (* absurd case *)) |
---|
| 499 | | List.Cons (b, x) -> |
---|
| 500 | (fun _ -> Obj.magic (Rapc_state (b, f.RTLabs_semantics.next)))) |
---|
| 501 | | RTLabs_semantics.Callstate (x, x0, x1, x2, fs, x3) -> |
---|
| 502 | (match stk with |
---|
| 503 | | List.Nil -> (fun _ _ -> assert false (* absurd case *)) |
---|
| 504 | | List.Cons (b, x4) -> |
---|
| 505 | (fun _ _ -> |
---|
| 506 | Obj.magic (Rapc_call |
---|
| 507 | ((match fs with |
---|
| 508 | | List.Nil -> Types.None |
---|
| 509 | | List.Cons (f, x6) -> Types.Some f.RTLabs_semantics.next), b)))) |
---|
| 510 | __ |
---|
| 511 | | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> |
---|
| 512 | (match stk with |
---|
| 513 | | List.Nil -> (fun _ -> Obj.magic (Rapc_ret Types.None)) |
---|
| 514 | | List.Cons (b, x3) -> (fun _ -> Obj.magic (Rapc_ret (Types.Some b)))) |
---|
| 515 | | RTLabs_semantics.Finalstate x -> (fun _ -> Obj.magic Rapc_fin)) __ |
---|
| 516 | |
---|
| 517 | (** val rTLabs_pc_to_cost_label : |
---|
| 518 | RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t -> rTLabs_pc |
---|
| 519 | -> CostLabel.costlabel Types.option **) |
---|
| 520 | let rTLabs_pc_to_cost_label ge = function |
---|
| 521 | | Rapc_state (b, l) -> |
---|
| 522 | (match Globalenvs.find_funct_ptr ge b with |
---|
| 523 | | Types.None -> Types.None |
---|
| 524 | | Types.Some fd -> |
---|
| 525 | (match fd with |
---|
| 526 | | AST.Internal f -> |
---|
[2773] | 527 | (match Identifiers.lookup PreIdentifiers.LabelTag |
---|
[2730] | 528 | f.RTLabs_syntax.f_graph l with |
---|
| 529 | | Types.None -> Types.None |
---|
| 530 | | Types.Some s -> CostSpec.cost_label_of s) |
---|
| 531 | | AST.External x -> Types.None)) |
---|
| 532 | | Rapc_call (x, x0) -> Types.None |
---|
| 533 | | Rapc_ret x -> Types.None |
---|
| 534 | | Rapc_fin -> Types.None |
---|
| 535 | |
---|
| 536 | (** val rTLabs_call_ident : |
---|
| 537 | RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 -> AST.ident **) |
---|
| 538 | let rTLabs_call_ident ge s = |
---|
| 539 | let s0 = s in |
---|
| 540 | (let { ras_state = s'; ras_fn_stack = stk } = s0 in |
---|
| 541 | (match s' with |
---|
| 542 | | RTLabs_semantics.State (f, x, x0) -> |
---|
[2903] | 543 | (fun _ -> assert false (* absurd case *)) |
---|
| 544 | | RTLabs_semantics.Callstate (fid, x, x0, x1, x2, x3) -> (fun _ -> fid) |
---|
[2730] | 545 | | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> |
---|
[2903] | 546 | (fun _ -> assert false (* absurd case *)) |
---|
[2730] | 547 | | RTLabs_semantics.Finalstate x -> |
---|
[2903] | 548 | (fun _ -> assert false (* absurd case *)))) __ |
---|
[2730] | 549 | |
---|
| 550 | (** val rTLabs_status : |
---|
| 551 | RTLabs_semantics.genv -> StructuredTraces.abstract_status **) |
---|
| 552 | let rTLabs_status ge = |
---|
| 553 | { StructuredTraces.as_pc = rTLabs_deqset; StructuredTraces.as_pc_of = |
---|
| 554 | (Obj.magic (rTLabs_ext_state_to_pc ge)); StructuredTraces.as_classify = |
---|
[2773] | 555 | (fun h -> rTLabs_classify (Obj.magic h).ras_state); |
---|
[2730] | 556 | StructuredTraces.as_label_of_pc = |
---|
[2773] | 557 | (Obj.magic (rTLabs_pc_to_cost_label ge)); StructuredTraces.as_result = |
---|
| 558 | (fun h -> RTLabs_semantics.rTLabs_is_final (Obj.magic h).ras_state); |
---|
[2730] | 559 | StructuredTraces.as_call_ident = (Obj.magic (rTLabs_call_ident ge)); |
---|
| 560 | StructuredTraces.as_tailcall_ident = (fun s -> assert false |
---|
| 561 | (* absurd case *)) } |
---|
| 562 | |
---|