I am following these lecture notes on performing AI for a simple bytecode language: absint winter school, Saint petersburg.
I could find no approachable uses of abstract interpretation, so I decided to write one up for myself.
There is a TUI implementation using brick
, a general abstract
interpretation framework (currently instantiated against presburger
arithmetic), with haskell bindings to the ISL library for presburger arithmetic.
- Is this sane? While it is possibly "mathematically correct", I have no idea if this is tasteful since I do not know AI literature. Critique on this would help
- Consider the two frameworks of AI. One which specifies an
alpha
and agamma
in a galois connection. Given a concrete operatorf
, we construct the abstract operatorf# = alpha . f . gamma
. The second framework, which for each concrete operatorf
, defines an abstract operatorf#
, and also provides agamma
, under the condition thatf <= gamma(f#)
. Given this, can we recoveralpha
andgamma
? If not, how are the two approaches related? Answer: See Antoine Mine's thesis, where he defines three styles of AI:alpha, gamma
based AI.- defining abstract operators
f#
for everyf
with a givengamma
. gamma
, partialalpha
based AI.
I'm trying to understand the symbolic abstract domain as constructed by Mine.
-
See
Definition 6.3.4
: The definition ofgamma^symb
is confusing. I don't understand the type / what it returns. In particular, it seems recursively defined? there is arho
that occurs on both the LHS and the RHS. -
Similarly, theorem
6.3.1
, seems to assert that substituting bound variables is always sound. I don't understand what's going on there. Consider the case of:subst :: B^symb x V x B^symb -> B^symb rho#(X) = Z expr = X Theorem asserts: expr <= subst(expr, X, rho#(X)) X <= subst(X, X, Z) X <= Z
But is it true that
X <= Z
? I would have assumed that the variables are incomparable in the lattice. I could not find the partial order defined onB^symb
. It is defined onB^constant
atDefinition 6.3.1
. -
Also, the symbolic abstract domain's denotation operator
[[ . ]]
is not clearly described. It is referred to inDefinition 6.3.1
, sub part3
, but I could not find an actual definition. -
The meaning of a symbolic value is
(V -> I) -> powerset(I)
(Definition6.3.1
). That is, given an environment, it provides a set of values the symbolic expression can take. How is this related to the actual collecting semantics? That is, we are provided a concretisation functiongamma :: B^symb -> (V -> I) -> powerset(I)
. But(V -> I) -> powerset(I)
is not the collecting semantics. So, what is the proof of correctness of this concretisation functiongamma
?
- When defining the collecting semantics, one can of course use the "standard" collecting semantics. However, to perform analyses such as reaching definitions, we modify the collecting semantics with extra information (Lecture Notes: Widening Operators and Collecting Semantics - Jonathan Aldrich). What kinds of modification to the collecting semantics is legal?
- How do we view symbolic computation as abstract interpretation?