Movable

A symbolic execution tool for Move, which is a smart contract language designed for Diem.

Diem Setup

Clone Diem to the parent directory of Movable. The directory structure should look like:

|_ diem
|_ Movable

Diem repository should be checkout to tag diem-framework-v1.2.0. Other versions are untested.

Usage

cargo run <BYTECODE_FILE> -f <FUNCTION_NAME>

Roadmap

Engine

Transaction configuration
Symbolic execution configuration

Symbolic Chain State

Start from states other than genesis
Symbolic writeset
Custom data store

Symbolic VM

Vector bound check (in plugin or not?)
Native function modelling
Stdlib test
More benchmarks
Docking with plugin system (intarith plugin running)
Gas infrastructure
Debug and log infrastructure

Plugin System

Single instruction listening support (intarith plugin added)
Verification plugin support