Theory Voblint_Result.Analysis_Surface

theory Analysis_Surface
  imports
    "Voblint_Framework.Solved_Table"
    "Voblint_Framework.Check_Report"
    "Voblint_Compile.Compile_Invariants"
begin

section ‹The surface a solved table publishes›

text ‹
  What every domain, at every solver discipline and context policy, ends up
  publishing about a whole program: the state its solved table (an
  ‹solved_table›) holds at a point under a context, and the check report read
  off those states. ‹analysis_surface› states both once, generically in the
  domain ‹'a› and the context type ‹'c›, so a domain's public API is one
  interpretation rather than a rewritten copy per domain, solver discipline and
  policy. A context-insensitive run reads it at the one context ‹()›.
›

text ‹
  An interpretation publishes the complete surface for a solved table. Solver
  disciplines therefore share one construction and cannot accidentally expose
  only a subset of the result and report operations.

  \<^const>‹bot› at an \<^const>‹Bot› point is the reading every existing report function
  already makes: nothing reaches the point, so no store does, and \<^const>‹bot› is the
  abstract state whose concretisation is empty.
›

text ‹
  ‹bot_state› is a parameter rather than the \<^class>‹order_bot› class operation, and that is
  a code-generation requirement, not a stylistic choice. A sort constraint here would make
  the surface's code equation polymorphic in ‹'a::order_bot›, and generating code for it at
  an abstract state --- a function type \<^typ>‹String.literal ⇒ 'b› --- would demand an
  executable \<^const>‹bot› arity for that function type, which needs the domain to be
  \<^class>‹enum›. \<^typ>‹String.literal› is not. Taking the element as a parameter keeps the
  equation free of sorts; every interpretation still passes \<^const>‹bot›, where the concrete
  instance is executable exactly as it was before.
›

locale analysis_surface =
  fixes table :: "imp_prog ⇒ ('c, 'a) solved_table"
    and bot_state :: 'a
    and classify :: "exp ⇒ 'a ⇒ check_result"
begin

definition state_at :: "imp_prog ⇒ 'c ⇒ pp ⇒ 'a" where
  "state_at p ctx v =
     (case lookup_table (table p) v ctx of Bot ⇒ bot_state | Lifted st ⇒ st)"

definition report :: "imp_prog ⇒ 'c ⇒ check_report_entry list" where
  "report p ctx = classify_checks (prog_cfg p) (state_at p ctx) classify"

text ‹
  The same table read with its \<^const>‹Bot› entries kept visible: ‹True› marks a
  point whose entry in ‹table› is \<^const>‹Bot›, which a report consumer suppresses
  instead of printing the bottom state's vacuous verdict. Exact for the same reason
  \<^const>‹state_at› is -- it is the \<^const>‹lookup_table› case split itself, not a
  second test on the raw unknown (‹fst_reach_state_at› states exactly that).

  The flag is a fact about the table and nothing more. This locale assumes nothing
  whatever about ‹table›, so it cannot and does not say that such a point is one no
  solver covered, or one no concrete run reaches. A caller wanting either reading owes
  it from its own soundness theorem about the table it supplies.
›

definition reach_state_at :: "imp_prog ⇒ 'c ⇒ pp ⇒ bool × 'a" where
  "reach_state_at p ctx v =
     (case lookup_table (table p) v ctx of
        Bot ⇒ (True, bot_state) | Lifted st ⇒ (False, st))"

text ‹
  The two readings agree on the state: ‹reach_state_at› adds a column and changes no
  verdict, so a report that shows reachability classifies exactly what
  \<^const>‹report› does. Without this the two definitions are only visibly similar,
  and every caller reproves it by unfolding both.
›

lemma state_at_Bot [simp]:
  "lookup_table (table p) v ctx = Bot ⟹ state_at p ctx v = bot_state"
  by (simp add: state_at_def)

lemma state_at_Lifted [simp]:
  "lookup_table (table p) v ctx = Lifted st ⟹ state_at p ctx v = st"
  by (simp add: state_at_def)

lemma reach_state_at_Bot [simp]:
  "lookup_table (table p) v ctx = Bot ⟹ reach_state_at p ctx v = (True, bot_state)"
  by (simp add: reach_state_at_def)

lemma reach_state_at_Lifted [simp]:
  "lookup_table (table p) v ctx = Lifted st ⟹ reach_state_at p ctx v = (False, st)"
  by (simp add: reach_state_at_def)

lemma snd_reach_state_at [simp]:
  "snd (reach_state_at p ctx v) = state_at p ctx v"
  by (simp add: reach_state_at_def state_at_def split: lifted.splits)

lemma fst_reach_state_at [simp]:
  "fst (reach_state_at p ctx v) = (lookup_table (table p) v ctx = Bot)"
  by (simp add: reach_state_at_def split: lifted.splits)

definition report_with_state ::
  "imp_prog ⇒ 'c ⇒ (pp × exp × check_result × bool × 'a) list" where
  "report_with_state p ctx =
     classify_checks_with_state (prog_cfg p) (reach_state_at p ctx)
       (λc (_, s). classify c s)"

end

text ‹
  Register the generic surface equations outside the locale so code generation can
  call them directly with the table, bottom state and classifier as parameters.
›

declare
  analysis_surface.state_at_def [code]
  analysis_surface.report_def [code]
  analysis_surface.reach_state_at_def [code]
  analysis_surface.report_with_state_def [code]

end