Theory Conf

theory Conf
imports Store
begin

section ‹Configurations, Subsumption and Symbolic Execution›

text ‹In this section, we first introduce most elements related to our modeling of program 
behaviors. We first define the type of configurations, on which symbolic execution performs, and 
define the various concepts we will rely upon in the following and state and prove properties about 
them. Then, we introduce symbolic execution. After giving a number of basic properties about 
symbolic execution, we prove that symbolic execution is monotonic with respect to the subsumption 
relation, which is a crucial point in order to prove the main theorems of \verb?RB.thy?. Moreover, 
Isabelle/HOL requires the actual formalization of a number of facts one would not worry when 
implementing or writing a sketch proof. Here, we will need to prove that there exist successors of 
the configurations on which symbolic execution is performed. Although this seems quite obvious in 
practice, proofs of such facts will be needed a number of times in the following theories. Finally, 
we define the feasibility of a sequence of labels.›


subsection ‹Basic Definitions and Properties›

subsubsection‹Configurations›

text ‹Configurations are pairs @{term "(store,pred)"} where:
\begin{itemize}
  \item @{term "store"} is a store mapping program variable to symbolic variables,
  \item @{term "pred"} is a set of boolean expressions over program variables whose conjunction is
the actual path predicate.
\end{itemize}›


record ('v,'d) conf = 
  store :: "'v store"
  pred  :: "('v symvar,'d) bexp set"


subsubsection ‹Symbolic variables of a configuration.›

text ‹The set of symbolic variables of a configuration is the union of the set of symbolic 
variables of its store component with the set of variables of its path predicate.›


definition symvars :: 
  "('v,'d) conf ⇒ 'v symvar set" 
where
  "symvars c = Store.symvars (store c) ∪ Bexp.vars (conjunct (pred c))"


subsubsection ‹Freshness.›

text ‹A symbolic variable is said to be fresh for a configuration if it is not an element of its 
set of symbolic variables.›


definition fresh_symvar :: 
  "'v symvar ⇒ ('v,'d) conf ⇒ bool" 
where
  "fresh_symvar sv c = (sv ∉ symvars c)"


subsubsection ‹Satisfiability›

text ‹A configuration is said to be satisfiable if its path predicate is satisfiable.›


abbreviation sat :: 
  "('v,'d) conf ⇒ bool" 
where
  "sat c ≡ Bexp.sat (conjunct (pred c))"


subsubsection ‹States of a configuration›

text ‹Configurations represent sets of program states. The set of program states represented by a 
configuration, or simply its set of program states, is defined as the set of program states such that 
consistent symbolic states wrt.\ the store component of the configuration satisfies its path 
predicate.›


definition states :: 
  "('v,'d) conf ⇒ ('v,'d) state set" 
where
 "states c = {σ. ∃ σ⇩s⇩y⇩m. consistent σ σ⇩s⇩y⇩m (store c) ∧ conjunct (pred c) σ⇩s⇩y⇩m}"


text ‹A configuration is satisfiable if and only if its set of states is not empty.›


lemma sat_eq :  
  "sat c = (states c ≠ {})"
using consistentI2 by (simp add : sat_def states_def) fast



subsubsection ‹Subsumption›

text ‹A configuration @{term "c⇩2"} is subsumed by a configuration @{term "c⇩1"} if the set of 
states of @{term "c⇩2"} is a subset of the set of states of @{term "c⇩1"}.›


definition subsums :: 
  "('v,'d) conf ⇒ ('v,'d) conf ⇒ bool" (infixl ‹⊑› 55) 
where     
  "c⇩2 ⊑ c⇩1 ≡ (states c⇩2 ⊆ states c⇩1)"


text ‹The subsumption relation is reflexive and transitive.›


lemma subsums_refl :
  "c ⊑ c"
by (simp only : subsums_def)


lemma subsums_trans :
  "c1 ⊑ c2 ⟹ c2 ⊑ c3 ⟹ c1 ⊑ c3"
unfolding subsums_def by simp


text ‹However, it is not anti-symmetric. This is due to the fact that different configurations 
can have the same sets of program states. However, the following lemma trivially follows the 
definition of subsumption.›


lemma
  assumes "c1 ⊑ c2"
  assumes "c2 ⊑ c1"
  shows   "states c1 = states c2"
using assms by (simp add : subsums_def)


text ‹A satisfiable configuration can only be subsumed by satisfiable configurations.›


lemma sat_sub_by_sat :
  assumes "sat c⇩2"
  and     "c⇩2 ⊑ c⇩1"
  shows   "sat c⇩1"
using assms sat_eq[of c⇩1] sat_eq[of c⇩2] 
by (simp add : subsums_def) fast


text ‹On the other hand, an unsatisfiable configuration can only subsume unsatisfiable 
configurations.›


lemma unsat_subs_unsat :
  assumes "¬ sat c1"
  assumes "c2 ⊑ c1"
  shows   "¬ sat c2"
using assms sat_eq[of c1] sat_eq[of c2] 
by (simp add : subsums_def)


subsubsection ‹Semantics of a configuration›

text ‹The semantics of a configuration @{term "c"} is a boolean expression @{term "e"} over 
program states associating \emph{true} to a program state if it is a state of @{term "c"}. In 
practice, given two configurations @{term "c⇩1"} and @{term "c⇩2"}, it is not possible to enumerate 
their sets of states to establish the inclusion in order to detect a subsumption. We detect the 
subsumption of the former by the latter by asking a constraint solver if @{term "sem c⇩1"} entails 
@{term "sem c⇩2"}. The following theorem shows that the way we detect subsumption in practice is 
correct.›


definition sem :: 
  "('v,'d) conf ⇒ ('v,'d) bexp" 
where
 "sem c = (λ σ. σ ∈ states c)"


theorem
  "c⇩2 ⊑ c⇩1 ⟷ sem c⇩2 ⊨⇩B sem c⇩1"
unfolding subsums_def sem_def subset_iff entails_def by (rule refl)


subsubsection ‹Abstractions›

text ‹Abstracting a configuration consists in removing a given expression from its @{term "pred"} 
component, i.e.\ weakening its path predicate. This definition of abstraction motivates the fact 
that the @{term "pred"} component of configurations has been defined as a set of boolean expressions 
instead of a boolean expression.›


definition abstract ::
  "('v,'d) conf ⇒ ('v,'d) conf ⇒ bool"
where
  "abstract c c⇩a ≡ c ⊑ c⇩a"


subsubsection ‹Entailment›

text ‹A configuration \emph{entails} a boolean expression if its semantics entails this expression. 
This is equivalent to say that this expression holds for any state of this configuration.›


abbreviation entails :: 
  "('v,'d) conf ⇒ ('v,'d) bexp ⇒ bool" (infixl ‹⊨⇩c› 55) 
where
  "c ⊨⇩c φ ≡ sem c ⊨⇩B φ"

lemma 
  "sem c ⊨⇩B e ⟷ (∀ σ ∈ states c. e σ)"
by (auto simp add : states_def sem_def entails_def)



end