diff --git a/package/version b/package/version index f8bc4c6..d8a023e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.18 +0.1.19 diff --git a/pyproject.toml b/pyproject.toml index d71914c..4628faa 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "ksoroban" -version = "0.1.18" +version = "0.1.19" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/ksoroban/kdist/soroban-semantics/data.md b/src/ksoroban/kdist/soroban-semantics/data.md index 27356cf..db87512 100644 --- a/src/ksoroban/kdist/soroban-semantics/data.md +++ b/src/ksoroban/kdist/soroban-semantics/data.md @@ -3,6 +3,8 @@ [Documentation - Host Value Type](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#host-value-type) ```k +requires "errors.md" + module HOST-OBJECT-SYNTAX imports BOOL-SYNTAX imports INT-SYNTAX @@ -10,6 +12,7 @@ module HOST-OBJECT-SYNTAX imports STRING-SYNTAX imports LIST imports MAP + imports ERRORS ``` ## ScVal @@ -48,8 +51,9 @@ various contexts: ```k syntax ScVal - ::= SCBool(Bool) [symbol(SCVal:Bool)] + ::= SCBool(Bool) [symbol(SCVal:Bool)] | "Void" [symbol(SCVal:Void)] + | Error(ErrorType, Int) [symbol(SCVal:Error)] | U32(Int) [symbol(SCVal:U32)] | I32(Int) [symbol(SCVal:I32)] | U64(Int) [symbol(SCVal:U64)] @@ -97,10 +101,12 @@ module HOST-OBJECT imports WASM syntax Int ::= getMajor(HostVal) [function, total, symbol(getMajor)] + | getMinor(HostVal) [function, total, symbol(getMinor)] | getTag(HostVal) [function, total, symbol(getTag)] | getBody(HostVal) [function, total, symbol(getBody)] // ----------------------------------------------------------------------- rule getMajor(HostVal(I)) => I >>Int 32 + rule getMinor(HostVal(I)) => (I &Int (#pow(i32) -Int 1)) >>Int 8 rule getTag(HostVal(I)) => I &Int 255 rule getBody(HostVal(I)) => I >>Int 8 @@ -139,6 +145,7 @@ module HOST-OBJECT rule getTag(SCBool(true)) => 0 rule getTag(SCBool(false)) => 1 rule getTag(Void) => 2 + rule getTag(Error(_,_)) => 3 rule getTag(U32(_)) => 4 rule getTag(I32(_)) => 5 rule getTag(U64(I)) => 6 requires I <=Int #maxU64small @@ -204,6 +211,10 @@ module HOST-OBJECT rule fromSmall(VAL) => Void requires getTag(VAL) ==Int 2 + rule fromSmall(VAL) => Error(Int2ErrorType(getMinor(VAL)), getMajor(VAL)) + requires getTag(VAL) ==Int 3 + andBool Int2ErrorTypeValid(getMinor(VAL)) + rule fromSmall(VAL) => U32(getMajor(VAL)) requires getTag(VAL) ==Int 4 rule fromSmall(VAL) => I32(#signed(i32, getMajor(VAL))) @@ -232,6 +243,7 @@ module HOST-OBJECT rule toSmall(SCBool(false)) => fromMajorMinorAndTag(0, 0, 0) rule toSmall(SCBool(true)) => fromMajorMinorAndTag(0, 0, 1) rule toSmall(Void) => fromMajorMinorAndTag(0, 0, 2) + rule toSmall(Error(TYP, I)) => fromMajorMinorAndTag(I, ErrorType2Int(TYP), 3) rule toSmall(U32(I)) => fromMajorMinorAndTag(I, 0, 4) rule toSmall(I32(I)) => fromMajorMinorAndTag(#unsigned(i32, I), 0, 5) requires definedUnsigned(i32, I) diff --git a/src/ksoroban/kdist/soroban-semantics/errors.md b/src/ksoroban/kdist/soroban-semantics/errors.md new file mode 100644 index 0000000..270ad1e --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/errors.md @@ -0,0 +1,73 @@ +# Errors + + +```k +module ERRORS + imports BOOL + imports INT + + syntax ErrorType ::= "ErrContract" [symbol(ErrorType:Contract)] + | "ErrWasmVm" [symbol(ErrorType:WasmVm)] + | "ErrContext" [symbol(ErrorType:Context)] + | "ErrStorage" [symbol(ErrorType:Storage)] + | "ErrObject" [symbol(ErrorType:Object)] + | "ErrCrypto" [symbol(ErrorType:Crypto)] + | "ErrEvents" [symbol(ErrorType:Events)] + | "ErrBudget" [symbol(ErrorType:Budget)] + | "ErrValue" [symbol(ErrorType:Value)] + | "ErrAuth" [symbol(ErrorType:Auth)] + + syntax Int ::= ErrorType2Int(ErrorType) [function, total, symbol(ErrorType2Int)] + // ------------------------------------------------------------------------------------- + rule ErrorType2Int(ErrContract) => 0 + rule ErrorType2Int(ErrWasmVm) => 1 + rule ErrorType2Int(ErrContext) => 2 + rule ErrorType2Int(ErrStorage) => 3 + rule ErrorType2Int(ErrObject) => 4 + rule ErrorType2Int(ErrCrypto) => 5 + rule ErrorType2Int(ErrEvents) => 6 + rule ErrorType2Int(ErrBudget) => 7 + rule ErrorType2Int(ErrValue) => 8 + rule ErrorType2Int(ErrAuth) => 9 + + syntax ErrorType ::= Int2ErrorType(Int) [function, total, symbol(Int2ErrorType)] + // ---------------------------------------------------------------------------------- + rule Int2ErrorType(1) => ErrWasmVm + rule Int2ErrorType(2) => ErrContext + rule Int2ErrorType(3) => ErrStorage + rule Int2ErrorType(4) => ErrObject + rule Int2ErrorType(5) => ErrCrypto + rule Int2ErrorType(6) => ErrEvents + rule Int2ErrorType(7) => ErrBudget + rule Int2ErrorType(8) => ErrValue + rule Int2ErrorType(9) => ErrAuth + rule Int2ErrorType(_) => ErrContract [owise] + + syntax Bool ::= Int2ErrorTypeValid(Int) [function, total, symbol(Int2ErrorTypeValid)] + // --------------------------------------------------------------------------------------- + rule Int2ErrorTypeValid(I) => 0 <=Int I andBool I <=Int 9 + + syntax Int ::= "ArithDomain" [macro] + | "IndexBounds" [macro] + | "InvalidInput" [macro] + | "MissingValue" [macro] + | "ExistingValue" [macro] + | "ExceededLimit" [macro] + | "InvalidAction" [macro] + | "InternalError" [macro] + | "UnexpectedType" [macro] + | "UnexpectedSize" [macro] + // -------------------------------------------- + rule ArithDomain => 0 + rule IndexBounds => 1 + rule InvalidInput => 2 + rule MissingValue => 3 + rule ExistingValue => 4 + rule ExceededLimit => 5 + rule InvalidAction => 6 + rule InternalError => 7 + rule UnexpectedType => 8 + rule UnexpectedSize => 9 + +endmodule +``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/host/context.md b/src/ksoroban/kdist/soroban-semantics/host/context.md index 0337c2d..e417fea 100644 --- a/src/ksoroban/kdist/soroban-semantics/host/context.md +++ b/src/ksoroban/kdist/soroban-semantics/host/context.md @@ -19,6 +19,34 @@ Return the current ledger sequence number as `U32`. .Map SEQ_NUM +``` + +## fail_with_error + +```k + rule [hostfun-fail-with-error]: + hostCall ( "x" , "5" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) ~> _REST + => .K + + (.K => pushStack(fromSmall(HostVal(ERR)))) ... + + 0 |-> < i64 > ERR + + requires fromSmallValid(HostVal(ERR)) + andBool getTag(HostVal(ERR)) ==Int 3 + andBool Int2ErrorType(getMinor(HostVal(ERR))) ==K ErrContract // error type must be ErrContract + + rule [hostfun-fail-with-error-wrong-type]: + hostCall ( "x" , "5" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) ~> _REST + => .K + + (.K => pushStack(Error(ErrContext, UnexpectedType))) ... + + 0 |-> < i64 > ERR + + requires fromSmallValid(HostVal(ERR)) + andBool getTag(HostVal(ERR)) ==Int 3 + andBool Int2ErrorType(getMinor(HostVal(ERR))) =/=K ErrContract endmodule ``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/switch.md b/src/ksoroban/kdist/soroban-semantics/switch.md index fb31b4d..2eab37c 100644 --- a/src/ksoroban/kdist/soroban-semantics/switch.md +++ b/src/ksoroban/kdist/soroban-semantics/switch.md @@ -34,6 +34,16 @@ module SWITCH stack after the function execution. ```k + rule [endWasm-error]: + #endWasm + => popCallState + ~> popWorldState + ... + + .K + (Error(_,_) #as ERR) : _ => ERR : .HostStack + [priority(40)] + rule [endWasm]: #endWasm => popCallState @@ -44,6 +54,12 @@ module SWITCH .K RELS STACK + [priority(50)] + + rule [endWasm-trap]: + #endWasm ... + trap => .K + S => Error(ErrContext, InvalidAction) : S ``` diff --git a/src/tests/integration/data/errors.wast b/src/tests/integration/data/errors.wast new file mode 100644 index 0000000..09aeaf2 --- /dev/null +++ b/src/tests/integration/data/errors.wast @@ -0,0 +1,169 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +;; #![no_std] +;; use soroban_sdk::{contract, contracterror, contractimpl, panic_with_error, Env}; +;; +;; #[contracterror] +;; #[derive(Copy, Clone, Debug, Eq, PartialEq, PartialOrd, Ord)] +;; #[repr(u32)] +;; pub enum CustomError { +;; CustomErrorCode1 = 1, +;; CustomErrorCode2 = 2, +;; } +;; +;; #[contract] +;; pub struct IncrementContract; +;; +;; #[contractimpl] +;; impl IncrementContract { +;; /// Increment increments an internal counter, and returns the value. Errors +;; /// if the value is attempted to be incremented past 5. +;; pub fn custom_fail(_env: Env, p: bool) -> Result { +;; Err( +;; match p { +;; false => CustomError::CustomErrorCode1, +;; true => CustomError::CustomErrorCode2 +;; } +;; ) +;; } +;; +;; pub fn panic_fail(_env: Env) { +;; panic!() +;; } +;; +;; pub fn panic_with_error_fail(env: Env, p: bool) { +;; panic_with_error!(env, match p { +;; false => CustomError::CustomErrorCode1, +;; true => CustomError::CustomErrorCode2 +;; }) +;; } +;; } +;; mod test; +(module $soroban_errors_contract.wasm + (type (;0;) (func (param i64) (result i64))) + (type (;1;) (func (result i64))) + (type (;2;) (func)) + (type (;3;) (func (param i64))) + (import "x" "5" (func $_ZN17soroban_env_guest5guest7context15fail_with_error17h712c0ad18a303073E (type 0))) + (func $custom_fail (type 0) (param i64) (result i64) + (local i32) + block ;; label = @1 + local.get 0 + i32.wrap_i64 + i32.const 255 + i32.and + local.tee 1 + i32.const 2 + i32.lt_u + br_if 0 (;@1;) + unreachable + unreachable + end + i64.const 8589934595 + i64.const 4294967299 + local.get 1 + select) + (func $panic_fail (type 1) (result i64) + call $_ZN23soroban_errors_contract17IncrementContract10panic_fail19panic_cold_explicit17h500069efcbed89a3E + unreachable) + (func $_ZN23soroban_errors_contract17IncrementContract10panic_fail19panic_cold_explicit17h500069efcbed89a3E (type 2) + call $_ZN4core9panicking14panic_explicit17h47855c360709a39dE + unreachable) + (func $panic_with_error_fail (type 0) (param i64) (result i64) + (local i32) + block ;; label = @1 + local.get 0 + i32.wrap_i64 + i32.const 255 + i32.and + local.tee 1 + i32.const 2 + i32.ge_u + br_if 0 (;@1;) + i64.const 8589934595 + i64.const 4294967299 + local.get 1 + select + call $_ZN70_$LT$soroban_sdk..env..Env$u20$as$u20$soroban_env_common..env..Env$GT$15fail_with_error17h4649cb3441ec7f31E + end + unreachable + unreachable) + (func $_ZN70_$LT$soroban_sdk..env..Env$u20$as$u20$soroban_env_common..env..Env$GT$15fail_with_error17h4649cb3441ec7f31E (type 3) (param i64) + local.get 0 + call $_ZN17soroban_env_guest5guest7context15fail_with_error17h712c0ad18a303073E + drop) + (func $_ZN4core9panicking14panic_explicit17h47855c360709a39dE (type 2) + call $_ZN4core9panicking13panic_display17hbd841ae85eb3dff4E + unreachable) + (func $_ZN4core9panicking9panic_fmt17h5c7ce52813e94bcdE (type 2) + unreachable + unreachable) + (func $_ZN4core9panicking13panic_display17hbd841ae85eb3dff4E (type 2) + call $_ZN4core9panicking9panic_fmt17h5c7ce52813e94bcdE + unreachable) + (func $_ (type 2)) + (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 "custom_fail" (func $custom_fail)) + (export "panic_fail" (func $panic_fail)) + (export "panic_with_error_fail" (func $panic_with_error_fail)) + (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-sc"), + b"test-wasm", + .List +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "panic_fail", + .List, + Error(ErrContext, InvalidAction) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "custom_fail", + ListItem(SCBool(false)), + Error(ErrContract, 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "custom_fail", + ListItem(SCBool(true)), + Error(ErrContract, 2) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "panic_with_error_fail", + ListItem(SCBool(false)), + Error(ErrContract, 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "panic_with_error_fail", + ListItem(SCBool(true)), + Error(ErrContract, 2) +) + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/increment_panic.wast b/src/tests/integration/data/increment_panic.wast new file mode 100644 index 0000000..4cb225b --- /dev/null +++ b/src/tests/integration/data/increment_panic.wast @@ -0,0 +1,221 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +;; pub struct IncrementContract; +;; +;; #[contractimpl] +;; impl IncrementContract { +;; pub fn increment(env: Env) -> u32 { +;; let mut count: u32 = env.storage().instance().get(&COUNTER).unwrap_or(0); +;; count += 1; +;; env.storage().instance().set(&COUNTER, &count); +;; count +;; } +;; +;; pub fn increment_panic(env: Env) -> u32 { +;; let mut count: u32 = env.storage().instance().get(&COUNTER).unwrap_or(0); +;; count += 1; +;; env.storage().instance().set(&COUNTER, &count); +;; panic!() +;; } +;; } +(module $soroban_increment_contract.wasm + (type (;0;) (func (param i64 i64) (result i64))) + (type (;1;) (func (param i64 i64 i64) (result i64))) + (type (;2;) (func (param i32))) + (type (;3;) (func (result i64))) + (type (;4;) (func)) + (import "l" "0" (func $_ZN17soroban_env_guest5guest6ledger17has_contract_data17he4c980238e117d85E (type 0))) + (import "l" "1" (func $_ZN17soroban_env_guest5guest6ledger17get_contract_data17h4f075bb2afc11861E (type 0))) + (import "l" "_" (func $_ZN17soroban_env_guest5guest6ledger17put_contract_data17hbcf4a2a09b350844E (type 1))) + (func $_ZN11soroban_sdk7storage8Instance3get17hbc53ccbc4676241bE (type 2) (param i32) + (local i32 i64 i32) + block ;; label = @1 + block ;; label = @2 + block ;; label = @3 + i64.const 253576579652878 + i64.const 2 + call $_ZN17soroban_env_guest5guest6ledger17has_contract_data17he4c980238e117d85E + i64.const 1 + i64.eq + br_if 0 (;@3;) + i32.const 0 + local.set 1 + br 1 (;@2;) + end + i64.const 253576579652878 + i64.const 2 + call $_ZN17soroban_env_guest5guest6ledger17get_contract_data17h4f075bb2afc11861E + local.tee 2 + i64.const 255 + i64.and + i64.const 4 + i64.ne + br_if 1 (;@1;) + local.get 2 + i64.const 32 + i64.shr_u + i32.wrap_i64 + local.set 3 + i32.const 1 + local.set 1 + end + local.get 0 + local.get 3 + i32.store offset=4 + local.get 0 + local.get 1 + i32.store + return + end + unreachable + unreachable) + (func $_ZN11soroban_sdk7storage8Instance3set17h1e50b5daa6d5db02E (type 2) (param i32) + i64.const 253576579652878 + local.get 0 + i64.extend_i32_u + i64.const 32 + i64.shl + i64.const 4 + i64.or + i64.const 2 + call $_ZN17soroban_env_guest5guest6ledger17put_contract_data17hbcf4a2a09b350844E + drop) + (func $increment (type 3) (result i64) + (local i32 i32) + global.get $__stack_pointer + i32.const 16 + i32.sub + local.tee 0 + global.set $__stack_pointer + local.get 0 + i32.const 8 + i32.add + call $_ZN11soroban_sdk7storage8Instance3get17hbc53ccbc4676241bE + block ;; label = @1 + local.get 0 + i32.load offset=12 + i32.const 0 + local.get 0 + i32.load offset=8 + select + i32.const 1 + i32.add + local.tee 1 + br_if 0 (;@1;) + call $_ZN4core9panicking11panic_const24panic_const_add_overflow17hde776086e9d58b0fE + unreachable + end + local.get 1 + call $_ZN11soroban_sdk7storage8Instance3set17h1e50b5daa6d5db02E + local.get 0 + i32.const 16 + i32.add + global.set $__stack_pointer + local.get 1 + i64.extend_i32_u + i64.const 32 + i64.shl + i64.const 4 + i64.or) + (func $_ZN4core9panicking11panic_const24panic_const_add_overflow17hde776086e9d58b0fE (type 4) + call $_ZN4core9panicking9panic_fmt17h5c7ce52813e94bcdE + unreachable) + (func $increment_panic (type 3) (result i64) + (local i32) + global.get $__stack_pointer + i32.const 16 + i32.sub + local.tee 0 + global.set $__stack_pointer + local.get 0 + i32.const 8 + i32.add + call $_ZN11soroban_sdk7storage8Instance3get17hbc53ccbc4676241bE + block ;; label = @1 + local.get 0 + i32.load offset=12 + i32.const 0 + local.get 0 + i32.load offset=8 + select + i32.const 1 + i32.add + local.tee 0 + i32.eqz + br_if 0 (;@1;) + local.get 0 + call $_ZN11soroban_sdk7storage8Instance3set17h1e50b5daa6d5db02E + call $_ZN26soroban_increment_contract17IncrementContract15increment_panic19panic_cold_explicit17h2e1d9a10feff35b7E + unreachable + end + call $_ZN4core9panicking11panic_const24panic_const_add_overflow17hde776086e9d58b0fE + unreachable) + (func $_ZN26soroban_increment_contract17IncrementContract15increment_panic19panic_cold_explicit17h2e1d9a10feff35b7E (type 4) + call $_ZN4core9panicking14panic_explicit17h47855c360709a39dE + unreachable) + (func $_ZN4core9panicking14panic_explicit17h47855c360709a39dE (type 4) + call $_ZN4core9panicking13panic_display17hbd841ae85eb3dff4E + unreachable) + (func $_ZN4core9panicking9panic_fmt17h5c7ce52813e94bcdE (type 4) + unreachable + unreachable) + (func $_ZN4core9panicking13panic_display17hbd841ae85eb3dff4E (type 4) + call $_ZN4core9panicking9panic_fmt17h5c7ce52813e94bcdE + unreachable) + (func $_ (type 4)) + (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 "increment" (func $increment)) + (export "increment_panic" (func $increment_panic)) + (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-sc"), + b"test-wasm", + .List +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "increment", + .List, + U32(1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "increment", + .List, + U32(2) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "increment_panic", + .List, + Error(ErrContext, InvalidAction) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "increment", + .List, + U32(3) +) + +setExitCode(0) \ No newline at end of file