Move symtab2gb to codegen step #1686
Conversation
|
@danielsn can you please fix this PR? |
danielsn
force-pushed
the
move-symtab-earlier
branch
3 times, most recently
from
1750d4a to
22f03d9
Compare
kani-driver/src/main.rs
Outdated
| @@ -44,7 +43,9 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> { | |||
|
|
|||
| let mut goto_objs: Vec<PathBuf> = Vec::new(); | |||
| for symtab in &outputs.symtabs { | |||
| goto_objs.push(ctx.symbol_table_to_gotoc(symtab)?); | |||
| let goto_obj_filename = symtab.with_extension("out"); | |||
| ctx.record_temporary_files(&[&goto_obj_filename]); | |||
There was a problem hiding this comment.
Do we remove these files still? If so, wouldn't this break subsequent runs of cargo kani?
There was a problem hiding this comment.
They were being removed before, and I thought it best to keep that behaviour. @tedinski thoughts?
There was a problem hiding this comment.
The file removal behavior for cargo kani was something I went "huh that's strange" and just preserved what the original python scripts did. We seem to keep some things and delete others and I'm not sure why really.
I'm open to any behavior that makes sense here.
There was a problem hiding this comment.
@celinval? Vote? Honestly, I think for cargo we should probably just keep everything since it goes into a target folder anyway.
There was a problem hiding this comment.
We do globs for what to link together in the end though, and that might motivate the deletion?
There was a problem hiding this comment.
For now, why don't we keep the current behaviour, and have an issue to have a principled set of things to keep/delete?
There was a problem hiding this comment.
Testing showed that removing the files makes repeated cargo-kani fail
There was a problem hiding this comment.
I don't think they are random today. We cannot delete the files that are generated by kani-compiler, otherwise rebuild breaks as @danielsn was able to verify.
That said, I do think we need better strategy. We should eventually implement a cache, and we should also consider not using glob anymore. We can use cargo_metadata to retrieve the files generated by the compiler instead.
danielsn
force-pushed
the
move-symtab-earlier
branch
from
22f03d9 to
35e950a
Compare
danielsn
force-pushed
the
move-symtab-earlier
branch
from
12c88ba to
6d6df75
Compare
Description of changes:
Currently, we compile each crate to a symbol-table json, then at the very end run
symtab2gb.This step logically belongs as part of codegen.
As a benefit, we now parallelize
symtab2gbcalls and get a speedup.Resolved issues:
Resolves #1453
Related RFC:
Call-outs:
Testing:
How is this change tested? Existing reg tests
Is this a refactor change? No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.