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

abstract: remove two obsolete functions

This commit is contained in:
Gerwin Klein 2017-02-10 10:55:28 +11:00
parent a40d6986fd
commit 82ab5500a1
2 changed files with 0 additions and 55 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
proof/invariant-abstract/Tcb_AI.thy
View File

@ -129,40 +129,6 @@ lemma restart_tcb[wp]:
"\<lbrace>tcb_at t'\<rbrace> Tcb_A.restart t \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>"
by (simp add: tcb_at_typ, wp restart_typ_at)
lemma copyAreaToRegs_typ_at:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> copyAreaToRegs regs a b \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
apply (simp add: copyAreaToRegs_def)
apply (wp thread_set_typ_at mapM_wp')
done
lemma copyAreaToRegs_tcb'[wp]:
"\<lbrace>tcb_at t\<rbrace> copyAreaToRegs regs a b \<lbrace>\<lambda>rv. tcb_at t\<rbrace>"
by (simp add: tcb_at_typ, wp copyAreaToRegs_typ_at)
lemma copyRegsToArea_typ_at:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> copyRegsToArea regs a b \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
apply (simp add: copyRegsToArea_def)
apply (wpsimp wp: zipWithM_x_inv)
done
lemma copyRegsToArea_tcb'[wp]:
"\<lbrace>tcb_at t\<rbrace> copyRegsToArea regs a b \<lbrace>\<lambda>rv. tcb_at t\<rbrace>"
by (simp add: tcb_at_typ, wp copyRegsToArea_typ_at)
lemma copyRegsToArea_invs[wp]:
"\<lbrace>invs\<rbrace> copyRegsToArea regs a b \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: copyRegsToArea_def)
apply (wpsimp wp: zipWithM_x_inv)
done
lemma copyAreaToRegs_invs[wp]:
"\<lbrace>invs and tcb_at b\<rbrace> copyAreaToRegs regs a b \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: copyAreaToRegs_def)
apply (wpsimp wp: mapM_wp' thread_set_invs_trivial simp: tcb_cap_cases_def)
done
lemmas suspend_tcb_at[wp] = tcb_at_typ_at [OF suspend_typ_at]

21
spec/abstract/Tcb_A.thy
View File

@ -276,25 +276,4 @@ definition
return (take (unat (mi_length info)) $ cpu_mrs @ buf_mrs)
od"
text {* Copy a set of registers from a thread to memory and vice versa. *}
definition
copyRegsToArea :: "register list \<Rightarrow> obj_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
"copyRegsToArea regs thread ptr \<equiv> do
context \<leftarrow> thread_get (arch_tcb_context_get o tcb_arch) thread;
zipWithM_x (store_word_offs ptr)
[0 ..< length regs]
(map context regs)
od"
definition
copyAreaToRegs :: "register list \<Rightarrow> obj_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
"copyAreaToRegs regs ptr thread \<equiv> do
old_regs \<leftarrow> thread_get (arch_tcb_context_get o tcb_arch) thread;
vals \<leftarrow> mapM (load_word_offs ptr) [0 ..< length regs];
vals2 \<leftarrow> return $ zip vals regs;
vals3 \<leftarrow> return $ map (\<lambda>(v, r). (sanitiseRegister r v, r)) vals2;
new_regs \<leftarrow> return $ foldl (\<lambda>rs (v, r). rs ( r := v )) old_regs vals3;
thread_set (\<lambda>tcb. tcb \<lparr> tcb_arch := arch_tcb_context_set new_regs (tcb_arch tcb) \<rparr>) thread
od"
end