Source file sail2_operators.ml

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
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
(*Generated by Lem from sail2_operators.lem.*)
open Lem_pervasives_extra
open Lem_machine_word
open Sail2_values

(*** Bit vector operations *)

(*val concat_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => 'a -> 'b -> list bitU*)
let concat_bv dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b l r:(bitU)list=  ( List.rev_append (List.rev (
  dict_Sail2_values_Bitvector_a.bits_of_method l)) (dict_Sail2_values_Bitvector_b.bits_of_method r))

(*val cons_bv : forall 'a. Bitvector 'a => bitU -> 'a -> list bitU*)
let cons_bv dict_Sail2_values_Bitvector_a b v:(bitU)list=  (b :: 
  dict_Sail2_values_Bitvector_a.bits_of_method v)

(*val cast_unit_bv : bitU -> list bitU*)
let cast_unit_bv b:(bitU)list=  ([b])

(*val bv_of_bit : integer -> bitU -> list bitU*)
let bv_of_bit len b:(bitU)list=  (extz_bits len [b])

let most_significant dict_Sail2_values_Bitvector_a v:bitU=  ((match  
  dict_Sail2_values_Bitvector_a.bits_of_method v with
  | b :: _ -> b
  | _ -> B0 (* Treat empty bitvector as all zeros *)
  ))

let get_max_representable_in sign (n : Nat_big_num.num) : Nat_big_num.num=
   (if ( Nat_big_num.equal n( (Nat_big_num.of_int 64))) then (match sign with | true -> max_64 | false -> max_64u )
  else if (Nat_big_num.equal n( (Nat_big_num.of_int 32))) then (match sign with | true -> max_32 | false -> max_32u )
  else if (Nat_big_num.equal n( (Nat_big_num.of_int 8))) then max_8
  else if (Nat_big_num.equal n( (Nat_big_num.of_int 5))) then max_5
  else (match sign with | true -> Nat_big_num.pow_int( (Nat_big_num.of_int 2)) ( Nat_num.nat_monus(abs (Nat_big_num.to_int n))1)
                       | false -> Nat_big_num.pow_int( (Nat_big_num.of_int 2)) (abs (Nat_big_num.to_int n))
       ))

let get_min_representable_in _ (n : Nat_big_num.num) : Nat_big_num.num=
   (if Nat_big_num.equal n( (Nat_big_num.of_int 64)) then min_64
  else if Nat_big_num.equal n( (Nat_big_num.of_int 32)) then min_32
  else if Nat_big_num.equal n( (Nat_big_num.of_int 8)) then min_8
  else if Nat_big_num.equal n( (Nat_big_num.of_int 5)) then min_5
  else Nat_big_num.sub( (Nat_big_num.of_int 0)) (Nat_big_num.pow_int( (Nat_big_num.of_int 2)) (abs (Nat_big_num.to_int n))))

(*val arith_op_bv_int : forall 'a 'b. Bitvector 'a =>
  (integer -> integer -> integer) -> bool -> 'a -> integer -> 'a*)
let arith_op_bv_int dict_Sail2_values_Bitvector_a op sign l r:'a=
   (let r' = (dict_Sail2_values_Bitvector_a.of_int_method (dict_Sail2_values_Bitvector_a.length_method l) r) in  dict_Sail2_values_Bitvector_a.arith_op_bv_method op sign l r')

(*val arith_op_int_bv : forall 'a 'b. Bitvector 'a =>
  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a*)
let arith_op_int_bv dict_Sail2_values_Bitvector_a op sign l r:'a=
   (let l' = (dict_Sail2_values_Bitvector_a.of_int_method (dict_Sail2_values_Bitvector_a.length_method r) l) in  dict_Sail2_values_Bitvector_a.arith_op_bv_method op sign l' r)

let arith_op_bv_bool dict_Sail2_values_Bitvector_a op sign l r:'a=  (arith_op_bv_int 
  dict_Sail2_values_Bitvector_a op sign l (if r then  (Nat_big_num.of_int 1) else  (Nat_big_num.of_int 0)))
let arith_op_bv_bit dict_Sail2_values_Bitvector_a op sign l r:'a option=  (Lem.option_map (arith_op_bv_bool 
  dict_Sail2_values_Bitvector_a op sign l) (bool_of_bitU r))

