Support some of std::vec::Vec methods

src/analyze/basic_block.rs

@@ -209,7 +209,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     fn const_value_ty(&self, val: &mir::ConstValue<'tcx>, ty: &mir_ty::Ty<'tcx>) -> PlaceType {
         use mir::{interpret::Scalar, ConstValue, Mutability};
         match (ty.kind(), val) {
-            (mir_ty::TyKind::Int(_), ConstValue::Scalar(Scalar::Int(val))) => {
+            (
+                mir_ty::TyKind::Int(_) | mir_ty::TyKind::Uint(_),
+                ConstValue::Scalar(Scalar::Int(val)),
+            ) => {
                 let val = val.try_to_int(val.size()).unwrap();
                 PlaceType::with_ty_and_term(
                     rty::Type::int(),
@@ -576,7 +579,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     {
         // TODO: handle const_fn_def on Env side
         let func_ty = if let Some((def_id, args)) = func.const_fn_def() {
-            let resolved_def_id = if self.ctx.is_fn_trait_method(def_id) {
+            let (resolved_def_id, resolved_args) = if self.ctx.is_fn_trait_method(def_id) {
                 // When calling a closure via `Fn`/`FnMut`/`FnOnce` trait,
                 // we simply replace the def_id with the closure's function def_id.
                 // This skips shims, and makes self arguments mismatch. visitor::RustCallVisitor
@@ -585,7 +588,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                     panic!("expected closure arg for fn trait");
                 };
                 tracing::debug!(?closure_def_id, "closure instance");
-                *closure_def_id
+                (*closure_def_id, args)
             } else {
                 let param_env = self
                     .tcx
@@ -594,17 +597,17 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 let instance =
                     mir_ty::Instance::resolve(self.tcx, param_env, def_id, args).unwrap();
                 if let Some(instance) = instance {
-                    instance.def_id()
+                    (instance.def_id(), instance.args)
                 } else {
-                    def_id
+                    (def_id, args)
                 }
             };
             if def_id != resolved_def_id {
-                tracing::info!(?def_id, ?resolved_def_id, "resolve",);
+                tracing::info!(?def_id, ?resolved_def_id, ?resolved_args, "resolved");
             }
 
             self.ctx
-                .def_ty_with_args(resolved_def_id, args)
+                .def_ty_with_args(resolved_def_id, resolved_args)
                 .expect("unknown def")
                 .ty
                 .vacuous()

src/analyze/local_def.rs

@@ -387,7 +387,16 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                         rustc_hir::def::DefKind::Fn | rustc_hir::def::DefKind::AssocFn
                     ) {
                         assert!(self.inner_def_id.is_none(), "invalid extern_spec_fn");
-                        self.inner_def_id = Some(def_id);
+
+                        let args = typeck_result.node_args(hir_id);
+                        let param_env = self.tcx.param_env(self.outer_def_id);
+                        let instance =
+                            mir_ty::Instance::resolve(self.tcx, param_env, def_id, args).unwrap();
+                        if let Some(instance) = instance {
+                            self.inner_def_id = Some(instance.def_id());
+                        } else {
+                            self.inner_def_id = Some(def_id);
+                        }
                     }
                 }
             }

src/annot.rs

@@ -145,6 +145,8 @@ pub enum ParseAttrError {
     UnexpectedTerm { context: &'static str },
     #[error("unexpected formula {context}")]
     UnexpectedFormula { context: &'static str },
+    #[error("unknown method {ident:?} with {arg_count} arguments")]
+    UnknownMethod { ident: Ident, arg_count: usize },
 }
 
 impl ParseAttrError {
@@ -176,6 +178,10 @@ impl ParseAttrError {
     fn unexpected_formula(context: &'static str) -> Self {
         ParseAttrError::UnexpectedFormula { context }
     }
+
+    fn unknown_method(ident: Ident, arg_count: usize) -> Self {
+        ParseAttrError::UnknownMethod { ident, arg_count }
+    }
 }
 
 type Result<T> = std::result::Result<T, ParseAttrError>;
@@ -422,7 +428,7 @@ where
     }
 
     fn parse_arg_terms(&mut self) -> Result<Vec<chc::Term<T::Output>>> {
-        if self.look_ahead_token(0).is_none() {
+        if self.look_ahead_token_tree(0).is_none() {
             return Ok(Vec::new());
         }
 
@@ -607,23 +613,60 @@ where
     fn parse_postfix(&mut self) -> Result<FormulaOrTerm<T::Output>> {
         let formula_or_term = self.parse_atom()?;
 
-        let mut fields = Vec::new();
+        enum Field<V> {
+            Select(chc::Term<V>),
+            Store(chc::Term<V>, chc::Term<V>),
+            Index(usize),
+        }
+
+        let mut fields: Vec<Field<T::Output>> = Vec::new();
         while let Some(Token {
             kind: TokenKind::Dot,
             ..
         }) = self.look_ahead_token(0)
         {
             self.consume();
-            match self.next_token("field")? {
-                Token {
-                    kind: TokenKind::Literal(lit),
-                    ..
-                } if matches!(lit.kind, LitKind::Integer) => {
+            let t = self.next_token("field")?.clone();
+            if let Token {
+                kind: TokenKind::Literal(lit),
+                ..
+            } = t
+            {
+                if matches!(lit.kind, LitKind::Integer) {
                     let idx = lit.symbol.as_str().parse().unwrap();
-                    fields.push(idx);
+                    fields.push(Field::Index(idx));
+                    continue;
                 }
-                t => return Err(ParseAttrError::unexpected_token("field", t.clone())),
             }
+            if let Some((ident, _)) = t.ident() {
+                let next_tt = self.look_ahead_token_tree(0);
+                if let Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, args)) = next_tt {
+                    let args = args.clone();
+                    self.consume();
+                    let mut parser = Parser {
+                        resolver: self.boxed_resolver(),
+                        self_type_name: self.self_type_name.clone(),
+                        cursor: args.trees(),
+                        formula_existentials: self.formula_existentials.clone(),
+                    };
+                    let args = parser.parse_arg_terms()?;
+                    match ident.as_str() {
+                        "select" if args.len() == 1 => {
+                            fields.push(Field::Select(args.into_iter().next().unwrap()));
+                            continue;
+                        }
+                        "store" if args.len() == 2 => {
+                            let mut args = args.into_iter();
+                            let idx = args.next().unwrap();
+                            let val = args.next().unwrap();
+                            fields.push(Field::Store(idx, val));
+                            continue;
+                        }
+                        _ => return Err(ParseAttrError::unknown_method(ident, args.len())),
+                    }
+                }
+            }
+            return Err(ParseAttrError::unexpected_token("field", t.clone()));
         }
 
         if fields.is_empty() {
@@ -633,8 +676,19 @@ where
         let (term, sort) = formula_or_term
             .into_term()
             .ok_or_else(|| ParseAttrError::unexpected_formula("before projection"))?;
-        let term = fields.iter().fold(term, |acc, idx| acc.tuple_proj(*idx));
-        let sort = fields.iter().fold(sort, |acc, idx| acc.tuple_elem(*idx));
+        let sort = fields
+            .iter()
+            .try_fold(sort, |acc, field| match (acc, field) {
+                (acc, Field::Index(idx)) => Ok(acc.tuple_elem(*idx)),
+                (acc, Field::Store(_, _)) => Ok(acc),
+                (chc::Sort::Array(_, elem), Field::Select(_)) => Ok(*elem),
+                (acc, _) => Err(ParseAttrError::unsorted_op("select", acc.clone())),
+            })?;
+        let term = fields.into_iter().fold(term, |acc, field| match field {
+            Field::Index(idx) => acc.tuple_proj(idx),
+            Field::Store(idx, val) => acc.store(idx, val),
+            Field::Select(idx) => acc.select(idx),
+        });
         Ok(FormulaOrTerm::Term(term, sort))
     }
 

src/chc.rs

@@ -95,6 +95,7 @@ pub enum Sort {
     Box(Box<Sort>),
     Mut(Box<Sort>),
     Tuple(Vec<Sort>),
+    Array(Box<Sort>, Box<Sort>),
     Datatype(DatatypeSort),
 }
 
@@ -137,6 +138,21 @@ where
                         .group()
                 }
             }
+            Sort::Array(s1, s2) => {
+                if matches!(**s1, Sort::Int) {
+                    s2.pretty(allocator).brackets()
+                } else {
+                    allocator.text("array").append(
+                        allocator
+                            .line()
+                            .append(s1.pretty_atom(allocator))
+                            .append(allocator.text("->"))
+                            .append(allocator.line())
+                            .append(s2.pretty_atom(allocator))
+                            .parens(),
+                    )
+                }
+            }
             Sort::Datatype(sort) => sort.pretty(allocator),
         }
     }
@@ -164,18 +180,22 @@ impl Sort {
     fn walk_impl<'a, 'b>(&'a self, mut f: Box<dyn FnMut(&'a Sort) + 'b>) {
         f(self);
         match self {
+            Sort::Null | Sort::Int | Sort::Bool | Sort::String | Sort::Param(_) => {}
             Sort::Box(s) | Sort::Mut(s) => s.walk(Box::new(&mut f)),
             Sort::Tuple(ss) => {
                 for s in ss {
                     s.walk(Box::new(&mut f));
                 }
             }
+            Sort::Array(s1, s2) => {
+                s1.walk(Box::new(&mut f));
+                s2.walk(Box::new(&mut f));
+            }
             Sort::Datatype(sort) => {
                 for s in &sort.args {
                     s.walk(Box::new(&mut f));
                 }
             }
-            _ => {}
         }
     }
 
@@ -233,6 +253,10 @@ impl Sort {
         Sort::Tuple(sorts)
     }
 
+    pub fn array(from: Sort, to: Sort) -> Self {
+        Sort::Array(Box::new(from), Box::new(to))
+    }
+
     pub fn datatype(symbol: DatatypeSymbol, args: Vec<Sort>) -> Self {
         Sort::Datatype(DatatypeSort { symbol, args })
     }
@@ -257,6 +281,7 @@ impl Sort {
             Sort::Tuple(ts) => ts.iter().all(Sort::is_singleton),
             Sort::Box(s) => s.is_singleton(),
             Sort::Mut(s) => s.is_singleton(),
+            Sort::Array(_, s) => s.is_singleton(),
             _ => false,
         }
     }
@@ -271,6 +296,10 @@ impl Sort {
                     s.instantiate_params(args);
                 }
             }
+            Sort::Array(s1, s2) => {
+                s1.instantiate_params(args);
+                s2.instantiate_params(args);
+            }
             Sort::Datatype(sort) => {
                 for s in &mut sort.args {
                     s.instantiate_params(args);
@@ -361,7 +390,7 @@ impl Function {
         self.is_infix
     }
 
-    fn sort<I>(&self, _args: I) -> Sort
+    fn sort<I>(&self, args: I) -> Sort
     where
         I: IntoIterator<Item = Sort>,
     {
@@ -376,6 +405,13 @@ impl Function {
             Self::LT => Sort::bool(),
             Self::NOT => Sort::bool(),
             Self::NEG => Sort::int(),
+            Self::STORE => args.into_iter().next().unwrap(),
+            Self::SELECT => {
+                let Sort::Array(_, elem) = args.into_iter().next().unwrap() else {
+                    panic!("invalid SELECT sort");
+                };
+                *elem
+            }
             _ => unimplemented!(),
         }
     }
@@ -390,6 +426,8 @@ impl Function {
     pub const LT: Function = Function::infix("<");
     pub const NOT: Function = Function::new("not");
     pub const NEG: Function = Function::new("-");
+    pub const STORE: Function = Function::new("store");
+    pub const SELECT: Function = Function::new("select");
 }
 
 /// A logical term.
@@ -561,7 +599,11 @@ impl<V> Term<V> {
             Term::BoxCurrent(t) => t.sort(var_sort).deref(),
             Term::MutCurrent(t) => t.sort(var_sort).deref(),
             Term::MutFinal(t) => t.sort(var_sort).deref(),
-            Term::App(fun, args) => fun.sort(args.iter().map(|t| t.sort(&mut var_sort))),
+            Term::App(fun, args) => {
+                // TODO: remove this
+                let mut var_sort: Box<dyn FnMut(&V) -> Sort> = Box::new(var_sort);
+                fun.sort(args.iter().map(|t| t.sort(&mut var_sort)))
+            }
             Term::Tuple(ts) => {
                 // TODO: remove this
                 let mut var_sort: Box<dyn FnMut(&V) -> Sort> = Box::new(var_sort);
@@ -690,6 +732,14 @@ impl<V> Term<V> {
         Term::App(Function::NEG, vec![self])
     }
 
+    pub fn select(self, index: Self) -> Self {
+        Term::App(Function::SELECT, vec![self, index])
+    }
+
+    pub fn store(self, index: Self, elem: Self) -> Self {
+        Term::App(Function::STORE, vec![self, index, elem])
+    }
+
     pub fn tuple(ts: Vec<Term<V>>) -> Self {
         Term::Tuple(ts)
     }