From 2a2c291106b02c5b9c6c7375922c1aa4a7c0719d Mon Sep 17 00:00:00 2001 From: naum_tomov Date: Mon, 4 Jul 2022 18:53:19 +0200 Subject: [PATCH 1/2] problem in viper with exceptions in proof blocks jumping out of the proof which cannot really happen --- col/src/main/java/vct/col/ast/Node.scala | 6 +- .../statement/composite/WandCreateImpl.scala | 4 +- .../statement/terminal/WandQedImpl.scala | 7 - .../statement/terminal/WandUseImpl.scala | 7 - .../vct/col/coerce/CoercingRewriter.scala | 6 +- .../java/vct/col/feature/FeatureRainbow.scala | 4 +- col/src/main/java/vct/col/origin/Blame.scala | 10 + col/src/main/java/vct/col/print/Printer.scala | 8 +- col/src/main/java/vct/col/resolve/Spec.scala | 3 + examples/archive/chalice/ListIterator.java | 389 ++++++++---------- parsers/lib/antlr4/LangCLexer.g4 | 1 + parsers/lib/antlr4/LangPVLLexer.g4 | 1 + parsers/lib/antlr4/SpecLexer.g4 | 4 +- parsers/lib/antlr4/SpecParser.g4 | 4 +- .../java/vct/parsers/transform/CToCol.scala | 6 +- .../vct/parsers/transform/JavaToCol.scala | 6 +- .../java/vct/parsers/transform/PVLToCol.scala | 6 +- .../vct/col/newrewrite/PrettifyBlocks.scala | 3 + .../ResolveExpressionSideEffects.scala | 4 +- .../java/vct/main/stages/Transformation.scala | 1 - .../src/main/java/viper/api/ColToSilver.scala | 11 + .../main/java/viper/api/SilverBackend.scala | 30 +- 22 files changed, 256 insertions(+), 265 deletions(-) delete mode 100644 col/src/main/java/vct/col/ast/temporaryimplpackage/statement/terminal/WandQedImpl.scala delete mode 100644 col/src/main/java/vct/col/ast/temporaryimplpackage/statement/terminal/WandUseImpl.scala diff --git a/col/src/main/java/vct/col/ast/Node.scala b/col/src/main/java/vct/col/ast/Node.scala index 641bc4a75f..949b4161a2 100644 --- a/col/src/main/java/vct/col/ast/Node.scala +++ b/col/src/main/java/vct/col/ast/Node.scala @@ -166,9 +166,7 @@ final case class Unlock[G](obj: Expr[G])(val blame: Blame[UnlockFailure])(implic final case class Commit[G](obj: Expr[G])(val blame: Blame[CommitFailed])(implicit val o: Origin) extends NormallyCompletingStatement[G] with CommitImpl[G] final case class Fold[G](res: Expr[G])(val blame: Blame[FoldFailed])(implicit val o: Origin) extends NormallyCompletingStatement[G] with FoldImpl[G] final case class Unfold[G](res: Expr[G])(val blame: Blame[UnfoldFailed])(implicit val o: Origin) extends NormallyCompletingStatement[G] with UnfoldImpl[G] -final case class WandQed[G](res: Expr[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with WandQedImpl[G] -final case class WandApply[G](res: Expr[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with WandApplyImpl[G] -final case class WandUse[G](res: Expr[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with WandUseImpl[G] +final case class WandApply[G](res: Expr[G])(val blame: Blame[WandApplyFailed])(implicit val o: Origin) extends NormallyCompletingStatement[G] with WandApplyImpl[G] final case class Havoc[G](loc: Expr[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with HavocImpl[G] final case class FramedProof[G](pre: Expr[G], body: Statement[G], post: Expr[G])(val blame: Blame[FramedProofFailure])(implicit val o: Origin) extends NormallyCompletingStatement[G] with FramedProofImpl[G] @@ -196,7 +194,7 @@ final case class ParAtomic[G](inv: Seq[Ref[G, ParInvariantDecl[G]]], content: St final case class ParBarrier[G](block: Ref[G, ParBlockDecl[G]], invs: Seq[Ref[G, ParInvariantDecl[G]]], requires: Expr[G], ensures: Expr[G], content: Statement[G])(val blame: Blame[ParBarrierFailed])(implicit val o: Origin) extends CompositeStatement[G] with ParBarrierImpl[G] final case class ParStatement[G](impl: ParRegion[G])(implicit val o: Origin) extends CompositeStatement[G] with ParStatementImpl[G] final case class VecBlock[G](iters: Seq[IterVariable[G]], requires: Expr[G], ensures: Expr[G], content: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with VecBlockImpl[G] -final case class WandCreate[G](statements: Seq[Statement[G]])(implicit val o: Origin) extends CompositeStatement[G] with WandCreateImpl[G] +final case class WandPackage[G](res: Expr[G], proof: Statement[G])(val blame: Blame[PackageFailed])(implicit val o: Origin) extends CompositeStatement[G] with WandCreateImpl[G] final case class ModelDo[G](model: Expr[G], perm: Expr[G], after: Expr[G], action: Expr[G], impl: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with ModelDoImpl[G] sealed abstract class Declaration[G] extends Node[G] with DeclarationImpl[G] { diff --git a/col/src/main/java/vct/col/ast/temporaryimplpackage/statement/composite/WandCreateImpl.scala b/col/src/main/java/vct/col/ast/temporaryimplpackage/statement/composite/WandCreateImpl.scala index 3481ad04e9..3a66cbc80d 100644 --- a/col/src/main/java/vct/col/ast/temporaryimplpackage/statement/composite/WandCreateImpl.scala +++ b/col/src/main/java/vct/col/ast/temporaryimplpackage/statement/composite/WandCreateImpl.scala @@ -1,7 +1,7 @@ package vct.col.ast.temporaryimplpackage.statement.composite -import vct.col.ast.WandCreate +import vct.col.ast.WandPackage -trait WandCreateImpl[G] { this: WandCreate[G] => +trait WandCreateImpl[G] { this: WandPackage[G] => } \ No newline at end of file diff --git a/col/src/main/java/vct/col/ast/temporaryimplpackage/statement/terminal/WandQedImpl.scala b/col/src/main/java/vct/col/ast/temporaryimplpackage/statement/terminal/WandQedImpl.scala deleted file mode 100644 index 83a2103e62..0000000000 --- a/col/src/main/java/vct/col/ast/temporaryimplpackage/statement/terminal/WandQedImpl.scala +++ /dev/null @@ -1,7 +0,0 @@ -package vct.col.ast.temporaryimplpackage.statement.terminal - -import vct.col.ast.WandQed - -trait WandQedImpl[G] { this: WandQed[G] => - -} \ No newline at end of file diff --git a/col/src/main/java/vct/col/ast/temporaryimplpackage/statement/terminal/WandUseImpl.scala b/col/src/main/java/vct/col/ast/temporaryimplpackage/statement/terminal/WandUseImpl.scala deleted file mode 100644 index a6506568b4..0000000000 --- a/col/src/main/java/vct/col/ast/temporaryimplpackage/statement/terminal/WandUseImpl.scala +++ /dev/null @@ -1,7 +0,0 @@ -package vct.col.ast.temporaryimplpackage.statement.terminal - -import vct.col.ast.WandUse - -trait WandUseImpl[G] { this: WandUse[G] => - -} \ No newline at end of file diff --git a/col/src/main/java/vct/col/coerce/CoercingRewriter.scala b/col/src/main/java/vct/col/coerce/CoercingRewriter.scala index f775faacec..a14445ff8c 100644 --- a/col/src/main/java/vct/col/coerce/CoercingRewriter.scala +++ b/col/src/main/java/vct/col/coerce/CoercingRewriter.scala @@ -1176,10 +1176,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends Rewriter[Pre] with case u @ Unlock(obj) => Unlock(cls(obj)._1)(u.blame) case VecBlock(iters, requires, ensures, content) => VecBlock(iters, res(requires), res(ensures), content) case w @ Wait(obj) => Wait(cls(obj)._1)(w.blame) - case WandApply(assn) => WandApply(res(assn)) - case WandCreate(statements) => WandCreate(statements) - case WandQed(assn) => WandQed(res(assn)) - case WandUse(assn) => WandUse(res(assn)) + case w @ WandApply(assn) => WandApply(res(assn))(w.blame) + case w @ WandPackage(expr, stat) => WandPackage(res(expr), stat)(w.blame) } } diff --git a/col/src/main/java/vct/col/feature/FeatureRainbow.scala b/col/src/main/java/vct/col/feature/FeatureRainbow.scala index ac99cfd990..7e46e6cf1a 100644 --- a/col/src/main/java/vct/col/feature/FeatureRainbow.scala +++ b/col/src/main/java/vct/col/feature/FeatureRainbow.scala @@ -309,10 +309,8 @@ class FeatureRainbow[G] { case node: Unlock[G] => IntrinsicLocks case node: Fold[G] => return Nil case node: Unfold[G] => return Nil - case node: WandCreate[G] => MagicWand - case node: WandQed[G] => MagicWand + case node: WandPackage[G] => MagicWand case node: WandApply[G] => MagicWand - case node: WandUse[G] => MagicWand case node: ModelDo[G] => Models case node: Havoc[G] => return Nil case node: Break[G] => ExceptionalLoopControl diff --git a/col/src/main/java/vct/col/origin/Blame.scala b/col/src/main/java/vct/col/origin/Blame.scala index 7b100cdbc0..999aeb6ddf 100644 --- a/col/src/main/java/vct/col/origin/Blame.scala +++ b/col/src/main/java/vct/col/origin/Blame.scala @@ -147,6 +147,16 @@ case class FoldFailed(failure: ContractFailure, node: Fold[_]) extends WithContr override def descInContext: String = "Fold may fail, since" override def inlineDescWithSource(node: String, failure: String): String = s"`$node` may fail, since $failure." } +case class PackageFailed(failure: ContractFailure, node: WandPackage[_]) extends WithContractFailure { + override def baseCode: String = "packageFailed" + override def descInContext: String = "Package statement may fail, since" + override def inlineDescWithSource(node: String, failure: String): String = s"`$node` may fail, since $failure." +} +case class WandApplyFailed(failure: ContractFailure, node: WandApply[_]) extends WithContractFailure { + override def baseCode: String = "applyFailed" + override def descInContext: String = "Wand apply may fail, since" + override def inlineDescWithSource(node: String, failure: String): String = s"`$node` may fail, since $failure." +} case class SendFailed(failure: ContractFailure, node: Send[_]) extends WithContractFailure { override def baseCode: String = "sendFailed" override def descInContext: String = "Send may fail, since" diff --git a/col/src/main/java/vct/col/print/Printer.scala b/col/src/main/java/vct/col/print/Printer.scala index 6b19bc905d..653db0b81b 100644 --- a/col/src/main/java/vct/col/print/Printer.scala +++ b/col/src/main/java/vct/col/print/Printer.scala @@ -544,14 +544,10 @@ case class Printer(out: Appendable, spec(statement("fold", space, pred)) case Unfold(pred) => spec(statement("unfold", space, pred)) - case WandCreate(statements) => - spec(control(phrase("create"), Block(statements)(DiagnosticOrigin))) - case WandQed(wand) => - spec(statement("qed", space, wand)) + case WandPackage(expr, state) => + spec(control(phrase("package", expr), state)) case WandApply(wand) => spec(statement("apply", space, wand)) - case WandUse(pred) => - spec(statement("use", space, pred)) case Havoc(loc) => ??? case Break(label) => diff --git a/col/src/main/java/vct/col/resolve/Spec.scala b/col/src/main/java/vct/col/resolve/Spec.scala index 482596d58f..d4075a93cd 100644 --- a/col/src/main/java/vct/col/resolve/Spec.scala +++ b/col/src/main/java/vct/col/resolve/Spec.scala @@ -238,6 +238,9 @@ case object Spec { case TClass(Ref(cls)) => cls.declarations.flatMap(Referrable.from).collectFirst { case ref @ RefInstancePredicate(decl) if ref.name == name => decl } + case JavaTClass(Ref(cls), _) => cls.declarations.flatMap(Referrable.from).collectFirst { + case ref @ RefInstancePredicate(decl) if ref.name == name => decl + } case _ => None } diff --git a/examples/archive/chalice/ListIterator.java b/examples/archive/chalice/ListIterator.java index cc3774bcb2..fa62d65dd6 100644 --- a/examples/archive/chalice/ListIterator.java +++ b/examples/archive/chalice/ListIterator.java @@ -8,278 +8,251 @@ // Example disabled because it must be rewritten. /** - - The command line to verify with the VerCors Tool is: - - vct --chalice ListIterator.java - - The expected result is Pass. - - Note that depending on which version of chalice is used, - this spec may take a very very long time to check. -*/ + + The command line to verify with the VerCors Tool is: + + vct --chalice ListIterator.java + + The expected result is Pass. + + Note that depending on which version of chalice is used, + this spec may take a very very long time to check. + */ public class ListIterator { /*@ - resource ready()= - Value(iteratee) ** iteratee!=null **Perm(iteratee.sentinel,100) ** iteratee.sentinel!=null - **Perm(current,100)**Perm(last,100)**current!=null - **Perm(current.val,100)**Perm(current.next,100)**Perm(current.prev,100) - **(current.prev==null ==> current==iteratee.sentinel) - **(current.prev!=null ==> current.prev.reverse() ** current.prev.first()==iteratee.sentinel ** current.prev.rev_next()==current) - **current.next->state(); - resource readyForNext()= - Value(iteratee) ** iteratee!=null **Perm(iteratee.sentinel,100) ** iteratee.sentinel!=null - **Perm(current,100)**Perm(last,100)**current!=null - **Perm(current.val,100)**Perm(current.next,100)**Perm(current.prev,100) - **(current.prev==null ==> current==iteratee.sentinel) - **(current.prev!=null ==> current.prev.reverse() ** current.prev.first()==iteratee.sentinel ** current.prev.rev_next()==current) - **current.next->state()**current.next!=null; - resource readyForRemove()= - Value(iteratee) ** iteratee!=null **Perm(iteratee.sentinel,100) ** iteratee.sentinel!=null - **Perm(current,100)**Perm(last,100)**current!=null - **Perm(current.val,100)**Perm(current.next,100)**Perm(current.prev,100) - **current.next->state()**current.prev==last - **last!=null**Perm(last.val,100)**Perm(last.next,100)**Perm(last.prev,100) - **(last.prev==null ==> last==iteratee.sentinel) - **(last.prev!=null ==> last.prev.reverse() ** last.prev.first()==iteratee.sentinel ** last.prev.rev_next()==last) - **last.next==current; - @*/ - - List iteratee; - Node current; - Node last; - - /*@ - requires l!=null ** l.state(); - ensures ready(); - ensures wand:(ready() -* l.state()); + resource ready() = + Value(iteratee) ** iteratee!=null ** Perm(iteratee.sentinel, write) ** iteratee.sentinel!=null + **Perm(current, write) ** Perm(last, write) ** current!=null + **Perm(current.val, write) ** Perm(current.next, write) ** Perm(current.prev, write) + **(current.prev == null ==> current == iteratee.sentinel) + **(current.prev != null ==> current.prev.reverse() ** current.prev.first()==iteratee.sentinel + ** current.prev.rev_next()==current) ** current.next?.state(); + + resource readyForNext() = + Value(iteratee) ** iteratee!=null ** Perm(iteratee.sentinel, write) ** iteratee.sentinel != null + ** Perm(current, write) ** Perm(last, write) ** current != null + ** Perm(current.val, write) ** Perm(current.next, write) ** Perm(current.prev, write) + ** (current.prev == null ==> current == iteratee.sentinel) + ** (current.prev != null ==> current.prev.reverse() ** current.prev.first() == iteratee.sentinel + ** current.prev.rev_next() == current) ** current.next?.state() ** current.next != null; + + resource readyForRemove() = + Value(iteratee) ** iteratee!=null **Perm(iteratee.sentinel, write) ** iteratee.sentinel != null + ** Perm(current, write) ** Perm(last, write) ** current != null + ** Perm(current.val, write) ** Perm(current.next, write) ** Perm(current.prev, write) + ** current.next?.state() ** current.prev == last + ** last != null ** Perm(last.val, write) ** Perm(last.next, write) ** Perm(last.prev, write) + ** (last.prev == null ==> last == iteratee.sentinel) + ** (last.prev != null ==> last.prev.reverse() ** last.prev.first() == iteratee.sentinel + ** last.prev.rev_next() == last) ** last.next == current; @*/ - public ListIterator(List l){ - //@ unfold l.state(); - current=l.sentinel; - //@ unfold current.state(); - current.prev=null; - iteratee=l; - //@ fold ready(); + + List iteratee; + Node current; + Node last; + /*@ - create wand:(ready() -* l.state()){ - use Value(this.iteratee); - use this.iteratee==l; - unfold ready(); - fold this.current.state(); - if (this.current.get_prev()!=null){ - this.current.get_prev().swap(this.iteratee.sentinel,this.current); - } - fold l.state(); - } + requires l != null ** l.state(); + ensures ready(); + ensures ready() -* l.state(); @*/ - } + public ListIterator(List l){ + //@ unfold l.state(); + current = l.sentinel; + //@ unfold current.state(); + current.prev = null; + iteratee = l; + //@ fold ready(); + /*@ package ready() -* l.state() { + unfold ready(); + fold this.current.state(); + if (this.current.get_prev() != null) { + this.current.get_prev().swap(this.iteratee.sentinel, this.current); + } + fold l.state(); + } @*/ + } - /*@ - requires ready(); - ensures \result ==> readyForNext(); - ensures !\result ==> ready(); - @*/ - boolean hasNext(){ - //@ unfold ready(); - boolean res=current.next!=null; /*@ - if(!res) { + requires ready(); + ensures \result ==> readyForNext(); + ensures !\result ==> ready(); + @*/ + boolean hasNext(){ + //@ unfold ready(); + boolean res=current.next!=null; + /*@ ghost if (!res) { fold ready(); - } else { + } + else { fold readyForNext(); } @*/ - return res; - } - - /*@ - requires readyForNext(); - ensures readyForRemove(); - ensures wand:(readyForRemove() -* ready()); - @*/ - int next(){ - int res; - //@ unfold readyForNext(); - last=current; - current=current.next; - //@ unfold current.state(); - res=current.val; - current.prev=last; - //@ fold readyForRemove(); + return res; + } + /*@ - create wand:(readyForRemove() -* ready()){ - unfold readyForRemove(); - fold this.current.prev.reverse(); - fold ready(); - } + requires readyForNext(); + ensures readyForRemove(); + ensures readyForRemove() -* ready(); @*/ - return res; - } + int next(){ + int res; + //@ unfold readyForNext(); + last = current; + current = current.next; + //@ unfold current.state(); + res = current.val; + current.prev = last; + //@ fold readyForRemove(); + /*@ package readyForRemove() -* ready() { + unfold readyForRemove(); + fold this.current.prev.reverse(); + fold ready(); + } @*/ + return res; + } - /*@ - requires readyForRemove(); - ensures ready(); - @*/ - void remove(){ - //@ unfold readyForRemove(); - last.next=current.next; - current=last; - //@ fold ready(); - } - - /* @ spec_ignore * / - public static void main(String args[]){ - List l=new List(); - Example e=new Example(); - e.main(l); - }*/ + /*@ + requires readyForRemove(); + ensures ready(); + @*/ + void remove(){ + //@ unfold readyForRemove(); + last.next=current.next; + current=last; + //@ fold ready(); + } } class List { - Node sentinel; - - /*@ - resource state()=Perm(sentinel,100)**sentinel!=null**sentinel.state(); - @*/ + Node sentinel; /*@ - ensures state(); - @*/ - public List(){ - sentinel=new Node(0,null); - //@ fold state(); - } - - /*@ - requires state(); - ensures state(); + resource state() = + Perm(sentinel, write) ** sentinel!=null ** sentinel.state(); @*/ - public void put(int v){ - //@ unfold state(); - //@ unfold sentinel.state(); - sentinel.next=new Node(v,sentinel.next); - //@ fold sentinel.state(); - //@ fold state(); - } - - /* @ spec_ignore * / - void print(){ - ListIterator i=new ListIterator(this); - System.out.printf("["); - while(i.hasNext()){ - System.out.printf(" %d",i.next()); + + /*@ + ensures state(); + @*/ + public List(){ + sentinel=new Node(0,null); + //@ fold state(); + } + + /*@ + requires state(); + ensures state(); + @*/ + public void put(int v){ + //@ unfold state(); + //@ unfold sentinel.state(); + sentinel.next=new Node(v,sentinel.next); + //@ fold sentinel.state(); + //@ fold state(); } - System.out.printf(" ]%n"); - }*/ } class Example { - /*@ - requires l!=null ** l.state(); - ensures l!=null ** l.state(); - @*/ - void main(List l){ - boolean b; - l.put(1); - l.put(0); - l.put(-1); - /* @ spec_ignore * / l.print();*/ - ListIterator i; - //@ witness recover:(i.ready() -* l.state()); - //@ witness keep:(i.readyForRemove() -* i.ready()); - i=new ListIterator(l) /*@ then { recover = wand; } */; - b=i.hasNext(); + /*@ + requires l!=null ** l.state(); + ensures l!=null ** l.state(); + @*/ + void main(List l){ + boolean b; + l.put(1); + l.put(0); + l.put(-1); + ListIterator i; + i=new ListIterator(l); + b=i.hasNext(); /*@ loop_invariant b ==> i.readyForNext(); loop_invariant !b ==> i.ready(); @*/ - while(b){ - int tmp=i.next() /*@ then { keep = wand ;} */; - if (tmp<0) { - i.remove(); - } else { - //@ apply keep:(i.readyForRemove() -* i.ready()); - } - b=i.hasNext(); + while(b){ + int tmp=i.next(); + if (tmp<0) { + i.remove(); + } else { + //@ apply i.readyForRemove() -* i.ready(); + } + b=i.hasNext(); + } + //@ apply i.ready() -* l.state(); } - //@ apply recover:(i.ready() -* l.state()); - /* @ spec_ignore * / l.print();*/ - } - + } class Node { - public int val; - public Node prev; - public Node next; + public int val; + public Node prev; + public Node next; /*@ - resource state()=Perm(val,100)**Perm(prev,100)**Perm(next,100)**next->state(); + resource state() = + Perm(val, write) ** Perm(prev, write) ** Perm(next, write) ** next?.state(); - resource reverse()=Perm(val,100)**Perm(prev,100)**Perm(next,100)** + resource reverse() = + Perm(val, write) ** Perm(prev, write) ** Perm(next, write) ** (prev!=null ==> prev.reverse() ** prev.rev_next()==this); @*/ /*@ requires state(); - pure Node get_next()=next; + pure Node get_next() = next; @*/ /*@ requires state(); - pure Node get_prev()=prev; + pure Node get_prev() = prev; @*/ /*@ requires reverse(); - pure Node rev_next()=next; + pure Node rev_next() = next; @*/ /*@ requires reverse(); - pure Node rev_prev()=prev; + pure Node rev_prev() = prev; @*/ /*@ requires reverse(); - pure Node first()=(prev==null)?this:(prev.first()); + pure Node first() = prev==null ? this : prev.first(); @*/ - - /*@ - requires n->state(); - ensures state() ** get_next()==n; - @*/ - Node(int v,Node n){ - val=v; - next=n; - //@fold state(); - } - /*@ - requires fst!=null ** reverse() ** rev_next()==nxt ** nxt->state() ** first()==fst; - ensures fst!=null ** fst.state(); - @*/ - void swap(Node fst,Node nxt){ - //@ unfold reverse(); - if (prev==null) { - //@ fold state(); - } else { - // Chalice cannot prove this simple fact: - // assert prev.first()==fst; - // So we assume it - //@ assume prev.first()==fst; - Node tmp=prev; - //@ fold state(); - tmp.swap(fst,this); + /*@ + requires n?.state(); + ensures state() ** get_next()==n; + @*/ + Node(int v, Node n){ + val=v; + next=n; + //@ fold state(); + } + + /*@ + requires fst!=null ** reverse() ** rev_next() == nxt ** nxt->state() ** first() == fst; + ensures fst!=null ** fst.state(); + @*/ + void swap(Node fst,Node nxt){ + //@ unfold reverse(); + if (prev==null) { + //@ fold state(); + } else { + Node tmp=prev; + //@ fold state(); + tmp.swap(fst,this); + } } - } - } diff --git a/parsers/lib/antlr4/LangCLexer.g4 b/parsers/lib/antlr4/LangCLexer.g4 index 1b1fc6a8ae..ad7a04e181 100644 --- a/parsers/lib/antlr4/LangCLexer.g4 +++ b/parsers/lib/antlr4/LangCLexer.g4 @@ -16,6 +16,7 @@ VAL_ASSERT: 'assert'; VAL_TRUE: 'true'; VAL_FALSE: 'false'; VAL_SIZEOF: EOF EOF; +VAL_PACKAGE: 'package'; Placeholder : EOF EOF ; diff --git a/parsers/lib/antlr4/LangPVLLexer.g4 b/parsers/lib/antlr4/LangPVLLexer.g4 index d5739e014b..601647d3c8 100644 --- a/parsers/lib/antlr4/LangPVLLexer.g4 +++ b/parsers/lib/antlr4/LangPVLLexer.g4 @@ -7,6 +7,7 @@ channels { VAL_INLINE: 'inline'; VAL_ASSERT: 'assert'; +VAL_PACKAGE: 'package'; PAREN_OPEN: '('; PAREN_CLOSE: ')'; diff --git a/parsers/lib/antlr4/SpecLexer.g4 b/parsers/lib/antlr4/SpecLexer.g4 index 5161ec56a0..c6b442c047 100644 --- a/parsers/lib/antlr4/SpecLexer.g4 +++ b/parsers/lib/antlr4/SpecLexer.g4 @@ -25,6 +25,7 @@ VAL_INLINE: 'inline'; VAL_ASSERT: 'assert'; VAL_TRUE: 'true'; VAL_FALSE: 'false'; +VAL_PACKAGE: 'package'; */ // Must be able to contain identifiers from any frontend, so it's fine to over-approximate valid identifiers a bit. @@ -73,10 +74,7 @@ VAL_LOCK_INVARIANT: 'lock_invariant'; VAL_SIGNALS: 'signals'; VAL_DECREASES: 'decreases'; -VAL_CREATE: 'create_wand'; -VAL_QED: 'qed'; VAL_APPLY: 'apply'; -VAL_USE: 'use'; VAL_FOLD: 'fold'; VAL_UNFOLD: 'unfold'; VAL_OPEN: 'open'; diff --git a/parsers/lib/antlr4/SpecParser.g4 b/parsers/lib/antlr4/SpecParser.g4 index e84b5dec73..fce5ea10a9 100644 --- a/parsers/lib/antlr4/SpecParser.g4 +++ b/parsers/lib/antlr4/SpecParser.g4 @@ -63,10 +63,8 @@ valBlock ; valStatement - : 'create_wand' valBlock # valCreateWand - | 'qed' langExpr ';' # valQedWand + : 'package' langExpr langStatement # valPackage | 'apply' langExpr ';' # valApplyWand - | 'use' langExpr ';' # valUseWand | 'fold' langExpr ';' # valFold | 'unfold' langExpr ';' # valUnfold | 'open' langExpr ';' # valOpen diff --git a/parsers/src/main/java/vct/parsers/transform/CToCol.scala b/parsers/src/main/java/vct/parsers/transform/CToCol.scala index 62f65d554e..0089efee7c 100644 --- a/parsers/src/main/java/vct/parsers/transform/CToCol.scala +++ b/parsers/src/main/java/vct/parsers/transform/CToCol.scala @@ -734,10 +734,8 @@ case class CToCol[G](override val originProvider: OriginProvider, override val b } def convert(implicit stat: ValStatementContext): Statement[G] = stat match { - case ValCreateWand(_, block) => WandCreate(convert(block)) - case ValQedWand(_, wand, _) => WandQed(convert(wand)) - case ValApplyWand(_, wand, _) => WandApply(convert(wand)) - case ValUseWand(_, wand, _) => WandUse(convert(wand)) + case ValPackage(_, expr, innerStat) => WandPackage(convert(expr), convert(innerStat))(blame(stat)) + case ValApplyWand(_, wand, _) => WandApply(convert(wand))(blame(stat)) case ValFold(_, predicate, _) => Fold(convert(predicate))(blame(stat)) case ValUnfold(_, predicate, _) => diff --git a/parsers/src/main/java/vct/parsers/transform/JavaToCol.scala b/parsers/src/main/java/vct/parsers/transform/JavaToCol.scala index f8d0cbe889..3860f57a85 100644 --- a/parsers/src/main/java/vct/parsers/transform/JavaToCol.scala +++ b/parsers/src/main/java/vct/parsers/transform/JavaToCol.scala @@ -975,10 +975,8 @@ case class JavaToCol[G](override val originProvider: OriginProvider, override va } def convert(implicit stat: ValStatementContext): Statement[G] = stat match { - case ValCreateWand(_, block) => WandCreate(convert(block)) - case ValQedWand(_, wand, _) => WandQed(convert(wand)) - case ValApplyWand(_, wand, _) => WandApply(convert(wand)) - case ValUseWand(_, wand, _) => WandUse(convert(wand)) + case ValPackage(_, expr, innerStat) => WandPackage(convert(expr), convert(innerStat))(blame(stat)) + case ValApplyWand(_, wand, _) => WandApply(convert(wand))(blame(stat)) case ValFold(_, predicate, _) => Fold(convert(predicate))(blame(stat)) case ValUnfold(_, predicate, _) => diff --git a/parsers/src/main/java/vct/parsers/transform/PVLToCol.scala b/parsers/src/main/java/vct/parsers/transform/PVLToCol.scala index 19f749337d..34d7df8cf8 100644 --- a/parsers/src/main/java/vct/parsers/transform/PVLToCol.scala +++ b/parsers/src/main/java/vct/parsers/transform/PVLToCol.scala @@ -721,10 +721,8 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val } def convert(implicit stat: ValStatementContext): Statement[G] = stat match { - case ValCreateWand(_, block) => WandCreate(convert(block)) - case ValQedWand(_, wand, _) => WandQed(convert(wand)) - case ValApplyWand(_, wand, _) => WandApply(convert(wand)) - case ValUseWand(_, wand, _) => WandUse(convert(wand)) + case ValPackage(_, expr, innerStat) => WandPackage(convert(expr), convert(innerStat))(blame(stat)) + case ValApplyWand(_, wand, _) => WandApply(convert(wand))(blame(stat)) case ValFold(_, predicate, _) => Fold(convert(predicate))(blame(stat)) case ValUnfold(_, predicate, _) => diff --git a/src/main/java/vct/col/newrewrite/PrettifyBlocks.scala b/src/main/java/vct/col/newrewrite/PrettifyBlocks.scala index 2fce8e4fdb..688e078035 100644 --- a/src/main/java/vct/col/newrewrite/PrettifyBlocks.scala +++ b/src/main/java/vct/col/newrewrite/PrettifyBlocks.scala @@ -49,6 +49,9 @@ case class PrettifyBlocks[Pre <: Generation]() extends Rewriter[Pre] { case act: ModelDo[Pre] => act.rewrite(impl = collectVariables(act.impl)) + case pack: WandPackage[Pre] => + pack.rewrite(proof = collectVariables(pack.proof)) + case other => rewriteDefault(other) } diff --git a/src/main/java/vct/col/newrewrite/ResolveExpressionSideEffects.scala b/src/main/java/vct/col/newrewrite/ResolveExpressionSideEffects.scala index 0976a0a2e8..daafc48bed 100644 --- a/src/main/java/vct/col/newrewrite/ResolveExpressionSideEffects.scala +++ b/src/main/java/vct/col/newrewrite/ResolveExpressionSideEffects.scala @@ -249,10 +249,8 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() extends Rewriter[Pr case unlock @ Unlock(obj) => frame(obj, Unlock(_)(unlock.blame)) case fold: Fold[Pre] => rewriteDefault(fold) case unfold: Unfold[Pre] => rewriteDefault(unfold) - case create: WandCreate[Pre] => rewriteDefault(create) - case qed: WandQed[Pre] => rewriteDefault(qed) + case create: WandPackage[Pre] => rewriteDefault(create) case apply: WandApply[Pre] => rewriteDefault(apply) - case use: WandUse[Pre] => rewriteDefault(use) case modelDo: ModelDo[Pre] => rewriteDefault(modelDo) case havoc: Havoc[Pre] => rewriteDefault(havoc) // PB: pretty sure you can only havoc locals? case break: Break[Pre] => rewriteDefault(break) diff --git a/src/main/java/vct/main/stages/Transformation.scala b/src/main/java/vct/main/stages/Transformation.scala index a2b2728bdd..9eeea40ede 100644 --- a/src/main/java/vct/main/stages/Transformation.scala +++ b/src/main/java/vct/main/stages/Transformation.scala @@ -74,7 +74,6 @@ class Transformation val tempUnsupported = Set[feature.Feature]( feature.MatrixVector, feature.NumericReductionOperator, - feature.MagicWand, feature.Models, ) diff --git a/viper/src/main/java/viper/api/ColToSilver.scala b/viper/src/main/java/viper/api/ColToSilver.scala index 4330810ad2..eb4c8b257c 100644 --- a/viper/src/main/java/viper/api/ColToSilver.scala +++ b/viper/src/main/java/viper/api/ColToSilver.scala @@ -275,6 +275,7 @@ case class ColToSilver(program: col.Program[_]) { val silver = pred(res) silver.perm.info.asInstanceOf[NodeInfo[_]].permissionValuePermissionNode = Some(res) silver + case col.Wand(left, right) => silver.MagicWand(exp(left), exp(right))(pos = pos(e), info=expInfo(e)) case col.SilverCurPredPerm(p, args) => silver.CurrentPerm(silver.PredicateAccess(args.map(exp), ref(p))(pos=pos(e), info=expInfo(e)))(pos=pos(e), info=expInfo(e)) case col.SilverCurFieldPerm(obj, field) => silver.CurrentPerm(silver.FieldAccess(exp(obj), fields(field.decl))(pos=pos(e), info=expInfo(e)))(pos=pos(e), info=expInfo(e)) case col.Local(v) => silver.LocalVar(ref(v), typ(v.decl.t))(pos=pos(e), info=expInfo(e)) @@ -392,6 +393,16 @@ case class ColToSilver(program: col.Program[_]) { case col.Fold(p: col.PredicateApply[_]) => silver.Fold(pred(p))(pos=pos(s), info=NodeInfo(s)) case col.Unfold(p: col.PredicateApply[_]) => silver.Unfold(pred(p))(pos=pos(s), info=NodeInfo(s)) case col.SilverNewRef(v, fs) => silver.NewStmt(silver.LocalVar(ref(v), typ(v.decl.t))(), fs.map(ref => fields(ref.decl)))(pos=pos(s), info=NodeInfo(s)) + case col.WandPackage(wand @ col.Wand(left, right), proof) => + silver.Package( + silver.MagicWand(exp(left), exp(right))(pos = pos(wand), info=NodeInfo(wand)), stat(proof) match { + // ugly hack to fix scoping issue in viper + case seqn: silver.Seqn => seqn + case other => silver.Seqn(Seq(other), Nil)(pos = pos(proof), info=NodeInfo(proof)) + } + )(pos = pos(s), info=NodeInfo(s)) + case col.WandApply(wand @ col.Wand(left, right)) => + silver.Apply(silver.MagicWand(exp(left), exp(right))(pos = pos(wand), info=NodeInfo(wand)))(pos = pos(s), info=NodeInfo(s)) case other => ??(other) } diff --git a/viper/src/main/java/viper/api/SilverBackend.scala b/viper/src/main/java/viper/api/SilverBackend.scala index cf340871f8..b6ea237417 100644 --- a/viper/src/main/java/viper/api/SilverBackend.scala +++ b/viper/src/main/java/viper/api/SilverBackend.scala @@ -198,9 +198,35 @@ trait SilverBackend extends Backend with LazyLogging { case TerminationFailed(_, _, _) => throw NotSupported(s"Vercors does not support termination measures from Viper") case PackageFailed(node, reason, _) => - throw NotSupported(s"Vercors does not support magic wands from Viper") + val packageNode = get[col.WandPackage[_]](node) + reason match { + case reasons.AssertionFalse(_) | reasons.NegativePermission(_) => + packageNode.blame.blame(blame.PackageFailed(getFailure(reason), packageNode)) + case reasons.InsufficientPermission(permNode) => + get[col.Node[_]](permNode) match { + case col.Perm(_, _) | col.PredicateApply(_, _, _) => + packageNode.blame.blame(blame.PackageFailed(getFailure(reason), packageNode)) + case _ => + defer(reason) + } + case _ => + defer(reason) + } case ApplyFailed(node, reason, _) => - throw NotSupported(s"Vercors does not support magic wands from Viper") + val applyNode = get[col.WandApply[_]](node) + reason match { + case reasons.AssertionFalse(_) | reasons.NegativePermission(_) => + applyNode.blame.blame(blame.WandApplyFailed(getFailure(reason),applyNode)) // take the blame + case reasons.InsufficientPermission(permNode) => + get[col.Node[_]](permNode) match { + case col.Perm(_, _) | col.PredicateApply(_, _, _) => + applyNode.blame.blame(blame.WandApplyFailed(getFailure(reason),applyNode)) // take the blame + case _ => + defer(reason) + } + case _ => + defer(reason) + } case MagicWandNotWellformed(_, _, _) => throw NotSupported(s"Vercors does not support magic wands from Viper") case LetWandFailed(_, _, _) => From 67562f90cd43b2931393346cbddb6cc3f707649a Mon Sep 17 00:00:00 2001 From: naum_tomov Date: Tue, 5 Jul 2022 17:46:24 +0200 Subject: [PATCH 2/2] added some test, gave up on making ListIterator.java example work for now, due to limitations of using footprint added some errors to accommodate exceptions in package proof blocks the test for conditional footprint fails when using carbon, which is very interesting, kept it as silicon only for now --- col/src/main/java/vct/col/ast/Node.scala | 2 +- col/src/main/java/vct/col/origin/Blame.scala | 8 +- examples/archive/chalice/ListIterator.java | 12 +-- .../exc/EncodeTryThrowSignals.scala | 71 +++++++++++++-- .../integration/features/MagicWandSpec.scala | 91 +++++++++++++++++++ .../main/java/viper/api/SilverBackend.scala | 2 + 6 files changed, 170 insertions(+), 16 deletions(-) create mode 100644 src/test/scala/vct/test/integration/features/MagicWandSpec.scala diff --git a/col/src/main/java/vct/col/ast/Node.scala b/col/src/main/java/vct/col/ast/Node.scala index 949b4161a2..936f40bcc9 100644 --- a/col/src/main/java/vct/col/ast/Node.scala +++ b/col/src/main/java/vct/col/ast/Node.scala @@ -194,7 +194,7 @@ final case class ParAtomic[G](inv: Seq[Ref[G, ParInvariantDecl[G]]], content: St final case class ParBarrier[G](block: Ref[G, ParBlockDecl[G]], invs: Seq[Ref[G, ParInvariantDecl[G]]], requires: Expr[G], ensures: Expr[G], content: Statement[G])(val blame: Blame[ParBarrierFailed])(implicit val o: Origin) extends CompositeStatement[G] with ParBarrierImpl[G] final case class ParStatement[G](impl: ParRegion[G])(implicit val o: Origin) extends CompositeStatement[G] with ParStatementImpl[G] final case class VecBlock[G](iters: Seq[IterVariable[G]], requires: Expr[G], ensures: Expr[G], content: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with VecBlockImpl[G] -final case class WandPackage[G](res: Expr[G], proof: Statement[G])(val blame: Blame[PackageFailed])(implicit val o: Origin) extends CompositeStatement[G] with WandCreateImpl[G] +final case class WandPackage[G](res: Expr[G], proof: Statement[G])(val blame: Blame[PackageFailure])(implicit val o: Origin) extends CompositeStatement[G] with WandCreateImpl[G] final case class ModelDo[G](model: Expr[G], perm: Expr[G], after: Expr[G], action: Expr[G], impl: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with ModelDoImpl[G] sealed abstract class Declaration[G] extends Node[G] with DeclarationImpl[G] { diff --git a/col/src/main/java/vct/col/origin/Blame.scala b/col/src/main/java/vct/col/origin/Blame.scala index 999aeb6ddf..83c08d794b 100644 --- a/col/src/main/java/vct/col/origin/Blame.scala +++ b/col/src/main/java/vct/col/origin/Blame.scala @@ -147,7 +147,13 @@ case class FoldFailed(failure: ContractFailure, node: Fold[_]) extends WithContr override def descInContext: String = "Fold may fail, since" override def inlineDescWithSource(node: String, failure: String): String = s"`$node` may fail, since $failure." } -case class PackageFailed(failure: ContractFailure, node: WandPackage[_]) extends WithContractFailure { +trait PackageFailure extends VerificationFailure +case class PackageThrows(node: WandPackage[_]) extends PackageFailure with NodeVerificationFailure { + override def code: String = "packageThrows" + override def descInContext: String = "Package proof may throw an exception" + override def inlineDescWithSource(source: String): String = s"`$node` may throw an exception." +} +case class PackageFailed(failure: ContractFailure, node: WandPackage[_]) extends PackageFailure with WithContractFailure { override def baseCode: String = "packageFailed" override def descInContext: String = "Package statement may fail, since" override def inlineDescWithSource(node: String, failure: String): String = s"`$node` may fail, since $failure." diff --git a/examples/archive/chalice/ListIterator.java b/examples/archive/chalice/ListIterator.java index fa62d65dd6..38c0d9941a 100644 --- a/examples/archive/chalice/ListIterator.java +++ b/examples/archive/chalice/ListIterator.java @@ -203,30 +203,30 @@ resource state() = resource reverse() = Perm(val, write) ** Perm(prev, write) ** Perm(next, write) ** - (prev!=null ==> prev.reverse() ** prev.rev_next()==this); + (prev != null ==> prev.reverse() ** prev.rev_next() == this); @*/ /*@ requires state(); - pure Node get_next() = next; + pure Node get_next() = \unfolding state() \in next; @*/ /*@ requires state(); - pure Node get_prev() = prev; + pure Node get_prev() = \unfolding state() \in prev; @*/ /*@ requires reverse(); - pure Node rev_next() = next; + pure Node rev_next() = \unfolding reverse() \in next; @*/ /*@ requires reverse(); - pure Node rev_prev() = prev; + pure Node rev_prev() = \unfolding reverse() \in prev; @*/ /*@ requires reverse(); - pure Node first() = prev==null ? this : prev.first(); + pure Node first() = \unfolding reverse() \in (prev==null ? this : prev.first()); @*/ diff --git a/src/main/java/vct/col/newrewrite/exc/EncodeTryThrowSignals.scala b/src/main/java/vct/col/newrewrite/exc/EncodeTryThrowSignals.scala index 29415099d3..d8950c6f65 100644 --- a/src/main/java/vct/col/newrewrite/exc/EncodeTryThrowSignals.scala +++ b/src/main/java/vct/col/newrewrite/exc/EncodeTryThrowSignals.scala @@ -14,6 +14,7 @@ import scala.collection.mutable case object EncodeTryThrowSignals extends RewriterBuilder { override def key: String = "tryThrowSignals" + override def desc: String = "Encode try, throw and signals specifications to goto, exception out-parameters and regular postconditions." case class ThrowNullAssertFailed(t: Throw[_]) extends Blame[AssertFailed] { @@ -21,45 +22,67 @@ case object EncodeTryThrowSignals extends RewriterBuilder { t.blame.blame(ThrowNull(t)) } + case class PackageThrowsAssertFailed(pack: WandPackage[_]) extends Blame[AssertFailed] { + override def blame(error: AssertFailed): Unit = pack.blame.blame(PackageThrows(pack)) + } + case object ExcVar extends Origin { override def preferredName: String = "exc" + override def shortPosition: String = "generated" + override def context: String = "[At variable generated to contain thrown exception]" + override def inlineContext: String = "[Current exception]" } case object CurrentlyHandling extends Origin { override def preferredName: String = "currently_handling_exc" + override def shortPosition: String = "generated" + override def context: String = "[At variable generated to remember exception currently being handled]" + override def inlineContext: String = "[Exception currently being handled]" } case object ReturnPoint extends Origin { override def preferredName: String = "bubble" + override def shortPosition: String = "generated" + override def context: String = "[At label generated to bubble an exception]" + override def inlineContext: String = "[Exception bubble label]" } case object CatchLabel extends Origin { override def preferredName: String = "catches" + override def shortPosition: String = "generated" + override def context: String = "[At label generated for catch blocks]" + override def inlineContext: String = "[Catch label]" } case object FinallyLabel extends Origin { override def preferredName: String = "finally" + override def shortPosition: String = "generated" + override def context: String = "[At label generated for finally]" + override def inlineContext: String = "[Finally label]" } case object ExcBeforeLoop extends Origin { override def preferredName: String = "excBeforeLoop" + override def shortPosition: String = "generated" + override def context: String = "[At variable generated to contain exc before loop]" + override def inlineContext: String = "[Exception before loop]" } @@ -75,12 +98,14 @@ case object EncodeTryThrowSignals extends RewriterBuilder { } case class EncodeTryThrowSignals[Pre <: Generation]() extends Rewriter[Pre] { + import EncodeTryThrowSignals._ val currentException: ScopedStack[Variable[Post]] = ScopedStack() val exceptionalHandlerEntry: ScopedStack[LabelDecl[Post]] = ScopedStack() val returnHandler: ScopedStack[LabelDecl[Post]] = ScopedStack() + val needCurrentExceptionRestoration: ScopedStack[Boolean] = ScopedStack() needCurrentExceptionRestoration.push(false) @@ -116,7 +141,9 @@ case class EncodeTryThrowSignals[Pre <: Generation]() extends Rewriter[Pre] { val catchImpl = Block[Post](catches.map { case CatchClause(decl, body) => - val typedExc = collectOneInScope(variableScopes) { dispatch(decl) } + val typedExc = collectOneInScope(variableScopes) { + dispatch(decl) + } Scope(Seq(typedExc), Branch(Seq(( (getExc !== Null[Post]()) && InstanceOf(getExc, TypeValue(dispatch(decl.t))), Block(Seq( @@ -128,19 +155,21 @@ case class EncodeTryThrowSignals[Pre <: Generation]() extends Rewriter[Pre] { } }, ), - ))))) + ))))) }) val finallyImpl = Block[Post](Seq( Label(finallyEntry, Block(Nil)), - needCurrentExceptionRestoration.having(true) { dispatch(after) }, + needCurrentExceptionRestoration.having(true) { + dispatch(after) + }, Branch(Seq(( getExc !== Null(), Goto(exceptionalHandlerEntry.top.ref), ))), )) - val (store: Statement[Post], restore: Statement[Post], vars: Seq[Variable[Post]]) = if(needCurrentExceptionRestoration.top) { + val (store: Statement[Post], restore: Statement[Post], vars: Seq[Variable[Post]]) = if (needCurrentExceptionRestoration.top) { val tmp = new Variable[Post](TClass(rootClass.top))(CurrentlyHandling) ( Block[Post](Seq( @@ -161,7 +190,7 @@ case class EncodeTryThrowSignals[Pre <: Generation]() extends Rewriter[Pre] { restore, ))) - case t @ Throw(obj) => + case t@Throw(obj) => Block(Seq( assignLocal(getExc, dispatch(obj)), Assert(getExc !== Null())(ThrowNullAssertFailed(t)), @@ -192,12 +221,33 @@ case class EncodeTryThrowSignals[Pre <: Generation]() extends Rewriter[Pre] { Scope(Seq(beforeLoop), Block[Post](Seq( assignLocal(beforeLoop.get, getExc), loop.rewrite(contract = loop.contract match { - case inv @ LoopInvariant(invariant) => + case inv@LoopInvariant(invariant) => LoopInvariant(getExc === beforeLoop.get &* dispatch(invariant))(inv.blame) case it: IterationContract[Pre] => rewriteDefault(it) }) ))) + case w@WandPackage(wand, proof) => + val exc = new Variable[Post](TClass(rootClass.top))(ExcVar) + val labelHandler = new LabelDecl[Post]() + val labelDone = new LabelDecl[Post]() + exceptionalHandlerEntry.having(labelHandler) { + currentException.having(exc) { + WandPackage(dispatch(wand), + Scope(Seq(exc), + Block( + Seq( + dispatch(proof), + Goto[Post](labelDone.ref), + Label(labelHandler, Block(Nil)), + Assert[Post](BooleanValue(false))(PackageThrowsAssertFailed(w)), + Label(labelDone, Block(Nil)), + )) + ) + )(w.blame) + } + } + case other => rewriteDefault(other) } } @@ -240,7 +290,9 @@ case class EncodeTryThrowSignals[Pre <: Generation]() extends Rewriter[Pre] { case SignalsClause(binding, assn) => binding.drop() ((exc.get !== Null()) && InstanceOf(exc.get, TypeValue(dispatch(binding.t)))) ==> - signalsBinding.having((binding, exc.get)) { dispatch(assn) } + signalsBinding.having((binding, exc.get)) { + dispatch(assn) + } })), ), ) @@ -254,7 +306,10 @@ case class EncodeTryThrowSignals[Pre <: Generation]() extends Rewriter[Pre] { ), ), body = body, - outArgs = collectInScope(variableScopes) { exc.declareDefault(this); method.outArgs.foreach(dispatch) }, + outArgs = collectInScope(variableScopes) { + exc.declareDefault(this); + method.outArgs.foreach(dispatch) + }, contract = method.contract.rewrite(ensures = ensures, signals = Nil), ).succeedDefault(method) } diff --git a/src/test/scala/vct/test/integration/features/MagicWandSpec.scala b/src/test/scala/vct/test/integration/features/MagicWandSpec.scala new file mode 100644 index 0000000000..c85309ea01 --- /dev/null +++ b/src/test/scala/vct/test/integration/features/MagicWandSpec.scala @@ -0,0 +1,91 @@ +package vct.test.integration.features + +import vct.test.integration.helper.VercorsSpec + +class MagicWandSpec extends VercorsSpec { + vercors should verify using anyBackend in "Testing the magic wand feature" pvl + """ + void test() { + Test obj = new Test(); + package Perm(obj.f, write) -* Perm(obj.f, write) {} + assert Perm(obj.f, write); + } + + class Test { + int f; + } + """ + + vercors should verify using anyBackend in "Testing the magic wand feature with footprint" pvl + """ + void test() { + Test obj = new Test(); + Test obj2 = new Test(); + package Perm(obj.f, write) -* Perm(obj2.f, write) ** Perm(obj.f, write) {} + /*[/expect assertFailed:perm]*/ + assert Perm(obj2.f, write); + /*[/end]*/ + } + + class Test { + int f; + } + """ + + vercors should verify using anyBackend in "Testing the magic wand feature with oversight footprint" pvl + """ + void test() { + Test obj = new Test(); + Test obj2; + /*[/expect packageFailed:perm]*/ + package Perm(obj.f, write) -* Perm(obj2.f, write) ** Perm(obj.f, write) {} + /*[/end]*/ + } + + class Test { + int f; + } + """ + + vercors should verify using anyBackend in "Testing you can't throw errors in package block" java + """ + class Test { + + void test() { + /*[/expect packageThrows]*/ + /*@ package true -* true + { + throw new Exception(); + } @*/ + } + /*[/end]*/ + int f; + } + """ + + vercors should verify using anyBackend in "Testing that when applied a wand is exhaustively consumed" pvl + """ + void test () { + package true -* true {} + apply true -* true; + /*[/expect applyFailed:perm]*/ + apply true -* true; + /*[/end]*/ + } + """ + + vercors should verify using silicon in "Testing that conditional footprint works" pvl + """ + void test() { + boolean b; + Test a = new Test(); + package (b ==> Perm(a.a, write)) -* Perm(a.a, write) {} + assert b ==> Perm(a.a, write); + assert !b ==> (perm(a.a) == none); + } + + class Test { + boolean a; + } + """ +} diff --git a/viper/src/main/java/viper/api/SilverBackend.scala b/viper/src/main/java/viper/api/SilverBackend.scala index b6ea237417..19e8a34d85 100644 --- a/viper/src/main/java/viper/api/SilverBackend.scala +++ b/viper/src/main/java/viper/api/SilverBackend.scala @@ -224,6 +224,8 @@ trait SilverBackend extends Backend with LazyLogging { case _ => defer(reason) } + case reasons.MagicWandChunkNotFound(magicWand) => + applyNode.blame.blame(blame.WandApplyFailed(blame.InsufficientPermissionToExhale(get(magicWand)), applyNode)) case _ => defer(reason) }