Merge pull request rust-lang#22 from Chris-Hawblitzel/arc

Switch from Rc to Arc

verify/air/src/ast.rs

@@ -1,24 +1,24 @@
 use std::collections::HashMap;
-use std::rc::Rc;
+use std::sync::Arc;
 
-pub type RawSpan = Rc<dyn std::any::Any>;
+pub type RawSpan = Arc<dyn std::any::Any + std::marker::Sync + std::marker::Send>;
 #[derive(Clone)] // for Debug, see ast_util
 pub struct Span {
     pub description: Option<String>,
     pub raw_span: RawSpan,
     pub as_string: String, // if we can't print (description, raw_span), print as_string instead
 }
-pub type SpanOption = Rc<Option<Span>>;
+pub type SpanOption = Arc<Option<Span>>;
 
 pub type TypeError = String;
 
-pub type Ident = Rc<String>;
+pub type Ident = Arc<String>;
 
 pub(crate) type Snapshot = HashMap<Ident, u32>;
 pub(crate) type Snapshots = HashMap<Ident, Snapshot>;
 
-pub type Typ = Rc<TypX>;
-pub type Typs = Rc<Vec<Typ>>;
+pub type Typ = Arc<TypX>;
+pub type Typs = Arc<Vec<Typ>>;
 #[derive(Debug)]
 pub enum TypX {
     Bool,
@@ -29,7 +29,7 @@ pub enum TypX {
 #[derive(Clone, PartialEq, Eq, Hash)] // for Debug, see ast_util
 pub enum Constant {
     Bool(bool),
-    Nat(Rc<String>),
+    Nat(Arc<String>),
 }
 
 #[derive(Copy, Clone, Debug)]
@@ -59,8 +59,8 @@ pub enum MultiOp {
     Distinct,
 }
 
-pub type Binder<A> = Rc<BinderX<A>>;
-pub type Binders<A> = Rc<Vec<Binder<A>>>;
+pub type Binder<A> = Arc<BinderX<A>>;
+pub type Binders<A> = Arc<Vec<Binder<A>>>;
 #[derive(Clone)] // for Debug, see ast_util
 pub struct BinderX<A: Clone> {
     pub name: Ident,
@@ -74,17 +74,17 @@ pub enum Quant {
 }
 
 pub type Trigger = Exprs;
-pub type Triggers = Rc<Vec<Trigger>>;
+pub type Triggers = Arc<Vec<Trigger>>;
 
-pub type Bind = Rc<BindX>;
+pub type Bind = Arc<BindX>;
 #[derive(Clone, Debug)]
 pub enum BindX {
     Let(Binders<Expr>),
     Quant(Quant, Binders<Typ>, Triggers),
 }
 
-pub type Expr = Rc<ExprX>;
-pub type Exprs = Rc<Vec<Expr>>;
+pub type Expr = Arc<ExprX>;
+pub type Exprs = Arc<Vec<Expr>>;
 #[derive(Debug)]
 pub enum ExprX {
     Const(Constant),
@@ -99,8 +99,8 @@ pub enum ExprX {
     LabeledAssertion(SpanOption, Expr),
 }
 
-pub type Stmt = Rc<StmtX>;
-pub type Stmts = Rc<Vec<Stmt>>;
+pub type Stmt = Arc<StmtX>;
+pub type Stmts = Arc<Vec<Stmt>>;
 #[derive(Debug)]
 pub enum StmtX {
     Assume(Expr),
@@ -119,8 +119,8 @@ pub type Variants = Binders<Fields>;
 pub type Datatype = Binder<Variants>;
 pub type Datatypes = Binders<Variants>;
 
-pub type Decl = Rc<DeclX>;
-pub type Decls = Rc<Vec<Decl>>;
+pub type Decl = Arc<DeclX>;
+pub type Decls = Arc<Vec<Decl>>;
 #[derive(Debug)]
 pub enum DeclX {
     Sort(Ident),
@@ -131,15 +131,15 @@ pub enum DeclX {
     Axiom(Expr),
 }
 
-pub type Query = Rc<QueryX>;
+pub type Query = Arc<QueryX>;
 #[derive(Debug)]
 pub struct QueryX {
     pub local: Decls,    // local declarations
     pub assertion: Stmt, // checked by SMT with global and local declarations
 }
 
-pub type Command = Rc<CommandX>;
-pub type Commands = Rc<Vec<Command>>;
+pub type Command = Arc<CommandX>;
+pub type Commands = Arc<Vec<Command>>;
 #[derive(Debug)]
 pub enum CommandX {
     Push,                    // push space for temporary global declarations

verify/air/src/ast_util.rs

@@ -3,7 +3,7 @@ use crate::ast::{
     Typ, TypX, UnaryOp,
 };
 use std::fmt::Debug;
-use std::rc::Rc;
+use std::sync::Arc;
 
 impl Debug for Span {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> Result<(), std::fmt::Error> {
@@ -29,7 +29,7 @@ impl<A: Clone> BinderX<A> {
         &self,
         f: impl FnOnce(&A) -> Result<B, E>,
     ) -> Result<Binder<B>, E> {
-        Ok(Rc::new(BinderX { name: self.name.clone(), a: f(&self.a)? }))
+        Ok(Arc::new(BinderX { name: self.name.clone(), a: f(&self.a)? }))
     }
 }
 
@@ -43,55 +43,55 @@ impl<A: Clone + Debug> std::fmt::Debug for BinderX<A> {
 }
 
 pub fn str_ident(x: &str) -> Ident {
-    Rc::new(x.to_string())
+    Arc::new(x.to_string())
 }
 
 pub fn ident_var(x: &Ident) -> Expr {
-    Rc::new(ExprX::Var(x.clone()))
+    Arc::new(ExprX::Var(x.clone()))
 }
 
 pub fn string_var(x: &String) -> Expr {
-    Rc::new(ExprX::Var(Rc::new(x.clone())))
+    Arc::new(ExprX::Var(Arc::new(x.clone())))
 }
 
 pub fn str_var(x: &str) -> Expr {
-    Rc::new(ExprX::Var(Rc::new(x.to_string())))
+    Arc::new(ExprX::Var(Arc::new(x.to_string())))
 }
 
 pub fn ident_apply(x: &Ident, args: &Vec<Expr>) -> Expr {
-    Rc::new(ExprX::Apply(x.clone(), Rc::new(args.clone())))
+    Arc::new(ExprX::Apply(x.clone(), Arc::new(args.clone())))
 }
 
 pub fn string_apply(x: &String, args: &Vec<Expr>) -> Expr {
-    Rc::new(ExprX::Apply(Rc::new(x.clone()), Rc::new(args.clone())))
+    Arc::new(ExprX::Apply(Arc::new(x.clone()), Arc::new(args.clone())))
 }
 
 pub fn str_apply(x: &str, args: &Vec<Expr>) -> Expr {
-    Rc::new(ExprX::Apply(Rc::new(x.to_string()), Rc::new(args.clone())))
+    Arc::new(ExprX::Apply(Arc::new(x.to_string()), Arc::new(args.clone())))
 }
 
 pub fn int_typ() -> Typ {
-    Rc::new(TypX::Int)
+    Arc::new(TypX::Int)
 }
 
 pub fn bool_typ() -> Typ {
-    Rc::new(TypX::Bool)
+    Arc::new(TypX::Bool)
 }
 
 pub fn ident_typ(x: &Ident) -> Typ {
-    Rc::new(TypX::Named(x.clone()))
+    Arc::new(TypX::Named(x.clone()))
 }
 
 pub fn string_typ(x: &String) -> Typ {
-    Rc::new(TypX::Named(Rc::new(x.clone())))
+    Arc::new(TypX::Named(Arc::new(x.clone())))
 }
 
 pub fn str_typ(x: &str) -> Typ {
-    Rc::new(TypX::Named(Rc::new(x.to_string())))
+    Arc::new(TypX::Named(Arc::new(x.to_string())))
 }
 
 pub fn ident_binder<A: Clone>(x: &Ident, a: &A) -> Binder<A> {
-    Rc::new(BinderX { name: x.clone(), a: a.clone() })
+    Arc::new(BinderX { name: x.clone(), a: a.clone() })
 }
 
 pub fn mk_quantifier(
@@ -100,8 +100,8 @@ pub fn mk_quantifier(
     triggers: &Vec<Trigger>,
     body: &Expr,
 ) -> Expr {
-    Rc::new(ExprX::Bind(
-        Rc::new(BindX::Quant(quant, Rc::new(binders.clone()), Rc::new(triggers.clone()))),
+    Arc::new(ExprX::Bind(
+        Arc::new(BindX::Quant(quant, Arc::new(binders.clone()), Arc::new(triggers.clone()))),
         body.clone(),
     ))
 }
@@ -115,11 +115,11 @@ pub fn mk_exists(binders: &Vec<Binder<Typ>>, triggers: &Vec<Trigger>, body: &Exp
 }
 
 pub fn mk_true() -> Expr {
-    Rc::new(ExprX::Const(Constant::Bool(true)))
+    Arc::new(ExprX::Const(Constant::Bool(true)))
 }
 
 pub fn mk_false() -> Expr {
-    Rc::new(ExprX::Const(Constant::Bool(false)))
+    Arc::new(ExprX::Const(Constant::Bool(false)))
 }
 
 pub fn mk_and(exprs: &Vec<Expr>) -> Expr {
@@ -136,7 +136,7 @@ pub fn mk_and(exprs: &Vec<Expr>) -> Expr {
     } else if exprs.len() == 1 {
         exprs[0].clone()
     } else {
-        Rc::new(ExprX::Multi(MultiOp::And, Rc::new(exprs)))
+        Arc::new(ExprX::Multi(MultiOp::And, Arc::new(exprs)))
     }
 }
 
@@ -154,7 +154,7 @@ pub fn mk_or(exprs: &Vec<Expr>) -> Expr {
     } else if exprs.len() == 1 {
         exprs[0].clone()
     } else {
-        Rc::new(ExprX::Multi(MultiOp::Or, Rc::new(exprs)))
+        Arc::new(ExprX::Multi(MultiOp::Or, Arc::new(exprs)))
     }
 }
 
@@ -163,7 +163,7 @@ pub fn mk_not(e1: &Expr) -> Expr {
         ExprX::Const(Constant::Bool(false)) => mk_true(),
         ExprX::Const(Constant::Bool(true)) => mk_false(),
         ExprX::Unary(UnaryOp::Not, e) => e.clone(),
-        _ => Rc::new(ExprX::Unary(UnaryOp::Not, e1.clone())),
+        _ => Arc::new(ExprX::Unary(UnaryOp::Not, e1.clone())),
     }
 }
 
@@ -173,7 +173,7 @@ pub fn mk_implies(e1: &Expr, e2: &Expr) -> Expr {
         (ExprX::Const(Constant::Bool(true)), _) => e2.clone(),
         (_, ExprX::Const(Constant::Bool(false))) => mk_not(e1),
         (_, ExprX::Const(Constant::Bool(true))) => mk_true(),
-        _ => Rc::new(ExprX::Binary(BinaryOp::Implies, e1.clone(), e2.clone())),
+        _ => Arc::new(ExprX::Binary(BinaryOp::Implies, e1.clone(), e2.clone())),
     }
 }
 
@@ -185,10 +185,10 @@ pub fn mk_ite(e1: &Expr, e2: &Expr, e3: &Expr) -> Expr {
         (_, _, ExprX::Const(Constant::Bool(false))) => mk_and(&vec![e1.clone(), e2.clone()]),
         (_, ExprX::Const(Constant::Bool(true)), _) => mk_implies(&mk_not(e1), e3),
         (_, ExprX::Const(Constant::Bool(false)), _) => mk_and(&vec![mk_not(e1), e3.clone()]),
-        _ => Rc::new(ExprX::IfElse(e1.clone(), e2.clone(), e3.clone())),
+        _ => Arc::new(ExprX::IfElse(e1.clone(), e2.clone(), e3.clone())),
     }
 }
 
 pub fn mk_eq(e1: &Expr, e2: &Expr) -> Expr {
-    Rc::new(ExprX::Binary(BinaryOp::Eq, e1.clone(), e2.clone()))
+    Arc::new(ExprX::Binary(BinaryOp::Eq, e1.clone(), e2.clone()))
 }

verify/air/src/block_to_assert.rs

@@ -3,18 +3,18 @@ use crate::ast::{
 };
 use crate::ast_util::bool_typ;
 use crate::def::SWITCH_LABEL;
-use std::rc::Rc;
+use std::sync::Arc;
 
 fn stmt_to_expr(label_n: &mut u64, locals: &mut Vec<Decl>, stmt: &Stmt, pred: Expr) -> Expr {
     match &**stmt {
         StmtX::Assume(expr) => {
             // wp((assume Q), P) = Q ==> P
-            Rc::new(ExprX::Binary(BinaryOp::Implies, expr.clone(), pred))
+            Arc::new(ExprX::Binary(BinaryOp::Implies, expr.clone(), pred))
         }
         StmtX::Assert(span, expr) => {
             // wp((assert Q), P) = Q /\ P
-            let assertion = Rc::new(ExprX::LabeledAssertion(span.clone(), expr.clone()));
-            Rc::new(ExprX::Multi(MultiOp::And, Rc::new(vec![assertion, pred])))
+            let assertion = Arc::new(ExprX::LabeledAssertion(span.clone(), expr.clone()));
+            Arc::new(ExprX::Multi(MultiOp::And, Arc::new(vec![assertion, pred])))
         }
         StmtX::Havoc(_) => panic!("internal error: Havoc in block_to_assert"),
         StmtX::Assign(_, _) => panic!("internal error: Assign in block_to_assert"),
@@ -32,27 +32,27 @@ fn stmt_to_expr(label_n: &mut u64, locals: &mut Vec<Decl>, stmt: &Stmt, pred: Ex
             // To avoid duplicating P, we use:
             // wp((s1 or s2), P) = (P ==> label) ==> wp(s1, label) /\ wp(s2, label)
             //                   = (wp(s1, label) /\ wp(s2, label)) \/ (!label /\ P)
-            let label = Rc::new(format!("{}{}", SWITCH_LABEL, label_n));
+            let label = Arc::new(format!("{}{}", SWITCH_LABEL, label_n));
             *label_n += 1;
-            locals.push(Rc::new(DeclX::Const(label.clone(), bool_typ())));
-            let exp_label = Rc::new(ExprX::Var(label));
+            locals.push(Arc::new(DeclX::Const(label.clone(), bool_typ())));
+            let exp_label = Arc::new(ExprX::Var(label));
             let mut exprs: Vec<Expr> = Vec::new();
             for stmt in stmts.iter() {
                 exprs.push(stmt_to_expr(label_n, locals, stmt, exp_label.clone()));
             }
-            let neg_label = Rc::new(ExprX::Unary(UnaryOp::Not, exp_label));
-            let and1 = Rc::new(ExprX::Multi(MultiOp::And, Rc::new(exprs)));
-            let and2 = Rc::new(ExprX::Multi(MultiOp::And, Rc::new(vec![neg_label, pred])));
-            Rc::new(ExprX::Multi(MultiOp::Or, Rc::new(vec![and1, and2])))
+            let neg_label = Arc::new(ExprX::Unary(UnaryOp::Not, exp_label));
+            let and1 = Arc::new(ExprX::Multi(MultiOp::And, Arc::new(exprs)));
+            let and2 = Arc::new(ExprX::Multi(MultiOp::And, Arc::new(vec![neg_label, pred])));
+            Arc::new(ExprX::Multi(MultiOp::Or, Arc::new(vec![and1, and2])))
         }
     }
 }
 
 pub(crate) fn lower_query(query: &Query) -> Query {
     let mut locals: Vec<Decl> = (*query.local).clone();
     let mut switch_label: u64 = 0;
-    let tru = Rc::new(ExprX::Const(Constant::Bool(true)));
+    let tru = Arc::new(ExprX::Const(Constant::Bool(true)));
     let expr = stmt_to_expr(&mut switch_label, &mut locals, &query.assertion, tru);
-    let assertion = Rc::new(StmtX::Assert(Rc::new(None), expr));
-    Rc::new(QueryX { local: Rc::new(locals), assertion })
+    let assertion = Arc::new(StmtX::Assert(Arc::new(None), expr));
+    Arc::new(QueryX { local: Arc::new(locals), assertion })
 }

verify/air/src/context.rs

@@ -3,7 +3,7 @@ use crate::model::Model;
 use crate::print_parse::Logger;
 use crate::typecheck::Typing;
 use std::collections::{HashMap, HashSet};
-use std::rc::Rc;
+use std::sync::Arc;
 use z3::ast::Dynamic;
 use z3::{FuncDecl, Sort};
 
@@ -24,10 +24,10 @@ pub enum ValidityResult<'a> {
 pub struct Context<'ctx> {
     pub(crate) context: &'ctx z3::Context,
     pub(crate) solver: &'ctx z3::Solver<'ctx>,
-    pub(crate) typs: HashMap<Ident, Rc<Sort<'ctx>>>,
-    pub(crate) vars: HashMap<Ident, Dynamic<'ctx>>, // no Rc; Dynamic implements Clone
-    pub(crate) funs: HashMap<Ident, Rc<FuncDecl<'ctx>>>,
-    pub(crate) assert_infos: HashMap<Ident, Rc<AssertionInfo>>,
+    pub(crate) typs: HashMap<Ident, Arc<Sort<'ctx>>>,
+    pub(crate) vars: HashMap<Ident, Dynamic<'ctx>>, // no Arc; Dynamic implements Clone
+    pub(crate) funs: HashMap<Ident, Arc<FuncDecl<'ctx>>>,
+    pub(crate) assert_infos: HashMap<Ident, Arc<AssertionInfo>>,
     pub(crate) assert_infos_count: u64,
     pub(crate) typing: Typing,
     pub(crate) debug: bool,

verify/air/src/model.rs

@@ -79,7 +79,7 @@ impl<'a> Model<'a> {
                     let var_smt = new_const(context, &var_name, &typ);
                     let val = self.lookup_z3_var(&var_name, &var_smt);
                     value_snapshot.insert(var_name.clone(), val);
-                    //value_snapshot.insert(Rc::new((*var_name).clone()), val);
+                    //value_snapshot.insert(Arc::new((*var_name).clone()), val);
                 } else {
                     panic!("Expected local vars to all be constants at this point");
                 }