Rewrite topological sorting

Use Tarjan's algorithm for finding strongly connected components (and finding a
topological sorting of components at the same time), in order to properly take
into account mutually recursive functions.  The sorting is stable, i.e.,
definitions are only moved when necessary.  Exceptions to this are statements
that do not have any dependencies: default bitvector order declarations,
operator fixity declarations, and top-level comments.  These are moved to the
beginning (like with the previous sorting implementation).

Any dependency cycles that are found are additionally printed to the console in
dot-format, for easy visualisation with graphviz.

1 files changed, 136 insertions, 251 deletions

diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index b35bc48f..19f7b085 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -64,133 +64,6 @@ let set_to_string n =
   list_to_string (Nameset.elements n)
 
 
-(*Query a spec for its default order if one is provided. Assumes Inc if not *)
-(* let get_default_order_sp (DT_aux(spec,_)) =
-  match spec with
-  | DT_order (Ord_aux(o,_)) ->
-    (match o with
-     | Ord_inc -> Some {order = Oinc}
-     | Ord_dec -> Some { order = Odec}
-     | _ -> Some {order = Oinc})
-  | _ -> None
-
-let get_default_order_def = function
-  | DEF_default def_spec -> get_default_order_sp def_spec
-  | _ -> None
-
-let rec default_order (Defs defs) =
-  match defs with
-  | [] -> { order = Oinc } (*When no order is specified, we assume that it's inc*)
-  | def::defs ->
-    match get_default_order_def def with
-    | None -> default_order (Defs defs)
-    | Some o -> o *)
-
-(*Is within range*)
-
-(* let check_in_range (candidate : big_int) (range : typ) : bool =
-  match range.t with
-  | Tapp("range", [TA_nexp min; TA_nexp max]) | Tabbrev(_,{t=Tapp("range", [TA_nexp min; TA_nexp max])}) ->
-    let min,max = 
-      match min.nexp,max.nexp with
-      | (Nconst min, Nconst max)
-      | (Nconst min, N2n(_, Some max))
-      | (N2n(_, Some min), Nconst max)
-      | (N2n(_, Some min), N2n(_, Some max))
-        -> min, max
-      | (Nneg n, Nconst max) | (Nneg n, N2n(_, Some max))->
-        (match n.nexp with
-         | Nconst abs_min | N2n(_,Some abs_min) ->
-           (minus_big_int abs_min), max
-         | _ -> assert false (*Put a better error message here*))
-      | (Nconst min,Nneg n) | (N2n(_, Some min), Nneg n) ->
-        (match n.nexp with
-         | Nconst abs_max | N2n(_,Some abs_max) ->
-           min, (minus_big_int abs_max)
-         | _ -> assert false (*Put a better error message here*))
-    | (Nneg nmin, Nneg nmax) ->
-      ((match nmin.nexp with
-          | Nconst abs_min | N2n(_,Some abs_min) -> (minus_big_int abs_min)
-          | _ -> assert false (*Put a better error message here*)),
-       (match nmax.nexp with
-        | Nconst abs_max | N2n(_,Some abs_max) -> (minus_big_int abs_max)
-        | _ -> assert false (*Put a better error message here*)))
-    | _ -> assert false        
-    in le_big_int min candidate && le_big_int candidate max
-  | _ -> assert false
-
-(*Rmove me when switch to zarith*)
-let rec power_big_int b n =
-  if eq_big_int n zero_big_int
-  then unit_big_int
-  else mult_big_int b (power_big_int b (sub_big_int n unit_big_int))
-
-let unpower_of_2 b =
-  let two = big_int_of_int 2 in
-  let four = big_int_of_int 4 in
-  let eight = big_int_of_int 8 in
-  let sixteen = big_int_of_int 16 in
-  let thirty_two = big_int_of_int 32 in
-  let sixty_four = big_int_of_int 64 in
-  let onetwentyeight = big_int_of_int 128 in
-  let twofiftysix = big_int_of_int 256 in
-  let fivetwelve = big_int_of_int 512 in
-  let oneotwentyfour = big_int_of_int 1024 in
-  let to_the_sixteen = big_int_of_int 65536 in
-  let to_the_thirtytwo = big_int_of_string "4294967296" in
-  let to_the_sixtyfour = big_int_of_string "18446744073709551616" in
-  let ck i = eq_big_int b i in
-  if      ck unit_big_int     then zero_big_int
-  else if ck two              then unit_big_int
-  else if ck four             then two
-  else if ck eight            then big_int_of_int 3
-  else if ck sixteen          then four
-  else if ck thirty_two       then big_int_of_int 5
-  else if ck sixty_four       then big_int_of_int 6
-  else if ck onetwentyeight   then big_int_of_int 7
-  else if ck twofiftysix      then eight
-  else if ck fivetwelve       then big_int_of_int 9
-  else if ck oneotwentyfour   then big_int_of_int 10
-  else if ck to_the_sixteen   then sixteen
-  else if ck to_the_thirtytwo then thirty_two
-  else if ck to_the_sixtyfour then sixty_four
-  else let rec unpower b power =
-         if eq_big_int b unit_big_int
-         then power
-         else (unpower (div_big_int b  two) (succ_big_int power)) in
-    unpower b zero_big_int
-
-let is_within_range candidate range constraints =
-  let candidate_actual = match candidate.t with
-    | Tabbrev(_,t) -> t
-    | _ -> candidate in
-  match candidate_actual.t with
-  | Tapp("atom", [TA_nexp n]) ->
-    (match n.nexp with
-     | Nconst i | N2n(_,Some i) -> if check_in_range i range then Yes else No
-     | _ -> Maybe)
-  | Tapp("range", [TA_nexp bot; TA_nexp top]) ->
-    (match bot.nexp,top.nexp with
-     | Nconst b, Nconst t | Nconst b, N2n(_,Some t) | N2n(_, Some b), Nconst t | N2n(_,Some b), N2n(_, Some t) ->
-       let at_least_in = check_in_range b range in
-       let at_most_in = check_in_range t range in
-       if at_least_in && at_most_in
-       then Yes
-       else if at_least_in || at_most_in
-       then Maybe
-       else No
-     | _ -> Maybe)
-  | Tapp("vector", [_; TA_nexp size ; _; _]) ->
-    (match size.nexp with
-     | Nconst i | N2n(_, Some i) ->
-       if check_in_range (power_big_int (big_int_of_int 2) i) range
-       then Yes
-       else No
-     | _ -> Maybe)
-  | _ -> Maybe
-
-let is_within_machine64 candidate constraints = is_within_range candidate int64_t constraints *)
-  
 (************************************************************************************************)
 (*FV finding analysis: identifies the free variables of a function, expression, etc *)
 
@@ -313,9 +186,11 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
     fv_of_exp consider_var bound u set e
   | E_app(id,es) ->
     let us = conditional_add_exp bound used id in
+    let us = conditional_add_exp bound us (prepend_id "val:" id) in
     list_fv bound us set es
   | E_app_infix(l,id,r) ->
     let us = conditional_add_exp bound used id in
+    let us = conditional_add_exp bound us (prepend_id "val:" id) in
     list_fv bound us set [l;r]
   | E_if(c,t,e) -> list_fv bound used set [c;t;e]
   | E_for(id,from,to_,by,_,body) ->
@@ -462,8 +337,12 @@ let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_)
     | [] -> failwith "fv_of_fun fell off the end looking for the function name"
     | FCL_aux(FCL_Funcl(id,_),_)::_ -> string_of_id id in
   let base_bounds = match rec_opt with
