Merge pull request #20 from FuzzingLabs/dev/antonin

Improve unit tests generation & symbolic execution documentation

README.md

@@ -7,9 +7,11 @@ Sierra-Analyzer is a security toolkit for analyzing Sierra files.
 3) [Analyze a remote contract](#analyze-a-remote-contract)
 4) [Print the contract's Control-Flow Graph](#print-the-contracts-control-flow-graph)
 5) [Print the contract's Callgraph](#print-the-contracts-callgraph)
-6) [Run the detectors](#print-the-contracts-callgraph)
-7) [Use it as a library](#print-the-contracts-callgraph)
+6) [Run the detectors](#run-the-detectors)
+7) [Use the symbolic execution to generate unit tests](#use-the-symbolic-execution-to-generate-unit-tests)
 8) [Improve the decompiler output using LLMs](#print-the-contracts-callgraph)
+9) [Use it as a library](#print-the-contracts-callgraph)
+
 
 #### Project structure 
 
@@ -96,16 +98,46 @@ cargo run -- -f ./examples/sierra/fib_array.sierra  -d
 	<img src="/doc/images/detectors-output.png" height="130px"/>
 </p>
 
-#### Use it as a library 
+#### Use the symbolic execution to generate unit tests
 
-It is also possible to use the `sierra-analyzer-lib` library to decompile serialised or unserialised Sierra files.
+##### 1) Using the Tests generator detector
+
+Symbolic execution can be used to generate unit tests for the functions that take `felt252` arguments as input. 
+
+For example the file [symbolic_execution_test.sierra](https://github.com/FuzzingLabs/sierra-analyzer/blob/master/examples/sierra/symbolic_execution_test.sierra) contains a main function that takes four `felt252` arguments *v0*, *v1*, *v2* and *v3*. The function includes four conditions that check if `v0 == 102`, `v1 == 117`, `v2 == 122` and `v3 == 122` which correspond to the ASCII values for the letters *f*, *u*, *z*, and *z*, respectively.
+
+When running the detectors we can generate test cases for each path in the function with the **Tests generator detector**:
+
+
+```
+cargo run -- -f ./examples/sierra/fib_array.sierra  -d
+
+[...]
+
+[Informational] Tests generator
+        - symbolic::symbolic::symbolic_execution_test : 
+        - v0: 102, v1: 0, v2: 0, v3: 0
+        - v0: 103, v1: 0, v2: 0, v3: 0
+        - v0: 102, v1: 117, v2: 0, v3: 0
+        - v0: 0, v1: 118, v2: 0, v3: 0
+        - v0: 102, v1: 117, v2: 122, v3: 0
+        - v0: 0, v1: 0, v2: 123, v3: 0
+        - v0: 102, v1: 117, v2: 122, v3: 122
+        - v0: 0, v1: 0, v2: 0, v3: 123
+```
+
+##### 2) Using the library
 
-Examples can be found [here](/lib/examples/).
+The tests generator can also be used [with the library](https://github.com/FuzzingLabs/sierra-analyzer/blob/master/lib/examples/tests_generator.rs).
 
 #### Improve the decompiler output using LLMs
 
 [Here](/doc/llm-decompilation.md) is a tutorial on how to improve the decompiler output using LLMs.
 
+#### Use it as a library 
+
+It is also possible to use the `sierra-analyzer-lib` library to decompile serialised or unserialised Sierra files.
+
 #### Features
 
 - [x] Decompiler

lib/src/detectors/mod.rs

@@ -2,11 +2,13 @@ pub mod detector;
 pub mod functions_detector;
 pub mod statistics_detector;
 pub mod strings_detector;
+pub mod tests_generator_detector;
 
 use crate::detectors::detector::Detector;
 use crate::detectors::functions_detector::FunctionsDetector;
 use crate::detectors::statistics_detector::StatisticsDetector;
 use crate::detectors::strings_detector::StringsDetector;
+use crate::detectors::tests_generator_detector::TestsGeneratorDetector;
 
 /// Macro to create a vector of detectors
 macro_rules! create_detectors {
@@ -21,5 +23,10 @@ macro_rules! create_detectors {
 
 /// Returns a vector of all the instantiated detectors
 pub fn get_detectors() -> Vec<Box<dyn Detector>> {
-    create_detectors!(FunctionsDetector, StringsDetector, StatisticsDetector)
+    create_detectors!(
+        FunctionsDetector,
+        StringsDetector,
+        StatisticsDetector,
+        TestsGeneratorDetector
+    )
 }

lib/src/detectors/tests_generator_detector.rs

@@ -0,0 +1,76 @@
+use crate::decompiler::decompiler::Decompiler;
+use crate::detectors::detector::{Detector, DetectorType};
+use crate::sym_exec::sym_exec::generate_test_cases_for_function;
+
+#[derive(Debug)]
+pub struct TestsGeneratorDetector;
+
+impl TestsGeneratorDetector {
+    /// Creates a new `TestsGeneratorDetector` instance
+    pub fn new() -> Self {
+        Self
+    }
+}
+
+impl Detector for TestsGeneratorDetector {
+    /// Returns the id of the detector
+    #[inline]
+    fn id(&self) -> &'static str {
+        "tests"
+    }
+
+    /// Returns the name of the detector
+    #[inline]
+    fn name(&self) -> &'static str {
+        "Tests generator"
+    }
+
+    /// Returns the description of the detector
+    #[inline]
+    fn description(&self) -> &'static str {
+        "Returns the tests cases for the functions."
+    }
+
+    /// Returns the type of the detector
+    #[inline]
+    fn detector_type(&self) -> DetectorType {
+        DetectorType::INFORMATIONAL
+    }
+
+    /// Returns the generated unit tests for the function if they exist
+    fn detect(&mut self, decompiler: &mut Decompiler) -> String {
+        let mut result = String::new();
+
+        for function in &mut decompiler.functions {
+            // Determine the function name
+            let function_name = if let Some(prototype) = &function.prototype {
+                // Remove the "func " prefix and then split at the first parenthese
+                let stripped_prototype = &prototype[5..];
+                if let Some(first_space_index) = stripped_prototype.find('(') {
+                    Some(stripped_prototype[..first_space_index].trim().to_string())
+                } else {
+                    None
+                }
+            } else {
+                None
+            };
+
+            // If a function name was found, proceed with the mutable borrow
+            if let Some(function_name) = function_name {
+
+                // Add the test cases to the result
+                let test_cases = generate_test_cases_for_function(
+                    function,
+                    decompiler.declared_libfuncs_names.clone(),
+                );
+
+                if !test_cases.is_empty() {
+                    result += &format!("{} : \n", function_name);
+                    result += &format!("{}\n", test_cases);
+                }
+            }
+        }
+
+        result
+    }
+}

lib/src/sym_exec/sym_exec.rs

@@ -45,15 +45,18 @@ pub fn generate_test_cases_for_function(
         let cfg = Config::new();
         let context = Context::new(&cfg);
 
-        // Create a solver
-        let solver = Solver::new(&context);
-
         // Create Z3 variables for each felt252 argument
         let z3_variables: Vec<Int> = felt252_arguments
             .iter()
             .map(|(arg_name, _)| Int::new_const(&context, &**arg_name))
             .collect();
 
+        // Create a solver
+        let mut symbolic_execution = SymbolicExecution::new(&context);
+
+        let mut zero_constraints = Vec::new();
+        let mut other_constraints = Vec::new();
+
         // Convert Sierra statements to z3 constraints
         for basic_block in path {
             for statement in &basic_block.statements {
@@ -63,16 +66,30 @@ pub fn generate_test_cases_for_function(
                     &context,
                     declared_libfuncs_names.clone(),
                 ) {
-                    solver.assert(&constraint);
+                    symbolic_execution.add_constraint(&constraint);
+
+                    // Identify if it's a zero check and store the variable for non-zero testing
+                    if let GenStatement::Invocation(invocation) = &statement.statement {
+                        let libfunc_id_str = parse_element_name_with_fallback!(
+                            invocation.libfunc_id,
+                            declared_libfuncs_names
+                        );
+
+                        if IS_ZERO_REGEX.is_match(&libfunc_id_str) {
+                            let operand_name = format!("v{}", invocation.args[0].id.to_string());
+                            let operand = Int::new_const(&context, operand_name.clone());
+                            zero_constraints.push((operand, constraint));
+                        } else {
+                            // Store other constraints for reuse
+                            other_constraints.push(constraint);
+                        }
+                    }
                 }
             }
-        }
 
-        // Check if the constraints are satisfiable
-        match solver.check() {
-            SatResult::Sat => {
-                // If solvable, add the argument names and values to the result
-                if let Some(model) = solver.get_model() {
+            // Check if the constraints are satisfiable (value == 0)
+            if symbolic_execution.check() == SatResult::Sat {
+                if let Some(model) = symbolic_execution.solver.get_model() {
                     let values: Vec<String> = felt252_arguments
                         .iter()
                         .zip(z3_variables.iter())
@@ -84,16 +101,44 @@ pub fn generate_test_cases_for_function(
                             )
                         })
                         .collect();
-                    let values_str = format!("{:?}\n", values);
+                    let values_str = format!("{}", values.join(", "));
                     if unique_results.insert(values_str.clone()) {
-                        result.push_str(&values_str);
+                        result.push_str(&format!("{}\n", values_str));
                     }
                 }
             }
-            SatResult::Unsat | SatResult::Unknown => {
-                let non_solvable_str = "non solvable\n".to_string();
-                if unique_results.insert(non_solvable_str.clone()) {
-                    result.push_str(&non_solvable_str);
+
+            // Now generate test cases where the value is not equal to 0
+            for (operand, _) in &zero_constraints {
+                // Create a fresh solver for the non-zero case
+                let non_zero_solver = Solver::new(&context);
+
+                // Re-apply all other constraints except the zero-equality one
+                for constraint in &other_constraints {
+                    non_zero_solver.assert(constraint);
+                }
+
+                // Add a constraint to force the operand to be not equal to 0
+                non_zero_solver.assert(&operand._eq(&Int::from_i64(&context, 0)).not());
+
+                if non_zero_solver.check() == SatResult::Sat {
+                    if let Some(model) = non_zero_solver.get_model() {
+                        let values: Vec<String> = felt252_arguments
+                            .iter()
+                            .zip(z3_variables.iter())
+                            .map(|((arg_name, _), var)| {
+                                format!(
+                                    "{}: {}",
+                                    arg_name,
+                                    model.eval(var, true).unwrap().to_string()
+                                )
+                            })
+                            .collect();
+                        let values_str = format!("{}", values.join(", "));
+                        if unique_results.insert(values_str.clone()) {
+                            result.push_str(&format!("{}\n", values_str));
+                        }
+                    }
                 }
             }
         }