partially resolve models

crates/verifier/src/ast.rs

@@ -1,4 +1,8 @@
+use std::rc::Rc;
+
+use folidity_diagnostics::Report;
 use folidity_semantics::{
+    ast::Expression,
     GlobalSymbol,
     Span,
     SymbolInfo,
@@ -11,16 +15,22 @@ use z3::{
     },
     Context,
     Solver,
+    Sort,
+};
+
+use crate::{
+    executor::SymbolicExecutor,
+    transformer::transform_expr,
 };
 /// A declaration in the code AST.
-#[derive(Debug, Clone)]
+#[derive(Debug)]
 pub struct Declaration<'ctx> {
     /// Info about the declaration
     pub decl_sym: GlobalSymbol,
     /// Parent of the declaration.
     pub parent: Option<SymbolInfo>,
     /// Constraint block of the declaration.
-    pub block: ConstraintBlock<'ctx>,
+    pub constraints: Vec<Constraint<'ctx>>,
 }
 
 /// A singular constraint.
@@ -42,13 +52,41 @@ impl<'ctx> Constraint<'ctx> {
     pub fn sym_to_const<'a>(&self, ctx: &'a Context) -> Bool<'a> {
         Bool::new_const(ctx, self.binding_sym)
     }
+
+    pub fn from_expr(
+        expr: &Expression,
+        ctx: &'ctx Context,
+        diagnostics: &mut Vec<Report>,
+        executor: &mut SymbolicExecutor<'ctx>,
+    ) -> Result<Constraint<'ctx>, ()> {
+        let resolve_e = transform_expr(expr, &ctx, diagnostics, executor)?;
+        let Some(bool_expr) = resolve_e.element.as_bool() else {
+            diagnostics.push(Report::ver_error(
+                resolve_e.loc.clone(),
+                String::from("Expression must be boolean."),
+            ));
+            return Err(());
+        };
+        let (binding_const, n) = executor.create_constant(&Sort::bool(&ctx), &ctx);
+
+        let binding_expr = binding_const
+            .as_bool()
+            .expect("must be bool")
+            .implies(&bool_expr);
+
+        Ok(Constraint {
+            loc: resolve_e.loc.clone(),
+            binding_sym: n,
+            expr: binding_expr,
+        })
+    }
 }
 
 /// Block of constraints of to be verified.
-#[derive(Debug, Clone)]
+#[derive(Debug)]
 pub struct ConstraintBlock<'ctx> {
+    pub context: Context,
     /// Solver which is scoped to the specific constraint block.
-    pub solver: Solver<'ctx>,
     /// List of constraints in the given block.
     pub constraints: Vec<Constraint<'ctx>>,
 }
@@ -57,7 +95,7 @@ impl<'ctx> ConstraintBlock<'ctx> {
     /// Translate context to the new solver.
     pub fn translate_to_solver<'a>(&self, solver: &Solver<'a>) -> Solver<'a> {
         let new_ctx = solver.get_context();
-        self.solver.translate(new_ctx)
+        Solver::new(&self.context).translate(new_ctx)
     }
 
     /// Transform the list of ids of constraints into concrete boolean constants.

crates/verifier/src/executor.rs

@@ -1,44 +1,108 @@
+use std::rc::Rc;
+
 use folidity_diagnostics::Report;
+use folidity_semantics::{
+    ContractDefinition,
+    GlobalSymbol,
+    SymbolInfo,
+};
 use z3::{
-    ast::Dynamic,
+    ast::{
+        Ast,
+        Dynamic,
+    },
     Context,
     Solver,
     Sort,
 };
 
-use crate::ast::Declaration;
+use crate::{
+    ast::{
+        Constraint,
+        Declaration,
+        Z3Expression,
+    },
+    transformer::transform_expr,
+    z3_cfg,
+};
+
+//
 
-#[derive(Debug, Clone)]
+#[derive(Debug)]
 pub struct SymbolicExecutor<'ctx> {
     /// Global solver of the executor.
-    solver: Solver<'ctx>,
+    ///
+    /// We encapsulate it as it can't be easily transferred between scopes.
+    context: Context,
     /// List of resolved declaration to verify.
     pub declarations: Vec<Declaration<'ctx>>,
