Cherry-pick SymCC fixes/refactorings to 4.6.x

cedar-policy-core/src/extensions/decimal.rs

@@ -162,12 +162,12 @@ impl Decimal {
 
 impl std::fmt::Display for Decimal {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(
-            f,
-            "{}.{}",
-            self.value / i64::pow(10, NUM_DIGITS),
-            (self.value % i64::pow(10, NUM_DIGITS)).abs()
-        )
+        let abs = i128::from(self.value).abs();
+        if self.value.is_negative() {
+            write!(f, "-")?;
+        }
+        let pow = i128::pow(10, NUM_DIGITS);
+        write!(f, "{}.{:04}", abs / pow, abs % pow)
     }
 }
 
@@ -664,7 +664,7 @@ mod tests {
 
     fn check_round_trip(s: &str) {
         let d = Decimal::from_str(s).expect("should be a valid decimal");
-        assert_eq!(s, d.to_string());
+        assert_eq!(d, Decimal::from_str(d.to_string()).unwrap());
     }
 
     #[test]

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

@@ -329,11 +329,13 @@ impl<S: tokio::io::AsyncWrite + Unpin + Send> Encoder<'_, S> {
         ty_enc: &str,
         t_encs: impl IntoIterator<Item = &'s str>,
     ) -> Result<String> {
-        self.define_term(
-            ty_enc,
-            &format!("({ty_enc} {})", t_encs.into_iter().join(" ")),
-        )
-        .await
+        let t_encs = t_encs.into_iter().join(" ");
+        let t_enc = if t_encs.is_empty() {
+            format!("{ty_enc}")
+        } else {
+            format!("({ty_enc} {})", t_encs)
+        };
+        self.define_term(ty_enc, &t_enc).await
     }
 
     pub async fn encode_uuf(&mut self, uuf: &Uuf) -> Result<String> {
@@ -827,7 +829,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

@@ -35,7 +35,7 @@ use cedar_policy_core::validator::{
     ValidatorActionId,
 };
 use cedar_policy_core::validator::{ValidatorEntityType, ValidatorEntityTypeKind};
-use smol_str::SmolStr;
+use smol_str::{format_smolstr, SmolStr};
 use std::collections::{BTreeMap, BTreeSet};
 use std::ops::Deref;
 use std::sync::Arc;
@@ -55,15 +55,15 @@ impl SymRequest {
     pub fn empty_sym_req() -> Self {
         SymRequest {
             principal: Term::Var(TermVar {
-                id: "principal".to_string(),
+                id: "principal".into(),
                 ty: TermType::Bool,
             }),
             action: Term::Var(TermVar {
-                id: "action".to_string(),
+                id: "action".into(),
                 ty: TermType::Bool,
             }),
             resource: Term::Var(TermVar {
-                id: "resource".to_string(),
+                id: "resource".into(),
                 ty: TermType::Bool,
             }),
             context: Term::Record(Arc::new(BTreeMap::new())),
@@ -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_smolstr!("attrs[{ety}]"),
                     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_smolstr!("ancs[{ety}, {anc_ty}]"),
                         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_smolstr!("tagKeys[{ety}]"),
                             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_smolstr!("tagVals[{ety}]"),
                             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()
@@ -372,20 +373,20 @@ impl SymRequest {
     fn of_request_type(req_ty: &RequestType<'_>) -> Result<Self, CompileError> {
         Ok(Self {
             principal: Term::Var(TermVar {
-                id: "principal".to_string(),
+                id: "principal".into(),
                 ty: TermType::Entity {
                     ety: req_ty.principal.clone(),
                 },
             }),
             action: Term::Prim(TermPrim::Entity(req_ty.action.clone())),
             resource: Term::Var(TermVar {
-                id: "resource".to_string(),
+                id: "resource".into(),
                 ty: TermType::Entity {
                     ety: req_ty.resource.clone(),
                 },
             }),
             context: Term::Var(TermVar {
-                id: "context".to_string(),
+                id: "context".into(),
                 ty: TermType::of_type(&record(req_ty.context.clone()))?,
             }),
         })

cedar-policy-symcc/src/symcc/extension_types/decimal.rs

@@ -107,12 +107,12 @@ impl FromStr for Decimal {
 
 impl std::fmt::Display for Decimal {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(
-            f,
-            "{}.{}",
-            self.0 / i64::pow(10, DECIMAL_DIGITS),
-            (self.0 % i64::pow(10, DECIMAL_DIGITS)).abs()
-        )
+        let abs = i128::from(self.0).abs();
+        if self.0.is_negative() {
+            write!(f, "-")?;
+        }
+        let pow = i128::pow(10, DECIMAL_DIGITS);
+        write!(f, "{}.{:04}", abs / pow, abs % pow)
     }
 }
 

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;
 
@@ -57,17 +57,21 @@ 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
+            table: Arc::new(new_table),
+            default: udf.default.clone(),
+            arg: udf.arg.clone(),
+            out: udf.out,
         }
     }
 }
@@ -98,7 +102,7 @@ impl Interpretation<'_> {
             for fun in ent_data.ancestors.values() {
                 if let UnaryFunction::Uuf(uuf) = fun {
                     funs.insert(
-                        uuf.clone(),
+                        uuf.as_ref().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,
         }
     }