Enum model implementation #103
Closed
yuetongz417 wants to merge 1901 commits intoavanhatt:verify-mainfrom
Closed
Conversation
Enable rust cache in CI.
Add `:named` attribute on expression assignment assertions. The debugging experience is still awful, but naming some assertions still gives the possibility that a motivated expert can deduce something from an unsat core. Updates bytecodealliance#142
Add support for fetching models containing unspecified values. With the addition of declared sorts in bytecodealliance#141, this broke the code that parses constants from SMT models. The backend solvers differ on how they implement this. This PR deals with the CVC5 format only, in which unspecified values are represented as something like `(as @Unspecified_0 Unspecified)`. Updates avanhatt#45
Use temporary log directory in filetests. Prevents the tests from conflicting with each other.
Provide specs for store rules and verify a subset of expansions. Updates wellesley-prog-sys#34
Adds a basic status tool that reports: * Number of expansions in the coverage set (excluding skipped tags) * Number of expansions in the coverage set that have specifications for all terms * Unspecified terms ranked by appearance count in the coverage set Updates avanhatt#47
This PR adds a `matches` clause to specs which describes the conditions when an extractor (non-infallible) or partial constructor matches. Currently, the meaning of the `requires` clause on specs is conflated. It's treated as a traditional function pre-condition, and as a specification of when an `Option<..>` return from a term is `Some`. This dual purpose leads to confusing semantics that prevents us from modeling priorities correctly, see mmcloughlin/veriisle-wasmtime#128 (comment). This change may well be controversial given its departure from the Crocus conventions. We could also revert to dual-purpose `require` clauses, and change the semantics to fix the priority problem. I personally would advocate for the new syntax as it clarifies the meanings of the two cases. Updates bytecodealliance#128
Fix the `Extend` spec to use 8-bit bitvectors for `from_bits` and `to_bits`.
Generates the flag-setting opcodes for `AluRRImm12`. Relies on the CSE fix in ASLp added in mmcloughlin/aslp#5. Updates wellesley-prog-sys#36 wellesley-prog-sys#35
Populate a `rule_map` in the `sema::TermEnv` mapping interned rule names to rule IDs. This is similar to the `term_map` that already exists. This should be useful in bytecodealliance#151 bytecodealliance#128 where we need to apply attributes to rules.
Provide support for incorporating rule priorities into verification conditions. When priorities are considered, the behavior is that for all strictly higher-priority rules that may overlap with the rule under expansion, the negation of the overlapping rule's constraints are brought into the expansion. This necessitates brining in more bindings referenced by the negated rule's constraints. One problem is that overlap detection does not work when internal extractors are left unexpanded. This is the most gross aspect of the approach here, since we have to parse and run `sema` on the input ISLE twice, once without internal extractor expansion just so we can deduce the rule overlap sets. When rule priorities are factored in it can lead to poor user experience since the negated constraints bring in more terms that have to be satisfied. In the fairly common case where priorities are not actually relevant for correctness this can be annoying. Therefore, we introduce a new rule attribute `(attr <rule> (veri priority))` which denotes that the rule's correctness depends on priority. Negated higher-priority rules will only be considered when this attribute is present. Updates bytecodealliance#128
Verify the `iabs` rules. This did uncover an oddity that the `iabs` 32-bit and lower cases emit extend instructions from 32-to-32 bits. This failed at first since our ASLp generation only generated cases with `from_bits < to_bits`. Updates wellesley-prog-sys#34 wellesley-prog-sys#35
Implement most remaining spec ops, with the exception of the encoded ops and bitwise rotates. Removed `Subs` since I hope we can handle it via ASLp. Renamed `BV2Int` to `BV2Nat` to more faithfully represent the produced SMT operator.
Assume that enum discriminants are in the right range: positive integers less than the number of variants. Fixes bytecodealliance#158
Verify integer min/max. These rules are a great demonstration of the new priority support, since the correctness of the `cmp_and_choose` helper rule for `fits_in_64` relies on the higher priority 16-bit case. Updates bytecodealliance#128
Verify `imul`, `smulhi` and `umulhi` rules. Updates wellesley-prog-sys#34
Verify rules involving `bxor`. Updates wellesley-prog-sys#34
Implements match variant bindings in verification condition generation. Updates avanhatt#48
Generate conditional-set and conditional-set-mask instruction specs. Update wellesley-prog-sys#35
Generate conditional compare instruction specs. Updates wellesley-prog-sys#35
Add the `cls` (count leading sign rules). - Add custom encoding for cls. - Utilizes the new priority support for the 32/64 cases bytecodealliance#128 Co-authored-by: Vaishu Chintam <jc103@wellesley.edu>
Allow specificiation of type instantiations for enum variant terms. Updates avanhatt#48
…codealliance#168) Generate load/store specs using `AMode.UnsignedOffset`. Updates wellesley-prog-sys#36 avanhatt#49 wellesley-prog-sys#35
Attach positional information to spec expressions. This is the first stage in the positional information plumbing required to support more helpful error messages. Updates bytecodealliance#169
Add a spec expression `(as <expr> <ty>)` to specify the type of a spec expression inline. The syntax is motivated by SMT-LIB qualified identifiers. The motivation for this is the need to express register width constraints in ASLp-derived specs.
Model the `Reg` type on AArch64 as unknown bitvector width. Reverses bytecodealliance#108. The motivation for this is the need to model vector intructions, where `Reg` is also used to represent ARM `Z` 128-bit registers. The type inference problems that necessitated the 64-bit type before have now been fixed by a combination of bytecodealliance#167 and bytecodealliance#171. Updates avanhatt#46 wellesley-prog-sys#34
Generate spec for `MInst.VecLanes`, required for `popcnt` lowering. Updates wellesley-prog-sys#34 wellesley-prog-sys#35
Generate the `MovToFpu` specs, required for `popcnt`. Updates wellesley-prog-sys#34 wellesley-prog-sys#35
Implement conditional branch joining logic for if/else branches that assign to distinct targets. Until now all conditionals in ASLp programs have assigned to the same targets on both branches. The merging logic or "phi nodes" only implemented the logic for this simpler case. The `VecMisc` instructions required for `popcnt` verification include `if` statements without `else`, and therefore fail in this step. This PR refactors the code to handle the distinct case. The change is a no-op on current specs. Updates wellesley-prog-sys#35 wellesley-prog-sys#34
Generate `VecMisc` count opcode spec, required for popcount verification. Updates wellesley-prog-sys#34
…_load, RegMemImm.Mem.
README file to the CS340 final project.
Filetests are failing in CI with `can't resolve libcall` errors.
Set the solver strategy when using `z3`.
Line counting for ISLE code. Based on bytecodealliance#305. Co-authored-by: Chris Fallin <chris@cfallin.org>
…llesley-prog-sys#29) Verify x86 narrow load/store
…into arrival-runner
add Compound::ExtEnum to type.rs Implemented Display and resolve for ExtEnum and unwrap as_enum() in type.rs Extended alloc_value to allocate ExtEnum values in veri.rs Add Symbolic::ExtEnum and Value::ExtEnum variants in veri.rs Implemented eval and Display for ExtEnum in veri.rs Verified compilation succeeds after these changes.
In ast.rs: added ModelType::ExtEnum and ModelValue::ExtEnumValue, and introduced ModelVariant In types.rs: extended Compound::from_ast to lower ModelType::ExtEnum into Compound::ExtEnum In specs.rs: added two helpers to extend collect_models to handle ExtEnum (clone base enum, lower extra fields, and insert new Compound::ExtEnum into type_model
1. in parser.rs: extend parse_model to recognize (type-ext-enum) 2. in specs.rs (minor change)
in parser.rs - extend 'parse_model' to recognize (type-ext-enum)
… problem - still facing duplicate model problem
…d fix specs.rs by specifying that if a spec already exists, do not generate one for it
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
5 participants
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.