From a9ea83d0bb3112c29da5f287d2eb75f6c86115f5 Mon Sep 17 00:00:00 2001 From: Wolfgang Grieskamp Date: Sun, 12 Oct 2025 21:32:16 -0700 Subject: [PATCH 1/2] [compiler & language] Support builtin constant `__COMPILE_FOR_TESTING__`. Allow code to branch over a compile time constant `__COMPILE_FOR_TESTING__`. The non-reachable branch will be optimized (or at least turned into dead code.) The name is under discussion. We should make the right decision here since any future compile time constants should be following this naming convention. I see compile constants as an equivalent to Rust attributes, at least if it comes to conditional compilation. This falls into the categorie of builtin constants which we already have for the spec llanguage. At the same time, we would enable `MAX_U64` et. all as builtin constants in the language. Builtin constants can be shadowed by the user, so no harm to existing move programs would be implied. --- .../tests/compile_for_testing_test.move | 7 ++++++ .../move/move-compiler-v2/src/experiments.rs | 8 +++++++ .../testing-constant/compile_for_testing.move | 8 +++++++ ...ile_for_testing.testing-constant-false.exp | 24 +++++++++++++++++++ ...pile_for_testing.testing-constant-true.exp | 23 ++++++++++++++++++ .../transactional-tests/tests/tests.rs | 21 ++++++++++++++++ third_party/move/move-model/src/ast.rs | 8 +++++++ .../move/move-model/src/builder/builtins.rs | 21 ++++++++++++++++ .../move-model/src/builder/exp_builder.rs | 7 ++++-- .../move-model/src/builder/model_builder.rs | 9 +++---- third_party/move/move-model/src/lib.rs | 1 + third_party/move/move-model/src/options.rs | 4 ++++ .../move/move-model/tests/testsuite.rs | 4 +--- .../src/framework.rs | 4 ++++ 14 files changed, 138 insertions(+), 11 deletions(-) create mode 100644 aptos-move/framework/move-stdlib/tests/compile_for_testing_test.move create mode 100644 third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.move create mode 100644 third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.testing-constant-false.exp create mode 100644 third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.testing-constant-true.exp diff --git a/aptos-move/framework/move-stdlib/tests/compile_for_testing_test.move b/aptos-move/framework/move-stdlib/tests/compile_for_testing_test.move new file mode 100644 index 0000000000000..163f0a76f4b67 --- /dev/null +++ b/aptos-move/framework/move-stdlib/tests/compile_for_testing_test.move @@ -0,0 +1,7 @@ +#[test_only] +module std::test_compile_for_testing { + #[test] + fun test() { + assert!(__COMPILE_FOR_TESTING__, 66); + } +} diff --git a/third_party/move/move-compiler-v2/src/experiments.rs b/third_party/move/move-compiler-v2/src/experiments.rs index 06712ca53df51..0fc6adf855a00 100644 --- a/third_party/move/move-compiler-v2/src/experiments.rs +++ b/third_party/move/move-compiler-v2/src/experiments.rs @@ -286,6 +286,13 @@ pub static EXPERIMENTS: Lazy> = Lazy::new(|| { .to_string(), default: Given(false), }, + Experiment { + name: Experiment::COMPILE_FOR_TESTING.to_string(), + description: "Compile for testing. If set, constant \ + `__COMPILE_FOR_TESTING__` will be true, otherwise false." + .to_string(), + default: Given(false), + }, ]; experiments .into_iter() @@ -305,6 +312,7 @@ impl Experiment { pub const CFG_SIMPLIFICATION: &'static str = "cfg-simplification"; pub const CHECKS: &'static str = "checks"; pub const CMP_REWRITE: &'static str = "cmp-rewrite"; + pub const COMPILE_FOR_TESTING: &'static str = "compile-for-testing"; pub const DEAD_CODE_ELIMINATION: &'static str = "dead-code-elimination"; pub const DUPLICATE_STRUCT_PARAMS_CHECK: &'static str = "duplicate-struct-params-check"; pub const FAIL_ON_WARNING: &'static str = "fail-on-warning"; diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.move b/third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.move new file mode 100644 index 0000000000000..81ef05543eb85 --- /dev/null +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.move @@ -0,0 +1,8 @@ +//# publish --print-bytecode +module 0x66::m { + fun run() { + if (__COMPILE_FOR_TESTING__) abort 1 else abort 2 + } +} + +//#run 0x66::m::run diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.testing-constant-false.exp b/third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.testing-constant-false.exp new file mode 100644 index 0000000000000..f06f777d61e5d --- /dev/null +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.testing-constant-false.exp @@ -0,0 +1,24 @@ +processed 2 tasks +task 0 lines 1-6: publish --print-bytecode [module 0x66::m {] + +== BEGIN Bytecode == +// Bytecode version v9 +module 0x66::m +// Function definition at index 0 +fun run() + branch l0 + ld_u64 1 + abort +l0: ld_u64 2 + abort + + +== END Bytecode == +task 1 lines 8-8: run 0x66::m::run +Error: Function execution failed with VMError: { + major_status: ABORTED, + sub_status: Some(2), + location: 0x66::m, + indices: [], + offsets: [(FunctionDefinitionIndex(0), 4)], +} diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.testing-constant-true.exp b/third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.testing-constant-true.exp new file mode 100644 index 0000000000000..b31dde99ee85d --- /dev/null +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/testing-constant/compile_for_testing.testing-constant-true.exp @@ -0,0 +1,23 @@ +processed 2 tasks +task 0 lines 1-6: publish --print-bytecode [module 0x66::m {] + +== BEGIN Bytecode == +// Bytecode version v9 +module 0x66::m +// Function definition at index 0 +fun run() + ld_u64 1 + abort + ld_u64 2 + abort + + +== END Bytecode == +task 1 lines 8-8: run 0x66::m::run +Error: Function execution failed with VMError: { + major_status: ABORTED, + sub_status: Some(1), + location: 0x66::m, + indices: [], + offsets: [(FunctionDefinitionIndex(0), 1)], +} diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/tests.rs b/third_party/move/move-compiler-v2/transactional-tests/tests/tests.rs index 3badb15dd2588..b3a0c226aa4eb 100644 --- a/third_party/move/move-compiler-v2/transactional-tests/tests/tests.rs +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/tests.rs @@ -39,6 +39,7 @@ const COMMON_EXCLUSIONS: &[&str] = &[ "/no-recursive-check/", "/no-access-check/", "/no-recursive-type-check/", + "/testing-constant/", ]; /// Note that any config which has different output for a test directory @@ -139,6 +140,24 @@ const TEST_CONFIGS: &[TestConfig] = &[ exclude: &[], cross_compile: false, }, + TestConfig { + name: "testing-constant-true", + runner: |p| run(p, get_config_by_name("testing-constant-true")), + experiments: &[(Experiment::COMPILE_FOR_TESTING, true)], + language_version: LanguageVersion::latest(), + include: &["/testing-constant/"], + exclude: &[], + cross_compile: false, + }, + TestConfig { + name: "testing-constant-false", + runner: |p| run(p, get_config_by_name("testing-constant-false")), + experiments: &[(Experiment::COMPILE_FOR_TESTING, false)], + language_version: LanguageVersion::latest(), + include: &["/testing-constant/"], + exclude: &[], + cross_compile: false, + }, ]; /// Test files which must use separate baselines because their result @@ -178,6 +197,8 @@ const SEPARATE_BASELINE: &[&str] = &[ "misc/bug_14817_extended.move", // run in verbose mode to unveil the exact error messages "/signed-int/", + // different expected result + "/testing-constant/", ]; fn get_config_by_name(name: &str) -> TestConfig { diff --git a/third_party/move/move-model/src/ast.rs b/third_party/move/move-model/src/ast.rs index 32fa3a6ab8fa1..d4e8b48222d61 100644 --- a/third_party/move/move-model/src/ast.rs +++ b/third_party/move/move-model/src/ast.rs @@ -3065,6 +3065,14 @@ impl ModuleName { ModuleName(addr, name) } + /// Returns builtin module name. + pub fn builtin_module(env: &GlobalEnv) -> Self { + Self::new( + Address::Numerical(AccountAddress::ZERO), + env.symbol_pool().make("$$"), + ) + } + pub fn from_address_bytes_and_name( addr: legacy_move_compiler::shared::NumericalAddress, name: Symbol, diff --git a/third_party/move/move-model/src/builder/builtins.rs b/third_party/move/move-model/src/builder/builtins.rs index a39b21b377237..5b7e9ed901528 100644 --- a/third_party/move/move-model/src/builder/builtins.rs +++ b/third_party/move/move-model/src/builder/builtins.rs @@ -9,6 +9,7 @@ use crate::{ builder::model_builder::{ConstEntry, EntryVisibility, ModelBuilder, SpecOrBuiltinFunEntry}, metadata::LanguageVersion, model::{Parameter, TypeParameter, TypeParameterKind}, + options::ModelBuilderOptions, ty::{Constraint, PrimitiveType, ReferenceKind, Type}, }; use legacy_move_compiler::parser::ast as PA; @@ -35,6 +36,11 @@ pub(crate) fn declare_builtins(trans: &mut ModelBuilder) { ) }; + let options = trans + .env + .get_extension::() + .unwrap_or_default(); + let param_t = &Type::TypeParameter(0); let param_t_decl = TypeParameter::new_named(&trans.env.symbol_pool().make("T"), &loc); @@ -45,6 +51,21 @@ pub(crate) fn declare_builtins(trans: &mut ModelBuilder) { visibility, }; + let mk_bool_const = |value: bool, visibility: EntryVisibility| ConstEntry { + loc: loc.clone(), + ty: bool_t.clone(), + value: Value::Bool(value), + visibility, + }; + + { + // Compiler builtin constants. + trans.define_const( + trans.builtin_qualified_symbol("__COMPILE_FOR_TESTING__"), + mk_bool_const(options.compile_for_testing, EntryVisibility::Impl), + ); + } + { // Builtin Constants (for specifications) use EntryVisibility::Spec; diff --git a/third_party/move/move-model/src/builder/exp_builder.rs b/third_party/move/move-model/src/builder/exp_builder.rs index 79d4e94658308..06a0e9177d672 100644 --- a/third_party/move/move-model/src/builder/exp_builder.rs +++ b/third_party/move/move-model/src/builder/exp_builder.rs @@ -3881,8 +3881,11 @@ impl ExpTranslator<'_, '_, '_> { context: &ErrorMessageContext, sym: &QualifiedSymbol, ) -> ExpData { - // Constants are always visible in specs. - if self.mode != ExpTranslationMode::Spec && sym.module_name != self.parent.module_name { + // Constants are always visible in specs. Builtin constants are visible everywhere. + if self.mode != ExpTranslationMode::Spec + && sym.module_name != self.parent.module_name + && sym.module_name != ModuleName::builtin_module(self.env()) + { self.error( loc, &format!( diff --git a/third_party/move/move-model/src/builder/model_builder.rs b/third_party/move/move-model/src/builder/model_builder.rs index ce00c2cec9396..43949615c4ea7 100644 --- a/third_party/move/move-model/src/builder/model_builder.rs +++ b/third_party/move/move-model/src/builder/model_builder.rs @@ -8,7 +8,7 @@ //! system, as well as type checking it and translating it to the spec language ast. use crate::{ - ast::{Address, Attribute, FriendDecl, ModuleName, Operation, QualifiedSymbol, Spec, Value}, + ast::{Attribute, FriendDecl, ModuleName, Operation, QualifiedSymbol, Spec, Value}, builder::builtins, intrinsics::IntrinsicDecl, model::{ @@ -23,7 +23,7 @@ use codespan_reporting::diagnostic::Severity; use itertools::Itertools; use legacy_move_compiler::{expansion::ast as EA, parser::ast as PA, shared::NumericalAddress}; use move_binary_format::file_format::Visibility; -use move_core_types::{ability::AbilitySet, account_address::AccountAddress}; +use move_core_types::ability::AbilitySet; use std::collections::{BTreeMap, BTreeSet}; /// A builder is used to enter a sequence of modules in acyclic dependency order into the model. The @@ -693,10 +693,7 @@ impl<'env> ModelBuilder<'env> { /// Returns the name for the pseudo builtin module. pub fn builtin_module(&self) -> ModuleName { - ModuleName::new( - Address::Numerical(AccountAddress::ZERO), - self.env.symbol_pool().make("$$"), - ) + ModuleName::builtin_module(self.env) } /// Adds a spec function to used_spec_funs set. diff --git a/third_party/move/move-model/src/lib.rs b/third_party/move/move-model/src/lib.rs index 9b8fc5bf25bad..e7c0fe016e2e6 100644 --- a/third_party/move/move-model/src/lib.rs +++ b/third_party/move/move-model/src/lib.rs @@ -96,6 +96,7 @@ pub fn run_model_builder_in_compiler_mode( deps.into_iter().map(to_package_paths).collect(), ModelBuilderOptions { language_version, + compile_for_testing: compile_test_code, ..ModelBuilderOptions::default() }, Flags::model_compilation() diff --git a/third_party/move/move-model/src/options.rs b/third_party/move/move-model/src/options.rs index ab5b217ecb9c8..bfafff58e38b9 100644 --- a/third_party/move/move-model/src/options.rs +++ b/third_party/move/move-model/src/options.rs @@ -19,4 +19,8 @@ pub struct ModelBuilderOptions { /// Ignore the "opaque" pragma on all function specs when possible. The opaque can be ignored /// as long as the function spec has no property marked as `[concrete]` or `[abstract]`. pub ignore_pragma_opaque_when_possible: bool, + + /// Whether to compiler for testing. This will be reflected in the builtin constant + /// `__COMPILE_FOR_TESTING__`. + pub compile_for_testing: bool, } diff --git a/third_party/move/move-model/tests/testsuite.rs b/third_party/move/move-model/tests/testsuite.rs index 2e087c28808e5..f009e0cede2b5 100644 --- a/third_party/move/move-model/tests/testsuite.rs +++ b/third_party/move/move-model/tests/testsuite.rs @@ -41,9 +41,7 @@ fn test_runner(path: &Path, options: ModelBuilderOptions) -> datatest_stable::Re } fn runner(path: &Path) -> datatest_stable::Result<()> { - test_runner(path, ModelBuilderOptions { - ..Default::default() - }) + test_runner(path, ModelBuilderOptions::default()) } datatest_stable::harness!(runner, "tests/sources", r".*\.move$"); diff --git a/third_party/move/testing-infra/transactional-test-runner/src/framework.rs b/third_party/move/testing-infra/transactional-test-runner/src/framework.rs index fbe5cd6d2de9b..3483e7970fbd3 100644 --- a/third_party/move/testing-infra/transactional-test-runner/src/framework.rs +++ b/third_party/move/testing-infra/transactional-test-runner/src/framework.rs @@ -32,6 +32,7 @@ use move_command_line_common::{ types::ParsedType, values::{ParsableValue, ParsedValue}, }; +use move_compiler_v2::Experiment; use move_core_types::{ account_address::AccountAddress, identifier::{IdentStr, Identifier}, @@ -946,6 +947,9 @@ fn compile_source_unit_v2( for (exp, value) in experiments { options = options.set_experiment(exp, value) } + if options.experiment_on(Experiment::COMPILE_FOR_TESTING) { + options.compile_test_code = true + } let mut error_writer = termcolor::Buffer::no_color(); let result = { let mut emitter = options.error_emitter(&mut error_writer); From d46acdbebcef98d7b7aeb7fc88215ca7e4ed0c87 Mon Sep 17 00:00:00 2001 From: Wolfgang Grieskamp Date: Tue, 14 Oct 2025 09:05:30 -0700 Subject: [PATCH 2/2] Fully support MIN/MAX for all integer types. Also move unit test out of framework, because it may not compile with older compilers. --- .../tests/compile_for_testing_test.move | 7 - .../tests/constants/builtin_constants.exp | 6 + .../tests/constants/builtin_constants.move | 45 +++++ .../round-trip/builtin_constants.decompiled | 26 +++ .../builtin_constants.decompiled.baseline.exp | 6 + .../move/move-model/src/builder/builtins.rs | 167 ++++++++++++++++-- 6 files changed, 235 insertions(+), 22 deletions(-) delete mode 100644 aptos-move/framework/move-stdlib/tests/compile_for_testing_test.move create mode 100644 third_party/move/move-compiler-v2/transactional-tests/tests/constants/builtin_constants.exp create mode 100644 third_party/move/move-compiler-v2/transactional-tests/tests/constants/builtin_constants.move create mode 100644 third_party/move/move-compiler-v2/transactional-tests/tests/constants/round-trip/builtin_constants.decompiled create mode 100644 third_party/move/move-compiler-v2/transactional-tests/tests/constants/round-trip/builtin_constants.decompiled.baseline.exp diff --git a/aptos-move/framework/move-stdlib/tests/compile_for_testing_test.move b/aptos-move/framework/move-stdlib/tests/compile_for_testing_test.move deleted file mode 100644 index 163f0a76f4b67..0000000000000 --- a/aptos-move/framework/move-stdlib/tests/compile_for_testing_test.move +++ /dev/null @@ -1,7 +0,0 @@ -#[test_only] -module std::test_compile_for_testing { - #[test] - fun test() { - assert!(__COMPILE_FOR_TESTING__, 66); - } -} diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/constants/builtin_constants.exp b/third_party/move/move-compiler-v2/transactional-tests/tests/constants/builtin_constants.exp new file mode 100644 index 0000000000000..a21bb5fd207e8 --- /dev/null +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/constants/builtin_constants.exp @@ -0,0 +1,6 @@ +processed 5 tasks +task 0 lines 1-30: publish [module 0x66::m {] +task 1 lines 32-32: run 0x66::m::compile_for_testing +task 2 lines 34-34: run 0x66::m::min_max +task 3 lines 36-43: publish [module 0x66::shadow {] +task 4 lines 45-45: run 0x66::shadow::shadowed diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/constants/builtin_constants.move b/third_party/move/move-compiler-v2/transactional-tests/tests/constants/builtin_constants.move new file mode 100644 index 0000000000000..ebaac2e72883e --- /dev/null +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/constants/builtin_constants.move @@ -0,0 +1,45 @@ +//# publish +module 0x66::m { + fun compile_for_testing() { + // We are NOT compiling for testing, so expect this to be false. See independent + // compile_for_testing test. + assert!(!__COMPILE_FOR_TESTING__, 66); + } + + fun min_max() { + assert!(MAX_U8 == 255, 1); + assert!(MAX_U16 == 65535, 1); + assert!(MAX_U32 == 4294967295, 1); + assert!(MAX_U64 == 18446744073709551615, 1); + assert!(MAX_U128 == 340282366920938463463374607431768211455, 1); + assert!(MAX_U256 == 115792089237316195423570985008687907853269984665640564039457584007913129639935, 1); + + assert!(MIN_I8 == -128, 1); + assert!(MAX_I8 == 127, 1); + assert!(MIN_I16 == -32768, 1); + assert!(MAX_I16 == 32767, 1); + assert!(MIN_I32 == -2147483648, 1); + assert!(MAX_I32 == 2147483647, 1); + assert!(MIN_I64 == -9223372036854775808, 1); + assert!(MAX_I64 == 9223372036854775807, 1); + assert!(MIN_I128 == -170141183460469231731687303715884105728, 1); + assert!(MAX_I128 == 170141183460469231731687303715884105727, 1); + assert!(MIN_I256 == -57896044618658097711785492504343953926634992332820282019728792003956564819968, 1); + assert!(MAX_I256 == 57896044618658097711785492504343953926634992332820282019728792003956564819967, 1); + } +} + +//# run 0x66::m::compile_for_testing + +//# run 0x66::m::min_max + +//# publish +module 0x66::shadow { + const MAX_U8: bool = false; + + fun shadowed() { + assert!(!MAX_U8, 66); + } +} + +//# run 0x66::shadow::shadowed diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/constants/round-trip/builtin_constants.decompiled b/third_party/move/move-compiler-v2/transactional-tests/tests/constants/round-trip/builtin_constants.decompiled new file mode 100644 index 0000000000000..e91eff8706d88 --- /dev/null +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/constants/round-trip/builtin_constants.decompiled @@ -0,0 +1,26 @@ +//**** Cross-compiled for `move` syntax from `tests/constants/builtin_constants.move` + +//# publish +module 0x66::m { + fun compile_for_testing() { + () + } + fun min_max() { + () + } +} + + +//# run 0x66::m::compile_for_testing + +//# run 0x66::m::min_max + +//# publish +module 0x66::shadow { + fun shadowed() { + () + } +} + + +//# run 0x66::shadow::shadowed \ No newline at end of file diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/constants/round-trip/builtin_constants.decompiled.baseline.exp b/third_party/move/move-compiler-v2/transactional-tests/tests/constants/round-trip/builtin_constants.decompiled.baseline.exp new file mode 100644 index 0000000000000..61fc61d75c521 --- /dev/null +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/constants/round-trip/builtin_constants.decompiled.baseline.exp @@ -0,0 +1,6 @@ +processed 5 tasks +task 0 lines 3-11: publish [module 0x66::m {] +task 1 lines 14-14: run 0x66::m::compile_for_testing +task 2 lines 16-16: run 0x66::m::min_max +task 3 lines 18-23: publish [module 0x66::shadow {] +task 4 lines 26-26: run 0x66::shadow::shadowed diff --git a/third_party/move/move-model/src/builder/builtins.rs b/third_party/move/move-model/src/builder/builtins.rs index 5b7e9ed901528..0946c0e265157 100644 --- a/third_party/move/move-model/src/builder/builtins.rs +++ b/third_party/move/move-model/src/builder/builtins.rs @@ -15,7 +15,7 @@ use crate::{ use legacy_move_compiler::parser::ast as PA; use move_core_types::{ ability::{Ability, AbilitySet}, - int256::U256, + int256::{I256, U256}, }; use num::BigInt; use std::collections::BTreeMap; @@ -23,6 +23,7 @@ use std::collections::BTreeMap; /// Adds builtin functions. pub(crate) fn declare_builtins(trans: &mut ModelBuilder) { let loc = trans.env.internal_loc(); + let prim_ty = |p| Type::new_prim(p); let bool_t = &Type::new_prim(PrimitiveType::Bool); let num_t = &Type::new_prim(PrimitiveType::Num); let range_t = &Type::new_prim(PrimitiveType::Range); @@ -44,13 +45,16 @@ pub(crate) fn declare_builtins(trans: &mut ModelBuilder) { let param_t = &Type::TypeParameter(0); let param_t_decl = TypeParameter::new_named(&trans.env.symbol_pool().make("T"), &loc); - let mk_num_const = |value: BigInt, visibility: EntryVisibility| ConstEntry { + let mk_int_const = |value: BigInt, ty: &Type, visibility: EntryVisibility| ConstEntry { loc: loc.clone(), - ty: num_t.clone(), + ty: ty.clone(), value: Value::Number(value), visibility, }; + let mk_num_const = + |value: BigInt, visibility: EntryVisibility| mk_int_const(value, num_t, visibility); + let mk_bool_const = |value: bool, visibility: EntryVisibility| ConstEntry { loc: loc.clone(), ty: bool_t.clone(), @@ -59,40 +63,173 @@ pub(crate) fn declare_builtins(trans: &mut ModelBuilder) { }; { - // Compiler builtin constants. - trans.define_const( - trans.builtin_qualified_symbol("__COMPILE_FOR_TESTING__"), - mk_bool_const(options.compile_for_testing, EntryVisibility::Impl), - ); + if options.language_version.is_at_least(LanguageVersion::V2_3) { + use EntryVisibility::SpecAndImpl; + // Compiler builtin constants. + trans.define_const( + trans.builtin_qualified_symbol("__COMPILE_FOR_TESTING__"), + mk_bool_const(options.compile_for_testing, SpecAndImpl), + ); + } } { + use EntryVisibility::{Spec, SpecAndImpl}; + + let range_visibility = if options.language_version.is_at_least(LanguageVersion::V2_3) { + SpecAndImpl + } else { + Spec + }; + // Builtin Constants (for specifications) - use EntryVisibility::Spec; trans.define_const( trans.builtin_qualified_symbol("MAX_U8"), - mk_num_const(BigInt::from(u8::MAX), Spec), + mk_int_const( + BigInt::from(u8::MAX), + &prim_ty(PrimitiveType::U8), + range_visibility, + ), ); trans.define_const( trans.builtin_qualified_symbol("MAX_U16"), - mk_num_const(BigInt::from(u16::MAX), Spec), + mk_int_const( + BigInt::from(u16::MAX), + &prim_ty(PrimitiveType::U16), + range_visibility, + ), ); trans.define_const( trans.builtin_qualified_symbol("MAX_U32"), - mk_num_const(BigInt::from(u32::MAX), Spec), + mk_int_const( + BigInt::from(u32::MAX), + &prim_ty(PrimitiveType::U32), + range_visibility, + ), ); trans.define_const( trans.builtin_qualified_symbol("MAX_U64"), - mk_num_const(BigInt::from(u64::MAX), Spec), + mk_int_const( + BigInt::from(u64::MAX), + &prim_ty(PrimitiveType::U64), + range_visibility, + ), ); trans.define_const( trans.builtin_qualified_symbol("MAX_U128"), - mk_num_const(BigInt::from(u128::MAX), Spec), + mk_int_const( + BigInt::from(u128::MAX), + &prim_ty(PrimitiveType::U128), + range_visibility, + ), ); trans.define_const( trans.builtin_qualified_symbol("MAX_U256"), - mk_num_const(BigInt::from(U256::MAX), Spec), + mk_int_const( + BigInt::from(U256::MAX), + &prim_ty(PrimitiveType::U256), + range_visibility, + ), + ); + + trans.define_const( + trans.builtin_qualified_symbol("MAX_I8"), + mk_int_const( + BigInt::from(i8::MAX), + &prim_ty(PrimitiveType::I8), + range_visibility, + ), + ); + trans.define_const( + trans.builtin_qualified_symbol("MAX_I16"), + mk_int_const( + BigInt::from(i16::MAX), + &prim_ty(PrimitiveType::I16), + range_visibility, + ), + ); + trans.define_const( + trans.builtin_qualified_symbol("MAX_I32"), + mk_int_const( + BigInt::from(i32::MAX), + &prim_ty(PrimitiveType::I32), + range_visibility, + ), + ); + trans.define_const( + trans.builtin_qualified_symbol("MAX_I64"), + mk_int_const( + BigInt::from(i64::MAX), + &prim_ty(PrimitiveType::I64), + range_visibility, + ), ); + trans.define_const( + trans.builtin_qualified_symbol("MAX_I128"), + mk_int_const( + BigInt::from(i128::MAX), + &prim_ty(PrimitiveType::I128), + range_visibility, + ), + ); + trans.define_const( + trans.builtin_qualified_symbol("MAX_I256"), + mk_int_const( + BigInt::from(I256::MAX), + &prim_ty(PrimitiveType::I256), + range_visibility, + ), + ); + + trans.define_const( + trans.builtin_qualified_symbol("MIN_I8"), + mk_int_const( + BigInt::from(i8::MIN), + &prim_ty(PrimitiveType::I8), + range_visibility, + ), + ); + trans.define_const( + trans.builtin_qualified_symbol("MIN_I16"), + mk_int_const( + BigInt::from(i16::MIN), + &prim_ty(PrimitiveType::I16), + range_visibility, + ), + ); + trans.define_const( + trans.builtin_qualified_symbol("MIN_I32"), + mk_int_const( + BigInt::from(i32::MIN), + &prim_ty(PrimitiveType::I32), + range_visibility, + ), + ); + trans.define_const( + trans.builtin_qualified_symbol("MIN_I64"), + mk_int_const( + BigInt::from(i64::MIN), + &prim_ty(PrimitiveType::I64), + range_visibility, + ), + ); + trans.define_const( + trans.builtin_qualified_symbol("MIN_I128"), + mk_int_const( + BigInt::from(i128::MIN), + &prim_ty(PrimitiveType::I128), + range_visibility, + ), + ); + trans.define_const( + trans.builtin_qualified_symbol("MIN_I256"), + mk_int_const( + BigInt::from(I256::MIN), + &prim_ty(PrimitiveType::I256), + range_visibility, + ), + ); + trans.define_const( trans.builtin_qualified_symbol("EXECUTION_FAILURE"), mk_num_const(BigInt::from(-1), Spec),