diff --git a/docs/dev-guide/src/config/flags.md b/docs/dev-guide/src/config/flags.md index b6771a1b113..89fbfb766c4 100644 --- a/docs/dev-guide/src/config/flags.md +++ b/docs/dev-guide/src/config/flags.md @@ -60,7 +60,7 @@ | [`SERVER_ADDRESS`](#server_address) | `Option` | `None` | A | | [`SERVER_MAX_CONCURRENCY`](#server_max_concurrency) | `Option` | `None` | A | | [`SERVER_MAX_STORED_VERIFIERS`](#server_max_stored_verifiers) | `Option` | `None` | A | -| [`SIMPLIFY_ENCODING`](#simplify_encoding) | `bool` | `true` | A | +| [`SIMPLIFY_ENCODING`](#simplify_encoding) | `bool` | `false` | A | | [`SKIP_UNSUPPORTED_FEATURES`](#skip_unsupported_features) | `bool` | `false` | A | | [`SMT_QI_BOUND_GLOBAL`](#smt_qi_bound_global) | `Option` | `None` | A | [`SMT_QI_BOUND_GLOBAL_KIND`](#smt_qi_bound_global_kind) | `Option` | `None` | A | diff --git a/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs b/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs index 4a42eda82a1..84b62b55b79 100644 --- a/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs +++ b/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs @@ -2,7 +2,7 @@ use prusti_contracts::*; // To inhibit constant-propagation optimizations: #[pure] -fn id(x: T) -> T { x} +fn id(x: T) -> T { x } fn check_division(){ assert!(id(3i32) / 2 == 1); @@ -23,6 +23,10 @@ fn check_modulo() { assert!(id(10) % -3 == 1); assert!(id(-10) % 3 == -1); assert!(id(-10) % -3 == -1); + prusti_assert!(id(10) % 3 == 1); + prusti_assert!(id(10) % -3 == 1); + prusti_assert!(id(-10) % 3 == -1); + prusti_assert!(id(-10) % -3 == -1); assert!(id(3) % 3 == 0); assert!(id(2) % 3 == 2); @@ -33,8 +37,18 @@ fn check_modulo() { assert!(id(-3) % 3 == 0); assert!(id(-4) % 3 == -1); assert!(id(-5) % 3 == -2); + prusti_assert!(id(3) % 3 == 0); + prusti_assert!(id(2) % 3 == 2); + prusti_assert!(id(1) % 3 == 1); + prusti_assert!(id(0) % 3 == 0); + prusti_assert!(id(-1) % 3 == -1); + prusti_assert!(id(-2) % 3 == -2); + prusti_assert!(id(-3) % 3 == 0); + prusti_assert!(id(-4) % 3 == -1); + prusti_assert!(id(-5) % 3 == -2); assert!(id(-4) % 2 == 0); + prusti_assert!(id(-4) % 2 == 0); // Smoke test assert!(false); //~ ERROR the asserted expression might not hold diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index 2e46d55519c..6b4a52f7356 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -82,7 +82,7 @@ lazy_static::lazy_static! { settings.set_default("check_panics", true).unwrap(); settings.set_default("encode_unsigned_num_constraint", true).unwrap(); settings.set_default("encode_bitvectors", false).unwrap(); - settings.set_default("simplify_encoding", true).unwrap(); + settings.set_default("simplify_encoding", false).unwrap(); settings.set_default("log", "").unwrap(); settings.set_default("log_style", "auto").unwrap(); settings.set_default("log_dir", "log").unwrap(); diff --git a/prusti-viper/src/encoder/mir_encoder/mod.rs b/prusti-viper/src/encoder/mir_encoder/mod.rs index 700807d8833..142adcee295 100644 --- a/prusti-viper/src/encoder/mir_encoder/mod.rs +++ b/prusti-viper/src/encoder/mir_encoder/mod.rs @@ -494,7 +494,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> MirEncoder<'p, 'v, 'tcx> { vir::Expr::rem(left, right) } } - mir::BinOp::Div => vir::Expr::div(left, right), + mir::BinOp::Div => { + if matches!(ty.kind(), ty::TyKind::Uint(_)) { + vir::Expr::unsigned_div(left, right) + } else { + vir::Expr::div(left, right) + } + } mir::BinOp::MulUnchecked | mir::BinOp::Mul => vir::Expr::mul(left, right), mir::BinOp::BitAnd if is_bool => vir::Expr::and(left, right), mir::BinOp::BitOr if is_bool => vir::Expr::or(left, right), diff --git a/vir/defs/polymorphic/ast/expr.rs b/vir/defs/polymorphic/ast/expr.rs index e85ee38e739..d3198e97723 100644 --- a/vir/defs/polymorphic/ast/expr.rs +++ b/vir/defs/polymorphic/ast/expr.rs @@ -151,7 +151,7 @@ __binary_op__! { add Add, sub Sub, mul Mul, - div Div, + unsigned_div Div, modulo Mod, and And, or Or, @@ -315,8 +315,21 @@ impl Expr { Expr::not(Expr::eq_cmp(left, right)) } - #[allow(clippy::should_implement_trait)] - /// Encode Rust reminder. This is *not* Viper modulo. + /// Encode Rust's division. This is *not* Viper's division. + pub fn div(left: Expr, right: Expr) -> Self { + Expr::ite( + Expr::or( + Expr::ge_cmp(left.clone(), 0.into()), + Expr::eq_cmp(Expr::modulo(left.clone(), right.clone()), 0.into()), + ), + // positive value or left % right == 0 + Expr::unsigned_div(left.clone(), right.clone()), + // negative value + Expr::minus(Expr::unsigned_div(Expr::minus(left), right)), + ) + } + + /// Encode Rust's signed reminder. This is *not* Viper's modulo. pub fn rem(left: Expr, right: Expr) -> Self { let abs_right = Expr::ite( Expr::ge_cmp(right.clone(), 0.into()), diff --git a/vir/src/legacy/ast/expr.rs b/vir/src/legacy/ast/expr.rs index 14876f6a800..ce188fb54f5 100644 --- a/vir/src/legacy/ast/expr.rs +++ b/vir/src/legacy/ast/expr.rs @@ -561,7 +561,8 @@ impl Expr { } #[allow(clippy::should_implement_trait)] - pub fn div(left: Expr, right: Expr) -> Self { + /// Encode Rust's unsigned division. This is the same as Viper's division. + pub fn unsigned_div(left: Expr, right: Expr) -> Self { Expr::BinOp( BinaryOpKind::Div, Box::new(left), @@ -570,6 +571,22 @@ impl Expr { ) } + #[allow(clippy::should_implement_trait)] + /// Encode Rust's division. This is *not* Viper's division. + pub fn div(left: Expr, right: Expr) -> Self { + Expr::ite( + Expr::or( + Expr::ge_cmp(left.clone(), 0.into()), + Expr::eq_cmp(Expr::modulo(left.clone(), right.clone()), 0.into()), + ), + // positive value or left % right == 0 + Expr::unsigned_div(left.clone(), right.clone()), + // negative value + Expr::minus(Expr::unsigned_div(Expr::minus(left), right)), + ) + } + + /// Encode Rust's unsigned reminder. This is the same as Viper's modulo. pub fn modulo(left: Expr, right: Expr) -> Self { Expr::BinOp( BinaryOpKind::Mod, @@ -580,7 +597,7 @@ impl Expr { } #[allow(clippy::should_implement_trait)] - /// Encode Rust reminder. This is *not* Viper modulo. + /// Encode Rust's signed reminder. This is *not* Viper's modulo. pub fn rem(left: Expr, right: Expr) -> Self { let abs_right = Expr::ite( Expr::ge_cmp(right.clone(), 0.into()),