Skip to content

Isle documentation#37

Closed
yuetongz417 wants to merge 45 commits intowellesley-prog-sys:veriislefrom
yuetongz417:isle_doc
Closed

Isle documentation#37
yuetongz417 wants to merge 45 commits intowellesley-prog-sys:veriislefrom
yuetongz417:isle_doc

Conversation

@yuetongz417
Copy link
Copy Markdown

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.

yuetongz417 and others added 30 commits April 28, 2025 19:40
…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.
README file to the CS340 final project.
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
Copy link
Copy Markdown

@avanhatt avanhatt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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>* ")"
```
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@avanhatt avanhatt closed this Mar 10, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants