1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
|
open import Pervasives
open import Interp
open import Interp_ast
import Maybe_extra
open import Num
open import List
open import Word
open import Bool
let ignore_sail x = V_lit (L_aux L_unit Unknown) ;;
let compose f g x = f (V_tuple [g x]) ;;
let is_one (V_lit (L_aux b lb)) = V_lit (L_aux (if b = L_one then L_true else L_false) lb) ;;
let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;;
let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
| L_one -> L_zero
| L_zero -> L_one end) la) ;;
let neq = compose neg eq ;;
let lt_range (V_tuple[V_lit (L_aux (L_num l1) lr);V_lit (L_aux (L_num l2) ll);]) =
if l1 < l2
then V_lit (L_aux L_one Unknown)
else V_lit (L_aux L_zero Unknown)
let bit_to_bool b = match b with
V_lit (L_aux L_zero _) -> false
| V_lit (L_aux L_one _) -> true
end ;;
let bool_to_bit b = match b with
false -> V_lit (L_aux L_zero Unknown)
| true -> V_lit (L_aux L_one Unknown)
end ;;
let bitwise_not (V_vector idx inc v) =
let apply x = bool_to_bit(not (bit_to_bool x)) in
V_vector idx inc (List.map apply v)
let bitwise_not_bit (V_lit (L_aux l loc)) = match l with
| L_zero -> (V_lit (L_aux L_one loc))
| L_one -> (V_lit (L_aux L_zero loc))
end;;
let bitwise_binop_bit op (V_tuple [x; y]) =
bool_to_bit (op (bit_to_bool x) (bit_to_bool y))
;;
let bitwise_binop op (V_tuple [V_vector idx inc v; V_vector idx' inc' v']) =
(* typechecker ensures inc = inc', idx = idx' and length v = length v' *)
let apply (x, y) = bool_to_bit(op (bit_to_bool x) (bit_to_bool y)) in
V_vector idx inc (List.map apply (List.zip v v'))
(* BitSeq expects LSB first.
* By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
* hence MSB first.
* http://en.wikipedia.org/wiki/Bit_numbering *)
let to_num signed (V_vector idx inc l) =
(* Word library in Lem expects bitseq with LSB first *)
let l = if inc then reverse l else l in
(* Make sure the last bit is a zero to force unsigned numbers *)
let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in
V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown);;
let to_vec_inc len (V_lit(L_aux (L_num n) ln)) =
let l = boolListFrombitSeq len (bitSeqFromInteger Nothing n) in
V_vector 0 true (map bool_to_bit (reverse l)) ;;
let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
let l = boolListFrombitSeq len (bitSeqFromInteger Nothing n) in
V_vector 0 false (map bool_to_bit l) ;;
let to_vec ord len n =
if ord
then to_vec_inc len n
else to_vec_dec len n
;;
let exts len ((V_vector _ inc _) as v) =
to_vec inc len (to_num true v)
;;
let arith_op op (V_tuple args) = match args with
| [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (op x y)) lx)
end ;;
let arith_op_vec op (V_tuple args) = match args with
| [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
let (l1',l2') = (to_num false l1,to_num false l2) in
let n = arith_op op (V_tuple [l1';l2']) in
to_vec ord (List.length cs) n
end ;;
let arith_op_range_vec op (V_tuple args) = match args with
| [n; (V_vector _ ord cs as l2)] ->
arith_op_vec op (V_tuple [(to_vec ord (List.length cs) n);l2])
end ;;
let arith_op_vec_range op (V_tuple args) = match args with
| [(V_vector _ ord cs as l1);n] ->
arith_op_vec op (V_tuple [l1;(to_vec ord (List.length cs) n)])
end ;;
let arith_op_range_vec_range op (V_tuple args) = match args with
| [n;(V_vector _ _ _ as l2)] ->
arith_op op (V_tuple [n;(to_num true l2)])
end ;;
let arith_op_vec_range_range op (V_tuple args) = match args with
| [(V_vector _ _ _ as l1);n] ->
arith_op op (V_tuple [(to_num true l1);n])
end ;;
let compare_op op (V_tuple args) = match args with
| [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] ->
if (op x y)
then V_lit(L_aux L_one lx)
else V_lit(L_aux L_zero lx)
end ;;
let compare_op_vec op (V_tuple args) = match args with
| [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
let (l1',l2') = (to_num true l1, to_num true l2) in
compare_op op (V_tuple[l1';l2'])
end ;;
let rec vec_concat (V_tuple args) = match args with
| [V_vector n d l; V_vector n' d' l'] ->
(* XXX d = d' ? droping n' ? *)
V_vector n d (l ++ l')
| [V_lit l; x] -> vec_concat (V_tuple [litV_to_vec l; x])
| [x; V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l])
end ;;
let function_map = [
("ignore", ignore_sail);
("add", arith_op (+));
("add_vec", arith_op_vec (+));
("add_vec_range", arith_op_vec_range (+));
("add_vec_range_range", arith_op_vec_range_range (+));
("add_range_vec", arith_op_range_vec (+));
("add_range_vec_range", arith_op_range_vec_range (+));
("minus", arith_op (-));
("minus_vec", arith_op_vec (-));
("eq", eq);
("neq", neq);
("vec_concat", vec_concat);
("is_one", is_one);
("to_num_inc", to_num false);
("to_num_dec", to_num false);
("exts", exts 64);
(* XXX the size of the target vector should be given by the interpreter *)
("to_vec_inc", to_vec_inc 64);
("to_vec_dec", to_vec_dec 64);
("bitwise_not", bitwise_not);
("bitwise_not_bit", bitwise_not_bit);
("bitwise_and", bitwise_binop (&&));
("bitwise_or", bitwise_binop (||));
("bitwise_xor", bitwise_binop xor);
("bitwise_and_bit", bitwise_binop_bit (&&));
("bitwise_or_bit", bitwise_binop_bit (||));
("bitwise_xor_bit", bitwise_binop_bit xor);
("lt", compare_op (<));
("gt", compare_op (>));
("lt_vec", compare_op_vec (<));
("gt_vec", compare_op_vec (>));
] ;;
let eval_external name v = (Maybe_extra.fromJust (List.lookup name function_map)) v ;;
|
