Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
113 changes: 113 additions & 0 deletions xlsynth-driver/src/common.rs
Original file line number Diff line number Diff line change
Expand Up @@ -413,3 +413,116 @@ pub fn execute_command_with_context(
}
result
}

// -----------------------------------------------------------------------------
// Shared DSLX -> IR conversion / optimization artifacts
// -----------------------------------------------------------------------------

pub struct DslxIrArtifacts {
pub raw_ir: String,
pub optimized_ir: Option<String>,
pub mangled_top: String,
}

pub struct DslxIrBuildOptions<'a> {
pub input_path: &'a std::path::Path,
pub dslx_top: &'a str,
pub dslx_stdlib_path: Option<&'a str>,
pub dslx_path: Option<&'a str>, // semicolon separated when Some
pub enable_warnings: Option<&'a [String]>,
pub disable_warnings: Option<&'a [String]>,
pub tool_path: Option<&'a str>,
pub type_inference_v2: Option<bool>,
pub optimize: bool,
}

/// Generalized builder that produces raw IR and (optionally) optimized IR for a
/// DSLX module. If `optimize` is false, `optimized_ir` will be `None`.
pub fn dslx_to_ir(opts: &DslxIrBuildOptions) -> DslxIrArtifacts {
let module_name = opts
.input_path
.file_stem()
.and_then(|s| s.to_str())
.expect("valid module name");
let mangled_top =
xlsynth::mangle_dslx_name(module_name, opts.dslx_top).expect("mangling succeeds");

if let Some(tool_path) = opts.tool_path {
// External tool path conversion.
let raw_ir = crate::tools::run_ir_converter_main(
opts.input_path,
Some(opts.dslx_top),
opts.dslx_stdlib_path,
opts.dslx_path,
tool_path,
opts.enable_warnings,
opts.disable_warnings,
opts.type_inference_v2,
);
let optimized_ir = if opts.optimize {
let tmp = tempfile::NamedTempFile::new().unwrap();
std::fs::write(tmp.path(), &raw_ir).unwrap();
Some(crate::tools::run_opt_main(
tmp.path(),
Some(&mangled_top),
tool_path,
))
} else {
None
};
DslxIrArtifacts {
raw_ir,
optimized_ir,
mangled_top,
}
} else {
if opts.type_inference_v2 == Some(true) {
eprintln!("error: --type_inference_v2 is only supported with external toolchain");
std::process::exit(1);
}
// Internal conversion path.
let dslx_contents = std::fs::read_to_string(opts.input_path).unwrap_or_else(|e| {
eprintln!(
"Failed to read DSLX file {}: {}",
opts.input_path.display(),
e
);
std::process::exit(1);
});
let stdlib_path = opts.dslx_stdlib_path.map(|p| std::path::Path::new(p));
let additional_search_paths: Vec<&std::path::Path> = opts
.dslx_path
.map(|s| s.split(';').map(|p| std::path::Path::new(p)).collect())
.unwrap_or_default();
let convert_result = xlsynth::convert_dslx_to_ir_text(
&dslx_contents,
opts.input_path,
&xlsynth::DslxConvertOptions {
dslx_stdlib_path: stdlib_path,
additional_search_paths,
enable_warnings: opts.enable_warnings,
disable_warnings: opts.disable_warnings,
},
)
.expect("successful DSLX->IR conversion");
for w in &convert_result.warnings {
log::warn!("DSLX warning: {}", w);
}
let raw_ir = convert_result.ir;
let optimized_ir = if opts.optimize {
let pkg = xlsynth::IrPackage::parse_ir(&raw_ir, Some(&mangled_top)).unwrap();
Some(
xlsynth::optimize_ir(&pkg, &mangled_top)
.unwrap()
.to_string(),
)
} else {
None
};
DslxIrArtifacts {
raw_ir,
optimized_ir,
mangled_top,
}
}
}
114 changes: 22 additions & 92 deletions xlsynth-driver/src/dslx_equiv.rs
Original file line number Diff line number Diff line change
@@ -1,87 +1,14 @@
// SPDX-License-Identifier: Apache-2.0

use crate::common::{dslx_to_ir, DslxIrBuildOptions};
use crate::ir_equiv::{dispatch_ir_equiv, EquivInputs};
use crate::parallelism::ParallelismStrategy;
use crate::solver_choice::SolverChoice;
use crate::toolchain_config::{get_dslx_path, get_dslx_stdlib_path, ToolchainConfig};
use crate::tools::{run_ir_converter_main, run_opt_main};
use xlsynth::{mangle_dslx_name, DslxConvertOptions, IrPackage};
use xlsynth_g8r::equiv::prove_equiv::AssertionSemantics;

const SUBCOMMAND: &str = "dslx-equiv";

