open Preamble

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Coqlib

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Extranat

open Vector

open FoldStuff

open BitVector

open Z

open BitVectorZ

open Pointers

type val0 =
| Vundef
| Vint of AST.intsize * AST.bvint
| Vnull
| Vptr of Pointers.pointer

(** val val_rect_Type4 :
    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
    'a1) -> val0 -> 'a1 **)
let rec val_rect_Type4 h_Vundef h_Vint h_Vnull h_Vptr = function
| Vundef -> h_Vundef
| Vint (sz, x_5112) -> h_Vint sz x_5112
| Vnull -> h_Vnull
| Vptr x_5113 -> h_Vptr x_5113

(** val val_rect_Type5 :
    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
    'a1) -> val0 -> 'a1 **)
let rec val_rect_Type5 h_Vundef h_Vint h_Vnull h_Vptr = function
| Vundef -> h_Vundef
| Vint (sz, x_5119) -> h_Vint sz x_5119
| Vnull -> h_Vnull
| Vptr x_5120 -> h_Vptr x_5120

(** val val_rect_Type3 :
    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
    'a1) -> val0 -> 'a1 **)
let rec val_rect_Type3 h_Vundef h_Vint h_Vnull h_Vptr = function
| Vundef -> h_Vundef
| Vint (sz, x_5126) -> h_Vint sz x_5126
| Vnull -> h_Vnull
| Vptr x_5127 -> h_Vptr x_5127

(** val val_rect_Type2 :
    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
    'a1) -> val0 -> 'a1 **)
let rec val_rect_Type2 h_Vundef h_Vint h_Vnull h_Vptr = function
| Vundef -> h_Vundef
| Vint (sz, x_5133) -> h_Vint sz x_5133
| Vnull -> h_Vnull
| Vptr x_5134 -> h_Vptr x_5134

(** val val_rect_Type1 :
    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
    'a1) -> val0 -> 'a1 **)
let rec val_rect_Type1 h_Vundef h_Vint h_Vnull h_Vptr = function
| Vundef -> h_Vundef
| Vint (sz, x_5140) -> h_Vint sz x_5140
| Vnull -> h_Vnull
| Vptr x_5141 -> h_Vptr x_5141

(** val val_rect_Type0 :
    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
    'a1) -> val0 -> 'a1 **)
let rec val_rect_Type0 h_Vundef h_Vint h_Vnull h_Vptr = function
| Vundef -> h_Vundef
| Vint (sz, x_5147) -> h_Vint sz x_5147
| Vnull -> h_Vnull
| Vptr x_5148 -> h_Vptr x_5148

