Insert raw commands into .smt2 file with #![raw_command()] attribute

.github/workflows/ci.yml

@@ -24,9 +24,33 @@ jobs:
     runs-on: ubuntu-latest
     permissions:
       contents: read
+    env:
+      COAR_IMAGE: ghcr.io/hiroshi-unno/coar@sha256:73144ed27a02b163d1a71b41b58f3b5414f12e91326015600cfdca64ff19f011
     steps:
       - uses: actions/checkout@v4
       - uses: ./.github/actions/setup-z3
+      - name: Setup thrust-pcsat-wrapper
+        run: |
+          docker pull "$COAR_IMAGE"
+
+          cat <<"EOF" > thrust-pcsat-wrapper
+          #!/bin/bash
+
+          smt2=$(mktemp -p . --suffix .smt2)
+          trap "rm -f $smt2" EXIT
+          cp "$1" "$smt2"
+          out=$(
+            docker run --rm -v "$PWD:/mnt" -w /root/coar "$COAR_IMAGE" \
+              main.exe -c ./config/solver/pcsat_tbq_ar.json -p pcsp "/mnt/$smt2"
+          )
+          exit_code=$?
+          echo "${out%,*}"
+          exit "$exit_code"
+          EOF
+          chmod +x thrust-pcsat-wrapper
+
+          mkdir -p ~/.local/bin
+          mv thrust-pcsat-wrapper ~/.local/bin/thrust-pcsat-wrapper
       - run: rustup show
       - uses: Swatinem/rust-cache@v2
       - run: cargo test

.github/workflows/docs.yml

@@ -0,0 +1,30 @@
+on:
+  push:
+    branches:
+      - main
+
+permissions: {}
+
+concurrency:
+  group: ${{ github.workflow }}
+
+jobs:
+  docs:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      pages: write
+      id-token: write
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - uses: actions/checkout@v4
+      - run: cargo doc --no-deps --document-private-items
+      - run: echo '<meta http-equiv="refresh" content="0;url=thrust">' > target/doc/index.html
+      - uses: actions/configure-pages@v5
+      - uses: actions/upload-pages-artifact@v3
+        with:
+          path: 'target/doc'
+      - id: deployment
+        uses: actions/deploy-pages@v4

src/analyze.rs

@@ -1,15 +1,24 @@
+//! Analysis of Rust MIR to generate a CHC system.
+//!
+//! The [`Analyzer`] generates subtyping constraints in the form of CHCs ([`chc::System`]).
+//! The entry point is [`crate_::Analyzer::run`], followed by [`local_def::Analyzer::run`]
+//! and [`basic_block::Analyzer::run`], while accumulating the necessary information in
+//! [`Analyzer`]. Once [`chc::System`] is collected for the entire input, it invokes an external
+//! CHC solver with the [`Analyzer::solve`] and subsequently reports the result.
+
 use std::cell::RefCell;
 use std::collections::HashMap;
 use std::rc::Rc;
 
 use rustc_hir::lang_items::LangItem;
+use rustc_index::IndexVec;
 use rustc_middle::mir::{self, BasicBlock, Local};
 use rustc_middle::ty::{self as mir_ty, TyCtxt};
 use rustc_span::def_id::{DefId, LocalDefId};
 
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
-use crate::refine::{self, BasicBlockType};
+use crate::refine::{self, BasicBlockType, TypeBuilder};
 use crate::rty;
 
 mod annot;
@@ -95,6 +104,44 @@ impl<'tcx> ReplacePlacesVisitor<'tcx> {
     }
 }
 
+#[derive(Debug, Clone)]
+struct DeferredDefTy<'tcx> {
+    cache: Rc<RefCell<HashMap<mir_ty::GenericArgsRef<'tcx>, rty::RefinedType>>>,
+}
+
+#[derive(Debug, Clone)]
+enum DefTy<'tcx> {
+    Concrete(rty::RefinedType),
+    Deferred(DeferredDefTy<'tcx>),
+}
+
+#[derive(Debug, Clone, Default)]
+pub struct EnumDefs {
+    defs: HashMap<DefId, rty::EnumDatatypeDef>,
+}
+
+impl EnumDefs {
+    pub fn find_by_name(&self, name: &chc::DatatypeSymbol) -> Option<&rty::EnumDatatypeDef> {
+        self.defs.values().find(|def| &def.name == name)
+    }
+
+    pub fn get(&self, def_id: DefId) -> Option<&rty::EnumDatatypeDef> {
+        self.defs.get(&def_id)
+    }
+
+    pub fn insert(&mut self, def_id: DefId, def: rty::EnumDatatypeDef) {
+        self.defs.insert(def_id, def);
+    }
+}
+
+impl refine::EnumDefProvider for Rc<RefCell<EnumDefs>> {
+    fn enum_def(&self, name: &chc::DatatypeSymbol) -> rty::EnumDatatypeDef {
+        self.borrow().find_by_name(name).unwrap().clone()
+    }
+}
+
+pub type Env = refine::Env<Rc<RefCell<EnumDefs>>>;
+
 #[derive(Clone)]
 pub struct Analyzer<'tcx> {
     tcx: TyCtxt<'tcx>,
