Theory BasicDefs

chapter ‹The Framework›

theory BasicDefs imports AuxLemmas begin

text ‹
  As slicing is a program analysis that can be completely based on the
  information given in the CFG, we want to provide a framework which
  allows us to formalize and prove properties of slicing regardless of
  the actual programming language. So the starting point for the formalization 
  is the definition of an abstract CFG, i.e.\ without considering features 
  specific for certain languages. By doing so we ensure that our framework 
  is as generic as possible since all proofs hold for every language whose 
  CFG conforms to this abstract CFG.

  Static Slicing analyses a CFG prior to execution. Whereas dynamic
  slicing can provide better results for certain inputs (i.e.\ trace and
  initial state), static slicing is more conservative but provides
  results independent of inputs. 

  Correctness for static slicing is defined using a weak
  simulation between nodes and states when traversing the original and
  the sliced graph. The weak simulation property demands that if a
  (node,state) tuples $(n_1,s_1)$ simulates $(n_2,s_2)$
  and making an observable move in the original graph leads from 
  $(n_1,s_1)$ to $(n_1',s_1')$, this tuple simulates a 
  tuple $(n_2,s_2)$ which is the result of making an
  observable move in the sliced graph beginning in $(n_2',s_2')$.  
›

section ‹Basic Definitions›

fun fun_upds :: "('a  'b)  'a list  'b list  ('a  'b)"
where "fun_upds f [] ys = f"
  | "fun_upds f xs [] = f"
  | "fun_upds f (x#xs) (y#ys) = (fun_upds f xs ys)(x := y)"

notation fun_upds ("_'(_ /[:=]/ _')")

lemma fun_upds_nth:
  "i < length xs; length xs = length ys; distinct xs
   f(xs [:=] ys)(xs!i) = (ys!i)"
proof(induct xs arbitrary:ys i)
  case Nil thus ?case by simp
next
  case (Cons x' xs')
  note IH = ys i. i < length xs'; length xs' = length ys; distinct xs'
     f(xs' [:=] ys) (xs'!i) = ys!i
  from distinct (x'#xs') have "distinct xs'" and "x'  set xs'" by simp_all
  from length (x'#xs') = length ys obtain y' ys' where [simp]:"ys = y'#ys'"
    and "length xs' = length ys'"
    by(cases ys) auto
  show ?case
  proof(cases i)
    case 0 thus ?thesis by simp
  next
    case (Suc j)
    with i < length (x'#xs') have "j < length xs'" by simp
    from IH[OF this length xs' = length ys' distinct xs']
    have "f(xs' [:=] ys') (xs'!j) = ys'!j" .
    with x'  set xs' j < length xs'
    have "f((x'#xs') [:=] ys) ((x'#xs')!(Suc j)) = ys!(Suc j)" by fastforce
    with Suc show ?thesis by simp
  qed
qed


lemma fun_upds_eq:
  assumes "V  set xs" and "length xs = length ys" and "distinct xs"
  shows "f(xs [:=] ys) V = f'(xs [:=] ys) V"
proof -
  from V  set xs obtain i where "i < length xs" and "xs!i = V"
    by(fastforce simp:in_set_conv_nth)
  with length xs = length ys distinct xs
  have "f(xs [:=] ys)(xs!i) = (ys!i)" by -(rule fun_upds_nth)
  moreover
  from i < length xs xs!i = V length xs = length ys distinct xs
  have "f'(xs [:=] ys)(xs!i) = (ys!i)" by -(rule fun_upds_nth)
  ultimately show ?thesis using xs!i = V by simp
qed


lemma fun_upds_notin:"x  set xs  f(xs [:=] ys) x = f x"
by(induct xs arbitrary:ys,auto,case_tac ys,auto)


subsection distinct_fst›
 
definition distinct_fst :: "('a × 'b) list  bool" where
  "distinct_fst    distinct  map fst"

lemma distinct_fst_Nil [simp]:
  "distinct_fst []" 
  by(simp add:distinct_fst_def)

lemma distinct_fst_Cons [simp]:
  "distinct_fst ((k,x)#kxs) = (distinct_fst kxs  (y. (k,y)  set kxs))"
by(auto simp:distinct_fst_def image_def)


lemma distinct_fst_isin_same_fst:
  "(x,y)  set xs; (x,y')  set xs; distinct_fst xs
   y = y'"
by(induct xs,auto simp:distinct_fst_def image_def)


subsection‹Edge kinds›

text ‹Every procedure has a unique name, e.g. in object oriented languages
  pname› refers to class + procedure.›

text ‹A state is a call stack of tuples, which consists of:
  \begin{enumerate}
  \item data information, i.e.\ a mapping from the local variables in the call 
  frame to their values, and
  \item control flow information, e.g.\ which node called the current procedure.
  \end{enumerate}

  Update and predicate edges check and manipulate only the data information
  of the top call stack element. Call and return edges however may use the data and
  control flow information present in the top stack element to state if this edge is
  traversable. The call edge additionally has a list of functions to determine what
  values the parameters have in a certain call frame and control flow information for
  the return. The return edge is concerned with passing the values 
  of the return parameter values to the underlying stack frame. See the funtions 
  transfer› and pred› in locale CFG›.›

datatype (dead 'var, dead 'val, dead 'ret, dead 'pname) edge_kind =
    UpdateEdge "('var  'val)  ('var  'val)"                  ("_")
  | PredicateEdge "('var  'val)  bool"                         ("'(_')")
  | CallEdge "('var  'val) × 'ret  bool" "'ret" "'pname"  
             "(('var  'val)  'val) list"                       ("_:_↪⇘__" 70)
  | ReturnEdge "('var  'val) × 'ret  bool" "'pname" 
               "('var  'val)  ('var  'val)  ('var  'val)" ("_↩⇘__" 70)


definition intra_kind :: "('var,'val,'ret,'pname) edge_kind  bool"
where "intra_kind et  (f. et = f)  (Q. et = (Q))"


lemma edge_kind_cases [case_names Intra Call Return]:
  "intra_kind et  P; Q r p fs. et = Q:r↪⇘pfs  P;
    Q p f. et = Q↩⇘pf  P  P"
by(cases et,auto simp:intra_kind_def)


end