program slicing support in Caesar

src/ast/diagnostic.rs

@@ -124,6 +124,18 @@ impl Files {
         self.get(span.file).unwrap().char_span(span)
     }
 
+    pub fn get_human_span(&self, span: Span) -> Option<(&StoredFile, usize, usize)> {
+        if span.file == FileId::DUMMY {
+            None
+        } else {
+            let file = self.get(span.file).unwrap();
+            let char_span = file.char_span(span);
+            let (_line, line_number, col_number) =
+                file.lines.get_offset_line(char_span.start).unwrap();
+            Some((file, line_number + 1, col_number + 1))
+        }
+    }
+
     /// Formats the start of the span as a human-readable string. The format is
     /// `FILE:LINE:COL`, where `LINE` and `COL` are 1-indexed character offsets
     /// into the file.
@@ -133,20 +145,8 @@ impl Files {
     ///
     /// Returns `None` if the span's file id is [`FileId::DUMMY`].
     pub fn format_span_start(&self, span: Span) -> Option<String> {
-        if span.file == FileId::DUMMY {
-            None
-        } else {
-            let file = self.get(span.file).unwrap();
-            let char_span = file.char_span(span);
-            let (_line, line_number, col_number) =
-                file.lines.get_offset_line(char_span.start).unwrap();
-            Some(format!(
-                "{}:{}:{}",
-                file.path,
-                line_number + 1,
-                col_number + 1
-            ))
-        }
+        let (file, line_number, col_number) = self.get_human_span(span)?;
+        Some(format!("{}:{}:{}", file.path, line_number, col_number))
     }
 }
 

src/ast/expr.rs

