-
Notifications
You must be signed in to change notification settings - Fork 119
/
sail2_prompt.lem
163 lines (133 loc) · 6.23 KB
/
sail2_prompt.lem
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
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 'e 'a 'b. either 'e 'a -> ('a -> either 'e 'b) -> either 'e 'b
declare isabelle target_rep function (>>$=) = infix `\<bind>\<^sub>R`
let inline ~{isabelle} (>>$=) = either_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 (>>$) : forall 'e 'a. either 'e unit -> either 'e 'a -> either 'e 'a
declare isabelle target_rep function (>>$) = infix `\<then>\<^sub>R`
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
val foreachE : forall 'a 'vars 'e.
list 'a -> 'vars -> ('a -> 'vars -> either 'e 'vars) -> either 'e 'vars
let rec foreachE l vars body =
match l with
| [] -> Right vars
| (x :: xs) ->
body x vars >>$= fun vars ->
foreachE 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. Register_Value 'rv => 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. Register_Value 'rv => 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, Register_Value 'rv => 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, Register_Value 'rv => 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. Register_Value 'rv => string -> nat -> monad 'rv (list bool) 'e
let choose_bools descr n = genlistM (fun _ -> choose_bool descr) n
val choose_bitvector : forall 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => string -> nat -> monad 'rv 'a 'e
let choose_bitvector descr n = choose_bools descr n >>= fun v -> return (of_bools v)
val choose_from_list : forall 'rv 'a 'e. Register_Value 'rv => string -> list 'a -> monad 'rv 'a 'e
let choose_from_list descr xs =
choose_int ("choose_from_list " ^ descr) >>= fun idx ->
match index xs (natFromInteger idx mod List.length xs) with
| Just x -> return x
| Nothing -> Fail ("choose_from_list " ^ descr)
end
val choose_int_in_range : forall 'rv 'e. Register_Value 'rv => string -> integer -> integer -> monad 'rv integer 'e
let choose_int_in_range descr i j =
choose_int descr >>= fun k ->
return (max i (min j k))
val choose_nat : forall 'rv 'e. Register_Value 'rv => string -> monad 'rv integer 'e
let choose_nat descr = choose_int descr >>= fun i -> return (max 0 i)
val internal_pick : forall 'rv 'a 'e. Register_Value 'rv => list 'a -> monad 'rv 'a 'e
let internal_pick xs = choose_from_list "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*)