Skip to content

Commit 6129e7f

Browse files
committed
fv crate
1 parent 2097ec5 commit 6129e7f

File tree

26 files changed

+1092
-57
lines changed

26 files changed

+1092
-57
lines changed

.github/workflows/expensive.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,10 +29,10 @@ jobs:
2929
uses: Swatinem/rust-cache@v1
3030

3131
- name: Build
32-
run: cargo test --workspace --all-features --no-run --locked -- --ignored
32+
run: cargo test --workspace --features solc-backend --no-run --locked -- --ignored
3333
- name: Run expensive tests
3434
id: expensive_tests
35-
run: cargo test --workspace --all-features --verbose -- --ignored
35+
run: cargo test --workspace --features solc-backend --verbose -- --ignored
3636
- name: Report
3737
if: failure() && steps.expensive_tests.outcome == 'failure'
3838
run: |

.github/workflows/main.yml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -121,9 +121,9 @@ jobs:
121121
- name: Cache Dependencies
122122
uses: Swatinem/rust-cache@v1
123123
- name: Build
124-
run: cargo test --workspace --all-features --no-run --locked
124+
run: cargo test --workspace --features solc-backend --no-run --locked
125125
- name: Run tests
126-
run: cargo test --workspace --all-features --verbose
126+
run: cargo test --workspace --features solc-backend --verbose
127127

128128
wasm-test:
129129
runs-on: ubuntu-latest
@@ -179,7 +179,7 @@ jobs:
179179
toolchain: stable
180180
override: true
181181
- name: Build
182-
run: cargo build --all-features --release && strip target/release/fe && mv target/release/fe target/release/${{ matrix.BIN_FILE }}
182+
run: cargo build --features solc-backend --release && strip target/release/fe && mv target/release/fe target/release/${{ matrix.BIN_FILE }}
183183
- name: Release
184184
uses: softprops/action-gh-release@v1
185185
with:

Cargo.lock

Lines changed: 9 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -73,11 +73,11 @@ docker-wasm-test:
7373

7474
.PHONY: coverage
7575
coverage:
76-
cargo tarpaulin --workspace --all-features --verbose --timeout 120 --exclude-files 'tests/*' --exclude-files 'main.rs' --out xml html -- --skip differential::
76+
cargo tarpaulin --workspace --features solc-backend --verbose --timeout 120 --exclude-files 'tests/*' --exclude-files 'main.rs' --out xml html -- --skip differential::
7777

7878
.PHONY: clippy
7979
clippy:
80-
cargo clippy --workspace --all-targets --all-features -- -D warnings -A clippy::upper-case-acronyms -A clippy::large-enum-variant -W clippy::redundant_closure_for_method_calls
80+
cargo clippy --workspace --all-targets --features solc-backend -- -D warnings -A clippy::upper-case-acronyms -A clippy::large-enum-variant -W clippy::redundant_closure_for_method_calls
8181

8282
.PHONY: rustfmt
8383
rustfmt:

crates/driver/src/lib.rs

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ pub struct CompiledContract {
3030
pub yul: String,
3131
#[cfg(feature = "solc-backend")]
3232
pub bytecode: String,
33+
#[cfg(feature = "solc-backend")]
34+
pub runtime_bytecode: String,
3335
}
3436

3537
#[derive(Debug)]
@@ -128,6 +130,15 @@ fn compile_module_id(
128130
IndexMap::new()
129131
};
130132

133+
// compile runtimes to yul
134+
let yul_contract_runtimes = fe_yulgen::compile_runtimes(db, lowered_module_id);
135+
136+
let _bytecode_contract_runtimes = if _with_bytecode {
137+
compile_yul_runtimes(yul_contract_runtimes.iter(), _optimize)
138+
} else {
139+
IndexMap::new()
140+
};
141+
131142
// combine all of the named contract maps
132143
let contracts = json_abis
133144
.keys()
@@ -143,6 +154,12 @@ fn compile_module_id(
143154
} else {
144155
"".to_string()
145156
},
157+
#[cfg(feature = "solc-backend")]
158+
runtime_bytecode: if _with_bytecode {
159+
_bytecode_contract_runtimes[name].to_owned()
160+
} else {
161+
"".to_string()
162+
},
146163
},
147164
)
148165
})
@@ -185,3 +202,34 @@ fn compile_yul(
185202
#[cfg(not(feature = "solc-backend"))]
186203
IndexMap::new()
187204
}
205+
206+
fn compile_yul_runtimes(
207+
_contracts: impl Iterator<Item = (impl AsRef<str>, impl AsRef<str>)>,
208+
_optimize: bool,
209+
) -> IndexMap<String, String> {
210+
#[cfg(feature = "solc-backend")]
211+
{
212+
match fe_yulc::compile_runtimes(_contracts, _optimize) {
213+
Err(error) => {
214+
for error in serde_json::from_str::<Value>(&error.0)
215+
.expect("unable to deserialize json output")["errors"]
216+
.as_array()
217+
.expect("errors not an array")
218+
{
219+
eprintln!(
220+
"Error: {}",
221+
error["formattedMessage"]
222+
.as_str()
223+
.expect("error value not a string")
224+
.replace("\\\n", "\n")
225+
)
226+
}
227+
panic!("Yul compilation failed with the above errors")
228+
}
229+
Ok(contracts) => contracts,
230+
}
231+
}
232+
233+
#[cfg(not(feature = "solc-backend"))]
234+
IndexMap::new()
235+
}

