Fix cargo test and rustfmt

isla-axiomatic/src/page_table.rs

@@ -1266,18 +1266,24 @@ mod tests {
         tables.get_mut(l1)[va.level_index(1)] = Desc::new_table(l2);
         tables.get_mut(l0)[va.level_index(0)] = Desc::new_table(l1);
 
-        assert_eq!(Sat, solver.check_sat());
+        assert_eq!(Sat, solver.check_sat(SourceLoc::unknown()));
 
         // Translate our concrete virtual address to a symbolic
         // physical address, and check it could be in either page
         if let Some(pa) = simple_translation_table_walk(&tables, l0, va, &mut solver) {
-            assert_eq!(Sat, solver.check_sat_with(&Eq(Box::new(Var(pa)), Box::new(bits64(0x8000_0EEF, 64)))));
-            assert_eq!(Sat, solver.check_sat_with(&Eq(Box::new(Var(pa)), Box::new(bits64(0x8000_1EEF, 64)))));
+            assert_eq!(
+                Sat,
+                solver.check_sat_with(&Eq(Box::new(Var(pa)), Box::new(bits64(0x8000_0EEF, 64))), SourceLoc::unknown())
+            );
+            assert_eq!(
+                Sat,
+                solver.check_sat_with(&Eq(Box::new(Var(pa)), Box::new(bits64(0x8000_1EEF, 64))), SourceLoc::unknown())
+            );
 
             // Additionally, it  can't be anything other than those two addresses
             solver.add(Assert(Neq(Box::new(Var(pa)), Box::new(bits64(0x8000_0EEF, 64)))));
             solver.add(Assert(Neq(Box::new(Var(pa)), Box::new(bits64(0x8000_1EEF, 64)))));
-            assert_eq!(Unsat, solver.check_sat());
+            assert_eq!(Unsat, solver.check_sat(SourceLoc::unknown()));
         } else {
             panic!("simple_translation_table_walk failed")
         }

isla-lib/src/executor.rs

@@ -1226,10 +1226,13 @@ fn run_loop<'ir, 'task, B: BV>(
                                         primop::eq_anything(req.clone(), arg.clone(), solver, *info)
                                             .map(|v| match v {
                                                 Val::Symbolic(var) => {
-                                                    solver.check_sat_with(&smtlib::Exp::Eq(
-                                                        Box::new(smtlib::Exp::Var(var)),
-                                                        Box::new(smtlib::Exp::Bool(false)),
-                                                    ), *info) == SmtResult::Unsat
+                                                    solver.check_sat_with(
+                                                        &smtlib::Exp::Eq(
+                                                            Box::new(smtlib::Exp::Var(var)),
+                                                            Box::new(smtlib::Exp::Bool(false)),
+                                                        ),
+                                                        *info,
+                                                    ) == SmtResult::Unsat
                                                 }
                                                 Val::Bool(b) => b,
                                                 _ => panic!("TODO"),

isla-lib/src/ir.rs

@@ -284,7 +284,7 @@ impl<B: BV> Val<B> {
             SymbolicCtor(discriminant, vals) => {
                 vars.insert(*discriminant);
                 vals.iter().for_each(|(_, val)| val.collect_symbolic_variables(vars))
-            },
+            }
         }
     }
 

isla-lib/src/primop.rs

@@ -2750,7 +2750,7 @@ mod tests {
             SourceLoc::unknown(),
         );
 
-        assert!(solver.check_sat() == SmtResult::Sat);
+        assert!(solver.check_sat(SourceLoc::unknown()) == SmtResult::Sat);
         Ok(())
     }
 }

isla-lib/src/smt.rs

@@ -42,12 +42,16 @@ use libc::{c_int, c_uint};
 use serde::{Deserialize, Serialize};
 
 #[cfg(feature = "smtperf")]
-use petgraph::{Directed, graph::{Graph, NodeIndex}, visit::Dfs};
+use petgraph::{
+    graph::{Graph, NodeIndex},
+    visit::Dfs,
+    Directed,
+};
 
 use z3_sys::*;
 
 #[cfg(feature = "smtperf")]
-use std::time::{Instant, Duration};
+use std::time::{Duration, Instant};
 
 use std::collections::{HashMap, HashSet};
 use std::convert::TryInto;
@@ -304,7 +308,6 @@ impl<B: BV> Event<B> {
                 if let Some(tag_value) = tag_value {
                     tag_value.collect_symbolic_variables(vars)
                 }
-
             }
             _ => (),
         }
