v0.9.5 of uclid5.

What's new?

+ Much improved tutorial.
+ Initial support for SyGuS
+ New operators (distinct, bv_sign_extend, bv_zero_extend).
+ Local scoped variables are allowed in every block now.
+ We have the beginnings of an optimizer.
+ Lots and lots and lots of bugfixes.

Author: pramodsu

README.md

@@ -16,7 +16,7 @@ Download the latest stable pre-built package from [releases tab](https://github.
 
 # Install From Source
 
-Or, you could clone this repository and build 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.
 
 ## Compiling uclid5
 

build.sbt

@@ -1,5 +1,5 @@
 name := "uclid"
-version := "0.9.1"
+version := "0.9.5"
 scalaVersion := "2.12.0"
 
 scalacOptions += "-feature"

examples/README

@@ -25,3 +25,11 @@ setuid.ucl
 setuid_fixed.ucl
  - This is a "fixed" version of the setuid model.
 
+two-safety.ucl
+ - This is an example of verifying a simple hyperproperty (a 2-safety property)
+   by self-composition. It is based on an example in Chapter 17 of Lee & Seshia.
+
+simple-datapath.ucl
+  - This is an example from the original UCLID work on processor verification (Bryant, Lahiri, Seshia, CAV'02),
+    showing Burch-Dill style correspondence (refinement) checking.
+

examples/cpu_induction.ucl

@@ -26,11 +26,12 @@ module common {
 }
 
 module cpu {
-  type addr_t = common.addr_t;
-  type mem_t  = common.mem_t;
-  type word_t = common.word_t;
-  type op_t   = common.op_t;
-  type mode_t = common.mode_t;
+  // type addr_t = common.addr_t;
+  // type mem_t  = common.mem_t;
+  // type word_t = common.word_t;
+  // type op_t   = common.op_t;
+  // type mode_t = common.mode_t;
+  type * = common.*;
 
   type regindex_t;
   type regs_t = [regindex_t]word_t;
@@ -168,7 +169,7 @@ module main {
   type mode_t     = common.mode_t;
   type regindex_t = cpu.regindex_t;
 
-  // Instruction memory is the same for both CPUs.
+  // Instruction memory for the CPUs.
   var imem1, imem2 : mem_t;
 
   // Create two instances of the CPU module.

examples/crypto.ucl

@@ -0,0 +1,35 @@
+module main
+{
+  type plaintext_t;
+  type ciphertext_t;
+  type key_t;
+
+  const pt       : plaintext_t;
+  var   ct       : ciphertext_t;
+  var   sk       : key_t; // secret key
+
+  input ik       : key_t; // input key
+  var   dt       : plaintext_t; // "decoded" text
+
+  function enc(k : key_t, pt : plaintext_t)  : ciphertext_t;
+  function dec(k : key_t, ct : ciphertext_t) : plaintext_t;
+
+  axiom dec_enc : 
+    (forall (k1, k2 : key_t, p : plaintext_t) ::
+        (dec(k2, enc(k1, p)) == p) <==> (k1 == k2));
+
+  init {
+    ct = enc(sk, pt);
+  }
+
+  next {
+    dt' = dec(ik, ct);
+    assert (dt' == pt) ==> (ik == sk);
+  }
+
+  control {
+    v = unroll(5);
+    check;
+    print_results;
+  }
+}

examples/simple-datapath.ucl

@@ -0,0 +1,243 @@
+// Simple pipelined datapath, based on old uclid model in the old UCLID user manual 
+
+module common {
+  // Types
+  // Words -- Addresses, Data, etc.
+  type word_t = bv32;
+  // Registers
+  type reg_t = bv8; // arbit choice
+  // Register file  
+  type rf_t = [reg_t]word_t;
+  // OpCode 
+  type op_t = bv8;  // arbit choice
+
+  // Uninterpreted functions
+  function newPC(a: word_t)  : word_t;
+  const pc0 : word_t;
+  function rf0 (r : reg_t) : word_t;
+  function src1 (i : word_t) : reg_t;
+  function src2 (i : word_t) : reg_t;
+  function dest (i : word_t) : reg_t;
+  function op (i : word_t) : op_t; 
+  function alu (op : op_t, arg1: word_t, arg2 : word_t) : word_t;
+
+}
+
+// Specification/ISA model
+module spec {
+
+  input proj_impl : boolean;
+  input impl_RF : common.rf_t;
+  input impl_PC : common.word_t;
+
+  var sPC : common.word_t;
+  var sRF : common.rf_t;
+
+  procedure update_sRF() 
+    modifies sRF;
+  {
+      sRF[common.dest(sPC)] = common.alu(common.op(sPC),
+	      			         sRF[common.src1(sPC)],
+					 sRF[common.src2(sPC)]);
+  }
+
+  init {
+    sPC = common.pc0;
+    assume (forall (i : common.reg_t) :: (sRF[i] == common.rf0(i)));
+  }
+ 
+  next {
+    if (proj_impl) {
+      sPC' = impl_PC;
+      sRF' = impl_RF;
+    }
+    else {
+      sPC' = common.newPC(sPC);
+      call update_sRF();
+    }
+  }
+}
+
+// Pipeline model
+module impl {
+
+  input flush : boolean;
+  input reinit : boolean;
+
+  var pPC : common.word_t;
+  var pRF : common.rf_t;
+  var eOP : common.op_t; 
+  var eSRC2 : common.reg_t;
+  var eDEST : common.reg_t;
+  var eARG1 : common.word_t;
+  var eARG2 : common.word_t;
+  var eWRT : boolean;
+  var wVAL : common.word_t;
+  var wDEST : common.reg_t;
+  var wWRT : boolean;
+
+  const op0 : common.op_t;
+  const s0, d0, d1 : common.reg_t;
+  const a1, a2, x0 : common.word_t;
+  const w0, w1 : boolean;
+
+  procedure update_pRF() 
+    modifies pRF;
+  {
+    if (wWRT) { pRF[wDEST] = wVAL; }
+  }
+
+  define stall() : boolean = eWRT && (common.src1(pPC) == eDEST);
+
+  init {
+    // initialize PC and RF same as spec module
+    pPC = common.pc0;
+    assume (forall (i : common.reg_t) :: (pRF[i] == common.rf0(i)));
+    // all other state variables get arbit symbolic initialization 
+    eOP = op0;
+    eSRC2 = s0;
+    eARG1 = a1;
+    eARG2 = a2;
+    eDEST = d0;
+    eWRT = w0;
+    wVAL = x0;
+    wDEST = d1;
+    wWRT = w1;
+  }
+
+  
+  next {
+   if (reinit) {
+    pPC' = common.pc0;
+    havoc pRF;
+    assume (forall (i : common.reg_t) :: (pRF'[i] == common.rf0(i)));
+    // all other state variables get same arbit symbolic initialization as before
+    eOP' = op0;
+    eSRC2' = s0;
+    eARG1' = a1;
+    eARG2' = a2;
+    eDEST' = d0;
+    eWRT' = w0;
+    wVAL' = x0;
+    wDEST' = d1;
+    wWRT' = w1;
+   } 
+   else { 
+    // updates to PC and RF
+    if ((!flush) && (! stall())) { pPC' = common.newPC(pPC); }
+    call update_pRF();
+    // Execute stage
+    eOP' = common.op(pPC);
+    eSRC2' = common.src2(pPC);
+    eARG1' = pRF'[common.src1(pPC)];
+    eARG2' = pRF'[common.src2(pPC)];
+    eDEST' = common.dest(pPC);
+    eWRT' = (!stall()) && (!flush);
+    // Writeback stage
+    wDEST' = eDEST;
+    wWRT' = eWRT;
+    if (wWRT && (wDEST == eSRC2)) // fwding logic
+    {
+      wVAL' = common.alu(eOP,eARG1,wVAL);
+    } 
+    else {
+      wVAL' = common.alu(eOP,eARG1,eARG2);
+    }
+   }
+  }
+
+}
+
+// Main module
+module main {
+
+  var flush_pipeline : boolean;
+  var reinit : boolean;
+  var project_impl : boolean;
+  
+  var step : integer;
+
+  // Variables to store impl state
+  var I_pc : common.word_t;
+  var I_rf : common.rf_t;
+  // Variables to store spec state
+  var S_pc0 : common.word_t; // after 0 steps
+  var S_rf0 : common.rf_t;
+  var S_pc1 : common.word_t; // after 1 step
+  var S_rf1 : common.rf_t;
+
+  // instantiate spec and impl modules
+  instance impl_i : impl(flush : (flush_pipeline), reinit : (reinit));
+  instance spec_i : spec(proj_impl : (project_impl), impl_RF : (impl_i.pRF), impl_PC : (impl_i.pPC));
+
+  init {
+    step = 0;
+    flush_pipeline = false;
+    project_impl = false;
+    reinit = false;
+  }
+
+  next {
+    step' = step + 1;
+    case
+      (step == 0) : { 
+         flush_pipeline' = true; 
+         next(impl_i);  // step impl module, normal step
+      }
+      (step == 1) : { 
+         flush_pipeline' = true; 
+         next(impl_i);  // step impl module, flush
+      }
+      (step == 2) : { 
+         flush_pipeline' = false; 
+         reinit' = true;
+         next(impl_i);  // step impl module, flush
+      }
+      (step == 3) : { 
+         flush_pipeline' = true; 
+         reinit' = false;
+         I_pc' = impl_i.pPC; // store impl state after pipeline flushed for 2 steps
+         I_rf' = impl_i.pRF;
+         next(impl_i);  // step impl module, reinitialize
+      }
+      (step == 4) : { 
+         flush_pipeline' = true; 
+         next(impl_i);  // step impl module, flush
+      }
+      (step == 5) : { 
+         flush_pipeline' = false; 
+         project_impl' = true; 
+         next(impl_i);  // step impl module, flush
+      }
+      (step == 6) : { 
+         project_impl' = false;
+         next(spec_i); // step spec to project impl state onto spec
+      }
+      (step == 7) : { // step spec module
+         S_pc0' = spec_i.sPC; // initial state of spec
+         S_rf0' = spec_i.sRF;
+         next(spec_i); // step
+      }
+      (step == 8) : { // store spec state after one step
+         S_pc1' = spec_i.sPC;
+         S_rf1' = spec_i.sRF;
+      }
+      (step == 9) : { 
+         // assert(false); // sanity check to make sure execution can get here
+         // correspondence check
+         assert(((S_pc1 == I_pc) && (S_rf1 == I_rf)) || ((S_pc0 == I_pc) && (S_rf0 == I_rf)));
+      }
+    esac;
+
+  }
+
+
+  control {
+    vobj = unroll(10);
+    check;
+    print_results;
+    vobj.print_cex(step, flush_pipeline, reinit, project_impl, I_pc, I_rf, S_pc0, S_rf0, S_pc1, S_rf1, impl_i.pPC, impl_i.pRF, spec_i.sPC, spec_i.sRF, impl_i.wVAL);
+  }
+
+
+}

examples/tutorial/ex2.1-alu.ucl

@@ -21,6 +21,8 @@ module main {
     call set_init_state(); 
   }
 
+  define double(arg : bv8) : bv8 = (arg + arg);
+
   procedure exec_cmd() 
     returns (r : result_t)
     modifies regs;
@@ -39,12 +41,12 @@ module main {
 
   next {
     call (result') = exec_cmd();
-    cnt' = cnt + cnt;
+    cnt' = double(cnt);
   }
 
   assume regindex_zero    : (r1 == 0bv3 && r2 == 0bv3);
   assume cmd_is_add       : (cmd == add) && valid;
-  invariant result_eq_cnd : (cnt == result.value);
+  invariant result_eq_cnt : (cnt == result.value);
 
   control {
     f = unroll (5);

examples/tutorial/ex3.4-fib-model-revisited.ucl

@@ -1,5 +1,5 @@
 module main {
-  // System description. blah
+  // System description. 
   var a, b   : integer;
   const flag : boolean;