riscv SEAR: arch-split SEAR for clz and ctz
Signed-off-by: Mitchell Buckley <mitchell.buckley@data61.csiro.au>
This commit is contained in:
parent
f96f7763fd
commit
9cea8ed18b
|
@ -206,6 +206,8 @@ session SimplExportAndRefine in "asmrefine" = SimplExport +
|
||||||
"SEL4GraphRefine"
|
"SEL4GraphRefine"
|
||||||
|
|
||||||
session SimplExport in "asmrefine/export" = CSpec +
|
session SimplExport in "asmrefine/export" = CSpec +
|
||||||
|
directories
|
||||||
|
"$L4V_ARCH"
|
||||||
theories
|
theories
|
||||||
"SEL4SimplExport"
|
"SEL4SimplExport"
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1,31 @@
|
||||||
|
(*
|
||||||
|
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: GPL-2.0-only
|
||||||
|
*)
|
||||||
|
|
||||||
|
theory ArchSEL4SimplExport
|
||||||
|
imports "AsmRefine.SimplExport" "CSpec.Substitute"
|
||||||
|
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"
|
||||||
|
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"
|
||||||
|
apply (simp add: clzl_body_def)
|
||||||
|
apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body)
|
||||||
|
apply (clarsimp simp: bv_clz_def meq_def)
|
||||||
|
done
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
end
|
|
@ -0,0 +1,11 @@
|
||||||
|
(*
|
||||||
|
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: GPL-2.0-only
|
||||||
|
*)
|
||||||
|
|
||||||
|
theory ArchSEL4SimplExport
|
||||||
|
imports "AsmRefine.SimplExport"
|
||||||
|
begin
|
||||||
|
|
||||||
|
end
|
|
@ -5,7 +5,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory SEL4SimplExport
|
theory SEL4SimplExport
|
||||||
imports "AsmRefine.SimplExport" "CSpec.Substitute"
|
imports "ArchSEL4SimplExport" "CSpec.Substitute"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
ML \<open>
|
ML \<open>
|
||||||
|
@ -16,22 +16,6 @@ val csenv = let
|
||||||
|
|
||||||
context kernel_all_substitute 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"
|
|
||||||
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"
|
|
||||||
apply (simp add: clzl_body_def)
|
|
||||||
apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body)
|
|
||||||
apply (clarsimp simp: bv_clz_def meq_def)
|
|
||||||
done
|
|
||||||
|
|
||||||
declare ctcb_offset_defs[simp]
|
declare ctcb_offset_defs[simp]
|
||||||
|
|
||||||
ML \<open>
|
ML \<open>
|
||||||
|
@ -44,4 +28,3 @@ ML \<open>
|
||||||
end
|
end
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue