Cache constant RHS value evaluation at runtime

[robin-aws]

Summary

Constants with RHS are currently compiled to nullary functions, which means they are recalculated on every reference at runtime. This is done this way because Dafny permits some initialization patterns that not all target languages allow, so it is a conservative and correct strategy. This can have a severe and surprising runtime cost, however.

Background and Motivation

Example program:

module Foo {

  const X := SomeExpensiveFunction(10000000)

  function SomeExpensiveFunction(n: nat): nat {
    if n == 0 then 0 else SomeExpensiveFunction(n - 1)
  }

  method Main() {
    var n := 0;
    // Using this instead makes the program take less than a second
    // var x := SomeExpensiveFunction(10000000)
    for i := 0 to 10000 {
      n := n + X;
    }
  }
}

The constant X is compiled to:

  public static java.math.BigInteger X()
  {
    return __default.SomeExpensiveFunction(java.math.BigInteger.valueOf(10000000L));
  }

Proposed Feature

The above example should instead compile to something like this (in Java for e.g.):

  public static java.math.BigInteger X()
  {
    if (!__X_populated) {
      __X = __default.SomeExpensiveFunction(java.math.BigInteger.valueOf(10000000L));
      __X_populated = true;
    }
    return __X;
  }

Note that some care will be necessary to support all possible types, and to be threadsafe (the fields above will need to be volatile in Java for example)

Alternatives

Importantly, the lack of this feature cannot be effectively worked around in Dafny source code, as far as I can tell.

It may be possible to detect when it is legal to declare an actual target language constant, but given that is much more technically challenging and risks soundness issues, the simpler improvement above is likely a better short term solution.

[ajewellamz]

It seems to me that, in many cases, Dafny knows the final computed value of SomeExpensiveFunction(), because I can
assert SomeExpensiveFunction() == 42
and so the final code could instead be

public static java.math.BigInteger X()
  {
    return 42;
  }

[robin-aws]

I'm sure there are loads of cases where we can do better. I propose this first step as a simple-to-implement step forwards that ensures all constants are only evaluated once (except in rare race conditions, and even then still safely). We can follow up with optimizing cases after that.