Skip to content

Commit 670b9b6

Browse files
committed
Upgrade Rust support for LLVM 8
* Install the most recent Rust compiler to support LLVM 8 * Improve entry point detection * Streamline Rust compiler installation. Closes #489
1 parent b820162 commit 670b9b6

File tree

4 files changed

+6
-7
lines changed

4 files changed

+6
-7
lines changed

bin/build.sh

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -387,8 +387,9 @@ if [ ${INSTALL_RUST} -eq 1 ] ; then
387387
${WGET} https://static.rust-lang.org/dist/${RUST_VERSION}/rust-nightly-x86_64-unknown-linux-gnu.tar.gz -O rust.tar.gz
388388
tar xf rust.tar.gz
389389
cd rust-nightly-x86_64-unknown-linux-gnu
390-
sudo ./install.sh
390+
sudo ./install.sh --without=rust-docs
391391
cd ..
392+
rm -r rust-nightly-x86_64-unknown-linux-gnu rust.tar.gz
392393

393394
puts "Installed Rust"
394395
fi

bin/versions

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,4 +8,4 @@ SYMBOOGLIX_COMMIT=7210e5d09b
88
LOCKPWN_COMMIT=73eddf97bd
99
LLVM_SHORT_VERSION=8
1010
LLVM_FULL_VERSION=8.0.1
11-
RUST_VERSION=2016-12-16
11+
RUST_VERSION=2019-07-16

lib/smack/SmackInstGenerator.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -646,10 +646,8 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) {
646646
} else if (name.find(Naming::RUST_ENTRY) != std::string::npos) {
647647
// Set the entry point for Rust programs
648648
auto castExpr = ci.getArgOperand(0);
649-
if (auto CE = dyn_cast<const Constant>(castExpr)) {
650-
auto mainFunc = CE->getOperand(0);
651-
emit(Stmt::call(mainFunc->getName(), {}, {}));
652-
}
649+
auto mainFunction = cast<const Function>(castExpr);
650+
emit(Stmt::call(mainFunction->getName(), {}, {}));
653651

654652
} else if (name.find(Naming::RUST_PANIC1) != std::string::npos ||
655653
name.find(Naming::RUST_PANIC2) != std::string::npos) {

share/smack/frontend.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -220,7 +220,7 @@ def rust_frontend(input_file, args):
220220
"""Generate Boogie code from Rust programming language source(s)."""
221221
compile_command = ['rustc', '-A', 'unused-imports', '-C', 'opt-level=0',
222222
'-C', 'no-prepopulate-passes', '-g', '--emit=llvm-bc',
223-
'--cfg', 'verifier="smack"']
223+
'--cfg', 'verifier="smack"', '-C', 'passes=name-anon-globals']
224224

225225
# This links in the Rust SMACK library. This is needed due to the way rustc
226226
# finds a programs libraries.

0 commit comments

Comments
 (0)