[Rust] Change representation of Value for performance improvement

CHANGELOG.md

@@ -9,6 +9,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 ### Changed
+
+- Improved performance of small frequently allocated values (#1761)
+
 ### Deprecated
 ### Removed
 ### Fixed

evaluator/src/evaluator.rs

@@ -441,7 +441,7 @@ impl<'a> Interpreter<'a> {
             })
             .collect::<Vec<_>>();
 
-        Value::Lambda(registers, body)
+        Value::lambda(registers, body)
     }
 
     pub fn compile(&mut self, expr: &QuintEx) -> CompiledExpr {
@@ -470,17 +470,17 @@ impl<'a> Interpreter<'a> {
         match expr {
             QuintEx::QuintInt { id: _, value } => {
                 let value = *value;
-                CompiledExpr::new(move |_| Ok(Value::Int(value)))
+                CompiledExpr::new(move |_| Ok(Value::int(value)))
             }
 
             QuintEx::QuintBool { id: _, value } => {
                 let value = *value;
-                CompiledExpr::new(move |_| Ok(Value::Bool(value)))
+                CompiledExpr::new(move |_| Ok(Value::bool(value)))
             }
 
             QuintEx::QuintStr { id: _, value } => {
                 let value = value.clone();
-                CompiledExpr::new(move |_| Ok(Value::Str(value.clone())))
+                CompiledExpr::new(move |_| Ok(Value::str(value.clone())))
             }
 
             QuintEx::QuintName { id, name } => self
@@ -515,7 +515,7 @@ impl<'a> Interpreter<'a> {
                         CompiledExpr::new(move |env| {
                             let value = expr.execute(env)?;
                             register.borrow_mut().value = Some(value.clone());
-                            Ok(Value::Bool(true))
+                            Ok(Value::bool(true))
                         })
                     })
                 } else if LAZY_OPS.contains(&opcode.as_str()) {
@@ -546,7 +546,6 @@ impl<'a> Interpreter<'a> {
                     // Check if this is specifically a oneOf application
                     if let QuintEx::QuintApp { opcode, args, .. } = &opdef.expr {
                         if opcode == "oneOf" && args.len() == 1 {
-                            // Special handling for nondet oneOf on potentially empty sets
                             let set_expr = self.compile(&args[0]);
                             let cached_value = {
                                 let cached = self
@@ -607,12 +606,12 @@ impl<'a> Interpreter<'a> {
 
 fn builtin_value(name: &str) -> CompiledExpr {
     match name {
-        "true" => CompiledExpr::new(move |_| Ok(Value::Bool(true))),
-        "false" => CompiledExpr::new(move |_| Ok(Value::Bool(false))),
+        "true" => CompiledExpr::new(move |_| Ok(Value::bool(true))),
+        "false" => CompiledExpr::new(move |_| Ok(Value::bool(false))),
         "Bool" => CompiledExpr::new(move |_| {
-            Ok(Value::Set(ImmutableSet::from(vec![
-                Value::Bool(true),
-                Value::Bool(false),
+            Ok(Value::set(ImmutableSet::from(vec![
+                Value::bool(true),
+                Value::bool(false),
             ])))
         }),
         _ => unimplemented!("Unknown builtin name: {}", name),

evaluator/src/itf.rs

@@ -5,7 +5,7 @@
 //! This format can be parsed by Quint's typescript tool and by the ITF trace
 //! viewer extension on VSCode.
 
-use crate::value::Value;
+use crate::value::{Value, ValueInner};
 use chrono::{self};
 use itf;
 use std::collections::BTreeMap;
@@ -33,10 +33,14 @@ impl Trace {
 
         // Find the variable names by taking the fields from the first state
         // (which should be a record)
-        let vars = if let Some(Value::Record(map)) = self.states.first() {
-            map.keys().map(|v| v.to_string()).collect::<Vec<_>>()
+        let vars = if let Some(first_state) = self.states.first() {
+            if let ValueInner::Record(map) = first_state.0.as_ref() {
+                map.keys().map(|v| v.to_string()).collect::<Vec<_>>()
+            } else {
+                panic!("Expected a record, got {}", self.states[0]);
+            }
         } else {
-            panic!("Expected a record, got {}", self.states[0]);
+            panic!("No states found");
         };
 
         let mut other = BTreeMap::new();
@@ -74,37 +78,39 @@ impl Trace {
 
 impl Value {
     pub fn to_itf(&self) -> itf::Value {
-        match self {
-            Self::Int(i) => itf::Value::Number(*i),
-            Self::Bool(b) => itf::Value::Bool(*b),
-            Self::Str(s) => itf::Value::String(s.to_string()),
-            Self::Set(_)
-            | Self::Interval(_, _)
-            | Self::CrossProduct(_)
-            | Self::PowerSet(_)
-            | Self::MapSet(_, _) => {
+        match self.0.as_ref() {
+            ValueInner::Int(i) => itf::Value::Number(*i),
+            ValueInner::Bool(b) => itf::Value::Bool(*b),
+            ValueInner::Str(s) => itf::Value::String(s.to_string()),
+            ValueInner::Set(_)
+            | ValueInner::Interval(_, _)
+            | ValueInner::CrossProduct(_)
+            | ValueInner::PowerSet(_)
+            | ValueInner::MapSet(_, _) => {
                 itf::Value::Set(self.as_set().iter().map(|v| v.to_itf()).collect())
             }
-            Self::Tuple(elems) => itf::Value::Tuple(elems.iter().map(|v| v.to_itf()).collect()),
-            Self::Record(fields) => itf::Value::Record(
+            ValueInner::Tuple(elems) => {
+                itf::Value::Tuple(elems.iter().map(|v| v.to_itf()).collect())
+            }
+            ValueInner::Record(fields) => itf::Value::Record(
                 fields
                     .iter()
                     .map(|(k, v)| (k.to_string(), v.to_itf()))
                     .collect(),
             ),
-            Self::Map(map) => {
+            ValueInner::Map(map) => {
                 itf::Value::Map(map.iter().map(|(k, v)| (k.to_itf(), v.to_itf())).collect())
             }
-            Self::List(elems) => itf::Value::List(elems.iter().map(|v| v.to_itf()).collect()),
-            Self::Variant(label, value) => itf::Value::Record(
+            ValueInner::List(elems) => itf::Value::List(elems.iter().map(|v| v.to_itf()).collect()),
+            ValueInner::Variant(label, value) => itf::Value::Record(
                 vec![
                     ("tag".to_string(), itf::Value::String(label.to_string())),
                     ("value".to_string(), value.to_itf()),
                 ]
                 .into_iter()
                 .collect(),
             ),
-            Self::Lambda(_, _) => panic!("Cannot convert Lambda to ITF"),
+            ValueInner::Lambda(_, _) => panic!("Cannot convert Lambda to ITF"),
         }
     }
 }

evaluator/src/nondet.rs

@@ -6,7 +6,7 @@
 use crate::{
     evaluator::{CompiledExpr, Env},
     ir::QuintError,
-    value::Value,
+    value::{Value, ValueInner},
 };
 use std::cell::RefCell;
 use std::rc::Rc;
@@ -71,7 +71,7 @@ pub fn eval_nondet_one_of(
         let bounds = set.bounds();
         for bound in &bounds {
             if *bound == 0 {
-                return Ok(Value::Bool(false));
+                return Ok(Value::bool(false));
             }
         }
 
@@ -93,7 +93,8 @@ pub fn eval_nondet_one_of(
             let result = body_expr.execute(env);
 
             // If result is false and we can retry, try next position
-            let should_retry = matches!(result, Ok(Value::Bool(false))) && should_retry_set;
+            let should_retry = matches!(result, Ok(ref v) if matches!(v.0.as_ref(), ValueInner::Bool(false)))
+                && should_retry_set;
 
             if should_retry {
                 // Increment positions to try next combination

evaluator/src/normalizer.rs

@@ -2,42 +2,45 @@
 //! map keys and set elements, to make sure we don't end up with something like
 //! `Map(Set(1, 2, 3) -> "a", 1.to(3) -> "b")` (the two keys are the same).
 
-use crate::value::Value;
-use std::rc::Rc;
+use crate::value::{Value, ValueInner};
 
 impl Value {
     #[allow(clippy::unnecessary_to_owned)]
     pub fn normalize(self) -> Value {
-        match self {
-            Value::Int(_) | Value::Bool(_) | Value::Str(_) => self,
-            Value::Set(_)
-            | Value::Interval(_, _)
-            | Value::CrossProduct(_)
-            | Value::PowerSet(_)
-            | Value::MapSet(_, _) => Value::Set(
+        match self.0.as_ref() {
+            ValueInner::Int(_) | ValueInner::Bool(_) | ValueInner::Str(_) => self,
+            ValueInner::Set(_)
+            | ValueInner::Interval(_, _)
+            | ValueInner::CrossProduct(_)
+            | ValueInner::PowerSet(_)
+            | ValueInner::MapSet(_, _) => Value::set(
                 self.as_set()
                     .into_owned()
                     .into_iter()
                     .map(|v| v.normalize())
                     .collect(),
             ),
-            Value::Tuple(elems) => Value::Tuple(elems.into_iter().map(|v| v.normalize()).collect()),
-            Value::Record(fields) => Value::Record(
+            ValueInner::Tuple(elems) => {
+                Value::tuple(elems.iter().cloned().map(|v| v.normalize()).collect())
+            }
+            ValueInner::Record(fields) => Value::record(
                 fields
-                    .into_iter()
-                    .map(|(k, v)| (k, v.normalize()))
+                    .iter()
+                    .map(|(k, v)| (k.clone(), v.clone().normalize()))
                     .collect(),
             ),
-            Value::Map(map) => Value::Map(
-                map.into_iter()
-                    .map(|(k, v)| (k.normalize(), v.normalize()))
+            ValueInner::Map(map) => Value::map(
+                map.iter()
+                    .map(|(k, v)| (k.clone().normalize(), v.clone().normalize()))
                     .collect(),
             ),
-            Value::List(elems) => Value::List(elems.into_iter().map(|v| v.normalize()).collect()),
-            Value::Variant(label, value) => {
-                Value::Variant(label, Rc::new(<Value as Clone>::clone(&value).normalize()))
+            ValueInner::List(elems) => {
+                Value::list(elems.iter().cloned().map(|v| v.normalize()).collect())
+            }
+            ValueInner::Variant(label, value) => {
+                Value::variant(label.clone(), value.clone().normalize())
             }
-            Value::Lambda(_, _) => panic!("Cannot normalize lambda"),
+            ValueInner::Lambda(_, _) => panic!("Cannot normalize lambda"),
         }
     }
 }

evaluator/src/picker.rs

@@ -1,7 +1,7 @@
 //! Picking values out of sets without enumerating the elements.
 
-use crate::value::{powerset_at_index, ImmutableMap, Value};
-use std::{convert::TryInto, rc::Rc};
+use crate::value::{powerset_at_index, ImmutableMap, Value, ValueInner};
+use std::convert::TryInto;
 
 impl Value {
     /// Pick a value from the set, using the given indexes, without enumerating
@@ -10,46 +10,46 @@ impl Value {
     /// The given indexes should have the same length as the length [`bounds`]
     /// for this value, and each value should be within its respective bound.
     pub fn pick<T: Iterator<Item = usize>>(&self, indexes: &mut T) -> Value {
-        match self {
-            Value::Set(set) => {
+        match self.0.as_ref() {
+            ValueInner::Set(set) => {
                 let index = indexes
                     .next()
                     .expect("Internal error: too few positions. Report a bug");
                 set.iter().collect::<Vec<_>>()[index].clone()
             }
-            Value::Interval(start, end) => {
+            ValueInner::Interval(start, end) => {
                 let index = indexes
                     .next()
                     .expect("Internal error: too few positions. Report a bug");
                 let idx: i64 = <usize as TryInto<i64>>::try_into(index).unwrap();
                 assert!(idx <= end - start);
-                Value::Int(start + idx)
+                Value::int(start + idx)
             }
-            Value::CrossProduct(sets) => {
-                Value::Tuple(sets.iter().map(|value| value.pick(indexes)).collect())
+            ValueInner::CrossProduct(sets) => {
+                Value::tuple(sets.iter().map(|value| value.pick(indexes)).collect())
             }
-            Value::PowerSet(base_set) => {
+            ValueInner::PowerSet(base_set) => {
                 let index = indexes
                     .next()
                     .expect("Internal error: too few positions. Report a bug");
                 powerset_at_index(&base_set.as_set(), index)
             }
-            Value::MapSet(domain, range) => {
+            ValueInner::MapSet(domain, range) => {
                 let domain_size = domain.cardinality();
                 let range_size = range.cardinality();
 
                 if domain_size == 0 {
                     // To reflect the behaviour of TLC, an empty domain needs to give Set(Map()),
                     // so the only element we can pick is Map().
-                    return Value::Map(ImmutableMap::default());
+                    return Value::map(ImmutableMap::default());
                 }
 
                 assert!(range_size > 0, "Range can't be zero");
 
-                let range_to_pick = if let Value::MapSet(_, _) = **range {
-                    Rc::new(Value::Set(range.as_set().into_owned()))
+                let range_to_pick = if matches!(range.0.as_ref(), ValueInner::MapSet(_, _)) {
+                    Value::set(range.as_set().into_owned())
                 } else {
-                    Rc::clone(range)
+                    range.clone()
                 };
 
                 let keys = domain.as_set();
@@ -58,7 +58,7 @@ impl Value {
                     (key.clone(), value)
                 });
 
-                Value::Map(ImmutableMap::from_iter(key_values))
+                Value::map(ImmutableMap::from_iter(key_values))
             }
             _ => panic!("Not a set"),
         }
@@ -69,12 +69,12 @@ impl Value {
     // (set1.pick(r1), set2.pick(r2), ..., setn.pick(rn)). The `bounds` function will return the list of
     // ranges (bounds) from which each of those numbers should be picked from.
     pub fn bounds(&self) -> Vec<usize> {
-        match self {
-            Value::Set(set) => vec![set.len()],
-            Value::Interval(_, _) => vec![self.cardinality()],
-            Value::CrossProduct(sets) => sets.iter().map(|set| set.cardinality()).collect(),
-            Value::PowerSet(base_set) => vec![base_set.cardinality()],
-            Value::MapSet(domain, range) => {
+        match self.0.as_ref() {
+            ValueInner::Set(set) => vec![set.len()],
+            ValueInner::Interval(_, _) => vec![self.cardinality()],
+            ValueInner::CrossProduct(sets) => sets.iter().map(|set| set.cardinality()).collect(),
+            ValueInner::PowerSet(base_set) => vec![base_set.cardinality()],
+            ValueInner::MapSet(domain, range) => {
                 // Cardinality of range repeated domain times
                 vec![range.cardinality(); domain.cardinality()]
             }

evaluator/src/storage.rs

@@ -69,7 +69,7 @@ impl Storage {
         });
 
         // TODO: add nondet picks and action taken
-        Value::Record(ImmutableMap::from_iter(map))
+        Value::record(ImmutableMap::from_iter(map))
     }
 
     pub fn take_snapshot(&self) -> Snapshot {