crates/fe/src/main.rs

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ arg_enum! {
2222
Ast,
2323
LoweredAst,
2424
Bytecode,
25+
RuntimeBytecode,
2526
Tokens,
2627
Yul,
2728
}
@@ -52,7 +53,15 @@ pub fn main() {
5253
.short("e")
5354
.long("emit")
5455
.help("Comma separated compile targets e.g. -e=bytecode,yul")
55-
.possible_values(&["abi", "bytecode", "ast", "tokens", "yul", "loweredAst"])
56+
.possible_values(&[
57+
"abi",
58+
"bytecode",
59+
"runtimeBytecode",
60+
"ast",
61+
"tokens",
62+
"yul",
63+
"loweredAst",
64+
])
5665
.default_value("abi,bytecode")
5766
.use_delimiter(true)
5867
.takes_value(true),
@@ -240,6 +249,15 @@ fn write_compiled_module(
240249
let file_name = format!("{}.bin", &name);
241250
write_output(&contract_output_dir.join(file_name), &contract.bytecode)?;
242251
}
252+
253+
#[cfg(feature = "solc-backend")]
254+
if targets.contains(&CompilationTarget::RuntimeBytecode) {
255+
let file_name = format!("{}.runtime.bin", &name);
256+
write_output(
257+
&contract_output_dir.join(file_name),
258+
&contract.runtime_bytecode,
259+
)?;
260+
}
243261
}
244262

245263
Ok(())

crates/fv/Cargo.toml

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
[package]
2+
authors = ["The Fe Developers <snakecharmers@ethereum.org>"]
3+
categories = ["cryptography::cryptocurrencies", "command-line-utilities", "development-tools"]
4+
description = "Fe formal verification utilities"
5+
edition = "2021"
6+
keywords = ["ethereum", "fe", "yul", "smart", "contract", "compiler"]
7+
license = "GPL-3.0-or-later"
8+
name = "fv"
9+
readme = "README.md"
10+
repository = "https://github.com/ethereum/fe"
11+
version = "0.14.0-alpha"
12+
13+
[features]
14+
solc-backend = ["fe-driver/solc-backend"]
15+
kevm-backend = []
16+
17+
[dependencies]
18+
fe-driver = {path = "../driver", version = "^0.14.0-alpha"}
19+
fe-yulgen = {path = "../yulgen", version = "^0.14.0-alpha"}
20+
fe-test-files = {path = "../test-files", version = "^0.14.0-alpha"}