(* TODO (or just omit and define it per spec if needed)
val arith_op_overflow_bv : forall 'a. Bitvector 'a =>
  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> (list bitU * bitU * bitU)
let arith_op_overflow_bv op sign size l r =
  let len = length l in
  let act_size = len * size in
  match (int_of_bv sign l, int_of_bv sign r, int_of_bv false l, int_of_bv false r) with
    | (Just l_sign, Just r_sign, Just l_unsign, Just r_unsign) ->
       let n = op l_sign r_sign in
       let n_unsign = op l_unsign r_unsign in
       let correct_size = of_int act_size n in
       let one_more_size_u = bits_of_int (act_size + 1) n_unsign in
       let overflow =
         if n <= get_max_representable_in sign len &&
              n >= get_min_representable_in sign len
         then B0 else B1 in
       let c_out = most_significant one_more_size_u in
       (correct_size,overflow,c_out)
    | (_, _, _, _) ->
       (repeat [BU] act_size, BU, BU)
  end

let add_overflow_bv = arith_op_overflow_bv integerAdd false 1
let adds_overflow_bv = arith_op_overflow_bv integerAdd true 1
let sub_overflow_bv = arith_op_overflow_bv integerMinus false 1
let subs_overflow_bv = arith_op_overflow_bv integerMinus true 1
let mult_overflow_bv = arith_op_overflow_bv integerMult false 2
let mults_overflow_bv = arith_op_overflow_bv integerMult true 2

val arith_op_overflow_bv_bit : forall 'a. Bitvector 'a =>
  (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> (list bitU * bitU * bitU)
let arith_op_overflow_bv_bit op sign size l r_bit =
  let act_size = length l * size in
  match (int_of_bv sign l, int_of_bv false l, r_bit = BU) with
    | (Just l', Just l_u, false) ->
       let (n, nu, changed) = match r_bit with
         | B1 -> (op l' 1, op l_u 1, true)
         | B0 -> (l', l_u, false)
         | BU -> (* unreachable due to check above *)
            failwith "arith_op_overflow_bv_bit applied to undefined bit"
         end in
       let correct_size = of_int act_size n in
       let one_larger = bits_of_int (act_size + 1) nu in
       let overflow =
         if changed
         then
           if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
           then B0 else B1
         else B0 in
       (correct_size, overflow, most_significant one_larger)
    | (_, _, _) ->
       (repeat [BU] act_size, BU, BU)
  end

let add_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd false 1
let adds_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd true 1
let sub_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus false 1
let subs_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus true 1*)

type shift = LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot

let invert_shift:shift ->shift=  ((function
  | LL_shift -> RR_shift
  | RR_shift -> LL_shift
  | RR_shift_arith -> LL_shift
  | LL_rot -> RR_rot
  | RR_rot -> LL_rot
))

(*val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> list bitU*)
let shift_op_bv dict_Sail2_values_Bitvector_a op v n:(bitU)list=
   (let v = (dict_Sail2_values_Bitvector_a.bits_of_method v) in
  if Nat_big_num.equal n( (Nat_big_num.of_int 0)) then v else
  let (op, n) = (if Nat_big_num.greater n( (Nat_big_num.of_int 0)) then (op, n) else (invert_shift op, Nat_big_num.negate n)) in
  (match op with
  | LL_shift -> 
     List.rev_append (List.rev (subrange_list true v n ( Nat_big_num.sub(Nat_big_num.of_int (List.length v))( (Nat_big_num.of_int 1))))) (repeat [B0] n)
  | RR_shift -> 
     List.rev_append (List.rev (repeat [B0] n)) (subrange_list true v( (Nat_big_num.of_int 0)) ( Nat_big_num.sub (Nat_big_num.sub(Nat_big_num.of_int (List.length v)) n)( (Nat_big_num.of_int 1))))
  | RR_shift_arith -> 
     List.rev_append (List.rev (repeat [most_significant 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) v] n)) (subrange_list true v( (Nat_big_num.of_int 0)) ( Nat_big_num.sub (Nat_big_num.sub(Nat_big_num.of_int (List.length v)) n)( (Nat_big_num.of_int 1))))
  | LL_rot -> 
     List.rev_append (List.rev (subrange_list true v n ( Nat_big_num.sub(Nat_big_num.of_int (List.length v))( (Nat_big_num.of_int 1))))) (subrange_list true v( (Nat_big_num.of_int 0)) ( Nat_big_num.sub n( (Nat_big_num.of_int 1))))
  | RR_rot -> 
     List.rev_append (List.rev (subrange_list false v( (Nat_big_num.of_int 0)) ( Nat_big_num.sub n( (Nat_big_num.of_int 1))))) (subrange_list false v n ( Nat_big_num.sub(Nat_big_num.of_int (List.length v))( (Nat_big_num.of_int 1))))
  ))

let shiftl_bv dict_Sail2_values_Bitvector_a:'a ->Nat_big_num.num ->(bitU)list=  (shift_op_bv 
  dict_Sail2_values_Bitvector_a LL_shift) (*"<<"*)
let shiftr_bv dict_Sail2_values_Bitvector_a:'a ->Nat_big_num.num ->(bitU)list=  (shift_op_bv 
  dict_Sail2_values_Bitvector_a RR_shift) (*">>"*)
let arith_shiftr_bv dict_Sail2_values_Bitvector_a:'a ->Nat_big_num.num ->(bitU)list=  (shift_op_bv 
  dict_Sail2_values_Bitvector_a RR_shift_arith)
let rotl_bv dict_Sail2_values_Bitvector_a:'a ->Nat_big_num.num ->(bitU)list=  (shift_op_bv 
  dict_Sail2_values_Bitvector_a LL_rot) (*"<<<"*)
let rotr_bv dict_Sail2_values_Bitvector_a:'a ->Nat_big_num.num ->(bitU)list=  (shift_op_bv 
  dict_Sail2_values_Bitvector_a LL_rot) (*">>>"*)

