Model Counting extension

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 <[email protected]>
+Date:   Tue Oct 27 15:12:03 2020 -0700
+
+    fixes mistake in previous commit
+
+commit 6502265e4a85688ff92d963419c1957ef3cb73b5
+Author: polgreen <[email protected]>
+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. 

README.md

@@ -12,12 +12,14 @@ Sanjit A. Seshia and Pramod Subramanyan. <font color="blue">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
+## <a name="prereqs"></a> 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
+## <a name="prebuilt"></a> Download Pre-Built Binaries
 
 Download the latest stable pre-built package from [releases tab](https://github.com/uclid-org/uclid/releases).
 
-## Building From Source
+## <a name="srcbuild"></a> 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
 

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))

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())

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 {

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.