Theory LLVM_Examples
section ‹Examples›
theory LLVM_Examples
imports
"../ds/LLVM_DS_All"
"../ds/LLVM_DS_Array_List"
begin
text ‹Examples on top of Isabelle-LLVM basic layer.
For the verification of more complex algorithms, consider using
Isabelle-LLVM with the Refinement Framework, and the Sepref tool.
See, e.g., @{file Bin_Search.thy}.
›
subsection ‹Numeric Algorithms›
subsubsection ‹Exponentiation›
definition exp :: "'a::len word ⇒ 'b::len word llM" where [llvm_code]: "exp r ≡ doM {
a ← ll_const (unsigned 1);
(a,r) ← llc_while
(λ(a,r). doM { ll_icmp_ult (unsigned 0) r})
(λ(a,r). doM {
Mreturn (a*unsigned 2,r-unsigned 1)
})
(a,r);
Mreturn a
}"
abbreviation exp32::"32 word ⇒ 32 word llM" where "exp32 ≡ exp"
abbreviation exp64::"64 word ⇒ 64 word llM" where "exp64 ≡ exp"
export_llvm
exp32 is "uint32_t exp32 (uint32_t)"
exp64 is "uint64_t exp64 (uint64_t)"
file "code/exp.ll"
lemma exp_aux1:
assumes "2 ^ nat k < (N::int)" "t ≤ k" "0 < t"
shows "2 * 2 ^ nat (k - t) < N"
proof -
have "⟦2 ^ k < N; 0 < t; t ≤ k⟧ ⟹ 2 * 2 ^ (k - t) < (N::int)" for k t :: nat
by (metis Suc_leI diff_less less_le_trans not_less power.simps(2) power_increasing_iff rel_simps(49) semiring_norm(76))
with assms show ?thesis
by (auto simp add: nat_diff_distrib' dest!: nat_mono simp flip: zero_less_nat_eq)
qed
lemma exp_aux2: "⟦t ≤ k; 0 < t⟧ ⟹ nat (1+k-t) = Suc (nat (k-t))" by simp
lemma exp_correct:
assumes "LENGTH('b::len) ≥ 2"
shows "llvm_htriple
(↿uint.assn k (ki::'a::len word) ** ↑(2^nat k ∈ uints LENGTH('b)))
(exp ki)
(λr::'b word. ↿uint.assn (2^nat k) r ** ↿uint.assn k ki)"
unfolding exp_def
apply (rewrite annotate_llc_while[where
I="λ(ai,ri) t. EXS a r. ↿uint.assn a ai ** ↿uint.assn r ri ** ↑⇩d( 0≤r ∧ r≤k ∧ a = 2^nat (k-r) ) ** ↑⇩!(t = r)"
and R="measure nat"
])
apply vcg_monadify
apply (vcg'; (clarsimp simp: algebra_simps)?)
using assms
apply (simp_all add: exp_aux1 exp_aux2)
done
subsubsection ‹Euclid's Algorithm›
definition [llvm_code]: "euclid (a::'a::len word) b ≡ doM {
(a,b) ← llc_while
(λ(a,b) ⇒ ll_cmp (a ≠ b))
(λ(a,b) ⇒ if (a≤b) then Mreturn (a,b-a) else Mreturn (a-b,b))
(a,b);
Mreturn a
}"
export_llvm (debug)
"euclid :: 64 word ⇒ 64 word ⇒ 64 word llM" is "uint64_t euclid (uint64_t, uint64_t)"
file "code/euclid.ll"
lemma gcd_diff1': "gcd (a::int) (b-a) = gcd a b"
by (metis gcd.commute gcd_diff1)
lemma "llvm_htriple
(↿uint.assn a⇩0 ai ** ↿uint.assn b⇩0 bi ** ↑⇩d(0<a⇩0 ∧ 0<b⇩0))
(euclid ai bi)
(λri. ↿uint.assn (gcd a⇩0 b⇩0) ri)"
unfolding euclid_def
apply (rewrite annotate_llc_while[where
I="λ(ai,bi) t. EXS a b. ↿uint.assn a ai ** ↿uint.assn b bi
** ↑⇩a(t=a+b) ** ↑⇩d(0<a ∧ 0<b ∧ gcd a b = gcd a⇩0 b⇩0)"
and R="measure nat"
])
apply vcg_monadify
apply (vcg'; clarsimp?)
apply (simp_all add: gcd_diff1 gcd_diff1')
done
subsubsection ‹Fibonacci Numbers›
definition fib :: "'n::len word ⇒ 'n word llM" where [llvm_code]: "fib n ≡ REC (λfib' n.
if n≤unsigned 1 then Mreturn n
else doM {
n⇩1 ← fib' (n-unsigned 1);
n⇩2 ← fib' (n-unsigned 2);
Mreturn (n⇩1+n⇩2)
}) n"
abbreviation fib64 :: "64 word ⇒ 64 word llM" where "fib64 ≡ fib"
export_llvm thms: fib64
prepare_code_thms (LLVM) [code] fib_def
definition test :: "64 word ⇒ 64 word ⇒ _ llM"
where [llvm_code]: "test a b ≡ doM {
Mreturn (a,b)
}"
ML_val ‹
local open LLC_Preprocessor
val ctxt = @{context}
in
val thm = @{thm test_def}
|> cthm_inline ctxt
|> cthm_monadify ctxt
end
›
find_theorems llc_while
lemma "foo (test)"
unfolding test_def
apply (simp named_ss llvm_pre_simp:)
oops
export_llvm test
subsubsection ‹Distance between two Points (double)›
context begin
definition ddist :: "double × double ⇒ double × double ⇒ double llM"
where [llvm_code]: "ddist p⇩1 p⇩2 ≡ doM {
let (x⇩1,y⇩1) = p⇩1;
let (x⇩2,y⇩2) = p⇩2;
let dx = x⇩1 - x⇩2;
let dy = y⇩1 - y⇩2;
Mreturn (dsqrt ( dx*dx + dy*dy ))
}"
export_llvm ddist
interpretation llvm_prim_arith_setup .
lemma "llvm_htriple □ (ddist p⇩1 p⇩2) (λ_. □)"
unfolding ddist_def
apply (simp split: prod.split add: Let_def)
apply vcg
done
end
text ‹Example and Regression Tests using LLVM-VCG directly,
i.e., without Refinement Framework›
subsection ‹Custom and Named Structures›
typedef ('a,'b) my_pair = "UNIV :: ('a::llvm_rep × 'b::llvm_rep) set" by simp
lemmas my_pair_bij[simp] = Abs_my_pair_inverse[simplified] Rep_my_pair_inverse
instantiation my_pair :: (llvm_rep,llvm_rep)llvm_rep
begin
definition "from_val_my_pair ≡ Abs_my_pair o from_val"
definition "to_val_my_pair ≡ to_val o Rep_my_pair"
definition [simp]: "struct_of_my_pair (_:: ('a,'b)my_pair itself) ≡ struct_of TYPE('a × 'b)"
definition "init_my_pair ≡ Abs_my_pair init"
instance
apply standard
unfolding from_val_my_pair_def to_val_my_pair_def struct_of_my_pair_def init_my_pair_def
apply (auto simp: to_val_word_def init_zero)
done
end
definition "my_sel_fst ≡ fst o Rep_my_pair"
definition "my_sel_snd ≡ snd o Rep_my_pair"
lemma my_pair_to_val[ll_to_val]: "to_val x = LL_STRUCT [to_val (my_sel_fst x), to_val (my_sel_snd x)]"
by (auto simp: my_sel_fst_def my_sel_snd_def to_val_my_pair_def to_val_prod)
definition my_fst :: "('a::llvm_rep,'b::llvm_rep)my_pair ⇒ 'a llM" where [llvm_inline]: "my_fst x ≡ ll_extract_value x 0"
definition my_snd :: "('a::llvm_rep,'b::llvm_rep)my_pair ⇒ 'b llM" where [llvm_inline]: "my_snd x ≡ ll_extract_value x 1"
definition my_ins_fst :: "('a::llvm_rep,'b::llvm_rep)my_pair ⇒ 'a ⇒ ('a,'b)my_pair llM" where [llvm_inline]: "my_ins_fst x a ≡ ll_insert_value x a 0"
definition my_ins_snd :: "('a::llvm_rep,'b::llvm_rep)my_pair ⇒ 'b ⇒ ('a,'b)my_pair llM" where [llvm_inline]: "my_ins_snd x a ≡ ll_insert_value x a 1"
definition [llvm_code]: "add_add (a::_ word) ≡ doM {
x ← ll_add a a;
x ← ll_add x x;
Mreturn x
}"
definition [llvm_code]: "test_named (a::32 word) (b::64 word) ≡ doM {
a ← add_add a;
b ← add_add b;
let n = (init::(32 word,64 word)my_pair);
a ← my_fst n;
b ← my_snd n;
n ← my_ins_fst n init;
n ← my_ins_snd n init;
Mreturn b
}"
lemma my_pair_id_struct[ll_identified_structures]: "ll_is_identified_structure ''my_pair'' TYPE((_,_)my_pair)"
unfolding ll_is_identified_structure_def
apply (simp add: )
done
thm ll_identified_structures
export_llvm (debug) test_named file "code/test_named.ll"
definition test_foo :: "(64 word × 64 word ptr) ptr ⇒ 64 word ⇒ 64 word llM"
where [llvm_code]:
"test_foo a b ≡ Mreturn 0"
export_llvm test_foo is ‹int64_t test_foo(larray_t*, elem_t)›
defines ‹
typedef uint64_t elem_t;
typedef struct {
int64_t len;
elem_t *data;
} larray_t;
›
subsubsection ‹Linked List›