adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

c-parser: fixed testfiles to support multiple architectures

This commit is contained in:
Joel Beeren 2016-10-11 12:20:04 +11:00
parent 0dbaf71636
commit 33262e9bef
9 changed files with 106 additions and 60 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
tools/c-parser/testfiles/ARM/MachineWords.thy Normal file
View File

@ -0,0 +1,24 @@
(*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*)
theory MachineWords
imports "../../CTranslation"
begin
type_synonym machine_word_len = "32"
type_synonym machine_word = "machine_word_len word"
abbreviation "machine_word_bytes \<equiv> 4 :: nat"
lemma of_nat_machine_word_bytes[simp]: "of_nat machine_word_bytes = 4"
by simp
end

24
tools/c-parser/testfiles/X64/MachineWords.thy Normal file
View File

@ -0,0 +1,24 @@
(*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*)
theory MachineWords
imports "../../CTranslation"
begin
type_synonym machine_word_len = "64"
type_synonym machine_word = "machine_word_len word"
abbreviation "machine_word_bytes \<equiv> 8 :: nat"
lemma of_nat_machine_word_bytes[simp]: "of_nat machine_word_bytes = 8"
by simp
end

22
tools/c-parser/testfiles/factorial.c
View File

@ -11,24 +11,24 @@
/** FNSPEC alloc_spec:
"\<forall>\<sigma> k. \<Gamma> \<turnstile>
\<lbrace>\<sigma>. (free_pool k)\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__ptr_to_unsigned :== PROC alloc()
\<acute>ret__ptr_to_unsigned_long :== PROC alloc()
\<lbrace> ((\<lambda>p s. if k > 0 then (\<turnstile>\<^sub>s p \<and>\<^sup>* \<turnstile>\<^sub>s (p +\<^sub>p 1) \<and>\<^sup>*
free_pool (k - 1)) s else (free_pool k) s \<and> p = NULL) \<acute>ret__ptr_to_unsigned)\<^bsup>sep\<^esup> \<rbrace>"
free_pool (k - 1)) s else (free_pool k) s \<and> p = NULL) \<acute>ret__ptr_to_unsigned_long)\<^bsup>sep\<^esup> \<rbrace>"
*/
unsigned int *alloc(void)
unsigned long *alloc(void)
{
/* Stub */
}
/** FNSPEC free_spec:
"\<forall>\<sigma> k. \<Gamma> \<turnstile>
\<lbrace>\<sigma>. (sep_cut' (ptr_val \<acute>p) (2 * size_of TYPE(word32)) \<and>\<^sup>* free_pool k)\<^bsup>sep\<^esup> \<rbrace>
\<lbrace>\<sigma>. (sep_cut' (ptr_val \<acute>p) (2 * size_of TYPE(machine_word)) \<and>\<^sup>* free_pool k)\<^bsup>sep\<^esup> \<rbrace>
PROC free(\<acute>p)
\<lbrace> (free_pool (k + 1))\<^bsup>sep\<^esup> \<rbrace>"
*/
void free(unsigned int *p)
void free(unsigned long *p)
{
/* Stub */
}
@ -36,14 +36,14 @@ void free(unsigned int *p)
/** FNSPEC factorial_spec:
"\<forall>\<sigma> k. \<Gamma> \<turnstile>
\<lbrace>\<sigma>. (free_pool k)\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__ptr_to_unsigned :== PROC factorial(\<acute>n)
\<lbrace> if \<acute>ret__ptr_to_unsigned \<noteq> NULL then (sep_fac_list \<^bsup>\<sigma>\<^esup>n \<acute>ret__ptr_to_unsigned \<and>\<^sup>*
\<acute>ret__ptr_to_unsigned_long :== PROC factorial(\<acute>n)
\<lbrace> if \<acute>ret__ptr_to_unsigned_long \<noteq> NULL then (sep_fac_list \<^bsup>\<sigma>\<^esup>n \<acute>ret__ptr_to_unsigned_long \<and>\<^sup>*
free_pool (k - (unat \<^bsup>\<sigma>\<^esup>n + 1)))\<^bsup>sep\<^esup> \<and> (unat \<^bsup>\<sigma>\<^esup>n + 1) \<le> k else (free_pool k)\<^bsup>sep\<^esup> \<rbrace>"
*/
unsigned int *factorial(unsigned int n)
unsigned long *factorial(unsigned long n)
{
unsigned int *p, *q;
unsigned long *p, *q;
if (n == 0) {
p = alloc();
@ -69,7 +69,7 @@ unsigned int *factorial(unsigned int n)
/** INV: "\<lbrace> \<exists>xs. (sep_list xs \<acute>q \<and>\<^sup>* free_pool (k - length xs))\<^bsup>sep\<^esup> \<and>
length xs \<le> k \<rbrace>" */
{
unsigned int *k = (unsigned int *)*(q + 1);
unsigned long *k = (unsigned long *)*(q + 1);
free(q);
q = k;
@ -79,7 +79,7 @@ unsigned int *factorial(unsigned int n)
}
*p = n * *q;
*(p + 1) = (unsigned int)q;
*(p + 1) = (unsigned long)q;
return p;
}

68
tools/c-parser/testfiles/factorial.thy
View File

@ -1,5 +1,5 @@
(*
* Copyright 2014, NICTA
* Copyright 201machine_word_bytes, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
@ -9,7 +9,7 @@
*)
theory factorial
imports "../CTranslation"
imports "../CTranslation" "$L4V_ARCH/MachineWords"
begin
declare hrs_simps [simp add]
@ -18,7 +18,7 @@ declare sep_conj_ac [simp add]
consts free_pool :: "nat \<Rightarrow> heap_assert"
primrec
fac :: "nat \<Rightarrow> word32"
fac :: "nat \<Rightarrow> machine_word"
where
"fac 0 = 1"
| "fac (Suc n) = of_nat (Suc n) * fac n"
@ -40,7 +40,7 @@ lemma fac_unfold:
done
primrec
fac_list :: "nat \<Rightarrow> word32 list"
fac_list :: "nat \<Rightarrow> machine_word list"
where
"fac_list 0 = [1]"
| "fac_list (Suc n) = fac (Suc n) # fac_list n"
@ -58,7 +58,7 @@ lemma fac_list_unfold:
done
primrec
sep_list :: "word32 list \<Rightarrow> word32 ptr \<Rightarrow> heap_assert"
sep_list :: "machine_word list \<Rightarrow> machine_word ptr \<Rightarrow> heap_assert"
where
"sep_list [] p = (\<lambda>s. p=NULL \<and> \<box> s)"
| "sep_list (x#xs) p = (\<lambda>s. \<exists>j. ((p \<mapsto> x) \<and>\<^sup>* (p +\<^sub>p 1) \<mapsto> j \<and>\<^sup>*
@ -69,7 +69,7 @@ lemma sep_list_NULL [simp]:
by (case_tac xs) auto
definition
sep_fac_list :: "word32 \<Rightarrow> word32 ptr \<Rightarrow> heap_assert"
sep_fac_list :: "machine_word \<Rightarrow> machine_word ptr \<Rightarrow> heap_assert"
where
"sep_fac_list n p \<equiv> sep_list (fac_list (unat n)) p"
@ -103,7 +103,7 @@ install_C_file memsafe "factorial.c"
thm factorial_global_addresses.factorial_body_def
lemma (in factorial_global_addresses) mem_safe_alloc:
"mem_safe (\<acute>ret__ptr_to_unsigned :== PROC alloc()) \<Gamma>"
"mem_safe (\<acute>ret__ptr_to_unsigned_long :== PROC alloc()) \<Gamma>"
apply(insert alloc_impl)
apply(unfold alloc_body_def)
apply(subst mem_safe_restrict)
@ -113,10 +113,10 @@ lemma (in factorial_global_addresses) mem_safe_alloc:
done
lemma (in factorial_global_addresses) sep_frame_alloc:
"\<lbrakk> \<forall>\<sigma>. \<Gamma> \<turnstile> \<lbrace>\<sigma>. (P (f \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace> \<acute>ret__ptr_to_unsigned :== PROC alloc() \<lbrace> (Q (g \<sigma> \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>;
"\<lbrakk> \<forall>\<sigma>. \<Gamma> \<turnstile> \<lbrace>\<sigma>. (P (f \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace> \<acute>ret__ptr_to_unsigned_long :== PROC alloc() \<lbrace> (Q (g \<sigma> \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>;
htd_ind f; htd_ind g; \<forall>s. htd_ind (g s) \<rbrakk> \<Longrightarrow>
\<forall>\<sigma>. \<Gamma> \<turnstile> \<lbrace>\<sigma>. (P (f \<acute>(\<lambda>x. x)) \<and>\<^sup>* R (h \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__ptr_to_unsigned :== PROC alloc()
\<acute>ret__ptr_to_unsigned_long :== PROC alloc()
\<lbrace> (Q (g \<sigma> \<acute>(\<lambda>x. x)) \<and>\<^sup>* R (h \<sigma>))\<^bsup>sep\<^esup> \<rbrace>"
unfolding sep_app_def
by (rule sep_frame, auto intro!: mem_safe_alloc)
@ -124,9 +124,9 @@ lemma (in factorial_global_addresses) sep_frame_alloc:
lemma (in alloc_spec) alloc_spec':
shows "\<forall>\<sigma> k R f. factorial_global_addresses.\<Gamma> \<turnstile>
\<lbrace>\<sigma>. ((\<lambda>x. free_pool k) ((\<lambda>x. undefined) \<acute>(\<lambda>x. x)) \<and>\<^sup>* R (f \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__ptr_to_unsigned :== PROC alloc()
\<acute>ret__ptr_to_unsigned_long :== PROC alloc()
\<lbrace> ((\<lambda>p s. if k > 0 then (\<turnstile>\<^sub>s p \<and>\<^sup>* \<turnstile>\<^sub>s (p +\<^sub>p 1) \<and>\<^sup>*
free_pool (k - 1)) s else (free_pool k) s \<and> p = NULL) \<acute>ret__ptr_to_unsigned
free_pool (k - 1)) s else (free_pool k) s \<and> p = NULL) \<acute>ret__ptr_to_unsigned_long
\<and>\<^sup>* R (f \<sigma>))\<^bsup>sep\<^esup> \<rbrace>"
apply clarify
apply(insert alloc_spec)
@ -159,7 +159,7 @@ lemma (in factorial_global_addresses) sep_frame_free:
lemma (in free_spec) free_spec':
shows "\<forall>\<sigma> k R f. factorial_global_addresses.\<Gamma> \<turnstile>
\<lbrace>\<sigma>. ((\<lambda>p. sep_cut' (ptr_val p) (2 * size_of TYPE(word32)) \<and>\<^sup>* free_pool k) \<acute>p \<and>\<^sup>* R (f \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>
\<lbrace>\<sigma>. ((\<lambda>p. sep_cut' (ptr_val p) (2 * size_of TYPE(machine_word)) \<and>\<^sup>* free_pool k) \<acute>p \<and>\<^sup>* R (f \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>
PROC free(\<acute>p)
\<lbrace> ((\<lambda>x. free_pool (k + 1)) ((\<lambda>x. ()) \<acute>(\<lambda>x. x)) \<and>\<^sup>* R (f \<sigma>))\<^bsup>sep\<^esup> \<rbrace>"
apply clarify
@ -171,28 +171,28 @@ lemma (in free_spec) free_spec':
done
lemma double_word_sep_cut':
"(p \<mapsto> x \<and>\<^sup>* (p +\<^sub>p 1) \<mapsto> y) s \<Longrightarrow> sep_cut' (ptr_val (p::word32 ptr)) 8 s"
"(p \<mapsto> x \<and>\<^sup>* (p +\<^sub>p 1) \<mapsto> y) s \<Longrightarrow> sep_cut' (ptr_val (p::machine_word ptr)) (2*machine_word_bytes) s"
apply(clarsimp simp: sep_conj_def sep_cut'_def dest!: sep_map_dom)
apply(subgoal_tac "{ptr_val p..+4} \<subseteq> {ptr_val p..+8}")
apply(subgoal_tac "{ptr_val p+4..+4} \<subseteq> {ptr_val p..+8}")
apply(subgoal_tac "{ptr_val p..+machine_word_bytes} \<subseteq> {ptr_val p..+(2*machine_word_bytes)}")
apply(subgoal_tac "{ptr_val p+(of_nat machine_word_bytes)..+machine_word_bytes} \<subseteq> {ptr_val p..+(2*machine_word_bytes)}")
apply rule
apply fast
apply (fastforce simp: ptr_add_def)
apply clarsimp
apply(drule intvlD)
apply clarsimp
apply(case_tac "k < 4")
apply(case_tac "k < machine_word_bytes")
apply(erule intvlI)
apply(erule notE)
apply(clarsimp simp: intvl_def)
apply(rule_tac x="k - 4" in exI)
apply(rule_tac x="k - machine_word_bytes" in exI)
apply rule
apply(simp only: unat_simps)
apply(subst mod_less)
apply(simp add: addr_card)
apply simp
apply (simp add: ptr_add_def addr_card)
apply simp
apply(clarsimp simp: intvl_def)
apply(rule_tac x="4+k" in exI)
apply(rule_tac x="machine_word_bytes+k" in exI)
apply simp
apply(rule intvl_start_le)
apply simp
@ -209,11 +209,9 @@ lemma (in specs) factorial_spec:
prefer 2
apply (simp add: whileAnno_def factorial_invs_body_def)
apply(subst factorial_invs_body_def)
apply (simp only: ucast_id)
apply(unfold sep_app_def)
apply (vcg exspec=alloc_spec' exspec=free_spec')
apply (fold lift_def)
apply(clarsimp simp: sep_app_def)
apply (rule conjI)
apply clarsimp
@ -224,12 +222,12 @@ lemma (in specs) factorial_spec:
apply (rule conjI)
apply clarsimp
apply clarsimp
apply (rename_tac a b ret__ptr_to_unsigned)
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned \<and>\<^sup>* sep_true) (lift_state (a,b))")
apply (rename_tac a b ret__ptr_to_unsigned_long)
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned_long \<and>\<^sup>* sep_true) (lift_state (a,b))")
prefer 2
apply(drule sep_conj_sep_true_right)
apply simp
apply(subgoal_tac "(\<turnstile>\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \<and>\<^sup>* sep_true) (lift_state (a,b))")
apply(subgoal_tac "(\<turnstile>\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \<and>\<^sup>* sep_true) (lift_state (a,b))")
prefer 2
apply(drule sep_conj_sep_true_left)
apply simp
@ -258,18 +256,18 @@ lemma (in specs) factorial_spec:
apply(rule_tac x="fac_list (unat (n - 1))" in exI)
apply clarsimp
apply clarsimp
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned \<and>\<^sup>* sep_true) (lift_state (ab,bb))")
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned_long \<and>\<^sup>* sep_true) (lift_state (ab,bb))")
prefer 2
apply(erule (1) sep_conj_impl)
apply simp
apply(subgoal_tac "(\<turnstile>\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \<and>\<^sup>* sep_true) (lift_state (ab,bb))")
apply(subgoal_tac "(\<turnstile>\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \<and>\<^sup>* sep_true) (lift_state (ab,bb))")
prefer 2
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned \<and>\<^sup>*
\<turnstile>\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \<and>\<^sup>*
sep_fac_list (n - 1) ret__ptr_to_unsigneda \<and>\<^sup>*
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned_long \<and>\<^sup>*
\<turnstile>\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \<and>\<^sup>*
sep_fac_list (n - 1) ret__ptr_to_unsigned_longa \<and>\<^sup>*
free_pool (k - Suc (unat n))) =
(\<turnstile>\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \<and>\<^sup>* (\<turnstile>\<^sub>s ret__ptr_to_unsigned \<and>\<^sup>*
sep_fac_list (n - 1) ret__ptr_to_unsigneda \<and>\<^sup>*
(\<turnstile>\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \<and>\<^sup>* (\<turnstile>\<^sub>s ret__ptr_to_unsigned_long \<and>\<^sup>*
sep_fac_list (n - 1) ret__ptr_to_unsigned_longa \<and>\<^sup>*
free_pool (k - Suc (unat n))))")
prefer 2
apply simp
@ -282,7 +280,7 @@ lemma (in specs) factorial_spec:
apply clarsimp
apply (rule conjI, unat_arith)
apply sep_exists_tac
apply(rule_tac x="ptr_val ret__ptr_to_unsigneda" in exI)
apply(rule_tac x="ptr_val ret__ptr_to_unsigned_longa" in exI)
apply clarsimp
apply(subst fac_unfold)
apply unat_arith
@ -317,7 +315,7 @@ lemma (in specs) factorial_spec:
apply(subst (asm) sep_conj_assoc [symmetric])+
apply(erule sep_conj_impl)
apply simp
apply(erule double_word_sep_cut')
apply(erule double_word_sep_cut'[simplified])
apply assumption
apply simp
apply clarsimp
@ -330,7 +328,7 @@ lemma (in specs) factorial_spec:
declare hrs_simps [simp del]
lemma (in factorial_global_addresses) mem_safe_factorial:
shows "mem_safe (\<acute>ret__ptr_to_unsigned :== PROC factorial(\<acute>n)) \<Gamma>"
shows "mem_safe (\<acute>ret__ptr_to_unsigned_long :== PROC factorial(\<acute>n)) \<Gamma>"
apply(subst mem_safe_restrict)
apply(rule intra_mem_safe)
apply (insert factorial_impl free_impl alloc_impl)

4
tools/c-parser/testfiles/kmalloc.thy
View File

@ -9,14 +9,14 @@
*)
theory kmalloc
imports "../CTranslation"
imports "../CTranslation" "$L4V_ARCH/MachineWords"
begin
(* no proof here, just testing the parser *)
consts
KMC :: word32
ptr_retyps :: "nat \<Rightarrow> word32 \<Rightarrow> heap_typ_desc \<Rightarrow> heap_typ_desc"
ptr_retyps :: "nat \<Rightarrow> machine_word \<Rightarrow> heap_typ_desc \<Rightarrow> heap_typ_desc"
install_C_file "kmalloc.c"

8
tools/c-parser/testfiles/list_reverse.c
View File

@ -8,16 +8,16 @@
* @TAG(NICTA_BSD)
*/
typedef unsigned int word_t;
typedef unsigned long word_t;
/** FNSPEC reverse_spec:
"\<Gamma> \<turnstile>
\<lbrace> (list zs \<acute>i)\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__int :== PROC reverse(\<acute>i)
\<lbrace> (list (rev zs) (Ptr (scast \<acute>ret__int)))\<^bsup>sep\<^esup> \<rbrace>"
\<acute>ret__long :== PROC reverse(\<acute>i)
\<lbrace> (list (rev zs) (Ptr (scast \<acute>ret__long)))\<^bsup>sep\<^esup> \<rbrace>"
*/
int reverse(word_t *i)
long reverse(word_t *i)
{
word_t j = 0;

4
tools/c-parser/testfiles/list_reverse.thy
View File

@ -9,7 +9,7 @@
*)
theory list_reverse
imports "../CTranslation"
imports "../CTranslation" "$L4V_ARCH/MachineWords"
begin
declare hrs_simps [simp add]
@ -17,7 +17,7 @@ declare exists_left [simp add]
declare sep_conj_ac [simp add]
primrec
list :: "word32 list \<Rightarrow> word32 ptr \<Rightarrow> heap_state \<Rightarrow> bool"
list :: "machine_word list \<Rightarrow> machine_word ptr \<Rightarrow> heap_state \<Rightarrow> bool"
where
"list [] i = (\<lambda>s. i=NULL \<and> \<box> s)"
| "list (x#xs) i = (\<lambda>s. i=Ptr x \<and> x\<noteq>0 \<and> (\<exists>j. ((i \<mapsto> j) \<and>\<^sup>* list xs (Ptr j)) s))"

6
tools/c-parser/testfiles/list_reverse_norm.c
View File

@ -8,13 +8,13 @@
* @TAG(NICTA_BSD)
*/
typedef unsigned int word_t;
typedef unsigned long word_t;
/** FNSPEC reverse_spec:
"\<Gamma> \<turnstile>
\<lbrace> list (lift_t_c \<zeta>) zs \<acute>i \<rbrace>
\<acute>ret__unsigned :== PROC reverse(\<acute>i)
\<lbrace> list (lift_t_c \<zeta>) (rev zs) (Ptr \<acute>ret__unsigned) \<rbrace>"
\<acute>ret__unsigned_long :== PROC reverse(\<acute>i)
\<lbrace> list (lift_t_c \<zeta>) (rev zs) (Ptr \<acute>ret__unsigned_long) \<rbrace>"
*/

6
tools/c-parser/testfiles/list_reverse_norm.thy
View File

@ -9,14 +9,14 @@
*)
theory list_reverse_norm
imports "../CTranslation"
imports "../CTranslation" "$L4V_ARCH/MachineWords"
begin
declare sep_conj_ac [simp add]
declare hrs_simps [simp add]
primrec
list :: "word32 typ_heap \<Rightarrow> word32 list \<Rightarrow> word32 ptr \<Rightarrow> bool"
list :: "machine_word typ_heap \<Rightarrow> machine_word list \<Rightarrow> machine_word ptr \<Rightarrow> bool"
where
"list h [] i = (i = Ptr 0)"
@ -63,7 +63,7 @@ lemma in_list_Some:
lemma in_list_valid [simp]:
"\<lbrakk> list (lift_t_c (h,d)) xs p; ptr_val q \<in> set xs \<rbrakk>
\<Longrightarrow> d \<Turnstile>\<^sub>t (q::word32 ptr)"
\<Longrightarrow> d \<Turnstile>\<^sub>t (q::machine_word ptr)"
by (auto dest: in_list_Some simp: lift_t_if split: split_if_asm)
lemma list_restrict: