SMT: Make path conditionals more precise

Previously path conditionals for a node were defined as the path
conditional of the immediate dominator (+ a guard for explicit guard
nodes after conditional branches), whereas now they are the path
conditional of the immediate dominator plus an expression
encapsulating all the guards between the immediate dominator and the
node. This is needed as the previous method was incorrect for certain
control flow graphs.

This slows down the generated SMT massively, because it causes the
path conditionals to become huge when the immediate dominator is far
away from the node in question. It also changes computing path
conditionals from O(n) to O(n^2) which is not ideal as our inlined
graphs can become massive. Need to figure out a better way to generate
minimal path conditionals between the immediate dominator and the
node.

I upped the timeout for the SMT tests from 20s to 300s each but this
may still cause a failure in Jenkins because that machine is slow.

3 files changed, 66 insertions, 2 deletions

diff --git a/test/smt/encdec.sat.sail b/test/smt/encdec.sat.sail
new file mode 100644
index 00000000..d34f3629
--- /dev/null
+++ b/test/smt/encdec.sat.sail
@@ -0,0 +1,64 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+$include <mapping.sail>
+
+type regbits  = bits(5)
+
+val reg_name : bits(5) <-> string
+mapping reg_name = {
+  0b00000 <-> "zero",
+  0b00001 <-> "ra",
+  0b00010 <-> "sp",
+  0b00011 <-> "gp",
+  0b00100 <-> "tp",
+  0b00101 <-> "t0",
+  0b00110 <-> "t1",
+  0b00111 <-> "t2",
+  0b01000 <-> "fp",
+  0b01001 <-> "s1",
+  0b01010 <-> "a0",
+  0b01011 <-> "a1",
+  0b01100 <-> "a2",
+  0b01101 <-> "a3",
+  0b01110 <-> "a4",
+  0b01111 <-> "a5",
+  0b10000 <-> "a6",
+  0b10001 <-> "a7",
+  0b10010 <-> "s2",
+  0b10011 <-> "s3",
+  0b10100 <-> "s4",
+  0b10101 <-> "s5",
+  0b10110 <-> "s6",
+  0b10111 <-> "s7",
+  0b11000 <-> "s8",
+  0b11001 <-> "s9",
+  0b11010 <-> "s10",
+  0b11011 <-> "s11",
+  0b11100 <-> "t3",
+  0b11101 <-> "t4",
+  0b11110 <-> "t5",
+  0b11111 <-> "t6"
+}
+
+enum uop = RISCV_LUI | RISCV_AUIPC
+
+mapping utype_mnemonic : uop <-> string = {
+  RISCV_LUI   <-> "lui",
+  RISCV_AUIPC <-> "auipc"
+}
+
+val assembly : ast <-> string
+
+scattered union ast
+
+union clause ast = UTYPE : (bits(20), regbits, uop)
+
+mapping clause assembly = UTYPE(imm, rd, op)
+  <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm)
+
+$counterexample
+function prop(x: string) -> bool = {
+  not_bool(utype_mnemonic(RISCV_LUI) == x)
+}
diff --git a/test/smt/run_tests.py b/test/smt/run_tests.py
index c9cadec3..f59bdba9 100755
--- a/test/smt/run_tests.py
+++ b/test/smt/run_tests.py
@@ -23,7 +23,7 @@ def test_smt(name, solver, sail_opts):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('sail {} -smt {} -o {}'.format(sail_opts, filename, basename))
-                step('timeout 20s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
+                step('timeout 300s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
                 if re.match('.+\.sat\.sail$', filename):
                     step('grep -q ^sat$ {}.out'.format(basename))
                 else:
diff --git a/test/smt/rv_add_0.unsat.sail b/test/smt/rv_add_0.unsat.sail
index 87c55487..ed45112e 100644
--- a/test/smt/rv_add_0.unsat.sail
+++ b/test/smt/rv_add_0.unsat.sail
@@ -145,7 +145,7 @@ function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
 
 function clause decode _ = None()
 
-$counterexample
+$property
 function prop(imm:  bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
   X(rs1) = v;
   match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {