SMT: Provide a more useful error message when topsort fails

3 files changed, 17 insertions, 2 deletions

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index d48ecd9a..ee2e7fc9 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1410,6 +1410,7 @@ let smt_header ctx stack cdefs =
      Declare_tuple 3;
      Declare_tuple 4;
      Declare_tuple 5;
+     Declare_tuple 6;
      declare_datatypes (mk_record "Bits" [("len", Bitvec ctx.lbits_index);
                                           ("contents", Bitvec (lbits_size ctx))])
 
@@ -1504,7 +1505,17 @@ let smt_cdef props lets name_file ctx all_cdefs = function
 
         let open Jib_ssa in
         let start, cfg = ssa instrs in
-        let visit_order = topsort cfg in
+        let visit_order =
+          try topsort cfg with
+          | Not_a_DAG n ->
+             let gv_file = string_of_id function_id ^ ".gv" in
+             let out_chan = open_out gv_file in
+             make_dot out_chan cfg;
+             close_out out_chan;
+             raise (Reporting.err_general pragma_l
+                      (Printf.sprintf "$%s %s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s"
+                         prop_type (string_of_id function_id) n gv_file))
+        in
 
         List.iter (fun n ->
             begin match get_vertex cfg n with
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 1e008362..ad2302de 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -124,6 +124,8 @@ let reachable roots graph =
   in
   IntSet.iter reachable' roots; !visited
 
+exception Not_a_DAG of int;;
+  
 let topsort graph =
   let marked = ref IntSet.empty in
   let temp_marked = ref IntSet.empty in
@@ -131,7 +133,7 @@ let topsort graph =
 
   let rec visit node =
     if IntSet.mem node !temp_marked then
-      failwith "Not a DAG"
+      raise (Not_a_DAG node)
     else if IntSet.mem node !marked then
       ()
     else
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index 88bb46c0..759e1ccb 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -73,6 +73,8 @@ val add_vertex : 'a -> 'a array_graph -> int
    if either of the vertices do not exist. *)
 val add_edge : int -> int -> 'a array_graph -> unit
 
+exception Not_a_DAG of int
+
 val topsort : 'a array_graph -> int list
 
 type cf_node =