State built up before a loop is lost

[sebmarkbage]

(function () {
  var n = __abstract('number', '(5)');
  var arr = {0: 'a', 1: 'b'};
  var i = 2;
  do {
    arr[i] = 'x';
    i++;
  } while(i < n);
  result = arr;
})();

If a loop is building up state before a loop, it is lost once the unknown property is widened. But that state is not restored by the loop.

[hermanventer]

Before we can hope to deal with this, we'll need a range domain (#1066).

[sebmarkbage]

If you change the numeric properties to named ones, there's still a problem though.

[hermanventer]

Yes, with loops you have to widen and once you widen, precision is lost. Range domains let you regain some of this precision. If you range over an unbounded collection of strings and use them as property names, it's pretty much game over.

[sebmarkbage]

When we SetPartial outside a loop, then we weakly update the known properties. Is there a reason we can't do that for widened properties?

[hermanventer]

We can do weak updates only if there is a join condition that is stable. A widened property name does not fit the bill.

[sebmarkbage]

The interesting thing is that something like this works:

  var arr = {};
  var i = 0;
  do {
    arr[i] = i === 0 ? 'a' : i === 1 ? 'b' : 'x';

So I guess it's just important that the join condition gets evaluated inside the loop. Not after the loop.

[sebmarkbage]

Wouldn’t snapshotting be an appropriate solution here?

In general we’re ok with losing precision later as long as we can serialize the state of an object as it was before we entered the lost precision (eg havocing or Object.assign).

[hermanventer]

If you want to use the object before the loop, a snapshot should do the trick. I'm not sure if we can do this without the aid of an annotation. Could you provide a complete test case that represents the scenario you care about?