proof rules: better error handling

when proof rules were invoked with the wrong number of arguments, Caesar would just crash because the implementations of `resolve` assumed the correct number of arguments already, before type checking was done. we now do resolving independently of the number of arguments and let the type checking do that checking later. additionally, we also now properly handle the case where the first argument to the omega proof rule is not an identifier.
moves-rwth · Jun 21, 2024 · d432bbd · d432bbd
1 parent 8a45abb
commit d432bbd
Show file tree

Hide file tree

Showing 8 changed files with 71 additions and 91 deletions.
diff --git a/src/ast/visit.rs b/src/ast/visit.rs
@@ -80,7 +80,7 @@ pub trait VisitorMut: Sized {
         walk_expr(self, e)
     }
 
-    fn visit_exprs(&mut self, es: &mut Vec<Expr>) -> Result<(), Self::Err> {
+    fn visit_exprs(&mut self, es: &mut [Expr]) -> Result<(), Self::Err> {
         for e in es {
             self.visit_expr(e)?;
         }

diff --git a/src/front/resolve.rs b/src/front/resolve.rs
@@ -69,6 +69,7 @@ impl<'tcx> Resolve<'tcx> {
 pub enum ResolveError {
     AlreadyDefined(Span, Ident),
     NotFound(Ident),
+    NotIdent(Span),
 }
 
 impl ResolveError {
@@ -80,6 +81,9 @@ impl ResolveError {
             ResolveError::NotFound(ident) => Diagnostic::new(ReportKind::Error, ident.span)
                 .with_message(format!("Name `{}` is not declared", ident))
                 .with_label(Label::new(ident.span).with_message("not declared")),
+            ResolveError::NotIdent(span) => Diagnostic::new(ReportKind::Error, span)
+                .with_message(format!("Expression must be an identifier"))
+                .with_label(Label::new(span).with_message("found expression instead")),
         }
     }
 }

diff --git a/src/proof_rules/induction.rs b/src/proof_rules/induction.rs
@@ -24,9 +24,10 @@ use crate::{
     tyctx::TyCtx,
 };
 
-use super::{Encoding, EncodingEnvironment, EncodingGenerated};
-
-use super::util::*;
+use super::{
+    util::{encode_extend, encode_iter, intrinsic_param, lit_u128, one_arg, two_args},
+    Encoding, EncodingEnvironment, EncodingGenerated,
+};
 
 /// The "@induction" encoding is just syntactic sugar for 1-induction.
 pub struct InvariantAnnotation(pub AnnotationDecl);
@@ -80,8 +81,7 @@ impl Encoding for InvariantAnnotation {
         _call_span: Span,
         args: &mut [Expr],
     ) -> Result<(), ResolveError> {
-        let [invariant] = mut_one_arg(args);
-        resolve.visit_expr(invariant)
+        resolve.visit_exprs(args)
     }
 
     fn is_calculus_allowed(&self, calculus: &Calculus, direction: Direction) -> bool {
@@ -149,6 +149,15 @@ impl Encoding for KIndAnnotation {
         self.0.name
     }
 
+    fn resolve(
+        &self,
+        resolve: &mut Resolve<'_>,
+        _call_span: Span,
+        args: &mut [Expr],
+    ) -> Result<(), ResolveError> {
+        resolve.visit_exprs(args)
+    }
+
     fn tycheck(
         &self,
         tycheck: &mut Tycheck<'_>,
@@ -159,17 +168,6 @@ impl Encoding for KIndAnnotation {
         Ok(())
     }
 
-    fn resolve(
-        &self,
-        resolve: &mut Resolve<'_>,
-        _call_span: Span,
-        args: &mut [Expr],
-    ) -> Result<(), ResolveError> {
-        let [k, invariant] = mut_two_args(args);
-        resolve.visit_expr(k)?;
-        resolve.visit_expr(invariant)
-    }
-
     fn is_calculus_allowed(&self, calculus: &Calculus, direction: Direction) -> bool {
         matches!(
             (&calculus.calculus_type, direction),

diff --git a/src/proof_rules/mod.rs b/src/proof_rules/mod.rs
@@ -61,14 +61,6 @@ pub struct EncodingEnvironment {
 pub trait Encoding: fmt::Debug {
     fn name(&self) -> Ident;
 
-    /// Typecheck the arguments of the annotation call
-    fn tycheck(
-        &self,
-        tycheck: &mut Tycheck<'_>,
-        call_span: Span,
-        args: &mut [Expr],
-    ) -> Result<(), TycheckError>;
-
     /// Resolve the arguments of the annotation call
     fn resolve(
         &self,
@@ -77,6 +69,14 @@ pub trait Encoding: fmt::Debug {
         args: &mut [Expr],
     ) -> Result<(), ResolveError>;
 
+    /// Typecheck the arguments of the annotation call
+    fn tycheck(
+        &self,
+        tycheck: &mut Tycheck<'_>,
+        call_span: Span,
+        args: &mut [Expr],
+    ) -> Result<(), TycheckError>;
+
     /// Transform the annotated loop into a sequence of statements and declarations
     fn transform(
         &self,

diff --git a/src/proof_rules/omega.rs b/src/proof_rules/omega.rs
@@ -24,9 +24,10 @@ use crate::{
     tyctx::TyCtx,
 };
 
-use super::{Encoding, EncodingEnvironment, EncodingGenerated};
-
-use super::util::*;
+use super::{
+    util::{encode_iter, hey_const, intrinsic_param, two_args},
+    Encoding, EncodingEnvironment, EncodingGenerated,
+};
 
 pub struct OmegaInvAnnotation(AnnotationDecl);
 
@@ -64,36 +65,40 @@ impl Encoding for OmegaInvAnnotation {
         self.0.name
     }
 
-    fn tycheck(
+    fn resolve(
         &self,
-        tycheck: &mut Tycheck<'_>,
+        resolve: &mut Resolve<'_>,
         call_span: Span,
         args: &mut [Expr],
-    ) -> Result<(), TycheckError> {
-        check_annotation_call(tycheck, call_span, &self.0, args)?;
-        Ok(())
+    ) -> Result<(), ResolveError> {
+        let mut args_iter = args.iter_mut();
+        if let Some(free_var) = args_iter.next() {
+            if let ExprKind::Var(var_ref) = &free_var.kind {
+                let var_decl = VarDecl {
+                    name: *var_ref,
+                    ty: TyKind::UInt,
+                    kind: VarKind::Mut,
+                    init: None,
+                    span: call_span,
+                    created_from: None,
+                };
+                // Declare the free variable to be used in the omega invariant
+                resolve.declare(DeclKind::VarDecl(DeclRef::new(var_decl)))?;
+            } else {
+                return Err(ResolveError::NotIdent(free_var.span));
+            }
+        }
+        resolve.visit_exprs(args_iter.into_slice())
     }
 
-    fn resolve(
+    fn tycheck(
         &self,
-        resolve: &mut Resolve<'_>,
+        tycheck: &mut Tycheck<'_>,
         call_span: Span,
         args: &mut [Expr],
-    ) -> Result<(), ResolveError> {
-        let [free_var, omega_inv] = mut_two_args(args);
-        if let ExprKind::Var(var_ref) = &free_var.kind {
-            let var_decl = VarDecl {
-                name: *var_ref,
-                ty: TyKind::UInt,
-                kind: VarKind::Mut,
-                init: None,
-                span: call_span,
-                created_from: None,
-            };
-            // Declare the free variable to be used in the omega invariant
-            resolve.declare(DeclKind::VarDecl(DeclRef::new(var_decl)))?;
-        }
-        resolve.visit_expr(omega_inv)
+    ) -> Result<(), TycheckError> {
+        check_annotation_call(tycheck, call_span, &self.0, args)?;
+        Ok(())
     }
 
     fn is_calculus_allowed(&self, calculus: &Calculus, direction: Direction) -> bool {

diff --git a/src/proof_rules/past.rs b/src/proof_rules/past.rs
@@ -66,6 +66,15 @@ impl Encoding for PASTAnnotation {
         self.0.name
     }
 
+    fn resolve(
+        &self,
+        resolve: &mut Resolve<'_>,
+        _call_span: Span,
+        args: &mut [Expr],
+    ) -> Result<(), ResolveError> {
+        resolve.visit_exprs(args)
+    }
+
     fn tycheck(
         &self,
         tycheck: &mut Tycheck<'_>,
@@ -75,17 +84,6 @@ impl Encoding for PASTAnnotation {
         check_annotation_call(tycheck, call_span, &self.0, args)?;
         Ok(())
     }
-    fn resolve(
-        &self,
-        resolve: &mut Resolve<'_>,
-        _call_span: Span,
-        args: &mut [Expr],
-    ) -> Result<(), ResolveError> {
-        let [inv, eps, k] = mut_three_args(args);
-        resolve.visit_expr(inv)?;
-        resolve.visit_expr(eps)?;
-        resolve.visit_expr(k)
-    }
 
     fn is_calculus_allowed(&self, calculus: &Calculus, direction: Direction) -> bool {
         matches!(calculus.calculus_type, CalculusType::Ert) && direction == Direction::Up

diff --git a/src/proof_rules/unroll.rs b/src/proof_rules/unroll.rs
@@ -23,9 +23,10 @@ use crate::{
     tyctx::TyCtx,
 };
 
-use super::{Encoding, EncodingEnvironment, EncodingGenerated};
-
-use super::util::*;
+use super::{
+    util::{encode_unroll, hey_const, intrinsic_param, lit_u128, two_args},
+    Encoding, EncodingEnvironment, EncodingGenerated,
+};
 
 pub struct UnrollAnnotation(AnnotationDecl);
 
@@ -78,9 +79,7 @@ impl Encoding for UnrollAnnotation {
         _call_span: Span,
         args: &mut [Expr],
     ) -> Result<(), ResolveError> {
-        let [k, invariant] = mut_two_args(args);
-        resolve.visit_expr(k)?;
-        resolve.visit_expr(invariant)
+        resolve.visit_exprs(args)
     }
 
     fn is_calculus_allowed(&self, calculus: &Calculus, direction: Direction) -> bool {

diff --git a/src/proof_rules/util.rs b/src/proof_rules/util.rs
@@ -241,14 +241,6 @@ pub fn one_arg(args: &[Expr]) -> [&Expr; 1] {
     }
 }
 
-pub fn mut_one_arg(args: &mut [Expr]) -> [&mut Expr; 1] {
-    if let [a] = args {
-        [a]
-    } else {
-        unreachable!()
-    }
-}
-
 pub fn two_args(args: &[Expr]) -> [&Expr; 2] {
     if let [a, b] = args {
         [a, b]
@@ -257,14 +249,6 @@ pub fn two_args(args: &[Expr]) -> [&Expr; 2] {
     }
 }
 
-pub fn mut_two_args(args: &mut [Expr]) -> [&mut Expr; 2] {
-    if let [ref mut a, ref mut b] = args {
-        [a, b]
-    } else {
-        unreachable!()
-    }
-}
-
 pub fn three_args(args: &[Expr]) -> [&Expr; 3] {
     if let [a, b, c] = args {
         [a, b, c]
@@ -273,14 +257,6 @@ pub fn three_args(args: &[Expr]) -> [&Expr; 3] {
     }
 }
 
-pub fn mut_three_args(args: &mut [Expr]) -> [&mut Expr; 3] {
-    if let [a, b, c] = args {
-        [a, b, c]
-    } else {
-        unreachable!()
-    }
-}
-
 pub fn four_args(args: &[Expr]) -> [&Expr; 4] {
     if let [a, b, c, d] = args {
         [a, b, c, d]