►
From YouTube: Polonius-rustc walkthrough
Description
A walk through the rustc and Polonius code bases, showing how the two are connected.
Paper doc is viewable here: https://paper.dropbox.com/doc/Polonius-Walkthrough-2--AZVdfdGwg3j9xs693~KyChtnAg-Wr90dk3V5DQQem9duos4P
A
A
A
There's
Polonius
and
Polonius
engine
Polonius
is
like
the
data.
The
testing
harness
it's
not
actually
used
by
rusty
blow.
Gnaeus
engine
is
and
within
it,
there's
this
fax
file,
and
this
is
one
of
the
interface
to
rusty
alright,
and
so
it's
totally
generic
over
what
exactly
represents
a
region
alone
or
a
point
in
the
control
flow
graph.
These
are
always
some
new
type
integer.
Basically,
but
the
the
actual
new
types
are
not
in
this
great
there's.
A
No,
it's
generic
might
be
declared
in
rusty
and
so
on,
and
you
have
here
this
basically
one
vector
for
each
of
the
inputs
to
the
analysis,
so
the
one
that
we
are
gonna
look
at
most
closely
today,
I
guess
or
the
one
that
we're
looking
to.
Let's
say:
replace
is
this
region?
Why
that?
And
the
reason
is
that
most
of
these,
like
the
control
flow
graph
edge,
for
example,
is
something
you
can
directly
get
out
of
the
mirror
control
flow
graph.
A
A
It's
just
a
different
representation
of
the
data
structure
and,
to
a
certain
extent,
that's
true
for
for
all
of
these,
a
little
bit
less
so
for
something
like
killed,
which
I
don't
think
we've
even
talked
about,
but
that
basically
says
there's
an
assignment
at
this
location
like
x,
equals
foo
and
there's
a
borrow
of
some
sub
path
of
X,
like
X
dot
bar
and
therefore
you
put
it
in
the
vector.
But
it's
still
fairly
easy
to
understand.
A
lot
of
interpretation
involved.
A
Liveness
is
different
in
liveness.
What's
happening
is
the
compilers?
We're
going
to
see
is
going
to
do
a
live,
miss
computation
of
figuring
out,
what's
live
at
each
point
and
then
encode
the
results
of
that
computation,
which
is
itself
a
fixed
point
computation
into
this
vector
and
that's
kind
of
silly.
It
would
be
better
to
do
we'd
like
to
move
these
like
I,
guess,
that's
the
real
distinction,
anything
that
requires
iteration.
A
A
A
A
So
one
place
we
might
look
at
in
the
bar
checker
there's
this.
This
is
this
module
called
fracks
and
you
can
see
here
that
it
grabs
from
polonius
Engine
the
all
facts,
structure
which
it
renamed
stopped:
the
polonius
all
effects
and-
and
then
we
defined
we
here,
we
export
a
sort
of
version
of
this
that
uses
the
compilers
new
types
all
right,
so
we're
Polonius
talks
about
a
region
in
the
compiler.
A
That's
represented
by
this
data
structure
called
region
vid
where
vid
stands
for
variable,
ID
and
Baro
index
is
what
we
call
a
lone
location
index
is
a
point
in
the
control
flow
graph.
So
you
can
see
that
there
are
they're
just
integers,
but
they
have
their
own
little
local
names.
So
this
is
our
like
local
instantiation
and
then
this
this
trait.
This
is
like
an
extension
trait
to
add
some
methods
to
it,
so
you
can
ask
if
it's
enabled
and
the
right
to
derp.
A
All
that
does
is
on
this
really
dump
these
into
files
that
are
in
the
format
that
Polonius
can
import,
and
the
point
of
that
is
that
rusty
can
run
with
an
option
to
dump
these
files
so
that
you
can
then
run
Polonius
in
a
standalone
way
without
the
rest
of
rusty
and
just
reproduce
the
actual
analysis.
So
that's
where
the
facts
are
like
that's
one
part
of
it.
At
least.
Let's
see
the
next
part
is.
A
A
A
Then
I
create
an
instance
of
the
effects
which
is
empty
and
store
it
in
this
variable,
and
then
we
run-
and
you
can
see
we
give
this
variable,
for
example,
to
the
type
checker
and
that
will
the
type
checker
will
emit
facts
like
that.
One
lifetime
has
to
outlive
another
or
very
1/1
regions
ever
so
it
generates
some
subset
of
facts,
and
then
you
know
here
we're
adding
some
more
facts
into
that
into
that
variable.
A
Saying:
okay:
let's
extend
that
with
the
set
of
universal
regions
or
free
regions
and
so
forth,
and
and
again
here
this
constraint
generation,
so
where
all
these
things
are
basically
populating.
The
facts
table
right
and
the
generate
invalidates.
This
is
saying,
invalidates
this,
how
Polonia
says
well,
this
action
would
be
incompatible
with
that
loan.
At
this
point,
we're
done,
and
you
can
kind
of
see
that
by
the
fact
that
we're
gonna
write
out.
A
If
they've
asked
us
to
write
these
things
to
files,
the
user,
then
we
will
do
so,
and
the
other
thing
we'll
do
here
is
where
we
write
to
the
files.
If
we
do,
our
ask
to
the
other
thing
we'll
do
is
if
we're
asked
to
use
balunia
s--
in
order
to
create
our
errors,
then
we
actually
invoke
polonius
here
right
and
this
output
is
comes
from
the
somewhere
here
comes
from
the
polonius
engine,
so
this
is
actually
the
sort
of
main
way
that
Polonius
executes
and
you
can
see
we
picked
the
algorithm.
A
We
get
it
from
a
string,
but
we
tell
Polonius
to
figure
out
the
algorithm
and
compute
the
result,
and
that
goes
into
this
variable.
Polonius
output,
so
it
will
have
the
either
none
or
it'll
have
the
results
that
Polonius
gives
back.
Let
me
put
them
in
a
ref
counted
things
so
that
we
don't
have
to
so.
We
can
clone
it
because
they're
immutable
once
they
get
created
and
then
Polonius
output
happens
at
that.
A
A
Is
this
data
structure,
and
the
only
thing
in
here
that's
that
these
these
maps
are
all
going
to
be
empty.
These
are
only
used
as
it
says,
for
debugging,
but
it
will
contain
a
list
of
errors
at
each
point.
It's
basically
at
this
point.
There
was
an
error,
because
this
loan,
and
so
the
actual
later
on
the
error
reporting
code
is
gonna.
A
A
Okay,
oh
I,
see
yeah
so
in
the
borough
check-in,
the
type
Jack
there's
the
directory
called
liveness
and
in
this
liveness
code
we
actually.
This
is
this-
is
the
current
aliveness
computation
and
it's
a
little
bit
complicated.
It's
a
little
bit
more
than
just
liveness
in
the
traditional
compiler
sense
of
normally.
That
would
just
be
like.
Is
this
variable
used
later
and
we
do
that,
but
we
distinguish
a
few
different
kinds
of
uses.
A
But
we
do
this
computation
and
we
append
it
in
and
so
what
we're
gonna?
What
our
initial
goal,
I
think
would
be
not
to
change
anything
here,
but
just
to
add
to
it
that
we're
gonna
add
a
new
set
of
facts
which
is
probably
two
things
or
it's
certainly,
where
is
each
variable
defined
and
where
is
it
used
all
right
and
I
mentioned
that
there's
two
kinds
of
uses.
So
let's
see,
let's
scroll
down
a
little
bit,
how
does
this
go
to
work
anyway?
I,
remember.
A
A
A
A
It's
called
it
variables
and
then
there
are
the
variable
definitions.
Probably
that's
it's
like
a
vector
of
V
and
P.
So
a
variable
definition
occurs
at
some
point
and
they'll
be
like
variable.
Regular
use
is,
which
is
also
a
vector
of
V
and
P,
and
we
just
mean
variable
is
regular,
used
point
and
things
like
that,
and
we
could
have
a
variable
drop
uses
to
mean
if
the
variable
is
drop
used
at
some
point
and
drop.
Yours
means
that
it's
that
implicit
drop
I
mentioned
probably
just
start
with
this.
A
So
what
about
this
mapping?
So
if
we
were
going
to
do
liveness
computation,
there's
going
to
be
some
rules
that
are
gonna
say
something
like
the
variable
is
lie.
Let's
say
we
we
have
these
variable
regular
uses,
variable
job
uses
and
so
on,
and
you
might
say
anytime
that
a
variable
is
regular
used
at
a
given
point.
A
A
That
P,
then
it's
going
to
be
live
at
P,
also
right,
so
we
walk
backwards
to
the
control
program.
So
that's
like
our
basic
rule
and
now
what
I
want
to
show
you
now
because
you've
seen
a
lot
of
rules
like
this
is
how
do
you
map
these
sorts
of
rules
into
data
fraud?
It's
not
entirely
obvious,
so
we
won't
map
that
actual
rule,
because
we
don't
have
that
rule
yet,
but
we'll
map
a
different
rule
and
will
use
go
if
we
go
to
the
naive
computation,
let's
find
a
subset
is
pretty
similar.
A
So
if
you
recall
there
were
rules
in
the
naive
computation
make
this
a
little
bigger
like
this
one.
Well,
let's
start
with
a
simple
one:
this
is
a
transitive
rule.
This
says
if
at
some
point,
P
R
1
is
a
subset
of
R,
2
and
R.
2
is
a
subset
of
R
3,
then
R
1
is
a
subset
of
R
3,
pretty
simple
and
the
way
that
that
gets
encoded
I
take
this
over
to
my
our
data.
Frog
works.
So
this
is
the.
A
A
So
what
what
this
so
oh
I
see?
We
have
this
iteration.
So,
first
of
all,
there's
gonna
be
the
first
thing
in
data
fog.
You
always
have
is
some
kind
of
iteration
and
what
that
basically
means
is.
This
is
a
computation
and
an
iteration
can
have
associated
with
it
the
various
variables
which
represent
the
relations
your
computing,
and
so
when
you
write
iteration
that
variable
you
give
it
some
some
types
region.
This
correspond
to.
You
know,
region
and
region,
point
region,
region
point.
So
it's
a
tuple.
A
Basically,
this
tuple
is
what
the
variable
consists
of
a
set
of
those
tuples
and
then
there's.
The
reason
that
thing
is
called
iteration
is
because
there's
actually
a
bit
of
russ
code
here
you
know
we're
doing
a
fixed
point
iteration,
which
means
we're
continually
working,
adding
things
until
we
get
no
more
changes.
So
the
way
that
happens
in
rust,
like
data
frog
itself,
is
just
some
libraries
that
you
can
invoke
and
the
actual
iteration
is
here.
A
So
we
keep
going
while
it's
changed
and
then
we
do
this
call-
and
this
corresponds
to
this
rule
right
and
what
this
from
join
does.
Is.
It
says
add
in
to
so
the
current
value
of
subset.
Add
any
new
tuples
that
you
get
by
joining
in
the
database
sense.
These
two
other
variables
will
come
to
those
variables
in
a
second,
so
joining
meaning
take
the
set
of
tuples
from
one
and
the
set
from
the
other
and
see
where
they
have
overlap.
A
So
in
this
case,
these
are
expected
to
always
be
two
tuples
where
there's
like
a
key
and
a
value
one
and
a
key
and
a
value,
two,
that's
the
type.
These
types
have
to
be
mapped
to
that,
and
so
these
keys,
wherever
the
keys
match
up
you
get
it.
You
get
a
callback.
So
what
you
have
here
is
this
is
the
key,
and
this
is
the
first
value,
and
this
is
the
second
value.
So
so
what
is
this
r2p
and
r1p
going
on?
A
Well,
these
are
also
variables
they're,
like
temporary
variables,
basically
they're,
not
the
real.
They
don't
even
appear
in
the
data
log
but
they're
like
intermediate
variables
that
you
would
use
and
the
way
they're
defined
just
exactly
the
same
as
subsets,
except
to
be
organized
there,
like
a
ver
like
a
database
index,
which
that
means
just
reorganized
to
identify
what
the
key
is
right.
A
So
we
this
from
map
says,
add
into
subset
r1p
all
the
tuples
that
that
are
in
subset
but
apply
this
closure
first,
so
we're
taking
the
subset
tuple,
which
is
the
three
things
all
equal
and
we're
reorganizing
them,
so
that
we
have
the
key
we
want,
which
is
basically
we
look
here.
We
see.
Oh
this
thing.
What
this
have
in
common
is
that
they're
there
at
a
specific
point
and.
A
R2
appears
in
both
of
them
right,
so
we
want
to
join
where
the
second
part
of
this
tuple
is
equal
to
the
first
part
of
this
tuple
and
the
third
parts
of
the
tuple
are
equal.
So
first
we
extract
out
the
first
part
and
we
make
a
map
that
has
the
first
part
and
the
point,
the
first
region
and
the
point,
and
then
we
have
another
one
or
a
to
P,
which
is
basically
the
same
except
it's
gonna
pull
out
the
second
part,
and
then
we
join
those
together
and
now.
A
So
what
we
essentially
have
here
is
the
r2p
and
the
r1p,
and
now
you
can
start
to
see
where
the
naming
convention
comes
from.
This
underscore
like
r2p,
is
telling
you
okay.
This
is
the
key.
This
is
the
same
as
subset,
but
with
this
key-
and
this
is
the
same
as
subset
that
key,
and
so
when
we
get
the
call
back
here
that,
where
these
names
come
from,
this
are
that
kind
of
comes
from
this.
A
This
data
log
code,
the
r1,
is
the
second
half
of
this
tuple,
which,
in
our
data
log
code,
is
r1,
and
the
r3
is
the
second
half
of
this
tuple,
which
would
be
that
r3
and
then
this
is
the
final
result:
r1
r3
RP,
so
you
can
kind
of
make
this
in
a
fairly
mechanical.
It's
like
hard,
it's
not
trivial,
but
it's
mechanical
to
convert
the
data
log
rules
into
this
data
fraudulence.
That's
the
basic
structure!
There
is
some
more
fancy
stuff.
A
You
can
do
in
particular,
there's
from
leap
join,
which
is
more
efficient
and
kind
of
nifty,
but
also
kind
of
wacky.
Let's
see
if
we
can
walk
through
how
it
works,
see
if
I
can
remember
how
it
works.
So
what
this?
What
this
rule
is
trying
to
do?
This
is
somewhat
similar
to
the
rule
that
liveness
will
ultimately
want
what
this
rule
is
trying
to.
That's
the
one
thing
I
hate
about
not
the
one
thing,
but
it
is
one
thing
that
I
hate
about
flux
paper
when
you
paste
in
anyway,
so
right.
A
A
So
that's
what
a
variable
is
in,
and
data
frog,
I
didn't
actually
say
that
explicitly.
There's
actually
two
concepts,
state
variables
and
relations
and
relations
are
essentially
your
inputs
from
the
point
of
view
of
any
computation,
so
they're
not
changing
during
the
iteration
they're
fixed
and
the
variables
are
the
things
that
are
actually
growing
at
each
round.
Right
and
here
we
have
this-
the
only
fall
of
these
are
relations.
These
are
all
base
inputs
that
don't
grow
with
the
exception
of
subsets
and
that's
also
the
output.
A
So
there's
like
a
recursive
thing
going
on,
and
in
that
case
we
have
a
particular
optimized
method,
called
from
leap
join
that
can
be
more
efficient
in
the
way
that
it's
implemented,
that
you
can
use
and
what
it
does
so
how
it
works
is.
Actually
it
doesn't
matter
that
they're
the
same
I,
don't
think
it
just
matters
that
there's
one
variable
and
and
then
some
number
of
relations
that
it
gets
combined
with
and
so
there's
the
same
basic
structure.
A
You
call
from
leap
join
and
that
adds
things
into
subsets,
and
then
you
give
that
one
variable
here,
that's
the
first
parameter
and
then
the
rest
of
the
parameters
are
a
definition
are
derived
from
the
relations.
So
the
things
that
aren't
changing
the
inputs-
and
they
tell
you
how
it
should
be
like
combined
with
the
value
of
that
variable.
A
So
in
this
case
the
first
one
extend
with
what
that
says,
is
first
look
at
this
tuple
here,
r1
r2
P
lets
you
see
that
in
each
case
it's
r1,
r2
P,
we're
gonna
pull
out
just
the
p
value,
and
oh,
this
config
edge
relation
yeah.
This
is
just
config
edge
like
so
so
we're
gonna.
Take
that
whatever
gets
returned
from
here
we're
gonna
match.
This
has
to
be
a
2-tuple,
we're
gonna
match
to
the
first
part
and
then
and
then
we're
gonna.
A
Take
the
we're
going
to
match
to
the
first
part
and
we'll
take
that
Q
value,
and
we
will
use
it
later
on
to
make
new
tuples
with
right.
So
that's
what
happens
here
so
basically
here
we're
finding
we're
basically
doing
this
joint
and
then
actually
I'm
a
little
surprised
by
this,
but
that's
okay
and
then
what
this
is
saying
is.
A
Right
kind
of
oh
I
see
right
because
these
Q's
all
have
to
be
the
same,
so
kind
of
the
same
thing
same
kind
of
join,
except
that
in
order
to
all
of
these
extend,
which
calls
are
going
to
produce
a
new
Q
value,
basically
they're
all
proposing
new.
What
is
a
possible
value
for
Q,
because
all
the
rest
of
the
variables
came
from
the
input.
A
So
that's,
okay
and
that'll
propose
a
queue
and
this
will
propose
a
queue
and
then
for
all
the
things
that
they
all
proposed
in
common
you'll,
get
a
callback
where
here
was
the
input
value
that
we
passed
to
each
prisoner,
and
here
was
the
queue
they
all
agreed
on
and
now
you
can
return
a
new
value.
Something
roughly
like
that
and
there's
some
other
methods
and
options
so
extend
with
is
the
basic
one
that
lets
you
say,
pull
out
some
part
of
the
variable
use.
A
A
So
that
would
be
useful
for
something
like
not
variable
to
find
right
and
there's
some
other
things:
filter,
filter
width
and
filter
anti,
which
is
kind
of
the
same
thing
except
here:
you're
always
joining
the
first
half
and
the
second
half
you're,
either
you're,
either
proposing
or
killing
right.
So,
if
you
say
extend
anti,
then
it
would
say
anytime
that
you
have
a
match
and
it
has
a
Q
that
Q
is
not
part
of
the
output
and
filter
within
filter
anti.
A
Take
these
entire
tuples
here
or
these
tuples
or
I
forget
exactly,
but
they
don't
propose
new.
They
don't
don't
have
that
key
value
of
thing,
it's
more
like
you're.
Just
checking
is
this
tuple
part
of
the
set
or
not
anyway,
we
can
get
to
that,
but
that's
it
I'm
after
I
have
to
go,
but
we
just
made
it
with
a
cover
E
of
how
sort
of
data
frog
and
Polonius
work
we
won't
get
to
this.
But
that's
okay,
it's
not
very
important,
and
we
kind
of
did
this.