|
| 1 | +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. |
| 2 | +// SPDX-License-Identifier: Apache-2.0 OR MIT |
| 3 | +// compile-flags: --crate-type lib |
| 4 | +// kani-flags: --function find_error |
| 5 | +#![feature(decl_macro)] |
| 6 | + |
| 7 | +pub type Key = i8; |
| 8 | +pub struct Metadata { |
| 9 | + header: u32, |
| 10 | + typ: Option<i8>, |
| 11 | +} |
| 12 | + |
| 13 | +impl Metadata { |
| 14 | + pub fn unknown(&self) -> bool { |
| 15 | + self.typ.is_some() |
| 16 | + } |
| 17 | +} |
| 18 | + |
| 19 | +pub fn find(key: &Key) -> Result<Metadata, defs::Error> { |
| 20 | + use crate::defs::INVALID_KEY_ERROR; |
| 21 | + |
| 22 | + let metadata = Metadata { header: 0, typ: None }; |
| 23 | + if metadata.unknown() && (*key < 0) { |
| 24 | + return Err(INVALID_KEY_ERROR); |
| 25 | + } |
| 26 | + Ok(metadata) |
| 27 | +} |
| 28 | + |
| 29 | +#[cfg(kani)] |
| 30 | +mod proof_harnesses { |
| 31 | + use super::*; |
| 32 | + |
| 33 | + #[kani::proof] |
| 34 | + fn find_error() { |
| 35 | + let key = kani::any::<Key>(); |
| 36 | + kani::assume(key > 0); |
| 37 | + assert!(find(&key).is_ok()); |
| 38 | + } |
| 39 | +} |
| 40 | + |
| 41 | +/// This module is a reduced testcase from file handling in the std. |
| 42 | +pub mod defs { |
| 43 | + |
| 44 | + use std::ptr::NonNull; |
| 45 | + |
| 46 | + pub(crate) const INVALID_KEY_ERROR: Error = const_io_error!( |
| 47 | + ErrorKind::InvalidInput, |
| 48 | + "the source path is neither a regular file nor a symlink to a regular file", |
| 49 | + ); |
| 50 | + |
| 51 | + /// Create and return an `Error` for a given `ErrorKind` and constant |
| 52 | + /// message. This doesn't allocate. |
| 53 | + pub(crate) macro const_io_error($kind:expr, $message:expr $(,)?) { |
| 54 | + $crate::defs::Error::from_static_message({ |
| 55 | + const MESSAGE_DATA: $crate::defs::SimpleMessage = |
| 56 | + $crate::defs::SimpleMessage::new($kind, $message); |
| 57 | + &MESSAGE_DATA |
| 58 | + }) |
| 59 | + } |
| 60 | + |
| 61 | + pub struct Error { |
| 62 | + repr: Repr, |
| 63 | + } |
| 64 | + |
| 65 | + //#[repr(transparent)] |
| 66 | + pub(super) struct Repr(std::ptr::NonNull<()>); |
| 67 | + |
| 68 | + impl Repr { |
| 69 | + #[inline] |
| 70 | + pub(super) const fn new_simple_message(m: &'static SimpleMessage) -> Self { |
| 71 | + // Safety: References are never null. |
| 72 | + Self(unsafe { NonNull::new_unchecked(m as *const _ as *mut ()) }) |
| 73 | + } |
| 74 | + } |
| 75 | + |
| 76 | + impl Error { |
| 77 | + /// Creates a new I/O error from a known kind of error as well as a constant |
| 78 | + /// message. |
| 79 | + /// |
| 80 | + /// This function does not allocate. |
| 81 | + /// |
| 82 | + /// You should not use this directly, and instead use the `const_io_error!` |
| 83 | + /// macro: `const_io_error!(ErrorKind::Something, "some_message")`. |
| 84 | + /// |
| 85 | + /// This function should maybe change to `from_static_message<const MSG: &'static |
| 86 | + /// str>(kind: ErrorKind)` in the future, when const generics allow that. |
| 87 | + #[inline] |
| 88 | + pub(crate) const fn from_static_message(msg: &'static SimpleMessage) -> Error { |
| 89 | + Self { repr: Repr::new_simple_message(msg) } |
| 90 | + } |
| 91 | + } |
| 92 | + |
| 93 | + //#[repr(align(4))] |
| 94 | + #[derive(Debug)] |
| 95 | + pub(crate) struct SimpleMessage { |
| 96 | + kind: ErrorKind, |
| 97 | + message: &'static str, |
| 98 | + } |
| 99 | + |
| 100 | + impl SimpleMessage { |
| 101 | + pub(crate) const fn new(kind: ErrorKind, message: &'static str) -> Self { |
| 102 | + Self { kind, message } |
| 103 | + } |
| 104 | + } |
| 105 | + |
| 106 | + #[derive(Clone, Copy, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] |
| 107 | + #[allow(deprecated)] |
| 108 | + #[non_exhaustive] |
| 109 | + pub enum ErrorKind { |
| 110 | + NotFound, |
| 111 | + PermissionDenied, |
| 112 | + InvalidInput, |
| 113 | + } |
| 114 | +} |
0 commit comments