extend model checker options (#2147)

* refactor(ethers-solc): reorder the sanitized

* feat(ethers-solc): feat divModWithSlacks, showUnproved and solvers

ethers-solc/src/artifacts/mod.rs

@@ -106,10 +106,12 @@ impl CompilerInput {
     pub fn sanitized(mut self, version: &Version) -> Self {
         static PRE_V0_6_0: once_cell::sync::Lazy<VersionReq> =
             once_cell::sync::Lazy::new(|| VersionReq::parse("<0.6.0").unwrap());
-        static PRE_V0_8_10: once_cell::sync::Lazy<VersionReq> =
-            once_cell::sync::Lazy::new(|| VersionReq::parse("<0.8.10").unwrap());
         static PRE_V0_7_5: once_cell::sync::Lazy<VersionReq> =
             once_cell::sync::Lazy::new(|| VersionReq::parse("<0.7.5").unwrap());
+        static PRE_V0_8_7: once_cell::sync::Lazy<VersionReq> =
+            once_cell::sync::Lazy::new(|| VersionReq::parse("<0.8.7").unwrap());
+        static PRE_V0_8_10: once_cell::sync::Lazy<VersionReq> =
+            once_cell::sync::Lazy::new(|| VersionReq::parse("<0.8.10").unwrap());
         static PRE_V0_8_18: once_cell::sync::Lazy<VersionReq> =
             once_cell::sync::Lazy::new(|| VersionReq::parse("<0.8.18").unwrap());
 
@@ -123,6 +125,18 @@ impl CompilerInput {
             let _ = self.settings.debug.take();
         }
 
+        if PRE_V0_7_5.matches(version) {
+            // introduced in 0.7.5 <https://github.com/ethereum/solidity/releases/tag/v0.7.5>
+            self.settings.via_ir.take();
+        }
+
+        if PRE_V0_8_7.matches(version) {
+            // lower the disable version from 0.8.10 to 0.8.7, due to `divModNoSlacks`,
+            // `showUnproved` and `solvers` are implemented
+            // introduced in <https://github.com/ethereum/solidity/releases/tag/v0.8.7>
+            self.settings.model_checker = None;
+        }
+
         if PRE_V0_8_10.matches(version) {
             if let Some(ref mut debug) = self.settings.debug {
                 // introduced in <https://docs.soliditylang.org/en/v0.8.10/using-the-compiler.html#compiler-api>
@@ -130,13 +144,10 @@ impl CompilerInput {
                 debug.debug_info.clear();
             }
 
-            // 0.8.10 is the earliest version that has all model checker options.
+            if let Some(ref mut model_checker) = self.settings.model_checker {
-            self.settings.model_checker = None;
+                // introduced in <https://github.com/ethereum/solidity/releases/tag/v0.8.10>
-        }
+                model_checker.invariants = None;
-
+            }
-        if PRE_V0_7_5.matches(version) {
-            // introduced in 0.7.5 <https://github.com/ethereum/solidity/releases/tag/v0.7.5>
-            self.settings.via_ir.take();
         }
 
         if PRE_V0_8_18.matches(version) {
@@ -144,6 +155,13 @@ impl CompilerInput {
             if let Some(ref mut meta) = self.settings.metadata {
                 meta.cbor_metadata = None;
             }
+
+            if let Some(ref mut model_checker) = self.settings.model_checker {
+                if let Some(ref mut solvers) = model_checker.solvers {
+                    // elf solver introduced in 0.8.18 <https://github.com/ethereum/solidity/releases/tag/v0.8.18>
+                    solvers.retain(|solver| *solver != ModelCheckerSolver::Eld);
+                }
+            }
         }
 
         self
@@ -1021,6 +1039,12 @@ pub struct ModelCheckerSettings {
     pub targets: Option<Vec<ModelCheckerTarget>>,
     #[serde(skip_serializing_if = "Option::is_none")]
     pub invariants: Option<Vec<ModelCheckerInvariant>>,
+    #[serde(rename = "showUnproved", skip_serializing_if = "Option::is_none")]
+    pub show_unproved: Option<bool>,
+    #[serde(rename = "divModWithSlacks", skip_serializing_if = "Option::is_none")]
+    pub div_mod_with_slacks: Option<bool>,
+    #[serde(skip_serializing_if = "Option::is_none")]
+    pub solvers: Option<Vec<ModelCheckerSolver>>,
 }
 
 /// Which model checker engine to run.
@@ -1137,6 +1161,42 @@ impl FromStr for ModelCheckerInvariant {
     }
 }
 
+/// Which model checker solvers to check.
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub enum ModelCheckerSolver {
+    Cvc4,
+    Eld,
+    Smtlib2,
+    Z3,
+}
+
+impl fmt::Display for ModelCheckerSolver {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let string = match self {
+            ModelCheckerSolver::Cvc4 => "cvc4",
+            ModelCheckerSolver::Eld => "eld",
+            ModelCheckerSolver::Smtlib2 => "smtlib2",
+            ModelCheckerSolver::Z3 => "z3",
+        };
+        write!(f, "{string}")
+    }
+}
+
+impl FromStr for ModelCheckerSolver {
+    type Err = String;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        match s {
+            "cvc4" => Ok(ModelCheckerSolver::Cvc4),
+            "eld" => Ok(ModelCheckerSolver::Cvc4),
+            "smtlib2" => Ok(ModelCheckerSolver::Smtlib2),
+            "z3" => Ok(ModelCheckerSolver::Z3),
+            s => Err(format!("Unknown model checker invariant: {s}")),
+        }
+    }
+}
+
 #[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
 pub struct Compiler {
     pub version: String,

ethers-solc/tests/project.rs

@@ -1610,6 +1610,9 @@ fn can_compile_model_checker_sample() {
         engine: Some(CHC),
         targets: None,
         timeout: Some(10000),
+        show_unproved: None,
+        div_mod_with_slacks: None,
+        solvers: None,
         invariants: None,
     });
     let compiled = project.compile().unwrap();