jonny goes to england

Today something a bit technical once again. Only suitable for people knowing something of ML etc.

In compilers, semantics and program analysis it’s sometimes handy or needed to transform loops into nested if’s. Perhaps for efficiency reasons, for precision of some invariant detection, or perhaps to know the meaning of a loop up to some defined iteration.

Unrolling a loop twice consists of the transformation from

while(B) { C; }

to the following nested if statements:

if(B) { C; if (B) { C; while(B) { C; } } }

Recently, I thought about how to do that (more or less) elegantly given an abstract syntax tree of the loop. Here my approach in Ocaml. First, we start with a simple language of only boolean expressions and some commands.

type bexp = Random
and cmd =
  Skip
  |Assign
  |Seq of cmd list
  |If of bexp * cmd * cmd
  |While of bexp * cmd

We have a boolean expression Random and the usual commands cmd: Skip, Assignments, Sequences, If, and While constructs. Let’s define a simple loop:

let loop1 = While(Random, Assign)

Which corresponds to something like while(Random) { Assign; }. Obviously, the commands and boolean expressions are not really useful, but that’s just for demonstration purposes — it could easily be replaced with real AST constructs.

Next, let’s write out how we would like to have the first unrolling look like:

let unrolled1 = If(Random, Seq [Assign; loop1], Skip)

Which corresponds to something like if(Random) { Assign; While(Random) { Assign; } else { Skip; }. All we did is taking the body of the loop, wrapping it in an if, given the guard of the body, and concatenating the whole loop to the then-branch.

How do the second and third unrolling look like?

let unrolled2 = If(Random, Seq [Assign;
If(Random, Seq [Assign; loop1], Skip)], Skip)

let unrolled3 = If(Random, Seq [Assign;
If(Random, Seq [Assign;
If(Random, Seq [Assign; loop1], Skip)], Skip)], Skip)

Ok, we see a very repetitive structure (obviously!). Let’s try to write some functions which solve our problem.

The first pattern we see is the following: If(GUARD, Seq[ BODY; REMAINING] , Skip). Basically, we can generalise the stuff written in capitals with arguments of a function:

let buildIfSkip guard body remain = If(guard, Seq[body; remain], Skip)

Given the body and guard of loop1 we could now curry buildIfSkip as follows:

let doRemain = buildIfSkip Random Assign

The function doRemain has only one argument which defines what gets put in REMAINING.

That’s already it, almost! The first unrolling we get by:

doRemain (doRemain loop1)

which produces

If (True, Seq [Assign; If (True, Seq [Assign; While (True, Assign)], Skip)], Skip)

All which is needed now is a function which parametrises all of this. It needs to do the following:

• Take a loop, get the guard and the body of it
• Produce the function doRemain as shown above
• recursively apply doRemain to itself

Here’s the complete function:

let unroll loop n =
   let guard,body = match loop with
     |While(guard,body) -> guard,body
     |_ -> raise Not_found in
   let buildIfSkip guard body remain = If(guard, Seq[body; remain], Skip) in
   let doRemain = buildIfSkip guard body in
   let iterate n f v =
      let rec iter v = function
        0  -> v
        |n -> iter (f v) (n-1) in
      iter v n in
   iterate n doRemain loop

To check we can do the following:

# unroll loop1 3 = unrolled3;;
- : bool = true
#

Feel free to use the code

(source ilachinski.com)

I realized I don’t write a lot about what I’m actually doing day in day out for work. This is partly because it is thought as “hard to describe” to non-computer science people. Today, I want to describe a method which is widely used in the software verification community in an easy way.

The technique is called Abstract Interpretation (AI from now on) and has been first described by Cousot in 1976/77 [1]. Now, to describe AI I’ll directly start with an example also partly taken from [1]:

Imagine you are presented with the following calculation .

Now I’m asking you to tell me the result of this multiplication without the help of a calculator. Obviously, unless you are a scary person, you don’t know the result because it is too complex to calculate in your head. However, when I change the question and ask you to tell me the sign of the result of this multiplication you will tell me instantly that the result is positive. How did you know that? Most probably you used your old highschool knowledge that the multiplication of positive numbers yields a positive result. So you used, without actually realising it, an abstraction of the multiplication operator to get the correct answer. This is a kind of abstract interpretation.

What we learned so far is: Abstract interpretation is replacing the actual domain of the answer (in our case the set of integers) with an abstract domain, in our case the sign domain which has only two elements . Also, it is replacing the normal operations with abstract operations. Our abstract multiplication operation has the following properties on the sign domain:

Now all that is missing is an abstraction function from the concrete domain to the abstract domain. This is defined as follows

Using these definitions we can easily solve the problem from above:

Now you could define more abstract operators on the sign domain and you would end up with a full abstract interpreter for basic mathematical operations. Cool, isn’t it?

To sum up, this technique is simplifying a problem by abstracting away information you don’t need to solve the problem (e.g. only getting the sign of a computation). The nice thing then is that the more abstract version is easier to calculate and the abstract result is saying something about the concrete result!

Of course, the sign domain is very primitive and has only limited use. Real abstract interpreter support many different abstract domains but the idea is always the same.

—-

[1] Cousot, P. and Cousot, R. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los Angeles, California, January 17 – 19, 1977). POPL ‘77. ACM, New York, NY, 238-252. DOI= http://doi.acm.org/10.1145/512950.512973

http://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml