extracted/frontend_misc.ml

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Coqlib
   6
   7 open Proper
   8
   9 open PositiveMap
  10
  11 open Deqsets
  12
  13 open ErrorMessages
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Extralib
  20
  21 open Lists
  22
  23 open Positive
  24
  25 open Identifiers
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Util
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Jmeq
  42
  43 open Russell
  44
  45 open List
  46
  47 open Setoids
  48
  49 open Monad
  50
  51 open Option
  52
  53 open Extranat
  54
  55 open Bool
  56
  57 open Relations
  58
  59 open Nat
  60
  61 open Integers
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Types
  72
  73 open AST
  74
  75 open Csyntax
  76
  77 open TypeComparison
  78
  79 open ClassifyOp
  80
  81 open Events
  82
  83 open Smallstep
  84
  85 open Extra_bool
  86
  87 open Values
  88
  89 open FrontEndVal
  90
  91 open Hide
  92
  93 open ByteValues
  94
  95 open Division
  96
  97 open Z
  98
  99 open BitVectorZ
 100
 101 open Pointers
 102
 103 open GenMem
 104
 105 open FrontEndMem
 106
 107 open Globalenvs
 108
 109 open Csem
 110
 111 open Star
 112
 113 open IOMonad
 114
 115 open IO
 116
 117 open Sets
 118
 119 open Listb
 120
 121 (** val typ_eq_dec : AST.typ -> AST.typ -> (__, __) Types.sum **)
 122 let typ_eq_dec t1 t2 =
 123   match t1 with
 124   | AST.ASTint (x, x0) ->
 125     (match t2 with
 126      | AST.ASTint (sz, sg) ->
 127        (fun sz' sg' ->
 128          match sz with
 129          | AST.I8 ->
 130            (match sz' with
 131             | AST.I8 ->
 132               AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I8, sg))
 133             | AST.I16 ->
 134               AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I8,
 135                 sg))
 136             | AST.I32 ->
 137               AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I8,
 138                 sg)))
 139          | AST.I16 ->
 140            (match sz' with
 141             | AST.I8 ->
 142               AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I16,
 143                 sg))
 144             | AST.I16 ->
 145               AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I16,
 146                 sg))
 147             | AST.I32 ->
 148               AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I16,
 149                 sg)))
 150          | AST.I32 ->
 151            (match sz' with
 152             | AST.I8 ->
 153               AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I32,
 154                 sg))
 155             | AST.I16 ->
 156               AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I32,
 157                 sg))
 158             | AST.I32 ->
 159               AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I32,
 160                 sg))))
 161      | AST.ASTptr -> (fun sz sg -> Types.Inr __)) x x0
 162   | AST.ASTptr ->
 163     (match t2 with
 164      | AST.ASTint (sz, sg) -> Types.Inr __
 165      | AST.ASTptr -> Types.Inl __)
 166
 167 (** val block_DeqSet : Deqsets.deqSet **)
 168 let block_DeqSet =
 169   Obj.magic Pointers.eq_block
 170
 171 (** val mem_assoc_env :
 172     AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool **)
 173 let rec mem_assoc_env i = function
 174 | List.Nil -> Bool.False
 175 | List.Cons (hd, tl) ->
 176   let { Types.fst = id; Types.snd = ty } = hd in
 177   (match Identifiers.identifier_eq PreIdentifiers.SymbolTag i id with
 178    | Types.Inl _ -> Bool.True
 179    | Types.Inr _ -> mem_assoc_env i tl)
 180
 181 type 'a lset = 'a List.list
 182
 183 (** val empty_lset : 'a1 List.list **)
 184 let empty_lset =
 185   List.Nil
 186
 187 (** val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list **)
 188 let lset_union l1 l2 =
 189   List.append l1 l2
 190
 191 (** val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list **)
 192 let lset_remove a l elt =
 193   List.filter (fun x -> Bool.notb (Deqsets.eqb a x elt)) l
 194
 195 (** val lset_difference :
 196     Deqsets.deqSet -> __ lset -> __ lset -> __ List.list **)
 197 let lset_difference a l1 l2 =
 198   List.filter (fun x -> Bool.notb (Listb.memb a x l2)) l1
 199
 200 (** val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2 **)
 201 let rec wF_rect f x =
 202   f x __ (fun y _ -> wF_rect f y)
 203
 204 (** val one_bv : Nat.nat -> BitVector.bitVector **)
 205 let one_bv n =
 206   (Arithmetic.add_with_carries n (BitVector.zero n) (BitVector.zero n)
 207     Bool.True).Types.fst
 208
 209 (** val ith_carry :
 210     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 211     Bool.bool **)
 212 let rec ith_carry n a b init =
 213   (match n with
 214    | Nat.O -> (fun x x0 -> init)
 215    | Nat.S x ->
 216      (fun a' b' ->
 217        let hd_a = Vector.head' x a' in
 218        let hd_b = Vector.head' x b' in
 219        let tl_a = Vector.tail x a' in
 220        let tl_b = Vector.tail x b' in
 221        Arithmetic.carry_of hd_a hd_b (ith_carry x tl_a tl_b init))) a b
 222
 223 (** val ith_bit :
 224     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 225     Bool.bool **)
 226 let ith_bit n a b init =
 227   (match n with
 228    | Nat.O -> (fun x x0 -> init)
 229    | Nat.S x ->
 230      (fun a' b' ->
 231        let hd_a = Vector.head' x a' in
 232        let hd_b = Vector.head' x b' in
 233        let tl_a = Vector.tail x a' in
 234        let tl_b = Vector.tail x b' in
 235        Bool.xorb (Bool.xorb hd_a hd_b) (ith_carry x tl_a tl_b init))) a b
 236
 237 (** val bitvector_fold :
 238     Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
 239     Bool.bool) -> BitVector.bitVector **)
 240 let rec bitvector_fold n v f =
 241   match v with
 242   | Vector.VEmpty -> Vector.VEmpty
 243   | Vector.VCons (sz, elt, tl) ->
 244     let bit = f n v in Vector.VCons (sz, bit, (bitvector_fold sz tl f))
 245
 246 (** val bitvector_fold2 :
 247     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
 248     BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
 249     BitVector.bitVector **)
 250 let rec bitvector_fold2 n v1 v2 f =
 251   (match v1 with
 252    | Vector.VEmpty -> (fun x -> Vector.VEmpty)
 253    | Vector.VCons (sz, elt, tl) ->
 254      (fun v2' ->
 255        let bit = f n v1 v2 in
 256        Vector.VCons (sz, bit, (bitvector_fold2 sz tl (Vector.tail sz v2') f))))
 257     v2
 258
 259 (** val addition_n_direct :
 260     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 261     BitVector.bitVector **)
 262 let addition_n_direct n v1 v2 init =
 263   bitvector_fold2 n v1 v2 (fun n0 v10 v20 -> ith_bit n0 v10 v20 init)
 264
 265 (** val increment_direct :
 266     Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
 267 let increment_direct n v =
 268   addition_n_direct n v (one_bv n) Bool.False
 269
 270 (** val twocomp_neg_direct :
 271     Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
 272 let twocomp_neg_direct n v =
 273   increment_direct n (BitVector.negation_bv n v)
 274
 275 (** val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool **)
 276 let rec andb_fold n = function
 277 | Vector.VEmpty -> Bool.True
 278 | Vector.VCons (sz, elt, tl) -> Bool.andb elt (andb_fold sz tl)
 279