Runtime errors detection mode
As a static analyzer, TSA can operate in two modes:
- Runtime error detection for local smart contracts with report generation in SARIF format;
- Test generation for Blueprint projects.
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 --help
Usage: ton-analysis tact [<options>]
Options for analyzing Tact sources of smart contracts
Contract properties:
-d, --data=<text> The serialized contract persistent data
Options:
-c, --config=<path> The path to the Tact config (tact.config.json)
-p, --project=<text> Name of the Tact project to analyze
-i, --input=<text> Name of the Tact smart contract to analyze
-h, --help Show this message and exitFunC source code
$ java -jar tsa-cli.jar func --help
Usage: ton-analysis func [<options>]
Options for analyzing FunC sources of smart contracts
Contract properties:
-d, --data=<text> The serialized contract persistent data
Fift options:
--fift-std=<path> The path to the Fift standard library (dir containing Asm.fif, Fift.fif)
FunC options:
--func-std=<path> The path to the FunC standard library file (stdlib.fc)
TlB scheme options:
-t, --tlb=<path> The path to the parsed TL-B scheme.
Options:
-i, --input=<path> The path to the FunC source of the smart contract
-h, --help Show this message and exitFift assembler code
$ java -jar tsa-cli.jar fift --help
Usage: ton-analysis fift [<options>]
Options for analyzing smart contracts in Fift assembler
Contract properties:
-d, --data=<text> The serialized contract persistent data
Fift options:
--fift-std=<path> The path to the Fift standard library (dir containing Asm.fif, Fift.fif)
Options:
-i, --input=<path> The path to the Fift assembly of the smart contract
-h, --help Show this message and exitBoC (compiled code)
$ java -jar tsa-cli.jar boc --help
Usage: ton-analysis boc [<options>]
Options for analyzing a smart contract in the BoC format
Contract properties:
-d, --data=<text> The serialized contract persistent data
Options:
-i, --input=<path> The path to the smart contract in the BoC format
-h, --help Show this message and exitOptionally, 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:
coveragefield in the report - instruction coverage percentage by the analyzer for the methoddecoratedNameandstmt- the method id and instruction number where the error may occur, correspondinglytextin amessage- error code and its typecallFlows- call stack at the moment of the error occurrence in the form (method id - instruction)usedParameters- possible (but not necessarily unique) parameters set causing the errorgasUsage- approximate gas usage of the execution when the error occurred
For more information about error types, see the Detectors page.
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 following examples will cover both cases: with source maps and with raw SARIF.
Example with patched compilers via source maps
Source-maps disclaimer
We use patched versions of the Tact compiler, FunC compiler, and the TSA analyzer,
to achieve full error mapping in the source code, as demonstrated in this pull request via GitHub Actions
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:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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;
}
}
Running the patched analyzer for this contract with patched Tact compiler with the following command (according to the PR):
java -jar tsa-cli.jar \
tact -c "tact.config.json" -p "sample" -i "Divider" \
> Divider.sarifproduces a SARIF report that could be rendered in GitHub highlighting a possible error:
Example with a raw SARIF
Consider a simple smart contract that may encounter a cell overflow error when the write method receives a value greater than 4:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
#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 {
;; Do nothing
}
Running the analyzer for this contract with the following command (assuming the contract, FunC and Fift stdlibs are located in the current directory):
docker run --platform linux/amd64 -it --rm -v $PWD:/project ghcr.io/espritoxyz/tsa:latest func -i /project/example.fc \
--func-std /project/stdlib.fc \
--fift-std /project/fiftstdlib(please note that FunC stdlib is pointed using the specific option func-std, not as a part of the input file) identifies the error in the raw SARIF report:
Raw SARIF report
{
"$schema": "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json",
"version": "2.1.0",
"runs": [
{
"properties": {
"coverage": {
"0": 100.0,
"75819": 100.0
}
},
"results": [
{
"codeFlows": [
{
"threadFlows": [
{
"locations": [
{
"location": {
"logicalLocations": [
{
"fullyQualifiedName": "Lambda",
"properties": {
"stmt": "STREF#5"
}
}
]
}
}
]
},
{
"locations": [
{
"location": {
"logicalLocations": [
{
"fullyQualifiedName": "Lambda",
"properties": {
"stmt": "artificial_jmp_to_TvmOrdContinuation(stmt=TvmStackBasicPushInst(location=Lambda:#0, i=0), savelist=TvmRegisterSavelist(c0=null, c1=null, c2=null, c3=null, c4=null, c5=null, c7=null))#1"
}
}
]
}
}
]
},
{
"locations": [
{
"location": {
"logicalLocations": [
{
"fullyQualifiedName": "Lambda",
"properties": {
"stmt": "implicit RET#7"
}
}
]
}
}
]
},
{
"locations": [
{
"location": {
"logicalLocations": [
{
"fullyQualifiedName": "Lambda",
"properties": {
"stmt": "artificial_jmp_to_TvmOrdContinuation(stmt=TvmStackBasicPushInst(location=Lambda:#0, i=0), savelist=TvmRegisterSavelist(c0=null, c1=null, c2=null, c3=null, c4=null, c5=null, c7=null))#1"
}
}
]
}
}
]
},
{
"locations": [
{
"location": {
"logicalLocations": [
{
"fullyQualifiedName": "Lambda",
"properties": {
"stmt": "implicit RET#7"
}
}
]
}
}
]
},
{
"locations": [
{
"location": {
"logicalLocations": [
{
"fullyQualifiedName": "Lambda",
"properties": {
"stmt": "artificial_jmp_to_TvmOrdContinuation(stmt=TvmStackBasicPushInst(location=Lambda:#0, i=0), savelist=TvmRegisterSavelist(c0=null, c1=null, c2=null, c3=null, c4=null, c5=null, c7=null))#1"
}
}
]
}
}
]
},
{
"locations": [
{
"location": {
"logicalLocations": [
{
"fullyQualifiedName": "Lambda",
"properties": {
"stmt": "implicit RET#7"
}
}
]
}
}
]
},
{
"locations": [
{
"location": {
"logicalLocations": [
{
"fullyQualifiedName": "Lambda",
"properties": {
"stmt": "artificial_jmp_to_TvmOrdContinuation(stmt=TvmStackBasicPushInst(location=Lambda:#0, i=0), savelist=TvmRegisterSavelist(c0=null, c1=null, c2=null, c3=null, c4=null, c5=null, c7=null))#1"
}
}
]
}
}
]
},
{
"locations": [
{
"location": {
"logicalLocations": [
{
"fullyQualifiedName": "Lambda",
"properties": {
"stmt": "implicit RET#7"
}
}
]
}
}
]
},
{
"locations": [
{
"location": {
"logicalLocations": [
{
"fullyQualifiedName": "Lambda",
"properties": {
"stmt": "artificial_jmp_to_TvmOrdContinuation(stmt=TvmStackBasicPushInst(location=Lambda:#0, i=0), savelist=TvmRegisterSavelist(c0=null, c1=null, c2=null, c3=null, c4=null, c5=null, c7=null))#1"
}
}
]
}
}
]
},
{
"locations": [
{
"location": {
"logicalLocations": [
{
"decoratedName": "75819",
"properties": {
"stmt": "REPEAT#11"
}
}
]
}
}
]
}
]
}
],
"level": "error",
"locations": [
{
"logicalLocations": [
{
"decoratedName": "75819"
}
]
}
],
"message": {
"text": "TvmFailure(exit=TVM cell overflow, exit code: 8, type=UnknownError)"
},
"properties": {
"gasUsage": 3451,
"usedParameters": [
"2097151"
],
"resultStack": [
"0"
]
},
"ruleId": "cell-overflow"
}
],
"tool": {
"driver": {
"name": "TSA",
"organization": "Explyt"
}
}
}
]
}Here the analyzed method has the id 75819,
the analyzer covered 100% instructions of this method,
and the cell overflow error with exit code 8 occurred in the stmt with the index 11 in the REPEAT loop inside this method,
2097151 value passed to this method causes this error,
and gas usage equals to 3451.
For more examples containing erroneous places, take a look at the directory in the repository with manually written contracts.