From 060e145ea2175d6709c533718b87e8788ceb6df9 Mon Sep 17 00:00:00 2001
From: "wiasliaw.eth" <wiasliaw@protonmail.com>
Date: Sat, 11 Feb 2023 03:51:01 +0800
Subject: [PATCH] feat(ethers-solc): extend model checker setting field (#2123)

---
 ethers-solc/src/artifacts/mod.rs | 32 ++++++++++++++++++++++++++++++++
 ethers-solc/tests/project.rs     |  1 +
 2 files changed, 33 insertions(+)

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/tests/project.rs b/ethers-solc/tests/project.rs
index 1b754273..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();