asmrefine: remove globals_swap ref
Using a shared ref for configuration reduces the understandability of code. It turns out the contents of the `globals_swap` ref: 1. Was always the same. 2. Was only used in one spot. 3. Could be recreated at that one spot. So we do that instead.
This commit is contained in:
parent
b4242a3ae8
commit
9ba1d498df
|
@ -46,10 +46,6 @@ local_setup \<open>
|
||||||
|
|
||||||
context graph_refine_locale begin
|
context graph_refine_locale begin
|
||||||
|
|
||||||
ML \<open>
|
|
||||||
SimplToGraphProof.globals_swap
|
|
||||||
:= (fn t => @{term "globals_swap t_hrs_' t_hrs_'_update symbol_table globals_list"} $ t)
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
local_setup \<open>
|
local_setup \<open>
|
||||||
add_globals_swap_rewrites @{thms kernel_all_global_addresses.global_data_mems}
|
add_globals_swap_rewrites @{thms kernel_all_global_addresses.global_data_mems}
|
||||||
|
|
|
@ -45,8 +45,6 @@ local_setup \<open>
|
||||||
context graph_refine_locale begin
|
context graph_refine_locale begin
|
||||||
|
|
||||||
ML \<open>
|
ML \<open>
|
||||||
SimplToGraphProof.globals_swap
|
|
||||||
:= (fn t => @{term "globals_swap t_hrs_' t_hrs_'_update symbol_table globals_list"} $ t)
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
local_setup \<open>
|
local_setup \<open>
|
||||||
|
|
|
@ -1799,8 +1799,6 @@ structure SimplToGraphProof = struct
|
||||||
fun mk_ptr_val_app p =
|
fun mk_ptr_val_app p =
|
||||||
Const (@{const_name ptr_val}, fastype_of p --> @{typ word32}) $ p
|
Const (@{const_name ptr_val}, fastype_of p --> @{typ word32}) $ p
|
||||||
|
|
||||||
val globals_swap = ref (fn (x : term) => x)
|
|
||||||
|
|
||||||
fun mk_arr_idx arr i = let
|
fun mk_arr_idx arr i = let
|
||||||
val arrT = fastype_of arr
|
val arrT = fastype_of arr
|
||||||
val elT = case arrT of Type (@{type_name "array"}, [elT, _])
|
val elT = case arrT of Type (@{type_name "array"}, [elT, _])
|
||||||
|
@ -1815,13 +1813,24 @@ val gammaT_to_stateT = strip_type #> snd
|
||||||
|
|
||||||
fun mk_simpl_acc ctxt sT nm = let
|
fun mk_simpl_acc ctxt sT nm = let
|
||||||
val sst = Free ("sst", sT)
|
val sst = Free ("sst", sT)
|
||||||
val globals_sst = Syntax.read_term ctxt "globals :: globals myvars \<Rightarrow> _"
|
val symbol_table = Free ("symbol_table", @{typ "string => machine_word"})
|
||||||
$ sst
|
|
||||||
|
val [globals, globals_swap, t_hrs, t_hrs_update, globals_list, pms, pms_encode] =
|
||||||
|
map (Syntax.read_term ctxt) [
|
||||||
|
"globals :: globals myvars \<Rightarrow> _",
|
||||||
|
"globals_swap :: (globals \<Rightarrow> _) \<Rightarrow> _",
|
||||||
|
"t_hrs_' :: globals \<Rightarrow> _",
|
||||||
|
"t_hrs_'_update :: _ \<Rightarrow> globals \<Rightarrow> globals",
|
||||||
|
"globals_list",
|
||||||
|
"phantom_machine_state_' :: globals \<Rightarrow> _",
|
||||||
|
"encode_machine_state"
|
||||||
|
];
|
||||||
|
|
||||||
|
val globals_sst = globals $ sst
|
||||||
val _ = type_of globals_sst (* does type checking *)
|
val _ = type_of globals_sst (* does type checking *)
|
||||||
|
|
||||||
val t_hrs = Syntax.read_term ctxt "t_hrs_' :: globals \<Rightarrow> _"
|
val globals_swap = globals_swap $ t_hrs $ t_hrs_update $ symbol_table $ globals_list
|
||||||
val pms = Syntax.read_term ctxt "phantom_machine_state_' :: globals \<Rightarrow> _"
|
|
||||||
val pms_encode = Syntax.read_term ctxt "encode_machine_state"
|
|
||||||
fun do_pms_encode t = case pms_encode of Const _ => pms_encode $ t
|
fun do_pms_encode t = case pms_encode of Const _ => pms_encode $ t
|
||||||
| _ => raise TERM ("mk_simpl_acc: requires `encode_machine_state :: machine_state => unit \<times> nat'", [t])
|
| _ => raise TERM ("mk_simpl_acc: requires `encode_machine_state :: machine_state => unit \<times> nat'", [t])
|
||||||
|
|
||||||
|
@ -1829,7 +1838,7 @@ fun mk_simpl_acc ctxt sT nm = let
|
||||||
fun get_ghost_assns_fetch () = case head_of ghost_assns_fetch of Const _ => ghost_assns_fetch
|
fun get_ghost_assns_fetch () = case head_of ghost_assns_fetch of Const _ => ghost_assns_fetch
|
||||||
| _ => raise TERM ("mk_simpl_acc: requires `ghost_assns_from_globals :: globals => word64 => word32", [])
|
| _ => raise TERM ("mk_simpl_acc: requires `ghost_assns_from_globals :: globals => word64 => word32", [])
|
||||||
|
|
||||||
fun mk_sst_acc "Mem" = @{term hrs_mem} $ (t_hrs $ ((! globals_swap) globals_sst))
|
fun mk_sst_acc "Mem" = @{term hrs_mem} $ (t_hrs $ (globals_swap $ globals_sst))
|
||||||
| mk_sst_acc "HTD" = @{term hrs_htd} $ (t_hrs $ globals_sst)
|
| mk_sst_acc "HTD" = @{term hrs_htd} $ (t_hrs $ globals_sst)
|
||||||
| mk_sst_acc "PMS" = do_pms_encode (pms $ globals_sst)
|
| mk_sst_acc "PMS" = do_pms_encode (pms $ globals_sst)
|
||||||
| mk_sst_acc "GhostAssertions" = get_ghost_assns_fetch () $ globals_sst
|
| mk_sst_acc "GhostAssertions" = get_ghost_assns_fetch () $ globals_sst
|
||||||
|
|
|
@ -123,10 +123,6 @@ local_setup \<open>add_field_h_val_rewrites #> add_field_to_bytes_rewrites\<clos
|
||||||
|
|
||||||
context graph_refine begin
|
context graph_refine begin
|
||||||
|
|
||||||
ML \<open>SimplToGraphProof.globals_swap
|
|
||||||
:= (fn t => @{term "globals_swap t_hrs_' t_hrs_'_update symbol_table globals_list"} $ t)
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
local_setup \<open>add_globals_swap_rewrites @{thms global_array_swap_global_addresses.global_data_mems}\<close>
|
local_setup \<open>add_globals_swap_rewrites @{thms global_array_swap_global_addresses.global_data_mems}\<close>
|
||||||
|
|
||||||
definition
|
definition
|
||||||
|
|
|
@ -123,10 +123,6 @@ local_setup \<open>add_field_h_val_rewrites #> add_field_to_bytes_rewrites\<clos
|
||||||
|
|
||||||
context g_asm_graph_refine begin
|
context g_asm_graph_refine begin
|
||||||
|
|
||||||
ML \<open>SimplToGraphProof.globals_swap
|
|
||||||
:= (fn t => @{term "globals_swap t_hrs_' t_hrs_'_update symbol_table globals_list"} $ t)
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
local_setup \<open>add_globals_swap_rewrites @{thms global_asm_stmt_global_addresses.global_data_mems}\<close>
|
local_setup \<open>add_globals_swap_rewrites @{thms global_asm_stmt_global_addresses.global_data_mems}\<close>
|
||||||
|
|
||||||
definition
|
definition
|
||||||
|
|
|
@ -123,10 +123,6 @@ local_setup \<open>add_field_h_val_rewrites #> add_field_to_bytes_rewrites\<clos
|
||||||
|
|
||||||
context graph_refine begin
|
context graph_refine begin
|
||||||
|
|
||||||
ML \<open>SimplToGraphProof.globals_swap
|
|
||||||
:= (fn t => @{term "globals_swap t_hrs_' t_hrs_'_update symbol_table globals_list"} $ t)
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
local_setup \<open>add_globals_swap_rewrites @{thms inf_loop_global_addresses.global_data_mems}\<close>
|
local_setup \<open>add_globals_swap_rewrites @{thms inf_loop_global_addresses.global_data_mems}\<close>
|
||||||
|
|
||||||
definition
|
definition
|
||||||
|
|
Loading…
Reference in New Issue