Skip to content

Commit 4757c65

Browse files
junxzm1990junxzm1990
committed
[Move Prover] add signed int support
1 parent 37febd6 commit 4757c65

File tree

19 files changed

+1654
-708
lines changed

19 files changed

+1654
-708
lines changed

‎third_party/move/move-model/src/builder/builtins.rs‎

Lines changed: 54 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ use crate::{
1414
use legacy_move_compiler::parser::ast as PA;
1515
use move_core_types::{
1616
ability::{Ability, AbilitySet},
17-
int256::U256,
17+
int256::{I256, U256},
1818
};
1919
use num::BigInt;
2020
use std::collections::BTreeMap;
@@ -48,6 +48,8 @@ pub(crate) fn declare_builtins(trans: &mut ModelBuilder) {
4848
{
4949
// Builtin Constants (for specifications)
5050
use EntryVisibility::Spec;
51+
52+
// Unsigned integers
5153
trans.define_const(
5254
trans.builtin_qualified_symbol("MAX_U8"),
5355
mk_num_const(BigInt::from(u8::MAX), Spec),
@@ -72,6 +74,57 @@ pub(crate) fn declare_builtins(trans: &mut ModelBuilder) {
7274
trans.builtin_qualified_symbol("MAX_U256"),
7375
mk_num_const(BigInt::from(U256::MAX), Spec),
7476
);
77+
78+
// Signed integers
79+
trans.define_const(
80+
trans.builtin_qualified_symbol("MAX_I8"),
81+
mk_num_const(BigInt::from(i8::MAX), Spec),
82+
);
83+
trans.define_const(
84+
trans.builtin_qualified_symbol("MIN_I8"),
85+
mk_num_const(BigInt::from(i8::MIN), Spec),
86+
);
87+
trans.define_const(
88+
trans.builtin_qualified_symbol("MAX_I16"),
89+
mk_num_const(BigInt::from(i16::MAX), Spec),
90+
);
91+
trans.define_const(
92+
trans.builtin_qualified_symbol("MIN_I16"),
93+
mk_num_const(BigInt::from(i16::MIN), Spec),
94+
);
95+
trans.define_const(
96+
trans.builtin_qualified_symbol("MAX_I32"),
97+
mk_num_const(BigInt::from(i32::MAX), Spec),
98+
);
99+
trans.define_const(
100+
trans.builtin_qualified_symbol("MIN_I32"),
101+
mk_num_const(BigInt::from(i32::MIN), Spec),
102+
);
103+
trans.define_const(
104+
trans.builtin_qualified_symbol("MAX_I64"),
105+
mk_num_const(BigInt::from(i64::MAX), Spec),
106+
);
107+
trans.define_const(
108+
trans.builtin_qualified_symbol("MIN_I64"),
109+
mk_num_const(BigInt::from(i64::MIN), Spec),
110+
);
111+
trans.define_const(
112+
trans.builtin_qualified_symbol("MAX_I128"),
113+
mk_num_const(BigInt::from(i128::MAX), Spec),
114+
);
115+
trans.define_const(
116+
trans.builtin_qualified_symbol("MIN_I128"),
117+
mk_num_const(BigInt::from(i128::MIN), Spec),
118+
);
119+
trans.define_const(
120+
trans.builtin_qualified_symbol("MAX_I256"),
121+
mk_num_const(BigInt::from(I256::MAX), Spec),
122+
);
123+
trans.define_const(
124+
trans.builtin_qualified_symbol("MIN_I256"),
125+
mk_num_const(BigInt::from(I256::MIN), Spec),
126+
);
127+
75128
trans.define_const(
76129
trans.builtin_qualified_symbol("EXECUTION_FAILURE"),
77130
mk_num_const(BigInt::from(-1), Spec),

‎third_party/move/move-model/src/builder/exp_builder.rs‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ use move_ir_types::{
4444
location::{sp, Spanned},
4545
sp,
4646
};
47-
use num::{BigInt, FromPrimitive};
47+
use num::{BigInt, FromPrimitive, Zero};
4848
use std::{
4949
cell::RefCell,
5050
collections::{BTreeMap, BTreeSet, LinkedList},
@@ -3193,8 +3193,12 @@ impl ExpTranslator<'_, '_, '_> {
31933193
_ => unreachable!("not primitive"),
31943194
}
31953195
} else if self.is_spec_mode() {
3196-
// In specification mode, use U256.
3197-
vec![PrimitiveType::U256]
3196+
// In specification mode, use I256 or U256.
3197+
if value < BigInt::zero() {
3198+
vec![PrimitiveType::I256]
3199+
} else {
3200+
vec![PrimitiveType::U256]
3201+
}
31983202
} else {
31993203
// Infer the possible types from the value
32003204
PrimitiveType::possible_int_types(value.clone())

‎third_party/move/move-model/src/ty.rs‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1257,6 +1257,36 @@ impl Type {
12571257
false
12581258
}
12591259

1260+
/// Returns true if this is signed int type.
1261+
pub fn is_signed_int(&self) -> bool {
1262+
matches!(
1263+
self,
1264+
Type::Primitive(
1265+
PrimitiveType::I8
1266+
| PrimitiveType::I16
1267+
| PrimitiveType::I32
1268+
| PrimitiveType::I64
1269+
| PrimitiveType::I128
1270+
| PrimitiveType::I256
1271+
)
1272+
)
1273+
}
1274+
1275+
/// Returns true if this is unsigned int type.
1276+
pub fn is_unsigned_int(&self) -> bool {
1277+
matches!(
1278+
self,
1279+
Type::Primitive(
1280+
PrimitiveType::U8
1281+
| PrimitiveType::U16
1282+
| PrimitiveType::U32
1283+
| PrimitiveType::U64
1284+
| PrimitiveType::U128
1285+
| PrimitiveType::U256
1286+
)
1287+
)
1288+
}
1289+
12601290
/// Returns compatible number type if `self` and `ty` are compatible number types.
12611291
pub fn is_compatible_num_type(&self, ty: &Type) -> Option<Type> {
12621292
let skip_reference_self = self.skip_reference();

‎third_party/move/move-prover/boogie-backend/src/boogie_helpers.rs‎

Lines changed: 51 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ pub const MAX_MAKE_VEC_ARGS: usize = 4;
3434
pub const TABLE_NATIVE_SPEC_ERROR: &str =
3535
"Native functions defined in Table cannot be used as specification functions";
3636
const NUM_TYPE_BASE_ERROR: &str = "cannot infer concrete integer type from `num`, consider using a concrete integer type or explicit type cast";
37+
pub const BITWISE_NOT_ENABLED_ERROR: &str = "bitwise operations not enabled for this type";
3738

3839
/// Return boogie name of given module.
3940
pub fn boogie_module_name(env: &ModuleEnv<'_>) -> String {
@@ -338,14 +339,11 @@ pub fn boogie_type(env: &GlobalEnv, ty: &Type) -> String {
338339
use Type::*;
339340
match ty {
340341
Primitive(p) => match p {
341-
U8 | U16 | U32 | U64 | U128 | U256 | Num | Address => "int".to_string(),
342+
U8 | U16 | U32 | U64 | U128 | U256 | I8 | I16 | I32 | I64 | I128 | I256 | Num
343+
| Address => "int".to_string(),
342344
Signer => "$signer".to_string(),
343345
Bool => "bool".to_string(),
344346
Range | EventStore => panic!("unexpected type"),
345-
I8 | I16 | I32 | I64 | I128 | I256 => {
346-
// TODO(#17645): add support
347-
unimplemented!("signed integer not supported");
348-
},
349347
},
350348
Vector(et) => format!("Vec ({})", boogie_type(env, et)),
351349
Struct(mid, sid, inst) => boogie_struct_name(&env.get_module(*mid).into_struct(*sid), inst),
@@ -389,6 +387,7 @@ pub fn boogie_bv_type(env: &GlobalEnv, ty: &Type) -> String {
389387
U64 => "bv64".to_string(),
390388
U128 => "bv128".to_string(),
391389
U256 => "bv256".to_string(),
390+
I8 | I16 | I32 | I64 | I128 | I256 => unreachable!("{}", BITWISE_NOT_ENABLED_ERROR),
392391
Address => "int".to_string(),
393392
Signer => "$signer".to_string(),
394393
Bool => "bool".to_string(),
@@ -397,10 +396,6 @@ pub fn boogie_bv_type(env: &GlobalEnv, ty: &Type) -> String {
397396
//TODO(tengzhang): add error message with accurate location info
398397
"<<num is not unsupported here>>".to_string()
399398
},
400-
I8 | I16 | I32 | I64 | I128 | I256 => {
401-
// TODO(#17645): add support
402-
unimplemented!("signed integer not supported")
403-
},
404399
},
405400
Vector(et) => format!("Vec ({})", boogie_bv_type(env, et)),
406401
Struct(mid, sid, inst) => {
@@ -424,6 +419,14 @@ pub fn boogie_num_type_base_bv(env: &GlobalEnv, loc: Option<Loc>, ty: &Type) ->
424419
Type::Primitive(PrimitiveType::U64) => "Bv64",
425420
Type::Primitive(PrimitiveType::U128) => "Bv128",
426421
Type::Primitive(PrimitiveType::U256) => "Bv256",
422+
Type::Primitive(PrimitiveType::I8)
423+
| Type::Primitive(PrimitiveType::I16)
424+
| Type::Primitive(PrimitiveType::I32)
425+
| Type::Primitive(PrimitiveType::I64)
426+
| Type::Primitive(PrimitiveType::I128)
427+
| Type::Primitive(PrimitiveType::I256) => {
428+
unreachable!("{}", BITWISE_NOT_ENABLED_ERROR);
429+
},
427430
Type::Primitive(PrimitiveType::Num) => {
428431
env.error(&loc.unwrap_or_default(), NUM_TYPE_BASE_ERROR);
429432
"<<num is not unsupported here>>"
@@ -454,13 +457,13 @@ pub fn boogie_num_literal(num: &String, base: usize, bv_flag: bool) -> String {
454457
}
455458
}
456459

457-
pub fn boogie_num_type_string(num: &str, bv_flag: bool) -> String {
458-
let pre = if bv_flag { "bv" } else { "u" };
460+
pub fn boogie_num_type_string(kind: &str, num: &str, bv_flag: bool) -> String {
461+
let pre = if bv_flag { "bv" } else { kind };
459462
[pre, num].join("")
460463
}
461464

462-
pub fn boogie_num_type_string_capital(num: &str, bv_flag: bool) -> String {
463-
let pre = if bv_flag { "Bv" } else { "U" };
465+
pub fn boogie_num_type_string_capital(kind: &str, num: &str, bv_flag: bool) -> String {
466+
let pre = if bv_flag { "Bv" } else { kind };
464467
[pre, num].join("")
465468
}
466469

@@ -475,6 +478,9 @@ pub fn boogie_num_type_base(env: &GlobalEnv, loc: Option<Loc>, ty: &Type) -> Str
475478
U64 => "64".to_string(),
476479
U128 => "128".to_string(),
477480
U256 => "256".to_string(),
481+
I8 | I16 | I32 | I64 | I128 | I256 => {
482+
unreachable!("{}", BITWISE_NOT_ENABLED_ERROR);
483+
},
478484
Num => {
479485
env.error(&loc.unwrap_or_default(), NUM_TYPE_BASE_ERROR);
480486
"<<num is not unsupported here>>".to_string()
@@ -492,12 +498,18 @@ pub fn boogie_type_suffix_bv(env: &GlobalEnv, ty: &Type, bv_flag: bool) -> Strin
492498

493499
match ty {
494500
Primitive(p) => match p {
495-
U8 => boogie_num_type_string("8", bv_flag),
496-
U16 => boogie_num_type_string("16", bv_flag),
497-
U32 => boogie_num_type_string("32", bv_flag),
498-
U64 => boogie_num_type_string("64", bv_flag),
499-
U128 => boogie_num_type_string("128", bv_flag),
500-
U256 => boogie_num_type_string("256", bv_flag),
501+
U8 => boogie_num_type_string("u", "8", bv_flag),
502+
U16 => boogie_num_type_string("u", "16", bv_flag),
503+
U32 => boogie_num_type_string("u", "32", bv_flag),
504+
U64 => boogie_num_type_string("u", "64", bv_flag),
505+
U128 => boogie_num_type_string("u", "128", bv_flag),
506+
U256 => boogie_num_type_string("u", "256", bv_flag),
507+
I8 => boogie_num_type_string("i", "8", bv_flag),
508+
I16 => boogie_num_type_string("i", "16", bv_flag),
509+
I32 => boogie_num_type_string("i", "32", bv_flag),
510+
I64 => boogie_num_type_string("i", "64", bv_flag),
511+
I128 => boogie_num_type_string("i", "128", bv_flag),
512+
I256 => boogie_num_type_string("i", "256", bv_flag),
501513
Num => {
502514
if bv_flag {
503515
//TODO(tengzhang): add error message with accurate location info
@@ -511,10 +523,6 @@ pub fn boogie_type_suffix_bv(env: &GlobalEnv, ty: &Type, bv_flag: bool) -> Strin
511523
Bool => "bool".to_string(),
512524
Range => "range".to_string(),
513525
EventStore => format!("<<unsupported {:?}>>", ty),
514-
I8 | I16 | I32 | I64 | I128 | I256 => {
515-
// TODO(#17645): add support
516-
unimplemented!("signed integer not supported")
517-
},
518526
},
519527
Vector(et) => format!(
520528
"vec{}",
@@ -704,9 +712,17 @@ pub fn boogie_constant(env: &GlobalEnv, _options: &BoogieOptions, val: &Constant
704712
Constant::Bool(true) => "true".to_string(),
705713
Constant::Bool(false) => "false".to_string(),
706714
Constant::U8(num) => num.to_string(),
715+
Constant::U16(num) => num.to_string(),
716+
Constant::U32(num) => num.to_string(),
707717
Constant::U64(num) => num.to_string(),
708718
Constant::U128(num) => num.to_string(),
709719
Constant::U256(num) => num.to_string(),
720+
Constant::I8(num) => num.to_string(),
721+
Constant::I16(num) => num.to_string(),
722+
Constant::I32(num) => num.to_string(),
723+
Constant::I64(num) => num.to_string(),
724+
Constant::I128(num) => num.to_string(),
725+
Constant::I256(num) => num.to_string(),
710726
Constant::Address(v) => boogie_address(env, v),
711727
Constant::ByteArray(v) => boogie_byte_blob(_options, v, false),
712728
Constant::AddressArray(v) => boogie_address_blob(env, _options, v),
@@ -715,17 +731,6 @@ pub fn boogie_constant(env: &GlobalEnv, _options: &BoogieOptions, val: &Constant
715731
.map(|v| boogie_constant(env, _options, v))
716732
.collect_vec(),
717733
),
718-
Constant::U16(num) => num.to_string(),
719-
Constant::U32(num) => num.to_string(),
720-
Constant::I8(_)
721-
| Constant::I16(_)
722-
| Constant::I32(_)
723-
| Constant::I64(_)
724-
| Constant::I128(_)
725-
| Constant::I256(_) => {
726-
// TODO(#17645): add support
727-
unimplemented!("signed integer not supported")
728-
},
729734
}
730735
}
731736

@@ -967,6 +972,12 @@ fn type_name_to_ident_tokens(
967972
Type::Primitive(PrimitiveType::U64) => TypeIdentToken::make("u64"),
968973
Type::Primitive(PrimitiveType::U128) => TypeIdentToken::make("u128"),
969974
Type::Primitive(PrimitiveType::U256) => TypeIdentToken::make("u256"),
975+
Type::Primitive(PrimitiveType::I8) => TypeIdentToken::make("i8"),
976+
Type::Primitive(PrimitiveType::I16) => TypeIdentToken::make("i16"),
977+
Type::Primitive(PrimitiveType::I32) => TypeIdentToken::make("i32"),
978+
Type::Primitive(PrimitiveType::I64) => TypeIdentToken::make("i64"),
979+
Type::Primitive(PrimitiveType::I128) => TypeIdentToken::make("i128"),
980+
Type::Primitive(PrimitiveType::I256) => TypeIdentToken::make("i256"),
970981
Type::Primitive(PrimitiveType::Address) => TypeIdentToken::make("address"),
971982
Type::Primitive(PrimitiveType::Signer) => TypeIdentToken::make("signer"),
972983
Type::Vector(element) => {
@@ -1022,15 +1033,6 @@ fn type_name_to_ident_tokens(
10221033
Type::Error | Type::Var(..) => {
10231034
unreachable!("Unexpected temporary type in type_name call");
10241035
},
1025-
Type::Primitive(PrimitiveType::I8)
1026-
| Type::Primitive(PrimitiveType::I16)
1027-
| Type::Primitive(PrimitiveType::I32)
1028-
| Type::Primitive(PrimitiveType::I64)
1029-
| Type::Primitive(PrimitiveType::I128)
1030-
| Type::Primitive(PrimitiveType::I256) => {
1031-
// TODO(#17645): add support
1032-
unimplemented!("signed integer not supported")
1033-
},
10341036
}
10351037
}
10361038

@@ -1103,6 +1105,12 @@ fn type_name_to_info_pack(env: &GlobalEnv, ty: &Type) -> Option<TypeInfoPack> {
11031105
| Type::Primitive(PrimitiveType::U64)
11041106
| Type::Primitive(PrimitiveType::U128)
11051107
| Type::Primitive(PrimitiveType::U256)
1108+
| Type::Primitive(PrimitiveType::I8)
1109+
| Type::Primitive(PrimitiveType::I16)
1110+
| Type::Primitive(PrimitiveType::I32)
1111+
| Type::Primitive(PrimitiveType::I64)
1112+
| Type::Primitive(PrimitiveType::I128)
1113+
| Type::Primitive(PrimitiveType::I256)
11061114
| Type::Primitive(PrimitiveType::Address)
11071115
| Type::Primitive(PrimitiveType::Signer)
11081116
| Type::Vector(_) => None,
@@ -1123,15 +1131,6 @@ fn type_name_to_info_pack(env: &GlobalEnv, ty: &Type) -> Option<TypeInfoPack> {
11231131
Type::Error | Type::Var(..) => {
11241132
unreachable!("Unexpected temporary type in type_name call");
11251133
},
1126-
Type::Primitive(PrimitiveType::I8)
1127-
| Type::Primitive(PrimitiveType::I16)
1128-
| Type::Primitive(PrimitiveType::I32)
1129-
| Type::Primitive(PrimitiveType::I64)
1130-
| Type::Primitive(PrimitiveType::I128)
1131-
| Type::Primitive(PrimitiveType::I256) => {
1132-
// TODO(#17645): add support
1133-
unimplemented!("signed integer not supported")
1134-
},
11351134
}
11361135
}
11371136

0 commit comments

Comments
 (0)