blob: 3cde7ade782121166c10d4d902f2f73eddab95c2 (
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
|
open import Pervasives_extra
(*open import Sail_impl_base*)
open import Sail2_values
open import Sail2_prompt_monad
open import {isabelle} `Sail2_prompt_monad_lemmas`
val (>>=) : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
declare isabelle target_rep function (>>=) = infix `\<bind>`
let inline ~{isabelle} (>>=) = bind
val (>>) : forall 'rv 'b 'e. monad 'rv unit 'e -> monad 'rv 'b 'e -> monad 'rv 'b 'e
declare isabelle target_rep function (>>) = infix `\<then>`
let inline ~{isabelle} (>>) m n = m >>= fun (_ : unit) -> n
val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
let rec iter_aux i f xs = match xs with
| x :: xs -> f i x >> iter_aux (i + 1) f xs
| [] -> return ()
end
declare {isabelle} termination_argument iter_aux = automatic
val iteri : forall 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
let iteri f xs = iter_aux 0 f xs
val iter : forall 'rv 'a 'e. ('a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
let iter f xs = iteri (fun _ x -> f x) xs
val foreachM : forall 'a 'rv 'vars 'e.
list 'a -> 'vars -> ('a -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
let rec foreachM l vars body =
match l with
| [] -> return vars
| (x :: xs) ->
body x vars >>= fun vars ->
foreachM xs vars body
end
declare {isabelle} termination_argument foreachM = automatic
val genlistM : forall 'a 'rv 'e. (nat -> monad 'rv 'a 'e) -> nat -> monad 'rv (list 'a) 'e
let genlistM f n =
let indices = genlist (fun n -> n) n in
foreachM indices [] (fun n xs -> (f n >>= (fun x -> return (xs ++ [x]))))
val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
let and_boolM l r = l >>= (fun l -> if l then r else return false)
val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
let or_boolM l r = l >>= (fun l -> if l then return true else r)
val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e
let bool_of_bitU_fail = function
| B0 -> return false
| B1 -> return true
| BU -> Fail "bool_of_bitU"
end
val bool_of_bitU_nondet : forall 'rv 'e. bitU -> monad 'rv bool 'e
let bool_of_bitU_nondet = function
| B0 -> return false
| B1 -> return true
| BU -> choose_bool "bool_of_bitU"
end
val bools_of_bits_nondet : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
let bools_of_bits_nondet bits =
foreachM bits []
(fun b bools ->
bool_of_bitU_nondet b >>= (fun b ->
return (bools ++ [b])))
val of_bits_nondet : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
let of_bits_nondet bits =
bools_of_bits_nondet bits >>= (fun bs ->
return (of_bools bs))
val of_bits_fail : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
let of_bits_fail bits = maybe_fail "of_bits" (of_bits bits)
val mword_nondet : forall 'rv 'a 'e. Size 'a => unit -> monad 'rv (mword 'a) 'e
let mword_nondet () =
bools_of_bits_nondet (repeat [BU] (integerFromNat size)) >>= (fun bs ->
return (wordFromBitlist bs))
val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
let rec whileM vars cond body =
cond vars >>= fun cond_val ->
if cond_val then
body vars >>= fun vars -> whileM vars cond body
else return vars
val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
let rec untilM vars cond body =
body vars >>= fun vars ->
cond vars >>= fun cond_val ->
if cond_val then return vars else untilM vars cond body
val choose_bools : forall 'rv 'e. string -> nat -> monad 'rv (list bool) 'e
let choose_bools descr n = genlistM (fun _ -> choose_bool descr) n
val choose : forall 'rv 'a 'e. string -> list 'a -> monad 'rv 'a 'e
let choose descr xs =
(* Use sufficiently many nondeterministically chosen bits and convert into an
index into the list *)
choose_bools descr (List.length xs) >>= fun bs ->
let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
match index xs idx with
| Just x -> return x
| Nothing -> Fail ("choose " ^ descr)
end
declare {isabelle} rename function choose = chooseM
val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
let internal_pick xs = choose "internal_pick" xs
(*let write_two_regs r1 r2 vec =
let is_inc =
let is_inc_r1 = is_inc_of_reg r1 in
let is_inc_r2 = is_inc_of_reg r2 in
let () = ensure (is_inc_r1 = is_inc_r2)
"write_two_regs called with vectors of different direction" in
is_inc_r1 in
let (size_r1 : integer) = size_of_reg r1 in
let (start_vec : integer) = get_start vec in
let size_vec = length vec in
let r1_v =
if is_inc
then slice vec start_vec (size_r1 - start_vec - 1)
else slice vec start_vec (start_vec - size_r1 - 1) in
let r2_v =
if is_inc
then slice vec (size_r1 - start_vec) (size_vec - start_vec)
else slice vec (start_vec - size_r1) (start_vec - size_vec) in
write_reg r1 r1_v >> write_reg r2 r2_v*)
|
