WhileyCompiler icon indicating copy to clipboard operation
WhileyCompiler copied to clipboard

Improve MoveAnalysis Phase

Open DavePearce opened this issue 8 years ago • 1 comments

(see also #706)

Currently, MoveAnalysis has two distinct limitations which should be addressed:

  1. Does not distinguish moves from borrows. Consider the expression arr[i] for some array arr. The analysis currently marks the variable access arr as a move. But this is not correct as, by definition, a variable should be undefined after a move. Thus, following the semantics properly, we should not be able to use arr after this access. In fact, what we're doing is temporarily borrowing arr. Therefore, we want to distinguish this I think.

  2. Does not perform live variables analysis. Currently, this is no live variables analysis being performed. This means some potential moves are not being spotted. Furthermore, it means the analysis is actually only ever spotting borrows and never spots any real moves.

Another limitation is related to multiple returns. Consider this example:

function f(int[] xs) -> (int[] ys, int[] zs):
    return xs,xs

At the moment, both occurrences of xs are copied. But, in fact, the last one does not need to be.

DavePearce avatar Sep 27 '17 02:09 DavePearce

In addition, there are problems related to field and array accesses (and possibly others). As an example, consider this:

method f(int[][] xs) :
   //
   int[] ys = xs[0]
   ys[0] = ys[0] + 1
   assert xs[0][0] != ys[0]

This should evaluate without problem unless there is hidden aliasing between xs[0] and ys. At the moment, this translates into something like the following:

static void f(BigInteger[][] xs) {
  BigInteger[] ys = xs[0];
  ys[0] = ys[0] + 1;
  assert !xs[0][0].equals(ys[0]);
}

We can clearly see the problem is that xs[0] is not cloned before being loaded into ys.

Realistically, we need to consider that record and array accesses can either be copying, borrowing or moving.

DavePearce avatar Sep 28 '17 02:09 DavePearce