►
From YouTube: Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Description
Zvonimir Rakamaric
A
A
A
A
If
you
have
any
questions,
please
either
unmute
yourself
or
ask
them
in
the
chat
one
of
my
students,
who
is
a
collaborator
on
this
project.
Mark
baronovsky,
he's
here
as
well
and
so
he'll
be
keeping
an
eye
on
chad
as
well,
and
there
were
two
other
students
who
attribute
this
to
this
work:
jay,
garzella
and
shah,
boheh
and
and
this
project
is
supported
by
nsf,
amazon
and
vmware.
A
A
I'm
not
sure
how
many
of
you
are
familiar
with
boogie.
It's
a
pretty
popular
intermediate
verification
language,
supported
by
a
number
of
verification
tools
and
the
one
that
we
mainly
use
is
called
chorale
and
coral
is
basically
a
bounded
model,
checking
engine
with
some
advanced
techniques
to
make
it
scale
better.
A
Okay,
so
are
we
so?
The
main
advantage,
I
would
say
of
the
smack
verifier,
is
that
the
couple's
source
language
details
from
verifier
implementations
so
because
we
will
leverage
lumir
and
boogie
intermediate
verification
language,
and
that
enables,
as
we'll
see
also
in
this
talk
fast
verifier
input,
language
and
translation
prototyping.
A
A
If
you
develop
a
verifier
for
boogie,
you
plug
it
into
the
smack
tool
flow
and
you
have
instant
access
to
maybe
10
000
benchmark
or
something
like
that
on
which
you
can
try.
Your
verifier,
compare
it
with
the
existing
verifiers
and
so
on.
So
the
tool
is
free
and
open
source.
It
has
a
very
permissible
license.
It
is
it's
easy
to
use
in
the
industry
we
host
on
github.
A
A
So
you
know
we
plotted
on
something
like
open,
ssh
and
clearly
to
be
able
to
do
that.
You
have
to
understand
their
build
system.
Smek
is
fairly
automatic,
scalable,
precise
and
soundy.
We
try
to
kind
of
list
all
the
assumptions
we
make
in
terms
of
soundness
in
general.
False
bugs
are
quite
rare,
so
it's
remodeling
is
really
precise
and
then
whether
we
miss
bugs
or
not,
that
depends
on
the
select
backhand
verifier.
A
Usually
we
use
coral,
which
is
bounded
mullet
checking,
and
so
the
typical
reason
why
we
might
miss
bugs
is
if
we
don't
roll
loops
enough
and
then
it
generates
error
trace
for
debugging,
and
we
have
some
experimental
support
for
deductive
verification.
We
pre
post
conditions
and
it's
something
we
want
to
work
more
on.
A
Okay,
so
that's
the
overview
of
smack.
Let
me
just
quickly
walk
you
through
how
this
translation
works
into
boogie.
So
the
first
thing
we
do
is
we
translate
to
lmir
using
clang.
We
don't
do
anything
special
there,
it's
just
off
the
shelf
clan
compiler
and
here
is
a
small
example
c
program.
This
is
the
yellow
mirror
code
that
you
get
on
the
right
and
then
the
meat
of
smack
is
this
translation
into
boogie.
A
I
want
to
spend
a
little
bit
more
time
here.
I'm
not
going
to
go
into
details.
You
know
original
c
code
is
on
the
right.
It
goes
to
lmir
and
you
get
the
boogie
code
on
on
the
on
the
right
and,
if
you've
never
seen
boogie,
you
know
it's
a
procedural
language
and
it's
meant
for
verification,
so
the
type
system
is
kind
of
similar
to
what
you
see
in
smt
solvers.
A
So
there
are
no
things
like
pointers
and
so
on.
Usually
you
model
memory
using
areas,
and
you
can
see
this
area
dollar
m
here-
that
we
use
to
model
memory
and
another
important
thing
that
I
want
to
stress
out
is
that
you
know
the
original
c
code
involves
malloc
in
boogie.
We
translate
that
to
the
invocation
of
this
procedure
called
malloc,
but
we
have
to
provide
some
kind
of
model
for
this.
You
know
we
don't
translate
the
actual
allocators
into
boogie
directly,
but
rather
we
model
memory
allocation.
A
A
A
A
B
A
A
A
In
fact,
they
can
get
massed,
even
if
you
don't
enable
any
optimizations,
because
clang
will
sometimes
generate
interesting,
lvm
ir
depending
on
whether
you
have
undefined
behaviors
or
not.
So
we
don't
provide
any
guarantees
that
undefined
behaviours
are
not
going
to
get
messed.
Typically,
they
don't,
but
we
certainly
see
kind
of
corner
cases
where
we
just
don't
see
them
anymore
in
smack
and
you
might
miss
bugs
because
of
that
you
can
also
get
false
bugs
because
of
that,
and
so
on.
So.
A
Okay-
so
I
didn't
want
to
talk
more
about
this,
but
I
I
have
this
dream
that
all
these
kind
of
frontends,
like
clang
and
rossi
and
so
on,
will
one
day
have
a
target
called
verify
or
verification
where
the
kind
of
things
they
do
will
be
verification,
targeted
and,
for
example,
they're
not
going
to
mask
undefined
behaviors,
and
there
is
a
bunch
of
other
things
that
these
front
ends
kind
of.
Do
that
makes
verification
harder.
A
A
A
A
You
know
one
such
program
in
every
one
of
these
seven
languages
and
then
we
ran
smack
of
that
on
all
of
them
and
we
tried
to
extend
smack
kind
of
with
with
basic
things,
to
support
all
these
languages
and
here's
the
table.
That
summarizes
the
results,
and
you
know
xs
marked
features
that
smack
that
was
that
weren't
easy
to
support
and
smack
in
a
particular
language.
A
And
if
you
look
at
kind
of
x's
versus
checks
marks,
you
can
kind
of
see
that
you
know
c
c,
plus
plus
rust,
fortran
d
work
fairly
well,
almost
kind
of
out
of
the
box.
I'll
talk
more
about
this,
while
languages
such
as
objective
c,
swift
and
kotlin
are
much
harder
to
support,
and
this
is
typically
because
of
kind
of
dynamic
features
in
languages
and
big
run
times
and
so
on
that
are
present
in
objective
three
swift
and
kotlin.
A
So
the
the
more
similar
the
language
is
to
see
the
kind
of
easier
it
is
supported
in
smack.
So
fortran
is
an
example
of
a
language
that
it
worked
almost
out
of
the
box.
We
didn't
have
to
change
smack
at
all
and
we
could
verify
fairly
complex
programs
in
fortran
without
any
problems.
Just
because
it's
the
way
it's
compiled
into
lmir
is
very
similar
to
c,
okay
and
now
I'll
focus
on
what
we
did
with
rust
and
how
we
went
about
supporting
rust.
A
A
A
Then
we
have
some
common
models,
such
as,
for
example,
modeling
of
memory
allocation.
So
these
we
just
reused
from
what
was
written
for
c,
so
we
didn't
have
to
do
any
work
there.
So
memory
allocation
in
rust.
We
basically
use
the
same
model
as
as
what
we
have
for
c
and
then
in
this
lvm2
bpm
model
module.
A
We
had
to
extend
it
to
support
some
additional
lvmir
instructions
and
features
that
we
did
not
need
for
c
and
I'll
talk
more
about
these
in
the
upcoming
slides.
So
you
know,
smake
doesn't
support
the
whole
of
the
whole
of
lomir.
Lmr
is
really
big,
and
so
we
support
the
subset
and
the
subsidy
support
was
mainly
driven
by
what
clang
generates
to
support
rust.
We
had
to
add
a
few
more
things.
A
A
So
basically
we
can
compile
this
into
an
executable
as
well
and
in
that
case,
instead
of
non-domestic
value.
This
value
five
is
going
to
be
plugged
into
this
test
case,
and
then
you
can
check
assertion
assertions
very
similar
to
the
way
you
would
write
assertions
in
russ.
So
daniel
is
asking.
Why
do
we
need
to
make
a
cert
instead
of
just
a
cert?
A
It's
funny,
because
we
played
with
a
couple
of
different
syntaxes
and
it's
really
easy
to
support,
assert
as
well,
but
then
raz
doesn't
have
assume,
and
so
we
had
like
smack
assume
and
assert
and
we
were
kind
of
debating
what
to
do
to
make
it
consistent.
And
then
we
had
a
smack
in
front
of
a
cert,
but
we
can
support
assert
as
well
easily.
It
was
just
kind
of
a
syntactic
choice.
A
A
What
do
I
mean
by
structures
operations
so
lvmar
supports
structures,
so
a
function
can
return
a
structure.
You
can
take
a
structure
as
input
and
so
on.
The
c
compiler
clank
rarely
generates
coded
user
structures.
Rust
generates
it
all
the
time,
and
so
we
get
a
much
better
support
for
structures
in
smack.
We
model
them
as
android's
functions.
A
I'm
not
going
to
go
into
details,
how
we
do
that,
but
that's
kind
of
one
extension
that
was
needed
and
then
rust
uses
this
checked,
integer,
integer,
arithmetic,
all
the
time
that
wasn't
too
hard
to
to
support.
Typically,
we
perform
operations
in
double
bit
width
and
then
we
check
for
what
we
needed.
A
A
So
we
applied
smack
on
some
small,
let's
scale
real
world
programs
just
to
see
how
far
we
can
push
it.
So
we
picked
this
utils
library,
which
is
basically
implement
reimbursation
of
new
core
utils,
which
is
well
known
kind
of
test
bench
from
the
clip
project
and
we
verified
a
couple
of
simple
utilities.
There.
D
A
Work
a
lot
on
performance
and
scalability.
You
know
this
factor
utility.
It's
like
a
hundred
lines
of
code.
If
you
want
to
verify
kind
of
a
notion
of
functional
correctness,
it
takes
like
15
minutes,
which
is
way
too
long
and
they're
kind
of
good
reasons.
For
that
that
I
can
talk
about
more
okay,
so
one
advantage
of
using
lmir
as
opposed
to.
A
Something
like
mir
is
that
we
can
easily
do
cross
language
verification,
so
we
have
examples
with
that
mix,
rust,
unsafe,
rust
and
c,
and
we
can
just
handle
them
using.
You
know
off
the
shelf
smack
once
we
did
this
edition
additions,
and
so
so,
I
think,
that's
that's
kind
of
a
nice
side
effect
of
using
yellow
my
r.
I
have
one
such
example
here.
You
know
this
fibonacci
implementation
in
c.
A
I
won't
go
into
details,
but
you
know
we
can
invoke
it
from
rust.
We
can
pass
those
initial
values
for
it.
We
have
also
a
simple
implementation
of
fibonacci
and
rust.
We
can
check
that
return.
The
same
result-
and
this
is
all
really
easy
to
do
with
smack
you
compile
all
these
things.
You
link
them
together
and
it
just
works.
A
So
some
advantages.
So
we
avoid
the
mess
of
dealing
with
target
lanes
directly,
for
example,
something
like
rust
closures,
just
work,
they're
compiled
some
kind
of
function,
pointers
in
lmar
that
we
support
in
smack
and
you
write
russ
projects
with
closures
and
you
run
smack
on
it
and
things
just
work,
then
adding
back
and
verifies
and
solvers
is
easy.
I
already
mentioned
this
and
we
have
access
to
all
sorts
of
llvms
analysis,
optimizations
and
then.
A
A
A
And
then
you
know
in
terms
of
vector.
You
know
you
have
a
fine
line,
five
line.
We
saw
cases
where
we
have
a
five
line
program
that
uses
a
vector
and
it
takes.
You
know
15
minutes
to
verify,
because
this
implementation
of
the
vector
drags
in
like
lots
and
lots
of
additional
code
that
smack
has
to
go
through.
So.
A
Yeah,
that's
a
great
point.
Yes,
so
so
we
could
do
that
and
that's
something
that
we
would
like
to
do.
More
of
people
even
publish
these
papers.
You
know
automatically
generating
specifications,
summaries
and
stuff
like
that.
So
that's
something
we
could
try
to
explore
as
well,
but
so
yeah
you
could
write
a
simple
summary.
You
could
check
whether
the
implementation
matches
the
summary
and
then
you
could
just
use
this
summary
in
smac.
A
Okay,
so
mark
is
taking
care
of
a
bunch
of
questions
in
chat,
so
I'm
not
going
to
jump
there.
Let
me
talk,
maybe
a
minute
about
ongoing
work.
There
is
lots
of
it
and
we
are
really
interested
in
collaborating
with
people
here.
I
think
they're
kind
of
interesting
projects
that
we
could
kind
of
come
together
on,
so
we
want
to
modern
more
of
the
standard
libraries.
A
This
problem
kind
of
starts
comes
over
and
over
again
comes
up
over
and
over
again,
as
we
are
moving
to
more
and
more
kind
of
target
applications
we're
working
on
integrating
smart
smack
with
russ
verification
tools.
This
project
was
presented
here
as
well.
This
should
be
really
straightforward,
because
we
already
support
all
the
features
that
are
needed,
currently
we're
kind
of
focused
on
verification
of
unsafe
rust.
A
A
We
are
collaborating
with
my
colleague,
anthon
bertstrep,
from
uc
irvine
on
some
rust
os
verification,
but
we
are
always
kind
of
keeping
our
eyes
open
for
for
good
kind
of
medium-sized
benchmark,
let's
say
to
drive
the
work
and
then
there
is
this
benchmark
suite
that
we
have
been
working
on
it's
open
source.
It's
on
github.
A
So
I
know
dirk
bear
well
and
he
will
run
the
competition
for
you
as
long
as
you
provide
him
him
with
benchmarks,
and
so
the
organization
we
could
get
almost
for
free
and
I
have
kind
of
love
hate
relationships
with
these
competitions,
but
they
can
be
kind
of
useful
to
drive
the
area
forward
and
so
I'll
create.
Maybe
a
topic
on
the
chat
about
this.
A
D
A
A
So
I'm
not
sure
exactly
what
you
mean,
but,
for
example,
we
have
an
option
where
we
mod
the
pointers
at
kind
of
bite
level
accesses
at
byte
level,
and
so,
if
you
turn
something
you
know
into
narrative
bytes
and
then
you
read
the
second
byte
you'll
get
the
right
value
out
of
it
and
stuff
like
that.
What.
C
C
Yeah,
but
it
has
roots
right,
like
you
can't,
if,
if
you
leave
the
bounds
of
the
in
particular,
get
element
pointed
without
inbounds
can
is
allowed
you're
allowed
to
create
pointers
that
point
outside
the
bounds
of
the
allocation.
But
if
you
dereference
those
points,
it's
still
ub
because
it
still
is
like
attached.
It
remembers
the
original
object
the
pointer
comes
from,
and
you
can't
use
it
to
access
other
pointers,
but
yeah.
A
So
so
we
we
do
some
of
that
I
mean
it's
not
so
we
have
an
option
to
do
like
memory,
safety
checking
and
then
in
that
case
we
track
a
bunch
of
additional
information
about
objects
and
pointers,
and
so
on
that
allows
us
to
check
things
like
that.
I'm
sure
that
we
are
not
modeling
the
semantics
completely
and
totally
precisely,
but
we
do
a
little
bit
of
that
and
I'll
take
a
look
at
the
link
you
sent
and
then
maybe
I
can
comment
more.