Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove --harness requirement from stubbing #2495

Merged
merged 4 commits into from
Jun 3, 2023
Merged

Remove --harness requirement from stubbing #2495

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
0ec3aab
Remove --harness requirement from stubbing
celinval May 29, 2023
5c129e5
Merge branch 'main' into issue-1841-stub
celinval Jun 2, 2023
9ac6a90
Update kani-compiler/src/kani_compiler.rs
celinval Jun 2, 2023
e667bb8
Update kani-compiler/src/kani_compiler.rs
celinval Jun 2, 2023
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
39 changes: 23 additions & 16 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,10 @@

use crate::codegen_cprover_gotoc::GotocCtx;
use crate::kani_middle::analysis;
use crate::kani_middle::attributes::is_proof_harness;
use crate::kani_middle::attributes::is_test_harness_description;
use crate::kani_middle::check_crate_items;
use crate::kani_middle::check_reachable_items;
use crate::kani_middle::metadata::{gen_proof_metadata, gen_test_metadata};
use crate::kani_middle::metadata::gen_test_metadata;
use crate::kani_middle::provide;
use crate::kani_middle::reachability::{
collect_reachable_items, filter_const_crate_items, filter_crate_items,
Expand All @@ -33,6 +32,7 @@ use rustc_data_structures::fx::FxHashMap;
use rustc_data_structures::temp_dir::MaybeTempDir;
use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
use rustc_hir::def_id::LOCAL_CRATE;
use rustc_hir::definitions::DefPathHash;
use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
use rustc_metadata::EncodedMetadata;
use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
Expand All @@ -49,6 +49,7 @@ use rustc_target::abi::Endian;
use rustc_target::spec::PanicStrategy;
use std::any::Any;
use std::collections::BTreeMap;
use std::collections::HashSet;
use std::ffi::OsString;
use std::fmt::Write;
use std::fs::File;
Expand Down Expand Up @@ -234,13 +235,17 @@ impl CodegenBackend for GotocCodegenBackend {
match reachability {
ReachabilityType::Harnesses => {
// Cross-crate collecting of all items that are reachable from the crate harnesses.
let harnesses = filter_crate_items(tcx, |_, def_id| is_proof_harness(tcx, def_id));
let harnesses = queries.target_harnesses();
let mut items: HashSet<DefPathHash> = HashSet::with_capacity(harnesses.len());
items.extend(harnesses.into_iter());
let harnesses =
filter_crate_items(tcx, |_, def_id| items.contains(&tcx.def_path_hash(def_id)));
for harness in harnesses {
let metadata = gen_proof_metadata(tcx, harness.def_id(), &base_filename);
let model_path = &metadata.goto_file.as_ref().unwrap();
let model_path =
queries.harness_model_path(&tcx.def_path_hash(harness.def_id())).unwrap();
let (gcx, items) =
self.codegen_items(tcx, &[harness], model_path, &results.machine_model);
results.extend(gcx, items, Some(metadata));
results.extend(gcx, items, None);
}
}
ReachabilityType::Tests => {
Expand Down Expand Up @@ -296,16 +301,18 @@ impl CodegenBackend for GotocCodegenBackend {
// Print compilation report.
results.print_report(tcx);

// In a workspace, cargo seems to be using the same file prefix to build a crate that is
// a package lib and also a dependency of another package.
// To avoid overriding the metadata for its verification, we skip this step when
// reachability is None, even because there is nothing to record.
write_file(
&base_filename,
ArtifactType::Metadata,
&results.generate_metadata(),
queries.output_pretty_json,
);
if reachability != ReachabilityType::Harnesses {
// In a workspace, cargo seems to be using the same file prefix to build a crate that is
// a package lib and also a dependency of another package.
// To avoid overriding the metadata for its verification, we skip this step when
// reachability is None, even because there is nothing to record.
write_file(
&base_filename,
ArtifactType::Metadata,
&results.generate_metadata(),
queries.output_pretty_json,
);
}
}
codegen_results(tcx, rustc_metadata, &results.machine_model)
}
Expand Down
Loading