From a45ce2aecdd27de565dd32d42c8c79d10e2edd0a Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 20 Feb 2019 14:18:49 +0000
Subject: Remove dead branches when compiling to C

Specifically remove branches where flow-typing implies false, as this
allows the optimizer to prove anything, which can result in nonsense
code. This does incur something of a performance hit.
---
 src/anf.ml                |  2 ++
 src/anf.mli               |  2 ++
 src/c_backend.ml          | 36 ++++++++++++++++++++++--------------
 test/c/dead_branch.expect |  2 ++
 test/c/dead_branch.sail   | 42 ++++++++++++++++++++++++++++++++++++++++++
 5 files changed, 70 insertions(+), 14 deletions(-)
 create mode 100644 test/c/dead_branch.expect
 create mode 100644 test/c/dead_branch.sail

diff --git a/src/anf.ml b/src/anf.ml
index 38c77e0b..5db836e9 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -436,6 +436,8 @@ and pp_aval = function
 
 let ae_lit lit typ = AE_val (AV_lit (lit, typ))
 
+let is_dead_aexp (AE_aux (_, env, _)) = prove __POS__ env nc_false
+
 (** GLOBAL: gensym_counter is used to generate fresh identifiers where
    needed. It should be safe to reset between top level
    definitions. **)
diff --git a/src/anf.mli b/src/anf.mli
index 5e162b7c..6b9c9b51 100644
--- a/src/anf.mli
+++ b/src/anf.mli
@@ -112,6 +112,8 @@ val apat_globals : 'a apat -> (id * 'a) list
 
 val apat_types : 'a apat -> 'a Bindings.t
 
+val is_dead_aexp : 'a aexp -> bool
+
 (* Compiling to ANF expressions *)
 
 val anf_pat : ?global:bool -> tannot pat -> typ apat
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 2981660e..fd728111 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1083,7 +1083,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let compile_case (apat, guard, body) =
        let trivial_guard = match guard with
          | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _)
-         | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true
+           | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true
          | _ -> false
        in
        let case_label = label "case_" in
@@ -1103,7 +1103,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
          @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
          @ [igoto finish_match_label]
        in
-       [iblock case_instrs; ilabel case_label]
+       if is_dead_aexp body then
+         [ilabel case_label]
+       else
+         [iblock case_instrs; ilabel case_label]
      in
      [icomment "begin match"]
      @ aval_setup @ [idecl ctyp case_return_id]
@@ -1159,18 +1162,23 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      []
 
   | AE_if (aval, then_aexp, else_aexp, if_typ) ->
-     let if_ctyp = ctyp_of_typ ctx if_typ in
-     let compile_branch aexp =
-       let setup, call, cleanup = compile_aexp ctx aexp in
-       fun clexp -> setup @ [call clexp] @ cleanup
-     in
-     let setup, cval, cleanup = compile_aval l ctx aval in
-     setup,
-     (fun clexp -> iif cval
-                       (compile_branch then_aexp clexp)
-                       (compile_branch else_aexp clexp)
-                       if_ctyp),
-     cleanup
+     if is_dead_aexp then_aexp then
+       compile_aexp ctx else_aexp
+     else if is_dead_aexp else_aexp then
+       compile_aexp ctx then_aexp
+     else
+       let if_ctyp = ctyp_of_typ ctx if_typ in
+       let compile_branch aexp =
+         let setup, call, cleanup = compile_aexp ctx aexp in
+         fun clexp -> setup @ [call clexp] @ cleanup
+       in
+       let setup, cval, cleanup = compile_aval l ctx aval in
+       setup,
+       (fun clexp -> iif cval
+                         (compile_branch then_aexp clexp)
+                         (compile_branch else_aexp clexp)
+                         if_ctyp),
+       cleanup
 
   (* FIXME: AE_record_update could be AV_record_update - would reduce some copying. *)
   | AE_record_update (aval, fields, typ) ->
diff --git a/test/c/dead_branch.expect b/test/c/dead_branch.expect
new file mode 100644
index 00000000..ca6ef09a
--- /dev/null
+++ b/test/c/dead_branch.expect
@@ -0,0 +1,2 @@
+v = 0x5678EF91
+v = 0xABCD12345678EF91
diff --git a/test/c/dead_branch.sail b/test/c/dead_branch.sail
new file mode 100644
index 00000000..4d7900eb
--- /dev/null
+++ b/test/c/dead_branch.sail
@@ -0,0 +1,42 @@
+default Order dec
+
+$include <arith.sail>
+$include <vector_dec.sail>
+
+type xlen : Int = 32
+type xlenbits = bits(xlen)
+
+register reg : bits(64)
+
+function read_xlen (arg : bool) -> xlenbits = {
+  match (arg, sizeof(xlen)) {
+    (_, 32) => reg[31 .. 0],
+    (_, 64) => reg,
+    (_, _)  => if   sizeof(xlen) == 32
+               then reg[31 .. 0]
+	       else reg[63 .. 32]
+  }
+}
+
+type ylen : Int = 64
+type ylenbits = bits(ylen)
+
+function read_ylen (arg : bool) -> ylenbits = {
+  match (arg, sizeof(ylen)) {
+    (_, 32) => reg[31 .. 0],
+    (_, 64) => reg,
+    (_, _)  => if   sizeof(ylen) == 32
+               then reg[31 .. 0]
+	       else reg
+  }
+}
+
+val main : unit -> unit effect {rreg, wreg}
+function main() = {
+  reg = 0xABCD_1234_5678_EF91;
+  let v = read_xlen(true);
+  print_bits("v = ", v);
+  let v = read_ylen(true);
+  print_bits("v = ", v);
+  ()
+}
-- 
cgit v1.2.3