Skip to content

Commit 8454749

Browse files
rahxephon89rahxephon89
authored
[Prover] code refactor for bitwise operation analysis (aptos-labs#16785)
* improve error message * refactor code
1 parent 03fe57e commit 8454749

File tree

14 files changed

+445
-420
lines changed

14 files changed

+445
-420
lines changed

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

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1103,6 +1103,29 @@ impl Type {
11031103
false
11041104
}
11051105

1106+
/// Returns compatible number type if `self` and `ty` are compatible number types.
1107+
pub fn is_compatible_num_type(&self, ty: &Type) -> Option<Type> {
1108+
let skip_reference_self = self.skip_reference();
1109+
let skip_reference_ty = ty.skip_reference();
1110+
if !skip_reference_self.is_number() || !skip_reference_ty.is_number() {
1111+
return None;
1112+
}
1113+
match (skip_reference_self, skip_reference_ty) {
1114+
(Type::Primitive(PrimitiveType::Num), Type::Primitive(PrimitiveType::Num)) => {
1115+
Some(Type::Primitive(PrimitiveType::Num))
1116+
},
1117+
(Type::Primitive(PrimitiveType::Num), _) => Some(skip_reference_ty.clone()),
1118+
(_, Type::Primitive(PrimitiveType::Num)) => Some(skip_reference_self.clone()),
1119+
_ => {
1120+
if skip_reference_self == skip_reference_ty {
1121+
Some(skip_reference_self.clone())
1122+
} else {
1123+
None
1124+
}
1125+
},
1126+
}
1127+
}
1128+
11061129
/// Returns true if this is an address or signer type.
11071130
pub fn is_signer_or_address(&self) -> bool {
11081131
matches!(

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

Lines changed: 30 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ use move_core_types::account_address::AccountAddress;
1313
use move_model::{
1414
ast::{Address, MemoryLabel, TempIndex, Value},
1515
model::{
16-
FieldEnv, FieldId, FunctionEnv, GlobalEnv, ModuleEnv, QualifiedInstId, SpecFunId,
16+
FieldEnv, FieldId, FunctionEnv, GlobalEnv, Loc, ModuleEnv, QualifiedInstId, SpecFunId,
1717
StructEnv, StructId, SCRIPT_MODULE_NAME,
1818
},
1919
pragmas::INTRINSIC_TYPE_MAP,
@@ -29,6 +29,7 @@ use num::BigUint;
2929
pub const MAX_MAKE_VEC_ARGS: usize = 4;
3030
pub const TABLE_NATIVE_SPEC_ERROR: &str =
3131
"Native functions defined in Table cannot be used as specification functions";
32+
const NUM_TYPE_BASE_ERROR: &str = "cannot infer concrete integer type from `num`, consider using a concrete integer type or explicit type cast";
3233

3334
/// Return boogie name of given module.
3435
pub fn boogie_module_name(env: &ModuleEnv<'_>) -> String {
@@ -347,7 +348,10 @@ pub fn boogie_bv_type(env: &GlobalEnv, ty: &Type) -> String {
347348
Signer => "$signer".to_string(),
348349
Bool => "bool".to_string(),
349350
Range | EventStore => panic!("unexpected type"),
350-
Num => "<<num is not unsupported here>>".to_string(),
351+
Num => {
352+
//TODO(tengzhang): add error message with accurate location info
353+
"<<num is not unsupported here>>".to_string()
354+
},
351355
},
352356
Vector(et) => format!("Vec ({})", boogie_bv_type(env, et)),
353357
Struct(mid, sid, inst) => {
@@ -361,6 +365,24 @@ pub fn boogie_bv_type(env: &GlobalEnv, ty: &Type) -> String {
361365
}
362366
}
363367

368+
/// Return boogie BV type for a number type.
369+
pub fn boogie_num_type_base_bv(env: &GlobalEnv, loc: Option<Loc>, ty: &Type) -> String {
370+
let base = match ty.skip_reference() {
371+
Type::Primitive(PrimitiveType::U8) => "Bv8",
372+
Type::Primitive(PrimitiveType::U16) => "Bv16",
373+
Type::Primitive(PrimitiveType::U32) => "Bv32",
374+
Type::Primitive(PrimitiveType::U64) => "Bv64",
375+
Type::Primitive(PrimitiveType::U128) => "Bv128",
376+
Type::Primitive(PrimitiveType::U256) => "Bv256",
377+
Type::Primitive(PrimitiveType::Num) => {
378+
env.error(&loc.unwrap_or_default(), NUM_TYPE_BASE_ERROR);
379+
"<<num is not unsupported here>>"
380+
},
381+
_ => unreachable!(),
382+
};
383+
base.to_string()
384+
}
385+
364386
pub fn boogie_type_param(_env: &GlobalEnv, idx: u16) -> String {
365387
format!("#{}", idx)
366388
}
@@ -392,7 +414,7 @@ pub fn boogie_num_type_string_capital(num: &str, bv_flag: bool) -> String {
392414
[pre, num].join("")
393415
}
394416

395-
pub fn boogie_num_type_base(ty: &Type) -> String {
417+
pub fn boogie_num_type_base(env: &GlobalEnv, loc: Option<Loc>, ty: &Type) -> String {
396418
use PrimitiveType::*;
397419
use Type::*;
398420
match ty {
@@ -403,7 +425,10 @@ pub fn boogie_num_type_base(ty: &Type) -> String {
403425
U64 => "64".to_string(),
404426
U128 => "128".to_string(),
405427
U256 => "256".to_string(),
406-
Num => "<<num is not unsupported here>>".to_string(),
428+
Num => {
429+
env.error(&loc.unwrap_or_default(), NUM_TYPE_BASE_ERROR);
430+
"<<num is not unsupported here>>".to_string()
431+
},
407432
_ => format!("<<unsupported {:?}>>", ty),
408433
},
409434
_ => format!("<<unsupported {:?}>>", ty),
@@ -425,6 +450,7 @@ pub fn boogie_type_suffix_bv(env: &GlobalEnv, ty: &Type, bv_flag: bool) -> Strin
425450
U256 => boogie_num_type_string("256", bv_flag),
426451
Num => {
427452
if bv_flag {
453+
//TODO(tengzhang): add error message with accurate location info
428454
"<<num is not unsupported here>>".to_string()
429455
} else {
430456
"num".to_string()

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

Lines changed: 45 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1589,7 +1589,11 @@ impl FunctionTranslator<'_> {
15891589
if srcs_1_bv_flag {
15901590
args_src_1_str = format!(
15911591
"$bv2int.{}({})",
1592-
boogie_num_type_base(&local_ty_srcs_1),
1592+
boogie_num_type_base(
1593+
self.parent.env,
1594+
Some(self.fun_target.get_bytecode_loc(attr_id)),
1595+
&local_ty_srcs_1
1596+
),
15931597
args_src_1_str
15941598
);
15951599
}
@@ -1636,7 +1640,11 @@ impl FunctionTranslator<'_> {
16361640
writer,
16371641
"call {} := $int2bv{}({}({}));",
16381642
dest_str,
1639-
boogie_num_type_base(&local_ty),
1643+
boogie_num_type_base(
1644+
self.parent.env,
1645+
Some(self.fun_target.get_bytecode_loc(attr_id)),
1646+
&local_ty
1647+
),
16401648
fun_name,
16411649
args_str
16421650
);
@@ -1675,7 +1683,11 @@ impl FunctionTranslator<'_> {
16751683
writer,
16761684
"call {} := $int2bv{}({}({}));",
16771685
dest_str,
1678-
boogie_num_type_base(&local_ty),
1686+
boogie_num_type_base(
1687+
self.parent.env,
1688+
Some(self.fun_target.get_bytecode_loc(attr_id)),
1689+
&local_ty
1690+
),
16791691
fun_name,
16801692
args_str
16811693
);
@@ -1993,7 +2005,11 @@ impl FunctionTranslator<'_> {
19932005
let bv_flag = self.bv_flag(num_oper);
19942006
if bv_flag {
19952007
let src_type = self.get_local_type(src);
1996-
let base = boogie_num_type_base(&src_type);
2008+
let base = boogie_num_type_base(
2009+
self.parent.env,
2010+
Some(self.fun_target.get_bytecode_loc(attr_id)),
2011+
&src_type,
2012+
);
19972013
emitln!(
19982014
writer,
19992015
"call {} := $CastBv{}to{}({});",
@@ -2302,7 +2318,11 @@ impl FunctionTranslator<'_> {
23022318
| Type::Error
23032319
| Type::Var(_) => unreachable!(),
23042320
};
2305-
let src_type = boogie_num_type_base(&self.get_local_type(op2));
2321+
let src_type = boogie_num_type_base(
2322+
self.parent.env,
2323+
Some(self.fun_target.get_bytecode_loc(attr_id)),
2324+
&self.get_local_type(op2),
2325+
);
23062326
emitln!(
23072327
writer,
23082328
"call {} := ${}{}From{}({}, {});",
@@ -2480,7 +2500,11 @@ impl FunctionTranslator<'_> {
24802500
let op1_str = if !op1_bv_flag {
24812501
format!(
24822502
"$int2bv.{}({})",
2483-
boogie_num_type_base(op1_ty),
2503+
boogie_num_type_base(
2504+
self.parent.env,
2505+
Some(self.fun_target.get_bytecode_loc(attr_id)),
2506+
op1_ty
2507+
),
24842508
str_local(op1)
24852509
)
24862510
} else {
@@ -2489,7 +2513,11 @@ impl FunctionTranslator<'_> {
24892513
let op2_str = if !op2_bv_flag {
24902514
format!(
24912515
"$int2bv.{}({})",
2492-
boogie_num_type_base(op2_ty),
2516+
boogie_num_type_base(
2517+
self.parent.env,
2518+
Some(self.fun_target.get_bytecode_loc(attr_id)),
2519+
op2_ty
2520+
),
24932521
str_local(op2)
24942522
)
24952523
} else {
@@ -2574,7 +2602,11 @@ impl FunctionTranslator<'_> {
25742602
let bv2int_str = if *num_oper_code == Bitwise {
25752603
format!(
25762604
"$int2bv.{}($abort_code)",
2577-
boogie_num_type_base(&self.get_local_type(*code))
2605+
boogie_num_type_base(
2606+
self.parent.env,
2607+
Some(self.fun_target.get_bytecode_loc(attr_id)),
2608+
&self.get_local_type(*code)
2609+
)
25782610
)
25792611
} else {
25802612
"$abort_code".to_string()
@@ -2594,7 +2626,11 @@ impl FunctionTranslator<'_> {
25942626
let int2bv_str = if *num_oper_code == Bitwise {
25952627
format!(
25962628
"$bv2int.{}({})",
2597-
boogie_num_type_base(&self.get_local_type(*src)),
2629+
boogie_num_type_base(
2630+
self.parent.env,
2631+
Some(self.fun_target.get_bytecode_loc(attr_id)),
2632+
&self.get_local_type(*src)
2633+
),
25982634
str_local(*src)
25992635
)
26002636
} else {

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -216,7 +216,7 @@ pub fn add_prelude(
216216
.iter()
217217
.filter(|ty| ty.is_number() && !matches!(ty, Type::Primitive(PrimitiveType::Num)))
218218
.map(|ty| {
219-
boogie_num_type_base(ty)
219+
boogie_num_type_base(env, None, ty)
220220
.parse::<usize>()
221221
.expect("parse error")
222222
})

0 commit comments

Comments
 (0)