let shiftl_mword w n:Lem.mword=  (Lem.word_shiftLeft w (nat_of_int n))
let shiftr_mword w n:Lem.mword=  (Lem.word_shiftRight w (nat_of_int n))
let arith_shiftr_mword w n:Lem.mword=  (Lem.word_arithShiftRight w (nat_of_int n))
let rotl_mword w n:Lem.mword=  (Lem.word_rol (nat_of_int n) w)
let rotr_mword w n:Lem.mword=  (Lem.word_ror (nat_of_int n) w)

let arith_op_no0 (op : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) l r:(Nat_big_num.num)option=
   (if Nat_big_num.equal r( (Nat_big_num.of_int 0))
  then None
  else Some (op l r))

(*val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> maybe 'b*)
let arith_op_bv_no0 dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b op sign size l r:'b option=
   (Lem.option_bind (int_of_bv 
  dict_Sail2_values_Bitvector_a sign l) (fun l' ->
  Lem.option_bind (int_of_bv 
  dict_Sail2_values_Bitvector_a sign r) (fun r' ->
  if Nat_big_num.equal r'( (Nat_big_num.of_int 0)) then None else Some (
  dict_Sail2_values_Bitvector_b.of_int_method ( Nat_big_num.mul(dict_Sail2_values_Bitvector_a.length_method l) size) (op l' r')))))

let mod_bv dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b:'b ->'b ->'a option=  (arith_op_bv_no0 
  dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a tmod_int false( (Nat_big_num.of_int 1)))
let quot_bv dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b:'b ->'b ->'a option=  (arith_op_bv_no0 
  dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a tdiv_int false( (Nat_big_num.of_int 1)))
let quots_bv dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b:'b ->'b ->'a option=  (arith_op_bv_no0 
  dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a tdiv_int true( (Nat_big_num.of_int 1)))

let mod_mword:Lem.mword ->Lem.mword ->Lem.mword=  Lem.word_mod
let quot_mword:Lem.mword ->Lem.mword ->Lem.mword=  Lem.word_udiv
let quots_mword:Lem.mword ->Lem.mword ->Lem.mword=  Lem_machine_word.signedDivide

let arith_op_bv_int_no0 dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b op sign size l r:'b option=
   (arith_op_bv_no0 dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b op sign size l (dict_Sail2_values_Bitvector_a.of_int_method (dict_Sail2_values_Bitvector_a.length_method l) r))

let quot_bv_int dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b:'b ->Nat_big_num.num ->'a option=  (arith_op_bv_int_no0 
  dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a tdiv_int false( (Nat_big_num.of_int 1)))
let mod_bv_int dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b:'b ->Nat_big_num.num ->'a option=  (arith_op_bv_int_no0 
  dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a tmod_int false( (Nat_big_num.of_int 1)))

let mod_mword_int dict_Machine_word_Size_a l r:Lem.mword=  (Lem.word_mod l (wordFromInteger 
  dict_Machine_word_Size_a r))
let quot_mword_int dict_Machine_word_Size_a l r:Lem.mword=  (Lem.word_udiv l (wordFromInteger 
  dict_Machine_word_Size_a r))
let quots_mword_int dict_Machine_word_Size_a l r:Lem.mword=  (Lem_machine_word.signedDivide l (wordFromInteger 
  dict_Machine_word_Size_a r))

let replicate_bits_bv dict_Sail2_values_Bitvector_a v count:(bitU)list=  (repeat (
  dict_Sail2_values_Bitvector_a.bits_of_method v) count)
let duplicate_bit_bv dict_Sail2_values_BitU_a bit len:(bitU)list=  (replicate_bits_bv 
  (instance_Sail2_values_Bitvector_list_dict dict_Sail2_values_BitU_a) [bit] len)

(*val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*)
let eq_bv dict_Sail2_values_Bitvector_a l r:bool=  ( (listEqualBy (=)(
  dict_Sail2_values_Bitvector_a.bits_of_method l) (dict_Sail2_values_Bitvector_a.bits_of_method r)))

(*val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*)
let neq_bv dict_Sail2_values_Bitvector_a l r:bool=  (not (eq_bv 
  dict_Sail2_values_Bitvector_a l r))

(*val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a*)
let get_slice_int_bv dict_Sail2_values_Bitvector_a len n lo:'a=
   (let hi = (Nat_big_num.sub (Nat_big_num.add lo len)( (Nat_big_num.of_int 1))) in
  let bs = (bools_of_int ( Nat_big_num.add hi( (Nat_big_num.of_int 1))) n) in  
  dict_Sail2_values_Bitvector_a.of_bools_method (subrange_list false bs hi lo))

(*val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer*)
let set_slice_int_bv dict_Sail2_values_Bitvector_a len n lo v:Nat_big_num.num=
   (let hi = (Nat_big_num.sub (Nat_big_num.add lo len)( (Nat_big_num.of_int 1))) in
  let bs = (bits_of_int ( Nat_big_num.add hi( (Nat_big_num.of_int 1))) n) in
  maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (
  dict_Sail2_values_Bitvector_a.bits_of_method v))))