@@ -13,6 +13,24 @@ use super::{shared::Shared, DeclKind, DeclRef, Ident, Span, Spanned, Symbol, TyK
 
 pub type Expr = Shared<ExprData>;
 
+impl Expr {
+    /// Replace this expression with another expression in-place.
+    ///
+    /// The alternative would be to simply clone this expression and then
+    /// overwrite the original location with the new expression. However, would
+    /// cause an unnecessary clone of the underlying [`ExprData`].
+    pub fn replace_with(&mut self, f: impl FnOnce(Expr) -> Expr) {
+        let default = || {
+            Shared::new(ExprData {
+                kind: ExprKind::Lit(Spanned::with_dummy_span(LitKind::Bool(false))),
+                ty: Some(TyKind::Bool),
+                span: Span::dummy_span(),
+            })
+        };
+        replace_with::replace_with(self, default, f)
+    }
+}
+
 impl fmt::Display for Expr {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         self.pretty().render_fmt(80, f)
@@ -373,7 +391,7 @@ impl FromStr for LitKind {
 impl fmt::Display for LitKind {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
-            LitKind::Str(symbol) => symbol.fmt(f),
+            LitKind::Str(symbol) => f.write_fmt(format_args!("\"{}\"", symbol)),
             LitKind::UInt(num) => num.fmt(f),
             LitKind::Frac(frac) => frac.fmt(f),
             LitKind::Infinity => f.write_str("∞"),

src/ast/ty.rs

@@ -25,6 +25,8 @@ pub enum TyKind {
     List(Box<TyKind>),
     /// A domain type.
     Domain(DeclRef<DomainDecl>),
+    /// A string type.
+    String,
     /// This is the current TyCtx's spec_ty
     SpecTy,
     /// A type defined somewhere which is not resolved yet.
@@ -63,6 +65,7 @@ impl fmt::Debug for TyKind {
             Self::Tuple(arg0) => f.debug_tuple("Tuple").field(arg0).finish(),
             Self::List(arg0) => f.debug_tuple("List").field(arg0).finish(),
             Self::Domain(arg0) => f.debug_tuple("Domain").field(&arg0.borrow().name).finish(),
+            Self::String => write!(f, "String"),
             Self::SpecTy => write!(f, "<spec ty>"),
             Self::Unresolved(arg0) => f.debug_tuple("Unresolved").field(arg0).finish(),
             Self::None => write!(f, "None"),
@@ -91,6 +94,7 @@ impl fmt::Display for TyKind {
             }
             Self::List(element_ty) => write!(f, "[]{}", element_ty),
             Self::Domain(arg0) => write!(f, "{}", &arg0.borrow().name),
+            Self::String => write!(f, "String"),
             Self::SpecTy => write!(f, "<spec ty>"),
             Self::Unresolved(name) => write!(f, "{}", name),
             Self::None => write!(f, "<none>"),

src/driver.rs

@@ -23,8 +23,13 @@ use crate::{
         SpecCall,
     },
     proof_rules::EncCall,
+    slicing::{
+        selection::SliceSelection,
+        transform::{SliceStmts, StmtSliceVisitor},
+    },
     tyctx::TyCtx,
     vc::vcgen::Vcgen,
+    Options,
 };
 use tracing::{info_span, instrument, trace};
 
@@ -329,6 +334,21 @@ impl VerifyUnit {
         spec_call.visit_stmts(&mut self.block)
     }
 
+    /// Prepare the code for slicing.
+    #[instrument(skip(self, options, tcx))]
+    pub fn prepare_slicing(&mut self, options: &Options, tcx: &mut TyCtx) -> SliceStmts {
+        let mut selection = SliceSelection::default();
+        if !options.no_slice_error {
+            selection |= SliceSelection::FAILURE_SELECTION;
+        }
+        if options.slice_verify {
+            selection |= SliceSelection::VERIFIED_SELECTION;
+        }
+        let mut stmt_slicer = StmtSliceVisitor::new(tcx, self.direction, selection);
+        stmt_slicer.visit_stmts(&mut self.block).unwrap();
+        stmt_slicer.finish()
+    }
+
     /// Generate the verification conditions with post-expectation `∞` or `0`
     /// depending on the direction (down or up, respectively).
     ///

src/front/parser/mod.rs

@@ -89,7 +89,7 @@ impl ParseError {
 }
 
 /// Parse a source code file into a list of declarations.
-#[instrument]
+#[instrument(skip(source))]
 pub fn parse_decls(file_id: FileId, source: &str) -> Result<Vec<DeclKind>, ParseError> {
     let clean_source = remove_comments(source).unwrap();
     let parser = grammar::DeclsParser::new();

src/intrinsic/annotations.rs

@@ -10,6 +10,7 @@ use crate::{
         tycheck::{Tycheck, TycheckError},
     },
     proof_rules::Encoding,
+    slicing::selection::SliceAnnotation,
 };
 
 #[derive(Debug, Clone)]
@@ -72,12 +73,14 @@ impl AnnotationError {
 #[derive(Debug, Clone)]
 pub enum AnnotationKind {
     Encoding(Rc<dyn Encoding>),
+    Slicing(Rc<SliceAnnotation>),
 }
 
 impl AnnotationKind {
     pub fn name(&self) -> Ident {
         match self {
             AnnotationKind::Encoding(encoding) => encoding.name(),
+            AnnotationKind::Slicing(annotation) => annotation.ident,
         }
     }
 
@@ -89,6 +92,7 @@ impl AnnotationKind {
     ) -> Result<(), TycheckError> {
         match self {
             AnnotationKind::Encoding(encoding) => encoding.tycheck(tycheck, call_span, args),
+            AnnotationKind::Slicing(annotation) => annotation.tycheck(tycheck, call_span, args),
         }
     }
 
@@ -100,6 +104,7 @@ impl AnnotationKind {
     ) -> Result<(), ResolveError> {
         match self {
             AnnotationKind::Encoding(encoding) => encoding.resolve(resolve, call_span, args),
+            AnnotationKind::Slicing(_) => Ok(()), // at the moment, these don't need the resolver
         }
     }
 }