Isle documentation#37
Closed
yuetongz417 wants to merge 45 commits intowellesley-prog-sys:veriislefrom
Closed
Conversation
…reg_mem, chain to_amode, add model for GprMem
…reg_mem, chain to_amode, add model for GprMem
…er returning unmatched types (concrete type error between types: bv 16 int)
…ix MInst.MovzxRmR to have a structure similar to MInst.ULoad8; fix spec for synthetic_amode_to_reg_mem & reg_mem_to_gpr_mem corresponding to GprMem definition; fix type issue for ext_mode; 2) identify 4 new rules - 2.1 left_shift_small: wrote vacuous spec for raw_operand_size_of_type; 2.2 store_narror; 2.3 Xor_mem_reg; 2.4 stack_add_guard
2. store_narrow: added spec for raw_operand_size_of_type; MInst.MovRM TODO 3. stack_add: got stuck on 'providing a model for StackSlot’ 4. Xor_mem_reg: added model for SinkableLoad; spec for sinkable_load & MInst.AluRM TODO 5. left_shift_small: added model for Imm8Gpr; added chain for put_masked_in_imm8_gpr; spec for const_to_type_masked_imm8 TODO; x64_shl if chained, program stucks
…to be analyzed); fix type_inference.rs to print conflicts; 2. store_narrow, xor_mem_reg: not updated; 3. stack_add_guard: deleted; 4. left_shift_small: defined model for Imm8Gpr as a struct; chained put_masked_in_imm8_gpr; wrote specs for const_to_type_masked_imm8, x64_shl (*no extern, but if chained, the script cannot run), gpr_to_imm8_gpr, shift_mask; working on specs for RegMemImm.Imm.
1. load_narrow: fix MInstr.MovzxRmR; fix reg_mem_to_gpr_mem to have to be ; 2. left_shift_small: added spec for RegMemImm.Imm; fixed put_masked_in_imm8_gpr by removing the chain and providing a spec; fixed spec for x64_shl to type-check # of bits.
…_load, RegMemImm.Mem.
README file to the CS340 final project.
…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
…d specs, still got underconstrained error
…pplicable conditions
…tions: 323 || 476 and 1643 || 1781
avanhatt
requested changes
Mar 3, 2026
avanhatt
left a comment
There was a problem hiding this comment.
As we discussed in slack, this needs to be rebased off of veriisle, not your other changes. Otherwise, looks on the right track! Lots of inline comments.
| <sig-args> ::= "(" "args" <model-ty>* ")" | ||
| <sig-ret> ::= "(" "ret" <model-ty>* ")" | ||
| <sig-canon> ::= "(" "canon" <model-ty>* ")" | ||
| ``` |
There was a problem hiding this comment.
Add a new section on the end on how to run the verifier on individual rules/rule chains, using the artifact documentation as a starting point
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
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.
Update ISLE reference for verification subset (Markdown/formal grammar work)
Separated the verification grammar into four main verification features: spec, model, form, and instantiate.
For each feature, I included the formal grammar, an explanation of its semantic meaning, a brief description of the parser implementation, and an example of how it is used during verification.