diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 000000000..a9c36098d --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,54 @@ +# Contributing to UCLID5 + +UCLID5 is a relatively new tool and we welcome new contributors who want to get involved. Here are some very minimalistic guidelines on code and pull requests: + + +## CODE: +1. Every new function introduced should be documented, for example like this: +~~~ +/** + * Create new SMT symbolic variables for each state. + * + * This is called after each step of symbolic simulation and prevents the expression + * trees from blowing up. + * + * @param st The symbol table. + * @param step The current frame number. + * @param scope The current scope. + */ + def renameStates(st : SymbolTable, eqStates : Set[Identifier], frameNumber : Int, scope : Scope, addAssumption : (smt.Expr, List[ExprDecorator]) => Unit) : SymbolTable = { +~~~ + +2. Please don’t leave commented out code in the code base if you can avoid it. If it really must stay, add a comment to it saying why it must stay, what it was for and why it was commented out. + +## Pull requests: +1. Each new feature or bug fix should be done on a new branch +2. Create a separate PR for each new feature or bug fix. +3. Where possible break down large new features into separate PRs. +4. Every PR for a new feature should include a set of regression tests that fully test the feature +5. Every PR for a bug fix should include a regression test that tests the fix +6. When you get feedback on a PR, push the changes to the same branch so they appear in the same PR. +7. Write good commit messages: https://blogs.gnome.org/danni/2011/10/25/a-guide-to-writing-git-commit-messages/ +Every commit should have a meaningful commit message, which is less than 72 characters long. If you need more than that, the commit should have a short heading commit message followed by a longer description on a new line. +8. Tidy up your commit history before you PR: use interactive rebase to squash together messy commits into a single meaningful commit with a good commit message. e.g., these two commits should be squashed into one: +~~~ +commit c76ef1e8bbfa1cb06f42dsdd3g02138002bca938 +Author: polgreen +Date: Tue Oct 27 15:12:03 2020 -0700 + + fixes mistake in previous commit + +commit 6502265e4a85688ff92d963419c1957ef3cb73b5 +Author: polgreen +Date: Tue Oct 27 11:18:52 2020 -0700 + + Add array reads to readset + + The redundant assignment eliminator was removing relevant assigns because + it was failing to count array select statements as reads of the index variable, if the array select + happens on the LHS of an assign. Bug exposed by test/test-redundant-assign.ucl +~~~ +9. Preserve bisectability: every commit should compile. If your commit does not compile, use interactive rebase to fix it. +10. Don’t change whitespace unnecessarily. If you are going to change whitespace, then change it in a specific commit with a message that says “white space changes” +11. Don’t change the .gitignore unnecessarily. If you are going to change it, do it in a separate commit with a message that explains why the commit is necessary +12. Delete any branches on the main repo (uclid-org/uclid) as soon as the PR has been merged. If you want to keep branches, do it on your own fork. diff --git a/README.md b/README.md index 0e2e89174..c2f5ed03e 100644 --- a/README.md +++ b/README.md @@ -12,12 +12,14 @@ Sanjit A. Seshia and Pramod Subramanyan. UCLID5: Integrating *Proceedings of the 16th ACM-IEEE International Conference on Formal Methods and Models for System Design*. **(MEMOCODE 2018)**. Beijing, China. October 2018. # Installation -There are currently two ways to install UCLID5: downloading the latest pre-build package and building from source. Please make sure you have all the pre-requisites before proceeding to installation. Due to the nuances in the later Mac OS versions, we prepare separately a compact list of the installation instructions [here](mac-install.md). +There are currently two ways to install UCLID5: [downloading the latest pre-build package](#prebuilt) and [building from source](#srcbuild). Please make sure you have all the pre-requisites before proceeding to installation. Due to the nuances in the later Mac OS versions, we prepare separately a compact list of the installation instructions [here](mac-install.md). -## Pre-requisites +## Pre-requisites -#### 1. [Z3 version 4.6.0.](https://github.com/Z3Prover/z3/releases/tag/z3-4.6.0) -You will need the Z3 SMT solver to be installed on your system. If you are building Z3 from source, make sure the Z3/Java interface is enabled in your build (typically by passing `--java` to the `mk_make.py` script). To install z3 on Unix-like systems, download the source code and run the following: +#### 1. [Z3 version 4.8.8.](https://github.com/Z3Prover/z3/releases/tag/z3-4.8.8) +You will need the Z3 SMT solver to be installed on your system. Earlier versions of Z3 should work, but the CI is tested with version 4.8.8. uclid5 requires that the Z3 dynamic link library (libz3.so on Unix-like platforms) as well as the dynamic link library for the Z3/Java API (libz3java.so on Unix-like platforms) be in your dynamic library path (`$LD_LIBRARY_PATH` on Unix-like platforms; just `PATH` on Windows). If compiling from source, the source repository provides an easy way to set up Z3. See the instructions for [compiling from source](#srcbuild) for details. + +If you prefer to build Z3 from source, make sure the Z3/Java interface is enabled in your build (typically by passing `--java` to the `mk_make.py` script). To install z3 on Unix-like systems from source, download the source code and run the following: ```bash python scripts/mk_make.py --java @@ -26,7 +28,7 @@ make sudo make install ``` -uclid5 requires that the Z3 dynamic link library (libz3.so on Unix-like platforms) as well as the dynamic link library for the Z3/Java API (libz3java.so on Unix-like platforms) be in your dynamic library path (`$LD_LIBRARY_PATH` on Unix-like platforms; just `PATH` on Windows). +Finally copy the jar file `path/to/z3/build/com.microsoft.z3.jar` to the dir `path/to/uclid5/lib/com.microsoft.z3.jar` **If you are using Mac OS X El Capitan or above**, System Integrity Protection is a feature introduced by Apple in OS X El Capitan; it prevents the modifications of system-owned files and directories by any process without a specific ‘entitlement’, even when executed by a root user or a user with root privileges. Since Java is a SIP protected executable, it ignores the user set DYLD_LIBRARY_PATH, which prevents the system from recognizing the Z3 Dynamic Library. @@ -40,34 +42,23 @@ https://github.com/Z3Prover/z3/issues/294 #### 2. [OpenJDK version 8](https://openjdk.java.net/) or [Oracle JDK version 8](https://www.oracle.com/java/technologies/javase/javase-jdk8-downloads.html) **If you are using Mac OS X Mojave or above**, we recommend using Java 11 or earlier. We have found some issues related to the System Integrity Protection when using Catalina or Mojave and later versions of OpenJDK. -#### 3. [SBT version 1.0 or greater.](http://www.scala-sbt.org/1.0/docs/Setup.html) -If you intend to build from source, you need to install sbt. You can skip this step if you are using the pre-build binaries. Install instructions for sbt are available at http://www.scala-sbt.org/1.0/docs/Setup.html - -## Download Pre-Built Binaries +## Download Pre-Built Binaries Download the latest stable pre-built package from [releases tab](https://github.com/uclid-org/uclid/releases). -## Building From Source +## Building From Source Or, you could clone this repository and build from source. If you run into problems here, don't forget you can always fall back on the pre-built binaries linked above. +### Pre-requisites +In addition to the prerequisites mentioned [above](#prereqs), please also note the following if compiling from source: -### Prerequisites -Before you begin, make sure you have the following installed and properly set up: - -#### 1. Z3 version 4.6.0. -Make sure the Z3/Java interface is enabled in your build (typically by passing `--java` to the `mk_make.py` script). +#### 1. Z3 Setup Script -**(Z3 configuration)** uclid5 requires that the Z3 dynamic link library (libz3.so on Unix-like platforms) as well as the dynamic link library for the Z3/Java API (libz3java.so on Unix-like platforms) be in your dynamic library path (`$LD_LIBRARY_PATH` on Unix-like platforms; just `PATH` on Windows). - -Finally copy the jar file `path/to/z3/build/com.microsoft.z3.jar` to the dir `path/to/uclid5/lib/com.microsoft.z3.jar` - -#### 2. OpenJDK version 8 or Oracle JDK version 8 - -#### 3. SBT version 1.0 or greater. - -Install instructions for sbt are available at http://www.scala-sbt.org/1.0/docs/Setup.html +The `get-z3-linux.sh` script in the source repository makes it easy to set up Z3 for use with uclid5. To use the script, simply run `source get-z3-linux.sh` from the root directory of the uclid5 source repository. This script will download Z3 binaries from GitHub and set up your `PATH` and `LD_LIBRARY_PATH` accordingly (it uses `setup-z3-linux.sh` to do the latter). You will need to rerun `setup-z3-linux.sh` (or the commands in it) each time you open a new bash shell, or you can simply source it from your `.profile` or `.bashrc`. +#### 2. [SBT version 1.0 or greater.](http://www.scala-sbt.org/1.0/docs/Setup.html) +If you intend to build from source, you need to install sbt. You can skip this step if you are using the pre-build binaries. Install instructions for sbt are available at http://www.scala-sbt.org/1.0/docs/Setup.html ### Compiling uclid5 diff --git a/src/main/scala/uclid/AssertionTree.scala b/src/main/scala/uclid/AssertionTree.scala index bd78d22c3..ec6a6a249 100644 --- a/src/main/scala/uclid/AssertionTree.scala +++ b/src/main/scala/uclid/AssertionTree.scala @@ -175,10 +175,18 @@ class AssertionTree { solver.curAssertName = e.name solver.curAssertLabel = e.label val sat = solver.check(getModel) - val result = sat.result match { - case Some(true) => smt.SolverResult(Some(false), sat.model) - case Some(false) => smt.SolverResult(Some(true), sat.model) - case None => smt.SolverResult(None, None) + val result = if (e.decorators.contains(SATOnlyDecorator)) { + sat.result match { + case Some(true) => smt.SolverResult(Some(true), sat.model) + case Some(false) => smt.SolverResult(Some(false), sat.model) + case None => smt.SolverResult(None, None) + } + } else { + sat.result match { + case Some(true) => smt.SolverResult(Some(false), sat.model) + case Some(false) => smt.SolverResult(Some(true), sat.model) + case None => smt.SolverResult(None, None) + } } solver.pop() Some(CheckResult(e, result)) diff --git a/src/main/scala/uclid/Hashable.scala b/src/main/scala/uclid/Hashable.scala index 908e13c39..f527fe364 100644 --- a/src/main/scala/uclid/Hashable.scala +++ b/src/main/scala/uclid/Hashable.scala @@ -22,19 +22,43 @@ trait Hashable { md5.reset() md5.update(intToBytes(hashBaseId)) md5.update(intToBytes(hashId)) + md5.update(intToBytes(args.size)) // Recursively compute the md5 hash def computeMD5HashR(a : Any) : Unit = { a match { - case None => computeMD5HashR(0) - case Some(opt) => computeMD5HashR(opt) - case integer : Int => md5.update(intToBytes(integer)) - case str : String => md5.update(str.getBytes("UTF-8")) - case bigint : BigInt => md5.update(bigint.toByteArray) - case bool : Boolean => md5.update(if (bool) intToBytes(1) else intToBytes(0)) - case tuple2 : (Any, Any) => { computeMD5HashR(tuple2._1); computeMD5HashR(tuple2._2); } - case tuple3 : (Any, Any, Any) => { computeMD5HashR(tuple3._1); computeMD5HashR(tuple3._2); computeMD5HashR(tuple3._3) } - case lista : List[Any] => lista.foreach(e => computeMD5HashR(e)) - case hash : Hashable => md5.update(hash.md5hashCode) + case None => + md5.update(intToBytes(111)) + computeMD5HashR(0) + case Some(opt) => + md5.update(intToBytes(112)) + computeMD5HashR(opt) + case integer : Int => + md5.update(intToBytes(113)) + md5.update(intToBytes(integer)) + case str : String => + md5.update(intToBytes(114)) + md5.update(str.getBytes("UTF-8")) + case bigint : BigInt => + md5.update(intToBytes(115)) + md5.update(bigint.toByteArray) + case bool : Boolean => + md5.update(intToBytes(116)) + md5.update(if (bool) intToBytes(1) else intToBytes(0)) + case tuple2 : (Any, Any) => + md5.update(intToBytes(117)) + computeMD5HashR(tuple2._1) + computeMD5HashR(tuple2._2) + case tuple3 : (Any, Any, Any) => + md5.update(intToBytes(118)) + computeMD5HashR(tuple3._1) + computeMD5HashR(tuple3._2) + computeMD5HashR(tuple3._3) + case lista : List[Any] => + md5.update(intToBytes(119)) + md5.update(intToBytes(lista.size)) + lista.foreach(e => computeMD5HashR(e)) + case hash : Hashable => + md5.update(hash.md5hashCode) case _ => { UclidMain.println("Can't convert: " + a.getClass().toString()) throw new Utils.RuntimeError("Should not get here; Missing case!" + a.getClass().toString()) diff --git a/src/main/scala/uclid/SymbolicSimulator.scala b/src/main/scala/uclid/SymbolicSimulator.scala index c09d0b53a..ab97ddd16 100644 --- a/src/main/scala/uclid/SymbolicSimulator.scala +++ b/src/main/scala/uclid/SymbolicSimulator.scala @@ -280,8 +280,8 @@ class SymbolicSimulator (module : Module) { val procName = cmd.args(0)._1.asInstanceOf[Identifier] val proc = module.procedures.find(p => p.id == procName).get val label : String = cmd.resultVar match { - case Some(l) => l.toString + ": verify(%s)".format(procName.toString()) - case None => "verify(%s)".format(procName.toString) + case Some(l) => l.toString + ": verify_%s".format(procName.toString()) + case None => "verify_%s".format(procName.toString) } verifyProcedure(proc, label) case "check" => { @@ -1741,7 +1741,7 @@ class SymbolicSimulator (module : Module) { frameLog.debug("symbolTable: %s".format(symbolTable.toString())) s match { case SkipStmt() => return symbolTable - case AssertStmt(e, id) => + case AssertStmt(e, id, decorators) => val frameTableP = frameTable.clone() frameTableP += symbolTable val simTable = ArrayBuffer(frameTableP) @@ -1753,7 +1753,7 @@ class SymbolicSimulator (module : Module) { val assert = AssertInfo( assertionName, label, simTable.clone(), scope, frameNumber, pathCondExpr, - assertExpr, List.empty, s.position) + assertExpr, decorators, s.position) assertLog.debug("Assertion: {}", e.toString) assertLog.debug("VC: {}", assertExpr.toString) frameLog.debug("FrameTableSize: {}", frameTableP.size) @@ -1829,7 +1829,7 @@ class SymbolicSimulator (module : Module) { def writeSet(stmt: Statement) : Set[Identifier] = stmt match { case SkipStmt() => Set.empty - case AssertStmt(e, id) => Set.empty + case AssertStmt(e, id, _) => Set.empty case AssumeStmt(e, id) => Set.empty case HavocStmt(h) => h match { diff --git a/src/main/scala/uclid/UclidMain.scala b/src/main/scala/uclid/UclidMain.scala index 7a44fac57..cb249bbca 100644 --- a/src/main/scala/uclid/UclidMain.scala +++ b/src/main/scala/uclid/UclidMain.scala @@ -78,7 +78,8 @@ object UclidMain { printStackTrace: Boolean = false, verbose : Int = 0, files : Seq[java.io.File] = Seq(), - testFixedpoint: Boolean = false + testFixedpoint: Boolean = false, + modelCounter: Boolean = false ) def parseOptions(args: Array[String]) : Option[Config] = { @@ -120,6 +121,10 @@ object UclidMain { opt[Unit]('t', "test-fixedpoint").action { (_, c) => c.copy(testFixedpoint = true) }.text("Test fixed point") + + opt[Unit]('C', "model-counter").action { + (_, c) => c.copy(modelCounter = true) + }.text("Model counter DSL.") help("help").text("prints this usage text") @@ -140,6 +145,10 @@ object UclidMain { smt.Z3HornSolver.test1() return } + if (config.modelCounter) { + config.files.foreach(f => extensions.modelcounts.UMCMain.checkModel(f, config)) + return + } val mainModuleName = Identifier(config.mainModuleName) val modules = compile(config.files, mainModuleName) val mainModule = instantiate(config, modules, mainModuleName, true) @@ -239,7 +248,6 @@ object UclidMain { def compile(srcFiles : Seq[java.io.File], mainModuleName : Identifier, test : Boolean = false): List[Module] = { type NameCountMap = Map[Identifier, Int] var nameCnt : NameCountMap = Map().withDefaultValue(0) - val passManager = createCompilePassManager(test, mainModuleName) val filenameAdderPass = new AddFilenameRewriter(None) // Helper function to parse a single file. @@ -252,7 +260,17 @@ object UclidMain { val parsedModules = srcFiles.foldLeft(List.empty[Module]) { (acc, srcFile) => acc ++ parseFile(srcFile.getPath()) } - + compileModules(parsedModules, mainModuleName, test) + } + + /** Compile a list of modules (do everything pre-module-instantiation. */ + def compileModules( + parsedModules : List[Module], + mainModuleName : Identifier, + test : Boolean) : List[Module] = + { + // create a pass manager. + val passManager = createCompilePassManager(test, mainModuleName) // now process each module val init = (List.empty[Module], Scope.empty) // NOTE: The foldLeft/:: combination here reverses the order of modules. diff --git a/src/main/scala/uclid/extensions/modelcounts/UMCLanguage.scala b/src/main/scala/uclid/extensions/modelcounts/UMCLanguage.scala new file mode 100644 index 000000000..b82f370ad --- /dev/null +++ b/src/main/scala/uclid/extensions/modelcounts/UMCLanguage.scala @@ -0,0 +1,638 @@ +/* + * UCLID5 Verification and Synthesis Engine + * + * Copyright (c) 2017. + * Sanjit A. Seshia, Rohit Sinha and Pramod Subramanyan. + * + * All Rights Reserved. + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * 1. Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * + * documentation and/or other materials provided with the distribution. + * 3. Neither the name of the copyright holder nor the names of its + * contributors may be used to endorse or promote products derived from this + * software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, + * THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR + * PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR + * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + * Author: Pramod Subramanyan, Shubham Sahai + * + * Main file for the UCLID model counter. + * + */ +package uclid.extensions.modelcounts + + +import uclid.UclidMain +import uclid.{lang => l} +import uclid.Utils +import uclid.Memo +import uclid.lang.{Identifier, Type} + + +/** CountingOp is a new operator we introduce for the UMC extension. */ +case class CountingOp(xs: List[(l.Identifier, l.Type)], ys: List[(l.Identifier, l.Type)], e : l.Expr) extends l.Expr { + override def toString() = { + val s1 = Utils.join(xs.map(v => v._1.toString() + " : " + v._2.toString()), ", ") + val s2 = if (ys.size > 0) { + val s2 = Utils.join(ys.map(v => v._1.toString() + " : " + v._2.toString()), ", ") + "#[(" + s1 + ") for (" + s2 + ")] :: " + } else { + "#[(" + s1 + ")] :: " + } + s2 + "(" + e.toString() + ")" + } + override val hashId = 1402 + override val md5hashCode = computeMD5Hash(xs, ys) +} + + +/** This is the base class for all the "statements" in the proof. */ +sealed abstract class Statement extends l.ASTNode { + override def toString = Utils.join(toLines, "\n") + "\n" + def toLines : List[String] + val countingOps : Seq[CountingOp] + val expressions: Seq[l.Expr] + def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] +} + +case class AssertStmt(e : l.Expr) extends Statement { + override val hashId = 130000 + override val md5hashCode = computeMD5Hash(e) + override def toLines = List("assert " + e.toString()) + override val countingOps = { + def isCountingOp(e : l.Expr) = { + e match { + case CountingOp(_, _, _) => true + case _ => false + } + } + UMCExpressions.findSubExpressions(e, isCountingOp).map(_.asInstanceOf[CountingOp]).toSeq + } + override val expressions = Seq(e) + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + rewriter(e) match { + case Some(eP) => Some(AssertStmt(eP)) + case None => None + } + } +} + +case class OrStmt(e1 : CountingOp, e2 : CountingOp, e3 : CountingOp) extends Statement { + assert (e1.xs == e2.xs && e2.xs == e3.xs) + assert (e1.ys == e2.ys && e2.ys == e3.ys) + + override val hashId = 130001 + override val md5hashCode = computeMD5Hash(e1, e2, e3) + override def toLines = List("assert or: " + e1.toString() + " == " + e2.toString() + " + " + e3.toString()) + override val countingOps = Seq(e1, e2, e3) + override val expressions = Seq(e1, e2, e3) + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + (rewriter(e1.e), rewriter(e2.e), rewriter(e3.e)) match { + case (Some(e1p), Some(e2p), Some(e3p)) => + val op1 = CountingOp(e1.xs, e1.ys, e1p) + val op2 = CountingOp(e2.xs, e2.ys, e2p) + val op3 = CountingOp(e3.xs, e3.ys, e3p) + Some(OrStmt(op1, op2, op3)) + case _ => None + } + } +} + +case class RangeStmt(op : CountingOp, cnt : l.Expr, assump: l.Expr) extends Statement { + lazy val lb : l.Expr = { + op.e match { + case l.OperatorApplication(l.ConjunctionOp(), + List(l.OperatorApplication(l.LEOp(), List(lb, l.Identifier(v))), + l.OperatorApplication(l.LTOp(), List(l.Identifier(u), ub)))) => lb + case _ => + throw new Utils.AssertionError("Unexpected operand to range expression.") + } + } + lazy val ub : l.Expr = { + op.e match { + case l.OperatorApplication(l.ConjunctionOp(), + List(l.OperatorApplication(l.LEOp(), List(lb, l.Identifier(v))), + l.OperatorApplication(l.LTOp(), List(l.Identifier(u), ub)))) => ub + case _ => + throw new Utils.AssertionError("Unexpected operand to range expression.") + } + } + lazy val v : l.Identifier = { + op.e match { + case l.OperatorApplication(l.ConjunctionOp(), + List(l.OperatorApplication(l.LEOp(), List(lb, l.Identifier(v))), + l.OperatorApplication(l.LTOp(), List(l.Identifier(u), ub)))) => + assert(u == v) + l.Identifier(v) + case _ => + throw new Utils.AssertionError("Unexpected operand to range expression.") + } + } + override val hashId = 130002 + override val md5hashCode = computeMD5Hash(op, cnt) + override def toLines = List("assert range: " + assump.toString + " ==> " + op.toString() + " == " + cnt.toString()) + override val countingOps = Seq(op) + override val expressions = Seq(op, cnt) + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + (rewriter(op.e), rewriter(cnt), rewriter(assump)) match { + case (Some(ep), Some(cntp), Some(aP)) => + val op1 = CountingOp(op.xs, op.ys, ep) + Some(RangeStmt(op1, cntp, aP)) + case _ => None + } + } +} +case class ConstLbStmt(e : CountingOp, v : l.IntLit, assump: l.Expr) extends Statement { + override val hashId = 130003 + override val md5hashCode = computeMD5Hash(e, v, assump) + override def toLines = { + if (assump == l.BoolLit(true)) { + List("assert constLB: " + e.toString() + " >= " + v.toString()) + } else { + List("assert constLB: " + assump.toString() + " ==> " + e.toString() + " >= " + v.toString()) + } + } + override val countingOps = Seq(e) + override val expressions = Seq(e, v, assump) + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + (rewriter(e.e), rewriter(v), rewriter(assump)) match { + case (Some(e1p), Some(e2p), Some(aP)) => + val e1 = CountingOp(e.xs, e.ys, e1p) + Some(ConstLbStmt(e1, e2p.asInstanceOf[l.IntLit], aP)) + case _ => None + } + } +} + +case class ConstUbStmt(e : CountingOp, v : l.IntLit, assump : l.Expr) extends Statement { + override val hashId = 130004 + override val md5hashCode = computeMD5Hash(e, v, assump) + override def toLines = { + if (assump == l.BoolLit(true)) { + List("assert constUB: " + e.toString() + " < " + v.toString()) + } else { + List("assert constUB: " + assump.toString() + " ==> " + e.toString() + " < " + v.toString()) + } + } + override val countingOps = Seq(e) + override val expressions = Seq(e, v, assump) + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + (rewriter(e.e), rewriter(v), rewriter(assump)) match { + case (Some(e1p), Some(e2p), Some(aP)) => + val e1 = CountingOp(e.xs, e.ys, e1p) + Some(ConstUbStmt(e1, e2p.asInstanceOf[l.IntLit], aP)) + case _ => None + } + } +} + +case class ConstEqStmt(e : CountingOp, v : l.IntLit, assump : l.Expr) extends Statement { + override val hashId = 130005 + override val md5hashCode = computeMD5Hash(e, v, assump) + override def toLines = { + if (assump == l.BoolLit(true)) { + List("assert constEq: " + e.toString() + " >= " + v.toString()) + } else { + List("assert constEq: " + assump.toString() + " ==> " + e.toString() + " == " + v.toString()) + } + } + override val countingOps = Seq(e) + override val expressions = Seq(e, v, assump) + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + (rewriter(e.e), rewriter(v), rewriter(assump)) match { + case (Some(e1p), Some(e2p), Some(aP)) => + val e1 = CountingOp(e.xs, e.ys, e1p) + Some(ConstEqStmt(e1, e2p.asInstanceOf[l.IntLit], assump)) + case _ => None + } + } +} + +case class IndLbStmt(fp : CountingOp, f : CountingOp, g : CountingOp, skolems : List[l.Expr]) extends Statement { + assert (fp.ys.size >= 1 && f.ys.size >= 1 && g.ys.size >= 1) + assert (fp.ys(0)._2.isInt) + assert (fp.ys == f.ys) + val n = fp.ys(0)._1 + assert (new ExprRewriter(Map(n -> UMCExpressions.plus(n, l.IntLit(1)))).rewrite(f.e) == fp.e) + + override val hashId = 130006 + override val md5hashCode = computeMD5Hash(fp, f, g, skolems) + override def toLines = { + List("assert indLB: " + fp.toString + " >= " + + f.toString() + " * " + g.toString() + " skolems (" + + Utils.join(skolems.map(_.toString()), ", ") + ");") + } + override val countingOps = Seq(fp, f, g) + override val expressions = Seq(fp, f, g) ++ skolems + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + val e_fp = rewriter(fp.e) + val e_f = rewriter(f.e) + val e_g = rewriter(g.e) + val skolemsP = skolems.flatMap(rewriter(_)) + (e_fp, e_f, e_g) match { + case (Some(e1), Some(e2), Some(e3)) => + val fpNew = CountingOp(fp.xs, fp.ys, e1) + val fNew = CountingOp(f.xs, f.ys, e2) + val gNew = CountingOp(g.xs, g.ys, e3) + Some(IndLbStmt(fpNew, fNew, gNew, skolemsP)) + case _ => None + } + } +} + +case class UbStmt(e1 : CountingOp, e2: CountingOp) extends Statement { + assert (e1.xs == e2.xs && e1.ys == e2.ys) + + override val hashId = 130007 + override val md5hashCode = computeMD5Hash(e1, e2) + override def toLines = + List("assert UB: " + e1.toString() + " <= " + e2.toString()) + override val countingOps = Seq(e1, e2) + override val expressions = Seq(e1, e2) + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + (rewriter(e1.e), rewriter(e2.e)) match { + case (Some(e1p), Some(e2p)) => + val e1New = CountingOp(e1.xs, e1.ys, e1p) + val e2New = CountingOp(e2.xs, e2.ys, e2p) + Some(UbStmt(e1New, e2New)) + case _ => None + } + } +} + +case class AndUbStmt(e1 : CountingOp, e2 : CountingOp, e3 : CountingOp) extends Statement { + assert (e1.xs.toSet == (e2.xs.toSet union e3.xs.toSet)) + + override val hashId = 130008 + override val md5hashCode = computeMD5Hash(e1, e2, e3) + override def toLines = List("assert andUB: " + e1.toString() + " <= " + e2.toString() + " * " + e3.toString()) + override val countingOps = Seq(e1, e2, e3) + override val expressions = Seq(e1, e2, e3) + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + (rewriter(e1.e), rewriter(e2.e), rewriter(e3.e)) match { + case (Some(e1p), Some(e2p), Some(e3p)) => + val op1 = CountingOp(e1.xs, e1.ys, e1p) + val op2 = CountingOp(e2.xs, e2.ys, e2p) + val op3 = CountingOp(e3.xs, e3.ys, e3p) + Some(AndUbStmt(op1, op2, op3)) + case _ => None + } + } +} + +case class DisjointStmt(e1 : CountingOp, e2 : CountingOp, e3 : CountingOp) extends Statement { + assert (e1.xs.toSet == (e2.xs.toSet union e3.xs.toSet)) + + override val hashId = 130009 + override val md5hashCode = computeMD5Hash(e1, e2, e3) + override def toLines = List("assert disjoint: " + e1.toString() + " == " + e2.toString() + " * " + e3.toString()) + override val countingOps = Seq(e1, e2, e3) + override val expressions = Seq(e1, e2, e3) + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + (rewriter(e1.e), rewriter(e2.e), rewriter(e3.e)) match { + case (Some(e1p), Some(e2p), Some(e3p)) => + val op1 = CountingOp(e1.xs, e1.ys, e1p) + val op2 = CountingOp(e2.xs, e2.ys, e2p) + val op3 = CountingOp(e3.xs, e3.ys, e3p) + Some(DisjointStmt(op1, op2, op3)) + case _ => None + } + } +} + +case class InjectivityStmt(f : CountingOp, g: CountingOp, skolems : List[l.Expr] ) extends Statement { + override val hashId = 130010 + override val md5hashCode = computeMD5Hash(f, g, skolems) + override def toLines = + List("assert injectivity: " + f.toString() + " <= " + g.toString() + " skolems (" + + Utils.join(skolems.map(_.toString()), ", ") + ");") + override val countingOps = Seq(f, g) + override val expressions = Seq(f, g) ++ skolems + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + val skolemsP = skolems.flatMap(rewriter(_)) + (rewriter(f.e), rewriter(g.e)) match { + case (Some(e1p), Some(e2p)) => + val e1New = CountingOp(f.xs, f.ys, e1p) + val e2New = CountingOp(g.xs, g.ys, e2p) + Some(InjectivityStmt(e1New, e2New, skolemsP)) + case _ => None + } + } +} + +case class IndUbStmt(fp : CountingOp, f : CountingOp, g : CountingOp, skolems : List[l.Expr]) extends Statement { + assert (fp.ys.size == 1 && f.ys.size == 1 && g.ys.size == 1) + assert (fp.ys(0)._2.isInt) + assert (fp.ys == f.ys && f.ys == g.ys) + val n = fp.ys(0)._1 + assert (new ExprRewriter(Map(n -> UMCExpressions.plus(n, l.IntLit(1)))).rewrite(f.e) == fp.e) + + override val hashId = 130011 + override val md5hashCode = computeMD5Hash(fp, f, g, skolems) + override def toLines = { + List("assert indUB: " + fp.toString + " <= " + + f.toString() + " * " + g.toString() + " skolems (" + + Utils.join(skolems.map(_.toString()), ", ") + ");") + } + override val countingOps = Seq(fp, f, g) + override val expressions = Seq(fp, f, g) ++ skolems + override def rewrite(rewriter : l.Expr => Option[l.Expr]) : Option[Statement] = { + val e_fp = rewriter(fp.e) + val e_f = rewriter(f.e) + val e_g = rewriter(g.e) + val skolemsP = skolems.flatMap(rewriter(_)) + (e_fp, e_f, e_g) match { + case (Some(e1), Some(e2), Some(e3)) => + val fpNew = CountingOp(fp.xs, fp.ys, e1) + val fNew = CountingOp(f.xs, f.ys, e2) + val gNew = CountingOp(g.xs, g.ys, e3) + Some(IndUbStmt(fpNew, fNew, gNew, skolemsP)) + case _ => None + } + } +} + +case class CountingProof(id : l.Identifier, decls : List[l.Decl], lemmas: List[l.ProcedureDecl], + stmts : List[Statement]) extends l.ASTNode { + override def toString = { + "module " + id.toString() + " {\n" + + Utils.join(decls.map(" " + _.toString()), "\n") + "\n\n" + + Utils.join(lemmas.map(" " + _.toString()), "\n") + + "\n\n proof {\n" + + Utils.join(stmts.map(st => " " + st.toString()), "\n") + + "\n }\n}" + } + def rewriteStatments(rewriter : l.ASTRewriter) : CountingProof = { + val ctx = decls.foldLeft(l.Scope.empty)((acc, d) => acc + d) + def rewriterFn(expr : l.Expr) : Option[l.Expr] = { + rewriter.visitExpr(expr, ctx) + } + + val stmtsP = stmts.flatMap(st => st.rewrite(rewriterFn)) + CountingProof(id, decls, lemmas, stmtsP) + } + override val hashId = 131001 + override val md5hashCode = computeMD5Hash(id, decls, stmts) +} + +/** Helpers to construct UCLID5 expressions. */ +object UMCExpressions { + // Helper functions to more easily construct expressions. + def forall(vs : List[(l.Identifier, l.Type)], e : l.Expr) = { + if (vs.nonEmpty) { + val op = l.ForallOp(vs, List.empty) + l.OperatorApplication(op, List(e)) + } else { + e + } + } + + def exists(vs : List[(l.Identifier, l.Type)], e : l.Expr) = { + assert (vs.nonEmpty) + val op = l.ExistsOp(vs, List.empty) + l.OperatorApplication(op, List(e)) + } + + def and(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.ConjunctionOp(), List(e1, e2)) + } + + def andL(es : Seq[l.Expr]) = { + assert (es.nonEmpty) + es.foldLeft(l.BoolLit(true).asInstanceOf[l.Expr])((acc, e) => and(acc, e)) + } + + def or(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.DisjunctionOp(), List(e1, e2)) + } + + def orL(es : Seq[l.Expr]) = { + assert (es.nonEmpty) + es.foldLeft(l.BoolLit(false).asInstanceOf[l.Expr])((acc, e) => or(acc, e)) + } + + def iff(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.IffOp(), List(e1, e2)) + } + + def implies(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.ImplicationOp(), List(e1, e2)) + } + def not(e : l.Expr) = { + l.OperatorApplication(l.NegationOp(), List(e)) + } + + def eq(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.EqualityOp(), List(e1, e2)) + } + + def plus(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.AddOp(), List(e1, e2)) + } + + def minus(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.SubOp(), List(e1, e2)) + } + + def mul(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.MulOp(), List(e1, e2)) + } + + def le(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.IntLEOp(), List(e1, e2)) + } + + def lt(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.IntLTOp(), List(e1, e2)) + } + + def ge(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.IntGEOp(), List(e1, e2)) + } + + def gt(e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.IntGTOp(), List(e1, e2)) + } + + + def rng(e1 : l.Expr, e2 : l.Expr, e3 : l.Expr) = { + and(le(e1, e2), lt(e2, e3)) + } + + def ite(c : l.Expr, e1 : l.Expr, e2 : l.Expr) = { + l.OperatorApplication(l.ITEOp(), List(c, e1, e2)) + } + + def max(e1 : l.Expr, e2 : l.Expr) = { + ite(lt(e1, e2), e2, e1) + } + + def distinct(es : l.Expr*) = { + if (es.size <= 1) { + l.BoolLit(true) + } else { + l.OperatorApplication(l.DistinctOp(), es.toList) + } + } + + def apply(id : l.Identifier, args : List[l.Expr]) = { + l.FuncApplication(id, args) + } + + def _findSubExpressions(e : l.Expr, fn : l.Expr => Boolean) : Set[l.Expr] = + findSubExpressions((e, fn)) + + val findSubExpressions = new Memo[(l.Expr, l.Expr => Boolean), Set[l.Expr]]( + (p : (l.Expr, l.Expr => Boolean)) => { + val expr = p._1 + val fn = p._2 + val subExprs : Set[l.Expr] = expr match { + case _ : l.Literal => Set.empty + case _ : l.Identifier => Set.empty + case _ : l.ExternalIdentifier => Set.empty + case l.ConstArray(e, t) => _findSubExpressions(e, fn) + case l.Tuple(es) => es.foldLeft(Set.empty[l.Expr])((acc, e) => _findSubExpressions(e, fn) ++ acc) + case l.OperatorApplication(op, args) => + val opExprs = op match { + case l.ArraySelect(inds) => + inds.foldLeft(Set.empty[l.Expr])((acc, e) => _findSubExpressions(e, fn) ++ acc) + case l.ArrayUpdate(inds, value) => + inds.foldLeft(_findSubExpressions(value, fn))((acc, e) => _findSubExpressions(e, fn) ++ acc) + case _ => + Set.empty[l.Expr] + } + args.foldLeft(opExprs)((acc, e) => _findSubExpressions(e, fn) ++ acc) + case l.Lambda(ids, e) => _findSubExpressions(e, fn) + case l.FuncApplication(e1, e2) => e2.foldLeft(_findSubExpressions(e1, fn))((acc, e) => acc ++ _findSubExpressions(e, fn)) + case CountingOp(xs, ys, e) => _findSubExpressions(e, fn) + } + if (fn(expr)) { subExprs + expr} + else { subExprs } + } + ) + + def findSupport(es : Seq[l.Expr]) : Set[l.Identifier] = { + es.foldLeft(Set.empty[l.Identifier])((acc, e) => acc ++ findSupport(e)) + } + val findSupport : Memo[l.Expr, Set[l.Identifier]] = new Memo[l.Expr, Set[l.Identifier]]( + e => { + e match { + case _ : l.Literal | _ : l.Identifier => + Set.empty + case l.ConstArray(e, t) => + findSupport(e) + case l.Tuple(es) => + findSupport(es) + case l.OperatorApplication(op, args) => + val subSupport = findSupport(args) + op match { + case qOp : l.QuantifiedBooleanOperator => + subSupport -- qOp.variables.map(_._1).toSet + case l.ArraySelect(inds) => + findSupport(inds) + case l.ArrayUpdate(inds, value) => + findSupport(inds) ++ findSupport(value) ++ subSupport + case _ => + subSupport + } + case l.Lambda(ids, exp) => + val subSupport = findSupport(exp) + subSupport -- ids.map(_._1).toSet + case CountingOp(xs, ys, e) => + // FIXME: this is a major hack. + // Introducing this because we *want* the variables in a CountingOp + // to be "captured" by outer quantifiers. + // Need to revist and fix this. + Set.empty + case _ : l.ExternalIdentifier => + throw new Utils.AssertionError("Eliminate external identifiers before calling findSupport.") + case l.FuncApplication(e1, e2s) => + throw new Utils.AssertionError("Eliminate function applications before calling findSupport.") + } + } + ) +} + +class ExprRewriter(val rwMap : Map[l.Expr, l.Expr]) { + val supports = rwMap.map(p => p._1 -> UMCExpressions.findSupport(p._1)).toMap + + val rewrite : Memo[l.Expr, l.Expr] = new Memo[l.Expr, l.Expr]( + exp => { + val expP : l.Expr = exp match { + case _ : l.Literal | _ : l.Identifier | _ : l.ExternalIdentifier => + exp + case l.ConstArray(e, t) => + val eP : l.Expr = rewrite(e) + l.ConstArray(eP, t) + case l.Tuple(es) => + val esP = es.map(e => rewrite(e)) + l.Tuple(esP) + case l.OperatorApplication(op, args) => + op match { + case qOp : l.QuantifiedBooleanOperator => + val mapP = rwMap.filter(p => !qOp.variables.exists(v => supports(p._1).contains(v._1))) + if (mapP != rwMap) { + // have to eliminate the bound variables. + val rewriter = new ExprRewriter(mapP) + val argsP = args.map(arg => rewriter.rewrite(arg)) + l.OperatorApplication(op, argsP) + } else { + // do the usual + val argsP = args.map(arg => rewrite(arg)) + l.OperatorApplication(op, argsP) + } + case l.ArraySelect(inds) => + val indsP = inds.map(ind => rewrite(ind)) + val argsP = args.map(arg => rewrite(arg)) + l.OperatorApplication(l.ArraySelect(indsP), argsP) + case l.ArrayUpdate(inds, e) => + val indsP = inds.map(ind => rewrite(ind)) + val eP = rewrite(e) + val argsP = args.map(arg => rewrite(arg)) + l.OperatorApplication(l.ArrayUpdate(indsP, eP), argsP) + case _ => + // do the usual. + val argsP = args.map(arg => rewrite(arg)) + l.OperatorApplication(op, argsP) + } + case l.Lambda(ids, exp) => + val mapP = rwMap.filter(p => !ids.exists(v => supports(p._1).contains(v._1))) + val expP = if (mapP != rwMap) { + // have to eliminate the bound variables. + val rewriter = new ExprRewriter(mapP) + rewriter.rewrite(exp) + } else { + // do the usual. + rewrite(exp) + } + l.Lambda(ids, exp) + case l.FuncApplication(e1, e2s) => + val e1p = rewrite(e1) + val e2sp = e2s.map(e2 => rewrite(e2)) + l.FuncApplication(e1p, e2sp) + case CountingOp(xs, ys, e) => + val eP = rewrite(e) + CountingOp(xs, ys, eP) + } + rwMap.get(expP) match { + case Some(repl) => repl + case None => expP + } + }) +} \ No newline at end of file diff --git a/src/main/scala/uclid/extensions/modelcounts/UMCMain.scala b/src/main/scala/uclid/extensions/modelcounts/UMCMain.scala new file mode 100644 index 000000000..133fa32e8 --- /dev/null +++ b/src/main/scala/uclid/extensions/modelcounts/UMCMain.scala @@ -0,0 +1,67 @@ +/* + * UCLID5 Verification and Synthesis Engine + * + * Copyright (c) 2017. + * Sanjit A. Seshia, Rohit Sinha and Pramod Subramanyan. + * + * All Rights Reserved. + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * 1. Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * + * documentation and/or other materials provided with the distribution. + * 3. Neither the name of the copyright holder nor the names of its + * contributors may be used to endorse or promote products derived from this + * software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, + * THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR + * PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR + * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + * Author: Pramod Subramanyan, Shubham Sahai + * + * Main file for the UCLID model counter. + * + */ +package uclid.extensions.modelcounts + +import uclid.UclidMain +import uclid.{lang => l} +import uclid.Utils + + +object UMCMain { + /** Executes regular UCLID5 on the processed module. */ + def runProcessedModel(module : l.Module, config: UclidMain.Config) : Unit = { + val mainModuleName = l.Identifier("main") + val modules = UclidMain.compileModules(List(module), mainModuleName, false) + val mainModule = UclidMain.instantiate(config, modules, mainModuleName, true) + mainModule match { + case Some(m) => UclidMain.execute(m, config) + case None => + throw new Utils.ParserError("Unable to find main module", None, None) + } + } + + def checkModel(f: java.io.File, config: UclidMain.Config) { + val module = UMCParser.parseUMCModel(f) + println("Parsed module: " + module.id.toString()) + println(module.toString()) + val moduleP = new UMCRewriter(module).process() + println("\nModule after rewriting: ") + println(moduleP.toString()) + runProcessedModel(moduleP, config) + } +} diff --git a/src/main/scala/uclid/extensions/modelcounts/UMCParser.scala b/src/main/scala/uclid/extensions/modelcounts/UMCParser.scala new file mode 100644 index 000000000..4d63b6a8b --- /dev/null +++ b/src/main/scala/uclid/extensions/modelcounts/UMCParser.scala @@ -0,0 +1,269 @@ +/* + * UCLID5 Verification and Synthesis Engine + * + * Copyright (c) 2017. + * Sanjit A. Seshia, Rohit Sinha and Pramod Subramanyan. + * + * All Rights Reserved. + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * 1. Redistributions of source code must retain the above copyright notice, + * + * this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * + * documentation and/or other materials provided with the distribution. + * 3. Neither the name of the copyright holder nor the names of its + * contributors may be used to endorse or promote products derived from this + * software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, + * THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR + * PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR + * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + * Author: Pramod Subramanyan, Shubham Sahai + * + * Parser for the UCLID model counter. + * + */ + +package uclid.extensions.modelcounts + +import uclid.{Utils, lang => l} +import uclid.lang.{Decl, Identifier, ProcedureAnnotations, Type} +import uclid.smt.IntLit +import uclid.extensions.modelcounts.{UMCExpressions => E} + +class UMCParser extends l.UclidParser { + lazy val KwLemmas = "lemmas" + lazy val KwLemma = "lemma" + lazy val KwProof = "proof" + lazy val KwConstLB = "constLB" + lazy val KwConstUB = "constUB" + lazy val KwConstEq = "constEq" + lazy val KwUB = "UB" + lazy val KwAndUB = "andUB" + lazy val KwDisjoint = "disjoint" + lazy val KwOr = "or" + lazy val KwInj = "injectivity" + lazy val KwIndLb = "indLB" + lazy val KwIndUb = "indUB" + lazy val KwSkolems = "skolems" + + lexical.reserved += (KwProof, KwOr, KwConstLB, KwConstUB, KwConstEq, KwIndLb, KwSkolems, KwUB, KwAndUB, + KwDisjoint, KwInj, KwIndUb, KwLemmas, KwLemma) + + lazy val UMCDecl: PackratParser[l.Decl] = + positioned (TypeDecl | DefineDecl | FuncDecl | AxiomDecl) + + lazy val CountingOpPrefix : PackratParser[(List[(Identifier, Type)], List[(Identifier, Type)])] = + ("#[" ~> IdTypeList) ~ (KwFor ~> IdTypeList) <~ "]" ~ "::" ^^ { + case xs ~ ys => (xs, ys) + } | + ("#[" ~> IdTypeList) <~ "]" ~ "::" ^^ { + case xs => (xs, List.empty) + } + + lazy val CountingExpr : PackratParser[CountingOp] = positioned { + CountingOpPrefix ~ ("(" ~> Expr <~ ")") ^^ { + case xs ~ e => CountingOp(xs._1, xs._2, e) + } + } + + lazy val C0: PackratParser[l.Expr] = positioned { CountingExpr | E1 } + + override lazy val E15: PackratParser[l.Expr] = positioned { + Literal | + "{" ~> Expr ~ rep("," ~> Expr) <~ "}" ^^ {case e ~ es => l.Tuple(e::es)} | + KwIf ~> ("(" ~> Expr <~ ")") ~ (KwThen ~> Expr) ~ (KwElse ~> Expr) ^^ { + case expr ~ thenExpr ~ elseExpr => l.OperatorApplication(l.ITEOp(), List(expr, thenExpr, elseExpr)) + } | + ConstArray | + KwLambda ~> (IdTypeList) ~ ("." ~> Expr) ^^ { case idtyps ~ expr => l.Lambda(idtyps, expr) } | + "(" ~> CExpr <~ ")" | + Id <~ OpPrime ^^ { case id => l.OperatorApplication(l.GetNextValueOp(), List(id)) } | + Id + } + + lazy val CExpr: PackratParser[l.Expr] = positioned { C0 } + + lazy val Stmt: PackratParser[Statement] = positioned { + KwAssert ~ KwOr ~ ":" ~> + (CountingExpr <~ "==") ~ (CountingExpr <~ "+") ~ CountingExpr <~ ";" ^^ { + case e1 ~ e2 ~ e3 => OrStmt(e1, e2, e3) + } | + KwAssert ~ KwRange ~ ":" ~> CountingExpr ~ ("==" ~> Expr) <~ ";" ^^ { + case e1 ~ e2 => { + RangeStmt(e1, e2, l.BoolLit(true)) + } + } | + KwAssert ~ KwRange ~ ":" ~> (Expr <~ "==>") ~ CountingExpr ~ ("==" ~> Expr) <~ ";" ^^ { + case assump ~ e1 ~ e2 => { + RangeStmt(e1, e2, assump) + } + } | + KwAssert ~ KwConstLB ~ ":" ~> CountingExpr ~ (">=" ~> Integer) <~ ";" ^^ { + case e ~ v => { + ConstLbStmt(e, v, l.BoolLit(true)) + } + } | + KwAssert ~ KwConstLB ~ ":" ~> (Expr <~ "==>") ~ CountingExpr ~ (">=" ~> Integer) <~ ";" ^^ { + case assump ~ e ~ v => { + ConstLbStmt(e, v, assump) + } + } | + KwAssert ~ KwConstUB ~ ":" ~> CountingExpr ~ ("<" ~> Integer) <~ ";" ^^ { + case e ~ v => { + ConstUbStmt(e, v, l.BoolLit(true)) + } + } | + KwAssert ~ KwConstUB ~ ":" ~> (Expr <~ "==>") ~ CountingExpr ~ ("<" ~> Integer) <~ ";" ^^ { + case assump ~ e ~ v => { + ConstUbStmt(e, v, assump) + } + } | + KwAssert ~ KwConstEq ~ ":" ~> CountingExpr ~ ("==" ~> Integer) <~ ";" ^^ { + case e ~ v => { + ConstEqStmt(e, v, l.BoolLit(true)) + } + } | + KwAssert ~ KwConstEq ~ ":" ~> (Expr <~ "==>") ~ CountingExpr ~ ("==" ~> Integer) <~ ";" ^^ { + case assump ~ e ~ v => { + ConstEqStmt(e, v, assump) + } + } | + KwAssert ~ KwIndLb ~ ":" ~> CountingExpr ~ (">=" ~> CountingExpr) ~ ("*" ~> CountingExpr) ~ (KwSkolems ~> ExprList <~ ";") ^^ { + case e1 ~ e2 ~ e3 ~ es => { + IndLbStmt(e1, e2, e3, es) + } + } | + KwAssert ~ KwUB ~ ":" ~> CountingExpr ~ ("<=" ~> CountingExpr) <~ ";" ^^ { + case e1 ~ e2 => { + UbStmt(e1, e2) + } + } | + KwAssert ~ KwAndUB ~ ":" ~> + (CountingExpr <~ "<=") ~ (CountingExpr <~ "*") ~ CountingExpr <~ ";" ^^ { + case e1 ~ e2 ~ e3 => AndUbStmt(e1, e2, e3) + } | + KwAssert ~ KwDisjoint ~ ":" ~> + (CountingExpr <~ "==") ~ (CountingExpr <~ "*") ~ CountingExpr <~ ";" ^^ { + case e1 ~ e2 ~ e3 => DisjointStmt(e1, e2, e3) + } | + KwAssert ~ KwInj ~ ":" ~> CountingExpr ~ ("<=" ~> CountingExpr) ~ (KwSkolems ~> ExprList <~ ";") ^^ { + case e1 ~ e2 ~ es => { + InjectivityStmt(e1, e2, es) + } + } | + KwAssert ~ KwIndUb ~ ":" ~> CountingExpr ~ ("<=" ~> CountingExpr) ~ ("*" ~> CountingExpr) ~ (KwSkolems ~> ExprList <~ ";") ^^ { + case e1 ~ e2 ~ e3 ~ es => { + IndUbStmt(e1, e2, e3, es) + } + } | + KwAssert ~> CExpr <~ ";" ^^ { + case e => AssertStmt(e) + } + } + + lazy val LemmaDecl : PackratParser[l.ProcedureDecl] = positioned { + KwLemma ~> ProcedureAnnotationList.? ~ Id ~ IdTypeList ~ (KwReturns ~> IdTypeList) ~ + rep(ProcedureVerifExpr) ~ BlkStmt ^^ + { case annotOpt ~ id ~ args ~ outs ~ verifExprs ~ body => + val annotations = annotOpt match { + case Some(ids) => ProcedureAnnotations(ids.toSet) + case None => ProcedureAnnotations(Set.empty) + } + val verifExprList = verifExprs.flatMap(v => v) + val requiresList = collectRequires(verifExprList) + val ensuresList = collectEnsures(verifExprList) + val modifiesList = collectModifies(verifExprList) + l.ProcedureDecl(id, l.ProcedureSig(args,outs), + body, requiresList, ensuresList, modifiesList.toSet, annotations) } | + // procedure with no return value + KwLemma ~> ProcedureAnnotationList.? ~ Id ~ IdTypeList ~ rep(ProcedureVerifExpr) ~ BlkStmt ^^ + { case annotOpt ~ id ~ args ~ verifExprs ~ body => + val annotations = annotOpt match { + case Some(ids) => ProcedureAnnotations(ids.toSet) + case None => ProcedureAnnotations(Set.empty) + } + val verifExprList = verifExprs.flatMap(v => v) + val requiresList = collectRequires(verifExprList) + val ensuresList = collectEnsures(verifExprList) + val modifiesList = collectModifies(verifExprList) + l.ProcedureDecl(id, l.ProcedureSig(args, List.empty), + body, requiresList, ensuresList, modifiesList.toSet, annotations) } + } + + lazy val LemmaDeclarations: PackratParser[l.ProcedureDecl] = + positioned ( LemmaDecl ); + + lazy val LemmaBlock: PackratParser[List[l.ProcedureDecl]] = { + KwLemmas ~ "{" ~> rep(LemmaDeclarations) <~ "}" + } + + lazy val ProofStmt: PackratParser[Statement] = + positioned ( Stmt ); + + lazy val ProofScript: PackratParser[List[Statement]] = { + KwProof ~ "{" ~> rep(ProofStmt) <~ "}" + } + + lazy val CntProof: PackratParser[CountingProof] = positioned { + KwModule ~> Id ~ ("{" ~> rep(UMCDecl)) ~ (ProofScript <~ "}") ^^ { + case id ~ decls ~ proof => { + CountingProof(id, decls, List(), proof) + } + } | + KwModule ~> Id ~ ("{" ~> rep(UMCDecl)) ~ LemmaBlock ~ (ProofScript <~ "}") ^^ { + case id ~ decls ~ lemmas ~ proof => { + CountingProof(id, decls, lemmas, proof) + } + } + } + + def parseUMCModel(filename : String, text: String): CountingProof = { + val tokens = new PackratReader(new lexical.Scanner(text)) + phrase(CntProof)(tokens) match { + case Success(module, _) => module + case NoSuccess(msg, next) => throw new uclid.Utils.SyntaxError(msg, Some(next.pos), Some(filename)) + } + } +} + +class RewriteDefines extends l.RewriteDefines { + override def visitExpr(e : l.Expr, context : l.Scope) : Option[l.Expr] = { + val eP = (e match { + case i : Identifier => visitIdentifier(i, context) + case eId : l.ExternalIdentifier => visitExternalIdentifier(eId, context) + case lit : l.Literal => visitLiteral(lit, context) + case rec : l.Tuple => visitTuple(rec, context) + case opapp : l.OperatorApplication => visitOperatorApp(opapp, context) + case a : l.ConstArray => visitConstArray(a, context) + case fapp : l.FuncApplication => visitFuncApp(fapp, context) + case lambda : l.Lambda => visitLambda(lambda, context) + case cntOp : CountingOp => + visitExpr(cntOp.e, context).flatMap(eP => Some(CountingOp(cntOp.xs, cntOp.ys, eP))) + }).flatMap(pass.rewriteExpr(_, context)) + return l.ASTNode.introducePos(true, true, eP, e.position) + } +} +object UMCParser { + val parserObj = new UMCParser() + val rewriter = new RewriteDefines() + def parseUMCModel(file: java.io.File) : CountingProof = { + val filePath = file.getPath() + val text = scala.io.Source.fromFile(filePath).mkString + val model = parserObj.parseUMCModel(filePath, text) + model.rewriteStatments(rewriter) + } +} diff --git a/src/main/scala/uclid/extensions/modelcounts/UMCRewriter.scala b/src/main/scala/uclid/extensions/modelcounts/UMCRewriter.scala new file mode 100644 index 000000000..3fbc78359 --- /dev/null +++ b/src/main/scala/uclid/extensions/modelcounts/UMCRewriter.scala @@ -0,0 +1,493 @@ +/* + * UCLID5 Verification and Synthesis Engine + * + * Copyright (c) 2017. + * Sanjit A. Seshia, Rohit Sinha and Pramod Subramanyan. + * + * All Rights Reserved. + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * 1. Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. Neither the name of the copyright holder nor the names of its + * contributors may be used to endorse or promote products derived from this + * software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, + * THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR + * PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR + * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + * Author: Pramod Subramanyan, Shubham Sahai + * + * Rewriter for the UCLID5 model counter. + * + */ +package uclid.extensions.modelcounts + +import uclid.{lang => l} +import uclid.Memo +import uclid.extensions.modelcounts.{UMCExpressions => E} +import scala.collection.mutable.{Set => MutableSet, Map => MutableMap} +import uclid.lang.BlockStmt + + +class UMCRewriter(cntProof : CountingProof) { + /* We will be using this set in a number of places. */ + type CountingOpSet = Set[CountingOp] + /* A map from counting ops to the UFs that represent them. */ + type UFMap = Map[CountingOp, l.FunctionDecl] + + + /** Finding all the counting operators in a list of assert statements. */ + def identifyCountOps(proofBlk: List[Statement]) : CountingOpSet = { + proofBlk.foldLeft(Set.empty[CountingOp]) { + (acc, st) => acc ++ st.countingOps.toSet + } + } + + /** Identifiers that are already declared in the module. */ + val existingIds = cntProof.decls.flatMap(d => d.declNames).toSet + /** Identifiers that are declared + newly generated names. */ + val usedIds : MutableSet[l.Identifier] = MutableSet.empty[l.Identifier] ++ existingIds + /** Counters that track (roughly) the number of generated identifiers with each prefix. */ + val counters = MutableMap.empty[String, Int] + /** Generate a new id. */ + def generateId(prefix: String) : l.Identifier = { + var cnt = counters.get(prefix) match { + case Some(n) => n + 1 + case None => 1 + } + def getName(n : Int) = l.Identifier(prefix + "_" + n.toString()) + var name = getName(cnt) + while (usedIds.contains(name)) { + cnt += 1 + name = getName(cnt) + } + usedIds += name + counters.put(prefix, cnt) + name + } + /** Generate UF decls for the identified counting operators. + * + */ + def generateCountingOpToUFMap(ops : CountingOpSet) : (UFMap) = { + ops.map { + op => { + val ufId = generateId("count") + val sig = l.FunctionSig(op.ys, l.IntegerType()) + val uf = l.FunctionDecl(ufId, sig) + op -> uf + } + }.toMap + } + + /** + * Create the list of UF + Axiom declarations. + */ + def generateUFDecls(ufMap : UFMap) : List[l.Decl] = { + def geqZero(e : l.Expr) : l.Expr = { + l.OperatorApplication(l.IntGEOp(), List(e, l.IntLit(0))) + } + def quantify(ufDecl : l.FunctionDecl, e : l.Expr) : l.Expr = { + if (ufDecl.sig.args.nonEmpty) { + l.OperatorApplication(l.ForallOp(ufDecl.sig.args, List.empty), List(e)) + } else { + e + } + } + ufMap.flatMap { + p => { + val ufDecl = p._2 + val innerExpr = geqZero(l.FuncApplication(ufDecl.id, ufDecl.sig.args.map(_._1))) + val axExpr = quantify(ufDecl, innerExpr) + val axiomDecl = l.AxiomDecl(Some(generateId("assump")), axExpr, List.empty) + List(ufDecl, axiomDecl) + } + }.toList + } + + def _apply(uf : l.FunctionDecl) = { + l.FuncApplication(uf.id, uf.sig.args.map(_._1)) + } + + def rewriteAssert(ufMap : UFMap, st : AssertStmt) : List[l.Statement] = { + val rewriter = new ExprRewriter(ufMap.map(p => (p._1 -> _apply(p._2))).toMap) + val eP = rewriter.rewrite(st.e) + val assertStmt = l.AssertStmt(eP, None, List.empty) + List(assertStmt) + } + + def rewriteOr(ufMap : UFMap, st : OrStmt) : List[l.Statement] = { + val o1 = st.e1 + val o2 = st.e2 + val o3 = st.e3 + val args = o1.xs ++ o1.ys + val f1 = o1.e + val f2 = o2.e + val f3 = o3.e + val assertExpr = E.and(E.forall(args, E.iff(f1, E.or(f2, f3))), + E.forall(args, E.not(E.and(f2, f3)))) + val assertStmt = l.AssertStmt(assertExpr, Some(l.Identifier("Or")), List.empty) + val ufn1 = _apply(ufMap(o1)) + val ufn2 = _apply(ufMap(o2)) + val ufn3 = _apply(ufMap(o3)) + val assumeExpr = E.forall(st.e1.ys, E.eq(ufn1, E.plus(ufn2, ufn3))) + val assumeStmt = l.AssumeStmt(assumeExpr, None) + List(assertStmt, assumeStmt) + } + + def rewriteRange(ufMap : UFMap, st : RangeStmt) : List[l.Statement] = { + val ufn = _apply(ufMap(st.op)) + val assumeExpr = E.forall(st.op.ys, E.eq(ufn, E.max(l.IntLit(0), E.minus(st.ub, st.lb)))) + val assumeStmt = l.AssumeStmt(assumeExpr, None) + val assertExpr = E.forall(st.op.ys, E.implies(st.assump, E.eq(ufn, st.cnt))) + val assertStmt = l.AssertStmt(assertExpr, Some(l.Identifier("Range")), List.empty) + List(assumeStmt, assertStmt) + } + + def getCnstBoundStmt(ufMap : UFMap, assump : l.Expr, e : CountingOp, cnt : Int, decorators : List[l.ExprDecorator]) = { + val cntArgs = e.xs + val qVars = e.ys + val ante = assump + val argVars = cntArgs.map(a => a._1) + val argsListP = (1 to cnt).map(i => cntArgs.map(a => generateId(a._1.name))) + val rwMaps = argsListP.map(argsP => (argVars.map(_.asInstanceOf[l.Expr]) zip argsP).toMap) + val exprs = rwMaps.map(rwMap => l.ExprRewriter.rewriteExprOnce(e.e, rwMap, l.Scope.empty)) + val newVars : List[(l.Identifier, l.Type)] = + argsListP.map(argsP => (cntArgs zip argsP).map(p => (p._2, p._1._2)).toList).toList.flatten ++ + e.ys + val blkDecls = newVars.map(p => l.BlockVarsDecl(List(p._1), p._2)) + val trueLit = l.BoolLit(true).asInstanceOf[l.Expr] + val conjunction = exprs.foldLeft(trueLit)((acc, e) => E.and(acc, e)) + val falseLit = l.BoolLit(false).asInstanceOf[l.Expr] + val distincts = E.distinct(rwMaps.map(m => l.Tuple(m.map(p => p._2).toList)).toList : _*) + val query = E.forall(qVars, E.implies(ante, E.and(conjunction, distincts))) + val assertStmt = l.AssertStmt(query, Some(l.Identifier("ConstantBound")), decorators) + BlockStmt(blkDecls, List(assertStmt)) + } + def rewriteConstLb(ufMap : UFMap, st : ConstLbStmt) : List[l.Statement] = { + val blkStmt = getCnstBoundStmt(ufMap, st.assump, st.e, st.v.value.toInt, List(l.CoverDecorator, l.SATOnlyDecorator)) + val ufn = _apply(ufMap(st.e)) + val assumeExpr = E.forall(st.e.ys, E.implies(st.assump, E.ge(ufn, st.v))) + val assumeStmt = l.AssumeStmt(assumeExpr, None) + List(blkStmt, assumeStmt) + } + + def rewriteConstUb(ufMap : UFMap, st : ConstUbStmt) : List[l.Statement] = { + val blkStmt = getCnstBoundStmt(ufMap, st.assump, st.e, st.v.value.toInt, List(l.CoverDecorator)) + val ufn = _apply(ufMap(st.e)) + val assumeExpr = E.forall(st.e.ys, E.implies(st.assump, E.lt(ufn, st.v))) + val assumeStmt = l.AssumeStmt(assumeExpr, None) + List(blkStmt, assumeStmt) + } + + def rewriteUb(ufMap : UFMap, st : UbStmt) : List[l.Statement] = { + val s1 = st.e1 + val s2 = st.e2 + val args = s1.xs ++ s1.ys + val f = s1.e + val g = s2.e + val assertExpr = E.forall(args, E.implies(f, g)) + val assertStmt = l.AssertStmt(assertExpr, Some(l.Identifier("UB")), List.empty) + val ufn1 = _apply(ufMap(s1)) + val ufn2 = _apply(ufMap(s2)) + val assumeExpr = E.forall(st.e1.ys, E.le(ufn1, ufn2)) + val assumeStmt = l.AssumeStmt(assumeExpr, None) + List(assertStmt, assumeStmt) + } + + def rewriteAndUb(ufMap : UFMap, st : AndUbStmt) : List[l.Statement] = { + val s1 = st.e1 + val s2 = st.e2 + val s3 = st.e3 + val args1 = s1.xs ++ s1.ys + val args2 = s2.xs ++ s2.ys + val args3 = s3.xs ++ s3.ys + val f1 = s1.e + val f2 = s2.e + val f3 = s3.e + val assertExpr = E.iff(E.forall(args1, f1), E.and(E.forall(args2, f2), E.forall(args3, f3))) + val assertStmt = l.AssertStmt(assertExpr, Some(l.Identifier("AndUB")), List.empty) + val ufn1 = _apply(ufMap(s1)) + val ufn2 = _apply(ufMap(s2)) + val ufn3 = _apply(ufMap(s3)) + val assumeExpr = E.forall(st.e1.ys, E.le(ufn1, E.mul(ufn2, ufn3))) + val assumeStmt = l.AssumeStmt(assumeExpr, None) + List(assertStmt, assumeStmt) + } + + def rewriteInjectivity(ufMap : UFMap, inj : InjectivityStmt) : List[l.Statement] = { + // forall x. f(x) ==> g(skolem(x)) + val f = inj.f + val g = inj.g + val f_x = f.e + val g_y = g.e + val skSubs = (g.xs.map(_._1.asInstanceOf[l.Expr]) zip inj.skolems).toMap + val conseq = new ExprRewriter(skSubs).rewrite(g_y) + val impl = E.implies(f_x, conseq) + val qVars = f.xs ++ f.ys + val qOp = E.forall(qVars, impl) + val liftAssertStmt = l.AssertStmt(qOp, Some(l.Identifier("Injectivity_SkolemApplication")), List.empty) + + // Next we want to show injectivity of the skolem: + // f(x1) && f(x2) && (x1 != x2) ==> skolem(x1) != skolem(x2) + val x1s = f.xs.map(p => generateId(p._1.toString())) + val x2s = f.xs.map(p => generateId(p._1.toString())) + val rwx1 = new ExprRewriter((f.xs zip x1s).map(p => (p._1._1.asInstanceOf[l.Expr] -> p._2.asInstanceOf[l.Expr])).toMap) + val rwx2 = new ExprRewriter((f.xs zip x2s).map(p => (p._1._1.asInstanceOf[l.Expr] -> p._2.asInstanceOf[l.Expr])).toMap) + + val f_x1n = rwx1.rewrite(f.e) + val f_x2n = rwx2.rewrite(f.e) + val xdiff = E.orL((x1s zip x2s).map(p => E.distinct(p._1, p._2))) + val sk1s = inj.skolems.map(sk => rwx1.rewrite(sk)) + val sk2s = inj.skolems.map(sk => rwx2.rewrite(sk)) + val ante2 = E.andL(List(f_x1n, f_x2n, xdiff)) + val skdiff = E.orL((sk1s zip sk2s).map(p => E.distinct(p._1, p._2))) + val impl2 = E.implies(ante2, skdiff) + val vars = (f.xs zip x1s).map(p => (p._2, p._1._2)) ++ + (f.xs zip x2s).map(p => (p._2, p._1._2)) ++ f.ys + val injAssertStmt = l.AssertStmt(E.forall(vars, impl2), Some(l.Identifier("Injectivity_SkolemInjectivity")), List.empty) + + // Now the assumption. + val ufn = _apply(ufMap(f)) + val ugn = _apply(ufMap(g)) + val leqExpr = E.le(ufn, ugn) + val assumpStmt1 = l.AssumeStmt(E.forall(f.ys, leqExpr), None) + + List(liftAssertStmt, injAssertStmt, assumpStmt1) + } + + + def rewriteDisjoint(ufMap : UFMap, st : DisjointStmt) : List[l.Statement] = { + val e2s = st.e2.xs.toSet + val e3s = st.e3.xs.toSet + val intersection = if ((e2s intersect e3s).isEmpty) l.BoolLit(true) + else l.BoolLit(false) + val s1 = st.e1 + val s2 = st.e2 + val s3 = st.e3 + val args1 = s1.xs ++ s1.ys + val args2 = s2.xs ++ s2.ys + val args3 = s3.xs ++ s3.ys + val f1 = s1.e + val f2 = s2.e + val f3 = s3.e + val assertExpr = E.and(E.iff(E.forall(args1, f1), E.and(E.forall(args2, f2), E.forall(args3, f3))), intersection) + val assertStmt = l.AssertStmt(assertExpr, Some(l.Identifier("Disjoint")), List.empty) + val ufn1 = _apply(ufMap(s1)) + val ufn2 = _apply(ufMap(s2)) + val ufn3 = _apply(ufMap(s3)) + val assumeExpr = E.forall(st.e1.ys, E.eq(ufn1, E.mul(ufn2, ufn3))) + val assumeStmt = l.AssumeStmt(assumeExpr, None) + List(assertStmt, assumeStmt) + } + + def rewriteIndLb(ufMap : UFMap, indlb : IndLbStmt) : List[l.Statement] = { + // First we want f(x, n) && g(y, n) ==> f(skolem(x, y), n + 1) + val f = indlb.f + val g = indlb.g + val f_xn = f.e + val g_yn = g.e + val ante = E.and(f_xn, g_yn) + val nplus1 = E.plus(indlb.n, l.IntLit(1)) + val skSubs = (f.xs.map(_._1.asInstanceOf[l.Expr]) zip indlb.skolems).toMap + + (indlb.n.asInstanceOf[l.Expr] -> nplus1) + val conseq = new ExprRewriter(skSubs).rewrite(f_xn) + val impl = E.implies(ante, conseq) + val qVars = f.xs ++ g.xs ++ f.ys ++ g.ys + val qOp = E.forall(qVars.distinct, impl) + val liftAssertStmt = l.AssertStmt(qOp, Some(l.Identifier("IndLB_SkolemApplication")), List.empty) + + // Now we want to show injectivity of the skolem: + // f(x1, n) && g(y1, n) && f(x2, n) && g(y2, n) && (x1 != x2 || y1 != y2) + // ==> skolem(x1, y1, n) != skolem(x2, y2, n) + val x1s = f.xs.map(p => generateId(p._1.toString())) + val x2s = f.xs.map(p => generateId(p._1.toString())) + val y1s = g.xs.map(p => generateId(p._1.toString())) + val y2s = g.xs.map(p => generateId(p._1.toString())) + val rwx1 = new ExprRewriter((f.xs zip x1s).map(p => (p._1._1.asInstanceOf[l.Expr] -> p._2.asInstanceOf[l.Expr])).toMap) + val rwy1 = new ExprRewriter((g.xs zip y1s).map(p => (p._1._1.asInstanceOf[l.Expr] -> p._2.asInstanceOf[l.Expr])).toMap) + val rwx2 = new ExprRewriter((f.xs zip x2s).map(p => (p._1._1.asInstanceOf[l.Expr] -> p._2.asInstanceOf[l.Expr])).toMap) + val rwy2 = new ExprRewriter((g.xs zip y2s).map(p => (p._1._1.asInstanceOf[l.Expr] -> p._2.asInstanceOf[l.Expr])).toMap) + val rwxy1 = new ExprRewriter(rwx1.rwMap ++ rwy1.rwMap) + val rwxy2 = new ExprRewriter(rwx2.rwMap ++ rwy2.rwMap) + val f_x1n = rwx1.rewrite(f.e) + val g_y1n = rwy1.rewrite(g.e) + val f_x2n = rwx2.rewrite(f.e) + val g_y2n = rwy2.rewrite(g.e) + val xdiff = E.orL((x1s zip x2s).map(p => E.distinct(p._1, p._2))) + val ydiff = E.orL((y1s zip y2s).map(p => E.distinct(p._1, p._2))) + val sk1s = indlb.skolems.map(sk => rwxy1.rewrite(sk)) + val sk2s = indlb.skolems.map(sk => rwxy2.rewrite(sk)) + val ante2 = E.andL(List(f_x1n, f_x2n, g_y1n, g_y2n, E.or(xdiff, ydiff))) + val skdiff = E.orL((sk1s zip sk2s).map(p => E.distinct(p._1, p._2))) + val impl2 = E.implies(ante2, skdiff) + val vars = (f.xs zip x1s).map(p => (p._2, p._1._2)) ++ + (f.xs zip x2s).map(p => (p._2, p._1._2)) ++ + (g.xs zip y1s).map(p => (p._2, p._1._2)) ++ + (g.xs zip y2s).map(p => (p._2, p._1._2)) ++ f.ys ++ g.ys + val injAssertStmt = l.AssertStmt(E.forall(vars.distinct, impl2), Some(l.Identifier("IndLB_SkolemInjectivity")), List.empty) + + // Finally, we have to produce the assumption. + val ufn = _apply(ufMap(f)) + val ugn = _apply(ufMap(g)) + val ufnplus1 = E.apply(ufMap(f).id, List(nplus1) ++ ufMap(f).sig.args.drop(1).map(_._1)) + val geqExpr = E.ge(ufnplus1, E.mul(ufn, ugn)) + val assumpStmt1 = l.AssumeStmt(E.forall(f.ys ++ g.ys, geqExpr), None) + val ufpn = _apply(ufMap(indlb.fp)) + val eqExpr = E.eq(ufnplus1, ufpn) + val assumpStmt2 = l.AssumeStmt(E.forall(f.ys, eqExpr), None) + List(liftAssertStmt, injAssertStmt, assumpStmt1, assumpStmt2) + } + + def rewriteIndUb(ufMap : UFMap, indub : IndUbStmt) : List[l.Statement] = { + // First we want f(x, n) ==> f(skolem_x(x, n), n - 1) && g(skolem_y(x, n), n - 1) + val fp = indub.fp + val f = indub.f + val g = indub.g + val f_xn = f.e + val g_yn = g.e + val ante = fp.e + val skSubs = (f.xs.map(_._1.asInstanceOf[l.Expr]) zip indub.skolems.lift(0)).toMap ++ + (g.xs.map(_._1.asInstanceOf[l.Expr]) zip indub.skolems.lift(1)).toMap + + val conseq_f_subs = new ExprRewriter(skSubs).rewrite(f_xn) + val conseq_g_subs = new ExprRewriter(skSubs).rewrite(g_yn) + + // add base case of induction to consequent. i.e. n+1 == 0 + val nplus1 = E.plus(indub.n, l.IntLit(1)) + val conseq_base = E.eq(nplus1,l.IntLit(0)) + + val conseq = E.or( E.and(conseq_f_subs, conseq_g_subs), conseq_base) + val impl = E.implies(ante, conseq) + val qVars = f.xs ++ g.xs ++ f.ys ++ g.ys + val qOp = E.forall(qVars.distinct, impl) + val lowerAssertStmt = l.AssertStmt(qOp, Some(l.Identifier("IndUB_SkolemApplication")), List.empty) + + // Now we want to show injectivity of the skolem: + // f(x1, n+1) && f(x2, n+1) && (x1 != x2) + // ==> skolem_x(x1, n) != skolem_x(x2,n) || skolem_y(x1,n) != skolem_y(x2, n) + val x1s = fp.xs.map(p => generateId(p._1.toString())) + val x2s = fp.xs.map(p => generateId(p._1.toString())) + + val rwx1 = new ExprRewriter((fp.xs zip x1s).map(p => (p._1._1.asInstanceOf[l.Expr] -> p._2.asInstanceOf[l.Expr])).toMap) + val rwx2 = new ExprRewriter((fp.xs zip x2s).map(p => (p._1._1.asInstanceOf[l.Expr] -> p._2.asInstanceOf[l.Expr])).toMap) + + val f_x1n = rwx1.rewrite(fp.e) + val f_x2n = rwx2.rewrite(fp.e) + val xdiff = E.orL((x1s zip x2s).map(p => E.distinct(p._1, p._2))) + + val ante2 = E.andL(List(f_x1n, f_x2n, xdiff)) + + val sk_x1 = indub.skolems.map(sk => rwx1.rewrite(sk)) + val sk_x2 = indub.skolems.map(sk => rwx2.rewrite(sk)) + + val skdiff = E.orL((sk_x1 zip sk_x2).map(p => E.distinct(p._1, p._2))) + + val impl2 = E.implies(ante2, skdiff) + + val vars = (f.xs zip x1s).map(p => (p._2, p._1._2)) ++ + (f.xs zip x2s).map(p => (p._2, p._1._2)) ++ f.ys + val injAssertStmt = l.AssertStmt(E.forall(vars.distinct, impl2), Some(l.Identifier("IndUB_SkolemInjectivity")), List.empty) + + // Finally, we have to produce the assumption. + val ufn = _apply(ufMap(f)) + val ugn = _apply(ufMap(g)) + val ufnplus1 = E.apply(ufMap(f).id, List(nplus1) ++ ufMap(f).sig.args.drop(1).map(_._1)) + val geqExpr = E.le(ufnplus1, E.mul(ufn, ugn)) + val assumpStmt1 = l.AssumeStmt(E.forall(f.ys ++ g.ys, geqExpr), None) + val ufpn = _apply(ufMap(indub.fp)) + val eqExpr = E.eq(ufnplus1, ufpn) + val assumpStmt2 = l.AssumeStmt(E.forall(f.ys, eqExpr), None) + List(lowerAssertStmt, injAssertStmt, assumpStmt1, assumpStmt2) + } + + + def rewriteAssert(ufmap : UFMap, st : Statement) : List[l.Statement] = { + val newStmts : List[l.Statement] = st match { + case a : AssertStmt => + rewriteAssert(ufmap, a) + case d : OrStmt => + rewriteOr(ufmap, d) + case r : RangeStmt => + rewriteRange(ufmap, r) + case constLb : ConstLbStmt => + rewriteConstLb(ufmap, constLb) + case constUb : ConstUbStmt => + rewriteConstUb(ufmap, constUb) + case eq : ConstEqStmt => + rewriteConstLb(ufmap, ConstLbStmt(eq.e, eq.v, eq.assump)) ++ + rewriteConstUb(ufmap, ConstUbStmt(eq.e, l.IntLit(eq.v.value + 1), eq.assump)) + case indLb : IndLbStmt => + rewriteIndLb(ufmap, indLb) + case ub : UbStmt => + rewriteUb(ufmap, ub) + case andUb : AndUbStmt => + rewriteAndUb(ufmap, andUb) + case disj : DisjointStmt => + rewriteDisjoint(ufmap, disj) + case inj : InjectivityStmt => + rewriteInjectivity(ufmap, inj) + case indUb : IndUbStmt => + rewriteIndUb(ufmap, indUb) + case _ => + throw new AssertionError("Unknown proof statement: " + st.toString()) + } + l.ASTNode.introducePos(true, true, newStmts, st.position) + } + + lazy val controlBlock : List[l.GenericProofCommand] = List( + l.GenericProofCommand( + l.Identifier("verify"), + List.empty, List((l.Identifier("countingProof"), "countingProof")), + Some(l.Identifier("v")), None), + l.GenericProofCommand( + l.Identifier("check"), + List.empty, List.empty, + None, None), + l.GenericProofCommand( + l.Identifier("print_results"), + List.empty, List.empty, + None, None), + ) + + lazy val verifyLemmas : List[l.GenericProofCommand] = + cntProof.lemmas.map(lem => l.GenericProofCommand( + l.Identifier("verify"), + List.empty, List((lem.id, lem.id.toString+ " in Lemma block.")), + None, None)) + + def process() : l.Module = { + val countingOps = identifyCountOps(cntProof.stmts) + val ufMap = generateCountingOpToUFMap(countingOps) + val ufDecls = generateUFDecls(ufMap) + val newProofStmts = cntProof.stmts.flatMap(st => rewriteAssert(ufMap, st)) + val newProofProc = l.ProcedureDecl( + l.Identifier("countingProof"), + l.ProcedureSig(List.empty, List.empty), + l.BlockStmt(List.empty, newProofStmts), + List.empty, List.empty, Set.empty, l.ProcedureAnnotations(Set.empty)) + val prevDecls = cntProof.decls.filter(p => !p.isInstanceOf[l.ProcedureDecl]) + val prevProcDecls = cntProof.lemmas + val moduleP = l.Module(cntProof.id, + prevDecls ++ prevProcDecls ++ ufDecls ++ List(newProofProc), + verifyLemmas ++ controlBlock, List.empty) + println(ufMap.toString()) + println(ufDecls.toString()) + moduleP + } +} \ No newline at end of file diff --git a/src/main/scala/uclid/lang/ASTVisitorUtils.scala b/src/main/scala/uclid/lang/ASTVisitorUtils.scala index 3469b5cd7..d386fe0ea 100644 --- a/src/main/scala/uclid/lang/ASTVisitorUtils.scala +++ b/src/main/scala/uclid/lang/ASTVisitorUtils.scala @@ -130,6 +130,7 @@ object ExprRewriter val rewriter = new ASTRewriter("", new ExprRewriterPass(rewrites)) rewriter.visitLhs(lhs, context).get } + } class ExprRewriter(name: String, rewrites : Map[Expr, Expr]) diff --git a/src/main/scala/uclid/lang/ASTVistors.scala b/src/main/scala/uclid/lang/ASTVistors.scala index e53236903..8a9ed83cd 100644 --- a/src/main/scala/uclid/lang/ASTVistors.scala +++ b/src/main/scala/uclid/lang/ASTVistors.scala @@ -1610,8 +1610,9 @@ class ASTRewriter (_passName : String, _pass: RewritePass, setFilename : Boolean def visitAssertStatement(st : AssertStmt, context : Scope) : Option[Statement] = { val idP = st.id.flatMap(id => visitIdentifier(id, context)) val envP = if (context.environment == ProceduralEnvironment) ProceduralAssertEnvironment else AssertEnvironment + // TODO: implement visitDecorator val stP = visitExpr(st.e, context.withEnvironment(envP)).flatMap((e) => { - pass.rewriteAssert(AssertStmt(e, idP), context) + pass.rewriteAssert(AssertStmt(e, idP, st.decorators), context) }) return ASTNode.introducePos(setPosition, setFilename, stP, st.position) } diff --git a/src/main/scala/uclid/lang/ModularProductProgram.scala b/src/main/scala/uclid/lang/ModularProductProgram.scala index bf0bb6f07..5da7956df 100644 --- a/src/main/scala/uclid/lang/ModularProductProgram.scala +++ b/src/main/scala/uclid/lang/ModularProductProgram.scala @@ -524,7 +524,7 @@ class ModularProductProgramPass extends RewritePass { } } - case AssertStmt(expr, id) => + case AssertStmt(expr, id, decorators) => val activationVariableArray = helperObj.mapOfActivationVariables(currentScope) val emptyVarsList: List[BlockVarsDecl] = List() expr match { @@ -546,7 +546,7 @@ class ModularProductProgramPass extends RewritePass { andCondition = Operator.and(andCondition, checkActVarCondition) } val renamedExpression = getRenamedExpr(expr, context, k) - val newAssertStatement = AssertStmt(renamedExpression, id) + val newAssertStatement = AssertStmt(renamedExpression, id, decorators) ASTNode.introducePos(true, true, newAssertStatement, stmts.head.position) val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssertStatement.asInstanceOf[Statement])) val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) @@ -560,7 +560,7 @@ class ModularProductProgramPass extends RewritePass { val currentActVarName = activationVariableArray(i) val checkActVarCondition = currentActVarName.asInstanceOf[Expr] val renamedExpression = getRenamedExpr(expr, context, i) - val newAssertStatement = AssertStmt(renamedExpression, id) + val newAssertStatement = AssertStmt(renamedExpression, id, decorators) ASTNode.introducePos(true, true, newAssertStatement, stmts.head.position) val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssertStatement.asInstanceOf[Statement])) val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) @@ -576,7 +576,7 @@ class ModularProductProgramPass extends RewritePass { val currentActVarName = activationVariableArray(i) val checkActVarCondition = currentActVarName.asInstanceOf[Expr] val renamedExpression = getRenamedExpr(expr, context, i) - val newAssertStatement = AssertStmt(renamedExpression, id) + val newAssertStatement = AssertStmt(renamedExpression, id, decorators) ASTNode.introducePos(true, true, newAssertStatement, stmts.head.position) val trueBlockStmt = BlockStmt(emptyVarsList,List(newAssertStatement.asInstanceOf[Statement])) val falseBlockStmt = BlockStmt(emptyVarsList, List(SkipStmt())) @@ -1094,7 +1094,7 @@ class ModularProductProgramPass extends RewritePass { newstmts += oldstmts.head } - case AssertStmt(expr, _) => + case AssertStmt(expr, id, decorators) => expr match { case OperatorApplication(op, operands) => val hasHyperSelect = isHyperSelectPresent(op, operands) diff --git a/src/main/scala/uclid/lang/ModuleFlattener.scala b/src/main/scala/uclid/lang/ModuleFlattener.scala index de1c4749d..4e920957e 100644 --- a/src/main/scala/uclid/lang/ModuleFlattener.scala +++ b/src/main/scala/uclid/lang/ModuleFlattener.scala @@ -550,7 +550,7 @@ class ModuleInstantiatorPass(module : Module, inst : InstanceDecl, targetModule val preconditionAsserts : List[Statement] = proc.requires.map { (req) => { val exprP = oldRewriter.rewriteExpr(rewriter.rewriteExpr(req, context), context) - val node = AssertStmt(exprP, Some(Identifier("precondition"))) + val node = AssertStmt(exprP, Some(Identifier("precondition")), List.empty) ASTNode.introducePos(true, true, node, req.position) } } @@ -559,7 +559,7 @@ class ModuleInstantiatorPass(module : Module, inst : InstanceDecl, targetModule proc.ensures.map { (ens) => { val exprP = oldRewriter.rewriteExpr(rewriter.rewriteExpr(ens, context), context) - val node = AssertStmt(exprP, Some(Identifier("postcondition"))) + val node = AssertStmt(exprP, Some(Identifier("postcondition")), List.empty) ASTNode.introducePos(true, true, node, ens.position) } } diff --git a/src/main/scala/uclid/lang/ModuleTypeChecker.scala b/src/main/scala/uclid/lang/ModuleTypeChecker.scala index 141e65cff..9fdeeb51c 100644 --- a/src/main/scala/uclid/lang/ModuleTypeChecker.scala +++ b/src/main/scala/uclid/lang/ModuleTypeChecker.scala @@ -50,7 +50,7 @@ class ModuleTypeCheckerPass extends ReadOnlyPass[Set[ModuleError]] in } else { st match { - case AssertStmt(e, _) => + case AssertStmt(e, id, _) => val eType = exprTypeChecker.typeOf(e, context) if (!eType.isBool) { in + ModuleError("Assertion expression must be of Boolean or Temporal type", st.position) diff --git a/src/main/scala/uclid/lang/PrimedAssignmentChecker.scala b/src/main/scala/uclid/lang/PrimedAssignmentChecker.scala index f8864503d..09777d377 100644 --- a/src/main/scala/uclid/lang/PrimedAssignmentChecker.scala +++ b/src/main/scala/uclid/lang/PrimedAssignmentChecker.scala @@ -100,11 +100,11 @@ class PrimedAssignmentCheckerPass extends ReadOnlyPass[Set[ModuleError]] } } st match { - case IfElseStmt(_, _, _) | - ForStmt(_, _, _, _) | WhileStmt(_, _, _) | - CaseStmt(_) | SkipStmt() | - AssertStmt(_, _) | AssumeStmt(_, _) | - HavocStmt(_) | BlockStmt(_, _) => + case IfElseStmt(_, _, _) | + ForStmt(_, _, _, _) | WhileStmt(_, _, _) | + CaseStmt(_) | SkipStmt() | + AssertStmt(_, _, _) | AssumeStmt(_, _) | + HavocStmt(_) | BlockStmt(_, _) => in case ModuleCallStmt(_) => checkParallelConstruct("next") diff --git a/src/main/scala/uclid/lang/ProcedureInliner.scala b/src/main/scala/uclid/lang/ProcedureInliner.scala index b3ae57d3c..183ba2203 100644 --- a/src/main/scala/uclid/lang/ProcedureInliner.scala +++ b/src/main/scala/uclid/lang/ProcedureInliner.scala @@ -185,7 +185,7 @@ trait NewProcedureInlinerPass extends RewritePass { val preconditionAsserts : List[Statement] = proc.requires.map { (req) => { val exprP = oldRewriter.rewriteExpr(rewriter.rewriteExpr(req, context), context) - val node = AssertStmt(exprP, Some(Identifier("precondition"))) + val node = AssertStmt(exprP, Some(Identifier("precondition")), List.empty) ASTNode.introducePos(true, true, node, req.position) } } @@ -194,7 +194,7 @@ trait NewProcedureInlinerPass extends RewritePass { proc.ensures.map { (ens) => { val exprP = oldRewriter.rewriteExpr(rewriter.rewriteExpr(ens, context), context) - val node = AssertStmt(exprP, Some(Identifier("postcondition"))) + val node = AssertStmt(exprP, Some(Identifier("postcondition")), List.empty) ASTNode.introducePos(true, true, node, ens.position) } } diff --git a/src/main/scala/uclid/lang/Scope.scala b/src/main/scala/uclid/lang/Scope.scala index 5fda03d3c..94f394537 100644 --- a/src/main/scala/uclid/lang/Scope.scala +++ b/src/main/scala/uclid/lang/Scope.scala @@ -244,6 +244,37 @@ case class Scope ( Scope(map + (m.id -> Scope.ModuleDefinition(m)), module, procedure, cmd, environment, parent) } + def +(d: Decl) : Scope = { + val mapP = d match { + case instD : InstanceDecl => + Scope.addToMap(map, Scope.Instance(instD)) + case ProcedureDecl(id, sig, _, _, _, _, _) => Scope.addToMap(map, Scope.Procedure(id, sig.typ)) + case TypeDecl(id, typ) => Scope.addToMap(map, Scope.TypeSynonym(id, typ)) + case StateVarsDecl(ids, typ) => ids.foldLeft(map)((acc, id) => Scope.addToMap(acc, Scope.StateVar(id, typ))) + case InputVarsDecl(ids, typ) => ids.foldLeft(map)((acc, id) => Scope.addToMap(acc, Scope.InputVar(id, typ))) + case OutputVarsDecl(ids, typ) => ids.foldLeft(map)((acc, id) => Scope.addToMap(acc, Scope.OutputVar(id, typ))) + case SharedVarsDecl(ids, typ) => ids.foldLeft(map)((acc, id) => Scope.addToMap(acc, Scope.SharedVar(id, typ))) + case ConstantLitDecl(id, lit) => Scope.addToMap(map, Scope.ConstantLit(id, lit)) + case ConstantsDecl(ids, typ) => ids.foldLeft(map)((acc, id) => Scope.addToMap(acc, Scope.ConstantVar(id, typ))) + case GrammarDecl(id, sig, nts) => Scope.addToMap(map, Scope.Grammar(id, sig.typ, nts)) + case FunctionDecl(id, sig) => Scope.addToMap(map, Scope.Function(id, sig.typ)) + case SynthesisFunctionDecl(id, sig, _, _, _) => Scope.addToMap(map, Scope.Function(id, sig.typ)) // FIXME + case DefineDecl(id, sig, expr) => Scope.addToMap(map, Scope.Define(id, sig.typ, DefineDecl(id, sig, expr))) + case SpecDecl(id, expr, params) => Scope.addToMap(map, Scope.SpecVar(id, expr, params)) + case AxiomDecl(sId, expr, params) => sId match { + case Some(id) => Scope.addToMap(map, Scope.AxiomVar(id, expr, params)) + case None => map + } + //case ModuleConstantsImportDecl(id) => Scope.addToMap(mapAcc, Scope.ConstantsImport(id)) + //case ModuleFunctionsImportDecl(id) => Scope.addToMap(mapAcc, Scope.FunctionsImport(id)) + case ModuleConstantsImportDecl(_) => map + case ModuleFunctionsImportDecl(_) => map + case ModuleTypesImportDecl(_) | + ModuleDefinesImportDecl(_) | + InitDecl(_) | NextDecl(_) => map + } + Scope(mapP, None, None, None, environment, parent) + } /** Return a new context with the declarations in this module added to it. */ def +(m: Module) : Scope = { Utils.assert(module.isEmpty, "A module was already added to this Context.") diff --git a/src/main/scala/uclid/lang/StatementScheduler.scala b/src/main/scala/uclid/lang/StatementScheduler.scala index 324a44fb0..0e826828b 100644 --- a/src/main/scala/uclid/lang/StatementScheduler.scala +++ b/src/main/scala/uclid/lang/StatementScheduler.scala @@ -48,8 +48,8 @@ object StatementScheduler { def writeSet(st : Statement, context : Scope) : Set[Identifier] = { st match { case SkipStmt() => Set.empty - case AssertStmt(_, _) => Set.empty - case AssumeStmt(_, _) => Set.empty + case AssertStmt(e, _, _) => Set.empty + case AssumeStmt(e, _) => Set.empty case HavocStmt(h) => h match { case HavocableId(id) => Set(id) @@ -111,8 +111,8 @@ object StatementScheduler { def writeSetIds(st : Statement, context : Scope) : Set[Identifier] = { st match { case SkipStmt() => Set.empty - case AssertStmt(_, _) => Set.empty - case AssumeStmt(_, _) => Set.empty + case AssertStmt(e, _, _) => Set.empty + case AssumeStmt(e, _) => Set.empty case HavocStmt(h) => h match { case HavocableId(id) => Set(id) @@ -182,10 +182,18 @@ object StatementScheduler { def readSet(st : Statement, context : Scope) : Set[Identifier] = { st match { case SkipStmt() => Set.empty - case AssertStmt(e, _) => readSet(e) + case AssertStmt(e, _, _) => readSet(e) case AssumeStmt(e, _) => readSet(e) case HavocStmt(_) => Set.empty - case AssignStmt(_, rhss) => readSets(rhss) + case AssignStmt(lhss, rhss) => + { + val arrayIndices = + lhss flatMap { + case arrayselect : LhsArraySelect => Some(arrayselect.indices) + case _ => None + } + readSets(rhss)++readSets(arrayIndices.flatten) + } case BlockStmt(vars, stmts) => val declaredVars : Set[Identifier] = vars.flatMap(vs => vs.ids.map(v => v)).toSet readSets(stmts, context + vars) -- declaredVars @@ -236,10 +244,20 @@ object StatementScheduler { def primeReadSet(st : Statement, context : Scope) : Set[Identifier] = { st match { case SkipStmt() => Set.empty - case AssertStmt(e, _) => primeReadSet(e) + case AssertStmt(e, _, _) => primeReadSet(e) case AssumeStmt(e, _) => primeReadSet(e) case HavocStmt(_) => Set.empty - case AssignStmt(_, rhss) => primeReadSets(rhss) + case AssignStmt(lhss, rhss) => + // this code is not necessary because we do not support updating arrays using an array select e.g., A[i]' = 0 + // but it is added here incase we do support this in future + { + val arrayIndices = + lhss flatMap { + case arrayselect : LhsArraySelect => Some(arrayselect.indices) + case _ => None + } + primeReadSets(rhss)++primeReadSets(arrayIndices.flatten) + } case BlockStmt(vars, stmts) => val declaredVars : Set[Identifier] = vars.flatMap(vs => vs.ids.map(v => v)).toSet primeReadSets(stmts, context + vars) -- declaredVars diff --git a/src/main/scala/uclid/lang/UclidLanguage.scala b/src/main/scala/uclid/lang/UclidLanguage.scala index 75498a9a4..8647b871b 100644 --- a/src/main/scala/uclid/lang/UclidLanguage.scala +++ b/src/main/scala/uclid/lang/UclidLanguage.scala @@ -135,7 +135,7 @@ object ASTNode { /** All elements in the AST are derived from this class. * The plan is to stick an ID into this later so that we can use the ID to store auxiliary information. */ -sealed trait ASTNode extends Positional with PositionedNode { +trait ASTNode extends Positional with PositionedNode { val astNodeId = IdGenerator.newId() } @@ -643,11 +643,11 @@ case class GetNextValueOp() extends Operator { } case class DistinctOp() extends Operator { override def toString = "distinct" - override def fixity = Operator.INFIX + override def fixity = Operator.PREFIX override val hashId = 1709 override val md5hashCode = computeMD5Hash } -sealed abstract class Expr extends ASTNode { +abstract class Expr extends ASTNode { /** Is this value a statically-defined constant? */ def isConstant = false def isTemporal = false @@ -746,6 +746,8 @@ case class OperatorApplication(op: Operator, operands: List[Expr]) extends Possi operands(0).toString + "." + i.toString case SelectFromInstance(f) => operands(0).toString + "." + f.toString + case ITEOp() => + "(if (" + operands(0).toString + ") then (" + operands(1).toString + ") else (" + operands(2).toString + "))" case ForallOp(_, _) | ExistsOp(_, _) => "(" + op.toString + operands(0).toString + ")" case _ => @@ -846,17 +848,19 @@ case object CoverDecorator extends ExprDecorator { override val hashId = 2605 override val md5hashCode = computeMD5Hash } +case object SATOnlyDecorator extends ExprDecorator { + override def toString = "SATOnly" + override val hashId = 2606 + override val md5hashCode = computeMD5Hash +} object ExprDecorator { /** Factory constructor. */ def parse(e : Expr) : ExprDecorator = { val dec = e match { - case Identifier(id) => - if (id == "LTL") { - LTLExprDecorator - } else { - UnknownDecorator(e.toString) - } + case Identifier("LTL") => LTLExprDecorator + case Identifier("cover") => CoverDecorator + case Identifier("SATOnly") => SATOnlyDecorator case _ => UnknownDecorator(e.toString) } dec.pos = e.pos @@ -1136,7 +1140,7 @@ case class HavocableInstanceId(opapp : OperatorApplication) extends HavocableEnt } /** Statements **/ -sealed abstract class Statement extends ASTNode { +abstract class Statement extends ASTNode { override def toString = Utils.join(toLines, "\n") + "\n" def hasStmtBlock = false val isLoop = false @@ -1152,8 +1156,24 @@ case class SkipStmt() extends Statement { override val hashId = 3000 override val md5hashCode = computeMD5Hash } -case class AssertStmt(e: Expr, id : Option[Identifier]) extends Statement { - override def toLines = List("assert " + e + "; // " + position.toString) +case class AssertStmt(e: Expr, id : Option[Identifier], decorators: List[ExprDecorator]) extends Statement { + override def toLines = { + val name = "assert" + val decoratorStr = if (decorators.size > 0) { + " [" + Utils.join(decorators.map(_.toString()), ", ") + "] : " + } else { " " } + val prefix = id match { + case Some(n) => + if (decorators.nonEmpty) { + name + " " + n.toString() + decoratorStr + } + else { + name + " " + n.toString() + " : " + } + case None => name + decoratorStr + } + List(prefix + e.toString() + "; // " + position.toString) + } override val hasCall = false override val hasInternalCall = false override val hashId = 3001 @@ -1681,10 +1701,10 @@ case class AxiomDecl(id : Option[Identifier], expr: Expr, params: List[ExprDecor override val hashId = 3918 override val md5hashCode = computeMD5Hash(id, expr, params) override def toString = { - id match { + (id match { case Some(id) => "axiom " + id.toString + " : " + expr.toString() case None => "axiom " + expr.toString - } + }) + "; // " + pos.toString() } override def declNames = id match { case Some(i) => List(i) @@ -1732,7 +1752,7 @@ case class GenericProofCommand( override def toString = { val nameStr = name.toString val paramStr = if (params.size > 0) { "[" + Utils.join(params.map(_.toString), ", ") + "]" } else { "" } - val argStr = if (args.size > 0) { "(" + Utils.join(args.map(_.toString), ", ") + ")" } else { "" } + val argStr = if (args.size > 0) { "(" + Utils.join(args.map(a => a._1.toString + " /* " + a._2 + "*/"), ", ") + ")" } else { "" } val resultStr = resultVar match { case Some(id) => id.toString + " = "; case None => "" } val objStr = argObj match { case Some(id) => id.toString + "->"; case None => "" } resultStr + objStr + nameStr + paramStr + argStr + ";" + " // " + position.toString diff --git a/src/main/scala/uclid/lang/UclidParser.scala b/src/main/scala/uclid/lang/UclidParser.scala index 9b8d53249..808e836c0 100644 --- a/src/main/scala/uclid/lang/UclidParser.scala +++ b/src/main/scala/uclid/lang/UclidParser.scala @@ -83,7 +83,7 @@ trait UclidTokenParsers extends TokenParsers { elem("identifier", _.isInstanceOf[Identifier]) ^^ (_.chars) } -object UclidParser extends UclidTokenParsers with PackratParsers { +class UclidParser extends UclidTokenParsers with PackratParsers { type Tokens = UclidTokens val lexical = new UclidLexical @@ -180,7 +180,7 @@ object UclidParser extends UclidTokenParsers with PackratParsers { // lazy val TemporalOpWUntil = "W" // lazy val TemporalOpRelease = "R" - lexical.delimiters ++= List("(", ")", ",", "[", "]", + lexical.delimiters ++= List("(", ")", ",", "[", "]", "#[", "bv", "{", "}", ";", "=", ":", "::", ".", "*", "::=", "->", OpAnd, OpOr, OpBvAnd, OpBvOr, OpBvXor, OpBvNot, OpAdd, OpSub, OpMul, OpBiImpl, OpImpl, OpLT, OpGT, OpLE, OpGE, OpULT, OpUGT, OpULE, OpUGE, @@ -276,7 +276,7 @@ object UclidParser extends UclidTokenParsers with PackratParsers { lazy val Pattern : PackratParser[(lang.Identifier, List[List[lang.Expr]])] = Id ~ ("[" ~> PatternList <~ "]") ^^ { case id ~ pats => (id, pats) } - lazy val E1: PackratParser[Expr] = + lazy val E1: PackratParser[Expr] = KwForall ~> IdTypeList ~ Pattern.? ~ ("::" ~> E1) ^^ { case ids ~ pat ~ expr => { pat match { @@ -459,7 +459,18 @@ object UclidParser extends UclidTokenParsers with PackratParsers { lazy val Statement: PackratParser[Statement] = positioned { KwSkip <~ ";" ^^ { case _ => SkipStmt() } | - KwAssert ~> Expr <~ ";" ^^ { case e => AssertStmt(e, None) } | + KwAssert ~> Expr <~ ";" ^^ { case e => AssertStmt(e, None, List.empty) } | + KwAssert ~> ("[" ~> IdList <~ "]" ~ ":") ~ Expr <~ ";" ^^ { + case ids ~ e => + AssertStmt(e, None, ids.map(ExprDecorator.parse(_))) + } | + KwAssert ~> (Id <~ ":") ~ Expr <~ ";" ^^ { + case id ~ e => AssertStmt(e, Some(id), List.empty) + } | + KwAssert ~> (Id) ~ ("[" ~> IdList <~ "]" ~ ":") ~ Expr <~ ";" ^^ { + case id ~ ids ~ e => + AssertStmt(e, Some(id), ids.map(ExprDecorator.parse(_))) + } | KwAssume ~> Expr <~ ";" ^^ { case e => AssumeStmt(e, None) } | KwHavoc ~> Id <~ ";" ^^ { case id => HavocStmt(HavocableId(id)) } | Lhs ~ rep("," ~> Lhs) ~ "=" ~ Expr ~ rep("," ~> Expr) <~ ";" ^^ @@ -804,4 +815,12 @@ object UclidParser extends UclidTokenParsers with PackratParsers { case NoSuccess(msg, next) => throw new Utils.SyntaxError(msg, Some(next.pos), Some(filename)) } } +} + +object UclidParser { + val parserObj = new UclidParser() + def parseModel(filename: String, text: String): List[Module] = { + parserObj.parseModel(filename, text) } +} + diff --git a/src/main/scala/uclid/lang/WhileLoopRewriter.scala b/src/main/scala/uclid/lang/WhileLoopRewriter.scala index e492e686b..6c81b5fc5 100644 --- a/src/main/scala/uclid/lang/WhileLoopRewriter.scala +++ b/src/main/scala/uclid/lang/WhileLoopRewriter.scala @@ -47,7 +47,7 @@ class WhileLoopRewriterPass extends RewritePass { val invs = whileSt.invariants val initialAsserts = invs.map{ inv => { - ASTNode.introducePos(true, true, AssertStmt(inv, Some(Identifier("loop invariant (entry)"))), inv.position) + ASTNode.introducePos(true, true, AssertStmt(inv, Some(Identifier("loop invariant (entry)")), List.empty), inv.position) } } val varsToHavoc = StatementScheduler.writeSetIds(whileSt.body, context).toList @@ -59,7 +59,7 @@ class WhileLoopRewriterPass extends RewritePass { val assumeStmts = AssumeStmt(cond, None) :: invs.map(inv => AssumeStmt(inv, None)) val assertStmts = invs.map{ inv => { - ASTNode.introducePos(true, true, AssertStmt(inv, Some(Identifier("loop invariant (iteration)"))), inv.position) + ASTNode.introducePos(true, true, AssertStmt(inv, Some(Identifier("loop invariant (iteration)")), List.empty), inv.position) } } val finishAssump = AssumeStmt(Operator.not(cond), None) diff --git a/src/main/scala/uclid/smt/SMTLIB2Interface.scala b/src/main/scala/uclid/smt/SMTLIB2Interface.scala index 613054e88..b0670f02d 100644 --- a/src/main/scala/uclid/smt/SMTLIB2Interface.scala +++ b/src/main/scala/uclid/smt/SMTLIB2Interface.scala @@ -170,7 +170,7 @@ trait SMTLIB2Base { /** * Translates an smt operator to its string representation. * - * @opIn The smt operator to be translated. + * @param opIn The smt operator to be translated. */ def translateOp(opIn: Operator) : String = { opIn match { diff --git a/src/test/scala/VerifierSpec.scala b/src/test/scala/VerifierSpec.scala index 69769fc23..5ed949c23 100644 --- a/src/test/scala/VerifierSpec.scala +++ b/src/test/scala/VerifierSpec.scala @@ -434,6 +434,9 @@ class ModuleVerifSpec extends AnyFlatSpec { "issue-187b.ucl" should "verify all assertions." in { VerifierSpec.expectedFails("./test/issue-187b.ucl", 0) } + "test-redundant-assign.ucl" should "verify all assertions." in { + VerifierSpec.expectedFails("./test/test-redundant-assign.ucl", 0) + } } class LTLVerifSpec extends AnyFlatSpec { "test-history-1.ucl" should "verify all assertions." in { diff --git a/test/debug/mc.ucl b/test/debug/mc.ucl new file mode 100644 index 000000000..c50871535 --- /dev/null +++ b/test/debug/mc.ucl @@ -0,0 +1,17 @@ +module main{ + var arr_1: [integer]boolean; + var n_1: integer; + + init { + assert [cover, SATOnly]: + (true && (n_1 > 0) ==> + (forall (i : integer) :: (((i < 0) || (i >= n_1)) ==> !((arr_1)[i]))) && + (exists (i : integer) :: (((0 <= i) && (i < n_1)) && (arr_1)[i]))); + } + + control { + v = unroll(1); + check; + print_results; + } +} diff --git a/test/debug/mc2.ucl b/test/debug/mc2.ucl new file mode 100644 index 000000000..919c8d01e --- /dev/null +++ b/test/debug/mc2.ucl @@ -0,0 +1,24 @@ + module main { + define X (b: boolean): boolean = true; + function count_1(n: integer): integer; // line 0 + axiom assump_1 : (forall (n : integer) :: (count_1(n) >= 0)); // + function count_2(n: integer): integer; // line 0 + axiom assump_2 : (forall (n : integer) :: (count_2(n) >= 0)); // + + procedure countingProof() returns () + { + var arr : [integer]boolean; // line 22 + var n : integer; // line 22 + assert [cover, SATOnly]: + forall (n : integer) :: + (n > 0 && + (forall (i : integer) :: (i < 0 || i >= n) ==> !arr[i]) && + (exists (i : integer) :: 0 <= i < n && arr[i])); + } + control { + v = verify(countingProof /* countingProof*/); // line 0 + check; // line 0 + print_results; // line 0 + } + } + diff --git a/test/debug/mc3.ucl b/test/debug/mc3.ucl new file mode 100644 index 000000000..3ad825520 --- /dev/null +++ b/test/debug/mc3.ucl @@ -0,0 +1,19 @@ + +module main{ + init { + var arr_2 : [integer]boolean; // line 16 + var arr_3 : [integer]boolean; // line 16 + var n : integer; // line 16 + assert[cover]: + (((true && (forall (i : integer) :: !((arr_2)[i]))) && + (forall (i : integer) :: !((arr_3)[i]))) && + distinct({arr_2}, {arr_3})); // line 0 + + } + + control { + v = unroll(1); + check; + print_results; + } +} diff --git a/test/modelcounter/counting-zkhat.ucl b/test/modelcounter/counting-zkhat.ucl new file mode 100644 index 000000000..9b351dd0e --- /dev/null +++ b/test/modelcounter/counting-zkhat.ucl @@ -0,0 +1,41 @@ +// Model counting in ZK Hats - Motivating example in CAV 2020 paper + +module main { + + define V(Y : [integer]boolean, R : integer) : boolean = + (R >= 0) && (exists (i : integer) :: 0 <= i < R && Y[i]) + && (forall (i : integer) :: (i < 0 || i >= R) ==> !Y[i]); + + define Vf(Y : [integer]boolean, R : integer) : boolean = + (R >= 0) && (forall (i : integer) :: (i < 0 || i >= R) ==> !Y[i]); + + define V1(Y : [integer]boolean, R : integer) : boolean = + (R >= 0) && (forall (i : integer) :: !Y[i]); + + define W(i : integer) : boolean = 0 <= i < 2; + + proof { + // Proof rules 2 - 7 from paper. + + // 2. (Or) #Y. Vf(Y, R) = #Y. V(Y, R) + #Y.(V1(Y,R)) + assert or: #[(Y: [integer]boolean) for (R : integer)] :: (Vf(Y, R)) == + #[(Y: [integer]boolean) for (R : integer)] :: (V(Y, R)) + + #[(Y: [integer]boolean) for (R : integer)] :: (V1(Y, R)); + + // 3. (ConstEq) #Y. V1(Y, R) = 1 + assert constEq: R >= 0 ==> #[(Y: [integer]boolean) for (R: integer)] :: (V1(Y, R)) == 1; + + // 4. (ConstEq) #Y. Vf(Y, 1) = 2 + assert constEq: R == 1 ==> #[(Y: [integer]boolean) for (R: integer)] :: (Vf(Y, R)) == 2; + + // 5. (IndLB) #Y. Vf(Y, R) >= #i.W(i) * #Y. Vf(Y, R-1) + assert indLB: #[(Y: [integer]boolean) for (R: integer)] :: (Vf(Y, R + 1)) >= + #[(Y: [integer]boolean) for (R: integer)] :: (Vf(Y, R)) * + #[(i: integer) for (R: integer)] :: (W(i)) + skolems(Y[(R) -> (i == 1)]); + + // 6. (Range) #i. W(i) == 2 + assert range: #[(i: integer) for (R: integer)] :: (W(i)) == 2; + + } +} diff --git a/test/modelcounter/test-AndUB.ucl b/test/modelcounter/test-AndUB.ucl new file mode 100644 index 000000000..0c1e08038 --- /dev/null +++ b/test/modelcounter/test-AndUB.ucl @@ -0,0 +1,14 @@ +module main { + define f(n : integer) : boolean = 1 <= n < 10; + define g(n : integer) : boolean = 5 <= n < 10; + define h(n : integer, m : integer) : boolean = (1 <= n < 10) && (5 <= m < 10); + + proof { + assert andUB: #[(n: integer, m : integer)] :: (h(n, m)) <= + #[(n: integer)] :: (f(n)) * + #[(m: integer)] :: (g(m)); + } +} + + + diff --git a/test/modelcounter/test-UB.ucl b/test/modelcounter/test-UB.ucl new file mode 100644 index 000000000..4a0c822e3 --- /dev/null +++ b/test/modelcounter/test-UB.ucl @@ -0,0 +1,9 @@ +module main { + define f(n : integer) : boolean = 11 <= n < 21; + define g(n : integer) : boolean = 5 <= n < 21; + + proof { + assert UB: #[(n:integer)] :: (f(n)) <= #[(n:integer)] :: (g(n)); + } +} + diff --git a/test/modelcounter/test-constLB.ucl b/test/modelcounter/test-constLB.ucl new file mode 100644 index 000000000..95bed7400 --- /dev/null +++ b/test/modelcounter/test-constLB.ucl @@ -0,0 +1,9 @@ +module main { + + define f(n : integer) : boolean = 1 <= n < 10; + + proof { + assert constLB: #[(n:integer)] :: (f(n)) >= 5; + assert constLB: #[(a:bv1, b:bv1)] :: (a == b) >= 2; + } +} diff --git a/test/modelcounter/test-constUB.ucl b/test/modelcounter/test-constUB.ucl new file mode 100644 index 000000000..131ca6c88 --- /dev/null +++ b/test/modelcounter/test-constUB.ucl @@ -0,0 +1,6 @@ +module main { + + proof { + assert constUB: #[(a:bv1, b:bv1)] :: (a == b) < 3; + } +} diff --git a/test/modelcounter/test-disjoint.ucl b/test/modelcounter/test-disjoint.ucl new file mode 100644 index 000000000..5df6c3990 --- /dev/null +++ b/test/modelcounter/test-disjoint.ucl @@ -0,0 +1,11 @@ +module main { + define f(n : integer) : boolean = 1 <= n < 10; + define g(n : integer) : boolean = 5 <= n < 10; + define h(n : integer, m : integer) : boolean = (1 <= n < 10) && (5 <= m < 10); + + proof { + assert disjoint: #[(n: integer, m : integer)] :: (h(n, m)) == + #[(n: integer)] :: (f(n)) * + #[(m: integer)] :: (g(m)); + } +} \ No newline at end of file diff --git a/test/modelcounter/test-indLB.ucl b/test/modelcounter/test-indLB.ucl new file mode 100644 index 000000000..8dcd9cf67 --- /dev/null +++ b/test/modelcounter/test-indLB.ucl @@ -0,0 +1,11 @@ +module main { + define X(j: integer) : boolean = 0 <= j < 2; + define U(arr: [integer]integer, n: integer): boolean = + (n >= 0) && (forall (i: integer) :: (i < 0 || i >= n) ==> arr[i] == 0) && (forall (i: integer) :: (i >= 0 || i < n) ==> (0 <= arr[i] < 2)); + proof { + assert indLB: #[(arr: [integer]integer) for (n : integer)] :: (U(arr, n+1)) >= + #[(arr: [integer]integer) for (n : integer)] :: (U(arr, n)) * + #[(j : integer) for (n : integer)] :: (X(j)) + skolems (arr[n -> j]); + } +} \ No newline at end of file diff --git a/test/modelcounter/test-indUB.ucl b/test/modelcounter/test-indUB.ucl new file mode 100644 index 000000000..0d0e4eba8 --- /dev/null +++ b/test/modelcounter/test-indUB.ucl @@ -0,0 +1,11 @@ +module main { + define X(j: integer) : boolean = 0 <= j < 2; + define U(arr: [integer]integer, n: integer): boolean = + (n >= 0) && (forall (i: integer) :: (i < 0 || i >= n) ==> arr[i] == 0) && (forall (i: integer) :: (i >= 0 || i < n) ==> (0 <= arr[i] < 2)); + proof { + assert indUB: #[(arr: [integer]integer) for (n : integer)] :: (U(arr, n+1)) <= + #[(arr: [integer]integer) for (n : integer)] :: (U(arr, n)) * + #[(j : integer) for (n : integer)] :: (X(j)) + skolems (arr[n -> 0], arr[n]); + } +} diff --git a/test/modelcounter/test-injectivity.ucl b/test/modelcounter/test-injectivity.ucl new file mode 100644 index 000000000..349f09ae4 --- /dev/null +++ b/test/modelcounter/test-injectivity.ucl @@ -0,0 +1,8 @@ +module main { + define f(n : integer) : boolean = 1 <= n < 10; + define g(n : integer) : boolean = 15 <= n < 30; + + proof { + assert injectivity: #[(n: integer)] :: (f(n)) <= #[(m: integer)] :: (g(m)) skolems(n+14); + } +} \ No newline at end of file diff --git a/test/modelcounter/test-or.ucl b/test/modelcounter/test-or.ucl new file mode 100644 index 000000000..e2fc2b748 --- /dev/null +++ b/test/modelcounter/test-or.ucl @@ -0,0 +1,11 @@ +module main { + + define f(n : integer) : boolean = 5 <= n < 21; + define g(n : integer) : boolean = 11 <= n < 21; + define h(n : integer) : boolean = 5 <= n < 11; + + proof { + assert or: #[(n:integer) for ()] :: (f(n)) == + #[(n:integer)] :: (g(n)) + #[(n:integer)] :: (h(n)); + } +} diff --git a/test/modelcounter/test-range-symb.ucl b/test/modelcounter/test-range-symb.ucl new file mode 100644 index 000000000..a5a27398b --- /dev/null +++ b/test/modelcounter/test-range-symb.ucl @@ -0,0 +1,8 @@ +module main { + + define f(i : integer, j: integer, R: integer) : boolean = j <= i < R; + + proof { + assert range: (j > 0 && R > j) ==> #[(i: integer) for (j: integer, R: integer)] :: (f(i, j, R)) == (R - j); + } +} diff --git a/test/modelcounter/test-range.ucl b/test/modelcounter/test-range.ucl new file mode 100644 index 000000000..4a25a259a --- /dev/null +++ b/test/modelcounter/test-range.ucl @@ -0,0 +1,8 @@ +module main { + + define f(n : integer) : boolean = 1 <= n < 21; + + proof { + assert range: #[(n:integer)] :: (f(n)) == 20; + } +} diff --git a/test/test-redundant-assign.ucl b/test/test-redundant-assign.ucl new file mode 100644 index 000000000..53b70b945 --- /dev/null +++ b/test/test-redundant-assign.ucl @@ -0,0 +1,31 @@ +module main { + + var index: integer; + var myArray: [integer]integer; + + procedure shouldPass() + modifies myArray, index; + { + index = 1; + myArray[index] = 0; + assert(myArray[1] == 0); // this assertion should pass + } + + procedure shouldPass2() + modifies myArray, index; + { + index = 1; + myArray[index] = 0; + assert(myArray[1] == 0); // this assertion should pass + index = 2; // assignment should be ignored + } + + + control { + v = verify(shouldPass); + v = verify(shouldPass2); + check; + print_results; + v.print_cex(index); + } +} diff --git a/vim/uclid.vim b/vim/uclid.vim index 5c2977dae..c16efd22b 100644 --- a/vim/uclid.vim +++ b/vim/uclid.vim @@ -21,6 +21,7 @@ syn keyword ucl4Decl module init next control function procedure retu syn keyword ucl4Cmd unroll lazysc check print_module print_cex print_results k_induction_base k_induction_step induction clear_context synthesize_invariant set_solver_option " user labels syn keyword ucl4Constant false true +syn keyword ucl4Count proof range constUB constLB constEq UB andUB disjoint or injectivity indLB indUB skolems lemmas lemma syn match ucl4Identifier display "[A-Za-z_][A-Za-z0-9_]*" @@ -41,7 +42,7 @@ syn match ucl4Number "\<\d\+bv\d\+\>" syn match ucl4Number "\<0[xX][0-9A-F]\+bv\d\+\>" syn match ucl4Number "\<0[bB][01]\+bv\d\+\>" syn match ucl4Delimiter "\[\|\]\|(\|)" -syn match ucl4Operator "=\|==\|+\|-\|*\|&&\|||\|^\|!\|==>\|<==>\|<\|<=\|>\|>=" +syn match ucl4Operator "=\|==\|+\|-\|*\|&&\|||\|^\|!\|==>\|<==>\|<\|<=\|>\|>=\|#" syn match ucl4UComparator "<_u\|<=_u\|>_u\|>=_u" syn region ucl4MultilineComment start="/\*" end="\*/" @@ -63,5 +64,6 @@ hi def link ucl4Cmd Define hi def link ucl4Operator Special hi def link ucl4Delimiter Normal hi def link ucl4Number Number +hi def link ucl4Count Keyword let b:current_syntax = "ucl"