►
Description
RustConf 2018 - C2Rust: Migrating Legacy Code to Rust by Per Larsen
Although Rust is safer and more modern than C/C++, it is still difficult to justify the cost of migrating existing, mature systems code.
This talk will present a trifecta of tools to address the costs and risks of such migration efforts. The first tool is a transpiler which generates structurally equivalent-yet-unsafe Rust code from the input C code. The second is a dynamic analysis tool which runs the original C code alongside the new Rust code to check whether they are performing the same computations. The third is a refactoring tool which helps programmers idiomize the output of our transpiler.
Our aim is to automate many of the steps that are entirely manual when migrating from C to Rust today. However, we do not expect that the migration process will be fully automatic. Therefore, we focus on detecting unexpected discrepancies as the programmer gradually rewrites the transpiled code to make better use of Rust idioms. Our tools are open source and available to anyone.
Additional resources:
Code: https://www.github.com/immunant/c2rust
Demo: https://www.c2rust.com
Slides: https://www.ics.uci.edu/~perl/rustconf18_c2rust.pdf
Writeup: https://galois.com/blog/2018/08/c2rust/
A
A
Okay,
just
in
case
you
thought
this
was
going
to
be
a
talk
with
cute
cat
pictures
and
gifts
and
jokes.
It's
not
what
we
we
do
is
has
been
funded
in
part
by
DARPA
and
and
they
require
us
to
start
with
this
legal
disclaimer.
So
I'm,
sorry,
but
this
is
what
I
have
to
show
you
that
we
asked.
If
we
could
please
talk
to
people
about
this
at
Ross,
conf
and
and
DARPA
said
yes,
so
that's
all
the
legalese
I
have
to
bore
you
guys
with
so
just
really
quickly.
A
My
background
is
mainly
in
c
and
c++,
exploit
mitigation
and
I'll
talk
about
how
that
led
us
to
the
C
to
rust
work,
but
first
I
just
want
to
acknowledge
that
I'm
part
of
a
much
larger
team.
There's
three
gentlemen
from
Galois
shown
here
and
three
of
my
colleagues
at
immune
end
that
are
all
crack
coders
and,
and
they
do
much
of
the
heavy
lifting
and
if
you
have
any,
really
hard
questions
I'm
going
to
defer
to
Andre
who's
in
the
audience
today.
A
A
This
it's
I,
think
that's
a
fair
question
to
ask
so
I've,
showing
a
graph
here
from
the
National
Institute
of
Technology's
national
boner
ability
database
and
it
essentially
tracks
20
years
worth
of
stats
on
buffer
errors,
which
is
not
the
only
security
issue
you
can
have
in
C
and
C++
code.
But
it's
it's
among
one
of
the
most
common.
So
that's
this
kind
of
stuff
where
you
under
overflow
and
array
index
and
you
access
memory
that
you're
not
supposed
to
and
in
many
cases
that's
exploitable
and
all
hell
could
break
loose.
A
So,
as
I
said,
I
have
a
background
in
working
on
C
and
C++
exploit
mitigations,
where
we
try
to
change
the
way
we
compile
C
and
C++
code
and-
and
you
can
do
something-
to
sort
of
take
the
lowest
hanging
fruit
off
the
table
to
adversaries.
But
in
the
end
the
pattern
is
that
you
come
up
with
a
new
exploit
mitigation
and
then
the
adversaries
find
another
way
to
work
around
that
and
still
exploit
the
C
and
C++
code.
So
it's
it's!
It's
an
arms
race
really
in
in
in
rust,
is
an
attractive
migration
target.
A
I'm
sure
I
won't
have
to
sell
you
guys
on
rust,
but
it
does
have
this
interesting
property
of
providing
not
just
type
and
memory
safety,
but
also
freedom
from
data
data
races.
So
that's
that's
like
catnip
to
people
that
have
written
a
lot
of
C
in
C++,
so
we
thought
well.
Okay,
rust
is
great,
but
it's
obviously
not
easy
to
get
into
rust.
Is
there
anything
we
can
do
to
lower
the
barrier
to
entry
there?
A
Syntax
I'm
gonna
show
you
some
really
disturbing
and
ugly
rust
code
later
and
that's
something
you
you're
gonna
want
to
refactor
into
pretty
and
idiomatic
rusted
that
doesn't
make
your
eyes
bleed
and
as
you're
doing
that
that's
gonna
be
a
mostly
manual
process,
so
we're
also
gonna
do
something
to
try
and
help
you
catch
errors
during
transfer
factoring
into
a
more
idiomatic
rust.
So
this
is.
This
is
the
grand
idea.
This
is
what
we
pitched
initially
and
and
what
I
hope
we
can
get
to
one
day
in
the
far
future.
A
So
the
main
points
of
this
year
is
to
notice
is
the
flow
on
the
top,
where
we're
taking
untrusted
unsafe
C
code,
and
we
run
it
through
a
transpiler
and
outcomes
unsafe,
rust.
It's
a
syntax,
driven
translation
into
rust
that
basically
projects
the
structure
of
the
C
code
into
rust
and
uses
C
types,
and
it
doesn't
buy
much
in
terms
of
security,
but
at
least
it
compiles
to
rust,
C
and
that's
something.
A
So
that's
the
initial
stage
from
0
to
1
and
then
the
latter
stages
is
sort
of
iterative
from
n
to
n
plus
1,
where
you
have
some
Russ
code
that
you're
not
entirely
happy
with
yet,
and
you
want
to
make
it
more
dramatic
and
you
basically
have
two
options.
You
can
either
manually
rewrite
it
or
you
can
hope
that
we
provide
some
sort
of
refactoring
that
can
either
suggest
or
do
a
rewrite
for
you
that
improves
the
the
quality
of
the
rust.
In
some
way,
and
in
case
you
are
forced
to
do
a
manual
rewriting.
A
We
know
that
humans
are
tend
to
make
errors,
we're
not
perfect.
So
what
we
do
to
catch.
Those
errors
are,
is
that
we
cross-check
the
Russ
code.
You
have
against
the
original
C
program
so
we're
we
have
a
tacit
assumption
here
that
you
wanna
at
some
level
preserve
the
functionality
of
what
your
C
programming
is
doing.
So,
let's
say:
you're
trans
you're
migrating
decoder.
You
still
want
to
decode
an
output
from
your
s
code
to
be
the
same
as
your
C
code.
A
So
there's
lots
of
opportunities
in
there
to
to
check
the
two
versions
or
sanitize
them
against
each
other.
So
we'll
talk
about
that
later,
but
first
transpiling
the
things
we
wanted
to
accomplish
without
transpiler
I'm
going
to
talk
about
a
few
other
transpilers
in
a
second.
So
we
have
some
unique
goals
partially
informed
by
the
experiences
of
others.
That
fought
to
build
deterrents
pilot
before
us
and
inspired
us
in
that
way
is
that
we
wanted
to
do
robust,
C
and
C++
parsing.
A
We
basically
want
to
handle
more
than
hello
world.
We
want
to
be
able
to
take
huge
and
crusty
old,
C
code
bases
and
parse
them,
and
we
want
to
preserve
the
functionality
of
that
code
because
it's
most
likely
we'll
just
the
despair.
If
you
care
enough
about
it
to
move
it
into
rust,
so
we've
got
to
preserve
the
functionality
of
the
code
we
take
in
and
convert
to
rust.
A
A
Finally,
we're
also
excited
about
rust.
So
we
want
to
write
as
much
as
a
transpiler
in
rust
and
we
want
to
reuse
some
of
the
rust
compiler
internals
on
the
back
end.
So,
first,
a
hat
tip
to
other
efforts.
Co-Wrote
was
the
first
C
to
rust,
transpiler,
it's
written
in
Haskell
in
the
by
Jamie
sharp.
We
met
him
yesterday,
nice
gentleman,
it
uses
the
Haskell
C
parsing
library,
and
because
that
is
less
used
and
less
maintained
and
and
battle-tested
than
the
clang
c
compiler.
A
That
leads
to
certain
limitations,
but
it's
certainly
an
impressive
effort
for
one
guy
and
and
so
that's
good
work
and
there's
also
a
citrus
RS,
which
is
interesting
because
it's
it's
based
on
clang
like
we
do,
but
it's
not
making
any
effort
to
generate
C
code
that
were
a
sorry,
rust
code
that
would
actually
run
right
away.
It's
trying
to
generate
the
closest
approximation
of
what
what
you
would
want
to
write.
Ultimately,
so
it's
it's!
It's
merely
trying
to
help
you
with
the
syntactical
changes.
A
So
we
sort
of
slot
in
between
these
two
by
by
handling
all
C
input
and
also
generating
something
that
runs
and
that
you
can
work
further
on.
So
our
transpiler
is
kind
of
a
chimera.
It's
C++
on
the
front
end,
because
if
clang
and
then
it's
rust
in
the
back
end,
so
the
flow
is
that
we
take
in
a
bunch
of
C
sources
and
we
take
a
JSON
file.
That's
called
compile,
commands
n,
which
informs
us
of
how
the
compiler
was
invoked.
A
So
we
can
have
playing
pre-process
the
the
C
code
and
then
we
translate
it
and
that
that
has
some
interesting
consequences
that
I'll
mention
briefly
later.
So
all
of
this
is
driven
by
a
blue
Python
script
and
underneath
the
hood
we
have
two
one
is
a
C++
binary
called
the
ASC
exporter.
It's
very
boring
it.
It
merely
serializes
the
clang
ast
into
a
c4
file,
it's
a
completely
arbitrary
choice
of
format
and
that
seaboard
file
isn't
consumed
by
our
ast
importer.
A
So
the
a
ste
importers
that
is
the
most
interesting
part
of
the
transpiler.
It
DC
realizes
the
Seaboard
file,
and
then
that
gives
you
a
claim
AST
which
we
represent
in
in
in
in
rust,
and
I
think
we
use
pungent
too
to
make
sure
that
we
synchronize
some
of
the
data
structures
there.
We
transform
that
clang
ast
into
our
own
internal
importer
ASC
and
then,
as
a
second
step,
we
do
a
similar
transformation.
A
For
now
in
in
the
in
the
process
of
this
second
stage
conversion,
we
prune
a
seed
declaration
that
we
don't
see
being
used
in
the
current
translation
unit,
because
you
have,
even
in
your
hello
world,
you'll
you'll,
probably
have
to
include
a
header
file
for
printf
and
that
that
pulls
in
a
lot
of
other
gunk
that
you
are.
You
don't
necessarily
use
so
we'd
prune
that
out,
and
we
also
look
at
loops
that
contain
unstructured
control
flow,
such
as
go
twos,
and
we
try
to
generate
a
valid
dress
code.
For
that.
A
So
I
have
a
few
details
on
that
later
too,
but
first
pre-processing
we
do
our
transpiling
after
pre-processing,
and
that
means
that
we
need
to
know
how
to
invoke
the
compiler
with
the
write
flags
for
a
given
platform.
So
this
is
a
problem
that
IDs
always
also
have
an
analysis
tools.
So
there's
an
existing
solution
where
clang
will
actually
read
this
JSON
file.
I
mentioned
earlier.
There's
an
example
on
on
the
right
showing
the
contents.
It's
very
simple.
A
It
just
gives
the
arguments
of
the
compiler
and
in
the
build
context,
and
you
can
get
this
file
automatically,
but
the
way
you
do
so
depends
a
little
bit
on
what
build
system
you
have
on
what
platform
you're
on.
So,
if
you're
using
C
make
great,
you
just
add
another
flag,
if
you're
not
using
see
make
claim
comes
with
a
script,
that's
called
intercept
built
that
you
can
use
for
make
file
projects
both
on
Linux
and
Mac
OS
or
you
can
use
pair
on
Linux.
A
So
let's
get
back
to
transpiling
loops
in
the
simple
case
where
the
C
code
doesn't
have
any
unstructured
control
file,
we
simply
generate
rust
while
loops,
so
that's
fairly,
simple
and
straightforward.
We
generated
while
loop,
no
matter
whether
you
put
in
a
for
loop
or
Y
loop
on
the
see
sign
in
case
you
have
go-to
things,
get
a
lot
more
interesting.
A
So
this
this
code
example,
we
have
a
demo
I,
don't
know
if
you've
seen
it
out
front,
but
the
conveniens
from
gondwana
they've
they've
been
running
the
demo
website
and
somebody
actually
submitted
this
code
example
to
the
demo
website
and
and
and
we're
presenting
here
for
your
viewing
pleasure.
It
actually
reads
quite
nicely
too,
while
loop
in
rust,
so
I'm
calling
you
looping
because
we're
using
the
real
looper
algorithm
by
Alan
Sakai
of
the
inscription
project.
A
They
face
the
similar
project,
a
problem
in
so
far
that
they're
translating
LLVM
ir
into
javascript
code,
which
also
doesn't
allow
in
structured
control
flow.
So
we
we
reuse
the
Alan's
work,
but
we're
doing
a
little
bit
more
because
we
are
interested
in
human
consumption
of
our
output,
where
it's
Krypton
is
simply
feeding
the
JavaScript
to
a
JavaScript
compiler.
Hopefully,
nobody
touches
that
once
it's
been
transpired,
so
we
try
to
preserve
comments
while
real
ooping
and-
and
we
also
optimize
for
readability
and
in
this.
A
A
That's
a
Lib,
C
rusts,
create
issue,
but
macros
is
is
something
that
that
we're
not
showing
in
the
output,
because
we
do
the
translation
after
macro
expansion.
So
that
means
whatever
the
macros
expand
to
on
your
platform.
That's
what
the
Bross
code
is
going
to
reflect.
Now
it
would
be
much
nicer
if
you
could
preserve
the
portability
and
flexibility
of
your
C
code
by
at
least
handling
macro
cases
where
there
is
a
reasonable
translation
into
rust.
So
remember
that
C
macros
don't
operate
on
on
the
syntax
tree.
A
There
they're
purely
textual
replacements,
so
it's
possible
for
a
macro
to
expand
to
something
that
doesn't
generate
a
valid
syntax
tree,
and
sometimes
you
have
pair
of
Mac
pairs
of
macros
begin
and
end
that
have
to
be
used
together
to
get
valid
C
code
so
stuff
like.
That
is
something
we
don't
see
ourselves
ever
supporting
in
Reverse.
But
there's
there's
probably
a
good
deal
of
macros
that
we
can
support
with
reasonable
effort.
But
as
of
now
we
don't
so.
This
is
the
web
demo.
A
I
hope
everybody
has
seen
this
already
now
and
actually
talked
to
people
that
at
the
demo
slot
instead.
But
if
you
haven't
go
to
C
to
Roz
comm
and
you
can
see
that
you
can
either
type
in
your
own
C
code
or
you
can
choose
from
a
few
pre-baked
examples,
you
can
translate
it
download
the
output.
Hopefully
it
runs
and
there's
also
links
to
the
source
code
in
an
FAQ.
So
we
consider
this
our
our
our
business
card
and
the
way
to
get
ahold
of
us
if
you
want
to
complain.
A
So
if
you
want
to
do
more
than
just
translate
one
file
at
a
time,
you
got
a
clone
the
software
and
build
it
locally
and
it
the
way
you
do.
That
depends
a
little
bit
on
what
platform
you
are
on.
So
some
of
the
our
code
is
Linux
only
so
if
you're
on
another
platform,
I'd
encourage
you
to
either
take
a
look
at
docker
or
vagrant.
We
provide
scripts
for
both
it's
one.
A
It's
a
containerization
technology
and
another
one
is
a
virtualization
technology
and
we
provide
scripts
that
will
build
a
doctor
of
a
current
environment
and
provision.
It's
such
that
you
have
all
the
right
packages
in
the
right
places
for
the
seizure
or
s
build
systems
to
just
function
flawlessly
and
if
they
don't
I,
hope,
you'll
file,
an
issue
or
write
me
a
sternly,
a
worded
letter.
A
So
because
it's
kind
of
a
chimera
we
use
Python
to
glue
together
the
build
processes.
So
you
simply
run
the
build
translator,
script
with
claim,
and
that
gives
you
the
translator
and
you
can
similarly
build
all
the
projects
that
your
that
are
required
for
cross.
Checking
on
this
c
and
c,
plus
a
c
and
rust
side
and
the
refracting
tool
is
pure
rust.
That's
that's
built
with
cargo.
A
The
way
we
know
and
love,
so
here's
an
example
of
how
to
transpile
I've
have
a
little
buffer,
a
library
that
I
cloned
from
from
c
lips
and
I
removed
very
attic
functions.
So
I
won't
be
embarrassed
by
warning
messages
in
harris
and
you
simply
use
bear
to
make
it
such
that
you
get
a
compiled,
commands
a
json
file
as
you
build
it
and
it
automatically
runs
the
test
suite
and
prints
out.
Okay,
so
that's
just
the
c
code
and
then
you
can.
A
You
can
use
our
trans
pilot
that
py
script
to
point
it
to
the
compiled
commands
and
we'll
look
at
all.
The
C
files
and
it'll
run
the
transpiler
on
them
and
it
will
pick
up
the
main
method
from
the
test
translation
unit,
because
we
put
a
pass
in
the
m
argument
and
then
you
can
simply
go
into
the
C.
Trust,
builds
up
gear
and
run
cargo,
and
lo
and
behold
it
does
the
same
thing
great
success.
So
here's
here's
an
example:
input
function
from
that
buffer
library.
A
That
I
just
showed
you,
and
here
is
the
translated
rust
output.
So
you
can
see
it's
not
exactly
the
rust
that
a
human
would
write.
It's
it
uses
its
it's
all
unsafe.
It
uses
no
mangle.
It
basically
calls
malloc.
Just
like
the
C
code.
Did
it
has
the
same
kind
of
error,
handling
and
initializes
the
allocation
after
it's
returned,
you
can
see
pointer
accesses
are
not
pretty
ads.
We
use
wrapping,
add
to
preserve
C
semantics,
so
that's
also
not
pretty
and
and
there's
a
there's.
A
A
few
superfluous
casts
in
there
or
not
superfluous,
but
ideally
one
wouldn't
have
that
have
them
in
idiomatic
rust.
So
here's
here's
something
we
rewrote
by
hand
and
you
can
see
that
it
does
the
same
thing.
It's
much
cleaner
and
more
compact
there's
one
little
change,
which
is
that
when
we
allocate
on
the
heap
with
rust,
we
get
zero
allocated
memory.
So
this
is
actually
not
a
semantics,
preserving
transformation
and
that's
why
we
do
refactoring
separately.
So
we
can
have
a
program
approve
these
changes
rather
than
just
doing
them
silently.
A
So,
when
we're
doing
manual,
refactoring
I
mentioned
that
there's
there's
the
possibility
for
errors
creeping
in,
so
we
have
a
cross-checking
tool
to
verify
that
your
current
rust
version
does
something
similar
to
the
original
C
code.
To
the
extent
you
want
to
so
what
you
gotta
do
is
instrument
the
original
C
code
and
the
translated
rust
code.
A
We
provide
plugins
to
do
that,
I'll
get
to
those
in
a
second,
and
once
you
have
your
instrumented
C
in
rust
code,
you
run
both
of
their
programs
and
you
feed
them
identical
inputs
such
that
you'd
expect
them
to
carry
out
the
same
computations,
and
you
can
see
an
example
here
where
we
have
a
symbol:
ID
function.
What
we'll
do
is
we'll
cross
check
that
the
function
names
are
the
same
and
that
argument
values
coming
into
the
function
are
the
same
and
we'll
also
also
cross
check
that
they
return
the
same
value.
A
So
this
is
a
very
simple
example.
It
gets
a
little
bit
more
here
once
the
functions
are
non-trivial,
so
you
have
two
options
for
cross-checking.
One
is
to
do
the
cross-checking
online
using
something
that's
called
an
MBE
I'll,
explain
that
in
a
second,
but
for
now,
just
think
of
it
as
a
way
to
execute
two
processes
side
by
side
and
make
sure
that
they
get
the
same
input.
So
you
want
to
do
this
because
you
don't
have
to
do
any
logging
and
the
NVE
will
replicate
inputs
to
the
two
processes
for
you.
A
It
does
have
some
drawbacks
in
the
area
of
compatibility.
You
can
can't
take
something
as
complex
as
a
web
browser
and
run
two
copies
and
cross
checks
and
with
an
MBE
for
a
variety
of
reasons
that
I'm
not
going
to
bore
you
with
today.
So
if,
if
you
can't
use
an
MBE,
you
have
the
option
of
doing
cross
offline
checking
where
we
log
the
program
behavior
to
do
log
files,
and
if
you
program
small
enough,
that's
something
you
can
do
and
you'll
you
avoid
some
of
the
compatibility
issues
of
using
MBEs
so
really
quickly.
A
This
is
a
fairly
large
research
area,
but
the
idea
is,
you
have
two
variants
of
the
same
program.
So
in
our
case
it
would
be
a
C
program
on
one
side
and
the
translate
the
Ross
program
on
the
other
side
and
as
soon
as
they
make
a
system
call,
we
have
a
monitoring
component
that
intercept
system
calls
and
forwards
them
to
the
kernel.
So
you
can
see
first,
we
call
a
BRK
to
allocate
memory
and
in
that
case
we
want
to
allocate
memory
for
both
processes.
A
So
the
money's
were
forwards,
both
calls
and
then
later
we
make
a
right
to
system
call,
and
in
that
case
the
monitor
intercepts
both
calls,
but
it
only
forwards,
one
of
them
to
the
kernel
and
it
waits
for
the
results,
and
then
it
sends
the
results
back
to
both
of
the
processes.
So
essentially,
the
monitor
provides
the
surrounding
host
with
illusion
of
one
process
running
when
in
fact,
you
have
two
processes
running
and
doing
the
same
thing
receiving
the
same
input
and
the
monitor
will
also
cross
check
that
the
two
variants
produce
the
same
output.
A
So
that's
how
we
we
can
detect
differences
in
the
C
code
and
the
run
rust
code
online
without
logging.
So,
as
I
said,
we
have
plugins
to
instrument
the
code.
We
have
different
runtimes,
based
on
whether
you
use
MV,
based
or
cross
checking
or
log
based
cross-checking.
You
have
a
zeroing
matter
replacement,
so
in
case
we
end
up
cross-checking
data
that
that
would
be
uninitialized
than
the
seaside
that
that
does
not
create
any
problem
for
us.
A
I'm
gonna
skip
the
last
because
we're
running
a
little
behind
schedule,
so
here's
an
example
of
cross-checking,
a
very
simple
library
that
we
just
transpired.
We
make
it
again.
We
transpile
it
and
this
time
we
add
two
new
flags
to
transpile.
We
add
dash
X
to
enable
cross,
checking
and
you
to
select
the
log
based
cross
checking,
and
then
we
built
it
again,
and
we
point
I,
said
LD
library
path
to
point
to
our
log
based
cross,
checking,
runtime
and
then
I.
A
Simply,
cargo
run
and
output,
I
log
standard
error
to
a
file
and
then
I
I
run
the
C
program,
which
has
also
been
instrumented,
because
I
have
a
make
file
target
called
test,
underscore
X
check,
which
passes
the
write,
plug-in
parameters
to
claim
such
that
the
C
code
will
be
instrumented
for
cross-checking
and
again
when
it's
run,
I,
lock
the
standard
error,
output
to
two
buffered
CX
checks
and
then
I
simply
dip
it
to
and
and
that
returns
zero.
So
the
they
did
the
same
thing,
which
is
lucky
for
this
example.
A
So,
finally
briefly,
we
I
mentioned
that
we
also
want
to
do
refactoring.
This
is
the
this
is
the
least
mature
area
for
our
work
right
now
so
I'm
just
gonna
show
you
a
simple
example
where
you
have
some,
while
loops
that
step
from
0
to
9
and
it
with
a
stride
of
1
and
2,
and
and
we
have
simple
patterns
that
can
recognize
that
this
is
better
expressed
as
a
for
range
loop
in
interest.
A
This
is
obviously
fairly
simple
and
and
and
and
we
hope
that
that
will
get
to
substantially
more
advanced
refactoring
across
files
and
involving
a
substantial
amounts
of
program
analysis
to
do
much
more
useful
things.
So
if
we
have
a
few
minutes,
I'll
just
really
briefly
talk
about
pie
in
the
sky
stuff
that
we
hope
we'll
be
able
to
do
so.
The
main
main
feed
we've
gotten
so
far
in
our
project
is
that
it
would
be
really
nice
if
we
could
do
something
to
generate
safer,
rust,
right
away
or
automate.
A
Some
of
the
tasks
so
100%
automation
is,
is
really
really
difficult.
So
I
I
have
this
illustration
here.
That
shows
that
the
arrows
were
sort
of
we're
sort
of
moving
on
on
rings
in
and
without
any
kind
of
safety
transformation
we're
just
staying
on
the
outer
rings,
and
what
we
want
to
do
is
we
want
to
bend
those
rings,
so
we
go
into
a
provably,
safe,
subset
of
rust,
and
the
challenges
of
doing
so
is
that
we
have
no.
A
An
automated
analysis
has
no
domain
knowledge,
that's
really
hard
and
then
Russ
has
a
substantially
different
type
system,
so
things
like
ownership
gain
are
aware
of
simply
propagating
types
around.
So
a
really
quick
example
here
is
something
Istanbul
upon,
while
just
refactoring
a
very
simple
quicksort
example:
the
partition
method
function,
sorry
calls
swap-
and
this
is
all
done
with
raw
pointer.
A
So
that's
that
kind
of
a
bummer
for
us
so
like
any
sane
rust
program,
would
realize
that
the
array
slice
type
provides
exactly
what
we
need
and
one
should
simply
use
that
and
that
allows
us
to
get
rid
of
this.
The
C
code.
Hooray
right,
that's
awesome!
The
problem
is
that
that
that
we
have
no
domain
knowledge
in
in
in
in
a
mechanised
analysis.
A
So
we
have
to
do
something
well,
I'm,
not
sure
what
the
best
solution
is,
but
one
thing
I
could
imagine
or
be
convinced
that
a
mechanised
analysis
could
do
is
is
do
some
some
some
magic
swapping
where
we
basically
take
elements
out
of
of
the
array
and
pass
them
to
swap
both
mutable
and
then
put
them
back
into
the
array,
and
that
lets
us
do
is
actually
preserve
the
swap
function
as
as
we
have
it.
So
that's
that's
one
way
to
get
to
say
for
us,
but
it's
pie-in-the-sky.
It's
it's!
It's
an
open
question.