@@ -104,33 +151,23 @@ pub struct Analyzer<'tcx> {
     /// currently contains only local-def templates,
     /// but will be extended to contain externally known def's refinement types
     /// (at least for every defs referenced by local def bodies)
-    defs: HashMap<DefId, rty::RefinedType>,
+    defs: HashMap<DefId, DefTy<'tcx>>,
 
     /// Resulting CHC system.
     system: Rc<RefCell<chc::System>>,
 
     basic_blocks: HashMap<LocalDefId, HashMap<BasicBlock, BasicBlockType>>,
     def_ids: did_cache::DefIdCache<'tcx>,
 
-    enum_defs: Rc<RefCell<HashMap<DefId, rty::EnumDatatypeDef>>>,
+    enum_defs: Rc<RefCell<EnumDefs>>,
 }
 
-impl<'tcx> crate::refine::TemplateTypeGenerator<'tcx> for Analyzer<'tcx> {
-    fn tcx(&self) -> TyCtxt<'tcx> {
-        self.tcx
-    }
-
+impl<'tcx> crate::refine::TemplateRegistry for Analyzer<'tcx> {
     fn register_template<V>(&mut self, tmpl: rty::Template<V>) -> rty::RefinedType<V> {
         tmpl.into_refined_type(|pred_sig| self.generate_pred_var(pred_sig))
     }
 }
 
