Repository: gakonst/ethers-rs
Pull request #2123 (2023-02-08 08:02:28)

feat(ethers-solc): extend model checker setting field
## Motivation

- extend model checker setting's field to open `invariants` flag.
- [invariants docs](https://docs.soliditylang.org/en/v0.8.18/smtchecker.html#reported-inferred-inductive-invariants) 

## PR Checklist

-   [ ] Added Tests
-   [ ] Added Documentation
-   [ ] Updated the changelog
-   [ ] Breaking changes


wiasliaw: @mattsse 
Found in [0.8.10](https://blog.soliditylang.org/2021/11/09/solidity-0.8.10-release-announcement/).

Patch:
diff --git a/Cargo.lock b/Cargo.lock
index 2fee682e..e1ffa773 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -4027,9 +4027,9 @@ dependencies = [
 
 [[package]]
 name = "solang-parser"
-version = "0.2.1"
+version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6e9653f278d9531b60f042c29732bb835d519943f4167b1e5684c7e820dd9fec"
+checksum = "58feb14d4002859db0b744b0915840bae403b8a5675efded3e8adddb6beb85b2"
 dependencies = [
  "itertools",
  "lalrpop",
diff --git a/ethers-contract/ethers-contract-abigen/src/contract/common.rs b/ethers-contract/ethers-contract-abigen/src/contract/common.rs
index c48e306d..b53b08d6 100644
--- a/ethers-contract/ethers-contract-abigen/src/contract/common.rs
+++ b/ethers-contract/ethers-contract-abigen/src/contract/common.rs
@@ -62,7 +62,7 @@ where
 }
 
 pub(crate) fn imports(name: &str) -> TokenStream {
-    let doc_str = format!("{name} was auto-generated with ethers-rs Abigen. More information at: https://github.com/gakonst/ethers-rs");
+    let doc_str = format!("{name} was auto-generated with ethers-rs Abigen. More information at: <https://github.com/gakonst/ethers-rs>");
 
     let ethers_core = ethers_core_crate();
     let ethers_providers = ethers_providers_crate();
diff --git a/ethers-contract/ethers-contract-abigen/src/contract/structs.rs b/ethers-contract/ethers-contract-abigen/src/contract/structs.rs
index 4002e7b6..b2b3dbeb 100644
--- a/ethers-contract/ethers-contract-abigen/src/contract/structs.rs
+++ b/ethers-contract/ethers-contract-abigen/src/contract/structs.rs
@@ -596,7 +596,7 @@ fn struct_type_projections(name: &str) -> Vec<String> {
 fn expand_struct_type(struct_ty: &StructFieldType) -> TokenStream {
     match struct_ty {
         StructFieldType::Type(ty) => {
-            let ty = util::ident(ty.name());
+            let ty = util::ident(&ty.name().to_pascal_case());
             quote! {#ty}
         }
         StructFieldType::Array(ty) => {
diff --git a/ethers-middleware/src/transformer/ds_proxy/factory.rs b/ethers-middleware/src/transformer/ds_proxy/factory.rs
index 122c7bf1..71d35043 100644
--- a/ethers-middleware/src/transformer/ds_proxy/factory.rs
+++ b/ethers-middleware/src/transformer/ds_proxy/factory.rs
@@ -42,7 +42,7 @@ mod dsproxyfactory_mod {
         types::*,
     };
     use ethers_providers::Middleware;
-    #[doc = "DsProxyFactory was auto-generated with ethers-rs Abigen. More information at: https://github.com/gakonst/ethers-rs"]
+    #[doc = "DsProxyFactory was auto-generated with ethers-rs Abigen. More information at: <https://github.com/gakonst/ethers-rs>"]
     use std::sync::Arc;
 
     pub static DSPROXYFACTORY_ABI: Lazy<Abi> = Lazy::new(|| {
diff --git a/ethers-solc/Cargo.toml b/ethers-solc/Cargo.toml
index 7b432680..3530f53c 100644
--- a/ethers-solc/Cargo.toml
+++ b/ethers-solc/Cargo.toml
@@ -37,7 +37,7 @@ tempfile = { version = "3.3.0", optional = true }
 fs_extra = { version = "1.3.0", optional = true }
 sha2 = { version = "0.10.6", default-features = false, optional = true }
 dunce = "1.0.3"
-solang-parser = { default-features = false, version = "=0.2.1" }
+solang-parser = { default-features = false, version = "=0.2.2" }
 rayon = "1.6.0"
 rand = { version = "0.8.5", optional = true }
 path-slash = "0.2.1"
diff --git a/ethers-solc/src/artifacts/mod.rs b/ethers-solc/src/artifacts/mod.rs
index 94806f9c..a90b0962 100644
--- a/ethers-solc/src/artifacts/mod.rs
+++ b/ethers-solc/src/artifacts/mod.rs
@@ -1018,6 +1018,8 @@ pub struct ModelCheckerSettings {
     pub timeout: Option<u32>,
     #[serde(skip_serializing_if = "Option::is_none")]
     pub targets: Option<Vec<ModelCheckerTarget>>,
+    #[serde(skip_serializing_if = "Option::is_none")]
+    pub invariants: Option<Vec<ModelCheckerInvariant>>,
 }
 
 /// Which model checker engine to run.
@@ -1104,6 +1106,36 @@ impl FromStr for ModelCheckerTarget {
     }
 }
 
+/// Which model checker invariants to check.
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub enum ModelCheckerInvariant {
+    Contract,
+    Reentrancy,
+}
+
+impl fmt::Display for ModelCheckerInvariant {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let string = match self {
+            ModelCheckerInvariant::Contract => "contract",
+            ModelCheckerInvariant::Reentrancy => "reentrancy",
+        };
+        write!(f, "{string}")
+    }
+}
+
+impl FromStr for ModelCheckerInvariant {
+    type Err = String;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        match s {
+            "contract" => Ok(ModelCheckerInvariant::Contract),
+            "reentrancy" => Ok(ModelCheckerInvariant::Reentrancy),
+            s => Err(format!("Unknown model checker invariant: {s}")),
+        }
+    }
+}
+
 #[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
 pub struct Compiler {
     pub version: String,
diff --git a/ethers-solc/src/resolver/mod.rs b/ethers-solc/src/resolver/mod.rs
index 732b5d1a..08b1b0f1 100644
--- a/ethers-solc/src/resolver/mod.rs
+++ b/ethers-solc/src/resolver/mod.rs
@@ -455,17 +455,20 @@ impl Graph {
             all_nodes: &mut HashMap<usize, (PathBuf, Source)>,
             sources: &mut Sources,
             edges: &[Vec<usize>],
-            num_input_files: usize,
+            processed_sources: &mut HashSet<usize>,
         ) {
+            // iterate over all dependencies not processed yet
             for dep in edges[idx].iter().copied() {
-                // we only process nodes that were added as part of the resolve step because input
-                // nodes are handled separately
-                if dep >= num_input_files {
-                    // library import
-                    if let Some((path, source)) = all_nodes.remove(&dep) {
-                        sources.insert(path, source);
-                        insert_imports(dep, all_nodes, sources, edges, num_input_files);
-                    }
+                // keep track of processed dependencies, if the dep was already in the set we have
+                // processed it already
+                if !processed_sources.insert(dep) {
+                    continue
+                }
+
+                // library import
+                if let Some((path, source)) = all_nodes.get(&dep).cloned() {
+                    sources.insert(path, source);
+                    insert_imports(dep, all_nodes, sources, edges, processed_sources);
                 }
             }
         }
@@ -480,17 +483,21 @@ impl Graph {
         // determine the `Sources` set for each solc version
         for (version, input_node_indices) in versioned_nodes {
             let mut sources = Sources::new();
+
+            // all input nodes will be processed
+            let mut processed_sources = input_node_indices.iter().copied().collect();
+
             // we only process input nodes (from sources, tests for example)
             for idx in input_node_indices {
                 // insert the input node in the sources set and remove it from the available set
-                let (path, source) = all_nodes.remove(&idx).expect("node is preset. qed");
+                let (path, source) = all_nodes.get(&idx).cloned().expect("node is preset. qed");
                 sources.insert(path, source);
                 insert_imports(
                     idx,
                     &mut all_nodes,
                     &mut sources,
                     &edges.edges,
-                    edges.num_input_files,
+                    &mut processed_sources,
                 );
             }
             versioned_sources.insert(version, sources);


Test patch:
diff --git a/ethers-solc/tests/project.rs b/ethers-solc/tests/project.rs
index 45aa9079..3cc8c97e 100644
--- a/ethers-solc/tests/project.rs
+++ b/ethers-solc/tests/project.rs
@@ -1610,6 +1610,7 @@ fn can_compile_model_checker_sample() {
         engine: Some(CHC),
         targets: None,
         timeout: Some(10000),
+        invariants: None,
     });
     let compiled = project.compile().unwrap();
 
@@ -1860,7 +1861,7 @@ fn can_parse_doc() {
 
     let contract = r#"
 // SPDX-License-Identifier: GPL-3.0-only
-pragma solidity ^0.8.0;
+pragma solidity 0.8.17;
 
 /// @title Not an ERC20.
 /// @author Notadev