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

asserting in #455

Closed
wants to merge 8 commits into from
Closed

asserting in #455

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
7e0ef76
Added asserting-in expression
dewert99 May 22, 2022
b7f533b
Extracted super trait HintExp for Unfolding, Applying, and Asserting
dewert99 May 25, 2022
8bd9a7e
Added timeout tests
dewert99 Jun 1, 2022
3d7b8ce
Fixed TimeoutPortableCarbonTests to take repetitions into account
dewert99 Jun 2, 2022
cdd32f1
Made sure processes were destroyed if they timed out
dewert99 Jun 20, 2022
832a4ee
Also kill Boogies children (Z3) on timeout
dewert99 Jun 23, 2022
579aac9
Merge remote-tracking branch 'origin-dewert/master' into benchmark-co…
dewert99 Mar 8, 2023
07a5871
Reverted non asserting changes
dewert99 Mar 14, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion silver
Open in desktop
Copy link
Contributor

Choose a reason for hiding this comment

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

I'm not sure how pull requests work across submodules; could this be a separate pull request for silver?

Copy link
Contributor

Choose a reason for hiding this comment

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

In any case, github doesn't seem to understand how to present the diffs for these files.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I did make two pull requests: see viperproject/silver#660, this pull request references the silver commit in the silver pull request

Submodule silver updated 15 files
+10 −5 src/main/scala/viper/silver/ast/Expression.scala
+2 −0 src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
+1 −2 src/main/scala/viper/silver/ast/utility/Consistency.scala
+1 −2 src/main/scala/viper/silver/ast/utility/Expressions.scala
+1 −0 src/main/scala/viper/silver/ast/utility/Nodes.scala
+5 −2 src/main/scala/viper/silver/parser/FastParser.scala
+8 −0 src/main/scala/viper/silver/parser/ParseAst.scala
+1 −0 src/main/scala/viper/silver/parser/Transformer.scala
+2 −0 src/main/scala/viper/silver/parser/Translator.scala
+7 −8 src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+1 −2 src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
+16 −0 src/test/resources/all/asserting-in/other-fail.vpr
+7 −0 src/test/resources/all/asserting-in/pass.vpr
+15 −0 src/test/resources/all/asserting-in/simple-fail.vpr
+5 −0 src/test/resources/all/asserting-in/wand.vpr
38 changes: 22 additions & 16 deletions src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,33 +6,33 @@

package viper.carbon.modules.impls

import viper.carbon.modules.{ExpModule, StatelessComponent}
import viper.silver.{ast => sil}
import viper.carbon.boogie._
import viper.carbon.verifier.Verifier
import viper.silver.verifier.{PartialVerificationError, reasons}
import viper.carbon.boogie.Implicits._
import viper.carbon.boogie._
import viper.carbon.modules.components.DefinednessComponent
import viper.silver.ast.{LocationAccess, MagicWand, PredicateAccess, Ref}
import viper.carbon.modules.{ExpModule, StatelessComponent}
import viper.carbon.verifier.Verifier
import viper.silver.ast.utility.Expressions
import viper.silver.ast.{LocationAccess, MagicWand, PredicateAccess, Ref}
import viper.silver.verifier.{PartialVerificationError, reasons}
import viper.silver.{ast => sil}

/**
* The default implementation of [[viper.carbon.modules.ExpModule]].
*/
class DefaultExpModule(val verifier: Verifier) extends ExpModule with DefinednessComponent with StatelessComponent {

import verifier._
import heapModule._
import domainModule._
import seqModule._
import setModule._
import exhaleModule._
import funcPredModule._
import heapModule._
import inhaleModule._
import mainModule._
import mapModule._
import permModule._
import inhaleModule._
import funcPredModule._
import exhaleModule._
import seqModule._
import setModule._
import stateModule._
import mainModule._

override def start(): Unit = {
register(this)
Expand Down Expand Up @@ -74,9 +74,7 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
sys.error("should not occur here (either, we inhale or exhale this expression, in which case whenInhaling/whenExhaling should be used, or the expression is not allowed to occur.")
case [email protected](_, _) =>
translateLocationAccess(p)
case sil.Unfolding(_, exp) =>
translateExp(exp)
case sil.Applying(_, exp) => translateExp(exp)
case h: sil.HintExp => translateExp(h.body)
Copy link
Contributor

Choose a reason for hiding this comment

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

This is nice to have. Is HintExp a sealed trait?

case sil.Old(exp) =>
val prevState = stateModule.state
stateModule.replaceState(stateModule.oldState)
Expand Down Expand Up @@ -373,6 +371,14 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
checkDefinednessImpl(e1, error, makeChecks = makeChecks) :: // short-circuiting evaluation:
If(UnExp(Not, translateExp(e1)), checkDefinednessImpl(e2, error, makeChecks = makeChecks), Statements.EmptyStmt) ::
Nil
case sil.Asserting(assertion, e) =>
checkDefinedness(assertion, error, makeChecks = makeChecks) ::
NondetIf(
MaybeComment("Exhale assertion of asserting", exhale(Seq((assertion, error)))) ++
MaybeComment("Stop execution", Assume(FalseLit()))
, Nil) ::
checkDefinedness(e, error, makeChecks = makeChecks) ::
Nil
case [email protected](_, _) =>
checkDefinednessWand(w, error, makeChecks = makeChecks)
case sil.Let(v, e, body) =>
Expand Down