Skip to content

Commit d7efaf7

Browse files
Implementing hook_LIST_updateMInt in bytes.cpp for supporting MInt{64} only
Adding `list-update` unit test
1 parent 5d7dd50 commit d7efaf7

File tree

5 files changed

+2971
-0
lines changed

5 files changed

+2971
-0
lines changed

runtime/collections/lists.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,16 @@ list hook_LIST_make(SortInt len, SortKItem value) {
140140
return {length, value};
141141
}
142142

143+
list hook_LIST_updateMInt(SortList list, uint64_t idx, SortKItem value) {
144+
if (idx >= list->size()) {
145+
KLLVM_HOOK_INVALID_ARGUMENT(
146+
"Index out of range for update64: index={}, size={}", idx,
147+
list->size());
148+
}
149+
150+
return list->set(idx, value);
151+
}
152+
143153
list hook_LIST_update_long(SortList list, size_t idx, SortKItem value) {
144154
if (idx >= list->size()) {
145155
KLLVM_HOOK_INVALID_ARGUMENT(
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
module LIST-UPDATE
2+
3+
imports INT
4+
imports MINT
5+
imports BOOL
6+
imports LIST
7+
imports K-EQUAL
8+
9+
syntax MInt{64}
10+
11+
syntax List ::= "listOfMInt" [macro]
12+
rule listOfMInt => ListItem(2p64) (ListItem(3p64) (ListItem(4p64) .List))
13+
14+
syntax Bool ::= "testListUpdate" [function]
15+
// This function only support MInt{64} for now, use MInt{256} can cause undefined behavior
16+
rule testListUpdate => listOfMInt[2p64 <- 10p64] ==K listOfMInt[2 <- 10p64]
17+
18+
endmodule

0 commit comments

Comments
 (0)