Add symbolic execution documentation/example

examples/sierra/symbolic_execution_test.sierra

@@ -0,0 +1,51 @@
+type felt252 = felt252;
+type NonZero<felt252> = NonZero<felt252>;
+
+libfunc felt252_const<102> = felt252_const<102>;
+libfunc felt252_sub = felt252_sub;
+libfunc store_temp<felt252> = store_temp<felt252>;
+libfunc felt252_is_zero = felt252_is_zero;
+libfunc branch_align = branch_align;
+libfunc jump = jump;
+libfunc drop<NonZero<felt252>> = drop<NonZero<felt252>>;
+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<felt252>([5]) -> ([5]);
+felt252_is_zero([5]) { fallthrough() 6([6]) };
+branch_align() -> ();
+jump() { 8() };
+branch_align() -> ();
+drop<NonZero<felt252>>([6]) -> ();
+felt252_const<117>() -> ([7]);
+felt252_sub([1], [7]) -> ([8]);
+store_temp<felt252>([8]) -> ([8]);
+felt252_is_zero([8]) { fallthrough() 14([9]) };
+branch_align() -> ();
+jump() { 16() };
+branch_align() -> ();
+drop<NonZero<felt252>>([9]) -> ();
+felt252_const<122>() -> ([10]);
+felt252_sub([2], [10]) -> ([11]);
+store_temp<felt252>([11]) -> ([11]);
+felt252_is_zero([11]) { fallthrough() 22([12]) };
+branch_align() -> ();
+jump() { 24() };
+branch_align() -> ();
+drop<NonZero<felt252>>([12]) -> ();
+felt252_const<122>() -> ([13]);
+felt252_sub([3], [13]) -> ([14]);
+store_temp<felt252>([14]) -> ([14]);
+felt252_is_zero([14]) { fallthrough() 30([15]) };
+branch_align() -> ();
+jump() { 32() };
+branch_align() -> ();
+drop<NonZero<felt252>>([15]) -> ();
+felt252_const<0>() -> ([16]);
+store_temp<felt252>([16]) -> ([17]);
+return([17]);
+
+symbolic::symbolic::symbolic_execution_test@0([0]: felt252, [1]: felt252, [2]: felt252, [3]: felt252) -> (felt252);

lib/examples/tests_generator.rs

@@ -0,0 +1,38 @@
+use sierra_analyzer_lib::sierra_program::SierraProgram;
+use sierra_analyzer_lib::sym_exec::sym_exec::generate_test_cases_for_function;
+
+fn main() {
+    // 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();
+
+    // Initialize a new SierraProgram with the content of the .sierra file
+    let program = SierraProgram::new(content);
+
+    // Disable verbose output for the decompiler
+    let verbose_output = false;
+
+    // Create a decompiler instance for the Sierra program
+    let mut decompiler = program.decompiler(verbose_output);
+
+    // Decompile the Sierra program
+    let use_color = false;
+    decompiler.decompile(use_color);
+
+    // 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);
+}

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