[2601] | 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 | |
---|
[2717] | 21 | open Exp |
---|
| 22 | |
---|
[2601] | 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 | |
---|
[2649] | 39 | open ErrorMessages |
---|
| 40 | |
---|
[2601] | 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 |
---|
[2773] | 124 | | List.Cons (hd, tl) -> |
---|
| 125 | (match hd with |
---|
[2601] | 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 -> |
---|
[2773] | 154 | Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
[2601] | 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 | |
---|