source: extracted/frontEndVal.ml @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

File size: 4.4 KB
RevLine 
[2601]1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open Extralib
10
11open Lists
12
13open Identifiers
14
15open Integers
16
17open AST
18
19open Division
20
21open Arithmetic
22
23open Extranat
24
25open Vector
26
27open FoldStuff
28
29open BitVector
30
31open Z
32
33open BitVectorZ
34
35open Pointers
36
[2649]37open ErrorMessages
38
[2601]39open Option
40
41open Setoids
42
43open Monad
44
45open Positive
46
47open PreIdentifiers
48
49open Errors
50
51open Div_and_mod
52
53open Jmeq
54
55open Russell
56
57open Util
58
59open Bool
60
61open Relations
62
63open Nat
64
65open List
66
67open Hints_declaration
68
69open Core_notation
70
71open Pts
72
73open Logic
74
75open Types
76
77open Coqlib
78
79open Values
80
81open Hide
82
83open ByteValues
84
85(** val make_parts : ByteValues.part List.list **)
86let make_parts =
87  List.map ByteValues.part_from_sig (Lists.range_strong AST.size_pointer)
88
89(** val make_be_null : ByteValues.beval List.list **)
90let make_be_null =
91  List.map (fun p -> ByteValues.BVnull p) make_parts
92
93(** val bytes_of_bitvector :
94    Nat.nat -> BitVector.bitVector -> BitVector.byte List.list **)
95let rec bytes_of_bitvector n v =
96  (match n with
97   | Nat.O -> (fun x -> List.Nil)
98   | Nat.S m ->
99     (fun v0 ->
100       let { Types.fst = h; Types.snd = t } =
101         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
102           (Nat.S Nat.O))))))))
103           (Nat.times m (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
104             (Nat.S Nat.O))))))))) v0
105       in
106       List.Cons (h, (bytes_of_bitvector m t)))) v
107
108(** val fe_to_be_values :
109    AST.typ -> Values.val0 -> ByteValues.beval List.list **)
110let fe_to_be_values t = function
111| Values.Vundef -> List.make_list ByteValues.BVundef (AST.typesize t)
112| Values.Vint (sz, i) ->
113  List.map (fun b -> ByteValues.BVByte b)
114    (bytes_of_bitvector (AST.size_intsize sz) i)
115| Values.Vnull -> make_be_null
116| Values.Vptr ptr -> ByteValues.bevals_of_pointer ptr
117
118(** val check_be_null :
119    Nat.nat -> ByteValues.beval List.list -> Bool.bool **)
120let rec check_be_null n = function
121| List.Nil -> Nat.eqb AST.size_pointer n
122| List.Cons (hd0, tl) ->
123  (match hd0 with
124   | ByteValues.BVundef -> Bool.False
125   | ByteValues.BVnonzero -> Bool.False
126   | ByteValues.BVXor (x, x0, x1) -> Bool.False
127   | ByteValues.BVByte x -> Bool.False
128   | ByteValues.BVnull pt ->
129     Bool.andb (Nat.eqb (ByteValues.part_no pt) n)
130       (check_be_null (Nat.S n) tl)
131   | ByteValues.BVptr (x, x0) -> Bool.False
132   | ByteValues.BVpc (x, x0) -> Bool.False)
133
134(** val build_integer :
135    Nat.nat -> ByteValues.beval List.list -> BitVector.bitVector Types.option **)
136let rec build_integer n l =
137  match n with
138  | Nat.O ->
139    (match l with
140     | List.Nil -> Types.Some Vector.VEmpty
141     | List.Cons (x, x0) -> Types.None)
142  | Nat.S m ->
143    (match l with
144     | List.Nil -> Types.None
145     | List.Cons (h, t) ->
146       (match h with
147        | ByteValues.BVundef -> Types.None
148        | ByteValues.BVnonzero -> Types.None
149        | ByteValues.BVXor (x, x0, x1) -> Types.None
150        | ByteValues.BVByte b ->
151          Types.option_map (fun tl ->
152            Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
153              (Nat.S Nat.O))))))))
154              (Nat.times m (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
155                (Nat.S Nat.O))))))))) b tl) (build_integer m t)
156        | ByteValues.BVnull x -> Types.None
157        | ByteValues.BVptr (x, x0) -> Types.None
158        | ByteValues.BVpc (x, x0) -> Types.None))
159
160(** val build_integer_val :
161    AST.typ -> ByteValues.beval List.list -> Values.val0 **)
162let build_integer_val t l =
163  match t with
164  | AST.ASTint (sz, sg) ->
165    Types.option_map_def (fun x -> Values.Vint (sz, x)) Values.Vundef
166      (build_integer (AST.size_intsize sz) l)
167  | AST.ASTptr -> Values.Vundef
168
169(** val be_to_fe_value :
170    AST.typ -> ByteValues.beval List.list -> Values.val0 **)
171let be_to_fe_value ty l = match l with
172| List.Nil -> Values.Vundef
173| List.Cons (h, t) ->
174  (match h with
175   | ByteValues.BVundef -> Values.Vundef
176   | ByteValues.BVnonzero -> Values.Vundef
177   | ByteValues.BVXor (x, x0, x1) -> Values.Vundef
178   | ByteValues.BVByte b -> build_integer_val ty l
179   | ByteValues.BVnull pt ->
180     (match Bool.andb (Nat.eqb (ByteValues.part_no pt) Nat.O)
181              (check_be_null (Nat.S Nat.O) t) with
182      | Bool.True -> Values.Vnull
183      | Bool.False -> Values.Vundef)
184   | ByteValues.BVptr (x, x0) ->
185     (match ByteValues.pointer_of_bevals l with
186      | Errors.OK ptr -> Values.Vptr ptr
187      | Errors.Error x1 -> Values.Vundef)
188   | ByteValues.BVpc (x, x0) -> Values.Vundef)
189
Note: See TracBrowser for help on using the repository browser.