mc: add some more nice error messages

Author: Philipp15b

src/ast/symbol.rs

@@ -23,6 +23,13 @@ impl Symbol {
     }
 }
 
+impl PartialEq<str> for Symbol {
+    fn eq(&self, other: &str) -> bool {
+        let interned = INTERNED_STRINGS.lock().unwrap();
+        interned.resolve(self.0).unwrap() == other
+    }
+}
+
 impl fmt::Debug for Symbol {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         let interned = INTERNED_STRINGS.lock().unwrap();

src/driver.rs

@@ -96,7 +96,7 @@ impl SourceUnitName {
         res
     }
 
-    /// Create a filne name for this source unit with the given file extension.
+    /// Create a file name for this source unit with the given file extension.
     ///
     /// This is used to create e.g. SMT-LIB output files for debugging. It is
     /// not necessarily related to the actual file name of the source unit.

src/intrinsic/annotations.rs

@@ -151,7 +151,6 @@ pub struct Calculus {
 }
 
 #[derive(Debug, Clone, Copy, PartialEq)]
-
 pub enum CalculusType {
     Wp,
     Wlp,

src/mc/mod.rs

@@ -18,6 +18,7 @@ use jani::{
     types::{BasicType, BoundedType, BoundedTypeBase, Type},
     Identifier,
 };
+use lsp_types::NumberOrString;
 
 use crate::{
     ast::{
@@ -45,10 +46,12 @@ pub enum JaniConversionError {
     UnsupportedPre(Expr),
     UnsupportedAssume(Expr),
     UnsupportedAssert(Expr),
+    UnsupportedHavoc { stmt: Stmt, can_eliminate: bool },
     UnsupportedInftyPost(Expr),
     NondetSelection(Span),
     MismatchedDirection(Span),
     UnsupportedCall(Span, Ident),
+    UnsupportedCalculus { proc: Ident, calculus: Ident },
 }
 
 impl JaniConversionError {
@@ -85,6 +88,16 @@ impl JaniConversionError {
                     .with_message("JANI: Assertion must be a Boolean expression")
                     .with_label(Label::new(expr.span).with_message("expected ?(b) here"))
             }
+            JaniConversionError::UnsupportedHavoc {stmt, can_eliminate} => {
+                let diagnostic = Diagnostic::new(ReportKind::Error, stmt.span)
+                    .with_message("JANI: Havoc is not supported")
+                    .with_label(Label::new(stmt.span).with_message("here"));
+                if *can_eliminate {
+                    diagnostic.with_note("You can replace the havoc with a re-declaration of its variables.")
+                } else {
+                    diagnostic
+                }
+            }
             JaniConversionError::UnsupportedInftyPost(expr) => {
                 Diagnostic::new(ReportKind::Error, expr.span)
                     .with_message("JANI: Post that evaluates to ∞ is not supported")
@@ -103,7 +116,11 @@ impl JaniConversionError {
                     .with_message(format!("JANI: Cannot call '{}'", ident.name))
                     .with_label(Label::new(*span).with_message("must be a func with a body"))
             }
+            JaniConversionError::UnsupportedCalculus { proc, calculus }=> Diagnostic::new(ReportKind::Error, proc.span)
+                .with_message(format!("JANI: Calculus '{}' is not supported", calculus))
+                .with_label(Label::new(proc.span).with_message("here")),
         }
+        .with_code(NumberOrString::String("model checking".to_owned()))
     }
 }
 
@@ -112,6 +129,8 @@ pub fn proc_to_model(
     tcx: &TyCtx,
     proc: &ProcDecl,
 ) -> Result<Model, JaniConversionError> {
+    check_calculus_annotation(proc)?;
+
     let expr_translator = ExprTranslator::new(tcx);
 
     // initialize the spec automaton
@@ -197,6 +216,20 @@ pub fn proc_to_model(
     Ok(model)
 }
 
+fn check_calculus_annotation(proc: &ProcDecl) -> Result<(), JaniConversionError> {
+    if let Some(calculus) = proc.calculus {
+        if &calculus.name != "wp" || &calculus.name != "ert"
+        // yeah that's ugly
+        {
+            return Err(JaniConversionError::UnsupportedCalculus {
+                proc: proc.name,
+                calculus,
+            });
+        }
+    }
+    Ok(())
+}
+
 /// Translate variable declarations, including local variable declarations, as
 /// well as input and output parameters.
 fn translate_var_decls(

src/mc/opsem.rs

@@ -142,10 +142,11 @@ fn translate_stmt(
 
             Ok(start)
         }
-        StmtKind::Havoc(_, _)
-        | StmtKind::Compare(_, _)
-        | StmtKind::Negate(_)
-        | StmtKind::Validate(_) => {
+        StmtKind::Havoc(dir, _) => Err(JaniConversionError::UnsupportedHavoc {
+            stmt: stmt.clone(),
+            can_eliminate: automaton.spec_part.direction == *dir,
+        }),
+        StmtKind::Compare(_, _) | StmtKind::Negate(_) | StmtKind::Validate(_) => {
             Err(JaniConversionError::UnsupportedStmt(Box::new(stmt.clone())))
         }
         StmtKind::Tick(expr) => translate_assign(