forked from afp-mirror/Core_DOM
259 lines
14 KiB
Plaintext
259 lines
14 KiB
Plaintext
(***********************************************************************************
|
|
* Copyright (c) 2016-2018 The University of Sheffield, UK
|
|
*
|
|
* All rights reserved.
|
|
*
|
|
* Redistribution and use in source and binary forms, with or without
|
|
* modification, are permitted provided that the following conditions are met:
|
|
*
|
|
* * Redistributions of source code must retain the above copyright notice, this
|
|
* list of conditions and the following disclaimer.
|
|
*
|
|
* * Redistributions in binary form must reproduce the above copyright notice,
|
|
* this list of conditions and the following disclaimer in the documentation
|
|
* and/or other materials provided with the distribution.
|
|
*
|
|
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
|
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
|
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
|
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
|
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
|
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
|
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
|
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
|
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
|
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
|
*
|
|
* SPDX-License-Identifier: BSD-2-Clause
|
|
***********************************************************************************)
|
|
|
|
section\<open>Object\<close>
|
|
text\<open>In this theory, we introduce the monadic method setup for the Object class.\<close>
|
|
theory ObjectMonad
|
|
imports
|
|
BaseMonad
|
|
"../classes/ObjectClass"
|
|
begin
|
|
|
|
type_synonym ('object_ptr, 'Object, 'result) dom_prog
|
|
= "((_) heap, exception, 'result) prog"
|
|
register_default_tvars "('object_ptr, 'Object, 'result) dom_prog"
|
|
|
|
global_interpretation l_ptr_kinds_M object_ptr_kinds defines object_ptr_kinds_M = a_ptr_kinds_M .
|
|
lemmas object_ptr_kinds_M_defs = a_ptr_kinds_M_def
|
|
|
|
|
|
global_interpretation l_dummy defines get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t = "l_get_M.a_get_M get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t" .
|
|
lemma get_M_is_l_get_M: "l_get_M get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t type_wf object_ptr_kinds"
|
|
by (simp add: a_type_wf_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf l_get_M_def)
|
|
lemmas get_M_defs = get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def[unfolded l_get_M.a_get_M_def[OF get_M_is_l_get_M]]
|
|
|
|
adhoc_overloading get_M get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
|
|
|
|
locale l_get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas = l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
|
|
begin
|
|
interpretation l_get_M get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t type_wf object_ptr_kinds
|
|
apply(unfold_locales)
|
|
apply (simp add: get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf local.type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t)
|
|
by (simp add: a_type_wf_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf)
|
|
lemmas get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ok = get_M_ok[folded get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def]
|
|
lemmas get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ptr_in_heap = get_M_ptr_in_heap[folded get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def]
|
|
end
|
|
|
|
global_interpretation l_get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas type_wf
|
|
by (simp add: l_get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas_def l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_axioms)
|
|
|
|
lemma object_ptr_kinds_M_reads:
|
|
"reads (\<Union>object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) object_ptr_kinds_M h h'"
|
|
apply(auto simp add: object_ptr_kinds_M_defs get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf type_wf_defs reads_def
|
|
preserved_def get_M_defs
|
|
split: option.splits)[1]
|
|
using a_type_wf_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf by blast+
|
|
|
|
|
|
global_interpretation l_put_M type_wf object_ptr_kinds get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
|
|
rewrites "a_get_M = get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t"
|
|
defines put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t = a_put_M
|
|
apply (simp add: get_M_is_l_get_M l_put_M_def)
|
|
by (simp add: get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def)
|
|
lemmas put_M_defs = a_put_M_def
|
|
adhoc_overloading put_M put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
|
|
|
|
|
|
locale l_put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas = l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
|
|
begin
|
|
interpretation l_put_M type_wf object_ptr_kinds get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
|
|
apply(unfold_locales)
|
|
using get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t.type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t local.l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_axioms apply blast
|
|
by (simp add: a_type_wf_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf)
|
|
lemmas put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ok = put_M_ok[folded put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def]
|
|
lemmas put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ptr_in_heap = put_M_ptr_in_heap[folded put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def]
|
|
end
|
|
|
|
global_interpretation l_put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas type_wf
|
|
by (simp add: l_put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas_def l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_axioms)
|
|
|
|
|
|
definition check_in_heap :: "(_) object_ptr \<Rightarrow> (_, unit) dom_prog"
|
|
where
|
|
"check_in_heap ptr = do {
|
|
h \<leftarrow> get_heap;
|
|
(if ptr |\<in>| object_ptr_kinds h then
|
|
return ()
|
|
else
|
|
error SegmentationFault
|
|
)}"
|
|
|
|
lemma check_in_heap_ptr_in_heap: "ptr |\<in>| object_ptr_kinds h \<longleftrightarrow> h \<turnstile> ok (check_in_heap ptr)"
|
|
by(auto simp add: check_in_heap_def)
|
|
lemma check_in_heap_pure [simp]: "pure (check_in_heap ptr) h"
|
|
by(auto simp add: check_in_heap_def intro!: bind_pure_I)
|
|
lemma check_in_heap_is_OK [simp]:
|
|
"ptr |\<in>| object_ptr_kinds h \<Longrightarrow> h \<turnstile> ok (check_in_heap ptr \<bind> f) = h \<turnstile> ok (f ())"
|
|
by(simp add: check_in_heap_def)
|
|
lemma check_in_heap_returns_result [simp]:
|
|
"ptr |\<in>| object_ptr_kinds h \<Longrightarrow> h \<turnstile> (check_in_heap ptr \<bind> f) \<rightarrow>\<^sub>r x = h \<turnstile> f () \<rightarrow>\<^sub>r x"
|
|
by(simp add: check_in_heap_def)
|
|
lemma check_in_heap_returns_heap [simp]:
|
|
"ptr |\<in>| object_ptr_kinds h \<Longrightarrow> h \<turnstile> (check_in_heap ptr \<bind> f) \<rightarrow>\<^sub>h h' = h \<turnstile> f () \<rightarrow>\<^sub>h h'"
|
|
by(simp add: check_in_heap_def)
|
|
|
|
lemma check_in_heap_reads:
|
|
"reads {preserved (get_M object_ptr nothing)} (check_in_heap object_ptr) h h'"
|
|
apply(simp add: check_in_heap_def reads_def preserved_def)
|
|
by (metis a_type_wf_def get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ok get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ptr_in_heap is_OK_returns_result_E
|
|
is_OK_returns_result_I unit_all_impI)
|
|
|
|
subsection\<open>Invoke\<close>
|
|
|
|
fun invoke_rec :: "(((_) object_ptr \<Rightarrow> bool) \<times> ((_) object_ptr \<Rightarrow> 'args
|
|
\<Rightarrow> (_, 'result) dom_prog)) list \<Rightarrow> (_) object_ptr \<Rightarrow> 'args
|
|
\<Rightarrow> (_, 'result) dom_prog"
|
|
where
|
|
"invoke_rec ((P, f)#xs) ptr args = (if P ptr then f ptr args else invoke_rec xs ptr args)"
|
|
| "invoke_rec [] ptr args = error InvokeError"
|
|
|
|
definition invoke :: "(((_) object_ptr \<Rightarrow> bool) \<times> ((_) object_ptr \<Rightarrow> 'args
|
|
\<Rightarrow> (_, 'result) dom_prog)) list
|
|
\<Rightarrow> (_) object_ptr \<Rightarrow> 'args \<Rightarrow> (_, 'result) dom_prog"
|
|
where
|
|
"invoke xs ptr args = do { check_in_heap ptr; invoke_rec xs ptr args}"
|
|
|
|
lemma invoke_split: "P (invoke ((Pred, f) # xs) ptr args) =
|
|
((\<not>(Pred ptr) \<longrightarrow> P (invoke xs ptr args))
|
|
\<and> (Pred ptr \<longrightarrow> P (do {check_in_heap ptr; f ptr args})))"
|
|
by(simp add: invoke_def)
|
|
|
|
lemma invoke_split_asm: "P (invoke ((Pred, f) # xs) ptr args) =
|
|
(\<not>((\<not>(Pred ptr) \<and> (\<not> P (invoke xs ptr args)))
|
|
\<or> (Pred ptr \<and> (\<not> P (do {check_in_heap ptr; f ptr args})))))"
|
|
by(simp add: invoke_def)
|
|
lemmas invoke_splits = invoke_split invoke_split_asm
|
|
|
|
lemma invoke_ptr_in_heap: "h \<turnstile> ok (invoke xs ptr args) \<Longrightarrow> ptr |\<in>| object_ptr_kinds h"
|
|
by (metis bind_is_OK_E check_in_heap_ptr_in_heap invoke_def is_OK_returns_heap_I)
|
|
|
|
lemma invoke_pure [simp]: "pure (invoke [] ptr args) h"
|
|
by(auto simp add: invoke_def intro!: bind_pure_I)
|
|
|
|
lemma invoke_is_OK [simp]:
|
|
"ptr |\<in>| object_ptr_kinds h \<Longrightarrow> Pred ptr
|
|
\<Longrightarrow> h \<turnstile> ok (invoke ((Pred, f) # xs) ptr args) = h \<turnstile> ok (f ptr args)"
|
|
by(simp add: invoke_def)
|
|
lemma invoke_returns_result [simp]:
|
|
"ptr |\<in>| object_ptr_kinds h \<Longrightarrow> Pred ptr
|
|
\<Longrightarrow> h \<turnstile> (invoke ((Pred, f) # xs) ptr args) \<rightarrow>\<^sub>r x = h \<turnstile> f ptr args \<rightarrow>\<^sub>r x"
|
|
by(simp add: invoke_def)
|
|
lemma invoke_returns_heap [simp]:
|
|
"ptr |\<in>| object_ptr_kinds h \<Longrightarrow> Pred ptr
|
|
\<Longrightarrow> h \<turnstile> (invoke ((Pred, f) # xs) ptr args) \<rightarrow>\<^sub>h h' = h \<turnstile> f ptr args \<rightarrow>\<^sub>h h'"
|
|
by(simp add: invoke_def)
|
|
|
|
lemma invoke_not [simp]: "\<not>Pred ptr \<Longrightarrow> invoke ((Pred, f) # xs) ptr args = invoke xs ptr args"
|
|
by(auto simp add: invoke_def)
|
|
|
|
lemma invoke_empty [simp]: "\<not>h \<turnstile> ok (invoke [] ptr args)"
|
|
by(auto simp add: invoke_def check_in_heap_def)
|
|
|
|
lemma invoke_empty_reads [simp]: "\<forall>P \<in> S. reflp P \<and> transp P \<Longrightarrow> reads S (invoke [] ptr args) h h'"
|
|
apply(simp add: invoke_def reads_def preserved_def)
|
|
by (meson bind_returns_result_E error_returns_result)
|
|
|
|
|
|
subsection\<open>Modified Heaps\<close>
|
|
|
|
lemma get_object_ptr_simp [simp]:
|
|
"get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h) = (if ptr = object_ptr then Some obj else get object_ptr h)"
|
|
by(auto simp add: get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: option.splits Option.bind_splits)
|
|
|
|
lemma object_ptr_kinds_simp [simp]: "object_ptr_kinds (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h) = object_ptr_kinds h |\<union>| {|ptr|}"
|
|
by(auto simp add: object_ptr_kinds_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: option.splits)
|
|
|
|
lemma type_wf_put_I:
|
|
assumes "type_wf h"
|
|
shows "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
|
|
using assms
|
|
by(auto simp add: type_wf_defs split: option.splits)
|
|
|
|
lemma type_wf_put_ptr_not_in_heap_E:
|
|
assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
|
|
assumes "ptr |\<notin>| object_ptr_kinds h"
|
|
shows "type_wf h"
|
|
using assms
|
|
by(auto simp add: type_wf_defs split: option.splits if_splits)
|
|
|
|
lemma type_wf_put_ptr_in_heap_E:
|
|
assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
|
|
assumes "ptr |\<in>| object_ptr_kinds h"
|
|
shows "type_wf h"
|
|
using assms
|
|
by(auto simp add: type_wf_defs split: option.splits if_splits)
|
|
|
|
|
|
subsection\<open>Preserving Types\<close>
|
|
|
|
lemma type_wf_preserved: "type_wf h = type_wf h'"
|
|
by(auto simp add: type_wf_defs)
|
|
|
|
|
|
lemma object_ptr_kinds_preserved_small:
|
|
assumes "\<And>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
|
|
shows "object_ptr_kinds h = object_ptr_kinds h'"
|
|
using assms
|
|
apply(auto simp add: object_ptr_kinds_def preserved_def get_M_defs get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
|
|
split: option.splits)[1]
|
|
apply (metis (mono_tags, lifting) domIff error_returns_result fmdom.rep_eq fmember.rep_eq
|
|
old.unit.exhaust option.case_eq_if return_returns_result)
|
|
by (metis (mono_tags, lifting) domIff error_returns_result fmdom.rep_eq fmember.rep_eq
|
|
old.unit.exhaust option.case_eq_if return_returns_result)
|
|
|
|
lemma object_ptr_kinds_preserved:
|
|
assumes "writes SW setter h h'"
|
|
assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
|
|
assumes "\<And>h h' w object_ptr. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h'
|
|
\<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
|
|
shows "object_ptr_kinds h = object_ptr_kinds h'"
|
|
proof -
|
|
{
|
|
fix object_ptr w
|
|
have "preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
|
|
apply(rule writes_small_big[OF assms])
|
|
by auto
|
|
}
|
|
then show ?thesis
|
|
using object_ptr_kinds_preserved_small by blast
|
|
qed
|
|
|
|
|
|
lemma reads_writes_preserved2:
|
|
assumes "writes SW setter h h'"
|
|
assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
|
|
assumes "\<And>h h' x. \<forall>w \<in> SW. h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr getter) h h'"
|
|
shows "preserved (get_M ptr getter) h h'"
|
|
apply(clarsimp simp add: preserved_def)
|
|
using reads_singleton assms(1) assms(2)
|
|
apply(rule reads_writes_preserved)
|
|
using assms(3)
|
|
by(auto simp add: preserved_def)
|
|
end
|