Enable tracing support (#1328)

* Enable tracing support

* Make tracing crate compile alone

* Create `log_dir` for trace output

* Disable doctests

* Documentation

Cargo.toml

@@ -6,6 +6,7 @@ members = [
     "prusti-tests",
     "prusti-common",
     "prusti-utils",
+    "tracing",
     "prusti-interface",
     "prusti-viper",
     "prusti-server",

analysis/Cargo.toml

@@ -12,6 +12,7 @@ env_logger = "0.10"
 syn = { version = "1.0", features = [ "full", "parsing" ] }
 derive_more = "0.99"
 prusti-rustc-interface = { path = "../prusti-rustc-interface" }
+tracing = { path = "../tracing" }
 
 [dev-dependencies]
 compiletest_rs = "0.9"

analysis/src/domains/definitely_accessible/state.rs

@@ -80,6 +80,7 @@ impl fmt::Debug for DefinitelyAccessibleState<'_> {
 
 impl<'mir, 'tcx: 'mir> PointwiseState<'mir, 'tcx, DefinitelyAccessibleState<'tcx>> {
     /// Make a best-effort at injecting statements to check the analysis state.
+    #[tracing::instrument(level = "debug", skip_all)]
     pub fn generate_test_program(&self, tcx: TyCtxt<'tcx>, source_map: &SourceMap) -> String {
         let mir_span = self.mir.span;
         let source_file = source_map.lookup_source_file(mir_span.data().lo);

analysis/src/domains/maybe_borrowed/analysis.rs

@@ -28,6 +28,7 @@ impl<'mir, 'tcx: 'mir> MaybeBorrowedAnalysis<'mir, 'tcx> {
         }
     }
 
+    #[tracing::instrument(level = "debug", skip(self))]
     pub fn run_analysis(
         &self,
     ) -> AnalysisResult<PointwiseState<'mir, 'tcx, MaybeBorrowedState<'tcx>>> {