extracted/frontEndVal.ml

   1 open Preamble
   2
   3 open Proper
   4
   5 open PositiveMap
   6
   7 open Deqsets
   8
   9 open Extralib
  10
  11 open Lists
  12
  13 open Identifiers
  14
  15 open Integers
  16
  17 open AST
  18
  19 open Division
  20
  21 open Exp
  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 Hide
  84
  85 open ByteValues
  86
  87 (** val make_parts : ByteValues.part List.list **)
  88 let make_parts =
  89   List.map ByteValues.part_from_sig (Lists.range_strong AST.size_pointer)
  90
  91 (** val make_be_null : ByteValues.beval List.list **)
  92 let make_be_null =
  93   List.map (fun p -> ByteValues.BVnull p) make_parts
  94
  95 (** val bytes_of_bitvector :
  96     Nat.nat -> BitVector.bitVector -> BitVector.byte List.list **)
  97 let rec bytes_of_bitvector n v =
  98   (match n with
  99    | Nat.O -> (fun x -> List.Nil)
 100    | Nat.S m ->
 101      (fun v0 ->
 102        let { Types.fst = h; Types.snd = t } =
 103          Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 104            (Nat.S Nat.O))))))))
 105            (Nat.times m (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 106              (Nat.S Nat.O))))))))) v0
 107        in
 108        List.Cons (h, (bytes_of_bitvector m t)))) v
 109
 110 (** val fe_to_be_values :
 111     AST.typ -> Values.val0 -> ByteValues.beval List.list **)
 112 let fe_to_be_values t = function
 113 | Values.Vundef -> List.make_list ByteValues.BVundef (AST.typesize t)
 114 | Values.Vint (sz, i) ->
 115   List.map (fun b -> ByteValues.BVByte b)
 116     (bytes_of_bitvector (AST.size_intsize sz) i)
 117 | Values.Vnull -> make_be_null
 118 | Values.Vptr ptr -> ByteValues.bevals_of_pointer ptr
 119
 120 (** val check_be_null :
 121     Nat.nat -> ByteValues.beval List.list -> Bool.bool **)
 122 let rec check_be_null n = function
 123 | List.Nil -> Nat.eqb AST.size_pointer n
 124 | List.Cons (hd, tl) ->
 125   (match hd with
 126    | ByteValues.BVundef -> Bool.False
 127    | ByteValues.BVnonzero -> Bool.False
 128    | ByteValues.BVXor (x, x0, x1) -> Bool.False
 129    | ByteValues.BVByte x -> Bool.False
 130    | ByteValues.BVnull pt ->
 131      Bool.andb (Nat.eqb (ByteValues.part_no pt) n)
 132        (check_be_null (Nat.S n) tl)
 133    | ByteValues.BVptr (x, x0) -> Bool.False
 134    | ByteValues.BVpc (x, x0) -> Bool.False)
 135
 136 (** val build_integer :
 137     Nat.nat -> ByteValues.beval List.list -> BitVector.bitVector Types.option **)
 138 let rec build_integer n l =
 139   match n with
 140   | Nat.O ->
 141     (match l with
 142      | List.Nil -> Types.Some Vector.VEmpty
 143      | List.Cons (x, x0) -> Types.None)
 144   | Nat.S m ->
 145     (match l with
 146      | List.Nil -> Types.None
 147      | List.Cons (h, t) ->
 148        (match h with
 149         | ByteValues.BVundef -> Types.None
 150         | ByteValues.BVnonzero -> Types.None
 151         | ByteValues.BVXor (x, x0, x1) -> Types.None
 152         | ByteValues.BVByte b ->
 153           Types.option_map (fun tl ->
 154             Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 155               (Nat.S Nat.O))))))))
 156               (Nat.times m (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 157                 (Nat.S Nat.O))))))))) b tl) (build_integer m t)
 158         | ByteValues.BVnull x -> Types.None
 159         | ByteValues.BVptr (x, x0) -> Types.None
 160         | ByteValues.BVpc (x, x0) -> Types.None))
 161
 162 (** val build_integer_val :
 163     AST.typ -> ByteValues.beval List.list -> Values.val0 **)
 164 let build_integer_val t l =
 165   match t with
 166   | AST.ASTint (sz, sg) ->
 167     Types.option_map_def (fun x -> Values.Vint (sz, x)) Values.Vundef
 168       (build_integer (AST.size_intsize sz) l)
 169   | AST.ASTptr -> Values.Vundef
 170
 171 (** val be_to_fe_value :
 172     AST.typ -> ByteValues.beval List.list -> Values.val0 **)
 173 let be_to_fe_value ty l = match l with
 174 | List.Nil -> Values.Vundef
 175 | List.Cons (h, t) ->
 176   (match h with
 177    | ByteValues.BVundef -> Values.Vundef
 178    | ByteValues.BVnonzero -> Values.Vundef
 179    | ByteValues.BVXor (x, x0, x1) -> Values.Vundef
 180    | ByteValues.BVByte b -> build_integer_val ty l
 181    | ByteValues.BVnull pt ->
 182      (match Bool.andb (Nat.eqb (ByteValues.part_no pt) Nat.O)
 183               (check_be_null (Nat.S Nat.O) t) with
 184       | Bool.True -> Values.Vnull
 185       | Bool.False -> Values.Vundef)
 186    | ByteValues.BVptr (x, x0) ->
 187      (match ByteValues.pointer_of_bevals l with
 188       | Errors.OK ptr -> Values.Vptr ptr
 189       | Errors.Error x1 -> Values.Vundef)
 190    | ByteValues.BVpc (x, x0) -> Values.Vundef)
 191