+    (* Current Sail does not have syntax for declaring functions as recursive,
+       and type checker does not check whether functions are recursive, so
+       just always add a self-dependency of functions on themselves
     | Rec_aux(Ast.Rec_rec,_) -> init_env fun_name
-    | _ -> mt in
+    | _ -> mt*)
+    | _ -> init_env fun_name in
   let base_bounds,ns_r = match tannot_opt with
     | Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ),_) ->
       let bindings = if consider_var then typq_bindings typq else mt in
@@ -575,7 +454,9 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function
   | DEF_val lebind -> ((fun (b,u,_) -> (b,u)) (fv_of_let consider_var mt mt mt lebind))
   | DEF_spec vspec -> fv_of_vspec consider_var vspec
   | DEF_fixity _ -> mt,mt
-  | DEF_overload (id,ids) -> init_env (string_of_id id), List.fold_left (fun ns id -> Nameset.add (string_of_id id) ns) mt ids
+  | DEF_overload (id,ids) ->
+     init_env (string_of_id id),
+     List.fold_left (fun ns id -> Nameset.add ("val:" ^ string_of_id id) ns) mt ids
   | DEF_default def -> mt,mt
   | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef
   | DEF_reg_dec rdec -> fv_of_rd consider_var rdec
@@ -584,129 +465,133 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function
 let group_defs consider_scatter_as_one (Ast.Defs defs) =
   List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs
 
