transform basic operations and literals

crates/diagnostics/src/lib.rs

@@ -20,7 +20,7 @@ pub enum ErrorType {
     Parser,
     Semantics,
     Type,
-    Functional,
+    Verification,
 }
 
 impl Display for ErrorType {
@@ -31,7 +31,7 @@ impl Display for ErrorType {
             ErrorType::Parser => word("Parser error"),
             ErrorType::Semantics => word("Semantic error"),
             ErrorType::Type => word("Type error"),
-            ErrorType::Functional => word("Functional error"),
+            ErrorType::Verification => word("Verification error"),
         }
     }
 }
@@ -64,6 +64,8 @@ pub struct Report {
     pub level: Level,
     /// Message of an error
     pub message: String,
+
+    pub additional_info: Vec<Report>,
 }
 
 impl Report {
@@ -74,6 +76,7 @@ impl Report {
             error_type: ErrorType::Lexer,
             level: Level::Error,
             message,
+            additional_info: vec![],
         }
     }
 
@@ -84,6 +87,7 @@ impl Report {
             error_type: ErrorType::Parser,
             level: Level::Error,
             message,
+            additional_info: vec![],
         }
     }
 
@@ -94,6 +98,7 @@ impl Report {
             error_type: ErrorType::Semantics,
             level: Level::Error,
             message,
+            additional_info: vec![],
         }
     }
 
@@ -104,6 +109,7 @@ impl Report {
             error_type: ErrorType::Semantics,
             level: Level::Warning,
             message,
+            additional_info: vec![],
         }
     }
 
@@ -114,16 +120,28 @@ impl Report {
             error_type: ErrorType::Type,
             level: Level::Error,
             message,
+            additional_info: vec![],
         }
     }
 
-    /// Build a report from the functional error.
-    pub fn func_error(loc: Span, message: String) -> Self {
+    /// Build a report from the verification error.
+    pub fn ver_error(loc: Span, message: String) -> Self {
+        Self {
+            loc,
+            error_type: ErrorType::Verification,
+            level: Level::Error,
+            message,
+            additional_info: vec![],
+        }
+    }
+    /// Build a report from the verification error with additional info.
+    pub fn ver_error_with_extra(loc: Span, message: String, errs: Vec<Report>) -> Self {
         Self {
             loc,
-            error_type: ErrorType::Functional,
+            error_type: ErrorType::Verification,
             level: Level::Error,
             message,
+            additional_info: errs,
         }
     }
 }

crates/semantics/src/expression/eval.rs

@@ -586,7 +586,7 @@ where
     let a = TryGetValue::<T>::try_get(u.left.as_ref())?;
     let b = TryGetValue::<T>::try_get(u.right.as_ref())?;
     let result = func(a, b).ok_or_else(|| {
-        contract.diagnostics.push(Report::func_error(
+        contract.diagnostics.push(Report::semantic_error(
             loc.clone(),
             String::from("The operation is invalid. Probably resulted from the division by 0 or overflow/underflow."),
         ));

crates/verifier/src/ast.rs

@@ -6,6 +6,7 @@ use folidity_semantics::{
 };
 use z3::{
     ast::{
+        Ast,
         Bool,
         Dynamic,
         Int,
@@ -72,72 +73,23 @@ impl<'ctx> ConstraintBlock<'ctx> {
     }
 }
 
-pub struct Variable<'ctx> {
-    /// Location of the expression
-    pub loc: Span,
-    /// Element of the expression.
-    pub element: Dynamic<'ctx>,
-}
-
-/// A list of Z3 concrete expression.
-/// Translated from the semantics AST?
-pub enum Z3Expression<'ctx> {
-    Variable(Z3UnaryExpression<usize>),
-
-    // Literals
-    Int(Z3UnaryExpression<Int<'ctx>>),
-    Real(Z3UnaryExpression<Real<'ctx>>),
-    Boolean(Z3UnaryExpression<Bool<'ctx>>),
-    String(Z3UnaryExpression<String<'ctx>>),
-
-    // Maths operations.
-    Multiply(Z3BinaryExpression),
-    Divide(Z3BinaryExpression),
-    Modulo(Z3BinaryExpression),
-    Add(Z3BinaryExpression),
-    Subtract(Z3BinaryExpression),
-
-    // Boolean relations.
-    Equal(Z3BinaryExpression),
-    NotEqual(Z3BinaryExpression),
-    Greater(Z3BinaryExpression),
-    Less(Z3BinaryExpression),
-    GreaterEq(Z3BinaryExpression),
-    LessEq(Z3BinaryExpression),
-    In(Z3BinaryExpression),
-    Not(Z3UnaryExpression<Box<Expression>>),
-
-    // Boolean operations.
-    Or(Z3BinaryExpression),
-    And(Z3BinaryExpression),
-
-    List(Z3UnaryExpression<Vec<Expression>>),
-}
-
 /// Represents unary style expression.
 ///
 /// # Example
 /// `false`
 #[derive(Clone, Debug, PartialEq)]
-pub struct Z3UnaryExpression<T> {
+pub struct Z3Expression<'ctx> {
     /// Location of the expression
     pub loc: Span,
     /// Element of the expression.
-    pub element: T,
+    pub element: Dynamic<'ctx>,
 }
 
-/// Represents binary-style expression.
-///
-/// # Example
-///
-/// - `10 + 2`
-/// - `a > b`
-#[derive(Clone, Debug, PartialEq)]
-pub struct Z3BinaryExpression {
-    /// Location of the parent expression.
-    pub loc: Span,
-    /// Left expression.
-    pub left: Box<Expression>,
-    /// Right expression
-    pub right: Box<Expression>,
+impl<'ctx> Z3Expression<'ctx> {
+    pub fn new(loc: &Span, e: &impl Ast<'ctx>) -> Self {
+        Self {
+            loc: loc.clone(),
+            element: Dynamic::from_ast(e),
+        }
+    }
 }