Using command-line arguments ('argv')
One important difference between C and Rust is that the C main function expects
to be given a list of command line arguments via argc
/argv
function
parameters while Rust programs access their command line arguments via the
sys::env::args()
library function.
This raises the problem when verifying Rust programs of how can we pass command line arguments to a program when we are verifying it. This document sketches how Rust’s command line arguments work (on Linux) and how we can set them when verifying Rust programs.
[Note:
You should not need any of the information in this note to
use propverify
if you are using the cargo-verify
script.
These instructions are mostly useful if you want to create your own
tools or if you hit problems.]
How Rust handles command-line arguments (on Linux)
[For more information about this, see this blog post and, of course, the source code.]
The Rust runtime system provides an initializer function
ARGV_INIT_ARRAY::init_wrapper(argc, argv, envp)
that saves the values of
argc
and argv
in global variables so that they can be accessed later by
std::env::args()
and it places a pointer to this function in a global variable
in an ELF section called .init_array_000099
.
When the Linux kernel runs a Rust program, it starts by executing code from the GNU C
library. This library calls some initialization functions before calling the
Rust main
function. These initialization functions are found in ELF
sections with names like .init_array
and they expect to be called with three
arguments: argc
, argv
and envp
.
How our tools handle command-line arguments
To make it possible to pass command-line arguments to a program when it is being
verified, we need to arrange that the initialization functions are called and that
they are passed the values of argc
and argv
.
(I am unsure whether we also need to pass the value of envp
.)
Since verification tools like KLEE
are normally used to verify C programs,
they expect to start with a call to main(argc, argv)
so, to verify Rust programs,
we need to arrange that calling main
will call any initialization functions.
We do this by transforming the LLVM bitcode file generated by the Rust compiler
so that the first thing that main
does is to call all the initialization functions
and to pass them the values of argc/argv
.
The cargo-verify
script invokes this transformation if any command line arguments
are passed to the program.
This results in an LLVM main
function like this (the change is the third line that calls __init_function
).
define i32 @main(i32 %0, i8** nocapture readnone %1) unnamed_addr #5 {
top:
call void @__init_function(i32 %0, i8** %1, i8** null)
%2 = load volatile i8, i8* getelementptr inbounds ([34 x i8], [34 x i8]* @__rustc_debug_gdb_scripts_section__, i64 0, i64 0), align 1
%3 = sext i32 %0 to i64
%4 = call i64 @_ZN3std2rt10lang_start17ha6542edf6afbeb15E(void ()* @_ZN4argv4main17h878bf90218e36557E, i64 %3, i8** %1)
%5 = trunc i64 %4 to i32
call void @klee.dtor_stub()
ret i32 %5
}
and the __init_function
that calls all the initializers looks like this
define void @__init_function(i32 %0, i8** %1, i8** %2) {
entry:
call void @_ZN3std3sys4unix4args3imp15ARGV_INIT_ARRAY12init_wrapper17hac2c035213cf4e54E(i32 %0, i8** %1, i8** %2)
ret void
}