Additional Marker Configuration (#56)

## What Changed?

Exposes two marker configuration flags that I'd been toying with to the
outside. To do that it adds a new command line argument section for
grouping reasons.

The default behavior (both flags set to false) is the same as it was
before.

## Why Does It Need To?

These options were available before but not exposed.

## Checklist

- [x] Above description has been filled out so that upon quash merge we
have a
  good record of what changed.
- [x] New functions, methods, types are documented. Old documentation is
updated
  if necessary
- [x] Documentation in Notion has been updated
- [ ] Tests for new behaviors are provided
  - [ ] New test suites (if any) ave been added to the CI tests (in
`.github/workflows/rust.yml`) either as compiler test or integration
test.
*Or* justification for their omission from CI has been provided in this
PR
    description.

crates/paralegal-flow/src/args.rs

@@ -30,6 +30,7 @@ impl TryFrom<ClapArgs> for Args {
             anactrl,
             modelctrl,
             dump,
+            marker_control,
         } = value;
         let mut dump: DumpArgs = dump.into();
         if let Ok(from_env) = std::env::var("PARALEGAL_DUMP") {
@@ -59,6 +60,7 @@ impl TryFrom<ClapArgs> for Args {
             modelctrl,
             dump,
             build_config,
+            marker_control,
         })
     }
 }
@@ -76,6 +78,8 @@ pub struct Args {
     target: Option<String>,
     /// Abort the compilation after finishing the analysis
     abort_after_analysis: bool,
+    /// Additional arguments on marker assignment and discovery
+    marker_control: MarkerControl,
     /// Additional arguments that control the flow analysis specifically
     anactrl: AnalysisCtrl,
     /// Additional arguments that control the generation and composition of the model
@@ -120,6 +124,9 @@ pub struct ClapArgs {
     /// Additional arguments that control the flow analysis specifically
     #[clap(flatten, next_help_heading = "Flow Analysis")]
     anactrl: AnalysisCtrl,
+    /// Additional arguments which control marker assignment and discovery
+    #[clap(flatten, next_help_heading = "Marker Control")]
+    marker_control: MarkerControl,
     /// Additional arguments that control the generation and composition of the model
     #[clap(flatten, next_help_heading = "Model Generation")]
     modelctrl: ModelCtrl,
@@ -319,6 +326,10 @@ impl Args {
     pub fn build_config(&self) -> &BuildConfig {
         &self.build_config
     }
+
+    pub fn marker_control(&self) -> &MarkerControl {
+        &self.marker_control
+    }
 }
 
 #[derive(serde::Serialize, serde::Deserialize, clap::Args)]
@@ -357,6 +368,33 @@ impl ModelCtrl {
     }
 }
 
+/// Arguments which control marker assignment and discovery
+#[derive(serde::Serialize, serde::Deserialize, clap::Args)]
+pub struct MarkerControl {
+    /// Eagerly load markers for local items. This guarantees that all markers
+    /// on local items are emitted in the model, even if those items are never
+    /// used in the flow.
+    #[clap(long, env = "PARALEGAL_EAGER_LOCAL_MARKERS")]
+    eager_local_markers: bool,
+    /// Don't mark the outputs of local functions if they are of a marked type.
+    ///
+    /// Be aware that disabling this can cause unsoundness as inline
+    /// construction of such types will not be emitted into the model. A warning
+    /// is however emitted in that case.
+    #[clap(long, env = "PARALEGAL_NO_LOCAL_FUNCTION_TYPE_MARKING")]
+    no_local_function_type_marking: bool,
+}
+
+impl MarkerControl {
+    pub fn lazy_local_markers(&self) -> bool {
+        !self.eager_local_markers
+    }
+
+    pub fn local_function_type_marking(&self) -> bool {
+        !self.no_local_function_type_marking
+    }
+}
+
 /// Arguments that control the flow analysis
 #[derive(serde::Serialize, serde::Deserialize, clap::Args)]
 pub struct AnalysisCtrl {

crates/paralegal-flow/src/discover.rs

@@ -84,6 +84,13 @@ impl<'tcx> intravisit::Visitor<'tcx> for CollectingVisitor<'tcx> {
         self.tcx.hir()
     }
 
+    fn visit_id(&mut self, hir_id: rustc_hir::HirId) {
+        if !self.opts.marker_control().lazy_local_markers()
+            && let Some(owner_id) = hir_id.as_owner() {
+            self.marker_ctx.is_locally_marked(owner_id.def_id);
+        }
+    }
+
     /// Finds the functions that have been marked as targets.
     fn visit_fn(
         &mut self,

crates/paralegal-flow/src/marker_db.rs

@@ -3,7 +3,7 @@
 //! All interactions happen through the central database object: [`MarkerCtx`].
 
 use crate::{
-    args::Args,
+    args::{Args, MarkerControl},
     consts,
     desc::{Annotation, MarkerAnnotation},
     mir, ty,
@@ -36,7 +36,7 @@ impl<'tcx> MarkerCtx<'tcx> {
     /// Constructs a new marker database.
     ///
     /// This also loads any external annotations, as specified in the `args`.
-    pub fn new(tcx: TyCtxt<'tcx>, args: &Args) -> Self {
+    pub fn new(tcx: TyCtxt<'tcx>, args: &'static Args) -> Self {
         Self(Rc::new(MarkerDatabase::init(tcx, args)))
     }
 
@@ -242,8 +242,13 @@ impl<'tcx> MarkerCtx<'tcx> {
         self.combined_markers(function.def_id())
             .zip(std::iter::repeat(None))
             .chain(
-                self.all_type_markers(function.sig(self.tcx()).skip_binder().output())
-                    .map(|(marker, typeinfo)| (marker, Some(typeinfo))),
+                (self.0.config.local_function_type_marking() || !function.def_id().is_local())
+                    .then(|| {
+                        self.all_type_markers(function.sig(self.tcx()).skip_binder().output())
+                            .map(|(marker, typeinfo)| (marker, Some(typeinfo)))
+                    })
+                    .into_iter()
+                    .flatten(),
             )
     }
 }
@@ -262,16 +267,19 @@ struct MarkerDatabase<'tcx> {
     external_annotations: ExternalMarkers,
     /// Cache whether markers are reachable transitively.
     marker_reachable_cache: CopyCache<DefId, bool>,
+    /// Configuration options
+    config: &'static MarkerControl,
 }
 
 impl<'tcx> MarkerDatabase<'tcx> {
     /// Construct a new database, loading external markers.
-    fn init(tcx: TyCtxt<'tcx>, args: &Args) -> Self {
+    fn init(tcx: TyCtxt<'tcx>, args: &'static Args) -> Self {
         Self {
             tcx,
             local_annotations: Cache::default(),
             external_annotations: resolve_external_markers(args, tcx),
             marker_reachable_cache: Default::default(),
+            config: args.marker_control(),
         }
     }
 }