pub struct OptimizedIrText {
pub ir_text: String,
pub mangled_top: String,
}

/// Builds (always optimized) IR text plus mangled top name for a DSLX module.
fn build_ir_for_dslx(
input_path: &std::path::Path,
dslx_top: &str,
dslx_stdlib_path: Option<&str>,
dslx_path: Option<&str>,
enable_warnings: Option<&[String]>,
disable_warnings: Option<&[String]>,
tool_path: Option<&str>,
type_inference_v2: Option<bool>,
) -> OptimizedIrText {
let module_name = input_path.file_stem().unwrap().to_str().unwrap();
let mangled_top = mangle_dslx_name(module_name, dslx_top).unwrap();

if let Some(tool_path) = tool_path {
// Convert via external tool then always optimize.
let mut ir_text = run_ir_converter_main(
input_path,
Some(dslx_top),
dslx_stdlib_path,
dslx_path,
tool_path,
enable_warnings,
disable_warnings,
type_inference_v2,
);
let tmp = tempfile::NamedTempFile::new().unwrap();
std::fs::write(tmp.path(), &ir_text).unwrap();
ir_text = run_opt_main(tmp.path(), Some(&mangled_top), tool_path);
OptimizedIrText {
ir_text,
mangled_top,
}
} else {
if type_inference_v2 == Some(true) {
eprintln!("error: --type_inference_v2 is only supported with external toolchain");
std::process::exit(1);
}
let dslx_contents = std::fs::read_to_string(input_path).unwrap_or_else(|e| {
eprintln!("Failed to read DSLX file {}: {}", input_path.display(), e);
std::process::exit(1);
});
let dslx_stdlib_path: Option<&std::path::Path> =
dslx_stdlib_path.map(|s| std::path::Path::new(s));
let additional_search_paths: Vec<&std::path::Path> = dslx_path
.map(|s| s.split(';').map(|p| std::path::Path::new(p)).collect())
.unwrap_or_default();
let result = xlsynth::convert_dslx_to_ir_text(
&dslx_contents,
input_path,
&DslxConvertOptions {
dslx_stdlib_path,
additional_search_paths,
enable_warnings,
disable_warnings,
},
)
.expect("successful DSLX->IR conversion");
let pkg = IrPackage::parse_ir(&result.ir, Some(&mangled_top)).unwrap();
let optimized = xlsynth::optimize_ir(&pkg, &mangled_top).unwrap();
OptimizedIrText {
ir_text: optimized.to_string(),
mangled_top,
}
}
}

pub fn handle_dslx_equiv(matches: &clap::ArgMatches, config: &Option<ToolchainConfig>) {
log::info!("handle_dslx_equiv");
let lhs_file = matches.get_one::<String>("lhs_dslx_file").unwrap();
Expand Down Expand Up @@ -172,38 +99,41 @@ pub fn handle_dslx_equiv(matches: &clap::ArgMatches, config: &Option<ToolchainCo

let tool_path = config.as_ref().and_then(|c| c.tool_path.as_deref());

let OptimizedIrText {
ir_text: lhs_ir_text,
mangled_top: lhs_mangled_top,
} = build_ir_for_dslx(
lhs_path,
lhs_top.unwrap(),
// Build artifacts (always optimized) for both sides.
let lhs_artifacts = dslx_to_ir(&DslxIrBuildOptions {
input_path: lhs_path,
dslx_top: lhs_top.unwrap(),
dslx_stdlib_path,
dslx_path,
enable_warnings,
disable_warnings,
tool_path,
type_inference_v2,
);
let OptimizedIrText {
ir_text: rhs_ir_text,
mangled_top: rhs_mangled_top,
} = build_ir_for_dslx(
rhs_path,
rhs_top.unwrap(),
optimize: true,
});
let rhs_artifacts = dslx_to_ir(&DslxIrBuildOptions {
input_path: rhs_path,
dslx_top: rhs_top.unwrap(),
dslx_stdlib_path,
dslx_path,
enable_warnings,
disable_warnings,
tool_path,
type_inference_v2,
);
optimize: true,
});

let inputs = EquivInputs {
lhs_ir_text: &lhs_ir_text,
rhs_ir_text: &rhs_ir_text,
lhs_top: Some(&lhs_mangled_top),
rhs_top: Some(&rhs_mangled_top),
lhs_ir_text: lhs_artifacts
.optimized_ir
.as_deref()
.unwrap_or(&lhs_artifacts.raw_ir),
rhs_ir_text: rhs_artifacts
.optimized_ir
.as_deref()
.unwrap_or(&rhs_artifacts.raw_ir),
lhs_top: Some(&lhs_artifacts.mangled_top),
rhs_top: Some(&rhs_artifacts.mangled_top),
flatten_aggregates,
drop_params: &drop_params,
strategy,
Expand Down
Loading