Installation

To start using TSA, you can either use the prebuilt artifacts (depending on your operating system) or build the artifacts yourself from the source code.

Running Prebuilt Artifacts

Linux/MacOS

Using a Docker Container

docker run --platform linux/amd64 -it --rm -v [SOURCES_DIR_ABSOLUTE_PATH]:/project ghcr.io/espritoxyz/tsa:latest [ANALYZER_OPTIONS]

Here:

• SOURCES_DIR_ABSOLUTE_PATH – the absolute path to the directory containing the source code of the project you want to analyze;
• ANALYZER_OPTIONS – analyzer options (see details, or use the --help option).

NOTE: All paths in ANALYZER_OPTIONS must be RELATIVE to SOURCES_DIR_ABSOLUTE_PATH.

For example, to analyze inter-contract interactions between two FunC contracts located in sender.fc and receiver.fc, run the following command:

docker run --platform linux/amd64 -it --rm -v [SOURCES_DIR_ABSOLUTE_PATH]:/project ghcr.io/espritoxyz/tsa:latest inter /project/[FIRST_CONTRACT_RELATIVE_PATH] /project/[SECOND_CONTRACT_RELATIVE_PATH] --func-std /project/[PATH_TO_FUNC_STDLIB] --fift-std /project/[PATH_TO_FIFT_STDLIB_DIR]

Using JAR Executables

The Releases page provides two JAR executables:

• tsa-cli.jar
• tsa-safety-properties.jar

Before using them, ensure you have the following installed:

• JRE
• Tact compiler
• FunC and Fift compilers

Then, you can run the analysis in the standard error-checking/tests generation mode:

java -jar tsa-cli.jar

or in the safety-properties checker mode:

java -jar tsa-safety-properties.jar

Windows

Currently, TSA can only be run on Windows using the JAR executables. Refer to the relevant section for details.

Building from sources

1. Install all prerequisites:
   • At least JDK 11 - any preferred build
   • Gradle
   • NodeJS
   • Tact compiler
   • FunC and Fift compilers
2. Clone this repo with all submodules (using IntelliJ Idea or git clone git clone --recurse-submodules https://github.com/espritoxyz/tsa/).

3. Build the submodule:

    cd tvm-disasm
    npm i
    npm run build
   

4. Ensure tact, func, and fift are in your $PATH
5. Run ./gradlew tsa-cli:shadowJar from the root of the project to build error-checking analysis tool (will be located in the build dir) or ./gradlew tsa-safety-properties:shadowJar to build safety-properties checker (will be located in the build dir)