#547 Decouple Solver Component into Standalone Crate

Cargo.toml

@@ -10,6 +10,7 @@ members = [
     "integration/libafl/fuzzers/pure_concolic",
     "macros",
     "orchestrator",
+    "solver",
 ]
 exclude = [
     "runtime/shim",

solver/Cargo.toml

@@ -0,0 +1,27 @@
+[package]
+name = "leafsolver"
+version = { workspace = true }
+edition = "2021"
+
+[lib]
+name = "leafsolver"
+path = "src/lib.rs"
+
+[[bin]]
+name = "leafsolver"
+path = "src/bin/main.rs"
+
+
+[features]
+default = ["serde"]
+serde = ["dep:serde", "common/serde"]
+
+[dependencies]
+serde = { workspace = true, optional = true }
+serde_json = { workspace = true }
+clap = { workspace = true }
+delegate = { workspace = true }
+z3 = { workspace = true }
+z3-sys = { workspace = true }
+derive_more = { workspace = true }
+common = { workspace = true, features = ["z3", "logging", "serde"] }

solver/README.md

@@ -0,0 +1,151 @@
+# Leaf Solver
+
+A standalone SMT solver crate built on Z3
+
+## Example Usage
+
+```rust
+use leafsolver::{
+    AstAndVars, AstNode, BVNode, Constraint, ConstraintKind, Z3Solver,
+    Config, Context, SolveResult, ast, Ast
+};
+
+// Create a Z3 context and solver
+let context = Context::new(&Config::new());
+let solver: Z3Solver<'_, i32> = Z3Solver::new(&context);
+
+// Create symbolic variables: a + b == 15, a == 10
+let a = ast::BV::new_const(&context, "a", 32);
+let b = ast::BV::new_const(&context, "b", 32);
+let ten = ast::BV::from_i64(&context, 10, 32);
+let fifteen = ast::BV::from_i64(&context, 15, 32);
+
+let sum = a.bvadd(&b);
+let eq_constraint = sum._eq(&fifteen);  // a + b == 15
+let a_eq_ten = a._eq(&ten);             // a == 10
+
+let variables = vec![
+    (1, AstNode::BitVector(BVNode::new(a, true))),
+    (2, AstNode::BitVector(BVNode::new(b, true))),
+];
+
+let constraints = vec![
+    Constraint {
+        discr: AstAndVars { value: AstNode::Bool(eq_constraint), variables: variables.clone() },
+        kind: ConstraintKind::True,
+    },
+    Constraint {
+        discr: AstAndVars { value: AstNode::Bool(a_eq_ten), variables },
+        kind: ConstraintKind::True,
+    },
+];
+
+// Solve
+let result = solver.check(constraints.into_iter());
+match result {
+    SolveResult::Sat(model) => {
+        // Solver found: a = 10, b = 5
+        println!("Solution found!");
+    }
+    SolveResult::Unsat => println!("No solution exists"),
+    SolveResult::Unknown => println!("Could not determine"),
+}
+```
+
+> See the [`tests/`](tests/) directory for more examples
+
+## CLI
+
+The solver provides a standalone binary for solving constraints from JSONL files
+
+### Installation
+
+From the root of the repository, run:
+
+```bash
+cargo install --path solver --bin leafsolver
+```
+
+### Usage
+
+```bash
+leafsolver [OPTIONS]
+```
+
+**Options:**
+- `-i, --input <FILE>` - Input JSONL file with constraints (default: `sym_decisions.jsonl`)
+- `-o, --output <FILE>` - Output JSON file with results (default: `solver_result.json`)
+- `--format <FORMAT>` - Output format for the model: `standard` or `bytes` (default: `standard`)
+
+**Output Formats:**
+- `standard`: Full SmtLibExpr format with SMT-LIB representation
+- `bytes`: Raw byte values only (u8)
+
+> The binary is currently tested using constraint files generated from the `samples/` directory. The `test_data/` folder contains constraint files produced by running Leaf on sample programs. These files are used in the test suite.
+
+Example usage with the `is_sorted` test case:
+```bash
+# Standard format (default)
+leafsolver -i test_data/is_sorted_complex.jsonl -o result.json
+
+# Bytes format for direct byte values
+leafsolver -i test_data/hello_world_simple.jsonl -o result.json --format bytes
+```
+
+### Input Format
+
+The binary expects JSONL format where each line contains a constraint entry:
+
+```json
+{
+  "step": {
+    "value": "0:4:2",
+    "index": 3
+  },
+  "constraint": {
+    "discr": {
+      "decls": {
+        "1": {
+          "name": "k!1",
+          "sort": {"BitVector": {"is_signed": false}},
+          "smtlib_rep": "(declare-fun k!1 () (_ BitVec 8))"
+        }
+      },
+      "sort": "Bool",
+      "smtlib_rep": "(bvult k!1 #x05)"
+    },
+    "kind": "False"
+  }
+}
+```
+
+### Output Format
+
+#### Standard Format (default)
+
+```json
+{
+  "result": "sat",
+  "model": {
+    "1": {
+      "decls": {},
+      "sort": {"BitVector": {"is_signed": false}},
+      "smtlib_rep": "#x08"
+    }
+  }
+}
+```
+
+#### Bytes Format
+
+```json
+{
+  "result": "sat",
+  "model": {
+    "1": 8
+  }
+}
+```
+> The bytes output format only supports 8-bit `BitVector` variables. Other sorts (Bool, Int, etc.) will cause an error.
+> 
+> Byte values must be in the range 0-255 (u8). Larger BitVectors are not supported in bytes format

solver/src/backend/mod.rs

@@ -0,0 +1,3 @@
+pub mod z3;
+
+pub use z3::Z3Solver;

solver/src/backend/z3/mod.rs

@@ -0,0 +1,58 @@
+mod node;
+#[cfg(feature = "serde")]
+pub mod serdes;
+mod solve;
+
+use std::{collections::HashMap, hash::Hash};
+
+use z3::ast::{self, Ast};
+
+use crate::{solver::SolveResult, solver::Solver};
+use common::types::trace::Constraint;
+
+pub use node::*;
+pub use solve::{WrappedSolver, set_global_params};
+
+pub trait BVExt {
+    fn as_u128(&self) -> Option<u128>;
+}
+
+impl<'ctx> BVExt for ast::BV<'ctx> {
+    fn as_u128(&self) -> Option<u128> {
+        if self.get_size() <= 128 {
+            unsafe {
+                use std::ffi::CStr;
+                Some(z3_sys::Z3_get_numeral_string(
+                    self.get_ctx().get_z3_context(),
+                    self.get_z3_ast(),
+                ))
+                .filter(|x| !x.is_null())
+                .map(|x| CStr::from_ptr(x))
+                .and_then(|s| s.to_str().ok())
+                .and_then(|s| u128::from_str_radix(s, 10).ok())
+            }
+        } else {
+            None
+        }
+    }
+}
+
+/// Z3-based solver implementation
+pub type Z3Solver<'ctx, I> = WrappedSolver<'ctx, I>;
+
+impl<'a, 'ctx: 'a, I> Solver for Z3Solver<'ctx, I>
+where
+    I: Eq + Hash + Clone,
+    Self: 'ctx,
+{
+    type Value = AstAndVars<'ctx, I>;
+    type Case = AstNode<'ctx>;
+    type Model = HashMap<I, AstNode<'ctx>>;
+
+    fn check(
+        &mut self,
+        constraints: impl Iterator<Item = Constraint<Self::Value, Self::Case>>,
+    ) -> SolveResult<Self::Model> {
+        Z3Solver::check(self, constraints)
+    }
+}