source: driver/extracted/frontEndVal.ml @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 4.4 KB
Line 
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 Exp
22
23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
39open ErrorMessages
40
41open Option
42
43open Setoids
44
45open Monad
46
47open Positive
48
49open PreIdentifiers
50
51open Errors
52
53open Div_and_mod
54
55open Jmeq
56
57open Russell
58
59open Util
60
61open Bool
62
63open Relations
64
65open Nat
66
67open List
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Types
78
79open Coqlib
80
81open Values
82
83open Hide
84
85open ByteValues
86
87(** val make_parts : ByteValues.part List.list **)
88let 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 **)
92let 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 **)
97let 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 **)
112let 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 **)
122let 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 **)
138let 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 **)
164let 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 **)
173let 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
Note: See TracBrowser for help on using the repository browser.