From da857be6f3ce18141179a8fc76a440126f037732 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 30 Oct 2024 08:18:33 -0700 Subject: [PATCH 1/9] Fix overflow in conversion from uvalue to svalue Signed-off-by: Alan Jowett --- src/crab/ebpf_domain.cpp | 3 ++- test-data/shift.yaml | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 35 insertions(+), 1 deletion(-) diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 7d34ba9df..6039cbf11 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -2374,7 +2374,8 @@ void ebpf_domain_t::lshr(const Reg& dst_reg, int imm, int finite_width) { } } m_inv.set(dst.uvalue, interval_t{lb_n, ub_n}); - if (ub_n.narrow() >= lb_n.narrow()) { + if ((ub_n.fits() && lb_n.fits()) && + ub_n.narrow() >= lb_n.narrow()) { // ? m_inv.set(dst.svalue, crab::interval_t{number_t{(int64_t)lb_n}, number_t{(int64_t)ub_n}}); m_inv.assign(dst.svalue, dst.uvalue); } else { diff --git a/test-data/shift.yaml b/test-data/shift.yaml index 2a78650a5..93368ad50 100644 --- a/test-data/shift.yaml +++ b/test-data/shift.yaml @@ -1104,3 +1104,36 @@ post: - r2.type=number - r2.svalue=32 - r2.uvalue=32 + +--- +test-case: check that unsigned right shift by 0 is idempotent + +pre: + - r0.type=number + - r0.svalue=-8863041185711652825 + - r0.uvalue=9583702887997898791 + - r1.type=number + - r1.svalue=-8863041185711652825 + - r1.uvalue=9583702887997898791 + +code: + : | + r0 >>= 0 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.type=number + - r0.uvalue=9583702887997898791 + - r1.type=number + - r1.svalue=-8863041185711652825 + - r1.uvalue=9583702887997898791 + - r0.uvalue=r1.uvalue + - r2.type=number + - r2.svalue=[0, 1] + - r2.uvalue=[0, 1] + - r2.svalue=r2.uvalue From 087156bdf42c26417bb208d4c3c977a7203c3c0d Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 30 Oct 2024 08:23:43 -0700 Subject: [PATCH 2/9] Add positive and negative test cases Signed-off-by: Alan Jowett --- test-data/shift.yaml | 39 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/test-data/shift.yaml b/test-data/shift.yaml index 93368ad50..7db1e823e 100644 --- a/test-data/shift.yaml +++ b/test-data/shift.yaml @@ -1106,7 +1106,7 @@ post: - r2.uvalue=32 --- -test-case: check that unsigned right shift by 0 is idempotent +test-case: check that unsigned right shift by 0 is idempotent - svalue out of range pre: - r0.type=number @@ -1137,3 +1137,40 @@ post: - r2.svalue=[0, 1] - r2.uvalue=[0, 1] - r2.svalue=r2.uvalue + +--- +test-case: check that unsigned right shift by 0 is idempotent - valid svalue + +pre: + - r0.type=number + - r0.svalue=9223372036854775807 + - r0.uvalue=9223372036854775807 + - r1.type=number + - r1.svalue=9223372036854775807 + - r1.uvalue=9223372036854775807 + +code: + : | + r0 >>= 0 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.svalue=9223372036854775807 + - r0.svalue=r1.svalue + - r0.type=number + - r0.uvalue=9223372036854775807 + - r0.uvalue=r1.uvalue + - r1.svalue=9223372036854775807 + - r1.type=number + - r1.uvalue=9223372036854775807 + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + +messages: + - "1:2: Code is unreachable after 1:2" From 0167dd0a428b8166502128820c09eca1332253db Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 30 Oct 2024 08:28:37 -0700 Subject: [PATCH 3/9] PR feedback Signed-off-by: Alan Jowett --- test-data/shift.yaml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/test-data/shift.yaml b/test-data/shift.yaml index 7db1e823e..b6cf60d62 100644 --- a/test-data/shift.yaml +++ b/test-data/shift.yaml @@ -1110,11 +1110,12 @@ test-case: check that unsigned right shift by 0 is idempotent - svalue out of ra pre: - r0.type=number - - r0.svalue=-8863041185711652825 - - r0.uvalue=9583702887997898791 + # This is 0x8000000000000000, which is out of range for a signed 64-bit number. + - r0.svalue=-9223372036854775808 + - r0.uvalue=9223372036854775808 - r1.type=number - - r1.svalue=-8863041185711652825 - - r1.uvalue=9583702887997898791 + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 code: : | @@ -1128,10 +1129,11 @@ code: post: - r0.type=number - - r0.uvalue=9583702887997898791 + - r0.uvalue=9223372036854775808 + # Note: The svalue gets havoced by the shift, so we can't check it. - r1.type=number - - r1.svalue=-8863041185711652825 - - r1.uvalue=9583702887997898791 + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 - r0.uvalue=r1.uvalue - r2.type=number - r2.svalue=[0, 1] @@ -1143,6 +1145,7 @@ test-case: check that unsigned right shift by 0 is idempotent - valid svalue pre: - r0.type=number + # This is 0x7fffffffffffffff, which is in range for a signed 64-bit number. - r0.svalue=9223372036854775807 - r0.uvalue=9223372036854775807 - r1.type=number From b08fffe01b34e6c780ad782614ef9aae987b3d3d Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 30 Oct 2024 08:43:20 -0700 Subject: [PATCH 4/9] Add test to ensure immediate and register versions of unsigned right shift match Signed-off-by: Alan Jowett --- test-data/shift.yaml | 85 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) diff --git a/test-data/shift.yaml b/test-data/shift.yaml index b6cf60d62..384752886 100644 --- a/test-data/shift.yaml +++ b/test-data/shift.yaml @@ -1177,3 +1177,88 @@ post: messages: - "1:2: Code is unreachable after 1:2" + +--- +test-case: check that unsigned right shift by 0 is idempotent - svalue out of range - via register + +pre: + - r0.type=number + # This is 0x8000000000000000, which is out of range for a signed 64-bit number. + - r0.svalue=-9223372036854775808 + - r0.uvalue=9223372036854775808 + - r1.type=number + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +code: + : | + r0 >>= r3 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.type=number + - r0.uvalue=9223372036854775808 + # Note: The svalue gets havoced by the shift, so we can't check it. + - r1.type=number + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 + - r0.uvalue=r1.uvalue + - r2.type=number + - r2.svalue=[0, 1] + - r2.uvalue=[0, 1] + - r2.svalue=r2.uvalue + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +--- +test-case: check that unsigned right shift by 0 is idempotent - valid svalue + +pre: + - r0.type=number + # This is 0x7fffffffffffffff, which is in range for a signed 64-bit number. + - r0.svalue=9223372036854775807 + - r0.uvalue=9223372036854775807 + - r1.type=number + - r1.svalue=9223372036854775807 + - r1.uvalue=9223372036854775807 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +code: + : | + r0 >>= r3 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.svalue=9223372036854775807 + - r0.svalue=r1.svalue + - r0.type=number + - r0.uvalue=9223372036854775807 + - r0.uvalue=r1.uvalue + - r1.svalue=9223372036854775807 + - r1.type=number + - r1.uvalue=9223372036854775807 + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +messages: + - "1:2: Code is unreachable after 1:2" From 609e11fa229ec528b08db25d457e309b40e00c11 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 30 Oct 2024 09:39:54 -0700 Subject: [PATCH 5/9] PR feedback Signed-off-by: Alan Jowett --- src/crab/ebpf_domain.cpp | 10 +++------- test-data/shift.yaml | 22 ++++++++++++++-------- 2 files changed, 17 insertions(+), 15 deletions(-) diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 6039cbf11..816140c55 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -2374,13 +2374,9 @@ void ebpf_domain_t::lshr(const Reg& dst_reg, int imm, int finite_width) { } } m_inv.set(dst.uvalue, interval_t{lb_n, ub_n}); - if ((ub_n.fits() && lb_n.fits()) && - ub_n.narrow() >= lb_n.narrow()) { - // ? m_inv.set(dst.svalue, crab::interval_t{number_t{(int64_t)lb_n}, number_t{(int64_t)ub_n}}); - m_inv.assign(dst.svalue, dst.uvalue); - } else { - havoc(dst.svalue); - } + m_inv.assign(dst.svalue, dst.uvalue); + overflow_signed(m_inv, dst.svalue, finite_width); + overflow_unsigned(m_inv, dst.uvalue, finite_width); return; } havoc(dst.svalue); diff --git a/test-data/shift.yaml b/test-data/shift.yaml index 384752886..53bb2594a 100644 --- a/test-data/shift.yaml +++ b/test-data/shift.yaml @@ -1129,16 +1129,19 @@ code: post: - r0.type=number + - r0.svalue=-9223372036854775808 - r0.uvalue=9223372036854775808 - # Note: The svalue gets havoced by the shift, so we can't check it. - r1.type=number - r1.svalue=-9223372036854775808 - r1.uvalue=9223372036854775808 + - r0.svalue=r1.svalue - r0.uvalue=r1.uvalue + - r2.svalue=1 - r2.type=number - - r2.svalue=[0, 1] - - r2.uvalue=[0, 1] - - r2.svalue=r2.uvalue + - r2.uvalue=1 + +messages: + - "1:2: Code is unreachable after 1:2" --- test-case: check that unsigned right shift by 0 is idempotent - valid svalue @@ -1205,20 +1208,23 @@ code: post: - r0.type=number + - r0.svalue=-9223372036854775808 - r0.uvalue=9223372036854775808 - # Note: The svalue gets havoced by the shift, so we can't check it. - r1.type=number - r1.svalue=-9223372036854775808 - r1.uvalue=9223372036854775808 + - r0.svalue=r1.svalue - r0.uvalue=r1.uvalue + - r2.svalue=1 - r2.type=number - - r2.svalue=[0, 1] - - r2.uvalue=[0, 1] - - r2.svalue=r2.uvalue + - r2.uvalue=1 - r3.type=number - r3.uvalue=0 - r3.svalue=0 +messages: + - "1:2: Code is unreachable after 1:2" + --- test-case: check that unsigned right shift by 0 is idempotent - valid svalue From f4c915a1e51d55256b199f985f54779e335e845a Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 30 Oct 2024 10:00:33 -0700 Subject: [PATCH 6/9] PR feedback and fix other cases Signed-off-by: Alan Jowett --- src/crab/ebpf_domain.cpp | 16 +- test-data/shift.yaml | 332 ++++++++++++++++++++++++++++++++++++++- 2 files changed, 330 insertions(+), 18 deletions(-) diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 816140c55..48ae3c265 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -2334,11 +2334,9 @@ void ebpf_domain_t::shl(const Reg& dst_reg, int imm, const int finite_width) { ub_n = ub_n << imm & uint_max; } m_inv.set(dst.uvalue, interval_t{lb_n, ub_n}); - if (to_signed(ub_n) >= to_signed(lb_n)) { - m_inv.assign(dst.svalue, dst.uvalue); - } else { - havoc(dst.svalue); - } + m_inv.assign(dst.svalue, dst.uvalue); + overflow_signed(m_inv, dst.svalue, finite_width); + overflow_unsigned(m_inv, dst.uvalue, finite_width); return; } } @@ -2461,11 +2459,9 @@ void ebpf_domain_t::ashr(const Reg& dst_reg, const linear_expression_t& right_sv } } m_inv.set(dst.svalue, interval_t{lb_n, ub_n}); - if (to_unsigned(ub_n) >= to_unsigned(lb_n)) { - m_inv.assign(dst.uvalue, dst.svalue); - } else { - havoc(dst.uvalue); - } + m_inv.assign(dst.uvalue, dst.svalue); + overflow_signed(m_inv, dst.svalue, finite_width); + overflow_unsigned(m_inv, dst.uvalue, finite_width); return; } } diff --git a/test-data/shift.yaml b/test-data/shift.yaml index 53bb2594a..3d9e0d939 100644 --- a/test-data/shift.yaml +++ b/test-data/shift.yaml @@ -1106,11 +1106,10 @@ post: - r2.uvalue=32 --- -test-case: check that unsigned right shift by 0 is idempotent - svalue out of range +test-case: check that unsigned right shift by 0 is idempotent - MIN_INT64 pre: - r0.type=number - # This is 0x8000000000000000, which is out of range for a signed 64-bit number. - r0.svalue=-9223372036854775808 - r0.uvalue=9223372036854775808 - r1.type=number @@ -1144,11 +1143,10 @@ messages: - "1:2: Code is unreachable after 1:2" --- -test-case: check that unsigned right shift by 0 is idempotent - valid svalue +test-case: check that unsigned right shift by 0 is idempotent - MAX_INT64 pre: - r0.type=number - # This is 0x7fffffffffffffff, which is in range for a signed 64-bit number. - r0.svalue=9223372036854775807 - r0.uvalue=9223372036854775807 - r1.type=number @@ -1182,11 +1180,10 @@ messages: - "1:2: Code is unreachable after 1:2" --- -test-case: check that unsigned right shift by 0 is idempotent - svalue out of range - via register +test-case: check that unsigned right shift by 0 is idempotent - MIN_INT64 - via register pre: - r0.type=number - # This is 0x8000000000000000, which is out of range for a signed 64-bit number. - r0.svalue=-9223372036854775808 - r0.uvalue=9223372036854775808 - r1.type=number @@ -1226,11 +1223,10 @@ messages: - "1:2: Code is unreachable after 1:2" --- -test-case: check that unsigned right shift by 0 is idempotent - valid svalue +test-case: check that unsigned right shift by 0 is idempotent - MIN_INT64 - via register pre: - r0.type=number - # This is 0x7fffffffffffffff, which is in range for a signed 64-bit number. - r0.svalue=9223372036854775807 - r0.uvalue=9223372036854775807 - r1.type=number @@ -1268,3 +1264,323 @@ post: messages: - "1:2: Code is unreachable after 1:2" + +--- +test-case: check that signed right shift by 0 is idempotent - MIN_INT64 + +pre: + - r0.type=number + - r0.svalue=-9223372036854775808 + - r0.uvalue=9223372036854775808 + - r1.type=number + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 + +code: + : | + r0 s>>= 0 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.type=number + - r0.svalue=-9223372036854775808 + - r0.uvalue=9223372036854775808 + - r1.type=number + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 + - r0.svalue=r1.svalue + - r0.uvalue=r1.uvalue + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + +messages: + - "1:2: Code is unreachable after 1:2" + +--- +test-case: check that signed right shift by 0 is idempotent - MAX_INT64 + +pre: + - r0.type=number + - r0.svalue=9223372036854775807 + - r0.uvalue=9223372036854775807 + - r1.type=number + - r1.svalue=9223372036854775807 + - r1.uvalue=9223372036854775807 + +code: + : | + r0 s>>= 0 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.svalue=9223372036854775807 + - r0.svalue=r1.svalue + - r0.type=number + - r0.uvalue=9223372036854775807 + - r0.uvalue=r1.uvalue + - r1.svalue=9223372036854775807 + - r1.type=number + - r1.uvalue=9223372036854775807 + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + +messages: + - "1:2: Code is unreachable after 1:2" + +--- +test-case: check that signed right shift by 0 is idempotent - MIN_INT64 - via register + +pre: + - r0.type=number + - r0.svalue=-9223372036854775808 + - r0.uvalue=9223372036854775808 + - r1.type=number + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +code: + : | + r0 s>>= r3 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.type=number + - r0.svalue=-9223372036854775808 + - r0.uvalue=9223372036854775808 + - r1.type=number + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 + - r0.svalue=r1.svalue + - r0.uvalue=r1.uvalue + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +messages: + - "1:2: Code is unreachable after 1:2" + +--- +test-case: check that signed right shift by 0 is idempotent - MAX_INT64 + +pre: + - r0.type=number + - r0.svalue=9223372036854775807 + - r0.uvalue=9223372036854775807 + - r1.type=number + - r1.svalue=9223372036854775807 + - r1.uvalue=9223372036854775807 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +code: + : | + r0 s>>= r3 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.svalue=9223372036854775807 + - r0.svalue=r1.svalue + - r0.type=number + - r0.uvalue=9223372036854775807 + - r0.uvalue=r1.uvalue + - r1.svalue=9223372036854775807 + - r1.type=number + - r1.uvalue=9223372036854775807 + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +messages: + - "1:2: Code is unreachable after 1:2" + +--- +test-case: check that left shift by 0 is idempotent - MIN_INT64 + +pre: + - r0.type=number + - r0.svalue=-9223372036854775808 + - r0.uvalue=9223372036854775808 + - r1.type=number + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 + +code: + : | + r0 <<= 0 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.type=number + - r0.svalue=-9223372036854775808 + - r0.uvalue=9223372036854775808 + - r1.type=number + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 + - r0.svalue=r1.svalue + - r0.uvalue=r1.uvalue + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + +messages: + - "1:2: Code is unreachable after 1:2" + +--- +test-case: check that left shift by 0 is idempotent - MAX_INT64 + +pre: + - r0.type=number + - r0.svalue=9223372036854775807 + - r0.uvalue=9223372036854775807 + - r1.type=number + - r1.svalue=9223372036854775807 + - r1.uvalue=9223372036854775807 + +code: + : | + r0 <<= 0 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.svalue=9223372036854775807 + - r0.svalue=r1.svalue + - r0.type=number + - r0.uvalue=9223372036854775807 + - r0.uvalue=r1.uvalue + - r1.svalue=9223372036854775807 + - r1.type=number + - r1.uvalue=9223372036854775807 + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + +messages: + - "1:2: Code is unreachable after 1:2" + +--- +test-case: check that left shift by 0 is idempotent - MIN_INT64 - via register + +pre: + - r0.type=number + - r0.svalue=-9223372036854775808 + - r0.uvalue=9223372036854775808 + - r1.type=number + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +code: + : | + r0 <<= r3 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.type=number + - r0.svalue=-9223372036854775808 + - r0.uvalue=9223372036854775808 + - r1.type=number + - r1.svalue=-9223372036854775808 + - r1.uvalue=9223372036854775808 + - r0.svalue=r1.svalue + - r0.uvalue=r1.uvalue + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +messages: + - "1:2: Code is unreachable after 1:2" + +--- +test-case: check that left shift by 0 is idempotent - MAX_INT64 + +pre: + - r0.type=number + - r0.svalue=9223372036854775807 + - r0.uvalue=9223372036854775807 + - r1.type=number + - r1.svalue=9223372036854775807 + - r1.uvalue=9223372036854775807 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +code: + : | + r0 <<= r3 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.svalue=9223372036854775807 + - r0.svalue=r1.svalue + - r0.type=number + - r0.uvalue=9223372036854775807 + - r0.uvalue=r1.uvalue + - r1.svalue=9223372036854775807 + - r1.type=number + - r1.uvalue=9223372036854775807 + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +messages: + - "1:2: Code is unreachable after 1:2" From 86182c2e7062fcbb34523985d9bef0ecfe9f7cce Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 30 Oct 2024 10:12:27 -0700 Subject: [PATCH 7/9] PR feedback Signed-off-by: Alan Jowett --- test-data/shift.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-data/shift.yaml b/test-data/shift.yaml index 3d9e0d939..335ef61f4 100644 --- a/test-data/shift.yaml +++ b/test-data/shift.yaml @@ -1223,7 +1223,7 @@ messages: - "1:2: Code is unreachable after 1:2" --- -test-case: check that unsigned right shift by 0 is idempotent - MIN_INT64 - via register +test-case: check that unsigned right shift by 0 is idempotent - MAX_INT64 - via register pre: - r0.type=number From 27527cd52ccad874d542543c605711b06f0366dd Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 30 Oct 2024 10:13:05 -0700 Subject: [PATCH 8/9] PR feedback Signed-off-by: Alan Jowett --- test-data/shift.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-data/shift.yaml b/test-data/shift.yaml index 335ef61f4..ca2faf973 100644 --- a/test-data/shift.yaml +++ b/test-data/shift.yaml @@ -1543,7 +1543,7 @@ messages: - "1:2: Code is unreachable after 1:2" --- -test-case: check that left shift by 0 is idempotent - MAX_INT64 +test-case: check that left shift by 0 is idempotent - MAX_INT64 - via register pre: - r0.type=number From d885eba0ba820c5af8f9b95bc12a9cb825512fb5 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 30 Oct 2024 10:21:51 -0700 Subject: [PATCH 9/9] PR feedback Signed-off-by: Alan Jowett --- test-data/shift.yaml | 80 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 80 insertions(+) diff --git a/test-data/shift.yaml b/test-data/shift.yaml index ca2faf973..b9d0e1ac3 100644 --- a/test-data/shift.yaml +++ b/test-data/shift.yaml @@ -1339,6 +1339,43 @@ post: messages: - "1:2: Code is unreachable after 1:2" +--- +test-case: check that signed right shift by 0 is idempotent - MAX_UINT64 + +pre: + - r0.type=number + - r0.svalue=-1 + - r0.uvalue=18446744073709551615 + - r1.type=number + - r1.svalue=-1 + - r1.uvalue=18446744073709551615 + +code: + : | + r0 s>>= 0 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.svalue=-1 + - r0.svalue=r1.svalue + - r0.type=number + - r0.uvalue=18446744073709551615 + - r0.uvalue=r1.uvalue + - r1.svalue=-1 + - r1.type=number + - r1.uvalue=18446744073709551615 + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + +messages: + - "1:2: Code is unreachable after 1:2" + --- test-case: check that signed right shift by 0 is idempotent - MIN_INT64 - via register @@ -1425,6 +1462,49 @@ post: messages: - "1:2: Code is unreachable after 1:2" +--- +test-case: check that signed right shift by 0 is idempotent - MAX_UINT64 - via register + +pre: + - r0.type=number + - r0.svalue=-1 + - r0.uvalue=18446744073709551615 + - r1.type=number + - r1.svalue=-1 + - r1.uvalue=18446744073709551615 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +code: + : | + r0 s>>= r3 + if r1 == r0 goto + r2 = 0 + exit + : | + r2 = 1 + exit + +post: + - r0.svalue=-1 + - r0.svalue=r1.svalue + - r0.type=number + - r0.uvalue=18446744073709551615 + - r0.uvalue=r1.uvalue + - r1.svalue=-1 + - r1.type=number + - r1.uvalue=18446744073709551615 + - r2.svalue=1 + - r2.type=number + - r2.uvalue=1 + - r3.type=number + - r3.uvalue=0 + - r3.svalue=0 + +messages: + - "1:2: Code is unreachable after 1:2" + --- test-case: check that left shift by 0 is idempotent - MIN_INT64