From eb94e53d1f87dc5fe10f25b7268e977cfad24984 Mon Sep 17 00:00:00 2001 From: Leo Date: Fri, 13 May 2022 22:29:13 +0200 Subject: [PATCH] Add basic solc model checker options (#1258) * Add basic solc model checker options * Changelog entry * review 1 * chore: fmt Co-authored-by: Georgios Konstantopoulos --- CHANGELOG.md | 2 + ethers-solc/src/artifacts/mod.rs | 113 ++++++++++++++++++ .../test-data/model-checker-sample/Assert.sol | 5 + ethers-solc/tests/project.rs | 21 +++- 4 files changed, 140 insertions(+), 1 deletion(-) create mode 100644 ethers-solc/test-data/model-checker-sample/Assert.sol diff --git a/CHANGELOG.md b/CHANGELOG.md index 853c8d1e..bfe4d21b 100644 --- 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 index 3001716d..497e008a 100644 --- a/ethers-solc/src/artifacts/mod.rs +++ b/ethers-solc/src/artifacts/mod.rs @@ -123,6 +123,9 @@ impl CompilerInput { // 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, pub optimizer: Optimizer, + /// Model Checker options. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub model_checker: Option, /// Metadata settings #[serde(default, skip_serializing_if = "Option::is_none")] pub metadata: Option, @@ -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, } +/// 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>, + #[serde( + default, + with = "serde_helpers::display_from_str_opt", + skip_serializing_if = "Option::is_none" + )] + pub engine: Option, + #[serde(skip_serializing_if = "Option::is_none")] + pub timeout: Option, + #[serde(skip_serializing_if = "Option::is_none")] + pub targets: Option>, +} + +/// 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 { + 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 { + 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 new file mode 100644 index 00000000..4d6656e0 --- /dev/null +++ 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 index 40f9aaa4..5bc568e7 100644 --- 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::::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()); +}