x64 abstract/machine: introduce and use FPUNullState
The FPU state is opaque, and its null state is not necessary an array of zeroes. Instead, the null state is a snapshot taken after initialisation.
This commit is contained in:
parent
f20ec59695
commit
8744fb20d7
|
@ -108,7 +108,7 @@ definition
|
||||||
|
|
||||||
definition
|
definition
|
||||||
new_context :: "user_context" where
|
new_context :: "user_context" where
|
||||||
"new_context \<equiv> UserContext (\<lambda>r. 0) ((\<lambda>r. 0)(CS := selCS3, SS := selDS3, FLAGS := 0x202))"
|
"new_context \<equiv> UserContext FPUNullState ((\<lambda>r. 0)(CS := selCS3, SS := selDS3, FLAGS := 0x202))"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
pptr_base :: "machine_word" where
|
pptr_base :: "machine_word" where
|
||||||
|
|
|
@ -20,7 +20,7 @@ context Arch begin global_naming X64_H
|
||||||
definition
|
definition
|
||||||
newContext :: "user_context"
|
newContext :: "user_context"
|
||||||
where
|
where
|
||||||
"newContext \<equiv> UserContext (\<lambda>w. 0) ((K 0) aLU initContext)"
|
"newContext \<equiv> UserContext FPUNullState ((K 0) aLU initContext)"
|
||||||
|
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
|
|
|
@ -265,6 +265,9 @@ definition
|
||||||
where
|
where
|
||||||
"setFPUState fc \<equiv> modify (\<lambda>s. UserContext fc (user_regs s))"
|
"setFPUState fc \<equiv> modify (\<lambda>s. UserContext fc (user_regs s))"
|
||||||
|
|
||||||
|
(* The FPU state is opaque; the null state is a constant snapshot taken after initialisation *)
|
||||||
|
consts'
|
||||||
|
FPUNullState :: fpu_state
|
||||||
|
|
||||||
consts'
|
consts'
|
||||||
initL2Cache_impl :: "unit machine_rest_monad"
|
initL2Cache_impl :: "unit machine_rest_monad"
|
||||||
|
|
Loading…
Reference in New Issue