SMT: Fix error in get_pathcond

2 files changed, 72 insertions, 9 deletions

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 3b42e749..d73d1a02 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1284,25 +1284,24 @@ let smt_ssanode ctx cfg preds =
 
 let rec get_pathcond n cfg ctx =
   let open Jib_ssa in
+  let get_pi m =
+    match get_vertex cfg m with
+    | Some ((ssanodes, _), _, _) ->
+       V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes))
+    | None -> failwith "Node does not exist"
+  in
   match get_vertex cfg n with
   | Some ((_, CF_guard cond), _, _) ->
-     smt_cval ctx (get_cond cfg cond)
+     smt_cval ctx (get_pi n)
   | Some (_, preds, succs) ->
      if IntSet.cardinal preds = 0 then
        Bool_lit true
      else if IntSet.cardinal preds = 1 then
        get_pathcond (IntSet.min_elt preds) cfg ctx
      else
-       let get_pi m =
-         match get_vertex cfg m with
-         | Some ((ssanodes, _), _, _) ->
-            V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes))
-         | None -> failwith "Predecessor node does not exist"
-       in
        let pis = List.map get_pi (IntSet.elements preds) in
-       prerr_endline (string_of_int n ^ string_of_cval (V_call (Bor, pis)));
        smt_cval ctx (V_call (Bor, pis))
-       
+
   | None -> assert false (* Should never be called for a non-existent node *)
 
 (* For any complex l-expression we need to turn it into a
diff --git a/test/smt/assembly_mapping.sat.sail b/test/smt/assembly_mapping.sat.sail
new file mode 100644
index 00000000..a7b0bec5
--- /dev/null
+++ b/test/smt/assembly_mapping.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(assembly(UTYPE(0x00000, 0b00000, RISCV_LUI)) == x)
+}