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

x64: create arch-specific CKernel

This commit is contained in:
Matthew Brecknell 2017-06-22 17:06:30 +10:00
parent 8ce2a86cb7
commit ce748b7522
14 changed files with 87 additions and 120 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
.gitignore vendored
View File

@ -7,16 +7,16 @@
*.lev *.lev
*#*# *#*#
/spec/cspec/c/32/ /spec/cspec/*/c/32/
/spec/cspec/c/64/ /spec/cspec/*/c/64/
/spec/cspec/c/api/ /spec/cspec/*/c/api/
/spec/cspec/c/arch/ /spec/cspec/*/c/arch/
/spec/cspec/c/kernel_all.c /spec/cspec/*/c/kernel_all.c
/spec/cspec/c/kernel_all.c_pp /spec/cspec/*/c/kernel_all.c_pp
/spec/cspec/c/parsetab.py /spec/cspec/*/c/parsetab.py
/spec/cspec/c/plat/ /spec/cspec/*/c/plat/
/spec/cspec/c/sources_list_updated /spec/cspec/*/c/sources_list_updated
/spec/cspec/c/autoconf.h /spec/cspec/*/c/autoconf.h
/spec/haskell/doc/**/*.aux /spec/haskell/doc/**/*.aux
/spec/haskell/doc/**/*.bbl /spec/haskell/doc/**/*.bbl

40
.licenseignore
View File

