New release with several bugfixes.

CONTRIBUTORS.md

@@ -5,6 +5,8 @@
 | Pramod Subramanyan | [email protected] |
 | Sanjit Seshia      | [email protected] |
 | Rohit Sinha        | [email protected]  |
+| Kevin Cheang       | [email protected]      |
+| Cameron Rasmussen  | [email protected]   |
 
 ## Other Contributors
 

README.md

@@ -4,7 +4,7 @@
 
 The [tutorial](https://github.com/uclid-org/uclid/blob/master/tutorial/tutorial.pdf) has a gentle introduction to using uclid5.
 
-If you use uclid5 in your own research, it is suggested that you cite the following MEMOCODE 2018 paper.
+If you use uclid5 in your work, please cite the following MEMOCODE 2018 paper:
 
 Sanjit A. Seshia and Pramod Subramanyan. <font color="blue">UCLID5: Integrating Modeling, Verification, Synthesis and Learning.</font>
  [\[PDF\]](https://cse.iitk.ac.in/users/spramod/papers/memocode18.pdf)    
@@ -18,6 +18,17 @@ You will need the [Z3 SMT solver](https://github.com/Z3Prover/z3) to be installe
 
 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).
 
+### Mac OS X El Capitan or up
+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. 
+
+To fix this issue, put:
+- JNI dynamic link libraries (e.g libz3java.dylib) in:       /Library/Java/Extensions
+- non-JNI dynamic link libraries (e.g libz3.dylib) in:      /usr/local/lib
+
+For more information on the resolution of this issue, please refer to:
+https://github.com/Z3Prover/z3/issues/294
+
+
 ## Download Pre-Built Binaries
 
 Download the latest stable pre-built package from [releases tab](https://github.com/uclid-org/uclid/releases).
@@ -40,7 +51,7 @@ If compilation and tests pass, you can build a universal package.
 
 This will create uclid/target/universal/uclid-0.8.zip, which contains the uclid binary in the bin/ subdirectory. Unzip this file, and add it to your path.
 
-## Installing uclid5
+## Installing and Running uclid5
 
     $ unzip uclid-0.9.5.zip
     $ cd uclid-0.9.5

build.sbt

@@ -1,18 +1,19 @@
 name := "uclid"
 version := "0.9.5"
-scalaVersion := "2.12.6"
+maintainer := "[email protected]"
+scalaVersion := "2.12.7"
 
 scalacOptions += "-feature"
 scalacOptions += "-unchecked"
 scalacOptions += "-deprecation"
 
 resolvers += "Artima Maven Repository" at "http://repo.artima.com/releases"
 
-libraryDependencies += "com.typesafe.scala-logging" %% "scala-logging" % "3.8.0"
+libraryDependencies += "com.typesafe.scala-logging" %% "scala-logging" % "3.9.0"
 libraryDependencies += "ch.qos.logback" % "logback-classic" % "1.2.3"
-libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.6" withSources()
-libraryDependencies += "org.scalactic" %% "scalactic" % "3.0.1"
-libraryDependencies += "org.scalatest" %% "scalatest" % "3.0.1" % "test"
+libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "1.1.1" withSources()
+libraryDependencies += "org.scalactic" %% "scalactic" % "3.0.5"
+libraryDependencies += "org.scalatest" %% "scalatest" % "3.0.5" % "test"
 libraryDependencies += "com.github.scopt" %% "scopt" % "3.7.0"
 
 enablePlugins(JavaAppPackaging)

examples/dining-philosophers-deadlocked.ucl

@@ -0,0 +1,115 @@
+module main {
+
+       var fork_taken : [bv2]boolean;
+       var num_forks  : [bv2]bv2;
+       var eaten      : [bv2]boolean;
+
+
+       var got_forks_left : [bv2]boolean;
+       var got_forks_right : [bv2]boolean;
+
+
+       init {
+            fork_taken = const(false, [bv2]boolean);
+            num_forks = const(0bv2, [bv2]bv2);
+            eaten = const(false, [bv2]boolean);
+            got_forks_left = const(false, [bv2]boolean);
+            got_forks_right = const(false, [bv2]boolean);
+       }
+
+
+       procedure acquire_left(i: bv2)
+        returns (success: boolean)
+        modifies fork_taken;
+       {
+            success = false;
+            if (fork_taken[i - 1bv2] == false) {
+               fork_taken[i - 1bv2] = true;
+               success = true;
+            }
+       }
+
+
+       procedure acquire_right(i: bv2)
+        returns (success: boolean)
+        modifies fork_taken;
+        {
+            success = false;
+            if (fork_taken[i] == false) {
+               fork_taken[i] = true;
+               success = true;
+            }
+        }
+
+       input i: bv2;
+       input tryLeft : boolean;
+       input tryRight: boolean;
+
+       procedure get_forks(i: bv2)
+        modifies fork_taken, num_forks, got_forks_left, got_forks_right;
+        {
+                var got_fork : boolean;
+
+                // each philosopher tries to acquire left fork first and then right fork
+
+                if (tryLeft && !got_forks_left[i]) {
+                   call (got_fork) = acquire_left(i);
+                   if (got_fork) {
+                      num_forks[i] = num_forks[i] + 1bv2;
+                      got_forks_left[i] = true;
+                   }
+                }
+
+                if (tryRight && got_forks_left[i] && !got_forks_right[i]) {
+                   call (got_fork) = acquire_right(i);
+                   if (got_fork) {
+                      num_forks[i] = num_forks[i] + 1bv2;
+                      got_forks_right[i] = true;
+                   }
+                }
+        }
+
+       procedure release_forks(i: bv2)
+        modifies num_forks, fork_taken, got_forks_left, got_forks_right;
+        {
+                // releases the forks after philosopher has eaten once
+                // and again competes to acquire the forks
+                num_forks[i] = 0bv2;
+                fork_taken[i] = false;
+                fork_taken[i - 1bv2] = false;
+                got_forks_right[i] = false;
+                got_forks_left[i] = false;
+        }
+
+        next {
+
+             if (eaten[i] == false) {
+                // try acquiring two forks
+                call get_forks(i);
+                if (num_forks[i] == 2bv2) { eaten' = eaten[i -> true]; }
+             }
+             else {
+                call release_forks(i);
+                eaten' = eaten[i -> false];
+             }
+        }
+
+        // Given all resource has been consumed and all users have tried,
+        // then atleast one philosopher has succeed
+        // (i.e. no deadlock, however starvation is possible)
+        property[LTL] someone_eats:
+
+                G ( F(i == 0bv2) && F ((i == 1bv2)) && F(i == 2bv2) && F(i == 3bv2) &&
+                    F(fork_taken[0bv2] == true) &&   F(fork_taken[1bv2] == true) &&
+                    F(fork_taken[2bv2] == true) &&  F(fork_taken[3bv2] == true))
+                        ==>  F(eaten[0bv2] || eaten[1bv2] || eaten[2bv2] || eaten[3bv2]);
+
+
+
+        control {
+                v = bmc(8);
+                check;
+                print_results;
+                v.print_cex(i, tryLeft, tryRight, got_forks_left, got_forks_right, fork_taken, num_forks, eaten);
+        }
+}

examples/dining-philosophers-no-deadlock.ucl

@@ -0,0 +1,105 @@
+module main {
+
+       var fork_taken : [bv2]boolean;
+       var num_forks  : [bv2]bv2;
+       var eaten      : [bv2]boolean;
+
+
+       var got_forks_left : [bv2]boolean;
+       var got_forks_right : [bv2]boolean;
+
+
+       init {
+            fork_taken = const(false, [bv2]boolean);
+            num_forks = const(0bv2, [bv2]bv2);
+            eaten = const(false, [bv2]boolean);
+            got_forks_left = const(false, [bv2]boolean);
+            got_forks_right = const(false, [bv2]boolean);
+       }
+
+
+       procedure acquire_left(i: bv2)
+        returns (success: boolean)
+        modifies fork_taken;
+       {
+            success = false;
+            if (fork_taken[i - 1bv2] == false) {
+               fork_taken[i - 1bv2] = true;
+               success = true;
+            }
+       }
+
+
+       procedure acquire_right(i: bv2)
+        returns (success: boolean)
+        modifies fork_taken;
+        {
+            success = false;
+            if (fork_taken[i] == false) {
+               fork_taken[i] = true;
+               success = true;
+            }
+        }
+
+       input i: bv2;
+       input tryLeft : boolean;
+       input tryRight: boolean;
+
+       procedure get_forks(i: bv2)
+        modifies fork_taken, num_forks, got_forks_left, got_forks_right;
+        {
+                var got_fork : boolean;
+
+                // Philosophers either gets both forks or none
+
+                if (tryLeft && tryRight && !fork_taken[i-1bv2] && !fork_taken[i]) {
+                   num_forks[i] = num_forks[i] + 2bv2;
+                   got_forks_left[i] = true;
+                   got_forks_right[i] = true;
+                }
+        }
+
+       procedure release_forks(i: bv2)
+        modifies num_forks, fork_taken, got_forks_left, got_forks_right;
+        {
+                // releases the forks after philosopher has eaten once
+                // and again competes to acquire the forks
+                num_forks[i] = 0bv2;
+                fork_taken[i] = false;
+                fork_taken[i - 1bv2] = false;
+                got_forks_right[i] = false;
+                got_forks_left[i] = false;
+        }
+
+        next {
+
+             if (eaten[i] == false) {
+               // try acquiring two forks
+               call get_forks(i);
+
+               if (num_forks[i] == 2bv2) { eaten' = eaten[i -> true]; }
+             } else {
+                            call release_forks(i);
+                            eaten' = eaten[i -> false];
+             }
+        }
+
+        // Given all resource has been consumed and all users have tried,
+        // then atleast one philosopher has succeed
+        // (i.e. no deadlock, however starvation is possible)
+        property[LTL] someone_eats:
+
+                G ( F(i == 0bv2) && F ((i == 1bv2)) && F(i == 2bv2) && F(i == 3bv2) &&
+                    F(fork_taken[0bv2] == true) &&   F(fork_taken[1bv2] == true) &&
+                    F(fork_taken[2bv2] == true) &&  F(fork_taken[3bv2] == true))
+                        ==>  F(eaten[0bv2] || eaten[1bv2] || eaten[2bv2] || eaten[3bv2]);
+
+
+
+        control {
+                v = bmc(12);
+                check;
+                print_results;
+                v.print_cex(i, tryLeft, tryRight, fork_taken, num_forks, eaten);
+        }
+}

examples/fib2safety.ucl

@@ -0,0 +1,44 @@
+module fib
+{
+    var a, b : integer;
+
+    init {
+        assume (a >= 0);
+        assume (b >  0);
+        assume (a <= b);
+    }
+
+    next {
+        a' = b;
+        b' = a + b;
+    }
+}
+
+module main
+{
+    instance fib1 : fib();
+    instance fib2 : fib();
+
+    init {
+        assume (fib1.a == fib2.a && fib1.b == fib2.b);
+    }
+
+    next {
+        next (fib1);
+        next (fib2);
+    }
+
+    property b_are_eq : fib1.b == fib2.b;
+    property a_are_eq : fib1.a == fib2.a;
+    property b_gt_0  : fib1.b > 0 && fib2.b > 0;
+    property a_ge_0  : fib1.a >= 0 && fib2.a >= 0;
+    property a_le_b  : fib1.a <= fib1.b && fib2.a <= fib2.b;
+
+    control {
+        v = unroll(5);
+        // v = induction;
+        check;
+        print_results;
+        v.print_cex(fib1.a, fib1.b, fib2.a, fib2.b);
+    }
+}

examples/hash.ucl

@@ -0,0 +1,54 @@
+module main
+{
+  function hash(d1 : integer, h1 : integer) : integer;
+
+  axiom forall (d1 : integer, d2 : integer, h1 : integer, h2 : integer) 
+    pattern[hash(d1, h1), hash(d2, h2)]
+    :: (d1 == d2 && h1 == h2) <==> hash(d1, h1) == hash(d2, h2);
+
+  var dcopy : [integer]integer;
+  var data  : [integer]integer;
+  var dhash : integer;
+
+  procedure compute_hash(d : [integer]integer)
+    returns (h : integer)
+  {
+    var h1, h2 : integer;
+    h1 = hash(d[1], d[2]);
+    h2 = hash(d[3], d[4]);
+    h  = hash(h1, h2);
+  }
+
+  init {
+    dcopy = data;
+    call (dhash) = compute_hash(data);
+    data[0] = dhash;
+  }
+
+  next {
+    var idx  : integer;
+    var dat  : integer;
+    var arr1 : [integer]integer;
+    var arrh : integer;
+
+    // havoc the index idx with dat.
+    arr1 = data[idx -> dat];
+    // update the hash
+    call (arrh) = compute_hash(arr1);
+    // store the hash.
+    data' = arr1[0 -> arrh];
+  }
+
+  invariant init_hash:
+    dhash == hash(hash(dcopy[1], dcopy[2]), hash(dcopy[3], dcopy[4]));
+  invariant eq_data :
+    (data[0] == dhash) ==> (data[1] == dcopy[1] && data[2] == dcopy[2] && 
+                            data[3] == dcopy[3] && data[4] == dcopy[4]);
+
+  control {
+    set_solver_option(":mbqi", false);
+    v = induction(1);
+    check;
+    print_results;
+  }
+}

project/plugins.sbt

@@ -1,5 +1,5 @@
 // this adds the native packager.
-addSbtPlugin("com.typesafe.sbt" % "sbt-native-packager" % "1.3.1")
+addSbtPlugin("com.typesafe.sbt" % "sbt-native-packager" % "1.3.14")
 // this helps create eclipse projects.
-addSbtPlugin("com.typesafe.sbteclipse" % "sbteclipse-plugin" % "5.2.3")
+addSbtPlugin("com.typesafe.sbteclipse" % "sbteclipse-plugin" % "5.2.4")