From a787652f33521c5641b646bf37401a49f9376026 Mon Sep 17 00:00:00 2001 From: Rog3rSm1th Date: Wed, 7 Aug 2024 15:38:33 +0200 Subject: [PATCH 1/2] Create an example using `generate_test_cases_for_function` --- .../sierra/symbolic_execution_test.sierra | 51 +++++++++++++++++++ lib/examples/tests_generator.rs | 28 ++++++++++ lib/src/sym_exec/sym_exec.rs | 3 +- 3 files changed, 81 insertions(+), 1 deletion(-) create mode 100644 examples/sierra/symbolic_execution_test.sierra create mode 100644 lib/examples/tests_generator.rs diff --git a/examples/sierra/symbolic_execution_test.sierra b/examples/sierra/symbolic_execution_test.sierra new file mode 100644 index 0000000..75e672e --- /dev/null +++ b/examples/sierra/symbolic_execution_test.sierra @@ -0,0 +1,51 @@ +type felt252 = felt252; +type NonZero = NonZero; + +libfunc felt252_const<102> = felt252_const<102>; +libfunc felt252_sub = felt252_sub; +libfunc store_temp = store_temp; +libfunc felt252_is_zero = felt252_is_zero; +libfunc branch_align = branch_align; +libfunc jump = jump; +libfunc drop> = drop>; +libfunc felt252_const<117> = felt252_const<117>; +libfunc felt252_const<122> = felt252_const<122>; +libfunc felt252_const<0> = felt252_const<0>; + +felt252_const<102>() -> ([4]); +felt252_sub([0], [4]) -> ([5]); +store_temp([5]) -> ([5]); +felt252_is_zero([5]) { fallthrough() 6([6]) }; +branch_align() -> (); +jump() { 8() }; +branch_align() -> (); +drop>([6]) -> (); +felt252_const<117>() -> ([7]); +felt252_sub([1], [7]) -> ([8]); +store_temp([8]) -> ([8]); +felt252_is_zero([8]) { fallthrough() 14([9]) }; +branch_align() -> (); +jump() { 16() }; +branch_align() -> (); +drop>([9]) -> (); +felt252_const<122>() -> ([10]); +felt252_sub([2], [10]) -> ([11]); +store_temp([11]) -> ([11]); +felt252_is_zero([11]) { fallthrough() 22([12]) }; +branch_align() -> (); +jump() { 24() }; +branch_align() -> (); +drop>([12]) -> (); +felt252_const<122>() -> ([13]); +felt252_sub([3], [13]) -> ([14]); +store_temp([14]) -> ([14]); +felt252_is_zero([14]) { fallthrough() 30([15]) }; +branch_align() -> (); +jump() { 32() }; +branch_align() -> (); +drop>([15]) -> (); +felt252_const<0>() -> ([16]); +store_temp([16]) -> ([17]); +return([17]); + +symbolic::symbolic::symbolic_execution_test@0([0]: felt252, [1]: felt252, [2]: felt252, [3]: felt252) -> (felt252); diff --git a/lib/examples/tests_generator.rs b/lib/examples/tests_generator.rs new file mode 100644 index 0000000..e2d1053 --- /dev/null +++ b/lib/examples/tests_generator.rs @@ -0,0 +1,28 @@ +use sierra_analyzer_lib::sierra_program::SierraProgram; +use sierra_analyzer_lib::sym_exec::sym_exec::generate_test_cases_for_function; + +fn main() { + // Read file content + let content = include_str!("../../examples/sierra/symbolic_execution_test.sierra").to_string(); + + // Init a new SierraProgram with the .sierra file content + let program = SierraProgram::new(content); + + // Don't use the verbose output + let verbose_output = false; + + // Decompile the Sierra program + let mut decompiler = program.decompiler(verbose_output); + + // Decompile the sierra program + let use_color = false; + decompiler.decompile(use_color); + + // Generate test cases + let mut functions = decompiler.functions; + let test_cases = generate_test_cases_for_function( + &mut functions[0], + decompiler.declared_libfuncs_names.clone(), + ); + println!("{}", test_cases); +} diff --git a/lib/src/sym_exec/sym_exec.rs b/lib/src/sym_exec/sym_exec.rs index c1422f7..d44ff62 100644 --- a/lib/src/sym_exec/sym_exec.rs +++ b/lib/src/sym_exec/sym_exec.rs @@ -98,7 +98,8 @@ pub fn generate_test_cases_for_function( } } } - result + + result.trim_end().to_string() } /// A struct that represents a symbolic execution solver From af6084394418bfe357d492a0481d6e32ef24cf5b Mon Sep 17 00:00:00 2001 From: Rog3rSm1th Date: Thu, 8 Aug 2024 16:47:55 +0200 Subject: [PATCH 2/2] Improve `tests_generator` example --- lib/examples/tests_generator.rs | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/lib/examples/tests_generator.rs b/lib/examples/tests_generator.rs index e2d1053..e887d41 100644 --- a/lib/examples/tests_generator.rs +++ b/lib/examples/tests_generator.rs @@ -2,27 +2,37 @@ use sierra_analyzer_lib::sierra_program::SierraProgram; use sierra_analyzer_lib::sym_exec::sym_exec::generate_test_cases_for_function; fn main() { - // Read file content + // Read the content of the Sierra program file + // The file `symbolic_execution_test.sierra` contains a function `symbolic::symbolic::symbolic_execution_test` + // that takes 4 parameters (v0, v1, v2, and v3) as input. + // To pass all the conditions in the function, the values of the parameters should be: + // v0: 102, v1: 117, v2: 122, v3: 122 ("f", "u", "z", "z"). let content = include_str!("../../examples/sierra/symbolic_execution_test.sierra").to_string(); - // Init a new SierraProgram with the .sierra file content + // Initialize a new SierraProgram with the content of the .sierra file let program = SierraProgram::new(content); - // Don't use the verbose output + // Disable verbose output for the decompiler let verbose_output = false; - // Decompile the Sierra program + // Create a decompiler instance for the Sierra program let mut decompiler = program.decompiler(verbose_output); - // Decompile the sierra program + // Decompile the Sierra program let use_color = false; decompiler.decompile(use_color); - // Generate test cases + // Retrieve the decompiled functions let mut functions = decompiler.functions; + + // Generate test cases for the `symbolic::symbolic::symbolic_execution_test` function + // This should return the input values that maximize code coverage: + // ["v0: 102", "v1: 117", "v2: 122", "v3: 122"] let test_cases = generate_test_cases_for_function( &mut functions[0], decompiler.declared_libfuncs_names.clone(), ); + + // Print the generated test cases println!("{}", test_cases); }