Add basic solc model checker options (gakonst#1258)

* Add basic solc model checker options * Changelog entry * review 1 * chore: fmt Co-authored-by: Georgios Konstantopoulos <[email protected]>
joleeee · May 13, 2022 · eb94e53 · eb94e53
1 parent b21d7b2
commit eb94e53
Show file tree

Hide file tree

Showing 4 changed files with 140 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -121,6 +121,8 @@
   `enum BytecodeObject` [#656](https://github.com/gakonst/ethers-rs/pull/656).
 - Nit: remove accidentally doubled double-quotes in an error message
 - Fix when compiler-out metadata is empty and there's no internalType [#1182](https://github.com/gakonst/ethers-rs/pull/1182)
+- Add basic `solc` model checker options.
+  [#1258](https://github.com/gakonst/ethers-rs/pull/1258)
 
 ### 0.6.0
 

diff --git a/ethers-solc/src/artifacts/mod.rs b/ethers-solc/src/artifacts/mod.rs
@@ -123,6 +123,9 @@ impl CompilerInput {
                 // <https://github.com/ethereum/solidity/releases/tag/v0.8.10>
                 debug.debug_info.clear();
             }
+
+            // 0.8.10 is the earliest version that has all model checker options.
+            self.settings.model_checker = None;
         }
 
         self
@@ -241,6 +244,9 @@ pub struct Settings {
     #[serde(default, skip_serializing_if = "Vec::is_empty")]
     pub remappings: Vec<Remapping>,
     pub optimizer: Optimizer,
+    /// Model Checker options.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub model_checker: Option<ModelCheckerSettings>,
     /// Metadata settings
     #[serde(default, skip_serializing_if = "Option::is_none")]
     pub metadata: Option<SettingsMetadata>,
@@ -386,6 +392,7 @@ impl Default for Settings {
             debug: None,
             libraries: Default::default(),
             remappings: Default::default(),
+            model_checker: None,
         }
         .with_ast()
     }
@@ -837,6 +844,112 @@ pub struct MetadataSource {
     pub license: Option<String>,
 }
 
+/// Model checker settings for solc
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
+pub struct ModelCheckerSettings {
+    #[serde(default, skip_serializing_if = "BTreeMap::is_empty")]
+    pub contracts: BTreeMap<String, Vec<String>>,
+    #[serde(
+        default,
+        with = "serde_helpers::display_from_str_opt",
+        skip_serializing_if = "Option::is_none"
+    )]
+    pub engine: Option<ModelCheckerEngine>,
+    #[serde(skip_serializing_if = "Option::is_none")]
+    pub timeout: Option<u32>,
+    #[serde(skip_serializing_if = "Option::is_none")]
+    pub targets: Option<Vec<ModelCheckerTarget>>,
+}
+
+/// Which model checker engine to run.
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
+pub enum ModelCheckerEngine {
+    Default,
+    All,
+    BMC,
+    CHC,
+}
+
+impl fmt::Display for ModelCheckerEngine {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let string = match self {
+            ModelCheckerEngine::Default => "none",
+            ModelCheckerEngine::All => "all",
+            ModelCheckerEngine::BMC => "bmc",
+            ModelCheckerEngine::CHC => "chc",
+        };
+        write!(f, "{}", string)
+    }
+}
+
+impl FromStr for ModelCheckerEngine {
+    type Err = String;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        match s {
+            "none" => Ok(ModelCheckerEngine::Default),
+            "all" => Ok(ModelCheckerEngine::All),
+            "bmc" => Ok(ModelCheckerEngine::BMC),
+            "chc" => Ok(ModelCheckerEngine::CHC),
+            s => Err(format!("Unknown model checker engine: {}", s)),
+        }
+    }
+}
+
+impl Default for ModelCheckerEngine {
+    fn default() -> Self {
+        ModelCheckerEngine::Default
+    }
+}
+
+/// Which model checker targets to check.
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub enum ModelCheckerTarget {
+    Assert,
+    Underflow,
+    Overflow,
+    DivByZero,
+    ConstantCondition,
+    PopEmptyArray,
+    OutOfBounds,
+    Balance,
+}
+
+impl fmt::Display for ModelCheckerTarget {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let string = match self {
+            ModelCheckerTarget::Assert => "assert",
+            ModelCheckerTarget::Underflow => "underflow",
+            ModelCheckerTarget::Overflow => "overflow",
+            ModelCheckerTarget::DivByZero => "divByZero",
+            ModelCheckerTarget::ConstantCondition => "constantCondition",
+            ModelCheckerTarget::PopEmptyArray => "popEmptyArray",
+            ModelCheckerTarget::OutOfBounds => "outOfBounds",
+            ModelCheckerTarget::Balance => "balance",
+        };
+        write!(f, "{}", string)
+    }
+}
+
+impl FromStr for ModelCheckerTarget {
+    type Err = String;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        match s {
+            "assert" => Ok(ModelCheckerTarget::Assert),
+            "underflow" => Ok(ModelCheckerTarget::Underflow),
+            "overflow" => Ok(ModelCheckerTarget::Overflow),
+            "divByZero" => Ok(ModelCheckerTarget::DivByZero),
+            "constantCondition" => Ok(ModelCheckerTarget::ConstantCondition),
+            "popEmptyArray" => Ok(ModelCheckerTarget::PopEmptyArray),
+            "outOfBounds" => Ok(ModelCheckerTarget::OutOfBounds),
+            "balance" => Ok(ModelCheckerTarget::Balance),
+            s => Err(format!("Unknown model checker target: {}", s)),
+        }
+    }
+}
+
 #[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
 pub struct Compiler {
     pub version: String,

diff --git a/ethers-solc/test-data/model-checker-sample/Assert.sol b/ethers-solc/test-data/model-checker-sample/Assert.sol
@@ -0,0 +1,5 @@
+contract Assert {
+	function f(uint x) public pure {
+		assert(x > 0);
+	}
+}
diff --git a/ethers-solc/tests/project.rs b/ethers-solc/tests/project.rs
@@ -9,7 +9,7 @@ use std::{
 
 use ethers_core::types::Address;
 use ethers_solc::{
-    artifacts::{BytecodeHash, Libraries},
+    artifacts::{BytecodeHash, Libraries, ModelCheckerEngine::CHC, ModelCheckerSettings},
     cache::{SolFilesCache, SOLIDITY_FILES_CACHE_FILENAME},
     project_util::*,
     remappings::Remapping,
@@ -1310,3 +1310,22 @@ fn can_compile_std_json_input() {
         assert!(out.sources.contains_key("lib/ds-test/src/test.sol"));
     }
 }
+
+#[test]
+fn can_compile_model_checker_sample() {
+    let root = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("test-data/model-checker-sample");
+    let paths = ProjectPathsConfig::builder().sources(root);
+
+    let mut project = TempProject::<ConfigurableArtifacts>::new(paths).unwrap();
+    project.project_mut().solc_config.settings.model_checker = Some(ModelCheckerSettings {
+        contracts: BTreeMap::new(),
+        engine: Some(CHC),
+        targets: None,
+        timeout: Some(10000),
+    });
+    let compiled = project.compile().unwrap();
+
+    assert!(compiled.find("Assert").is_some());
+    assert!(!compiled.has_compiler_errors());
+    assert!(compiled.has_compiler_warnings());
+}