Skip to content

Commit 3cf9470

Browse files
mndstrmrmndstrmr
committed
Avoid producing gotos where possible
This makes all codegen generally nicer where possible.
1 parent 0a978e0 commit 3cf9470

File tree

7 files changed

+233
-56
lines changed

7 files changed

+233
-56
lines changed

‎src/lib/jib_compile.ml‎

Lines changed: 172 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -258,6 +258,8 @@ module type CONFIG = sig
258258
val use_real : bool
259259
val branch_coverage : out_channel option
260260
val track_throw : bool
261+
val needs_cleanup : bool
262+
val unreach_exceptions : bool
261263
end
262264

263265
module IdGraph = Graph.Make (Id)
@@ -727,6 +729,126 @@ module Make (C : CONFIG) = struct
727729
end
728730
| AP_nil _ -> ([ijump l (V_call (Bnot, [V_call (List_is_empty, [cval])])) case_label], [], [], ctx)
729731

732+
let rec compile_match_no_jump ctx (AP_aux (apat_aux, env, l)) cval =
733+
let ctx = { ctx with local_env = env } in
734+
let ctyp = cval_ctyp cval in
735+
match apat_aux with
736+
| AP_global (pid, typ) ->
737+
let global_ctyp = ctyp_of_typ ctx typ in
738+
([
739+
(None, [icopy l (CL_id (name pid, global_ctyp)) cval], [])
740+
], ctx)
741+
| AP_id (pid, _) when is_ct_enum ctyp -> begin
742+
match Env.lookup_id pid ctx.tc_env with
743+
| Unbound _ -> ([
744+
(None, [idecl l ctyp (name pid); icopy l (CL_id (name pid, ctyp)) cval], [])
745+
], ctx)
746+
| _ -> ([
747+
(Some (V_call (Neq, [V_id (name pid, ctyp); cval])), [], [])
748+
], ctx)
749+
end
750+
| AP_id (pid, typ) ->
751+
let id_ctyp = ctyp_of_typ ctx typ in
752+
let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in
753+
([
754+
None, [idecl l id_ctyp (name pid); icopy l (CL_id (name pid, id_ctyp)) cval], [iclear id_ctyp (name pid)]
755+
], ctx)
756+
| AP_as (apat, id, typ) ->
757+
let id_ctyp = ctyp_of_typ ctx typ in
758+
let steps, ctx = compile_match_no_jump ctx apat cval in
759+
let ctx = { ctx with locals = Bindings.add id (Immutable, id_ctyp) ctx.locals } in
760+
(
761+
steps @ [(
762+
None, [idecl l id_ctyp (name id); icopy l (CL_id (name id, id_ctyp)) cval], [iclear id_ctyp (name id)]
763+
)], ctx
764+
)
765+
| AP_struct (afpats, _) -> begin
766+
let fold (steps, ctx) (field, apat) =
767+
let steps', ctx = compile_match_no_jump ctx apat (V_field (cval, field)) in
768+
(steps @ steps', ctx)
769+
in
770+
List.fold_left fold ([], ctx) afpats
771+
end
772+
| AP_tuple apats -> begin
773+
let get_tup n = V_tuple_member (cval, List.length apats, n) in
774+
let fold (steps, n, ctx) apat ctyp =
775+
let steps', ctx = compile_match_no_jump ctx apat (get_tup n) in
776+
(steps @ steps', n + 1, ctx)
777+
in
778+
match ctyp with
779+
| CT_tup ctyps ->
780+
let steps, _, ctx = List.fold_left2 fold ([], 0, ctx) apats ctyps in
781+
(steps, ctx)
782+
| _ -> Reporting.unreachable l __POS__ ("AP_tuple with ctyp " ^ string_of_ctyp ctyp)
783+
end
784+
| AP_app (ctor, apat, variant_typ) -> begin
785+
match ctyp with
786+
| CT_variant (var_id, ctors) ->
787+
let pat_ctyp = apat_ctyp ctx apat in
788+
(* These should really be the same, something has gone wrong if they are not. *)
789+
if not (ctyp_equal (cval_ctyp cval) (ctyp_of_typ ctx variant_typ)) then
790+
raise
791+
(Reporting.err_general l
792+
(Printf.sprintf "When compiling constructor pattern, %s should have the same type as %s"
793+
(string_of_ctyp (cval_ctyp cval))
794+
(string_of_ctyp (ctyp_of_typ ctx variant_typ))
795+
)
796+
);
797+
let unifiers, ctor_ctyp =
798+
let generic_ctors = Bindings.find var_id ctx.variants |> snd |> Bindings.bindings in
799+
let unifiers =
800+
ctyp_unify l (CT_variant (var_id, generic_ctors)) (cval_ctyp cval) |> KBindings.bindings |> List.map snd
801+
in
802+
match List.find_opt (fun (id, ctyp) -> Id.compare id ctor = 0 && is_polymorphic ctyp) generic_ctors with
803+
| Some (_, poly_ctor_ctyp) ->
804+
let instantiated_parts = KBindings.map ctyp_suprema (ctyp_unify l poly_ctor_ctyp pat_ctyp) in
805+
(unifiers, subst_poly instantiated_parts poly_ctor_ctyp)
806+
| None -> begin
807+
match List.find_opt (fun (id, _) -> Id.compare id ctor = 0) ctors with
808+
| Some (_, ctor_ctyp) -> (unifiers, ctor_ctyp)
809+
| None ->
810+
Reporting.unreachable l __POS__
811+
("Expected constructor " ^ string_of_id ctor ^ " for " ^ full_string_of_ctyp ctyp)
812+
end
813+
in
814+
let steps, ctx =
815+
compile_match_no_jump ctx apat (V_ctor_unwrap (cval, (ctor, unifiers), ctor_ctyp))
816+
in
817+
(
818+
(
819+
Some (V_ctor_kind (cval, (ctor, unifiers), pat_ctyp)), [], []
820+
) :: steps, ctx
821+
)
822+
| ctyp ->
823+
raise
824+
(Reporting.err_general l
825+
(Printf.sprintf "Variant constructor %s : %s matching against non-variant type %s : %s"
826+
(string_of_id ctor) (string_of_typ variant_typ) (string_of_cval cval) (string_of_ctyp ctyp)
827+
)
828+
)
829+
end
830+
| AP_wild _ -> ([], ctx)
831+
| AP_cons (hd_apat, tl_apat) -> begin
832+
match ctyp with
833+
| CT_list ctyp ->
834+
let hd, ctx = compile_match_no_jump ctx hd_apat (V_call (List_hd, [cval])) in
835+
let tl, ctx = compile_match_no_jump ctx tl_apat (V_call (List_tl, [cval])) in
836+
((Some (V_call (List_is_empty, [cval])), [], []) :: hd @ tl, ctx)
837+
| _ -> raise (Reporting.err_general l "Tried to pattern match cons on non list type")
838+
end
839+
| AP_nil _ -> ([
840+
(Some (V_call (Bnot, [V_call (List_is_empty, [cval])])), [], [])
841+
], ctx)
842+
843+
let compile_match_if_else ctx a cval l tcase =
844+
let steps, ctx = compile_match_no_jump ctx a cval in
845+
let rec fold steps = match steps with
846+
| [] -> tcase
847+
| (Some cond, ds, cl) :: steps -> [iif l (V_call (Bnot, [cond])) (ds @ fold steps @ cl) [] CT_unit]
848+
| (None, ds, cl) :: steps -> ds @ fold steps @ cl
849+
in
850+
(fold steps, ctx)
851+
730852
let unit_cval = V_lit (VL_unit, CT_unit)
731853

732854
let rec compile_alexp ctx alexp =
@@ -768,9 +890,8 @@ module Make (C : CONFIG) = struct
768890
let branch_id, on_reached = coverage_branch_reached ctx l in
769891
let case_return_id = ngensym () in
770892
let finish_match_label = label "finish_match_" in
771-
let compile_case (apat, guard, body) =
772-
let case_label = label "case_" in
773-
if is_dead_aexp body then [ilabel case_label]
893+
let compile_case_else (apat, guard, body) next =
894+
if is_dead_aexp body then next
774895
else (
775896
let trivial_guard =
776897
match guard with
@@ -779,36 +900,41 @@ module Make (C : CONFIG) = struct
779900
true
780901
| _ -> false
781902
in
782-
let pre_destructure, destructure, destructure_cleanup, ctx = compile_match ctx apat cval case_label in
783903
let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in
784904
let body_setup, body_call, body_cleanup = compile_aexp ctx body in
785-
let gs = ngensym () in
905+
let matched = ngensym () in
906+
let tcase =
907+
if not trivial_guard then
908+
guard_setup @ [guard_call (CL_id (matched, CT_bool))] @ guard_cleanup @
909+
[
910+
iif l (V_id (matched, CT_bool))
911+
(body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup)
912+
[]
913+
CT_unit
914+
]
915+
else
916+
[icopy l (CL_id (matched, CT_bool)) (V_lit (VL_bool true, CT_bool))] @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup
917+
in
918+
let check, ctx = compile_match_if_else ctx apat cval l tcase in
786919
let case_instrs =
787-
pre_destructure @ destructure
788-
@ ( if not trivial_guard then
789-
guard_setup
790-
@ [idecl l CT_bool gs; guard_call (CL_id (gs, CT_bool))]
791-
@ guard_cleanup
792-
@ [
793-
iif l (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit;
794-
]
795-
else []
796-
)
797-
@ (if num_cases > 1 then coverage_branch_target_taken ctx branch_id body else [])
798-
@ body_setup
799-
@ [body_call (CL_id (case_return_id, ctyp))]
800-
@ body_cleanup @ destructure_cleanup
801-
@ [igoto finish_match_label]
920+
[
921+
idecl l CT_bool matched;
922+
icopy l (CL_id (matched, CT_bool)) (V_lit (VL_bool false, CT_bool))
923+
] @ check @ [
924+
iif l (V_call (Bnot, [V_id (matched, CT_bool)]))
925+
next
926+
[]
927+
CT_unit
928+
]
802929
in
803-
[iblock case_instrs; ilabel case_label]
930+
case_instrs
804931
)
805932
in
806933
( aval_setup
807934
@ [icomment ("Case with num_cases: " ^ string_of_int num_cases)]
808935
@ (if num_cases > 1 then on_reached else [])
809936
@ [idecl l ctyp case_return_id]
810-
@ List.concat (List.map compile_case cases)
811-
@ [imatch_failure l]
937+
@ (List.fold_right compile_case_else cases [imatch_failure l])
812938
@ [ilabel finish_match_label],
813939
(fun clexp -> icopy l clexp (V_id (case_return_id, ctyp))),
814940
[iclear ctyp case_return_id] @ aval_cleanup
@@ -1031,8 +1157,10 @@ module Make (C : CONFIG) = struct
10311157
(return_setup @ creturn, (fun clexp -> icomment "unreachable after return"), [])
10321158
| AE_throw (aval, typ) ->
10331159
(* Cleanup info will be handled by fix_exceptions *)
1034-
let throw_setup, cval, _ = compile_aval l ctx aval in
1035-
(throw_setup @ [ithrow l cval], (fun clexp -> icomment "unreachable after throw"), [])
1160+
if C.unreach_exceptions then ([imatch_failure l], (fun clexp -> icomment "unreachable after throw"), [])
1161+
else
1162+
let throw_setup, cval, _ = compile_aval l ctx aval in
1163+
(throw_setup @ [ithrow l cval], (fun clexp -> icomment "unreachable after throw"), [])
10361164
| AE_exit (aval, typ) ->
10371165
let exit_setup, cval, _ = compile_aval l ctx aval in
10381166
(exit_setup @ [iexit l], (fun clexp -> icomment "unreachable after exit"), [])
@@ -1086,21 +1214,24 @@ module Make (C : CONFIG) = struct
10861214
@ [
10871215
iblock
10881216
([
1089-
ijump l
1090-
(V_call ((if is_inc then Igt else Ilt), [V_id (loop_var, CT_fint 64); V_id (to_gs, CT_fint 64)]))
1091-
loop_end_label;
1217+
iif l
1218+
(V_call (Bnot, [V_call ((if is_inc then Igt else Ilt), [V_id (loop_var, CT_fint 64); V_id (to_gs, CT_fint 64)])]))
1219+
(
1220+
body_setup
1221+
@ [body_call (CL_id (body_gs, CT_unit))]
1222+
@ body_cleanup
1223+
@ [
1224+
icopy l
1225+
(CL_id (loop_var, CT_fint 64))
1226+
(V_call
1227+
((if is_inc then Iadd else Isub), [V_id (loop_var, CT_fint 64); V_id (step_gs, CT_fint 64)])
1228+
);
1229+
]
1230+
@ continue ()
1231+
)
1232+
[]
1233+
CT_unit
10921234
]
1093-
@ body_setup
1094-
@ [body_call (CL_id (body_gs, CT_unit))]
1095-
@ body_cleanup
1096-
@ [
1097-
icopy l
1098-
(CL_id (loop_var, CT_fint 64))
1099-
(V_call
1100-
((if is_inc then Iadd else Isub), [V_id (loop_var, CT_fint 64); V_id (step_gs, CT_fint 64)])
1101-
);
1102-
]
1103-
@ continue ()
11041235
);
11051236
]
11061237
in
@@ -1461,9 +1592,9 @@ module Make (C : CONFIG) = struct
14611592
@ [call (CL_id (return, ret_ctyp))]
14621593
@ cleanup @ destructure_cleanup @ arg_cleanup
14631594
in
1464-
let instrs = fix_early_return (exp_loc exp) (CL_id (return, ret_ctyp)) instrs in
1595+
let instrs = if C.needs_cleanup then fix_early_return (exp_loc exp) (CL_id (return, ret_ctyp)) instrs else instrs @ [iend def_annot.loc] in
14651596
let instrs = unique_names instrs in
1466-
let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in
1597+
let instrs = if C.unreach_exceptions then instrs else fix_exception ~return:(Some ret_ctyp) ctx instrs in
14671598
let instrs = coverage_function_entry ctx id (exp_loc exp) @ instrs in
14681599

14691600
if Option.is_some debug_attr then (

‎src/lib/jib_compile.mli‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -158,6 +158,12 @@ module type CONFIG = sig
158158
for debugging C but we want to turn it off for SMT generation
159159
where we can't use strings *)
160160
val track_throw : bool
161+
162+
(* If false then cleanup code may be omitted *)
163+
val needs_cleanup : bool
164+
165+
(* If true, then exceptions become assertions for unreachability *)
166+
val unreach_exceptions : bool
161167
end
162168

163169
module IdGraph : sig

‎src/lib/jib_optimize.ml‎

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -105,16 +105,17 @@ let rec flatten_instrs = function
105105
let fid = flat_id () in
106106
I_aux (I_init (ctyp, fid, cval), aux) :: flatten_instrs (instrs_rename decl_id fid instrs)
107107
| I_aux ((I_block block | I_try_block block), _) :: instrs -> flatten_instrs block @ flatten_instrs instrs
108-
| I_aux (I_if (cval, then_instrs, else_instrs, _), (_, l)) :: instrs ->
109-
let then_label = label "then_" in
110-
let endif_label = label "endif_" in
111-
[ijump l cval then_label]
112-
@ flatten_instrs else_instrs
113-
@ [igoto endif_label]
114-
@ [ilabel then_label]
115-
@ flatten_instrs then_instrs
116-
@ [ilabel endif_label]
117-
@ flatten_instrs instrs
108+
| I_aux (I_if (cval, then_instrs, else_instrs, t), a) :: instrs ->
109+
I_aux (I_if (cval, flatten_instrs then_instrs, flatten_instrs else_instrs, t), a) :: flatten_instrs instrs
110+
(* let then_label = label "then_" in *)
111+
(* let endif_label = label "endif_" in *)
112+
(* [ijump l cval then_label] *)
113+
(* @ flatten_instrs else_instrs *)
114+
(* @ [igoto endif_label] *)
115+
(* @ [ilabel then_label] *)
116+
(* @ flatten_instrs then_instrs *)
117+
(* @ [ilabel endif_label] *)
118+
(* @ flatten_instrs instrs *)
118119
| I_aux (I_comment _, _) :: instrs -> flatten_instrs instrs
119120
| instr :: instrs -> instr :: flatten_instrs instrs
120121
| [] -> []

‎src/sail_c_backend/c_backend.ml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -593,6 +593,8 @@ end) : CONFIG = struct
593593
let use_real = false
594594
let branch_coverage = Opts.branch_coverage
595595
let track_throw = true
596+
let needs_cleanup = true
597+
let unreach_exceptions = false
596598
end
597599

598600
(** Functions that have heap-allocated return types are implemented by

‎src/sail_smt_backend/jib_smt.ml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1557,6 +1557,8 @@ end) : Jib_compile.CONFIG = struct
15571557
let use_real = true
15581558
let branch_coverage = None
15591559
let track_throw = false
1560+
let needs_cleanup = false
1561+
let unreach_exceptions = false
15601562
end
15611563

15621564
(**************************************************************************)

‎src/sail_sv_backend/jib_sv.ml‎

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -743,8 +743,13 @@ module Make (Config : CONFIG) = struct
743743
| I_raw s -> return (string s ^^ semi)
744744
| I_undefined ctyp ->
745745
Reporting.unreachable l __POS__ "Unreachable instruction should not reach SystemVerilog backend"
746-
| I_jump _ | I_goto _ | I_label _ ->
747-
Reporting.unreachable l __POS__ "Non-structured control flow should not reach SystemVerilog backend"
746+
| I_jump (_, lab) ->
747+
return (string "/* conditional jump to " ^^ string lab ^^ string " */")
748+
| I_goto lab ->
749+
return (string "/* jump to " ^^ string lab ^^ string " */")
750+
(* Reporting.unreachable l __POS__ "Non-structured control flow should not reach SystemVerilog backend" *)
751+
| I_label lab ->
752+
return (string "/* label: " ^^ string lab ^^ string " */")
748753
| I_throw _ | I_try_block _ ->
749754
Reporting.unreachable l __POS__ "Exception handling should not reach SystemVerilog backend"
750755
| I_clear _ | I_reset _ | I_reinit _ ->
@@ -787,11 +792,12 @@ module Make (Config : CONFIG) = struct
787792

788793
let filter_clear = filter_instrs (function I_aux (I_clear _, _) -> false | _ -> true)
789794

790-
let variable_decls_to_top instrs =
795+
let rec variable_decls_to_top instrs =
791796
let decls, others =
792797
List.fold_left
793798
(fun (decls, others) instr ->
794799
match instr with
800+
| I_aux (I_if (cval, tcase, fcase, t), a) -> (decls, I_aux (I_if (cval, variable_decls_to_top tcase, variable_decls_to_top fcase, t), a) :: others)
795801
| I_aux (I_decl (ctyp, id), (_, l)) -> (idecl l ctyp id :: decls, others)
796802
| I_aux (I_init (ctyp, id, cval), (_, l)) ->
797803
(idecl l ctyp id :: decls, icopy l (CL_id (id, ctyp)) cval :: others)
@@ -920,8 +926,12 @@ module Make (Config : CONFIG) = struct
920926
else (
921927
let body =
922928
Jib_optimize.(
923-
body |> flatten_instrs |> remove_dead_code |> variable_decls_to_top |> structure_control_flow_block
924-
|> remove_undefined |> filter_clear
929+
body
930+
|> flatten_instrs
931+
|> remove_dead_code
932+
|> remove_undefined
933+
|> filter_clear
934+
|> variable_decls_to_top
925935
)
926936
in
927937
begin

0 commit comments

Comments
 (0)