(** val val_inv_rect_Type4 :
    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
let val_inv_rect_Type4 hterm h1 h2 h3 h4 =
  let hcut = val_rect_Type4 h1 h2 h3 h4 hterm in hcut __

(** val val_inv_rect_Type3 :
    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
let val_inv_rect_Type3 hterm h1 h2 h3 h4 =
  let hcut = val_rect_Type3 h1 h2 h3 h4 hterm in hcut __

(** val val_inv_rect_Type2 :
    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
let val_inv_rect_Type2 hterm h1 h2 h3 h4 =
  let hcut = val_rect_Type2 h1 h2 h3 h4 hterm in hcut __

(** val val_inv_rect_Type1 :
    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
let val_inv_rect_Type1 hterm h1 h2 h3 h4 =
  let hcut = val_rect_Type1 h1 h2 h3 h4 hterm in hcut __

(** val val_inv_rect_Type0 :
    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
let val_inv_rect_Type0 hterm h1 h2 h3 h4 =
  let hcut = val_rect_Type0 h1 h2 h3 h4 hterm in hcut __

(** val val_discr : val0 -> val0 -> __ **)
let val_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Vundef -> Obj.magic (fun _ dH -> dH)
     | Vint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Vnull -> Obj.magic (fun _ dH -> dH)
     | Vptr a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val val_jmdiscr : val0 -> val0 -> __ **)
let val_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Vundef -> Obj.magic (fun _ dH -> dH)
     | Vint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Vnull -> Obj.magic (fun _ dH -> dH)
     | Vptr a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val vzero : AST.intsize -> val0 **)
let vzero sz =
  Vint (sz, (BitVector.zero (AST.bitsize_of_intsize sz)))

(** val vone : AST.intsize -> val0 **)
let vone sz =
  Vint (sz, (AST.repr sz (Nat.S Nat.O)))

(** val mone : AST.intsize -> BitVector.bitVector **)
let mone sz =
  BitVectorZ.bitvector_of_Z (AST.bitsize_of_intsize sz) (Z.Neg Positive.One)

(** val vmone : AST.intsize -> val0 **)
let vmone sz =
  Vint (sz, (mone sz))

(** val vtrue : val0 **)
let vtrue =
  vone AST.I32

(** val vfalse : val0 **)
let vfalse =
  vzero AST.I32

(** val of_bool : Bool.bool -> val0 **)
let of_bool = function
| Bool.True -> vtrue
| Bool.False -> vfalse

(** val eval_bool_of_val : val0 -> Bool.bool Errors.res **)
let eval_bool_of_val = function
| Vundef -> Errors.Error (Errors.msg ErrorMessages.ValueNotABoolean)
| Vint (x, i) ->
  Errors.OK
    (Bool.notb
      (BitVector.eq_bv (AST.bitsize_of_intsize x) i
        (BitVector.zero (AST.bitsize_of_intsize x))))
| Vnull -> Errors.OK Bool.False
| Vptr x -> Errors.OK Bool.True

(** val neg : val0 -> val0 **)
let neg = function
| Vundef -> Vundef
| Vint (sz, n) ->
  Vint (sz,
    (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz) n))
| Vnull -> Vundef
| Vptr x -> Vundef

(** val notint : val0 -> val0 **)
let notint = function
| Vundef -> Vundef
| Vint (sz, n) ->
  Vint (sz,
    (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz) n
      (mone sz)))
| Vnull -> Vundef
| Vptr x -> Vundef

(** val notbool : val0 -> val0 **)
let notbool = function
| Vundef -> Vundef
| Vint (sz, n) ->
  of_bool
    (BitVector.eq_bv (AST.bitsize_of_intsize sz) n
      (BitVector.zero (AST.bitsize_of_intsize sz)))
| Vnull -> vtrue
| Vptr x -> vfalse

(** val zero_ext : AST.intsize -> val0 -> val0 **)
let zero_ext rsz = function
| Vundef -> Vundef
| Vint (sz, n) ->
  Vint (rsz,
    (Arithmetic.zero_ext (AST.bitsize_of_intsize sz)
      (AST.bitsize_of_intsize rsz) n))
| Vnull -> Vundef
| Vptr x -> Vundef

(** val sign_ext : AST.intsize -> val0 -> val0 **)
let sign_ext rsz = function
| Vundef -> Vundef
| Vint (sz, i) ->
  Vint (rsz,
    (Arithmetic.sign_ext (AST.bitsize_of_intsize sz)
      (AST.bitsize_of_intsize rsz) i))
| Vnull -> Vundef
| Vptr x -> Vundef

(** val add : val0 -> val0 -> val0 **)
let add v1 v2 =
  match v1 with
  | Vundef -> Vundef
  | Vint (sz1, n1) ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
         (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))) Vundef
     | Vnull -> Vundef
     | Vptr ptr ->
       Vptr (Pointers.shift_pointer (AST.bitsize_of_intsize sz1) ptr n1))
  | Vnull -> Vundef
  | Vptr ptr ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (x, n2) ->
       Vptr (Pointers.shift_pointer (AST.bitsize_of_intsize x) ptr n2)
     | Vnull -> Vundef
     | Vptr x -> Vundef)

(** val sub : val0 -> val0 -> val0 **)
let sub v1 v2 =
  match v1 with
  | Vundef -> Vundef
  | Vint (sz1, n1) ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
         (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2)))
         Vundef
     | Vnull -> Vundef
     | Vptr x -> Vundef)
  | Vnull ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (x, x0) -> Vundef
     | Vnull -> vzero AST.I32
     | Vptr x -> Vundef)
  | Vptr ptr1 ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (sz2, n2) ->
       Vptr (Pointers.neg_shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2)
     | Vnull -> Vundef
     | Vptr ptr2 ->
       (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
        | Bool.True ->
          Vint (AST.I32,
            (Pointers.sub_offset (AST.bitsize_of_intsize AST.I32)
              ptr1.Pointers.poff ptr2.Pointers.poff))
        | Bool.False -> Vundef))

(** val mul : val0 -> val0 -> val0 **)
let mul v1 v2 =
  match v1 with
  | Vundef -> Vundef
  | Vint (sz1, n1) ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
         (Vector.vsplit (AST.bitsize_of_intsize sz2)
           (AST.bitsize_of_intsize sz2)
           (Arithmetic.multiplication (AST.bitsize_of_intsize sz2) n10 n2)).Types.snd))
         Vundef
     | Vnull -> Vundef
     | Vptr x -> Vundef)
  | Vnull -> Vundef
  | Vptr x -> Vundef

(** val v_and : val0 -> val0 -> val0 **)
let v_and v1 v2 =
  match v1 with
  | Vundef -> Vundef
  | Vint (sz1, n1) ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
         (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2)))
         Vundef
     | Vnull -> Vundef
     | Vptr x -> Vundef)
  | Vnull -> Vundef
  | Vptr x -> Vundef

(** val or0 : val0 -> val0 -> val0 **)
let or0 v1 v2 =
  match v1 with
  | Vundef -> Vundef
  | Vint (sz1, n1) ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
         (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
           n2))) Vundef
     | Vnull -> Vundef
     | Vptr x -> Vundef)
  | Vnull -> Vundef
  | Vptr x -> Vundef

