diff --git a/package/version b/package/version index 1180819..699c6c6 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.7 +0.1.8 diff --git a/pyproject.toml b/pyproject.toml index 1458aa2..b0dd506 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "ksoroban" -version = "0.1.7" +version = "0.1.8" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/ksoroban/kdist/soroban-semantics/configuration.md b/src/ksoroban/kdist/soroban-semantics/configuration.md index 620aaa1..449517a 100644 --- a/src/ksoroban/kdist/soroban-semantics/configuration.md +++ b/src/ksoroban/kdist/soroban-semantics/configuration.md @@ -46,7 +46,7 @@ module CONFIG syntax HostStack ::= List{HostStackVal, ":"} [symbol(hostStackList)] - syntax HostStackVal ::= ScVal | HostVal + syntax HostStackVal ::= ScVal | HostVal | Bytes syntax InternalCmd ::= #callResult(ValStack, List) [symbol(#callResult)] @@ -154,7 +154,15 @@ These internal commands manages the call stack when calling and returning from a ## `ScVal` Operations -```k +### Creating host objects + +If `SCV` is an object (i.e., not a small value), `allocObject(SCV)` creates a new host object +and pushes a `HostVal` onto the `` that points to the newly created object. +If `SCV` is a container such as a Vector or Map, `allocObject` recursively allocates host objects for its content +but only pushes a single `HostVal` for the entire container onto the stack. +If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly equivalent to `SCV`. + +```k syntax InternalCmd ::= allocObject(ScVal) [symbol(allocObject)] // --------------------------------------------------------------------------- rule [allocObject-small]: @@ -162,12 +170,38 @@ These internal commands manages the call stack when calling and returning from a STACK => toSmall(SCV) : STACK requires toSmallValid(SCV) + // recursively allocate vector items + rule [allocObject-vec]: + allocObject(ScVec(ITEMS)) + => allocObjects(ITEMS) + ~> allocObjectVecAux + ... + + + syntax InternalCmd ::= "allocObjectVecAux" + // ------------------------------------------ + rule [allocObjectVecAux]: + allocObjectVecAux => addObject(ScVec(V)) ... + ScVec(V) : S => S + rule [allocObject]: - allocObject(SCV) => .K ... - OBJS => OBJS ListItem(SCV) - STACK => fromHandleAndTag(indexToHandle(size(OBJS), false), getTag(SCV)) : STACK + allocObject(SCV) => addObject(SCV) ... [owise] + // Allows using `allocObject` in the `` cell + rule [allocObject-instr]: + allocObject(SCV) => #waitCommands ... + (.K => allocObject(SCV)) ... + + syntax InternalCmd ::= addObject(ScVal) [symbol(addObject)] + // -------------------------------------------------------------------------------------------- + rule [addObject]: + addObject(SCV) => .K ... + OBJS => OBJS ListItem(SCV) + STACK + => fromHandleAndTag(indexToHandle(size(OBJS), false), getTag(SCV)) : STACK + + syntax InternalCmd ::= allocObjects (List) [symbol(allocObjects)] | allocObjectsAux (List) [symbol(allocObjectsAux)] | allocObjectsCollect(Int) [symbol(allocObjectsCollect)] @@ -185,20 +219,23 @@ These internal commands manages the call stack when calling and returning from a ... + rule [allocObjectsAux-HostVal]: + allocObjectsAux(ListItem(HV:HostVal) L) + => allocObjectsAux(L) + ~> pushStack(HV) + ... + + rule [allocObjectsCollect]: allocObjectsCollect(LENGTH) => .K ... STACK => ScVec(take(LENGTH, STACK)) : drop(LENGTH, STACK) - syntax HostStack ::= drop(Int, HostStack) [function, total, symbol(HostStack:drop)] - // ------------------------------------------------------------------------------------- - rule drop(N, _ : S) => drop(N -Int 1, S) requires N >Int 0 - rule drop(_, S) => S [owise] - - syntax List ::= take(Int, HostStack) [function, total, symbol(HostStack:take)] - // ------------------------------------------------------------------------------------- - rule take(N, X : S) => ListItem(X) take(N -Int 1, S) requires N >Int 0 - rule take(_, _) => .List [owise] +``` + +### Accessing host objects + +```k syntax InternalInstr ::= loadObject(HostVal) [symbol(loadObject)] // -------------------------------------------------------------------- rule [loadObject-abs]: @@ -220,6 +257,28 @@ These internal commands manages the call stack when calling and returning from a andBool isRelativeObjectHandle(VAL) andBool 0 <=Int getIndex(VAL) andBool getIndex(VAL) loadObject(VAL) => .K ... + S => fromSmall(VAL) : S + requires notBool isObject(VAL) + andBool fromSmallValid(VAL) + + +``` + +### Auxiliary functions + +```k + syntax HostStack ::= drop(Int, HostStack) [function, total, symbol(HostStack:drop)] + // ------------------------------------------------------------------------------------- + rule drop(N, _ : S) => drop(N -Int 1, S) requires N >Int 0 + rule drop(_, S) => S [owise] + + syntax List ::= take(Int, HostStack) [function, total, symbol(HostStack:take)] + // ------------------------------------------------------------------------------------- + rule take(N, X : S) => ListItem(X) take(N -Int 1, S) requires N >Int 0 + rule take(_, _) => .List [owise] ``` ## Call result handling @@ -231,36 +290,47 @@ These internal commands manages the call stack when calling and returning from a rule [callResult]: #callResult( I : SS, RELS) => #callResult(SS, RELS) - ~> HostVal2ScVal(HostVal(I), RELS) + ~> pushStack(HostVal2ScVal(HostVal(I), OBJS, RELS)) ... - - syntax InternalCmd ::= HostVal2ScVal(HostVal, List) [symbol(HostVal2ScVal)] - // -------------------------------------------------------------------------- - rule [HostVal2ScVal-obj-abs]: - HostVal2ScVal(VAL, _RELS) => .K ... OBJS - S => OBJS {{ getIndex(VAL) }} orDefault Void : S + + // Convert HostVals to ScVal recursively + syntax ScVal ::= HostVal2ScVal(HostVal, objs: List, rels: List) [function, total, symbol(HostVal2ScVal)] + // ------------------------------------------------------------------------------------------------------------------- + rule HostVal2ScVal(VAL, OBJS, RELS) => HostVal2ScValRec(OBJS {{ getIndex(VAL) }} orDefault Void, OBJS, RELS) requires isObject(VAL) andBool notBool(isRelativeObjectHandle(VAL)) andBool getIndex(VAL) HostVal2ScVal(VAL, RELS) - => HostVal2ScVal(RELS {{ getIndex(VAL) }} orDefault HostVal(0), RELS) - ... - + rule HostVal2ScVal(VAL, OBJS, RELS) => HostVal2ScVal(RELS {{ getIndex(VAL) }} orDefault HostVal(0), OBJS, RELS) requires isObject(VAL) andBool isRelativeObjectHandle(VAL) andBool getIndex(VAL) HostVal2ScVal(VAL, _RELS) => .K ... - S => fromSmall(VAL) : S + rule HostVal2ScVal(VAL, _OBJS, _RELS) => fromSmall(VAL) requires notBool isObject(VAL) andBool fromSmallValid(VAL) + rule HostVal2ScVal(_, _, _) => Void [owise] + + syntax ScVal ::= HostVal2ScValRec(ScVal, objs: List, rels: List) [function, total, symbol(HostVal2ScValRec)] + // ------------------------------------------------------------------------------------------------------------------- + rule HostVal2ScValRec(ScVec(VEC), OBJS, RELS) => ScVec(HostVal2ScValMany(VEC, OBJS, RELS)) + rule HostVal2ScValRec(SCV, _OBJS, _RELS) => SCV [owise] + + syntax List ::= HostVal2ScValMany(List, objs: List, rels: List) [function, total, symbol(HostVal2ScValMany)] + // ------------------------------------------------------------------------------------------------------------------- + rule HostVal2ScValMany(ListItem(V:HostVal) REST, OBJS, RELS) + => ListItem(HostVal2ScVal(V, OBJS, RELS)) HostVal2ScValMany(REST, OBJS, RELS) + + rule HostVal2ScValMany(ListItem(V:ScVal) REST, OBJS, RELS) + => ListItem(HostVal2ScValRec(V, OBJS, RELS)) HostVal2ScValMany(REST, OBJS, RELS) + + rule HostVal2ScValMany(_, _, _) + => .List [owise] + ``` ```k diff --git a/src/ksoroban/kdist/soroban-semantics/data.md b/src/ksoroban/kdist/soroban-semantics/data.md index 5687482..9b72912 100644 --- a/src/ksoroban/kdist/soroban-semantics/data.md +++ b/src/ksoroban/kdist/soroban-semantics/data.md @@ -31,6 +31,7 @@ storing data on the host side. | ScVec(List) [symbol(SCVal:Vec)] | ScMap(Map) [symbol(SCVal:Map)] | ScAddress(Address) [symbol(SCVal:Address)] + | Symbol(String) [symbol(SCVal:Symbol)] syntax Address ::= AccountId | ContractId syntax AccountId ::= Account(Bytes) [symbol(AccountId)] @@ -121,6 +122,9 @@ module HOST-OBJECT rule getTag(ScVec(_)) => 75 rule getTag(ScMap(_)) => 76 rule getTag(ScAddress(_)) => 77 + rule getTag(Symbol(BS)) => 14 requires lengthString(BS) <=Int 9 + rule getTag(Symbol(BS)) => 74 requires lengthString(BS) >Int 9 + // 64-bit integers that fit in 56 bits syntax Int ::= "#maxU64small" [macro] @@ -184,6 +188,9 @@ module HOST-OBJECT rule fromSmall(VAL) => U128(getBody(VAL)) requires getTag(VAL) ==Int 10 + rule fromSmall(VAL) => Symbol(decode6bit(getBody(VAL))) + requires getTag(VAL) ==Int 14 + // return `Void` for invalid values rule fromSmall(_) => Void [owise] @@ -201,9 +208,10 @@ module HOST-OBJECT rule toSmall(U32(I)) => fromMajorMinorAndTag(I, 0, 4) rule toSmall(I32(I)) => fromMajorMinorAndTag(#unsigned(i32, I), 0, 5) requires definedUnsigned(i32, I) - rule toSmall(U64(I)) => fromBodyAndTag(I, 6) requires I <=Int #maxU64small - rule toSmall(U128(I)) => fromBodyAndTag(I, 10) requires I <=Int #maxU64small - rule toSmall(_) => HostVal(-1) [owise] + rule toSmall(U64(I)) => fromBodyAndTag(I, 6) requires I <=Int #maxU64small + rule toSmall(U128(I)) => fromBodyAndTag(I, 10) requires I <=Int #maxU64small + rule toSmall(Symbol(S)) => fromBodyAndTag(encode6bit(S), 14) requires lengthString(S) <=Int 9 + rule toSmall(_) => HostVal(-1) [owise] syntax Bool ::= toSmallValid(ScVal) [function, total, symbol(toSmallValid)] @@ -211,5 +219,53 @@ module HOST-OBJECT rule toSmallValid(VAL) => toSmall(VAL) =/=K HostVal(-1) + syntax String ::= decode6bit(Int) [function, total, symbol(decode6bit)] + // -------------------------------------------------------------------------------- + rule decode6bit(I) => decode6bit(I >>Int 6) +String decode6bitChar(I &Int 63) requires 0 "" [owise] + + syntax String ::= "sixBitStringTable" [macro] + // ------------------------------------------------------------------------------------------- + rule sixBitStringTable => "_0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefgyahijklmnopqrstuvwxyz" + + syntax String ::= decode6bitChar(Int) [function, total, symbol(decode6bitChar)] + // --------------------------------------------------------------------------------- + rule decode6bitChar(I) => substrString(sixBitStringTable, I -Int 1, I) + + syntax Int ::= encode6bit ( String) [function, total, symbol(encode6bit)] + | encode6bitAux(Int, String) [function, total, symbol(encode6bitAux)] + // -------------------------------------------------------------------------------- + rule encode6bit(S) => encode6bitAux(0, S) + + rule encode6bitAux(A, S) + => encode6bitAux((A < A + [owise] + + syntax Int ::= encode6bitChar(String) [function, total, symbol(encode6bitChar)] + // --------------------------------------------------------------------------------- + rule encode6bitChar(I) => findChar(sixBitStringTable, I, 0) +Int 1 + + syntax Bool ::= validSymbol(String) [function, total, symbol(validSymbol)] + | validSymbolChar(String) [function, total, symbol(validSymbolChar)] + // -------------------------------------------------------------------------------- + rule validSymbol(S) => true + requires lengthString(S) ==Int 0 + rule validSymbol(S) => validSymbolChar(head(S)) andBool validSymbol(tail(S)) + requires 0 false + requires 32 findChar(sixBitStringTable, I, 0) =/=Int -1 + + syntax String ::= head(String) [function, total, symbol(headString)] + | tail(String) [function, total, symbol(tailString)] + // ----------------------------------------------------------------------- + rule head(S) => "" requires lengthString(S) <=Int 0 + rule head(S) => substrString(S, 0, 1) requires lengthString(S) >Int 0 + rule tail(S) => "" requires lengthString(S) <=Int 0 + rule tail(S) => substrString(S, 1, lengthString(S)) requires lengthString(S) >Int 0 + endmodule -``` \ No newline at end of file +``` diff --git a/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md b/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md index c4512cd..6a1dc64 100644 --- a/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md +++ b/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md @@ -1,8 +1,12 @@ ```k requires "integer.md" +requires "symbol.md" +requires "vector.md" module HOSTFUNS imports HOST-INTEGER + imports HOST-SYMBOL + imports HOST-VECTOR endmodule ``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/host/symbol.md b/src/ksoroban/kdist/soroban-semantics/host/symbol.md new file mode 100644 index 0000000..70932d5 --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/host/symbol.md @@ -0,0 +1,40 @@ +# Symbol + +```k +requires "../configuration.md" +requires "../switch.md" +requires "../wasm-ops.md" +requires "integer.md" + +module HOST-SYMBOL + imports CONFIG-OPERATIONS + imports WASM-OPERATIONS + imports HOST-INTEGER + imports SWITCH-SYNTAX + + // symbol_new_from_linear_memory + rule [hostfun-symbol-new-from-linear-memory]: + hostCall ( "b" , "j" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => #memLoad(getMajor(HostVal(LM_POS)), getMajor(HostVal(LEN))) + ~> symbolNewFromLinearMemory + ... + + + 0 |-> < i64 > LM_POS // U32 + 1 |-> < i64 > LEN // U32 + + requires fromSmallValid(HostVal(LM_POS)) + andBool fromSmallValid(HostVal(LEN)) + + + syntax InternalInstr ::= "symbolNewFromLinearMemory" [symbol(symbolNewFromLinearMemory)] + rule [symbolNewFromLinearMemory]: + symbolNewFromLinearMemory + => allocObject(Symbol(Bytes2String(BS))) + ~> returnHostVal + ... + + BS:Bytes : S => S + requires validSymbol(Bytes2String(BS)) +endmodule +``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/host/vector.md b/src/ksoroban/kdist/soroban-semantics/host/vector.md new file mode 100644 index 0000000..8ca0f81 --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/host/vector.md @@ -0,0 +1,89 @@ + +```k +requires "../configuration.md" +requires "../switch.md" +requires "../wasm-ops.md" +requires "integer.md" + +module HOST-VECTOR + imports CONFIG-OPERATIONS + imports WASM-OPERATIONS + imports HOST-INTEGER + imports SWITCH-SYNTAX + + // vec_unpack_to_linear_memory + rule [hostfun-vec-unpack-to-linear-memory]: + hostCall ( "v" , "h" , [ i64 i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(LEN)) + ~> loadObject(HostVal(VALS_POS)) + ~> loadObject(HostVal(VEC)) + ~> vecUnpackToLinearMemory + ~> toSmall(Void) + ... + + + 0 |-> < i64 > VEC // Vec + 1 |-> < i64 > VALS_POS // U32 + 2 |-> < i64 > LEN // U32 + + + syntax InternalInstr ::= "vecUnpackToLinearMemory" [symbol(vecUnpackToLinearMemory)] + // --------------------------------------------------------------------------------------- + rule [vecUnpackToLinearMemory]: + vecUnpackToLinearMemory => #memStore(VALS_POS, Vals2Bytes(VEC)) ... + ScVec(VEC) : U32(VALS_POS) : U32(LEN) : S => S + requires size(VEC) ==Int LEN + + // vec_new_from_linear_memory + rule [hostfun-vec-new-from-linear-memory]: + hostCall ( "v" , "g" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(LEN)) + ~> loadObject(HostVal(VALS_POS)) + ~> vecNewFromLinearMemory + ~> returnHostVal + ... + + + 0 |-> < i64 > VALS_POS // U32 + 1 |-> < i64 > LEN // U32 + + + syntax InternalInstr ::= "vecNewFromLinearMemory" [symbol(vecNewFromLinearMemory)] + | "vecNewFromLinearMemoryAux" [symbol(vecNewFromLinearMemoryAux)] + + // -------------------------------------------------------------------------------------------------------------------- + rule [vecNewFromLinearMemory]: + vecNewFromLinearMemory + => #memLoad(VALS_POS, LEN *Int 8) + ~> vecNewFromLinearMemoryAux + ... + + U32(VALS_POS) : U32(LEN) : S => S + + rule [vecNewFromLinearMemoryAux]: + vecNewFromLinearMemoryAux => #waitCommands ... + (.K => allocObject(ScVec(Bytes2Vals(BS)))) ... + BS : S => S + + + syntax Bytes ::= Vals2Bytes(List) [function, total] + // ----------------------------------------------------------------------------------------- + rule Vals2Bytes(ListItem(HostVal(V)) REST) => Int2Bytes(8, V, LE) +Bytes Vals2Bytes(REST) + rule Vals2Bytes(_) => .Bytes + [owise] + + syntax List ::= Bytes2Vals(Bytes) [function, total] + // ----------------------------------------------------------------------------------------- + rule Bytes2Vals(BS) => ListItem(parseHostVal(substrBytes(BS, 0, 8))) + Bytes2Vals(substrBytes(BS, 8, lengthBytes(BS))) + requires lengthBytes(BS) >=Int 8 + + rule Bytes2Vals(_) => .List + [owise] + + syntax HostVal ::= parseHostVal(Bytes) [function, total] + // ------------------------------------------------------------- + rule parseHostVal(BS) => HostVal(Bytes2Int(BS, LE, Unsigned)) + +endmodule +``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/kasmer.md b/src/ksoroban/kdist/soroban-semantics/kasmer.md index 7c965d3..d82dce3 100644 --- a/src/ksoroban/kdist/soroban-semantics/kasmer.md +++ b/src/ksoroban/kdist/soroban-semantics/kasmer.md @@ -24,6 +24,8 @@ module KASMER-SYNTAX-COMMON syntax Steps ::= List{Step, ""} [symbol(kasmerSteps)] + syntax String ::= str(WasmString) [function, total] + endmodule module KASMER @@ -37,6 +39,9 @@ module KASMER 1 + rule str(WS) => unescape(#parseWasmString(WS)) + rule str(.WasmString) => "" + rule [load-program]: (_S:Step _SS:Steps) #as PGM => .Steps _ => PGM diff --git a/src/ksoroban/kdist/soroban-semantics/wasm-ops.md b/src/ksoroban/kdist/soroban-semantics/wasm-ops.md new file mode 100644 index 0000000..c5101c3 --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/wasm-ops.md @@ -0,0 +1,67 @@ + +```k +requires "configuration.md" +module WASM-OPERATIONS + imports CONFIG-OPERATIONS +``` + +## Memory Operations + +```k + syntax InternalInstr ::= #memStore ( offset: Int , bytes: Bytes ) + // ----------------------------------------------------------------- + rule [memStore]: + #memStore(OFFSET, BS) => .K ... + MODIDX:Int + + MODIDX + 0 |-> MEMADDR + ... + + + MEMADDR + SIZE + DATA => #setBytesRange(DATA, OFFSET, BS) + ... + + requires #signed(i32 , OFFSET) +Int lengthBytes(BS) <=Int (SIZE *Int #pageSize()) + andBool 0 <=Int #signed(i32 , OFFSET) + [preserves-definedness] // setBytesRange total, MEMADDR key existed prior in map + + rule [memStore-trap]: + #memStore(_, _) => trap ... + [owise] + + syntax InternalInstr ::= #memLoad ( offset: Int , length: Int ) + // --------------------------------------------------------------- + rule [memLoad-zero-length]: + #memLoad(_, 0) => .K ... + STACK => .Bytes : STACK + + rule [memLoad]: + #memLoad(OFFSET, LENGTH) => .K ... + STACK => #getBytesRange(DATA, OFFSET, LENGTH) : STACK + MODIDX:Int + + MODIDX + 0 |-> MEMADDR + ... + + + MEMADDR + SIZE + DATA + ... + + requires #signed(i32 , LENGTH) >Int 0 + andBool #signed(i32 , OFFSET) >=Int 0 + andBool #signed(i32 , OFFSET) +Int #signed(i32 , LENGTH) <=Int (SIZE *Int #pageSize()) + + rule [memLoad-trap]: + #memLoad(_, _) => trap ... + [owise] +``` + +```k +endmodule +``` \ No newline at end of file diff --git a/src/tests/integration/data/symbol_small.wast b/src/tests/integration/data/symbol_small.wast new file mode 100644 index 0000000..7ed010e --- /dev/null +++ b/src/tests/integration/data/symbol_small.wast @@ -0,0 +1,47 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +(module + (type (;0;) (func (param i64 i64) (result i64))) + (type (;1;) (func (result i64))) + (type (;2;) (func (param i32 i32) (result i64))) + (type (;3;) (func)) + (import "b" "j" (func $symbol_new_from_linear_memory (type 0))) + (func $symbol_small (type 1) (result i64) + ;; address + i64.const 0 + i64.const 32 + i64.shl + i64.const 4 + i64.or + + ;; size + i64.const 8 + i64.const 32 + i64.shl + i64.const 4 + i64.or + call $symbol_new_from_linear_memory) + (memory (data "_ABCabc0")) + (export "symbol_small" (func $symbol_small))) +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm", + .List +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "symbol_small", + .List, + Symbol(str("_ABCabc0")) +) + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/symbols.wast b/src/tests/integration/data/symbols.wast new file mode 100644 index 0000000..7f67ce3 --- /dev/null +++ b/src/tests/integration/data/symbols.wast @@ -0,0 +1,175 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +;; #![no_std] +;; use soroban_sdk::{contract, contractimpl, Env, Symbol}; +;; +;; #[contract] +;; pub struct IncrementContract; +;; +;; #[contractimpl] +;; impl IncrementContract { +;; pub fn symbol_small(env: Env) -> Symbol { +;; Symbol::new(&env, "_ABCabc0") +;; } +;; +;; pub fn symbol_object(env: Env) -> Symbol { +;; Symbol::new(&env, "_ABCabc0123456789qwerty") +;; } +;; } +(module $soroban_increment_contract.wasm + (type (;0;) (func (param i64 i64) (result i64))) + (type (;1;) (func (result i64))) + (type (;2;) (func (param i32 i32) (result i64))) + (type (;3;) (func)) + (import "b" "j" (func $_ZN17soroban_env_guest5guest3buf29symbol_new_from_linear_memory17h79212fcc6ba452faE (type 0))) + (func $symbol_small (type 1) (result i64) + i32.const 1048576 + i32.const 8 + call $_ZN11soroban_sdk6symbol6Symbol3new17hd0e466fd0e8d4f8eE) + (func $_ZN11soroban_sdk6symbol6Symbol3new17hd0e466fd0e8d4f8eE (type 2) (param i32 i32) (result i64) + (local i32 i64 i64 i32) + i32.const 0 + local.set 2 + i64.const 0 + local.set 3 + block ;; label = @1 + block ;; label = @2 + loop ;; label = @3 + local.get 1 + local.get 2 + i32.eq + br_if 1 (;@2;) + local.get 2 + i32.const 9 + i32.eq + br_if 2 (;@1;) + i64.const 1 + local.set 4 + block ;; label = @4 + local.get 0 + local.get 2 + i32.add + i32.load8_u + local.tee 5 + i32.const 95 + i32.eq + br_if 0 (;@4;) + local.get 5 + i64.extend_i32_u + local.set 4 + block ;; label = @5 + local.get 5 + i32.const -48 + i32.add + i32.const 10 + i32.lt_u + br_if 0 (;@5;) + block ;; label = @6 + local.get 5 + i32.const -65 + i32.add + i32.const 26 + i32.lt_u + br_if 0 (;@6;) + local.get 5 + i32.const -97 + i32.add + i32.const 25 + i32.gt_u + br_if 5 (;@1;) + local.get 4 + i64.const -59 + i64.add + local.set 4 + br 2 (;@4;) + end + local.get 4 + i64.const -53 + i64.add + local.set 4 + br 1 (;@4;) + end + local.get 4 + i64.const -46 + i64.add + local.set 4 + end + local.get 2 + i32.const 1 + i32.add + local.set 2 + local.get 4 + local.get 3 + i64.const 6 + i64.shl + i64.or + local.set 3 + br 0 (;@3;) + end + end + local.get 3 + i64.const 8 + i64.shl + i64.const 14 + i64.or + return + end + local.get 0 + i64.extend_i32_u + i64.const 32 + i64.shl + i64.const 4 + i64.or + local.get 1 + i64.extend_i32_u + i64.const 32 + i64.shl + i64.const 4 + i64.or + call $_ZN17soroban_env_guest5guest3buf29symbol_new_from_linear_memory17h79212fcc6ba452faE) + (func $symbol_object (type 1) (result i64) + i32.const 1048584 + i32.const 23 + call $_ZN11soroban_sdk6symbol6Symbol3new17hd0e466fd0e8d4f8eE) + (func $_ (type 3)) + (memory (;0;) 17) + (global $__stack_pointer (mut i32) (i32.const 1048576)) + (global (;1;) i32 (i32.const 1048607)) + (global (;2;) i32 (i32.const 1048608)) + (export "memory" (memory 0)) + (export "symbol_small" (func $symbol_small)) + (export "symbol_object" (func $symbol_object)) + (export "_" (func $_)) + (export "__data_end" (global 1)) + (export "__heap_base" (global 2)) + (data $.rodata (i32.const 1048576) "_ABCabc0_ABCabc0123456789qwerty")) +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm", + .List +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "symbol_small", + .List, + Symbol(str("_ABCabc0")) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "symbol_object", + .List, + Symbol(str("_ABCabc0123456789qwerty")) +) + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/tuple_to_vec.wast b/src/tests/integration/data/tuple_to_vec.wast new file mode 100644 index 0000000..b43209f --- /dev/null +++ b/src/tests/integration/data/tuple_to_vec.wast @@ -0,0 +1,236 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", + +;; /// `tuple_to_vec` takes a tuple and returns elements in reverse order + +;; #![no_std] +;; use soroban_sdk::{contract, contractimpl, Env, contracttype, Vec}; +;; +;; #[contract] +;; pub struct IncrementContract; +;; +;; #[contracttype] +;; #[derive(Debug, Clone)] +;; pub struct Point(u32, u32, u32); +;; +;; #[contractimpl] +;; impl IncrementContract { +;; +;; pub fn tuple_to_vec(env: Env, p: Point) -> Vec { +;; Vec::from_array(&env, [p.2, p.1, p.0]) +;; } +;; } + +(module $tuple_to_vec.wasm + (type (;0;) (func (param i64 i64 i64) (result i64))) + (type (;1;) (func (param i64 i64) (result i64))) + (type (;2;) (func (param i64) (result i64))) + (type (;3;) (func)) + (import "v" "h" (func $_ZN17soroban_env_guest5guest3vec27vec_unpack_to_linear_memory17h43fbd7ea3c12e8b3E (type 0))) + (import "v" "g" (func $_ZN17soroban_env_guest5guest3vec26vec_new_from_linear_memory17h31f0f68089eaf9f9E (type 1))) + (func $tuple_to_vec (type 2) (param i64) (result i64) + (local i32 i32 i64 i64 i64 i32) + global.get $__stack_pointer + i32.const 48 + i32.sub + local.tee 1 + global.set $__stack_pointer + block ;; label = @1 + local.get 0 + i64.const 255 + i64.and + i64.const 75 + i64.ne + br_if 0 (;@1;) + i32.const 0 + local.set 2 + block ;; label = @2 + loop ;; label = @3 + local.get 2 + i32.const 24 + i32.eq + br_if 1 (;@2;) + local.get 1 + i32.const 24 + i32.add + local.get 2 + i32.add + i64.const 2 + i64.store + local.get 2 + i32.const 8 + i32.add + local.set 2 + br 0 (;@3;) + end + end + local.get 0 + local.get 1 + i32.const 24 + i32.add + i64.extend_i32_u + local.tee 3 + i64.const 32 + i64.shl + i64.const 4 + i64.or + i64.const 12884901892 + call $_ZN17soroban_env_guest5guest3vec27vec_unpack_to_linear_memory17h43fbd7ea3c12e8b3E + drop + local.get 1 + i64.load offset=24 + local.tee 0 + i64.const 255 + i64.and + i64.const 4 + i64.ne + br_if 0 (;@1;) + local.get 1 + i64.load offset=32 + local.tee 4 + i64.const 255 + i64.and + i64.const 4 + i64.ne + br_if 0 (;@1;) + local.get 1 + i64.load offset=40 + local.tee 5 + i64.const 255 + i64.and + i64.const 4 + i64.ne + br_if 0 (;@1;) + local.get 1 + local.get 0 + i64.const 32 + i64.shr_u + i32.wrap_i64 + i32.store offset=20 + local.get 1 + local.get 4 + i64.const 32 + i64.shr_u + i32.wrap_i64 + i32.store offset=16 + local.get 1 + local.get 5 + i64.const 32 + i64.shr_u + i64.store32 offset=12 + i32.const 0 + local.set 2 + loop ;; label = @2 + block ;; label = @3 + local.get 2 + i32.const 24 + i32.ne + br_if 0 (;@3;) + local.get 1 + i32.const 24 + i32.add + local.set 6 + i32.const 0 + local.set 2 + block ;; label = @4 + loop ;; label = @5 + local.get 2 + i32.const 12 + i32.eq + br_if 1 (;@4;) + local.get 6 + local.get 1 + i32.const 12 + i32.add + local.get 2 + i32.add + i64.load32_u + i64.const 32 + i64.shl + i64.const 4 + i64.or + i64.store + local.get 2 + i32.const 4 + i32.add + local.set 2 + local.get 6 + i32.const 8 + i32.add + local.set 6 + br 0 (;@5;) + end + end + local.get 3 + i64.const 32 + i64.shl + i64.const 4 + i64.or + i64.const 12884901892 + call $_ZN17soroban_env_guest5guest3vec26vec_new_from_linear_memory17h31f0f68089eaf9f9E + local.set 0 + local.get 1 + i32.const 48 + i32.add + global.set $__stack_pointer + local.get 0 + return + end + local.get 1 + i32.const 24 + i32.add + local.get 2 + i32.add + i64.const 2 + i64.store + local.get 2 + i32.const 8 + i32.add + local.set 2 + br 0 (;@2;) + end + end + unreachable + unreachable) + (func $_ (type 3)) + (memory (;0;) 16) + (global $__stack_pointer (mut i32) (i32.const 1048576)) + (global (;1;) i32 (i32.const 1048576)) + (global (;2;) i32 (i32.const 1048576)) + (export "memory" (memory 0)) + (export "tuple_to_vec" (func $tuple_to_vec)) + (export "_" (func $_)) + (export "__data_end" (global 1)) + (export "__heap_base" (global 2))) +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-ctr"), + b"test-wasm", + .List +) + +callTx( + Account(b"test-caller"), + Contract(b"test-ctr"), + "tuple_to_vec", + ListItem( + ScVec( + ListItem(U32(1)) + ListItem(U32(2)) + ListItem(U32(3)) + ) + ), + ScVec( + ListItem(U32(3)) + ListItem(U32(2)) + ListItem(U32(1)) + ) +) + +setExitCode(0) \ No newline at end of file