From 4ec14b90e79e764216bcc0b2f4bee90e17b94896 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 6 Sep 2024 13:10:16 +1000 Subject: [PATCH] Use Euclidean division/modulus to express T-division/modulus for SMT hooks (#4616) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #4606 The following reasoning was applied: Given dividend `D` and divisor `d`, let the `q₋` and `r₋` in ``` D = d · qₑ + rₑ # Euclidean division D = d · qₜ + rₜ # T-division ``` be Euclidean and T division results. In terms of K operations, ``` qₑ = D divInt d rₑ = D modInt d qₜ = D /Int d rₜ = D %Int d ``` According to [1], we can express Euclidean division by T-division: ``` qₑ = qₜ − I rₑ = rₜ + I · d where I = if rₜ >= 0 then 0 else if d > 0 then 1 else −1 ``` To transform the equations to isolate `qₜ` and `rₜ`, we need to express the `where` clause without `rₜ`. We use 1. `rₑ = 0 <=> rₜ = 0`, and 2. `rₜ ≠ 0 => sgn(rₜ) = sgn(D)` (as per [1]) to rewrite the first `if` to `if (rₑ = 0 || D > 0) ...`. Now we can transform the equations to isolate `qₜ` and `rₜ`, getting (written with `let`): ``` let I = if (rₑ = 0 || D > 0) then 0 else if d > 0 then 1 else -1 in qₜ = qₑ + I rₜ = rₑ - I · d ``` We need two independent equations, so lifting the shared `I` is not beneficial. we can write two `if` expressions per equation. ``` qₜ = if (rₑ = 0 || D > 0) then qₑ else if d > 0 then qₑ + 1 else qₑ - 1 rₜ = if (rₑ = 0 || D > 0) then rₑ else if d > 0 then rₑ - d else rₑ + d ``` Written as SMT hook expressions (coherent with [2]): * (`#1 /Int #2`): `ite (or (= 0 (mod #1 #2)) (>= #1 0)) (div #1 #2) (ite (> #2 0) (+ (div #1 #2) 1) (- (div #1 #2) 1))` * (`#1 %Int #2`): `ite (or (= 0 (mod #1 #2)) (>= #1 0)) (mod #1 #2) (ite (> #2 0) (- (mod #1 #2) #2) (+ (mod #1 #2) #2))` [1] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf [2] https://gist.github.com/Rufflewind/a880e03fb0d13644a1e8 --- .../include/kframework/builtin/domains.md | 10 +- .../tests/integration/test_division_hooks.py | 101 ++++++++++++++++++ 2 files changed, 108 insertions(+), 3 deletions(-) create mode 100644 pyk/src/tests/integration/test_division_hooks.py diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 851e0865dca..675a7338f7a 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1241,9 +1241,13 @@ You can: > left: Int "*Int" Int [function, total, symbol(_*Int_), left, comm, smt-hook(*), hook(INT.mul)] /* FIXME: translate /Int and %Int into smtlib */ - /* /Int and %Int implement t-division, which rounds towards 0 */ - | Int "/Int" Int [function, symbol(_/Int_), left, smt-hook(div), hook(INT.tdiv)] - | Int "%Int" Int [function, symbol(_%Int_), left, smt-hook(mod), hook(INT.tmod)] + /* /Int and %Int implement t-division, which rounds towards 0. SMT hooks need to convert from Euclidian division operations */ + | Int "/Int" Int [function, symbol(_/Int_), left, + smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (div #1 #2) (ite (> #2 0) (+ (div #1 #2) 1) (- (div #1 #2) 1)))), + hook(INT.tdiv)] + | Int "%Int" Int [function, symbol(_%Int_), left, + smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (mod #1 #2) (ite (> #2 0) (- (mod #1 #2) #2) (+ (mod #1 #2) #2)))), + hook(INT.tmod)] /* divInt and modInt implement e-division according to the Euclidean division theorem, therefore the remainder is always positive */ | Int "divInt" Int [function, symbol(_divInt_), left, smt-hook(div), hook(INT.ediv)] | Int "modInt" Int [function, symbol(_modInt_), left, smt-hook(mod), hook(INT.emod)] diff --git a/pyk/src/tests/integration/test_division_hooks.py b/pyk/src/tests/integration/test_division_hooks.py new file mode 100644 index 00000000000..59b815d72e9 --- /dev/null +++ b/pyk/src/tests/integration/test_division_hooks.py @@ -0,0 +1,101 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +import pytest + +from pyk.kore.prelude import BOOL, INT, TRUE, eq_int, int_dv +from pyk.kore.rpc import SatResult +from pyk.kore.syntax import App, Equals, EVar +from pyk.testing import KoreClientTest + +if TYPE_CHECKING: + from typing import Final + + from pyk.kore.rpc import KoreClient + +T_DIVISION_TEST_DATA: Final = ( + # Op , a, b, a Op b + ('/Int', +8, +3, +2), + ('/Int', +8, -3, -2), + ('/Int', -8, +3, -2), + ('/Int', -8, -3, +2), + ('%Int', +8, +3, +2), + ('%Int', +8, -3, +2), + ('%Int', -8, +3, -2), + ('%Int', -8, -3, -2), + ##################### + ('/Int', +1, +2, 0), + ('/Int', +1, -2, 0), + ('/Int', -1, +2, 0), + ('/Int', -1, -2, 0), + ('%Int', +1, +2, +1), + ('%Int', +1, -2, +1), + ('%Int', -1, +2, -1), + ('%Int', -1, -2, -1), + ##################### + ('/Int', +4, +2, +2), + ('/Int', +4, -2, -2), + ('/Int', -4, +2, -2), + ('/Int', -4, -2, +2), + ('%Int', +4, +2, 0), + ('%Int', +4, -2, 0), + ('%Int', -4, +2, 0), + ('%Int', -4, -2, 0), +) + +kore_for = {'/Int': "Lbl'UndsSlsh'Int'Unds'", '%Int': "Lbl'UndsPerc'Int'Unds'"} + + +class TestDivisionHooksHs(KoreClientTest): + KOMPILE_DEFINITION = """ + module SMT + imports INT + endmodule + """ + KOMPILE_MAIN_MODULE = 'SMT' + KOMPILE_ARGS = {'syntax_module': 'SMT'} + LLVM_ARGS = {'syntax_module': 'SMT'} + + @pytest.mark.parametrize( + 'op, a, b, c', + T_DIVISION_TEST_DATA, + ids=[f'get-model: {a} {op} {b} == {c}' for op, a, b, c in T_DIVISION_TEST_DATA], + ) + def test_smt_t_division(self, kore_client: KoreClient, op: str, a: int, b: int, c: int) -> None: + """checks whether the SMT solver returns ``X = c`` for ``X = a op b``.""" + + # Given + pattern = Equals( + BOOL, + INT, + TRUE, + eq_int(App(kore_for[op], (), (int_dv(a), int_dv(b))), EVar('X', INT)), + ) + + # When + actual = kore_client.get_model(pattern, None) + + # Then + expected = SatResult(Equals(INT, INT, EVar('X', INT), int_dv(c))) + + assert actual == expected + + @pytest.mark.parametrize( + 'op, a, b, c', + T_DIVISION_TEST_DATA, + ids=[f'simplify: {a} {op} {b} == {c}' for op, a, b, c in T_DIVISION_TEST_DATA], + ) + def test_llvm_t_division(self, kore_client: KoreClient, op: str, a: int, b: int, c: int) -> None: + """checks whether kore-rpc (HS hook) and booster (LLVM library) both return ``c`` for ``a op b``.""" + + # Given + pattern = App(kore_for[op], (), (int_dv(a), int_dv(b))) + + # When + actual = kore_client.simplify(pattern) + + # Then + expected = (int_dv(c), ()) + + assert actual == expected