Contracts for a few core functions

Cargo.toml

@@ -62,6 +62,7 @@ exclude = [
   "tests/perf",
   "tests/cargo-ui",
   "tests/slow",
+  "tests/std-checks",
   "tests/assess-scan-test-scaffold",
   "tests/script-based-pre",
   "tests/script-based-pre/build-cache-bin/target/new_dep",

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -211,7 +211,7 @@ impl GotocHook for Panic {
 struct IsReadOk;
 impl GotocHook for IsReadOk {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        matches_function(tcx, instance.def, "KaniIsReadOk")
+        matches_function(tcx, instance.def, "KaniIsValidPtr")
     }
 
     fn handle(

kani-compiler/src/kani_middle/transform/body.rs

@@ -12,6 +12,7 @@ use stable_mir::mir::{
     VarDebugInfo,
 };
 use stable_mir::ty::{Const, GenericArgs, Span, Ty, UintTy};
+use std::fmt::Debug;
 use std::mem;
 
 /// This structure mimics a Body that can actually be modified.
@@ -224,6 +225,15 @@ impl MutableBody {
             }
         }
     }
+
+    /// Clear all the existing logic of this body and turn it into a simple `return`.
+    ///
+    /// We do not prune the local variables today for simplicity.
+    pub fn clear_body(&mut self) {
+        self.blocks.clear();
+        let terminator = Terminator { kind: TerminatorKind::Return, span: self.span };
+        self.blocks.push(BasicBlock { statements: Vec::default(), terminator })
+    }
 }
 
 #[derive(Clone, Debug)]

kani-compiler/src/kani_middle/transform/check_values.rs

@@ -19,7 +19,6 @@ use crate::kani_middle::transform::check_values::SourceOp::UnsupportedCheck;
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, WrappingRange};
 use stable_mir::mir::mono::{Instance, InstanceKind};
 use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef};
@@ -31,19 +30,14 @@ use stable_mir::mir::{
 use stable_mir::target::{MachineInfo, MachineSize};
 use stable_mir::ty::{AdtKind, Const, IndexedVal, RigidTy, Ty, TyKind, UintTy};
 use stable_mir::CrateDef;
-use std::fmt::{Debug, Formatter};
+use std::fmt::Debug;
 use strum_macros::AsRefStr;
 use tracing::{debug, trace};
 
 /// Instrument the code with checks for invalid values.
+#[derive(Debug)]
 pub struct ValidValuePass {
-    check_type: CheckType,
-}
-
-impl ValidValuePass {
-    pub fn new(tcx: TyCtxt) -> Self {
-        ValidValuePass { check_type: CheckType::new(tcx) }
-    }
+    pub check_type: CheckType,
 }
 
 impl TransformPass for ValidValuePass {
@@ -81,13 +75,6 @@ impl TransformPass for ValidValuePass {
     }
 }
 
-impl Debug for ValidValuePass {
-    /// Implement manually since MachineInfo doesn't currently derive Debug.
-    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
-        "ValidValuePass".fmt(f)
-    }
-}
-
 impl ValidValuePass {
     fn build_check(&self, tcx: TyCtxt, body: &mut MutableBody, instruction: UnsafeInstruction) {
         debug!(?instruction, "build_check");
@@ -98,89 +85,30 @@ impl ValidValuePass {
                     let value = body.new_assignment(rvalue, &mut source);
                     let rvalue_ptr = Rvalue::AddressOf(Mutability::Not, Place::from(value));
                     for range in ranges {
-                        let result =
-                            self.build_limits(body, &range, rvalue_ptr.clone(), &mut source);
-                        let msg = format!(
-                            "Undefined Behavior: Invalid value of type `{}`",
-                            // TODO: Fix pretty_ty
-                            rustc_internal::internal(tcx, target_ty)
-                        );
+                        let result = build_limits(body, &range, rvalue_ptr.clone(), &mut source);
+                        let msg =
+                            format!("Undefined Behavior: Invalid value of type `{target_ty}`",);
                         body.add_check(tcx, &self.check_type, &mut source, result, &msg);
                     }
                 }
                 SourceOp::DerefValidity { pointee_ty, rvalue, ranges } => {
                     for range in ranges {
-                        let result = self.build_limits(body, &range, rvalue.clone(), &mut source);
-                        let msg = format!(
-                            "Undefined Behavior: Invalid value of type `{}`",
-                            // TODO: Fix pretty_ty
-                            rustc_internal::internal(tcx, pointee_ty)
-                        );
+                        let result = build_limits(body, &range, rvalue.clone(), &mut source);
+                        let msg =
+                            format!("Undefined Behavior: Invalid value of type `{pointee_ty}`",);
                         body.add_check(tcx, &self.check_type, &mut source, result, &msg);
                     }
                 }
                 SourceOp::UnsupportedCheck { check, ty } => {
                     let reason = format!(
-                        "Kani currently doesn't support checking validity of `{check}` for `{}` type",
-                        rustc_internal::internal(tcx, ty)
+                        "Kani currently doesn't support checking validity of `{check}` for `{ty}`",
                     );
                     self.unsupported_check(tcx, body, &mut source, &reason);
                 }
             }
         }
     }
 