(** val xor : val0 -> val0 -> val0 **)
let xor v1 v2 =
  match v1 with
  | Vundef -> Vundef
  | Vint (sz1, n1) ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
           n2))) Vundef
     | Vnull -> Vundef
     | Vptr x -> Vundef)
  | Vnull -> Vundef
  | Vptr x -> Vundef

(** val cmp_match : Integers.comparison -> val0 **)
let cmp_match = function
| Integers.Ceq -> vtrue
| Integers.Cne -> vfalse
| Integers.Clt -> Vundef
| Integers.Cle -> Vundef
| Integers.Cgt -> Vundef
| Integers.Cge -> Vundef

(** val cmp_mismatch : Integers.comparison -> val0 **)
let cmp_mismatch = function
| Integers.Ceq -> vfalse
| Integers.Cne -> vtrue
| Integers.Clt -> Vundef
| Integers.Cle -> Vundef
| Integers.Cgt -> Vundef
| Integers.Cge -> Vundef

(** val cmp_offset :
    Integers.comparison -> Pointers.offset -> Pointers.offset -> Bool.bool **)
let cmp_offset c x y =
  match c with
  | Integers.Ceq -> Pointers.eq_offset x y
  | Integers.Cne -> Bool.notb (Pointers.eq_offset x y)
  | Integers.Clt -> Pointers.lt_offset x y
  | Integers.Cle -> Bool.notb (Pointers.lt_offset y x)
  | Integers.Cgt -> Pointers.lt_offset y x
  | Integers.Cge -> Bool.notb (Pointers.lt_offset x y)

(** val cmp_int :
    Nat.nat -> Integers.comparison -> BitVector.bitVector ->
    BitVector.bitVector -> Bool.bool **)
let cmp_int n c x y =
  match c with
  | Integers.Ceq -> BitVector.eq_bv n x y
  | Integers.Cne -> Bool.notb (BitVector.eq_bv n x y)
  | Integers.Clt -> Arithmetic.lt_s n x y
  | Integers.Cle -> Bool.notb (Arithmetic.lt_s n y x)
  | Integers.Cgt -> Arithmetic.lt_s n y x
  | Integers.Cge -> Bool.notb (Arithmetic.lt_s n x y)

(** val cmpu_int :
    Nat.nat -> Integers.comparison -> BitVector.bitVector ->
    BitVector.bitVector -> Bool.bool **)
let cmpu_int n c x y =
  match c with
  | Integers.Ceq -> BitVector.eq_bv n x y
  | Integers.Cne -> Bool.notb (BitVector.eq_bv n x y)
  | Integers.Clt -> Arithmetic.lt_u n x y
  | Integers.Cle -> Bool.notb (Arithmetic.lt_u n y x)
  | Integers.Cgt -> Arithmetic.lt_u n y x
  | Integers.Cge -> Bool.notb (Arithmetic.lt_u n x y)

(** val cmp : Integers.comparison -> val0 -> val0 -> val0 **)
let cmp c v1 v2 =
  match v1 with
  | Vundef -> Vundef
  | Vint (sz1, n1) ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
         of_bool (cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)) Vundef
     | Vnull -> Vundef
     | Vptr x -> Vundef)
  | Vnull ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (x, x0) -> Vundef
     | Vnull -> cmp_match c
     | Vptr x -> cmp_mismatch c)
  | Vptr ptr1 ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (x, x0) -> Vundef
     | Vnull -> cmp_mismatch c
     | Vptr ptr2 ->
       (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
        | Bool.True ->
          of_bool (cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff)
        | Bool.False -> cmp_mismatch c))

(** val cmpu : Integers.comparison -> val0 -> val0 -> val0 **)
let cmpu c v1 v2 =
  match v1 with
  | Vundef -> Vundef
  | Vint (sz1, n1) ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
         of_bool (cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)) Vundef
     | Vnull -> Vundef
     | Vptr x -> Vundef)
  | Vnull ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (x, x0) -> Vundef
     | Vnull -> cmp_match c
     | Vptr x -> cmp_mismatch c)
  | Vptr ptr1 ->
    (match v2 with
     | Vundef -> Vundef
     | Vint (x, x0) -> Vundef
     | Vnull -> cmp_mismatch c
     | Vptr ptr2 ->
       (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
        | Bool.True ->
          of_bool (cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff)
        | Bool.False -> cmp_mismatch c))

(** val load_result : AST.typ -> val0 -> val0 **)
let rec load_result chunk v = match v with
| Vundef -> Vundef
| Vint (sz, n) ->
  (match chunk with
   | AST.ASTint (sz', sg) ->
     (match AST.eq_intsize sz sz' with
      | Bool.True -> v
      | Bool.False -> Vundef)
   | AST.ASTptr -> Vundef)
| Vnull ->
  (match chunk with
   | AST.ASTint (x, x0) -> Vundef
   | AST.ASTptr -> Vnull)
| Vptr ptr ->
  (match chunk with
   | AST.ASTint (x, x0) -> Vundef
   | AST.ASTptr -> Vptr ptr)