Ugly commit 29.12

viperproject · Jan 16, 2024 · d05e2ef · d05e2ef
1 parent f2c58f2
commit d05e2ef
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 4 deletions.
diff --git a/prusti-contracts/prusti-contracts/src/core_spec.rs b/prusti-contracts/prusti-contracts/src/core_spec.rs
@@ -75,7 +75,8 @@ impl<T> Pointer<T> {
     #[pure]
     // FIXME: Check provenance.
     #[structural_requires(same_allocation(self, origin))]
-    #[structural_requires(address_from(self, origin) * Int::new_usize(std::mem::size_of::<T>()) <= Int::new_isize(isize::MAX))]
+    // #[structural_requires(address_from(self, origin) * Int::new_usize(std::mem::size_of::<T>()) <= Int::new_isize(isize::MAX))]
+    #[structural_requires(multiply_int(address_from(self, origin), Int::new_usize(std::mem::size_of::<T>())) <= Int::new_isize(isize::MAX))]
     #[structural_requires(address_from(self, origin) >= Int::new_isize(0))]
     #[ensures(Int::new_isize(result) == address_from(self, origin))]
     #[no_panic]
@@ -86,7 +87,8 @@ impl<T> Pointer<T> {
     #[terminates]
     #[pure]
     // FIXME: Check provenance.
-    #[structural_requires(Int::new_usize(count) * Int::new_usize(std::mem::size_of::<T>()) <= Int::new_isize(isize::MAX))]
+    // #[structural_requires(Int::new_usize(count) * Int::new_usize(std::mem::size_of::<T>()) <= Int::new_isize(isize::MAX))]
+    #[structural_requires(multiply_int(Int::new_usize(count), Int::new_usize(std::mem::size_of::<T>())) <= Int::new_usize(usize::MAX))]
     #[ensures(result == address_offset(self, Int::new_usize(count)))]
     #[no_panic]
     #[no_panic_ensures_postcondition]
@@ -141,7 +143,7 @@ impl<T> MutPointer<T> {
     #[pure]
     // FIXME: Check provenance.
     #[structural_requires(same_allocation(self, origin))]
-    #[structural_requires(address_from(self, origin) * Int::new_usize(std::mem::size_of::<T>()) <= Int::new_isize(isize::MAX))]
+    #[structural_requires(multiply_int(address_from(self, origin), Int::new_usize(std::mem::size_of::<T>())) <= Int::new_isize(isize::MAX))]
     #[structural_requires(address_from(self, origin) >= Int::new_isize(0))]
     #[ensures(Int::new_isize(result) == address_from(self, origin))]
     #[no_panic]

diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs
@@ -104,6 +104,7 @@ lazy_static::lazy_static! {
         settings.set_default("assert_timeout", 10_000).unwrap();
         settings.set_default("smt_qi_eager_threshold", 1000).unwrap();
         settings.set_default("smt_use_nonlinear_arithmetic_solver", false).unwrap();
+        settings.set_default("define_multiply_int", false).unwrap();
         settings.set_default("use_more_complete_exhale", false).unwrap();
         settings.set_default("use_carbon_qps", true).unwrap();
         settings.set_default("use_z3_api", false).unwrap();
@@ -537,6 +538,11 @@ pub fn smt_use_nonlinear_arithmetic_solver() -> bool {
     read_setting("smt_use_nonlinear_arithmetic_solver")
 }
 
+/// Define `multiply_int` as a multiplication.
+pub fn define_multiply_int() -> bool {
+    read_setting("define_multiply_int")
+}
+
 /// Maximum time (in milliseconds) for the verifier to spend on checks.
 /// Set to None uses the verifier's default value. Maps to the verifier command-line
 /// argument `--checkTimeout`.

diff --git a/prusti-viper/src/encoder/middle/core_proof/arithmetic_wrappers/interface.rs b/prusti-viper/src/encoder/middle/core_proof/arithmetic_wrappers/interface.rs
@@ -177,7 +177,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ArithmeticWrappersInterface for Lowerer<'p, 'v, 'tcx>
                     vir_low::DomainAxiomDecl::new(None, "mul_wrapper$positive_increases", body);
                 self.declare_axiom(DOMAIN_NAME, axiom)?;
             }
-            if config::smt_use_nonlinear_arithmetic_solver() {
+            if config::define_multiply_int() {
                 let body = vir_low::Expression::forall(
                     vec![left.clone(), right.clone()],
                     vec![vir_low::Trigger::new(vec![call.clone()])],