Cheaper clones in symcc

Signed-off-by: Shaobo He <[email protected]>

Author: shaobo-he-aws

cedar-policy-symcc/src/symcc/concretizer.rs

@@ -282,7 +282,7 @@ impl Term {
 impl Udf {
     fn get_all_entity_uids(&self, uids: &mut BTreeSet<EntityUid>) {
         self.default.get_all_entity_uids(uids);
-        for (k, v) in &self.table {
+        for (k, v) in self.table.iter() {
             k.get_all_entity_uids(uids);
             v.get_all_entity_uids(uids);
         }

cedar-policy-symcc/src/symcc/decoder.rs

@@ -676,7 +676,7 @@ impl Uuf {
         Udf {
             arg: self.arg.clone(),
             out: self.out.clone(),
-            table: BTreeMap::new(),
+            table: Arc::new(BTreeMap::new()),
             default: self.out.default_literal(env),
         }
     }
@@ -1139,7 +1139,7 @@ impl SExpr {
                 Udf {
                     arg: uuf.arg.clone(),
                     out: uuf.out.clone(),
-                    table,
+                    table: Arc::new(table),
                     default,
                 },
             ));

cedar-policy-symcc/src/symcc/encoder.rs

@@ -341,7 +341,7 @@ impl<S: tokio::io::AsyncWrite + Unpin + Send> Encoder<'_, S> {
             Some(enc) => Ok(enc.clone()),
             None => {
                 let id = uuf_id(self.uufs.len());
-                self.script.comment(&uuf.id).await?;
+                self.script.comment(&uuf.id.clone()).await?;
                 let encoded_arg_type = self.encode_type(&uuf.arg).await?;
                 let encoded_out_type = self.encode_type(&uuf.out).await?;
                 self.script
@@ -827,7 +827,7 @@ mod unit_tests {
         };
         let mut encoder = Encoder::new(&symenv, Vec::<u8>::new()).unwrap();
         let my_uuf = crate::symcc::op::Uuf {
-            id: "my_fun".to_string(),
+            id: "my_fun".into(),
             arg: TermType::Bool,
             out: TermType::Bool,
         };

cedar-policy-symcc/src/symcc/env.rs

@@ -183,30 +183,30 @@ impl SymEntityData {
         match EntitySchemaEntry::of_schema(ety, validator_ety, schema) {
             // Corresponds to `SymEntityData.ofStandardEntityType` in Lean
             EntitySchemaEntry::Standard(sch) => {
-                let attrs_uuf = Uuf(op::Uuf {
-                    id: format!("attrs[{ety}]"),
+                let attrs_uuf = Uuf(Arc::new(op::Uuf {
+                    id: format!("attrs[{ety}]").into(),
                     arg: entity(ety.clone()), // more efficient than the Lean: avoids `TermType::of_type()` and constructs the `TermType` directly
                     out: TermType::of_type(&record(sch.attrs))?,
-                });
+                }));
                 let ancs_uuf = |anc_ty: &EntityType| {
-                    Uuf(op::Uuf {
-                        id: format!("ancs[{ety}, {anc_ty}]"),
+                    Uuf(Arc::new(op::Uuf {
+                        id: format!("ancs[{ety}, {anc_ty}]").into(),
                         arg: entity(ety.clone()), // more efficient than the Lean: avoids `TermType::of_type()` and constructs the `TermType` directly
                         out: TermType::set_of(entity(anc_ty.clone())), // more efficient than the Lean: avoids `TermType::of_type()` and constructs the `TermType` directly
-                    })
+                    }))
                 };
                 let sym_tags = |tag_ty: Type| -> Result<SymTags, CompileError> {
                     Ok(SymTags {
-                        keys: Uuf(op::Uuf {
-                            id: format!("tagKeys[{ety}]"),
+                        keys: Uuf(Arc::new(op::Uuf {
+                            id: format!("tagKeys[{ety}]").into(),
                             arg: entity(ety.clone()), // more efficient than the Lean: avoids `TermType::of_type()` and constructs the `TermType` directly
                             out: TermType::set_of(TermType::String),
-                        }),
-                        vals: Uuf(op::Uuf {
-                            id: format!("tagVals[{ety}]"),
+                        })),
+                        vals: Uuf(Arc::new(op::Uuf {
+                            id: format!("tagVals[{ety}]").into(),
                             arg: TermType::tag_for(ety.clone()), // record representing the pair type (ety, .string)
                             out: TermType::of_type(&tag_ty)?,
-                        }),
+                        })),
                     })
                 };
 
@@ -227,14 +227,14 @@ impl SymEntityData {
 
             // Corresponds to `SymEntityData.ofEnumEntityType` in Lean
             EntitySchemaEntry::Enum(eids) => {
-                let attrs_udf = Udf(function::Udf {
+                let attrs_udf = Udf(Arc::new(function::Udf {
                     arg: entity(ety.clone()),
                     out: TermType::Record {
                         rty: Arc::new(BTreeMap::new()),
                     },
-                    table: BTreeMap::new(),
+                    table: Arc::new(BTreeMap::new()),
                     default: Term::Record(Arc::new(BTreeMap::new())),
-                });
+                }));
                 Ok(SymEntityData {
                     attrs: attrs_udf,
                     ancestors: BTreeMap::new(),
@@ -251,14 +251,14 @@ impl SymEntityData {
         schema: &ValidatorSchema,
     ) -> Self {
         let sch = ActionSchemaEntries::of_schema(schema);
-        let attrs_udf = Udf(function::Udf {
+        let attrs_udf = Udf(Arc::new(function::Udf {
             arg: entity(act_ty.clone()),
             out: TermType::Record {
                 rty: Arc::new(BTreeMap::new()),
             },
-            table: BTreeMap::new(),
+            table: Arc::new(BTreeMap::new()),
             default: Term::Record(Arc::new(BTreeMap::new())),
-        });
+        }));
         let term_of_type = |ety: EntityType, uid: EntityUID| -> Option<Term> {
             if uid.type_name() == &ety {
                 Some(Term::Prim(TermPrim::Entity(uid)))
@@ -277,23 +277,24 @@ impl SymEntityData {
             }
         };
         let ancs_udf = |anc_ty: &EntityType| -> UnaryFunction {
-            Udf(function::Udf {
+            Udf(Arc::new(function::Udf {
                 arg: entity(act_ty.clone()),
                 out: TermType::set_of(entity(anc_ty.clone())),
-                table: sch
-                    .iter()
-                    .filter_map(|(uid, entry)| {
-                        Some((
-                            term_of_type(act_ty.clone(), uid.clone())?,
-                            ancs_term(anc_ty, &entry.ancestors),
-                        ))
-                    })
-                    .collect(),
+                table: Arc::new(
+                    sch.iter()
+                        .filter_map(|(uid, entry)| {
+                            Some((
+                                term_of_type(act_ty.clone(), uid.clone())?,
+                                ancs_term(anc_ty, &entry.ancestors),
+                            ))
+                        })
+                        .collect(),
+                ),
                 default: Term::Set {
                     elts: Arc::new(BTreeSet::new()),
                     elts_ty: entity(anc_ty.clone()),
                 },
-            })
+            }))
         };
         let acts = sch
             .iter()

cedar-policy-symcc/src/symcc/extractor.rs

@@ -25,7 +25,7 @@
 //! and transitive (assuming the suitable acyclicity and transitivity
 //! constraints are satisfied for the footprint).
 
-use std::collections::BTreeSet;
+use std::{collections::BTreeSet, sync::Arc};
 
 use cedar_policy_core::ast::Expr;
 
@@ -46,7 +46,7 @@ impl Uuf {
         arg_ety: &EntityType,
         footprints: &BTreeSet<EntityUID>,
         interp: &Interpretation<'_>,
-    ) -> Udf {
+    ) -> Arc<Udf> {
         // Get the current, potentially incorrect interpretation
         let udf = interp.interpret_fun(self);
 
@@ -57,18 +57,22 @@ impl Uuf {
                 if uid.type_name() == arg_ety {
                     let t = Term::Prim(TermPrim::Entity(uid.clone()));
                     // In the domain of this ancestor function
-                    Some((t.clone(), factory::app(UnaryFunction::Udf(udf.clone()), t)))
+                    Some((
+                        t.clone(),
+                        factory::app(UnaryFunction::Udf(Arc::new(udf.clone())), t),
+                    ))
                 } else {
                     None
                 }
             })
             .collect();
 
-        Udf {
-            table: new_table,
-            default: udf.out.default_literal(interp.env), // i.e., empty set
-            ..udf
-        }
+        Arc::new(Udf {
+            table: Arc::new(new_table),
+            default: udf.default.clone(),
+            arg: udf.arg.clone(),
+            out: udf.out.clone(),
+        })
     }
 }
 
@@ -98,8 +102,12 @@ impl Interpretation<'_> {
             for fun in ent_data.ancestors.values() {
                 if let UnaryFunction::Uuf(uuf) = fun {
                     funs.insert(
-                        uuf.clone(),
-                        uuf.repair_as_counterexample(ety, &footprint_uids, self),
+                        (**uuf).clone(),
+                        Arc::unwrap_or_clone(uuf.repair_as_counterexample(
+                            ety,
+                            &footprint_uids,
+                            self,
+                        )),
                     );
                 }
             }

cedar-policy-symcc/src/symcc/factory.rs

@@ -215,7 +215,7 @@ pub fn app(f: UnaryFunction, t: Term) -> Term {
         UnaryFunction::Uuf(f) => {
             let ret_ty = f.out.clone();
             Term::App {
-                op: Op::Uuf(Arc::new(f)),
+                op: Op::Uuf(f),
                 args: Arc::new(vec![t]),
                 ret_ty,
             }
@@ -224,10 +224,10 @@ pub fn app(f: UnaryFunction, t: Term) -> Term {
             if t.is_literal() {
                 match f.table.get(&t) {
                     Some(v) => v.clone(),
-                    None => f.default,
+                    None => f.default.clone(),
                 }
             } else {
-                f.table.iter().rfold(f.default, |acc, (t1, t2)| {
+                f.table.iter().rfold(f.default.clone(), |acc, (t1, t2)| {
                     ite(eq(t.clone(), t1.clone()), t2.clone(), acc)
                 })
             }

cedar-policy-symcc/src/symcc/function.rs

@@ -14,7 +14,7 @@
  * limitations under the License.
  */
 
-use std::collections::BTreeMap;
+use std::{collections::BTreeMap, sync::Arc};
 
 use super::{op::Uuf, term::Term, term_type::TermType};
 
@@ -23,7 +23,7 @@ use super::{op::Uuf, term::Term, term_type::TermType};
 pub struct Udf {
     pub arg: TermType,
     pub out: TermType,
-    pub table: BTreeMap<Term, Term>,
+    pub table: Arc<BTreeMap<Term, Term>>,
     pub default: Term,
 }
 
@@ -50,22 +50,22 @@ impl Udf {
 /// solver (CVC5) always returns interpretations of this form.
 #[derive(Clone, Debug, PartialEq, Eq, Ord, PartialOrd)]
 pub enum UnaryFunction {
-    Uuf(Uuf),
-    Udf(Udf),
+    Uuf(Arc<Uuf>),
+    Udf(Arc<Udf>),
 }
 
 impl UnaryFunction {
-    pub fn arg_type(self) -> TermType {
+    pub fn arg_type(&self) -> &TermType {
         match self {
-            UnaryFunction::Uuf(f) => f.arg,
-            UnaryFunction::Udf(f) => f.arg,
+            UnaryFunction::Uuf(f) => &f.arg,
+            UnaryFunction::Udf(f) => &f.arg,
         }
     }
 
-    pub fn out_type(self) -> TermType {
+    pub fn out_type(&self) -> &TermType {
         match self {
-            UnaryFunction::Uuf(f) => f.out,
-            UnaryFunction::Udf(f) => f.out,
+            UnaryFunction::Uuf(f) => &f.out,
+            UnaryFunction::Udf(f) => &f.out,
         }
     }
 

cedar-policy-symcc/src/symcc/interpretation.rs

@@ -109,7 +109,7 @@ impl Term {
                 ),
 
                 (Op::Uuf(uuf), [arg]) => factory::app(
-                    UnaryFunction::Udf(interp.interpret_fun(uuf)),
+                    UnaryFunction::Udf(Arc::new(interp.interpret_fun(uuf))),
                     arg.interpret(interp),
                 ),
 
@@ -252,7 +252,7 @@ impl UnaryFunction {
     pub fn interpret(&self, interp: &Interpretation<'_>) -> UnaryFunction {
         match self {
             UnaryFunction::Udf(..) => self.clone(),
-            UnaryFunction::Uuf(uuf) => UnaryFunction::Udf(interp.interpret_fun(uuf)),
+            UnaryFunction::Uuf(uuf) => UnaryFunction::Udf(Arc::new(interp.interpret_fun(uuf))),
         }
     }
 }

cedar-policy-symcc/src/symcc/op.rs

@@ -18,14 +18,16 @@
 
 use std::sync::Arc;
 
+use smol_str::SmolStr;
+
 use super::term_type::TermType;
 use super::type_abbrevs::*;
 
 /// Uninterpreted unary function.
 #[derive(Clone, Debug, PartialEq, Eq, Ord, PartialOrd)]
 pub struct Uuf {
     /// A unique identifier of the unary function.
-    pub id: String,
+    pub id: SmolStr,
     /// Argument type.
     pub arg: TermType,
     /// Output type.