From 3ec7f6d6373b6b8b5011daecbcf712f5a9d2dc7c Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 27 Mar 2020 01:19:40 +0000
Subject: Be more careful when flow-typing loops

Asserting constraints from the loop condition in the body is fine for
while-loops, but doesn't make sense for until-loops.
---
 src/type_check.ml                               | 6 +++++-
 test/typecheck/pass/repeat_constraint.sail      | 9 +++++++++
 test/typecheck/pass/repeat_constraint/v1.expect | 6 ++++++
 test/typecheck/pass/repeat_constraint/v1.sail   | 9 +++++++++
 4 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 test/typecheck/pass/repeat_constraint.sail
 create mode 100644 test/typecheck/pass/repeat_constraint/v1.expect
 create mode 100644 test/typecheck/pass/repeat_constraint/v1.sail

diff --git a/src/type_check.ml b/src/type_check.ml
index 82bc92d8..08b6eb5a 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3882,7 +3882,11 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        | Measure_aux (Measure_some exp,l) ->
           Measure_aux (Measure_some (crule check_exp env exp int_typ),l)
      in
-     let checked_body = crule check_exp (add_opt_constraint (assert_constraint env true checked_cond) env) body unit_typ in
+     let nc = match loop_type with
+       | While -> assert_constraint env true checked_cond
+       | Until -> None
+     in
+     let checked_body = crule check_exp (add_opt_constraint nc env) body unit_typ in
      annot_exp (E_loop (loop_type, checked_measure, checked_cond, checked_body)) unit_typ
   | E_for (v, f, t, step, ord, body) ->
      begin
diff --git a/test/typecheck/pass/repeat_constraint.sail b/test/typecheck/pass/repeat_constraint.sail
new file mode 100644
index 00000000..6d63f2e8
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint.sail
@@ -0,0 +1,9 @@
+$include <flow.sail>
+
+val main : unit -> unit
+
+function main() = {
+  repeat {
+    _not_prove(constraint(false));
+  } until (false);
+}
diff --git a/test/typecheck/pass/repeat_constraint/v1.expect b/test/typecheck/pass/repeat_constraint/v1.expect
new file mode 100644
index 00000000..9d561e11
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint/v1.expect
@@ -0,0 +1,6 @@
+Type error:
+[repeat_constraint/v1.sail]:7:4-29
+7 |    _prove(constraint(false));
+  |    ^-----------------------^
+  | Cannot prove false
+  | 
diff --git a/test/typecheck/pass/repeat_constraint/v1.sail b/test/typecheck/pass/repeat_constraint/v1.sail
new file mode 100644
index 00000000..5dd2f513
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint/v1.sail
@@ -0,0 +1,9 @@
+$include <flow.sail>
+
+val main : unit -> unit
+
+function main() = {
+  repeat {
+    _prove(constraint(false));
+  } until (false);
+}
-- 
cgit v1.2.3