From ef81395ecfaaec11f49a62834cf01bc52dd5d91a Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 21 Feb 2020 14:18:09 +0000
Subject: Nl_flow: Consider early returns

Tells the typechecker that, for example, in a block after

  if (i < 0) then {
    return ();
  } else {
    ...
  }

the constraint not(i < 0) holds.  This is a useful pattern when
type-checking code generated from ASL.
---
 src/nl_flow.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/nl_flow.ml b/src/nl_flow.ml
index 6196f23b..24ef73fa 100644
--- a/src/nl_flow.ml
+++ b/src/nl_flow.ml
@@ -60,6 +60,13 @@ let rec escapes (E_aux (aux, _)) =
   | E_block exps -> escapes (List.hd (List.rev exps))
   | _ -> false
 
+let rec returns (E_aux (aux, _)) =
+  match aux with
+  | E_return _ -> true
+  | E_block [] -> false
+  | E_block exps -> returns (List.hd (List.rev exps))
+  | _ -> false
+
 let is_bitvector_literal (L_aux (aux, _)) =
   match aux with
   | L_bin _ | L_hex _ -> true
@@ -112,6 +119,12 @@ let analyze' exps =
         List.map (modify_unsigned id value) exps
      | _ -> exps
      end
+  | (E_aux (E_if (cond, then_exp, _), (l, _)) as exp) :: next :: rest
+    when returns then_exp ->
+     let msg = mk_lit_exp (L_string "") in
+     let not_cond = locate (fun _ -> gen_loc l) (mk_exp (E_app (mk_id "not_bool", [cond]))) in
+     let assertion = locate (fun _ -> gen_loc l) (mk_exp (E_assert (not_cond, msg))) in
+     exp :: assertion :: next :: rest
   | _ -> exps
 
 let analyze exps =
-- 
cgit v1.2.3