Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391use std::{collections::HashMap, fmt::Display};
use rustc_span::Span;use vir::ast::VirErr;
pub(crate) fn err_span<A, S: Into<String>>(span: Span, msg: S) -> Result<A, VirErr> { Err(vir::messages::error(&crate::spans::err_air_span(span), msg))}
pub(crate) fn err_span_vec<A, S: Into<String>>(span: Span, msg: S) -> Result<A, Vec<VirErr>> { Err(vec![vir::messages::error(&crate::spans::err_air_span(span), msg)])}
pub(crate) fn err_span_bare<S: Into<String>>(span: Span, msg: S) -> VirErr { vir::messages::error(&crate::spans::err_air_span(span), msg)}
pub(crate) fn vir_err_span_str(span: Span, msg: &str) -> VirErr { vir_err_span_string(span, msg.to_string())}
pub(crate) fn vir_err_span_string(span: Span, msg: String) -> VirErr { vir::messages::error(&crate::spans::err_air_span(span), msg)}
pub(crate) fn unsupported_err_span<A>(span: Span, msg: String) -> Result<A, VirErr> { err_span(span, format!("Verus does not currently support {}", msg))}
pub(crate) fn internal_err_span<A>(span: Span, msg: String) -> Result<A, VirErr> { vir::util::internal_err_span(crate::spans::err_air_span(span), msg)}
#[macro_export]macro_rules! unsupported_err { ($span: expr, $msg: expr) => {{ $crate::util::unsupported_err_span($span, $msg.to_string())?; unreachable!() }}; ($span: expr, $msg: expr, $info: expr) => {{ dbg!($info); $crate::util::unsupported_err_span($span, $msg.to_string())?; unreachable!() }};}
#[macro_export]macro_rules! unsupported_err_vec { ($span: expr, $msg: expr) => {{ $crate::util::unsupported_err_span($span, $msg.to_string()).map_err(|e| vec![e])?; unreachable!() }}; ($span: expr, $msg: expr, $info: expr) => {{ dbg!($info); $crate::util::unsupported_err_span($span, $msg.to_string()).map_err(|e| vec![e])?; unreachable!() }};}
#[macro_export]macro_rules! internal_err { ($span: expr, $msg: expr) => {{ $crate::util::internal_err_span($span, $msg.to_string())?; unreachable!() }}; ($span: expr, $msg: expr, $info: expr) => {{ dbg!($info); $crate::util::internal_err_span($span, $msg.to_string())?; unreachable!() }};}
#[macro_export]macro_rules! internal_err_unless { ($assertion: expr, $span: expr, $msg: expr) => { if (!$assertion) { $crate::util::internal_err_span($span, $msg.to_string())?; } }; ($assertion: expr, $span: expr, $msg: expr, $info: expr) => { if (!$assertion) { dbg!($info); $crate::util::internal_err_span($span, $msg.to_string())?; } };}
#[macro_export]macro_rules! unsupported_err_unless { ($assertion: expr, $span: expr, $msg: expr) => { if (!$assertion) { $crate::util::unsupported_err_span($span, $msg.to_string())?; } }; ($assertion: expr, $span: expr, $msg: expr, $info: expr) => { if (!$assertion) { dbg!($info); $crate::util::unsupported_err_span($span, $msg.to_string())?; } };}
#[macro_export]macro_rules! unsupported_err_vec_unless { ($assertion: expr, $span: expr, $msg: expr) => { if (!$assertion) { $crate::util::unsupported_err_span($span, $msg.to_string()).map_err(|e| vec![e])?; } }; ($assertion: expr, $span: expr, $msg: expr, $info: expr) => { if (!$assertion) { dbg!($info); $crate::util::unsupported_err_span($span, $msg.to_string()).map_err(|e| vec![e])?; } };}
#[macro_export]macro_rules! err_unless { ($assertion: expr, $span: expr, $msg: expr) => { if (!$assertion) { $crate::util::err_span($span, $msg)?; } }; ($assertion: expr, $span: expr, $msg: expr, $info: expr) => { if (!$assertion) { dbg!($info); $crate::util::err_span($span, $msg)?; } };}
/// Basic error, with just a messagepub fn error<S: Into<String>>(msg: S) -> VirErr { vir::messages::error_bare(msg)}
#[allow(dead_code)]pub(crate) fn vec_map<A, B, F: FnMut(&A) -> B>(v: &Vec<A>, f: F) -> Vec<B> { v.iter().map(f).collect()}
#[allow(dead_code)]pub(crate) fn vec_map_result<A, B, E, F>(v: &Vec<A>, f: F) -> Result<Vec<B>, E>where F: Fn(&A) -> Result<B, E>,{ v.iter().map(f).collect()}
#[allow(dead_code)]pub(crate) fn slice_vec_map_result<A, B, E, F: Fn(&A) -> Result<B, E>>( slice: &[A], f: F,) -> Result<Vec<B>, E> { slice.iter().map(f).collect()}
pub enum VerusBuildProfile { Debug, Release, Unknown,}
impl std::fmt::Display for VerusBuildProfile { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let s = match self { VerusBuildProfile::Debug => "debug", VerusBuildProfile::Release => "release", VerusBuildProfile::Unknown => "unknown", }; f.write_str(s) }}
const fn verus_build_profile() -> VerusBuildProfile { let profile = option_env!("VARGO_BUILD_PROFILE"); match profile { Some(p) => { if const_str_equal(p, "release") { VerusBuildProfile::Release } else if const_str_equal(p, "debug") { VerusBuildProfile::Debug } else { panic!("unexpected VARGO_BUILD_PROFILE"); } } None => VerusBuildProfile::Unknown, }}
pub struct VerusBuildInfo { pub profile: VerusBuildProfile, pub version: &'static str, pub platform_os: &'static str, pub platform_arch: &'static str, pub toolchain: &'static str, pub sha: &'static str,}
const VARGO_TOOLCHAIN: Option<&'static str> = option_env!("VARGO_TOOLCHAIN");
pub const fn verus_build_info() -> VerusBuildInfo { let profile = verus_build_profile(); let version = match option_env!("VARGO_BUILD_VERSION") { Some(v) => v, None => "Unknown", }; let platform_os = std::env::consts::OS; let platform_arch = std::env::consts::ARCH; let toolchain = match VARGO_TOOLCHAIN { Some(toolchain) => toolchain, None => "unkown", }; let sha = match option_env!("VARGO_BUILD_SHA") { Some(v) => v, None => "Unknown", }; VerusBuildInfo { profile, version, platform_os, platform_arch, toolchain, sha }}
impl Display for VerusBuildInfo { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { writeln!(f, "Verus")?; writeln!(f, " Version: {}", self.version)?; writeln!(f, " Profile: {}", self.profile)?; writeln!(f, " Platform: {}_{}", self.platform_os, self.platform_arch)?; writeln!(f, " Toolchain: {}", self.toolchain)?; Ok(()) }}
impl VerusBuildInfo { pub fn to_json(&self) -> serde_json::Value { serde_json::json!({ "verus": { "profile": self.profile.to_string(), "version": self.version.to_string(), "platform": { "os": self.platform_os.to_string(), "arch": self.platform_arch.to_string(), }, "toolchain": self.toolchain.to_string(), "commit": self.sha, } }) }}
// ==================================================================================================// this function was copied from https://github.com/Nugine/const-str/blob/main/const-str/src/bytes.rs// const-str is MIT licensedpub const fn const_str_equal(lhs: &str, rhs: &str) -> bool { let lhs = lhs.as_bytes(); let rhs = rhs.as_bytes(); if lhs.len() != rhs.len() { return false; } let mut i = 0; while i < lhs.len() { if lhs[i] != rhs[i] { return false; } i += 1; } true}// ==================================================================================================
// this is unfortunate, but when processing a reveal we cannot get the type of the// corresponding node in HIR because the body of the reveal closure cannot be// successfully typechecked, and I did not find a public interface to this in rustc// NOTE: do not use this if you have a body context with `types` or can otherwise obtain TypeckResultspub fn hir_prim_ty_to_mir_ty<'tcx>( tcx: rustc_middle::ty::TyCtxt<'tcx>, prim_ty: &rustc_hir::PrimTy,) -> rustc_middle::ty::Ty<'tcx> { match prim_ty { rustc_hir::PrimTy::Int(int_ty) => match int_ty { rustc_ast::IntTy::Isize => tcx.types.isize, rustc_ast::IntTy::I8 => tcx.types.i8, rustc_ast::IntTy::I16 => tcx.types.i16, rustc_ast::IntTy::I32 => tcx.types.i32, rustc_ast::IntTy::I64 => tcx.types.i64, rustc_ast::IntTy::I128 => tcx.types.i128, }, rustc_hir::PrimTy::Uint(uint_ty) => match uint_ty { rustc_ast::UintTy::Usize => tcx.types.usize, rustc_ast::UintTy::U8 => tcx.types.u8, rustc_ast::UintTy::U16 => tcx.types.u16, rustc_ast::UintTy::U32 => tcx.types.u32, rustc_ast::UintTy::U64 => tcx.types.u64, rustc_ast::UintTy::U128 => tcx.types.u128, }, rustc_hir::PrimTy::Float(float_ty) => match float_ty { rustc_ast::FloatTy::F16 => tcx.types.f16, rustc_ast::FloatTy::F32 => tcx.types.f32, rustc_ast::FloatTy::F64 => tcx.types.f64, rustc_ast::FloatTy::F128 => tcx.types.f128, }, rustc_hir::PrimTy::Str => tcx.types.str_, rustc_hir::PrimTy::Bool => tcx.types.bool, rustc_hir::PrimTy::Char => tcx.types.char, }}
#[allow(unused_macros)]macro_rules! dbg_backtrace { ($val: expr) => { match $val { tmp => { std::eprintln!( "[{}:{}:{}] {} = {:#?}", std::file!(), std::line!(), std::column!(), std::stringify!($val), &tmp ); eprintln!( "[{}:{}:{}]\n{}", std::file!(), std::line!(), std::column!(), std::backtrace::Backtrace::force_capture() ); tmp } } };}
#[allow(unused_imports)]pub(crate) use dbg_backtrace;
#[allow(unused_macros)]macro_rules! backtrace { () => { eprintln!( "[{}:{}:{}]\n{}", std::file!(), std::line!(), std::column!(), std::backtrace::Backtrace::force_capture() ); };}
#[allow(unused_imports)]pub(crate) use backtrace;
pub trait HashMapAbsorbWith<K, V> { fn absorb_with<F>(&mut self, other: HashMap<K, V>, absorb_value: F) where F: Fn(&mut V, V);}
impl<K, V> HashMapAbsorbWith<K, V> for HashMap<K, V>where K: Eq + std::hash::Hash,{ fn absorb_with<F>(&mut self, other: HashMap<K, V>, absorb_value: F) where F: Fn(&mut V, V), { use std::collections::hash_map::Entry; for (key, rhs) in other { match self.entry(key) { Entry::Vacant(vacant_entry) => { vacant_entry.insert(rhs); } Entry::Occupied(mut occupied_entry) => { absorb_value(occupied_entry.get_mut(), rhs); } } } }}
pub(crate) fn no_builtin_err(span: &vir::messages::Span) -> VirErr { vir::messages::error(span, "the `verus_builtin` crate was not imported but it is necessary to run Verus; you likely need to add `use vstd::prelude::*;` at the top of a lib.rs or main.rs file") .help("for getting started with Verus, see: https://verus-lang.github.io/verus/guide/getting_started.html")}
pub(crate) fn iter_crate_free_items<'tcx>( tcx: rustc_middle::ty::TyCtxt<'tcx>,) -> impl Iterator<Item = &'tcx rustc_hir::Item<'tcx>> { tcx.hir_crate_items(()).free_items().map(move |item_id| tcx.hir_item(item_id))}