mx-wasm

Symbolic execution backend for the MultiversX blockchain network

Running

Example:

cd kmxwasm
time poetry run kmxwasm-property \
    --claim tmp2/test_change_quorum-spec-1k.json \
    --kcfg=../.property/kcfg.json

Profiling

Example:

• Run a contract normally:

  cd kmxwasm
  time poetry run kmxwasm-property \
  --claim tmp2/test_change_quorum-spec-1k.json \
  --kcfg=../.property/kcfg.json

• List all configurations:

  cd kmxwasm
  time poetry run kmxwasm-property \
  --claim tmp2/test_change_quorum-spec-1k.json \
  --kcfg=../.property/kcfg.json \
  --tree

• Look at configurations and pick one (example for configuration 48):

  cd kmxwasm
  time poetry run kmxwasm-property \
  --claim tmp2/test_change_quorum-spec-1k.json \
  --kcfg=../.property/kcfg.json \
  --show-node 48

• Run profiling using that configuration as a base; also, pick an instruction from PROFILE_INSTRUCTIONS:

  cd kmxwasm
  time poetry run kmxwasm-property \
  --claim tmp2/test_change_quorum-spec-1k.json \
  --kcfg=../.property/kcfg.json \
  --profile 48
  --profile-instruction aIConst