Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

RASI Generator #1171

Merged
merged 86 commits into from
Apr 7, 2024
Merged

RASI Generator #1171

merged 86 commits into from
Apr 7, 2024

Conversation

PBHTasche
Copy link
Contributor

@PBHTasche PBHTasche commented Mar 22, 2024 •
edited
Loading

Before merging this PR, please check the following:

  • I made sure the wiki is updated in accordance with the changes in this PR. For example, syntax changes, semantics changes, VerCors flags changes, etc.

PR description

  • Fixed problems in VeSUV that would not allow the program to run
  • Improved the VeSUV transformation
  • Added the ability to create a control flow graph out of a COL AST
  • Organized COL nodes by their behavior for the CFG
  • Added the ability to explore the state space of a COL program at an abstract level
  • Added flags to create either the CFG or the abstract state space from a given PVL program
  • Added a PVL keyword for a program entry point, "vesuv_entry"

@PBHTasche
Started work on RASI generator
860e66c
@PBHTasche
Solidified architecture of RASI generator
97e4ad3
@PBHTasche
Refined execution state tracking
c441e63
@PBHTasche
Working on Control Flow Graph for VerCors
df1654b
@PBHTasche
Added indexing system for nested statements
258827c
@PBHTasche
Added context indices for subroutine calls
e1cf533
@PBHTasche
Continued working on indexing system
9e766d0
@PBHTasche
Fixed typo
023ebe3
@PBHTasche
Allowed sets of successor indices, added support for fork, added recu…
485a276 
…rsion stop for resolve
@PBHTasche
Added support for break, continue, return and throw and started on sw…
967a6c4 
…itch statements
@PBHTasche
Added general support for statements hidden in expressions with side …
d36e867 
…effects
@PBHTasche
Improved support for expressions with side effects
7aedcd4
@PBHTasche
Continued support for expression side effects, some syntax fixes, add…
344df78 
…ed condition information to edges
@PBHTasche
Syntax fixes, project compiles
c4a7755
@PBHTasche
Implemented GraphViz/DOT printer for control flow graph
4bbb2ab
@PBHTasche
Started work on frontend support for CFG conversion
c89a728
@PBHTasche
Fixed implementation of subroutine invocations
1f994f6
@PBHTasche
Renamed VeSUV pass to avoid confusion
f9672e0
@PBHTasche
Connected frontend to backend for control flow graph printer
77e242a
@PBHTasche
Fixed small errors preventing execution
817d067
@PBHTasche
Fixed an infinite recursion when referring back to incompletely trans…
dc5d57b 
…formed nodes
@PBHTasche
Added path conditions to CFG edges
b7c114e
@PBHTasche
Finding main method automatically, added support for unresolved-conta…
7daac9e 
…iners, some code cleanup
@PBHTasche
Changed fork to create new stack; enabled terminal CFG nodes
2bc3a50
@PBHTasche
Enable terminal node
585c3c7
@PBHTasche
Added support for edge conditions in expression side effects
8da6793
@PBHTasche
Started work on CFG traversal for RASI generation
bd091dc
@PBHTasche
Working on RASI generator
d43a762
@PBHTasche
Added uncertain values to RASI generator
0d22af4
@PBHTasche
Finished expression side effects for With and Then
8f212d1
PBHTasche and others added 28 commits March 12, 2024 12:54
@PBHTasche
Some documentation for the abstract state
693064b
@PBHTasche
Improved support for extracting information out of assumptions
1aefbaa
@PBHTasche
Removed impossible states from assumption resolution
978f078
@PBHTasche
Fixed errors in the VeSUV implementation
c7136dd
@PBHTasche
Fixed some errors in the CFG and variable resolution for the RASI
a9f08ab
@PBHTasche
Added support for semantics of more expressions
8854b98
@PBHTasche
Fixed some errors in VeSUV from porting to VerCors 2.0.0
f233552
@PBHTasche
Fixed an error where state class constructors would ensure idle tokens
9c83f67
@PBHTasche
Implemented return value resolution from contracts; cleaned up constr…
ce9bd80 
…aint resolution
@PBHTasche
Fixed some type errors
2280f94
@PBHTasche
Fixed an error in the redundant state filter of the RASI generator
8b56687
@PBHTasche
Implemented verification support for vesuv main method
1e109ff
@PBHTasche
Enabled parsing and resolution of VeSUV main method
1299e5b
@PBHTasche
Started implementing support for considering atomic blocks
6123a98
@PBHTasche
Added predicate unfolding in search of global invariant
4671b54
@PBHTasche
Added explicit checks for loop and method contracts into the AST
b9bca0b
@PBHTasche
Fixed an error where atomic blocks would never terminate if they coul…
8640b79 
…d not make progress
@PBHTasche
Documentation; Fixed an error where atomic steps would always step ov…
35035f2 
…er unlock statements without letting other processes execute
@PBHTasche
Cleanup
99747d1
@PBHTasche
Tried to change constraint solving implementation
dbeca4e
@PBHTasche
Revert "Tried to change constraint solving implementation"
82854f7 
This reverts commit dbeca4e.
@PBHTasche
Taking into account expression viability for constraint resolution; a…
f10d417 
…dded more expressions to resolve
@PBHTasche
Fixed an error where global invariant assertions were not properly de…
960ed51 
…tected
@PBHTasche
Changed encoding of find_minimum_advance in VeSUV to avoid sequence p…
eba3309 
…arameter
@PBHTasche
Added mechanism by which variables in function contracts are uncertai…
c6db2ae 
…n if they are not old
@PBHTasche
Fixed errors in uncertain value comparisons; removed initial state fr…
14cd710 
…om RASI
@PBHTasche
Fixed errors with sequence operations and object comparison; added de…
6933480 
…bug information
@pieter-bos
Merge branch 'dev' into rasi_generator
1d6b44a
@pieter-bos pieter-bos merged commit 023d134 into dev Apr 7, 2024
6 checks passed
@pieter-bos pieter-bos deleted the rasi_generator branch April 7, 2024 08:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@PBHTasche @pieter-bos