-(*******************************************************************************
- * Reorder defs take 2
-*)
 
-(*remove all of ns1 instances from ns2*)
-let remove_all ns1 ns2 =
-  List.fold_right Nameset.remove (Nameset.elements ns1) ns2
-
-let remove_from_all_uses bs dbts =
-  List.map (fun ((b,uses),d) -> (b,remove_all bs uses),d) dbts
-
-let remove_local_or_lib_vars dbts =
-  let bound_in_dbts = List.fold_right (fun ((b,_),_) bounds -> Nameset.union b bounds) dbts mt in
-  let is_bound_in_defs s = Nameset.mem s bound_in_dbts in
-  let rec remove_from_uses = function
-    | [] -> []
-    | ((b,uses),d)::defs ->
-      ((b,(Nameset.filter is_bound_in_defs uses)),d)::remove_from_uses defs in
-  remove_from_uses dbts
+(*
+ *  Sorting definitions, take 3
+ *)
+
+module Namemap = Map.Make(String)
+(* Nodes are labeled with strings.  A graph is represented as a map associating
+   each node with its sucessors *)
+type graph = Nameset.t Namemap.t
+type node_idx = { index : int; root : int }
+
+(* Find strongly connected components using Tarjan's algorithm.
+   This algorithm also returns a topological sorting of the graph components. *)
+let scc ?(original_order : string list option) (g : graph) =
+  let components = ref [] in
+  let index = ref 0 in
+
+  let stack = ref [] in
+  let push v = (stack := v :: !stack) in
+  let pop () =
+    begin
+      let v = List.hd !stack in
+      stack := List.tl !stack;
+      v
+    end
+  in
 
-let compare_dbts ((_,u1),_) ((_,u2),_) = Pervasives.compare (Nameset.cardinal u1) (Nameset.cardinal u2)
+  let node_indices = Hashtbl.create (Namemap.cardinal g) in
+  let get_index v = (Hashtbl.find node_indices v).index in
+  let get_root v = (Hashtbl.find node_indices v).root in
+  let set_root v r =
+    Hashtbl.replace node_indices v { (Hashtbl.find node_indices v) with root = r } in
+
+  let rec visit_node v =
+    begin
+      Hashtbl.add node_indices v { index = !index; root = !index };
+      index := !index + 1;
+      push v;
+      if Namemap.mem v g then Nameset.iter (visit_edge v) (Namemap.find v g);
+      if get_root v = get_index v then (* v is the root of a SCC *)
+        begin
+          let component = ref [] in
+          let finished = ref false in
+          while not !finished do
+            let w = pop () in
+            component := w :: !component;
+            if String.compare v w = 0 then finished := true;
+          done;
+          components := !component :: !components;
+        end
+    end
+  and visit_edge v w =
+    if not (Hashtbl.mem node_indices w) then
+      begin
+        visit_node w;
+        if Hashtbl.mem node_indices w then set_root v (min (get_root v) (get_root w));
+      end else begin
+        if List.mem w !stack then set_root v (min (get_root v) (get_index w))
+      end
+  in
 
