Theory Analysis_Query

theory Analysis_Query
  imports "Voblint_Domain.Query_Lift" "Voblint_Domain.Int_Lattice"
begin

unbundle lattice_syntax

section ‹Queries one analysis answers for another›

text ‹
  An analysis in a combination may ask its partners a question about the stores the
  current state describes, as a Goblint transfer asks ‹man.ask›. What an answer
  claims is fixed by one relation, ‹answer_holds q a s›: answer ‹a› to query ‹q›
  is true of store ‹s›. Answers form a meet-semilattice with top, as Goblint's
  per-query result lattices do (‹queries.ml› at ‹5320a6b7›): ‹⊤› claims
  nothing, and ‹⊓› combines what several analyses answered. The two laws below
  are all a combination needs to trust a combined answer; associativity and
  commutativity of the combination come from the class.
›

locale query_algebra =
  fixes answer_holds :: "'q ⇒ 'r::{semilattice_inf, order_top} ⇒ store ⇒ bool"
  assumes top_sound: "answer_holds q ⊤ s"
      and inf_sound: "⟦answer_holds q a s; answer_holds q b s⟧ ⟹ answer_holds q (a ⊓ b) s"
begin

text ‹
  A channel answers every query. It holds at a store when each of its answers
  is true there. Component transfers are proved against this predicate, never
  against a particular partner.
›

definition channel_holds :: "('q ⇒ 'r) ⇒ store ⇒ bool" where
  "channel_holds ch s ⟷ (∀q. answer_holds q (ch q) s)"

lemma channel_holdsD: "channel_holds ch s ⟹ answer_holds q (ch q) s"
  by (simp add: channel_holds_def)

lemma channel_holds_top [simp, intro]: "channel_holds (λ_. ⊤) s"
  by (simp add: channel_holds_def top_sound)

lemma channel_holds_inf [intro]:
  "channel_holds ch⇩₁ s ⟹ channel_holds ch⇩₂ s ⟹ channel_holds (λq. ch⇩₁ q ⊓ ch⇩₂ q) s"
  by (simp add: channel_holds_def inf_sound)

end

section ‹The value of an expression›

text ‹
  Version 1 has one query kind, Goblint's ‹EvalInt›: which integers an
  expression may evaluate to (‹queries.ml› line 108 at ‹0dc12d355›). Goblint
  answers it in ‹Lattice.Lift(IntDomTuple)›, and so does Voblint: the answer
  is an \<^typ>‹int_dom› under \<^typ>‹'a query_lift›. A comparison or logical
  operator evaluates to ‹0› or ‹1›, so its truth is the exact answer ‹1› or
  ‹0›; Goblint derives its former ‹MustBeEqual› and ‹MayBeLess› queries from
  ‹EvalInt› the same way (lines 528 to 539). The query is a constructor
  rather than a bare \<^typ>‹exp› so that a later kind extends the datatype.
›

datatype query = EvalInt exp

type_synonym answer = "int_dom query_lift"

abbreviation gamma_answer :: "answer ⇒ int set" where
  "gamma_answer ≡ gamma_query_lift gamma_int_dom"

text ‹
  An answer claims that the expression evaluates into its concretization.
  ‹QTop› claims nothing: an analysis that does not understand the question
  declines with it. ‹QBot› admits no value, so a sound handler returns it
  only for a state that represents no concrete store. The meet combines two
  answers about one expression, and since the \<^typ>‹int_dom› meet is exact,
  two sound analyses whose answers do not overlap describe no store in common.
›

fun eval_holds :: "query ⇒ answer ⇒ store ⇒ bool" where
  "eval_holds (EvalInt e) a s ⟷ ⟦e⟧⇩_e s ∈ gamma_answer a"

interpretation eval_query: query_algebra eval_holds
proof
  fix q :: query and a b :: answer and s
  show "eval_holds q ⊤ s"
    by (cases q) simp
  show "eval_holds q a s ⟹ eval_holds q b s ⟹ eval_holds q (a ⊓ b) s"
    by (cases q) (simp add: gamma_query_lift_inf[OF gamma_inf_int_dom])
qed

declare eval_query.top_sound [simp]

text ‹
  The exact answer for a known integer, and a known integer read back from
  an answer, as Goblint's ‹ID.of_int› and ‹ID.to_int›. A consumer that reads
  ‹n› back may use it for the expression at every store the answer holds at.
›

definition answer_of_int :: "int ⇒ answer" where
  "answer_of_int n = QLifted (int_dom_of_int n)"

lemma gamma_answer_of_int [simp]:
  "gamma_answer (answer_of_int n) = {n}"
  by (simp add: answer_of_int_def)

fun answer_const :: "answer ⇒ int option" where
  "answer_const (QLifted d) = int_dom_constant d"
| "answer_const _ = None"

lemma eval_holds_constD:
  assumes "eval_holds (EvalInt e) a s" and "answer_const a = Some n"
  shows "⟦e⟧⇩_e s = n"
  using assms gamma_int_dom_constant_subset
  by (cases a rule: answer_const.cases) auto

lemma answer_const_of_int [simp]: "answer_const (answer_of_int n) = Some n"
  by (simp add: answer_of_int_def int_dom_of_int_def int_dom_constant_def
      top_int_dom_ext_def)

text ‹
  An interval analysis knows only the interval component; the others stay at
  their top, so the answer claims exactly what the interval does.
›

definition answer_of_ivl :: "ivl ⇒ answer" where
  "answer_of_ivl i = QLifted ((⊤ :: int_dom)⦇int_ivl := i⦈)"

lemma gamma_answer_of_ivl [simp]:
  "gamma_answer (answer_of_ivl i) = gamma_ivl i"
  by (simp add: answer_of_ivl_def top_int_dom_ext_def top_sign_def top_parity_def
      gamma_int_dom_def)

end