hacking

crates/analyzer/src/db.rs

@@ -110,6 +110,8 @@ pub trait AnalyzerDb: SourceDb + Upcast<dyn SourceDb> + UpcastMut<dyn SourceDb>
     fn module_submodules(&self, module: ModuleId) -> Rc<[ModuleId]>;
     #[salsa::invoke(queries::module::module_tests)]
     fn module_tests(&self, module: ModuleId) -> Vec<FunctionId>;
+    #[salsa::invoke(queries::module::module_invariants)]
+    fn module_invariants(&self, module: ModuleId) -> Vec<FunctionId>;
 
     // Module Constant
     #[salsa::cycle(queries::module::module_constant_type_cycle)]

crates/analyzer/src/db/queries/module.rs

@@ -760,3 +760,12 @@ pub fn module_tests(db: &dyn AnalyzerDb, ingot: ModuleId) -> Vec<FunctionId> {
         .filter(|function| function.is_test(db))
         .collect()
 }
+
+pub fn module_invariants(db: &dyn AnalyzerDb, ingot: ModuleId) -> Vec<FunctionId> {
+    ingot
+        .all_functions(db)
+        .iter()
+        .copied()
+        .filter(|function| function.is_invariant(db))
+        .collect()
+}

crates/analyzer/src/namespace/items.rs

@@ -555,6 +555,10 @@ impl ModuleId {
         db.module_tests(*self)
     }
 
