include id in error on failing to find enumeration

rems-project · Jun 11, 2024 · 68ed1ca · 68ed1ca
1 parent 589695e
commit 68ed1ca
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 7 deletions.
diff --git 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
@@ -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<Accessor>);
 
 #[derive(Copy, Clone, Debug, Serialize, Deserialize)]
@@ -326,7 +332,9 @@ impl<B: BV> Val<B> {
             }
             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
@@ -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<B: BV, V: WriteVar>(
         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<B: BV>(
                     }
                     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
@@ -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)
             }