[2829] | 1 | open Preamble |
---|
| 2 | |
---|
[2951] | 3 | open ExtraMonads |
---|
| 4 | |
---|
| 5 | open Deqsets_extra |
---|
| 6 | |
---|
| 7 | open State |
---|
| 8 | |
---|
| 9 | open Bind_new |
---|
| 10 | |
---|
| 11 | open BindLists |
---|
| 12 | |
---|
| 13 | open Blocks |
---|
| 14 | |
---|
| 15 | open TranslateUtils |
---|
| 16 | |
---|
[2829] | 17 | open ExtraGlobalenvs |
---|
| 18 | |
---|
| 19 | open I8051bis |
---|
| 20 | |
---|
| 21 | open String |
---|
| 22 | |
---|
| 23 | open Sets |
---|
| 24 | |
---|
| 25 | open Listb |
---|
| 26 | |
---|
| 27 | open LabelledObjects |
---|
| 28 | |
---|
| 29 | open BitVectorTrie |
---|
| 30 | |
---|
| 31 | open Graphs |
---|
| 32 | |
---|
| 33 | open I8051 |
---|
| 34 | |
---|
| 35 | open Order |
---|
| 36 | |
---|
| 37 | open Registers |
---|
| 38 | |
---|
| 39 | open BackEndOps |
---|
| 40 | |
---|
| 41 | open Joint |
---|
| 42 | |
---|
| 43 | open BEMem |
---|
| 44 | |
---|
| 45 | open CostLabel |
---|
| 46 | |
---|
| 47 | open Events |
---|
| 48 | |
---|
| 49 | open IOMonad |
---|
| 50 | |
---|
| 51 | open IO |
---|
| 52 | |
---|
| 53 | open Extra_bool |
---|
| 54 | |
---|
| 55 | open Coqlib |
---|
| 56 | |
---|
| 57 | open Values |
---|
| 58 | |
---|
| 59 | open FrontEndVal |
---|
| 60 | |
---|
| 61 | open Hide |
---|
| 62 | |
---|
| 63 | open ByteValues |
---|
| 64 | |
---|
| 65 | open Division |
---|
| 66 | |
---|
| 67 | open Z |
---|
| 68 | |
---|
| 69 | open BitVectorZ |
---|
| 70 | |
---|
| 71 | open Pointers |
---|
| 72 | |
---|
| 73 | open GenMem |
---|
| 74 | |
---|
| 75 | open FrontEndMem |
---|
| 76 | |
---|
| 77 | open Proper |
---|
| 78 | |
---|
| 79 | open PositiveMap |
---|
| 80 | |
---|
| 81 | open Deqsets |
---|
| 82 | |
---|
| 83 | open Extralib |
---|
| 84 | |
---|
| 85 | open Lists |
---|
| 86 | |
---|
| 87 | open Identifiers |
---|
| 88 | |
---|
| 89 | open Exp |
---|
| 90 | |
---|
| 91 | open Arithmetic |
---|
| 92 | |
---|
| 93 | open Vector |
---|
| 94 | |
---|
| 95 | open Div_and_mod |
---|
| 96 | |
---|
| 97 | open Util |
---|
| 98 | |
---|
| 99 | open FoldStuff |
---|
| 100 | |
---|
| 101 | open BitVector |
---|
| 102 | |
---|
| 103 | open Extranat |
---|
| 104 | |
---|
| 105 | open Integers |
---|
| 106 | |
---|
| 107 | open AST |
---|
| 108 | |
---|
| 109 | open ErrorMessages |
---|
| 110 | |
---|
| 111 | open Option |
---|
| 112 | |
---|
| 113 | open Setoids |
---|
| 114 | |
---|
| 115 | open Monad |
---|
| 116 | |
---|
| 117 | open Jmeq |
---|
| 118 | |
---|
| 119 | open Russell |
---|
| 120 | |
---|
| 121 | open Positive |
---|
| 122 | |
---|
| 123 | open PreIdentifiers |
---|
| 124 | |
---|
| 125 | open Bool |
---|
| 126 | |
---|
| 127 | open Relations |
---|
| 128 | |
---|
| 129 | open Nat |
---|
| 130 | |
---|
| 131 | open List |
---|
| 132 | |
---|
| 133 | open Hints_declaration |
---|
| 134 | |
---|
| 135 | open Core_notation |
---|
| 136 | |
---|
| 137 | open Pts |
---|
| 138 | |
---|
| 139 | open Logic |
---|
| 140 | |
---|
| 141 | open Types |
---|
| 142 | |
---|
| 143 | open Errors |
---|
| 144 | |
---|
| 145 | open Globalenvs |
---|
| 146 | |
---|
| 147 | open Joint_semantics |
---|
| 148 | |
---|
[2951] | 149 | open SemanticsUtils |
---|
| 150 | |
---|
[2829] | 151 | open StructuredTraces |
---|
| 152 | |
---|
| 153 | type evaluation_params = { globals : AST.ident List.list; |
---|
| 154 | ev_genv : Joint_semantics.genv } |
---|
| 155 | |
---|
| 156 | (** val evaluation_params_rect_Type4 : |
---|
[2960] | 157 | Joint_semantics.sem_params -> (AST.ident List.list -> |
---|
[2829] | 158 | Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **) |
---|
[3019] | 159 | let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_316 = |
---|
| 160 | let { globals = globals0; ev_genv = ev_genv0 } = x_316 in |
---|
[2960] | 161 | h_mk_evaluation_params globals0 ev_genv0 |
---|
[2829] | 162 | |
---|
| 163 | (** val evaluation_params_rect_Type5 : |
---|
[2960] | 164 | Joint_semantics.sem_params -> (AST.ident List.list -> |
---|
[2829] | 165 | Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **) |
---|
[3019] | 166 | let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_318 = |
---|
| 167 | let { globals = globals0; ev_genv = ev_genv0 } = x_318 in |
---|
[2960] | 168 | h_mk_evaluation_params globals0 ev_genv0 |
---|
[2829] | 169 | |
---|
| 170 | (** val evaluation_params_rect_Type3 : |
---|
[2960] | 171 | Joint_semantics.sem_params -> (AST.ident List.list -> |
---|
[2829] | 172 | Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **) |
---|
[3019] | 173 | let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_320 = |
---|
| 174 | let { globals = globals0; ev_genv = ev_genv0 } = x_320 in |
---|
[2960] | 175 | h_mk_evaluation_params globals0 ev_genv0 |
---|
[2829] | 176 | |
---|
| 177 | (** val evaluation_params_rect_Type2 : |
---|
[2960] | 178 | Joint_semantics.sem_params -> (AST.ident List.list -> |
---|
[2829] | 179 | Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **) |
---|
[3019] | 180 | let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_322 = |
---|
| 181 | let { globals = globals0; ev_genv = ev_genv0 } = x_322 in |
---|
[2960] | 182 | h_mk_evaluation_params globals0 ev_genv0 |
---|
[2829] | 183 | |
---|
| 184 | (** val evaluation_params_rect_Type1 : |
---|
[2960] | 185 | Joint_semantics.sem_params -> (AST.ident List.list -> |
---|
[2829] | 186 | Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **) |
---|
[3019] | 187 | let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_324 = |
---|
| 188 | let { globals = globals0; ev_genv = ev_genv0 } = x_324 in |
---|
[2960] | 189 | h_mk_evaluation_params globals0 ev_genv0 |
---|
[2829] | 190 | |
---|
| 191 | (** val evaluation_params_rect_Type0 : |
---|
[2960] | 192 | Joint_semantics.sem_params -> (AST.ident List.list -> |
---|
[2829] | 193 | Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **) |
---|
[3019] | 194 | let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_326 = |
---|
| 195 | let { globals = globals0; ev_genv = ev_genv0 } = x_326 in |
---|
[2960] | 196 | h_mk_evaluation_params globals0 ev_genv0 |
---|
[2829] | 197 | |
---|
[2960] | 198 | (** val globals : |
---|
| 199 | Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list **) |
---|
| 200 | let rec globals p xxx = |
---|
[2829] | 201 | xxx.globals |
---|
| 202 | |
---|
[2960] | 203 | (** val ev_genv : |
---|
| 204 | Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv **) |
---|
| 205 | let rec ev_genv p xxx = |
---|
[2829] | 206 | xxx.ev_genv |
---|
| 207 | |
---|
| 208 | (** val evaluation_params_inv_rect_Type4 : |
---|
[2960] | 209 | Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list |
---|
[2829] | 210 | -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **) |
---|
[2960] | 211 | let evaluation_params_inv_rect_Type4 x1 hterm h1 = |
---|
| 212 | let hcut = evaluation_params_rect_Type4 x1 h1 hterm in hcut __ |
---|
[2829] | 213 | |
---|
| 214 | (** val evaluation_params_inv_rect_Type3 : |
---|
[2960] | 215 | Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list |
---|
[2829] | 216 | -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **) |
---|
[2960] | 217 | let evaluation_params_inv_rect_Type3 x1 hterm h1 = |
---|
| 218 | let hcut = evaluation_params_rect_Type3 x1 h1 hterm in hcut __ |
---|
[2829] | 219 | |
---|
| 220 | (** val evaluation_params_inv_rect_Type2 : |
---|
[2960] | 221 | Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list |
---|
[2829] | 222 | -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **) |
---|
[2960] | 223 | let evaluation_params_inv_rect_Type2 x1 hterm h1 = |
---|
| 224 | let hcut = evaluation_params_rect_Type2 x1 h1 hterm in hcut __ |
---|
[2829] | 225 | |
---|
| 226 | (** val evaluation_params_inv_rect_Type1 : |
---|
[2960] | 227 | Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list |
---|
[2829] | 228 | -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **) |
---|
[2960] | 229 | let evaluation_params_inv_rect_Type1 x1 hterm h1 = |
---|
| 230 | let hcut = evaluation_params_rect_Type1 x1 h1 hterm in hcut __ |
---|
[2829] | 231 | |
---|
| 232 | (** val evaluation_params_inv_rect_Type0 : |
---|
[2960] | 233 | Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list |
---|
[2829] | 234 | -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **) |
---|
[2960] | 235 | let evaluation_params_inv_rect_Type0 x1 hterm h1 = |
---|
| 236 | let hcut = evaluation_params_rect_Type0 x1 h1 hterm in hcut __ |
---|
[2829] | 237 | |
---|
[2960] | 238 | (** val evaluation_params_discr : |
---|
| 239 | Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> |
---|
| 240 | __ **) |
---|
| 241 | let evaluation_params_discr a1 x y = |
---|
| 242 | Logic.eq_rect_Type2 x |
---|
| 243 | (let { globals = a0; ev_genv = a10 } = x in |
---|
| 244 | Obj.magic (fun _ dH -> dH __ __)) y |
---|
| 245 | |
---|
[2829] | 246 | (** val evaluation_params_jmdiscr : |
---|
[2960] | 247 | Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> |
---|
| 248 | __ **) |
---|
| 249 | let evaluation_params_jmdiscr a1 x y = |
---|
[2829] | 250 | Logic.eq_rect_Type2 x |
---|
[2960] | 251 | (let { globals = a0; ev_genv = a10 } = x in |
---|
| 252 | Obj.magic (fun _ dH -> dH __ __)) y |
---|
[2829] | 253 | |
---|
[2960] | 254 | (** val dpi1__o__ev_genv__o__inject : |
---|
| 255 | Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair -> |
---|
| 256 | Joint_semantics.genv Types.sig0 **) |
---|
| 257 | let dpi1__o__ev_genv__o__inject x0 x2 = |
---|
| 258 | x2.Types.dpi1.ev_genv |
---|
[2951] | 259 | |
---|
[2960] | 260 | (** val dpi1__o__ev_genv__o__genv_to_genv_t__o__inject : |
---|
| 261 | Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair -> |
---|
| 262 | Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t |
---|
| 263 | Types.sig0 **) |
---|
| 264 | let dpi1__o__ev_genv__o__genv_to_genv_t__o__inject x0 x2 = |
---|
| 265 | Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0) |
---|
| 266 | x2.Types.dpi1.globals x2.Types.dpi1.ev_genv |
---|
[2829] | 267 | |
---|
[2960] | 268 | (** val dpi1__o__ev_genv__o__genv_to_genv_t : |
---|
| 269 | Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair -> |
---|
| 270 | Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **) |
---|
| 271 | let dpi1__o__ev_genv__o__genv_to_genv_t x0 x2 = |
---|
| 272 | let p = Joint_semantics.spp'__o__spp x0 in |
---|
| 273 | let globals0 = x2.Types.dpi1.globals in |
---|
| 274 | let g = x2.Types.dpi1.ev_genv in g.Joint_semantics.ge |
---|
[2829] | 275 | |
---|
[2960] | 276 | (** val eject__o__ev_genv__o__inject : |
---|
| 277 | Joint_semantics.sem_params -> evaluation_params Types.sig0 -> |
---|
| 278 | Joint_semantics.genv Types.sig0 **) |
---|
| 279 | let eject__o__ev_genv__o__inject x0 x2 = |
---|
| 280 | (Types.pi1 x2).ev_genv |
---|
[2829] | 281 | |
---|
[2960] | 282 | (** val eject__o__ev_genv__o__genv_to_genv_t__o__inject : |
---|
| 283 | Joint_semantics.sem_params -> evaluation_params Types.sig0 -> |
---|
| 284 | Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t |
---|
| 285 | Types.sig0 **) |
---|
| 286 | let eject__o__ev_genv__o__genv_to_genv_t__o__inject x0 x2 = |
---|
| 287 | Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0) |
---|
| 288 | (Types.pi1 x2).globals (Types.pi1 x2).ev_genv |
---|
[2829] | 289 | |
---|
[2960] | 290 | (** val eject__o__ev_genv__o__genv_to_genv_t : |
---|
| 291 | Joint_semantics.sem_params -> evaluation_params Types.sig0 -> |
---|
| 292 | Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **) |
---|
| 293 | let eject__o__ev_genv__o__genv_to_genv_t x0 x2 = |
---|
| 294 | let p = Joint_semantics.spp'__o__spp x0 in |
---|
| 295 | let globals0 = (Types.pi1 x2).globals in |
---|
| 296 | let g = (Types.pi1 x2).ev_genv in g.Joint_semantics.ge |
---|
[2829] | 297 | |
---|
[2960] | 298 | (** val ev_genv__o__genv_to_genv_t : |
---|
| 299 | Joint_semantics.sem_params -> evaluation_params -> |
---|
| 300 | Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **) |
---|
| 301 | let ev_genv__o__genv_to_genv_t x0 x1 = |
---|
| 302 | let p = Joint_semantics.spp'__o__spp x0 in |
---|
| 303 | let globals0 = x1.globals in let g = x1.ev_genv in g.Joint_semantics.ge |
---|
[2829] | 304 | |
---|
[2960] | 305 | (** val ev_genv__o__genv_to_genv_t__o__inject : |
---|
| 306 | Joint_semantics.sem_params -> evaluation_params -> |
---|
| 307 | Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t |
---|
| 308 | Types.sig0 **) |
---|
| 309 | let ev_genv__o__genv_to_genv_t__o__inject x0 x1 = |
---|
| 310 | Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0) |
---|
| 311 | x1.globals x1.ev_genv |
---|
| 312 | |
---|
| 313 | (** val ev_genv__o__inject : |
---|
| 314 | Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv |
---|
| 315 | Types.sig0 **) |
---|
| 316 | let ev_genv__o__inject x0 x1 = |
---|
| 317 | x1.ev_genv |
---|
| 318 | |
---|
| 319 | (** val dpi1__o__ev_genv : |
---|
| 320 | Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair -> |
---|
| 321 | Joint_semantics.genv **) |
---|
| 322 | let dpi1__o__ev_genv x0 x2 = |
---|
| 323 | x2.Types.dpi1.ev_genv |
---|
| 324 | |
---|
| 325 | (** val eject__o__ev_genv : |
---|
| 326 | Joint_semantics.sem_params -> evaluation_params Types.sig0 -> |
---|
| 327 | Joint_semantics.genv **) |
---|
| 328 | let eject__o__ev_genv x0 x2 = |
---|
| 329 | (Types.pi1 x2).ev_genv |
---|
| 330 | |
---|
[2829] | 331 | type prog_params = { prog_spars : Joint_semantics.sem_params; |
---|
| 332 | prog : Joint.joint_program; |
---|
| 333 | stack_sizes : (AST.ident -> Nat.nat Types.option) } |
---|
| 334 | |
---|
| 335 | (** val prog_params_rect_Type4 : |
---|
| 336 | (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> |
---|
| 337 | Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **) |
---|
[3019] | 338 | let rec prog_params_rect_Type4 h_mk_prog_params x_342 = |
---|
[2829] | 339 | let { prog_spars = prog_spars0; prog = prog0; stack_sizes = |
---|
[3019] | 340 | stack_sizes0 } = x_342 |
---|
[2829] | 341 | in |
---|
| 342 | h_mk_prog_params prog_spars0 prog0 stack_sizes0 |
---|
| 343 | |
---|
| 344 | (** val prog_params_rect_Type5 : |
---|
| 345 | (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> |
---|
| 346 | Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **) |
---|
[3019] | 347 | let rec prog_params_rect_Type5 h_mk_prog_params x_344 = |
---|
[2829] | 348 | let { prog_spars = prog_spars0; prog = prog0; stack_sizes = |
---|
[3019] | 349 | stack_sizes0 } = x_344 |
---|
[2829] | 350 | in |
---|
| 351 | h_mk_prog_params prog_spars0 prog0 stack_sizes0 |
---|
| 352 | |
---|
| 353 | (** val prog_params_rect_Type3 : |
---|
| 354 | (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> |
---|
| 355 | Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **) |
---|
[3019] | 356 | let rec prog_params_rect_Type3 h_mk_prog_params x_346 = |
---|
[2829] | 357 | let { prog_spars = prog_spars0; prog = prog0; stack_sizes = |
---|
[3019] | 358 | stack_sizes0 } = x_346 |
---|
[2829] | 359 | in |
---|
| 360 | h_mk_prog_params prog_spars0 prog0 stack_sizes0 |
---|
| 361 | |
---|
| 362 | (** val prog_params_rect_Type2 : |
---|
| 363 | (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> |
---|
| 364 | Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **) |
---|
[3019] | 365 | let rec prog_params_rect_Type2 h_mk_prog_params x_348 = |
---|
[2829] | 366 | let { prog_spars = prog_spars0; prog = prog0; stack_sizes = |
---|
[3019] | 367 | stack_sizes0 } = x_348 |
---|
[2829] | 368 | in |
---|
| 369 | h_mk_prog_params prog_spars0 prog0 stack_sizes0 |
---|
| 370 | |
---|
| 371 | (** val prog_params_rect_Type1 : |
---|
| 372 | (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> |
---|
| 373 | Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **) |
---|
[3019] | 374 | let rec prog_params_rect_Type1 h_mk_prog_params x_350 = |
---|
[2829] | 375 | let { prog_spars = prog_spars0; prog = prog0; stack_sizes = |
---|
[3019] | 376 | stack_sizes0 } = x_350 |
---|
[2829] | 377 | in |
---|
| 378 | h_mk_prog_params prog_spars0 prog0 stack_sizes0 |
---|
| 379 | |
---|
| 380 | (** val prog_params_rect_Type0 : |
---|
| 381 | (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> |
---|
| 382 | Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **) |
---|
[3019] | 383 | let rec prog_params_rect_Type0 h_mk_prog_params x_352 = |
---|
[2829] | 384 | let { prog_spars = prog_spars0; prog = prog0; stack_sizes = |
---|
[3019] | 385 | stack_sizes0 } = x_352 |
---|
[2829] | 386 | in |
---|
| 387 | h_mk_prog_params prog_spars0 prog0 stack_sizes0 |
---|
| 388 | |
---|
| 389 | (** val prog_spars : prog_params -> Joint_semantics.sem_params **) |
---|
| 390 | let rec prog_spars xxx = |
---|
| 391 | xxx.prog_spars |
---|
| 392 | |
---|
| 393 | (** val prog : prog_params -> Joint.joint_program **) |
---|
| 394 | let rec prog xxx = |
---|
| 395 | xxx.prog |
---|
| 396 | |
---|
| 397 | (** val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option **) |
---|
| 398 | let rec stack_sizes xxx = |
---|
| 399 | xxx.stack_sizes |
---|
| 400 | |
---|
| 401 | (** val prog_params_inv_rect_Type4 : |
---|
| 402 | prog_params -> (Joint_semantics.sem_params -> Joint.joint_program -> |
---|
| 403 | (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **) |
---|
| 404 | let prog_params_inv_rect_Type4 hterm h1 = |
---|
| 405 | let hcut = prog_params_rect_Type4 h1 hterm in hcut __ |
---|
| 406 | |
---|
| 407 | (** val prog_params_inv_rect_Type3 : |
---|
| 408 | prog_params -> (Joint_semantics.sem_params -> Joint.joint_program -> |
---|
| 409 | (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **) |
---|
| 410 | let prog_params_inv_rect_Type3 hterm h1 = |
---|
| 411 | let hcut = prog_params_rect_Type3 h1 hterm in hcut __ |
---|
| 412 | |
---|
| 413 | (** val prog_params_inv_rect_Type2 : |
---|
| 414 | prog_params -> (Joint_semantics.sem_params -> Joint.joint_program -> |
---|
| 415 | (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **) |
---|
| 416 | let prog_params_inv_rect_Type2 hterm h1 = |
---|
| 417 | let hcut = prog_params_rect_Type2 h1 hterm in hcut __ |
---|
| 418 | |
---|
| 419 | (** val prog_params_inv_rect_Type1 : |
---|
| 420 | prog_params -> (Joint_semantics.sem_params -> Joint.joint_program -> |
---|
| 421 | (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **) |
---|
| 422 | let prog_params_inv_rect_Type1 hterm h1 = |
---|
| 423 | let hcut = prog_params_rect_Type1 h1 hterm in hcut __ |
---|
| 424 | |
---|
| 425 | (** val prog_params_inv_rect_Type0 : |
---|
| 426 | prog_params -> (Joint_semantics.sem_params -> Joint.joint_program -> |
---|
| 427 | (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **) |
---|
| 428 | let prog_params_inv_rect_Type0 hterm h1 = |
---|
| 429 | let hcut = prog_params_rect_Type0 h1 hterm in hcut __ |
---|
| 430 | |
---|
| 431 | (** val prog_params_jmdiscr : prog_params -> prog_params -> __ **) |
---|
| 432 | let prog_params_jmdiscr x y = |
---|
| 433 | Logic.eq_rect_Type2 x |
---|
| 434 | (let { prog_spars = a0; prog = a1; stack_sizes = a2 } = x in |
---|
| 435 | Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
| 436 | |
---|
[2960] | 437 | (** val prog_spars__o__spp' : |
---|
[2951] | 438 | prog_params -> Joint_semantics.serialized_params **) |
---|
[2960] | 439 | let prog_spars__o__spp' x0 = |
---|
| 440 | x0.prog_spars.Joint_semantics.spp' |
---|
[2951] | 441 | |
---|
[2960] | 442 | (** val prog_spars__o__spp'__o__msu_pars : |
---|
[2829] | 443 | prog_params -> Joint.joint_closed_internal_function |
---|
| 444 | Joint_semantics.sem_unserialized_params **) |
---|
[2960] | 445 | let prog_spars__o__spp'__o__msu_pars x0 = |
---|
| 446 | Joint_semantics.spp'__o__msu_pars x0.prog_spars |
---|
[2829] | 447 | |
---|
[2960] | 448 | (** val prog_spars__o__spp'__o__msu_pars__o__st_pars : |
---|
[2829] | 449 | prog_params -> Joint_semantics.sem_state_params **) |
---|
[2960] | 450 | let prog_spars__o__spp'__o__msu_pars__o__st_pars x0 = |
---|
| 451 | Joint_semantics.spp'__o__msu_pars__o__st_pars x0.prog_spars |
---|
[2829] | 452 | |
---|
[2960] | 453 | (** val prog_spars__o__spp'__o__spp : prog_params -> Joint.params **) |
---|
| 454 | let prog_spars__o__spp'__o__spp x0 = |
---|
| 455 | Joint_semantics.spp'__o__spp x0.prog_spars |
---|
[2829] | 456 | |
---|
[2960] | 457 | (** val prog_spars__o__spp'__o__spp__o__stmt_pars : |
---|
[2829] | 458 | prog_params -> Joint.stmt_params **) |
---|
[2960] | 459 | let prog_spars__o__spp'__o__spp__o__stmt_pars x0 = |
---|
| 460 | Joint_semantics.spp'__o__spp__o__stmt_pars x0.prog_spars |
---|
[2829] | 461 | |
---|
[2960] | 462 | (** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars : |
---|
[2829] | 463 | prog_params -> Joint.uns_params **) |
---|
[2960] | 464 | let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 = |
---|
| 465 | Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars x0.prog_spars |
---|
[2829] | 466 | |
---|
[2960] | 467 | (** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars : |
---|
[2829] | 468 | prog_params -> Joint.unserialized_params **) |
---|
[2960] | 469 | let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 = |
---|
| 470 | Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars |
---|
| 471 | x0.prog_spars |
---|
[2829] | 472 | |
---|
[2960] | 473 | (** val joint_make_global : prog_params -> evaluation_params **) |
---|
| 474 | let joint_make_global p = |
---|
| 475 | { globals = (AST.prog_var_names p.prog.Joint.joint_prog); ev_genv = |
---|
| 476 | (SemanticsUtils.joint_globalenv p.prog_spars p.prog p.stack_sizes) } |
---|
| 477 | |
---|
| 478 | (** val joint_make_global__o__ev_genv : |
---|
| 479 | prog_params -> Joint_semantics.genv **) |
---|
| 480 | let joint_make_global__o__ev_genv x0 = |
---|
| 481 | (joint_make_global x0).ev_genv |
---|
| 482 | |
---|
| 483 | (** val joint_make_global__o__ev_genv__o__genv_to_genv_t : |
---|
| 484 | prog_params -> Joint.joint_closed_internal_function AST.fundef |
---|
| 485 | Globalenvs.genv_t **) |
---|
| 486 | let joint_make_global__o__ev_genv__o__genv_to_genv_t x0 = |
---|
| 487 | ev_genv__o__genv_to_genv_t x0.prog_spars (joint_make_global x0) |
---|
| 488 | |
---|
| 489 | (** val joint_make_global__o__ev_genv__o__genv_to_genv_t__o__inject : |
---|
| 490 | prog_params -> Joint.joint_closed_internal_function AST.fundef |
---|
| 491 | Globalenvs.genv_t Types.sig0 **) |
---|
| 492 | let joint_make_global__o__ev_genv__o__genv_to_genv_t__o__inject x0 = |
---|
| 493 | ev_genv__o__genv_to_genv_t__o__inject x0.prog_spars (joint_make_global x0) |
---|
| 494 | |
---|
| 495 | (** val joint_make_global__o__ev_genv__o__inject : |
---|
| 496 | prog_params -> Joint_semantics.genv Types.sig0 **) |
---|
| 497 | let joint_make_global__o__ev_genv__o__inject x0 = |
---|
| 498 | ev_genv__o__inject x0.prog_spars (joint_make_global x0) |
---|
| 499 | |
---|
| 500 | (** val joint_make_global__o__inject : |
---|
| 501 | prog_params -> evaluation_params Types.sig0 **) |
---|
| 502 | let joint_make_global__o__inject x0 = |
---|
| 503 | joint_make_global x0 |
---|
| 504 | |
---|
[2968] | 505 | (** val make_initial_state : |
---|
| 506 | prog_params -> Joint_semantics.state_pc Errors.res **) |
---|
[2829] | 507 | let make_initial_state pars = |
---|
| 508 | let p = pars.prog in |
---|
[2960] | 509 | let ge = ev_genv pars.prog_spars in |
---|
[2968] | 510 | Obj.magic |
---|
| 511 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
| 512 | (Obj.magic (Globalenvs.init_mem (fun x -> x) p.Joint.joint_prog)) |
---|
| 513 | (fun m0 -> |
---|
| 514 | (let { Types.fst = m; Types.snd = spb } = |
---|
| 515 | GenMem.alloc m0 (Z.z_of_nat Nat.O) I8051bis.external_ram_size |
---|
| 516 | in |
---|
| 517 | (fun _ -> |
---|
| 518 | let globals_size = |
---|
| 519 | Joint.globals_stacksize |
---|
| 520 | (Joint_semantics.spp'__o__spp pars.prog_spars) p |
---|
| 521 | in |
---|
| 522 | let spp = { Pointers.pblock = spb; Pointers.poff = |
---|
| 523 | (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
| 524 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
[3019] | 525 | (Nat.S Nat.O)))))))))))))))) |
---|
| 526 | (Z.zopp (Z.z_of_nat (Nat.S globals_size)))) } |
---|
[2968] | 527 | in |
---|
[3001] | 528 | let main = AST.prog_main p.Joint.joint_prog in |
---|
[2968] | 529 | let st = { Joint_semantics.st_frms = (Types.Some |
---|
| 530 | (prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT); |
---|
| 531 | Joint_semantics.istack = Joint_semantics.Empty_is; |
---|
| 532 | Joint_semantics.carry = (ByteValues.BBbit Bool.False); |
---|
| 533 | Joint_semantics.regs = |
---|
| 534 | ((prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT |
---|
| 535 | spp); Joint_semantics.m = m; Joint_semantics.stack_usage = |
---|
| 536 | globals_size } |
---|
| 537 | in |
---|
| 538 | Monad.m_return0 (Monad.max_def Errors.res0) |
---|
| 539 | { Joint_semantics.st_no_pc = |
---|
| 540 | (Joint_semantics.set_sp |
---|
| 541 | (prog_spars__o__spp'__o__msu_pars__o__st_pars pars) spp st); |
---|
| 542 | Joint_semantics.pc = Joint_semantics.init_pc; |
---|
| 543 | Joint_semantics.last_pop = (Joint_semantics.null_pc Positive.One) })) |
---|
| 544 | __)) |
---|
[2829] | 545 | |
---|
| 546 | (** val joint_classify_step : |
---|
[2960] | 547 | Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step -> |
---|
| 548 | StructuredTraces.status_class **) |
---|
| 549 | let joint_classify_step p g = function |
---|
[2829] | 550 | | Joint.COST_LABEL x -> StructuredTraces.Cl_other |
---|
| 551 | | Joint.CALL (f, args, dest) -> StructuredTraces.Cl_call |
---|
| 552 | | Joint.COND (x, x0) -> StructuredTraces.Cl_jump |
---|
| 553 | | Joint.Step_seq x -> StructuredTraces.Cl_other |
---|
| 554 | |
---|
| 555 | (** val joint_classify_final : |
---|
[2960] | 556 | Joint.unserialized_params -> Joint.joint_fin_step -> |
---|
[2829] | 557 | StructuredTraces.status_class **) |
---|
| 558 | let joint_classify_final p = function |
---|
| 559 | | Joint.GOTO x -> StructuredTraces.Cl_other |
---|
| 560 | | Joint.RETURN -> StructuredTraces.Cl_return |
---|
| 561 | | Joint.TAILCALL (f, args) -> StructuredTraces.Cl_tailcall |
---|
| 562 | |
---|
| 563 | (** val joint_classify : |
---|
[2960] | 564 | Joint_semantics.sem_params -> evaluation_params -> |
---|
| 565 | Joint_semantics.state_pc -> StructuredTraces.status_class **) |
---|
| 566 | let joint_classify p pars st = |
---|
| 567 | match Joint_semantics.fetch_statement p pars.globals pars.ev_genv |
---|
| 568 | st.Joint_semantics.pc with |
---|
[2829] | 569 | | Errors.OK i_fn_s -> |
---|
| 570 | (match i_fn_s.Types.snd with |
---|
[2960] | 571 | | Joint.Sequential (s, x) -> |
---|
| 572 | joint_classify_step |
---|
| 573 | (Joint.uns_pars__o__u_pars |
---|
| 574 | (Joint_semantics.spp'__o__spp__o__stmt_pars p)) pars.globals s |
---|
| 575 | | Joint.Final s -> |
---|
| 576 | joint_classify_final |
---|
| 577 | (Joint.uns_pars__o__u_pars |
---|
| 578 | (Joint_semantics.spp'__o__spp__o__stmt_pars p)) s |
---|
[2829] | 579 | | Joint.FCOND (x0, x1, x2) -> StructuredTraces.Cl_jump) |
---|
| 580 | | Errors.Error x -> StructuredTraces.Cl_other |
---|
| 581 | |
---|
| 582 | (** val joint_call_ident : |
---|
[2960] | 583 | Joint_semantics.sem_params -> evaluation_params -> |
---|
| 584 | Joint_semantics.state_pc -> AST.ident **) |
---|
| 585 | let joint_call_ident p pars st = |
---|
[2829] | 586 | let dummy = Positive.One in |
---|
[2960] | 587 | (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv |
---|
| 588 | st.Joint_semantics.pc with |
---|
[2829] | 589 | | Errors.OK x -> |
---|
| 590 | (match x.Types.snd with |
---|
| 591 | | Joint.Sequential (s, next) -> |
---|
| 592 | (match s with |
---|
| 593 | | Joint.COST_LABEL x0 -> dummy |
---|
[2933] | 594 | | Joint.CALL (f', args, dest) -> |
---|
| 595 | (match Obj.magic |
---|
| 596 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
[2960] | 597 | (Joint_semantics.block_of_call p pars.globals |
---|
| 598 | (let p0 = Joint_semantics.spp'__o__spp p in |
---|
| 599 | let globals0 = pars.globals in |
---|
| 600 | let g = pars.ev_genv in g.Joint_semantics.ge) f' |
---|
[2933] | 601 | st.Joint_semantics.st_no_pc) (fun bl -> |
---|
| 602 | Obj.magic |
---|
[2960] | 603 | (Joint_semantics.fetch_internal_function pars.globals |
---|
| 604 | pars.ev_genv bl))) with |
---|
[2933] | 605 | | Errors.OK i_f -> i_f.Types.fst |
---|
| 606 | | Errors.Error x0 -> dummy) |
---|
[2829] | 607 | | Joint.COND (x0, x1) -> dummy |
---|
[2933] | 608 | | Joint.Step_seq x0 -> dummy) |
---|
[2829] | 609 | | Joint.Final x0 -> dummy |
---|
| 610 | | Joint.FCOND (x0, x1, x2) -> dummy) |
---|
| 611 | | Errors.Error x -> dummy) |
---|
| 612 | |
---|
| 613 | (** val joint_tailcall_ident : |
---|
[2960] | 614 | Joint_semantics.sem_params -> evaluation_params -> |
---|
| 615 | Joint_semantics.state_pc -> AST.ident **) |
---|
| 616 | let joint_tailcall_ident p pars st = |
---|
[2829] | 617 | let dummy = Positive.One in |
---|
[2960] | 618 | (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv |
---|
| 619 | st.Joint_semantics.pc with |
---|
[2829] | 620 | | Errors.OK x -> |
---|
| 621 | (match x.Types.snd with |
---|
| 622 | | Joint.Sequential (x0, x1) -> dummy |
---|
| 623 | | Joint.Final s -> |
---|
| 624 | (match s with |
---|
| 625 | | Joint.GOTO x0 -> dummy |
---|
| 626 | | Joint.RETURN -> dummy |
---|
| 627 | | Joint.TAILCALL (f', args) -> |
---|
| 628 | (match Obj.magic |
---|
| 629 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
[2960] | 630 | (Joint_semantics.block_of_call p pars.globals |
---|
| 631 | (let p0 = Joint_semantics.spp'__o__spp p in |
---|
| 632 | let globals0 = pars.globals in |
---|
| 633 | let g = pars.ev_genv in g.Joint_semantics.ge) f' |
---|
[2829] | 634 | st.Joint_semantics.st_no_pc) (fun bl -> |
---|
| 635 | Obj.magic |
---|
[2960] | 636 | (Joint_semantics.fetch_internal_function pars.globals |
---|
| 637 | pars.ev_genv bl))) with |
---|
[2829] | 638 | | Errors.OK i_f -> i_f.Types.fst |
---|
| 639 | | Errors.Error x0 -> dummy)) |
---|
| 640 | | Joint.FCOND (x0, x1, x2) -> dummy) |
---|
| 641 | | Errors.Error x -> dummy) |
---|
| 642 | |
---|
| 643 | (** val pcDeq : Deqsets.deqSet **) |
---|
| 644 | let pcDeq = |
---|
| 645 | Obj.magic ByteValues.eq_program_counter |
---|
| 646 | |
---|
| 647 | (** val cost_label_of_stmt : |
---|
[2997] | 648 | Joint.stmt_params -> AST.ident List.list -> Joint.joint_statement -> |
---|
| 649 | CostLabel.costlabel Types.option **) |
---|
| 650 | let cost_label_of_stmt p g = function |
---|
[2829] | 651 | | Joint.Sequential (s0, x) -> |
---|
| 652 | (match s0 with |
---|
| 653 | | Joint.COST_LABEL lbl -> Types.Some lbl |
---|
| 654 | | Joint.CALL (x0, x1, x2) -> Types.None |
---|
| 655 | | Joint.COND (x0, x1) -> Types.None |
---|
| 656 | | Joint.Step_seq x0 -> Types.None) |
---|
| 657 | | Joint.Final x -> Types.None |
---|
| 658 | | Joint.FCOND (x0, x1, x2) -> Types.None |
---|
| 659 | |
---|
| 660 | (** val joint_label_of_pc : |
---|
[2960] | 661 | Joint_semantics.sem_params -> evaluation_params -> |
---|
| 662 | ByteValues.program_counter -> CostLabel.costlabel Types.option **) |
---|
| 663 | let joint_label_of_pc p pars pc = |
---|
| 664 | match Joint_semantics.fetch_statement p pars.globals pars.ev_genv pc with |
---|
[2997] | 665 | | Errors.OK fn_stmt -> |
---|
| 666 | cost_label_of_stmt (Joint_semantics.spp'__o__spp__o__stmt_pars p) |
---|
| 667 | pars.globals fn_stmt.Types.snd |
---|
[2829] | 668 | | Errors.Error x -> Types.None |
---|
| 669 | |
---|
[2951] | 670 | (** val exit_pc' : ByteValues.program_counter **) |
---|
| 671 | let exit_pc' = |
---|
| 672 | { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O))); |
---|
| 673 | ByteValues.pc_offset = (Positive.P1 Positive.One) } |
---|
| 674 | |
---|
| 675 | (** val joint_final : |
---|
[2960] | 676 | Joint_semantics.sem_params -> evaluation_params -> |
---|
| 677 | Joint_semantics.state_pc -> Integers.int Types.option **) |
---|
| 678 | let joint_final p pars st = |
---|
| 679 | let ge = pars.ev_genv in |
---|
| 680 | (match ByteValues.eq_program_counter st.Joint_semantics.pc exit_pc' with |
---|
| 681 | | Bool.True -> |
---|
| 682 | let ret = |
---|
| 683 | (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main |
---|
| 684 | in |
---|
[2967] | 685 | (match Obj.magic |
---|
| 686 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
| 687 | (Obj.magic |
---|
| 688 | (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result |
---|
| 689 | pars.globals |
---|
| 690 | (let p0 = Joint_semantics.spp'__o__spp p in |
---|
| 691 | let globals0 = pars.globals in |
---|
| 692 | let g = ge in g.Joint_semantics.ge) ret |
---|
| 693 | st.Joint_semantics.st_no_pc)) (fun vals -> |
---|
| 694 | Obj.magic (ByteValues.word_of_list_beval vals))) with |
---|
| 695 | | Errors.OK v -> Types.Some v |
---|
| 696 | | Errors.Error x -> Types.Some (BitVector.maximum Integers.wordsize)) |
---|
[2960] | 697 | | Bool.False -> Types.None) |
---|
[2951] | 698 | |
---|
[2829] | 699 | (** val joint_abstract_status : |
---|
| 700 | prog_params -> StructuredTraces.abstract_status **) |
---|
| 701 | let joint_abstract_status p = |
---|
| 702 | { StructuredTraces.as_pc = pcDeq; StructuredTraces.as_pc_of = |
---|
| 703 | (Obj.magic |
---|
[2960] | 704 | (Joint_semantics.pc (prog_spars__o__spp'__o__msu_pars__o__st_pars p))); |
---|
| 705 | StructuredTraces.as_classify = |
---|
| 706 | (Obj.magic (joint_classify p.prog_spars (joint_make_global p))); |
---|
[2829] | 707 | StructuredTraces.as_label_of_pc = |
---|
[2960] | 708 | (Obj.magic (joint_label_of_pc p.prog_spars (joint_make_global p))); |
---|
[2829] | 709 | StructuredTraces.as_result = |
---|
[2960] | 710 | (Obj.magic (joint_final p.prog_spars (joint_make_global p))); |
---|
[2951] | 711 | StructuredTraces.as_call_ident = (fun st -> |
---|
[2960] | 712 | joint_call_ident p.prog_spars (joint_make_global p) |
---|
| 713 | (Types.pi1 (Obj.magic st))); StructuredTraces.as_tailcall_ident = |
---|
| 714 | (fun st -> |
---|
| 715 | joint_tailcall_ident p.prog_spars (joint_make_global p) |
---|
| 716 | (Types.pi1 (Obj.magic st))) } |
---|
[2829] | 717 | |
---|
| 718 | (** val joint_status : |
---|
| 719 | Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> |
---|
| 720 | Nat.nat Types.option) -> StructuredTraces.abstract_status **) |
---|
| 721 | let joint_status p prog0 stacksizes = |
---|
| 722 | joint_abstract_status { prog_spars = p; prog = prog0; stack_sizes = |
---|
| 723 | stacksizes } |
---|
| 724 | |
---|