Merge pull request #42 from umutdural/32-calculus-annotations-check-p…

…roc-calls

Refactored unsoundness checking

src/driver.rs

@@ -29,7 +29,7 @@ use crate::{
  proc_verify::{to_direction_lower_bounds, verify_proc},
  SpecCall,
  },
- proof_rules::EncCall,
+ proof_rules::EncodingVisitor,
  resource_limits::{LimitError, LimitsRef},
  servers::Server,
  slicing::{
@@ -360,10 +360,10 @@ impl SourceUnit {
  tcx: &mut TyCtx,
  source_units_buf: &mut Vec<Item<SourceUnit>>,
  ) -> Result<(), VerifyError> {
- let mut enc_call = EncCall::new(tcx, source_units_buf);
+ let mut encoding_visitor = EncodingVisitor::new(tcx, source_units_buf);
  let res = match self {
- SourceUnit::Decl(decl) => enc_call.visit_decl(decl),
- SourceUnit::Raw(block) => enc_call.visit_block(block),
+ SourceUnit::Decl(decl) => encoding_visitor.visit_decl(decl),
+ SourceUnit::Raw(block) => encoding_visitor.visit_block(block),
  };
  Ok(res.map_err(|ann_err| ann_err.diagnostic())?)
  }
@@ -416,11 +416,12 @@ pub struct VerifyUnit {
 impl VerifyUnit {
  /// Desugar assignments with procedure calls.
  #[instrument(skip(self, tcx))]
- pub fn desugar_spec_calls(&mut self, tcx: &mut TyCtx) -> Result<(), ()> {
- let mut spec_call = SpecCall::new(tcx);
- // TODO: give direction to spec_call so that it can check that only
- // valid directions are called
- spec_call.visit_block(&mut self.block)
+ pub fn desugar_spec_calls(&mut self, tcx: &mut TyCtx, name: String) -> Result<(), VerifyError> {
+ // Pass the context direction to the SpecCall so that it can check direction compatibility with called procedures
+ let mut spec_call = SpecCall::new(tcx, self.direction, name);
+ let res = spec_call.visit_block(&mut self.block);
+
+ Ok(res.map_err(|ann_err| ann_err.diagnostic())?)
  }
 
  /// Prepare the code for slicing.

src/intrinsic/annotations.rs

@@ -26,83 +26,131 @@ pub struct AnnotationDecl {
 
 #[derive(Debug)]
 pub enum AnnotationError {
- NotInProcedure(Span, Ident),
- NotOnWhile(Span, Ident, Stmt),
- WrongArgument(Span, Expr, String),
- NotTerminator(Span, Ident),
- CalculusEncodingMismatch(Direction, Span, Ident, Ident),
- UnknownAnnotation(Span, Ident),
+ NotInProcedure {
+ span: Span,
+ annotation_name: Ident,
+ },
+ NotOnWhile {
+ span: Span,
+ annotation_name: Ident,
+ annotated: Stmt,
+ },
+ WrongArgument {
+ span: Span,
+ arg: Expr,
+ message: String,
+ },
+ UnknownAnnotation {
+ span: Span,
+ annotation_name: Ident,
+ },
+}
+
+#[derive(Debug)]
+pub enum AnnotationUnsoundnessError {
+ NotTerminator {
+ span: Span,
+ enc_name: Ident,
+ },
+ CalculusEncodingMismatch {
+ direction: Direction,
+ span: Span,
+ calculus_name: Ident,
+ enc_name: Ident,
+ },
+ CalculusCallMismatch {
+ span: Span,
+ context_calculus: Ident,
+ call_calculus: Ident,
+ },
 }
 
 impl AnnotationError {
  pub fn diagnostic(self) -> Diagnostic {
  match self {
- AnnotationError::NotInProcedure(span, annotation) => {
- Diagnostic::new(ReportKind::Error, span)
- .with_message(format!(
- "The annotation `{}` can only be used inside a procedure.",
- annotation
- ))
- .with_label(
- Label::new(annotation.span).with_message("here"),
- )
- }
- AnnotationError::NotOnWhile(span, annotation, annotated) => {
- Diagnostic::new(ReportKind::Error, span)
- .with_message(format!(
- "The proof rule `{}` must be used on a while loop.",
- annotation
- ))
- .with_label(
- Label::new(annotated.span).with_message("This should be a while statement"),
- )
- }
- AnnotationError::WrongArgument(span, arg, message) => {
+ AnnotationError::NotInProcedure {
+ span,
+ annotation_name,
+ } => Diagnostic::new(ReportKind::Error, span)
+ .with_message(format!(
+ "The annotation `{}` can only be used inside a procedure.",
+ annotation_name
+ ))
+ .with_label(Label::new(annotation_name.span).with_message("here")),
+ AnnotationError::NotOnWhile {
+ span,
+ annotation_name,
+ annotated,
+ } => Diagnostic::new(ReportKind::Error, span)
+ .with_message(format!(
+ "The proof rule `{}` must be used on a while loop.",
+ annotation_name
+ ))
+ .with_label(
+ Label::new(annotated.span).with_message("This should be a while statement"),
+ ),
+ AnnotationError::WrongArgument { span, arg, message } => {
  Diagnostic::new(ReportKind::Error, span)
  .with_message(message)
  .with_label(Label::new(arg.span).with_message("here"))
  }
- AnnotationError::NotTerminator(span, encoding_name) => {
+ AnnotationError::UnknownAnnotation {
+ span,
+ annotation_name,
+ } => Diagnostic::new(ReportKind::Error, span)
+ .with_message(format!(
+ "The '{}' annotation is unknown.",
+ annotation_name.name
+ ))
+ .with_label(Label::new(span).with_message("This annotation is not defined.")),
+ }
+ }
+}
+
+impl AnnotationUnsoundnessError {
+ pub fn diagnostic(self) -> Diagnostic {
+ match self {
+ AnnotationUnsoundnessError::NotTerminator{span, enc_name} => {
  Diagnostic::new(ReportKind::Error, span)
  .with_message(format!(
  "The '{}' annotation must annotate the last statement of the program.",
- encoding_name.name
+ enc_name.name
  ))
  .with_label(Label::new(span).with_message(
  "There must not be any statements after this annotated statement (and the annotated statement must not be nested in a block).",
  ))
  }
- AnnotationError::CalculusEncodingMismatch(direction, span, calculus_name, encoding_name ) => {
+ AnnotationUnsoundnessError::CalculusEncodingMismatch{direction, span, calculus_name, enc_name } => {
  Diagnostic::new(ReportKind::Error, span)
  .with_message(format!(
  "In {}s, the '{}' calculus does not support the '{}' encoding.",
- direction.prefix("proc"), calculus_name.name, encoding_name.name
+ direction.prefix("proc"), calculus_name.name, enc_name.name
  ))
  .with_label(Label::new(span).with_message(
  "The calculus, proof rule, and direction are incompatible.",
  ))
  }
- AnnotationError::UnknownAnnotation(span, anno_name ) => {
+ AnnotationUnsoundnessError::CalculusCallMismatch{span,context_calculus,call_calculus} => {
  Diagnostic::new(ReportKind::Error, span)
  .with_message(format!(
- "The '{}' annotation is unknown.",
- anno_name.name
+ "Cannot call '{}' proc from '{}' proc.",
+  call_calculus.name, context_calculus.name
  ))
  .with_label(Label::new(span).with_message(
- "This annotation is not defined.",
+ "The calculus of the called procedure must match the calculus of the calling procedure.",
  ))
  }
  }
  }
 }
 
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, Copy, PartialEq)]
 pub struct Calculus {
  pub name: Ident,
  pub calculus_type: CalculusType,
 }
 
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, Copy, PartialEq)]
 
 pub enum CalculusType {
  Wp,

src/main.rs

@@ -588,7 +588,7 @@ fn verify_files_main(
  let (name, mut verify_unit) = verify_unit.enter_with_name();
 
  // 4. Desugaring: transforming spec calls to procs
- verify_unit.desugar_spec_calls(&mut tcx).unwrap();
+ verify_unit.desugar_spec_calls(&mut tcx, name.to_string())?;
 
  // print HeyVL core after desugaring if requested
  if options.print_core {

src/procs/spec_call.rs

@@ -1,28 +1,96 @@
 //! Replacement of calls to procedures by their specification.
 
+use std::ops::DerefMut;
+
+use ariadne::ReportKind;
+
 use crate::{
  ast::{
  util::FreeVariableCollector,
  visit::{walk_stmt, VisitorMut},
- Block, DeclKind, DeclRef, Expr, ExprData, ExprKind, Ident, Param, ProcSpec, Shared, Span,
- SpanVariant, Spanned, Stmt, StmtKind, Symbol, VarDecl, VarKind,
+ Block, DeclKind, DeclRef, Diagnostic, Direction, Expr, ExprData, ExprKind, Ident, Label,
+ Param, ProcSpec, Shared, Span, SpanVariant, Spanned, Stmt, StmtKind, Symbol, VarDecl,
+ VarKind,
  },
  slicing::{wrap_with_error_message, wrap_with_success_message},
  tyctx::TyCtx,
 };
 
 pub struct SpecCall<'tcx> {
  tcx: &'tcx mut TyCtx,
+ direction: Direction,
+ proc_name: String,
 }
 
 impl<'tcx> SpecCall<'tcx> {
- pub fn new(tcx: &'tcx mut TyCtx) -> Self {
- SpecCall { tcx }
+ pub fn new(tcx: &'tcx mut TyCtx, direction: Direction, proc_name: String) -> Self {
+ SpecCall {
+ tcx,
+ direction,
+ proc_name,
+ }
+ }
+}
+
+#[derive(Debug)]
+pub enum SpecCallError {
+ ProcDirectionMismatch {
+ calling_direction: Direction,
+ called_direction: Direction,
+ span: Span,
+ calling_proc: String,
+ called_proc: Ident,
+ },
+}
+
+impl SpecCallError {
+ pub fn diagnostic(&self) -> Diagnostic {
+ match self {
+ SpecCallError::ProcDirectionMismatch {
+ calling_direction,
+ called_direction,
+ span,
+ calling_proc,
+ called_proc,
+ } => Diagnostic::new(ReportKind::Error, *span)
+ .with_message(format!(
+ "The direction of '{} {}' does not match with the direction of the '{} {}'.",
+ calling_direction.prefix("proc"),
+ calling_proc,
+ called_direction.prefix("proc"),
+ called_proc.name
+ ))
+ .with_label(Label::new(*span).with_message(
+ "The direction of the called procedure must match the direction of the calling procedure.",
+ )),
+ }
  }
 }
 
 impl<'tcx> VisitorMut for SpecCall<'tcx> {
- type Err = ();
+ type Err = SpecCallError;
+
+ fn visit_expr(&mut self, e: &mut Expr) -> Result<(), Self::Err> {
+ if let ExprKind::Call(ref ident, _) = e.deref_mut().kind {
+ if let DeclKind::ProcDecl(proc_ref) = self.tcx.get(*ident).unwrap().as_ref() {
+ let proc_ref = proc_ref.clone(); // lose the reference to &mut self
+ let proc = proc_ref.borrow();
+ let context_direction = &self.direction;
+
+ if *context_direction != proc.direction {
+ // Throw direction unsoundness mismatch error
+ return Err(SpecCallError::ProcDirectionMismatch {
+ calling_direction: *context_direction,
+ called_direction: proc.direction,
+ span: e.span,
+ calling_proc: self.proc_name.clone(), // If there is a direction, there should be an ident as well
+ called_proc: proc.name,
+ });
+ }
+ }
+ }
+ Ok(())
+ }
 
  fn visit_stmt(&mut self, s: &mut Stmt) -> Result<(), Self::Err> {
  match &mut s.node {
@@ -45,6 +113,8 @@ impl<'tcx> VisitorMut for SpecCall<'tcx> {
  }
  }
  StmtKind::Assign(lhses, rhs) => {
+ // Visit the right-hand side first to ensure that the procedure call is valid.
+ self.visit_expr(rhs)?;
  if let Some(block) = self.encode_assign(s.span, lhses, rhs) {
  s.span = block.span;
  s.node = StmtKind::Seq(block.node);
@@ -233,4 +303,24 @@ mod test {
  let res = verify_test(source).0.unwrap();
  assert_eq!(res, false);
  }
+
+ #[test]
+ fn test_proc_direction_mismatch() {
+ // this should produce an error
+ let source = r#"
+ 
+ coproc test1() -> () {}
+ 
+ proc test2() -> () {
+ test1() // a coproc is being called from a proc
+ }
+ "#;
+ let res = verify_test(source).0;
+ assert!(res.is_err());
+ let err = res.unwrap_err();
+ assert_eq!(
+ err.to_string(),
+ "Error: The direction of 'proc <builtin>::test2' does not match with the direction of the 'coproc test1'."
+ );
+ }
 }

src/proof_rules/induction.rs

@@ -85,7 +85,7 @@ impl Encoding for InvariantAnnotation {
  resolve.visit_exprs(args)
  }
 
- fn is_calculus_allowed(&self, calculus: &Calculus, direction: Direction) -> bool {
+ fn is_calculus_allowed(&self, calculus: Calculus, direction: Direction) -> bool {
  matches!(
  (&calculus.calculus_type, direction),
  (CalculusType::Wp | CalculusType::Ert, Direction::Up)
@@ -169,7 +169,7 @@ impl Encoding for KIndAnnotation {
  Ok(())
  }
 
- fn is_calculus_allowed(&self, calculus: &Calculus, direction: Direction) -> bool {
+ fn is_calculus_allowed(&self, calculus: Calculus, direction: Direction) -> bool {
  matches!(
  (&calculus.calculus_type, direction),
  (CalculusType::Wp | CalculusType::Ert, Direction::Up)