From 8614d49e63bb672e90a34fbf7ed284c7b94f82ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 2 Dec 2024 13:53:50 -0500 Subject: [PATCH] expr: replace get_str with [...] --- src/expr/context.rs | 16 ++++++++++------ src/expr/eval.rs | 7 ++----- src/expr/nodes.rs | 2 +- src/expr/serialize.rs | 4 ++-- src/mc/smt.rs | 4 ++-- src/smt/serialize.rs | 4 ++-- src/system/serialize.rs | 2 +- 7 files changed, 20 insertions(+), 19 deletions(-) diff --git a/src/expr/context.rs b/src/expr/context.rs index 3f6a3d8..51409f5 100644 --- a/src/expr/context.rs +++ b/src/expr/context.rs @@ -105,12 +105,6 @@ impl Context { ExprRef::from_index(index) } - pub(crate) fn get_str(&self, reference: StringRef) -> &str { - self.strings - .get_index((reference.0.get() as usize) - 1) - .expect("Invalid StringRef!") - } - pub(crate) fn string(&mut self, value: std::borrow::Cow) -> StringRef { if let Some(index) = self.strings.get_index_of(value.as_ref()) { StringRef::from_index(index) @@ -135,6 +129,16 @@ impl Index for Context { } } +impl Index for Context { + type Output = String; + + fn index(&self, index: StringRef) -> &Self::Output { + self.strings + .get_index(index.index()) + .expect("Invalid StringRef!") + } +} + /// Convenience methods to construct IR nodes. impl Context { // helper functions to construct expressions diff --git a/src/expr/eval.rs b/src/expr/eval.rs index 771040f..e751e32 100644 --- a/src/expr/eval.rs +++ b/src/expr/eval.rs @@ -257,10 +257,7 @@ fn eval_expr_internal( Expr::BVSymbol { name, width } => { // we should not get here // TODO: turn into return Err - panic!( - "No value found for symbol: {} : bv<{width}>", - ctx.get_str(*name) - ); + panic!("No value found for symbol: {} : bv<{width}>", ctx[*name]); } Expr::BVLiteral(value) => bv_stack.push(value.get(ctx).into()), // unary @@ -333,7 +330,7 @@ fn eval_expr_internal( // TODO: turn into return Err panic!( "No value found for symbol: {} : bv<{index_width}> -> bv<{data_width}>", - ctx.get_str(*name) + ctx[*name] ); } Expr::ArrayConstant { index_width, .. } => { diff --git a/src/expr/nodes.rs b/src/expr/nodes.rs index be31da7..99827cb 100644 --- a/src/expr/nodes.rs +++ b/src/expr/nodes.rs @@ -164,7 +164,7 @@ impl Expr { } pub fn get_symbol_name<'a>(&self, ctx: &'a Context) -> Option<&'a str> { - self.get_symbol_name_ref().map(|r| ctx.get_str(r)) + self.get_symbol_name_ref().map(|r| ctx[r].as_str()) } pub fn is_true(&self) -> bool { diff --git a/src/expr/serialize.rs b/src/expr/serialize.rs index 8135f66..6a91f12 100644 --- a/src/expr/serialize.rs +++ b/src/expr/serialize.rs @@ -38,7 +38,7 @@ where W: Write, { match expr { - Expr::BVSymbol { name, .. } => write!(writer, "{}", ctx.get_str(*name)), + Expr::BVSymbol { name, .. } => write!(writer, "{}", ctx[*name]), Expr::BVLiteral(value) => { if value.width() <= 8 { write!(writer, "{}'b{}", value.width(), value.get(ctx).to_bit_str()) @@ -342,7 +342,7 @@ where } write!(writer, ")") } - Expr::ArraySymbol { name, .. } => write!(writer, "{}", ctx.get_str(*name)), + Expr::ArraySymbol { name, .. } => write!(writer, "{}", ctx[*name]), Expr::ArrayConstant { e, index_width, .. } => { write!(writer, "([")?; if (serialize_child)(e, writer)? { diff --git a/src/mc/smt.rs b/src/mc/smt.rs index aaadf6a..a5b919b 100644 --- a/src/mc/smt.rs +++ b/src/mc/smt.rs @@ -405,7 +405,7 @@ impl UnrollSmtEncoding { let skip = !(filter)(info); if !skip { let tpe = convert_tpe(smt_ctx, expr.get_type(ctx)); - let name = name_at(ctx.get_str(info.name), step); + let name = name_at(&ctx[info.name], step); if ctx[*expr].is_symbol() { smt_ctx.declare_const(escape_smt_identifier(&name), tpe)?; } else { @@ -431,7 +431,7 @@ impl UnrollSmtEncoding { let name_ref = if info.is_const { info.name } else { - let name = name_at(ctx.get_str(info.name), step); + let name = name_at(&ctx[info.name], step); ctx.string(name.into()) }; let tpe = signal.get_type(ctx); diff --git a/src/smt/serialize.rs b/src/smt/serialize.rs index 0b8fee8..6199069 100644 --- a/src/smt/serialize.rs +++ b/src/smt/serialize.rs @@ -31,7 +31,7 @@ pub fn convert_expr( match &ctx[expr_ref] { Expr::BVSymbol { name, .. } => { - let name_str = ctx.get_str(*name); + let name_str = &ctx[*name]; smt_ctx.atom(escape_smt_identifier(name_str)) } Expr::BVLiteral(value) => { @@ -220,7 +220,7 @@ pub fn convert_expr( let f = convert_expr(smt_ctx, ctx, *fals, patch_expr); smt_ctx.ite(c, t, f) } - Expr::ArraySymbol { name, .. } => smt_ctx.atom(escape_smt_identifier(ctx.get_str(*name))), + Expr::ArraySymbol { name, .. } => smt_ctx.atom(escape_smt_identifier(&ctx[*name])), Expr::ArrayConstant { e, index_width, diff --git a/src/system/serialize.rs b/src/system/serialize.rs index b92a4f2..c5f2501 100644 --- a/src/system/serialize.rs +++ b/src/system/serialize.rs @@ -32,7 +32,7 @@ fn serialize_transition_system( .map(|n| n.to_string()) .unwrap_or_else(|| { sys.names[root.expr] - .map(|n| ctx.get_str(n).to_string()) + .map(|n| ctx[n].clone()) .unwrap_or(format!("%{}", root.expr.index())) }); names[root.expr] = Some(name);