Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adding support for MInt{128} #1160

Merged
merged 6 commits into from
Oct 23, 2024
Merged

Adding support for MInt{128} #1160

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
c048aca
Adding support for `MInt{128}` hashing and k equality function
Robertorosmaninho Oct 21, 2024
c609e81
Updating `hash-mint` tests with new `MInt{128}`
Robertorosmaninho Oct 21, 2024
de2996f
Formatting
Robertorosmaninho Oct 21, 2024
a8fd62c
Modiying test to only verify the K cell!
Robertorosmaninho Oct 22, 2024
8ba616e
Deleting temp file and unused rule on the test
Robertorosmaninho Oct 22, 2024
4823404
Updating kore test
Robertorosmaninho Oct 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions in.kore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),Lblfoo'LParRParUnds'TEST'Unds'KItem{}())))
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved
6 changes: 6 additions & 0 deletions runtime/collections/hash.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,12 @@ void k_hash(block *arg, void *h) {
add_hash64(h, *intptr);
break;
}
case MINT_LAYOUT + 128: {
auto *intptr = (uint64_t *)(argintptr + offset);
add_hash64(h, intptr[0]);
add_hash64(h, intptr[1]);
break;
}
case MINT_LAYOUT + 160: {
auto *intptr = (uint64_t *)(argintptr + offset);
add_hash64(h, intptr[0]);
Expand Down
10 changes: 10 additions & 0 deletions runtime/collections/kelemle.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,16 @@ bool hook_KEQUAL_eq(block *arg1, block *arg2) {
}
break;
}
case MINT_LAYOUT + 128: {
auto *child1ptr = (int64_t *)(child1intptr);
auto *child2ptr = (int64_t *)(child2intptr);
bool cmp
= child1ptr[0] == child2ptr[0] && child1ptr[1] == child2ptr[1];
if (!cmp) {
return false;
}
break;
}
case MINT_LAYOUT + 160: {
auto *child1ptr = (int64_t *)(child1intptr);
auto *child2ptr = (int64_t *)(child2intptr);
Expand Down
677 changes: 416 additions & 261 deletions test/defn/hash-mint.kore
View file
Open in desktop

Large diffs are not rendered by default.

9 changes: 7 additions & 2 deletions test/defn/k-files/hash-mint.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,20 @@ module HASH-MINT

syntax MInt{160}
syntax MInt{256}
syntax MInt{128}

configuration <k> $PGM:K </k>
<state> 0p256 |-> 1p256 0p160 |-> 1p160 </state>
<state> 0p256 |-> 1p256 0p160 |-> 1p160 0p128 |-> 1p128 </state>

syntax KItem ::= foo() | bar()
syntax KItem ::= foo() | bar() | baz()

rule <k> foo() => bar() ~> State [ 0p256 ] ...</k>
<state> State </state>
rule <k> bar() => baz() ~> State [ 0p160 ] ...</k>
<state> State </state>
rule <k> bar() => State [ 0p160 ] ...</k>
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved
<state> State </state> [owise]
rule <k> baz() => State [ 0p128 ] ...</k>
<state> State </state>

endmodule
2 changes: 1 addition & 1 deletion test/input/hash-mint.in
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),Lblfoo'LParRParUnds'TEST'Unds'KItem{}())))
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),Lblfoo'LParRParUnds'HASH-MINT'Unds'KItem{}())))
2 changes: 1 addition & 1 deletion test/output/hash-mint.out.diff
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("1p160")),kseq{}(inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("1p256")),dotk{}()))),Lbl'-LT-'state'-GT-'{}(\left-assoc{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("0p256")),inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("1p256"))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("0p160")),inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("1p160")))))),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))
Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortMInt{Sort128{}}, SortKItem{}}(\dv{SortMInt{Sort128{}}}("1p128")),kseq{}(inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("1p160")),kseq{}(inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("1p256")),dotk{}()))))
Loading