rust_verify/src/verus_items.rs
Line | Count | Source |
1 | | use air::ast::Ident; |
2 | | use regex::Regex; |
3 | | use rustc_middle::ty::{TyCtxt, TyKind}; |
4 | | use rustc_span::def_id::DefId; |
5 | | use std::{collections::HashMap, sync::Arc}; |
6 | | |
7 | | // The names returned by this are intended exclusively for matching in `get_rust_item` |
8 | 496k | fn ty_to_stable_string_partial<'tcx>( |
9 | 496k | tcx: TyCtxt<'tcx>, |
10 | 496k | ty: &rustc_middle::ty::Ty<'_>, |
11 | 496k | ) -> Option<String> { |
12 | 496k | Some(match ty.kind() { |
13 | 27 | TyKind::Bool => format!("bool"), |
14 | 2 | TyKind::Char => format!("char"), |
15 | 11.5k | TyKind::Int(t) => format!("{}", t.name_str()), |
16 | 15.0k | TyKind::Uint(t) => format!("{}", t.name_str()), |
17 | 0 | TyKind::Float(t) => format!("{}", t.name_str()), |
18 | 435 | TyKind::RawPtr(ty, tm) => format!( |
19 | | "*{} {}", |
20 | 435 | match tm { |
21 | 321 | rustc_ast::Mutability::Mut => "mut", |
22 | 114 | rustc_ast::Mutability::Not => "const", |
23 | | }, |
24 | 435 | ty_to_stable_string_partial(tcx, ty)?, |
25 | | ), |
26 | 0 | TyKind::Ref(_r, ty, mutbl) => format!( |
27 | | "&{} {}", |
28 | 0 | match mutbl { |
29 | 0 | rustc_ast::Mutability::Mut => "mut", |
30 | 0 | rustc_ast::Mutability::Not => "const", |
31 | | }, |
32 | 0 | ty_to_stable_string_partial(tcx, ty)?, |
33 | | ), |
34 | 0 | TyKind::Never => format!("!"), |
35 | 0 | TyKind::Tuple(tys) => format!( |
36 | | "({})", |
37 | 0 | tys.iter() |
38 | 0 | .map(|ty| ty_to_stable_string_partial(tcx, &ty)) |
39 | 0 | .collect::<Option<Vec<_>>>()? |
40 | 0 | .join(",") |
41 | | ), |
42 | 1.41k | TyKind::Param(param_ty) => format!("{}", param_ty.name.as_str()), |
43 | 464k | TyKind::Adt(def, _substs) => { |
44 | 464k | return Some(def_id_to_stable_rust_path(tcx, def.did())?); |
45 | | } |
46 | 375 | TyKind::Str => format!("str"), |
47 | 28 | TyKind::Array(ty, sz) => { |
48 | 28 | format!("[{}; {}]", ty_to_stable_string_partial(tcx, &ty)?, sz) |
49 | | } |
50 | 956 | TyKind::Slice(ty) => format!("[{}]", ty_to_stable_string_partial(tcx, &ty)?), |
51 | 1.64k | _ => return None, |
52 | | }) |
53 | 496k | } |
54 | | |
55 | | /// NOTE: do not use this to determine if something is a well known / rust lang item |
56 | | /// use verus_items::get_rust_item instead |
57 | 5.11M | pub(crate) fn def_id_to_stable_rust_path<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option<String> { |
58 | 5.11M | let def_path = tcx.def_path(def_id); |
59 | 5.11M | let mut segments: Vec<String> = Vec::with_capacity(def_path.data.len()); |
60 | 5.11M | let crate_name = tcx.crate_name(def_path.krate); |
61 | 5.11M | segments.push(crate_name.to_ident_string()); |
62 | 5.11M | let mut one_impl_block_in_path = false; |
63 | 11.5M | for d in def_path.data.iter() { |
64 | | use rustc_hir::definitions::DefPathData; |
65 | 11.5M | match &d.data { |
66 | 9.06M | DefPathData::ValueNs(symbol) | DefPathData::TypeNs(symbol) => { |
67 | 11.0M | segments.push(symbol.to_string()) |
68 | | } |
69 | 0 | DefPathData::Ctor => segments.push(vir::def::RUST_DEF_CTOR.to_string()), |
70 | | DefPathData::Impl => { |
71 | 494k | if one_impl_block_in_path { |
72 | 0 | return None; |
73 | 494k | } |
74 | 494k | one_impl_block_in_path = true; |
75 | 494k | let self_ty = tcx.type_of(tcx.parent(def_id)).skip_binder(); |
76 | 494k | let path = ty_to_stable_string_partial(tcx, &self_ty)?; |
77 | 493k | segments.clear(); |
78 | 493k | segments.push(path); |
79 | | } |
80 | 1 | DefPathData::ForeignMod => { |
81 | 1 | // this segment can be ignored |
82 | 1 | } |
83 | 0 | _ => return None, |
84 | | } |
85 | | } |
86 | 5.11M | Some(segments.join("::")) |
87 | 5.11M | } |
88 | | |
89 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
90 | | pub(crate) enum SpecItem { |
91 | | Admit, |
92 | | Assume, |
93 | | NoMethodBody, |
94 | | Requires, |
95 | | Recommends, |
96 | | Ensures, |
97 | | Returns, |
98 | | InvariantExceptBreak, |
99 | | Invariant, |
100 | | AtomicSpec, |
101 | | AtomicCallLoop, |
102 | | Decreases, |
103 | | DecreasesWhen, |
104 | | DecreasesBy, |
105 | | RecommendsBy, |
106 | | OpensInvariantMask, |
107 | | InvMaskNone, |
108 | | InvMaskAny, |
109 | | InvMaskList, |
110 | | InvMaskListCompl, |
111 | | InvMaskSet, |
112 | | Atomically, |
113 | | NoUnwind, |
114 | | NoUnwindWhen, |
115 | | } |
116 | | |
117 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
118 | | pub(crate) enum QuantItem { |
119 | | Forall, |
120 | | Exists, |
121 | | } |
122 | | |
123 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
124 | | pub(crate) enum DirectiveItem { |
125 | | ExtraDependency, |
126 | | RevealHide, |
127 | | RevealHideInternalPath, |
128 | | RevealStrlit, |
129 | | InlineAirStmt, |
130 | | } |
131 | | |
132 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
133 | | pub(crate) enum ExprItem { |
134 | | Choose, |
135 | | ChooseTuple, |
136 | | Old, |
137 | | GetVariantField, |
138 | | GetUnionField, |
139 | | IsVariant, |
140 | | ArrayIndex, |
141 | | F32ToBits, |
142 | | F64ToBits, |
143 | | StrSliceLen, |
144 | | StrSliceGetChar, |
145 | | ArchWordBits, |
146 | | ClosureToFnSpec, |
147 | | ClosureToFnProof, |
148 | | SignedMin, |
149 | | SignedMax, |
150 | | UnsignedMax, |
151 | | IsSmallerThan, |
152 | | IsSmallerThanLexicographic, |
153 | | IsSmallerThanRecursiveFunctionField, |
154 | | DefaultEnsures, |
155 | | InferSpecForLoopIter, |
156 | | ShrRefStructWrap, |
157 | | } |
158 | | |
159 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
160 | | pub(crate) enum CompilableOprItem { |
161 | | Implies, |
162 | | // SmartPtrNew, |
163 | | GhostExec, |
164 | | GhostNew, |
165 | | TrackedNew, |
166 | | TrackedExec, |
167 | | TrackedExecBorrow, |
168 | | TrackedGet, |
169 | | TrackedBorrow, |
170 | | TrackedBorrowMut, |
171 | | // GhostSplitTuple, |
172 | | // TrackedSplitTuple, |
173 | | } |
174 | | |
175 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
176 | | pub(crate) enum BuiltinDerefItem { |
177 | | TrackedDeref, |
178 | | TrackedDerefMut, |
179 | | GhostDeref, |
180 | | GhostDerefMut, |
181 | | } |
182 | | |
183 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
184 | | pub(crate) enum ArithItem { |
185 | | BuiltinAdd, |
186 | | BuiltinSub, |
187 | | BuiltinMul, |
188 | | } |
189 | | |
190 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
191 | | pub(crate) enum EqualityItem { |
192 | | Equal, |
193 | | SpecEq, |
194 | | ExtEqual, |
195 | | ExtEqualDeep, |
196 | | } |
197 | | |
198 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
199 | | pub(crate) enum SpecOrdItem { |
200 | | Le, |
201 | | Ge, |
202 | | Lt, |
203 | | Gt, |
204 | | } |
205 | | |
206 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
207 | | pub(crate) enum SpecArithItem { |
208 | | Add, |
209 | | Sub, |
210 | | Mul, |
211 | | EuclideanOrRealDiv, |
212 | | EuclideanMod, |
213 | | } |
214 | | |
215 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
216 | | pub(crate) enum SpecBitwiseItem { |
217 | | BitAnd, |
218 | | BitOr, |
219 | | BitXor, |
220 | | Shl, |
221 | | Shr, |
222 | | } |
223 | | |
224 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
225 | | pub(crate) enum IeeeFloatUnaryItem { |
226 | | Cast, |
227 | | Neg, |
228 | | Floor, |
229 | | Ceil, |
230 | | Round, |
231 | | RoundTiesEven, |
232 | | Trunc, |
233 | | IsNormal, |
234 | | IsSubnormal, |
235 | | IsZero, |
236 | | IsInfinite, |
237 | | IsNaN, |
238 | | IsNegative, |
239 | | IsPositive, |
240 | | } |
241 | | |
242 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
243 | | pub(crate) enum IeeeFloatBinaryItem { |
244 | | Add, |
245 | | Sub, |
246 | | Mul, |
247 | | Div, |
248 | | Eq, |
249 | | Le, |
250 | | Ge, |
251 | | Lt, |
252 | | Gt, |
253 | | } |
254 | | |
255 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
256 | | pub(crate) enum BinaryOpItem { |
257 | | Arith(ArithItem), |
258 | | Equality(EqualityItem), |
259 | | SpecOrd(SpecOrdItem), |
260 | | SpecArith(SpecArithItem), |
261 | | SpecBitwise(SpecBitwiseItem), |
262 | | IeeeFloat(IeeeFloatBinaryItem), |
263 | | } |
264 | | |
265 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
266 | | pub(crate) enum ChainedItem { |
267 | | Value, |
268 | | Le, |
269 | | Lt, |
270 | | Ge, |
271 | | Gt, |
272 | | Cmp, |
273 | | Eq, |
274 | | } |
275 | | |
276 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
277 | | pub(crate) enum AssertItem { |
278 | | Assert, |
279 | | AssertBy, |
280 | | AssertByCompute, |
281 | | AssertByComputeOnly, |
282 | | AssertNonlinearBy, |
283 | | AssertBitvectorBy, |
284 | | AssertForallBy, |
285 | | AssertBitVector, |
286 | | } |
287 | | |
288 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
289 | | pub(crate) enum SpecLiteralItem { |
290 | | Integer, |
291 | | Int, |
292 | | Nat, |
293 | | Decimal, |
294 | | } |
295 | | |
296 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
297 | | pub(crate) enum SpecGhostTrackedItem { |
298 | | GhostView, |
299 | | GhostBorrow, |
300 | | GhostBorrowMut, |
301 | | TrackedView, |
302 | | } |
303 | | |
304 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
305 | | pub(crate) enum UnaryOpItem { |
306 | | SpecLiteral(SpecLiteralItem), |
307 | | SpecNeg, |
308 | | SpecCastInteger, |
309 | | SpecCastReal, |
310 | | SpecCastFloat, |
311 | | RealFloor, |
312 | | SpecGhostTracked(SpecGhostTrackedItem), |
313 | | IeeeFloat(IeeeFloatUnaryItem), |
314 | | } |
315 | | |
316 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
317 | | pub(crate) enum OpenInvariantBlockItem { |
318 | | OpenLocalInvariantBegin, |
319 | | OpenAtomicInvariantBegin, |
320 | | OpenInvariantEnd, |
321 | | } |
322 | | |
323 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
324 | | pub(crate) enum OpenAtomicUpdateItem { |
325 | | TryOpenAtomicUpdateBegin, |
326 | | TryOpenAtomicUpdateEnd, |
327 | | } |
328 | | |
329 | | #[derive(PartialEq, Eq, Debug, Clone, Hash)] |
330 | | pub(crate) enum InvariantItem { |
331 | | AtomicInvariantNamespace, |
332 | | AtomicInvariantInv, |
333 | | LocalInvariantNamespace, |
334 | | LocalInvariantInv, |
335 | | CreateOpenInvariantCredit, |
336 | | SpendOpenInvariantCredit, |
337 | | SpendOpenInvariantCreditInProof, |
338 | | } |
339 | | |
340 | | #[derive(PartialEq, Eq, Debug, Clone, Hash)] |
341 | | pub(crate) enum AtomicUpdateItem { |
342 | | AtomicUpdateReq, |
343 | | AtomicUpdateEns, |
344 | | AtomicUpdatePred, |
345 | | AtomicUpdateResolves, |
346 | | AtomicUpdateInput, |
347 | | AtomicUpdateOutput, |
348 | | AtomicUpdateOuterMask, |
349 | | AtomicUpdateInnerMask, |
350 | | } |
351 | | |
352 | | #[derive(PartialEq, Eq, Debug, Clone, Hash)] |
353 | | pub(crate) enum SetItem { |
354 | | Type, |
355 | | Empty, |
356 | | Full, |
357 | | Contains, |
358 | | SubsetOf, |
359 | | Insert, |
360 | | Remove, |
361 | | } |
362 | | |
363 | | #[derive(PartialEq, Eq, Debug, Clone, Hash)] |
364 | | pub(crate) enum VstdItem { |
365 | | SeqFn(vir::interpreter::SeqFn), |
366 | | SetItem(SetItem), |
367 | | ISetItem(SetItem), |
368 | | Invariant(InvariantItem), |
369 | | AtomicUpdate(AtomicUpdateItem), |
370 | | PredArgs, |
371 | | BranchBool, |
372 | | ExecNonstaticCall, |
373 | | ProofNonstaticCall, |
374 | | ArrayIndexGet, |
375 | | ArrayAsSlice, |
376 | | ArrayFillForCopyTypes, |
377 | | SpecArrayUpdate, |
378 | | SliceIndexGet, |
379 | | SpecSliceUpdate, |
380 | | SpecSliceLen, |
381 | | SpecSliceIndex, |
382 | | CastPtrToThinPtr, |
383 | | CastArrayPtrToSlicePtr, |
384 | | CastSlicePtrToSlicePtr, |
385 | | CastSlicePtrToStrPtr, |
386 | | CastStrPtrToSlicePtr, |
387 | | CastPtrToUsize, |
388 | | FloatCast, |
389 | | RefMutArrayUnsizingCoercion, |
390 | | VecIndex, |
391 | | VecIndexMut, |
392 | | SharedReference, |
393 | | } |
394 | | |
395 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
396 | | pub(crate) enum MarkerItem { |
397 | | Structural, |
398 | | } |
399 | | |
400 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
401 | | pub(crate) enum BuiltinTypeItem { |
402 | | Int, |
403 | | Nat, |
404 | | Real, |
405 | | FnSpec, |
406 | | Ghost, |
407 | | Tracked, |
408 | | } |
409 | | |
410 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
411 | | pub(crate) enum BuiltinTraitItem { |
412 | | Integer, |
413 | | Chainable, |
414 | | Sealed, |
415 | | } |
416 | | |
417 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
418 | | pub(crate) enum BuiltinFunctionItem { |
419 | | CallRequires, |
420 | | CallEnsures, |
421 | | ConstrainType, |
422 | | GetFutureOutputType, |
423 | | } |
424 | | |
425 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
426 | | pub(crate) enum GlobalItem { |
427 | | SizeOf, |
428 | | } |
429 | | |
430 | | #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] |
431 | | #[allow(non_camel_case_types)] |
432 | | pub(crate) enum ExternalItem { |
433 | | FnProof, |
434 | | FOpts, |
435 | | FnProofReq, |
436 | | FnProofEns, |
437 | | ProofFnOnce, |
438 | | ProofFnMut, |
439 | | ProofFn, |
440 | | Trk, |
441 | | RqEn, |
442 | | } |
443 | | |
444 | | #[derive(PartialEq, Eq, Debug, Clone, Hash)] |
445 | | pub(crate) enum VerusItem { |
446 | | Spec(SpecItem), |
447 | | Quant(QuantItem), |
448 | | Directive(DirectiveItem), |
449 | | Expr(ExprItem), |
450 | | CompilableOpr(CompilableOprItem), |
451 | | BinaryOp(BinaryOpItem), |
452 | | UnaryOp(UnaryOpItem), |
453 | | Chained(ChainedItem), |
454 | | Assert(AssertItem), |
455 | | UseTypeInvariant, |
456 | | WithTriggers, |
457 | | OpenInvariantBlock(OpenInvariantBlockItem), |
458 | | OpenAtomicUpdate(OpenAtomicUpdateItem), |
459 | | Vstd(VstdItem, Option<Ident>), |
460 | | Marker(MarkerItem), |
461 | | BuiltinType(BuiltinTypeItem), |
462 | | BuiltinTrait(BuiltinTraitItem), |
463 | | BuiltinFunction(BuiltinFunctionItem), |
464 | | BuiltinDeref(BuiltinDerefItem), |
465 | | Global(GlobalItem), |
466 | | External(ExternalItem), |
467 | | HasResolved, |
468 | | HasResolvedUnsized, |
469 | | MutRefCurrent, |
470 | | MutRefFuture, |
471 | | Final, |
472 | | AfterBorrow, |
473 | | ErasedGhostValue, |
474 | | ShadowGhostValue, |
475 | | MutableReferenceTie, |
476 | | TwoPhaseMutableReferenceTie, |
477 | | GetFirst, |
478 | | DummyCapture(DummyCaptureItem), |
479 | | MutRefTracked, |
480 | | } |
481 | | |
482 | | #[derive(PartialEq, Eq, Debug, Clone, Hash)] |
483 | | pub(crate) enum DummyCaptureItem { |
484 | | Struct, |
485 | | New, |
486 | | Consume, |
487 | | } |
488 | | |
489 | | #[rustfmt::skip] |
490 | 4.25k | fn verus_items_map() -> Vec<(&'static str, VerusItem)> { |
491 | 4.25k | vec![ |
492 | 4.25k | ("verus::verus_builtin::admit", VerusItem::Spec(SpecItem::Admit)), |
493 | 4.25k | ("verus::verus_builtin::assume_", VerusItem::Spec(SpecItem::Assume)), |
494 | 4.25k | ("verus::verus_builtin::no_method_body", VerusItem::Spec(SpecItem::NoMethodBody)), |
495 | 4.25k | ("verus::verus_builtin::requires", VerusItem::Spec(SpecItem::Requires)), |
496 | 4.25k | ("verus::verus_builtin::recommends", VerusItem::Spec(SpecItem::Recommends)), |
497 | 4.25k | ("verus::verus_builtin::ensures", VerusItem::Spec(SpecItem::Ensures)), |
498 | 4.25k | ("verus::verus_builtin::returns", VerusItem::Spec(SpecItem::Returns)), |
499 | 4.25k | ("verus::verus_builtin::invariant_except_break", VerusItem::Spec(SpecItem::InvariantExceptBreak)), |
500 | 4.25k | ("verus::verus_builtin::invariant", VerusItem::Spec(SpecItem::Invariant)), |
501 | 4.25k | ("verus::verus_builtin::atomic_spec", VerusItem::Spec(SpecItem::AtomicSpec)), |
502 | 4.25k | ("verus::verus_builtin::atomic_call_loop", VerusItem::Spec(SpecItem::AtomicCallLoop)), |
503 | 4.25k | ("verus::verus_builtin::decreases", VerusItem::Spec(SpecItem::Decreases)), |
504 | 4.25k | ("verus::verus_builtin::decreases_when", VerusItem::Spec(SpecItem::DecreasesWhen)), |
505 | 4.25k | ("verus::verus_builtin::decreases_by", VerusItem::Spec(SpecItem::DecreasesBy)), |
506 | 4.25k | ("verus::verus_builtin::recommends_by", VerusItem::Spec(SpecItem::RecommendsBy)), |
507 | | |
508 | 4.25k | ("verus::verus_builtin::opens_invariant_mask", VerusItem::Spec(SpecItem::OpensInvariantMask)), |
509 | | |
510 | 4.25k | ("verus::verus_builtin::inv_mask_none", VerusItem::Spec(SpecItem::InvMaskNone)), |
511 | 4.25k | ("verus::verus_builtin::inv_mask_any", VerusItem::Spec(SpecItem::InvMaskAny)), |
512 | 4.25k | ("verus::verus_builtin::inv_mask_list", VerusItem::Spec(SpecItem::InvMaskList)), |
513 | 4.25k | ("verus::verus_builtin::inv_mask_list_compl", VerusItem::Spec(SpecItem::InvMaskListCompl)), |
514 | 4.25k | ("verus::verus_builtin::inv_mask_set", VerusItem::Spec(SpecItem::InvMaskSet)), |
515 | | |
516 | 4.25k | ("verus::verus_builtin::no_unwind", VerusItem::Spec(SpecItem::NoUnwind)), |
517 | 4.25k | ("verus::verus_builtin::no_unwind_when", VerusItem::Spec(SpecItem::NoUnwindWhen)), |
518 | | |
519 | 4.25k | ("verus::verus_builtin::forall", VerusItem::Quant(QuantItem::Forall)), |
520 | 4.25k | ("verus::verus_builtin::exists", VerusItem::Quant(QuantItem::Exists)), |
521 | | |
522 | 4.25k | ("verus::verus_builtin::extra_dependency", VerusItem::Directive(DirectiveItem::ExtraDependency)), |
523 | 4.25k | ("verus::verus_builtin::reveal_hide", VerusItem::Directive(DirectiveItem::RevealHide)), |
524 | 4.25k | ("verus::verus_builtin::reveal_hide_internal_path", VerusItem::Directive(DirectiveItem::RevealHideInternalPath)), |
525 | 4.25k | ("verus::verus_builtin::reveal_strlit", VerusItem::Directive(DirectiveItem::RevealStrlit)), |
526 | 4.25k | ("verus::verus_builtin::inline_air_stmt", VerusItem::Directive(DirectiveItem::InlineAirStmt)), |
527 | | |
528 | 4.25k | ("verus::verus_builtin::choose", VerusItem::Expr(ExprItem::Choose)), |
529 | 4.25k | ("verus::verus_builtin::choose_tuple", VerusItem::Expr(ExprItem::ChooseTuple)), |
530 | 4.25k | ("verus::verus_builtin::old", VerusItem::Expr(ExprItem::Old)), |
531 | 4.25k | ("verus::verus_builtin::get_variant_field", VerusItem::Expr(ExprItem::GetVariantField)), |
532 | 4.25k | ("verus::verus_builtin::get_union_field", VerusItem::Expr(ExprItem::GetUnionField)), |
533 | 4.25k | ("verus::verus_builtin::is_variant", VerusItem::Expr(ExprItem::IsVariant)), |
534 | 4.25k | ("verus::verus_builtin::array_index", VerusItem::Expr(ExprItem::ArrayIndex)), |
535 | 4.25k | ("verus::verus_builtin::f32_to_bits", VerusItem::Expr(ExprItem::F32ToBits)), |
536 | 4.25k | ("verus::verus_builtin::f64_to_bits", VerusItem::Expr(ExprItem::F64ToBits)), |
537 | 4.25k | ("verus::verus_builtin::strslice_len", VerusItem::Expr(ExprItem::StrSliceLen)), |
538 | 4.25k | ("verus::verus_builtin::strslice_get_char", VerusItem::Expr(ExprItem::StrSliceGetChar)), |
539 | 4.25k | ("verus::verus_builtin::arch_word_bits", VerusItem::Expr(ExprItem::ArchWordBits)), |
540 | 4.25k | ("verus::verus_builtin::closure_to_fn_spec", VerusItem::Expr(ExprItem::ClosureToFnSpec)), |
541 | 4.25k | ("verus::verus_builtin::closure_to_fn_proof", VerusItem::Expr(ExprItem::ClosureToFnProof)), |
542 | 4.25k | ("verus::verus_builtin::signed_min", VerusItem::Expr(ExprItem::SignedMin)), |
543 | 4.25k | ("verus::verus_builtin::signed_max", VerusItem::Expr(ExprItem::SignedMax)), |
544 | 4.25k | ("verus::verus_builtin::unsigned_max", VerusItem::Expr(ExprItem::UnsignedMax)), |
545 | 4.25k | ("verus::verus_builtin::is_smaller_than", VerusItem::Expr(ExprItem::IsSmallerThan)), |
546 | 4.25k | ("verus::verus_builtin::is_smaller_than_lexicographic", VerusItem::Expr(ExprItem::IsSmallerThanLexicographic)), |
547 | 4.25k | ("verus::verus_builtin::is_smaller_than_recursive_function_field", VerusItem::Expr(ExprItem::IsSmallerThanRecursiveFunctionField)), |
548 | 4.25k | ("verus::verus_builtin::default_ensures", VerusItem::Expr(ExprItem::DefaultEnsures)), |
549 | 4.25k | ("verus::verus_builtin::infer_spec_for_loop_iter", VerusItem::Expr(ExprItem::InferSpecForLoopIter)), |
550 | 4.25k | ("verus::verus_builtin::shr_ref_struct_wrap", VerusItem::Expr(ExprItem::ShrRefStructWrap)), |
551 | | |
552 | 4.25k | ("verus::verus_builtin::imply", VerusItem::CompilableOpr(CompilableOprItem::Implies)), |
553 | | // TODO ("verus::verus_builtin::smartptr_new", VerusItem::CompilableOpr(CompilableOprItem::SmartPtrNew)), |
554 | 4.25k | ("verus::verus_builtin::ghost_exec", VerusItem::CompilableOpr(CompilableOprItem::GhostExec)), |
555 | 4.25k | ("verus::verus_builtin::Ghost::new", VerusItem::CompilableOpr(CompilableOprItem::GhostNew)), |
556 | 4.25k | ("verus::verus_builtin::Tracked::new", VerusItem::CompilableOpr(CompilableOprItem::TrackedNew)), |
557 | 4.25k | ("verus::verus_builtin::tracked_exec", VerusItem::CompilableOpr(CompilableOprItem::TrackedExec)), |
558 | 4.25k | ("verus::verus_builtin::tracked_exec_borrow", VerusItem::CompilableOpr(CompilableOprItem::TrackedExecBorrow)), |
559 | 4.25k | ("verus::verus_builtin::Tracked::get", VerusItem::CompilableOpr(CompilableOprItem::TrackedGet)), |
560 | 4.25k | ("verus::verus_builtin::Tracked::borrow", VerusItem::CompilableOpr(CompilableOprItem::TrackedBorrow)), |
561 | 4.25k | ("verus::verus_builtin::Tracked::borrow_mut", VerusItem::CompilableOpr(CompilableOprItem::TrackedBorrowMut)), |
562 | | |
563 | 4.25k | ("verus::verus_builtin::Tracked::deref", VerusItem::BuiltinDeref(BuiltinDerefItem::TrackedDeref)), |
564 | 4.25k | ("verus::verus_builtin::Tracked::deref_mut", VerusItem::BuiltinDeref(BuiltinDerefItem::TrackedDerefMut)), |
565 | 4.25k | ("verus::verus_builtin::Ghost::deref", VerusItem::BuiltinDeref(BuiltinDerefItem::GhostDeref)), |
566 | 4.25k | ("verus::verus_builtin::Ghost::deref_mut", VerusItem::BuiltinDeref(BuiltinDerefItem::GhostDerefMut)), |
567 | | |
568 | 4.25k | ("verus::verus_builtin::add", VerusItem::BinaryOp(BinaryOpItem::Arith(ArithItem::BuiltinAdd))), |
569 | 4.25k | ("verus::verus_builtin::sub", VerusItem::BinaryOp(BinaryOpItem::Arith(ArithItem::BuiltinSub))), |
570 | 4.25k | ("verus::verus_builtin::mul", VerusItem::BinaryOp(BinaryOpItem::Arith(ArithItem::BuiltinMul))), |
571 | | |
572 | 4.25k | ("verus::verus_builtin::equal", VerusItem::BinaryOp(BinaryOpItem::Equality(EqualityItem::Equal))), |
573 | 4.25k | ("verus::verus_builtin::spec_eq", VerusItem::BinaryOp(BinaryOpItem::Equality(EqualityItem::SpecEq))), |
574 | 4.25k | ("verus::verus_builtin::ext_equal", VerusItem::BinaryOp(BinaryOpItem::Equality(EqualityItem::ExtEqual))), |
575 | 4.25k | ("verus::verus_builtin::ext_equal_deep", VerusItem::BinaryOp(BinaryOpItem::Equality(EqualityItem::ExtEqualDeep))), |
576 | | |
577 | 4.25k | ("verus::verus_builtin::SpecOrd::spec_le", VerusItem::BinaryOp(BinaryOpItem::SpecOrd(SpecOrdItem::Le))), |
578 | 4.25k | ("verus::verus_builtin::SpecOrd::spec_ge", VerusItem::BinaryOp(BinaryOpItem::SpecOrd(SpecOrdItem::Ge))), |
579 | 4.25k | ("verus::verus_builtin::SpecOrd::spec_lt", VerusItem::BinaryOp(BinaryOpItem::SpecOrd(SpecOrdItem::Lt))), |
580 | 4.25k | ("verus::verus_builtin::SpecOrd::spec_gt", VerusItem::BinaryOp(BinaryOpItem::SpecOrd(SpecOrdItem::Gt))), |
581 | | |
582 | 4.25k | ("verus::verus_builtin::SpecAdd::spec_add", VerusItem::BinaryOp(BinaryOpItem::SpecArith(SpecArithItem::Add))), |
583 | 4.25k | ("verus::verus_builtin::SpecSub::spec_sub", VerusItem::BinaryOp(BinaryOpItem::SpecArith(SpecArithItem::Sub))), |
584 | 4.25k | ("verus::verus_builtin::SpecMul::spec_mul", VerusItem::BinaryOp(BinaryOpItem::SpecArith(SpecArithItem::Mul))), |
585 | 4.25k | ("verus::verus_builtin::SpecEuclideanOrRealDiv::spec_euclidean_or_real_div", VerusItem::BinaryOp(BinaryOpItem::SpecArith(SpecArithItem::EuclideanOrRealDiv))), |
586 | 4.25k | ("verus::verus_builtin::SpecEuclideanMod::spec_euclidean_mod", VerusItem::BinaryOp(BinaryOpItem::SpecArith(SpecArithItem::EuclideanMod))), |
587 | | |
588 | 4.25k | ("verus::verus_builtin::SpecBitAnd::spec_bitand", VerusItem::BinaryOp(BinaryOpItem::SpecBitwise(SpecBitwiseItem::BitAnd))), |
589 | 4.25k | ("verus::verus_builtin::SpecBitOr::spec_bitor", VerusItem::BinaryOp(BinaryOpItem::SpecBitwise(SpecBitwiseItem::BitOr))), |
590 | 4.25k | ("verus::verus_builtin::SpecBitXor::spec_bitxor", VerusItem::BinaryOp(BinaryOpItem::SpecBitwise(SpecBitwiseItem::BitXor))), |
591 | 4.25k | ("verus::verus_builtin::SpecShl::spec_shl", VerusItem::BinaryOp(BinaryOpItem::SpecBitwise(SpecBitwiseItem::Shl))), |
592 | 4.25k | ("verus::verus_builtin::SpecShr::spec_shr", VerusItem::BinaryOp(BinaryOpItem::SpecBitwise(SpecBitwiseItem::Shr))), |
593 | | |
594 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_add", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Add))), |
595 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_sub", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Sub))), |
596 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_mul", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Mul))), |
597 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_div", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Div))), |
598 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_eq", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Eq))), |
599 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_le", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Le))), |
600 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_ge", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Ge))), |
601 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_lt", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Lt))), |
602 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_gt", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Gt))), |
603 | | |
604 | 4.25k | ("verus::verus_builtin::spec_chained_value", VerusItem::Chained(ChainedItem::Value)), |
605 | 4.25k | ("verus::verus_builtin::spec_chained_le", VerusItem::Chained(ChainedItem::Le)), |
606 | 4.25k | ("verus::verus_builtin::spec_chained_lt", VerusItem::Chained(ChainedItem::Lt)), |
607 | 4.25k | ("verus::verus_builtin::spec_chained_ge", VerusItem::Chained(ChainedItem::Ge)), |
608 | 4.25k | ("verus::verus_builtin::spec_chained_gt", VerusItem::Chained(ChainedItem::Gt)), |
609 | 4.25k | ("verus::verus_builtin::spec_chained_cmp", VerusItem::Chained(ChainedItem::Cmp)), |
610 | 4.25k | ("verus::verus_builtin::spec_chained_eq", VerusItem::Chained(ChainedItem::Eq)), |
611 | | |
612 | 4.25k | ("verus::verus_builtin::assert_", VerusItem::Assert(AssertItem::Assert)), |
613 | 4.25k | ("verus::verus_builtin::assert_by", VerusItem::Assert(AssertItem::AssertBy)), |
614 | 4.25k | ("verus::verus_builtin::assert_by_compute", VerusItem::Assert(AssertItem::AssertByCompute)), |
615 | 4.25k | ("verus::verus_builtin::assert_by_compute_only", VerusItem::Assert(AssertItem::AssertByComputeOnly)), |
616 | 4.25k | ("verus::verus_builtin::assert_nonlinear_by", VerusItem::Assert(AssertItem::AssertNonlinearBy)), |
617 | 4.25k | ("verus::verus_builtin::assert_bitvector_by", VerusItem::Assert(AssertItem::AssertBitvectorBy)), |
618 | 4.25k | ("verus::verus_builtin::assert_forall_by", VerusItem::Assert(AssertItem::AssertForallBy)), |
619 | 4.25k | ("verus::verus_builtin::assert_bit_vector", VerusItem::Assert(AssertItem::AssertBitVector)), |
620 | 4.25k | ("verus::verus_builtin::use_type_invariant", VerusItem::UseTypeInvariant), |
621 | | |
622 | 4.25k | ("verus::verus_builtin::with_triggers", VerusItem::WithTriggers), |
623 | | |
624 | 4.25k | ("verus::verus_builtin::spec_literal_integer", VerusItem::UnaryOp(UnaryOpItem::SpecLiteral(SpecLiteralItem::Integer))), |
625 | 4.25k | ("verus::verus_builtin::spec_literal_int", VerusItem::UnaryOp(UnaryOpItem::SpecLiteral(SpecLiteralItem::Int))), |
626 | 4.25k | ("verus::verus_builtin::spec_literal_nat", VerusItem::UnaryOp(UnaryOpItem::SpecLiteral(SpecLiteralItem::Nat))), |
627 | 4.25k | ("verus::verus_builtin::spec_literal_decimal", VerusItem::UnaryOp(UnaryOpItem::SpecLiteral(SpecLiteralItem::Decimal))), |
628 | 4.25k | ("verus::verus_builtin::SpecNeg::spec_neg", VerusItem::UnaryOp(UnaryOpItem::SpecNeg)), |
629 | 4.25k | ("verus::verus_builtin::spec_cast_integer", VerusItem::UnaryOp(UnaryOpItem::SpecCastInteger)), |
630 | 4.25k | ("verus::verus_builtin::spec_cast_real", VerusItem::UnaryOp(UnaryOpItem::SpecCastReal)), |
631 | 4.25k | ("verus::verus_builtin::spec_cast_float", VerusItem::UnaryOp(UnaryOpItem::SpecCastFloat)), |
632 | 4.25k | ("verus::verus_builtin::real::floor", VerusItem::UnaryOp(UnaryOpItem::RealFloor)), |
633 | 4.25k | ("verus::verus_builtin::Ghost::view", VerusItem::UnaryOp(UnaryOpItem::SpecGhostTracked(SpecGhostTrackedItem::GhostView))), |
634 | 4.25k | ("verus::verus_builtin::Ghost::borrow", VerusItem::UnaryOp(UnaryOpItem::SpecGhostTracked(SpecGhostTrackedItem::GhostBorrow))), |
635 | 4.25k | ("verus::verus_builtin::Ghost::borrow_mut", VerusItem::UnaryOp(UnaryOpItem::SpecGhostTracked(SpecGhostTrackedItem::GhostBorrowMut))), |
636 | 4.25k | ("verus::verus_builtin::Tracked::view", VerusItem::UnaryOp(UnaryOpItem::SpecGhostTracked(SpecGhostTrackedItem::TrackedView))), |
637 | | |
638 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_neg", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Neg))), |
639 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_floor", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Floor))), |
640 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_ceil", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Ceil))), |
641 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_round", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Round))), |
642 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_round_ties_even", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::RoundTiesEven))), |
643 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_trunc", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Trunc))), |
644 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_is_normal", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsNormal))), |
645 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_is_subnormal", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsSubnormal))), |
646 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_is_zero", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsZero))), |
647 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_is_infinite", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsInfinite))), |
648 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_is_nan", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsNaN))), |
649 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_is_negative", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsNegative))), |
650 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_is_positive", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsPositive))), |
651 | 4.25k | ("verus::verus_builtin::IeeeFloat::ieee_is_positive", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsPositive))), |
652 | 4.25k | ("verus::verus_builtin::IeeeFloatCast::ieee_cast", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Cast))), |
653 | | |
654 | 4.25k | ("verus::verus_builtin::erased_ghost_value", VerusItem::ErasedGhostValue), |
655 | 4.25k | ("verus::verus_builtin::shadow_ghost_value", VerusItem::ShadowGhostValue), |
656 | 4.25k | ("verus::verus_builtin::mutable_reference_tie", VerusItem::MutableReferenceTie), |
657 | 4.25k | ("verus::verus_builtin::two_phase_mutable_reference_tie", VerusItem::TwoPhaseMutableReferenceTie), |
658 | 4.25k | ("verus::verus_builtin::verus_erasure_get_first", VerusItem::GetFirst), |
659 | 4.25k | ("verus::verus_builtin::DummyCapture", VerusItem::DummyCapture(DummyCaptureItem::Struct)), |
660 | 4.25k | ("verus::verus_builtin::dummy_capture_new", VerusItem::DummyCapture(DummyCaptureItem::New)), |
661 | 4.25k | ("verus::verus_builtin::dummy_capture_consume", VerusItem::DummyCapture(DummyCaptureItem::Consume)), |
662 | | |
663 | 4.25k | ("verus::vstd::invariant::open_atomic_invariant_begin", VerusItem::OpenInvariantBlock(OpenInvariantBlockItem::OpenAtomicInvariantBegin)), |
664 | 4.25k | ("verus::vstd::invariant::open_local_invariant_begin", VerusItem::OpenInvariantBlock(OpenInvariantBlockItem::OpenLocalInvariantBegin)), |
665 | 4.25k | ("verus::vstd::invariant::open_invariant_end", VerusItem::OpenInvariantBlock(OpenInvariantBlockItem::OpenInvariantEnd)), |
666 | | |
667 | 4.25k | ("verus::vstd::atomic::try_open_atomic_update_begin", VerusItem::OpenAtomicUpdate(OpenAtomicUpdateItem::TryOpenAtomicUpdateBegin)), |
668 | 4.25k | ("verus::vstd::atomic::try_open_atomic_update_end", VerusItem::OpenAtomicUpdate(OpenAtomicUpdateItem::TryOpenAtomicUpdateEnd)), |
669 | | |
670 | 4.25k | ("verus::vstd::seq::Seq::empty", VerusItem::Vstd(VstdItem::SeqFn(vir::interpreter::SeqFn::Empty ), Some(Arc::new("seq::Seq::empty" .to_owned())))), |
671 | 4.25k | ("verus::vstd::seq::Seq::new", VerusItem::Vstd(VstdItem::SeqFn(vir::interpreter::SeqFn::New ), Some(Arc::new("seq::Seq::new" .to_owned())))), |
672 | 4.25k | ("verus::vstd::seq::Seq::push", VerusItem::Vstd(VstdItem::SeqFn(vir::interpreter::SeqFn::Push ), Some(Arc::new("seq::Seq::push" .to_owned())))), |
673 | 4.25k | ("verus::vstd::seq::Seq::update", VerusItem::Vstd(VstdItem::SeqFn(vir::interpreter::SeqFn::Update ), Some(Arc::new("seq::Seq::update" .to_owned())))), |
674 | 4.25k | ("verus::vstd::seq::Seq::subrange", VerusItem::Vstd(VstdItem::SeqFn(vir::interpreter::SeqFn::Subrange), Some(Arc::new("seq::Seq::subrange" .to_owned())))), |
675 | 4.25k | ("verus::vstd::seq::Seq::add", VerusItem::Vstd(VstdItem::SeqFn(vir::interpreter::SeqFn::Add ), Some(Arc::new("seq::Seq::add" .to_owned())))), |
676 | 4.25k | ("verus::vstd::seq::Seq::len", VerusItem::Vstd(VstdItem::SeqFn(vir::interpreter::SeqFn::Len ), Some(Arc::new("seq::Seq::len" .to_owned())))), |
677 | 4.25k | ("verus::vstd::seq::Seq::index", VerusItem::Vstd(VstdItem::SeqFn(vir::interpreter::SeqFn::Index ), Some(Arc::new("seq::Seq::index" .to_owned())))), |
678 | 4.25k | ("verus::vstd::seq::Seq::ext_equal", VerusItem::Vstd(VstdItem::SeqFn(vir::interpreter::SeqFn::ExtEqual), Some(Arc::new("seq::Seq::ext_equal" .to_owned())))), |
679 | 4.25k | ("verus::vstd::seq::Seq::last", VerusItem::Vstd(VstdItem::SeqFn(vir::interpreter::SeqFn::Last ), Some(Arc::new("seq::Seq::last" .to_owned())))), |
680 | | |
681 | 4.25k | ("verus::vstd::set::Set", VerusItem::Vstd(VstdItem::SetItem(SetItem::Type), Some(Arc::new("set::Set".to_owned())))), |
682 | 4.25k | ("verus::vstd::set::Set::empty", VerusItem::Vstd(VstdItem::SetItem(SetItem::Empty), Some(Arc::new("set::Set::empty".to_owned())))), |
683 | 4.25k | ("verus::vstd::set::Set::full", VerusItem::Vstd(VstdItem::SetItem(SetItem::Full), Some(Arc::new("set::Set::full".to_owned())))), |
684 | 4.25k | ("verus::vstd::set::Set::contains", VerusItem::Vstd(VstdItem::SetItem(SetItem::Contains), Some(Arc::new("set::Set::contains".to_owned())))), |
685 | 4.25k | ("verus::vstd::set::Set::subset_of", VerusItem::Vstd(VstdItem::SetItem(SetItem::SubsetOf), Some(Arc::new("set::Set::subset_of".to_owned())))), |
686 | 4.25k | ("verus::vstd::set::Set::insert", VerusItem::Vstd(VstdItem::SetItem(SetItem::Insert), Some(Arc::new("set::Set::insert".to_owned())))), |
687 | 4.25k | ("verus::vstd::set::Set::remove", VerusItem::Vstd(VstdItem::SetItem(SetItem::Remove), Some(Arc::new("set::Set::remove".to_owned())))), |
688 | | |
689 | 4.25k | ("verus::vstd::iset::ISet", VerusItem::Vstd(VstdItem::ISetItem(SetItem::Type), Some(Arc::new("iset::ISet".to_owned())))), |
690 | 4.25k | ("verus::vstd::iset::ISet::empty", VerusItem::Vstd(VstdItem::ISetItem(SetItem::Empty), Some(Arc::new("iset::ISet::empty".to_owned())))), |
691 | 4.25k | ("verus::vstd::iset::ISet::full", VerusItem::Vstd(VstdItem::ISetItem(SetItem::Full), Some(Arc::new("iset::ISet::full".to_owned())))), |
692 | 4.25k | ("verus::vstd::iset::ISet::contains", VerusItem::Vstd(VstdItem::ISetItem(SetItem::Contains), Some(Arc::new("iset::ISet::contains".to_owned())))), |
693 | 4.25k | ("verus::vstd::iset::ISet::subset_of", VerusItem::Vstd(VstdItem::ISetItem(SetItem::SubsetOf), Some(Arc::new("iset::ISet::subset_of".to_owned())))), |
694 | 4.25k | ("verus::vstd::iset::ISet::insert", VerusItem::Vstd(VstdItem::ISetItem(SetItem::Insert), Some(Arc::new("iset::ISet::insert".to_owned())))), |
695 | 4.25k | ("verus::vstd::iset::ISet::remove", VerusItem::Vstd(VstdItem::ISetItem(SetItem::Remove), Some(Arc::new("iset::ISet::remove".to_owned())))), |
696 | | |
697 | 4.25k | ("verus::vstd::invariant::AtomicInvariant::namespace", VerusItem::Vstd(VstdItem::Invariant(InvariantItem::AtomicInvariantNamespace ), Some(Arc::new("invariant::AtomicInvariant::namespace" .to_owned())))), |
698 | 4.25k | ("verus::vstd::invariant::AtomicInvariant::inv", VerusItem::Vstd(VstdItem::Invariant(InvariantItem::AtomicInvariantInv ), Some(Arc::new("invariant::AtomicInvariant::inv" .to_owned())))), |
699 | 4.25k | ("verus::vstd::invariant::LocalInvariant::namespace", VerusItem::Vstd(VstdItem::Invariant(InvariantItem::LocalInvariantNamespace ), Some(Arc::new("invariant::LocalInvariant::namespace" .to_owned())))), |
700 | 4.25k | ("verus::vstd::invariant::LocalInvariant::inv", VerusItem::Vstd(VstdItem::Invariant(InvariantItem::LocalInvariantInv ), Some(Arc::new("invariant::LocalInvariant::inv" .to_owned())))), |
701 | 4.25k | ("verus::vstd::invariant::create_open_invariant_credit", VerusItem::Vstd(VstdItem::Invariant(InvariantItem::CreateOpenInvariantCredit ), Some(Arc::new("invariant::create_open_invariant_credit" .to_owned())))), |
702 | 4.25k | ("verus::vstd::invariant::spend_open_invariant_credit", VerusItem::Vstd(VstdItem::Invariant(InvariantItem::SpendOpenInvariantCredit ), Some(Arc::new("invariant::spend_open_invariant_credit" .to_owned())))), |
703 | 4.25k | ("verus::vstd::invariant::spend_open_invariant_credit_in_proof", VerusItem::Vstd(VstdItem::Invariant(InvariantItem::SpendOpenInvariantCreditInProof), Some(Arc::new("invariant::spend_open_invariant_credit_in_proof".to_owned())))), |
704 | 4.25k | ("verus::vstd::vstd::exec_nonstatic_call", VerusItem::Vstd(VstdItem::ExecNonstaticCall, Some(Arc::new("pervasive::exec_nonstatic_call".to_owned())))), |
705 | 4.25k | ("verus::vstd::vstd::proof_nonstatic_call", VerusItem::Vstd(VstdItem::ProofNonstaticCall, Some(Arc::new("pervasive::proof_nonstatic_call".to_owned())))), |
706 | | |
707 | 4.25k | ("verus::vstd::atomic::atomically", VerusItem::Spec(SpecItem::Atomically)), |
708 | 4.25k | ("verus::vstd::atomic::pred_args", VerusItem::Vstd(VstdItem::PredArgs, Some(Arc::new("atomic::pred_args".to_owned())))), |
709 | 4.25k | ("verus::vstd::atomic::branch_bool", VerusItem::Vstd(VstdItem::BranchBool, Some(Arc::new("atomic::branch_bool".to_owned())))), |
710 | 4.25k | ("verus::vstd::atomic::AtomicUpdate::req", VerusItem::Vstd(VstdItem::AtomicUpdate(AtomicUpdateItem::AtomicUpdateReq), Some(Arc::new("atomic::AtomicUpdate::req".to_owned())))), |
711 | 4.25k | ("verus::vstd::atomic::AtomicUpdate::ens", VerusItem::Vstd(VstdItem::AtomicUpdate(AtomicUpdateItem::AtomicUpdateEns), Some(Arc::new("atomic::AtomicUpdate::ens".to_owned())))), |
712 | 4.25k | ("verus::vstd::atomic::AtomicUpdate::pred", VerusItem::Vstd(VstdItem::AtomicUpdate(AtomicUpdateItem::AtomicUpdatePred), Some(Arc::new("atomic::AtomicUpdate::pred".to_owned())))), |
713 | 4.25k | ("verus::vstd::atomic::AtomicUpdate::resolves", VerusItem::Vstd(VstdItem::AtomicUpdate(AtomicUpdateItem::AtomicUpdateResolves), Some(Arc::new("atomic::AtomicUpdate::resolves".to_owned())))), |
714 | 4.25k | ("verus::vstd::atomic::AtomicUpdate::input", VerusItem::Vstd(VstdItem::AtomicUpdate(AtomicUpdateItem::AtomicUpdateInput), Some(Arc::new("atomic::AtomicUpdate::input".to_owned())))), |
715 | 4.25k | ("verus::vstd::atomic::AtomicUpdate::output", VerusItem::Vstd(VstdItem::AtomicUpdate(AtomicUpdateItem::AtomicUpdateOutput), Some(Arc::new("atomic::AtomicUpdate::output".to_owned())))), |
716 | 4.25k | ("verus::vstd::atomic::AtomicUpdate::outer_mask", VerusItem::Vstd(VstdItem::AtomicUpdate(AtomicUpdateItem::AtomicUpdateOuterMask), Some(Arc::new("atomic::AtomicUpdate::outer_mask".to_owned())))), |
717 | 4.25k | ("verus::vstd::atomic::AtomicUpdate::inner_mask", VerusItem::Vstd(VstdItem::AtomicUpdate(AtomicUpdateItem::AtomicUpdateInnerMask), Some(Arc::new("atomic::AtomicUpdate::inner_mask".to_owned())))), |
718 | | |
719 | 4.25k | ("verus::vstd::std_specs::vec::vec_index", VerusItem::Vstd(VstdItem::VecIndex, Some(Arc::new("std_specs::vec::vec_index".to_owned())))), |
720 | 4.25k | ("verus::vstd::std_specs::vec::vec_index_mut", VerusItem::Vstd(VstdItem::VecIndexMut, Some(Arc::new("std_specs::vec::vec_index_mut".to_owned())))), |
721 | 4.25k | ("verus::vstd::array::array_index_get", VerusItem::Vstd(VstdItem::ArrayIndexGet, Some(Arc::new("array::array_index_get".to_owned())))), |
722 | 4.25k | ("verus::vstd::array::array_as_slice", VerusItem::Vstd(VstdItem::ArrayAsSlice, Some(Arc::new("array::array_as_slice".to_owned())))), |
723 | 4.25k | ("verus::vstd::array::array_fill_for_copy_types", VerusItem::Vstd(VstdItem::ArrayFillForCopyTypes, Some(Arc::new("array::array_fill_for_copy_types".to_owned())))), |
724 | 4.25k | ("verus::vstd::array::ref_mut_array_unsizing_coercion", VerusItem::Vstd(VstdItem::RefMutArrayUnsizingCoercion, Some(Arc::new("array::ref_mut_array_unsizing_coercion".to_owned())))), |
725 | 4.25k | ("verus::vstd::array::spec_array_update", VerusItem::Vstd(VstdItem::SpecArrayUpdate, Some(Arc::new("array::spec_array_update".to_owned())))), |
726 | 4.25k | ("verus::vstd::slice::slice_index_get", VerusItem::Vstd(VstdItem::SliceIndexGet, Some(Arc::new("slice::slice_index_get".to_owned())))), |
727 | 4.25k | ("verus::vstd::slice::spec_slice_update", VerusItem::Vstd(VstdItem::SpecSliceUpdate, Some(Arc::new("slice::spec_slice_update".to_owned())))), |
728 | 4.25k | ("verus::vstd::slice::spec_slice_len", VerusItem::Vstd(VstdItem::SpecSliceLen, Some(Arc::new("slice::spec_slice_len".to_owned())))), |
729 | 4.25k | ("verus::vstd::slice::spec_slice_index", VerusItem::Vstd(VstdItem::SpecSliceIndex, Some(Arc::new("slice::spec_slice_index".to_owned())))), |
730 | 4.25k | ("verus::vstd::raw_ptr::cast_ptr_to_thin_ptr", VerusItem::Vstd(VstdItem::CastPtrToThinPtr, Some(Arc::new("raw_ptr::cast_ptr_to_thin_ptr".to_owned())))), |
731 | 4.25k | ("verus::vstd::raw_ptr::cast_array_ptr_to_slice_ptr", VerusItem::Vstd(VstdItem::CastArrayPtrToSlicePtr, Some(Arc::new("raw_ptr::cast_array_ptr_to_slice_ptr".to_owned())))), |
732 | 4.25k | ("verus::vstd::raw_ptr::cast_slice_ptr_to_slice_ptr", VerusItem::Vstd(VstdItem::CastSlicePtrToSlicePtr, Some(Arc::new("raw_ptr::cast_slice_ptr_to_slice_ptr".to_owned())))), |
733 | 4.25k | ("verus::vstd::raw_ptr::cast_slice_ptr_to_str_ptr", VerusItem::Vstd(VstdItem::CastSlicePtrToStrPtr, Some(Arc::new("raw_ptr::cast_slice_ptr_to_str_ptr".to_owned())))), |
734 | 4.25k | ("verus::vstd::raw_ptr::cast_str_ptr_to_slice_ptr", VerusItem::Vstd(VstdItem::CastStrPtrToSlicePtr, Some(Arc::new("raw_ptr::cast_str_ptr_to_slice_ptr".to_owned())))), |
735 | 4.25k | ("verus::vstd::raw_ptr::cast_ptr_to_usize", VerusItem::Vstd(VstdItem::CastPtrToUsize, Some(Arc::new("raw_ptr::cast_ptr_to_usize".to_owned())))), |
736 | 4.25k | ("verus::vstd::raw_ptr::SharedReference", VerusItem::Vstd(VstdItem::SharedReference, Some(Arc::new("raw_ptr::SharedReference".to_owned())))), |
737 | 4.25k | ("verus::vstd::float::float_cast", VerusItem::Vstd(VstdItem::FloatCast, Some(Arc::new("float::float_cast".to_owned())))), |
738 | | // SeqFn(vir::interpreter::SeqFn::Last ))), |
739 | | |
740 | 4.25k | ("verus::verus_builtin::Structural", VerusItem::Marker(MarkerItem::Structural)), |
741 | | |
742 | 4.25k | ("verus::verus_builtin::int", VerusItem::BuiltinType(BuiltinTypeItem::Int)), |
743 | 4.25k | ("verus::verus_builtin::nat", VerusItem::BuiltinType(BuiltinTypeItem::Nat)), |
744 | 4.25k | ("verus::verus_builtin::real", VerusItem::BuiltinType(BuiltinTypeItem::Real)), |
745 | 4.25k | ("verus::verus_builtin::FnSpec", VerusItem::BuiltinType(BuiltinTypeItem::FnSpec)), |
746 | 4.25k | ("verus::verus_builtin::Ghost", VerusItem::BuiltinType(BuiltinTypeItem::Ghost)), |
747 | 4.25k | ("verus::verus_builtin::Tracked", VerusItem::BuiltinType(BuiltinTypeItem::Tracked)), |
748 | | |
749 | 4.25k | ("verus::verus_builtin::Integer", VerusItem::BuiltinTrait(BuiltinTraitItem::Integer)), |
750 | 4.25k | ("verus::verus_builtin::Chainable", VerusItem::BuiltinTrait(BuiltinTraitItem::Chainable)), |
751 | 4.25k | ("verus::verus_builtin::private::Sealed", VerusItem::BuiltinTrait(BuiltinTraitItem::Sealed)), |
752 | | |
753 | 4.25k | ("verus::verus_builtin::call_requires", VerusItem::BuiltinFunction(BuiltinFunctionItem::CallRequires)), |
754 | 4.25k | ("verus::verus_builtin::call_ensures", VerusItem::BuiltinFunction(BuiltinFunctionItem::CallEnsures)), |
755 | 4.25k | ("verus::verus_builtin::constrain_type", VerusItem::BuiltinFunction(BuiltinFunctionItem::ConstrainType)), |
756 | 4.25k | ("verus::verus_builtin::get_future_output_type", VerusItem::BuiltinFunction(BuiltinFunctionItem::GetFutureOutputType)), |
757 | | |
758 | 4.25k | ("verus::verus_builtin::global_size_of", VerusItem::Global(GlobalItem::SizeOf)), |
759 | | |
760 | 4.25k | ("verus::verus_builtin::FnProof", VerusItem::External(ExternalItem::FnProof)), |
761 | 4.25k | ("verus::verus_builtin::FOpts", VerusItem::External(ExternalItem::FOpts)), |
762 | 4.25k | ("verus::verus_builtin::ProofFnReqEnsDef::req", VerusItem::External(ExternalItem::FnProofReq)), |
763 | 4.25k | ("verus::verus_builtin::ProofFnReqEnsDef::ens", VerusItem::External(ExternalItem::FnProofEns)), |
764 | 4.25k | ("verus::verus_builtin::ProofFnOnce", VerusItem::External(ExternalItem::ProofFnOnce)), |
765 | 4.25k | ("verus::verus_builtin::ProofFnMut", VerusItem::External(ExternalItem::ProofFnMut)), |
766 | 4.25k | ("verus::verus_builtin::ProofFn", VerusItem::External(ExternalItem::ProofFn)), |
767 | 4.25k | ("verus::verus_builtin::Trk", VerusItem::External(ExternalItem::Trk)), |
768 | 4.25k | ("verus::verus_builtin::RqEn", VerusItem::External(ExternalItem::RqEn)), |
769 | 4.25k | ("verus::verus_builtin::has_resolved", VerusItem::HasResolved), |
770 | 4.25k | ("verus::verus_builtin::has_resolved_unsized", VerusItem::HasResolvedUnsized), |
771 | 4.25k | ("verus::verus_builtin::mut_ref_current", VerusItem::MutRefCurrent), |
772 | 4.25k | ("verus::verus_builtin::mut_ref_future", VerusItem::MutRefFuture), |
773 | 4.25k | ("verus::verus_builtin::final_", VerusItem::Final), |
774 | 4.25k | ("verus::verus_builtin::after_borrow", VerusItem::AfterBorrow), |
775 | 4.25k | ("verus::verus_builtin::mut_ref_tracked", VerusItem::MutRefTracked), |
776 | | ] |
777 | 4.25k | } |
778 | | |
779 | | pub(crate) struct VerusItems { |
780 | | pub(crate) id_to_name: HashMap<DefId, VerusItem>, |
781 | | pub(crate) name_to_id: HashMap<VerusItem, DefId>, |
782 | | } |
783 | | |
784 | 4.25k | pub(crate) fn from_diagnostic_items( |
785 | 4.25k | diagnostic_items: &rustc_hir::diagnostic_items::DiagnosticItems, |
786 | 4.25k | ) -> VerusItems { |
787 | 4.25k | let verus_item_map: HashMap<&str, VerusItem> = verus_items_map().into_iter().collect(); |
788 | 4.25k | let diagnostic_name_to_id = &diagnostic_items.name_to_id; |
789 | 4.25k | let mut id_to_name: HashMap<DefId, VerusItem> = HashMap::new(); |
790 | 4.25k | let mut name_to_id: HashMap<VerusItem, DefId> = HashMap::new(); |
791 | 2.84M | for (name, id) in diagnostic_name_to_id { |
792 | 2.84M | let name = name.as_str(); |
793 | 2.84M | if name.starts_with("verus::verus_builtin") || name.starts_with("verus::vstd") { |
794 | 864k | if let Some(item) = verus_item_map.get(name) { |
795 | 864k | id_to_name.insert(id.clone(), item.clone()); |
796 | 864k | name_to_id.insert(item.clone(), id.clone()); |
797 | 864k | } else { |
798 | 0 | panic!("unexpected verus diagnostic item {}", name); |
799 | | } |
800 | 1.97M | } |
801 | | } |
802 | 4.25k | VerusItems { id_to_name, name_to_id } |
803 | 4.25k | } |
804 | | |
805 | | #[derive(PartialEq, Eq, Debug, Clone, Copy)] |
806 | | pub(crate) enum RustIntType { |
807 | | U8, |
808 | | U16, |
809 | | U32, |
810 | | U64, |
811 | | U128, |
812 | | USize, |
813 | | |
814 | | I8, |
815 | | I16, |
816 | | I32, |
817 | | I64, |
818 | | I128, |
819 | | ISize, |
820 | | } |
821 | | |
822 | | #[derive(PartialEq, Eq, Debug, Clone, Copy)] |
823 | | pub(crate) enum RustIntConst { |
824 | | Min, |
825 | | Max, |
826 | | Bits, |
827 | | } |
828 | | |
829 | | #[derive(PartialEq, Eq, Debug, Clone, Copy)] |
830 | | pub(crate) struct RustIntIntrinsicItem(pub(crate) RustIntType, pub(crate) RustIntConst); |
831 | | |
832 | | #[derive(PartialEq, Eq, Debug, Clone, Copy)] |
833 | | pub(crate) enum RustItem { |
834 | | Panic, |
835 | | Box, |
836 | | Fn, |
837 | | FnOnce, |
838 | | FnMut, |
839 | | Drop, |
840 | | Sized, |
841 | | Copy, |
842 | | Send, |
843 | | Sync, |
844 | | Any, |
845 | | Clone, |
846 | | StructuralPartialEq, |
847 | | Eq, |
848 | | PartialEq, |
849 | | Ord, |
850 | | PartialOrd, |
851 | | Hash, |
852 | | Default, |
853 | | Debug, |
854 | | Rc, |
855 | | Arc, |
856 | | BoxNew, |
857 | | ArcNew, |
858 | | RcNew, |
859 | | CloneClone, |
860 | | CloneFrom, |
861 | | IntIntrinsic(RustIntIntrinsicItem), |
862 | | TryTraitBranch, |
863 | | ResidualTraitFromResidual, |
864 | | IntoIterFn, |
865 | | ManuallyDrop, |
866 | | PhantomData, |
867 | | Destruct, |
868 | | SliceSealed, |
869 | | Vec, |
870 | | Thin, |
871 | | } |
872 | | |
873 | 4.68M | pub(crate) fn get_rust_item<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option<RustItem> { |
874 | | // if tcx.parent(def_id) == partial_eq { |
875 | 4.68M | if tcx.lang_items().panic_fn() == Some(def_id) { |
876 | 13.1k | return Some(RustItem::Panic); |
877 | 4.67M | } |
878 | 4.67M | if tcx.lang_items().owned_box() == Some(def_id) { |
879 | 11.2k | return Some(RustItem::Box); |
880 | 4.66M | } |
881 | 4.66M | if tcx.lang_items().fn_trait() == Some(def_id) { |
882 | 1 | return Some(RustItem::Fn); |
883 | 4.66M | } |
884 | 4.66M | if tcx.lang_items().fn_mut_trait() == Some(def_id) { |
885 | 217 | return Some(RustItem::FnMut); |
886 | 4.65M | } |
887 | 4.65M | if tcx.lang_items().fn_once_trait() == Some(def_id) { |
888 | 435 | return Some(RustItem::FnOnce); |
889 | 4.65M | } |
890 | 4.65M | if tcx.lang_items().drop_trait() == Some(def_id) { |
891 | 8 | return Some(RustItem::Drop); |
892 | 4.65M | } |
893 | 4.65M | if tcx.lang_items().structural_peq_trait() == Some(def_id) { |
894 | 722 | return Some(RustItem::StructuralPartialEq); |
895 | 4.65M | } |
896 | 4.65M | if tcx.lang_items().eq_trait() == Some(def_id) { |
897 | 840 | return Some(RustItem::PartialEq); |
898 | 4.65M | } |
899 | 4.65M | if tcx.lang_items().branch_fn() == Some(def_id) { |
900 | 65 | return Some(RustItem::TryTraitBranch); |
901 | 4.65M | } |
902 | 4.65M | if tcx.lang_items().from_residual_fn() == Some(def_id) { |
903 | 65 | return Some(RustItem::ResidualTraitFromResidual); |
904 | 4.65M | } |
905 | 4.65M | if tcx.lang_items().into_iter_fn() == Some(def_id) { |
906 | 313 | return Some(RustItem::IntoIterFn); |
907 | 4.65M | } |
908 | 4.65M | if tcx.lang_items().manually_drop() == Some(def_id) { |
909 | 1.82k | return Some(RustItem::ManuallyDrop); |
910 | 4.65M | } |
911 | 4.65M | if tcx.lang_items().phantom_data() == Some(def_id) { |
912 | 4.35k | return Some(RustItem::PhantomData); |
913 | 4.65M | } |
914 | 4.65M | if tcx.lang_items().destruct_trait() == Some(def_id) { |
915 | 542 | return Some(RustItem::Destruct); |
916 | 4.65M | } |
917 | 4.65M | if tcx.lang_items().partial_ord_trait() == Some(def_id) { |
918 | 976 | return Some(RustItem::PartialOrd); |
919 | 4.64M | } |
920 | 4.64M | let rust_path = def_id_to_stable_rust_path(tcx, def_id); |
921 | 4.64M | let rust_path = rust_path.as_ref().map(|x| x.as_str()); |
922 | 4.64M | get_rust_item_str(rust_path) |
923 | 4.68M | } |
924 | | |
925 | | #[allow(dead_code)] |
926 | 0 | pub(crate) fn get_rust_item_path(rust_path: &vir::ast::Path) -> Option<RustItem> { |
927 | 0 | get_rust_item_str(Some(&vir::ast_util::path_as_friendly_rust_name(rust_path))) |
928 | 0 | } |
929 | | |
930 | 4.64M | pub(crate) fn get_rust_item_str(rust_path: Option<&str>) -> Option<RustItem> { |
931 | | // We could use rust's diagnostic_items for these, but they are only defined when cfg(not(test)) |
932 | | // and they may get changed without us noticing, so we are using paths instead |
933 | 4.64M | if rust_path == Some("core::cmp::Eq") { |
934 | 1.39k | return Some(RustItem::Eq); |
935 | 4.64M | } |
936 | 4.64M | if rust_path == Some("alloc::rc::Rc") { |
937 | 3.41k | return Some(RustItem::Rc); |
938 | 4.64M | } |
939 | 4.64M | if rust_path == Some("alloc::sync::Arc") { |
940 | 3.00k | return Some(RustItem::Arc); |
941 | 4.64M | } |
942 | | |
943 | 4.64M | if rust_path == Some("alloc::boxed::Box::new") { |
944 | 445 | return Some(RustItem::BoxNew); |
945 | 4.64M | } |
946 | 4.64M | if rust_path == Some("alloc::sync::Arc::new") { |
947 | 38 | return Some(RustItem::ArcNew); |
948 | 4.64M | } |
949 | 4.64M | if rust_path == Some("alloc::rc::Rc::new") { |
950 | 34 | return Some(RustItem::RcNew); |
951 | 4.64M | } |
952 | | |
953 | 4.64M | if rust_path == Some("core::marker::Sized") { |
954 | 26.4k | return Some(RustItem::Sized); |
955 | 4.61M | } |
956 | 4.61M | if rust_path == Some("core::marker::Send") { |
957 | 58 | return Some(RustItem::Send); |
958 | 4.61M | } |
959 | 4.61M | if rust_path == Some("core::marker::Sync") { |
960 | 28 | return Some(RustItem::Sync); |
961 | 4.61M | } |
962 | 4.61M | if rust_path == Some("core::marker::Copy") { |
963 | 587 | return Some(RustItem::Copy); |
964 | 4.61M | } |
965 | 4.61M | if rust_path == Some("core::clone::Clone") { |
966 | 2.90k | return Some(RustItem::Clone); |
967 | 4.61M | } |
968 | 4.61M | if rust_path == Some("core::clone::Clone::clone") { |
969 | 875 | return Some(RustItem::CloneClone); |
970 | 4.61M | } |
971 | 4.61M | if rust_path == Some("core::clone::Clone::clone_from") { |
972 | 0 | return Some(RustItem::CloneFrom); |
973 | 4.61M | } |
974 | | |
975 | 4.61M | if rust_path == Some("core::slice::index::private_slice_index::Sealed") { |
976 | 54 | return Some(RustItem::SliceSealed); |
977 | 4.61M | } |
978 | 4.61M | if rust_path == Some("core::fmt::Debug") { |
979 | 217 | return Some(RustItem::Debug); |
980 | 4.61M | } |
981 | 4.61M | if rust_path == Some("core::hash::Hash") { |
982 | 957 | return Some(RustItem::Hash); |
983 | 4.60M | } |
984 | 4.60M | if rust_path == Some("core::default::Default") { |
985 | 586 | return Some(RustItem::Default); |
986 | 4.60M | } |
987 | 4.60M | if rust_path == Some("core::cmp::Ord") { |
988 | 842 | return Some(RustItem::Ord); |
989 | 4.60M | } |
990 | 4.60M | if rust_path == Some("alloc::vec::Vec") { |
991 | 25.7k | return Some(RustItem::Vec); |
992 | 4.58M | } |
993 | 4.58M | if rust_path == Some("core::ptr::metadata::Thin") { |
994 | 2 | return Some(RustItem::Thin); |
995 | 4.58M | } |
996 | 4.58M | if rust_path == Some("core::any::Any") { |
997 | 0 | return Some(RustItem::Any); |
998 | 4.58M | } |
999 | | |
1000 | 4.58M | if let Some(rust_path) = rust_path { |
1001 | | static NUM_RE: std::sync::OnceLock<Regex> = std::sync::OnceLock::new(); |
1002 | 4.58M | let num_re = |
1003 | 4.58M | NUM_RE.get_or_init(|| Regex::new(r"^([A-Za-z0-9_]+)::(MIN|MAX|BITS)").unwrap()); |
1004 | 4.58M | if let Some(captures) = num_re.captures(rust_path) { |
1005 | 20.0k | let ty_name = captures.get(1).expect("invalid int intrinsic regex"); |
1006 | 20.0k | let const_name = captures.get(2).expect("invalid int intrinsic regex"); |
1007 | | use RustIntType::*; |
1008 | 20.0k | let ty = match ty_name.as_str() { |
1009 | 20.0k | "u8" => Some(U8), |
1010 | 18.2k | "u16" => Some(U16), |
1011 | 16.5k | "u32" => Some(U32), |
1012 | 14.8k | "u64" => Some(U64), |
1013 | 13.2k | "u128" => Some(U128), |
1014 | 11.9k | "usize" => Some(USize), |
1015 | | |
1016 | 8.65k | "i8" => Some(I8), |
1017 | 6.98k | "i16" => Some(I16), |
1018 | 5.43k | "i32" => Some(I32), |
1019 | 3.92k | "i64" => Some(I64), |
1020 | 2.58k | "i128" => Some(I128), |
1021 | 1.51k | "isize" => Some(ISize), |
1022 | | |
1023 | 0 | _ => None, |
1024 | | }; |
1025 | 20.0k | return ty.map(|ty| { |
1026 | 20.0k | let const_ = match const_name.as_str() { |
1027 | 20.0k | "MIN" => RustIntConst::Min, |
1028 | 12.1k | "MAX" => RustIntConst::Max, |
1029 | 2.32k | "BITS" => RustIntConst::Bits, |
1030 | | |
1031 | 0 | _ => panic!("unexpected int const"), |
1032 | | }; |
1033 | 20.0k | RustItem::IntIntrinsic(RustIntIntrinsicItem(ty, const_)) |
1034 | 20.0k | }); |
1035 | 4.56M | } |
1036 | 1.64k | } |
1037 | | |
1038 | 4.56M | None |
1039 | 4.64M | } |