Theory Ownership_Split_Exec

theory Ownership_Split_Exec
  imports
    Exec_DG_State
    "Voblint_Framework.DG_Ownership_Split_Spec"
    "Voblint_Framework.Routed_Context"
begin

unbundle default_st_syntax

section ‹The ownership-splitting analysis at the executable carrier›

text ‹
  \<^const>‹ownership_split_transfer_gen› asks only that a carrier can merge a local and a
  global half and project each back out. The association-list carrier answers
  with \<^const>‹combine_default_st› and the two ‹restrict_…_default_st›
  projections, so the executable analysis is that transfer at those three
  arguments -- not a second definition of what the analysis does.
›

definition ownership_split_transfer_st ::
  "('x,'k,unit,'a::bounded_semilattice_sup_bot default_st,'a default_st) man_transfer
   ⇒ ('x,'k,unit,'a default_st,'a default_st) man_transfer"
where
  "ownership_split_transfer_st =
     ownership_split_transfer_gen combine_default_st restrict_global_default_st restrict_local_default_st"

text ‹
  Entry is the same wrapping one step up in arity: it answers a list of
  caller-continuation/callee-entry pairs rather than one successor value, so the
  executable carrier supplies the same three operations to
  \<^const>‹ownership_split_enter_transfer_gen›.
›

definition ownership_split_enter_transfer_st ::
  "('x,'k,unit,'a::bounded_semilattice_sup_bot default_st,'a default_st) man_enter_transfer
   ⇒ ('x,'k,unit,'a default_st,'a default_st) man_enter_transfer"
where
  "ownership_split_enter_transfer_st =
     ownership_split_enter_transfer_gen combine_default_st restrict_global_default_st
       restrict_local_default_st"

text ‹
  The callee exit reaches the wrapped stage merged against the same shared fact,
  like the caller continuation. The return slot is read off it at the classifier's
  own location for \<^const>‹ret_var›; that name is local, so the merge leaves it
  at the callee's own value.
›

definition ownership_split_combine_transfer_st ::
  "(vname ⇒ bool) ⇒ call_info
   ⇒ ('x,'k,unit,'a::bounded_semilattice_sup_bot default_st,'a default_st) man_combine_transfer"
where
  "ownership_split_combine_transfer_st 𝒢 ci =
     ownership_split_combine_transfer_gen combine_default_st restrict_global_default_st
       restrict_local_default_st
       (local_combine_transfer
          (λenv de. combine_assign_default_st 𝒢 (ci_dst ci)
                      de⟨location_of 𝒢 ret_var⟩ env))"

definition ownership_split_dg_spec_st_for ::
  "(vname ⇒ bool)
   ⇒ (edge_action ⇒ 'a::bounded_semilattice_sup_bot default_st ⇒ 'a default_st)
   ⇒ (call_info ⇒ 'a default_st ⇒ 'a default_st)
   ⇒ ('x,'k,unit,'a default_st,'a default_st) dg_spec"
where
  "ownership_split_dg_spec_st_for 𝒢 tf_st enter_st = local_dg_spec_template⦇
     dgs_skip := ownership_split_transfer_st (local_transfer (tf_st EA_Nop)),
     dgs_assign := (λx e. ownership_split_transfer_st (local_transfer (tf_st (EA_Assign x e)))),
     dgs_special := (λsc x. ownership_split_transfer_st (local_transfer (tf_st (EA_Special sc x)))),
     dgs_branch := (λb pol. ownership_split_transfer_st
                      (local_transfer (tf_st (if pol then EA_Assume b else EA_AssumeNot b)))),
     dgs_body := (λp. ownership_split_transfer_st (local_transfer (tf_st (EA_Body p)))),
     dgs_return := (λe p. ownership_split_transfer_st (local_transfer (tf_st (EA_Ret e p)))),
     dgs_enter := (λci. ownership_split_enter_transfer_st
                          (local_enter_transfer (λd. [(d, enter_st ci d)]))),
     dgs_event := (λev. case ev of Check_Event l bc
                     ⇒ ownership_split_transfer_st (local_transfer (tf_st (EA_Check l bc)))),
     dgs_combine_assign := ownership_split_combine_transfer_st 𝒢 ⦈"

unbundle no default_st_syntax

end