extracted/values.ml

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Util
  10
  11 open Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open List
  18
  19 open Hints_declaration
  20
  21 open Core_notation
  22
  23 open Pts
  24
  25 open Logic
  26
  27 open Types
  28
  29 open Coqlib
  30
  31 open ErrorMessages
  32
  33 open Option
  34
  35 open Setoids
  36
  37 open Monad
  38
  39 open Positive
  40
  41 open PreIdentifiers
  42
  43 open Errors
  44
  45 open Proper
  46
  47 open PositiveMap
  48
  49 open Deqsets
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Extranat
  68
  69 open Vector
  70
  71 open FoldStuff
  72
  73 open BitVector
  74
  75 open Z
  76
  77 open BitVectorZ
  78
  79 open Pointers
  80
  81 type val0 =
  82 | Vundef
  83 | Vint of AST.intsize * AST.bvint
  84 | Vnull
  85 | Vptr of Pointers.pointer
  86
  87 (** val val_rect_Type4 :
  88     'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
  89     'a1) -> val0 -> 'a1 **)
  90 let rec val_rect_Type4 h_Vundef h_Vint h_Vnull h_Vptr = function
  91 | Vundef -> h_Vundef
  92 | Vint (sz, x_5112) -> h_Vint sz x_5112
  93 | Vnull -> h_Vnull
  94 | Vptr x_5113 -> h_Vptr x_5113
  95
  96 (** val val_rect_Type5 :
  97     'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
  98     'a1) -> val0 -> 'a1 **)
  99 let rec val_rect_Type5 h_Vundef h_Vint h_Vnull h_Vptr = function
 100 | Vundef -> h_Vundef
 101 | Vint (sz, x_5119) -> h_Vint sz x_5119
 102 | Vnull -> h_Vnull
 103 | Vptr x_5120 -> h_Vptr x_5120
 104
 105 (** val val_rect_Type3 :
 106     'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
 107     'a1) -> val0 -> 'a1 **)
 108 let rec val_rect_Type3 h_Vundef h_Vint h_Vnull h_Vptr = function
 109 | Vundef -> h_Vundef
 110 | Vint (sz, x_5126) -> h_Vint sz x_5126
 111 | Vnull -> h_Vnull
 112 | Vptr x_5127 -> h_Vptr x_5127
 113
 114 (** val val_rect_Type2 :
 115     'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
 116     'a1) -> val0 -> 'a1 **)
 117 let rec val_rect_Type2 h_Vundef h_Vint h_Vnull h_Vptr = function
 118 | Vundef -> h_Vundef
 119 | Vint (sz, x_5133) -> h_Vint sz x_5133
 120 | Vnull -> h_Vnull
 121 | Vptr x_5134 -> h_Vptr x_5134
 122
 123 (** val val_rect_Type1 :
 124     'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
 125     'a1) -> val0 -> 'a1 **)
 126 let rec val_rect_Type1 h_Vundef h_Vint h_Vnull h_Vptr = function
 127 | Vundef -> h_Vundef
 128 | Vint (sz, x_5140) -> h_Vint sz x_5140
 129 | Vnull -> h_Vnull
 130 | Vptr x_5141 -> h_Vptr x_5141
 131
 132 (** val val_rect_Type0 :
 133     'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
 134     'a1) -> val0 -> 'a1 **)
 135 let rec val_rect_Type0 h_Vundef h_Vint h_Vnull h_Vptr = function
 136 | Vundef -> h_Vundef
 137 | Vint (sz, x_5147) -> h_Vint sz x_5147
 138 | Vnull -> h_Vnull
 139 | Vptr x_5148 -> h_Vptr x_5148
 140
 141 (** val val_inv_rect_Type4 :
 142     val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
 143     'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
 144 let val_inv_rect_Type4 hterm h1 h2 h3 h4 =
 145   let hcut = val_rect_Type4 h1 h2 h3 h4 hterm in hcut __
 146
 147 (** val val_inv_rect_Type3 :
 148     val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
 149     'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
 150 let val_inv_rect_Type3 hterm h1 h2 h3 h4 =
 151   let hcut = val_rect_Type3 h1 h2 h3 h4 hterm in hcut __
 152
 153 (** val val_inv_rect_Type2 :
 154     val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
 155     'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
 156 let val_inv_rect_Type2 hterm h1 h2 h3 h4 =
 157   let hcut = val_rect_Type2 h1 h2 h3 h4 hterm in hcut __
 158
 159 (** val val_inv_rect_Type1 :
 160     val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
 161     'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
 162 let val_inv_rect_Type1 hterm h1 h2 h3 h4 =
 163   let hcut = val_rect_Type1 h1 h2 h3 h4 hterm in hcut __
 164
 165 (** val val_inv_rect_Type0 :
 166     val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
 167     'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
 168 let val_inv_rect_Type0 hterm h1 h2 h3 h4 =
 169   let hcut = val_rect_Type0 h1 h2 h3 h4 hterm in hcut __
 170
 171 (** val val_discr : val0 -> val0 -> __ **)
 172 let val_discr x y =
 173   Logic.eq_rect_Type2 x
 174     (match x with
 175      | Vundef -> Obj.magic (fun _ dH -> dH)
 176      | Vint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 177      | Vnull -> Obj.magic (fun _ dH -> dH)
 178      | Vptr a0 -> Obj.magic (fun _ dH -> dH __)) y
 179
 180 (** val val_jmdiscr : val0 -> val0 -> __ **)
 181 let val_jmdiscr x y =
 182   Logic.eq_rect_Type2 x
 183     (match x with
 184      | Vundef -> Obj.magic (fun _ dH -> dH)
 185      | Vint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 186      | Vnull -> Obj.magic (fun _ dH -> dH)
 187      | Vptr a0 -> Obj.magic (fun _ dH -> dH __)) y
 188
 189 (** val vzero : AST.intsize -> val0 **)
 190 let vzero sz =
 191   Vint (sz, (BitVector.zero (AST.bitsize_of_intsize sz)))
 192
 193 (** val vone : AST.intsize -> val0 **)
 194 let vone sz =
 195   Vint (sz, (AST.repr sz (Nat.S Nat.O)))
 196
 197 (** val mone : AST.intsize -> BitVector.bitVector **)
 198 let mone sz =
 199   BitVectorZ.bitvector_of_Z (AST.bitsize_of_intsize sz) (Z.Neg Positive.One)
 200
 201 (** val vmone : AST.intsize -> val0 **)
 202 let vmone sz =
 203   Vint (sz, (mone sz))
 204
 205 (** val vtrue : val0 **)
 206 let vtrue =
 207   vone AST.I32
 208
 209 (** val vfalse : val0 **)
 210 let vfalse =
 211   vzero AST.I32
 212
 213 (** val of_bool : Bool.bool -> val0 **)
 214 let of_bool = function
 215 | Bool.True -> vtrue
 216 | Bool.False -> vfalse
 217
 218 (** val eval_bool_of_val : val0 -> Bool.bool Errors.res **)
 219 let eval_bool_of_val = function
 220 | Vundef -> Errors.Error (Errors.msg ErrorMessages.ValueNotABoolean)
 221 | Vint (x, i) ->
 222   Errors.OK
 223     (Bool.notb
 224       (BitVector.eq_bv (AST.bitsize_of_intsize x) i
 225         (BitVector.zero (AST.bitsize_of_intsize x))))
 226 | Vnull -> Errors.OK Bool.False
 227 | Vptr x -> Errors.OK Bool.True
 228
 229 (** val neg : val0 -> val0 **)
 230 let neg = function
 231 | Vundef -> Vundef
 232 | Vint (sz, n) ->
 233   Vint (sz,
 234     (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz) n))
 235 | Vnull -> Vundef
 236 | Vptr x -> Vundef
 237
 238 (** val notint : val0 -> val0 **)
 239 let notint = function
 240 | Vundef -> Vundef
 241 | Vint (sz, n) ->
 242   Vint (sz,
 243     (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz) n
 244       (mone sz)))
 245 | Vnull -> Vundef
 246 | Vptr x -> Vundef
 247
 248 (** val notbool : val0 -> val0 **)
 249 let notbool = function
 250 | Vundef -> Vundef
 251 | Vint (sz, n) ->
 252   of_bool
 253     (BitVector.eq_bv (AST.bitsize_of_intsize sz) n
 254       (BitVector.zero (AST.bitsize_of_intsize sz)))
 255 | Vnull -> vtrue
 256 | Vptr x -> vfalse
 257
 258 (** val zero_ext : AST.intsize -> val0 -> val0 **)
 259 let zero_ext rsz = function
 260 | Vundef -> Vundef
 261 | Vint (sz, n) ->
 262   Vint (rsz,
 263     (Arithmetic.zero_ext (AST.bitsize_of_intsize sz)
 264       (AST.bitsize_of_intsize rsz) n))
 265 | Vnull -> Vundef
 266 | Vptr x -> Vundef
 267
 268 (** val sign_ext : AST.intsize -> val0 -> val0 **)
 269 let sign_ext rsz = function
 270 | Vundef -> Vundef
 271 | Vint (sz, i) ->
 272   Vint (rsz,
 273     (Arithmetic.sign_ext (AST.bitsize_of_intsize sz)
 274       (AST.bitsize_of_intsize rsz) i))
 275 | Vnull -> Vundef
 276 | Vptr x -> Vundef
 277
 278 (** val add : val0 -> val0 -> val0 **)
 279 let add v1 v2 =
 280   match v1 with
 281   | Vundef -> Vundef
 282   | Vint (sz1, n1) ->
 283     (match v2 with
 284      | Vundef -> Vundef
 285      | Vint (sz2, n2) ->
 286        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
 287          (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))) Vundef
 288      | Vnull -> Vundef
 289      | Vptr ptr ->
 290        Vptr (Pointers.shift_pointer (AST.bitsize_of_intsize sz1) ptr n1))
 291   | Vnull -> Vundef
 292   | Vptr ptr ->
 293     (match v2 with
 294      | Vundef -> Vundef
 295      | Vint (x, n2) ->
 296        Vptr (Pointers.shift_pointer (AST.bitsize_of_intsize x) ptr n2)
 297      | Vnull -> Vundef
 298      | Vptr x -> Vundef)
 299
 300 (** val sub : val0 -> val0 -> val0 **)
 301 let sub v1 v2 =
 302   match v1 with
 303   | Vundef -> Vundef
 304   | Vint (sz1, n1) ->
 305     (match v2 with
 306      | Vundef -> Vundef
 307      | Vint (sz2, n2) ->
 308        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
 309          (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2)))
 310          Vundef
 311      | Vnull -> Vundef
 312      | Vptr x -> Vundef)
 313   | Vnull ->
 314     (match v2 with
 315      | Vundef -> Vundef
 316      | Vint (x, x0) -> Vundef
 317      | Vnull -> vzero AST.I32
 318      | Vptr x -> Vundef)
 319   | Vptr ptr1 ->
 320     (match v2 with
 321      | Vundef -> Vundef
 322      | Vint (sz2, n2) ->
 323        Vptr (Pointers.neg_shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2)
 324      | Vnull -> Vundef
 325      | Vptr ptr2 ->
 326        (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
 327         | Bool.True ->
 328           Vint (AST.I32,
 329             (Pointers.sub_offset (AST.bitsize_of_intsize AST.I32)
 330               ptr1.Pointers.poff ptr2.Pointers.poff))
 331         | Bool.False -> Vundef))
 332
 333 (** val mul : val0 -> val0 -> val0 **)
 334 let mul v1 v2 =
 335   match v1 with
 336   | Vundef -> Vundef
 337   | Vint (sz1, n1) ->
 338     (match v2 with
 339      | Vundef -> Vundef
 340      | Vint (sz2, n2) ->
 341        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
 342          (Vector.vsplit (AST.bitsize_of_intsize sz2)
 343            (AST.bitsize_of_intsize sz2)
 344            (Arithmetic.multiplication (AST.bitsize_of_intsize sz2) n10 n2)).Types.snd))
 345          Vundef
 346      | Vnull -> Vundef
 347      | Vptr x -> Vundef)
 348   | Vnull -> Vundef
 349   | Vptr x -> Vundef
 350
 351 (** val v_and : val0 -> val0 -> val0 **)
 352 let v_and v1 v2 =
 353   match v1 with
 354   | Vundef -> Vundef
 355   | Vint (sz1, n1) ->
 356     (match v2 with
 357      | Vundef -> Vundef
 358      | Vint (sz2, n2) ->
 359        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
 360          (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2)))
 361          Vundef
 362      | Vnull -> Vundef
 363      | Vptr x -> Vundef)
 364   | Vnull -> Vundef
 365   | Vptr x -> Vundef
 366
 367 (** val or0 : val0 -> val0 -> val0 **)
 368 let or0 v1 v2 =
 369   match v1 with
 370   | Vundef -> Vundef
 371   | Vint (sz1, n1) ->
 372     (match v2 with
 373      | Vundef -> Vundef
 374      | Vint (sz2, n2) ->
 375        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
 376          (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
 377            n2))) Vundef
 378      | Vnull -> Vundef
 379      | Vptr x -> Vundef)
 380   | Vnull -> Vundef
 381   | Vptr x -> Vundef
 382
 383 (** val xor : val0 -> val0 -> val0 **)
 384 let xor v1 v2 =
 385   match v1 with
 386   | Vundef -> Vundef
 387   | Vint (sz1, n1) ->
 388     (match v2 with
 389      | Vundef -> Vundef
 390      | Vint (sz2, n2) ->
 391        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
 392          (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
 393            n2))) Vundef
 394      | Vnull -> Vundef
 395      | Vptr x -> Vundef)
 396   | Vnull -> Vundef
 397   | Vptr x -> Vundef
 398
 399 (** val cmp_match : Integers.comparison -> val0 **)
 400 let cmp_match = function
 401 | Integers.Ceq -> vtrue
 402 | Integers.Cne -> vfalse
 403 | Integers.Clt -> Vundef
 404 | Integers.Cle -> Vundef
 405 | Integers.Cgt -> Vundef
 406 | Integers.Cge -> Vundef
 407
 408 (** val cmp_mismatch : Integers.comparison -> val0 **)
 409 let cmp_mismatch = function
 410 | Integers.Ceq -> vfalse
 411 | Integers.Cne -> vtrue
 412 | Integers.Clt -> Vundef
 413 | Integers.Cle -> Vundef
 414 | Integers.Cgt -> Vundef
 415 | Integers.Cge -> Vundef
 416
 417 (** val cmp_offset :
 418     Integers.comparison -> Pointers.offset -> Pointers.offset -> Bool.bool **)
 419 let cmp_offset c x y =
 420   match c with
 421   | Integers.Ceq -> Pointers.eq_offset x y
 422   | Integers.Cne -> Bool.notb (Pointers.eq_offset x y)
 423   | Integers.Clt -> Pointers.lt_offset x y
 424   | Integers.Cle -> Bool.notb (Pointers.lt_offset y x)
 425   | Integers.Cgt -> Pointers.lt_offset y x
 426   | Integers.Cge -> Bool.notb (Pointers.lt_offset x y)
 427
 428 (** val cmp_int :
 429     Nat.nat -> Integers.comparison -> BitVector.bitVector ->
 430     BitVector.bitVector -> Bool.bool **)
 431 let cmp_int n c x y =
 432   match c with
 433   | Integers.Ceq -> BitVector.eq_bv n x y
 434   | Integers.Cne -> Bool.notb (BitVector.eq_bv n x y)
 435   | Integers.Clt -> Arithmetic.lt_s n x y
 436   | Integers.Cle -> Bool.notb (Arithmetic.lt_s n y x)
 437   | Integers.Cgt -> Arithmetic.lt_s n y x
 438   | Integers.Cge -> Bool.notb (Arithmetic.lt_s n x y)
 439
 440 (** val cmpu_int :
 441     Nat.nat -> Integers.comparison -> BitVector.bitVector ->
 442     BitVector.bitVector -> Bool.bool **)
 443 let cmpu_int n c x y =
 444   match c with
 445   | Integers.Ceq -> BitVector.eq_bv n x y
 446   | Integers.Cne -> Bool.notb (BitVector.eq_bv n x y)
 447   | Integers.Clt -> Arithmetic.lt_u n x y
 448   | Integers.Cle -> Bool.notb (Arithmetic.lt_u n y x)
 449   | Integers.Cgt -> Arithmetic.lt_u n y x
 450   | Integers.Cge -> Bool.notb (Arithmetic.lt_u n x y)
 451
 452 (** val cmp : Integers.comparison -> val0 -> val0 -> val0 **)
 453 let cmp c v1 v2 =
 454   match v1 with
 455   | Vundef -> Vundef
 456   | Vint (sz1, n1) ->
 457     (match v2 with
 458      | Vundef -> Vundef
 459      | Vint (sz2, n2) ->
 460        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
 461          of_bool (cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)) Vundef
 462      | Vnull -> Vundef
 463      | Vptr x -> Vundef)
 464   | Vnull ->
 465     (match v2 with
 466      | Vundef -> Vundef
 467      | Vint (x, x0) -> Vundef
 468      | Vnull -> cmp_match c
 469      | Vptr x -> cmp_mismatch c)
 470   | Vptr ptr1 ->
 471     (match v2 with
 472      | Vundef -> Vundef
 473      | Vint (x, x0) -> Vundef
 474      | Vnull -> cmp_mismatch c
 475      | Vptr ptr2 ->
 476        (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
 477         | Bool.True ->
 478           of_bool (cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff)
 479         | Bool.False -> cmp_mismatch c))
 480
 481 (** val cmpu : Integers.comparison -> val0 -> val0 -> val0 **)
 482 let cmpu c v1 v2 =
 483   match v1 with
 484   | Vundef -> Vundef
 485   | Vint (sz1, n1) ->
 486     (match v2 with
 487      | Vundef -> Vundef
 488      | Vint (sz2, n2) ->
 489        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
 490          of_bool (cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)) Vundef
 491      | Vnull -> Vundef
 492      | Vptr x -> Vundef)
 493   | Vnull ->
 494     (match v2 with
 495      | Vundef -> Vundef
 496      | Vint (x, x0) -> Vundef
 497      | Vnull -> cmp_match c
 498      | Vptr x -> cmp_mismatch c)
 499   | Vptr ptr1 ->
 500     (match v2 with
 501      | Vundef -> Vundef
 502      | Vint (x, x0) -> Vundef
 503      | Vnull -> cmp_mismatch c
 504      | Vptr ptr2 ->
 505        (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
 506         | Bool.True ->
 507           of_bool (cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff)
 508         | Bool.False -> cmp_mismatch c))
 509
 510 (** val load_result : AST.typ -> val0 -> val0 **)
 511 let rec load_result chunk v = match v with
 512 | Vundef -> Vundef
 513 | Vint (sz, n) ->
 514   (match chunk with
 515    | AST.ASTint (sz', sg) ->
 516      (match AST.eq_intsize sz sz' with
 517       | Bool.True -> v
 518       | Bool.False -> Vundef)
 519    | AST.ASTptr -> Vundef)
 520 | Vnull ->
 521   (match chunk with
 522    | AST.ASTint (x, x0) -> Vundef
 523    | AST.ASTptr -> Vnull)
 524 | Vptr ptr ->
 525   (match chunk with
 526    | AST.ASTint (x, x0) -> Vundef
 527    | AST.ASTptr -> Vptr ptr)
 528