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
|
open import Pervasives
open import Vector
open import State
open import Sail_values
(*
let rec countLeadingZeros_helper bits =
((match bits with
| (Interp.V_lit (L_aux( L_zero, _)))::bits ->
let (Interp.V_lit (L_aux( (L_num n), loc))) = (countLeadingZeros_helper bits) in
Interp.V_lit (L_aux( (L_num (Nat_big_num.add n(Nat_big_num.of_int 1))), loc))
| _ -> Interp.V_lit (L_aux( (L_num(Nat_big_num.of_int 0)), Interp_ast.Unknown))
))
let rec countLeadingZeros (Interp.V_tuple v) = ((match v with
| [Interp.V_track( v, r);Interp.V_track( v2, r2)] ->
Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) ( Pset.(union) r r2)
| [Interp.V_track( v, r);v2] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r
| [v;Interp.V_track( v2, r2)] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r2
| [Interp.V_unknown;_] -> Interp.V_unknown
| [_;Interp.V_unknown] -> Interp.V_unknown
| [Interp.V_vector( _, _, bits);Interp.V_lit (L_aux( (L_num n), _))] ->
countLeadingZeros_helper (snd (Lem_list.split_at (abs (Nat_big_num.to_int n)) bits))
))
*)
let MEMr (addr,l) = read_memory (unsigned addr) l
let MEMr_reserve (addr,l) = read_memory (unsigned addr) l
let MEMw (addr,l,value) = write_memory (unsigned addr) l value
let MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return true
let I_Sync () = return ()
let H_Sync () = return ()
let LW_Sync () = return ()
let EIEIO_Sync () = return ()
let recalculate_dependency () = return ()
let trap () = ()
(* this needs to change, but for that we'd have to make the type checker know about trap
* as an effect *)
val countLeadingZeroes : vector bit * integer -> integer
let countLeadingZeroes (V bits _ _ ,n) =
let (_,bits) = List.splitAt (natFromInteger n) bits in
integerFromNat (List.length (takeWhile ((=) O) bits))
|
