search

jyoo980 / silver

Definition of the Viper intermediate verification language.
Mozilla Public License 2.0
0 stars 0 forks source link

adding method rewrite proof-of-concept 3 (electric boogalee) #3

Closed ionathanch closed 3 years ago

ionathanch commented 4 years ago

This is mostly based off of 513/poc-2 but I combined a bunch of stuff so that fewer traversals are needed but maybe it's bad practice :speak_no_evil: We should probably also ask Alex/the Viper devs how to properly traverse things because I have no idea if these Strategy things are correct...

jyoo980 commented 3 years ago

@ionathanch I think this is good to merge. We can then branch off of master when we all dogpile on it

ionathanch commented 3 years ago

Do you prefer that I merge with or without squashing?

jyoo980 commented 3 years ago

@ionathanch

In most projects I like squashing, but since we're pretty new to all this - I think leaving behind a set of commits with very targeted work performed in them might be a good idea to onboard other people. That said, it's up to you 🙂

jyoo980 commented 3 years ago

i could not resist 😩

tested with 

field elem: Int
field next: Ref

predicate list(this: Ref) {
  acc(this.elem) && acc(this.next) && (this.next != null ==> list(this.next))
}

does not detect mutually-recursive predicates...yet

ionathanch commented 3 years ago

I didn't know viper.silver.ast had all these visitor functions omg that's a lot cleaner... I have some code in InlineRewrite to rewrite