diff --git a/isla-axiomatic/src/run_litmus.rs b/isla-axiomatic/src/run_litmus.rs index 42eff1e..2da6246 100644 --- a/isla-axiomatic/src/run_litmus.rs +++ b/isla-axiomatic/src/run_litmus.rs @@ -601,7 +601,9 @@ where .type_info .enums .get(&name) - .ok_or_else(|| CallbackError::Internal("Failed to get enumeration".to_string()))?; + .ok_or_else(|| CallbackError::Internal( + format!("Failed to get enumeration '{}'", name) + ))?; let name = zencode::decode(arch.shared_state.symtab.to_str(name)); write!(&mut fd, "(declare-datatypes ((|{}| 0)) ((", name).map_err(internal_err)?; for member in members.iter() { diff --git a/isla-lib/src/ir.rs b/isla-lib/src/ir.rs index fceb215..851d323 100644 --- a/isla-lib/src/ir.rs +++ b/isla-lib/src/ir.rs @@ -46,7 +46,7 @@ use serde::{Deserialize, Serialize}; use std::collections::{BTreeMap, HashMap, HashSet}; use std::fmt; use std::hash::Hash; -use std::io::Write; +use std::io::{Write, Error, ErrorKind}; use std::sync::Arc; use crate::bitvector::{b64::B64, BV}; @@ -82,6 +82,12 @@ impl Name { } } +impl fmt::Display for Name { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + write!(f, "{}", self.id) + } +} + pub type RegisterField = (Name, Vec); #[derive(Copy, Clone, Debug, Serialize, Deserialize)] @@ -326,7 +332,9 @@ impl Val { } String(s) => write!(buf, "\"{}\"", s), Enum(EnumMember { enum_id, member }) => { - let members = shared_state.type_info.enums.get(&enum_id.to_name()).expect("Failed to get enumeration"); + let members = shared_state.type_info.enums.get(&enum_id.to_name()).ok_or_else(|| + Error::new(ErrorKind::Other, format!("Failed to get enumeration '{}'", enum_id.to_name())) + )?; let name = zencode::decode(symtab.to_str(members[*member])); write!(buf, "|{}|", name) } diff --git a/isla-lib/src/simplify.rs b/isla-lib/src/simplify.rs index b4624b5..23d6592 100644 --- a/isla-lib/src/simplify.rs +++ b/isla-lib/src/simplify.rs @@ -34,7 +34,7 @@ use std::borrow::{Borrow, BorrowMut, Cow}; use std::cmp::Ordering; use std::collections::{HashMap, HashSet}; -use std::io::Write; +use std::io::{Write, Error, ErrorKind}; use crate::bitvector::{write_bits64, BV}; use crate::ir::{BitsSegment, Loc, Name, SharedState, Symtab, Val, HAVE_EXCEPTION}; @@ -1384,7 +1384,9 @@ fn write_exp( Bits(bv) => write_bits(buf, bv), Bits64(bv) => write_bits64(buf, bv.lower_u64(), bv.len()), Enum(e) => { - let members = shared_state.type_info.enums.get(&e.enum_id.to_name()).expect("Failed to get enumeration"); + let members = shared_state.type_info.enums.get(&e.enum_id.to_name()).ok_or_else(|| + Error::new(ErrorKind::Other, format!("Failed to get enumeration '{}'", e.enum_id.to_name())) + )?; let name = zencode::decode(shared_state.symtab.to_str(members[e.member])); write!(buf, "|{}|", name) } @@ -1736,7 +1738,9 @@ pub fn write_events_in_context( } Def::DefineEnum(name, size) => { if !opts.just_smt { - let members = shared_state.type_info.enums.get(name).expect("Failed to get enumeration"); + let members = shared_state.type_info.enums.get(name).ok_or_else(|| + Error::new(ErrorKind::Other, format!("Failed to get enumeration '{}'", name)) + )?; let members = members .iter() .map(|constr| zencode::decode(shared_state.symtab.to_str(*constr))) diff --git a/isla-mml/src/smt.rs b/isla-mml/src/smt.rs index fd7e4e1..3819ba1 100644 --- a/isla-mml/src/smt.rs +++ b/isla-mml/src/smt.rs @@ -30,6 +30,7 @@ use id_arena::{Arena, Id}; use std::borrow::Cow; use std::collections::{BTreeSet, HashMap}; +use std::io; use std::io::Write; use std::ops::Index; use std::sync::atomic::{AtomicU32, Ordering}; @@ -323,7 +324,9 @@ impl Sexp { } }, Sexp::Enum(e) => { - let members = typedefs.enums.get(&e.enum_id.to_name()).expect("Failed to get enumeration"); + let members = typedefs.enums.get(&e.enum_id.to_name()).ok_or_else(|| + io::Error::new(io::ErrorKind::Other, format!("Failed to get enumeration '{}'", e.enum_id.to_name())) + )?; let name = zencode::decode(typedefs.symtab.to_str(members[e.member])); write!(buf, "{}", name) }