diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/jib_compile.mli | 7 | ||||
| -rw-r--r-- | src/jib/jib_optimize.ml | 12 |
2 files changed, 13 insertions, 6 deletions
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index 6269b40d..c863b6ba 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -83,10 +83,9 @@ val initial_ctx : Env.t -> ctx (** {2 Compilation functions} *) (** The Config module specifies static configuration for compiling - Sail into Jib. We have to provide a conversion - function from Sail types into Jib types, as well as a function that - optimizes ANF expressions (which can just be the identity function) - *) + Sail into Jib. We have to provide a conversion function from Sail + types into Jib types, as well as a function that optimizes ANF + expressions (which can just be the identity function) *) module type Config = sig val convert_typ : ctx -> typ -> ctyp val optimize_anf : ctx -> typ aexp -> typ aexp diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml index 82906cb6..f4d9c9c2 100644 --- a/src/jib/jib_optimize.ml +++ b/src/jib/jib_optimize.ml @@ -345,6 +345,15 @@ let rec remove_pointless_goto = function instr :: remove_pointless_goto instrs | [] -> [] +let rec remove_pointless_exit = function + | I_aux (I_end id, aux) :: I_aux (I_end _, _) :: instrs -> + I_aux (I_end id, aux) :: remove_pointless_exit instrs + | I_aux (I_end id, aux) :: I_aux (I_undefined _, _) :: instrs -> + I_aux (I_end id, aux) :: remove_pointless_exit instrs + | instr :: instrs -> + instr :: remove_pointless_exit instrs + | [] -> [] + module StringSet = Set.Make(String) let rec get_used_labels set = function @@ -362,7 +371,6 @@ let remove_unused_labels instrs = in go [] instrs - let remove_dead_after_goto instrs = let rec go acc = function | (I_aux (I_goto _, _) as instr) :: instrs -> go_dead (instr :: acc) instrs @@ -377,7 +385,7 @@ let remove_dead_after_goto instrs = let rec remove_dead_code instrs = let instrs' = - instrs |> remove_unused_labels |> remove_pointless_goto |> remove_dead_after_goto + instrs |> remove_unused_labels |> remove_pointless_goto |> remove_dead_after_goto |> remove_pointless_exit in if List.length instrs' < List.length instrs then remove_dead_code instrs' |