@ -70,27 +70,27 @@ spec/haskell/src/SEL4/Object/IOPort/X64.lhs-boot
spec/design/version spec/design/version
spec/cspec/c/32/* spec/cspec/*/c/32/*
spec/cspec/c/64/* spec/cspec/*/c/64/*
spec/cspec/c/api/* spec/cspec/*/c/api/*
spec/cspec/c/arch/* spec/cspec/*/c/arch/*
spec/cspec/c/kernel_all.c spec/cspec/*/c/kernel_all.c
spec/cspec/c/kernel_all.c_pp spec/cspec/*/c/kernel_all.c_pp
spec/cspec/c/parsetab.py spec/cspec/*/c/parsetab.py
spec/cspec/c/plat/* spec/cspec/*/c/plat/*
spec/cspec/c/sources_list_updated spec/cspec/*/c/sources_list_updated
spec/cspec/c/autoconf.h spec/cspec/*/c/autoconf.h
spec/cspec/c/arch/object/structures_defs.thy spec/cspec/*/c/arch/object/structures_defs.thy
spec/cspec/c/arch/object/structures_proofs.thy spec/cspec/*/c/arch/object/structures_proofs.thy
spec/cspec/c/arch/api/shared_types_defs.thy spec/cspec/*/c/arch/api/shared_types_defs.thy
spec/cspec/c/arch/api/shared_types_proofs.thy spec/cspec/*/c/arch/api/shared_types_proofs.thy
spec/cspec/c/32/mode/api/shared_types_defs.thy spec/cspec/*/c/32/mode/api/shared_types_defs.thy
spec/cspec/c/32/mode/api/shared_types_proofs.thy spec/cspec/*/c/32/mode/api/shared_types_proofs.thy
spec/cspec/c/plat/machine/hardware_proofs.thy spec/cspec/*/c/plat/machine/hardware_proofs.thy
spec/cspec/c/plat/machine/hardware_defs.thy spec/cspec/*/c/plat/machine/hardware_defs.thy
spec/cspec/c/api/types_proofs.thy spec/cspec/*/c/api/types_proofs.thy
spec/cspec/c/api/types_defs.thy spec/cspec/*/c/api/types_defs.thy
tools/c-parser/Simpl/SyntaxTest.thy tools/c-parser/Simpl/SyntaxTest.thy
tools/c-parser/Simpl/HoareTotalProps.thy tools/c-parser/Simpl/HoareTotalProps.thy

2
proof/tests.xml
View File

@ -28,7 +28,7 @@
<!-- CRefine --> <!-- CRefine -->
<sequence depends="CParser"> <sequence depends="CParser">
<test name="CKernel" cpu-timeout="10800">make CKernel</test> <test name="CKernel" cpu-timeout="14400">make CKernel</test>
<test name="CSpec" cpu-timeout="7200">make CSpec</test> <test name="CSpec" cpu-timeout="7200">make CSpec</test>
<test name="CBaseRefine" depends="Refine" cpu-timeout="28800">make CBaseRefine</test> <test name="CBaseRefine" depends="Refine" cpu-timeout="28800">make CBaseRefine</test>
<test name="CRefine" cpu-timeout="28800">make CRefine</test> <test name="CRefine" cpu-timeout="28800">make CRefine</test>

2
run_tests
View File

@ -33,7 +33,7 @@ echo "Testing for L4V_ARCH=${L4V_ARCH}:"
# Run the tests from the script directory. # Run the tests from the script directory.
cd ${DIR} cd ${DIR}
default="ASpec ExecSpec AInvs SpecCheck HaskellKernel BaseRefine Refine Licenses" default="ASpec ExecSpec AInvs SpecCheck HaskellKernel BaseRefine Refine Licenses CKernel"
if [ "${bamboo_l4v_regression_identifier}" == "test board" ] if [ "${bamboo_l4v_regression_identifier}" == "test board" ]
then then
bamboo_args=$(echo "$@" | ( [ -z "${bamboo_l4v_regression_options}" ] && cat - || sed 's/'"${bamboo_l4v_regression_options}"'//')) bamboo_args=$(echo "$@" | ( [ -z "${bamboo_l4v_regression_options}" ] && cat - || sed 's/'"${bamboo_l4v_regression_options}"'//'))

5
spec/Makefile
View File

@ -37,7 +37,7 @@ spec-check: .FORCE
# Preprocess the kernel's source code and bitfield theory files. # Preprocess the kernel's source code and bitfield theory files.
c-kernel: .FORCE c-kernel: .FORCE
cd cspec/c && L4V_REPO_PATH=$(L4V_REPO_PATH) $(MAKE) cspec cd cspec/$(L4V_ARCH)/c && L4V_REPO_PATH=$(L4V_REPO_PATH) $(MAKE) cspec
.PHONY: c-kernel .PHONY: c-kernel
# Produce the input data for the binary verification problem at -O1 # Produce the input data for the binary verification problem at -O1
@ -49,7 +49,8 @@ binary-verification-input: c-kernel
# Clean # Clean
clean: clean:
rm -rf abstract/generated rm -rf abstract/generated
cd cspec/c && $(MAKE) clean SKIP_PATH_CHECKS=1 cd cspec/$(L4V_ARCH)/c && $(MAKE) clean SKIP_PATH_CHECKS=1
rm -f cspec/$(L4V_ARCH)/umm_types.txt
rm -f umm_types.txt rm -f umm_types.txt
.PHONY: clean .PHONY: clean

12
spec/ROOT
View File

@ -76,18 +76,18 @@ session ExecSpec = Word_Lib +
session CSpec = CKernel + session CSpec = CKernel +
theories [condition = "SORRY_BITFIELD_PROOFS", quick_and_dirty] theories [condition = "SORRY_BITFIELD_PROOFS", quick_and_dirty]
"cspec/KernelInc_C" "cspec/$L4V_ARCH/KernelInc_C"
theories theories
"cspec/KernelInc_C" "cspec/$L4V_ARCH/KernelInc_C"
"cspec/KernelState_C" "cspec/$L4V_ARCH/KernelState_C"
session CKernel = CParser + session CKernel = CParser +
theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty] theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty]
"cspec/Kernel_C" "cspec/$L4V_ARCH/Kernel_C"
theories theories
"cspec/Kernel_C" "cspec/$L4V_ARCH/Kernel_C"
files files
"cspec/c/kernel_all.c_pp" "cspec/$L4V_ARCH/c/kernel_all.c_pp"
session SimplExport = CSpec + session SimplExport = CSpec +
theories "cspec/SimplExport" theories "cspec/SimplExport"

2
spec/cspec/KernelInc_C.thy → spec/cspec/X64/KernelInc_C.thy
View File

@ -11,7 +11,7 @@
theory KernelInc_C theory KernelInc_C
imports imports
Kernel_C Kernel_C
Substitute "../Substitute"
"c/arch/object/structures_defs" "c/arch/object/structures_defs"
"c/arch/object/structures_proofs" "c/arch/object/structures_proofs"
"c/32/mode/api/shared_types_defs" "c/32/mode/api/shared_types_defs"

6
spec/cspec/KernelState_C.thy → spec/cspec/X64/KernelState_C.thy
View File

@ -10,10 +10,10 @@
theory KernelState_C theory KernelState_C
imports imports
"../../lib/$L4V_ARCH/WordSetup" "../../../lib/$L4V_ARCH/WordSetup"
"../../lib/BitFieldProofsLib" "../../../lib/BitFieldProofsLib"
Kernel_C Kernel_C
Substitute "../Substitute"
begin begin
type_synonym c_ptr_name = int type_synonym c_ptr_name = int

48
spec/cspec/Kernel_C.thy → spec/cspec/X64/Kernel_C.thy
View File

@ -10,9 +10,9 @@
theory Kernel_C theory Kernel_C
imports imports
"../machine/$L4V_ARCH/MachineTypes" "../../machine/$L4V_ARCH/MachineTypes"
"../../lib/CTranslationNICTA" "../../../lib/CTranslationNICTA"
"../../tools/asmrefine/CommonOps" "../../../tools/asmrefine/CommonOps"
begin begin
declare Char_eq_Char_iff [simp del] declare Char_eq_Char_iff [simp del]
@ -32,13 +32,13 @@ type_synonym cghost_state = "(machine_word \<rightharpoonup> vmpage_size) * (mac
* ghost_assertions" * ghost_assertions"
definition definition
gs_clear_region :: "word32 \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where gs_clear_region :: "addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
"gs_clear_region ptr bits gs \<equiv> "gs_clear_region ptr bits gs \<equiv>
(%x. if x \<in> {ptr..+2 ^ bits} then None else fst gs x, (%x. if x \<in> {ptr..+2 ^ bits} then None else fst gs x,
%x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd gs) x, snd (snd gs))" %x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd gs) x, snd (snd gs))"
definition definition
gs_new_frames:: "vmpage_size \<Rightarrow> word32 \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" gs_new_frames:: "vmpage_size \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
where where
"gs_new_frames sz ptr bits \<equiv> \<lambda>gs. "gs_new_frames sz ptr bits \<equiv> \<lambda>gs.
if bits < pageBitsForSize sz then gs if bits < pageBitsForSize sz then gs
@ -47,7 +47,7 @@ definition
else fst gs x, snd gs)" else fst gs x, snd gs)"
definition definition
gs_new_cnodes:: "nat \<Rightarrow> word32 \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" gs_new_cnodes:: "nat \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
where where
"gs_new_cnodes sz ptr bits \<equiv> \<lambda>gs. "gs_new_cnodes sz ptr bits \<equiv> \<lambda>gs.
if bits < sz + 4 then gs if bits < sz + 4 then gs
@ -56,12 +56,12 @@ definition
else fst (snd gs) x, snd (snd gs))" else fst (snd gs) x, snd (snd gs))"
abbreviation abbreviation
gs_get_assn :: "int \<Rightarrow> cghost_state \<Rightarrow> word32" gs_get_assn :: "int \<Rightarrow> cghost_state \<Rightarrow> machine_word"
where where
"gs_get_assn k \<equiv> ghost_assertion_data_get k (snd o snd)" "gs_get_assn k \<equiv> ghost_assertion_data_get k (snd o snd)"
abbreviation abbreviation
gs_set_assn :: "int \<Rightarrow> word32 \<Rightarrow> cghost_state \<Rightarrow> cghost_state" gs_set_assn :: "int \<Rightarrow> machine_word \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
where where
"gs_set_assn k v \<equiv> ghost_assertion_data_set k v (apsnd o apsnd)" "gs_set_assn k v \<equiv> ghost_assertion_data_set k v (apsnd o apsnd)"
@ -70,36 +70,24 @@ declare [[allow_underscore_idents = true]]
end end
(* workaround for the fact that the C parser wants to know the vmpage sizes*) (* x86-64 asm statements are not yet supported by the c-parser *)
setup {* Context.theory_map (ASM_Ignore_Hooks.add_hook (fn _ => true)) *}
(* create appropriately qualified aliases *)
context begin interpretation Arch . global_naming vmpage_size context begin interpretation Arch . global_naming vmpage_size
requalify_consts X64SmallPage X64LargePage X64HugePage
requalify_consts ARMSmallPage ARMLargePage ARMSection ARMSuperSection
end end
install_C_file "c/kernel_all.c_pp" install_C_file "c/kernel_all.c_pp"
[machinety=machine_state, ghostty=cghost_state] [machinety=machine_state, ghostty=cghost_state]
(* hide them again *) hide_const
vmpage_size.X64SmallPage
vmpage_size.X64LargePage
vmpage_size.X64HugePage
hide_const context Arch begin
vmpage_size.ARMSmallPage global_naming "X64.vmpage_size" requalify_consts X64SmallPage X64LargePage X64HugePage
vmpage_size.ARMLargePage global_naming "X64" requalify_consts X64SmallPage X64LargePage X64HugePage
vmpage_size.ARMSection
vmpage_size.ARMSuperSection
(* re-allow fully qualified accesses (for consistency). Slightly clunky *)
context Arch begin
global_naming "ARM.vmpage_size"
requalify_consts ARMSmallPage ARMLargePage ARMSection ARMSuperSection
global_naming ARM
requalify_consts ARMSmallPage ARMLargePage ARMSection ARMSuperSection
end end
end end

40
spec/cspec/c/Makefile → spec/cspec/X64/c/Makefile
View File

@ -9,40 +9,17 @@
# #
# Config makefile for building sel4 within the l4.verified repository # Config makefile for building sel4 within the l4.verified repository
SOURCE_ROOT=../../../../seL4 SOURCE_ROOT=../../../../../seL4
UMM_TYPES=../../umm_types.txt UMM_TYPES=../umm_types.txt
PARSERPATH=../../../tools/c-parser/standalone-parser PARSERPATH=../../../../tools/c-parser/standalone-parser
PATH:=${PARSERPATH}:${PATH} PATH:=${PARSERPATH}:${PATH}
export PATH export PATH
SHELL=bash SHELL=bash
ifeq ($(L4V_ARCH),ARM) ARCH=x86
ARCH=arm SEL4_ARCH=x86_64
ARMV=armv7-a PLAT=pc99
PLAT=imx6 CONFIG_DOMAIN_SCHEDULE=config_sched.c
CPU=cortex-a9
CONFIG_DOMAIN_SCHEDULE=config_arm.c
TOOLPREFIX ?= arm-none-eabi-
endif
ifeq ($(L4V_ARCH),ARM_HYP)
ARCH=arm
ARMV=armv7-a
PLAT=tk1
CPU=cortex-a15
CONFIG_DOMAIN_SCHEDULE=config_arm.c
TOOLPREFIX ?= arm-none-eabi-
endif
ifeq ($(L4V_ARCH),X64)
ARCH=x86
SEL4_ARCH=x86_64
PLAT=pc99
endif
ifndef ARCH
$(error Bad value for L4V_ARCH)
endif
ifeq ($(shell which ${TOOLPREFIX}cpp),) ifeq ($(shell which ${TOOLPREFIX}cpp),)
ifeq ($(shell which cpp),) ifeq ($(shell which cpp),)
@ -52,6 +29,7 @@ ifeq ($(shell which ${TOOLPREFIX}cpp),)
TOOLPREFIX := TOOLPREFIX :=
endif endif
endif endif
# modifies are produced by the parser # modifies are produced by the parser
SKIP_MODIFIES=1 SKIP_MODIFIES=1
FASTPATH=yes FASTPATH=yes
@ -64,7 +42,7 @@ cspec: kernel_all.c_pp ${UMM_TYPES} theories
# Create "umm_types" if necessary. # Create "umm_types" if necessary.
${UMM_TYPES}: kernel_all.c_pp ${UMM_TYPES}: kernel_all.c_pp
python mk_umm_types.py --root $(L4V_REPO_PATH) $< $@ python ../../mk_umm_types.py --root $(L4V_REPO_PATH) $< $@
include ${SOURCE_ROOT}/Makefile include ${SOURCE_ROOT}/Makefile

0
spec/cspec/c/config_arm.c → spec/cspec/X64/c/config_sched.c
View File

0
spec/cspec/c/mk_umm_types.py → spec/cspec/mk_umm_types.py
View File

16
tools/asmrefine/CommonOps.thy
View File

@ -55,11 +55,11 @@ definition
"mem_upd mem addr v = heap_update (Ptr addr) v mem" "mem_upd mem addr v = heap_update (Ptr addr) v mem"
definition definition
"store_word32 (addr :: word32) (w :: word32) "store_word32 (addr :: addr) (w :: word32)
= heap_update_list addr (rev (word_rsplit w))" = heap_update_list addr (rev (word_rsplit w))"
definition definition
"load_word32 (addr :: word32) memory "load_word32 (addr :: addr) memory
= (word_rcat (rev (heap_list memory 4 addr)) :: word32)" = (word_rcat (rev (heap_list memory 4 addr)) :: word32)"
definition definition
@ -79,7 +79,7 @@ where
(msb x \<noteq> msb y) \<and> (msb x \<noteq> msb (x + y + cinw)))" (msb x \<noteq> msb y) \<and> (msb x \<noteq> msb (x + y + cinw)))"
definition definition
all_htd_updates :: "('a :: c_type) itself \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> word32 all_htd_updates :: "('a :: c_type) itself \<Rightarrow> word32 \<Rightarrow> addr \<Rightarrow> word32
\<Rightarrow> heap_typ_desc \<Rightarrow> heap_typ_desc" \<Rightarrow> heap_typ_desc \<Rightarrow> heap_typ_desc"
where where
"all_htd_updates (tp :: ('a :: c_type) itself) x y z "all_htd_updates (tp :: ('a :: c_type) itself) x y z
@ -91,17 +91,17 @@ where
else if x = 4 then ptr_arr_retyps (unat z) (Ptr y :: 'a ptr) else if x = 4 then ptr_arr_retyps (unat z) (Ptr y :: 'a ptr)
else ptr_arr_retyps (2 ^ unat z) (Ptr y :: 'a ptr))" else ptr_arr_retyps (2 ^ unat z) (Ptr y :: 'a ptr))"
type_synonym ghost_assertions = "word64 \<Rightarrow> word32" type_synonym ghost_assertions = "int \<Rightarrow> addr"
definition definition
ghost_assertion_data_get :: "int \<Rightarrow> ('a \<Rightarrow> ghost_assertions) \<Rightarrow> 'a \<Rightarrow> word32" ghost_assertion_data_get :: "int \<Rightarrow> ('a \<Rightarrow> ghost_assertions) \<Rightarrow> 'a \<Rightarrow> addr"
where where
"ghost_assertion_data_get k acc s = (acc s) (word_of_int k)" "ghost_assertion_data_get k acc s = (acc s) k"
definition definition
ghost_assertion_data_set :: "int \<Rightarrow> word32 \<Rightarrow> ((ghost_assertions \<Rightarrow> ghost_assertions) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ghost_assertion_data_set :: "int \<Rightarrow> addr \<Rightarrow> ((ghost_assertions \<Rightarrow> ghost_assertions) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
where where
"ghost_assertion_data_set k v upd = upd (\<lambda>f. f (word_of_int k := v))" "ghost_assertion_data_set k v upd = upd (\<lambda>f. f (k := v))"
definition definition
"pvalid htd (v :: ('a :: c_type) itself) x = h_t_valid htd c_guard (Ptr x :: 'a ptr)" "pvalid htd (v :: ('a :: c_type) itself) x = h_t_valid htd c_guard (Ptr x :: 'a ptr)"

14
tools/asmrefine/GlobalsSwap.thy
View File

@ -16,11 +16,11 @@ imports
begin begin
datatype 'g global_data = datatype 'g global_data =
GlobalData "string" "nat" "word32 \<Rightarrow> bool" "'g \<Rightarrow> word8 list" GlobalData "string" "nat" "addr \<Rightarrow> bool" "'g \<Rightarrow> word8 list"
"word8 list \<Rightarrow> 'g \<Rightarrow> 'g" "word8 list \<Rightarrow> 'g \<Rightarrow> 'g"
| ConstGlobalData "string" "nat" "word32 \<Rightarrow> bool" | ConstGlobalData "string" "nat" "addr \<Rightarrow> bool"
"word8 list" "word8 list \<Rightarrow> bool" "word8 list" "word8 list \<Rightarrow> bool"
| AddressedGlobalData "string" "nat" "word32 \<Rightarrow> bool" | AddressedGlobalData "string" "nat" "addr \<Rightarrow> bool"
(* in each case the symbol name, length in bytes, tag and constraint on (* in each case the symbol name, length in bytes, tag and constraint on
address. for active globals a getter/setter, for const globals address. for active globals a getter/setter, for const globals
a sample value and a way to check a value *) a sample value and a way to check a value *)
@ -70,7 +70,7 @@ type_synonym 'g hrs_update = "(heap_raw_state \<Rightarrow> heap_raw_state) \<Ri
definition definition
global_swap :: "('g \<Rightarrow> heap_raw_state) \<Rightarrow> 'g hrs_update global_swap :: "('g \<Rightarrow> heap_raw_state) \<Rightarrow> 'g hrs_update
\<Rightarrow> (string \<Rightarrow> word32) \<Rightarrow> 'g global_data \<Rightarrow> 'g \<Rightarrow> 'g" \<Rightarrow> (string \<Rightarrow> addr) \<Rightarrow> 'g global_data \<Rightarrow> 'g \<Rightarrow> 'g"
where where
"global_swap g_hrs g_hrs_upd symtab gd \<equiv> "global_swap g_hrs g_hrs_upd symtab gd \<equiv>
(case gd of GlobalData name len n g p \<Rightarrow> \<lambda>gs. (case gd of GlobalData name len n g p \<Rightarrow> \<lambda>gs.
@ -82,7 +82,7 @@ where
definition definition
globals_swap :: "('g \<Rightarrow> heap_raw_state) \<Rightarrow> 'g hrs_update globals_swap :: "('g \<Rightarrow> heap_raw_state) \<Rightarrow> 'g hrs_update
\<Rightarrow> (string \<Rightarrow> word32) \<Rightarrow> 'g global_data list \<Rightarrow> 'g \<Rightarrow> 'g" \<Rightarrow> (string \<Rightarrow> addr) \<Rightarrow> 'g global_data list \<Rightarrow> 'g \<Rightarrow> 'g"
where where
"globals_swap g_hrs g_hrs_upd symtab gds "globals_swap g_hrs g_hrs_upd symtab gds
= foldr (global_swap g_hrs g_hrs_upd symtab) gds" = foldr (global_swap g_hrs g_hrs_upd symtab) gds"
@ -217,7 +217,7 @@ lemma hrs_htd_globals_swap:
lemmas foldr_hrs_htd_global_swap = hrs_htd_globals_swap[unfolded globals_swap_def] lemmas foldr_hrs_htd_global_swap = hrs_htd_globals_swap[unfolded globals_swap_def]
definition definition
globals_list_distinct :: "word32 set \<Rightarrow> (string \<Rightarrow> word32) globals_list_distinct :: "addr set \<Rightarrow> (string \<Rightarrow> addr)
\<Rightarrow> 'g global_data list \<Rightarrow> bool" \<Rightarrow> 'g global_data list \<Rightarrow> bool"
where where
"globals_list_distinct D symtab gds = distinct_prop (\<lambda>S T. S \<inter> T = {}) "globals_list_distinct D symtab gds = distinct_prop (\<lambda>S T. S \<inter> T = {})
@ -605,7 +605,7 @@ lemma globals_list_valid_optimisation:
by blast by blast
definition definition
const_globals_in_memory :: "(string \<Rightarrow> word32) \<Rightarrow> 'g global_data list const_globals_in_memory :: "(string \<Rightarrow> addr) \<Rightarrow> 'g global_data list
\<Rightarrow> heap_mem \<Rightarrow> bool" \<Rightarrow> heap_mem \<Rightarrow> bool"
where where
"const_globals_in_memory symtab xs hmem = "const_globals_in_memory symtab xs hmem =