Refactor run_litmus

Pass candidate execution as a struct to reduce number of arguments to callback

isla-axiomatic/src/axiomatic.rs

@@ -1092,7 +1092,8 @@ pub fn final_state_from_z3_output<'exec, 'ev, 'litmus, 'model, B: BV>(
     let model_buf: &str = &z3_output[3..];
     let mut event_names: Vec<&'ev str> = exec.smt_events.iter().map(|ev| ev.name.as_ref()).collect();
     event_names.push("IW");
-    let mut model = Model::<B>::parse(&event_names, model_buf).map_err(|mpe| FinalLocValuesError::ReadModelError(format!("{}", mpe)))?;
+    let mut model = Model::<B>::parse(&event_names, model_buf)
+        .map_err(|mpe| FinalLocValuesError::ReadModelError(format!("{}", mpe)))?;
 
     let mut calc = |loc: &'litmus LitmusLoc<String>| match loc {
         LitmusLoc::Register { reg, thread_id } => exec

isla-axiomatic/src/footprint_analysis.rs

@@ -334,7 +334,7 @@ pub fn data_dep<B: BV>(from: usize, to: usize, instrs: &[Option<B>], footprints:
     if to_footprint.is_system_register_write {
         for reg in &to_footprint.register_reads {
             if touched.contains(reg) {
-                return true
+                return true;
             }
         }
     }
@@ -672,8 +672,11 @@ where
                             evrefs.collect_taints(*v, events, &mut footprint.branch_addr_taints)
                         }
                     }
-                    Event::Abstract { name, .. } if arch.shared_state.symtab.to_str(*name) == "zsail_system_register_write" =>
-                        footprint.is_system_register_write = true,
+                    Event::Abstract { name, .. }
+                        if arch.shared_state.symtab.to_str(*name) == "zsail_system_register_write" =>
+                    {
+                        footprint.is_system_register_write = true
+                    }
                     _ => (),
                 }
             }