From 2505aecda6715c5ac4dc366ea3a567ea8180eaf1 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 26 Apr 2019 18:33:24 +0100
Subject: Fix boolean short-circuiting operators causing some flow-typing
 unsoundness

---
 test/typecheck/pass/short_circuit_bool_ex.sail     | 36 ++++++++++++++++++++++
 .../typecheck/pass/short_circuit_bool_ex/v1.expect |  8 +++++
 test/typecheck/pass/short_circuit_bool_ex/v1.sail  | 34 ++++++++++++++++++++
 3 files changed, 78 insertions(+)
 create mode 100644 test/typecheck/pass/short_circuit_bool_ex.sail
 create mode 100644 test/typecheck/pass/short_circuit_bool_ex/v1.expect
 create mode 100644 test/typecheck/pass/short_circuit_bool_ex/v1.sail

(limited to 'test/typecheck')

diff --git a/test/typecheck/pass/short_circuit_bool_ex.sail b/test/typecheck/pass/short_circuit_bool_ex.sail
new file mode 100644
index 00000000..5cfdc1dc
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex.sail
@@ -0,0 +1,36 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+
+val assertive : forall 'n. int('n) -> range(0,'n) effect {escape}
+
+function assertive(n) = {
+  assert(n > 0);
+  0
+}
+
+val ok : unit -> bool(0 == 1) effect {escape}
+
+function ok() = {
+  let n = -1;
+  let a = assertive(n) > 0 in
+  if (true | a) then true else true
+}
+
+/*
+val bad : unit -> bool(0 == 1) effect {escape}
+
+function bad() = {
+  let n = -1;
+  if (true | assertive(n) > 0) then true else true
+}
+*/
+
+val main : unit -> unit effect {escape}
+
+function main() =
+  if ok() then
+    print_endline("0 = 1")
+  else
+    print_endline("0 != 1")
\ No newline at end of file
diff --git a/test/typecheck/pass/short_circuit_bool_ex/v1.expect b/test/typecheck/pass/short_circuit_bool_ex/v1.expect
new file mode 100644
index 00000000..fc98db1b
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex/v1.expect
@@ -0,0 +1,8 @@
+Type error:
+[short_circuit_bool_ex/v1.sail]:25:36-40
+25 |  if (true | assertive(n) > 0) then true else true
+   |                                    ^--^
+   | Tried performing type coercion from bool(true) to bool(0 == 1) on true
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/short_circuit_bool_ex/v1.sail b/test/typecheck/pass/short_circuit_bool_ex/v1.sail
new file mode 100644
index 00000000..2faf12af
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex/v1.sail
@@ -0,0 +1,34 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+
+val assertive : forall 'n. int('n) -> range(0,'n) effect {escape}
+
+function assertive(n) = {
+  assert(n > 0);
+  0
+}
+
+val ok : unit -> bool(0 == 1) effect {escape}
+
+function ok() = {
+  let n = -1;
+  let a = assertive(n) > 0 in
+  if (true | a) then true else true
+}
+
+val bad : unit -> bool(0 == 1) effect {escape}
+
+function bad() = {
+  let n = -1;
+  if (true | assertive(n) > 0) then true else true
+}
+
+val main : unit -> unit effect {escape}
+
+function main() =
+  if bad() then
+    print_endline("0 = 1")
+  else
+    print_endline("0 != 1")
\ No newline at end of file
-- 
cgit v1.2.3