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
|
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_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 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 _ _ _ as l1);(V_vector _ _ _ as l2)] ->
let (l1',l2') = (to_num true l1,to_num true l2) in
arith_op op (V_tuple [l1';l2'])
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 (+));
("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", to_num true);
(* 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_and", bitwise_binop (&&));
("bitwise_or", bitwise_binop (||));
("bitwise_xor", bitwise_binop 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 ;;
|
