Docs
Error Detection Mode
Error Detection Mode
Use TSA to find exceptional executions.
In runtime error detection mode, TSA accepts as input a contract file in one of the following formats:
Tact source code
java -jar tsa-cli.jar tact --helpFunC source code
java -jar tsa-cli.jar func --helpFift assembler code
java -jar tsa-cli.jar fift --helpBoC (compiled code)
java -jar tsa-cli.jar boc --helpFor now, there is no separate command for analyzing Tolk source code, but you can always compile it manually and then analyze it as BoC.
By default, TSA analyzes only recv_internal and recv_external. To analyze a specific method, use --method option.
Optionally, it also accepts a TL-B scheme for the recv_internal method. For detailed input format information, use the --help argument.
The output in this mode is a SARIF report containing the following information about methods that may encounter a TVM error during execution.
Description of the errors that are found in this mode is given here.
Examples
NOTE: the original Tact and FunC compilers do not preserve source code location information (source maps) in the resulting compiled code, and the SARIF report generated by the tool will not be able to pinpoint errors directly in the source code.
The position of the instruction where the failure happens is given in format cell-hash + offset, which is used in the tasm tool.
Tact example
Consider a simple smart contract written in Tact that may encounter an arithmetic overflow error when the divide method receives a value of subtrahend close to the minimal integer value:
contract Divider {
init() {}
receive() {}
get fun subtractAndDivide(subtrahend: Int, dividend: Int, flag: Bool): Int {
let divider: Int = 42;
if (flag) {
divider -= subtrahend;
} else {
divider = 2;
}
if (dividend == 100) {
throw(100);
}
return dividend / divider;
}
}The method we want to analyze is subtractAndDivide, which has method id 127452.
To eliminate executions that fail with user-defined exceptions, we also use --no-user-errors flag.
Running TSA for this contract:
java -jar tsa-cli.jar \
tact -c "tact.config.json" -p "sample" -i "Divider" --method 127452 --no-user-errors \
> Divider.sarifproduces a SARIF report.
Raw SARIF report
{
"$schema": "https://docs.oasis-open.org/sarif/sarif/v2.1.0/errata01/os/schemas/sarif-schema-2.1.0.json",
"version": "2.1.0",
"runs": [
{
"properties": {
"coverage": {
"127452": 100.0
}
},
"results": [
{
"level": "error",
"locations": [
{
"logicalLocations": [
{
"decoratedName": "127452",
"properties": {
"position": {
"cellHashHex": "91FC6E7B5CEC4435584AD4A60E936B9971A56CCC3B302F5B8CE2CD88D4E88833",
"offset": 24
},
"inst": "LDI"
}
}
]
}
],
"message": {
"text": "TvmFailure(exit=TVM cell underflow, exit code: 9, type=FixedStructuralError, phase=COMPUTE_PHASE)"
},
"properties": {
"gasUsage": 306,
"usedParameters": {
"type": "stackInput",
"usedParameters": [
]
},
"rootContractInitialC4": {
"type": "org.usvm.test.resolver.TvmTestDataCellValue",
"knownTypes": [
{
"type": {
"type": "org.usvm.test.resolver.TvmTestCellDataIntegerRead",
"bitSize": 1,
"isSigned": true,
"endian": "BigEndian"
},
"offset": 0
}
]
},
"resultStack": [
"0"
]
},
"ruleId": "cell-underflow"
},
{
"level": "error",
"locations": [
{
"logicalLocations": [
{
"decoratedName": "127452",
"properties": {
"position": {
"cellHashHex": "15A117B18C56A6869BB2D4DC8756972F73922F336788916F7AEA4898CC2E2A25",
"offset": 40
},
"inst": "SUB"
}
}
]
}
],
"message": {
"text": "TvmFailure(exit=TVM integer overflow, exit code: 4, phase=COMPUTE_PHASE)"
},
"properties": {
"gasUsage": 687,
"usedParameters": {
"type": "stackInput",
"usedParameters": [
"-115792089237316195423570985008687907853269984665640564039457584007913129639894",
"1"
]
},
"rootContractInitialC4": {
"type": "org.usvm.test.resolver.TvmTestDataCellValue",
"data": "0",
"refs": [
{
"type": "org.usvm.test.resolver.TvmTestDataCellValue"
}
],
"knownTypes": [
{
"type": {
"type": "org.usvm.test.resolver.TvmTestCellDataIntegerRead",
"bitSize": 1,
"isSigned": true,
"endian": "BigEndian"
},
"offset": 0
}
]
},
"resultStack": [
"0"
]
},
"ruleId": "integer-overflow"
},
{
"level": "error",
"locations": [
{
"logicalLocations": [
{
"decoratedName": "127452",
"properties": {
"position": {
"cellHashHex": "15A117B18C56A6869BB2D4DC8756972F73922F336788916F7AEA4898CC2E2A25",
"offset": 136
},
"inst": "DIV"
}
}
]
}
],
"message": {
"text": "TvmFailure(exit=TVM integer overflow, exit code: 4, phase=COMPUTE_PHASE)"
},
"properties": {
"gasUsage": 796,
"usedParameters": {
"type": "stackInput",
"usedParameters": [
"42",
"101",
"1"
]
},
"rootContractInitialC4": {
"type": "org.usvm.test.resolver.TvmTestDataCellValue",
"data": "0",
"refs": [
{
"type": "org.usvm.test.resolver.TvmTestDataCellValue"
},
{
"type": "org.usvm.test.resolver.TvmTestDataCellValue"
}
],
"knownTypes": [
{
"type": {
"type": "org.usvm.test.resolver.TvmTestCellDataIntegerRead",
"bitSize": 1,
"isSigned": true,
"endian": "BigEndian"
},
"offset": 0
}
]
},
"resultStack": [
"0"
]
},
"ruleId": "integer-overflow"
},
{
"level": "error",
"locations": [
{
"logicalLocations": [
{
"decoratedName": "127452",
"properties": {
"position": {
"cellHashHex": "15A117B18C56A6869BB2D4DC8756972F73922F336788916F7AEA4898CC2E2A25",
"offset": 136
},
"inst": "DIV"
}
}
]
}
],
"message": {
"text": "TvmFailure(exit=TVM integer overflow, exit code: 4, phase=COMPUTE_PHASE)"
},
"properties": {
"gasUsage": 796,
"usedParameters": {
"type": "stackInput",
"usedParameters": [
"43",
"-115792089237316195423570985008687907853269984665640564039457584007913129639936",
"1"
]
},
"rootContractInitialC4": {
"type": "org.usvm.test.resolver.TvmTestDataCellValue",
"data": "0",
"refs": [
{
"type": "org.usvm.test.resolver.TvmTestDataCellValue"
},
{
"type": "org.usvm.test.resolver.TvmTestDataCellValue"
},
{
"type": "org.usvm.test.resolver.TvmTestDataCellValue"
},
{
"type": "org.usvm.test.resolver.TvmTestDataCellValue"
}
],
"knownTypes": [
{
"type": {
"type": "org.usvm.test.resolver.TvmTestCellDataIntegerRead",
"bitSize": 1,
"isSigned": true,
"endian": "BigEndian"
},
"offset": 0
}
]
},
"resultStack": [
"0"
]
},
"ruleId": "integer-overflow"
},
{
"level": "error",
"locations": [
{
"logicalLocations": [
{
"decoratedName": "127452",
"properties": {
"position": {
"cellHashHex": "15A117B18C56A6869BB2D4DC8756972F73922F336788916F7AEA4898CC2E2A25",
"offset": 40
},
"inst": "SUB"
}
}
]
}
],
"message": {
"text": "TvmFailure(exit=TVM integer overflow, exit code: 4, phase=COMPUTE_PHASE)"
},
"properties": {
"gasUsage": 687,
"usedParameters": {
"type": "stackInput",
"usedParameters": [
"-115792089237316195423570985008687907853269984665640564039457584007913129639894",
"1"
]
},
"rootContractInitialC4": {
"type": "org.usvm.test.resolver.TvmTestDataCellValue",
"data": "1",
"knownTypes": [
{
"type": {
"type": "org.usvm.test.resolver.TvmTestCellDataIntegerRead",
"bitSize": 1,
"isSigned": true,
"endian": "BigEndian"
},
"offset": 0
}
]
},
"resultStack": [
"0"
]
},
"ruleId": "integer-overflow"
},
{
"level": "error",
"locations": [
{
"logicalLocations": [
{
"decoratedName": "127452",
"properties": {
"position": {
"cellHashHex": "15A117B18C56A6869BB2D4DC8756972F73922F336788916F7AEA4898CC2E2A25",
"offset": 136
},
"inst": "DIV"
}
}
]
}
],
"message": {
"text": "TvmFailure(exit=TVM integer overflow, exit code: 4, phase=COMPUTE_PHASE)"
},
"properties": {
"gasUsage": 796,
"usedParameters": {
"type": "stackInput",
"usedParameters": [
"43",
"-115792089237316195423570985008687907853269984665640564039457584007913129639936",
"1"
]
},
"rootContractInitialC4": {
"type": "org.usvm.test.resolver.TvmTestDataCellValue",
"data": "1",
"knownTypes": [
{
"type": {
"type": "org.usvm.test.resolver.TvmTestCellDataIntegerRead",
"bitSize": 1,
"isSigned": true,
"endian": "BigEndian"
},
"offset": 0
}
]
},
"resultStack": [
"0"
]
},
"ruleId": "integer-overflow"
},
{
"level": "error",
"locations": [
{
"logicalLocations": [
{
"decoratedName": "127452",
"properties": {
"position": {
"cellHashHex": "15A117B18C56A6869BB2D4DC8756972F73922F336788916F7AEA4898CC2E2A25",
"offset": 136
},
"inst": "DIV"
}
}
]
}
],
"message": {
"text": "TvmFailure(exit=TVM integer overflow, exit code: 4, phase=COMPUTE_PHASE)"
},
"properties": {
"gasUsage": 796,
"usedParameters": {
"type": "stackInput",
"usedParameters": [
"42",
"0",
"1"
]
},
"rootContractInitialC4": {
"type": "org.usvm.test.resolver.TvmTestDataCellValue",
"data": "1",
"knownTypes": [
{
"type": {
"type": "org.usvm.test.resolver.TvmTestCellDataIntegerRead",
"bitSize": 1,
"isSigned": true,
"endian": "BigEndian"
},
"offset": 0
}
]
},
"resultStack": [
"0"
]
},
"ruleId": "integer-overflow"
}
],
"tool": {
"driver": {
"name": "TSA",
"organization": "Esprito"
}
}
}
]
}The first error occurs due to incorrectly initialized C4. To eliminate such errors, set concrete C4 with option --data.
The other errors show different possible integer overflows in such contract.
FunC example
Consider a simple smart contract that may encounter a cell overflow error when the write method receives a value greater than 4:
#include "stdlib.fc";
(builder) write(int loop_count) method_id {
builder b = begin_cell();
if (loop_count < 0) {
return b;
}
;; Ensure loop count is in range [-2^31;2^31] for the repeat loop
loop_count = loop_count & 0x111111;
var i = 0;
repeat(loop_count) {
builder value = begin_cell().store_int(i, 32);
b = b.store_ref(value.end_cell());
}
return b;
}
() recv_internal(int msg_value, cell in_msg, slice in_msg_body) impure {
int loop_count = in_msg_body~load_int(32);
builder value = write(loop_count);
set_data(value.end_cell());
}Running the analyzer for this contract with the following command (assuming the contract, FunC and Fift stdlibs are located in the current directory):
java -jar tsa-cli.jar \
func -i /project/example.fc --fift-std /project/fiftstdlib --method 0 \
> CellOverflow.sarifidentifies the error in the raw SARIF report:
Raw SARIF report
{
"$schema": "https://docs.oasis-open.org/sarif/sarif/v2.1.0/errata01/os/schemas/sarif-schema-2.1.0.json",
"version": "2.1.0",
"runs": [
{
"properties": {
"coverage": {
"0": 100.0
}
},
"results": [
{
"level": "error",
"locations": [
{
"logicalLocations": [
{
"decoratedName": "0",
"properties": {
"position": {
"cellHashHex": "D61895B014C3C65BD3848270B17ACC2CD2A6AE3889C8D0E8BB51D862EBF18576",
"offset": 16
},
"inst": "LDI"
}
}
]
}
],
"message": {
"text": "TvmFailure(exit=TVM cell underflow, exit code: 9, type=FixedStructuralError, phase=COMPUTE_PHASE)"
},
"properties": {
"gasUsage": 188,
"usedParameters": {
"type": "recvInternalInput",
"srcAddress": {
"cell": {
"data": "100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
}
},
"msgBody": {
"cell": {
"knownTypes": [
{
"type": {
"type": "org.usvm.test.resolver.TvmTestCellDataIntegerRead",
"bitSize": 32,
"isSigned": true,
"endian": "BigEndian"
},
"offset": 0
}
]
}
},
"msgValue": "73786976294838206464",
"bounce": false,
"bounced": false,
"ihrDisabled": false,
"ihrFee": "0",
"fwdFee": "0",
"createdLt": "0",
"createdAt": "0"
},
"rootContractInitialC4": {
"type": "org.usvm.test.resolver.TvmTestDataCellValue"
},
"resultStack": [
"0"
]
},
"ruleId": "cell-underflow"
},
{
"level": "error",
"locations": [
{
"logicalLocations": [
{
"decoratedName": "0",
"properties": {
"position": {
"cellHashHex": "FB03ED4CCA61DC70C17C9A270289101970E900837BA0F3EEABB0DD5D91CEA5D3",
"offset": 184
},
"inst": "STREF"
}
}
]
}
],
"message": {
"text": "TvmFailure(exit=TVM cell overflow, exit code: 8, phase=COMPUTE_PHASE)"
},
"properties": {
"gasUsage": 3760,
"usedParameters": {
"type": "recvInternalInput",
"srcAddress": {
"cell": {
"data": "100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
}
},
"msgBody": {
"cell": {
"data": "00000000000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
"knownTypes": [
{
"type": {
"type": "org.usvm.test.resolver.TvmTestCellDataIntegerRead",
"bitSize": 32,
"isSigned": true,
"endian": "BigEndian"
},
"offset": 0
}
]
}
},
"msgValue": "73786976294838206464",
"bounce": false,
"bounced": false,
"ihrDisabled": false,
"ihrFee": "0",
"fwdFee": "0",
"createdLt": "0",
"createdAt": "0"
},
"rootContractInitialC4": {
"type": "org.usvm.test.resolver.TvmTestDataCellValue"
},
"resultStack": [
"0"
]
},
"ruleId": "cell-overflow"
}
],
"tool": {
"driver": {
"name": "TSA",
"organization": "Esprito"
}
}
}
]
}Here we analyzed recv_internal, which has method id 0. The analyzer covered 100% instructions.
The first error occurs when the given message body is too short.
Another error is the expected cell overflow.
Since we analyzed recv_internal, the input is given not as raw stack elements, but as parsed message data, including fields like msgValue, bounced and other.