Lean build riscv full #2
Open
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
Re-organise so the funding information is clearly distinct from the BSD 2-clause license
This reduces the number of warnings+errors from 3021 to 1562 on the RISC-V spec. This closes rems-project#1011. Co-authored-by: Léo Stefanesco <[email protected]>
1. We handle irrefutable patterns in argument positions by adding an equivalent let in the prelude of the function. 2. We handle `atom` types deep inside the type of the arguments. We translate the pattern in the argument as above as a variable, and we replace the sail type variable by `tuple.2.1` in the return type. This path and the variable bound in the let binding in the prelude are definitionally equal. 3. As a side fix, we use more unique names for the autogenerated variable names by numbering them, which should avoid some spurious shadowing.
This partially addresses the fact that Sail has a different namespace for types and terms, and as such some models have types with the same names as terms.
This is useful for the RISC-V model which requires some functions to be implemented by the backend. To add a file, use the --lean-import-file option, it can be repeated. If we want to do as the Coq backend and have some of these functions be axioms in order to leave them arbitrary, we need to declare the whole output as noncomputable, which is controlled by a new option --lean-noncomputable.
1. Fix vectorUpdate being conflated with bitvectorUpdate 2. Use boolean operators instead of Prop connectives, the lean coertion mechanism seemed confused in big monadic expressions.
Since master is protected we don't need on push, as this just duplicates jobs on PRs from branches in the main repo
* First test * Lean: adding support for early returns * CI: Remove new test from lean/sv suites --------- Co-authored-by: Alasdair <[email protected]>
* Lean: Small fixes for the RISC-V model * fix ite in argument * remove_er
Call initialize_registers before main if present Note there is an issue with registers that have specific initial values i.e. register R = <initial_value> and these are not currently translated correctly
The only semantic change this PR proposes is to not assert on argument pattern that we cannot yet translate, but instead to record them as `TODO_ARG_PATTERN`. This is sufficient to build the full RISC-V Sail model without assertions and with about 3500 warnings and errors remaining. This PR also introduces a GitHub action to validate that the RISC-V model builds. The RISC-V model currently requires two patches (one in Ryan's repository and one applied through this patch). Over time, we expect to switch to the main RISC-V repo. Co-authored-by: Léo Stefanesco <[email protected]>
* Add rounding normal handing for same exp if no reach limit * Add more rounding mode and exception flags. * Make sure the code change covered by test. Signed-off-by: Pan Li <[email protected]>
…project#1050) * Lean: Adding support for handling while loops * Removing Coes that weren't supposed to be here * formatting * fix test * Fixing type error * Fixing inner loops with early returns * Adding a comment to early_ret * handling early returns in match/ite * Fixing effectful early returns * small fix for app id
Add a few more tests that now pass to CI
…roject#1084) * Lean: Adding a specialization file from `PreSailM` to `SailM` * formatting * fix main_of_sail_main * Lean: specialize throw/tryCatch --------- Co-authored-by: Léo Stefanesco <[email protected]>
This fixes the translation of the main function of the RISC-V model.
…#1088) This attempts to solve 1075 by just doing all of the operations in Int instead of `Nat.
This fixed Lean getting confused with Decidable instances Co-authored-by: Léon Frenot <[email protected]>
* Lean: Change loops to use native lean loops TODO: handle while and remove useless loop_ functions * Add while * Remove loops from library * remove `early_ret` from context * Changing loop body from monadic to pure * fixing exclusive range issue * fix ret_return
Mostly for testing Nat -> Int conversion in theorem prover backends, but caught a small bug in generated `string_of_` functions in Sail to OCaml
Adds a new rewrite to produce a sail_model_init function that, like the C backend's model_init, assigns the initialisation expression for each register to the register, then uses initialize_registers to set the rest to undefined. Hopefully this can also be used by other prover backends.
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.
No description provided.