| 1 | open Preamble |
|---|
| 2 | |
|---|
| 3 | open CostLabel |
|---|
| 4 | |
|---|
| 5 | open Proper |
|---|
| 6 | |
|---|
| 7 | open PositiveMap |
|---|
| 8 | |
|---|
| 9 | open Deqsets |
|---|
| 10 | |
|---|
| 11 | open Extralib |
|---|
| 12 | |
|---|
| 13 | open Lists |
|---|
| 14 | |
|---|
| 15 | open Identifiers |
|---|
| 16 | |
|---|
| 17 | open Integers |
|---|
| 18 | |
|---|
| 19 | open AST |
|---|
| 20 | |
|---|
| 21 | open Division |
|---|
| 22 | |
|---|
| 23 | open Arithmetic |
|---|
| 24 | |
|---|
| 25 | open Extranat |
|---|
| 26 | |
|---|
| 27 | open Vector |
|---|
| 28 | |
|---|
| 29 | open FoldStuff |
|---|
| 30 | |
|---|
| 31 | open BitVector |
|---|
| 32 | |
|---|
| 33 | open Z |
|---|
| 34 | |
|---|
| 35 | open BitVectorZ |
|---|
| 36 | |
|---|
| 37 | open Pointers |
|---|
| 38 | |
|---|
| 39 | open ErrorMessages |
|---|
| 40 | |
|---|
| 41 | open Option |
|---|
| 42 | |
|---|
| 43 | open Setoids |
|---|
| 44 | |
|---|
| 45 | open Monad |
|---|
| 46 | |
|---|
| 47 | open Positive |
|---|
| 48 | |
|---|
| 49 | open PreIdentifiers |
|---|
| 50 | |
|---|
| 51 | open Errors |
|---|
| 52 | |
|---|
| 53 | open Div_and_mod |
|---|
| 54 | |
|---|
| 55 | open Jmeq |
|---|
| 56 | |
|---|
| 57 | open Russell |
|---|
| 58 | |
|---|
| 59 | open Util |
|---|
| 60 | |
|---|
| 61 | open Bool |
|---|
| 62 | |
|---|
| 63 | open Relations |
|---|
| 64 | |
|---|
| 65 | open Nat |
|---|
| 66 | |
|---|
| 67 | open List |
|---|
| 68 | |
|---|
| 69 | open Hints_declaration |
|---|
| 70 | |
|---|
| 71 | open Core_notation |
|---|
| 72 | |
|---|
| 73 | open Pts |
|---|
| 74 | |
|---|
| 75 | open Logic |
|---|
| 76 | |
|---|
| 77 | open Types |
|---|
| 78 | |
|---|
| 79 | open Coqlib |
|---|
| 80 | |
|---|
| 81 | open Values |
|---|
| 82 | |
|---|
| 83 | open Events |
|---|
| 84 | |
|---|
| 85 | open FrontEndVal |
|---|
| 86 | |
|---|
| 87 | open Hide |
|---|
| 88 | |
|---|
| 89 | open ByteValues |
|---|
| 90 | |
|---|
| 91 | open GenMem |
|---|
| 92 | |
|---|
| 93 | open FrontEndMem |
|---|
| 94 | |
|---|
| 95 | open IOMonad |
|---|
| 96 | |
|---|
| 97 | open IO |
|---|
| 98 | |
|---|
| 99 | open Extra_bool |
|---|
| 100 | |
|---|
| 101 | open Globalenvs |
|---|
| 102 | |
|---|
| 103 | open SmallstepExec |
|---|
| 104 | |
|---|
| 105 | open FrontEndOps |
|---|
| 106 | |
|---|
| 107 | open Cminor_syntax |
|---|
| 108 | |
|---|
| 109 | type env = Values.val0 Identifiers.identifier_map |
|---|
| 110 | |
|---|
| 111 | type genv = Cminor_syntax.internal_function AST.fundef Globalenvs.genv_t |
|---|
| 112 | |
|---|
| 113 | type cont = |
|---|
| 114 | | Kend |
|---|
| 115 | | Kseq of Cminor_syntax.stmt * cont |
|---|
| 116 | | Kblock of cont |
|---|
| 117 | |
|---|
| 118 | val cont_rect_Type4 : |
|---|
| 119 | 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1) |
|---|
| 120 | -> cont -> 'a1 |
|---|
| 121 | |
|---|
| 122 | val cont_rect_Type3 : |
|---|
| 123 | 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1) |
|---|
| 124 | -> cont -> 'a1 |
|---|
| 125 | |
|---|
| 126 | val cont_rect_Type2 : |
|---|
| 127 | 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1) |
|---|
| 128 | -> cont -> 'a1 |
|---|
| 129 | |
|---|
| 130 | val cont_rect_Type1 : |
|---|
| 131 | 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1) |
|---|
| 132 | -> cont -> 'a1 |
|---|
| 133 | |
|---|
| 134 | val cont_rect_Type0 : |
|---|
| 135 | 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1) |
|---|
| 136 | -> cont -> 'a1 |
|---|
| 137 | |
|---|
| 138 | val cont_inv_rect_Type4 : |
|---|
| 139 | cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ -> |
|---|
| 140 | 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 |
|---|
| 141 | |
|---|
| 142 | val cont_inv_rect_Type3 : |
|---|
| 143 | cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ -> |
|---|
| 144 | 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 |
|---|
| 145 | |
|---|
| 146 | val cont_inv_rect_Type2 : |
|---|
| 147 | cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ -> |
|---|
| 148 | 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 |
|---|
| 149 | |
|---|
| 150 | val cont_inv_rect_Type1 : |
|---|
| 151 | cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ -> |
|---|
| 152 | 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 |
|---|
| 153 | |
|---|
| 154 | val cont_inv_rect_Type0 : |
|---|
| 155 | cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ -> |
|---|
| 156 | 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 |
|---|
| 157 | |
|---|
| 158 | val cont_discr : cont -> cont -> __ |
|---|
| 159 | |
|---|
| 160 | val cont_jmdiscr : cont -> cont -> __ |
|---|
| 161 | |
|---|
| 162 | type cont_inv = __ |
|---|
| 163 | |
|---|
| 164 | type stack = |
|---|
| 165 | | SStop |
|---|
| 166 | | Scall of (AST.ident, AST.typ) Types.prod Types.option |
|---|
| 167 | * Cminor_syntax.internal_function * Pointers.block * env * cont * |
|---|
| 168 | stack |
|---|
| 169 | |
|---|
| 170 | val stack_rect_Type4 : |
|---|
| 171 | 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option -> |
|---|
| 172 | Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ -> |
|---|
| 173 | cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 |
|---|
| 174 | |
|---|
| 175 | val stack_rect_Type3 : |
|---|
| 176 | 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option -> |
|---|
| 177 | Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ -> |
|---|
| 178 | cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 |
|---|
| 179 | |
|---|
| 180 | val stack_rect_Type2 : |
|---|
| 181 | 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option -> |
|---|
| 182 | Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ -> |
|---|
| 183 | cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 |
|---|
| 184 | |
|---|
| 185 | val stack_rect_Type1 : |
|---|
| 186 | 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option -> |
|---|
| 187 | Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ -> |
|---|
| 188 | cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 |
|---|
| 189 | |
|---|
| 190 | val stack_rect_Type0 : |
|---|
| 191 | 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option -> |
|---|
| 192 | Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ -> |
|---|
| 193 | cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 |
|---|
| 194 | |
|---|
| 195 | val stack_inv_rect_Type4 : |
|---|
| 196 | stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> |
|---|
| 197 | Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ -> |
|---|
| 198 | cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 |
|---|
| 199 | |
|---|
| 200 | val stack_inv_rect_Type3 : |
|---|
| 201 | stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> |
|---|
| 202 | Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ -> |
|---|
| 203 | cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 |
|---|
| 204 | |
|---|
| 205 | val stack_inv_rect_Type2 : |
|---|
| 206 | stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> |
|---|
| 207 | Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ -> |
|---|
| 208 | cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 |
|---|
| 209 | |
|---|
| 210 | val stack_inv_rect_Type1 : |
|---|
| 211 | stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> |
|---|
| 212 | Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ -> |
|---|
| 213 | cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 |
|---|
| 214 | |
|---|
| 215 | val stack_inv_rect_Type0 : |
|---|
| 216 | stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> |
|---|
| 217 | Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ -> |
|---|
| 218 | cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 |
|---|
| 219 | |
|---|
| 220 | val stack_jmdiscr : stack -> stack -> __ |
|---|
| 221 | |
|---|
| 222 | type state0 = |
|---|
| 223 | | State of Cminor_syntax.internal_function * Cminor_syntax.stmt * env |
|---|
| 224 | * GenMem.mem1 * Pointers.block * cont * stack |
|---|
| 225 | | Callstate of Cminor_syntax.internal_function AST.fundef |
|---|
| 226 | * Values.val0 List.list * GenMem.mem1 * stack |
|---|
| 227 | | Returnstate of Values.val0 Types.option * GenMem.mem1 * stack |
|---|
| 228 | | Finalstate of Integers.int |
|---|
| 229 | |
|---|
| 230 | val state_rect_Type4 : |
|---|
| 231 | (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __ |
|---|
| 232 | -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) -> |
|---|
| 233 | (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
|---|
| 234 | GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 -> |
|---|
| 235 | stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
|---|
| 236 | |
|---|
| 237 | val state_rect_Type5 : |
|---|
| 238 | (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __ |
|---|
| 239 | -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) -> |
|---|
| 240 | (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
|---|
| 241 | GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 -> |
|---|
| 242 | stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
|---|
| 243 | |
|---|
| 244 | val state_rect_Type3 : |
|---|
| 245 | (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __ |
|---|
| 246 | -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) -> |
|---|
| 247 | (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
|---|
| 248 | GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 -> |
|---|
| 249 | stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
|---|
| 250 | |
|---|
| 251 | val state_rect_Type2 : |
|---|
| 252 | (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __ |
|---|
| 253 | -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) -> |
|---|
| 254 | (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
|---|
| 255 | GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 -> |
|---|
| 256 | stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
|---|
| 257 | |
|---|
| 258 | val state_rect_Type1 : |
|---|
| 259 | (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __ |
|---|
| 260 | -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) -> |
|---|
| 261 | (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
|---|
| 262 | GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 -> |
|---|
| 263 | stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
|---|
| 264 | |
|---|
| 265 | val state_rect_Type0 : |
|---|
| 266 | (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __ |
|---|
| 267 | -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) -> |
|---|
| 268 | (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
|---|
| 269 | GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 -> |
|---|
| 270 | stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
|---|
| 271 | |
|---|
| 272 | val state_inv_rect_Type4 : |
|---|
| 273 | state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> |
|---|
| 274 | __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __ -> |
|---|
| 275 | 'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0 |
|---|
| 276 | List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0 |
|---|
| 277 | Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __ |
|---|
| 278 | -> 'a1) -> 'a1 |
|---|
| 279 | |
|---|
| 280 | val state_inv_rect_Type3 : |
|---|
| 281 | state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> |
|---|
| 282 | __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __ -> |
|---|
| 283 | 'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0 |
|---|
| 284 | List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0 |
|---|
| 285 | Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __ |
|---|
| 286 | -> 'a1) -> 'a1 |
|---|
| 287 | |
|---|
| 288 | val state_inv_rect_Type2 : |
|---|
| 289 | state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> |
|---|
| 290 | __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __ -> |
|---|
| 291 | 'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0 |
|---|
| 292 | List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0 |
|---|
| 293 | Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __ |
|---|
| 294 | -> 'a1) -> 'a1 |
|---|
| 295 | |
|---|
| 296 | val state_inv_rect_Type1 : |
|---|
| 297 | state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> |
|---|
| 298 | __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __ -> |
|---|
| 299 | 'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0 |
|---|
| 300 | List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0 |
|---|
| 301 | Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __ |
|---|
| 302 | -> 'a1) -> 'a1 |
|---|
| 303 | |
|---|
| 304 | val state_inv_rect_Type0 : |
|---|
| 305 | state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> |
|---|
| 306 | __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __ -> |
|---|
| 307 | 'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0 |
|---|
| 308 | List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0 |
|---|
| 309 | Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __ |
|---|
| 310 | -> 'a1) -> 'a1 |
|---|
| 311 | |
|---|
| 312 | val state_jmdiscr : state0 -> state0 -> __ |
|---|
| 313 | |
|---|
| 314 | val eval_expr : |
|---|
| 315 | genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block -> |
|---|
| 316 | GenMem.mem1 -> (Events.trace, Values.val0) Types.prod Errors.res |
|---|
| 317 | |
|---|
| 318 | val k_exit : |
|---|
| 319 | Nat.nat -> cont -> Cminor_syntax.internal_function -> env -> cont |
|---|
| 320 | Types.sig0 Errors.res |
|---|
| 321 | |
|---|
| 322 | val find_case : |
|---|
| 323 | AST.intsize -> AST.bvint -> (AST.bvint, 'a1) Types.prod List.list -> 'a1 -> |
|---|
| 324 | 'a1 |
|---|
| 325 | |
|---|
| 326 | val find_label : |
|---|
| 327 | PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont -> |
|---|
| 328 | Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont) |
|---|
| 329 | Types.prod Types.sig0 Types.option |
|---|
| 330 | |
|---|
| 331 | val find_label_always : |
|---|
| 332 | PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont -> |
|---|
| 333 | Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont) |
|---|
| 334 | Types.prod Types.sig0 |
|---|
| 335 | |
|---|
| 336 | val bind_params : |
|---|
| 337 | Values.val0 List.list -> (AST.ident, AST.typ) Types.prod List.list -> env |
|---|
| 338 | Types.sig0 Errors.res |
|---|
| 339 | |
|---|
| 340 | val init_locals : env -> (AST.ident, AST.typ) Types.prod List.list -> env |
|---|
| 341 | |
|---|
| 342 | val trace_map_inv : |
|---|
| 343 | ('a1 -> __ -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list |
|---|
| 344 | -> (Events.trace, 'a2 List.list) Types.prod Errors.res |
|---|
| 345 | |
|---|
| 346 | val eval_step : |
|---|
| 347 | genv -> state0 -> (IO.io_out, IO.io_in, (Events.trace, state0) Types.prod) |
|---|
| 348 | IOMonad.iO |
|---|
| 349 | |
|---|
| 350 | val is_final0 : state0 -> Integers.int Types.option |
|---|
| 351 | |
|---|
| 352 | val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system |
|---|
| 353 | |
|---|
| 354 | val make_global0 : Cminor_syntax.cminor_program -> genv |
|---|
| 355 | |
|---|
| 356 | val make_initial_state0 : Cminor_syntax.cminor_program -> state0 Errors.res |
|---|
| 357 | |
|---|
| 358 | val cminor_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec |
|---|
| 359 | |
|---|
| 360 | val make_noinit_global : Cminor_syntax.cminor_noinit_program -> genv |
|---|
| 361 | |
|---|
| 362 | val make_initial_noinit_state : |
|---|
| 363 | Cminor_syntax.cminor_noinit_program -> state0 Errors.res |
|---|
| 364 | |
|---|
| 365 | val cminor_noinit_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec |
|---|
| 366 | |
|---|