+    pub fn invariants(&self, db: &dyn AnalyzerDb) -> Vec<FunctionId> {
+        db.module_invariants(*self)
+    }
+
     /// Returns `true` if the `item` is in scope of the module.
     pub fn is_in_scope(&self, db: &dyn AnalyzerDb, item: Item) -> bool {
         if let Some(val) = item.module(db) {
@@ -1351,6 +1355,13 @@ impl FunctionId {
             .iter()
             .any(|attribute| attribute.name(db) == "test")
     }
+
+    pub fn is_invariant(&self, db: &dyn AnalyzerDb) -> bool {
+        Item::Function(*self)
+            .attributes(db)
+            .iter()
+            .any(|attribute| attribute.name(db) == "invariant")
+    }
 }
 
 trait FunctionsAsItems {

crates/codegen/src/yul/isel/test.rs

@@ -22,7 +22,21 @@ pub fn lower_test(db: &dyn CodegenDb, test: FunctionId) -> yul::Object {
         .map(yul::Statement::FunctionDefinition)
         .collect();
     let test_func_name = identifier! { (db.codegen_function_symbol_name(test)) };
-    let call = function_call_statement! {[test_func_name]()};
+    let call_args = test
+        .signature(db.upcast())
+        .params
+        .iter()
+        .enumerate()
+        .filter_map(|(n, param)| {
+            if param.name == "ctx" {
+                None
+            } else {
+                let value = literal_expression! { (n * 32) };
+                Some(expression! { calldataload([value]) })
+            }
+        })
+        .collect::<Vec<_>>();
+    let call = function_call_statement! {[test_func_name]([call_args...])};
 
     let code = code! {
         [dep_functions...]

crates/codegen/src/yul/runtime/mod.rs

@@ -163,7 +163,8 @@ pub trait RuntimeProvider {
             expression! { signextend([significant], [value]) }
         } else {
             let mask = BitMask::new(from_size);
-            expression! { and([value], [mask.as_expr()]) }
+            // expression! { and([value], [mask.as_expr()]) }
+            value
         }
     }
 

crates/driver/Cargo.toml

@@ -20,6 +20,7 @@ fe-codegen = {path = "../codegen", version = "^0.22.0"}
 fe-parser = {path = "../parser", version = "^0.22.0"}
 fe-yulc = {path = "../yulc", version = "^0.22.0", features = ["solc-backend"], optional = true}
 fe-test-runner = {path = "../test-runner", version = "^0.22.0"}
+fe-specgen = {path = "../specgen", version = "^0.22.0"}
 indexmap = "1.6.2"
 vfs = "0.5.1"
 smol_str = "0.1.21"

crates/driver/src/lib.rs

@@ -7,6 +7,7 @@ use fe_common::db::Upcast;
 use fe_common::diagnostics::Diagnostic;
 use fe_common::files::FileKind;
 use fe_parser::ast::SmolStr;
+use fe_specgen::KSpec;
 use fe_test_runner::TestSink;
 use indexmap::{indexmap, IndexMap};
 use serde_json::Value;
@@ -86,6 +87,23 @@ pub fn compile_single_file_tests(
     }
 }
 
+#[cfg(feature = "solc-backend")]
+pub fn generate_single_file_specs(
+    db: &mut Db,
+    path: &str,
+    src: &str,
+    optimize: bool,
+) -> Result<Vec<KSpec>, CompileError> {
+    let module = ModuleId::new_standalone(db, path, src);
+    let diags = module.diagnostics(db);
+
+    if diags.is_empty() {
+        Ok(generate_module_specs(db, module, optimize))
+    } else {
+        Err(CompileError(diags))
+    }
+}
+
 // Run analysis with ingot
 // Return vector error,waring...
 pub fn check_ingot(
@@ -176,6 +194,46 @@ pub fn compile_ingot_tests(
     }
 }
 
+#[cfg(feature = "solc-backend")]
+pub fn generate_ingot_specs(
+    db: &mut Db,
+    name: &str,
+    files: &[(impl AsRef<str>, impl AsRef<str>)],
+    optimize: bool,
+) -> Result<Vec<KSpec>, CompileError> {
+    let std = IngotId::std_lib(db);
+    let ingot = IngotId::from_files(
+        db,
+        name,
+        IngotMode::Main,
+        FileKind::Local,
+        files,
+        indexmap! { "std".into() => std },
+    );
+
+    let mut diags = ingot.diagnostics(db);
+    ingot.sink_external_ingot_diagnostics(db, &mut diags);
+    if !diags.is_empty() {
+        return Err(CompileError(diags));
+    }
+
+    if diags.is_empty() {
+        // Ok(ingot
+        //     .all_modules(db)
+        //     .iter()
+        //     .fold(vec![], |mut accum, module| {
+        //         accum.push((
+        //             module.name(db),
+        //             generate_module_specs(db, *module, optimize),
+        //         ));
+        //         accum
+        //     }))
+        Ok(vec![])
+    } else {
+        Err(CompileError(diags))
+    }
+}
+
 /// Returns graphviz string.
 // TODO: This is temporary function for debugging.
 pub fn dump_mir_single_file(db: &mut Db, path: &str, src: &str) -> Result<String, CompileError> {
@@ -196,6 +254,7 @@ fn compile_test(db: &mut Db, test: FunctionId, optimize: bool) -> CompiledTest {
     let yul_test = fe_codegen::yul::isel::lower_test(db, test)
         .to_string()
         .replace('"', "\\\"");
+    // panic!("{}", yul_test);
     let bytecode = compile_to_evm("test", &yul_test, optimize);
     CompiledTest::new(test.name(db), bytecode)
 }
@@ -209,6 +268,21 @@ fn compile_module_tests(db: &mut Db, module_id: ModuleId, optimize: bool) -> Vec
         .collect()
 }
 
+#[cfg(feature = "solc-backend")]
+fn generate_spec(db: &mut Db, test: FunctionId, optimize: bool) -> KSpec {
+    let code = compile_test(db, test, optimize).bytecode;
+    KSpec::new(test.name(db), code, test.signature(db).params.len())
+}
+
+#[cfg(feature = "solc-backend")]
+fn generate_module_specs(db: &mut Db, module_id: ModuleId, optimize: bool) -> Vec<KSpec> {
+    module_id
+        .invariants(db)
+        .iter()
+        .map(|test| generate_spec(db, *test, optimize))
+        .collect()
+}
+
 #[cfg(feature = "solc-backend")]
 fn compile_module(
     db: &mut Db,

crates/fe/Cargo.toml

@@ -24,3 +24,4 @@ fe-test-runner = {path = "../test-runner", version = "^0.22.0"}
 fe-common = {path = "../common", version = "^0.22.0"}
 fe-driver = {path = "../driver", version = "^0.22.0"}
 fe-parser = {path = "../parser", version = "^0.22.0"}
+fe-specgen = {path = "../specgen", version = "^0.22.0"}

crates/fe/src/main.rs

@@ -30,5 +30,9 @@ fn main() {
         Commands::Test(arg) => {
             task::test(arg);
         }
+        #[cfg(feature = "solc-backend")]
+        Commands::Specs(arg) => {
+            task::specs(arg);
+        }
     }
 }

crates/fe/src/task/mod.rs

@@ -1,6 +1,7 @@
 mod build;
 mod check;
 mod new;
+mod specs;
 #[cfg(feature = "solc-backend")]
 mod test;
 mod utils;
@@ -9,6 +10,7 @@ pub use build::{build, BuildArgs};
 pub use check::{check, CheckArgs};
 use clap::Subcommand;
 pub use new::{create_new_project, NewProjectArgs};
+pub use specs::{specs, SpecsArgs};
 #[cfg(feature = "solc-backend")]
 pub use test::{test, TestArgs};
 
@@ -19,4 +21,5 @@ pub enum Commands {
     New(NewProjectArgs),
     #[cfg(feature = "solc-backend")]
     Test(TestArgs),
+    Specs(SpecsArgs),
 }