isla-litmus-dump Working version, no register dump, need to split in …

…libraries

Cargo.toml

@@ -46,6 +46,11 @@ name = "isla-client"
 path = "src/client.rs"
 doc = false
 
+[[bin]]
+name = "isla-litmus-dump"
+path = "src/litmus-dump.rs"
+doc = false
+
 [[bin]]
 name = "isla-preprocess"
 path = "src/preprocess.rs"
@@ -75,6 +80,7 @@ doc = false
 crossbeam = "0.8.1"
 getopts = "0.2.21"
 toml = "0.5.5"
+pretty = "0.11.3"
 serde = "1.0.104"
 bincode = "1.2.1"
 sha2 = "0.8.1"

isla-axiomatic/src/footprint_analysis.rs

@@ -63,36 +63,36 @@ type RegisterField = (Name, Vec<Accessor>);
 pub struct Footprint {
     /// Tracks which (symbolic) registers / memory reads can feed into
     /// a memory write within an instruction
-    write_data_taints: (Taints, bool),
+    pub write_data_taints: (Taints, bool),
     /// Tracks with (symbolic) registers / memory reads can feed into
     /// a memory operator (read/write) address within an instruction
-    mem_addr_taints: (Taints, bool),
+    pub mem_addr_taints: (Taints, bool),
     /// Tracks which (symbolic) registers / memory reads can feed into
     /// the address of a branch
-    branch_addr_taints: (Taints, bool),
+    pub branch_addr_taints: (Taints, bool),
     /// The set of register reads (with subfield granularity)
-    register_reads: HashSet<RegisterField>,
+    pub register_reads: HashSet<RegisterField>,
     /// The set of register writes (also with subfield granularity)
-    register_writes: HashSet<RegisterField>,
+    pub register_writes: HashSet<RegisterField>,
     /// The set of register writes where the value was tainted by a memory read
-    register_writes_tainted: HashSet<RegisterField>,
+    pub register_writes_tainted: HashSet<RegisterField>,
     /// All register read-write pairs to the following registers are
     /// ignored for tracking dependencies within an instruction. If
     /// the first element of the tuple is None then all writes are
     /// ignored
-    register_writes_ignored: HashSet<(Option<Name>, Name)>,
+    pub register_writes_ignored: HashSet<(Option<Name>, Name)>,
     /// If we see `mark_register(R, "pick")` then we have internal
     /// pick dependencies from all registers affecting the intrinsic
     /// control order up till that point to R
-    register_pick_deps: HashMap<Name, HashSet<RegisterField>>,
+    pub register_pick_deps: HashMap<Name, HashSet<RegisterField>>,
     /// A store is any instruction with a WriteMem event
-    is_store: bool,
+    pub is_store: bool,
     /// A load is any instruction with a ReadMem event
-    is_load: bool,
+    pub is_load: bool,
     /// A branch is any instruction with a Branch event
-    is_branch: bool,
+    pub is_branch: bool,
     /// An exclusive is any event with an exclusive read or write kind.
-    is_exclusive: bool,
+    pub is_exclusive: bool,
 }
 
 pub struct Footprintkey {

isla-lib/src/bitvector/b129.rs

@@ -49,20 +49,22 @@ pub struct B129 {
 
 impl fmt::LowerHex for B129 {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let prefix = if f.alternate() { "0x" } else { "" };
         if self.len <= 128 || !self.tag {
-            write!(f, "{:x}", self.bits)
+            write!(f, "{}{:x}", prefix, self.bits)
         } else {
-            write!(f, "1{:0>32x}", self.bits)
+            write!(f, "{}1{:0>32x}", prefix, self.bits)
         }
     }
 }
 
 impl fmt::UpperHex for B129 {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let prefix = if f.alternate() { "0X" } else { "" };
         if self.len <= 128 || !self.tag {
-            write!(f, "{:X}", self.bits)
+            write!(f, "{}{:X}", prefix, self.bits)
         } else {
-            write!(f, "1{:0>32X}", self.bits)
+            write!(f, "{}1{:0>32X}", prefix, self.bits)
         }
     }
 }

isla-lib/src/bitvector/b64.rs

@@ -47,13 +47,13 @@ pub struct B64 {
 
 impl fmt::LowerHex for B64 {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "{:x}", self.bits)
+        fmt::LowerHex::fmt(&self.bits, f)
     }
 }
 
 impl fmt::UpperHex for B64 {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "{:x}", self.bits)
+        fmt::UpperHex::fmt(&self.bits, f)
     }
 }
 

isla-lib/src/memory.rs

@@ -148,7 +148,7 @@ impl<B> Region<B> {
         }
     }
 
-    fn region_range(&self) -> &Range<Address> {
+    pub fn region_range(&self) -> &Range<Address> {
         match self {
             Region::Constrained(r, _) => r,
             Region::Symbolic(r) => r,
@@ -241,6 +241,10 @@ impl<B: BV> Memory<B> {
         Memory { regions: Vec::new(), client_info: None }
     }
 
+    pub fn regions(&self) -> &[Region<B>] {
+        &self.regions
+    }
+
     pub fn region_name_at(&self, addr: Address) -> &'static str {
         for region in &self.regions {
             if region.region_range().contains(&addr) {

isla-lib/src/simplify.rs

@@ -979,8 +979,8 @@ fn accessor_to_string(acc: &[Accessor], symtab: &Symtab) -> String {
 pub struct EventTree<B> {
     fork_id: Option<u32>,
     source_loc: SourceLoc,
-    prefix: Vec<Event<B>>,
-    forks: Vec<EventTree<B>>,
+    pub prefix: Vec<Event<B>>,
+    pub forks: Vec<EventTree<B>>,
 }
 
 /// When used with a stable sort, will push declare-const events