Theory Clean_Symbex

(******************************************************************************
 * Clean
 *
 * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

theory Clean_Symbex
  imports Clean
begin


section‹Clean Symbolic Execution Rules ›


subsection‹Basic NOP - Symbolic Execution Rules.  ›

text‹  As they are equalities, they can also
be used as program optimization rules. ›

lemma non_exec_assign  : 
assumes "▹ σ"
shows "(σ ⊨ ( _ ← assign f; M)) = ((f σ) ⊨  M)"
by (simp add: assign_def assms exec_bind_SE_success)

lemma non_exec_assign'  : 
assumes "▹ σ"
shows "(σ ⊨ (assign f;- M)) = ((f σ) ⊨  M)"
by (simp add: assign_def assms exec_bind_SE_success bind_SE'_def)

lemma exec_assign  : 
assumes "exec_stop σ"
shows "(σ ⊨ ( _ ← assign f; M)) = (σ ⊨ M)"
by (simp add: assign_def assms exec_bind_SE_success)     

lemma exec_assign'  : 
assumes "exec_stop σ"
shows "(σ ⊨ (assign f;- M)) = (σ ⊨ M)"
by (simp add: assign_def assms exec_bind_SE_success bind_SE'_def)     

subsection‹Assign Execution Rules.  ›

lemma non_exec_assign_global  : 
assumes "▹ σ"
shows   "(σ ⊨ ( _ ← assign_global upd rhs; M)) = ((upd (λ_. rhs σ) σ) ⊨  M)"
by(simp add: assign_global_def non_exec_assign assms)

lemma non_exec_assign_global'  : 
assumes "▹ σ"
shows   "(σ ⊨ (assign_global upd rhs;- M)) = ((upd (λ_. rhs σ) σ) ⊨  M)"
  by (metis (full_types) assms bind_SE'_def non_exec_assign_global)


lemma exec_assign_global  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( _ ← assign_global upd rhs; M)) = ( σ ⊨  M)"
  by (simp add: assign_global_def assign_def assms exec_bind_SE_success)

lemma exec_assign_global'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (assign_global upd rhs;- M)) = ( σ ⊨  M)"
  by (simp add: assign_global_def assign_def assms exec_bind_SE_success bind_SE'_def)

lemma non_exec_assign_local  : 
assumes "▹ σ"
shows   "(σ ⊨ ( _ ← assign_local upd rhs; M)) = ((upd (upd_hd (λ_. rhs σ)) σ) ⊨  M)"
  by(simp add: assign_local_def non_exec_assign assms)

lemma non_exec_assign_local'  : 
assumes "▹ σ"
shows   "(σ ⊨ (assign_local upd rhs;- M)) = ((upd (upd_hd (λ_. rhs σ)) σ) ⊨  M)"
  by (metis assms bind_SE'_def non_exec_assign_local)

lemmas non_exec_assign_localD'= non_exec_assign[THEN iffD1]

lemma exec_assign_local  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( _ ← assign_local upd rhs; M)) = ( σ ⊨  M)"
  by (simp add: assign_local_def assign_def assms exec_bind_SE_success)

lemma exec_assign_local'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( assign_local upd rhs;- M)) = ( σ ⊨  M)" 
  unfolding assign_local_def assign_def 
  by (simp add: assms exec_bind_SE_success2)

lemmas exec_assignD = exec_assign[THEN iffD1]
thm exec_assignD

lemmas exec_assignD' = exec_assign'[THEN iffD1]
thm exec_assignD'

lemmas exec_assign_globalD =  exec_assign_global[THEN iffD1]

lemmas exec_assign_globalD' =  exec_assign_global'[THEN iffD1]

lemmas exec_assign_localD = exec_assign_local[THEN iffD1]
thm exec_assign_localD

lemmas exec_assign_localD' = exec_assign_local'[THEN iffD1]



subsection‹Basic Call Symbolic Execution Rules.  ›



lemma exec_call_0  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( _ ← call_0⇩_C M; M')) = (σ ⊨  M')"
  by (simp add: assms call_0⇩_C_def exec_bind_SE_success)

lemma exec_call_0'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (call_0⇩_C M;- M')) = (σ ⊨  M')"
  by (simp add: assms bind_SE'_def exec_call_0)



lemma exec_call_1  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( x ← call_1⇩_C M A⇩₁; M' x)) = (σ ⊨  M' undefined)"
  by (simp add: assms call_1⇩_C_def call⇩_C_def exec_bind_SE_success)

lemma exec_call_1'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (call_1⇩_C M A⇩₁;- M')) = (σ ⊨  M')"
  by (simp add: assms bind_SE'_def exec_call_1)

lemma exec_call  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( x ← call⇩_C M A⇩₁; M' x)) = (σ ⊨  M' undefined)"
  by (simp add: assms call⇩_C_def call_1⇩_C_def exec_bind_SE_success)

lemma exec_call'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (call⇩_C M A⇩₁;- M')) = (σ ⊨  M')"
  by (metis assms call_1⇩_C_def exec_call_1')

lemma exec_call_2  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( _ ← call_2⇩_C M A⇩₁ A⇩₂; M')) = (σ ⊨  M')"
  by (simp add: assms call_2⇩_C_def exec_bind_SE_success)

lemma exec_call_2'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (call_2⇩_C M A⇩₁ A⇩₂;- M')) = (σ ⊨ M')"
  by (simp add: assms bind_SE'_def exec_call_2)

subsection‹Basic Call Symbolic Execution Rules.  ›

lemma non_exec_call_0  : 
assumes "▹ σ"
shows   "(σ ⊨ ( _ ← call_0⇩_C M; M')) = (σ ⊨ M;- M')"
  by (simp add: assms bind_SE'_def bind_SE_def call_0⇩_C_def valid_SE_def)

lemma non_exec_call_0'  : 
assumes "▹ σ"
shows   "(σ ⊨ call_0⇩_C M;- M') = (σ ⊨ M;- M')"
  by (simp add: assms bind_SE'_def non_exec_call_0)

lemma non_exec_call_1  : 
assumes "▹ σ"
shows   "(σ ⊨ ( x ← (call_1⇩_C M (A⇩₁)); M' x)) = (σ ⊨ (x ← M (A⇩₁ σ); M' x))"
  by (simp add: assms bind_SE'_def call⇩_C_def bind_SE_def call_1⇩_C_def valid_SE_def)

lemma non_exec_call_1'  : 
assumes "▹ σ"
shows   "(σ ⊨ call_1⇩_C M (A⇩₁);- M') = (σ ⊨  M (A⇩₁ σ);- M')"
  by (simp add: assms bind_SE'_def non_exec_call_1)

(* general case *)
lemma non_exec_call  : 
assumes "▹ σ"
shows   "(σ ⊨ ( x ← (call⇩_C M (A⇩₁)); M' x)) = (σ ⊨ (x ← M (A⇩₁ σ); M' x))"
  by (simp add: assms call⇩_C_def bind_SE'_def bind_SE_def call_1⇩_C_def valid_SE_def)

lemma non_exec_call'  : 
assumes "▹ σ"
shows   "(σ ⊨ call⇩_C M (A⇩₁);- M') = (σ ⊨  M (A⇩₁ σ);- M')"
  by (simp add: assms bind_SE'_def non_exec_call)


lemma non_exec_call_2  : 
assumes "▹ σ"
shows   "(σ ⊨ ( _ ← (call_2⇩_C M (A⇩₁) (A⇩₂)); M')) = (σ ⊨ M (A⇩₁ σ) (A⇩₂ σ);- M')"
  by (simp add: assms bind_SE'_def bind_SE_def call_2⇩_C_def valid_SE_def)

lemma non_exec_call_2'  : 
assumes "▹ σ"
shows   "(σ ⊨ call_2⇩_C M (A⇩₁) (A⇩₂);- M') = (σ ⊨  M (A⇩₁ σ) (A⇩₂ σ);- M')"
  by (simp add: assms bind_SE'_def non_exec_call_2)


subsection‹Conditional.  ›

lemma exec_If⇩_C_If⇩_S⇩_E  : 
assumes "▹ σ"
shows   "((if⇩_C P then B⇩₁ else B⇩₂ fi))σ = ((if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi)) σ "
  unfolding if_SE_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def
  by (simp add: assms bind_SE_def if_C_def)
    
    
lemma valid_exec_If⇩_C  : 
assumes "▹ σ"
shows   "(σ ⊨ (if⇩_C P then B⇩₁ else B⇩₂ fi);-M) = (σ ⊨ (if⇩_S⇩_E P then B⇩₁ else B⇩₂ fi);-M)"
  by (meson assms exec_If⇩_C_If⇩_S⇩_E valid_bind'_cong)


      
lemma exec_If⇩_C'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (if⇩_C P then B⇩₁ else B⇩₂ fi);-M) = (σ ⊨ M)"    
  unfolding if_SE_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def bind_SE_def
    by (simp add: assms if_C_def)
    
lemma exec_While⇩_C'  : 
assumes "exec_stop σ"
shows  "(σ ⊨ (while⇩_C P do B⇩₁ od);-M) = (σ ⊨ M)"    
  unfolding while_C_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def bind_SE_def
  apply simp using assms by blast    


    
    
lemma if⇩_C_cond_cong : "f σ = g σ ⟹ (if⇩_C f then c else d fi) σ = 
                                     (if⇩_C g then c else d fi) σ"
  unfolding if_C_def
   by simp 
   
 
subsection‹Break - Rules.  ›

lemma break_assign_skip [simp]: "(break ;- assign f) = break"
  apply(rule ext)
  unfolding break_def assign_def exec_stop_def bind_SE'_def   bind_SE_def
  by auto



lemma break_if_skip [simp]: "(break ;- if⇩_C b then c else d fi) = break"
  apply(rule ext)
  unfolding break_def assign_def exec_stop_def if_C_def bind_SE'_def   bind_SE_def
  by auto
    
                       
lemma break_while_skip [simp]: "(break ;- while⇩_C b do c od) = break"
  apply(rule ext)
  unfolding while_C_def skip⇩_S⇩_E_def unit_SE_def bind_SE'_def bind_SE_def break_def exec_stop_def
  by simp

    
lemma unset_break_idem [simp] : 
 "(unset_break_status ;- unset_break_status ;- M) = (unset_break_status ;- M)"
  apply(rule ext)  unfolding unset_break_status_def bind_SE'_def bind_SE_def by auto

lemma return_cancel1_idem [simp] : 
 "(return⇘X⇙(E) ;- X :==⇩_G E' ;- M) = ( return⇩_C X E ;- M)"
  apply(rule ext, rename_tac "σ")  
  unfolding unset_break_status_def bind_SE'_def bind_SE_def
            assign_def return⇩_C_def return⇩_C0_def assign_global_def assign_local_def
  apply(case_tac "exec_stop σ")
  apply auto
  by (simp add: exec_stop_def set_return_status_def)
    
lemma return_cancel2_idem [simp] : 
 "( return⇘X⇙(E) ;- X :==⇩_L E' ;- M) = ( return⇩_C X E ;- M)"
    apply(rule ext, rename_tac "σ")  
  unfolding unset_break_status_def bind_SE'_def bind_SE_def
            assign_def return⇩_C_def return⇩_C0_def assign_global_def assign_local_def
  apply(case_tac "exec_stop σ")
   apply auto
  by (simp add: exec_stop_def set_return_status_def)


subsection‹While.  ›     

lemma while⇩_C_skip [simp]: "(while⇩_C (λ x. False) do c od) = skip⇩_S⇩_E"
  apply(rule ext)
  unfolding while_C_def skip⇩_S⇩_E_def unit_SE_def
  apply auto
  unfolding exec_stop_def skip⇩_S⇩_E_def unset_break_status_def bind_SE'_def unit_SE_def bind_SE_def
  by simp
 

txt‹ Various tactics for various coverage criteria ›

definition while_k :: "nat ⇒ (('σ_ext) control_state_ext ⇒ bool) 
                        ⇒ (unit, ('σ_ext) control_state_ext)MON⇩_S⇩_E 
                        ⇒ (unit, ('σ_ext) control_state_ext)MON⇩_S⇩_E"
where     "while_k _ ≡ while_C"


text‹Somewhat amazingly, this unfolding lemma crucial for symbolic execution still holds ... 
     Even in the presence of break or return...› 
lemma exec_while⇩_C : 
"(σ ⊨ ((while⇩_C b do c od) ;- M)) = 
 (σ ⊨ ((if⇩_C b then c ;- ((while⇩_C b do c od) ;- unset_break_status) else skip⇩_S⇩_E fi)  ;- M))"
proof (cases "exec_stop σ")
  case True
  then show ?thesis 
    by (simp add: True exec_If⇩_C' exec_While⇩_C')
next
  case False
  then show ?thesis
    proof (cases "¬ b σ")
      case True
      then show ?thesis
        apply(subst valid_bind'_cong)
        using ‹¬ exec_stop σ› apply simp_all
        apply (auto simp: skip⇩_S⇩_E_def unit_SE_def)
          apply(subst while_C_def, simp)
         apply(subst bind'_cong)
         apply(subst MonadSE.while_SE_unfold)
          apply(subst if⇩_S⇩_E_cond_cong [of _ _ "λ_. False"])
          apply simp_all
        apply(subst if⇩_C_cond_cong [of _ _ "λ_. False"], simp add: )
        apply(subst exec_If⇩_C_If⇩_S⇩_E,simp_all)
        by (simp add: exec_stop_def unset_break_status_def)
    next
      case False
      have * : "b σ"  using False by auto
      then show ?thesis
           unfolding while_k_def 
           apply(subst  while_C_def)
           apply(subst  if_C_def)
           apply(subst  valid_bind'_cong)
            apply (simp add: ‹¬ exec_stop σ›)
           apply(subst  (2) valid_bind'_cong)
            apply (simp add: ‹¬ exec_stop σ›)
            apply(subst MonadSE.while_SE_unfold)
            apply(subst valid_bind'_cong)
            apply(subst bind'_cong)
             apply(subst if⇩_S⇩_E_cond_cong [of _ _ "λ_. True"])
              apply(simp_all add:   ‹¬ exec_stop σ› )
            apply(subst bind_assoc', subst bind_assoc')
            proof(cases "c σ")
              case None
              then show "(σ ⊨ c;-((while⇩_S⇩_E (λσ. ¬ exec_stop σ ∧ b σ) do c od);-unset_break_status);-M) =
                         (σ ⊨ c;-(while⇩_C b do c od) ;- unset_break_status ;- M)"
                by (simp add: bind_SE'_def exec_bind_SE_failure)
            next
              case (Some a)
              then show "(σ ⊨ c ;- ((while⇩_S⇩_E (λσ. ¬ exec_stop σ ∧ b σ) do c od);-unset_break_status);-M) =
                         (σ ⊨ c ;- (while⇩_C b do c od) ;- unset_break_status ;- M)"
                apply(insert ‹c σ = Some a›, subst (asm) surjective_pairing[of a])
                apply(subst exec_bind_SE_success2, assumption)
                apply(subst exec_bind_SE_success2, assumption)
                proof(cases "exec_stop (snd a)")
                  case True
                  then show "(snd a ⊨((while⇩_S⇩_E (λσ. ¬ exec_stop σ ∧ b σ) do c od);-unset_break_status);-M)=
                             (snd a ⊨ (while⇩_C b do c od) ;- unset_break_status ;- M)"
                       by (metis (no_types, lifting) bind_assoc' exec_While⇩_C' exec_skip if_SE_D2' 
                                                  skip⇩_S⇩_E_def while_SE_unfold)
                next
                  case False
                  then show "(snd a ⊨ ((while⇩_S⇩_E(λσ. ¬exec_stop σ ∧ b σ) do c od);-unset_break_status);-M)=
                             (snd a ⊨ (while⇩_C b do c od) ;- unset_break_status ;- M)"
                          unfolding  while_C_def
                          by(subst (2) valid_bind'_cong,simp)(simp)
                qed       
            qed  
    qed
qed
(* ... although it is, oh my god, amazingly complex to prove. *)


lemma while_k_SE : "while_C = while_k k"
by (simp only: while_k_def)


corollary exec_while_k : 
"(σ ⊨ ((while_k (Suc n) b c) ;- M)) = 
 (σ ⊨ ((if⇩_C b then c ;- (while_k n b c) ;- unset_break_status else skip⇩_S⇩_E fi)  ;- M))"
  by (metis exec_while⇩_C while_k_def)
    

txt‹ Necessary prerequisite: turning ematch and dmatch into a proper Isar Method. ›
(* TODO : this code shoud go to TestGen Method setups *)
ML‹
local
fun method_setup b tac =
  Method.setup b
    (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o K (tac ctxt rules))))
in
val _ =
  Theory.setup (   method_setup @{binding ematch} ematch_tac "fast elimination matching"
                #> method_setup @{binding dmatch} dmatch_tac "fast destruction matching"
                #> method_setup @{binding match} match_tac "resolution based on fast matching")
end
›

lemmas exec_while_kD = exec_while_k[THEN iffD1]

end