blob: 85a01bf9fe59d231d7a1fb8a85fbd39ff369300f (
plain)
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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
|
Require Import Sail.Values.
Require Import Sail.Operators.
(*
(* Specialisation of operators to bit lists *)
val access_vec_inc : list bitU -> integer -> bitU
let access_vec_inc = access_bv_inc
val access_vec_dec : list bitU -> integer -> bitU
let access_vec_dec = access_bv_dec
val update_vec_inc : list bitU -> integer -> bitU -> list bitU
let update_vec_inc = update_bv_inc
val update_vec_dec : list bitU -> integer -> bitU -> list bitU
let update_vec_dec = update_bv_dec
val subrange_vec_inc : list bitU -> integer -> integer -> list bitU
let subrange_vec_inc = subrange_bv_inc
val subrange_vec_dec : list bitU -> integer -> integer -> list bitU
let subrange_vec_dec = subrange_bv_dec
val update_subrange_vec_inc : list bitU -> integer -> integer -> list bitU -> list bitU
let update_subrange_vec_inc = update_subrange_bv_inc
val update_subrange_vec_dec : list bitU -> integer -> integer -> list bitU -> list bitU
let update_subrange_vec_dec = update_subrange_bv_dec
val extz_vec : integer -> list bitU -> list bitU
let extz_vec = extz_bv
val exts_vec : integer -> list bitU -> list bitU
let exts_vec = exts_bv
val concat_vec : list bitU -> list bitU -> list bitU
let concat_vec = concat_bv
val cons_vec : bitU -> list bitU -> list bitU
let cons_vec = cons_bv
val bool_of_vec : mword ty1 -> bitU
let bool_of_vec = bool_of_bv
val cast_unit_vec : bitU -> mword ty1
let cast_unit_vec = cast_unit_bv
val vec_of_bit : integer -> bitU -> list bitU
let vec_of_bit = bv_of_bit
val msb : list bitU -> bitU
let msb = most_significant
val int_of_vec : bool -> list bitU -> integer
let int_of_vec = int_of_bv
val string_of_vec : list bitU -> string
let string_of_vec = string_of_bv
val and_vec : list bitU -> list bitU -> list bitU
val or_vec : list bitU -> list bitU -> list bitU
val xor_vec : list bitU -> list bitU -> list bitU
val not_vec : list bitU -> list bitU
let and_vec = and_bv
let or_vec = or_bv
let xor_vec = xor_bv
let not_vec = not_bv
val add_vec : list bitU -> list bitU -> list bitU
val sadd_vec : list bitU -> list bitU -> list bitU
val sub_vec : list bitU -> list bitU -> list bitU
val mult_vec : list bitU -> list bitU -> list bitU
val smult_vec : list bitU -> list bitU -> list bitU
let add_vec = add_bv
let sadd_vec = sadd_bv
let sub_vec = sub_bv
let mult_vec = mult_bv
let smult_vec = smult_bv
val add_vec_int : list bitU -> integer -> list bitU
val sadd_vec_int : list bitU -> integer -> list bitU
val sub_vec_int : list bitU -> integer -> list bitU
val mult_vec_int : list bitU -> integer -> list bitU
val smult_vec_int : list bitU -> integer -> list bitU
let add_vec_int = add_bv_int
let sadd_vec_int = sadd_bv_int
let sub_vec_int = sub_bv_int
let mult_vec_int = mult_bv_int
let smult_vec_int = smult_bv_int
val add_int_vec : integer -> list bitU -> list bitU
val sadd_int_vec : integer -> list bitU -> list bitU
val sub_int_vec : integer -> list bitU -> list bitU
val mult_int_vec : integer -> list bitU -> list bitU
val smult_int_vec : integer -> list bitU -> list bitU
let add_int_vec = add_int_bv
let sadd_int_vec = sadd_int_bv
let sub_int_vec = sub_int_bv
let mult_int_vec = mult_int_bv
let smult_int_vec = smult_int_bv
val add_vec_bit : list bitU -> bitU -> list bitU
val sadd_vec_bit : list bitU -> bitU -> list bitU
val sub_vec_bit : list bitU -> bitU -> list bitU
let add_vec_bit = add_bv_bit
let sadd_vec_bit = sadd_bv_bit
let sub_vec_bit = sub_bv_bit
val add_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU)
val add_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU)
val sub_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU)
val sub_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU)
val mult_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU)
val mult_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU)
let add_overflow_vec = add_overflow_bv
let add_overflow_vec_signed = add_overflow_bv_signed
let sub_overflow_vec = sub_overflow_bv
let sub_overflow_vec_signed = sub_overflow_bv_signed
let mult_overflow_vec = mult_overflow_bv
let mult_overflow_vec_signed = mult_overflow_bv_signed
val add_overflow_vec_bit : list bitU -> bitU -> (list bitU * bitU * bitU)
val add_overflow_vec_bit_signed : list bitU -> bitU -> (list bitU * bitU * bitU)
val sub_overflow_vec_bit : list bitU -> bitU -> (list bitU * bitU * bitU)
val sub_overflow_vec_bit_signed : list bitU -> bitU -> (list bitU * bitU * bitU)
let add_overflow_vec_bit = add_overflow_bv_bit
let add_overflow_vec_bit_signed = add_overflow_bv_bit_signed
let sub_overflow_vec_bit = sub_overflow_bv_bit
let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed
val shiftl : list bitU -> integer -> list bitU
val shiftr : list bitU -> integer -> list bitU
val arith_shiftr : list bitU -> integer -> list bitU
val rotl : list bitU -> integer -> list bitU
val rotr : list bitU -> integer -> list bitU
let shiftl = shiftl_bv
let shiftr = shiftr_bv
let arith_shiftr = arith_shiftr_bv
let rotl = rotl_bv
let rotr = rotr_bv
val mod_vec : list bitU -> list bitU -> list bitU
val quot_vec : list bitU -> list bitU -> list bitU
val quot_vec_signed : list bitU -> list bitU -> list bitU
let mod_vec = mod_bv
let quot_vec = quot_bv
let quot_vec_signed = quot_bv_signed
val mod_vec_int : list bitU -> integer -> list bitU
val quot_vec_int : list bitU -> integer -> list bitU
let mod_vec_int = mod_bv_int
let quot_vec_int = quot_bv_int
val replicate_bits : list bitU -> integer -> list bitU
let replicate_bits = replicate_bits_bv
val duplicate : bitU -> integer -> list bitU
let duplicate = duplicate_bit_bv
val eq_vec : list bitU -> list bitU -> bool
val neq_vec : list bitU -> list bitU -> bool
val ult_vec : list bitU -> list bitU -> bool
val slt_vec : list bitU -> list bitU -> bool
val ugt_vec : list bitU -> list bitU -> bool
val sgt_vec : list bitU -> list bitU -> bool
val ulteq_vec : list bitU -> list bitU -> bool
val slteq_vec : list bitU -> list bitU -> bool
val ugteq_vec : list bitU -> list bitU -> bool
val sgteq_vec : list bitU -> list bitU -> bool
let eq_vec = eq_bv
let neq_vec = neq_bv
let ult_vec = ult_bv
let slt_vec = slt_bv
let ugt_vec = ugt_bv
let sgt_vec = sgt_bv
let ulteq_vec = ulteq_bv
let slteq_vec = slteq_bv
let ugteq_vec = ugteq_bv
let sgteq_vec = sgteq_bv
*)
|