-let rec print_dependencies orig_queue work_queue names =
-  match work_queue with
-  | [] -> ()
-  | ((binds,uses),_)::wq ->
-    (if not(Nameset.is_empty(Nameset.inter names binds))
-     then ((Printf.eprintf "binds of %s has uses of %s\n" (set_to_string binds) (set_to_string uses));
-           print_dependencies orig_queue orig_queue uses));
-    print_dependencies orig_queue wq names
-
-let merge_mutrecs defs =
-  let merge_aux ((binds', uses'), def) ((binds, uses), fundefs) =
-    let fundefs = match def with
-      | DEF_fundef fundef -> fundef :: fundefs
-      | DEF_internal_mutrec fundefs' -> fundefs' @ fundefs
-      | _ ->
-        (* let _ = Pretty_print_sail2.pp_defs stderr (Defs [def]) in *)
-        raise (Reporting_basic.err_unreachable (def_loc def)
-          "Trying to merge non-function definition with mutually recursive functions") in
-    (* let _ = Printf.eprintf " - Merging %s (using %s)\n" (set_to_string binds') (set_to_string uses') in *)
-    ((Nameset.union binds' binds, Nameset.union uses' uses), fundefs) in
-  let ((binds, uses), fundefs) = List.fold_right merge_aux defs ((mt, mt), []) in
-  ((binds, uses), DEF_internal_mutrec fundefs)
-
-let rec topological_sort work_queue defs =
-  match work_queue with
-  | [] -> List.rev defs
-  | ((binds,uses),def)::wq ->
-    (*Assumes work queue given in sorted order, invariant mantained on appropriate recursive calls*)
-    if (Nameset.cardinal uses = 0)
-    then (*let _ = Printf.eprintf "Adding def that binds %s to definitions\n" (set_to_string binds) in*)
-      topological_sort (remove_from_all_uses binds wq) (def::defs)
-    else if not(Nameset.is_empty(Nameset.inter binds uses))
-    then topological_sort (((binds,(remove_all binds uses)),def)::wq) defs
-    else
-      match List.stable_sort compare_dbts work_queue with (*We wait to sort until there are no 0 dependency nodes on top*)
-      | [] -> failwith "sort shrunk the list???"
-      | (((n,uses),def)::rest) as wq ->
-        if (Nameset.cardinal uses = 0)
-        then topological_sort wq defs
-        else
-          let _ = Printf.eprintf "Merging (potentially) mutually recursive definitions %s and %s\n" (set_to_string n) (set_to_string uses) in
-          let is_used ((binds', uses'), def') = not(Nameset.is_empty(Nameset.inter binds' uses)) in
-          let (used, rest) = List.partition is_used rest in
-          let wq = merge_mutrecs (((n,uses),def)::used) :: rest in
-          topological_sort wq defs
-
-let rec add_to_partial_order ((binds,uses),def) = function
-  | [] ->
-(*    let _ = Printf.eprintf "add_to_partial_order for def with bindings %s, uses %s.\n Eol case.\n" (set_to_string binds) (set_to_string uses) in*)
-    [(binds,uses),def]
-  | (((bf,uf),deff)::defs as full_defs) ->
-    (*let _ = Printf.eprintf "add_to_partial_order for def with bindings %s, uses %s.\n None eol case. With first def binding %s, uses %s\n" (set_to_string binds) (set_to_string uses) (set_to_string bf) (set_to_string uf) in*)
-    if Nameset.is_empty uses
-    then ((binds,uses),def)::full_defs
-    else if Nameset.subset binds uf (*deff relies on def, so def must be defined first*)
-    then ((binds,uses),def)::((bf,(remove_all binds uf)),deff)::defs
-    else if Nameset.subset bf uses (*def relies at least on deff, but maybe more, push in*)
-    then ((bf,uf),deff)::(add_to_partial_order ((binds,(remove_all bf uses)),def) defs)
-    else (*These two are unrelated but new def might need to go further in*)
-      ((bf,uf),deff)::(add_to_partial_order ((binds,uses),def) defs)
-
-let rec gather_defs name already_included def_bind_triples =
-  match def_bind_triples with
-  | [] -> [],already_included,mt
-  | ((binds,uses),def)::def_bind_triples ->
-    let (defs,already_included,requires) = gather_defs name already_included def_bind_triples in
-    let bound_names = Nameset.elements binds in
-    if List.mem name already_included || List.exists (fun b -> List.mem b already_included) bound_names 
-    then (defs,already_included,requires)
-    else
-      let uses = List.fold_right Nameset.remove already_included uses in
-      if Nameset.mem name binds
-      then (def::defs,(bound_names@already_included), Nameset.remove name (Nameset.union uses requires))
-      else (defs,already_included,requires)
-
-let rec gather_all names already_included def_bind_triples =
-  let rec gather ns already_included defs reqs = match ns with
-    | [] -> defs,already_included,reqs
-    | name::ns ->
-      if List.mem name already_included
-      then gather ns already_included defs (Nameset.remove name reqs)
-      else
-        let (new_defs,already_included,new_reqs) = gather_defs name already_included def_bind_triples in
-        gather ns already_included (new_defs@defs) (Nameset.remove name (Nameset.union new_reqs reqs))
+  let nodes = match original_order with
+    | Some nodes -> nodes
+    | None -> List.map fst (Namemap.bindings g)
   in