+    pub contexts: Vec<Context>,
     /// Symbol counter to track boolean constants across the program.
     pub symbol_counter: u32,
     pub diagnostics: Vec<Report>,
 }
 
 impl<'ctx> SymbolicExecutor<'ctx> {
-    pub fn new(context: &'ctx Context) -> Self {
+    pub fn new(context: Context) -> Self {
         Self {
-            solver: Solver::new(context),
+            context,
+            contexts: vec![],
             declarations: vec![],
             diagnostics: vec![],
             symbol_counter: 0,
         }
     }
 
+    pub fn parse_declarations(&mut self, contract: &ContractDefinition) -> Result<(), ()> {
+        let mut error = false;
+        let mut diagnostics = Vec::new();
+
+        for (i, m) in contract.models.iter().enumerate() {
+            let context = Context::new(&z3_cfg());
+            let z3_exprs: Vec<Z3Expression> = m
+                .bounds
+                .iter()
+                .filter_map(|e| {
+                    match transform_expr(e, &context, &mut diagnostics, self) {
+                        Ok(c) => Some(c),
+                        Err(_) => {
+                            error = true;
+                            None
+                        }
+                    }
+                })
+                .collect();
+
+            // let decl = Declaration {
+            //     decl_sym: GlobalSymbol::Model(SymbolInfo::new(m.loc.clone(), i)),
+            //     parent: m.parent.clone(),
+            //     constraints,
+            // };
+
+            // self.declarations.push(decl);
+        }
+
+        if error {
+            return Err(());
+        }
+        Ok(())
+    }
+
     /// Create a Z3 constant with the current symbol counter as a name while increasing
     /// the counter.
-    pub fn create_constant(
+    pub fn create_constant<'a>(
         &mut self,
-        sort: &Sort<'ctx>,
-        context: &'ctx Context,
-    ) -> (Dynamic<'ctx>, u32) {
+        sort: &Sort<'a>,
+        context: &'a Context,
+    ) -> (Dynamic<'a>, u32) {
         let id = self.symbol_counter;
-        let c = Dynamic::new_const(context, id, sort);
+        let c = Dynamic::new_const(&context, id, sort);
         self.symbol_counter += 1;
         (c, id)
     }
+
+    /// Retrieve the context of the internal `solver`.
+    pub fn context(&self) -> &Context {
+        &self.context
+    }
 }

crates/verifier/src/lib.rs

@@ -30,7 +30,7 @@ impl<'ctx> Runner<ContractDefinition, ()> for SymbolicExecutor<'ctx> {
         Self: std::marker::Sized,
     {
         let context = Context::new(&z3_cfg());
-        let executor = SymbolicExecutor::new(&context);
+        let executor = SymbolicExecutor::new(context);
 
         Ok(())
     }

crates/verifier/src/tests.rs

@@ -14,10 +14,7 @@ use num_bigint::{
 use num_traits::FromPrimitive;
 use z3::{
     ast::{
-        exists_const,
-        forall_const,
         Ast,
-        Bool,
         Int,
         Set,
         String as Z3String,
@@ -55,8 +52,9 @@ fn mul_transform() {
     });
 
     let context = Context::new(&z3_cfg());
-    let mut executor = SymbolicExecutor::new(&context);
-    let z3_res = transform_expr(&mul, &context, &mut executor);
+    let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg()));
+    let mut diagnostics = vec![];
+    let z3_res = transform_expr(&mul, &context, &mut diagnostics, &mut executor);
 
     assert!(z3_res.is_ok());
     let z3_e = z3_res.expect("Should be Ok");
@@ -76,8 +74,9 @@ fn var_transform() {
     });
 
     let context = Context::new(&z3_cfg());
-    let mut executor = SymbolicExecutor::new(&context);
-    let z3_res = transform_expr(&var, &context, &mut executor);
+    let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg()));
+    let mut diagnostics = vec![];
+    let z3_res = transform_expr(&var, &context, &mut diagnostics, &mut executor);
 
     assert!(z3_res.is_ok());
     let z3_e = z3_res.expect("Should be Ok");
@@ -94,8 +93,9 @@ fn string_hex_transform() {
     });
 
     let context = Context::new(&z3_cfg());
-    let mut executor = SymbolicExecutor::new(&context);
-    let z3_res = transform_expr(&string, &context, &mut executor);
+    let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg()));
+    let mut diagnostics = vec![];
+    let z3_res = transform_expr(&string, &context, &mut diagnostics, &mut executor);
 
     assert!(z3_res.is_ok());
     let z3_e = z3_res.expect("Should be Ok");
@@ -109,7 +109,7 @@ fn string_hex_transform() {
         element: hex::decode("AB").unwrap(),
         ty: TypeVariant::Int,
     });
-    let z3_res = transform_expr(&hex, &context, &mut executor);
+    let z3_res = transform_expr(&hex, &context, &mut diagnostics, &mut executor);
 
     assert!(z3_res.is_ok());
     let z3_e = z3_res.expect("Should be Ok");
@@ -145,8 +145,9 @@ fn list_transform() {
     });
 
     let context = Context::new(&z3_cfg());
-    let mut executor = SymbolicExecutor::new(&context);
-    let z3_res = transform_expr(&list, &context, &mut executor);
+    let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg()));
+    let mut diagnostics = vec![];
+    let z3_res = transform_expr(&list, &context, &mut diagnostics, &mut executor);
 
     assert!(z3_res.is_ok());
     let z3_e = z3_res.expect("Should be Ok");
@@ -233,11 +234,12 @@ fn in_transform() {
     });
 
     let context = Context::new(&z3_cfg());
-    let mut executor = SymbolicExecutor::new(&context);
+    let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg()));
+    let mut diagnostics = vec![];
 
     // verify that `30` is in the list.
     let solver = Solver::new(&context);
-    let z3_res = transform_expr(&in_true, &context, &mut executor);
+    let z3_res = transform_expr(&in_true, &context, &mut diagnostics, &mut executor);
     assert!(z3_res.is_ok());
     let z3_in_true = z3_res.expect("Ok");
     solver.push();
@@ -248,7 +250,7 @@ fn in_transform() {
     solver.push();
 
     // verify that `40` is not in the list.
-    let z3_res = transform_expr(&in_false, &context, &mut executor);
+    let z3_res = transform_expr(&in_false, &context, &mut diagnostics, &mut executor);
     assert!(z3_res.is_ok());
     let z3_in_true = z3_res.expect("Ok");
     solver.assert(&z3_in_true.element.as_bool().expect("Should be bool.").not());