@@ -772,9 +775,12 @@ impl<'ctx> Ast<'ctx> {
     fn simplify(&mut self) {
         unsafe {
             let z3_params = Z3_mk_params(self.ctx.z3_ctx);
-            let push_ite_bv = Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(PUSH_ITE_BV).as_ptr());
-            let bv_le_extra = Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(BV_LE_EXTRA).as_ptr());
-            let bv_sort_ac = Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(BV_SORT_AC).as_ptr());
+            let push_ite_bv =
+                Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(PUSH_ITE_BV).as_ptr());
+            let bv_le_extra =
+                Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(BV_LE_EXTRA).as_ptr());
+            let bv_sort_ac =
+                Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(BV_SORT_AC).as_ptr());
             Z3_params_inc_ref(self.ctx.z3_ctx, z3_params);
             Z3_params_set_bool(self.ctx.z3_ctx, z3_params, push_ite_bv, true);
             Z3_params_set_bool(self.ctx.z3_ctx, z3_params, bv_le_extra, true);
@@ -1261,7 +1267,6 @@ impl<'ctx> Drop for Ast<'ctx> {
 #[cfg(not(feature = "smtperf"))]
 struct PerformanceInfo {}
 
-
 #[cfg(feature = "smtperf")]
 struct PerformanceInfo {
     vars: Graph<(Sym, SourceLoc), (), Directed>,
@@ -1344,8 +1349,8 @@ impl PerformanceInfo {
 
         // Remove the edges and dummy root we added
         for edge in edges {
-             self.vars.remove_edge(edge);
-         }
+            self.vars.remove_edge(edge);
+        }
         self.vars.remove_node(root);
     }
 
@@ -1368,10 +1373,16 @@ impl PerformanceInfo {
 
         for (n, (info, duration)) in times.iter().enumerate() {
             if n >= 10 {
-                break
+                break;
             }
 
-            msg += &info.message(dir.as_ref(), files, &format!("#{} time: {}ms", n + 1, duration.as_millis()), false, true);
+            msg += &info.message(
+                dir.as_ref(),
+                files,
+                &format!("#{} time: {}ms", n + 1, duration.as_millis()),
+                false,
+                true,
+            );
             msg += "\n"
         }
 
@@ -1386,6 +1397,7 @@ impl PerformanceInfo {
 /// For example:
 /// ```
 /// # use isla_lib::bitvector::b64::B64;
+/// # use isla_lib::source_loc::SourceLoc;
 /// # use isla_lib::smt::smtlib::Exp::*;
 /// # use isla_lib::smt::smtlib::Def::*;
 /// # use isla_lib::smt::smtlib::*;
@@ -1399,7 +1411,7 @@ impl PerformanceInfo {
 /// // (assert v0)
 /// solver.add(Assert(Var(x)));
 /// // (check-sat)
-/// assert!(solver.check_sat() == SmtResult::Sat)
+/// assert!(solver.check_sat(SourceLoc::unknown()) == SmtResult::Sat)
 /// ```
 ///
 /// The other thing the Solver type does is maintain a trace of
@@ -1410,6 +1422,7 @@ impl PerformanceInfo {
 /// For example:
 /// ```
 /// # use isla_lib::bitvector::b64::B64;
+/// # use isla_lib::source_loc::SourceLoc;
 /// # use isla_lib::smt::smtlib::Exp::*;
 /// # use isla_lib::smt::smtlib::Def::*;
 /// # use isla_lib::smt::smtlib::*;
@@ -1427,7 +1440,7 @@ impl PerformanceInfo {
 /// let cfg = Config::new();
 /// let ctx = Context::new(cfg);
 /// let mut solver = Solver::from_checkpoint(&ctx, point);
-/// assert!(solver.check_sat() == SmtResult::Unsat);
+/// assert!(solver.check_sat(SourceLoc::unknown()) == SmtResult::Unsat);
 pub struct Solver<'ctx, B> {
     trace: Trace<B>,
     next_var: u32,
@@ -1456,6 +1469,7 @@ impl<'ctx, B> Drop for Solver<'ctx, B> {
 ///
 /// ```
 /// # use isla_lib::bitvector::b64::B64;
+/// # use isla_lib::source_loc::SourceLoc;
 /// # use isla_lib::smt::smtlib::Exp::*;
 /// # use isla_lib::smt::smtlib::Def::*;
 /// # use isla_lib::smt::smtlib::*;
@@ -1467,7 +1481,7 @@ impl<'ctx, B> Drop for Solver<'ctx, B> {
 /// let mut solver = Solver::<B64>::new(&ctx);
 /// solver.add(DeclareConst(x, Ty::BitVec(4)));
 /// solver.add(Assert(Bvsgt(Box::new(Var(x)), Box::new(Bits(vec![false,false,true,false])))));
-/// assert!(solver.check_sat() == SmtResult::Sat);
+/// assert!(solver.check_sat(SourceLoc::unknown()) == SmtResult::Sat);
 /// let mut model = Model::new(&solver);
 /// let var0 = model.get_var(x).unwrap().unwrap();
 /// ```
@@ -1878,7 +1892,7 @@ impl<'ctx, B: BV> Solver<'ctx, B> {
                     for used in exp.variables().iter() {
                         self.performance_info.add_var_edge(v, used);
                         self.performance_info.add_var_edge(used, v)
-                    };
+                    }
                 }
                 let mut ast = self.translate_exp(exp);
                 ast.simplify();
@@ -2267,7 +2281,7 @@ mod tests {
         solver.add(Assert(Eq(Box::new(var(2)), Box::new(v2))));
         solver.add(Assert(Eq(Box::new(var(3)), Box::new(v3))));
         solver.add(Assert(Eq(Box::new(var(4)), Box::new(v4))));
-        match solver.check_sat() {
+        match solver.check_sat(SourceLoc::unknown()) {
             Sat => (),
             _ => panic!("Round-trip failed, trace {:?}", solver.trace()),
         }
@@ -2284,15 +2298,15 @@ mod tests {
         let v1 = solver.declare_const(Ty::Enum(e), SourceLoc::unknown());
         let v2 = solver.declare_const(Ty::Enum(e), SourceLoc::unknown());
         solver.assert_eq(Var(v0), Var(v1));
-        assert!(solver.check_sat() == Sat);
+        assert!(solver.check_sat(SourceLoc::unknown()) == Sat);
         let (m0, m1) = {
             let mut model = Model::new(&solver);
             assert!(model.get_var(v2).unwrap().is_none());
             (model.get_var(v0).unwrap().unwrap(), model.get_var(v1).unwrap().unwrap())
         };
         solver.assert_eq(Var(v0), m0);
         solver.assert_eq(Var(v1), m1);
-        match solver.check_sat() {
+        match solver.check_sat(SourceLoc::unknown()) {
             Sat => (),
             _ => panic!("Round-trip failed, trace {:?}", solver.trace()),
         }
@@ -2311,7 +2325,7 @@ mod tests {
             .add(Assert(Eq(Box::new(App(Sym::from_u32(0), vec![bv!("10"), bv!("0110")])), Box::new(bv!("01011011")))));
         solver.add(Assert(Eq(Box::new(App(Sym::from_u32(0), vec![var(2), bv!("0110")])), Box::new(var(1)))));
         solver.add(Assert(Eq(Box::new(var(2)), Box::new(bv!("10")))));
-        assert!(solver.check_sat() == Sat);
+        assert!(solver.check_sat(SourceLoc::unknown()) == Sat);
         let mut model = Model::new(&solver);
         let val = model.get_var(Sym::from_u32(1)).unwrap().unwrap();
         assert!(match val {
@@ -2334,6 +2348,6 @@ mod tests {
             )),
             Box::new(bv!("0101")),
         )));
-        assert!(solver.check_sat() == Unsat);
+        assert!(solver.check_sat(SourceLoc::unknown()) == Unsat);
     }
 }

isla-lib/src/smt/smtlib.rs

@@ -1143,6 +1143,7 @@ mod tests {
     use super::Exp::*;
     use super::*;
     use crate::smt::{Config, Context, Solver, Unsat};
+    use crate::source_loc::SourceLoc;
 
     #[test]
     fn bits_to_i128_test() {
@@ -1159,7 +1160,7 @@ mod tests {
         let post_eval = exp.clone().eval();
         assert_ne!(exp, post_eval);
         solver.add(Assert(Neq(Box::new(exp.clone()), Box::new(post_eval.clone()))));
-        assert_eq!(solver.check_sat(), Unsat, "Mismatch {:?} and {:?}", exp, post_eval);
+        assert_eq!(solver.check_sat(SourceLoc::unknown()), Unsat, "Mismatch {:?} and {:?}", exp, post_eval);
     }
 
     fn exp_eval_unchanged(exp: Exp<Sym>) {

isla-lib/src/source_loc.rs

@@ -264,8 +264,11 @@ impl SourceLoc {
         let blue = if use_colors { BLUE } else { "" };
         let no_color = if use_colors { NO_COLOR } else { "" };
 
-        let (short_error, error_sep) =
-            if is_error { (format!("{}error{}: {}", red, no_color, message), "\n") } else { (message.to_string(), "\n") };
+        let (short_error, error_sep) = if is_error {
+            (format!("{}error{}: {}", red, no_color, message), "\n")
+        } else {
+            (message.to_string(), "\n")
+        };
 
         let file = TryInto::<usize>::try_into(self.file).ok().and_then(|i| files.get(i));
         if file.is_none() {

src/axiomatic.rs

@@ -75,8 +75,7 @@ fn main() {
     process::exit(code)
 }
 
-type FinalState =
-    HashMap<LitmusLoc<String>, Val<B129>>;
+type FinalState = HashMap<LitmusLoc<String>, Val<B129>>;
 
 #[derive(Debug)]
 enum AxResult {