summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-02-20 14:18:49 +0000
committerAlasdair Armstrong2019-02-20 14:21:23 +0000
commita45ce2aecdd27de565dd32d42c8c79d10e2edd0a (patch)
tree379ef84eae44cb28ce8b6730f94a2f82f780bd04 /test
parentfc7d360e9442ab2e945e0d2da97faaf0eefec66f (diff)
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.
Diffstat (limited to 'test')
-rw-r--r--test/c/dead_branch.expect2
-rw-r--r--test/c/dead_branch.sail42
2 files changed, 44 insertions, 0 deletions
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);
+ ()
+}