forked from rems-project/sail
-
Notifications
You must be signed in to change notification settings - Fork 12
/
Copy pathAarch64_extras.thy
136 lines (105 loc) · 6.35 KB
/
Aarch64_extras.thy
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
chapter \<open>Generated by Lem from \<open>/auto/homes/tb592/REMS/sail/aarch64/mono/aarch64_extras.lem\<close>.\<close>
theory "Aarch64_extras"
imports
Main
"LEM.Lem_pervasives_extra"
"Sail.Sail2_instr_kinds"
"Sail.Sail2_values"
"Sail.Sail2_operators_mwords"
"Sail.Sail2_prompt_monad"
"Sail.Sail2_prompt"
begin
(*open import Pervasives_extra*)
(*open import Sail2_instr_kinds*)
(*open import Sail2_values*)
(*open import Sail2_operators_mwords*)
(*open import Sail2_prompt_monad*)
(*open import Sail2_prompt*)
(*type ty512*)
(*type ty1024*)
(*type ty2048*)
definition hexchar_to_bool_list :: " char \<Rightarrow>((bool)list)option " where
" hexchar_to_bool_list c = (
if c = (CHR ''0'') then Some ([False,False,False,False])
else if c = (CHR ''1'') then Some ([False,False,False,True ])
else if c = (CHR ''2'') then Some ([False,False,True, False])
else if c = (CHR ''3'') then Some ([False,False,True, True ])
else if c = (CHR ''4'') then Some ([False,True, False,False])
else if c = (CHR ''5'') then Some ([False,True, False,True ])
else if c = (CHR ''6'') then Some ([False,True, True, False])
else if c = (CHR ''7'') then Some ([False,True, True, True ])
else if c = (CHR ''8'') then Some ([True, False,False,False])
else if c = (CHR ''9'') then Some ([True, False,False,True ])
else if c = (CHR ''A'') then Some ([True, False,True, False])
else if c = (CHR ''a'') then Some ([True, False,True, False])
else if c = (CHR ''B'') then Some ([True, False,True, True ])
else if c = (CHR ''b'') then Some ([True, False,True, True ])
else if c = (CHR ''C'') then Some ([True, True, False,False])
else if c = (CHR ''c'') then Some ([True, True, False,False])
else if c = (CHR ''D'') then Some ([True, True, False,True ])
else if c = (CHR ''d'') then Some ([True, True, False,True ])
else if c = (CHR ''E'') then Some ([True, True, True, False])
else if c = (CHR ''e'') then Some ([True, True, True, False])
else if c = (CHR ''F'') then Some ([True, True, True, True ])
else if c = (CHR ''f'') then Some ([True, True, True, True ])
else None )"
definition hexstring_to_bools :: " string \<Rightarrow>((bool)list)option " where
" hexstring_to_bools s = (
(case ( s) of
z # x # hs =>
(let str = (if ((z = (CHR ''0'')) \<and> (x = (CHR ''x''))) then hs else z # (x # hs)) in
map_option List.concat (just_list (List.map hexchar_to_bool_list str)))
| _ => None
))"
(*val hex_slice : forall 'rv 'n 'e. Size 'n => string -> integer -> integer -> monad 'rv (mword 'n) 'e*)
definition hex_slice :: " string \<Rightarrow> int \<Rightarrow> int \<Rightarrow>('rv,(('n::len)Word.word),'e)monad " where
" hex_slice v len lo = (
maybe_fail (''hex_slice'') (hexstring_to_bools v) \<bind> (\<lambda> bs .
(let hi = ((len + lo) -( 1 :: int)) in
(let bs = (ext_list False (len + lo) bs) in
return (Word.of_bl (subrange_list False bs hi lo))))))"
(*val BigEndianReverse : forall 'rv 'n 'e. Size 'n => mword 'n -> monad 'rv (mword 'n) 'e*)
definition BigEndianReverse :: "('n::len)Word.word \<Rightarrow>('rv,(('n::len)Word.word),'e)monad " where
" BigEndianReverse w = ( return (reverse_endianness w))"
(* Use constants for some undefined values for now *)
definition undefined_string :: " unit \<Rightarrow>('b,(string),'a)monad " where
" undefined_string _ = ( return (''''))"
definition undefined_unit :: " unit \<Rightarrow>('b,(unit),'a)monad " where
" undefined_unit _ = ( return () )"
definition undefined_int :: " unit \<Rightarrow>('b,(int),'a)monad " where
" undefined_int _ = ( return (( 0 :: int)::ii))"
(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*)
definition undefined_vector :: " int \<Rightarrow> 'a \<Rightarrow>('rv,('a list),'e)monad " where
" undefined_vector len u = ( return (repeat [u] len))"
(*val undefined_bitvector : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e*)
definition undefined_bitvector :: " int \<Rightarrow>('rv,(('a::len)Word.word),'e)monad " where
" undefined_bitvector len = ( return (Word.of_bl (repeat [False] len)))"
(*val undefined_bits : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e*)
definition undefined_bits :: " int \<Rightarrow>('rv,(('a::len)Word.word),'e)monad " where
" undefined_bits = ( undefined_bitvector )"
definition undefined_bit :: " unit \<Rightarrow>('b,(bitU),'a)monad " where
" undefined_bit _ = ( return B0 )"
definition undefined_real :: " unit \<Rightarrow>('b,(real),'a)monad " where
" undefined_real _ = ( return (realFromFrac(( 0 :: int))(( 1 :: int))))"
definition undefined_range :: " 'a \<Rightarrow> 'd \<Rightarrow>('c,'a,'b)monad " where
" undefined_range i j = ( return i )"
definition undefined_atom :: " 'a \<Rightarrow>('c,'a,'b)monad " where
" undefined_atom i = ( return i )"
definition undefined_nat :: " unit \<Rightarrow>('b,(int),'a)monad " where
" undefined_nat _ = ( return (( 0 :: int)::ii))"
(*val write_ram : forall 'rv 'a 'b 'c 'e. Size 'b, Size 'c =>
integer -> integer -> mword 'a -> mword 'b -> mword 'c -> monad 'rv unit 'e*)
definition write_ram :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('b::len)Word.word \<Rightarrow>('c::len)Word.word \<Rightarrow>('rv,(unit),'e)monad " where
" write_ram addrsize size1 hexRAM address value1 = (
(write_mem_ea instance_Sail2_values_Bitvector_Machine_word_mword_dict Write_plain address size1 \<then>
write_mem_val instance_Sail2_values_Bitvector_Machine_word_mword_dict value1) \<bind> (\<lambda>x . (case x of _ => return () )) )"
(*val read_ram : forall 'rv 'a 'b 'c 'e. Size 'b, Size 'c =>
integer -> integer -> mword 'a -> mword 'b -> monad 'rv (mword 'c) 'e*)
definition read_ram :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('b::len)Word.word \<Rightarrow>('rv,(('c::len)Word.word),'e)monad " where
" read_ram addrsize size1 hexRAM address = (
(*let _ = prerr_endline (Reading ^ (stringFromInteger size) ^ bytes from address ^ (stringFromInteger (unsigned address))) in*)
read_mem instance_Sail2_values_Bitvector_Machine_word_mword_dict instance_Sail2_values_Bitvector_Machine_word_mword_dict Read_plain address size1 )"
(*val elf_entry : unit -> integer*)
definition elf_entry :: " unit \<Rightarrow> int " where
" elf_entry _ = (( 0 :: int))"
end