Add method to assert a pointer is valid (model-checking#3062)

This new method will assert that a pointer isn't null, and that its is
valid for access of a given type.

Co-authored-by: Zyad Hassan <[email protected]>

cprover_bindings/src/goto_program/expr.rs

@@ -126,6 +126,10 @@ pub enum ExprValue {
     Nondet,
     /// `NULL`
     PointerConstant(u64),
+    ReadOk {
+        ptr: Expr,
+        size: Expr,
+    },
     // `op++` etc
     SelfOp {
         op: SelfOperator,
@@ -717,6 +721,14 @@ impl Expr {
         expr!(Nondet, typ)
     }
 
+    /// `read_ok(ptr, size)`
+    pub fn read_ok(ptr: Expr, size: Expr) -> Self {
+        assert_eq!(*ptr.typ(), Type::void_pointer());
+        assert_eq!(*size.typ(), Type::size_t());
+
+        expr!(ReadOk { ptr, size }, Type::bool())
+    }
+
     /// `e.g. NULL`
     pub fn pointer_constant(c: u64, typ: Type) -> Self {
         assert!(typ.is_pointer());

cprover_bindings/src/irep/to_irep.rs

@@ -293,6 +293,11 @@ impl ToIrep for ExprValue {
                     Irep::just_bitpattern_id(*i, mm.pointer_width, false)
                 )],
             },
+            ExprValue::ReadOk { ptr, size } => Irep {
+                id: IrepId::ROk,
+                sub: vec![ptr.to_irep(mm), size.to_irep(mm)],
+                named_sub: linear_map![],
+            },
             ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
             ExprValue::StatementExpression { statements: ops } => side_effect_irep(
                 IrepId::StatementExpression,

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

@@ -217,6 +217,41 @@ impl GotocHook for Panic {
     }
 }
 
+/// Encodes __CPROVER_r_ok
+struct IsReadOk;
+impl GotocHook for IsReadOk {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance, "KaniIsReadOk")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        mut fargs: Vec<Expr>,
+        assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 2);
+        let size = fargs.pop().unwrap();
+        let ptr = fargs.pop().unwrap().cast_to(Type::void_pointer());
+        let target = target.unwrap();
+        let loc = gcx.codegen_caller_span_stable(span);
+        let ret_place =
+            unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to));
+        let ret_type = ret_place.goto_expr.typ().clone();
+
+        Stmt::block(
+            vec![
+                ret_place.goto_expr.assign(Expr::read_ok(ptr, size).cast_to(ret_type), loc),
+                Stmt::goto(bb_label(target), Location::none()),
+            ],
+            Location::none(),
+        )
+    }
+}
+
 struct RustAlloc;
 // Removing this hook causes regression failures.
 // https://github.com/model-checking/kani/issues/1170
@@ -373,6 +408,7 @@ pub fn fn_hooks() -> GotocHooks {
             Rc::new(Assert),
             Rc::new(Cover),
             Rc::new(Nondet),
+            Rc::new(IsReadOk),
             Rc::new(RustAlloc),
             Rc::new(MemCmp),
             Rc::new(UntrackedDeref),

kani_metadata/src/unstable.rs

@@ -82,6 +82,8 @@ pub enum UnstableFeature {
     LineCoverage,
     /// Enable function contracts [RFC 9](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html)
     FunctionContracts,
+    /// Memory predicate APIs.
+    MemPredicates,
 }
 
 impl UnstableFeature {

library/kani/src/lib.rs

@@ -14,13 +14,16 @@
 #![feature(repr_simd)]
 // Features used for tests only.
 #![cfg_attr(test, feature(core_intrinsics, portable_simd))]
-// Required for rustc_diagnostic_item
+// Required for `rustc_diagnostic_item` and `core_intrinsics`
 #![allow(internal_features)]
+// Required for implementing memory predicates.
+#![feature(ptr_metadata)]
 
 pub mod arbitrary;
 #[cfg(feature = "concrete_playback")]
 mod concrete_playback;
 pub mod futures;
+pub mod mem;
 pub mod slice;
 pub mod tuple;
 pub mod vec;
@@ -33,6 +36,7 @@ mod models;
 pub use arbitrary::Arbitrary;
 #[cfg(feature = "concrete_playback")]
 pub use concrete_playback::concrete_playback_run;
+
 #[cfg(not(feature = "concrete_playback"))]
 /// NOP `concrete_playback` for type checking during verification mode.
 pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
@@ -80,18 +84,12 @@ pub fn assume(cond: bool) {
 /// `implies!(premise => conclusion)` means that if the `premise` is true, so
 /// must be the `conclusion`.
 ///
-/// This simply expands to `!premise || conclusion` and is intended to be used
-/// in function contracts to make them more readable, as the concept of an
-/// implication is more natural to think about than its expansion.
-///
-/// For further convenience multiple comma separated premises are allowed, and
-/// are joined with `||` in the expansion. E.g. `implies!(a, b => c)` expands to
-/// `!a || !b || c` and says that `c` is true if both `a` and `b` are true (see
-/// also [Horn Clauses](https://en.wikipedia.org/wiki/Horn_clause)).
+/// This simply expands to `!premise || conclusion` and is intended to make checks more readable,
+/// as the concept of an implication is more natural to think about than its expansion.
 #[macro_export]
 macro_rules! implies {
-    ($($premise:expr),+ => $conclusion:expr) => {
-        $(!$premise)||+ || ($conclusion)
+    ($premise:expr => $conclusion:expr) => {
+        !($premise) || ($conclusion)
     };
 }
 
@@ -217,13 +215,7 @@ pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
 #[inline(never)]
 #[allow(dead_code)]
 fn any_raw_inner<T>() -> T {
-    // while we could use `unreachable!()` or `panic!()` as the body of this
-    // function, both cause Kani to produce a warning on any program that uses
-    // kani::any() (see https://github.com/model-checking/kani/issues/2010).
-    // This function is handled via a hook anyway, so we just need to put a body
-    // that rustc does not complain about. An infinite loop works out nicely.
-    #[allow(clippy::empty_loop)]
-    loop {}
+    kani_intrinsic()
 }
 
 /// Function used to generate panic with a static message as this is the only one currently
@@ -239,6 +231,20 @@ pub const fn panic(message: &'static str) -> ! {
     panic!("{}", message)
 }
 
+/// An empty body that can be used to define Kani intrinsic functions.
+///
+/// A Kani intrinsic is a function that is interpreted by Kani compiler.
+/// While we could use `unreachable!()` or `panic!()` as the body of a kani intrinsic
+/// function, both cause Kani to produce a warning since we don't support caller location.
+/// (see https://github.com/model-checking/kani/issues/2010).
+///
+/// This function is dead, since its caller is always  handled via a hook anyway,
+/// so we just need to put a body that rustc does not complain about.
+/// An infinite loop works out nicely.
+fn kani_intrinsic<T>() -> T {
+    #[allow(clippy::empty_loop)]
+    loop {}
+}
 /// A macro to check if a condition is satisfiable at a specific location in the
 /// code.
 ///