-impl<'tcx> crate::refine::UnrefinedTypeGenerator<'tcx> for Analyzer<'tcx> {
-    fn tcx(&self) -> TyCtxt<'tcx> {
-        self.tcx
-    }
-}
-
 impl<'tcx> Analyzer<'tcx> {
     pub fn generate_pred_var(&mut self, sig: chc::PredSig) -> chc::PredVarId {
         self.system
@@ -165,7 +202,58 @@ impl<'tcx> Analyzer<'tcx> {
         }
     }
 
-    pub fn register_enum_def(&mut self, def_id: DefId, enum_def: rty::EnumDatatypeDef) {
+    fn build_enum_def(&self, def_id: DefId) -> rty::EnumDatatypeDef {
+        let adt = self.tcx.adt_def(def_id);
+
+        let name = refine::datatype_symbol(self.tcx, def_id);
+        let variants: IndexVec<_, _> = adt
+            .variants()
+            .iter()
+            .map(|variant| {
+                let name = refine::datatype_symbol(self.tcx, variant.def_id);
+                // TODO: consider using TyCtxt::tag_for_variant
+                let discr = resolve_discr(self.tcx, variant.discr);
+                let field_tys = variant
+                    .fields
+                    .iter()
+                    .map(|field| {
+                        let field_ty = self.tcx.type_of(field.did).instantiate_identity();
+                        TypeBuilder::new(self.tcx, def_id).build(field_ty)
+                    })
+                    .collect();
+                rty::EnumVariantDef {
+                    name,
+                    discr,
+                    field_tys,
+                }
+            })
+            .collect();
+
+        let generics = self.tcx.generics_of(def_id);
+        let ty_params = (0..generics.count())
+            .filter(|idx| {
+                matches!(
+                    generics.param_at(*idx, self.tcx).kind,
+                    mir_ty::GenericParamDefKind::Type { .. }
+                )
+            })
+            .count();
+        tracing::debug!(?def_id, ?name, ?ty_params, "ty_params count");
+
+        rty::EnumDatatypeDef {
+            name,
+            ty_params,
+            variants,
+        }
+    }
+
+    pub fn get_or_register_enum_def(&self, def_id: DefId) -> rty::EnumDatatypeDef {
+        let mut enum_defs = self.enum_defs.borrow_mut();
+        if let Some(enum_def) = enum_defs.get(def_id) {
+            return enum_def.clone();
+        }
+
+        let enum_def = self.build_enum_def(def_id);
         tracing::debug!(def_id = ?def_id, enum_def = ?enum_def, "register_enum_def");
         let ctors = enum_def
             .variants
@@ -190,30 +278,71 @@ impl<'tcx> Analyzer<'tcx> {
             params: enum_def.ty_params,
             ctors,
         };
-        self.enum_defs.borrow_mut().insert(def_id, enum_def);
+        enum_defs.insert(def_id, enum_def.clone());
         self.system.borrow_mut().datatypes.push(datatype);
-    }
 
-    pub fn find_enum_variant(
-        &self,
-        ty_sym: &chc::DatatypeSymbol,
-        v_sym: &chc::DatatypeSymbol,
-    ) -> Option<rty::EnumVariantDef> {
-        self.enum_defs
-            .borrow()
-            .iter()
-            .find(|(_, d)| &d.name == ty_sym)
-            .and_then(|(_, d)| d.variants.iter().find(|v| &v.name == v_sym))
-            .cloned()
+        enum_def
     }
 
     pub fn register_def(&mut self, def_id: DefId, rty: rty::RefinedType) {
         tracing::info!(def_id = ?def_id, rty = %rty.display(), "register_def");
-        self.defs.insert(def_id, rty);
+        self.defs.insert(def_id, DefTy::Concrete(rty));
     }
 
-    pub fn def_ty(&self, def_id: DefId) -> Option<&rty::RefinedType> {
-        self.defs.get(&def_id)
+    pub fn register_deferred_def(&mut self, def_id: DefId) {
+        tracing::info!(def_id = ?def_id, "register_deferred_def");
+        self.defs.insert(
+            def_id,
+            DefTy::Deferred(DeferredDefTy {
+                cache: Rc::new(RefCell::new(HashMap::new())),
+            }),
+        );
+    }
+
+    pub fn concrete_def_ty(&self, def_id: DefId) -> Option<&rty::RefinedType> {
+        self.defs.get(&def_id).and_then(|def_ty| match def_ty {
+            DefTy::Concrete(rty) => Some(rty),
+            DefTy::Deferred(_) => None,
+        })
+    }
+
+    pub fn def_ty_with_args(
+        &mut self,
+        def_id: DefId,
+        generic_args: mir_ty::GenericArgsRef<'tcx>,
+    ) -> Option<rty::RefinedType> {
+        let deferred_ty = match self.defs.get(&def_id)? {
+            DefTy::Concrete(rty) => {
+                let type_builder = TypeBuilder::new(self.tcx, def_id);
+
+                let mut def_ty = rty.clone();
+                def_ty.instantiate_ty_params(
+                    generic_args
+                        .types()
+                        .map(|ty| type_builder.build(ty))
+                        .map(rty::RefinedType::unrefined)
+                        .collect(),
+                );
+                return Some(def_ty);
+            }
+            DefTy::Deferred(deferred) => deferred,
+        };
+
+        let deferred_ty_cache = Rc::clone(&deferred_ty.cache); // to cut reference to allow &mut self
+        if let Some(rty) = deferred_ty_cache.borrow().get(&generic_args) {
+            return Some(rty.clone());
+        }
+
+        let mut analyzer = self.local_def_analyzer(def_id.as_local()?);
+        analyzer.generic_args(generic_args);
+
+        let expected = analyzer.expected_ty();
+        deferred_ty_cache
+            .borrow_mut()
+            .insert(generic_args, expected.clone());
+
+        analyzer.run(&expected);
+        Some(expected)
     }
 
     pub fn register_basic_block_ty(
@@ -243,14 +372,8 @@ impl<'tcx> Analyzer<'tcx> {
         self.register_def(panic_def_id, rty::RefinedType::unrefined(panic_ty.into()));
     }
 
-    pub fn new_env(&self) -> refine::Env {
-        let defs = self
-            .enum_defs
-            .borrow()
-            .values()
-            .map(|def| (def.name.clone(), def.clone()))
-            .collect();
-        refine::Env::new(defs)
+    pub fn new_env(&self) -> Env {
+        refine::Env::new(Rc::clone(&self.enum_defs))
     }
 
     pub fn crate_analyzer(&mut self) -> crate_::Analyzer<'tcx, '_> {
@@ -277,4 +400,40 @@ impl<'tcx> Analyzer<'tcx> {
             self.tcx.dcx().err(format!("verification error: {:?}", err));
         }
     }
+
+    /// Computes the signature of the local function.
+    ///
+    /// This works like `self.tcx.fn_sig(local_def_id).instantiate_identity().skip_binder()`,
+    /// but extracts parameter and return types directly from the given `body` to obtain a signature that
+    /// reflects potential type instantiations happened after `optimized_mir`.
+    pub fn local_fn_sig_with_body(
+        &self,
+        local_def_id: LocalDefId,
+        body: &mir::Body<'tcx>,
+    ) -> mir_ty::FnSig<'tcx> {
+        let ty = self.tcx.type_of(local_def_id).instantiate_identity();
+        let sig = if let mir_ty::TyKind::Closure(_, substs) = ty.kind() {
+            substs.as_closure().sig().skip_binder()
+        } else {
+            ty.fn_sig(self.tcx).skip_binder()
+        };
+
+        self.tcx.mk_fn_sig(
+            body.args_iter().map(|arg| body.local_decls[arg].ty),
+            body.return_ty(),
+            sig.c_variadic,
+            sig.unsafety,
+            sig.abi,
+        )
+    }
+
+    /// Computes the signature of the local function.
+    ///
+    /// This works like `self.tcx.fn_sig(local_def_id).instantiate_identity().skip_binder()`,
+    /// but extracts parameter and return types directly from [`mir::Body`] to obtain a signature that
+    /// reflects the actual type of lifted closure functions.
+    pub fn local_fn_sig(&self, local_def_id: LocalDefId) -> mir_ty::FnSig<'tcx> {
+        let body = self.tcx.optimized_mir(local_def_id);
+        self.local_fn_sig_with_body(local_def_id, body)
+    }
 }