Skip to content

Commit

Permalink
[compiler v2] Stackless Bytecode Refactoring
Browse files Browse the repository at this point in the history
This is the 2nd step in the refactoring started in #9698.  This splits off prover specific parts from the crate `move-model/bytecode` into `move-prover/bytecode-pipeline`. Sharable dataflow analysis and transformation processors, like livevar and reaching definitions, stay. The tests have been split as well, and a common testing driver has been moved in its own test utility crate.

Github does not nicely show diffs like this, but this is functionally a no-op which only Moves code around.
  • Loading branch information
wrwg committed Aug 22, 2023
1 parent c84d1e2 commit 7350baf
Show file tree
Hide file tree
Showing 92 changed files with 951 additions and 5,879 deletions.
55 changes: 53 additions & 2 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 4 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -195,8 +195,10 @@ members = [
"third_party/move/move-ir/types",
"third_party/move/move-model",
"third_party/move/move-model/bytecode",
"third_party/move/move-model/bytecode-test-utils",
"third_party/move/move-prover",
"third_party/move/move-prover/boogie-backend",
"third_party/move/move-prover/bytecode-pipeline",
"third_party/move/move-prover/lab",
"third_party/move/move-prover/move-abigen",
"third_party/move/move-prover/move-docgen",
Expand Down Expand Up @@ -658,7 +660,9 @@ move-model = { path = "third_party/move/move-model" }
move-package = { path = "third_party/move/tools/move-package" }
move-prover = { path = "third_party/move/move-prover" }
move-prover-boogie-backend = { path = "third_party/move/move-prover/boogie-backend" }
move-prover-bytecode-pipeline = { path = "third_party/move/move-prover/bytecode-pipeline" }
move-stackless-bytecode = { path = "third_party/move/move-model/bytecode" }
move-stackless-bytecode-test-utils = { path = "third_party/move/move-model/bytecode-test-utils" }
aptos-move-stdlib = { path = "aptos-move/framework/move-stdlib" }
aptos-table-natives = { path = "aptos-move/framework/table-natives" }
move-prover-test-utils = { path = "third_party/move/move-prover/test-utils" }
Expand Down
3 changes: 2 additions & 1 deletion aptos-move/framework/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ anyhow = { workspace = true }
aptos-aggregator = { workspace = true }
aptos-crypto = { workspace = true, features = ["fuzzing"] }
aptos-gas-algebra = { workspace = true }
aptos-gas-schedule = { workspace = true }
aptos-gas-schedule = { workspace = true }
aptos-move-stdlib = { workspace = true }
aptos-native-interface = { workspace = true }
aptos-sdk-builder = { workspace = true }
Expand Down Expand Up @@ -59,6 +59,7 @@ move-model = { workspace = true }
move-package = { workspace = true }
move-prover = { workspace = true }
move-prover-boogie-backend = { workspace = true }
move-prover-bytecode-pipeline = { workspace = true }
move-stackless-bytecode = { workspace = true }
move-vm-runtime = { workspace = true }
move-vm-types = { workspace = true }
Expand Down
6 changes: 3 additions & 3 deletions aptos-move/framework/src/prover.rs
Original file line number Diff line number Diff line change
Expand Up @@ -176,12 +176,12 @@ impl ProverOptions {
let opts = move_prover::cli::Options {
output_path: "".to_string(),
verbosity_level,
prover: move_stackless_bytecode::options::ProverOptions {
prover: move_prover_bytecode_pipeline::options::ProverOptions {
stable_test_output: self.stable_test_output,
auto_trace_level: if self.trace {
move_stackless_bytecode::options::AutoTraceLevel::VerifiedFunction
move_prover_bytecode_pipeline::options::AutoTraceLevel::VerifiedFunction
} else {
move_stackless_bytecode::options::AutoTraceLevel::Off
move_prover_bytecode_pipeline::options::AutoTraceLevel::Off
},
report_severity: Severity::Warning,
dump_bytecode: self.dump,
Expand Down
20 changes: 20 additions & 0 deletions third_party/move/move-model/bytecode-test-utils/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
[package]
name = "move-stackless-bytecode-test-utils"
version = "0.1.0"
authors = ["Diem Association <[email protected]>"]
description = "Move stackless bytecode"
repository = "https://github.com/diem/diem"
homepage = "https://diem.com"
license = "Apache-2.0"
publish = false
edition = "2021"

[dependencies]
anyhow = "1.0.52"
codespan-reporting = { version = "0.11.1", features = ["serde", "serialization"] }
move-command-line-common = { path = "../../move-command-line-common" }
move-compiler = { path = "../../move-compiler" }
move-model = { path = ".." }
move-prover-test-utils = { path = "../../move-prover/test-utils" }
move-stackless-bytecode = { path = "../bytecode" }
move-stdlib = { path = "../../move-stdlib" }
93 changes: 93 additions & 0 deletions third_party/move/move-model/bytecode-test-utils/src/lib.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,93 @@
// Copyright © Aptos Foundation
// Parts of the project are originally copyright © Meta Platforms, Inc.
// SPDX-License-Identifier: Apache-2.0

use anyhow::anyhow;
use codespan_reporting::{diagnostic::Severity, term::termcolor::Buffer};
use move_command_line_common::testing::EXP_EXT;
use move_compiler::shared::{known_attributes::KnownAttribute, PackagePaths};
use move_model::{model::GlobalEnv, options::ModelBuilderOptions, run_model_builder_with_options};
use move_prover_test_utils::{baseline_test::verify_or_update_baseline, extract_test_directives};
use move_stackless_bytecode::{
function_target_pipeline::{
FunctionTargetPipeline, FunctionTargetsHolder, ProcessorResultDisplay,
},
print_targets_for_test,
};
use std::path::Path;

/// A test runner which dumps annotated bytecode and can be used for implementing a `datatest`
/// runner. In addition to the path where the Move source resides, an optional processing
/// pipeline is passed to establish the state to be tested. This will dump the initial
/// bytecode and the result of the pipeline in a baseline file.
/// The Move source file can use comments of the form `// dep: file.move` to add additional
/// sources.
pub fn test_runner(
path: &Path,
pipeline_opt: Option<FunctionTargetPipeline>,
) -> anyhow::Result<()> {
let mut sources = extract_test_directives(path, "// dep:")?;
sources.push(path.to_string_lossy().to_string());
let env: GlobalEnv = run_model_builder_with_options(
vec![PackagePaths {
name: None,
paths: sources,
named_address_map: move_stdlib::move_stdlib_named_addresses(),
}],
vec![],
ModelBuilderOptions::default(),
false,
KnownAttribute::get_all_attribute_names(),
)?;
let out = if env.has_errors() {
let mut error_writer = Buffer::no_color();
env.report_diag(&mut error_writer, Severity::Error);
String::from_utf8_lossy(&error_writer.into_inner()).to_string()
} else {
let dir_name = path
.parent()
.and_then(|p| p.file_name())
.and_then(|p| p.to_str())
.ok_or_else(|| anyhow!("bad file name"))?;

// Initialize and print function targets
let mut text = String::new();
let mut targets = FunctionTargetsHolder::default();
for module_env in env.get_modules() {
for func_env in module_env.get_functions() {
targets.add_target(&func_env);
}
}
text += &print_targets_for_test(&env, "initial translation from Move", &targets);

// Run pipeline if any
if let Some(pipeline) = pipeline_opt {
pipeline.run(&env, &mut targets);
let processor = pipeline.last_processor();
if !processor.is_single_run() {
text += &print_targets_for_test(
&env,
&format!("after pipeline `{}`", dir_name),
&targets,
);
}
text += &ProcessorResultDisplay {
env: &env,
targets: &targets,
processor,
}
.to_string();
}
// add Warning and Error diagnostics to output
let mut error_writer = Buffer::no_color();
if env.has_errors() || env.has_warnings() {
env.report_diag(&mut error_writer, Severity::Warning);
text += "============ Diagnostics ================\n";
text += &String::from_utf8_lossy(&error_writer.into_inner());
}
text
};
let baseline_path = path.with_extension(EXP_EXT);
verify_or_update_baseline(baseline_path.as_path(), &out)?;
Ok(())
}
3 changes: 1 addition & 2 deletions third_party/move/move-model/bytecode/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,7 @@ serde = { version = "1.0.124", features = ["derive"] }
[dev-dependencies]
anyhow = "1.0.52"
datatest-stable = "0.1.1"
move-prover-test-utils = { path = "../../move-prover/test-utils" }
move-stdlib = { path = "../../move-stdlib" }
move-stackless-bytecode-test-utils = { path = "../bytecode-test-utils" }

[[test]]
name = "testsuite"
Expand Down
23 changes: 1 addition & 22 deletions third_party/move/move-model/bytecode/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,44 +10,23 @@ use std::fmt::Write;

pub mod annotations;
pub mod borrow_analysis;
pub mod clean_and_optimize;
pub mod compositional_analysis;
pub mod data_invariant_instrumentation;
pub mod dataflow_analysis;
pub mod dataflow_domains;
pub mod debug_instrumentation;
pub mod eliminate_imm_refs;
pub mod function_data_builder;
pub mod function_target;
pub mod function_target_pipeline;
pub mod global_invariant_analysis;
pub mod global_invariant_instrumentation;
pub mod global_invariant_instrumentation_v2;
pub mod graph;
pub mod inconsistency_check;
pub mod livevar_analysis;
pub mod loop_analysis;
pub mod memory_instrumentation;
pub mod mono_analysis;
pub mod mut_ref_instrumentation;
pub mod mutation_tester;
pub mod number_operation;
pub mod number_operation_analysis;
pub mod options;
pub mod packed_types_analysis;
pub mod pipeline_factory;
pub mod reaching_def_analysis;
pub mod spec_instrumentation;
pub mod stackless_bytecode;
pub mod stackless_bytecode_generator;
pub mod stackless_control_flow_graph;
pub mod usage_analysis;
pub mod verification_analysis;
pub mod verification_analysis_v2;
pub mod well_formed_instrumentation;

/// An error message used for cases where a compiled module is expected to be attached
pub(crate) const COMPILED_MODULE_AVAILABLE: &str = "compiled module missing";
pub const COMPILED_MODULE_AVAILABLE: &str = "compiled module missing";

/// Print function targets for testing and debugging.
pub fn print_targets_for_test(
Expand Down
Loading

0 comments on commit 7350baf

Please sign in to comment.