optimise ast lifetimes

crates/verifier/src/ast.rs

@@ -23,7 +23,7 @@ use crate::{
     transformer::transform_expr,
 };
 /// A declaration in the code AST.
-#[derive(Debug)]
+#[derive(Debug, Default)]
 pub struct Declaration<'ctx> {
     /// Info about the declaration
     pub decl_sym: GlobalSymbol,
@@ -33,6 +33,37 @@ pub struct Declaration<'ctx> {
     pub constraints: Vec<Constraint<'ctx>>,
 }
 
+impl<'ctx> Declaration<'ctx> {
+    /// Translate context to the new solver.
+    pub fn translate_to_solver<'src_ctx>(
+        &self,
+        solver: &Solver<'src_ctx>,
+    ) -> Vec<Constraint<'src_ctx>>
+    where
+        'ctx: 'src_ctx,
+    {
+        let new_ctx = solver.get_context();
+        self.constraints
+            .iter()
+            .map(|c| {
+                Constraint {
+                    loc: c.loc.clone(),
+                    binding_sym: c.binding_sym,
+                    expr: c.expr.translate(new_ctx).clone(),
+                }
+            })
+            .collect()
+    }
+
+    /// Transform the list of ids of constraints into concrete boolean constants.
+    pub fn constraint_consts<'a>(&self, ctx: &'a Context) -> Vec<Bool<'a>> {
+        self.constraints
+            .iter()
+            .map(|c| c.sym_to_const(ctx))
+            .collect()
+    }
+}
+
 /// A singular constraint.
 #[derive(Debug, Clone)]
 pub struct Constraint<'ctx> {
@@ -53,12 +84,12 @@ impl<'ctx> Constraint<'ctx> {
         Bool::new_const(ctx, self.binding_sym)
     }
 
-    pub fn from_expr(
+    pub fn from_expr<'a>(
         expr: &Expression,
-        ctx: &'ctx Context,
+        ctx: &'a Context,
         diagnostics: &mut Vec<Report>,
         executor: &mut SymbolicExecutor<'ctx>,
-    ) -> Result<Constraint<'ctx>, ()> {
+    ) -> Result<Constraint<'a>, ()> {
         let resolve_e = transform_expr(expr, &ctx, diagnostics, executor)?;
         let Some(bool_expr) = resolve_e.element.as_bool() else {
             diagnostics.push(Report::ver_error(
@@ -82,31 +113,6 @@ impl<'ctx> Constraint<'ctx> {
     }
 }
 
-/// Block of constraints of to be verified.
-#[derive(Debug)]
-pub struct ConstraintBlock<'ctx> {
-    pub context: Context,
-    /// Solver which is scoped to the specific constraint block.
-    /// List of constraints in the given block.
-    pub constraints: Vec<Constraint<'ctx>>,
-}
-
-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();
-        Solver::new(&self.context).translate(new_ctx)
-    }
-
-    /// Transform the list of ids of constraints into concrete boolean constants.
-    pub fn constraint_consts<'a>(&self, ctx: &'a Context) -> Vec<Bool<'a>> {
-        self.constraints
-            .iter()
-            .map(|c| c.sym_to_const(ctx))
-            .collect()
-    }
-}
-
 /// Represents unary style expression.
 ///
 /// # Example

crates/verifier/src/executor.rs

@@ -33,53 +33,58 @@ pub struct SymbolicExecutor<'ctx> {
     /// Global solver of the executor.
     ///
     /// We encapsulate it as it can't be easily transferred between scopes.
-    context: Context,
+    solver: Solver<'ctx>,
+    pub local_contexts: Vec<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: Context) -> Self {
+    pub fn new(context: &'ctx Context) -> Self {
         Self {
-            context,
-            contexts: vec![],
+            solver: Solver::new(context),
+            local_contexts: vec![],
             declarations: vec![],
             diagnostics: vec![],
             symbol_counter: 0,
         }
     }
 
-    pub fn parse_declarations(&mut self, contract: &ContractDefinition) -> Result<(), ()> {
+    pub fn parse_declarations(
+        &mut self,
+        contract: &ContractDefinition,
+        context: &'ctx Context,
+    ) -> 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
-                        }
+        for i in 0..contract.models.len() {
+            let mut constraints: Vec<Constraint> = vec![];
+            let m = &contract.models[i];
+
+            for e in &m.bounds {
+                match Constraint::from_expr(e, context, &mut diagnostics, self) {
+                    Ok(c) => constraints.push(c),
+                    Err(_) => {
+                        error = true;
+                        continue;
                     }
-                })
-                .collect();
+                };
+            }
 
-            // let decl = Declaration {
-            //     decl_sym: GlobalSymbol::Model(SymbolInfo::new(m.loc.clone(), i)),
-            //     parent: m.parent.clone(),
-            //     constraints,
-            // };
+            let decl = Declaration {
+                constraints,
+                decl_sym: GlobalSymbol::Model(SymbolInfo {
+                    loc: m.loc.clone(),
+                    i,
+                }),
+                parent: m.parent.clone(),
+            };
 
-            // self.declarations.push(decl);
+            self.declarations.push(decl);
         }
 
         if error {
@@ -103,6 +108,6 @@ impl<'ctx> SymbolicExecutor<'ctx> {
 
     /// Retrieve the context of the internal `solver`.
     pub fn context(&self) -> &Context {
-        &self.context
+        self.solver.get_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

@@ -52,7 +52,7 @@ fn mul_transform() {
     });
 
     let context = Context::new(&z3_cfg());
-    let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg()));
+    let mut executor = SymbolicExecutor::new(&context);
     let mut diagnostics = vec![];
     let z3_res = transform_expr(&mul, &context, &mut diagnostics, &mut executor);
 
@@ -74,7 +74,7 @@ fn var_transform() {
     });
 
     let context = Context::new(&z3_cfg());
-    let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg()));
+    let mut executor = SymbolicExecutor::new(&context);
     let mut diagnostics = vec![];
     let z3_res = transform_expr(&var, &context, &mut diagnostics, &mut executor);
 
@@ -93,7 +93,7 @@ fn string_hex_transform() {
     });
 
     let context = Context::new(&z3_cfg());
-    let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg()));
+    let mut executor = SymbolicExecutor::new(&context);
     let mut diagnostics = vec![];
     let z3_res = transform_expr(&string, &context, &mut diagnostics, &mut executor);
 
@@ -145,7 +145,7 @@ fn list_transform() {
     });
 
     let context = Context::new(&z3_cfg());
-    let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg()));
+    let mut executor = SymbolicExecutor::new(&context);
     let mut diagnostics = vec![];
     let z3_res = transform_expr(&list, &context, &mut diagnostics, &mut executor);
 
@@ -234,7 +234,7 @@ fn in_transform() {
     });
 
     let context = Context::new(&z3_cfg());
-    let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg()));
+    let mut executor = SymbolicExecutor::new(&context);
     let mut diagnostics = vec![];
 
     // verify that `30` is in the list.