f9c8b5e93d
This PR fixes theoretical leaks in the handling of `Array.get!Internal`
in the code generator.
Currently, the code generator assumes that the value returned by
`get!Internal` is derived from the
`Array` argument. However, this does not generally hold up as we might
also return the `Inhabited`
value in case of an out of bounds access (recall that we continue
execution after panics by
default). This means that we sometimes convert an `Array.get!Internal`
to
`Array.get!InternalBorrowed` when we are not allowed to do so because in
the panic case the
`Inhabited` instance can be returned and if it is an owned value it is
going to leak.
The fix consists of adapting several components to this change:
1. `PropagateBorrow` will only mark the derived value as forcibly
borrowed if both the `Inhabited`
and `Array` argument are forcibly borrowed.
2. `InferBorrow` will do the same for its data flow analysis
3. The derived value analysis of `ExplicitRC` is extended from a derived
value tree to a derived
value graph where a value may have more than one parent. We only
consider a value borrowed if all
of its parents are still accessible. Then `get!Internal` is equipped
with both its `Inhabited`
and its `Array` parent.
These changes are sufficient for correctness on their own. However, they
are going to break
`get!Internal` to `get!InternalBorrowed` conversion in most places. This
happens because almost all
`Inhabited` instances are going to be constants. Currently reads from
constants yield semantically
owned values and thus block the `get!InternalBorrowed` conversion. We
would thus prefer for these
constants to be treated as borrows instead.
The owned return is implemented in two ways at the moment:
1. In the C code emitter we do not need to do anything as constants are
marked persistent to begin
with
2. In the interpreter whenever a constant is pulled from the constant
cache it is `inc`-ed and then
later `dec`-ed somewhere (potentially using a `dec[persistent]` which is
a no-op in C)
This PR changes the semantics of constant reads to instead be borrows
from the constant (they can be
cutely interpreted as "being borrowed from the world"). This enables
many `get!Internal` to have
both their arguments be marked as borrowed and thus still converted to
`get!InternalBorrowed`. Note
that this PR does not yet change the semantics of the interpreter to
account for this
(it will be done in a part 2) and thus introduces (very minor) leaks
temporarily.
Furthermore, we observed code with signatures such as the following:
```lean
@[specialize]
def foo {a : Type} [inst : Inhabited a] (xs : Array a) (f : a -> a -> Bool) ... :=
...
let x := Array.get!Internal inst xs i
...
```
being instantiated with `a := UInt32`. This poses a challenge because
`Inhabited` is currently
marked as `nospecialize`, meaning that we are sometimes going to end up
with code such as:
```
def foo._spec (inst : UInt32) (xs : @&Array UInt32) ... :=
...
let inst := box inst
let x := Array.get!Internal inst xs i
dec inst
...
```
Here `xs` itself was inferred as borrowed, however, the `UInt32`
`Inhabited` instance was not
specialized for (as `Inhabited` is marked `nospecialize`) and thus needs
to be boxed. This causes
the `inst` parameter to `get!Internal` to be owned and thus
`get!InternalBorrowed` conversion fails.
This PR marks `Inhabited` as `weak_specialize` which will make it get
specialized for in this case,
yielding code such as:
```
def foo._spec (xs : @&Array UInt32) ... :=
...
let inst := instInhabitedUInt32
let inst := box inst
let x := Array.get!Internal inst xs i
dec inst
...
```
Fortunately the closed term extractor has support for precisely this
feature and thus produces:
```
def inst.boxed_const :=
let inst := instInhabitedUInt32
let inst := box inst
return inst
def foo._spec (xs : @&Array UInt32) ... :=
...
let inst := inst.boxed_const
let x := Array.get!Internal inst xs i
...
```
As described above reads from constants are now interpreted as borrows
and thus the conversion to
`get!InternalBorrowed` becomes legal again.
352 lines
10 KiB
Text
352 lines
10 KiB
Text
[Compiler.IR] [result]
|
|
def Exp.ctorIdx (x_1 : @& tobj) : tobj :=
|
|
case x_1 : tobj of
|
|
Exp.var →
|
|
let x_2 : tagged := 0;
|
|
ret x_2
|
|
Exp.app →
|
|
let x_3 : tagged := 1;
|
|
ret x_3
|
|
Exp.a1 →
|
|
let x_4 : tagged := 2;
|
|
ret x_4
|
|
Exp.a2 →
|
|
let x_5 : tagged := 3;
|
|
ret x_5
|
|
Exp.a3 →
|
|
let x_6 : tagged := 4;
|
|
ret x_6
|
|
Exp.a4 →
|
|
let x_7 : tagged := 5;
|
|
ret x_7
|
|
Exp.a5 →
|
|
let x_8 : tagged := 6;
|
|
ret x_8
|
|
def Exp.ctorIdx._boxed (x_1 : tobj) : tobj :=
|
|
let x_2 : tobj := Exp.ctorIdx x_1;
|
|
dec x_1;
|
|
ret x_2
|
|
[Compiler.IR] [result]
|
|
def Exp.ctorElim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
|
|
case x_1 : tobj of
|
|
Exp.var →
|
|
let x_3 : u32 := sproj[0, 0] x_1;
|
|
dec x_1;
|
|
let x_4 : tobj := box x_3;
|
|
let x_5 : tobj := app x_2 x_4;
|
|
ret x_5
|
|
Exp.app →
|
|
let x_6 : tobj := proj[0] x_1;
|
|
inc x_6;
|
|
let x_7 : tobj := proj[1] x_1;
|
|
inc x_7;
|
|
dec x_1;
|
|
let x_8 : tobj := app x_2 x_6 x_7;
|
|
ret x_8
|
|
default →
|
|
dec x_1;
|
|
ret x_2
|
|
[Compiler.IR] [result]
|
|
def Exp.ctorElim (x_1 : ◾) (x_2 : @& tobj) (x_3 : tobj) (x_4 : ◾) (x_5 : tobj) : tobj :=
|
|
let x_6 : tobj := Exp.ctorElim._redArg x_3 x_5;
|
|
ret x_6
|
|
def Exp.ctorElim._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) : tobj :=
|
|
let x_6 : tobj := Exp.ctorElim x_1 x_2 x_3 x_4 x_5;
|
|
dec x_2;
|
|
ret x_6
|
|
[Compiler.IR] [result]
|
|
def Exp.var.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
|
|
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def Exp.var.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
|
|
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
|
|
ret x_5
|
|
[Compiler.IR] [result]
|
|
def Exp.app.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
|
|
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def Exp.app.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
|
|
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
|
|
ret x_5
|
|
[Compiler.IR] [result]
|
|
def Exp.a1.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
|
|
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def Exp.a1.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
|
|
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
|
|
ret x_5
|
|
[Compiler.IR] [result]
|
|
def Exp.a2.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
|
|
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def Exp.a2.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
|
|
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
|
|
ret x_5
|
|
[Compiler.IR] [result]
|
|
def Exp.a3.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
|
|
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def Exp.a3.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
|
|
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
|
|
ret x_5
|
|
[Compiler.IR] [result]
|
|
def Exp.a4.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
|
|
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def Exp.a4.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
|
|
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
|
|
ret x_5
|
|
[Compiler.IR] [result]
|
|
def Exp.a5.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
|
|
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def Exp.a5.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
|
|
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
|
|
ret x_5
|
|
[Compiler.IR] [result]
|
|
def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
|
|
case x_1 : tobj of
|
|
Exp.var._impl →
|
|
dec x_3;
|
|
let x_9 : u32 := sproj[0, 8] x_1;
|
|
dec x_1;
|
|
let x_10 : tobj := box x_9;
|
|
let x_11 : tobj := app x_2 x_10;
|
|
ret x_11
|
|
Exp.app._impl →
|
|
dec x_2;
|
|
let x_12 : tobj := proj[0] x_1;
|
|
inc x_12;
|
|
let x_13 : tobj := proj[1] x_1;
|
|
inc x_13;
|
|
dec x_1;
|
|
let x_14 : tobj := app x_3 x_12 x_13;
|
|
ret x_14
|
|
Exp.a1._impl →
|
|
dec x_3;
|
|
dec x_2;
|
|
inc x_4;
|
|
ret x_4
|
|
Exp.a2._impl →
|
|
dec x_3;
|
|
dec x_2;
|
|
inc x_5;
|
|
ret x_5
|
|
Exp.a3._impl →
|
|
dec x_3;
|
|
dec x_2;
|
|
inc x_6;
|
|
ret x_6
|
|
Exp.a4._impl →
|
|
dec x_3;
|
|
dec x_2;
|
|
inc x_7;
|
|
ret x_7
|
|
Exp.a5._impl →
|
|
dec x_3;
|
|
dec x_2;
|
|
inc x_8;
|
|
ret x_8
|
|
def Exp.casesOn._override._redArg._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) : tobj :=
|
|
let x_9 : tobj := Exp.casesOn._override._redArg x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8;
|
|
dec x_8;
|
|
dec x_7;
|
|
dec x_6;
|
|
dec x_5;
|
|
dec x_4;
|
|
ret x_9
|
|
[Compiler.IR] [result]
|
|
def Exp.casesOn._override (x_1 : ◾) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) (x_9 : @& tobj) : tobj :=
|
|
case x_2 : tobj of
|
|
Exp.var._impl →
|
|
dec x_4;
|
|
let x_10 : u32 := sproj[0, 8] x_2;
|
|
dec x_2;
|
|
let x_11 : tobj := box x_10;
|
|
let x_12 : tobj := app x_3 x_11;
|
|
ret x_12
|
|
Exp.app._impl →
|
|
dec x_3;
|
|
let x_13 : tobj := proj[0] x_2;
|
|
inc x_13;
|
|
let x_14 : tobj := proj[1] x_2;
|
|
inc x_14;
|
|
dec x_2;
|
|
let x_15 : tobj := app x_4 x_13 x_14;
|
|
ret x_15
|
|
Exp.a1._impl →
|
|
dec x_4;
|
|
dec x_3;
|
|
inc x_5;
|
|
ret x_5
|
|
Exp.a2._impl →
|
|
dec x_4;
|
|
dec x_3;
|
|
inc x_6;
|
|
ret x_6
|
|
Exp.a3._impl →
|
|
dec x_4;
|
|
dec x_3;
|
|
inc x_7;
|
|
ret x_7
|
|
Exp.a4._impl →
|
|
dec x_4;
|
|
dec x_3;
|
|
inc x_8;
|
|
ret x_8
|
|
Exp.a5._impl →
|
|
dec x_4;
|
|
dec x_3;
|
|
inc x_9;
|
|
ret x_9
|
|
def Exp.casesOn._override._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) (x_9 : tobj) : tobj :=
|
|
let x_10 : tobj := Exp.casesOn._override x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9;
|
|
dec x_9;
|
|
dec x_8;
|
|
dec x_7;
|
|
dec x_6;
|
|
dec x_5;
|
|
ret x_10
|
|
[Compiler.IR] [result]
|
|
def Exp.var._override (x_1 : u32) : tobj :=
|
|
let x_2 : u64 := UInt32.toUInt64 x_1;
|
|
let x_3 : u64 := 1000;
|
|
let x_4 : u64 := UInt64.add x_2 x_3;
|
|
let x_5 : obj := ctor_0.0.12[Exp.var._impl];
|
|
sset x_5[0, 0] : u64 := x_4;
|
|
sset x_5[0, 8] : u32 := x_1;
|
|
ret x_5
|
|
def Exp.var._override._boxed (x_1 : tobj) : tobj :=
|
|
let x_2 : u32 := unbox x_1;
|
|
dec x_1;
|
|
let x_3 : tobj := Exp.var._override x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def Exp.hash._override (x_1 : @& tobj) : u64 :=
|
|
case x_1 : tobj of
|
|
Exp.var._impl →
|
|
let x_2 : u64 := sproj[0, 0] x_1;
|
|
ret x_2
|
|
Exp.app._impl →
|
|
let x_3 : u64 := sproj[2, 0] x_1;
|
|
ret x_3
|
|
default →
|
|
let x_4 : u64 := 42;
|
|
ret x_4
|
|
def Exp.hash._override._boxed (x_1 : tobj) : obj :=
|
|
let x_2 : u64 := Exp.hash._override x_1;
|
|
dec x_1;
|
|
let x_3 : obj := box x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def Exp.app._override (x_1 : tobj) (x_2 : tobj) : tobj :=
|
|
let x_3 : u64 := Exp.hash._override x_1;
|
|
let x_4 : u64 := Exp.hash._override x_2;
|
|
let x_5 : u64 := mixHash x_3 x_4;
|
|
let x_6 : obj := ctor_1.0.8[Exp.app._impl] x_1 x_2;
|
|
sset x_6[2, 0] : u64 := x_5;
|
|
ret x_6
|
|
[Compiler.IR] [result]
|
|
def Exp.a1._override : tobj :=
|
|
let x_1 : tagged := ctor_2[Exp.a1._impl];
|
|
ret x_1
|
|
[Compiler.IR] [result]
|
|
def Exp.a2._override : tobj :=
|
|
let x_1 : tagged := ctor_3[Exp.a2._impl];
|
|
ret x_1
|
|
[Compiler.IR] [result]
|
|
def Exp.a3._override : tobj :=
|
|
let x_1 : tagged := ctor_4[Exp.a3._impl];
|
|
ret x_1
|
|
[Compiler.IR] [result]
|
|
def Exp.a4._override : tobj :=
|
|
let x_1 : tagged := ctor_5[Exp.a4._impl];
|
|
ret x_1
|
|
[Compiler.IR] [result]
|
|
def Exp.a5._override : tobj :=
|
|
let x_1 : tagged := ctor_6[Exp.a5._impl];
|
|
ret x_1
|
|
[Compiler.IR] [result]
|
|
def f._closed_0 : tobj :=
|
|
let x_1 : u32 := 10;
|
|
let x_2 : tobj := Exp.var._override x_1;
|
|
ret x_2
|
|
def f._closed_1 : tobj :=
|
|
let x_1 : tagged := ctor_5[Exp.a4._impl];
|
|
let x_2 : tobj := f._closed_0;
|
|
inc x_2;
|
|
let x_3 : tobj := Exp.app._override x_2 x_1;
|
|
ret x_3
|
|
def f._closed_2 : u64 :=
|
|
let x_1 : tobj := f._closed_1;
|
|
let x_2 : u64 := Exp.hash._override x_1;
|
|
ret x_2
|
|
def f : u64 :=
|
|
let x_1 : u64 := f._closed_2;
|
|
ret x_1
|
|
[Compiler.IR] [result]
|
|
def g (x_1 : @& tobj) : u8 :=
|
|
case x_1 : tobj of
|
|
Exp.a3._impl →
|
|
let x_2 : u8 := 1;
|
|
ret x_2
|
|
default →
|
|
let x_3 : u8 := 0;
|
|
ret x_3
|
|
def g._boxed (x_1 : tobj) : tagged :=
|
|
let x_2 : u8 := g x_1;
|
|
dec x_1;
|
|
let x_3 : tagged := box x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def hash' (x_1 : @& tobj) : tobj :=
|
|
case x_1 : tobj of
|
|
Exp.var._impl →
|
|
let x_2 : u32 := sproj[0, 8] x_1;
|
|
let x_3 : tobj := UInt32.toNat x_2;
|
|
ret x_3
|
|
Exp.app._impl →
|
|
let x_4 : tobj := proj[0] x_1;
|
|
let x_5 : tobj := proj[1] x_1;
|
|
let x_6 : tobj := hash' x_4;
|
|
let x_7 : tobj := hash' x_5;
|
|
let x_8 : tobj := Nat.add x_6 x_7;
|
|
dec x_7;
|
|
dec x_6;
|
|
ret x_8
|
|
default →
|
|
let x_9 : tagged := 42;
|
|
ret x_9
|
|
def hash'._boxed (x_1 : tobj) : tobj :=
|
|
let x_2 : tobj := hash' x_1;
|
|
dec x_1;
|
|
ret x_2
|
|
[Compiler.IR] [result]
|
|
def getAppFn (x_1 : @& tobj) : tobj :=
|
|
case x_1 : tobj of
|
|
Exp.app._impl →
|
|
let x_2 : tobj := proj[0] x_1;
|
|
let x_3 : tobj := getAppFn x_2;
|
|
ret x_3
|
|
default →
|
|
inc x_1;
|
|
ret x_1
|
|
def getAppFn._boxed (x_1 : tobj) : tobj :=
|
|
let x_2 : tobj := getAppFn x_1;
|
|
dec x_1;
|
|
ret x_2
|
|
[Compiler.IR] [result]
|
|
def Exp.f (x_1 : @& tobj) : tobj :=
|
|
let x_2 : tobj := getAppFn x_1;
|
|
ret x_2
|
|
def Exp.f._boxed (x_1 : tobj) : tobj :=
|
|
let x_2 : tobj := Exp.f x_1;
|
|
dec x_1;
|
|
ret x_2
|