Abstract Interpretation

Point: Abstract interpretation of programs is a unified approach to apparently unrelated program analysis techniques.

Syntax

  • Program: a set of "nodes".
  • Node: has successor and predecessor nodes
    • Entry: no pred, one succ
    • Assignment: one pred, one succ; "Ident" <- "Expr"
    • Test: one pred, two succ; if "Bexpr" then "Expr" else "Expr"
    • Junction: one succ, more than one pred.
    • Exit: one pred, no succ.

Semantics

  • $S_0 = lattice(S \,\cup {\bot_S, \top_S}), \forall x \in S, \bot_S \leq x \leq \top_S$
  • "Values" semantic domain: a complete lattice as sum of primitive domains
  • $Env = Ident^0 \rightarrow Values$
  • Meaning of an expression: $val: Expr \rightarrow [Env \rightarrow Values]$, in particular $\underline{val}: Bexpr \rightarrow [Env \rightarrow Bool]$
  • $\forall s \in States, s = \langle cs(s), env(s)\rangle$, i.e. control state and environment state
  • ??? if $e \in Env, v \in Values, x \in Ident$, then $e [v / x] = \lambda y . \underline{cond}(y = x, v, e(y))$
  • $\texttt{n-state }: States \rightarrow States$

And there are a lot of other stuff defined. But in total they look pretty puzzling to me ...

Static Semantics of Programs

$Cv$ is a static summary of the possible executions of the program.

Before that, a lot of definitions are here. But I hardly know the motivations for such definitions.

Quite difficult. I decide to have a glimpse at MIT course first.

Note of Notes of MIT Course

Well .. The first slide is a bit puzzling ... I should continue or look at the reading assignments? CONTINUE.

This paper reading will be transformed into course reading of the MIT course.