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

Fix #107 #114

Closed Rog3rSm1th closed 1 year ago

Rog3rSm1th commented 1 year ago

This PR Fixes #107.

For example this program:

%builtins output

func sum2(x: felt, y: felt) -> felt {
    return x + y;
}

func main{output_ptr: felt*}() {
    let x = 1;
    let y = 2;
    let sum = sum2(x, y); 
    return ();
}

You can determine the values of x and y needed for the sum to be 10 with this command:

thoth local tests/json_files/cairo_0/cairo_felt_sum.json --symbolic -function __main__.sum2 -constraint v4==10 -solve v0_x v1_y

v0_x: 10
v1_y: 0