max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: integer overflows

Browse source
This commit is contained in:
Sebastian Ullrich 2022-11-14 17:51:48 +01:00 • committed by Leonardo de Moura
parent 591eccee4f
commit 3f9ba30424
4 changed files with 12 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/ci.yml vendored
View file

@ -142,7 +142,7 @@ jobs:
if: matrix.os == 'windows-2022'
- name: Install Brew Packages
run: |
brew install ccache tree zstd coreutils
brew install ccache tree zstd coreutils gmp
if: matrix.os == 'macos-latest'
- name: Cache
uses: actions/cache@v2

6
src/runtime/mpz.cpp
View file

@ -47,7 +47,7 @@ mpz::mpz(uint64 v):
mpz::mpz(int64 v) {
uint64 w;
if (v < 0) w = -v;
if (v < 0) w = -static_cast<uint64>(v);
else w = v;
mpz_init_set_ui(m_val, static_cast<unsigned>(w));
mpz tmp(static_cast<unsigned>(w >> 32));
@ -146,13 +146,13 @@ mpz & mpz::operator+=(mpz const & o) { mpz_add(m_val, m_val, o.m_val); return *t
mpz & mpz::operator+=(unsigned u) { mpz_add_ui(m_val, m_val, u); return *this; }
mpz & mpz::operator+=(int u) { if (u >= 0) mpz_add_ui(m_val, m_val, u); else mpz_sub_ui(m_val, m_val, -u); return *this; }
mpz & mpz::operator+=(int u) { if (u >= 0) mpz_add_ui(m_val, m_val, u); else mpz_sub_ui(m_val, m_val, -static_cast<unsigned>(u)); return *this; }
mpz & mpz::operator-=(mpz const & o) { mpz_sub(m_val, m_val, o.m_val); return *this; }
mpz & mpz::operator-=(unsigned u) { mpz_sub_ui(m_val, m_val, u); return *this; }
mpz & mpz::operator-=(int u) { if (u >= 0) mpz_sub_ui(m_val, m_val, u); else mpz_add_ui(m_val, m_val, -u); return *this; }
mpz & mpz::operator-=(int u) { if (u >= 0) mpz_sub_ui(m_val, m_val, u); else mpz_add_ui(m_val, m_val, -static_cast<unsigned>(u)); return *this; }
mpz & mpz::operator*=(mpz const & o) { mpz_mul(m_val, m_val, o.m_val); return *this; }

2
tests/lean/1825.lean Normal file
View file

@ -0,0 +1,2 @@
theorem boom : -2147483648 + 2147483648 = 0 := by rfl
theorem boom' : -2147483648 + 2147483648 = -18446744069414584320 := by native_decide

6
tests/lean/1825.lean.expected.out Normal file
View file

@ -0,0 +1,6 @@
1825.lean:2:8-2:13: error: application type mismatch
Lean.ofReduceBool boom'._nativeDecide_1 true (Eq.refl true)
argument has type
true = true
but function has type
Lean.reduceBool boom'._nativeDecide_1 = true → boom'._nativeDecide_1 = true