-  let (defs,already_included,reqs) = gather names already_included [] mt in
-  if Nameset.is_empty reqs
-  then defs
-  else (gather_all (Nameset.elements reqs) already_included def_bind_triples)@defs
-    
-let restrict_defs defs name_list =
-  let defsno = gather_all name_list [] (group_defs false defs) in
-  let rdbts = group_defs true (Defs defsno) in
-  (*let partial_order =
-    List.fold_left (fun po d -> add_to_partial_order d po) [] rdbts in
-    let defs = List.map snd partial_order in*)
-  let defs = topological_sort (List.sort compare_dbts (remove_local_or_lib_vars rdbts)) [] in
-  Defs defs
-
-
-let top_sort_defs defs =
-  let rdbts = group_defs true defs in
-  let defs = topological_sort (List.stable_sort compare_dbts (remove_local_or_lib_vars rdbts)) [] in
-  Defs defs
+  List.iter (fun v -> if not (Hashtbl.mem node_indices v) then visit_node v) nodes;
+  List.rev !components
+
+let add_def_to_graph (prelude, original_order, defset, graph) d =
+  let bound, used = fv_of_def false true [] d in
+  try
+    (* A definition may bind multiple identifiers, e.g. "let (x, y) = ...".
+       We add all identifiers to the dependency graph as a cycle.  The actual
+       definition is attached to only one of the identifiers, so it will not
+       be duplicated in the final output. *)
+    let id = Nameset.choose bound in
+    let other_ids = Nameset.remove id bound in
+    let graph_id = Namemap.add id (Nameset.union used other_ids) graph in
+    let add_other_node id' g = Namemap.add id' (Nameset.singleton id) g in
+    prelude,
+    original_order @ [id],
+    Namemap.add id d defset,
+    Nameset.fold add_other_node other_ids graph_id
+  with
+  | Not_found ->
+     (* Some definitions do not bind any identifiers at all.  This *should*
+        only happen for default bitvector order declarations, operator fixity
+        declarations, and comments.  The sorting does not (currently) attempt
+        to preserve the positions of these AST nodes; they are collected
+        separately and placed at the beginning of the output.  Comments are
+        currently ignored by the Lem and OCaml backends, anyway.  For
+        default order and fixity declarations, this means that specifications
+        currently have to assume those declarations are moved to the
+        beginning when using a backend that requires topological sorting. *)
+     prelude @ [d], original_order, defset, graph
+
+let print_dot graph component : unit =
+  match component with
+  | root :: _ ->
+     print_endline ("// Dependency cycle including " ^ root);
+     print_endline ("digraph cycle_" ^ root ^ " {");
+     List.iter (fun caller ->
+       let print_edge callee = print_endline ("  \"" ^ caller ^ "\" -> \"" ^ callee ^ "\";") in
+       Namemap.find caller graph
+       |> Nameset.filter (fun id -> List.mem id component)
+       |> Nameset.iter print_edge) component;
+     print_endline "}"
+  | [] -> ()
+
+let def_of_component graph defset comp =
+  let get_def id = if Namemap.mem id defset then [Namemap.find id defset] else [] in
+  match List.concat (List.map get_def comp) with
+  | [] -> []
+  | [def] -> [def]
+  | (def :: _) as defs ->
+     let get_fundefs = function
+       | DEF_fundef fundef -> [fundef]
+       | DEF_internal_mutrec fundefs -> fundefs
+       | _ ->
+          raise (Reporting_basic.err_unreachable (def_loc def)
+            "Trying to merge non-function definition with mutually recursive functions") in
+     let fundefs = List.concat (List.map get_fundefs defs) in
+     print_dot graph (List.map (fun fd -> string_of_id (id_of_fundef fd)) fundefs);
+     [DEF_internal_mutrec fundefs]
+
+let top_sort_defs (Defs defs) =
+  let prelude, original_order, defset, graph =
+    List.fold_left add_def_to_graph ([], [], Namemap.empty, Namemap.empty) defs in
+  let components = scc ~original_order:original_order graph in
+  Defs (prelude @ List.concat (List.map (def_of_component graph defset) components))