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

riscv: fix CLZ and CTZ for riscv32 builds (#257) 

This commit verifies seL4 PR [#325][], which fixes the riscv32 build
broken by seL4 commit [9ec5df5f][].

[#325]: https://github.com/seL4/seL4/pull/325
[9ec5df5]: https://github.com/seL4/seL4/commit/9ec5df5f

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
This commit is contained in:
Matthew Brecknell 2021-03-30 13:17:41 +11:00 committed by GitHub
parent 7983107b71
commit d020be3b89
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 14 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
proof/asmrefine/export/ARM/ArchSEL4SimplExport.thy
View File

@ -11,16 +11,16 @@ begin
context kernel_all_substitute begin
lemma ctzl_body_refines:
"simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x \<noteq> 0\<rbrace>
(\<acute>ret__long :== ucast (bv_ctz (\<acute>x)))) ctzl_body"
"simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x___unsigned_long \<noteq> 0\<rbrace>
(\<acute>ret__long :== ucast (bv_ctz (\<acute>x___unsigned_long)))) ctzl_body"
apply (simp add: ctzl_body_def)
apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body)
apply (clarsimp simp: bv_ctz_def meq_def)
done
lemma clzl_body_refines:
"simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x \<noteq> 0\<rbrace>
(\<acute>ret__long :== ucast (bv_clz (\<acute>x)))) clzl_body"
"simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x___unsigned_long \<noteq> 0\<rbrace>
(\<acute>ret__long :== ucast (bv_clz (\<acute>x___unsigned_long)))) clzl_body"
apply (simp add: clzl_body_def)
apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body)
apply (clarsimp simp: bv_clz_def meq_def)

4
proof/crefine/ARM/IpcCancel_C.thy
View File

@ -1927,8 +1927,8 @@ lemma ksReadyQueuesL1Bitmap_word_log2_max:
by (fastforce dest: word_log2_nth_same bitmapQ_no_L1_orphansD)
lemma clzl_spec:
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call clzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_clz (x_' s)) \<rbrace>"
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x___unsigned_long_' s \<noteq> 0} Call clzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_clz (x___unsigned_long_' s))\<rbrace>"
apply (rule allI, rule conseqPre, vcg)
apply clarsimp
apply (rule_tac x="ret__long_'_update f x" for f in exI)

4
proof/crefine/ARM_HYP/IpcCancel_C.thy
View File

@ -2108,8 +2108,8 @@ lemma ksReadyQueuesL2Bitmap_nonzeroI:
done
lemma clzl_spec:
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call clzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_clz (x_' s)) \<rbrace>"
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x___unsigned_long_' s \<noteq> 0} Call clzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_clz (x___unsigned_long_' s))\<rbrace>"
apply (rule allI, rule conseqPre, vcg)
apply clarsimp
apply (rule_tac x="ret__long_'_update f x" for f in exI)

4
proof/crefine/ARM_HYP/Syscall_C.thy
View File

@ -1645,8 +1645,8 @@ lemma ucast_maxIRQ_is_not_less:
(* FIXME ARMHYP: move *)
lemma ctzl_spec:
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call ctzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_ctz (x_' s)) \<rbrace>"
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x___unsigned_long_' s \<noteq> 0} Call ctzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_ctz (x___unsigned_long_' s)) \<rbrace>"
apply (rule allI, rule conseqPre, vcg)
apply clarsimp
apply (rule_tac x="ret__long_'_update f x" for f in exI)

4
proof/crefine/X64/IpcCancel_C.thy
View File

@ -2119,8 +2119,8 @@ lemma ksReadyQueuesL2Bitmap_nonzeroI:
done
lemma clzl_spec:
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call clzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_clz (x_' s)) \<rbrace>"
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x___unsigned_long_' s \<noteq> 0} Call clzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_clz (x___unsigned_long_' s))\<rbrace>"
apply (rule allI, rule conseqPre, vcg)
apply clarsimp
apply (rule_tac x="ret__long_'_update f x" for f in exI)

4
proof/crefine/X64/Syscall_C.thy
View File

@ -1595,8 +1595,8 @@ lemma ucast_maxIRQ_is_not_less:
(* FIXME ARMHYP: move *)
lemma ctzl_spec:
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call ctzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_ctz (x_' s)) \<rbrace>"
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x___unsigned_long_' s \<noteq> 0} Call ctzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_ctz (x___unsigned_long_' s)) \<rbrace>"
apply (rule allI, rule conseqPre, vcg)
apply clarsimp
apply (rule_tac x="ret__long_'_update f x" for f in exI)