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
|
theory Aarch64_code
imports
Aarch64_lemmas
"HOL-Library.Code_Char"
"HOL-Library.Code_Target_Nat"
"HOL-Library.Code_Target_Int"
"HOL-Library.Code_Real_Approx_By_Float"
begin
declare [[code abort: failwith]]
termination shl_int by lexicographic_order
termination while sorry
termination whileM sorry
termination untilM sorry
declare insert_code[code del]
declare union_coset_filter[code del]
lemma [code]: "(set xs) \<union> (set ys) = set (xs @ ys)"
by auto
lemma [code]: "insert x (set xs) = set (x # xs)"
by auto
declare [[code drop:
"less :: real \<Rightarrow> real \<Rightarrow> bool"
"less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
"floor :: real \<Rightarrow> int"]]
code_printing constant "floor :: real \<Rightarrow> int" \<rightharpoonup> (OCaml) "(Int'_of'_integer (Big'_int.big'_int'_of'_int (Pervasives.int'_of'_float (Pervasives.floor _))))"
code_identifier constant ASR \<rightharpoonup> (OCaml) "Aarch64.asr0"
code_identifier constant LSL \<rightharpoonup> (OCaml) "Aarch64.lsl0"
code_identifier constant LSR \<rightharpoonup> (OCaml) "Aarch64.lsr0"
fun prerr_endline' :: "String.literal \<Rightarrow> unit" where "prerr_endline' _ = ()"
lemma [code]: "prerr_endline s = prerr_endline' (String.implode s)" by auto
fun putchar' :: "char \<Rightarrow> unit" where "putchar' _ = ()"
lemma [code]: "putchar c = putchar' (char_of_nat (nat c))" by auto
code_identifier code_module List \<rightharpoonup> (OCaml) "List0"
code_printing constant String.implode \<rightharpoonup> (OCaml) "!(let l = _ in let res = Bytes.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> Bytes.set res i c; imp (i + 1) l in imp 0 l)"
code_printing constant prerr_endline' \<rightharpoonup> (OCaml) "Pervasives.prerr'_endline"
code_printing constant putchar' \<rightharpoonup> (OCaml) "Pervasives.print'_char"
fun write_char_mem :: "int \<Rightarrow> char \<Rightarrow> (regstate, unit, exception) monadS" where
"write_char_mem addr c =
bindS (write_mem_eaS BC_bitU_list Write_plain (bits_of_int 64 addr) 1) (\<lambda>_.
bindS (write_mem_valS BC_bitU_list (bits_of_nat 8 (nat_of_char c))) (\<lambda>_.
returnS ()))"
definition "initial_state \<equiv> init_state initial_regstate"
code_printing constant elf_entry \<rightharpoonup> (OCaml) "(Int'_of'_integer (Elf'_loader.elf'_entry _))"
termination BigEndianReverse sorry
export_code main initial_state liftState get_regval set_regval bindS returnS iteriS iterS write_char_mem integer_of_int int_of_integer "op + :: int \<Rightarrow> int \<Rightarrow> int" prerr_results in OCaml module_name "Aarch64" file "aarch64_export.ml"
end
|
