From c6e45fee454c68b2102ddbfc14c488cedc8d7d30 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 6 Sep 2024 00:57:39 +0100 Subject: [PATCH] SV: Order phi functions using original variable locations --- src/lib/jib_compile.ml | 16 ++++++++--- src/sail_sv_backend/jib_sv.ml | 43 +++++++++++++++++++++--------- src/sail_sv_backend/sv_optimize.ml | 6 +---- test/c/split.sail | 1 + 4 files changed, 44 insertions(+), 22 deletions(-) diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 0691334cc..79b16271d 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -893,9 +893,7 @@ module Make (C : CONFIG) = struct [iblock case_instrs; ilabel case_label] ) in - ( aval_setup - @ [icomment ("Case with num_cases: " ^ string_of_int num_cases)] - @ on_reached + ( aval_setup @ on_reached @ [idecl l ctyp case_return_id] @ List.concat (List.map compile_case cases) @ (if Option.is_some (get_attribute "complete" uannot) then [] else [imatch_failure l]) @@ -1254,7 +1252,17 @@ module Make (C : CONFIG) = struct (* We can either generate an actual loop body for C, or unroll the body for SMT *) let actual = loop_body [ilabel loop_start_label] (fun () -> [igoto loop_start_label]) in let rec unroll max n = loop_body [] (fun () -> if n < max then unroll max (n + 1) else [imatch_failure l]) in - let body = match C.unroll_loops with Some times -> unroll times 0 | None -> actual in + let body = + match (get_attribute "unroll" uannot, C.unroll_loops) with + | Some attr_data_opt, Some _ -> ( + match attr_data_opt with + | _, Some (AD_aux (AD_num times, _)) -> unroll (Big_int.to_int times) 0 + | _, Some (AD_aux (_, l)) -> raise (Reporting.err_general l "Invalid argument on unroll attribute") + | l, None -> raise (Reporting.err_general l "Expected numeric argument for unroll attribute") + ) + | None, Some times -> unroll times 0 + | _ -> actual + in ( variable_init from_gs from_setup from_call from_cleanup @ variable_init to_gs to_setup to_call to_cleanup diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml index af6894c42..490519b04 100644 --- a/src/sail_sv_backend/jib_sv.ml +++ b/src/sail_sv_backend/jib_sv.ml @@ -336,7 +336,6 @@ let collect_spec_info ctx cdefs = match cdef with | CDEF_aux (CDEF_fundef (f, _, _, body), _) -> let direct_footprint = empty_direct_footprint () in - prerr_endline ("visit " ^ string_of_id f); let _ = visit_cdef (new footprint_visitor ctx registers direct_footprint) cdef in CTSet.iter (fun ctyp -> @@ -1382,7 +1381,6 @@ module Make (Config : CONFIG) = struct | I_funcall (CR_one clexp, ext, (f, []), args) -> begin match Bindings.find_opt f spec_info.footprints with | Some footprint -> - prerr_endline ("Threading " ^ string_of_id f); let reads = List.map (fun id -> V_id (Name (id, -1), Bindings.find id spec_info.registers)) @@ -1452,10 +1450,7 @@ module Make (Config : CONFIG) = struct ) else SkipChildren ) - else ( - prerr_endline ("No footprint: " ^ string_of_id f); - SkipChildren - ) + else SkipChildren end | _ -> DoChildren end @@ -1612,14 +1607,25 @@ module Make (Config : CONFIG) = struct (fun pred -> match get_vertex cfg pred with Some ((_, CF_block (_, T_exit _)), _, _) -> true | _ -> false) preds - let natural_name_compare n1 n2 = + let natural_name_compare variable_locations n1 n2 = + let open Lexing in + let name_compare id1 id2 ssa_num1 ssa_num2 = + let c = natural_id_compare id1 id2 in + if c <> 0 then c else Int.compare ssa_num1 ssa_num2 + in match (n1, n2) with - | Name (id1, ssa_num1), Name (id2, ssa_num2) when ssa_num1 = ssa_num2 -> natural_id_compare id1 id2 + | Name (id1, ssa_num1), Name (id2, ssa_num2) -> ( + let get_pos id = Option.bind (Bindings.find_opt id variable_locations) Reporting.simp_loc in + match (get_pos id1, get_pos id2) with + | Some (p1, _), Some (p2, _) -> + let c = Int.compare p1.pos_cnum p2.pos_cnum in + if c <> 0 then c else name_compare id1 id2 ssa_num1 ssa_num2 + | _ -> name_compare id1 id2 ssa_num1 ssa_num2 + ) | _ -> Name.compare n1 n2 let svir_module ?debug_attr ?(footprint = pure_footprint) ?(return_vars = [Jib_util.return]) spec_info ctx name params param_ctyps ret_ctyps body = - prerr_endline Util.(string_of_sv_name name |> red |> clear); let footprint, is_recursive = match name with | SVN_id id -> @@ -1643,9 +1649,6 @@ module Make (Config : CONFIG) = struct Queue.add stmt always_comb in - List.iter prerr_endline - (List.map (fun (I_aux (_, (_, l)) as instr) -> string_of_instr instr ^ " " ^ Reporting.short_loc_to_string l) body); - let open Jib_ssa in let _, end_node, cfg = ssa @@ -1667,6 +1670,16 @@ module Make (Config : CONFIG) = struct ) in + let variable_locations = ref Bindings.empty in + List.iter + (iter_instr (function + | I_aux (I_decl (_, Name (id, _)), (_, l)) | I_aux (I_init (_, Name (id, _), _), (_, l)) -> + variable_locations := Bindings.add id l !variable_locations + | _ -> () + ) + ) + body; + let phivars = ref (-1) in let phivar () = incr phivars; @@ -1718,6 +1731,11 @@ module Make (Config : CONFIG) = struct pathconds in let* muxers = fmap Util.option_these (mapM (smt_ssanode cfg pathcond_vars) ssa_elems) in + let muxers = + List.stable_sort + (fun (id1, _, _) (id2, _, _) -> natural_name_compare !variable_locations id1 id2) + muxers + in List.iter (fun (id, ctyp, mux) -> add_comb_statement @@ -1737,7 +1755,6 @@ module Make (Config : CONFIG) = struct in let final_names = get_final_names !ssa_vars cfg in - NameMap.iter (fun x y -> prerr_endline (string_of_name x ^ " -> " ^ string_of_name y)) final_names; (* Create the always_comb definition, lifting/hoisting the module instantations out of the block *) let module_instantiations = Queue.create () in diff --git a/src/sail_sv_backend/sv_optimize.ml b/src/sail_sv_backend/sv_optimize.ml index f52fe3f5f..36d26ea7f 100644 --- a/src/sail_sv_backend/sv_optimize.ml +++ b/src/sail_sv_backend/sv_optimize.ml @@ -671,11 +671,7 @@ module RemoveUnusedVariables = struct let uses = Hashtbl.create 4096 in defs_uses (ref []) uses defs; let defs = visit_sv_defs (new remove_unused_visitor uses changes skip) defs in - if !changes > 0 then ( - prerr_endline (Printf.sprintf "Made %d changes" !changes); - go defs - ) - else defs + if !changes > 0 then go defs else defs in let defs = go defs in visit_sv_defs (new unnumber_var_visitor) defs diff --git a/test/c/split.sail b/test/c/split.sail index 90c9897ad..24ce9a1c9 100644 --- a/test/c/split.sail +++ b/test/c/split.sail @@ -11,6 +11,7 @@ val split : forall 'n 'm, 'n * 'm == 64 & 'n in {1, 2, 4, 8}. (int('n), int('m), function split(n, m, bv) = { var result: vector('n, dec, bits('m)) = undefined; + $[unroll 8] foreach (i from 0 to (n - 1)) { result[i] = sail_shiftright(bv, i * m)[m - 1 .. 0] };