Fix and fmt

Author: toolCHAINZ

jingle/README.md

@@ -21,6 +21,56 @@ This will install `jingle` in your path. Note that
 
 `jingle` requires that a Ghidra installation be present.
 
+When you provide it as the first argument to the `jingle` CLI, it
+will save that path for future usage.
+
+Once it has been configured, you can simple run it as follows:
+
+```shell
+jingle disassemble x86:LE:32:default 89fb
+jingle lift x86:LE:32:default 89fb
+jingle model x86:LE:32:default 89fb
+```
+
+These three invocations will print disassembly, pcode translation, and
+a logical model respectively. None of these, particularly the logical model,
+are intended to be used directly from this utility; this is merely for demonstration.
+The proper way to use this tool is through the API.
+
+The above invocations will produce the following output:
+```shell
+# jingle disassemble x86:LE:32:default 89fb
+MOV EBX,EDI
+```
+
+```shell
+# jingle lift x86:LE:32:default 89fb
+EBX = COPY EDI
+```
+
+```shell
+# jingle model x86:LE:32:default 89fb
+; benchmark generated from rust API
+(set-info :status unknown)
+(declare-fun register!4 () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun register!9 () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun ram!3 () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun ram!8 () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun OTHER!1 () (Array (_ BitVec 64) (_ BitVec 8)))
+(declare-fun OTHER!6 () (Array (_ BitVec 64) (_ BitVec 8)))
+(assert
+ (let ((?x77 (store (store register!4 (_ bv12 32) (select register!4 (_ bv28 32))) (_ bv13 32) (select register!4 (_ bv29 32)))))
+ (let ((?x81 (store (store ?x77 (_ bv14 32) (select register!4 (_ bv30 32))) (_ bv15 32) (select register!4 (_ bv31 32)))))
+ (let (($x82 (= register!9 ?x81)))
+ (let (($x63 (= ram!8 ram!3)))
+ (let (($x62 (= OTHER!6 OTHER!1)))
+ (and $x62 $x63 $x82)))))))
+(check-sat)
+
+```
+
+### Usage string
+
 ```shell
 Usage: jingle [GHIDRA_PATH] <COMMAND>
 

jingle/src/main.rs

@@ -125,10 +125,10 @@ fn get_instructions(
     let img = decode(hex_bytes)?;
     let max_len = img.len();
     let mut offset = 0;
-    let sleigh = sleigh_build
-        .build(&architecture)
-        .context("Unable to build the selected architecture.\n\
-        This is either a bug in sleigh or the .sinc file for your architecture is malformed.")?;
+    let sleigh = sleigh_build.build(&architecture).context(
+        "Unable to build the selected architecture.\n\
+        This is either a bug in sleigh or the .sinc file for your architecture is malformed.",
+    )?;
     let sleigh = sleigh.initialize_with_image(img)?;
     let mut instrs = vec![];
     while offset < max_len {
@@ -192,7 +192,6 @@ fn model(config: &JingleConfig, architecture: String, hex_bytes: String) -> anyh
     let jingle_ctx = JingleContext::new(&z3, &sleigh);
     let block = ModeledBlock::read(&jingle_ctx, instrs.into_iter())?;
     let final_state = jingle_ctx.fresh_state();
-    println!("{}", block.get_final_state().fmt_smt_arrays());
     solver.assert(&final_state._eq(block.get_final_state())?.simplify());
     println!("{}", solver.to_smt2());
     Ok(())

jingle/src/modeling/slice.rs

@@ -50,4 +50,3 @@ impl<'ctx, T: ModelingContext<'ctx>> ModelingContext<'ctx> for &[T] {
         self.last().unwrap().get_branch_constraint()
     }
 }
-

jingle/src/modeling/state/mod.rs

@@ -310,8 +310,8 @@ impl<'ctx> State<'ctx> {
         let eq_terms: Vec<&Bool> = terms.iter().collect();
         Ok(Bool::and(self.jingle.z3, eq_terms.as_slice()))
     }
-    
-    pub fn fmt_smt_arrays(&self)-> String{
+
+    pub fn fmt_smt_arrays(&self) -> String {
         let mut lines = vec![];
         for x in &self.spaces {
             lines.push(x.fmt_smt_array())