FuzzingLabs / thoth

Cairo/Starknet security toolkit (bytecode analyzer, disassembler, decompiler, symbolic execution, SBMC)
https://fuzzinglabs.com/
GNU Affero General Public License v3.0
245 stars 21 forks source link

Dev/antonin #121

Closed Rog3rSm1th closed 1 year ago

Rog3rSm1th commented 1 year ago
thoth local tests/json_files/cairo_0/cairo_test_symbolic_execution.json --symbolic -function __main__.test_symbolic_execution -constraint v4\>=0 v6\<=0 -solve v0_x v1_y

v0_x: 10
v1_y: 15

For example with this config.yaml file:

function: "__main__.test_symbolic_execution"
constraints: 
    - "v13>0"
    - "v14>=0"
    - "v15<=0"
solves:
   - "v0_f"
   - "v1_u" 
   - "v2_z"
   - "v3_z2"
variables:
   - "v3_z2=26"

We can run this command:

thoth local tests/json_files/cairo_0/cairo_test_symbolic_execution_3.json --symbolic -config ./config.yaml
v0_f: 103
v1_u: 117
v2_z: 122
v3_z2: 26