Tried to run &inator on a simple program:
int main() {
return 0;
}&inator segfaulted.
After some debugging, found that the segfault occurs on line 50 in constraints/datatypes/loan.rs:
ctx.datatypes.insert(Self::CONTEXT_KEY, builder.finish());My current theory is that the data type that we are trying to build here has no variants, which somehow causes a segfault in Z3.
Based on running the following Z3 code on the playground, it seems like having zero variants is not valid.
(declare-datatypes () ((Foo)))Now looking for why there are zero variants
ctx.rvals.borrowing (accessed by ctx.rvals.borrow_typelabs()) is empty, which means there are no datatype variants produced.
ctx.rvals is built in src/analysis/rvals.rs in Rvalues::new on line 30.
LATER: what does the
rvalsfield represent?
In Rvalues::new, it looks like certain IR nodes add a value to the borrowing map.
borrowing is tracking type labels for some reason.
Why are we tracking type labels in borrowing?
NOTE: type labels are basically just a way to identify AST nodes
When I come back, I need to look at Rvalues::new to see why a type label would be added to the borrowing map.