Solver does not report anything...

[acmLL]

Dear,

I took a provided example and modified it a bit as follows

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

func main{output_ptr: felt*}() { tempvar x; tempvar y; if (sum2(x, y) == 10) { return (); } return (); }

By executing the command "thoth local se.json -a assignations", I got

[Optimization] Assignations

• v4 = v0_x + v1_y
• v8 = v7_return_instruction + -10
• v9 = v5_output_ptr
• v10 = v5_output_ptr

[+] 1 analyzer was run (1 detected)

Then I ran the command "thoth local se.json --symbolic -function main.test_symbolic_execution -constraint v4==0 -solve v0_x v1_y", but the solver/thoth did not report anything. What is wrong with my test?

Best regards!

[pventuzelo]

Hey, thanks for reporting. We will take a look asap ;)

[pventuzelo]

@acmLL It should be good now, can you try again? don't forget to install the new version 0.7.0 with pip install .

[acmLL]

Hey, pventuzelo. Thanks for the update. I tried the same code and got this

thoth local test.json -d
// Function 0 func main.sum2{}(x : felt, y : felt){ v4 = v0_x + v1_y ret }

// Function 1 func main.main{output_ptr : felt*}(){ sum2(v6_callers_function_frame, v7_return_instruction) v8 = v7_return_instruction - 10 if (v8 == 0) { v9 = v5_output_ptr ret

}
v10 = v5_output_ptr
ret

}

Then I run thoth local test.json -a assignations and got this

[Optimization] Assignations

• v4 = v0_x + v1_y
• v8 = v7_return_instruction + -10
• v9 = v5_output_ptr
• v10 = v5_output_ptr

Finally, I run thoth local test.json --symbolic -function main.test_symbolic_execution -constraint v8==0 v4==10 -solve v7_return_instruction v_0x v1_y

but thoth returned nothing. Did I make some mistake? Best regards!

P.S.: Is there any chance to connect v4 and v7_return_instruction as the same variable? Because in this way I just have to propose v8==0 and ask the solver to find v0_x and v1_y...

[Rog3rSm1th]

Hello !

If you run

 thoth local test.json --symbolic -function main.test_symbolic_execution -constraint v4==10 -solve v_0x v1_y

and

 thoth local test.json --symbolic -function main.test_symbolic_execution -constraint v8==0 -solve v7_return_instruction 

It should now return the result with the changes applied in #114.

[acmLL]

Hi, Rog3rSm1th. When I run thoth local test.json --symbolic -function main.test_symbolic_execution -constraint v4==10 -solve v_0x v1_y, I get nothing. But when I run thoth local test.json --symbolic -function main.sum2 -constraint v4==10 -solve v_0x v1_y, it returns correctly. However, I cannot get a similar behavior for thoth local test.json --symbolic -function main.test_symbolic_execution -constraint v8==0 -solve v7_return_instruction. With this command, it returns nothing. And with this modified one thoth local test.json --symbolic -function main.main -constraint v8==0 -solve v7_return_instruction (I do not know it this modified version makes sense but it is similar to the case sum2 except for the parameters), it returns "No solution". Regards

[pventuzelo]

it should be good with the last commit ;) thx

[acmLL]

Unfortunately, it is not pventuzelo :-(. I deleted the thoth folder right now and reinstalled it again. And my above is being repeated. I can get the values in the function sum2 if I reference it specifically in the command instead of the general -function main.test_symbolic_execution. But I get a "No solution" in the case of mainmain :-( Thanks!

[Rog3rSm1th]

I added the example you are trying to use to the tests here. Using symbolic execution I can now solve the constraints with these commands:

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

thoth local ./tests/json_files/cairo_0/cairo_test_symbolic_execution_5.json --symbolic -function __main__.main -constraint v8==0 -solve v7_return_instruction
v7_return_instruction: 10

I hope this helps!

[acmLL]

Thanks, Rog3rSm1th! For some reason...

(cairo_venv) acmLL@MacBook-Air thoth % thoth local ./tests/json_files/cairo_0/cairo_test_symbolic_execution_5.json --symbolic -function main.main -constraint v8==0 -solve v7_return_instruction No solution

Do you know what can be the problem with my installation? Best!

[Rog3rSm1th]

Did you reinstall thoth ? also can you send me the file you use ?

[acmLL]

Yes, Rog3rSm1th. I reinstalled it. test.cairo.zip