FreeBSD amd64 support #1409
Closed
FreeBSD amd64 support #1409
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Wow. This is really fantastic. |
|
I've committed the LLVM patch to our LLVM branch. Testing the Rust patches on the bots now. We really need a FreeBSD bot (#1410) in order to start snapshotting. Not sure how soon we can get that set up. |
|
Merged. Thanks! It will take some time to get the snapshots going. If nothing happens in a week feel free to bug graydon or I about it. |
|
Consider yourself bugged about it. Thanks! |
|
@dominicmarks Thanks ;-) |
celinval
added a commit
to celinval/rust-dev
that referenced
this pull request
Jun 4, 2024
* feat: prototype E2E mechanism for gen det vals and running exec trace This was formed by squashing the following commits: feat: exec-trace POC that gets kani::any assignments feat: init work making exec_trace a Kani command line flag feat: make trace parsing more precise feat: allow for multiple extracted values feat: Move parsing code into the driver refactor: move functions outside KaniSession test: add basic UI test for det val feat: change any_raw to make it easier to parse trace feat: update any_raw to use byte array feat: update parser to take in byte array chore: run rustfmt test: add constant generic bound to func abstraction tests test: fix remaining test issues to pass regression feat: update any_raw_inner to return bytes chore: remove spurious results file feat: update any_raw_inner to read from det_vals file feat: add exec_trace flag to kani-compiler refactor(kani-compiler): rename vars to increase readability feat(kani-compiler): specify different Kani lib paths feat: prototype E2E mechanism for gen det vals & running exec trace fix: add generic const trait bounds to any_vec feat: add print out to get debug command chore: remove det vals from tmp file list for demo * feat: towards printing unit test case * feat: add source modification feature * refactor: lots of it * feat: call cbmc only once * add back exe trace and fix unit test line numbers * refactor: create exe trace main * chore: revert kani-compiler changes * fix: update parser for new cbmc trace format * refactor: change contains to starts_with for perf * chore: revert check-output change * feat: put Kani lib exe trace code behind a feature * tests: fix one-assert test * feat: add more code under exe_trace feat * fix: reverse det vals list since we're popping off vals * feat: add exe_trace impls for other kani lib funcs * fix: assertion failed may not always be failure * fix: strict string equality actually works * feat: add fields to get the end of a func * feat: insert exe trace after harness * refactor: rename everything to exe_trace instead of exec_trace * refactor: move funcs out of kani session and remove pub visibility * refactor: move some code into parser module * refactor: remove generic const any_raw_inner since it will only be called on ints after Celina's PR * fix: remove 1 TODO and make 1 func priv * fix: add newline to cargo toml * feat: switch to using Vec<Vec<u8>> * feat: add comment in exe trace with interp det val * refactor: extend iterator * feat: don't insert same exe trace twice * feat: add kani lib func to init det vals * tests: forgot to add generic const stuff back into tests * tests: forgot about one-assert going back to normal * feat: add exe trace functionality for kani standalone * tests: add kani overall test * tests: forgot to add the exe trace test dir * chore: add safety msg back in * some more tests work * fix: clippy and license checks * tests: exe-trace test covers more primitives * docs: add func comments * small changes * docs: add comments * refactor: use named params in format strings * fix: update generic const invariants in kani lib after arbitrary change * fix: change parser to accomodate kani lib arbitrary changes * docs: add test case comment * docs: make arg comment a bit nicer * refactor: generalize rustfmt func in a nice way * feat: add any_raw_inner to more reliably get CBMC output. Also clarify test case semantics * feat: better formatting of printed test case * test: split tests into different directories per primitive * test: add f32, f64 tests * test: add comment about f32/f64 NaN values * docs: add better explanations for generic_const_exprs feature * refactor: rename parser funcs * feat: convert DET_VALS to static mut * feat: add lock around det vals for thread safety, update playback api to exe_trace_run * address some of Celina's PR comments * one way of implementing file reads using String vectors * refactor: different way of implementing src code modification, all as big strings * feat: hide exe traces under quiet flag * refactor: generate output filename once * feat: add more arg exclusions * refactor: call exe_trace_main inside run_cbmc * ui: add more info to concrete-mode assertion conversions * refactor: as much as possible, move Kani lib exe trace code to separate module * refactor: add kani::any_raw_internal exe_trace impl to sep mod also * refactor: replace whitespace with constant * refactor: add ExeTrace and DetVal structs * refactor, docs: rename bunch of funcs and add CBMC output format * refactor: remove as_slice * refactor: split up big if let in parser * fix: small typo that printed out test name instead of actual test * ui: make exe trace exists in src code comment more specific * feat: add anyhow error handling to CBMC trace parser * feat: add anyhow error handling to rest of kani driver exe_trace file * fix: clippy to_string display lints * feat: remove extra string allocation for new src file * ui: don't abreviate exe trace * docs: add todo for new parser * ui: add error handling for multiple diff asserts and checks * ui: add warning for adding unit tests for multiple failing harnesses * refactor: move have_parsed_assert_fail into parser glob var * refactor: make DET_VALS a thread_local static refcell * fix: had incorrect type info in the refcell changes * fix: changed exe_trace::any_raw_internal to pub crate * feat: add error handling around using any_raw funcs and switch to if cfg bang feature * ui: add assert around --output-format old * fix: make exe_trace mod private * refactor: change over to if cfg exe_trace instead of cfg exe_trace macro * refactor: require harness arg -> make have_parsed_assert_fail local to a single harness * fix: in CBMC output parser, write CBMC output to file if using exe_trace flag. This is for old exe_trace parser compatibility * lints: add carrots around URLs to fix clippy warning * refactor: move buf writer inside parser, but there's still an ownership issue * fix: the cbmc output parser ownership issue * fix: address PR comments around cbmc output parser changes Co-authored-by: Celina G. Val <celinval@amazon.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Before bootstrapping, it needs to install devel/libexecinfo and lang/gcc44+.
In order to enable segmented stacks, it also needs to patch LLVM.
This patch uses tcb_spare field in the tcb structure to store info.
For i386 arch there is no spare field so it can only work on amd64.
It currently failed on "modf(float::infinity, d2) == 0.0" and "pow(-1.0, float::infinity) == 1.0" in make check.
LLVM segmented stack patch:
http://people.cs.nctu.edu.tw/~jyyou/rust/bsd-seg-stack.diff
stage3 snapshot:
http://people.cs.nctu.edu.tw/~jyyou/rust/rust-stage0.tar.bz2