1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191
// Copyright (c) The Diem Core Contributors
// SPDX-License-Identifier: Apache-2.0
//! Provides pragmas and properties of the specification language.
use crate::{ast::ConditionKind, builder::module_builder::SpecBlockContext};
/// Pragma indicating whether verification should be performed for a function.
pub const VERIFY_PRAGMA: &str = "verify";
/// Pragma defining a timeout.
pub const TIMEOUT_PRAGMA: &str = "timeout";
/// Pragma defining a random seed.
pub const SEED_PRAGMA: &str = "seed";
/// Pragma indicating an estimate how long verification takes. Verification
/// is skipped if the timeout is smaller than this.
pub const VERIFY_DURATION_ESTIMATE_PRAGMA: &str = "verify_duration_estimate";
/// Pragma indicating whether implementation of function should be ignored and
/// instead treated to be like a native function.
pub const INTRINSIC_PRAGMA: &str = "intrinsic";
/// Pragma indicating whether implementation of function should be ignored and
/// instead interpreted by its pre and post conditions only.
pub const OPAQUE_PRAGMA: &str = "opaque";
/// Pragma indicating whether emits specification should be considered partial.
pub const EMITS_IS_PARTIAL_PRAGMA: &str = "emits_is_partial";
/// Pragma indicating whether no emits specification should mean that no events are to be emitted.
pub const EMITS_IS_STRICT_PRAGMA: &str = "emits_is_strict";
/// Pragma indicating whether aborts_if specification should be considered partial.
pub const ABORTS_IF_IS_PARTIAL_PRAGMA: &str = "aborts_if_is_partial";
/// Pragma indicating whether no explicit aborts_if specification should be treated
/// like `aborts_if` false.
pub const ABORTS_IF_IS_STRICT_PRAGMA: &str = "aborts_if_is_strict";
/// Pragma indicating that requires are also enforced if the aborts condition is true.
pub const REQUIRES_IF_ABORTS_PRAGMA: &str = "requires_if_aborts";
/// Pragma indicating that the function will run smoke tests
pub const ALWAYS_ABORTS_TEST_PRAGMA: &str = "always_aborts_test";
/// Pragma indicating that adding u64 or u128 values should not be checked
/// for overflow.
pub const ADDITION_OVERFLOW_UNCHECKED_PRAGMA: &str = "addition_overflow_unchecked";
/// Pragma indicating that aborts from this function shall be ignored.
pub const ASSUME_NO_ABORT_FROM_HERE_PRAGMA: &str = "assume_no_abort_from_here";
/// Pragma which indicates that the function's abort and ensure conditions shall be exported
/// to the verification context even if the implementation of the function is inlined.
pub const EXPORT_ENSURES_PRAGMA: &str = "export_ensures";
/// Pragma indicating that the function can only be called from certain caller.
/// Unlike other pragmas, this pragma expects a function name like `0x1::M::f` instead
/// of a boolean or a number.
pub const FRIEND_PRAGMA: &str = "friend";
/// Pragma indicating that invariants are not to be checked between entry and exit
/// to this function
pub const DISABLE_INVARIANTS_IN_BODY_PRAGMA: &str = "disable_invariants_in_body";
/// Pragma indicating that invariants are not to be checked between entry and exit
/// to this function
pub const DELEGATE_INVARIANTS_TO_CALLER_PRAGMA: &str = "delegate_invariants_to_caller";
/// Checks whether a pragma is valid in a specific spec block.
pub fn is_pragma_valid_for_block(target: &SpecBlockContext<'_>, pragma: &str) -> bool {
use crate::builder::module_builder::SpecBlockContext::*;
match target {
Module => matches!(
pragma,
VERIFY_PRAGMA
| EMITS_IS_STRICT_PRAGMA
| EMITS_IS_PARTIAL_PRAGMA
| ABORTS_IF_IS_STRICT_PRAGMA
| ABORTS_IF_IS_PARTIAL_PRAGMA
| INTRINSIC_PRAGMA
),
Function(..) => matches!(
pragma,
VERIFY_PRAGMA
| TIMEOUT_PRAGMA
| SEED_PRAGMA
| VERIFY_DURATION_ESTIMATE_PRAGMA
| INTRINSIC_PRAGMA
| OPAQUE_PRAGMA
| EMITS_IS_STRICT_PRAGMA
| EMITS_IS_PARTIAL_PRAGMA
| ABORTS_IF_IS_PARTIAL_PRAGMA
| ABORTS_IF_IS_STRICT_PRAGMA
| REQUIRES_IF_ABORTS_PRAGMA
| ALWAYS_ABORTS_TEST_PRAGMA
| ADDITION_OVERFLOW_UNCHECKED_PRAGMA
| ASSUME_NO_ABORT_FROM_HERE_PRAGMA
| EXPORT_ENSURES_PRAGMA
| FRIEND_PRAGMA
| DISABLE_INVARIANTS_IN_BODY_PRAGMA
| DELEGATE_INVARIANTS_TO_CALLER_PRAGMA
),
_ => false,
}
}
/// Internal property attached to conditions if they are injected via an apply or a module
/// invariant.
pub const CONDITION_INJECTED_PROP: &str = "$injected";
/// Property which can be attached to conditions to make them exported into the VC context
/// even if they are injected.
pub const CONDITION_EXPORT_PROP: &str = "export";
/// Property which can be attached to a module invariant to make it global.
pub const CONDITION_GLOBAL_PROP: &str = "global";
/// Property which can be attached to a global invariant to mark it as not to be used as
/// an assumption in other verification steps. This can be used for invariants which are
/// nonoperational constraints on system behavior, i.e. the systems "works" whether the
/// invariant holds or not. Invariant marked as such are not assumed when
/// memory is accessed, but only in the pre-state of a memory update.
pub const CONDITION_ISOLATED_PROP: &str = "isolated";
/// Abstract property which can be used together with an opaque specification. An abstract
/// property is not verified against the implementation, but will be used for the
/// function's behavior in the application context. This allows to "override" the specification
/// with a more abstract version. In general we would need to prove the abstraction is
/// subsumed by the implementation, but this is currently not done.
pub const CONDITION_ABSTRACT_PROP: &str = "abstract";
/// Opposite to the abstract property.
pub const CONDITION_CONCRETE_PROP: &str = "concrete";
/// Property which indicates that an aborts_if should be assumed.
/// For callers of a function with such an aborts_if, the negation of the condition becomes
/// an assumption.
pub const CONDITION_ABORT_ASSUME_PROP: &str = "assume";
/// Property which indicates that an aborts_if should be asserted.
/// For callers of a function with such an aborts_if, the negation of the condition becomes
/// an assertion.
pub const CONDITION_ABORT_ASSERT_PROP: &str = "assert";
/// A property which can be attached to any condition to exclude it from verification. The
/// condition will still be type checked.
pub const CONDITION_DEACTIVATED_PROP: &str = "deactivated";
/// A property which can be attached to an aborts_with to indicate that it should act as check
/// whether the function produces exactly the provided number of error codes.
pub const CONDITION_CHECK_ABORT_CODES_PROP: &str = "check";
/// A property that can be attached to a global invariant to indicate that it should be
/// enabled disabled by the disable_invariant_in_body pragma
pub const CONDITION_SUSPENDABLE_PROP: &str = "suspendable";
/// A function which determines whether a property is valid for a given condition kind.
pub fn is_property_valid_for_condition(kind: &ConditionKind, prop: &str) -> bool {
if matches!(
prop,
CONDITION_INJECTED_PROP
| CONDITION_EXPORT_PROP
| CONDITION_ABSTRACT_PROP
| CONDITION_CONCRETE_PROP
| CONDITION_DEACTIVATED_PROP
) {
// Applicable everywhere.
return true;
}
use crate::ast::ConditionKind::*;
match kind {
GlobalInvariant(..) | GlobalInvariantUpdate(..) => {
matches!(
prop,
CONDITION_GLOBAL_PROP | CONDITION_ISOLATED_PROP | CONDITION_SUSPENDABLE_PROP
)
}
SucceedsIf | AbortsIf => matches!(
prop,
CONDITION_ABORT_ASSERT_PROP | CONDITION_ABORT_ASSUME_PROP
),
AbortsWith => matches!(prop, CONDITION_CHECK_ABORT_CODES_PROP),
_ => {
// every other condition can only take general properties
false
}
}
}