crates/fv/README.md

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
This crate contains utilities for building and running kevm specs. A system installation of [evm-semantics](https://github.com/kframework/evm-semantics) is required to run the specs.
2+
3+
Once the evm-semantics project has been built, set the `KEVM_PATH` environment variable.
4+
5+
e.g. `$ export KEVM_PATH=/path/to/evm-semantics`
6+
7+
and then run the tests: `$ cargo test --features "solc-backend, kevm-backend"`.

crates/fv/src/lib.rs

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
#![cfg(feature = "kevm-backend")]
2+
use fe_yulgen::Db;
3+
use std::path::Path;
4+
use std::process::Command;
5+
use std::{env, fs};
6+
7+
const SPECS_DIR: &str = "tests/specs/fe/";
8+
9+
pub fn kevm_path() -> String {
10+
env::var("KEVM_PATH").expect("`KEVM_PATH` not set")
11+
}
12+
13+
pub fn run_spec(name: &str, src_path: &str, src: &str, spec: &str) -> Result<(), String> {
14+
let kevm_path = kevm_path();
15+
16+
let spec = build_spec(name, src_path, src, spec);
17+
let spec_path = Path::new(&kevm_path)
18+
.join(SPECS_DIR)
19+
.join(name)
20+
.with_extension("k");
21+
fs::write(spec_path.clone(), spec).expect("unable to write file");
22+
23+
let path = env::var("PATH").expect("PATH is not set");
24+
25+
let out = Command::new("kevm")
26+
.arg("prove")
27+
.arg(spec_path.to_str().unwrap())
28+
.arg("--backend")
29+
.arg("haskell")
30+
.arg("--format-failures")
31+
// we should define out own verification module
32+
.arg("--directory")
33+
.arg("tests/specs/erc20/verification/haskell")
34+
.env("PATH", format!(".build/usr/bin:{}", path))
35+
.current_dir(&kevm_path)
36+
.output()
37+
.expect("failed to execute process");
38+
39+
if out.status.code() != Some(0) {
40+
Err(format!(
41+
"{}\n{}",
42+
String::from_utf8_lossy(&out.stderr),
43+
String::from_utf8_lossy(&out.stdout)
44+
))
45+
} else {
46+
Ok(())
47+
}
48+
}
49+
50+
pub fn build_spec(name: &str, src_path: &str, src: &str, spec: &str) -> String {
51+
let mut db = Db::default();
52+
let module = fe_driver::compile_single_file(&mut db, src_path, src, true, true).unwrap();
53+
54+
// replace placeholders
55+
let mut new_spec = spec.to_owned().replace("$TEST_NAME", &name.to_uppercase());
56+
for (name, contract) in module.contracts.iter() {
57+
new_spec = new_spec.replace(
58+
&format!("${}::RUNTIME", name),
59+
&format!("\"0x{}\"", contract.runtime_bytecode),
60+
)
61+
}
62+
63+
new_spec
64+
}

crates/fv/tests/specs.rs

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
#![cfg(feature = "kevm-backend")]
2+
3+
/// Checks if a contract spec is valid.
4+
macro_rules! test_spec {
5+
($name:ident, $src_path:expr, $spec_path:expr) => {
6+
#[test]
7+
fn $name() {
8+
let src = fe_test_files::fixture(concat!("kspecs/", $src_path));
9+
let spec = fe_test_files::fixture(concat!("kspecs/", $spec_path));
10+
11+
if let Err(output) =
12+
fv::run_spec(&stringify!($name).replace("_", "-"), $src_path, &src, &spec)
13+
{
14+
panic!("{}", output)
15+
}
16+
}
17+
};
18+
}
19+
20+
/// Checks if a contract spec is invalid.
21+
macro_rules! test_spec_invalid {
22+
($name:ident, $src_path:expr, $spec_path:expr) => {
23+
#[test]
24+
fn $name() {
25+
let src = fe_test_files::fixture(concat!("kspecs/", $src_path));
26+
let spec = fe_test_files::fixture(concat!("kspecs/", $spec_path));
27+
28+
match fv::run_spec(&stringify!($name).replace("_", "-"), $src_path, &src, &spec) {
29+
Ok(()) => panic!("spec is valid"),
30+
Err(output) => {
31+
// we want to make sure it didn't fail for some other reason
32+
if !output.contains("the claimed implication is not valid") {
33+
panic!("spec claim was not checked {}", output)
34+
}
35+
}
36+
}
37+
}
38+
};
39+
}
40+
41+
test_spec! { sanity_returns_42, "sanity/foo.fe", "sanity/returns_42.k" }
42+
test_spec! { sanity_returns_in, "sanity/foo.fe", "sanity/returns_in.k" }
43+
test_spec! { sanity_returns_in_cond1, "sanity/foo.fe", "sanity/returns_in_cond1.k" }
44+
test_spec! { sanity_returns_in_cond2, "sanity/foo.fe", "sanity/returns_in_cond2.k" }
45+
46+
// these are just for extra sanity
47+
test_spec_invalid! { sanity_returns_42_invalid, "sanity/foo.fe", "sanity/returns_42_invalid.k" }
48+
test_spec_invalid! { sanity_returns_in_invalid, "sanity/foo.fe", "sanity/returns_in_invalid.k" }
49+
test_spec_invalid! { sanity_returns_in_cond2_invalid, "sanity/foo.fe", "sanity/returns_in_cond2_invalid.k" }

0 commit comments

Comments
 (0)