Merged
Conversation
* Use asserts when type checking * Subst global constants in constraints
* Support integer comparisons * Support ite * More aggressive (and unsound) fdiv reasoning * Support pow2
* Path constraints are scoped and informed by: * Literal pattern matches * If conditions * Asserts * Only expressions that can be shown constant are considered * Constant checking logic is currently broken for local vars
* Unroll pow2 to a finite bound to avoid reasoning over reals * Mark Expr_If as supported
* Allow casting of unknown value back to expression. Maybe this is indicative of some greater problem, but these unknowns have been so abused, don't really care at this point. * Allow comparison over enums when integers would be expected.
* Support emitting zdiv_int as sdiv_bits. This is actually the easy case, but never came up in ARMv8. * Disable the collection of cse terms under an If. Injection of the common var def is not quite right.
* Support extracting boolean literals when building syms * Support extracting values from an Expr_Tuple
RISCV has many wide fields that are tested down to ~10 values at most. These are a pain for the coverage, which wants to enumerate the whole field. Added a quick script to extract these values and generate case statements for coverage automatically.
* Generalised encoding of all division tricks * Common path for uninterp
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
We have a reasonable RISC-V model by translation from Sail. A few changes are necessary to get ASLi to accept these models though, as the Sail type system is more complex. Even with these changes, there are a number of functions that do not type check due to a reliance on if-statement guards to prove type correctness.
Changes include:
PSTATE, etc. exists in the model.Expr_If,pow2_int, and more (unsound) heuristics aroundfdiv_int.Stmt_Assertwhen reasoning over types.