Resources, Obligations, Time Reasoning#1408

Open

vfukala wants to merge 90 commits intoviperproject:masterfrom

vfukala:simplest-obligation

Commits on Jun 27, 2023

Add resource predicates

Pialex99
authored and
vfukala
committed
Add tests for time resources

Pialex99
authored and
vfukala
committed
Fix unfolding issue

Pialex99
authored and
vfukala
committed
Add resource predicates generation

Pialex99
authored and
vfukala
committed
Feedback

Pialex99
authored and
vfukala
committed
Add flag to enable time reasoning

Pialex99
authored and
vfukala
committed
Add more test for time reasoning

Pialex99
authored and
vfukala
committed
Add new tick builtin method

Pialex99
authored and
vfukala
committed
Add calls to tick in loops

Pialex99
authored and
vfukala
committed
Update tests

Pialex99
authored and
vfukala
committed
Add more tests

Pialex99
authored and
vfukala
committed
Remove calls to tick to an exhale and an inhale for error reporting

Pialex99
authored and
vfukala
committed
More tests and add an expression simplifier for methods

Pialex99
authored and
vfukala
committed
Formating

Pialex99
authored and
vfukala
committed
Add position to time credits/receipts expr

Pialex99
authored and
vfukala
committed
Add temporary error reporting

Pialex99
authored and
vfukala
committed
Add more complex tests

Pialex99
authored and
vfukala
committed
Fix position for error reporting

Pialex99
authored and
vfukala
committed
Fix rebase

Pialex99
authored and
vfukala
committed
Fix clippy error

Pialex99
authored and
vfukala
committed
Pull request reviews

Pialex99
authored and
vfukala
committed
Add scope id to resource predicate for loop body

Pialex99
authored and
vfukala
committed
Add functions to modify resource predicate scope

Pialex99
authored and
vfukala
committed
Add loop cost

Pialex99
authored and
vfukala
committed
More quadratic loops in a seperate test

Pialex99
authored and
vfukala
committed
Clippy

Pialex99
authored and
vfukala
committed
Fix small issues from rebase
vfukala
committed
Implement hardcoded PyRefObligation without leak checks yet
vfukala
committed
Add forperm expressions and (very hacky) leak checks
vfukala
committed
Replace PyRefObligations with generic obligations in VIR
vfukala
committed
Add general obligations (quite hacky so far)
vfukala
committed
Fix obligation access with struct arguments by also patching it in snapshot patcher
vfukala
committed
Add amount and scope_id to obligations
vfukala
committed
Add a few demo programs
vfukala
committed
Add alloc-dealloc demo program
vfukala
committed
Add demos, preprocess quantifiers, disable fix_quantifiers optimization
vfukala
committed
Add a simple demo with struct as an argument to an obligation
vfukala
committed
Add leak checks to poly. VIR and generate them also in loops
vfukala
committed
Fix compile errors from last update
vfukala
committed
Revert import reformatting in procedure encoder
vfukala
committed
Revert reformatting of the first half of the procedure encoder
vfukala
committed
A few things missed in last commit
vfukala
committed
Revert the rest of reformatting in procedure encoder
vfukala
committed
Revert remaining reformatting
vfukala
committed
Add back an accidentally removed trace! invocation
vfukala
committed
Don't include guard in loop invariant if it inhales an impure expression
vfukala
committed
Fix folding optimization for obligations, add pass tests for obligations
vfukala
committed
Replace leak check statements by leak check expressions
vfukala
committed
Remove commented code from obligation parsing
vfukala
committed
Autoformat
vfukala
committed
Satisfy Clippy
vfukala
committed

Commits on Jun 29, 2023

Fix method purifier crash due to forperm
vfukala
committed

Commits on Jul 2, 2023

Commits on Jul 3, 2023

Only split quantifiers if body impure; check for and report misplaced impure exprs
vfukala
committed

Commits on Jul 4, 2023

Properly attach position info to float backend functions; move #729 to pass; bump specs version
vfukala
committed

Commits on Jul 6, 2023

Commits on Jul 8, 2023

Commits on Jul 10, 2023

Commits on Jul 13, 2023

Commits on Jul 14, 2023

Commits on Jul 15, 2023

Commits on Jul 18, 2023

Temporarily remove snap from spec-only checks
vfukala
committed

Commits on Jul 23, 2023

Patch resources in pure function contracts
vfukala
committed

Commits on Jul 26, 2023

Fix stack overflow for non-trusted functions calling themselves in their contracts
vfukala
committed

Commits on Jul 28, 2023