►
Description
Memory safety is one of the key selling points of Rust. However, even the Rust compiler is not omniscient, so sometimes programmers need to resort to "unsafe" code and take on the responsibility of ensuring memory safety themselves. In this talk I will introduce key terms surrounding unsafe code such as "undefined behavior" and "soundness", and explain how to write unsafe code in a systematic way that reduces the chance of getting it wrong. I will also demonstrate how you can use Miri to check your unsafe code for otherwise hard-to-detect bugs.
Slides: https://github.com/rust-zurichsee/meetups/tree/master/2023-06-08_miri-simd-hir
Ralf's Blog: https://ralfj.de/blog/
Would you like to chat or give a talk? Join us in our Matrix room:
https://matrix.to/#/#rust-zuerisee:matrix.coredump.ch
Chapters:
00:00 Introduction
01:45 Rust is a memory-safe language
08:49 Common misconceptions with unsafe code
18:12 Examples of Undefined Behavior
44:28 Questions
B
This
is
meant
to
be
interactive,
I'm,
hoping
for
tons
of
questions,
because
otherwise
I
will
not
have
enough
material
to
fill
45
minutes.
So
please
ask
away
any
time
during
the
talk
when
I
say
something
that's
unclear,
I
hope,
I
hope
at
least
some
of
the
things
that
I
say
will
surprise
some
people
here
and
and
incur
some
follow-up
questions.
Can
we
close
the
door
all
right?
B
So,
let's,
let's
start
with
the
usual
kind
of
high
level
selling
point
that
we
that
we
tell
other
people
about
rust,
which
is
that
rust
is
a
memory
saved
language.
So
the
compiler
guarantees
that
all
sorts
of
bad
things
do
not
happen.
In
your
program,
there's
no
program
is
not
going
to
access
memory
out
of
bounds
or
out
of
time
it's
not
going
to
execute
the
wrong
code
by
executing
some
kind
of
Shell
Code
or
whatever
nonsense
might
happen.
B
It's
not
going
to
have
any
data
races,
a
bunch
of
like
pretty
fundamental
flaws
that
plague
software
all
day
and
it
cause
security
issues
and
crashes,
do
not
happen
in
Rust.
That's
the
idea,
except,
of
course,
there's
a
big
asterisk
here,
because
there
is
this
thing
called
unsafe
code
and
an
unsafe
code.
You
can
do
all
sorts
of
nastiness
like
take
a
pointer
to
something,
do
some
arithmetic
to
take
it
out
of
bounds
and
then
do
an
access,
and
now
we
do
have
another
point
to
access,
even
though
this
is
rust.
B
So
most
of
the
rust
code
out
there
is
completely
written
in
safe
code.
This
talk
is
not
concerned
with
that.
This
talk
is
concerned
with
the
I.
Don't
have
data
one
percent
I,
don't
know
the
small
fraction
of
rust
code
that
has
to
use
unsafe
for
various
reasons.
Unsafe
exists
for
good
reasons.
We
needed
to
be
able
to
write
low
level
high
performance
code,
that's
correct
for
reasons
which
are
too
complicated
for
the
compiler
to
understand,
but
it's
a
very
sharp
knife
and
we
have
to
be
super
careful
in
how
we
use
it.
B
So,
let's
start
a
bit
by
seeing
just
how
sharp
this
knife
is
once
you
start
writing
unsafe
rust.
Guaranteeing
memory
is
safety.
Guaranteeing
all
these
nice
property
is
your
responsibility,
and
this
the
like
a
nice
way
to
think
about
this-
is
that
you're
kind
of
entering
a
contract
with
the
compiler
we're
both
parties
have
obligations
and
kind
of
Rights
or
privileges,
and
the
key
obligation
of
both
sides
is
that,
on
the
one
hand,
the
compiler
is
obligated
to
generate
a
binary
that
when
you
run
it
does
the
thing
that
matches
the
source
code.
B
You
wrote,
but
there's
also
an
obligation
on
your
side,
which
is
that
you
have
to
follow
the
rules
you.
You
must
not
do
things
like
that.
You
must
not
perform
other
forms,
memory,
accesses
or
all
sorts
of
other
things,
and
this
application
is
not
to
be
taken
lightly.
If
you
break
that
obligation,
all
sorts
of
weird
stuff
can
happen.
This
might
look
like
a
nice
magical,
Wonderland
and
a
good
drug
trip,
or
something,
but
really
it's
more
like
a
nightmare
drug
trip
in
in
our
reality.
B
B
B
True
at
the
bottom
of
this
here
is
a
little
thing
with
the
main
function
which
calls
that
function
and
then,
if
it
returns
false
states
that
the
bad
thing
happened
and
if
you
run
this
on
current
stable,
rust,
now
I
hope
the
demo
gods
are
with
me,
then
the
impossible
has
in
fact
happened.
This
is
the
kind
of
stuff
that
happens
that
can
happen
when
you
break
your
part
of
the
obligation.
B
Do
not
do
not
ignore
the
obligation.
Of
course,
the
annoying
thing
is
that
in
many
cases
like,
if
you
change
this
code,
just
a
bit-
maybe
like
that,
then
the
impossible
will
not
happen
anymore.
So
it's
not
like
you
can
rely
on
strange
stuff
happening.
It's
just
sometimes
strange
stuff
might
happen,
and
it
might
not
happen
on
Mondays,
but
it
might
happen
on
Tuesdays.
B
So
this
strange
stuff
happening
you
failing
to
uphold
your
obligation
as
an
unsafe
code
author.
That
is
what
we
call
undefined
behavior
and
rust,
and
you
might
have
followed
away
later
term,
which
I
want
to
briefly
talk
about.
Even
though
most
of
this
talk
will
be
about
undefined
Behavior.
The
letter
term
is
soundness,
so
soundness
is
a
property
of
a
function
that
you
write,
like
imagine,
you're
a
library
create
author
you're
using
some
unsafe
code
internally,
but
you're
a
good
citizen,
and
you
want
to
expose
safe
to
use
functions
to
the
outside
world.
B
Something
like
this
call
me
function,
which
of
course,
is
completely
silly
to
use
unsafe
for
that.
This
is
just
for
purpose
of
demonstration.
So
what
does
this
function?
Do?
It
takes
a
shared
reference
to
a
Boolean.
It
does
some
pointer
casting
to
turn
this
into
a
raw
pointer
to
type
u8,
so
we
can
kind
of
look
at
the
underlying
bits
and
bytes
of
the
Boolean.
B
We
do
a
load,
we
check
if
it's
two,
but
it
shouldn't
never
shouldn't
ever
be
because
it's
a
Boolean
and
if
it
is
2,
we
call
this
hint
unreachable,
unchecked,
which
is
kind
of
the
ultimate
form
of
undefined
Behavior.
If
that
code
ever
executes,
we
have
immediate
ambient
behavior,
and
so
this
reaching
this
line
is
an
immediate
violation
of
your
obligation
as
part
of
this
compiler
programmer
contract,
and
this
function
is
sound
because,
no
matter
which
kind
of
save
code
you
will
write,
a
shared
reference
to
a
bullet
will
always
be
true
or
false.
B
It
will
always
be
one
or
zero.
It
will
never
be
two.
So,
even
though
there
is
unsafe
here,
this
unsafe
is
kind
of
safely
hidden
behind
a
typed
API
that
uses
the
rest
types
to
express
the
constraints
needed
to
make
this
thing
safer.
But
if
we
replace
the
bull
by
u8,
this
function
would
no
longer
be
sound.
B
B
B
Like
one
of
the
ways
we
could
break
it
is
by
creating
a
reference
to
two
and
turning
that
reference
into
a
raw
point
and
passing
it
to
core
me
all
of
those
things
creating
a
reference
and
then
trying
to
get
into
a
raw
pointer
are
possible
from
safe
code.
So
this
is
sufficient
to
demonstrate
that
this
library
is
answered
because
we've
demonstrated
a
safe
client
where
the
bad
line
has
been
reached.
B
B
So
the
to
summarize
the
keto
analogy
here,
undefined
behavior
is
a
property
of
an
entire
program,
a
thing
with
the
main
function,
something
you
can
run
and
the
property
is
well
undefined.
Behavior
means
it
violates
the
rules
where
soundness
is
a
property
of
a
library.
So
those
properties
talk
about
different
they're
kind
of
talk
about
objects
of
different
type.
A
library
is
sound
in
approximation.
There's
an
asterisk
here.
B
If
you
cannot
use
it
to
cause
undefined
behavior
from
safe
code,
I
will
not
go
into
the
asterisk.
Now.
If
we
have
a
bit
of
time
left
at
the
end,
I'm
happy
to
talk
about
that,
but
this
distinction
is
crucial.
It
doesn't
make
sense
to
to
ask
if
a
function
like
call
me
here
has
UB
or
not,
because
this
is
not
code,
you
can
run
it
takes
inputs.
You
need
to
First
Supply
some
inputs,
so
this
is.
This
is
important.
B
Now
I
want
to
go
over
briefly
a
list
of
kind
of
common
things.
People
get
wrong
about
undefined
behavior,
and
this
is
by
far
the
most
common
one.
People
test
their
code.
They
run
their
test,
Suite
I
know
they
write
their
whole
program,
they
put
it
on
the
Internet
or
something,
and
they
say
my
code
is
fine.
I
tested
this,
so
there
can't
be
any
undefined
behavior
and
we've
already
seen
the
example
earlier
right.
We
have
changed
the
comparison
a
bit
so
that
always
return
true
still
return.
B
True,
it
was
still
that
program
still
was
wrong.
It
was
just
now.
It
happened
to
be
the
case
that
the
arbitrary
thing
the
compiler
did
and
is
allowed
to
do
when
you
violate
your
contract,
was
actually
the
thing
you're
meanted
to
do.
That
can
happen.
That's
almost
the
worst
thing
that
can
happen
because
then
you
think
you
are
safe,
but
you're,
not
anytime.
You
upgrade
your
compiler.
You
change
your
flags,
you
change
anything
about
the
dependencies.
This
can
be
arbitrarily
unstable
and
behavior
might
change
again.
B
Another
common
thing
you
hear
in
these
discussions
is
people
starting
to
talk
about
what
the
hardware
does.
What
the
hardware
does
is
utterly
irrelevant.
When
we
talk
about
undefined
Behavior
the
the
kind
of
the
rules
for
what
you
can
and
cannot
do
in
raster
stated
on
the
level
of
the
rust
language,
they
don't
care
about.
Hardware
Concepts
and
the
link
between
what
the
final
program
produced
by
the
compiler
does
and
what
your
Source
Pro
does.
While
it
might
look,
direct
is
actually
a
very,
very
fragile.
B
The
compiler
is
doing
tons
of
amazing
things
to
make
your
code
go
fast,
and
you
probably
want
that.
Otherwise,
you
would
write
assembly
and
you
would
have
to
do
register
allocation
by
hand
and
all
sorts
of
other
fun
things,
but
because
that
link
is
so
fragile.
The
the
very
concept
of
looking
what
your
program
does
on
the
hardware
only
makes
sense
after
we
have
established
that
we
don't
have
undefined
Behavior.
B
You
can
never
argue
with
Hardware
things
before
we
first
made
sure
that
there
even
is
any
kind
of
connection
between
your
Source
program
and
the
output,
and
such
a
connection
only
exists.
If
you
satisfied
your
part
of
the
obligation
in
the
contract
with
the
compiler.
So
what
the
hardware
does
is
irrelevant.
B
Some
people
also
say
things
like
well,
you
know
I
upgraded
my
compiler,
my
code
broke
either.
Compiler
I
mean
we
try
to
avoid
this,
but
when
you
have
undefined
behavior
in
your
code,
it's
totally
possible
that
it
worked
with
one
compiler
and
then
stops
working
later.
That's
just
that's
just
the
nature
of
the
Beast.
B
Some
people
think
undefined
behavior
is
something
that
compilers
or
compiler
writers
spend
like
days
and
weeks
to
find
in
your
program
only
to
backstab
you
and
break
your
code.
That's
not
how
it
works.
Compiler
optimizations
are
just
written
under
the
assumption
that
there
is
no
Army
find
behavior
and
well
when
assumptions
get
evaluated.
Weird
nonsense
happens.
So
it's
not
like
compiler
authors
willingly
withhold
information
from
you.
Knowing
your
program
has
to
be
and
not
tell
you
that
the
opposite
of
what
happens?
They
don't
have
they
don't
know.
B
If
your
program
has
UB
or
not,
they
just
assume
it
doesn't,
and
then,
if
it
does
anyway,
weird
happens,
you
might
think
this
always
sounds
terrible.
Why?
Why
should
we
keep
up
with
this?
I
should
just
go
back
to
C.
C
is
all
the
same
guy
there's
no
difference
in
undefined
Behavior
between
C
and
rust.
It's
all
the
same
problems
and
if
you
use
inline
assembly
to
like,
maybe
maybe
you
think
you
can
do
out
of
one's
memory
access
in
an
assembly.
B
So
there
are
some
things
you
actually
can
do,
but
you
have
to
be
super
super
careful,
it's
not
a
free
pass.
There
are
all
sorts
of
assumptions
that
the
compiler,
see
and
rust
alike
makes
about
how
the
entire
program
works.
You
cannot
break
those
within
an
assembly
So
within
an
assembly.
You
are
almost
always
just
making
your
life
harder
and
finally,
I
disabled,
optimization.
B
So
UB
can't
be
a
thing
that
works
even
without
optimizations,
there's
a
whole
bunch
of
stuff
going
on
even
basic
things
like
register
allocation
can
kind
of
break
when
you
have
undefined
Behavior.
It's
true
that
without
optimizations
it's
much
less
likely
that
only
find
Behavior
affects
your
program
Behavior,
but
it's
by
far
not
guaranteed
that
it
doesn't
happen.
It's
still
very,
very
possible.
B
Oh
yeah
and
I
also
saw
that
I
think
at
some
point.
It's
fine.
If
I
put
unsafe
around
it.
That's
not
what
unsafe
is
for
unsafe
doesn't
mean
undefined
behavior
is
allowed.
Unsafe
means
it's
your
responsibility
to
not
have
undefined
Behavior
outside
of
unsafe.
It's
the
compiler's
responsibility
or
the
responsibility
of
whoever
wrote
the
libraries
as
you
are
using
inside
unsafe.
It's
your
responsibility,
and
if
my
behavior
is
never
okay,
just
not
a
thing.
C
B
Example,
yes,
yeah
right
UB
can
so
so
for
the
people
on
the
stream.
This
was
there
was
a
there
was
a
change
in
clang
to
kind
of
make
the
company
exploit
that
this
can
ever
be
now
turns
out.
Many
programs
have
this
penal,
including
V8,
which
is
kind
of
important,
and
so
they
wrote
that
back.
Yes,
that's
one
of
the
problems
with
widespread
misunderstandings,
about
misunderstandings,
about
what
is
and
isn't
UB
so
I
said
it's
all
the
same
mess
in
C
I
would
argue.
B
The
message
is
a
lot
worse
and
see
because
in
Rust
we
are,
or
at
least
strive
to
be
and
I'm
kind
of
there's
people
working
on
that
very
strict
and
precise
about
what
is
and
isn't
undefined
behavior
and
also
most
people
don't
have
to
think
about
it
because
most
people
write
safe
rest,
whereas
in
C
it's
a
lot
less
clear,
like
undefined
behaviors.
Everything
not
mentioned
in
the
standard,
which
is
already
kind
of
a
weird
way
to
go
about
this.
B
A
lot
of
undefined
Behavior
also
is
mentioned.
The
standard
also
nobody
reads
the
standard
and
the
people
that
do
don't
understand
it,
including
myself,
so
I
think
we
are
in
a
better
situation
in
Rust,
because
we
are
closer
to
having
a
very
precise
understanding
to
what
is
and
isn't
UB.
The
nature
of
the
problem,
though,
is
the
same,
so
I
hope
it's
clear
now
that
knowing
these
rules
about
what
is
an
isn't,
UB
is
absolutely
crucial.
B
When
writing
unsafecode,
you
shouldn't
be
writing
unsafe
code
without
understanding
the
part
of
the
rules
that
applies
to
the
kind
of
unsafe
code.
You're
right,
you
don't
always
have
to
know
all
the
unsafe
rules.
When
you
write
unsafe
code,
if
you're
just
calling
get
unchecked,
which
says
that
you
have
to
like,
have
your
index
inbounds?
That's
all
you
need
to
know.
B
Thankfully,
there
is
a
tool
that
can
help
you.
These
two
can't
replace
knowing
the
rules,
but
it
can
help
you
like
learn
the
rules
and
it
can
help
you
gain
confidence
that
you
followed
the
rules,
and
this
is
a
tool
called
Mary
that
I've
been
I
didn't
start
it.
The
originally
was
started
by
a
couple.
Other
people
I've
been
working
on
it
for
quite
a
few
years.
Now
it's
called
Miri
and
it's
basically
a
way
to
run
your
code
and
test
it
for
undefined
Behavior.
B
So
it
does
the
thing
which
earlier
I
said,
doesn't
work
like
if
you
just
build
your
comp,
you
code
with
a
regular
compiler
and
run
it,
and
then
it
works
that
doesn't
tell
you
anything
about
an
event
Behavior.
If
you
run
it
with
Miri.
That
does
tell
you
something
so
specifically
Miri
can
tell
if
a
given
program
or
a
test
Suite,
which
is
just
a
program
kind
of
shows
undefined
behavior
during
this
execution.
B
Mary
cannot-
and
this
is
important
to
remember-
Mary-
cannot
tell
you
whether
a
library
is
summed
because
to
test
the
library
is
sound.
The
least
you
have
to
test
is
that
it
doesn't
cause
you
B
for
every
possible
input
and
that's
a
few
too
many
inputs
for
Mary
to
try.
Maybe
it's
also
very
slow.
So,
even
even
if
it's
technically
finite,
it
doesn't
work
very
well.
B
So
you
still
have
to
have
a
good
test
Suite
to
increase
confidence
in
the
memory
results,
and
even
then
you
can
still
be
surprised,
but
it
helps
a
lot
so
to
ensure
soundness.
We
need
a
CR
improver.
This
is
something
which
is
not
decidable,
it's
not
something
you
can
just
have
a
button
and
it
will
guarantee
to
tell
you.
There
are
of
course,
tools
that
can
help
you
approximate
and
things
like
that.
I
mean
okay.
So
far,
there
aren't
such
dudes,
but
people
are
working
on
them
and
they
find
behavior.
B
On
the
other
hand,
on
a
concrete
program
execution
with
a
concrete
set
of
inputs
and
concrete
choices
for
all
the
non-determinism
is
a
decidable
question
which
we
can
answer.
But,
of
course,
if
tomorrow
the
threat
scheduler
starts
to
work
a
bit
differently,
then
maybe
you
undefined
behavior
is
like
showing
up
where
it
was
hidden
before
or
something
like
that.
So
there's
no
there's
no
guarantee
that
all
the
possibilities
was
found
in
alternative
execution,
branches
or
other
inputs
of
your
program,
but
it
helps
a
lot.
B
B
Mary
knows
a
few
well-known
functions
if
you're
accessing
an
environment
variable
or
opening
a
file,
maybe
you
can
deal
with
that,
but
that
list
is
not
very
long.
If
you
try
to
talk
to
the
network,
it's
already
done,
but
if
you're
writing
pure
rust
data
structures
or
things
like
that,
you
can
get
very
far
in
testing
with
Mary
Mary
is
also
as
I
mentioned,
very
slow.
B
So
if
you
have
tests
which
try
like
tens
of
thousands
of
inputs,
you
might
want
to
reduce
the
number
of
inputs
for
Miri,
but
Mary
has
found
tons
of
blocks
in
real
world
called
the
understand
library
and
in
crates
out
there.
We
test
the
stand.
Library
test
Suite
in
Miri
every
day,
a
whole
bunch
of
crates
have
memory
on
the
sci
is
really
a
thing
you
can
use
it's
very
easy
to
install
because
it
comes
with
rust
up
only
on
the
Knight
D2
train.
B
So,
to
emphasize
one
important
point
is
Mary
cannot
ensure
that
library
is
sound,
so
it's
still
worth
knowing
the
rules.
So
the
the
remaining
time
that
I
have
I
would
like
to
use
to
go
over.
Some
of
these
rules
show
a
few
example
programs
and
then
run
them
in
Miri
and
show
how
Mary
catches
the
problem
and
hopefully
answer
any
questions
that
come
up
about
the
undefined
behavior
in
this
program,
but
before
we
get
there,
does
anyone
want
to
like
anyone,
have
any
questions
about
the
general
framework
or
things
like
that.
B
B
Well,
for
these
unsafe
functions,
that's
a
conclusive
list,
it's
written
in
English,
so
it's
not
always
completely
clear
what
it
means
when
the
requirements
are
a
bit
less
local
I
mean
it's
very
easy
for
things
like
get
unchecked,
where
just
this
has
to
be
inbounds
and
then
done,
but
some
of
these
requirements
are
a
bit
less
local
than
that.
We
will
see
examples
and
also
there's
a
big
warning
here
at
the
top
of
the
list
which
which
basically
is
US
hedging,
that
we
are
not
done
yet
writing
the
spec.
B
B
B
So
what
the
compiler
doesn't
have
the
optimization
isn't
really
relevant
but
relevant
is
that
you
broke
the
rules
and
which
other
rules
that
you
broke.
So
the
the
and
the
rules
in
this
case
is
that
there's
some
uninitely
as
memory
here.
If
you
run
this
in
Miri,
we
can
say
that
already
on
this
line
before
you
even
start
doing
anything
with
the
analicious
memory,
maybe
it
tells
you
no,
no!
No!
No!
This
is
not
okay,
you're
returning
unjust
memory.
Here,
it's
between
that
type,
u8
u8s
have
to
be
initialized
period.
B
What
happens
internally
is
that
unjust
memory
is
represented
as
a
kind
of
unstable
value
which
every
time
you
look
at
it
can
look
different
a
bit
like
a
weird
Quantum
kind
of
value.
I
mean
if
physicist
system's
room,
don't
listen,
it's
not
actually
anything
but
Quantum.
I
know
that
so
it's
the
this
is
a
thing
that
exists
in
llvm
and
conceptually
in
many
of
these
low-level
IRS
we
use
inside
compilers.
B
They
have
values
which
are
different
from
every
possible
bit
pattern
that
they
would
actually
see
in
a
real
machine
and
every
time
you
look
at
them,
they
might
look
different,
which
represents
the
fact
that
lvm,
if
it
sees
an
initialized
value,
doesn't
want
to
waste
an
entire
register
on
that,
so
it
might
actually
use
different
registers
each
like
each
time
you
look
at
it.
I
might
use
a
different
register
just
picking
one
at
random.
B
That's
what
could
happen
that
what
actually
happens
here
is
then
elevmcs
we
are
asking
if
an
unstable
value
is
less
than
120
and
I
will
be
like
man,
I
guess,
that's
false,
and
then
we
are
asking
it
if
it's
equal
and
it
goes
like
yeah
false
and
for
great
it
also
gets
false,
but
for
greater
equal,
it
says
true,
but
that's
arbitrary
choices.
They
could
have
done
either
way
they're.
Just
yes,.
B
B
E
B
Know
unknown
I
mean
basically,
everybody
in
memory
is
an
option
you
ate
is
a
way
to
think
about
it.
It's
actually
bytes
are
actually
a
bit
more
complicated
for
pointer
reasons,
I
won't
get
into,
but
you
can
think
of
it
as
as
everybody
memory
is
an
option
you
ate.
If
that
was
the
question
yeah
something.
B
H
B
Very
unclear
it's
so
in
C,
plus
plus
they
have
a
list
of
things
you
can
do
with
indeterminate
values,
which
is
their
name
for
this,
and,
for
example,
passing
them
to
a
function
is
not
allowed,
so
the
UB
would
happen.
Certainly
the
latest
the
moment
we're
passing
X
to
always
return
true
in
C
is
not
entirely
clear
enough.
This
will
also
depend
on
the
type
you
are
using
like
if
you're
using
an
INT,
then
there's
more
positions
a
lot
on
internet
than
on
car,
so
maybe
with
car,
it's
okay,
but
within
it
isn't.
B
E
I
I
B
B
I
B
I
I
I
B
I
I
B
B
No,
but
first
really
I
mean
I,
don't
like
the
term
money
from
Behavior,
but
we
took
it
from
C
because
it's
what
people
know
and
if
you
write
against
and
if
you're
writing
as
an
arbitrary
unknown
C
compiler,
like
the
only
thing
you
know
about
your
compiler,
is
that
it
conforms
to
the
spec.
Then
all
the
same
rules
apply.
B
Okay,
let's
look
at
some
kind
of
undefined
behavior
and
how
they
look
like
in
Mary,
so
I
mean
okay,
I
already
briefly
showed
the
underneath
thing.
The
other
bonds
axis.
That's
the
that's
the
very
first
program
I
had
in
the
beginning
of
the
talk
and
I
mean
okay.
This
is
hopefully
not
too
surprising
and
not
too
hard.
When
you
do
the
read
Miri
will
tell
you
well,
there's
some
allocation,
it's
size.
Four!
B
You
had
F
UI
at
offset
four
and
reading
four
more
bytes
that
just
doesn't
work
use
after
free
is
also
easy.
I,
don't
think
I
have
to
show
the
code
for
that
out
of
bounds.
Point
arithmic
might
be
a
bit
more
surprising.
So
if
you
read
the
documentation
of
functions
like
add,
offset
or
sub
on
pointers,
then
the
documentation
says
that
even
just
doing
the
arithmetic,
if
it
goes
out
of
bounds,
is
undefined
Behavior.
B
This
is
just
like
pointer,
arithmetic
Works
in
C,
and
Mary
will
tell
you
that
if
you,
if
you're
using,
add
the
wrong
way,
then
you're
doing
out
of
Bounce
pointer
arithmetic,
there
is
another
function
you
can
use,
which
is
called
wrapping.
Add
which
doesn't
have
this
Clause
so
with
wrapping
at
this
program
is
now
fine.
However,
just
because
you
can
do
the
arithmetic
to
go
out
of
bonds
doesn't
mean
you
are
actually
allowed
to
use
that
pointer
to
access
memory,
but
now
it
even
tells
me
the
unsafe
block
is
unnecessary.
B
E
B
Allowed
so
this
is
not
going
to
complain
about
that.
Okay
thanks
I
mean
there
might
be
other
rules,
you're
breaking
inadvertently,
because
data
might
look
the
wrong
way
or
something.
But
in
principle
the
in
C,
Point
arithmetic
is
limited
to
array
things
and
rust
within
an
object.
You
can
do
a
pointer
arithmetic.
Any
way
you
want.
You
just
have
to
make
sure
once
you
actually
do
a
load
that
you
are
in
bounds
and
that
the
type
that
you're
using
for
that
load
is
the
right
one.
That
I
will
have
examples
for
that
later.
B
Insufficient
alignment
is
one
that
people
often
get
wrong.
So
here's
an
example:
we
are
creating
an
array
of
four
u8s
and
we
are
casting
the
pointer
into
a
u32
pointer
and
using
a
bunch
of
methods
instead
of
the
usual
casts
and
rust,
because
I
think
the
as
cast
keyword
and
rust
is
one
of
the
worst
things
to
use
when
using
raw
pointers.
It
would
way
too
many
things
and
accidentally
break
your
code.
This
way,
you
have
a
bit
more
type
safety.
B
B
The
alignment
requirement
of
such
an
array
is
one,
so
the
address
has
to
be
divisible
by
one,
which
is
rather
trivial,
whereas
integers
have
an
element
requirement
of
four
on
most
platforms,
so
the
address
of
every
integer
that
you
load
or
store
or
create
a
reference
to
has
to
be
divisible
by
four
and
we
are
violating
the
C
and
that's
undefined.
Behavior
again,
the
same
rule
exist
in
C.
It's
just
not
that
widely
known.
B
C
B
Good
question
Mary
is
not
guaranteed
to
find
this
error,
because
the
actual
address
of
this
thing
is
random.
It
in
this
case
it
happens
to
be
divisible
by
two,
but
not
four.
That's
why
this
was
the
error
in
general.
It
could
only
have
been
divisible
by
one,
so
this
is
one
of
the
case
where
the
non-determinism
that
occurs
when
creating
a
new
object,
creating
at
a
random
address
means
errors
might
sometimes
be
found
and
sometimes
not
found.
B
So
one
of
the
things
that
you
can
do
is
run
memory
many
times
it
has
a
flag
to
change
the
random
seat.
That's
used
for
all
the
non-determinism,
so
you
run
it
with
a
bunch
of
different
flags.
You
get
higher
chances
of
finding
bugs
like
this.
Maybe
also
has
a
special
mode
where
it
will
treat
alignment
in
a
more
symbolic
way
and
is
guaranteed
to
find
bugs
like
this.
Unfortunately,
it
might
then
also
flag
arrows
in
code
that
is
actually
completely
correct.
B
But
if
you
use
read
or
the
normal
star,
the
laminate
requirement
always
applies
on
our
platforms
and
it
doesn't
just
apply
when
you
do
a
read.
Even
just
creating
a
reference
already
incurs
a
requirement,
or
even
actually
just
writing
star
PTR,
no
matter
what
happens
afterwards,
increase
the
requirement.
B
B
B
E
E
B
Just
think
about
this
for
a
second
yeah,
okay
I'm,
going
to
do
a
quickly
over
some
of
those,
so
invalid
values
are
bad.
Rust
cares
a
lot
about
its
types
now
we're
getting
into
some
kind
of
things
which
are
UB
and
rust,
but
not
like
that
in
C,
I'm,
not
actually
sure
about
wool.
It's
a
bit
unclear,
I,
think
in
Buddha's
might
and
for
Buddhas
might
be
ubnc
as
well,
but
in
general,
see
less
strict
about
its
type.
So
turning
two
into
a
Boolean
is
undefined
Behavior.
B
Even
if
you
never
look
at
that,
Boolean
just
creating
the
Bool
is
undefined
Behavior.
This
is
important
because
there
are
optimizations
which
might
introduce
code
looking
at
the
Boolean.
Even
if
you
didn't
write
any
such
code,
so
we
want
to
have
that
requirement.
Always
such
optimizations
occur
very
naturally.
B
B
So
that's
that's
why
we
have
some
of
these
rules
where
just
creating
bad
data
is
UB,
even
if
you
never
look
at
it
so
that
we
can
do
things
like
move
loop
and
variant
code
out
of
a
loop
and
there
are
more
invalid
values.
What
we
have
here
characters
there's
a
requirement
that
car
is
a
valid
Unicode
code
point,
so
don't
violate
that
one
of
the
Lesser
known
ones
is
function.
B
B
Maybe
we
can
find
data
races,
that's
something
I'm
very
happy
about,
because
I
didn't
Implement.
Any
part
of
this
people
just
showed
up
open
source
is
amazing
and
started
implementing
more
and
more
ingredients
for
us
to
sub
for
Mary
to
suddenly
support
all
sorts
of
concurrency,
which
is
not
what
I
expected.
B
But
here
tells
me
that
between
lines,
11
and
8,
there
is
a
there's,
a
data
race
because
we're
doing
two
right
accesses
which
are
insufficiently
synchronized
and
last,
not
least,
I'm
not
even
going
to
show
the
example.
Here
There
are
rules
about
references,
shared
references
are
immutable
and
mutable
references
are
unique.
Those
rules
are
the
most
complicated
undefined
Behavior
rules
we
have.
They
are
also
very
important
and
very
like
unstable
in
the
sense
of
we
haven't.
B
K
B
Or
it
is
not
quite
as
much
as
you
might
think,
so.
The
detection
is
based
on
Vector
clocks,
which
means
we
don't
have
to
have
these
operations
actually
execute
adjacently.
It
works
pretty
much
exactly
like
what
is
the
well
grind
base
with
detector
called
again
helicron.
No,
there
are
two
data
rate
detectors
for
that
grind:
I
forgot
what
they're
called
they
use.
Basically
the
same
thing
where
you
detect
that
an
access
happened
and
then
let
another
access
happened
and
I
was
in
synchronization.
B
B
This
rarely
happens
on
real
Hunter,
but
it
does
happen
and
Mary
will
just
uniformly
at
random
pick
one
of
the
values
and
so
there
you
might
have
to
run
your
program
a
couple
times
to
make
sure
they
are
all
covered.
Mario,
also
emulates
the
weak,
compare
and
swap
in
The
Sound
Library,
which
is
a
companion
swap
that
might
fail
to
tell
you
when
it
did
successfully
a
thing.
That's
the
atomic
visibility
problem.
Yes,
yes,
exactly
so
I'm
I'm
out
of
time,
so
for
a
more
complete
list.
B
As
the
I
already
mentioned
earlier,
when
the
question
came
up,
you
can
check
the
reference.
Every
unsafe,
Library
function
must
document
their
requirements.
If
you
find
a
crate
with
an
unsafe
function
that
doesn't
document
it.
The
great
author
did
it
wrong,
and
so
with
that
remember,
when
writing
unsafe
rust,
always
follow
the
rules
and,
if
possible,
use
memory
to
help.
You
do
that.
Thank
God
thanks
a
lot.
L
Yeah,
so
you
mentioned
that
Miri
stops
when
it
encounters
C
code.
My
question
is
whether
it
stops
completely
or
just
for
the
C
part
and
continues
with
like
rust.
Only
so
I
could
imagine
that,
like
C
returns
to
some
pointers,
so
obviously
it
cannot
reason
about
this
pointer,
but
maybe
later
in
code,
there
are
like
pure
rust
pointers
that
it
can
know
something
about.
No.
B
B
Mary
will
warn
you,
because
once
you
start
doing
that,
it
won't
be
able
to
find
all
bugs
anymore.
The
spec
for
those
things
is
kind
of
not
quite
there.
Yet
at
the
spec
we
have
is
not
something
you
can
actually
run,
it's
only
something
you
can
prove,
and
so
maybe
we
warn
you
about
that
and
and
see
it
would
just
be
a
lot
more
of
that
kind
of
maybe
possibly
missing,
bugs
around
really
weird
pointer,
shenanigans.
B
M
B
Be
bad,
wouldn't
it
I
mean
so
first
of
all,
like
movie,
doesn't
work
in
that
case.
Obviously,
Mary
has
no
clue
that
you
have
an
MMA
where
to
start
address
42.
on
the
rust
side.
No,
this
is
not
undefined
Behavior.
The
the
full
way
of
making
this
formal
is
complicated,
but
basically
we
don't
assume
that
Russ
knows
all
the
memory
that
exists.
Rust
controls
some
amount
of
memory.
B
You
have
to
still
follow
the
rust
rules
as
in,
if
you
create
a
reference
to
that
memory,
all
the
aliasing
things
still
apply
and
stuff.
Like
that,
but
it
is
okay
to
access
memory
like
that,
so
in
that
case,
yeah
there's
a
big
Asset
Risk.
According
to
what
the
hardware
does
this.
This
refers
to
arguments
of
the
form
of
x86
doesn't
have
alignment
requirements.
Therefore,
it's
okay
to
de-ref,
unaligned
pointers
and
see
when
you
compile
only
to
x86.
B
No,
they
were
like
I
think
it
was
Rand
like
some
really
really
big
rust
crates,
which
had
a
CF
like
if
CFG
Bank
to
be
like.
Oh
on
on
x86.
We
just
do
the
online
accesses
everywhere
else.
We
are
careful.
This
is
just
not
okay,
it's
always
will
be
on
all
platforms,
but
if
you
have
very
specific
environment
kind
of
things,
that's
less
about
my
assembly,
my
CPU
doesn't
have
databases
or
something
that's
more
about
there's
extra
things
in
my
environment
that
are
outside
of
the
control
of
rust.
B
F
You
said
that
Mary
doesn't
have
any
support
for
sort
of
symbolic
calculations.
I
was
running
coming
back
to
this
ffi
if
there,
if
it
would
be
possible
to
sort
of
specify
the
behavior
of
a
foreign
function
and
then
have
Meri
like
sort
of
bypass
the
foreign
function
based
on
those
assumptions,
even
though
it's
not
possible
now
like
is
there
anything
in
Miriam.
B
B
The
thing
we
do
is
that
for
when
on
functions
like
I,
don't
know
when
you
want
to
access
the
environment
variable
or
print
the
standard
out,
Miri
is
like
oh
I
know
this
C
function,
it's
called
like
get
anth
I
will
actually
Implement
that
so
we
have
in
in,
we
call
them
shims.
You
have
a
whole
lot
of
these
shims
inside
memory,
which
will
then
behave
as
if
you
did
get
NF,
so
you
do
set
Anthony
to
get.
If
you
actually
see
the
value
change.
B
This
is
completely
separate
from
the
actual
process
environment,
though
we
also
have
a
flag
which
allows
them
to
to
be
sucked
so
like
for
specific
functions.
We
can
add
support
that
way.
Obviously,
we
can
only
do
this
for
like
big
popular
functions
that
have
reasonable
small
functionality.
If
you
link
your
C
code
with
the
python
interpreter
and
call
that
we
will
not
embed
a
python
interpreter
in
Mary
just
to
implement
that.
B
Yes,
it's
it's
a
mirror
e
the
mirror
interpreter,
though
we
don't
spell
it
like
that
it
works
on
this
IR
level
called
mirror
in
the
compiler.
It's
really
basically
just
another
front
end
for
the
compiler
like
it's
it.
It
actually
well,
backend
I,
don't
know
it
reuses
all
of
the
compiler
infrastructure,
but
then,
instead
of
generating
code
it
it
just
interprets
it
line
by
line.
B
I
B
I
think
there
is
currently
someone
working,
so
they
existing
interpreter
for
lvmir.
It
doesn't
actually
describe
all
lvmir
UB
the
way
Mary
does.
But
there
is
someone
currently
trying
to
wire
that
up
with
Mary
as
I
found
out
when
they
reported
that
they
get
weird
linking
errors
when
they
try
doing
that.
B
E
B
G
I
guess
a
bit
open
question,
but
let
me
give
it
a
try.
So
there
is
a
bunch
of
code
that
it's
aimed
to
be
compiled
and
to
run
as,
for
example,
web
assembly,
but
the
way
people
test
this
code
is
they
just
write
unit
tests
to,
like
you,
know,
cargo
test
and
then
it's
compiled
on
their
actual
architecture.
They
work
on
like
x86
or
arm
or
whatever,
and
then
it
keeps
me
in
this
place
of
discomfort.
The
developers
test
the
code
all
the
time
on
different
architecture.
G
B
I
mean
rust
is
in
general,
fairly
portable,
so
like,
if
you
don't
have
UB,
and
if
you
don't
have
CFG
Target
art
or
Target
whatever
in
your
code,
then
it
should
behave.
The
same
on
x86
and
and
webassembly.
Some
of
the
non-determinism
might
be
different
like
if
you
look
at
the
addresses
of
the
stack
or
interleavings
of
threads
or
something
those
are
different,
but
that's
a
problem
even
like
between
an
x86,
Linux
and
windows,
or
even
two
linuxes
or
whatever
so
but
like
most
of
rust,
is
actually
very
portable.
B
But
it
depends
a
lot
on
the
details.
I
should
also
mention
one
other
thing:
Mary
is
quite
useful
for,
if
you're
doing
low
level
coding,
one
of
the
things
that
you
might
run
into
at
some
point
is
this
funny
thing
called
indianness,
where
some
targets
represent
integers
different
from
different
from
other
targets,
because
Mary
is
an
interpreter
it
can
cross
interpret.
B
So
you
can
be
on
your
Linux
64-bit
little
Indian
system
and
you
just
said
dash
dash
Target
mips,
something
something
like
the
correct,
Target
triple,
which
might
be
a
32-bit
big
engine
system,
and
maybe
we'll
run
your
code
as
if
it
were
on
that
Target.
You
can
be
on
a
Windows
host
and
run
it
as
if
it
were
Linux.
All
these,
like
in
principle,
any
possible
combination.
There
is
possible
there
in
terms
of
maybe
just
testing
your
code
and
making
sure
like
so
so,
like
the
bytescribe
I.