Theory IMP2_Program_Analysis

section ‹Program Analysis›
theory IMP2_Program_Analysis
imports "../basic/Annotated_Syntax" "../lib/Subgoal_Focus_Some" "../parser/Parser" IMP2_Basic_Decls
begin
  subsection ‹Analysis Simproc›

  
  definition [simp]: "ANALYZE x ≡ x"
  (*lemma ANALYZE_cong[named_ss vcg_bb cong]: "ANALYZE x = ANALYZE x" by simp*)
  
  simproc_setup ANALYZE ("ANALYZE x") 
    = ‹fn _ => fn ctxt => let
    
        val analysis_unfolds = 
          @{thm ANALYZE_def} 
          :: Named_Theorems.get ctxt @{named_theorems analysis_unfolds}
          @ Named_Theorems.get ctxt @{named_theorems vcg_annotation_defs}
    
        val unfold_conv = 
           map (Local_Defs.meta_rewrite_rule ctxt #> perhaps (try Drule.abs_def)) analysis_unfolds
        |> Raw_Simplifier.rewrite ctxt true
    
    in
      unfold_conv #> SOME
    end  
  ›
  declare [[simproc del: ANALYZE]]

  declaration ‹fn _ => Named_Simpsets.map_ctxt @{named_simpset vcg_bb} (
    fn ctxt => ctxt addsimprocs [@{simproc ANALYZE}]
  )›

  (* TODO: There's a more general concept here: 
    Activating specific simpsets depending on the context, or, in this case, a trigger constant.
    DUP with STRIP_ANNOT in VCG
  *)

  
  lemmas [analysis_unfolds] = Inline_def Params_def AssignIdx_retv_def ArrayCpy_retv_def
  

  subsection ‹Modifies Sets›
  
  definition modifies :: "vname set ⇒ state ⇒ state ⇒ bool" where
    "modifies vars s⇩1 s⇩2 = (∀x. x∉vars ⟶ s⇩1 x = s⇩2 x)"
  
  context notes[simp] = modifies_def begin
    lemma modifies_refl[intro!, simp]: "modifies vs a a" by simp
    lemma modifies_sym[sym]: "modifies vs a b ⟹ modifies vs b a" by simp
    lemma modifies_trans'[trans]: "modifies vs⇩1 a b ⟹ modifies vs⇩2 b c ⟹ modifies (vs⇩1∪vs⇩2) a c" by simp
    lemma modifies_trans[trans]: "modifies vs a b ⟹ modifies vs b c ⟹ modifies vs a c" by simp
  
    (* Test for correct order of trans-rules *)
    notepad begin
      fix vs a b c
      assume "modifies vs a b"
      also assume "modifies vs b c"
      finally have "modifies vs a c" . (* This must be trivial. If you get vs∪vs, something went wrong! *)
    end
    
    
    lemma modifies_join: "⟦ modifies vs⇩1 a b; modifies vs⇩2 a b ⟧ ⟹ modifies (vs⇩1∩vs⇩2) a b" by auto
    
    lemma modifies_mono: "⟦ vs⇩1⊆vs⇩2; modifies vs⇩1 a b ⟧ ⟹ modifies vs⇩2 a b" by auto
    
    lemma modifies_equals: "modifies vs s s' ⟹ x∉vs ⟹ s x = s' x" by auto
    lemma modifies_upd: 
      "x∈vs ⟹ modifies vs s (s'(x:=v)) ⟷ modifies vs s s'" 
      "x∈vs ⟹ modifies vs (s(x:=v)) s' ⟷ modifies vs s s'" 
      by auto
      
    lemma modifies_split: "modifies vs (<l|g>) (<l'|g'>) 
      ⟷ modifies (Collect is_global ∪ vs) l l' ∧ modifies (Collect is_local ∪ vs) g g'"  
      apply (auto simp: combine_query) by (metis combine_query)
      
  end  
    
  definition "wp_mod π vs c Q s = wp π c (λs'. modifies vs s' s ∧ Q s') s "
  definition "wlp_mod π vs c Q s = wlp π c (λs'. modifies vs s' s ∧ Q s') s "
    
  subsubsection ‹Simplification of Modifies Tags›  
    
  ML ‹
  
    val simp_modifies_tac = let
      fun is_modifies _ ct = case Thm.term_of ct of _ $ \<^Const_>‹modifies for _ _ _› => true | _ => false
      fun dest_modifies (Const _ $ \<^Const_>‹modifies for vs s d›) = (vs,s,d)
        | dest_modifies t = raise TERM("dest_modifies",[t])
        
        
    in
      Subgoal_Focus_Some.FOCUS_SOME_PREMS is_modifies (fn {context=ctxt, prems, concl, ...} => let
      
        val sts = map (#2 o dest_modifies o Thm.prop_of) prems |> Termtab.make_set
  
        fun collect_vars (a$b) = if Termtab.defined sts a then Termtab.insert_set b else collect_vars a o collect_vars b
          | collect_vars (Abs (_,_,t)) = collect_vars t
          | collect_vars _ = I
            
        val vars = 
          Termtab.empty
          |> collect_vars (Thm.term_of concl) o fold collect_vars (map Thm.prop_of prems)
          |> Termtab.keys 
          |> map (Thm.cterm_of ctxt)
  
        val ctxt_bb = Named_Simpsets.put @{named_simpset vcg_bb} ctxt  
        fun mk_mod_thm x thm = let
          val thm = @{thm modifies_equals} OF [thm]
          fun is_triv thm = case Thm.prop_of thm of @{prop "True"} => true | _ => false
          
          val thm = Drule.infer_instantiate' ctxt [SOME x] thm
            |> full_simplify ctxt_bb
        in
          if is_triv thm then NONE else SOME thm
        end
          
        val thms = map_product (mk_mod_thm) vars prems |> map_filter I 
        
        val ctxt = Simplifier.put_simpset HOL_basic_ss ctxt addsimps thms
        
      
      in HEADGOAL (asm_full_simp_tac ctxt) end)
    end
  ›
  
  method_setup i_vcg_modifies_simp = ‹Scan.succeed (SIMPLE_METHOD' o simp_modifies_tac)›
  
  
  subsubsection ‹Syntactic Approximation of Modifies Set›

  primrec lhsv' :: "com ⇒ vname set" where
    "lhsv' (x[_] ::= _) = {x}"
  | "lhsv' (x[] ::= _) = {x}"
  | "lhsv' (CLEAR x[]) = {x}"
  | "lhsv' (Assign_Locals l) = Collect is_local"
  | "lhsv' SKIP = {}"  
  | "lhsv' (c⇩1;; c⇩2) = lhsv' c⇩1 ∪ lhsv' c⇩2"
  | "lhsv' (IF _ THEN c⇩1 ELSE c⇩2) = lhsv' c⇩1 ∪ lhsv' c⇩2"
  | "lhsv' (WHILE _ DO c) = lhsv' c"
  | "lhsv' (SCOPE c) = Set.filter is_global (lhsv' c)"
  | "lhsv' (PCall p) = {}"
  | lhsv'_pscope_simp_orig[simp del]: 
    "lhsv' (PScope π c) = ⋃(ran (map_option lhsv' o π)) ∪ lhsv' c"
  
  definition "lhsvπ π ≡ (⋃c∈ran π. lhsv' c)"
  
  lemma lhsv'_pscope_simp[simp]: "lhsv' (PScope π c) = lhsvπ π ∪ lhsv' c"
    by (auto simp: ran_def lhsv'_pscope_simp_orig lhsvπ_def)

  lemma lhsvπ_empty: "lhsvπ Map.empty = {}" by (auto simp: lhsvπ_def)
  lemma lhsvπ_upd: "m p = None ⟹ lhsvπ (m(p↦c)) = lhsv' c ∪ lhsvπ m" 
    apply (auto simp: lhsvπ_def ran_def)
    by (metis option.simps(3))

  lemmas lhsvπ_maplet[simp] = lhsvπ_empty lhsvπ_upd
  
  notepad begin
    have "lhsvπ [''foo'' ↦ \<^imp>‹a=5›, ''bar'' ↦ \<^imp>‹c=7; b=5; rec foo()›] = {''a'', ''b'', ''c''}"
      by (simp add: Params_def)
  end

  
  primrec lhsv :: "program ⇒ com ⇒ vname set" where
    "lhsv π (x[_] ::= _) = {x}"
  | "lhsv π (x[] ::= _) = {x}"
  | "lhsv π (CLEAR x[]) = {x}"
  | "lhsv π (Assign_Locals l) = Collect is_local"
  | "lhsv π SKIP = {}"  
  | "lhsv π (c⇩1;; c⇩2) = lhsv π c⇩1 ∪ lhsv π c⇩2"
  | "lhsv π (IF _ THEN c⇩1 ELSE c⇩2) = lhsv π c⇩1 ∪ lhsv π c⇩2"
  | "lhsv π (WHILE _ DO c) = lhsv π c"
  | "lhsv π (SCOPE c) = Set.filter is_global (lhsv π c)"
  | "lhsv π (PCall p) = lhsvπ π"
  | "lhsv π (PScope π' c) = lhsvπ π' ∪ lhsv' c"
  
  
  text ‹Install special rule for procedure scope›  
  lemmas [named_ss vcg_bb] = lhsv'.simps
  lemmas [named_ss vcg_bb del] = lhsv'_pscope_simp_orig 
  lemmas [named_ss vcg_bb] = lhsv'_pscope_simp
  
  lemmas [named_ss vcg_bb] = lhsv.simps
  lemmas [named_ss vcg_bb] = lhsvπ_maplet
    
  lemmas [named_ss vcg_bb] = is_global.simps
  
  
          
    
  lemma modifies_lhsv'_gen:
    assumes "lhsvπ π ⊆ vs"
    assumes "lhsv' c ⊆ vs"
    assumes "π: (c,s) ⇒ t"
    shows "modifies vs t s"
    using assms(3,1,2)
  proof (induction arbitrary: vs)
    case (Scope π c s s')
    from Scope.IH[where vs="vs ∪ Collect is_local"] Scope.prems 
    show ?case by (fastforce simp: modifies_def combine_states_def) 
  next
    case (PCall π p c s t)
    then show ?case by (auto simp: ran_def lhsvπ_def)
  next
    case (PScope π' p c s t π)
    then show ?case by (simp add: SUP_le_iff ranI lhsvπ_def)
  qed (auto simp: modifies_def combine_states_def)

  lemma modifies_lhsvπ:
    assumes "π: (c, s) ⇒ t"
    assumes "π p = Some c"
    shows "modifies (lhsvπ π) t s"
    apply (rule modifies_lhsv'_gen[OF _ _ assms(1)])
    using assms(2) by (auto simp: lhsvπ_def ran_def)

  lemma lhsv_approx: "lhsv π' c ⊆ lhsvπ π' ∪ lhsv' c" 
    apply (induction c arbitrary: π')
              apply auto
    apply (auto simp: lhsvπ_def)
    done
  
              

  lemma modifies_lhsv:
    assumes "π: (c, s) ⇒ t"
    shows "modifies (lhsv π c) t s"
    using assms
    apply (induction)
                apply (all ‹(auto simp: modifies_def combine_states_def; fail)?›)
     subgoal by (auto simp: modifies_lhsvπ) []
    subgoal using lhsv_approx by (auto simp: modifies_def)
    done
    
    
      
  lemma wp_strengthen_modset: "wp π c Q s ⟹ wp π c (λs'. Q s' ∧ modifies (lhsv π c) s' s) s"
    unfolding wp_def 
    by (blast intro: modifies_lhsv)
  
  lemma wlp_strengthen_modset: "wlp π c Q s ⟹ wlp π c (λs'. Q s' ∧ modifies (lhsv π c) s' s) s"
    unfolding wlp_def 
    by (blast intro: modifies_lhsv)

  lemma wp_mod_lhsv_eq: "wp_mod π (lhsv π c) c Q s = wp π c Q s"
    unfolding wp_mod_def
    using modifies_lhsv wp_def by auto
  
  lemma wlp_mod_lhsv_eq: "wlp_mod π (lhsv π c) c Q s = wlp π c Q s"
    unfolding wlp_mod_def
    using modifies_lhsv wlp_def by auto

    
  subsubsection ‹Hoare-Triple with Modifies-Set›
  text ‹We define a Hoare-Triple that contains a modifies declaration›
  definition "HT_mods π mods P c Q ≡ HT π P c (λs⇩0 s. modifies mods s s⇩0 ∧ Q s⇩0 s)"
  definition "HT_partial_mods π mods P c Q ≡ HT_partial π P c (λs⇩0 s. Q s⇩0 s ∧ modifies mods s s⇩0)"

  lemma HT_mods_cong[named_ss vcg_bb cong]:
    assumes "vs = vs'"
    assumes "P=P'"
    assumes "c=c'"
    assumes "⋀s⇩0 s. modifies vs s s⇩0 ⟹ Q s⇩0 s = Q' s⇩0 s"
    shows "HT_mods π vs P c Q = HT_mods π vs' P' c' Q'"
    unfolding HT_mods_def HT_def using assms
    by (auto intro: wp_conseq)
    
  lemma HT_partial_mods_cong[named_ss vcg_bb cong]:
    assumes "vs = vs'"
    assumes "P=P'"
    assumes "c=c'"
    assumes "⋀s⇩0 s. modifies vs s s⇩0 ⟹ Q s⇩0 s = Q' s⇩0 s"
    shows "HT_partial_mods π vs P c Q = HT_partial_mods π vs' P' c' Q'"
    unfolding HT_partial_mods_def HT_partial_def using assms
    by (auto intro: wlp_conseq)
  
  lemma vcg_wp_conseq:
    assumes "HT_mods π mods P c Q"
    assumes "P s"
    assumes "⋀s'. ⟦modifies mods s' s; Q s s'⟧ ⟹ Q' s'"
    shows "wp π c Q' s"
    using assms unfolding HT_mods_def HT_def
    by (metis (no_types, lifting) wp_def)
    
  lemma vcg_wlp_conseq:
    assumes "HT_partial_mods π mods P c Q"
    assumes "P s"
    assumes "⋀s'. ⟦modifies mods s' s; Q s s'⟧ ⟹ Q' s'"
    shows "wlp π c Q' s"
    using assms unfolding HT_partial_mods_def HT_partial_def
    by (metis (no_types, lifting) wlp_def)

  text ‹The last rule allows us to re-use a total correctness verification in a partial 
    correctness proof.›  
  lemma vcg_wlp_wp_conseq:
    assumes "HT_mods π mods P c Q"
    assumes "P s"
    assumes "⋀s'. ⟦modifies mods s' s; Q s s'⟧ ⟹ Q' s'"
    shows "wlp π c Q' s"
    using assms vcg_wp_conseq wp_imp_wlp by auto
    
  (*
    TODO: Rules for combining proofs over the same program!
  *)
        
    
    
    
subsection ‹Free Variables of Expressions› 

text ‹This function computes the set of variables that occur in an expression›
fun fv_aexp :: "aexp ⇒ vname set" where
  "fv_aexp (N _) = {}"
| "fv_aexp (Vidx x i) = insert x (fv_aexp i)"
| "fv_aexp (Unop f a) = fv_aexp a"
| "fv_aexp (Binop f a b) = fv_aexp a ∪ fv_aexp b"

    
declare fv_aexp.simps[named_ss vcg_bb]

lemma aval_eq_on_fv: "(∀x∈fv_aexp a. s x = s' x) ⟹ aval a s = aval a s'"
  by (induction a) auto
    
lemma aval_indep_non_fv: "x∉fv_aexp a ⟹ aval a (s(x:=y)) = aval a s"
  by (induction a) auto

lemma redundant_array_assignment: "(x[] ::= a;; a[] ::= x) ∼ (x[] ::= a)"
  apply rule
   apply (auto)
   apply (metis ArrayCpy fun_upd_def fun_upd_idem_iff)
  by (metis ArrayCpy Seq fun_upd_apply fun_upd_idem)

lemma redundant_var_assignment: 
  assumes "x∉fv_aexp i" "x∉fv_aexp j"
  shows "(x[i] ::= Vidx a j;; a[j] ::= Vidx x i) ∼ (x[i] ::= Vidx a j)"
  apply (rule)
  using assms[THEN aval_indep_non_fv]
   apply auto
  subgoal
    by (smt Assign' aval.simps(1) aval.simps(2) fun_upd_apply fun_upd_idem_iff)
  subgoal
    by (simp add: Assign' fun_upd_twist)
  subgoal
    by (smt Seq aval.simps(2) big_step.intros(2) fun_upd_def fun_upd_triv)
  done

    
end