mirai_annotations/
lib.rs

1// Copyright (c) Facebook, Inc. and its affiliates.
2//
3// This source code is licensed under the MIT license found in the
4// LICENSE file in the root directory of this source tree.
5
6// A set of macros and functions to use for annotating source files that are being checked with MIRAI
7
8/// Provides a way to specify a value that should be treated abstractly by the verifier.
9/// The concrete argument provides type information to the verifier and a meaning for
10/// the expression when compiled by the rust compiler.
11///
12/// The expected use case for this is inside test cases. Principally this would be test cases
13/// for the verifier itself, but it can also be used to "fuzz" unit tests in user code.
14#[macro_export]
15macro_rules! abstract_value {
16    ($value:expr) => {
17        if cfg!(mirai) {
18            mirai_annotations::mirai_abstract_value($value)
19        } else {
20            $value
21        }
22    };
23}
24
25/// A type used to specify how tag types transfer over operations. The type is an alias of `u128`.
26/// Each bit of the bit vector controls the transfer function for an operation.
27/// If a bit is set to one, the corresponding operation will propagate the tag.
28/// If a bit is set to zero, the corresponding operation will block the tag.
29pub type TagPropagationSet = u128;
30
31/// An enum type of controllable operations for MIRAI tag types.
32/// In general, the result of the operation corresponding to an enum value will
33/// get tagged with all of the tags of the operands.
34#[derive(Ord, PartialOrd, Eq, PartialEq, Debug, Copy, Clone)]
35pub enum TagPropagation {
36    Add,
37    AddOverflows,
38    And,
39    BitAnd,
40    BitNot,
41    BitOr,
42    BitXor,
43    Cast,
44    Div,
45    Equals,
46    GreaterOrEqual,
47    GreaterThan,
48    IntrinsicBinary,
49    IntrinsicBitVectorUnary,
50    IntrinsicFloatingPointUnary,
51    LessOrEqual,
52    LessThan,
53    LogicalNot,
54    Memcmp,
55    Mul,
56    MulOverflows,
57    Ne,
58    Neg,
59    Or,
60    Offset,
61    Rem,
62    Shl,
63    ShlOverflows,
64    Shr,
65    ShrOverflows,
66    Sub,
67    /// Tagging a structured value also tags all of the component values.
68    SubComponent,
69    SubOverflows,
70    /// Tagging a value also tags any structured value that includes it.
71    SuperComponent,
72    Transmute,
73    UninterpretedCall,
74}
75
76/// Provide a way to create tag propagation sets. It is equivalent to bitwise-or of all its arguments.
77#[macro_export]
78macro_rules! tag_propagation_set {
79    ($($x:expr),*) => {
80        0 $(| (1 << ($x as u8)))*
81    };
82}
83
84/// A tag propagation set indicating a tag is propagated by all operations.
85pub const TAG_PROPAGATION_ALL: TagPropagationSet = tag_propagation_set!(
86    TagPropagation::Add,
87    TagPropagation::AddOverflows,
88    TagPropagation::And,
89    TagPropagation::BitAnd,
90    TagPropagation::BitNot,
91    TagPropagation::BitOr,
92    TagPropagation::BitXor,
93    TagPropagation::Cast,
94    TagPropagation::Div,
95    TagPropagation::Equals,
96    TagPropagation::GreaterOrEqual,
97    TagPropagation::GreaterThan,
98    TagPropagation::IntrinsicBinary,
99    TagPropagation::IntrinsicBitVectorUnary,
100    TagPropagation::IntrinsicFloatingPointUnary,
101    TagPropagation::LessOrEqual,
102    TagPropagation::LessThan,
103    TagPropagation::LogicalNot,
104    TagPropagation::Memcmp,
105    TagPropagation::Mul,
106    TagPropagation::MulOverflows,
107    TagPropagation::Ne,
108    TagPropagation::Neg,
109    TagPropagation::Or,
110    TagPropagation::Offset,
111    TagPropagation::Rem,
112    TagPropagation::Shl,
113    TagPropagation::ShlOverflows,
114    TagPropagation::Shr,
115    TagPropagation::ShrOverflows,
116    TagPropagation::Sub,
117    TagPropagation::SubComponent,
118    TagPropagation::SubOverflows,
119    TagPropagation::SuperComponent,
120    TagPropagation::UninterpretedCall
121);
122
123/// Equivalent to a no op when used with an unmodified Rust compiler.
124/// When compiled with MIRAI, this causes MIRAI to associate (tag) the value with the given type.
125/// Typically the type will be private to a scope so that only privileged code can add the tag.
126/// Once added, a tag cannot be removed and the tagged value may not be modified.
127/// To determine if a value has been tagged, use the has_tag! macro.
128#[macro_export]
129macro_rules! add_tag {
130    ($value:expr, $tag:ty) => {
131        if cfg!(mirai) {
132            mirai_annotations::mirai_add_tag::<_, $tag>($value)
133        }
134    };
135}
136
137/// Provides a way to check if a value has been tagged with a type, using the add_tag! macro.
138/// When compiled with an unmodified Rust compiler, this results in true.
139/// When compiled with MIRAI, this will be true if all data flows into the argument of this
140/// call has gone via a call to add_tag!.
141#[macro_export]
142macro_rules! has_tag {
143    ($value:expr, $tag:ty) => {
144        if cfg!(mirai) {
145            mirai_annotations::mirai_has_tag::<_, $tag>($value)
146        } else {
147            true
148        }
149    };
150}
151
152/// Provides a way to check if a value has *not* been tagged with a type using add_tag!.
153/// When compiled with an unmodified Rust compiler, this results in true.
154/// When compiled with MIRAI, this will be true if none data flows into the argument of this
155/// call has gone via a call to add_tag!.
156#[macro_export]
157macro_rules! does_not_have_tag {
158    ($value:expr, $tag:ty) => {
159        if cfg!(mirai) {
160            mirai_annotations::mirai_does_not_have_tag::<_, $tag>($value)
161        } else {
162            true
163        }
164    };
165}
166
167/// Equivalent to a no op when used with an unmodified Rust compiler.
168/// When compiled with MIRAI, this causes MIRAI to assume the condition unless it can
169/// prove it to be false.
170#[macro_export]
171macro_rules! assume {
172    ($condition:expr) => {
173        if cfg!(mirai) {
174            mirai_annotations::mirai_assume($condition)
175        }
176    };
177}
178
179/// Equivalent to a no op when used with an unmodified Rust compiler.
180/// When compiled with MIRAI, this causes MIRAI to assume that the preconditions of the next
181/// function call have been met.
182/// This is to be used when the precondition has been inferred and involves private state that
183/// cannot be constrained by a normal assumption.
184/// Note that it is bad style for an API to rely on preconditions that cannot be checked by the
185/// caller, so this is only here for supporting legacy APIs.
186#[macro_export]
187macro_rules! assume_preconditions {
188    () => {
189        if cfg!(mirai) {
190            mirai_annotations::mirai_assume_preconditions()
191        }
192    };
193}
194
195/// Equivalent to the standard assert! when used with an unmodified Rust compiler.
196/// When compiled with MIRAI, this causes MIRAI to assume the condition unless it can
197/// prove it to be false.
198#[macro_export]
199macro_rules! checked_assume {
200    ($condition:expr) => (
201        if cfg!(mirai) {
202            mirai_annotations::mirai_assume($condition)
203        } else {
204            assert!($condition);
205        }
206    );
207    ($condition:expr, $($arg:tt)*) => (
208        if cfg!(mirai) {
209            mirai_annotations::mirai_assume($condition);
210        } else {
211            assert!($condition, $($arg)*);
212        }
213    );
214}
215
216/// Equivalent to the standard assert_eq! when used with an unmodified Rust compiler.
217/// When compiled with MIRAI, this causes MIRAI to assume the condition unless it can
218/// prove it to be false.
219#[macro_export]
220macro_rules! checked_assume_eq {
221    ($left:expr, $right:expr) => (
222        if cfg!(mirai) {
223            mirai_annotations::mirai_assume($left == $right)
224        } else {
225            assert_eq!($left, $right);
226        }
227    );
228    ($left:expr, $right:expr, $($arg:tt)*) => (
229        if cfg!(mirai) {
230            mirai_annotations::mirai_assume($left == $right);
231        } else {
232            assert_eq!($left, $right, $($arg)*);
233        }
234    );
235}
236
237/// Equivalent to the standard assert_ne! when used with an unmodified Rust compiler.
238/// When compiled with MIRAI, this causes MIRAI to assume the condition unless it can
239/// prove it to be false.
240#[macro_export]
241macro_rules! checked_assume_ne {
242    ($left:expr, $right:expr) => (
243        if cfg!(mirai) {
244            mirai_annotations::mirai_assume($left != $right)
245        } else {
246            assert_ne!($left, $right);
247        }
248    );
249    ($left:expr, $right:expr, $($arg:tt)*) => (
250        if cfg!(mirai) {
251            mirai_annotations::mirai_assume($left != $right);
252        } else {
253            assert_ne!($left, $right, $($arg)*);
254        }
255    );
256}
257
258/// Equivalent to the standard debug_assert! when used with an unmodified Rust compiler.
259/// When compiled with MIRAI, this causes MIRAI to assume the condition unless it can
260/// prove it to be false.
261#[macro_export]
262macro_rules! debug_checked_assume {
263    ($condition:expr) => (
264        if cfg!(mirai) {
265            mirai_annotations::mirai_assume($condition)
266        } else {
267            debug_assert!($condition);
268        }
269    );
270    ($condition:expr, $($arg:tt)*) => (
271        if cfg!(mirai) {
272            mirai_annotations::mirai_assume($condition);
273        } else {
274            debug_assert!($condition, $($arg)*);
275        }
276    );
277}
278
279/// Equivalent to the standard debug_assert_eq! when used with an unmodified Rust compiler.
280/// When compiled with MIRAI, this causes MIRAI to assume the condition unless it can
281/// prove it to be false.
282#[macro_export]
283macro_rules! debug_checked_assume_eq {
284    ($left:expr, $right:expr) => (
285        if cfg!(mirai) {
286            mirai_annotations::mirai_assume($left == $right)
287        } else {
288            debug_assert_eq!($left, $right);
289        }
290    );
291    ($left:expr, $right:expr, $($arg:tt)*) => (
292        if cfg!(mirai) {
293            mirai_annotations::mirai_assume($left == $right);
294        } else {
295            debug_assert_eq!($left, $right, $($arg)*);
296        }
297    );
298}
299
300/// Equivalent to the standard debug_assert_ne! when used with an unmodified Rust compiler.
301/// When compiled with MIRAI, this causes MIRAI to assume the condition unless it can
302/// prove it to be false.
303#[macro_export]
304macro_rules! debug_checked_assume_ne {
305    ($left:expr, $right:expr) => (
306        if cfg!(mirai) {
307            mirai_annotations::mirai_assume($left != $right)
308        } else {
309            debug_assert_ne!($left, $right);
310        }
311    );
312    ($left:expr, $right:expr, $($arg:tt)*) => (
313        if cfg!(mirai) {
314            mirai_annotations::mirai_assume($left != $right);
315        } else {
316            debug_assert_ne!($left, $right, $($arg)*);
317        }
318    );
319}
320
321/// Equivalent to a no op when used with an unmodified Rust compiler.
322/// When compiled with MIRAI, this causes MIRAI to verify the condition at the
323/// point where it appears in a function, but to also add it a postcondition that can
324/// be assumed by the caller of the function.
325#[macro_export]
326macro_rules! postcondition {
327    ($condition:expr) => {
328        #[cfg(mirai)] {
329            mirai_annotations::mirai_postcondition($condition, false, "unsatisfied postcondition");
330        }
331    };
332    ($condition:expr, $message:literal) => {
333        #[cfg(mirai)] {
334            mirai_annotations::mirai_postcondition($condition, false,  concat!("unsatisfied postcondition: ", $message));
335        }
336    };
337    ($condition:expr, $($arg:tt)*) => {
338        #[cfg(mirai)] {
339            mirai_annotations::mirai_postcondition($condition, false,  concat!("unsatisfied postcondition: ", stringify!($($arg)*)));
340        }
341    };
342}
343
344/// Equivalent to a no op when used with an unmodified Rust compiler.
345/// When compiled with MIRAI, this causes MIRAI to assume the condition at the
346/// point where it appears in a function, but to also add it a postcondition that can
347/// be assumed by the caller of the function.
348#[macro_export]
349macro_rules! assumed_postcondition {
350    ($condition:expr) => {
351        #[cfg(mirai)]
352        {
353            mirai_annotations::mirai_postcondition($condition, true, "")
354        }
355        #[cfg(not(mirai))]
356        {
357            debug_assert!($condition);
358        }
359    };
360}
361
362/// Equivalent to the standard assert! when used with an unmodified Rust compiler.
363/// When compiled with MIRAI, this causes MIRAI to verify the condition at the
364/// point where it appears in a function, but to also add it a postcondition that can
365/// be assumed by the caller of the function.
366#[macro_export]
367macro_rules! checked_postcondition {
368    ($condition:expr) => (
369        #[cfg(mirai)] {
370            mirai_annotations::mirai_postcondition($condition, false,  "unsatisfied postcondition")
371        }
372        #[cfg(not(mirai))] {
373            assert!($condition);
374        }
375    );
376    ($condition:expr, $message:literal) => {
377        #[cfg(mirai)] {
378            mirai_annotations::mirai_postcondition($condition, false,  concat!("unsatisfied postcondition: ", $message))
379        }
380        #[cfg(not(mirai))] {
381            assert!($condition, $message);
382        }
383    };
384    ($condition:expr, $($arg:tt)*) => {
385        #[cfg(mirai)] {
386            mirai_annotations::mirai_postcondition($condition, false,  concat!("unsatisfied postcondition: ", stringify!($($arg)*)));
387        }
388        #[cfg(not(mirai))] {
389            assert!($condition, $($arg)*);
390        }
391    };
392}
393
394/// Equivalent to the standard assert_eq! when used with an unmodified Rust compiler.
395/// When compiled with MIRAI, this causes MIRAI to verify the condition at the
396/// point where it appears in a function, but to also add it a postcondition that can
397/// be assumed by the caller of the function.
398#[macro_export]
399macro_rules! checked_postcondition_eq {
400    ($left:expr, $right:expr) => (
401        if cfg!(mirai) {
402            mirai_annotations::mirai_postcondition($left == $right, false,  concat!("unsatisfied postcondition: ", stringify!($left == $right)))
403        } else {
404            assert_eq!($left, $right);
405        }
406    );
407    ($left:expr, $right:expr, $message:literal) => (
408        if cfg!(mirai) {
409            mirai_annotations::mirai_postcondition($left == $right, false,  concat!("unsatisfied postcondition: ", stringify!($left == $right), ", ", $message))
410        } else {
411            assert_eq!($left, $right, $message);
412        }
413    );
414    ($left:expr, $right:expr, $($arg:tt)*) => (
415        if cfg!(mirai) {
416            mirai_annotations::mirai_postcondition($left == $right, false,  concat!("unsatisfied postcondition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
417        } else {
418            assert_eq!($left, $right, $($arg)*);
419        }
420    );
421}
422
423/// Equivalent to the standard assert_ne! when used with an unmodified Rust compiler.
424/// When compiled with MIRAI, this causes MIRAI to verify the condition at the
425/// point where it appears in a function, but to also add it a postcondition that can
426/// be assumed by the caller of the function.
427#[macro_export]
428macro_rules! checked_postcondition_ne {
429    ($left:expr, $right:expr) => (
430        if cfg!(mirai) {
431            mirai_annotations::mirai_postcondition($left != $right, false,  concat!("unsatisfied postcondition: ", stringify!($left != $right)))
432        } else {
433            assert_ne!($left, $right);
434        }
435    );
436    ($left:expr, $right:expr, $message:literal) => (
437        if cfg!(mirai) {
438            mirai_annotations::mirai_postcondition($left != $right, false,  concat!("unsatisfied postcondition: ", stringify!($left != $right), ", ", $message))
439        } else {
440            assert_ne!($left, $right, $message);
441        }
442    );
443    ($left:expr, $right:expr, $($arg:tt)*) => (
444        if cfg!(mirai) {
445            mirai_annotations::mirai_postcondition($left != $right, false,  concat!("unsatisfied postcondition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
446        } else {
447            assert_ne!($left, $right, $($arg)*);
448        }
449    );
450}
451
452/// Equivalent to the standard debug_assert! when used with an unmodified Rust compiler.
453/// When compiled with MIRAI, this causes MIRAI to verify the condition at the
454/// point where it appears in a function, but to also add it a postcondition that can
455/// be assumed by the caller of the function.
456#[macro_export]
457macro_rules! debug_checked_postcondition {
458    ($condition:expr) => (
459        #[cfg(mirai)] {
460            mirai_annotations::mirai_postcondition($condition, false,  "unsatisfied postcondition")
461        }
462        #[cfg(not(mirai))] {
463            debug_assert!($condition);
464        }
465    );
466    ($condition:expr, $message:literal) => (
467        #[cfg(mirai)] {
468            mirai_annotations::mirai_postcondition($condition, false,  concat!("unsatisfied postcondition: ", $message))
469        }
470        #[cfg(not(mirai))] {
471            debug_assert!($condition, $message);
472        }
473    );
474    ($condition:expr, $($arg:tt)*) => (
475        #[cfg(mirai)] {
476            mirai_annotations::mirai_postcondition($condition, false,  concat!("unsatisfied postcondition: ", stringify!($($arg)*)));
477        }
478        #[cfg(not(mirai))] {
479            debug_assert!($condition, $($arg)*);
480        }
481    );
482}
483
484/// Equivalent to the standard debug_assert_eq! when used with an unmodified Rust compiler.
485/// When compiled with MIRAI, this causes MIRAI to verify the condition at the
486/// point where it appears in a function, but to also add it a postcondition that can
487/// be assumed by the caller of the function.
488#[macro_export]
489macro_rules! debug_checked_postcondition_eq {
490    ($left:expr, $right:expr) => (
491        #[cfg(mirai)] {
492            mirai_annotations::mirai_postcondition($left == $right, false,  concat!("unsatisfied postcondition: ", stringify!($left == $right)))
493        }
494        #[cfg(not(mirai))] {
495            debug_assert_eq!($left, $right);
496        }
497    );
498    ($left:expr, $right:expr, $message:literal) => (
499        #[cfg(mirai)] {
500            mirai_annotations::mirai_postcondition($left == $right, false,  concat!("unsatisfied postcondition: ", stringify!($left == $right), ", ", $message))
501        }
502        #[cfg(not(mirai))] {
503            debug_assert_eq!($left, $right, $message);
504        }
505    );
506    ($left:expr, $right:expr, $($arg:tt)*) => (
507        #[cfg(mirai)] {
508            mirai_annotations::mirai_postcondition($left == $right, false,  concat!("unsatisfied postcondition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
509        }
510        #[cfg(not(mirai))] {
511            debug_assert_eq!($left, $right, $($arg)*);
512        }
513    );
514}
515
516/// Equivalent to the standard debug_assert_ne! when used with an unmodified Rust compiler.
517/// When compiled with MIRAI, this causes MIRAI to verify the condition at the
518/// point where it appears in a function, but to also add it a postcondition that can
519/// be assumed by the caller of the function.
520#[macro_export]
521macro_rules! debug_checked_postcondition_ne {
522    ($left:expr, $right:expr) => (
523        #[cfg(mirai)] {
524            mirai_annotations::mirai_postcondition($left != $right, false,  concat!("unsatisfied postcondition: ", stringify!($left != $right)))
525        }
526        #[cfg(not(mirai))] {
527            debug_assert_ne!($left, $right);
528        }
529    );
530    ($left:expr, $right:expr, $message:literal) => (
531        #[cfg(mirai)] {
532            mirai_annotations::mirai_postcondition($left != $right, false,  concat!("unsatisfied postcondition: ", stringify!($left != $right), ", ", $message))
533        }
534        #[cfg(not(mirai))] {
535            debug_assert_ne!($left, $right, $message);
536        }
537    );
538    ($left:expr, $right:expr, $($arg:tt)*) => (
539        #[cfg(mirai)] {
540            mirai_annotations::mirai_postcondition($left != $right, false,  concat!("unsatisfied postcondition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
541        }
542        #[cfg(not(mirai))] {
543            debug_assert_ne!($left, $right, $($arg)*);
544        }
545    );
546}
547
548/// Equivalent to a no op when used with an unmodified Rust compiler.
549/// When compiled with MIRAI, this causes MIRAI to assume the condition at the
550/// point where it appears in a function, but to also add it a precondition that must
551/// be verified by the caller of the function.
552#[macro_export]
553macro_rules! precondition {
554    ($condition:expr) => {
555        if cfg!(mirai) {
556            mirai_annotations::mirai_precondition_start();
557            mirai_annotations::mirai_precondition($condition, "unsatisfied precondition")
558        }
559    };
560    ($condition:expr, $message:literal) => {
561        if cfg!(mirai) {
562            mirai_annotations::mirai_precondition_start();
563            mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", $message))
564        }
565    };
566    ($condition:expr, $($arg:tt)*) => {
567        if cfg!(mirai) {
568            mirai_annotations::mirai_precondition_start();
569            mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", stringify!($($arg)*)));
570        }
571    };
572}
573
574/// Equivalent to the standard assert! when used with an unmodified Rust compiler.
575/// When compiled with MIRAI, this causes MIRAI to assume the condition at the
576/// point where it appears in a function, but to also add it a precondition that must
577/// be verified by the caller of the function.
578#[macro_export]
579macro_rules! checked_precondition {
580    ($condition:expr) => (
581        if cfg!(mirai) {
582            mirai_annotations::mirai_precondition_start();
583            mirai_annotations::mirai_precondition($condition, "unsatisfied precondition")
584        } else {
585            assert!($condition);
586        }
587    );
588    ($condition:expr, $message:literal) => (
589        if cfg!(mirai) {
590            mirai_annotations::mirai_precondition_start();
591            mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", $message))
592        } else {
593            assert!($condition, $message);
594        }
595    );
596    ($condition:expr, $($arg:tt)*) => (
597        if cfg!(mirai) {
598            mirai_annotations::mirai_precondition_start();
599            mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", stringify!($($arg)*)));
600        } else {
601            assert!($condition, $($arg)*);
602        }
603    );
604}
605
606/// Equivalent to the standard assert_eq! when used with an unmodified Rust compiler.
607/// When compiled with MIRAI, this causes MIRAI to assume the condition at the
608/// point where it appears in a function, but to also add it a precondition that must
609/// be verified by the caller of the function.
610#[macro_export]
611macro_rules! checked_precondition_eq {
612    ($left:expr, $right:expr) => (
613        if cfg!(mirai) {
614            mirai_annotations::mirai_precondition_start();
615            mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right)))
616        } else {
617            assert_eq!($left, $right);
618        }
619    );
620    ($left:expr, $right:expr, $message:literal) => (
621        if cfg!(mirai) {
622            mirai_annotations::mirai_precondition_start();
623            mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", $message))
624        } else {
625            assert_eq!($left, $right, $message);
626        }
627    );
628    ($left:expr, $right:expr, $($arg:tt)*) => (
629        if cfg!(mirai) {
630            mirai_annotations::mirai_precondition_start();
631            mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
632        } else {
633            assert_eq!($left, $right, $($arg)*);
634        }
635    );
636}
637
638/// Equivalent to the standard assert_ne! when used with an unmodified Rust compiler.
639/// When compiled with MIRAI, this causes MIRAI to assume the condition at the
640/// point where it appears in a function, but to also add it a precondition that must
641/// be verified by the caller of the function.
642#[macro_export]
643macro_rules! checked_precondition_ne {
644    ($left:expr, $right:expr) => (
645        if cfg!(mirai) {
646            mirai_annotations::mirai_precondition_start();
647            mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right)))
648        } else {
649            assert_ne!($left, $right);
650        }
651    );
652    ($left:expr, $right:expr, $message:literal) => (
653        if cfg!(mirai) {
654            mirai_annotations::mirai_precondition_start();
655            mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", $message))
656        } else {
657            assert_ne!($left, $right, $message);
658        }
659    );
660    ($left:expr, $right:expr, $($arg:tt)*) => (
661        if cfg!(mirai) {
662            mirai_annotations::mirai_precondition_start();
663            mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
664        } else {
665            assert_ne!($left, $right, $($arg)*);
666        }
667    );
668}
669
670/// Equivalent to the standard debug_assert! when used with an unmodified Rust compiler.
671/// When compiled with MIRAI, this causes MIRAI to assume the condition at the
672/// point where it appears in a function, but to also add it a precondition that must
673/// be verified by the caller of the function.
674#[macro_export]
675macro_rules! debug_checked_precondition {
676    ($condition:expr) => (
677        if cfg!(mirai) {
678            mirai_annotations::mirai_precondition_start();
679            mirai_annotations::mirai_precondition($condition, "unsatisfied precondition")
680        } else {
681            debug_assert!($condition);
682        }
683    );
684    ($condition:expr, $message:literal) => (
685        if cfg!(mirai) {
686            mirai_annotations::mirai_precondition_start();
687            mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", $message))
688        } else {
689            debug_assert!($condition, $message);
690        }
691    );
692    ($condition:expr, $($arg:tt)*) => (
693        if cfg!(mirai) {
694            mirai_annotations::mirai_precondition_start();
695            mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", stringify!($($arg)*)));
696        } else {
697            debug_assert!($condition, $($arg)*);
698        }
699    );
700}
701
702/// Equivalent to the standard debug_assert_eq! when used with an unmodified Rust compiler.
703/// When compiled with MIRAI, this causes MIRAI to assume the condition at the
704/// point where it appears in a function, but to also add it a precondition that must
705/// be verified by the caller of the function.
706#[macro_export]
707macro_rules! debug_checked_precondition_eq {
708    ($left:expr, $right:expr) => (
709        if cfg!(mirai) {
710            mirai_annotations::mirai_precondition_start();
711            mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right)))
712        } else {
713            debug_assert_eq!($left, $right);
714        }
715    );
716    ($left:expr, $right:expr, $message:literal) => (
717        if cfg!(mirai) {
718            mirai_annotations::mirai_precondition_start();
719            mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", $message))
720        } else {
721            debug_assert_eq!($left, $right, $message);
722        }
723    );
724    ($left:expr, $right:expr, $($arg:tt)*) => (
725        if cfg!(mirai) {
726            mirai_annotations::mirai_precondition_start();
727            mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
728        } else {
729            debug_assert_eq!($left, $right, $($arg)*);
730        }
731    );
732}
733
734/// Equivalent to the standard debug_assert_ne! when used with an unmodified Rust compiler.
735/// When compiled with MIRAI, this causes MIRAI to assume the condition at the
736/// point where it appears in a function, but to also add it a precondition that must
737/// be verified by the caller of the function.
738#[macro_export]
739macro_rules! debug_checked_precondition_ne {
740    ($left:expr, $right:expr) => (
741        if cfg!(mirai) {
742            mirai_annotations::mirai_precondition_start();
743            mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right)))
744        } else {
745            debug_assert_ne!($left, $right);
746        }
747    );
748    ($left:expr, $right:expr, $message:literal) => (
749        if cfg!(mirai) {
750            mirai_annotations::mirai_precondition_start();
751            mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", $message))
752        } else {
753            debug_assert_ne!($left, $right, $message);
754        }
755    );
756    ($left:expr, $right:expr, $($arg:tt)*) => (
757        if cfg!(mirai) {
758            mirai_annotations::mirai_precondition_start();
759            mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
760        } else {
761            debug_assert_ne!($left, $right, $($arg)*);
762        }
763    );
764}
765
766/// Terminates the program with a panic that is tagged as being an unrecoverable error.
767/// Use this for errors that arise in correct programs due to external factors.
768/// For example, if a file that is essential for running cannot be found for some reason.
769#[macro_export]
770macro_rules! unrecoverable {
771    ($fmt:expr) => (
772        panic!(concat!("unrecoverable: ", stringify!($fmt)));
773    );
774    ($fmt:expr, $($arg:tt)+) => (
775        panic!(concat!("unrecoverable: ", stringify!($fmt)), $($arg)+);
776    );
777}
778
779/// Equivalent to a no op when used with an unmodified Rust compiler.
780/// When compiled with MIRAI, this causes MIRAI to check the condition and
781/// emit a diagnostic unless it can prove it to be true.
782#[macro_export]
783macro_rules! verify {
784    ($condition:expr) => {
785        if cfg!(mirai) {
786            mirai_annotations::mirai_verify($condition, "false verification condition")
787        }
788    };
789}
790
791/// Equivalent to the standard assert! when used with an unmodified Rust compiler.
792/// When compiled with MIRAI, this causes MIRAI to check the condition and
793/// emit a diagnostic unless it can prove it to be true.
794#[macro_export]
795macro_rules! checked_verify {
796    ($condition:expr) => (
797        if cfg!(mirai) {
798            mirai_annotations::mirai_verify($condition, "false verification condition")
799        } else {
800            assert!($condition);
801        }
802    );
803    ($condition:expr, $message:literal) => {
804        if cfg!(mirai) {
805            mirai_annotations::mirai_verify($condition, concat!("false verification condition: ", $message))
806        } else {
807            assert!($condition, $message);
808        }
809    };
810    ($condition:expr, $($arg:tt)*) => (
811        if cfg!(mirai) {
812            mirai_annotations::mirai_verify($condition,  concat!("false verification condition: ", stringify!($($arg)*)));
813        } else {
814            assert!($condition, $($arg)*);
815        }
816    );
817}
818
819/// Equivalent to the standard assert_eq! when used with an unmodified Rust compiler.
820/// When compiled with MIRAI, this causes MIRAI to check the condition and
821/// emit a diagnostic unless it can prove it to be true.
822#[macro_export]
823macro_rules! checked_verify_eq {
824    ($left:expr, $right:expr) => (
825        if cfg!(mirai) {
826            mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right)))
827        } else {
828            assert_eq!($left, $right);
829        }
830    );
831    ($left:expr, $right:expr, $message:literal) => (
832        if cfg!(mirai) {
833            mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", $message))
834        } else {
835            assert_eq!($left, $right, $message);
836        }
837    );
838    ($left:expr, $right:expr, $($arg:tt)*) => (
839        if cfg!(mirai) {
840            mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
841        } else {
842            assert_eq!($left, $right, $($arg)*);
843        }
844    );
845}
846
847/// Equivalent to the standard assert_eq! when used with an unmodified Rust compiler.
848/// When compiled with MIRAI, this causes MIRAI to check the condition and
849/// emit a diagnostic unless it can prove it to be true.
850#[macro_export]
851macro_rules! checked_verify_ne {
852    ($left:expr, $right:expr) => (
853        if cfg!(mirai) {
854            mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right)))
855        } else {
856            assert_ne!($left, $right);
857        }
858    );
859    ($left:expr, $right:expr, $message:literal) => (
860        if cfg!(mirai) {
861            mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", $message))
862        } else {
863            assert_ne!($left, $right, $message);
864        }
865    );
866    ($left:expr, $right:expr, $($arg:tt)*) => (
867        if cfg!(mirai) {
868            mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
869        } else {
870            assert_ne!($left, $right, $($arg)*);
871        }
872    );
873}
874
875/// Equivalent to the standard debug_assert! when used with an unmodified Rust compiler.
876/// When compiled with MIRAI, this causes MIRAI to check the condition and
877/// emit a diagnostic unless it can prove it to be true.
878#[macro_export]
879macro_rules! debug_checked_verify {
880    ($condition:expr) => (
881        if cfg!(mirai) {
882            mirai_annotations::mirai_verify($condition, "false verification condition")
883        } else {
884            debug_assert!($condition);
885        }
886    );
887    ($condition:expr, $message:literal) => {
888        if cfg!(mirai) {
889            mirai_annotations::mirai_verify($condition, concat!("false verification condition: ", $message))
890        } else {
891            debug_assert!($condition, $message);
892        }
893    };
894    ($condition:expr, $($arg:tt)*) => (
895        if cfg!(mirai) {
896            mirai_annotations::mirai_verify($condition,  concat!("false verification condition: ", stringify!($($arg)*)));
897        } else {
898            debug_assert!($condition, $($arg)*);
899        }
900    );
901}
902
903/// Equivalent to the standard debug_assert_eq! when used with an unmodified Rust compiler.
904/// When compiled with MIRAI, this causes MIRAI to check the condition and
905/// emit a diagnostic unless it can prove it to be true.
906#[macro_export]
907macro_rules! debug_checked_verify_eq {
908    ($left:expr, $right:expr) => (
909        if cfg!(mirai) {
910            mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right)))
911        } else {
912            debug_assert_eq!($left, $right);
913        }
914    );
915    ($left:expr, $right:expr, $message:literal) => (
916        if cfg!(mirai) {
917            mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", $message))
918        } else {
919            debug_assert_eq!($left, $right, $message);
920        }
921    );
922    ($left:expr, $right:expr, $($arg:tt)*) => (
923        if cfg!(mirai) {
924            mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
925        } else {
926            debug_assert_eq!($left, $right, $($arg)*);
927        }
928    );
929}
930
931/// Equivalent to the standard debug_assert_ne! when used with an unmodified Rust compiler.
932/// When compiled with MIRAI, this causes MIRAI to check the condition and
933/// emit a diagnostic unless it can prove it to be true.
934#[macro_export]
935macro_rules! debug_checked_verify_ne {
936    ($left:expr, $right:expr) => (
937        if cfg!(mirai) {
938            mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right)))
939        } else {
940            debug_assert_ne!($left, $right);
941        }
942    );
943    ($left:expr, $right:expr, $message:literal) => (
944        if cfg!(mirai) {
945            mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", $message))
946        } else {
947            debug_assert_ne!($left, $right, $message);
948        }
949    );
950    ($left:expr, $right:expr, $($arg:tt)*) => (
951        if cfg!(mirai) {
952            mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
953        } else {
954            debug_assert_ne!($left, $right, $($arg)*);
955        }
956    );
957}
958
959/// Retrieves the value of the specified model field, or the given default value if the model field
960/// is not set.
961/// This function has no meaning outside of a verification
962/// condition and should not be used with checked or debug_checked conditions.
963/// For example: precondition!(get_model_field!(x, f) > 1).
964#[macro_export]
965macro_rules! get_model_field {
966    ($target:expr, $field_name:ident, $default_value:expr) => {
967        mirai_annotations::mirai_get_model_field($target, stringify!($field_name), $default_value)
968    };
969}
970
971/// Provides a way to refer to the result value of an abstract or contract function without
972/// specifying an actual value anywhere.
973/// This macro expands to unimplemented!() unless the program is compiled with MIRAI.
974/// It result should therefore not be assigned to a variable unless the assignment is contained
975/// inside a specification macro argument list.
976/// It may, however, be the return value of the function, which should never be called and
977/// therefore unimplemented!() is the right behavior for it at runtime.
978#[macro_export]
979macro_rules! result {
980    () => {
981        if cfg!(mirai) {
982            mirai_annotations::mirai_result()
983        } else {
984            unimplemented!()
985        }
986    };
987}
988
989/// Sets the value of the specified model field.
990/// A model field does not exist at runtime and is invisible to the Rust compiler.
991/// This macro expands to nothing unless the program is compiled with MIRAI.
992#[macro_export]
993macro_rules! set_model_field {
994    ($target:expr, $field_name:ident, $value:expr) => {
995        if cfg!(mirai) {
996            mirai_annotations::mirai_set_model_field($target, stringify!($field_name), $value);
997        }
998    };
999}
1000
1001/// Equivalent to unreachable! when used with an unmodified Rust compiler.
1002/// When compiled with MIRAI, this causes MIRAI to assume that the annotation statement cannot be reached.
1003#[macro_export]
1004macro_rules! assume_unreachable {
1005    () => {
1006        if cfg!(mirai) {
1007            unreachable!()
1008        } else {
1009            unreachable!()
1010        }
1011    };
1012    ($message:literal) => {
1013        if cfg!(mirai) {
1014            unreachable!()
1015        } else {
1016            unreachable!($message)
1017        }
1018    };
1019    ($msg:expr,) => ({
1020        if cfg!(mirai) {
1021            unreachable!()
1022        } else {
1023            unreachable!($msg)
1024        }
1025    });
1026    ($fmt:expr, $($arg:tt)*) => {
1027        if cfg!(mirai) {
1028            unreachable!()
1029        } else {
1030            unreachable!($fmt, $($arg)*)
1031        }
1032    };
1033}
1034
1035/// Equivalent to unreachable! when used with an unmodified Rust compiler.
1036/// When compiled with MIRAI, this causes MIRAI to verify that the annotation statement cannot be reached.
1037#[macro_export]
1038macro_rules! verify_unreachable {
1039    () => {
1040        if cfg!(mirai) {
1041            panic!("statement is reachable");
1042        } else {
1043            unreachable!()
1044        }
1045    };
1046    ($message:literal) => {
1047        if cfg!(mirai) {
1048            panic!($message);
1049        } else {
1050            unreachable!($message)
1051        }
1052    };
1053    ($msg:expr,) => ({
1054        if cfg!(mirai) {
1055            panic!($message)
1056        } else {
1057            unreachable!($msg)
1058        }
1059    });
1060    ($fmt:expr, $($arg:tt)*) => {
1061        if cfg!(mirai) {
1062            panic!($fmt, $($arg)*);
1063        } else {
1064            unreachable!($fmt, $($arg)*)
1065        }
1066    };
1067}
1068
1069// Helper function for MIRAI. Should only be called via the abstract_value! macro.
1070#[doc(hidden)]
1071pub fn mirai_abstract_value<T>(x: T) -> T {
1072    x
1073}
1074
1075// Helper function for MIRAI. Should only be called via the add_tag! macro.
1076#[doc(hidden)]
1077pub fn mirai_add_tag<V: ?Sized, T>(_v: &V) {}
1078
1079// Helper function for MIRAI. Should only be called via the has_tag! macro.
1080#[doc(hidden)]
1081pub fn mirai_has_tag<V: ?Sized, T>(_v: &V) -> bool {
1082    false
1083}
1084
1085// Helper function for MIRAI. Should only be called via the does_not_have_tag! macro.
1086#[doc(hidden)]
1087pub fn mirai_does_not_have_tag<V: ?Sized, T>(_v: &V) -> bool {
1088    false
1089}
1090
1091// Helper function for MIRAI. Should only be called via the assume macros.
1092#[doc(hidden)]
1093pub fn mirai_assume(_condition: bool) {}
1094
1095// Helper function for MIRAI. Should only be called via the assume_precondition macro.
1096#[doc(hidden)]
1097pub fn mirai_assume_preconditions() {}
1098
1099// Helper function for MIRAI. Should only be called via the postcondition macros.
1100#[doc(hidden)]
1101pub fn mirai_postcondition(_condition: bool, _assumed: bool, _message: &str) {}
1102
1103// Helper function for MIRAI. Should only be called via the precondition macros.
1104#[doc(hidden)]
1105pub fn mirai_precondition_start() {}
1106
1107// Helper function for MIRAI. Should only be called via the precondition macros.
1108#[doc(hidden)]
1109pub fn mirai_precondition(_condition: bool, _message: &str) {}
1110
1111// Helper function for MIRAI. Should only be called via the verify macros.
1112#[doc(hidden)]
1113pub fn mirai_verify(_condition: bool, _message: &str) {}
1114
1115// Helper function for MIRAI. Should only be called via the get_model_field macro.
1116#[doc(hidden)]
1117pub fn mirai_get_model_field<T, V>(_target: T, _field_name: &str, default_value: V) -> V {
1118    default_value
1119}
1120
1121// Helper function for MIRAI. Should only be called via the result! macro.
1122#[doc(hidden)]
1123pub fn mirai_result<T>() -> T {
1124    unreachable!()
1125}
1126
1127// Helper function for MIRAI. Should only be called via the set_model_field macro.
1128#[doc(hidden)]
1129pub fn mirai_set_model_field<T, V>(_target: T, _field_name: &str, _value: V) {}
mirai_annotations/lib.rs

mirai_annotations/
lib.rs
