Theory Example_Call_String_Precision

theory Example_Call_String_Precision
  imports "Voblint_CLI.Analysis_Certified"
    "Voblint_Examples_Sign.Example_Sign_DG_CallString_K2"
begin

section ‹Longer call strings decide a check through the analyzer›

text ‹
  \<^theory>‹Voblint_Examples_Sign.Example_Sign_DG_CallString_K2› compares two hand-built
  routed equation systems. This theory makes the same comparison on the public
  operation \<^const>‹run_voblint›, by evaluation. ‹f› passes its argument to ‹g›, and
  ‹main› calls ‹f› with a positive and a negative value. Under Sign with call strings
  of length 1, both activations of ‹g› share the context of its one call site in ‹f›,
  so Sign joins the two arguments to ‹⊤› and neither check is decided. Call strings
  of length 2 also record the call in ‹main›, keep the two activations apart, and
  prove both checks.
›

definition cs_nest_prog :: imp_prog where
  "cs_nest_prog = program {
     fun g(p) { return p + p; }
     fun f(p) { t = g(p); return t; }
     fun main() {
       x = f(3);
       y = f(-10);
       __voblint_check(0 < x);
       __voblint_check(y < 0);
     }
   }"

abbreviation cs_nest_config :: "nat ⇒ analysis_config" where
  "cs_nest_config k ≡ Analysis_Config [Sign_Analysis] Globals_Warrow (Ctx_CallString k)
     Program_Globals_Flow_Sensitive"

abbreviation cs_nest_checks where
  "cs_nest_checks res ≡ map (λc. (check_point c, check_exp c, check_verdict c)) (report_checks res)"

abbreviation cs_x_pos :: exp where "cs_x_pos ≡ Less (N 0) (V (STR ''x''))"
abbreviation cs_y_neg :: exp where "cs_y_neg ≡ Less (V (STR ''y'')) (N 0)"

lemma cs_nest_reports:
  "(case (run_voblint (cs_nest_config 1) cs_nest_prog, run_voblint (cs_nest_config 2) cs_nest_prog) of
      (Analysed res1, Analysed res2) ⇒
        cs_nest_checks res1
          = [(Statement 7, cs_x_pos, Decided Check_Unknown),
             (Statement 8, cs_y_neg, Decided Check_Unknown)]
      ∧ cs_nest_checks res2
          = [(Statement 7, cs_x_pos, Decided Check_Proved),
             (Statement 8, cs_y_neg, Decided Check_Proved)]
    | _ ⇒ False)"
  by eval

lemma HAS_VERDICT_of_checks:
  assumes "cs_nest_checks res = xs" and "(v, e, Decided r) ∈ set xs"
  shows "HAS_VERDICT res v e r"
proof -
  from assms obtain c where "c ∈ set (report_checks res)" "check_point c = v"
    and "check_exp c = e" "check_verdict c = Decided r"
    by auto
  then show ?thesis unfolding HAS_VERDICT_def by auto
qed

text ‹
  The two runs, read through the report's verdicts: length 1 leaves both checks
  ‹UNKNOWN›, length 2 proves both.
›

theorem run_voblint_call_string_2_decides:
  "∃res1 res2.
     run_voblint (cs_nest_config 1) cs_nest_prog = Analysed res1
   ∧ run_voblint (cs_nest_config 2) cs_nest_prog = Analysed res2
   ∧ UNKNOWN res1 (Statement 7) cs_x_pos ∧ UNKNOWN res1 (Statement 8) cs_y_neg
   ∧ PROVED res2 (Statement 7) cs_x_pos ∧ PROVED res2 (Statement 8) cs_y_neg"
proof -
  obtain res1 res2 where
      run1: "run_voblint (cs_nest_config 1) cs_nest_prog = Analysed res1"
    and run2: "run_voblint (cs_nest_config 2) cs_nest_prog = Analysed res2"
    and c1: "cs_nest_checks res1
               = [(Statement 7, cs_x_pos, Decided Check_Unknown),
                  (Statement 8, cs_y_neg, Decided Check_Unknown)]"
    and c2: "cs_nest_checks res2
               = [(Statement 7, cs_x_pos, Decided Check_Proved),
                  (Statement 8, cs_y_neg, Decided Check_Proved)]"
    using cs_nest_reports
    by (auto split: analysis_answer.splits)
  have "UNKNOWN res1 (Statement 7) cs_x_pos" "UNKNOWN res1 (Statement 8) cs_y_neg"
    by (rule HAS_VERDICT_of_checks[OF c1], simp)+
  moreover have "PROVED res2 (Statement 7) cs_x_pos" "PROVED res2 (Statement 8) cs_y_neg"
    by (rule HAS_VERDICT_of_checks[OF c2], simp)+
  ultimately show ?thesis using run1 run2 by blast
qed

text ‹
  With the soundness theorem, the length-2 verdicts are facts about the program: every
  store that reaches either check satisfies it.
›

corollary cs_nest_checks_hold:
  assumes "s ∈ 𝒞⇘declared_global cs_nest_prog,prog_cfg cs_nest_prog,
                   cinit_stores (declared_global cs_nest_prog)⇙ (Statement 7)"
    and "t ∈ 𝒞⇘declared_global cs_nest_prog,prog_cfg cs_nest_prog,
                   cinit_stores (declared_global cs_nest_prog)⇙ (Statement 8)"
  shows "truthy (⟦cs_x_pos⟧⇩e s)" and "truthy (⟦cs_y_neg⟧⇩e t)"
  using run_voblint_call_string_2_decides run_voblint_proved assms by blast+

end