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

Switch from Rc to Arc
utaal · Aug 23, 2021 · d02dead · d02dead
2 parents 1af55b2 9469863
commit d02dead
Show file tree

Hide file tree

Showing 31 changed files with 530 additions and 526 deletions.
diff --git a/verify/air/src/ast.rs b/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

diff --git a/verify/air/src/ast_util.rs b/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()))
 }
diff --git a/verify/air/src/block_to_assert.rs b/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 })
 }
diff --git a/verify/air/src/context.rs b/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,

diff --git a/verify/air/src/model.rs b/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");
  }