Skip to content

Commit

Permalink
Support for stubbing out foreign functions (model-checking#2658)
Browse files Browse the repository at this point in the history
Signed-off-by: Felipe R. Monteiro <[email protected]>
  • Loading branch information
feliperodri authored Aug 8, 2023
1 parent 63f513f commit 6a151f9
Show file tree
Hide file tree
Showing 4 changed files with 136 additions and 13 deletions.
4 changes: 3 additions & 1 deletion kani-compiler/src/kani_middle/provide.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,9 @@ fn run_kani_mir_passes<'tcx>(
body: &'tcx Body<'tcx>,
) -> &'tcx Body<'tcx> {
tracing::debug!(?def_id, "Run Kani transformation passes");
stubbing::transform(tcx, def_id, body)
let mut transformed_body = stubbing::transform(tcx, def_id, body);
stubbing::transform_foreign_functions(tcx, &mut transformed_body);
tcx.arena.alloc(transformed_body)
}

/// Runs a reachability analysis before running the default
Expand Down
61 changes: 53 additions & 8 deletions kani-compiler/src/kani_middle/stubbing/transform.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,12 @@ use lazy_static::lazy_static;
use regex::Regex;
use rustc_data_structures::fingerprint::Fingerprint;
use rustc_hir::{def_id::DefId, definitions::DefPathHash};
use rustc_middle::{mir::Body, ty::TyCtxt};
use rustc_index::IndexVec;
use rustc_middle::mir::{
interpret::ConstValue, visit::MutVisitor, Body, ConstantKind, Local, LocalDecl, Location,
Operand,
};
use rustc_middle::ty::{self, TyCtxt};

/// Returns the `DefId` of the stub for the function/method identified by the
/// parameter `def_id`, and `None` if the function/method is not stubbed.
Expand All @@ -23,18 +28,58 @@ pub fn get_stub(tcx: TyCtxt, def_id: DefId) -> Option<DefId> {

/// Returns the new body of a function/method if it has been stubbed out;
/// otherwise, returns the old body.
pub fn transform<'tcx>(
tcx: TyCtxt<'tcx>,
def_id: DefId,
old_body: &'tcx Body<'tcx>,
) -> &'tcx Body<'tcx> {
pub fn transform<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, old_body: &'tcx Body<'tcx>) -> Body<'tcx> {
if let Some(replacement) = get_stub(tcx, def_id) {
let new_body = tcx.optimized_mir(replacement).clone();
if check_compatibility(tcx, def_id, old_body, replacement, &new_body) {
return tcx.arena.alloc(new_body);
return new_body;
}
}
old_body.clone()
}

/// Traverse `body` searching for calls to foreing functions and, whevever there is
/// a stub available, replace the call to the foreign function with a call
/// to its correspondent stub. This happens as a separate step because there is no
/// body available to foreign functions at this stage.
pub fn transform_foreign_functions<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) {
if let Some(stub_map) = get_stub_mapping(tcx) {
let mut visitor =
ForeignFunctionTransformer { tcx, local_decls: body.clone().local_decls, stub_map };
visitor.visit_body(body);
}
}

struct ForeignFunctionTransformer<'tcx> {
/// The compiler context.
tcx: TyCtxt<'tcx>,
/// Local declarations of the callee function. Kani searches here for foreign functions.
local_decls: IndexVec<Local, LocalDecl<'tcx>>,
/// Map of functions/methods to their correspondent stubs.
stub_map: HashMap<DefId, DefId>,
}

impl<'tcx> MutVisitor<'tcx> for ForeignFunctionTransformer<'tcx> {
fn tcx(&self) -> TyCtxt<'tcx> {
self.tcx
}

fn visit_operand(&mut self, operand: &mut Operand<'tcx>, _location: Location) {
let func_ty = operand.ty(&self.local_decls, self.tcx);
if let ty::FnDef(reachable_function, arguments) = *func_ty.kind() {
if self.tcx.is_foreign_item(reachable_function) {
if let Some(stub) = self.stub_map.get(&reachable_function) {
let Operand::Constant(function_definition) = operand else {
return;
};
function_definition.literal = ConstantKind::from_value(
ConstValue::ZeroSized,
self.tcx.type_of(stub).instantiate(self.tcx, arguments),
);
}
}
}
}
old_body
}

/// Checks whether the stub is compatible with the original function/method: do
Expand Down
8 changes: 4 additions & 4 deletions tests/.gitignore
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
*.goto
# Temporary files and folders
*.json

# Temporary folders
rmet*/
kani_concrete_playback
rmet*/
target/

# Binary artifacts
*.goto
*out
smoke
check_tests
Expand Down
76 changes: 76 additions & 0 deletions tests/kani/Stubbing/foreign_functions.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// kani-flags: --enable-unstable --enable-stubbing
//
//! Check support for stubbing out foreign functions.
#![feature(rustc_private)]
extern crate libc;

use libc::c_char;
use libc::c_int;
use libc::c_longlong;
use libc::size_t;

#[allow(dead_code)] // Avoid warning when using stubs.
#[allow(unused_variables)]
mod stubs {
use super::*;

pub unsafe extern "C" fn strlen(cs: *const c_char) -> size_t {
4
}

pub unsafe extern "C" fn sysconf(_input: c_int) -> c_longlong {
10
}
}

fn dig_deeper(input: c_int) {
unsafe {
type FunctionPointerType = unsafe extern "C" fn(c_int) -> c_longlong;
let ptr: FunctionPointerType = libc::sysconf;
assert_eq!(ptr(input) as usize, 10);
}
}

fn deeper_call() {
dig_deeper(libc::_SC_PAGESIZE)
}

fn function_pointer_call(function_pointer: unsafe extern "C" fn(c_int) -> c_longlong) {
assert_eq!(unsafe { function_pointer(libc::_SC_PAGESIZE) } as usize, 10);
}

#[kani::proof]
#[kani::stub(libc::strlen, stubs::strlen)]
fn standard() {
let str: Box<i8> = Box::new(4);
let str_ptr: *const i8 = &*str;
assert_eq!(unsafe { libc::strlen(str_ptr) }, 4);
}

#[kani::proof]
#[kani::stub(libc::strlen, stubs::strlen)]
fn function_pointer_standard() {
let str: Box<i8> = Box::new(4);
let str_ptr: *const i8 = &*str;
let new_ptr = libc::strlen;
assert_eq!(unsafe { new_ptr(str_ptr) }, 4);
}

#[kani::proof]
#[kani::stub(libc::sysconf, stubs::sysconf)]
fn function_pointer_with_layers() {
deeper_call();
}

#[kani::proof]
#[kani::stub(libc::sysconf, stubs::sysconf)]
fn function_pointer_as_parameter() {
type FunctionPointerType = unsafe extern "C" fn(c_int) -> c_longlong;
let function_pointer: FunctionPointerType = libc::sysconf;
function_pointer_call(function_pointer);
function_pointer_call(libc::sysconf);
}

0 comments on commit 6a151f9

Please sign in to comment.