-    fn build_limits(
-        &self,
-        body: &mut MutableBody,
-        req: &ValidValueReq,
-        rvalue_ptr: Rvalue,
-        source: &mut SourceInstruction,
-    ) -> Local {
-        let span = source.span(body.blocks());
-        debug!(?req, ?rvalue_ptr, ?span, "build_limits");
-        let primitive_ty = uint_ty(req.size.bytes());
-        let start_const = body.new_const_operand(req.valid_range.start, primitive_ty, span);
-        let end_const = body.new_const_operand(req.valid_range.end, primitive_ty, span);
-        let orig_ptr = if req.offset != 0 {
-            let start_ptr = move_local(body.new_assignment(rvalue_ptr, source));
-            let byte_ptr = move_local(body.new_cast_ptr(
-                start_ptr,
-                Ty::unsigned_ty(UintTy::U8),
-                Mutability::Not,
-                source,
-            ));
-            let offset_const = body.new_const_operand(req.offset as _, UintTy::Usize, span);
-            let offset = move_local(body.new_assignment(Rvalue::Use(offset_const), source));
-            move_local(body.new_binary_op(BinOp::Offset, byte_ptr, offset, source))
-        } else {
-            move_local(body.new_assignment(rvalue_ptr, source))
-        };
-        let value_ptr =
-            body.new_cast_ptr(orig_ptr, Ty::unsigned_ty(primitive_ty), Mutability::Not, source);
-        let value =
-            Operand::Copy(Place { local: value_ptr, projection: vec![ProjectionElem::Deref] });
-        let start_result = body.new_binary_op(BinOp::Ge, value.clone(), start_const, source);
-        let end_result = body.new_binary_op(BinOp::Le, value, end_const, source);
-        if req.valid_range.wraps_around() {
-            // valid >= start || valid <= end
-            body.new_binary_op(
-                BinOp::BitOr,
-                move_local(start_result),
-                move_local(end_result),
-                source,
-            )
-        } else {
-            // valid >= start && valid <= end
-            body.new_binary_op(
-                BinOp::BitAnd,
-                move_local(start_result),
-                move_local(end_result),
-                source,
-            )
-        }
-    }
-
     fn unsupported_check(
         &self,
         tcx: TyCtxt,
@@ -216,7 +144,7 @@ fn uint_ty(bytes: usize) -> UintTy {
 
 /// Represent a requirement for the value stored in the given offset.
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
-struct ValidValueReq {
+pub struct ValidValueReq {
     /// Offset in bytes.
     offset: usize,
     /// Size of this requirement.
@@ -783,10 +711,49 @@ fn expect_instance(locals: &[LocalDecl], func: &Operand) -> Instance {
     }
 }
 
+pub fn build_limits(
+    body: &mut MutableBody,
+    req: &ValidValueReq,
+    rvalue_ptr: Rvalue,
+    source: &mut SourceInstruction,
+) -> Local {
+    let span = source.span(body.blocks());
+    debug!(?req, ?rvalue_ptr, ?span, "build_limits");
+    let primitive_ty = uint_ty(req.size.bytes());
+    let start_const = body.new_const_operand(req.valid_range.start, primitive_ty, span);
+    let end_const = body.new_const_operand(req.valid_range.end, primitive_ty, span);
+    let orig_ptr = if req.offset != 0 {
+        let start_ptr = move_local(body.new_assignment(rvalue_ptr, source));
+        let byte_ptr = move_local(body.new_cast_ptr(
+            start_ptr,
+            Ty::unsigned_ty(UintTy::U8),
+            Mutability::Not,
+            source,
+        ));
+        let offset_const = body.new_const_operand(req.offset as _, UintTy::Usize, span);
+        let offset = move_local(body.new_assignment(Rvalue::Use(offset_const), source));
+        move_local(body.new_binary_op(BinOp::Offset, byte_ptr, offset, source))
+    } else {
+        move_local(body.new_assignment(rvalue_ptr, source))
+    };
+    let value_ptr =
+        body.new_cast_ptr(orig_ptr, Ty::unsigned_ty(primitive_ty), Mutability::Not, source);
+    let value = Operand::Copy(Place { local: value_ptr, projection: vec![ProjectionElem::Deref] });
+    let start_result = body.new_binary_op(BinOp::Ge, value.clone(), start_const, source);
+    let end_result = body.new_binary_op(BinOp::Le, value, end_const, source);
+    if req.valid_range.wraps_around() {
+        // valid >= start || valid <= end
+        body.new_binary_op(BinOp::BitOr, move_local(start_result), move_local(end_result), source)
+    } else {
+        // valid >= start && valid <= end
+        body.new_binary_op(BinOp::BitAnd, move_local(start_result), move_local(end_result), source)
+    }
+}
+
 /// Traverse the type and find all invalid values and their location in memory.
 ///
 /// Not all values are currently supported. For those not supported, we return Error.
-fn ty_validity_per_offset(
+pub fn ty_validity_per_offset(
     machine_info: &MachineInfo,
     ty: Ty,
     current_offset: usize,

kani-compiler/src/kani_middle/transform/kani_intrinsics.rs

@@ -0,0 +1,138 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Module responsible for generating code for a few Kani intrinsics.
+//!
+//! These intrinsics have code that depend on information from the compiler, such as type layout
+//! information; thus, they are implemented as a transformation pass where their body get generated
+//! by the transformation.
+
+use crate::kani_middle::attributes::matches_diagnostic;
+use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruction};
+use crate::kani_middle::transform::check_values::{build_limits, ty_validity_per_offset};
+use crate::kani_middle::transform::{TransformPass, TransformationType};
+use crate::kani_queries::QueryDb;
+use rustc_middle::ty::TyCtxt;
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::{
+    BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL,
+};
+use stable_mir::target::MachineInfo;
+use stable_mir::ty::{Const, RigidTy, TyKind};
+use std::fmt::Debug;
+use strum_macros::AsRefStr;
+use tracing::trace;
+
+/// Generate the body for a few Kani intrinsics.
+#[derive(Debug)]
+pub struct IntrinsicGeneratorPass {
+    pub check_type: CheckType,
+}
+
+impl TransformPass for IntrinsicGeneratorPass {
+    fn transformation_type() -> TransformationType
+    where
+        Self: Sized,
+    {
+        TransformationType::Instrumentation
+    }
+
+    fn is_enabled(&self, _query_db: &QueryDb) -> bool
+    where
+        Self: Sized,
+    {
+        true
+    }
+
+    /// Transform the function body by inserting checks one-by-one.
+    /// For every unsafe dereference or a transmute operation, we check all values are valid.
+    fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+        trace!(function=?instance.name(), "transform");
+        if matches_diagnostic(tcx, instance.def, Intrinsics::KaniValidValue.as_ref()) {
+            (true, self.valid_value_body(tcx, body))
+        } else {
+            (false, body)
+        }
+    }
+}
+
+impl IntrinsicGeneratorPass {
+    /// Generate the body for valid value. Which should be something like:
+    ///
+    /// ```
+    /// pub fn has_valid_value<T>(ptr: *const T) -> bool {
+    ///     let mut ret = true;
+    ///     let bytes = ptr as *const u8;
+    ///     for req in requirements {
+    ///         ret &= in_range(bytes, req);
+    ///     }
+    ///     ret
+    /// }
+    /// ```
+    fn valid_value_body(&self, tcx: TyCtxt, body: Body) -> Body {
+        let mut new_body = MutableBody::from(body);
+        new_body.clear_body();
+
+        // Initialize return variable with True.
+        let ret_var = RETURN_LOCAL;
+        let mut terminator = SourceInstruction::Terminator { bb: 0 };
+        let span = new_body.locals()[ret_var].span;
+        let assign = StatementKind::Assign(
+            Place::from(ret_var),
+            Rvalue::Use(Operand::Constant(Constant {
+                span,
+                user_ty: None,
+                literal: Const::from_bool(true),
+            })),
+        );
+        let stmt = Statement { kind: assign, span };
+        new_body.insert_stmt(stmt, &mut terminator);
+        let machine_info = MachineInfo::target();
+
+        // First argument type.
+        let arg_ty = new_body.locals()[1].ty;
+        let TyKind::RigidTy(RigidTy::RawPtr(target_ty, _)) = arg_ty.kind() else { unreachable!() };
+        let validity = ty_validity_per_offset(&machine_info, target_ty, 0);
+        match validity {
+            Ok(ranges) if ranges.is_empty() => {
+                // Nothing to check
+            }
+            Ok(ranges) => {
+                // Given the pointer argument, check for possible invalid ranges.
+                let rvalue = Rvalue::Use(Operand::Move(Place::from(1)));
+                for range in ranges {
+                    let result =
+                        build_limits(&mut new_body, &range, rvalue.clone(), &mut terminator);
+                    let rvalue = Rvalue::BinaryOp(
+                        BinOp::BitAnd,
+                        Operand::Move(Place::from(ret_var)),
+                        Operand::Move(Place::from(result)),
+                    );
+                    let assign = StatementKind::Assign(Place::from(ret_var), rvalue);
+                    let stmt = Statement { kind: assign, span };
+                    new_body.insert_stmt(stmt, &mut terminator);
+                }
+            }
+            Err(msg) => {
+                // We failed to retrieve all the valid ranges.
+                let rvalue = Rvalue::Use(Operand::Constant(Constant {
+                    literal: Const::from_bool(false),
+                    span,
+                    user_ty: None,
+                }));
+                let result = new_body.new_assignment(rvalue, &mut terminator);
+                let reason = format!(
+                    "Kani currently doesn't support checking validity of `{target_ty}`. {msg}"
+                );
+                new_body.add_check(tcx, &self.check_type, &mut terminator, result, &reason);
+            }
+        }
+        new_body.into()
+    }
+}
+
+#[derive(Debug, Copy, Clone, Eq, PartialEq, AsRefStr)]
+#[strum(serialize_all = "PascalCase")]
+enum Intrinsics {
+    KaniValidValue,
+}